Updates to Cryptol Monadification (+ add qsort to saw-core)

examples/mr_solver/monadify_module.saw

@@ -0,0 +1,3 @@
+enable_experimental;
+// write_coq_cryptol_module "monadify.cry" "monadify_gen.v" [] ["fib"];
+write_coq_cryptol_module_monadic "monadify.cry" "monadify_gen_m.v" [] [];

heapster-saw/examples/sha512_mr_solver.saw

@@ -12,20 +12,6 @@ processBlocks <- parse_core_mod "SHA512" "processBlocks";
 // mr_solver_test round_00_15 round_00_15;
 
 import "sha512.cry";
-// FIXME: Why aren't we monadifying these automatically when they're used?
-monadify_term {{ K }};
-monadify_term {{ SIGMA_0 }};
-monadify_term {{ SIGMA_1 }};
-monadify_term {{ sigma_0 }};
-monadify_term {{ sigma_1 }};
-monadify_term {{ Ch }};
-monadify_term {{ Maj }};
-monadify_term {{ round_00_15_spec }};
-monadify_term {{ round_16_80_spec }};
-monadify_term {{ processBlock_loop_spec }};
-monadify_term {{ processBlock_spec }};
-monadify_term {{ processBlocks_loop_spec }};
-monadify_term {{ processBlocks_spec }};
 
 mr_solver_prove round_00_15 {{ round_00_15_spec }};
 mr_solver_prove round_16_80 {{ round_16_80_spec }};

saw-core-coq/coq/_CoqProject

@@ -1,8 +1,9 @@
 -Q generated/CryptolToCoq   CryptolToCoq
 -Q handwritten/CryptolToCoq CryptolToCoq
 
-generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v
 generated/CryptolToCoq/SAWCorePrelude.v
+generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v
+generated/CryptolToCoq/CryptolMPrimitivesForSAWCore.v
 
 handwritten/CryptolToCoq/CompM.v
 handwritten/CryptolToCoq/CompMExtra.v

saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreScaffolding.v

@@ -118,6 +118,17 @@ Global Instance Inhabited_unit : Inhabited unit :=
 Global Instance Inhabited_bool : Inhabited bool :=
   MkInhabited bool false.
 
+Program Instance QuantType_Bool : QuantType Bool :=
+ { quantEnc := QEnc_nat;
+   quantEnum := fun n => match n with
+                         | 0 => false
+                         | S _ => true
+                         end;
+   quantEnumInv := fun b => if b then 1 else 0 }.
+Next Obligation.
+ destruct a; reflexivity.
+Defined.
+
 (* SAW uses an alternate form of eq_rect where the motive function P also
 depends on the equality proof itself *)
 Definition Eq__rec (A : Type) (x : A) (P: forall y, x=y -> Type) (p:P x eq_refl) y (e:x=y) :

saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v

@@ -86,6 +86,41 @@ Qed.
 Instance Inhabited_Vec (n:nat) (a:Type) {Ha:Inhabited a} : Inhabited (Vec n a) :=
   MkInhabited (Vec n a) (gen n a (fun _ => inhabitant)).
 
+(* Build the encoding of the N-tuple of a given encoding *)
+Fixpoint QEnc_NTuple n (qenc : QuantEnc) : QuantEnc :=
+ match n with
+ | 0 => QEnc_prop True
+ | S n' => QEnc_pair qenc (QEnc_NTuple n' qenc)
+ end.
+
+(* The quantEnum function for Vec n a *)
+Definition quantEnum_Vec n A `{QuantType A} :
+ encodes (QEnc_NTuple n (quantEnc (A:=A))) -> Vec n A :=
+ nat_rect
+   (fun n => encodes (QEnc_NTuple n (quantEnc (A:=A))) -> Vec n A)
+   (fun _ => VectorDef.nil _)
+   (fun n enumF x => VectorDef.cons _ (quantEnum (fst x)) _ (enumF (snd x)))
+   n.
+
+(* The quantEnumInv function for Vec n a *)
+Definition quantEnumInv_Vec n A `{QuantType A} :
+ Vec n A -> encodes (QEnc_NTuple n (quantEnc (A:=A))) :=
+ nat_rect
+   (fun n => Vec n A -> encodes (QEnc_NTuple n (quantEnc (A:=A))))
+   (fun _ => I)
+   (fun n enumInvF x => (quantEnumInv (VectorDef.hd x), enumInvF (VectorDef.tl x)))
+   n.
+
+Program Instance QuantType_Vec n A `{QuantType A} : QuantType (Vec n A) :=
+ { quantEnc := QEnc_NTuple n (quantEnc (A:=A));
+   quantEnum := quantEnum_Vec n A;
+   quantEnumInv := quantEnumInv_Vec n A }.
+Next Obligation.
+ induction a.
+ - reflexivity.
+ - simpl. rewrite quantEnumSurjective. rewrite IHa. reflexivity.
+Defined.
+
 Theorem gen_domain_eq n T : forall f g (domain_eq : forall i, f i = g i),
     gen n T f = gen n T g.
 Proof.

saw-core-coq/coq/handwritten/CryptolToCoq/SpecMExtra.v

@@ -14,64 +14,6 @@ From EnTree Require Export
 Import SAWCorePrelude.
 
 
-(***
- *** QuantType Instances
- ***)
-
-(** Simple QuantType Instances **)
-
-Program Instance QuantType_Bool : QuantType Bool :=
-  { quantEnc := QEnc_nat;
-    quantEnum := fun n => match n with
-                          | 0 => false
-                          | S _ => true
-                          end;
-    quantEnumInv := fun b => if b then 1 else 0 }.
-Next Obligation.
-  destruct a; reflexivity.
-Defined.
-
-
-(** QuantType Vec Instance **)
-
-(* Build the encoding of the N-tuple of a given encoding *)
-Fixpoint QEnc_NTuple n (qenc : QuantEnc) : QuantEnc :=
-  match n with
-  | 0 => QEnc_prop True
-  | S n' => QEnc_pair qenc (QEnc_NTuple n' qenc)
-  end.
-
-(* The quantEnum function for Vec n a *)
-Definition quantEnum_Vec n A `{QuantType A} :
-  encodes (QEnc_NTuple n (quantEnc (A:=A))) -> Vec n A :=
-  nat_rect
-    (fun n => encodes (QEnc_NTuple n (quantEnc (A:=A))) -> Vec n A)
-    (fun _ => VectorDef.nil _)
-    (fun n enumF x => VectorDef.cons _ (quantEnum (fst x)) _ (enumF (snd x)))
-    n.
-
-(* The quantEnumInv function for Vec n a *)
-Definition quantEnumInv_Vec n A `{QuantType A} :
-  Vec n A -> encodes (QEnc_NTuple n (quantEnc (A:=A))) :=
-  nat_rect
-    (fun n => Vec n A -> encodes (QEnc_NTuple n (quantEnc (A:=A))))
-    (fun _ => I)
-    (fun n enumInvF x => (quantEnumInv (VectorDef.hd x), enumInvF (VectorDef.tl x)))
-    n.
-
-Program Instance QuantType_Vec n A `{QuantType A} : QuantType (Vec n A) :=
-  { quantEnc := QEnc_NTuple n (quantEnc (A:=A));
-    quantEnum := quantEnum_Vec n A;
-    quantEnumInv := quantEnumInv_Vec n A }.
-Next Obligation.
-  induction a.
-  - reflexivity.
-  - simpl. rewrite quantEnumSurjective. rewrite IHa. reflexivity.
-Defined.
-
-Program Instance QuantType_bitvector w : QuantType (bitvector w) :=
-  QuantType_Vec w _.
-
 
 (***
  *** Additional Automation

saw-core-coq/saw/generate_scaffolding.saw

@@ -1,3 +1,3 @@
 enable_experimental;
 write_coq_sawcore_prelude                "../coq/generated/CryptolToCoq/SAWCorePrelude.v" [] [];
-write_coq_cryptol_primitives_for_sawcore "../coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v" [] [];
+write_coq_cryptol_primitives_for_sawcore "../coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v" "../coq/generated/CryptolToCoq/CryptolMPrimitivesForSAWCore.v" [] [];

saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs

@@ -464,10 +464,9 @@ translateParam ::
   TermTranslationMonad m =>
   (LocalName, Term) -> m [Coq.Binder]
 translateParam (n, ty) =
-  translateBinder n ty >>= \case
-    Left (n',ty') -> return [Coq.Binder n' (Just ty')]
-    Right (n',ty',nh,nhty) ->
-      return [Coq.Binder n' (Just ty'), Coq.ImplicitBinder nh (Just nhty)]
+  translateBinder n ty >>= \(n',ty',nhs) ->
+    return $ Coq.Binder n' (Just ty') :
+             map (\(nh,nhty) -> Coq.ImplicitBinder nh (Just nhty)) nhs
 
 translatePi :: TermTranslationMonad m => [(LocalName, Term)] -> Term -> m Coq.Term
 translatePi binders body = withLocalTranslationState $ do
@@ -479,44 +478,44 @@ translatePiBinder ::
   TermTranslationMonad m => (LocalName, Term) -> m [Coq.PiBinder]
 translatePiBinder (n, ty) =
   translateBinder n ty >>= \case
-    Left (n',ty')
+    (n',ty',[])
       | n == "_"  -> return [Coq.PiBinder Nothing ty']
       | otherwise -> return [Coq.PiBinder (Just n') ty']
-    Right (n',ty',nh,nhty) ->
-      return [Coq.PiBinder (Just n') ty', Coq.PiImplicitBinder (Just nh) nhty]
+    (n',ty',nhs) ->
+      return $ Coq.PiBinder (Just n') ty' :
+               map (\(nh,nhty) -> Coq.PiImplicitBinder (Just nh) nhty) nhs
 
 translateBinder ::
   TermTranslationMonad m =>
   LocalName ->
   Term ->
-  m (Either (Coq.Ident,Coq.Type) (Coq.Ident,Coq.Type,Coq.Ident,Coq.Type))
-translateBinder n ty@(asPiList -> (args, asISort -> Just _s)) =
+  m (Coq.Ident,Coq.Type,[(Coq.Ident,Coq.Type)])
+translateBinder n ty@(asPiList -> (args, asSortWithFlags -> mb_sort)) =
   do ty' <- translateTerm ty
      n' <- freshenAndBindName n
-     hty' <- translateInhHyp args (Coq.Var n')
-     hn' <- translateLocalIdent ("Inh_" <> n )
-     return $ Right (n',ty',hn',hty')
-translateBinder n ty =
-  do ty' <- translateTerm ty
-     n'  <- freshenAndBindName n
-     return $ Left (n',ty')
-
-translateInhHyp ::
+     let flagValues = sortFlagsToList $ maybe noFlags snd mb_sort
+         flagLocalNames = [("Inh", "SAWCoreScaffolding.Inhabited"),
+                           ("QT", "QuantType")]
+     nhs <- forM (zip flagValues flagLocalNames) $ \(fi,(prefix,tc)) ->
+       if not fi then return []
+       else do nhty <- translateImplicitHyp (Coq.Var tc) args (Coq.Var n')
+               nh <- translateLocalIdent (prefix <> "_" <> n)
+               return [(nh,nhty)]
+     return (n',ty',concat nhs)
+
+translateImplicitHyp ::
   TermTranslationMonad m =>
-  [(LocalName, Term)] -> Coq.Term -> m Coq.Term
-translateInhHyp [] tm = return (Coq.App (Coq.Var "SAWCoreScaffolding.Inhabited") [tm])
-translateInhHyp args tm = withLocalTranslationState $
+  Coq.Term -> [(LocalName, Term)] -> Coq.Term -> m Coq.Term
+translateImplicitHyp tc [] tm = return (Coq.App tc [tm])
+translateImplicitHyp tc args tm = withLocalTranslationState $
   do args' <- mapM (uncurry translateBinder) args
      return $ Coq.Pi (concatMap mkPi args')
-                (Coq.App (Coq.Var "SAWCoreScaffolding.Inhabited") [Coq.App tm (map mkArg args')])
+                (Coq.App tc [Coq.App tm (map mkArg args')])
  where
-  mkPi (Left (nm,ty)) =
-    [Coq.PiBinder (Just nm) ty]
-  mkPi (Right (nm,ty,hnm,hty)) =
-    [Coq.PiBinder (Just nm) ty, Coq.PiImplicitBinder (Just hnm) hty]
-
-  mkArg (Left (nm,_)) = Coq.Var nm
-  mkArg (Right (nm,_,_,_)) = Coq.Var nm
+  mkPi (nm,ty,nhs) =
+    Coq.PiBinder (Just nm) ty :
+    map (\(nh,nhty) -> Coq.PiImplicitBinder (Just nh) nhty) nhs
+  mkArg (nm,_,_) = Coq.Var nm
 
 -- | Translate a local name from a saw-core binder into a fresh Coq identifier.
 translateLocalIdent :: TermTranslationMonad m => LocalName -> m Coq.Ident

saw-core/prelude/Prelude.sawcore

@@ -3011,11 +3011,11 @@ primitive errorS : (E:EvType) -> (stack:FunStack) -> (a:sort 0) -> String ->
                    SpecM E stack a;
 
 -- The spec that universally quantifies over all return values of type a
-primitive forallS : (E:EvType) -> (stack:FunStack) -> (a:sort 0) ->
+primitive forallS : (E:EvType) -> (stack:FunStack) -> (a:qsort 0) ->
                     SpecM E stack a;
 
 -- The spec that existentially quantifies over all return values of type a
-primitive existsS : (E:EvType) -> (stack:FunStack) -> (a:sort 0) ->
+primitive existsS : (E:EvType) -> (stack:FunStack) -> (a:qsort 0) ->
                     SpecM E stack a;
 
 -- Assume a proposition holds
@@ -3048,9 +3048,22 @@ assertingS : (E:EvType) -> (stack:FunStack) -> (a : sort 0) -> Bool ->
 assertingS E stack a cond m =
   bindS E stack #() a (assertBoolS E stack cond) (\ (_:#()) -> m);
 
+-- Lift a computation into a stack with an additional frame
+primitive pushStackS : (E:EvType) -> (frame:List1 LetRecType) ->
+                       (stack:FunStack) -> (A:sort 0) ->
+                       SpecM E stack A -> SpecM E (pushFunStack frame stack) A;
+
 -- Lift a computation in the empty stack to an arbitrary stack
-primitive liftStackS : (E:EvType) -> (stack:FunStack) -> (A:sort 0) ->
-                       SpecM E emptyFunStack A -> SpecM E stack A;
+liftStackS : (E:EvType) -> (stack:FunStack) -> (A:sort 0) ->
+             SpecM E emptyFunStack A -> SpecM E stack A;
+liftStackS E stack A m0 =
+  List1#rec
+  (List1 LetRecType)
+  (\ (stack:FunStack) -> SpecM E stack A)
+  m0
+  (\ (frame:List1 LetRecType) (stack:FunStack) (m:SpecM E stack A) ->
+     pushStackS E frame stack A m)
+  stack;
 
 -- The computation that nondeterministically chooses one computation or another.
 -- As a specification, represents the disjunction of two specifications.

saw-core/src/Verifier/SAW/Conversion.hs

@@ -282,7 +282,7 @@ asAnySort = asVar $ \t -> do Sort v _ <- R.asFTermF t; return v
 
 -- | Match a specific sort.
 asSort :: Sort -> Matcher ()
-asSort s = Matcher (termToPat (Unshared (FTermF (Sort s False)))) fn
+asSort s = Matcher (termToPat (Unshared (FTermF (Sort s noFlags)))) fn
   where fn t = do s' <- R.asSort t
                   guard (s == s')
 

saw-core/src/Verifier/SAW/ExternalFormat.hs

@@ -184,8 +184,8 @@ scWriteExternal t0 =
             RecordValue elems   -> pure $ unwords ["Record", show elems]
             RecordProj e prj    -> pure $ unwords ["RecordProj", show e, Text.unpack prj]
             Sort s h
-              | s == propSort -> pure $ unwords ["Prop", show h]
-              | otherwise     -> pure $ unwords ["Sort", drop 5 (show s), show h]
+              | s == propSort -> pure $ unwords ("Prop" : map show (sortFlagsToList h))
+              | otherwise     -> pure $ unwords ("Sort" : drop 5 (show s) : map show (sortFlagsToList h))
                                                         -- /\ Ugly hack to drop "sort "
             NatLit n            -> pure $ unwords ["Nat", show n]
             ArrayValue e v      -> pure $ unwords ("Array" : show e :
@@ -347,8 +347,8 @@ scReadExternal sc input =
         ["Record", elems] ->
           FTermF <$> (RecordValue <$> (traverse (traverse getTerm) =<< readM elems))
         ["RecordProj", e, prj] -> FTermF <$> (RecordProj <$> readIdx e <*> pure (Text.pack prj))
-        ["Prop", h]         -> FTermF <$> (Sort propSort <$> readM h)
-        ["Sort", s, h]      -> FTermF <$> (Sort <$> (mkSort <$> readM s) <*> readM h)
+        ("Prop" : h)        -> FTermF <$> (Sort propSort . sortFlagsFromList <$> (mapM readM h))
+        ("Sort" : s : h)    -> FTermF <$> (Sort <$> (mkSort <$> readM s) <*> (sortFlagsFromList <$> mapM readM h))
         ["Nat", n]          -> FTermF <$> (NatLit <$> readM n)
         ("Array" : e : es)  -> FTermF <$> (ArrayValue <$> readIdx e <*> (V.fromList <$> traverse readIdx es))
         ("String" : ts)     -> FTermF <$> (StringLit <$> (readM (unwords ts)))

saw-core/src/Verifier/SAW/Grammar.y

@@ -73,6 +73,8 @@ import Verifier.SAW.Lexer
   'module'    { PosPair _ (TKey "module") }
   'sort'      { PosPair _ (TKey "sort") }
   'isort'     { PosPair _ (TKey "isort") }
+  'qsort'     { PosPair _ (TKey "qsort") }
+  'qisort'    { PosPair _ (TKey "qisort") }
   'Prop'      { PosPair _ (TKey "Prop") }
   'where'     { PosPair _ (TKey "where") }
   'axiom'     { PosPair _ (TKey "axiom") }
@@ -182,9 +184,8 @@ AtomTerm
   | string                       { StringLit (pos $1) (Text.pack (tokString (val $1))) }
   | Ident                        { Name $1 }
   | IdentRec                     { Recursor Nothing $1 }
-  | 'Prop'                       { Sort (pos $1) propSort False }
-  | 'sort' nat                   { Sort (pos $1) (mkSort (tokNat (val $2))) False }
-  | 'isort' nat                  { Sort (pos $1) (mkSort (tokNat (val $2))) True }
+  | 'Prop'                       { Sort (pos $1) propSort noFlags }
+  | Sort nat                     { Sort (pos $1) (mkSort (tokNat (val $2))) (val $1) }
   | AtomTerm '.' Ident           { RecordProj $1 (val $3) }
   | AtomTerm '.' IdentRec        {% parseRecursorProj $1 $3 }
   | AtomTerm '.' nat             {% parseTupleSelector $1 (fmap tokNat $3) }
@@ -201,6 +202,12 @@ Ident : ident { fmap (Text.pack . tokIdent) $1 }
 IdentRec :: { PosPair Text }
 IdentRec : identrec { fmap (Text.pack . tokRecursor) $1 }
 
+Sort :: { PosPair SortFlags }
+Sort : 'sort'   { fmap (const $ SortFlags False False) $1 }
+     | 'isort'  { fmap (const $ SortFlags True  False) $1 }
+     | 'qsort'  { fmap (const $ SortFlags False True ) $1 }
+     | 'qisort' { fmap (const $ SortFlags True  True ) $1 }
+
 FieldValue :: { (PosPair FieldName, Term) }
 FieldValue : Ident '=' Term { ($1, $3) }
 

saw-core/src/Verifier/SAW/Lexer.x

@@ -73,7 +73,8 @@ $idchar    = [a-z A-Z 0-9 \' \_]
 @punct = "#" | "," | "->" | "." | ";" | ":" | "=" | "*"
        | "\" | "(" | ")" | "[" | "]" | "{" | "}" | "|"
 @keywords = "data" | "hiding" | "import" | "module" | "injectCode"
-          | "sort" | "isort" | "Prop" | "where" | "primitive" | "axiom"
+          | "sort" | "isort" | "qsort" | "qisort"
+          | "Prop" | "where" | "primitive" | "axiom"
 @key = @punct | @keywords
 
 @escape      = \\ ($charesc | @ascii | @decimal | o @octal | x @hex)

saw-core/src/Verifier/SAW/OpenTerm.hs

@@ -131,7 +131,7 @@ flatOpenTerm ftf = OpenTerm $
 
 -- | Build an 'OpenTerm' for a sort
 sortOpenTerm :: Sort -> OpenTerm
-sortOpenTerm s = flatOpenTerm (Sort s False)
+sortOpenTerm s = flatOpenTerm (Sort s noFlags)
 
 -- | Build an 'OpenTerm' for a natural number literal
 natOpenTerm :: Natural -> OpenTerm

saw-core/src/Verifier/SAW/Recognizer.hs

@@ -56,7 +56,7 @@ module Verifier.SAW.Recognizer
   , asConstant
   , asExtCns
   , asSort
-  , asISort
+  , asSortWithFlags
     -- * Prelude recognizers.
   , asBool
   , asBoolType
@@ -340,12 +340,12 @@ asSort t = do
     Sort s _ -> return s
     _      -> Nothing
 
-asISort :: Recognizer Term Sort
-asISort t = do
+asSortWithFlags :: Recognizer Term (Sort, SortFlags)
+asSortWithFlags t = do
   ftf <- asFTermF t
   case ftf of
-    Sort s True -> return s
-    _           -> Nothing
+    Sort s h -> return (s, h)
+    _      -> Nothing