From 63fac018891757f298d64ac7ba906efafc88ad18 Mon Sep 17 00:00:00 2001
From: mrwulf <mrwulf.cleaner@gmail.com>
Date: Sun, 2 Aug 2026 02:24:15 +0200
Subject: [PATCH] Round-7 F1: make model/template correspondence SEMANTIC, and
 fail closed
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

THE DEFECT, as found. GPT-5.6 showed the textual classifier could report
PROVEN for a name Lean resolves to an axiom: a definition appearing only
inside a `/- -/` comment was read as real. Repairing that exposed something
larger and already live. Aeneas wraps long declarations:

    axiom
      curve25519_dalek.edwards.EdwardsPoint.Insts.CoreOpsArithNegEdwardsPoint.neg

The old scanner required keyword and name on one physical line, so it matched
nothing there and SILENTLY DROPPED the declaration — no MODEL row, no PROVEN
row, no failure. Nine to ten externals per fork had no row at all, and the
tier-A/B `neg` was missing from every committed table while the trust
documents claimed that class was machine-checked. Four pinned tables were
wrong, in four repositories, with the buttons green over them. No attacker
was required; Aeneas's own formatting did it.

The lesson is not "write a better regex". The scanner was FAIL-OPEN: input it
could not parse produced silence instead of a stop. A gate that drops what it
cannot read is worse than no gate, because the green covers a gap that is
invisible in the diff.

THE REPAIR, in three layers that each do only what they honestly can.

  · DISCOVERY stays textual, because the template cannot be imported — it
    declares the same names as the model and they would clash. It now strips
    NESTED `/- -/` blocks, reads a name that wraps to a later line, tracks
    namespace/section/end, and FAILS CLOSED: an unparseable keyword exits 2
    naming file and line.
  · Phase 0d keeps the cheap pre-compile comparison against the table.
  · Phase 2d is new and authoritative. After compilation it generates a temp
    Lean driver (the Phase 2b idiom, so no permanent module and no manifest
    churn), imports every non-template gen module, and asks env.find? what
    each external IS: kind and originating module. Model module -> MODEL;
    non-axiom in a generated module -> PROVEN; an axiom outside the model, or
    a name that does not resolve, is a failure. Lean's verdict must equal the
    committed table's, and the answer count must equal the question count so
    a truncated resolver cannot pass.

THE TABLES were regenerated and verified three ways before being committed:
an independently written second scanner agreed on 228/228 rows across the
four forks; all 47 changed rows carry file:line evidence; and the PROVEN row
was put to Lean directly — kind = def, module = CurveField.Funs.

  dalek 54 -> 64 rows   anza 42 -> 51   risc0 48 -> 57   betrusted 47 -> 56

Also corrected: `from_residual` was recorded EXTRA in every fork; the
template does demand it, so it is MODEL. anza carried a spurious `hash|EXTRA`
row from a mis-parse.

NEGATIVE-TESTED. With Phase 0d neutered so Phase 2d was the gate under test,
a PROVEN row edited to MODEL produces:

    SEMANTIC DRIFT: ...neg — table says MODEL, Lean says PROVEN

selftest-correspondence.sh grew 4 cases -> 7: GPT's comment counterexample,
the wrapped declaration that was actually live, and a fail-closed check.

WHAT THIS DOES NOT CLOSE. Phase 2d resolves names in the environment built
from gen/. It establishes what a name IS — assumption or proof, and where —
not that the extraction faithfully represents the Rust. That remains the
Charon/Aeneas trust assumption and no gate here can close it.

Certified: both buttons, all four forks, purged trees. 8/8 green, with
62/48/53/52 externals resolved by Lean and every verdict matching.
---
 .gitignore                              |   1 +
 verification/HARNESS.sha256             |   8 +-
 verification/MODEL-CORRESPONDENCE.txt   |  14 +-
 verification/check.sh                   | 122 ++++++++++++++++
 verification/model-correspondence.py    | 184 +++++++++++++++++++++---
 verification/selftest-correspondence.sh |  43 ++++++
 6 files changed, 344 insertions(+), 28 deletions(-)

diff --git a/.gitignore b/.gitignore
index 1e9659c..1a42d43 100644
--- a/.gitignore
+++ b/.gitignore
@@ -2,3 +2,4 @@
 .lake/
 lake-manifest.json
 .audit-basis
+__pycache__/
diff --git a/verification/HARNESS.sha256 b/verification/HARNESS.sha256
index c54580a..69424f1 100644
--- a/verification/HARNESS.sha256
+++ b/verification/HARNESS.sha256
@@ -1,14 +1,14 @@
 c0cfe800f41ce6c12420afb97ad40330b14a2aaad232077e7579e376c48e2ae4  AUDIT-MANIFEST.txt
 6b25b7e261633f4fa703de0be1dfd3c263d043107e3b3225d4c5079a93b6a64d  check-scalar.sh
-03de9a93e27698714ca90fbe92989296c5847f75f14e60f2eb289e7540ef2d53  check.sh
+5dd0b73ce3692fbc9052d9003ca87550e01dac854c5f9d576ee51b08b22a0d1f  check.sh
 5e582e44dfd210cb5b8e56f6c31907162fc8e1adf7dac7caf3afb435bbaccb53  extract.sh
 d93d7b77831b7db7acc2f88c395526db850219389a967a0873f3d59ee1f64dd4  GEN-MODEL.sha256
 9acc69d66d0c35a88da6d6d020027e5b66ce992763cef3af8de653319abfbb8c  inventory-allowlist-scalar.txt
 8e2950712ce39ace9cffd3bb58a13984832ff7f3f43ba7b68aa2b1eaa2bc2116  inventory-allowlist.txt
 0bb01bc4abaafa8537d460682004d1f336980b28bc4fe1968bcc9c3bc3bc71ba  inventory_gate.sh
 736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce  lean-guard
-fde2e987a9f69cb9f39b18ab8b405d73db4d9abee9f714f8be993a40ef617c03  model-correspondence.py
-2281dfc465954b026ebc3ac20c12d8dbadf307b4e1fecfc2dab11376a825634f  MODEL-CORRESPONDENCE.txt
+7a9c89cf2b96313bd4bcddb534e8d06724bd7250234e670baadf6a9b0d1fbf81  model-correspondence.py
+665cea5463959d5bc80c6549bf899c0450f3e9d597a4ac6acae7f1559325c1e8  MODEL-CORRESPONDENCE.txt
 79a001107928713a22e679e4c4028549df76d0733455bb9937a4f438a0c315c8  Proofs/Audit.lean
 18e0cef25366bdcda67e8e347a222c169469654547b87adb01eb5b12aa9a9529  Proofs/InventoryBasic.lean
 2b4f2bad2c82c64a1d29c873554b1728b86148f0bc27324c6e0b16defda22ca9  Proofs/InventoryCore.lean
@@ -16,7 +16,7 @@ fde2e987a9f69cb9f39b18ab8b405d73db4d9abee9f714f8be993a40ef617c03  model-correspo
 6fbeb50d3951c7c5ac593f6dec91096fc798123ed0c500fdfa39fb20b118ea78  Proofs/InventoryScalar.lean
 bf71e8d4eb312ebc687bf7e218d90b910543cd92e782078174868d012aca7250  selftest-auditonly.sh
 eb81df6d154b413b243ad282e3b1bfec92fde158a215f89993c08586a121f171  selftest-axgate.sh
-73d629325b667e715c7e6a633332950ace019e18e6d143ec5cb25846b8ddeb80  selftest-correspondence.sh
+9bf6559fb364bbfdec94649c459215061df80f1f813b4b0ec869c7f8e18a8cfc  selftest-correspondence.sh
 3d5898161d663eccad162269a5a6c102319077e22e1f2d89a8bfcab6926d29f6  selftest-harness.sh
 1df031a075fc438c5229d01cbc44ee6ac489a272cd736624f7ca45ef1a4ddb7f  selftest-inventory.sh
 26f10a749e03cecd7ad173d0d621498386444d8e347f606a99a2fadb06738d86  selftest-shapes.sh
diff --git a/verification/MODEL-CORRESPONDENCE.txt b/verification/MODEL-CORRESPONDENCE.txt
index b28db44..3839df8 100644
--- a/verification/MODEL-CORRESPONDENCE.txt
+++ b/verification/MODEL-CORRESPONDENCE.txt
@@ -11,18 +11,27 @@ CurveField/FunsExternal|U64.Insts.SubtleConditionallySelectable.conditional_swap
 CurveField/FunsExternal|U8.Insts.CoreHashHash.hash|MODEL
 CurveField/FunsExternal|U8.Insts.SubtleConstantTimeEq.ct_eq|MODEL
 CurveField/FunsExternal|backend.get_selected_backend|MODEL
+CurveField/FunsExternal|backend.serial.curve_models.AffineNielsPoint.Insts.SubtleConditionallySelectable.conditional_swap|MODEL
+CurveField/FunsExternal|backend.serial.curve_models.ProjectiveNielsPoint.Insts.SubtleConditionallySelectable.conditional_swap|MODEL
 CurveField/FunsExternal|backend.serial.scalar_mul.variable_base.mul|MODEL
+CurveField/FunsExternal|backend.serial.u64.field.FieldElement51.Insts.CoreCmpEq.assert_fields_are_eq|MODEL
 CurveField/FunsExternal|core.array.from_fn|MODEL
 CurveField/FunsExternal|core.fmt.Formatter.debug_struct_field2_finish|MODEL
 CurveField/FunsExternal|core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.get|MODEL
 CurveField/FunsExternal|core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.get_mut|MODEL
+CurveField/FunsExternal|core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.get_unchecked|MODEL
+CurveField/FunsExternal|core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.get_unchecked_mut|MODEL
 CurveField/FunsExternal|core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.index|MODEL
+CurveField/FunsExternal|core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.index_mut|MODEL
 CurveField/FunsExternal|edwards.CompressedEdwardsY.Insts.CoreCmpEq.assert_fields_are_eq|MODEL
 CurveField/FunsExternal|edwards.CompressedEdwardsY.from_slice|MODEL
 CurveField/FunsExternal|edwards.EdwardsPoint.Insts.CoreCmpEq.assert_fields_are_eq|MODEL
 CurveField/FunsExternal|edwards.EdwardsPoint.Insts.CoreIterTraitsAccumSum.sum|MODEL
+CurveField/FunsExternal|edwards.EdwardsPoint.Insts.SubtleConditionallySelectable.conditional_assign|MODEL
 CurveField/FunsExternal|edwards.EdwardsPoint.Insts.SubtleConditionallySelectable.conditional_swap|MODEL
 CurveField/FunsExternal|edwards.affine.AffinePoint.Insts.CoreCmpEq.assert_fields_are_eq|MODEL
+CurveField/FunsExternal|edwards.affine.AffinePoint.Insts.SubtleConditionallySelectable.conditional_assign|MODEL
+CurveField/FunsExternal|edwards.affine.AffinePoint.Insts.SubtleConditionallySelectable.conditional_swap|MODEL
 CurveField/FunsExternal|field.FieldElement51.internal_invert_batch|MODEL
 CurveField/FunsExternal|subtle.Choice.Insts.CoreConvertFromU8.from|MODEL
 CurveField/FunsExternal|subtle.Choice.Insts.CoreOpsBitBitAndChoiceChoice.bitand|MODEL
@@ -33,8 +42,10 @@ CurveField/FunsExternal|subtle.ConditionallySelectable.conditional_swap.default|
 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/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
 CurveSig/FunsExternal|curve25519_dalek.edwards.CompressedEdwardsY.as_bytes|PROVEN
+CurveSig/FunsExternal|curve25519_dalek.edwards.EdwardsPoint.Insts.CoreOpsArithNegEdwardsPoint.neg|PROVEN
 CurveSig/FunsExternal|curve25519_dalek.edwards.EdwardsPoint.compress|PROVEN
 CurveSig/FunsExternal|curve25519_dalek.edwards.EdwardsPoint.vartime_double_scalar_mul_basepoint|PROVEN
 CurveSig/FunsExternal|curve25519_dalek.scalar.Scalar.from_bytes_mod_order|PROVEN
@@ -45,11 +56,10 @@ CurveSig/FunsExternal|signature.error.Error.new|MODEL
 CurveSig/FunsExternal|verifying.sha512_finalize_bytes|MODEL
 CurveSig/FunsExternal|verifying.sha512_new|MODEL
 CurveSig/FunsExternal|verifying.sha512_update|MODEL
-CurveSig/FunsExternal|core.result.Result.Insts.CoreOpsTry_traitFromResidualResultInfallibleE.from_residual|EXTRA
 CurveSig/TypesExternal|curve25519_dalek.edwards.CompressedEdwardsY|PROVEN
 CurveSig/TypesExternal|curve25519_dalek.edwards.EdwardsPoint|PROVEN
 CurveSig/TypesExternal|curve25519_dalek.scalar.Scalar|PROVEN
 CurveSig/TypesExternal|ed25519.Signature|MODEL
 CurveSig/TypesExternal|sha2.Sha512|MODEL
 CurveSig/TypesExternal|signature.error.Error|MODEL
-CORRESPONDENCE-COUNT|54
+CORRESPONDENCE-COUNT|64
diff --git a/verification/check.sh b/verification/check.sh
index e06df2f..4f1f60c 100755
--- a/verification/check.sh
+++ b/verification/check.sh
@@ -791,6 +791,128 @@ for f in "$HERE"/Proofs/*.lean; do
   fi
 done
 [ "$INVFAIL" = 0 ] || { echo "INVENTORY COVERAGE FAILED"; exit 1; }
+# ── Phase 2d: SEMANTIC model/template correspondence ────────────────────────
+# Phase 0d asks a text scanner what the extraction's boundary looks like. This
+# phase asks LEAN what it actually is, and requires the two to agree.
+#
+# WHY BOTH. Round-7 review (GPT-5.6, finding F1) showed the textual classifier
+# could be made to report PROVEN for a name Lean resolves to an axiom — a
+# definition inside a `/- -/` comment was read as real. Worse, and found while
+# repairing that: Aeneas wraps long declarations, and the old scanner required
+# keyword and name on one physical line, so it SILENTLY DROPPED them. Nine to
+# ten externals per fork had no row at all, and one — the tier-A/B `neg` — was
+# missing from every committed table while the docs claimed that class was
+# machine-checked.
+#
+# A source scanner cannot decide this question. Whether a name resolves to an
+# assumption or to a proof is a property of the elaborated ENVIRONMENT: it turns
+# on imports, namespaces, `export`, aliases and shadowing, none of which are
+# visible to a regex. So the scanner's job is now only DISCOVERY — what does the
+# template ask for — and even that fails closed. The verdict comes from Lean.
+#
+# The template itself is deliberately not imported: it declares the same names
+# as the hand-written model and the two would clash. Discovery is therefore
+# unavoidably textual, which is exactly why `model-correspondence.py` must stop
+# rather than skip on anything it cannot parse.
+echo "=== Phase 2d: semantic model/template correspondence ==="
+SEMNAMES=$(mktemp /tmp/check-semnames-XXXX.txt)
+SEMOUT=$(mktemp /tmp/check-semout-XXXX.txt)
+python3 "$HERE/model-correspondence.py" --names "$HERE" > "$SEMNAMES" || {
+  echo "MODEL CORRESPONDENCE FAILED: could not enumerate the extraction's externals."
+  rm -f "$SEMNAMES" "$SEMOUT"; exit 1; }
+
+SEM=$(mktemp "$HERE/.semcheck-XXXX.lean")
+{
+  # Import every generated module that is not a template. There are no name
+  # clashes between crates (verified), and the crate roots transitively pull
+  # their own models, so this is the same environment the proofs are built on.
+  for m in $(cd "$HERE/gen" && find . -name '*.lean' -not -name '*_Template.lean' \
+             | sed 's|^\./||; s|\.lean$||; s|/|.|g' | sort); do
+    echo "import $m"
+  done
+  cat <<'LEANSEM'
+open Lean in
+#eval show CoreM Unit from do
+  let env ← getEnv
+  let path := System.FilePath.mk (← IO.getEnv "SEMNAMES").get!
+  for line in (← IO.FS.lines path) do
+    let parts := line.splitOn "|"
+    if h : parts.length = 2 then
+      let rel := parts[0]!
+      let nm  := parts[1]!.toName
+      match env.find? nm with
+      | none => IO.println s!"SEM|{rel}|{parts[1]!}|ABSENT|-"
+      | some ci =>
+        let kind := match ci with
+          | .axiomInfo _  => "axiom"
+          | .defnInfo _   => "def"
+          | .thmInfo _    => "theorem"
+          | .opaqueInfo _ => "opaque"
+          | .inductInfo _ => "inductive"
+          | .ctorInfo _   => "ctor"
+          | .recInfo _    => "recursor"
+          | .quotInfo _   => "quot"
+        let mdl := match env.getModuleIdxFor? nm with
+          | some i => toString env.header.moduleNames[i]!
+          | none   => "<current>"
+        IO.println s!"SEM|{rel}|{parts[1]!}|{kind}|{mdl}"
+LEANSEM
+} > "$SEM"
+
+cd "$AENEAS_LEAN"
+SEM_RC=0
+SEMNAMES="$SEMNAMES" lake env bash -c "
+  set -uo pipefail
+  cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
+  cd '$HERE'
+  LEAN_TIMEOUT=$TIMEOUT LEAN_MAX_CORES=$CORES '$HERE/lean-guard' '$SEM'
+" > "$SEMOUT" 2>&1 || SEM_RC=$?
+cd "$HERE"
+rm -f "$SEM" "${SEM%.lean}.olean"
+if [ "$SEM_RC" -ne 0 ]; then
+  echo "SEMANTIC CORRESPONDENCE FAILED: the resolver did not run."
+  tail -12 "$SEMOUT" | sed 's/^/    /'
+  rm -f "$SEMNAMES" "$SEMOUT"; exit 1
+fi
+
+# Every name the extraction asks for must have been resolved, and its Lean
+# verdict must equal the committed table's. The mapping is deliberately strict:
+#   resolves into the hand-written model module  -> MODEL
+#   resolves to a NON-AXIOM in a generated module -> PROVEN
+#   anything else                                 -> failure
+SEMFAIL=0
+NSEM=$(grep -c '^SEM|' "$SEMOUT" || true)
+NWANT=$(grep -c '|' "$SEMNAMES" || true)
+if [ "$NSEM" -ne "$NWANT" ]; then
+  echo "  SEMANTIC CORRESPONDENCE TRUNCATED: asked about $NWANT externals, Lean answered for $NSEM"
+  SEMFAIL=1
+fi
+while IFS='|' read -r _tag rel name kind mdl; do
+  [ "$_tag" = SEM ] || continue
+  want=$(awk -F'|' -v r="$rel" -v n="$name" '$1==r && $2==n {print $3}' "$HERE/MODEL-CORRESPONDENCE.txt")
+  case "$kind:$mdl" in
+    axiom:"${rel//\//.}")  got=MODEL ;;
+    *:"${rel//\//.}")      got=MODEL ;;
+    axiom:*)               got=AXIOM-OUTSIDE-MODEL ;;
+    ABSENT:*)              got=UNRESOLVED ;;
+    *)                     got=PROVEN ;;
+  esac
+  if [ -z "$want" ]; then
+    echo "  SEMANTIC DRIFT: $rel|$name resolves ($kind in $mdl) but has NO ROW in MODEL-CORRESPONDENCE.txt"
+    SEMFAIL=1
+  elif [ "$want" != "$got" ]; then
+    echo "  SEMANTIC DRIFT: $rel|$name — table says $want, Lean says $got ($kind in $mdl)"
+    SEMFAIL=1
+  fi
+done < "$SEMOUT"
+rm -f "$SEMNAMES" "$SEMOUT"
+if [ "$SEMFAIL" != 0 ]; then
+  echo "SEMANTIC CORRESPONDENCE FAILED: the committed table does not match what Lean resolves."
+  exit 1
+fi
+echo "  $NWANT externals resolved by Lean; every verdict matches the committed table"
+echo ""
+
 # ── Phase 3: axiom audit of every certificate ───────────────────────────────
 echo "=== Phase 3: axiom audit ==="
 EXPECTED="[propext, Classical.choice, Quot.sound]"
diff --git a/verification/model-correspondence.py b/verification/model-correspondence.py
index 1563013..c8d987c 100755
--- a/verification/model-correspondence.py
+++ b/verification/model-correspondence.py
@@ -8,36 +8,151 @@ needs from outside. Each such name must be provided by exactly one of:
             assumption, which the axiom gate and the per-certificate cones
             then govern;
   PROVEN  — resolved to a real definition in the proven corpus, because a
-            module of this repository declares it (namespace-aware). This is
-            the valuable case and the one the docs claim for the tier-A/B
-            curve calls; nothing has ever checked it.
+            module of this repository declares it (namespace-aware).
 
 Anything else is drift: the extraction asks for something this repository does
 not provide.
-"""
-import re, sys, os, glob
 
-DECL = re.compile(
-    r'^[ \t]*(?:@\[[^\]]*\]\s*)?(?:private |protected |noncomputable |unsafe )*'
-    r'(axiom|def|abbrev|opaque|structure|inductive)[ \t]+([A-Za-z_][A-Za-z0-9_.\'!?]*)')
-NS = re.compile(r'^[ \t]*(namespace|end)[ \t]+([A-Za-z_][A-Za-z0-9_.\']*)')
+────────────────────────────────────────────────────────────────────────────
+WHY THIS FILE WAS REWRITTEN — 2026-08-01, round-7 external review
+
+The first version matched declarations with a LINE-ORIENTED regex requiring the
+keyword and the name on the same physical line, and it did not strip comments.
+Both assumptions are false about Lean, and false about Aeneas's own output.
+Three of the four forks contain, verbatim:
+
+    axiom
+      curve25519_dalek.edwards.EdwardsPoint.Insts.CoreOpsArithNegEdwardsPoint.neg
+      :
+      curve25519_dalek.edwards.EdwardsPoint -> Result ...
+
+The old pattern matched nothing there, so that declaration was SILENTLY
+DROPPED: no MODEL row, no PROVEN row, and no failure. Every committed
+MODEL-CORRESPONDENCE.txt was missing it, and every button passed green over the
+incomplete table. A reviewer separately showed that a definition appearing only
+inside a `/- ... -/` comment was read as a real declaration, so the scanner
+could also report PROVEN for a name Lean resolves to an axiom.
+
+The lesson is not "write a better regex". It is that this scanner was
+FAIL-OPEN: input it could not parse produced silence instead of a stop. A gate
+that drops what it cannot read is worse than no gate, because the button prints
+green across the gap and the gap is invisible in the diff.
+
+This version therefore:
+  · strips comments first, including NESTED `/- ... -/` blocks, which Lean has
+    and which a non-greedy match would close at the first inner `-/`;
+  · allows a declaration's name to appear on a later line than its keyword;
+  · tracks `namespace` / `section` / `end` over the stripped text;
+  · FAILS CLOSED — every declaration keyword must yield a name, or the scanner
+    exits non-zero naming file and line. Nothing is dropped, ever.
+
+WHAT IT STILL IS NOT. This is a source scanner, not a semantic Lean query. It
+cannot see `export`, aliases, or how Lean actually resolves a name at
+elaboration. A PROVEN row is documentary evidence about the extraction
+boundary; it is NOT a Lean-checked fact, and the trust documents must not claim
+it is. What the estate relies on for soundness is kernel-side and
+environment-derived — Phase 2b's axiom gate, Phase 2c's inventory, and the
+exact per-certificate cones of Phase 3/3b — none of which consult this file.
+────────────────────────────────────────────────────────────────────────────
+"""
+import re
+import sys
+import os
+import glob
+
+KEYWORDS = ('axiom', 'def', 'abbrev', 'opaque', 'structure', 'inductive',
+            'instance', 'theorem', 'lemma')
+
+# A declaration keyword opening a logical line, after any attributes and
+# modifiers. The NAME is deliberately NOT part of this pattern: it may sit on a
+# later line, which is precisely the case the previous scanner dropped.
+KW = re.compile(
+    r'^[ \t]*(?:@\[[^\]]*\][ \t\n]*)*'
+    r'(?:private |protected |noncomputable |unsafe |partial |scoped |local )*'
+    r'(' + '|'.join(KEYWORDS) + r')(?=[ \t\n])',
+    re.M)
+
+IDENT = re.compile(r"[ \t\n]*([A-Za-z_][A-Za-z0-9_.'!?]*)")
+
+NS = re.compile(
+    r"^[ \t]*(namespace|section|end)(?:[ \t]+([A-Za-z_][A-Za-z0-9_.']*))?[ \t]*$",
+    re.M)
+
+
+class ScanError(Exception):
+    """Raised when a declaration cannot be parsed. Never swallowed."""
+
+
+def strip_comments(text):
+    """Remove Lean comments, preserving newlines so line numbers stay true.
+
+    Block comments NEST in Lean, so this needs a depth counter: a non-greedy
+    `/-.*?-/` would close the outer block at the first inner `-/` and leave the
+    tail of a nested comment looking like source.
+    """
+    out, i, n, depth = [], 0, len(text), 0
+    while i < n:
+        if text.startswith('/-', i):
+            depth += 1
+            out.append('  ')
+            i += 2
+            continue
+        if text.startswith('-/', i):
+            if depth:
+                depth -= 1
+            out.append('  ')
+            i += 2
+            continue
+        if depth:
+            out.append('\n' if text[i] == '\n' else ' ')
+            i += 1
+            continue
+        if text.startswith('--', i):
+            j = text.find('\n', i)
+            if j < 0:
+                out.append(' ' * (n - i))
+                break
+            out.append(' ' * (j - i))
+            i = j
+            continue
+        out.append(text[i])
+        i += 1
+    return ''.join(out)
+
 
 def declared(path):
-    """Fully-qualified names declared in one file, honouring namespaces."""
-    names, stack = set(), []
-    for line in open(path, encoding='utf-8', errors='replace'):
-        m = NS.match(line)
-        if m:
-            if m.group(1) == 'namespace':
-                stack.append(m.group(2))
-            elif stack and stack[-1] == m.group(2):
+    """Fully-qualified names declared in one file.
+
+    Raises ScanError on any declaration keyword whose name cannot be read.
+    """
+    raw = open(path, encoding='utf-8', errors='replace').read()
+    text = strip_comments(raw)
+
+    # 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()
+    for m in KW.finditer(text):
+        im = IDENT.match(text, m.end())
+        if not im:
+            line = text.count('\n', 0, m.start()) + 1
+            raise ScanError(
+                "%s:%d: `%s` with no parseable name. This scanner fails closed:"
+                " it will not drop a declaration it cannot read."
+                % (path, line, m.group(1)))
+        stack = []
+        for off, kind, arg in events:
+            if off > m.start():
+                break
+            if kind in ('namespace', 'section'):
+                stack.append(arg)
+            elif stack:
                 stack.pop()
-            continue
-        d = DECL.match(line)
-        if d:
-            names.add('.'.join(stack + [d.group(2)]) if stack else d.group(2))
+        prefix = [p for p in stack if p]
+        names.add('.'.join(prefix + [im.group(1)]) if prefix else im.group(1))
     return names
 
+
 def main(root):
     gen = os.path.join(root, 'gen')
     templates = sorted(glob.glob(os.path.join(gen, '*', '*_Template.lean')))
@@ -70,5 +185,30 @@ def main(root):
     print(f'CORRESPONDENCE-COUNT|{len(rows)}')
     return 1 if unresolved else 0
 
+
+def emit_names(root):
+    """Every name the EXTRACTION asks for, as `<rel>|<name>`.
+
+    Template discovery is unavoidably textual: the template is not imported (it
+    would clash with the model, which declares the same names), so no Lean
+    environment contains it. That is why `declared()` fails closed — this list
+    is the input to the semantic phase, and a name missing here is a name
+    nothing will ever check.
+    """
+    gen = os.path.join(root, 'gen')
+    for t in sorted(glob.glob(os.path.join(gen, '*', '*_Template.lean'))):
+        rel = os.path.relpath(t, gen).replace('_Template.lean', '')
+        for n in sorted(declared(t)):
+            print(f'{rel}|{n}')
+    return 0
+
+
 if __name__ == '__main__':
-    sys.exit(main(sys.argv[1]))
+    try:
+        if len(sys.argv) > 2 and sys.argv[1] == '--names':
+            sys.exit(emit_names(sys.argv[2]))
+        sys.exit(main(sys.argv[1]))
+    except ScanError as e:
+        # Fail closed and loudly. Never degrade to a partial table.
+        print('MODEL CORRESPONDENCE SCAN FAILED: %s' % e, file=sys.stderr)
+        sys.exit(2)
diff --git a/verification/selftest-correspondence.sh b/verification/selftest-correspondence.sh
index 7fe9813..a826900 100755
--- a/verification/selftest-correspondence.sh
+++ b/verification/selftest-correspondence.sh
@@ -114,6 +114,49 @@ sed -i '0,/|MODEL$/s/|MODEL$/|PROVEN/' "$HERE/MODEL-CORRESPONDENCE.txt"
 expect "case 4: a verdict edited in the committed table" 1 "MODEL CORRESPONDENCE DRIFT"
 cp "$STASH/corr" "$HERE/MODEL-CORRESPONDENCE.txt"
 
+# ── 5/6. THE ROUND-7 FINDINGS, so they cannot regress ──────────────────────
+# Both were real. Case 5 is GPT-5.6's constructive counterexample: a definition
+# that exists ONLY inside a block comment was read as a real declaration, so the
+# scanner reported PROVEN for a name Lean resolves to an axiom. Case 6 is the
+# one that was live in four committed tables: Aeneas wraps long declarations,
+# the old scanner required keyword and name on one physical line, and so it
+# SILENTLY DROPPED them — nine to ten externals per fork had no row at all.
+#
+# Case 6 is the more important of the two. A gate that drops what it cannot
+# read is worse than no gate: it prints green across a gap that is invisible in
+# the diff. The scanner must now FAIL rather than skip.
+CX=$(mktemp -d)
+mkdir -p "$CX/gen/Forged"
+printf 'axiom Forged.value : Nat\n' > "$CX/gen/Forged/FunsExternal_Template.lean"
+printf 'axiom\n  Forged.value : Nat\n'  > "$CX/gen/Forged/FunsExternal.lean"
+printf '/-\nnamespace Forged\ndef value : Nat := 0\nend Forged\n-/\n' > "$CX/gen/Forged/Funs.lean"
+OUT=$(python3 "$HERE/model-correspondence.py" "$CX" 2>&1)
+if grep -q 'Forged.value|MODEL' <<<"$OUT"; then
+  echo "  ✓ case 5: a definition inside a block comment is not read as a declaration"
+else
+  echo "  ✗ case 5: comment-only definition mis-read — scanner says:"; sed 's/^/      /' <<<"$OUT"
+  FAILURES=$((FAILURES+1))
+fi
+
+printf 'axiom\n  Forged.wrapped\n  :\n  Nat\n' >> "$CX/gen/Forged/FunsExternal_Template.lean"
+OUT=$(python3 "$HERE/model-correspondence.py" "$CX" 2>&1); RC=$?
+if [ "$RC" -ne 0 ] && grep -q 'UNRESOLVED\|Forged.wrapped' <<<"$OUT"; then
+  echo "  ✓ case 6: a declaration whose name wraps to the next line is SEEN, not dropped"
+else
+  echo "  ✗ case 6: wrapped declaration dropped or mis-handled (rc=$RC):"; sed 's/^/      /' <<<"$OUT"
+  FAILURES=$((FAILURES+1))
+fi
+
+printf 'axiom\n' > "$CX/gen/Forged/FunsExternal_Template.lean"
+OUT=$(python3 "$HERE/model-correspondence.py" "$CX" 2>&1); RC=$?
+if [ "$RC" -eq 2 ] && grep -q 'fails closed' <<<"$OUT"; then
+  echo "  ✓ case 7: an unparseable declaration stops the scanner (exit 2), never silence"
+else
+  echo "  ✗ case 7: unparseable declaration did not fail closed (rc=$RC)"
+  FAILURES=$((FAILURES+1))
+fi
+rm -rf "$CX"
+
 expect "restored: the table matches again" 0 "answered by PROVEN definitions"
 
 echo ""