Repository navigation
ci(fpga-build): synthesise the AX7203 WASM cell with a utilisation receipt (Closes #12411) - #12457
Conversation
…oop (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>
…ceipt (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>
… (Refs #12419) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…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>
…hi_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>
#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>
PR DashboardGenerated at: 2026-10-25 15:09:56 UTC
Summary
Seal Status
|
…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>
…into ci/fpga-synth-ax7203-12411
…' into ci/fpga-synth-ax7203-12411
|
Merged master (
No change to the synth job itself. |
PR DashboardGenerated at: 2026-10-26 01:02:28 UTC
Summary
Seal Status
|
… -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>
|
Thanks for the read. Two of the five items are fixed in place in
The other three are read against the generated cell rather than Verilog in general, and need no change:
🤖 Addressed by Claude Code |
PR DashboardGenerated at: 2026-10-26 01:22:35 UTC
Summary
Seal Status
|
…e 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>
…#12483) * policy: foreign exception for the AX7203 WASM board top (Refs #12456) Records the owner's 2026-10-25 approval of fpga/verilog/wasm_board_ax7203_top.v (at most 40 lines, label owner-approved-foreign, paid by deleting the ported fpga/verilog/link_node.v) in tools/policy/foreign-exceptions.txt. The local own-language hook reads this list from origin/master (lefthook.yml, since #7399), so a new foreign file cannot be committed on any branch until its entry is on master. This commit carries the entry only; the top follows in its own PR on top of #12457 (milestone A). No code changes. Refs #12411 Refs #9367 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> * policy: re-apply the AX7203 WASM board top exception after the master merge (Refs #12456) The merge of master 3888382 took master's side of the conflicting tail of tools/policy/foreign-exceptions.txt (the #12479 release-leg block, 2dafa31), which dropped this PR's one entry. This commit puts the same nine lines back, under the same owner word, after master's block. Nothing else changes. Refs #12411, #9367, #12387 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 Fable 5.1 <noreply@anthropic.com>
PR DashboardGenerated at: 2026-10-26 01:36:46 UTC
Summary
Seal Status
|
… 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>
|
Note, 2026-10-26 01:42Z: the Written by Claude Code |
PR DashboardGenerated at: 2026-10-26 02:17:12 UTC
Summary
Seal Status
|
Summary
Adds the CI job
fpga-synth-ax7203to.github/workflows/fpga-build.yml: the AX7203 WASM cell (module fpga_wasm_board, generated fromspecs/fpga/wasm_board_ax7203.t27) is synthesised for the board's own part,xc7a200tfbg484-2, and every run leaves a utilisation receipt.This is milestone A of #12411. There is no board top yet, so this is synthesis only; the board top and place-and-route are milestone B (#12456).
What the job does
The job
needs: fpga-smokeand reuses itsfpga-verilogartifact. It never rebuildst27c.github.event.beforeon push) and runs only whenspecs/fpga/wasm_board_ax7203.t27,specs/fpga/wasm_opcodes.t27or.github/workflows/fpga-build.ymlchanged. The base ref is passed throughenv:, not interpolated intorun:(scripts/ci/check_untrusted_shell_interp.pyreports OK).fpga-verilogartifact and check thatwasm_board_ax7203.vdeclaresmodule fpga_wasm_board.regbits (//comments stripped, packed and unpacked ranges multiplied) and fail with one::error::line naming gen-verilog: a module-level [N]u8 read and written inside the async-reset always block becomes 65536 registers, not block RAM #12297 if the sum exceeds 269200, the flip-flop count of the xc7a200t die. A 64 KiB memory page written as registers would be 524288 bits and is refused here, before the toolchain image is pulled.regymm/openxc7(6 tries with growing back-off).yosysin that image:read_verilog -sv -DSIMULATION,synth_xilinx -flatten -abc9 -arch xc7 -top fpga_wasm_board,stat,write_json. The call runs undertimeout 3600anddocker run --memory 12g, so an overrun ends with an exit code (124 or 137) that the error line names. yosys is found withcommand -v yosys, falling back to/yosys/yosys(the pathdocs/fpga/IGLA_FPGA_LAUNCH_PLAN.mduses).-sv -DSIMULATIONis the read convention ofbootstrap/src/service.rs;setundefis dropped.receipt.txt): spec sha256, commit, part, declared register bits, the cell counts LUT1..LUT6, FDRE, FDSE, CARRY4, RAMB18E1, RAMB36E1, DSP48E1 (awk handles both name-first and count-firststatlayouts), and theEstimated number of LCsline.wasm-board-ax7203-synth(yosys.log,fpga_wasm_board.json,receipt.txt, 14 days), also on failure.Why synthesis only
The cell has no board top yet (#12456), so there are no pin or clock constraints for place-and-route to work against. Synthesis against the real part already answers the question this job exists for: does the cell fit the AX7203's xc7a200t, and how much of it does it use. Board top and place-and-route follow in #12456.
Register-bit number for master's cell
Declared register bits in the current generated
wasm_board_ax7203.v(113regdeclarations): 4861, far under the 269200 budget. The count was cross-checked by two independent methods over a recentfpga-verilogartifact, since the job cannot be run locally (heavy-command hook, no docker or yosys on the Mac); it was validated here by reading, actionlint (with shellcheck), yamllint, the repo's untrusted-interpolation gate, and awk tests over that Verilog and over syntheticstattext.Foreign-line arithmetic
The own-language gate counts
.ymlas foreign: at most 40 added hand-written lines per file, 80 per PR, and added must not exceed deleted.git diff --numstat origin/master...HEAD:foreign-budget,own-languageandsecret-gateall passed on commit and on push, without--no-verify.The two removed helpers,
fpga/tools/synth_gf16_matrix.shandfpga/tools/load_sram.sh, targeted the Wukong's 676-ball part, not the AX7203, and the canonical path is thetriCLI (L7 UNITY). The one docs sentence indocs/reports/FPGA_LOOP_EVIDENCE_2026-07-04.mdrecords the removal. No other job infpga-build.yml, no gate file and no other workflow is touched.Test plan
fpga-synth-ax7203runs on this PR (the workflow file is in its own gate), reaches yosys and uploadswasm-board-ax7203-synth.receipt.txtshows the spec sha256, the commit, the part and the cell counts.fpga-build.ymljobs are unchanged.Closes #12411
Refs #9367
Refs #12387
🤖 Generated with Claude Code