Repository navigation
fpga: wasm_module -- the wasm binary container law: LEB128, header, section walk (refs #11781) - #11864
Merged
Conversation
…e header, the section walk (refs #11781, the wasm_interp loader's read side)
Contributor
Summary by t27-beesChecked by the t27 compilert27c parse, parse-complete and typecheck on each changed .t27 file at
Read by the modelThis PR introduces the WebAssembly module container law: LEB128 (unsigned/signed), the magic+version header, and a section walker that refuses truncated sections. It's the binary format foundation for Worth a look
Read: 1 files, +221 -0, the whole diff. Head |
This was referenced Oct 23, 2026
Open
github-actions Bot
pushed a commit
that referenced
this pull request
Oct 25, 2026
…b split that turns fpga-lint green (Closes #12051) (#12059) * elab baseline: rows for wasm_module 6 and wasm_opcodes 149, the two law tables that landed without rows (Closes #12051) Both reached master without rows (#11864, #11867), so the ratchet read them as NEW and the fpga-conformance step has been red on master since (run 40109127962: 431 against 276; 276 + 6 + 149 = 431, no other module moved). The note under the notes mark records the measured shape of each count: one ROWS line with 149 unsized zeros, and src_len unbound in 4 fns plus the 2 condition lines derived from them. No bless, no spec change, no gate change. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * fpga(hdmi_grab): one home per character and the libc tail to specs/t27os, so fpga-lint and the elab ratchet pass (Refs #12171, Refs #12051) fpga-lint has been red on master since #10949 landed hdmi_grab (2026-10-22): gen-verilog copies a t27 char literal verbatim, Verilog reads '0 as an unsized literal, and yosys stopped at line 88 of hdmi_grab.v. Behind that line the same file carried its libc host part (getenv, fork, execve, fopen, main), which cannot be Verilog either, so a compiler fix alone would have moved the error, not removed it. #12171 keeps the compiler side open; this is the spec side. - specs/fpga/hdmi_grab.t27: the ten characters the checker compares bytes against are consts (CH_0 .. CH_SP), one home each; no char literal is left. The host tail (HG_BUF/HG_LIST/HG_CMD/HG_PATH, hg_cat, hg_env, hg_sh, hg_slurp, hg_path, main) left the file. test-report: 14 tests, 14 pass, 0 vacuous. - specs/t27os/hdmi_grab_main.t27 (new, module T27osHdmiGrabMain): that host tail, verbatim, importing hg_* / V_PASS / CH_0 from fpga::hdmi_grab by use, the way plist_main.t27 imports install/release. t27c gen splices the imports into one .zig (use_resolve.rs); zig build-exe -lc builds it (1.9 MB binary, no diagnostics). Two tests on the two helpers it adds (frame path, byte copy): 2 pass, 0 vacuous. - tools/elab_baseline.txt: hdmi_grab 57 -> 5 (431 -> 379), note dated 2026-10-25. The 5: 4 x pixel_at taken by use from vga_text_core (gen-verilog binds no imports) and 1 x nd_len, an unsized array param (#2410). Measured on the regenerated hdmi_grab.v with a master-equivalent t27c: yosys -p "read_verilog -sv -DSIMULATION hdmi_grab.v; hierarchy -top fpga_hdmi_grab" exits 0; grep -c "\$signed('" = 0; iverilog -g2012 -DSIMULATION: 5 error lines without the summary line, as the ratchet counts. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> --------- Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>
github-actions Bot
pushed a commit
that referenced
this pull request
Oct 25, 2026
… frame_main that writes each run's frame to a PPM (Closes #12203) (#12270) * elab baseline: rows for wasm_module 6 and wasm_opcodes 149, the two law tables that landed without rows (Closes #12051) Both reached master without rows (#11864, #11867), so the ratchet read them as NEW and the fpga-conformance step has been red on master since (run 40109127962: 431 against 276; 276 + 6 + 149 = 431, no other module moved). The note under the notes mark records the measured shape of each count: one ROWS line with 149 unsized zeros, and src_len unbound in 4 fns plus the 2 condition lines derived from them. No bless, no spec change, no gate change. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * fpga(hdmi_grab): one home per character and the libc tail to specs/t27os, so fpga-lint and the elab ratchet pass (Refs #12171, Refs #12051) fpga-lint has been red on master since #10949 landed hdmi_grab (2026-10-22): gen-verilog copies a t27 char literal verbatim, Verilog reads '0 as an unsized literal, and yosys stopped at line 88 of hdmi_grab.v. Behind that line the same file carried its libc host part (getenv, fork, execve, fopen, main), which cannot be Verilog either, so a compiler fix alone would have moved the error, not removed it. #12171 keeps the compiler side open; this is the spec side. - specs/fpga/hdmi_grab.t27: the ten characters the checker compares bytes against are consts (CH_0 .. CH_SP), one home each; no char literal is left. The host tail (HG_BUF/HG_LIST/HG_CMD/HG_PATH, hg_cat, hg_env, hg_sh, hg_slurp, hg_path, main) left the file. test-report: 14 tests, 14 pass, 0 vacuous. - specs/t27os/hdmi_grab_main.t27 (new, module T27osHdmiGrabMain): that host tail, verbatim, importing hg_* / V_PASS / CH_0 from fpga::hdmi_grab by use, the way plist_main.t27 imports install/release. t27c gen splices the imports into one .zig (use_resolve.rs); zig build-exe -lc builds it (1.9 MB binary, no diagnostics). Two tests on the two helpers it adds (frame path, byte copy): 2 pass, 0 vacuous. - tools/elab_baseline.txt: hdmi_grab 57 -> 5 (431 -> 379), note dated 2026-10-25. The 5: 4 x pixel_at taken by use from vga_text_core (gen-verilog binds no imports) and 1 x nd_len, an unsized array param (#2410). Measured on the regenerated hdmi_grab.v with a master-equivalent t27c: yosys -p "read_verilog -sv -DSIMULATION hdmi_grab.v; hierarchy -top fpga_hdmi_grab" exits 0; grep -c "\$signed('" = 0; iverilog -g2012 -DSIMULATION: 5 error lines without the summary line, as the ratchet counts. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * fpga(wasm_fb): a 320x200 palette framebuffer in the video raster, and frame_main that writes each run's frame to a PPM (Closes #12203) Three files: - specs/fpga/wasm_fb.t27 (module fpga_wasm_fb): a 320x200 u8 framebuffer FB and a 256-entry u32 palette PAL, scaled 2x into the 640x400 band at rows 40..439 of the 640x480 raster (40 black rows above and below, black at x >= 640). pal_default is a 16-step ramp per colour group, fb_test_pattern paints 20x12 blocks and a gradient below, frame_pixel_at picks the framebuffer or the text raster. The single pixel_at call site is frame_pixel_at. - specs/t27os/frame_main.t27 (module T27osFrameMain): a host program that writes the 640x480 frame to a P6 PPM after every run (FRAME_OUT, default /tmp/t27_frame.ppm). FRAME_MODE=title runs hg_check and exits 1 on any verdict but PASS; FRAME_MODE=pattern paints the pattern and skips hg_check; a bad mode, an unopenable path or a short write exits 2. - tools/elab_baseline.txt: new row `wasm_fb 2` and a dated note, 379 -> 381. Measured: - t27c test-report wasm_fb.t27: 8 of 8 pass, 0 vacuous. - t27c test-report frame_main.t27: 2 of 2 pass, 0 vacuous. - iverilog -g2012 -DSIMULATION on the gen-verilog output: exactly 2 lines, `No function named pixel_at` (the use-taken name, same class as hdmi_grab) and its derived `Unable to elaborate condition expression`. That is the wasm_fb 2 row. - yosys read_verilog -sv + hierarchy -top fpga_wasm_fb: exit 0. - frame_main built with zig 0.16.0; the title run exits 0 with hg_check verdict 0 (PASS); the pattern run exits 0; both PPMs are 921615 bytes (15 header + 640*480*3), and they differ. - ffmpeg converts both PPMs to PNG, 640x480 each. Nothing here is flashed to a board. No hand-written code in another language; the baseline is a data file. Refs #9367; see Trinity-S-AI-DNA/trinity-fpga#917 Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> --------- Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>
github-actions Bot
pushed a commit
that referenced
this pull request
Oct 25, 2026
…lk, function table, exports, data segments (Closes #12201) (#12278) * elab baseline: rows for wasm_module 6 and wasm_opcodes 149, the two law tables that landed without rows (Closes #12051) Both reached master without rows (#11864, #11867), so the ratchet read them as NEW and the fpga-conformance step has been red on master since (run 40109127962: 431 against 276; 276 + 6 + 149 = 431, no other module moved). The note under the notes mark records the measured shape of each count: one ROWS line with 149 unsized zeros, and src_len unbound in 4 fns plus the 2 condition lines derived from them. No bless, no spec change, no gate change. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * fpga(hdmi_grab): one home per character and the libc tail to specs/t27os, so fpga-lint and the elab ratchet pass (Refs #12171, Refs #12051) fpga-lint has been red on master since #10949 landed hdmi_grab (2026-10-22): gen-verilog copies a t27 char literal verbatim, Verilog reads '0 as an unsized literal, and yosys stopped at line 88 of hdmi_grab.v. Behind that line the same file carried its libc host part (getenv, fork, execve, fopen, main), which cannot be Verilog either, so a compiler fix alone would have moved the error, not removed it. #12171 keeps the compiler side open; this is the spec side. - specs/fpga/hdmi_grab.t27: the ten characters the checker compares bytes against are consts (CH_0 .. CH_SP), one home each; no char literal is left. The host tail (HG_BUF/HG_LIST/HG_CMD/HG_PATH, hg_cat, hg_env, hg_sh, hg_slurp, hg_path, main) left the file. test-report: 14 tests, 14 pass, 0 vacuous. - specs/t27os/hdmi_grab_main.t27 (new, module T27osHdmiGrabMain): that host tail, verbatim, importing hg_* / V_PASS / CH_0 from fpga::hdmi_grab by use, the way plist_main.t27 imports install/release. t27c gen splices the imports into one .zig (use_resolve.rs); zig build-exe -lc builds it (1.9 MB binary, no diagnostics). Two tests on the two helpers it adds (frame path, byte copy): 2 pass, 0 vacuous. - tools/elab_baseline.txt: hdmi_grab 57 -> 5 (431 -> 379), note dated 2026-10-25. The 5: 4 x pixel_at taken by use from vga_text_core (gen-verilog binds no imports) and 1 x nd_len, an unsized array param (#2410). Measured on the regenerated hdmi_grab.v with a master-equivalent t27c: yosys -p "read_verilog -sv -DSIMULATION hdmi_grab.v; hierarchy -top fpga_hdmi_grab" exits 0; grep -c "\$signed('" = 0; iverilog -g2012 -DSIMULATION: 5 error lines without the summary line, as the ratchet counts. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * fpga(wasm_module): load a whole .wasm image: LEB128 pairs, section walk, function table, exports, data segments (Closes #12201) The loader walks one module held in a [SRC_MAX]u8 array plus an explicit src_len and returns a ModuleDesc: per-function code ranges and locals vectors, the import function count, exports (name offset, length, kind, index), data segments as (destination, source offset, length) triples, memory and table limits, the start function, and the global and element payload ranges. Failures are named codes: ERR_BAD_MAGIC, ERR_BAD_VERSION, ERR_TRUNCATED, ERR_TOO_MANY, ERR_MALFORMED, ERR_UNSUPPORTED. Never indexes past the array. LEB128 u32, s32 and s33 readers return a (value, n) struct under the 5-byte limit. No new function takes a slice; the existing uleb_read and sleb32_read stay. Struct locals born in loops and branches are declared once at the top of the function body and assigned inside, because gen-verilog hoists only top-level locals. 15 new tests (21 in the spec): the spec appendix LEB vectors, four hand-encoded modules with offsets counted by hand, and the four error codes. Refs #9367; see Trinity-S-AI-DNA/trinity-fpga#917 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> --------- Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The container law for the WASM line: LEB128 unsigned/signed (the spec appendix's own vectors), the magic+version header, the section walk with the truncation refusal (the end sentinel). The consumers: wasm_interp.t27's loader (reads), the future emitter (writes) — the round-trip on the same structures is the law.
6/6 tests, 0 FAIL, 0 vacuous. The sleb32 accumulates in i64 and wraps (the spec's own method — the i32-domain sign-extension shifted the accumulator wrong; found and fixed by the spec's own vectors).
phi^2 + 1/phi^2 = 3 | TRINITY