From 7b64242ef0311fdb4ef1319135955891431d54fb Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Tue, 14 Sep 2021 19:54:05 -0400
Subject: [PATCH 1/7] fix debug output for widening

---
 heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs | 1 +
 heapster-saw/src/Verifier/SAW/Heapster/Widening.hs      | 7 ++++---
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
index 37f01075a7..3c082ae4b6 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
@@ -4074,6 +4074,7 @@ visitEntry names can_widen blk entry =
 
   mapM (traverseF $
         visitCallSite entry) (typedEntryCallers entry) >>= \callers ->
+  debugTrace dlevel ("can_widen: " ++ show can_widen ++ ", any_fails: "  ++ show (any (anyF typedCallSiteImplFails) callers)) $
   if can_widen && any (anyF typedCallSiteImplFails) callers then
     case widenEntry dlevel entry of
       Some entry' ->
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs b/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs
index b52408a0e0..2460e27d71 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs
@@ -180,9 +180,10 @@ setVarNamesM :: String -> RAssign ExprVar tps -> WideningM ()
 setVarNamesM base xs = modify $ over wsPPInfo $ ppInfoAddExprNames base xs
 
 traceM :: (PPInfo -> Doc ()) -> WideningM ()
-traceM f =
-  debugTrace <$> (view wsDebugLevel <$> get)
-  <*> (renderDoc <$> f <$> view wsPPInfo <$> get) <*> (return ())
+traceM f = do
+  dlevel <- view wsDebugLevel <$> get
+  str <- renderDoc <$> f <$> view wsPPInfo <$> get
+  debugTrace dlevel str $ return ()
 
 
 ----------------------------------------------------------------------

From 43326d4670d351b1f886a6d7be68bc2b6c1976a4 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Tue, 14 Sep 2021 19:55:05 -0400
Subject: [PATCH 2/7] widen equal variables with different offsets, proveEqH
 still not working

---
 .../src/Verifier/SAW/Heapster/Permissions.hs  |  1 +
 .../src/Verifier/SAW/Heapster/Widening.hs     | 26 +++++++++++--------
 2 files changed, 16 insertions(+), 11 deletions(-)

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
index a7c41f5a3c..60c1bc730f 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
@@ -4779,6 +4779,7 @@ isDeterminingExpr (PExpr_BV [BVFactor _ _] _) =
   -- A linear expression N*x + M lets you solve for x when it is possible
   True
 isDeterminingExpr (PExpr_ValPerm (ValPerm_Eq e)) = isDeterminingExpr e
+isDeterminingExpr (PExpr_LLVMOffset _ off) = isDeterminingExpr off
 isDeterminingExpr e =
   -- If an expression has no free variables then it vacuously determines all of
   -- its free variables
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs b/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs
index 2460e27d71..7c66f3466c 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs
@@ -271,17 +271,21 @@ widenExpr' tp e1@(asVarOffset -> Just (x1, off1)) e2@(asVarOffset ->
        _ | x1 == x2 && offsetsEq off1 off2 ->
            visitM x1 >> return e1
 
-       -- If we have the same variable but different offsets, then the two sides
-       -- cannot be equal, so we generalize with a new variable
-       _ | x1 == x2 ->
-           do x <- bindFreshVar tp
-              visitM x
-              ((p1',p2'), p') <-
-                doubleSplitWidenPerm tp (offsetPerm off1 p1) (offsetPerm off2 p2)
-              setOffVarPermM x1 off1 p1'
-              setOffVarPermM x2 off2 p2'
-              setVarPermM x p'
-              return $ PExpr_Var x
+       -- If we have the same variable but different offsets, e.g., if we are
+       -- widening x &+ bv1 and x &+ bv2, then bind a fresh variable bv for the
+       -- offset and return x &+ bv. Note that we cannot have the same variable
+       -- x on both sides unless they have been visited, so we can safely
+       -- ignore the isv1 and isv2 flags. The complexity of having these two
+       -- cases is to find the BVType of one of off1 or off2; because the
+       -- previous case did not match, we know at least one is LLVMPermOffset.
+       _ | x1 == x2, LLVMPermOffset (exprType -> off_tp) <- off1 ->
+           do off_var <- bindFreshVar off_tp
+              visitM off_var
+              return $ PExpr_LLVMOffset x1 (PExpr_Var off_var)
+       _ | x1 == x2, LLVMPermOffset (exprType -> off_tp) <- off2 ->
+           do off_var <- bindFreshVar off_tp
+              visitM off_var
+              return $ PExpr_LLVMOffset x1 (PExpr_Var off_var)
 
        -- If a variable has an eq(e) permission, replace it with e and recurse
        (ValPerm_Eq e1', _, _, _) ->

From 2da2e101db802c103090bd3ef1229ea86e5d5929 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Tue, 21 Sep 2021 18:08:45 -0400
Subject: [PATCH 3/7] handle offsets in proveEqH, get simpl0 working, fix bvNeg
 Coq defn

---
 heapster-saw/examples/_CoqProject             |   2 +
 heapster-saw/examples/loops_proofs.v          |   2 +-
 heapster-saw/examples/sha512.bc               | Bin 0 -> 5760 bytes
 heapster-saw/examples/sha512.c                | 231 ++++++++++++++++++
 heapster-saw/examples/sha512.saw              |  15 ++
 heapster-saw/examples/sha512_proofs.v         |  88 +++++++
 .../src/Verifier/SAW/Heapster/Implication.hs  |  81 +++++-
 .../Verifier/SAW/Heapster/SAWTranslation.hs   |   5 +
 .../CryptolToCoq/SAWCoreBitvectors.v          |  16 +-
 .../CryptolToCoq/SAWCoreVectorsAsCoqVectors.v |   5 +-
 10 files changed, 431 insertions(+), 14 deletions(-)
 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/loops_proofs.v b/heapster-saw/examples/loops_proofs.v
index f87bc5035d..725ef7e572 100644
--- a/heapster-saw/examples/loops_proofs.v
+++ b/heapster-saw/examples/loops_proofs.v
@@ -108,7 +108,7 @@ Lemma compare_sum_spec_ref : refinesFun compare_sum compare_sum_spec.
 Proof.
   unfold compare_sum, compare_sum__tuple_fun, compare_sum_spec.
   time "compare_sum_spec_ref" prove_refinement.
-  all: rewrite bvSub_zero_bvNeg in e_assert.
+  all: rewrite bvSub_zero_n in e_assert.
   (* Note that there are two versions of each case because of the if! *)
   (* The `x < y + z` case: *)
   1,4: continue_prove_refinement_left.
diff --git a/heapster-saw/examples/sha512.bc b/heapster-saw/examples/sha512.bc
new file mode 100644
index 0000000000000000000000000000000000000000..a842697c86310e7ad92adc1644e1b1ad40f595d6
GIT binary patch
literal 5760
zcmc&Ye{d7mnQy)Fu58QF8ViuHq^vOUi4^RW48mahkSqfxI7ARG2UG5>wI#5@Kh~14
zEt5-DmSGL&%gB_pZp+O`sgrYm+>BBfj@;!BSvHQ3a~VT(oJ&27Jp2e{2z45Ir4#OQ
z-&_9(y*B;tdOLb=-}}Dreee7I-s)CzWe$Qz3(dO%AsQi~%9Xse5dbho^(t=7Ti<;5
zo!|V&8!bP*@bc&X^vTb+uCFF+nSe8^5Mp4ElVL^~Fo)%c4i^qMClos=#<uwk(W`ns
zQ>iy8{<dD!Zp)}TlT$Us*tBIz-L7og-o6@P%v@N#OzLNxXEMAK%J;OaYkMF2uY_%H
zukHoQ3sLK9iGu^|<q6<>ibZHSylty%vRLm4#Wz+D^+I>MHy+h4t3BPH(>qkl91JL8
z+z!!gAsKO8nRGbJr>!S<=ZUcmJD9U?D~T1>j1!jKs5_wWM9G0ME!un<SfV{TgvQ}r
z@bu4~d;t$3pezgNAXB1F>WtDMi_{*YJ0>K1RO%e2J6XxkN_JKXCZr&Y8zZ4UIuw)a
z9NpCz=}^+$4mxQ_g^l;(1~F_%IZcnu#+i8Ty|C#9Z<ykZH$A5NPSdRs<JEZXG@y7R
z>M>mBO(~~gI&Qcrno?%tbUb(5Y?uZn1Sbg|DP*BVjt(iM4vS<LrOq0<GbZ_?G>d6a
zkMRm`x);w)J55)3%<4)!cakvOG#e(qT;3=J1<CG_{AHM-Jt6sZbaxjWYK$DOq5UyB
zh|-9inKj;IjWZ(#;D$NGjH$3`>Pseq)Y(WL8<sjm$sUsgh6Z^;Xc9z)O$m8<(wG_n
z-M?~qBvc~>1lfjDpn}vn_y<jgQpQ{HTrgCMFr~ptvxeUjMx;YsbUPSiknUDW?fdEU
z%GYOCjuXZkyy-q~e0|CI1PjJb@rE0+iEf3lmF~|P@5FP*;-<+F!xg6qoO0dy+!Z28
zilA3i3Rvjw#z?y;b)$6LFyl1+Y6R>IJ~Ca68}5U4ad5He0XDcv+^C~p>m$oO5j;qe
z_WfiaDTSi6eSf5*k$w%}gOcE&1M&b|3GmP$=nj<fU~q8|BRBOej3Mea1AUUNxI~H&
zb-;mxU?T%y`9?{={#r8o1KH#EW{s0!)6Jw|dKP;P1(b9L?1Jo;6pm_*sBk-s=x-8)
z{=Z@R2D*u&;-6283=u^+4!R&(g_e1UALRBr(QAo#Sr6;5Yx@`lfzVFK4+Z2$evhY$
zt!1gVxgsSE37@|Klr4XfSsshnm2{Vgg8|D1Su=<YQYJ*ohRIEdNbb9Cb<32xdrsYg
zG=6~w=>sg?&C&iTYL2Bl8F?%N=LsMjI~;VkhYn6rzkptzws_QCi0)=+zeu;F)m<^V
z-LtR|h+DXvc9!mn<)xy1K@@8FJQdC6C?ppqoa6|Ry1n`-LLuU@{CJS-g|F>GNVy0=
zDo@R?DLtu3E<rHOzB$wH@QF^d?h9`t#O5gEwKmfrqtC02_GcCC7+1JXZ*%y6<P51!
z-*qc}Zm`pPV86cuj-^V`Fg9yAq$Mi*TxGqZ{Z(=V2L{_!_mJijM*Ub+m#V5vkUtP)
zhqz3cEK)E@R!+Do`^n15uKu7vA6L?lLV`ed3uH%^B(RcxGEe<5s-EREt(@leoO;f!
zE@j4yw;(Oe#uRTl#GNYtAW}Z%+I)em_#jfzOO{X0X*)dh@kV-6BSaOwNyI@fc)*2p
z$CFH8+bK$QkW@O!KPZI;!|NW+sUM})zfP(ja%BBP+;AsufE<8+hBsU>8^*#=gQy!(
z*X9Y==0Ul?G+K7nRR(!+cC-XGecDt05m}xXRejhb3Hv3#5D7NYT^=c@lY%ixfAtm3
zBc%D2TYV?0zU|P=vg(JR1#5v~gtP9t*)S6}&7=)?W{nRB(;?lSvV?2Pxk&k>d(DC(
z9;vg7?i$=v`#7q>7BC%=^W1ENQu{h#!UCI(b3C>0M5JtTv^?Re1cN+HRorov_rY|u
z|8h2HDs_T9P{b{?e=vOTHlu!+RNr;0KjR8Vt~*V4W>-RX-2wq>^yP_2<%LK=?`T=S
zYxCr2#ifzW6QiJG#bnKecE~*s-Hxl0r2qN2`k_bjNg85ZbC=WHWi|ilR<|<h+ngGv
zpQWi^q}6xa>L;9Q_NEyh8*_v#Iiwy6u?X2=;5XH<u0EAM%Wtb;3&Z^b1J|l!jKy1F
zwN<?tHGi**|D4)YxHjv@bZa{2#jWg$t%jd$)jgT3P9gM4^)B{RpFhyl)>_@k`wuNm
zeD%i;vpZW4wJkzA8yb0kU7)Gk=icdJYkeKQ=0GFA(P}GhDEW&3uqbKagTWBrz<0E@
z`bvPvxwpC`z;~_>H29l@U`eBo7Xm?_e?7oTd|iBt(CiC11?bs^X1?_>+c7T(3oN-}
zj<v|p^;R1Pv*J=)v2AS$CU0usgCK68WPd}O*H_F7LW!%bHRx*%21=^2SZ#vOU*c}&
zgNNGuErF7k_=cBX*<UOy0G^=%<(JR_@6iQ982#VwQ*tceFKKFRXg=okmDB}8f-g`~
zcdV&3Xx~s5EN)yJHMfCH<nCB&py_a{&&vYM|C4BCi;}@$NgNyze?oZzA+Xbexo{j}
zk>=ljLLr(;%j^qM6gSq@d3k?lQ>&a7b-~|rR#R*1u@+QxX#U9HdYI*f$}`p;##pG#
zv-L2~7b*vAXP0wc5eO7MnTlZ1Dch)+`7>3dsJT=%o%{(G9J7zcmQOn}JqE;)oJ&;g
zLvS(w%z*S8V#tuJ&h=Oi&k>FCdUCl)qGSc_pqLC6qbiTg5l3ZI{zg#`g9NS}sP-eI
zLC8@c!Xbn>H&Klcu+5)myKjN*9wC|IFko`bX=mFU;l~s7)6DT>=)-oyhv5^tzA*k>
zBE0X1*A7Pt#GWm~ku8_P1%nwC!;yYPk)_aX{}=nWE^hkqmW#HPr56+D-`|t{OESVS
zk%QCI4{siv7`u9K{K59Df8HlguTNZ=xxYQ@3PRt9vk`xL<YfCTaOTk6`-MSQB^(_I
z*XF6wo_mJz`AZ;NDb2?FaxGu6;kHNpu^WyE%^iGDXg+qUA1BhV7EZ8XeEkM~*BFH0
z^hfk$#ZaXD92`PqWh_zw2U2tt+lFTm>VS8?qIw;W%GU(Nc61~L7oATz__hJq>Kzl&
zJ=xVH{x%3SK`G+`;Aw<@I22JmKy0L5lZ^<+7%AG2cwn1Ad&TOnove65x~I9JaKYqA
zQ5AZObl*~TdIp@c6oLA8^_E|nhz*hi8h<`zoF??TCWOSRWR_PsU@nYDiE{Lj%|nY>
zDaA|7xyGJ!4Jys68j7ZB70lWpE}y8*UaKl#$SPDw(Wu8G)SQQ#+}1R{&mr86_B;28
za8XSr2(v-K)eDGKQqr2wG3pcOG->FzPU^ImSIvMtIs;PnjF>Our5;Q~;_n|#DRp85
z(6Ce3iSnuBIw#lQW=D+(Wr?u1CO{)0OaLN5I28(xN2*QA8XaIJ1R8Pw#;Qho3CBsc
zl-ia`6X-FkxB_#hGM{o#Y>^68p>JC)XA~Ng&LE0ZB2QLjDLpB~Zjb6CRn9qtx|xi_
zDWtQr=R^bq2YNi?F~`Yr_!z}2SKU=3PedPiTmJ~$RuBFlp?zJER9{qmyBGT&KRk=j
zZg}S_oL~AkyXS@yVA#K_;Vt`DJq8ho(9Zz&%FdVEwbnY<-UIG^FV{7<@!q;)P_FBJ
zLeTH`1sDBJp3<yY^82=24-PZ=S$9N)?OBZj2iP<_6gD-lR(LdG`zg2@JE$`z1>%bH
z=F;j3&x;^)k@6d*P64i#&-%F8q0A%}9P{Y}c8mi%#`Vhu$0+D7wCMec_W-zc5))0y
zF79_)t$^0|{k_#POlXiuIl+E;WG`}Z9+R0nokfb2<B;m~iz6hO2CEKJ6-X4Z0dR%*
zx+1NX6@iXt5n2X%<SS}q`(Ya^j(8L?*0LfqoIzk4?f{r<!&QB9{rKxV<p_Y#{FR}u
zzPYX8C=|~iU)SdM`tZF1a>yD8@<AWJ&)NhB-BK=*Z)(eyY<gf@g7zZn+K*PJNn1^%
z{?)w4gnr0r{h{)ysJhOoURA}C+5ecRS7!cY*NJVp5HV<ou;85wln(8TM{Uo`;IfmK
zs;9|vmfWq)z)5)AGeCSyW#A;Nyfh(xHzFsYX@<}TAqi#T3N})l3!V!gZ;bXJEe1v^
zSn_4~<6$bqhE-;pcg?<4+BqUN9TPPulOns(aG7q3Oe*5vDN^QdbP7Mn>S=)7J=){p
z!LPe<?)EO_?qoF@sLC$Qb6{|_cJ24LW`|C_=<e|Mu_xWwlab#-2YHzJ8|pYhqg3@Z
zCfPSah^)@A{{co_fNtv`bYDPf3hyK!@0uNqYKc`Gv*Lb-6`cdD7V3uQAMkoPygZl^
z>c%zeGw63QdJJQh(3Q`i-@)h)o<+|Z0exOE((fdwQ3&ZgTqrzK4+(TInd~L7o&-^=
zL!-GF`4s4-Q(<~lDi2_1%WMtqK4*$XQ(>kopF)`;rlhKuG0A?XnWCRVXnhax^E#;4
zunL(_`l4O1my^nV4%fOkRG|iUlmHfv99(zwS|GfDY&<&1&Tqd#-d>RfTMZKWIk_zT
zd%u&X4ky8O^=@1!v-AomeR>P59i<dnygN@RVfSrVo5OBc<yK7e5<(bP#ROr^l#5>h
zvsbSI+5xH-q**rtq6~$vgD86qAj+!h*MVJb_#~*kZB;Ey&Z~O!fM1jQF@d6)6aCIO
z^&xC>0BgNciOXpLv)=(*ARpfMsPGi_rJmXMJ$c{BWm+&~f%XlE{>xU_bL1Y4#BhN)
zudpzJfZurqxORX#0sKRlSu67?Y^uW+zvLW|Eq)GHYXYoxqM!^kU&+i%;F2YHD-4KC
z0}F^sC9z8O%a~p+`jgARTJw(F(%_zOLJTqt3CAbY5r^iYD#ZTR$TxZI8aGZ%)XvWT
zhhS4Pt9#M=l!ZAiD#ExLBjkhs5jVkm8F@B=ODC>H_&S9PYb`Vk+Yb#t_>KR2oWc`$
znxU<Nb`l!qwpff8@c@$P@%v3^i{}HTgDCz2twHE580SI5FlGU+T!+xRFvh&`|C;zx
zwMd_YF@~2wTZCi!n=l7MqZ(+C155NUM1Q41aPY}G{ub*qf1hY>?r16Y)*mkR`rt#z
z@B7LVNG5FYwKNE!Vu5Qao9~+J8~%8$o&U<}Dzn$wH>`(`sAk{#7QUe^&}HR{ts9H&
giywFMrJ1Yy-}2Obr9ktfe@LRbKQ0nB#xu|V04RZKiU0rr

literal 0
HcmV?d00001

diff --git a/heapster-saw/examples/sha512.c b/heapster-saw/examples/sha512.c
new file mode 100644
index 0000000000..ccf8e32c1b
--- /dev/null
+++ b/heapster-saw/examples/sha512.c
@@ -0,0 +1,231 @@
+#include <stdlib.h>
+#include <stdint.h>
+#include <string.h>
+
+uint64_t simpl0(const uint8_t *in, size_t num) {
+  uint64_t sum = 0;
+  
+  while (num--) {
+    sum += in[0];
+    in += 1;
+  }
+  
+  return sum;
+}
+
+// First simplication of sha512_block_data_order
+
+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) T1 += a;
+
+#define SIMPL1_ROUND_02_10(i, j, a) T1 += a;
+
+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;
+  }
+}
\ No newline at end of file
diff --git a/heapster-saw/examples/sha512.saw b/heapster-saw/examples/sha512.saw
new file mode 100644
index 0000000000..362d9f95f6
--- /dev/null
+++ b/heapster-saw/examples/sha512.saw
@@ -0,0 +1,15 @@
+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_typecheck_fun env "simpl0" "(num:bv 64).arg0:array(0,<num,*1,[(W,0,8) |-> int8<>]), arg1:eq(llvmword(num)) -o arg0:array(0,<num,*1,[(W,0,8) |-> int8<>]), arg1:true, ret:int64<>";
+
+// heapster_assume_fun env "SIMPL1_CRYPTO_load_u64_be" "(rw:rwmodality, l1:lifetime, l2:lifetime, b:llvmblock 64).arg0:[l2]memblock(rw,0,8,eqsh(b)) -o arg0:[l2]memblock(rw,0,8,eqsh(b)), ret:[l1]memblock(W,0,8,eqsh(b))" "\\ (_:#()) -> returnM (#() * #() * #()) ((),(),())";
+
+// heapster_typecheck_fun env "sha512_block_data_order_simpl1" "(num:bv 64).arg0:array(0,<1,*8,[(W,0) |-> int64<>]), arg1:array(0,<2*num,*8,[(W,0) |-> int64<>]), arg2:eq(llvmword(num)) -o arg0:array(0,<1,*8,[(W,0) |-> int64<>]), arg1:array(0,<2*num,*8,[(W,0) |-> 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..e05c78eb68
--- /dev/null
+++ b/heapster-saw/examples/sha512_proofs.v
@@ -0,0 +1,88 @@
+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.
+
+Load "sha512_gen.v".
+Import SHA512.
+
+Import VectorNotations.
+
+
+Definition simpl0_invar (num0 idx num : bitvector 64) :=
+  isBvule 64 idx num0 /\ num = bvSub 64 num0 idx.
+
+Lemma no_errors_simpl0 : refinesFun simpl0 (fun num arr => noErrorsSpec).
+Proof.
+  unfold simpl0, simpl0__tuple_fun.
+  prove_refinement_match_letRecM_l.
+  - exact (fun num0 idx num sum arr _ _ _ => assumingM (simpl0_invar num0 idx num) noErrorsSpec).
+  unfold noErrorsSpec, simpl0_invar.
+  time "no_errors_simpl0" prove_refinement.
+  all: try assumption.
+  - assert (isBvult 64 a2 a1).
+    + apply isBvule_to_isBvult_or_eq in e_assuming.
+      destruct e_assuming; [assumption |].
+      apply bvEq_bvSub_r in H.
+      symmetry in H; contradiction.
+    + rewrite H in e_maybe; discriminate e_maybe.
+  - apply isBvult_to_isBvule_suc; assumption.
+  - repeat rewrite bvSub_eq_bvAdd_neg.
+    rewrite bvAdd_assoc; f_equal.
+    rewrite bvNeg_bvAdd_distrib; reflexivity.
+  - apply isBvule_zero_n.
+  - symmetry; apply bvSub_n_zero.
+Qed.
+
+
+Definition simpl0_spec num : BVVec 64 num (bitvector 8) -> bitvector 64 :=
+  foldr _ _ _ (fun a b => bvAdd 64 b (bvUExt 56 8 a)) (intToBv 64 0).
+
+Definition simpl0_letRec_spec num0 idx num (sum : bitvector 64) arr (_ _ _ : unit) :=
+  forallM (fun (pf : isBvule 64 idx num0) =>
+  assumingM (num = bvSub 64 num0 idx)
+            (returnM (arr, (bvAdd 64 sum (simpl0_spec (bvSub 64 num0 idx)
+                                                      (dropBVVec _ _ _ idx pf arr)), tt)))).
+
+Lemma simpl0_spec_ref :
+  refinesFun simpl0 (fun num arr => returnM (arr, (simpl0_spec num arr, tt))).
+Proof.
+  unfold simpl0, simpl0__tuple_fun.
+  prove_refinement_match_letRecM_l.
+  - exact simpl0_letRec_spec.
+  unfold noErrorsSpec, simpl0_letRec_spec, simpl0_spec.
+  time "simpl0_spec_ref" prove_refinement.
+  (* Why didn't prove_refinement do this? *)
+  3: prove_refinement_eauto; [| apply refinesM_returnM ].
+  7: prove_refinement_eauto; [| apply refinesM_returnM ].
+  (* same as no_errors_simpl0 *)
+  - assert (isBvult 64 a2 a1).
+    + apply isBvule_to_isBvult_or_eq in e_forall.
+      destruct e_forall; [assumption |].
+      apply bvEq_bvSub_r in H.
+      symmetry in H; contradiction.
+    + rewrite H in e_maybe; discriminate e_maybe.
+  - apply isBvult_to_isBvule_suc; assumption.
+  - repeat rewrite bvSub_eq_bvAdd_neg.
+    rewrite bvAdd_assoc; f_equal.
+    rewrite bvNeg_bvAdd_distrib; reflexivity.
+  (* unique to this proof *)
+  - admit.
+  - repeat f_equal.
+    admit.
+  (* same as no_errors_simpl0 *)
+  - apply isBvule_zero_n.
+  - symmetry; apply bvSub_n_zero.
+  (* unique to this proof *)
+  - rewrite bvAdd_id_l.
+    repeat f_equal.
+    admit.
+Admitted.
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
index 2a430f012a..826897df7c 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
@@ -30,6 +30,7 @@
 module Verifier.SAW.Heapster.Implication where
 
 import Data.Maybe
+import Data.Either
 import Data.List
 import Data.Functor.Product
 import Data.Functor.Compose
@@ -219,6 +220,12 @@ someEqProof1 x e flag =
   let eq_step = EqProofStep (MNil :>: EqPerm x e flag) (\(_ :>: e') -> e') in
   SomeEqProofCons (SomeEqProofRefl $ eqProofStepLHS eq_step) eq_step
 
+-- | A 'SomeEqProof' for the identity @x = x &+ 0@
+someEqProofZeroOffset :: (1 <= w, KnownNat w) => ExprVar (LLVMPointerType w) ->
+                         SomeEqProof (PermExpr (LLVMPointerType w))
+someEqProofZeroOffset x =
+  someEqProof1 x (PExpr_LLVMOffset x (zeroOfType (BVRepr knownNat))) True
+
 -- | Apply symmetry to a 'SomeEqProof', changing an @e1=e2@ proof to @e2=e1@
 someEqProofSym :: SomeEqProof a -> SomeEqProof a
 someEqProofSym eqp_top =
@@ -419,6 +426,12 @@ data SimplImpl ps_in ps_out where
                       SimplImpl (RNil :> LLVMPointerType w :> BVType w)
                       (RNil :> LLVMPointerType w)
 
+  -- | The implication that @x@ is the same as @x &+ 0@
+  --
+  -- > . -o x:eq(x &+ 0)
+  SImpl_LLVMOffsetZeroEq :: (1 <= w, KnownNat w) => ExprVar (LLVMPointerType w) ->
+                            SimplImpl RNil (RNil :> LLVMPointerType w)
+
   -- | Introduce an empty conjunction on @x@, i.e.:
   --
   -- > . -o x:true
@@ -1569,6 +1582,7 @@ simplImplIn (SImpl_InvTransEq x y e) =
 simplImplIn (SImpl_CopyEq x e) = distPerms1 x (ValPerm_Eq e)
 simplImplIn (SImpl_LLVMWordEq x y e) =
   distPerms2 x (ValPerm_Eq (PExpr_LLVMWord (PExpr_Var y))) y (ValPerm_Eq e)
+simplImplIn (SImpl_LLVMOffsetZeroEq _) = DistPermsNil
 simplImplIn (SImpl_IntroConj _) = DistPermsNil
 simplImplIn (SImpl_ExtractConj x ps _) = distPerms1 x (ValPerm_Conj ps)
 simplImplIn (SImpl_CopyConj x ps _) = distPerms1 x (ValPerm_Conj ps)
@@ -1872,6 +1886,8 @@ simplImplOut (SImpl_InvTransEq x y _) = distPerms1 x (ValPerm_Eq $ PExpr_Var y)
 simplImplOut (SImpl_CopyEq x e) = distPerms2 x (ValPerm_Eq e) x (ValPerm_Eq e)
 simplImplOut (SImpl_LLVMWordEq x _ e) =
   distPerms1 x (ValPerm_Eq (PExpr_LLVMWord e))
+simplImplOut (SImpl_LLVMOffsetZeroEq x) =
+  distPerms1 x (ValPerm_Eq (PExpr_LLVMOffset x (zeroOfType (BVRepr knownNat))))
 simplImplOut (SImpl_IntroConj x) = distPerms1 x ValPerm_True
 simplImplOut (SImpl_ExtractConj x ps i) =
   if i < length ps then
@@ -2368,6 +2384,8 @@ instance SubstVar PermVarSubst m =>
       SImpl_CopyEq <$> genSubst s x <*> genSubst s e
     [nuMP| SImpl_LLVMWordEq x y e |] ->
       SImpl_LLVMWordEq <$> genSubst s x <*> genSubst s y <*> genSubst s e
+    [nuMP| SImpl_LLVMOffsetZeroEq x |] ->
+      SImpl_LLVMOffsetZeroEq <$> genSubst s x
     [nuMP| SImpl_IntroConj x |] ->
       SImpl_IntroConj <$> genSubst s x
     [nuMP| SImpl_ExtractConj x ps i |] ->
@@ -3507,6 +3525,9 @@ implProveEqPerms DistPermsNil = pure ()
 implProveEqPerms (DistPermsCons ps' x (ValPerm_Eq (PExpr_Var y)))
   | x == y
   = implProveEqPerms ps' >>> introEqReflM x
+implProveEqPerms (DistPermsCons ps' x (ValPerm_Eq (PExpr_LLVMOffset y off)))
+  | x == y, bvMatchConstInt off == Just 0
+  = implProveEqPerms ps' >>> implSimplM Proxy (SImpl_LLVMOffsetZeroEq x)
 implProveEqPerms (DistPermsCons ps' x p@(ValPerm_Eq _)) =
   implProveEqPerms ps' >>> implPushCopyM x p
 implProveEqPerms _ = error "implProveEqPerms: non-equality permission"
@@ -4528,7 +4549,8 @@ substEqsWithProof a =
 
 
 -- | The main work horse for 'proveEq' on expressions
-proveEqH :: NuMatchingAny1 r => PartialSubst vars -> PermExpr a ->
+proveEqH :: forall vars a s r ps. NuMatchingAny1 r =>
+            PartialSubst vars -> PermExpr a ->
             Mb vars (PermExpr a) ->
             ImplM vars s r ps ps (SomeEqProof (PermExpr a))
 proveEqH psubst e mb_e = case (e, mbMatch mb_e) of
@@ -4575,6 +4597,20 @@ proveEqH psubst e mb_e = case (e, mbMatch mb_e) of
             Just _ -> proveEqH psubst e mb_e
             Nothing -> proveEqFail e mb_e
 
+  -- To prove @x &+ o = e@, we subtract @o@ from the RHS and recurse
+  (PExpr_LLVMOffset x off, _) ->
+    proveEq (PExpr_Var x) (fmap (`addLLVMOffset` bvNegate off) mb_e) >>= \some_eqp ->
+    pure $ fmap (`addLLVMOffset` off) some_eqp
+
+  -- To prove @x = x &+ o@, we prove that @0 = o@ and combine it with the fact
+  -- that @x = x &+ 0@ ('someEqProofZeroOffset') using transitivity
+  (PExpr_Var x, [nuMP| PExpr_LLVMOffset mb_y mb_off |])
+    | Right y <- mbNameBoundP mb_y
+    , x == y ->
+      proveEq (zeroOfType (BVRepr knownNat)) mb_off >>= \some_eqp ->
+      pure $ someEqProofTrans (someEqProofZeroOffset y)
+                              (fmap (PExpr_LLVMOffset y) some_eqp)
+
   -- To prove x=e, try to see if x:eq(e') and proceed by transitivity
   (PExpr_Var x, _) ->
     getVarEqPerm x >>= \case
@@ -4599,19 +4635,48 @@ proveEqH psubst e mb_e = case (e, mbMatch mb_e) of
   (PExpr_LLVMWord e', [nuMP| PExpr_LLVMWord mb_e' |]) ->
     fmap PExpr_LLVMWord <$> proveEqH psubst e' mb_e'
 
-  -- Prove e = N*z + M where e - M is a multiple of N by setting z = (e-M)/N
-  (_, [nuMP| PExpr_BV [BVFactor (BV.BV mb_n) z] (BV.BV mb_m) |])
-    | Left memb <- mbNameBoundP z
-    , Nothing <- psubstLookup psubst memb
-    , bvIsZero (bvMod (bvSub e (bvInt $ mbLift mb_m)) (mbLift mb_n)) ->
-      setVarM memb (bvDiv (bvSub e (bvInt $ mbLift mb_m)) (mbLift mb_n)) >>>
-      pure (SomeEqProofRefl e)
+  -- Prove e = L_1*y_1 + ... + L_k*y_k + N*z + M where z is an unset variable,
+  -- each y_i is either a set variable with value e_i or an unbound variable
+  -- with e_i = y_i, and e - (L_1*e_1 + ... + L_k*e_k + M) is divisible by N,
+  -- by setting z = (e - (L_1*e_1 + ... + L_k*e_k + M))/N
+  (_, [nuMP| PExpr_BV mb_factors (BV.BV mb_m) |])
+    | Just (n, memb, e_factors) <- getUnsetBVFactor mb_factors
+    , e' <- bvSub e (bvAdd e_factors (bvInt $ mbLift mb_m))
+    , bvIsZero (bvMod e' n) ->
+      setVarM memb (bvDiv e' n) >>> pure (SomeEqProofRefl e)
 
   -- FIXME: add cases to prove struct(es1)=struct(es2)
 
   -- Otherwise give up!
   _ -> proveEqFail e mb_e
 
+  where -- If there is exactly one 'BVFactor' in a list of 'BVFactor's which is
+        -- an unset variable, return the value of its 'BV', the witness that it
+        -- is bound, and the result of adding together the remaining factors
+        getUnsetBVFactor :: (1 <= w, KnownNat w) => Mb vars [BVFactor w] ->
+                            Maybe (Integer, Member vars (BVType w), PermExpr (BVType w))
+        getUnsetBVFactor (mbList -> mb_factors) =
+          case partitionEithers $ mbFactorNameBoundP <$> mb_factors of
+            ([(n, memb)], xs) -> Just (n, memb, foldl' bvAdd (bvInt 0) xs)
+            _ -> Nothing
+
+        -- If a 'BVFactor' in a binding is an unset variable, return the value
+        -- of its 'BV' and the witness that it is bound. Otherwise, return the
+        -- constant of the factor multiplied by the variable's value if it is
+        -- a set variable, or the constant of the factor multiplied by the
+        -- variable, if it is an unbound variable
+        mbFactorNameBoundP :: Mb vars (BVFactor w) ->
+                              Either (Integer, Member vars (BVType w))
+                                     (PermExpr (BVType w))
+        mbFactorNameBoundP (mbMatch -> [nuMP| BVFactor (BV.BV mb_n) mb_z |]) =
+          let n = mbLift mb_n in
+          case mbNameBoundP mb_z of
+            Left memb -> case psubstLookup psubst memb of 
+                           Nothing -> Left (n, memb)
+                           Just e' -> Right (bvMultBV (BV.mkBV knownNat n) e')
+            Right z -> Right (PExpr_BV [BVFactor (BV.mkBV knownNat n) z]
+                                       (BV.zero knownNat))
+
 
 -- | Build a proof on the top of the stack that @x:eq(e)@. Assume that all @x@
 -- permissions are on the top of the stack and given by argument @p@, and pop
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
index 080a890d2d..fd39e0e2b8 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
@@ -2226,6 +2226,11 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
     (\(pctx :>: _ :>: _) -> (pctx :>: PTrans_Eq (fmap PExpr_LLVMWord e)))
     m
 
+  [nuMP| SImpl_LLVMOffsetZeroEq x |] ->
+    let bvZero = zeroOfType (BVRepr knownNat) in
+    withPermStackM (:>: translateVar x)
+                   (:>: PTrans_Eq (fmap (flip PExpr_LLVMOffset bvZero) x)) m
+
   [nuMP| SImpl_IntroConj x |] ->
     withPermStackM (:>: translateVar x) (:>: PTrans_True) m
 
diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v
index af2d4cb0be..b0f1520905 100644
--- a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v
@@ -141,6 +141,9 @@ Instance Proper_isBvslt_isBvsle w : Proper (isBvsle w --> isBvsle w ==> impl) (i
 Definition isBvult_to_isBvule w a b : isBvult w a b -> isBvule w a b. Admitted.
 Instance Proper_isBvult_isBvule w : Proper (isBvule w --> isBvule w ==> impl) (isBvult w). Admitted.
 
+Definition isBvule_to_isBvult_or_eq w a b : isBvule w a b -> isBvult w a b \/ a = b.
+Admitted.
+
 Definition isBvslt_to_isBvsle_suc w a b : isBvslt w a b ->
                                           isBvsle w (bvAdd w a (intToBv w 1)) b.
 Admitted.
@@ -169,6 +172,9 @@ Admitted.
 Definition isBvslt_antirefl w a : ~ isBvslt w a a.
 Admitted.
 
+Definition isBvule_zero_n w a : isBvule w (intToBv w 0) a.
+Admitted.
+
 Definition isBvule_n_zero w a : isBvule w a (intToBv w 0) <-> a = intToBv w 0.
 Admitted.
 
@@ -198,16 +204,22 @@ Admitted.
 
 (** Lemmas about bitvector subtraction, negation, and sign bits **)
 
-Lemma bvSub_zero_bvNeg w a : bvSub w (intToBv w 0) a = bvNeg w a.
+Lemma bvSub_n_zero w a : bvSub w a (intToBv w 0) = a.
 Admitted.
 
-Hint Rewrite bvSub_zero_bvNeg : SAWCoreBitvectors_eqs.
+Lemma bvSub_zero_n w a : bvSub w (intToBv w 0) a = bvNeg w a.
+Admitted.
+
+Hint Rewrite bvSub_zero_n : SAWCoreBitvectors_eqs.
 
 Lemma bvNeg_msb w a : msb w (bvNeg (Succ w) a) = not (msb w a).
 Admitted.
 
 Hint Rewrite bvNeg_msb : SAWCoreBitvectors_eqs.
 
+Lemma bvNeg_bvAdd_distrib w a b : bvNeg w (bvAdd w a b) = bvAdd w (bvNeg w a) (bvNeg w b).
+Admitted.
+
 Lemma bvslt_bvSub_r w a b : isBvslt w a b <-> isBvslt w (intToBv w 0) (bvSub w b a).
 Admitted.
 
diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v
index abeb37c3dd..c55770b12b 100644
--- a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v
@@ -234,11 +234,10 @@ Definition bvMul (n : nat) (a : bitvector n) (b : bitvector n)
   := bitsToBv (mulB (bvToBITS a) (bvToBITS b)).
 Global Opaque bvMul.
 
-(* This is annoying to implement, so using BITS conversion *)
+(* This is annoying to implement, so use bvSub *)
 Definition bvNeg (n : nat) (a : bitvector n)
   : bitvector n
-  := bitsToBv (invB (bvToBITS a)).
-Global Opaque bvNeg.
+  := bvSub n (intToBv n 0) a.
 
 (* FIXME this is not implemented *)
 Definition bvUDiv (n : nat) (a : bitvector n) (b : bitvector n)

From 22d9b79cbe79ae81cdb0834d59aef439b35e5ff2 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Tue, 12 Oct 2021 12:46:03 -0700
Subject: [PATCH 4/7] regenerate Coq files

---
 .../generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v | 9 +++++++++
 saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v | 6 ++++++
 2 files changed, 15 insertions(+)

diff --git a/saw-core-coq/coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v b/saw-core-coq/coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v
index bd70288f3f..3e1306614c 100644
--- a/saw-core-coq/coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v
+++ b/saw-core-coq/coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v
@@ -782,6 +782,15 @@ Definition ecArrayLookup : forall (a : Type), forall (b : Type), @SAWCorePrelude
 Definition ecArrayUpdate : forall (a : Type), forall (b : Type), @SAWCorePrelude.Array a b -> a -> b -> @SAWCorePrelude.Array a b :=
   @SAWCorePrelude.arrayUpdate.
 
+Definition ecArrayCopy : forall (n : @Num), forall (a : Type), @SAWCorePrelude.Array (@seq n (@SAWCoreScaffolding.Bool)) a -> @seq n (@SAWCoreScaffolding.Bool) -> @SAWCorePrelude.Array (@seq n (@SAWCoreScaffolding.Bool)) a -> @seq n (@SAWCoreScaffolding.Bool) -> @seq n (@SAWCoreScaffolding.Bool) -> @SAWCorePrelude.Array (@seq n (@SAWCoreScaffolding.Bool)) a :=
+  @finNumRec (fun (n : @Num) => forall (a : Type), @SAWCorePrelude.Array (@seq n (@SAWCoreScaffolding.Bool)) a -> @seq n (@SAWCoreScaffolding.Bool) -> @SAWCorePrelude.Array (@seq n (@SAWCoreScaffolding.Bool)) a -> @seq n (@SAWCoreScaffolding.Bool) -> @seq n (@SAWCoreScaffolding.Bool) -> @SAWCorePrelude.Array (@seq n (@SAWCoreScaffolding.Bool)) a) (@SAWCorePrelude.arrayCopy).
+
+Definition ecArraySet : forall (n : @Num), forall (a : Type), @SAWCorePrelude.Array (@seq n (@SAWCoreScaffolding.Bool)) a -> @seq n (@SAWCoreScaffolding.Bool) -> a -> @seq n (@SAWCoreScaffolding.Bool) -> @SAWCorePrelude.Array (@seq n (@SAWCoreScaffolding.Bool)) a :=
+  @finNumRec (fun (n : @Num) => forall (a : Type), @SAWCorePrelude.Array (@seq n (@SAWCoreScaffolding.Bool)) a -> @seq n (@SAWCoreScaffolding.Bool) -> a -> @seq n (@SAWCoreScaffolding.Bool) -> @SAWCorePrelude.Array (@seq n (@SAWCoreScaffolding.Bool)) a) (@SAWCorePrelude.arraySet).
+
+Definition ecArrayRangeEq : forall (n : @Num), forall (a : Type), @SAWCorePrelude.Array (@seq n (@SAWCoreScaffolding.Bool)) a -> @seq n (@SAWCoreScaffolding.Bool) -> @SAWCorePrelude.Array (@seq n (@SAWCoreScaffolding.Bool)) a -> @seq n (@SAWCoreScaffolding.Bool) -> @seq n (@SAWCoreScaffolding.Bool) -> @SAWCoreScaffolding.Bool :=
+  @finNumRec (fun (n : @Num) => forall (a : Type), @SAWCorePrelude.Array (@seq n (@SAWCoreScaffolding.Bool)) a -> @seq n (@SAWCoreScaffolding.Bool) -> @SAWCorePrelude.Array (@seq n (@SAWCoreScaffolding.Bool)) a -> @seq n (@SAWCoreScaffolding.Bool) -> @seq n (@SAWCoreScaffolding.Bool) -> @SAWCoreScaffolding.Bool) (@SAWCorePrelude.arrayRangeEq).
+
 Definition AESEncRound : @SAWCoreVectorsAsCoqVectors.Vec 4 (@SAWCoreVectorsAsCoqVectors.Vec 32 (@SAWCoreScaffolding.Bool)) -> @SAWCoreVectorsAsCoqVectors.Vec 4 (@SAWCoreVectorsAsCoqVectors.Vec 32 (@SAWCoreScaffolding.Bool)) :=
   fun (x : @SAWCoreVectorsAsCoqVectors.Vec 4 (@SAWCoreVectorsAsCoqVectors.Vec 32 (@SAWCoreScaffolding.Bool))) => @SAWCoreScaffolding.error (@SAWCoreVectorsAsCoqVectors.Vec 4 (@SAWCoreVectorsAsCoqVectors.Vec 32 (@SAWCoreScaffolding.Bool))) "Unimplemented: AESEncRound"%string.
 
diff --git a/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v b/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v
index 36631738c1..4ef4273fa5 100644
--- a/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v
+++ b/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v
@@ -1060,6 +1060,12 @@ Axiom arrayLookup : forall (a : Type), forall (b : Type), @Array a b -> a -> b .
 
 Axiom arrayUpdate : forall (a : Type), forall (b : Type), @Array a b -> a -> b -> @Array a b .
 
+Axiom arrayCopy : forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), @Array (@SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) a -> @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool) -> @Array (@SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) a -> @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool) -> @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool) -> @Array (@SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) a .
+
+Axiom arraySet : forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), @Array (@SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) a -> @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool) -> a -> @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool) -> @Array (@SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) a .
+
+Axiom arrayRangeEq : forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), @Array (@SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) a -> @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool) -> @Array (@SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool)) a -> @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool) -> @SAWCoreVectorsAsCoqVectors.Vec n (@SAWCoreScaffolding.Bool) -> @SAWCoreScaffolding.Bool .
+
 Axiom arrayEq : forall (a : Type), forall (b : Type), @Array a b -> @Array a b -> @SAWCoreScaffolding.Bool .
 
 (* Prelude.bveq_sameL was skipped *)

From b4b73f210829b680fc751bf529c0eb95c2d6a7d0 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Tue, 12 Oct 2021 13:16:25 -0700
Subject: [PATCH 5/7] fix tuples in simpl0 proof

---
 heapster-saw/examples/sha512_proofs.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/heapster-saw/examples/sha512_proofs.v b/heapster-saw/examples/sha512_proofs.v
index e05c78eb68..ec1d2f3d4e 100644
--- a/heapster-saw/examples/sha512_proofs.v
+++ b/heapster-saw/examples/sha512_proofs.v
@@ -49,11 +49,11 @@ Definition simpl0_spec num : BVVec 64 num (bitvector 8) -> bitvector 64 :=
 Definition simpl0_letRec_spec num0 idx num (sum : bitvector 64) arr (_ _ _ : unit) :=
   forallM (fun (pf : isBvule 64 idx num0) =>
   assumingM (num = bvSub 64 num0 idx)
-            (returnM (arr, (bvAdd 64 sum (simpl0_spec (bvSub 64 num0 idx)
-                                                      (dropBVVec _ _ _ idx pf arr)), tt)))).
+            (returnM (arr, bvAdd 64 sum (simpl0_spec (bvSub 64 num0 idx)
+                                                     (dropBVVec _ _ _ idx pf arr))))).
 
 Lemma simpl0_spec_ref :
-  refinesFun simpl0 (fun num arr => returnM (arr, (simpl0_spec num arr, tt))).
+  refinesFun simpl0 (fun num arr => returnM (arr, simpl0_spec num arr)).
 Proof.
   unfold simpl0, simpl0__tuple_fun.
   prove_refinement_match_letRecM_l.

From a087f5426ee59a547f5dad1f41172572063448e4 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Tue, 12 Oct 2021 14:30:36 -0700
Subject: [PATCH 6/7] move simpl0 from sha512.c to sum_inc_ptr in arrays.c,
 remove sha512.c

---
 heapster-saw/examples/_CoqProject     |   2 -
 heapster-saw/examples/arrays.bc       | Bin 9136 -> 10656 bytes
 heapster-saw/examples/arrays.c        |  11 ++
 heapster-saw/examples/arrays.saw      |   2 +
 heapster-saw/examples/arrays_proofs.v |  71 ++++++++
 heapster-saw/examples/sha512.bc       | Bin 5760 -> 0 bytes
 heapster-saw/examples/sha512.c        | 231 --------------------------
 heapster-saw/examples/sha512.saw      |  15 --
 heapster-saw/examples/sha512_proofs.v |  88 ----------
 9 files changed, 84 insertions(+), 336 deletions(-)
 delete mode 100644 heapster-saw/examples/sha512.bc
 delete mode 100644 heapster-saw/examples/sha512.c
 delete mode 100644 heapster-saw/examples/sha512.saw
 delete mode 100644 heapster-saw/examples/sha512_proofs.v

diff --git a/heapster-saw/examples/_CoqProject b/heapster-saw/examples/_CoqProject
index 8012aab001..878793f383 100644
--- a/heapster-saw/examples/_CoqProject
+++ b/heapster-saw/examples/_CoqProject
@@ -28,5 +28,3 @@ clearbufs_gen.v
 clearbufs_proofs.v
 mbox_gen.v
 mbox_proofs.v
-sha512_gen.v
-sha512_proofs.v
diff --git a/heapster-saw/examples/arrays.bc b/heapster-saw/examples/arrays.bc
index 0d4c1e9f711667041a379515e28307c50e790467..52ffa9c5ea5ffcec69227a12ea664f30260f4144 100644
GIT binary patch
literal 10656
zcmc&)eRLbum4D+I&B(Ss#ve)KSQ6tT1VJ2oY$wJcNs(k5oK0wDNWegPtg&Us2FD&t
zia!EnN0y9CYI+n%sadi;atW+kOjnQ;QkvaLvJ*^dsA1F84cV+sOd4oN4WwOmOLzCa
z(PwDb!#~^AIWzO#oA+_wd%yd;_rB4&@Um<KzkIlSHzLF!L|CiC=hj03q*0TKU-jLm
zo`3G&fBm<+|K-Rx{`Bfc@7}t$hA3CSyCM}r2Qv}M&L~0|kY5TH<5{`iGDU5n+42of
z5I)uQ3T1(j`gW6)Uz=flBHMb1Ezhq~>b7Q;-#Jt#P8O}K$@LGjmM1bCQ_7d}x$4`7
zxHpLMJAJyFOg9C}9uDo?&mEtFejnoy(!sNQMO`N67^I$DamWX^^S;qQe(tt?!`Z$=
z+gP`Y3Yvo~hs;fsoeQ#u4p^UO5oI1zap=w#j$qeNnJDnAO^JwL)$P(uF&UIT)Dyae
z@ZYagK97{S3RDk+yawYGetyGe{|!GvM42YiOhzT0zc;}2oBZ8Drf14u8SwXxF}<AM
z$@wcezdPi2L%Pk|Kg9G0{gph^*XHd}GJDNTSReHmE{y6Wk3MQKUM@169aUfO7*7lO
z8NqPIZoFtQo{JdX8dcB2E5U#U^zR79s6{_Jsy`zcqeX_<QT2%;{Va4s@P5(m?>8|L
z&-5$(Jtlvp<nOIxdV_vvfZ=c*G+;O>7%z;f=PbsP0`BVMsCt?(o+;8#rJA?--J-wJ
z?srz<4l6@`r;gd%$Mm;(AF5-VLB@^d5O;RoaE3FSjp(5_+(Xb1^%!STorwP4HgeCH
zzen;{2K^$-fIR(Z8bpOb3AuUL5RJgxzqGlxzs~Ox<u#mvDfoLwuDNt5YB)ElhJ}g}
z#yMD}dHr7qBQgDbOgAjZ2(wq|?`~k`mOV1R>;z#rEf_BfhDVZ%PjImKQ9*xNUZQgz
zyh<164GW{{$x-8UM1Rs^giU$Ja@|QHOiD1XfZt_e_O^MuCI4PDH>y8tF@6$(b%s4M
zzBQ`92(uf7EjE6L7u+bV*D((dksIw^oCuSZ4WujV?+-AQ4c?wM=3yuw@r!20B`07j
zp}c<t<_<OG#7H6$ByS#yrvY^vpnjOybd;0;b<hJ3U?W|y@@;+*?^kl!Ka_X;!n|SH
zV>}bq&(7mrLoOxL1EZiyQxv0GD^WJH0euUhEr55dyLkh4E2tRCTL(gK{7kVi=&e*T
zeG=YOJO-eD1W&9=^j3|LH;26H=WUwZGn&1Nn%zk26d91h#W8z%#yLYTa!fBPr{%&}
z1%OqLnb~V++%xnCaF?^Y?V3Ks>}46J#O$8a^aYu2d%Pi3-pyxsb4*__CmK+)wP^K!
zL<3oER7_xy6(Nb%-MKzMP!i6_zZq2hqqi&wDH8=~xxMZu^kW&woGgJlH{H_r#eN>o
zcn%>pS!rE3@Zr*Y8cE5LAo1w-`Nb-Ppk@50<_`@pTL{D@3Q(I=^xZmL4zOsV$V{q!
zXlwf6RU(<2yymyxq>xmM2gI_L8%OdBa<&DAGgse!f~tP4*4#I4=~un>zD?O;gAIBK
z_UUn`SD}>jlk@u4d}8xZb(L>o*eWC6HPWrRfV3a6nk$l~LS;3A-T^pUd4*ifTR2T_
zo~qtFOm3d;8+MD#LrMlzPZXKGBH7dD7dd~ybdKgyKr_#4J9+K-Ma`m3Q^8Ie&Vf1?
z8KQ!*m49sGG4IBi>J3N8O~<^OeB{RI#rz&S^H3Xea~q(Mxmm)>BH95mOwVTu=(bn#
zH-a+i{LT@7|A?pf@}lPQoaPT<%_W{}ni|zFjOsym;C@!npDfZ(dVss=(}C&@Q`H+r
z<onTyssq(kpic)TN@38?2R5D}H-;uuuebZf2ESAEy4#pOyWg$zyMz9Mx9-wjM%qto
znuUPoyjeTXX)eJmI1`W<*4B55^k+TBvvc}|dBcZ<u~k=J6{^1Fpm*c6ZB=|Cc7Jal
z(>GGT?Mgt4SHSpy%nwBdpy)>kBNn*Guqe>m2fbC(6B|R-n_)pdk8WD1-Z%u=iQ(f}
zFjIdo$OGhWVw@wMo#$E2rLg9Go90t~W#k=;abbQLXyrK&psrwJ$h-N7x6n6HHC(-6
zdScVj$cCv2nB%7Dx+C47vv#H%vzfo(-4mKicI`)Vpj+DadF}h0_K!AAC#yNnYasjS
z9R0zZX2GWUjIW+QQ-saUA|XqTVc5?hGz(9sv5u=AQWa!6%j>w6p5gub->wO=Cda0-
za_e^jMbFmNpQpC2yfO1-rgJVkt4{wWPyJbHAkkelTe-VioUZn+&YE7q*_zC>H0{~N
zZRu?7N|f|Aw+YThSNq-;+m>o>TT4$%hv0My{jQSc(j6}7qI9?5cJ~X-LQhv`ODR;c
z+*woV5_;FVnw{;UyR@xE5MAyT=UON$ZRrzsiybX4iwJkFxkKpO#r4GG;L6HN_!6Eo
z$)#({%6Z6@RFs#L-&l&Pw>JxJ5Z6`O(A?!{DG@}mw7RR)-O}lHmDXUfy2KV|sjWkB
zw{|&qyGrj6n!j;ZLx~tKNUH;rPri0J9*kFn)c@@`rF&e?()P~gjy;Z+QdhsLw9(x!
zw!ovk(_Oi)(OuFOPjqy_s>nAefW_`;>1_Wiik1*-Pg1T#Dka#SPFMS`&K3s;bzFOP
zqm{~Emk&r~E0y<D42T;b2M<g2y+j@jOlan4fGQAiM!-~|+F^f_-<eT4VN?G`<-N^b
zp}MDDy&at(Pz9=>rp$^ELi{g@fQ8I56WdOqrPZ|2Cb#G7$xYBrE6Rd<*zGB^5j6-+
zyO4wTWQZtly>$I^5oSzg>1lo>QZOFb=0hO@^dj@*(Bp6Z_|4}&dVKslFHRpHUVEvd
z^FY)2TYmqGL0mq#?b3A1c;^B0Rylk9<KxqhLk@i59|A{XKRP?hX#(zJ_BMzk)tiCB
zLe(2)CI&9(PsE%UaEXcx7iCUay6(JP^IIEGm39FWmiD(c&6Us`v;`&|!|o&W_cj;_
zJSk>+(;@H1gFuGl=Ad^I5My8hPe9-h8ir>cb(?HYusx@4Lw^Gg^f8anDtNBAeJW5-
z*HCImH-jb!?VT>Z(b>`r`4<kYRGmdiZ&Z_o2(yDkWk|ZWc99nB`osH>CK?`UT|(%6
z#Cy{>Wo%HAj%RjIPL|&HvWNFp@MOhojS_r`^SSftgS_c24oTgQEz;l6<+pMue6*&I
zG^w&GbjUt{zM1Dk&u~-$42ddo!ixRTZ8f6h5T8fvWN)0VLCb2gCg{lk8y<=f5~tJM
zi#>4d0^Dw$#$F5GY|9rGX~cJ!l}ch*r$@>G&wh{m>c8MV@j2YI6?E-9-G$HuT_YyD
z`pxh0tM}lR>gplr%1m$-^k8?GKr?7+*dp*EG*nwf8cO#=>2x_|g<*BC7ou>8=w3xZ
zMqjH(;bKdffC4$t##7})XgexzwsBABk(n7_r*-*5D;eB(9vv2|XQT+!+77i2tH>Pu
zl4S54cr^i;EoG3|YTKqmM=0o{xX^&mS_xic>t;Zz3>e|10|XS(tP)DUT>z!=soUvE
zJXUtK++7WUyW46>beB&+ck3b`IGsnEF+MRa?x(^S0`gDbzAA2flm=Q{g`37CZpbMO
zcQtNUgNz$)pNyNxf{Yt)dki<<#kg5t<z1h`&G&ifbR0Kd*O_-EaT8pRal`J+qm*C3
z4JG3y=PTpJ-1HT2qoA0tfE)883Eb4W0U;~_JCsuv!wnC(sXdUwO-(v(>XNvzVce8$
zNZ@8$3O7%F5jSN!Qn-0C9XH!kxWU+K&|}<q00DO=aU(npxCtvTMoy<-Ls(<5S(*-;
zyRU|gJsmdJ#LW=kA&;uNCf{5S@8Wzz!tp=~H;_(n&5P>Ft1%N+%b1Z0TbEdXYj)9x
z_n9@(;MUe95xvi{>qXs%oc4-+=Za&VJo?=N3h^a5=jJlKyVVrZeNQQ(LE=^5$cvi-
z=119r^4xueeWbac>_Q`)`7~8@bhVP8znpWVBvH)DL?Ls|6tD&6oQ{8$mA^<&@l7J)
zlr(+ePw-|!W~WbNO3~%NyZl&EFFk+2Y{cQ4H%>{4Wf20Y3R#Z@0Vfn&pj%O?M@WG+
zUB48_f&?N`ynY;N-K-=Ep!6V=^1tA8Kpqh_z{`Q@!Tkm_T7nyWvw}f09*zRQeQ%mT
zHZ<iU__ORfJ9O=y!3;HFmS0ZE18=KFP}Bc5P+G2D7NM-!*5`%ZuE)LY)J+m-=Uf>2
z=r9)(1kll8N*=izGpUcv2@hL7R)cyRre60EW(}5BM?t<2suE?0guTVw@`~!28f>%h
zPv8)G0-j%nlVW%m!^tG2g>;HvgjVnYlUOM`>Ma9@pr#VBBpTU4b+NRA2TrL{lI6M>
zTng+lxTv1Ex0YuF8-04;sOFE7wvufX=?6pfGfE;v#?jL((y&!qeK+?-?W)t}n7y*;
zh9k>WDEO&4qrmEzsxy`A06<Si!i8wHa%R0n8OpQ<z}S8{hEjIxX&FQ3Wn{n&V`w;{
z1AG7gGOTDN&7c9h-SJPj!jN16-zI<(=<XOzQB2ajeT-qmrkl6py3etC${-3v5@e((
zFu_)>!(0&X<N<Wfa+Cu`4iGpK!;yt1VZ#eBOSA+qXfSux({CotR;)A~N(YE_xH-=P
z80zWA09PR*vJRWU1H^6cW~(Se<v7?*I*BF+4>-OCnk;m++`+sVcW@BP9_wHMiygE;
zJ{0j0ENt_a;pvSuJmEUn&yg-Gk!MBB*IARmRMsSO3id07DOZ=%-QvJ5Pn*!u+AH)Y
z@wL9qyFMLXB1?CO(>DzOzAC}>0Xp&&Rvq4F2Tw>HlJSL@ljAGKynMjxxI1UoqMM3T
zzM#CssV+(dz(sSu$nt|01TGPw`99y^UC$zb-l<5T&!Qg(nPTSbH&oHg|Awbvl9QIp
zOe5oIMutnXZJbyRRtE57P2#ET=kP9uCo`@EczTKMfkRw#23FQWJ=SEkB?C;9qOce;
zhgBYI8al*SPmfwLLlov?dn4;O1<eKvt6aF52R9omtb<J4iRqjJ#+bo|>|<JG0KdmN
z14zh6<pMAmrPV>tT|Cf@12vrp_K}Zjko`5!USB53k=QK?5g$_+1jj70<-sV5>%{@f
ze}eSdOL#VzJ+b;sdhUXGs6n7wy?qY?Pq6|DiF*Km9p)<8@#&s}?Pl{qo+9Qku!Wm3
ztvP3A3FPLK0Nz-sLV|%{6<YCh^bI|DI)m6Ja|WQfZ3(u^j6;OM@?o&!`a^Ki7asCp
zchvL%2Yh;5U)75lv1Ta?j9A9J4)2R2;0v-#u`V$V3ED2hf*OK^G2ssG5$QgJ4q=b%
zltn*Bpa3n`h9CinRu<Pj1+^0+b(=AB8>*nq1WoDWg*p}SB-D+f@!a}Y*tZT|K-45)
zKIYraUFF+-OV*XzYue}=5_$sMjzgrqEzYh+IaW{E=*?r^&FOjpy!&vRcfS_r-Rnjo
z`vlD=W^JV^3?bBNE4qlyaTln7F{T3Z>hJTjaTN#?`Sin~tIV{PK8I|N@QbvRnX&y2
zHse8X_dp!r*$9pgVtyWu4*=^EmIOw2{xe3$Fh&Q9Zy4*$yD>AZOPJ{szrtqPD=W{(
zkh&EX?V$h;4dO`Kc?_5O;Fjzq!sN&dm6K1w%1-CPJ}9o^!1@BPn{A6k(o$b1%Iah_
zV|BW&O;)E245Wv7*cLf3c$*na80&8ZzzWB3D3=2KbBZziuMpty@mqOl_y`YmW-ud1
z7=Z;`L^5PO*$>;F6h#FC-O_CP98)Ex$uypPYE`=3eFWApkGl5W-w5wyyPM@x{1Vcs
zy>D!FcJ1zJZB1f;tPhd(=@<ZRd=@YO+~}<b40!auh)G;S-!kLfJZna~LSSqkW2IZr
ziR&};RRWi_i^V~p<h?;vBg9=b2rRj*2YDpDMP@pb`-@hN-X<Uo+L1+y>E7D4F+e8y
z&Yr>mhqn+gP?Ti{zQf^R(tcjU7aKGkC1RVLgbIBEL#6sEkM0Ly2KHU{g37Y6-Be($
zdp3x73CD_MSpn!p^s)h9m$IzyK&IG>75BIa?~?4U1+3tun-xF@iW^q}cN&y9nv_dH
zN-7&iY=`E+5>Mx<K;v&zK^-?n+OYNdYa#&p27U$vj96i&fPk2toCCk>DKONrpTHsX
z3MBKW+pnqnJiLqfT|PxFq+8oNz};#TIvtI0Jkuz4ffR8+o!oJh+>yTjzyafN4!Aqc
z0c%Dg<0}GQzHJbU;j~3}#QKw_G4g8{z3PeO2P4ZnR#0J$d?xU9-B>i~xsy8@NCIFI
zEwl-ttOwzc24Dhb1q}jl*i1j?Q5BUtR^_iz9V3EG0uWmsHTHKLmGb4kzz>P@1Im-M
zo4QocpYY|!GO(Y16_?n523sFvfdr05vwA?k__(+KJjMoj6*gW7$9fr%-TC-&MZ;yN
zr~NtZEiqikO38Sn=#)pDmGt|^C2*7E_%V{TGliu{)_pRT?3jGkr~rg+?D`+EmdCMF
zyJlSyOR-WSe$o&GD88MQ=KZf(1#p?f&5uUG(3-OVii2y4-3chlr5K7i7>YlhgTsaC
zT(C#S*W^Q;E4X1e1IMJ;_9}|a&|3_{u~IxPs>ON{!VI^Qiv<wd;sFGBg*n;SE8K#s
zjI%W8#j>5iX0QR<&B;h86a~67FTtV}n{Y@0m0#vzg~76={J>otcoXtZ;1HUJR35eE
zn)n9SD~9jfN%B#SLKxKLj*ha9@&^*Q_TG2VdtW-P;XvzE%xfEz-unU9guxeCdjN0^
zPF{GhNp|w)tYt4KFLNq!UUj#s-<<VasA-10t7@=Ty$AyyBusEeg+uGX+BJCZ@S#Nl
zV$_9jruV*CF9M_w=#N=+r=rW1ICfotbG6{o({>zvaLjhyY;-vsWtQYzKv~}V;mjS^
zH%wY|bGSSemFzT)k>(Gq76bZlDZPMfKjS$@%8a(&!481swCDLaI4C(o72)H4u%R<o
z+t8Sf#6uX_w04+v*@;l&rC;GFV^L<pKVv8ZBdrx-$HChfO)6F4NBEV@y{90By|YsT
z%VG0jPivCo+;JFQ-FgLgXv4LDoa?iDIZ%d}Qk_^WE0wIEf525?%U=n{dI5^hqZ4O<
z_hUa$E30T?xU*IqlE`O(a_j+^@6MhAlx1R+y($4r0@#dpXTzCDf}p#zmt#-OD`A3O
zi+MKg1oWjOmEw|mvY&*yA;JPCT8L4zqQnHgVhyI|xq%))s}k!&NgwtF)iEcaM1;&?
zl@B`sM{VGDvg8}Xmi^fpV?4(GDK}4`E3z{hD^++v{v){01?ylknlHg_pX^7o6wG3O
zb~ZSMiVW<x(!P8aYuHvBjPaUn4#vP$JlRd)v5FA|EL(^uQlv?pk7c4>2lptu8l2)g
z<P}0R==L&4Ob>UY^zdxd3^QAbXI5&0eaCuu40|P@hZNxHeu~q)qI!Uvk32Q6KC}r#
z3<(@U8abw^N!P^(g3th;J-+~TWLvXZ^#LSN_O1FiZ`FOaSOaOSm+*<BQFJ^1pT1aB
z;SVYJg9Rj#Un%f6tiPf>=^uCSmoqF<?D<y|qP?Q3GX9CFq^+^hAvk;6JLL~~jc)lv
zPI7f%u@Yx^qG?b}=g?l3KF_|W`-EGvU9b_r-{>KYq<Rk#ti7IWfIkRa7m{6+&=@fd
z+b?M`Am9~7(zjwCYJwR7;68c@0<eaDi>AUFGf^egs_nlbOp6&Tj#LmdAK&nqSIgr6
zAfZ`)+;iP<6e5p00wRyzIiIEKGq3>gJpzJnrN3SdzRwa%==ZLQJRZ=~myqoOZwLO&
z*cInb%$cXI=1icqG@tVyF;~rCT1)r}IhqzwzN>xCpW+HUX1K)pUv1T-97)DLY&851
zUTI&3Thdb)B3)nf6v{LcunID%ou4@i*3}-fuB>cbC)63a5PKZ2QpvOvWq}|ZHsF!~
z=>;zN2i63pSy2I{1=0wQl!W6%kn_Vi+gt{*S|tgjHB)JiBJR;A3cNqi=WasM*9OB+
z^XO5v@&-=IB<)XeBW0!&!ch`&bfCcdp8mi_B&l0f`&_!q5N|dmV-Mhjr+s*1i^`C^
zi`nlWrO#s;Cbt|IY(L2CTlK(?#<PEM<niAf)2gCo)d@*;GOT(_4p~t*7i&|lVORLj
zC50*2C6PnQI__yn@qAVr`*Vp|R1KkjlQPG&V<8=23ZWMGmT^BkbIAj9IPS&QlW;*`
ziMGLoD>cA{fB1?2;AWRwBJ?z*!J?wWa4F$R1k8!|P$bvK&!54CzkA>xt_S<|-}qzN
z8<5V4m$C73B^+j+fi%W6?3&yzQ6Cc@MlL>^%7iOX{wbt!`*m>Pc8PNEi_sFuSHqQ`
zR*q+n=W-8RxW7dGl~9iR5#UPirvl3JpiG1-7p_G8+n^lp*8p62%@XBzKshWe!e{$<
zoJ2V!(Kq46eei@e|0!PY)VUfQsC9Jo>@IOM?J99VT7ZJ|4~&h;Tr$xppYNu!siV16
zD4I&iLFr${C^4@t&4$GO63|yw*;u)5Eqw9sXj!{kXzp_LmGLEI>q{yV|3pX$gbxE7
tzbO0{UZ-VK0?YEJy-7`=F-`8YB#x^a|8fp;yj30xyW*A*FLv7Re*mi?QK0|;

literal 9136
zcmbta4OCNCp1+Ux@?L->1i>04i7$S%s0iUh1W}s=s5s)8*s5b!dq^Zf=<pGe$cJUz
zgn&UyJFzkyrghH-%gox<cIoQ0PLI<jfR@^{LpzRR9gY)Lhjlx)OF!4{ba(dufB67g
zJE!ODJLlcpd*8kP`|<z%fB*lza4oPPnZT0{uWtz<93hmUEO2c#R6w5Wk!Y7b{q!$>
z{$IcU`$vBJ%J={B%7=gc;`_;4T~!nz8VMmQ#e^g$Xh;IIy$4>-z2t~~oY}<6^Glwh
zx+Tj*;tVzO_#Rh!MS|g}WW$g=KfPG2*qoIAU~i>uOtYkXp0`h~e=5N;E`BMUFMFVu
zf0N38uv@VrYlSbbb9na={`@$|J;X=k=P#~I<SjkS(ZxgEkX-K`^rg?MI^37sJyaz(
zIT*jrFXxGF4`br}@}YjiFXV*LosjV4K`T$mS2Bsj_nc8oD1Y%r!j@?NUEH;tbb<V>
z3PN6m-^{P>yZu*qC>u%4qIL9$OW|$vaUEIS7C+ZI?k)0p+fHz8yw}cqi+Hbd*z1IR
zou{Lh>+pMvv|M|gr&Y}D*Kq;mh+8#1sC2oNBYO2m8r9^WblR=HY*tQ~RaZ^wn|k%N
zpz57L=@s~7R*^2{duH{BUU_9udDW#J(WtHrN-t=XS3n4*_1a9{jx5fl<vPUP)+}$4
z%iC7TwfVhvAID=G(xtj+R!<K~!+P~aGm5%6C=F5Ss~Y9_Z1*~^)8;KQdF{n0uxQw8
zS8)5=xsE!|W0joU&pAn$@RL)jtGsG5s03*!!LJ%|t0!iK*t~6Z^u80`R+qQP@3qM}
zm`?`@!Bk;TO6VR?jRaxs-`d^NQR#Kqggu;qC3xEg?z(kkM0IUY3L7;-sl%{KQ_62l
z#>I8Cb1kqT1KfVGw`C_6UT|P)!39cn*{r^4Rvn0MKE=c4kC>I0g)O?~#$CEOrMfXF
z9UD}Kg360}H7Mmh{i2IhfOf&Ud|pQux4+KQ;_~h%;X&o3Uj0cB_8D}ferHg56IM3}
zDpr4h8?JV(R&brYbg9XMnE+k1lXe8W9X_sTr>C`!>xB9NuT94}gbb(>>N^Ht?a)%l
z48$^idQERM52!1F_5p6)S=t4t0|{CH8|{Fduk+eaU-51KK+yQ~lq%#_Ukxa)Orh3@
zL(H|pD5QuVK~$%>7^6-FFejS;?`X4WT_yvMzlAXA(%Yg^zo$sdwYyNMI0m4902fwl
z^Aw+;*SI`Vt5McCA=^JAYxK!lb=-av=bT`tT^vlOh3DEQ*pFP?egK7^bMVoxr{$d8
z#VyoG4w0>l>8V`F^R5R7!C@m$olCQw&d?FylISDV4t=0xh$~hme(K=1ANsNgVd7QL
z=D26$*W~;z%a{Zd7Hg!VCC@kM&18<~g{I2+vLDk#7i&W%NZE>Z9}pgHi14^r#e;{s
zQz;^k)sRBh80$X10;c#d50yC8eDy$jMrxI>FY(@u7nrhVDs;|M`VR3kJw|q!QAWs1
zu*V0WU4hu89Gg<src>*C%Zj^4`wRkV9Rn?rX_E4xT=tnuRv<B`!DawhwOWzT%##_S
z*N>O2@1xg;+WVX~?lCb3W@EE)`)zb<yVu5hGeW7dTRz#8Hl<0Ma(zZNW0V!h$5hwA
z6g8?5v$|G$sPvqtbfT=}48880XI(d48k$LOHF1yCack-TN!%J20^Mc;b#tw^MIg4#
z<*f!oQh4nH-i`rx_D3_akHWIg1F~CMde8Wv^2VSNa1ZIES$R>T9CHKju$O&hCF5l!
z144Rsw79>l7;K?`G#3W_s;l%8T{=7}d86KI+v&C2JkC0<-Q;yDyiUJ2<DG|6J|Zcf
z7-ctnvg^8(DPDF9R>5Zh0imV6r%_J2)stc6jVaX!l)6^2wRpH}?J-Yj$hb7R5R<p9
zoogT1TJ@PP1$RLGs9@U~70~MeN{tiNsAkOUwjNJ$XtZ>=Y&~qqS0n3gl$G{EakTGz
z60FqQ2J->p&f@F??%mhrvReV!pNz6kwM&BU>D4!;7Jx-vg9%h-ln#5=pYddNj~4fp
zm4rsuoeh?ZkHQ+)g(}aqfW4Wx7J-RK2LR=tK>v1iC12Jn$w;*4SMp2TeMgSGTke-<
zS=Qy{8=mxOp3B-=LvLQPJh6*wHYRT@khrt?%g~KHRKA(tVYNHzo14np%=X%N!MbPP
zUVc+kZF8)qt)|XwuXfb$w;DH<@m1DVYlGQtH+ML4YI3(bKt!(9V(G};Yi?++cjP+E
zZL1tL_IjH$*J8Cfa_g*So5N|fuYwP`)^>BFt-<Qh+aTp@8q7_5`PRrJ_`JLvZ4T&0
zs9lwpr!By8eoj&T^4zNWJ$AFbBexs}Z?;+Oxn<3bjpimxReh6nTXS=RBNx`=$lYSD
z`Tj#Ya~zf*=I(RYbL*RG8unSNxsDD;Znd++W`&>nCTCG$wKJzKnrUc;IS2_<z`7c&
zP4)lZ@nU1`iw_pd&5pLO$x*+z$!g)DjbmRUSt34~-=$l%M4VR8rCkjr_*q}Jh5A$j
z%A&y736P4oK=P38ZEcld^{7^QSu$F&tw6FfPr8j<phy8JV8(SKA0gV`P`+S7l8&mn
zM4n#Es<kZk)^4TO!H<Oig^_^MooA$=9C8qg+?`+}X{%kLe+Y7Zf!#t{pFU$KSk+BV
zPynjLi@i_0{o>m{|L}=ZPreX3-?!>kLsS3a-xj_2Ru9(qRNV?$Pc`+E%|db66Q@E?
zKuJQLhiL;<k>n(M7T7+wf2VDrY(1Fpa9PR3XxFszLc{@sJJ+ag3O03*az>Z(iCp%%
zF6Ab97Z?)f&V|+uc}kCg(bMbwo^?O~zEPZ~nJ45h{H8GvWFwg(#WD|&@4*lGSWC!a
z_+7kl+_#l2XQYs?X$BS7H#xM`c54lkPYzwLp~EY0`hkke^9iBJz;>o_CgY7$i*26Y
z^w!RIXLj}$oD_${WiLNmLAZZB-oTIhCF3qhQEGyg3!E*lqo-G1<cX{0&;<MT4}5My
zuFo5k9{U&GLy>#MzSVm1i-`so&b1&laKkrJRjw@=(xy>WvgM(2a<nXIlpXWQ1HD1Y
z#VZs87#*hk36lFK(4%T=jOpeHmS`JvVlmaHP!e&M+uehobpHzp{XdYT6tERjY$G9~
zY`HBiN+F244&P@*JqDt56kovhw49~DF^%`>&DtjDC^gtvs67I;p?t;w!zwmrlE5(4
zvXp^>@;nr>^?7FEONBn}VjCgbNPdlxpQj``u1g+Lr1#Ps%1&bgwz3IV5L#`6R;ML&
zDt^2!tU)WKps*>GBihZzDg`;ifQ;;Cm4vKv!G~nUILs;mMtG^;4VA2147HDEKy7sC
zMs^IxN?rmI8g%6pircJ-iA$$IT%jK3%BHb89h@H!54#u_s$O`^{CCAmH-osn125Gv
zym)Ssggfw3A>bwVuz;7N0$!dK@KXJAzzZ+E$V=mR@l1Q(i{d53{UnB$l<x_6aj(|9
zzJ?b@z)R|P#*1#xcfgB?;l2Z2bO&O1sc-@^<P>NoH7|k}E#Rf1e-<z0bMaCc$BPm1
zl2;PLOVuo1j(#04dE004a&#_Uw$0)NF}L#=;>8V`-x0@)`DcKafC#a1c@{2IegrP}
z%!SL2JK<uQ3zxg%#S1t{V=C{;FH7NDlwat?xp;wmgj@b_*+k!gm6lQDmLF%<&JSjG
z9?J-=NGQJjs%1y&Sn&4`uRK_CmR_g$skkxFxhsPq+MLv@{x4rHloQkL#b@20w$u~i
zdWTN5h>vKN44!otk^VIktSd2L+ZK7k54+^MVc5UHGp;x}ESTk)5HJMtOv59B!E2O^
zc8`tlV)nx4e}OObmyo1<3d#Mjxqn!ACT@!@Um^o(F&X^|8x^pk1;3(*BvbCz6X1bt
zJ&3jSW)dPo>sEdN<U<4bh~D@$v|1ykGNASt)N0@26+jq4DL~7Dl;GS1DxQy>9!cZK
zgqvpoY(E{Nh>?tUQ`$*+p$SAgjiB@FQJwHHAPihpMxdqlO`x%PN?{6lHO6)tq%A{f
zyA|gsvO63A84bE@iUJBc%?KkmBYSq!sewNI$5Jqj)65&)lum}TRWMM_gr-y;_=gCe
zyexTkDTkX4kC}(N4fy>wjI4lf5sZv6DUhG#6mu<vMNyn&de$mvLg|*$L`z%`S4^;r
zG9;%D2c#SF6#`T&uD1~?7x|xUXIf@{;{N5H0nfS#kCe&i*Do9j-fJK?Nd!4HMi!K`
zxx1+DwY*B2A{Uk!GK>GH7zz@yHf5<#Q+}|od$9+>lOZ`nnYzfsY2D#xcm{m+ckxkI
z{u7mb1CqF7=?f|V7ohkA16jgyq|0P7y@n0?Ao;5flTn}nwk1MM3>SB0pCf#DOk%F=
zyy7b~NdY{*V2pr78CjsBLbQLM`%{3-B+pm?13n515&Y;`4`3|=nZfEqupnP;Ww*p#
zRHSw;g!-v;a2{`I<p6@MY$D)km<kr6%j>7^MYm!TAaWl3BpXMOMGN@73ySpYs9-`<
zIuvjW=N=Jo1E=lRLwPvZP08i-x8mr+92_CmFqUymi-{Wo8H{I^$FP(%#$AG-Virq|
zX1mjB!LX*z+)&$Q?ug=QmuL0Pxws0mi!zm`4~L~2iXglJ3Tg_6R&*8Lo+QsAu7d9T
zlj7;{Q4cWEMDRZD52qIUJwKKWv>Xbvp;uU|oIuQD^GxsZL`W&5&+KgRL5Nl*_X7c$
z(z<z^_qXH7ALpQl1r8E$bO{jxdv=Oi2p$D+WQgO)5{6F^92v0{;OHf`H4IdefX11r
zM9Y=x6TlsbGP9v@TH;1G&|r&5I%q&f$V^AyBG@zo-Fh;MTd<oOyY*yNLLnNcG=+g7
zCeUep%=RI03=@EWbdqld#$r+wAh}r!^kN}<F8JH&2V}(b>frwFM4G2D^cki;W>ER(
z^n#Z`^hE8!=l*Y)eaeTp8k~``*g?o81jZOu#1Wgm5G!p^2|Sc02Odi0-T~gyBb@EN
z378cPv(j)<RV?BXYGaIOsfA(3-4zIDBeJQ6dlR~E$L<atyN{4^jE+M3g@Btrg#rV~
zr&x^iLhgs4Q-jVTL{knMd>6=*n6d9Z9otHX6Z>AG7G9x<lNY10aC=P<?=6JQtWd!z
zosfDY*nKt*THnV2>t52UpmlVl1g;!Ly5z1AMsn$OxCJUDw2dgmgrTULbA$cFLN^kL
z-TZgNZjTA}QE^vayewuLz~gwr*>ANsR}1IVxG(mUT$yVNz_E)W9J?XHv7IJ%<-uZb
z!B@1z>SLc3Q$89z?-}aT5A|_(`~@#%kZGI3ot=pMo9leKgYu00d52TjtHgLfD|qDc
zE%L5MyW~637J?Y}N8&h)`vKph`WP;DzK)3SLGo7~6T~;SOW+ZWBIb$@{s~?2s9-Rk
zKn`8;V?GS|qv+cCYpm^sBrYY$9TB9YrZZYIXcWApXb}${7QkF%oT1|0c#%yoA%hN0
zXi=SDLJ1hOcWS|egn<8DP84&<Kk|X6jbK2i1<0pnBji7$AfVH3)<VYvT4*zY>>K3F
zGc2(M69n5h0=5yKiUbB)TVwnRX%Q)L4ktd%%=N9Ee?#Z@#dMz3E&9zJI<Ky^H#aud
z*2Z+7CR!^Oky-y5X8)K4x(`cV+X}j;l%3B7UQpbCt0EIk#T@Fipyoj5@rXlZ*3@m-
z8gZyynP-CcCDntcjz?n;m;+L>J&A521HA5cjAr;=aZq$O-P3Vy+x<FfP0+m-RR_A)
zB$<HQz#7GIA9<HJt0(I$nhI=v93mHfhY;}y5Q#-=#{(SbTZnM-lF&Db&_<v0qju2X
z@{;7>@oXNs4=g$_NrvH+M+ZPTpM}~HLNT8KqHmoD>|C^bDe$C9jGQ6V!Yr9&3M3AN
z!P|!BNx-I;OQ4Mt5!PoA0j+&g^B^0z7&Jd%fR%#g(O>Lh{L+^tPlGd#JZ7GdGmuSV
zHs00NbKqMfrs@{WgM4j$1B6o5a353+S1HxDX5i6C{QXeRTH{>3gUzpu*!+%&&7U%{
zrw<d^Ydb1y=j)Z7FBo4?OzTp<Fpc`y2nG0~6!5$uP669A5ejJJe{>Qlpl>s?#<pQc
zB`n1myNx@aL^qNXI~8?wfT51xE7rqRz^O!ojrs;AV)p=yJMJ5QAjDY0;XM|gpGd&i
z`ws5deGc&>SbYpXgGsGmPuge%|4YO~*&UcT8Hh;f5<>LowZl(8f_5o_r;QCaY`7ud
zkYQ(|<fM2kf64_RkZ>LhCQSkoqZkS%U4=rn$Ao0FQUc&}VmN=sFfWRsij{?N3`J^V
zHwJ!y;JZn4BKnm}0VZSE{p<)hQ(Y23uxDkqJqAIc79p655PUHVmjt1Ca=`A&bZGM#
zb_^uo8B>bb&DMdm2zDd2I4-F`dl*JW+s#J~1y#{Q0YrSM$r$l%!X~HWEZD<>-N0U;
zfNi??>1KEY=uI~tr<R?C#{_8nuUgn)W^4|h?S(%&0!ZO8^Mw2d{H8IR?uzRT@J+z=
zyfOM9&kzK2zNI0rA^*`Ro=^6yKQR~2g!|(vz%ws<Z5QC#t?Yco2zWNhHtfy<T2pnN
zH9~l|_O@+GvP06wCp|a3CqO@#)l(szfuZ`TEJ#UaZ{fJ7u+p=oo7|+}%o%ol`KTr(
z0ol(s!B(#t5^gCd*<|=+PoV<Oq5=13?;94vm10inzXiT*(twkO#?BdbQO*!7HGa$(
z>FFvV{W<9&%HL#$o4{Wt(>CD8-BEr7lNe4k_~7sg0t!+m?(~xpyNHI8g8OXHDUxGH
zhr##p)Ic!t#BRY>*+9#13pN-xq`$*}E9G@a?!N*F2AP+-7J|Y-kL7V9t~-MbZlf#{
zwgMvFn%o9|p^h5T!6Lzs1f%={n}V8O4n(8?or80W8qzbj;A@Itma*X`4S2*5?(c-N
z1mL_Sxe}0-h{$@y1<>%Jt87VzdySYOwIn|ykg*HNcolML)X_U<XDav&n5jECO@+Qd
z4{q2Tp<z)@mJ<R#q~UPa4zK|++CWY_M1gSCCph{X8x&4Uy3x^}H9~kPr{C<;A4z@^
zLb+u)vtRM=Q{*!t*o)MP+%W$$DD#HF8b6ii6hjaPA%&U98Cb=U<i}w$q6BCPacsIA
zt!lFo#Jy^SXi#Y4PTpfg&ma<F0*z?StkZE$%o`8_C6B@mZ4q{euwc&%ED_t=K5KiE
zBRs6^9$Z;&7U&&q?;J)RV0-vyyj@Hfe9EKz`@yHDq(h}dlLvba^~oV3?sjMO(VO~v
z>W|&mHFW5oPbI%~=7~R_OOcG|Bo|x~7#f}yo(MPP`7-(9ZgNzVHB;}RPjZ#I$6cZe
ziFM(#F79zjukVU0@pYNd0TL_RIc|sFd365?j9>BXg%^ATse%`20763H!C#D1E2G@-
zB;>)Q$O(AG@PbJQPwYDuusuG*@Wuwkb_iMmmr<`lJ{4Z9lSk{t*@R$hlmajQaTfc<
z+Fye_%3KLA?oF)zCgibyA-vcxR(~7v^WiOnH+@dM6xM+M=<x%1QC_UQ0_stY8Q!^a
zvY<W<>TK|$|BkgUg?fwuy5Pk<i`7GxJOX>W4Sr#7kK?}1o_*oa+tAS3m}A+qH^%~b
zGgQpI=&z2K;+bmU?q#+(dwiZfHq7RPVDg(WMueRsf3|8bE~+jnTxG_;YprTD*EBoY
z^Rzj6t8=umKb6hS0#E7HU!U>UKF=x6&Qh54oG-JpuAVd5Iav&XtG_vMAxO%%;I7{J
F{2!GHdU^l=

diff --git a/heapster-saw/examples/arrays.c b/heapster-saw/examples/arrays.c
index eee14010ad..da3bb6d47c 100644
--- a/heapster-saw/examples/arrays.c
+++ b/heapster-saw/examples/arrays.c
@@ -91,3 +91,14 @@ uint64_t sum_2d (int64_t **arr, uint64_t l1, uint64_t l2) {
   }
   return sum;
 }
+
+/* Finds the sum of the elements of an array by incrementing the given pointer
+   instead of using a for loop over an index */
+uint64_t sum_inc_ptr(const uint8_t *arr, size_t len) {
+  uint64_t sum = 0;
+  while (len--) {
+    sum += arr[0];
+    arr += 1;
+  }
+  return sum;
+}
diff --git a/heapster-saw/examples/arrays.saw b/heapster-saw/examples/arrays.saw
index 1a12837847..b7b1848938 100644
--- a/heapster-saw/examples/arrays.saw
+++ b/heapster-saw/examples/arrays.saw
@@ -25,4 +25,6 @@ heapster_typecheck_fun env "filter_and_sum_pos" "(len:bv 64).arg0:int64array<len
 
 heapster_typecheck_fun env "sum_2d" "(l1:bv 64,l2:bv 64).arg0:array(0,<l1,*8,[(W,0) |-> array(0,<l2,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))])]), arg1:eq(llvmword(l1)), arg2:eq(llvmword(l2)) -o arg0:array(0,<l1,*8,[(W,0) |-> array(0,<l2,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))])]), arg1:true, arg2:true, ret:int64<>";
 
+heapster_typecheck_fun env "sum_inc_ptr" "(len:bv 64).arg0:array(0,<len,*1,[(W,0,8) |-> int8<>]), arg1:eq(llvmword(len)) -o arg0:array(0,<len,*1,[(W,0,8) |-> int8<>]), arg1:true, ret:int64<>";
+
 heapster_export_coq env "arrays_gen.v";
diff --git a/heapster-saw/examples/arrays_proofs.v b/heapster-saw/examples/arrays_proofs.v
index 6f26a35f70..b1e5f1dd2e 100644
--- a/heapster-saw/examples/arrays_proofs.v
+++ b/heapster-saw/examples/arrays_proofs.v
@@ -137,3 +137,74 @@ Admitted.
 (*   * apply isBvslt_to_isBvsle_suc; assumption. *)
 (*   * apply isBvult_to_isBvslt_pos; assumption. *)
 (* Qed. *)
+
+
+Definition sum_inc_ptr_invar (len0 idx len : bitvector 64) :=
+  isBvule 64 idx len0 /\ len = bvSub 64 len0 idx.
+
+Lemma no_errors_sum_inc_ptr : refinesFun sum_inc_ptr (fun len arr => noErrorsSpec).
+Proof.
+  unfold sum_inc_ptr, sum_inc_ptr__tuple_fun.
+  prove_refinement_match_letRecM_l.
+  - exact (fun len0 idx len sum arr _ _ _ => assumingM (sum_inc_ptr_invar len0 idx len) noErrorsSpec).
+  unfold noErrorsSpec, sum_inc_ptr_invar.
+  time "no_errors_sum_inc_ptr" prove_refinement.
+  all: try assumption.
+  - assert (isBvult 64 a2 a1).
+    + apply isBvule_to_isBvult_or_eq in e_assuming.
+      destruct e_assuming; [assumption |].
+      apply bvEq_bvSub_r in H.
+      symmetry in H; contradiction.
+    + rewrite H in e_maybe; discriminate e_maybe.
+  - apply isBvult_to_isBvule_suc; assumption.
+  - repeat rewrite bvSub_eq_bvAdd_neg.
+    rewrite bvAdd_assoc; f_equal.
+    rewrite bvNeg_bvAdd_distrib; reflexivity.
+  - apply isBvule_zero_n.
+  - symmetry; apply bvSub_n_zero.
+Qed.
+
+
+Definition sum_inc_ptr_spec len : BVVec 64 len (bitvector 8) -> bitvector 64 :=
+  foldr _ _ _ (fun a b => bvAdd 64 b (bvUExt 56 8 a)) (intToBv 64 0).
+
+Definition sum_inc_ptr_letRec_spec len0 idx len (sum : bitvector 64) arr (_ _ _ : unit) :=
+  forallM (fun (pf : isBvule 64 idx len0) =>
+  assumingM (len = bvSub 64 len0 idx)
+            (returnM (arr, bvAdd 64 sum (sum_inc_ptr_spec (bvSub 64 len0 idx)
+                                                     (dropBVVec _ _ _ idx pf arr))))).
+
+Lemma sum_inc_ptr_spec_ref :
+  refinesFun sum_inc_ptr (fun len arr => returnM (arr, sum_inc_ptr_spec len arr)).
+Proof.
+  unfold sum_inc_ptr, sum_inc_ptr__tuple_fun.
+  prove_refinement_match_letRecM_l.
+  - exact sum_inc_ptr_letRec_spec.
+  unfold noErrorsSpec, sum_inc_ptr_letRec_spec, sum_inc_ptr_spec.
+  time "sum_inc_ptr_spec_ref" prove_refinement.
+  (* Why didn't prove_refinement do this? *)
+  3: prove_refinement_eauto; [| apply refinesM_returnM ].
+  7: prove_refinement_eauto; [| apply refinesM_returnM ].
+  (* same as no_errors_sum_inc_ptr *)
+  - assert (isBvult 64 a2 a1).
+    + apply isBvule_to_isBvult_or_eq in e_forall.
+      destruct e_forall; [assumption |].
+      apply bvEq_bvSub_r in H.
+      symmetry in H; contradiction.
+    + rewrite H in e_maybe; discriminate e_maybe.
+  - apply isBvult_to_isBvule_suc; assumption.
+  - repeat rewrite bvSub_eq_bvAdd_neg.
+    rewrite bvAdd_assoc; f_equal.
+    rewrite bvNeg_bvAdd_distrib; reflexivity.
+  (* unique to this proof *)
+  - admit.
+  - repeat f_equal.
+    admit.
+  (* same as no_errors_sum_inc_ptr *)
+  - apply isBvule_zero_n.
+  - symmetry; apply bvSub_n_zero.
+  (* unique to this proof *)
+  - rewrite bvAdd_id_l.
+    repeat f_equal.
+    admit.
+Admitted.
diff --git a/heapster-saw/examples/sha512.bc b/heapster-saw/examples/sha512.bc
deleted file mode 100644
index a842697c86310e7ad92adc1644e1b1ad40f595d6..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 5760
zcmc&Ye{d7mnQy)Fu58QF8ViuHq^vOUi4^RW48mahkSqfxI7ARG2UG5>wI#5@Kh~14
zEt5-DmSGL&%gB_pZp+O`sgrYm+>BBfj@;!BSvHQ3a~VT(oJ&27Jp2e{2z45Ir4#OQ
z-&_9(y*B;tdOLb=-}}Dreee7I-s)CzWe$Qz3(dO%AsQi~%9Xse5dbho^(t=7Ti<;5
zo!|V&8!bP*@bc&X^vTb+uCFF+nSe8^5Mp4ElVL^~Fo)%c4i^qMClos=#<uwk(W`ns
zQ>iy8{<dD!Zp)}TlT$Us*tBIz-L7og-o6@P%v@N#OzLNxXEMAK%J;OaYkMF2uY_%H
zukHoQ3sLK9iGu^|<q6<>ibZHSylty%vRLm4#Wz+D^+I>MHy+h4t3BPH(>qkl91JL8
z+z!!gAsKO8nRGbJr>!S<=ZUcmJD9U?D~T1>j1!jKs5_wWM9G0ME!un<SfV{TgvQ}r
z@bu4~d;t$3pezgNAXB1F>WtDMi_{*YJ0>K1RO%e2J6XxkN_JKXCZr&Y8zZ4UIuw)a
z9NpCz=}^+$4mxQ_g^l;(1~F_%IZcnu#+i8Ty|C#9Z<ykZH$A5NPSdRs<JEZXG@y7R
z>M>mBO(~~gI&Qcrno?%tbUb(5Y?uZn1Sbg|DP*BVjt(iM4vS<LrOq0<GbZ_?G>d6a
zkMRm`x);w)J55)3%<4)!cakvOG#e(qT;3=J1<CG_{AHM-Jt6sZbaxjWYK$DOq5UyB
zh|-9inKj;IjWZ(#;D$NGjH$3`>Pseq)Y(WL8<sjm$sUsgh6Z^;Xc9z)O$m8<(wG_n
z-M?~qBvc~>1lfjDpn}vn_y<jgQpQ{HTrgCMFr~ptvxeUjMx;YsbUPSiknUDW?fdEU
z%GYOCjuXZkyy-q~e0|CI1PjJb@rE0+iEf3lmF~|P@5FP*;-<+F!xg6qoO0dy+!Z28
zilA3i3Rvjw#z?y;b)$6LFyl1+Y6R>IJ~Ca68}5U4ad5He0XDcv+^C~p>m$oO5j;qe
z_WfiaDTSi6eSf5*k$w%}gOcE&1M&b|3GmP$=nj<fU~q8|BRBOej3Mea1AUUNxI~H&
zb-;mxU?T%y`9?{={#r8o1KH#EW{s0!)6Jw|dKP;P1(b9L?1Jo;6pm_*sBk-s=x-8)
z{=Z@R2D*u&;-6283=u^+4!R&(g_e1UALRBr(QAo#Sr6;5Yx@`lfzVFK4+Z2$evhY$
zt!1gVxgsSE37@|Klr4XfSsshnm2{Vgg8|D1Su=<YQYJ*ohRIEdNbb9Cb<32xdrsYg
zG=6~w=>sg?&C&iTYL2Bl8F?%N=LsMjI~;VkhYn6rzkptzws_QCi0)=+zeu;F)m<^V
z-LtR|h+DXvc9!mn<)xy1K@@8FJQdC6C?ppqoa6|Ry1n`-LLuU@{CJS-g|F>GNVy0=
zDo@R?DLtu3E<rHOzB$wH@QF^d?h9`t#O5gEwKmfrqtC02_GcCC7+1JXZ*%y6<P51!
z-*qc}Zm`pPV86cuj-^V`Fg9yAq$Mi*TxGqZ{Z(=V2L{_!_mJijM*Ub+m#V5vkUtP)
zhqz3cEK)E@R!+Do`^n15uKu7vA6L?lLV`ed3uH%^B(RcxGEe<5s-EREt(@leoO;f!
zE@j4yw;(Oe#uRTl#GNYtAW}Z%+I)em_#jfzOO{X0X*)dh@kV-6BSaOwNyI@fc)*2p
z$CFH8+bK$QkW@O!KPZI;!|NW+sUM})zfP(ja%BBP+;AsufE<8+hBsU>8^*#=gQy!(
z*X9Y==0Ul?G+K7nRR(!+cC-XGecDt05m}xXRejhb3Hv3#5D7NYT^=c@lY%ixfAtm3
zBc%D2TYV?0zU|P=vg(JR1#5v~gtP9t*)S6}&7=)?W{nRB(;?lSvV?2Pxk&k>d(DC(
z9;vg7?i$=v`#7q>7BC%=^W1ENQu{h#!UCI(b3C>0M5JtTv^?Re1cN+HRorov_rY|u
z|8h2HDs_T9P{b{?e=vOTHlu!+RNr;0KjR8Vt~*V4W>-RX-2wq>^yP_2<%LK=?`T=S
zYxCr2#ifzW6QiJG#bnKecE~*s-Hxl0r2qN2`k_bjNg85ZbC=WHWi|ilR<|<h+ngGv
zpQWi^q}6xa>L;9Q_NEyh8*_v#Iiwy6u?X2=;5XH<u0EAM%Wtb;3&Z^b1J|l!jKy1F
zwN<?tHGi**|D4)YxHjv@bZa{2#jWg$t%jd$)jgT3P9gM4^)B{RpFhyl)>_@k`wuNm
zeD%i;vpZW4wJkzA8yb0kU7)Gk=icdJYkeKQ=0GFA(P}GhDEW&3uqbKagTWBrz<0E@
z`bvPvxwpC`z;~_>H29l@U`eBo7Xm?_e?7oTd|iBt(CiC11?bs^X1?_>+c7T(3oN-}
zj<v|p^;R1Pv*J=)v2AS$CU0usgCK68WPd}O*H_F7LW!%bHRx*%21=^2SZ#vOU*c}&
zgNNGuErF7k_=cBX*<UOy0G^=%<(JR_@6iQ982#VwQ*tceFKKFRXg=okmDB}8f-g`~
zcdV&3Xx~s5EN)yJHMfCH<nCB&py_a{&&vYM|C4BCi;}@$NgNyze?oZzA+Xbexo{j}
zk>=ljLLr(;%j^qM6gSq@d3k?lQ>&a7b-~|rR#R*1u@+QxX#U9HdYI*f$}`p;##pG#
zv-L2~7b*vAXP0wc5eO7MnTlZ1Dch)+`7>3dsJT=%o%{(G9J7zcmQOn}JqE;)oJ&;g
zLvS(w%z*S8V#tuJ&h=Oi&k>FCdUCl)qGSc_pqLC6qbiTg5l3ZI{zg#`g9NS}sP-eI
zLC8@c!Xbn>H&Klcu+5)myKjN*9wC|IFko`bX=mFU;l~s7)6DT>=)-oyhv5^tzA*k>
zBE0X1*A7Pt#GWm~ku8_P1%nwC!;yYPk)_aX{}=nWE^hkqmW#HPr56+D-`|t{OESVS
zk%QCI4{siv7`u9K{K59Df8HlguTNZ=xxYQ@3PRt9vk`xL<YfCTaOTk6`-MSQB^(_I
z*XF6wo_mJz`AZ;NDb2?FaxGu6;kHNpu^WyE%^iGDXg+qUA1BhV7EZ8XeEkM~*BFH0
z^hfk$#ZaXD92`PqWh_zw2U2tt+lFTm>VS8?qIw;W%GU(Nc61~L7oATz__hJq>Kzl&
zJ=xVH{x%3SK`G+`;Aw<@I22JmKy0L5lZ^<+7%AG2cwn1Ad&TOnove65x~I9JaKYqA
zQ5AZObl*~TdIp@c6oLA8^_E|nhz*hi8h<`zoF??TCWOSRWR_PsU@nYDiE{Lj%|nY>
zDaA|7xyGJ!4Jys68j7ZB70lWpE}y8*UaKl#$SPDw(Wu8G)SQQ#+}1R{&mr86_B;28
za8XSr2(v-K)eDGKQqr2wG3pcOG->FzPU^ImSIvMtIs;PnjF>Our5;Q~;_n|#DRp85
z(6Ce3iSnuBIw#lQW=D+(Wr?u1CO{)0OaLN5I28(xN2*QA8XaIJ1R8Pw#;Qho3CBsc
zl-ia`6X-FkxB_#hGM{o#Y>^68p>JC)XA~Ng&LE0ZB2QLjDLpB~Zjb6CRn9qtx|xi_
zDWtQr=R^bq2YNi?F~`Yr_!z}2SKU=3PedPiTmJ~$RuBFlp?zJER9{qmyBGT&KRk=j
zZg}S_oL~AkyXS@yVA#K_;Vt`DJq8ho(9Zz&%FdVEwbnY<-UIG^FV{7<@!q;)P_FBJ
zLeTH`1sDBJp3<yY^82=24-PZ=S$9N)?OBZj2iP<_6gD-lR(LdG`zg2@JE$`z1>%bH
z=F;j3&x;^)k@6d*P64i#&-%F8q0A%}9P{Y}c8mi%#`Vhu$0+D7wCMec_W-zc5))0y
zF79_)t$^0|{k_#POlXiuIl+E;WG`}Z9+R0nokfb2<B;m~iz6hO2CEKJ6-X4Z0dR%*
zx+1NX6@iXt5n2X%<SS}q`(Ya^j(8L?*0LfqoIzk4?f{r<!&QB9{rKxV<p_Y#{FR}u
zzPYX8C=|~iU)SdM`tZF1a>yD8@<AWJ&)NhB-BK=*Z)(eyY<gf@g7zZn+K*PJNn1^%
z{?)w4gnr0r{h{)ysJhOoURA}C+5ecRS7!cY*NJVp5HV<ou;85wln(8TM{Uo`;IfmK
zs;9|vmfWq)z)5)AGeCSyW#A;Nyfh(xHzFsYX@<}TAqi#T3N})l3!V!gZ;bXJEe1v^
zSn_4~<6$bqhE-;pcg?<4+BqUN9TPPulOns(aG7q3Oe*5vDN^QdbP7Mn>S=)7J=){p
z!LPe<?)EO_?qoF@sLC$Qb6{|_cJ24LW`|C_=<e|Mu_xWwlab#-2YHzJ8|pYhqg3@Z
zCfPSah^)@A{{co_fNtv`bYDPf3hyK!@0uNqYKc`Gv*Lb-6`cdD7V3uQAMkoPygZl^
z>c%zeGw63QdJJQh(3Q`i-@)h)o<+|Z0exOE((fdwQ3&ZgTqrzK4+(TInd~L7o&-^=
zL!-GF`4s4-Q(<~lDi2_1%WMtqK4*$XQ(>kopF)`;rlhKuG0A?XnWCRVXnhax^E#;4
zunL(_`l4O1my^nV4%fOkRG|iUlmHfv99(zwS|GfDY&<&1&Tqd#-d>RfTMZKWIk_zT
zd%u&X4ky8O^=@1!v-AomeR>P59i<dnygN@RVfSrVo5OBc<yK7e5<(bP#ROr^l#5>h
zvsbSI+5xH-q**rtq6~$vgD86qAj+!h*MVJb_#~*kZB;Ey&Z~O!fM1jQF@d6)6aCIO
z^&xC>0BgNciOXpLv)=(*ARpfMsPGi_rJmXMJ$c{BWm+&~f%XlE{>xU_bL1Y4#BhN)
zudpzJfZurqxORX#0sKRlSu67?Y^uW+zvLW|Eq)GHYXYoxqM!^kU&+i%;F2YHD-4KC
z0}F^sC9z8O%a~p+`jgARTJw(F(%_zOLJTqt3CAbY5r^iYD#ZTR$TxZI8aGZ%)XvWT
zhhS4Pt9#M=l!ZAiD#ExLBjkhs5jVkm8F@B=ODC>H_&S9PYb`Vk+Yb#t_>KR2oWc`$
znxU<Nb`l!qwpff8@c@$P@%v3^i{}HTgDCz2twHE580SI5FlGU+T!+xRFvh&`|C;zx
zwMd_YF@~2wTZCi!n=l7MqZ(+C155NUM1Q41aPY}G{ub*qf1hY>?r16Y)*mkR`rt#z
z@B7LVNG5FYwKNE!Vu5Qao9~+J8~%8$o&U<}Dzn$wH>`(`sAk{#7QUe^&}HR{ts9H&
giywFMrJ1Yy-}2Obr9ktfe@LRbKQ0nB#xu|V04RZKiU0rr

diff --git a/heapster-saw/examples/sha512.c b/heapster-saw/examples/sha512.c
deleted file mode 100644
index ccf8e32c1b..0000000000
--- a/heapster-saw/examples/sha512.c
+++ /dev/null
@@ -1,231 +0,0 @@
-#include <stdlib.h>
-#include <stdint.h>
-#include <string.h>
-
-uint64_t simpl0(const uint8_t *in, size_t num) {
-  uint64_t sum = 0;
-  
-  while (num--) {
-    sum += in[0];
-    in += 1;
-  }
-  
-  return sum;
-}
-
-// First simplication of sha512_block_data_order
-
-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) T1 += a;
-
-#define SIMPL1_ROUND_02_10(i, j, a) T1 += a;
-
-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;
-  }
-}
\ No newline at end of file
diff --git a/heapster-saw/examples/sha512.saw b/heapster-saw/examples/sha512.saw
deleted file mode 100644
index 362d9f95f6..0000000000
--- a/heapster-saw/examples/sha512.saw
+++ /dev/null
@@ -1,15 +0,0 @@
-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_typecheck_fun env "simpl0" "(num:bv 64).arg0:array(0,<num,*1,[(W,0,8) |-> int8<>]), arg1:eq(llvmword(num)) -o arg0:array(0,<num,*1,[(W,0,8) |-> int8<>]), arg1:true, ret:int64<>";
-
-// heapster_assume_fun env "SIMPL1_CRYPTO_load_u64_be" "(rw:rwmodality, l1:lifetime, l2:lifetime, b:llvmblock 64).arg0:[l2]memblock(rw,0,8,eqsh(b)) -o arg0:[l2]memblock(rw,0,8,eqsh(b)), ret:[l1]memblock(W,0,8,eqsh(b))" "\\ (_:#()) -> returnM (#() * #() * #()) ((),(),())";
-
-// heapster_typecheck_fun env "sha512_block_data_order_simpl1" "(num:bv 64).arg0:array(0,<1,*8,[(W,0) |-> int64<>]), arg1:array(0,<2*num,*8,[(W,0) |-> int64<>]), arg2:eq(llvmword(num)) -o arg0:array(0,<1,*8,[(W,0) |-> int64<>]), arg1:array(0,<2*num,*8,[(W,0) |-> 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
deleted file mode 100644
index ec1d2f3d4e..0000000000
--- a/heapster-saw/examples/sha512_proofs.v
+++ /dev/null
@@ -1,88 +0,0 @@
-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.
-
-Load "sha512_gen.v".
-Import SHA512.
-
-Import VectorNotations.
-
-
-Definition simpl0_invar (num0 idx num : bitvector 64) :=
-  isBvule 64 idx num0 /\ num = bvSub 64 num0 idx.
-
-Lemma no_errors_simpl0 : refinesFun simpl0 (fun num arr => noErrorsSpec).
-Proof.
-  unfold simpl0, simpl0__tuple_fun.
-  prove_refinement_match_letRecM_l.
-  - exact (fun num0 idx num sum arr _ _ _ => assumingM (simpl0_invar num0 idx num) noErrorsSpec).
-  unfold noErrorsSpec, simpl0_invar.
-  time "no_errors_simpl0" prove_refinement.
-  all: try assumption.
-  - assert (isBvult 64 a2 a1).
-    + apply isBvule_to_isBvult_or_eq in e_assuming.
-      destruct e_assuming; [assumption |].
-      apply bvEq_bvSub_r in H.
-      symmetry in H; contradiction.
-    + rewrite H in e_maybe; discriminate e_maybe.
-  - apply isBvult_to_isBvule_suc; assumption.
-  - repeat rewrite bvSub_eq_bvAdd_neg.
-    rewrite bvAdd_assoc; f_equal.
-    rewrite bvNeg_bvAdd_distrib; reflexivity.
-  - apply isBvule_zero_n.
-  - symmetry; apply bvSub_n_zero.
-Qed.
-
-
-Definition simpl0_spec num : BVVec 64 num (bitvector 8) -> bitvector 64 :=
-  foldr _ _ _ (fun a b => bvAdd 64 b (bvUExt 56 8 a)) (intToBv 64 0).
-
-Definition simpl0_letRec_spec num0 idx num (sum : bitvector 64) arr (_ _ _ : unit) :=
-  forallM (fun (pf : isBvule 64 idx num0) =>
-  assumingM (num = bvSub 64 num0 idx)
-            (returnM (arr, bvAdd 64 sum (simpl0_spec (bvSub 64 num0 idx)
-                                                     (dropBVVec _ _ _ idx pf arr))))).
-
-Lemma simpl0_spec_ref :
-  refinesFun simpl0 (fun num arr => returnM (arr, simpl0_spec num arr)).
-Proof.
-  unfold simpl0, simpl0__tuple_fun.
-  prove_refinement_match_letRecM_l.
-  - exact simpl0_letRec_spec.
-  unfold noErrorsSpec, simpl0_letRec_spec, simpl0_spec.
-  time "simpl0_spec_ref" prove_refinement.
-  (* Why didn't prove_refinement do this? *)
-  3: prove_refinement_eauto; [| apply refinesM_returnM ].
-  7: prove_refinement_eauto; [| apply refinesM_returnM ].
-  (* same as no_errors_simpl0 *)
-  - assert (isBvult 64 a2 a1).
-    + apply isBvule_to_isBvult_or_eq in e_forall.
-      destruct e_forall; [assumption |].
-      apply bvEq_bvSub_r in H.
-      symmetry in H; contradiction.
-    + rewrite H in e_maybe; discriminate e_maybe.
-  - apply isBvult_to_isBvule_suc; assumption.
-  - repeat rewrite bvSub_eq_bvAdd_neg.
-    rewrite bvAdd_assoc; f_equal.
-    rewrite bvNeg_bvAdd_distrib; reflexivity.
-  (* unique to this proof *)
-  - admit.
-  - repeat f_equal.
-    admit.
-  (* same as no_errors_simpl0 *)
-  - apply isBvule_zero_n.
-  - symmetry; apply bvSub_n_zero.
-  (* unique to this proof *)
-  - rewrite bvAdd_id_l.
-    repeat f_equal.
-    admit.
-Admitted.

From a0dfd11a7daea5ce08e2df94085fec66cfddf716 Mon Sep 17 00:00:00 2001
From: Matthew Yacavone <matthew@yacavone.net>
Date: Tue, 12 Oct 2021 16:18:40 -0700
Subject: [PATCH 7/7] move `where` defs from `proveEqH` into a new section in
 Permissions.hs

---
 .../src/Verifier/SAW/Heapster/Implication.hs  | 30 +---------------
 .../src/Verifier/SAW/Heapster/Permissions.hs  | 35 +++++++++++++++++++
 2 files changed, 36 insertions(+), 29 deletions(-)

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
index c9172ee384..63e0f255e2 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
@@ -30,7 +30,6 @@
 module Verifier.SAW.Heapster.Implication where
 
 import Data.Maybe
-import Data.Either
 import Data.List
 import Data.Functor.Product
 import Data.Functor.Compose
@@ -4625,7 +4624,7 @@ proveEqH psubst e mb_e = case (e, mbMatch mb_e) of
   -- with e_i = y_i, and e - (L_1*e_1 + ... + L_k*e_k + M) is divisible by N,
   -- by setting z = (e - (L_1*e_1 + ... + L_k*e_k + M))/N
   (_, [nuMP| PExpr_BV mb_factors (BV.BV mb_m) |])
-    | Just (n, memb, e_factors) <- getUnsetBVFactor mb_factors
+    | Just (n, memb, e_factors) <- getUnsetBVFactor psubst mb_factors
     , e' <- bvSub e (bvAdd e_factors (bvInt $ mbLift mb_m))
     , bvIsZero (bvMod e' n) ->
       setVarM memb (bvDiv e' n) >>> pure (SomeEqProofRefl e)
@@ -4635,33 +4634,6 @@ proveEqH psubst e mb_e = case (e, mbMatch mb_e) of
   -- Otherwise give up!
   _ -> proveEqFail e mb_e
 
-  where -- If there is exactly one 'BVFactor' in a list of 'BVFactor's which is
-        -- an unset variable, return the value of its 'BV', the witness that it
-        -- is bound, and the result of adding together the remaining factors
-        getUnsetBVFactor :: (1 <= w, KnownNat w) => Mb vars [BVFactor w] ->
-                            Maybe (Integer, Member vars (BVType w), PermExpr (BVType w))
-        getUnsetBVFactor (mbList -> mb_factors) =
-          case partitionEithers $ mbFactorNameBoundP <$> mb_factors of
-            ([(n, memb)], xs) -> Just (n, memb, foldl' bvAdd (bvInt 0) xs)
-            _ -> Nothing
-
-        -- If a 'BVFactor' in a binding is an unset variable, return the value
-        -- of its 'BV' and the witness that it is bound. Otherwise, return the
-        -- constant of the factor multiplied by the variable's value if it is
-        -- a set variable, or the constant of the factor multiplied by the
-        -- variable, if it is an unbound variable
-        mbFactorNameBoundP :: Mb vars (BVFactor w) ->
-                              Either (Integer, Member vars (BVType w))
-                                     (PermExpr (BVType w))
-        mbFactorNameBoundP (mbMatch -> [nuMP| BVFactor (BV.BV mb_n) mb_z |]) =
-          let n = mbLift mb_n in
-          case mbNameBoundP mb_z of
-            Left memb -> case psubstLookup psubst memb of 
-                           Nothing -> Left (n, memb)
-                           Just e' -> Right (bvMultBV (BV.mkBV knownNat n) e')
-            Right z -> Right (PExpr_BV [BVFactor (BV.mkBV knownNat n) z]
-                                       (BV.zero knownNat))
-
 
 -- | Build a proof on the top of the stack that @x:eq(e)@. Assume that all @x@
 -- permissions are on the top of the stack and given by argument @p@, and pop
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
index 93c7b049a1..26d6c8b8ba 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
@@ -31,6 +31,7 @@ import Prelude hiding (pred)
 
 import Data.Char (isDigit)
 import Data.Maybe
+import Data.Either
 import Data.Foldable (asum)
 import Data.List hiding (sort)
 import Data.List.NonEmpty (NonEmpty(..))
@@ -5570,6 +5571,40 @@ partialSubstForce :: Substable PartialSubst a Maybe => PartialSubst ctx ->
 partialSubstForce s mb msg = fromMaybe (error msg) $ partialSubst s mb
 
 
+----------------------------------------------------------------------
+-- * Additional functions involving partial substitutions
+----------------------------------------------------------------------
+
+-- | If there is exactly one 'BVFactor' in a list of 'BVFactor's which is
+-- an unset variable, return the value of its 'BV', the witness that it
+-- is bound, and the result of adding together the remaining factors
+getUnsetBVFactor :: (1 <= w, KnownNat w) => PartialSubst vars ->
+                    Mb vars [BVFactor w] ->
+                    Maybe (Integer, Member vars (BVType w), PermExpr (BVType w))
+getUnsetBVFactor psubst (mbList -> mb_factors) =
+  case partitionEithers $ mbFactorNameBoundP psubst <$> mb_factors of
+    ([(n, memb)], xs) -> Just (n, memb, foldl' bvAdd (bvInt 0) xs)
+    _ -> Nothing
+
+-- | If a 'BVFactor' in a binding is an unset variable, return the value
+-- of its 'BV' and the witness that it is bound. Otherwise, return the
+-- constant of the factor multiplied by the variable's value if it is
+-- a set variable, or the constant of the factor multiplied by the
+-- variable, if it is an unbound variable
+mbFactorNameBoundP :: PartialSubst vars ->
+                      Mb vars (BVFactor w) ->
+                      Either (Integer, Member vars (BVType w))
+                             (PermExpr (BVType w))
+mbFactorNameBoundP psubst (mbMatch -> [nuMP| BVFactor (BV.BV mb_n) mb_z |]) =
+  let n = mbLift mb_n in
+  case mbNameBoundP mb_z of
+    Left memb -> case psubstLookup psubst memb of 
+                   Nothing -> Left (n, memb)
+                   Just e' -> Right (bvMultBV (BV.mkBV knownNat n) e')
+    Right z -> Right (PExpr_BV [BVFactor (BV.mkBV knownNat n) z]
+                               (BV.zero knownNat))
+
+
 ----------------------------------------------------------------------
 -- * Abstracting Out Variables
 ----------------------------------------------------------------------