From 897f631910b9b217174c59689d9648585abc037d Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 27 May 2020 15:34:58 -0700 Subject: [PATCH] Fix reference semantics of the signed bitvector primitives --- docs/Semantics.pdf | Bin 231569 -> 231550 bytes src/Cryptol/Eval/Reference.lhs | 17 +++++++---------- 2 files changed, 7 insertions(+), 10 deletions(-) diff --git a/docs/Semantics.pdf b/docs/Semantics.pdf index c7078cc3bfde5159b87925f912c0072722d2fa2d..1f71a76b24d721f8a6e9f2df6c187246e57ac947 100644 GIT binary patch delta 10919 zcmajFQ*b40(5@ZZo@B+C*tVUCZQI6V#kOr5E4C-j#I`-Lv)}Kl|3BF$`{b#syZWT7 zx~seHei9Q=z7kLxCbYph(?vodX%dy7fJMSs{?D2X3fYSu1K@#mGLMB_Eo%zRTke&= zt=izDiz!9IVyq5#ZjjO^NI1#Tbsh^j<*X+`&2{gBz@NR|I%epST;8Ctl)kG!E5JomxLtDP1sAEpBbhx)fu5@5 z8*xbN9`xK{t-e^7h)XWQei_49gClX{^n#P5R)|;@=51s@aX4)md!l&bOVdPgU z==DtOqFgV^(QXI;6GvzoUi;8};BKCEJYE+@BT1LIvK5VNFLh2i4=S1S_f%-P8atJw zKIL-Wa2Y>puTP;37@34gMV9s%um>jdhIu`(pkjdX3kCSIxoLHcO^V4uXS+h?{trsz zbt%LlGxpSk=(=|n#SKTJ?;+hmJ?dFe!YFZq6NQx~(iN-RbYiI%q znnVX5Hv&B+KN$`GuKsQ05%GWq>zi71`(b*5f?8w(m{wETeivO4!n~0oV!ABI)H>~Z_Wp=s}ltYxdd=Ap|A8+BixpMiaUjYom`Q| zt)Scv1J<0J5PxD`Nwh`ZC-S1ANxJ%%@MI=2;~&HOpObjSi7(OmmJcnfGyEqdUAEJdw?p9?$VLQ;G!^j1 zK`B%TOgaxla>8Wga{bq$RnlDT5c`LhI+ai~v4$zQ~n2my7cUM;FCxr`|q-clCc6R{_(SF12TRu-p zy{)6GqwHxc*!6Je`r`);qmgo-EYdscojiNL1A9n-t#+tB?y7rqVI%T@W{?1^HXHn; zSB}J>S8r+OGLL1Bz(OjSC8@35w_Sg0?4H?lcPhC&K52JMRgw2&71Au(I&kec!}0vb zj`(F^>|M~T6!+AP^*|vq6w>jO68$#>Lwm%RjZEY!gN-m!Kr<|2U-32ldaj0F*G3cK-GehjIR_(8EASh)eycIjQEcUp+P2m0x}^*>8v= zc2Z~8P2F71^oO~_T?4)#zo#7uyVfj=14G8xu@hDqL7P8}`b2fTouWA$Ygn*=#ND%` z;>v(oJCA{H@LjW!H&6ed>(PEFuF+Ng+-+7GJ-bt}$Va(jk@j$-2)NvBWm~pnA5f!S zb`?7LD`DA>ESTZH6n8#uvcNJuWJ&PUIF})Y@PingVmu6{6up!>Gu!LX5vUg?-;YjAD+5*cY)?i;LGy=knoy=pcM zQ^*jbQ*Hj4{yfdDnB+0`o=7T3V9ngh%#`x^rWYQi6p}|R)vA$Y9MD=b!(>Iw1V)GiZCWeR}=y zN}?OQMpsS!fXD}l?dI0Z@0-%vW}3;&(pYQxPfirVd0sST68I(-1*9CuCUKMwQ*4+C z$7bATF+*v`DZy~FqM<&8$a+I)tp(PDKK`wTA3wKD{c+`&Hzsc~QOsW8ocWPUkzv%b zc%J^@E#O^Zvg{ovQLR->Cd7Ozz+?N2`)C)f3X5T`0vmF}^3vTy$355He~!)E*xx#{ zzcQQ4WbUFaDL9%1c0@oITz!mdYUTJ_K%&3dmEmohK75UNPie?}oRCR--FnA7>xB{S zVG??*#&ccX=514mh`=@#fmEwI#i$&$we! ze$(^B11V3^d}iGP|2m|n`2HBmIq@@b2X$BILU6hu=rQQb+7b$L;U!V(c0_br_iL%o z3K0z4d7k0bdB|vF5mj-n;kq5amH-n`bk8}jh|7=2O`3N9`V;=^X+mZ0RsSo!VeP0A z3AlwXmD;)}Tj14`%CeW7Nc}WCX$MHSR7-9awg}Y+xegAIVL9Wy&TSMes{rTiT zgU+lvTq-5Q^zLqR*J^KeNflbtcI1X_qu5s3qJLXit{R1lxf$KapFrs*Of91*M()Qo zLJkU7pPap7r zqyggFIu=Xb`uamh(PCf3G0@`;J(B9LA7-h#wYXgWmMOM^v?U;ffsiwi`~0_s%Zav+ zCzfR37KLSWJL79%=`oj@Swu&S^01HKrvEq4{4X%9vII*fGzZAdodx)CGdYVw)FW7* zFso|sH0eS+J(kXVnF!7LDM;p(0}~y{83Gi0-0B)QIy}gVa2Y84J{8mNADF{gUWGravAe=7GncOAW_=?jFNo?|e&Aono^^W?Te$pCWG zWP~8G3^{ZpjkB7Gov%FcyJ&J%#rVCZFpWC5R}na9a{5~#xeb9t0RrLMk6GM`WQZu^ zW{)-{@M*I&Q4A71CXHLAkEFufzFkPF-FUCcdjO+-mM z5ta0{)mD%|=>+RA9Auc)z`uaQAXnT>LXPU(*h*U)d<|J{-HkTMW0mQQDF>9eMV#ij zDl*uyARgC}Kj!X1Y|_ZHLz3$1aM`dpWiJwi`LaGdFejc~8tYyIfU6!#4)9s7kEIr8 z!Y~t7Sj|DzDc1!n&U2H+=9<1My>2u3-{A1k_}h+Y+%3{&`ZUQ>>3CcmP$;4KDz+wj z>FIYOwaS7BNpCI|pt28?bbuax0~UVqtt*7~b%;~SrVY+gTe(qc|3Hx&)ns9HW@!44 zm=zfg6Q)?udBZT_p$PVsiwI`HSGPBCOqiGGmy^43Wg=K;+Ito+RAY(Z(VoF7I^1y| zLz2;Oq35VoO_QW{xmq9^^gI?w*5l&VmlgwBt6Chv&AL{an65@QaNrs}`?-JL-%X;- zZo9>2vkmKa=r;?t?2saV9qGylpK8q|Qe>iOkkp0!XB95fHck?>`SC(+C5Mh4r(~%- zC>nUKP@&Ni(RVIWvz5|*sTz3{vmDR*W?WDE)Rcnzjr+r%vP!gqZcsxhFE*3P$?k_& z6FjGN!)GL!5K>X57EnT)p0EOZr7-0zzmS`;fkBK#0kJ)$d_2e`bE>gMn2xeo&-j$l z$;e*Dym?!6rlIn*Q&pdTnmitgWh+u)K{;4n?|@pbkx%nc39qRqr!O~(E^3&s6DX!h z$sMaiy{$xEbl0^pFsGr6KZiZ1ER*`j9xZ(F^h>vqY*L`r49J+Lq)~QM0jiRAPGkAy zy{ObtqE%Oyfd=780Y&CId?qY2rdF&4agB$`jl?nNpfN6NIxC20wLGUZ7Q?Grtd}-@ z!2d8JdmM4E#h7tyOg#e!^%f|i(63w$fpNd%ZICA`Nd~T{a`=}xxqnEA4Q>Nr7|}uC zYXce^W4a*#7KqeF?4>4`MAPe8vlSTmi%^BDgr)v|&4;u{=lq67qCr*~5X5;>>vIL= z1*NxuWzg%~8dtk)nKS|CUAW&97)Z2Uc1L75d&RNkEjKR*^NW*OPW_gVvdhQIIj)?0 zE9G!3WdxAO-NV1>8FY87a6q${gw^#z?(LRiA__zG2-HoKA6t~aOsuJGNyijJoD-E! zkWQMPGY8@l#ed66KiRkSF#P#K_tibo#;zTeXB#2)ScwOF!o%45rYP9DteS4GmjujD z!{ZB}RLB#oKDfJ&dSkJ3Hmum+;ev?eji8w1IH*xp=Y*eb?_cWtJ$rWCsuD^or>nR? zTX)WUK<6Nb{Ty-)Wo#5R^TT7x!;Uj{em}3_7QvCz^@Kj*fbe(Jg2}NqfsnStYBIUc z?)v5-igAniKYA8{Nz+3;Q~Crch4rQI?s>)&TR-9~%(g-MoEs-{p~qEwLGRuhY|>!; zd#y~z>){V#<)OKRJ8n@Li)n9_!Xa&V@!Y*-w(!&WSYoRQSvuFfi$bqUV+$m-DCYH$ zNj=zY@U?X%x^sZ0?M6gPVGLx9bZWz0EbM9V=ULgy-(=|}r#R)>&Jj6{xefMYRsV*@ zDxbtydMv8ub+S&Nx-v9h*!+G(r?d5iekm!2^~k83hX+2P7- z7&3X4%R;N8e{ZsL&qp42>zQZM_HVdPZ1dvSQ8GyG@<;DEUAg_`;au!>l|QKN6!7YG zPhoZ+IiQYg1PxR?lMV+qaJrB6_nCaVY6gz%k#1ATqo6iQxuVx`eP$j2D-gGd&BBeTJ$tkI-xwEWO`Q}nVrRjY^F2^j1*y`4>9eg) zXV0o#jLmE5den@aIIurLTrt$0}%*3bk>?XOCp(jSdVrh1>Xz8NYp6k;K*i4m_`#lThB|R9} zWQMdnO8H$nLG%Ox9jnJx452kv^l@UuR zn`SD z!dvBqZl+ySpOUWR^_9V1NV_C+)d!k{)70?Hu# zksElv!U8K0>xR|_{v`>^Lw?POnVy`>#H#W~OeMwXxZq{pk0?Uy8YfbDQlw}$&irYU zQM_g%xEyJYh2Ug0BVMssQE2cyvr8KI?!tb-`>3QjQK1;a{%IL=$P9f16CK)^p;4oo zSN;M_fZHylx+wog%GK7Bg?OH?~ei2?ZmzZjxwg z5CsiCn=r1LO+^`Wu2ui8lg)7=EgB1xlcZZytfZ73(-Hum9?nQ@KoBCSDr;z8f%E4; zu!U(@qK=)=0Qfa(UkL6YnpH=;7E1k=dWe;i3?_e1r zwF~n1!-4sF2_p^uz67`B?(XP$eYyX)t=}<}y^?-?d;Rjb{n^#+3HBI4?ga7ZUt%x?j@Q#!(qosCyt<@M|B@ngaZC zp_A1fv#L81R^{-Taq(@B;5k`@e>xW%G^qxP)GF^K?9}y=ht>S~$7!}#z&|dR*2~&iKzk&Fvhq3d=&K{H4YVz<2(HGPAfMDO1KkR1>SBOW-WC{Wa5cz?BhZG4u4C z{Fz}5B$swi%S73R0|}g^4o~*}YaWuR|CFf@{@HUJH?=EMe@CrqPK@v=W%%Gx334^G zw#^(>gJoIbJZ1GwYBq85P&D2b2e@|l9#7-c04&y->>4btRV1fr)~ea>mv1>CDJ7`htMfwEB+UkPW}2GygV z(sm$2*nD=5M-l+Zzv;Tq%?`yi3~xuBAZ>>ymxGW|SXc_ol|DT~Y9CTw1H+ktcGf^B zATZ!jI^3;vMWJL4fmITYw@gAOnQwaph}j0Zs4Zhi2XqZ&4tFi@_KZ~o?NR)Kzej=u<1q@*FcD(J>rKUT7YS3dzD53o zoEQDmFT4rviN?>2x3C)27=q?N=4=xh;++~HPfa3*09DG-3N`w36cdUBRFcQ<&008{ z9*yjM7czHp$~VPA?szK_!YqTz8Y1E+yn%-D4;&l_UjA}>5Rd88r1ML068Tm5bbP>7 zbSEvJ>(CCOUeKy=mWnt)H6!E!9(8&|r|YE2a_E&vam7GgFHLzNLm;~jO~_YJ|Hnsp z%Qo8?K8KSP-Edw--GEj*#Nhcg|M{TKsw$fPK(D*|20~vsX_hE3t~J@B-6y{I1Y_tZ zZx|YwGpfk2^&p?LTN~swqIi$B!`bw*DQz4D9)EBuBaZ#Z>KjzdC}yS-G^(AE{71R{ z;89nwW+6THVFq;eIo#_NQQ-Cce#`RpW)^Lu9a24?A9ZD%7$bWO zL?MchM&Iq0LF?-NQyHUvmBU&Wenk>rcWDNQ#y&`eR?oY^G1yf=xWT)TeEl9V6}HtG zR6HG4WGpV-*0gRB0|gjm*^B@QBbPhTfeTP)iZ)5cu5N%u=4C$!j*IS?>EmCbb0t_2 zKeA)co$tA~M03WKXrTRp*SuCDOO!w1R>`wU@zrvm?cZ%TT>gVreC`>(vSjCxhY`1dIh1x*_gIkm)fD2}i6F7^(y| z|7|ZW=X8Q@36Qi~<&(uE7O}}tm^A>JQkVI+F!pNVd}{FOr9$6idj?Y0gkh~WY!|Zu z^u?t}LFN^acu%65jYZE^ur|ubKYvnRh#i$YH+*rlYB(_u^yfHR(SmXxxY>t$+{w^N zf{0L%j_ReSy*OsVcyKu!i}n;=k8@d1;Vmd?F#i$Ju|yyc&{7hXDD%k(7!(7C<+9oF zw_Xga0TQ7^Reup~$ix~6>nsZw{ojvTDGGN5saF=3Ea64 z54a|?O$OGkzg+ym5$^YG6x0?scMSchh&`}#+&w~9yzrX6OcE?H-`oTk3NyI26;GS@ zpUPc4+;fSXh5gzl1@L&+vF?Fu4`=%}1{j=$<=J<~gm{5mePzEIzWPVq8wYK^V11+w z7ch0^l4eeGw&$Sr=Z}g?=sL?T)+{>rq+IqNlu!9S(2pckNA&Kz5d7J zGPrK&$^LE1kL-ayMPcAkjsfG1M&R59Q`^cBgx4qB)Xd}~?_5`g2-2u@cWK*5mEP3k zq=H>-(7=WZhps_C;KRRdGX?kLzCcMpJogqWn>24STU)%1QD`6oZ|B0hv3HcZ&mh$t z^MX73LGjJ9L#Oqpx{#TQ;*KC6KmRxt$FKhWoI!Yj85;jBa93c}eZM1zT_OZ-q(9}+sU@}|dv;PA93Y`7GYVQ}`?$no35b}+=IMh=qhH65*)yF){g14v ziCg64S&Oum9&_MY)E4$83cU`6`JWYDLuB)64XX4@k<5=Pp#P`!w}i|4HhU@0ODrb6 z_eSuRqbreBFpnGF`!H5rUwt{8#*%mU0MZHF7-XwUfCc{6b za<5zK@4Y$;gP1>jEuQr1hn9m43+Mn*I&k3dsQY7cJPe3C$&(N&^Y6LK+4{zAP_S~}VPPHB9oPCH?E zLn*Lja`AiFc|o^o@O*j@gs{#$wWg`SGo{~LJ=oFI)97D{yc4UuuaFE~h{0M}$G4@s&7<Qv1sOgZ&k64yL-Fll5byEqH2UKzboQ(5_wSLUbdF<8RilTvE3GY^RMIhz$hx zO4!7;F=3Azk+SFnd(xC2qU3A=y48zsH^6RLbKA@bKZaWdr>8E-oT-Jn*~H2*;U}QD z9*Vq0^kQc{xQB{fsx38Bx~JD-cK!Y$q(ZhZc8;}eZ_4X9yF zpZYO3j+*E*#QT^DYynQSK|-O4jw7jCNSYA40r z$}?6MZlbGdCq>Q4GtwGvqN-{q`F~;A|9ESpsF#5}Bmc4f|MLHj?=&a^?x@vO7V0h9 zsq|7LccQ(cm`%p1zg2iQk6PJ8720hu8SlW=;x(&|wL16mSWmPbo#<`jO7U5eT{pue zmjQCiwp0%(0)Xf&QMOwyD=&j2dp$Gg=%QMVQ;Kc2Dg;ZJIg=fR}$<>m*QD z){e{n6Fk(OjmJGiIIT)sAfFnxOQHoa8+8@^ty(+3Dx(T?7Y>@%(6841raFHFVMiqr zqogftEhsduU!oDEqrdLqAfyY#LF6H>q9l;J!b?R?Q$kR5FUb{&k41&`=4?%I<{I1f zG&8ooh+ggHtDI1A$f_~20I8ijhJ(agKb)yqI);PA8yP`9i#pZBc~<%uJ8W=5M0EGpd&lodA6p~qJhH&Df*-w$M6n__CvA zC*ihre3W)s%P4s`KlSQTbO@%i|D+S}Gl zkUcIlOd}zDM2P@I@;P*Y+4gZ!z=cJpasjt|LtTZ`=jybQ;Wcy0^H=PN)Ryf+v z^%5h~h*lrs6kDaFq7%(K%aO7Srh2M>)d9!4A?M8bSLFM~_~xqQ`l(}+(MexTjM>TG z7aK1B*u8>)idx9eLKVU0LFs{o5SZynA&>^jV$959tm5nv5)#bZBBCs8BAo2pl9D3K z;-V}fZ0wvof+YO^&k%hCCV6uQOE)VLE>5oh`GrRZt#*%#QjaSb6{ol<^1X@`f zON7ciLBs+LT^x(KktIzhQ_0ALoYRKh4#Z5#vL-1H`X{7i8=v|uqMbiIv3=3)dEIm3 zcao9$sW64%TFuB=)%EV~lQAIzvFxN-sX}5)yw^^;ZkG@|If^`g9K^3D=n%k34Cu$+ zf3rpf20`edUnAI)QV*u?F)rW)V{D@95!=&H52^3_Sfd8A*Ws*)`QiZvmJT|tCq-aZ zqArSR!BX21+vPy&1^6p*7bUgeE$wpcDC@-qC@Y~|(!NNG2X9VSAmm-{YuamwD|jai zt{6VW4Y(|)6(@U8xiFgpz%%ZNojW+YzhxfS8qnPC4Nxxv|3Z)E{uEEX1GR^mrin8R zXO9x*l&y^2rWV@W!bIZy*LJ?#Jy|%))z#)J{#M1H;B}p=j=_QyYQc$A2rdZ80lapY z(E+FoC{-i;sQ_(e*y92B1~7*J2`5bYzzv5dp@Yd?9Id@8wgP}!0KO7(6&PQJT>wzM z?b1M@V8pm9*?n0!{4h_~n4x&US(YwYN~Ct9Ee6I-TEzibXz?6yCVbf0ayW4|mGH!U zx@_UXOH9EhyZK+urLwYFBNPFw+j=$eNv=ff$PYN%$)uWsBP3fkUSa?=C<;m^oZpgh z!(mBYoA$5KfHR~gF8nQxz6p+hPQX&FzqTG5R&!w9@FO)NS6^{CNz!3O(^tl&IVw_W zMMGDA^8kqmMHm7OivHt?g(OVQBlgwmb@|~JwSVN0It4bCz^oBeFp3?R{3p>%NN8D( zo_uuUUZ9jCwcFa7U0mg>W`8m@?mk^7!@#N31W>l20uR$(8`G?jFHg=76oJS!tOYh( z_Rk$v$ch5nDr9c1XY2e(7zq&83D9nV#{qf?ux^1wVDFJHy~ULXn`}(#*qx3Z)wFjM z)vD@^KM7IQQoUFk%BvQWpEs%|_|@AA&e5!(*5}Zf5k>v;90p4C@CcrB@zA)?wkpN delta 10977 zcmajFQ*b2=uq_;GV%s)$Y@0irm=oLDv29~w+qP|66HhWR?srbrU-jRo`_i?ltDhRH zS9SGQ0&-#^a{Z(Z1P5vIfCW8B*I||>|zdVVmoMc5J;V+QdEm> zqg-D&9aQ(A!U>j0j#~*j)$FVzjkZ(bPf%xSAKp8-J=VnL?^?YZk&hUHu83bJUoU~3w55@-rEL695mtw#3QK?4t{?jWofoe08SZaNoHL^0 zL*nwT$t^2LP(@pQ_*<=zZ;0b%XV11+L+&$uo?BX&`7luN{yZRJeDWkptW-Rip9JB% z4z_a`q_w%KV-;YFBKR6mjTJH~3!Vx-xskwjZZE4$M1iRrLyWD{zuA&4IAJZlq-Y?~ zN1xG253g;dhik=Dsl25q+>ue?CQ4+cUMZ7xEJ8hjZgSNiHJ|Y`rs=enZrQt{F)At1 z*$lHU!M4;maP+AWFO(KU@TQWpW)$S_NKl^4~Plk9_VkdeW)+lfMzat5kNa&aywn z$Hd(Gf=&g5Kd9{6lby29=-2h0hB^CHn@ld$!E9>Rmy?0y;AQ)7hUq}~b`IG* zFFqh>5^ACax@^0baSC#;kz<$F>Mbw4QZt3a$)|AMl&u!- zl3a9eiU1#{!lzFoDSGYYI`pB!7y%5VdIBV}{Va=KRZIO zSw-h=BxLx6qlO0{1;+6!%;Xiva?t$mFJ-x5dsUiAyyS#oS4Tgb`A0kYd6%Cb4htzk zn$m&TUOUn*?d80%kmEBNmIsD$Wxr`K&M(iFENQh;5;FRoRpH0DN~V&N;-I*soGJ>?@X=S!BDy)4_cWP#}@*FqZ0u;~I zj>FrL2$mr>VCq0hOV)ypGIE{^?d26_t(E2ejT~hc*dnKVWk{gIRGgEQ)Nw5N`z`^% zQYVZ^SSm(@R4h~VV0~D@4?^4Ykq;RutK5GHt!Wem3M{vWJV|`KNi%?WaxGVZ3Jpj> z1H0XCndG0ugGF6pX<$?M2r`{Z1f-7tTDYf^l@K~r2^B*%C3e*4JI&X-Z$lPCUWP_T zR3)v_kZq^NHAFx|r;2H#^b%7Io5O|m=K6d3&56FLX0OL<_%F@b+7y@H41@Rq;FrT( z0~V7?;%fBE_ZugE+(@a#*ROlgX8cxs?yP-WtEXtU?1V(@&?2Qf3ZKnD&L4q>`sXTW zgXftwcyK(`ii@l;T$3jRNmNK%sq>uMh2?nwp z%Ay>~N3MhrOOy(95MN?F>5pjNqwZh$G0eIg6!7O(Fz(B3#)&_Oxl~1sq+ywXKGb(S z)K}Ho{-YpVjw^rK+TVyK<;P>wD91yzh7!XZqr^uxIZDG!(Rd?gJiik4cScl8#}8~p z(82$XlxAS{L~QhgEvH2DrnbYg;0FNkua1L>J9csDdmKdLz8J}_*z$YPVpemMq(Jo2{R9x^k2bCB4N-1v=S#+YK)#^Ty$+3Mk=2@MeZSr?)VwqCUo7mh zcmb?NC19Z-)xGjV4Gs4mLS8hflhy;1&6e*Jh}ot51rT02Tli7N&61?D>lv{SZ|181 zp#icWA1K8uR^0s);S}px0UWQyal$OMGdy2j%ZVG3(J4!MP+F~9%t~6$r z6Ke49>$TN|aQ{o+tW_+-xW49V9$9nNHz z{e;r=h6C<8QS?cD`0i#{=xg&EZOh9thXxd~d1(D^f&XYz%KHqvM?$v{LH0(skb^!G zCovSg*(uS~Fa^x>Di#RNbI$Wx5}G-O8ypo)J&UN%j$cl@o(H@vqqn>}iu+@0H->Ej zV;12faR6lB@3w|_&wu%umcY5#Gs7EpH=RP5-I|(Day_0%V2zJz{^Mjb7guL<VU< z;`w1i)O;1j8x!ATqrDMxu|J`dYU1$Xisdfl7yVLV*|Izyw0RQ8Kj*#PTji2K1>jV< z;n(A!dVhCXP;Mr0E^~<(9DvW!O?N^R-(3|f>>yA~z5lVr_LKw9ksff=gh}Bf>D1!GXktuV! z?n>r!HD_#jMKv+;VQ%6d=cGV4TQnXd$hRX<0vI)w z6JMPpn|vR>)lYK!P@^P!z%j+tgmJ?xnJy&=$u62vr(Cn65_Ra?Cvci_i7g-SEI0-F z^IKV`q5Z6lp*x7{jQQdYJG=OhrElu?gD3#%zST z>5m0_X+fC6uv=&Z@KLe##7Ea?=n%PjIH5tWK?vyo9IJ>dAz%D4#XIwx_@*h|jIn@$ z(2v52LRo6GJ&%FgE=`|(QVBsGnm}Qz)@T1)TN-ofo||{6^;yFfo2#5_%1&3G+5}w zq-;1;7p@ukYz$aziI8ZG{`^z^uR;ckrLw(eTI^hHblzOpY19Aw-J?d-?#ULEFoiJo z)$Ogqh>38kVV+KAo0-wafR@J!?tJ=L`V!uwK0l=PQtZy@X1twS(v(U>O8@?;DS9v7n!&gdQ1$-8TRncmZWUkzh^vm9HY@l(%TszY6U zOw<^wQjz7*!5h6Q4}Hy#o-H4=_@*i)e1$b)aE5;LOZ!|BCRXgeRM*K?H1aYmCa z&UXw$IRh>CqiHM9xKc?1H^ic%S>`wmikRc=g9aRph8b2TlAmUFsZm{1Q-UXsx6Epp zwWC;@OC6wTCklj<&{C3_yl9aC@!aHKrg=Sut%4b@@*iNikmVh9Ukes!|KI~fUWqq z=uwxMFpD1THs~}LIn_*=Dfb*#!|%9I!zQAF|3I%}55D16{DsB_m7M@XY{~8zT7q_m zyWYv%?R#cRjqjvr=1Ynm*c=W+rx_ho1ch^bi`O7Zv z!Kd0oBnvVVI}?KvCy}2jWxp1ueK2rGF7=S2;DtF86hG)+G{4+dZanGVy9+C4=slWu z{yK3u$&@X%K5&FhTzXIA%9C+9Zj>7OimUkPBevRS$`DpGh8X`nl#0uM z^&j*qpJs*k`yCC|#`U=^i!FsI5EL|I5;IwwW>RuCfq4rEzM#-CcRv0n?lF>M8?hkS zcsT#tCA6R#?G5`aK2*OsEjYi5Sb_%1mUVl9s1dZReg_{KKlRee;q@sXckWqq)JD>wdD|+t~37)t?Zos8B(K(3S~^r znj8g2C?$rujWp8^ZYpfFPaa8VlvRqxPOvMDkluls1TcoyF_hE2{D<}K|4z*{*{~_7 z2~Uo&?s2g3tc#L`w_=(`ORI-4wm-Co221I3(>3IQ;7^ZikBaE*xK zsE$`LEfRz7+v`e-5{L*4CpQ8uD2y|dV!~YyRDt5uA&6t97ZK+c|G?*Uvh$6jf=hDL z3~WFapAhwO^`WOmv)D5%l4)&}4Do}6Wk+c=%gTPvNyqjKHF@e!-zWq;AATMQPgOJ> zD7J^7qMYjt*K9*PM$|8c`|g=8n+XS}-shqnqi@gPH7&<;7!v*p!z44^E`~Gx!}PED zefD)4^;i*+MXo+!pR}(PjT5p9S;b@fD?-qmAy~EWb&jK6Xfr6@ zHMqIZfm;&2UZ^x&v?6Oiy}B~TqKwfxZGyKKxXwt;xp29`@?+ec0rZym56n?6OLPgbT%zWyq zoG*3bc;d4Ub6F7{q-xF2Z`!pMtyR#TheI-Vg&T$wLqng~i{xE|s<(G_d5ZRUPG)X` z4z}vvGfatubuT^(ug|11SBk*H&FWF$@z_F{$IydWnaa9k4e89sSD~KDYND< zb)LhpJB|_w6|r%37!Q)d@{eGLy$y%aXe;mvHQEg!wQ71MOE~uxf;at2VSf!F8SKGt zw3MrnW#&$`qao>MqL5B4+XP=$uK%Z_@Ll z^DGKAU7lf;->amC+&-vN?Zt~|^oE=-Mw7Xik!5id1SWMM(oQ;S;xs(_TU=54E4{*k zoQ4<_qnVLOgKcqA826U{cdpAR%b6yQkl#>a#quSSSG4H2ej#bA{wYHKWarO|%lvlY zF_F`eKnCD{mk8LWgi%^a=#)^|FFm|!%`w&RnqwJK43qKrN|>EaQS*W&oy%zxmw&<^ zQ*)NdFl`|qI9%T5KnLg`KzOStvS=eM0+drCkI388XNOx95re7C3EjLn`3$3EWWJ0X z;aQd#0x#^q_fK(gASWupCUyqZF?##&3Mv_?ABkdkOwcpy!Y{4gmKN z9hSk;n)N}H(Ane`FkPwgDAk}T? z_r=cu-nq3wq?VP4a8uy~6H<)|7fH@rPz&s@>Gc3161`weVqT$Z65`QZm-(^F_i>z) zn>%cSRV8W}ROGu+S4C&;_>O8CJVaPu)k9LvwK5p^YEdaNF(+k2IxN8`wUHj{qeFX& z>TyAqkp)usJ_Aa$w0t#_LaS{s{4$82G&XE_x(uRt{89OAsg!~n;X5wk4Mjm%%pr6k z#!e%rO}f*#N2`#csBGMV&~!+p9Lu!osQa=bc}e{Q_*X76=#QufzN=nApN5ry!=-bOE-mce& zl!Rgr(+IJBSCF(F?CJ)b4et3Kw))`iaA~G1Kfdk2ji=kwp9r}w&d_0~Z_4N2TE6th z-P7}t^9!21pnvyg44raR`q0$TSvCtOf0sx&Uv1)IMS1KQ)ctvIYU6pWBZJ1ha*kB$ z^$u^!=E66Tt6Iq?^`M6g&;UN#Hi^1GJBGT4T7^C#E-_}N`LJ`zmzJ=xpE;8PfsuKv zT;l@!)MwMP+sAp3xeGa?>U;{ZWo#3q)H=rW8b$jez6!|Ua%RQ<(4@EGIY67oKi?d_}y`bY;ZA>`}9LQ+(d6ygUUu zkBQ~zVze&WOTRAmThq1KXG|6=K8nlc#OrS>N~d3xCpr|7qY$rpvo=K`n{c~5(54Sr zZz80(J}oqrf~D-SvaoD5(Znf>3oF9ZV+sq$&RM#(E#G8Q9c5Nc054Fr%FhWqEV;cz z242Z;AyzdNK}Ysm-4F~9&J@s1CKYWk)LILgx^&ur&)4{hf4aEah@pRQi7>SCi5bOp2tQr+x^Yb3t; zr{eaEGyyjM`tq;F6y6C$8+0uAJSpb?$<|S-KE>t}DS2NjdlLyS8^L08vfiwoU1{?sx^5I4a8TValx!3Zm_dK5PDq%==fj) zwStg~Fwww;9FHPOJl-sbmWmO8sX96cXJKSbA<{&;i2!CM$YzXSQwaXxh*V!Z5=Jf+ zjJOttYl?J`hH+FJKpa00UgtjSJW^;JiDjVNo;pl_BC3sQ!*kA-rESBAMtcPfM<7KA zDX{Hw$OC}l9)`CKV5VsRhs;3$WfT^2X3LyLa2O#=8$&WWGeYC!~Q%U>bQYNDc?cF++|l&A9=|-I!pA$HmV^Q1=LQOWC_B2{SR#5V^Ud(s^M@5@d168GN3SSI zsoi~X#N@|*vGQVAJQH$|Pz0{!J@^9nz{}lHJcf6-!Hm)*)2qn&{nA-TFO#st#08Xr z-@I79k`UNZ%=sfc%FM`5ez%RL1K-J|7A&I^1hM{9;* zb@jCZMm=z2HxFX-nj|1}A@-xLR-5sO0%wRO?wqPe5~5ZFLxv#eHn2ZKPH)EQYk6^I zd>Nx!1GVeLD(`TsltqZU2LfQFmuVy`fpx;}7gWS3Zl)GAY;`AlOuK#m#zeA;HzoCD zXJJCLaaw_+DE5xy_eFj!-u)4p_VM|8WAOFPG29x|)A4rf)volFur5$ag{D?-c2F{; zo*B&_DR>_xp4<#db+q#~t=hy3l30g2)cDmU<%v^ls{6}lQJ*C7qMl!iwRuAYFb#L1 zsks%C7%;>WMv#b2dw^+AMM|Tnuu6+2O+dQflDu2i%gSYy4kJB`MEOUWH+DG6+gtzo zcWhw=7OZs|5cMrZt-ZqCk#{K5 zS1k&r=+d7*MldU#*6aFSE2aVl9Ye&CW_)9berv1(;+5r&;_^28v6dn5 z8xGFbvtQsqJ=7@)FISvlCiq%Yhd$;D_9a6aI`zF?INF2OGKI*Og7`xV5&%pw-LR~P z16lyqlux{O0qcs2C_kJ|b#2 z*1H8dBgQ1Mj~?-T^7QJUh0mT(w)6T#PU+7!Tq4y56&zJ+n{s|b`bilsnf{zln!N}z zSfbKjSZOS_=`75C{nc5rC9L_F=KmXXC7CmKR-oH&g%$^+{SAu!RNm|Le?BZ|HH_JC zSn%hu8@i`jci?!>wcd!2H#8M~2!0YSRXzs+jShG}BZ(K&A8GII!}8|a9*O*vL6G(q zkAyEB1?i9UrWavf#M+xu?&rVWN@fzeQN-gx{CvLOl+g*?CnwjxwNVl%@nGO>;SuKI z^voz5a>!Rvhhf&)czKiBCV0y)UbRp}`<5|t7n-(4es4o)HLaMmgk1h}L-YKR71#s% z@#28|?FT`R^JwDMg&bnw*U>?r-hU}=LWh}1*3dg82VU~6hagt?n? z`TB>@_wN1LS~oABDM;iWs`(($Hq4W`?hI|G^aIMp#Mc3Pr5)^mBjt%bDS&Zd<3+tCwGco!v#Q?b&#Ha5s5RKxxCFTj*-FMc=om zIRazHw0gNh;S);(b(Zl|__5Ja-G!Sj}lxrpDQcpm{cppt{-z%QR zSNvVdB9`Zk#lAAf-|=5d;;v&(x%{-XczCt#&D${$CjgF|QZTh<%tURBW#G?7aSH0< zG_fD2&qoD@%*3Cx-h{dPg42Om%e%Ex^7%LJd|SX8S?Rv~br~&Ry;^B&*|<$KyNlB= z4}rWp_B_p#5O>F~_kFpDUOs*>7Sk;09;dRDt&{28(OZgX08>*A>Bga9GUcb^;jI(i zX)fKGsl-Rxjh?6OU$=V#{6f|yRsjAtOgU!8LI=1KMqmsSa4+n+QUin$f{G8H;{caF z8|T%~#kRY2v@yH>&#wC7&Ap50*VC2TTw2o#uO(F484eEBG%o}9aqzepF~VA+Af8f+ z2337Pk#`H!AJ6F+h3FE5eTxl?EpHa^7HP41X#R*)!vlR7X zrgXBRL=BL?Ob9-xX2SoLJwKNB6_*A z4%}T&FO7hfMXSwoIlKP>p8@#6AI17M@An*gcwi*dE>6^FkzUhvic0 zvqDaH9jzRS*S+Jx`C^jqmIm>Mm|c8byTfI=RsquG+|SLz zmE3XN*9e^*k&BYz&T))S^gBapBDp4Xguo9cJX7;xuT`J^>x}>imt>Rp;`*`qAz>SM z6s$ki`-Ik#AG%2|Pi+1(1lbdn*4y`;ADCZ4G$?ZbZLZ*raig?6g9AgqJ4;n*tcR9L zYrKC|Y9J;Jzw*TaigI+*O6^*Dy77f*t=U0Jr=gDq1PPl5_vS(e;`O;c9xf{a~RX8dA}GqUc2gj-pr{DTcMyzYXS zTUjRjVhs~?t%8`@StcC+Hw4jf{jXb4tYP+l;ANJ{{}1jcJKC`K&rY*UOW(L%f+)E)W~*BR4(wYR^uF7M2b)09jgpC)p225iO9-15&|@yYBw5i z8W&$3XfG2+v&B7(YcTbi&w8*o{ML0lt=z!Q1>Mc|Y?$ViPn_C2lFoHt3+nyK&c|O( z0`7!UZ9#7oq^%;a4|yjuzo`!!3%(X^{CU&I5^dW)V!w@O^>8gA>@x~AISwzY+W4Ai z)pmG>i=T@4aD)t3<<6kFEpm-pT6Xd!@n;+6GqI^2nUYJjRxO{Epuw(Mr9KklE z1*xFsszq8~sd~i^5T`$DpC>Z;5I$vekBP^d=v)4)Zc!IzWlhZ{3>677aj)=BD9Bi- zB&L)(qeS>$)68QJ!{0t^Kmh>zvBB1n3$fAA0fcHabtwi5+R8BtCE_hANb3Su@vg)E z18eT+7zYpLm_K(`Pa%EWK%v@3_Y1W3YW*6Io6@)i-z~orjd*G|aa~|z5MFPBps*zg+v)~u3bn;- zglNJKv3}DM8V+uH*Oki~sI&$hBj0}u2E+G>%vaz-qrlqBn;e{hCL`|+#Q}n$-WmvB znCJo#9RsGb{f#RcfpBRp&5y za%2SmC1}jK^9^>hX^EH4<_3wG9vA|tuf{4R#VIBZkmTa!OD_Zo819*`?E9qITbHR6B6mVXOlftLT0u zJrJFJKr3#_{-ooXrMxI!ErLf{E1~-S)Bc+kgD6%l_L_9pk76esJ(g?xdf2rPesNtS z_ICGet4(~B=*!{U-!+i`+L`rGt_>1KatGa(xB{fMt+r)1{R-gM;xB*ipdjyuIpsFP z4v=lb-9XuK@Wc=dxy=)UGqpQyJ8c#fV1c*;ZOZH*#~fXFDkUI&DQXWN(G(}^M$qGQ z(3v7qN0D+$*YXbx!x{$=(Cwi3F$s8>6tl~BR$4CwTvhl)iE3u`j8)_?NlxSfyTGId zBw1lb2cR;bfJXS!0XmNG(}7b)#CqUb1Dy3>wOu;QN6|*`j7@Kdtx*twI0lAnItTWCsyox=*@H=$MA7Y;t@wWuw{5mz&#bYpOYRL|B+3?Ut|;`}++ zvs~P8SdwSI-F+3|1>!7s){dt04Tx2^7L&o7$^J4HpOmFAqoreKGYN=3q2k)UQ=10- z6Cvl?W%rdtp(d*Sd+mBxnU@{&m}<5|&@z=^f2@W6FS@vWypUA@0GcjRwXLl01WpY# zHN)BGRU+;MN;OiajT`8ko}muP?;h^n+KR^~m1#i4-fsOGXZmYww?w}_3t9<(#@99$ zS;^W;-*#RTbbD?*AZ9>s o^7R1H2fE9+#-@QN`5Pc8tAG-kbd3l|Qg{F-0u_~{vJ}Gq0UxgAasU7T diff --git a/src/Cryptol/Eval/Reference.lhs b/src/Cryptol/Eval/Reference.lhs index 1f4e51ec..451a58a6 100644 --- a/src/Cryptol/Eval/Reference.lhs +++ b/src/Cryptol/Eval/Reference.lhs @@ -632,11 +632,11 @@ by corresponding typeclasses > , ("/$" , vFinPoly $ \n -> > VFun $ \l -> > VFun $ \r -> -> vWord n $ appOp2 divWrap (fromVWord l) (fromVWord r)) +> vWord n $ appOp2 divWrap (fromSignedVWord l) (fromSignedVWord r)) > , ("%$" , vFinPoly $ \n -> > VFun $ \l -> > VFun $ \r -> -> vWord n $ appOp2 modWrap (fromVWord l) (fromVWord r)) +> vWord n $ appOp2 modWrap (fromSignedVWord l) (fromSignedVWord r)) > , (">>$" , signedShiftRV) > , ("lg2" , vFinPoly $ \n -> > VFun $ \v -> @@ -1299,20 +1299,17 @@ amount, but as lazy as possible in the list values. > > signedShiftRV :: Value > signedShiftRV = -> VNumPoly $ \n -> +> VNumPoly $ \(Nat n) -> > VPoly $ \ix -> > VFun $ \v -> > VFun $ \x -> -> copyByTValue (tvSeq n TVBit) $ +> copyByTValue (tvSeq (Nat n) TVBit) $ > case cryToInteger ix x of -> Left e -> cryError e (tvSeq n TVBit) -> Right i -> VList n $ +> Left e -> cryError e (tvSeq (Nat n) TVBit) +> Right i -> VList (Nat n) $ > let vs = fromVList v > z = head vs in -> case n of -> Nat m -> genericReplicate (min m i) z ++ genericTake (m - min m i) vs -> Inf -> genericReplicate i z ++ vs - +> genericReplicate (min n i) z ++ genericTake (n - min n i) vs Indexing --------