mirror of
https://github.com/saymrwulf/anza-ed25519-verified.git
synced 2026-09-04 20:24:06 +00:00
mrwulf
15101f32bd
THE GAP. The capability matrix in the control repo — built after the author
answered a capability question by grepping for a FILENAME rather than for the
property, three times in one session — asked whether each repository's auditor
enumerates itself. The four ed25519 forks answered no. Following that up found
something larger: `Proofs/Audit.lean`, the statement-binding driver from P1-a,
is compiled, is a member of the manifest, and was enumerated by NOTHING. The
kernel counted 3058 declarations where the inventory accounted for 3022, and
26 of the 36 missing were its.
THE PROPERTY, now enforced: every constant the kernel sees under this button's
manifest must appear, BY NAME, in either the corpus inventory or the
instruments' own surface. `emitDrivers` in InventoryCore walks the audit
modules and fails closed on an axiom (which would widen the trusted base
outside every cone) or on a standalone claim (which no certificate covers and
no allowlist pins), while admitting the obligations the elaborator generates
for a definition declared alongside it.
TWO WRONG FORMULATIONS FIRST, both recorded because the second is instructive:
· `kernel = corpus + instruments + N_DRIVERS`, where the last term was
justified as a per-driver "self-observation blind spot". It fitted dalek
and anza (2 drivers, residual 2) and broke on risc0 and betrusted
(1 driver, residual 2). The residual is 2 everywhere and has nothing to do
with drivers. This was curve-fitting from a sample of one, and it was named
as the highest-risk claim in the round-7 self-assessment BEFORE the data
refuted it.
· distinct-by-name counting, which collapses `CurveFieldProofs.zero_spec` —
a name that genuinely denotes two different declarations, in Proofs.Basic
and Proofs.ConstSpecs, walked by two drivers with separate environments.
THE MEASURED CAUSE of the residual. Lean materialises equation lemmas lazily,
when something forces an unfold, and each module that forces one gets its own
copy in its object file. `CurveFieldProofs.denote.eq_1` sits in both
SubNegSpec.olean and ConstSpecs.olean; `CurveFieldProofs.limbsVal.eq_1` in both
ReduceSpec.olean and ConstSpecs.olean. The kernel gate reads object files and
counts both copies; the environment holds one constant per name. Counts cannot
relate those two views in either direction — so the check compares SETS, which
is the idiom the rest of this estate already uses, and no constant remains that
could be widened to make a red run green.
Negative-tested: with the instrument walk disabled, the check names
Proofs.Audit's declarations as unaccounted.
ANZA also lacked one allowlist row, `subtle.Choice...from.eq_1`, the same
lazy-materialisation effect seen from the other side. Verified rather than
assumed before adding it: the parent is declared in gen/CurveField/
FunsExternal.lean — the model, pinned by bytes and not inventoried by
declaration — the lemma materialised in Proofs.CompressSpec which forced the
unfold, and all three other forks carry the lemma row while none carries the
parent.
CONSEQUENCE WORTH DISCLOSING: the audited declaration surface is not purely a
function of the corpus source. It depends on which proofs forced which
unfolds. This is now a known gap in the round-7 kit.
Also corrected here: Proofs/Inventory.lean's header claimed the audit drivers
were excluded from the compile manifest. They are lines 42-44 of PROOFS.
Certified by a full sweep: both buttons, all four forks, purged trees. 8/8.
24 lines
2 KiB
Text
24 lines
2 KiB
Text
12dc724bffd590e6f706573d97bf07425b8f268a1be2d72a3bbd9aef48f9c277 AUDIT-MANIFEST.txt
|
|
6b25b7e261633f4fa703de0be1dfd3c263d043107e3b3225d4c5079a93b6a64d check-scalar.sh
|
|
5f1611459785a8c261007f9234606aaac4f8ba6e0fe37e74b0c7d14cb7eabbbd check.sh
|
|
fdd1337f1f44fa73fdb14e6cda001e4e7358513b9c178c517456b24511d96a8e extract.sh
|
|
52afbe130c5551686f45643a35065729fd5bb8166b5fa3db67b74c60ba3eff62 GEN-MODEL.sha256
|
|
6033c86eb08b4c2ea0bd7cdbd2cfb5748059179ece3efa9673270dc17a2e38b9 inventory-allowlist-scalar.txt
|
|
80cdd232c9a0f3078b2b712957e34797add5421b51bd695a151bf64a7855687a inventory-allowlist.txt
|
|
0bb01bc4abaafa8537d460682004d1f336980b28bc4fe1968bcc9c3bc3bc71ba inventory_gate.sh
|
|
736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard
|
|
fde2e987a9f69cb9f39b18ab8b405d73db4d9abee9f714f8be993a40ef617c03 model-correspondence.py
|
|
a8e2fa50e6f14278e9d088eb6339debc846419df297b0cdb2b9fbb77294545bd MODEL-CORRESPONDENCE.txt
|
|
34c102ca7a38719ef8890b8dedd3f07c3f92e10ae4a1ce2c47a7db4d53523354 Proofs/Audit.lean
|
|
dd957bb260df0bd33266418a6594b45720c4754c5687bfab4ecb30ad573a286c Proofs/InventoryBasic.lean
|
|
859dcb7fcef13e8b49a8b36a496f46e9fc56448410d3bde16c78361215f4bc19 Proofs/InventoryCore.lean
|
|
660d35343f5673d4bc854787b6a34063c956567bd7e2eb62955a92e3c55bfa6b Proofs/Inventory.lean
|
|
6fbeb50d3951c7c5ac593f6dec91096fc798123ed0c500fdfa39fb20b118ea78 Proofs/InventoryScalar.lean
|
|
bf71e8d4eb312ebc687bf7e218d90b910543cd92e782078174868d012aca7250 selftest-auditonly.sh
|
|
eb81df6d154b413b243ad282e3b1bfec92fde158a215f89993c08586a121f171 selftest-axgate.sh
|
|
73d629325b667e715c7e6a633332950ace019e18e6d143ec5cb25846b8ddeb80 selftest-correspondence.sh
|
|
3d5898161d663eccad162269a5a6c102319077e22e1f2d89a8bfcab6926d29f6 selftest-harness.sh
|
|
1df031a075fc438c5229d01cbc44ee6ac489a272cd736624f7ca45ef1a4ddb7f selftest-inventory.sh
|
|
26f10a749e03cecd7ad173d0d621498386444d8e347f606a99a2fadb06738d86 selftest-shapes.sh
|
|
2c591fb2a0cc50cfdf76c3328e5d72d52b69c02f5b230ebc55c977d6570ecc0f selftest-statements.sh
|
|
df2389909839c5c2275097044b112bd254e48aa21b4b8f6c1430847c0a0c7cc6 selftest-tiers.sh
|