mirror of
https://github.com/saymrwulf/dalek-ed25519-verified.git
synced 2026-09-03 20:13:48 +00:00
mrwulf
dd10ba26a0
Phase 2c exists because a source-regex enumerator proved evadable in ltl-accumulator-verified: attributed, private and `instance` declarations and a nested-namespace basename collision all slipped past it. The fix was to stop reading source text and ask the Lean environment, and that fix was ported here. But a fix ported is not a fix tested. selftest-inventory.sh proves the GATE reacts to a difference; it feeds synthetic observations and never runs the walker. Nothing here had ever asked whether the WALKER SEES a declaration written in an evasive shape. selftest-shapes.sh adds all four shapes to an audited module, recompiles it, runs the real Phase 2c, and requires each one to be NAMED in the UNCLASSIFIED list. Asserting that the gate merely failed would not do: one shape surfacing fails the run while the other three ride along unseen. All four forks report all four. Negative-tested by removing the injection — the run then reports the walker blind and fails. The victim module is derived from each repo's own manifest, not named: the forks do not share a corpus (dalek/anza attack Proofs.Basic, risc0/betrusted Proofs.DecompressMain), and a hard-coded name would have silently found nothing on half of them. It must be manifested, must not be an inventory or audit driver, and must be imported by no other manifest module. Two notes for whoever edits this next. When re-deriving a leaf module, the inventory drivers must be excluded from the set of IMPORTERS as well as from the candidates: they import the whole corpus, so leaving them in makes every module look imported, finds no leaf, and the test silently has no victim at all. And a lift of Phase 2c needs SCALAR_SH/SCALAR_MANIFEST alongside PROOFS, or the coverage check dies on an unbound variable. New executable pinned in HARNESS.sha256. Certified by a full sweep: both buttons, all four forks, purged trees, machine otherwise idle. 8/8 green. |
||
|---|---|---|
| .. | ||
| gen | ||
| Proofs | ||
| AUDIT-MANIFEST.txt | ||
| check-scalar.sh | ||
| check.sh | ||
| CurveField.llbc | ||
| CurveSig.llbc | ||
| extract.sh | ||
| GEN-MODEL.sha256 | ||
| HARNESS.sha256 | ||
| inventory-allowlist-scalar.txt | ||
| inventory-allowlist.txt | ||
| inventory_gate.sh | ||
| lean-guard | ||
| selftest-auditonly.sh | ||
| selftest-axgate.sh | ||
| selftest-harness.sh | ||
| selftest-inventory.sh | ||
| selftest-shapes.sh | ||
| selftest-statements.sh | ||
| selftest-tiers.sh | ||