From 2568e9741010062942583035c47c1e7b0da56d5e Mon Sep 17 00:00:00 2001 From: mrwulf Date: Sun, 2 Aug 2026 21:29:54 +0200 Subject: [PATCH] correspondence: a named section is not a namespace; an extra axiom is a failure MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Round-8 review (GPT-5.6, register key `section-prefix-bug`, CRITICAL). Reproduced here exactly before fixing. model-correspondence.py treated `namespace`, `section` and `end` as one event class and pushed a named section onto the fully-qualified-name prefix. Lean does not: `section Foo` opens a scope for `variable`/`open` and gives `end Foo` a label; it does not turn `bar` into `Foo.bar`. Given a template reading section Foo axiom bar : Nat end Foo the scanner reported `Foo.bar`, `--names` handed Phase 2d only `Foo.bar`, Lean resolved an unrelated `Foo.bar` definition elsewhere in the corpus, and the verdict came back PROVEN. The axiom the extraction ACTUALLY depends on was never queried. This survived both the fail-closed rewrite and the new Lean-semantic phase, in a scanner rewritten that same week specifically to stop dropping things. AND THE REASON IT STAYED SILENT, which is the half worth keeping. The real external did not vanish — it landed in the table as EXTRA, the one verdict that could not fail. A silent bucket beside a fail-closed parser is a slower way of dropping things. An extra AXIOM is now EXTRA-AXIOM and stops the button: the model exists to answer the template, so an assumption nothing asks for is either a parse we got wrong or an assumption nobody governs. Extra definitions stay tolerated; helpers in a model file are ordinary. That gate fired on the real corpora on its first run. Each fork's hand-maintained gen/CurveField/FunsExternal.lean carried AVX2/AVX512 backend axioms present in no template, no proof, no cone and no allowlist — dead assumptions in a pinned trusted-base file, reported as EXTRA and therefore invisible. extract.sh:16 confirms these files are never overwritten by extraction, so they were hand-written and are removed here: dalek 2, anza 3, risc0 4, betrusted 4 Nothing referenced them, so no certificate's cone changes; the trusted base simply gets smaller. Table rows 64->62, 51->48, 57->53, 56->52, and Phase 2d independently resolved 62/48/53/52 externals against the regenerated tables. GEN-MODEL.sha256 and HARNESS.sha256 both move: the model bytes changed, and the harness pins the table and the gen manifest themselves. Certified: round-10 sweep, 2h53m, ten instruments in each of four forks, 40/40 GREEN, 0 failing, 0 resource-limited. A full run was required — the --audit-only staleness gate correctly refused after a source change. Registered in formal-verification-control/review-findings.tsv as `section-prefix-bug` and `dead-model-axioms`. Co-Authored-By: Claude Opus 4.8 --- verification/GEN-MODEL.sha256 | 2 +- verification/HARNESS.sha256 | 6 +- verification/MODEL-CORRESPONDENCE.txt | 6 +- verification/gen/CurveField/FunsExternal.lean | 29 --------- verification/model-correspondence.py | 61 ++++++++++++++++--- 5 files changed, 58 insertions(+), 46 deletions(-) diff --git a/verification/GEN-MODEL.sha256 b/verification/GEN-MODEL.sha256 index 86f83a5..d4b3a30 100644 --- a/verification/GEN-MODEL.sha256 +++ b/verification/GEN-MODEL.sha256 @@ -1,4 +1,4 @@ -cf0761191d3f69794c9d74884dc9d93a3e7958cb0d8d5ef378b9bdf1f14e893f CurveField/FunsExternal.lean +37eb720775a1151630434eb24db92b232d3391c4415c128c34317fc124c31a6e CurveField/FunsExternal.lean 85c6056c35d4d02bbd56ce51e3b448c759d302000a7ecbc4074a218990459ea1 CurveField/FunsExternal_Template.lean cd49ea057b48b78294b2ca857575738af60d5cdd68506146411a83251c6c4648 CurveField/Funs.lean d197d7b9fe515863784eeee59a2fbb69735d10ebcf5cc4e03feb3afbeb53a2b7 CurveField/TypesExternal.lean diff --git a/verification/HARNESS.sha256 b/verification/HARNESS.sha256 index 9b037d0..1b9eb42 100644 --- a/verification/HARNESS.sha256 +++ b/verification/HARNESS.sha256 @@ -2,14 +2,14 @@ d505e4dd9283673e78fb34e25780c94334e03de4ad20400f8289d594ab004daf check-scalar.sh 9b0fa638179282b4dd74a6aad3d140ad1299b4e092d1f19dc337832c172947e3 check.sh 71244d824847311bcb3ba8ad1f1905c4b24fe8f015e3230969914019cb628b61 extract.sh -c9672a28825cd1d4055fb9efbb4a1d94c921c7b5c79e4cd5d0626ba061e554c1 GEN-MODEL.sha256 +3898670a2cb3db74d7381372a09649f6518e49384adc935d73bd6be7f825f7b9 GEN-MODEL.sha256 e6f31b4303f5a344781d353f1dddefc185876df470e27b285c81556621e65c05 inventory-allowlist-scalar.txt 86ee83b703d17c1f04af654657219b344b0076bc994c0b791ca6b6c5a0090d4f inventory-allowlist.txt 0bb01bc4abaafa8537d460682004d1f336980b28bc4fe1968bcc9c3bc3bc71ba inventory_gate.sh 736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard b982bd1aa56b0648b10516985a2e0f6a9cacff4e1d19b441dadc5b35d69ec732 lift-guard.sh -7a9c89cf2b96313bd4bcddb534e8d06724bd7250234e670baadf6a9b0d1fbf81 model-correspondence.py -1ba5ff18b170e3139e10805c221b03188ca8c2a433ee807d7139b3afb9df2437 MODEL-CORRESPONDENCE.txt +1942177f13d6ae229d87a3b0b33f7fbb4b2ae20fe1059cc83010e73f6a156427 model-correspondence.py +77e356f607c01ff597193f28f60b48a701ca2b9597cc9a991ac5b27b00aeaf81 MODEL-CORRESPONDENCE.txt 772ca6dd22443c83dc35d5428598c8d17a01c69db5be008474d06476fa66f7f8 Proofs/Audit.lean 859dcb7fcef13e8b49a8b36a496f46e9fc56448410d3bde16c78361215f4bc19 Proofs/InventoryCore.lean 660d35343f5673d4bc854787b6a34063c956567bd7e2eb62955a92e3c55bfa6b Proofs/Inventory.lean diff --git a/verification/MODEL-CORRESPONDENCE.txt b/verification/MODEL-CORRESPONDENCE.txt index dcdcdca..ebf8599 100644 --- a/verification/MODEL-CORRESPONDENCE.txt +++ b/verification/MODEL-CORRESPONDENCE.txt @@ -32,10 +32,6 @@ CurveField/FunsExternal|subtle.Choice.Insts.CoreOpsBitBitOrChoiceChoice.bitor|MO CurveField/FunsExternal|subtle.Choice.unwrap_u8|MODEL CurveField/FunsExternal|subtle.ConditionallySelectable.conditional_assign.default|MODEL CurveField/FunsExternal|subtle.ConditionallySelectable.conditional_swap.default|MODEL -CurveField/FunsExternal|backend.vector.scalar_mul.variable_base.spec_avx2.mul|EXTRA -CurveField/FunsExternal|backend.vector.scalar_mul.variable_base.spec_avx512ifma_avx512vl.mul|EXTRA -CurveField/FunsExternal|backend.vector.scalar_mul.vartime_double_base.spec_avx2.mul|EXTRA -CurveField/FunsExternal|backend.vector.scalar_mul.vartime_double_base.spec_avx512ifma_avx512vl.mul|EXTRA CurveField/TypesExternal|subtle.Choice|MODEL CurveSig/FunsExternal|core.result.Result.Insts.CoreOpsTry_traitFromResidualResultInfallibleE.from_residual|MODEL CurveSig/FunsExternal|core.result.Result.Insts.CoreOpsTry_traitTry.branch|MODEL @@ -54,4 +50,4 @@ CurveSig/TypesExternal|curve25519_dalek.edwards.EdwardsPoint|PROVEN CurveSig/TypesExternal|curve25519_dalek.scalar.Scalar|PROVEN CurveSig/TypesExternal|ed25519.Signature|MODEL CurveSig/TypesExternal|signature.error.Error|MODEL -CORRESPONDENCE-COUNT|56 +CORRESPONDENCE-COUNT|52 diff --git a/verification/gen/CurveField/FunsExternal.lean b/verification/gen/CurveField/FunsExternal.lean index 207b5ba..7906d50 100644 --- a/verification/gen/CurveField/FunsExternal.lean +++ b/verification/gen/CurveField/FunsExternal.lean @@ -301,40 +301,11 @@ def U64.Insts.SubtleConditionallySelectable.conditional_swap def backend.get_selected_backend : Result backend.BackendKind := ok backend.BackendKind.Serial -/-- [curve25519_dalek::backend::vector::scalar_mul::variable_base::spec_avx512ifma_avx512vl::mul]: - Source: 'curve25519-dalek/src/backend/vector/scalar_mul/variable_base.rs', lines 3:0-6:2 - Visibility: public -/ -axiom backend.vector.scalar_mul.variable_base.spec_avx512ifma_avx512vl.mul - : edwards.EdwardsPoint → scalar.Scalar → Result edwards.EdwardsPoint - -/-- [curve25519_dalek::backend::vector::scalar_mul::variable_base::spec_avx2::mul]: - Source: 'curve25519-dalek/src/backend/vector/scalar_mul/variable_base.rs', lines 3:0-6:2 - Visibility: public -/ -axiom backend.vector.scalar_mul.variable_base.spec_avx2.mul - : edwards.EdwardsPoint → scalar.Scalar → Result edwards.EdwardsPoint - /-- [curve25519_dalek::backend::serial::scalar_mul::variable_base::mul]: Source: 'curve25519-dalek/src/backend/serial/scalar_mul/variable_base.rs', lines 11:0-48:1 -/ axiom backend.serial.scalar_mul.variable_base.mul : edwards.EdwardsPoint → scalar.Scalar → Result edwards.EdwardsPoint -/-- [curve25519_dalek::backend::vector::scalar_mul::vartime_double_base::spec_avx512ifma_avx512vl::mul]: - Source: 'curve25519-dalek/src/backend/vector/scalar_mul/vartime_double_base.rs', lines 14:0-17:2 - Visibility: public -/ -axiom - backend.vector.scalar_mul.vartime_double_base.spec_avx512ifma_avx512vl.mul - : - scalar.Scalar → edwards.EdwardsPoint → scalar.Scalar → Result - edwards.EdwardsPoint - -/-- [curve25519_dalek::backend::vector::scalar_mul::vartime_double_base::spec_avx2::mul]: - Source: 'curve25519-dalek/src/backend/vector/scalar_mul/vartime_double_base.rs', lines 14:0-17:2 - Visibility: public -/ -axiom backend.vector.scalar_mul.vartime_double_base.spec_avx2.mul - : - scalar.Scalar → edwards.EdwardsPoint → scalar.Scalar → Result - edwards.EdwardsPoint - /-- [curve25519_dalek::backend::serial::curve_models::{impl subtle::ConditionallySelectable for curve25519_dalek::backend::serial::curve_models::ProjectiveNielsPoint}::conditional_swap]: Source: 'curve25519-dalek/src/backend/serial/curve_models/mod.rs', lines 295:0-311:1 Visibility: public -/ diff --git a/verification/model-correspondence.py b/verification/model-correspondence.py index c8d987c..ba9f810 100755 --- a/verification/model-correspondence.py +++ b/verification/model-correspondence.py @@ -121,7 +121,11 @@ def strip_comments(text): def declared(path): - """Fully-qualified names declared in one file. + """{fully-qualified name: declaration keyword} for one file. + + Returns a MAPPING, not a set, because the keyword is load-bearing: an + `axiom` the template never asks for must stop the button, while an extra + `def` is an ordinary helper. Callers that only need names take `set(...)`. Raises ScanError on any declaration keyword whose name cannot be read. """ @@ -131,7 +135,7 @@ def declared(path): # Scope events by offset, so each declaration can be placed in its stack. events = [(m.start(), m.group(1), m.group(2)) for m in NS.finditer(text)] - names = set() + names = {} for m in KW.finditer(text): im = IDENT.match(text, m.end()) if not im: @@ -144,12 +148,31 @@ def declared(path): for off, kind, arg in events: if off > m.start(): break - if kind in ('namespace', 'section'): + if kind == 'namespace': stack.append(arg) + elif kind == 'section': + # A NAMED SECTION DOES NOT QUALIFY DECLARATION NAMES. `section + # Foo` opens a scope for `variable`/`open` and gives `end Foo` a + # label to match; it does not make `bar` into `Foo.bar`. This + # line pushed `arg`, so a template reading + # section Foo + # axiom bar : Nat + # end Foo + # was reported as declaring `Foo.bar`. Round-8 review (GPT-5.6, + # register key `section-prefix-bug`) showed the consequence: + # `--names` handed Phase 2d only `Foo.bar`, Lean happily + # resolved an unrelated `Foo.bar` definition elsewhere in the + # corpus and returned PROVEN, and the axiom the extraction + # ACTUALLY depends on was never queried at all. The scanner had + # been rewritten that same week specifically to be fail-closed. + # None appends a frame so `end` still balances, and the + # comprehension below drops it from the prefix. + stack.append(None) elif stack: stack.pop() prefix = [p for p in stack if p] - names.add('.'.join(prefix + [im.group(1)]) if prefix else im.group(1)) + full = '.'.join(prefix + [im.group(1)]) if prefix else im.group(1) + names.setdefault(full, m.group(1)) return names @@ -163,14 +186,15 @@ def main(root): for f in sorted(glob.glob(os.path.join(gen, '*', '*.lean'))): if f in models or f.endswith('_Template.lean'): continue - corpus |= declared(f) + corpus.update(declared(f)) rows, unresolved = [], [] for t in templates: model = t.replace('_Template', '') rel = os.path.relpath(t, gen).replace('_Template.lean', '') - tnames = declared(t) - mnames = declared(model) if os.path.exists(model) else set() + tnames = set(declared(t)) + mkinds = declared(model) if os.path.exists(model) else {} + mnames = set(mkinds) for n in sorted(tnames): if n in mnames: rows.append(f'{rel}|{n}|MODEL') @@ -179,8 +203,29 @@ def main(root): else: rows.append(f'{rel}|{n}|UNRESOLVED') unresolved.append(f'{rel}|{n}') + # AN EXTRA AXIOM IS A FAILURE, and this is the second half of the + # round-8 section-prefix finding. EXTRA was the one verdict that could + # not fail: the model declares something the template did not ask for. + # When the scanner mis-derived the template's name (`Foo.bar` instead of + # `bar`), the axiom the extraction ACTUALLY depends on did not vanish — + # it landed here, as a harmless-looking EXTRA row, while the invented + # name was certified PROVEN. A silent bucket next to a fail-closed + # parser is just a slower way of dropping things. + # + # There is no benign reading of an extra AXIOM either way. The model + # exists to answer the template; an assumption nothing asks for is + # either a parse the scanner got wrong or an unaudited assumption + # nobody is governing. Both must stop the button. Extra non-axiom + # declarations stay reportable-but-tolerated: helper definitions in a + # model file are ordinary. for n in sorted(mnames - tnames): - rows.append(f'{rel}|{n}|EXTRA') + kind = mkinds.get(n, '') + if kind == 'axiom': + rows.append(f'{rel}|{n}|EXTRA-AXIOM') + unresolved.append(f'{rel}|{n} (axiom in the model that no ' + f'template external asks for)') + else: + rows.append(f'{rel}|{n}|EXTRA') print('\n'.join(rows)) print(f'CORRESPONDENCE-COUNT|{len(rows)}') return 1 if unresolved else 0