mirror of
https://github.com/saymrwulf/ltl-accumulator-verified.git
synced 2026-09-03 19:53:48 +00:00
mrwulf
b575e857e3
STATEMENT BINDING (Phase 3d). The coverage gate pins every constant's name,
kind and axiom cone, both directions, and none of selftest_audit.sh's nine
attacks defeat it. It is nevertheless blind to what a declaration SAYS — and
that is demonstrated here rather than argued:
Wrapping one branch of `LTLAcc.pinAccept`'s body in `id (…)` is
definitionally equal. Every downstream proof still compiles. The name, the
kind, the type and the axiom cone are unchanged. The inventory gate reports
"222 constants, environment == allowlist" — GREEN.
That edit is harmless by construction; the point is that nothing stood between
it and a genuinely vacuous redefinition of a specification. Proofs/Inventory.lean
now also emits, for every inventoried constant, its fully-elaborated TYPE, and
for every definition its fully-elaborated BODY — 266 lines over 222 constants.
Proof terms are deliberately absent: by proof irrelevance a theorem's content
is its statement. check.sh Phase 3d binds the SHA-256 and the block is
committed as AUDIT-MANIFEST.txt so a mismatch is DIFFED, not merely reported.
The existing gate is untouched, per the standing rule that the port flows FROM
this repo, not to it: INV lines are byte-identical, inventory_gate.sh is
unchanged, and all nine of its attacks still fail as before.
selftest_statements.sh replays the defeq edit as case 1, asserting BOTH that
the coverage gate passes it and that Phase 3d catches it — so if the coverage
gate ever grows to see this, the test says so instead of quietly re-labelling.
Cases 2-4 cover a hand-edited committed block, a truncated block, and a
constant inventoried without a statement.
FIDELITY PIN (unrelated, found while running the button). Phase 4 had been
failing since 2026-07-23: LIED_PIN_DIV expected 3,867 divergences between the
Lean model and the deployed consistency verifier, and observed 0. Cause is
pacta ddbb5a4, which restored the RFC 9162 2.1.4.2 Step-7 terminal `sn == 0`
condition; that one conjunct removes every divergence in the pinned
73,573-case family. KNOWN-GAPS gap 14 already recorded the closure on the day
it landed — only this constant was stale, so the button had been red for five
days with nobody running it. The pin now reads 0 with the history in a comment.
Nothing about the paper, public log entry 13, or the attested commit 172a1d0
changes; the historical divergence stays reproducible at the tagged pre-fix
commit.
KNOWN-GAPS gap 16 records what the binding does not buy: identity, not
meaning; an author who edits and re-pins in one commit is caught by review and
not by the script; and proof terms are unbound by design.
Button green end to end: ATTESTATION GREEN (Lean + fidelity).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
366 lines
19 KiB
Bash
Executable file
366 lines
19 KiB
Bash
Executable file
#!/usr/bin/env bash
|
|
# ─────────────────────────────────────────────────────────────────────────────
|
|
# check.sh — THE button (accumulator corpus). Same discipline as the
|
|
# *-ed25519-verified repos: compiles every shipped .lean through lean-guard
|
|
# and axiom-audits every certificate against its DOCUMENTED exact cone,
|
|
# both directions.
|
|
#
|
|
# Phases: 0 resource/integrity · 1 stub+axiom-smuggling audit ·
|
|
# 2 compile manifest · 3 boundary-exact axiom audit ·
|
|
# 3b environment-derived coverage · 3c doc-consistency ·
|
|
# 3d statement + specification binding · 4 definition fidelity
|
|
# ─────────────────────────────────────────────────────────────────────────────
|
|
set -euo pipefail
|
|
# Toolchain bootstrap is overridable for reviewers with their own install
|
|
# (review round 3, GPT §7); the operator default stays pinned.
|
|
AENEAS_ENV="${AENEAS_ENV:-$HOME/aeneas-toolchain/env.sh}"
|
|
[ -f "$AENEAS_ENV" ] || { echo "FATAL: Aeneas environment not found: $AENEAS_ENV (set AENEAS_ENV; or use run_bare.sh with a plain lean per lean-toolchain)"; exit 1; }
|
|
source "$AENEAS_ENV"
|
|
HERE="$(cd "$(dirname "$0")" && pwd)"
|
|
AENEAS_LEAN="$AENEAS_HOME/backends/lean"
|
|
TIMEOUT="${LEAN_TIMEOUT:-600}"
|
|
export LEAN_MEM_MB="${LEAN_MEM_MB:-4096}"
|
|
CORES="${LEAN_MAX_CORES:-0-3}"
|
|
|
|
GEN_MODULES=( LTLAcc/HashExternal )
|
|
PROOFS=( Basic Completeness Extract Descent Consistency Binding3 Refactor Theorem3 PinStore )
|
|
|
|
# Certificates and their exact expected cones (observed via #print axioms,
|
|
# never guessed; any drift in EITHER direction is a failure).
|
|
# AUDIT SURFACE: Phase 3b pins the FULL environment of the corpus modules
|
|
# (inventory-allowlist.txt, every compiler-generated auxiliary included —
|
|
# the count is pinned by the allowlist itself and asserted against the
|
|
# docs in Phase 3c); the entries below are the human-reviewed statement
|
|
# surface, additionally queried through #print axioms in Phase 3 and
|
|
# cross-checked against the inventory's independently computed cones.
|
|
declare -A CONES=(
|
|
[LTLAcc.domsep]=""
|
|
[LTLAcc.kbelow_pos]="propext, Quot.sound"
|
|
[LTLAcc.kbelow_lt]="propext, Quot.sound"
|
|
[LTLAcc.le_two_kbelow]="propext, Quot.sound"
|
|
[LTLAcc.kbelow_pow2]="propext, Quot.sound"
|
|
[LTLAcc.MTH]="propext, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.Root]="propext, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.ConsRec]="propext, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.Path]="propext, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.incl_complete]="propext, Classical.choice, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.hnode_preimage_inj]="propext"
|
|
[LTLAcc.IsCollision]="LTLAcc.sha256"
|
|
[LTLAcc.extractIncl]="propext, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.extractIncl_correct]="propext, Classical.choice, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.extractIncl_nonvacuous]="propext, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.extractMTH]="propext, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.extractMTH_correct]="propext, Classical.choice, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.extractMTH_nonvacuous]="propext, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.kbelow_prefix_eq]="propext, Quot.sound"
|
|
[LTLAcc.take_take_le]="propext, Quot.sound"
|
|
[LTLAcc.take_drop_prefix]="propext, Classical.choice, Quot.sound"
|
|
[LTLAcc.extractConsNode]="propext, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.take_all]="propext"
|
|
[LTLAcc.consRecBinding]="propext, Classical.choice, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.consRec_base_false_eq]="propext, Classical.choice, Quot.sound"
|
|
[LTLAcc.consRec_base_true_eq]="propext"
|
|
[LTLAcc.extractCons]="propext, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.extractCons_correct]="propext, Classical.choice, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.extractCons_nonvacuous]="propext, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.pinAccept_monotone]="propext, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.pin_prefix_correct]="propext, Classical.choice, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.fork_distinct]="propext, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.pin_prefix_nonvacuous]="propext, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.MTH_single]="propext, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.MTH_split]="propext, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.Root_left]="propext, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.Root_one]="propext, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.Root_one_cons]="propext, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.Root_right]="propext, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.acceptCons]="propext, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.exists_singleton_of_length_one]="propext, Classical.choice, Quot.sound"
|
|
[LTLAcc.getD_drop]="propext, Quot.sound"
|
|
[LTLAcc.getD_take]="propext, Quot.sound"
|
|
[LTLAcc.hleaf]="LTLAcc.sha256"
|
|
[LTLAcc.hnode]="LTLAcc.sha256"
|
|
[LTLAcc.kbelow]="propext, Quot.sound"
|
|
[LTLAcc.kbelow_eq_of_pow2_between]="propext, Quot.sound"
|
|
[LTLAcc.pinAccept]="propext, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.pinExtract]="propext, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.pow2_exp_unique]="propext, Quot.sound"
|
|
[LTLAcc.take_append_drop]=""
|
|
[LTLAcc.eq_dropLast_append_of_getLast?]="propext"
|
|
[LTLAcc.instInhabitedHash]="propext"
|
|
[LTLAcc.instDecidableEqHash]=""
|
|
[LTLAcc.Hash]=""
|
|
[LTLAcc.acceptIncl]="propext, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.acceptIncl_complete]="propext, Classical.choice, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.acceptIncl_sound]="propext, Classical.choice, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.extractCons_correct_paper]="propext, Classical.choice, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.consRec_some_le]="propext, LTLAcc.sha256, Quot.sound"
|
|
[LTLAcc.acceptCons_sound]="propext, Classical.choice, LTLAcc.sha256, Quot.sound"
|
|
)
|
|
|
|
# (The former EXCLUDE table is gone: since Phase 3b reads the environment,
|
|
# sha256 and Bytes are ordinary allowlist entries — the axiom is pinned as
|
|
# the SINGLE axiom-kind constant, the abbrev carries its empty cone.)
|
|
|
|
free -m | awk '/Mem:/{if($7<2048){print "FATAL: <2GB RAM available — refusing to compile"; exit 1}}'
|
|
echo "=== Phase 0: source integrity ==="
|
|
for f in "$HERE"/gen/LTLAcc/*.lean "$HERE"/Proofs/*.lean; do
|
|
[ -f "$f" ] || continue
|
|
if ! grep -qE '^(/-|import |namespace |theorem |def |noncomputable |open |set_option |--|abbrev )' "$f"; then
|
|
echo "CORRUPTED: $f is not Lean source. Restore: git checkout HEAD -- $f"; exit 1
|
|
fi
|
|
done
|
|
echo " all sources valid"
|
|
# Recursive: no compiled artifact anywhere in the tree may lack its source
|
|
# (review round 2, GPT M1 — previously scanned Proofs/*.olean only).
|
|
while IFS= read -r -d '' o; do
|
|
[ -f "${o%.olean}.lean" ] || { echo "ORPHAN OLEAN: $o has no sibling .lean (stale artifact)"; exit 1; }
|
|
done < <(find "$HERE" -name '*.olean' -print0)
|
|
|
|
echo "=== Phase 1: stub + axiom-smuggling audit ==="
|
|
if grep -rn 'by trivial' "$HERE"/Proofs/*.lean 2>/dev/null; then
|
|
echo "STUB DETECTED"; exit 1; fi
|
|
if grep -rn ' : True :=' "$HERE"/Proofs/*.lean 2>/dev/null; then
|
|
echo "STUB DETECTED: True-target theorem"; exit 1; fi
|
|
if grep -rnE '^(private |protected |noncomputable )*axiom ' "$HERE"/Proofs/*.lean 2>/dev/null; then
|
|
echo "AXIOM SMUGGLING DETECTED: axiom under Proofs/ — gen/ is the only sanctioned site."; exit 1
|
|
fi
|
|
# gen/ is the sanctioned site for exactly ONE axiom (review round 2, GPT M1).
|
|
# This textual pin is the fast belt; the semantic guarantee is Phase 3b's
|
|
# environment inventory (exactly one axiom-kind constant, LTLAcc.sha256).
|
|
AXCOUNT=$(grep -hcE '^(private |protected |noncomputable )*axiom ' "$HERE"/gen/LTLAcc/*.lean | paste -sd+ - | bc)
|
|
[ "$AXCOUNT" = 1 ] || { echo "AXIOM COUNT DRIFT: gen/ declares $AXCOUNT axioms, sanctioned: 1 (sha256)"; exit 1; }
|
|
echo " clean"
|
|
|
|
echo "=== Phase 2: compile ==="
|
|
LOG=$(mktemp /tmp/acc-check-XXXX.log)
|
|
cd "$AENEAS_LEAN"
|
|
lake env bash -c "
|
|
set -euo pipefail
|
|
cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
|
|
compile() {
|
|
echo \" · \$1\"
|
|
LEAN_TIMEOUT=$TIMEOUT LEAN_MAX_CORES=$CORES '$HERE/lean-guard' \"\${1}.lean\" 2>&1 | tee -a '$LOG' || { echo \"FAIL: \$1\"; exit 1; }
|
|
}
|
|
for m in ${GEN_MODULES[*]}; do compile \"\$m\"; done
|
|
cd '$HERE'
|
|
for m in ${PROOFS[*]}; do
|
|
[ -f \"Proofs/\$m.lean\" ] || { echo \"MISSING: Proofs/\$m.lean\"; exit 1; }
|
|
compile \"Proofs/\$m\"
|
|
done
|
|
for f in Proofs/*.lean; do
|
|
b=\$(basename \"\$f\" .lean)
|
|
[ \"\$b\" = AxiomCheck ] && continue # audit infrastructure, compiled in Phase 3
|
|
[ \"\$b\" = Inventory ] && continue # audit infrastructure, compiled in Phase 3b
|
|
case \" ${PROOFS[*]} \" in (*\" \$b \"*) ;; (*) echo \"DEAD FILE: \$f\"; exit 1;; esac
|
|
done
|
|
# gen/ gets the same unmanifested-source check (review round 2, GPT M1)
|
|
for f in gen/LTLAcc/*.lean; do
|
|
b=\"LTLAcc/\$(basename \"\$f\" .lean)\"
|
|
case \" ${GEN_MODULES[*]} \" in (*\" \$b \"*) ;; (*) echo \"DEAD FILE (gen): \$f\"; exit 1;; esac
|
|
done
|
|
"
|
|
if grep -q "uses 'sorry'" "$LOG"; then echo "STUB: sorry detected"; exit 1; fi
|
|
rm -f "$LOG"
|
|
|
|
echo "=== Phase 3: boundary-exact axiom audit ==="
|
|
AUD=$(mktemp /tmp/acc-audit-XXXX.log)
|
|
cd "$AENEAS_LEAN"
|
|
lake env bash -c "
|
|
cd '$HERE' && export LEAN_PATH=\"\$LEAN_PATH:$HERE/gen:$HERE\"
|
|
LEAN_TIMEOUT=300 LEAN_MAX_CORES=$CORES '$HERE/lean-guard' Proofs/AxiomCheck.lean
|
|
" > "$AUD" 2>&1 || { cat "$AUD"; exit 1; }
|
|
FAIL=0
|
|
for cert in "${!CONES[@]}"; do
|
|
want="${CONES[$cert]}"
|
|
if [ -z "$want" ]; then
|
|
exp="'$cert' does not depend on any axioms"
|
|
else
|
|
exp="'$cert' depends on axioms: [$want]"
|
|
fi
|
|
if ! grep -qF "$exp" "$AUD"; then
|
|
echo " CONE DRIFT: $cert"
|
|
echo " expected: $exp"
|
|
echo " observed: $(grep -F "'$cert'" "$AUD" || echo '(missing)')"
|
|
FAIL=1
|
|
else
|
|
echo " ✓ $cert [$want]"
|
|
fi
|
|
done
|
|
rm -f "$AUD"
|
|
|
|
# -- Phase 3b: ENVIRONMENT-derived audit-surface coverage (fail-closed) ------
|
|
# Review round 2 (GPT H1 / Claude NEW-1): the previous source-regex
|
|
# enumerator was evadable (attributes, indentation, private/protected,
|
|
# instance, and namespace-nested basename collisions). Replaced entirely:
|
|
# Proofs/Inventory.lean reads the compiled Lean ENVIRONMENT and emits every
|
|
# constant of every corpus module — fully qualified, unfiltered, each with
|
|
# kind and axiom cone (its own walker, cross-checked in-process against
|
|
# core collectAxioms). inventory_gate.sh diffs that against the pinned
|
|
# allowlist, fail-closed BOTH directions. No name shape can hide: what the
|
|
# kernel saw is what gets audited.
|
|
echo "=== Phase 3b: environment-derived audit-surface coverage ==="
|
|
COVFAIL=0
|
|
INVLOG=$(mktemp /tmp/acc-inv-XXXX.log)
|
|
cd "$AENEAS_LEAN"
|
|
lake env bash -c "
|
|
cd '$HERE' && export LEAN_PATH=\"\$LEAN_PATH:$HERE/gen:$HERE\"
|
|
LEAN_TIMEOUT=600 LEAN_MAX_CORES=$CORES '$HERE/lean-guard' Proofs/Inventory.lean
|
|
" > "$INVLOG" 2>&1 || { cat "$INVLOG"; echo "INVENTORY COMPILE FAILED"; exit 1; }
|
|
"$HERE/inventory_gate.sh" "$INVLOG" "$HERE/inventory-allowlist.txt" || COVFAIL=1
|
|
|
|
# The inventory's corpus-module list must BE the compile manifest — both
|
|
# directions, so neither can drift from the other silently.
|
|
for m in "${GEN_MODULES[@]}" "${PROOFS[@]}"; do
|
|
mod=$(echo "$m" | sed 's|^LTLAcc/|LTLAcc.|; s|^\([A-Z]\)|Proofs.\1|; s|^Proofs\.LTLAcc\.|LTLAcc.|')
|
|
grep -qF "\`$mod" "$HERE/Proofs/Inventory.lean" || {
|
|
echo " MANIFEST DRIFT: $mod compiled by check.sh but not inventoried"; COVFAIL=1; }
|
|
done
|
|
NMANIFEST=$(( ${#GEN_MODULES[@]} + ${#PROOFS[@]} ))
|
|
NINV=$(grep -oE '`(LTLAcc|Proofs)\.[A-Za-z0-9_.]+' "$HERE/Proofs/Inventory.lean" | wc -l)
|
|
[ "$NMANIFEST" = "$NINV" ] || {
|
|
echo " MANIFEST DRIFT: check.sh compiles $NMANIFEST modules, Inventory lists $NINV"; COVFAIL=1; }
|
|
|
|
# CONES ⊆ allowlist with IDENTICAL cones: the #print-axioms-pinned table
|
|
# and the environment inventory are two independent computations of the
|
|
# same facts — any disagreement is a failure of one of them.
|
|
# (cones are compared as SETS: CONES keeps #print-axioms order, the
|
|
# inventory emits byte-sorted order — canonicalize both before comparing)
|
|
canon() { tr -d ' ' <<<"$1" | tr ',' '\n' | LC_ALL=C sort | paste -sd, -; }
|
|
while IFS='|' read -r _ name _ cone; do
|
|
if [ -n "${CONES[$name]+x}" ]; then
|
|
want=$(canon "${CONES[$name]}")
|
|
got=$(canon "$cone")
|
|
[ "$want" = "$got" ] || {
|
|
echo " CONE CROSS-CHECK FAILED: $name CONES=[$want] inventory=[$got]"; COVFAIL=1; }
|
|
fi
|
|
done < <(grep '^INV|' "$HERE/inventory-allowlist.txt")
|
|
# (field-equality, not regex — dots in names must not act as wildcards;
|
|
# review round 3, F4)
|
|
for cert in "${!CONES[@]}"; do
|
|
awk -F'|' -v n="$cert" '$1=="INV" && $2==n {found=1} END {exit !found}' \
|
|
"$HERE/inventory-allowlist.txt" || {
|
|
echo " PINNED BUT NOT INVENTORIED: $cert (in CONES, not in allowlist)"; COVFAIL=1; }
|
|
done
|
|
# (INVLOG is NOT removed here: Phase 3d binds the statement block emitted by
|
|
# this same run. Removed at the end of 3d.)
|
|
|
|
# every pinned cert must actually be queried by AxiomCheck (no pin-but-never-check)
|
|
for cert in "${!CONES[@]}"; do
|
|
grep -qF "#print axioms $cert" "$HERE/Proofs/AxiomCheck.lean" || {
|
|
echo " PINNED BUT NOT QUERIED: $cert (in CONES, absent from AxiomCheck.lean)"; COVFAIL=1; }
|
|
done
|
|
[ "$COVFAIL" = 0 ] && echo " coverage complete: environment == allowlist, CONES cross-checked"
|
|
[ "$COVFAIL" = 0 ] || { echo "COVERAGE FAILED"; FAIL=1; }
|
|
[ "$FAIL" = 0 ] || exit 1
|
|
|
|
# -- Phase 3c: documentation consistency (review R4-1: hand-maintained ------
|
|
# counts went stale three rounds running — so the docs' numbers are now
|
|
# ASSERTED against their sources: allowlist, CONES, and the fidelity pins.
|
|
echo "=== Phase 3c: doc-consistency ==="
|
|
DOCFAIL=0
|
|
NALLOW=$(grep -c '^INV|' "$HERE/inventory-allowlist.txt")
|
|
NCONES=${#CONES[@]}
|
|
SMAP="$HERE/../STATEMENT-MAP.md"
|
|
RDME="$HERE/../README.md"
|
|
grep -qF "$NALLOW constants" "$SMAP" || { echo " DOC DRIFT: STATEMENT-MAP lacks '$NALLOW constants'"; DOCFAIL=1; }
|
|
grep -qF "$NCONES human-reviewed" "$SMAP" || { echo " DOC DRIFT: STATEMENT-MAP lacks '$NCONES human-reviewed'"; DOCFAIL=1; }
|
|
grep -qF "$NALLOW constants" "$RDME" || { echo " DOC DRIFT: README lacks '$NALLOW constants'"; DOCFAIL=1; }
|
|
grep -qF "$NCONES human-reviewed" "$RDME" || { echo " DOC DRIFT: README lacks '$NCONES human-reviewed'"; DOCFAIL=1; }
|
|
# fidelity pins quoted in the docs must equal the harness's pinned constants
|
|
for n in $(python3 -c "
|
|
import re
|
|
src = open('$HERE/fidelity/run_fidelity.py').read()
|
|
vals = [re.search(r'assert ti == ([0-9_]+)', src).group(1),
|
|
re.search(r'assert tc == ([0-9_]+)', src).group(1),
|
|
re.search(r'LIED_PIN_TOTAL = ([0-9_]+)', src).group(1),
|
|
re.search(r'LIED_PIN_DIV = ([0-9_]+)', src).group(1)]
|
|
print(' '.join(f'{int(v.replace(chr(95),\"\")):,}' for v in vals))"); do
|
|
grep -qF "$n" "$SMAP" || { echo " DOC DRIFT: STATEMENT-MAP lacks fidelity pin '$n'"; DOCFAIL=1; }
|
|
done
|
|
[ "$DOCFAIL" = 0 ] && echo " docs agree with allowlist ($NALLOW), CONES ($NCONES), fidelity pins"
|
|
[ "$DOCFAIL" = 0 ] || { echo "DOC-CONSISTENCY FAILED"; exit 1; }
|
|
# -- Phase 3d: statement + specification binding (P1-a) ---------------------
|
|
# WHAT PHASES 3/3b DO NOT ESTABLISH. Phase 3 pins each certificate's exact
|
|
# axiom cone; Phase 3b pins the full environment surface, kind and cone, both
|
|
# directions. Neither records what a declaration SAYS. A theorem gutted to a
|
|
# tautology keeps its name, its kind and its cone. A `def` redefined to BE the
|
|
# thing it was meant to specify keeps all three, and every certificate stated
|
|
# against it silently becomes vacuous — with the allowlist unmoved.
|
|
#
|
|
# Proofs/Inventory.lean therefore also emits, for every inventoried constant,
|
|
# its fully-elaborated TYPE, and for every definition its fully-elaborated
|
|
# BODY. Proof terms are deliberately absent: by proof irrelevance a theorem's
|
|
# content is its statement. This phase binds the SHA-256 of that block, and
|
|
# the block itself is committed as AUDIT-MANIFEST.txt so a mismatch is DIFFED
|
|
# rather than merely reported.
|
|
#
|
|
# To rotate deliberately: run check.sh, take the printed OBSERVED digest, and
|
|
# update the constant below AND AUDIT-MANIFEST.txt in the same reviewable
|
|
# commit. Visibility in review is the defence; no harness audits its author.
|
|
EXPECTED_STMT_SHA256="e7d422f0be9a9e6f5465058292e30c711d52856428da2b01c470a57ec181540c"
|
|
echo "=== Phase 3d: statement + specification binding ==="
|
|
STMTFAIL=0
|
|
STMT_BLOCK=$(awk '/^STMT-BEGIN/{f=1;next} /^STMT-END/{f=0} f' "$INVLOG")
|
|
# FAIL CLOSED ON ABSENCE: no block and a matching block must not share a path.
|
|
if [ -z "$STMT_BLOCK" ]; then
|
|
echo " NO STATEMENT BLOCK emitted by Proofs/Inventory.lean (fail-closed)"; STMTFAIL=1
|
|
else
|
|
# Output integrity, same discipline as the INV-COUNT trailer: a truncated or
|
|
# crashed run must not pass as a short-but-matching block.
|
|
N_STMT=$(printf '%s\n' "$STMT_BLOCK" | grep -c '^STMT|')
|
|
STMT_TRAILER=$(grep '^STMT-COUNT|' "$INVLOG" | tail -1 | cut -d'|' -f2)
|
|
if [ -z "$STMT_TRAILER" ] || [ "$STMT_TRAILER" != "$N_STMT" ]; then
|
|
echo " STATEMENT BLOCK TRUNCATED: trailer=${STMT_TRAILER:-absent}, observed $N_STMT"; STMTFAIL=1
|
|
fi
|
|
# Every inventoried constant must carry a statement line. Inventory.lean
|
|
# asserts this internally too; asserting it here as well means a tampered
|
|
# Inventory.lean cannot simply drop its own check.
|
|
N_INV=$(grep -c '^INV|' "$INVLOG")
|
|
N_TYPES=$(printf '%s\n' "$STMT_BLOCK" | grep -c '|type=')
|
|
if [ "$N_TYPES" != "$N_INV" ]; then
|
|
echo " STATEMENT COVERAGE GAP: $N_INV constants inventoried, $N_TYPES carry a statement"; STMTFAIL=1
|
|
fi
|
|
GOT_STMT_SHA=$(printf '%s\n' "$STMT_BLOCK" | sha256sum | cut -d' ' -f1)
|
|
if [ "$GOT_STMT_SHA" != "$EXPECTED_STMT_SHA256" ]; then
|
|
printf '%s\n' "$STMT_BLOCK" > "$HERE/.stmt-manifest.observed"
|
|
echo " STATEMENT DIGEST MISMATCH."
|
|
echo " expected: $EXPECTED_STMT_SHA256"
|
|
echo " observed: $GOT_STMT_SHA"
|
|
echo " A statement or a definition body changed. First differences:"
|
|
diff -u "$HERE/AUDIT-MANIFEST.txt" "$HERE/.stmt-manifest.observed" 2>/dev/null \
|
|
| head -30 | sed 's/^/ /' || echo " (AUDIT-MANIFEST.txt absent — cannot diff)"
|
|
rm -f "$HERE/.stmt-manifest.observed"
|
|
STMTFAIL=1
|
|
elif ! printf '%s\n' "$STMT_BLOCK" | cmp -s - "$HERE/AUDIT-MANIFEST.txt"; then
|
|
# The digest's INPUT must be committed and current, or the diff above would
|
|
# compare against a stale reference and quietly mislead the next reader.
|
|
echo " COMMITTED BLOCK STALE: AUDIT-MANIFEST.txt does not match the emitted block"
|
|
echo " (the digest matched, so the committed copy needs refreshing)"; STMTFAIL=1
|
|
fi
|
|
fi
|
|
[ "$STMTFAIL" = 0 ] && echo " statements bound: $N_STMT lines over $N_INV constants, sha256 = $GOT_STMT_SHA"
|
|
[ "$STMTFAIL" = 0 ] || { echo "STATEMENT BINDING FAILED"; rm -f "$INVLOG"; exit 1; }
|
|
rm -f "$INVLOG"
|
|
|
|
# -- Phase 4: definition fidelity (Lean defs vs deployed pacta verifiers) --
|
|
echo "=== Phase 4: definition fidelity ==="
|
|
PACTA_SRC="${PACTA_SRC:-$HERE/../../proof-aware-crypto-tooling-agent/src}"
|
|
FIDELITY_RAN=0
|
|
if [ "${SKIP_FIDELITY:-0}" = "1" ]; then
|
|
echo " skipped (SKIP_FIDELITY=1)"
|
|
elif [ -d "$PACTA_SRC/pacta" ]; then
|
|
PACTA_SRC="$PACTA_SRC" python3 "$HERE/fidelity/run_fidelity.py" || { echo "FIDELITY FAILED"; exit 1; }
|
|
FIDELITY_RAN=1
|
|
else
|
|
echo " SKIPPED: pacta repo not found at $PACTA_SRC (set PACTA_SRC to run)"
|
|
fi
|
|
|
|
# Fail-closed markers (review H2): the Lean corpus is green either way, but
|
|
# only the strong marker — required by the attestation gate — is emitted
|
|
# when fidelity actually ran. Never conflate the two.
|
|
echo "=== LEAN GREEN ==="
|
|
if [ "$FIDELITY_RAN" = 1 ]; then
|
|
echo "=== ATTESTATION GREEN (Lean + fidelity) ==="
|
|
else
|
|
echo "=== FIDELITY NOT RUN — NOT attestation-ready (run with pacta present) ==="
|
|
fi
|