formal: repetition witnesses, and four defects in the instruments themselves (Props. 57-58) #2034

Planned: repetition witnesses (Prop. 57)

Prop. 56 closed interleaving reachability for dma_controller and weight_prefetch_ctrl and stated the rest of its scope: the other three modules had witnesses for concurrency but none for repetition.

14 witnesses now gate, up from 11. Every module is probed for all three shapes: happens / overlaps / repeats. Each was validated by a constraint that removes exactly what it probes and makes it prove.

Found instead: four defects in the instruments (Prop. 58)

w_ls_two_layers first reported PROVES — "two layer runs are unreachable", which reads as a restart defect, and I went and read the sequencer looking for one. Yosys had actually printed proof did fail.

1. A shell flipped a verdict. Yosys prints signal names backslash-prefixed; layer_sequencer has chunk_id; a shell whose echo expands escapes reads \c as stop output here. A 31 966-byte trace became 4 893 bytes and the verdict line was gone. bash does not expand these, zsh does — so the same command gives different answers on CI and on a developer's machine, in exactly the direction the docs invite by printing reproduction commands. Fixed with printf '%s\n'.
2. The mutation harness scored a crash as a kill. yos() returned returncode == 0 and every caller read its negation as refuted, so a mutation that makes the RTL unparseable was counted as a killed mutant — never tested, reported as evidence the gate bites. Validated by extracting the shipped yos() out of the workflow YAML and running it on a proving script, a refuting script, and an unparseable mutant.
3. The free-property scan passed while scanning nothing. identity_scan.py globbed relative to the caller's cwd; run from anywhere but the repo root it printed "scanned 0 assertion bodies in 0 files" and exited 0.
4. The documentation gate was never wired up. README.md has claimed "a documentation gate covering all N propositions" for many waves. Nothing in .github/ or formal/ implemented it — it was a habit, a script pasted into a terminal. It now ships as formal/doc_gate.py and was mutation-tested against four ways of breaking the document before being believed.

All four share one shape: an absence read as a pass. No output, no verdict, no gate — each was silence, and silence scored green.

Nine RTL defects were found by these harnesses. An instrument that has been right nine times is not thereby verified.

User Scenarios

• Given the formal verification suite has 11 witnesses gating concurrency properties, when Prop. 57 adds repetition witnesses for interrupt_controller, axi_lite_slave, and layer_sequencer, then 14 witnesses gate covering happens/overlaps/repeats for all modules.
• Given the yos() harness in the workflow YAML treats a Yosys crash (returncode 0) as a killed mutant, when a mutation makes RTL unparseable, then the harness must not count it as a kill.
• Given identity_scan.py runs from a non-root directory and scans 0 files, when it exits 0, then the scan must fail instead of passing silently.

Requirements

• FR-001: The repetition witnesses w_irq_serviced_twice, w_axi_two_writes, w_ls_two_layers MUST be added to the formal spec and validated by constraint removal.
• FR-002: The shell command that captures Yosys trace output MUST use printf '%s\n' to prevent backslash-escape expansion (e.g., \c in chunk_id).
• FR-003: The yos() harness MUST distinguish Yosys crashes (parse errors) from proof results and MUST NOT score a crash as a killed mutant.
• FR-004: identity_scan.py MUST resolve assertion-file globs relative to the repository root and MUST exit non-zero when zero files are scanned.
• FR-005: The documentation gate formal/doc_gate.py MUST be integrated into CI so that README.md's claim of a "documentation gate covering all N propositions" is enforced automatically.

Success Criteria

• t27c specs/fpga/formal.t27 compiles and t27c specs/igla/race/formal.t27 compiles — both exit 0.
• make formal (or the CI command that runs the 14 witnesses) completes with 14 witnesses reported — exit 0.
• Running the mutation harness on an unparseable RTL mutant yields "survived" not "killed" — exit 0 with correct classification.
• Running python formal/identity_scan.py from a subdirectory exits non-zero and prints an error — exit 1.
• Running python formal/doc_gate.py against README.md with a missing proposition reference fails — exit 1.
• The .trinity/seals/Formal.json seal is updated to reflect 14 witnesses — file exists and contains updated count.

Boundary

• README.md
• specs/fpga/formal.t27
• specs/igla/race/formal.t27
• specs/fpga/formal.v
• .trinity/seals/Formal.json
• specs/igla/race/formal.zig