From 63bc072e91cdd7207c808681039743e7cac2276b Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Wed, 9 Mar 2022 15:51:52 -0800 Subject: [PATCH 01/15] added the cryptol_add_prim_type SAW command to set the translation of Cryptol abstract types --- cryptol-saw-core/src/Verifier/SAW/Cryptol.hs | 10 ++++++++-- cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs | 3 +++ src/SAWScript/Builtins.hs | 13 ++++++++++++- src/SAWScript/Interpreter.hs | 7 +++++++ 4 files changed, 30 insertions(+), 3 deletions(-) diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs index acf988b2c5..e678bf34e4 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs @@ -82,10 +82,11 @@ 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 + , 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 liftTerm :: (Term, Int) -> (Term, Int) liftTerm (t, j) = (t, j + 1) @@ -102,6 +103,7 @@ liftEnv env = , envC = envC env , envS = envS env , envRefPrims = envRefPrims env + , envPrimTypes = envPrimTypes env } bindTParam :: SharedContext -> C.TParam -> Env -> IO Env @@ -262,7 +264,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) -> + return t + | True -> panic ("importType: unknown primitive type: " ++ show n) [] C.PC pc -> case pc of C.PLiteral -> -- we omit first argument to class Literal diff --git a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs index 1e9a9fc9ad..70ebb0c2d3 100644 --- a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs +++ b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs @@ -126,6 +126,7 @@ 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 + , ePrimTypes :: Map C.PrimIdent Term -- ^ SAWCore terms for primitive type names } @@ -217,6 +218,7 @@ initCryptolEnv sc = do , eExtraTypes = Map.empty , eExtraTSyns = Map.empty , eTermEnv = termEnv + , ePrimTypes = Map.empty } -- Parse ----------------------------------------------------------------------- @@ -297,6 +299,7 @@ mkCryEnv env = let cryEnv = C.emptyEnv { C.envE = fmap (\t -> (t, 0)) terms , C.envC = types' + , C.envPrimTypes = ePrimTypes env } return cryEnv diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index 1765ce785b..bf5b995de9 100644 --- a/src/SAWScript/Builtins.hs +++ b/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,16 @@ cryptol_add_path path = let rw' = rw { rwCryptol = ce' } putTopLevelRW rw' +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 diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 4a4b2c8f10..6e5a890a12 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -1878,6 +1878,13 @@ primitives = Map.fromList , "Cryptol source files." ] + , prim "cryptol_add_prim_type" "String -> String -> Term -> TopLevel ()" + (pureVal cryptol_add_prim_type) + Current + [ "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" From c0b9ed38b6f2d45cfa02e403dac419dfba7579a7 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Wed, 9 Mar 2022 15:58:27 -0800 Subject: [PATCH 02/15] whoops, marked cryptol_add_prim_type as experimental --- src/SAWScript/Interpreter.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 6e5a890a12..2e746e155f 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -1880,7 +1880,7 @@ primitives = Map.fromList , prim "cryptol_add_prim_type" "String -> String -> Term -> TopLevel ()" (pureVal cryptol_add_prim_type) - Current + Experimental [ "cryptol_add_prim_type mod nm tp sets the translation of Cryptol" , "primitive type nm in module mod to tp" ] From 7952a1d0751c313e1038fad536362b410cae783d Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Wed, 9 Mar 2022 17:10:42 -0800 Subject: [PATCH 03/15] added cryptol_add_prim; also fixed a bug in translating abstract types, where the translation of the types were not getting applied --- cryptol-saw-core/src/Verifier/SAW/Cryptol.hs | 10 ++++++++-- cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs | 5 ++++- saw-core/src/Verifier/SAW/SharedTerm.hs | 13 +++++++++++++ src/SAWScript/Builtins.hs | 11 +++++++++++ src/SAWScript/Interpreter.hs | 7 +++++++ 5 files changed, 43 insertions(+), 3 deletions(-) diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs index e678bf34e4..e61eaff02e 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs @@ -82,11 +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 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) @@ -103,6 +105,7 @@ liftEnv env = , envC = envC env , envS = envS env , envRefPrims = envRefPrims env + , envPrims = envPrims env , envPrimTypes = envPrimTypes env } @@ -267,7 +270,7 @@ importType sc env ty = C.TCAbstract (C.UserTC n _) | Just prim <- C.asPrim n , Just t <- Map.lookup prim (envPrimTypes env) -> - return t + scApplyAllBeta sc t =<< traverse go tyargs | True -> panic ("importType: unknown primitive type: " ++ show n) [] C.PC pc -> case pc of @@ -674,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 = diff --git a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs index 70ebb0c2d3..13e6689366 100644 --- a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs +++ b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs @@ -126,6 +126,7 @@ 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 } @@ -218,7 +219,8 @@ initCryptolEnv sc = do , eExtraTypes = Map.empty , eExtraTSyns = Map.empty , eTermEnv = termEnv - , ePrimTypes = Map.empty + , ePrims = Map.empty + , ePrimTypes = Map.empty } -- Parse ----------------------------------------------------------------------- @@ -299,6 +301,7 @@ 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 diff --git a/saw-core/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs index ef6b1146c8..4a8cde027a 100644 --- a/saw-core/src/Verifier/SAW/SharedTerm.hs +++ b/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 diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index bf5b995de9..4edc37ef2d 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -1527,6 +1527,17 @@ 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 diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 2e746e155f..2b11857fb3 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -1878,6 +1878,13 @@ 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 From eb4ed6a694415b9c5c5d8d6eff0202af6ff61fa4 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Thu, 10 Mar 2022 06:41:52 -0800 Subject: [PATCH 04/15] added a macro for monadifying the either eliminator --- .../src/Verifier/SAW/Cryptol/Monadify.hs | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs index 526990782e..ea79ee1b21 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs @@ -959,6 +959,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 +1067,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" From 747d31f288555c2fa48e52480513d9dbf5818034 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Thu, 10 Mar 2022 07:23:01 -0800 Subject: [PATCH 05/15] changed cryptol monadification to translate any global of semi-pure type to itself --- .../src/Verifier/SAW/Cryptol/Monadify.hs | 40 ++++++++++++++++++- 1 file changed, 38 insertions(+), 2 deletions(-) diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs index ea79ee1b21..b296dabb4d 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs +++ b/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] From fa1110a94372a311a1d3498ffa9053ea3565edf7 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Thu, 10 Mar 2022 07:29:45 -0800 Subject: [PATCH 06/15] added a case to computation normalization in Mr Solver to handle beta redexes --- src/SAWScript/Prover/MRSolver/Solver.hs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs index fbde43b184..8d7fb09157 100644 --- a/src/SAWScript/Prover/MRSolver/Solver.hs +++ b/src/SAWScript/Prover/MRSolver/Solver.hs @@ -209,6 +209,8 @@ normComp (CompBind m f) = normComp (CompTerm t) = withFailureCtx (FailCtxMNF t) $ case asApplyAll t of + (f@(asLambda -> Just _), args) -> + mrApplyAll f args >>= normCompTerm (isGlobalDef "Prelude.returnM" -> Just (), [_, x]) -> return $ ReturnM x (isGlobalDef "Prelude.bindM" -> Just (), [_, _, m, f]) -> From a25cefcfd4da60cea21d5068377c8fc904916d84 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Thu, 10 Mar 2022 11:10:01 -0800 Subject: [PATCH 07/15] changed mrApplyAll to use the new scApplyAllBeta combinator rather than beta normalizing the entire output term --- src/SAWScript/Prover/MRSolver/Monad.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs index 433a4a382f..48ed75dc43 100644 --- a/src/SAWScript/Prover/MRSolver/Monad.hs +++ b/src/SAWScript/Prover/MRSolver/Monad.hs @@ -448,7 +448,7 @@ funNameType (GlobalName gd projs) = -- | Apply a 'Term' to a list of arguments and beta-reduce in Mr. Monad mrApplyAll :: Term -> [Term] -> MRM Term -mrApplyAll f args = liftSC2 scApplyAll f args >>= liftSC1 betaNormalize +mrApplyAll f args = liftSC2 scApplyAllBeta f args -- | Get the current context of uvars as a list of variable names and their -- types as SAW core 'Term's, with the least recently bound uvar first, i.e., in From 235dcf4b1399f8a53aee66bb7f68ab12ddf6b98f Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Thu, 10 Mar 2022 11:11:47 -0800 Subject: [PATCH 08/15] trying to prove is_elem refines a cryptol spec for its behavior --- heapster-saw/examples/Either.cry | 10 ++++++++++ heapster-saw/examples/either.saw | 15 +++++++++++++++ heapster-saw/examples/linked_list.cry | 14 ++++++++++++++ 3 files changed, 39 insertions(+) create mode 100644 heapster-saw/examples/Either.cry create mode 100644 heapster-saw/examples/either.saw create mode 100644 heapster-saw/examples/linked_list.cry diff --git a/heapster-saw/examples/Either.cry b/heapster-saw/examples/Either.cry new file mode 100644 index 0000000000..6adf0f39e0 --- /dev/null +++ b/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 diff --git a/heapster-saw/examples/either.saw b/heapster-saw/examples/either.saw new file mode 100644 index 0000000000..b711c9a8fb --- /dev/null +++ b/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"; diff --git a/heapster-saw/examples/linked_list.cry b/heapster-saw/examples/linked_list.cry new file mode 100644 index 0000000000..85e63ec8c4 --- /dev/null +++ b/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) From 8ec0be1bc643df324b481ef25eaad8e3ea625582 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Thu, 10 Mar 2022 12:32:49 -0800 Subject: [PATCH 09/15] reimplemented assertFiniteM to use the maybe eliminator --- cryptol-saw-core/saw/CryptolM.sawcore | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/cryptol-saw-core/saw/CryptolM.sawcore b/cryptol-saw-core/saw/CryptolM.sawcore index 452fb45cbc..61df5156f2 100644 --- a/cryptol-saw-core/saw/CryptolM.sawcore +++ b/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)) -> From 09681ad2348c36367af691848eab3d514ddc8d56 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Thu, 10 Mar 2022 13:53:36 -0800 Subject: [PATCH 10/15] added support to Mr Solver for maybe eliminators over isFinite proofs --- src/SAWScript/Prover/MRSolver/Monad.hs | 28 +++++++++++++-- src/SAWScript/Prover/MRSolver/Solver.hs | 46 ++++++++++++++++++++++--- 2 files changed, 67 insertions(+), 7 deletions(-) diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs index 48ed75dc43..9e8acd6c60 100644 --- a/src/SAWScript/Prover/MRSolver/Monad.hs +++ b/src/SAWScript/Prover/MRSolver/Monad.hs @@ -229,12 +229,15 @@ instance PrettyInCtx CoIndHyp where -- | An assumption that something is equal to one of the constructors of a -- datatype, e.g. equal to @Left@ of some 'Term' or @Right@ of some 'Term' -data DataTypeAssump = IsLeft Term | IsRight Term - deriving (Generic, Show, TermLike) +data DataTypeAssump + = IsLeft Term | IsRight Term | IsNum Term | IsInf + deriving (Generic, Show, TermLike) instance PrettyInCtx DataTypeAssump where prettyInCtx (IsLeft x) = prettyInCtx x >>= ppWithPrefix "Left _ _" prettyInCtx (IsRight x) = prettyInCtx x >>= ppWithPrefix "Right _ _" + prettyInCtx (IsNum x) = prettyInCtx x >>= ppWithPrefix "TCNum" + prettyInCtx (IsRight x) = prettyInCtx x >>= ppWithPrefix "TCInf" -- | Recognize a term as a @Left@ or @Right@ asEither :: Recognizer Term (Either Term Term) @@ -243,6 +246,20 @@ asEither (asCtor -> Just (c, [_, _, x])) | primName c == "Prelude.Right" = return $ Right x asEither _ = Nothing +-- | Recognize a term as a @TCNum n@ or @TCInf@ +asNum :: Recognizer Term (Either Term ()) +asNum (asCtor -> Just (c, [n])) + | primName c == "Cryptol.TCNum" = return $ Left n +asNum (asCtor -> Just (c, [])) + | primName c == "Cryptol.TCInf" = return $ Right () +asNum _ = Nothing + +-- | Recognize a term as being of the form @isFinite n@ +asIsFinite :: Recognizer Term Term +asIsFinite (asApp -> Just (isGlobalDef "CryptolM.isFinite" -> Just (), n)) = + Just n +asIsFinite _ = Nothing + -- | A map from 'Term's to 'DataTypeAssump's over that term type DataTypeAssumps = HashMap Term DataTypeAssump @@ -590,6 +607,13 @@ mrVarTerm (MRVar ec) = vars <- getAllUVarTerms liftSC2 scApplyAll var_tm vars +-- | Create a dummy proof term of the specified type, which can be open but +-- should be of @Prop@ sort, by creating an 'ExtCns' axiom. This is sound as +-- long as we only use the resulting term in computation branches where we know +-- the proposition holds. +mrDummyProof :: Term -> MRM Term +mrDummyProof tp = piUVarsM tp >>= mrFreshVar "pf" >>= mrVarTerm + -- | Get the 'VarInfo' associated with a 'MRVar' mrVarInfo :: MRVar -> MRM (Maybe MRVarInfo) mrVarInfo var = Map.lookup var <$> mrVars diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs index 8d7fb09157..758d2acdd9 100644 --- a/src/SAWScript/Prover/MRSolver/Solver.hs +++ b/src/SAWScript/Prover/MRSolver/Solver.hs @@ -497,28 +497,64 @@ mrRefines' (ErrorM _) (ErrorM _) = return () mrRefines' (ReturnM e) (ErrorM _) = throwMRFailure (ReturnNotError e) mrRefines' (ErrorM _) (ReturnM e) = throwMRFailure (ReturnNotError e) --- FIXME: Add support for arbitrary maybe asusmptions, like the either case +-- A maybe eliminator on an equality type on the left mrRefines' (MaybeElim (Type (asEq -> Just (tp,e1,e2))) m1 f1 _) m2 = do cond <- mrEq' tp e1 e2 not_cond <- liftSC1 scNot cond - cond_pf <- - liftSC1 scEqTrue cond >>= piUVarsM >>= mrFreshVar "pf" >>= mrVarTerm + cond_pf <- liftSC1 scEqTrue cond >>= mrDummyProof m1' <- applyNormCompFun f1 cond_pf cond_holds <- mrProvable cond if cond_holds then mrRefines m1' m2 else withAssumption cond (mrRefines m1' m2) >> withAssumption not_cond (mrRefines m1 m2) + +-- A maybe eliminator on an equality type on the right mrRefines' m1 (MaybeElim (Type (asEq -> Just (tp,e1,e2))) m2 f2 _) = do cond <- mrEq' tp e1 e2 not_cond <- liftSC1 scNot cond - cond_pf <- - liftSC1 scEqTrue cond >>= piUVarsM >>= mrFreshVar "pf" >>= mrVarTerm + cond_pf <- liftSC1 scEqTrue cond >>= mrDummyProof m2' <- applyNormCompFun f2 cond_pf cond_holds <- mrProvable cond if cond_holds then mrRefines m1 m2' else withAssumption cond (mrRefines m1 m2') >> withAssumption not_cond (mrRefines m1 m2) +-- A maybe eliminator on an isFinite type on the left +mrRefines' (MaybeElim (Type (asIsFinite -> Just n1)) m1 f1 _) m2 = + do n1_norm <- liftSC1 scWhnf n1 + maybe_assump <- mrGetDataTypeAssump n1_norm + fin_pf <- + liftSC2 scGlobalApply "CryptolM.isFinite" [n1_norm] >>= mrDummyProof + case (maybe_assump, asNum n1_norm) of + (_, Just (Left _)) -> applyNormCompFun f1 fin_pf >>= flip mrRefines m2 + (_, Just (Right _)) -> mrRefines m1 m2 + (Just (IsNum _), _) -> applyNormCompFun f1 fin_pf >>= flip mrRefines m2 + (Just IsInf, _) -> mrRefines m1 m2 + _ -> + withDataTypeAssump n1_norm IsInf (mrRefines m1 m2) >> + liftSC0 scNatType >>= \nat_tp -> + (withUVarLift "n" (Type nat_tp) (n1_norm, f1, m2) $ \ n (n1', f1', m2') -> + withDataTypeAssump n1' (IsNum n) + (applyNormCompFun f1' n >>= flip mrRefines m2')) + +-- A maybe eliminator on an isFinite type on the right +mrRefines' m1 (MaybeElim (Type (asIsFinite -> Just n2)) m2 f2 _) = + do n2_norm <- liftSC1 scWhnf n2 + maybe_assump <- mrGetDataTypeAssump n2_norm + fin_pf <- + liftSC2 scGlobalApply "CryptolM.isFinite" [n2_norm] >>= mrDummyProof + case (maybe_assump, asNum n2_norm) of + (_, Just (Left _)) -> applyNormCompFun f2 fin_pf >>= mrRefines m1 + (_, Just (Right _)) -> mrRefines m1 m2 + (Just (IsNum _), _) -> applyNormCompFun f2 fin_pf >>= mrRefines m1 + (Just IsInf, _) -> mrRefines m1 m2 + _ -> + withDataTypeAssump n2_norm IsInf (mrRefines m1 m2) >> + liftSC0 scNatType >>= \nat_tp -> + (withUVarLift "n" (Type nat_tp) (n2_norm, f2, m1) $ \ n (n2', f2', m1') -> + withDataTypeAssump n2' (IsNum n) + (applyNormCompFun f2' n >>= mrRefines m1')) + mrRefines' (Ite cond1 m1 m1') m2 = liftSC1 scNot cond1 >>= \not_cond1 -> mrProvable cond1 >>= \cond1_true_pv-> From 6cacfc5974123a5f63d64065d069802ad364961c Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Thu, 10 Mar 2022 15:15:17 -0800 Subject: [PATCH 11/15] added support for CompM types during normalization with normSMTProp --- src/SAWScript/Prover/MRSolver/SMT.hs | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/src/SAWScript/Prover/MRSolver/SMT.hs b/src/SAWScript/Prover/MRSolver/SMT.hs index 04f85ece7f..6a63e8e5a3 100644 --- a/src/SAWScript/Prover/MRSolver/SMT.hs +++ b/src/SAWScript/Prover/MRSolver/SMT.hs @@ -1,6 +1,7 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE ImplicitParams #-} {- | Module : SAWScript.Prover.MRSolver.SMT @@ -136,7 +137,16 @@ smtNormPrims sc = Map.fromList PrimFun $ \_n -> PrimFun $ \_len -> tvalFun $ \a -> primGenBVVec sc $ \f -> primBVTermFun sc $ \ix -> PrimFun $ \_pf -> Prim (VExtra <$> VExtraTerm a <$> scApply sc f ix) - ) + ), + ("Prelude.CompM", + PrimFilterFun "CompM" (\case + TValue tv -> return tv + _ -> mzero) $ \tv -> + Prim (do let ?recordEC = \_ec -> return () + let cfg = error "FIXME: smtNormPrims: need the simulator config" + tv_trm <- readBackTValue sc cfg tv + TValue <$> VTyTerm (mkSort 0) <$> + scGlobalApply sc "Prelude.CompM" [tv_trm])) ] -- | Normalize a 'Term' before building an SMT query for it From 5daa95aee27a8cd76fc884aaec8df040289eb7ff Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Thu, 10 Mar 2022 15:15:58 -0800 Subject: [PATCH 12/15] changed the handling for normalizing multiFixM so that the function being called is not unfolded during normalization; also added a special case for normalizing multiArgFixM --- src/SAWScript/Prover/MRSolver/Solver.hs | 24 +++++++++++++----------- 1 file changed, 13 insertions(+), 11 deletions(-) diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs index 758d2acdd9..5dd5129902 100644 --- a/src/SAWScript/Prover/MRSolver/Solver.hs +++ b/src/SAWScript/Prover/MRSolver/Solver.hs @@ -251,21 +251,23 @@ normComp (CompTerm t) = mrApplyAll body args >>= normCompTerm -} + -- Recognize and unfold a multiArgFixM + (f@(isGlobalDef "Prelude.multiArgFixM" -> Just ()), args) + | Just (_, Just body) <- asConstant f -> + mrApplyAll body args >>= normCompTerm + -- Recognize (multiFixM lrts (\ f1 ... fn -> (body1, ..., bodyn))).i args (asTupleSelector -> Just (asApplyAll -> (isGlobalDef "Prelude.multiFixM" -> Just (), [lrts, defs_f]), - i), args) - -- Extract out the function \f1 ... fn -> bodyi - | Just (vars, body_i) <- synProjFunBody i defs_f -> - do - -- Bind fresh function variables for the functions f1 ... fn - fun_tms <- mrFreshLetRecVars lrts defs_f - -- Re-abstract the body - body_f <- liftSC2 scLambdaList vars body_i - -- Apply body_f to f1 ... fn and the top-level arguments - body_tm <- mrApplyAll body_f (fun_tms ++ args) - normComp (CompTerm body_tm) + i), args) -> + do + -- Bind fresh function variables for the functions f1 ... fn + fun_tms <- mrFreshLetRecVars lrts defs_f + -- Apply fi to the top-level arguments, keeping in mind that tuple + -- selectors are one-based, not zero-based, so we subtract 1 from i + body_tm <- mrApplyAll (fun_tms !! (i-1)) args + normComp (CompTerm body_tm) -- For an ExtCns, we have to check what sort of variable it is From 54be292c3b20945087b19eaf9a56c70c2a5a6378 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Thu, 10 Mar 2022 15:54:49 -0800 Subject: [PATCH 13/15] renamed normSMTProp to mrNormTerm, and added a mrNormOpenTerm function that can normalize open terms --- src/SAWScript/Prover/MRSolver/SMT.hs | 24 +++++++++++++++++++----- src/SAWScript/Prover/MRSolver/Solver.hs | 25 ++++++++----------------- 2 files changed, 27 insertions(+), 22 deletions(-) diff --git a/src/SAWScript/Prover/MRSolver/SMT.hs b/src/SAWScript/Prover/MRSolver/SMT.hs index 6a63e8e5a3..efb196f0bc 100644 --- a/src/SAWScript/Prover/MRSolver/SMT.hs +++ b/src/SAWScript/Prover/MRSolver/SMT.hs @@ -124,7 +124,7 @@ primBVTermFun sc = scVectorReduced sc tp tms v -> lift (putStrLn ("primBVTermFun: unhandled value: " ++ show v)) >> mzero --- | Implementations of primitives for normalizing SMT terms +-- | Implementations of primitives for normalizing Mr Solver terms smtNormPrims :: SharedContext -> Map Ident TmPrim smtNormPrims sc = Map.fromList [ @@ -149,15 +149,29 @@ smtNormPrims sc = Map.fromList scGlobalApply sc "Prelude.CompM" [tv_trm])) ] --- | Normalize a 'Term' before building an SMT query for it -normSMTProp :: Term -> MRM Term -normSMTProp t = +-- | Normalize a 'Term' using some Mr Solver specific primitives +mrNormTerm :: Term -> MRM Term +mrNormTerm t = debugPrint 2 "Normalizing term:" >> debugPrettyInCtx 2 t >> liftSC0 return >>= \sc -> liftSC0 scGetModuleMap >>= \modmap -> liftSC5 normalizeSharedTerm modmap (smtNormPrims sc) Map.empty Set.empty t +-- | Normalize an open term by wrapping it in lambdas, normalizing, and then +-- removing those lambdas +mrNormOpenTerm :: Term -> MRM Term +mrNormOpenTerm body = + do ctx <- mrUVarCtx + fun_term <- liftSC2 scLambdaList ctx body + normed_fun <- mrNormTerm fun_term + return (peel_lambdas (length ctx) normed_fun) + where + peel_lambdas :: Int -> Term -> Term + peel_lambdas 0 t = t + peel_lambdas i (asLambda -> Just (_, _, t)) = peel_lambdas (i-1) t + peel_lambdas _ _ = error "mrNormOpenTerm: unexpected non-lambda term!" + ---------------------------------------------------------------------- -- * Checking Provability with SMT @@ -192,7 +206,7 @@ mrProvable bool_tm = do assumps <- mrAssumptions prop <- liftSC2 scImplies assumps bool_tm >>= liftSC1 scEqTrue prop_inst <- instantiateUVarsM instUVar prop - normSMTProp prop_inst >>= mrProvableRaw + mrNormTerm prop_inst >>= mrProvableRaw where -- | Given a UVar name and type, generate a 'Term' to be passed to -- SMT, with special cases for BVVec and pair types instUVar :: LocalName -> Term -> MRM Term diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs index 5dd5129902..f6b711a1e7 100644 --- a/src/SAWScript/Prover/MRSolver/Solver.hs +++ b/src/SAWScript/Prover/MRSolver/Solver.hs @@ -152,18 +152,6 @@ asNestedPairs (asPairValue -> Just (x, asNestedPairs -> Just xs)) = Just (x:xs) asNestedPairs (asFTermF -> Just UnitValue) = Just [] asNestedPairs _ = Nothing --- | Syntactically project then @i@th element of the body of a lambda. That is, --- assuming the input 'Term' has the form --- --- > \ (x1:T1) ... (xn:Tn) -> (e1, (e2, ... (en, ()))) --- --- return the bindings @x1:T1,...,xn:Tn@ and @ei@ -synProjFunBody :: Int -> Term -> Maybe ([(LocalName, Term)], Term) -synProjFunBody i (asLambdaList -> (vars, asTupleValue -> Just es)) = - -- NOTE: we are doing 1-based indexing instead of 0-based, thus the -1 - Just $ (vars, es !! (i-1)) -synProjFunBody _ _ = Nothing - -- | Bind fresh function variables for a @letRecM@ or @multiFixM@ with the given -- @LetRecTypes@ and definitions for the function bodies as a lambda mrFreshLetRecVars :: Term -> Term -> MRM [Term] @@ -266,7 +254,10 @@ normComp (CompTerm t) = fun_tms <- mrFreshLetRecVars lrts defs_f -- Apply fi to the top-level arguments, keeping in mind that tuple -- selectors are one-based, not zero-based, so we subtract 1 from i - body_tm <- mrApplyAll (fun_tms !! (i-1)) args + body_tm <- + if i > 0 && i <= length fun_tms then + mrApplyAll (fun_tms !! (i-1)) args + else throwMRFailure (MalformedComp t) normComp (CompTerm body_tm) @@ -523,7 +514,7 @@ mrRefines' m1 (MaybeElim (Type (asEq -> Just (tp,e1,e2))) m2 f2 _) = -- A maybe eliminator on an isFinite type on the left mrRefines' (MaybeElim (Type (asIsFinite -> Just n1)) m1 f1 _) m2 = - do n1_norm <- liftSC1 scWhnf n1 + do n1_norm <- mrNormOpenTerm n1 maybe_assump <- mrGetDataTypeAssump n1_norm fin_pf <- liftSC2 scGlobalApply "CryptolM.isFinite" [n1_norm] >>= mrDummyProof @@ -541,7 +532,7 @@ mrRefines' (MaybeElim (Type (asIsFinite -> Just n1)) m1 f1 _) m2 = -- A maybe eliminator on an isFinite type on the right mrRefines' m1 (MaybeElim (Type (asIsFinite -> Just n2)) m2 f2 _) = - do n2_norm <- liftSC1 scWhnf n2 + do n2_norm <- mrNormOpenTerm n2 maybe_assump <- mrGetDataTypeAssump n2_norm fin_pf <- liftSC2 scGlobalApply "CryptolM.isFinite" [n2_norm] >>= mrDummyProof @@ -577,7 +568,7 @@ mrRefines' m1 (Ite cond2 m2 m2') = withAssumption not_cond2 (mrRefines m1 m2') mrRefines' (Either ltp1 rtp1 f1 g1 t1) m2 = - liftSC1 scWhnf t1 >>= \t1' -> + mrNormOpenTerm t1 >>= \t1' -> mrGetDataTypeAssump t1' >>= \mb_assump -> case (mb_assump, asEither t1') of (_, Just (Left x)) -> applyNormCompFun f1 x >>= flip mrRefines m2 @@ -593,7 +584,7 @@ mrRefines' (Either ltp1 rtp1 f1 g1 t1) m2 = applyNormCompFun g1' x >>= withDataTypeAssump t1'' (IsRight x) . flip mrRefines m2') mrRefines' m1 (Either ltp2 rtp2 f2 g2 t2) = - liftSC1 scWhnf t2 >>= \t2' -> + mrNormOpenTerm t2 >>= \t2' -> mrGetDataTypeAssump t2' >>= \mb_assump -> case (mb_assump, asEither t2') of (_, Just (Left x)) -> applyNormCompFun f2 x >>= mrRefines m1 From 648c5ba31776bb534b8cafdfd55f397003b3bf4a Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Thu, 10 Mar 2022 15:57:06 -0800 Subject: [PATCH 14/15] updated the linked_list_mr_solver.saw test case to prove that is_elem refines a cryptol version of its specification --- .../examples/linked_list_mr_solver.saw | 31 ++++++++++++++++++- 1 file changed, 30 insertions(+), 1 deletion(-) diff --git a/heapster-saw/examples/linked_list_mr_solver.saw b/heapster-saw/examples/linked_list_mr_solver.saw index 931e102351..c741d7e890 100644 --- a/heapster-saw/examples/linked_list_mr_solver.saw +++ b/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,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; From 3007ec9a850c3c3eb8e8ac0d4664c595af4b703c Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Fri, 11 Mar 2022 06:24:38 -0800 Subject: [PATCH 15/15] whoops, fixed some typos --- src/SAWScript/Prover/MRSolver/Monad.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs index 9e8acd6c60..71e79735ba 100644 --- a/src/SAWScript/Prover/MRSolver/Monad.hs +++ b/src/SAWScript/Prover/MRSolver/Monad.hs @@ -237,7 +237,7 @@ instance PrettyInCtx DataTypeAssump where prettyInCtx (IsLeft x) = prettyInCtx x >>= ppWithPrefix "Left _ _" prettyInCtx (IsRight x) = prettyInCtx x >>= ppWithPrefix "Right _ _" prettyInCtx (IsNum x) = prettyInCtx x >>= ppWithPrefix "TCNum" - prettyInCtx (IsRight x) = prettyInCtx x >>= ppWithPrefix "TCInf" + prettyInCtx IsInf = return "TCInf" -- | Recognize a term as a @Left@ or @Right@ asEither :: Recognizer Term (Either Term Term)