Merge pull request #1609 from GaloisInc/cryptol-abstract-types

Mr Solver support for monadic Cryptol specs

cryptol-saw-core/saw/CryptolM.sawcore

@@ -24,12 +24,20 @@ numAssertEqM n m =
 isFinite : Num -> Prop;
 isFinite = Num_rec (\ (_:Num) -> Prop) (\ (_:Nat) -> TrueProp) FalseProp;
 
+-- Check whether a Num is finite
+checkFinite : (n:Num) -> Maybe (isFinite n);
+checkFinite =
+  Num_rec (\ (n:Num) -> Maybe (isFinite n))
+          (\ (n:Nat) -> Just (isFinite (TCNum n)) (Refl Bool True))
+          (Nothing (isFinite TCInf));
+
 -- Assert that a Num is finite, or fail
 assertFiniteM : (n:Num) -> CompM (isFinite n);
-assertFiniteM =
-  Num_rec (\ (n:Num) -> CompM (isFinite n))
-          (\ (_:Nat) -> returnM TrueProp TrueI)
-          (errorM FalseProp "assertFiniteM: Num not finite");
+assertFiniteM n =
+  maybe (isFinite n) (CompM (isFinite n))
+        (errorM (isFinite n) "assertFiniteM: Num not finite")
+        (returnM (isFinite n))
+        (checkFinite n);
 
 -- Recurse over a Num known to be finite
 Num_rec_fin : (p: Num -> sort 1) -> ((n:Nat) -> p (TCNum n)) ->

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

@@ -82,10 +82,13 @@ data Env = Env
   , envC :: Map C.Name C.Schema    -- ^ Cryptol type environment
   , envS :: [Term]                 -- ^ SAW-Core bound variable environment (for type checking)
   , envRefPrims :: Map C.PrimIdent C.Expr
+  , envPrims :: Map C.PrimIdent Term -- ^ Translations for other primitives
+  , envPrimTypes :: Map C.PrimIdent Term -- ^ Translations for primitive types
   }
 
 emptyEnv :: Env
-emptyEnv = Env Map.empty Map.empty Map.empty Map.empty [] Map.empty
+emptyEnv =
+  Env Map.empty Map.empty Map.empty Map.empty [] Map.empty Map.empty Map.empty
 
 liftTerm :: (Term, Int) -> (Term, Int)
 liftTerm (t, j) = (t, j + 1)
@@ -102,6 +105,8 @@ liftEnv env =
       , envC = envC env
       , envS = envS env
       , envRefPrims = envRefPrims env
+      , envPrims = envPrims env
+      , envPrimTypes = envPrimTypes env
       }
 
 bindTParam :: SharedContext -> C.TParam -> Env -> IO Env
@@ -262,7 +267,11 @@ importType sc env ty =
                                b <- go (tyargs !! 1)
                                scFun sc a b
             C.TCTuple _n -> scTupleType sc =<< traverse go tyargs
-            C.TCAbstract{} -> panic "importType TODO: abstract type" []
+            C.TCAbstract (C.UserTC n _)
+              | Just prim <- C.asPrim n
+              , Just t <- Map.lookup prim (envPrimTypes env) ->
+                scApplyAllBeta sc t =<< traverse go tyargs
+              | True -> panic ("importType: unknown primitive type: " ++ show n) []
         C.PC pc ->
           case pc of
             C.PLiteral -> -- we omit first argument to class Literal
@@ -668,6 +677,9 @@ importPrimitive sc primOpts env n sch
          nmi <- importName n
          scConstant' sc nmi e t
 
+  -- lookup primitive in the extra primitive lookup table
+  | Just nm <- C.asPrim n, Just t <- Map.lookup nm (envPrims env) = return t
+
   -- Optionally, create an opaque constant representing the primitive
   -- if it doesn't match one of the ones we know about.
   | Just _ <- C.asPrim n, allowUnknownPrimitives primOpts =

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

@@ -398,6 +398,7 @@ monadifyType ctx tp@(asPi -> Just (_, _, tp_out))
 monadifyType ctx tp@(asPi -> Just (x, tp_in, tp_out)) =
   MTyArrow (monadifyType ctx tp_in)
   (monadifyType ((x,tp,Nothing):ctx) tp_out)
+monadifyType _ (asTupleType -> Just []) = mkMonType0 unitTypeOpenTerm
 monadifyType ctx (asPairType -> Just (tp1, tp2)) =
   MTyPair (monadifyType ctx tp1) (monadifyType ctx tp2)
 monadifyType ctx (asRecordType -> Just tps) =
@@ -529,6 +530,36 @@ fromCompTerm :: MonType -> OpenTerm -> MonTerm
 fromCompTerm mtp t | isBaseType mtp = CompMonTerm mtp t
 fromCompTerm mtp t = ArgMonTerm $ fromArgTerm mtp t
 
+-- | Test if a monadification type @tp@ is pure, meaning @MT(tp)=tp@
+monTypeIsPure :: MonType -> Bool
+monTypeIsPure (MTyForall _ _ _) = False -- NOTE: this could potentially be true
+monTypeIsPure (MTyArrow _ _) = False
+monTypeIsPure (MTySeq _ _) = False
+monTypeIsPure (MTyPair mtp1 mtp2) = monTypeIsPure mtp1 && monTypeIsPure mtp2
+monTypeIsPure (MTyRecord fld_mtps) = all (monTypeIsPure . snd) fld_mtps
+monTypeIsPure (MTyBase _ _) = True
+monTypeIsPure (MTyNum _) = True
+
+-- | Test if a monadification type @tp@ is semi-pure, meaning @SemiP(tp) = tp@,
+-- where @SemiP@ is defined in the documentation for 'fromSemiPureTermFun' below
+monTypeIsSemiPure :: MonType -> Bool
+monTypeIsSemiPure (MTyForall _ k tp_f) =
+  monTypeIsSemiPure $ tp_f $ MTyBase k $
+  -- This dummy OpenTerm should never be inspected by the recursive call
+  error "monTypeIsSemiPure"
+monTypeIsSemiPure (MTyArrow tp_in tp_out) =
+  monTypeIsPure tp_in && monTypeIsSemiPure tp_out
+monTypeIsSemiPure (MTySeq _ _) = False
+monTypeIsSemiPure (MTyPair mtp1 mtp2) =
+  -- NOTE: functions in pairs are not semi-pure; only pure types in pairs are
+  -- semi-pure
+  monTypeIsPure mtp1 && monTypeIsPure mtp2
+monTypeIsSemiPure (MTyRecord fld_mtps) =
+  -- Same as pairs, record types are only semi-pure if they are pure
+  all (monTypeIsPure . snd) fld_mtps
+monTypeIsSemiPure (MTyBase _ _) = True
+monTypeIsSemiPure (MTyNum _) = True
+
 -- | Build a monadification term from a function on terms which, when viewed as
 -- a lambda, is a "semi-pure" function of the given monadification type, meaning
 -- it maps terms of argument type @MT(tp)@ to an output value of argument type;
@@ -857,8 +888,13 @@ monadifyTerm' _ (asApplyAll -> (asTypedGlobalDef -> Just glob, args)) =
     do let (macro_args, reg_args) = splitAt (macroNumArgs macro) args
        mtrm_f <- macroApply macro glob macro_args
        monadifyApply mtrm_f reg_args
-  Nothing -> error ("Monadification failed: unhandled constant: "
-                    ++ globalDefString glob)
+  Nothing ->
+    monadifyTypeM (globalDefType glob) >>= \glob_mtp ->
+    if monTypeIsSemiPure glob_mtp then
+      monadifyApply (ArgMonTerm $ fromSemiPureTerm glob_mtp $
+                     globalDefOpenTerm glob) args
+    else error ("Monadification failed: unhandled constant: "
+                ++ globalDefString glob)
 monadifyTerm' _ (asApp -> Just (f, arg)) =
   do mtrm_f <- monadifyTerm Nothing f
      monadifyApply mtrm_f [arg]
@@ -959,6 +995,25 @@ iteMacro = MonMacro 4 $ \_ args ->
          [toCompType mtp, toArgTerm atrm_cond,
           toCompTerm mtrm1, toCompTerm mtrm2]
 
+-- | The macro for the either elimination function, which converts the
+-- application @either a b c@ to @either a b (CompM c)@
+eitherMacro :: MonMacro
+eitherMacro = MonMacro 3 $ \_ args ->
+  do let (tp_a, tp_b, tp_c) =
+           case args of
+             [t1, t2, t3] -> (t1, t2, t3)
+             _ -> error "eitherMacro: wrong number of arguments!"
+     mtp_a <- monadifyTypeM tp_a
+     mtp_b <- monadifyTypeM tp_b
+     mtp_c <- monadifyTypeM tp_c
+     let eith_app = applyGlobalOpenTerm "Prelude.either" [toArgType mtp_a,
+                                                          toArgType mtp_b,
+                                                          toCompType mtp_c]
+     let tp_eith = dataTypeOpenTerm "Prelude.Either" [toArgType mtp_a,
+                                                      toArgType mtp_b]
+     return $ fromCompTerm (MTyArrow (MTyArrow mtp_a mtp_c)
+                            (MTyArrow (MTyArrow mtp_b mtp_c)
+                             (MTyArrow (mkMonType0 tp_eith) mtp_c))) eith_app
 
 -- | Make a 'MonMacro' that maps a named global whose first argument is @n:Num@
 -- to a global of semi-pure type that takes an additional argument of type
@@ -1048,6 +1103,7 @@ defaultMonEnv =
     mmCustom "Prelude.unsafeAssert" unsafeAssertMacro
   , mmCustom "Prelude.ite" iteMacro
   , mmCustom "Prelude.fix" fixMacro
+  , mmCustom "Prelude.either" eitherMacro
 
     -- Top-level sequence functions
   , mmArg "Cryptol.seqMap" "CryptolM.seqMapM"

cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs

@@ -126,6 +126,8 @@ data CryptolEnv = CryptolEnv
   , eExtraTypes :: Map T.Name T.Schema  -- ^ Cryptol types for extra names in scope
   , eExtraTSyns :: Map T.Name T.TySyn   -- ^ Extra Cryptol type synonyms in scope
   , eTermEnv    :: Map T.Name Term      -- ^ SAWCore terms for *all* names in scope
+  , ePrims      :: Map C.PrimIdent Term -- ^ SAWCore terms for primitives
+  , ePrimTypes  :: Map C.PrimIdent Term -- ^ SAWCore terms for primitive type names
   }
 
 
@@ -217,6 +219,8 @@ initCryptolEnv sc = do
     , eExtraTypes = Map.empty
     , eExtraTSyns = Map.empty
     , eTermEnv    = termEnv
+    , ePrims      = Map.empty
+    , ePrimTypes  = Map.empty
     }
 
 -- Parse -----------------------------------------------------------------------
@@ -297,6 +301,8 @@ mkCryEnv env =
      let cryEnv = C.emptyEnv
            { C.envE = fmap (\t -> (t, 0)) terms
            , C.envC = types'
+           , C.envPrims = ePrims env
+           , C.envPrimTypes = ePrimTypes env
            }
      return cryEnv
 

heapster-saw/examples/Either.cry

@@ -0,0 +1,10 @@
+
+/* The definition of the Either type as an abstract type in Cryptol */
+
+module Either where
+
+primitive type Either : * -> * -> *
+
+primitive Left : {a, b} a -> Either a b
+primitive Right : {a, b} b -> Either a b
+primitive either : {a, b, c} (a -> c) -> (b -> c) -> Either a b -> c

heapster-saw/examples/either.saw

@@ -0,0 +1,15 @@
+/* Helper SAW script for defining the Either type in Cryptol */
+
+eith_tp <- parse_core "\\ (a b:sort 0) -> Either a b";
+cryptol_add_prim_type "Either" "Either" eith_tp;
+
+left_fun <- parse_core "\\ (a b:sort 0) (x:a) -> Left a b x";
+cryptol_add_prim "Either" "Left" left_fun;
+
+right_fun <- parse_core "\\ (a b:sort 0) (x:b) -> Right a b x";
+cryptol_add_prim "Either" "Right" right_fun;
+
+either_fun <- parse_core "either";
+cryptol_add_prim "Either" "either" either_fun;
+
+import "Either.cry";

heapster-saw/examples/linked_list.cry

@@ -0,0 +1,14 @@
+
+module LinkedList where
+
+import Either
+
+primitive type List : * -> *
+
+primitive foldList : {a} Either () (a, List a) -> List a
+primitive unfoldList : {a} List a -> Either () (a, List a)
+
+is_elem_spec : [64] -> List [64] -> [64]
+is_elem_spec x l =
+  either (\ _ -> 0) (\ (y,l') -> if x == y then 1 else is_elem_spec x l')
+         (unfoldList l)

heapster-saw/examples/linked_list_mr_solver.saw

@@ -1,5 +1,9 @@
 include "linked_list.saw";
 
+/***
+ *** Testing infrastructure
+ ***/
+
 let eq_bool b1 b2 =
   if b1 then
     if b2 then true else false
@@ -15,12 +19,37 @@ let run_test name test expected =
          do { print "Test failed\n"; exit 1; }; };
 
 
+/***
+ *** Setup Cryptol environment
+ ***/
+
+include "either.saw";
+
+list_tp <- parse_core "\\ (a:sort 0) -> List a";
+cryptol_add_prim_type "LinkedList" "List" list_tp;
+
+fold_fun <- parse_core "foldList";
+cryptol_add_prim "LinkedList" "foldList" fold_fun;
+
+unfold_fun <- parse_core "unfoldList";
+cryptol_add_prim "LinkedList" "unfoldList" unfold_fun;
+
+import "linked_list.cry";
+
+
+/***
+ *** The actual tests
+ ***/
+
 heapster_typecheck_fun env "is_head"
   "(). arg0:int64<>, arg1:List<int64<>,always,R> -o \
      \ arg0:true, arg1:true, ret:int64<>";
 
+/*
 is_head <- parse_core_mod "linked_list" "is_head";
 run_test "is_head |= is_head" (mr_solver is_head is_head) true;
+*/
 
 is_elem <- parse_core_mod "linked_list" "is_elem";
-run_test "is_elem |= is_elem" (mr_solver is_elem is_elem) true;
+run_test "is_elem |= is_elem_spec" (mr_solver_debug 2 is_elem {{ is_elem_spec }}) true;
+//run_test "is_elem |= is_elem" (mr_solver_debug 1 is_elem is_elem) true;

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

@@ -108,6 +108,8 @@ module Verifier.SAW.SharedTerm
     -- *** Functions and function application
   , scApply
   , scApplyAll
+  , scApplyBeta
+  , scApplyAllBeta
   , scGlobalApply
   , scFun
   , scFunAll
@@ -1283,6 +1285,17 @@ betaNormalize sc t0 =
 scApplyAll :: SharedContext -> Term -> [Term] -> IO Term
 scApplyAll sc = foldlM (scApply sc)
 
+-- | Apply a function to an argument, beta-reducing if the function is a lambda
+scApplyBeta :: SharedContext -> Term -> Term -> IO Term
+scApplyBeta sc (asLambda -> Just (_, _, body)) arg =
+  instantiateVar sc 0 arg body
+scApplyBeta sc f arg = scApply sc f arg
+
+-- | Apply a function 'Term' to zero or more arguments, beta reducing any time
+-- the function is a lambda
+scApplyAllBeta :: SharedContext -> Term -> [Term] -> IO Term
+scApplyAllBeta sc = foldlM (scApplyBeta sc)
+
 -- | Returns the defined constant with the given 'Ident'. Fails if no
 -- such constant exists in the module.
 scLookupDef :: SharedContext -> Ident -> IO Term

src/SAWScript/Builtins.hs

@@ -106,7 +106,8 @@ import qualified Cryptol.Backend.Monad as C (runEval)
 import qualified Cryptol.Eval.Type as C (evalType)
 import qualified Cryptol.Eval.Value as C (fromVBit, fromVWord)
 import qualified Cryptol.Eval.Concrete as C (Concrete(..), bvVal)
-import qualified Cryptol.Utils.Ident as C (mkIdent, packModName)
+import qualified Cryptol.Utils.Ident as C (mkIdent, packModName,
+                                           textToModName, PrimIdent(..))
 import qualified Cryptol.Utils.RecordMap as C (recordFromFields)
 
 import qualified SAWScript.SBVParser as SBV
@@ -1526,6 +1527,27 @@ cryptol_add_path path =
      let rw' = rw { rwCryptol = ce' }
      putTopLevelRW rw'
 
+cryptol_add_prim :: String -> String -> TypedTerm -> TopLevel ()
+cryptol_add_prim mnm nm trm =
+  do rw <- getTopLevelRW
+     let env = rwCryptol rw
+     let prim_name =
+           C.PrimIdent (C.textToModName $ Text.pack mnm) (Text.pack nm)
+     let env' =
+           env { CEnv.ePrims =
+                   Map.insert prim_name (ttTerm trm) (CEnv.ePrims env) }
+     putTopLevelRW (rw { rwCryptol = env' })
+
+cryptol_add_prim_type :: String -> String -> TypedTerm -> TopLevel ()
+cryptol_add_prim_type mnm nm tp =
+  do rw <- getTopLevelRW
+     let env = rwCryptol rw
+     let prim_name =
+           C.PrimIdent (C.textToModName $ Text.pack mnm) (Text.pack nm)
+     let env' = env { CEnv.ePrimTypes =
+                        Map.insert prim_name (ttTerm tp) (CEnv.ePrimTypes env) }
+     putTopLevelRW (rw { rwCryptol = env' })
+
 -- | Call 'Cryptol.importSchema' using a 'CEnv.CryptolEnv'
 importSchemaCEnv :: SharedContext -> CEnv.CryptolEnv -> Cryptol.Schema ->
                     IO Term

src/SAWScript/Interpreter.hs

@@ -1878,6 +1878,20 @@ primitives = Map.fromList
     , "Cryptol source files."
     ]
 
+  , prim "cryptol_add_prim"    "String -> String -> Term -> TopLevel ()"
+    (pureVal cryptol_add_prim)
+    Experimental
+    [ "cryptol_add_prim mod nm trm sets the translation of Cryptol primitive"
+    , "nm in module mod to trm"
+    ]
+
+  , prim "cryptol_add_prim_type"    "String -> String -> Term -> TopLevel ()"
+    (pureVal cryptol_add_prim_type)
+    Experimental
+    [ "cryptol_add_prim_type mod nm tp sets the translation of Cryptol"
+    , "primitive type nm in module mod to tp"
+    ]
+
   -- Java stuff
 
   , prim "java_bool"           "JavaType"