diff --git a/verification/GEN-MODEL.sha256 b/verification/GEN-MODEL.sha256 index ebb16ce..a3b1f18 100644 --- a/verification/GEN-MODEL.sha256 +++ b/verification/GEN-MODEL.sha256 @@ -1,4 +1,4 @@ -7f173f9ead5b88f2b5444130d906d7b4a3c1c44f960845ad236c9aab796e2c82 CurveField/FunsExternal.lean +69e5aa74675faafdf18702d87780f5b85b0dcffcaf0652d3a01348e3708f5075 CurveField/FunsExternal.lean e0aa7f126fe8e4a2dd4ef083f076192a2db98dc4e723f69cf204c3019a87f7c4 CurveField/FunsExternal_Template.lean 6aebc152991c3b82fd2b7b576d59ab1524d8ff3e9002264dc84a74b379b3ba74 CurveField/Funs.lean 127b84e0aff8b079f4d74b4f5e898b7f031f740b836a22519069cee99a3e5f2a CurveField/TypesExternal.lean diff --git a/verification/HARNESS.sha256 b/verification/HARNESS.sha256 index 4fb93b6..107efe2 100644 --- a/verification/HARNESS.sha256 +++ b/verification/HARNESS.sha256 @@ -2,14 +2,14 @@ 6b25b7e261633f4fa703de0be1dfd3c263d043107e3b3225d4c5079a93b6a64d check-scalar.sh b55a405e1af95d28a6d222f4cfc1d1e33428da2650b7a6668ecdda852eea6330 check.sh fdd1337f1f44fa73fdb14e6cda001e4e7358513b9c178c517456b24511d96a8e extract.sh -52afbe130c5551686f45643a35065729fd5bb8166b5fa3db67b74c60ba3eff62 GEN-MODEL.sha256 +5a5fd8a0e1d29033e00b98fd0d37b860a3754205d7a46d2c5168d68c26b3dc25 GEN-MODEL.sha256 6033c86eb08b4c2ea0bd7cdbd2cfb5748059179ece3efa9673270dc17a2e38b9 inventory-allowlist-scalar.txt 80cdd232c9a0f3078b2b712957e34797add5421b51bd695a151bf64a7855687a inventory-allowlist.txt 0bb01bc4abaafa8537d460682004d1f336980b28bc4fe1968bcc9c3bc3bc71ba inventory_gate.sh 736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard b982bd1aa56b0648b10516985a2e0f6a9cacff4e1d19b441dadc5b35d69ec732 lift-guard.sh -7a9c89cf2b96313bd4bcddb534e8d06724bd7250234e670baadf6a9b0d1fbf81 model-correspondence.py -6c1503880f38e4b827df32a4854902b66b7b2ea4783f9eb5c44e691a2c293ae1 MODEL-CORRESPONDENCE.txt +1942177f13d6ae229d87a3b0b33f7fbb4b2ae20fe1059cc83010e73f6a156427 model-correspondence.py +cf86c955dd5b637bc9d673c4222684979f507a4e11e488ab514e654c49f4e569 MODEL-CORRESPONDENCE.txt 34c102ca7a38719ef8890b8dedd3f07c3f92e10ae4a1ce2c47a7db4d53523354 Proofs/Audit.lean dd957bb260df0bd33266418a6594b45720c4754c5687bfab4ecb30ad573a286c Proofs/InventoryBasic.lean 859dcb7fcef13e8b49a8b36a496f46e9fc56448410d3bde16c78361215f4bc19 Proofs/InventoryCore.lean diff --git a/verification/MODEL-CORRESPONDENCE.txt b/verification/MODEL-CORRESPONDENCE.txt index fa28eb0..f9f7288 100644 --- a/verification/MODEL-CORRESPONDENCE.txt +++ b/verification/MODEL-CORRESPONDENCE.txt @@ -44,9 +44,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.vartime_double_base.spec_avx2.mul|EXTRA -CurveField/FunsExternal|backend.vector.scalar_mul.vartime_triple_base.spec_avx2.mul_128_128_256_prechecked|EXTRA CurveField/TypesExternal|ed25519.Signature|MODEL CurveField/TypesExternal|subtle.Choice|MODEL -CORRESPONDENCE-COUNT|51 +CORRESPONDENCE-COUNT|48 diff --git a/verification/gen/CurveField/FunsExternal.lean b/verification/gen/CurveField/FunsExternal.lean index 92acab7..ca48a96 100644 --- a/verification/gen/CurveField/FunsExternal.lean +++ b/verification/gen/CurveField/FunsExternal.lean @@ -342,28 +342,6 @@ axiom backend.serial.scalar_mul.vartime_triple_base.mul_128_128_256_prechecked scalar.Scalar → edwards.EdwardsPoint → scalar.Scalar → edwards.EdwardsPoint → scalar.Scalar → Result edwards.EdwardsPoint -/-- [curve25519::backend::vector::scalar_mul::variable_base::spec_avx2::mul]: - Source: 'curve25519/solana-ed25519/src/backend/vector/scalar_mul/variable_base.rs', lines 3:0-3:68 - Visibility: public -/ -axiom backend.vector.scalar_mul.variable_base.spec_avx2.mul - : edwards.EdwardsPoint → scalar.Scalar → Result edwards.EdwardsPoint - -/-- [curve25519::backend::vector::scalar_mul::vartime_double_base::spec_avx2::mul]: - Source: 'curve25519/solana-ed25519/src/backend/vector/scalar_mul/vartime_double_base.rs', lines 14:0-14:68 - Visibility: public -/ -axiom backend.vector.scalar_mul.vartime_double_base.spec_avx2.mul - : - scalar.Scalar → edwards.EdwardsPoint → scalar.Scalar → Result - edwards.EdwardsPoint - -/-- [curve25519::backend::vector::scalar_mul::vartime_triple_base::spec_avx2::mul_128_128_256_prechecked]: - Source: 'curve25519/solana-ed25519/src/backend/vector/scalar_mul/vartime_triple_base.rs', lines 10:0-10:68 -/ -axiom - backend.vector.scalar_mul.vartime_triple_base.spec_avx2.mul_128_128_256_prechecked - : - scalar.Scalar → edwards.EdwardsPoint → scalar.Scalar → - edwards.EdwardsPoint → scalar.Scalar → Result edwards.EdwardsPoint - /-- [curve25519::backend::scalar_fits_in_128_bits]: Source: 'curve25519/solana-ed25519/src/backend.rs', lines 283:0-285:1 -/ axiom backend.scalar_fits_in_128_bits : scalar.Scalar → Result Bool 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