fix(fpga): compute theorem_matrix_ok instead of hardcoding it true

[gHashTag]

Refs #2306 (item 1 of two; see "Scope" at the bottom for why this is Refs and not Closes).

The defect is live on origin/master

Re-verified on ee494b990 immediately before pushing — cli/tri/src/fpga.rs:6101:

    let theorem_matrix_ok = true;

consumed at :6342 as the conjunct

        && (!run_theorem_matrix || theorem_matrix_ok)

Those were its only two mentions. There was no theorem-matrix phase body in smoke_gate(), so --theorem-matrix reported the phase passed without executing a line of it, report["theorem_matrix"] kept the null from its initializer at :5970, and the process exited 0.

This fails open, unlike its sibling dry_run_sweep_ok (#2304, fixed in #2305), which was declared false and never assigned and so failed closed — unpassable and loud.

Which case this is: compute it

The underlying check does exist; only its call site was gone. rustc had been saying so on every build:

warning: function `generate_theorem_matrix` is never used
warning: function `replay_theorem_matrix` is never used
warning: function `build_theorem_matrix_report` is never used
warning: function `pvt_context_inside_envelope` is never used
warning: function `cclk_period_ns` is never used
warning: unused variable: `replay_fixtures`
warning: unused variable: `dry_run_live`

and the 24-variant block those functions emit is still committed in tests/fixtures/fpga/smoke-gate/validate_lean_standalone_snapshot.json. So the honest fix is to compute the flag, not to delete it and not to leave a plausible-looking true.

The change

let mut theorem_matrix_ok = false; plus the restored phase, in the same shape verify_lean_ok uses twenty lines above: set the flag and write the report entry inside the success path, record the phase as failed and bail! otherwise.

--replay-fixtures and --dry-run-live were unused parameters — --replay-fixtures had been silently regenerating instead of replaying — and are now wired to replay_theorem_matrix and to the documented dry_run_live label and theorem-matrix-dry-run-live/ directory.

The three bars

TRUE

cargo test -p tri — 168 passed; 0 failed. cli/tri/src/fpga.rs is rustfmt-clean (the other 12 files in the crate have pre-existing cargo fmt --check diffs on master; none is touched here).

ALIVE

The phase does real work: 24 .lean files on disk, 2 theorem declarations each, every one run through verify_lean.

[smoke-gate] theorem-matrix OK (24 variants, source=synthetic, replay=false)
[smoke-gate] complete (passed: true)

$ ls build/fpga/theorem-matrix-fixtures/*.lean | wc -l
24
$ grep -h "^theorem " build/fpga/theorem-matrix-fixtures/theorem_matrix_ss_oscfsel_7.lean
theorem smoke_gate_ss_oscfsel_7_synthetic_ss_oscfsel_7_30_15_15_satisfies_flash_spec :
theorem smoke_gate_ss_oscfsel_7_synthetic_ss_oscfsel_7_30_15_15_transaction_ok (bits : Nat) :

The new test opens each variant's .lean off disk rather than trusting the JSON block, because a report object alone is satisfiable by a literal.

BITING — two guards, two separate mutants

One mutant per guard, not one per file: assertions abort in order, and mutant B is chosen so that every variant it produces is valid, which means it cannot trip guard A and therefore proves guard B on its own.

Mutant A — sabotage the underlying property. pvt_context_inside_envelope bound flipped, ctx.temp_c >= PVT_TEMP_MIN_C → ctx.temp_c > PVT_TEMP_MAX_C, so the envelope check is false for every context.

Before (master, mutant planted) — the verdict still reports OK:

[smoke-gate] complete (passed: true)
CLI exit code = 0
  "passed": true,
  "theorem_matrix": null,

After (this branch, same mutant) — it bites:

Error: theorem-matrix generation failed: theorem-matrix envelope-check failed for corner ff OSCFSEL 0: synthetic PVT context is outside the operating envelope
CLI exit code = 1

and through the test:

thread 'fpga::tests::test_smoke_gate_json_theorem_matrix_is_computed' panicked at cli/tri/src/fpga.rs:10201:9:
smoke-gate theorem-matrix path failed: Err(theorem-matrix generation failed: theorem-matrix envelope-check failed for corner ff OSCFSEL 0: synthetic PVT context is outside the operating envelope)

Mutant B — cut the matrix short. for corner_str in ["ff", "tt", "ss"] → ["ff", "tt"] in generate_theorem_matrix only (the identical line in replay_theorem_matrix left alone). All 16 variants it emits verify cleanly, so guard A stays silent.

Before (master, mutant planted):

CLI exit code = 0
  "passed": true,
  "theorem_matrix": null,

After (this branch, same mutant):

Error: theorem-matrix verified 16 variants, expected 24
CLI exit code = 1

thread 'fpga::tests::test_smoke_gate_json_theorem_matrix_is_computed' panicked at cli/tri/src/fpga.rs:10201:9:
smoke-gate theorem-matrix path failed: Err(theorem-matrix verified 16 variants, expected 24)

Reverted, both mutants removed:

test fpga::tests::test_smoke_gate_missing_bitstream_matches_snapshot ... ok
test fpga::tests::test_smoke_gate_json_synthetic_verify_lean ... ok
test fpga::tests::test_smoke_gate_json_theorem_matrix_is_computed ... ok
test fpga::tests::test_smoke_gate_validate_lean_standalone_matches_snapshot ... ok
test fpga::tests::test_smoke_gate_json_synthetic_validate_lean_standalone ... ok

test result: ok. 5 passed; 0 failed

Why the existing suite was blind to it

test_smoke_gate_json_synthetic_verify_lean already passes run_theorem_matrix = true and asserts passed == true. That is exactly the assertion a hardcoded true satisfies for free, which is why a test that runs in CI today could never have caught this. The new test reads the theorem_matrix phase itself, checks all 24 corner/OSCFSEL pairs appear exactly once, and opens the generated theorems.

Nothing weakened

No || true, no continue-on-error, no relaxed assertion, no dropped case. One addition that is not the defect: smoke_gate() derives its dry-run and fixture directories from the repo root rather than from arguments and clears stale logs there on entry, so a second concurrent smoke-gate test made it die on remove ... boot-log-*.json: No such file or directory. Only one test reached those directories before, so the race had nothing to collide with. The four smoke-gate tests now take a mutex — serialisation only, no assertion touched.

Cargo.lock is deliberately not in this PR: local cargo runs pruned 20 lines from it, which is a build artifact of my machine and not part of this change.

Scope — why Refs #2306 and not Closes

#2306 reports two defects and its own "Suggested order" puts this one first as "a live false-green today". Item 2, validate_lean_standalone_ok, is deliberately not fixed here:

• it fails closed, not open, so it is not a false green;
• it has no success point to attach an assignment to — the phase body has to be written back from scratch;
• both of its tests return early without lake on PATH, which is on neither this machine nor the cli-tri runner, so I could not execute a candidate implementation even once.

Landing a phase body that cannot be run, behind a proof gate, is how an unproven guard gets in. #2306 stays open on item 2, which is what Refs records. Its own text already documents that item fully, so no duplicate issue is filed.

Corpus Ratchet, Seal Coverage and FPGA E2E Build are red on master already and are not required contexts.

[github-actions]

PR Dashboard

Generated at: 2026-08-21 15:59:56 UTC

• fix(fpga): compute theorem_matrix_ok instead of hardcoding it true #2343 fix(fpga): compute theorem_matrix_ok instead of hardcoding it true | Created: 2026-08-21 | Updated: 2026-08-21 | 20 failing / 26 total
• fix(bitnet): make the DMA local write strobe a pulse, not a level #2339 fix(bitnet): make the DMA local write strobe a pulse, not a level | Created: 2026-08-21 | Updated: 2026-08-21 | 5 failing / 33 total
• corpus: freeze the damage, patch one class at a time, and say where one rule stops #2161 corpus: freeze the damage, patch one class at a time, and say where one rule stops | Created: 2026-08-14 | Updated: 2026-08-21 | 0 failing / 9 total
• Unbreak FPGA CI and correct two unbacked hardware claims #2081 Unbreak FPGA CI and correct two unbacked hardware claims | Created: 2026-08-11 | Updated: 2026-08-20 | 5 failing / 27 total

Summary

Status	Count
Total Open PRs	4
PRs with Failing Checks	2
PRs with All Checks Green	2
READY	1
FAILING	2
PENDING	0

Seal Status

• ⚠️ STALE -- sha256(compiler.rs)=65f033d04125 != 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]

📓 NotebookLM Notebook linked to this PR

• Notebook ID: b83263109fb055dc
• URL: https://notebooklm.google.com/notebook/b83263109fb055dc

This notebook contains session context, decisions, and artifacts for this work.