From 6fa80c47129cce7fdc297daef0000d92f0733f33 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Wed, 1 Jun 2022 12:02:16 -0700 Subject: [PATCH 01/17] reorganize sha512_mr_solver.saw, add remaining specs to sha512.cry --- heapster-saw/examples/arrays_mr_solver.saw | 2 +- heapster-saw/examples/sha512.bc | Bin 46384 -> 46288 bytes heapster-saw/examples/sha512.c | 2 +- heapster-saw/examples/sha512.cry | 69 ++++++++++++++++ heapster-saw/examples/sha512.saw | 51 ++++++++++++ heapster-saw/examples/sha512_mr_solver.saw | 92 ++------------------- heapster-saw/examples/sha512_proofs.v | 12 --- 7 files changed, 130 insertions(+), 98 deletions(-) diff --git a/heapster-saw/examples/arrays_mr_solver.saw b/heapster-saw/examples/arrays_mr_solver.saw index 5dfbb1fa9b..3100b82983 100644 --- a/heapster-saw/examples/arrays_mr_solver.saw +++ b/heapster-saw/examples/arrays_mr_solver.saw @@ -11,5 +11,5 @@ include "specPrims.saw"; import "arrays.cry"; zero_array <- parse_core_mod "arrays" "zero_array"; -// mr_solver_prove zero_array {{ zero_array_loop_spec }}; +mr_solver_test zero_array {{ zero_array_loop_spec }}; mr_solver_prove zero_array {{ zero_array_spec }}; diff --git a/heapster-saw/examples/sha512.bc b/heapster-saw/examples/sha512.bc index 711867222ce4e6bd9d46cb07698e7ba8c164c5f5..a8b922d8df3fa2fce62a69272fa3530e2fabf644 100644 GIT binary patch delta 16670 zcmZ{L30zZG_Wym^g&4vjggq=ODq=vZR8SLSv!X>yEiO1=DWx5%=rDroOIS1_N-$Wl zW1WaPV_Vyzaa!s!O;{9L+tU7-DecEvKs#j|>cp0I7;E)+&V4Ts|Nr0Lk4AVo>-U~} z&b{Z}*Lp|L^G|`|rai!uz#l*OcjSVS76Ctxj+ckOmtUx&l8F9#s;aR<; z7#_ERBtkSFtJ@gOVx>n^S_=N|q0S{l?Eyd8!6~bJf={vO3k=>p;Q7?i2-yqa~-zV%s&}0eo4Py__a0;9#h#<$aGj@FTgH2ENl- zzVQu=9n>oRVNl#r2h5#&ac)4u+1ZEBURWVW%&gu2@!KCy-hbx${tZofzuj^P84_A1 z`@J4|OR<@0tDc)!JC`U)>L4LbLat1%ic7BOk({#p%P%BWa{tkzM~jEx!|Mb1Saek0#BYL#-4(b42_M^M6^XpMFY7>}{z%wZn?6+DRg!IxM?j{o43?rzOEZo^3&k zn;yca20uFLb@|g@i6iz_Cc;moDJUaqnItm+Jrw>EKD=(h2YUFYcF6@oIwYxDrQPIU z3~H4+ltOR<3F_hFk)|-a`NPm50qN121FHvf=H?L+Csg_IJYOppPk^{JDdM0+KrSniSIC}&7F>8{rqrym6aIi;F!)S}rE@f&h5 zW`1Gz$)`BDd9(vCi11IonveswWdY%gvI~BV%;+|+@Tie~0Y6)I+5*@YHQUBr|R+heaxZiiW^_u}Hc58{2;$i@3b z>(`D2o$Z9&^2rZ)H_5(d0U`Qzk;8%t=_sa0wti_%-q2kV{xczlO?z8CZ-(}FghBp^ z^WHLWQMjWIk{e1lIL4nx$ld4*$~ZwNM^){nAn*pWa2PTiD*muv;mr3UH~}w`uXPLi zAWF9@4Dxb@l^X>3R4=KpdgU|3@QH9jk*qNy>iFj^hEQ@UKs-!hcBy*A+9OvCab$|D zP_OV6B_!^dATYuYk)cy$HS@ESrr$TKmBSjH`m6jZZCi)PSP2A-7Z8L2K{60*ZB{ok z3$m1-Siw6o+dH+mu|2Evpyl$mxfW}%ujRwwaJC8Ou2ni)QoG=igJyzzP61P|3L&y8 zCdKO=_;!(boTjOr(hLl{(Y%c`GzXxZt_7_qhtCotJ(x_YN8!V38>EPSq0N)^>@gf6!Q2WFSGcOVnC6SUUy`iW24m{=(@Q?$NgxBBP zbegHoe3w)qT)^D`+dpDhbhUbf%NP@nI7goCKq$%+tQgAx+TixW+ ztZH@1^&8bn+*rA6`u;d;3D5chBwX2odQ@l_=e4`@R?|fLo{P89>$;n(N_2Jc_wYeo z9qKp>CM{J0mJc+5rCA7Bw<`SAJj=(S!MFqIm;8cQfD~HNZ>_D8XXW676Go6c)rH z+ZxI?CE^|qsviWg&f6CPB;Q92PQK;9+R~&Jt|tcXY5~z{%5o#Y&g{rRF&X-nNd8mi z1*85{%q3dv)P8mdEg!F0v_MJ(3>Xw+1P`wJ$Y)E^p7H~-90>v7R<;a@iLE)jmC0vj z5$$s|{js3vP@{r-~^BEg@f?*2G}JN(SS>EOWSm@M1wn2Pj5KtS>Hlz zpH4ovusbE79XM-l;!ZS(W z>X;4aY6Ne?iUevy0%yYUcGd`BcpuPE9hnx{SJ-glb-DQQ2g%V`}V8pym(mYVJ=1HKm*y<>Dc~<>1Yj z8uTWgR};UOs+r5FNd<4Hn%>2zWP92s5z!}o4iFcK}}@}%@X?cJBtg!o2T8q zari1}mN2fTYLYoM>%g0*sW{SMT$x~s9z0yTC{jdtUk-~A4}$#wUJ z@#nnB-$>QyIW?u=O)m9jBdTd{$+T@t97{#&2cYJxyP8ilGJIr)>agv};n(Dn!Fh$* zrrLI>P^DTCm0Z9;o|XqIcTT1A$X^B^#_E8qJ`KyuDJf+4f>;mRf%$eQ`RksV2`yl1({5|N9c+134ugv03s@JSnqbePz$^ojH zsH&MN0!1liUqL7_tke+96wFLXVm|5dfDEr8ai?t`CtqfYu^y($dgB4X>w<~kTDshW zh#dCUKT_i(4peg;lPmd`3d%+CabN%kjamX@xmrsLOXqa1mK1Zi)_}2_{INd$tpImP zgW#}p;aALx7p0_mvI^XdoY}O6kb-OKU>JfmnRlT&P1LQGlz?9+#osE3<|D1-A6WEX zTyb6q)u{<29{0bRM6|Q^9F||79rLOFiZy$m&=#!AVVEdeS;{>o)PT}6L3+W=0~Lte zqrkqGv~L3IS^qt@U8y;Y;A*n1H_gd}MtH%ZqDKN@vNq)3gj^1}`Gn?ceK`)qOoeSA z14s{Sv&~!LWWuV$i2fC|0+t2uCf>w>f3QJ+)ffVcskF5rKikrlf&u@ry_yB2ur7ze z4h6F}Y`P>QBbzI~wV$bO1zwN$5}mfw%YpO<+pkXpsbU8)tgcE1gl`U3N}*IczcB8X zYH-cCanq2^b0v@t+w{+XTlWdEiFN`q_O5#h((}>4$3lzO!v(wXOcxR3E^h8sK+* zg)9wt&4B8hbs#j#wl@!ik_m`vEub35qZ-rqC+91`8XvI7cKA1lYNqXbJ)-J^sCodZ zc|5AmXr47@0B=>C!gjv^Q9WqOE<#kJ5mkRc^#YIT8~XQBJ_O#hypSoj^~GSoRGaMu zM0E+GIunrD!lRn!s2Be-2~fS5m~C^s2&5}*{=Y?3n-JA?0L@(<)vHy@JmZkJV$*3` z^vghc#xHX*tR4)TG{XD8~iG2eK)&i?@P;c8)29zbX8=HVKR{*HC12Ww_stuk$ z$MszV*4u#Uo!=p$@O{QwTy@kH$2n zbPQPDtPIRW)4!q8Q+es8eitq&|BG}dl^#!}@Bb@eRRGed@Cp1fJU%8JgokVmT*PI% zmA|3p$$A4QYQ+;U)rRkemd$JNG0UU+#6)Id#IU_wE7AtMD=(a%IqU56ZGY2MS<1Jr zV!3wO>?5_a8MhXTG46)()zlf1_1Zn<*q?IVa2#n$!ELiH;9OFo?r z6q5R-qP)JlWEr*dEU3g>)Dx9e4Ll@*35+o8LN&98qedWyUVnTOJe z#O(`B+c<;C!3nbds1*dJ6m@6DJQ3I}*4BQgwHUS;S%z*g|APCjUiiQU*U=?`(8_{z z{$ZMHCwj?2cZKI4BfA#Hk?kEPGg30!V`O`$0U5vD{XudHzw5@GU^e`F#KOEVPN^T? z>uuE1z1}c<=k*hOU|+7}2X_gy8D}4pKm{Ch6QD)`9shbvz)I*dj+t;A#kO$*SfoW0 zn%yK2YQp0Z&bdoKu0^enn*be5JKql2*#93COOYM(!3TSbHWAjWDb;a=Ovcqkui)fo z7Q>DpU+4qErZobhusZ^#hGWXLILli*RC3teW~bujZ`r{-%V#@OIS`8KI^1ghAsTkx zp-RDq@jYt<-7>aagWa(<0Qao(mcV8h_N+HyFTiN0$PM|zDi0Y{$x2HhY<}n9-m~oB zuw}u{z~_)D6qyovrUJK(uAOdl2XCWxjT#J$n0gI5w$d7d9JbjWBq1N;WeqL=M?=7{ zITFlc|A_w5^488k7L|RdkAOV>S~qQ*=!DQ*EwgGRg=$GYk^J!sF@EO-x2^#}a`nKnW7ToyA%LnbpB)p{Oj_3rG$r zu%9rr1fc3+BAnHb$po0Xw+(`vby|B314}+R!(>4gkmB(EOx;+BZk%g?M+8wxhYI(W^`^jP)!JWJtIb8Pu z-1uYSMN1y5ng=$QOrkvy-sZAem(9EWUz=}xc!JGZ@t2k}Y)~*XovjdNr$rF9Ogv;C zZ1qF#8&Q968DN)j-T7*bvsN?SSDq`|Zt(nrj2RL`W^-1>-O#D}X~r`KY#C5=>MaF^ zsq9a`!sKw`3|UMYW?--C2JDPovnTi)_{wV+d@QPg56nm=ro)q%9p_*Npvr{B<(yb- ztqAMKn(Wr4vN}lfatZWCA_)wVnYn^pt88rb`}hM$MOMi4r69}8?6A}03+PmWOL|Ly z@wv5J2G0lyGcej{1tDHUzsh^0JyZ)#T4!yN;aJ*4I3gj?9fCilYC98B7U4hFTcA`x zA|4XwwN*<)1lR<<-0E53?61Nse>?!1=f`p_*NllQO$gj^%6I4(7}O9nLX&JtiYv+1 z=)QsPysSuY6h6@N zgQeismnxuJSJ*mKuWLM{Lzy3g%r8UWX^8hQJlqK*4hLVpa@aLCPJ&;0iwdt;d%zIG zL=^Mn7`A(R~sO?^dau}biKqGk2&xe{_uLrAXWwcVk7gp80qKaHn};z_VJ za@5Ohb^3t2`t;rO_(>C$-&)|TtuXAF=#lMlYV5Dw0}{$8CX}J}Ez*Ck@L=dtssFBe z!BaXs*|2(k9eOfjnjB9y${iQ0M`FYR8hbk`tYPe_Y`Rtw!;Xf1H!L7@?ItLfexDDA z#rRxPom7U;wci;<2{qm3#_ZV%R?kdBq=m^NS;{MRFF4|GN_}hMN$rGoRZY7nU!Iy@ zrIDP_=v2a$&FXsHv@B(}-EWGl6Mm58z`4ik8l6V?Ed1~$vHYtg%Hs9LM9UmgD9aT2 zPlE#WNyykaXq3wK{4Z)gPmo>)oZq~dD0v0vH2esyo%No`p88@ewF2h{boOW4r zC1~6lEyd=)yftUTUPNrTV_?(t>&U8c@wZA(xP3?0sp|3X;NTYdSSTu{>7DpoIsWA- zH%7WVC9dzzKPL1NK6X-*0KPW-jynw=RSF@?@g4iD2*_>yw?4y;y|$IX+~hQJKpWX? zoccTF(6OnBz)lYnz8lt*X}IVbT>Lp?dXpN4ct;M9_<2LIG*e?Kcx-o4w+D zz|1;jFDz~&!k?$;(#m@v77ns&cO(Plwjf{ zApcZ~n;0NQ+E3_lyq$qI+NCw4!rK~;0;S+(l&u5V7ivNFNCbMC=Pg(Th76s615A?6 z^}O!Yf}z%i3^>O*EX?pYt|?@*d!#Ke+R)!i!PAnF&$xj(h80!3Qw4&!_3s@z6!EzJ zTM>Q;2IwsY&Ae|1=_M1<_};630^@&6H}rHgxRafqywRHTbP;{08jW$0qgQObDiO|n zi~))_3?b<{d5RvIR%ttNK$;|2#fKLo%Y{hM8&LcDGLWa99upZ)C}528!y8~pJxe;r zQ2Q)+J1m4KQ_WQij095sFD1abd!pk97kMI$c%c-|sGMIJ{mmUQCY|gy z;N3)|CiEWB3a+^!stqxqjiOV6#dbFEfTig#0%i^~T_`wZ}DEMxk4F z{IS`RiL+%FH(Rt!=q_k4^?0Sy2_mBtWaI=LDOR1T!z09$MRExDm2?yEO9al1>1b0Q zoiRDMqv+bD2hUD=pl3f9f@kVy>1HGxcB|wX_3T$VXAW{gbQpHgwAb?UEp85kVBdGf zgmSIogjy1jjXghh5ng6_sTSwW1J}GMhmja{pEsNK!Z`Nx^JYfR;`vDJN?|mEv3v%b zA;Ys)=bqy*72cy$VNontob?5taszvXD-jS=w@qQ~VI2Uz7pjv07sNsOL zmTjUebQPI6-y6(-cn^kgWHW0Qo16C_xqB{i^0}->Oy|)f4MdD71S96b9=!2$n@)vA z)4{VyDWqGzKG%ODuL>5#FN;8>~xhwNb#jsY)(CNyOdkh4HP8^TT%Uq+N7 z;X6}DnJ4S3R5jWVh}1_ajMNaklVmVqph6>m6e5WJ|;R|o7uJiNUzS-dTC zEMWn>$dw$A7%NkE8jPc<8!BnfM@(3mU^0^Hz)I*iYUxZ#4Wd;iC5+Ca)J`lk+c99` zBcXRh{!2acejQl4!_l#N8Rq4O=vYB2Ej84!s6lYd%q~LDRE-*x!g5k@z2%~JFE zX^cDNVa+C7rIcz%tF;6&-d?6o%wY!dmRW6L|S z;54ISo7l)B;MoB6%y$5oWmD0!quuCPB6>EMiWAvT#!10>>>}5>Rh%^)v0TL|D!5`z zY{a#|OSnT8*VO|DR2)0rZ}5w!EZjwkQoP^5W{bcWSeN~#!1Ym9_jfaH)Ehs^K4;MnO{bnGOZ$Jwhn zAqhP!(4XVzOCX3e1zg41U>9>0=V=(vX$hz|7b{M7BfmbgcR|I8#M_&EXXHR7R-8I5 z*m60n%&}o!L3l8gv5i=tJ=fWB^D%X1{c-BkNt}6m*C;f5E zR@Gp|`3qWlHu8_)*){6fB%H|PASZ-Q2&^5Fnzgjzw3@Ku zRM4rAHU(_DKy8{?0FL$Kp<^YDxNN>lhiqRN@Rp;cY|NV5IA#~ov(F+6aO$(1ln*iN z9&+?nT0Xdnb59q!a~~^CoB(VY*=+Z8 z#=s`OJ&hI|R>-ZM%e-Mx3ajTHPg-#T;sHL>9E_Mt-B@u>(y5RZ3!X(z#37q?5Tq$z zM9(U{mxHC5)i}-e?EueGgK!Mir_zeU3CYB1to$uUK8IEhT5#BR7OfL<6=x1aYCs_9 z-S%Wn`nHo-A!SF=Za($FZ<-HijmJ=gQgU1uj&=UJ=^O+gy}dQN3j5n7*t>1^Hi0i~ z5v^X>p?eFw&%563_kwFdfMT@si# z9zp+vMo7$DM4?B9ZIA3ybimpej}0)MycoJ_+Or5xRr=>v5MO{mi1)WbZv;-0|9-mR zK3Gw5dm_k6mq)`Ah{#u_o^23OuUYk6{jDcZ*EIP4^b^>3>dov0k>_a?q`wXQn?Z{B z6D`oKQEo&FPB*>{iYif2+I|BlBKOeXx}d=7aqVo93Y>y)tYQjcjh) z|7f%!kgaY>zX?|BJGBDX(%ALsevdM_Otxk5yv@+KIo;R-x;7wYwG^`vDzcP9_6Ioh3q!!>Ea-}h6b~B!4$KD z96iM>IvitS1H~+JA-Zyd$1JxY@JJ(+gvTK3&uR)-!a;VkW5HJdSsR7y?+BUr0ESr( zl~_h0yN?(cDP(_>>R9k21Ti~J74>sr#-hb`4zq_GJ;m%-bWo5%!|Xn~B0j)}+5Mr$ zFfh98F~|l}-{&DyFLK^mh^lCmEkwv}Q^;6#3W$u%z%UbdBW6$1Ff*YA-4ruz4Jb-G zK*P)^!!Qe>kfm_s6tbE~glsc~OqPa_-R2>K<>iwW)bLo8J>3+}LB`6`Q&Ur@E)27W zh*>Sg>^v1&PBEK=2U*7{W^bVd9-#M=?mEVYVMF=%bL8qM|Mi zvM(uQp%gNnoI+L+*~vSu)twf1wE@$?k4d~~pi!>k=$5jXH* z7B=nBN~*#=n{7^;c8G&aon^nBfx2jzWguiD6tW_e*g_#I@Wm)wK%?vrN*4SWqL}re zqO=AYW@pjjx-g0vPtRpD>fkmCnQ0liGQvZaXnAhyAyn~Ln62~6<{|rg>ax$NDunD4 zgshfA#*R>tJ4FA2j6M%B8;Dv9`SfdwS@=D`Y-l+u8qLH4(DND&veP>O3qTS_{sI<& z3UshNqZbRnUG${3;XGFW60aRv2axR$DL|I10DP6UgoBK&u`VAf!poxJG|ZMGW)CQ4 z+fd|SMk~zB&nae$&S5q?h8B!^zXOU=Ye7+0Lk$*yy&eczcmx&zpGgSuqRm(UqNig_ z>`KJ}%gjMf9%OO_pwF@?@G$hh1~dBI3PAt*rd%Gghn-K~M_n|V{fwB2n`t(qBJC8i zm52c|1tB|x7I#2|t~_Pqy-n8hPzB~+1#V%GCETCC(Seb4JwnE6|A8V4C}s%(7&nD9%-%-}R1~x8 zsHls>?1(3ZSv-Y|C#R4V#UW%@C}iDv2w6Q3nd9vUgoZ_Q`@Q7)ike<-5h@&Us^y))=lyDYIWtHFaKCmVfb;60! z_{s7+Q9oIh9Y4z-8GX?&{&M`tXl|@MtSM#M_}}&^DP#+SH(%fd6K4>fG2)e&?-lwJ ze%$+D_OF@JrgrYW&4nbx{*`L(zDF|brsU5ci@Gim**KtQ?7(J4J z!=6Go_#LAg;pp-!$LZ+lL@S;$jFX+NqT*JRkCV}Z3adL=S}AURL94FJ(t5&=b+M

rZdOz%!sTN;VhkO>&5#f7jJh4(Wc zu1jNZFNV?Hyg$QYJ6YukzmL%4f{Dv5+EW?pUInf$yt+~MrCA8QpD_6?vlKcJ@xd?S z=8N8jiNZsN;zHbYnrJuvx&$|b99JSdjZ?v?H+05#8wi{)U!a#p&Krj;w@&R59E!7) z{;7b)cFQ_k?dgJRC~V$zYuU3KCB0AEkaPX=;N4W5y}jwsV$=3>Pi13Ik+#eMmrVe5 z?mmlo7W&pY5ze-`D<-6mGDJ#1L#HnF%#hSRGOrx(7zWe(=1S07$CD#f1Qlk*woHFztXSRcEV3ZpKB!*J;A4XsN&j$w(6TPmQ%0)iEXFz@mq+X zMJlKk8%z#59G_Xo&JzV5^gNNi=cR{f`2GOCfCSU2Y8+?9_*@s9=W* zGkRa(*o?MnF+#bQy{^CtH@K`7_OooMHs<-U(@jG=y}&lWTT{DXgtMm6>}Jh5{Fc7? zh1Og+?!j4;;ARb-#q_KYtr>P%vu8ZNSP8Y}-z*680&~uC=9Fqx`EJ(GyKI+vYr0(4 ztT4D)L*H+6(isTWTy$A;&)an`$4Xyv>!63opvVzihc^;z&Hj!P8cI&>Czyn#&pV@&s?07NQ=x^sUKgn9_xvHGh6?^yM~ z3?2xkccNZ{D)QHOc&n{ktA=KF`@DnPe1f;LusF8QGtrJO*C}!Chbw3k41QQDKWH4b zRG)d79n`LkcxR2~57K}tKgTR1uGGNOfNnhE>xXv%$vT4+W|u+w7rg&v#4fEf z6RudnO|2S6TZpq-knFCNG=Nq^H$7sij0RbLq^O;=5w9}1Z)Vx}Rsq}TmNIIt;uXBD zC?+NOT~~52?Sa?&wA;9+?RwYDA7l{OdDu@e?RgI_G<#H&X delta 16811 zcmZ{L3tW^{`u}<7E{x1@QHF~!TvWUdNJ@q}gMeCOpk|s%!zFWDQZ%>F(3#;Ph_|7! zm0D{@a$DQ1MW=1ew1$gHWxLq28})Auh%Id08jD&g%is4o?>jL5|G&Q<9pQbS`*|+s zJkOb~tFo3aWFc3)k--dqBJeNvPmLjILiR~ZwMG_F?75)Xr4%Y$IUz}kdR3{}RTeT) z)~ffoLUzhkzu2^`;xn&neAuM@58++C|Zd zhfVD*Dp|}W)3Mer)okr1b4#nXJv!nSuI*tlwjDm<2_P{xTTy9RZ_SI+nq!AswXN}a z-E0FMd)4&P^q%poU|M7hO3KN?ulgY4YCHrJ=G6*m1@cV%R7p(nyUZFiJ5*L4vxc=d{dF6QMiVKgkeK5@@6Q2^sQ`0KV z(>aD#VGVlO7!1m$U~hUgQ+u_R8T%r}2zVQBw=!m*L2%#1vZy11fhmFAMDO??k%2SV zO}`z9Wk(FSVIQgA=iwNbLPA;Co=8i z?87I|6jWs_sonqHEALI*f8x^qO^56eyR|CjgTjoxXb=}aIB081-Q#xkj@7Q25r-zo zb&m<&>N)1xIZV&82N?UBu?rJrvob5XR4=$biHM!}*?(`|yxINGndK>MUdJs%*2~Ti+_!jRxbh zpAf)N0;tEwO;bsJ(>oL3J6&dHRCWK#IfaZxk54PfKhj{JrwmW?`&VAFM>1WJ3E4z`9jtPZP3cr3W0U9&V3fg)K~~8GBtf-RLoW>|Dc61^GfoM z-RTN)L<@U8mdJQvY#Y`yadD@!K-Hm&bUk8-wy~FviI#f8UHb$x_*ZhnIAK<=urS-x z;EwbeCpN6f=?boB2|IrxaZs7LaZmB8&>>me+3eJpG&=-cadXqXigR}L?1D>Es|vl< z&!lV^XPMR8dUu3~K3PH!7tseL^cz685q_J5Un1e3lJM6^_%ndt8&csM5Bv&s=90as z;ODceAKn6f6<+zDG9YedZ|nWBo(5~2&pPA4njEI9@Q%NDBJsF7)4I20Rj5}U_v(3w z`=y}!s9!|i1awTK zp6s*E6xo{zJ!MR$TSD(9^kp*L7ZUnogl;?JmA@h3uP6M8zFrC6PWT(gWO^n10m3ho z>Avn?o!Zf{+IhagGU=VR>0-=Tb)!Cg?dXV4x6bdxl7AZJh@6w@RWD%7x-QWtt5XkC z#@u(8qR=+zWAVdCOk4JNgX7|QxwLRx9^%KIZ;mAi+U-4ob( zo%{`!@;5_|(yJ)aUMi|Gt3Eebj9vKQSi8cJUpGc}G9+A4HDQt_`;I)l=J6(@{wo0V z0-yr`P5`9p!WFaKbz|D1x{+p1?#ObvW5QkU#Kha26pK#vY*p?2vjUIo>pq#V&k)Nr zRYI2Tk9fOq-zdx>8Hee+769`K!SI+SI_KxN5FIJ%hq`{i+eO3p&}~P^_sZLYnUpv* z^ILwl;RU1AvM3H|W7vntAL0EH9xuE>FNv;l!4gDql1k00toE+zFYs7Qr30-9dfm7H zo=(p5D}oStUI^gnCW77{@j)zY5yLG=n&FRE+QqXNTcdb7 zHRb1ot1e?))T-wrnLVuvM2w9?GPcdEX)9`DZe|QuA@grhD!|F!aT&Qc*0Mp{;9Rmp zVDpTMPfbNEpE<|Ktv&WmnXD-_C98i>$=nBx@UA7v=UfNlqV5Adr$JwO!EM-cERwn9 zS>++&DyC#lo7nEL^)rq3sOsY61IX}GdL~%ylA;f4^^RVZ| zgi}JX$cE*B&94L5Y)b~4)gqhT@e|V$q0e1``m{=Hgh8 zT+&IuI_72Ib2yMs+eGkLC-TXUKk?*Ls58Qc)ajG>Y>DT5W{P~0p$_NM9Z!4;n>C)l zPCO;pB&!vIO;aG7u1R2H71?+v&;BM2>f{BgBZP~~(>Iy3F^O!ZL!CUX&QxMk+^knK z_e!C&Mksf@+gl@;Uy{L3d#et=j?dlJ$){2d`Bk-Vh73;!%5Y^eWGEG7Fr}SYaR*c# zk%3fAkYp%G<1(a)GNeOQE<<-3$*`f>;Q4mSDL)%y4cI&r$mUuK*lZNpxaSqUx(KS? z9jK~BV$(X0vq=}(WJ1-uxvF;%n}?f?9?kR-Hr_*E^P506KTH9eGLemb(O|?fXfwiw zv?-F zhs5USU7SsZ$R-ckEF*2Y?; ziB0G#&Ssv-W+k-YY*wx!Hjg!Dcr0lnY>eGt^PD*#cuQx1O+^;Z64t_<8%m(fJ%QS^ zhUfDv;V9&6GDSA)pv^s8n?hoL*?anYGn7~=?$I(^Su5X;nr58q)qQ~ z)49M+=YrVBwKx}4O+SXLUKo;S7%0~7Mas8~zmqRXs78r;8r9h#tXBQofO4_nC=j5a!_2UjYs|c`bW9a%$p+D`H4t{oc&bl-FQ!vZ zKNR*Y_(&+&qGnAK4Ny06M#STc6~Aqa!4llRpbJI5zXNY!CefmVb{xi;3v*tys%x0(KF-9`&BCQjMMo?)a5-yZ|Le)Q3jz##p2-8~#rd?@ z6Cn1cE$Al?kgPu+Ia>({ofcyd5 zp)pxS7u@xG<#Eh?xc#r{@8WB0KI&1nj>W*Ont8zULor#^<;gE4t0t3G$HS^;B&+_x`sb{7fSa>EcCx2%0|ZF%cpf6F zE+wnZfMp(&th&B+pYq3Xu<9Eb%RQ~X0O(53_+OG$50O>Z!8Bh=R=rqtckoQYeSFIa zPx2!GZSid11hu9Ku6gll>@Te^YIoy-Y3UDl-{-{j768`TA+slE)`ZyCSgq&y{w_ zQW=UQq3;Q%9qMp1c9es5{qeWN%_eL$>xj$wc+~0w#LrXb_;zqs12RE~#_?mYxV218 z`JwHqlAX5O`QFrky{U=SU*p7g5pm~7ocIlic;^W5HV_voqHIL`94FrIC;rn2@t^+} z;{V~q-CXj2a^mLaMac(8h|AKCK+a$dgu&J~!3gQ>y@k}n2#qF&|Kbc2(;EuIxH>mS zIA*n9b-h#(wVFi#gj3I!sMq)U?UMDsQ1@}_shs-$H_2ATpw5Ypk+$KfDY+mXyFF^5 znCX^3z{S&aM{=ue7(=Nxo?0-^rlu@Q>QypLy`V%ZWv#**`I@$5-V)Qv2T%Xq(%{;* zeU(jYjLkk;I~y%NsWHaeDUN5dr>P#uulp7Cn|!^kPdA}WNk``IW(Y&I4bX_$%#^w@rrV4mr@{S_Z z3nC%+H)dH>R%z#wl-r_ul;+xZye|6=ht0vyY#usyb>V{=R!5db;ZTKi{!WhnXm{4a z!A{)*_I8{Iwr3Pf;9w_j0oyZW^tk)A>UnzSrBkFC|8Ck47mi5*XT8lvI_tIn8y~tM zd{Cclw@X=1E$6k-REMgDP3!qQh@GojuE+9CFRy8Fe2aO(3KU38^^XpzGxa z-TndMZZbl^gvm>B0#w)7wK!%6v9u!cm-~77KN1VU(p8klK1;spdU>0qx93pZm$^UrI z--21WAn7<_=3W1<%mYEeklC!f>N;VIjzR0j4L3WkfZGbG$Uai;8!~?D>a*P~cH65>tj;vr zL!P6lbO--NBMd9ibsUz>>a`dKdB$svMANs!?kcuVw*BWP1V;Bzg#a>-JbLorK)x~+k08a2vdRDgBU>#g!-c0ye@V1VyW`|C34=V z-KxFn%9cHPdm-;6yM?%Im6*LK96gN94mEFRY-vvV#Qp)& z2Ql!0eA*An7VUznCaCH?1Rst*m0FT-?WWl8e9sWk^eqHk1VNSKf8tJ)Yr@(oR{`7E zNW00q2s?ipwxhp(0Gq9dBdIB;t|6^FSq7axGyra0Nz33qOXE|mMDsn+{4f?zV?(du z;Z7_!rdZ)x92pzO;g{~xk_+xG2x1=#&v^vP&zD|W`AE`|{uCJ*>%qV@T#++fkKc8! zHM{579#k%Olb^8bCNx~}zc_wUC@`yI21Skyg{`Y|NjX<_)$dx`aZOr@z1=CTU9aLE$y2`r0vVhJ9_Afh;MiGO2!NvKZtm znvDBer{w87**Hu;regYWFQy+anJgyxswU$R%QUj~?9glkSDwNZSs&`!-yG>msh?nL zeDEJB2=!$XMh288_)tJjU3lGPEO%TfJRW5$eVf^zhg#acq_?z#T8M^N&W;WNPSYZ^ zUK0FCs4eIWy*-YPn|e6Y)jl->2qh{}?GJ6uw1J;(cOZg;J42yR-g9{U{0bMl5mVN`OR!qN>*GkYMeJw6C~+5_?|0 z`%GMriQPs6?Ib!D)7)Bm+KI8X1iOVYXp$-fbF1E$+a?(63iQ=_TL#glxpc$~(01xl zagrKr(0`0wa6_n z#ATozbc}l;`T0tkmkp5QO$QqwO(seHjRTT97dvg(6D**S``0A;rMio-U>xmnzt_Nm z(o;2^b^uJUf8ld@uYi8r*|i$wfGMb0FMEV&J3#wPEocuVkf!THW%ogl!RNIoQMqDs zOsIpP?t^t0_#Bo$6!g5Q#FpQsZsXyl$fB{z&}DI9o}<#M+-U$IaijbNUy4-PC>F$H z$j4q5NX#F+puTY|3EzDY<2~~)`N^NJhByNHHk71!mG8E{s3u|j;G~sppCJRoA;;X1 z6ZY6#i#E%O?pDrDT9893D)-kG5z3iF#R(M2p2dW-kI$1F?IBpBqIezl-m}!{&e~Pb z_L>}CW|(7?IT*^qj~juyd#vU*zCbOyYFMb3_TJ}r(wZpLil=SpxjYXiGiLCed^`?W ztdDE zd_ji`<*s^QU@YZD3n}PEioDP^5+y#05}y<$>Nm@S3ET)VQTN0FSo~O?0f2(MGO2QvLYGUe=|IO&FFsVQH}KSlKLy?tYR3?zL@MoV_X2gQy@kYWRiZ9G<{ zh*Z+xv+m_&h{pJbxa;@Q?)1t6yL_ubnW}Nb!$ZDLCB7-NzwPoziyb?>qqjuMQi_&c zVziho6Q~c>rK{lqqTvBD^gLfFn=#u$v&O82TDbdiep>i3fnsAS$<)ImW~GDHY?l?9 z9Sb7OzAJ%d#(VjxB_79G_BPk-Cmu6TibO2rcFDXc^WCRn48&4{_>M8ZGKV~GR3+q7 zbI`VsS||_KQrz6|$IY*>62pOUnw`sFe+XH-=T|y@p=pGOc!>*QQgzB%$TIs+759P3vD+uGD9K$ z&$wQIR2^;DNc!C*`s(C6A+g(;5NX|hT9oZ%b8vw|7!9L;r4x1h8lA$ zJoTo5JT;asBiZZ8QPJ_g0Z(F$i8`I)4dCiEaQ>*s4w zUqhiUQAwawErD+htTMHCi&f?{;v+PXdMfAJaa;)s4W(r9ipFxM4aQ4cF5)PuGIix( z9qT($y1U-R$s}tcfmSV?7ILhvzLh}SUOll&UOzeBES?G&E>5M1E z_Gu_D|4fP%XY*3S6-(-;D6=gj%?ynuqGA)N(0_ty9Tf8ae<`bbVnmmO$Aj^*1ebsBaI|y3C)0j98vN`K%mr`aPt~N7d zygj_)gptSGSxUvfkz^`J#AP@3vVztu>}^onIFU3vq@i*-%>vDuvln0u?jJ+WI5Ck| z9FfQ|UU4MwXgGqu;6yKQpy1e0al#N&dw9hOql%MPDpi~X@T8{tz={)16(>>8E6yS3 z-rvFwd5XY_6TXG7l;$a3aZI69ajaF8z4qiG6cpj4*s=~PI8CJ37F%KzH0$GXquYfSvmxb?Y98ci4RGh>RvEqdDijz_d^X1<|4zr|@D$Wj)DW_pI zH0$P?El;NG^&Dx|n276t>?tKJS;Y5H?D%w2>==*Z{52wxv|bzFPl@p2RUEP6Z0b~s z73UtT=ae+!yP7IaextNM>pYK&lSmgfr4~xacB(iHX2^0b)|++PXRt$lXkf)z*&(h} zM-~sG9A0p2!Q?U1(kK@0C!tn{?uBOE+}aJLpmuCLt=Xy?syKflNlzxmL$kNJX5%Q3 z*^?p>9>&R$99%ILD(7m&ilci|syK*`;v8OZ_EN!_o~E*a19oa}VkuU4h*gS@F&zg{ zajc>Be5bayC-(sYuM+c^gIAor89;4U)vV?SSpQ2AJe^k$UT|z*EwswTijxjcjf?`yj@xT4>^N}|DLaX`{kaYi)55?t zm0S^}~U(~zkh zmFm_|8^^hslsVp*N~9$44J7uP+^uroC$TF@%bfi!tv1S~bsrlVL!s)!17krfSDTD| z8q;pd4sBHMrE$-#D49#Vrr>qTTixXw3~n7p#YMP;U;? z`h&4=H=<7DUV&w;9cCGhhFI(P01Kjt>^=!^vB#4*$ z-Vpb_1LS+hIJT!2 zlXD34J#YB=#bM-nHoffTpzde*UOD%@pUC$b1AH%$)ZWT{FP!F1jokO1CUy<6-1oA{ z7z3j3?IC44Mc<1Q!MX3vB(W10bKhG>V&@!afwj%EY;|GVU2{2$K;O&Fx!ooDo-rqX zAe(rR?;X!3-y0nDy|=mA6S(i?k{pBF_tJ=6)?)I#C%G}^aobdV7 zAi29l-kAC-Jh$Q{bQ2bP_1i|^f6&@1_#yD_Q}i=VZae6OmJeD97?-&;U(6fY*< z`HUIPQDP$QVPS?>$Ra9Ta^}0_VQ>7>V61`rb9} zdk00|tIPQCDcgFm-*HRcyOLA%l$7_D4VL12HIoaHr|0`G?Mpr7L-jC^B#L@;dK}BBH!zGk?$=W^}QEJj{e0hc$dcISa^!^-iyR- zIP@#{!@64IY@6!*!5YeYuLqG;;}gJ&Z583SlH3Da?p@hD@7+ss-&i8%y^N;Gy z-G>!1@w|5*`Ck3fk(&ErFsYr&eQ!O7%3_q}5?$*3Ko?@8c1 z?VZ)zAh$l8``&hvJ7JROd&2tC+zrIy7T@y}3`xFcJ^ZTzEPhrV`Cisx^1YH#-}{c_ zD9$6_JH_QF;l6i{tYio$-@8V}INwxbqec9Xv}s7?z9+$R-z%L(a$gXA?*USC-%`={ znhrmA^=V=e=zGRZhZ-f{`|^C@7g&6Q3wh7_Yb(lIXDQaky`7dhHR%~JRVB$~;i{RK zS`^G`W!Pr%n-{4`)w7uWFNTN*!?4p-bTB4o{<-#BNk6&%<31^kG(YeuKOCJ&&6&>P zo2sUa{%xC-#dZjE@5ZXC@I}*vlP=_p)mhsk#BY~*`-HNlHu1L4yiEJp6-M#4Po27@ zC`id?Lc>1eoV-?XNM*IFPZkBK*}en}i!}1g`mrm_B7&jUQr46u^MA9ZwB5C!c~@@h zHOvNd=kT$RhUhdTKf9ZnIM_ZfHH=I&wj23GgMUecrU^7(ZAqmAe7i~^Q@Qe=kFZq} zK7Ape%q#E%>6S|W&}2y*pHH}n$SBy52v$@v3dTnj&RfBbi(jHC*ft8rZ|(4rkDppj znT?LnSSL&QDBP;YHrvBm46 zfpwlPjx>Deq^3Ze_EV=C?Tyr!N9aVy@8TrUBx6Gf9cAlzi~o{}PMIQB2A<9|VCIf? z`))hKbo&gyvhu3K=c@i)oow7Jm-dBX8})G3(FW2IqmcSO)FJKKO_W~ez0ElhIMv~X z4o(oc=-Zil#iyE)rvzKx$^vfFIA@V=En_iR7caQH)(Fqa&k&zhjXW)ygvaYlf%jhU z{lkxQp`tiL7YD{xPx$ZG3Q}NwJY0JvAh0r7yw4F3SYnV-cvVt(okMszW5nz8sg`BST7A(5v*8e}gO^VfcEV3U`eV zhL4WUC{y^1Q5+T0R``Me$6iGA-l&m?c8d|sZ_ZGcCZ@a#hh$rsIpx8Tk*Ph4XNR{W zX=*nOiPAJW1Egu8x5GR%AkCShL83Hi0n+fO?xKKL1Zl4MrKuauFYaC%-O9hR;Zp~3 zPKx4`nGHn&((t=@ZvcdBbKWmafjvN)6ZCe_FU=c%X|9L*@6@?lh|?lInFgcQm=e+( z*RA4cCT*kd@yUYzKva7DRL-S}7Ov?UrNX~7*UlFUR4&JC5veF*{gZ835Dm2#_KXm@ zu7+W<$@P8vkHPh0>BiTat#sq73lZHHLpQWCmCvH8yqSuts@u#)w9MP)J}CwmzAQ%N zvTbfX?<G)Yp9g2%89T zi6E8>kiNF!82O;`1oW$|IKh8D?WUi-_}Q#h;0tQYQaakTehtbOb4VxNvZrbO6m*@m z(~PG~R6>$Bl(c@I zUWWm@X3(WU!@(CLS#J#{nhn?Mi9;mciqyfZ=F_A`apo!DwecC#r>$6F{Y>%(!@)m7 zxpJCUoUfp8XMKE3c0Hwf6g0ZD8qfiuJ8q|?s8pjF(^OJA8uLd`Ld;7{y$ZF9FYJ3 diff --git a/heapster-saw/examples/sha512.c b/heapster-saw/examples/sha512.c index a467b2ffaa..b5a9690c00 100644 --- a/heapster-saw/examples/sha512.c +++ b/heapster-saw/examples/sha512.c @@ -235,7 +235,7 @@ static void processBlock(uint64_t *a, uint64_t *b, uint64_t *c, uint64_t *d, const uint8_t *in) { uint64_t s0, s1, T1; uint64_t X[16]; - int i; + uint64_t i; T1 = X[0] = CRYPTO_load_u64_be(in); round_00_15(0, a, b, c, d, e, f, g, h, &T1); diff --git a/heapster-saw/examples/sha512.cry b/heapster-saw/examples/sha512.cry index c118a7c12b..7dbf6f5daf 100644 --- a/heapster-saw/examples/sha512.cry +++ b/heapster-saw/examples/sha512.cry @@ -1,6 +1,8 @@ module SHA512 where +import SpecPrims + // ============================================================================ // Definitions from cryptol-specs/Primitive/Keyless/Hash/SHA512.cry, with some // type annotations added to SIGMA_0, SIGMA_1, sigma_0, and sigma_1 to get @@ -83,3 +85,70 @@ round_16_80_spec i j a b c d e f g h X T1 = X' = update X (j && 15) T1' (a', b', c', d', e', f', g', h', T1'') = round_00_15_spec (i + j) a b c d e f g h T1' + +processBlock_spec : [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> + [16][w] -> + ([w], [w], [w], [w], [w], [w], [w], [w], [16][w]) +processBlock_spec a b c d e f g h in = + processBlock_loop_spec 16 aF bF cF dF eF fF gF hF X T1 in + where (a0,b0,c0,d0,e0,f0,g0,h0,_) = round_00_15_spec 0 a b c d e f g h (in @ ( 0 : [w])) + (h1,a1,b1,c1,d1,e1,f1,g1,_) = round_00_15_spec 1 h0 a0 b0 c0 d0 e0 f0 g0 (in @ ( 1 : [w])) + (g2,h2,a2,b2,c2,d2,e2,f2,_) = round_00_15_spec 2 g1 h1 a1 b1 c1 d1 e1 f1 (in @ ( 2 : [w])) + (f3,g3,h3,a3,b3,c3,d3,e3,_) = round_00_15_spec 3 f2 g2 h2 a2 b2 c2 d2 e2 (in @ ( 3 : [w])) + (e4,f4,g4,h4,a4,b4,c4,d4,_) = round_00_15_spec 4 e3 f3 g3 h3 a3 b3 c3 d3 (in @ ( 4 : [w])) + (d5,e5,f5,g5,h5,a5,b5,c5,_) = round_00_15_spec 5 d4 e4 f4 g4 h4 a4 b4 c4 (in @ ( 5 : [w])) + (c6,d6,e6,f6,g6,h6,a6,b6,_) = round_00_15_spec 6 c5 d5 e5 f5 g5 h5 a5 b5 (in @ ( 6 : [w])) + (b7,c7,d7,e7,f7,g7,h7,a7,_) = round_00_15_spec 7 b6 c6 d6 e6 f6 g6 h6 a6 (in @ ( 7 : [w])) + (a8,b8,c8,d8,e8,f8,g8,h8,_) = round_00_15_spec 8 a7 b7 c7 d7 e7 f7 g7 h7 (in @ ( 8 : [w])) + (h9,a9,b9,c9,d9,e9,f9,g9,_) = round_00_15_spec 9 h8 a8 b8 c8 d8 e8 f8 g8 (in @ ( 9 : [w])) + (gA,hA,aA,bA,cA,dA,eA,fA,_) = round_00_15_spec 10 g9 h9 a9 b9 c9 d9 e9 f9 (in @ (10 : [w])) + (fB,gB,hB,aB,bB,cB,dB,eB,_) = round_00_15_spec 11 fA gA hA aA bA cA dA eA (in @ (11 : [w])) + (eC,fC,gC,hC,aC,bC,cC,dC,_) = round_00_15_spec 12 eB fB gB hB aB bB cB dB (in @ (12 : [w])) + (dD,eD,fD,gD,hD,aD,bD,cD,_) = round_00_15_spec 13 dC eC fC gC hC aC bC cC (in @ (13 : [w])) + (cE,dE,eE,fE,gE,hE,aE,bE,_) = round_00_15_spec 14 cD dD eD fD gD hD aD bD (in @ (14 : [w])) + (bF,cF,dF,eF,fF,gF,hF,aF,T1) = round_00_15_spec 15 bE cE dE eE fE gE hE aE (in @ (15 : [w])) + X = [in @ ( 0 : [w]), in @ ( 1 : [w]), in @ ( 2 : [w]), in @ ( 3 : [w]), + in @ ( 4 : [w]), in @ ( 5 : [w]), in @ ( 6 : [w]), in @ ( 7 : [w]), + in @ ( 8 : [w]), in @ ( 9 : [w]), in @ (10 : [w]), in @ (11 : [w]), + in @ (12 : [w]), in @ (13 : [w]), in @ (14 : [w]), in @ (15 : [w])] + +processBlock_loop_spec : [w] -> + [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> + [16][w] -> [w] -> [16][w] -> + ([w], [w], [w], [w], [w], [w], [w], [w], [16][w]) +processBlock_loop_spec i a b c d e f g h X T1 in = + if i < 80 then processBlock_loop_spec (i+16) aF bF cF dF eF fF gF hF XF T1F in + else (a,b,c,d,e,f,g,h,in) + where (a0,b0,c0,d0,e0,f0,g0,h0,X0,_,_,T10) = round_16_80_spec i 0 a b c d e f g h X T1 + (h1,a1,b1,c1,d1,e1,f1,g1,X1,_,_,T11) = round_16_80_spec i 1 h0 a0 b0 c0 d0 e0 f0 g0 X0 T10 + (g2,h2,a2,b2,c2,d2,e2,f2,X2,_,_,T12) = round_16_80_spec i 2 g1 h1 a1 b1 c1 d1 e1 f1 X1 T11 + (f3,g3,h3,a3,b3,c3,d3,e3,X3,_,_,T13) = round_16_80_spec i 3 f2 g2 h2 a2 b2 c2 d2 e2 X2 T12 + (e4,f4,g4,h4,a4,b4,c4,d4,X4,_,_,T14) = round_16_80_spec i 4 e3 f3 g3 h3 a3 b3 c3 d3 X3 T13 + (d5,e5,f5,g5,h5,a5,b5,c5,X5,_,_,T15) = round_16_80_spec i 5 d4 e4 f4 g4 h4 a4 b4 c4 X4 T14 + (c6,d6,e6,f6,g6,h6,a6,b6,X6,_,_,T16) = round_16_80_spec i 6 c5 d5 e5 f5 g5 h5 a5 b5 X5 T15 + (b7,c7,d7,e7,f7,g7,h7,a7,X7,_,_,T17) = round_16_80_spec i 7 b6 c6 d6 e6 f6 g6 h6 a6 X6 T16 + (a8,b8,c8,d8,e8,f8,g8,h8,X8,_,_,T18) = round_16_80_spec i 8 a7 b7 c7 d7 e7 f7 g7 h7 X7 T17 + (h9,a9,b9,c9,d9,e9,f9,g9,X9,_,_,T19) = round_16_80_spec i 9 h8 a8 b8 c8 d8 e8 f8 g8 X8 T18 + (gA,hA,aA,bA,cA,dA,eA,fA,XA,_,_,T1A) = round_16_80_spec i 10 g9 h9 a9 b9 c9 d9 e9 f9 X9 T19 + (fB,gB,hB,aB,bB,cB,dB,eB,XB,_,_,T1B) = round_16_80_spec i 11 fA gA hA aA bA cA dA eA XA T1A + (eC,fC,gC,hC,aC,bC,cC,dC,XC,_,_,T1C) = round_16_80_spec i 12 eB fB gB hB aB bB cB dB XB T1B + (dD,eD,fD,gD,hD,aD,bD,cD,XD,_,_,T1D) = round_16_80_spec i 13 dC eC fC gC hC aC bC cC XC T1C + (cE,dE,eE,fE,gE,hE,aE,bE,XE,_,_,T1E) = round_16_80_spec i 14 cD dD eD fD gD hD aD bD XD T1D + (bF,cF,dF,eF,fF,gF,hF,aF,XF,_,_,T1F) = round_16_80_spec i 15 bE cE dE eE fE gE hE aE XE T1E + +processBlocks_spec : {n} Literal n [64] => [8][w] -> [16*n][w] -> + ([8][w], [16*n][w]) +processBlocks_spec = processBlocks_loop_spec 0 `n + +processBlocks_loop_spec : {n} Literal n [64] => [w] -> [w] -> [8][w] -> + [16*n][w] -> ([8][w], [16*n][w]) +processBlocks_loop_spec i j state in = invariantHint (i + j == `n) ( + if j != 0 then processBlocks_loop_spec (i+1) (j-1) state' in + else (state, in)) + where (a,b,c,d,e,f,g,h) = (state @ ( 0 : [w]), state @ ( 1 : [w]), + state @ ( 2 : [w]), state @ ( 3 : [w]), + state @ ( 4 : [w]), state @ ( 5 : [w]), + state @ ( 6 : [w]), state @ ( 7 : [w])) + in_i = split in @ i + (a',b',c',d',e',f',g',h',_) = processBlock_spec a b c d e f g h in_i + state' = [a', b', c', d', e', f', g', h'] diff --git a/heapster-saw/examples/sha512.saw b/heapster-saw/examples/sha512.saw index f5b470e4a5..6624a9f6fc 100644 --- a/heapster-saw/examples/sha512.saw +++ b/heapster-saw/examples/sha512.saw @@ -7,11 +7,17 @@ heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x) heapster_define_perm env "int32" " " "llvmptr 32" "exists x:bv 32.eq(llvmword(x))"; heapster_define_perm env "int8" " " "llvmptr 8" "exists x:bv 8.eq(llvmword(x))"; +// FIXME: We always have rw=W, but without the rw arguments below Heapster +// doesn't realize the perm is not copyable (it needs to unfold named perms). +heapster_define_perm env "int64_ptr" "rw:rwmodality" "llvmptr 64" "ptr((rw,0) |-> int64<>)"; +heapster_define_perm env "true_ptr" "rw:rwmodality" "llvmptr 64" "ptr((rw,0) |-> true)"; + heapster_assume_fun env "CRYPTO_load_u64_be" "(). arg0:ptr((R,0) |-> int64<>) -o \ \ arg0:ptr((R,0) |-> int64<>), ret:int64<>" "\\ (x:Vec 64 Bool) -> returnM (Vec 64 Bool * Vec 64 Bool) (x, x)"; +/* heapster_typecheck_fun env "return_state" "(). arg0:array(W,0,<8,*8,fieldsh(int64<>)) -o \ \ arg0:array(W,0,<8,*8,fieldsh(int64<>))"; @@ -24,5 +30,50 @@ heapster_typecheck_fun env "sha512_block_data_order" \ arg0:array(W,0,<8,*8,fieldsh(int64<>)), \ \ arg1:array(R,0,<16*num,*8,fieldsh(int64<>)), \ \ arg2:true, ret:true"; +*/ + +heapster_typecheck_fun env "round_00_15" + "(). arg0:int64<>, \ + \ arg1:int64_ptr, arg2:int64_ptr, arg3:int64_ptr, arg4:int64_ptr, \ + \ arg5:int64_ptr, arg6:int64_ptr, arg7:int64_ptr, arg8:int64_ptr, \ + \ arg9:int64_ptr -o \ + \ arg1:int64_ptr, arg2:int64_ptr, arg3:int64_ptr, arg4:int64_ptr, \ + \ arg5:int64_ptr, arg6:int64_ptr, arg7:int64_ptr, arg8:int64_ptr, \ + \ arg9:int64_ptr, ret:true"; + +heapster_typecheck_fun env "round_16_80" + "(). arg0:int64<>, arg1:int64<>, \ + \ arg2:int64_ptr, arg3:int64_ptr, arg4:int64_ptr, arg5:int64_ptr, \ + \ arg6:int64_ptr, arg7:int64_ptr, arg8:int64_ptr, arg9:int64_ptr, \ + \ arg10:array(W,0,<16,*8,fieldsh(int64<>)), \ + \ arg11:true_ptr, arg12:true_ptr, arg13:int64_ptr -o \ + \ arg2:int64_ptr, arg3:int64_ptr, arg4:int64_ptr, arg5:int64_ptr, \ + \ arg6:int64_ptr, arg7:int64_ptr, arg8:int64_ptr, arg9:int64_ptr, \ + \ arg10:array(W,0,<16,*8,fieldsh(int64<>)), \ + \ arg11:int64_ptr, arg12:int64_ptr, arg13:int64_ptr, ret:true"; + +heapster_typecheck_fun env "return_X" + "(). arg0:array(W,0,<16,*8,fieldsh(int64<>)) -o \ + \ arg0:array(W,0,<16,*8,fieldsh(int64<>))"; + +heapster_set_translation_checks env false; +heapster_typecheck_fun env "processBlock" + "(). arg0:int64_ptr, arg1:int64_ptr, arg2:int64_ptr, \ + \ arg3:int64_ptr, arg4:int64_ptr, arg5:int64_ptr, \ + \ arg6:int64_ptr, arg7:int64_ptr, \ + \ arg8:array(R,0,<16,*8,fieldsh(int64<>)) -o \ + \ arg0:int64_ptr, arg1:int64_ptr, arg2:int64_ptr, \ + \ arg3:int64_ptr, arg4:int64_ptr, arg5:int64_ptr, \ + \ arg6:int64_ptr, arg7:int64_ptr, \ + \ arg8:array(R,0,<16,*8,fieldsh(int64<>)), ret:true"; + +heapster_set_translation_checks env false; +heapster_typecheck_fun env "processBlocks" + "(num:bv 64). arg0:array(W,0,<8,*8,fieldsh(int64<>)), \ + \ arg1:array(R,0,<16*num,*8,fieldsh(int64<>)), \ + \ arg2:eq(llvmword(num)) -o \ + \ arg0:array(W,0,<8,*8,fieldsh(int64<>)), \ + \ arg1:array(R,0,<16*num,*8,fieldsh(int64<>)), \ + \ arg2:true, ret:true"; heapster_export_coq env "sha512_gen.v"; diff --git a/heapster-saw/examples/sha512_mr_solver.saw b/heapster-saw/examples/sha512_mr_solver.saw index 928e7ab40f..7b063e1d00 100644 --- a/heapster-saw/examples/sha512_mr_solver.saw +++ b/heapster-saw/examples/sha512_mr_solver.saw @@ -1,84 +1,4 @@ -enable_experimental; -env <- heapster_init_env "SHA512" "sha512.bc"; - -// Heapster - -heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))"; -heapster_define_perm env "int32" " " "llvmptr 32" "exists x:bv 32.eq(llvmword(x))"; -heapster_define_perm env "int8" " " "llvmptr 8" "exists x:bv 8.eq(llvmword(x))"; - -// FIXME: We always have rw=W, but without the rw arguments below Heapster -// doesn't realize the perm is not copyable (it needs to unfold named perms). -heapster_define_perm env "int64_ptr" "rw:rwmodality" "llvmptr 64" "ptr((rw,0) |-> int64<>)"; -heapster_define_perm env "true_ptr" "rw:rwmodality" "llvmptr 64" "ptr((rw,0) |-> true)"; - -heapster_assume_fun env "CRYPTO_load_u64_be" - "(). arg0:ptr((R,0) |-> int64<>) -o \ - \ arg0:ptr((R,0) |-> int64<>), ret:int64<>" - "\\ (x:Vec 64 Bool) -> returnM (Vec 64 Bool * Vec 64 Bool) (x, x)"; - -heapster_typecheck_fun env "round_00_15" - "(). arg0:int64<>, \ - \ arg1:int64_ptr, arg2:int64_ptr, arg3:int64_ptr, arg4:int64_ptr, \ - \ arg5:int64_ptr, arg6:int64_ptr, arg7:int64_ptr, arg8:int64_ptr, \ - \ arg9:int64_ptr -o \ - \ arg1:int64_ptr, arg2:int64_ptr, arg3:int64_ptr, arg4:int64_ptr, \ - \ arg5:int64_ptr, arg6:int64_ptr, arg7:int64_ptr, arg8:int64_ptr, \ - \ arg9:int64_ptr, ret:true"; - -heapster_typecheck_fun env "round_16_80" - "(). arg0:int64<>, arg1:int64<>, \ - \ arg2:int64_ptr, arg3:int64_ptr, arg4:int64_ptr, arg5:int64_ptr, \ - \ arg6:int64_ptr, arg7:int64_ptr, arg8:int64_ptr, arg9:int64_ptr, \ - \ arg10:array(W,0,<16,*8,fieldsh(int64<>)), \ - \ arg11:true_ptr, arg12:true_ptr, arg13:int64_ptr -o \ - \ arg2:int64_ptr, arg3:int64_ptr, arg4:int64_ptr, arg5:int64_ptr, \ - \ arg6:int64_ptr, arg7:int64_ptr, arg8:int64_ptr, arg9:int64_ptr, \ - \ arg10:array(W,0,<16,*8,fieldsh(int64<>)), \ - \ arg11:int64_ptr, arg12:int64_ptr, arg13:int64_ptr, ret:true"; - -heapster_typecheck_fun env "return_X" - "(). arg0:array(W,0,<16,*8,fieldsh(int64<>)) -o \ - \ arg0:array(W,0,<16,*8,fieldsh(int64<>))"; - -heapster_set_translation_checks env false; -heapster_typecheck_fun env "processBlock" - "(). arg0:int64_ptr, arg1:int64_ptr, arg2:int64_ptr, \ - \ arg3:int64_ptr, arg4:int64_ptr, arg5:int64_ptr, \ - \ arg6:int64_ptr, arg7:int64_ptr, \ - \ arg8:array(R,0,<16,*8,fieldsh(int64<>)) -o \ - \ arg0:int64_ptr, arg1:int64_ptr, arg2:int64_ptr, \ - \ arg3:int64_ptr, arg4:int64_ptr, arg5:int64_ptr, \ - \ arg6:int64_ptr, arg7:int64_ptr, \ - \ arg8:array(R,0,<16,*8,fieldsh(int64<>)), ret:true"; - -// FIXME: This translation contains errors -heapster_set_translation_checks env false; -heapster_typecheck_fun env "processBlocks" - "(num:bv 64). arg0:array(W,0,<8,*8,fieldsh(int64<>)), \ - \ arg1:array(R,0,<16*num,*8,fieldsh(int64<>)), \ - \ arg2:eq(llvmword(num)) -o \ - \ arg0:array(W,0,<8,*8,fieldsh(int64<>)), \ - \ arg1:array(R,0,<16*num,*8,fieldsh(int64<>)), \ - \ arg2:true, ret:true"; - -heapster_export_coq env "sha512_mr_solver_gen.v"; - -// Mr. Solver - -let eq_bool b1 b2 = - if b1 then - if b2 then true else false - else - if b2 then false else true; - -let fail = do { print "Test failed"; exit 1; }; -let run_test name test expected = - do { if expected then print (str_concat "Test: " name) else - print (str_concat (str_concat "Test: " name) " (expecting failure)"); - actual <- test; - if eq_bool actual expected then print "Success\n" else - do { print "Test failed\n"; exit 1; }; }; +include "sha512.saw"; round_00_15 <- parse_core_mod "SHA512" "round_00_15"; round_16_80 <- parse_core_mod "SHA512" "round_16_80"; @@ -100,10 +20,14 @@ monadify_term {{ sigma_0 }}; monadify_term {{ sigma_1 }}; monadify_term {{ Ch }}; monadify_term {{ Maj }}; - -// FIXME: Why does monadification fail without this line while running -// "round_16_80 |= round_16_80_spec"? monadify_term {{ round_00_15_spec }}; +monadify_term {{ round_16_80_spec }}; +monadify_term {{ processBlock_loop_spec }}; +monadify_term {{ processBlock_spec }}; +// monadify_term {{ processBlocks_loop_spec }}; +// monadify_term {{ processBlocks_spec }}; mr_solver_prove round_00_15 {{ round_00_15_spec }}; mr_solver_prove round_16_80 {{ round_16_80_spec }}; +// mr_solver_assume processBlock {{ processBlock_spec }}; +// mr_solver_prove processBlocks {{ processBlocks_spec }}; diff --git a/heapster-saw/examples/sha512_proofs.v b/heapster-saw/examples/sha512_proofs.v index 143fa9204c..ad4fd7101b 100644 --- a/heapster-saw/examples/sha512_proofs.v +++ b/heapster-saw/examples/sha512_proofs.v @@ -13,15 +13,3 @@ Import SAWCorePrelude. Require Import Examples.sha512_gen. Import SHA512. - -Definition sha512_block_data_order_precond num := isBvslt 64 (intToBv 64 0) num. - -Lemma no_errors_sha512_block_data_order : - refinesFun sha512_block_data_order - (fun num _ _ => assumingM (sha512_block_data_order_precond num) noErrorsSpec). -Proof. - unfold sha512_block_data_order, sha512_block_data_order__tuple_fun. - (* time "sha512_block_data_order (1)" prove_refinement_match_letRecM_l. *) - (* 1-2: intros; apply noErrorsSpec. *) - (* time "sha512_block_data_order (2)" prove_refinement. *) -Admitted. From 5fd71ac4b5b736145d4637b8dafbaf5fe93c8cdb Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Wed, 1 Jun 2022 12:15:30 -0700 Subject: [PATCH 02/17] add scBvLit --- saw-core/src/Verifier/SAW/SharedTerm.hs | 14 +++++++-- src/SAWScript/Prover/MRSolver/Monad.hs | 42 +++++++++++++++++-------- src/SAWScript/Prover/MRSolver/SMT.hs | 2 +- src/SAWScript/Prover/MRSolver/Solver.hs | 15 +++------ 4 files changed, 47 insertions(+), 26 deletions(-) diff --git a/saw-core/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs index 4a8cde027a..d0cfae71e7 100644 --- a/saw-core/src/Verifier/SAW/SharedTerm.hs +++ b/saw-core/src/Verifier/SAW/SharedTerm.hs @@ -212,6 +212,7 @@ module Verifier.SAW.SharedTerm , scBvToNat , scBvAt , scBvConst + , scBvLit , scFinVal , scBvForall , scUpdBvFun @@ -2019,14 +2020,23 @@ scBvToNat sc n x = do n' <- scNat sc n scGlobalApply sc "Prelude.bvToNat" [n',x] --- | Create a term computing a bitvector of the given length representing the --- given 'Integer' value (if possible). +-- | Create a @bvNat@ term computing a bitvector of the given length +-- representing the given 'Integer' value (if possible). scBvConst :: SharedContext -> Natural -> Integer -> IO Term scBvConst sc w v = assert (w <= fromIntegral (maxBound :: Int)) $ do x <- scNat sc w y <- scNat sc $ fromInteger $ v .&. (1 `shiftL` fromIntegral w - 1) scGlobalApply sc "Prelude.bvNat" [x, y] +-- | Create a vector literal term computing a bitvector of the given length +-- representing the given 'Integer' value (if possible). +scBvLit :: SharedContext -> Natural -> Integer -> IO Term +scBvLit sc w v = assert (w <= fromIntegral (maxBound :: Int)) $ do + do bool_tp <- scBoolType sc + bits <- mapM (scBool sc . testBit v) + [(fromIntegral w - 1), (fromIntegral w - 2) .. 0] + scVector sc bool_tp bits + -- TODO: This doesn't appear to be used anywhere, and "FinVal" doesn't appear -- in Prelude.sawcore... can this be deleted? -- | FinVal :: (x r :: Nat) -> Fin (Succ (addNat r x)); diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs index dbb20fd7e7..3595aff8e3 100644 --- a/src/SAWScript/Prover/MRSolver/Monad.hs +++ b/src/SAWScript/Prover/MRSolver/Monad.hs @@ -26,7 +26,6 @@ module SAWScript.Prover.MRSolver.Monad where import Data.List (find, findIndex, foldl') import qualified Data.Text as T import Numeric.Natural (Natural) -import Data.Bits (testBit) import System.IO (hPutStrLn, stderr) import Control.Monad.Reader import Control.Monad.State @@ -267,10 +266,6 @@ instance PrettyInCtx DataTypeAssump where prettyInCtx (IsNum x) = prettyInCtx x >>= ppWithPrefix "TCNum" prettyInCtx IsInf = return "TCInf" --- | Create a term representing the type @IsFinite n@ -mrIsFinite :: Term -> MRM Term -mrIsFinite n = liftSC2 scGlobalApply "CryptolM.isFinite" [n] - -- | A map from 'Term's to 'DataTypeAssump's over that term type DataTypeAssumps = HashMap Term DataTypeAssump @@ -445,6 +440,35 @@ liftSC5 :: (SharedContext -> a -> b -> c -> d -> e -> IO f) -> liftSC5 f a b c d e = mrSC >>= \sc -> liftIO (f sc a b c d e) +---------------------------------------------------------------------- +-- * Functions for Building Terms +---------------------------------------------------------------------- + +-- | Create a term representing the type @IsFinite n@ +mrIsFinite :: Term -> MRM Term +mrIsFinite n = liftSC2 scGlobalApply "CryptolM.isFinite" [n] + +-- | Create a term representing an application of @Prelude.error@ +mrErrorTerm :: Term -> T.Text -> MRM Term +mrErrorTerm a str = + do err_str <- liftSC1 scString str + liftSC2 scGlobalApply "Prelude.error" [a, err_str] + +-- | Create a term representing an application of @Prelude.genBVVecFromVec@, +-- where the default value argument is @Prelude.error@ of the given 'T.Text' +mrGenBVVecFromVec :: Term -> Term -> Term -> T.Text -> Term -> Term -> MRM Term +mrGenBVVecFromVec m a v def_err_str n len = + do err_tm <- mrErrorTerm a def_err_str + liftSC2 scGlobalApply "Prelude.genBVVecFromVec" [m, a, v, err_tm, n, len] + +-- | Create a term representing an application of @Prelude.genFromBVVec@, +-- where the default value argument is @Prelude.error@ of the given 'T.Text' +mrGenFromBVVec :: Term -> Term -> Term -> Term -> T.Text -> Term -> MRM Term +mrGenFromBVVec n len a v def_err_str m = + do err_tm <- mrErrorTerm a def_err_str + liftSC2 scGlobalApply "Prelude.genFromBVVec" [n, len, a, v, err_tm, m] + + ---------------------------------------------------------------------- -- * Monadic Operations on Terms ---------------------------------------------------------------------- @@ -488,14 +512,6 @@ mrBvToNat _ (asArrayValue -> Just (asBoolType -> Just _, liftSC1 scNat $ foldl' (\n bit -> if bit then 2*n+1 else 2*n) 0 bits mrBvToNat n len = liftSC2 scBvNat n len --- | Like 'scBvConst', but returns a bitvector literal -mrBvConst :: Natural -> Integer -> MRM Term -mrBvConst n x = - do bool_tp <- liftSC0 scBoolType - bits <- mapM (liftSC1 scBool . testBit x) - [(fromIntegral n - 1), (fromIntegral n - 2) .. 0] - liftSC2 scVector bool_tp bits - -- | Get the current context of uvars as a list of variable names and their -- types as SAW core 'Term's, with the least recently bound uvar first, i.e., in -- the order as seen "from the outside" diff --git a/src/SAWScript/Prover/MRSolver/SMT.hs b/src/SAWScript/Prover/MRSolver/SMT.hs index 70bf769020..65486b53ca 100644 --- a/src/SAWScript/Prover/MRSolver/SMT.hs +++ b/src/SAWScript/Prover/MRSolver/SMT.hs @@ -118,7 +118,7 @@ primBVTermFun sc = VExtra (VExtraTerm _ w_tm) -> return w_tm VWord (Left (_,w_tm)) -> return w_tm VWord (Right bv) -> - lift $ scBvConst sc (fromIntegral (Prim.width bv)) (Prim.unsigned bv) + lift $ scBvLit sc (fromIntegral (Prim.width bv)) (Prim.unsigned bv) VVector vs -> lift $ do tms <- traverse (boolValToTerm sc <=< force) (V.toList vs) diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs index 002317237c..34804a6b7c 100644 --- a/src/SAWScript/Prover/MRSolver/Solver.hs +++ b/src/SAWScript/Prover/MRSolver/Solver.hs @@ -296,11 +296,8 @@ normComp (CompTerm t) = i)]) -> do body <- mrGlobalDefBody "CryptolM.bvVecAtM" if n < 1 `shiftL` fromIntegral w then do - n' <- mrBvConst w (toInteger n) - err_str <- liftSC1 scString "FIXME: normComp (atM) error" - err_tm <- liftSC2 scGlobalApply "Prelude.error" [a, err_str] - xs' <- liftSC2 scGlobalApply "Prelude.genBVVecFromVec" - [n_tm, a, xs, err_tm, w_tm, n'] + n' <- liftSC2 scBvLit w (toInteger n) + xs' <- mrGenBVVecFromVec n_tm a xs "normComp (atM)" w_tm n' mrApplyAll body [w_tm, n', a, xs', i] >>= normCompTerm else throwMRFailure (MalformedComp t) @@ -323,11 +320,9 @@ normComp (CompTerm t) = i), x]) -> do body <- mrGlobalDefBody "CryptolM.fromBVVecUpdateM" if n < 1 `shiftL` fromIntegral w then do - n' <- mrBvConst w (toInteger n) - err_str <- liftSC1 scString "FIXME: normComp (updateM) error" - err_tm <- liftSC2 scGlobalApply "Prelude.error" [a, err_str] - xs' <- liftSC2 scGlobalApply "Prelude.genBVVecFromVec" - [n_tm, a, xs, err_tm, w_tm, n'] + n' <- liftSC2 scBvLit w (toInteger n) + xs' <- mrGenBVVecFromVec n_tm a xs "normComp (updateM)" w_tm n' + err_tm <- mrErrorTerm a "normComp (updateM)" mrApplyAll body [w_tm, n', a, xs', i, x, err_tm, n_tm] >>= normCompTerm else throwMRFailure (MalformedComp t) From ab5aaa46f48cb7bbddc888e304688ff7959cd801 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Wed, 1 Jun 2022 12:26:52 -0700 Subject: [PATCH 03/17] improvements to Mr. Solver debug printing --- src/SAWScript/Prover/MRSolver/Monad.hs | 4 ++-- src/SAWScript/Prover/MRSolver/SMT.hs | 8 +++---- src/SAWScript/Prover/MRSolver/Solver.hs | 13 +++++----- src/SAWScript/Prover/MRSolver/Term.hs | 32 +++++++++++++++++-------- 4 files changed, 34 insertions(+), 23 deletions(-) diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs index 3595aff8e3..1b113fec30 100644 --- a/src/SAWScript/Prover/MRSolver/Monad.hs +++ b/src/SAWScript/Prover/MRSolver/Monad.hs @@ -250,9 +250,9 @@ instance PrettyInCtx CoIndHyp where (case invar2 of Just f -> prettyTermApp f args2 Nothing -> return "True"), return "=>", - prettyInCtx (FunBind f1 args1 CompFunReturn), + prettyTermApp (funNameTerm f1) args1, return "|=", - prettyInCtx (FunBind f2 args2 CompFunReturn)] + prettyTermApp (funNameTerm f2) args2] -- | An assumption that something is equal to one of the constructors of a -- datatype, e.g. equal to @Left@ of some 'Term' or @Right@ of some 'Term' diff --git a/src/SAWScript/Prover/MRSolver/SMT.hs b/src/SAWScript/Prover/MRSolver/SMT.hs index 65486b53ca..379f57709b 100644 --- a/src/SAWScript/Prover/MRSolver/SMT.hs +++ b/src/SAWScript/Prover/MRSolver/SMT.hs @@ -415,12 +415,12 @@ mrAssertProveEq = mrAssertProveRel False mrProveRel :: Bool -> Term -> Term -> MRM Bool mrProveRel het t1 t2 = do let nm = if het then "mrProveRel" else "mrProveEq" - mrDebugPPPrefixSep 1 nm t1 (if het then "~=" else "==") t2 + mrDebugPPPrefixSep 2 nm t1 (if het then "~=" else "==") t2 tp1 <- mrTypeOf t1 >>= mrSubstEVars tp2 <- mrTypeOf t2 >>= mrSubstEVars cond_in_ctx <- mrProveRelH het tp1 tp2 t1 t2 res <- withTermInCtx cond_in_ctx mrProvable - debugPrint 1 $ nm ++ ": " ++ if res then "Success" else "Failure" + debugPrint 2 $ nm ++ ": " ++ if res then "Success" else "Failure" return res -- | Prove that two terms are related, heterogeneously iff the first argument, @@ -461,7 +461,7 @@ mrProveRelH' var_map _ tp1 tp2 (asEVarApp var_map -> Just (evar, args, Nothing)) t2' <- mrSubstEVars t2 success <- mrTrySetAppliedEVar evar args t2' when success $ - mrDebugPPPrefixSep 2 "mrProveRelH setting evar" evar "to" t2 + mrDebugPPPrefixSep 1 "setting evar" evar "to" t2 TermInCtx [] <$> liftSC1 scBool success -- If t2 is an instantiated evar, substitute and recurse @@ -477,7 +477,7 @@ mrProveRelH' var_map _ tp1 tp2 t1 (asEVarApp var_map -> Just (evar, args, Nothin t1' <- mrSubstEVars t1 success <- mrTrySetAppliedEVar evar args t1' when success $ - mrDebugPPPrefixSep 2 "mrProveRelH setting evar" evar "to" t1 + mrDebugPPPrefixSep 1 "setting evar" evar "to" t1 TermInCtx [] <$> liftSC1 scBool success -- For unit types, always return true diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs index 34804a6b7c..d3a05a958e 100644 --- a/src/SAWScript/Prover/MRSolver/Solver.hs +++ b/src/SAWScript/Prover/MRSolver/Solver.hs @@ -531,8 +531,6 @@ proveCoIndHyp hyp = -- NOTE: the state automatically gets reset here because we defined -- MRM with ExceptT at a lower level than StateT do mrDebugPPPrefixSep 1 "Widening recursive assumption for" nm1' "|=" nm2' - debugPrint 2 ("Widening indices: " ++ - intercalate ", " (map show new_vars)) hyp' <- generalizeCoIndHyp hyp new_vars proveCoIndHyp hyp' e -> throwError e @@ -542,7 +540,8 @@ proveCoIndHyp hyp = -- given arguments, otherwise throw an exception saying that widening is needed matchCoIndHyp :: CoIndHyp -> [Term] -> [Term] -> MRM () matchCoIndHyp hyp args1 args2 = - do (args1', args2') <- instantiateCoIndHyp hyp + do mrDebugPPPrefix 1 "matchCoIndHyp" hyp + (args1', args2') <- instantiateCoIndHyp hyp eqs1 <- zipWithM mrProveEq args1' args1 eqs2 <- zipWithM mrProveEq args2' args2 if and (eqs1 ++ eqs2) then return () else @@ -556,17 +555,15 @@ generalizeCoIndHyp :: CoIndHyp -> [Either Int Int] -> MRM CoIndHyp generalizeCoIndHyp hyp [] = return hyp generalizeCoIndHyp hyp all_specs@(arg_spec:arg_specs) = withOnlyUVars (coIndHypCtx hyp) $ do - mrDebugPPPrefixSep 2 "generalizeCoIndHyp" hyp "with arg specs" (show all_specs) + withNoUVars $ mrDebugPPPrefixSep 2 "generalizeCoIndHyp with indices" + all_specs "on" hyp -- Get the arg and type associated with arg_spec let arg = coIndHypArg hyp arg_spec arg_tp <- mrTypeOf arg - ctx <- mrUVarCtx - debugPretty 2 ("Current context: " <> ppCtx ctx) -- Sort out the other args that equal arg eq_uneq_specs <- forM arg_specs $ \spec' -> do let arg' = coIndHypArg hyp spec' tp' <- mrTypeOf arg' - mrDebugPPPrefixSep 2 "generalizeCoIndHyp: the type of" arg' "is" tp' tps_eq <- mrConvertible arg_tp tp' args_eq <- if tps_eq then mrProveEq arg arg' else return False return $ if args_eq then Left spec' else Right spec' @@ -613,6 +610,8 @@ mrRefines t1 t2 = do m1 <- toNormComp t1 m2 <- toNormComp t2 mrDebugPPPrefixSep 1 "mrRefines" m1 "|=" m2 + -- ctx <- reverse . map (\(a,Type b) -> (a,b)) <$> mrUVars + -- mrDebugPPPrefix 2 "in context:" $ ppCtx ctx withFailureCtx (FailCtxRefines m1 m2) $ mrRefines' m1 m2 -- | The main implementation of 'mrRefines' diff --git a/src/SAWScript/Prover/MRSolver/Term.hs b/src/SAWScript/Prover/MRSolver/Term.hs index ef093df317..7d855cc86e 100644 --- a/src/SAWScript/Prover/MRSolver/Term.hs +++ b/src/SAWScript/Prover/MRSolver/Term.hs @@ -384,6 +384,9 @@ instance TermLike Term where instance TermLike FunName where liftTermLike _ _ = return substTermLike _ _ = return +instance TermLike LocalName where + liftTermLike _ _ = return + substTermLike _ _ = return deriving instance TermLike Type deriving instance TermLike NormComp @@ -426,16 +429,15 @@ prettyTermApp f_top args = -- | FIXME: move this helper function somewhere better... ppCtx :: [(LocalName,Term)] -> SawDoc -ppCtx = helper [] where - helper :: [LocalName] -> [(LocalName,Term)] -> SawDoc - helper _ [] = "" +ppCtx = align . sep . helper [] where + helper :: [LocalName] -> [(LocalName,Term)] -> [SawDoc] + helper _ [] = [] + helper ns [(n,tp)] = + [ppTermInCtx defaultPPOpts (n:ns) (Unshared $ LocalVar 0) <> ":" <> + ppTermInCtx defaultPPOpts ns tp] helper ns ((n,tp):ctx) = - let ns' = n:ns in - ppTermInCtx defaultPPOpts ns' (Unshared $ LocalVar 0) <> ":" <> - ppTermInCtx defaultPPOpts ns tp <> ", " <> helper ns' ctx - -instance PrettyInCtx String where - prettyInCtx str = return $ fromString str + (ppTermInCtx defaultPPOpts (n:ns) (Unshared $ LocalVar 0) <> ":" <> + ppTermInCtx defaultPPOpts ns tp <> ",") : (helper (n:ns) ctx) instance PrettyInCtx SawDoc where prettyInCtx pp = return pp @@ -446,13 +448,23 @@ instance PrettyInCtx Type where instance PrettyInCtx MRVar where prettyInCtx (MRVar ec) = return $ ppName $ ecName ec -instance PrettyInCtx [Term] where +instance PrettyInCtx a => PrettyInCtx [a] where prettyInCtx xs = list <$> mapM prettyInCtx xs +instance {-# OVERLAPPING #-} PrettyInCtx String where + prettyInCtx str = return $ fromString str + +instance PrettyInCtx Int where + prettyInCtx i = return $ viaShow i + instance PrettyInCtx a => PrettyInCtx (Maybe a) where prettyInCtx (Just x) = (<+>) "Just" <$> prettyInCtx x prettyInCtx Nothing = return "Nothing" +instance (PrettyInCtx a, PrettyInCtx b) => PrettyInCtx (Either a b) where + prettyInCtx (Left a) = (<+>) "Left" <$> prettyInCtx a + prettyInCtx (Right b) = (<+>) "Right" <$> prettyInCtx b + instance (PrettyInCtx a, PrettyInCtx b) => PrettyInCtx (a,b) where prettyInCtx (x, y) = (\x' y' -> parens (x' <> "," <> y')) <$> prettyInCtx x <*> prettyInCtx y From d679d8f5c781d257d8c284d72d8a4691b41b9717 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Wed, 1 Jun 2022 12:35:01 -0700 Subject: [PATCH 04/17] add a Type to CompFunReturn --- src/SAWScript/Prover/MRSolver/Monad.hs | 10 +++- src/SAWScript/Prover/MRSolver/Solver.hs | 69 ++++++++++++++++--------- src/SAWScript/Prover/MRSolver/Term.hs | 29 +++++------ 3 files changed, 65 insertions(+), 43 deletions(-) diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs index 1b113fec30..19f23ae01a 100644 --- a/src/SAWScript/Prover/MRSolver/Monad.hs +++ b/src/SAWScript/Prover/MRSolver/Monad.hs @@ -919,8 +919,8 @@ mrGetFunAssump nm = Map.lookup nm <$> mrFunAssumps -- are 'Term's that can have the current uvars free withFunAssump :: FunName -> [Term] -> NormComp -> MRM a -> MRM a withFunAssump fname args rhs m = - do mrDebugPPPrefixSep 1 "withFunAssump" (FunBind - fname args CompFunReturn) "|=" rhs + do k <- CompFunReturn <$> Type <$> mrFunOutType fname args + mrDebugPPPrefixSep 1 "withFunAssump" (FunBind fname args k) "|=" rhs ctx <- mrUVarCtx assumps <- mrFunAssumps let assump = FunAssump ctx args (RewriteFunAssump rhs) @@ -996,6 +996,12 @@ withDataTypeAssump x assump m = mrGetDataTypeAssump :: Term -> MRM (Maybe DataTypeAssump) mrGetDataTypeAssump x = HashMap.lookup x <$> mrDataTypeAssumps +-- | Convert a 'FunAssumpRHS' to a 'NormComp' +mrFunAssumpRHSAsNormComp :: FunAssumpRHS -> MRM NormComp +mrFunAssumpRHSAsNormComp (OpaqueFunAssump f args) = + FunBind f args <$> CompFunReturn <$> Type <$> mrFunOutType f args +mrFunAssumpRHSAsNormComp (RewriteFunAssump rhs) = return rhs + -- | Print a 'String' if the debug level is at least the supplied 'Int' debugPrint :: Int -> String -> MRM () debugPrint i str = diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs index d3a05a958e..ee65f481ad 100644 --- a/src/SAWScript/Prover/MRSolver/Solver.hs +++ b/src/SAWScript/Prover/MRSolver/Solver.hs @@ -353,10 +353,12 @@ normComp (CompTerm t) = -- FIXME: substitute for evars if they have been instantiated ((asExtCns -> Just ec), args) -> do fun_name <- extCnsToFunName ec - return $ FunBind fun_name args CompFunReturn + fun_tp <- Type <$> mrFunOutType fun_name args + return $ FunBind fun_name args (CompFunReturn fun_tp) ((asGlobalFunName -> Just f), args) -> - return $ FunBind f args CompFunReturn + do fun_tp <- Type <$> mrFunOutType f args + return $ FunBind f args (CompFunReturn fun_tp) _ -> throwMRFailure (MalformedComp t) @@ -380,34 +382,42 @@ normBind (ForallM tp f) k = return $ ForallM tp (compFunComp f k) normBind (FunBind f args k1) k2 -- Turn `bvVecMapInvarM ... >>= k` into `bvVecMapInvarBindM ... k` | GlobalName (globalDefString -> "CryptolM.bvVecMapInvarM") [] <- f - , not (isCompFunReturn (compFunComp k1 k2)) = + , (a:b:args_rest) <- args = do f' <- mrGlobalDef "CryptolM.bvVecMapInvarBindM" cont <- compFunToTerm (compFunComp k1 k2) - return $ FunBind f' (args ++ [cont]) CompFunReturn + c <- compFunReturnType k2 + return $ FunBind f' ((a:b:c:args_rest) ++ [cont]) + (CompFunReturn (Type c)) -- Turn `bvVecMapInvarBindM ... k1 >>= k2` into -- `bvVecMapInvarBindM ... (composeM ... k1 k2)` | GlobalName (globalDefString -> "CryptolM.bvVecMapInvarBindM") [] <- f - , (args_pre, [cont]) <- splitAt 8 args - , not (isCompFunReturn (compFunComp k1 k2)) = + , (args_pre, [cont]) <- splitAt 8 args = do cont' <- compFunToTerm (compFunComp (compFunComp (CompFunTerm cont) k1) k2) - return $ FunBind f (args_pre ++ [cont']) CompFunReturn + c <- compFunReturnType k2 + return $ FunBind f (args_pre ++ [cont']) (CompFunReturn (Type c)) | otherwise = return $ FunBind f args (compFunComp k1 k2) -- | Bind a 'Term' for a computation with a function and normalize normBindTerm :: Term -> CompFun -> MRM NormComp normBindTerm t f = normCompTerm t >>= \m -> normBind m f +-- | Get the return type of a 'CompFun' +compFunReturnType :: CompFun -> MRM Term +compFunReturnType (CompFunTerm t) = mrTypeOf t +compFunReturnType (CompFunComp _ g) = compFunReturnType g +compFunReturnType (CompFunReturn (Type t)) = return t + -- | Apply a computation function to a term argument to get a computation applyCompFun :: CompFun -> Term -> MRM Comp applyCompFun (CompFunComp f g) t = -- (f >=> g) t == f t >>= g do comp <- applyCompFun f t return $ CompBind comp g -applyCompFun CompFunReturn t = +applyCompFun (CompFunReturn _) t = return $ CompReturn t applyCompFun (CompFunTerm f) t = CompTerm <$> mrApplyAll f [t] --- | Convert a 'CompFun' which is not a 'CompFunReturn' into a 'Term' +-- | Convert a 'CompFun' into a 'Term' compFunToTerm :: CompFun -> MRM Term compFunToTerm (CompFunTerm t) = return t compFunToTerm (CompFunComp f g) = @@ -418,9 +428,16 @@ compFunToTerm (CompFunComp f g) = case (f_tp, g_tp) of (asPi -> Just (_, a, asCompM -> Just b), asPi -> Just (_, _, asCompM -> Just c)) -> - liftSC2 scGlobalApply "Prelude.composeM" [a, b, c, f', g'] + -- we explicitly unfold @Prelude.composeM@ here so @mrApplyAll@ will + -- beta-reduce + let nm = maybe "ret_val" id (compFunVarName f) in + mrLambdaLift [(nm, a)] (b, c, f', g') $ \[arg] (b', c', f'', g'') -> + do app <- mrApplyAll f'' [arg] + liftSC2 scGlobalApply "Prelude.bindM" [b', c', app, g''] _ -> error "compFunToTerm: type(s) not of the form: a -> CompM b" -compFunToTerm CompFunReturn = error "compFunToTerm: got a CompFunReturn" +compFunToTerm (CompFunReturn (Type a)) = + mrLambdaLift [("ret_val", a)] a $ \[ret_val] (a') -> + liftSC2 scGlobalApply "Prelude.returnM" [a', ret_val] -- | Convert a 'Comp' into a 'Term' compToTerm :: Comp -> MRM Term @@ -428,7 +445,7 @@ compToTerm (CompTerm t) = return t compToTerm (CompReturn t) = do tp <- mrTypeOf t liftSC2 scGlobalApply "Prelude.returnM" [tp, t] -compToTerm (CompBind m CompFunReturn) = compToTerm m +compToTerm (CompBind m (CompFunReturn _)) = compToTerm m compToTerm (CompBind m f) = do m' <- compToTerm m f' <- compFunToTerm f @@ -760,7 +777,7 @@ mrRefines' m1@(FunBind (EVarFunName _) _ _) m2 = mrRefines' m1 m2@(FunBind (EVarFunName _) _ _) = throwMRFailure (CompsDoNotRefine m1 m2) {- -mrRefines' (FunBind (EVarFunName evar) args CompFunReturn) m2 = +mrRefines' (FunBind (EVarFunName evar) args (CompFunReturn _)) m2 = mrGetEVar evar >>= \case Just f -> (mrApplyAll f args >>= normCompTerm) >>= \m1' -> @@ -812,11 +829,12 @@ mrRefines' m1@(FunBind f1 args1 k1) m2@(FunBind f2 args2 k2) = -- f1 args1' refines some f args where f /= f2 and f2 does not match the -- case above, treat either case like we have a rewrite FunAssump and prove -- that args1 = args1' and then that f args refines m2 - (_, Just (FunAssump ctx args1' (funAssumpRHSAsNormComp -> rhs))) -> - do evars <- mrFreshEVars ctx - (args1'', rhs') <- substTermLike 0 evars (args1', rhs) + (_, Just (FunAssump ctx args1' rhs)) -> + do rhs' <- mrFunAssumpRHSAsNormComp rhs + evars <- mrFreshEVars ctx + (args1'', rhs'') <- substTermLike 0 evars (args1', rhs') zipWithM_ mrAssertProveEq args1'' args1 - m1' <- normBind rhs' k1 + m1' <- normBind rhs'' k1 mrRefines m1' m2 -- If f1 unfolds and is not recursive in itself, unfold it and recurse @@ -851,11 +869,12 @@ mrRefines' m1@(FunBind f1 args1 k1) m2 = -- If we have an assumption that f1 args' refines some rhs, then prove that -- args1 = args' and then that rhs refines m2 - Just (FunAssump ctx args1' (funAssumpRHSAsNormComp -> rhs)) -> - do evars <- mrFreshEVars ctx - (args1'', rhs') <- substTermLike 0 evars (args1', rhs) + Just (FunAssump ctx args1' rhs) -> + do rhs' <- mrFunAssumpRHSAsNormComp rhs + evars <- mrFreshEVars ctx + (args1'', rhs'') <- substTermLike 0 evars (args1', rhs') zipWithM_ mrAssertProveEq args1'' args1 - m1' <- normBind rhs' k1 + m1' <- normBind rhs'' k1 mrRefines m1' m2 -- Otherwise, see if we can unfold f1 @@ -883,7 +902,7 @@ mrRefines' m1 m2@(FunBind f2 args2 k2) = -- proving m1 |= f2_body under the assumption that m1 |= f2 args2 {- FIXME: implement something like this Just (f2_body, True) - | CompFunReturn <- k2 -> + | CompFunReturn _ <- k2 -> withFunAssumpR m1 f2 args2 $ -} @@ -925,7 +944,7 @@ mrRefines'' m1 m2 = throwMRFailure (CompsDoNotRefine m1 m2) -- | Prove that one function refines another for all inputs mrRefinesFun :: CompFun -> CompFun -> MRM () -mrRefinesFun CompFunReturn CompFunReturn = return () +mrRefinesFun (CompFunReturn _) (CompFunReturn _) = return () mrRefinesFun f1 f2 | Just nm <- compFunVarName f1 `mplus` compFunVarName f2 , Just tp <- compFunInputType f1 `mplus` compFunInputType f2 = @@ -1037,14 +1056,14 @@ askMRSolverH _ (asCompM -> Just _) t1 (asCompM -> Just _) t2 = case (m1, m2) of -- If t1 and t2 are both named functions, our result is the opaque -- FunAssump that forall xs. f1 xs |= f2 xs' - (FunBind f1 args1 CompFunReturn, FunBind f2 args2 CompFunReturn) -> + (FunBind f1 args1 (CompFunReturn _), FunBind f2 args2 (CompFunReturn _)) -> mrUVarCtx >>= \uvar_ctx -> return $ Just (f1, FunAssump { fassumpCtx = uvar_ctx, fassumpArgs = args1, fassumpRHS = OpaqueFunAssump f2 args2 }) -- If just t1 is a named function, our result is the rewrite FunAssump -- that forall xs. f1 xs |= m2 - (FunBind f1 args1 CompFunReturn, _) -> + (FunBind f1 args1 (CompFunReturn _), _) -> mrUVarCtx >>= \uvar_ctx -> return $ Just (f1, FunAssump { fassumpCtx = uvar_ctx, fassumpArgs = args1, diff --git a/src/SAWScript/Prover/MRSolver/Term.hs b/src/SAWScript/Prover/MRSolver/Term.hs index 7d855cc86e..5ce92c0cb6 100644 --- a/src/SAWScript/Prover/MRSolver/Term.hs +++ b/src/SAWScript/Prover/MRSolver/Term.hs @@ -131,21 +131,21 @@ data CompFun -- | An arbitrary term = CompFunTerm Term -- | A special case for the term @\ (x:a) -> returnM a x@ - | CompFunReturn + | CompFunReturn Type -- | The monadic composition @f >=> g@ | CompFunComp CompFun CompFun deriving (Generic, Show) -- | Compose two 'CompFun's, simplifying if one is a 'CompFunReturn' compFunComp :: CompFun -> CompFun -> CompFun -compFunComp CompFunReturn f = f -compFunComp f CompFunReturn = f +compFunComp (CompFunReturn _) f = f +compFunComp f (CompFunReturn _) = f compFunComp f g = CompFunComp f g -- | If a 'CompFun' contains an explicit lambda-abstraction, then return the -- textual name bound by that lambda compFunVarName :: CompFun -> Maybe LocalName -compFunVarName (CompFunTerm (asLambda -> Just (nm, _, _))) = Just nm +compFunVarName (CompFunTerm t) = asLambdaName t compFunVarName (CompFunComp f _) = compFunVarName f compFunVarName _ = Nothing @@ -154,13 +154,9 @@ compFunVarName _ = Nothing compFunInputType :: CompFun -> Maybe Type compFunInputType (CompFunTerm (asLambda -> Just (_, tp, _))) = Just $ Type tp compFunInputType (CompFunComp f _) = compFunInputType f +compFunInputType (CompFunReturn t) = Just t compFunInputType _ = Nothing --- | Returns true iff the given 'CompFun' is 'CompFunReturn' -isCompFunReturn :: CompFun -> Bool -isCompFunReturn CompFunReturn = True -isCompFunReturn _ = False - -- | A computation of type @CompM a@ for some @a@ data Comp = CompTerm Term | CompBind Comp CompFun | CompReturn Term deriving (Generic, Show) @@ -223,6 +219,11 @@ asNonBVVecVectorType :: Recognizer Term (Term, Term) asNonBVVecVectorType (asBVVecType -> Just _) = Nothing asNonBVVecVectorType t = asVectorType t +-- | Like 'asLambda', but only return's the lambda-bound variable's 'LocalName' +asLambdaName :: Recognizer Term LocalName +asLambdaName (asLambda -> Just (nm, _, _)) = Just nm +asLambdaName _ = Nothing + ---------------------------------------------------------------------- -- * Mr Solver Environments @@ -233,11 +234,6 @@ asNonBVVecVectorType t = asVectorType t data FunAssumpRHS = OpaqueFunAssump FunName [Term] | RewriteFunAssump NormComp --- | Convert a 'FunAssumpRHS' to a 'NormComp' -funAssumpRHSAsNormComp :: FunAssumpRHS -> NormComp -funAssumpRHSAsNormComp (OpaqueFunAssump f args) = FunBind f args CompFunReturn -funAssumpRHSAsNormComp (RewriteFunAssump rhs) = rhs - -- | An assumption that a named function refines some specification. This has -- the form -- @@ -490,7 +486,8 @@ instance PrettyInCtx Comp where instance PrettyInCtx CompFun where prettyInCtx (CompFunTerm t) = prettyInCtx t - prettyInCtx CompFunReturn = return "returnM" + prettyInCtx (CompFunReturn t) = + prettyAppList [return "returnM", parens <$> prettyInCtx t] prettyInCtx (CompFunComp f g) = prettyAppList [prettyInCtx f, return ">=>", prettyInCtx g] @@ -527,7 +524,7 @@ instance PrettyInCtx NormComp where prettyInCtx (ForallM tp f) = prettyAppList [return "forallM", prettyInCtx tp, return "_", parens <$> prettyInCtx f] - prettyInCtx (FunBind f args CompFunReturn) = + prettyInCtx (FunBind f args (CompFunReturn _)) = prettyTermApp (funNameTerm f) args prettyInCtx (FunBind f [] k) = prettyAppList [prettyInCtx f, return ">>=", prettyInCtx k] From dcf57a106f5cf7b986ff7b9267927de7689f808a Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Wed, 1 Jun 2022 12:36:03 -0700 Subject: [PATCH 05/17] fix infinite loop edge case in normComp --- src/SAWScript/Prover/MRSolver/Solver.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs index ee65f481ad..7d29169253 100644 --- a/src/SAWScript/Prover/MRSolver/Solver.hs +++ b/src/SAWScript/Prover/MRSolver/Solver.hs @@ -212,7 +212,7 @@ normComp (CompTerm t) = (>>) (mrDebugPPPrefix 3 "normCompTerm:" t) $ withFailureCtx (FailCtxMNF t) $ case asApplyAll t of - (f@(asLambda -> Just _), args) -> + (f@(asLambda -> Just _), args@(_:_)) -> mrApplyAll f args >>= normCompTerm (isGlobalDef "Prelude.returnM" -> Just (), [_, x]) -> return $ ReturnM x From ffec443ea039283a3811d6f10d930d65de12b15d Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Wed, 1 Jun 2022 12:52:20 -0700 Subject: [PATCH 06/17] actually add bound on BVVec ix and add BVVec/BVVec case in mrProveRelH' --- src/SAWScript/Prover/MRSolver/SMT.hs | 56 +++++++++++++++++++++------- 1 file changed, 42 insertions(+), 14 deletions(-) diff --git a/src/SAWScript/Prover/MRSolver/SMT.hs b/src/SAWScript/Prover/MRSolver/SMT.hs index 379f57709b..5368f569c6 100644 --- a/src/SAWScript/Prover/MRSolver/SMT.hs +++ b/src/SAWScript/Prover/MRSolver/SMT.hs @@ -361,9 +361,10 @@ mrEq' _ _ _ = error "mrEq': unsupported type" -- "outside in", meaning the highest deBruijn index comes first data TermInCtx = TermInCtx [(LocalName,Term)] Term --- | Conjoin two 'TermInCtx's, assuming they both have Boolean type -andTermInCtx :: TermInCtx -> TermInCtx -> MRM TermInCtx -andTermInCtx (TermInCtx ctx1 t1) (TermInCtx ctx2 t2) = +-- | Lift a binary operation on 'Term's to one on 'TermInCtx's +liftTermInCtx2 :: (SharedContext -> Term -> Term -> IO Term) -> + TermInCtx -> TermInCtx -> MRM TermInCtx +liftTermInCtx2 op (TermInCtx ctx1 t1) (TermInCtx ctx2 t2) = do -- Insert the variables in ctx2 into the context of t1 starting at index 0, -- by lifting its variables starting at 0 by length ctx2 @@ -372,7 +373,7 @@ andTermInCtx (TermInCtx ctx1 t1) (TermInCtx ctx2 t2) = -- length ctx2, by lifting its variables starting at length ctx2 by length -- ctx1 t2' <- liftTermLike (length ctx2) (length ctx1) t2 - TermInCtx (ctx1++ctx2) <$> liftSC2 scAnd t1' t2' + TermInCtx (ctx1++ctx2) <$> liftSC2 op t1' t2' -- | Extend the context of a 'TermInCtx' with additional universal variables -- bound "outside" the 'TermInCtx' @@ -520,16 +521,43 @@ mrProveRelH' _ het tp1@(asBVVecType -> Just (n1, len1, tpA1)) liftSC0 scBoolType >>= \bool_tp -> liftSC2 scVecType n1 bool_tp >>= \ix_tp -> withUVarLift "eq_ix" (Type ix_tp) (n1,(len1,(tpA1,(tpA2,(t1,t2))))) $ - \ix' (n1',(len1',(tpA1',(tpA2',(t1',t2'))))) -> - liftSC2 scGlobalApply "Prelude.is_bvult" [n1', ix', len1'] >>= \pf_tp -> - withUVarLift "eq_pf" (Type pf_tp) (n1',(len1',(tpA1',(tpA2',(ix',(t1',t2')))))) $ - \pf'' (n1'',(len1'',(tpA1'',(tpA2'',(ix'',(t1'',t2'')))))) -> - do t1_prj <- liftSC2 scGlobalApply "Prelude.atBVVec" [n1'', len1'', tpA1'', - t1'', ix'', pf''] - t2_prj <- liftSC2 scGlobalApply "Prelude.atBVVec" [n1'', len1'', tpA2'', - t2'', ix'', pf''] - extTermInCtx [("eq_ix",ix_tp),("eq_pf",pf_tp)] <$> - mrProveRelH het tpA1'' tpA2'' t1_prj t2_prj + \ix (n1',(len1',(tpA1',(tpA2',(t1',t2'))))) -> + do ix_bound <- liftSC2 scGlobalApply "Prelude.bvult" [n1', ix, len1'] + pf <- liftSC2 scGlobalApply "Prelude.unsafeAssertBVULt" [n1', ix, len1'] + t1_prj <- liftSC2 scGlobalApply "Prelude.atBVVec" [n1', len1', tpA1', + t1', ix, pf] + t2_prj <- liftSC2 scGlobalApply "Prelude.atBVVec" [n1', len1', tpA2', + t2', ix, pf] + cond <- mrProveRelH het tpA1' tpA2' t1_prj t2_prj + extTermInCtx [("eq_ix",ix_tp)] <$> + liftTermInCtx2 scImplies (TermInCtx [] ix_bound) cond + +-- For non-BVVec vector types where at least one side is an application of +-- genFromBVVec, wrap both sides in genBVVecFromVec and recurse +mrProveRelH' _ het tp1@(asNonBVVecVectorType -> Just (m1, tpA1)) + tp2@(asNonBVVecVectorType -> Just (m2, tpA2)) + t1@(asGenFromBVVecTerm -> Just (n, len, _, _, _, _)) t2 = + do ms_are_eq <- mrConvertible m1 m2 + if ms_are_eq then return () else + throwMRFailure (TypesNotEq (Type tp1) (Type tp2)) + len' <- liftSC2 scGlobalApply "Prelude.bvToNat" [n, len] + tp1' <- liftSC2 scVecType len' tpA1 + tp2' <- liftSC2 scVecType len' tpA2 + t1' <- mrGenBVVecFromVec m1 tpA1 t1 "mrProveRelH (BVVec/BVVec)" n len + t2' <- mrGenBVVecFromVec m2 tpA2 t2 "mrProveRelH (BVVec/BVVec)" n len + mrProveRelH het tp1' tp2' t1' t2' +mrProveRelH' _ het tp1@(asNonBVVecVectorType -> Just (m1, tpA1)) + tp2@(asNonBVVecVectorType -> Just (m2, tpA2)) + t1 t2@(asGenFromBVVecTerm -> Just (n, len, _, _, _, _)) = + do ms_are_eq <- mrConvertible m1 m2 + if ms_are_eq then return () else + throwMRFailure (TypesNotEq (Type tp1) (Type tp2)) + len' <- liftSC2 scGlobalApply "Prelude.bvToNat" [n, len] + tp1' <- liftSC2 scVecType len' tpA1 + tp2' <- liftSC2 scVecType len' tpA2 + t1' <- mrGenBVVecFromVec m1 tpA1 t1 "mrProveRelH (BVVec/BVVec)" n len + t2' <- mrGenBVVecFromVec m2 tpA2 t2 "mrProveRelH (BVVec/BVVec)" n len + mrProveRelH het tp1' tp2' t1' t2' -- If our relation is heterogeneous and we have a BVVec on one side and a -- non-BVVec vector on the other, wrap the non-BVVec vector term in From 506b07270fdb4c9b0f43340d0bbe54f863b058a4 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Wed, 1 Jun 2022 13:09:57 -0700 Subject: [PATCH 07/17] make mrRefinesFun, generalizeCoIndHypArgs het., add het. interface --- heapster-saw/examples/sha512_mr_solver.saw | 2 +- src/SAWScript/Prover/MRSolver/Monad.hs | 114 ++++++- src/SAWScript/Prover/MRSolver/SMT.hs | 108 +++--- src/SAWScript/Prover/MRSolver/Solver.hs | 370 +++++++++++++-------- 4 files changed, 400 insertions(+), 194 deletions(-) diff --git a/heapster-saw/examples/sha512_mr_solver.saw b/heapster-saw/examples/sha512_mr_solver.saw index 7b063e1d00..587ab8a528 100644 --- a/heapster-saw/examples/sha512_mr_solver.saw +++ b/heapster-saw/examples/sha512_mr_solver.saw @@ -29,5 +29,5 @@ monadify_term {{ processBlock_spec }}; mr_solver_prove round_00_15 {{ round_00_15_spec }}; mr_solver_prove round_16_80 {{ round_16_80_spec }}; -// mr_solver_assume processBlock {{ processBlock_spec }}; +mr_solver_prove processBlock {{ processBlock_spec }}; // mr_solver_prove processBlocks {{ processBlocks_spec }}; diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs index 19f23ae01a..2bd3888fb7 100644 --- a/src/SAWScript/Prover/MRSolver/Monad.hs +++ b/src/SAWScript/Prover/MRSolver/Monad.hs @@ -59,13 +59,14 @@ import SAWScript.Prover.MRSolver.Term -- | The context in which a failure occurred data FailCtx = FailCtxRefines NormComp NormComp + | FailCtxCoIndHyp CoIndHyp | FailCtxMNF Term deriving Show -- | That's MR. Failure to you data MRFailure = TermsNotRel Bool Term Term - | TypesNotEq Type Type + | TypesNotRel Bool Type Type | CompsDoNotRefine NormComp NormComp | ReturnNotError Term | FunsNotEq FunName FunName @@ -89,6 +90,9 @@ data MRFailure pattern TermsNotEq :: Term -> Term -> MRFailure pattern TermsNotEq t1 t2 = TermsNotRel False t1 t2 +pattern TypesNotEq :: Type -> Type -> MRFailure +pattern TypesNotEq t1 t2 = TypesNotRel False t1 t2 + -- | Remove the context from a 'MRFailure', i.e. remove all applications of the -- 'MRFailureLocalVar' and 'MRFailureCtx' constructors mrFailureWithoutCtx :: MRFailure -> MRFailure @@ -118,6 +122,9 @@ instance PrettyInCtx FailCtx where prettyInCtx (FailCtxRefines m1 m2) = group <$> nest 2 <$> ppWithPrefixSep "When proving refinement:" m1 "|=" m2 + prettyInCtx (FailCtxCoIndHyp hyp) = + group <$> nest 2 <$> + ppWithPrefix "When doing co-induction with hypothesis:" hyp prettyInCtx (FailCtxMNF t) = group <$> nest 2 <$> vsepM [return "When normalizing computation:", prettyInCtx t] @@ -127,8 +134,10 @@ instance PrettyInCtx MRFailure where ppWithPrefixSep "Could not prove terms equal:" t1 "and" t2 prettyInCtx (TermsNotRel True t1 t2) = ppWithPrefixSep "Could not prove terms heterogeneously related:" t1 "and" t2 - prettyInCtx (TypesNotEq tp1 tp2) = + prettyInCtx (TypesNotRel False tp1 tp2) = ppWithPrefixSep "Types not equal:" tp1 "and" tp2 + prettyInCtx (TypesNotRel True tp1 tp2) = + ppWithPrefixSep "Types not heterogeneously related:" tp1 "and" tp2 prettyInCtx (CompsDoNotRefine m1 m2) = ppWithPrefixSep "Could not prove refinement: " m1 "|=" m2 prettyInCtx (ReturnNotError t) = @@ -236,6 +245,28 @@ coIndHypArg :: CoIndHyp -> Either Int Int -> Term coIndHypArg hyp (Left i) = (coIndHypLHS hyp) !! i coIndHypArg hyp (Right i) = (coIndHypRHS hyp) !! i +-- | Set the @i@th argument on either the left- or right-hand side of a +-- coinductive hypothesis to the given value +coIndHypSetArg :: CoIndHyp -> Either Int Int -> Term -> CoIndHyp +coIndHypSetArg hyp@(CoIndHyp {..}) (Left i) x = + hyp { coIndHypLHS = take i coIndHypLHS ++ x : drop (i+1) coIndHypLHS } +coIndHypSetArg hyp@(CoIndHyp {..}) (Right i) x = + hyp { coIndHypRHS = take i coIndHypRHS ++ x : drop (i+1) coIndHypRHS } + +-- | Set all of the arguments in the given list to the given value in a +-- coinductive hypothesis, using 'coIndHypSetArg' +coIndHypSetArgs :: CoIndHyp -> [Either Int Int] -> Term -> CoIndHyp +coIndHypSetArgs hyp specs x = + foldl' (\hyp' spec -> coIndHypSetArg hyp' spec x) hyp specs + +-- | Add a variable to the context of a coinductive hypothesis, returning the +-- updated coinductive hypothesis and a 'Term' which is the new variable +coIndHypWithVar :: CoIndHyp -> LocalName -> Type -> MRM (CoIndHyp, Term) +coIndHypWithVar (CoIndHyp ctx f1 f2 args1 args2 invar1 invar2) nm (Type tp) = + do var <- liftSC1 scLocalVar 0 + (args1', args2') <- liftTermLike 0 1 (args1, args2) + return (CoIndHyp (ctx ++ [(nm,tp)]) f1 f2 args1' args2' invar1 invar2, var) + -- | A map from pairs of function names to co-inductive hypotheses over those -- names type CoIndHyps = Map (FunName, FunName) CoIndHyp @@ -440,6 +471,59 @@ liftSC5 :: (SharedContext -> a -> b -> c -> d -> e -> IO f) -> liftSC5 f a b c d e = mrSC >>= \sc -> liftIO (f sc a b c d e) +---------------------------------------------------------------------- +-- * Relating Types Heterogeneously +---------------------------------------------------------------------- + +-- | A datatype encapsulating all the way in which we consider two types to +-- be heterogeneously related: either one is a @Num@ and the other is a @Nat@, +-- one is a @BVVec@ and the other is a non-@BVVec@ vector (of the same length, +-- this is checked in 'matchHet'), or both sides are pairs (whose components +-- are respectively heterogeneously related, this recursion must be done where +-- 'matchHet' is used, see 'typesHetRelated', for example) +data HetRelated = HetBVNum Natural + | HetNumBV Natural + | HetBVVecVec (Term, Term, Term) (Term, Term) + | HetVecBVVec (Term, Term) (Term, Term, Term) + | HetPair (Term, Term) (Term, Term) + +-- | Check to see if the given types match one of the cases of 'HetRelated' +matchHet :: Term -> Term -> MRM (Maybe HetRelated) +matchHet (asBitvectorType -> Just n) + (asDataType -> Just (primName -> "Cryptol.Num", _)) = + return $ Just $ HetBVNum n +matchHet (asDataType -> Just (primName -> "Cryptol.Num", _)) + (asBitvectorType -> Just n) = + return $ Just $ HetNumBV n +matchHet (asBVVecType -> Just (n, len, a)) + (asNonBVVecVectorType -> Just (m, a')) = + do m' <- mrBvToNat n len + ms_are_eq <- mrConvertible m' m + return $ if ms_are_eq then Just $ HetBVVecVec (n, len, a) (m, a') + else Nothing +matchHet (asNonBVVecVectorType -> Just (m, a')) + (asBVVecType -> Just (n, len, a)) = + do m' <- mrBvToNat n len + ms_are_eq <- mrConvertible m' m + return $ if ms_are_eq then Just $ HetVecBVVec (m, a') (n, len, a) + else Nothing +matchHet (asPairType -> Just (tpL1, tpR1)) + (asPairType -> Just (tpL2, tpR2)) = + return $ Just $ HetPair (tpL1, tpR1) (tpL2, tpR2) +matchHet _ _ = return $ Nothing + +-- | Return true iff the given types are heterogeneously related +typesHetRelated :: Term -> Term -> MRM Bool +typesHetRelated tp1 tp2 = matchHet tp1 tp2 >>= \case + Just (HetBVNum _) -> return True + Just (HetNumBV _) -> return True + Just (HetBVVecVec (_, _, a) (_, a')) -> typesHetRelated a a' + Just (HetVecBVVec (_, a') (_, _, a)) -> typesHetRelated a' a + Just (HetPair (tpL1, tpR1) (tpL2, tpR2)) -> + (&&) <$> typesHetRelated tpL1 tpL2 <*> typesHetRelated tpR1 tpR2 + Nothing -> mrConvertible tp1 tp2 + + ---------------------------------------------------------------------- -- * Functions for Building Terms ---------------------------------------------------------------------- @@ -504,6 +588,10 @@ funNameType (GlobalName gd projs) = mrApplyAll :: Term -> [Term] -> MRM Term mrApplyAll f args = liftSC2 scApplyAllBeta f args +-- | Apply a 'Term' to a single argument and beta-reduce in Mr. Monad +mrApply :: Term -> Term -> MRM Term +mrApply f arg = mrApplyAll f [arg] + -- | Like 'scBvNat', but if given a bitvector literal it is converted to a -- natural number literal mrBvToNat :: Term -> Term -> MRM Term @@ -566,6 +654,18 @@ uniquifyNames (nm:nms) nms_other = let nm' = uniquifyName nm nms_other in nm' : uniquifyNames nms (nm' : nms_other) +-- | Build a lambda term with the lifting (in the sense of 'incVars') of an +-- MR Solver term +mrLambdaLift :: TermLike tm => [(LocalName,Term)] -> tm -> + ([Term] -> tm -> MRM Term) -> MRM Term +mrLambdaLift [] t f = f [] t +mrLambdaLift ctx t f = + do nms <- uniquifyNames (map fst ctx) <$> map fst <$> mrUVars + let ctx' = zipWith (\nm (_,tp) -> (nm,tp)) nms ctx + vars <- reverse <$> mapM (liftSC1 scLocalVar) [0 .. length ctx - 1] + t' <- liftTermLike 0 (length ctx) t + f vars t' >>= liftSC2 scLambdaList ctx' + -- | Run a MR Solver computation in a context extended with a universal -- variable, which is passed as a 'Term' to the sub-computation. Note that any -- assumptions made in the sub-computation will be lost when it completes. @@ -728,6 +828,11 @@ mrCallsFun f = memoFixTermFun $ \recurse t -> case t of (unwrapTermF -> tf) -> foldM (\b t' -> if b then return b else recurse t') False tf + +---------------------------------------------------------------------- +-- * Monadic Operations on Mr. Solver State +---------------------------------------------------------------------- + -- | Make a fresh 'MRVar' of a given type, which must be closed, i.e., have no -- free uvars mrFreshVar :: LocalName -> Term -> MRM MRVar @@ -1002,6 +1107,11 @@ mrFunAssumpRHSAsNormComp (OpaqueFunAssump f args) = FunBind f args <$> CompFunReturn <$> Type <$> mrFunOutType f args mrFunAssumpRHSAsNormComp (RewriteFunAssump rhs) = return rhs + +---------------------------------------------------------------------- +-- * Functions for Debug Output +---------------------------------------------------------------------- + -- | Print a 'String' if the debug level is at least the supplied 'Int' debugPrint :: Int -> String -> MRM () debugPrint i str = diff --git a/src/SAWScript/Prover/MRSolver/SMT.hs b/src/SAWScript/Prover/MRSolver/SMT.hs index 5368f569c6..c7a15f09d2 100644 --- a/src/SAWScript/Prover/MRSolver/SMT.hs +++ b/src/SAWScript/Prover/MRSolver/SMT.hs @@ -2,6 +2,7 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE TupleSections #-} {- | Module : SAWScript.Prover.MRSolver.SMT @@ -499,17 +500,6 @@ mrProveRelH' _ _ (asBoolType -> Just _) (asBoolType -> Just _) t1 t2 = mrProveRelH' _ _ (asIntegerType -> Just _) (asIntegerType -> Just _) t1 t2 = mrProveEqSimple (liftSC2 scIntEq) t1 t2 --- For pair types, prove both the left and right projections are related -mrProveRelH' _ het (asPairType -> Just (tpL1, tpR1)) - (asPairType -> Just (tpL2, tpR2)) t1 t2 = - do t1L <- liftSC1 scPairLeft t1 - t2L <- liftSC1 scPairLeft t2 - t1R <- liftSC1 scPairRight t1 - t2R <- liftSC1 scPairRight t2 - condL <- mrProveRelH het tpL1 tpL2 t1L t2L - condR <- mrProveRelH het tpR1 tpR2 t1R t2R - andTermInCtx condL condR - -- For BVVec types, prove all projections are related by quantifying over an -- index variable and proving the projections at that index are related mrProveRelH' _ het tp1@(asBVVecType -> Just (n1, len1, tpA1)) @@ -559,42 +549,60 @@ mrProveRelH' _ het tp1@(asNonBVVecVectorType -> Just (m1, tpA1)) t2' <- mrGenBVVecFromVec m2 tpA2 t2 "mrProveRelH (BVVec/BVVec)" n len mrProveRelH het tp1' tp2' t1' t2' --- If our relation is heterogeneous and we have a BVVec on one side and a --- non-BVVec vector on the other, wrap the non-BVVec vector term in --- genBVVecFromVec and recurse -mrProveRelH' _ True tp1@(asBVVecType -> Just (n, len, _)) - tp2@(asNonBVVecVectorType -> Just (m, tpA2)) t1 t2 = - do m' <- mrBvToNat n len - ms_are_eq <- mrConvertible m' m - if ms_are_eq then return () else - throwMRFailure (TypesNotEq (Type tp1) (Type tp2)) - len' <- liftSC2 scGlobalApply "Prelude.bvToNat" [n, len] - tp2' <- liftSC2 scVecType len' tpA2 - err_str_tm <- liftSC1 scString "FIXME: mrProveRelH error" - err_tm <- liftSC2 scGlobalApply "Prelude.error" [tpA2, err_str_tm] - t2' <- liftSC2 scGlobalApply "Prelude.genBVVecFromVec" - [m, tpA2, t2, err_tm, n, len] - -- mrDebugPPPrefixSep 2 "mrProveRelH on BVVec/Vec: " t1 "and" t2' - mrProveRelH True tp1 tp2' t1 t2' -mrProveRelH' _ True tp1@(asNonBVVecVectorType -> Just (m, tpA1)) - tp2@(asBVVecType -> Just (n, len, _)) t1 t2 = - do m' <- mrBvToNat n len - ms_are_eq <- mrConvertible m' m - if ms_are_eq then return () else - throwMRFailure (TypesNotEq (Type tp1) (Type tp2)) - len' <- liftSC2 scGlobalApply "Prelude.bvToNat" [n, len] - tp1' <- liftSC2 scVecType len' tpA1 - err_str_tm <- liftSC1 scString "FIXME: mrProveRelH error" - err_tm <- liftSC2 scGlobalApply "Prelude.error" [tpA1, err_str_tm] - t1' <- liftSC2 scGlobalApply "Prelude.genBVVecFromVec" - [m, tpA1, t1, err_tm, n, len] - -- mrDebugPPPrefixSep 2 "mrProveRelH on Vec/BVVec: " t1' "and" t2 - mrProveRelH True tp1' tp2 t1' t2 - --- As a fallback, for types we can't handle, just check convertibility -mrProveRelH' _ _ tp1 tp2 t1 t2 = - do success <- mrConvertible t1 t2 - if success then return () else - mrDebugPPPrefixSep 2 "mrProveRelH could not match types: " tp1 "and" tp2 >> - mrDebugPPPrefixSep 2 "and could not prove convertible: " t1 "and" t2 - TermInCtx [] <$> liftSC1 scBool success +mrProveRelH' _ het tp1 tp2 t1 t2 = (het,) <$> matchHet tp1 tp2 >>= \case + + -- If our relation is heterogeneous and we have a bitvector on one side and + -- a Num on the other, ensure that the Num term is TCNum of some Nat, wrap + -- the Nat with bvNat, and recurse + (True, Just (HetBVNum n)) + | Just (primName -> "Cryptol.TCNum", [t2']) <- asCtor t2 -> + do n_tm <- liftSC1 scNat n + t2'' <- liftSC2 scGlobalApply "Prelude.bvNat" [n_tm, t2'] + mrProveRelH True tp1 tp1 t1 t2'' + | otherwise -> throwMRFailure (TermsNotEq t1 t2) + (True, Just (HetNumBV n)) + | Just (primName -> "Cryptol.TCNum", [t1']) <- asCtor t1 -> + do n_tm <- liftSC1 scNat n + t1'' <- liftSC2 scGlobalApply "Prelude.bvNat" [n_tm, t1'] + mrProveRelH True tp1 tp1 t1'' t2 + | otherwise -> throwMRFailure (TermsNotEq t1 t2) + + -- If our relation is heterogeneous and we have a BVVec on one side and a + -- non-BVVec vector on the other, wrap the non-BVVec vector term in + -- genBVVecFromVec and recurse + (True, Just (HetBVVecVec (n, len, _) (m, tpA2))) -> + do len' <- liftSC2 scGlobalApply "Prelude.bvToNat" [n, len] + tp2' <- liftSC2 scVecType len' tpA2 + t2' <- mrGenBVVecFromVec m tpA2 t2 "mrProveRelH (BVVec/Vec)" n len + -- mrDebugPPPrefixSep 2 "mrProveRelH on BVVec/Vec: " t1 "an`d" t2' + mrProveRelH True tp1 tp2' t1 t2' + (True, Just (HetVecBVVec (m, tpA1) (n, len, _))) -> + do len' <- liftSC2 scGlobalApply "Prelude.bvToNat" [n, len] + tp1' <- liftSC2 scVecType len' tpA1 + t1' <- mrGenBVVecFromVec m tpA1 t1 "mrProveRelH (Vec/BVVec)" n len + -- mrDebugPPPrefixSep 2 "mrProveRelH on Vec/BVVec: " t1' "and" t2 + mrProveRelH True tp1' tp2 t1' t2 + + -- For pair types, prove both the left and right projections are related + (_, Just (HetPair (tpL1, tpR1) (tpL2, tpR2))) -> + do t1L <- liftSC1 scPairLeft t1 + t2L <- liftSC1 scPairLeft t2 + t1R <- liftSC1 scPairRight t1 + t2R <- liftSC1 scPairRight t2 + condL <- mrProveRelH het tpL1 tpL2 t1L t2L + condR <- mrProveRelH het tpR1 tpR2 t1R t2R + liftTermInCtx2 scAnd condL condR + + -- As a fallback, for types we can't handle, just check convertibility (we do + -- this in two cases to make sure we catch any missed 'HetRelated' patterns) + (True, Nothing) -> + do success <- mrConvertible t1 t2 + if success then return () else + mrDebugPPPrefixSep 2 "mrProveRel could not match types: " tp1 "and" tp2 >> + mrDebugPPPrefixSep 2 "and could not prove convertible: " t1 "and" t2 + TermInCtx [] <$> liftSC1 scBool success + (False, _)-> + do success <- mrConvertible t1 t2 + if success then return () else + mrDebugPPPrefixSep 2 "mrProveEq could not prove convertible: " t1 "and" t2 + TermInCtx [] <$> liftSC1 scBool success diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs index 7d29169253..0948a1425a 100644 --- a/src/SAWScript/Prover/MRSolver/Solver.hs +++ b/src/SAWScript/Prover/MRSolver/Solver.hs @@ -125,7 +125,8 @@ module SAWScript.Prover.MRSolver.Solver where import Data.Maybe import Data.Either -import Data.List (findIndices, intercalate) +import Data.List (find, findIndices) +import Data.Foldable (foldlM) import Data.Bits (shiftL) import Control.Monad.Except import qualified Data.Map as Map @@ -134,7 +135,6 @@ import qualified Data.Text as Text import Prettyprinter import Verifier.SAW.Term.Functor -import Verifier.SAW.Term.CtxTerm (substTerm) import Verifier.SAW.SharedTerm import Verifier.SAW.Recognizer import Verifier.SAW.Cryptol.Monadify @@ -531,7 +531,7 @@ mrRefinesCoInd f1 args1 f2 args2 = -- | Prove the refinement represented by a 'CoIndHyp' coinductively. This is the -- main loop implementing 'mrRefinesCoInd'. See that function for documentation. proveCoIndHyp :: CoIndHyp -> MRM () -proveCoIndHyp hyp = +proveCoIndHyp hyp = withFailureCtx (FailCtxCoIndHyp hyp) $ do let f1 = coIndHypLHSFun hyp f2 = coIndHypRHSFun hyp args1 = coIndHypLHS hyp @@ -577,32 +577,97 @@ generalizeCoIndHyp hyp all_specs@(arg_spec:arg_specs) = -- Get the arg and type associated with arg_spec let arg = coIndHypArg hyp arg_spec arg_tp <- mrTypeOf arg - -- Sort out the other args that equal arg + -- Sort out the other args that are heterogeneously related to arg eq_uneq_specs <- forM arg_specs $ \spec' -> do let arg' = coIndHypArg hyp spec' tp' <- mrTypeOf arg' - tps_eq <- mrConvertible arg_tp tp' - args_eq <- if tps_eq then mrProveEq arg arg' else return False - return $ if args_eq then Left spec' else Right spec' + tps_rel <- typesHetRelated arg_tp tp' + args_rel <- if tps_rel then mrProveRel True arg arg' else return False + return $ if args_rel then Left (spec', tp') else Right spec' let (eq_specs, uneq_specs) = partitionEithers eq_uneq_specs - -- Add a new variable of type arg_tp, set all eq_specs plus our original - -- arg_spec to it, and recurse - hyp' <- generalizeCoIndHypArgs hyp arg_tp (arg_spec:eq_specs) + -- Group the eq_specs by their type, i.e. turn a list @[(Idx, Type)]@ into a + -- list @[([Idx], Type)]@, where all the indices in each pair share the same + -- type (as in 'mrConvertible') + let addArgByTp :: [([a], Term)] -> (a, Term) -> MRM [([a], Term)] + addArgByTp [] (x, tp) = return [([x], tp)] + addArgByTp ((xs, tp):xstps) (x, tp') = + do tps_eq <- mrConvertible tp' tp + if tps_eq then return ((x:xs, tp):xstps) + else ((xs, tp):) <$> addArgByTp xstps (x, tp') + eq_specs_gpd <- foldlM addArgByTp [] ((arg_spec,arg_tp):eq_specs) + -- Add a new variable, set all the indices in @eq_specs_gpd@ to it as in + -- 'generalizeCoIndHypArgs', and recurse + hyp' <- generalizeCoIndHypArgs hyp eq_specs_gpd generalizeCoIndHyp hyp' uneq_specs --- | Add a new variable of the given type to the context of a coinductive --- hypothesis and set the specified arguments to that new variable -generalizeCoIndHypArgs :: CoIndHyp -> Term -> [Either Int Int] -> MRM CoIndHyp -generalizeCoIndHypArgs (CoIndHyp ctx f1 f2 args1 args2 invar1 invar2) tp specs = - do let set_arg i args = - take i args ++ (Unshared $ LocalVar 0) : drop (i+1) args - let (specs1, specs2) = partitionEithers specs - -- NOTE: need to lift the arguments because we are adding a variable - args1' <- liftTermLike 0 1 args1 - args2' <- liftTermLike 0 1 args2 - let args1'' = foldr set_arg args1' specs1 - args2'' = foldr set_arg args2' specs2 - return $ CoIndHyp (ctx ++ [("z",tp)]) f1 f2 args1'' args2'' invar1 invar2 +-- | Assuming all the types in the given list are related by 'typesHetRelated' +-- and no two of them are convertible, add a new variable and set all of +-- indices in the given list to it, modulo possibly some wrapper functions +-- determined by how the types are heterogeneously related +generalizeCoIndHypArgs :: CoIndHyp -> [([Either Int Int], Term)] -> MRM CoIndHyp + +-- If all the arguments we need to generalize have the same type, introduce a +-- new variable and set all of the given arguments to it +generalizeCoIndHypArgs hyp [(specs, tp)] = + do (hyp', var) <- coIndHypWithVar hyp "z" (Type tp) + return $ coIndHypSetArgs hyp' specs var + +generalizeCoIndHypArgs hyp [(specs1, tp1), (specs2, tp2)] = matchHet tp1 tp2 >>= \case + + -- If we need to generalize bitvector arguments with Num arguments, introduce + -- a bitvector variable and set all of the bitvector arguments to it and + -- all of the Num arguments to `TCNum` of `bvToNat` of it + Just (HetBVNum n) -> + do (hyp', var) <- coIndHypWithVar hyp "z" (Type tp1) + nat_tm <- liftSC2 scBvToNat n var + num_tm <- liftSC2 scCtorApp "Cryptol.TCNum" [nat_tm] + let hyp'' = coIndHypSetArgs hyp' specs1 var + return $ coIndHypSetArgs hyp'' specs2 num_tm + Just (HetNumBV n) -> + do (hyp', var) <- coIndHypWithVar hyp "z" (Type tp2) + nat_tm <- liftSC2 scBvToNat n var + num_tm <- liftSC2 scCtorApp "Cryptol.TCNum" [nat_tm] + let hyp'' = coIndHypSetArgs hyp' specs1 num_tm + return $ coIndHypSetArgs hyp'' specs2 var + + -- If we need to generalize BVVec arguments with Vec arguments, introduce a + -- BVVec variable and set all of the BVVec arguments to it and all of the + -- Vec arguments to `genBVVecFromVec` of it + -- FIXME: Could we handle the a /= a' case here and in mrRefinesFunH? + Just (HetBVVecVec (n, len, a) (m, a')) -> + do as_are_eq <- mrConvertible a a' + if as_are_eq then return () else + throwMRFailure (TypesNotRel True (Type tp1) (Type tp2)) + (hyp', var) <- coIndHypWithVar hyp "z" (Type tp1) + bvv_tm <- mrGenFromBVVec n len a var "generalizeCoIndHypArgs (BVVec/Vec)" m + let hyp'' = coIndHypSetArgs hyp' specs1 var + return $ coIndHypSetArgs hyp'' specs2 bvv_tm + Just (HetVecBVVec (m, a') (n, len, a)) -> + do as_are_eq <- mrConvertible a a' + if as_are_eq then return () else + throwMRFailure (TypesNotRel True (Type tp1) (Type tp2)) + (hyp', var) <- coIndHypWithVar hyp "z" (Type tp2) + bvv_tm <- mrGenFromBVVec n len a var "generalizeCoIndHypArgs (Vec/BVVec)" m + let hyp'' = coIndHypSetArgs hyp' specs1 bvv_tm + return $ coIndHypSetArgs hyp'' specs2 var + + -- This case should be unreachable because in 'mrRefinesFunH' we always + -- expand all tuples - though in principle we could handle it + Just (HetPair _ _) -> + debugPrint 0 "generalizeCoIndHypArgs: trying to widen distinct tuple types:" >> + throwMRFailure (TypesNotRel True (Type tp1) (Type tp2)) + + Nothing -> throwMRFailure (TypesNotRel True (Type tp1) (Type tp2)) + +generalizeCoIndHypArgs _ specs = map fst <$> mrUVars >>= \uvar_ctx -> + -- Being in this case implies we have types @tp1, tp2, tp3@ which are related + -- by 'typesHetRelated' but no two of them are convertible. As of the time of + -- writing, the only way this could be possible is if the types are pair + -- types related in different components (e.g. @(a,b), (a',b), (a,b')@). In + -- 'mrRefinesFunH' we always expand all tuples, so when we hit this function + -- no such types should remain. + error $ "generalizeCoIndHypArgs: too many distinct types to widen: " + ++ showInCtx uvar_ctx specs ---------------------------------------------------------------------- @@ -788,12 +853,13 @@ mrRefines' (FunBind (EVarFunName evar) args (CompFunReturn _)) m2 = mrRefines' (FunBind (LetRecName f) args1 k1) (FunBind (LetRecName f') args2 k2) | f == f' && length args1 == length args2 = zipWithM_ mrAssertProveEq args1 args2 >> - mrRefinesFun k1 k2 + mrFunOutType (LetRecName f) args1 >>= \tp -> + mrRefinesFun tp k1 tp k2 mrRefines' m1@(FunBind f1 args1 k1) m2@(FunBind f2 args2 k2) = mrFunOutType f1 args1 >>= \tp1 -> mrFunOutType f2 args2 >>= \tp2 -> - mrConvertible tp1 tp2 >>= \tps_eq -> + typesHetRelated tp1 tp2 >>= \tps_rel -> mrFunBodyRecInfo f1 args1 >>= \maybe_f1_body -> mrFunBodyRecInfo f2 args2 >>= \maybe_f2_body -> mrGetCoIndHyp f1 f2 >>= \maybe_coIndHyp -> @@ -808,7 +874,7 @@ mrRefines' m1@(FunBind f1 args1 k1) m2@(FunBind f2 args2 k2) = -- * Otherwise, throw a 'CoIndHypMismatchFailure' error. (Just hyp, _) -> matchCoIndHyp hyp args1 args2 >> - mrRefinesFun k1 k2 + mrRefinesFun tp1 k1 tp2 k2 -- If we have an opaque FunAssump that f1 args1' refines f2 args2', then -- prove that args1 = args1', args2 = args2', and then that k1 refines k2 @@ -817,7 +883,7 @@ mrRefines' m1@(FunBind f1 args1 k1) m2@(FunBind f2 args2 k2) = (args1'', args2'') <- substTermLike 0 evars (args1', args2') zipWithM_ mrAssertProveEq args1'' args1 zipWithM_ mrAssertProveEq args2'' args2 - mrRefinesFun k1 k2 + mrRefinesFun tp1 k1 tp2 k2 -- If we have an opaque FunAssump that f1 refines some f /= f2, and f2 -- unfolds and is not recursive in itself, unfold f2 and recurse @@ -847,13 +913,13 @@ mrRefines' m1@(FunBind f1 args1 k1) m2@(FunBind f2 args2 k2) = -- If we don't have a co-inducitve hypothesis for f1 and f2, don't have an -- assumption that f1 refines some specification, and both f1 and f2 are - -- recursive and have the same return type, then try to coinductively prove - -- that f1 args1 |= f2 args2 under the assumption that f1 args1 |= f2 args2, - -- and then try to prove that k1 |= k2 - _ | tps_eq + -- recursive and have return types which are heterogeneously related, then + -- try to coinductively prove that f1 args1 |= f2 args2 under the assumption + -- that f1 args1 |= f2 args2, and then try to prove that k1 |= k2 + _ | tps_rel , Just _ <- maybe_f1_body , Just _ <- maybe_f2_body -> - mrRefinesCoInd f1 args1 f2 args2 >> mrRefinesFun k1 k2 + mrRefinesCoInd f1 args1 f2 args2 >> mrRefinesFun tp1 k1 tp2 k2 -- If we cannot line up f1 and f2, then making progress here would require us -- to somehow split either m1 or m2 into some bind m' >>= k' such that m' is @@ -941,18 +1007,123 @@ mrRefines'' (ForallM tp f1) m2 = -- If none of the above cases match, then fail mrRefines'' m1 m2 = throwMRFailure (CompsDoNotRefine m1 m2) - -- | Prove that one function refines another for all inputs -mrRefinesFun :: CompFun -> CompFun -> MRM () -mrRefinesFun (CompFunReturn _) (CompFunReturn _) = return () -mrRefinesFun f1 f2 - | Just nm <- compFunVarName f1 `mplus` compFunVarName f2 - , Just tp <- compFunInputType f1 `mplus` compFunInputType f2 = - withUVarLift nm tp (f1,f2) $ \x (f1', f2') -> - do m1' <- applyNormCompFun f1' x - m2' <- applyNormCompFun f2' x - mrRefines m1' m2' -mrRefinesFun _ _ = error "mrRefinesFun: unreachable!" +mrRefinesFun :: Term -> CompFun -> Term -> CompFun -> MRM () +mrRefinesFun tp1 f1 tp2 f2 = + do mrDebugPPPrefixSep 1 "mrRefinesFun on types:" tp1 "," tp2 + mrDebugPPPrefixSep 1 "mrRefinesFun" f1 "|=" f2 + f1' <- compFunToTerm f1 + f2' <- compFunToTerm f2 + let lnm = maybe "call_ret_val" id (compFunVarName f1) + rnm = maybe "call_ret_val" id (compFunVarName f2) + mrRefinesFunH mrRefines [] [(lnm, tp1)] f1' [(rnm, tp2)] f2' + +-- | The main loop of 'mrRefinesFun' and 'askMRSolver': given a continuation, +-- two terms of function type, and two equal-length lists representing the +-- argument types of the two terms, add a uvar for each corresponding pair of +-- types (assuming the types are either equal or are heterogeneously related, +-- as in 'HetRelated'), apply the terms to these uvars (modulo possibly some +-- wrapper functions determined by how the types are heterogeneously related), +-- and call the continuation on the resulting terms. The second argument is +-- an accumulator of variables to introduce, innermost first. +mrRefinesFunH :: (Term -> Term -> MRM a) -> [Term] -> + [(LocalName,Term)] -> Term -> [(LocalName,Term)] -> Term -> + MRM a + +mrRefinesFunH k vars ((nm1, tp1):tps1) t1 ((nm2, tp2):tps2) t2 = matchHet tp1 tp2 >>= \case + + -- If we need to introduce a bitvector on one side and a Num on the other, + -- introduce a bitvector variable and substitute `TCNum` of `bvToNat` of that + -- variable on the Num side + Just (HetBVNum n) -> + let nm = maybe "_" id $ find ((/=) '_' . Text.head) + $ [nm1, nm2] ++ catMaybes [ asLambdaName t1 + , asLambdaName t2 ] in + withUVarLift nm (Type tp1) (vars, t1, t2) $ \var (vars', t1', t2') -> + do nat_tm <- liftSC2 scBvToNat n var + num_tm <- liftSC2 scCtorApp "Cryptol.TCNum" [nat_tm] + tps2' <- substTermLike 0 (num_tm : vars') tps2 + t1'' <- mrApplyAll t1' [var] + t2'' <- mrApplyAll t2' [num_tm] + mrRefinesFunH k (var : vars') tps1 t1'' tps2' t2'' + Just (HetNumBV n) -> + let nm = maybe "_" id $ find ((/=) '_' . Text.head) + $ [nm1, nm2] ++ catMaybes [ asLambdaName t1 + , asLambdaName t2 ] in + withUVarLift nm (Type tp2) (vars, t1, t2) $ \var (vars', t1', t2') -> + do nat_tm <- liftSC2 scBvToNat n var + num_tm <- liftSC2 scCtorApp "Cryptol.TCNum" [nat_tm] + tps1' <- substTermLike 0 (num_tm : vars') tps1 + t1'' <- mrApplyAll t1' [num_tm] + t2'' <- mrApplyAll t2' [var] + mrRefinesFunH k (var : vars') tps1' t1'' tps2 t2'' + + -- If we need to introduce a BVVec on one side and a non-BVVec vector on the + -- other, introduce a BVVec variable and substitute `genBVVecFromVec` of that + -- variable on the non-BVVec side + -- FIXME: Could we handle the a /= a' case here and in generalizeCoIndHypArgs? + Just (HetBVVecVec (n, len, a) (m, a')) -> + do as_are_eq <- mrConvertible a a' + if as_are_eq then return () else + throwMRFailure (TypesNotRel True (Type tp1) (Type tp2)) + let nm = maybe "_" id $ find ((/=) '_' . Text.head) + $ [nm1, nm2] ++ catMaybes [ asLambdaName t1 + , asLambdaName t2 ] + withUVarLift nm (Type tp1) (vars, t1, t2) $ \var (vars', t1', t2') -> + do bvv_tm <- mrGenFromBVVec n len a var "mrRefinesFunH (BVVec/Vec)" m + tps2' <- substTermLike 0 (bvv_tm : vars') tps2 + t1'' <- mrApplyAll t1' [var] + t2'' <- mrApplyAll t2' [bvv_tm] + mrRefinesFunH k (var : vars') tps1 t1'' tps2' t2'' + Just (HetVecBVVec (m, a') (n, len, a)) -> + do as_are_eq <- mrConvertible a a' + if as_are_eq then return () else + throwMRFailure (TypesNotRel True (Type tp1) (Type tp2)) + let nm = maybe "_" id $ find ((/=) '_' . Text.head) + $ [nm1, nm2] ++ catMaybes [ asLambdaName t1 + , asLambdaName t2 ] + withUVarLift nm (Type tp2) (vars, t1, t2) $ \var (vars', t1', t2') -> + do bvv_tm <- mrGenFromBVVec n len a var "mrRefinesFunH (BVVec/Vec)" m + tps1' <- substTermLike 0 (bvv_tm : vars') tps1 + t1'' <- mrApplyAll t1' [var] + t2'' <- mrApplyAll t2' [bvv_tm] + mrRefinesFunH k (var : vars') tps1' t1'' tps2 t2'' + + -- We always curry pair values before introducing them (NOTE: we do this even + -- when the have the same types to ensure we never have to unify a projection + -- of an evar with a non-projected value, i.e. evar.1 == val ) + Just (HetPair (tpL1, tpR1) (tpL2, tpR2)) -> + do let tps1' = (nm1 <> "_1", tpL1):(nm1 <> "_2", tpR1):tps1 + tps2' = (nm2 <> "_1", tpL2):(nm2 <> "_2", tpR2):tps2 + t1'' <- mrLambdaLift [(nm1, tpL1), (nm1, tpR1)] t1 $ \[prj1, prj2] t1' -> + liftSC2 scPairValue prj1 prj2 >>= mrApply t1' + t2'' <- mrLambdaLift [(nm2, tpL2), (nm2, tpR2)] t2 $ \[prj1, prj2] t2' -> + liftSC2 scPairValue prj1 prj2 >>= mrApply t2' + mrRefinesFunH k vars tps1' t1'' tps2' t2'' + + -- Introduce variables of the same type together + Nothing -> + do tps_are_eq <- mrConvertible tp1 tp2 + if tps_are_eq then return () else + throwMRFailure (TypesNotRel True (Type tp1) (Type tp2)) + let nm = maybe "_" id $ find ((/=) '_' . Text.head) + $ [nm1, nm2] ++ catMaybes [ asLambdaName t1 + , asLambdaName t2 ] + withUVarLift nm (Type tp1) (vars, t1, t2) $ \var (vars', t1', t2') -> + do t1'' <- mrApplyAll t1' [var] + t2'' <- mrApplyAll t2' [var] + mrRefinesFunH k (var : vars') tps1 t1'' tps2 t2'' + +-- Error if we don't have the same number of arguments on both sides +-- FIXME: Add a specific error for this case +mrRefinesFunH _ _ ((_,tp1):_) _ [] _ = + liftSC0 scUnitType >>= \utp -> + throwMRFailure (TypesNotEq (Type tp1) (Type utp)) +mrRefinesFunH _ _ [] _ ((_,tp2):_) _ = + liftSC0 scUnitType >>= \utp -> + throwMRFailure (TypesNotEq (Type utp) (Type tp2)) + +mrRefinesFunH k _ [] t1 [] t2 = k t1 t2 ---------------------------------------------------------------------- @@ -964,93 +1135,12 @@ mrRefinesFun _ _ = error "mrRefinesFun: unreachable!" -- a function name type MRSolverResult = Maybe (FunName, FunAssump) --- | The main loop of 'askMRSolver'. The first argument is an accumulator of --- variables to introduce, innermost first. -askMRSolverH :: [Term] -> Term -> Term -> Term -> Term -> MRM MRSolverResult - --- If we need to introduce a bitvector on one side and a Num on the other, --- introduce a bitvector variable and substitute `TCNum` of `bvToNat` of that --- variable on the Num side -askMRSolverH vars (asPi -> Just (nm1, tp@(asBitvectorType -> Just n), body1)) t1 - (asPi -> Just (nm2, asDataType -> Just (primName -> "Cryptol.Num", _), body2)) t2 = - let nm = if Text.head nm2 == '_' then nm1 else nm2 in - withUVarLift nm (Type tp) (vars, t1, t2) $ \var (vars', t1', t2') -> - do nat_tm <- liftSC2 scBvToNat n var - num_tm <- liftSC2 scCtorApp "Cryptol.TCNum" [nat_tm] - body2' <- substTerm 0 (num_tm : vars') body2 - t1'' <- mrApplyAll t1' [var] - t2'' <- mrApplyAll t2' [num_tm] - askMRSolverH (var : vars') body1 t1'' body2' t2'' -askMRSolverH vars (asPi -> Just (nm1, asDataType -> Just (primName -> "Cryptol.Num", _), body1)) t1 - (asPi -> Just (nm2, tp@(asBitvectorType -> Just n), body2)) t2 = - let nm = if Text.head nm2 == '_' then nm1 else nm2 in - withUVarLift nm (Type tp) (vars, t1, t2) $ \var (vars', t1', t2') -> - do nat_tm <- liftSC2 scBvToNat n var - num_tm <- liftSC2 scCtorApp "Cryptol.TCNum" [nat_tm] - body1' <- substTerm 0 (num_tm : vars') body1 - t1'' <- mrApplyAll t1' [num_tm] - t2'' <- mrApplyAll t2' [var] - askMRSolverH (var : vars') body1' t1'' body2 t2'' - --- If we need to introduce a BVVec on one side and a non-BVVec vector on the --- other, introduce a BVVec variable and substitute `genBVVecFromVec` of that --- variable on the non-BVVec side -askMRSolverH vars tp1@(asPi -> Just (nm1, tp@(asBVVecType -> Just (n, len, a)), body1)) t1 - tp2@(asPi -> Just (nm2, asNonBVVecVectorType -> Just (m, a'), body2)) t2 = - do m' <- mrBvToNat n len - ms_are_eq <- mrConvertible m' m - as_are_eq <- mrConvertible a a' - if ms_are_eq && as_are_eq then return () else - throwMRFailure (TypesNotEq (Type tp1) (Type tp2)) - let nm = if Text.head nm2 == '_' then nm1 else nm2 - withUVarLift nm (Type tp) (vars, t1, t2) $ \var (vars', t1', t2') -> - do err_str_tm <- liftSC1 scString "FIXME: askMRSolverH error" - err_tm <- liftSC2 scGlobalApply "Prelude.error" [a, err_str_tm] - bvvec_tm <- liftSC2 scGlobalApply "Prelude.genFromBVVec" - [n, len, a, var, err_tm, m] - body2' <- substTerm 0 (bvvec_tm : vars') body2 - t1'' <- mrApplyAll t1' [var] - t2'' <- mrApplyAll t2' [bvvec_tm] - askMRSolverH (var : vars') body1 t1'' body2' t2'' -askMRSolverH vars tp1@(asPi -> Just (nm1, asNonBVVecVectorType -> Just (m, a'), body2)) t1 - tp2@(asPi -> Just (nm2, tp@(asBVVecType -> Just (n, len, a)), body1)) t2 = - do m' <- mrBvToNat n len - ms_are_eq <- mrConvertible m' m - as_are_eq <- mrConvertible a a' - if ms_are_eq && as_are_eq then return () else - throwMRFailure (TypesNotEq (Type tp1) (Type tp2)) - let nm = if Text.head nm2 == '_' then nm1 else nm2 - withUVarLift nm (Type tp) (vars, t1, t2) $ \var (vars', t1', t2') -> - do err_str_tm <- liftSC1 scString "FIXME: askMRSolverH error" - err_tm <- liftSC2 scGlobalApply "Prelude.error" [a, err_str_tm] - bvvec_tm <- liftSC2 scGlobalApply "Prelude.genFromBVVec" - [n, len, a, var, err_tm, m] - body1' <- substTerm 0 (bvvec_tm : vars') body1 - t1'' <- mrApplyAll t1' [var] - t2'' <- mrApplyAll t2' [bvvec_tm] - askMRSolverH (var : vars') body1' t1'' body2 t2'' - --- Introduce variables of the same type together -askMRSolverH vars tp11@(asPi -> Just (nm1, tp1, body1)) t1 - tp22@(asPi -> Just (nm2, tp2, body2)) t2 = - do tps_are_eq <- mrConvertible tp1 tp2 - if tps_are_eq then return () else - throwMRFailure (TypesNotEq (Type tp11) (Type tp22)) - let nm = if Text.head nm2 == '_' then nm1 else nm2 - withUVarLift nm (Type tp1) (vars, t1, t2) $ \var (vars', t1', t2') -> - do t1'' <- mrApplyAll t1' [var] - t2'' <- mrApplyAll t2' [var] - askMRSolverH (var : vars') body1 t1'' body2 t2'' - --- Error if we don't have the same number of arguments on both sides -askMRSolverH _ tp1@(asPi -> Just _) _ tp2 _ = - throwMRFailure (TypesNotEq (Type tp1) (Type tp2)) -askMRSolverH _ tp1 _ tp2@(asPi -> Just _) _ = - throwMRFailure (TypesNotEq (Type tp1) (Type tp2)) - --- The base case: both sides are CompM of the same type -askMRSolverH _ (asCompM -> Just _) t1 (asCompM -> Just _) t2 = - do m1 <- normCompTerm t1 +-- | The continuation passed to 'mrRefinesFunH' in 'askMRSolver': normalizes +-- both resulting terms using 'normCompTerm', calls mrRefines on the terms, +-- then returns a 'FunAssump', if possible +askMRSolverH :: Term -> Term -> MRM MRSolverResult +askMRSolverH t1 t2 = + do m1 <- normCompTerm t1 m2 <- normCompTerm t2 mrRefines m1 m2 case (m1, m2) of @@ -1070,25 +1160,23 @@ askMRSolverH _ (asCompM -> Just _) t1 (asCompM -> Just _) t2 = fassumpRHS = RewriteFunAssump m2 }) _ -> return Nothing --- Error if we don't have CompM at the end -askMRSolverH _ (asCompM -> Just _) _ tp2 _ = - throwMRFailure (NotCompFunType tp2) -askMRSolverH _ tp1 _ _ _ = - throwMRFailure (NotCompFunType tp1) - - -- | Test two monadic, recursive terms for refinement. On success, if the --- left-hand term is a named function, add the refinement to the 'MREnv' --- environment. +-- left-hand term is a named function, returning a 'FunAssump' to add to the +-- 'MREnv'. askMRSolver :: SharedContext -> MREnv {- ^ The Mr Solver environment -} -> Maybe Integer {- ^ Timeout in milliseconds for each SMT call -} -> Term -> Term -> IO (Either MRFailure MRSolverResult) - askMRSolver sc env timeout t1 t2 = do tp1 <- scTypeOf sc t1 >>= scWhnf sc tp2 <- scTypeOf sc t2 >>= scWhnf sc runMRM sc timeout env $ mrDebugPPPrefixSep 1 "mr_solver" t1 "|=" t2 >> - askMRSolverH [] tp1 t1 tp2 t2 + case (asPiList tp1, asPiList tp2) of + ((tps1, asCompM -> Just _), (tps2, asCompM -> Just _)) -> + mrRefinesFunH askMRSolverH [] tps1 t1 tps2 t2 + ((_, asCompM -> Just _), (_, tp2')) -> + throwMRFailure (NotCompFunType tp2') + ((_, tp1'), _) -> + throwMRFailure (NotCompFunType tp1') From d24be72763003db1fbf9a27d7a325162c360446b Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Wed, 1 Jun 2022 13:10:29 -0700 Subject: [PATCH 08/17] add mr_solver_assume --- src/SAWScript/Builtins.hs | 48 +++++++++++++++++++------ src/SAWScript/Interpreter.hs | 6 ++++ src/SAWScript/Prover/MRSolver.hs | 2 +- src/SAWScript/Prover/MRSolver/Monad.hs | 3 +- src/SAWScript/Prover/MRSolver/Solver.hs | 34 ++++++++++++++---- 5 files changed, 74 insertions(+), 19 deletions(-) diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index d6404c0f35..52907927b4 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -1656,13 +1656,14 @@ ensureMonadicTerm sc t False -> monadifyTypedTerm sc t ensureMonadicTerm sc t = monadifyTypedTerm sc t --- | A wrapper for 'Prover.askMRSolver' from @MRSolver.hs@ which if the first --- argument is @Just str@, prints out @str@ followed by an abridged version --- of the refinement being asked -askMRSolver :: Maybe SawDoc -> SharedContext -> TypedTerm -> TypedTerm -> - TopLevel (NominalDiffTime, - Either Prover.MRFailure Prover.MRSolverResult) -askMRSolver printStr sc t1 t2 = +-- | A wrapper for either 'Prover.askMRSolver' or 'Prover.assumeMRSolver' from +-- @MRSolver.hs@: if the first argument is @Just str@, prints out @str@ +-- followed by an abridged version of the refinement being asked, then calls +-- the given function, returning how long it took to execute +mrSolver :: (SharedContext -> Prover.MREnv -> Maybe Integer -> Term -> Term -> IO a) -> + Maybe SawDoc -> SharedContext -> TypedTerm -> TypedTerm -> + TopLevel (NominalDiffTime, a) +mrSolver f printStr sc t1 t2 = do env <- rwMRSolverEnv <$> get m1 <- collapseEta <$> ttTerm <$> ensureMonadicTerm sc t1 m2 <- collapseEta <$> ttTerm <$> ensureMonadicTerm sc t2 @@ -1672,7 +1673,7 @@ askMRSolver printStr sc t1 t2 = "[MRSolver] " <> str <> ": " <> ppTmHead m1 <> " |= " <> ppTmHead m2 time1 <- liftIO getCurrentTime - res <- io $ Prover.askMRSolver sc env Nothing m1 m2 + res <- io $ f sc env Nothing m1 m2 time2 <- liftIO getCurrentTime return (diffUTCTime time2 time1, res) where -- Turn a term of the form @\x1 ... xn -> f x1 ... xn@ into @f@ @@ -1701,7 +1702,7 @@ mrSolverProve :: Bool -> SharedContext -> TypedTerm -> TypedTerm -> TopLevel () mrSolverProve addToEnv sc t1 t2 = do dlvl <- Prover.mreDebugLevel <$> rwMRSolverEnv <$> get let printStr = if addToEnv then "Proving" else "Testing" - (diff, res) <- askMRSolver (Just printStr) sc t1 t2 + (diff, res) <- mrSolver Prover.askMRSolver (Just printStr) sc t1 t2 case res of Left err | dlvl == 0 -> io (putStrLn $ Prover.showMRFailure err) >> @@ -1730,7 +1731,7 @@ mrSolverProve addToEnv sc t1 t2 = mrSolverQuery :: SharedContext -> TypedTerm -> TypedTerm -> TopLevel Bool mrSolverQuery sc t1 t2 = do dlvl <- Prover.mreDebugLevel <$> rwMRSolverEnv <$> get - (diff, res) <- askMRSolver (Just "Querying") sc t1 t2 + (diff, res) <- mrSolver Prover.askMRSolver (Just "Querying") sc t1 t2 case res of Left _ | dlvl == 0 -> printOutLnTop Info (printf "[MRSolver] Failure in %s" (show diff)) >> @@ -1745,6 +1746,33 @@ mrSolverQuery sc t1 t2 = printOutLnTop Info (printf "[MRSolver] Success in %s" (show diff)) >> return True +-- | Generate the 'Prover.FunAssump' which corresponds to the given refinement +-- and add it to the 'Prover.MREnv' +mrSolverAssume :: SharedContext -> TypedTerm -> TypedTerm -> TopLevel () +mrSolverAssume sc t1 t2 = + do dlvl <- Prover.mreDebugLevel <$> rwMRSolverEnv <$> get + (_, res) <- mrSolver Prover.assumeMRSolver (Just "Assuming") sc t1 t2 + case res of + Left err | dlvl == 0 -> + io (putStrLn $ Prover.showMRFailure err) >> + printOutLnTop Info (printf "[MRSolver] Failure") >> + io (Exit.exitWith $ Exit.ExitFailure 1) + Left err -> + -- we ignore the MRFailure context here since it will have already + -- been printed by the debug trace + io (putStrLn $ Prover.showMRFailureNoCtx err) >> + printOutLnTop Info (printf "[MRSolver] Failure") >> + io (Exit.exitWith $ Exit.ExitFailure 1) + Right (Just (fnm, fassump)) -> + printOutLnTop Info ( + printf "[MRSolver] Success, added as an opaque assumption") >> + modify (\rw -> rw { rwMRSolverEnv = + Prover.mrEnvAddFunAssump fnm fassump (rwMRSolverEnv rw) }) + _ -> + printOutLnTop Info $ printf $ + "[MRSolver] Failure, given refinement cannot be interpreted as" ++ + " an assumption" + -- | Set the debug level of the 'Prover.MREnv' mrSolverSetDebug :: Int -> TopLevel () mrSolverSetDebug dlvl = diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index e5743e2b00..54fa0b36be 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -3287,6 +3287,12 @@ primitives = Map.fromList , " be considered in future calls to Mr. Solver, and unlike both," , " this command will never fail." ] + , prim "mr_solver_assume" "Term -> Term -> TopLevel Bool" + (scVal mrSolverAssume) + Experimental + [ "Add the refinement of the two given expressions as an assumption" + , " which will be used in future calls to Mr. Solver." ] + , prim "mr_solver_set_debug_level" "Int -> TopLevel ()" (pureVal mrSolverSetDebug) Experimental diff --git a/src/SAWScript/Prover/MRSolver.hs b/src/SAWScript/Prover/MRSolver.hs index b422cfd996..32760eb2db 100644 --- a/src/SAWScript/Prover/MRSolver.hs +++ b/src/SAWScript/Prover/MRSolver.hs @@ -9,7 +9,7 @@ Portability : non-portable (language extensions) -} module SAWScript.Prover.MRSolver - (askMRSolver, MRSolverResult, + (askMRSolver, assumeMRSolver, MRSolverResult, MRFailure(..), showMRFailure, showMRFailureNoCtx, FunAssump(..), FunAssumpRHS(..), MREnv(..), emptyMREnv, mrEnvAddFunAssump, mrEnvSetDebugLevel, diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs index 2bd3888fb7..0aedffccdc 100644 --- a/src/SAWScript/Prover/MRSolver/Monad.hs +++ b/src/SAWScript/Prover/MRSolver/Monad.hs @@ -96,7 +96,8 @@ pattern TypesNotEq t1 t2 = TypesNotRel False t1 t2 -- | Remove the context from a 'MRFailure', i.e. remove all applications of the -- 'MRFailureLocalVar' and 'MRFailureCtx' constructors mrFailureWithoutCtx :: MRFailure -> MRFailure -mrFailureWithoutCtx (MRFailureLocalVar _ err) = mrFailureWithoutCtx err +mrFailureWithoutCtx (MRFailureLocalVar x err) = + MRFailureLocalVar x (mrFailureWithoutCtx err) mrFailureWithoutCtx (MRFailureCtx _ err) = mrFailureWithoutCtx err mrFailureWithoutCtx (MRFailureDisj err1 err2) = MRFailureDisj (mrFailureWithoutCtx err1) (mrFailureWithoutCtx err2) diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs index 0948a1425a..132073ac18 100644 --- a/src/SAWScript/Prover/MRSolver/Solver.hs +++ b/src/SAWScript/Prover/MRSolver/Solver.hs @@ -1135,14 +1135,15 @@ mrRefinesFunH k _ [] t1 [] t2 = k t1 t2 -- a function name type MRSolverResult = Maybe (FunName, FunAssump) --- | The continuation passed to 'mrRefinesFunH' in 'askMRSolver': normalizes --- both resulting terms using 'normCompTerm', calls mrRefines on the terms, --- then returns a 'FunAssump', if possible -askMRSolverH :: Term -> Term -> MRM MRSolverResult -askMRSolverH t1 t2 = +-- | The continuation passed to 'mrRefinesFunH' in 'askMRSolver' and +-- 'assumeMRSolver': normalizes both resulting terms using 'normCompTerm', +-- calls the given monadic function, then returns a 'FunAssump', if possible +askMRSolverH :: (NormComp -> NormComp -> MRM ()) -> + Term -> Term -> MRM MRSolverResult +askMRSolverH f t1 t2 = do m1 <- normCompTerm t1 m2 <- normCompTerm t2 - mrRefines m1 m2 + f m1 m2 case (m1, m2) of -- If t1 and t2 are both named functions, our result is the opaque -- FunAssump that forall xs. f1 xs |= f2 xs' @@ -1175,7 +1176,26 @@ askMRSolver sc env timeout t1 t2 = mrDebugPPPrefixSep 1 "mr_solver" t1 "|=" t2 >> case (asPiList tp1, asPiList tp2) of ((tps1, asCompM -> Just _), (tps2, asCompM -> Just _)) -> - mrRefinesFunH askMRSolverH [] tps1 t1 tps2 t2 + mrRefinesFunH (askMRSolverH mrRefines) [] tps1 t1 tps2 t2 + ((_, asCompM -> Just _), (_, tp2')) -> + throwMRFailure (NotCompFunType tp2') + ((_, tp1'), _) -> + throwMRFailure (NotCompFunType tp1') + +-- | Return the 'FunAssump' to add to the 'MREnv' that would be generated if +-- 'askMRSolver' succeeded on the given terms. +assumeMRSolver :: + SharedContext -> + MREnv {- ^ The Mr Solver environment -} -> + Maybe Integer {- ^ Timeout in milliseconds for each SMT call -} -> + Term -> Term -> IO (Either MRFailure MRSolverResult) +assumeMRSolver sc env timeout t1 t2 = + do tp1 <- scTypeOf sc t1 >>= scWhnf sc + tp2 <- scTypeOf sc t2 >>= scWhnf sc + runMRM sc timeout env $ + case (asPiList tp1, asPiList tp2) of + ((tps1, asCompM -> Just _), (tps2, asCompM -> Just _)) -> + mrRefinesFunH (askMRSolverH (\_ _ -> return ())) [] tps1 t1 tps2 t2 ((_, asCompM -> Just _), (_, tp2')) -> throwMRFailure (NotCompFunType tp2') ((_, tp1'), _) -> From e98a6bed683dc44a27224e4be0d808a17d3a2a92 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Wed, 1 Jun 2022 15:42:32 -0700 Subject: [PATCH 09/17] changed monadification to never use openOpenTerm, to fix some free variable bugs --- .../src/Verifier/SAW/Cryptol/Monadify.hs | 54 ++++++++++++------- 1 file changed, 35 insertions(+), 19 deletions(-) diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs index 76de3b0318..ab1e5c46d5 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs @@ -90,6 +90,7 @@ import Verifier.SAW.Recognizer -- import Verifier.SAW.Position import Verifier.SAW.Cryptol.PreludeM +import GHC.Stack import Debug.Trace @@ -345,6 +346,12 @@ typeclassMonMap = ("Cryptol.PIntegral", "Cryptol.PIntegral"), ("Cryptol.PLiteral", "Cryptol.PLiteral")] +-- | The list of functions that are monadified as themselves in types +typeLevelOpMonList :: [Ident] +typeLevelOpMonList = ["Cryptol.tcAdd", "Cryptol.tcSub", "Cryptol.tcMul", + "Cryptol.tcDiv", "Cryptol.tcMod", "Cryptol.tcExp", + "Cryptol.tcMin", "Cryptol.tcMax"] + -- | A context of local variables used for monadifying types, which includes the -- variable names, their original types (before monadification), and, if their -- types corespond to 'MonKind's, a local 'MonType' that quantifies over them. @@ -364,25 +371,20 @@ ppTermInTypeCtx ctx t = typeCtxPureCtx :: MonadifyTypeCtx -> [(LocalName,Term)] typeCtxPureCtx = map (\(x,tp,_) -> (x,tp)) --- | Make a monadification type that is to be considered a base type -mkTermBaseType :: MonadifyTypeCtx -> MonKind -> Term -> MonType -mkTermBaseType ctx k t = - MTyBase k $ openOpenTerm (typeCtxPureCtx ctx) t - -- | Monadify a type and convert it to its corresponding argument type -monadifyTypeArgType :: MonadifyTypeCtx -> Term -> OpenTerm +monadifyTypeArgType :: HasCallStack => MonadifyTypeCtx -> Term -> OpenTerm monadifyTypeArgType ctx t = toArgType $ monadifyType ctx t -- | Apply a monadified type to a type or term argument in the sense of -- 'applyPiOpenTerm', meaning give the type of applying @f@ of a type to a -- particular argument @arg@ -applyMonType :: MonType -> Either MonType ArgMonTerm -> MonType +applyMonType :: HasCallStack => MonType -> Either MonType ArgMonTerm -> MonType applyMonType (MTyArrow _ tp_ret) (Right _) = tp_ret applyMonType (MTyForall _ _ f) (Left mtp) = f mtp applyMonType _ _ = error "applyMonType: application at incorrect type" -- | Convert a SAW core 'Term' to a monadification type -monadifyType :: MonadifyTypeCtx -> Term -> MonType +monadifyType :: HasCallStack => MonadifyTypeCtx -> Term -> MonType {- monadifyType ctx t | trace ("\nmonadifyType:\n" ++ ppTermInTypeCtx ctx t) False = undefined @@ -417,15 +419,12 @@ monadifyType ctx (asDataType -> Just (pn, args)) -- and/or Nums MTyBase k_out $ dataTypeOpenTerm (primName pn) (map toArgType margs) monadifyType ctx (asVectorType -> Just (len, tp)) = - let lenOT = openOpenTerm (typeCtxPureCtx ctx) len in + let lenOT = monadifyTypeNat ctx len in MTySeq (ctorOpenTerm "Cryptol.TCNum" [lenOT]) $ monadifyType ctx tp -monadifyType ctx tp@(asApplyAll -> ((asGlobalDef -> Just seq_id), [n, a])) +monadifyType ctx (asApplyAll -> ((asGlobalDef -> Just seq_id), [n, a])) | seq_id == "Cryptol.seq" = - case monTypeNum (monadifyType ctx n) of - Just n_trm -> MTySeq n_trm (monadifyType ctx a) - Nothing -> - error ("Monadify type: not a number: " ++ ppTermInTypeCtx ctx n - ++ " in type: " ++ ppTermInTypeCtx ctx tp) + let nOT = monadifyTypeArgType ctx n in + MTySeq nOT $ monadifyType ctx a monadifyType ctx (asApp -> Just ((asGlobalDef -> Just f), arg)) | Just f_trans <- lookup f typeclassMonMap = MTyBase (MKType $ mkSort 1) $ @@ -442,9 +441,16 @@ monadifyType ctx (asApplyAll -> (f, args)) MTyBase k_out (applyOpenTermMulti (globalDefOpenTerm glob) $ map toArgType margs) -} -monadifyType ctx tp@(asCtor -> Just (pn, _)) - | primName pn == "Cryptol.TCNum" || primName pn == "Cryptol.TCInf" = - MTyNum $ openOpenTerm (typeCtxPureCtx ctx) tp +monadifyType _ (asCtor -> Just (pn, [])) + | primName pn == "Cryptol.TCInf" + = MTyNum $ ctorOpenTerm "Cryptol.TCInf" [] +monadifyType ctx (asCtor -> Just (pn, [n])) + | primName pn == "Cryptol.TCNum" + = MTyNum $ ctorOpenTerm "Cryptol.TCNum" [monadifyTypeNat ctx n] +monadifyType ctx (asApplyAll -> ((asGlobalDef -> Just f), args)) + | f `elem` typeLevelOpMonList = + MTyNum $ + applyOpenTermMulti (globalOpenTerm f) $ map (monadifyTypeArgType ctx) args monadifyType ctx (asLocalVar -> Just i) | i < length ctx , (_,_,Just tp) <- ctx!!i = tp @@ -452,6 +458,16 @@ monadifyType ctx tp = error ("monadifyType: not a valid type for monadification: " ++ ppTermInTypeCtx ctx tp) +-- | Monadify a type-level natural number +monadifyTypeNat :: HasCallStack => MonadifyTypeCtx -> Term -> OpenTerm +monadifyTypeNat _ (asNat -> Just n) = natOpenTerm n +monadifyTypeNat ctx (asLocalVar -> Just i) + | i < length ctx + , (_,_,Just tp) <- ctx!!i = toArgType tp +monadifyTypeNat ctx tp = + error ("monadifyTypeNat: not a valid natural number for monadification: " + ++ ppTermInTypeCtx ctx tp) + ---------------------------------------------------------------------- -- * Monadified Terms @@ -814,7 +830,7 @@ assertIsFinite _ = ---------------------------------------------------------------------- -- | Monadify a type in the context of the 'MonadifyM' monad -monadifyTypeM :: Term -> MonadifyM MonType +monadifyTypeM :: HasCallStack => Term -> MonadifyM MonType monadifyTypeM tp = do ctx <- monStCtx <$> ask return $ monadifyType (ctxToTypeCtx ctx) tp From 4b31670e936d8d29c3040e4a941c4f0420492089 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Wed, 1 Jun 2022 17:22:14 -0700 Subject: [PATCH 10/17] added more debugging to monadification --- .../src/Verifier/SAW/Cryptol/Monadify.hs | 28 +++++++++++++------ 1 file changed, 19 insertions(+), 9 deletions(-) diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs index ab1e5c46d5..e1b1a06a4d 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs @@ -607,13 +607,21 @@ failArgMonTerm :: MonType -> String -> ArgMonTerm failArgMonTerm tp str = fromArgTerm tp (failOpenTerm str) -- | Apply a monadified term to a type or term argument -applyMonTerm :: MonTerm -> Either MonType ArgMonTerm -> MonTerm +applyMonTerm :: HasCallStack => MonTerm -> Either MonType ArgMonTerm -> MonTerm applyMonTerm (ArgMonTerm (FunMonTerm _ _ _ f)) (Right arg) = f arg applyMonTerm (ArgMonTerm (ForallMonTerm _ _ f)) (Left mtp) = f mtp -applyMonTerm _ _ = error "applyMonTerm: application at incorrect type" +applyMonTerm (ArgMonTerm (FunMonTerm _ _ _ _)) (Left _) = + error "applyMonTerm: application of term-level function to type-level argument" +applyMonTerm (ArgMonTerm (ForallMonTerm _ _ _)) (Right _) = + error "applyMonTerm: application of type-level function to term-level argument" +applyMonTerm (ArgMonTerm (BaseMonTerm _ _)) _ = + error "applyMonTerm: application of non-function base term" +applyMonTerm (CompMonTerm _ _) _ = + error "applyMonTerm: application of computational term" -- | Apply a monadified term to 0 or more arguments -applyMonTermMulti :: MonTerm -> [Either MonType ArgMonTerm] -> MonTerm +applyMonTermMulti :: HasCallStack => MonTerm -> [Either MonType ArgMonTerm] -> + MonTerm applyMonTermMulti = foldl applyMonTerm -- | Build a 'MonTerm' from a global of a given argument type @@ -836,7 +844,7 @@ monadifyTypeM tp = return $ monadifyType (ctxToTypeCtx ctx) tp -- | Monadify a term to a monadified term of argument type -monadifyArg :: Maybe MonType -> Term -> MonadifyM ArgMonTerm +monadifyArg :: HasCallStack => Maybe MonType -> Term -> MonadifyM ArgMonTerm {- monadifyArg _ t | trace ("Monadifying term of argument type: " ++ showTerm t) False @@ -848,7 +856,7 @@ monadifyArg mtp t = monadifyTerm' mtp t >>= argifyMonTerm -- | Monadify a term to argument type and convert back to a term -monadifyArgTerm :: Maybe MonType -> Term -> MonadifyM OpenTerm +monadifyArgTerm :: HasCallStack => Maybe MonType -> Term -> MonadifyM OpenTerm monadifyArgTerm mtp t = toArgTerm <$> monadifyArg mtp t -- | Monadify a term @@ -868,7 +876,7 @@ monadifyTerm mtp t = -- (i.e.,, lambdas, pairs, and records), but is optional for elimination forms -- (i.e., applications, projections, and also in this case variables). Note that -- this means monadification will fail on terms with beta or tuple redexes. -monadifyTerm' :: Maybe MonType -> Term -> MonadifyM MonTerm +monadifyTerm' :: HasCallStack => Maybe MonType -> Term -> MonadifyM MonTerm monadifyTerm' (Just mtp) t@(asLambda -> Just _) = ask >>= \(MonadifyROState { monStEnv = env, monStCtx = ctx }) -> return $ monadifyLambdas env ctx mtp t @@ -954,7 +962,7 @@ monadifyTerm' _ t = -- | Monadify the application of a monadified term to a list of terms, using the -- type of the already monadified to monadify the arguments -monadifyApply :: MonTerm -> [Term] -> MonadifyM MonTerm +monadifyApply :: HasCallStack => MonTerm -> [Term] -> MonadifyM MonTerm monadifyApply f (t : ts) | MTyArrow tp_in _ <- getMonType f = do mtrm <- monadifyArg (Just tp_in) t @@ -969,7 +977,8 @@ monadifyApply f [] = return f -- | FIXME: documentation; get our type down to a base type before going into -- the MonadifyM monad -monadifyLambdas :: MonadifyEnv -> MonadifyCtx -> MonType -> Term -> MonTerm +monadifyLambdas :: HasCallStack => MonadifyEnv -> MonadifyCtx -> + MonType -> Term -> MonTerm monadifyLambdas env ctx (MTyForall _ k tp_f) (asLambda -> Just (x, x_tp, body)) = -- FIXME: check that monadifyKind x_tp == k @@ -984,7 +993,8 @@ monadifyLambdas env ctx tp t = monadifyEtaExpand env ctx tp tp t [] -- | FIXME: documentation -monadifyEtaExpand :: MonadifyEnv -> MonadifyCtx -> MonType -> MonType -> Term -> +monadifyEtaExpand :: HasCallStack => MonadifyEnv -> MonadifyCtx -> + MonType -> MonType -> Term -> [Either MonType ArgMonTerm] -> MonTerm monadifyEtaExpand env ctx top_mtp (MTyForall x k tp_f) t args = ArgMonTerm $ ForallMonTerm x k $ \mtp -> From 6da9d1b5e4473abe894d3cc567964994b8b58988 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Wed, 1 Jun 2022 17:24:53 -0700 Subject: [PATCH 11/17] eta-expanded the call to processBlocks_loop_spec in processBlocks_spec in order to get monadification to work --- heapster-saw/examples/sha512.cry | 2 +- heapster-saw/examples/sha512_mr_solver.saw | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/heapster-saw/examples/sha512.cry b/heapster-saw/examples/sha512.cry index 7dbf6f5daf..6301f45d4b 100644 --- a/heapster-saw/examples/sha512.cry +++ b/heapster-saw/examples/sha512.cry @@ -138,7 +138,7 @@ processBlock_loop_spec i a b c d e f g h X T1 in = processBlocks_spec : {n} Literal n [64] => [8][w] -> [16*n][w] -> ([8][w], [16*n][w]) -processBlocks_spec = processBlocks_loop_spec 0 `n +processBlocks_spec x y = processBlocks_loop_spec 0 `n x y processBlocks_loop_spec : {n} Literal n [64] => [w] -> [w] -> [8][w] -> [16*n][w] -> ([8][w], [16*n][w]) diff --git a/heapster-saw/examples/sha512_mr_solver.saw b/heapster-saw/examples/sha512_mr_solver.saw index 587ab8a528..d9bb612591 100644 --- a/heapster-saw/examples/sha512_mr_solver.saw +++ b/heapster-saw/examples/sha512_mr_solver.saw @@ -24,10 +24,10 @@ monadify_term {{ round_00_15_spec }}; monadify_term {{ round_16_80_spec }}; monadify_term {{ processBlock_loop_spec }}; monadify_term {{ processBlock_spec }}; -// monadify_term {{ processBlocks_loop_spec }}; -// monadify_term {{ processBlocks_spec }}; +monadify_term {{ processBlocks_loop_spec }}; +monadify_term {{ processBlocks_spec }}; mr_solver_prove round_00_15 {{ round_00_15_spec }}; mr_solver_prove round_16_80 {{ round_16_80_spec }}; mr_solver_prove processBlock {{ processBlock_spec }}; -// mr_solver_prove processBlocks {{ processBlocks_spec }}; +mr_solver_prove processBlocks {{ processBlocks_spec }}; From 59f44952a68336454f1aee51df185c75e14218b9 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Tue, 7 Jun 2022 13:22:18 -0700 Subject: [PATCH 12/17] fully apply processBlocks_loop_spec --- heapster-saw/examples/sha512.cry | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/heapster-saw/examples/sha512.cry b/heapster-saw/examples/sha512.cry index 6301f45d4b..75591adc34 100644 --- a/heapster-saw/examples/sha512.cry +++ b/heapster-saw/examples/sha512.cry @@ -138,7 +138,7 @@ processBlock_loop_spec i a b c d e f g h X T1 in = processBlocks_spec : {n} Literal n [64] => [8][w] -> [16*n][w] -> ([8][w], [16*n][w]) -processBlocks_spec x y = processBlocks_loop_spec 0 `n x y +processBlocks_spec state in = processBlocks_loop_spec 0 `n state in processBlocks_loop_spec : {n} Literal n [64] => [w] -> [w] -> [8][w] -> [16*n][w] -> ([8][w], [16*n][w]) From ce0142a3e91e0a72e210b722753678096b1936ba Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Tue, 7 Jun 2022 13:31:47 -0700 Subject: [PATCH 13/17] move BVVec/Vec length checking out of matchHet --- src/SAWScript/Prover/MRSolver/Monad.hs | 34 +++++++++++-------------- src/SAWScript/Prover/MRSolver/SMT.hs | 15 ++++++++--- src/SAWScript/Prover/MRSolver/Solver.hs | 28 ++++++++++++-------- 3 files changed, 44 insertions(+), 33 deletions(-) diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs index 0aedffccdc..c7755839ea 100644 --- a/src/SAWScript/Prover/MRSolver/Monad.hs +++ b/src/SAWScript/Prover/MRSolver/Monad.hs @@ -479,9 +479,9 @@ liftSC5 f a b c d e = mrSC >>= \sc -> liftIO (f sc a b c d e) -- | A datatype encapsulating all the way in which we consider two types to -- be heterogeneously related: either one is a @Num@ and the other is a @Nat@, -- one is a @BVVec@ and the other is a non-@BVVec@ vector (of the same length, --- this is checked in 'matchHet'), or both sides are pairs (whose components --- are respectively heterogeneously related, this recursion must be done where --- 'matchHet' is used, see 'typesHetRelated', for example) +-- which must be checked where 'matchHet' is used), or both sides are pairs +-- (whose components are respectively heterogeneously related, which must be +-- checked where 'matchHet' is used). See 'typesHetRelated' for an example. data HetRelated = HetBVNum Natural | HetNumBV Natural | HetBVVecVec (Term, Term, Term) (Term, Term) @@ -489,37 +489,33 @@ data HetRelated = HetBVNum Natural | HetPair (Term, Term) (Term, Term) -- | Check to see if the given types match one of the cases of 'HetRelated' -matchHet :: Term -> Term -> MRM (Maybe HetRelated) +matchHet :: Term -> Term -> Maybe HetRelated matchHet (asBitvectorType -> Just n) (asDataType -> Just (primName -> "Cryptol.Num", _)) = - return $ Just $ HetBVNum n + Just $ HetBVNum n matchHet (asDataType -> Just (primName -> "Cryptol.Num", _)) (asBitvectorType -> Just n) = - return $ Just $ HetNumBV n + Just $ HetNumBV n matchHet (asBVVecType -> Just (n, len, a)) (asNonBVVecVectorType -> Just (m, a')) = - do m' <- mrBvToNat n len - ms_are_eq <- mrConvertible m' m - return $ if ms_are_eq then Just $ HetBVVecVec (n, len, a) (m, a') - else Nothing + Just $ HetBVVecVec (n, len, a) (m, a') matchHet (asNonBVVecVectorType -> Just (m, a')) (asBVVecType -> Just (n, len, a)) = - do m' <- mrBvToNat n len - ms_are_eq <- mrConvertible m' m - return $ if ms_are_eq then Just $ HetVecBVVec (m, a') (n, len, a) - else Nothing + Just $ HetVecBVVec (m, a') (n, len, a) matchHet (asPairType -> Just (tpL1, tpR1)) (asPairType -> Just (tpL2, tpR2)) = - return $ Just $ HetPair (tpL1, tpR1) (tpL2, tpR2) -matchHet _ _ = return $ Nothing + Just $ HetPair (tpL1, tpR1) (tpL2, tpR2) +matchHet _ _ = Nothing -- | Return true iff the given types are heterogeneously related typesHetRelated :: Term -> Term -> MRM Bool -typesHetRelated tp1 tp2 = matchHet tp1 tp2 >>= \case +typesHetRelated tp1 tp2 = case matchHet tp1 tp2 of Just (HetBVNum _) -> return True Just (HetNumBV _) -> return True - Just (HetBVVecVec (_, _, a) (_, a')) -> typesHetRelated a a' - Just (HetVecBVVec (_, a') (_, _, a)) -> typesHetRelated a' a + Just (HetBVVecVec (n, len, a) (m, a')) -> mrBvToNat n len >>= \m' -> + (&&) <$> mrConvertible m m' <*> typesHetRelated a a' + Just (HetVecBVVec (m, a') (n, len, a)) -> mrBvToNat n len >>= \m' -> + (&&) <$> mrConvertible m m' <*> typesHetRelated a a' Just (HetPair (tpL1, tpR1) (tpL2, tpR2)) -> (&&) <$> typesHetRelated tpL1 tpL2 <*> typesHetRelated tpR1 tpR2 Nothing -> mrConvertible tp1 tp2 diff --git a/src/SAWScript/Prover/MRSolver/SMT.hs b/src/SAWScript/Prover/MRSolver/SMT.hs index c7a15f09d2..6c14d14cbc 100644 --- a/src/SAWScript/Prover/MRSolver/SMT.hs +++ b/src/SAWScript/Prover/MRSolver/SMT.hs @@ -2,7 +2,6 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE ImplicitParams #-} -{-# LANGUAGE TupleSections #-} {- | Module : SAWScript.Prover.MRSolver.SMT @@ -549,7 +548,7 @@ mrProveRelH' _ het tp1@(asNonBVVecVectorType -> Just (m1, tpA1)) t2' <- mrGenBVVecFromVec m2 tpA2 t2 "mrProveRelH (BVVec/BVVec)" n len mrProveRelH het tp1' tp2' t1' t2' -mrProveRelH' _ het tp1 tp2 t1 t2 = (het,) <$> matchHet tp1 tp2 >>= \case +mrProveRelH' _ het tp1 tp2 t1 t2 = case (het, matchHet tp1 tp2) of -- If our relation is heterogeneous and we have a bitvector on one side and -- a Num on the other, ensure that the Num term is TCNum of some Nat, wrap @@ -571,13 +570,21 @@ mrProveRelH' _ het tp1 tp2 t1 t2 = (het,) <$> matchHet tp1 tp2 >>= \case -- non-BVVec vector on the other, wrap the non-BVVec vector term in -- genBVVecFromVec and recurse (True, Just (HetBVVecVec (n, len, _) (m, tpA2))) -> - do len' <- liftSC2 scGlobalApply "Prelude.bvToNat" [n, len] + do m' <- mrBvToNat n len + ms_are_eq <- mrConvertible m' m + if ms_are_eq then return () else + throwMRFailure (TypesNotRel True (Type tp1) (Type tp2)) + len' <- liftSC2 scGlobalApply "Prelude.bvToNat" [n, len] tp2' <- liftSC2 scVecType len' tpA2 t2' <- mrGenBVVecFromVec m tpA2 t2 "mrProveRelH (BVVec/Vec)" n len -- mrDebugPPPrefixSep 2 "mrProveRelH on BVVec/Vec: " t1 "an`d" t2' mrProveRelH True tp1 tp2' t1 t2' (True, Just (HetVecBVVec (m, tpA1) (n, len, _))) -> - do len' <- liftSC2 scGlobalApply "Prelude.bvToNat" [n, len] + do m' <- mrBvToNat n len + ms_are_eq <- mrConvertible m' m + if ms_are_eq then return () else + throwMRFailure (TypesNotRel True (Type tp1) (Type tp2)) + len' <- liftSC2 scGlobalApply "Prelude.bvToNat" [n, len] tp1' <- liftSC2 scVecType len' tpA1 t1' <- mrGenBVVecFromVec m tpA1 t1 "mrProveRelH (Vec/BVVec)" n len -- mrDebugPPPrefixSep 2 "mrProveRelH on Vec/BVVec: " t1' "and" t2 diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs index 132073ac18..34cb3c7ac3 100644 --- a/src/SAWScript/Prover/MRSolver/Solver.hs +++ b/src/SAWScript/Prover/MRSolver/Solver.hs @@ -612,7 +612,7 @@ generalizeCoIndHypArgs hyp [(specs, tp)] = do (hyp', var) <- coIndHypWithVar hyp "z" (Type tp) return $ coIndHypSetArgs hyp' specs var -generalizeCoIndHypArgs hyp [(specs1, tp1), (specs2, tp2)] = matchHet tp1 tp2 >>= \case +generalizeCoIndHypArgs hyp [(specs1, tp1), (specs2, tp2)] = case matchHet tp1 tp2 of -- If we need to generalize bitvector arguments with Num arguments, introduce -- a bitvector variable and set all of the bitvector arguments to it and @@ -635,16 +635,20 @@ generalizeCoIndHypArgs hyp [(specs1, tp1), (specs2, tp2)] = matchHet tp1 tp2 >>= -- Vec arguments to `genBVVecFromVec` of it -- FIXME: Could we handle the a /= a' case here and in mrRefinesFunH? Just (HetBVVecVec (n, len, a) (m, a')) -> - do as_are_eq <- mrConvertible a a' - if as_are_eq then return () else + do m' <- mrBvToNat n len + ms_are_eq <- mrConvertible m m' + as_are_eq <- mrConvertible a a' + if ms_are_eq && as_are_eq then return () else throwMRFailure (TypesNotRel True (Type tp1) (Type tp2)) (hyp', var) <- coIndHypWithVar hyp "z" (Type tp1) bvv_tm <- mrGenFromBVVec n len a var "generalizeCoIndHypArgs (BVVec/Vec)" m let hyp'' = coIndHypSetArgs hyp' specs1 var return $ coIndHypSetArgs hyp'' specs2 bvv_tm Just (HetVecBVVec (m, a') (n, len, a)) -> - do as_are_eq <- mrConvertible a a' - if as_are_eq then return () else + do m' <- mrBvToNat n len + ms_are_eq <- mrConvertible m m' + as_are_eq <- mrConvertible a a' + if ms_are_eq && as_are_eq then return () else throwMRFailure (TypesNotRel True (Type tp1) (Type tp2)) (hyp', var) <- coIndHypWithVar hyp "z" (Type tp2) bvv_tm <- mrGenFromBVVec n len a var "generalizeCoIndHypArgs (Vec/BVVec)" m @@ -1030,7 +1034,7 @@ mrRefinesFunH :: (Term -> Term -> MRM a) -> [Term] -> [(LocalName,Term)] -> Term -> [(LocalName,Term)] -> Term -> MRM a -mrRefinesFunH k vars ((nm1, tp1):tps1) t1 ((nm2, tp2):tps2) t2 = matchHet tp1 tp2 >>= \case +mrRefinesFunH k vars ((nm1, tp1):tps1) t1 ((nm2, tp2):tps2) t2 = case matchHet tp1 tp2 of -- If we need to introduce a bitvector on one side and a Num on the other, -- introduce a bitvector variable and substitute `TCNum` of `bvToNat` of that @@ -1063,8 +1067,10 @@ mrRefinesFunH k vars ((nm1, tp1):tps1) t1 ((nm2, tp2):tps2) t2 = matchHet tp1 tp -- variable on the non-BVVec side -- FIXME: Could we handle the a /= a' case here and in generalizeCoIndHypArgs? Just (HetBVVecVec (n, len, a) (m, a')) -> - do as_are_eq <- mrConvertible a a' - if as_are_eq then return () else + do m' <- mrBvToNat n len + ms_are_eq <- mrConvertible m m' + as_are_eq <- mrConvertible a a' + if ms_are_eq && as_are_eq then return () else throwMRFailure (TypesNotRel True (Type tp1) (Type tp2)) let nm = maybe "_" id $ find ((/=) '_' . Text.head) $ [nm1, nm2] ++ catMaybes [ asLambdaName t1 @@ -1076,8 +1082,10 @@ mrRefinesFunH k vars ((nm1, tp1):tps1) t1 ((nm2, tp2):tps2) t2 = matchHet tp1 tp t2'' <- mrApplyAll t2' [bvv_tm] mrRefinesFunH k (var : vars') tps1 t1'' tps2' t2'' Just (HetVecBVVec (m, a') (n, len, a)) -> - do as_are_eq <- mrConvertible a a' - if as_are_eq then return () else + do m' <- mrBvToNat n len + ms_are_eq <- mrConvertible m m' + as_are_eq <- mrConvertible a a' + if ms_are_eq && as_are_eq then return () else throwMRFailure (TypesNotRel True (Type tp1) (Type tp2)) let nm = maybe "_" id $ find ((/=) '_' . Text.head) $ [nm1, nm2] ++ catMaybes [ asLambdaName t1 From d963243d5c429021ede5d260f599eb9b6a3ce23b Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Tue, 7 Jun 2022 13:34:48 -0700 Subject: [PATCH 14/17] fix substitution in mrRefinesFunH in the case of dependent types --- src/SAWScript/Prover/MRSolver/Solver.hs | 24 ++++++++++++++++++------ 1 file changed, 18 insertions(+), 6 deletions(-) diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs index 34cb3c7ac3..15915e1271 100644 --- a/src/SAWScript/Prover/MRSolver/Solver.hs +++ b/src/SAWScript/Prover/MRSolver/Solver.hs @@ -1016,8 +1016,8 @@ mrRefinesFun :: Term -> CompFun -> Term -> CompFun -> MRM () mrRefinesFun tp1 f1 tp2 f2 = do mrDebugPPPrefixSep 1 "mrRefinesFun on types:" tp1 "," tp2 mrDebugPPPrefixSep 1 "mrRefinesFun" f1 "|=" f2 - f1' <- compFunToTerm f1 - f2' <- compFunToTerm f2 + f1' <- compFunToTerm f1 >>= liftSC1 scWhnf + f2' <- compFunToTerm f2 >>= liftSC1 scWhnf let lnm = maybe "call_ret_val" id (compFunVarName f1) rnm = maybe "call_ret_val" id (compFunVarName f2) mrRefinesFunH mrRefines [] [(lnm, tp1)] f1' [(rnm, tp2)] f2' @@ -1046,7 +1046,10 @@ mrRefinesFunH k vars ((nm1, tp1):tps1) t1 ((nm2, tp2):tps2) t2 = case matchHet t withUVarLift nm (Type tp1) (vars, t1, t2) $ \var (vars', t1', t2') -> do nat_tm <- liftSC2 scBvToNat n var num_tm <- liftSC2 scCtorApp "Cryptol.TCNum" [nat_tm] - tps2' <- substTermLike 0 (num_tm : vars') tps2 + tps2' <- zipWithM (\i tp -> liftTermLike 0 i num_tm >>= \num_tm' -> + substTermLike i (num_tm' : vars') tp >>= + mapM (liftSC1 scWhnf)) + [0..] tps2 t1'' <- mrApplyAll t1' [var] t2'' <- mrApplyAll t2' [num_tm] mrRefinesFunH k (var : vars') tps1 t1'' tps2' t2'' @@ -1057,7 +1060,10 @@ mrRefinesFunH k vars ((nm1, tp1):tps1) t1 ((nm2, tp2):tps2) t2 = case matchHet t withUVarLift nm (Type tp2) (vars, t1, t2) $ \var (vars', t1', t2') -> do nat_tm <- liftSC2 scBvToNat n var num_tm <- liftSC2 scCtorApp "Cryptol.TCNum" [nat_tm] - tps1' <- substTermLike 0 (num_tm : vars') tps1 + tps1' <- zipWithM (\i tp -> liftTermLike 0 i num_tm >>= \num_tm' -> + substTermLike i (num_tm' : vars') tp >>= + mapM (liftSC1 scWhnf)) + [0..] tps1 t1'' <- mrApplyAll t1' [num_tm] t2'' <- mrApplyAll t2' [var] mrRefinesFunH k (var : vars') tps1' t1'' tps2 t2'' @@ -1077,7 +1083,10 @@ mrRefinesFunH k vars ((nm1, tp1):tps1) t1 ((nm2, tp2):tps2) t2 = case matchHet t , asLambdaName t2 ] withUVarLift nm (Type tp1) (vars, t1, t2) $ \var (vars', t1', t2') -> do bvv_tm <- mrGenFromBVVec n len a var "mrRefinesFunH (BVVec/Vec)" m - tps2' <- substTermLike 0 (bvv_tm : vars') tps2 + tps2' <- zipWithM (\i tp -> liftTermLike 0 i bvv_tm >>= \bvv_tm' -> + substTermLike i (bvv_tm' : vars') tp >>= + mapM (liftSC1 scWhnf)) + [0..] tps2 t1'' <- mrApplyAll t1' [var] t2'' <- mrApplyAll t2' [bvv_tm] mrRefinesFunH k (var : vars') tps1 t1'' tps2' t2'' @@ -1092,7 +1101,10 @@ mrRefinesFunH k vars ((nm1, tp1):tps1) t1 ((nm2, tp2):tps2) t2 = case matchHet t , asLambdaName t2 ] withUVarLift nm (Type tp2) (vars, t1, t2) $ \var (vars', t1', t2') -> do bvv_tm <- mrGenFromBVVec n len a var "mrRefinesFunH (BVVec/Vec)" m - tps1' <- substTermLike 0 (bvv_tm : vars') tps1 + tps1' <- zipWithM (\i tp -> liftTermLike 0 i bvv_tm >>= \bvv_tm' -> + substTermLike i (bvv_tm' : vars') tp >>= + mapM (liftSC1 scWhnf)) + [0..] tps1 t1'' <- mrApplyAll t1' [var] t2'' <- mrApplyAll t2' [bvv_tm] mrRefinesFunH k (var : vars') tps1' t1'' tps2 t2'' From cd2a42734fcd356143f8cd917d9f700a472f8f2c Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Tue, 7 Jun 2022 13:42:31 -0700 Subject: [PATCH 15/17] add mrEq' case for `Num`s --- src/SAWScript/Prover/MRSolver/SMT.hs | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/SAWScript/Prover/MRSolver/SMT.hs b/src/SAWScript/Prover/MRSolver/SMT.hs index 6c14d14cbc..29f83c6cb9 100644 --- a/src/SAWScript/Prover/MRSolver/SMT.hs +++ b/src/SAWScript/Prover/MRSolver/SMT.hs @@ -350,11 +350,20 @@ mrEq t1 t2 = mrTypeOf t1 >>= \tp -> mrEq' tp t1 t2 -- are equal, where the first 'Term' gives their type (which we assume is the -- same for both). This is like 'scEq' except that it works on open terms. mrEq' :: Term -> Term -> Term -> MRM Term +-- FIXME: For this Nat case, the definition of 'equalNat' in @Prims.hs@ means +-- that if both sides do not have immediately clear bit-widths (e.g. either +-- side is is an application of @mulNat@) this will 'error'... mrEq' (asNatType -> Just _) t1 t2 = liftSC2 scEqualNat t1 t2 mrEq' (asBoolType -> Just _) t1 t2 = liftSC2 scBoolEq t1 t2 mrEq' (asIntegerType -> Just _) t1 t2 = liftSC2 scIntEq t1 t2 mrEq' (asVectorType -> Just (n, asBoolType -> Just ())) t1 t2 = liftSC3 scBvEq n t1 t2 +mrEq' (asDataType -> Just (primName -> "Cryptol.Num", _)) t1 t2 = + liftSC1 scWhnf t1 >>= \t1' -> liftSC1 scWhnf t2 >>= \t2' -> case (t1', t2') of + (asCtor -> Just (primName -> "Cryptol.TCNum", [t1'']), + asCtor -> Just (primName -> "Cryptol.TCNum", [t2''])) -> + liftSC0 scNatType >>= \nat_tp -> mrEq' nat_tp t1'' t2'' + _ -> error "mrEq': Num terms do not normalize to TCNum constructors" mrEq' _ _ _ = error "mrEq': unsupported type" -- | A 'Term' in an extended context of universal variables, which are listed From 01cad57f468707ab0441cf3def657b36fd418bfa Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Tue, 7 Jun 2022 13:42:47 -0700 Subject: [PATCH 16/17] comment out processBlocks |= processBlocks_spec for now --- heapster-saw/examples/sha512_mr_solver.saw | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/heapster-saw/examples/sha512_mr_solver.saw b/heapster-saw/examples/sha512_mr_solver.saw index d9bb612591..bd7ea87192 100644 --- a/heapster-saw/examples/sha512_mr_solver.saw +++ b/heapster-saw/examples/sha512_mr_solver.saw @@ -30,4 +30,4 @@ monadify_term {{ processBlocks_spec }}; mr_solver_prove round_00_15 {{ round_00_15_spec }}; mr_solver_prove round_16_80 {{ round_16_80_spec }}; mr_solver_prove processBlock {{ processBlock_spec }}; -mr_solver_prove processBlocks {{ processBlocks_spec }}; +// mr_solver_prove processBlocks {{ processBlocks_spec }}; From b8d2a5f44899734550949232e2dc403a6004b7e5 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Tue, 7 Jun 2022 16:46:24 -0700 Subject: [PATCH 17/17] modify mrProveRelH' to pass GHC 9.0's pattern match checker --- src/SAWScript/Prover/MRSolver/SMT.hs | 52 +++++++++++++++++----------- 1 file changed, 31 insertions(+), 21 deletions(-) diff --git a/src/SAWScript/Prover/MRSolver/SMT.hs b/src/SAWScript/Prover/MRSolver/SMT.hs index 29f83c6cb9..29142dc90c 100644 --- a/src/SAWScript/Prover/MRSolver/SMT.hs +++ b/src/SAWScript/Prover/MRSolver/SMT.hs @@ -557,18 +557,18 @@ mrProveRelH' _ het tp1@(asNonBVVecVectorType -> Just (m1, tpA1)) t2' <- mrGenBVVecFromVec m2 tpA2 t2 "mrProveRelH (BVVec/BVVec)" n len mrProveRelH het tp1' tp2' t1' t2' -mrProveRelH' _ het tp1 tp2 t1 t2 = case (het, matchHet tp1 tp2) of +mrProveRelH' _ True tp1 tp2 t1 t2 | Just mh <- matchHet tp1 tp2 = case mh of -- If our relation is heterogeneous and we have a bitvector on one side and -- a Num on the other, ensure that the Num term is TCNum of some Nat, wrap -- the Nat with bvNat, and recurse - (True, Just (HetBVNum n)) + HetBVNum n | Just (primName -> "Cryptol.TCNum", [t2']) <- asCtor t2 -> do n_tm <- liftSC1 scNat n t2'' <- liftSC2 scGlobalApply "Prelude.bvNat" [n_tm, t2'] mrProveRelH True tp1 tp1 t1 t2'' | otherwise -> throwMRFailure (TermsNotEq t1 t2) - (True, Just (HetNumBV n)) + HetNumBV n | Just (primName -> "Cryptol.TCNum", [t1']) <- asCtor t1 -> do n_tm <- liftSC1 scNat n t1'' <- liftSC2 scGlobalApply "Prelude.bvNat" [n_tm, t1'] @@ -578,7 +578,7 @@ mrProveRelH' _ het tp1 tp2 t1 t2 = case (het, matchHet tp1 tp2) of -- If our relation is heterogeneous and we have a BVVec on one side and a -- non-BVVec vector on the other, wrap the non-BVVec vector term in -- genBVVecFromVec and recurse - (True, Just (HetBVVecVec (n, len, _) (m, tpA2))) -> + HetBVVecVec (n, len, _) (m, tpA2) -> do m' <- mrBvToNat n len ms_are_eq <- mrConvertible m' m if ms_are_eq then return () else @@ -588,7 +588,7 @@ mrProveRelH' _ het tp1 tp2 t1 t2 = case (het, matchHet tp1 tp2) of t2' <- mrGenBVVecFromVec m tpA2 t2 "mrProveRelH (BVVec/Vec)" n len -- mrDebugPPPrefixSep 2 "mrProveRelH on BVVec/Vec: " t1 "an`d" t2' mrProveRelH True tp1 tp2' t1 t2' - (True, Just (HetVecBVVec (m, tpA1) (n, len, _))) -> + HetVecBVVec (m, tpA1) (n, len, _) -> do m' <- mrBvToNat n len ms_are_eq <- mrConvertible m' m if ms_are_eq then return () else @@ -600,25 +600,35 @@ mrProveRelH' _ het tp1 tp2 t1 t2 = case (het, matchHet tp1 tp2) of mrProveRelH True tp1' tp2 t1' t2 -- For pair types, prove both the left and right projections are related - (_, Just (HetPair (tpL1, tpR1) (tpL2, tpR2))) -> + -- (this should be the same as the pair case below - we have to split them + -- up because otherwise GHC 9.0's pattern match checker complains...) + HetPair (tpL1, tpR1) (tpL2, tpR2) -> do t1L <- liftSC1 scPairLeft t1 t2L <- liftSC1 scPairLeft t2 t1R <- liftSC1 scPairRight t1 t2R <- liftSC1 scPairRight t2 - condL <- mrProveRelH het tpL1 tpL2 t1L t2L - condR <- mrProveRelH het tpR1 tpR2 t1R t2R + condL <- mrProveRelH True tpL1 tpL2 t1L t2L + condR <- mrProveRelH True tpR1 tpR2 t1R t2R liftTermInCtx2 scAnd condL condR - -- As a fallback, for types we can't handle, just check convertibility (we do - -- this in two cases to make sure we catch any missed 'HetRelated' patterns) - (True, Nothing) -> - do success <- mrConvertible t1 t2 - if success then return () else - mrDebugPPPrefixSep 2 "mrProveRel could not match types: " tp1 "and" tp2 >> - mrDebugPPPrefixSep 2 "and could not prove convertible: " t1 "and" t2 - TermInCtx [] <$> liftSC1 scBool success - (False, _)-> - do success <- mrConvertible t1 t2 - if success then return () else - mrDebugPPPrefixSep 2 "mrProveEq could not prove convertible: " t1 "and" t2 - TermInCtx [] <$> liftSC1 scBool success +-- For pair types, prove both the left and right projections are related +-- (this should be the same as the pair case below - we have to split them +-- up because otherwise GHC 9.0's pattern match checker complains...) +mrProveRelH' _ False tp1 tp2 t1 t2 + | Just (HetPair (tpL1, tpR1) (tpL2, tpR2)) <- matchHet tp1 tp2 = + do t1L <- liftSC1 scPairLeft t1 + t2L <- liftSC1 scPairLeft t2 + t1R <- liftSC1 scPairRight t1 + t2R <- liftSC1 scPairRight t2 + condL <- mrProveRelH False tpL1 tpL2 t1L t2L + condR <- mrProveRelH False tpR1 tpR2 t1R t2R + liftTermInCtx2 scAnd condL condR + +-- As a fallback, for types we can't handle, just check convertibility +mrProveRelH' _ het tp1 tp2 t1 t2 = + do success <- mrConvertible t1 t2 + if success then return () else + if het then mrDebugPPPrefixSep 2 "mrProveRelH' could not match types: " tp1 "and" tp2 >> + mrDebugPPPrefixSep 2 "and could not prove convertible: " t1 "and" t2 + else mrDebugPPPrefixSep 2 "mrProveEq could not prove convertible: " t1 "and" t2 + TermInCtx [] <$> liftSC1 scBool success