From 123d51f0545ee010e01c56cc6fe52d9a20416ccc Mon Sep 17 00:00:00 2001 From: Jan Ferdinand Sauer Date: Fri, 3 Feb 2023 16:55:26 +0100 Subject: [PATCH] update specification, AET relation diagram, and cheatsheet --- specification/cheatsheet.pdf | Bin 121363 -> 121342 bytes specification/cheatsheet.tex | 34 +-- specification/src/img/aet-relations.ipe | 200 ++++++++---------- specification/src/img/aet-relations.pdf | Bin 27351 -> 27401 bytes specification/src/img/aet-relations.png | Bin 23658 -> 30604 bytes specification/src/jump-stack-table.md | 88 ++++---- specification/src/operational-stack-table.md | 98 ++++----- specification/src/processor-table.md | 102 ++++----- .../src/random-access-memory-table.md | 38 ++-- specification/src/registers.md | 39 ++-- 10 files changed, 281 insertions(+), 318 deletions(-) diff --git a/specification/cheatsheet.pdf b/specification/cheatsheet.pdf index 06ba4a89ccddc0e3bbe8608dce72281dbf294c9d..f242007b3e66cf6452f0180f93fcf99bc902f9f1 100644 GIT binary patch delta 8875 zcmai(MN}LNkgWrO#8UpKJm{2d**DaU*KQ2weV^UfGq1hO{q2;vvC9tfxjblESc# zhABJAbd%U#oTL8XPtX`jPQV%3|AlFCgZZ+q7w~e9G#c%hC%6{y8jJc1IdDGSLk&nN zFvyLe;AOQu^WiNuwL5sd_G#g5h~BSr%%lo=Ru23~@jSjBe#pm zY1P_{wE83h2YB_ZO9rtjXWmPfz zIkO=o-A`?gPT@knK7RMk0ga*`_y1n4z@l+n8W5FXfqgC)+rlb$Po3qN>+|jDD2`aR z<1V_-$4pEXk5PUF$k`POxMO=KZSajHegaRPE;-VqyR-A%|M8|nOQf$*j154RZwvj~ z*f#8NcqP_mAZ}o1W@hFu%fqXM^EB2R(7q31Z?m${z7I{7qf~+?j@&%_bw>^J><0nb z&VeNu{OIfn_VH^Jf`%cYV^@JUS=9KtlfbW`J{OG2|W*X z^uA07^Kwd0+oEbLFe1^N)BB`8A0$G zjU$Q>RTPaqYLW(H7Tc~lw%|bu&vl|!;{9@e@I~~E)R_wkxPF30l6cDG2><2 zGQg2)F7X26<&jiVSovEfaLZfq!S~!vvxHXwEQfJ6XS5Q6Cl-r^e-{bj^hhiR&LSE zRJzr^Ytm+buxO98aL3i3^%Yg}8_AJNIwdbXI z$Jvj2?vPDR^wPs)vz&1yx2sac8mmz^1O2lFpN?|rcfo}B+ufPO_E;bw79G#;%~QpX zv*XLK&@+!C^1FtXPgSZ2(GqHg=b93c4?D756;>zO0KY@+)~xlI1C=Mr8h=?ec~_W& zu&5f!_e(cOJjb8|?37|VNH245z@U`Ed%;XJs9|1zmeSh;?#Q6TE zd8%Jl*je^dMA5{EBNSc(wF5dxHJ?dpTivtpdO12NV52(}k@c1xXezZlvK%-fV%x;V zZg~)L2a~7fg2}xc>o#2d)~KkO%6=q*9m3sY@*Fae1p$iosDyx(99IM7v2MjWlQOd4 zfX=N4)0GM45SRxIfalnWVk&`}56}XHsyt$}Ovf8XV}8j)F5cmYiJ7@l`U6GLK8r>i z3? z{rp3E+1AGBu#4$o%c)tc_}mj1y*Ym?9A3@-gSx>sGlo4)INXrDVWY6V+3N1l=6bD`&?I0?iq4rVh_w?jq9 z-hU5cG;)$5^@$l=)CN;hg&J(`_GQ?tsOR2qk6UsOSJ!iB(|r%RwXVbaQ)eU66{}g= zxIUpLlVUT@8TCyzntwMKJ+_ zBgR`DIk%#_$xceOI*(^Ke$4@{CV9B&>18z z-?GJK=Le>?al<;c_(kvHuj^!L4_W)71N5@_xl_%YVW3{yNGm;(l@9*J@2KBQvUTM-jC?(U= zIC(AcC6wS50%{~2EiOj&JxCo;TJm*3F^K5|>{!OFc+->Yh ztzK%~w)eTVk|hN-b;Q=bxk)7qDmjV7mAfX6W^^Y@QK^7G6)(F6&^PxF;Yn&iPaF%Y z9bP|Uv3MdpsG)taq`x1lyk}Qn(AXi?@N}8o7yQG_Y*u$PUezbqincr@m$>LmZTX?> z)ThdhQ=I9<$RFfY$2L;i(UD=hIdo0HS7Ac)H$!V=Y# z&T4%+hB!87XBnSxx5~py=^NwkSQVrVe#sg)t1w%{&DE-EBB!Q?V1}P(D3RCzpxO1r z8#s0roB93(rfcaBySIz4QvJCQ0a{mI(V@wG_3x#5F~5HKmRA6!*&kiX(Yk6fcG|k; zBgs10-0XZ!0-S=%VaF*r{-WWCmj7<$6ragVk*cH(6Rd#QSpYM%dD6#@8W+PQE2@jG zjQ(I*DmF3;FlR4REN^RPj;Dq1YS@t80mH5Yd*b;qp1%?E<@Skc2g_ic zK!1!Oq`0ieQi(x=d+c$A?|boU@@2idi2V3jBjRw)K7#;yd~ipF_KuiBMZedmR?4zq zbT|-hZD{(1l?Et|i#5VB-`2DS+B3w*#nN3RBu2T!jOusS_n_UHBN&!za56DrkkV6N zG{lUTeFwe%h-E~x)BnkR+5s-KgZ2K5kZv^qg^7}K?}ll2{k>(mT>LA?U;4X@QJ`EP z%>;wTvW6Y%!kI8)%Q{p5%VeKA&wI;lYusvu5*gl9%Rhw|{i%jZh6}=0>0rmm=BI>YE4o(<@N}MJ}6^4BFPkigutEDoV!sNJlNFfWZ=@p$!#ZQJ*kxc@68$JTV8~ zs_0msP8oEF z;kC|!Dn=#gL>q4ZlKqRUuh>rF+!5_?W>x81_^?)n?ymRviKQM+PH~}6e3US)tjgBOZ^VaQbd)U(+GRL|(QtgZGDoN#_28JHIBtk{jv}IGfP-TJ_XbzJK~XajTo%9K z^RU!kRh|E(6vmcdH6b{y&;W0Anew_FFf5tv6Fuc_=4DAo!?$LBKwGdsX->Rg6Em$Id+kp|1-oZapUCWd0r!?wj1X^#KyPhonSYqlYNliH# zG|d-se|@>3)1^KHmx$_{@?0FmD~w(@tMZR%!K&gHS<;IvtisjOs4*1TS9dZ+H6Ykp zKpZk3*(XLiI``<#)Bcq^6cf4aIDB2$MuYt(YdyTv92PU@;9@?!qO-|BD z@Ft4Ig`0rs;!vTu-ut#{{tXt*HUl}k@t$v-h8b3CPz7DMB*L)>H>si_z}Z3 zd!EE0Ruc=UfON>{RKNDkV>Pp=wfy$mA)F7`oReCz*)HRbkhAPdRf0IJB|rvGnjtZ} z8aCAmb&ORiVazr**qI^Auv#$F9yZR3{ccSLZ-LR@wrG&z58~iVSRzGZM*e8PBvObiv|iea{IU0eOR|MD$!Pic zoUu9QBVj^q((et-DmYSKAFs~sza*bYP4nKd*yGa!rtf&#F&5m5g%#CA*tiz3fz%BQ z&)74bE;j8JfoWNV_!mC9VhCqpYYlutv_t4Lya+nFhB+SB6ce~sa~-#1ZnnWyJUTkl z5e~?D?JI}92mKRuJ621BJW@4rYw(M;(w8tEX0s1=5_rk7og|IGS-G@mlSSV##|B&N z8BqQPYL4fvlNt2eClr)(pj>hiT?rODJ3k8_8TbDb4qgrx4l;ILjz(E}E@)^TuB0Ri zaE;bvyg4`W=CYQ#aE!6w-%I%5Kb;ZEbO`8YIA^OYJAFqd2 zcaX|o`~pLJgj_f2MNZ6oR0mF`qP>+s@b!H`vc8URw9CW=L)Bd5evTlk}ztWNY$Sl{B+p<)8c_L4{gh>`yzu3$WE$uY+eYh&qXAta)eJfV5-rJ zg0}O{*WEHNchL`zBJ2Qa7M^8m+qoK?dNh0QKZvwO48s zoek~dWl;xA--YQ?3jS5=nGwNJt0z)&A-3o1*Q8$%dZ%gM`!$oG)x~$-&C7~8942nX z7F9~S*-l2XtA>#zs}Urt;sC=Zz#lPJGUSix@OR{;hY#!h7Ug=PYD0bo-oTxTzjk*v z8`33&H34Wjf|?~B&-p%8n#F81Gjcda;%TIR`&SoM78IUFl#Om5x_>L$A1*vYgoKb_ zU&!be(ehZsafk|gN^iS$vx2x4oN#o~>55qN4I=%Cm6s1z)-p}1Dun}3dYpzQhz2yA!mFDnp!eoLJQq(n z;waT4RAm5guH6nInG zQ8G8t1H)xtG~J*Dmxq@P@H>~U92)8%{K$fp{WpGJ{9k`MD<()i)BGOe&E*9eGO*Sd zE*c88+7e(NC<1?wf%#WsSW(xbSbe0Y9@qSG2#!(l%79hzkU+kqt)zKY+N#ufwpbps zbQ4B2mk4J6Lx8S{6D<$9G#P2hcRtUrME9sWZ8_Wz(Wg{6>COH7{gZOiO+e%rs>uT} z5g{(w(S9I^)N-%|#nW7Pw_Ya1e#E*}Jw;`7AE>?^nMm#mW^kBn6Aspv9tv{v+)vMx zyC2ul&8xfBE1jxXh5WQhe+|RN8yQqVPgK&D#3=NIA*Y2WhC}}0L)!2)>}0{uYb;l& zMqO?lu4aOJMJ^Aoscai>- z5pXO+GeA8P+>`TCD!+)Cgy3nD2?s6io{-l~lMP@bblTxiV4^XBE0ASAFhc3S9J@;4Q7$TA$AT?4@oK76{x^;~Vm>Xg!g-K!?bY(9WR z2p?)U^~RS94`(>%r9omU!C8=Ao46fHel}U|zQMp|C&0YhSmoDlEpzZq7ocJq(}_xG zkWT>=EX}BmI&6)BCg;nBaGak5m*tEC65=}2`~k3<)pd?j+{ILL8!JFS`F04Ng&>Wp za_Rp>xPTKbRxuVt!Vkx<7N1(t(X}ql&vQ@Z?aS0>cZQG8S5byFO)<|7Dri&7#CY15 z^WzdQXNp?XKKxRgx+7bPj{gGjne%>b5L2#A_H5lIXEnkcJ8o5Rf4Ss=6<^2^b4twF zps9h(ZvL}tO(E&sin!RJIeh?+^V=0Bk-=JDL1&>gJg}wW+QNr+bi4F&pP{~(q>qc^ zNweVa*}!p}zYk%O#b$?MAdCv-9g6k^xFrk8;#7|0lG)9JbD72*(MAHA$fvkZMvT=~ z6K?P>!>YuIRF-0zH$WoEK_zvrqPh)v;H>~pgRx|&{>&MKsHvo8(N z0V&-><6blIW)x$~x-7v=828GkA`Ro=I3FSn0m=jK3y-yminn&A&uZgE+h*sk%bgkE z`{mfbBUSCL%dhJmvD)Ap?a?SwS}B-=e{`qCD9)CoFtHI5vgp1W`J<=KY}2}@=rgsT zaj~^4n)T35YqCp^?>i>Rdy2=b#t^EnP~KZ1HT&q)O5un^PF!HQMv-(TA?WL6+9GoZ zz#(2X^a=`MZDJ9nR==9tyU#X3&!(A=3-EGTcpA9+ zo?slp&M34z#Q=svK?Piba>8uK<8Uy~_=5Z z$)IVOQlk?b;r!8mVKhyW-`5J3o8&)>!E=ObWnX>eIR%O-1v;kZA@Lt1vp2smE)8)3 zb)KdXZeTWAJzoU7EEZ)4W(}Mu@mO|6J*5&mUsKp6TPJpI66o*M%~RYKESzaO*ne!v z8mLhdD#Vc(6_b_Chr8xyrR_Gky#ElZ38tK<*j93&P8Xy((~(;P-Ri;CNk#AtT%(wE zT&DB~)PoQG6b0%q5)}Wm#7vp$1DD*E1WGwhXuvrz-Nj<+1#g9YLkKRxgqu}WSVtVw z0q&~KCeAeMnU29Xr%*1?_}{up5N>i?j01MKh6f+;Nw4z*1`u|NCw$m@ymM7_5&gpJ z5O)nb`N>=GG;gF)0+ph2!cCC#^3Yg674%%%-U-<x+m@DLWImx!gk)>u zyd2Go2gL(s4$rNXria|U+iuf^G@3FQ)5+i`yH&??MX)*X+Zo;4J?zN?qQIjf zV~o{^^*l!HAd%ueM*PtctlVtw0(JJ3EPPEu%exa6N@?c`PLmsPL0cj~$DaW1eNYfR zzOHckWdBe-QTN^#081!pnml!X*iyzfJ0c}n(vx_k#P1|>g-%@-if^oa`kzY#OyJ89W6PLPt*H)9FPt}zN2^+UBS5b6>UPOhBbx{ft)3b8vNziWPmX_ ztJp(O?w}~L$2Ei%G9`lkk6^!~njc{sEs z=C24zfJoq{>G6(nUSoUK5DNWR1UzFQ;`#0#abfbLXB45n;$u`{oiwDYP5NR$Ejj=09h*s4AaEHf`%&0kH+t^%N`IN)#Ij(&a=DZ1^aZvL3jD_ONB)--dm5}u z5}t`DpF(d)w#j4d+i*}|iPt~EccV-cIi9qt75{Vl$AwjlHGimpu$*h@C@c1M1N+;I z_mGNN0kQLnX>NmihK`=o>8)Xd;8)l8)l~MIezX0&l^RvF7*CmJigwtz-;~}0VC|bmX%X0 znzB)LX&$fR&pD5VC<`K5?5<~^lQCQ$5-CM9@R0v7=4_{I5!`+TZ$Lr7c=i>`Hcpzp zd+Mhqf&a$W1aN`TNT}*s&qa9Qbx?cZZJng9>}%+@vItg_Q4@)cc2ZZ%(+mxwWgVSB za*F6+bfnGSVbe?1#|AaV;Zd|vKc|nCJO+>Uv63B?@XwvSf!^&gYLXP?hm-QRX1q^c zYuLD!$M`LhORxfWhn|93-*F8Yv}mTDUR1=`M1~x^W8s`BZbtao#(Z^(d1#5yDP~TGP83n zK-4afeaom08&^@NDrt4PdYaDZ!Dj2hw&<0ONTd}`DZhaMYt$}4@(zCm(R$z@dZQg6 z@R8dxg>|YIAZrxJZ?|*D*34O;W*o<-(}S}hg|eNV*BLHOHO(ad=^^3hA>p>%%|P`% z&(^ZvVD}f$LpuRJ&JFh$1Cv%Hb#&eJp_41krClA2U)U$ZxiT!quel8zwDB90kTQ|; zq3ozQQ5n2FR?HDLfs=>Y7*P_{8wnM-R`tMvy5v3%o)a$9J?I+_UmEY&Qg}}myC=mOAV7DmVh3h>O1eWey>A>M`h+G zi_fMmi+YNY3sV1SjIn3mP$6#@bw66EXD3m0zEKI5wo|Y2TeSVLq*Rj&SyWT(P3=nj z*;T?JbDCP>DonJ$zDFfC)H5i}K(_T?tV%Ixp7<{riUTxHB^xn@M^$fb$329GFr!CI zjgJ{bg?ldtaFerD!WU4F5KVEH!8cIh=$u$d=BQ1h1LFJ1QCCnbQo(2F&z(Y6xD+Ug zbGg8YbT(9q#TiYBn)85Foz_jyvD2&)RGEH@3LyN3b~Kc1YYAW7gFQWz{l~T&ZryR? z9~2^U=KC+BCi2~V;|(PuJ4{vJq2VT1{wjS3y5-i1%?ej=@qy35jUK%{qq58TZ)jFD n-QI^oG_Ln=oByA|OdS5Fb27C}dtHS>`wyuQsi`HEr4augZX^Kj delta 8884 zcmai1MNpj$ki_Mo!QCGO=iwGyfQBZ0&I`J=0ZP zJymn)srhI`Olm@`vn7Dx<4iJ!`wUd;YrB%Pe)3zCYZ+HbHj`UHwSg^Ad%#%xRQR`Lpx({?9&f^dOIBVsO3E;an3xwIDAyJ7HdCcQvX;>YP?7*N-EPJ@q2Ug z`f#Ib%9oxMzIcxlBkOK!@9OQ?7JffJ9Hj$kqk1as;@3WV#8q}*3@K_j>fBQ&=NOm zj71G2;9OSujsprk0f0MJ*90{ks%pFFV$cfCA#y^~Mo1UCnSB?mY4qF->3AJFrL50%p+0;@zqIZu732bPt`l*HVG zAL*zGGkJ?#ZqQ9}wp^mK!y_4Ls0o%P&WC?vtzA9muNr70W(CxmYJvivY*fj89W>@C z4I#@Q2VCP#qbu^ATJP;K;mkSdkAV4|szPz^WEYzcyO>!MH)NdLvRziq{${Gw$(5ht zWKEo+0MK9qya#;eBJ2%zVl1&||48Tn^N)e={<1@j2Ov2tm>b#P3OV)AGJn4MQi2WZ z+vxB?t!XEYcyzE-a!kH5Cmp*MT+{ztB^y49L9W5h_5~W zIeqPnE6ertr$08MxYHRS9Yh@YfE}6D=R3=ROfT>zb z)0G{AfDW^>0}apTDfB}Np%z4)ML1$Dw9x5dAUR>S>DZwd%sfF%D49ePK-i?!m%cNJ zsBN330$p1HF;|tY@}~d|e_=;8$f`HJWB$S(ZIIDsdS$mC%BOlx26i4z7vE>G9syV8 z$YsfCU^hI47O;0Wdy)}*+r~lSL}0G8nyVW;sqz$ia~Jk4v`vC`$9K20vdrm)7#+R= z_E&u+&8W;}(gZek6kkTP0z_ySW+36i^)PXssO<>+38*P@GEor0x=6D~^=FFsDCzY5 zF#R~QwjsfIr~H3OW+=+y;-RsKPqBM;O@;4+$l&Eyor8ECH2E)Cdl{JcmeaASt3lC z2*}Ze_VESvb4_*s0quAnUuF|_`e3N21`&!*Kc}ausi^Ix=itTU=sS5yOb8rFAZjpL z=d-*i>c5LWA1`P3?~R$~km5SC zs>~P5DYH1r)%ZCw<8p``@ZZWQ?`dr8ewwt7HTz0Ya*y6ngLIdAd?hGHY6J`7S**5@ z;k%H2BjRAWO-4+z!bI8}V# z)M2~#?Y0P6c8ccuLq8tA2mA9iZ5O_TA+)+$-EaLke)d{~} z`M>LkWkrN+vk&;C4U%&B1a=Z>TC_G^`zo>51;8~acz4CR;8mZWL`4#dJ2H_#{hiA)op0yoey$;57ra2rWNvj5eC3Y%( z{?)J*ukS@bl!7_v25p{BHKBDJOZJB5MswwmSSq7{rwaqX$K_$5 z>yD#CrX#4&u9H+5_jKp!;wjRd)ltOz=~6UN9}}Diw=MM6e(_I{wd^AO`jELZ9i3_C z=ihTRipX`~861>e5|YuI3+i9y>%EG-nxlHl+ClvVQKa|8>Pb%bQ~|V=1}ZrjJm}r2 z_M1e%6M)WUoIb7P7+3Lrh|pYpQWN{Ej7jm@Zsu8k;5YP@%}=ATfwxbhsZeQL-P|3!P-cO}bT6|+{QG9BqM{w{;N_QBgE|eschKBdw9am5e3<@Y= z(7ugaw%;DJZc2n9@27qw@{s)Rc7c)LwFev~nCWaX3xpfyx(ghf^wJGBm7`8PP(X#) z>QVf4iAhYyav|$a+Y3sJ%n=j2<)$AuI7|THIHl&|dbtZ~kM{3mD`p6ncRRR z$C0kD-9|u5Py_ZGzd5yU_r(mdRY~S2n*f2ba`%g9W%~jFpM;cy7#;3Ds-N3VYR1YC zgxaZDB>nksaf*Gm>ZC#VWk)!jGey@!!yVF-;*V7ds|%uD{c_)55x}NPI^fZ|svpjD zblR0KkCVuGko_EIC$kq5{ywZ*SU*&F+wf%UCAIlU=kNfC@Zo9LLwH;Lep z7uw`=9#s6=aUzpw-A?eSN4U9XxHf%r0_JSC**9%^-YlY?v)+6qkBQb&vu(hxKfG#Q zW)x2U0p0*?H2?mQsV+{^O<+Mi|DA2#uIujACLQIn$%Ax**ufD-pclG0Ra25InagYJ zQZr6GfN3`_TbVE{$BZVNT{-Q%u=$kF+gb`I|pvj1!^9hmvyDL8ggLG;#bru+Eb%*8+79Pz>uG6a!j$IQ^CM+0A`-RF648t zD4f&u1$0wi-7@WYIS5s!ED9+RIcq9s66@&eQ2COWpvN?pXgTu(+8%*%iwgDt^fW58 zVaf|aXw3p541!_?Q4xDdPXdx^87@ui+)qCdA>Bu`e~{<7mD*(_`KXQMk+J`E?ML#w z$i#b+Vvs7q1E@sd6zm6_I^<#ARtlBvP_CmfkY&Y0aVUSlWo#0V43vJOZQP=JYnDLt zHtUxd=V)S zDun68-g&@7<$Om8B6=m+`4b8|OU(WEZ_`%63@$9ENMU0Mg)UA;J$o;tI3*gKCo<0* zc6ugj_b;mz=zo4vcq1=b3kwR~yUv8)SXyo|y!CjiTTJcq^8luJy+u>H|yXwyg z@I@Qgx0~%ZEGP8qA_{-D>^pOnF5b&>sBzj)ZCb?!fV-D0E# z92U;3Mj;i&!=mZ0Int|E)03ObW(buq?_o%$bgWL2o7!i{7t5F7g?7AaCau;>;+lV1{&DZBa{$5#;&MtzWi z`xi4FYc9?v%+DUMVX_|(jUWGnJ&9mZl9WG}VDs>?@KSJc{0Hp3Y%J^)5MJI!WO_~* z7zlSl0u?Z{8hK~uDf z%xZIEKR1SwmADn^cV?*$zVT+eB$bMepVjW}QU&VFS|)xc93XJfwW>E{mC$ldYJVGy(m?N7Mwv+atxYbPF5iidi=69pJhJsZH(^ZD>+|=^o@#Gf88N?-jZl9P03Tt;x!!8~VST`~MR1^Zc7z zHbM!LTz@|nfacy&y0nx6O+B@+It&~-XP(Oj`RvMW)z7i4x3}{ZqH2|QT97%gPx3!D zy=vm;9zZ_I4xBBzj5YU&=nW1yBDyp2R`rBpJ?^{NUknKC3y(VoUJQsm$5?4saGz69 zJM2uK#@gj^**A?e*3WKyo2x;$Kjjqe@4w(jZ1;0$!fW`M3TvqfesvpTVFZkrRXlds zuhdGRp5LhKU;R%O^bKeiH{1%AGvuKvYuaa{Sk`{8xaF;cINWxzxRd&(gkfAxZNOd} z;J03qg)EP(2Am8oMSkWM)JJ4N*>(vcsO^iKl5*+uq^-tq`au!kGCV1p-F1=4JKh@V z;V#BZPe*1GehBMLv7PPYF9w`CM~WLr;#Yj-?^jv*JkT9nbox`0KC+dmUy-((fIs|~ zI;DICUSS+N7mt$g$?}(B%E4@G*&O!xxcXwrk*ne^yt&$|97r_Y=BPF2RiWdV!`%Y4 z0g={r@*OK_6vlo{Y_@0L2?C_>n|+NZ3cg!-rH$U8t2O318-wkTA5 zT}UCMsCdmV3vX5NGSo#4 zeJXaS4u;MWD`lO3t(2_Fs&0!LwCe|(ES`Z)4zl2hFxfKfAEv(@@yOXhz>k1$fA>;> z%jI$Ms4GKjt1&V4jkMqTDBNGGu`L2p>Oq2U)j8GcxXT18^{DcTTC2#v%31wlw^8G- z%~$Nu1mqUj5PtaW95q!I)rm|0cZZR_t*g?#BO?UJ^Ck6jVmF$wF(Wqq<3ogQjO2BP zPKx7sO+pahOL7)`OX3scO%fJ(39|pvYX1c~BL*45&IjS;;AZDc!D-<;a8>wU{Bx9k*!yc;Thv zRn?Z0J(F!e{7;}00wDHj%ElVWLxK$+nNCbVAz#*oGQ3WL=sdzq0vRzR@bjp;I74Ac zprv?IBZwhF1@$7EV47w=lwgt*5>0^k8^AmH!ZRdmk`W|;BlA0Ac}T~ai0DF5U?9R& znKt}jPImw;UI)p_YD#ehvsY8mD6GAoo>MtA?O0F=H%sD7EbU>lq zi9~V`oYCh$Ck}#dX^dA%@8=(i&M66z0=>vsdcjtW;!!KnVp(8Tc`)wZwN%{MH`cnuqtcFwbvzk%~P#rAAgA%a;$0 z2OGsHSRFb3r%ek*ty%HsJ2W|D0H3J>Csr}kbdKq*{|edAjToA-ax2G4b7+n~D=LRS z(!tm>%;>p@MR%SSRB!?Z8`WO=(c+tQTWxI;-MHBDFKn}z*V#n)wds%YFz(=Xge?Mj z24ePYk>6Pcl{<>{`>=y`01cM;yQUX8h|hS81I+nZl4?2k!~TEX#-xin}5pq$1oc*c-{Hf>0j9J z+}3_%UJrV5sb1Isospj^S;;C1u5X9Je`J%a&I8`K#D-@!6FCJT3y2+iG;mD-oeu05eLA4lGt7(xSvcy`5jP z5tfQ(Q7_~RK!J6%2n*HhTBw6+z-X|2VAP3qYPTs%^d-AS- z=kJvmucI=KeQWC~-drcN+INfJ`K`=zbS3Ov_s`rK`khYs$NT=Ey-<#m^R}YBv@enw zU|c10aH6@5q?@@`=G-ay*lS-wj5;Him6z9VNv>arpWOZmz(ecP96h3h!2 zEAHE87&j^Q?tEgmJhFMy%sD)Tzqs9{q%U;uQQLE5=Zm_T^U$OVd+w>FZciS0u?A92 z0;B|e>-B^)Kwq}q9=OWBL$JA7O`8H8GQw%kms0aL0#~cDdw9tcNxpuCeKom#N-t1T zxiVlZl~=G7owFEMNS zGu#1&V4rh~;9n+M!{l5~gp}WjLLt8Xd~Hu0_QQJ*4t-W9q6sN;8E0cGN>VD8qnWq7`PL*%GX?iA>}yJ0Z? zU!g;UWpIy-bq;x$nP&K{oD7L1S5&iQI+9&TrNdjhqFwP2dmm~0^GzPm4r1v`pow3; z-jojcq?&OqV%6up}BW03!r#Ln3 zz~XiBNlt1NjD4M~pJ!3#3h^>cGsEnZnK7zVn1gf}-EwznyahvJ~FL}xqsy>V@9SzOij4C7{F?zjtf7q~QjY&_wnq7mbKxh+jq z7P$1pg5{ug5_yuzc}8@jUG`(Ab~P+{s~qH}k-g-*fQvRLzTX8jFC)4uLwQ~@$)9r>d0nxDEZs1!rDfb&Eh_Td?d!Be1_1^ zU>z5$79H_5ywm+wa-p#Dgd`hLing_70NE^N)wWq{l9t zv%--v?}Klu$r)$6F?p2}2wTOvZdn%#UtVJUf4sj*dy8NU)_er#4$OSOJUrO{+6ue4 zyGb-!;UiM+gTB5x8np=IJIG z(Zd^(Gzos+rFchhLCER6!H0c`*`B|=1FTnA*YsFSZ(|nEXUoE@Zu#y$eV-zy%pE@b z-ZNhIfKn=U3Rg|Xzv{L;dHixQc(fQan}0e!t``{4fTbbx3y0Vd)Zt>VfJ;u-0iq;R zs?EtZy0pc4mFR^UPb4-P04V-8TeDla^H(db5N)ZIr}>kD^>zO2;QG_cH!@&!{xxC) zADAF~mxg`0Cqwuk<KneKn0%DXS`n0|0a#X0yG2-4m18KE za}kx^QOW68UpeCoex&%5-iKMg77|Ae!2XGx7{s%tKYs*-KeXojx4nyvC2!XEg|j}V z_ZJ?^YkZ(Gl9hJj-!@BcP0BLkk_(fapMBKxsGOMO%Jmn3{`C)s0KEw)f(&_Q^TyA% zkPpW>EF$|0k{*FgAk)f?C$IR&tga}WKWA$TCR##@Y6|A2R?#yHyX$g$i8kZ-OLv2! z+;AMvhU35gKAdKtt6f-$wEE!Fk9gUAVF`t16{+bQ*V{Xls{GglN%!v)-c!gFQ8NY= ztQEhp@n>!5SZdt%sc8Qz-}?sm49S#!lQzOgtL;INAML3C?t&&>f+>$fATssA!6+xV zyn#J;UKcOk-rwj`7~)&XfH5suA)7(m(Z;JP?&ZQ9CnP;=v$+ zlHW=M;U{7so~_T2Cfdkt?%WR%5G>q}$VYeh`4()<7+_unEQjl(2#Y=m&)SA+q(Oc{ zW2YsoLK`THazez!CB&upc-Yy*IC;3a_;@+R#Mybc#iYbIIN8L7CRJIBhhgQY5URlA29Q*6dV2&#qvps6gkN|94=VqN2}xf zivunuiLQ&NUR3HP)i-rD7@Ds(QJ5Z43UW=M+9(=w&D?+$b9=+dJkhdFheflzZL5aT zK!xUFEttHR$?_-3{#LzOL6oVl4u*61FTS^8to^J;cVu=csWD7K+5;MyeY0dUikWtM zlmv#aX8ksi#WGM>hO0{K4HY!0Df1}iRrxfgvNn=3h75!TS*VPv+MROoYDq-jP%^d` z{>smlep&!Th-9!M5-k?QbYzIF=}6 x#e!vamvC1vh4%;YA5e^3;^`oB2QybU7jt8Kka^nP8Z-_v2R8@|mQ<1g{SSt^?CAgi diff --git a/specification/cheatsheet.tex b/specification/cheatsheet.tex index 2762ce398..f5f5a0578 100644 --- a/specification/cheatsheet.tex +++ b/specification/cheatsheet.tex @@ -87,14 +87,14 @@ \rowcolors{2}{row2}{row1} \begin{tabular}{lllllllllllllllllllllll} \toprule - Table & \multicolumn{5}{l}{Base Columns} & & & & & & & & & & & & & & & & & \\ \midrule - Program & \multicolumn{3}{l}{Address} & & \multicolumn{2}{l}{Instruction} & \multicolumn{4}{l}{LookupMultiplicity} & \multicolumn{3}{l}{IsPadding} & & & & & & & & & \\ - Processor & \texttt{CLK} & IsPadding & \texttt{IP} & \texttt{PI} & \texttt{CI} & \texttt{NIA} & \texttt{IB0} & \dots & \texttt{IB7} & \texttt{JSP} & \texttt{JSO} & \texttt{JSD} & \texttt{ST0} & \dots & \texttt{ST15} & \texttt{OSP} & \texttt{OSV} & \texttt{HV0} & \dots & \texttt{HV3} & \texttt{RAMP} & \texttt{RAMV} \\ - OpStack & \texttt{CLK} & \texttt{clk\_di} & & & & & & \multicolumn{4}{l}{\texttt{IB1} ($\widehat{=}$ shrink stack)} & & & & & \texttt{OSP} & \texttt{OSV} & & & & & \\ - RAM & \texttt{CLK} & \texttt{clk\_di} & & \texttt{PI} & & \texttt{bcpc0} & \multicolumn{2}{l}{\texttt{bcpc1}} & & & & & & & & & & \multicolumn{3}{l}{\texttt{RAMP}DiffInv} & \texttt{RAMP} & \texttt{RAMV} \\ - JumpStack & \texttt{CLK} & \texttt{clk\_di} & & & \texttt{CI} & & & & & \texttt{JSP} & \texttt{JSO} & \texttt{JSD} & & & & & & & & & & \\ - Hash & \multicolumn{4}{l}{RoundNumber} & \texttt{CI} & & & & & & & & \texttt{ST0} & \dots & \texttt{ST15} & \multicolumn{3}{r}{\texttt{CONSTANT0A}} & \dots & \multicolumn{3}{l}{\texttt{CONSTANT15B}} \\ - U32 & \texttt{CF} & \multicolumn{3}{l}{\texttt{Bits\quad Bits-33\_inv}} & \texttt{CI} & \texttt{LHS} & \texttt{RHS} & \texttt{LT} & \texttt{AND} & \texttt{XOR} & \multicolumn{2}{l}{\texttt{Log2Floor}} & \texttt{Pow} & \multicolumn{2}{l}{\texttt{LHS\_inv}} & \multicolumn{2}{l}{RHS\_inv} & & & & & \\ \bottomrule + Table & \multicolumn{5}{l}{Base Columns} & & & & & & & & & & & & & & & & & \\ \midrule + Program & \multicolumn{3}{l}{Address} & & \multicolumn{3}{l}{Instruction} & \multicolumn{4}{l}{LookupMultiplicity} & \multicolumn{3}{l}{IsPadding} & & & & & & & & \\ + Processor & \texttt{CLK} & IsPadding & \texttt{IP} & \texttt{PI} & \texttt{CI} & \texttt{NIA} & \texttt{IB0} & \dots & \texttt{IB7} & \texttt{JSP} & \texttt{JSO} & \texttt{JSD} & \texttt{ST0} & \dots & \texttt{ST15} & \texttt{OSP} & \texttt{OSV} & \texttt{HV0} & \dots & \texttt{HV3} & \texttt{RAMP} & \texttt{RAMV} \\ + OpStack & \texttt{CLK} & & & & & & & \multicolumn{4}{l}{\texttt{IB1} ($\widehat{=}$ shrink stack)} & & & & & \texttt{OSP} & \texttt{OSV} & & & & & \\ + RAM & \texttt{CLK} & & & \texttt{PI} & & & \multicolumn{2}{l}{\texttt{bcpc0}} & \multicolumn{2}{l}{\texttt{bcpc1}} & & & & & & & & \multicolumn{3}{l}{\texttt{RAMP}DiffInv} & \texttt{RAMP} & \texttt{RAMV} \\ + JumpStack & \texttt{CLK} & & & & \texttt{CI} & & & & & \texttt{JSP} & \texttt{JSO} & \texttt{JSD} & & & & & & & & & & \\ + Hash & \multicolumn{4}{l}{RoundNumber} & \texttt{CI} & & & & & & & & \texttt{ST0} & \dots & \texttt{ST15} & \multicolumn{3}{r}{\texttt{CONSTANT0A}} & \dots & \multicolumn{3}{l}{\texttt{CONSTANT15B}} \\ + U32 & \texttt{CF} & \multicolumn{3}{l}{\texttt{Bits\quad Bits-33\_inv}} & \texttt{CI} & \texttt{LHS} & \texttt{RHS} & \texttt{LT} & \texttt{AND} & \texttt{XOR} & \multicolumn{2}{l}{\texttt{Log2Floor}} & \texttt{Pow} & \multicolumn{2}{l}{\texttt{LHS\_inv}} & \multicolumn{2}{l}{RHS\_inv} & & & & & \\ \bottomrule \end{tabular} } %end scalebox \begin{tikzpicture}[remember picture, overlay] @@ -119,12 +119,12 @@ & base & ext & $\sum$ \\ \midrule Program & 4 & 1 & 5 \\ Processor & 44 & 13 & 57 \\ - OpStack & 5 & 2 & 7 \\ - RAM & 8 & 6 & 14 \\ - JumpStack & 6 & 2 & 8 \\ + OpStack & 4 & 2 & 6 \\ + RAM & 7 & 6 & 13 \\ + JumpStack & 5 & 2 & 7 \\ Hash & 50 & 3 & 53 \\ U32 & 14 & 1 & 15 \\ \bottomrule\bottomrule - $\sum$ & 131 & 28 & 159 + $\sum$ & 128 & 28 & 156 \end{tabular} \end{minipage}% \hfill% @@ -148,14 +148,14 @@ \toprule & init & cons & trans & term & $\sum$ \\ \midrule Program & 2 & 1 & 3 & & 6 \\ - Processor & 39 & 12 & 77 & 2 & 130 \\ - OpStack & 5 & & 6 & & 11 \\ - Ram & 8 & & 14 & 1 & 23 \\ - JumpStack & 6 & & 8 & & 14 \\ + Processor & 39 & 13 & 75 & 1 & 128 \\ + OpStack & 5 & & 4 & & 9 \\ + Ram & 8 & & 12 & 1 & 21 \\ + JumpStack & 6 & & 6 & & 12 \\ Hash & 5 & 40 & 26 & & 71 \\ U32 & 2 & 14 & 22 & 2 & 40 \\ Cross-Table & & & & 1 & 1 \\ \bottomrule\bottomrule - $\sum$ & 67 & 67 & 156 & 6 & 296 + $\sum$ & 67 & 68 & 148 & 5 & 288 \end{tabular} \end{minipage} diff --git a/specification/src/img/aet-relations.ipe b/specification/src/img/aet-relations.ipe index 656d4b244..18306f154 100644 --- a/specification/src/img/aet-relations.ipe +++ b/specification/src/img/aet-relations.ipe @@ -1,7 +1,7 @@ - + \usepackage{lmodern} \renewcommand*\familydefault{\sfdefault} \usepackage[T1]{fontenc} @@ -318,119 +318,74 @@ h - + - + -80 188 m -80 44 l -280 44 l -280 188 l +120 172 m +120 60 l +272 60 l +272 172 l h - + +158.864 117.909 m +164.993 121.995 l + + +168 124 m +156 116 l + + +158.864 117.909 m +164.993 121.995 l + + 192 138 m 192 154 l processor program -output -input - -176 120 m -176 108 l -176 104 -172 104 c -100 104 l -96 104 -96 100 c -96 96 l - -jumpStack +output +input +RAM opStack -RAM -hash - -128 154 m -128 134 l -128 130 -132 130 c -168 130 l - - -256 154 m -256 134 l -256 130 -252 130 c -216 130 l - - +jumpStack + +144 152 m +144 132 l +144 128 +148 128 c +168 128 l + + +240 152 m +240 132 l +240 128 +236 128 c +216 128 l + + 192 124 m 192 92 l - -200 124 m -200 104 l -200 100 -204 100 c -228 100 l -232 100 -232 96 c -232 92 l - - -184 124 m -184 104 l -184 100 -180 100 c -148 100 l -144 100 -144 96 c + +180 124 m +180 108 l +180 104 +176 104 c +148 104 l +144 104 +144 100 c 144 92 l 1.20123 0 0 1.20123 176 176 e - + 1.20123 0 0 1.20123 176 176 e - -176 124 m -176 108 l -176 104 -172 104 c -100 104 l -96 104 -96 100 c -96 92 l - - -208 124 m -208 120 l -208 116 -212 116 c -252 116 l -256 116 -256 112 c -256 64 l - - -240 76 m -240 64 l - - -192 76 m -192 64 l - - -144 76 m -144 64 l - - -140 64 m -260 64 l - - + 160 100 m 8 0 0 -8 160 92 152 92 a @@ -438,26 +393,45 @@ h 160 100 m 8 0 0 -8 160 92 152 92 a -u32 - -176 120 m -176 108 l -176 104 -172 104 c -100 104 l -96 104 -96 100 c -96 96 l - +u32 -168 124 m -164 120 l -160 116 -156 116 c -100 116 l -96 116 -96 120 c -96 124 l +216 124 m +228 116 l + +hash + +184 124 m +184 104 l +184 100 +180 100 c +152 100 l +148 100 +148 96 c +148 92 l + + +180 124 m +180 108 l +180 104 +176 104 c +148 104 l +144 104 +144 100 c +144 92 l + + +184 124 m +184 104 l +184 100 +180 100 c +152 100 l +148 100 +148 96 c +148 92 l + + +192 124 m +192 92 l diff --git a/specification/src/img/aet-relations.pdf b/specification/src/img/aet-relations.pdf index 6ddb3f710d107f9010f2f43a3df830b5233207e5..b0dd76df0f8cc314b968f46758f5571b2d74b9a7 100644 GIT binary patch delta 1573 zcmZurdoLbjTeVl#U-OU=nxmb`{xa#NUBB9E}?Ar-giN7hP`>$RCC z?^fhldEBl^8hKMfB$?N_xwre*J$1i7zVp5Q_cTzW@F}-C2c_I+v>RAe7f) zJ}=||p6--uVXf1~qRynzEHWyj)2iY(s<`-kQ4BcIq~2T%;$D8=B&K{5hRsSgA%( z^lPw@HzJxt%ZqjtPH0^a{fU#=UaYp=Eqzq;vf#?tJ}1iVjGV8<9w+pa4V_bWV!<`{ zJ;nTK-RMlWh1iPi8j|bMd715@;PKRflw2V#oYR(M=5T2{;J6KNfI$*ldEb&}Y!Hil zm3c(|xT3HAWTA(pV^geGG-Rk~HgG=R9W75+9Iuf@X6Bt;z8@oE{*K=DiVpL($~2g* zmv_DGvRi7g_x_@I+QA4K?^;f`u-LM31-_?SBO8?n(|b^x|K%y`P6Ey@6y}~uSGrv* z>qXm9iqphTMRzRrA|1s%drJvV`0AEbIizy3&@<5KTGm2W?_EI}3Ii!Ao0Xf->=K|-Uvx(mRP+absOjB#=gr=ksqv{yznJYM z*WN|rrXMzp1xer56}2t=Wkd1da!tl+=(l9$_nvSxN<0`-rmnof*AO=OMz@w+!VVie z!vFXzxRQO~p7d~17-L$~YxBzOeG+MlmW2J@6}psGJ9*!yv`yI5i7jKr&GZU-v#SDt>w?%Sx@d1v%MlWLI+fL0SXGuOZV}kHGb16vR2XZuGUr zyo!=TWAtofyovs`;YwrexyNxTuWaoMzPvB*Ptpbx$F)A+p;LqR4hiIPm?Su||KVJj zNcmY}6KQ3Ok)hJy(c^QDc7%)?H9@~7H_>JTGkiU{r@6;#tF&h(_>m-?q)Han&&95b zTfKRjal?9fSH}y&JpzPnj1sfE*%notZO}0Wvp3Xzh!=v02+bsOuC! zMAy@~#I%7l8Olg>ONLItpWyrK)d;(65;wkyk)wP8ec`1$D_io#Bfq^!o_;fczj_I()6#fMGxez3VXX(}HXw{t z^p#bw#uz+Ox-`)h8};Izh1i+irz~#8y`^XClozxl%t2^-HX^LIs-y*)9o#g$4gsEi zrn!TWN(D1g2rT7&PB#wPctc*?X2v@Uc+z?Mgj7n>lkS$Wm5bWFb?Xq%S1x@dr`*k$ zEYukZ(z?(|MVk3%{Bl4 delta 1541 zcmZvUdpOez7{~31PQy_;E^*RaM#yZx*^O{g=(y%O%2uwGgIwb&ERQIZ+g6@jin)c1 zk!EbdveqbancNR^%VqAQ(z*S0o}BlO@AG~?@8@}w1)za`P|X$BI%{`vP~Anh1rYg) z>o(cW<2o63VT;T-A4TSPY}9Fb28#cHK$HI@s*~FBZ_<9jNV5mJB+X)hP z-xJV85Uw$BeB|P>7u9?>%2LP7_Rr+?cLK9Gyobx6<3TSlG;>Y+gDTHDY0ho2;5timR6o6yKddk`s%Qt031iMJV~G6N1tvJ%n$#>7i-k<&e=g z`|rd6DZ+%MR7pe(Z{>gg-%9!X=UIUZVO4jKNy;=0+jx<3VqF$@wvPLbrt9Z_pAK%R=I2a z8!DZ%ZQK#FVrjq2!$3xOLAZopYfb^gQnF)5r`{Xn5_^5SJ88%z889)L7Ddj{G`Q=vIa)(JQNupXs% z!-kkl997!=X_LQdFwkMN{rn4F@v#u`txOo|&+@`gDC-b~$Ygeo!hok~TGS>R_)I(! zM4fAD`%F}c<{4-SnvF0(U=E!WS2XK#YI9z#wsW1MW_V-++weg~XYY7D7`_6D<@g&Kk8k3XZq2Zx=0; zTj-=PPPE!n=$%>4?6kOs{G2DivaCZ@;SBCE-guGkAfextzL|>YJQ>u4Pcppf)-g7Wsq`eJX+f zxY4R*N+eeUd&SZKEtpTaLP5Far3UZ6R9ZaCt!hZ;1hzuGdl#YJ!dwaEgYZW|TW_6a zF*bn+=r$>)mEBhuwme699j?n@c&TWtS;Y>$-uLkeZ&c~121m)MD!*z-zF*0aE^XWE zK5*c}Q-j#FG3ks|KS7|3u}u$L@>cBl?DNW^n$uR}naCfVhMcu`4@kz_;_9fr=Rrse z4u*voBL5Bm3x@#^1QrVe2w;O#VG-unq9GUl=T1iW-#dT+a0n~{K)}gdfA)Xcy~~y$ zWL@v&B9JKnK;ZujBp3qzcL4wd7QKfV;`TBW8cu$G)mR?&y^RF0IP$)L>n6xO&(R1R c?t2{#U<~&#q#>CRa29NcfrFt?3kOT^U+;~@eEP%n1AqCa@Xr&z z-O&&g;zwK~|0UF?BvEC(K3r@vRhiiM%Ca?(n1Y*|ke;5N$n|2^2SW%3F59dr zEbCX1EiCcB9r52+DT0VP8LQ_4Pl$+mcIR7Bo^sp0#`hO2qobnov0U!?Vq)?!kcj7l zs3-|Ldn5syiP>_`v##!Lb93|G0=_s3N=gJym!qQ!FJHby=uMQ;icmH*Hdfg0lcS-b zB_}7Vo03;(fyo+r?B&4LIv&+k^1g6#R&W|<~t88ddP*9XBt-M7e z=onnDobEipm&vvp7#L72(70_ll1s+T9pmM7*I+19pfjA-{(Q4+_xPCY=}bo$brgf< z9SjVNTeohRZH}`n^~831J|OV&^Gk*)9Bhn*^u9U251aLTnTuPuhmh5DT1-sr{>P6W zxp$keyP}v-adB};u7Zc8<>YXF|NhM{Boq=E=_PfKi;Ih!n|tTzsHLlG=XKH?k%W&U z4dv=?-b)RayGA2=%+8q`Z;QVrr=^Ab{P{H{g{+{UfRNqn>%oE5)LC{mO=4nVx%D~@ zkHf*AmKO3}!^s-Q2$&qo?9x)pSdngp<8iKPv{IQ#f$Oyk7?SxKEV99FbX3$T#!*H_ zhL*PW7abkXl#~=zE^KVdQ0`YRUw%__X+M21o+VG8DjqGUrIoB2{pZiyv*YdF{uEI> z1`Q9B)6I!8eD)7Y zoZ}XUhNfnp9`mb|58~pB$1|?F`%B%oZr?Uv8>ECi6V%X1% zLJE;g285nVCazXg@zb;S>rW{0%N$tk-u#NJwaF zvZArs7uVaz=RIX}5Q$KJSy^j+{coAMT%|HP@c!Ggf81_@am=r-QYKOO>VZMuC*qE* zuw3ph)E4cD=j{z96IB3XRa8{0KIj)^HXaXM>W*GFjtC2D{`;G6tXLoW=;)~W@@S&i zbVhZ1pVw~Zxk{A{852_o?ACreMf~4XaRS80IPUhr3~98xcM~8kY>b!q(y3G~cyEI< zSMRnEXlZHXoBeyQYQOk|8UF#ej^^KlcTFuVH+J9xk5AtCdyh;`#z3Ti^=v6OpWit= zY#tg4gUFUD5#N)oSQN=(h_g9fq6yQva~u*H+5`?MK2d6Xx>3}-v%ilFKY6uhKH8n( zK|g=~L8q_&(;h-$zm|~}$*6sAdU`sB$1yyR_bSq#fX(7x!)=#~T_G?=ok`+?U*!;w zs%*CfDZdvLF(KE!y&bJhcwDzPj*OKx9Ol}Wqf{o9B^cULz#rfmCR%cp5gZ%q@9+O0 zmeaZc-s~^P=a0{#H&a`)g^q)bExodiTt$p$oU{M_xxw2?3`bJ=eqdC(*GT!y&dxGA z(VjxF}4K}4UT{5YyqeG)Bk^#Jlz>gks zM1f{2qs@lG6lEOj%ZkQisd2PwSliErx!Y#e)@0zLGcM=;aI=4FYxln9sC_VhD| zbfHp&JPyTD;!nxIB~m_97=MLms%~KLOSj@EA?(+$&nt#{n5>w4ySsgtF9Uphs19bS zI!1Q>H9nw=XE#sWy4ZvT_4f7c9B657{vJjxFO~K&mU~^NH%|P+hr0m*0W=EvZ%w%c zOu%~^ySx2&cFbx|=6t!=0|_~9yglBU+Rq-K6P1uyzBt`Kt>&Ab`yL~eSbD7Cb#!qB z{<0VP&Jr?QO#Of`gqA^`tK+)s*yYLWj10=DO6!|{srz{EzkmP!gP2%TL&JM{e}-f* zMp%xZ&`_f|~-0#>8D3m4-~JIZ0{)h&UXyIc=Mc7Y zl`Dcxt9oL&2$bW_c^(gwlaZyAe~}ZGl$1oUb8vk5@+HWW%hJ+vYFDI6T$`e`ZclzQ zq%z2^dd(|0151Epq`ugge=5ujd`sN#=*hCpG3m+l~djYxGv^>#^iS|k^?FFcZofxrxzzQg?dOY1RZ*w|h@Ey&KAk)-ZkX$)g%AMS zR0ylCalEisMVgUrOoSssImIwnPi*X|H}NW^t*0mVp!G4wRal+D%mAGsMC8g=a2`lEG|*Fz{zz*Pi7 z$i?->3dta^SgrPdhv3!Xhu0X%py}tpd)k~;qSgNB;^IOfUmaz5cv$Qgvp0le^QA7l zxw$!oN~;XX^M?XZZCbe=dw6)fpD>&NTY18PCfBr^Oxnu(Q&ZjiLqFYbUtIbd9CeJo z4!>RB-E<)$RohDJbXH|&O9{;-G%_~!FDtVRQY~}6zCs}LOn!d8(}aM4K!NSHYK^hQ z`Bv5TYbGYmM$ZQas{=pQNAg1A;y%vQIxE&Vu)vk+q?Au9TrN5DYL4)sICk3aW`nUH zL-K3&KZvQ6pO}WLmE3v~rcKSwt0ojiA1o{iw-|XfKYDYwjm`_}6N!pgT)6vqS7e4H z8+*Xz36zNl3A4{7mgeV^Y-c+!smDI;eE^SY@hAAcrF71TIWZgCpTI+Zkw9N}5&ZQl z;<+xVy<}&FblS(}?rw40)rjA9;-5d`gPD;~QhGxM#;XoBfZy2J+5bX;$Z9eP{&gQp z79&{r8N(D`5=KTTw!$*gnc6!O9-f}z<5wQFtwfIZsi~=_Qq(-})amHzT5gOoFfuVA z!8bIyq(mfrm%T{>yu}e*5nlNer9t`XvpdTA~Eb0GD|;tlt`d$sHw>Zn|x5( zu5z!&YV}cVZEfW;l&*xlE|ck<-Ng|jkiynd-Nin9n1$kzS?_OxLR}j%&U|Yia>~^Z zT_7j^aJ@SHp;)A|yBzO&gCn9)ulE`5cVAz0*np)d-MAOepMOPGt>9JTWu}2rKANoo zyM02$t9P<#74rYg&Spbt1_cNni@{?^6GK&@9pmG_AT;i*Bn9H^Pt7c^ulqv878Vvp zCUCJh?kLCs(phq}klpiaH!EK`hlht38&8D8dc$?bN{tDSS#E3$FD2BZg=6z=F01kQ z0^VCC{ML{;B2gd9i>#H%EGFS`L8u~^AQ(cavzn?sSXfq;1{-DH!&^~au5N6MES=$C z;_>5$Cj4SxK-J#fj@+k&cQ>alYEO3$4oKPApQb!MKi(cuk}uNf{;?-&m~A_4|D%`p zIwnIpO#=$2W5YVw6G-qavn;JGc4w<;V};u2$o=Q$RyO67p~b|+L?-Jvmot6$yuMmz zM~HE);N%LWMp5;wkUh8$2c^ZLS;g7%Y$eCW#&+wjF9U@`$jwi7zMLJdqkjGV{r2kW zYGh>O&dGcr_S2^d*(12$Ep2VnpsFS0vhjl&!#%#Fq=dzIyqJMK!d9Q~KNWM&ZeF5h zZV#zG!S64Pp0KrF_m_JuFVC#OPV!4jQy~CwAB}3>smmuPC%0N3_J>o&BVu9+D97>r z@5sx`LlvGborVGBF})RkMo0*D&gYVsq@*5$gEHAUIp#JtEdvAlzb_han%DE{dPWO0 zPcQa+PtUjOy#4)~8ynr^9&S_8B1(xo{vH5(`0Zero!q*nQ57XD{KJB^qbP>Q1C z(j|lORBlH~`9QJt=+UDF0l|^> ze}g|P1n0dJ3GiQBS{+EHAfMY<_ti`id|o7j_QK;8YH+cCC_ZtoTZS~pVI!v2a^-cF zW0lRp#gURhnX!^vAH2!#=?DACyLh(Sg^7-~AA92SBJxpkiQaT=UtK8&of87M@k$de zV|KBg=gnhHHFKz_ufJh;Y5ggaFzM0zySw>8kQHX1P~S7QT)(h4dHi$q`>TK=(cZ$< z@8ZcVDRNe?5`R_Yn>-`9gF#BkS((W9@b*v3alsE>UavE!Hh0XFm5N`@>oqmLU-gBAfl~Z@MT9`Mu&X&;X^-8`@%%NN2fpIN*{J*=ZKcXVzu0z zcAP?L2$|Xn$SNZqyCU6mTSOr zy4oT@L`L_atH4ilHj?G`nhMAF^55l@-zJXxjF$y25S+=zpc@W<@U9LHPBu=qA$IyB zO7U?=ug;}X8{+}~-{a+Yyi!wQ92P@4b*scmG{vZaELH}l->WOBh$c0!h({H#tSdz4 zKU1=qiu~sqD!1rdTn;X_xTf|~^Qzwu^d)KIOG{=l1~ZkHFTO+^It(W@pPb8+e(+Wf zCFe^qr=<*%{|Go&y4Fk9DSH3&`$xZRqQ}{ptq{+(zLOeDIwT%#bxY%q1V6H0Bo$Wj z5)qt;Mh@W1wI{+3^We^`&51E(kgt^VC)3X&3t=Guf>AxJ>9-4X7%d+~%<_yXjR=Y? zBr>OG)6iwBD5(>`{oWw&$8Qmce~h=0q(nz%Avq3rAv<-b4>^LB*aP^DpDeK^yR)gw z!}BKoT22T|Q@rIMF@<0C6hOGd;I%3||SDdtC=tJon9V)r0mH0%Gu_d&nB$;2e z;=dQ4a(u(O968OLx@y}$cG+X{DCrSOl%7DSn5085EVPC8_B5lP;A2>x7gTP33-@1M zbzI}*>#*8yCsM;?2n8tp4TWJIfCTcBnb|Kdo?H6g#0cbkt-gtv+Sj3HOInPk?Teg_ zccyo8wyS7)mH8u*?}s0qzoCjkS*~B=Ljf}6O8@B?yXWtHhsltMQ+&H=g(=BCd7Gs2 zFf}~&;G&d*B+x(kV=E_Ow0vAfrabXpk(E_b(`5CBiP7@Pa7pIG^u6Ip53I$Wq!83R zkLqvVV{fyXaI~{Cv24#0kKp9qpW%%mNHdvTn3tLU;$x67tQoi~qW7w-vEd**Z*wNT zEA;W&@mllz^<|z(g?AL5Nsdy4ZRAVh|12pXk@f4`-{chb=#t7us;Z-o_N%l5(+;D< zQ?X|f+>$7gXqrf@^fA@Zfqw3-TUeGWSY1k#H zCeKzu|3tyf@x>>FSVM70>@}`yP$mE{z8}2jeg}ZWSf_@Em$RA%_-9ee_4Gh7FJ&_I zl7lsTR64CqOc>?)8|F}F@VDQ1OnT?jj>XQ~JYB|GvoTm?u=;m@Te7_VDNZ8z6U+Si z*DijE;XIcGseha^PT6n{LrF1nxv`Dloe_zc=T7s2-@<8LP;&nAtFq-d=@W`kEcQwZ zr%y8}Gg&mQVl&L%&h&2=hbG?N^?9$f5HvOEM z=NU6Tk?XZ{%PrLT^EqFE+EiQ%!I$Uv@fsrcmseppdSc@3JzZMcj@t$6yw{ZOw$Gay z-vOYFS@8$3&K=0R>WeFFmISPS7k%kP772?pQpldAiEI8H&KWH)N0`k`n2sISqmsE8 zzaSEX-M91lo~_(|)gFS9Z)K+5Hsd<56QwKS%zGGb_wBdi@!F%~Ao{w6u0(;9TH+U( zT#%BvlOH7|j_#hVBO)h8Uz_dgC@YoH6kT$#={F>7P81ZEp{kE4nLZ?@Dtr1Q@f9TK z-Jj#EHZ&Q#y9lfEHEOVtPfO=k#(m#ZXIwGgLXI{fViCEMiY9prIh?x!n`3+nN1F)d zjhXnRyc#)^a}#c(r{aQs2n#v}^oji6lSj1tvJ~J^KmOJSzPVu`Xm1>e{^ZyYcaUl6yQvmLh1R{Ny`D+r1ZC*IXk3DxGC2a-VVB;_vLaFJs;kqjC`D zSRAIE`{s^fXY~hBZrd2RUw75f&7|w|tgc{=kB_6u2+uZevAWgs^8Dt{$IryyYiUJo zt9fO9GyDawvvmD;Z3P$0&@0eyXC`Qghd@{N~Q?|ZaAFT3&tUZ-6N zjQ4gYJclfJU^RTS-P@d_)ZWwfr@!8fO+%A`fx4=(!3W@fp8!Ek1CdLLxIY=@^XCPz zJXz6M%6Gp+{wEGrPOT?0^d%HNp;9tmYnArMt>xYQaN=ne;A|~s8hysIj;l{hMeUo< zVrbQSeY(X}bGXD}psr!?*>A;PcX9Tulod0)+-5xCHCZZNw$<>9g}cAZH0nwZD={-< zuN*7vtMM}>Zch6ZTG5KIL`OnmoOoS=?RV3HHAjco6r=lFRTrPi=vtS%JIkh^{&5r3 z)M{!5r`4)m|K@TPMZ7lnZ`<`cI?K&X8~+EEY#4ITXxsHIWM2@}6x3_Hl6De~y-nUU zrc=K()tsBBvg9ps44Cb#w#4$b>(ZbeSRZF4;w)}szzypKSfbTszNJrhS7YsP#jS;O z`BNw%L1#MvN+o=#rBhX;Vt38s|9c0wX+1H&_0>0=vyx(6=-1nhn{5xLG(vW1Sf->B3+bxbL-|5#iF^}s<(~;xxYEP-$69Ry%8^B(0sagJi~Fk5yyfa zvD9sCoJYhdv$T6xa_Bz^>$S|w-oRe0d2;@YiJGddU8cJ0kLQ@YP1BvCWgEk%`v?xU zdzAD2<>5z+Oq;K45K5Ss;~!(%iq?l$!-pK_ye+(i{%f#dUJPUw)I!v2hv~Y5>x;GB zI)8h4*K;~WL`f()@e!>;#I)~2$>z;W)%43uLoC+Arz?v@!&iuS$Me)Gno0R(ffDl) zY0}M?_)WGa*vrx|*ibGxT{2PH+}w-#wMaA~IQ(aVQbb&6a`gU0e_ui5L)_S~kb%pm zTa$e}Jz~QD2EW}#jI!w^$dh5cU-(b@luELBux6Dltsb3tU*V?S=~6Tzxuw-|p_AUa zv#7t{DzG~{+vngH*%t%-49A$LUzv_h7ty9x?u(x<*3~NO_1}A)FSvfk3iIooz37$4 zO<~R*vO3Tstg(D_xm#gbVZB9&z$q=QWL@?4ZuTm+v)Jxz=)w5v;fu?0F{b;r=X4WJ z`4LLo?`6o4nNQ2fb3yGTy@c_n;f&$o8R4;rM08a-?cQEuWnIJx#FF(!8b{POkp%%-e?u0CTsoR92($SG zVOET1J{>*75AJpH)aWY?Y-QXI3XI{tz8~K8r`+;5aUZC8gBcmkNrFYCjC2KuI4erkqf7jZJVQX?a#t zvs$Dl8HJ2wI{L+4VAP$DhD0rtmZ+mdlqoKPd5d zn_~0G7?EhRy>w91H^*vXa(}WK&ro-nG4P#NrWi!Muul(;@yp9>N0j6yVPK_1MAiAG z@h0k@x26wyXI$0hM(F*Hg6Y2cEoePY6T51du3=|3Qdm021wTg?OpBKnm!!r9`kxcw z(@F&jng)N=b9_qmBqxwR}Xeu?@!ebC}Ga0 znml=rbfx}G#X9l_=PXT7Q*O(o$B;x7zFGmM6o3n7~!%tm2(tDEs zuMT(rU*xjQ!>GumO8v%~Xkws>Wzz}^5q~4Yr~UQ$S3{Cj_`@+UDqAzkOy$){fx+f1 z1dlnEE3>f5p4H=jN2-q-6jj2aBPWMQZf=z~V}`d_WSE;*wgwkdvk8wkt1oWce>)dO z{e;jP>wT#5mS)t^2{{!7yfQmn$%0^TbF18c3m=kgCge_cRIU<_zURmPSTNXz!Om*q z?%T6iuBJE+>H0nxS-UdYUBsWsmOCRjw7_6XV!=f|<>^XH%}euMd~#b(I;8j?EkICc zJmeudlPM7?F)@K3H{JpOOd=GZwa^xnoRSjs>sJS`O?b?DSa06E866+*|ILRAv}ug) z#NqnLK(-=NoZTGSRAG(d@m>Qu{p|dFBY>j&Mj^q$4S>vj1Y*P7%q#&w7GTVO;W6o$ z9dD^5X?&EB&;^psYHJb?7*``BBLKxxZMUbp;(6nN!geaFu~@u!eKt}D;2#Q5k4V4| zc(_M|ghu(!%F2WTX%a}J3C5%G<;y$ZL{>%%NSJiGo-;ES^KXitjXhpAecmAmS?(VJ z+l|?=6m;^Xr6+_zuYO7ycsvp~GW>yIfRkP^JWRFQ5$1!D*0t$0|9}O3&((}TW8mAW&#|v22|he76JfnK9`xqZW|&xnwtft%FRi7O98!1v#_w}FB#Bdu54Xe zS~38-!(o$zghUp8ur>x1IxIFecDk1E*)!j%TIM&=iB}K!$Hoqam0;kC2`^bqb63px zuS$jc>D>N8mRCEN;k1@gTwQ(gOe*U0P+H*DrNMPKD}!X6^;$C2>DCq3X6>=XC@gk6 z>LoUtpP%62Wt19?B?9D=siX^-;T3>F+!K{mRav@m_JSxK)6=TX2Yo^Y01Q#l(R~E1 zh}+E$;Kxuh0WUQG=6?+UQRJ5akUSkTGit~4>f6&bcQhZMp-BSsFZ0#H+FG_qw^t4o zgYXjr1H;>W!pgar42xxKZ1`XZFGvL2cx&lqS@-g! ziK?&1xvHj2RY>fSten%GA^pRy%6jvC`?ZaC#qT zYuP+ip4;gXZ%&(LS)*BvrM@}GG%H!Zrk-yFdsOB~VAt`+{G=reBvaQ+t(N-Z9 zg(^91-oHwj7{$Vl0J&0eF-fbS-TmY$5t*WyCUC)wyd#HI7^2qOdc9C0Kvi&7YBxA0p^fc0hu1LJvX+@Dbn$F#kX-Kv5_$ zcmnJnl0JZNi3Gac&nXSgC%218hb&Ghg2 zvr%!%d?79J!AQs~+CR`*iR0ObXZ8-cK6cegO~xX|?94Zf$8zbcA6l!WMF+55p=I5uUt3+z$W^NeA zF6#OvrZdyCHb4coZA|6`#Y2cMa5yxeQ!WR_m0U-MZ%{Fk4NnY^xwb_2tTPy!Uv~kJ%a5&?=L`NgxrROkKX}WjJtR5 zsskz0Y@qfTEWzC6??SlCa==!BaV)3(@Pxg?4b0Z-`UW_{&;Hw%SiipbA#`^1UBii9 zpgA~M#m7ilWtG{PGd5LXd8@>*iI9{3J^w9Ab8{#xLR7x%N>r8GTe=OD>gZ~j=`VkL zFPHPu=+dF4!mq?=a&m`&DV3(NYaTRQm91ddoki2!@rF{}plmugSlCkk}`iM{)s2kho^w;Fc+Abk6q5A=6X1{qkK=@QWaIL( znyN{6b0CZC8AXSNhHk%^cG?%e{R((XYY?J2O{mm5DUOYg zQ@sVn%16^Fn5^~rc!i~I(DZz!Y}Vrhs6=G=`T2uNX}xS_$C8CZe5PuXjiv+iO~ z^v0HWFD!QxxAs_rSS%+}BO)a&4YkvK%3~9iNTvT5mAkv!O1z#!{Klz#i~B6vw6^`h z=Calw5U_Z+v&>H>ymN;zgbHj>^M(h1*l8wLLXb7LpTu zt4^#b&2Y@xvRwWq$R}vQSVbA;yMSm&nm-UgG>N5!_#uOiELN3uIb3+e`zdyV$ zo||}{)|alvWh2vCdnPhvKl^#UFt{pB2g(VM;^cxrQO3X^^WOdYGB;5%26OTt0@RM& z#U1YKbZ(ae{(LB}?kW?+i?Rv|k!Qfs$Uv~LUWYMi?yvwOnUN|6CH)RVE|LCHeV(9j`!sm3eYv7Zx0xNUe)|V0u-vZs9v#Tl^-v@WZ$WWf&akp#YQZDJl@T z7?0+^^T%TnWYO>E=U``lg^i89I5(FFTyk2e@q}FBQOfREs4Scb@h9#iNQ(F)TqxfQ zsCeBgvs#s!N`4O8%S_W~xdf*lwExI0!O#9rM8ZG|f~J>>7g#@}#2ASx{O={kiCx;H z6xbK%+u19_{+gCcp{unwZffovU&jt*@%ffq#){f1jA@d!E)h~Mw%tG9X+)eID2gj9 z8x)lC*6c95TAjKp)t8BI6jleDk{4wjQ(=g4e9GQrVk*Mpw&TgGF3brf8L-{gVXSe? z)7Tiz@$hI0TdnnYWy)-9%UQj^q-%>lIFIE$_{pNz1@Oo$exm@i$x~ z(G_x*l4JLD)pS+goLeY*WE7>&;J;)QK)gO`PykZlRsWH6+LmsM-&;gDjeW3W5)t*` zQxs2(skV-=7nRF#aW>qi3nT|?vhi^|>+=g*vgGGa68(S@mUP%st?3v`5j|aR#y!oo zF%B;=Xs$h;S>Bs*osk%Q`+%*C(f0)%U6|oWFye!F_uN7|fxx(`Hnqu}sp{if4Xhqv zHeL>L+2!#H7{s-53!C(p&S+sd2ro=u3TmFLK@Fybv%dAp))y7Qi3O#mb;*v^F3w}l zrM=uquKSVH@{bhDcbNG+jhcoIuk}W@7Rd3GPq6=z_~{E* z&%avyA^rCydsD^#9Ungn;a3MKqF(IS6EGwH3%84TvC=)B1NoHBE+RPZvg_su?=!}(9t(!j|_ z!VVgoI5s#bkJL=$b4e}cnyhQIv*ds5)T6eLHEj49H4v@jcxK!q2G9+y# z{i4)5oW99s?DL#<(}nCgY@|DC64bvmL+m9wT`M5Wi7_#1-0x-6*ik38*(h&1+6)4v z+}*bt8k_{I9z|dHdN5zn(>ppGW=bHZwxNhABt)6w+aVBK`nqHM>Jn|HxP6vW$kepj z;jkgg)^yEgJK%flGhm)Bh6_kmy*W@@O)Qt^rfZ#}nsIR>I&xJa4#NfbNulm|kmN8y zrS$MD?P|89Yf$Xvl~2Mhy1yuk+*fea!^|6qEV=LavBh9f-h-%j^1kO_l2G%YOQR3; z-;<^|aC378!2C=1?a#Gi{pp(z9^6+hp(^eQE)~4VdpQ`9kPv+fwY5N}`}WzPVcT4@ zGlJcA3umHCs8F+&>}bn>Zfh#$o~V}A4RqW%oqr7j3W`ynWq4a@oux$1a8HuZ;-k{j z#kC-k%2udj>@e~9w~1XBhJ11D$w)oo_Lm3pU0ngUM2w#1xjuAUdyD|uBw>-jG*sUS z?D4go%U=Dot&0Xm%g@KLp}ME;HQW7#{eL+AVN>K{iiYJd3zrOcz!D zlU+lib;-ZJt(TmG!@WD2WRFIzgvukEMqAyt|BJ3}eY`8ipJ7(r*Z)p-xva??)YNpR z9kN(lFAurPOlsOIt$XLTRQXKL2M5J^V%pDZzo&nI04d4oy63%R9*gm8r4CLn^DSSt z7sJvv0Zi;2)9ys14`t)k;L^O>KiL!Qp_aQvP~z-@wlcTmn@o|4%SFeRt1L|V`gO}} z?|83`@~4JKghnrIdQ#+YY-|qHDjr!9L^Jx+zIhWiRh4u<*VpUAUjl^o z&u{34^iP$;qJ9Z`xT$IgKc(_F%=s*Pa<~{_vjiBizUV>Y43SeJ6jKHub+0WgX!#MyN4(gV#E)Y@*9{HkdIv_-nM^Zh9!k*ql+;o&K+neV)U z0af=44vO*1sjAwt-|=~(rK_`6BJA(0Iq>(lR!WMSU}K1A`0QZ$K`$z=UiUBbWZa+W z_o#z}h`q=es2FArf2YJK-1BLTd}RNwX0@L#sP%i3`F>Zo(+KX-7%7ErzIJD`(@2E1 zx3b|il4frlq?zqV*zk z9bx;+#Voq;T_w<&Y*xgLZ0`cLdr|Tw>T5Q(FN+;lgSoMm(`QM6 z7=^}4q{6}+X>Y{DEit}NlnV40uRg+|VOLpVK$9d4E*7X|l$II=;xl_?I(FjUKRc_n zrgYaU5MJ~dJ>`z%t+XN2Yk!0|l86&qD2-XAT({o-xQxftLDupO?sz-A4gHnBp?0d) zqbqqkH)B6p(MFGS8d81UWEmS)VTRM=6AcU^Eqz}c!qYub zF%P)tpei#->s9W-GY06g&0Y&Q(z|(^sah zTX^W4Kigj}rythlFRXDJ{$CYHoBBB4-xD0sHqSSYPUCO5cs%x44u9lx2^GI>Kt;Co z>Rdannib0IaL!|sX)%;PLqndM6R7+1fi(qHwklWQw7C9T))W-Fj~%bguwyGyA7l-(kJDW_{-J(i`(Z_dwM&yVhOMRm=@@>Z(hOZ%%9w@)CstWFMn@ zb#jvcH^Rb^zGeC;Y2Eas`v~#!@?5wt8C{T&5XHl%c0=iGJdHzDx6zuTvzV`%6mcoPI~pweA=c~}_|%(%0A ziiR0TJgRt)H{9cu7wP7Yzi#>iUMK7Hh#S0@p;>Mm?iPNlDih@u470twc=iXcRBIg9 zYfJ+3>ROVd(<~f`&CN3eiAm{|y?T{i%C}H#`Yrf9ifEJ1!(gct(qC!y`i&;LCyh_G zheblid$SRH;B8;W^rGy`k}Zm`jTZ2{9--_z!Au>6-dq z=;j*D;Ho7zpX@H4sSf91QujX~CZZ8ewaCezTblj1}CK31Rd}|&yQ7%wg9aqxx z(xNgi12O$6jzV{_eYu}1xnO55Ecf#IU%!*aCyKFa?#xP^K1)2P#I{svb=}vw=ZU(WnO@lA*+|%OkAO#jsxIP}Q+A6ak8!jaj4F> zrFV8c^M2!t6Lx;i5PEBKlNKevpxv>($GwJwZ}|u9Gn#E)`&m^S+%jd-MlXxJ7kz!g z_JaP=QB&93ATXUi?Y2BFEn+IH$fw)>N+05w_hs>?ZNNtGMceC>vBB!=F+HO4zSgkI zGqSzzX!<2ef8^Q@Yf)2Q;)QBz1hd=a&q^MqbdQWgU7r8g-|uyfdi^`Bp0(wmGK7fT z7+DETI~dB3-JvJ?JVdU44SG@#k3c_*qGH&!yor5lbkwg7&w6)Z|3K7)i5QLprHV%& zMnU+ks}Ri2Eej1qsI?6C_s^ac2FJwwmdCfXDb=a}HeGBOVM$w2<@jJY#}Nl=5tV3k z+&MIifB_!N8N0ekV;y6`WxUwkXaBO4jvA(M&AM4k?FB6a3mo&JS--Czl3rf&j8&gr z>7E@;7)P=f&@L?%f;g@ymeuwZWjK)1fTpRAGu}{6fVt z{_3VBAKuKpp`T0LDo=STDRFLhji@T*aoKVxE9qSS`yoxEWK(M7j*FRM5K=5qZxcY= z3rsvh57Za5Gfvo+1O#!POa187T=cEBD+}}UUoQp;Z7?wO?Tj0CqoLt7X62pzZXZG+ zd_61K6Zfopp?$NUm>KlS_`1vIJW{QWWnY}E{v=g9ZE257nB9 zKir73kG~W-@oT_ZPG0bm$;W|bZFSgCjJepp?1ARD*1vWNnl;DrgyY8RhuN*^(n%|O z0=P8m|RBw67wC6fCXcKqBxN2h`J+V3R;!!!Aj zi!|Yq0tPrN^;BQl5Oj5mTcIj_U1sGL+B?)T;@PXKNp6wh>ty@fZzUtmIKWt7Q%WaS z4eG4;m6ef#qM|?JoY&VjwYAX1#p02k&d+Vpyg1qxG?J*=*fe+x{bq_4?F45j_x=Qv zRs6s+>gBl^xxIEWiMi_xUK{JpJ=0{jRzV)mUM%8%?16&zL)%E^3?BNLgQrA9rIC>f zuDu(z&cy#FDbayZR6jl`aP@ikL98d3bt_7`6HL3eERRl^nK!5Zz%XY z?~k<=Xp)$ly_yk`k%V5hBE7zstVW}6?d;fra636W>ray)CKrqRT4G&4a|$wTCdVTq zKy;ho=Yo=w=HA{wVC44tMd`x^s_g7ONL2l*a#*+v5IcHX6nZr@V@8hrt&0w7>GF%# z?OEU+*3$z~QW)nKLq(hf+myY^#DWtuO0!i)UT({`TKyMXj zs8v2*CKul;W-2R9?VW4Z6BGL+Qm{EB-!2yB{nEqkZ+A4MSgga>vqRjSt8+);4{dlH zTMJsvlNCJavee5zrZ&c=R;;#Tu3P;7IUOmge{YV72OV@c2)>g-HO7ne`2_?Xg8p4f z>JbS3(?Ed_JH-TTB#DW8J)Gq_-T2ea$0|U(L~>Y?Ll5H%8XCVR)N+4;cR~QJA_%<1 z2Vr5#?J{{|7o+{<} zCy9lkAA1t)_fxte%|F=6zsAOX0FV*aOOn>z`0Ghxw>YK|d)~=O3o5LE)Mx5Kc$4eZ z<&UtjPiNgR&CJb_?H7S>&h7$5I&}s{Q{ZyxfXG#=>uFF<8$@hP*K~q3zo4*Cqc@JH z`WWPZ&`1HeF{4%+77V)ufL8DN55%uwY z0VUxTKEt=|sVT+jN|y6CCtpLOkJGZnYE*V&Q$6fPlhbr9&uxB97j76eN2n3~*6j@w zi>r>WaZIwZL>85P^|Ip-h!G2sUcj%E5r(mb9X0mb0dM=w{JA# z0!Eq}5}VW3BL}^E{z*c4yQ^t#qvO8@Y8-hSj*k-M^Uj>EDtNbR%H-L0J8GTjWqi)9 zuAy^IAc@kh>)l0-D8C{1YmAo3NkYKcrYqT0Td<_1rIC$PF!;8%w&&1@3+*YP+&e#F z;y=b0{f`!abkktT#*RH&)$W~br&#D*T8qDBk0I|LC=NNH@p7n&?a=Ws(Pn*k(IyG= zMP{N-w?SWa6mPuCT5paL<;JAF_cJcK0%u23$zv04=qIfQv#wmxgG_HG{Pn0Yo?zXYY|prlY@INj0j-M&DPq}6Cgxn?*RgY zxUXNo-Z%!0K`XE?&}e{OT3V{0pzsL@SWcUbHa|S3yANpXY%=GXqA9MpY!#+cAAmH! zS1jx?c2Yz>$aeHW1I1nT<>qyO@BH@~M}1!XM_YlsbZDSHF@s8DdjP8=yq&BMK;nyb+fc&uZv0}W@W{E z4Ly%2&@ZYzS#EAWj>PG|*M3xcXS zOg&pe|L`ylkRs5Q?&ae%2Qmd9p5?dEmHX`;aIo6a>0`$DmReXOy7a~kZV#d7P1j`T zH?7}&;gc(jtqbX1r@=!GoXdPi{r-Q!kxQw{VcVI@MhItAbfc)yua1mbMn*Ky)2XgT{i-0*a$Fl}>tTLSQZ4vU4m&^D)BZ5IS_ z`6jZJ99pL%bP1r(64|iDYV;Jzt;3}tiX+>S9k*+KNcsG)R+|B;`mnl0*^8-684OvckL(GP!M?n8SIvbe01R}1r? z<>x5Kf1RRKR_SyU#VZt8+jh7joIfrT@|V+m@El~q){y}a7?n+r=yhE&|kq4V&~)d@V>fG~YT=lbdr;YZA?x*Y@T z9J0ZR@__rJ`5a5K&QxV}km0RztV9dQF1r0;UmB_83x^rm*jhU}e4w9|kQr+xAnP zU}J~ea7BA_DAV&N2sjIKwh<1^Has#kvz^&@g+=~#vRcA(Pu_d=??DSxP;l^jpsL_8 z3dj~FAPJDEsuJ-01;uXUV<244H`ykqrp9WWxnK#kAD=d+eJ0-oS`lA4x5nrtP?7u{?FW>+x z3!7A7K7WVJWb&2S)fAYD+4?Xo*j_8pMI4StSG1?qH8oM}<}ZOd>bAX3d6)+>EpkY4 zP$m6=l*JAY%%GObR)_ZN+a~)Ur(x3XCxvF!(PI6Om{z)*LyY>-QBSswZ=<3z*={L= z`bNVncj^L8JO2knaSA^2Ze*^mu2b_srag`JULs>174c+&6}(1iK_kb^vo;F z*?6}vp5p2VZOMl(a2U+_1PUev#QCuwU`J#tJ2+%tR2=Aq|2pJ1_^hbErs-pdXAHpaj&0b?AM`nD}@gC{OsbPoZ5I z9t80eT4|}u>FX^!Jpn< zOz4n(MN8WZCXZ}WeewD=7WCGiKnBZ)?zgQ4Ssl>hnORu8hvk4Ma2Gh?(b3V_=^96c zA|2#2I{qy0uhKP-y z8l)RRI^@tuh_rM_$DQZB-~A81amRRvp|mq~pF8#o zyQNqe@J(O}4Z*jQm6w;ueU|@wem(%W3&z`X9f)sVYOkE$4l^;FI*=j7Z#dnfyGVcE z7sOj2{K%-Rqyfqd0SQS<%|?9~7><>BuS*izj8NPTRoydn`%}$u7uPO_H7)L-EPh@K zrxUmcX6X^ke`r{kk#YKo&QlK$50H%^i+yQr0HVOmt+4ARa{2P*&CN}5n8VArG&d(^ zBPl0;qgvT;Mn7$c6Z8jOy1q9vTCC>kKF-WK&mGZqzBR>EdD3HsG}h+0@yx8O7e|GM zQp-Vpe)^}vGW!%%|dR9F&lFgYfvG_FwH_Gq|hebp2fDk_4}$TyiP^|uv6_ZLOspy%^72*bPeBQWJgh^GQvNiI^5dD((ehWlPf&yi@RlOiCzq9K9?;&+#6dn56=8eqO$<8n z{?F%vBkTQ=1$M9y$AwpZiC0s`d-`{mQ;bZmBS@aMQ|fv-VL$nhb<6M1U#^(!tXf4VCCj=WhyE}5qER|PST!(3r|7Z*NUh7VCv zdhZ??I%vL(uHW3Iz(R%#>ip-s`ouXuH$5Xz#%HxLj+R%*-TXHa-=C{NWjoQ1gFH@} z3v-!XD_Crom9(}A07sJK7IzPVbiGe$3chswa^}0Fh|D9|owgAd#GhA+#fY7q{QAvB z!rQv8!T$b_rDUdO@KmsT6YrgZmQHe)hPB_n!N=;ueH0cY8@H307PdCozeWH;#`0Ku?muY25xY(+iTFQTH zLHB_T-(WG&N`Zx?v@}x4eY9^!tfOPp91zm0jDD70tsQFMT@^8ud*}D|JiS+t{)blpiq)T&tr57~K##_K;1m4u;E3CV;hlU`-AF`kcYNS=AT$m6%Ub%}u?lulq9 zqE6CK04Qy1oA{kSE{;O&nS7~(FuLdsHVTan#X^dUzaof&!oA07Q&)EuE;J4dC`I*O zk{>UdsM859Dw3>p=hHB%5;r6=Fz~o9sNLABL=e;d;rZJaEE3F200E8Mi7P&Og zCT*^m_2-M?x`Ylh>za1=S}LiewzAsmXKUJ)Hq+kT7e`B2X?#~_z7td((O`E4IVo%m_7g)-CT((I=z?@Fz} zt0ASl$+*CF4<1f)vYqoo%>*)R><@;vN(}|?l}>i;>};P`#B4-axs#KVNwbvJ!W|dc zW=D&8?hEN)As6XonM7qwLQOaiG~+-u1ee{u`)mLIUB-_fYA!A5vc_Z}Xz=doxbua0D&GxO4yAQ*=^0f4-LJZ(ta>YHewUWjQE$Suc z=OJRLa#Q4y#O`O|LV8qT8xsAmZ@ungMe6kz_0}TRGa^%TNVGEx>0*O$;bL$w2>gjq z#!@m!Nmc*XklJO;RU9AfiGvgyfu#m_&0Cf}$g)aTALT(?-RE=ESR9s-n(<-^FQ1{M zOzMNa1MQV(1|NlNuT#NhN1p2I14d5<#^VZCs&`Tt=AFt2qI_(@LzX`Gbw>WQxDOsB*D{;@iuO3Xg1dPk!-W1AnGK z8~Ro+1BJgM-r^qqKLVNAgz?O(%qo3$Mc0|?$QJc`U((G5mOr#HnzhAojCs&4y}*+p zC#L-&$?17dhexpORWJ1W{hrGquLf=k9eeVZP?SV(Y2au@?Ms&lkGdtUr3{1nlj5r00fd zn?EcuO@F|QdP%tM-U-`r)4M=pPupRee3bLK=G=65+h?cvX!l#x(qE;IE_P+BU)D%3 zsigQ}`J-JlIikzJ0B`zDRPTV`bwhnbN`L$+%ka2%W8G~IWf4lI{@WQ!tU(%_5`rbEw$z)p_!+FySpJWLfg&bdm+OT9vsA`Vth_h2j%(1>veR4B_ zh+Ww#wysbl(1r#NVejFT?uA+vw*%by!+9bDN%F}YcNJEv9HA=76Q#0?PmAzvijz0NGD?)v&e0R_=c+Ryp~(CxtRwh>rAe$XUvam>E!N>UA-nh zuDv}sLrG8L;;S$!O6kSpIs1~p^29+RI90Q}+#hz9XS0_*ESmd*YwWO$W?LiaivAUS zo}$1DwmmImqaRo8IzNmTs6h}$eb?adgK#|g=mr0`&e!9f$Faa&BEOH5?u_h85is|t zH`XEr`<>Ij&W9a&r6?c8mG*t;fV{;VU!|VeXIz=6skYg+d7>_+n_`dl+qCYbqKlNv= z&wUJBmPRzu&cdXuWbz2&oa$^bkWY$?k+|@|68ke1FB>IB>3fF-PS8AWY4}z9y(w~n5Zx= z+*nq~UYl%gI*AGJhwY=8jv6 z8f+#1D9X+Ky@r{qe-2-c@v!PMmTL1Y+T#w4Xn_h?8hN zd`;8aE0+DiC82NeQ?<6ech^P(Q|JT7>W;H!-v|bNhn{2yVM@k?cTG};*p{FF9FCaS zl98Ob7wt{qqBOxGjm{Oz%~RzFtENi4#q*7>W8O?$!Vwqxchj;|lQHUwHE++X#3zo{ zaJPr^N8>l?k;e(YGd6uT2&bINzuqpyBNP7Y!Z+bE(XtdGwLl|S>eu_Tn9se))R&%jNlW2d_1Mo9C8zQ5wRP=T;eKH^z;4<>(ML z_8WTC@gJUm#)1G`u>dnsqrYkX*mPJEev^E`k)^LF-|6mt-QMn6o0-eJub0OrH(H&~ zr+ZwLQzv41_-^u5HrifICSfQ^>TB`8oBbCvtD1+OiOOr8PV;fq$Wyt6{j9dK zDvO-I`iHQ-s$cl7_#ip$5jO4%CAIWhO*MGcIg_7%dejPtJb6gv8swHM66jw-+|oLn zCM6WkX-OQAML?=P*`lhN5SnGZtx%biEc+_>{>-g#hy*jOUyNz5owE6BHGavBZ$j!!Vu^T= zSLq$C&~R=O+xAhf*oe5s=&Pcy6}2ujd=ZrMo(4NMMIp8IEf_n%o7&H6^SY5LLuSP0 z=&R+4YoYsyz^e+$CuJrcUu(a-Bnc?TO)E8PiC?73;EYiZnWmAA3u9}@#V9s zsctk0V}{yD)Ofa-+$@bA8t-odh1wU(FZJ>0Q{f;f{blNudSZ6Oq;lHB)vj4t_!&74>RUVR>G90L+C)-r%$Nk!&iQRI4 ztoj$H4U1j2rLGd)zngB}j}l9<<~972NC-aOvLx2-_vMrl>FgCV!^z1`U;S@@Sn9#r z?^4A6@$8a6+nnLUCyMURw3N}Jd;s(36hXIm;oiL;Yz~T#9;*&ZDJjlM z>2)Tx^Ib*d!xDq9NiGeLP_0$5La-E*onIK_qg899^x*Y)cjJ7uAfav6XjPLmwOSo5 zrL@ST9G_pqO@ERq!tt!`Hq`JC!yqpI2*DAcu|#|M>l{~PW!b04D8&ld7mCm> zdE`GfS$VSU`8b|iXMyaux)**r8Pq2%jr38&8|}eNkkRiQzJ|ap*B>}po~q%af)cY_ z>c$h+*8WSw`Fw)TrOo4IepR>y{ER=1H1QL(l8su~P zA~iijQwq^r#|8y6F^KK`fT$JsHbMeHq^oX>D1QLgb>8j zSsG3*u9@Gz8`s*P=ycYLym=VC@~E+KMW%Js^tn`LXXhxCB_)bqGep$RG_|!$$V3ms zr)NYf5)x?E>(n$fR)pyN7M7OU5uQ&^+aXk!wK)KVGQ&X53UK@aT(MOMvC=Xv!oNhv zK=B&L_7oTQl{f^<=EGSUD2)43L}qSo9a?SK3HRU!c4H@)}O#fu|@?lhd`^py0@a zpP!!u`30cg{fb|e_8H^$og1b2WQ^TwE0AY;5#QI*VdN>AmYA4W3S>u+u$ z_S3?UlP_uB*a%$vGKA)7nWAWJ=g^Uc_201hJvONTc`beSWmZU1D)(JlCNm)cbUG$x z`~Ca($^{hq{^8*v4WtHdP!Ix@5EIbn(|nYwW;LakoRs9CI02RJ>NSaVSpYFd#32PN zub`lAtD&bC0jm)U!4%nU*$2;LR4XfgD`3*16cf>Z_N-O({KWAx)Y!o+XhF1E6AT9RRv|3wXoQQc^s{n%$jUU1J)6RRR8OA0}rN7e`G@LShO65#_2V;OH&@ zZC!+~eRk`=i{Jy63B%SSA~tCYHA9dq4457P#48bAkj(tIXYlTPqSo!3(pYFHQMuQ# zGvGq+FKle|!JQ@6)CfTh6@6G#l-=h3GuS2dM}N64Q&F|Reo6#J!x*g7ZwnRPZ4s7eVyRfF@RD=WYlpdFKF<_OPzDRuk&r&?RE0yOb4^ka$dh@-wtoLQ+x*gOGD}I5QVl z*uSNINlPu!v_8nnsHcv4?5!FBx4(OGGDS;U`z|s;_-tnp&Ih7-5I7`;g@t`D1~Zuu z5<<9-rB!73x-&slMMV=dG%Ke(z*o?ok<^=(t1@iDzO6jCU&C^DJF{nYD*+74_o%1r zc{>%GTU*LCx$!4ST0e9{rI<@>x_OLUQ8x-5{+dDRbnby zN>g>Y3%*z1m738em(I^KFffb(*Z&9L40=)&`1-CwvDhBuXMoS$OggOUK?jTkn96)! zJe$F&RuzG}&x`(<46v<%ZD?KGxr$t-p=nnF);wgKw2X|Hg#bM4vHUr{GWIXzy_`Bn zggLN^2r1c$;Gukjx;$sd-|vlE722-=rGFGy@anB9T3Q{L)bG*WT2~5vnGYN#tvNY4 zYU?Jeqs1ghvZ$B4--Za#jkgXx`62J=43(PP5art&;_!gX?)rK@ z5L>PP{T;f+%>3F6$cI3bCu?J(xUxplvyyow%`G4jY5}8-r=6I>oSDB#|M!$oj4$o#>Z%f2g+nAaZxAyb2oI#B_vSh%1DyDtbb=a; zox9=15T|YOh=Gq@{wSo>#z53I25P1rKGsejOp)gMfw`7h{NY%JQ&Us7`1sW4MPFMis%2@zliPU*g{Q!d;`ur){d^r4AD>${ z4Jpt9i95G%KdbJ68v4oxEei{ax?|P%rB_Yzp#GBt(W!DUOSwDkb1s6@cyfA5{azLQ zzW*8ey-%Rkh*dZ$KS1Ezeo<3XqrigW`Emn1-AJz|7AobW=SAmSRy{={Ug37dCfs&R;7L8H|HVMU$syUREErc6kTlKTW3#C;r*I30LTta*+Jgb zMMEtOv}`B@^mgGeDA{@EoVR-*M5*e`F9(|JUBnv7sfqr3!uKo-_3N}P50mmaa*|Bu zUFJaIAV0EF?QJdRWU{u6rzXZf8Ehd2dRgS-lQdD?5o|LI1qIZU9Pj!Eg*Iw&#P_6D z0dmUA*)_Yx1Lc(%`ahkpA=I|^Q3tVsKm-e+2*CxV%)~Z8aPd^WG*yFey>^ZX{bQ zJ&q0YRoU6>kl)9HRP}dw8gaJqaKa?Jq?`6K zU8uLWS3Z7(Uhi>=4Q)p8KNE#qI;`egCa2U=RtiD^14}6O_xsgV5hMROJ157zV77xW zKq8{6>%xT#SV(ASXzI$JPvsbI9!{i}j*fm&QDo5jBox%KvrsSF0#M+0?>qYX@P8hV zSvxuLVN^D{b?(%_#%1T^{0<5T+Oj90oD%u4CC0Sr&CJlh)&n%-*-SbrlLR#Sr`bE1J&Qa2 za2_J!0GILmWzgWw;JX?+07pJd`v*Z~?~yZMfOcacpc=B=#a{*==S@R{7={H6syM@r zx2zZu%iGx4n6$LQm;0)*wTTO`b0P%K09jCEIlu-ubtCYfc~Gb(usFqF6d$d{vulF@ z8{7frIC+%a6l_Rf48QF00RO96`?#QLawj|*14g+oD4727BLdw!DgpZqB2eNOS$}YB zBlcxdV+3+(vEk6*{%VU$Qs`~{cB8Z{{3;Hn{*GQnMMceaAC8&zPI>)DSJf%6@w8Sh zP!SUoyLxyyu7FGfl5+XaYTNCKCZiT&6(XEXAJeBv}JxUnSiy!*Q&{V>CV~P}%l889q+%cVJkVYVNr&--4O8)?? zY48vT5RlMFLRmR_&3S!-@T(dTptM0+D3k9M#US*)CO9HA6n$SAykh$deQ8j=!G++N zr3hq6ha&qM(<3efM7-cKl)-I&gWJqJh5G$wXm?>;Oar);r$;;hn!f;Qy%0271t!e+ zaC@F}|H}((e^}}u5u^28y`sOvxe2{kXvDmQG5%(an;F>jON@+>@R&i-kR2|m|GKkK zP+boCsw7>XSNu>mS?{H@ybboB0ZzXQNG%}jCvfCCF`oSLQxELdAC*4W8vh`|;FzAI z3eVK{F^_Ng05k-Yyja(S@Z;2Vw}s4{HcGI@{A9QBZNV7_Q2x1vR;{c~4$>CMrs4u6?AY$xH&&bdM z>-?+6r9rReT(1x@X1QRYjg&&5&!dU8fVa_+19{Y5#S+u z7FR(c&O`s_>?3glF$lP3mNdk&Su_E_II>=Bq|&#Qq2Ua=0Bq5V+| zEqw}BVZZ;)(-@l1&4RPn@fhQXRWUdnzKz-cjNd4Fx~m%CG*X~v0@i(YSYU8oK|Q`0 zPS4@xd%C|sVbX>0z^m-%6*^ThTAlwn_{GAP!Q5+se1%#mItddRFau?geAlor2S`f# zZr!?7Nm;res_(fa?F=6hoCmA+3$%7So10JFJP)Hl_;U=RxD~HE@J^U}ulwVPIUq8K zetARl6sPi-CAt0alcpy_xPp^kn2JG$ow6wl_kMq<0tH^MjhfBmPdDxF`(B)zo!izCDv5$@F z1m$$5HmI{3o;+Z+N$l*D4|pvN$C?)K$3S#r0+W3R1ammZ_;WM!El(}1ovxeU>4@=r zp`Sl?b}9oQ;c%IihV997(8QIScD!}R|6C~I+6ekzXs+ zk>iXj0jk0th_4)Rx}mue3Oq2(;NY(*0_4j@q1S>rxaOun_U|4Th*bn?55xVJ;>-9O z;4GOzbj29^wJ*>MilEWb9suA=;05LVhY#IAu+W0CiLUN$HTPTa`h{tI1jkxs$g^sf zjb43^HNL%_KCzLj(sC)W&{FIzoz?wo*FH{tB8*7Pf|If}lK#Q>6yRQ-i<*QN=j3n> z14#i-_&iv_uKtj%Vj3{%TzRTDEw4~f6@lB7atb%_FLm)lt)9W##l*;_D?v5cfA$q*+)nZ7F}WPYS@CROQK`B)-J2qOi` zaDsMXh&U{wfAoaRfBV-G-25SdnKMxUb18zq1_kkT=$8X9r33*x zMmD7n*&9Czlx1#3wGn6iCrsk?8JrKp4DtqMkpAR259R(FGdcWd$>MQmReCg#$8=#t z%*@Edi*BDg%R2GR_Y#Q|#vpR^Zg$rdX2HFpCFZF}cRG|D3h~{oef7b>LH}l3Cr5A7 zgoq;+(jT8uZ26b1c1q^dt%i`fhi=l6GF?)pkV!h;Os~?P6cOze6%5w3sQC>C$SYe{>e+HW)PRT`!1^9%Ip%5Oo=B>_MBLq5@R64Y(FL;$f>E!@(?OL(*q^?$-#43*vH=<;|7Z8ln(TvbNlzS| z>7ORwi2Qiv4T2;FB#x37zxJS6OI!8faq1cr$w`zV1wOM> z4LeLOYp#jLtkOCI(s(R6Eh9TZj)>dJ-A1&~ww!!XaXKG}Vbb*MHr~|5i6Fn5m&jr? zl15Co$R$esV4}4*v*#`iw-jI@l|q%X-|YLceBQZKlzc0-Dsi3bxQcA2&EX*9<7Gdt z%r+nh)qCncVbcv3C9VX_8A}r1uAYOBkf6_n>~WK@+zn_v61+} zWQiUVEh6r!ku0{X1H&bJ#FQKH=-sd^Ng!a3kdaG{epJ2vn`q?xu;jdNSds8d6$jg02^sct2mRAc9M>5ks`1ZPU7*8eq`)A zym2L9KOh2cuPjh3=~y+&-M~%crJaz?|wA0r{_dV#w^8U z>?W+w1A7iF`#kG;!r}JgZcjHhl^vB!ZoCw9N;bcTM?PdLPL)Kef{N!@vIh zle2-fxsJJY@ThOhoyfVQc0%Srzxn|-sjvx#iLJxjG{E}jl^mz;~owu|;)H+ds zfe9%4sXZfPtEVaG&XI@v3})`iOkHz~R&4U<1Lkoob3C?bkwulcIspGec0SyB;_;=M2XpMAIKSKe%ahYK7w6o zU_H+o(e$o5AV$V`vg#&0miaDA$j(B-LJD7^CcvRNXt;L3=0!aE_KbEbAJUjBqCa2% zi_M>g4Gi{@uU{Dsd~;Kv60_V$v%ds9sd-a zS1IfXvrg@3X-s%#5)BU%<`tc-C4$#6Lkt?OFTWf)4EihS<#e*D0h{9mRAXIajy5{E4D(A0_TDQv%NdK zM^~A-31F)xHFg$rpZ%li$Ux7tX1&_S~NJfg*JX;4o&zCulsvmy!ltBASD8nCgw=J4TCP; z|E}LM9iriWliS?(d1NYsdwQC=n7=cz^iSf4iu4@JQcu8+qjl%SI%L3dZ_DpI)mOiW z&xLbyQHL?2TCF2kO-9yh8McI3%c4lNATpnIQ4+$)vV~%8ha^q`o0Z7N;y@93h w|MkZMk0RR91 literal 23658 zcmeFZbx@pZ^ENny1d?D0K@v0sf?IGW5G1&}1$PK8gM0FCRl8fYe{P*RbvQHg*xh}1Uw!q}PmsKGsCfFte|3NX35*LBoBmVi-m>mUyyoN}K2r0WJ?asS+;EdnhA5QLPol8`H;-s)cbCZ}bRG1$FTKJy8Z*O!VRDAtokiU>*fGN_k#dqF!z zgrAJ_508}a0IaC^Y1UMovf~AZv%c@LG~&si&$9D zLW+utRExyG;>JpZ&piDR6{S({%mAAxEO({>OU@?yRTF$S#Qem9?%?3y(^^-g-?wj? z_0b00&@=iFJcgCOp@b8RqK_5)&DN(3_jo9B{DHwRqJH5aj+V}jb|?L5u_v5|9o60b zgIau1oNgnQcb{4yJCntORH+_+`r=uqOZ1UD!-&%r(#39I zdiN{cRHv4KV^Dc|eiHT*(P5NE;Yd33L58n`SSS|hWM>~N{h8H*A z)v2?Kh>NpA&#bC!<|Q2+*}yZMYz_N{3*P-qV7J_ubx~Et6A}_~gfAp>J8T?GXxWx} zT-pQEn2+b-j%Lecs}<{th>9MLNHLW3SC?!@u9j=;%TYS346)9qw-23=9n~*P`TH_bMk5t^&Mdk?9ybo`$Jjq;~s?~HqJOa@c>U&!&b{(NVsUTgnWj_>fHOaj|);B6I_ zlVO^b7P$4_P)R)^V3WnHzze7S@-@i3P&UvAvd-7Vt2cy_w2* zJ~tL_Zte{y5THKLbhP*&_xFM&tW_g=^-9C6UvwOTaGSZgxu^7_+m2R?O^scX%Z1eo zJ?GaTFd^mWH4B6bT;;gc=I7Ia&4Y{x4Wd<4lKV@ozAw>HW~yz&L;Dwz%iSAOA|jrF z-Oc5C@LDpLr8tw8=$;~n{qMp82^CegM=v@Ga>Vt#p#*pm)GmJY;2uj5Mj%9jUJWgE zxk|@!f)XD;E^Q5`S6EH|umGWBY61AB&3xT+eEiO!7gT+{$Cx$M0q1*V<>es-@KpA> zpz?B7Sy@@_CXd>o)261Tu_7Jb#j*x0LhG3dni9{2y1u?XgUQ$X^kB{Q9BS*xiJo!)+8iGQk-;zIB}AV9oyrgoNU@CRliS})jOw2qg++DO6dy;Uat2@fAW z{0#O}T3XsuKd6Dh8?7p<*49=sJt(-7&Gw)d4W|=Y^tuf{4-P(SR#|m}AlkQx9M>K| z>ebcYc6@QzN&1S_M7qi8{zk_vBt4xR*pA}u+sGe36kk6sFE0-Y4ej{Ej0pKjB=F=g z{&lCDdM#pOiEmAGKERR>+ET#kuY%oBQ(vzH_QkP%vTT5CHaR~({~~Ekx6#VY<*|QN zDyN_0^|_3wjMWQcDh>{g#Zc{NMd?J2P{I3~C_DyD=1(nO3@SnTkuEDMb3N*&I@ZB{ z$Ic$}s;|s_a>snq1 zOG1~kc@Pk){kx3}22=Pio9+j@yY&~FJdI3DMjG54jz3D7hw;icfIv!mAFL&=@q+}c zHuKA=Mkwcao=V&BaOBjKI>;@hm6e&+vsIVh9y;+5laP>5P*9Y3-+LYRbvbMf;9ho* z&Ce5mQOcGDYb6ZsrMtTu{S`}wc1mj3`qoxgl$?M>I0=7_No7t_S^` zi#XgjH*&v!|8BUuf_dB=cCwj|_%(T6gRIpCfJ?2%B}+K}*-ND?>F)ENAZPrDkC$ls zhVkU-Q{m#t^wI6l4i4lL6n?)y1dNm!_ZkSsJtr4q_P+A~AV%owWcx!Dr3{zT4vsf) z%hJ?t)b%mjgQ%aI3MOF~XATQ-^JAqq-DHB-MGYOu>L4Qy4<4n{3C zl3w(1cXziBbv9qE_(w`gSaY+W=hX?#XLi=EWMbI%b~lL5++H_a@7}%h^Ya@jH59+O zxp^wxb9i)=2K@VFs2I2a$o6!O-wLU<78VwE7n?~z08}m3?T?{Tdnw?-1wG%-1WWhU z0w#EWi3JuY3q)(H*{V>06GlO52Y~G_Q}fMN-PHS`i1_%R`g&e)HLLl$7zVAX61QU$ z)dKa_lkHIuoH0njlb4&o zp-bX*3FC*J4HfCs+ZQV+^Q&xKOiHD4oO=2_US4tycEv^6F|Ei0|1crG$L z91CRL)!giqG!U}TiFu-dLm8TycGfy$RXA4uYE zQ`7V8KzQHh<|9DbBn!|pLN8eQuqy4s-|)2lXc$k$2qTJ)An z7Vs?4P6k!m$dBJ}$u}#v=iFQ_j5}4lEfjhUUBSz362W0r2FBpB`~Dy-+HJv#9lYgf z7mo_Gs<~=E`QXxGt8}av#!X-D%UZ^fl$)-8}Xb}PE%Ss z5@wsir4TkAm}heNYu$*_bY*fT9L1MFy`D&++uCjWEvDxwZd{esayPC0iBl!G`F zo8M$0!)CGRGAyb}R`%rb$}-R2PrZ;)p*C5=9tA=uPN-Ov@yy}ZR`Dml8nwvYxXnan zsQaM-ovM--MGoB)EmKo5zkuVGaKQ&l(>c%OM8!r7=D6t8C~5OEwkQlR+n3fhMPT@v z$e-O0&FR$M(w2{g;H_WZ?jEhH7+h$5t^3gp)+9!1!3BE` zs!JNWjC+~a*KjU~)N#KxzXg@u+gO}rk=<7Hq?@Dz_y*SdrNH-)0eS(${t=P4D$1|L zRehFipIDHI1kDTV7P78kilO+U+&0R7YxaMH%dwkmtMiuhE*5dcsrby=#*LO`pQM{b ziK@m*j7f+ZAAx%pxN1$>x5i`Tv;TD>3bD7?<$@@Up(%Sx)#V$d?7MenoPrN;zqAfO z5Wg;{e`II;zfSsbp>{Nj=!F`2kwM8I#^(16^cC55B>RNelB5QGc)g8MP{4nl0=tsu zDa5zYC(PC*`5j7nT7F_TZk?xjLtg9R~42T^-DE^?%eJJ-~8tM7&_b-q0=hsC!nAMUjAjy zAvAiUIBHh2V(Q2-%)(OUS)rOUHajG^Wogy9Qve@y-)^;zOyq*8wElciHS{4v-|Dc<#POmN{ zb6pYPX*fhFLPB~}<#ce;-l)rO;j|~2*c~NN>mI`oD)Zk=%|?Trqz>lCCMZlAid%;M zIn-+>^kjY}8M^g<|6K2{_MGjxqM#gIGb%Ype*FG~A2O;nGlW7_n`u)*>_Ht8%Z932QJE~Rk6)V^0D`?VP_R?&cy(si* zT2`*%RIKlY|KOr22>e@*lI;%sTDKc6_L*wasXUdb+S+*~XcZ$PUxf$v-F#i-vsc~U zOj9f6Glip>fb08>>r9pSq#tkS!}kYTN|>#5wCP8RLet58|NQxUa=5Il{?b&fpyXq{ za5UAwpYQ$T!1!VV66wAZOtZpzlYo7T+fsGkYrzdQdd^o#nI1uX<<|j&tC7F?oUass zC&#Zsd2PmGfdhQSVYTb|K(U@4<@K|)f{%bYE7);Ve+gko^&;?1)`{Q!V9GqS6K`sN zuGS6Lp{FJNw>h<^z5ERYN!p^VX&rAX=O?*tPW7X6T|e{($ zdkaDLeu9uHCJ_w;qZ8e=5yw$(Gsm-0onYJKfcIWZ7-d<`|F~K9-mtA5V~)@LxX9W# zJ0s#HacE;buL7Ogkx~d=pR>bi-$*82?x}|>SNZ&W{A9)x;NG3J?oNuudQ=P?6L0p= z6iEJUh?T{D(l0epcJw=qfqq>NA+cDR1H*3OLO#B6$O|%!@F`g_;RjHGyO+^#Sh?d1 zi<<}f4LczvPWELV3pr$Ef8iWv%a-2mRZBE_5r5&ozh&CCvv0Oic!yXTNeXH<>P7fA z=O|K_^Z*-^<%vA`NtHjT?vH^~(~g5>50!M3=cFExFW}ZsNj;uHHh0EzXRC`vEl%Mx zxaaPtkeqWsiMYBUmB7mfFY?4NVgZM6vptG89rw&w6gZi}8+M+tmcp}SCNb=n1nO&b zO3k-oYh}g|HUggLR;gI#!x{FkBwjDS@SHD(4}2<-F6AM1x;{nz1qvML2ItV?zy{3DZ;ySJu8hibb4R1aW2-p2tKAj?Z{qdF1QW_TEfR?uf@FY6#LOgDYyYTa1)t9@UkUY#Rvc4eTt_NT$NJu^ z-N_l{FH^aYeYwX{|6D>n6q6me<;B5yvM|wmTf+~%PhLQ#F8Av<*12E3g1jUmqE|L9 zY6vn1(PYDzcM*yeopw1@I;HOV-#b}ze8$zVbWrV^jf}((_mb-2h@x8E+LIaUi4iH( zesV*c17aK=1A8%lV)IOMi5+>i*EI$&C+AG#Ri5biTM>qH_e^cxOoNqU|b74Mt zpVb8N?CxZgLR5TpZ4eG|NpfvlKcoRk!NBG)sXk679W@7vzA>*xR3dy?X) zq2D-J?k(UZa(fG+gJ+D=_oUtwzo0JIZ^(mO?>!-DYQT%)d>4QRGJFVZQ{htE!PaWQ-BX%e85e1FG!{*~s{lP5&i z+f*TAE+*TGibcAQT7Je$fS~_ar!{<5x0LUqS+tD{%&gXo5Q@9lhpV(5Q9E= z-y>G$CzB)g;Q|yd*S2%k7WvmGZ2M>dimq3VqJ@tiQo$hdA5f5jIny{1mXK^Y;vszu zH4_)F_r6ao?F>_BwAT8X3LSW}?$3A6H!dvfYH;tx(|B98UgSzC!d+JCj3gWwTnMYz zS)Q-ARU<-Vw5f&0SabBpUi;i3{!Py&-tdD!`9HuXupfdf{@)_gQ6u>PfB)fpHKvBf zMnKm52FzT+4UFZ>eMa;OU}%4Xf)3QLqcwJhpo;8RZVTwGMV$T55gYCpplJYIeFVrl zM2WW69pwfp`dYhHln>v~mt)j)X%2o4r;D@Nt%#hs^S1?Hb@um%`lI2GGhO zcIwfTVfZj8g&-S)se_>4e}aZ)2&nUoJvC7JkcadA$&iTJ0;GqKkV{jfr|}OL)U<*O z3Ocnne$Qg#o|9sIY0S=!p`#H@xcbQAysPeYdphYsh5^#*py&BKYRmq7eSa?~za8Aq z_mi12kiMb6`qRtQENx;!nd)_AK8;^QhUtBKn6=nozAlMailZ=VOzg3V<^BBuKr*4} zRNF2JeDP>p1y%Wh_VYMYA`YvU5L7IZiqA1KCa{&STFE>a^EE;sfle@rKPIE!xzf{E z8oePYV$f@i){r+fF-aTUHXF-P@NuG3EqI?jdiV#82`9f0@LGY0f~io8v(5!>qk9J^ zb(~kb``#ExRFsslX;;C8s&R}E?WvmKo|wQ9=6GoY%Zwo3-vGwod;uB`=$Pg0ZHeo% zy?8-0EreEgHK@r-Rqf@`+`P*f0rXxLEKoWeHqmYjBApp~OzRt;| zU>($g--&r+DPbJA0l)N(O$XAN2$TFZFvjD3s3I z+Z&gNs367TNa7fZBo8=i>n3Yb_bswhKmjF^avF6-cvu6rHM{5UU$M*U>wLhyD*$w}qpZ+DZ%~@!K(lzQ9143MF zWiR+TDfpV;$=>Y!<)#HnjxjPS=o1}{DU}QDEidZ}P;>L}siJr(G-xdOZG#Ky^lW#j}?UrC?1*)sC($S zwHo|y$?X2wy4qSAa64IYsYQT`I^zGoA+t#wR@$E!8ycnqzCI%@J^i>aBqT(sH;ze7 zlE&%cKtFR5rUGARRI#wgb4$b^Kt=h>HyQI?zBB3 zN|UJ!i1`uNX&$f@Eh}qz*I97Ajzo%*oo+g>M7>?xP3!sD{Y2O+rIjj?ZSBQoJx{IT zlmsMNk3SEAAr~r$$Eu<0F={x!bX}MId2P-?TmapGRDs5Jb~O(1rhDD~iqd!Iknp>U z^g5@@vdZ4Ph@-DpyTP~!r|6xn%Dv|_|8bRP((i!^caurXBOcAlt%;(NYAmjQbP86j z7;?IkU%Y|#8?=`m%>L~J{R*eusnV|7P!fJkq#eM^Y#67cr1T69!iy^1-QDxPVG!oM zm5Rl=u)VoB>=_;&Zm`z9fV#OM+&-_k=}J-*?}+`+d==fcL*1;UBWJ#NxGL*=hOH6N zWZedJ;+rF>Q*SRXU`!=_{kJx9IC82Md37~z<(kJAs|ZsiAXzA+3ea9x6)WWhrX=u$ zU&;OrBkukFiuD2niOZD`rlD=eM^*9cmUy;}r+6TI@XPU^M&ss<#R7ouZ~Eyq>~ARf z*^hfo5ptBa+rb^nEli5?YIbk1;M*874{SnhZwU1gnf=B8U zU8pnc)O=L2_FpYP*l?M#l+8kegs|`fK>ybo5>EoKPDbYA=l4+T`%8s2XBrwB&>}1O z)cOFy>LR#wzy`OciH0!0M3+wCi%){n=T9Q^u}^& zbD4#b&rzggWhvR&aq;ovJYfHV;l&CX$PF@pC@xe;qr7y1{Z-1Ab2tOES)2gyfv!P!;ZW; zOcd)4x-5Ejf+jPfXA3&JuBBD5`FfY2)E79n1oJ^Oyor4o6jsT}b_WN{OfI=9XkVi9 z)j$PY*}fNCU+!d|rn)&Wwl^7$Cnp#RAZn#l8A1NT)A2WVC7b<;oi%o=Pjy_DT996! z^X<%jm@#8x0T>1Z@V1FUttXh6RUWOlNwUS+!zKD`SFpJwa4nXVm9CE;OYDttJI`{J zxX;5!y?!uhFZKO+n*=%xme8{=itqQwmmj#FWq94+RS*d_ja~O48WwK4)Oee=jsKT+ z#gRYnT1r!maW5Vb5mDbBNDClMw17P|RqH^N3~*6}wYa!A=vuadPD>5w)q@syhr2F{ zuMc2Lzxw*VVzcFI%FI~)R?F!!vzj5 zu9~hh;QJYnanQo@fEPwb>r%RJn!Bq++M+o9}Ub+HG4Nd7;_lpS4-QIJW2{aCYbM@ zj-l(npI98rP2X^J&wKT&sX$jJ6OScc<}n&97xa~}q!~i6kPs>efb_l-a)zbwL$N`_ zPfqYw1n3H=WRsRa05S!{@x~rVUGGx`Jp1l#CkkGH9!P;^WiXvu5i>|#fKWDF@B*E7 zdcCG3027y1R=z4eT@|zuTi)0ZQ&(5l;Nw^DFL=eD5QT=frnLd;wYJ|Mo;=0KbS~E2 zvZiN!Z~PyweR%k}nwpyX$(9hHuBRH@SOGWwr>)Ib@b1DFG%@0Kf$!eh?9wg&qfTiDoCdsi&yW1W7{w|zGDQjtMO$1=U1JDWpDg+S` z5y&$_LXf=C;LY~}0F6_V#b@o7BfDl}OW?!yqApzKo*{X$_ z6jW5@j@ya=E+AYN_({h?5yfC`P4RGYl5RyHU>IZp8(pghI*~%f)8&Vkuxneg9{FMx zm;znq7+727j~@f=9UYYcK2QemQWf;@6auhFRS~H?fz?#jrxT#WoI$~RZ3NswV4$7x z{Crdr*Y~$~*YHQ6V5lmr-BcL!77!3HK0Oh^J-XL*C9B@tT}}Vf8D9Nyu$H=d@T$pi z`v(E1O_Ie}PUO+)sS2o7204-IC>lFJPbDXS#Qh_HeRP6?g6u%rP-!(?#w%a~pv%s3 z0I4cyg)4#mM@vB=(s(vwxdXiKvTC-}Fo1x=>Svx#ebv#)i84UXN&uV{fd;&?{e7jZNvkysb@(lpT&qe zYZ7o`l4iNrJLAE)@!uAsZo%P$U|;k&>IpyYhpFhBc%tdc0G51gcdUEH_%T`DYngd| zDWEcXcKKg@*M~)6v+u2+-h*ag)idFb;s4bj{m-g#)KR{((^S3wA(>?V5AWuz0{SvV zMf!;pQA<`KgS7RT@{?=bF!HptQ7ieu6i#JuqHTsQ2VQ| zch!62p-Px=L*r(d^B#9d1(hGW8AlF2Bj2NzzoGaA+Ck4c9M-xp#J;Obd_M5NByB=^ zf4aly;x;z_R#ZHS1V5nLjKY4p3~B?P)N_DuHW+rQ>^s@JDJoJ94?m%PbiA2bvpEA0 zJ(px_sUc@~S66LzmA$?6?kqlX%gtpcyq1HkKr~7yIo^EjU|AhvvmjmFMdd`+({s4W z>9!IiXf}Uk8q3IUh}o=JsqK2b7j`~(mn$05Cn#R1=_F?zFC9Ez?_kTC_~S>%LgTr! z-VrX{fC0<;U4wqxCDa1#(`eQl)`nPmkP~dbu#rKFF)}`$@Jy>(w{8>bt+09sr7sWP z4d3>*w|9bW9otCo_+y2d1`@{*Ji)_WCaTZQRqOqnyz-58tdMe(Q<37y`D3pE`b%iw z6-fTm=H{6;ma|p86ck1Y-g*reef;B9M%|0yf{xU&`D#-4{8#a;Pm=f(UA3&U8B~Gb zDwl}wrGwnw6McpR^c~R<`+!FAP>Tn1*MzE%rLIh|W~QfOCv`0cYaL#g&5Q-WCY8)5 z`U0MlKY+XGNo)>0cUXeR0xiS-bkuGI+d!d?)(!~PJ@>j#(RfvMQcUda@d!C?ZpWj$ zGt}!UPFn8=&oA>-6fOly;{1kl)SLLuk?*=9g}f`hZAm5lO7Qw0IhkZdj_0Qj!<;}t z=3+5!zuXl`$a2F_u-_h3^MHRVSBckt`48*OdGq=5zRe&i>Dog6WwHy8Mh2%REj@bl zo6qf!2?UQGLrn3Q7*(_=M;Di4Hb*kGc4u80mG^G%phiCMNcday`&VPtHpZo1x0i~Q zm2StP28N?%lSMqmjT0mn^~kS9MAK`3=~nL(Nl3)cxugnKTGTRIsoNBbfObnI22oAl z4RJ;5FVIrd94gl1=i}S;nOoS-RXSv|wTWL~yCLrJ`Td)XfCIfT6hk3jH8MFtbET@v zrm?Tm@)4=p%=7#|!fu^mbeRNq0uGd|d`N>VmFohGY;1uOg|}u?L%v&E6qqF68C0Oc z>QNhCug*Bt_wSL98SwvTE_jra6Z1~A{1poy&binvzjcIFMVv2$w3sP3+&39RNB>#n z;5D$yg$wLkdN>vmzxx`dcd?e*%2}{G7K5%wR(soGcejRrN~FTfGCa*ftF~;dZBZw-udd2=?q*tosi#xR=LrWEszT?iujYJ|G-57Ni$&? zJ{!9NY5Cp zt=-BS#lJtMAS3e)49xfQyBPlEgYF#?ETIGd?>F?vpEGsp^=jZvi)JH6Bq+X&i|%9v z>up#rKm?drS~^_*sr9}48G4J6ViIqhNVy5P>b=7h@8DkBB4`(d%rDHl*Me%t`+^tT z`oY1mXc5!)!TJ2cWWK5>?)3^)_28MTbRPxt0V?DR>K zgP$SQs>$|Tk3qLb7zFM;1S6meJKLj&s`(1aI+Cr;_l^F!O4XoY4e+qfccND!=le(- z)>(3JtI~y&ZPAdY=+Mn>!aD(-zGd4eiBhZSWZ&bt+7&GCVoh98ldQwA*=P!M_!-$7 zZf;l@DZ0)1W@=nuXg~kpjo|%se}Cfk`~40%)uQjTcGkjXJ|I^Ga~d?%Wox)CzIKBH@IpS%4-ub>b_#1nn}d+x8;U>g=E$}j8L z9X9h7Pq|8VvnBl$*hsTC|L!h21QFaie>;;^h_MPKyYxtznLW#v4PEW$bYN=y`SWLM zu9Dn4V@X0Q>(edA*zMBC3Pfr}8J`zDn-3AWskhhX;NbZQOl`73fFgqcKs=-Iyx({* znMKCi4VfQl>7XF@Em$)``~_%y2qE;^;8A6F2J=ftbb_%jtDT(*Oc2HTDncsR?}#`J zAi2`+d8{ld3CWqqp(xYY9+XH;jTe$7yVsS%A3j`ah(SbT70j-k9An(Ru+ZXpe(A8( z@o7Ub>$bVZ3kqMnc4WMB#Zo(J`Sa zCmWWlzW3z!BObt>wJ2NSKZuBp4ULK_ygb*eY}(iv$6?fQNAdQad;s&OmI5yK&dUP` zRm_1ewguy2#hX5lV^@;J)Tp*WI>{sJY!Vrp<6FbOY@3~=*ZAt*oMP#3s5<=`J#DZm9X20{h-j~OMZN>V%Gr8Zxxv=q z;SJe-9L?E*WVP)PV0n$f;HeI1mwlA(Tg%P<^NP=v8$1Cz@l0S~pu#%d2m~~D zi1_&J4o*a}2k$wY4h~vcN6V+kFkHOh(QA#y%v*hAI?*fN9PQ5b5Ox`Un#_3Lq*ZZ{ z>1@pzMpWAxMywWGDF|FgN$6HiDXT&>+n3t`vxkC3VFLgJkK0rI2gu%^78=rPYNrp| zux{0>tODI!)s*Q`e8ced`iNz{FV`82jOX33lb&g2Z2z*E8B5$uL0g_Er2mF~ncUR{ z2pbC8-(zD|O;YN@|>)XwjIHm%BLyWh4yKk0gN zDELvTx5`;UI65%Pm*CSx0f{4QV-SRg3hQgM(X2h{;SL->YH5&ad*j4eO!_o$Zkso1 zH#zJ#q#qP&UY6;9pr%v9?B^ucRMwW2t)kapc}YqN=mZ`a*hDi>NF5raCNlU{;@*c) z(3O_6mVn_hBd@bhx1wOF$s3rhZndUi!BkH#a3VHcPD=Yp7wT zjs3p%kIM(7Jj8ql@A-8-N-=;z-?4sE+$R%4@2annv)dr)g%LS;C+ zWg52=ZHiL%8q`vOCnW{5!d5St>;nOd>*o&uCX_l$qP8m zV7qKC>xWlYlVcFNca=Ef0S)%E+!(O{SgsPKTWol+gaWee%CI=$3)0lq zgJrtBIg$5>F88y9jipa*;erD16FIzq);cQHTR?yBM^DVZ@s9rTYR-e@fZA%0{`zzS z6*7ciDNPtufs9Ba*q`TXdT0OSl>l{Zx>;Cfh|uNRoVMI zZHxsQyT)l7d-80T%>L4T#K6FeTmM0Fwv3@fvlo}E`^c#;R)J2|vp-L1mF2TLJM63$ z_!w;#`o@!ayQL+|z$2?i1IBV}Z!};cit_h&F+AsOVNEM~a!%_XuNH-s6>#6=IDlI_ z+ejq3+#s}PVMT~b`a470=%^o~%E^KFD3o3994{Q50M>HA%L}Mb7;P5^5WE#=;(&%C ztNS2{M*@4fbI|%5xOG8vnGKn+S>T2*&*h&-s_2A(ITc4V8xeYxnNULQ`BGmP^elpe zRL)s4xUv@~ZS1>-h7kot#B+Rc(8z_JO*e!ogL?Yc z`!>X{>m$i@UCfr?-D{wz%U!5q@Wo?D1LCr&`g*N;5i;5&&>x57D0TMt#Ne!LZurY9E0m76ZJ+I%Rv$j#LXY|kEjp8tgsF%dgh2+h0{3@Ph zR#?v(LjcQfye|2)tekbIs*p53UhHhY(Pq!yZ|Gsamo`5$l!Ienpu%J0m6!Q^0*~j_ zki$d)3n3;>8tqiwDU0aIsW*3{%Dn~R$jeYwR2ERn29f65#c%C zU8@(x%_-2mgYKwVvonz((-iY=anik&>P1=5Y%DaNl*PQ6Fj1tOAk`aeAU;-yIx^72 zi^?rwoS+#w1`L1SV~K?nf3YtpI~p;P&+hp9i@<3O82S@jQic2UD<7MEql7 zjMw5#Ii5YYi}@Sch^QMT7;`^@2;Xq$j+!Mi+ZyUH`|$-<}@r@swC9_Nv?AM>Z0I(81b zpfB)mo*mp)!Q)Bar4DjMN&SiSUt0Qa4h0SK5@+rX z6U%(lvt3=jJ69!>fw|6}7}M!W7(u-=q933N@}}8DUt)HuO?QnQ!)LqF-K~!%vXof2 ziyy4G8~wkH6O`T5uCo=7H?;4u6--13Qr@-(czbm5(k;;lt9nf z!$=ytLzrw<(!-rgKQDvgufV$0v$1YXg(GF|qjm9&m4`XGQv)ozjv-mLa|}u8@bk%% zzdzH#1y=ZIg^3b@nypo-d;S9%l**i&1t`;3^HJwtqphpqoa^gxv%`5YbB@9|{Q$FP z%d&5eB!rTV_rmTnDpFc`(ChSkCKKnEzg<4Rv=0T;fuUZ^taCJh=#Whvpxc$uQ?o#N9 zIa#nowl4|)gU48;t$p$Q%<(vKg2V%W{etJ}Wa1Pvy5VNxunL>1H%wkHF5hQr^qUaX zxPH0cyGs?FE!w5X5v^s3$6;!$c$E2RAZY<0?kVBuF-4f}L;nin-u1Um_+SNiJ#InG7i`Ip##e5Ij z@?~gnpR{2lEanfNkbHD9sJ_M0|8#W3c9K{ID;{)`ZuY^-%Vms=ac|*{^%Vtd6C_$8 zg{@W6rp7Qw9Y9!8C>=>L)?zTu%8`Z%-1ngn8c^~eZ$i8 zNnMQdxV!YSw?FdknknBTAm+INgy_B9vT#`pZNUu-Yv@?+F-9oieMpks0~kL5Y-015QtUo z9Q#jNines{%g*wz0|3X_j@?OwfkcKPau{i~w=G zJ&4QwT(=!m-jqB%Pa1VQFAkSCj`d-aalF4(D0qk|-WszQ_n2(-^9FAh7kHh|C)4YZ z1a)T&!JJff3@Fz7{}EPPP>x6++GnqnOA1U^D`u{;s(tvS9(uUXor0ebSsKaa z4uiXqGo88xy>D)T7P%ZYb=+VdqBV=$e9cd%<8dUawSSo2OE_1OV^JU_?0fq{8}b*i4*{CBiVE6cVI1f$Qgi$qvh}7m779T z(Mi4Fs1FppZ0^r_+)pSw!#4*wbn8yOUs{F%0_yPCp-j?K#i#XGFXwXyz}bEhaAO%D z8u`3=t_orpnlsa94|Q>2w4D{}8K097?=gB~ zud%<|(xPu4Iu-o4yE_(@v_Nm|Dv~^tQ|I}7ZuUfBq9D6Pmr!-V^wgHy*6(kkMa{EN z%lExVkfb1P-+bSEH#cP~oCs(&y_AJAgG-LUl~{$FhN3$*O*{?Tf%W?+0vY-q-f zJa!h_V`FNLaYJiaIgdEAA854HvcFn1MefrSMEjCmCty76slt)))PkDphM{c%ckv6- zDcY+$)rtu5&MXLo2o>>O09!rZIw#}5E~0BYnimJvy2VlX{W0mfjTWmgt*+mu-Wqf)DlE!5&fn5!DjH^tIku#C zO+e`Z9_N85hIcPTS#V*AcQb-j)fnw~I<73k!QuW5-CX|DWg8Ygyzx}H7(WNDl?t9n zK==CHfy*E#2ls@%KiK>Bv&YV7lr;Q7?~eceieB0Cv0dF;vHtg1Xgfeic@Kzq&{@Y_ zR4p``s{eYu`8fx%h`y+t^q;*gtWKcD9cjl>2cR@b58kwASw0Lpq2`j&t?yzr-G8i)Y=Z1ux&2qdE z`tV>dBo})PFSfkX`PN7mFndq@K{&6wq#Ac>YU>r>1-v*`(t)z0d_L89qD$jt%&^B{ zWUBLxQ7NxB!+dk}$*v;=Q=9L7n+3-7#faF=+ztJRmvMIYFAgxQPzW@PM4ldC-G0>E zetOfk5YzTc2&1b$&o))SsZdi&#ray^#k|?;=ZNW3DJsT}4uSJFRc#9**2%$&kDm9s zH@3%vo(X6An=szoO{Kv%)@qLu&@H}Dri&rfHd-ohqmz;Zw*KmzoKygJ{=~%vO2Bp? z0_244FJuaJWMjs&<#YgHT2nU@V>Wf2`t2L~`WR}qnN~JK1mQ$%M0|3PknPgwkld40 zqOfAiZOejSHt6_G1itRC?yX^<)YhoS(I+Dz!K9!R2v1Hnx!)C`N#Z%h>F$2z>dK{F zA5Gf}5RUL4H1(Af(MmpxQkNawmC=<$`?9`6P7_u1>AzOBSL!t8SAjHSI+ryyQyTRT z_4VEPu}26#UmM9tl_-Bio|>N0HzkMPj*RRMRU=+)fzYuFKbHA_$tfV@ut4e`A0H29 z{CJ#pjDj|3J&08#z;Gf$A9OzNLaM8)dvSRQ=vZ;YoH9_G6zb?Af#J4xox-AR`hCX1CQBiePp^8H;!V)aZz^FNw=M|gDK$3Z>1Iibm zwOj>yXP>yZxM?8F#s8oXU4Mtg&dW>q<|`Nj=BkU<%rz&4?D}72ja!rgO~b|Ywc++i z=D1hi5m0=r0-?l99!F}RXOeEU4%yl=3w+GN%9>AHZ9U78B;ZK^#u=UYF%9IEFkT5> z?@X1Z`_hq#8<6HCilqwytp%8}{k+uTL)&R=WYhwtXTe-+8<5^g_gX#2#{MecdG(r= z^#zLW?;gAD?QNiKQ`H+%IDI*$OrFf+^Zk$g<-Y! z>rXkXroMoea$o}u1mMX5NoailUNB$?zUP=91Y)PpJ7Y9fi%s)8S6{zAD9~#r0fIfV zxf;7r(!u$>0pBYiY52)v{B)+uIs^!g48VP=2uuSBrHG{DQ(%4!Qc_aHYJelST=tVX zrpn4#GP1JLz}zYjF+cb4^n8wo_YJtr+WPuB85#iWNlypv4C*c6$)JiDv-Z%dR|W;Ty`rDzhM#wgGEZysdo+p1LDAS8TQ*2 zbW5tSzFh4+GKKkGMW?2QgLk4VgYoZwt6E`h=rrejcT5@`9sQ~A=Q{`l3P~6 z2hS4^C&366^F29n%!jEJYWk0iD1tj!*zXjAh!|CkDN0BLK_Y|*;(v6!@nPa))q)|q|(JgGXQEsXm-j=!K*y{sDs~t zLA%K6MK7(pn@vHf`@7qYjt)`q!VA6p|D&5T4~O#o_xNKQSu*)nh%Aj(`##x1h<0m= zL6&S;5<|A3CdJ5FC{k0&8c7&SLuHNZ`#LeoJ|t9=_S2Q0GW7kB3@IHUWE9x zJUBA!;U98n#VrG+iUh3jv|6NdmC~I&erM|K$IwHRftoxNl8rHhrqYCCyKI~ z_}K?Y!mnR9V!S55eIwbuer+iln6@xXiFtll$*n`8B48oSy~6HwDo`r85kNCUx>xv4 z&CkwCwWP=@5BEVTk*OB_(|h=t1CY^zWlYLB%F;rt83^8Ul5&*e0+8l&q|}Kn(y|g2g3s+x$5) zO5)_nlP+{8C#SP>ur#h%6IN#}xp;YZA=g25`F6OcL~wqAEwK^;W`Q`QfWlkqfcPr~ zq>mS>;Jhi03)ur0j`~Vi_*}>(YH(@q@R)E9pl2w|;|x$$??9G8uS|+k$XT$W=oK6$ zJ=VZCdyeK==Cen0)!eGm<0=D>MNNfDR!=~n^rd;tMTZ|DT0XPp*i`|zMnr^ajIs@DSHf~ag!Hdo& zC?~BAgT;Pj4c7KiQD8W?K$<|u?={rcsyPkohZ}(-qE{9c76X>&y?TvIroMeki?xS0 zK@tFZWbHWzQrF#x0Lz78yP{IG!EBk}<5ILotxyldh)WBIR9#mM3sl2@x7f2scn-Vl z2?kMh9+J@1WSmc-s^+W)Q%l@BkHb>Ds>X;EwA*253j6n+n2+Sbn?`dh%CjIqtOcLG z=c9AkY$m@4(`6yBo&iDuYG`*cAO;*kv%V$SgUBR;W_#l4=DKULl~!Ji#$!u8J(evw z^2%&456I(6E-sFb--Jv(-u3ddT9`NI)^bN8z$ug4tVnt;AtS>J3jnm1I1+PkL${zF(7aC0w z^1-<-(rOoipH=@sipF^6i8Sra^&i{#_!^*DdK136A=L<$2Y^;_UJDFtg!GpPU!d2V z)@^~0u)F5(+OXGRe{1V@c*0+6!#-PDVnjD6NFDTvOTa={`W#`M(_L5+P&m1;{)-+D z$}WncbJGs+Ai-dX8yXr4&|$fP6eAmm6ZBfNj*9Kz%*#}};-d%12k|3E?v01c@g%43 z>4*9=kmZG9XGbD>iSe&|@%Z|x#cH0wz`*%2YSjt(IM10FXu+P7$?vmblt$)(a`OK{LTG{NES3EJKGz+m=dRX%y$Qo|V%{7jCCl!wU|p+8qtR5*;i3jzuFLk+x?LEY?8 zy5ZSVr%xv)Bt!t0DDCeSIs=Iyk+{?4`O_Xg+=gTk`E>rSm_zA(lw#i6<8C5Na{Ms> zp+X1s?1?RvC#ZK`KukfEtOMmO8yby{`L2<{2lTPy4i5YH#I&NYw9uUZX?dsKjHlJGB75hVq)~cOa)?U*M7DCdd-k$Sz*WkOe))HV95w6Tt4Js-1GK!InJ0HbQtYX(t-Px4`DDr`{EtYAynP&$ z&Apldygv+7Oo7-VK!tX2H>LKFc>%RKQ1;L;bjRcqnpZGCP)mJ<` zJTRDiP<|RqUTf;a1(2&b&1W>{E+UfiPx7$$weE>8D<>TWMvue3evM|GA zXnJk)?@vj2c{C8r@`_Vz@QY)jSNmSwOivd9nAI)NqdInFo>XfWI(iD9o!zTy6Y{Jq z4C$#BWRx8%>b=Fm^JR9H1pVe008O~e71~irfc_!nJqWrkh|vV-PXLUjo8Ox@%78$0nYt9S4QN)0_wN%y zk?Yt&*2}_!hf5!JB1Isuj>%xc*w_Pftrkc{rTuowHm+Vn+E{G=icbi{ICy$^K%)%k zoN?&yUFM+nzaps3E-s=W91vXqxfOX1D&Z>q!B%yqNNBhN*iPh5w`+_M^|wC~0qXgo&zL3v--*w_LZ`m=Oi6cM!Om*5Tu0KEovsJ^?~9Qf^rj^Pkkim?dW(D(HdV;U)C45DJow@#2)qzd&|tvhkrF09!~o zKzO2H!T|IY9TRgOHozCDu^%ocxIPIwk*4B~*|%?>lIMT|Fc}L5EAq?M>RX{kACfeR zdjOrjJ1nEyk&&OkR3sxuGVSH7%*io^yBTJ8f7%k9e_bpov=Hn8UQaU6<)EGG0x-{fj(WH4aJ)fzD^g0q)`6(N3zfZbpBrbrF3qEga3IttOHPqRibP(YG03JukQk-t4M zg4@D1ZsX$m;1sX@ZMrMU_^VJ4yOmYH6fhI z8B9}KA@fi1r=a-(U*RiPl4%|k{M_bV-1gqcVkI`%E^b4PUZ2FAI@K(S<5$ed)f3{q z)tVlTo>ILUr(PtSCymvKS66p6v9P$%>UJGvL)jorOf+AUlP!2(=2bzd;ONDoR8^yF ztJ=mXG*UWem?&_52J2)IUwz+O)lp0_KvqT*(o!i^?gc@f@ zwI*M+vgZ{M;6RLrq&B z{bK}QL#S1&@wAqFeiZL?L{}I0xp2+gh2isH`VuMsIo7w0dzoeF&ySXjN^R)6x;hJ#zo(~bc{x00Cwv2W?VYivHnBqSt6HrWH2K|@)=g`h`{uqFuprEaSX0*O zi0BLF!hcNrG&;ZynQOz%?u$>f)9Fj&G1DCmM;J9aJOwr(X>l9X0kLpt-O+`D!@B*2 ztsOO+cR}f|?K!lLNewp@xx=yrTFj8o4-4aD?$0OOHxDYI zeXdU)w!nI3X(n5;;~7z~(%=2g`npIKzCrY3zx~sj+1crA`TIj&W*cF!Kc&RNwcdMH zR8>iDF#D^Gji=*?obvF+^IP1Jg!z=mBO-cw$ApyjZ_~&~A58V-73t#&Uw7hkc73Yr z>}2Dyf36TQEh@^mUa04PzJwI@8MQ=u z!Lx4)znUjzYB~qn(%$gbB~j#}qFoTl@2I09IU0FB{e?58cHR-GshT+3-A1YUc*p~L z>+8S5ATKSM^ry3ef=TruNe^~j1<@zag_3Xs^ zena2BqljcOIa5p;V^kho+S7T!L{wU?kk?aHN> + `+ (jsp' - jsp)·(ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative)` ## Terminal Constraints diff --git a/specification/src/operational-stack-table.md b/specification/src/operational-stack-table.md index dbee0e07c..07f202257 100644 --- a/specification/src/operational-stack-table.md +++ b/specification/src/operational-stack-table.md @@ -8,19 +8,18 @@ It is initially empty. ## Base Columns -The Operational Stack Table consists of 5 columns: +The Operational Stack Table consists of 4 columns: 1. the cycle counter `clk` -1. the inverse-or-zero of the difference between two consecutive `clk` values minus one, `clk_di`, 1. the shrink stack indicator `shrink_stack` 1. the operational stack value `osv`, and 1. the operational stack pointer `osp`. -| Clock | Inverse of Clock Difference Minus One | Shrink Stack Indicator | Op Stack Pointer | Op Stack Value | -|:------|:--------------------------------------|:-----------------------|:-----------------|:---------------| -| - | - | - | - | - | +| Clock | Shrink Stack Indicator | Op Stack Pointer | Op Stack Value | +|:------|:-----------------------|:-----------------|:---------------| +| - | - | - | - | Columns `clk`, `shrink_stack`, `osp`, and `osv` correspond to columns `clk`, `ib1`, `osp`, and `osv` in the [Processor Table](processor-table.md), respectively. -A Permutation Argument with the Processor Table establishes that, selecting the columns with these labels, the two tables' sets of rows are identical. +A [Permutation Argument](permutation-argument.md) with the Processor Table establishes that, selecting the columns with these labels, the two tables' sets of rows are identical. In order to guarantee [memory consistency](memory-consistency.md), the rows of the operational stack table are sorted by operational stack pointer `osp` first, cycle count `clk` second. The mechanics are best illustrated by an example. @@ -64,41 +63,41 @@ Execution trace: Operational Stack Table: -| `clk` | `clk_di` | `shrink_stack` | (comment) | `osp` | `osv` | -|------:|-----------------------:|---------------:|:----------|------:|------:| -| 0 | (23 - 0 - 1)${}^{-1}$ | 0 | (`push`) | 4 | 0 | -| 23 | (1 - 23 - 1)${}^{-1}$ | 1 | (`pop`) | 4 | 0 | -| 1 | (22 - 1 - 1)${}^{-1}$ | 0 | (`push`) | 5 | 0 | -| 22 | (2 - 22 - 1)${}^{-1}$ | 1 | (`pop`) | 5 | 0 | -| 2 | (21 - 2 - 1)${}^{-1}$ | 0 | (`push`) | 6 | 0 | -| 21 | (3 - 21 - 1)${}^{-1}$ | 1 | (`pop`) | 6 | 0 | -| 3 | (12 - 3 - 1)${}^{-1}$ | 0 | (`push`) | 7 | 0 | -| 12 | (20 - 12 - 1)${}^{-1}$ | 0 | (`push`) | 7 | 0 | -| 20 | (4 - 20 - 1)${}^{-1}$ | 1 | (`pop`) | 7 | 0 | -| 4 | (11 - 4 - 1)${}^{-1}$ | 0 | (`push`) | 8 | 0 | -| 11 | (13 - 11 - 1)${}^{-1}$ | 1 | (`pop`) | 8 | 0 | -| 13 | (14 - 13 - 1)${}^{-1}$ | 0 | (`swap`) | 8 | 0 | -| 14 | (19 - 14 - 1)${}^{-1}$ | 0 | (`push`) | 8 | 0 | -| 19 | (5 - 19 - 1)${}^{-1}$ | 1 | (`pop`) | 8 | 0 | -| 5 | (10 - 5 - 1)${}^{-1}$ | 0 | (`push`) | 9 | 42 | -| 10 | (15 - 10 - 1)${}^{-1}$ | 1 | (`pop`) | 9 | 99 | -| 15 | (16 - 15 - 1)${}^{-1}$ | 0 | (`swap`) | 9 | 77 | -| 16 | (18 - 16 - 1)${}^{-1}$ | 0 | (`push`) | 9 | 77 | -| 18 | (6 - 18 - 1)${}^{-1}$ | 1 | (`pop`) | 9 | 77 | -| 6 | (9 - 6 - 1)${}^{-1}$ | 0 | (`push`) | 10 | 43 | -| 9 | (17 - 9 - 1)${}^{-1}$ | 1 | (`pop`) | 10 | 43 | -| 17 | (7 - 17 - 1)${}^{-1}$ | 1 | (`pop`) | 10 | 78 | -| 7 | (8 - 7 - 1)${}^{-1}$ | 0 | (`nop`) | 11 | 44 | -| 8 | 0 | 1 | (`pop`) | 11 | 44 | +| `clk` | `shrink_stack` | (comment) | `osp` | `osv` | +|------:|---------------:|:----------|------:|------:| +| 0 | 0 | (`push`) | 4 | 0 | +| 23 | 1 | (`pop`) | 4 | 0 | +| 1 | 0 | (`push`) | 5 | 0 | +| 22 | 1 | (`pop`) | 5 | 0 | +| 2 | 0 | (`push`) | 6 | 0 | +| 21 | 1 | (`pop`) | 6 | 0 | +| 3 | 0 | (`push`) | 7 | 0 | +| 12 | 0 | (`push`) | 7 | 0 | +| 20 | 1 | (`pop`) | 7 | 0 | +| 4 | 0 | (`push`) | 8 | 0 | +| 11 | 1 | (`pop`) | 8 | 0 | +| 13 | 0 | (`swap`) | 8 | 0 | +| 14 | 0 | (`push`) | 8 | 0 | +| 19 | 1 | (`pop`) | 8 | 0 | +| 5 | 0 | (`push`) | 9 | 42 | +| 10 | 1 | (`pop`) | 9 | 99 | +| 15 | 0 | (`swap`) | 9 | 77 | +| 16 | 0 | (`push`) | 9 | 77 | +| 18 | 1 | (`pop`) | 9 | 77 | +| 6 | 0 | (`push`) | 10 | 43 | +| 9 | 1 | (`pop`) | 10 | 43 | +| 17 | 1 | (`pop`) | 10 | 78 | +| 7 | 0 | (`nop`) | 11 | 44 | +| 8 | 1 | (`pop`) | 11 | 44 | ## Extension Columns -The Op Stack Table has 2 extension columns, `rppa` and `rpcjd`. +The Op Stack Table has 2 extension columns, `rppa` and `ClockJumpDifferenceLookupClientLogDerivative`. 1. A Permutation Argument establishes that the rows of the Op Stack Table correspond to the rows of the [Processor Table](processor-table.md). The running product for this argument is contained in the `rppa` column. -1. In order to achieve [memory consistency](memory-consistency.md), a [multi-table Permutation Argument](memory-consistency.md#memory-like-tables) shows that all clock jump differences greater than one, from all memory-like tables (i.e., including the [RAM Table](random-access-memory-table.md) and the [JumpStack Table](jump-stack-table.md)), are contained in the `cjd` column of the [Processor Table](processor-table.md). - The running product for this argument is contained in the `rpcjd` column. +1. In order to achieve [memory consistency](memory-consistency.md), a [Lookup Argument](lookup-argument.md) shows that all clock jump differences are contained in the `clk` column of the [Processor Table](processor-table.md). + The logarithmic derivative for this argument is contained in the `ClockJumpDifferenceLookupClientLogDerivative` column. ## Padding @@ -116,11 +115,8 @@ Memory-consistency follows from two more primitive properties: Since the memory pointer for the Op Stack table, `osp` can change by at most one per cycle, it is possible to enforce a full sorting using AIR constraints. 2. Correct inner-sorting within contiguous regions. Specifically, the rows within each contiguous region of constant memory pointer should be sorted for clock cycle. - This property is established by the clock jump difference lookup argument. - In a nutshell, every difference of consecutive clock cycles that - a) occurs within one contiguous block of constant memory pointer, and - b) is greater than 1, is shown itself to be a valid clock cycle through a separate cross-table argument. - The construction is described in more details in [Memory Consistency](memory-consistency.md#memory-like-tables). + This property is established by the clock jump difference [Lookup Argument](lookup-argument.md). + In a nutshell, every difference of consecutive clock cycles that occurs within one contiguous block of constant memory pointer is shown itself to be a valid clock cycle through a separate cross-table argument. # Arithmetic Intermediate Representation @@ -134,7 +130,7 @@ Both types of challenges are X-field elements, _i.e._, elements of $\mathbb{F}_{ 1. `osv` is 0. 1. `osp` is the number of available stack registers, _i.e._, 16. 1. The running product for the permutation argument with the Processor Table `rppa` starts off having accumulated the first row with respect to challenges 🍋, 🍊, 🍉, and 🫒 and indeterminate 🪤. -1. The running product of clock jump differences `rpcjd` starts off with 1. +1. The logarithmic derivative for the clock jump difference lookup `ClockJumpDifferenceLookupClientLogDerivative` is 0. ### Initial Constraints as Polynomials @@ -142,7 +138,7 @@ Both types of challenges are X-field elements, _i.e._, elements of $\mathbb{F}_{ 1. `osv` 1. `osp - 16` 1. `rppa - (🪤 - 🍋·clk - 🍊·ib1 - 🍉·osp - 🫒osv)` -1. `rpcjd - 1` +1. `ClockJumpDifferenceLookupClientLogDerivative` ## Consistency Constraints @@ -154,32 +150,26 @@ None. - the `osp` increases by 1, *or* - the `osp` does not change AND the `osv` does not change, *or* - the `osp` does not change AND the shrink stack indicator `shrink_stack` is 1. -1. The clock jump difference inverse column `clk_di` is the inverse of the clock jump difference minus one if a) the clock jump difference is greater than 1, and b) the op stack pointer remains the same. 1. The running product for the permutation argument with the Processor Table `rppa` absorbs the next row with respect to challenges 🍋, 🍊, 🍉, and 🫒 and indeterminate 🪤. -1. The running product for clock jump differences `rpcjd` accumulates a factor `(clk' - clk)` (relative to indeterminate `🚿`) if - a) the clock jump difference is greater than 1, and if - b) the op stack pointer does not change; - and remains the same otherwise. +1. If the op stack pointer `osp` does not change, then the logarithmic derivative for the clock jump difference lookup `ClockJumpDifferenceLookupClientLogDerivative` accumulates a factor `(clk' - clk)` relative to indeterminate 🪞. + Otherwise, it remains the same. Written as Disjunctive Normal Form, the same constraints can be expressed as: 1. - the `osp` increases by 1 or the `osp` does not change - the `osp` increases by 1 or the `osv` does not change or the shrink stack indicator `shrink_stack` is 1 -1. `osp' - osp = 1` or `clk_di` is the multiplicative inverse of `(clk' - clk - 1)` or `0` if that inverse does not exist. 1. `rppa' = rppa·(🪤 - 🍋·clk' - 🍊·ib1' - 🍉·osp' - 🫒osv')` -1. `rpcjd' = rpcjd` and `(clk' - clk - 1) = 0`; - or `rpcjd' = rpcjd` and `osp' ≠ osp`; - or `rpcjd' = rpcjd·(🚿 - clk' + clk)` and `(clk' - clk - 1)·clk_di = 1` and `osp' = osp`. +1. - the `osp` changes or the logarithmic derivative accumulates a summand, and + - the `osp` does not change or the logarithmic derivative does not change. ### Transition Constraints as Polynomials 1. `(osp' - (osp + 1))·(osp' - osp)` 1. `(osp' - (osp + 1))·(osv' - osv)·(1 - shrink_stack)` -1. `clk_di·(osp' - osp - 1)·(1 - clk_di·(clk' - clk - one))` -1. `(clk' - clk - one)·(osp' - osp - 1)·(1 - clk_di·(clk' - clk - one))` 1. `rppa' - rppa·(🪤 - 🍋·clk' - 🍊·ib1' - 🍉·osp' - 🫒osv')` -1. `(clk' - clk - 1)·(rpcjd' - rpcjd) + (osp' - osp - 1)·(rpcjd' - rpcjd) + (1 - (clk' - clk - 1)·clk_di)·(osp' - osp)·(rpcjd' - rpcjd·(🚿 - clk' + clk))` +1. `(osp' - (osp + 1))·((ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative) · (🪞 - clk' + clk) - 1)`
+ `+ (osp' - osp)·(ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative)` ## Terminal Constraints diff --git a/specification/src/processor-table.md b/specification/src/processor-table.md index b50c438c1..cef75e856 100644 --- a/specification/src/processor-table.md +++ b/specification/src/processor-table.md @@ -7,7 +7,7 @@ Each register is assigned a column in the processor table. ## Extension Colums -The Processor Table has 15 extension columns, corresponding to Evaluation Arguments and Permutation Arguments. +The Processor Table has 13 extension columns, corresponding to Evaluation Arguments and Permutation Arguments. Namely: 1. `RunningEvaluationStandardInput` for the Evaluation Argument with the input symbols. 1. `RunningEvaluationStandardOutput` for the Evaluation Argument with the output symbols. @@ -19,32 +19,25 @@ Namely: 1. `RunningEvaluationHashDigest` for the Evaluation Argument with the [Hash Table](hash-table.md) for copying the hash digest from the hash coprocessor to the processor. 1. `RunningEvaluationSponge` for the Evaluation Argument with the [Hash Table](hash-table.md) for copying the 10 next to-be-absorbed elements from the processor to the hash coprocessor or the 10 next squeezed elements from the hash coprocessor to the processor, depending on the instruction. 1. `RunningProductU32Table` for the Permutation Argument with the [U32 Table](u32-table.md). -1. `RunningProductAllClockJumpDifferences` for the [Multi-Table Set Equality argument](memory-consistency.md#clock-jump-differences-with-multiplicities-in-the-processor-table) with the [RAM Table](random-access-memory-table.md), the [JumpStack Table](jump-stack-table.md), and the [OpStack Table](operational-stack-table.md). +1. `ClockJumpDifferenceLookupServerLogDerivativeOpStack` for the [Lookup Argument](lookup-argument.md) of clock jump differences with the [OpStack Table](operational-stack-table.md). +1. `ClockJumpDifferenceLookupServerLogDerivativeRam` for the [Lookup Argument](lookup-argument.md) of clock jump differences with the [RAM Table](random-access-memory-table.md). +1. `ClockJumpDifferenceLookupServerLogDerivativeJumpStack` for the [Lookup Argument](lookup-argument.md) of clock jump differences with the [JumpStack Table](jump-stack-table.md). -Lastly, extension columns `RunningEvaluationSelectedClockCycles` and `RunningEvaluationUniqueClockJumpDifferences` help achieving [memory consistency](memory-consistency.md#unique-clock-jump-differences-in-the-processor-table). ## Padding A padding row is a copy of the Processor Table's last row with the following modifications: -1. column `clk` is increased by 1, and -1. column `IsPadding` is set to 1. - -## Memory Consistency: Inner Sorting Argument - -In order to satisfy [Memory-Consistency](memory-consistency.md), the rows of memory-like tables (*i.e.*, [RAM Table](random-access-memory-table.md), [JumpStack Table](jump-stack-table.md), [OpStack Table](operational-stack-table.md)), need to be sorted in a special way. -In particular, the regions of constant memory pointer need to be contiguous; -and the rows in each such contiguous region must be sorted for clock cycle. -The contiguity of regions is trivial for the JumpStack and OpStack Table, and for the RAM Table the [Contiguity Argument](memory-consistency.md#contiguity-for-ram-table) establishes this fact. - -The [Inner Sorting Argument via Clock Jump Differences](memory-consistency.md#clock-jump-differences-and-inner-sorting) impacts the Processor Table quite substantially. -Concretely, the following 3 base columns and 3 extension columns only help achieving memory consistency. - -- Base column `cjd`, the list of all clock jump differences greater than 1 in all memory-like tables. -- Base column `invm`, the list of inverses of clock jump differences, counting multiplicities. This column helps to select all nonzero `cjd`'s. -- Base column `invu`, the list of inverses of unique clock jump differences, *i.e.*, without counting multiplicities. This column helps to select the unique nonzero `cjd`'s. -- Extension column `rer`, the running evaluation of relevant clock cycles. -- Extension column `reu`, the running evaluation of unique clock cycle differences. -- Extension column `rpm`, the running product of all clock jump differences, with multiplicities. +1. column `clk` is increased by 1, +1. column `IsPadding` is set to 1, +1. column `cjd_mul_op_stack` is set to 0, +1. column `cjd_mul_ram` is set to 0, and +1. column `cjd_mul_jump_stack` is set to 0. + +A notable exception: +if the row with `clk` equal to 1 is a padding row, then the values of `cjd_mul_op_stack`, `cjd_mul_ram`, and `cjd_mul_jump_stack` are not constrained in that row. +The reason for this exception is the lack of “awareness” of padding rows in the three memory-like tables. +In fact, all memory-like tables keep looking up clock jump differences in their padding section. +All these clock jumps are guaranteed to have magnitude 1 due to the [Permutation Arguments](permutation-argument.md) with the respective memory-like tables. # Arithmetic Intermediate Representation @@ -102,11 +95,9 @@ However, in order to verify the correctness of `RunningEvaluationHashDigest`, th 1. `RunningEvaluationHashDigest` is 1. 1. `RunningEvaluationSponge` is 1. 1. `RunningProductU32Table` is 1. -1. The running evaluation of relevant clock cycles is 1. -1. The running evaluation of unique clock jump differences starts off having applied one evaluation step with the clock jump difference with respect to indeterminate 🛒, if the `cjd` column does not start with zero. -1. The running product of all clock jump differences starts starts off having accumulated the first factor with respect to indeterminate 🚿, but only if the `cjd` column does not start with zero. - -(Note that the `cjd` column can start with a zero, but only if all other elements of this column are zero. This event indicates the absence of clock jumps.) +1. `ClockJumpDifferenceLookupServerLogDerivativeOpStack` is 0. +1. `ClockJumpDifferenceLookupServerLogDerivativeRam` is 0. +1. `ClockJumpDifferenceLookupServerLogDerivativeJumpStack` is 0. ### Initial Constraints as Polynomials @@ -147,28 +138,46 @@ However, in order to verify the correctness of `RunningEvaluationHashDigest`, th 1. `RunningEvaluationHashDigest - 1` 1. `RunningEvaluationSponge - 1` 1. `RunningProductU32Table - 1` -1. `rer - 1` -1. `cjd · (reu - 🛒 - cjd)) + (1 - cjd · invm) · (reu - 1)` -1. `cjd · (rpm - (🚿 - cjd)) + (1 - cjd · invm) · (rpm - 1)` +1. `ClockJumpDifferenceLookupServerLogDerivativeOpStack` +1. `ClockJumpDifferenceLookupServerLogDerivativeRam` +1. `ClockJumpDifferenceLookupServerLogDerivativeJumpStack` ## Consistency Constraints -1. The composition of instruction buckets `ib0` through `ib7` corresponds to the current instruction `ci`. -1. The inverse of clock jump difference with multiplicity `invm` is the inverse-or-zero of the the clock jump difference `cjd`. (Results in 2 polynomials.) +1. The composition of instruction bits `ib0` through `ib7` corresponds to the current instruction `ci`. +1. The instruction bit `ib0` is a bit. +1. The instruction bit `ib1` is a bit. +1. The instruction bit `ib2` is a bit. +1. The instruction bit `ib3` is a bit. +1. The instruction bit `ib4` is a bit. +1. The instruction bit `ib5` is a bit. +1. The instruction bit `ib6` is a bit. +1. The instruction bit `ib7` is a bit. 1. The padding indicator `IsPadding` is either 0 or 1. +1. If the current padding row is a padding row and `clk` is not 1, then the clock jump difference lookup multiplicity of the Op Stack Table is 0. +1. If the current padding row is a padding row and `clk` is not 1, then the clock jump difference lookup multiplicity of the Ram Table is 0. +1. If the current padding row is a padding row and `clk` is not 1, then the clock jump difference lookup multiplicity of the Jump Stack Table is 0. ### Consistency Constraints as Polynomials 1. `ci - (2^7·ib7 + 2^6·ib6 + 2^5·ib5 + 2^4·ib4 + 2^3·ib3 + 2^2·ib2 + 2^1·ib1 + 2^0·ib0)` -1. `invm·(invm·cjd - 1)` -1. `cjd·(invm·cjd - 1)` +1. `ib0·(ib0 - 1)` +1. `ib1·(ib1 - 1)` +1. `ib2·(ib2 - 1)` +1. `ib3·(ib3 - 1)` +1. `ib4·(ib4 - 1)` +1. `ib5·(ib5 - 1)` +1. `ib6·(ib6 - 1)` +1. `ib7·(ib7 - 1)` 1. `IsPadding·(IsPadding - 1)` +1. `IsPadding·(clk - 1)·ClockJumpDifferenceLookupServerLogDerivativeOpStack` +1. `IsPadding·(clk - 1)·ClockJumpDifferenceLookupServerLogDerivativeRam` +1. `IsPadding·(clk - 1)·ClockJumpDifferenceLookupServerLogDerivativeJumpStack` ## Transition Constraints Due to their complexity, instruction-specific constraints are defined [in their own section](instruction-specific-transition-constraints.md). - -The following constraints apply to every pair of rows. +The following additional constraints also apply to every pair of rows. 1. The cycle counter `clk` increases by 1. 1. The padding indicator `IsPadding` is 0 or remains unchanged. @@ -189,11 +198,9 @@ The following constraints apply to every pair of rows. 1. `st0` in the next row and `st1` in the current row as well as the constants `opcode(lt)` and `1` with respect to challenges 🥜, 🌰, 🥑, and 🥕, and indeterminate 🧷. 1. `st0` in the current row and `st1` in the next row as well as `opcode(split)` with respect to challenges 🥜, 🌰, and 🥑, and indeterminate 🧷. 1. Else, _i.e._, if the current instruction is not a u32 instruction, the running product with the U32 Table remains unchanged. -1. The unique inverse column `invu'` holds the inverse-or-zero of the difference of consecutive `cjd`'s, if `cjd'` is nonzero. - (Results in 2 constraint polynomials.) -1. The running evaluation `reu` of unique `cjd`'s is updated relative to indeterminate 🛒 whenever the difference of `cjd`'s is nonzero *and* the next `cjd` is nonzero. -1. The running evaluation `rer` or relevant clock cycles is updated relative to indeterminate 🛒 or not at all. -1. The running product `rpm` of `cjd`'s with multiplicities is accumulates a factor `🚿 - cjd'` in every row, provided that `cjd'` is nonzero. +1. The running sum for the logarithmic derivative of the clock jump difference lookup argument with the Op Stack Table accumulates the next row's `clk` with the appropriate multiplicity with respect to indeterminate 🪞. +1. The running sum for the logarithmic derivative of the clock jump difference lookup argument with the Ram Table accumulates the next row's `clk` with the appropriate multiplicity with respect to indeterminate 🪑. +1. The running sum for the logarithmic derivative of the clock jump difference lookup argument with the Jump Stack Table accumulates the next row's `clk` with the appropriate multiplicity with respect to indeterminate 🧺. ### Transition Constraints as Polynomials @@ -224,18 +231,17 @@ The following constraints apply to every pair of rows. 1. `+ log_2_floor_deselector·(RunningProductU32Table' - RunningProductU32Table·(🧷 - 🥜·st0 - 🥑·ci - 🥕·st0'))` 1. `+ div_deselector·(RunningProductU32Table' - RunningProductU32Table·(🧷 - 🥜·st0' - 🌰·st1 - 🥑·opcode(lt) - 🥕)·(🧷 - 🥜·st0 - 🌰·st1' - 🥑·opcode(split)))` 1. `+ (1 - ib2)·(RunningProductU32Table' - RunningProductU32Table)` -1. `invu'·(invu'·(cjd' - cjd) - 1)·cjd'` -1. `(cjd' - cjd)·(invu'·(cjd' - cjd) - 1)·cjd'` -1. `(1 - (cjd' - cjd)·invu)·(reu' - reu) + (1 - cjd'·invm)·(reu' - reu) + cjd'·(cjd' - cjd)·(reu' - 🛒·reu - cjd')` -1. `(rer' - rer·🛒 - clk')·(rer' - rer)` -1. `cjd'·(rpm' - rpm·(🚿 - cjd')) + (cjd'·invm' - 1)·(rpm' - rpm)` +1. `(ClockJumpDifferenceLookupServerLogDerivativeOpStack' - ClockJumpDifferenceLookupServerLogDerivativeOpStack)`
+ `·(🪞 - clk') - cjd_mul_op_stack'` +1. `(ClockJumpDifferenceLookupServerLogDerivativeRam' - ClockJumpDifferenceLookupServerLogDerivativeRam)`
+ `·(🪑 - clk') - cjd_mul_ram'` +1. `(ClockJumpDifferenceLookupServerLogDerivativeJumpStack' - ClockJumpDifferenceLookupServerLogDerivativeJumpStack)`
+ `·(🧺 - clk') - cjd_mul_jump_stack'` ## Terminal Constraints 1. In the last row, register “current instruction” `ci` is 0, corresponding to instruction `halt`. -1. In the last row, the running evaluations `rer` and `reu` are equal. ### Terminal Constraints as Polynomials 1. `ci` -1. `rer - reu` diff --git a/specification/src/random-access-memory-table.md b/specification/src/random-access-memory-table.md index 72a6816d5..ca8240b57 100644 --- a/specification/src/random-access-memory-table.md +++ b/specification/src/random-access-memory-table.md @@ -4,9 +4,8 @@ The RAM is accessible through `read_mem` and `write_mem` commands. ## Base Columns -The RAM Table has 8 columns: +The RAM Table has 7 columns: 1. the cycle counter `clk`, -1. the inverse-or-zero of clock cycle differences minus 1 `clk_di`, 1. the instruction executed in the previous clock cycle `previous_instruction`, 1. RAM address pointer `ramp`, 1. the value of the memory at that address `ramv`, @@ -14,9 +13,9 @@ The RAM Table has 8 columns: 1. Bézout coefficient polynomial coefficient 0 `bcpc0`, 1. Bézout coefficient polynomial coefficient 1 `bcpc1`, -| Clock | Inverse of Clock Difference Minus One | Previous Instruction | RAM Pointer | RAM Value | Inverse of RAM Pointer Difference | Bézout coefficient polynomial's coefficients 0 | Bézout coefficient polynomial's coefficients 1 | -|:------|:--------------------------------------|:---------------------|:------------|:----------|:----------------------------------|:-----------------------------------------------|:-----------------------------------------------| -| - | - | - | - | - | - | - | - | +| Clock | Previous Instruction | RAM Pointer | RAM Value | Inverse of RAM Pointer Difference | Bézout coefficient polynomial's coefficients 0 | Bézout coefficient polynomial's coefficients 1 | +|:------|:---------------------|:------------|:----------|:----------------------------------|:-----------------------------------------------|:-----------------------------------------------| +| - | - | - | - | - | - | - | Columns `clk`, `previous_instruction`, `ramp`, and `ramv` correspond to the columns of the same name in the [Processor Table](processor-table.md). A permutation argument with the Processor Table establishes that, selecting the columns with these labels, the two tables' sets of rows are identical. @@ -27,17 +26,14 @@ The function of `iord` is best explained in the context of sorting the RAM Table The Bézout coefficient polynomial coefficients `bcpc0` and `bcpc1` represent the coefficients of polynomials that are needed for the [contiguity argument](memory-consistency.md#contiguity-for-ram-table). This argument establishes that all regions of constant `ramp` are contiguous. -Column `clk_di` is used to discount clock cycle differences that are equal to one. -It is necessary to establish the [inner sorting](memory-consistency.md#clock-jump-differences-and-inner-sorting) by `clk` within contiguous regions of constant `ramp`. - ## Extension Columns -The RAM Table has 2 extension columns, `rppa` and `rpcjd`. +The RAM Table has 2 extension columns, `rppa` and `ClockJumpDifferenceLookupClientLogDerivative`. 1. A Permutation Argument establishes that the rows in the RAM Table correspond to the rows of the [Processor Table](processor-table.md), after selecting for columns `clk`, `ramp`, `ramv` in both tables. The running product for this argument is contained in the `rppa` column. -1. In order to achieve [memory consistency](memory-consistency.md), a [multi-table Permutation Argument](memory-consistency.md#memory-like-tables) shows that all clock jump differences greater than one, from all memory-like tables (i.e., including the [OpStack Table](operational-stack-table.md) and the [JumpStack Table](jump-stack-table.md)), are contained in the `cjd` column of the [Processor Table](processor-table.md). - The running product for this argument is contained in the `rpcjd` column. +1. In order to achieve [memory consistency](memory-consistency.md), a [Lookup Argument](lookup-argument.md) shows that all clock jump differences are contained in the `clk` column of the [Processor Table](processor-table.md). + The logarithmic derivative for this argument is contained in the `ClockJumpDifferenceLookupClientLogDerivative` column. ## Sorting Rows @@ -183,8 +179,8 @@ Both types of challenges are X-field elements, _i.e._, elements of $\mathbb{F}_{ 1. The Bézout coefficient 1 `bc1` is equal to the first coefficient of the Bézout coefficient polynomial `bcpc1`. 1. The running product polynomial `rpp` starts with `🧼 - ramp`. 1. The formal derivative `fd` starts with 1. -1. The running product for clock jump differences `rpcjd` starts with 1. 1. The running product for the permutation argument with the Processor Table `rppa` has absorbed the first row with respect to challenges 🍍, 🍈, 🍎, and 🌽 and indeterminate 🛋. +1. The logarithmic derivative for the clock jump difference lookup `ClockJumpDifferenceLookupClientLogDerivative` is 0. ### Initial Constraints as Polynomials @@ -194,8 +190,8 @@ Both types of challenges are X-field elements, _i.e._, elements of $\mathbb{F}_{ 1. `bc1 - bcpc1` 1. `rpp - 🧼 + ramp` 1. `fd - 1` -1. `rpcjd - 1` 1. `rppa - 🛋 - 🍍·clk - 🍈·ramp - 🍎·ramv - 🌽·previous_instruction` +1. `ClockJumpDifferenceLookupClientLogDerivative` ## Consistency Constraints @@ -208,9 +204,9 @@ None. 1. If the `ramp` does not change and `previous_instruction` in the next row is not `write_mem`, then the RAM value `ramv` does not change. 1. The Bézout coefficient polynomial coefficients are allowed to change only when the `ramp` changes. 1. The running product polynomial `rpp` accumulates a factor `(🧼 - ramp)` whenever `ramp` changes. -1. The clock difference inverse `clk_di` is the inverse-or-zero of the clock difference minus 1. -1. The running product for clock jump differences `rpcjd` accumulates a factor `(🚿 - clk' + clk)` whenever that difference is greater than one and `ramp` is the same. 1. The running product for the permutation argument with the Processor Table `rppa` absorbs the next row with respect to challenges 🍍, 🍈, 🍎, and 🌽 and indeterminate 🛋. +1. If the RAM pointer `ramp` does not change, then the logarithmic derivative for the clock jump difference lookup `ClockJumpDifferenceLookupClientLogDerivative` accumulates a factor `(clk' - clk)` relative to indeterminate 🪑. + Otherwise, it remains the same. Written as Disjunctive Normal Form, the same constraints can be expressed as: 1. `iord` is 0 or `iord` is the inverse of `(ramp' - ramp)`. @@ -223,12 +219,9 @@ Written as Disjunctive Normal Form, the same constraints can be expressed as: 1. the formal derivative `fd` applies the product rule of differentiation (as necessary). 1. Bézout coefficient 0 is evaluated correctly. 1. Bézout coefficient 1 is evaluated correctly. -1. `clk_di` is zero or the inverse of `(clk' - clk - 1)`. -1. `(clk' - clk - 1)` is zero or the inverse of `clk_di`. -1. `(clk' - clk - 1) ≠ 0` and `rpcjd' = rpcjd`; - or `ramp' - ramp ≠ 0` and `rpcjd' = rpcjd`; - or `(clk' - clk - 1) = 0` and `ramp' - ramp = 0` and `rpcjd' = rpcjd·(🚿 - clk' + clk)`. 1. `rppa' = rppa·(🛋 - 🍍·clk' - 🍈·ramp' - 🍎·ramv' - 🌽·previous_instruction')` +1. - the `ramp` changes or the logarithmic derivative accumulates a summand, and + - the `ramp` does not change or the logarithmic derivative does not change. ### Transition Constraints as Polynomials @@ -242,10 +235,9 @@ Written as Disjunctive Normal Form, the same constraints can be expressed as: 1. `(iord·(ramp' - ramp) - 1)·(fd' - fd) + (ramp' - ramp)·(fd' - fd·(ramp'-🧼) - rpp)` 1. `(iord·(ramp' - ramp) - 1)·(bc0' - bc0) + (ramp' - ramp)·(bc0' - bc0·🧼 - bcpc0')` 1. `(iord·(ramp' - ramp) - 1)·(bc1' - bc1) + (ramp' - ramp)·(bc1' - bc1·🧼 - bcpc1')` -1. `clk_di·(clk_di·(clk' - clk - 1) - 1)` -1. `(clk' - clk - 1)·(clk_di·(clk' - clk - 1) - 1)` -1. `(clk' - clk - 1)·(rpcjd' - rpcjd) + (1 - (ramp' - ramp)·iord)·(rpcjd' - rpcjd) + (1 - (clk' - clk - 1)·clk_di)·ramp·(rpcjd' - rpcjd·(🚿 - clk' + clk))` 1. `rppa' - rppa·(🛋 - 🍍·clk' - 🍈·ramp' - 🍎·ramv' - 🌽·previous_instruction')` +1. `(iord·(ramp' - ramp) - 1)·((ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative) · (🪑 - clk' + clk) - 1)`
+ `+ (ramp' - ramp)·(ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative)` ## Terminal Constraints diff --git a/specification/src/registers.md b/specification/src/registers.md index 228d40679..1bc155af0 100644 --- a/specification/src/registers.md +++ b/specification/src/registers.md @@ -4,24 +4,27 @@ This section covers all columns in the Protocol Table. Only a subset of these registers relate to the instruction set; the remaining registers exist only to enable an efficient arithmetization and are marked with an asterisk (\*). -| Register | Name | Purpose | -|:-----------------------|:-----------------------------|:-------------------------------------------------------------------------------------------------------------------| -| *`clk` | cycle counter | counts the number of cycles the program has been running for | -| *`IsPadding` | padding indicator | indicates whether current state is only recorded to improve on STARK's computational runtime | -| *`PreviousInstruction` | previous instruction | holds the opcode of the instruction executed in the previous clock cycle (or 0 if such cycle exists) | -| `ip` | instruction pointer | contains the memory address (in Program Memory) of the instruction | -| `ci` | current instruction register | contains the current instruction | -| `nia` | next instruction register | contains either the instruction at the next address in Program Memory, or the argument for the current instruction | -| *`ib0` through `ib7` | instruction bit | decomposition of the instruction's opcode used to keep the AIR degree low | -| `jsp` | jump stack pointer | contains the memory address (in jump stack memory) of the top of the jump stack | -| `jso` | jump stack origin | contains the value of the instruction pointer of the last `call` | -| `jsd` | jump stack destination | contains the argument of the last `call` | -| `st0` through `st15` | operational stack registers | contain explicit operational stack values | -| *`osp` | operational stack pointer | contains the OpStack address of the top of the operational stack | -| *`osv` | operational stack value | contains the (stack) memory value at the given address | -| *`hv0` through `hv3` | helper variable registers | helper variables for some arithmetic operations | -| *`ramp` | RAM pointer | contains an address pointing into the RAM | -| *`ramv` | RAM value | contains the value of the RAM element at the address currently held in `ramp` | +| Register | Name | Purpose | +|:-----------------------|:-----------------------------------------------------|:---------------------------------------------------------------------------------------------------------------------------------| +| *`clk` | cycle counter | counts the number of cycles the program has been running for | +| *`IsPadding` | padding indicator | indicates whether current state is only recorded to improve on STARK's computational runtime | +| *`PreviousInstruction` | previous instruction | holds the opcode of the instruction executed in the previous clock cycle (or 0 if such cycle exists) | +| `ip` | instruction pointer | contains the memory address (in Program Memory) of the instruction | +| `ci` | current instruction register | contains the current instruction | +| `nia` | next instruction register | contains either the instruction at the next address in Program Memory, or the argument for the current instruction | +| *`ib0` through `ib7` | instruction bit | decomposition of the instruction's opcode used to keep the AIR degree low | +| `jsp` | jump stack pointer | contains the memory address (in jump stack memory) of the top of the jump stack | +| `jso` | jump stack origin | contains the value of the instruction pointer of the last `call` | +| `jsd` | jump stack destination | contains the argument of the last `call` | +| `st0` through `st15` | operational stack registers | contain explicit operational stack values | +| *`osp` | operational stack pointer | contains the OpStack address of the top of the operational stack | +| *`osv` | operational stack value | contains the (stack) memory value at the given address | +| *`hv0` through `hv3` | helper variable registers | helper variables for some arithmetic operations | +| *`ramp` | RAM pointer | contains an address pointing into the RAM | +| *`ramv` | RAM value | contains the value of the RAM element at the address currently held in `ramp` | +| *`cjd_mul_op_stack` | clock jump difference lookup multiplicity Op Stack | multiplicity with which the current `clk` is [looked up](lookup-argument.md) by the [Op Stack Table](operational-stack-table.md) | +| *`cjd_mul_ram` | clock jump difference lookup multiplicity Ram | multiplicity with which the current `clk` is [looked up](lookup-argument.md) by the [RAM Table](random-access-memory-table.md) | +| *`cjd_mul_jump_stack` | clock jump difference lookup multiplicity Jump Stack | multiplicity with which the current `clk` is [looked up](lookup-argument.md) by the [Jump Stack Table](jump-stack-table.md) | ## Instruction