Repository navigation
elab baseline rows for wasm_module and wasm_opcodes, and the hdmi_grab split that turns fpga-lint green (Closes #12051) - #12059
Conversation
…aw 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>
Summary by t27-beesThis PR adds baseline rows for Worth a look
Read: 1 files, +12 -0, the whole diff. Head |
PR DashboardGenerated at: 2026-10-24 18:53:05 UTC
Summary
Seal Status
|
PR DashboardGenerated at: 2026-10-25 04:13:35 UTC
Summary
Seal Status
|
|
Lab dispatched on head adfeb3c (night tick 159) for |
|
Lab receipt for head adfeb3c (night tick 160): |
|
night tick 161: lab redispatched on adfeb3c after the t27b asserts guard landed (t27#12228 b820da4, t27os#40 637d940693), run 40163543896, challenge c6ccf937401e48f3. Receipt lands at Trinity-S-AI-DNA/t27os runs/adfeb3c15709bb447b38d6958db0b20b8ac0bc6b.*.json and runs/adfeb3c15709bb447b38d6958db0b20b8ac0bc6b.t27b.txt. |
|
Night tick 163: lab receipt for head
|
…12461) (#12462) * dupe: trigit verbs write through handoff's put_lit, one copy of the loop (Closes #12419) #12388 added put_lit to specs/tri/handoff/handoff.t27 with the same loop body as put_s in specs/tri/trigit/verbs.t27, so the Duplicate Body Ratchet went red on every PR: "put_lit was copied [2] and is now copied [2, 2]". verbs.t27 already reads handoff.t27 (put_span, create_record, ...), so the one body stays in handoff and verbs' put_s delegates to it. put_lit now takes []const u8, like its sibling put_span: gen-rust lowered `string` to &'static str, and verbs passes runtime byte slices. String callers get .as_bytes() / b"..." from gen-rust; the bytes written are unchanged. dupe_scan: 1849 bodies in 691 groups (was 1851 in 692), ledger unchanged. test-report: handoff 12/12, verbs 17/17, handoff_view 4/4, 0 vacuous. Seals for the three specs re-saved by t27c built at master 672aaca. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * seals: drop the stale FpgaHdmiGrab seal that #12430 re-added (Closes #12461) Master commit b1a5857 (PR #12430) added .trinity/seals/fpga_FpgaHdmiGrab.json as a new file sealed on 2026-10-20 against a shape of specs/fpga/hdmi_grab.t27 that #12059 split up this morning. Since then `coverage` (seal-coverage.yml) and `spec-guards` (check_seal_currency.py) are red on master and on every PR that merged it: one seal, all four gen_hashes stale. Master had no seal for this spec before that commit, so the file is removed; a fresh seal from a master-built t27c is a follow-up PR. Local check_seal_coverage.py on this branch: OK, 3079 seals, 2966 hold, 113 known-broken listed in seal_baseline.txt. Refs #12387 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * numeric: drop the dead braceless invariant the parser discarded in zphi_alu.t27, reseal (Closes #12464) Master commit b1a5857 (PR #12430) added specs/numeric/zphi_alu.t27. Its `invariant sign_conj_negation` is written in the braceless form with an `if` statement inside the body; `parse_bdd_clauses` does not lower that shape, so the parser restores its checkpoint and drops the whole body (61 tokens, lines 483-493). The Corpus Ratchet's `parse-no-discard` phase refuses such a file, so every branch that carries b1a5857 is red on `Corpus Ratchet`. The invariant was never checked, and it cannot be made live as written: with the file's own `sign` and `conj`, sign(3, 5) = 1, conj(3, 5) = (3, -5), sign(3, -5) = 1, so the asserted `sc == -s` is 1 == -1. The claim is not a Z[phi] theorem either (the conjugate of 1 is 1). The block and its comment line are deleted; nothing else in the spec changes. After the edit `t27c parse-complete --show specs/numeric/zphi_alu.t27` reports "nothing discarded" and `t27c check` passes. The seal .trinity/seals/numeric_NumericZphiAlu.json is regenerated in the same commit from a master-built t27c, so `coverage` and `spec-guards` stay green after the spec edit. No ledger entry, no parser change. Refs #12387 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * fix(seal): re-save the T27osFrameGate seal that #12467 left stale (Closes #12486) #12467 (e376a06, merged 2026-10-25T15:20:07Z) changed specs/t27os/frame_gate.t27 without re-saving .trinity/seals/t27os_T27osFrameGate.json, so tools/check_seal_currency.py reports one STALE generated-code hash on master and every PR with base master is red on spec-guards. Re-saved with a master-built t27c (0.5.2+672aaca7d, newer than master's last bootstrap/src change 2b1858e) from the branch root: tests 12/12, gen_hash_rust cebbd2f90560, gen_hash_zig 5877f763f823, gen_hash_c d7aba556f229, gen_hash_verilog 575cb51da761, the four values the check computes from the spec. The spec is unchanged; the seal carries no home path. Refs #11640 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
…hi_alu.t27, reseal (Closes #12464) (#12465) * dupe: trigit verbs write through handoff's put_lit, one copy of the loop (Closes #12419) #12388 added put_lit to specs/tri/handoff/handoff.t27 with the same loop body as put_s in specs/tri/trigit/verbs.t27, so the Duplicate Body Ratchet went red on every PR: "put_lit was copied [2] and is now copied [2, 2]". verbs.t27 already reads handoff.t27 (put_span, create_record, ...), so the one body stays in handoff and verbs' put_s delegates to it. put_lit now takes []const u8, like its sibling put_span: gen-rust lowered `string` to &'static str, and verbs passes runtime byte slices. String callers get .as_bytes() / b"..." from gen-rust; the bytes written are unchanged. dupe_scan: 1849 bodies in 691 groups (was 1851 in 692), ledger unchanged. test-report: handoff 12/12, verbs 17/17, handoff_view 4/4, 0 vacuous. Seals for the three specs re-saved by t27c built at master 672aaca. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * seals: drop the stale FpgaHdmiGrab seal that #12430 re-added (Closes #12461) Master commit b1a5857 (PR #12430) added .trinity/seals/fpga_FpgaHdmiGrab.json as a new file sealed on 2026-10-20 against a shape of specs/fpga/hdmi_grab.t27 that #12059 split up this morning. Since then `coverage` (seal-coverage.yml) and `spec-guards` (check_seal_currency.py) are red on master and on every PR that merged it: one seal, all four gen_hashes stale. Master had no seal for this spec before that commit, so the file is removed; a fresh seal from a master-built t27c is a follow-up PR. Local check_seal_coverage.py on this branch: OK, 3079 seals, 2966 hold, 113 known-broken listed in seal_baseline.txt. Refs #12387 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * numeric: drop the dead braceless invariant the parser discarded in zphi_alu.t27, reseal (Closes #12464) Master commit b1a5857 (PR #12430) added specs/numeric/zphi_alu.t27. Its `invariant sign_conj_negation` is written in the braceless form with an `if` statement inside the body; `parse_bdd_clauses` does not lower that shape, so the parser restores its checkpoint and drops the whole body (61 tokens, lines 483-493). The Corpus Ratchet's `parse-no-discard` phase refuses such a file, so every branch that carries b1a5857 is red on `Corpus Ratchet`. The invariant was never checked, and it cannot be made live as written: with the file's own `sign` and `conj`, sign(3, 5) = 1, conj(3, 5) = (3, -5), sign(3, -5) = 1, so the asserted `sc == -s` is 1 == -1. The claim is not a Z[phi] theorem either (the conjugate of 1 is 1). The block and its comment line are deleted; nothing else in the spec changes. After the edit `t27c parse-complete --show specs/numeric/zphi_alu.t27` reports "nothing discarded" and `t27c check` passes. The seal .trinity/seals/numeric_NumericZphiAlu.json is regenerated in the same commit from a master-built t27c, so `coverage` and `spec-guards` stay green after the spec edit. No ledger entry, no parser change. Refs #12387 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * fix(seal): re-save the T27osFrameGate seal that #12467 left stale (Closes #12486) #12467 (e376a06, merged 2026-10-25T15:20:07Z) changed specs/t27os/frame_gate.t27 without re-saving .trinity/seals/t27os_T27osFrameGate.json, so tools/check_seal_currency.py reports one STALE generated-code hash on master and every PR with base master is red on spec-guards. Re-saved with a master-built t27c (0.5.2+672aaca7d, newer than master's last bootstrap/src change 2b1858e) from the branch root: tests 12/12, gen_hash_rust cebbd2f90560, gen_hash_zig 5877f763f823, gen_hash_c d7aba556f229, gen_hash_verilog 575cb51da761, the four values the check computes from the spec. The spec is unchanged; the seal carries no home path. Refs #11640 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
…arity/alu_eval in the cell, the table oracle calls them (Closes #12011) (#12060) * fpga(wasm): the 24 single-clock i32 ALU opcodes have one home -- alu_arity/alu_eval in the cell, the table oracle calls them (Refs #12011) The cell's step_all took 24 hand-copied ALU branches; they are now one arm through alu_arity(op) / alu_eval(op, a, b), written once in wasm_board_ax7203. wasm_opcodes uses the cell and its eval_byte calls the same two functions, so the oracle and the cell cannot differ. Deviation from FR-005 of #12011 ("exist once, in the table spec"): they exist once in the cell spec. t27c gen-verilog imports only enums and structs from a used module, never a function body; the splice of used function bodies happens only in test-report / t27b test. The direction is forced by the lowering. Tests: cell 21/21, table 16/16 + invariant, 0 vacuous in both. Law 14 pins the cell's accepted byte set against the table's i32 ALU rows in both directions (24 bytes: 4 unary, 20 binary); law 15 pins the 37 executed bytes. Behavior change: eval_byte returns 0 for i64 rows (it used to evaluate their i32 twin) and for div/rem rows, as before. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> * fpga(wasm): seals re-saved for the cell and the table after the ALU one-home change (Refs #12011) t27c seal --save on both specs from the master-built binary; tri seals sync-twins reports 497 twinned specs already consistent, 0 written. Cell 21/21, table 16/16 plus the signed_order_holds invariant. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * fpga(wasm): park the cell spec and its seal at the merge base so master merges clean (Refs #12011) Master's P3/P4 const floors (i64.const 0x42, f32.const 0x43, f64.const 0x44) and the #12042 reseal landed on the same lines this lane rewrote for the one-home ALU, so a plain merge stops in two files. The pre-commit gate measures a hand-committed merge by its staged diff against the lane tip, where master's own Rust reads as lines added here, and that gate is never bypassed. So this commit puts specs/fpga/wasm_board_ax7203.t27 and .trinity/seals/fpga_fpga_wasm_board.json back to 09bcdb0, the next commit is git's own clean merge of origin/master, and the commit after it re-applies this lane's cell over master's, resolved by hand. The three together are the one merge; the PR's squash keeps only the result. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * fpga(wasm): re-apply the one-home ALU cell over master's P3/P4 const floors, 40 executed bytes (Refs #12011) Completes the merge of origin/master that the two commits before it prepared (the park and git's clean merge). Resolution by hand, master's bytes kept verbatim: the P3/P4 constants and their notes after OP_I32_CONST; the i32.const arm now also takes OP_I64_CONST; the f32/f64 arm sits between the const arm and the i32.mul arm, with its closing brace at the end of the chain; the two wire tests p3_i64_wire_programs and p4_f32_wire_programs sit before the #12011 block. The executed-byte count goes 37 -> 40 in both specs: cell_runs and executed_beyond_alu take 0x41-0x44 as one range, the sweep asserts 40 runs / 216 tried, law 15 is the_40_executed_bytes_are_all_generated_bytes with beyond == 16, the cost note says 14 other arms. The two seals are this lane's old ones for now; they are re-saved from a master-built compiler in the next commit. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * seal(fpga): re-save the wasm board and opcode-table seals after the P3/P4 merge, 23/23 and 16/16 (Refs #12011) The two seals are re-saved from a compiler built at master commit 19a89f1, whose compiler tree (bootstrap, cli, Cargo.lock, Cargo.toml) is byte-identical to origin/master at 7273ad3; the previous seals named 94adbb1 and predated master's gen-rust change (#12042, resealed on master in #12062). built_by, spec_hash and the four gen hashes move; the board seal's test count moves 21 -> 23 with master's two const-floor tests; the seals carry no home path. Run: t27c seal --save, then t27c test-report, both specs, 0 vacuous. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * tools(dupe): lower the duplicate-bodies ledger by the two groups this lane removed (Refs #12011) The table's sar32 and lt_s were copies of the cell's; this lane deleted them, so the groups are gone and the ratchet refuses a ceiling left above the real number. Re-blessed with tools/dupe_scan.py --bless: the diff is two deleted lines, no group added, none grown. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * chore(fpga): park the table and its seal at the merge base before merging master (Refs #12011) Master dropped the copied lt_s and sar32 bodies from wasm_opcodes.t27 in favour of an import (#11885) and re-sealed the table; this branch rewrote the same region. The table and its seal go back to the merge-base version for one commit so the merge of master is clean, and the branch's change is re-applied on top in the next commit. The cell is untouched. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * fix(fpga): re-apply the one-home table on top of master's lt_s/sar32 import drop (Refs #12011) The merge of master brought the table back to master's text, where the copied lt_s and sar32 bodies were replaced by an import (#11885). This branch removes every restated ALU body from the table (the ALU lives once in the cell, issue #12011), so the import is not needed either: the table is byte-for-byte the version this branch carried before the merge, and so is its seal. A fresh `t27c seal` from a master-built t27c on the merged tree reproduces every hash in that seal (spec, zig, verilog, c, rust; 16 of 16 tests); only the built_by and sealed_at lines would change, so the previous file is kept and the stacked lanes merge this branch without touching the table again. The cell and its seal are untouched by master. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * dupe: trigit verbs write through handoff's put_lit, one copy of the loop (Closes #12419) #12388 added put_lit to specs/tri/handoff/handoff.t27 with the same loop body as put_s in specs/tri/trigit/verbs.t27, so the Duplicate Body Ratchet went red on every PR: "put_lit was copied [2] and is now copied [2, 2]". verbs.t27 already reads handoff.t27 (put_span, create_record, ...), so the one body stays in handoff and verbs' put_s delegates to it. put_lit now takes []const u8, like its sibling put_span: gen-rust lowered `string` to &'static str, and verbs passes runtime byte slices. String callers get .as_bytes() / b"..." from gen-rust; the bytes written are unchanged. dupe_scan: 1849 bodies in 691 groups (was 1851 in 692), ledger unchanged. test-report: handoff 12/12, verbs 17/17, handoff_view 4/4, 0 vacuous. Seals for the three specs re-saved by t27c built at master 672aaca. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * seals: drop the stale FpgaHdmiGrab seal that #12430 re-added (Closes #12461) Master commit b1a5857 (PR #12430) added .trinity/seals/fpga_FpgaHdmiGrab.json as a new file sealed on 2026-10-20 against a shape of specs/fpga/hdmi_grab.t27 that #12059 split up this morning. Since then `coverage` (seal-coverage.yml) and `spec-guards` (check_seal_currency.py) are red on master and on every PR that merged it: one seal, all four gen_hashes stale. Master had no seal for this spec before that commit, so the file is removed; a fresh seal from a master-built t27c is a follow-up PR. Local check_seal_coverage.py on this branch: OK, 3079 seals, 2966 hold, 113 known-broken listed in seal_baseline.txt. Refs #12387 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * numeric: drop the dead braceless invariant the parser discarded in zphi_alu.t27, reseal (Closes #12464) Master commit b1a5857 (PR #12430) added specs/numeric/zphi_alu.t27. Its `invariant sign_conj_negation` is written in the braceless form with an `if` statement inside the body; `parse_bdd_clauses` does not lower that shape, so the parser restores its checkpoint and drops the whole body (61 tokens, lines 483-493). The Corpus Ratchet's `parse-no-discard` phase refuses such a file, so every branch that carries b1a5857 is red on `Corpus Ratchet`. The invariant was never checked, and it cannot be made live as written: with the file's own `sign` and `conj`, sign(3, 5) = 1, conj(3, 5) = (3, -5), sign(3, -5) = 1, so the asserted `sc == -s` is 1 == -1. The claim is not a Z[phi] theorem either (the conjugate of 1 is 1). The block and its comment line are deleted; nothing else in the spec changes. After the edit `t27c parse-complete --show specs/numeric/zphi_alu.t27` reports "nothing discarded" and `t27c check` passes. The seal .trinity/seals/numeric_NumericZphiAlu.json is regenerated in the same commit from a master-built t27c, so `coverage` and `spec-guards` stay green after the spec edit. No ledger entry, no parser change. Refs #12387 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * fix(seal): re-save the T27osFrameGate seal that #12467 left stale (Closes #12486) #12467 (e376a06, merged 2026-10-25T15:20:07Z) changed specs/t27os/frame_gate.t27 without re-saving .trinity/seals/t27os_T27osFrameGate.json, so tools/check_seal_currency.py reports one STALE generated-code hash on master and every PR with base master is red on spec-guards. Re-saved with a master-built t27c (0.5.2+672aaca7d, newer than master's last bootstrap/src change 2b1858e) from the branch root: tests 12/12, gen_hash_rust cebbd2f90560, gen_hash_zig 5877f763f823, gen_hash_c d7aba556f229, gen_hash_verilog 575cb51da761, the four values the check computes from the spec. The spec is unchanged; the seal carries no home path. Refs #11640 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * ci(elab): baseline rows for the five specs/fpga modules the #12430 merge started emitting (Closes #12491) b1a5857 (the #12430 merge, 2026-10-25T13:29Z) brought specs/fpga/ hdmi_timing_640x480.t27, i2c_master.t27, lucas_accumulator.t27, sii9134_init.t27 and tmds_encoder.t27 onto master without rows in tools/elab_baseline.txt, so tools/check_elab_ratchet.py reads them as NEW and fpga-conformance is red on master (run 40197819164) and on every lane behind it (#12304, #12356, #12405). Five rows with the counts CI printed on that run (0, 20, 8, 2, 0; 384 -> 414) and one dated note. No existing row changes, no spec, generator or checker change. Refs #9367, #12387, #2325 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * gates(dupes): ledger row for the same group, the renamed remainder of the groups #12458 shrank (Closes #12498) #12458 (4f1c99a) deleted the bytes_equal, eq_s and mem_eql copies of the byte-equality body and dropped their ledger rows. The two copies it left, specs/tri/crypto/hex.t27:98 fn same and specs/igla/coder/tokenizer.t27:469 fn same_bytes, were members of those groups; tools/dupe_scan.py names a group by its alphabetically first member, so the remainder now reads `same 2` and was in no ledger. Neither file changed since 2026-10-23. One row added, nothing else. Replacing both bodies with std::mem::bytes_eq (and dropping the row again) stays with #12444. Refs #9367, #12387, #12444 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * port(scripts): move the build_tree use inside the 29 gen_w6NN modules so the parser keeps their closing brace; reseal (Closes #12497) #12458 (4f1c99a) replaced the local fn build_tree in gen_w631..657, 662 and 680 with `use port::scripts::gen_w_flat::build_tree;` on line 8, before `module gen_wNNN {` on line 9. The parser takes that form and drops the module's final `}` without an error (t27c parse-complete --show: 1 token DISCARDED, line 66); t27c check is blind to it, so the Corpus Ratchet reports 29 UNEXPECTED FAILURES [parse-no-discard] on master and on every lane behind it. The use line now sits first inside each module body; the constants, functions and tests do not change. The 29 seals are re-saved with the master-built t27c from the repository root. The parser defect itself (bootstrap/) is out of scope here. Refs #9367, #12387, #12444 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * seals(t27os): re-save the five t27os seals that #12373 added against older spec states (Closes #12509) #12373 (squashed to 70e3073) added seals for T27osDoctor, T27osGlassWindow, T27osLabPublish, T27osPtyServer and T27osReceiptName that were computed on its own branch, while master's copies of the five specs had moved on; they were stale the moment they landed, so coverage and spec-guards are red on master and on every PR that carries 70e3073 (FAIL: 6 seal(s) newly do not hold; STALE generated-code hash: 6). The five seals are re-saved with the master-built t27c 0.5.2 from the repository root at 70e3073; the gen hashes now equal the current= values spec-guards printed on master. Nothing else changes. The sixth stale seal, T27osSessionStore, is carried by #12495. Refs #9367, #12387 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 5.5 <noreply@anthropic.com>
…ceipt (Closes #12411) (#12457) * dupe: trigit verbs write through handoff's put_lit, one copy of the loop (Closes #12419) #12388 added put_lit to specs/tri/handoff/handoff.t27 with the same loop body as put_s in specs/tri/trigit/verbs.t27, so the Duplicate Body Ratchet went red on every PR: "put_lit was copied [2] and is now copied [2, 2]". verbs.t27 already reads handoff.t27 (put_span, create_record, ...), so the one body stays in handoff and verbs' put_s delegates to it. put_lit now takes []const u8, like its sibling put_span: gen-rust lowered `string` to &'static str, and verbs passes runtime byte slices. String callers get .as_bytes() / b"..." from gen-rust; the bytes written are unchanged. dupe_scan: 1849 bodies in 691 groups (was 1851 in 692), ledger unchanged. test-report: handoff 12/12, verbs 17/17, handoff_view 4/4, 0 vacuous. Seals for the three specs re-saved by t27c built at master 672aaca. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * ci(fpga-build): synthesise the AX7203 WASM cell with a utilisation receipt (Closes #12411) Job fpga-synth-ax7203 after fpga-smoke: register-bit budget check (#12297), yosys synth_xilinx -top fpga_wasm_board for xc7a200tfbg484-2 in regymm/openxc7, artifact wasm-board-ax7203-synth with receipt.txt. Gated to PRs touching the cell specs or this workflow. The two dead fbg676 helper scripts are removed to keep the hand-written foreign line count net negative. Board top and place-and-route follow in #12456. Refs #9367 Refs #12387 Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> * seals: drop the stale FpgaHdmiGrab seal that #12430 re-added (Closes #12461) Master commit b1a5857 (PR #12430) added .trinity/seals/fpga_FpgaHdmiGrab.json as a new file sealed on 2026-10-20 against a shape of specs/fpga/hdmi_grab.t27 that #12059 split up this morning. Since then `coverage` (seal-coverage.yml) and `spec-guards` (check_seal_currency.py) are red on master and on every PR that merged it: one seal, all four gen_hashes stale. Master had no seal for this spec before that commit, so the file is removed; a fresh seal from a master-built t27c is a follow-up PR. Local check_seal_coverage.py on this branch: OK, 3079 seals, 2966 hold, 113 known-broken listed in seal_baseline.txt. Refs #12387 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * numeric: drop the dead braceless invariant the parser discarded in zphi_alu.t27, reseal (Closes #12464) Master commit b1a5857 (PR #12430) added specs/numeric/zphi_alu.t27. Its `invariant sign_conj_negation` is written in the braceless form with an `if` statement inside the body; `parse_bdd_clauses` does not lower that shape, so the parser restores its checkpoint and drops the whole body (61 tokens, lines 483-493). The Corpus Ratchet's `parse-no-discard` phase refuses such a file, so every branch that carries b1a5857 is red on `Corpus Ratchet`. The invariant was never checked, and it cannot be made live as written: with the file's own `sign` and `conj`, sign(3, 5) = 1, conj(3, 5) = (3, -5), sign(3, -5) = 1, so the asserted `sc == -s` is 1 == -1. The claim is not a Z[phi] theorem either (the conjugate of 1 is 1). The block and its comment line are deleted; nothing else in the spec changes. After the edit `t27c parse-complete --show specs/numeric/zphi_alu.t27` reports "nothing discarded" and `t27c check` passes. The seal .trinity/seals/numeric_NumericZphiAlu.json is regenerated in the same commit from a master-built t27c, so `coverage` and `spec-guards` stay green after the spec edit. No ledger entry, no parser change. Refs #12387 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * ci(fpga-build): re-bless the census for the fpga-synth-ax7203 job (Refs #12411) `tri census pin --gate` (the cli-tri check) refused bee2493 because the new `fpga-synth-ax7203` job in .github/workflows/fpga-build.yml moved two pinned censuses and the commit did not say so. The moves, each the job's own footprint and intended: shell jobs 97 -> 98 the new job itself shell run: steps 331 -> 334 its three `run:` steps shell the runner does 310 -> 313 the same three, on the runner's shell (no container) quiet named a path but not quiet 258 -> 263 five of its steps name a path and none is `quiet` Re-blessed with `tri census pin --bless` from a master-built `tri` whose `--gate` reading on this tree equals CI's line for line (quiet 258 -> 263, jobs 97 -> 98). Only tools/census/quiet.txt and tools/census/shell.txt change; the job is as in bee2493. Refs #12387 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * fix(seal): re-save the T27osFrameGate seal that #12467 left stale (Closes #12486) #12467 (e376a06, merged 2026-10-25T15:20:07Z) changed specs/t27os/frame_gate.t27 without re-saving .trinity/seals/t27os_T27osFrameGate.json, so tools/check_seal_currency.py reports one STALE generated-code hash on master and every PR with base master is red on spec-guards. Re-saved with a master-built t27c (0.5.2+672aaca7d, newer than master's last bootstrap/src change 2b1858e) from the branch root: tests 12/12, gen_hash_rust cebbd2f90560, gen_hash_zig 5877f763f823, gen_hash_c d7aba556f229, gen_hash_verilog 575cb51da761, the four values the check computes from the spec. The spec is unchanged; the seal carries no home path. Refs #11640 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * gates(dupes): ledger row for the same group, the renamed remainder of the groups #12458 shrank (Closes #12498) #12458 (4f1c99a) deleted the bytes_equal, eq_s and mem_eql copies of the byte-equality body and dropped their ledger rows. The two copies it left, specs/tri/crypto/hex.t27:98 fn same and specs/igla/coder/tokenizer.t27:469 fn same_bytes, were members of those groups; tools/dupe_scan.py names a group by its alphabetically first member, so the remainder now reads `same 2` and was in no ledger. Neither file changed since 2026-10-23. One row added, nothing else. Replacing both bodies with std::mem::bytes_eq (and dropping the row again) stays with #12444. Refs #9367, #12387, #12444 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * port(scripts): move the build_tree use inside the 29 gen_w6NN modules so the parser keeps their closing brace; reseal (Closes #12497) #12458 (4f1c99a) replaced the local fn build_tree in gen_w631..657, 662 and 680 with `use port::scripts::gen_w_flat::build_tree;` on line 8, before `module gen_wNNN {` on line 9. The parser takes that form and drops the module's final `}` without an error (t27c parse-complete --show: 1 token DISCARDED, line 66); t27c check is blind to it, so the Corpus Ratchet reports 29 UNEXPECTED FAILURES [parse-no-discard] on master and on every lane behind it. The use line now sits first inside each module body; the constants, functions and tests do not change. The 29 seals are re-saved with the master-built t27c from the repository root. The parser defect itself (bootstrap/) is out of scope here. Refs #9367, #12387, #12444 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * seals(t27os): re-save the five t27os seals that #12373 added against older spec states (Closes #12509) #12373 (squashed to 70e3073) added seals for T27osDoctor, T27osGlassWindow, T27osLabPublish, T27osPtyServer and T27osReceiptName that were computed on its own branch, while master's copies of the five specs had moved on; they were stale the moment they landed, so coverage and spec-guards are red on master and on every PR that carries 70e3073 (FAIL: 6 seal(s) newly do not hold; STALE generated-code hash: 6). The five seals are re-saved with the master-built t27c 0.5.2 from the repository root at 70e3073; the gen hashes now equal the current= values spec-guards printed on master. Nothing else changes. The sixth stale seal, T27osSessionStore, is carried by #12495. Refs #9367, #12387 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * census: re-pin shell after merging master into the synth branch (Refs #12411) The synth job pinned +1 job, +3 run steps, +3 runner-named steps over 4f1c99a; master #12515 pinned the release-leg workflow (+1 file, +1 job, +2 steps, +2 runner-named) over the same base. The merge keeps master file, so the sum is re-blessed here: jobs 98 -> 99, run steps 333 -> 336, runner-named 312 -> 315. No workflow changes here. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * ci(fpga-synth): fail the pull step when the image never arrives; stat -tech xilinx for the LC line (Refs #12411) Two in-place lines in the synth job, after the t27-bees review of 2f88fd1: - the six-attempt docker pull loop ended with the status of its last sleep, so six failed pulls passed the step and the yosys step died with "image not found"; the step now checks the image after the loop and fails with its own message. - stat without -tech xilinx prints no "Estimated number of LCs" line, so the receipt grep was empty by construction; stat -tech xilinx prints it with the same per-cell table. The other three remarks do not apply to the generated cell: gen-verilog emits no comma-separated reg declarations (0 in the artifact) and writes module at column 1; a flattened stat prints each cell type once. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * census(quiet): re-bless, named-a-path-but-not-quiet 263 -> 264 for the image check in the synth job (Refs #12411) The quiet census moved by one line in 1b10fe5: the check that follows the six-attempt image pull loop in the fpga-synth-ax7203 job names regymm/openxc7:latest and is counted as "named a path but not quiet" (its stdout goes to /dev/null, but the census reads the line, not the redirect). cli-tri on that head: 889 tests passed, the gate step alone failed with "quiet moved 263 -> 264". Nothing else in tools/census moves (fetches and shell unchanged, tri census explain). Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * fpga: AX7203 board top for the WASM cell, paid by deleting the ported link_node.v (Refs #12456) (#12594) The one hand-written Verilog file of milestone B: fpga/verilog/wasm_board_ax7203_top.v (34 lines) wraps the generated cell fpga_wasm_board for the ALINX AX7203 (xc7a200tfbg484-2). Ports exactly rst_n, led[3:0], uart_rx, uart_tx (the pinned XDC: T6 / B13 C13 D14 D15 / P20 / N15); the clock is STARTUPE2 CFGMCLK through a BUFG, no board clock pin; two-flop reset and UART synchronisers; the cell runs with en high, rxd is {7'b0, uart_rx}, uart_tx is txd[0], the read-back outputs stay open (FR-001, FR-002). The payment under the foreign-budget rule, in the same commit because the pre-commit hook counts each commit's staged diff on its own: fpga/verilog/link_node.v (132 hand-written lines) is deleted; it was ported to specs/port/fpga/verilog/link_node.t27 and nothing but docs/now prose named it. The gate of the fpga-synth-ax7203 job also fires when the top changes (one regex line in .github/workflows/fpga-build.yml). Owner's approval, 2026-10-25, Claude Code session (translated from Russian): "Yes, write the board top wasm_board_ax7203_top.v for #12456 (up to 40 lines, under owner-approved-foreign, paid by deletions) through a Sonnet subagent on top of #12457, show the frames every run." The exception-list entry is #12483. Lint: yosys read_verilog -lib of cells_sim.v + cells_xtra.v and of the generated cell, hierarchy -check, check -assert: clean, one float-parameter warning on SIM_CCLK_FREQ. gen-verilog cannot instantiate primitives yet (specs/fpga/die_probe.t27), so the top stays foreign until that gap closes; the place-and-route steps of the job (FR-003 to FR-006) follow after #12457 lands. Refs #12411 Refs #9367 Refs #12387 Refs #6198 Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
…near memory, calls, i64 pairs (Closes #12371) (#12597) * fpga(wasm): the 24 single-clock i32 ALU opcodes have one home -- alu_arity/alu_eval in the cell, the table oracle calls them (Refs #12011) The cell's step_all took 24 hand-copied ALU branches; they are now one arm through alu_arity(op) / alu_eval(op, a, b), written once in wasm_board_ax7203. wasm_opcodes uses the cell and its eval_byte calls the same two functions, so the oracle and the cell cannot differ. Deviation from FR-005 of #12011 ("exist once, in the table spec"): they exist once in the cell spec. t27c gen-verilog imports only enums and structs from a used module, never a function body; the splice of used function bodies happens only in test-report / t27b test. The direction is forced by the lowering. Tests: cell 21/21, table 16/16 + invariant, 0 vacuous in both. Law 14 pins the cell's accepted byte set against the table's i32 ALU rows in both directions (24 bytes: 4 unary, 20 binary); law 15 pins the 37 executed bytes. Behavior change: eval_byte returns 0 for i64 rows (it used to evaluate their i32 twin) and for div/rem rows, as before. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> * fpga(wasm): seals re-saved for the cell and the table after the ALU one-home change (Refs #12011) t27c seal --save on both specs from the master-built binary; tri seals sync-twins reports 497 twinned specs already consistent, 0 written. Cell 21/21, table 16/16 plus the signed_order_holds invariant. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * fpga(wasm): block/loop/br/br_if/br_table and the label stack in the board cell -- scan submachine, fuel guard, ERR_LABEL/ERR_FUEL, five baked control-flow programs (Refs #12010) Five opcodes join the cell's executed set (37 -> 42): block 0x02, loop 0x03, br 0x0C, br_if 0x0D, br_table 0x0E. A label stack of LABEL_MAX 8 (kind, target, stack height, arity); a scan submachine that finds a block's matching end by skipping immediates (one-LEB opcodes, nested block/loop, br_table vectors; an unknown byte is ERR_OPCODE); a FUEL_MAX 65536 guard with ERR_FUEL 9 so a looping program cannot hang the wire, ERR_LABEL 8 for a branch past the stack; host_run_user awaits 8 * FUEL_MAX. Five reference programs baked into the store: CF_SUM 0x00 (30 bytes, sum 1..100 = 5050), CF_TAB 0x1E (26 bytes, br_table -> 10/20/30/10), CF_NEST 0x38, CF_FUEL 0x59, CF_VAL 0x6D (a branch unwinds the value stack: 43, not 5); CF_END 0x7C. Cell tests 30/30 (t27c test-report and t27b test agree, 0 vacuous); table 16/16 plus invariant, law 15 renamed to the_42_executed_bytes_are_all_generated_bytes. Dispatch arms 18 = the 13 of (#12011), one recipe. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * fpga(wasm): park the cell spec and its seal at the merge base so master merges clean (Refs #12011) Master's P3/P4 const floors (i64.const 0x42, f32.const 0x43, f64.const 0x44) and the #12042 reseal landed on the same lines this lane rewrote for the one-home ALU, so a plain merge stops in two files. The pre-commit gate measures a hand-committed merge by its staged diff against the lane tip, where master's own Rust reads as lines added here, and that gate is never bypassed. So this commit puts specs/fpga/wasm_board_ax7203.t27 and .trinity/seals/fpga_fpga_wasm_board.json back to 09bcdb0, the next commit is git's own clean merge of origin/master, and the commit after it re-applies this lane's cell over master's, resolved by hand. The three together are the one merge; the PR's squash keeps only the result. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * fpga(wasm): re-apply the one-home ALU cell over master's P3/P4 const floors, 40 executed bytes (Refs #12011) Completes the merge of origin/master that the two commits before it prepared (the park and git's clean merge). Resolution by hand, master's bytes kept verbatim: the P3/P4 constants and their notes after OP_I32_CONST; the i32.const arm now also takes OP_I64_CONST; the f32/f64 arm sits between the const arm and the i32.mul arm, with its closing brace at the end of the chain; the two wire tests p3_i64_wire_programs and p4_f32_wire_programs sit before the #12011 block. The executed-byte count goes 37 -> 40 in both specs: cell_runs and executed_beyond_alu take 0x41-0x44 as one range, the sweep asserts 40 runs / 216 tried, law 15 is the_40_executed_bytes_are_all_generated_bytes with beyond == 16, the cost note says 14 other arms. The two seals are this lane's old ones for now; they are re-saved from a master-built compiler in the next commit. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * fpga(wasm): park the cell and the table at the merge base so the ALU lane merges clean (Refs #12010) The ALU lane (lane/wasm-alu-one-home-12011, PR #12060) now carries master's P3/P4 const floors and master's own Rust; a plain merge of it stops in the cell and the table on the executed-byte counts. The pre-commit gate measures a hand-committed merge by its staged diff against the lane tip, where master's Rust reads as lines added here, and that gate is never bypassed. So this commit puts specs/fpga/wasm_board_ax7203.t27 and specs/fpga/wasm_opcodes.t27 back to 49c4dcb, the next commit is git's own clean merge of the ALU lane, and the commit after it re-applies the control-flow cell and table over it, resolved by hand. The three together are the one merge; the PR's squash keeps only the result. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * fpga(wasm): re-apply the control-flow cell and table over the ALU lane's P3/P4 merge, 45 executed bytes (Refs #12010) Completes the merge of lane/wasm-alu-one-home-12011 that the two commits before it prepared (the park and git's clean merge). The dispatch chain merged by itself: the four control-flow arms (block/loop, br, br_if, br_table) sit before local.get, the const arm takes i32.const and i64.const, the float arm follows it. Resolved by hand, only the counts: cell_runs and executed_beyond_alu take 0x41-0x44 as one range plus the five control-flow bytes, the sweep asserts 45 runs / 211 tried, law 15 is the_45_executed_bytes_are_all_generated_bytes with beyond == 21, the cost note says a 45-byte decode with 18 other arms. The two seals are this lane's old ones for now; they are re-saved from a master-built compiler in the next commit. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * seal(fpga): re-save the wasm board and opcode-table seals after the P3/P4 merge, 23/23 and 16/16 (Refs #12011) The two seals are re-saved from a compiler built at master commit 19a89f1, whose compiler tree (bootstrap, cli, Cargo.lock, Cargo.toml) is byte-identical to origin/master at 7273ad3; the previous seals named 94adbb1 and predated master's gen-rust change (#12042, resealed on master in #12062). built_by, spec_hash and the four gen hashes move; the board seal's test count moves 21 -> 23 with master's two const-floor tests; the seals carry no home path. Run: t27c seal --save, then t27c test-report, both specs, 0 vacuous. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * seal(fpga): re-save the wasm board and opcode-table seals for the control-flow cell, 32/32 and 16/16 (Refs #12010) Same compiler as the ALU lane's reseal: built at master commit 19a89f1, compiler tree byte-identical to origin/master at 7273ad3. The board seal's test count moves 30 -> 32 with master's two const-floor tests; built_by, spec_hash and the four gen hashes move; no home path. Run: t27c seal --save, then t27c test-report, both specs, 0 vacuous. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * tools(dupe): lower the duplicate-bodies ledger by the two groups this lane removed (Refs #12011) The table's sar32 and lt_s were copies of the cell's; this lane deleted them, so the groups are gone and the ratchet refuses a ceiling left above the real number. Re-blessed with tools/dupe_scan.py --bless: the diff is two deleted lines, no group added, none grown. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * fpga(wasm): move the P2..P4 page-load tests back below the cf_ suite so the Verilog run keeps the baked programs (Refs #12010) In the simulation Verilog every test block is an initial block over one shared code[]. The P2..P4 section loads pages over the baked programs and its header says it stays last, but the cf_ suite had been appended below it, so cf_fuel_then_link_alive and cf_restore_keeps_the_baked_programs read a cleared ID_ANSWER and ID_TEE_DUP in vvp (30 of 32) while the interpreter, one process per test, gave 32 of 32. This is a move of 956 lines plus a two-line comment stating the rule; no assert changed. Measured with gen-verilog-for-simulation, the two "save = undefined;" lines of master's P3/P4 tests deleted first (t27#12179), iverilog -g2005 and vvp -n: 32 starting, 32 PASSED, 0 FAILED. test-report: 32 of 32 and 16 of 16, 0 vacuous. Both seals re-saved from a master-equivalent compiler. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * fpga: wasm_board_ax7203 P5 -- one 64 KiB linear memory page, ten memory opcodes (Closes #12202) The board cell now executes i32.load (0x28), load8_s/u (0x2C/0x2D), load16_s/u (0x2E/0x2F), i32.store (0x36), store8 (0x3A), store16 (0x3B), memory.size (0x3F) and memory.grow (0x40) over one `var mem : [MEM_BYTES]u8` with MEM_BYTES = 65536. - Little-endian; a 2- or 4-byte access is a byte-per-step microsequence (mem_run) with one read site and one write site, both addressed by the register mem_addr; the extra steps spend no fuel (one unit per fetch). - The memarg is two LEB128 u32 (align ignored, offset kept); a fifth continuation byte answers ERR_LEB; scan_class steps over it, so a branch that skips a load with a two-byte offset ending in 0x0B lands correctly. - The effective address is a 33-bit sum; an access of width w traps when it exceeds 65536 - w (ERR_MEM = 10, RESP_BADOP on the wire) before any byte is written; no wrap, and the next request works. - load8_s/load16_s sign-extend, load8_u/load16_u zero-extend; store8 and store16 leave every other byte alone. - memory.size pushes 1; memory.grow pushes 0xFFFFFFFF for every delta, 0 included (a documented deviation from the WASM spec: it grows nothing). - Ten new cell tests (42 in all), placed before the P2..P4 page-load tests, which stay last. cell_runs, alu_unexecuted_bytes_are_opcode_errors, wire_is_the_node_link, machine_consts and cf_negative_controls updated (the unexecuted probe byte is now 0x29, since 0x28 is a class-6 memarg op). - wasm_opcodes: fn executed_beyond_alu grows from 21 to 31 bytes, and the executed-bytes law is renamed and re-pinned for 55 (24 ALU + 31). No row is added and no pinned const changes: the eight memory rows keep interp_ok = false, because the live interpreter has no memory. Measured: t27c test-report on the cell 42 of 42, 0 vacuous; on the table 16 tests pass, 1 invariant proved, 0 vacuous. Known gap, measured and not hidden: yosys 0.67 read_verilog on the generated cell answers "Replacing memory \mem with list of registers", so the page is not block RAM in this lowering (and read_verilog + hierarchy ran for more than ten minutes against 5.7 s for the base). gen-verilog emits no initial block for `[0] ** MEM_BYTES`, so an iverilog run reads X from an unwritten byte; the new tests store before they load. Both are t27c emitter gaps, not fixed here (this change touches only the two specs). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> * fpga(wasm): bounds check in 32-bit compares so the Verilog run agrees with the Zig run (Refs #12202) The first form of mem_fits summed three `as u64` casts and compared the 33-bit result with MEM_BYTES. The Zig run passed (42 of 42), the vector-level Verilog run did not (41 of 42): gen-verilog drops the u64 casts and emits `((base + off) + w) > MEM_BYTES` over 32-bit inputs, so 0xFFFFFFFF + 1 wrapped to a legal address and mem_access_past_the_page_traps lost its wrap cases (ten failed asserts). mem_fits now says the same thing with two 32-bit compares that cannot overflow: with lim = MEM_BYTES - w, the access fits exactly when base <= lim and off <= lim - base. mem_ea adds base + off without a cast, because it is only reached after mem_fits said yes. Measured after the change: t27c test-report 42 of 42, 0 vacuous; the emitted mem_fits carries the two compares; iverilog -g2012 elaboration 0 errors. The emitter gap itself is filed separately and not fixed here. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * seals: wasm_board_ax7203 and wasm_opcodes re-saved for the memory page (Refs #12202) Both seals come from a master-built t27c run at the lane root (`t27c seal <spec> --save`, then `tri seals sync-twins`); the cell seal now records 42 of 42 tests, the table seal its new gen hashes. No path under a home directory in either file. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * feat(fpga): wasm_board_ax7203 P6 -- if/else, call/return, call_indirect, globals on the existing frames (Closes #12323) Adds the call machinery to the board cell, on the label stack and the one-byte-per-step forward scan that #12010 introduced. wasm_board_ax7203.t27 - Six new executed bytes: if 0x04, else 0x05, call 0x10, call_indirect 0x11, global.get 0x23, global.set 0x24. `return` 0x0F now unwinds to the current call frame; the function-level `end` returns to the caller while a frame is open and ends the run otherwise. - Call stack of CALL_MAX = 4 frames (pc, sp, label height, locals base, code window); locals are one flat array of LOCALS_TOTAL = 20 entries addressed from the frame base. A function returns a result iff the operand stack is higher than at entry, otherwise it is void. - Function table (FUNC_MAX = 8 rows: off, np, nl, ty), element table (ELEM_MAX = 4, NO_FUNC marks null) and globals (GLOBAL_MAX = 4) are cell arrays, loadable over the wire with the new op LOAD_TABLES 0xFC. - New errors ERR_CALL 11, ERR_FUNC 12, ERR_TYPE 13, ERR_GLOBAL 14, each with a const and a wire test answering RESP_BADOP. - Fuel stays one unit per fetch. Runaway recursion ends with ERR_CALL at the depth limit; the next request works. - cell_runs is 1 for exactly 61 bytes. - 22 new tests with the prefix cl_, above the P2 header comment, each one behaviour with real WASM bytes and a closed-form golden. Hand traces with fuel counts for cl_if_takes_else_arm, cl_call_recursive_fact_to_depth and cl_return_unwinds_labels_and_frame. wasm_opcodes.t27 - executed_beyond_alu returns 1 for the six new bytes; the executed-bytes law is re-pinned: 24 ALU + 37 beyond = 61 (was 24 + 31 = 55). No row is added and no interp_ok value changes. Nothing was synthesised, simulated, flashed or run on the board in this commit; the tests were typechecked with t27_check only, and the Zig and Verilog runs are reported by the orchestrator. Closes #12323 Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> * seals: wasm_board_ax7203 and wasm_opcodes re-saved for P6 calls and if/else (Refs #12323) Both seals come from a master-built t27c run at the lane root (`t27c seal <spec> --save`, then `tri seals sync-twins`); the cell seal now records 64 of 64 tests, the table seal its new gen hashes for the 61-byte executed pin. No path under a home directory in either file. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * chore(fpga): park the table and its seal at the merge base before merging master (Refs #12011) Master dropped the copied lt_s and sar32 bodies from wasm_opcodes.t27 in favour of an import (#11885) and re-sealed the table; this branch rewrote the same region. The table and its seal go back to the merge-base version for one commit so the merge of master is clean, and the branch's change is re-applied on top in the next commit. The cell is untouched. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * fix(fpga): re-apply the one-home table on top of master's lt_s/sar32 import drop (Refs #12011) The merge of master brought the table back to master's text, where the copied lt_s and sar32 bodies were replaced by an import (#11885). This branch removes every restated ALU body from the table (the ALU lives once in the cell, issue #12011), so the import is not needed either: the table is byte-for-byte the version this branch carried before the merge, and so is its seal. A fresh `t27c seal` from a master-built t27c on the merged tree reproduces every hash in that seal (spec, zig, verilog, c, rust; 16 of 16 tests); only the built_by and sealed_at lines would change, so the previous file is kept and the stacked lanes merge this branch without touching the table again. The cell and its seal are untouched by master. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * feat(fpga): i64 pairs on the operand stack for DOOM's FixedMul in wasm_board_ax7203 (Closes #12371) An i64 is two u32 stack slots, HIGH deeper at st[sp-2], LOW on top at st[sp-1], so the root end still answers the low word and the P3 answers (987654321, -5) stand. Nine bytes join the cell behind one is_p7_op gate: i32.wrap_i64 0xA7, i64.extend_i32_s/u 0xAC/0xAD, i64.add/sub/mul 0x7C-0x7E, i64.shl/shr_s/shr_u 0x86-0x88. i64.mul is a 64-step shift-add microsequence (mul_run = 64) over 32-bit limbs; add, sub and the shifts finish in one step. No u64 value is read beyond its low 32 bits (#12296): a carry is "sum < addend", a borrow is "a < b", and only wrap32 masks. i64.const now decodes up to ten LEB bytes into a pair (the tenth byte may not continue, else ERR_LEB); scan_class gives it class 1 and the nine others class 0. wasm_opcodes.t27 pins the executed set 61 -> 70 bytes (46 beyond the 24 ALU bytes). The cell suite grows 64 -> 83 tests (64 + 19): consts, encoder, every LEB length, extends, wrap, add, sub, mul, the three shifts, FixedMul vectors plus FixedMul inside a call, stack traps, a limb oracle and a 64-pair mul sweep. No synthesis was run and nothing was flashed; seals are not re-saved here. Refs #9367 Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> * fix(fpga): i32.const 4-byte SLEB128 sign bit is bit 27 in wasm_board_ax7203 (Closes #12395) The final-byte arm for a 4-byte i32.const tested bit 23 and filled 0xF8000000, but a 4-byte SLEB128 carries 28 payload bits: the sign bit is bit 27 (0x8000000) and the fill is 0xF0000000. 41 80 80 80 04 gave 0xF8800000 (want 8388608) and 41 80 80 80 78 gave 0x0F000000 (want -16777216). New test i32_const_four_byte_sleb_sign pins both, plus 41 80 80 80 7C = -8388608 as the negative control that was already right. The i64 helpers and the sc_run scan are unchanged and correct. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> * chore(seals): re-save fpga_fpga_wasm_board and fpga_fpga_wasm_opcodes after the i64 pairs (Refs #12371) The two specs moved in the previous commit; their seals are re-saved from the lane root with a master-built t27c and the twins synced. No spec change. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * dupe: trigit verbs write through handoff's put_lit, one copy of the loop (Closes #12419) #12388 added put_lit to specs/tri/handoff/handoff.t27 with the same loop body as put_s in specs/tri/trigit/verbs.t27, so the Duplicate Body Ratchet went red on every PR: "put_lit was copied [2] and is now copied [2, 2]". verbs.t27 already reads handoff.t27 (put_span, create_record, ...), so the one body stays in handoff and verbs' put_s delegates to it. put_lit now takes []const u8, like its sibling put_span: gen-rust lowered `string` to &'static str, and verbs passes runtime byte slices. String callers get .as_bytes() / b"..." from gen-rust; the bytes written are unchanged. dupe_scan: 1849 bodies in 691 groups (was 1851 in 692), ledger unchanged. test-report: handoff 12/12, verbs 17/17, handoff_view 4/4, 0 vacuous. Seals for the three specs re-saved by t27c built at master 672aaca. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * seals: drop the stale FpgaHdmiGrab seal that #12430 re-added (Closes #12461) Master commit b1a5857 (PR #12430) added .trinity/seals/fpga_FpgaHdmiGrab.json as a new file sealed on 2026-10-20 against a shape of specs/fpga/hdmi_grab.t27 that #12059 split up this morning. Since then `coverage` (seal-coverage.yml) and `spec-guards` (check_seal_currency.py) are red on master and on every PR that merged it: one seal, all four gen_hashes stale. Master had no seal for this spec before that commit, so the file is removed; a fresh seal from a master-built t27c is a follow-up PR. Local check_seal_coverage.py on this branch: OK, 3079 seals, 2966 hold, 113 known-broken listed in seal_baseline.txt. Refs #12387 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * numeric: drop the dead braceless invariant the parser discarded in zphi_alu.t27, reseal (Closes #12464) Master commit b1a5857 (PR #12430) added specs/numeric/zphi_alu.t27. Its `invariant sign_conj_negation` is written in the braceless form with an `if` statement inside the body; `parse_bdd_clauses` does not lower that shape, so the parser restores its checkpoint and drops the whole body (61 tokens, lines 483-493). The Corpus Ratchet's `parse-no-discard` phase refuses such a file, so every branch that carries b1a5857 is red on `Corpus Ratchet`. The invariant was never checked, and it cannot be made live as written: with the file's own `sign` and `conj`, sign(3, 5) = 1, conj(3, 5) = (3, -5), sign(3, -5) = 1, so the asserted `sc == -s` is 1 == -1. The claim is not a Z[phi] theorem either (the conjugate of 1 is 1). The block and its comment line are deleted; nothing else in the spec changes. After the edit `t27c parse-complete --show specs/numeric/zphi_alu.t27` reports "nothing discarded" and `t27c check` passes. The seal .trinity/seals/numeric_NumericZphiAlu.json is regenerated in the same commit from a master-built t27c, so `coverage` and `spec-guards` stay green after the spec edit. No ledger entry, no parser change. Refs #12387 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * fix(seal): re-save the T27osFrameGate seal that #12467 left stale (Closes #12486) #12467 (e376a06, merged 2026-10-25T15:20:07Z) changed specs/t27os/frame_gate.t27 without re-saving .trinity/seals/t27os_T27osFrameGate.json, so tools/check_seal_currency.py reports one STALE generated-code hash on master and every PR with base master is red on spec-guards. Re-saved with a master-built t27c (0.5.2+672aaca7d, newer than master's last bootstrap/src change 2b1858e) from the branch root: tests 12/12, gen_hash_rust cebbd2f90560, gen_hash_zig 5877f763f823, gen_hash_c d7aba556f229, gen_hash_verilog 575cb51da761, the four values the check computes from the spec. The spec is unchanged; the seal carries no home path. Refs #11640 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * ci(elab): baseline rows for the five specs/fpga modules the #12430 merge started emitting (Closes #12491) b1a5857 (the #12430 merge, 2026-10-25T13:29Z) brought specs/fpga/ hdmi_timing_640x480.t27, i2c_master.t27, lucas_accumulator.t27, sii9134_init.t27 and tmds_encoder.t27 onto master without rows in tools/elab_baseline.txt, so tools/check_elab_ratchet.py reads them as NEW and fpga-conformance is red on master (run 40197819164) and on every lane behind it (#12304, #12356, #12405). Five rows with the counts CI printed on that run (0, 20, 8, 2, 0; 384 -> 414) and one dated note. No existing row changes, no spec, generator or checker change. Refs #9367, #12387, #2325 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * gates(dupes): ledger row for the same group, the renamed remainder of the groups #12458 shrank (Closes #12498) #12458 (4f1c99a) deleted the bytes_equal, eq_s and mem_eql copies of the byte-equality body and dropped their ledger rows. The two copies it left, specs/tri/crypto/hex.t27:98 fn same and specs/igla/coder/tokenizer.t27:469 fn same_bytes, were members of those groups; tools/dupe_scan.py names a group by its alphabetically first member, so the remainder now reads `same 2` and was in no ledger. Neither file changed since 2026-10-23. One row added, nothing else. Replacing both bodies with std::mem::bytes_eq (and dropping the row again) stays with #12444. Refs #9367, #12387, #12444 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * port(scripts): move the build_tree use inside the 29 gen_w6NN modules so the parser keeps their closing brace; reseal (Closes #12497) #12458 (4f1c99a) replaced the local fn build_tree in gen_w631..657, 662 and 680 with `use port::scripts::gen_w_flat::build_tree;` on line 8, before `module gen_wNNN {` on line 9. The parser takes that form and drops the module's final `}` without an error (t27c parse-complete --show: 1 token DISCARDED, line 66); t27c check is blind to it, so the Corpus Ratchet reports 29 UNEXPECTED FAILURES [parse-no-discard] on master and on every lane behind it. The use line now sits first inside each module body; the constants, functions and tests do not change. The 29 seals are re-saved with the master-built t27c from the repository root. The parser defect itself (bootstrap/) is out of scope here. Refs #9367, #12387, #12444 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * seals(t27os): re-save the five t27os seals that #12373 added against older spec states (Closes #12509) #12373 (squashed to 70e3073) added seals for T27osDoctor, T27osGlassWindow, T27osLabPublish, T27osPtyServer and T27osReceiptName that were computed on its own branch, while master's copies of the five specs had moved on; they were stale the moment they landed, so coverage and spec-guards are red on master and on every PR that carries 70e3073 (FAIL: 6 seal(s) newly do not hold; STALE generated-code hash: 6). The five seals are re-saved with the master-built t27c 0.5.2 from the repository root at 70e3073; the gen hashes now equal the current= values spec-guards printed on master. Nothing else changes. The sixth stale seal, T27osSessionStore, is carried by #12495. Refs #9367, #12387 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> * fpga(wasm): restore the lane's board spec after the master merge (Refs #12371) The merge of master 0ff9452 into the top lane brought the squash twin of W1 (#12060, 128c830). The two specs on master equal W1 at 3b68aca and every W1 commit that touched them is in this branch's history, so the lane's side was taken for the eight content conflicts, and the two pieces git re-added as plain additions, one ok_rsp() in step_all and a second copy of the #12011 test block at the end of the file, are removed again here by restoring the lane's file byte for byte. The seals of the lane stay valid. Refs #12010 Refs #12202 Refs #12323 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 5.5 <noreply@anthropic.com>
Closes #12051
Refs #12171
Master carries two red checks in the FPGA lane, and this PR clears both.
fpga-conformance("Elaboration errors may fall, never rise") has been red because the two WASM law tableswasm_moduleandwasm_opcodeslanded without rows intools/elab_baseline.txt; the ratchet reads a module with no row as NEW.fpga-lint (read_verilog + hierarchy)has been red since #10949 landedspecs/fpga/hdmi_grab.t27on 2026-10-22, because gen-verilog copies a t27 char literal verbatim and Verilog reads'0as an unsized literal. A red that is always red hides a real regression on the same screen, and every lane underspecs/fpgahas been reading both. The compiler side of the second one stays open in #12171; this PR is the spec side.What changed
tools/elab_baseline.txtonly: two rows,wasm_module 6andwasm_opcodes 149, and a dated note under the notes mark. Nothing removed, no--bless, no spec change, no gate change. Master run 40109127962 at3365e74f66printedelaboration errors: 431 (baseline 276),NEW wasm_module: 6 errors, not in baseline,NEW wasm_opcodes: 149 errors, not in baseline; 276 + 6 + 149 = 431, so no other module had moved.wasm_opcodes 149is 149 timesConcatenation operand "'sd0" has indefinite width, all on one line, theROWSparameter: gen-verilog lowers a const array of structs to{0 /* OpRow {...} */, ...}, one unsized0per row, and the table has 149 rows. One construct, not 149 defects, and the table is the opcode oracle, not hardware.wasm_module 6is 4 timesUnable to bind wire/reg/memory src_len(an unsized array parameter, the gen-verilog: slice params ([]T) lower to single scalars — mac_dot_product is silently wrong for len>1 #2410 class) plus the 2Unable to elaborate condition expressionlines derived from them.specs/fpga/hdmi_grab.t27: the ten characters the checker compares bytes against are now constsCH_0..CH_SP, one home each, so no char literal is left. The libc host tail (HG_BUF,HG_LIST,HG_CMD,HG_PATH,hg_cat,hg_env,hg_sh,hg_slurp,hg_path,main) moved out of the file, because getenv, fork, execve and fopen cannot be Verilog either and a compiler fix alone would have moved the error, not removed it.specs/t27os/hdmi_grab_main.t27(new, moduleT27osHdmiGrabMain): that host tail, verbatim, importinghg_*,V_PASSandCH_0fromfpga::hdmi_grabbyuse, the wayspecs/t27os/plist_main.t27imports install/release. It adds two helpers (frame path, byte copy) with one test each.tools/elab_baseline.txt: rowhdmi_grab57 -> 5, total 431 -> 379, note dated 2026-10-25. The remaining 5 are 4 xpixel_at(a name taken byusefromvga_text_core, which gen-verilog does not bind) and 1 xnd_len(an unsized array param, gen-verilog: slice params ([]T) lower to single scalars — mac_dot_product is silently wrong for len>1 #2410).All code touched is
.t27; the baseline is a data file. No hand-written code in another language.Measured
On the regenerated
hdmi_grab.vfrom a master-equivalent t27c, local:yosys -p "read_verilog -sv -DSIMULATION hdmi_grab.v; hierarchy -top fpga_hdmi_grab" -q: exit 0.grep -c "\$signed('" hdmi_grab.v: 0.iverilog -g2012 -DSIMULATION: 5 error lines without the summary line, as the ratchet counts them: 4 xNo function named pixel_at, 1 xUnable to bind nd_len. That matches the 5 in the baseline row.t27c test-report:hdmi_grab14 of 14 pass, 0 vacuous;hdmi_grab_main2 of 2 pass, 0 vacuous.t27c genofhdmi_grab_mainspliced the imports into one.zig, andzig build-exe -lcbuilt a 1.9 MB binary with no diagnostics.The
wasm_moduleandwasm_opcodescounts are iverilog 12.0 on CI and the same counts locally.Success criteria, to be read from this PR's own run and not from this text: the
fpga-conformancestep printsOK: no module gained elaboration errorsand exits 0, andfpga-lint (read_verilog + hierarchy)passes.Risk
The t27b expectations ledger,
docs/reports/t27b_expectations.json(jobt27b-native-ratchet), has a row forspecs/fpga/hdmi_grab.t27that says blocked / "type [N]T", and no row for the newspecs/t27os/hdmi_grab_main.t27. That ledger is generated bytri t27b ratchet --blesson the lab and was not regenerated here. Read against the law inspecs/tri/t27b/steward.t27(entry_code, ratchet_red) andscripts/tri_loop/t27b.py, with the job's--prflag: a blocked row whose spec now passes is UNEXPECTED PASS, and a reference-passing spec with no row whose t27b verdict is pass or blocked is UNLISTED; neither is red on a pull request. Both are red on master until the refresh bot or a--blessrecords the row, and a blessed non-pass row also needs the cap raised with--accept-new, because the ledger sits at its cap (125 of 125). Only a t27b fail, mismatch, crash or timeout on a reference-passing spec would be red here. If that happens, the next commit is the fix or the regenerated ledger; it is not a reason to revert this split.Not claimed
use. This PR only removes the spec's exposure to the first and counts the second in the baseline.wasm_opcodes 149is a generator question and is only named here.🤖 Generated with Claude Code