From 73a92fad53b8f71c15a59970c47de5874e42f98b Mon Sep 17 00:00:00 2001 From: mrwulf Date: Mon, 3 Aug 2026 17:34:00 +0200 Subject: [PATCH] Phase 3c: declaration coverage in both directions, and the accounting identity MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Completes the round-8 hardening of this repository. Round-8 review (Claude, register keys `drv-surface-no-cones` and `accounting-certifies-enumeration`). WHAT PHASE 3 DID NOT PIN. It proves each certificate's cone is exact and that no declaration in scope carries a disallowed axiom. It does not pin WHICH declarations exist: a new one that happens to be clean, and a silently vanished one, both pass it. inventory-allowlist.txt 265 rows — the audited corpus driver-allowlist.txt 35 rows — the audit INSTRUMENT's own surface both as INV|module|name|kind|CONE, diffed in BOTH directions by inventory_gate.sh, the same implementation the ed25519 repositories use, with a tag per surface. The instrument surface carries cones because the reviewer showed enumeration is not audit: a claim planted in an instrument is counted by an accounting identity and then examined by nothing, if its row carries no cone and no allowlist covers it. Here the instrument's 35 declarations are pinned exactly as the corpus's 265 are. INTERNAL NAMES ARE NO LONGER EXEMPT from the environment walk. They were skipped, which was harmless while nothing compared that walk against the kernel's view — and became a hole the moment something did: Phase 3b reads object files, which contain the compiler's auxiliaries. Exempting them would have left the accounting identity permanently short and forced the residual to be "explained" by a constant. That is the shape of the fudge term four-fork data refuted in the ed25519 repositories, and it is refused here before it can start. THE ACCOUNTING IDENTITY, as SET CONTAINMENT and never arithmetic: every constant the kernel holds must appear in one of the two walks. The kernel gate now emits KERNEL-NAME rows so the comparison names what is missing rather than reporting a count that has to be interpreted. kernel 300 = inventory 265 + instrument 35 residual: none Negative-tested, all three rejected by name and the tree restored to green: · a deleted INV row -> UNCLASSIFIED: INV|Proofs.ApexSpec|List.allM.eq_1|theorem| · a deleted DRV row -> UNCLASSIFIED: DRV|Proofs.Audit|SlhVerify.Audit.sortNames|def · a row with no declaration behind it -> STALE: …|fips205.ghost_that_does_not_exist|… Both allowlists join the pinned harness set: not executable, so the executable-bit rule cannot reach them, and an allowlist an attacker may rewrite pins nothing. fips205-slhdsa-verified now has the ed25519 repositories' gate set: 0 hygiene, 0d correspondence, 1 model, 2 proofs, 3 in-Lean audit, 3b kernel-side axiom gate, 3c coverage + accounting. Co-Authored-By: Claude Opus 4.8 --- verification/PROVENANCE.json | 7 +- verification/Proofs/Audit.lean | 45 ++++- verification/check.sh | 57 +++++- verification/driver-allowlist.txt | 39 ++++ verification/inventory-allowlist.txt | 270 +++++++++++++++++++++++++++ verification/inventory_gate.sh | 116 ++++++++++++ 6 files changed, 530 insertions(+), 4 deletions(-) create mode 100644 verification/driver-allowlist.txt create mode 100644 verification/inventory-allowlist.txt create mode 100755 verification/inventory_gate.sh diff --git a/verification/PROVENANCE.json b/verification/PROVENANCE.json index a58bcb6..aa14396 100644 --- a/verification/PROVENANCE.json +++ b/verification/PROVENANCE.json @@ -48,12 +48,15 @@ "harness_integrity_sha256": { "_comment": "The harness is part of the trusted computing base and its membership is now SELF-DERIVING: check.sh requires every executable file in verification/ to appear here (round-8 review \u2014 a hardcoded list was itself a second thing to keep in sync), plus Proofs/Audit.lean, which is not executable but computes the digest it is judged by. check.sh itself is excluded: it cannot pin itself, and is disclosed as trusted-unbound in TRUSTED-BASE.md item 11. Pinning check-selftest.sh matters beyond the button: it is the only artifact demonstrating the gates work, and its assertions have been defective in four consecutive rounds, so weakening it is now a reviewable pin rotation rather than an unnoticed edit.", "lean-guard": "690d861cfd81b327604ffd5ef85599ee01b2bcd943907f5b71b8b6f99bad418f", - "Proofs/Audit.lean": "6108b97d75a8a8e8e0b9bef642ba887ea1ae8b17ba5b7c11d66400bfd2847d9e", + "Proofs/Audit.lean": "3a1540187622c47ee2de4bf1dd2379fbbabf4a3d6ec902f2b602dcf486731691", "check-selftest.sh": "c6811482e25ae6e1fffa6ca50e60541e8e609a70c951db6bec4d2d39a4849e9a", "drill.sh": "915cf9310fa168c14ca5d76a1b84fd3b19acdfef9dfd0b03b01b19883548719e", "extract.sh": "01cff43c350ed8eaac0e65ccd7599b68fef47c9434cdb5ad01c92d2127a3bbe9", "model-correspondence.py": "1942177f13d6ae229d87a3b0b33f7fbb4b2ae20fe1059cc83010e73f6a156427", - "MODEL-CORRESPONDENCE.txt": "77bd374a60152689edcb3350c2a2547c6aaad192629e39e86d8548d2bad3f748" + "MODEL-CORRESPONDENCE.txt": "77bd374a60152689edcb3350c2a2547c6aaad192629e39e86d8548d2bad3f748", + "inventory_gate.sh": "3ebc8027f14c9e037f36322ef4119183c33214658efcc1a7bc985a98a9c32e4e", + "inventory-allowlist.txt": "6b27fb410f61d0d6e0d17f9089a5dc1f53027bec507c6c7c180554c5c8f40ede", + "driver-allowlist.txt": "5f9a4167068407ae5e31ec0c7c55d78af455a7ed7f1913b79912f6ae50c13686" }, "audit_gate": "verification/Proofs/Audit.lean \u2014 in-Lean audit (round 5). Per certificate: exact cone equality (collectAxioms) + elaborated-statement check. Enumeration: EVERY declaration kind (def/theorem/opaque/axiom \u2014 round 4 matched theorems only, so a `def : False` passed) in the eight certificate modules AND in Audit.lean itself (the auditor is not exempt). Binding digest: check.sh binds to the SHA-256 of a canonical AUDIT-MANIFEST block covering the POLICY constants (allowedBoundary + certModules \u2014 round-5 NEW-1: widening allowedBoundary previously re-opened the False-proof with the fingerprint byte-identical), every certificate's fully-elaborated statement, and every reachable specification definition's fully-elaborated BODY (round-5 NEW-2: redefining a reference fold to *be* the extracted loop previously left cone and fingerprint intact while the certificate degenerated to `loop = loop`). The 32-bit Expr.hash is retained only as a per-certificate diagnostic, not as the binding. Fail-closed; adversarially exercised by check-selftest.sh. check.sh Phase 0 additionally purges stale .olean files, forbids stray .lean outside gen/ and Proofs/, and pins model + harness bytes." } \ No newline at end of file diff --git a/verification/Proofs/Audit.lean b/verification/Proofs/Audit.lean index 748a55b..7c713d6 100644 --- a/verification/Proofs/Audit.lean +++ b/verification/Proofs/Audit.lean @@ -93,6 +93,21 @@ def manifest : List (Name × List Name × UInt64) := (`fips205.base2b_outer_loop_eq, kernel3, 324621577), (`fips205.slh_verify_128s_accepts_iff, kernel3 ++ [oracleF, oracleH, oracleTL, oracleTLen, oracleHMsg], 2489587792) ] +/-- Declaration kind, in the vocabulary the estate's allowlists already use. + A KIND is part of the record because "the name is still there" and "the + thing behind the name is still the same kind of thing" are different + facts: a theorem quietly replaced by a `def` keeps its name and loses its + meaning. -/ +def kindOf : ConstantInfo → String + | .axiomInfo _ => "axiom" + | .thmInfo _ => "theorem" + | .opaqueInfo _ => "opaque" + | .defnInfo _ => "def" + | .quotInfo _ => "quot" + | .inductInfo _ => "inductive" + | .ctorInfo _ => "ctor" + | .recInfo _ => "rec" + /-- Deterministic name ordering for the canonical serialization. -/ def sortNames (l : List Name) : List Name := ((l.map toString).toArray.qsort (· < ·)).toList.map (·.toName) @@ -172,18 +187,39 @@ elab "auditCones" : command => do let manifestNames := manifest.map (·.1) let mut nEnum := 0 let mut certsSeen : Array Name := #[] + let mut invRows : Array String := #[] + let mut drvRows : Array String := #[] for (nm, ci) in env.constants.toList do let scope : Option String := match env.getModuleIdxFor? nm with | some idx => let m := env.header.moduleNames[idx.toNat]! if certModules.contains m then some (toString m) else none - | none => if nm.isInternal then none else some "Proofs.Audit (this file)" + -- INTERNAL NAMES ARE NO LONGER EXEMPT. They were skipped here, which + -- was harmless while nothing compared this walk against the kernel's + -- view — and became a hole the moment it did: Phase 3b reads the object + -- files, which contain the compiler's auxiliaries, so exempting them + -- here would leave the accounting identity permanently short and force + -- it to be "explained" by a constant. A residual that has to be + -- explained away is the shape of the fudge term four-fork data refuted + -- in the ed25519 repos. + | none => some "Proofs.Audit" match scope with | none => pure () | some where_ => nEnum := nEnum + 1 if manifestNames.contains nm then certsSeen := certsSeen.push nm + -- THE ROW. Same shape as the corpus walks in the ed25519 repositories: + -- module, name, kind, cone. The originating module is part of the record + -- because two modules may legitimately declare the same name, and keyed + -- on name alone one would be covered by the other's entry. + let rowCone := (← collectAxioms nm).toList + let rowKind := kindOf ci + let rowStr := s!"{where_}|{nm}|{rowKind}|{String.intercalate "," ((sortNames rowCone).map toString)}" + if where_ == "Proofs.Audit" then + drvRows := drvRows.push s!"DRV|{rowStr}" + else + invRows := invRows.push s!"INV|{rowStr}" match ci with | .axiomInfo _ => -- the five oracle axioms live in gen/ (Phase-0 pinned); an axiom @@ -232,6 +268,13 @@ elab "auditCones" : command => do -- check.sh prints the certificate list it gets from HERE, not from a hand-kept -- bash array (drill finding: the one authoritative claim string was the one -- thing nothing bound — adding a name to it printed a cert that never existed). + -- The two walks, emitted for check.sh to diff against committed allowlists in + -- BOTH directions. A trailer per walk, so a truncated or crashed emission can + -- never pass as an empty diff. + for r in invRows.qsort (· < ·) do IO.println r + IO.println s!"INV-COUNT|{invRows.size}" + for r in drvRows.qsort (· < ·) do IO.println r + IO.println s!"DRV-COUNT|{drvRows.size}" logInfo s!"CERTIFICATES: {String.intercalate " " (manifestNames.map toString)}" logInfo s!"exact-cone audit PASSED: {manifest.length} certificates (cones + statements), {specs.toList.length} specification constants pinned, {nEnum} declarations enumerated clean" diff --git a/verification/check.sh b/verification/check.sh index 1057974..ff02a4d 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -270,6 +270,8 @@ fi echo " ✓ $(grep -oF 'exact-cone audit PASSED' <<<"$AUD_OUT" | head -1)" echo " ✓ audit-manifest digest matches (sha256 ${EXPECTED_AUDIT_SHA256:0:16}…)" + + # ── Phase 3b: kernel-side axiom-declaration gate ──────────────────────────── # WHY A SECOND GATE ON THE SAME PROPERTY. Phase 3's audit runs INSIDE Lean and # reads `env.constants` after the imports — an ELABORATION-TIME view. That view @@ -320,6 +322,12 @@ run_cmd do let (mod, _) ← readModuleData p for ci in mod.constants do nConst := nConst + 1 + -- The kernel's OWN list of names, for the accounting identity in check.sh: + -- every constant the kernel holds must be accounted for by one of the two + -- environment walks. Emitted rather than counted, because a count cannot + -- say WHICH constant is unaccounted for — the residual would then have to + -- be "explained", which is how a fudge term gets born. + IO.println s!"KERNEL-NAME|{ci.name}" if ci matches .axiomInfo _ then errs := errs.push s!" {name}: {ci.name}" unless errs.isEmpty do @@ -336,18 +344,65 @@ GATE_RC=0 # The temp source AND its artifact are removed on BOTH paths: under `set -e` a # bare rm after the call never runs when the gate goes red, which is how the # ed25519 repos once accumulated 101 orphan .olean files. +GATELOG=$(mktemp /tmp/slh-kernlog-XXXX.log) ( cd "$AENEAS_LEAN" && lake env bash -c " set -euo pipefail cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\" cd '$HERE' LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=$MEM '$HERE/lean-guard' '$GATE' -" ) || GATE_RC=$? +" ) 2>&1 | tee "$GATELOG" || GATE_RC=${PIPESTATUS[0]} rm -f "$GATE" "${GATE%.lean}.olean" if [ "$GATE_RC" -ne 0 ]; then echo "AXIOM SMUGGLING GATE FAILED (kernel-side) — see the error above." exit 1 fi +# ── Phase 3c: declaration coverage, both walks, both directions ───────────── +# Phase 3 proves each certificate's cone is exact and that no declaration in +# scope carries a disallowed axiom. It does NOT pin WHICH declarations exist: +# a new one that happens to be clean, or a silently vanished one, both pass it. +# These two gates diff the walks against committed allowlists in both +# directions — UNCLASSIFIED for something in the environment and not the list, +# STALE for the reverse — using the same implementation the ed25519 repositories +# use for their corpus, with a tag for each surface. +AUDROWS=$(mktemp /tmp/slh-audrows-XXXX.log) +printf '%s\n' "$AUD_OUT" > "$AUDROWS" +COVFAIL=0 +"$HERE/inventory_gate.sh" "$AUDROWS" "$HERE/inventory-allowlist.txt" INV || COVFAIL=1 +"$HERE/inventory_gate.sh" "$AUDROWS" "$HERE/driver-allowlist.txt" DRV || COVFAIL=1 + +# ── THE ACCOUNTING IDENTITY ───────────────────────────────────────────────── +# Round-8 review (Claude, `accounting-certifies-enumeration`). The two walks +# above are ENVIRONMENT views, taken while Audit.lean elaborates. Phase 3b reads +# the OBJECT FILES. Every constant the kernel holds must be accounted for by one +# of the two walks — otherwise a declaration exists that the button compiled, +# the kernel sees, and no allowlist describes. +# +# SET CONTAINMENT, never arithmetic. An earlier version of this identity in the +# ed25519 repositories carried a "+ N_DRIVERS" correction term fitted from one +# repository; four-fork data refuted it (the residual was 2 regardless of driver +# count). A residual that has to be explained is a fudge term waiting to absorb +# the next real finding, so this compares NAMES and prints the ones missing. +KERN=$(mktemp /tmp/slh-kern-XXXX.txt); ACCT=$(mktemp /tmp/slh-acct-XXXX.txt) +LC_ALL=C grep '^KERNEL-NAME|' "$GATELOG" | cut -d'|' -f2 | LC_ALL=C sort -u > "$KERN" +{ LC_ALL=C awk -F'|' '/^INV\|/{print $3}' "$HERE/inventory-allowlist.txt" + LC_ALL=C awk -F'|' '/^DRV\|/{print $3}' "$HERE/driver-allowlist.txt" +} | LC_ALL=C sort -u > "$ACCT" +UNACCOUNTED=$(LC_ALL=C comm -23 "$KERN" "$ACCT") +if [ ! -s "$KERN" ]; then + echo " ACCOUNTING FAILED: the kernel gate reported no names — the scan was vacuous" + COVFAIL=1 +elif [ -n "$UNACCOUNTED" ]; then + echo " ACCOUNTING FAILED: the kernel holds constants that neither walk accounts for:" + printf '%s\n' "$UNACCOUNTED" | head -20 | sed 's/^/ /' + COVFAIL=1 +else + echo " accounting: every one of $(wc -l < "$KERN") kernel constants is covered by the corpus inventory or the instrument surface" +fi +rm -f "$AUDROWS" "$KERN" "$ACCT" +[ "$COVFAIL" = 0 ] || { echo "COVERAGE FAILED"; exit 1; } +rm -f "$GATELOG" + echo echo "ALL GREEN — model compiles, proofs compile, and every certificate cone" diff --git a/verification/driver-allowlist.txt b/verification/driver-allowlist.txt new file mode 100644 index 0000000..48a8f37 --- /dev/null +++ b/verification/driver-allowlist.txt @@ -0,0 +1,39 @@ +# driver-allowlist.txt — the AUDIT INSTRUMENT's own declaration surface, +# with cones, gated by the same implementation that gates the corpus. +# Round-8 review (Claude): enumeration is not audit. Rows carrying no cone, +# covered by no allowlist, are counted and then examined by nothing. +DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1._sparseCasesOn_3|def|propext +DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1._sparseCasesOn_6|def|propext +DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_11|def| +DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_13|def|propext +DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_15|def| +DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_17|def| +DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_19|def|Classical.choice,Quot.sound,propext +DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_1|def| +DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_21|def| +DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_3|def|propext +DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_6|def|propext +DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_9|def| +DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1|def|Classical.choice,Quot.sound,propext +DRV|Proofs.Audit|SlhVerify.Audit.allowedBoundary|def| +DRV|Proofs.Audit|SlhVerify.Audit.certModules|def| +DRV|Proofs.Audit|SlhVerify.Audit.closureOf._sparseCasesOn_1|def|propext +DRV|Proofs.Audit|SlhVerify.Audit.closureOf._unsafe_rec|def|Classical.choice,Quot.sound,propext +DRV|Proofs.Audit|SlhVerify.Audit.closureOf.match_1|def|propext +DRV|Proofs.Audit|SlhVerify.Audit.closureOf.match_4|def| +DRV|Proofs.Audit|SlhVerify.Audit.closureOf|opaque|Classical.choice,Quot.sound,propext +DRV|Proofs.Audit|SlhVerify.Audit.commandAuditCones|def| +DRV|Proofs.Audit|SlhVerify.Audit.isSpecConst.match_1|def| +DRV|Proofs.Audit|SlhVerify.Audit.isSpecConst|def|Classical.choice,Quot.sound,propext +DRV|Proofs.Audit|SlhVerify.Audit.kernel3|def| +DRV|Proofs.Audit|SlhVerify.Audit.kindOf.match_1|def| +DRV|Proofs.Audit|SlhVerify.Audit.kindOf|def| +DRV|Proofs.Audit|SlhVerify.Audit.manifest|def| +DRV|Proofs.Audit|SlhVerify.Audit.normWs|def|Classical.choice,Quot.sound,propext +DRV|Proofs.Audit|SlhVerify.Audit.oracleF|def| +DRV|Proofs.Audit|SlhVerify.Audit.oracleHMsg|def| +DRV|Proofs.Audit|SlhVerify.Audit.oracleH|def| +DRV|Proofs.Audit|SlhVerify.Audit.oracleTLen|def| +DRV|Proofs.Audit|SlhVerify.Audit.oracleTL|def| +DRV|Proofs.Audit|SlhVerify.Audit.ppAll|def|Classical.choice,Quot.sound,propext +DRV|Proofs.Audit|SlhVerify.Audit.sortNames|def|Classical.choice,Quot.sound,propext diff --git a/verification/inventory-allowlist.txt b/verification/inventory-allowlist.txt new file mode 100644 index 0000000..873ddc6 --- /dev/null +++ b/verification/inventory-allowlist.txt @@ -0,0 +1,270 @@ +# inventory-allowlist.txt — the audited corpus, one row per declaration: +# INV|module|name|kind|cone +# Diffed in BOTH directions by inventory_gate.sh. A row here that is not in +# the environment is STALE; a declaration not here is UNCLASSIFIED. Neither +# passes. Regenerate deliberately and read the diff. +INV|Proofs.ApexSpec|List.allM.eq_1|theorem| +INV|Proofs.ApexSpec|List.allM.eq_2|theorem| +INV|Proofs.ApexSpec|List.allM.eq_def|theorem| +INV|Proofs.ApexSpec|_private.Proofs.ApexSpec.0.List.anyM.match_1.eq_1|theorem| +INV|Proofs.ApexSpec|_private.Proofs.ApexSpec.0.List.anyM.match_1.eq_2|theorem| +INV|Proofs.ApexSpec|_private.Proofs.ApexSpec.0.List.anyM.match_1.splitter|def| +INV|Proofs.ApexSpec|_private.Proofs.ApexSpec.0.List.mapA.match_1.eq_1|theorem| +INV|Proofs.ApexSpec|_private.Proofs.ApexSpec.0.List.mapA.match_1.eq_2|theorem| +INV|Proofs.ApexSpec|_private.Proofs.ApexSpec.0.List.mapA.match_1.splitter|def| +INV|Proofs.ApexSpec|fips205.allM_byteEq._proof_1_1|theorem|Quot.sound,propext +INV|Proofs.ApexSpec|fips205.allM_byteEq|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ApexSpec|fips205.arrayEqU8_spec|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ApexSpec|fips205.byteEq|theorem| +INV|Proofs.ApexSpec|fips205.htVerifyRoot._proof_1|theorem|propext +INV|Proofs.ApexSpec|fips205.htVerifyRoot._proof_2|theorem|propext +INV|Proofs.ApexSpec|fips205.htVerifyRoot|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l +INV|Proofs.ApexSpec|fips205.ht_verify_free_split|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l +INV|Proofs.ApexSpec|fips205.slhVerifyRoot._proof_1|theorem|propext +INV|Proofs.ApexSpec|fips205.slhVerifyRoot._proof_2|theorem|propext +INV|Proofs.ApexSpec|fips205.slhVerifyRoot._proof_3|theorem|propext +INV|Proofs.ApexSpec|fips205.slhVerifyRoot._proof_4|theorem|propext +INV|Proofs.ApexSpec|fips205.slhVerifyRoot._proof_5|theorem|propext +INV|Proofs.ApexSpec|fips205.slhVerifyRoot._proof_6|theorem|propext +INV|Proofs.ApexSpec|fips205.slhVerifyRoot|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.h_msg,verify_mono.oracle.t_l,verify_mono.oracle.t_len +INV|Proofs.ApexSpec|fips205.slh_verify_128s_accepts_iff|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.h_msg,verify_mono.oracle.t_l,verify_mono.oracle.t_len +INV|Proofs.ApexSpec|fips205.slh_verify_internal_accepts_iff|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.h_msg,verify_mono.oracle.t_l,verify_mono.oracle.t_len +INV|Proofs.ChainSpec|Aeneas.Std.core.cmp.impls.PartialOrdU32.lt.eq_1|theorem| +INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_1|theorem| +INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_2|theorem| +INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.splitter|def| +INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.fips205.chainFoldN.match_1.eq_1|theorem| +INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.fips205.chainFoldN.match_1.eq_2|theorem| +INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.fips205.chainFoldN.match_1.splitter|def| +INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_1|theorem| +INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_2|theorem| +INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.fips205.helpers.to_byte_loop.body.match_1.splitter|def| +INV|Proofs.ChainSpec|fips205.chainFoldN._f|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f +INV|Proofs.ChainSpec|fips205.chainFoldN._proof_1|theorem|propext +INV|Proofs.ChainSpec|fips205.chainFoldN._sunfold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f +INV|Proofs.ChainSpec|fips205.chainFoldN.eq_def|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f +INV|Proofs.ChainSpec|fips205.chainFoldN.match_1|def| +INV|Proofs.ChainSpec|fips205.chainFoldN|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f +INV|Proofs.ChainSpec|fips205.chain_free_loop_eq._proof_1_1|theorem|Quot.sound,propext +INV|Proofs.ChainSpec|fips205.chain_free_loop_eq._proof_1_6|theorem|Quot.sound,propext +INV|Proofs.ChainSpec|fips205.chain_free_loop_eq._proof_1_7|theorem|Quot.sound,propext +INV|Proofs.ChainSpec|fips205.chain_free_loop_eq._proof_1_8|theorem|Quot.sound,propext +INV|Proofs.ChainSpec|fips205.chain_free_loop_eq._proof_1_9|theorem|Quot.sound,propext +INV|Proofs.ChainSpec|fips205.chain_free_loop_eq|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f +INV|Proofs.ChainSpec|fips205.chain_step|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f +INV|Proofs.ChainSpec|fips205.fwd_succ|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ChainSpec|fips205.hbody|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f +INV|Proofs.ChainSpec|fips205.hnext|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ChainSpec|fips205.loop_unfold_bind|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ChainSpec|fips205.u32_succ._proof_1_1|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ChainSpec|fips205.u32_succ._proof_1_2|theorem|Quot.sound,propext +INV|Proofs.ChainSpec|fips205.u32_succ|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_1|theorem| +INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_2|theorem| +INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.splitter|def| +INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.fips205.forsInnerFold.match_1.eq_1|theorem| +INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.fips205.forsInnerFold.match_1.eq_2|theorem| +INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.fips205.forsInnerFold.match_1.splitter|def| +INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_1|theorem| +INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_2|theorem| +INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.fips205.helpers.to_byte_loop.body.match_1.splitter|def| +INV|Proofs.ForsInnerSpec|fips205.forsInnerFold._f|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.h +INV|Proofs.ForsInnerSpec|fips205.forsInnerFold._proof_1|theorem|propext +INV|Proofs.ForsInnerSpec|fips205.forsInnerFold._proof_2|theorem|propext +INV|Proofs.ForsInnerSpec|fips205.forsInnerFold._proof_3|theorem|propext +INV|Proofs.ForsInnerSpec|fips205.forsInnerFold._sunfold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.h +INV|Proofs.ForsInnerSpec|fips205.forsInnerFold.eq_def|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h +INV|Proofs.ForsInnerSpec|fips205.forsInnerFold.match_1|def| +INV|Proofs.ForsInnerSpec|fips205.forsInnerFold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.h +INV|Proofs.ForsInnerSpec|fips205.fors_inner_loop_eq._proof_1_1|theorem|Quot.sound,propext +INV|Proofs.ForsInnerSpec|fips205.fors_inner_loop_eq._proof_1_5|theorem|Quot.sound,propext +INV|Proofs.ForsInnerSpec|fips205.fors_inner_loop_eq._proof_1_6|theorem|Quot.sound,propext +INV|Proofs.ForsInnerSpec|fips205.fors_inner_loop_eq._proof_1_7|theorem|Quot.sound,propext +INV|Proofs.ForsInnerSpec|fips205.fors_inner_loop_eq._proof_1_8|theorem|Quot.sound,propext +INV|Proofs.ForsInnerSpec|fips205.fors_inner_loop_eq|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h +INV|Proofs.ForsInnerSpec|fips205.fors_inner_step|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h +INV|Proofs.ForsInnerSpec|fips205.hbody_fi|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h +INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_1|theorem| +INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_2|theorem| +INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.splitter|def| +INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.fips205.forsOuterFold.match_1.eq_1|theorem| +INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.fips205.forsOuterFold.match_1.eq_2|theorem| +INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.fips205.forsOuterFold.match_1.splitter|def| +INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_1|theorem| +INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_2|theorem| +INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.fips205.helpers.to_byte_loop.body.match_1.splitter|def| +INV|Proofs.ForsOuterSpec|fips205.forsOuterFold._f|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h +INV|Proofs.ForsOuterSpec|fips205.forsOuterFold._proof_1|theorem|propext +INV|Proofs.ForsOuterSpec|fips205.forsOuterFold._proof_2|theorem|propext +INV|Proofs.ForsOuterSpec|fips205.forsOuterFold._sunfold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h +INV|Proofs.ForsOuterSpec|fips205.forsOuterFold.eq_def|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h +INV|Proofs.ForsOuterSpec|fips205.forsOuterFold.match_1|def| +INV|Proofs.ForsOuterSpec|fips205.forsOuterFold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h +INV|Proofs.ForsOuterSpec|fips205.fors_outer_loop_eq._proof_1_1|theorem|Quot.sound,propext +INV|Proofs.ForsOuterSpec|fips205.fors_outer_loop_eq._proof_1_5|theorem|Quot.sound,propext +INV|Proofs.ForsOuterSpec|fips205.fors_outer_loop_eq._proof_1_6|theorem|Quot.sound,propext +INV|Proofs.ForsOuterSpec|fips205.fors_outer_loop_eq._proof_1_7|theorem|Quot.sound,propext +INV|Proofs.ForsOuterSpec|fips205.fors_outer_loop_eq._proof_1_8|theorem|Quot.sound,propext +INV|Proofs.ForsOuterSpec|fips205.fors_outer_loop_eq|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h +INV|Proofs.ForsOuterSpec|fips205.fors_outer_step|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h +INV|Proofs.ForsOuterSpec|fips205.hbody_fo|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h +INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_1|theorem| +INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_2|theorem| +INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.splitter|def| +INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_1|theorem| +INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_2|theorem| +INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.fips205.helpers.to_byte_loop.body.match_1.splitter|def| +INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.fips205.htFoldN.match_1.eq_1|theorem| +INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.fips205.htFoldN.match_1.eq_2|theorem| +INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.fips205.htFoldN.match_1.splitter|def| +INV|Proofs.HtSpec|fips205.hbody_ht|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l +INV|Proofs.HtSpec|fips205.htFoldN._f|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l +INV|Proofs.HtSpec|fips205.htFoldN._proof_1|theorem|propext +INV|Proofs.HtSpec|fips205.htFoldN._proof_2|theorem|propext +INV|Proofs.HtSpec|fips205.htFoldN._sunfold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l +INV|Proofs.HtSpec|fips205.htFoldN.eq_def|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l +INV|Proofs.HtSpec|fips205.htFoldN.match_1|def| +INV|Proofs.HtSpec|fips205.htFoldN|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l +INV|Proofs.HtSpec|fips205.ht_loop_eq._proof_1_1|theorem|Quot.sound,propext +INV|Proofs.HtSpec|fips205.ht_loop_eq._proof_1_5|theorem|Quot.sound,propext +INV|Proofs.HtSpec|fips205.ht_loop_eq._proof_1_6|theorem|Quot.sound,propext +INV|Proofs.HtSpec|fips205.ht_loop_eq._proof_1_7|theorem|Quot.sound,propext +INV|Proofs.HtSpec|fips205.ht_loop_eq._proof_1_8|theorem|Quot.sound,propext +INV|Proofs.HtSpec|fips205.ht_loop_eq|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l +INV|Proofs.HtSpec|fips205.ht_loop_step|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l +INV|Proofs.InputPrepSpec|Aeneas.Std.I32.ofInt.congr_simp|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_1|theorem| +INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_2|theorem| +INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.splitter|def| +INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.base2bOuterFold.match_1.eq_1|theorem|propext +INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.base2bOuterFold.match_1.eq_2|theorem|propext +INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.base2bOuterFold.match_1.splitter|def|propext +INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_1|theorem| +INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_2|theorem| +INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.helpers.to_byte_loop.body.match_1.splitter|def| +INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.helpers.to_int_loop.body.match_1.eq_1|theorem| +INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.helpers.to_int_loop.body.match_1.eq_2|theorem| +INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.helpers.to_int_loop.body.match_1.splitter|def| +INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.toByteFold.match_1.eq_1|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.toByteFold.match_1.eq_2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.toByteFold.match_1.splitter|def|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.toIntFold.match_1.eq_1|theorem| +INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.toIntFold.match_1.eq_2|theorem| +INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.toIntFold.match_1.splitter|def| +INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.wotsCsumFold.match_1.eq_1|theorem| +INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.wotsCsumFold.match_1.eq_2|theorem| +INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.wotsCsumFold.match_1.splitter|def| +INV|Proofs.InputPrepSpec|fips205.base2bOuterFold._f|def|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.base2bOuterFold._proof_1|theorem|propext +INV|Proofs.InputPrepSpec|fips205.base2bOuterFold._sunfold|def|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.base2bOuterFold.eq_def|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.base2bOuterFold.match_1|def|propext +INV|Proofs.InputPrepSpec|fips205.base2bOuterFold|def|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.base2b_outer_loop_eq._proof_1_1|theorem|Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.base2b_outer_loop_eq._proof_1_5|theorem|Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.base2b_outer_loop_eq._proof_1_6|theorem|Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.base2b_outer_loop_eq._proof_1_7|theorem|Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.base2b_outer_loop_eq._proof_1_8|theorem|Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.base2b_outer_loop_eq|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.base2b_outer_step|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.hbody_b2|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.hbody_cs|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.hbody_tb|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.hbody_ti|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.toByteFold._f|def|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.toByteFold._proof_1|theorem|propext +INV|Proofs.InputPrepSpec|fips205.toByteFold._proof_2|theorem|propext +INV|Proofs.InputPrepSpec|fips205.toByteFold._proof_3|theorem|propext +INV|Proofs.InputPrepSpec|fips205.toByteFold._proof_4|theorem|propext +INV|Proofs.InputPrepSpec|fips205.toByteFold._sunfold|def|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.toByteFold.eq_def|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.toByteFold.match_1|def|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.toByteFold|def|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.toIntFold._f|def|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.toIntFold._proof_1|theorem|propext +INV|Proofs.InputPrepSpec|fips205.toIntFold._proof_2|theorem|propext +INV|Proofs.InputPrepSpec|fips205.toIntFold._sunfold|def|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.toIntFold.eq_def|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.toIntFold.match_1|def| +INV|Proofs.InputPrepSpec|fips205.toIntFold|def|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.to_byte_loop_eq._proof_1_1|theorem|Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.to_byte_loop_eq._proof_1_5|theorem|Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.to_byte_loop_eq._proof_1_6|theorem|Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.to_byte_loop_eq._proof_1_7|theorem|Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.to_byte_loop_eq._proof_1_8|theorem|Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.to_byte_loop_eq|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.to_byte_step|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.to_int_loop_eq._proof_1_1|theorem|Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.to_int_loop_eq._proof_1_5|theorem|Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.to_int_loop_eq._proof_1_6|theorem|Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.to_int_loop_eq._proof_1_7|theorem|Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.to_int_loop_eq._proof_1_8|theorem|Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.to_int_loop_eq|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.to_int_step|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.wotsCsumFold._f|def|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.wotsCsumFold._sunfold|def|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.wotsCsumFold.eq_def|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.wotsCsumFold.match_1|def| +INV|Proofs.InputPrepSpec|fips205.wotsCsumFold|def|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.wots_csum_loop_eq._proof_1_1|theorem|Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.wots_csum_loop_eq._proof_1_5|theorem|Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.wots_csum_loop_eq._proof_1_6|theorem|Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.wots_csum_loop_eq._proof_1_7|theorem|Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.wots_csum_loop_eq._proof_1_8|theorem|Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.wots_csum_loop_eq|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.InputPrepSpec|fips205.wots_csum_step|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.WotsSpec|Aeneas.Std.core.cmp.impls.PartialOrdUsize.lt.eq_1|theorem| +INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_1|theorem| +INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_2|theorem| +INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.splitter|def| +INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.fips205.helpers.to_int_loop.body.match_1.eq_1|theorem| +INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.fips205.helpers.to_int_loop.body.match_1.eq_2|theorem| +INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.fips205.helpers.to_int_loop.body.match_1.splitter|def| +INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.fips205.wotsChainFold.match_1.eq_1|theorem| +INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.fips205.wotsChainFold.match_1.eq_2|theorem| +INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.fips205.wotsChainFold.match_1.splitter|def| +INV|Proofs.WotsSpec|fips205.fwd_succ_usize|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.WotsSpec|fips205.hbody1|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f +INV|Proofs.WotsSpec|fips205.hnext_usize|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.WotsSpec|fips205.usize_succ._proof_1_1|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.WotsSpec|fips205.usize_succ._proof_1_2|theorem|Quot.sound,propext +INV|Proofs.WotsSpec|fips205.usize_succ|theorem|Classical.choice,Quot.sound,propext +INV|Proofs.WotsSpec|fips205.wotsChainFold._f|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f +INV|Proofs.WotsSpec|fips205.wotsChainFold._proof_1|theorem|propext +INV|Proofs.WotsSpec|fips205.wotsChainFold._proof_2|theorem|propext +INV|Proofs.WotsSpec|fips205.wotsChainFold._sunfold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f +INV|Proofs.WotsSpec|fips205.wotsChainFold.eq_def|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f +INV|Proofs.WotsSpec|fips205.wotsChainFold.match_1|def| +INV|Proofs.WotsSpec|fips205.wotsChainFold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f +INV|Proofs.WotsSpec|fips205.wots_loop1_eq._proof_1_1|theorem|Quot.sound,propext +INV|Proofs.WotsSpec|fips205.wots_loop1_eq._proof_1_6|theorem|Quot.sound,propext +INV|Proofs.WotsSpec|fips205.wots_loop1_eq._proof_1_7|theorem|Quot.sound,propext +INV|Proofs.WotsSpec|fips205.wots_loop1_eq._proof_1_8|theorem|Quot.sound,propext +INV|Proofs.WotsSpec|fips205.wots_loop1_eq._proof_1_9|theorem|Quot.sound,propext +INV|Proofs.WotsSpec|fips205.wots_loop1_eq|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f +INV|Proofs.WotsSpec|fips205.wots_loop1_step|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f +INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_1|theorem| +INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_2|theorem| +INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.splitter|def| +INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_1|theorem| +INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_2|theorem| +INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.fips205.helpers.to_byte_loop.body.match_1.splitter|def| +INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.fips205.xmssFoldN.match_1.eq_1|theorem| +INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.fips205.xmssFoldN.match_1.eq_2|theorem| +INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.fips205.xmssFoldN.match_1.splitter|def| +INV|Proofs.XmssSpec|fips205.hbody_x|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h +INV|Proofs.XmssSpec|fips205.xmssFoldN._f|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.h +INV|Proofs.XmssSpec|fips205.xmssFoldN._proof_1|theorem|propext +INV|Proofs.XmssSpec|fips205.xmssFoldN._proof_2|theorem|propext +INV|Proofs.XmssSpec|fips205.xmssFoldN._proof_3|theorem|propext +INV|Proofs.XmssSpec|fips205.xmssFoldN._sunfold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.h +INV|Proofs.XmssSpec|fips205.xmssFoldN.eq_def|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h +INV|Proofs.XmssSpec|fips205.xmssFoldN.match_1|def| +INV|Proofs.XmssSpec|fips205.xmssFoldN|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.h +INV|Proofs.XmssSpec|fips205.xmss_loop_eq._proof_1_1|theorem|Quot.sound,propext +INV|Proofs.XmssSpec|fips205.xmss_loop_eq._proof_1_5|theorem|Quot.sound,propext +INV|Proofs.XmssSpec|fips205.xmss_loop_eq._proof_1_6|theorem|Quot.sound,propext +INV|Proofs.XmssSpec|fips205.xmss_loop_eq._proof_1_7|theorem|Quot.sound,propext +INV|Proofs.XmssSpec|fips205.xmss_loop_eq._proof_1_8|theorem|Quot.sound,propext +INV|Proofs.XmssSpec|fips205.xmss_loop_eq|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h +INV|Proofs.XmssSpec|fips205.xmss_loop_step|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h diff --git a/verification/inventory_gate.sh b/verification/inventory_gate.sh new file mode 100755 index 0000000..b0de821 --- /dev/null +++ b/verification/inventory_gate.sh @@ -0,0 +1,116 @@ +#!/usr/bin/env bash +# ───────────────────────────────────────────────────────────────────────────── +# inventory_gate.sh — diff an observed environment inventory against the +# pinned allowlist. PORTED VERBATIM from ltl-accumulator-verified apart from +# the axiom-surface assertion, which is repo-specific: there the corpus admits +# exactly one sanctioned axiom, here it admits none. +# +# This is THE production coverage gate: check.sh Phase 2c calls it, and the +# self-test exercises this exact script — the tested logic IS the shipping +# logic. +# +# Usage: inventory_gate.sh [] +# +# defaults to INV — the CORPUS walk. Pass DRV to gate the INSTRUMENTS' +# OWN SURFACE with this same implementation. +# +# WHY THE TAG EXISTS — round-8 review (Claude, register keys +# `drv-surface-no-cones`, `accounting-certifies-enumeration`). +# +# The accounting identity added in round 7 proved every constant the kernel +# sees is ENUMERATED by one of the two walks. The reviewer showed that +# enumeration is not audit: a claim planted in an instrument WAS enumerated — +# `DRV|LTLAccAudit.bait.smuggled|theorem` — and then nothing looked at it, +# because DRV rows carried name and kind and NO CONE, and no allowlist covered +# them. In their words, the identity "converted 36 declarations nobody +# enumerated into 36 declarations nobody examined. That is progress of one +# step, not two." +# +# The second step is here: DRV rows now carry their axiom cone and are pinned +# in a committed allowlist, by THIS gate, in both directions — exactly as the +# corpus is. One implementation, not two, because a second copy of a coverage +# gate is a second thing to drift. +# +# It also retires a heuristic. The driver-surface rule permits a theorem whose +# name extends a constant declared alongside it, since that is what the +# elaborator generates for a definition; the reviewer showed it "breaks in one +# line" — declare `def bait`, then `theorem bait.smuggled` passes. That rule is +# kept as a fast, readable first line of defence, but it is NO LONGER +# LOAD-BEARING: a planted claim now has to appear in the pinned allowlist, and +# a new row fails closed whatever it is named. +# +# Fail-closed in BOTH directions: +# UNCLASSIFIED — constant in the environment, absent from the allowlist +# (new/renamed decl, changed kind, or changed axiom cone) +# STALE — allowlist entry absent from the environment +# plus an output-integrity check: the INV-COUNT trailer emitted by +# Proofs/Inventory.lean must equal the number of INV lines actually seen, +# so a truncated or crashed run can never pass as an empty diff. +# ───────────────────────────────────────────────────────────────────────────── +set -uo pipefail +export LC_ALL=C # byte-order collation: sort/comm must agree with Lean's String order +obs_file="$1"; allow_file="$2"; TAG="${3:-INV}" +case "$TAG" in + INV) WHAT="the audited corpus"; TRAILER_TAG="INV-COUNT"; LABEL="inventory gate"; TRUNCLABEL="INVENTORY TRUNCATED" ;; + DRV) WHAT="the audit instruments"; TRAILER_TAG="DRV-COUNT"; LABEL="driver-surface gate"; TRUNCLABEL="DRIVER SURFACE TRUNCATED" ;; + *) echo " GATE MISUSE: unknown tag '$TAG' (expected INV or DRV)"; exit 1 ;; +esac + +# The trailer is an OUTPUT-INTEGRITY check: it must equal the number of rows +# the driver(s) actually emitted, BEFORE de-duplication. Comparing it to the +# de-duplicated count conflates "a run was truncated" with "two rows were +# identical", and the second is a record-format defect that must be fixed at +# the source, not absorbed here. (It was: DRV rows now carry their driver.) +N_RAW=$(grep -c "^$TAG|" "$obs_file" || true) +OBS=$(grep "^$TAG|" "$obs_file" | sort -u) +N_OBS=$(printf '%s' "$OBS" | grep -c "^$TAG|" || true) +if [ "$N_RAW" -ne "$N_OBS" ]; then + echo " DUPLICATE $TAG RECORDS: $N_RAW rows collapse to $N_OBS distinct ones." + echo " Two declarations share a record, so one is covered by the other's entry:" + grep "^$TAG|" "$obs_file" | sort | uniq -d | head -5 | sed 's/^/ /' + exit 1 +fi +# Each driver emits its own trailer, so DRV trailers are SUMMED; the corpus +# walk emits one and the last is taken. Either way a truncated or crashed run +# must never pass as an empty diff. +if [ "$TAG" = DRV ]; then + TRAILER=$(grep "^$TRAILER_TAG|" "$obs_file" | cut -d'|' -f2 | paste -sd+ - | bc) +else + TRAILER=$(grep "^$TRAILER_TAG|" "$obs_file" | tail -1 | cut -d'|' -f2) +fi +if [ -z "$TRAILER" ] || [ "$TRAILER" != "$N_RAW" ]; then + echo " $TRUNCLABEL: trailer=${TRAILER:-absent}, observed $N_RAW lines" + exit 1 +fi + +ALLOW=$(grep "^$TAG|" "$allow_file" | sort -u) +FAILGATE=0 +UNCLASS=$(comm -23 <(printf '%s\n' "$OBS") <(printf '%s\n' "$ALLOW")) +STALE=$(comm -13 <(printf '%s\n' "$OBS") <(printf '%s\n' "$ALLOW")) +if [ -n "$UNCLASS" ]; then + printf '%s\n' "$UNCLASS" | sed 's/^/ UNCLASSIFIED (in environment, not allowlisted): /' + FAILGATE=1 +fi +if [ -n "$STALE" ]; then + printf '%s\n' "$STALE" | sed 's/^/ STALE (allowlisted, not in environment): /' + FAILGATE=1 +fi + +# The audited corpus admits NO axiom declarations at all: the sanctioned +# external models live in gen/, outside every module these drivers cover, and +# are byte-pinned by Phase 0b. An axiom appearing here would be a declaration +# smuggled into the proof corpus, which Phase 2b also catches kernel-side — +# two independent gates on the same property, deliberately. +AXLINES=$(printf '%s\n' "$OBS" | grep '|axiom|' || true) +if [ -n "$AXLINES" ]; then + echo " AXIOM SURFACE DRIFT: $WHAT must declare no axioms; observed:" + printf '%s\n' "$AXLINES" | sed 's/^/ /' + FAILGATE=1 +fi + +# The message must describe what was actually checked. It said "single +# sanctioned axiom" when ported, which is the accumulator's policy; here the +# audited corpus permits NONE, and a success line describing a different rule +# is how an assertion quietly stops meaning anything. +[ "$FAILGATE" = 0 ] && echo " $LABEL: $N_OBS constants, environment == allowlist, zero axioms declared in $WHAT" +exit "$FAILGATE"