Expand Mr. Solver heterogeneity, improve monadification for SHA512 example

cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs

@@ -90,6 +90,7 @@ import Verifier.SAW.Recognizer
 -- import Verifier.SAW.Position
 import Verifier.SAW.Cryptol.PreludeM
 
+import GHC.Stack
 import Debug.Trace
 
 
@@ -345,6 +346,12 @@ typeclassMonMap =
    ("Cryptol.PIntegral", "Cryptol.PIntegral"),
    ("Cryptol.PLiteral", "Cryptol.PLiteral")]
 
+-- | The list of functions that are monadified as themselves in types
+typeLevelOpMonList :: [Ident]
+typeLevelOpMonList = ["Cryptol.tcAdd", "Cryptol.tcSub", "Cryptol.tcMul",
+                      "Cryptol.tcDiv", "Cryptol.tcMod", "Cryptol.tcExp",
+                      "Cryptol.tcMin", "Cryptol.tcMax"]
+
 -- | A context of local variables used for monadifying types, which includes the
 -- variable names, their original types (before monadification), and, if their
 -- types corespond to 'MonKind's, a local 'MonType' that quantifies over them.
@@ -364,25 +371,20 @@ ppTermInTypeCtx ctx t =
 typeCtxPureCtx :: MonadifyTypeCtx -> [(LocalName,Term)]
 typeCtxPureCtx = map (\(x,tp,_) -> (x,tp))
 
--- | Make a monadification type that is to be considered a base type
-mkTermBaseType :: MonadifyTypeCtx -> MonKind -> Term -> MonType
-mkTermBaseType ctx k t =
-  MTyBase k $ openOpenTerm (typeCtxPureCtx ctx) t
-
 -- | Monadify a type and convert it to its corresponding argument type
-monadifyTypeArgType :: MonadifyTypeCtx -> Term -> OpenTerm
+monadifyTypeArgType :: HasCallStack => MonadifyTypeCtx -> Term -> OpenTerm
 monadifyTypeArgType ctx t = toArgType $ monadifyType ctx t
 
 -- | Apply a monadified type to a type or term argument in the sense of
 -- 'applyPiOpenTerm', meaning give the type of applying @f@ of a type to a
 -- particular argument @arg@
-applyMonType :: MonType -> Either MonType ArgMonTerm -> MonType
+applyMonType :: HasCallStack => MonType -> Either MonType ArgMonTerm -> MonType
 applyMonType (MTyArrow _ tp_ret) (Right _) = tp_ret
 applyMonType (MTyForall _ _ f) (Left mtp) = f mtp
 applyMonType _ _ = error "applyMonType: application at incorrect type"
 
 -- | Convert a SAW core 'Term' to a monadification type
-monadifyType :: MonadifyTypeCtx -> Term -> MonType
+monadifyType :: HasCallStack => MonadifyTypeCtx -> Term -> MonType
 {-
 monadifyType ctx t
   | trace ("\nmonadifyType:\n" ++ ppTermInTypeCtx ctx t) False = undefined
@@ -417,15 +419,12 @@ monadifyType ctx (asDataType -> Just (pn, args))
     -- and/or Nums
     MTyBase k_out $ dataTypeOpenTerm (primName pn) (map toArgType margs)
 monadifyType ctx (asVectorType -> Just (len, tp)) =
-  let lenOT = openOpenTerm (typeCtxPureCtx ctx) len in
+  let lenOT = monadifyTypeNat ctx len in
   MTySeq (ctorOpenTerm "Cryptol.TCNum" [lenOT]) $ monadifyType ctx tp
-monadifyType ctx tp@(asApplyAll -> ((asGlobalDef -> Just seq_id), [n, a]))
+monadifyType ctx (asApplyAll -> ((asGlobalDef -> Just seq_id), [n, a]))
   | seq_id == "Cryptol.seq" =
-    case monTypeNum (monadifyType ctx n) of
-      Just n_trm -> MTySeq n_trm (monadifyType ctx a)
-      Nothing ->
-        error ("Monadify type: not a number: " ++ ppTermInTypeCtx ctx n
-               ++ " in type: " ++ ppTermInTypeCtx ctx tp)
+    let nOT = monadifyTypeArgType ctx n in
+    MTySeq nOT $ monadifyType ctx a
 monadifyType ctx (asApp -> Just ((asGlobalDef -> Just f), arg))
   | Just f_trans <- lookup f typeclassMonMap =
     MTyBase (MKType $ mkSort 1) $
@@ -442,16 +441,33 @@ monadifyType ctx (asApplyAll -> (f, args))
     MTyBase k_out (applyOpenTermMulti (globalDefOpenTerm glob) $
                    map toArgType margs)
 -}
-monadifyType ctx tp@(asCtor -> Just (pn, _))
-  | primName pn == "Cryptol.TCNum" || primName pn == "Cryptol.TCInf" =
-    MTyNum $ openOpenTerm (typeCtxPureCtx ctx) tp
+monadifyType _ (asCtor -> Just (pn, []))
+  | primName pn == "Cryptol.TCInf"
+  = MTyNum $ ctorOpenTerm "Cryptol.TCInf" []
+monadifyType ctx (asCtor -> Just (pn, [n]))
+  | primName pn == "Cryptol.TCNum"
+  = MTyNum $ ctorOpenTerm "Cryptol.TCNum" [monadifyTypeNat ctx n]
+monadifyType ctx (asApplyAll -> ((asGlobalDef -> Just f), args))
+  | f `elem` typeLevelOpMonList =
+    MTyNum $
+    applyOpenTermMulti (globalOpenTerm f) $ map (monadifyTypeArgType ctx) args
 monadifyType ctx (asLocalVar -> Just i)
   | i < length ctx
   , (_,_,Just tp) <- ctx!!i = tp
 monadifyType ctx tp =
   error ("monadifyType: not a valid type for monadification: "
          ++ ppTermInTypeCtx ctx tp)
 
+-- | Monadify a type-level natural number
+monadifyTypeNat :: HasCallStack => MonadifyTypeCtx -> Term -> OpenTerm
+monadifyTypeNat _ (asNat -> Just n) = natOpenTerm n
+monadifyTypeNat ctx (asLocalVar -> Just i)
+  | i < length ctx
+  , (_,_,Just tp) <- ctx!!i = toArgType tp
+monadifyTypeNat ctx tp =
+  error ("monadifyTypeNat: not a valid natural number for monadification: "
+         ++ ppTermInTypeCtx ctx tp)
+
 
 ----------------------------------------------------------------------
 -- * Monadified Terms
@@ -591,13 +607,21 @@ failArgMonTerm :: MonType -> String -> ArgMonTerm
 failArgMonTerm tp str = fromArgTerm tp (failOpenTerm str)
 
 -- | Apply a monadified term to a type or term argument
-applyMonTerm :: MonTerm -> Either MonType ArgMonTerm -> MonTerm
+applyMonTerm :: HasCallStack => MonTerm -> Either MonType ArgMonTerm -> MonTerm
 applyMonTerm (ArgMonTerm (FunMonTerm _ _ _ f)) (Right arg) = f arg
 applyMonTerm (ArgMonTerm (ForallMonTerm _ _ f)) (Left mtp) = f mtp
-applyMonTerm _ _ = error "applyMonTerm: application at incorrect type"
+applyMonTerm (ArgMonTerm (FunMonTerm _ _ _ _)) (Left _) =
+  error "applyMonTerm: application of term-level function to type-level argument"
+applyMonTerm (ArgMonTerm (ForallMonTerm _ _ _)) (Right _) =
+  error "applyMonTerm: application of type-level function to term-level argument"
+applyMonTerm (ArgMonTerm (BaseMonTerm _ _)) _ =
+  error "applyMonTerm: application of non-function base term"
+applyMonTerm (CompMonTerm _ _) _ =
+  error "applyMonTerm: application of computational term"
 
 -- | Apply a monadified term to 0 or more arguments
-applyMonTermMulti :: MonTerm -> [Either MonType ArgMonTerm] -> MonTerm
+applyMonTermMulti :: HasCallStack => MonTerm -> [Either MonType ArgMonTerm] ->
+                     MonTerm
 applyMonTermMulti = foldl applyMonTerm
 
 -- | Build a 'MonTerm' from a global of a given argument type
@@ -814,13 +838,13 @@ assertIsFinite _ =
 ----------------------------------------------------------------------
 
 -- | Monadify a type in the context of the 'MonadifyM' monad
-monadifyTypeM :: Term -> MonadifyM MonType
+monadifyTypeM :: HasCallStack => Term -> MonadifyM MonType
 monadifyTypeM tp =
   do ctx <- monStCtx <$> ask
      return $ monadifyType (ctxToTypeCtx ctx) tp
 
 -- | Monadify a term to a monadified term of argument type
-monadifyArg :: Maybe MonType -> Term -> MonadifyM ArgMonTerm
+monadifyArg :: HasCallStack => Maybe MonType -> Term -> MonadifyM ArgMonTerm
 {-
 monadifyArg _ t
   | trace ("Monadifying term of argument type: " ++ showTerm t) False
@@ -832,7 +856,7 @@ monadifyArg mtp t =
   monadifyTerm' mtp t >>= argifyMonTerm
 
 -- | Monadify a term to argument type and convert back to a term
-monadifyArgTerm :: Maybe MonType -> Term -> MonadifyM OpenTerm
+monadifyArgTerm :: HasCallStack => Maybe MonType -> Term -> MonadifyM OpenTerm
 monadifyArgTerm mtp t = toArgTerm <$> monadifyArg mtp t
 
 -- | Monadify a term
@@ -852,7 +876,7 @@ monadifyTerm mtp t =
 -- (i.e.,, lambdas, pairs, and records), but is optional for elimination forms
 -- (i.e., applications, projections, and also in this case variables). Note that
 -- this means monadification will fail on terms with beta or tuple redexes.
-monadifyTerm' :: Maybe MonType -> Term -> MonadifyM MonTerm
+monadifyTerm' :: HasCallStack => Maybe MonType -> Term -> MonadifyM MonTerm
 monadifyTerm' (Just mtp) t@(asLambda -> Just _) =
   ask >>= \(MonadifyROState { monStEnv = env, monStCtx = ctx }) ->
   return $ monadifyLambdas env ctx mtp t
@@ -938,7 +962,7 @@ monadifyTerm' _ t =
 
 -- | Monadify the application of a monadified term to a list of terms, using the
 -- type of the already monadified to monadify the arguments
-monadifyApply :: MonTerm -> [Term] -> MonadifyM MonTerm
+monadifyApply :: HasCallStack => MonTerm -> [Term] -> MonadifyM MonTerm
 monadifyApply f (t : ts)
   | MTyArrow tp_in _ <- getMonType f =
     do mtrm <- monadifyArg (Just tp_in) t
@@ -953,7 +977,8 @@ monadifyApply f [] = return f
 
 -- | FIXME: documentation; get our type down to a base type before going into
 -- the MonadifyM monad
-monadifyLambdas :: MonadifyEnv -> MonadifyCtx -> MonType -> Term -> MonTerm
+monadifyLambdas :: HasCallStack => MonadifyEnv -> MonadifyCtx ->
+                   MonType -> Term -> MonTerm
 monadifyLambdas env ctx (MTyForall _ k tp_f) (asLambda ->
                                               Just (x, x_tp, body)) =
   -- FIXME: check that monadifyKind x_tp == k
@@ -968,7 +993,8 @@ monadifyLambdas env ctx tp t =
   monadifyEtaExpand env ctx tp tp t []
 
 -- | FIXME: documentation
-monadifyEtaExpand :: MonadifyEnv -> MonadifyCtx -> MonType -> MonType -> Term ->
+monadifyEtaExpand :: HasCallStack => MonadifyEnv -> MonadifyCtx ->
+                     MonType -> MonType -> Term ->
                      [Either MonType ArgMonTerm] -> MonTerm
 monadifyEtaExpand env ctx top_mtp (MTyForall x k tp_f) t args =
   ArgMonTerm $ ForallMonTerm x k $ \mtp ->

heapster-saw/examples/arrays_mr_solver.saw

@@ -11,5 +11,5 @@ include "specPrims.saw";
 import "arrays.cry";
 
 zero_array <- parse_core_mod "arrays" "zero_array";
-// mr_solver_prove zero_array {{ zero_array_loop_spec }};
+mr_solver_test zero_array {{ zero_array_loop_spec }};
 mr_solver_prove zero_array {{ zero_array_spec }};

heapster-saw/examples/sha512.c

@@ -235,7 +235,7 @@ static void processBlock(uint64_t *a, uint64_t *b, uint64_t *c, uint64_t *d,
                          const uint8_t *in) {
   uint64_t s0, s1, T1;
   uint64_t X[16];
-  int i;
+  uint64_t i;
 
   T1 = X[0] = CRYPTO_load_u64_be(in);
   round_00_15(0, a, b, c, d, e, f, g, h, &T1);

heapster-saw/examples/sha512.cry

@@ -1,6 +1,8 @@
 
 module SHA512 where
 
+import SpecPrims
+
 // ============================================================================
 // Definitions from cryptol-specs/Primitive/Keyless/Hash/SHA512.cry, with some
 // type annotations added to SIGMA_0, SIGMA_1, sigma_0, and sigma_1 to get
@@ -83,3 +85,70 @@ round_16_80_spec i j a b c d e f g h X T1 =
         X' = update X (j && 15) T1'
         (a', b', c', d', e', f', g', h', T1'') =
           round_00_15_spec (i + j) a b c d e f g h T1'
+
+processBlock_spec : [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] ->
+                    [16][w] ->
+                    ([w], [w], [w], [w], [w], [w], [w], [w], [16][w])
+processBlock_spec a b c d e f g h in =
+  processBlock_loop_spec 16 aF bF cF dF eF fF gF hF X T1 in
+  where (a0,b0,c0,d0,e0,f0,g0,h0,_)  = round_00_15_spec  0 a  b  c  d  e  f  g  h  (in @ ( 0 : [w]))
+        (h1,a1,b1,c1,d1,e1,f1,g1,_)  = round_00_15_spec  1 h0 a0 b0 c0 d0 e0 f0 g0 (in @ ( 1 : [w]))
+        (g2,h2,a2,b2,c2,d2,e2,f2,_)  = round_00_15_spec  2 g1 h1 a1 b1 c1 d1 e1 f1 (in @ ( 2 : [w]))
+        (f3,g3,h3,a3,b3,c3,d3,e3,_)  = round_00_15_spec  3 f2 g2 h2 a2 b2 c2 d2 e2 (in @ ( 3 : [w]))
+        (e4,f4,g4,h4,a4,b4,c4,d4,_)  = round_00_15_spec  4 e3 f3 g3 h3 a3 b3 c3 d3 (in @ ( 4 : [w]))
+        (d5,e5,f5,g5,h5,a5,b5,c5,_)  = round_00_15_spec  5 d4 e4 f4 g4 h4 a4 b4 c4 (in @ ( 5 : [w]))
+        (c6,d6,e6,f6,g6,h6,a6,b6,_)  = round_00_15_spec  6 c5 d5 e5 f5 g5 h5 a5 b5 (in @ ( 6 : [w]))
+        (b7,c7,d7,e7,f7,g7,h7,a7,_)  = round_00_15_spec  7 b6 c6 d6 e6 f6 g6 h6 a6 (in @ ( 7 : [w]))
+        (a8,b8,c8,d8,e8,f8,g8,h8,_)  = round_00_15_spec  8 a7 b7 c7 d7 e7 f7 g7 h7 (in @ ( 8 : [w]))
+        (h9,a9,b9,c9,d9,e9,f9,g9,_)  = round_00_15_spec  9 h8 a8 b8 c8 d8 e8 f8 g8 (in @ ( 9 : [w]))
+        (gA,hA,aA,bA,cA,dA,eA,fA,_)  = round_00_15_spec 10 g9 h9 a9 b9 c9 d9 e9 f9 (in @ (10 : [w]))
+        (fB,gB,hB,aB,bB,cB,dB,eB,_)  = round_00_15_spec 11 fA gA hA aA bA cA dA eA (in @ (11 : [w]))
+        (eC,fC,gC,hC,aC,bC,cC,dC,_)  = round_00_15_spec 12 eB fB gB hB aB bB cB dB (in @ (12 : [w]))
+        (dD,eD,fD,gD,hD,aD,bD,cD,_)  = round_00_15_spec 13 dC eC fC gC hC aC bC cC (in @ (13 : [w]))
+        (cE,dE,eE,fE,gE,hE,aE,bE,_)  = round_00_15_spec 14 cD dD eD fD gD hD aD bD (in @ (14 : [w]))
+        (bF,cF,dF,eF,fF,gF,hF,aF,T1) = round_00_15_spec 15 bE cE dE eE fE gE hE aE (in @ (15 : [w]))
+        X = [in @ ( 0 : [w]), in @ ( 1 : [w]), in @ ( 2 : [w]), in @ ( 3 : [w]),
+             in @ ( 4 : [w]), in @ ( 5 : [w]), in @ ( 6 : [w]), in @ ( 7 : [w]),
+             in @ ( 8 : [w]), in @ ( 9 : [w]), in @ (10 : [w]), in @ (11 : [w]),
+             in @ (12 : [w]), in @ (13 : [w]), in @ (14 : [w]), in @ (15 : [w])]
+
+processBlock_loop_spec : [w] ->
+                         [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] ->
+                         [16][w] -> [w] -> [16][w] ->
+                         ([w], [w], [w], [w], [w], [w], [w], [w], [16][w])
+processBlock_loop_spec i a b c d e f g h X T1 in =
+  if i < 80 then processBlock_loop_spec (i+16) aF bF cF dF eF fF gF hF XF T1F in
+            else (a,b,c,d,e,f,g,h,in)
+  where (a0,b0,c0,d0,e0,f0,g0,h0,X0,_,_,T10) = round_16_80_spec i  0 a  b  c  d  e  f  g  h  X  T1 
+        (h1,a1,b1,c1,d1,e1,f1,g1,X1,_,_,T11) = round_16_80_spec i  1 h0 a0 b0 c0 d0 e0 f0 g0 X0 T10
+        (g2,h2,a2,b2,c2,d2,e2,f2,X2,_,_,T12) = round_16_80_spec i  2 g1 h1 a1 b1 c1 d1 e1 f1 X1 T11
+        (f3,g3,h3,a3,b3,c3,d3,e3,X3,_,_,T13) = round_16_80_spec i  3 f2 g2 h2 a2 b2 c2 d2 e2 X2 T12
+        (e4,f4,g4,h4,a4,b4,c4,d4,X4,_,_,T14) = round_16_80_spec i  4 e3 f3 g3 h3 a3 b3 c3 d3 X3 T13
+        (d5,e5,f5,g5,h5,a5,b5,c5,X5,_,_,T15) = round_16_80_spec i  5 d4 e4 f4 g4 h4 a4 b4 c4 X4 T14
+        (c6,d6,e6,f6,g6,h6,a6,b6,X6,_,_,T16) = round_16_80_spec i  6 c5 d5 e5 f5 g5 h5 a5 b5 X5 T15
+        (b7,c7,d7,e7,f7,g7,h7,a7,X7,_,_,T17) = round_16_80_spec i  7 b6 c6 d6 e6 f6 g6 h6 a6 X6 T16
+        (a8,b8,c8,d8,e8,f8,g8,h8,X8,_,_,T18) = round_16_80_spec i  8 a7 b7 c7 d7 e7 f7 g7 h7 X7 T17
+        (h9,a9,b9,c9,d9,e9,f9,g9,X9,_,_,T19) = round_16_80_spec i  9 h8 a8 b8 c8 d8 e8 f8 g8 X8 T18
+        (gA,hA,aA,bA,cA,dA,eA,fA,XA,_,_,T1A) = round_16_80_spec i 10 g9 h9 a9 b9 c9 d9 e9 f9 X9 T19
+        (fB,gB,hB,aB,bB,cB,dB,eB,XB,_,_,T1B) = round_16_80_spec i 11 fA gA hA aA bA cA dA eA XA T1A
+        (eC,fC,gC,hC,aC,bC,cC,dC,XC,_,_,T1C) = round_16_80_spec i 12 eB fB gB hB aB bB cB dB XB T1B
+        (dD,eD,fD,gD,hD,aD,bD,cD,XD,_,_,T1D) = round_16_80_spec i 13 dC eC fC gC hC aC bC cC XC T1C
+        (cE,dE,eE,fE,gE,hE,aE,bE,XE,_,_,T1E) = round_16_80_spec i 14 cD dD eD fD gD hD aD bD XD T1D
+        (bF,cF,dF,eF,fF,gF,hF,aF,XF,_,_,T1F) = round_16_80_spec i 15 bE cE dE eE fE gE hE aE XE T1E
+
+processBlocks_spec : {n} Literal n [64] => [8][w] -> [16*n][w] ->
+                     ([8][w], [16*n][w])
+processBlocks_spec state in = processBlocks_loop_spec 0 `n state in
+
+processBlocks_loop_spec : {n} Literal n [64] => [w] -> [w] -> [8][w] ->
+                          [16*n][w] -> ([8][w], [16*n][w])
+processBlocks_loop_spec i j state in = invariantHint (i + j == `n) (
+  if j != 0 then processBlocks_loop_spec (i+1) (j-1) state' in
+            else (state, in))
+  where (a,b,c,d,e,f,g,h) = (state @ ( 0 : [w]), state @ ( 1 : [w]),
+                             state @ ( 2 : [w]), state @ ( 3 : [w]),
+                             state @ ( 4 : [w]), state @ ( 5 : [w]),
+                             state @ ( 6 : [w]), state @ ( 7 : [w]))
+        in_i = split in @ i
+        (a',b',c',d',e',f',g',h',_) = processBlock_spec a b c d e f g h in_i
+        state' = [a', b', c', d', e', f', g', h']

heapster-saw/examples/sha512.saw

@@ -7,11 +7,17 @@ heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x)
 heapster_define_perm env "int32" " " "llvmptr 32" "exists x:bv 32.eq(llvmword(x))";
 heapster_define_perm env "int8" " " "llvmptr 8" "exists x:bv 8.eq(llvmword(x))";
 
+// FIXME: We always have rw=W, but without the rw arguments below Heapster
+// doesn't realize the perm is not copyable (it needs to unfold named perms).
+heapster_define_perm env "int64_ptr" "rw:rwmodality" "llvmptr 64" "ptr((rw,0) |-> int64<>)";
+heapster_define_perm env "true_ptr" "rw:rwmodality" "llvmptr 64" "ptr((rw,0) |-> true)";
+
 heapster_assume_fun env "CRYPTO_load_u64_be"
   "(). arg0:ptr((R,0) |-> int64<>) -o \
      \ arg0:ptr((R,0) |-> int64<>), ret:int64<>"
   "\\ (x:Vec 64 Bool) -> returnM (Vec 64 Bool * Vec 64 Bool) (x, x)";
 
+/*
 heapster_typecheck_fun env "return_state"
   "(). arg0:array(W,0,<8,*8,fieldsh(int64<>)) -o \
      \ arg0:array(W,0,<8,*8,fieldsh(int64<>))";
@@ -24,5 +30,50 @@ heapster_typecheck_fun env "sha512_block_data_order"
               \ arg0:array(W,0,<8,*8,fieldsh(int64<>)), \
               \ arg1:array(R,0,<16*num,*8,fieldsh(int64<>)), \
               \ arg2:true, ret:true";
+*/
+
+heapster_typecheck_fun env "round_00_15"
+ "(). arg0:int64<>, \
+    \ arg1:int64_ptr<W>, arg2:int64_ptr<W>, arg3:int64_ptr<W>, arg4:int64_ptr<W>, \
+    \ arg5:int64_ptr<W>, arg6:int64_ptr<W>, arg7:int64_ptr<W>, arg8:int64_ptr<W>, \
+    \ arg9:int64_ptr<W> -o \
+    \ arg1:int64_ptr<W>, arg2:int64_ptr<W>, arg3:int64_ptr<W>, arg4:int64_ptr<W>, \
+    \ arg5:int64_ptr<W>, arg6:int64_ptr<W>, arg7:int64_ptr<W>, arg8:int64_ptr<W>, \
+    \ arg9:int64_ptr<W>, ret:true";
+
+heapster_typecheck_fun env "round_16_80"
+ "(). arg0:int64<>, arg1:int64<>, \
+    \ arg2:int64_ptr<W>, arg3:int64_ptr<W>, arg4:int64_ptr<W>, arg5:int64_ptr<W>, \
+    \ arg6:int64_ptr<W>, arg7:int64_ptr<W>, arg8:int64_ptr<W>, arg9:int64_ptr<W>, \
+    \ arg10:array(W,0,<16,*8,fieldsh(int64<>)), \
+    \ arg11:true_ptr<W>, arg12:true_ptr<W>, arg13:int64_ptr<W> -o \
+    \ arg2:int64_ptr<W>, arg3:int64_ptr<W>, arg4:int64_ptr<W>, arg5:int64_ptr<W>, \
+    \ arg6:int64_ptr<W>, arg7:int64_ptr<W>, arg8:int64_ptr<W>, arg9:int64_ptr<W>, \
+    \ arg10:array(W,0,<16,*8,fieldsh(int64<>)), \
+    \ arg11:int64_ptr<W>, arg12:int64_ptr<W>, arg13:int64_ptr<W>, ret:true";
+
+heapster_typecheck_fun env "return_X"
+  "(). arg0:array(W,0,<16,*8,fieldsh(int64<>)) -o \
+     \ arg0:array(W,0,<16,*8,fieldsh(int64<>))";
+
+heapster_set_translation_checks env false;
+heapster_typecheck_fun env "processBlock"
+  "(). arg0:int64_ptr<W>, arg1:int64_ptr<W>, arg2:int64_ptr<W>, \
+     \ arg3:int64_ptr<W>, arg4:int64_ptr<W>, arg5:int64_ptr<W>, \
+     \ arg6:int64_ptr<W>, arg7:int64_ptr<W>, \
+     \ arg8:array(R,0,<16,*8,fieldsh(int64<>)) -o \
+     \ arg0:int64_ptr<W>, arg1:int64_ptr<W>, arg2:int64_ptr<W>, \
+     \ arg3:int64_ptr<W>, arg4:int64_ptr<W>, arg5:int64_ptr<W>, \
+     \ arg6:int64_ptr<W>, arg7:int64_ptr<W>, \
+     \ arg8:array(R,0,<16,*8,fieldsh(int64<>)), ret:true";
+
+heapster_set_translation_checks env false;
+heapster_typecheck_fun env "processBlocks"
+  "(num:bv 64). arg0:array(W,0,<8,*8,fieldsh(int64<>)), \
+              \ arg1:array(R,0,<16*num,*8,fieldsh(int64<>)), \
+              \ arg2:eq(llvmword(num)) -o \
+              \ arg0:array(W,0,<8,*8,fieldsh(int64<>)), \
+              \ arg1:array(R,0,<16*num,*8,fieldsh(int64<>)), \
+              \ arg2:true, ret:true";
 
 heapster_export_coq env "sha512_gen.v";