Skip to content

t27b: / and % of two integer constants fold at compile time, as Zig folds them (Closes #7812) - #8027

Merged
gHashTag merged 13 commits into
masterfrom
t27b-const-div
Oct 9, 2026
Merged

gHashTag merged 13 commits into
masterfrom
t27b-const-div

Conversation

@gHashTag

@gHashTag gHashTag commented Oct 9, 2026 •

Copy link
Copy Markdown
Owner

Closes #7812. Part of #6063 (t27b coverage), which is item C10 of #6488.

What the reference does

specs/port/fpga/vivado/gf16_uart_sim_bench.t27 passes the reference 5/5. t27b refused it with ConstDecl ('CLK_DIV' is not a compile-time integer or bool). The line is pub const CLK_DIV : u32 = CLK_HZ / (UART_BAUD * 16);. coerce_plan.t27 folds + - * & | ^ on two typed constants and left / and % to run, so the quotient was not a constant.

t27c prints the constant as written, and Zig evaluates it at compile time. Measured on the t27c lab (t27c test-report, zig 0.16.0, x86_64 Debug), one probe per shape:

shape reference
HZ / (BAUD * 16) and HZ % (BAUD * 16), u32 175 and 1750000
A / B, i32, -7 and 2 -3 (truncates toward zero)
A % B, i32 blocked: "remainder division with 'i32' and 'i32': signed integers and floats must use @Rem or @mod"
A / Z with Z = 0, used blocked: "division by zero here causes illegal behavior"
the same, never used pass
(A * B) / 4, u8, where A * B overflows blocked: "overflow of integer type 'u8'"
A / B and A % B of constants inside a fn body pass (14 and 2)

Decision, with the evidence

The decision is a t27 plan, specs/tri/t27b/const_div_plan.t27, with 4 tests. It takes B_PERCENT from coerce_plan.t27 through use rather than writing it twice. t27c gen-rust turns it into gen/rust/tri/t27b/const_div_plan.rs, and lower.rs mounts that file with #[path].

In binary, where two constants of one integer type already fold for + - * & | ^, the glue now also computes the exact quotient or remainder and asks div_folds:

  • / folds when the divisor is not 0 and the quotient fits the type;
  • % folds on an unsigned type under the same two conditions;
  • everything else keeps its path. A module constant that is not a constant is refused as ConstDecl, as the reference refuses those shapes. An expression in a fn body runs, with its traps.

Conformance spec first

specs/tri/t27b/conformance/const_division.t27 has 5 tests:

  • gf16_uart_sim_bench's clock divider, checked as div * 16 * baud + rem == hz;
  • a remainder of two unsigned constants;
  • a constant divided by a literal;
  • a signed quotient that truncates toward zero;
  • a u64 quotient.
result
reference, t27c test-report 5/5, 0 vacuous, 8 runtime asserts; sealed (seal --save, then --verify: all hashes MATCH)
master's t27b refused: ConstDecl
this branch's t27b (aarch64 under qemu, t27b test --check) 5/5, 8 runtime asserts
  • Mutants. 8 mutants of the conformance spec flip one assert each. Every one fails exactly one test, in the reference and in t27b alike.
  • The plan. t27c test-report 4/4, 0 vacuous; sealed. All 6 plan mutants are caught by its tests.
  • tail.rs. The glue's Rust test (-7 / 2 folds to -3; a signed % and a zero divisor stay refused as ConstDecl) was dropped in the budget port below; the conformance spec and the plan's tests carry those cases.

tests/source.rs, one line. module_var_rejections_are_precise used var h: u32 = B / 2; as an initializer t27b could not fold. With this PR it folds, and the reference passes it too (1/1). The case now uses B / 0. t27b refuses it with the same VarDecl(module) message, and the reference refuses it ("division by zero").

Budget port (strict gate, see #8236)

The strict budget lets hand-written code under cli/t27b only shrink. This PR's glue adds 5 lines to lower.rs and removes 2, so the same PR ports more than that out of hand Rust:

  • ArithOp's tables. ArithOp::symbol, is_shift and commutative in cli/t27b/src/ir.rs were a match table and two matches! lists. They are now t27c gen-rust of specs/tri/t27b/arith_op.t27 (gen/rust/tri/t27b/arith_op.rs, mounted in ir.rs as ao), one line each. A compile-time assert! pins ArithOp's discriminants to the spec's codes, which are the numbering eval_arith.t27 uses. Reference 4/4, 0 vacuous; 38 of 38 assert mutants fail under both t27b and the reference.
  • One Rust test dropped. The tail.rs test of the constant division is gone. Its pass case is conformance/const_division.t27, which the corpus runs; its refusals are const_div_plan.t27's decisions.

Hand lines under cli/t27b against master: +14 -35, net -21.

Lines (git diff --numstat --no-renames origin/master...HEAD)

file kind added deleted
cli/t27b/src/ir.rs hand-written, ported out 8 32
cli/t27b/src/lower.rs hand-written glue 5 2
cli/t27b/tests/source.rs hand-written test, one case changed 1 1
gen/rust/tri/t27b/arith_op.rs t27c gen-rust, not hand-edited 86 0
gen/rust/tri/t27b/const_div_plan.rs t27c gen-rust, not hand-edited (with coerce_plan.t27's items, taken by use) 108 0
specs/tri/t27b/arith_op.t27 plan spec, 4 tests 135 0
specs/tri/t27b/const_div_plan.t27 plan spec, 4 tests 74 0
specs/tri/t27b/conformance/const_division.t27 conformance spec, 5 tests 70 0
.trinity/seals/*.json (3) t27c seal --save, schema 2 81 0
docs/reports/t27b_expectations.json ledger 5 2
AGENTS.md t27b remainder line 6 1

Gates and checks (t27c lab, tree merged with master cde548e)

  • check_budget() over git diff --numstat --no-renames cde548ecd...HEAD, built from cde548e's gen/c/policy/own_language.c: exit 0.
  • check_all() with cde548e's tools/policy/foreign-exceptions.txt and the name-status: exit 0.
  • cargo test --release -p t27b (aarch64 under qemu): 14 suites ok, 0 failed.
  • Generated code. t27c gen-rust of both plans with that tree's t27c is byte-identical to the committed files.
  • Seals. All three re-minted with that t27c (schema 2); seal --verify: all hashes MATCH.
  • AGENTS.md, re-measured with wc -l: 14742 plus 1222, tests 8284, against master cde548e's 14763 plus 1222 and 8284.
  • Ledger. gf16_uart_sim_bench.t27 goes from blocked to pass, and three new rows all pass. max_not_pass is recounted from the rows.

Corpus (t27c lab, t27b corpus specs, master's t27b against this branch's, 1731 files)

file master this branch
specs/port/fpga/vivado/gf16_uart_sim_bench.t27 blocked, ConstDecl pass, 5 tests, 14 asserts
specs/fpga/uart.t27 blocked, ConstDecl blocked, ExprFieldAccess
specs/ternary/bigint.t27 blocked, ConstDecl blocked, ExprCall(method)
specs/ternary/hybrid_bigint.t27 blocked, ConstDecl blocked, type gf16
specs/blog/t27b_progress.t27 pass, 5 tests, 8 asserts pass, 5 tests, 6 asserts

No other file changes.

  • The three still-blocked files are not in the ledger, because the reference does not pass them.
  • t27b_progress.t27 still passes. Two of its asserts compare constant quotients, which now fold at compile time, so they no longer count as runtime asserts.

t27b lab: signed receipt (#7686)

Head c587883 is this branch merged with master 3ac8bef (which brings #8252, see #8248). It is requested on the t27b lab with a fresh 32-byte challenge. The base is a signed run of master 3ac8bef, requested with its own challenge because the lab had no run of that commit. The compare will be posted here when both runs are in.

The 3ac8bef merge resolved only the AGENTS.md line, re-measured with wc -l. Its tree was checked again on the t27c lab: cargo test --release -p t27b 14 suites ok, gen-rust byte-identical, seal --verify all hashes MATCH, check_budget() and check_all() (3ac8bef's gate files) exit 0.

Earlier receipt (before the budget port)

Head 77c6e01 against its parent, master 7c88448. Head 77c6e01 is this branch's first commit, on master 7c88448. Both are signed runs of the deployed t27b lab: the base is the lab's own master run, and the head was requested with a fresh 32-byte challenge.

/work/t27c-master corpus-receipt compare BASE HEAD --challenge-head <mine>, run on the t27b lab from /work/t27:

base "7c884488c8983812295d29d8304090e3693495dc" AUTH_MISSING_NONE AUTHOR leaves-bound true
head "77c6e01cd8376f5ac7d11384ab44ab5e03acbb53" AUTH_MISSING_NONE FRESH leaves-bound true
  lane improved specs/port/fpga/vivado/gf16_uart_sim_bench.t27
  lane improved specs/tri/t27b/conformance/const_division.t27
  lane improved specs/tri/t27b/const_div_plan.t27
  lane neutral ... (28 files)
totals false inputs false verdicts false outputs false: IMPROVED_ONLY

Exit 3, IMPROVED_ONLY. The 28 lane neutral files pass on both sides; only their t27b asm output changed, because a / or % of two constants in them now folds at compile time rather than dividing at run time. They include specs/numeric/gft*.t27, specs/boards/*.t27, specs/basics/09_expressions.t27 and specs/verified/device_dna.t27. None changed verdict.

base 7c88448 head 77c6e01
files 1662 1664 (+2: the new specs)
t27b pass / pass_vacuous 989 / 153 992 / 153
t27b fail 19 19
jit_interp_mismatch / crash 0 / 0 0 / 0
reference pass 1177 1179
reference disagree (files / tests) 0 / 0 0 / 0
cargo test --release -p t27b (aarch64, qemu) 144 passed, 0 failed 145 passed, 0 failed

gf16_uart_sim_bench.t27 passes with 14 runtime asserts, the conformance spec with 8 and the plan with 13.

The final head, bccbdbc, is 77c6e01 merged with master a97cb9e. That brings in #7744, #7863, #7870, #7853, #7934, #7875, #7862, #7831, #7924, #7918, #8056, #8059, #7913 and #7925. The merge resolved only:

Its tree was checked on the t27c lab with the results under Gates. t27b corpus specs --blockers on the tree merged with master 4270760, against that master, gives the same moves as listed under Corpus (1699 files).

gen-rust gaps

None. The plan is decisions over u8, usize and bool.

Generated with Claude Code

claude and others added 2 commits October 9, 2026 01:06
…olds them (Closes #7812)

t27c prints `pub const CLK_DIV : u32 = CLK_HZ / (UART_BAUD * 16);` as
written, and Zig evaluates it at compile time. coerce_plan.t27 folds
`+ - * & | ^` on two typed constants and left `/` and `%` to run, so the
quotient was not a constant and specs/port/fpga/vivado/gf16_uart_sim_bench.t27
was refused as ConstDecl.

The decision is in specs/tri/t27b/const_div_plan.t27 (4 tests; `%`'s byte is
coerce_plan.t27's, taken by `use`), generated with `t27c gen-rust` to
gen/rust/tri/t27b/const_div_plan.rs and mounted in cli/t27b/src/lower.rs.
`/` folds when the divisor is not 0 and the quotient fits the type; `%`
folds on an unsigned type under the same conditions. The rest keeps its path:
a signed `%`, a zero divisor and a quotient that does not fit are refused in a
module constant, as the reference refuses them.

The conformance spec is specs/tri/t27b/conformance/const_division.t27:
`t27c test-report` 5/5, 0 vacuous. Glue: lower.rs +5 -2, tests/tail.rs +17,
tests/source.rs +1 -1 (module_var_rejections_are_precise used `B / 2` as an
initializer t27b could not fold; it now uses `B / 0`, which both sides refuse).
Ledger: gf16_uart_sim_bench.t27 now passes; the two new specs are new rows.

Part of #6063.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…27b-const-div (Closes #7812)

lower.rs and tests/tail.rs keep both sides. AGENTS.md takes master's and adds
this branch's step: 15235 plus 1233 and 8200, on master 4270760's 15232
plus 1233 and 8183. The ledger takes master's (no stored counts since #7862)
and re-applies this branch's rows; max_not_pass 31 -> 30.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@github-actions

github-actions Bot commented Oct 9, 2026

Copy link
Copy Markdown
Contributor

PR Dashboard

Generated at: 2026-10-09 06:50:44 UTC

Summary

Status Count
Total Open PRs 50
PRs with Failing Checks 39
PRs with All Checks Green 11
READY 0
FAILING 39
PENDING 0
NO CHECKS YET 0

These columns do not partition: 0 + 39 + 0 + 0 = 39, and there are 50 open PRs. A PR is being counted twice or not at all.

Seal Status

  • ⚠️ STALE -- sha256(compiler.rs)=3c0ade9e73e4 != manifest seal=87e5cbd3ad94.
    The committed NMSE numbers were certified against an older compiler.rs.
    Run scripts/reseal-check.sh locally for the two-step reseal command (advisory; not a merge gate).

lower.rs merges cleanly. AGENTS.md takes master's and adds this branch's
step: 15274 plus 1233 and 8208, on master 2dfe978's 15271 plus 1233 and
8191. The ledger merges cleanly; max_not_pass recomputed from the entries.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@github-actions

github-actions Bot commented Oct 9, 2026

Copy link
Copy Markdown
Contributor

PR Dashboard

Generated at: 2026-10-09 07:19:35 UTC

Summary

Status Count
Total Open PRs 50
PRs with Failing Checks 43
PRs with All Checks Green 7
READY 0
FAILING 43
PENDING 0
NO CHECKS YET 0

These columns do not partition: 0 + 43 + 0 + 0 = 43, and there are 50 open PRs. A PR is being counted twice or not at all.

Seal Status

  • ⚠️ STALE -- sha256(compiler.rs)=3c0ade9e73e4 != manifest seal=87e5cbd3ad94.
    The committed NMSE numbers were certified against an older compiler.rs.
    Run scripts/reseal-check.sh locally for the two-step reseal command (advisory; not a merge gate).

AGENTS.md takes master's and adds this branch's step: 15274 plus 1239 and
8222, on master 09ffc2f's 15271 plus 1239 and 8205. The ledger merges cleanly;
max_not_pass recomputed from the entries: 28.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…7812)

The only conflict was the ledger; master's rows and this PR's are kept and
max_not_pass is recounted from the rows.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@github-actions

github-actions Bot commented Oct 9, 2026

Copy link
Copy Markdown
Contributor

PR Dashboard

Generated at: 2026-10-09 18:49:32 UTC

Summary

Status Count
Total Open PRs 50
PRs with Failing Checks 46
PRs with All Checks Green 4
READY 0
FAILING 46
PENDING 0
NO CHECKS YET 0

These columns do not partition: 0 + 46 + 0 + 0 = 46, and there are 50 open PRs. A PR is being counted twice or not at all.

Seal Status

  • ⚠️ STALE -- sha256(compiler.rs)=557cd271f4e3 != manifest seal=87e5cbd3ad94.
    The committed NMSE numbers were certified against an older compiler.rs.
    Run scripts/reseal-check.sh locally for the two-step reseal command (advisory; not a merge gate).

…7812)

Master brings #8252 (lower.rs's source-text rules move to source_text.t27).
The only conflict was the AGENTS.md remainder line, re-measured with wc -l.
Hand lines under cli/t27b against 3ac8bef: net -21.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…7812)

Master brings #8028. Conflicts were the AGENTS.md remainder line (re-measured
with wc -l) and, where both sides moved rows, the ledger (rows kept from both
sides, max_not_pass recounted). Hand lines under cli/t27b against 325b0b1:
net -21.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…7812)

Master brings #8258 (lower.rs's body walks move to ast_walk.t27). Conflicts
were the AGENTS.md remainder line (re-measured with wc -l) and the ledger
(rows kept from both sides, max_not_pass recounted from the rows). Hand lines
under cli/t27b against ab5b3b7: net -21.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@github-actions

github-actions Bot commented Oct 9, 2026

Copy link
Copy Markdown
Contributor

PR Dashboard

Generated at: 2026-10-09 20:22:39 UTC

Summary

Status Count
Total Open PRs 50
PRs with Failing Checks 44
PRs with All Checks Green 6
READY 0
FAILING 44
PENDING 0
NO CHECKS YET 0

These columns do not partition: 0 + 44 + 0 + 0 = 44, and there are 50 open PRs. A PR is being counted twice or not at all.

Seal Status

  • ⚠️ STALE -- sha256(compiler.rs)=557cd271f4e3 != manifest seal=87e5cbd3ad94.
    The committed NMSE numbers were certified against an older compiler.rs.
    Run scripts/reseal-check.sh locally for the two-step reseal command (advisory; not a merge gate).

@github-actions

github-actions Bot commented Oct 9, 2026

Copy link
Copy Markdown
Contributor

PR Dashboard

Generated at: 2026-10-09 20:34:29 UTC

Summary

Status Count
Total Open PRs 50
PRs with Failing Checks 45
PRs with All Checks Green 5
READY 0
FAILING 45
PENDING 0
NO CHECKS YET 0

These columns do not partition: 0 + 45 + 0 + 0 = 45, and there are 50 open PRs. A PR is being counted twice or not at all.

Seal Status

  • ⚠️ STALE -- sha256(compiler.rs)=557cd271f4e3 != manifest seal=87e5cbd3ad94.
    The committed NMSE numbers were certified against an older compiler.rs.
    Run scripts/reseal-check.sh locally for the two-step reseal command (advisory; not a merge gate).

@gHashTag
gHashTag merged commit da44826 into master Oct 9, 2026
28 of 31 checks passed
gHashTag pushed a commit that referenced this pull request Oct 9, 2026
…ed (Closes #7902)

Master brings #8027. The only conflict was the AGENTS.md remainder line,
re-measured with wc -l; max_not_pass is recounted from the rows. Hand lines
under cli/t27b against 54f3c14: net -5.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
gHashTag pushed a commit that referenced this pull request Oct 9, 2026
…Closes #7909)

Master brings #8027. The only conflict was the AGENTS.md remainder line,
re-measured with wc -l; max_not_pass is recounted from the rows. Hand lines
under cli/t27b against 54f3c14: net -7.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
gHashTag added a commit that referenced this pull request Oct 9, 2026
…loses #8347) (#8350)

* t27b: the node scans of lower.rs move to specs/tri/t27b/ast_scan.t27 (Closes #8347)

names_in, array_locals, decls_of, calls_in, scan_addr_taken,
count_assigns, ref_mutable_names, misprinted_ifs and mark_tail_returns
are now t27c gen-rust of specs/tri/t27b/ast_scan.t27
(gen/rust/tri/t27b/ast_scan.rs), mounted in lower.rs as `ax`. Each scan
reads ast_walk.t27's bytes of the node list (`flat`) and writes a mark
per node it collects; `marked` returns the marked nodes in preorder, and
each collector keeps its signature with a one-line body.

A differential of the deleted collectors against the new ones agrees on
1,000,000 random forests: sets, counts, the preorder of calls_in and
decls_of, and the node addresses misprinted_ifs and mark_tail_returns
collect.

docs/reports/t27b_expectations.json gets the new spec's row: t27b passes
it (9 of 9 tests).

Hand Rust under cli/t27b: 111 lines deleted, 20 added, net -91. See
#6198.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

* verified: ed25519.t27 states it makes no constant-time claim (Refs #8041) (#8065)

Replaces the one-line constant-time remark with an honest paragraph: no
timing claim is made or checked, sign/public_key touch the secret seed,
and the masked selects are shape, not a guarantee. Records the #8041
Wycheproof and differential-fuzz results. Comment-only change: generated
Rust is byte-identical; seal spec_hash refreshed, 16/16 tests pass.

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
Co-authored-by: Claude <claude@anthropic.com>

* verified(corpus_receipt): a request the lab has not fetched yet waits 30 min instead of being dropped (Closes #8320) (#8329)

`corpus-receipt admit` dropped a lane request at once when its sha was
not a branch head or on master's first-parent line as the lab last
fetched it. On 2026-10-09 that dropped four lane heads and the first
request for #8028's squash commit c6237a7, before the lab had fetched
it.

request_verdict() now answers WAIT_ORIGIN (5) for a sha not on origin
that has waited at most REQUEST_ORIGIN_GRACE_S (1800 s), and
request_exit() maps it to 2. lab.py already keeps any request whose
admit exit is neither 0 nor 1, so no hand-written line changes. Waiting
never runs a request: running still needs the sha on origin, so the
bound on who can put code in front of the signing step is unchanged.

Generated bootstrap/gen/rust/verified/corpus_receipt.rs with t27c
gen-rust; seal re-saved, 32 of 32 tests pass. On the t27c lab:
admit gives WAIT_ORIGIN/2 for 0,0,0 and 1800,3,0; NOT_ON_ORIGIN/1 for
1801,0,0; ADMIT/0 for 0,0,1; QUEUE_FULL/1 for 0,4,1; EXPIRED/1 for
21601,0,1. cargo test -p t27c -- receipt: 18 passed.

Co-authored-by: Claude <claude@anthropic.com>
Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

* skills: t27b-loop, one tick of the unattended t27b improvement loop (Closes #8331) (#8332)

Budget guard, health checks with self-repair (hooksPath, master's red
checks, lab staleness and deploy drift, disk, agents), merge-when-green
rules, one plan step through the t27c lab, and a ledger line. Records
the 2026-10-09 traps that stalled lanes: absolute core.hooksPath,
UNSTABLE refusing --auto, specs landing without ledger rows, the lab
dropping unfetched requests, closing keywords in prose. Part of the
loop epic (see #8326).

Co-authored-by: Claude <claude@anthropic.com>
Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

* t27c silicon reuses its bitstream; a ported script pays for the glue (Closes #8295) (#8296)

* t27c silicon reuses its bitstream; math_compare's Pell code moves to t27 (Closes #8295)

Wires specs/verified/bitstream_reuse.t27 (#8291) into t27c silicon. The
cache key hashes every input that can change a bit. A complete, intact
entry is loaded instead of running yosys, nextpnr and fasm2frames, and
every passing build is stored. Measured on this Mac with --skip-hardware
(so no board was touched): ternary_link built in 39 s, then the second
run printed 'bitstream REUSED' and finished in 4 s. The control bitstream
and the readback are untouched.

Hand-written code may not grow (owner rule 2026-10-09), so the same diff
ports math_compare.rs's Pell code to specs/math/pell_hybrid.t27: pell_u64,
pell_f64, hybrid_inner_product, hybrid_v2_cosine.
- The spec has 7 tests, 0 vacuous. Its GOLDEN_V2 vectors are held to
  1e-9; the Rust tests held them to 1e-6.
- math_compare.rs now calls the generated code, and all 10 of its existing
  Rust tests pass.
- Foreign lines: +39 -68, so a net of -29.

gen-rust lowers @sqrt of a bare float literal to (5.0).sqrt(), which rustc
rejects. The spec works around it with a typed constant.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

* Pay for the bitstream-reuse glue by deleting a ported script, not math_compare.rs (Closes #8295)

own-language refused the previous push: bootstrap/src/math_compare.rs is not
on the owner's exception list, so it may not be edited at all, not even to
remove code. The Pell port is withdrawn from this PR.

The glue's +32 lines are now offset by deleting scripts/gen_w662.py (145
lines). Its .t27 port, specs/port/scripts/gen_w662.t27, already exists
(#8160), and nothing references the .py. Deleting a whole file is allowed
for any hand-written file. Net hand-written change: -114.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

* bitstream reuse: the venv in the key, and every 10th hit is audited (Closes #8295)

Two weak spots from the loop ledger (#8314), both from Bazel's remote-cache
experience:
- an undeclared input poisons a cache, and fasm2frames and prjxray run
  under the openXC7 venv, so its pip freeze joins the key;
- nothing ever rechecked a hit. Every AUDIT_EVERY-th (10) hit is now
  rebuilt and compared; a mismatch deletes the entry and says so.

The first audit run found a real anomaly. Two builds of the same inputs
differed in 3 bytes, at offsets 162..165: the .bit header's build date
and time. So the audit compares the configuration stream from the sync
word 0xAA995566 (BIT_SYNC_WORD). Re-measured without hardware: audit run
'byte-identical', hits 10, then a REUSE run in 5 s.

Spec: 7 tests, 0 vacuous; the two new mutants are killed.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

---------

Co-authored-by: Claude <claude@anthropic.com>
Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

* t27b: / and % of two integer constants fold at compile time, as Zig folds them (Closes #7812) (#8027)

t27c prints `pub const CLK_DIV : u32 = CLK_HZ / (UART_BAUD * 16);` as
written, and Zig evaluates it at compile time. coerce_plan.t27 folds
`+ - * & | ^` on two typed constants and left `/` and `%` to run, so the
quotient was not a constant and specs/port/fpga/vivado/gf16_uart_sim_bench.t27
was refused as ConstDecl.

The decision is in specs/tri/t27b/const_div_plan.t27 (4 tests; `%`'s byte is
coerce_plan.t27's, taken by `use`), generated with `t27c gen-rust` to
gen/rust/tri/t27b/const_div_plan.rs and mounted in cli/t27b/src/lower.rs.
`/` folds when the divisor is not 0 and the quotient fits the type; `%`
folds on an unsigned type under the same conditions. The rest keeps its path:
a signed `%`, a zero divisor and a quotient that does not fit are refused in a
module constant, as the reference refuses them.

The conformance spec is specs/tri/t27b/conformance/const_division.t27:
`t27c test-report` 5/5, 0 vacuous. Glue: lower.rs +5 -2, tests/tail.rs +17,
tests/source.rs +1 -1 (module_var_rejections_are_precise used `B / 2` as an
initializer t27b could not fold; it now uses `B / 0`, which both sides refuse).
Ledger: gf16_uart_sim_bench.t27 now passes; the two new specs are new rows.

Part of #6063.

Co-authored-by: Claude <claude@anthropic.com>
Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

* spec(automation): tri-claim-batch v1 -- withdraw every accepted spec in a few wallet transactions (#8349)

Owner, 2026-10-09: "withdraw everything" -- 874 accepted specs on
dmitrii-f-t27, one press each until now. At most 16 mint messages per
request (4 earnings at a time to the signers), the wallet's own message
limit per transaction (4 by default, 255 at most), only earnings neither
revoked nor sent, oldest first, a cancelled prompt stops the run. The
minter is unchanged.

6/6 PASS, 9/9 negative controls caught, validate-vacuity 0 of 6.

Closes #8348

phi^2 + 1/phi^2 = 3 | TRINITY

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
Co-authored-by: Claude <claude@anthropic.com>
Co-authored-by: Dmitrii Fedorov <dmitrii.f@t27.ai>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

t27b: / and % of two integer constants fold at compile time (gf16_uart_sim_bench)

2 participants