smoke-gate: theorem_matrix_ok is a hardcoded true (false green), and validate_lean_standalone has no phase body

[gHashTag]

Follow-up to #2304 (fixed in #2305). While fixing dry_run_sweep_ok I read the whole smoke_gate() verdict through. The #2228 batch merge dropped three phase bodies, not one. #2305 restored the first. The other two are still on master, and one of them fails open.

All line numbers are against master @ d51db4ac10d38169449535067d0b831acd8a01c5.

1. theorem_matrix_ok is a hardcoded true — this is a false green

6101:    let theorem_matrix_ok = true;
6342:        && (!run_theorem_matrix || theorem_matrix_ok)

Those are its only two mentions. There is no theorem-matrix phase body anywhere in smoke_gate(). So when a caller passes --theorem-matrix, the gate reports that phase passed without executing a single line of it.

This is the more serious of the two. dry_run_sweep_ok failed closed — unpassable, loud, and it blocked CI for 12 runs until someone looked. theorem_matrix_ok fails open: it is a conjunct that can never be false, so it silently certifies work that never happened. It is the same absence-is-not-a-value defect closed in #2285, #2287 and #2302, except the gate is asserting success rather than refusing to look.

The three helper functions that phase would have called are still in the file, defined and never called — which is the evidence that a body was removed rather than never written:

6372: fn generate_theorem_matrix(
6509: fn replay_theorem_matrix(
6610: fn build_theorem_matrix_report(

The compiler has been saying so on every run:

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

report["theorem_matrix"] is likewise never written; it keeps the null from its initializer at 5970.

2. validate_lean_standalone_ok — same two-mention shape, no success point

6100:    let mut validate_lean_standalone_ok = false;
6343:        && (!validate_lean_standalone || validate_lean_standalone_ok)

Its phase body is absent too, so unlike dry_run_sweep_ok this one cannot be fixed by mirroring verify_lean_ok — there is no success point to attach an assignment to. The phase has to be written back.

It fails closed, and it is currently masked twice over: the conjunct is guarded by !validate_lean_standalone, and both of its tests return early when lake is not on PATH:

test fpga::tests::test_smoke_gate_json_synthetic_validate_lean_standalone ... ok
test fpga::tests::test_smoke_gate_validate_lean_standalone_matches_snapshot ... ok

Those two ok results are skips, not passes. SKIP: lake not on PATH. The moment a runner has lake installed, both fail — the tests assert validate_lean_standalone is an object with status: "ok" and an elapsed_ms, and nothing ever writes that key.

Note this is exactly how #2304 stayed invisible: a test that returns early reads as green.

Why these did not surface with #2304

--theorem-matrix and --validate-lean-standalone are not exercised by the cli-tri build job, and both conjuncts are guarded, so neither affects the check that #2305 turned green. They are latent, not active.

Suggested order

1. theorem_matrix_ok first — it is a live false-green today, not a latent one. Either restore the phase body from the pre-fix(tri): restore the seven definitions a batch merge dropped #2228 commit, or, if the phase is not coming back, delete the flag and its conjunct together with the three orphaned helpers. What it must not stay is a hardcoded true sitting in a verdict.
2. validate_lean_standalone_ok — restore the phase body; its tests already specify the required report shape (status: "ok" plus elapsed_ms), so they define the target.
3. Consider whether the guarded-conjunct idiom (!run_x || x_ok) is worth keeping. It is what let two missing phases sit unnoticed: a phase that does not exist and a phase that was not requested are indistinguishable in the verdict.

Recovering the dropped bodies from the #2228 parent commit is likely faster than rewriting, the way 494e659d8 supplied verify_lean_ok.

[gHashTag]

Item 1 landed in #2343 (merged, bd2d25df4b2e5bcc4cca61eb3da3b3505c73df7d). Item 2 is still live — leaving this issue open.

The defect was still on master verbatim when I started, at the line this issue quotes: cli/tri/src/fpga.rs:6101, let theorem_matrix_ok = true;, consumed at :6342. The suggested order here was right — this one was the live false-green.

It was the compute it case, not the no such check exists case, exactly as this issue predicted. All five functions the phase needs were still in the file and rustc was reporting them unused: the three named here plus pvt_context_inside_envelope and cclk_period_ns, the two properties they actually check. --replay-fixtures and --dry-run-live were unused parameters too, so --replay-fixtures had been silently regenerating rather than replaying; both are now wired.

Two guards, two separate mutants, since assertions abort in order:

• Flipping the PVT envelope bound to > PVT_TEMP_MAX_C — on master the gate still printed [smoke-gate] complete (passed: true) with "theorem_matrix": null and exit 0; after the fix it exits 1 with theorem-matrix generation failed: theorem-matrix envelope-check failed for corner ff OSCFSEL 0: synthetic PVT context is outside the operating envelope.
• Walking two corners instead of three, chosen so every variant it emits is valid and guard A stays silent — master again exits 0 with passed: true; after the fix, theorem-matrix verified 16 variants, expected 24.

Worth recording why the suite never caught it: test_smoke_gate_json_synthetic_verify_lean already passes run_theorem_matrix = true and asserts passed == true. That is precisely the assertion a hardcoded true satisfies for free, so a test running in CI today could not have caught this. The new test reads the theorem_matrix phase itself and opens each variant's .lean off disk.

Item 2, validate_lean_standalone_ok, deliberately not touched. It fails closed rather than open, it has no success point to attach an assignment to, and both its tests return early without lake on PATH — which is on neither my machine nor the cli-tri runner. I could not execute a candidate implementation even once, and landing an unrunnable phase body behind a proof gate is how an unproven guard gets in. Your point 3 (whether (!run_x || x_ok) is worth keeping) is also untouched and still stands.

[gHashTag]

Mutation evidence for #2343 — the theorem-matrix guard bites

The audit that reviewed #2343 confirmed it structurally but left the BITING bar unverified (a cli/tri build was judged unsafe on disk at the time). Settled now: cli/tri was built and its test suite run against master 6b19d8bebf825205d0fbc1e63a4205d7f904f563, and mutants were planted one per guard.

What master actually contains

cli/tri/src/fpga.rs:6101:    let mut theorem_matrix_ok = false;
cli/tri/src/fpga.rs:6455:        && (!run_theorem_matrix || theorem_matrix_ok)

Pre-#2343 that first line was let theorem_matrix_ok = true; (line 6101 then too; the consumption site sat at 6342 before the +113-line phase body shifted it to 6455). Confirmed against the merged patch itself, not from memory:

$ gh api repos/gHashTag/t27/pulls/2343/files --jq '.[0].patch' | head
@@ -6098,7 +6098,7 @@ fn smoke_gate(
-    let theorem_matrix_ok = true;
+    let mut theorem_matrix_ok = false;

Bar 1 — TRUE

cargo test -p tri on a clean checkout of 6b19d8bebf825205d0fbc1e63a4205d7f904f563:

test result: ok. 168 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 22.70s

The new test runs; it does not take the !bit.is_file() early return. fpga/verilog/ternary_mac_demo_top_200t.bit is present (9,730,768 bytes), and with --nocapture the run contains zero SKIP: demo bitstream not found lines and two [smoke-gate] theorem-matrix OK (24 variants, source=synthetic, replay=false) lines.

Correction to the earlier audit note: the suite is not zero-SKIP. Three unrelated tests skip on this machine —

test fpga::tests::test_measured_to_lean_standalone_builds_in_temp_lake_package ... skip: lake not on PATH
test fpga::tests::test_smoke_gate_json_synthetic_validate_lean_standalone ... SKIP: lake not on PATH
test fpga::tests::test_smoke_gate_validate_lean_standalone_matches_snapshot ... SKIP: lake not on PATH

test_smoke_gate_json_theorem_matrix_is_computed is not among them.

Bars 2 and 3 — ALIVE and BITING

One mutant per guard, each planted and reverted separately, each rebuilt and re-run:

#	Mutant	Guard it targets	Result
M1	continue before the push for tt/OSCFSEL 3 — 23 variants walked	variant-count check	FAIL
M2	envelope predicate forced false for tt/OSCFSEL 3, all 24 still walked	per-variant property	FAIL
M3	overwrite that variant's .lean after verify_lean ran	on-disk artefact assertion	FAIL
M4	fail-open restore: let mut theorem_matrix_ok = true;	verdict conjunct	survives — see below
M5	delete the theorem_matrix_ok = true; success assignment	verdict conjunct is wired	FAIL

Quoted failures, so the assertion is visibly reading the right span rather than merely reporting FAILED:

M1: smoke-gate theorem-matrix path failed: Err(theorem-matrix verified 23 variants, expected 24)

M2: smoke-gate theorem-matrix path failed: Err(theorem-matrix generation failed:
    theorem-matrix envelope-check failed for corner tt OSCFSEL 3:
    synthetic PVT context is outside the operating envelope)

M3: variant tt/3 .lean fixture declares no theorem:
    .../build/fpga/theorem-matrix-fixtures/theorem_matrix_tt_oscfsel_3.lean

M5: smoke-gate theorem-matrix path failed: Err(smoke-gate did not pass all phases)

M3 is the interesting one: the gate printed [smoke-gate] complete (passed: true) and the report block still said 24/ok. The test caught it anyway, because it opens each variant's .lean off disk. That is the "a report block alone would be satisfiable by a JSON literal" guard the PR author wrote, and it is real.

About M4 — it survives, and it is not a fail-open

Restoring the hardcoded flag alone leaves the test green. Read literally that is the fail-open signature, so it was checked rather than assumed: M4 was re-run composed with M1, i.e. hardcoded verdict flag and a genuinely broken 23-variant matrix.

M4+M1: smoke-gate theorem-matrix path failed: Err(theorem-matrix verified 23 variants, expected 24)

The gate still fails. Every failure path inside the restored phase — replay error, generation error, variant-count mismatch — exits through bail! before passed is ever computed, so theorem_matrix_ok == false is unreachable at line 6455 and the conjunct is a tautology given the surrounding control flow. M4 is therefore an equivalent mutant: it changes no reachable behaviour. M5 confirms the conjunct is nonetheless genuinely consumed (removing the success assignment flips passed to false and the gate bails).

Conclusion: no defect. #2343 is complete for the half of this issue it claimed. A broken theorem matrix cannot green the gate, with or without the old hardcoded flag. No follow-up issue filed and no change made to cli/tri/src/fpga.rs.

Why this issue should stay open

The other half named in this issue's title is still unfixed on master:

$ grep -n validate_lean_standalone_ok cli/tri/src/fpga.rs
6100:    let mut validate_lean_standalone_ok = false;
6456:        && (!validate_lean_standalone || validate_lean_standalone_ok)

Initialised false, never assigned anywhere — --validate-lean-standalone still has no phase body. It fails closed rather than open, so it is not a false green, but the phase does not exist. The three lake not on PATH skips above mean the tests that would exercise it did not run on this machine either.

All work was done in a throwaway worktree off freshly fetched origin/master; the worktree has been removed and no file on master was modified.

[gHashTag]

Re-verified both halves against master @ 6dcefd044c276c0453f7ce2c7206718d480052e5 during an unrelated fail-open sweep. Part 1 is fixed; part 2 is still live. Recording it so nobody re-does the first half.

Part 1 — theorem_matrix_ok: FIXED

The hardcoded true is gone. At the current head:

6101:    let mut theorem_matrix_ok = false;
6380:        theorem_matrix_ok = true;
6455:        && (!run_theorem_matrix || theorem_matrix_ok)

The phase body is back (if run_theorem_matrix { at 6297), report["theorem_matrix"] is now written at four sites (6307, 6346, 6365, 6381) instead of keeping its null, and all three formerly-orphaned helpers are called rather than merely defined — generate_theorem_matrix, replay_theorem_matrix and build_theorem_matrix_report each now occur more than once in the file. A regression test was added alongside it at 10152, whose message names the exact defect this issue reported:

was {}: a hardcoded theorem_matrix_ok leaves this null while passed stays true

The commentary at 6280-6296 documents the restoration in place.

Part 2 — validate_lean_standalone_ok: STILL LIVE

Unchanged. The variable still has exactly two mentions and no success point:

6100:    let mut validate_lean_standalone_ok = false;
6456:        && (!validate_lean_standalone || validate_lean_standalone_ok)

report["validate_lean_standalone"] is written zero times in the file — I grepped the whole of fpga.rs for it. So the key still keeps the null from its initializer while the conjunct forces passed to false whenever --validate-lean-standalone is passed.

Both guards are still masked exactly as this issue described, and the masking is structural rather than incidental: no workflow in .github/workflows/ installs a Lean toolchain. Grepping all 42 workflows for lake, elan and leanprover returns nothing, so lake --version fails on every runner and both tests take the early return at fpga.rs:10348 and 10446.

Confirming the mechanic decisively — the skip guard copied out of test_smoke_gate_json_synthetic_validate_lean_standalone (10343-10350) into a file with no production logic, with an unconditional panic!() placed immediately after the return to show the assertions are never reached:

running 1 test
SKIP: lake not on PATH
test test_smoke_gate_json_synthetic_validate_lean_standalone ... ok

test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s

The panic! never fires. So the two ok lines in this issue's body are, as it says, skips — and they will stay skips until a runner has lake, which today none does.

That makes the remaining work: restore the phase body (as this issue notes, there is no success point to mirror, so it has to be written), and decide whether the tests should install lake in CI or assert the skip is impossible — otherwise the restored phase gets the same silent-green coverage the current one has.

No code changed in this pass; verification only.

[gHashTag]

Correction to this issue's own provenance advice, measured on origin/master
6dcefd044c276c0453f7ce2c7206718d480052e5.

The advice to recover the phase body "from the #2228 parent commit" leads to a
dead end. At fc4f468f3c185f25c7259dc75ddcc2f21544751a — the last commit on
master before #2228 — cli/tri/src/fpga.rs already has exactly two mentions of
validate_lean_standalone_ok and no body:

5924:    let mut validate_lean_standalone_ok = false;
6055:        && (!validate_lean_standalone || validate_lean_standalone_ok)

The body was gone before #2228 touched the file. Anyone following the advice
fetches that blob, finds nothing, and concludes the phase was never written.

It was written. It is at a002243a51c946c9a82a7b83bd2616814b5e28eb (Wave Loop
448, "standalone Lean smoke gate"), with four mentions — two success points,
meaning a generate path and a replay path:

6228:    let mut validate_lean_standalone_ok = false;
6613:                    validate_lean_standalone_ok = true;
6743:                    validate_lean_standalone_ok = true;
6823:        && (!validate_lean_standalone || validate_lean_standalone_ok)

Same shape at 8eb0caf5c86681d605aed7f5bc273686ba4357eb (W450), at
6234/6631/6764/6844. Absent at ad503c130ccb75fcad1f5a6bde9905594ad44f05 (W447),
so W448 introduced it. The drop happened between W450 and fc4f468f; not pinned
further.

Framing, so this is not mis-scoped: this half fails closed, not open.
Passing --validate-lean-standalone can only ever produce passed: false. It is a
flag that cannot be earned — a different and less urgent defect than the hardcoded
true that #2343 repaired next door, and it must not be "fixed" by assigning
true.

Blocker, filed separately: lake is installed by no workflow, so the restored
phase could not execute in CI even once. See the linked issue.