From 13e74a9aa631b946c2a31fd28504f35ab4eac4f0 Mon Sep 17 00:00:00 2001 From: paulhuynh Date: Mon, 10 Jun 2024 10:54:53 +0400 Subject: [PATCH] Fix doctests for Linear_layer component in MILP and additional typos in documentation for various methods. Inequalities for wordwise truncated XOR have been regenerated as well. --- ..._xor_inequalities_between_n_input_bits.obj | Bin 152003 -> 56146 bytes ...ordwise_truncated_xor_with_n_input_bits.py | 3 +++ claasp/components/linear_layer_component.py | 7 +++--- claasp/components/xor_component.py | 21 ++++++++++-------- 4 files changed, 19 insertions(+), 12 deletions(-) diff --git a/claasp/cipher_modules/models/milp/utils/dictionary_containing_truncated_xor_inequalities_between_n_input_bits.obj b/claasp/cipher_modules/models/milp/utils/dictionary_containing_truncated_xor_inequalities_between_n_input_bits.obj index 096790f858ec85fcdaf4e984cf0336d76ca5c552..3b3c238e142dea79ed7f7dbe1c0b4c609ae6dc6d 100644 GIT binary patch literal 56146 zcma)lv92v!ZrsS0GaCW~1&S0anZbLu1OJ0E<$@u=4pxCIR4ub+PY39rZ?N|B#Q7=eJ>*PjfP0Zad_@_NP*^b?h2 zM&V-S31kXR@aF`wJ45_*0;ld;<7bL1RKdk!+4*lz4^Q!^autUZkK9zJLqvW)a?f=n z;!jl-G2{Aq2w16&>dw$m#pqP^QVZ}KHW0?t;%d;3K~+)|@jwNOtWdQQrSpFM1g`5R zK<6MKs+}5f#q{Ak1K0Hk=rWt})-%Hy@I^A7K;(LW-^MjEJ{hhzimR;AN7|hc*CWHe z&uecDD)sn9b+TFj85xOywVM~MhzD@3T`qy^dSukrs5S%oj!%&uD0;5IP~(@s`uFh& z{Bzv=_7vi*-shc%J)nV-P`&-R=aFN`M(0MZ_bu$(#%nrfLQE{S@x-t2o!`RD zk^mj+dmXmLUOI|q2p3HlizOUsx40*4@O+v3@do_ok$N=L_ceqSP}_Dsh7afpyDQ0# z6Z|>KPa*?zI6-&#VmDm8RYN%$aSZKCIM|3b)L3j4W{)97;x|eW(o-mTmtA0$=Ku-*3 z7!m#)*IH0Z6(5e~Y+xc=g6xR~N*=iYclc*Mnd~@+nf)`4OBiKP!Qaz@+@9g_px617 zP0$dQ+N!^0+ao^7dEUc?Rvaztw4lIc9+xnH2)~Wt(%~4wDeWcyEsQ$ZcHU}R_+;C8 z3rAH82)cw#`Ac3FK};=MrdDh3@acP)H!h`ep7(4>Hc@t*Y9jzVk7L-Hsoq`WNMtw^ z+~KSW4xB&X$g}X~IR$=%DexhuQ@TH<#^{uVL%}00Xs2wdmF6j|$H{eE-%D8eJUr~d zBhq@zXN!fEQ7ZRrCp2WtJf9A{s0c=D!?l-(u_Sp(0UcZR3o7ASI#iZ$NLNVWJnWZP za0uhNuGS;edv>*|`ci67kQ1JwL2jBVX-GKP(?n`^WK^ci9!r;OC0_zEyV;VU6V6N3 z!3>YlQ+v{#p2tLPjwG+yrwI?&pxJ^Ki85Q)?09lZ?Gq4CD#mQ(8?4n<-Vd{*erDG^ zP$zqzDuDE-COw|5aac{A>IdzyJ6P zf1@z5c$K$5_N1J@P+)*oP`u@kqw-ZyEz$U1(7;zgExf#AzuiF>^tI0`4=6wR4CSJ) z^Wka-l}{oSBn7ScRg(fy^cHSR_NL9zB?$6sx#JT88wgBLdofv$Ba;P!=?39WF@u{X zyD~B{;7kw5Cq)YyU)3ZF1|u#I*oPiFhzef$9mM9Mc^in%E9f|maGhWUHOZXgCsXd^ zTdwuBeBh5AS9k-p*)1QTlj*p%3s0ZS5^hDcpbgbD8OV-12t@(naR*`h5ae+Op$>vP zet=L3AUjr&db#A=&R39!)pj+ag4FQEv{)c-g6RgymCm&JBm3g$*wezhc$}Sbb&O4i|HOqGFc#)Zjfd-Ot1^*9@6nvw1a3J&HMn-I{NehqARrE z3uL`;8$UpHmwC9ZUKQTL8>nq&UA>VB`js#|3)*JZ)ti`(r6ZG>ney#6*O(`!7`4fn_41|1Mxyq%c08!-yN=*r}D>o=K9nfv2d@63u z-I=E1)(kQQ#jOPd1)7(P;IRo0vGk@W8$tA@D4Ri-vIW$YH4t{fJ`U@+39n(DPZp@* z!Z(55Lb}ohT$r3=1GVq~(k0l)9&N+lvDp06f^976liu}mm2Wc{mZhBFR8C>MHF9C{ z9&8psxP_g`#=JA}Nn+3$lwtABpwOgEN9m;;E{CQa6n&|QiAm4NDEiIBTNG~0nslEy z(*}yLtqU+Sli!vW-a*WcXUonc4lBpflLck|J1A%O&6HF7Vlq(Ks!5ZZX*TXm^2v=@ zEx2uzXW-2b5AD8_nh8`4j2qSN-WkTaF;22f__CPCS)33-=|Bj_0D z2`^LYPOL9T*$w)FB7BssnzSlm2dKK^3d@Ku&~d2j`#!r3)YNbz^nN@uT~E#ilH~G6 z%}u|%%lj@K6_$2`s3V*Aq8BI}w=t{e#Kdw9`j)#3f$s%*cMQ~o#{vWa%I+xO0cDtc zlHWkDWl;ZU|Pp?>|`%7tl~6mH!Opx%5w8XMEm6h*;`F*neqMz{P8a;E29 zuQO4TZpbKYH);p*rtaOnpw``a|7=WA0$6(z^S$b2VxU3!0GgPJGChnMNRkmip|HbB zUmy#&?jY#_*`?6LgclTHcE_UV@ntG%5Ty|}D4342iHYQ`JM!J#sl>5h0@;eaTh*B$ z1{aW>W{ym@*MvqBKwXZnzR7ac8Yj)9{ZGpx-F+ESq0pv_&7Y5M#WEw!hbQWd+ zwfn@!{A^})$0gZ7Mh@U{%N`$iwb>!8yCudvgHQvBb|l9Lk`5ks&`~306O&{X`4dRO z6RIu0yDMQUH-k!F>TxO;Oliaf(!GBTZy=(8BpG+S91n~|wm(dkBVd_p{L3dE}r5@w$8sC+l zgVDB0CUj-;QBeL4^00Ncf?P7lYA=(B~sH0lBO8WTF(0lK77RsZ9MM?DD(x=Emg)m zGLa*pn+4i&D%*UL1#Di!8Oy~$5QH6DIX*32*#c5I4fun}guCNwxuS`Dvv6x(6I?-V zBRufco0%+}(8U7h&@Oyhz~;5-Q#pmTDl}pQ*-*W^9RwUSJ!zAd+RD7S9s*Q0w+*=UM)AtQ@P0dzs*F+`_ z`vqy;kd4(lZrz*7aNA7a9}rN~QGI_vygBP;4opyNHB@909YD&CqJ-{D$M=b;*=W8GATLCyhBJV!seLnf zp&8_x3EjDwn9$|8l?$(r5jRM8E#Jy^kiXNJjXS9BQjpyG&xh%9XauDu=NLggJC?`<$OpK7Iy41>et@_nK;~FzM`!Y#EVCOx z`?}h zmrszHeSI*MeWEhszL+B0pnC2OAO#w9W%5GgdqL{XnX-vRlTXb%y+E=cG!goiy9;R- zZYIB(ASdoV&^;gvx7iIKT;dL$*-aqMj?mCIl(S3Oot1u>BJ5tzAUJ;dQl~r9>2WA$ zm(JZ1Omj>3qM$+A22u^_@x$oL+RF1)(pb-{oM#g%BlOT7EC?vavNJ)HyEQR2$*2m?Hcf=e(gD<_ zCiyFqn%_Wev>Nu#q@84sFR0I78}ZSdHNSwgBnX!$-NWRYiR-zUz+VFvM_alHbo$CM zKTI^x!&C+VHz=}g$D{NEy0+W4U}ti#XHa*DMOP-5ynwJ`)kZDx(jB4h{#(vxhd_=6 z)bCjMz$irr5INfH29VTnlg@DNa&>lMeVN+qHV_<#@F-;RZ3b7l2>W)=Ae(tQblhwhLaB!@VP9n`|+ zzILmX^K3$8!~kk)Xv6>t9k4u~1Bb`8qzU0(^Z{jzlWk{F%I_fGYfLAU z4Io^CE<&@@*KvYibw15UrX0m5Q{hNUoAB`I7@>u3Aaf|0aEhc?Q|d^!2GHI77gMox zVxpNT-->={O5X>NEo+(DCsQ;(gFs$3(=ELRe0;(g_(tI#fUr~so$xNqhJLJffM zWR1<7Ko)MpnLwO84rdoeP0^QkIx`gxuJXea*+@6}Gf0o+1GUmC({XD6-OYb89ZN^1 z>UBV`*@fie`^aRDC)DS-FrDFyOm&mo(tDpyA!~jC>D|1%r`urg!jPWd8o_XvKY~!f z3Z+{k2)aSdBMXfn)X|doR?Q%FWXGKeV$yLtpP1BeF=7JQgXS>dd;$fNL76atibHa1 z0y)#MbOIF{W$6S;P2u|lf+mEssI_PF?^{s9CVU2I(E@7vKbUfY6X@MZU1^)?h016* zke4W9?%kCECloDqP?WRY%lQCmVR1L%WeWnzVK4)QRq zTtR%QSP3w!pa_40kd69SOB_F#Jp2XHJxdPrI-YvHJB0;ZLB5UbZU=eTy4yjvPu|@Q zk_Ccp!kI0HG{^OlWyjVJdZ0*CRmC08{(5)QR z6lGI6_sOB3Ohx|01wou{<NsjiTh*%K`cOoelcC6otb~RCtM__zb!8qr)vg6jM$t>`q zVaLK$ES;E`9rE4Sg((Wj{TpQDX=5(&+#R91IcH6WNl+YTrYwYUyrAlGxCK;qTzU1q zK!a)n#-)2RIpzyQ0}0*B0fQ_G{{Wep_1>K{)y-t{11LsoZF{GKaAr5?3yQFf!i{}F z^2woEm=_e`W9cB=9ye#l1$|~0Oa@iyk;xoSs2h82L4?n6My9&sg6^7ff+N!zh?nLx z`#y0j%HBcrH^OH)jp=lUGqG;vI&|xj>D6$P2tV_8IdTWaCxdn!D z<`ay=F~`DTcQYXd7brPcE$ssNxNsUI^9|G3&^@F^Vd^l z^U0vHW7I^kPmj-l$#I6m9y^E)yZmBA19_NG--3aus!8Z|BeX&rNDaTfH%$r)8v4xl z3uHc>FwQuf28u8(MR){tH37ZK1(P@yP;__iLem6LE`PAvzTcqIohRI&%my@BZ;%2v z^eUI(RAy-t2useF{UX8a#H$H+CN2#3NeLq;2VxIlyk<}|{|%A_hJBgNURx1+4Z>sT zO!)`ssQCh=njOSC3QM2Po0-()YU-9=AoJ0gxLYHWMG};|)tQPWhmyI1f`fq{fNEGh zRwmxBAv~0s#tMpZ6#oNI4a=>{q&vj<0&3H&pe$#BAAo8YOLs9@If_2(#w$y?9LNgF zaNs8xMIEo_?b%&_ArCuizW07K>Mp0Femd4Zma9rT1Jre;8ljtf;ZHPE5$ zbU0$Zb|p8{4X7xb>(2oxeCeM-7xW91&>J+0GIV=BWqPr50d?pn zD4-8$5=HQNV5E@d)CP)5$imw&kH>M&Ao(2nf-LKL*~ftRcg*eInqyc5<;c@4r@#Z9 zKo4{W6=(-7qApNLZ?_8?O5r6?TOFCicUUjbEb0cG^fI9tbV0vB3B5t1s0Wnkutw*4 z6cnFM!1f^~y)Xrbpby9{UoZXacE)mr^)0I6&yPVs{R&Y0W4_pNth{mCr+G=YkN?+? zljrY!^2hiA$&rAjlrWX`U$WGAPo#o*%Qkfo*x&tPe zn9#dpxOF#zK;FtR?P4-Do$2`7 zCr}*WKeE8QMgmICj#nl?DWGWzGm)MHwjLX(Td??aGkuohK-lRZJecTpJQwZ(Cy339 z&)jOl14J9$CxbQ+xW{X!OZ6DJ9uEZ{DXuYnGSsfluzrU04P*v!YL0I4qv>nSys3#KUAK;5ShzG%{Dquc_D zRZ+PG6dY&-_zjd(lgcJME%2$a+|6VL=00tX>k*iIKHy8!&4hBGer^Qw`Y_3Y3v|Lb z<4#(4L%Cc!kgD7R>YJ%@56H5kD2MYp-n;XKxw|_YriSbLG6jf|86JJI?0~Y|&J;Td zI7r{_${ifSFHjcZK2aGC+gK3LPHHdE>-lt;Oa`KwVSTTCO1{RVZ0Fm3vgQ+%MK7if zis9TKWQTlO@H(!cW;t^UJHD9d9Moh2TDd56Ml0?S8tXTv$u^`KCYc-0mAlH!KZ-R!PUD#xs9J7GNI@fh~>Kc zYj#={DGMgs(o2)wuU+^6k_9%kFQzo`1H?xK%=%_}9Di&t|93x?T23qZBp1Bz{| z_sjq?CM$Zndq8F#%6)^}aho9TVDVjJ(LNEnf*8<%Ythc+pi^`&SD+IJHsLZ3=@Z@W z<=A{aoD$=ZmeTowMz&bI(PIuliPCMtlYBYXg*@MJ>T zT@F`dX71AfVj*?(p-D_u;tOPV3za!&G}9bsM_(Xk`syynlA5OOw3DcZqDTJaIJ>(v z-Da{E-2yukIn2zX$+&wt>gY>1fV7z=KYW@%<`b12&@DX69W#yl(nJgDQ-ynRfvhjL zpcL((xH&&9Ks98Qf!My^KGDX$Dii2gmA5;j_4(`ex`lH|OxcH-MlP`dvJrJA*n}Vr z+(GV>TZ#lhMFreD$ZV-OdXw0J~fhyChiG{8k;T5ji(vPM0Xx%gx$oqltFQ#kHXi6y&Y4^p_&Vs9zr^2T@-M|zkVhL*hY3_}r+uS*57-~7 zZcMgOKEoYk?Ux2dP1>j^clQ^u#FWB+0J5-~xs;35{kA~e1=DP1GJR=EGc}e^pQ79hk}dBM#OEW8p4on^ zSfKK+{IN^+WUnL3yaN)(*x@OUdF6nv0AK?sFV(PEXQrAk34g2BkA6*Ur#j_yy+^Id zy<9JPm|D3XfND5uCzFB`q|7d|Tr0kuD;LuVjG#HJS&vLL!Bi$lfjfLLxlOgnJWrJ_aiVMML-{VD*4ib;9*YgH?!w%h;T0#XWP{RXL1qJkIYu!~SAc^_{ zC29aw4sp+*X>jsr+RmDHvVpsJ{WHZ@{xOvX`p z1W8R>cwmZ5ezngM{(8zqKwq11U1IJbNW3!*5keZ%#v!sx)6AIV=J3FjO6|mdt750E zoL$HlGza?xDjZ6gLCMiUPj;5YNoQK19aPiJY*#*k%KVkpL8a|V8lWXSG3i=S(?L&Q zDz|WSCI`i|D$g_SisB0CF$KAK-1Du5vdB3;lgb{SvRsA-3vN*K*etjmS9kC1 ziY9-m++)ddfa>uznAyt((^c+flBUm9@hyO*t-Hg7GdTV$y7MgnbYUU~nGD)M?KbxT z51VN#=E_{tz+{&aL`$CsYwzxdW|{?yPkreEbXjnN%m`cJX2H?KFmH!P__YPTFju)? z@_Uze%VXvZilU1qv%olD#195c;kGaf6FFS?Wx=%tGt&(+z7I1^co?y0^6*^l@@W(< z%zLB**GFxB)X@Rkf|t(Y!^0A8pqf|ke%hEeXn?#rhw3|y`OZGkWz8RJcn?^CCX+$mavA2-$oH1(nv8W|QrpSLa^DtEjkr1C(M+llcLS+yFSju@;Tuzz zYy%l?gwC{pk}0P)bf;cIxb7MA{p!vxy**waj)F@Ue9Jz)MK2~eXg4^D22-8gFaPv+ z|L_0)(SOr`aQtih_s{sxuKwqC^>6SU|9S?S=dWPIeZ``7e<|lLPN={iP+qWGL9de- zOeb{U-pVQGw|4ttKJ%4KEzED=j=w%Y(BxDfAfGc>KS0) zQT>2PR39KQ87x8G2*_h(`QSRB2xZ>@$F*eQxcb2{^)CyadcZjBFa>wkn?Nyxlx|td zJWRojkSdR$t~#KWP?+v|EX6|wNq`Zu-VC~^lw-%rbV*-8ok}3fY)qYM12rlKA+s|z zsufhJ0#yFTPs|>?GJ?mSuHf2LF0S)ypxUot8X{(A0zR0u3kLobp!|OZKhL78Cck}{ zCio4Cj+z-aDAZ6tNSZouV6qxN0FkL%*^yd5SVVv$h3lni5=s^CxIRg0UKz+ zq$Xq9Fcq|73TVe1&<7?#r{AH^=q^Fd*oYkz*WzpD@T7xgOlVSc!8Fi@sh|~8Ks)Au zJ}?0)E&FEGac^d}oe0p7f7rX3Ex&<&`GfuZ^j`$WF@CE0%fG`n|MP$Rhu{20A-f(w zSN#cZbp5u&S{C9@bb+eM)l-d+EXVqj5IBB*j;m=PKL*9s1cN(1h5d=Q#7j6FEXC<_ zlz)T*RwlDnVTjA7xnM)GJvx#XKYIm9t0pi%;UqQ)Op1RzF%ACWk6#ZKt(R&Cdoi#O zqt0+H)T?%GUAY;h8ZFi#7!J3+4d8WruNEYJ_52Xtcr&?QjpVrc3vW+Q zjW_6@VbQU!ChfjU6&i2VKU0E!iD8ATsMP)$zOfuTu;CWM3Zf7WL&!d+!XYN?^4fM+%2Ss}BAG)B9^Gef2uJ=Q}lRzpU`dOVaz9PG`P{g#KQ zQwuR(C8iRpQcyB2vsA-Ua5jV@-b0O%iAgBww1YYE95wMIbH*#HG8)34vuxQj?CKa& z{0;#gFFyQIp=(2sDfpTpF{$#&yoVa&6^aa_n?fGHLe`VN z${S1FD2u|HcmfZhc$3l-z_!isIGCf+GRxzx!?pOeY!BJr)!A>0hb;YVlmA^rWU+!+ z?^>*I3RW3M9OEsN;@*(y@>-WdNRD4P+gT&bmL@_VGqq*mx_jpKp%Na+BC}&vsH^#jXb45Y7Q$fS`a*cQ u(GytpA}oAep*<+iE3#7Z5NZjGM^=If;d<53NvxrBmFW@s<)8lPcmE%_QSg)i literal 152003 zcmb8YKeJ`Ya^3ep!cc@{Fc36k(S9-pF%#6cc$VlhL>LnQLm?V~Xd;3RWsRrC_tpB7 zSyfqkXYS^i?sM~0{%Y0Atg3x)_sj$S+h707|NN)F`V(LO{NvAm`Jedqum0nYKmYOX ze*NXwc>VJ0FZuc{gCBqVyFGlM1y~<`dC{W69^U9$OhB%8eEl`q2Ke>2G~NI(9uf`k zTjqah0G4iv20(INLd_G>E6hu{{gfCKEYSc~AR-_PLol}h`x<>0kRMiUNaxtR1lBO{ zSOfDz!a(Y+HEtl9LSJV2?kGI?0|Br00GK*o#`vC9TsEbsw*;;=p1@_(Jl|6x%f=8_ zdjYD10dh;BO1uF@A^^ulz0bF-g+hR+o`a!xn*2*20(lOzi^5D zEI8I!VNrNPPavJ=UQwk~u@B7=LE-qcR^Cmc$u+#AJ!yN`*&Tsfz#iQZbrRU4JJLD< z?9m%u9^Fyomj~F{$sLv5%sJ~cU{V0@DfchSJWg!I6R4w}tg!&vd{oir zk1`u5J!sX<>`nmK!}iAa0_@=&Kc~Dd(E`7$Z>L-JQaI-tDu6vyr~pn4fD~%}=p>d@ zZUU%q<(~>80EIjMPOSojbajy*#>spH9|peUQg)eUTgeBp3QkCi)X(pg%(z{V6gHtUf-1 zl<_TCo3;P&yQ94c*n(sDWl}*OYu16B&W+uwJKC4;T{Y*QH+GMm$7PScMdx$iEx*Um zvvmmf=v&0@Ci<4&W7>y6_vl;X9W(lt-(x0iV2{2SmfZWc(Ra;b zg@tzHQ?(@@XiwhgKwjuXUMQQ|y_Ss6YyM@=R=|GbUtBF#&B{OFo#-07&=@ahj@_uo zD;i@DRO1)wu_wy$8`angitz`^u{RVy@vpOq1LfELJ1-sW16bW``g)*r#}`yHDh5t8 z2pTY3y%yAjyo#Mru`Y}3h>|s`sQ1dE_(KT4Dw=Zq8`wW{18!F5HOX8qa|(uyo8_t$O(>fc4Pf++;>oTTfMCHrSZ_h7VYh-EP?gP%jmA!>SfLTM z2Gjtns>P$Kn`I-qrCnKS0Fp-8w#EQdvRT0beXwp;G`2LWLHWm3ynseydsP@9D>S0c z0KI}W>S#hi1gdC6eGO$=J-r*N4sdOkg-9&Rx?2#dv#6<)_1*#blvi2X!ZuTlC-2UrN}Ld}e1MY@Gu%`!@CMwNA0U`JJ^Wk8xAs2Y1W zt9Hv?Sqw@t%Er1`Et<`OnXEj&LL>fk%(B_7XcmpX$nItdW%a7DMMY3mof=i$OQD=K z8StV;0e+xt?4wzwTf47lY@ldt+W|KVqCQzLo9HQfG>a&UqVXOzLDbQNiV&)3L`fKB zG@~E_Mf8CxucD4-Jvxv-F`!xN=YcKE)%a4g&`vdp=!%@jdqwp`VO=0|QiHN+*pzBU z4T^N2JL*ucO9LxvP)g#r4MfzS%o^QMhk^)nMJ+0e@|sbDLXi%_tD^?x>IQbyp(LcL z@)Wfwz(6zVQC8!!B5F{T#RD5>kWqtTQPxG(6?Lcxp(|=p5=JxXQ4oPfG@vLvI^gIX z#orgOENyH?&lcz!;&~}T&5Ec&@w^NGYtJZuAR{5whU23a>n^7*D2EI^P^!Eaq#d_}s)v_&$nh9Z9R`00s%Iyg>9JH#ybh~YU zd(fgZV1Nc34F&?G)ln5IvKsD|&9(;Q6=LC4QD;CKOB595G3rn>%K+E^K)D4{6+5c3 zS&2Go47e;FXsr(A-YW#zrYvhhkqcC1ji^qRE{t2y8}M-nl)ar%$a!PguNKw*>u7re z;t*b!E3ctiz-DP@y|Hg7OJNJxtPhlpH_8aVC)Gr`{){3Y1`v&?l6cb@kgS^ZUKTK+ zFz|tb2sF(0s_cMODXNIDH;oZn5?cTRR3=Z|u~~tF`ar28ErXLPh(y_d8AS&Oz^dwE zDMMLMjFsBdX(;rBKkm~6R7reQq>ut0hKix&~7CP;nu5S#dKpirgkfFcJ#f3dD;Lba|?MFUEwNXOBp@K9EwG%}-3L(AZ#3c?2HWK^YB z9)ditld9^9W_g8|L*S#WYNAJ(JG76mO26BD=Pvu~MMW?Ew4eTgTuL}W)a?%ENv5Sz~*nt%_sFoMHqYjnDFcA7J zN{dD_YEU`^5?&oOC>qWH-%0QwwJ{S_Gq8=wQM*BdZE10zZU254YJ`F8`fNCO!) z2A~=!zj#uMA}>`s9Z_`vRCGX5qsl)S^T5b!L=CDA2=(%u)S&7>s^aT_sspL|g|b7` zA~&ki01V<9K3q?M>M${PaZu#*B1F$gll>~1r%b!s17E!G}q28@f zrEG7&yA`TmC>vxnqqYMqB@H-gQ14b6_&}LX179dDs#$QNs4<|E1td$0hFX} zyRrCt6!yvnB5GCDtMvMzO3^?aHL8GUQ5QyLdAT2~pW0{vS$2R8*7LPN;}inr>Jy6Q z2S9Q};gu~21CBbcabRs=L}|c)tV+LE1tSBP;iy5O8UVk{D4Qi!ZQ5u+r_hf#a4^yD zmQJBiEkB^@fV4nDc0iG0<=g^&9Z+>Zs5+piYnF}+wbX$Lr2*>MfTK=T$3?2DicyE^ zxCoWm83ht(M2)J>E8HSY1ByCSyCswcCe*t{RI5)YT%wnu8c|~aPyk%tlR8wpB?EQ< zD-B8m5Mu|V$*4hTz^EFaNgb-)N&}wMqpC+IE20LKS0G5!tD**#R{@lqQEe<$iG880 z#b`vG0pEf^F$YnDG6##iFmVcr-jD5g!21*ubzwb<7O--lTwPJ4%8Cq-98qL-3T=S9 zFd8r*s}o8CMrCzEnWIIPCAc>L#Xu3MuGTB05+ykrh#M0f;39l!dll)kcT1;`fH!ME zv8patJ~9SW9niAsz+`|qEDZyALsf&SI$%`28c-Ubnzz7F(*X(^pn(}>v!u#>{Xn^~ zG=NjB?NZ}kw}1v%8@Ct688u#!Pn4@qDDr`F`4MHa@S6tk?x-=qW*Km+2Cozh)DEVy zbYsH+mD>)`fC0Wc>bycGP*ydn`o>~eHi~d-03`uJb5)$9&VV+SsGMq2htjJ6zR#-K zEvbrS)T**si8^Xf7R};$2-zz}d|8|k2l4^0qeWC^2Nd~G zHkL*6sPepipj_1`qtO6YP1P?H`9Kkks#q4gr4Aq>?0R0yN)%Q;P*yK3fL|y#R?U*= zU;q^F7OXMiuhy$-HcA5%3VWf-Xhf9^Rlq6fSzv>Qu@ff5{5>D8);zEGZ58c<&u zHD0wtz<3B@o6cX@^?>KmA}X^3N`ppabx=hdG*a91%?r0!Ub#*{xP^yY%RUlCo zq6zh0a#=+qN+}y)G@(rLY-x? zMuRH7;t;~2qXEU5fjXK{5>jPRSbyjMi9i|6C`*BsOiw6sWN?}yS_U{hUh$vGV$nnu zZD2?FU)4&MsxX2{8`x3)7r=?Kq!DErzo_bHYwc(mNEBa5XDyGiXwa$=^(b|WM%1HR zHB}W2DDr_i>QQn~jt+2*wk%gIl;usR{Sl35Ql*kr74@joR{cV`u2j|F$*UTW1~jeh z02B$REbI0t4W@w)RZ0b_sP6!lqCr)4N!8JSsu~*ri=zWCe(flp zgzA-1)-|J%x9I`pbDbvjfX^r`@aGi0^pmE(1%Ne5QFccbVUscEYKY_D8W?Cs6m-Fx}y%|x+;r495tvL zpbn@N!x_M`kRq_7M%7gbmFY=UqDCp-qxd;r`{lbu<5(Sdy!Z(({}qiMYw^^UU1VC6 zJ&I?RqZXyX`hagx{81}V)uc%c%Cgumm*uEO+0OK;s6|Q%+CSvok}_4kd1YM|7n@PIN;K%OVmyA=;jSYXr`01CN4BWh84 z%;&442K8Lbdu(ToNIM%C00Rn{c~SbsvjTSUdps29%N8q3laWd|^C z*ew(#fIb~f9S|xbAFAwCc3?u)0Rec6Nv#1PYF0)KifhPP!hoX&r2zxf{6J+e41A%? z8;z(j0Ei3w@fOkZa>d`l`*P`MYrn9u57|Vq?Dc?e(70Ssl2cA4xj~$8Ux;~K+)d`)ouxu(*Z?_>*~VD!E6BQ z+AF3Es;C%gq3YIvA{D5teyB<b&Z}rhySfGE@<l7Mrn0Ikq^{GO{y@!+Ub>FClt9rX>~$rzyJ-5C<@Wixm$w) z=mbhd>b8AlcMKq!QDEBA=m4#^yTuL&;QEf5jU{CO(Tu7Cp-S1ofI1*R9T-t|z$o5F zRT?1UEpXJ9l_(9&D4Qi!_TdB7HG~0P7QXr|U{a5Daf+VXl@EAbE^aK>kEizagb!5R zif7i0LW!4)&7y@tm3gBgCzL|GG2vBFTb3G|UPqK(tx5+IDz5_MbwX7${qlxMSG)Dv zSLzr=q#|E-R$G8Fq24VS;J!_$R+U#pBT6Zwj3$&F;FHK5(7a&_5`}{i zMKVxDbknOs%m$$Op_(Yc8RfcCrO^>(1NeaDHB?o-S1cN+qNyx^iQ4L*%2mTFolea{ zl9x+&i)QliR=ykT2YjNmFrn;`RT)hv4H{K6pv)U}G@z;q2UcaV8?#q5Rw%2QP-cxP z8c^f|bu^#=!Gr8dM<^s*VO!>ql8!e?Yw|4LF)mNeNXnpxP~5uGlT$ zeFsn#9|S}hO(>FqDjHDa19dc@1W}3&s0qDSrj05ZRB6ztqXAXXp(?m<7FSKxFBJJe z6-@@?=1Z3`jQ{@a!ws zH0o$;?PxVCP)SZ+*~wH@w6%7Ws)=g-NmZim0Ow4oc1v3n(Oz~(t68z}ROA{{vl0b1 zqAE%TA{tbw6kZh#C_$r+dXxr@M%1IKBvb|WC?!+%3q?LqN4+Y03C0(O(SX81ppJSJ zSfCO0D8W=!)T2xrjc7o*u4Qrgb=!zPYd80dOP}h=Pflp=WY^kh_I#mc+i(f`nBm>w{r<&IwOix~A zP-U&CQMEy$J8Dp`Z&kV-40u(mexb?>UD3M%{4}Q0eX`IuUMEb9S6nXtL7FH`1gdC2 zv2dV{dXyH8M%1Fr8_lRe@du4S1!_`*ssp}!n!@`qpxgy_z)_E4<$4WUlpgCfY*3d) z)MYVhP?p6XUWMWNl!L(PQ2%U&99*f1jng5`{GHDy99>$N1kDu(6PhGoYwPY1U{& z9U7+)Y1h{q!1-ib0hs*o%2QykjyeM>D^d2Am3JM$%7I4Ip>bf5mf1lSDOQCQUDkkd zV;|RW@Crc~ptz#Rt5G_bPRDMBu5lk6=Va%M*{|^IHE{~DzOpe1)xb7h#S)y;ITKV2bLyv9ni*7^}L47 z765x*!;8(k#k%5dp)Mco2GuFlc~uis);sD`7-xVx^3nnuU}FWSsS~QE3t)uTpo%Q} zB(DG&@fBYXac*`%2R6$ZQI=&@HDFLxSwdxYP-Wh#BBeihr7{nVP7J}OEG!u)z9{NY zCXM2KM430rXhf0K*``;YSXq7D0vhT@O`}J<3&WAl4sHNCj%q z9;G{;LhTkpMta2*#2Cp#$hrcB@QBi^QCgT#nH4It1IoNrMGmUU3pF{Q&_tGJUlF@J zbO6~vAv~hU2TBVQ%DhoV6RNyWMH5OPo-VTumDgB*Kv}p^M*PqQyEdY>P zo9$6>fjSyhfrKif0gV=6*;s!tASrr{+ufsDQ{Mz5TIji9$3^5lAxaZ@V&71fZj{l4 z(yUQM1IoNnM?I>%(1?0enlc#Ch(_7;fqy0x*-%w9ptNYzQI9fjG@>3Q2q?CI_^?}9 z3&m#?*-&-Vt5U~kL_KP&_UaScdtC;@YOlHtM%1Hfm75herZwR8DHTz#x}_rOQC%st z!FP+DL$o~bcJQTZXq4v#7)eIX>O9dMy`y+u z@>QDkY=NIyLTj@o6iY{66%8m&p3Uk}l_NBw7FE79t3mm5CSN>+exXzN6t6f0@ziz; zqAa!T$sXv{tcUDIv395`8dT}hsG}Zb-e^P}8ZAItASX2_3Q~_sv%0dx)|2&+jSdjK zn{~@>6fPmem!hZHg|Z%_j#|_$AWG03csCF&0BTardPR|!%i640R7>hSX>~=6Kqq*FxC>mgT}GR4ovy!UohWAnF$MXtV&R$@G|Cw^!xmHONHr>qc1& zih4Gybar(B-wB|hIgk#o?ONS~=EUg_a)yPYIMpcef6>Y5@h3d-R&3bq>Nr8yA){d-- z|AdP#3_DOWTp2s)*Kaym2H4mgIe(CTx(L9}kbx=^dXgJOK2S$Q3%O9{jYjk!6IEVl zMz>}>3Gq{_UP!O#S{;k{ZkdE?kkqGHy|T4JS#hi1gdC6)hv0| z$$B>s4M1`?>p{8$szx2yhpG<)@ z*Cl_{HNjy=nJv}DPZ=VJ(x^@@_3%1;_!?S_8Ap?<#DGGRvOS740jYkWUYDq&UR7&K zHKHEnqWEP4`hd`{M+cA&)X|`7i_l^9Tp~pueMOQEkdLTGxw_Ga29$(U`31iwlxcN9 z;Eb{wm&K@8RWZs()T1ItFZ@ zU-1(>`;Rk7RMCL4>qZ?7D9cY(MgxjmppGU~>(VRBA61d%qAH8gq-rIqDw$edDzGnBB-4>-mY%BmpBTB+3qZvgyP=b>I z8cdW87`(C=+$%l@@Y>%EbJvc$C99xy4OOFBP)Pp-PkR((v-l4qzFtu6j{q5+P&O!4 z36H9Ya{U=a-l{5pQk4$gdA8&SFwK+Rc|SfJY1!2q`aa_WFu z(0lc6B?`Dj*&WbmmYS*vaO@c(P0c?WCMv6()Sz6^s)*Ry9z|Bo*A|E!R1;-eDchsy zlL0h$MrnYXWCM=cvJ$0%8Rfo8l?Fag9ak7YMKar#C9e<*uZkwG0`P`;aSPlsF0eNi zNi0o(>wlm+gXwivWwWdbPEq64W$|chb^77!)hh(qCS+CCgd!KH${JCfEUHEedILT# zfzrf`Vri>VxJBc>pyIeMs{Lv}emB&~ChD?!6yDHK9&L~jA(jii*-u<<9apQODo$!p zw$%XFpHZJ|8VCois`eFPDhu?70Rw8li2AsOfmzkZ)u@DLuMi8biiT#f8l<%Yj5^e3 z&<0S{j3O;nef>bWw6=h|&>KLCrv<0N+v=k&o~F;^!ZTphWlgBcBB0f!-**7z1RBwR zvh*x#HbAS1Dr!{YzM$me8r}_vYv@ZLlvZ_K-_f`PNMh|7^@CWqKqp{U)w)uR=yA90 zHBPn+c)woG;3^BfN&}8sRa>-y4-{#s>Z_twm3u`4oZzTI;|v0IS9P@UDPGuczWkTf zdJyUsh#gTa9L-`gAkwKaZPknhl-0N_M-A$-c%WUDj&^4NJ;KVd1&SI~o`FO&>QNF> zWm%&EY9{JvPz4*Rjv6!zKd<4V0p8erRH<2N#>-{}s?(&Sy`o-~btB6yaMYnJ+USZ} z)ayc(zLsmAM+BhS=xmpPx1IkGmbv5?u;T&08$Z+2DmOzPT{Y~ zK%)3MqBLmLh$dAcGQg%z2Doafexb+*>S!J38h8m)zrxVy*eM!psKp0 z>S#b!jSYasfq@slcryK3|Gjo}$X%P!kh19kjmIk%bEKoIWsmja&joBNeumWZm1Y;Q z0(?_G9`Hh8WJGDys*WaAE7^dyHaqlYfc}UI98_u0sG|Yp`l%Yz!okA;S54I~6!}0E zO$Oiq$2B^j6*>djETix;qD)%V(PRK%7*I5z1XGpKgfc6yGCHAZK$JyzQdQY(7MA}& zWl*T1NmWutDLSCY;l&?R9qnuQI4H%uF(O|xl8%=*e!KkD5D8w(yEFkluBWM(S$Oc zs$Zyt=v781RW<-8n;l>@p;$CfMI%asQpJ=HRjwK+Nm}VI4EhRTKj67Ui_)S|nH^9p z8mOXK6=I>vx<=JR4NfT6l`2~?s%nqYfZ(L=#G{IIr9- zMu11JM(K4%Nk|pk7YZU!M56(&nkdQMD{|N@cmNJjMJz0jEynR_{S{535FJtE1Lg7) z%DhoVBg!nh?+c?(+JiT*>XlISiVXvC^weNdi}uwDBdkTGH5{2xLZPLU_xOpR2hw^k~V<%5#_4(%BV&E<$wFrU;T+M z{@(|qX3Rm<&e8uVF>Racla+WP#qOai>oLQUu(|lG;uJMqgHob)J*a{WRjxm&Vtrl* zXfa|p<|8IRUPqK(jZ$+)xffhkN9+UT!8HnS@X8$YcysV_gu?0$tS7x{*TEI54!ojj zt5mtX^cz*yVL(PF6hhj48(?oo0|waB5v2hGG%%uEk=5u7sIJxkbOJ^6fwEar)fpVi zVh1SA2>==4<#$Fpl=;_XiLwI|styRS(@|AdD?2c&CJIV+Y4Fu6-0>Dd714~cJ5=)) zIOzaf!e`T7PlY`I2sHX;QNe1Fi=({{Z7?477p1c!T{e7AxZ*-=BhYH4T>cL z<>E6+uTtgv2dWE`UNxyR;9C$V$e}DhUU^}BTo64PkPmpa71BE3jyjZ=z$jN&)SzfU z03=6LCmVzf&`a-Cy%Gx95v2hGvihM)H5$MSM}1iV@XL&{SyJWxk7(TO>;O#69T4E< z2UHyp%JpGlR7IKq-yKaI5ULI+>QEgQs;UDM3W!V?aMY>#YEe~HaZ-osxTJwum5(eL zV51y0s@^Sh*ZT{;HGrkjc%d>ophyL()jw3>F;pXJyaEb<>w8j%YPYBgX?1og3rret z)TwH>q$*8D9je_*1GB1jD^OL|s$vVc1Kcgvuc$LXuL3AJquN-i68l0~i_wTW1HJ`; zVh*APjmIl5j5bRTP2B`e@lS;LcQsMD&npXi5smK!zEe_l4_cI`#ai_Fp~?>F`Kn%h z7)X@88c-cq0W>h8@x*Xhs%t7M0Dhs}0YyFxWOV_+ z;;1}Mi=W!OQY3s{9knPH4K$+;r9Go7>QI9CWdn{{6zM=S>QEXqx}px{`l%XGhjP_a z{X&rsG^0+H9F(I2idvLK#gj0i4wXNlE9y`wg(}n;b*R#z`h{{`qZxIoYCswwJQ^^d z{hd)7OamXPJOhD7)Ow{^Ki)EGQ5Xm`qYkA#qburAfc(Ydl2M1U0jU~Mi)vk}VuB}i zD6$l`0Y@FGMTM@YMX6*oqaLM2dyS|==@m$LRn(z$Xmmv_Nmp(1?0fN<~?Y z8Wa@G;yX}8m=v#LM*Q1Wwlz?hP4c|s>tDQUB&-}0(xKxxpZqaGz^G@>5W`k@LK^V;3gszM_gP)Zqf z)T88lMk1O}EG&cc$#%6~RliYSBT9o-jc8CMm_DJ!Frr9?YDAN&%Ao;F`A|)iUuTr-suubfQ8z#xP%DNG zV9}6@s4r{R648WGl=)b{N6F#wipPs1-AHX1pE!Qyf91}y6J@s+u>$;+&hdb^s=Bp^ z6)coit*U5HRZ&764XCQZ9}x2aKccK9y+V0eT*2uzP;wJWhejPusyYKV$Q zH2q;9P<)xuID>4KPUGO!tI~j@3FV^lYS95@AvlCMrH=N6d3FG`B+6()S-4dd4JfS| zbu^#^QHs1Wnoy?Gz>LzMQAeXH5gB0l_|+a4ttr&eghD3_C>l_3SU5XCx;4O}0#!7i z&T-Oxu8?K^0PoDjHBVAPsQ+z5`em0Gs7#LTS;cq7mh)QlyV(FAz5iqUkk0%c(nN&`k!|9~=Yl+mn; zEczs`5LeWB)ouw@w`K#OD#=+DIyS)dCzPui)%qg}sX!?@q3jQic6LC~)B&S(FrmnW zDx(qA{)DRF{Sr@_>(fg9YeFf0uz}17*a{a{1TiE7FO| z?1*w>3B>xnDk-|u-Qw2SWVN~;@O)$i>gZuLQCc;sZVjrkDpd6k29OU`kgC>1@aIRosI0f|b#L4j#YqXV?gm(Ld?efHgA2Ly0^ zM-58K0HPUH2SSyyg8_9wfI2Xu?0`|ckE%34##`X1Eh|wPm{B%Ms_erDs%r=Xf-W+j+H63gjvo8EP!>LUPyn*3 zNev2BspW1B29OF=UnW&tK%HnTN(U3lEg+=bim3O>wq^$uHK;lu0BvhM&-HWtP;B6iRB3fUbp{2frU{J;n_gjdFuE)S@()21YcFYZw?&e}f5Ckc=7waR#mWg)&bqd7f0gTYOS!2D;H2 zV6)h++^rF1)kZVw%L>$elp#swYn=sr0rj2IQsnVd) z6?G_$rfNhTO376HLXi(NqfQkZEyQ_M)S_?@Xht0hEYKBoD8W>Xs6&}Hx}p~4x+;r4 z6m_T@pbn@N!x_M`kRrOGPSsTjmFY=UqDCp-qkFL(f%a<+#a~wQ2yl#w^qt)KEn%VX z7%1INDBEe2(S))VqlyNUd83YcRC%Eh^{6yuFrpESvgrf=OenIUs%SuI(Ws*yW!`8+ zJxUNzYyt6Mx3U(B&nU8?>Zn(xj?svE)K={^4|%xd!SKufhqkxDhJmv_}QvkLY;~b#ztt(SZD$QuZ}bmKF^Cd0W2ISqkRijE1;AAY9UdYolxej>S$60h~08o zItHWHM18h;6zc}6XfQyBMjZ{PtcF*g*vSCoR90Mr7PUd5jwS z1FB-MQ&|=xz0wF0`Imnv1Wyd35FSzF1EqxtW!@;G2~}RGq6wuCb}PJUiM}kHtw75) zeCYs$0%b(wohp+?6-_9uVq@hs&TglQH50Yf(LkVKwMTXNY#?sTP!`mL#`?Xgq>Qo! za|bB;yoO~5*4^T1K}M2_==L4u4j9!gytFk{)hnSg8**=|ZU9l2)uYVYfJs{6>rIs? zk3p2hs7Fy&pb#EWBm<>|2}M3onH^B(jfxyq*?uasES;F4EG!u)z9{NCz@$;Uk0|p- z8I35iJTCHjUc-u?NbOexMNpNGRLs`2~N9e&js$L0|SwpX=8$i@$^(gXm3BcrsS8YR-6}RBk093UN zLLH4|QOieQQdL<(-2iXwn*oae29RReKwVaY{{CnE-|YtcyohQ9E98&bc*Wno`B14a)}`D#O1A>!c0%P=0N!F! z*8@K@*aLvX>8&+jfCfgC1`P0hL~%fvrvcSJ7=UV^_!3d$)!*c)rJBaFbo{RGhj#;F zw|oeYq+|Mh>D5N*(x{_HTNlb=j7HR=%p1+9L49S33e=>>QEabx}pyC<+m!`BI;1DYSk}P zd7&9Ks$3FHz~zq!lj3#ESpViwrzNhg9vNoeP%Mn3)bW<0XLYGci$-O3Kr^rX9aTk2 z)lqL?=OgM-76YrO){*)qyGH}!I}8atj{}8tmi3C_W(7(U6G|ncvOAzs5-M^~wGvU2 zJsL^?g6vVX2#Swpoeeme1;s=e>Gh8C+niCFm{7LWsO%0X@`1Xr9@UysHQ5_bUaCR% zD4PZH(X7&d-7Id@-K-A9+JP!!VehDZ)DmjrYQZb2wo287xmj;0m((8Bll6j9$*48y zny(i$NMsQ4Wu}s=S!`=|K+!|=K&`C?)ZN=G_2$r8xsZ z_Gpk-v##~C0~EcR)uVJ#n$@CoY1Gl9s%1d+2#u&i-Bzj!q<(`&TLA>wqweZ;4ezSL zYwUe=z$a@!v38(}u5%6V`3Do#W0Zbhs#>V(5gJjes=N$j)S%H;paus6-ul|CM+59N zPs!P=3B}rHvj&td&t~N%U$qOP21Mjh%r4Xmg^VUsWHrUQlegx4`6eGl}yz2RP-VPjmisplSYFqULRzjYE1LSN10yg>(S_^ z*cvg~2y$3EbEpm|eqxW8RPzHh@|ElAzZ%-A8-22v603X*&tTxQxy|V)nm83RwTDHqt~)t z$=43NlW%B4zMviXL|gKK_T-HYq)|7sdB<*9Aa`qR-(zQ2CecRHidD5mwTjrKy4JZJ zti(b)SqWBExUwb8SwdMnb$qg+1qA1KuD+RfTCLWJ4lWNq@0enmgqx>PYe6b{Wbb{ZgNw2(RdKt<`Tl26one80#i z3Wn=@2IHKuM-c7vx|_AgWAce^G9|SV*Wl|w_won%s)|YY#n(yZ7>1WBF{6ciK}G4U zk}oJ125DV>h#7l;(Q4MNYmvv?if)PJVh^3@cU#lIUVcg1Kb_;XRT0HvCz)d>O3Y{> z-_RgK7@s_2e^!*u!iSv+?LBazJCQE-NJaN}lE*S9`V(!9zWz*GjY2=xUyGv+IhIj$ zKxE+Ato_l^f$o&G_vahknQ*ZOE_5f-?;fe>9#8VFDx0;)1wI;(%}VqjJ5{#v$ZVQAwkT2~1 zl+i|WB(C=Un9)LWpm_*j`x3p$X9E&_kS+QoJCw%?9@m5wtW$;b@pIPtQ^g_pj$-RW z?9g0erz#JLnL_6D1J!X7RLLjmgGcHjkI(T36EMbZ@_`0v?U)o}{(|@O=d7=`#v=o> zKHIubEFM0K-Th%1piK|&ByH|biK-wC?;Ob|>e5MF9u8*&|9Lp%Fxxa%C+lT6!f5@Y-H7qo` z9ba5_64!2-DdZA+Ln}F<7dfCe*`p7#MW1Ac#+|DZqFeY9k+(olB@=iF00*&%(6$@sFG_4+S&0KA}G3!dm+K5{bkrrNjQRvlV! zp=y-g&edVz%>bS4!m@0#Ir;p~y~)fPn6ib6ZG{&Md@v+5PU(c$M=hTsG6jKn|z=Tmxn$k$9zAtB)b*Qk8kKj zrq&C3lRf$%Tl7gb=Z4-6i@B5W^Baqk(}8Bjmb#{@P^)Gk3Ps2eUc42wBYjk z{bs^9{W30|90lpSbW zAWE|i)Ps~uZH~O5Pg2+uZCmg_`xe|NK6fp+P<}L;1+h4nbfFr5`+Hq*M)_qm>-FD4 zyrW$Uo~msN9w-Ky7ThR5H!ZkOeH2=o#kwz4&1zZ@D5mUYH7$5SyB0iAjJ&ttfpXxz z1vjeC?=84ce zLkpauYn_4k2*FG9QC8-c085Y89@D>%4Rntt$1TX0{}rRrJ(}4{>bwg5Bp3QkCi)X( zpg%(z{V7uD(fB1S#oCcInc7g^p6SqF1 zPF1VQz=}@PgZy6u)Qayjji^K6G*nmAp*n*+BtFB83c7ldqxp3u6li1D5Y+hU(EtRoZ1_zB)5$U^ubOjt zJyq2JA40Zb*e$Pb15}+2sI&Cy&h8o?X8@~m*?1652D~cE%4l`&QZ*p2LT|5X`_cNP zvl0s4c56V-zQ%dcZqdzk3)~n~eqKm5i(_kzVnCxSRh|0hfnq>y1$d)n>-s zQo9-h^7^v|xFi+!{Qn&s0EhHf*c6-qPU%BfilwGSfi8bsl{fhEVY%< znpwOa=6DXT7tupik`Rnrz-Z06P_~u-=wvx6=vs)QE3-y3s9vd-na9^x1G-zXa^J0^ zEO=edfr!>JmnsekJB##+Iuw#%)q#v!)U29i-CgHpAV?^!s8xkisu7K-L$yKjx}t*e zyNN{3)3C;F6dG8#qA^y`a|`59yOmKv*KV)T6|5A3t646Fsw-O4i0)TfS?Qg!>iIch zun%0S?iCuJs+h3G)|AVu0K5gtsGxp8Vn3^@x^<&zmSPz{zt#@y{BfysP+kYAMh{Sy|>`p&NxtLa7Kfwt|~WHqDP_O zRaWc9YG`<7=`n#C<3YseVPFkpfzPj32Usky};k zY6~)28W&1~bgRqls7005b0DLF`fjm@a&2pR;Bl;=1@NWTjTK!{-gz3V8=GUTDji~; zPnMz%MUt#K5K)IJ&0wyvhs43VNv8D^*w2 zp4rOtD{E})!tpVoon`K4Rp;lrCR#Z?` zs}@z)+OBpB?A2x2K}Dge4X+!UW7WX(;kWWD$ZwpBr4$whu%ZP&pM+qDa(@-IsA^HO zGAig={s^*d3yhzLyxq`B0CU#Zg6UPwqOpo%fMW%{wLpX_qZU=+I$0TYsLICX`MB^? zRXqyNFs1S<$D=INn+_dq|BJqMi(90+^=weoqGEkxISWyTx-6d86?G_u=zu3Hq7Ic& zyy;}o!PTr?ZT`SO1Dplr>NT5revRpC_2}!V%Kq?>=t-z((T~2Wa!e+M--B0H0z#^e zit6bxV&)eUV|fN>@jBYHFdS|6hrigYh?e+WmW~)v1~j{UqyY|NegLPHqWV%6FXUp5 zvM`)4JJc4)>rj>r5M9v{f0P9=_$C@ri>gB^FryBYqVqi8Dw_2l=QxLs zudijf11#%q7H_9sJbDrBUcVavc`SH`w*hUJo5k(Aui;)yH;N{Fw-l{~o~o4MZdvp? zgr}>rcXSV2!f%c`##71X{^d)Zi`94qLlit60~ZpGLER?mO5Z;py8 z4d4af)X%Yko&XocFWmx19clyYz=}GQinPPsil{@C2kYYq`+c)e9MbAQMx81bC#>V* zs6*LG;yQ$m3VI)Re2)CWh+OB@%d1(IKQ1xRcs}Vsd+X1ATgsPeoDr4;^zUc zg<^o@YmF7v%${F8X<(lszawK1MDBr&k^=PGW(Ms%n&tDJ$C33%ZAO`H1@( zD(X-!&R_1ZqJpaN+{UBsJyy||#?sV+c3%&#?y9aKjqpOQ3GOS;%5}2XXpI&0R8?6z z0~vKFmAJAlx1$q{cn!T2sUdnT2D~o&8qt!tP%Y06>xWX-RXcE~(jL|1)lpH^DWYDr zqF(i?cIakN{c&M9pH)=V7%K)IUa4x=x9W+~GWGK(&Edk}hwmR_atM0~SAjet*0J!_Q1&#{Jqrs}m#;&o7KKts;Sk&sPRJma~dfK{U z-xlvjF*&0dVOqRyG>X}PPMZoW=mA8BkY3S%QVNr!YyEDqCN@qN(os>>mE(>db?>o) zo?h7sPSSl-)S*lgjt(;_C>CS0p2tOF1+4}sj1kLUs%zR_D|d=tm(XI zqbj6VR8T($*!Z=Ww}7>7SC=YlX1i!0qM~|eK_~jUq825I-|(7IL3uXyPxTsO1w9Pd zp_?V$>p^s&c1UzZMU~BxL^Tj&H;Nj7vzrm^l}>cU$Ic&PYf@Zp_q!U1u{G=7t#F`? zm6y7)IsRDh7NzAzM_@SpIq#@P-$Z@_=s?KDj#u&9P!&b?(@L zy%{aaRZ$_2c0>hr2jHL>Ajz?U9tJFhy8R$}?En>OS?U$WT2(E|Gp3eI23(460hht= zR+X#D3NN>#Vn7>x^2DMp!zDSw*i&_iRW?A*j1L= za-lg^&{7uHwSkB_G-|=*6?G_UCZyxysGvH8gziJAv4S36y(|h01NRp2a;S!?8e^TR zy;5~W1*KOBSJfCR=;2kHhG|r#f$44q;gdzS9v4*$rZ!8H9vvXYhso)6jm=)&0X6F~ zaFi9bU}Qz7s^T?pd_%ax_+H=*J-xC~_@_6(;so$VvQLyGx4>loc*C-Mu`ItXRGUbV z(Ka>Ze112iRiwje-z=8T-?}i4I@KVNUQt2!E!fd6 z^+H+g)hrEgte{(g=ZPyLy`m0{~^t zcmY@`#tM3L0OoAPN1LV!>YZT;=Omit*o~q!kgI5n6|`!pT`JH~hq5@ncnBjZD7|w1 z+pEV4`Y;e3rozY3W{dcA#OtjCTqX&y928B?yG!YR&T%-<<$#Rlvj?wO0(8jTb5Mqm8ws#-WV*)0Kj<~I#rbqS{n=5 zdkgZ$RM8GQJ!S0{dx7W>V*v4 z8%qPe$ftge6$3un)!`m1=&6Ne*#lm~hzja%B6rli#|nC=vZ;KZVZlSoCyQf6^=KBR&;dqP zR8ThyF4#>Xr56P~RZUVgqk{7CAz{^s_Vf#deIR#P9xLcph-Im71BeRhqkWxMI^up; zw5VE5=T(JORA-aM&Mly##;O6e9Sff58Y}3-fXkwlM_C-Av8ozlMb)S1>Hz1`Z!POI zz&!QUKt)egFqmQx(Vkw=Jsc={v7>_WxY*Z@_VkKI1?RH%`nUyHjE$+gwZ?8$vK7?; z#|pZAWe1RsUR_6uV+B3DLP|~M#zxelmO@&NFs*ig zePyN^$g!g8#&Bm2D_Wmp1w8;eMB~Hjy#+MDGk6>DSgRVaA;wVOUi?Ua< zSTkQfB#H)AE$j|(-l1O&Q0D^NVNQCWva2m{)EL;qJkXTK$ck=NdvhwIF*HXKWNo%ZnHCb=L8mp-Gm35!0HhY!jLjsvNE{yi1TNR~NK)a=} z3q?&JPc0p7jTLk+=6i~H+%1ClBSVh|Zsg%`j}=w=Qp4l8RM!{k=R;A&+L-b%z)CTC zm*ugddX|MboaXzWsGur=1OYBk+E&nqs!o=sJWdwsX+f+sE zPdiTz^A7zBWtISU%TcH5e9`i8=k%hw6}$zQ8JoeVpnML<&r@qzpvVp}sH_v+v|=Bssjh+tb31DRIB6dJT7bOLR}Y( zaC!bZCRLP+UjPkwte~YVOmW-PY3LUe3drK^Say$96!y4&LDyJ89|kZ9ebrj`Gs~jS zzOu5*tDX9|xSGRtF_1U5c;ytDxK%O4%%P?Grm>=Wmc_2(#rxpbrOKUQb57MY)~doD zU8-4*3aYay;Iu+nPO2!^#|z+!_M{i|@~TN3yU^Hh-dJR7+bYWCX{~l3#wuzld!=Y; zTSd7j|Ea1mR#EE6VLn|>D-|Usbhn5b>#-YEw{HXL_SGyXP~%+I$Ax2;Dk|WwQdW*# zC_4nWpgC61vlw|{hh-E3w*h;_{BV8h7uB~X)gCM8!+@UyTIxQpEQal7-HDSeyl6-bR+x;}4t`ybX?)YYbVs=zeJ$|%X$0T-7V-vEs_ zR#hRR)*Q>~yAEr(PL|e$?uo9ks_J5Dv({Keu@22*a7DXq7b;L_MlH&^@ayy%xA1Xe zxjNv2=2$flqZnLKYkd5~_j}0xT1~^tx7D9=t z8e&Ja@3EJmFw1&BwpMwDlTecf8T<{qmCWXk82_89F+ z7aC@H24tr9Dk;dhSzLHfMHa6E;MMV1HQ-Sn7a8ci3dP&0y2h%i7n9c@j!74)9dKFf z!B7@E#NUUO9-11fsw4?(V;yx{z)b{M%gV7!l`Q_L24d_&wZ2c5%^Z^|YLZ@8)Oyv? zx(wu4Rn?++iw-bqRQGUv-_j(MiaE{YKDGFro5pX{d*zK)JI_g%S4@Y-)z=uiQ7?BC zlh^QJfU5W%ePy&uy;NbJ4h}$%PmNtDbTq7^cTIYrD!iz&P6)g_G@*4mR9`iAsd9aK zl|w~cSy~Ej>*;b9c&Vza=N4f0?N#MlmE|+)4CoBO;sI#4Fz4PajIda^T2ZH}Rc(Ol zPX?k_?0~yAd6n)7(2D-KcZ+pl;j1i<)xNS)p?<*ENfkwoWL3?vjsD9&{vUtREB?<& zX$97YIP6Xqh6Jo&mGoSRb_|xTN~@BRSjeHG}`R7ThL?)>Oe%T zsvW4T&}z}R=G8#>uVuM|_XB}lc{~v4kA8Ks9CZflukO|wdl*m;s#mOq)vjiFc{XcB zodMMfYCXKpgR>3%{%2kp?Evf*3)~fsZP+N`t6j9pu?H$)9YaT*TeT)S3zAWXDh=cS z=%4zxR|#2_lCvrscHe^-t7TD&|E%ZBY2`xUK+F1BKN_GW+r8`dvz}v@DkbSv4{$|$ zQbn;kRj;R3j6F~`07{y}s8iMI70?fgntrK*r30M-M}sPjsVr_**^H{{bOHR$jFTz~ zAxf#Nh&luG$=|vUjs}#XwXYb_ST!I~m{@mq>Z{6D2O=5_u&mpF$DRf_ZUc&XRV|A& z43q4=A`Rf`K#pAosD#&Xp7OXncgqqdsvATrw`!ny3wp1x$!fR-8MPe{SnBqDz{Jad z8-xzqjAjY1mG+R-6 zdh8Ythz^M^_jp|76u6Ey$jK{L0>LeasM`YMeMt1k_%J|C8;Gb=<)UdIq84Qbz;Fv9 zYEeoV&8SBq3fZy+8hU%Y$*#_Tqh6H`uZ@Kjja_Ge8xUS2>QpJf#;$94y1rDk)_t_O zJjQO6Y&j&m!#AoL&SiNYH2+d{RXzhmivF#NEM8>`yvNV)hIFd)iYbb^W@$|zI@*E{ z{c3>j@LPS2s8jW#LbW`i4z(!C@*@MnElR005K*hjPT_TE>G7$tt1J~|uT&qrvIG2w zCo7`X0P6y^uHn!DX$sA#S7ia^kf?1MyUJp#!fQl>s`hi;*vYH3SQe|pucO1&fL4dw z1ISzOJg-#q8HlL$$`%>Ts6)db(ktpvc?|=UEv~P!C>91H>QtSMRxbg=*G- zy8bvWR2{bfX*{9xZcQjpeyJOiV(jwjZn3W!bsdn`XqMRXG~B9ElWIhrs?$6!E9y|y z6dlkG3?1-!f)aQMA1C+4tI85t+g4F`D7HYttt$NykGsXFD=YsE>{@GoTfywi>L++f z@)~kGVYh7Ynjilb7X&=0ua1`1Uf}q1fl!<7y>eA8tK0u=07MvIG#W5U0~4zC*-dUN zehqz<5L$37tG4l>dv(BzMqjb~;FT!Xy;MC`w}1{QX0M9c4sbq;$y;!`uBvfLg=&Ew zwNt9Ds59X8jnWCC0cD3yfTzJ@)vN0--OMexziqe_8dyQ(KLsu8tl5UT^j7I>3RK>J38`*LGd{!&@9SCd3n)O)pAdX1<>-B+ZsI)sOB z@{yMTk^LE9QAE@%N4)`Q$v{LcYS}n0Tw*)}0(f3EZ9vteQ!97tz6JD0H6Lw7omU?x zp`67@9cqJW7A3*I#g0@d^`!KGk_(z^xD|LfL0ZnQD=aK zVEsHUj9S!Y^SF$t8*i_ehKE|Kstxe>Et_r8{8>^nXnbpC3SZZckHl7AdjqOU9az!U zMX`S6&#w@*SGBEIwMU_n9Xr51$SqLR83>127Oixs`h)Z0;{w$YrLfO{qh8h3#5Lrk z2HnH^!tCg+uVH|lYgPTEvR647(A>JURu16ncBhR!G7;`c72Tguj2-Za5Yd{o523s| zJ$UtQWe3oLwgbfgr*VtDKB8jafl@!L*6&+u+OrXlW))QyW&;r|C3fI}+JL%I4OEmz zKzEmyjZsncw_e>?CSl-zpjoQ}m{e3xuU-`+vHoq~*`=5PGduU}z$(j|Pz~hHocDB( zwO*---?6cbT9my4%d#SxQSFvcL@laX`1JBEnEI-A#(9N@;k@#B#TRaBM!f+wUj`y7 zX!wHGu{Yg~jm}h5PHG2^PkX~(q94Ei<*)zp*Z=R2|M=t2fBYNiY!koz@DQJ+F_lBh zyvBaT_p^Vqo6j)~sWoblu+-ubDX_G1;Fn*QRvC&9Iku^_E{B*-gf2qs8q&u-meeuR zS{qqfk0A`4W1;mJ60}A|Y2r1ck2$ufwSp59&dk4(j2O$D#H*DSPm2}Z0vfFM>t&T}I^QhZ2y70BiT)3bQfR|@f( z6@yyQ>)t7?=ye|{u5zt)uEOe$wXA}eL%c?!X$=#;J?49Z@5R7$mm`Mp{Q(i)cX zgqRkB{FH*Zm{M#XocSHl*+WSogUO+Wv}eg1GS3u_>k{14Gz%4zx5K4qhZt6SIb2gn zY{8YYpc-WxdzuAxZD3GhspwhWL)%!>LQv~R=X0?TWGV$qitS@vdIxm$5H40K=R^;Y z*r}BZhg{2o3@FK;0r>cGtapz4fu+=)1BzcxT{)`6{Zd3ZE2}rTmhOliK?h(PI?~8% zR!ofxt22s>7vW48)hvu*(C;~CrwD3A1d;VxT4WvUlG0&c2m4H654`Viq*oQ-dDzgoRH=pDP1CO4V$au;r6PaxL>u0ap&@2 zhi0@_=SZjb>O77pZM-!KOJQ1Gz4RD@Oyx}}sq%2hOq>nO;9B0%EX;x!UV?QNC#1ub zi5^PIf_F-Nu=y+HHms``*=Vmyjz;A?r{pkZWhQOxC&0=?O0#mKw2!Dog7|=v;~HSl z{fM>r(NY*bQ|yFDWh1j}FcZ^C>UF7{75bc)lQQ+Plv6fwEfuMhL3Zh7Y75?}ow;YB zBqdE`);-h_jiI%iQeHjg)D%A1`62sTl>D}oQ?EtvQ)qvmm#V81*mLbv{vQs$BD$g262qCi3TvYZ@j3ILvc^ zFI&%9^--yV61yDc*E9uZqcWo(?x7oNu}Zw)lfl`joq43zoX0E(?Ia@qiXQGvjAKBl z@uid-_#^3np?d1O3^ z??>ljnUzC;Umz5jIa2X0k5;_bdsFgQuN+kHi)&$ZOJiLzZ&jusgcFwUJ zBK4Aq9=>Iqdd*~AX~19QSZl>3|Cvbd%CY23=?7!|kz}R(mjem#$K#dCLH(qSj2{)U zu~VS+1OJ-E?^o;S+-p%}&piY!vQvi*oYpOCWukCXqB*Msc&cDI|co1o^eTWt!?H^$p&)KYpKmkifBha;BfwU!6(RJ60Mq{lMJ zpi35lZpQg;Fm1d{%T$$2hnVm(XMcAnS+Be5vN=y*si)dXZN5TFP{Sp+QasWnvv(Q8 zHM3K?2qn1%PA7e@IbP-z`x@ar1nGW?nCCSRwYzK>D#oqmP(x-sWnKs#MdAO zax5*a&s9@yB6m#R^cn=YMmfkb)&NB@h|gsx2Cp%-?yxOK8gx`1AYAC0uhp+H{>$pW z{Of=I@t1$iC&#~4_CRR%#~=R|_Vg14-Z&y*4dZNLWAJtj)5`h@mU^VcY^6H9l&;}a z%3;mlN^5wTkexk@`KDBild$;aha;CX#$2Fs9920Ac8-yHf^?)9QPZtLAS*DG zk1#ft!|N?*&u4~))EbLylF`xzwx_UTK^Oc*oAQfh-V+eXp?phNxiXw1nzCs(JLYJD zdvdBA!>7tIe5w%1#vUr?@S$=JM^89O#NLLb!*LAjGeW#7y+A1h9dgo4+*Ph2;)`BQ z)z}`!VryZ|JVf*v*@Mm@4j#j&#ba1>Oo`z=6yqqDOG;tA?GvkhkTw}v@&E9G#Eq@5hz-W26<()gTz?pwZhE@}3L-P&(??8WXkcQ8N=dy2Hne96V| z0iMH*V;dC(?Tyt)4r{CTNDiM1$_Ey*$Sx$tHN5LcN2VX+8cxN%$`&d57J1-Xq@+xz zfhB&3oVbTgY201FFh3n5yC;kwf8!XF;uP)-zW1av(0 diff --git a/claasp/cipher_modules/models/milp/utils/generate_inequalities_for_wordwise_truncated_xor_with_n_input_bits.py b/claasp/cipher_modules/models/milp/utils/generate_inequalities_for_wordwise_truncated_xor_with_n_input_bits.py index 66e61033..fe9f80f8 100644 --- a/claasp/cipher_modules/models/milp/utils/generate_inequalities_for_wordwise_truncated_xor_with_n_input_bits.py +++ b/claasp/cipher_modules/models/milp/utils/generate_inequalities_for_wordwise_truncated_xor_with_n_input_bits.py @@ -100,6 +100,7 @@ def get_valid_points_for_wordwise_xor(delta_in_1, zeta_in_1, delta_in_2, zeta_in zeta_out = 0 if delta_in_1 + delta_in_2 > 2: delta_out = 3 + zeta_out = -2 elif delta_in_1 + delta_in_2 == 1: delta_out = 1 zeta_out = zeta_in_1 + zeta_in_2 @@ -107,6 +108,7 @@ def get_valid_points_for_wordwise_xor(delta_in_1, zeta_in_1, delta_in_2, zeta_in delta_out = 0 elif zeta_in_1 + zeta_in_2 < 0: delta_out = 2 + zeta_out = -1 elif zeta_in_1 == zeta_in_2: delta_out = 0 else: @@ -169,6 +171,7 @@ def generate_valid_points_for_xor_between_n_input_words(wordsize=4, number_of_wo zeta[summand + 1]) delta_output, zeta_output = get_valid_points_for_wordwise_xor(tmp_delta[-1], tmp_zeta[-1], delta[-1], zeta[-1]) + zeta_output = max(0, zeta_output) if delta.count(3) == 0 and delta.count(2) == 1 and delta.count(1) > 1: only_fixed_patterns = [i[1] for i in enumerate(zeta) if delta[i[0]] == 1] if len(only_fixed_patterns) > 1: diff --git a/claasp/components/linear_layer_component.py b/claasp/components/linear_layer_component.py index 71dd4efb..fea07e44 100644 --- a/claasp/components/linear_layer_component.py +++ b/claasp/components/linear_layer_component.py @@ -607,10 +607,11 @@ def milp_wordwise_deterministic_truncated_xor_differential_constraints(self, mod ('x[mix_column_0_21_14]', x_46), ('x[mix_column_0_21_15]', x_47)] sage: constraints - [1 <= 1 + x_6 + x_8 + x_9 + x_10 + x_11 + x_13 + x_18 + x_19 - x_25, - 1 <= 1 + x_6 + x_8 + x_9 + x_10 + x_11 + x_12 + x_13 + x_19 - x_25, + [1 <= 2 - x_6 - x_12 + x_25, + 1 <= 3 - x_8 + x_9 + x_10 + x_11 - x_14 + x_15 + x_16 + x_17 + x_19 - x_25, + 1 <= 3 + x_8 - x_9 + x_10 + x_11 + x_14 - x_15 + x_16 + x_17 + x_19 - x_25, ... - 1 <= 2 - x_6 - x_8, + 1 <= 1 + x_1 - x_2, 1 <= 1 + x_7 - x_8] """ diff --git a/claasp/components/xor_component.py b/claasp/components/xor_component.py index 50466b52..ac108ebc 100644 --- a/claasp/components/xor_component.py +++ b/claasp/components/xor_component.py @@ -802,6 +802,9 @@ def milp_wordwise_deterministic_truncated_xor_differential_constraints(self, mod 1 <= 2 - x_30 - x_39] """ + if model.word_size == 8: + return self.milp_wordwise_deterministic_truncated_xor_differential_sequential_constraints(model) + x = model.binary_variable num_of_inputs = int(self.description[1]) @@ -845,20 +848,20 @@ def milp_wordwise_deterministic_truncated_xor_differential_sequential_constraint sage: from claasp.cipher_modules.models.milp.milp_models.milp_wordwise_deterministic_truncated_xor_differential_model import MilpWordwiseDeterministicTruncatedXorDifferentialModel sage: milp = MilpWordwiseDeterministicTruncatedXorDifferentialModel(cipher) sage: milp.init_model_in_sage_milp_class() - sage: xor_component = cipher.get_component_from_id("xor_0_32") + sage: xor_component = cipher.get_component_from_id("xor_0_31") sage: variables, constraints = xor_component.milp_wordwise_deterministic_truncated_xor_differential_sequential_constraints(milp) sage: variables - [('x[xor_0_31_word_0_class_bit_0]', x_0), - ('x[xor_0_31_word_0_class_bit_1]', x_1), + [('x[sbox_0_26_word_0_class_bit_0]', x_0), + ('x[sbox_0_26_word_0_class_bit_1]', x_1), ... - ('x[xor_0_32_30]', x_118), - ('x[xor_0_32_31]', x_119)] + ('x[xor_0_31_30]', x_158), + ('x[xor_0_31_31]', x_159)] sage: constraints - [1 <= 1 + x_0 + x_2 + x_3 + x_4 + x_5 + x_6 + x_7 + x_8 + x_9 + x_41 - x_81, - 1 <= 1 + x_1 + x_40 + x_42 + x_43 + x_44 + x_45 + x_46 + x_47 + x_48 + x_49 - x_81, + [1 <= 1 + x_0 + x_2 + x_3 + x_4 + x_5 + x_6 + x_7 + x_8 + x_9 + x_41 - x_161, + 1 <= 1 + x_1 + x_40 + x_42 + x_43 + x_44 + x_45 + x_46 + x_47 + x_48 + x_49 - x_161, ... - 1 <= 1 + x_31 - x_39, - 1 <= 2 - x_30 - x_39] + 1 <= 1 + x_111 - x_119, + 1 <= 2 - x_110 - x_119] """