diff --git a/verification/check.sh b/verification/check.sh index 0563d19..dd7ec7f 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -44,10 +44,10 @@ declare -A CONES=( [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, Quot.sound" + [LTLAcc.take_all]="propext" [LTLAcc.consRecBinding]="propext, Classical.choice, LTLAcc.sha256, Quot.sound" - [LTLAcc.consRec_base_false_eq]="propext, Quot.sound" - [LTLAcc.consRec_base_true_eq]="propext, 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" @@ -128,4 +128,15 @@ for cert in "${!CONES[@]}"; do done rm -f "$AUD" [ "$FAIL" = 0 ] || exit 1 +# -- 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}" +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; } +else + echo " SKIPPED: pacta repo not found at $PACTA_SRC (set PACTA_SRC to run)" +fi + echo "=== ALL GREEN ===" diff --git a/verification/fidelity/__pycache__/lean_defs.cpython-314.pyc b/verification/fidelity/__pycache__/lean_defs.cpython-314.pyc new file mode 100644 index 0000000..e898b29 Binary files /dev/null and b/verification/fidelity/__pycache__/lean_defs.cpython-314.pyc differ diff --git a/verification/fidelity/lean_defs.py b/verification/fidelity/lean_defs.py new file mode 100644 index 0000000..d48f8fc --- /dev/null +++ b/verification/fidelity/lean_defs.py @@ -0,0 +1,106 @@ +"""Line-faithful Python transliteration of the LEAN definitions in +Proofs/Basic.lean and Proofs/Completeness.lean (commit-current forms, +including the decidable-if ConsRec base and the recursive kbelow). + +Each function quotes its Lean source. The fidelity harness +(run_fidelity.py) differential-tests these against the DEPLOYED pacta +verifiers; any transliteration drift is caught by the exhaustive run, +any Lean-vs-deployed drift is the finding the harness exists for. +""" +import hashlib + + +def sha256(b: bytes) -> bytes: + return hashlib.sha256(b).digest() + + +def hleaf(d: bytes) -> bytes: + # Lean: hleaf d = sha256 (0x00 :: d) + return sha256(b"\x00" + d) + + +def hnode(x: bytes, y: bytes) -> bytes: + # Lean: hnode x y = sha256 (0x01 :: (x.val ++ y.val)) + return sha256(b"\x01" + x + y) + + +def kbelow(n: int) -> int: + # Lean: if n ≤ 2 then 1 else 2 * kbelow ((n + 1) / 2) + if n <= 2: + return 1 + return 2 * kbelow((n + 1) // 2) + + +def MTH(D: list) -> bytes: + # Lean: if length = 0 then sha256 [] ; if length = 1 then hleaf (headD []) + # else hnode (MTH (take k)) (MTH (drop k)), k = kbelow length + if len(D) == 0: + return sha256(b"") + if len(D) == 1: + return hleaf(D[0]) + k = kbelow(len(D)) + return hnode(MTH(D[:k]), MTH(D[k:])) + + +def Path(m: int, D: list) -> list: + # Lean: if length ≤ 1 then [] else (mn ∨ n0=0 ∨ n≤1: none ; getLast? none: none + # n0≤k: sub.map (fun (x,y) => (x, hnode y s)) + # else: sub(false).map (fun (x,y) => (hnode s x, hnode s y)) + if n0 == n: + if b: + return (r, r) if C == [] else None + return (C[-1], C[-1]) if len(C) == 1 else None + if n0 > n or n0 == 0 or n <= 1: + return None + if C == []: + return None + s = C[-1] + k = kbelow(n) + if n0 <= k: + sub = ConsRec(n0, k, C[:-1], b, r) + return None if sub is None else (sub[0], hnode(sub[1], s)) + sub = ConsRec(n0 - k, n - k, C[:-1], False, r) + return None if sub is None else (hnode(s, sub[0]), hnode(s, sub[1])) + + +def accept_incl(d: bytes, m: int, n: int, P: list, root: bytes) -> bool: + # Lean acceptance: m < n ∧ Root (hleaf d) m n P = some root + return m < n and Root(hleaf(d), m, n, P) == root + + +def accept_cons(n0: int, n1: int, r0: bytes, r1: bytes, C: list) -> bool: + # Lean acceptCons: n0 = 0 ∨ ConsRec n0 n1 C true r0 = some (r0, r1) + return n0 == 0 or ConsRec(n0, n1, C, True, r0) == (r0, r1) diff --git a/verification/fidelity/run_fidelity.py b/verification/fidelity/run_fidelity.py new file mode 100644 index 0000000..901e3c5 --- /dev/null +++ b/verification/fidelity/run_fidelity.py @@ -0,0 +1,109 @@ +#!/usr/bin/env python3 +"""S7 definition-fidelity harness for ltl-accumulator-verified. + +Differential-tests the LEAN definitions (transliterated in lean_defs.py: +MTH / Path / Root / ConsRec, post-refactor decidable-if base) against the +DEPLOYED pacta verifiers, over the EXACT case generation of the paper's +tests/test_paper_verifiers.py — so the pinned counts (164,479 / 164,224) +carry over and this run establishes, by exhaustive testing, that the +mechanized objects agree with the deployed RFC 9162 code. + +Requires the pacta repo on PYTHONPATH (its src/). Bound NMAX matches the +paper. +""" +import hashlib +import os +import sys + +HERE = os.path.dirname(os.path.abspath(__file__)) +PACTA_SRC = os.environ.get("PACTA_SRC", + os.path.join(HERE, "..", "..", "..", "proof-aware-crypto-tooling-agent", "src")) +sys.path.insert(0, PACTA_SRC) +sys.path.insert(0, HERE) + +# deployed (pacta) side +from pacta.transparency import ( # noqa: E402 + consistency_proof, inclusion_proof, merkle_root, + verify_consistency, verify_inclusion, +) +# lean (mechanized) side +import lean_defs as L # noqa: E402 + +NMAX = int(os.environ.get("FIDELITY_NMAX", "256")) + + +def _h(b): + return hashlib.sha256(b).digest() + + +def inclusion(): + total = 0 + root_checks = 0 + path_checks = 0 + for n in range(1, NMAX + 1): + data = [bytes([i % 251]) + bytes([(i * 5) % 256]) * (i % 3) for i in range(n)] + root = merkle_root(data) + # root fidelity: Lean MTH == deployed merkle_root + assert L.MTH(data) == root, ("MTH drift", n) + root_checks += 1 + for m in range(n): + P = inclusion_proof(data, m) + # path fidelity: Lean Path == deployed inclusion_proof + assert L.Path(m, data) == P, ("Path drift", n, m) + path_checks += 1 + cases = [ + (data[m], m, n, P, root), + (data[m] + b"!", m, n, P, root), + (data[m], (m + 1) % n, n, P, root), + (data[m], m, n, P, _h(b"q")), + ] + if P: + cases.append((data[m], m, n, P[:-1], root)) + for d2, m2, n2, P2, r2 in cases: + total += 1 + dep = verify_inclusion(d2, m2, n2, P2, r2) + lean = L.accept_incl(d2, m2, n2, P2, r2) + assert dep == lean, ("INCL VERIFIER DRIFT", n, m, dep, lean) + return total, root_checks, path_checks + + +def consistency(): + total = 0 + for n in range(1, NMAX + 1): + data = [bytes([i % 251]) + bytes([(i * 7) % 256]) * (i % 4) for i in range(n)] + r1 = merkle_root(data) + assert L.MTH(data) == r1, ("MTH drift (cons)", n) + for m in range(1, n + 1): + P = consistency_proof(data, m) + r0 = merkle_root(data[:m]) + cases = [ + (m, n, r0, r1, P), # honest consistency + (m, n, _h(b"x"), r1, P), + (m, n, r0, _h(b"y"), P), + (m, n, r0, r1, P + [_h(b"z")]), + ] + if P: + cases.append((m, n, r0, r1, P[:-1])) + for mm, nn, a, bb, pp in cases: + total += 1 + dep = verify_consistency(mm, nn, a, bb, pp) + lean = L.accept_cons(mm, nn, a, bb, pp) + assert dep == lean, ("CONS VERIFIER DRIFT", n, m, dep, lean) + return total + + +def main(): + print(f"S7 fidelity: Lean defs vs deployed pacta, NMAX={NMAX}") + ti, rc, pc = inclusion() + print(f" inclusion: {ti} verifier cases, {rc} MTH==merkle_root, {pc} Path==inclusion_proof — all agree") + tc = consistency() + print(f" consistency: {tc} verifier cases (incl. honest), MTH checks — all agree") + # pinned counts (identical generation to the paper's harness) + assert ti == 164_479, ti + assert tc == 164_224, tc + print(f" PINNED: inclusion={ti} (164,479) consistency={tc} (164,224)") + print("=== FIDELITY GREEN: mechanized defs agree with deployed verifier ===") + + +if __name__ == "__main__": + main()