From be9a39cd2b19bbb7eb2b81306fef0db69e15b1a0 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Tue, 7 Jul 2026 09:28:55 +0200 Subject: [PATCH] paper rigor pass: fix three claims that failed verification; serve the trust anchor Socratic audit findings, all verified against artifacts: - 'zero lines between structurally identical forks' was FALSE: risc0 vs betrusted differ by 27 lines (all annotation, documenting the risc0 fork's black_box trusted-base entry). Corrected to the true number. - '~64 Lean files per fork' over-rounded anza's 58. Now '58-64'. - completeness parenthetical now states both hypotheses (a=-1 square, d non-square), not just d. - 'key published in two independent locations' was ASPIRATIONAL: the site served only a fingerprint. New /log-public-key endpoint serves the key bytes; docs-page artifact-1 row links both copies; test added. Verified exactly and kept: 215-line parser diff (FromBytesSpec), 121-line signature-glue diff (SigApexSpec), byte-identical x4 math files incl. the carry-telescope file, 11-axiom upstream boundary, 16 certs/leaf, 153-line mirror verifier, leaf fields (toolchain + machine_protection), all 17 refs. Co-Authored-By: Claude Fable 5 --- paper/ltl.pdf | Bin 412316 -> 412489 bytes paper/ltl.tex | 15 +++++++++------ provider/src/pacta_provider/web.py | 15 +++++++++++++++ provider/src/pacta_provider/webdocs.py | 4 ++-- tests/test_web_and_witness.py | 6 ++++++ 5 files changed, 32 insertions(+), 8 deletions(-) diff --git a/paper/ltl.pdf b/paper/ltl.pdf index dcb96fc19ae54122a605f9be521b81f3f85211b9..32873485a6d5e205aaf6244554862a39a8a5bfd9 100644 GIT binary patch delta 17432 zcmV()K;OTdl^MyF8IU9cF*7xjQ7H2QM-^tqqYldbMo+3H`v%AWcC z{_R)aywZLpTq=dptG9P6;Z-U!wQ`wAbL&@cx2t!_>#JNRZ(qN-S}SLg*JW{k;HS4& zxk{Si&>oAXJZv7r_xk?o=Ix)qd1b^(z%0f{oO!Jc%&1pu0l%6j{`H}3N*E<=@-OA~ zwCSo3SJEY+sW@!$!6iR5kH@aQZ;InXwc&4nZR)Eve5&vG{Xeg~Nb1uDhd*%BUET1* zkHxV0FC8q30Iq~Gsm%OpEq&^LbIBn6WmkkLf2x}gS4JmA_rUvc`O3og^sz{(QKSKIuvreI*h)Q%`5AbOOk)n{v-DM>s_I1mE+d zY+7tI$%d#4zHZ8+gX(5YXF3BK{911rw5Hs2hqA?` zgk|D^-)(u^)d<8RLAvFC*3E?KunCFIL;q_;u}E%D9e-fh;Grp70PD2ts>6K`keooI zZ0b}%R?)U6V4)3;*I7~_Xj&xYrz0&@9@;bhpuMa4JVcfa4&)tu+gury09w`}X-@#f zzMMHb=;{*SWNi!pyWZg359J1T{~lqcnF{`C%3@cw9qgXiCC##bDQ=}soeQ`<4p~x3 zJd@+8<>#(=Pn!s@IKL8MgbyQVbM(4nsEXi$|+eQZo9RM}FPbIO^j8kGTT`?Ya5X zmQ9$sIxLc6mZjc*8iobeBZNzB+e%dx3oup`fZSy%YaHaRUsnuE>*dK zAB%D@;1Ul9M#0QkQePR7+|QG~N11D~*H>PGLW4&Uz!Yu;^Eu^735KOaW>e`TU@A+E zNMKftNS0u;~YW$%U0`IAr+#xGTA>BTb7! zkCpAhsYd#L+SN!~J_EX_TRavACtDV0f!p$Dm~G*xU;v#7fLkDf1$6GZvh50#zU=~r zNw`RzwAK9q_lDEpkaAzLUT7B>RU4INIzZ0^uUr(Z&h>VOO*A*01y0NDBop96!LMx) zp~wl~fN-TuEn)1lAv{hFF)dOYVarqp7HoF9=hBo+R0gltielb{Ub6!j( z_f^LoHuZjAbu_geOI`;;jJkZRx(6Orege%)iX55&169M1Ti)^J)bmA_PhgXIDwJl} zBFf7kKZ{RQz30ca>{{eyFf@LE!(@HI!c`<}g*DY32|Zw`Lm5WFp%&e#39l%aBN>Vb z9AH#`3OB%!%8?|C2KKloeTv%d08;P@r$x1eEn}6CCskJtW!@bcC5G9J z`Z76z^#kNY7v`Tm4bYKWcU!%LF0goZ;9dfwL%1-eQ~PV2W|^c zC=h@k;oiRHm%FA8+UeNfAhL(yZNS6}LPU9yDiJW%jV*kzEZfHx*ttbU*OmloMWU2G zZjhP+DM@6n^%f|pw_%_u*n7++BQSD%7V^1TDVwLtcm^Y=;cd0)2on}iPNcFSJCK-v z1sda~?XnKSkM%7m><^@b@Qf|-2I6SXZyWpqWWONg9O&1gX)0zci)1=4DwJ`l27ijS zP@WwTYlg>wgauQ!HGkpbw02BO{EZAm?9+e*qvhe{E`H^0U4d;^td}4HKTK;M4I((L zYZTZvIYdhbUNe{61&YDvA?{xePCXodyUuJBE%>-0ym2e?50&@4n zxk`~56|i{A3WS6=NXu=7ZU$oZ<;Z@`0@5P0pvB9Ko1yslQ_GKCkQEsqtJsEr#-iyZ zFq{i%)&;<_JT+cLz|ere12ZUt@#nTWkZniLr)t;nBeM-Y5lHwDltAeF<5n6Ya(=1y z#~tf)2d4cJrODi-R=P8#A(i*`2tI;~F!0E*0e!w87s}AaTZad-UR;1Hd}Ng$HGv~U zUN6DpO=?|m1?Wt)Gy|r@w}FCxqmO(1#^+n&Szse$NKQokpTgJRAMne+mCgHIxde|> zsS^P|ZMnN!2NppaBA5jlWD)KWf7vDiryVeXGVczwiwEWRD-vwUUmEz{;+lTAX7&y06x2xFTa#29Q zP^3x@cQ_E$pO$P>DNX8s^Wc($hB$(jHf-|;la3F`MXLcGqVR#oo_g`+Y+y&qWU}mM zD0cTX8FWiFy`<<^a5Bl315kn?FXNsm%t0sEQxK3>kP@iir$PbRDjrbB&Y>$?VcfzV z(!?y47}t!^plx|q9=2)F2cwu+wgN<_V5)O448*k%KrBBWu25=!BVOQlz&@8A;RF*x z+p{oyg&bQqdpb|>!6K6kEFx-W>6S<4bAtdCe4PfUpyMX+b;&&*P)xK7>xS!L0%tHLcn6CF@7TENEvZD)KI@Y|klfw);jR7|ia!@KGZlq=Yb5g0Qv z^@NmXSvW*Txn19XlGs_JVF^}Glo!Ag9H^)m0tYLf0rj|VYW?Xu@~dC}6F0vbQH8WJ z^?35b zfnhxEcf&Kb57n{f5Bl9>5Doo>5URpX^&JHkKH{IEiH^;GkR5{pp%~Xv_$c>hA^Z?6 zao~!4OwCAv;l$w6u?j?k60YU8!Lf;OY|u)lRvt=zzc@E(QQ+-@lp&Lg$IvHv6yM-DImRe8T-I z*ziZ{xJR@ZQhK}9FJJu!CyRtsE0g9F^SxV{9PlevP5^#Q6qLLLnXQ1Y9UM`}7ers& zf|al2%6jnj0`dMkX+;}E2>dcWN`3*hzdN<;>0~i~L;_DpK}8b=mV2ao5SXkYE!lx2 z6yb3~I?7OhWC($9{dq??rB_u49h+AuwhhU*@6NDf$k034+%Mg)81SGpzjYg z{(Rh(+k4tuMnpr5m@)Ta3rF3K1@8`BGitu&%~JLuLx!V|1N9N+*x-2&(1!tcSovwP2#YC5+LBkQ9Jt@W;w#7wnN7 zb3=rq-0+6UUg0mXo%A8~>}~4IPN8yHYHi@r9XimV>&wl6s1MZPUrsOr)frpB`= z3M0?%jt^F58#8w#n$;8p<5QP~NapDngzsg4o-dN5LPOiw@wm;Y`A`xN>us?s-!H_S z#DBvL#VghWr{rnY81{RIh;|Y3Kw|nT_*kQ;^Pf-PCku%Yhk5Tbp z<0y)3ybs|Xbe?~ycg3Lyakw`>|MCMr{a4x4*WBy-GDJqu$;MM6|1MYshN3o)7Xi3` z9vU!-Tpqv)W~x#YZ&rFDN0h<5(qv42Ikf>dL5zFd@U&yQ_Bw{@qPB2o6?4F@kA|q2 z3ZnQP;D&<+I-x-yL;v#Ah5qVyDAC~Q1A80xc!WsyH3{8qxkEsNBgd}K%`%S)$v)gJ zjNxEz*>QSQCPP;+=2gs)dV0#qDbhcG1m;!LeRhzDv1#W0YAsTmhxE4OZeFc4#+()Q z0vE%9T?9y1p_4Ijc{xn$pkT;xy1wUcS(eQ$3@RaiI`M6^PLcQrTL_4Y!f6;3@6iu1 zcpo{uM!C|(%q}ADV-CP?zvFrbcbBhQp5+5au#EZyjiVCNb`J zJ)X*`RLbd8b|%oTQjt%ly18cP+D)+|?W{*+vOtv@Y>gQD+Xp))9!ow$KrjYC9FO~- zr_W1ibmvARuA}c6)A~T=-)zgl8%GF&%|XGA=z@HR<|D>3*letZVG*2WzsQB!BdO__ zH!s^Z=xiV#mY{-@@bH77lyz5skro3U;}mZ}tlLz7>uqZhsu^S-!U7#va!X|5Wq6zc z!5%UXBPSFj>QwBpAR7%4>SAUK-HaP|8`GHrMeU59%%m@7^3V;ej8V561}%mX(fI?X z{BU2AuM7xjEoT#3sN!)z)9=^v62C)fT@~U-Mgf&cS#$6PU01tO?jkb zgg2C6RQ$**cn&6#{{yb|pW3GgTH74Nh#jx_=DEOvAbWi@24xDzYz`r&!k`T3aVnFv z5h+4-CdM+Pn%JdRoW9e51MoA79Vf*U87PCwp0I4yuZoK3_Y+3|)Sz%hO_DK+DQt?G zcWaZpUl=2k8?*+ZkQc*$uOpd0nh<=-x#V* zh9GbRIB(hw{2AneKgrm;@K`0?b$oV{gIX)Ri2IuC(_ z*@?mA!pPUT7dYg?QazinmVaFQdC85l>q(5YnbCrJZp$M*1m3QlYz9Tg&6RK&Y9t8^ z^)1h0XN7zQCJ5+6ASXae5ZHf>LM$6wszx9_GT5+S_^Nq-gyhbxBtV&SuVQYxOYBz9 zY*r(Jlp1eV&SA3OoRX;mYadGoL>|ccTwaxpjO*Fug$9WOV5-!L0OnJ+AQmWLr1I(V zRJ3IQlcRl%4J}DEJA)!WbYw!5vN=~L%(AdG=a@d%14IT5>0R>5kPGYeW>-+DOU&cO z;-o>;2Hn+v?jcGQ1PT-RyHj|r!sJZ_B8^PV1%cKV=1h%;Df|X-?L@4&3N<84vW)Fp zhN-EF-rB`aZ7k@e@>eWDpoD4gY0LCJozvAaOC^x+8h*V94xXRar3Lf!?TdNAgsgXa zSfG=k6d2nIL_&iq!0D{;^@&+AF}yIV>t|hogQ$RiM%Dtj)C6A6=Qp`|F<%T0;$?r@ zErSt}v$P8r#nN=*EKln9%kysLw}-WH|Gl6f{4*H)d#21u=R9GSZI;Y3ToDB`oa49r z^UO@e(=*MVw#2YVwnRfxJ-6uX=PWuQl^0L@29d*Mo`Wl+qN<4odSF~XtYC;0W!HZXZqF4-H>yHv!`IEzUPeZUwj83k;Oq8}2g7`EGr zg%N%Zu@HWVX4`^qWkB{@HD2<^=M_$_6%Z3qnSRlrphD^CsP5|4oXq(5D z1Oqys1#n_Cx{+0}xLGkX*NDT`fRI#Xf-W&(ML2dGWcOyHp6^ICzM8Xy(8`iyGjz_N z(Qsg9X!c&u9mE<8C=b>mh#ZQ`hXAMf5&{I5gd?On*W-lVf*r0$cKGA`oQm#A&CIEP zrpGksbm5hM;a0$Pwqm>&`G@R9&CjWxnlo&M^w5lh00a+i62?(Q>@Txf$3Rf1b!}5+ z11)@-iHK`(AN*>Kc?dT~`Diu;llj%4*W>J588F6hu310eVy>^}P5(J?F)*+6>>7Ur zytMa85?q0Y1$-=xL8bXb7F>fKux65f1t0CapG$+T?MZxL`zX(HGm8bVf&~)S=bTzT z#KIB&PB4AJd|6~z+$svL*w5Tz}JTK*j0!dMSwY*%2 zm`nqz62zJ^Hbw;d>xu(QKkrkRp@JJeVU-_$i-~H_)mE`mFqB(C^DW+cr2y~x4vPgY zqRuuI4yZ|BsgmdeZcm3CQHp{|H5xSQ)eTpYIo-<~4f^&eV_%^i2sYLPwzILnv=VRz zmJ^M}iG>RZp5iK6l7o-0?e8alzEC0EIl{Bx^e7DNxbZ^UXA(+U(S7&{?r3R@b=QaW z83G^fMl9y|VG^P3c(Pd|xKHx;*3$85I1S#{M+zNIjh9%AqAN6ro!MJb@hLTP13-1VIW}11|8pu?Srwy6+A#x3WbW?8J4YODR zOQfvFf=9}m;R<}i09KE6P@k^(Qsu{{I#&VC*Aj(YiX0SUyxz;1$_3iYTu+>au8xd` zJ|E-HQ;o7{IOw}zL+?Wj{>|0eN4vUx7K~hg8|W{yOpbDxtc&7S6 zV5RVI(EI1g9~{KLKh7jlbj#8e-JQQ^KP~s)AVzVosbnMAn zo~-`UbHM}&Zm+fDLC;YmiUw`fc+i>p?3ps3TOI$shrd`{JcH$b$b1f50za&X1KK;( z{CmX83<|tqQAWo(1N?Uo@8gIg+h z+f(hsGKha{RlsF`&Oj|15bvI@N?59r5KACDT?cUvQp_dX!V%2G#)M9t#{ci*IJ>z$ zmxB&&D2F;7F4ECRS6Cs>FT3il3#BKK4hMB4RTpkE4og$|dGDM0bezkdfT2d_1(^Fb z*vkL##7NaT&yeFhkZP~-K>pRa&q#2iPp_PT*s@>p~_E1>?2un zVIH?u9bVB4iIK^zj?e|sLwAVzbx6ZDITlR|rrY)TUf+TSaufe2H{gb=&$PxwPLAVn z%yAxnUte5oM8WMqHw*`>VRm$>#zO;Qhl9R-c551p;PFC!&bmw1p|&#Q(fM{d`i{{N z!RPodBj}%hYk+@=Wp}X*X7Du(EO&f4JDA>B68K}RGg|N%Jl;kA}t0Qc(#!3+jNJHBB;|0@l) zvqpE@`(bc)a8v1j0aq6Nv$N3`eis5aHIq>ahVH}8qfXpIa@CPNsVN?@{|Xgz(FskPk(*Z9@Vq^Sv~vHt9tUQ z;Q#eZ&01gS*3DdSm1@*%xqbDI88rISj9R{`D-+=J(+tV@rE>T!Kk2$^S{vG#uY&Ql zpMPy>-lf4O-C*b+@?vByX(>O%)t-UPx0Me~2{q#@tDD-E zNHa}kv~yXs##PoB8`5qhLa~jBR-!BuQ`b0n+MmQi2{GZc1egz18yZ{mY-<2T>wlU& zdZrYdC1Sx?qQ#zR^f>rLRt&FlJ=f7?K_}?&yMjv@TRHU-x?-y<@KV>{HSIUX*Fx6w z830qTy`lE?2xFico$;!KSg;_+rZI^YOyyv2@_|o;Vj~l+gjgn~u5s|RNs)sRVVTtu zWXiNvU61q!lG+d&m1ihO1$&uVuz#0{WoMou&oGr5qpe)pb+oD4RmS|za04JT`bD@& zt1EERSK&74H-TGR(C6R{cD7cnD&eM_so)?hQvyyo4YKr&&q8;qY8}*fwh)4lf@Ow= z$`^AaO37g)mi$Fp?iq*Aqkm6j$AB9x?Ki| zdktvQeiNX{I$i*pft}R0)+3xX;HCIlkK8rgfTz*~pU<^!JTwDZ-it&jcQFx1ILp-B zJI;`Sk~k@GmUu2M~J`@(Z8NTpMmsHIbxh`Do|B7e^?k)9x}T-+y+ z2Hqel^4|k#4cK<~BGRPQ6{NYVNSpMVB8}Ja64GEVjZ+1xFfh>Y(keZQL5*%8)Tj%K z0lqvmV9I2l1LF+IYXuR(_^Uq%-SpkWF_ohc=Qkyx@9 zX}PD2o(4aYoP-JG!hf#A%s}YlzbFd5jx!5W)=l#Q&SI-8IBTxqY}#*vv$&8KfM#JQ zZKKTyXKho}L7S1cW?EZ?0KQ6=G*IfmN=`N-QOa#h#1YOiwd~C^WTYfcN}MI0OPE>R zf(94;#Z;>UV8gbBw^on}7BjWrFcWjL`*RS})-G1ml-k5sc57*A@WYV#~SQ1GPm!zd_QyGLgh}MC}^6SuGAl#-5tareU zy&|C4EVd#EeZ0{D*0=s!ZERe3cRcooV|QHdcZVn}SAVPKjcQ)=`|ZsFy6sQ9RX02@ z`d_-`5t^toJWXbt;z<^t*PcXV;V6L@3+BL7aFQGyr4}DSmWhVR(F#2B)@B+E>A}$j zt5I3s+K>t0)cCfhlOJhlecCqANQnm1v}BNYWVAk^fz6H6C&IGeGZA4V2)A2X`=YA@ zb!K#H(tqHY5IKOs5;3v5DT#4GY526}b7`?gN=u4-uz@Ud8DxIJ)dYvn{yOxjx&aOW z!eF#3SGy}IGienY5%_j{z)?G2^;6(XTTe3<%=IF(oqz)h5a!gNpGxF_rwRbnFk*=v zr47hM1(T^tYiLM-isCLv1%fiQ#85$%jm~qVO@GMDlt{{qmrzm=x7CdMM;t61zyLLaS(j{Hc)ApC%BhD6&wRVguh_kC!SvLX|>}%x}7OfIhV=5esr^_-gNCl`ewFFf`l?~5xq+Lk7l$gqF zmw%W7Wm3Uzhq5>L(#m__B2AGg1*S5!#8g2|>q~QFDV)nt{HDCVtC-TD23u(HTQFrn zYN~w!Qqt)25H)E$HE+W6B|w?bR<>^37*NK+Ni>Zct0@C6X)ui{)D)7yJ*^8hRgelq zWon72f-2jc=SX{ynJFQa880Da0+{fc(0>xCw#F*}L1i^nPzp$8Y6+==niiPm$YMB` zVk}pt1zv@eY1&Gu-v%iQ^Vk;<#ce(hP~*1K08kjdX!gK!Z=C|~#KU2#ZQbI6o2J4l zjLSsya~y03hLDNaSlo_w<~_Oh>9qlkqBvBFH24i#!)|N}nt|i1VPDe74JcY2z<=f? z1`=gi@|vh<;# zOP=_o@l+)V&zAsISDqrzr|BEWxvITES610d8( zmIMFC;E0i`bpt-N3r(IRlOi)TU?L{QH)C>KW1c06;({c_P0wqL99^trV;$TfLk7Hh z^($TV7R?bReqb)|uGOxkRex+ms2f;~?T=@!`lR(){KtGR3dRfEHJn3gFp1PuO%uS= zXfbC6ihfIX>`dF#7M!C^Qz-O?HH(xRmMiYRa@kp5VY)!4dNJ{ASgQus*BY&aW(zNXt$q5}e zV=(Do3fu!Coi<-I5_*zg=goK|h*(Uh!xza33;^hRP2rvcWYS0;ZHaHlm+=NGv7fPZ zMqz#!o#bL9)C%DBu_621p)@8QP2i+h8VWjB+AH@ZBN;G(1|rCIJQDbt!M5nieZl(B zDp;c|n#vYj)xZiKw0|C!3{fL`r^4qfFJKJsDvn?oR z@T>V0f)ViOcP1)bV}o7sZCjER#4kX^r&HOm@ zH)`JV%R}F-zD5J}=8tV%jPf3$KR^G&3aq;dm>?h6huU9Eg-_=^OFr@H7sc|~qG>R3 z5I$Q&Hok!!pnq7lAVYi|lvhel0fC(bwun+ITVsg_4>U{h{p=@du>wB+J_9ELcHar_(hr!Lm&ztmlk-tC8zMcIryWj!7pJ}`pfC+E;jnfjsAlSkqU{OOf z4eNT!DYcnsz_z&>Es_P>;2auo2bRlOz$9QyVU2DXMSrlU$>H`hcrajG{Ve{bFM#pN zIzwS4j2!euk-)au+BPB*1u+2l6Y%Ts+Uf?D18@NK%OZ)N7wLN;k+b3t_<(q;dgh6v zUzvdbZS5(m)nFChT&exUW)0pE1|f_gPZb?-#Gd*2_|OY+z3T=c-k#PQ^3!16MW`?` z;}YAj-+xZJ9rmYT*%!4Ws;}khQaOqp6(!-beLEV>&G&E=AK?+paNTh~@aIw8>TrRt z<3lGUKN-88eP z8QLPN0k@$6M8gijDB$kLn*fyp-`!bq-e>Q&uz#LEuJ2D+sRU~{S6|=2#y9hK4?KLAY8;UD?A>K{Ud+p5-d|uOCGWB6aH_{4UVEVH|yPfT+Lm-JRV;2 z_kY8B2MAd9yvLwD{6tCy|3;)`DdArJ(yvehBaV!hCBX0FBhAzAR*U_PSK|R2tNVW7 z=b=A#YpQs{%kcp%z!qiZ>L_TBmO-A-Eb!A>x}@U-&$mfJFtdO0 zHyvv*YJjpDB>yF0I#_5vT4ix?r_@n1BtSpFKK?zb0Rm|t`GdJ zlQvuYbmEPq1Fq&jrfnpr1>%ZA&Ag{xA4PL6Zvfm3FKRo|NYJ!ZbN)mEoE$uhw_}wb zvyNQ3`BtE{-m!*pummOI1daZPGky0WWdAmVc4JUAL2{T4~K5sNAc+i3!sEC z_+l3N;VAbQ7SRM*t)dlc_53vo$jzVDu!Ho8=CE4NZ#xk#NVCU%%C*n8m zVmsl(LKs#jEYY@k(WHbLcv}m#XU$7`fEpc6qzJSZ#AsF-@PoQ@vD|=y6@U6;RFx=B z8lXj$=TNw4Wbc!bobU&(cbilLtAB7_VfgNL(<5$-1`7jLa8c+<`1M}SSIpF)nm7*7 zh|U{+NA-ulcxpgNkg})uJ#7AQ^ZfNSo^*|WdB!}UHpOv5oz$ofDxPh;h{GRg!|;o! zE9L^;H|yI0cKItAq`1Pu1b;c7c(yL6PK%`hyfm~W&!JB?lT{Ff17sEHl=v_T1B?fD z`pwgt%?;U+T4(68D(*z(8-5Zm$l*Oav~!s|+I@aQfxV7~auul$9UDk62K{!=UQYui z?QzWirMbGi;E<~bUkWk_P|d*mxi$E%)2)`gkDK-tyT-a*TE8g+zq? zNQDDo)q~1PK7U=0_8G~C;~Hcr!l|cBc~`YwghMvYsHj2}s?e|5D*&hWzBH~wm2N6@g1!X9%PRoir$DzvRiPMD|}e4^+k8D zKj2ZsgRf&yq2j3UK*0fq=;)iUP_-C$bQAcMvjb|LFPj1pdywbEF1-wT!D?&WR*@kD zP>Ni#H-B%FHxGfq>G2V~t%F1gDUhK{!4e$*^`G}d70TEhFEIAe>zGoZVksO1(5;D3%%Mw{7>uYQQRQTj_2yc!MCaG}yIme50m ze{4tows@=KBx)fM{F7;;p%30*mvjGPKYUy-d#M#D7s{^bVza>_;<)3(@%VW7`pp}( zfX7Ys&kun6b+sSvUtmJlRGb?RMwJMNrXLG$<=WoX4Md0%Ab+AV zcM!s@IO+0+~2VfyC)DSKQ4#o$KxKK4K7>pqWQhM?{_4p7X;qo?P`M;qpb5; z;0n$=d8Yv!dI}#l&m>TMe~cGI?vh2BD1Zh6@sP4-1J?=m1FA~21Ei4QfqxuC=d*)2 z3gMF^l}CS~95ajTUlu)=`WBcxyIZFac(me@MReRii|FiekKQ7Vx}hxj*6izN<3NyIS!fN3B3Bd4-{bBI+N z2x#sgmN<;lsMFsI;k-|`*?&C!TPC9{tGLS9RAI_(M`?wp!`GM7mC5xmjxx?pO+0m- zN)Yh)p?~IwzidJ*5Lhrjw=oq0(gi18>prcOaFZ(you{@3jbt$+<%9;7Zxch{M58* z-^%3f|GX4c!A4dsGF$fI^)8kVB&j9k2;kvq9n~s&c@{!tmfhl_47thv7Q&{FG|q}g ziNTExvM_eV9A(C19AE5i1HR}eTTIEi6=Q>3-`#3_p6nb`NSN6_^6`pf!XTUwe%s$o zs-NKQILyRyTNc6r27eJ4UO=AnZk$0z(_$%AOb6fU27O|3mVhejWm|MPp}1%ujQQ6+ z6$ftDlqaxtOhDk%hK<*<+wi;iUFb-!m&bD^1r%i(8B_{r>ovQ?QueSmi2ST}^XGNH zS2`@I{8E=@{L8uJYn=|!}V^gGGh_n(9W!g910VwtKCU-Bm5$~U zQxzETrLY|!)qfrO6#Qeip;#A!^^Sjk{PQ=9t6YFXP#X~oL=}ibNvQ1jdH>k`0~0Cq zJao&AJg?3>pG0C9limI5$TRFu6DHAA)R zhkiZq>;7~E>5&eCmg0ESbIMsiONx;U?BOaCjiM_+oPUx+33{n_P=TSS%_4mbjKnQy z`7^p?2TTZ12V6cSQb+>SOwY+;dQ8Kt`kZfaQ%)fM#6KiwuZjwJ9RLbb+onaQEarcK z3(7Epy?qz6NqD4TUJeeKbm)(-`H2&CEhWmo=8l5fHmAW+bDyyUp=Xp07wHD{I*BJ> zCFR*T%YR7OH7*ci?hQ?akRLZEd4gSi0NwC5Wn;)w2F4Y`Y#yv`FrMfe2+Or6|~h_hX+AizLC0hiuPsa1L*Dx^b(Yka=*EsX7tR zoZ@tt-2O_YUWuAd0bJG!_0&_te_crKn#9wF>3;x8$#AOrEz?GYeOIiTR_1Z%Lq zm#RIMc%zPm=f@MNZ^_X`u8Lu=@TA*NnNZ}qvHCE&(4sKdSoNufDsty98;Pem+ZivZ zXn#yKZh#-=o{AC&SP|Prn3}bL8tc=Mr(FlS)@hC8*0ht-1ZR7Z170Co{`dtBA|E^M>mlJd^*E>m`j_i`OpAqFQq#Cw12{F zGW;xg!hDc=^fh+;agqbLATAYvXxy|$+BWko=wL9J^7g=aNPdx<6u3p0yY7WLN*A}$ z1!}>=T@L$$5Qo0o@Du9Vd?KgEK=}Y}g~;w8w{yM+h8AdididXZDc5+4(k{CeeRW^G z7Tp=fWK_|?SHnrDxJnxc=)}5XL5lx zS|m1#OUGv_aCy}b3yT}Uu+d7TNgGDXn1&GWK%VGV9)*GFI)mj3Q z`(D0+X~pCQI`H`Z^gzjWd}M4xC#vdx#l)qUA8E56uJU9J-gz!8IkuN2@qev09DCPo z$yne=hAugR_*(3iZS7nuCoG8LbWhP25H@rhDuxMR%7_6!z=c?_876n_(gvjxBD(tH z>IN1hCY7zT+m=%L=9`-sJ{;n0KU(rtcOA3irjBwVONEL1xQn0+Dczykl;Gd&@$4-y zR#@?u&Ax+(5mD2aIk>t)<$p_J_{i~}N_o0V`UwAK7jHK3p^9Gd;(ilL#uK3^5sH>8 zo&1b?aIqXX!GQH=5X)N@g!WRpUhkwRmW$t0sRRe^fQfbvLPjze*hzxUT(|D&7J!ew zhSzCt`1%MCz==6w@>g!gp%ahQExP;Y1>di)vC?8iLc}8Bt+;)7n19L9u`x=72fiy~ zU33?(XGN{mm8#p(1h<=R`Qhi={V$(3XclwQtr>O2%YWPTKjWQN;NZ3!uENf%%C;il zVU1-}zWovW{Cn0Ai(>~`;ux!cxqP%tNeR!F@328kqu6*VhShKuU%`*c%z zd~h8lHR?)%t@LGo{XHYuiXF#}Hr4hHNJNVolMjc(nP)~0%BZBgQCV4Im37K`G+sF- zWeHEvunLrvGb&^>RuSY~P()_pqGBJEONt3iR@sJjxPb3sAd80{gF4O%e;;j-F{83E zTIFSijMgig98Ekco5?FLb7jb9lL`^@8mA(jC){92mr_y$ z9Ntc%v<#RLfG}8FNsAC~{QED9>1ULVpTbVJ4pwspK)E^C|&>i+PeFhRBe^ zP|>kUq873WGX~C(&(IInf08{A5!PaW$cie^M)V6p$l)(KpC_5oVlwD7dIw!V&NJlk zy?`4FO-C}aG597kw294#*(7{mMTTU*vLXkCSoBhGW@4dypfc#eBgWve2Fjvz17&0^ z+hVs2dM#$<7Als**4lRS8JmM1qu3b?gI(jmVIoUmf*pt)Ct$Kre;Q|*9QKk7%cB7G zS$PD#dMMLE@hL!+7FLu9qgu?KILf!6>y#ZJLkR{DEG!~hSb#%^!y17vyC|?2AD}=B z+klQSF8;HZaf4_W_6LK>fzbibIodQ4d(M%h2g8w(9lo>J3o~tLTa@Nf2O53OEr=KQI-gzec^E+eA zOSx2XY2>n$OD&fRx!lNQ)<2#1PphW~Cvp3eyphWXxs-BwXM&OTRo^r1QEZ;Q>CxOi zTgm0R?_2g?uX>o@_Qr4FULA((2g6*7xyUs2*S9J@b#`LZx8QPyMH6cg8K7?swz?byPjluX`F??JlL=fYl!6w{U<)y;jAG zd2=qPPfsVsf17XDr7C`(UX_#Lm%3`os#z%glgf&rHJCY)#|_N=OEjPq6^olFTo);6JQV%JdD_^#ouNnO(pBmu5%x=}(m z%K2mmdpp;p__OdQ81y=a z1i7=D_YKA@Ud^kI#k14Xc820vyVJ#4@z2*U<^Rc|S?E7LUX+(}T`#Ym0?mDZ)`O{b zwEOYd_GW_*(M$`ufUnk}3n!YPmXM;(QSd!ecg^s(%ernbUAcC%j|3u$x&`9M>LkIy z0RTL_e*>T-QNm>n-+wQV*&G-?OlOPnU?8aLAhA7Tn@GZ=_UqPocNoRxeA>*G->#c_ zM3uOxJy=3!4L0Pw!%hj?AZ_@FLZ)R^PFEws@IgzYC)S9$pqfEPgm;eGx_B7Ib#+rN z=FH;(@ewA1Qyp=pSQu$cFcFZj;IyG5P!{F1e+uK_2$8gN!gRA1hKqBfErUP8NWj(( z<9J^#t5s9ZtHrdsDn|swFb%&2C}GFa06@)`Iq+PJxkcU9fTC*Qw4S2o2+E#-Fy+HY z$_s}iB#(%MaDpW**&s>qD`3VCB3WL}5{~+ayAwRjL$au-kr#!CgM;|vEL3IbG1jsb ze^&qX@Bd(l*liq0tdKyttDD8*{E%pBMPqh40@46cGDb(F4g*AOB27pvj)@Y&3@nus zRB>F=Th@|W1dlfEVpX6Gi+Xu>J)M=R3*}$~O#_XoE?yUZ|JwX|)=ZmHb#Z)Bya3Z^ zHT@#UnO)NoNix)U7CWi%H!we^Nd| z#2yjnvql_&T1iWh1evjp*cl2qo$07|K&CpPcR=2)$;DeBj@s}#00@%v5rIV3F1Gax z5I>n8Aw~4#5$leGkk$NZ)zr%oqnShWlG4EjiOW_8oY4oN%&VpzlYd!nb(W(CPi?@% zK!UVXAqW)J9U)+|x|)CdE&{g8f6)o_h67v>Ym=mCq%G7D;TM7CUKqO-icvtgXuu_M zkHU$)z(9t;@Z-U-;Cxc%i&p3-*f0nN2`Z#3&K^Y(MnnNF>VTyoFA@IS>v>q zmlLp@_T@+B){}tJ>g;KFmFh#&T(ACC6vL`j1AwtqgXD#Zl+i4>0Nj1-fF>9IJg}>I z^Wo+_LiDF%HU0K!`Q>JDSx9~0q*+d@)wNj0?Aytr{tnRMwz5|le=#A;Ym}^w=+@w# z{y!0K)SO^&G4xu-3W7-^LB3wr_2tR*3-F$Fm9mqjt{3y_>I5gcYQ9_FaQ(E&LKzta z{ILHYV}C?x$!G^-@!-C~#)GgdmRF=m*pG4F{h}X&gS@jG8ccU&!MI6WJ{j$8Ixf43 zk%^^FJ4n_N7`=M{f5W;`V8QH|^Ksct13O zCs^*(5e_E!yA=kQhcMvL0%`Y#WG9gNN4|lP>O&hKtzEZn-THMK*6ljr+I7IS>ws(5 zf!3}AuXm#+|41Sv*0WUkLz_bwYz<41-_Vat{z>fB_dwvnf0FzPU;vPDlYcq9Vs;1s zsf}DIMQm$83%<%TMrcgdKqs$WlK&_VQ&m8@C`s?Js(|s;v}c2q!c;0&56I)bXMG zJY9^JW(rFYf4AB0hSZSd1)=2N!T2AQb0h87n6iD35VKQ`8A=gQ21ohxIJoXlj9&CR zgCt+I#;9!(33AJlk4tI^vd;W*_>_Q1iOSEF6ZtHRe5?+oEaWq*50e$Te*OJx_QGkh zH~XRs9MTxV&0NB`R6p%r?6}FJ^^)y-$9I!UWp0(EV`}+wGeq)MR!A znEKpMk$voN=94go)UJBH2B#luC;sO)o1e6{xv`+Vv49bXnShuXh*`Eb7O?VORX4IQ zGSN0LQa3PA*W}Xo%};SjEJ;<+aIrEnFfubR2SQ7blI>ev*$y%~yO}$gxwsmbnYuYT zS~{Cr8k!p$Iy$Gfad_HQ=xisCxm;QhEwuia!#gOEmRQ3Pk|2ClHfQW4yu0i3TBCbtBlAa_87&x;@9ba+E@(8J zf7MlJvdOb_nj3=~Ot!QV`mb|PD4avGyJr`9Le-80K*=hJXdFFBZL!JM8b zbBHUDR@VQ{kj=iUF9 zY99Twj_dyJ1s6Ck6%mTy7WqUd7ZnD^2Ef z#*B*wui3KF&YXWyKkK4tGMn4=o^_J3#=p`<&S}gEv{+o=_OR#B%Z=!Fx}|jNMXFe=fK^<7&t9 zrWa>9{pT*4FJ@cXS@&1KW&hpon*6>$KV)X^m;ZV4>H7YOt=1FmODFCxb_^=AUNqC= z<8O~&VM|i1g2H4q=l6y@Q3@4XdCtwKc4FH~kJHTm_wT7#yv;4Q_mX`~H|Oggu1|BGdY>ybFQvGoC^az`#L7>~;wmmlEGnre VN=@T3F*G!_u;5Zvb@g}S0ss|_OmqMM delta 17224 zcmV(@K-Ry>mKmIt8IU9cFfuTgkpTuMf8|`=bKFL9f7f5JZw6y7jQIwna#d`{ihZTz z?qt@vDl$_6cR>|zaIMe+Xn^v4VqzyhRn<%eA5g$vAQPft(xue%3KR(Gpp_3y8e z7k^&xt9k?H8_-Rq0Bawd9Lf8=|9 zy1K|z)a3j2kT=DC^W^L6yNm0qKYjDoh?Rg*jFC9BFb$@BCPe~QLYY`5>1r+0e>lw~ll12*_e1_vHy7-*h~&f0nBZ=#v&Z zBypC)NXbg9bQ+5^TN#_gR*Tiu4toB)zmRFv70~-aM6{OEBDmG4wHYueKp(%{#omPu=hO}8&v zoJv?09{AlBhpI**o`}*df0u41Qinw-bSbpIL>7za=Gbus(*_Ss(E?e=sw?+*Jwb9p zk+QK_U@9^nXWu)j{C5=qk{Dn1=(s$$=s_y^@(&HEveWUwJ0sBUv%R0M2Ui>N&U z6}w_)@1UuR;3R8ffY|j0$G$H%xcUdAnMTU_rz!HPY&%#z9hW#sf2O>ZI(E+U_Aoq> zO5&azjx9fT`2#J&zvB2x_#Ub6L5ri;imA%Wy>Cv602h^e=y{2o1HEA6B&siri0G()iBz^RzU~a6CgK71`BB1bw%6dsD0Z7 z4wG_`I%>UD?sldaQXJC^2gCSa$c^tM~+#mkc=+0|&~6AGf^X&9OfhNj9NPX0cG3 zX$veby#CBTmGzDv+oEgnECbN^0XCEE1uIt(F$!zSTT*&(r1pjH1)G|8$Hu>+Vh&;` zCUgL(e-v)OBbA{@<_)ZINA?u0-5#{y1rCd53rof(A&W|1zAGy*Ma8Cu8KM0fF7=Qg z>kR{xK~GN-Aek{q3E(~HS;O{->;|I?Fb%A~b6%Z^4tcrdryA|EAi03I8$P>3P-6JF zQCk)#KtCW(#9HzuY#pw@!x!I}sj+x4|J^P$DW7u@atB-5B8mvTUDPIL<8|bZtqYmZVCl za)Z+3MM>iET5my;dJF?a9`Erf8Ih6MlakNWO4%${CS@|b8QzwgjyPd~Q_!hv*H zf1ofd+AiB5tgLUqV1FbdgnMl1Y#@(z{Ir!=fJ+^O;hs0vM8qWszMnTYw)LN z3B}0~v1YgpC|EFLTXPL>r?q2Q;yMC|*rovuM$^N~ZK&mCT>!Sr*Gm+EAEtF001@og zB`Rzi?E}(**ThA)USjZh$on^gUH99re-j&23qEd$Z(NFJ2_JTO$7?UPOLTz~qBGB_ z{0_h$X=sq=z=U;h9_Dv7C2$4+U<2Z}?+Sd};_MPmEaHOWehcbnVN114dadhCK<1v= zS1DqnJQr`+fROSAZMiMc%|On+8R6H&Gc6nzM7(@(6I35xwfxw5U6BB@@~tn-f16$d z!@iJZT_7yUVw0*s7y<~~FoQZ6e{RY>VLN(0mQ}}(d~EQENWuqi1bo{cx6&Aq@k_Zo zRBX>3K>H<0lbMUHbSFteDev(JK7xxd@W`+LeLk-j3SY)chX+D0&eP>9+2jXH;E0iz zOZ22Bw$8f(v?p4c!J)*rfq|pSe;wBG{ua0wSjZfb6IK6}ul4=`zx+qhJXFOJJx;|= zc>c6Sb-VUQ1Tln%1sZe_t`UD36M@qXoIss-3)UqCh9AJcH)-L!mPcl>~g|E5A*+TLG|`oO*&yQ*Zs<${8Mt|*lp z?r@;0KP_QXDNUSa-X#YMe{ldSZ5Z==NXMJx0&0MVpnTx5mtK510qh`|ESCKUd39G4 zpj*Q9lA>eY$s{ZXq5Qvx85@_J3N&(7B?ofxuzA2+HE@2O80!t;v zHA6ILTih1=ZS3vAC?=MyfYC8Pbq&ncYHj2T{0@%Kf4N6E;e^okqzvEU ziLIL*?I-wP;gAdv5tXxc%fjJvg8&uOP6JfXaO2N)!7c7lO|%Qg8@z;*I^2=c^JXew zs071VMc%Nh!X+RR9Y`@E;KM++6W$B>ZI3q~+^ix>7Fg8bU3m+}6)l;!#YXp{ne|mzxfHT2?ijpaCF!PDf6xU6qKYd4j^}B!J;twOKkXFVi?)-3i zk(?1J9kc@r|Lw~`Cs<2UgOM!(){F67qu^ApmZ$K!e(z7I$oPDM7B zW|Tm`V^DP{z0jbBYq@N&ZNhIGl+vyh`-0!k_D$MYC1ONGIwe#p5zADL8eQ|~JB&wW zWEJ3zTy&()FS{+57M)tq`CgsfU|{+ggDc?mLE!MS#@MLu5;d~pjXU&)nC z!Q1n~`=4YLtydxN%ls(#1&;mgv1Lyu2_X`ALJ7(nf8Vj#q1=PQWD{u#2a-~R$BF1D zLjjT@1;X|F9q5!=#Wooedi};vci+>7QHf;)1q=e)>#ZLOass=(xd1{R_BH-IR>k&? z)|Qaa&_PW2^kNA|-3~dg4qY=UzTw4E_94LoN0kHf;m6rxk=-0C-;fwANUfI`%ALy& z4YEWFe-=%l22!xPRK`|#TRI4;W%^`?0HRues8_@>s_;nxcm{v0Xey6KGRzGTk21px zCcMHmp`7d?wd^rSa0*Hcvy%#hq*Pt(Zs3o z7~ecIDexf{VnS@O{rnkC0*FTI@c_N6+uiqW>@eh|r>p{48+VEPJC6zsMQxtW0&qPw0Et}Y$?-5% ze<_MLD?QO8%3xk;(kD9~+JKuN#;vY-*fFlX457MUEgYg^4%qe45EW8E6yF2haL_28Y(2@#GQyFNF|XH-b`;VR#UgSkb==}{RC zUBQr7F+=I;B`2du|B#rs!S>lfBF4r^f10k=BDR@NZ%b~Ls+Go=v%*&3VmQD>z;xvs z855?L!?X@6h75=6TmF_L$=t+X60+wL-$v^gg@3RF&$ytRhC%V3{Xj#Sh7(?+Ug<(+ z7n%21`k#+% z3G}O2WRsz;FPXY_lUHP&^+-$>q*4Rc2%*27$1!1BvKaw_K0xBQ-~T+nUrM7pH|lX2 ze9w^92Pyw%TMXVfLf|n61v`QZ@-e_ijAbxvEQetc9A>w83U!L2rbFJmXj^ZyL3~() z3Qoeq4~A0KT}f69&KRe7b2_?BfBE+wTMK`iLG~dmuyF;KghRYck29dyedb~0gn~w$ zsy$X@qb@?7jclQrapPuVIa6S$ozat#^w~%$Gy{||YIe<}g-{|of8dnw?+WsDeCULE z2F(bVQ@X;)5K*z9C4&N-#4eC435W_n)x_%FC3U?^+Hevt-)xElB_mQpe+fp#k32)l z!9?f1>!UuXQ#fX`_c0YFWgw4JourM3k*bq07CzO) zF1_OPodzC&pOIIb6jKCH1~+^Bv}Hdl8lvBi905>+iz{l9j8QCMQ`US~o9JPokBqJn z4Fn}GhP5M|J{k~w%DLepe-6h>DWk9XXOW(Eet_%w>As(J)=U!lh?4;OG1}Qam)mcR zG~lIq@8egW5)VN^Hxn6ij)gs*ojS_|CVMvx7#&P=C{}^lDSqbR`OJYJas)VU+70{} zJOy6XJH}ZL{7T9w)dNqL+WJh%(M#p&2vT+LHBj~?iw4k*XXs98fA1-f)QO07aMX%z zz)DShyu0^#-KA_Grdap&DIq#@slg1AsXL!Apumb3{-(f#GxQLKQa`#n6$n--IETvh z;kWw&{*)U|%8Tf2$uJ8&yJ~QEg7fYn8-#m*I)oxJVtqr=3`{ANoV;iQ3Wqf=S^$t7 z@b+a0)ZQ%|Jb}1Fe^>*5;W!M=;Jlf}dlDuc51!BAEfY&?5t-@C2NGrn2FQhxuTv{< z$c3f*Y{FXpapC6;7tYQnG1g{A6Y9AokL(b5yLPe|R2|nB!X;>tBpj%3c@#UVlgzq zNq2Szm;BI?@lnd=bUR`82wQWC>GOSna6o-}m%K7Oh4p$<<#g30q4gJYrr=>pzX4u55pG=hJ0wfGjPWhg)RcLTcCo4r z7kcUXD_%jMgsJywi})^{v(++*C5Z1DepBHcyma1{=6t4aUe7BgJbE|#1vwdNfiYGf z5gObAoQ?{$&y0$R;e}CMKk5n`LT}f`*udmbv4l5d>S7T>yyv)p*JuUowC;jis5;`Fc(OhG7#oUD>iP@@dwXBEFWZfd!N=(V2mIQIo}e z{Tw^+61q($bUrPBvM(dX0R0%S8x8#}10(RTe?W~rPnmMDoDjBU)i%#92>?2qC2#^7 z-3V1IE>_HpH9BEyU`Q+zK_4;Ujc{x@$nMQXJwK3Xd^?AP5M{|R44nfs8aB)fVejSK zMyvrqrGOSeuTKc;$aOurbiLo*Hn2t2q+7)KSMy-a2u13{tIwT+eavhZmpBCf%G zNLOpjL%1=^N24hiEL{y+JZT<-2|Bs%8&!hMAw1AvB327RGANYAE zK{@;ENeE+&PQqL&ZiI}!=!gKG{{MMI?D+{1jL?F`5c6j#GZaV)rsd5-#AF&!f0dxt zl(8Wq*nh4#K>Asq!t^(|p$c#Laa~AMr+nKg+!XZJt)Tb@zk8(s@A?)m3!J$MHWm(~ zN#Io_(Ffd~4><}bbK^eS7czqqq*ji*P(VX+a2tO1^?u#{egwzplD|l&FEykNfpbmK z)m^#Ai{QTN;ByLm{di$88}Ie^8qESzpO~98sJ3#sY;RzZ%~{C4n&GxpWm|kJbVFH!#-5Svzh@v zCPNovIKWQ}f^wP`?@5C8e;)OEQ3*j~g&y0m(@8$g>~Z)%orQjJfDa^dC7AbAHM}N!I^&B9jDi}r~8P5 zPh|Z?5xylt;)GYU`K2mvyLK#rgNqDh=XKQZZbU!sT~i+qa{+uAOS;7N&m@d=UE~FE zoG0@Ayey=n&Gn)9e=irOe~MclYa^CWb~c1(DSh*y!ne5onwbjRN3rCaVO&~v_>G{C z%uhZm@J*0C^bsq+4rSOzhrDS4)?J=HEL#9cZUVqFfNbH;+-Ko$0N}$uhk5>eefDLY z0@&fe77RP9VR~-ql7R-s4m*AO;?e+b>+wYCoJoz={&JsBf8=^R56%m_1N4aDu#tG9hCVkHs{ig_H7w@Y&LEzI*>~D0Zk^f&Wm1oP?CmeYc!wUYFHu%2* z{D+p9fMVR%F^`)0&$OR>Dyo~s48!j#dIj9i>lHKLgm(Oi1O2luSPo1>@smMxaPXn4!_1X58|Nx-uT0Kg@_sUn)!A@{_KswrhNUH*=LYu6DEC z?2E+(aZ5y1xz08=5f@rlt#h^krEaKsrr63ijn%Uib&SMCq;5yl+&j*&$Wug45@}WN zyeRm)?0h-HB_}l6l;>?hOFgHHzYq~ddYCLL3G~O=7eBDj0I z68DsEPX=z?pwbL}{H*dap^+(svy2`h0GkbG43yor%H|yEk z`L?gHO6)=pXW8!dlW&eu%5R0GsP7=i3r$##N1O>!w7S zX)B|x&7w87YK&=o+KoggwlUF4lx1S-8V67NlUOJr7C0>d=6uzE`L-!~b~QlJ**1@! zDFtVVSTL4ov1b}R4nC2Uz^h!(ZFDuz3EKaz;8Lckta=VzvDFQDsax=x_8a4C5!Ukw z08`jrU%PsQF{nmsoGKya8_2P3O`>^IS?o$!ruh&lGxu%}9UWlP9u1^2{y+ql+qze#1e7^H9JLdhU{}CPDTz}VtVAU*@pCbsVHHY(NMW! zjzlRrjKq?EzevkH0xrdxO_t#|oc>(-$eXn8LZrQF3t9N{cebMH7q z21??j#989GgqcygGELozrC35W_1Ed4lX7F(4_^iA;NM*iEl{nV-k&J*Jafn|oVt=di!s7C)j(NTwYO1fHq z*TB70d9k{tEpWA>#fDa~5wG=bx!LyX#qzw~oUmrw%!l({9{yVEHjw%k3pGD2U#R(p zp7#A(KHMFK{^u8_p7+D8Gdr1dEHIHo62vuW>87m=!5pHs@K}Bw8Vtg1&cHegcA6Uk zip^pxme9{Hw8#23f2~au*S$QQ`r~PTdDnQ@Azu=u?8B%%gK30^GBfvIqkEFYzg9wEy_qvU7>kGyL#4MRFOy098m zNk%5?<6CTQoIVj&1)qtCkq~ZoP3?+*t`_Rd z=+30UGa+(-!4fgCx-E%uL23B3=1XabMoLSHe29T8a~W)Y;cCL+YknR2RNaC@Ko~~5 zvbDXDG7GI@BL?68033Dmbw35pwDmM&AzUvq+X*v7_r2T(gt!- z-ejuM8VwmxQQQToKv1TZ7%HfLVWaaLX%jLtC6Y4ZC6pB6wz}0N42k3|#>{hMN`a$S9Z_XnX@<1$D^d%NQ(Ri)zwDkl+f$K$PJ8L8u5bdp807wYZIAI=&OpPF< zJ>&-Oy#N*>WK5`k>0*IMyC4)e%G44`1vTz;o+9l*=A}ea=DS3bA!XvNExH?M65Tn3 z=V_9HRKO`yOE?u&Szw+b3E_$igNe%vyoo5I02iG4-vTKEsp;ns6&hUv>Y67$X*^X) zf#++0sw>Bl=ZEPVT#;mO)AJf5M^`J^R0p@jkbzgPexE3I@z?EwnM5X08h!-3*RP#CGQ2f++JsyZI#(>}QRHBiFVD zoyw8Gr*B$kK4&C~CV-#uNR;;MOszjlO62v!)6?UBk;rXnyY92(L=K!Wl=LqJ?tnd{4hDm#Ym(T z;Pr_i`_!Q{B_55Jq*xjXoh$8>{hW~uOrSvo*^Nhnuj!kPT)EF!A6bRQsD?~s2UpdL zf``_Bqmm(ML}!)%l;wHK0~s?Kh?FCa9XNevq+9mKL3?;ddavoAoZ(l?DTEPl~m zUA09}f=bITj_a>Y8(9hn;pozGO>--4B&}j2wnfLyy(In{Gd~Ue3pMZM<)L4$zaj(m z>W^JrjPe%IpPT<-4ePEvCCCTyp$=D5;nO)Ul25YwMX`LbXc{IC;d5iy#<$o3j%5pf zGU98moKoQwFxW+4izv0SHI;biK#LUL&VJ$+Yw+>+8Jr00zG2Fa4q;=c4|yPt;Gp0S z!_A}5+w^&nzdy{rnf)-k;sL&$X}TCd3GeV5r)7j8*rFrQkcMbm(e<2D>N3&5w%M92 zQUlvyEg5hN%Vis25*SldqgzE0ENXUtxZMm72FBIR;&1u_j8}~{99Cjvudj*(+t$=g z8$_ZI1Hhlaucd3NTPz1~fch1Y#LtWLy^zR7@drL2-Kw5B=IB>uAfT-sXSG_Y;+q?_ zpV+LWJHimc81h`vfg|=L&!>kz5I6hf5Qy*2n=Sikn0MhTip-?MHXL@7ZpXuad06#D zEs5)Exw=%2(u|6d_}si6jb`Tu9K}aGQW|HJq!jUSQ+f`J0D8Soe?H!wV>%C;A^t+BEZS z5tfb?+rxb&oxbar)aYk!d6bs*Uu)=WX*u+(!?2d;am5$Qxqw3om1Ytq1kBjdsn@ca14^Yr`m;;@(1IACLa-w*OU^rz*9E1q~cJ&*<1 zk<4rz1?|W(geNi!^0WzE(s9D`yCfmZ97wzlIZyP;=ZPP~5#m|H=$qZ+w%_%88b&Iy zVJt4qVippHng{~XAl+hrU_mUyMnnYQV7-ic8g`>!u4wp&AZ99m-|v^FfHG|Qjy}H= zsp0E7faMfXcL);YW66h$h`hghc_~jCUNIjDj<%DY-iICmqT$3EIId>P+~xUhr=!9h!W?Byx`p7%q4zg>z3;|3(FA-r8~ z)yvpBwGTQEDqWcg7x0Q(7dCBm*dNckeqd47^A*nzJs0H0+x1?)Ekm0feLBlV@&Q-# zAJaCn(}K97P&042*Uv$7u3iA#0xxbm(nx69skwY&0ZtBHL$_m<8?#Pa+4(L&YqJ*( zW3dDk#0ic5NHZ>fw{i$=xRZg0)5CB$-#^5cULKCiT_44#CoDh-Q}87$^usCKV^~BJ z)Myp0Sf}SNNkDe~VS^pyPdrDX_59s32p7`qY2V~40g^s1SEn=c8+Wmr@X;U)s}q)Z z+g#A3j2gUc0<{;-%X)wt9nY)?v)(RWgR^h>7( zN`jR=zaOyqr|r{Mw|LSu{pFePMB0?b@pV$8+N*fB=^~DNW%DXf$=8J^O>n*=XT~7rRUuQ>V0RUU{5LlA2AfYB2fu_IX9IHZ z(Eq$y_xn|UWhTOHoBvX;qm;O#yr(Q%Y#c!L9UYZ_H{S`m*tmfhJPemS4ACu$F5Gx$ zI-Vefa-MY>dF(nW2>lF46kaygj(L)k%BN-ny@20vQnuv8IC5g}=}7Jnj3WRSj!&`s z5q!;f#|>5cn}EJ($7r`bUHf_;o`PZaBU|Z%#q#rsFM|%}?N*+~ZjvV*ca$e`f}-?P zDU29@DRP8p#~k92t1AL57e+S#=xx-mZDdk7efv1QX|~a0Mh8EUi#Ap3!$}}ieT382 zA*j^jE+1hu&g9?)8#V5xUUqd2jJJM%6r)-0iQ_$aDUav}| zR-~8768e^x8=c8Z20ALi1;LP)-qh_p4phUWA9lOV=?FQs&WQS;7BQUSHY^>Yk{+Rd z-*peI$gGju*pmxD?T)7niH}?EZ}9`*bgop=2+T=Ile+Ev9J~-I#Ub=n;t(RnIE1L{ zb1y_$RYM2a(Lr|egM0`fh`em}q1D4xmx{EQ&w3Thnd#P4bU~O|g_~^o4k`Ou62K~& z8t)SI-15ChRV+mhKQ5yt+#HYR{<^<^@VFd~d^Si?iZ_j?-R20}ytrY8>6S{g!s`&J ziN5$UC@iqpFFp*(G2kQ_mh#IcYRB#7cseHK8FZtZ7pTr{@ObtM>2iaQMoNj%o9vHt z2yuT~HN zy|j~AiNmF|y6Z!f$wvE5e&s-alcF8YtUW;6rK&U>JW^S$jW+38Ktg|Bt-8PzoUT3w z5;3j}uIwp97<9-1!PZo64ao5z^*y$i8%8sZ9`r~pF$ zoIu#czeB(?<*4o*4KBk`N}~8R)JL+;T_tb;}v4?d-=deu$}8{zDkLc@1e; zU+Io2^uD6MFjdI-a z;dFXDe)a0rmNenE`saJ#ep4NW`)8QYHP`;egK?n)!CJ_nxz5dh|NQ37_ww}h_ut;y z+qy*nn!U<}MTEGPpmKFi*%RWB{|1ASzWd;XDP^1ae{6=~FnoORPFGHi=Zb5;Cp@1X z&hILCEw7Htr`_=3yuEwH>@N65wwWfRVKNu+mk{mlkFczWs-A?B0=b)_<8lt(JbB2$ zxK^Zam6`u%v|PM@+PK)^RfeppeK$#qGKo6uZ+UBQ*1V2>J31I*os#4qI8(lrg!y6% zt;4#P8?2zYkNqb}wH*IfOBMR^a3?}set<~jaWyna0&p1>2X<9VnU;1{1d9hiU#5wrJuj2tWx+J zsa&)2NjzK_I0FsZ)sti|M{!+DGPc3DCDL~sFEA5( zp{yi=IF(7;J`BJP6n>fOo?{K!|EIWOeWJC0m#lZOdSFSdI6Z)e51Xh~$;(3kAEK|tRT)Z?!#jjc zKl3IjZpkNRX9?7>Ua>{j^OcJh zVa&fCxc2aFvzM^i$K(T^wqm?i%dNZzzl$8{&FXZ?WB^5(rG`p@w%&+K9I7gmj}iGb z+RmRg{dUdIvE;ni2G4ja)Fnb?SZ^r=Scy%4iGC&0N<5TV>5v|woA)8xfwfy$tZz?3 zypqi@ILYkTaHw^?0)r;|!|AH$Oc79WuPL#C_!O2WMeiwWP7If+YpA}{o&zunMh>xp zwlC_nsitq_&pJmnCn@uX^6?!-$`az+9Lzq_`MQ=hiVPXL>l~dP*%u0O05XX1akG_w zsdO}-l&YYJFNN)Z)biM;;Gen;#kvTrck=t=pTAz*q_4K&c@w^e3==;bIBBqpDG7jN%oUGucas-qs@k<>b%7NXAPz|GH~=F>#o3#n zX1G-T&~FBLJ)BRF9_t{q430-V=al$=lZ5gIHn7K=Otgw`7)eTsB6hpm zFcP<*lh5Rm9VsEe9ccNSNMQ+ZGd*XE=_n1e?sLA$PB}sRsoI$7;k5b^fa2_FM^0Hx z{ep`l7vOa)zBAszeEOL=0S1!GVe{wwJiaN9`+JZkO>mJoVI*+>n4a3HUf zc>*gb&&DZ6$*xKLnR0JrDgya&dk#<7)d%Q?*C`vro-!DVFm{F8IX%<#r|EC8cP z;XW*f!~WIR?6K{8ssIzY{{<1sDpb0#32( zlR2g7D5w2pn0g)5d!*-ZkZiopX$ICQ2vQd}WnA;MwR~-ail1k8^t3MK!^?VeJPn(7=KwiS=ybvw zZ0^IQ0IDEI9gFA3Gpp~Aql;V>!`|RYcfK+{IuMkcY$r7)MZw0pPbJ!aAb0t)4e_*O zJL4S~O{vB$_z~_E)gq2qk=R8{E!seh_36mdu07uxZA{3mY1_)h1j+Ui2eLx4{P(Zr z>Ac6+`+oUuv)!Dea>z|Zd;55E^436H5gx}cNldM+8t02_!su#9v}nbR6h}8wu2iz# zhHFVzYgV+*1tq^_m{7KVm)y~CE7>+xyIM6c&jDs%lWFnM-+Vz)u-t?Y@;ff5=loq}|!-wWT&tLsJ93#KTu6Xf?zzgjZvn`jT{A*6I& z9l~BxR}}U(Q2ktY>Vi)<>ZjzcMkF1Eo)ja!EpMJf<-wo{0*Y6EeRLaHpr;GOQ{|Pv zWZg$5NV`y`qfcwvC?n4yQ<#rZPu|8}K2EX#SHz{9hyC_hRczT1cT{#~9$zX72e_2O!U>p$Ovp#_qf)yw15}eA6JJ^9*{5Fez#lRln(uiIqgU~d;uDs zfD6lW@j~3GUu@Qr%LQw^NNN<9?qU_yNfq@qc~-jE<;C4{6$)loS!oPiU=GgvAU1-} z3}W-+YS=t-Nzal>4dsun=6QdycXRa+xn}P%0vlvp=qHP)TA^+q$^UnQGp2HIxE~W4untOTOu_)8FEnCZwgr(o*U^ z?jn>SCp=Vtms0%O1D(AEMGI^BvOO#jGrpEmIGo);m0M`^C=sAanYwEV$y?aq;Hf0H zcyYfy^UWhamI)E$ijj|ZlRV!|f*xF~2F@@LiKIeyQJMKadr>$(GNxJevxd5}iNEpZl3(x$vz zy$Zp1)In2NIaM{CDSVckO`u1C#;`tyU~Us)xb-1;M^TA}l%aGXYx7>-=)wUPE}p{I zhiQ2&a#H3s^F2{s)-hJf!ZkhyWISdVeR5lL0bdns!p>CmSKyqwzWCR5{};7Z*%Jz7 zZe(+pMlk~pv-nN$7=KM~+&B`w_pjhFIhf*Skz5!9WG0)L09jxVdx70eeCV`gr;(0i zbjwLRzkXj)YPs9}VU457?!jV9Dv_^>WYw#polqhQt3(o7X`zkK7L64qkkEuTXo7GQ zg;ByKG+GekjT1y_V!Q~}2@^#iG)W}wa(52jq9cu$7M+@q1b=>N$9;OCz1PC>2nnqf zIvSeTAao)tERU5SpM){a35U^aG{R|NJfkqekdMN7jH|5hcpotyx->B+LBL_n#B&?G zAP+#SgJo^B$Rj4;#t0r-MkQ>3#u3jW`oc&y#UP@^h)^>Efq|;gql*MN!pKlKvRTN8 z2qYmvKEXcFF@G^4*h?!Q(iqR7^?2^lLM{QRacY8}=*9}z)LR4HAqOBL;X9{cBUsuK zdeI7Bh5##KGJH}zRY8yqB0W%yhPZ1^z z=maPsfPV)m8v`x*$?2&m&P4HReO`;=rFga~XU)8>q<$`b`f2j)y$yuF@LnnPnlBY! z8on&~QuF1KFSmS|^>63>+v@qjLCo$T=Y09dmy$27Pt{6zg~AJ(~M>E56+H z&zAk?RS)xSr~eH1`Y>EO81AZnvf#@VUrzdw%YPoyy{WExNb?@%^-h=b{&Cgo*7VkI zwLFa9?c#sgmX?x7((?SGn97`)iLr zTjJB>|Q0_isIG0xnR_% zr+<^;{O+a{#qZPWa#H+KS4~+pD}k*I!AbG9T-CSBS-Ij6k)Qmdyqr&euD^+Q+!tj( zXD%k_V2Ll`L|d^JRaK*(cO2<>NcgebxVG_aLv3T*CbUg#o7@oxxZJe8xVD#z$rkoJ z)};8kUS5{V3`<=UzZI{GUvLADcENhg8h@y7t&Btn(orfz1*fzO@Pg#6OfEw1?Dj*0 zK8rW=>QnLJ^fZr9yvQ?MoE86k`_-1JrdUa&P3p-s zhiE35Tp*@MrWFV$GQcb@dYL@qdm$b!!{4szy1{T|=VqS>gbj5M#E_QJa|{Il#D7`? zK!{=-Qzd-=ULdnMFnpZO7URJ{P?s);YfKYyc$Btll{JS^T+OG=YI_VMKgO}R)!!T~D+j21vVLTw# zV~Jo_d+aHuQr1T-5s)xvq@p8G7Jucma^vA}o}>XO@>nF1`6flF!M8jX38?g893RSM zwQ9>00tKfNg_wN)yvzB;}<+ z5|TzlLfFBamaLIP_!ThYN0BVAW=Lbqcu2hS(sMedgLIrc_#mOG;O$L8KYwMpY{b=n z{rf-A5z~zw2^A?=QQa;U7l%Y+7WK(U4`(t!l$4U*r6Hm^k|bmn$3zKn21_+W>HKj? z3wt3o1Pwszx3LQFhDE(RyP3{P(Z+Jnfu@1QL>sV+zkh3fJ!_^-DcV3jDPDnUWJ|wt zylFdLf&|2c?l+Q97uUZL6n|6q8zjJY-M-?C#@qD`wDoR%gJtG@e*>}5i(%Sh-vQ^1 z-3>BMQoR&-f$pU^m+WsKc0VR^{(elynSXafoMZMQ07%rk4eC^)iUwc(-!1C*E?i{Um$Q) zbA*A->T3S!yBOFuNq;Bso8aJrf>e>KMpDBZ9)1yM_QKdMQH%n@cm*<%dK8A&3l_)_ z7$(|R~FRI3JsRQg)onmlIXZGXhf0| zG^ho#H85Z-5R0hlk-az&Wu?Mj>N~dW0o`+0N1#Kl5|DIr>VLw8%OFG8pEq62uWy$R za!62sqz4n5Ezy>OxWMbc4H9)p8a=32R!{ArD|op2FPgNkoNf`wWFCTHCe^gbVxa zeXE4-cq*g+E`Lt)z^h=HQSjJ34n7XPjVXY|ZbHII%0E(!IlP@8FH>n{q)lA@vC?ww zKZWc`Kxt*NG`vjpv1x8re=CY%<*EU|0+)mM)PU<~8e9PG-nT%baep4z^}P9b`vD>P zbFrG2MSns}NP!PWq+;7D+|&Oj;&vkMgc!;|Hs&$ zP+L;cV6j+mUuNTuSytdPQY7rhxbJS&55a*CEr$lvEm<&bVwX=!S{;weu47~jT&Nu+ zs|k$WJb!|rs}yK3yAaZG*>&VINS@M|ac{E1(QYer4| zkwS2!4_xGTIfGD`n!q)FML#n2C*+e@9cv(PV1JSS319$_aZ`WZy1eY*{$q|?F?vj^ zL)@YtnfYS@NX3~x{6pgZPB2`&1+akJGt!UC{9y?8e*{{T|L4F+!Wt#5q|<+8-v96b z2${a-YAvfDg|UPgffGnvJw0~zGMkNCjv?psX#&@5xg0~-p&q_AWD0i393RUs)5Um6 zCVz7jcAI%NxPr{*gPegoWq(x0jig^<$b5|8lMyBa7==M8Y~>^6y7Ei8%*gSFh@{-)*KwwyW{#njAcu zBFkkGIP_t%NQB~^Q;>bKCb)creN?v3>smpv_;huUu!mo=o(2lTiF)e?3bSj8cA&6^ zTO0`4#Rvi$1`2zS_JM|T2I^tK4HC8~<*6Aa9Blp{h+)F64OPR0Rg~Tj#LWKzK||-y zvk2hWeerWW;~bl$s_Bk~%)-r%h3$@oj6lo;#LPgGp1H@?h5X zBsaE$jLuF@t|sPAE+(diMvkUtPL38%X3lPI7G?&<&c?2eZfW~8c^?W;leDD zvso7oa42zcDHS9Lm}Cg3xU{T&Kda`)+}d@wH(&obSHLO4uVq1|MuU?w8)x`FmLSt? zbx$VF7b$O9G&wbI9Jy5(#PY4%I?~!L>G_L#Yx%^t8kwwXSoEe!Z{!GbG+fihGsTH> zP2<)8w$}?}HU%(F4bWCh`NI*Kv!9nOk)^CK**51v5&N6AM2Sbo+$PB<+WQ<-@i`zN z(@Uz;L{FPwuZw;-X6H3bi7N(s%YDb_B4Ts4_(*< zCH+!-J}SIvt>cVk{ugp4rfadX`vEt66r>Gi%uuAIoW%43;L|;=kfEbN;1z)1}#`c&4n=j1Atk?2EtV zoFI#(1zr!Q9MWtJUN1Q{X#JFWi+c;DIIq9^%^az2f4+K^u;iZCE90Kro3os4V!OVr zX_w9HZ&QRT|DFn-tddi(B+b)i<)N2`*1~XzP2Da^FRr+!u`_QTd5Uv(G1Yn)h} zx25LO|I^*!S*x#vty~)vy>#2D?(n!hzu2GM7n7fRjv@YD{OzogI}(}($2PG&w10kh W%I@h3-fZ$*CWfY5s;aL3Zd?FdO9Y7k diff --git a/paper/ltl.tex b/paper/ltl.tex index 7bfe8d8..a3d44c2 100644 --- a/paper/ltl.tex +++ b/paper/ltl.tex @@ -97,8 +97,9 @@ $E : -x^2+y^2 = 1+d\,x^2y^2$ over $\mathbb{F}_p$, \Bigl(\tfrac{x_1y_2+x_2y_1}{1+d\,x_1x_2y_1y_2},\; \tfrac{y_1y_2+x_1x_2}{1-d\,x_1x_2y_1y_2}\Bigr), \end{equation*} -including the completeness fact that makes it branch-free ($d$ is a -non-square, so the denominators never vanish~\cite{bernsteinlange}). +including the completeness fact that makes it branch-free ($a=-1$ is a +square and $d$ a non-square in $\mathbb{F}_p$, so the denominators never +vanish~\cite{bernsteinlange}). At the apex, writing $\code{accept}(A,m,R,s)$ for ``the extracted verifier returns \code{ok}'', with $k$ the scalar produced by the hash oracle $H(R,A,m)$ and no properties assumed of $H$, the byte-level tier @@ -287,7 +288,7 @@ Operator/consumer tooling and a twelve-lecture course: underlying proof corpora are in the \code{saymrwulf/*-ed25519-verified} repositories; every claim in this paper is re-checkable from these artifacts.} with eight leaves: one attestation per fork from each of two -full replay runs ($\approx$64 Lean files and $\approx$1{,}800\,s per +full replay runs (58--64 Lean files and $\approx$1{,}800\,s per fork, under hard memory caps and core pinning). In the second run all four forks reported 16/16 certificates proven with boundary-exact cones, pinned to exact commits. The first run is deliberately still in the log: its audit step @@ -328,9 +329,11 @@ lemma file) are byte-identical across all four; extraction-facing proof scripts diverge sharply where the forks' code or the extractor's naming differs (e.g., 215 changed lines for the byte-parser proofs on the two forks whose extraction produces a closure-based loader; 121 lines for -the signature-glue proofs on the same-crate fork; zero lines between -structurally identical forks). Per-target verification, in other words, -is doing measurable work exactly where the targets actually differ. +the signature-glue proofs on the same-crate fork; 27 lines---all +annotation---between the two structurally closest forks, documenting the +one fork's \code{black\_box} optimization barrier). Per-target +verification, in other words, is doing measurable work exactly where the +targets actually differ. \section{Related work} \label{sec:related} diff --git a/provider/src/pacta_provider/web.py b/provider/src/pacta_provider/web.py index fd9c388..0c134ec 100644 --- a/provider/src/pacta_provider/web.py +++ b/provider/src/pacta_provider/web.py @@ -54,6 +54,20 @@ def make_handler(log: TransparencyLog, base_path: str, docs_html: str, paper_pdf self.send_header("Content-Length", str(len(paper_pdf))) self.end_headers() self.wfile.write(paper_pdf) + elif route == "/log-public-key": + # TOFU mitigation depends on the key being published in two + # independent locations; this is the site's copy (the mirror + # carries the other). Serving only a fingerprint would not do. + key_path = Path(log.log_dir) / "provider.ed25519.pub" + if not key_path.is_file(): + self._send(404, {"error": "log public key not present in this log directory"}) + return + body = key_path.read_bytes() + self.send_response(200) + self.send_header("Content-Type", "text/plain; charset=utf-8") + self.send_header("Content-Length", str(len(body))) + self.end_headers() + self.wfile.write(body) elif route == "/healthz": self._send(200, {"ok": True, "tree_size": len(log.entries())}) elif route == f"/{API_VERSION}/metadata": @@ -124,6 +138,7 @@ def make_handler(log: TransparencyLog, base_path: str, docs_html: str, paper_pdf "endpoints": [ f"{base}/docs", f"{base}/paper", + f"{base}/log-public-key", f"{base}/healthz", f"{base}/{API_VERSION}/metadata", f"{base}/{API_VERSION}/sth", diff --git a/provider/src/pacta_provider/webdocs.py b/provider/src/pacta_provider/webdocs.py index c4867ed..fc0e8a7 100644 --- a/provider/src/pacta_provider/webdocs.py +++ b/provider/src/pacta_provider/webdocs.py @@ -164,9 +164,9 @@ library, plus optionally the whole mirror. Nothing else.

#ArtifactWhat it isWhere 1provider.ed25519.pub The trust anchor. The provider's public key — the only thing you -take on trust, once. Compare the copy here with the copy in the GitHub mirror; they +take on trust, once. Fetch it from BOTH independent locations and compare; the copies must be identical. -mirror +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. diff --git a/tests/test_web_and_witness.py b/tests/test_web_and_witness.py index 96d74ab..f3281bf 100644 --- a/tests/test_web_and_witness.py +++ b/tests/test_web_and_witness.py @@ -59,6 +59,12 @@ def test_web_endpoints_and_online_proof_roundtrip(tmp_path): with urllib.request.urlopen(base + "/paper", timeout=10) as r: assert r.headers["Content-Type"] == "application/pdf" assert r.read(5) == b"%PDF-" + # the site's copy of the trust anchor (TOFU: two independent locations) + import shutil + + shutil.copy2(tmp_path / "k.pub", tmp_path / "log" / "provider.ed25519.pub") + with urllib.request.urlopen(base + "/log-public-key", timeout=10) as r: + assert r.read() == (tmp_path / "k.pub").read_bytes() finally: server.shutdown()