From f54e47778bad60e9d4f0f7de367be30a0f991290 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Sun, 16 Aug 2026 16:49:44 +0200 Subject: [PATCH] =?UTF-8?q?site:=20the=20socratic=20round=20=E2=80=94=20ev?= =?UTF-8?q?ery=20stale=20claim=20fixed,=20every=20printed=20command=20runs?= =?UTF-8?q?,=20first-use=20glosses?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Operator-found (and root-caused): the v0.11 card replace had silently no-opped on an invisible NBSP in 'vs.\xa0today' — the page said 23 pages and still carried the July-snapshot card one paragraph under the 'New in v0.11' sentence. Fixed by byte-anchored replace with post-assert; a source regression test now forbids the stale markers outright and check-paper.sh binds the page-count claim to pdfinfo. Executability (tested by actually running them): the printed curl had no scheme and returned empty through the redirect -> https form; the zero-install one-liner was missing its cd -> added; 'Standard-library Python only' contradicted the openssl requirement stated 20 lines earlier -> made honest; 'table above' pointed at a table that is below -> below; '~25 lines of Python' vs the 346-line fail-closed verify.py -> 'one-page core (paper Appendix C), shipped verify.py wraps it'. Comprehensibility (fresh-eyes audit, 28 findings triaged): first-use glosses for STH, axiom cones, certificates, pinning, split view, pins.json, trusted base, residual-risk list, R0-R5, signature tiers; Lean 4 linked; Merkle accumulator glossed; operator=provider declared; the ✗-leaves explained as the failed round 1 vs clean re-attest; the flagship self-reference gets a plain lead sentence; TOFU named and bounded; pacta install source at the first pacta command; coined verb 'machine-re-check' uncoined; pitch parenthetical trimmed (SLH detail lives in its own block). Suite 153 green (new: webdocs stale-claim regression test). --- paper/check-paper.sh | 8 +++ paper/ltl.pdf | Bin 219017 -> 219017 bytes provider/src/pacta_provider/webdocs.py | 69 ++++++++++++------------- tests/test_web_and_witness.py | 22 ++++++++ 4 files changed, 64 insertions(+), 35 deletions(-) diff --git a/paper/check-paper.sh b/paper/check-paper.sh index 755fd94..4624af8 100755 --- a/paper/check-paper.sh +++ b/paper/check-paper.sh @@ -69,6 +69,14 @@ VERSION=$(grep -oP '\\date\{[^}]*---\s*\Kv[0-9.]+' ltl.tex || true) pdftotext -f 1 -l 1 ltl.pdf - | grep -q "$VERSION" || fail "title page does not carry $VERSION" ! pdftotext ltl.pdf - | grep -q '??' || fail "unresolved ?? reference in PDF" +# --- 5b. site claim binding: the webdocs paper card's page count --------- +WEBDOCS=../provider/src/pacta_provider/webdocs.py +if [[ -f "$WEBDOCS" ]]; then + STATED=$(grep -oP '\(PDF, \K[0-9]+(?= pages)' "$WEBDOCS" || true) + [[ -n "$STATED" ]] || fail "webdocs paper card lost its '(PDF, N pages' claim" + [[ "$STATED" -eq "$NPAGES" ]] || fail "webdocs says $STATED pages, PDF has $NPAGES" +fi + # --- 6. render for the mandatory eye pass -------------------------------- rm -rf "$PAGES_DIR"; mkdir -p "$PAGES_DIR" pdftoppm -png -r 110 ltl.pdf "$PAGES_DIR/p" diff --git a/paper/ltl.pdf b/paper/ltl.pdf index 1935968e111b527e96cd6ad9a93d494a58baef5e..6921d7da68fcb353b7bbe4152c701cb9d4c683ff 100644 GIT binary patch delta 4654 zcmV+}64C96uMLT>4S<9JgaWh!TRsFBqgA|@Up@nwe?j6zhZ0AY%M5MK@eU>07`{hk zJR&`;7vf0q1}1$(an4vteYkK$n{_1aS+CH_1j8~SxzV;JaimZGYwWEU{fIvu0_2ju zOZhQxqWx*^HQ%KUx^2HzqnqQFq{Vh!z6)s>sY!PH-D;!dkv`yCtdH~;l-r^CJvc&! zB8y`|e-UYs%>TuihCo(p;Hj%03+GDC8(mgs9d zN9v=OKdxaVl^a8JmghQineM4Pf?+Fcu2LD>o=l@?Loy*Ab>ksYpL{Ozk-y19w5;>` zKVSIL{u+o(JvX-Q?mvi+o6-gS zfA~KIkg0zUpTrmGAempdU2HQAw7XJRUCdS5+TAgS)7lNe>Jl&W#5>_fChH_l3ZZ&;lwKK-b}srO@QM12G?4#qY;LyVDW z2-PA}~Zj_|vY4>~-r$&#Be}-86*kWKS_{!R`ijgEiRUiqfP2~>N1lW~h+UKgg zBF;nf#59$IVcNt^t%Bh@(T#NglVCYG5H7h(W{TvFA}M^n7r6y9C4J(7jw-dubX$?< zSm9KwaXzI4inh_88i7i@AC_`066R=q?M$iy*#*f(6peuZ+89k+f14SGe-D<6h;bUu zLdlww9qx!GoK&60rDu<%HQXmrM9eG$sy5B27m|q&>&_kT{HJZ%G~tN^2Br=jL^-DZ zkc1N`koS#rRH<@Id=&GbBtv?0gWeZtD9_`jc_+^cdDlG)qq)%>$=0$IcsD;0P9G*5 zf|8EGb1Gvb4o;PYBA_4@fApBsEh;o9qzO6^ZG|FUAX30608JhmMMv3AfqrWv+bL~P z){*U$!YK&R5|?gFuNZI%h9olR%@1$cOckVVX*z286NTX-r{UB|l(0=;4c(B5T1h4f zUxj2^ap&HSqop?<1P?%_>CCz}Pdneq3hC7kI1@I}$hPS;@1WsQf17PHwPF>J&!JYE zdyxnNd?mB&_=O+n2%NHg;s#@zk7S=xCfh`#jB$RYM3SUDxP)gQTx+ryd_2AGLT}xq zYc^d}CRqExmDiB=ELtihQ+5f_sdLDZUb=DI1xXACNGy3FPaD~@X~VCuPqXwQ3VI51 zoI4#kHU@x5MEbDMf6xtJOx;jrg0Vs&y*WdE0ToNC7{ZdQOEvd6{#)(Y4G_svf*WU8 zbjBsuX2_L5bTlZ54t-}-szf9qkw{@AZhQy5R0Az&w8*Xxs3rN~id-LIII>d)lrRH5 z^(q}w6=GfU%RubiBF%a=eaOpU0!&^Gae}=ZRg%Ken!u=Of5aY+JRNy9C)u;neWET< z=p&L4xrro179z>=i!hQrvJQq#mM#hO^fnmWBZ1y3qLdGoO_PI=Pfdg3u1PtlK$Iqb zjCme|x#^Rs4RW-(j!XqnN!MA1^u`)kB^i3j{+8ZOz=z&ZF&22Vbc@C6C5sg|iGF%{ zDSrZkzz`o)e~F}xCKOZ+v%*)fJwjpXhhb+}?w$}Q=)=wvRmpLh#G6o~RKYS)dBB7; zB9I-YAE$efyXJsHuL%juT%;(<$B>RH4W9Hw;v?wfaA^`3NfQb-Oyq0!Hy#m~$VVBG zFH%s%6$M4=7ZTS_W~et3&XYrya6W~U*Qa_td*n;5e^16=+~pEDfvsCy>(t4u5|B;@ zFSbg&O(nitvaS(Y1CdIaQ;ugi=yXV9#L(9hD`@-PHe2Kl($VE(NJq7iQPPt&k@Xal zp6CE^E5rvww#4}IA)~-Gjn*P=L~BJlBsnyKQsXV*u#VUAXtT?zE?C+k|8)IG@?<_+ z(SxKFe=lc0x=+_sAga5QWzD6J9v(k>|K@K`p1z!ap3J1WeRqC&PIX`XwOrMoAI&c2 z{IK@pbh%pmb?f+i{-OSn99zb#+;PrYER^-ZVhx_v_`^ zVtTcjFZlI1T3EmTmR=;S-tzl;?Puxj7S-|ce~kJH!c}ya&Tq?Ts#l=u4edCp?oF;9 z*3*xlQl;ZRKE9ovuRhTl9rtyY9;@Cq@LabQy+mj|1y4kS>d|U)IXyd`eY~tkqB^;p zd|Zx{Q_>3b{?}yJu^V!CK?--8xshrojDpacs-{%v|Ancml=7wHDT;s$YIci?1DekD|F z8!G+)s0{UgC|bfcTEgLIdGzk&`0ej&e`>@{q9t_D(t17QaI_4%7KDKkEm{CAkzUN@ zH^+Z0S_b7;q9wM_(t63{TE{Zb|DkA+VjC{;aJanw?e)W#PYQBwC=R7p8cM8~?}|gx z48|d?O0WcqL($R}JdQ*9hsU9Q5f*T1Ue{>gVh?~zZ|4VNMQvflio>z;_XofKfByVl zK}!FuG^>VZv2C#2mgYzx+mAZfj2kb$$;%9hvP6w< zqb44Jnt|>Q#*Nv=jXWGT$B!T0d;hqhCfr~|Qr&DYhj9~HPR6p6q2G{*z6Uqo z7mO&IUf$k5*ik910G1rkHD;DRHe}7gf?N3}R zSNA?m79(l-CE9eZ6e3q;parBg+i^(JNv;sGSG)FDJ`S)koSQS_9tI-RfR-zj{(VtDaXc zs^2Qet(sIHsJvCpa-)}t zMpn?r!jb-KOEtR$a#$*L|Nf%~Z{MP)SCiTDMi&ircOgiBf7e2g4}+xKYhN z(@DR*C$0IBsnn48id0Is7lHI4i$DY2ADT*;?X=tJ{Zpy*j%s1cZZMU)-bdem|I6d! zlYWV{%-HR1#=yiuK00KTn`>ZF8nA5}aFYi;s7|V1s)yC1>T&gyGoqK(E12?|Eie1e zwx8|Eiv}dKf2WRIM@MBC6~0uF-%?R%tLT?spFVtiH+z>?e|`Qizuc**xWB_)Yf7y3 zBzE~))0^pHc5*xNFLlz-P5Mqa^=(ysp3aZ~rNov7tQYk;r?x3f=FB!-OcsmzpE*j> z>G_9Cj-Sm%Dw@?F`F*LB8edLUtLa(2nqSc%{1ZQCe=H}$$b;&vo?cFgHFT5DQ!gJ- z1t0WUU|_fC_k=>|rc|LcSFv#!Z>O{4*>bwRE-;aklFbb0(d&D!ej~!>v-u7%IJq|% zkf%3hi_^8)Dy0rclHqV}YeE58t&pw_h1iC|I*IyPPDlDV+fUZ%-S{74cE8`f``hbh zZQT#2e>qOwpw+qF`6WDLq#u~2pD*=3wnUwOPM~9T5C!aR`OnYbsJdEAA?_{6?__&V zEvSwbqW|_u#FH1#e|hj*llJ;y1>D$l(Dx!eG)qF1O=1$!4p8~6%C-FWP4Wl0-Ba#n zXOgcDO7egC?e9;1d(z5jcL?A7TatX)W@Oky-Xc8DLQ%l;@4Nt zwu9XbOp3bCJN16gJ3W%vR>bVtNkMfslOiE@ht0k@k>4>Vii2~aA?cNKqV^+BeaIuu ze}V1~ofG-($5uY?9^ZS$5s(u9IPCLoY(^Aa-;4+o*W2{=jWmv) ziQ9IX9mMvGD9wk`Y-l|fDonGV(ftG-x(iBDv~n$RP_Q|Ebobu#hb>3EL-78FgN+J9 zvz)Y^PwzN%qD|wBdoXP=x2Arj$agWhr_8$#tXz>yxx*G&PVT;YaQ{XB6TX(T<4xtT zQS?Rjp2wP{u)EKwXii?PdiHa*r+B-MjPypjCLDz5_wSy)JLyc)-Jp!UxVed%f9=gu z4FFC5E`^2%@u58>4xPtF+cUI6;5!-JQ|xiqV#I-u>h3;%^z6l({!I=ok;|Kcbh&+mcRS0^N!_RNhL~Yi3tTw>weo~L!U};_9OUij!o;nvo&ojx*^U-Jbo<3|` z+k>yGdbWfE+_41Y_nw=H>)^g~f9;2#xbQL{c@ytdTk4$vNsqv4T7_F(ZO%WeHs_zG z=joy@SBI|SeouYqU9&cESh{%k)vqTnUga!mc!9{^y9}e>o9i6H0xv z9CR}~RtF?m%;rpc6QVg}6Jmew2k%#vdTTZp?e(*{vU*BB))w1M7kn|>h~7i{z??Xe(7|LvUq{P5uLBx^P#gjxb*WrhW zln-;-P1EYu?2_`dp=XP{-ZAuKk$&R7c)ED7z+9OtkxGhmiMAe=850qilO`JH{{aA- ztRt842m=$BsZawNLNhsIG-EVnHf3QpHZW!|Wj8c7V=^>0Vqs!pIb>xuVm>@GIb$?q kG-WnrVKz1}W-w(pG&W;0G&W*kVq!UDWi?{A1yKWp26AFBtN;K2 delta 4654 zcmV+}64C96uMLT>4S<9JgaWh!TRsG6Wv#lGUp@nwe;G|ZSS5}uml@ie;~h%0F?^58 zctm7I%Qj_fXyVXX^BYnWPSRd&xD7QoNdvJsd zMHa_`e;t#~z9qgRe?tP0hXZ!~cT(N_d0ZpS60%no zUMWU2+mqMXo)WU14C}J)pV74GiY&`mlkFwx({dZK0G5Q+%w^P(tuxC#DmRAcEYEf3GTl>o1jAO?T%|I$J()()hGarK>c&H)KKWeaBY%^JXj$j= zf4=ag{WTDodTwmp-G2}t$w52o8e>-9=R!mlZ~AUKi{vP1Q8+CO|L6RH9#FP%Hl+*t zfAN0`AXEPyK8Y{VK{CIzB^OZNoN2fMb{v{Ez3MEF=8WsD+mfywyAN_ed`_T;0}THG zI(4$&0Xy)y(XAzeC*3nwKV;nOJg%)L9FOb*yU0M!$n$1NqL1kE?A*yR6|Y2iY1fpe z)W}(%^x`PpLwW*dsyO^uBtnE~vN#_je`{u6%Dyp;0S)Z(FRIo;|#lFT?Lv80`6yi?dB?6{oTa+%(wv_2<^l+^kodl2mi(n)gr zV$4x}<;T2H-uP2(#t8Y8%%2)H4pMW}(o*v$(B5Jyies+>KL)o>pIQSpY2!L?f4)w) z;+PH&eFW}qq-lSwjMUGm3u9D1^9!)z zvBIfV<9td96m6qFH3F4*KP=^1B+SwJ+L=@ZvI~-nC>jF+v@x2t{x&lVe;+It5#uzR zg_1QVJKPaXIH@{~OV1ujYq(FMh?rRhRBf73FC-Hm)}1@v`A^%jX~Gi;3``w5h;mH* zAqgi?AnzOLs8Z#a_$cN9Gof(MLU4@YQ-ubpF^!S z_aYGl_)2Ek@e4oD5jbW0#0|zaAIUzYOty(e8RPs)i6lvRa0$;qxYlGZ_;`BVh2FYJ z*KE3|OtAKWE3YB#S+rD2rtA`;Q|FK+y>#Qa3z8TPkXZ6Uo;I>)(}rJRpJwSr6!aA2 zICna7YzzRAi1cBhf1w+|n7X0L1Y?CldUJ;S0xFhNF@z;qmul{D{I}Y(8z7RU1UJsG z=!{FQ&5$dB=x9(99s16wREbDJB9X#K-1rW9sRmlmXpvnXP)qW|6}djbaAcQy?VD#W_xmx0*3MVj?$`jD5y1em-W;skp+sw9P_HGxsne~3LCc{=iJPO@jC`$S!! z&_^U8auZ32EJTv!7hxoMWE~8fEL{@l>1{B$M*_W7L@6IEn z81p;^bJHhN8{}wn9hnNElCHB1>5Vn8N;344{VlznfDgT+Vl41z=@yICOBO3`68-e@ zQvL)6fgwJqe-cR>O(>`uW`(a{dxXN&55vx|+&v*q(1)ETs*>Y0i8rA}se)yq@_-3x zL?Am(KTh`|cg+EZUK0|Qxkyozk0BjZ8a(NV#7EG{;nE~7k|q>vn8?@cZ#*I}k&iMW zU!DyZLq>sX8m&d#h}Md9NOEWdrN&#rVI8mK(Po!bU9hx8{^|OW|T>JbgL;Jef&#`|kYmoa(;%Yq_dFKbl?4 z`C;wH>2kIB>(=r4{6qay^?Y$&FQ&7Pw;r9>v(guxoOixe+y=j2X@7K$- z#q?@5U-0X3w6K2vExkxuz2*1y+RxJ4EvnN8M0IjG z`M4Y@r=%6={jbX!6up?t=F9qL(fk)g>%TjhLwcw%AVMlWnO@eIMddepNT~G+m%4}Z zf3=$S(a-Hh?6)6Q4`yfcbEu*!?j?bpPe8$(_YtOt&9CRb&!(td(;R0P4gFBL`~K0J zr|%0=fQm1dlf_M-#dOi)z6UMN4uJ*PK?xRw{M+hlb0D1Wr-T! zMol~bH3Qurj2p9!8+kZxjvqg~_x^E1O}N2`q`KLz`mSu(5921ZoQ!2BL%$&reGhKF zFCqs zuI_!BEJo7uOSI`+$u$l98!WsBaXpYr3H64hXV0G=zkCjso=#Suk|H`2gc3CN8jNfp z;NUzmVjMuyLQGHop_&Pk*d!qv&}f=V(=P`J!_SFM3x!&nclLvOX!KT9UoEGX^O>v` zpXSwa`tkFmI{P%Ou3#VYfAi{W{uwte>*caqUQU*us*kiqvQ(V>;t8}&? zTB@tdFU#ux>cza8&+2OR=e$~dTGTak{8$?Om&s-IVKF)TXT9R? z@_Fj;V|7{03v~|3Z%<9ejwX#LRp|~=&3dpD?vFX>LlBNE~}K*^?y}nslPA z$zC<~Xz*hGWl>#BfB#6jT-JZovuZX)m1`8(SSxy9d%c9U&Kr9z6gwcz{q&mNcPsR& z<&a*lcfTj^?>~F^s^u|uDA(Sw_w}mJ`y#7M-k09V?RsCQ+A1bjn|v%e)F*JHDM?n03Mf3Aff9|lt?C0a|&aHE=k zrjveqPg?UMQ>h{G6{(bNF9PX97J&x3KQxsx+iADc`=?Ur9o52?-C!zpy^p^C{+Gwc zC;bv@nX%j3jDd-Re00bvH`l~Y?BsUjU+ScvoAjM<>f5UNJe?r}N{KBESTE{xPHj_|%$aSvm@F3aKXa6% z)AJ9P96y_jR5YtU^7~RLHNKpzR@1Y3HNT=k_$PkOe^^e0kq6aTJ-wU~Yv?AQr(Qmw z3O?wyz`$7JmoIuCwAPU&s@}HlN+uxu3_N0~5?hwBDwm=txNck2C~cX}kTt%%vPlY;7OCPhN*4x4>*BEMr!6bI)-L((hfMD0hM`jAJQ ze*@hgIw$hmkF9*ze@^7%4m(7^J;V&(J-+vhBOoRIaoFeG*o-K;z8MiFuD9v!8)+Op z6SwU&JBaNWQJN2>+0c3}RG4Nzqx%UwbQhGQXysbspkQ#)D9?V)L{ z9!_iNXZ-13jPUJM_F&p#ZcY74k?&%1PnmZgSh*sZa)&LloZNl);QovLCwwhw$D7Jw zqv(t5J&!d@VRxTV(VV>!5pJ z-M6!&5P1{>s}S@kho9f1iQ267SZ#pU{iGhd!P2_Imz49eJasOFo@bJq=cCW=J$=}? zwg+EV^=t_TxMK;(?>#pY*TH?~f7%Z}ap7e^@+RJ^w$wWTk{*H8vJyJl_Tuypb6t6xuEyvkYB@B)#yHA`e{&+lCY1VS zIp}6~tPV)Bn9Z5?CPZ_{CdB^U58kgT_10`I+UsX?W%ZPNtSz>iF8E@$5z8I7PmbTc zdGoiYukJpTV%rGa4@_r8_n}BD2q6a1LoB5s|ESuth1iMuC)NAH-dZdiW@f)0|MK|p z-}7Yr$?E1_BQV`fn`XaFf14f=d$Uj?ecz@{sx!DyV(7787}1X?NTK77mk8vJmk5Se zO9muZnpb<@ra5HaW`FMon^)L=p)D3u2O4hhq0;^7#YMfSXJ6c-iL;mF_hWzNQr^RL5L%*izkU>uEP%# zDIeyvo2J#R*(K#^L(dj@y<_OfBK^dD@pSQEfw?kQB9#>B5^X&!GbSQ3CrvcY{{v-| ztR9!~2m=$BsZawNLSi;yV>dK8WiexBGBh?gWMpMEVl-wpGBz_bGc#c_Ha slh_block = "" return f"""

This key is the sole cryptographic identity anchor: it -authenticates that these statements were made by the operator. It does not, by itself, make +authenticates that these statements were made by the operator (the same party the artifacts call “the provider”). It does not, by itself, make those statements true — each attestation's truth additionally rests on the replay, theorem, -extraction and toolchain assumptions stated in that leaf. Every tree head and attestation is +extraction and toolchain assumptions stated in that leaf (one signed entry of the tree below). Every tree head and attestation is signature-checked against this key. -Pin it, and compare this copy byte-for-byte with the independently hosted -mirror copy; they must be identical.

+Pin it (save your own copy; from then on trust only what checks against that copy), and compare this copy byte-for-byte with the independently hosted +mirror copy; they must be identical. The first fetch is trust-on-first-use; the two-host byte-comparison is what bounds it.

{pem}

SHA-256 fingerprint {escape(fingerprint)}  ·  raw: {base or ''}/log-public-key - ·  curl -s ltl.zkdefi.org/log-public-key

+ ·  curl -s https://ltl.zkdefi.org/log-public-key

{slh_block}
""" @@ -197,11 +197,10 @@ def render_docs(log: TransparencyLog, base_path: str) -> str: · cv

LTL — the Lean Transparency Log

One sentence: a public, append-only Merkle -accumulator of signed statements that the Lean 4 formal proofs of specific -cryptographic Rust libraries, at specific git commits, machine-re-check with exactly +accumulator (a hash tree that only ever grows) of signed statements that the Lean 4 formal proofs of specific +cryptographic Rust libraries, at specific git commits, re-check by machine with exactly their documented assumptions — so that you can trust a proof result by checking -one required signature (Ed25519; heads from tree 14 add an additive post-quantum -SLH-DSA signature) and ~{max(1,(latest.get('tree_size') or 1).bit_length())} hashes in +one required signature (Ed25519) and ~{max(1,(latest.get('tree_size') or 1).bit_length())} hashes in milliseconds, instead of running a theorem prover for hours.

The trust anchor — pin this key

@@ -211,10 +210,10 @@ milliseconds, instead of running a theorem prover for hours.

{tree_svg}

verified attestation (all certificates proven, axiom cones boundary-exact) -historical audit-failure attestation — kept forever; an append-only ledger does not erase its bad day +historical audit-failure attestation — kept forever; an append-only ledger does not erase its bad day (leaves 0–3: an early audit round that failed; leaves 4–7 re-attest the same four libraries cleanly)

Every box above is computed from the live log at page render — leaf hashes, -internal nodes, the root, and the signature are the real ones. Before signing this +internal nodes, the root, and the signature are the real ones. The code that signs the log is itself an entry in the log — and checks its own entry before signing. In detail: before signing this root, the provider Merkle-verified its own signing library's leaf (index {provenance.get('signing_library_leaf_index','?')}, certificates {escape(str(provenance.get('signing_library_certificates_proven','?')))}) @@ -237,12 +236,12 @@ identical. this site · mirror 2<library>.attestation.json The claim. Which repo, which exact git commit, which theorems, -which observed axiom cones, what machine protection — signed by the provider. -table above, or mirror entries/ +which observed axiom cones (the exact set of assumptions each proof ultimately rests on), what machine protection — signed by the provider. +table below, or mirror entries/ 3<library>.receipt.json The proof of inclusion. Binds artifact 2 into the signed tree: -leaf index, sibling hashes, the Signed Tree Head. ~25 lines of Python verify it (stdlib hashing; signature checks shell out to the openssl binary). -table above, or mirror receipts/ +leaf index, sibling hashes, the Signed Tree Head (STH). A one-page Python core verifies it — printed as Appendix C of the paper; the shipped verify.py wraps that core with full fail-closed binding checks (stdlib hashing; signature checks shell out to the openssl binary). +table below, or mirror receipts/ +the full mirror clone Maximal benefit: become a witness. Every leaf + every signed head ever issued + verify.py (Python stdlib + the openssl binary for @@ -257,17 +256,19 @@ consumers.)

Attested libraries

{rows}
componentartifact 2artifact 3status
+

One certificate = one machine-checked theorem together with its exact assumption set (its axiom cone).

+

Three ways to use it

Quick check (any machine, milliseconds): download artifacts 1–3, then
pacta receipt-verify --attestation … --receipt … --log-public-key provider.ed25519.pub -
No Lean, no Rust, no account. Add --sth-store pins.json for split-view defense.
-
Zero-install audit: git clone {mirror} && python3 verify.py --all -
Standard-library Python only. You become a witness of the whole history.
+
No Lean, no Rust, no account. The pacta CLI ships in the pacta repository (pip install . from a clone). Add --sth-store pins.json to remember every Signed Tree Head (STH) you accept — your defense against a split view (the operator showing different histories to different consumers).
+
Zero-install audit: git clone {mirror} && cd lean-transparency-log && python3 verify.py --all +
Standard-library Python plus the system openssl binary (signature checks fail closed without it). You become a witness of the whole history.
Autonomous agent: the pacta tool adds STH pinning, freshness policy, online refresh from this service, risk scoring -(R0–R5) with policy-gated consequences, and optionally verifies every signature through +(R0–R5, six named residual-risk classes) with policy-gated consequences, and optionally verifies every signature through the proof-attested Ed25519 code path itself (--require-verified-verifier).
@@ -290,19 +291,19 @@ view.
does not mean A verified binary. The proofs cover Rust source; clone the attested commit (the commit id identifies the committed git tree — not external dependencies, toolchain downloads, or generated artifacts) and -build it yourself — compiler and build are declared trusted base -until the reproducible-builds program (R5) lands. Every attestation carries its full -residual-risk list. Honesty about the boundary is the product.
+build it yourself — compiler and build are declared trusted base (assumed, not proven) +until the reproducible-builds program lands and retires risk class R5. Every attestation carries its full +residual-risk list — the enumerated assumptions inside its attestation.json. Honesty about the boundary is the product.

You hold the ruler

The list of assumptions a certificate is allowed to rest on is not something this site hands you at verification time — it is a requirements card that lives in your tooling, on your disk, and that you can read in five minutes or rewrite from first -principles: Lean's three foundational axioms, plus — for the signature tiers only — +principles: Lean's three foundational axioms, plus — for the signature tiers only (the top proof layers, where full signature verification is proven) — named placeholders for SHA-512 and the wire format. Your tooling ignores this operator's pass/fail labels entirely and re-derives every verdict by comparing the -attestation's observed axiom list against your card, name by name. +attestation's observed axiom list (its cone) against your card, name by name. The operator is trusted to copy down what the proof kernel printed — never to interpret it.
A card you write yourself will match this log's supply @@ -312,13 +313,13 @@ shrunk until every remaining axiom justifies its existence. If your card is negotiate — the gap is itemized, never blurred, and you have three honest options: accept a named line item, walk away, or prove the missing piece and enter it into this same log. If your ruler is stricter than our supply, your ruler is -our roadmap. (The full walk-through is lecture 11 in the -course.)
+our roadmap. (The full walk-through is lecture 11 of the Jupyter course in the +pacta repo.)

The paper

Accountable Distribution of Machine-Checked Correctness Evidence: A Transparency Model and the Lean Transparency Log -(PDF, 23 pages, v0.11 — revised August 2026; the version is printed on the +(PDF, 25 pages, v0.11 — revised August 2026; the version is printed on the title page) — the trust decomposition (expensive verification produces an observation; transparency makes the observation accountable; consumer-local policy decides acceptance), collision-extracting soundness for inclusion and consistency, scheme-level @@ -334,14 +335,12 @@ instantiation section for the SLH-DSA (FIPS 205) verify path — eleven cer five uninterpreted hash oracles, exact cones — and a certificate appendix mirroring the Ed25519 tiers.
-
The paper's snapshot vs. today's log. The paper analyses -the log's 16 July 2026 snapshot — thirteen leaves, still leaves 0–12 today, -byte-identical, its pinned head still head #5 of sth-history.jsonl. Everything -since is additive: the four Ed25519 corpora re-attested at 44 certificates each -(leaves 13–16), the accumulator's hardened model (leaf 17), the first post-quantum -subject (leaf 18), and dual-signed heads from tree 14 on. -python3 verify.py --all re-verifies the paper-era prefix together with everything -after it.
+
Paper and log, one story. Since v0.11 the paper +describes this deployment as it runs — nineteen leaves, dual-signed heads, the +post-quantum verify path as leaf 18 with its own certificate appendix. The log is +append-only and keeps growing past any paper revision; every number the paper states +stays checkable against the retained history: python3 verify.py --all +re-verifies all of it, paper-era and after, from a clone of the mirror.

Log heads are signed offline; this service is read-only and holds no key material. Provider tooling, agent tooling, and the full Jupyter course live in the pacta repository.

diff --git a/tests/test_web_and_witness.py b/tests/test_web_and_witness.py index 30995e4..27870a5 100644 --- a/tests/test_web_and_witness.py +++ b/tests/test_web_and_witness.py @@ -159,3 +159,25 @@ def test_standalone_verify_py_runs(tmp_path): assert result.returncode == 0, result.stdout + result.stderr # hardened verifier: full mode (signatures verified) must report exactly this assert "RESULT: OK [full]" in result.stdout + + +def test_webdocs_source_carries_no_stale_paper_claims(): + # Regression for the 2026-08-16 operator finding: the paper card said + # "23 pages" and the July-snapshot card survived a silently failed + # replace (an invisible NBSP defeated the pattern). Guard the shipped + # STRINGS, not just version markers. + from pathlib import Path + + source = Path(__file__).resolve().parents[1] / "provider" / "src" / "pacta_provider" / "webdocs.py" + text = source.read_text(encoding="utf-8") + for stale in ("snapshot", "thirteen leaves", "16 July", "16 July", + "16\xa0July", "v0.9", "v0.10", "23 pages"): + assert stale not in text, f"stale marker {stale!r} in webdocs" + # printed commands must work as printed: curl needs the scheme + # (http->https redirect yields empty output), the clone one-liner + # needs the cd into the cloned directory + assert "curl -s ltl.zkdefi.org" not in text + assert "cd lean-transparency-log" in text + # first-use glosses the page promised: STH and axiom cones + assert "Signed Tree Head (STH)" in text + assert "axiom cones (the exact set of assumptions" in text