diff --git a/verification/HARNESS.sha256 b/verification/HARNESS.sha256 index 02eb375..74e173e 100644 --- a/verification/HARNESS.sha256 +++ b/verification/HARNESS.sha256 @@ -1,12 +1,14 @@ e7d422f0be9a9e6f5465058292e30c711d52856428da2b01c470a57ec181540c AUDIT-MANIFEST.txt -857a92d50d44c5fe4db2bfdb4fc3a28f7b345b369414a140a66298fd6ff1b0fe check.sh +29b20810b6d365d8aa0b1affbbd4e3a38f03f302eb839d10a314e94a60b46da7 check.sh 070147e2667053bd5d5e1174b969fc6c91bfcf15ded1a5bff57754e15f416885 fidelity/lean_defs.py +9661bc2d33e907453ab4378da918589a709127b2e117ef1fd578d4e0472edf87 fidelity/pacta_pin.py 5d82462a002ac9fc782e95afe78b7719ba64b6410b5d2bfa620fe5317367dbf2 fidelity/run_fidelity.py 503babb3f4e6aff82ebd59e8752469ecd60fba440ed3b11b3f97c2b655fbd9bf gen/LTLAcc/HashExternal.lean f1eb5cdd158e30df14c59065fe2050448c77b5262b282208fa831d050f6b6a71 inventory-allowlist.txt f66fb98d2a09503d9bd0d60dc964545eea6dc94b9bbb9246d1021195b79f2601 inventory_gate.sh 736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard ce4c4e3d87434b9663f46de25ce34b48a0cf0d392e0a320a0787b4674a2d7b61 lean-toolchain +6f39303b336aedc4da8381712de8180282e39c0725226c292fce15b47f9beb88 PACTA-PIN.sha256 eda93f520546a692926b2a46bcb79332e1795879e5083327a8bf2404aca5cf87 Proofs/AxiomCheck.lean de5cdf01724fd4333b0652769bfede3ee150fedfa0a6c4ffbc8e7ab065843928 Proofs/Inventory.lean 0b8a0fc6947af1d1e600a756eb2b07dc88d189b21df3220c4501a41be8b33f1e run_bare.sh diff --git a/verification/PACTA-PIN.sha256 b/verification/PACTA-PIN.sha256 new file mode 100644 index 0000000..9136add --- /dev/null +++ b/verification/PACTA-PIN.sha256 @@ -0,0 +1,8 @@ +# pacta subject pinned by fidelity/pacta_pin.py --write +# commit cd3b1bc92198f74b430b8fbd99c1ede1deb22988 +# 5 module(s), discovered by import, not by glob +a1bcc5d700071f531e6fe16989884412cb3fb0f2702adfdf5212d4bc84eba2bc pacta/__init__.py +31dd6ab7b3121a433c7c8b082ec2d011d1958782470481137db0513a9822532d pacta/postquantum.py +4dc1e5ae52519dea989460abe8296a3ea93cd177673a01dc22a8efc71311af56 pacta/signing.py +067332363d1014577619b958adeffb7ee168759855f21fd35f639b473cc7d511 pacta/transparency.py +7130d5a770db7af4d294389625cf5f0c4228ed562b78bd7ca148ca010087d834 pacta/yamlio.py diff --git a/verification/check.sh b/verification/check.sh index bee6e8b..2257653 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -165,6 +165,11 @@ HARNESS_EXTRA=( lean-toolchain # which Lean the corpus claims to have been checked by fidelity/lean_defs.py # the Python transcription the differential compares fidelity/run_fidelity.py # the differential itself + PACTA-PIN.sha256 # WHICH pacta the differential is entitled to compare + # against. Pinned here because it is not executable + # and would otherwise sit outside the harness set — + # a subject pin an attacker may rewrite pins nothing, + # the same shape as a forgeable .audit-basis. Proofs/Inventory.lean # audit driver: emits the inventory AND the statements Proofs/AxiomCheck.lean # audit driver: the #print axioms queries of Phase 3 ) @@ -599,18 +604,61 @@ FIDELITY_RAN=0 if [ "${SKIP_FIDELITY:-0}" = "1" ]; then echo " skipped (SKIP_FIDELITY=1)" elif [ -d "$PACTA_SRC/pacta" ]; then + # PIN THE SUBJECT BEFORE COMPARING AGAINST IT (round-8 review, GPT-5.6, + # register key `pacta-subject-unpinned`). This phase used to import whatever + # sat at $PACTA_SRC: no repository, no commit, no clean state, no hashes. It + # pinned the fidelity OUTPUTS while leaving the SUBJECT anonymous, so any + # program producing the same finite family of answers passed and the recorded + # result named no version of the thing it agreed with. Agreement with an + # unnamed program is not evidence about a deployed one. + PACTA_SRC="$PACTA_SRC" python3 "$HERE/fidelity/pacta_pin.py" --verify \ + || { echo "FIDELITY FAILED — the pacta subject is not the pinned one."; exit 1; } 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. +# Fail-closed markers AND A FAIL-CLOSED EXIT CODE (round-7 review: raised +# independently by both reviewers — Claude F1, GPT-5.6 F10; register key +# `acc-exit0-fidelity`). +# +# Until now this emitted the weak marker and RETURNED 0. The marker discipline +# was right and the exit code contradicted it: a caller doing the obvious thing +# +# ./check.sh && append +# +# read success from a run whose own last line says NOT attestation-ready. And +# because pacta is not part of this estate, the skip branch is the ONLY branch +# any third party ever takes — so for everyone but the author, the button +# always returned 0 without ever checking definition fidelity. A procedure of +# the form "run the button, then append" was unsound for this component. +# +# An exit code is what programs read. If the button cannot establish +# attestation-readiness it must not return success, whatever it prints. +# +# fidelity ran -> ATTESTATION GREEN, exit 0 +# SKIP_FIDELITY=1 -> exit 3: the caller opted out EXPLICITLY, so the +# code is distinguishable, but it is not 0 +# pacta absent -> exit 1: nobody opted out; this is a real failure +# to establish the property the button exists for +# +# The self-tests are unaffected: every SKIP_FIDELITY=1 case already expects a +# non-zero exit and asserts on a diagnostic from an earlier phase, and the +# control case compiles modules directly rather than invoking this script. echo "=== LEAN GREEN ===" if [ "$FIDELITY_RAN" = 1 ]; then echo "=== ATTESTATION GREEN (Lean + fidelity) ===" +elif [ "${SKIP_FIDELITY:-0}" = "1" ]; then + echo "=== FIDELITY SKIPPED ON REQUEST — NOT attestation-ready (exit 3) ===" + echo " The Lean corpus is green. Definition fidelity against the deployed" + echo " verifier was not checked, so this run does NOT certify that this" + echo " repository may be attested." + exit 3 else - echo "=== FIDELITY NOT RUN — NOT attestation-ready (run with pacta present) ===" + echo "=== FIDELITY NOT RUN — NOT attestation-ready (exit 1) ===" + echo " pacta was not found at: $PACTA_SRC" + echo " Set PACTA_SRC to a pacta checkout and re-run, or pass" + echo " SKIP_FIDELITY=1 to acknowledge deliberately skipping it (exit 3)." + exit 1 fi diff --git a/verification/fidelity/pacta_pin.py b/verification/fidelity/pacta_pin.py new file mode 100755 index 0000000..fc70cbc --- /dev/null +++ b/verification/fidelity/pacta_pin.py @@ -0,0 +1,159 @@ +#!/usr/bin/env python3 +"""Pin the pacta sources the fidelity harness actually consumes. + + pacta_pin.py --write # regenerate PACTA-PIN.sha256 (deliberate act) + pacta_pin.py --verify # check the subject; exit 1 on any drift + +───────────────────────────────────────────────────────────────────────────── +WHY THIS EXISTS — round-8 review (GPT-5.6, register key `pacta-subject-unpinned`) + +Phase 4 compares this repository's Lean definitions against the DEPLOYED +verifier. It did so by putting `$PACTA_SRC` on `sys.path` and importing +`pacta.transparency` — whatever happened to be there. No repository URL, no +commit, no clean-state check, no source hashes. + +So the fidelity counts pinned OUTPUTS while the SUBJECT was unpinned. Any +implementation producing the same finite family of answers passed, and the +recorded result named no version of the thing it agreed with. The reviewer's +zero-divergence run was specifically against pacta `cd3b1bc…` — because the +reviewer selected and recorded that checkout, not because the button required +it. + +A proof about a model is not evidence about an unnamed program. + +WHAT IS PINNED, AND WHY IT IS NOT A GLOB. The pin covers the transitive set of +pacta modules the harness ACTUALLY LOADS, discovered by importing the harness's +entry point and reading `sys.modules` — a membership property, not a directory +listing. Globbing `pacta/*.py` would pin files the comparison never touches +(noise that breaks the pin for unrelated edits) and would miss anything loaded +from outside that directory. The estate has been bitten by name-shaped +measurement before; this is the same error class. + +WHAT THIS DOES NOT ESTABLISH. Byte identity of a source tree is not proof that +the deployed service runs it, and finite-family agreement is not extensional +equality. This pin names the subject; it does not widen the claim. +───────────────────────────────────────────────────────────────────────────── +""" +import hashlib +import os +import subprocess +import sys + +HERE = os.path.dirname(os.path.abspath(__file__)) +VERIF = os.path.dirname(HERE) +PIN = os.path.join(VERIF, 'PACTA-PIN.sha256') +PACTA_SRC = os.environ.get( + 'PACTA_SRC', os.path.join(VERIF, '..', '..', + 'proof-aware-crypto-tooling-agent', 'src')) +PACTA_SRC = os.path.abspath(PACTA_SRC) + + +def loaded_sources(): + """{path relative to PACTA_SRC: sha256} for every pacta module imported. + + Imports the same entry point the fidelity harness does, then keeps the + modules whose file lives under PACTA_SRC. That is the consumed set by + construction: if the harness stops using a module, it leaves the pin; if it + starts using one, the pin fails until someone regenerates it deliberately. + """ + sys.path.insert(0, PACTA_SRC) + try: + import pacta.transparency # noqa: F401 + except Exception as e: # pragma: no cover + print(f'PACTA PIN: cannot import pacta.transparency from {PACTA_SRC}:' + f' {e}', file=sys.stderr) + raise SystemExit(1) + + out = {} + for mod in list(sys.modules.values()): + f = getattr(mod, '__file__', None) + if not f: + continue + f = os.path.abspath(f) + if not f.startswith(PACTA_SRC + os.sep) or not f.endswith('.py'): + continue + with open(f, 'rb') as fh: + out[os.path.relpath(f, PACTA_SRC)] = hashlib.sha256( + fh.read()).hexdigest() + return out + + +def head_commit(): + """The pacta commit, for the record. NOT the enforcement — hashes are.""" + try: + r = subprocess.run(['git', '-C', PACTA_SRC, 'rev-parse', 'HEAD'], + capture_output=True, text=True, timeout=10) + c = r.stdout.strip() if r.returncode == 0 else 'unknown' + d = subprocess.run(['git', '-C', PACTA_SRC, 'status', '--porcelain'], + capture_output=True, text=True, timeout=10) + dirty = bool(d.stdout.strip()) if d.returncode == 0 else True + return c, dirty + except Exception: # pragma: no cover + return 'unknown', True + + +def write(): + got = loaded_sources() + commit, dirty = head_commit() + if dirty: + print('PACTA PIN: refusing to pin a DIRTY pacta working tree.' + ' Commit or stash first — a pin taken over uncommitted edits' + ' names a subject nobody else can obtain.', file=sys.stderr) + raise SystemExit(1) + with open(PIN, 'w', encoding='utf-8') as fh: + fh.write(f'# pacta subject pinned by fidelity/pacta_pin.py --write\n') + fh.write(f'# commit {commit}\n') + fh.write(f'# {len(got)} module(s), discovered by import, not by glob\n') + for rel in sorted(got): + fh.write(f'{got[rel]} {rel}\n') + print(f'PACTA PIN: wrote {len(got)} module(s) at commit {commit[:7]}') + + +def verify(): + if not os.path.exists(PIN): + print('PACTA PIN: PACTA-PIN.sha256 is missing — the fidelity subject' + ' is unpinned. Refusing to certify agreement with an unnamed' + ' program.', file=sys.stderr) + return 1 + want = {} + commit = 'unknown' + for line in open(PIN, encoding='utf-8'): + if line.startswith('# commit '): + commit = line.split()[2] + if line.startswith('#') or not line.strip(): + continue + h, rel = line.rstrip('\n').split(' ', 1) + want[rel] = h + got = loaded_sources() + + bad = [] + for rel in sorted(set(want) | set(got)): + if rel not in got: + bad.append(f' {rel}: pinned but NOT LOADED by the harness') + elif rel not in want: + bad.append(f' {rel}: loaded by the harness but NOT PINNED') + elif want[rel] != got[rel]: + bad.append(f' {rel}: bytes differ from the pin') + if bad: + print('PACTA SUBJECT MISMATCH — the fidelity comparison would be' + ' against a different program than the one pinned:', + file=sys.stderr) + print('\n'.join(bad), file=sys.stderr) + print(f' pinned commit: {commit}', file=sys.stderr) + print(' Re-pin deliberately with fidelity/pacta_pin.py --write' + ' if the new subject is the intended one.', file=sys.stderr) + return 1 + _, dirty = head_commit() + state = ' (WORKING TREE DIRTY)' if dirty else '' + print(f' pacta subject: {len(got)} module(s) match the pin,' + f' commit {commit[:7]}{state}') + return 1 if dirty else 0 + + +if __name__ == '__main__': + if '--write' in sys.argv: + write() + elif '--verify' in sys.argv: + raise SystemExit(verify()) + else: + raise SystemExit(__doc__)