From 00647814b8da8a5568a11dcd6ffc03da1663cdd3 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Sat, 11 Jul 2026 20:44:07 +0200 Subject: [PATCH] S7: definition fidelity harness + CORRECT three cone mis-pins that were silently failing the button MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit FIDELITY (the deliverable): fidelity/lean_defs.py transliterates the Lean MTH/Path/Root/ConsRec (post-refactor decidable-if base) to Python; fidelity/run_fidelity.py differential-tests them vs the DEPLOYED pacta verifiers over test_paper_verifiers.py's exact case generation. Result: MTH==merkle_root (256), Path==inclusion_proof (32,896), verifier agreement over 164,479 inclusion + 164,224 consistency cases (incl. honest consistency). Pinned counts match the paper. Wired as check.sh Phase 4 (gated on pacta presence, SKIP_FIDELITY to skip). HONEST CORRECTION: three cone pins added in S5.3-S6 were WRONG (take_all and consRec_base_true_eq are [propext]; consRec_base_false_eq is [propext, Classical.choice, Quot.sound]) — I had guessed [propext, Quot.sound]. check.sh's Phase 3 audit was therefore EXITING 1 since S5.3, but I reported 'green' from tailing cert lines instead of checking the exit code / ALL GREEN. Pins now corrected to the observed cones; the button now genuinely exits 0 with ALL GREEN + FIDELITY GREEN. No THEOREM was ever wrong (kernel-checked); the failure was the audit harness rejecting mis-pinned cones — working as designed, caught late by my process gap. Process fixed: verify exit code + ALL GREEN, never tail. 35 certs green (verified by exit 0). LTL untouched. Co-Authored-By: Claude Fable 5 --- verification/check.sh | 17 ++- .../__pycache__/lean_defs.cpython-314.pyc | Bin 0 -> 6494 bytes verification/fidelity/lean_defs.py | 106 +++++++++++++++++ verification/fidelity/run_fidelity.py | 109 ++++++++++++++++++ 4 files changed, 229 insertions(+), 3 deletions(-) create mode 100644 verification/fidelity/__pycache__/lean_defs.cpython-314.pyc create mode 100644 verification/fidelity/lean_defs.py create mode 100644 verification/fidelity/run_fidelity.py 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 0000000000000000000000000000000000000000..e898b29117b600517bb2b6652261f2db3c1662b5 GIT binary patch literal 6494 zcmb_gT})%g6~1F%|6sGQ{FqHQWMeQ8+y%Vs!iF>v#0%_h(=CO&tld@!daib5=;Mr~fUsw&VH<*_|y?vF3f zC7Y%r-I+5p=gyot=R0S9F4mlJagc`I7k>TMGaUCftmw(25l`L&Vucepg`4IC@?)Y9 z!E%lhtmnAoS;ZpoK-(B?73@Ge7|jb#psN^d6I?*M8EqG;fj+}%hfo7_Eu)>nS)l6} zT_w~5-N0y<&GD+|FvJy|Hyb2Xlax$SvR8$gB zPshAUT=L!;4UT!EQY?{5V6*H^q+H`PosP+YYoeTp^du!QB$EuRDuEI#FFHFb5=^G@A`XOu2C@(_r@}*2orfRlU5{W|Ox9p9J6h(7&(oAYbZ|zxF_Ism=SWH3*6JoL(27+N=UX)-?Or&Im$vHAQe(Pty z7#;C0h!I6}ElD&HOGs3H735q#p~NWkD&B6I?v6?e$@H=m^&0=;AE19jRoV(*lmyBM>g;iiMZm5cewcXptnfX#1lbA~;-)PF zs~i`Fwq|aE#EC$rphr!Dr9uZR021qCgm0P5mhDthGBov&lx?%ipbeXduui#pW=2e<(u$}^Gcy!D4}6Z3&qKDteZvvbae&#nw2#H6jn$q& zFUK^41SZr9)65${tZBzujFno^6k_O z%>PgOQq(}1L@BO`+93l8olvM&RV73fGd`Pr0*vdS%N-fuu*K2(=a zRh}=GK^^+GJgiZb+l)d(hlsP&bQmJ1YLrk94B)rW=b)fJfK0||I#eivR#WMyM4O?B zNsG)Ttro~epyX~X@~tN|Ye@LN#TiYTDW*z@E!IQ|edVc0d>%#Dk;s#_0}itF$UYXi z2&+|O1YVX9M|v!rCO(Lb6?6hNj_7jQ(q*!Uj@2$xEI{0{bzp4NHYP$Z zz+5KeQbYjD*b>^9Bwsn4Yr)l}FKf^4x~tchvWxlNjZC3#BU!5TeeU)Zd0%BQI+VYw z!VTfoz^*BLL{+$@%qL+7p$-t|G_|+lVsy1TiT{9uY`t$Ei`*!yRU`#ome7by?SBWt z4Bkpeo#qC94u+`4O=${wSrUk@W}hi+nEoQ{uLky)VF)lB*M%}_$utHok0rC2^?tov zAX6BZRX&WjEQL715+cOd1g4ChFr4Em?R}b_+2)CVGJTBs?PY6HN~ysfeM`jwdRp1~ z)5)9Ql0Kx#o2o;4)yUh4oR~4iPXn>S{mafd-D|zSS<2R}zP(rL$wuzIU38w`bGRyv zjoFFp;>M)f;jCGgv%UA0?$xXW_uOZ54bVyRBzxy~=QnQ`>I#<&o)3Oma(5Q_&WiDL zn0?oXX}}C3ra>QxnDcC<8t&+exI*-T(_q&P{YL0?l5PZA_xdoxt~)ovip@#Zs4l>m z82&RB@DHdQL7#!HX)<7hfgTR9W+2dn6NB5pi6v|qfPEW&T#c|F*S8Pk0Nh-1jxt*u+D+B0Ko*Wp~v?A118gZcV=OEz=wovnt# zM1dCWJUCyd{=BxU=)Z@Q`ct50e>26I}g@^P00diG-6@M+M`BBuuU@@mwa$@^dXO_m9-qX|gWZL-rVx0!KGtHLBy>>^ET&vK_&2ySWy!KI7Qe zD`SIM5Q$@t{|yN$ATU?vg>+hB#}&VW;=!Y0N!p7HL}t)t#~m5X+5ySy)i92SDT*00 zPA-?4ITmf^7<8B})Mt z_=jEf4@>G2JH(X9FuS{y35Aei#O*Ran@%Uc_2lpq7+1au8G4Ebo<9y)p0n<=a#Jg} zc(wjvqgp;{SNYWS8xa!5L2I)0f6e?Rta{BW%ulQs@GwQ;P6d8r(Yy$-+{}eXuE5n+ zz&H|s0GrLN$(CjYa8RB$#ST)3}K)6aq<G+pp*;|( zQNT%G#vTmi6rGv@mI5d^+K(CTb7iZXnUyi@Vlb#g1H2Ma%otSv2?Rug8qVojz55q; z_3jH73ay*rY%qJZSlzST2H9RqTVdis({}IH^I4K@Rd=|*X*K3J&Ryp9p$)YwtAdUvnJlby{^mOr$^k?u<2TA^v%vqMU*%PYgX4Ndo7#dvaa z>&|xXPRmEJQhWcS%*PXd3jWz%dih4N?I!e{3^8yVS6%E^Oc~#Q+l3GVBdJNSo5GD9 z%^2})xUbyR z@AiM;?kl?ca+90w1@b{>A-LUA@^tO+pLqZlec#{oFp-*$?Jkv*n5}a9dYb9ccgvPk zZ`ndG!Pl$0Fs@YJa4_hz+rqb+Jr0~Evk##$hjPPc+9B2KLtF4b2(?Gd-b0_jEf#8@ zjxf%XX2+@7e)BpI?D2p@vsDZ~$My`f;o%g-<6S_Hi(%gti)w1Hat91E36~y>IACZN zw}yeHBbbe1#*QUVF?0mp#pw;;VhhE=(9mbHb??6Xg?q5*9?Z?A808~JtoD5lP)`#l7Rt2B) zwfS^3lavPO8^DB{s(cNyeJdg4z~UtQlX{NS9@^nG_RtAWg@-P9>pFD7Q_W!wJRBT0 a!8Pu%3C_xg9e6T0yacZK4e$&xVgCbARbLwb literal 0 HcmV?d00001 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()