Merge pull request #1844 from GaloisInc/monadify-coq-module

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/Language/Coq/AST.hs

@@ -42,11 +42,15 @@ data Term
 -- | Type synonym useful for indicating when a term is used as a type.
 type Type = Term
 
+-- | An 'Ident' with an optional 'Type', which may be explicit or implicit.
+-- For use representing the bound variables in 'Lambda's, 'Let's, etc.
 data Binder
   = Binder Ident (Maybe Type)
   | ImplicitBinder Ident (Maybe Type)
     deriving (Show)
 
+-- | An 'Type' with an optional 'Ident', which may be explicit or implicit.
+-- For use representing arguments in 'Pi' types.
 data PiBinder
   = PiBinder (Maybe Ident) Type
   | PiImplicitBinder (Maybe Ident) Type

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

@@ -455,68 +455,90 @@ freshenAndBindName n =
 mkLet :: (Coq.Ident, Coq.Term) -> Coq.Term -> Coq.Term
 mkLet (name, rhs) body = Coq.Let name [] Nothing rhs body
 
+-- | Given a list of 'LocalName's and their corresponding types (as 'Term's),
+-- return a list of explicit 'Binder's, for use representing the bound
+-- variables in 'Lambda's, 'Let's, etc.
 translateParams ::
   TermTranslationMonad m =>
   [(LocalName, Term)] -> m [Coq.Binder]
 translateParams bs = concat <$> mapM translateParam bs
 
+-- | Given a 'LocalName' and its type (as a 'Term'), return an explicit
+-- 'Binder', for use representing a bound variable in a 'Lambda',
+-- 'Let', etc.
 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
+
+-- | Given a list of 'LocalName's and their corresponding types (as 'Term's)
+-- representing argument types and a 'Term' representing the return type,
+-- return the resulting 'Pi', with additional implicit arguments added after
+-- each instance of @isort@, @qsort@, etc.
 translatePi :: TermTranslationMonad m => [(LocalName, Term)] -> Term -> m Coq.Term
 translatePi binders body = withLocalTranslationState $ do
   bindersT <- concat <$> mapM translatePiBinder binders
   bodyT <- translateTermLet body
   return $ Coq.Pi bindersT bodyT
 
+-- | Given a 'LocalName' and its type (as a 'Term'), return an explicit
+-- 'PiBinder' followed by zero or more implicit 'PiBinder's representing
+-- additonal implicit typeclass arguments, added if the given type is @isort@,
+-- @qsort@, etc.
 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
+
+-- | Given a 'LocalName' and its type (as a 'Term'), return the translation of
+-- the 'LocalName' as an 'Ident', the translation of the type as a 'Type',
+-- and zero or more additional 'Ident's and 'Type's representing additonal
+-- implicit typeclass arguments, added if the given type is @isort@, etc.
 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)
+
+-- | Given a typeclass (as a 'Term'), a list of 'LocalName's and their
+-- corresponding types (as 'Term's), and a type-level function with argument
+-- types given by the prior list, return a 'Pi' of the given arguments, inside
+-- of which is an 'App' of the typeclass to the fully-applied type-level
+-- function
+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)))