From a8194fdd1b0d87bf4a5d516d5efe4da7654eadc3 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Mon, 5 Dec 2022 14:53:36 -0800 Subject: [PATCH 01/27] Updated MR solver to work with SpecM instead of CompM --- saw-core/prelude/Prelude.sawcore | 20 ++ src/SAWScript/Builtins.hs | 2 +- src/SAWScript/Prover/MRSolver.hs | 2 +- src/SAWScript/Prover/MRSolver/Monad.hs | 34 +-- src/SAWScript/Prover/MRSolver/Solver.hs | 298 ++++++++++++++---------- src/SAWScript/Prover/MRSolver/Term.hs | 87 +++---- 6 files changed, 263 insertions(+), 180 deletions(-) diff --git a/saw-core/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore index b2b884dea8..c7ffe20c27 100644 --- a/saw-core/prelude/Prelude.sawcore +++ b/saw-core/prelude/Prelude.sawcore @@ -2941,14 +2941,34 @@ primitive forallS : (E:EvType) -> (stack:FunStack) -> (a:sort 0) -> primitive existsS : (E:EvType) -> (stack:FunStack) -> (a:sort 0) -> SpecM E stack a; +-- Assume a proposition holds primitive assumeS : (E:EvType) -> (stack:FunStack) -> (p:Prop) -> SpecM E stack #(); + +-- Assume a Boolean value is true +assumeBoolS : (E:EvType) -> (stack:FunStack) -> Bool -> SpecM E stack #(); +assumeBoolS E stack b = assumeS E stack (EqTrue b); + +-- Assert a proposition holds primitive assertS : (E:EvType) -> (stack:FunStack) -> (p:Prop) -> SpecM E stack #(); +-- Assert a Boolean value is true +assertBoolS : (E:EvType) -> (stack:FunStack) -> Bool -> SpecM E stack #(); +assertBoolS E stack b = assertS E stack (EqTrue b); + +-- 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; +-- The computation that nondeterministically chooses one computation or another. +-- As a specification, represents the disjunction of two specifications. +orS : (E:EvType) -> (stack:FunStack) -> (a : sort 0) -> + SpecM E stack a -> SpecM E stack a -> SpecM E stack a; +orS E stack a m1 m2 = + bindS E stack Bool a (existsS E stack Bool) + (\ (b:Bool) -> ite (SpecM E stack a) b m1 m2); + -- Return the type represented by a LetRecType LRTType : (E:EvType) -> FunStack -> LetRecType -> sort 0; LRTType E stack lrt = diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index 6bd35e14e9..8541b3e91f 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -2138,7 +2138,7 @@ monadifyTypedTerm sc t = ensureMonadicTerm :: SharedContext -> TypedTerm -> TopLevel TypedTerm ensureMonadicTerm sc t | TypedTermOther tp <- ttType t = - io (Prover.isCompFunType sc tp) >>= \case + io (Prover.isSpecFunType sc tp) >>= \case True -> return t False -> monadifyTypedTerm sc t ensureMonadicTerm sc t = monadifyTypedTerm sc t diff --git a/src/SAWScript/Prover/MRSolver.hs b/src/SAWScript/Prover/MRSolver.hs index 32760eb2db..c31cb1deb5 100644 --- a/src/SAWScript/Prover/MRSolver.hs +++ b/src/SAWScript/Prover/MRSolver.hs @@ -13,7 +13,7 @@ module SAWScript.Prover.MRSolver MRFailure(..), showMRFailure, showMRFailureNoCtx, FunAssump(..), FunAssumpRHS(..), MREnv(..), emptyMREnv, mrEnvAddFunAssump, mrEnvSetDebugLevel, - asProjAll, isCompFunType) where + asProjAll, isSpecFunType) where import SAWScript.Prover.MRSolver.Term import SAWScript.Prover.MRSolver.Monad diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs index 44ae0a8765..0b5de27dd5 100644 --- a/src/SAWScript/Prover/MRSolver/Monad.hs +++ b/src/SAWScript/Prover/MRSolver/Monad.hs @@ -72,7 +72,7 @@ data MRFailure | CannotLookupFunDef FunName | RecursiveUnfold FunName | MalformedLetRecTypes Term - | MalformedDefsFun Term + | MalformedDefs Term | MalformedComp Term | NotCompFunType Term | AssertionNotProvable Term @@ -141,7 +141,7 @@ instance PrettyInCtx MRFailure where prettyInCtx (CompsDoNotRefine m1 m2) = ppWithPrefixSep "Could not prove refinement: " m1 "|=" m2 prettyInCtx (ReturnNotError t) = - ppWithPrefix "errorM computation not equal to:" (ReturnM t) + ppWithPrefix "errorS computation not equal to:" (RetS t) prettyInCtx (FunsNotEq nm1 nm2) = vsepM [return "Named functions not equal:", prettyInCtx nm1, prettyInCtx nm2] @@ -151,8 +151,8 @@ instance PrettyInCtx MRFailure where ppWithPrefix "Recursive unfolding of function inside its own body:" nm prettyInCtx (MalformedLetRecTypes t) = ppWithPrefix "Not a ground LetRecTypes list:" t - prettyInCtx (MalformedDefsFun t) = - ppWithPrefix "Cannot handle letRecM recursive definitions term:" t + prettyInCtx (MalformedDefs t) = + ppWithPrefix "Cannot handle multiFixS recursive definitions term:" t prettyInCtx (MalformedComp t) = ppWithPrefix "Could not handle computation:" t prettyInCtx (NotCompFunType tp) = @@ -192,8 +192,8 @@ showMRFailureNoCtx = showMRFailure . mrFailureWithoutCtx data MRVarInfo -- | An existential variable, that might be instantiated = EVarInfo (Maybe Term) - -- | A letrec-bound function, with its body - | FunVarInfo Term + -- | A recursive function bound by @multiFixS@, with its body + | CallVarInfo Term -- | A map from 'MRVar's to their info type MRVarMap = Map MRVar MRVarInfo @@ -522,7 +522,7 @@ doTypeProj _ _ = -- | Get and normalize the type of a 'FunName' funNameType :: FunName -> MRM Term -funNameType (LetRecName var) = liftSC1 scWhnf $ mrVarType var +funNameType (CallSName var) = liftSC1 scWhnf $ mrVarType var funNameType (EVarFunName var) = liftSC1 scWhnf $ mrVarType var funNameType (GlobalName gd projs) = liftSC1 scWhnf (globalDefType gd) >>= \gd_tp -> @@ -536,6 +536,10 @@ mrApplyAll f args = liftSC2 scApplyAllBeta f args mrApply :: Term -> Term -> MRM Term mrApply f arg = mrApplyAll f [arg] +-- | Return the unit type as a 'Type' +mrUnitType :: MRM Type +mrUnitType = Type <$> liftSC0 scUnitType + -- | Build a constructor application in Mr. Monad mrCtorApp :: Ident -> [Term] -> MRM Term mrCtorApp = liftSC2 scCtorApp @@ -575,16 +579,16 @@ mrTypeOf t = mrConvertible :: Term -> Term -> MRM Bool mrConvertible = liftSC4 scConvertibleEval scTypeCheckWHNF True --- | Take a 'FunName' @f@ for a monadic function of type @vars -> CompM a@ and --- compute the type @CompM [args/vars]a@ of @f@ applied to @args@. Return the --- type @[args/vars]a@ that @CompM@ is applied to. +-- | Take a 'FunName' @f@ for a monadic function of type @vars -> SpecM a@ and +-- compute the type @SpecM [args/vars]a@ of @f@ applied to @args@. Return the +-- type @[args/vars]a@ that @SpecM@ is applied to. mrFunOutType :: FunName -> [Term] -> MRM Term mrFunOutType fname args = mrApplyAll (funNameTerm fname) args >>= mrTypeOf >>= \case - (asCompM -> Just tp) -> liftSC1 scWhnf tp + (asSpecM -> Just tp) -> liftSC1 scWhnf tp _ -> do pp_ftype <- funNameType fname >>= mrPPInCtx pp_fname <- mrPPInCtx fname - debugPrint 0 "mrFunOutType: function does not have CompM return type" + debugPrint 0 "mrFunOutType: function does not have SpecM return type" debugPretty 0 ("Function:" <> pp_fname <> " with type: " <> pp_ftype) error "mrFunOutType" @@ -726,7 +730,7 @@ mrVarInfo var = Map.lookup var <$> mrVars extCnsToFunName :: ExtCns Term -> MRM FunName extCnsToFunName ec = let var = MRVar ec in mrVarInfo var >>= \case Just (EVarInfo _) -> return $ EVarFunName var - Just (FunVarInfo _) -> return $ LetRecName var + Just (CallVarInfo _) -> return $ CallSName var Nothing | Just glob <- asTypedGlobalDef (Unshared $ FTermF $ ExtCns ec) -> return $ GlobalName glob [] @@ -746,9 +750,9 @@ mrGlobalDefBody ident = asConstant <$> liftSC1 scGlobalDef ident >>= \case -- | Get the body of a function @f@ if it has one mrFunNameBody :: FunName -> MRM (Maybe Term) -mrFunNameBody (LetRecName var) = +mrFunNameBody (CallSName var) = mrVarInfo var >>= \case - Just (FunVarInfo body) -> return $ Just body + Just (CallVarInfo body) -> return $ Just body _ -> error "mrFunBody: unknown letrec var" mrFunNameBody (GlobalName glob projs) | Just body <- globalDefBody glob diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs index 3ed6866d1c..6eca23b0d9 100644 --- a/src/SAWScript/Prover/MRSolver/Solver.hs +++ b/src/SAWScript/Prover/MRSolver/Solver.hs @@ -66,10 +66,10 @@ C,b=false |- m1'' |= m2, skipping either case where C,b=X is unsatisfiable; C |- m1 |= if b then m2' else m2'': similar to the above -C |- either T U (CompM V) f1 f2 e |= m: prove C,x:T,e=inl x |- f1 x |= m and +C |- either T U (SpecM V) f1 f2 e |= m: prove C,x:T,e=inl x |- f1 x |= m and C,y:U,e=inl y |- f2 y |= m, again skippping any case with unsatisfiable context; -C |- m |= either T U (CompM V) f1 f2 e: similar to previous +C |- m |= either T U (SpecM V) f1 f2 e: similar to previous C |- m |= forallM f: make a new universal variable x and recurse @@ -125,6 +125,7 @@ module SAWScript.Prover.MRSolver.Solver where import Data.Maybe import Data.Either +import Numeric.Natural (Natural) import Data.List (find, findIndices) import Data.Foldable (foldlM) import Data.Bits (shiftL) @@ -166,34 +167,82 @@ asNestedPairs (asPairValue -> Just (x, asNestedPairs -> Just xs)) = Just (x:xs) asNestedPairs (asFTermF -> Just UnitValue) = Just [] asNestedPairs _ = 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] -mrFreshLetRecVars lrts defs_f = +-- | Recognize a term of the form @Cons1 _ x1 (Cons1 _ x2 (... (Nil1 _)))@ +asList1 :: Recognizer Term [Term] +asList1 (asCtor -> Just (nm, [_])) + | primName nm == "Prelude.Nil1" = return [] +asList1 (asCtor -> Just (nm, [_, hd, tl])) + | primName nm == "Prelude.Cons1" = (hd:) <$> asList1 tl +asList1 _ = Nothing + +-- | Recognize a term of the form @mkFrameCall frame n arg1 ... argn@ +asMkFrameCall :: Recognizer Term (Term, Natural, [Term]) +asMkFrameCall (asApplyAll -> ((isGlobalDef "Prelude.mkFrameCall" -> Just ()), + (frame : (asNat -> Just n) : args))) = + Just (frame, n, args) +asMkFrameCall _ = Nothing + +-- | Recognize a term of the form @CallS _ _ _ (mkFrameCall frame n args)@ +asCallS :: Recognizer Term (Term, Natural, [Term]) +asCallS (asApplyAll -> + ((isGlobalDef "Prelude.callS" -> Just ()), + [_, _, _, + (asMkFrameCall -> Just (frame, n, args))])) = + Just (frame, n, args) +asCallS _ = Nothing + +-- | Recursively traverse a 'Term' and replace each term of the form +-- +-- > CallS _ _ _ (mkFrameCall _ i arg1 ... argn) +-- +-- with the term @tmi arg1 ... argn@, where @tmi@ is the @i@th term in the list +-- +-- FIXME: what we /actually/ want here is to only replace recursive calls as +-- they get normalized; that is, it would be more correct to only recurse inside +-- lambdas, to the left and right of binds, and into the computational subterms +-- of our variable monadic operations (including, e.g., if-then-else and the +-- either and maybe eliminators). But the implementation here should give the +-- correct result for any code we are actually going to see... +mrReplaceCallsWithTerms :: [Term] -> Term -> MRM Term +mrReplaceCallsWithTerms tms = + memoFixTermFun $ \recurse t -> case t of + (asCallS -> Just (_, i, args)) -> + mrApplyAll (tms!!(fromIntegral i)) args + (asApplyAll -> + (isGlobalDef "Prelude.multiFixS" -> Just (), _)) -> + -- Don't recurse inside another multiFixS, since it binds new calls + return t + _ -> traverseSubterms recurse t + + +-- | Bind fresh function variables for a @multiFixS@ with the given list of +-- @LetRecType@s and tuple of definitions for the function bodies +mrFreshCallVars :: Term -> Term -> Term -> Term -> MRM [MRVar] +mrFreshCallVars ev stack (frame@(asList1 -> Just lrts)) defs_tm = do - -- First, make fresh function constants for all the bound functions, using - -- the names bound by defs_f and just "F" if those run out - let fun_var_names = - map fst (fst $ asLambdaList defs_f) ++ repeat "F" - fun_tps <- asLRTList lrts - funs <- zipWithM mrFreshVar fun_var_names fun_tps - fun_tms <- mapM mrVarTerm funs - - -- Next, apply the definition function defs_f to our function vars, yielding - -- the definitions of the individual letrec-bound functions in terms of the - -- new function constants - defs_tm <- mrApplyAll defs_f fun_tms + -- First, make fresh function constants for all the recursive functions + new_stack <- liftSC2 scGlobalApply "Prelude.pushFunStack" [frame, stack] + fun_tps <- forM lrts $ \lrt -> + liftSC2 scGlobalApply "Prelude.LRTType" [ev, new_stack, lrt] + fun_vars <- mapM (mrFreshVar "F") fun_tps + fun_tms <- mapM mrVarTerm fun_vars + + -- Next, match on the tuple of recursive function definitions, and replace + -- all recursive calls in them with our new variable terms defs <- case asNestedPairs defs_tm of - Just defs -> return defs - Nothing -> throwMRFailure (MalformedDefsFun defs_f) + Just defs -> mapM (mrReplaceCallsWithTerms fun_tms) defs + Nothing -> throwMRFailure (MalformedDefs defs_tm) -- Remember the body associated with each fresh function constant zipWithM_ (\f body -> lambdaUVarsM body >>= \cl_body -> - mrSetVarInfo f (FunVarInfo cl_body)) funs defs + mrSetVarInfo f (CallVarInfo cl_body)) fun_vars defs - -- Finally, return the terms for the fresh function variables - return fun_tms + -- Finally, return the fresh function variables + return fun_vars + +mrFreshCallVars _ _ frame _ = + throwMRFailure (MalformedLetRecTypes frame) -- | Normalize a 'Term' of monadic type to monadic normal form @@ -204,7 +253,7 @@ normCompTerm = normComp . CompTerm -- contains have already been normalized with respect to beta and projections -- (but constants need not be unfolded) normComp :: Comp -> MRM NormComp -normComp (CompReturn t) = return $ ReturnM t +normComp (CompReturn t) = return $ RetS t normComp (CompBind m f) = do norm <- normComp m normBind norm f @@ -214,20 +263,20 @@ normComp (CompTerm 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]) -> + (isGlobalDef "Prelude.retS" -> Just (), [_, _, _, x]) -> + return $ RetS x + (isGlobalDef "Prelude.bindS" -> Just (), [_, _, _, _, m, f]) -> do norm <- normCompTerm m normBind norm (CompFunTerm f) - (isGlobalDef "Prelude.errorM" -> Just (), [_, str]) -> - return (ErrorM str) + (isGlobalDef "Prelude.errorS" -> Just (), [_, _, _, str]) -> + return (ErrorS str) (isGlobalDef "Prelude.ite" -> Just (), [_, cond, then_tm, else_tm]) -> return $ Ite cond (CompTerm then_tm) (CompTerm else_tm) (isGlobalDef "Prelude.either" -> Just (), [ltp, rtp, _, f, g, eith]) -> return $ Eithers [(Type ltp, CompFunTerm f), (Type rtp, CompFunTerm g)] eith (isGlobalDef "Prelude.eithers" -> Just (), - [_, matchEitherElims -> Just elims, eith]) -> + [_, (matchEitherElims -> Just elims), eith]) -> return $ Eithers elims eith (isGlobalDef "Prelude.maybe" -> Just (), [tp, _, m, f, mayb]) -> do tp' <- case asApplyAll tp of @@ -238,102 +287,101 @@ normComp (CompTerm t) = mrApplyAll body args _ -> return tp return $ MaybeElim (Type tp') (CompTerm m) (CompFunTerm f) mayb - (isGlobalDef "Prelude.orM" -> Just (), [_, m1, m2]) -> - return $ OrM (CompTerm m1) (CompTerm m2) - (isGlobalDef "Prelude.assertingM" -> Just (), [_, cond, body_tm]) -> - return $ AssertingM cond (CompTerm body_tm) - (isGlobalDef "Prelude.assumingM" -> Just (), [_, cond, body_tm]) -> - return $ AssumingM cond (CompTerm body_tm) - (isGlobalDef "Prelude.existsM" -> Just (), [tp, _, body_tm]) -> - return $ ExistsM (Type tp) (CompFunTerm body_tm) - (isGlobalDef "Prelude.forallM" -> Just (), [tp, _, body_tm]) -> - return $ ForallM (Type tp) (CompFunTerm body_tm) - (isGlobalDef "Prelude.letRecM" -> Just (), [lrts, _, defs_f, body_f]) -> - do - -- Bind fresh function vars for the letrec-bound functions - fun_tms <- mrFreshLetRecVars lrts defs_f - -- Apply the body function to our function vars and recursively - -- normalize the resulting computation - body_tm <- mrApplyAll body_f fun_tms - normCompTerm body_tm - - -- Recognize (multiFixM lrts (\ f1 ... fn -> (body1, ..., bodyn))).i args - (asTupleSelector -> - Just (asApplyAll -> (isGlobalDef "Prelude.multiFixM" -> Just (), - [lrts, defs_f]), - i), args) -> + (isGlobalDef "Prelude.orS" -> Just (), [_, _, _, m1, m2]) -> + return $ OrS (CompTerm m1) (CompTerm m2) + (isGlobalDef "Prelude.assertBoolS" -> Just (), [_, _, cond]) -> + do unit_tp <- mrUnitType + return $ AssertBoolBind cond (CompFunReturn unit_tp) + (isGlobalDef "Prelude.assumeBoolS" -> Just (), [_, _, cond]) -> + do unit_tp <- mrUnitType + return $ AssumeBoolBind cond (CompFunReturn unit_tp) + (isGlobalDef "Prelude.existsS" -> Just (), [_, _, tp]) -> + do unit_tp <- mrUnitType + return $ ExistsBind (Type tp) (CompFunReturn unit_tp) + (isGlobalDef "Prelude.forallS" -> Just (), [_, _, tp]) -> + do unit_tp <- mrUnitType + return $ ForallBind (Type tp) (CompFunReturn unit_tp) + (isGlobalDef "Prelude.multiFixS" -> Just (), + [ev, stack, frame, defs, (asMkFrameCall -> Just (_, 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 <- - if i > 0 && i <= length fun_tms then - mrApplyAll (fun_tms !! (i-1)) args - else throwMRFailure (MalformedComp t) - normCompTerm body_tm + -- Bind fresh function vars for the new recursive functions + fun_vars <- mrFreshCallVars ev stack frame defs + -- Return the @i@th variable to args as a normalized computation + let var = CallSName (fun_vars !! (fromIntegral i)) + out_tp <- mrFunOutType var args + return $ FunBind var args (CompFunReturn $ Type out_tp) -- Convert `vecMapM (bvToNat ...)` into `bvVecMapInvarM`, with the -- invariant being the current set of assumptions - (asGlobalDef -> Just "CryptolM.vecMapM", [a, b, asBvToNat -> Just (w, n), + (asGlobalDef -> Just "CryptolM.vecMapM", [a, b, (asBvToNat -> Just (w, n)), f, xs]) -> + error "FIXME HERE NOW: need SpecM version of vecMapM" + {- do invar <- mrAssumptions liftSC2 scGlobalApply "CryptolM.bvVecMapInvarM" [a, b, w, n, f, xs, invar] >>= normCompTerm + -} -- Convert `atM (bvToNat ...) ... (bvToNat ...)` into the unfolding of -- `bvVecAtM` - (asGlobalDef -> Just "CryptolM.atM", [asBvToNat -> Just (w1, n), a, xs, - asBvToNat -> Just (w2, i)]) -> + (asGlobalDef -> Just "CryptolM.atM", [(asBvToNat -> Just (w1, n)), a, xs, + (asBvToNat -> Just (w2, i))]) -> + error "FIXME HERE NOW: need SpecM version of atM" + {- do body <- mrGlobalDefBody "CryptolM.bvVecAtM" ws_are_eq <- mrConvertible w1 w2 if ws_are_eq then mrApplyAll body [w1, n, a, xs, i] >>= normCompTerm - else throwMRFailure (MalformedComp t) + else throwMRFailure (MalformedComp t) -} -- Convert `atM n ... xs (bvToNat ...)` for a constant `n` into the -- unfolding of `bvVecAtM` after converting `n` to a bitvector constant -- and applying `genBVVecFromVec` to `xs` (asGlobalDef -> Just "CryptolM.atM", [n_tm@(asNat -> Just n), a, xs, - asBvToNat -> - Just (w_tm@(asNat -> Just w), - i)]) -> + (asBvToNat -> + Just (w_tm@(asNat -> Just w), + i))]) -> + error "FIXME HERE NOW: need SpecM version of atM" + {- do body <- mrGlobalDefBody "CryptolM.bvVecAtM" if n < 1 `shiftL` fromIntegral w then do n' <- liftSC2 scBvLit w (toInteger n) xs' <- mrGenBVVecFromVec n_tm a xs "normComp (atM)" w_tm n' mrApplyAll body [w_tm, n', a, xs', i] >>= normCompTerm - else throwMRFailure (MalformedComp t) + else throwMRFailure (MalformedComp t) -} -- Convert `updateM (bvToNat ...) ... (bvToNat ...)` into the unfolding of -- `bvVecUpdateM` - (asGlobalDef -> Just "CryptolM.updateM", [asBvToNat -> Just (w1, n), a, xs, - asBvToNat -> Just (w2, i), x]) -> + (asGlobalDef -> Just "CryptolM.updateM", [(asBvToNat -> Just (w1, n)), a, xs, + (asBvToNat -> Just (w2, i)), x]) -> + error "FIXME HERE NOW: need SpecM version of updateM" + {- do body <- mrGlobalDefBody "CryptolM.bvVecUpdateM" ws_are_eq <- mrConvertible w1 w2 if ws_are_eq then mrApplyAll body [w1, n, a, xs, i, x] >>= normCompTerm - else throwMRFailure (MalformedComp t) + else throwMRFailure (MalformedComp t) -} -- Convert `updateM n ... xs (bvToNat ...)` for a constant `n` into the -- unfolding of `bvVecUpdateM` after converting `n` to a bitvector constant -- and applying `genBVVecFromVec` to `xs` - (asGlobalDef -> Just "CryptolM.updateM", [n_tm@(asNat -> Just n), a, xs, - asBvToNat -> - Just (w_tm@(asNat -> Just w), - i), x]) -> + (asGlobalDef -> Just "CryptolM.updateM", + [n_tm@(asNat -> Just n), a, xs, (asBvToNat -> + Just (w_tm@(asNat -> Just w), i)), x]) -> + error "FIXME HERE NOW: need SpecM version of updateM" + {- do body <- mrGlobalDefBody "CryptolM.fromBVVecUpdateM" if n < 1 `shiftL` fromIntegral w then do n' <- liftSC2 scBvLit w (toInteger n) xs' <- mrGenBVVecFromVec n_tm a xs "normComp (updateM)" w_tm n' err_tm <- mrErrorTerm a "normComp (updateM)" mrApplyAll body [w_tm, n', a, xs', i, x, err_tm, n_tm] >>= normCompTerm - else throwMRFailure (MalformedComp t) + else throwMRFailure (MalformedComp t) -} -- Always unfold: sawLet, multiArgFixM, invariantHint, Num_rec (f@(asGlobalDef -> Just ident), args) - | ident `elem` ["Prelude.sawLet", "Prelude.multiArgFixM", - "Prelude.invariantHint", "Cryptol.Num_rec"] + | ident `elem` ["Prelude.sawLet", "Prelude.invariantHint", + "Cryptol.Num_rec"] , Just (_, Just body) <- asConstant f -> mrApplyAll body args >>= normCompTerm @@ -369,20 +417,22 @@ normComp (CompTerm t) = -- | Bind a computation in whnf with a function, and normalize normBind :: NormComp -> CompFun -> MRM NormComp -normBind (ReturnM t) k = applyNormCompFun k t -normBind (ErrorM msg) _ = return (ErrorM msg) +normBind (RetS t) k = applyNormCompFun k t +normBind (ErrorS msg) _ = return (ErrorS msg) normBind (Ite cond comp1 comp2) k = return $ Ite cond (CompBind comp1 k) (CompBind comp2 k) normBind (Eithers elims t) k = return $ Eithers (map (\(tp,f) -> (tp, compFunComp f k)) elims) t normBind (MaybeElim tp m f t) k = return $ MaybeElim tp (CompBind m k) (compFunComp f k) t -normBind (OrM comp1 comp2) k = - return $ OrM (CompBind comp1 k) (CompBind comp2 k) -normBind (AssertingM cond comp) k = return $ AssertingM cond (CompBind comp k) -normBind (AssumingM cond comp) k = return $ AssumingM cond (CompBind comp k) -normBind (ExistsM tp f) k = return $ ExistsM tp (compFunComp f k) -normBind (ForallM tp f) k = return $ ForallM tp (compFunComp f k) +normBind (OrS comp1 comp2) k = + return $ OrS (CompBind comp1 k) (CompBind comp2 k) +normBind (AssertBoolBind cond f) k = + return $ AssertBoolBind cond (compFunComp f k) +normBind (AssumeBoolBind cond f) k = + return $ AssumeBoolBind cond (compFunComp f k) +normBind (ExistsBind tp f) k = return $ ExistsBind tp (compFunComp f k) +normBind (ForallBind tp f) k = return $ ForallBind tp (compFunComp f k) normBind (FunBind f args k1) k2 -- Turn `bvVecMapInvarM ... >>= k` into `bvVecMapInvarBindM ... k` | GlobalName (globalDefString -> "CryptolM.bvVecMapInvarM") [] <- f @@ -430,15 +480,15 @@ compFunToTerm (CompFunComp f g) = f_tp <- mrTypeOf f' g_tp <- mrTypeOf g' case (f_tp, g_tp) of - (asPi -> Just (_, a, asCompM -> Just b), - asPi -> Just (_, _, asCompM -> Just c)) -> + (asPi -> Just (_, a, asSpecM -> Just b), + asPi -> Just (_, _, asSpecM -> Just c)) -> -- we explicitly unfold @Prelude.composeM@ here so @mrApplyAll@ will -- beta-reduce let nm = maybe "ret_val" id (compFunVarName f) in mrLambdaLift [(nm, a)] (b, c, f', g') $ \[arg] (b', c', f'', g'') -> do app <- mrApplyAll f'' [arg] liftSC2 scGlobalApply "Prelude.bindM" [b', c', app, g''] - _ -> error "compFunToTerm: type(s) not of the form: a -> CompM b" + _ -> error "compFunToTerm: type(s) not of the form: a -> SpecM b" compFunToTerm (CompFunReturn (Type a)) = mrLambdaLift [("ret_val", a)] a $ \[ret_val] (a') -> liftSC2 scGlobalApply "Prelude.returnM" [a', ret_val] @@ -454,9 +504,9 @@ compToTerm (CompBind m f) = do m' <- compToTerm m f' <- compFunToTerm f mrTypeOf f' >>= \case - (asPi -> Just (_, a, asCompM -> Just b)) -> + (asPi -> Just (_, a, asSpecM -> Just b)) -> liftSC2 scGlobalApply "Prelude.bindM" [a, b, m', f'] - _ -> error "compToTerm: type not of the form: a -> CompM b" + _ -> error "compToTerm: type not of the form: a -> SpecM b" -- | Apply a 'CompFun' to a term and normalize the resulting computation applyNormCompFun :: CompFun -> Term -> MRM NormComp @@ -702,10 +752,10 @@ mrRefines t1 t2 = -- | The main implementation of 'mrRefines' mrRefines' :: NormComp -> NormComp -> MRM () -mrRefines' (ReturnM e1) (ReturnM e2) = mrAssertProveRel True e1 e2 -mrRefines' (ErrorM _) (ErrorM _) = return () -mrRefines' (ReturnM e) (ErrorM _) = throwMRFailure (ReturnNotError e) -mrRefines' (ErrorM _) (ReturnM e) = throwMRFailure (ReturnNotError e) +mrRefines' (RetS e1) (RetS e2) = mrAssertProveRel True e1 e2 +mrRefines' (ErrorS _) (ErrorS _) = return () +mrRefines' (RetS e) (ErrorS _) = throwMRFailure (ReturnNotError e) +mrRefines' (ErrorS _) (RetS e) = throwMRFailure (ReturnNotError e) -- maybe elimination on equality types mrRefines' (MaybeElim (Type (asEq -> Just (tp,e1,e2))) m1 f1 _) m2 = @@ -829,25 +879,27 @@ mrRefines' m1 (Eithers ((tp,f2):elims) t2) = (\x (elims', t2'', m1') -> withDataTypeAssump t2'' (IsRight x) (mrRefines m1' (Eithers elims' x))) -mrRefines' m1 (AssumingM cond2 m2) = - withAssumption cond2 $ mrRefines m1 m2 -mrRefines' (AssertingM cond1 m1) m2 = - withAssumption cond1 $ mrRefines m1 m2 +mrRefines' m1 (AssumeBoolBind cond2 k2) = + do m2 <- liftSC0 scUnitValue >>= applyCompFun k2 + withAssumption cond2 $ mrRefines m1 m2 +mrRefines' (AssertBoolBind cond1 k1) m2 = + do m1 <- liftSC0 scUnitValue >>= applyCompFun k1 + withAssumption cond1 $ mrRefines m1 m2 -mrRefines' m1 (ForallM tp f2) = +mrRefines' m1 (ForallBind tp f2) = let nm = maybe "x" id (compFunVarName f2) in withUVarLift nm tp (m1,f2) $ \x (m1',f2') -> applyNormCompFun f2' x >>= \m2' -> mrRefines m1' m2' -mrRefines' (ExistsM tp f1) m2 = +mrRefines' (ExistsBind tp f1) m2 = let nm = maybe "x" id (compFunVarName f1) in withUVarLift nm tp (f1,m2) $ \x (f1',m2') -> applyNormCompFun f1' x >>= \m1' -> mrRefines m1' m2' -mrRefines' m1 (OrM m2 m2') = +mrRefines' m1 (OrS m2 m2') = mrOr (mrRefines m1 m2) (mrRefines m1 m2') -mrRefines' (OrM m1 m1') m2 = +mrRefines' (OrS m1 m1') m2 = mrRefines m1 m2 >> mrRefines m1' m2 -- FIXME: the following cases don't work unless we either allow evars to be set @@ -865,10 +917,10 @@ mrRefines' (FunBind (EVarFunName evar) args (CompFunReturn _)) m2 = Nothing -> mrTrySetAppliedEVar evar args m2 -} -mrRefines' (FunBind (LetRecName f) args1 k1) (FunBind (LetRecName f') args2 k2) +mrRefines' (FunBind (CallSName f) args1 k1) (FunBind (CallSName f') args2 k2) | f == f' && length args1 == length args2 = zipWithM_ mrAssertProveEq args1 args2 >> - mrFunOutType (LetRecName f) args1 >>= \tp -> + mrFunOutType (CallSName f) args1 >>= \tp -> mrRefinesFun tp k1 tp k2 mrRefines' m1@(FunBind f1 args1 k1) m2@(FunBind f2 args2 k2) = @@ -1015,21 +1067,23 @@ mrRefines' m1 m2 = mrRefines'' m1 m2 -- so that they can quantify over as many universals as possible mrRefines'' :: NormComp -> NormComp -> MRM () -mrRefines'' m1 (AssertingM cond2 m2) = - mrProvable cond2 >>= \cond2_pv -> - if cond2_pv then mrRefines m1 m2 - else throwMRFailure (AssertionNotProvable cond2) -mrRefines'' (AssumingM cond1 m1) m2 = - mrProvable cond1 >>= \cond1_pv -> - if cond1_pv then mrRefines m1 m2 - else throwMRFailure (AssumptionNotProvable cond1) - -mrRefines'' m1 (ExistsM tp f2) = +mrRefines'' m1 (AssertBoolBind cond2 k2) = + do m2 <- liftSC0 scUnitValue >>= applyCompFun k2 + cond2_pv <- mrProvable cond2 + if cond2_pv then mrRefines m1 m2 + else throwMRFailure (AssertionNotProvable cond2) +mrRefines'' (AssumeBoolBind cond1 k1) m2 = + do m1 <- liftSC0 scUnitValue >>= applyCompFun k1 + cond1_pv <- mrProvable cond1 + if cond1_pv then mrRefines m1 m2 + else throwMRFailure (AssumptionNotProvable cond1) + +mrRefines'' m1 (ExistsBind tp f2) = do let nm = maybe "x" id (compFunVarName f2) evar <- mrFreshEVar nm tp m2' <- applyNormCompFun f2 evar mrRefines m1 m2' -mrRefines'' (ForallM tp f1) m2 = +mrRefines'' (ForallBind tp f1) m2 = do let nm = maybe "x" id (compFunVarName f1) evar <- mrFreshEVar nm tp m1' <- applyNormCompFun f1 evar @@ -1129,10 +1183,10 @@ mrRefinesFunH _ _ (asPi -> Nothing) _ (asPi -> Just (_,tp2,_)) _ = liftSC0 scUnitType >>= \utp -> throwMRFailure (TypesNotEq (Type utp) (Type tp2)) --- Error if either side's return type is not CompM -mrRefinesFunH _ _ tp1@(asCompM -> Nothing) _ _ _ = +-- Error if either side's return type is not SpecM +mrRefinesFunH _ _ tp1@(asSpecM -> Nothing) _ _ _ = throwMRFailure (NotCompFunType tp1) -mrRefinesFunH _ _ _ _ tp2@(asCompM -> Nothing) _ = +mrRefinesFunH _ _ _ _ tp2@(asSpecM -> Nothing) _ = throwMRFailure (NotCompFunType tp2) mrRefinesFunH k _ _ t1 _ t2 = k t1 t2 diff --git a/src/SAWScript/Prover/MRSolver/Term.hs b/src/SAWScript/Prover/MRSolver/Term.hs index adea7de1bf..37f1de611a 100644 --- a/src/SAWScript/Prover/MRSolver/Term.hs +++ b/src/SAWScript/Prover/MRSolver/Term.hs @@ -81,10 +81,10 @@ asProjAll (asPairSelector -> Just ((asProjAll -> (t, projs)), isRight)) asProjAll t = (t, []) -- | Names of functions to be used in computations, which are either names bound --- by letrec to for recursive calls to fixed-points, existential variables, or +-- by @multiFixS@ for recursive calls to fixed-points, existential variables, or -- (possibly projections of) of global named constants data FunName - = LetRecName MRVar | EVarFunName MRVar | GlobalName GlobalDef [TermProj] + = CallSName MRVar | EVarFunName MRVar | GlobalName GlobalDef [TermProj] deriving (Eq, Ord, Show) -- | Recognize a 'Term' as (possibly a projection of) a global name @@ -101,7 +101,7 @@ asGlobalFunName _ = Nothing -- | Convert a 'FunName' to an unshared term, for printing funNameTerm :: FunName -> Term -funNameTerm (LetRecName var) = Unshared $ FTermF $ ExtCns $ unMRVar var +funNameTerm (CallSName var) = Unshared $ FTermF $ ExtCns $ unMRVar var funNameTerm (EVarFunName var) = Unshared $ FTermF $ ExtCns $ unMRVar var funNameTerm (GlobalName gdef []) = globalDefTerm gdef funNameTerm (GlobalName gdef (TermProjLeft:projs)) = @@ -170,27 +170,27 @@ mrVarCtxOuterToInner = reverse . mrVarCtxInnerToOuter mrVarCtxFromOuterToInner :: [(LocalName,Term)] -> MRVarCtx mrVarCtxFromOuterToInner = mrVarCtxFromInnerToOuter . reverse --- | A Haskell representation of a @CompM@ in "monadic normal form" +-- | A Haskell representation of a @SpecM@ in "monadic normal form" data NormComp - = ReturnM Term -- ^ A term @returnM a x@ - | ErrorM Term -- ^ A term @errorM a str@ + = RetS Term -- ^ A term @retS _ _ a x@ + | ErrorS Term -- ^ A term @errorS _ _ a str@ | Ite Term Comp Comp -- ^ If-then-else computation | Eithers [EitherElim] Term -- ^ A multi-way sum elimination | MaybeElim Type Comp CompFun Term -- ^ A maybe elimination - | OrM Comp Comp -- ^ an @orM@ computation - | AssertingM Term Comp -- ^ an @assertingM@ computation - | AssumingM Term Comp -- ^ an @assumingM@ computation - | ExistsM Type CompFun -- ^ an @existsM@ computation - | ForallM Type CompFun -- ^ a @forallM@ computation + | OrS Comp Comp -- ^ an @orS@ computation + | AssertBoolBind Term CompFun -- ^ the bind of an @assertBoolS@ computation + | AssumeBoolBind Term CompFun -- ^ the bind of an @assumeBoolS@ computation + | ExistsBind Type CompFun -- ^ the bind of an @existsS@ computation + | ForallBind Type CompFun -- ^ the bind of a @forallS@ computation | FunBind FunName [Term] CompFun - -- ^ Bind a monadic function with @N@ arguments in an @a -> CompM b@ term + -- ^ Bind a monadic function with @N@ arguments in an @a -> SpecM b@ term deriving (Generic, Show) -- | An eliminator for an @Eithers@ type is a pair of the type of the disjunct -- and a function from that type to the output type type EitherElim = (Type,CompFun) --- | A computation function of type @a -> CompM b@ for some @a@ and @b@ +-- | A computation function of type @a -> SpecM b@ for some @a@ and @b@ data CompFun -- | An arbitrary term = CompFunTerm Term @@ -221,20 +221,20 @@ compFunInputType (CompFunComp f _) = compFunInputType f compFunInputType (CompFunReturn t) = Just t compFunInputType _ = Nothing --- | A computation of type @CompM a@ for some @a@ +-- | A computation of type @SpecM a@ for some @a@ data Comp = CompTerm Term | CompBind Comp CompFun | CompReturn Term deriving (Generic, Show) --- | Match a type as being of the form @CompM a@ for some @a@ -asCompM :: Term -> Maybe Term -asCompM (asApp -> Just (isGlobalDef "Prelude.CompM" -> Just (), tp)) = +-- | Match a type as being of the form @SpecM E stack a@ for some @a@ +asSpecM :: Term -> Maybe Term +asSpecM (asApplyAll -> (isGlobalDef "Prelude.SpecM" -> Just (), [_, _, tp])) = return tp -asCompM _ = fail "not a CompM type!" +asSpecM _ = fail "not a SpecM type!" -- | Test if a type normalizes to a monadic function type of 0 or more arguments -isCompFunType :: SharedContext -> Term -> IO Bool -isCompFunType sc t = scWhnf sc t >>= \case - (asPiList -> (_, asCompM -> Just _)) -> return True +isSpecFunType :: SharedContext -> Term -> IO Bool +isSpecFunType sc t = scWhnf sc t >>= \case + (asPiList -> (_, asSpecM -> Just _)) -> return True _ -> return False @@ -550,7 +550,7 @@ instance PrettyInCtx TermProj where prettyInCtx (TermProjRecord fld) = return (pretty '.' <> pretty fld) instance PrettyInCtx FunName where - prettyInCtx (LetRecName var) = prettyInCtx var + prettyInCtx (CallSName var) = prettyInCtx var prettyInCtx (EVarFunName var) = prettyInCtx var prettyInCtx (GlobalName g projs) = foldM (\pp proj -> (pp <>) <$> prettyInCtx proj) (ppName $ @@ -566,15 +566,18 @@ instance PrettyInCtx Comp where instance PrettyInCtx CompFun where prettyInCtx (CompFunTerm t) = prettyInCtx t prettyInCtx (CompFunReturn t) = - prettyAppList [return "returnM", parens <$> prettyInCtx t] + prettyAppList [return "retS", return "_", return "_", + parens <$> prettyInCtx t] prettyInCtx (CompFunComp f g) = prettyAppList [prettyInCtx f, return ">=>", prettyInCtx g] instance PrettyInCtx NormComp where - prettyInCtx (ReturnM t) = - prettyAppList [return "returnM", return "_", parens <$> prettyInCtx t] - prettyInCtx (ErrorM str) = - prettyAppList [return "errorM", return "_", parens <$> prettyInCtx str] + prettyInCtx (RetS t) = + prettyAppList [return "retS", return "_", return "_", return "_", + parens <$> prettyInCtx t] + prettyInCtx (ErrorS str) = + prettyAppList [return "errorS", return "_", return "_", return "_", + parens <$> prettyInCtx str] prettyInCtx (Ite cond t1 t2) = prettyAppList [return "ite", return "_", parens <$> prettyInCtx cond, parens <$> prettyInCtx t1, parens <$> prettyInCtx t2] @@ -585,21 +588,23 @@ instance PrettyInCtx NormComp where prettyAppList [return "maybe", parens <$> prettyInCtx tp, return (parens "CompM _"), parens <$> prettyInCtx m, parens <$> prettyInCtx f, parens <$> prettyInCtx mayb] - prettyInCtx (OrM t1 t2) = - prettyAppList [return "orM", return "_", + prettyInCtx (OrS t1 t2) = + prettyAppList [return "orS", return "_", return "_", return "_", parens <$> prettyInCtx t1, parens <$> prettyInCtx t2] - prettyInCtx (AssertingM cond t) = - prettyAppList [return "assertingM", parens <$> prettyInCtx cond, - parens <$> prettyInCtx t] - prettyInCtx (AssumingM cond t) = - prettyAppList [return "assumingM", parens <$> prettyInCtx cond, - parens <$> prettyInCtx t] - prettyInCtx (ExistsM tp f) = - prettyAppList [return "existsM", prettyInCtx tp, return "_", - parens <$> prettyInCtx f] - prettyInCtx (ForallM tp f) = - prettyAppList [return "forallM", prettyInCtx tp, return "_", - parens <$> prettyInCtx f] + prettyInCtx (AssertBoolBind cond k) = + prettyAppList [return "assertBoolS", return "_", return "_", + parens <$> prettyInCtx cond, return ">>=", + parens <$> prettyInCtx k] + prettyInCtx (AssumeBoolBind cond k) = + prettyAppList [return "assumeBoolS", return "_", return "_", + parens <$> prettyInCtx cond, return ">>=", + parens <$> prettyInCtx k] + prettyInCtx (ExistsBind tp k) = + prettyAppList [return "existsS", return "_", return "_", prettyInCtx tp, + return ">>=", parens <$> prettyInCtx k] + prettyInCtx (ForallBind tp k) = + prettyAppList [return "forallS", return "_", return "_", prettyInCtx tp, + return ">>=", parens <$> prettyInCtx k] prettyInCtx (FunBind f args (CompFunReturn _)) = prettyTermApp (funNameTerm f) args prettyInCtx (FunBind f [] k) = From 11bc8672c1208a0ae384dff56dfba4ef4d59bbd6 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Mon, 5 Dec 2022 18:03:44 -0800 Subject: [PATCH 02/27] got some of the MR solver unit tests working --- examples/mr_solver/mr_solver_unit_tests.saw | 45 +++++++++++++-------- saw-core/prelude/Prelude.sawcore | 28 +++++++++++++ 2 files changed, 56 insertions(+), 17 deletions(-) diff --git a/examples/mr_solver/mr_solver_unit_tests.saw b/examples/mr_solver/mr_solver_unit_tests.saw index 704ca9807c..75f8aa8521 100644 --- a/examples/mr_solver/mr_solver_unit_tests.saw +++ b/examples/mr_solver/mr_solver_unit_tests.saw @@ -15,14 +15,17 @@ let run_test name test expected = do { print "Test failed\n"; exit 1; }; }; // The constant 0 function const0 x = 0 -const0 <- parse_core "\\ (_:Vec 64 Bool) -> returnM (Vec 64 Bool) (bvNat 64 0)"; +const0 <- parse_core + "\\ (_:Vec 64 Bool) -> retS VoidEv emptyFunStack (Vec 64 Bool) (bvNat 64 0)"; // The constant 1 function const1 x = 1 -const1 <- parse_core "\\ (_:Vec 64 Bool) -> returnM (Vec 64 Bool) (bvNat 64 1)"; +const1 <- parse_core + "\\ (_:Vec 64 Bool) -> retS VoidEv emptyFunStack (Vec 64 Bool) (bvNat 64 1)"; // const0 <= const0 run_test "const0 |= const0" (mr_solver_query const0 const0) true; +/* // The function test_fun0 from the prelude = const0 test_fun0 <- parse_core "test_fun0"; run_test "const0 |= test_fun0" (mr_solver_query const0 test_fun0) true; @@ -34,12 +37,14 @@ run_test "const0 |= const1" (mr_solver_query const0 const1) false; test_fun1 <- parse_core "test_fun1"; run_test "const1 |= test_fun1" (mr_solver_query const1 test_fun1) true; run_test "const0 |= test_fun1" (mr_solver_query const0 test_fun1) false; +*/ // ifxEq0 x = If x == 0 then x else 0; should be equal to 0 ifxEq0 <- parse_core "\\ (x:Vec 64 Bool) -> \ - \ ite (CompM (Vec 64 Bool)) (bvEq 64 x (bvNat 64 0)) \ - \ (returnM (Vec 64 Bool) x) \ - \ (returnM (Vec 64 Bool) (bvNat 64 0))"; + \ ite (SpecM VoidEv emptyFunStack (Vec 64 Bool)) \ + \ (bvEq 64 x (bvNat 64 0)) \ + \ (retS VoidEv emptyFunStack (Vec 64 Bool) x) \ + \ (retS VoidEv emptyFunStack (Vec 64 Bool) (bvNat 64 0))"; // ifxEq0 <= const0 run_test "ifxEq0 |= const0" (mr_solver_query ifxEq0 const0) true; @@ -47,10 +52,9 @@ run_test "ifxEq0 |= const0" (mr_solver_query ifxEq0 const0) true; // not ifxEq0 <= const1 run_test "ifxEq0 |= const1" (mr_solver_query ifxEq0 const1) false; -// noErrors1 x = exists x. returnM x -noErrors1 <- parse_core "\\ (x:Vec 64 Bool) -> \ - \ existsM (Vec 64 Bool) (Vec 64 Bool) \ - \ (\\ (x:Vec 64 Bool) -> returnM (Vec 64 Bool) x)"; +// noErrors1 x = existsS x. retS x +noErrors1 <- parse_core + "\\ (_:Vec 64 Bool) -> existsS VoidEv emptyFunStack (Vec 64 Bool)"; // const0 <= noErrors run_test "noErrors1 |= noErrors1" (mr_solver_query noErrors1 noErrors1) true; @@ -58,20 +62,27 @@ run_test "noErrors1 |= noErrors1" (mr_solver_query noErrors1 noErrors1) true; // const1 <= noErrors run_test "const1 |= noErrors1" (mr_solver_query const1 noErrors1) true; -// noErrorsRec1 x = orM (existsM x. returnM x) (noErrorsRec1 x) +// noErrorsRec1 _ = orS (existsM x. returnM x) (noErrorsRec1 x) // Intuitively, this specifies functions that either return a value or loop noErrorsRec1 <- parse_core - "fixM (Vec 64 Bool) (\\ (_:Vec 64 Bool) -> Vec 64 Bool) \ - \ (\\ (f: Vec 64 Bool -> CompM (Vec 64 Bool)) (x:Vec 64 Bool) -> \ - \ orM (Vec 64 Bool) \ - \ (existsM (Vec 64 Bool) (Vec 64 Bool) \ - \ (\\ (x:Vec 64 Bool) -> returnM (Vec 64 Bool) x)) \ + "fixS VoidEv emptyFunStack (Vec 64 Bool) (\\ (_:Vec 64 Bool) -> Vec 64 Bool) \ + \ (\\ (f: fixSFun VoidEv emptyFunStack \ + \ (Vec 64 Bool) (\\ (_:Vec 64 Bool) -> Vec 64 Bool)) \ + \ (x:Vec 64 Bool) -> \ + \ orS VoidEv (singletonStack (Vec 64 Bool) \ + \ (\\ (_:Vec 64 Bool) -> Vec 64 Bool)) \ + \ (Vec 64 Bool) \ + \ (existsS VoidEv (singletonStack (Vec 64 Bool) \ + \ (\\ (_:Vec 64 Bool) -> Vec 64 Bool)) \ + \ (Vec 64 Bool)) \ \ (f x))"; // loop x = loop x loop1 <- parse_core - "fixM (Vec 64 Bool) (\\ (_:Vec 64 Bool) -> Vec 64 Bool) \ - \ (\\ (f: Vec 64 Bool -> CompM (Vec 64 Bool)) (x:Vec 64 Bool) -> f x)"; + "fixS VoidEv emptyFunStack (Vec 64 Bool) (\\ (_:Vec 64 Bool) -> Vec 64 Bool) \ + \ (\\ (f: fixSFun VoidEv emptyFunStack \ + \ (Vec 64 Bool) (\\ (_:Vec 64 Bool) -> Vec 64 Bool)) \ + \ (x:Vec 64 Bool) -> f x)"; // loop1 <= noErrorsRec1 run_test "loop1 |= noErrorsRec1" (mr_solver_query loop1 noErrorsRec1) true; diff --git a/saw-core/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore index c7ffe20c27..0366f265da 100644 --- a/saw-core/prelude/Prelude.sawcore +++ b/saw-core/prelude/Prelude.sawcore @@ -3004,6 +3004,34 @@ primitive multiFixS : (call : FrameCall frame) -> SpecM E stack (FrameCallRet frame call); +-- Build a frame with a single function of a single input type +singletonFrame : (a:sort 0) -> (b:a -> sort 0) -> List1 LetRecType; +singletonFrame a b = + Cons1 LetRecType (LRT_Fun a (\ (x:a) -> LRT_Ret (b x))) (Nil1 LetRecType); + +-- Build a stack with a single singleton frame +singletonStack : (a:sort 0) -> (b:a -> sort 0) -> FunStack; +singletonStack a b = pushFunStack (singletonFrame a b) emptyFunStack; + +-- Helper type for fixS +fixSFun : (E:EvType) -> (stack:FunStack) -> + (a:sort 0) -> (b:a -> sort 0) -> sort 0; +fixSFun E stack a b = + (x:a) -> SpecM E (pushFunStack (singletonFrame a b) stack) (b x); + +-- Bind a single recursive function with a single input and pass it the given +-- input argument +fixS : (E:EvType) -> (stack:FunStack) -> (a:sort 0) -> (b:a -> sort 0) -> + (fixSFun E stack a b -> fixSFun E stack a b) -> + (x:a) -> SpecM E stack (b x); +fixS E stack a b body_f x_top = + multiFixS + E stack (singletonFrame a b) + (body_f (\ (x:a) -> + callS E stack (singletonFrame a b) + (mkFrameCall (singletonFrame a b) 0 x)), ()) + (mkFrameCall (singletonFrame a b) 0 x_top); + -- Apply a pure function to the result of a computation fmapS : (E:EvType) -> (stack:FunStack) -> (a b:sort 0) -> (a -> b) -> SpecM E stack a -> From 3b28cc152f70b98529c7beeb31d034c2e636103f Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Mon, 5 Dec 2022 18:25:01 -0800 Subject: [PATCH 03/27] changed mrFreshCallVars to normalize the frame argument --- src/SAWScript/Prover/MRSolver/Solver.hs | 19 ++++--------------- 1 file changed, 4 insertions(+), 15 deletions(-) diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs index 6eca23b0d9..b9e567f3d7 100644 --- a/src/SAWScript/Prover/MRSolver/Solver.hs +++ b/src/SAWScript/Prover/MRSolver/Solver.hs @@ -149,17 +149,6 @@ import SAWScript.Prover.MRSolver.SMT -- * Normalizing and Matching on Terms ---------------------------------------------------------------------- --- | Pattern-match on a @LetRecTypes@ list in normal form and return a list of --- the types it specifies, each in normal form and with uvars abstracted out -asLRTList :: Term -> MRM [Term] -asLRTList (asCtor -> Just (primName -> "Prelude.LRT_Nil", [])) = - return [] -asLRTList (asCtor -> Just (primName -> "Prelude.LRT_Cons", [lrt, lrts])) = - do tp <- liftSC2 scGlobalApply "Prelude.lrtToType" [lrt] - tp_norm_closed <- liftSC1 scWhnf tp >>= piUVarsM - (tp_norm_closed :) <$> asLRTList lrts -asLRTList t = throwMRFailure (MalformedLetRecTypes t) - -- | Match a right-nested series of pairs. This is similar to 'asTupleValue' -- except that it expects a unit value to always be at the end. asNestedPairs :: Recognizer Term [Term] @@ -218,9 +207,12 @@ mrReplaceCallsWithTerms tms = -- | Bind fresh function variables for a @multiFixS@ with the given list of -- @LetRecType@s and tuple of definitions for the function bodies mrFreshCallVars :: Term -> Term -> Term -> Term -> MRM [MRVar] -mrFreshCallVars ev stack (frame@(asList1 -> Just lrts)) defs_tm = +mrFreshCallVars ev stack frame defs_tm = do -- First, make fresh function constants for all the recursive functions + lrts <- liftSC1 scWhnf frame >>= \case + (asList1 -> Just lrts) -> return lrts + _ -> throwMRFailure (MalformedLetRecTypes frame) new_stack <- liftSC2 scGlobalApply "Prelude.pushFunStack" [frame, stack] fun_tps <- forM lrts $ \lrt -> liftSC2 scGlobalApply "Prelude.LRTType" [ev, new_stack, lrt] @@ -241,9 +233,6 @@ mrFreshCallVars ev stack (frame@(asList1 -> Just lrts)) defs_tm = -- Finally, return the fresh function variables return fun_vars -mrFreshCallVars _ _ frame _ = - throwMRFailure (MalformedLetRecTypes frame) - -- | Normalize a 'Term' of monadic type to monadic normal form normCompTerm :: Term -> MRM NormComp From ffd5b186b1427dccda210d5a860c3c0e1bc1f2f0 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Tue, 6 Dec 2022 13:46:42 -0800 Subject: [PATCH 04/27] fixed a bug in mrFreshCallVars where uvars were not getting properly abstracted out of callS body definitions --- src/SAWScript/Prover/MRSolver/Monad.hs | 19 ++++++++++----- src/SAWScript/Prover/MRSolver/Solver.hs | 32 ++++++++++++++----------- 2 files changed, 31 insertions(+), 20 deletions(-) diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs index 0b5de27dd5..caafa7f800 100644 --- a/src/SAWScript/Prover/MRSolver/Monad.hs +++ b/src/SAWScript/Prover/MRSolver/Monad.hs @@ -195,6 +195,12 @@ data MRVarInfo -- | A recursive function bound by @multiFixS@, with its body | CallVarInfo Term +instance PrettyInCtx MRVarInfo where + prettyInCtx (EVarInfo maybe_t) = + prettyAppList [ return "EVar", parens <$> prettyInCtx maybe_t] + prettyInCtx (CallVarInfo t) = + prettyAppList [ return "CallVar", parens <$> prettyInCtx t] + -- | A map from 'MRVar's to their info type MRVarMap = Map MRVar MRVarInfo @@ -807,12 +813,13 @@ mrFreshVar nm tp = MRVar <$> liftSC2 scFreshEC nm tp -- | Set the info associated with an 'MRVar', assuming it has not been set mrSetVarInfo :: MRVar -> MRVarInfo -> MRM () mrSetVarInfo var info = - modify $ \st -> - st { mrsVars = - Map.alter (\case - Just _ -> error "mrSetVarInfo" - Nothing -> Just info) - var (mrsVars st) } + debugPretty 3 ("mrSetVarInfo" <+> ppInEmptyCtx var <+> "=" <+> ppInEmptyCtx info) >> + (modify $ \st -> + st { mrsVars = + Map.alter (\case + Just _ -> error "mrSetVarInfo" + Nothing -> Just info) + var (mrsVars st) }) -- | Make a fresh existential variable of the given type, abstracting out all -- the current uvars and returning the new evar applied to all current uvars diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs index b9e567f3d7..eda78f0c06 100644 --- a/src/SAWScript/Prover/MRSolver/Solver.hs +++ b/src/SAWScript/Prover/MRSolver/Solver.hs @@ -209,26 +209,28 @@ mrReplaceCallsWithTerms tms = mrFreshCallVars :: Term -> Term -> Term -> Term -> MRM [MRVar] mrFreshCallVars ev stack frame defs_tm = do - -- First, make fresh function constants for all the recursive functions + -- First, make fresh function constants for all the recursive functions, + -- noting that each constant must abstract out the current uvar context + new_stack <- liftSC2 scGlobalApply "Prelude.pushFunStack" [frame, stack] lrts <- liftSC1 scWhnf frame >>= \case (asList1 -> Just lrts) -> return lrts _ -> throwMRFailure (MalformedLetRecTypes frame) - new_stack <- liftSC2 scGlobalApply "Prelude.pushFunStack" [frame, stack] fun_tps <- forM lrts $ \lrt -> - liftSC2 scGlobalApply "Prelude.LRTType" [ev, new_stack, lrt] + piUVarsM =<< liftSC2 scGlobalApply "Prelude.LRTType" [ev, new_stack, lrt] fun_vars <- mapM (mrFreshVar "F") fun_tps - fun_tms <- mapM mrVarTerm fun_vars - -- Next, match on the tuple of recursive function definitions, and replace - -- all recursive calls in them with our new variable terms - defs <- case asNestedPairs defs_tm of - Just defs -> mapM (mrReplaceCallsWithTerms fun_tms) defs + -- Next, match on the tuple of recursive function definitions and convert + -- each definition to a function body, by lambda-abstracting all the current + -- uvars and then replacing all recursive calls in each function body with + -- our new variable terms (which are applied to the current uvars; see + -- mrVarTerm) + fun_tms <- mapM mrVarTerm fun_vars + bodies <- case asNestedPairs defs_tm of + Just defs -> mapM (mrReplaceCallsWithTerms fun_tms >=> lambdaUVarsM) defs Nothing -> throwMRFailure (MalformedDefs defs_tm) -- Remember the body associated with each fresh function constant - zipWithM_ (\f body -> - lambdaUVarsM body >>= \cl_body -> - mrSetVarInfo f (CallVarInfo cl_body)) fun_vars defs + zipWithM_ (\f body -> mrSetVarInfo f (CallVarInfo body)) fun_vars bodies -- Finally, return the fresh function variables return fun_vars @@ -295,10 +297,12 @@ normComp (CompTerm t) = do -- Bind fresh function vars for the new recursive functions fun_vars <- mrFreshCallVars ev stack frame defs - -- Return the @i@th variable to args as a normalized computation + -- Return the @i@th variable to args as a normalized computation, noting + -- that it must be applied to all of the uvars as well as the args let var = CallSName (fun_vars !! (fromIntegral i)) - out_tp <- mrFunOutType var args - return $ FunBind var args (CompFunReturn $ Type out_tp) + all_args <- (++ args) <$> getAllUVarTerms + out_tp <- mrFunOutType var all_args + return $ FunBind var all_args (CompFunReturn $ Type out_tp) -- Convert `vecMapM (bvToNat ...)` into `bvVecMapInvarM`, with the -- invariant being the current set of assumptions From 409888e461984730bc49aa45b0f7cebf87013c06 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Tue, 6 Dec 2022 17:51:24 -0800 Subject: [PATCH 05/27] changed CompFuns to keep around their event types and fun stacks --- src/SAWScript/Prover/MRSolver/Monad.hs | 10 +-- src/SAWScript/Prover/MRSolver/Solver.hs | 87 ++++++++++++++----------- src/SAWScript/Prover/MRSolver/Term.hs | 46 +++++++++---- 3 files changed, 87 insertions(+), 56 deletions(-) diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs index caafa7f800..9281788556 100644 --- a/src/SAWScript/Prover/MRSolver/Monad.hs +++ b/src/SAWScript/Prover/MRSolver/Monad.hs @@ -587,11 +587,11 @@ mrConvertible = liftSC4 scConvertibleEval scTypeCheckWHNF True -- | Take a 'FunName' @f@ for a monadic function of type @vars -> SpecM a@ and -- compute the type @SpecM [args/vars]a@ of @f@ applied to @args@. Return the --- type @[args/vars]a@ that @SpecM@ is applied to. -mrFunOutType :: FunName -> [Term] -> MRM Term +-- type @[args/vars]a@ that @SpecM@ is applied to, along with its parameters. +mrFunOutType :: FunName -> [Term] -> MRM (SpecMParams, Term) mrFunOutType fname args = mrApplyAll (funNameTerm fname) args >>= mrTypeOf >>= \case - (asSpecM -> Just tp) -> liftSC1 scWhnf tp + (asSpecM -> Just (params, tp)) -> (params,) <$> liftSC1 scWhnf tp _ -> do pp_ftype <- funNameType fname >>= mrPPInCtx pp_fname <- mrPPInCtx fname debugPrint 0 "mrFunOutType: function does not have SpecM return type" @@ -997,7 +997,7 @@ mrGetFunAssump nm = Map.lookup nm <$> mrFunAssumps -- are 'Term's that can have the current uvars free withFunAssump :: FunName -> [Term] -> NormComp -> MRM a -> MRM a withFunAssump fname args rhs m = - do k <- CompFunReturn <$> Type <$> mrFunOutType fname args + do k <- mkCompFunReturn <$> mrFunOutType fname args mrDebugPPPrefixSep 1 "withFunAssump" (FunBind fname args k) "|=" rhs ctx <- mrUVars assumps <- mrFunAssumps @@ -1077,7 +1077,7 @@ mrGetDataTypeAssump x = HashMap.lookup x <$> mrDataTypeAssumps -- | Convert a 'FunAssumpRHS' to a 'NormComp' mrFunAssumpRHSAsNormComp :: FunAssumpRHS -> MRM NormComp mrFunAssumpRHSAsNormComp (OpaqueFunAssump f args) = - FunBind f args <$> CompFunReturn <$> Type <$> mrFunOutType f args + FunBind f args <$> mkCompFunReturn <$> mrFunOutType f args mrFunAssumpRHSAsNormComp (RewriteFunAssump rhs) = return rhs diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs index eda78f0c06..5f7a4fa6f0 100644 --- a/src/SAWScript/Prover/MRSolver/Solver.hs +++ b/src/SAWScript/Prover/MRSolver/Solver.hs @@ -256,20 +256,22 @@ normComp (CompTerm t) = mrApplyAll f args >>= normCompTerm (isGlobalDef "Prelude.retS" -> Just (), [_, _, _, x]) -> return $ RetS x - (isGlobalDef "Prelude.bindS" -> Just (), [_, _, _, _, m, f]) -> + (isGlobalDef "Prelude.bindS" -> Just (), [e, stack, _, _, m, f]) -> do norm <- normCompTerm m - normBind norm (CompFunTerm f) + normBind norm (CompFunTerm (SpecMParams e stack) f) (isGlobalDef "Prelude.errorS" -> Just (), [_, _, _, str]) -> return (ErrorS str) (isGlobalDef "Prelude.ite" -> Just (), [_, cond, then_tm, else_tm]) -> return $ Ite cond (CompTerm then_tm) (CompTerm else_tm) - (isGlobalDef "Prelude.either" -> Just (), [ltp, rtp, _, f, g, eith]) -> - return $ Eithers [(Type ltp, CompFunTerm f), - (Type rtp, CompFunTerm g)] eith + (isGlobalDef "Prelude.either" -> Just (), + [ltp, rtp, (asSpecM -> Just (params, _)), f, g, eith]) -> + return $ Eithers [(Type ltp, CompFunTerm params f), + (Type rtp, CompFunTerm params g)] eith (isGlobalDef "Prelude.eithers" -> Just (), [_, (matchEitherElims -> Just elims), eith]) -> return $ Eithers elims eith - (isGlobalDef "Prelude.maybe" -> Just (), [tp, _, m, f, mayb]) -> + (isGlobalDef "Prelude.maybe" -> Just (), + [tp, (asSpecM -> Just (params, _)), m, f, mayb]) -> do tp' <- case asApplyAll tp of -- Always unfold: is_bvult, is_bvule (tpf@(asGlobalDef -> Just ident), args) @@ -277,21 +279,25 @@ normComp (CompTerm t) = , Just (_, Just body) <- asConstant tpf -> mrApplyAll body args _ -> return tp - return $ MaybeElim (Type tp') (CompTerm m) (CompFunTerm f) mayb + return $ MaybeElim (Type tp') (CompTerm m) (CompFunTerm params f) mayb (isGlobalDef "Prelude.orS" -> Just (), [_, _, _, m1, m2]) -> return $ OrS (CompTerm m1) (CompTerm m2) - (isGlobalDef "Prelude.assertBoolS" -> Just (), [_, _, cond]) -> + (isGlobalDef "Prelude.assertBoolS" -> Just (), [ev, stack, cond]) -> do unit_tp <- mrUnitType - return $ AssertBoolBind cond (CompFunReturn unit_tp) - (isGlobalDef "Prelude.assumeBoolS" -> Just (), [_, _, cond]) -> + return $ AssertBoolBind cond (CompFunReturn + (SpecMParams ev stack) unit_tp) + (isGlobalDef "Prelude.assumeBoolS" -> Just (), [ev, stack, cond]) -> do unit_tp <- mrUnitType - return $ AssumeBoolBind cond (CompFunReturn unit_tp) - (isGlobalDef "Prelude.existsS" -> Just (), [_, _, tp]) -> + return $ AssumeBoolBind cond (CompFunReturn + (SpecMParams ev stack) unit_tp) + (isGlobalDef "Prelude.existsS" -> Just (), [ev, stack, tp]) -> do unit_tp <- mrUnitType - return $ ExistsBind (Type tp) (CompFunReturn unit_tp) - (isGlobalDef "Prelude.forallS" -> Just (), [_, _, tp]) -> + return $ ExistsBind (Type tp) (CompFunReturn + (SpecMParams ev stack) unit_tp) + (isGlobalDef "Prelude.forallS" -> Just (), [ev, stack, tp]) -> do unit_tp <- mrUnitType - return $ ForallBind (Type tp) (CompFunReturn unit_tp) + return $ ForallBind (Type tp) (CompFunReturn + (SpecMParams ev stack) unit_tp) (isGlobalDef "Prelude.multiFixS" -> Just (), [ev, stack, frame, defs, (asMkFrameCall -> Just (_, i, args))]) -> do @@ -301,8 +307,7 @@ normComp (CompTerm t) = -- that it must be applied to all of the uvars as well as the args let var = CallSName (fun_vars !! (fromIntegral i)) all_args <- (++ args) <$> getAllUVarTerms - out_tp <- mrFunOutType var all_args - return $ FunBind var all_args (CompFunReturn $ Type out_tp) + FunBind var all_args <$> mkCompFunReturn <$> mrFunOutType var all_args -- Convert `vecMapM (bvToNat ...)` into `bvVecMapInvarM`, with the -- invariant being the current set of assumptions @@ -398,12 +403,11 @@ normComp (CompTerm t) = -- FIXME: substitute for evars if they have been instantiated ((asExtCns -> Just ec), args) -> do fun_name <- extCnsToFunName ec - fun_tp <- Type <$> mrFunOutType fun_name args - return $ FunBind fun_name args (CompFunReturn fun_tp) + FunBind fun_name args <$> mkCompFunReturn <$> + mrFunOutType fun_name args ((asGlobalFunName -> Just f), args) -> - do fun_tp <- Type <$> mrFunOutType f args - return $ FunBind f args (CompFunReturn fun_tp) + FunBind f args <$> mkCompFunReturn <$> mrFunOutType f args _ -> throwMRFailure (MalformedComp t) @@ -428,6 +432,7 @@ normBind (ExistsBind tp f) k = return $ ExistsBind tp (compFunComp f k) normBind (ForallBind tp f) k = return $ ForallBind tp (compFunComp f k) normBind (FunBind f args k1) k2 -- Turn `bvVecMapInvarM ... >>= k` into `bvVecMapInvarBindM ... k` + {- | GlobalName (globalDefString -> "CryptolM.bvVecMapInvarM") [] <- f , (a:b:args_rest) <- args = do f' <- mrGlobalDef "CryptolM.bvVecMapInvarBindM" @@ -442,17 +447,19 @@ normBind (FunBind f args k1) k2 do cont' <- compFunToTerm (compFunComp (compFunComp (CompFunTerm cont) k1) k2) c <- compFunReturnType k2 return $ FunBind f (args_pre ++ [cont']) (CompFunReturn (Type c)) - | otherwise = return $ FunBind f args (compFunComp k1 k2) + | otherwise -} = return $ FunBind f args (compFunComp k1 k2) -- | Bind a 'Term' for a computation with a function and normalize normBindTerm :: Term -> CompFun -> MRM NormComp normBindTerm t f = normCompTerm t >>= \m -> normBind m f +{- -- | Get the return type of a 'CompFun' compFunReturnType :: CompFun -> MRM Term -compFunReturnType (CompFunTerm t) = mrTypeOf t +compFunReturnType (CompFunTerm _ t) = mrTypeOf t compFunReturnType (CompFunComp _ g) = compFunReturnType g compFunReturnType (CompFunReturn (Type t)) = return t +-} -- | Apply a computation function to a term argument to get a computation applyCompFun :: CompFun -> Term -> MRM Comp @@ -460,32 +467,34 @@ applyCompFun (CompFunComp f g) t = -- (f >=> g) t == f t >>= g do comp <- applyCompFun f t return $ CompBind comp g -applyCompFun (CompFunReturn _) t = +applyCompFun (CompFunReturn _ _) t = return $ CompReturn t -applyCompFun (CompFunTerm f) t = CompTerm <$> mrApplyAll f [t] +applyCompFun (CompFunTerm _ f) t = CompTerm <$> mrApplyAll f [t] -- | Convert a 'CompFun' into a 'Term' compFunToTerm :: CompFun -> MRM Term -compFunToTerm (CompFunTerm t) = return t +compFunToTerm (CompFunTerm _ t) = return t compFunToTerm (CompFunComp f g) = do f' <- compFunToTerm f g' <- compFunToTerm g f_tp <- mrTypeOf f' g_tp <- mrTypeOf g' case (f_tp, g_tp) of - (asPi -> Just (_, a, asSpecM -> Just b), - asPi -> Just (_, _, asSpecM -> Just c)) -> + (asPi -> Just (_, a, asSpecM -> Just (params, b)), + asPi -> Just (_, _, asSpecM -> Just (_, c))) -> -- we explicitly unfold @Prelude.composeM@ here so @mrApplyAll@ will -- beta-reduce let nm = maybe "ret_val" id (compFunVarName f) in mrLambdaLift [(nm, a)] (b, c, f', g') $ \[arg] (b', c', f'', g'') -> do app <- mrApplyAll f'' [arg] - liftSC2 scGlobalApply "Prelude.bindM" [b', c', app, g''] + liftSC2 scGlobalApply "Prelude.bindS" (specMParamsArgs params ++ + [b', c', app, g'']) _ -> error "compFunToTerm: type(s) not of the form: a -> SpecM b" -compFunToTerm (CompFunReturn (Type a)) = +compFunToTerm (CompFunReturn params (Type a)) = mrLambdaLift [("ret_val", a)] a $ \[ret_val] (a') -> - liftSC2 scGlobalApply "Prelude.returnM" [a', ret_val] + liftSC2 scGlobalApply "Prelude.retS" (specMParamsArgs params ++ [a', ret_val]) +{- -- | Convert a 'Comp' into a 'Term' compToTerm :: Comp -> MRM Term compToTerm (CompTerm t) = return t @@ -500,6 +509,7 @@ compToTerm (CompBind m f) = (asPi -> Just (_, a, asSpecM -> Just b)) -> liftSC2 scGlobalApply "Prelude.bindM" [a, b, m', f'] _ -> error "compToTerm: type not of the form: a -> SpecM b" +-} -- | Apply a 'CompFun' to a term and normalize the resulting computation applyNormCompFun :: CompFun -> Term -> MRM NormComp @@ -510,8 +520,8 @@ matchEitherElims :: Term -> Maybe [EitherElim] matchEitherElims (asCtor -> Just (primName -> "Prelude.FunsTo_Nil", [_])) = Just [] matchEitherElims (asCtor -> Just (primName -> "Prelude.FunsTo_Cons", - [_, tp, f, rest])) = - ((Type tp, CompFunTerm f):) <$> + [asSpecM -> Just (params, _), tp, f, rest])) = + ((Type tp, CompFunTerm params f):) <$> matchEitherElims rest matchEitherElims _ = Nothing @@ -913,12 +923,12 @@ mrRefines' (FunBind (EVarFunName evar) args (CompFunReturn _)) m2 = mrRefines' (FunBind (CallSName f) args1 k1) (FunBind (CallSName f') args2 k2) | f == f' && length args1 == length args2 = zipWithM_ mrAssertProveEq args1 args2 >> - mrFunOutType (CallSName f) args1 >>= \tp -> + mrFunOutType (CallSName f) args1 >>= \(_, tp) -> mrRefinesFun tp k1 tp k2 mrRefines' m1@(FunBind f1 args1 k1) m2@(FunBind f2 args2 k2) = - mrFunOutType f1 args1 >>= \tp1 -> - mrFunOutType f2 args2 >>= \tp2 -> + mrFunOutType f1 args1 >>= \(_, tp1) -> + mrFunOutType f2 args2 >>= \(_, tp2) -> findInjConvs tp1 Nothing tp2 Nothing >>= \mb_convs -> mrFunBodyRecInfo f1 args1 >>= \maybe_f1_body -> mrFunBodyRecInfo f2 args2 >>= \maybe_f2_body -> @@ -1207,14 +1217,15 @@ askMRSolverH f t1 t2 = case (m1, m2) of -- If t1 and t2 are both named functions, our result is the opaque -- FunAssump that forall xs. f1 xs |= f2 xs' - (FunBind f1 args1 (CompFunReturn _), FunBind f2 args2 (CompFunReturn _)) -> + (FunBind f1 args1 (CompFunReturn _ _), + FunBind f2 args2 (CompFunReturn _ _)) -> mrUVars >>= \uvar_ctx -> return $ Just (f1, FunAssump { fassumpCtx = uvar_ctx, fassumpArgs = args1, fassumpRHS = OpaqueFunAssump f2 args2 }) -- If just t1 is a named function, our result is the rewrite FunAssump -- that forall xs. f1 xs |= m2 - (FunBind f1 args1 (CompFunReturn _), _) -> + (FunBind f1 args1 (CompFunReturn _ _), _) -> mrUVars >>= \uvar_ctx -> return $ Just (f1, FunAssump { fassumpCtx = uvar_ctx, fassumpArgs = args1, diff --git a/src/SAWScript/Prover/MRSolver/Term.hs b/src/SAWScript/Prover/MRSolver/Term.hs index 37f1de611a..9f95889009 100644 --- a/src/SAWScript/Prover/MRSolver/Term.hs +++ b/src/SAWScript/Prover/MRSolver/Term.hs @@ -170,6 +170,15 @@ mrVarCtxOuterToInner = reverse . mrVarCtxInnerToOuter mrVarCtxFromOuterToInner :: [(LocalName,Term)] -> MRVarCtx mrVarCtxFromOuterToInner = mrVarCtxFromInnerToOuter . reverse +-- | A Haskell representation of the two non-type parameters of @SpecM@ +data SpecMParams = SpecMParams { specMEvType :: Term, + specMStack :: Term } + deriving (Generic, Show) + +-- | Convert a 'SpecMParams' to a list of arguments +specMParamsArgs :: SpecMParams -> [Term] +specMParamsArgs (SpecMParams ev stack) = [ev, stack] + -- | A Haskell representation of a @SpecM@ in "monadic normal form" data NormComp = RetS Term -- ^ A term @retS _ _ a x@ @@ -193,42 +202,52 @@ type EitherElim = (Type,CompFun) -- | A computation function of type @a -> SpecM b@ for some @a@ and @b@ data CompFun -- | An arbitrary term - = CompFunTerm Term + = CompFunTerm SpecMParams Term -- | A special case for the term @\ (x:a) -> returnM a x@ - | CompFunReturn Type + | CompFunReturn SpecMParams Type -- | The monadic composition @f >=> g@ | CompFunComp CompFun CompFun deriving (Generic, Show) +-- | Apply 'CompFunReturn' to a pair of a 'SpecMParams' and a 'Term' +mkCompFunReturn :: (SpecMParams, Term) -> CompFun +mkCompFunReturn (params, tp) = CompFunReturn params $ Type tp + -- | Compose two 'CompFun's, simplifying if one is a 'CompFunReturn' compFunComp :: CompFun -> CompFun -> CompFun -compFunComp (CompFunReturn _) f = f -compFunComp f (CompFunReturn _) = f +compFunComp (CompFunReturn _ _) f = f +compFunComp f (CompFunReturn _ _) = f compFunComp f g = CompFunComp f g -- | If a 'CompFun' contains an explicit lambda-abstraction, then return the -- textual name bound by that lambda compFunVarName :: CompFun -> Maybe LocalName -compFunVarName (CompFunTerm t) = asLambdaName t +compFunVarName (CompFunTerm _ t) = asLambdaName t compFunVarName (CompFunComp f _) = compFunVarName f compFunVarName _ = Nothing -- | If a 'CompFun' contains an explicit lambda-abstraction, then return the -- input type for it compFunInputType :: CompFun -> Maybe Type -compFunInputType (CompFunTerm (asLambda -> Just (_, tp, _))) = Just $ Type tp +compFunInputType (CompFunTerm _ (asLambda -> Just (_, tp, _))) = Just $ Type tp compFunInputType (CompFunComp f _) = compFunInputType f -compFunInputType (CompFunReturn t) = Just t +compFunInputType (CompFunReturn _ t) = Just t compFunInputType _ = Nothing +-- | Get the @SpecM@ non-type parameters from a 'CompFun' +compFunSpecMParams :: CompFun -> SpecMParams +compFunSpecMParams (CompFunTerm params _) = params +compFunSpecMParams (CompFunReturn params _) = params +compFunSpecMParams (CompFunComp f _) = compFunSpecMParams f + -- | A computation of type @SpecM a@ for some @a@ data Comp = CompTerm Term | CompBind Comp CompFun | CompReturn Term deriving (Generic, Show) -- | Match a type as being of the form @SpecM E stack a@ for some @a@ -asSpecM :: Term -> Maybe Term -asSpecM (asApplyAll -> (isGlobalDef "Prelude.SpecM" -> Just (), [_, _, tp])) = - return tp +asSpecM :: Term -> Maybe (SpecMParams, Term) +asSpecM (asApplyAll -> (isGlobalDef "Prelude.SpecM" -> Just (), [ev, stack, tp])) = + return (SpecMParams { specMEvType = ev, specMStack = stack }, tp) asSpecM _ = fail "not a SpecM type!" -- | Test if a type normalizes to a monadic function type of 0 or more arguments @@ -455,6 +474,7 @@ instance TermLike Natural where substTermLike _ _ = return deriving anyclass instance TermLike Type +deriving instance TermLike SpecMParams deriving instance TermLike NormComp deriving instance TermLike CompFun deriving instance TermLike Comp @@ -564,8 +584,8 @@ instance PrettyInCtx Comp where prettyAppList [ return "returnM", return "_", parens <$> prettyInCtx t] instance PrettyInCtx CompFun where - prettyInCtx (CompFunTerm t) = prettyInCtx t - prettyInCtx (CompFunReturn t) = + prettyInCtx (CompFunTerm _ t) = prettyInCtx t + prettyInCtx (CompFunReturn _ t) = prettyAppList [return "retS", return "_", return "_", parens <$> prettyInCtx t] prettyInCtx (CompFunComp f g) = @@ -605,7 +625,7 @@ instance PrettyInCtx NormComp where prettyInCtx (ForallBind tp k) = prettyAppList [return "forallS", return "_", return "_", prettyInCtx tp, return ">>=", parens <$> prettyInCtx k] - prettyInCtx (FunBind f args (CompFunReturn _)) = + prettyInCtx (FunBind f args (CompFunReturn _ _)) = prettyTermApp (funNameTerm f) args prettyInCtx (FunBind f [] k) = prettyAppList [prettyInCtx f, return ">>=", prettyInCtx k] From 1804e0f54ed04e3420e769090feff2a225ecac6d Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Wed, 7 Dec 2022 13:09:37 -0800 Subject: [PATCH 06/27] added multiArgFixS --- saw-core/prelude/Prelude.sawcore | 52 ++++++++++++++++++++++---------- 1 file changed, 36 insertions(+), 16 deletions(-) diff --git a/saw-core/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore index 0366f265da..2c6db18106 100644 --- a/saw-core/prelude/Prelude.sawcore +++ b/saw-core/prelude/Prelude.sawcore @@ -2972,11 +2972,7 @@ orS E stack a m1 m2 = -- Return the type represented by a LetRecType LRTType : (E:EvType) -> FunStack -> LetRecType -> sort 0; LRTType E stack lrt = - LetRecType#rec - (\ (lrt:LetRecType) -> sort 0) - (\ (r:sort 0) -> SpecM E stack r) - (\ (a:sort 0) (_:a -> LetRecType) (b:a -> sort 0) -> (x:a) -> b x) - lrt; + lrt1Pi lrt (\ (args:LRTInput lrt) -> SpecM E stack (LRTOutput lrt args)); -- Build the right-nested tuple type (T1 * (T2 * ... (Tn * #()))) where each Ti -- is the result of calling LRTType on the ith LetRecType in a list @@ -3004,20 +3000,23 @@ primitive multiFixS : (call : FrameCall frame) -> SpecM E stack (FrameCallRet frame call); +-- Build a frame with a single function +singletonFrame : LetRecType -> List1 LetRecType; +singletonFrame lrt = Cons1 LetRecType lrt (Nil1 LetRecType); + -- Build a frame with a single function of a single input type -singletonFrame : (a:sort 0) -> (b:a -> sort 0) -> List1 LetRecType; -singletonFrame a b = - Cons1 LetRecType (LRT_Fun a (\ (x:a) -> LRT_Ret (b x))) (Nil1 LetRecType); +fixSFrame : (a:sort 0) -> (b:a -> sort 0) -> List1 LetRecType; +fixSFrame a b = singletonFrame (LRT_Fun a (\ (x:a) -> LRT_Ret (b x))); --- Build a stack with a single singleton frame -singletonStack : (a:sort 0) -> (b:a -> sort 0) -> FunStack; -singletonStack a b = pushFunStack (singletonFrame a b) emptyFunStack; +-- Build a stack with a single fixS frame +fixSStack : (a:sort 0) -> (b:a -> sort 0) -> FunStack; +fixSStack a b = pushFunStack (fixSFrame a b) emptyFunStack; -- Helper type for fixS fixSFun : (E:EvType) -> (stack:FunStack) -> (a:sort 0) -> (b:a -> sort 0) -> sort 0; fixSFun E stack a b = - (x:a) -> SpecM E (pushFunStack (singletonFrame a b) stack) (b x); + (x:a) -> SpecM E (pushFunStack (fixSFrame a b) stack) (b x); -- Bind a single recursive function with a single input and pass it the given -- input argument @@ -3026,11 +3025,32 @@ fixS : (E:EvType) -> (stack:FunStack) -> (a:sort 0) -> (b:a -> sort 0) -> (x:a) -> SpecM E stack (b x); fixS E stack a b body_f x_top = multiFixS - E stack (singletonFrame a b) + E stack (fixSFrame a b) (body_f (\ (x:a) -> - callS E stack (singletonFrame a b) - (mkFrameCall (singletonFrame a b) 0 x)), ()) - (mkFrameCall (singletonFrame a b) 0 x_top); + callS E stack (fixSFrame a b) + (mkFrameCall (fixSFrame a b) 0 x)), ()) + (mkFrameCall (fixSFrame a b) 0 x_top); + +-- Build a multi-argument fixed-point of type A1 -> ... -> An -> SpecM B +multiArgFixS : (E:EvType) -> (stack:FunStack) -> (lrt:LetRecType) -> + (LRTType E (pushFunStack (singletonFrame lrt) stack) lrt -> + LRTType E (pushFunStack (singletonFrame lrt) stack) lrt) -> + LRTType E stack lrt; +multiArgFixS E stack lrt body_f = + lrtLambda + lrt (\ (args:LRTInput lrt) -> SpecM E stack (LRTOutput lrt args)) + (\ (top_args:LRTInput lrt) -> + multiFixS + E stack (singletonFrame lrt) + (body_f + (lrtLambda + lrt (\ (args:LRTInput lrt) -> + SpecM E (pushFunStack (singletonFrame lrt) stack) + (LRTOutput lrt args)) + (\ (args:LRTInput lrt) -> + callS E stack (singletonFrame lrt) + (FrameCallOfArgs (singletonFrame lrt) 0 args))), ()) + (FrameCallOfArgs (singletonFrame lrt) 0 top_args)); -- Apply a pure function to the result of a computation fmapS : (E:EvType) -> (stack:FunStack) -> (a b:sort 0) -> (a -> b) -> From c3350ec14aa1f85728d0c4260a76e5bcbb2f46d2 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Wed, 7 Dec 2022 15:27:53 -0800 Subject: [PATCH 07/27] started updating linked_list_mr_solver.saw --- heapster-saw/examples/linked_list_mr_solver.saw | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/heapster-saw/examples/linked_list_mr_solver.saw b/heapster-saw/examples/linked_list_mr_solver.saw index 28cc8093bb..cf86e0a1fb 100644 --- a/heapster-saw/examples/linked_list_mr_solver.saw +++ b/heapster-saw/examples/linked_list_mr_solver.saw @@ -35,9 +35,11 @@ mr_solver_test is_elem is_elem; is_elem_noErrorsSpec <- parse_core "\\ (x:Vec 64 Bool) (y:List (Vec 64 Bool)) -> \ - \ fixM (Vec 64 Bool * List (Vec 64 Bool)) \ + \ fixS VoidEv emptyFunStack \ + \ (Vec 64 Bool * List (Vec 64 Bool)) \ \ (\\ (pr : Vec 64 Bool * List (Vec 64 Bool)) -> Vec 64 Bool) \ - \ (\\ (rec : (x : Vec 64 Bool * List (Vec 64 Bool)) -> CompM (Vec 64 Bool)) \ + \ (\\ (rec : (x : Vec 64 Bool * List (Vec 64 Bool)) -> \ + \ SpecM (pushFunStack (singletonFrame a b) stack) (Vec 64 Bool)) \ \ (x : Vec 64 Bool * List (Vec 64 Bool)) -> \ \ orM (Vec 64 Bool) \ \ (existsM (Vec 64 Bool) (Vec 64 Bool) (returnM (Vec 64 Bool))) \ From 9c63042dce423feb1993164c3f6c779e4b0e068d Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Wed, 7 Dec 2022 15:28:11 -0800 Subject: [PATCH 08/27] updated the core algorithm of the monadifier to use SpecM --- .../src/Verifier/SAW/Cryptol/Monadify.hs | 222 ++++++++++++------ examples/mr_solver/mr_solver_unit_tests.saw | 8 +- saw-core/prelude/Prelude.sawcore | 14 ++ src/SAWScript/Builtins.hs | 7 +- src/SAWScript/Prover/MRSolver/Monad.hs | 2 +- src/SAWScript/Prover/MRSolver/Term.hs | 19 +- 6 files changed, 180 insertions(+), 92 deletions(-) diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs index e1b1a06a4d..8c31fc68dc 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs @@ -5,7 +5,11 @@ {-# LANGUAGE TupleSections #-} {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE DeriveGeneric #-} {- | Module : Verifier.SAW.Cryptol.Monadify @@ -18,8 +22,8 @@ Portability : non-portable (language extensions) This module implements a "monadification" transformation, which converts "pure" SAW core terms that use inconsistent operations like @fix@ and convert them to monadic SAW core terms that use monadic versions of these operations that are -consistent. The monad that is used is the @CompM@ monad that is axiomatized in -the SAW cxore prelude. This is only a partial transformation, meaning that it +consistent. The monad that is used is the @SpecM@ monad that is axiomatized in +the SAW core prelude. This is only a partial transformation, meaning that it will fail on some SAW core terms. Specifically, it requires that all applications @f arg@ in a term either have a non-dependent function type for @f@ (i.e., a function with type @'Pi' x a b@ where @x@ does not occur in @b@) or a @@ -43,7 +47,7 @@ MT(_) = error CompMT(tp = Pi _ _ _) = MT(tp) CompMT(n : Num) = n -CompMT(tp) = CompM MT(tp) +CompMT(tp) = SpecM MT(tp) Term-level translation: @@ -51,7 +55,7 @@ Term-level translation: MonArg(t : tp) ==> MT(tp) MonArg(t) = case Mon(t) of - m : CompM MT(a) => shift \k -> m >>= \x -> k x + m : SpecM MT(a) => shift \k -> m >>= \x -> k x _ => t Mon(t : tp) ==> MT(tp) or CompMT(tp) (which are the same type for pis) @@ -80,6 +84,7 @@ import qualified Control.Monad.Fail as Fail -- import Control.Monad.IO.Class (MonadIO, liftIO) import qualified Data.Text as T import qualified Text.URI as URI +import GHC.Generics (Generic) import Verifier.SAW.Name import Verifier.SAW.Term.Functor @@ -206,6 +211,21 @@ asTypedGlobalDef t = Just $ GlobalDef (ecName ec) (ecVarIndex ec) (ecType ec) t Nothing _ -> Nothing +-- | The event type and function stack arguments to the @SpecM@ type, using type +-- @tm@ for terms +data SpecMParams tm = SpecMParams { specMEvType :: tm, specMStack :: tm } + deriving (Generic, Show) + +-- | The implicit argument version of 'SpecMParams' +type HasSpecMParams = (?specMParams :: SpecMParams OpenTerm) + +-- | The empty function stack +emptyStackOpenTerm :: OpenTerm +emptyStackOpenTerm = globalOpenTerm "Prelude.emptyFunStack" + +-- | Build a 'SpecMParams' with the empty stack from an 'EvType' +paramsOfEvType :: OpenTerm -> SpecMParams OpenTerm +paramsOfEvType ev = SpecMParams ev emptyStackOpenTerm data MonKind = MKType Sort | MKNum | MKFun MonKind MonKind deriving Eq @@ -313,7 +333,7 @@ applyKinds :: MonKind -> [MonType] -> Maybe MonKind applyKinds = foldM applyKind -- | Convert a 'MonType' to the argument type @MT(tp)@ it represents -toArgType :: MonType -> OpenTerm +toArgType :: HasSpecMParams => MonType -> OpenTerm toArgType (MTyForall x k body) = piOpenTerm x (monKindOpenTerm k) (\tp -> toCompType (body $ MTyBase k tp)) toArgType (MTyArrow t1 t2) = @@ -328,10 +348,12 @@ toArgType (MTyBase _ t) = t toArgType (MTyNum n) = n -- | Convert a 'MonType' to the computation type @CompMT(tp)@ it represents -toCompType :: MonType -> OpenTerm +toCompType :: HasSpecMParams => MonType -> OpenTerm toCompType mtp@(MTyForall _ _ _) = toArgType mtp toCompType mtp@(MTyArrow _ _) = toArgType mtp -toCompType mtp = applyOpenTerm (globalOpenTerm "Prelude.CompM") (toArgType mtp) +toCompType mtp = + let SpecMParams { specMEvType = ev, specMStack = stack } = ?specMParams in + applyOpenTermMulti (globalOpenTerm "Prelude.SpecM") [ev, stack, toArgType mtp] -- | The mapping for monadifying Cryptol typeclasses -- FIXME: this is no longer needed, as it is now the identity @@ -372,7 +394,8 @@ typeCtxPureCtx :: MonadifyTypeCtx -> [(LocalName,Term)] typeCtxPureCtx = map (\(x,tp,_) -> (x,tp)) -- | Monadify a type and convert it to its corresponding argument type -monadifyTypeArgType :: HasCallStack => MonadifyTypeCtx -> Term -> OpenTerm +monadifyTypeArgType :: HasCallStack => HasSpecMParams => MonadifyTypeCtx -> + Term -> OpenTerm monadifyTypeArgType ctx t = toArgType $ monadifyType ctx t -- | Apply a monadified type to a type or term argument in the sense of @@ -384,7 +407,8 @@ applyMonType (MTyForall _ _ f) (Left mtp) = f mtp applyMonType _ _ = error "applyMonType: application at incorrect type" -- | Convert a SAW core 'Term' to a monadification type -monadifyType :: HasCallStack => MonadifyTypeCtx -> Term -> MonType +monadifyType :: HasCallStack => HasSpecMParams => MonadifyTypeCtx -> Term -> + MonType {- monadifyType ctx t | trace ("\nmonadifyType:\n" ++ ppTermInTypeCtx ctx t) False = undefined @@ -459,7 +483,8 @@ monadifyType ctx tp = ++ ppTermInTypeCtx ctx tp) -- | Monadify a type-level natural number -monadifyTypeNat :: HasCallStack => MonadifyTypeCtx -> Term -> OpenTerm +monadifyTypeNat :: HasCallStack => HasSpecMParams => MonadifyTypeCtx -> Term -> + OpenTerm monadifyTypeNat _ (asNat -> Just n) = natOpenTerm n monadifyTypeNat ctx (asLocalVar -> Just i) | i < length ctx @@ -505,11 +530,12 @@ instance GetMonType MonTerm where -- | Convert a monadification term to a SAW core term of type @CompMT(tp)@ class ToCompTerm a where - toCompTerm :: a -> OpenTerm + toCompTerm :: HasSpecMParams => a -> OpenTerm instance ToCompTerm ArgMonTerm where toCompTerm (BaseMonTerm mtp t) = - applyOpenTermMulti (globalOpenTerm "Prelude.returnM") [toArgType mtp, t] + applyOpenTermMulti (globalOpenTerm "Prelude.retS") + [specMEvType ?specMParams, specMStack ?specMParams, toArgType mtp, t] toCompTerm (FunMonTerm x tp_in _ body) = lambdaOpenTerm x (toArgType tp_in) (toCompTerm . body . fromArgTerm tp_in) toCompTerm (ForallMonTerm x k body) = @@ -521,14 +547,14 @@ instance ToCompTerm MonTerm where -- | Convert an 'ArgMonTerm' to a SAW core term of type @MT(tp)@ -toArgTerm :: ArgMonTerm -> OpenTerm +toArgTerm :: HasSpecMParams => ArgMonTerm -> OpenTerm toArgTerm (BaseMonTerm _ t) = t toArgTerm t = toCompTerm t -- | Build a monadification term from a term of type @MT(tp)@ class FromArgTerm a where - fromArgTerm :: MonType -> OpenTerm -> a + fromArgTerm :: HasSpecMParams => MonType -> OpenTerm -> a instance FromArgTerm ArgMonTerm where fromArgTerm (MTyForall x k body) t = @@ -542,7 +568,7 @@ instance FromArgTerm MonTerm where fromArgTerm mtp t = ArgMonTerm $ fromArgTerm mtp t -- | Build a monadification term from a computational term of type @CompMT(tp)@ -fromCompTerm :: MonType -> OpenTerm -> MonTerm +fromCompTerm :: HasSpecMParams => MonType -> OpenTerm -> MonTerm fromCompTerm mtp t | isBaseType mtp = CompMonTerm mtp t fromCompTerm mtp t = ArgMonTerm $ fromArgTerm mtp t @@ -585,7 +611,8 @@ monTypeIsSemiPure (MTyNum _) = True -- > SemiP(Pi x Num b) = Pi x Num SemiP(b) -- > SemiP(Pi _ a b) = MT(a) -> SemiP(b) -- > SemiP(a) = MT(a) -fromSemiPureTermFun :: MonType -> ([OpenTerm] -> OpenTerm) -> ArgMonTerm +fromSemiPureTermFun :: HasSpecMParams => MonType -> ([OpenTerm] -> OpenTerm) -> + ArgMonTerm fromSemiPureTermFun (MTyForall x k body) f = ForallMonTerm x k $ \tp -> ArgMonTerm $ fromSemiPureTermFun (body tp) (f . (toArgType tp:)) @@ -595,15 +622,15 @@ fromSemiPureTermFun (MTyArrow t1 t2) f = fromSemiPureTermFun tp f = BaseMonTerm tp (f []) -- | Like 'fromSemiPureTermFun' but use a term rather than a term function -fromSemiPureTerm :: MonType -> OpenTerm -> ArgMonTerm +fromSemiPureTerm :: HasSpecMParams => MonType -> OpenTerm -> ArgMonTerm fromSemiPureTerm mtp t = fromSemiPureTermFun mtp (applyOpenTermMulti t) -- | Build a 'MonTerm' that 'fail's when converted to a term -failMonTerm :: MonType -> String -> MonTerm +failMonTerm :: HasSpecMParams => MonType -> String -> MonTerm failMonTerm mtp str = fromArgTerm mtp (failOpenTerm str) -- | Build an 'ArgMonTerm' that 'fail's when converted to a term -failArgMonTerm :: MonType -> String -> ArgMonTerm +failArgMonTerm :: HasSpecMParams => MonType -> String -> ArgMonTerm failArgMonTerm tp str = fromArgTerm tp (failOpenTerm str) -- | Apply a monadified term to a type or term argument @@ -625,17 +652,17 @@ applyMonTermMulti :: HasCallStack => MonTerm -> [Either MonType ArgMonTerm] -> applyMonTermMulti = foldl applyMonTerm -- | Build a 'MonTerm' from a global of a given argument type -mkGlobalArgMonTerm :: MonType -> Ident -> ArgMonTerm +mkGlobalArgMonTerm :: HasSpecMParams => MonType -> Ident -> ArgMonTerm mkGlobalArgMonTerm tp ident = fromArgTerm tp (globalOpenTerm ident) -- | Build a 'MonTerm' from a 'GlobalDef' of semi-pure type -mkSemiPureGlobalDefTerm :: GlobalDef -> ArgMonTerm +mkSemiPureGlobalDefTerm :: HasSpecMParams => GlobalDef -> ArgMonTerm mkSemiPureGlobalDefTerm glob = fromSemiPureTerm (monadifyType [] $ globalDefType glob) (globalDefOpenTerm glob) -- | Build a 'MonTerm' from a constructor with the given 'PrimName' -mkCtorArgMonTerm :: PrimName Term -> ArgMonTerm +mkCtorArgMonTerm :: HasSpecMParams => PrimName Term -> ArgMonTerm mkCtorArgMonTerm pn | not (isFirstOrderType (primType pn)) = failArgMonTerm (monadifyType [] $ primType pn) @@ -653,7 +680,7 @@ mkCtorArgMonTerm pn = -- before deciding how to monadify itself data MonMacro = MonMacro { macroNumArgs :: Int, - macroApply :: GlobalDef -> [Term] -> MonadifyM MonTerm } + macroApply :: HasSpecMParams => GlobalDef -> [Term] -> MonadifyM MonTerm } -- | Make a simple 'MonMacro' that inspects 0 arguments and just returns a term monMacro0 :: MonTerm -> MonMacro @@ -684,8 +711,26 @@ argGlobalMacro from to = else error ("Monadification macro for " ++ show from ++ " applied incorrectly") --- | An environment of named primitives and how to monadify them -type MonadifyEnv = Map NameInfo MonMacro +-- | An environment for monadification +data MonadifyEnv = MonadifyEnv { + -- | How to monadify named functions + monEnvMonTable :: Map NameInfo MonMacro, + -- | The @EvType@ used for monadification + monEnvEvType :: OpenTerm + } + +-- | Build a 'SpecMParams' with the empty funciton stack from a 'MonadifyEnv' +monEnvParams :: MonadifyEnv -> SpecMParams OpenTerm +monEnvParams env = paramsOfEvType (monEnvEvType env) + +-- | Look up the monadification of a name in a 'MonadifyEnv' +monEnvLookup :: NameInfo -> MonadifyEnv -> Maybe MonMacro +monEnvLookup nmi env = Map.lookup nmi (monEnvMonTable env) + +-- | Add a monadification for a name to a 'MonadifyEnv' +monEnvAdd :: NameInfo -> MonMacro -> MonadifyEnv -> MonadifyEnv +monEnvAdd nmi macro env = + env { monEnvMonTable = Map.insert nmi macro (monEnvMonTable env) } -- | A context for monadifying 'Term's which maintains, for each deBruijn index -- in scope, both its original un-monadified type along with either a 'MonTerm' @@ -726,10 +771,16 @@ data MonadifyROState = MonadifyROState { monStEnv :: MonadifyEnv, -- | The monadification context monStCtx :: MonadifyCtx, + -- | The current @SpecM@ function stack + monStStack :: OpenTerm, -- | The monadified return type of the top-level term being monadified monStTopRetType :: OpenTerm } +-- | Get the monadification table from a 'MonadifyROState' +monStMonTable :: MonadifyROState -> Map NameInfo MonMacro +monStMonTable = monEnvMonTable . monStEnv + -- | The monad for monadifying SAW core terms newtype MonadifyM a = MonadifyM { unMonadifyM :: @@ -738,8 +789,17 @@ newtype MonadifyM a = deriving (Functor, Applicative, Monad, MonadReader MonadifyROState, MonadState MonadifyMemoTable) +usingSpecMParams :: (HasSpecMParams => MonadifyM a) -> MonadifyM a +usingSpecMParams m = + do st <- ask + let ev = monEnvEvType $ monStEnv st + let stack = monStStack st + let ?specMParams = (SpecMParams { specMEvType = ev, + specMStack = stack }) in m + instance Fail.MonadFail MonadifyM where fail str = + usingSpecMParams $ do ret_tp <- topRetType shiftMonadifyM $ \_ -> failMonTerm (mkMonType0 ret_tp) str @@ -755,7 +815,8 @@ shiftMonadifyM f = MonadifyM $ lift $ lift $ cont f resetMonadifyM :: OpenTerm -> MonadifyM MonTerm -> MonadifyM MonTerm resetMonadifyM ret_tp m = do ro_st <- ask - return $ runMonadifyM (monStEnv ro_st) (monStCtx ro_st) ret_tp m + return $ + runMonadifyM (monStEnv ro_st) (monStCtx ro_st) (monStStack ro_st) ret_tp m -- | Get the monadified return type of the top-level term being monadified topRetType :: MonadifyM OpenTerm @@ -765,18 +826,20 @@ topRetType = monStTopRetType <$> ask -- -- FIXME: document the arguments runMonadifyM :: MonadifyEnv -> MonadifyCtx -> OpenTerm -> - MonadifyM MonTerm -> MonTerm -runMonadifyM env ctx top_ret_tp m = - let ro_st = MonadifyROState env ctx top_ret_tp in + OpenTerm -> MonadifyM MonTerm -> MonTerm +runMonadifyM env ctx stack top_ret_tp m = + let ro_st = MonadifyROState env ctx stack top_ret_tp in runCont (evalStateT (runReaderT (unMonadifyM m) ro_st) emptyMemoTable) id -- | Run a monadification computation using a mapping for identifiers that have -- already been monadified and generate a SAW core term runCompleteMonadifyM :: MonadIO m => SharedContext -> MonadifyEnv -> - Term -> MonadifyM MonTerm -> m Term + Term -> MonadifyM MonTerm -> + m Term runCompleteMonadifyM sc env top_ret_tp m = + let ?specMParams = monEnvParams env in liftIO $ completeOpenTerm sc $ toCompTerm $ - runMonadifyM env [] (toArgType $ monadifyType [] top_ret_tp) m + runMonadifyM env [] emptyStackOpenTerm (toArgType $ monadifyType [] top_ret_tp) m -- | Memoize a computation of the monadified term associated with a 'TermIndex' memoMonTerm :: TermIndex -> MonadifyM MonTerm -> MonadifyM MonTerm @@ -813,12 +876,13 @@ memoArgMonTerm i m = argifyMonTerm :: MonTerm -> MonadifyM ArgMonTerm argifyMonTerm (ArgMonTerm mtrm) = return mtrm argifyMonTerm (CompMonTerm mtp trm) = + usingSpecMParams $ do let tp = toArgType mtp top_ret_tp <- topRetType shiftMonadifyM $ \k -> CompMonTerm (mkMonType0 top_ret_tp) $ - applyOpenTermMulti (globalOpenTerm "Prelude.bindM") - [tp, top_ret_tp, trm, + applyOpenTermMulti (globalOpenTerm "Prelude.bindS") + [specMEvType ?specMParams, specMStack ?specMParams, tp, top_ret_tp, trm, lambdaOpenTerm "x" tp (toCompTerm . k . fromArgTerm mtp)] -- | Build a proof of @isFinite n@ by calling @assertFiniteM@ and binding the @@ -840,6 +904,7 @@ assertIsFinite _ = -- | Monadify a type in the context of the 'MonadifyM' monad monadifyTypeM :: HasCallStack => Term -> MonadifyM MonType monadifyTypeM tp = + usingSpecMParams $ do ctx <- monStCtx <$> ask return $ monadifyType (ctxToTypeCtx ctx) tp @@ -851,13 +916,13 @@ monadifyArg _ t = undefined -} monadifyArg mtp t@(STApp { stAppIndex = ix }) = - memoArgMonTerm ix $ monadifyTerm' mtp t + memoArgMonTerm ix $ usingSpecMParams $ monadifyTerm' mtp t monadifyArg mtp t = - monadifyTerm' mtp t >>= argifyMonTerm + usingSpecMParams (monadifyTerm' mtp t) >>= argifyMonTerm -- | Monadify a term to argument type and convert back to a term monadifyArgTerm :: HasCallStack => Maybe MonType -> Term -> MonadifyM OpenTerm -monadifyArgTerm mtp t = toArgTerm <$> monadifyArg mtp t +monadifyArgTerm mtp t = usingSpecMParams (toArgTerm <$> monadifyArg mtp t) -- | Monadify a term monadifyTerm :: Maybe MonType -> Term -> MonadifyM MonTerm @@ -867,19 +932,21 @@ monadifyTerm _ t = undefined -} monadifyTerm mtp t@(STApp { stAppIndex = ix }) = - memoMonTerm ix $ monadifyTerm' mtp t + memoMonTerm ix $ usingSpecMParams $ monadifyTerm' mtp t monadifyTerm mtp t = - monadifyTerm' mtp t + usingSpecMParams $ monadifyTerm' mtp t -- | The main implementation of 'monadifyTerm', which monadifies a term given an -- optional monadification type. The type must be given for introduction forms -- (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' :: HasCallStack => Maybe MonType -> Term -> MonadifyM MonTerm +monadifyTerm' :: HasCallStack => HasSpecMParams => + Maybe MonType -> Term -> MonadifyM MonTerm monadifyTerm' (Just mtp) t@(asLambda -> Just _) = - ask >>= \(MonadifyROState { monStEnv = env, monStCtx = ctx }) -> - return $ monadifyLambdas env ctx mtp t + ask >>= \(MonadifyROState { monStEnv = env, + monStCtx = ctx, monStStack = stack }) -> + return $ monadifyLambdas env ctx stack mtp t {- monadifyTerm' (Just mtp@(MTyForall _ _ _)) t = ask >>= \ro_st -> @@ -940,7 +1007,7 @@ monadifyTerm' _ (asTupleValue -> Just []) = monadifyTerm' _ (asCtor -> Just (pn, args)) = monadifyApply (ArgMonTerm $ mkCtorArgMonTerm pn) args monadifyTerm' _ (asApplyAll -> (asTypedGlobalDef -> Just glob, args)) = - (Map.lookup (globalDefName glob) <$> monStEnv <$> ask) >>= \case + (Map.lookup (globalDefName glob) <$> monStMonTable <$> ask) >>= \case Just macro -> do let (macro_args, reg_args) = splitAt (macroNumArgs macro) args mtrm_f <- macroApply macro glob macro_args @@ -977,34 +1044,35 @@ monadifyApply f [] = return f -- | FIXME: documentation; get our type down to a base type before going into -- the MonadifyM monad -monadifyLambdas :: HasCallStack => MonadifyEnv -> MonadifyCtx -> +monadifyLambdas :: HasCallStack => MonadifyEnv -> MonadifyCtx -> OpenTerm -> MonType -> Term -> MonTerm -monadifyLambdas env ctx (MTyForall _ k tp_f) (asLambda -> - Just (x, x_tp, body)) = +monadifyLambdas env ctx stack (MTyForall _ k tp_f) (asLambda -> + Just (x, x_tp, body)) = -- FIXME: check that monadifyKind x_tp == k ArgMonTerm $ ForallMonTerm x k $ \mtp -> - monadifyLambdas env ((x,x_tp,Left mtp) : ctx) (tp_f mtp) body -monadifyLambdas env ctx (MTyArrow tp_in tp_out) (asLambda -> - Just (x, x_tp, body)) = + monadifyLambdas env ((x,x_tp,Left mtp) : ctx) stack (tp_f mtp) body +monadifyLambdas env ctx stack (MTyArrow tp_in tp_out) (asLambda -> + Just (x, x_tp, body)) = -- FIXME: check that monadifyType x_tp == tp_in ArgMonTerm $ FunMonTerm x tp_in tp_out $ \arg -> - monadifyLambdas env ((x,x_tp,Right (ArgMonTerm arg)) : ctx) tp_out body -monadifyLambdas env ctx tp t = - monadifyEtaExpand env ctx tp tp t [] + monadifyLambdas env ((x,x_tp,Right (ArgMonTerm arg)) : ctx) stack tp_out body +monadifyLambdas env ctx stack tp t = + monadifyEtaExpand env ctx stack tp tp t [] -- | FIXME: documentation -monadifyEtaExpand :: HasCallStack => MonadifyEnv -> MonadifyCtx -> +monadifyEtaExpand :: HasCallStack => MonadifyEnv -> MonadifyCtx -> OpenTerm -> MonType -> MonType -> Term -> [Either MonType ArgMonTerm] -> MonTerm -monadifyEtaExpand env ctx top_mtp (MTyForall x k tp_f) t args = +monadifyEtaExpand env ctx stack top_mtp (MTyForall x k tp_f) t args = ArgMonTerm $ ForallMonTerm x k $ \mtp -> - monadifyEtaExpand env ctx top_mtp (tp_f mtp) t (args ++ [Left mtp]) -monadifyEtaExpand env ctx top_mtp (MTyArrow tp_in tp_out) t args = + monadifyEtaExpand env ctx stack top_mtp (tp_f mtp) t (args ++ [Left mtp]) +monadifyEtaExpand env ctx stack top_mtp (MTyArrow tp_in tp_out) t args = ArgMonTerm $ FunMonTerm "_" tp_in tp_out $ \arg -> - monadifyEtaExpand env ctx top_mtp tp_out t (args ++ [Right arg]) -monadifyEtaExpand env ctx top_mtp mtp t args = + monadifyEtaExpand env ctx stack top_mtp tp_out t (args ++ [Right arg]) +monadifyEtaExpand env ctx stack top_mtp mtp t args = + let ?specMParams = (monEnvParams env) { specMStack = stack } in applyMonTermMulti - (runMonadifyM env ctx (toArgType mtp) (monadifyTerm (Just top_mtp) t)) + (runMonadifyM env ctx stack (toArgType mtp) (monadifyTerm (Just top_mtp) t)) args @@ -1103,11 +1171,12 @@ assertingOrAssumingMacro doAsserting = MonMacro 3 $ \_ args -> atrm_cond <- monadifyArg (Just boolMonType) cond mtp <- monadifyTypeM tp mtrm <- resetMonadifyM (toArgType mtp) $ monadifyTerm (Just mtp) m - let ident = if doAsserting then "Prelude.assertingM" - else "Prelude.assumingM" + let ident = if doAsserting then "Prelude.assertingS" + else "Prelude.assumingS" return $ fromCompTerm mtp $ applyOpenTermMulti (globalOpenTerm ident) - [toArgType mtp, toArgTerm atrm_cond, toCompTerm mtrm] + [specMEvType ?specMParams, specMStack ?specMParams, + toArgType mtp, toArgTerm atrm_cond, toCompTerm mtrm] -- | 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 @@ -1131,7 +1200,7 @@ fin1Macro from to = return $ ArgMonTerm $ fromSemiPureTerm glob_tp_app to_app -- | Helper function: build a @LetRecType@ for a nested pi type -lrtFromMonType :: MonType -> OpenTerm +lrtFromMonType :: HasSpecMParams => MonType -> OpenTerm lrtFromMonType (MTyForall x k body_f) = ctorOpenTerm "Prelude.LRT_Fun" [monKindOpenTerm k, @@ -1153,8 +1222,9 @@ fixMacro = MonMacro 2 $ \_ args -> case args of do mtp <- monadifyTypeM tp amtrm_f <- monadifyArg (Just $ MTyArrow mtp mtp) f return $ fromCompTerm mtp $ - applyOpenTermMulti (globalOpenTerm "Prelude.multiArgFixM") - [lrtFromMonType mtp, toCompTerm amtrm_f] + applyOpenTermMulti (globalOpenTerm "Prelude.multiArgFixS") + [specMEvType ?specMParams, specMStack ?specMParams, + lrtFromMonType mtp, toCompTerm amtrm_f] [(asRecordType -> Just _), _] -> fail "Monadification failed: cannot yet handle mutual recursion" _ -> error "fixMacro: malformed arguments!" @@ -1189,7 +1259,12 @@ mmCustom from_id macro = (ModuleIdentifier from_id, macro) -- | The default monadification environment defaultMonEnv :: MonadifyEnv -defaultMonEnv = +defaultMonEnv = MonadifyEnv { monEnvMonTable = defaultMonTable, + monEnvEvType = globalOpenTerm "Prelude.VoidEv" } + +-- | The default primitive monadification table +defaultMonTable :: Map NameInfo MonMacro +defaultMonTable = Map.fromList [ -- Prelude functions @@ -1295,15 +1370,17 @@ ensureCryptolMLoaded sc = scLoadCryptolMModule sc -- | Monadify a type to its argument type and complete it to a 'Term' -monadifyCompleteArgType :: SharedContext -> Term -> IO Term -monadifyCompleteArgType sc tp = +monadifyCompleteArgType :: SharedContext -> MonadifyEnv -> Term -> + IO Term +monadifyCompleteArgType sc env tp = + let ?specMParams = monEnvParams env in completeOpenTerm sc $ monadifyTypeArgType [] tp -- | Monadify a term of the specified type to a 'MonTerm' and then complete that -- 'MonTerm' to a SAW core 'Term', or 'fail' if this is not possible monadifyCompleteTerm :: SharedContext -> MonadifyEnv -> Term -> Term -> IO Term monadifyCompleteTerm sc env trm tp = - runCompleteMonadifyM sc env tp $ + runCompleteMonadifyM sc env tp $ usingSpecMParams $ monadifyTerm (Just $ monadifyType [] tp) trm -- | Convert a name of a definition to the name of its monadified version @@ -1322,6 +1399,7 @@ monadifyNamedTerm :: SharedContext -> MonadifyEnv -> NameInfo -> Maybe Term -> Term -> IO MonTerm monadifyNamedTerm sc env nmi maybe_trm tp = trace ("Monadifying " ++ T.unpack (toAbsoluteName nmi)) $ + let ?specMParams = monEnvParams env in do let mtp = monadifyType [] tp nmi' <- monadifyName nmi comp_tp <- completeOpenTerm sc $ toCompType mtp @@ -1336,8 +1414,8 @@ monadifyNamedTerm sc env nmi maybe_trm tp = -- | Monadify a term with the specified type along with all constants it -- contains, adding the monadifications of those constants to the monadification -- environment -monadifyTermInEnv :: SharedContext -> MonadifyEnv -> Term -> Term -> - IO (Term, MonadifyEnv) +monadifyTermInEnv :: SharedContext -> MonadifyEnv -> + Term -> Term -> IO (Term, MonadifyEnv) monadifyTermInEnv sc top_env top_trm top_tp = flip runStateT top_env $ do lift $ ensureCryptolMLoaded sc @@ -1345,8 +1423,8 @@ monadifyTermInEnv sc top_env top_trm top_tp = map snd $ Map.toAscList $ getConstantSet top_trm forM_ const_infos $ \(nmi,tp,maybe_body) -> get >>= \env -> - if Map.member nmi env then return () else + if Map.member nmi (monEnvMonTable env) then return () else do mtrm <- lift $ monadifyNamedTerm sc env nmi maybe_body tp - put $ Map.insert nmi (monMacro0 mtrm) env + modify $ monEnvAdd nmi (monMacro0 mtrm) env <- get lift $ monadifyCompleteTerm sc env top_trm top_tp diff --git a/examples/mr_solver/mr_solver_unit_tests.saw b/examples/mr_solver/mr_solver_unit_tests.saw index 75f8aa8521..234836c1b3 100644 --- a/examples/mr_solver/mr_solver_unit_tests.saw +++ b/examples/mr_solver/mr_solver_unit_tests.saw @@ -69,11 +69,11 @@ noErrorsRec1 <- parse_core \ (\\ (f: fixSFun VoidEv emptyFunStack \ \ (Vec 64 Bool) (\\ (_:Vec 64 Bool) -> Vec 64 Bool)) \ \ (x:Vec 64 Bool) -> \ - \ orS VoidEv (singletonStack (Vec 64 Bool) \ - \ (\\ (_:Vec 64 Bool) -> Vec 64 Bool)) \ + \ orS VoidEv (fixSStack (Vec 64 Bool) \ + \ (\\ (_:Vec 64 Bool) -> Vec 64 Bool)) \ \ (Vec 64 Bool) \ - \ (existsS VoidEv (singletonStack (Vec 64 Bool) \ - \ (\\ (_:Vec 64 Bool) -> Vec 64 Bool)) \ + \ (existsS VoidEv (fixSStack (Vec 64 Bool) \ + \ (\\ (_:Vec 64 Bool) -> Vec 64 Bool)) \ \ (Vec 64 Bool)) \ \ (f x))"; diff --git a/saw-core/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore index 2c6db18106..292f78c6a3 100644 --- a/saw-core/prelude/Prelude.sawcore +++ b/saw-core/prelude/Prelude.sawcore @@ -2949,6 +2949,13 @@ primitive assumeS : (E:EvType) -> (stack:FunStack) -> assumeBoolS : (E:EvType) -> (stack:FunStack) -> Bool -> SpecM E stack #(); assumeBoolS E stack b = assumeS E stack (EqTrue b); +-- The specification which assumes that the first argument is True and then +-- runs the second argument +assumingS : (E:EvType) -> (stack:FunStack) -> (a : sort 0) -> Bool -> + SpecM E stack a -> SpecM E stack a; +assumingS E stack a cond m = + bindS E stack #() a (assumeBoolS E stack cond) (\ (_:#()) -> m); + -- Assert a proposition holds primitive assertS : (E:EvType) -> (stack:FunStack) -> (p:Prop) -> SpecM E stack #(); @@ -2957,6 +2964,13 @@ primitive assertS : (E:EvType) -> (stack:FunStack) -> assertBoolS : (E:EvType) -> (stack:FunStack) -> Bool -> SpecM E stack #(); assertBoolS E stack b = assertS E stack (EqTrue b); +-- The specification which asserts that the first argument is True and then +-- runs the second argument +assertingS : (E:EvType) -> (stack:FunStack) -> (a : sort 0) -> Bool -> + SpecM E stack a -> SpecM E stack a; +assertingS E stack a cond m = + bindS E stack #() a (assertBoolS E stack cond) (\ (_:#()) -> m); + -- 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; diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index 8541b3e91f..46580a76c8 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -2296,7 +2296,8 @@ setMonadification sc cry_str saw_str = -- putStrLn ("No Cryptol type for name: " ++ cry_str) >> scTypeOf sc cry_nm_trans _ -> fail ("Could not find type for Cryptol name: " ++ cry_str) - cry_mon_tp <- liftIO $ Monadify.monadifyCompleteArgType sc cry_saw_tp + cry_mon_tp <- + liftIO $ Monadify.monadifyCompleteArgType sc (rwMonadify rw) cry_saw_tp -- Step 3: convert the second string to a typed SAW core term, and if it -- has an existing macro, check that it has the same type as the type for @@ -2307,13 +2308,13 @@ setMonadification sc cry_str saw_str = saw_trm <- liftIO $ scGlobalDef sc saw_ident saw_tp <- liftIO $ scTypeOf sc saw_trm let (tp_to_check, macro) = - case Map.lookup (ModuleIdentifier saw_ident) (rwMonadify rw) of + case Monadify.monEnvLookup (ModuleIdentifier saw_ident) (rwMonadify rw) of Just existing_macro -> (cry_saw_tp, existing_macro) Nothing -> (cry_mon_tp, Monadify.argGlobalMacro cry_nmi saw_ident) liftIO $ scCheckSubtype sc Nothing (TC.TypedTerm saw_trm saw_tp) tp_to_check -- Step 4: Add the generated macro - put (rw { rwMonadify = Map.insert cry_nmi macro (rwMonadify rw) }) + put (rw { rwMonadify = Monadify.monEnvAdd cry_nmi macro (rwMonadify rw) }) parseSharpSATResult :: String -> Maybe Integer parseSharpSATResult s = parse (lines s) diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs index 9281788556..63d599e4c9 100644 --- a/src/SAWScript/Prover/MRSolver/Monad.hs +++ b/src/SAWScript/Prover/MRSolver/Monad.hs @@ -588,7 +588,7 @@ mrConvertible = liftSC4 scConvertibleEval scTypeCheckWHNF True -- | Take a 'FunName' @f@ for a monadic function of type @vars -> SpecM a@ and -- compute the type @SpecM [args/vars]a@ of @f@ applied to @args@. Return the -- type @[args/vars]a@ that @SpecM@ is applied to, along with its parameters. -mrFunOutType :: FunName -> [Term] -> MRM (SpecMParams, Term) +mrFunOutType :: FunName -> [Term] -> MRM (SpecMParams Term, Term) mrFunOutType fname args = mrApplyAll (funNameTerm fname) args >>= mrTypeOf >>= \case (asSpecM -> Just (params, tp)) -> (params,) <$> liftSC1 scWhnf tp diff --git a/src/SAWScript/Prover/MRSolver/Term.hs b/src/SAWScript/Prover/MRSolver/Term.hs index 9f95889009..62911a12c8 100644 --- a/src/SAWScript/Prover/MRSolver/Term.hs +++ b/src/SAWScript/Prover/MRSolver/Term.hs @@ -170,13 +170,8 @@ mrVarCtxOuterToInner = reverse . mrVarCtxInnerToOuter mrVarCtxFromOuterToInner :: [(LocalName,Term)] -> MRVarCtx mrVarCtxFromOuterToInner = mrVarCtxFromInnerToOuter . reverse --- | A Haskell representation of the two non-type parameters of @SpecM@ -data SpecMParams = SpecMParams { specMEvType :: Term, - specMStack :: Term } - deriving (Generic, Show) - -- | Convert a 'SpecMParams' to a list of arguments -specMParamsArgs :: SpecMParams -> [Term] +specMParamsArgs :: SpecMParams Term -> [Term] specMParamsArgs (SpecMParams ev stack) = [ev, stack] -- | A Haskell representation of a @SpecM@ in "monadic normal form" @@ -202,15 +197,15 @@ type EitherElim = (Type,CompFun) -- | A computation function of type @a -> SpecM b@ for some @a@ and @b@ data CompFun -- | An arbitrary term - = CompFunTerm SpecMParams Term + = CompFunTerm (SpecMParams Term) Term -- | A special case for the term @\ (x:a) -> returnM a x@ - | CompFunReturn SpecMParams Type + | CompFunReturn (SpecMParams Term) Type -- | The monadic composition @f >=> g@ | CompFunComp CompFun CompFun deriving (Generic, Show) -- | Apply 'CompFunReturn' to a pair of a 'SpecMParams' and a 'Term' -mkCompFunReturn :: (SpecMParams, Term) -> CompFun +mkCompFunReturn :: (SpecMParams Term, Term) -> CompFun mkCompFunReturn (params, tp) = CompFunReturn params $ Type tp -- | Compose two 'CompFun's, simplifying if one is a 'CompFunReturn' @@ -235,7 +230,7 @@ compFunInputType (CompFunReturn _ t) = Just t compFunInputType _ = Nothing -- | Get the @SpecM@ non-type parameters from a 'CompFun' -compFunSpecMParams :: CompFun -> SpecMParams +compFunSpecMParams :: CompFun -> SpecMParams Term compFunSpecMParams (CompFunTerm params _) = params compFunSpecMParams (CompFunReturn params _) = params compFunSpecMParams (CompFunComp f _) = compFunSpecMParams f @@ -245,7 +240,7 @@ data Comp = CompTerm Term | CompBind Comp CompFun | CompReturn Term deriving (Generic, Show) -- | Match a type as being of the form @SpecM E stack a@ for some @a@ -asSpecM :: Term -> Maybe (SpecMParams, Term) +asSpecM :: Term -> Maybe (SpecMParams Term, Term) asSpecM (asApplyAll -> (isGlobalDef "Prelude.SpecM" -> Just (), [ev, stack, tp])) = return (SpecMParams { specMEvType = ev, specMStack = stack }, tp) asSpecM _ = fail "not a SpecM type!" @@ -474,7 +469,7 @@ instance TermLike Natural where substTermLike _ _ = return deriving anyclass instance TermLike Type -deriving instance TermLike SpecMParams +deriving instance TermLike (SpecMParams Term) deriving instance TermLike NormComp deriving instance TermLike CompFun deriving instance TermLike Comp From b17a83e8903772b939c4263e869d8a2372e23571 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Wed, 7 Dec 2022 15:44:23 -0800 Subject: [PATCH 09/27] fixed mrFreshCallVars to normalize the defs term; fixed a small printing bug --- src/SAWScript/Prover/MRSolver/Solver.hs | 3 ++- src/SAWScript/Prover/MRSolver/Term.hs | 4 ++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs index 5f7a4fa6f0..035c6d94e1 100644 --- a/src/SAWScript/Prover/MRSolver/Solver.hs +++ b/src/SAWScript/Prover/MRSolver/Solver.hs @@ -225,7 +225,8 @@ mrFreshCallVars ev stack frame defs_tm = -- our new variable terms (which are applied to the current uvars; see -- mrVarTerm) fun_tms <- mapM mrVarTerm fun_vars - bodies <- case asNestedPairs defs_tm of + defs_tm' <- liftSC1 scWhnf defs_tm + bodies <- case asNestedPairs defs_tm' of Just defs -> mapM (mrReplaceCallsWithTerms fun_tms >=> lambdaUVarsM) defs Nothing -> throwMRFailure (MalformedDefs defs_tm) diff --git a/src/SAWScript/Prover/MRSolver/Term.hs b/src/SAWScript/Prover/MRSolver/Term.hs index 62911a12c8..72974a5b36 100644 --- a/src/SAWScript/Prover/MRSolver/Term.hs +++ b/src/SAWScript/Prover/MRSolver/Term.hs @@ -597,11 +597,11 @@ instance PrettyInCtx NormComp where prettyAppList [return "ite", return "_", parens <$> prettyInCtx cond, parens <$> prettyInCtx t1, parens <$> prettyInCtx t2] prettyInCtx (Eithers elims eith) = - prettyAppList [return "eithers", return (parens "CompM _"), + prettyAppList [return "eithers", return (parens "SpecM _ _ _"), prettyInCtx (map snd elims), parens <$> prettyInCtx eith] prettyInCtx (MaybeElim tp m f mayb) = prettyAppList [return "maybe", parens <$> prettyInCtx tp, - return (parens "CompM _"), parens <$> prettyInCtx m, + return (parens "SpecM _ _ _"), parens <$> prettyInCtx m, parens <$> prettyInCtx f, parens <$> prettyInCtx mayb] prettyInCtx (OrS t1 t2) = prettyAppList [return "orS", return "_", return "_", return "_", From f9c9486167b9b98ad3eed916470ee81192730169 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Wed, 7 Dec 2022 15:56:26 -0800 Subject: [PATCH 10/27] updated the noErrors spec in linked_list_mr_solver.saw --- .../examples/linked_list_mr_solver.saw | 23 +++++++++++++------ 1 file changed, 16 insertions(+), 7 deletions(-) diff --git a/heapster-saw/examples/linked_list_mr_solver.saw b/heapster-saw/examples/linked_list_mr_solver.saw index cf86e0a1fb..26b88f7a55 100644 --- a/heapster-saw/examples/linked_list_mr_solver.saw +++ b/heapster-saw/examples/linked_list_mr_solver.saw @@ -31,19 +31,28 @@ mr_solver_test is_head is_head; is_elem <- parse_core_mod "linked_list" "is_elem"; -mr_solver_test is_elem is_elem; +//mr_solver_set_debug_level 1; +// mr_solver_test is_elem is_elem; is_elem_noErrorsSpec <- parse_core "\\ (x:Vec 64 Bool) (y:List (Vec 64 Bool)) -> \ \ fixS VoidEv emptyFunStack \ \ (Vec 64 Bool * List (Vec 64 Bool)) \ - \ (\\ (pr : Vec 64 Bool * List (Vec 64 Bool)) -> Vec 64 Bool) \ - \ (\\ (rec : (x : Vec 64 Bool * List (Vec 64 Bool)) -> \ - \ SpecM (pushFunStack (singletonFrame a b) stack) (Vec 64 Bool)) \ + \ (\\ (_ : Vec 64 Bool * List (Vec 64 Bool)) -> Vec 64 Bool) \ + \ (\\ (f : fixSFun VoidEv emptyFunStack \ + \ (Vec 64 Bool * List (Vec 64 Bool)) \ + \ (\\ (pr : Vec 64 Bool * List (Vec 64 Bool)) -> \ + \ Vec 64 Bool)) \ \ (x : Vec 64 Bool * List (Vec 64 Bool)) -> \ - \ orM (Vec 64 Bool) \ - \ (existsM (Vec 64 Bool) (Vec 64 Bool) (returnM (Vec 64 Bool))) \ - \ (rec x)) (x, y)"; + \ orS VoidEv (fixSStack (Vec 64 Bool * List (Vec 64 Bool)) \ + \ (\\ (_ : Vec 64 Bool * List (Vec 64 Bool)) -> \ + \ Vec 64 Bool)) \ + \ (Vec 64 Bool) \ + \ (existsS VoidEv (fixSStack (Vec 64 Bool * List (Vec 64 Bool)) \ + \ (\\ (_ : Vec 64 Bool * List (Vec 64 Bool)) -> \ + \ Vec 64 Bool)) \ + \ (Vec 64 Bool)) \ + \ (f x)) (x, y)"; mr_solver_test is_elem is_elem_noErrorsSpec; mr_solver_prove is_elem {{ is_elem_spec }}; From 1280328589d6c60a8502b68a4c0929ab9af1268f Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Wed, 7 Dec 2022 16:29:17 -0800 Subject: [PATCH 11/27] add debug output to missing mrProveRel case --- src/SAWScript/Prover/MRSolver/SMT.hs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/SAWScript/Prover/MRSolver/SMT.hs b/src/SAWScript/Prover/MRSolver/SMT.hs index c3e9c1051f..c9f8b70d83 100644 --- a/src/SAWScript/Prover/MRSolver/SMT.hs +++ b/src/SAWScript/Prover/MRSolver/SMT.hs @@ -788,7 +788,10 @@ mrProveRel het t1 t2 = tp1 <- mrTypeOf t1 >>= mrSubstEVars tp2 <- mrTypeOf t2 >>= mrSubstEVars tps_eq <- mrConvertible tp1 tp2 - if not het && not tps_eq then return False + if not het && not tps_eq + then do mrDebugPPPrefixSep 2 (nm ++ ": Failure, types not equal:") + tp1 "and" tp2 + return False else do cond_in_ctx <- mrProveRelH het tp1 tp2 t1 t2 res <- withTermInCtx cond_in_ctx mrProvable debugPrint 2 $ nm ++ ": " ++ if res then "Success" else "Failure" From d72e04b44ccdd369e85846b83d2f551490a0d10d Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Wed, 7 Dec 2022 17:09:42 -0800 Subject: [PATCH 12/27] un-comment a line that was accidentally commented by a previous commit --- heapster-saw/examples/linked_list_mr_solver.saw | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/heapster-saw/examples/linked_list_mr_solver.saw b/heapster-saw/examples/linked_list_mr_solver.saw index 26b88f7a55..a80aab1a42 100644 --- a/heapster-saw/examples/linked_list_mr_solver.saw +++ b/heapster-saw/examples/linked_list_mr_solver.saw @@ -31,8 +31,7 @@ mr_solver_test is_head is_head; is_elem <- parse_core_mod "linked_list" "is_elem"; -//mr_solver_set_debug_level 1; -// mr_solver_test is_elem is_elem; +mr_solver_test is_elem is_elem; is_elem_noErrorsSpec <- parse_core "\\ (x:Vec 64 Bool) (y:List (Vec 64 Bool)) -> \ From 1e1b7e1af852afc1bf6632cdf247adb2a2a663b9 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Wed, 7 Dec 2022 17:12:23 -0800 Subject: [PATCH 13/27] fixed mrReplaceCallsWithTerms to use term lifting when it recurses into a variable binding --- src/SAWScript/Prover/MRSolver/Solver.hs | 21 +++++++++++++++++---- 1 file changed, 17 insertions(+), 4 deletions(-) diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs index 035c6d94e1..bb2f3c1127 100644 --- a/src/SAWScript/Prover/MRSolver/Solver.hs +++ b/src/SAWScript/Prover/MRSolver/Solver.hs @@ -129,6 +129,7 @@ import Numeric.Natural (Natural) import Data.List (find, findIndices) import Data.Foldable (foldlM) import Data.Bits (shiftL) +import Control.Monad.Reader import Control.Monad.Except import qualified Data.Map as Map import qualified Data.Text as Text @@ -193,14 +194,26 @@ asCallS _ = Nothing -- either and maybe eliminators). But the implementation here should give the -- correct result for any code we are actually going to see... mrReplaceCallsWithTerms :: [Term] -> Term -> MRM Term -mrReplaceCallsWithTerms tms = - memoFixTermFun $ \recurse t -> case t of +mrReplaceCallsWithTerms top_tms top_t = + flip runReaderT top_tms $ + flip memoFixTermFun top_t $ \recurse t -> case t of (asCallS -> Just (_, i, args)) -> - mrApplyAll (tms!!(fromIntegral i)) args + -- Replace a CallS with its corresponding term + ask >>= \tms -> lift $ mrApplyAll (tms!!(fromIntegral i)) args (asApplyAll -> (isGlobalDef "Prelude.multiFixS" -> Just (), _)) -> -- Don't recurse inside another multiFixS, since it binds new calls return t + (asLambda -> Just (x, tp, body)) -> + -- Lift our terms when we recurse inside a binder; also, not that we don't + -- expect to lift types, so we leave tp alone + do tms <- ask + tms' <- liftTermLike 0 1 tms + body' <- local (const tms') $ recurse body + lift $ liftSC3 scLambda x tp body' + (asPi -> Just _) -> + -- We don't expect to lift types, so we leave them alone + return t _ -> traverseSubterms recurse t @@ -227,7 +240,7 @@ mrFreshCallVars ev stack frame defs_tm = fun_tms <- mapM mrVarTerm fun_vars defs_tm' <- liftSC1 scWhnf defs_tm bodies <- case asNestedPairs defs_tm' of - Just defs -> mapM (mrReplaceCallsWithTerms fun_tms >=> lambdaUVarsM) defs + Just defs -> mapM (lambdaUVarsM >=> mrReplaceCallsWithTerms fun_tms) defs Nothing -> throwMRFailure (MalformedDefs defs_tm) -- Remember the body associated with each fresh function constant From c82e5e339ea5adbec0033370418e09818b16075c Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Fri, 9 Dec 2022 18:24:44 -0800 Subject: [PATCH 14/27] updated the monadified versions of the cryptol primitives to use SpecM --- cryptol-saw-core/saw/CryptolM.sawcore | 680 ++++++++++-------- .../src/Verifier/SAW/Cryptol/Monadify.hs | 163 +++-- src/SAWScript/Builtins.hs | 2 +- 3 files changed, 487 insertions(+), 358 deletions(-) diff --git a/cryptol-saw-core/saw/CryptolM.sawcore b/cryptol-saw-core/saw/CryptolM.sawcore index 2bc36ca777..f4568ada74 100644 --- a/cryptol-saw-core/saw/CryptolM.sawcore +++ b/cryptol-saw-core/saw/CryptolM.sawcore @@ -13,11 +13,12 @@ import Cryptol; primitive proveEqNum : (n m:Num) -> Maybe (Eq Num n m); -- A version of unsafeAssert specialized to the Num type -numAssertEqM : (n m:Num) -> CompM (Eq Num n m); -numAssertEqM n m = - maybe (Eq Num n m) (CompM (Eq Num n m)) - (errorM (Eq Num n m) "numAssertEqM: assertion failed") - (returnM (Eq Num n m)) +numAssertEqS : (E:EvType) -> (stack:FunStack) -> (n m:Num) -> + SpecM E stack (Eq Num n m); +numAssertEqS E stack n m = + maybe (Eq Num n m) (SpecM E stack (Eq Num n m)) + (errorS E stack (Eq Num n m) "numAssertEqS: assertion failed") + (retS E stack (Eq Num n m)) (proveEqNum n m); -- A proof that a Num is finite @@ -32,11 +33,12 @@ checkFinite = (Nothing (isFinite TCInf)); -- Assert that a Num is finite, or fail -assertFiniteM : (n:Num) -> CompM (isFinite n); -assertFiniteM n = - maybe (isFinite n) (CompM (isFinite n)) - (errorM (isFinite n) "assertFiniteM: Num not finite") - (returnM (isFinite n)) +assertFiniteS : (E:EvType) -> (stack:FunStack) -> (n:Num) -> + SpecM E stack (isFinite n); +assertFiniteM E stack n = + maybe (isFinite n) (SpecM E stack (isFinite n)) + (errorS E stack (isFinite n) "assertFiniteM: Num not finite") + (retS E stack (isFinite n)) (checkFinite n); -- Recurse over a Num known to be finite @@ -53,148 +55,193 @@ Num_rec_fin p f = -- The type of monadified sequences, which are just vectors for finite length -- but are sequences of computations for streams -mseq : Num -> sort 0 -> sort 0; -mseq num a = - Num_rec (\ (_:Num) -> sort 0) (\ (n:Nat) -> Vec n a) (Stream (CompM a)) num; - -bvVecMapInvarBindM : (a b c : isort 0) -> (n : Nat) -> (len : Vec n Bool) -> - (a -> CompM b) -> BVVec n len a -> - Bool -> (BVVec n len b -> CompM c) -> CompM c; -bvVecMapInvarBindM a b c n len f xs invar cont = - existsM (BVVec n len b) c (\ (ys0:BVVec n len b) -> - multiArgFixM +mseq : (E:EvType) -> (stack:FunStack) -> Num -> sort 0 -> sort 0; +mseq num E stack a = + Num_rec (\ (_:Num) -> sort 0) (\ (n:Nat) -> Vec n a) + (Stream (SpecM E stack a)) num; + +{- +bvVecMapInvarBindM : (E:EvType) -> (stack:FunStack) -> + (a b c : isort 0) -> (n : Nat) -> (len : Vec n Bool) -> + (a -> SpecM E stack b) -> BVVec n len a -> + Bool -> (BVVec n len b -> SpecM E stack c) -> + SpecM E stack c; +bvVecMapInvarBindM E stack a b c n len f xs invar cont = + bindS E stack (BVVec n len b) c + (existsS E stack (BVVec n len b)) (\ (ys0:BVVec n len b) -> + multiArgFixS + E stack (LRT_Fun (Vec n Bool) (\ (_:Vec n Bool) -> LRT_Fun (BVVec n len b) (\ (_:BVVec n len b) -> LRT_Ret c))) - (\ (rec : Vec n Bool -> BVVec n len b -> CompM c) + (\ (rec : Vec n Bool -> BVVec n len b -> + SpecM E (pushFunStack + (singletonFrame + (LRT_Fun (Vec n Bool) (\ (_:Vec n Bool) -> + LRT_Fun (BVVec n len b) (\ (_:BVVec n len b) -> + LRT_Ret c)))) stack) c) (i:Vec n Bool) (ys:BVVec n len b) -> - invariantHint (CompM c) (and (bvule n i len) invar) - (maybe (is_bvult n i len) (CompM c) + invariantHint + (SpecM E (pushFunStack + (singletonFrame + (LRT_Fun (Vec n Bool) (\ (_:Vec n Bool) -> + LRT_Fun (BVVec n len b) (\ (_:BVVec n len b) -> + LRT_Ret c)))) stack) c) + (and (bvule n i len) invar) + (maybe (is_bvult n i len) + (SpecM E (pushFunStack + (singletonFrame + (LRT_Fun (Vec n Bool) (\ (_:Vec n Bool) -> + LRT_Fun (BVVec n len b) (\ (_:BVVec n len b) -> + LRT_Ret c)))) stack) c) (cont ys) (\ (pf:is_bvult n i len) -> - bindM b c + bindS E stack b c (f (atBVVec n len a xs i pf)) (\ (y:b) -> rec (bvAdd n i (bvNat n 1)) (updBVVec n len b ys i y))) (bvultWithProof n i len))) (bvNat n 0) ys0); -bvVecMapInvarM : (a b : isort 0) -> (n : Nat) -> (len : Vec n Bool) -> - (a -> CompM b) -> BVVec n len a -> - Bool -> CompM (BVVec n len b); -bvVecMapInvarM a b n len f xs invar = - bvVecMapInvarBindM a b (BVVec n len b) n len f xs invar - (returnM (BVVec n len b)); - -bvVecMapM : (a b : isort 0) -> (n : Nat) -> (len : Vec n Bool) -> - (a -> CompM b) -> BVVec n len a -> CompM (BVVec n len b); -bvVecMapM a b n len f xs = bvVecMapInvarM a b n len f xs True; - -vecMapInvarBindM : (a b c : isort 0) -> (n : Nat) -> (a -> CompM b) -> - Vec n a -> Bool -> (Vec n b -> CompM c) -> CompM c; -vecMapInvarBindM a b c n f xs invar cont = +bvVecMapInvarM : (E:EvType) -> (stack:FunStack) -> + (a b : isort 0) -> (n : Nat) -> (len : Vec n Bool) -> + (a -> SpecM E stack b) -> BVVec n len a -> + Bool -> SpecM E stack (BVVec n len b); +bvVecMapInvarM E stack a b n len f xs invar = + bvVecMapInvarBindM E stack a b (BVVec n len b) n len f xs invar + (retS E stack (BVVec n len b)); + +bvVecMapM : (E:EvType) -> (stack:FunStack) -> + (a b : isort 0) -> (n : Nat) -> (len : Vec n Bool) -> + (a -> SpecM E stack b) -> BVVec n len a -> + SpecM E stack (BVVec n len b); +bvVecMapM E stack a b n len f xs = bvVecMapInvarM E stack a b n len f xs True; + +vecMapInvarBindM : (E:EvType) -> (stack:FunStack) -> + (a b c : isort 0) -> (n : Nat) -> (a -> SpecM E stack b) -> + Vec n a -> Bool -> (Vec n b -> SpecM E stack c) -> + SpecM E stack c; +vecMapInvarBindM E stack a b c n f xs invar cont = existsM (Vec n b) c (\ (ys0:Vec n b) -> multiArgFixM (LRT_Fun Nat (\ (_:Nat) -> LRT_Fun (Vec n b) (\ (_:Vec n b) -> LRT_Ret c))) - (\ (rec : Nat -> Vec n b -> CompM c) (i:Nat) (ys:Vec n b) -> - invariantHint (CompM c) (and (ltNat i (Succ n)) invar) - (maybe (IsLtNat i n) (CompM c) + (\ (rec : Nat -> Vec n b -> SpecM E stack c) (i:Nat) (ys:Vec n b) -> + invariantHint (SpecM E stack c) (and (ltNat i (Succ n)) invar) + (maybe (IsLtNat i n) (SpecM E stack c) (cont ys) (\ (pf:IsLtNat i n) -> - bindM b c + bindS E stack b c (f (atWithProof n a xs i pf)) (\ (y:b) -> rec (Succ i) (updWithProof n b ys i y pf))) (proveLtNat i n))) 0 ys0); -vecMapInvarM : (a b : isort 0) -> (n : Nat) -> (a -> CompM b) -> Vec n a -> - Bool -> CompM (Vec n b); -vecMapInvarM a b n f xs invar = - vecMapInvarBindM a b (Vec n b) n f xs invar (returnM (Vec n b)); +vecMapInvarM : (E:EvType) -> (stack:FunStack) -> + (a b : isort 0) -> (n : Nat) -> (a -> SpecM E stack b) -> + Vec n a -> Bool -> SpecM E stack (Vec n b); +vecMapInvarM E stack a b n f xs invar = + vecMapInvarBindM E stack a b (Vec n b) n f xs invar (retS E stack (Vec n b)); + +vecMapM : (E:EvType) -> (stack:FunStack) -> (a b : isort 0) -> (n : Nat) -> + (a -> SpecM E stack b) -> Vec n a -> SpecM E stack (Vec n b); +vecMapM E stack a b n f xs = vecMapInvarM E stack a b n f xs True; +-} -vecMapM : (a b : isort 0) -> (n : Nat) -> (a -> CompM b) -> Vec n a -> - CompM (Vec n b); -vecMapM a b n f xs = vecMapInvarM a b n f xs True; +primitive +vecMapM : (E:EvType) -> (stack:FunStack) -> (a b : isort 0) -> (n : Nat) -> + (a -> SpecM E stack b) -> Vec n a -> SpecM E stack (Vec n b); -- Computational version of seqMap -seqMapM : (a b : sort 0) -> (n : Num) -> (a -> CompM b) -> mseq n a -> - CompM (mseq n b); -seqMapM a b n_top f = - Num_rec (\ (n:Num) -> mseq n a -> CompM (mseq n b)) - (\ (n:Nat) -> vecMapM a b n f) - (\ (s:Stream (CompM a)) -> - returnM (Stream (CompM b)) - (streamMap (CompM a) (CompM b) - (\ (m:CompM a) -> bindM a b m f) s)) +seqMapM : (E:EvType) -> (stack:FunStack) -> + (a b : sort 0) -> (n : Num) -> (a -> SpecM E stack b) -> + mseq E stack n a -> SpecM E stack (mseq E stack n b); +seqMapM E stack a b n_top f = + Num_rec (\ (n:Num) -> mseq E stack n a -> SpecM E stack (mseq E stack n b)) + (\ (n:Nat) -> vecMapM E stack a b n f) + (\ (s:Stream (SpecM E stack a)) -> + retS E stack (Stream (SpecM E stack b)) + (streamMap (SpecM E stack a) (SpecM E stack b) + (\ (m:SpecM E stack a) -> bindS E stack a b m f) s)) n_top; -mseq_cong1 : (m : Num) -> (n : Num) -> (a : sort 0) -> - Eq Num m n -> Eq (sort 0) (mseq m a) (mseq n a); -mseq_cong1 m n a eq_mn = - eq_cong Num m n eq_mn (sort 0) (\ (x:Num) -> mseq x a); +mseq_cong1 : (E:EvType) -> (stack:FunStack) -> + (m : Num) -> (n : Num) -> (a : sort 0) -> + Eq Num m n -> Eq (sort 0) (mseq E stack m a) (mseq E stack n a); +mseq_cong1 E stack m n a eq_mn = + eq_cong Num m n eq_mn (sort 0) (\ (x:Num) -> mseq E stack x a); -- Convert a seq to an mseq -seqToMseq : (n:Num) -> (a:sort 0) -> seq n a -> mseq n a; -seqToMseq n_top a = - Num_rec (\ (n:Num) -> seq n a -> mseq n a) +seqToMseq : (E:EvType) -> (stack:FunStack) -> + (n:Num) -> (a:sort 0) -> seq n a -> mseq E stack n a; +seqToMseq E stack n_top a = + Num_rec (\ (n:Num) -> seq n a -> mseq E stack n a) (\ (n:Nat) (v:Vec n a) -> v) - (streamMap a (CompM a) (returnM a)) + (streamMap a (SpecM E stack a) (retS E stack a)) n_top; -------------------------------------------------------------------------------- -- Auxiliary functions -bvVecAtM : (n : Nat) -> (len : Vec n Bool) -> (a : isort 0) -> - BVVec n len a -> Vec n Bool -> CompM a; -bvVecAtM n len a xs i = - maybe (is_bvult n i len) (CompM a) - (errorM a "bvVecAtM: invalid sequence index") - (\ (pf:is_bvult n i len) -> returnM a (atBVVec n len a xs i pf)) +bvVecAtM : (E:EvType) -> (stack:FunStack) -> + (n : Nat) -> (len : Vec n Bool) -> (a : isort 0) -> + BVVec n len a -> Vec n Bool -> SpecM E stack a; +bvVecAtM E stack n len a xs i = + maybe (is_bvult n i len) (SpecM E stack a) + (errorS E stack a "bvVecAtM: invalid sequence index") + (\ (pf:is_bvult n i len) -> retS E stack a (atBVVec n len a xs i pf)) (bvultWithProof n i len); -atM : (n : Nat) -> (a : isort 0) -> Vec n a -> Nat -> CompM a; -atM n a xs i = - maybe (IsLtNat i n) (CompM a) - (errorM a "atM: invalid sequence index") - (\ (pf:IsLtNat i n) -> returnM a (atWithProof n a xs i pf)) +atM : (E:EvType) -> (stack:FunStack) -> + (n : Nat) -> (a : isort 0) -> Vec n a -> Nat -> SpecM E stack a; +atM E stack n a xs i = + maybe (IsLtNat i n) (SpecM E stack a) + (errorS E stack a "atM: invalid sequence index") + (\ (pf:IsLtNat i n) -> retS E stack a (atWithProof n a xs i pf)) (proveLtNat i n); -bvVecUpdateM : (n : Nat) -> (len : Vec n Bool) -> (a : isort 0) -> - BVVec n len a -> Vec n Bool -> a -> CompM (BVVec n len a); -bvVecUpdateM n len a xs i x = - maybe (is_bvult n i len) (CompM (BVVec n len a)) - (errorM (BVVec n len a) "bvVecUpdateM: invalid sequence index") - (\ (_:is_bvult n i len) -> returnM (BVVec n len a) - (updBVVec n len a xs i x)) +bvVecUpdateM : (E:EvType) -> (stack:FunStack) -> + (n : Nat) -> (len : Vec n Bool) -> (a : isort 0) -> + BVVec n len a -> Vec n Bool -> a -> + SpecM E stack (BVVec n len a); +bvVecUpdateM E stack n len a xs i x = + maybe (is_bvult n i len) (SpecM E stack (BVVec n len a)) + (errorS E stack (BVVec n len a) "bvVecUpdateM: invalid sequence index") + (\ (_:is_bvult n i len) -> retS E stack (BVVec n len a) + (updBVVec n len a xs i x)) (bvultWithProof n i len); -fromBVVecUpdateM : (n : Nat) -> (len : Vec n Bool) -> (a : isort 0) -> +fromBVVecUpdateM : (E:EvType) -> (stack:FunStack) -> + (n : Nat) -> (len : Vec n Bool) -> (a : isort 0) -> BVVec n len a -> Vec n Bool -> a -> - a -> (m : Nat) -> CompM (Vec m a); -fromBVVecUpdateM n len a xs i x def m = - maybe (is_bvult n i len) (CompM (Vec m a)) - (errorM (Vec m a) "bvVecUpdateM: invalid sequence index") - (\ (_:is_bvult n i len) -> returnM (Vec m a) - (genFromBVVec n len a - (updBVVec n len a xs i x) def m)) + a -> (m : Nat) -> SpecM E stack (Vec m a); +fromBVVecUpdateM E stack n len a xs i x def m = + maybe (is_bvult n i len) (SpecM E stack (Vec m a)) + (errorS E stack (Vec m a) "bvVecUpdateM: invalid sequence index") + (\ (_:is_bvult n i len) -> retS E stack (Vec m a) + (genFromBVVec n len a + (updBVVec n len a xs i x) def m)) (bvultWithProof n i len); -updateM : (n : Nat) -> (a : isort 0) -> Vec n a -> Nat -> a -> CompM (Vec n a); -updateM n a xs i x = - maybe (IsLtNat i n) (CompM (Vec n a)) - (errorM (Vec n a) "updateM: invalid sequence index") - (\ (pf:IsLtNat i n) -> returnM (Vec n a) (updWithProof n a xs i x pf)) +updateM : (E:EvType) -> (stack:FunStack) -> + (n : Nat) -> (a : isort 0) -> Vec n a -> Nat -> a -> + SpecM E stack (Vec n a); +updateM E stack n a xs i x = + maybe (IsLtNat i n) (SpecM E stack (Vec n a)) + (errorS E stack (Vec n a) "updateM: invalid sequence index") + (\ (pf:IsLtNat i n) -> retS E stack (Vec n a) (updWithProof n a xs i x pf)) (proveLtNat i n); -eListSelM : (a : isort 0) -> (n : Num) -> mseq n a -> Nat -> CompM a; -eListSelM a = - Num_rec (\ (n:Num) -> mseq n a -> Nat -> CompM a) +eListSelM : (E:EvType) -> (stack:FunStack) -> + (a : isort 0) -> (n : Num) -> mseq E stack n a -> Nat -> + SpecM E stack a; +eListSelM E stack a = + Num_rec (\ (n:Num) -> mseq E stack n a -> Nat -> SpecM E stack a) (\ (n:Nat) -> atM n a) - (eListSel (CompM a) TCInf); + (eListSel (SpecM E stack a) TCInf); -------------------------------------------------------------------------------- @@ -202,18 +249,23 @@ eListSelM a = -- FIXME primitive -fromM : (a b : sort 0) -> (m n : Num) -> mseq m a -> (a -> CompM (mseq n b)) -> - CompM (seq (tcMul m n) (a * b)); +fromM : (E:EvType) -> (stack:FunStack) -> + (a b : sort 0) -> (m n : Num) -> mseq E stack m a -> + (a -> SpecM E stack (mseq E stack n b)) -> + SpecM E stack (seq (tcMul m n) (a * b)); -- FIXME primitive -mletM : (a b : sort 0) -> (n : Num) -> a -> (a -> CompM (mseq n b)) -> - CompM (mseq n (a * b)); +mletM : (E:EvType) -> (stack:FunStack) -> + (a b : sort 0) -> (n : Num) -> a -> + (a -> SpecM E stack (mseq E stack n b)) -> + SpecM E stack (mseq E stack n (a * b)); -- FIXME primitive -seqZipM : (a b : sort 0) -> (m n : Num) -> mseq m a -> mseq n b -> - CompM (mseq (tcMin m n) (a * b)); +seqZipM : (E:EvType) -> (stack:FunStack) -> + (a b : sort 0) -> (m n : Num) -> mseq E stack m a -> + mseq E stack n b -> SpecM E stack (mseq E stack (tcMin m n) (a * b)); {- seqZipM a b m n ms1 ms2 = seqMap @@ -228,101 +280,120 @@ seqZipM a b m n ms1 ms2 = -- Monadic versions of the Cryptol typeclass instances -- PEq -PEqMSeq : (n:Num) -> isFinite n -> (a:isort 0) -> PEq a -> PEq (mseq n a); -PEqMSeq = - Num_rec_fin (\ (n:Num) -> (a:isort 0) -> PEq a -> PEq (mseq n a)) +PEqMSeq : (E:EvType) -> (stack:FunStack) -> + (n:Num) -> isFinite n -> (a:isort 0) -> PEq a -> + PEq (mseq E stack n a); +PEqMSeq E stack = + Num_rec_fin (\ (n:Num) -> (a:isort 0) -> PEq a -> PEq (mseq E stack n a)) (\ (n:Nat) -> PEqVec n); -PEqMSeqBool : (n : Num) -> isFinite n -> PEq (mseq n Bool); -PEqMSeqBool = - Num_rec_fin (\ (n:Num) -> PEq (mseq n Bool)) PEqWord; +PEqMSeqBool : (E:EvType) -> (stack:FunStack) -> + (n : Num) -> isFinite n -> PEq (mseq E stack n Bool); +PEqMSeqBool E stack = + Num_rec_fin (\ (n:Num) -> PEq (mseq E stack n Bool)) PEqWord; -- PCmp -PCmpMSeq : (n:Num) -> isFinite n -> (a:isort 0) -> PCmp a -> PCmp (mseq n a); -PCmpMSeq = - Num_rec_fin (\ (n:Num) -> (a:isort 0) -> PCmp a -> PCmp (mseq n a)) +PCmpMSeq : (E:EvType) -> (stack:FunStack) -> + (n:Num) -> isFinite n -> (a:isort 0) -> PCmp a -> + PCmp (mseq E stack n a); +PCmpMSeq E stack = + Num_rec_fin (\ (n:Num) -> (a:isort 0) -> PCmp a -> PCmp (mseq E stack n a)) (\ (n:Nat) -> PCmpVec n); -PCmpMSeqBool : (n : Num) -> isFinite n -> PCmp (seq n Bool); -PCmpMSeqBool = +PCmpMSeqBool : (E:EvType) -> (stack:FunStack) -> + (n : Num) -> isFinite n -> PCmp (seq n Bool); +PCmpMSeqBool E stack = Num_rec_fin (\ (n:Num) -> PCmp (seq n Bool)) PCmpWord; -- PSignedCmp -PSignedCmpMSeq : (n:Num) -> isFinite n -> (a:isort 0) -> PSignedCmp a -> - PSignedCmp (mseq n a); -PSignedCmpMSeq = +PSignedCmpMSeq : (E:EvType) -> (stack:FunStack) -> + (n:Num) -> isFinite n -> (a:isort 0) -> PSignedCmp a -> + PSignedCmp (mseq E stack n a); +PSignedCmpMSeq E stack = Num_rec_fin (\ (n:Num) -> (a:isort 0) -> PSignedCmp a -> - PSignedCmp (mseq n a)) + PSignedCmp (mseq E stack n a)) (\ (n:Nat) -> PSignedCmpVec n); -PSignedCmpMSeqBool : (n : Num) -> isFinite n -> PSignedCmp (seq n Bool); -PSignedCmpMSeqBool = +PSignedCmpMSeqBool : (E:EvType) -> (stack:FunStack) -> + (n : Num) -> isFinite n -> PSignedCmp (mseq E stack n Bool); +PSignedCmpMSeqBool E stack = Num_rec_fin (\ (n:Num) -> PSignedCmp (seq n Bool)) PSignedCmpWord; -- PZero -PZeroCompM : (a : sort 0) -> PZero a -> PZero (CompM a); -PZeroCompM = returnM; - -PZeroMSeq : (n : Num) -> (a : sort 0) -> PZero a -> PZero (mseq n a); -PZeroMSeq n_top a pa = - Num_rec (\ (n:Num) -> PZero (mseq n a)) +PZeroSpecM : (E:EvType) -> (stack:FunStack) -> + (a : sort 0) -> PZero a -> PZero (SpecM E stack a); +PZeroSpecM E stack = retS E stack; + +PZeroMSeq : (E:EvType) -> (stack:FunStack) -> + (n : Num) -> (a : sort 0) -> PZero a -> PZero (mseq E stack n a); +PZeroMSeq E stack n_top a pa = + Num_rec (\ (n:Num) -> PZero (mseq E stack n a)) (\ (n:Nat) -> seqConst (TCNum n) a pa) - (seqConst TCInf (CompM a) (returnM a pa)) + (seqConst TCInf (SpecM E stack a) (retS E stack a pa)) n_top; -- PLogic -PLogicCompM : (a : sort 0) -> PLogic a -> PLogic (CompM a); -PLogicCompM a pa = - { logicZero = returnM a (pa.logicZero) - , and = fmapM2 a a a (pa.and) - , or = fmapM2 a a a (pa.or) - , xor = fmapM2 a a a (pa.xor) - , not = fmapM a a (pa.not) +PLogicSpecM : (E:EvType) -> (stack:FunStack) -> + (a : sort 0) -> PLogic a -> PLogic (SpecM E stack a); +PLogicSpecM E stack a pa = + { logicZero = retS E stack a (pa.logicZero) + , and = fmapS2 E stack a a a (pa.and) + , or = fmapS2 E stack a a a (pa.or) + , xor = fmapS2 E stack a a a (pa.xor) + , not = fmapS E stack a a (pa.not) }; -PLogicMSeq : (n : Num) -> (a : isort 0) -> PLogic a -> PLogic (mseq n a); -PLogicMSeq n_top a pa = - Num_rec (\ (n:Num) -> PLogic (mseq n a)) +PLogicMSeq : (E:EvType) -> (stack:FunStack) -> + (n : Num) -> (a : isort 0) -> PLogic a -> + PLogic (mseq E stack n a); +PLogicMSeq E stack n_top a pa = + Num_rec (\ (n:Num) -> PLogic (mseq E stack n a)) (\ (n:Nat) -> PLogicVec n a pa) - (PLogicStream (CompM a) (PLogicCompM a pa)) + (PLogicStream (SpecM E stack a) (PLogicSpecM E stack a pa)) n_top; -PLogicMSeqBool : (n : Num) -> isFinite n -> PLogic (mseq n Bool); -PLogicMSeqBool = - Num_rec_fin (\ (n:Num) -> PLogic (mseq n Bool)) PLogicWord; +PLogicMSeqBool : (E:EvType) -> (stack:FunStack) -> + (n : Num) -> isFinite n -> PLogic (mseq E stack n Bool); +PLogicMSeqBool E stack = + Num_rec_fin (\ (n:Num) -> PLogic (mseq E stack n Bool)) PLogicWord; -- PRing -PRingCompM : (a : sort 0) -> PRing a -> PRing (CompM a); -PRingCompM a pa = - { ringZero = returnM a (pa.ringZero) - , add = fmapM2 a a a (pa.add) - , sub = fmapM2 a a a (pa.sub) - , mul = fmapM2 a a a (pa.mul) - , neg = fmapM a a (pa.neg) - , int = \ (i : Integer) -> returnM a (pa.int i) +PRingSpecM : (E:EvType) -> (stack:FunStack) -> + (a : sort 0) -> PRing a -> PRing (SpecM E stack a); +PRingSpecM E stack a pa = + { ringZero = retS E stack a (pa.ringZero) + , add = fmapS2 E stack a a a (pa.add) + , sub = fmapS2 E stack a a a (pa.sub) + , mul = fmapS2 E stack a a a (pa.mul) + , neg = fmapS E stack a a (pa.neg) + , int = \ (i : Integer) -> retS E stack a (pa.int i) }; -PRingMSeq : (n : Num) -> (a : isort 0) -> PRing a -> PRing (mseq n a); -PRingMSeq n_top a pa = - Num_rec (\ (n:Num) -> PRing (mseq n a)) +PRingMSeq : (E:EvType) -> (stack:FunStack) -> + (n : Num) -> (a : isort 0) -> PRing a -> PRing (mseq E stack n a); +PRingMSeq E stack n_top a pa = + Num_rec (\ (n:Num) -> PRing (mseq E stack n a)) (\ (n:Nat) -> PRingVec n a pa) - (PRingStream (CompM a) (PRingCompM a pa)) + (PRingStream (SpecM E stack a) (PRingSpecM E stack a pa)) n_top; -PRingMSeqBool : (n : Num) -> isFinite n -> PRing (mseq n Bool); -PRingMSeqBool = - Num_rec_fin (\ (n:Num) -> PRing (mseq n Bool)) PRingWord; +PRingMSeqBool : (E:EvType) -> (stack:FunStack) -> + (n : Num) -> isFinite n -> PRing (mseq E stack n Bool); +PRingMSeqBool E stack = + Num_rec_fin (\ (n:Num) -> PRing (mseq E stack n Bool)) PRingWord; -- Integral -PIntegralMSeqBool : (n : Num) -> isFinite n -> PIntegral (mseq n Bool); -PIntegralMSeqBool = - Num_rec_fin (\ (n:Num) -> PIntegral (mseq n Bool)) PIntegralWord; +PIntegralMSeqBool : (E:EvType) -> (stack:FunStack) -> + (n : Num) -> isFinite n -> PIntegral (mseq E stack n Bool); +PIntegralMSeqBool E stack = + Num_rec_fin (\ (n:Num) -> PIntegral (mseq E stack n Bool)) PIntegralWord; -- PLiteral -PLiteralSeqBoolM : (n : Num) -> isFinite n -> PLiteral (mseq n Bool); -PLiteralSeqBoolM = - Num_rec_fin (\ (n:Num) -> PLiteral (mseq n Bool)) bvNat; +PLiteralSeqBoolM : (E:EvType) -> (stack:FunStack) -> + (n : Num) -> isFinite n -> PLiteral (mseq E stack n Bool); +PLiteralSeqBoolM E stack = + Num_rec_fin (\ (n:Num) -> PLiteral (mseq E stack n Bool)) bvNat; -------------------------------------------------------------------------------- @@ -343,65 +414,76 @@ atCryM = at; -- just use Num_rec_fin directly, rather than using it and then calling out to -- the non-monadic version with finNumRec. -ecShiftLM : (m : Num) -> (ix a : sort 0) -> PIntegral ix -> PZero a -> - mseq m a -> ix -> mseq m a; -ecShiftLM = +ecShiftLM : (E:EvType) -> (stack:FunStack) -> + (m : Num) -> (ix a : sort 0) -> PIntegral ix -> PZero a -> + mseq E stack m a -> ix -> mseq E stack m a; +ecShiftLM E stack = Num_rec (\ (m:Num) -> (ix a : sort 0) -> PIntegral ix -> PZero a -> - mseq m a -> ix -> mseq m a) + mseq E stack m a -> ix -> mseq E stack m a) (\ (m:Nat) -> ecShiftL (TCNum m)) (\ (ix a : sort 0) (pix:PIntegral ix) (pa:PZero a) -> - ecShiftL TCInf ix (CompM a) pix (PZeroCompM a pa)); + ecShiftL TCInf ix (SpecM E stack a) pix (PZeroSpecM E stack a pa)); -ecShiftRM : (m : Num) -> (ix a : sort 0) -> PIntegral ix -> PZero a -> - mseq m a -> ix -> mseq m a; -ecShiftRM = +ecShiftRM : (E:EvType) -> (stack:FunStack) -> + (m : Num) -> (ix a : sort 0) -> PIntegral ix -> PZero a -> + mseq E stack m a -> ix -> mseq E stack m a; +ecShiftRM E satck = Num_rec (\ (m:Num) -> (ix a : sort 0) -> PIntegral ix -> PZero a -> - mseq m a -> ix -> mseq m a) + mseq E stack m a -> ix -> mseq E stack m a) (\ (m:Nat) -> ecShiftR (TCNum m)) (\ (ix a : sort 0) (pix:PIntegral ix) (pa:PZero a) -> - ecShiftR TCInf ix (CompM a) pix (PZeroCompM a pa)); + ecShiftR TCInf ix (SpecM E stack a) pix (PZeroSpecM E stack a pa)); -ecSShiftRM : (n : Num) -> isFinite n -> (ix : sort 0) -> PIntegral ix -> - mseq n Bool -> ix -> mseq n Bool; -ecSShiftRM = +ecSShiftRM : (E:EvType) -> (stack:FunStack) -> + (n : Num) -> isFinite n -> (ix : sort 0) -> PIntegral ix -> + mseq E stack n Bool -> ix -> mseq E stack n Bool; +ecSShiftRM E stack = Num_rec_fin - (\ (n:Num) -> (ix : sort 0) -> PIntegral ix -> mseq n Bool -> ix -> - mseq n Bool) + (\ (n:Num) -> (ix : sort 0) -> PIntegral ix -> mseq E stack n Bool -> ix -> + mseq E stack n Bool) (\ (n:Nat) -> ecSShiftR (TCNum n)); -ecRotLM : (m : Num) -> isFinite m -> (ix a : sort 0) -> PIntegral ix -> - mseq m a -> ix -> mseq m a; -ecRotLM = +ecRotLM : (E:EvType) -> (stack:FunStack) -> + (m : Num) -> isFinite m -> (ix a : sort 0) -> PIntegral ix -> + mseq E stack m a -> ix -> mseq E stack m a; +ecRotLM E stack = Num_rec_fin - (\ (m:Num) -> (ix a : sort 0) -> PIntegral ix -> mseq m a -> ix -> mseq m a) + (\ (m:Num) -> (ix a : sort 0) -> PIntegral ix -> mseq E stack m a -> ix -> + mseq E stack m a) (\ (m:Nat) -> ecRotL (TCNum m)); -ecRotRM : (m : Num) -> isFinite m -> (ix a : sort 0) -> PIntegral ix -> - mseq m a -> ix -> mseq m a; -ecRotRM = +ecRotRM : (E:EvType) -> (stack:FunStack) -> + (m : Num) -> isFinite m -> (ix a : sort 0) -> PIntegral ix -> + mseq E stack m a -> ix -> mseq E stack m a; +ecRotRM E stack = Num_rec_fin - (\ (m:Num) -> (ix a : sort 0) -> PIntegral ix -> mseq m a -> ix -> mseq m a) + (\ (m:Num) -> (ix a : sort 0) -> PIntegral ix -> mseq E stack m a -> ix -> + mseq E stack m a) (\ (m:Nat) -> ecRotR (TCNum m)); -ecCatM : (m : Num) -> isFinite m -> (n : Num) -> (a : sort 0) -> - mseq m a -> mseq n a -> mseq (tcAdd m n) a; -ecCatM = +ecCatM : (E:EvType) -> (stack:FunStack) -> + (m : Num) -> isFinite m -> (n : Num) -> (a : sort 0) -> + mseq E stack m a -> mseq E stack n a -> mseq E stack (tcAdd m n) a; +ecCatM E stack = Num_rec_fin - (\ (m:Num) -> (n:Num) -> (a:sort 0) -> mseq m a -> mseq n a -> - mseq (tcAdd m n) a) + (\ (m:Num) -> (n:Num) -> (a:sort 0) -> mseq E stack m a -> mseq E stack n a -> + mseq E stack (tcAdd m n) a) (\ (m:Nat) -> Num_rec - (\ (n:Num) -> (a:isort 0) -> Vec m a -> mseq n a -> - mseq (tcAdd (TCNum m) n) a) + (\ (n:Num) -> (a:isort 0) -> Vec m a -> mseq E stack n a -> + mseq E stack (tcAdd (TCNum m) n) a) -- Case for (TCNum m, TCNum n) (\ (n:Nat) -> \ (a:isort 0) -> append m n a) -- Case for (TCNum m, TCInf) (\ (a:isort 0) (v:Vec m a) -> - streamAppend (CompM a) m (map a (CompM a) (returnM a) m v))); + streamAppend (SpecM E stack a) m + (map a (SpecM E stack a) (retS E stack a) m v))); -- FIXME primitive -ecTakeM : (m n : Num) -> (a : sort 0) -> mseq (tcAdd m n) a -> mseq m a; +ecTakeM : (E:EvType) -> (stack:FunStack) -> + (m n : Num) -> (a : sort 0) -> mseq E stack (tcAdd m n) a -> + mseq E stack m a; {- ecTakeM = Num_rec (\ (m:Num) -> (n:Num) -> (a:sort 0) -> mseq (tcAdd m n) a -> mseq m a) @@ -411,45 +493,47 @@ ecTakeM = -} -- An alternate version of join from Prelude to get around the default Prim -joinCryM : (m n : Nat) - -> (a : isort 0) - -> Vec m (Vec n a) - -> Vec (mulNat m n) a; +joinCryM : (m n : Nat) -> (a : isort 0) -> + Vec m (Vec n a) -> Vec (mulNat m n) a; joinCryM m n a v = genCryM (mulNat m n) a (\ (i : Nat) -> atCryM n a (at m (Vec n a) v (divNat i n)) (modNat i n)); -- FIXME primitive -ecDropM : (m : Num) -> isFinite m -> (n : Num) -> (a : sort 0) -> - mseq (tcAdd m n) a -> mseq n a; - -ecJoinM : (m n : Num) -> (a : sort 0) -> mseq m (mseq n a) -> mseq (tcMul m n) a; -ecJoinM = +ecDropM : (E:EvType) -> (stack:FunStack) -> + (m : Num) -> isFinite m -> (n : Num) -> (a : sort 0) -> + mseq E stack (tcAdd m n) a -> mseq E stack n a; + +ecJoinM : (E:EvType) -> (stack:FunStack) -> + (m n : Num) -> (a : sort 0) -> mseq E stack m (mseq E stack n a) -> + mseq E stack (tcMul m n) a; +ecJoinM E stack = Num_rec - (\ (m:Num) -> (n:Num) -> (a:isort 0) -> mseq m (mseq n a) -> - mseq (tcMul m n) a) + (\ (m:Num) -> (n:Num) -> (a:isort 0) -> mseq E stack m (mseq E stack n a) -> + mseq E stack (tcMul m n) a) (\ (m:Nat) -> finNumRec - (\ (n:Num) -> (a:isort 0) -> Vec m (mseq n a) -> - mseq (tcMul (TCNum m) n) a) + (\ (n:Num) -> (a:isort 0) -> Vec m (mseq E stack n a) -> + mseq E stack (tcMul (TCNum m) n) a) -- Case for (TCNum m, TCNum n) (\ (n:Nat) -> \ (a:isort 0) -> joinCryM m n a)) -- No case for (TCNum m, TCInf), shoudn't happen (finNumRec - (\ (n:Num) -> (a:isort 0) -> Stream (CompM (mseq n a)) -> - mseq (tcMul TCInf n) a) + (\ (n:Num) -> (a:isort 0) -> Stream (SpecM E stack (mseq E stack n a)) -> + mseq E stack (tcMul TCInf n) a) -- Case for (TCInf, TCNum n) (\ (n:Nat) -> \ (a:isort 0) -> natCase - (\ (n':Nat) -> Stream (CompM (Vec n' a)) -> - mseq (if0Nat Num n' (TCNum 0) TCInf) a) - (\ (s:Stream (CompM (Vec 0 a))) -> EmptyVec a) - (\ (n':Nat) -> \ (s:Stream (CompM (Vec (Succ n') a))) -> - MkStream (CompM a) (\ (i:Nat) -> - fmapM (Vec (Succ n') a) a + (\ (n':Nat) -> Stream (SpecM E stack (Vec n' a)) -> + mseq E stack (if0Nat Num n' (TCNum 0) TCInf) a) + (\ (s:Stream (SpecM E stack (Vec 0 a))) -> EmptyVec a) + (\ (n':Nat) -> \ (s:Stream (SpecM E stack (Vec (Succ n') a))) -> + MkStream (SpecM E stack a) (\ (i:Nat) -> + fmapS E stack (Vec (Succ n') a) a (\ (v:Vec (Succ n') a) -> at (Succ n') a v (modNat i (Succ n'))) - (streamGet (CompM (Vec (Succ n') a)) s (divNat i (Succ n'))) )) + (streamGet (SpecM E stack (Vec (Succ n') a)) s + (divNat i (Succ n'))) )) n)); -- No case for (TCInf, TCInf), shouldn't happen @@ -460,118 +544,140 @@ splitCryM m n a v = genCryM n a (\ (j : Nat) -> atCryM (mulNat m n) a v (addNat (mulNat i n) j))); -ecSplitM : (m n : Num) -> (a : sort 0) -> mseq (tcMul m n) a -> - mseq m (mseq n a); -ecSplitM = +ecSplitM : (E:EvType) -> (stack:FunStack) -> + (m n : Num) -> (a : sort 0) -> mseq E stack (tcMul m n) a -> + mseq E stack m (mseq E stack n a); +ecSplitM E stack = Num_rec - (\ (m:Num) -> (n:Num) -> (a:isort 0) -> mseq (tcMul m n) a -> - mseq m (mseq n a)) + (\ (m:Num) -> (n:Num) -> (a:isort 0) -> mseq E stack (tcMul m n) a -> + mseq E stack m (mseq E stack n a)) (\ (m:Nat) -> finNumRec - (\ (n:Num) -> (a:isort 0) -> mseq (tcMul (TCNum m) n) a -> - Vec m (mseq n a)) + (\ (n:Num) -> (a:isort 0) -> mseq E stack (tcMul (TCNum m) n) a -> + Vec m (mseq E stack n a)) -- Case for (TCNum m, TCNum n) (\ (n:Nat) -> \ (a:isort 0) -> splitCryM m n a)) -- No case for (TCNum m, TCInf), shouldn't happen (finNumRec - (\ (n:Num) -> (a:isort 0) -> mseq (tcMul TCInf n) a -> - Stream (CompM (mseq n a))) + (\ (n:Num) -> (a:isort 0) -> mseq E stack (tcMul TCInf n) a -> + Stream (SpecM E stack (mseq E stack n a))) -- Case for (TCInf, TCNum n) (\ (n:Nat) -> \ (a:isort 0) -> natCase (\ (n':Nat) -> - mseq (if0Nat Num n' (TCNum 0) TCInf) a -> - Stream (CompM (Vec n' a))) - (\ (xs : Vec 0 a) -> streamConst (CompM (Vec 0 a)) - (returnM (Vec 0 a) xs)) - (\ (n':Nat) (xs : Stream (CompM a)) -> - streamMap (Vec (Succ n') (CompM a)) (CompM (Vec (Succ n') a)) - (vecMapM (CompM a) a (Succ n') (id (CompM a))) - (streamSplit (CompM a) (Succ n') xs)) + mseq E stack (if0Nat Num n' (TCNum 0) TCInf) a -> + Stream (SpecM E stack (Vec n' a))) + (\ (xs : Vec 0 a) -> streamConst (SpecM E stack (Vec 0 a)) + (retS E stack (Vec 0 a) xs)) + (\ (n':Nat) (xs : Stream (SpecM E stack a)) -> + streamMap (Vec (Succ n') (SpecM E stack a)) + (SpecM E stack (Vec (Succ n') a)) + (vecMapM E stack (SpecM E stack a) a (Succ n') + (id (SpecM E stack a))) + (streamSplit (SpecM E stack a) (Succ n') xs)) n)); -- No case for (TCInf, TCInf), shouldn't happen -ecReverseM : (n : Num) -> isFinite n -> (a : sort 0) -> mseq n a -> mseq n a; -ecReverseM = - Num_rec_fin (\ (n:Num) -> (a : sort 0) -> mseq n a -> mseq n a) +ecReverseM : (E:EvType) -> (stack:FunStack) -> + (n : Num) -> isFinite n -> (a : sort 0) -> mseq E stack n a -> + mseq E stack n a; +ecReverseM E stack = + Num_rec_fin (\ (n:Num) -> (a : sort 0) -> mseq E stack n a -> mseq E stack n a) (\ (n:Nat) -> ecReverse (TCNum n)); -- FIXME primitive -ecTransposeM : (m n : Num) -> (a : sort 0) -> mseq m (mseq n a) -> - mseq n (mseq m a); - -ecAtM : (n : Num) -> (a : isort 0) -> (ix : sort 0) -> PIntegral ix -> - mseq n a -> ix -> CompM a; -ecAtM n_top a ix pix = +ecTransposeM : (E:EvType) -> (stack:FunStack) -> + (m n : Num) -> (a : sort 0) -> mseq E stack m (mseq E stack n a) -> + mseq E stack n (mseq E stack m a); + +ecAtM : (E:EvType) -> (stack:FunStack) -> + (n : Num) -> (a : isort 0) -> (ix : sort 0) -> PIntegral ix -> + mseq E stack n a -> ix -> SpecM E stack a; +ecAtM E stack n_top a ix pix = Num_rec - (\ (n:Num) -> mseq n a -> ix -> CompM a) + (\ (n:Num) -> mseq E stack n a -> ix -> SpecM E stack a) (\ (n:Nat) (v:Vec n a) -> - pix.posNegCases (CompM a) (atM n a v) - (\ (_:Nat) -> errorM a "ecAtM: invalid sequence index")) - (\ (s:Stream (CompM a)) -> - pix.posNegCases (CompM a) (streamGet (CompM a) s) - (\ (_:Nat) -> errorM a "ecAtM: invalid sequence index")) + pix.posNegCases (SpecM E stack a) (atM n a v) + (\ (_:Nat) -> + errorS E stack a "ecAtM: invalid sequence index")) + (\ (s:Stream (SpecM E stack a)) -> + pix.posNegCases (SpecM E stack a) (streamGet (SpecM E stack a) s) + (\ (_:Nat) -> + errorS E stack a "ecAtM: invalid sequence index")) n_top; -ecUpdateM : (n : Num) -> (a : isort 0) -> (ix : sort 0) -> PIntegral ix -> - mseq n a -> ix -> a -> CompM (mseq n a); -ecUpdateM n_top a ix pix = +ecUpdateM : (E:EvType) -> (stack:FunStack) -> + (n : Num) -> (a : isort 0) -> (ix : sort 0) -> PIntegral ix -> + mseq E stack n a -> ix -> a -> SpecM E stack (mseq E stack n a); +ecUpdateM E stack n_top a ix pix = Num_rec - (\ (n:Num) -> mseq n a -> ix -> a -> CompM (mseq n a)) + (\ (n:Num) -> mseq E stack n a -> ix -> a -> + SpecM E stack (mseq E stack n a)) (\ (n:Nat) (v:Vec n a) (i:ix) (x:a) -> - pix.posNegCases (CompM (Vec n a)) - (\ (i:Nat) -> updateM n a v i x) - (\ (_:Nat) -> errorM (Vec n a) - "ecUpdateM: invalid sequence index") i) - (\ (s:Stream (CompM a)) (i:ix) (x:a) -> - pix.posNegCases (CompM (Stream (CompM a))) - (\ (i:Nat) -> returnM (Stream (CompM a)) - (streamUpd (CompM a) s i (returnM a x))) - (\ (_:Nat) -> errorM (Stream (CompM a)) - "ecUpdateM: invalid sequence index") i) + pix.posNegCases (SpecM E stack (Vec n a)) + (\ (i:Nat) -> updateM E stack n a v i x) + (\ (_:Nat) -> errorS E stack (Vec n a) + "ecUpdateM: invalid sequence index") i) + (\ (s:Stream (SpecM E stack a)) (i:ix) (x:a) -> + pix.posNegCases (SpecM E stack (Stream (SpecM E stack a))) + (\ (i:Nat) -> + retS E stack (Stream (SpecM E stack a)) + (streamUpd (SpecM E stack a) s i + (retS E stack a x))) + (\ (_:Nat) -> errorS E stack (Stream (SpecM E stack a)) + "ecUpdateM: invalid sequence index") i) n_top; -- FIXME primitive -ecAtBackM : (n : Num) -> isFinite n -> (a ix : sort 0) -> PIntegral ix -> - mseq n a -> ix -> CompM a; +ecAtBackM : (E:EvType) -> (stack:FunStack) -> + (n : Num) -> isFinite n -> (a ix : sort 0) -> PIntegral ix -> + mseq E stack n a -> ix -> SpecM E stack a; -- FIXME primitive -ecFromToM : (first : Num) -> isFinite first -> (last : Num) -> isFinite last -> +ecFromToM : (E:EvType) -> (stack:FunStack) -> + (first : Num) -> isFinite first -> (last : Num) -> isFinite last -> (a : isort 0) -> PLiteral a -> - mseq (tcAdd (TCNum 1) (tcSub last first)) a; + mseq E stack (tcAdd (TCNum 1) (tcSub last first)) a; -- FIXME primitive -ecFromToLessThanM : (first : Num) -> isFinite first -> (bound : Num) -> +ecFromToLessThanM : (E:EvType) -> (stack:FunStack) -> + (first : Num) -> isFinite first -> (bound : Num) -> (a : isort 0) -> PLiteralLessThan a -> - mseq (tcSub bound first) a; + mseq E stack (tcSub bound first) a; -- FIXME primitive ecFromThenToM : + (E:EvType) -> (stack:FunStack) -> (first next last : Num) -> (a : sort 0) -> (len : Num) -> isFinite len -> - PLiteral a -> PLiteral a -> PLiteral a -> mseq len a; + PLiteral a -> PLiteral a -> PLiteral a -> mseq E stack len a; -ecInfFromM : (a : sort 0) -> PIntegral a -> a -> mseq TCInf a; -ecInfFromM a pa x = - MkStream (CompM a) +ecInfFromM : (E:EvType) -> (stack:FunStack) -> + (a : sort 0) -> PIntegral a -> a -> mseq E stack TCInf a; +ecInfFromM E stack a pa x = + MkStream (SpecM E stack a) (\ (i : Nat) -> - returnM a (pa.integralRing.add x (pa.integralRing.int (natToInt i)))); + retS E stack a (pa.integralRing.add + x (pa.integralRing.int (natToInt i)))); -ecInfFromThenM : (a : sort 0) -> PIntegral a -> a -> a -> mseq TCInf a; -ecInfFromThenM a pa x y = - MkStream (CompM a) +ecInfFromThenM : (E:EvType) -> (stack:FunStack) -> + (a : sort 0) -> PIntegral a -> a -> a -> mseq E stack TCInf a; +ecInfFromThenM E stack a pa x y = + MkStream (SpecM E stack a) (\ (i : Nat) -> - returnM a (pa.integralRing.add x - (pa.integralRing.mul (pa.integralRing.sub y x) - (pa.integralRing.int (natToInt i))))); - -ecErrorM : (a : sort 0) -> (len : Num) -> mseq len (Vec 8 Bool) -> CompM a; -ecErrorM a len msg = - errorM a "encountered call to the Cryptol 'error' function"; + retS E stack a (pa.integralRing.add x + (pa.integralRing.mul (pa.integralRing.sub y x) + (pa.integralRing.int (natToInt i))))); + +ecErrorM : (E:EvType) -> (stack:FunStack) -> + (a : sort 0) -> (len : Num) -> mseq E stack len (Vec 8 Bool) -> + SpecM E stack a; +ecErrorM E stack a len msg = + errorS E stack a "encountered call to the Cryptol 'error' function"; -------------------------------------------------------------------------------- diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs index 8c31fc68dc..3f3ff426ff 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs @@ -216,6 +216,10 @@ asTypedGlobalDef t = data SpecMParams tm = SpecMParams { specMEvType :: tm, specMStack :: tm } deriving (Generic, Show) +-- | Convert a 'SpecMParams' to a list of terms +paramsToTerms :: SpecMParams tm -> [tm] +paramsToTerms SpecMParams { specMEvType = ev, specMStack = stack } = [ev,stack] + -- | The implicit argument version of 'SpecMParams' type HasSpecMParams = (?specMParams :: SpecMParams OpenTerm) @@ -651,15 +655,22 @@ applyMonTermMulti :: HasCallStack => MonTerm -> [Either MonType ArgMonTerm] -> MonTerm applyMonTermMulti = foldl applyMonTerm --- | Build a 'MonTerm' from a global of a given argument type -mkGlobalArgMonTerm :: HasSpecMParams => MonType -> Ident -> ArgMonTerm -mkGlobalArgMonTerm tp ident = fromArgTerm tp (globalOpenTerm ident) - --- | Build a 'MonTerm' from a 'GlobalDef' of semi-pure type -mkSemiPureGlobalDefTerm :: HasSpecMParams => GlobalDef -> ArgMonTerm -mkSemiPureGlobalDefTerm glob = - fromSemiPureTerm (monadifyType [] $ - globalDefType glob) (globalDefOpenTerm glob) +-- | Build a 'MonTerm' from a global of a given argument type, applying it to +-- the current 'SpecMParams' if the 'Bool' flag is 'True' +mkGlobalArgMonTerm :: HasSpecMParams => MonType -> Ident -> Bool -> ArgMonTerm +mkGlobalArgMonTerm tp ident params_p = + fromArgTerm tp (if params_p + then applyGlobalOpenTerm ident (paramsToTerms ?specMParams) + else globalOpenTerm ident) + +-- | Build a 'MonTerm' from a 'GlobalDef' of semi-pure type, applying it to +-- the current 'SpecMParams' if the 'Bool' flag is 'True' +mkSemiPureGlobalDefTerm :: HasSpecMParams => GlobalDef -> Bool -> ArgMonTerm +mkSemiPureGlobalDefTerm glob params_p = + fromSemiPureTerm (monadifyType [] $ globalDefType glob) + (if params_p + then applyOpenTermMulti (globalDefOpenTerm glob) (paramsToTerms ?specMParams) + else globalDefOpenTerm glob) -- | Build a 'MonTerm' from a constructor with the given 'PrimName' mkCtorArgMonTerm :: HasSpecMParams => PrimName Term -> ArgMonTerm @@ -689,25 +700,30 @@ monMacro0 mtrm = MonMacro 0 (\_ _ -> return mtrm) -- | Make a 'MonMacro' that maps a named global to a global of semi-pure type. -- (See 'fromSemiPureTermFun'.) Because we can't get access to the type of the -- global until we apply the macro, we monadify its type at macro application --- time. -semiPureGlobalMacro :: Ident -> Ident -> MonMacro -semiPureGlobalMacro from to = +-- time. The 'Bool' flag indicates whether the current 'SpecMParams' should also +-- be passed as the first two arguments to the "to" global. +semiPureGlobalMacro :: Ident -> Ident -> Bool -> MonMacro +semiPureGlobalMacro from to params_p = MonMacro 0 $ \glob args -> if globalDefName glob == ModuleIdentifier from && args == [] then return $ ArgMonTerm $ - fromSemiPureTerm (monadifyType [] $ globalDefType glob) (globalOpenTerm to) + fromSemiPureTerm (monadifyType [] $ globalDefType glob) + (if params_p then applyGlobalOpenTerm to (paramsToTerms ?specMParams) + else globalOpenTerm to) else error ("Monadification macro for " ++ show from ++ " applied incorrectly") --- | Make a 'MonMacro' that maps a named global to a global of argument --- type. Because we can't get access to the type of the global until we apply --- the macro, we monadify its type at macro application time. -argGlobalMacro :: NameInfo -> Ident -> MonMacro -argGlobalMacro from to = +-- | Make a 'MonMacro' that maps a named global to a global of argument type. +-- Because we can't get access to the type of the global until we apply the +-- macro, we monadify its type at macro application time. The 'Bool' flag +-- indicates whether the current 'SpecMParams' should also be passed as the +-- first two arguments to the "to" global. +argGlobalMacro :: NameInfo -> Ident -> Bool -> MonMacro +argGlobalMacro from to params_p = MonMacro 0 $ \glob args -> if globalDefName glob == from && args == [] then return $ ArgMonTerm $ - mkGlobalArgMonTerm (monadifyType [] $ globalDefType glob) to + mkGlobalArgMonTerm (monadifyType [] $ globalDefType glob) to params_p else error ("Monadification macro for " ++ show from ++ " applied incorrectly") @@ -1095,7 +1111,7 @@ unsafeAssertMacro = MonMacro 1 $ \_ ts -> [(asDataType -> Just (num, []))] | primName num == "Cryptol.Num" -> return $ ArgMonTerm $ - mkGlobalArgMonTerm numFunType "CryptolM.numAssertEqM" + mkGlobalArgMonTerm numFunType "CryptolM.numAssertEqS" True _ -> fail "Monadification failed: unsafeAssert applied to non-Num type" @@ -1180,9 +1196,10 @@ assertingOrAssumingMacro doAsserting = MonMacro 3 $ \_ args -> -- | 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 --- @isFinite n@ -fin1Macro :: Ident -> Ident -> MonMacro -fin1Macro from to = +-- @isFinite n@. The 'Bool' flag indicates whether the current 'SpecMParams' +-- should be passed as the first two arguments to @to@. +fin1Macro :: Ident -> Ident -> Bool -> MonMacro +fin1Macro from to params_p = MonMacro 1 $ \glob args -> do if globalDefName glob == ModuleIdentifier from && length args == 1 then return () @@ -1195,7 +1212,10 @@ fin1Macro from to = -- Apply the type of @glob@ to n, and apply @to@ to n and fin_pf let glob_tp = monadifyType [] $ globalDefType glob let glob_tp_app = applyMonType glob_tp $ Left n_mtp - let to_app = applyOpenTermMulti (globalOpenTerm to) [n, toArgTerm fin_pf] + let to_app = + applyOpenTermMulti (globalOpenTerm to) + ((if params_p then (paramsToTerms ?specMParams ++) else id) + [n, toArgTerm fin_pf]) -- Finally, return @to n fin_pf@ as a MonTerm of monadified type @to_tp n@ return $ ArgMonTerm $ fromSemiPureTerm glob_tp_app to_app @@ -1233,25 +1253,28 @@ fixMacro = MonMacro 2 $ \_ args -> case args of type MacroMapping = (NameInfo, MonMacro) -- | Build a 'MacroMapping' for an identifier to a semi-pure named function -mmSemiPure :: Ident -> Ident -> MacroMapping -mmSemiPure from_id to_id = - (ModuleIdentifier from_id, semiPureGlobalMacro from_id to_id) +mmSemiPure :: Ident -> Ident -> Bool -> MacroMapping +mmSemiPure from_id to_id params_p = + (ModuleIdentifier from_id, semiPureGlobalMacro from_id to_id params_p) -- | Build a 'MacroMapping' for an identifier to a semi-pure named function -- whose first argument is a @Num@ that requires an @isFinite@ proof -mmSemiPureFin1 :: Ident -> Ident -> MacroMapping -mmSemiPureFin1 from_id to_id = - (ModuleIdentifier from_id, fin1Macro from_id to_id) +mmSemiPureFin1 :: Ident -> Ident -> Bool -> MacroMapping +mmSemiPureFin1 from_id to_id params_p = + (ModuleIdentifier from_id, fin1Macro from_id to_id params_p) -- | Build a 'MacroMapping' for an identifier to itself as a semi-pure function mmSelf :: Ident -> MacroMapping mmSelf self_id = - (ModuleIdentifier self_id, semiPureGlobalMacro self_id self_id) + (ModuleIdentifier self_id, semiPureGlobalMacro self_id self_id False) --- | Build a 'MacroMapping' from an identifier to a function of argument type -mmArg :: Ident -> Ident -> MacroMapping -mmArg from_id to_id = (ModuleIdentifier from_id, - argGlobalMacro (ModuleIdentifier from_id) to_id) +-- | Build a 'MacroMapping' from an identifier to a function of argument type, +-- where the 'Bool' flag indicates whether the current 'SpecMArgs' should be +-- passed as additional arguments to the "to" identifier +mmArg :: Ident -> Ident -> Bool -> MacroMapping +mmArg from_id to_id params_p = + (ModuleIdentifier from_id, + argGlobalMacro (ModuleIdentifier from_id) to_id params_p) -- | Build a 'MacroMapping' from an identifier and a custom 'MonMacro' mmCustom :: Ident -> MonMacro -> MacroMapping @@ -1277,42 +1300,42 @@ defaultMonTable = , mmCustom "Prelude.assuming" (assertingOrAssumingMacro False) -- Top-level sequence functions - , mmArg "Cryptol.seqMap" "CryptolM.seqMapM" - , mmSemiPure "Cryptol.seq_cong1" "CryptolM.mseq_cong1" - , mmArg "Cryptol.eListSel" "CryptolM.eListSelM" + , mmArg "Cryptol.seqMap" "CryptolM.seqMapM" True + , mmSemiPure "Cryptol.seq_cong1" "CryptolM.mseq_cong1" True + , mmArg "Cryptol.eListSel" "CryptolM.eListSelM" True -- List comprehensions - , mmArg "Cryptol.from" "CryptolM.fromM" + , mmArg "Cryptol.from" "CryptolM.fromM" True -- FIXME: continue here... -- PEq constraints - , mmSemiPureFin1 "Cryptol.PEqSeq" "CryptolM.PEqMSeq" - , mmSemiPureFin1 "Cryptol.PEqSeqBool" "CryptolM.PEqMSeqBool" + , mmSemiPureFin1 "Cryptol.PEqSeq" "CryptolM.PEqMSeq" True + , mmSemiPureFin1 "Cryptol.PEqSeqBool" "CryptolM.PEqMSeqBool" True -- PCmp constraints - , mmSemiPureFin1 "Cryptol.PCmpSeq" "CryptolM.PCmpMSeq" - , mmSemiPureFin1 "Cryptol.PCmpSeqBool" "CryptolM.PCmpMSeqBool" + , mmSemiPureFin1 "Cryptol.PCmpSeq" "CryptolM.PCmpMSeq" True + , mmSemiPureFin1 "Cryptol.PCmpSeqBool" "CryptolM.PCmpMSeqBool" True -- PSignedCmp constraints - , mmSemiPureFin1 "Cryptol.PSignedCmpSeq" "CryptolM.PSignedCmpMSeq" - , mmSemiPureFin1 "Cryptol.PSignedCmpSeqBool" "CryptolM.PSignedCmpMSeqBool" + , mmSemiPureFin1 "Cryptol.PSignedCmpSeq" "CryptolM.PSignedCmpMSeq" True + , mmSemiPureFin1 "Cryptol.PSignedCmpSeqBool" "CryptolM.PSignedCmpMSeqBool" True -- PZero constraints - , mmSemiPureFin1 "Cryptol.PZeroSeq" "CryptolM.PZeroMSeq" + , mmSemiPureFin1 "Cryptol.PZeroSeq" "CryptolM.PZeroMSeq" True -- PLogic constraints - , mmSemiPure "Cryptol.PLogicSeq" "CryptolM.PLogicMSeq" - , mmSemiPureFin1 "Cryptol.PLogicSeqBool" "CryptolM.PLogicMSeqBool" + , mmSemiPure "Cryptol.PLogicSeq" "CryptolM.PLogicMSeq" True + , mmSemiPureFin1 "Cryptol.PLogicSeqBool" "CryptolM.PLogicMSeqBool" True -- PRing constraints - , mmSemiPure "Cryptol.PRingSeq" "CryptolM.PRingMSeq" - , mmSemiPureFin1 "Cryptol.PRingSeqBool" "CryptolM.PRingMSeqBool" + , mmSemiPure "Cryptol.PRingSeq" "CryptolM.PRingMSeq" True + , mmSemiPureFin1 "Cryptol.PRingSeqBool" "CryptolM.PRingMSeqBool" True -- PIntegral constraints - , mmSemiPureFin1 "Cryptol.PIntegeralSeqBool" "CryptolM.PIntegeralMSeqBool" + , mmSemiPureFin1 "Cryptol.PIntegeralSeqBool" "CryptolM.PIntegeralMSeqBool" True -- PLiteral constraints - , mmSemiPureFin1 "Cryptol.PLiteralSeqBool" "CryptolM.PLiteralSeqBoolM" + , mmSemiPureFin1 "Cryptol.PLiteralSeqBool" "CryptolM.PLiteralSeqBoolM" True -- The Cryptol Literal primitives , mmSelf "Cryptol.ecNumber" @@ -1334,27 +1357,27 @@ defaultMonTable = , mmSelf "Cryptol.ecGtEq" -- Sequences - , mmSemiPure "Cryptol.ecShiftL" "CryptolM.ecShiftLM" - , mmSemiPure "Cryptol.ecShiftR" "CryptolM.ecShiftRM" - , mmSemiPure "Cryptol.ecSShiftR" "CryptolM.ecSShiftRM" - , mmSemiPureFin1 "Cryptol.ecRotL" "CryptolM.ecRotLM" - , mmSemiPureFin1 "Cryptol.ecRotR" "CryptolM.ecRotRM" - , mmSemiPureFin1 "Cryptol.ecCat" "CryptolM.ecCatM" - , mmSemiPure "Cryptol.ecTake" "CryptolM.ecTakeM" - , mmSemiPureFin1 "Cryptol.ecDrop" "CryptolM.ecDropM" - , mmSemiPure "Cryptol.ecJoin" "CryptolM.ecJoinM" - , mmSemiPure "Cryptol.ecSplit" "CryptolM.ecSplitM" - , mmSemiPureFin1 "Cryptol.ecReverse" "CryptolM.ecReverseM" - , mmSemiPure "Cryptol.ecTranspose" "CryptolM.ecTransposeM" - , mmArg "Cryptol.ecAt" "CryptolM.ecAtM" - , mmArg "Cryptol.ecUpdate" "CryptolM.ecUpdateM" + , mmSemiPure "Cryptol.ecShiftL" "CryptolM.ecShiftLM" True + , mmSemiPure "Cryptol.ecShiftR" "CryptolM.ecShiftRM" True + , mmSemiPure "Cryptol.ecSShiftR" "CryptolM.ecSShiftRM" True + , mmSemiPureFin1 "Cryptol.ecRotL" "CryptolM.ecRotLM" True + , mmSemiPureFin1 "Cryptol.ecRotR" "CryptolM.ecRotRM" True + , mmSemiPureFin1 "Cryptol.ecCat" "CryptolM.ecCatM" True + , mmSemiPure "Cryptol.ecTake" "CryptolM.ecTakeM" True + , mmSemiPureFin1 "Cryptol.ecDrop" "CryptolM.ecDropM" True + , mmSemiPure "Cryptol.ecJoin" "CryptolM.ecJoinM" True + , mmSemiPure "Cryptol.ecSplit" "CryptolM.ecSplitM" True + , mmSemiPureFin1 "Cryptol.ecReverse" "CryptolM.ecReverseM" True + , mmSemiPure "Cryptol.ecTranspose" "CryptolM.ecTransposeM" True + , mmArg "Cryptol.ecAt" "CryptolM.ecAtM" True + , mmArg "Cryptol.ecUpdate" "CryptolM.ecUpdateM" True -- , mmArgFin1 "Cryptol.ecAtBack" "CryptolM.ecAtBackM" -- , mmSemiPureFin2 "Cryptol.ecFromTo" "CryptolM.ecFromToM" - , mmSemiPureFin1 "Cryptol.ecFromToLessThan" "CryptolM.ecFromToLessThanM" + , mmSemiPureFin1 "Cryptol.ecFromToLessThan" "CryptolM.ecFromToLessThanM" True -- , mmSemiPureNthFin 5 "Cryptol.ecFromThenTo" "CryptolM.ecFromThenToM" - , mmSemiPure "Cryptol.ecInfFrom" "CryptolM.ecInfFromM" - , mmSemiPure "Cryptol.ecInfFromThen" "CryptolM.ecInfFromThenM" - , mmArg "Cryptol.ecError" "CryptolM.ecErrorM" + , mmSemiPure "Cryptol.ecInfFrom" "CryptolM.ecInfFromM" True + , mmSemiPure "Cryptol.ecInfFromThen" "CryptolM.ecInfFromThenM" True + , mmArg "Cryptol.ecError" "CryptolM.ecErrorM" True ] diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index 46580a76c8..fcdaa7924c 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -2310,7 +2310,7 @@ setMonadification sc cry_str saw_str = let (tp_to_check, macro) = case Monadify.monEnvLookup (ModuleIdentifier saw_ident) (rwMonadify rw) of Just existing_macro -> (cry_saw_tp, existing_macro) - Nothing -> (cry_mon_tp, Monadify.argGlobalMacro cry_nmi saw_ident) + Nothing -> (cry_mon_tp, Monadify.argGlobalMacro cry_nmi saw_ident False) liftIO $ scCheckSubtype sc Nothing (TC.TypedTerm saw_trm saw_tp) tp_to_check -- Step 4: Add the generated macro From 19296d2ee0c4dc2b8d88e5704a42ec7bb0881e9b Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Mon, 12 Dec 2022 10:43:53 -0800 Subject: [PATCH 15/27] fixed some small bugs in CryptolM.sawcore --- cryptol-saw-core/saw/CryptolM.sawcore | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/cryptol-saw-core/saw/CryptolM.sawcore b/cryptol-saw-core/saw/CryptolM.sawcore index f4568ada74..2e2ac7846f 100644 --- a/cryptol-saw-core/saw/CryptolM.sawcore +++ b/cryptol-saw-core/saw/CryptolM.sawcore @@ -35,7 +35,7 @@ checkFinite = -- Assert that a Num is finite, or fail assertFiniteS : (E:EvType) -> (stack:FunStack) -> (n:Num) -> SpecM E stack (isFinite n); -assertFiniteM E stack n = +assertFiniteS E stack n = maybe (isFinite n) (SpecM E stack (isFinite n)) (errorS E stack (isFinite n) "assertFiniteM: Num not finite") (retS E stack (isFinite n)) @@ -56,7 +56,7 @@ Num_rec_fin p f = -- The type of monadified sequences, which are just vectors for finite length -- but are sequences of computations for streams mseq : (E:EvType) -> (stack:FunStack) -> Num -> sort 0 -> sort 0; -mseq num E stack a = +mseq E stack num a = Num_rec (\ (_:Num) -> sort 0) (\ (n:Nat) -> Vec n a) (Stream (SpecM E stack a)) num; @@ -240,7 +240,7 @@ eListSelM : (E:EvType) -> (stack:FunStack) -> SpecM E stack a; eListSelM E stack a = Num_rec (\ (n:Num) -> mseq E stack n a -> Nat -> SpecM E stack a) - (\ (n:Nat) -> atM n a) + (\ (n:Nat) -> atM E stack n a) (eListSel (SpecM E stack a) TCInf); @@ -301,9 +301,9 @@ PCmpMSeq E stack = (\ (n:Nat) -> PCmpVec n); PCmpMSeqBool : (E:EvType) -> (stack:FunStack) -> - (n : Num) -> isFinite n -> PCmp (seq n Bool); + (n : Num) -> isFinite n -> PCmp (mseq E stack n Bool); PCmpMSeqBool E stack = - Num_rec_fin (\ (n:Num) -> PCmp (seq n Bool)) PCmpWord; + Num_rec_fin (\ (n:Num) -> PCmp (mseq E stack n Bool)) PCmpWord; -- PSignedCmp PSignedCmpMSeq : (E:EvType) -> (stack:FunStack) -> @@ -317,7 +317,7 @@ PSignedCmpMSeq E stack = PSignedCmpMSeqBool : (E:EvType) -> (stack:FunStack) -> (n : Num) -> isFinite n -> PSignedCmp (mseq E stack n Bool); PSignedCmpMSeqBool E stack = - Num_rec_fin (\ (n:Num) -> PSignedCmp (seq n Bool)) PSignedCmpWord; + Num_rec_fin (\ (n:Num) -> PSignedCmp (mseq E stack n Bool)) PSignedCmpWord; -- PZero @@ -427,7 +427,7 @@ ecShiftLM E stack = ecShiftRM : (E:EvType) -> (stack:FunStack) -> (m : Num) -> (ix a : sort 0) -> PIntegral ix -> PZero a -> mseq E stack m a -> ix -> mseq E stack m a; -ecShiftRM E satck = +ecShiftRM E stack = Num_rec (\ (m:Num) -> (ix a : sort 0) -> PIntegral ix -> PZero a -> mseq E stack m a -> ix -> mseq E stack m a) (\ (m:Nat) -> ecShiftR (TCNum m)) @@ -598,7 +598,7 @@ ecAtM E stack n_top a ix pix = Num_rec (\ (n:Num) -> mseq E stack n a -> ix -> SpecM E stack a) (\ (n:Nat) (v:Vec n a) -> - pix.posNegCases (SpecM E stack a) (atM n a v) + pix.posNegCases (SpecM E stack a) (atM E stack n a v) (\ (_:Nat) -> errorS E stack a "ecAtM: invalid sequence index")) (\ (s:Stream (SpecM E stack a)) -> From c58bf458cc3086b15c8c4f35f4331ae2ed3a82e3 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Mon, 12 Dec 2022 14:41:30 -0800 Subject: [PATCH 16/27] added list1OpenTerm operator --- saw-core/src/Verifier/SAW/OpenTerm.hs | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/saw-core/src/Verifier/SAW/OpenTerm.hs b/saw-core/src/Verifier/SAW/OpenTerm.hs index 8839cc015d..08cfb71ac4 100644 --- a/saw-core/src/Verifier/SAW/OpenTerm.hs +++ b/saw-core/src/Verifier/SAW/OpenTerm.hs @@ -36,7 +36,7 @@ module Verifier.SAW.OpenTerm ( applyOpenTerm, applyOpenTermMulti, applyGlobalOpenTerm, applyPiOpenTerm, piArgOpenTerm, lambdaOpenTerm, lambdaOpenTermMulti, piOpenTerm, piOpenTermMulti, - arrowOpenTerm, letOpenTerm, sawLetOpenTerm, + arrowOpenTerm, letOpenTerm, sawLetOpenTerm, list1OpenTerm, -- * Monadic operations for building terms with binders OpenTermM(..), completeOpenTermM, dedupOpenTermM, lambdaOpenTermM, piOpenTermM, @@ -412,6 +412,13 @@ sawLetOpenTerm x tp tp_ret rhs body_f = applyOpenTermMulti (globalOpenTerm "Prelude.sawLet") [tp, tp_ret, rhs, lambdaOpenTerm x tp body_f] +-- | Build an 'OpenTerm' of type @List1 tp@ from 'OpenTerm's of type @tp@ +list1OpenTerm :: OpenTerm -> [OpenTerm] -> OpenTerm +list1OpenTerm tp xs = + foldr (\hd tl -> ctorOpenTerm "Prelude.Cons1" [tp, hd, tl]) + (ctorOpenTerm "Prelude.Nil1" [tp]) + xs + -- | The monad for building 'OpenTerm's if you want to add in 'IO' actions. This -- is just the type-checking monad, but we give it a new name to keep this -- module self-contained. From 98927cfe741750d50e0c871319435e44fa65fd5a Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Mon, 12 Dec 2022 16:48:46 -0800 Subject: [PATCH 17/27] fixed fixMacro to push the new frame onto the function stack when recursing inside the function bodies --- .../src/Verifier/SAW/Cryptol/Monadify.hs | 69 +++++++++++++------ 1 file changed, 47 insertions(+), 22 deletions(-) diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs index 3f3ff426ff..a73b81f712 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs @@ -223,6 +223,33 @@ paramsToTerms SpecMParams { specMEvType = ev, specMStack = stack } = [ev,stack] -- | The implicit argument version of 'SpecMParams' type HasSpecMParams = (?specMParams :: SpecMParams OpenTerm) +-- | Build a @LetRecType@ for a nested pi type +lrtFromMonType :: HasSpecMParams => MonType -> OpenTerm +lrtFromMonType (MTyForall x k body_f) = + ctorOpenTerm "Prelude.LRT_Fun" + [monKindOpenTerm k, + lambdaOpenTerm x (monKindOpenTerm k) (\tp -> lrtFromMonType $ + body_f $ MTyBase k tp)] +lrtFromMonType (MTyArrow mtp1 mtp2) = + ctorOpenTerm "Prelude.LRT_Fun" + [toArgType mtp1, + lambdaOpenTerm "_" (toArgType mtp1) (\_ -> lrtFromMonType mtp2)] +lrtFromMonType mtp = + ctorOpenTerm "Prelude.LRT_Ret" [toArgType mtp] + +-- | Push a frame of recursive functions with the given 'MonType's onto a +-- @FunStack@ +-- +-- FIXME HERE: This will give the incorrect type if any of the 'MonType's are +-- higher-order, meaning they themselves take in or return types containing +-- @SpecM@. In order to fix this, we will need a more general @LetRecType@. +pushSpecMFrame :: HasSpecMParams => [MonType] -> OpenTerm -> OpenTerm +pushSpecMFrame tps stack = + let frame = + list1OpenTerm (dataTypeOpenTerm "Prelude.LetRecType" []) $ + map lrtFromMonType tps in + applyGlobalOpenTerm "Prelude.pushFunStack" [frame, stack] + -- | The empty function stack emptyStackOpenTerm :: OpenTerm emptyStackOpenTerm = globalOpenTerm "Prelude.emptyFunStack" @@ -343,7 +370,8 @@ toArgType (MTyForall x k body) = toArgType (MTyArrow t1 t2) = arrowOpenTerm "_" (toArgType t1) (toCompType t2) toArgType (MTySeq n t) = - applyOpenTermMulti (globalOpenTerm "CryptolM.mseq") [n, toArgType t] + applyOpenTermMulti (globalOpenTerm "CryptolM.mseq") + [specMEvType ?specMParams, specMStack ?specMParams, n, toArgType t] toArgType (MTyPair mtp1 mtp2) = pairTypeOpenTerm (toArgType mtp1) (toArgType mtp2) toArgType (MTyRecord tps) = @@ -805,6 +833,7 @@ newtype MonadifyM a = deriving (Functor, Applicative, Monad, MonadReader MonadifyROState, MonadState MonadifyMemoTable) +-- | Run a 'MonadifyM' computation with the current 'SpecMParams' usingSpecMParams :: (HasSpecMParams => MonadifyM a) -> MonadifyM a usingSpecMParams m = do st <- ask @@ -813,6 +842,12 @@ usingSpecMParams m = let ?specMParams = (SpecMParams { specMEvType = ev, specMStack = stack }) in m +-- | Push a frame of recursive functions onto the current 'SpecMParams' +pushingSpecMParamsM :: [MonType] -> MonadifyM a -> MonadifyM a +pushingSpecMParamsM tps m = + usingSpecMParams $ + local (\rost -> rost { monStStack = pushSpecMFrame tps (monStStack rost) }) m + instance Fail.MonadFail MonadifyM where fail str = usingSpecMParams $ @@ -901,14 +936,15 @@ argifyMonTerm (CompMonTerm mtp trm) = [specMEvType ?specMParams, specMStack ?specMParams, tp, top_ret_tp, trm, lambdaOpenTerm "x" tp (toCompTerm . k . fromArgTerm mtp)] --- | Build a proof of @isFinite n@ by calling @assertFiniteM@ and binding the +-- | Build a proof of @isFinite n@ by calling @assertFiniteS@ and binding the -- result to an 'ArgMonTerm' -assertIsFinite :: MonType -> MonadifyM ArgMonTerm +assertIsFinite :: HasSpecMParams => MonType -> MonadifyM ArgMonTerm assertIsFinite (MTyNum n) = argifyMonTerm (CompMonTerm (mkMonType0 (applyOpenTerm (globalOpenTerm "CryptolM.isFinite") n)) - (applyOpenTerm (globalOpenTerm "CryptolM.assertFiniteM") n)) + (applyGlobalOpenTerm "CryptolM.assertFiniteS" + [specMEvType ?specMParams, specMStack ?specMParams, n])) assertIsFinite _ = fail ("assertIsFinite applied to non-Num argument") @@ -996,7 +1032,8 @@ monadifyTerm' (Just mtp@(MTySeq n mtp_elem)) (asFTermF -> do trms' <- traverse (monadifyArgTerm $ Just mtp_elem) trms return $ fromArgTerm mtp $ applyOpenTermMulti (globalOpenTerm "CryptolM.seqToMseq") - [n, toArgType mtp_elem, + [specMEvType ?specMParams, specMStack ?specMParams, + n, toArgType mtp_elem, flatOpenTerm $ ArrayValue (toArgType mtp_elem) trms'] monadifyTerm' _ (asPairSelector -> Just (trm, True)) = do mtrm <- monadifyArg Nothing trm @@ -1219,31 +1256,19 @@ fin1Macro from to params_p = -- Finally, return @to n fin_pf@ as a MonTerm of monadified type @to_tp n@ return $ ArgMonTerm $ fromSemiPureTerm glob_tp_app to_app --- | Helper function: build a @LetRecType@ for a nested pi type -lrtFromMonType :: HasSpecMParams => MonType -> OpenTerm -lrtFromMonType (MTyForall x k body_f) = - ctorOpenTerm "Prelude.LRT_Fun" - [monKindOpenTerm k, - lambdaOpenTerm x (monKindOpenTerm k) (\tp -> lrtFromMonType $ - body_f $ MTyBase k tp)] -lrtFromMonType (MTyArrow mtp1 mtp2) = - ctorOpenTerm "Prelude.LRT_Fun" - [toArgType mtp1, - lambdaOpenTerm "_" (toArgType mtp1) (\_ -> lrtFromMonType mtp2)] -lrtFromMonType mtp = - ctorOpenTerm "Prelude.LRT_Ret" [toArgType mtp] - -- | The macro for fix -- -- FIXME: does not yet handle mutual recursion fixMacro :: MonMacro fixMacro = MonMacro 2 $ \_ args -> case args of [tp@(asPi -> Just _), f] -> - do mtp <- monadifyTypeM tp - amtrm_f <- monadifyArg (Just $ MTyArrow mtp mtp) f + let orig_params = ?specMParams in + monadifyTypeM tp >>= \mtp -> + pushingSpecMParamsM [mtp] $ + do amtrm_f <- monadifyArg (Just $ MTyArrow mtp mtp) f return $ fromCompTerm mtp $ applyOpenTermMulti (globalOpenTerm "Prelude.multiArgFixS") - [specMEvType ?specMParams, specMStack ?specMParams, + [specMEvType orig_params, specMStack orig_params, lrtFromMonType mtp, toCompTerm amtrm_f] [(asRecordType -> Just _), _] -> fail "Monadification failed: cannot yet handle mutual recursion" From 8b284e363839207d102499956665754a9491890b Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Mon, 12 Dec 2022 18:14:37 -0800 Subject: [PATCH 18/27] fixed the fixMacro to wrk, I think... --- .../src/Verifier/SAW/Cryptol/Monadify.hs | 81 +++++++++++++------ 1 file changed, 58 insertions(+), 23 deletions(-) diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs index a73b81f712..d9a77152e9 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs @@ -604,6 +604,28 @@ fromCompTerm :: HasSpecMParams => MonType -> OpenTerm -> MonTerm fromCompTerm mtp t | isBaseType mtp = CompMonTerm mtp t fromCompTerm mtp t = ArgMonTerm $ fromArgTerm mtp t +-- | Take a function of type @A1 -> ... -> An -> SpecM E emptyFunStack B@ and +-- lift the stack of the output type to an arbitrary @stack@ parameter using +-- @liftStackS@ +class LiftCompStack a where + liftCompStack :: HasSpecMParams => a -> a + +instance LiftCompStack ArgMonTerm where + liftCompStack t@(BaseMonTerm _ _) = + -- A pure term need not be lifted, because it is not computational + t + liftCompStack (FunMonTerm nm tp_in tp_out body) = + FunMonTerm nm tp_in tp_out $ \x -> liftCompStack $ body x + liftCompStack (ForallMonTerm nm k body) = + ForallMonTerm nm k $ \x -> liftCompStack $ body x + +instance LiftCompStack MonTerm where + liftCompStack (ArgMonTerm amtrm) = ArgMonTerm $ liftCompStack amtrm + liftCompStack (CompMonTerm mtp trm) = + CompMonTerm mtp $ + applyGlobalOpenTerm "Prelude.liftStackS" + [specMEvType ?specMParams, specMStack ?specMParams, toArgType mtp, trm] + -- | Test if a monadification type @tp@ is pure, meaning @MT(tp)=tp@ monTypeIsPure :: MonType -> Bool monTypeIsPure (MTyForall _ _ _) = False -- NOTE: this could potentially be true @@ -684,9 +706,11 @@ applyMonTermMulti :: HasCallStack => MonTerm -> [Either MonType ArgMonTerm] -> applyMonTermMulti = foldl applyMonTerm -- | Build a 'MonTerm' from a global of a given argument type, applying it to --- the current 'SpecMParams' if the 'Bool' flag is 'True' +-- the current 'SpecMParams' if the 'Bool' flag is 'True' and lifting it using +-- @liftStackS@ if it is 'False' mkGlobalArgMonTerm :: HasSpecMParams => MonType -> Ident -> Bool -> ArgMonTerm mkGlobalArgMonTerm tp ident params_p = + (if params_p then id else liftCompStack) $ fromArgTerm tp (if params_p then applyGlobalOpenTerm ident (paramsToTerms ?specMParams) else globalOpenTerm ident) @@ -719,7 +743,7 @@ mkCtorArgMonTerm pn = -- before deciding how to monadify itself data MonMacro = MonMacro { macroNumArgs :: Int, - macroApply :: HasSpecMParams => GlobalDef -> [Term] -> MonadifyM MonTerm } + macroApply :: GlobalDef -> [Term] -> MonadifyM MonTerm } -- | Make a simple 'MonMacro' that inspects 0 arguments and just returns a term monMacro0 :: MonTerm -> MonMacro @@ -732,7 +756,7 @@ monMacro0 mtrm = MonMacro 0 (\_ _ -> return mtrm) -- be passed as the first two arguments to the "to" global. semiPureGlobalMacro :: Ident -> Ident -> Bool -> MonMacro semiPureGlobalMacro from to params_p = - MonMacro 0 $ \glob args -> + MonMacro 0 $ \glob args -> usingSpecMParams $ if globalDefName glob == ModuleIdentifier from && args == [] then return $ ArgMonTerm $ fromSemiPureTerm (monadifyType [] $ globalDefType glob) @@ -744,11 +768,13 @@ semiPureGlobalMacro from to params_p = -- | Make a 'MonMacro' that maps a named global to a global of argument type. -- Because we can't get access to the type of the global until we apply the -- macro, we monadify its type at macro application time. The 'Bool' flag --- indicates whether the current 'SpecMParams' should also be passed as the --- first two arguments to the "to" global. +-- indicates whether the "to" global is polymorphic in the event type and +-- function stack; if so, the current 'SpecMParams' are passed as its first two +-- arguments, and otherwise the returned computation is lifted with +-- @liftStackS@. argGlobalMacro :: NameInfo -> Ident -> Bool -> MonMacro argGlobalMacro from to params_p = - MonMacro 0 $ \glob args -> + MonMacro 0 $ \glob args -> usingSpecMParams $ if globalDefName glob == from && args == [] then return $ ArgMonTerm $ mkGlobalArgMonTerm (monadifyType [] $ globalDefType glob) to params_p @@ -833,14 +859,19 @@ newtype MonadifyM a = deriving (Functor, Applicative, Monad, MonadReader MonadifyROState, MonadState MonadifyMemoTable) --- | Run a 'MonadifyM' computation with the current 'SpecMParams' -usingSpecMParams :: (HasSpecMParams => MonadifyM a) -> MonadifyM a -usingSpecMParams m = +-- | Get the current 'SpecMParams' in a 'MonadifyM' computation +askSpecMParams :: MonadifyM (SpecMParams OpenTerm) +askSpecMParams = do st <- ask let ev = monEnvEvType $ monStEnv st let stack = monStStack st - let ?specMParams = (SpecMParams { specMEvType = ev, - specMStack = stack }) in m + return (SpecMParams { specMEvType = ev, specMStack = stack }) + +-- | Run a 'MonadifyM' computation with the current 'SpecMParams' +usingSpecMParams :: (HasSpecMParams => MonadifyM a) -> MonadifyM a +usingSpecMParams m = + do params <- askSpecMParams + let ?specMParams = params in m -- | Push a frame of recursive functions onto the current 'SpecMParams' pushingSpecMParamsM :: [MonType] -> MonadifyM a -> MonadifyM a @@ -1137,6 +1168,7 @@ monadifyEtaExpand env ctx stack top_mtp mtp t args = -- compared and dispatches to the proper comparison function unsafeAssertMacro :: MonMacro unsafeAssertMacro = MonMacro 1 $ \_ ts -> + usingSpecMParams $ let numFunType = MTyForall "n" (MKType $ mkSort 0) $ \n -> MTyForall "m" (MKType $ mkSort 0) $ \m -> @@ -1155,7 +1187,7 @@ unsafeAssertMacro = MonMacro 1 $ \_ ts -> -- | The macro for if-then-else, which contains any binds in a branch to that -- branch iteMacro :: MonMacro -iteMacro = MonMacro 4 $ \_ args -> +iteMacro = MonMacro 4 $ \_ args -> usingSpecMParams $ do let (tp, cond, branch1, branch2) = case args of [t1, t2, t3, t4] -> (t1, t2, t3, t4) @@ -1179,6 +1211,7 @@ iteMacro = MonMacro 4 $ \_ args -> -- application @either a b c@ to @either a b (CompM c)@ eitherMacro :: MonMacro eitherMacro = MonMacro 3 $ \_ args -> + usingSpecMParams $ do let (tp_a, tp_b, tp_c) = case args of [t1, t2, t3] -> (t1, t2, t3) @@ -1199,7 +1232,7 @@ eitherMacro = MonMacro 3 $ \_ args -> -- to @invariantHint (CompM a) cond m@ and which contains any binds in the body -- to the body invariantHintMacro :: MonMacro -invariantHintMacro = MonMacro 3 $ \_ args -> +invariantHintMacro = MonMacro 3 $ \_ args -> usingSpecMParams $ do let (tp, cond, m) = case args of [t1, t2, t3] -> (t1, t2, t3) @@ -1217,6 +1250,7 @@ invariantHintMacro = MonMacro 3 $ \_ args -> -- body to the body assertingOrAssumingMacro :: Bool -> MonMacro assertingOrAssumingMacro doAsserting = MonMacro 3 $ \_ args -> + usingSpecMParams $ do let (tp, cond, m) = case args of [t1, t2, t3] -> (t1, t2, t3) @@ -1224,11 +1258,12 @@ assertingOrAssumingMacro doAsserting = MonMacro 3 $ \_ args -> atrm_cond <- monadifyArg (Just boolMonType) cond mtp <- monadifyTypeM tp mtrm <- resetMonadifyM (toArgType mtp) $ monadifyTerm (Just mtp) m + params <- askSpecMParams let ident = if doAsserting then "Prelude.assertingS" else "Prelude.assumingS" return $ fromCompTerm mtp $ applyOpenTermMulti (globalOpenTerm ident) - [specMEvType ?specMParams, specMStack ?specMParams, + [specMEvType params, specMStack params, toArgType mtp, toArgTerm atrm_cond, toCompTerm mtrm] -- | Make a 'MonMacro' that maps a named global whose first argument is @n:Num@ @@ -1237,7 +1272,7 @@ assertingOrAssumingMacro doAsserting = MonMacro 3 $ \_ args -> -- should be passed as the first two arguments to @to@. fin1Macro :: Ident -> Ident -> Bool -> MonMacro fin1Macro from to params_p = - MonMacro 1 $ \glob args -> + MonMacro 1 $ \glob args -> usingSpecMParams $ do if globalDefName glob == ModuleIdentifier from && length args == 1 then return () else error ("Monadification macro for " ++ show from ++ @@ -1262,14 +1297,14 @@ fin1Macro from to params_p = fixMacro :: MonMacro fixMacro = MonMacro 2 $ \_ args -> case args of [tp@(asPi -> Just _), f] -> - let orig_params = ?specMParams in - monadifyTypeM tp >>= \mtp -> - pushingSpecMParamsM [mtp] $ - do amtrm_f <- monadifyArg (Just $ MTyArrow mtp mtp) f - return $ fromCompTerm mtp $ - applyOpenTermMulti (globalOpenTerm "Prelude.multiArgFixS") - [specMEvType orig_params, specMStack orig_params, - lrtFromMonType mtp, toCompTerm amtrm_f] + do orig_params <- askSpecMParams + mtp <- monadifyTypeM tp + pushingSpecMParamsM [mtp] $ usingSpecMParams $ do + amtrm_f <- monadifyArg (Just $ MTyArrow mtp mtp) f + return $ fromCompTerm mtp $ + applyOpenTermMulti (globalOpenTerm "Prelude.multiArgFixS") + [specMEvType orig_params, specMStack orig_params, + lrtFromMonType mtp, toCompTerm amtrm_f] [(asRecordType -> Just _), _] -> fail "Monadification failed: cannot yet handle mutual recursion" _ -> error "fixMacro: malformed arguments!" From 87bff2e1bd584d6d3f08fa2b74ea4bbd982adfdd Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Tue, 13 Dec 2022 06:29:02 -0800 Subject: [PATCH 19/27] changed mrFreshVar to abstract over the current uvar context; added support to normComp for normalizing multiArgFixS --- src/SAWScript/Prover/MRSolver/Monad.hs | 12 ++++++++---- src/SAWScript/Prover/MRSolver/Solver.hs | 26 +++++++++++++++++++++++-- 2 files changed, 32 insertions(+), 6 deletions(-) diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs index 63d599e4c9..7ead557815 100644 --- a/src/SAWScript/Prover/MRSolver/Monad.hs +++ b/src/SAWScript/Prover/MRSolver/Monad.hs @@ -726,7 +726,7 @@ mrVarTerm (MRVar ec) = -- 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 +mrDummyProof tp = mrFreshVar "pf" tp >>= mrVarTerm -- | Get the 'VarInfo' associated with a 'MRVar' mrVarInfo :: MRVar -> MRM (Maybe MRVarInfo) @@ -807,8 +807,13 @@ mrCallsFun f = memoFixTermFun $ \recurse t -> case t of -- | Make a fresh 'MRVar' of a given type, which must be closed, i.e., have no -- free uvars +mrFreshVarCl :: LocalName -> Term -> MRM MRVar +mrFreshVarCl nm tp = MRVar <$> liftSC2 scFreshEC nm tp + +-- | Make a fresh 'MRVar' of type @(u1:tp1) -> ... (un:tpn) -> tp@, where the +-- @ui@ are all the current uvars mrFreshVar :: LocalName -> Term -> MRM MRVar -mrFreshVar nm tp = MRVar <$> liftSC2 scFreshEC nm tp +mrFreshVar nm tp = piUVarsM tp >>= mrFreshVarCl nm -- | Set the info associated with an 'MRVar', assuming it has not been set mrSetVarInfo :: MRVar -> MRVarInfo -> MRM () @@ -825,8 +830,7 @@ mrSetVarInfo var info = -- the current uvars and returning the new evar applied to all current uvars mrFreshEVar :: LocalName -> Type -> MRM Term mrFreshEVar nm (Type tp) = - do tp' <- piUVarsM tp - var <- mrFreshVar nm tp' + do var <- mrFreshVar nm tp mrSetVarInfo var (EVarInfo Nothing) mrVarTerm var diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs index bb2f3c1127..31e79c24b2 100644 --- a/src/SAWScript/Prover/MRSolver/Solver.hs +++ b/src/SAWScript/Prover/MRSolver/Solver.hs @@ -229,7 +229,7 @@ mrFreshCallVars ev stack frame defs_tm = (asList1 -> Just lrts) -> return lrts _ -> throwMRFailure (MalformedLetRecTypes frame) fun_tps <- forM lrts $ \lrt -> - piUVarsM =<< liftSC2 scGlobalApply "Prelude.LRTType" [ev, new_stack, lrt] + liftSC2 scGlobalApply "Prelude.LRTType" [ev, new_stack, lrt] fun_vars <- mapM (mrFreshVar "F") fun_tps -- Next, match on the tuple of recursive function definitions and convert @@ -323,6 +323,27 @@ normComp (CompTerm t) = all_args <- (++ args) <$> getAllUVarTerms FunBind var all_args <$> mkCompFunReturn <$> mrFunOutType var all_args + (isGlobalDef "Prelude.multiArgFixS" -> Just (), ev:stack:lrt:body:args) -> + do + -- Bind a fresh function var for the new recursive function + body_tp <- mrTypeOf body + fun_tp <- case asPi body_tp of + Just (_, tp_in, _) -> return tp_in + Nothing -> throwMRFailure (MalformedDefs body) + fun_var <- mrFreshVar "F" fun_tp + fun_tm <- mrVarTerm fun_var + + -- Set the new function var to have body applied to it + body_app <- mrApply body fun_tm >>= lambdaUVarsM + mrSetVarInfo fun_var (CallVarInfo body_app) + + -- Return the function variable applied to args as a normalized + -- computation, noting that it must be applied to all of the uvars as + -- well as the args + let var = CallSName fun_var + all_args <- (++ args) <$> getAllUVarTerms + FunBind var all_args <$> mkCompFunReturn <$> mrFunOutType var all_args + -- Convert `vecMapM (bvToNat ...)` into `bvVecMapInvarM`, with the -- invariant being the current set of assumptions (asGlobalDef -> Just "CryptolM.vecMapM", [a, b, (asBvToNat -> Just (w, n)), @@ -393,7 +414,8 @@ normComp (CompTerm t) = -- Always unfold: sawLet, multiArgFixM, invariantHint, Num_rec (f@(asGlobalDef -> Just ident), args) | ident `elem` ["Prelude.sawLet", "Prelude.invariantHint", - "Cryptol.Num_rec"] + "Cryptol.Num_rec", "Prelude.multiArgFixS", + "Prelude.lrtLambda"] , Just (_, Just body) <- asConstant f -> mrApplyAll body args >>= normCompTerm From 9b168f33ad895ab66ee481922ace84386b5afa37 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Wed, 14 Dec 2022 07:17:13 -0800 Subject: [PATCH 20/27] updated the normalizer in SMT.hs to work with SpecM types --- src/SAWScript/Prover/MRSolver/SMT.hs | 35 +++++++++++++++++++++------- 1 file changed, 27 insertions(+), 8 deletions(-) diff --git a/src/SAWScript/Prover/MRSolver/SMT.hs b/src/SAWScript/Prover/MRSolver/SMT.hs index c9f8b70d83..f5f8be763f 100644 --- a/src/SAWScript/Prover/MRSolver/SMT.hs +++ b/src/SAWScript/Prover/MRSolver/SMT.hs @@ -247,7 +247,18 @@ readBackValueNoConfig err_str sc tv v = let cfg = error $ "FIXME: need the simulator config in " ++ err_str in readBackValue sc cfg tv v +-- | A primitive that returns a global as a term +primGlobal :: SharedContext -> Ident -> TmPrim +primGlobal sc glob = + Prim $ do tp <- scTypeOfGlobal sc glob + tp_tp <- scTypeOf sc tp >>= scWhnf sc + s <- case asSort tp_tp of + Just s -> return s + Nothing -> fail "primGlobal: expected sort" + VExtra <$> VExtraTerm (VTyTerm s tp) <$> scGlobalDef sc glob + -- | Implementations of primitives for normalizing Mr Solver terms +-- FIXME: eventually we need to add the current event type to this list smtNormPrims :: SharedContext -> Map Ident TmPrim smtNormPrims sc = Map.fromList [ -- Don't unfold @genBVVec@ or @genCryM when normalizing @@ -313,14 +324,22 @@ smtNormPrims sc = Map.fromList tm' <- smtNorm sc tm return $ VExtra $ VExtraTerm a tm') ), - -- Don't normalize applications of @CompM@ - ("Prelude.CompM", - PrimFilterFun "CompM" (\case - TValue tv -> return tv - _ -> mzero) $ \tv -> - Prim (do tv_trm <- readBackTValueNoConfig "smtNormPrims (CompM)" sc tv - TValue <$> VTyTerm (mkSort 0) <$> - scGlobalApply sc "Prelude.CompM" [tv_trm])) + -- Don't normalize applications of @SpecM@ and its arguments + ("Prelude.SpecM", + PrimStrict $ \ev -> PrimStrict $ \stack -> PrimStrict $ \tp -> + Prim $ + do ev_tp <- VTyTerm (mkSort 1) <$> scDataTypeApp sc "Prelude.EvType" [] + ev_tm <- readBackValueNoConfig "smtNormPrims (SpecM)" sc ev_tp ev + stack_tp <- VTyTerm (mkSort 1) <$> scGlobalDef sc "Prelude.FunStack" + stack_tm <- + readBackValueNoConfig "smtNormPrims (SpecM)" sc stack_tp stack + tp_tm <- readBackValueNoConfig "smtNormPrims (SpecM)" sc (VSort $ + mkSort 0) tp + ret_tm <- scGlobalApply sc "Prelude.SpecM" [ev_tm,stack_tm,tp_tm] + return $ TValue $ VTyTerm (mkSort 0) ret_tm), + ("Prelude.VoidEv", primGlobal sc "Prelude.VoidEv"), + ("Prelude.emptyFunStack", primGlobal sc "Prelude.emptyFunStack"), + ("Prelude.pushFunStack", primGlobal sc "Prelude.pushFunStack") ] -- | A version of 'mrNormTerm' in the 'IO' monad, and which does not add any From 0fe52c525a3a5919b3b6ac61661ae23854a3b3d4 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Tue, 24 Jan 2023 18:30:45 -0800 Subject: [PATCH 21/27] updated some of the monadification tests to work with SpecM --- examples/mr_solver/SpecPrims.cry | 18 +++++++++--------- examples/mr_solver/monadify.cry | 4 ++-- examples/mr_solver/monadify.saw | 4 ++-- 3 files changed, 13 insertions(+), 13 deletions(-) diff --git a/examples/mr_solver/SpecPrims.cry b/examples/mr_solver/SpecPrims.cry index 4d938e3ecd..0a3b5d9ce4 100644 --- a/examples/mr_solver/SpecPrims.cry +++ b/examples/mr_solver/SpecPrims.cry @@ -3,25 +3,25 @@ module SpecPrims where /* Specification primitives */ -// The specification that holds for f x for some input x -exists : {a, b} (a -> b) -> b -exists f = error "Cannot run exists" +// The specification that holds for for some element of type a +exists : {a} a +exists = error "Cannot run exists" -// The specification that holds for f x for all inputs x -forall : {a, b} (a -> b) -> b -forall f = error "Cannot run forall" +// The specification that holds for for all elements of type a +forall : {a} a +forall = error "Cannot run forall" // The specification that a computation has no errors noErrors : {a} a -noErrors = exists (\x -> x) +noErrors = exists // The specification that matches any computation. This calls exists at the -// function type () -> a, which is monadified to () -> CompM a. This means that +// function type () -> a, which is monadified to () -> SpecM a. This means that // the exists does not just quantify over all values of type a like noErrors, // but it quantifies over all computations of type a, including those that // contain errors. anySpec : {a} a -anySpec = exists (\f -> f ()) +anySpec = exists () // The specification which asserts that the first argument is True and then // returns the second argument diff --git a/examples/mr_solver/monadify.cry b/examples/mr_solver/monadify.cry index 1d5659f5f7..c048a2303c 100644 --- a/examples/mr_solver/monadify.cry +++ b/examples/mr_solver/monadify.cry @@ -21,5 +21,5 @@ sha1 (t, x, y, z) = fib : [64] -> [64] fib x = if x == 0 then 1 else x * fib (x - 1) -fibSpecNoErrors : [64] -> [64] -fibSpecNoErrors _ = noErrors +// fibSpecNoErrors : [64] -> [64] +// fibSpecNoErrors _ = noErrors diff --git a/examples/mr_solver/monadify.saw b/examples/mr_solver/monadify.saw index 37e0e54d28..911dcfaf50 100644 --- a/examples/mr_solver/monadify.saw +++ b/examples/mr_solver/monadify.saw @@ -3,8 +3,8 @@ enable_experimental; import "SpecPrims.cry" as SpecPrims; import "monadify.cry"; load_sawcore_from_file "../../cryptol-saw-core/saw/CryptolM.sawcore"; -set_monadification "SpecPrims::exists" "Prelude.existsM"; -set_monadification "SpecPrims::forall" "Prelude.forallM"; +set_monadification "SpecPrims::exists" "Prelude.existsS"; +set_monadification "SpecPrims::forall" "Prelude.forallS"; let run_test name cry_term mon_term_expected = do { print (str_concat "Test: " name); From 90454079255599fb916b78e457a85d4e9fe8b7ee Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Tue, 24 Jan 2023 18:36:04 -0800 Subject: [PATCH 22/27] commented out tests involving monadifying quantifiers, which don't quite work yet --- examples/mr_solver/monadify.saw | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/examples/mr_solver/monadify.saw b/examples/mr_solver/monadify.saw index 911dcfaf50..70d6de95df 100644 --- a/examples/mr_solver/monadify.saw +++ b/examples/mr_solver/monadify.saw @@ -3,8 +3,12 @@ enable_experimental; import "SpecPrims.cry" as SpecPrims; import "monadify.cry"; load_sawcore_from_file "../../cryptol-saw-core/saw/CryptolM.sawcore"; -set_monadification "SpecPrims::exists" "Prelude.existsS"; -set_monadification "SpecPrims::forall" "Prelude.forallS"; + +// FIXME: these either need a small update to set_monadification to allow an +// arbitrary SAW core term on the RHS, or we need to add defs in the Prelude for +// the terms on the RHS here +//set_monadification "SpecPrims::exists" "Prelude.existsS Prelude.VoidEV"; +//set_monadification "SpecPrims::forall" "Prelude.forallS Prelude.VoidEV"; let run_test name cry_term mon_term_expected = do { print (str_concat "Test: " name); @@ -101,6 +105,7 @@ fibM <- parse_core_mod "CryptolM" "\ \ _x"; run_test "fib" fib fibM; +/* noErrors <- unfold_term ["noErrors"] {{ SpecPrims::noErrors }}; noErrorsM <- parse_core_mod "CryptolM" "\\(a : sort 0) -> existsM a a (\\(x : a) -> returnM a x)"; run_test "noErrors" noErrors noErrorsM; @@ -112,3 +117,4 @@ fibSpecNoErrorsM <- parse_core_mod "CryptolM" "\ \ (\\(x : (mseq (TCNum 64) Bool)) -> \ \ returnM (mseq (TCNum 64) Bool) x)"; run_test "fibSpecNoErrors" fibSpecNoErrors fibSpecNoErrorsM; +*/ From 1e16b60d3cdaee0e4d9fa6014627f06250e0c7c2 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Wed, 25 Jan 2023 07:27:06 -0800 Subject: [PATCH 23/27] changed the set_monadification command to allow for monadifications that are polymorphic over the event type and fun stack params --- .../src/Verifier/SAW/Cryptol/Monadify.hs | 22 ++++++++++++++----- src/SAWScript/Builtins.hs | 10 +++++---- src/SAWScript/Interpreter.hs | 6 +++-- 3 files changed, 27 insertions(+), 11 deletions(-) diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs index d9a77152e9..93b6077853 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs @@ -1452,12 +1452,24 @@ ensureCryptolMLoaded sc = if is_loaded then return () else scLoadCryptolMModule sc --- | Monadify a type to its argument type and complete it to a 'Term' -monadifyCompleteArgType :: SharedContext -> MonadifyEnv -> Term -> +-- | Monadify a type to its argument type and complete it to a 'Term', +-- additionally quantifying over the event type and function stack if the +-- supplied 'Bool' is 'True' +monadifyCompleteArgType :: SharedContext -> MonadifyEnv -> Term -> Bool -> IO Term -monadifyCompleteArgType sc env tp = - let ?specMParams = monEnvParams env in - completeOpenTerm sc $ monadifyTypeArgType [] tp +monadifyCompleteArgType sc env tp poly_p = + completeOpenTerm sc $ + if poly_p then + -- Parameter polymorphism means pi-quantification over E and stack + (piOpenTerm "E" (dataTypeOpenTerm "Prelude.EvType" []) $ \e -> + piOpenTerm "stack" (globalOpenTerm "Prelude.FunStack") $ \st -> + let ?specMParams = SpecMParams { specMEvType = e, specMStack = st } in + -- NOTE: even though E and stack are free variables here, they are not + -- free in tp, which is a closed term, so we do not list them in the + -- MonadifyTypeCtx argument of monadifyTypeArgType + monadifyTypeArgType [] tp) + else + let ?specMParams = monEnvParams env in monadifyTypeArgType [] tp -- | Monadify a term of the specified type to a 'MonTerm' and then complete that -- 'MonTerm' to a SAW core 'Term', or 'fail' if this is not possible diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index fcdaa7924c..224debfd04 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -2266,8 +2266,8 @@ mrSolverSetDebug dlvl = modify (\rw -> rw { rwMRSolverEnv = Prover.mrEnvSetDebugLevel dlvl (rwMRSolverEnv rw) }) -setMonadification :: SharedContext -> String -> String -> TopLevel () -setMonadification sc cry_str saw_str = +setMonadification :: SharedContext -> String -> String -> Bool -> TopLevel () +setMonadification sc cry_str saw_str poly_p = do rw <- get -- Step 1: convert the first string to a Cryptol name @@ -2297,7 +2297,8 @@ setMonadification sc cry_str saw_str = scTypeOf sc cry_nm_trans _ -> fail ("Could not find type for Cryptol name: " ++ cry_str) cry_mon_tp <- - liftIO $ Monadify.monadifyCompleteArgType sc (rwMonadify rw) cry_saw_tp + liftIO $ + Monadify.monadifyCompleteArgType sc (rwMonadify rw) cry_saw_tp poly_p -- Step 3: convert the second string to a typed SAW core term, and if it -- has an existing macro, check that it has the same type as the type for @@ -2310,7 +2311,8 @@ setMonadification sc cry_str saw_str = let (tp_to_check, macro) = case Monadify.monEnvLookup (ModuleIdentifier saw_ident) (rwMonadify rw) of Just existing_macro -> (cry_saw_tp, existing_macro) - Nothing -> (cry_mon_tp, Monadify.argGlobalMacro cry_nmi saw_ident False) + Nothing -> (cry_mon_tp, + Monadify.argGlobalMacro cry_nmi saw_ident poly_p) liftIO $ scCheckSubtype sc Nothing (TC.TypedTerm saw_trm saw_tp) tp_to_check -- Step 4: Add the generated macro diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index cf4436979c..f2e4a8bd73 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -3788,11 +3788,13 @@ primitives = Map.fromList [ "Monadify a Cryptol term, converting it to a form where all recursion" , " and errors are represented as monadic operators"] - , prim "set_monadification" "String -> String -> TopLevel Term" + , prim "set_monadification" "String -> String -> Bool -> TopLevel Term" (scVal setMonadification) Experimental [ "Set the monadification of a specific Cryptol identifer to a SAW core " - , "identifier of monadic type" ] + , "identifier of monadic type. The supplied Boolean flag indicates if the " + , "SAW core term is polymorphic in the event type and function stack of the" + , "SpecM monad."] , prim "heapster_init_env" "String -> String -> TopLevel HeapsterEnv" From ef7c47c9bd3d9fdad5886f4343312a3677c1a45d Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Wed, 25 Jan 2023 07:27:21 -0800 Subject: [PATCH 24/27] updated the monadification tests to succeed with the new SpecM monad --- examples/mr_solver/monadify.cry | 4 +- examples/mr_solver/monadify.saw | 141 +++++++++++++++++--------------- 2 files changed, 78 insertions(+), 67 deletions(-) diff --git a/examples/mr_solver/monadify.cry b/examples/mr_solver/monadify.cry index c048a2303c..1d5659f5f7 100644 --- a/examples/mr_solver/monadify.cry +++ b/examples/mr_solver/monadify.cry @@ -21,5 +21,5 @@ sha1 (t, x, y, z) = fib : [64] -> [64] fib x = if x == 0 then 1 else x * fib (x - 1) -// fibSpecNoErrors : [64] -> [64] -// fibSpecNoErrors _ = noErrors +fibSpecNoErrors : [64] -> [64] +fibSpecNoErrors _ = noErrors diff --git a/examples/mr_solver/monadify.saw b/examples/mr_solver/monadify.saw index 70d6de95df..0ef484fd5f 100644 --- a/examples/mr_solver/monadify.saw +++ b/examples/mr_solver/monadify.saw @@ -4,11 +4,9 @@ import "SpecPrims.cry" as SpecPrims; import "monadify.cry"; load_sawcore_from_file "../../cryptol-saw-core/saw/CryptolM.sawcore"; -// FIXME: these either need a small update to set_monadification to allow an -// arbitrary SAW core term on the RHS, or we need to add defs in the Prelude for -// the terms on the RHS here -//set_monadification "SpecPrims::exists" "Prelude.existsS Prelude.VoidEV"; -//set_monadification "SpecPrims::forall" "Prelude.forallS Prelude.VoidEV"; +// Set the monadification of the Cryptol exists and forall functions +set_monadification "SpecPrims::exists" "Prelude.existsS" true; +set_monadification "SpecPrims::forall" "Prelude.forallS" true; let run_test name cry_term mon_term_expected = do { print (str_concat "Test: " name); @@ -25,40 +23,48 @@ let run_test name cry_term mon_term_expected = my_abs <- unfold_term ["my_abs"] {{ my_abs }}; my_abs_M <- parse_core_mod "CryptolM" "\ -\ \\(x : (mseq (TCNum 64) Bool)) -> \ -\ bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \ +\ \\(x : (mseq VoidEv emptyFunStack (TCNum 64) Bool)) -> \ +\ bindS VoidEv emptyFunStack (isFinite (TCNum 64)) \ +\ (mseq VoidEv emptyFunStack (TCNum 64) Bool) \ +\ (assertFiniteS VoidEv emptyFunStack (TCNum 64)) \ \ (\\(x' : (isFinite (TCNum 64))) -> \ -\ bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \ +\ bindS VoidEv emptyFunStack (isFinite (TCNum 64)) \ +\ (mseq VoidEv emptyFunStack (TCNum 64) Bool) \ +\ (assertFiniteS VoidEv emptyFunStack (TCNum 64)) \ \ (\\(x'' : (isFinite (TCNum 64))) -> \ -\ ite (CompM (mseq (TCNum 64) Bool)) \ -\ (ecLt (mseq (TCNum 64) Bool) (PCmpMSeqBool (TCNum 64) x') x \ -\ (ecNumber (TCNum 0) (mseq (TCNum 64) Bool) (PLiteralSeqBoolM (TCNum 64) x''))) \ -\ (bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \ +\ ite (SpecM VoidEv emptyFunStack (mseq VoidEv emptyFunStack (TCNum 64) Bool)) \ +\ (ecLt (mseq VoidEv emptyFunStack (TCNum 64) Bool) (PCmpMSeqBool VoidEv emptyFunStack (TCNum 64) x') x \ +\ (ecNumber (TCNum 0) (mseq VoidEv emptyFunStack (TCNum 64) Bool) (PLiteralSeqBoolM VoidEv emptyFunStack (TCNum 64) x''))) \ +\ (bindS VoidEv emptyFunStack (isFinite (TCNum 64)) \ +\ (mseq VoidEv emptyFunStack (TCNum 64) Bool) \ +\ (assertFiniteS VoidEv emptyFunStack (TCNum 64)) \ \ (\\(x''' : (isFinite (TCNum 64))) -> \ -\ returnM (mseq (TCNum 64) Bool) (ecNeg (mseq (TCNum 64) Bool) (PRingMSeqBool (TCNum 64) x''') x))) \ -\ (returnM (mseq (TCNum 64) Bool) x)))"; +\ retS VoidEv emptyFunStack \ +\ (mseq VoidEv emptyFunStack (TCNum 64) Bool) \ +\ (ecNeg (mseq VoidEv emptyFunStack (TCNum 64) Bool) (PRingMSeqBool VoidEv emptyFunStack (TCNum 64) x''') x))) \ +\ (retS VoidEv emptyFunStack (mseq VoidEv emptyFunStack (TCNum 64) Bool) x)))"; run_test "my_abs" my_abs my_abs_M; err_if_lt0 <- unfold_term ["err_if_lt0"] {{ err_if_lt0 }}; err_if_lt0_M <- parse_core_mod "CryptolM" "\ -\ \\(x : (mseq (TCNum 64) Bool)) -> \ -\ bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \ +\ \\(x : (mseq VoidEv emptyFunStack (TCNum 64) Bool)) -> \ +\ bindS VoidEv emptyFunStack (isFinite (TCNum 64)) (mseq VoidEv emptyFunStack (TCNum 64) Bool) (assertFiniteS VoidEv emptyFunStack (TCNum 64)) \ \ (\\(x' : (isFinite (TCNum 64))) -> \ -\ bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \ +\ bindS VoidEv emptyFunStack (isFinite (TCNum 64)) (mseq VoidEv emptyFunStack (TCNum 64) Bool) (assertFiniteS VoidEv emptyFunStack (TCNum 64)) \ \ (\\(x'' : (isFinite (TCNum 64))) -> \ -\ ite (CompM (mseq (TCNum 64) Bool)) \ -\ (ecLt (mseq (TCNum 64) Bool) (PCmpMSeqBool (TCNum 64) x') x \ -\ (ecNumber (TCNum 0) (mseq (TCNum 64) Bool) (PLiteralSeqBoolM (TCNum 64) x''))) \ -\ (bindM (isFinite (TCNum 8)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 8)) \ +\ ite (SpecM VoidEv emptyFunStack (mseq VoidEv emptyFunStack (TCNum 64) Bool)) \ +\ (ecLt (mseq VoidEv emptyFunStack (TCNum 64) Bool) (PCmpMSeqBool VoidEv emptyFunStack (TCNum 64) x') x \ +\ (ecNumber (TCNum 0) (mseq VoidEv emptyFunStack (TCNum 64) Bool) (PLiteralSeqBoolM VoidEv emptyFunStack (TCNum 64) x''))) \ +\ (bindS VoidEv emptyFunStack (isFinite (TCNum 8)) (mseq VoidEv emptyFunStack (TCNum 64) Bool) (assertFiniteS VoidEv emptyFunStack (TCNum 8)) \ \ (\\(x''' : (isFinite (TCNum 8))) -> \ -\ ecErrorM (mseq (TCNum 64) Bool) (TCNum 5) \ -\ (seqToMseq (TCNum 5) (mseq (TCNum 8) Bool) \ -\ [ ecNumber (TCNum 120) (mseq (TCNum 8) Bool) (PLiteralSeqBoolM (TCNum 8) x''') \ -\ , (ecNumber (TCNum 32) (mseq (TCNum 8) Bool) (PLiteralSeqBoolM (TCNum 8) x''')) \ -\ , ecNumber (TCNum 60) (mseq (TCNum 8) Bool) (PLiteralSeqBoolM (TCNum 8) x''') \ -\ , (ecNumber (TCNum 32) (mseq (TCNum 8) Bool) (PLiteralSeqBoolM (TCNum 8) x''')) \ -\ , ecNumber (TCNum 48) (mseq (TCNum 8) Bool) (PLiteralSeqBoolM (TCNum 8) x''') ]))) \ -\ (returnM (mseq (TCNum 64) Bool) x)))"; +\ ecErrorM VoidEv emptyFunStack (mseq VoidEv emptyFunStack (TCNum 64) Bool) (TCNum 5) \ +\ (seqToMseq VoidEv emptyFunStack (TCNum 5) (mseq VoidEv emptyFunStack (TCNum 8) Bool) \ +\ [ ecNumber (TCNum 120) (mseq VoidEv emptyFunStack (TCNum 8) Bool) (PLiteralSeqBoolM VoidEv emptyFunStack (TCNum 8) x''') \ +\ , (ecNumber (TCNum 32) (mseq VoidEv emptyFunStack (TCNum 8) Bool) (PLiteralSeqBoolM VoidEv emptyFunStack (TCNum 8) x''')) \ +\ , ecNumber (TCNum 60) (mseq VoidEv emptyFunStack (TCNum 8) Bool) (PLiteralSeqBoolM VoidEv emptyFunStack (TCNum 8) x''') \ +\ , (ecNumber (TCNum 32) (mseq VoidEv emptyFunStack (TCNum 8) Bool) (PLiteralSeqBoolM VoidEv emptyFunStack (TCNum 8) x''')) \ +\ , ecNumber (TCNum 48) (mseq VoidEv emptyFunStack (TCNum 8) Bool) (PLiteralSeqBoolM VoidEv emptyFunStack (TCNum 8) x''') ]))) \ +\ (retS VoidEv emptyFunStack (mseq VoidEv emptyFunStack (TCNum 64) Bool) x)))"; run_test "err_if_lt0" err_if_lt0 err_if_lt0_M; /* @@ -73,48 +79,53 @@ print_term sha1M; fib <- unfold_term ["fib"] {{ fib }}; fibM <- parse_core_mod "CryptolM" "\ -\ \\(_x : (mseq (TCNum 64) Bool)) -> \ -\ multiArgFixM (LRT_Fun (mseq (TCNum 64) Bool) (\\(_ : (mseq (TCNum 64) Bool)) -> LRT_Ret (mseq (TCNum 64) Bool))) \ -\ (\\(fib : ((mseq (TCNum 64) Bool) -> (CompM (mseq (TCNum 64) Bool)))) -> \ -\ \\(x : (mseq (TCNum 64) Bool)) -> \ -\ bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \ -\ (\\(x' : (isFinite (TCNum 64))) -> \ -\ bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \ -\ (\\(x'' : (isFinite (TCNum 64))) -> \ -\ ite (CompM (mseq (TCNum 64) Bool)) \ -\ (ecEq (mseq (TCNum 64) Bool) (PEqMSeqBool (TCNum 64) x') x \ -\ (ecNumber (TCNum 0) (mseq (TCNum 64) Bool) (PLiteralSeqBoolM (TCNum 64) x''))) \ -\ (bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \ -\ (\\(x''' : (isFinite (TCNum 64))) -> \ -\ returnM (mseq (TCNum 64) Bool) \ -\ (ecNumber (TCNum 1) (mseq (TCNum 64) Bool) \ -\ (PLiteralSeqBoolM (TCNum 64) x''')))) \ -\ (bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \ -\ (\\(x''' : (isFinite (TCNum 64))) -> \ -\ bindM (isFinite (TCNum 64)) (mseq (TCNum 64) Bool) (assertFiniteM (TCNum 64)) \ -\ (\\(x'''' : (isFinite (TCNum 64))) -> \ -\ bindM (mseq (TCNum 64) Bool) (mseq (TCNum 64) Bool) \ -\ (fib \ -\ (ecMinus (mseq (TCNum 64) Bool) (PRingMSeqBool (TCNum 64) x''') x \ -\ (ecNumber (TCNum 1) (mseq (TCNum 64) Bool) \ -\ (PLiteralSeqBoolM (TCNum 64) x'''')))) \ -\ (\\(x''''' : (mseq (TCNum 64) Bool)) -> \ -\ returnM (mseq (TCNum 64) Bool) \ -\ (ecMul (mseq (TCNum 64) Bool) (PRingMSeqBool (TCNum 64) x''') x \ -\ x''''')))))))) \ +\ \\(_x : (mseq VoidEv emptyFunStack (TCNum 64) Bool)) -> \ +\ multiArgFixS VoidEv emptyFunStack \ +\ (LRT_Fun (mseq VoidEv emptyFunStack (TCNum 64) Bool) \ +\ (\\(_ : (mseq VoidEv emptyFunStack (TCNum 64) Bool)) -> \ +\ LRT_Ret (mseq VoidEv emptyFunStack (TCNum 64) Bool))) \ +\ ((\\ (stk:FunStack) -> \ +\ (\\(fib : ((mseq VoidEv stk (TCNum 64) Bool) -> \ +\ (SpecM VoidEv stk (mseq VoidEv stk (TCNum 64) Bool)))) -> \ +\ \\(x : (mseq VoidEv stk (TCNum 64) Bool)) -> \ +\ bindS VoidEv stk (isFinite (TCNum 64)) (mseq VoidEv stk (TCNum 64) Bool) (assertFiniteS VoidEv stk (TCNum 64)) \ +\ (\\(x' : (isFinite (TCNum 64))) -> \ +\ bindS VoidEv stk (isFinite (TCNum 64)) (mseq VoidEv stk (TCNum 64) Bool) (assertFiniteS VoidEv stk (TCNum 64)) \ +\ (\\(x'' : (isFinite (TCNum 64))) -> \ +\ ite (SpecM VoidEv stk (mseq VoidEv stk (TCNum 64) Bool)) \ +\ (ecEq (mseq VoidEv stk (TCNum 64) Bool) (PEqMSeqBool VoidEv stk (TCNum 64) x') x \ +\ (ecNumber (TCNum 0) (mseq VoidEv stk (TCNum 64) Bool) (PLiteralSeqBoolM VoidEv stk (TCNum 64) x''))) \ +\ (bindS VoidEv stk (isFinite (TCNum 64)) (mseq VoidEv stk (TCNum 64) Bool) (assertFiniteS VoidEv stk (TCNum 64)) \ +\ (\\(x''' : (isFinite (TCNum 64))) -> \ +\ retS VoidEv stk (mseq VoidEv stk (TCNum 64) Bool) \ +\ (ecNumber (TCNum 1) (mseq VoidEv stk (TCNum 64) Bool) \ +\ (PLiteralSeqBoolM VoidEv stk (TCNum 64) x''')))) \ +\ (bindS VoidEv stk (isFinite (TCNum 64)) (mseq VoidEv stk (TCNum 64) Bool) (assertFiniteS VoidEv stk (TCNum 64)) \ +\ (\\(x''' : (isFinite (TCNum 64))) -> \ +\ bindS VoidEv stk (isFinite (TCNum 64)) (mseq VoidEv stk (TCNum 64) Bool) (assertFiniteS VoidEv stk (TCNum 64)) \ +\ (\\(x'''' : (isFinite (TCNum 64))) -> \ +\ bindS VoidEv stk (mseq VoidEv stk (TCNum 64) Bool) (mseq VoidEv stk (TCNum 64) Bool) \ +\ (fib \ +\ (ecMinus (mseq VoidEv stk (TCNum 64) Bool) (PRingMSeqBool VoidEv stk (TCNum 64) x''') x \ +\ (ecNumber (TCNum 1) (mseq VoidEv stk (TCNum 64) Bool) \ +\ (PLiteralSeqBoolM VoidEv stk (TCNum 64) x'''')))) \ +\ (\\(x''''' : (mseq VoidEv stk (TCNum 64) Bool)) -> \ +\ retS VoidEv stk (mseq VoidEv stk (TCNum 64) Bool) \ +\ (ecMul (mseq VoidEv stk (TCNum 64) Bool) (PRingMSeqBool VoidEv stk (TCNum 64) x''') x \ +\ x'''''))))))))) \ +\ (pushFunStack (singletonFrame (LRT_Fun (mseq VoidEv emptyFunStack (TCNum 64) Bool) \ +\ (\\ (_:Vec 64 Bool) -> \ +\ LRT_Ret (mseq VoidEv emptyFunStack (TCNum 64) Bool)))) \ +\ emptyFunStack)) \ \ _x"; run_test "fib" fib fibM; -/* noErrors <- unfold_term ["noErrors"] {{ SpecPrims::noErrors }}; -noErrorsM <- parse_core_mod "CryptolM" "\\(a : sort 0) -> existsM a a (\\(x : a) -> returnM a x)"; +noErrorsM <- parse_core_mod "CryptolM" "\\(a : sort 0) -> existsS VoidEv emptyFunStack a"; run_test "noErrors" noErrors noErrorsM; fibSpecNoErrors <- unfold_term ["fibSpecNoErrors"] {{ fibSpecNoErrors }}; fibSpecNoErrorsM <- parse_core_mod "CryptolM" "\ -\ \\(__p1 : (mseq (TCNum 64) Bool)) -> \ -\ existsM (mseq (TCNum 64) Bool) (mseq (TCNum 64) Bool) \ -\ (\\(x : (mseq (TCNum 64) Bool)) -> \ -\ returnM (mseq (TCNum 64) Bool) x)"; +\ \\(__p1 : (mseq VoidEv emptyFunStack (TCNum 64) Bool)) -> \ +\ existsS VoidEv emptyFunStack (mseq VoidEv emptyFunStack (TCNum 64) Bool)"; run_test "fibSpecNoErrors" fibSpecNoErrors fibSpecNoErrorsM; -*/ From 2a5bc52f915d815ec136432d06552d332356f5ca Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Wed, 25 Jan 2023 11:44:04 -0500 Subject: [PATCH 25/27] resolve defined-but-not-used warnings in Solver.hs --- src/SAWScript/Prover/MRSolver/Solver.hs | 26 ++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs index 31e79c24b2..8531409d70 100644 --- a/src/SAWScript/Prover/MRSolver/Solver.hs +++ b/src/SAWScript/Prover/MRSolver/Solver.hs @@ -128,7 +128,7 @@ import Data.Either import Numeric.Natural (Natural) import Data.List (find, findIndices) import Data.Foldable (foldlM) -import Data.Bits (shiftL) +-- import Data.Bits (shiftL) import Control.Monad.Reader import Control.Monad.Except import qualified Data.Map as Map @@ -323,7 +323,7 @@ normComp (CompTerm t) = all_args <- (++ args) <$> getAllUVarTerms FunBind var all_args <$> mkCompFunReturn <$> mrFunOutType var all_args - (isGlobalDef "Prelude.multiArgFixS" -> Just (), ev:stack:lrt:body:args) -> + (isGlobalDef "Prelude.multiArgFixS" -> Just (), _ev:_stack:_lrt:body:args) -> do -- Bind a fresh function var for the new recursive function body_tp <- mrTypeOf body @@ -346,8 +346,8 @@ normComp (CompTerm t) = -- Convert `vecMapM (bvToNat ...)` into `bvVecMapInvarM`, with the -- invariant being the current set of assumptions - (asGlobalDef -> Just "CryptolM.vecMapM", [a, b, (asBvToNat -> Just (w, n)), - f, xs]) -> + (asGlobalDef -> Just "CryptolM.vecMapM", [_a, _b, (asBvToNat -> Just (_w, _n)), + _f, _xs]) -> error "FIXME HERE NOW: need SpecM version of vecMapM" {- do invar <- mrAssumptions @@ -357,8 +357,8 @@ normComp (CompTerm t) = -- Convert `atM (bvToNat ...) ... (bvToNat ...)` into the unfolding of -- `bvVecAtM` - (asGlobalDef -> Just "CryptolM.atM", [(asBvToNat -> Just (w1, n)), a, xs, - (asBvToNat -> Just (w2, i))]) -> + (asGlobalDef -> Just "CryptolM.atM", [(asBvToNat -> Just (_w1, _n)), _a, _xs, + (asBvToNat -> Just (_w2, _i))]) -> error "FIXME HERE NOW: need SpecM version of atM" {- do body <- mrGlobalDefBody "CryptolM.bvVecAtM" @@ -370,10 +370,10 @@ normComp (CompTerm t) = -- Convert `atM n ... xs (bvToNat ...)` for a constant `n` into the -- unfolding of `bvVecAtM` after converting `n` to a bitvector constant -- and applying `genBVVecFromVec` to `xs` - (asGlobalDef -> Just "CryptolM.atM", [n_tm@(asNat -> Just n), a, xs, + (asGlobalDef -> Just "CryptolM.atM", [_n_tm@(asNat -> Just _n), _a, _xs, (asBvToNat -> - Just (w_tm@(asNat -> Just w), - i))]) -> + Just (_w_tm@(asNat -> Just _w), + _i))]) -> error "FIXME HERE NOW: need SpecM version of atM" {- do body <- mrGlobalDefBody "CryptolM.bvVecAtM" @@ -385,8 +385,8 @@ normComp (CompTerm t) = -- Convert `updateM (bvToNat ...) ... (bvToNat ...)` into the unfolding of -- `bvVecUpdateM` - (asGlobalDef -> Just "CryptolM.updateM", [(asBvToNat -> Just (w1, n)), a, xs, - (asBvToNat -> Just (w2, i)), x]) -> + (asGlobalDef -> Just "CryptolM.updateM", [(asBvToNat -> Just (_w1, _n)), _a, _xs, + (asBvToNat -> Just (_w2, _i)), _x]) -> error "FIXME HERE NOW: need SpecM version of updateM" {- do body <- mrGlobalDefBody "CryptolM.bvVecUpdateM" @@ -399,8 +399,8 @@ normComp (CompTerm t) = -- unfolding of `bvVecUpdateM` after converting `n` to a bitvector constant -- and applying `genBVVecFromVec` to `xs` (asGlobalDef -> Just "CryptolM.updateM", - [n_tm@(asNat -> Just n), a, xs, (asBvToNat -> - Just (w_tm@(asNat -> Just w), i)), x]) -> + [_n_tm@(asNat -> Just _n), _a, _xs, (asBvToNat -> + Just (_w_tm@(asNat -> Just _w), _i)), _x]) -> error "FIXME HERE NOW: need SpecM version of updateM" {- do body <- mrGlobalDefBody "CryptolM.fromBVVecUpdateM" From 603420fd1070666ee8b1eb36ee5ba8dfbcc9daba Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Wed, 25 Jan 2023 17:12:32 -0500 Subject: [PATCH 26/27] update pinned commit to entree-specs --- .github/workflows/ci.yml | 2 +- saw-core-coq/README.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 0009df81ab..da9944558c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -285,7 +285,7 @@ jobs: # If you change the entree-specs commit below, make sure you update the # documentation in saw-core-coq/README.md accordingly. - - run: opam pin -y entree-specs https://github.com/GaloisInc/entree-specs.git#b011f29680fdde87489bc06ae98bfff0f97795b3 + - run: opam pin -y entree-specs https://github.com/GaloisInc/entree-specs.git#52c4868f1f65c7ce74e90000214de27e23ba98fb # FIXME: the following steps generate Coq libraries for the SAW core to # Coq translator and builds them; if we do other Coq tests, these steps diff --git a/saw-core-coq/README.md b/saw-core-coq/README.md index e229b500df..ad8ca7c9e5 100644 --- a/saw-core-coq/README.md +++ b/saw-core-coq/README.md @@ -31,7 +31,7 @@ sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install. opam init opam repo add coq-released https://coq.inria.fr/opam/released opam install -y coq-bits -opam pin -y entree-specs https://github.com/GaloisInc/entree-specs.git#b011f29680fdde87489bc06ae98bfff0f97795b3 +opam pin -y entree-specs https://github.com/GaloisInc/entree-specs.git#52c4868f1f65c7ce74e90000214de27e23ba98fb ``` We have pinned the `entree-specs` dependency's commit to ensure that it points From cc9fd580a99aab9814041686347be252332da3d0 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Wed, 25 Jan 2023 17:24:20 -0500 Subject: [PATCH 27/27] style tweak in constraints in Monadify.hs --- cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs index 93b6077853..d1633e4111 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs @@ -426,7 +426,7 @@ typeCtxPureCtx :: MonadifyTypeCtx -> [(LocalName,Term)] typeCtxPureCtx = map (\(x,tp,_) -> (x,tp)) -- | Monadify a type and convert it to its corresponding argument type -monadifyTypeArgType :: HasCallStack => HasSpecMParams => MonadifyTypeCtx -> +monadifyTypeArgType :: (HasCallStack, HasSpecMParams) => MonadifyTypeCtx -> Term -> OpenTerm monadifyTypeArgType ctx t = toArgType $ monadifyType ctx t @@ -439,7 +439,7 @@ applyMonType (MTyForall _ _ f) (Left mtp) = f mtp applyMonType _ _ = error "applyMonType: application at incorrect type" -- | Convert a SAW core 'Term' to a monadification type -monadifyType :: HasCallStack => HasSpecMParams => MonadifyTypeCtx -> Term -> +monadifyType :: (HasCallStack, HasSpecMParams) => MonadifyTypeCtx -> Term -> MonType {- monadifyType ctx t @@ -515,7 +515,7 @@ monadifyType ctx tp = ++ ppTermInTypeCtx ctx tp) -- | Monadify a type-level natural number -monadifyTypeNat :: HasCallStack => HasSpecMParams => MonadifyTypeCtx -> Term -> +monadifyTypeNat :: (HasCallStack, HasSpecMParams) => MonadifyTypeCtx -> Term -> OpenTerm monadifyTypeNat _ (asNat -> Just n) = natOpenTerm n monadifyTypeNat ctx (asLocalVar -> Just i)