From 504a9e51c7f889b5623d6858ef3174e954a9e07c Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Thu, 21 Oct 2021 14:29:21 -0700 Subject: [PATCH 01/10] initial progress on SHA512 example --- heapster-saw/examples/_CoqProject | 2 + heapster-saw/examples/sha512.bc | Bin 0 -> 5360 bytes heapster-saw/examples/sha512.c | 228 ++++++++++++++++++++++++++ heapster-saw/examples/sha512.saw | 41 +++++ heapster-saw/examples/sha512_proofs.v | 20 +++ 5 files changed, 291 insertions(+) create mode 100644 heapster-saw/examples/sha512.bc create mode 100644 heapster-saw/examples/sha512.c create mode 100644 heapster-saw/examples/sha512.saw create mode 100644 heapster-saw/examples/sha512_proofs.v diff --git a/heapster-saw/examples/_CoqProject b/heapster-saw/examples/_CoqProject index 878793f383..8012aab001 100644 --- a/heapster-saw/examples/_CoqProject +++ b/heapster-saw/examples/_CoqProject @@ -28,3 +28,5 @@ clearbufs_gen.v clearbufs_proofs.v mbox_gen.v mbox_proofs.v +sha512_gen.v +sha512_proofs.v diff --git a/heapster-saw/examples/sha512.bc b/heapster-saw/examples/sha512.bc new file mode 100644 index 0000000000000000000000000000000000000000..2efb943af02a8ab38c990978fb8ccfc6d7730ed6 GIT binary patch literal 5360 zcmc&YZFCdYm2a$(M%c16#->OhDI;vM3ITg08)2{QAX%m{#W@H?Y?_G@LF!@r#h0gi@Ef9Jv@uvV`L_*(_(1 zv)TJbHf6U>|84i3^WMC7?|t{(d*8kHy*Jl08;cN>GN@Oep%5aP+?ne;^L^BzVJp7> z@(*77k6(VP_uX^*KmFGae!Y7~GhtT(y+wo2k4c1z3M{Aq#$SR;Maz%7X34!O+Fth( z5!Y;0stsoHI~_vVo`R;AikeQ-_Oe>FeqW*e;CKr^Z7FYFFHX>|mkK&()o05X_m{_+ zpAzBvzNKXy(|L^i-j>sGXl}$)iL&*rFH980Pq)&C z%29}voZO2jbwJIuNOszz<}Xcx{!hFqQoc+V}fEeaQhgS^NVup^i7}QgvBUB_1d!~g7N>mu- z5VN>sy2h9mCyl@jbC68gsCoVmOn7lPpcp(O4hf<|5_y^ec_L^IM1@5Od3wf_odn&# zaC$7#B8GU`hV!6;IGp^GrbAiN^;9t!DodDiV5KGF9|&ePdz)XsQ1QjC!=t* zDMA@BlAs)Iv7rF}OcRFx zg5kH&HIxt@TM%d>fr^~e=0p=(?e_e@|I2#T;sCM8M8~WrL_mVuRH3vD!0=UFlfy4?No5dF|+mwioGw zJO$E+7;2QIg7c~sh8m{jz6{J0fIAL3sZlQ#o>#pGtvu}YYDW+?N>f3B>dk3KBx=CB zIuVF_*`fi48j(t}iSaOs^nRL66s|yg2T|f$}LxggKd)uzrGNfOlQ6r#v zwdpD%*!x5y!n7)S@-5K+Fatm}RJ%Dz8%kOe6YCy+e1>$7?s4*OxFVX-n;x~_1H8_H zy}k={)oQ^wy=3evBO1ruwehKmCfQ>{$pOtRr2Bx@ek^FKHBDxS7jUXBRw8+7*wsnw~aYhcL95 zvYfe#eZKy!SpB@a?wq3Gtyn``Q9rj*HsqzA2~fKN;6>Cf0XsSGg)O6o?kR!oupqWW z5b4EWQj8>{+wZPu@8-1sp3&Z66&3;9gE+@1% zoVq1Odk3^&tdM+glwGzM7o+CIoN;-{^gdzk(jTZzyZ`!?SpA%*VpS2ZI6Oj)BoDNH zoX}wln7<*%wZ#Of^*O?f1-6)0IMtzJvD&$*`n0z3I_@#FkH9cA1x#HbOLA2LW0P_32pSx!C6TRPBVjZf>gK{AAti z6zJG6*K%$EV$Dkp;4CB>em$eT5U{A~<-*|z=i`R@`}|cvgnYqnK3o;> zb9^Z55AFb1m4Afm<$L@g7Y{At>*4yIW`^=|Fu;t%!75J=7w+m0_J*pS;C%a^Y^&r~0T0lC z^7ql9&ZDb@(EGn#r)n@1tm^Lb^$d3UtJ=d6-XE%JAMEZ6J8Ig)m4UThPe0g1ZU*~8 z-B0)VI~kyXJu6r1Y-4Ccx%zKyV=G1&*~eBY+=q!%7C=s_pg{zKp0`is$e(Kz70uO} zOU&DBYje#M+HlFK^coSXVBLb|5P~b*M@D3*k&rRdT|h8n@M*{^$NTfAfT4&R$c zL*37mzwUc9Wb+l(|HJ0jq;3C}4RRQ6DXk9~Uf;Ymc~BniEq^q0YV+0wnEua@%kaIh zs4!@S96^n?@kw_hgnHUtH$OFY%Q%xiq~XZ7m~P9l_obQ}UhVHZ5YoD39N4o_$10;~d6pjOqLFlK@DJ4DIffOmAmVLuZ zO3dvI%3}q@hmfJK0BpP-*>dVlM8e0 z{lQK@_Iq$w+y9ea)ULS&bng2C4#&TsJfR3U>8h{dB!ETAfB%9)bXV6pR;8#6w8Q=c zhr9daoYWrvqeuybxv;;xuWzuIJ7nvI(0To|yGY^una84_QL_~-An#Kp)6uJY-h9ES zt+83VHbjkqPS4!7g1Y%RDfv}$Q2INU?RE7XXLXE);jr}TBnQFMS148&<}^Md!PZ<%P@;dZc74 zOMaUxKKJ$pgythmRAaGsR-7=D%@fjPNzkHS6lVx&(TlXGG~V*}Ov}5ZOL|z{w9`eu zu`U}1g{n)k-%Dg$$qy?|v!x{s>mHeFCigcLR+mg-@bpI&r`R5+UQ0~qjYvI41iz2( zlIT-t+_x%ywr7E;_Y))U+zJ)^b zF}fDU%BVb{c|Dz(aD8YBB6N-hW^uwWOP~pT8CWWMSqY}mTLA~0Wx^8GIA%Es%*S08 z3OV;N)v9CqvJgxs?HoG7;N^RqH3R|duVB!8>1>?fqo`DsNfRYXlI76cdKx5nA`TMy zoGM`dO*P^0c_t8G5q7&?qWapeO-1!SS#Bxht1y+>IDvK!bzY|)=gxH#2UfD_jb?7Qe+5lFL( z^a?6W(mDhrn((Eno%W?UOKBnjC=19W>|?RXuKoUj`4-lLncdHegdG;Db+!+}m8HYahl4?X80GV8{d^ATSMzH=;orVB+|SBxuwUcR<1?i}` z8Jj67IF($*ecRckDcoaGpat)YD;qO(x3^4gShFwc#*=bV1z&Re*~30{l@fYj`}s^tg;e zmCq9RVmevb3Iyi?LM5v(dKIqTo?ip=u7qk>g(C)`%h1R0$DyvlF+DC{2VLN-z`ESQ za{u}JQBTiMZ)Io4)0LfmxV#7bU+6J1VXwc}$44r8w!1dpbUSMDcmI)EN4ukD2VCuY q{5yI%Uw>%C##Y*PRyx+69PNKzkoNyAN&6Ryk|+IBvS9t!%6|iC$>@#% literal 0 HcmV?d00001 diff --git a/heapster-saw/examples/sha512.c b/heapster-saw/examples/sha512.c new file mode 100644 index 0000000000..f60c585e1e --- /dev/null +++ b/heapster-saw/examples/sha512.c @@ -0,0 +1,228 @@ +#include +#include +#include + +// First simplication of sha512_block_data_order + +static inline uint64_t SIMPL1_CRYPTO_load_u64_be(const void *ptr) { + uint64_t ret; + memcpy(&ret, ptr, sizeof(ret)); + return ret; +} + +#define SIMPL1_ROUND_00_01(i, a) \ + do { \ + T1 += a; \ + a += T1; \ + } while (0) + +#define SIMPL1_ROUND_02_10(i, j, a) \ + do { \ + T1 += a; \ + a += T1; \ + } while (0) + +void sha512_block_data_order_simpl1(uint64_t *state, const uint8_t *in, size_t num) { + uint64_t a, T1; + int i; + + while (num--) { + + a = state[0]; + + T1 = SIMPL1_CRYPTO_load_u64_be(in); + SIMPL1_ROUND_00_01(0, a); + T1 = SIMPL1_CRYPTO_load_u64_be(in + 8); + SIMPL1_ROUND_00_01(1, a); + + for (i = 2; i < 10; i += 2) { + SIMPL1_ROUND_02_10(i, 0, a); + SIMPL1_ROUND_02_10(i, 1, a); + } + + state[0] += a; + + in += 2 * 8; + } +} + +// sha512_block_data_order + +static inline void *OPENSSL_memcpy(void *dst, const void *src, size_t n) { + if (n == 0) { + return dst; + } + + return memcpy(dst, src, n); +} + +static inline uint32_t CRYPTO_bswap4(uint32_t x) { + x = (x >> 16) | (x << 16); + x = ((x & 0xff00ff00) >> 8) | ((x & 0x00ff00ff) << 8); + return x; +} + +static inline uint64_t CRYPTO_bswap8(uint64_t x) { + return CRYPTO_bswap4(x >> 32) | (((uint64_t)CRYPTO_bswap4(x)) << 32); +} + +static inline uint64_t CRYPTO_load_u64_be(const void *ptr) { + uint64_t ret; + OPENSSL_memcpy(&ret, ptr, sizeof(ret)); + return CRYPTO_bswap8(ret); +} + +static const uint64_t K512[80] = { + UINT64_C(0x428a2f98d728ae22), UINT64_C(0x7137449123ef65cd), + UINT64_C(0xb5c0fbcfec4d3b2f), UINT64_C(0xe9b5dba58189dbbc), + UINT64_C(0x3956c25bf348b538), UINT64_C(0x59f111f1b605d019), + UINT64_C(0x923f82a4af194f9b), UINT64_C(0xab1c5ed5da6d8118), + UINT64_C(0xd807aa98a3030242), UINT64_C(0x12835b0145706fbe), + UINT64_C(0x243185be4ee4b28c), UINT64_C(0x550c7dc3d5ffb4e2), + UINT64_C(0x72be5d74f27b896f), UINT64_C(0x80deb1fe3b1696b1), + UINT64_C(0x9bdc06a725c71235), UINT64_C(0xc19bf174cf692694), + UINT64_C(0xe49b69c19ef14ad2), UINT64_C(0xefbe4786384f25e3), + UINT64_C(0x0fc19dc68b8cd5b5), UINT64_C(0x240ca1cc77ac9c65), + UINT64_C(0x2de92c6f592b0275), UINT64_C(0x4a7484aa6ea6e483), + UINT64_C(0x5cb0a9dcbd41fbd4), UINT64_C(0x76f988da831153b5), + UINT64_C(0x983e5152ee66dfab), UINT64_C(0xa831c66d2db43210), + UINT64_C(0xb00327c898fb213f), UINT64_C(0xbf597fc7beef0ee4), + UINT64_C(0xc6e00bf33da88fc2), UINT64_C(0xd5a79147930aa725), + UINT64_C(0x06ca6351e003826f), UINT64_C(0x142929670a0e6e70), + UINT64_C(0x27b70a8546d22ffc), UINT64_C(0x2e1b21385c26c926), + UINT64_C(0x4d2c6dfc5ac42aed), UINT64_C(0x53380d139d95b3df), + UINT64_C(0x650a73548baf63de), UINT64_C(0x766a0abb3c77b2a8), + UINT64_C(0x81c2c92e47edaee6), UINT64_C(0x92722c851482353b), + UINT64_C(0xa2bfe8a14cf10364), UINT64_C(0xa81a664bbc423001), + UINT64_C(0xc24b8b70d0f89791), UINT64_C(0xc76c51a30654be30), + UINT64_C(0xd192e819d6ef5218), UINT64_C(0xd69906245565a910), + UINT64_C(0xf40e35855771202a), UINT64_C(0x106aa07032bbd1b8), + UINT64_C(0x19a4c116b8d2d0c8), UINT64_C(0x1e376c085141ab53), + UINT64_C(0x2748774cdf8eeb99), UINT64_C(0x34b0bcb5e19b48a8), + UINT64_C(0x391c0cb3c5c95a63), UINT64_C(0x4ed8aa4ae3418acb), + UINT64_C(0x5b9cca4f7763e373), UINT64_C(0x682e6ff3d6b2b8a3), + UINT64_C(0x748f82ee5defb2fc), UINT64_C(0x78a5636f43172f60), + UINT64_C(0x84c87814a1f0ab72), UINT64_C(0x8cc702081a6439ec), + UINT64_C(0x90befffa23631e28), UINT64_C(0xa4506cebde82bde9), + UINT64_C(0xbef9a3f7b2c67915), UINT64_C(0xc67178f2e372532b), + UINT64_C(0xca273eceea26619c), UINT64_C(0xd186b8c721c0c207), + UINT64_C(0xeada7dd6cde0eb1e), UINT64_C(0xf57d4f7fee6ed178), + UINT64_C(0x06f067aa72176fba), UINT64_C(0x0a637dc5a2c898a6), + UINT64_C(0x113f9804bef90dae), UINT64_C(0x1b710b35131c471b), + UINT64_C(0x28db77f523047d84), UINT64_C(0x32caab7b40c72493), + UINT64_C(0x3c9ebe0a15c9bebc), UINT64_C(0x431d67c49c100d4c), + UINT64_C(0x4cc5d4becb3e42b6), UINT64_C(0x597f299cfc657e2a), + UINT64_C(0x5fcb6fab3ad6faec), UINT64_C(0x6c44198c4a475817), +}; + +#ifndef ROTR +#define ROTR(x, s) (((x) >> s) | (x) << (64 - s)) +#endif + +#define Sigma0(x) (ROTR((x), 28) ^ ROTR((x), 34) ^ ROTR((x), 39)) +#define Sigma1(x) (ROTR((x), 14) ^ ROTR((x), 18) ^ ROTR((x), 41)) +#define sigma0(x) (ROTR((x), 1) ^ ROTR((x), 8) ^ ((x) >> 7)) +#define sigma1(x) (ROTR((x), 19) ^ ROTR((x), 61) ^ ((x) >> 6)) + +#define Ch(x, y, z) (((x) & (y)) ^ ((~(x)) & (z))) +#define Maj(x, y, z) (((x) & (y)) ^ ((x) & (z)) ^ ((y) & (z))) + +#define ROUND_00_15(i, a, b, c, d, e, f, g, h) \ + do { \ + T1 += h + Sigma1(e) + Ch(e, f, g) + K512[i]; \ + h = Sigma0(a) + Maj(a, b, c); \ + d += T1; \ + h += T1; \ + } while (0) + +#define ROUND_16_80(i, j, a, b, c, d, e, f, g, h, X) \ + do { \ + s0 = X[(j + 1) & 0x0f]; \ + s0 = sigma0(s0); \ + s1 = X[(j + 14) & 0x0f]; \ + s1 = sigma1(s1); \ + T1 = X[(j) & 0x0f] += s0 + s1 + X[(j + 9) & 0x0f]; \ + ROUND_00_15(i + j, a, b, c, d, e, f, g, h); \ + } while (0) + +static void sha512_block_data_order(uint64_t *state, const uint8_t *in, + size_t num) { + uint64_t a, b, c, d, e, f, g, h, s0, s1, T1; + uint64_t X[16]; + int i; + + while (num--) { + + a = state[0]; + b = state[1]; + c = state[2]; + d = state[3]; + e = state[4]; + f = state[5]; + g = state[6]; + h = state[7]; + + T1 = X[0] = CRYPTO_load_u64_be(in); + ROUND_00_15(0, a, b, c, d, e, f, g, h); + T1 = X[1] = CRYPTO_load_u64_be(in + 8); + ROUND_00_15(1, h, a, b, c, d, e, f, g); + T1 = X[2] = CRYPTO_load_u64_be(in + 2 * 8); + ROUND_00_15(2, g, h, a, b, c, d, e, f); + T1 = X[3] = CRYPTO_load_u64_be(in + 3 * 8); + ROUND_00_15(3, f, g, h, a, b, c, d, e); + T1 = X[4] = CRYPTO_load_u64_be(in + 4 * 8); + ROUND_00_15(4, e, f, g, h, a, b, c, d); + T1 = X[5] = CRYPTO_load_u64_be(in + 5 * 8); + ROUND_00_15(5, d, e, f, g, h, a, b, c); + T1 = X[6] = CRYPTO_load_u64_be(in + 6 * 8); + ROUND_00_15(6, c, d, e, f, g, h, a, b); + T1 = X[7] = CRYPTO_load_u64_be(in + 7 * 8); + ROUND_00_15(7, b, c, d, e, f, g, h, a); + T1 = X[8] = CRYPTO_load_u64_be(in + 8 * 8); + ROUND_00_15(8, a, b, c, d, e, f, g, h); + T1 = X[9] = CRYPTO_load_u64_be(in + 9 * 8); + ROUND_00_15(9, h, a, b, c, d, e, f, g); + T1 = X[10] = CRYPTO_load_u64_be(in + 10 * 8); + ROUND_00_15(10, g, h, a, b, c, d, e, f); + T1 = X[11] = CRYPTO_load_u64_be(in + 11 * 8); + ROUND_00_15(11, f, g, h, a, b, c, d, e); + T1 = X[12] = CRYPTO_load_u64_be(in + 12 * 8); + ROUND_00_15(12, e, f, g, h, a, b, c, d); + T1 = X[13] = CRYPTO_load_u64_be(in + 13 * 8); + ROUND_00_15(13, d, e, f, g, h, a, b, c); + T1 = X[14] = CRYPTO_load_u64_be(in + 14 * 8); + ROUND_00_15(14, c, d, e, f, g, h, a, b); + T1 = X[15] = CRYPTO_load_u64_be(in + 15 * 8); + ROUND_00_15(15, b, c, d, e, f, g, h, a); + + for (i = 16; i < 80; i += 16) { + ROUND_16_80(i, 0, a, b, c, d, e, f, g, h, X); + ROUND_16_80(i, 1, h, a, b, c, d, e, f, g, X); + ROUND_16_80(i, 2, g, h, a, b, c, d, e, f, X); + ROUND_16_80(i, 3, f, g, h, a, b, c, d, e, X); + ROUND_16_80(i, 4, e, f, g, h, a, b, c, d, X); + ROUND_16_80(i, 5, d, e, f, g, h, a, b, c, X); + ROUND_16_80(i, 6, c, d, e, f, g, h, a, b, X); + ROUND_16_80(i, 7, b, c, d, e, f, g, h, a, X); + ROUND_16_80(i, 8, a, b, c, d, e, f, g, h, X); + ROUND_16_80(i, 9, h, a, b, c, d, e, f, g, X); + ROUND_16_80(i, 10, g, h, a, b, c, d, e, f, X); + ROUND_16_80(i, 11, f, g, h, a, b, c, d, e, X); + ROUND_16_80(i, 12, e, f, g, h, a, b, c, d, X); + ROUND_16_80(i, 13, d, e, f, g, h, a, b, c, X); + ROUND_16_80(i, 14, c, d, e, f, g, h, a, b, X); + ROUND_16_80(i, 15, b, c, d, e, f, g, h, a, X); + } + + state[0] += a; + state[1] += b; + state[2] += c; + state[3] += d; + state[4] += e; + state[5] += f; + state[6] += g; + state[7] += h; + + in += 16 * 8; + } +} diff --git a/heapster-saw/examples/sha512.saw b/heapster-saw/examples/sha512.saw new file mode 100644 index 0000000000..4d47a1f014 --- /dev/null +++ b/heapster-saw/examples/sha512.saw @@ -0,0 +1,41 @@ +enable_experimental; +env <- heapster_init_env "SHA512" "sha512.bc"; + +// heapster_set_debug_level env 1; + +heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))"; +heapster_define_perm env "int8" " " "llvmptr 8" "exists x:bv 8.eq(llvmword(x))"; + +/* +heapster_assume_fun env "llvm.memcpy.p0i8.p0i8.i64" + "(len:bv 64). arg0:array(W,0,)), \ + \ arg1:array(W,0,)), \ + \ arg2:eq(llvmword(len)), arg3:true -o \ + \ arg0:array(W,0,)), \ + \ arg1:array(W,0,))" + "\\ (len : Vec 64 Bool) (x y : BVVec 64 len (Vec 64 Bool)) -> \ + \ returnM (BVVec 64 len (Vec 64 Bool) * BVVec 64 len (Vec 64 Bool)) (y, y)"; + +// heapster_assume_fun env "llvm.objectsize.i64.p0i8" "().empty -o empty" "returnM #() ()"; +// +// heapster_assume_fun env "__memcpy_chk" +// "(len:bv 64). arg0:byte_array, arg1:byte_array, arg2:eq(llvmword (len)) -o \ +// \ arg0:byte_array, arg1:byte_array" +// "\\ (len:Vec 64 Bool) (_ src : BVVec 64 len (Vec 8 Bool)) -> \ +// \ returnM (BVVec 64 len (Vec 8 Bool) * BVVec 64 len (Vec 8 Bool)) (src, src)"; +*/ + +heapster_assume_fun env "SIMPL1_CRYPTO_load_u64_be" + "(). arg0:ptr((W,0) |-> int64<>) -o \ + \ arg0:ptr((W,0) |-> int64<>), ret:int64<>" + "\\ (x : Vec 64 Bool) -> returnM (Vec 64 Bool * Vec 64 Bool) (x,x)"; + +heapster_typecheck_fun env "sha512_block_data_order_simpl1" + "(num:bv 64). arg0:array(W,0,<1,*8,fieldsh(int64<>)), \ + \ arg1:array(W,0,<2*num,*8,fieldsh(int64<>)), \ + \ arg2:eq(llvmword(num)) -o \ + \ arg0:array(W,0,<1,*8,fieldsh(int64<>)), \ + \ arg1:array(W,0,<2*num,*8,fieldsh(int64<>)), \ + \ arg2:true, ret:true"; + +heapster_export_coq env "sha512_gen.v"; \ No newline at end of file diff --git a/heapster-saw/examples/sha512_proofs.v b/heapster-saw/examples/sha512_proofs.v new file mode 100644 index 0000000000..77bfbfe7d8 --- /dev/null +++ b/heapster-saw/examples/sha512_proofs.v @@ -0,0 +1,20 @@ +From Coq Require Import Program.Basics. +From Coq Require Import Lists.List. +From Coq Require Import String. +From Coq Require Import Vectors.Vector. +From CryptolToCoq Require Import SAWCoreScaffolding. +From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors. +From CryptolToCoq Require Import SAWCoreBitvectors. + +From CryptolToCoq Require Import SAWCorePrelude. +From CryptolToCoq Require Import CompMExtra. + +Import SAWCorePrelude. + +Require Import Examples.sha512_gen. +Import SHA512. + +Lemma no_errors_sha512_block_data_order_simpl1 : + refinesFun sha512_block_data_order_simpl1 (fun _ _ _ => noErrorsSpec). +Proof. + unfold sha512_block_data_order_simpl1, sha512_block_data_order_simpl1__tuple_fun. From 61f7006c9293af427bb3f1cbffef63d33619bc95 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Mon, 22 Nov 2021 12:52:47 -0800 Subject: [PATCH 02/10] more progress on sha512 example --- heapster-saw/examples/sha512.bc | Bin 5360 -> 36496 bytes heapster-saw/examples/sha512.c | 86 +++++++++++++++++++++---- heapster-saw/examples/sha512.saw | 87 ++++++++++++++++++-------- heapster-saw/examples/sha512_proofs.v | 1 + 4 files changed, 135 insertions(+), 39 deletions(-) diff --git a/heapster-saw/examples/sha512.bc b/heapster-saw/examples/sha512.bc index 2efb943af02a8ab38c990978fb8ccfc6d7730ed6..9ddf7975f59d2d85182c1585b0540f94ee9e929b 100644 GIT binary patch literal 36496 zcmdtLd3aOR7B{>zhYo3gPC(kG1*FWOU@3Fb7N`Ompo}u4EiDB~32mVRgXv@|7ch8H z>lHK%daHs~K?DVFTBfQ+3syj6NTonQz@m%_@~ySkNtyt@&-4B9y?=Z>q)GO$_8NYB z?X}N3C;O~D$eY1Ge|Rll%b0>OQEZ(3?9)&HpINexuFGq$zxVE)6E80OVdwLIeSYod z5xwI@Q8K6t_hGCsf-!G#I1|J7KzJz%JFhd;N}rLdqXxYyD)H$mQ+5cI{wvuMJW?F{ zs(0)Gb(DXMGI)$vRC0NO`9OH*_;zKh)rMEab83~J_-o@vm21BiMJ1O6_lWFa?YF#Y z#yahxTA=%~ma#B+kBTU7qn%SKZQpro3H&)uy z8X2tYAs2h~(;PO`YDBTmhO=Z*d3SM@bz*tpR919RSv0}tTXDjGfaGa`mJdLRneR@0 zUB)7N%Bm7xjsICA3ijXhYwfp%Yn9V0-x4P%Ezh#?!Hi{!80&Pu+ueuoPh@6oA|-lB zjU~7&*Q&^mEL&_-EUhhzwwC2qDsr`DS=zE_ZCOrLSq^+oFU~JljUlJBA*ZV~Kn*F_LTU;_>syJK%W~5tODfBjTFRnrWoESk_{nE= zz$y$X;@#~bHPs;dKXxz9PbkYaa~;-$2xYkyPgEVN2|2sT7Zg<^3Uz>%8a0nGV^QSi zDHel5Dij6Evc*#sj-Zu|L5D;k$CE;vlR{RylrPeP@@tYb$GM8m7NVA#8$+5l`5xF5 zT34<4#t;fdIc5m^Mr4;*KrU-pcBG;py?C*utbjQ-X-*qLf3F5TgN;JJ+oWj*={A9h zL$9F1LoH7SE0&i_hM0=+gIy9mRg!Hl%eN|`rxq_wS1gC}iZZiakS0%V7l z{6mHFgH1B9T=)#A8wBm`ilMtD7C;?P&;i&a*`WFKGBeuCrS>b_;ujl3>Iy?o*)=B{ z(P}JPsaOi5u;|DdM75tqYSf3Y6;+}Rf5X=o*(qkV3_od6i>%CBujpirW$jF&4}41u zYe6iqE&Y%hzcLf|b1yaDQTiscoG zeE5)Fw$#qys#N6YoVazu81Y#Fu89K`KPU#9i({w|fQP7-EVmaAVdVwpvV5f?8>Z?L zoFv-}zDolW@N6}oS%o2IQSDB@XOa{uSy+blRgt6Ex3ry9^y#LlC0b>)x(*QvsAkWA z|CYlV(!R(Ps~xMAZ`M5}JuHpYw@WFq^=dDcw;uqLa>!lT5LepzM(%(85)qCls}s+YHD6}f8unHN$6aGOi@iUN}& zr(S*;{_?L2O{zSmC{Qc1EQ*B=Rh~_;*d%m>#tU`ci?xb8+f9o)yv>~2gmrE8olBD1 zUS_|ax?LL5u1Xp=0M~5zS1rD34U7ohyotUl15F9H#=`mxD;52-i+$cdz+x>-?JQx? zrmG@U!t}0^Di+scYORI^<4TVIlona=gm)zqnOnDBcIyYBUP@-+E%1*?^itxVW&_hn zg(5Zc)@@z&a)wxJ5=t1GY6*XBdV-4iI9ZY+OLuGDXC|f4NQ*4J+wq8u#W}l)fTa(9 zHbrTfvk^m<)+ly~L`G*L1}x1V(b12+(W38*( zJT>}|G|uZ#k*wdWl>CrO0|UowUXp$8m1o{;c;QA~_LOedMx1*-Z|2>zZ!fNYFZc6} zAww6Y41RIS(T^^KD=r6|9yemty*(%IO>aW1kU}; zukp}txh;WX%qOa&O!K0be1E^sw7`G^J084v>)>CD6aSSP@LT_P&dgf*ZRd}^jlOc5^#AN<<2?4{?=X*&G$`oTL--^dv_aqjYo?=&sGyZ+p{_kSLI zcudG|)9&^>-2cR#7{71Z23+Z|Gj-RZpAyfNuB&_D)^iJ9y*jVx_Jeh|FAVGb)85Ku z(^tnW89nWP!;b%*d1Tq7lzXM^gVTOEz4PznvS}D?fVNqydhHuVozWIQhoy zfV#xYkpqYBKiyP%d-C{QYaTA0vE-LKKRum0^Ap+39W5(PpBOW3fz^!vDU87oEvxKr;^ty`koI8 zIrG{Z&&b!F+o_p0I578(>ZDV-C$i%gWo4KWXD)pDsc{V%ot}ibhp@Z1+J z9z2m&Ju!6h3!2M$<9gIfEV_N?%-*1T{f60B zEID7b=h|xcm7zP_FS+kzvA$X!J1BCC*sbXzO{1K z0>$jhXZJq5GwH=!NB=tG`^V1Vqrd7mrhi&Wr{8inWc@sT<%=B-+?(RFbm*b;>!YWv z|6KCwgYhx%Jy`a6O43sk-;n*ByZu6zlk%Hv{6_OFiR(NuQDVxNo5@0wb5)1vC{6B`P# z90WXRIvHP`4uRee-9b(;@q|h|o%R}}S52=qEv{N#4Z}HF)$&k7h|D`6yvUJ73bXW}) z11%VUnN8rP6-)2RfNZX%Y&HaV!LX*3*2Gzz5s^EWj?~hp@7XvZc`u%-j(ECM08YDxi_WK;3S7x4CmSrx^Nmt~V z%5s9sa%^QCzMJTGo%#K4R5e*u=kb`j`PCfgp(V z&H@7o9fnjD58GMXsbqi5>bOC5`-kqX9#p#@WE@(TuyZlQfhNUbjF8JZ{Cr4t)#P{0 z0qdFH1)bjot>0~l zHm=;KLz}Fq1a0TS)$7(Bjkl>I=M3!^6}#3Nz9mv_GA)JnV>)+l^Qj`U-miRQudi(W z_ss(ynjHJvw~13Lt97tuOpG6+ot&DLJ#SHFd~Q-!n(Iqy@{+mQXEM_kIZJX=(vz}g zXU{80H9ixk9hFIt^eNy^P$_5gB7bfN89Xk(4=CyOj9Q0!dvToi>t}_U;#@ zgKvHMNA-#7-WQwCOG(NBcC-6VO<6Q2wNH}S+&6AfW=?8mPIljTWNVQ*HLI^NBPl0s zQP#rjzT=Woo}W0ik69>iYXic&s}8 zfY~{H(w(0&76GsP&yvjSd2=&U=V+nL7|_JTXT}-F_M43#|G(u_5D9qB&PmEi{r`5b ze^g71Q!DVnr3ysJ|3!YX^T9@fsSumU621RlWMW?bm}r5EKIyY(&q>P4otMd{%IuuS zfHE&LbIHP_(ZhfIi z-rpxhx1ric(ovnJ+i#Q~4E9N6heWJDlLY9+%sy11mwQJtg>JlLs#nNz*rCEdyH8=r z*r4Eva!HjuPnW7=^DT=0%6yxm{nM5XP=6A}VQg%F%HKM&fEUA$o{hE@M4X^?}|Mz(;=t-)=m{g zgUx{<^`efIl8)v+N$(d2?=I|QDH>c^JQzMyh=*1dcefS~wiR}2E?g~rDzbBQ^q0|Z z>>Bv#;9XHc{dZOE*fZWMI$bg_PZCpGy5`77M@q+DtxMgOx!&YEAt`0Yg6wBH_srhX zsq5Y1@L~~bG1Z!smZ8A)`w%bSe#F}=D-zaWMZr{aMcgo0POIVu)$cF5s5wLzY2cDi zct|r}-vS4mH>oZeVcGO+!o}0?l2LWD$^m_0Rjmbo0(QA zSC0A<_L6azaYNYze@4^=`)}3DcQH0N#aIz*@@8tagkKANL2ARxq5NNxma*NyY

9 zF9aaW0w!&+EA?&E{TkXTS-mJkBr_Z^j@B~0BCjFfAT+q4W6TKcNR|@NE@PqaqUCIM za>k;R1u%(ol4dW;nv;ra9?HpFvL$L2iLJ7w1r+wK74?kYvC0wHWC~n0ZKT;d%jkV@ zTf}bJpxvd(liM~IX->!X`%t;mpvnyQNedA5trhjr>{w+BYGOfar;W6GXIZ@uZ;QAq z8&q4Gau7m{dR0&PVz^RrQh(AAX^ZWd5g|2cEQ?<@d0REM*hneU^=X?C{%=X5UMAwo zP0zA;ZPzjT?)a+GajFT`D#n7}Q0}sSZRmmX^nAPOz`=tOWJ6$6IV0j^Q8&d04wxm) zL#_Ik)E%PQT?zEc5*fcRTD>jFrG?X(e~eFq*i@vJ&(Rsw#ZeVn@EZp0ccvn}ty)@` zP~4^_xDwn4x8c|W$EI!7wHM_CcCU+P8%M$<(t~NoO6#%s=#t}+KAqHM@vO64!HP^4 zo9G-`_`hi3die8DmtwTlXikb5G#l00tokfAd(Wd;Y!7NCYi(A@o4xDNOxzoqtq#^O zWs#^zo{x1_yxgXT*Tem*4ePvC_h$C;YLP`7tWCGv!O~{<<98GOAne|6aVL5wh2^n4(*Xp2CUD(e~4g+J)R&`(jl+92{i*qbqf_nZA9 z=M?$?fl)qQOj>P!xfnWHWfuaO>7>Oh76VsvM0F6xXgc^z)YWVJubu zrj9*_BG{D3olHD7nC+Jz@K@V`nfAa8`;GfI^Kt7?5{Mmi zWAsql&>NIwlSS>8vF26k)xfL4d#>4=>5`4;AHEAib@q+~z3i7ugVc7cuLV2wGW1I^ zHpHS@LiNDw^vEm`tMtL)H*j{sP&eMv3LSgNw_L{+Z_}|_U~~?%wvjl*BCfj{ACOwd z%6U&~2L`tF%x;crk*9;XPS@-N3BI)?fH;f2OQEKhAu7e_sHukHF*dN!Zu3nstM7;iv6t=- zVwPjJPVMDPzL<&I%k^>#Xl7V&Mz~*58;M1X-{wknNldMA=g-RdW3NiEK2gEIIDOQJ zuW0RctrldkTtN`AGaM#PRSe~-sOUPCi`B!6}FLRC8*p`p9>bRY9|c)qZ*r`L#zEuV)YEhFBKy)B4o&BkP^gz zIscxT8)++=!ZKFm1`cTtKztI+qoIJXUZMdw{tZ-{`be<<7seJbvv$u(0Xvi~41)N; zjQpUnN=@8YMZ78*G&)%XQ%cr19-wp6OA6BEZ9w#pkskujiCPz^I=w}n6w%;D1<7zm2GFV6C2^#S3L zWt^qjQo>IWpvF{M4U;nySsED=3C^JtjMAtBhao)xYZt6TxW4W3d7v%a|N5q`Tg^~H zYcXEEgSD8ia~SYQ{iV-zhId@gKmo#f7O%kQOxTLVO_*j(e13MuqNF*qm%uhAITh-J zHM%%1P-PM6OMID0#g_$faBa27Tf|n6k-ngm4ANhPK&(wsu(`c-v!s99F)pW`p;yX8 zf`9$=O>~SFT)Ow)gFk-#@RP)5OzbnY&j8D`q9Z01Zueb*$PMLoQF8!f( z?WVZI-0}ZyT=L(eKZ#j0tRx)^do#Tr219#18kaop#+#dc#4;$Kvt;4Ie0X=pOJSR2 zVWLOkB}ZrE3zzh*Sk9MKD2ph_w;l_TE_AapYDa#>B zd6Ew6AUbO=ZB~23#6bL0Z0B$2;2+!FKW>o!=yd_lEPgF<50Cal810o#OcZrY=O@v;jaOGcQ^yCtJ6?0apcmmD2j~5F@Xq7d9_1b3Bb%a@ z8q~_ze~M*O=A@?0P0!Y4_nV4(WiNCMfmqd|*(UE@CATwejhyKeO!uMEZcrt6{?8<7 zqgL_N__`iNW~-znGA+OmQ(KtlzhjkF(_|S6p{`n$WeSB*SE(4Je+5F_l44EeXb5#{ z462h`DtPznLif8u_vJ$O;X?N?>TVahHw)eG3f=#P?&5r_OsKm@LEGT1lo`S)W<`hUFDahjetNK zx(Ba=?l+4yt81xy0(O6>Rdf-$x5MrUwT73eyB)jh+GUx9?lIVXeTim+(A|jLyM-$v zh3@{?{n=W>Dq-}IIC{G*o6vnKcHdc|*(P+KirxE$D|!jt1F`$qTEoAD(XqR(eU>BQ z@TyHuH6-_*>=RubxUgTJwsz60#Xl-bafc<2nUhu3u~Lg3gDJ+Trfvz4qsMSmeQj7k zn*fm}W>C5>Z2~OCy=z;`GYzWg`)SkQuy|+HcU;Oiow6C$;^S2kq7VC+oiD+)0oZ)l zlY*LTPvZiy_+_Trt5s}If*mC+9Ohkx6>sC-+8lG!X;n%b{>JDlS~ST+3J0WZ$> z-6GBIL(_4T z%qQ$${$X4555?o<8z;g3XXe~Bu(cK45<6GPD8Kj7p<2*iwkTkUoWEBTgWmT>i(8vY zY;zy|GqqVS=4~3Uy0zhc_pY;zY(W*$5wyV!mx($ho$B5IdL*}^;c@7Eg!WJ}S5_2Pa_W@KGTge*aZe8Pe*PX3h z)7`taU{_sh*J}5!`_Dq9-^b3bjU9d51hwHVulQGNfx6v$2qIyKL_w3E^aD*=C9upz zM0YeZi}zC6Pl&yQE#6Yt^!uzj8EhA^v<@ZNumNQMQ9^`MH>#ZqE>MIwmpVgx+Cjl4 ztJCNh#-?GYn%=pM0z=jN6sq!_%4VPpTctIfHOvx)yS&fVl}K2QURjgWx?Nl>!|h_j zp|%jQYhb(R^>acE-!7hqnA(WZHpI%ce503fUa4TVS0ExixUfqj?mLUJAcT*^JrZo* zGDIR6PfIrkXfY z=@>7>4ty0y(Y9F33_A0K2-uDlboK(JU10J%W(Y_}E{X)9Ac)cW!=~|Qr|0>!3YUvftbK(b zR$V(E2s9V@L$gFV2KLLhs6itGPyyz`p$^z3EZ|$kqWs;kVSLHd&4*?2%~nu@96J8Gkud;OWv5dj(Rc#lGYkzCwtO>i=Sby5Z2Jr2dtz8UI z=*jnrrmmT=qYXa^115|3Hmi3bFm?p@WESrkzj!cadx6Vt7>ly+p#k1>%5Lc|ep?4# z8HX_Tb+Ko$BU$!<6XbHNMHy|2k(B;CCsLvZ2|8owr;sX?&cFHb5 zq8o?AG#7goJC|dl%q0gw;xi731)Rv^kZ6eDkf`H*_wl|?NbIJ|H#>R%Om`{8eFR9X z21v9d10+V~36NkT0TM0lkjU%;kfZT@sWqJq6rewoPwn@LSi9@gm$zG5?RF9 z5M=BcF_!1anC%>wz4{fDy^#jcIb|0hF_c3h-^HG#p3AXM@dzYtag+YRi98O8rp_D^ zr+D8pysr}y_sL7#<^6AaNI61)1YTPDI|U$d&Ain5)u z3y>JcA@P=rJ&S|Ov5ymUTQ~+GDSb94@;D@JcHxj{=6xR!Gr~n)BU}cDg=YxwztUYw zaiRc;^#F;nsQ`(Q`Obx77C_>6cSwBm6hPt|f`q+W|39LzwG$HPCB_SoXza!zae*Mw z3%mq}L}CwwMBNtHQri+qE#IPAJ|wlg;ZzID3gD19;DcVGCx?XfO;1Rq%Qz&SE(Xp2 zh~HQs_CF@+n{9*vOr*rjtfNK~d-T#(r7uB@6V1c@1(f+-pyv4=y# zk>P^GF=A{UGPd2DGuGhAm@SvfZul8xzd-|h?v!1C#4HYpeJ=JaEnJQ>oS+*dR&bO4 z#fdx)iTI~DByRJ*4~Q875>^fg?TftsQxdo3QJgA3q5>c>Jq;jn&PvYoj zr&?H62M!5`3L(*-L!x%$Bao1DNbKd1@Zp*-xb!4QU^}+P7h4b{=5mATMj#}9a_QU+ z5(&B3g1khEyRtUJ&8HB4mM`QK>W3pFe&&#{uW&))7hc^ndn-8dxTdEbpHt|b8y4df+` z@%|sVODSF|Kw<+xB7H7EVq}5fCA1{~iJR__xEKkLI7X1L4Nlq_hpnBEKrgXQfJF6R z4vEVIiJ{;nI3yB>AS4>LKu+FvlGNhY2x{3uY6<y;t7d7 z6w@wCDFH>@BVlWsp8$zNTpertS|PEV8`L%$A@P?>=WdW_F0;5Gam8I(MJosrD>()I zXoSQA4hh>@7bJcs#&VIdYkXMm7Ei`(54r5sp(uN}luyv%PT2)WlyFG2!89V@5Lt|v zePkQeE;$Gi0b*P@dU7I<*APPLNQ?HTyq@t(}lSFY$>0iGFb$62B58;=xNS<6a^TA#rj` z0zg88yqK$FP%T4i21K4Bx)%^dj&QBW?PQ`4O}c{cL5T&-60X%6CiPlAYmD^ z=-r9f+6f7MT|$7wrZF56*9a10!AlS%#vmk4Z!rQS%%qm-sFw4jmd~7OVNu;UBz6X% zmw1jt!u+8pBu)Rw_9A0 zxa+R0*mnpLTR8>obcDn+91^CTE=Wx9;*fY38Qbp985{en2V=H3xa@}cD0@E{_Yyxk zWfvgv9*4v@7kd^nl4WN&K{rTj5(LV!fu$s7{D5hN19ODsn( zkvJJ4;n*@2AhDCwvK-a2fH=D6R13@M$sti6gkE9_heYMao{(rJ&EG}M{}jMA|GTH= zg-caj9oKjZg2cz%pe@M=iP#4hj9iR!Der zNc4IMArZ(Kn|{?35+}IqqSYw-CwzdS;4g(mQ-H)S4v9rB_AF*3%N}roZjiXaA#t7) zc^nc4dU8lC=Y2N@ab^Ta+$1m2!uwxzmr}e>fW$U{gku3f0-kfAOI6wifW%$B+oh^m zy#W%x#PO?_rdcb}Qn0lX68ySEn2}$-ES$w5af2W+1H1%>M8hnEMAH@%K;kZ`;fbXb4a}6V$Wjda%}A2l7nK2en?8cfD?Hf5)HjLB);K&_wl~Y zSR%$7H=)`Aynm*Ll-~)Er~*h_&j3gqbV1?-K;oV|Br^H{BrXyp>eIUXcLBC`LV{nH z5Fl|QjYHxOg2Wu~5-Yfun2V5T-jWWG7)omSAF5>;ab$I>h5g>2L!w-RUSd9nMDQL@ zNF?}zsqM0-%0TmPcI5bf?)noTF&W#j?Ysp+;zw@K`fP;6hc2DFL8A67wjeLD-CbF~ z{78^E&MBC)5fa-uB-kYvB(jLH!N}M(Vr;1=W475`_QLN`_C`KH(K}Ar1xTFckl5p5 z&r;9j*x2b2NG#zd{go4W91=~vIV4Wh5)F$G5?8mF z0TNbH%VktcX9Z5hq92@UVNruPB({d4m&oFfFz)kefB#CFvD9u0@YjNhIBi8O4- zj_?))iHqEz`jrTYBQBl0K_cNdiwhD1IBU*3^)3=5E^!KuWeADyIV2o+T#%?C#u|~a zH6fg_1D=f8c5vAZ_fYnEG{7HD*#$^k%Wu=`N-CrT_`J#%_6b5kTUg6B63{0ExfcAyKPSVv!Y6d^uxVi7>6seodRYR8j+;fKJu#>o&c zZu72HFNvOquFJ6NbIKgpJ48TE&G9OO^y%*-kil+vcVPW>Zg@TD7xJ0S`}nPU5xhQV zeG&@rCf)y8=i-n(OVu`By`8F$xvEKk<_DY$`%5T*|BGCJ^!=U!*#6{JyXCSvtKpP$ zcyrEl3^HxGO)~P4T0s-@6fv!?rh7DR@>UN#ZdX;)O{tX+ksE6pkf!z4P9xpRTG6!y zRFYh60)&iQ>2w-C#gLC4QLoj&ZC5tD?P|jkAGqx*Vg%e!Xqlyo2yRMN{|geS>%yMp z0YzJ-4AR9-3V)6mt4WI>Sw|qL29Pv!ko1O|cn{g?UlE5g%LIN8ty$Dt4)d?xi&(2X z=u%Owj54IBlhF#*Cd!u0@Nv#i$7;xCvdz_$B>gfNF9k&decUAm6?=FY$5yoZDc+P_ zBT6{S*zZE`--BDAcN*{gXsR^bUt)8j#Tx9PL6|jsjgIE`{LZki4&5s~j`HDR>F)C12$v0!O4jS9H!Q;#+VmiBwrml}#R%%BfVD*2a$4$*1|?{d!kN zcPN3o2u3O!`oZ#YTjC48M7TM8-M3mSq7}!wN;FmeYcS-_|Jno{z@rrE891kvdf1b| z9Src(Fql~Xix!;{z*uz{ChLDp##;f4My$$XY}G+h=#UO*^&NuMySWsqeSs|E_%~Xl zzr!wdY5_`8ay{osyxz5F8HJoESXTD<*YJ)q=9m|_^y_bq$Fr>=kG z_i%&D-B-4No8kAo!yW(QigTlv1V}T&4n}M1C!Wk^;H1VAkv+7pkxD> zy&Eato@R!?)wdeJG*=1%NB#38Qu_A{=2IuMH_WF`XjT*qxpPNOt`??MCj0ou<6biae>9*7LVELz-w-|lXm z!8;}N;Un=i?q-(tTkS~6?>^uJy>KBojknC#f4ixVB+z&20DyNS`vxx(G7z##)K4md zg%K#`6UDlA71f}a<)9c;>V8nFzCQxVY*@wFOeZ#tM_p`I4j?(J(s5>OOrx0<=N?^q-YzJ9lqYD(cfZP;vag8}_uU@|z2|mB-~E{zfLm{KNslhh1m7LJcdq-> z5Q$Hlf6#KNQHW6>HM>THg#dB$Kzblz@b|=EDrfLAF=!v_Vo-aV3}JbXJN~x`TE_-> zx|xLGf->fzGLFtAWkf%sj2b=`Youx};VCM*+*(ApzSNH31e@Mzbw+%z=?n;(zZU`m zZY6yLJRAaxqTqM5N2&5pstot245mtWCqIo5wLewWuO@nVKfu&v9~>nMnme8bQ^!>SLyZDM zgM7`fy$%sZ`KWpvPNgBRhir>@8cuq#&qOzni7PMOST=y1UO(Q+TER!+k1;i0(7tE* zO8#j_ej8dUs5=~jGus<+Z_4j?yt)A96TfB7QAF4Ik~tlqc#J4kbTxuAw44IPpi&jX z89O+SaIzfPv<)IQZ6CYXv~DCh9VbxEnjc8c2QE479Weeq@L$5DJ{sNKeL?ZHE_Y`h zWrsQc3_e{o-~(*RI{wHhwJ8MGGKUvgyfdR6(0lCDeA36-pho}_e}f0mmGUz%mvq5D zGbv!k2P4b^UGqZ64uebT)eHzvC&I#`UhyB2KbC$-49@2a&Y>X+kGL4re@2F2bI}mZ zlL=Z)8ISnmj|64>gvz)gj5Ms1)99oO|BtwY&z@+NFrJF0yA_S*4*p9{uz4mQubXsm z64M|q%wrk%k&Pc2^zezj&+qHATom}G%JCmlpza`irvSAPcO{gk+uMY-f<7liu_ z_j2^CAoQ@$UFac@KP27SmbimFKAMBG`9jObh1cY}Iyn&yXdOjWwsl0WWd}~p#81hB z_GqWuW3fLG8k0MrWAD+4vU#~Kze&-^jA)Lh!r#yhoK}N&VXt{0gP!M#;+?c_@{xG_ zRR66Zt@x(z-_b759S7=$1^++3CkGnOVYI~}!8kGra13#z+8-7a3Am7Wt zC^8~mwE`YU{+Zak%-NhnZ0c9I*tG2+IqhGeoa=XyoTmmlA0EsEUZ`$fMbX0q%TDM7Xlh=rRb z<9T~&F_&5kQg^^9ypsq!FBg49{x~v+7+h~g2G?YgKW?vbF22Y9^4vSV=_(+=}>Wr9I6Fs_*jgT6epS3h);A zh-)q_!pF{_mDsvP#5Xz6n&nh^g(}y0RBon9%e10_fR(g14hRO7>pF+Qvx!<2+{xT_ zP%~cUxSwe{T&Ph%gjufn3m=gOw+$e#9Y{|8caqm~80DSw70Da#l9xSuj?gntgCPHv z(8E@{&_f_UOS(0Lp>CZZuU*7JUjJ?53duy(vxA(72DH{umHrQ+=P1RgS-DbxnAzp_ zO8!R-&51$Bep48wr@|S>a>vf@33{2Lf<1*S9I?>SweAKcP?2Jt|9t${o^dPa)nn?<9HIc9ggFb&|KXRo?aA3g{V(=vg|5+|*bX zdI;nXvdHD`atFEk5(l~Mjs1NUOGE0HI1vqK4W=r~A);430;i^N5Lu92b^zk}9rntN z#87z-`px&VX_T*Aev>XhWnChrtqcJ-V2(rW!p~BCPZ7Y^ypyGgMv7&)UMccb6Nc1Y zc6n}Jw8cKnl|iO!>@$o4#dx_X$Okxv1wYORoq*yxqG<00zp4WHm1A(V3YB_a#LBl4 zn_HJ6n{Vb2(0+8WX_+vX^tJ%ytbdl|Ouy!mlfvyc2$Sq*ba(zgkm8evc)IuJynt=( zTfC`t9H+z`w`~LUHlM|~a6R?r>)S^dI`8gc0lCr!HyA9E`;oglvH zBAZgEtfb1sQ|^`JKTyxKHrGMv6X1VJl*>S3|sXNc~e_^{vZ!`-1>-6 zj%dem30!STILLeR^=$^W}z}{IvT0|*GH6* z%Ez)rxk;E#Mg3cg_-e(r=OaPOaT<^BKii_8IgI;H@R3=evcE1 z7O$-R&Z9DqD(l)^1+3`C*dZ8{y{vf%PnSwpz`ksKt-+5$ly*e&Z@<5X!JK=xN!bRr z82~tN$%aehv)Uk{ST+6{#~*lJMD6N+C+h&>*zPPUZGJ6hI=~p+8;?T zcb9`3u=}ER;eoep6ajSk6+5w4X{0u^UdJJLHd_9Zr+xGH38> zVo>+M#bCk(GK6g<7=nGWoKK~qhDZEy(LGYeHm-~){)pdh+pR~Gk-^8(N4Gu!Xvw0Y znARe?-2V$F$ZpVheE;e3l-;4>v?+VXxnuv0M%iiebnMo1q!+V6)S5FWulJ+y;3n_XRbJ@1F^!Okp1b*i@lTPT*VBz+G z4WQJIiA}9S2H`ej=y2W!HMg=E{};)bXGA$OMi5f{ygc`mmsgT|*ZJdGca{{deyPUe z`l)#W1GYv)l)Xox?=h1%bFZ`zoQw1emAihg3i--dxOmwd*KcmIi? zFCy=5Qah!N=?qd^juYWR7z_OI(Z9(b|0E1Cm@{~v7&Mi+7_9%B3}KH0L$E6k30nD) zo)tiLoI6y79`9Fy~^{ZRygQ81wa_#8@%OTR)x~pSUm7xa8Fj;zRG&1|fRV74#!a z_RXFkulMufp;h{5H;^m)(L=>>$;D=RMLg7nXh5q_mF`3I?r*XHNM74S5HtEa!%$1T zz)++Y#<3k~l;+WmV4~K?p|t}^FOFBl;09cYu}EQ$&O0Tj_(;ygSX_8l*?NDc=XNH> zRI=CouaCzl@X3iWq6mpGe5!sqC6c#7Ffy? zV^v!`5@Qq1W5T)At%)%r>`aUWm13~W29G8NQ#pf|i9vfW7lYcRWC+XaXo#k@1g&Ee zJpFM(sGy8@Q5i?KkTP~XqKq0o7HgzxF5xLEy4+eMB*wxx!KPREc#q#H(>$6U7Qe}@ zq>t#%BWh=2>=~;3lPbeKDubyK5@UcB*dZiBF!)?kWE)J3l|o`{q>vbkJo#SB>oDgE zBMv{)nizYP@L%4Aib16+o`uBNyM&Yb$fj)%v1xn9#in&8$?13=<*XS)az1d$DI~_;AWZ5L(cRq_ z6kqOgckYR?|6o(raU7>ai7{RTiLpcn^d38ro9)rWSh^QajGY`Oa!-uC@7NOSlA01@ zMA(@aTR{F;`W7)bpEEdzhA3R)Vo?7X8G?;QLo`Pdw3;d(@yD5hGRE_@P8exe52w+E z#Ms+h!e^gvl`x))rn?nUVr&^F*gTAn_k_gQ+p&5E=zjmdXeG-p7*?OvOZOJ~kt z6jj;U2Jl6@WeZNt#LZ+ud!p0rvDop1#^fI8*n9Ng{>L`OI7 zl@uOC@lM(fd?aULY*cAZK;0yl=N1xU9Rp5Iik!rMKIMstF`@{GF zJ;$5I|Cdvu#26I?ZP;dq-e;)yqlvLW0X#8g`#|iT7<-{QwbXSniV|Z)*qIm`9>9a{ z$V6gr{WfH9%?F%8@xNURTE5sLO1!a87*SZf#8Pg|wDkEVs zAFIoUtrAvJ(E+!jwdhZ^GdMx@Za&@<5@SwJ||3n6R#MS4@lrLSigHNQ`}8`aJdUoWack zgSTA_vNPKWz4y64-b>K3{_hcgyh2dMi+rtHBq-x!Pi53M^Rd!%S|zkzCZXMmH2n6S z_c=jZ10U}RiLtA+2yguYt;9Z1 z)*JR^J%z;B%<9#$zXIS|NWh@!;?~62N95#plDupU%3HgXNgN*9*9dQAmt^L@qZv&<*73*&O6>$>le%rM>o6IT4MCF{-j0B6`&iacUaxkp)?j z%k3#w5JTlv=r`a0m_`{M=;7E|)@)MR%3k0GT#2#&Q3UWc?__DBk%Yw9y?_bRw5hJ2 z`*J46rkGM2%lKuPCnm;-A|%Fo!-6cW5o2O3V9*RPD=#57w|;o8)5CGGQv| zt*1AJ+g{$Zb4_*0N#S--AYaqjx9INt_mkq2r+K<}N{n^lO|8D15+%ko)Z6@>7!zaE z`?18>RGt_Ub@X;mjJ+$%4SXaqrXm)diLt5NAKUuT5XSG2!NfzvV4aIW7MntbXhuWm z=l9}4hj!y5{`j<@j3KBDwMJ0JTu)_a2lKJiA#M^5A)(!hgv1yps4w8-(f-pTF=h;; zD_^g0D>WS^zJBqAE07q2U@&>)+Sf5LHUsu$Q-#FX;i7Tg zeQ?h8%GwJ#9A{!Im7ILSG&25kD6h408pv>FMAGT#2y_6aloGi>$GicW};~iLqWypXpBU^~yalw!?lxJVy9g>L(<|Hgbxv z?VX7W^4l^@jP=U0gHneOo3#s&%>q6mB*t89vae}$@mDCPwt(cUKjD&-!tJ|+Nw$-( zb?=bkOLlp>cOfyxo7(=(DG7`(o51=7zySP7oj~G1J%HaAR$PnfixIdoGp=HQ?)F1C85S`^luM(8;^CQYg zL2GDz&)KBP7O7kZz~Xa07YlPJ$#P#(JOJZ9VHkG$h8TigjE_^!|ra zQ~xemknMH3J#B-)&{_1GTTjs_1v5Myd+leWm%F>c4Y(3x8Q%PwX_ud|6ML0Lawf)J zNXRzSxzY&E#Mr{ZBeJL>nRdMg|{CAI+;t!YnF^X)O{GW1JwnLE}9k zF*buXMIrpxEY%gnw=*$Dm9|h`S^uU- zj@|kW>BXE6Zov64O}R0M!h;6hsmm2Uk~1;(h4l~d*L=NlPmEm=fA4*%55Ft}8I;Eo zV~IpDt<3>kkf(uSP^kt`>c_;U_7bugd7Rj6Ze=t6SCTVt7Rs41laTtoOHK;6FMmPq zy^6cLS)_RNZBO?uB*wnvj=P2^QDTf2If}jv!b<>Iy!T^?vFousF?MC9M`En+-F=TH z#)z;pF?OB&@lV1KUvLJO6N9EZE(YtrB171hp+CNoOVG;i>lt+T|4z!d%at)|7AfQ0 zBg)vgmrM8@Ra0V&iYBxc35hXIkj>BM<2@lUwwD&+9{i_bZ570~GchJq_U4t^4IY)v zR0)YO_@!Y;j17XgrB7BJPmIAy5;r1b!x-DMw|)&iakd+tIP-DL5>5fJfULI?0ww1SvKBi? z47W#i9v{QlYy0@m7LQs5tyIdwzl5L*PRlvaM)Am5Amvy2fcnT29nlNCkYry0u z3|P+xH1GlU@d1mR13qvKnEr$Tukit&<`SOa1I`x)Y<3N}`3VDp+Cai2KHvpDV2yLY zhpquLo-p8bKHxwu;W<8FrZ8Z+!>Q6=o-kkwAFz-QxaKQVsd%)Y(l)}cO81L2KR#gX z&C*f;!Qi42{;2AN+1yUb2B&MlN1UVO@Vn7)vP51NrofXWWDL*da0Ko0Ng13l;FHwd zKN>!017+cGrdNM>_f~1uFBMr!WeT-2&aktlNTMv+q)kk!7D;Q2>ivdk=E;Xs+rNW4Lo40)!Q7r4AR!YVPD_)KC{vpQC|C#owGk*;3m0-~aE6+zBFd4+s z8h!BSwsP+%ts0KeR&^O4_}=2s$XB2G=8GP>saD`YeQ5l0@0iDH$9{{a#nD+YMtFCg z6(fSra8?XIFCq{=3+JB6+QH{19T4L@lVrJ7wwwjKpW$XH)Ho!)gyYA2nzUhf0stHl zlhIyUB!M$XJkE%bI)D9s^K1Ak?`Hg^_+sIV7}@aCaB_;hoX+6t$d44^XOvVxBRo>1 zNs{8ttks{w<+kAoa0JPKUijR(qRw@SNRMZgtKc`n!|)W52wVxSO48tLpkyPS6*VOQ zF!GlTjvv9NbFS{E!{fvt?+e1&acFxveD{uiT#vnefC~7Rq-E>_cyBL_=V$In;Ini! zvknj&@gvvgQ}E99*)CrGoleT0H;#O6;>5AD7p5*uG3U?8&dJV7$%Hmeoo2VlvRicu zr#$qjtsVrYJm`a(9GbUB@&gZ<4LYz4ZC+uJX;VOSTXDTNoas<2d%-Hnc9i0w39)@n z7ilUay_9$sLzXD0$*!56#4TZ|mKuC&OhtM)P(`o@ozM1(>wGp?{%x+)Tuk%>{@egp zLG^g(%SD@f4?f9VVr^}vM(asDn^h@zvv^BuGltFRzyKFDvlldjTU{Wg%emux|!cM2LXwto`*O1xG9hn-yvIDl&^+yvJif63qzRUDqZRgFGr z2R?=#QZ$2E;PFF?1*S9Nf*+y8eL^qz?mbGZEGdj!EqP{r>AVe!Ra;;FV4L^1JJ#?|a|<0+S7aX@!CF8w0bFf(jagYT)4HM$NILkW-Bzza)iT zZ47M*56ch*k)rM~c4nD@!qxk+YN)m->2fZcy9KBJXzYVli2(QcUuj|~j26%9LS zzyXqRL^|jXZkG3P9wC$v-3pTn0-A2N;1NRH{*^d?;StKYKC24qGej(^8F0W0O$YdI zR1C$R(!65$M8;|v{<6CdUZ}WLkLO8s$N|%><|hCYj+Q|>aoAowdr7Xx7DgN*s2BW9 zMMGR9%=!&&ufmV>`X#}yPk3Ln|H5n3O29S-=vc-*Y>yjwhwxPO%M5MKP`I)xW%T5X!!BFk;H zsXV~ao3W}(pyD7qi?NLKHJvHyv)tYX#j?u_gYuHvhqHZfm`lkFwPcW4F-yrza9~O( z*qaVEX&Wrj(WxRz1=^d=K6D-#b-e|>hd&<7mZ#_v1ScL!z}~q=IFv6P&&Ru=N`#px ztA#V%eluMVTr`YR=n!}V({ypS>nrSPtX_mean zQ^9*j_#O%Gcs8mxyzrm19zSDy{HKF9=qLQ(g|dTbAF?it#Y1^p_#Oc-Y>VYeaFUat zJPf`^!7EfK$M!i;j$<0()xlY=Wo#{!qwkpqFA&K^|1Bs-S(d;HV>Rcvo1i=xz8AnN z$XTw1fM1}$4$7SLk)I!+9QnpI8)F+zM+*ngLOIH`7hWp2@>@`j-@kzu^5twV0R`jt z6Yz5KsRX&yP>$oBhZpjN?Qz`hP>yu|f|om;fl!Y9@gM4)(}(vsC`UQ53=QlohmUL~ zba)Nk!Pb>n=XRtx9xMKYBX=`0mM-iwCwXq4IjL}9dRFTH`4roKJQvXYusnV^-9OOb z!%=k8$E=$dLx1K)4|qJ1^o)hvy=Ba7AwZg)lD>dbT$DUNH6;g6?(PG$I8pZw1L#cn zyqM_O(F1zJk?$F)y%#2>EXvO7r|Z-2=|0iUqv(ahdOZ#$p8cqbX8(h1&d&d+Bu}zj rP5(&i9~CwGaZSzkRF$&@t@$rd1PBrz%>yWamCU z#&)H9pYQqo&bjBDd+)hUTvV;?*8eG0m;=~M*jG$rdWY&AcFesi-_)RTznSBnCJs}r z&fJvkI6U@Rap-W&Tvb_>u)jXjIwss$M4hw3x~`+NF-zzeW|O7UF&ys3CK9H6?`S+H zHti)x%3y$%rNDWZXx0ghvV-_^eYb2!Vp8Kx1A7T#?6-Q(1K*z+6WlLnqg8-rGr$6V zi@(}+{}DE(53(v}UCcvO#YAmXkoK8I2+IIGi98m0#;D&dcm-}!+^N&50Fu1+t&m|Z zF)|3JdmhXsve(cq$~Rh``S59?V#Awr$T0O)Pb`|iyvfl4axS_*0!G{-oeIx$k;&iU zdMyG9b=Vy{#)-w?O~kWy9$H}Q&ooGVS6rw0GoSf%ohqMd_A%bAQcXhgd3~vIRhm#Y zmF>>@jkY(F^HiPi7{Kh5K9@;8PqLHWHyls?E>8@h%`#n{JqiV7x*yu3YgU{&qHE># zEzFb+!8C^hFan%)T+guY^XhVslfNb06uq9B>rik@()g_)s>S*+e*|!Azp#R(Mh0uj zlk2yCqCG{m#TWgHjsB>kt$p_RK=*59m)rLY*xPgV|D^bmO|JU;Tz`N9Hsk&Q%jM#V z@x#jW$+A5IQ^ggl$p%yC;2$vcM%GtN(3%>%>AQYb7XDhG8CEg(FkvewD?PNBXm*na z_!D;2S#Q>v@2`1=Mb<4Qe^nrC1kBH7$UY`CFc=u@?C$M7*%LTo@9yp$ygXf>qn6(D z+0+C)m9Pr_XASd_j~Zr2C4G&(va29sJ=Wn{s#1Mpc}X7sHhWV3k;{Hr_qpU85^?&f zd@+sFe@OL1?KfoY49VH^#(~6e%X2G`2awXzLza?N1bzP!6BJ4?Dj_w=%`C`y2UExZ z@HeZ+G04>8bb=5~oW#&;5_V~PxCwk!*on0FnS`q-tm=aw6s6ol%^6LYa;W-qT|)Nb zKIJ&iMBu()@&=4H_&LOzVzoZ?*X|DC39oQluSDJ+4n+a(=G*kE(tF+jgio9$+8((Z zm!`ry(uW7v-AplN(1?2tpJsBe-7ElDJ}pFeo1>%rg2lAV$hYON9{!k{V&pr1(1S77 z_+z2*L)Inl)VaUzB3H8J1~DS1VJ?}N^RoBKr$wXTn_0V;JZ$J0cec}zrtmx54)yd`o|9|%k~;x#o%4J^QX^?5ESQDDzftJdIMn?Gheu+& zuj3NY0-7THmZ@{pK;~aKY?wQhE@VrW_+ z8n_W^GL6PZTsAF8O@fmfHk$@eopl7DRZ!LsN;M3F_E)HE*|->E`XXTDQZtM}!-@e| z$|vZ;(=l|ZUEWJ5^j~c9p<0Iz-6REzahHqJ zlwg6S;S}o7HeXCa&q}x&v`|@0v*lJ$I;MCv%PwG&f|CEZ2J%y$M zFQfe~@-YMa6RbbXQHu8!r0^p~iuhI-44~Y}-LP0+1(?@h+J2gjU@}?-j8UWVhLpW1 zq#yZ z+^`j-Jh!M-4hZs&XE4pJ64eVzyplbWmTp^57=eG<*uiz%14KD^O$4D&NQ)L^OiwY3 zXOyw8zi2P8pnr$IDtwlHJ5X4DfEE=92msIE*T}k*(n}vJQ+9NfzC^U_(g#8*yZU*2 z7XdyNlV_~Op}xWX{?0*Iuc`Z&Ghp7Rsp~b4G6CyX2CGA*+D9k*bU(8MOW6#MwMgRH zWHl_HhmfhcRH9ju%)zPa~l1grK}myTG9*r7@5-l{4oRpc5&WX2@4xIE6tg zihfAGG+Gp*e6}}1Xd1M?*R-OGO{7p zRj;o>ZSTcy*^q+(Rd5?86gadEpbE6Th<@W+K>hxlN&d3HMuNdtdiHj-eP?e+XL~Tv k-fYDqpkXGwa`RVA+$l;j`%f5uUT^6zs+XzRc2KlIn&hyVZp diff --git a/heapster-saw/examples/sha512.c b/heapster-saw/examples/sha512.c index f60c585e1e..a2817cecea 100644 --- a/heapster-saw/examples/sha512.c +++ b/heapster-saw/examples/sha512.c @@ -10,40 +10,91 @@ static inline uint64_t SIMPL1_CRYPTO_load_u64_be(const void *ptr) { return ret; } -#define SIMPL1_ROUND_00_01(i, a) \ - do { \ - T1 += a; \ - a += T1; \ - } while (0) +static const uint64_t SIMPL1_K512[80] = { + UINT64_C(0x428a2f98d728ae22), UINT64_C(0x7137449123ef65cd), + UINT64_C(0xb5c0fbcfec4d3b2f), UINT64_C(0xe9b5dba58189dbbc), + UINT64_C(0x3956c25bf348b538), UINT64_C(0x59f111f1b605d019), + UINT64_C(0x923f82a4af194f9b), UINT64_C(0xab1c5ed5da6d8118), + UINT64_C(0xd807aa98a3030242), UINT64_C(0x12835b0145706fbe), + UINT64_C(0x243185be4ee4b28c), UINT64_C(0x550c7dc3d5ffb4e2), + UINT64_C(0x72be5d74f27b896f), UINT64_C(0x80deb1fe3b1696b1), + UINT64_C(0x9bdc06a725c71235), UINT64_C(0xc19bf174cf692694), + UINT64_C(0xe49b69c19ef14ad2), UINT64_C(0xefbe4786384f25e3), + UINT64_C(0x0fc19dc68b8cd5b5), UINT64_C(0x240ca1cc77ac9c65), + UINT64_C(0x2de92c6f592b0275), UINT64_C(0x4a7484aa6ea6e483), + UINT64_C(0x5cb0a9dcbd41fbd4), UINT64_C(0x76f988da831153b5), + UINT64_C(0x983e5152ee66dfab), UINT64_C(0xa831c66d2db43210), + UINT64_C(0xb00327c898fb213f), UINT64_C(0xbf597fc7beef0ee4), + UINT64_C(0xc6e00bf33da88fc2), UINT64_C(0xd5a79147930aa725), + UINT64_C(0x06ca6351e003826f), UINT64_C(0x142929670a0e6e70), + UINT64_C(0x27b70a8546d22ffc), UINT64_C(0x2e1b21385c26c926), + UINT64_C(0x4d2c6dfc5ac42aed), UINT64_C(0x53380d139d95b3df), + UINT64_C(0x650a73548baf63de), UINT64_C(0x766a0abb3c77b2a8), + UINT64_C(0x81c2c92e47edaee6), UINT64_C(0x92722c851482353b), + UINT64_C(0xa2bfe8a14cf10364), UINT64_C(0xa81a664bbc423001), + UINT64_C(0xc24b8b70d0f89791), UINT64_C(0xc76c51a30654be30), + UINT64_C(0xd192e819d6ef5218), UINT64_C(0xd69906245565a910), + UINT64_C(0xf40e35855771202a), UINT64_C(0x106aa07032bbd1b8), + UINT64_C(0x19a4c116b8d2d0c8), UINT64_C(0x1e376c085141ab53), + UINT64_C(0x2748774cdf8eeb99), UINT64_C(0x34b0bcb5e19b48a8), + UINT64_C(0x391c0cb3c5c95a63), UINT64_C(0x4ed8aa4ae3418acb), + UINT64_C(0x5b9cca4f7763e373), UINT64_C(0x682e6ff3d6b2b8a3), + UINT64_C(0x748f82ee5defb2fc), UINT64_C(0x78a5636f43172f60), + UINT64_C(0x84c87814a1f0ab72), UINT64_C(0x8cc702081a6439ec), + UINT64_C(0x90befffa23631e28), UINT64_C(0xa4506cebde82bde9), + UINT64_C(0xbef9a3f7b2c67915), UINT64_C(0xc67178f2e372532b), + UINT64_C(0xca273eceea26619c), UINT64_C(0xd186b8c721c0c207), + UINT64_C(0xeada7dd6cde0eb1e), UINT64_C(0xf57d4f7fee6ed178), + UINT64_C(0x06f067aa72176fba), UINT64_C(0x0a637dc5a2c898a6), + UINT64_C(0x113f9804bef90dae), UINT64_C(0x1b710b35131c471b), + UINT64_C(0x28db77f523047d84), UINT64_C(0x32caab7b40c72493), + UINT64_C(0x3c9ebe0a15c9bebc), UINT64_C(0x431d67c49c100d4c), + UINT64_C(0x4cc5d4becb3e42b6), UINT64_C(0x597f299cfc657e2a), + UINT64_C(0x5fcb6fab3ad6faec), UINT64_C(0x6c44198c4a475817), +}; -#define SIMPL1_ROUND_02_10(i, j, a) \ +#define SIMPL1_ROUND_00_01(i, a, b) \ do { \ - T1 += a; \ + T1 += a + SIMPL1_K512[i]; \ a += T1; \ + b += T1; \ } while (0) -void sha512_block_data_order_simpl1(uint64_t *state, const uint8_t *in, size_t num) { - uint64_t a, T1; +#define SIMPL1_ROUND_02_10(i, j, a, b) \ + do { \ + SIMPL1_ROUND_00_01(i + j, a, b); \ + } while (0) + +void simpl1_return_state(uint64_t *state) { + +} + +uint64_t sha512_block_data_order_simpl1(uint64_t *state, const uint8_t *in, size_t num) { + uint64_t a, b, T1; int i; while (num--) { a = state[0]; + b = state[1]; + simpl1_return_state(state); T1 = SIMPL1_CRYPTO_load_u64_be(in); - SIMPL1_ROUND_00_01(0, a); + SIMPL1_ROUND_00_01(0, a, b); T1 = SIMPL1_CRYPTO_load_u64_be(in + 8); - SIMPL1_ROUND_00_01(1, a); + SIMPL1_ROUND_00_01(1, a, b); for (i = 2; i < 10; i += 2) { - SIMPL1_ROUND_02_10(i, 0, a); - SIMPL1_ROUND_02_10(i, 1, a); + SIMPL1_ROUND_02_10(i, 0, a, b); + SIMPL1_ROUND_02_10(i, 1, a, b); } state[0] += a; + state[1] += b; in += 2 * 8; } + return a; } // sha512_block_data_order @@ -145,6 +196,10 @@ static const uint64_t K512[80] = { ROUND_00_15(i + j, a, b, c, d, e, f, g, h); \ } while (0) +void return_state(uint64_t *state) { + +} + static void sha512_block_data_order(uint64_t *state, const uint8_t *in, size_t num) { uint64_t a, b, c, d, e, f, g, h, s0, s1, T1; @@ -161,6 +216,7 @@ static void sha512_block_data_order(uint64_t *state, const uint8_t *in, f = state[5]; g = state[6]; h = state[7]; + return_state(state); T1 = X[0] = CRYPTO_load_u64_be(in); ROUND_00_15(0, a, b, c, d, e, f, g, h); @@ -226,3 +282,7 @@ static void sha512_block_data_order(uint64_t *state, const uint8_t *in, in += 16 * 8; } } + +void dummy(uint64_t *state, const uint8_t *in, size_t num) { + sha512_block_data_order(state, in, num); +} diff --git a/heapster-saw/examples/sha512.saw b/heapster-saw/examples/sha512.saw index 4d47a1f014..84a6d1f9e8 100644 --- a/heapster-saw/examples/sha512.saw +++ b/heapster-saw/examples/sha512.saw @@ -1,41 +1,76 @@ enable_experimental; env <- heapster_init_env "SHA512" "sha512.bc"; -// heapster_set_debug_level env 1; +heapster_set_debug_level env 1; 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))"; -/* heapster_assume_fun env "llvm.memcpy.p0i8.p0i8.i64" - "(len:bv 64). arg0:array(W,0,)), \ - \ arg1:array(W,0,)), \ - \ arg2:eq(llvmword(len)), arg3:true -o \ - \ arg0:array(W,0,)), \ - \ arg1:array(W,0,))" - "\\ (len : Vec 64 Bool) (x y : BVVec 64 len (Vec 64 Bool)) -> \ - \ returnM (BVVec 64 len (Vec 64 Bool) * BVVec 64 len (Vec 64 Bool)) (y, y)"; - -// heapster_assume_fun env "llvm.objectsize.i64.p0i8" "().empty -o empty" "returnM #() ()"; -// -// heapster_assume_fun env "__memcpy_chk" -// "(len:bv 64). arg0:byte_array, arg1:byte_array, arg2:eq(llvmword (len)) -o \ -// \ arg0:byte_array, arg1:byte_array" -// "\\ (len:Vec 64 Bool) (_ src : BVVec 64 len (Vec 8 Bool)) -> \ -// \ returnM (BVVec 64 len (Vec 8 Bool) * BVVec 64 len (Vec 8 Bool)) (src, src)"; -*/ + "(rw:rwmodality, l1:lifetime, l2:lifetime, sh:llvmshape 64, \ + \ b:llvmblock 64, len:bv 64). \ + \ arg0:[l1]memblock(W,0,len,sh), arg1:[l2]memblock(rw,0,len,eqsh(b)), \ + \ arg2:eq(llvmword(len)) -o \ + \ arg0:[l1]memblock(W,0,len,eqsh(b)), arg1:[l2]memblock(rw,0,len,eqsh(b))" + "\\ (X:sort 0) (len:Vec 64 Bool) (x:X) (_:#()) -> returnM (#() * #()) ((),())"; -heapster_assume_fun env "SIMPL1_CRYPTO_load_u64_be" - "(). arg0:ptr((W,0) |-> int64<>) -o \ - \ arg0:ptr((W,0) |-> int64<>), ret:int64<>" - "\\ (x : Vec 64 Bool) -> returnM (Vec 64 Bool * Vec 64 Bool) (x,x)"; +/* +heapster_typecheck_fun env "SIMPL1_CRYPTO_load_u64_be" + "(). arg0:ptr((R,0) |-> int64<>) -o \ + \ arg0:ptr((R,0) |-> int64<>), ret:int64<>"; + +heapster_typecheck_fun env "simpl1_return_state" + "(). arg0:array(W,0,<2,*8,fieldsh(int64<>)) -o \ + \ arg0:array(W,0,<2,*8,fieldsh(int64<>))"; heapster_typecheck_fun env "sha512_block_data_order_simpl1" - "(num:bv 64). arg0:array(W,0,<1,*8,fieldsh(int64<>)), \ - \ arg1:array(W,0,<2*num,*8,fieldsh(int64<>)), \ + "(num:bv 64). arg0:array(W,0,<2,*8,fieldsh(int64<>)), \ + \ arg1:array(R,0,<2*num,*8,fieldsh(int64<>)), \ \ arg2:eq(llvmword(num)) -o \ - \ arg0:array(W,0,<1,*8,fieldsh(int64<>)), \ - \ arg1:array(W,0,<2*num,*8,fieldsh(int64<>)), \ + \ arg0:array(W,0,<2,*8,fieldsh(int64<>)), \ + \ arg1:array(R,0,<2*num,*8,fieldsh(int64<>)), \ \ arg2:true, ret:true"; +// arg0:array(W,0,<1,*8,fieldsh(int64<>)) +*/ + +/* +// A copy of the permissions for memcpy +heapster_assume_fun env "OPENSSL_memcpy" + "(rw:rwmodality, l1:lifetime, l2:lifetime, sh:llvmshape 64, \ + \ b:llvmblock 64, len:bv 64). \ + \ arg0:[l1]memblock(W,0,len,sh), arg1:[l2]memblock(rw,0,len,eqsh(b)), \ + \ arg2:eq(llvmword(len)) -o \ + \ arg0:[l1]memblock(W,0,len,eqsh(b)), arg1:[l2]memblock(rw,0,len,eqsh(b))" + "\\ (X:sort 0) (len:Vec 64 Bool) (x:X) (_:#()) -> returnM (#() * #()) ((),())"; + +heapster_typecheck_fun env "CRYPTO_bswap4" + "(). arg0:int32<> -o arg0:int32<>, ret:int32<>"; + +heapster_typecheck_fun env "CRYPTO_bswap8" + "(). arg0:int64<> -o arg0:int64<>, ret:int64<>"; + +heapster_typecheck_fun env "CRYPTO_load_u64_be" + "(). arg0:ptr((R,0) |-> int64<>) -o \ + \ arg0:ptr((R,0) |-> int64<>), ret:int64<>"; +*/ + +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<>))"; + +heapster_typecheck_fun env "sha512_block_data_order" + "(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"; \ No newline at end of file diff --git a/heapster-saw/examples/sha512_proofs.v b/heapster-saw/examples/sha512_proofs.v index 77bfbfe7d8..07986c6b3c 100644 --- a/heapster-saw/examples/sha512_proofs.v +++ b/heapster-saw/examples/sha512_proofs.v @@ -18,3 +18,4 @@ Lemma no_errors_sha512_block_data_order_simpl1 : refinesFun sha512_block_data_order_simpl1 (fun _ _ _ => noErrorsSpec). Proof. unfold sha512_block_data_order_simpl1, sha512_block_data_order_simpl1__tuple_fun. + Set Printing Depth 1000. From 1f152aa8337a4e50dba83a926c78a962543b2c1a Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Mon, 22 Nov 2021 13:47:51 -0800 Subject: [PATCH 03/10] don't duplicate arg permissions in tcJumpTarget --- heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs | 8 ++++++++ .../src/Verifier/SAW/Heapster/TypedCrucible.hs | 10 ++++++---- 2 files changed, 14 insertions(+), 4 deletions(-) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs index 7f7066474c..7068a9564c 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs @@ -4758,6 +4758,14 @@ buildDistPerms :: (forall a. Name a -> ValuePerm a) -> RAssign Name ps -> buildDistPerms _ MNil = DistPermsNil buildDistPerms f (ns :>: n) = DistPermsCons (buildDistPerms f ns) n (f n) +-- | Like 'buildDistPerms', but accumulates some state through a @foldr@ +foldrAndBuildDistPerms :: (forall a. Name a -> b -> (ValuePerm a, b)) -> b -> + RAssign Name ps -> (DistPerms ps, b) +foldrAndBuildDistPerms _ b0 MNil = (DistPermsNil, b0) +foldrAndBuildDistPerms f b0 (ns :>: n) + | (ps, b) <- foldrAndBuildDistPerms f b0 ns, (p, b') <- f n b + = (DistPermsCons ps n p, b') + -- | Split a list of distinguished permissions into two splitDistPerms :: f ps1 -> RAssign g ps2 -> DistPerms (ps1 :++: ps2) -> (DistPerms ps1, DistPerms ps2) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs index c94d803119..fc972cc47b 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs @@ -3825,10 +3825,12 @@ tcJumpTarget ctx (JumpTarget blkID args_tps args) = tops_perms = varPermsMulti tops_ns cur_perms tops_set = NameSet.fromList $ namesToNamesList tops_ns ghosts_perms = varPermsMulti ghosts_ns cur_perms - args_perms = - buildDistPerms (\n -> if NameSet.member n tops_set then - ValPerm_Eq (PExpr_Var n) - else cur_perms ^. varPerm n) args_ns + args_perms = fst $ + foldrAndBuildDistPerms (\n tops_or_seen -> + if NameSet.member n tops_or_seen + then (ValPerm_Eq (PExpr_Var n), tops_or_seen) + else (cur_perms ^. varPerm n, NameSet.insert n tops_or_seen)) + tops_set args_ns perms_in = appendDistPerms (appendDistPerms tops_perms args_perms) ghosts_perms in implTraceM (\i -> From aeec7ef68ade62e51eb5bcffac53036f78d10931 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Tue, 23 Nov 2021 07:05:30 -0800 Subject: [PATCH 04/10] bug fix: changed tcJumpTarget to freshen up the argument names in any jump, as both the type-checker and translator rely on all arguments being distinct variables --- .../src/Verifier/SAW/Heapster/Implication.hs | 23 +++++++++++++ .../Verifier/SAW/Heapster/TypedCrucible.hs | 32 +++++++------------ 2 files changed, 34 insertions(+), 21 deletions(-) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs index 824e900bd5..bed740f0b4 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs @@ -78,6 +78,16 @@ concatSomeRAssign :: [Some (RAssign f)] -> Some (RAssign f) concatSomeRAssign = foldl apSomeRAssign (Some MNil) -- foldl is intentional, appending RAssign matches on the second argument +-- | Map a monadic function over an 'RAssign' list from left to right while +-- maintaining an "accumulator" that is threaded through the mapping +rlMapMWithAccum :: Monad m => (forall a. accum -> f a -> m (g a, accum)) -> + accum -> RAssign f tps -> m (RAssign g tps, accum) +rlMapMWithAccum _ accum MNil = return (MNil, accum) +rlMapMWithAccum f accum (xs :>: x) = + do (ys,accum') <- rlMapMWithAccum f accum xs + (y,accum'') <- f accum' x + return (ys :>: y, accum'') + ---------------------------------------------------------------------- -- * Equality Proofs @@ -3424,6 +3434,19 @@ implLetBindVars CruCtxNil MNil = pure MNil implLetBindVars (CruCtxCons tps tp) (es :>: e) = (:>:) <$> implLetBindVars tps es <*> implLetBindVar tp e +-- | Freshen up a sequence of names by replacing any duplicate names in the list +-- with fresh, let-bound variables +implFreshenNames :: NuMatchingAny1 r => RAssign ExprVar tps -> + ImplM vars s r ps ps (RAssign ExprVar tps) +implFreshenNames ns = + fmap fst $ rlMapMWithAccum + (\prevs n -> + if NameSet.member n prevs then + (implGetVarType n >>>= \tp -> implLetBindVar tp (PExpr_Var n) >>>= \n' -> + return (n', prevs)) + else return (n, NameSet.insert n prevs)) + NameSet.empty ns + -- | Project out a field of a struct @x@ by binding a fresh variable @y@ for its -- contents, and assign the permissions for that field to @y@, replacing them -- with a proof that the field equals @y@, popping the permissions for @y@ and diff --git a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs index fc972cc47b..3657d60986 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs @@ -3767,21 +3767,6 @@ tcJumpTarget ctx (JumpTarget blkID args_tps args) = top_get >>= \top_st -> get >>= \st -> gets (permCheckExtStateNames . stExtState) >>= \(Some ext_ns) -> - let tops_ns = stTopVars st - args_t = tcRegs ctx args - args_ns = typedRegsToVars args_t - tops_args_ns = RL.append tops_ns args_ns - tops_args_ext_ns = RL.append tops_args_ns ext_ns - {- - (gen_perms_hint, join_point_hint) = - case stFnHandle top_st of - SomeHandle h -> - (lookupBlockGenPermsHint (stPermEnv top_st) h - (stBlockTypes top_st) blkID - , - lookupBlockJoinPointHint (stPermEnv top_st) h - (stBlockTypes top_st) blkID) -} in - tcBlockID blkID >>>= \tpBlkID -> -- Step 0: run all of the following steps inside a local ImplM computation, @@ -3792,6 +3777,13 @@ tcJumpTarget ctx (JumpTarget blkID args_tps args) = -- simplifications of each branch do not affect each other. pcmRunImplImplM CruCtxNil mempty $ + -- NOTE: the args all must be distinct variables (this is required by + -- implPushOrReflMultiM below and also the translation of jump targets) + implFreshenNames (typedRegsToVars $ tcRegs ctx args) >>>= \args_ns -> + let tops_ns = stTopVars st + tops_args_ns = RL.append tops_ns args_ns + tops_args_ext_ns = RL.append tops_args_ns ext_ns in + -- Step 1: Compute the variables whose values are determined by the -- permissions on the top and normal arguments as the starting point for -- figuring out our ghost variables. The determined variables are the only @@ -3825,12 +3817,10 @@ tcJumpTarget ctx (JumpTarget blkID args_tps args) = tops_perms = varPermsMulti tops_ns cur_perms tops_set = NameSet.fromList $ namesToNamesList tops_ns ghosts_perms = varPermsMulti ghosts_ns cur_perms - args_perms = fst $ - foldrAndBuildDistPerms (\n tops_or_seen -> - if NameSet.member n tops_or_seen - then (ValPerm_Eq (PExpr_Var n), tops_or_seen) - else (cur_perms ^. varPerm n, NameSet.insert n tops_or_seen)) - tops_set args_ns + args_perms = + buildDistPerms (\n -> if NameSet.member n tops_set + then ValPerm_Eq (PExpr_Var n) + else cur_perms ^. varPerm n) args_ns perms_in = appendDistPerms (appendDistPerms tops_perms args_perms) ghosts_perms in implTraceM (\i -> From d1eb9b47394fc78eff23c1a76c445715ddef0d84 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Tue, 23 Nov 2021 07:07:35 -0800 Subject: [PATCH 05/10] added a line to turn off translation checks when type-checking sha512_block_data_order --- heapster-saw/examples/sha512.saw | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/heapster-saw/examples/sha512.saw b/heapster-saw/examples/sha512.saw index 84a6d1f9e8..a85a7a522a 100644 --- a/heapster-saw/examples/sha512.saw +++ b/heapster-saw/examples/sha512.saw @@ -64,6 +64,7 @@ heapster_typecheck_fun env "return_state" "(). arg0:array(W,0,<8,*8,fieldsh(int64<>)) -o \ \ arg0:array(W,0,<8,*8,fieldsh(int64<>))"; +heapster_set_translation_checks env false; heapster_typecheck_fun env "sha512_block_data_order" "(num:bv 64). arg0:array(W,0,<8,*8,fieldsh(int64<>)), \ \ arg1:array(R,0,<16*num,*8,fieldsh(int64<>)), \ @@ -73,4 +74,4 @@ heapster_typecheck_fun env "sha512_block_data_order" \ arg2:true, ret:true"; -heapster_export_coq env "sha512_gen.v"; \ No newline at end of file +heapster_export_coq env "sha512_gen.v"; From 12d5eba992d6d5510d8309bafb21dbd5380ab650 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Tue, 23 Nov 2021 10:46:31 -0800 Subject: [PATCH 06/10] changed the translation of calls to multi-entry blocks so they no longer accumulate Hobbits variables from the caller --- .../Verifier/SAW/Heapster/SAWTranslation.hs | 28 ++++++++++++++++--- 1 file changed, 24 insertions(+), 4 deletions(-) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs index b1006d1b7b..72eb1af7d3 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs @@ -827,6 +827,13 @@ instance TransInfo info => Translate info ctx (ExprVar a) (ExprTrans a) where translate mb_x = RL.get (translateVar mb_x) <$> infoCtx <$> ask +instance TransInfo info => + Translate info ctx (RAssign ExprVar as) (ExprTransCtx as) where + translate mb_exprs = case mbMatch mb_exprs of + [nuMP| MNil |] -> return MNil + [nuMP| ns :>: n |] -> + (:>:) <$> translate ns <*> translate n + instance TransInfo info => Translate info ctx (PermExpr a) (ExprTrans a) where translate mb_tr = case mbMatch mb_tr of @@ -1980,6 +1987,15 @@ tpTransM = withInfoM (\(ImpTransInfo {..}) -> TypeTransInfo itiExprCtx itiPermEnv itiChecksFlag) +-- | Run an implication translation computation in an "empty" environment, where +-- there are no variables in scope and no permissions held anywhere +inEmptyEnvImpTransM :: ImpTransM ext blocks tops ret RNil RNil a -> + ImpTransM ext blocks tops ret ps ctx a +inEmptyEnvImpTransM = + withInfoM (\(ImpTransInfo {..}) -> + ImpTransInfo { itiExprCtx = MNil, itiPermCtx = MNil, + itiPermStack = MNil, itiPermStackVars = MNil, .. }) + -- | Get most recently bound variable getTopVarM :: ImpTransM ext blocks tops ret ps (ctx :> tp) (ExprTrans tp) getTopVarM = (\(_ :>: p) -> p) <$> itiExprCtx <$> ask @@ -4059,6 +4075,8 @@ translateCallEntry :: forall ext tops args ghosts blocks ctx ret. translateCallEntry nm entry_trans mb_tops_args mb_ghosts = -- First test that the stack == the required perms for entryID do let entry = typedEntryTransEntry entry_trans + ectx <- translate $ mbMap2 RL.append mb_tops_args mb_ghosts + stack <- itiPermStack <$> ask let mb_s = mbMap2 (\tops_args ghosts -> permVarSubstOfNames $ RL.append tops_args ghosts) @@ -4073,10 +4091,12 @@ translateCallEntry nm entry_trans mb_tops_args mb_ghosts = -- If so, call the letRec-bound function translateApply nm f mb_perms Nothing -> - -- If not, continue by translating entry, setting the variable - -- permission map to empty (as in the beginning of a block) - clearVarPermsM $ translate $ - fmap (\s -> varSubst s $ typedEntryBody entry) mb_s + inEmptyEnvImpTransM $ inCtxTransM ectx $ + do perms_trans <- translate $ typedEntryPermsIn entry + withPermStackM + (const $ RL.members ectx) + (const $ typeTransF perms_trans $ transTerms stack) + (translate $ typedEntryBody entry) instance PermCheckExtC ext => From 341035c7f985613c2ffbeb9bce4eecb0599a5d18 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Tue, 23 Nov 2021 11:19:46 -0800 Subject: [PATCH 07/10] whoops, removed an infinite loop in splitLLVMBlockPerm when it is called on a block with the empty shape --- heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs index 5a5e280817..eef99a5381 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs @@ -3942,6 +3942,10 @@ splitLLVMBlockPerm off bp | bvEq off (llvmBlockOffset bp) = Just (bp { llvmBlockLen = bvInt 0, llvmBlockShape = PExpr_EmptyShape }, bp) +splitLLVMBlockPerm off bp@(llvmBlockShape -> PExpr_EmptyShape) = + Just (bp { llvmBlockLen = bvSub off (llvmBlockOffset bp) }, + bp { llvmBlockOffset = off, + llvmBlockLen = bvSub (llvmBlockLen bp) off }) splitLLVMBlockPerm off bp@(LLVMBlockPerm { llvmBlockShape = sh }) | Just sh_len <- llvmShapeLength sh , bvLt sh_len (bvSub off (llvmBlockOffset bp)) = @@ -3951,10 +3955,6 @@ splitLLVMBlockPerm off bp@(LLVMBlockPerm { llvmBlockShape = sh }) splitLLVMBlockPerm off (bp { llvmBlockShape = PExpr_SeqShape sh PExpr_EmptyShape }) splitLLVMBlockPerm _ (llvmBlockShape -> PExpr_Var _) = Nothing -splitLLVMBlockPerm off bp@(llvmBlockShape -> PExpr_EmptyShape) = - Just (bp { llvmBlockLen = bvSub off (llvmBlockOffset bp) }, - bp { llvmBlockOffset = off, - llvmBlockLen = bvSub (llvmBlockLen bp) off }) splitLLVMBlockPerm off bp@(llvmBlockShape -> PExpr_NamedShape maybe_rw maybe_l nmsh args) | TrueRepr <- namedShapeCanUnfoldRepr nmsh From 7a0744338aae2f89ff8f8619e4aea3573e8f6b5f Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Tue, 23 Nov 2021 11:22:05 -0800 Subject: [PATCH 08/10] commented out the sha512 example from the _CoqProject, because it takes a while to run... --- heapster-saw/examples/_CoqProject | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/heapster-saw/examples/_CoqProject b/heapster-saw/examples/_CoqProject index 82dc5d4a7a..f3f488864e 100644 --- a/heapster-saw/examples/_CoqProject +++ b/heapster-saw/examples/_CoqProject @@ -30,5 +30,5 @@ clearbufs_gen.v clearbufs_proofs.v mbox_gen.v mbox_proofs.v -sha512_gen.v -sha512_proofs.v +#sha512_gen.v +#sha512_proofs.v From 3fb38093609805b153986443644364ce2ced15aa Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Tue, 23 Nov 2021 14:56:25 -0500 Subject: [PATCH 09/10] remove `foldrAndBuildDistPerms` --- heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs | 8 -------- 1 file changed, 8 deletions(-) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs index eef99a5381..3571d3fea9 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs @@ -4944,14 +4944,6 @@ buildDistPerms :: (forall a. Name a -> ValuePerm a) -> RAssign Name ps -> buildDistPerms _ MNil = DistPermsNil buildDistPerms f (ns :>: n) = DistPermsCons (buildDistPerms f ns) n (f n) --- | Like 'buildDistPerms', but accumulates some state through a @foldr@ -foldrAndBuildDistPerms :: (forall a. Name a -> b -> (ValuePerm a, b)) -> b -> - RAssign Name ps -> (DistPerms ps, b) -foldrAndBuildDistPerms _ b0 MNil = (DistPermsNil, b0) -foldrAndBuildDistPerms f b0 (ns :>: n) - | (ps, b) <- foldrAndBuildDistPerms f b0 ns, (p, b') <- f n b - = (DistPermsCons ps n p, b') - -- | Split a list of distinguished permissions into two splitDistPerms :: f ps1 -> RAssign g ps2 -> DistPerms (ps1 :++: ps2) -> (DistPerms ps1, DistPerms ps2) From 3f6bd04bbcb7c9c2faea0fc9dbfe36cd89525d3c Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Tue, 23 Nov 2021 13:14:08 -0800 Subject: [PATCH 10/10] get mbox_proofs.v working again --- heapster-saw/examples/mbox_proofs.v | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/heapster-saw/examples/mbox_proofs.v b/heapster-saw/examples/mbox_proofs.v index 97f3ad2742..def38151e9 100644 --- a/heapster-saw/examples/mbox_proofs.v +++ b/heapster-saw/examples/mbox_proofs.v @@ -59,9 +59,9 @@ Ltac either_unfoldMbox m := simpl foldMbox; simpl Mbox__rec in *; unfold_projs end. -Hint Extern 0 (SAWCorePrelude.either _ _ _ _ _ (unfoldMbox ?m) |= _) => +Global Hint Extern 0 (SAWCorePrelude.either _ _ _ _ _ (unfoldMbox ?m) |= _) => either_unfoldMbox m : refinesM. -Hint Extern 0 (_ |= SAWCorePrelude.either _ _ _ _ _ (unfoldMbox ?m)) => +Global Hint Extern 0 (_ |= SAWCorePrelude.either _ _ _ _ _ (unfoldMbox ?m)) => either_unfoldMbox m : refinesM. Lemma transMbox_Mbox_nil_r m : transMbox m Mbox_nil = m. @@ -232,7 +232,7 @@ Definition mbox_drop_spec : Mbox -> bitvector 64 -> Mbox := Mbox__rec _ (fun _ => Mbox_nil) (fun strt len next rec d ix => if bvuge 64 ix len then Mbox_cons (intToBv 64 0) (intToBv 64 0) (rec (bvSub 64 ix len)) d - else Mbox_cons (bvAdd 64 ix strt) (bvSub 64 len ix) next d). + else Mbox_cons (bvAdd 64 strt ix) (bvSub 64 len ix) next d). Lemma mbox_drop_spec_ref : refinesFun mbox_drop (fun x ix => returnM (mbox_drop_spec x ix)). @@ -382,9 +382,7 @@ Proof. (* Most of the remaining cases are taken care of with just bvAdd_id_l and bvAdd_id_r *) all: try rewrite bvAdd_id_r; try rewrite bvAdd_id_l; try reflexivity. (* The remaining case just needs a few more rewrites *) - - f_equal. - rewrite bvAdd_assoc; f_equal. - rewrite bvAdd_comm; reflexivity. + - rewrite bvAdd_assoc, bvAdd_comm, bvAdd_assoc; reflexivity. - cbn; rewrite transMbox_Mbox_nil_r; reflexivity. Time Qed.