mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-23 03:48:46 +03:00
Merge remote-tracking branch 'origin/master' into split-arith
This commit is contained in:
commit
bbba626052
@ -574,6 +574,7 @@ cmdProveSat isSat str = do
|
||||
(t, e) <- mkSolverResult cexStr (not isSat) (Left ts)
|
||||
bindItVariable t e
|
||||
AllSatResult tevss -> do
|
||||
rPutStrLn (if isSat then "Satisfiable" else "Counterexample")
|
||||
let tess = map (map $ \(t,e,_) -> (t,e)) tevss
|
||||
vss = map (map $ \(_,_,v) -> v) tevss
|
||||
resultRecs <- mapM (mkSolverResult cexStr isSat . Right) tess
|
||||
|
@ -35,6 +35,7 @@ import qualified Control.Exception as X
|
||||
import qualified Data.SBV.Dynamic as SBV
|
||||
import Data.SBV (Timing(SaveTiming))
|
||||
import Data.SBV.Internals (showTDiff)
|
||||
import Data.Time (NominalDiffTime)
|
||||
|
||||
import qualified Cryptol.ModuleSystem as M hiding (getPrimMap)
|
||||
import qualified Cryptol.ModuleSystem.Env as M
|
||||
@ -88,6 +89,7 @@ proverConfigs =
|
||||
, ("sbv-any" , SBV.defaultSMTCfg )
|
||||
]
|
||||
|
||||
-- | The names of all the solvers supported by SBV
|
||||
proverNames :: [String]
|
||||
proverNames = map fst proverConfigs
|
||||
|
||||
@ -104,6 +106,8 @@ satSMTResults (SBV.SatResult r) = [r]
|
||||
allSatSMTResults :: SBV.AllSatResult -> [SBV.SMTResult]
|
||||
allSatSMTResults (SBV.AllSatResult (_, _, _, rs)) = rs
|
||||
|
||||
-- | Check if the named solver can be found and invoked
|
||||
-- in the current solver environment.
|
||||
checkProverInstallation :: String -> IO Bool
|
||||
checkProverInstallation s =
|
||||
do let prover = lookupProver s
|
||||
@ -116,43 +120,27 @@ proverError :: String -> M.ModuleCmd (Maybe String, ProverResult)
|
||||
proverError msg (_,modEnv) =
|
||||
return (Right ((Nothing, ProverError msg), modEnv), [])
|
||||
|
||||
satProve :: ProverCommand -> M.ModuleCmd (Maybe String, ProverResult)
|
||||
satProve ProverCommand {..} =
|
||||
protectStack proverError $ \(evo,modEnv) ->
|
||||
|
||||
M.runModuleM (evo,modEnv) $ do
|
||||
let (isSat, mSatNum) = case pcQueryType of
|
||||
ProveQuery -> (False, Nothing)
|
||||
SatQuery sn -> case sn of
|
||||
SomeSat n -> (True, Just n)
|
||||
AllSat -> (True, Nothing)
|
||||
let extDgs = M.allDeclGroups modEnv ++ pcExtraDecls
|
||||
provers <-
|
||||
case pcProverName of
|
||||
"any" -> M.io SBV.sbvAvailableSolvers
|
||||
"sbv-any" -> M.io SBV.sbvAvailableSolvers
|
||||
_ -> return [(lookupProver pcProverName) { SBV.transcript = pcSmtFile
|
||||
, SBV.allSatMaxModelCount = mSatNum
|
||||
}]
|
||||
|
||||
|
||||
let provers' = [ p { SBV.timing = SaveTiming pcProverStats
|
||||
, SBV.verbose = pcVerbose
|
||||
, SBV.validateModel = pcValidate
|
||||
} | p <- provers ]
|
||||
let tyFn = if isSat then existsFinType else forallFinType
|
||||
runSingleProver ::
|
||||
ProverCommand ->
|
||||
[SBV.SMTConfig] ->
|
||||
(SBV.SMTConfig -> SBV.Symbolic SBV.SVal -> IO res) ->
|
||||
(res -> [SBV.SMTResult]) ->
|
||||
SBV.Symbolic SBV.SVal ->
|
||||
M.ModuleT IO (Maybe String, [SBV.SMTResult])
|
||||
runSingleProver ProverCommand{..} provers callSolver processResult e = do
|
||||
let lPutStrLn = M.withLogger logPutStrLn
|
||||
let runProver fn tag e = do
|
||||
|
||||
case provers of
|
||||
[prover] -> do
|
||||
when pcVerbose $
|
||||
lPutStrLn $ "Trying proof with " ++
|
||||
show (SBV.name (SBV.solver prover))
|
||||
res <- M.io (fn prover e)
|
||||
res <- M.io (callSolver prover e)
|
||||
when pcVerbose $
|
||||
lPutStrLn $ "Got result from " ++
|
||||
show (SBV.name (SBV.solver prover))
|
||||
return (Just (show (SBV.name (SBV.solver prover))), tag res)
|
||||
return (Just (show (SBV.name (SBV.solver prover))), processResult res)
|
||||
_ ->
|
||||
return ( Nothing
|
||||
, [ SBV.ProofError
|
||||
@ -161,39 +149,129 @@ satProve ProverCommand {..} =
|
||||
Nothing
|
||||
| prover <- provers ]
|
||||
)
|
||||
runProvers fn tag e = do
|
||||
|
||||
runMultiProvers ::
|
||||
ProverCommand ->
|
||||
[SBV.SMTConfig] ->
|
||||
([SBV.SMTConfig] -> SBV.Symbolic SBV.SVal -> IO (SBV.Solver, NominalDiffTime, res)) ->
|
||||
(res -> [SBV.SMTResult]) ->
|
||||
SBV.Symbolic SBV.SVal ->
|
||||
M.ModuleT IO (Maybe String, [SBV.SMTResult])
|
||||
runMultiProvers ProverCommand{..} provers callSolvers processResult e = do
|
||||
let lPutStrLn = M.withLogger logPutStrLn
|
||||
|
||||
when pcVerbose $
|
||||
lPutStrLn $ "Trying proof with " ++
|
||||
intercalate ", " (map (show . SBV.name . SBV.solver) provers)
|
||||
(firstProver, timeElapsed, res) <- M.io (fn provers' e)
|
||||
(firstProver, timeElapsed, res) <- M.io (callSolvers provers e)
|
||||
when pcVerbose $
|
||||
lPutStrLn $ "Got result from " ++ show firstProver ++
|
||||
", time: " ++ showTDiff timeElapsed
|
||||
return (Just (show firstProver), tag res)
|
||||
let runFn = case pcQueryType of
|
||||
ProveQuery -> runProvers SBV.proveWithAny thmSMTResults
|
||||
return (Just (show firstProver), processResult res)
|
||||
|
||||
-- | Select the appropriate solver or solvers from the given prover command,
|
||||
-- and invoke those solvers on the given symbolic value.
|
||||
runProver :: ProverCommand -> SBV.Symbolic SBV.SVal -> M.ModuleT IO (Maybe String, [SBV.SMTResult])
|
||||
runProver pc@ProverCommand{..} x =
|
||||
do let mSatNum = case pcQueryType of
|
||||
SatQuery (SomeSat n) -> Just n
|
||||
SatQuery AllSat -> Nothing
|
||||
ProveQuery -> Nothing
|
||||
|
||||
provers <-
|
||||
case pcProverName of
|
||||
"any" -> M.io SBV.sbvAvailableSolvers
|
||||
"sbv-any" -> M.io SBV.sbvAvailableSolvers
|
||||
_ -> return [(lookupProver pcProverName)
|
||||
{ SBV.transcript = pcSmtFile
|
||||
, SBV.allSatMaxModelCount = mSatNum
|
||||
}]
|
||||
|
||||
let provers' = [ p { SBV.timing = SaveTiming pcProverStats
|
||||
, SBV.verbose = pcVerbose
|
||||
, SBV.validateModel = pcValidate
|
||||
}
|
||||
| p <- provers
|
||||
]
|
||||
|
||||
case pcQueryType of
|
||||
ProveQuery -> runMultiProvers pc provers' SBV.proveWithAny thmSMTResults x
|
||||
SatQuery sn -> case sn of
|
||||
SomeSat 1 -> runProvers SBV.satWithAny satSMTResults
|
||||
_ -> runProver SBV.allSatWith allSatSMTResults
|
||||
SomeSat 1 -> runMultiProvers pc provers' SBV.satWithAny satSMTResults x
|
||||
_ -> runSingleProver pc provers' SBV.allSatWith allSatSMTResults x
|
||||
|
||||
|
||||
-- | Prepare a symbolic query by symbolically simulating the expression found in
|
||||
-- the @ProverQuery@. The result will either be an error or a list of the types
|
||||
-- of the symbolic inputs and the symbolic value to supply to the solver.
|
||||
--
|
||||
-- Note that the difference between sat and prove queries is reflected later
|
||||
-- in `runProver` where we call different SBV methods depending on the mode,
|
||||
-- so we do _not_ negate the goal here. Moreover, assumptions are added
|
||||
-- using conjunction for sat queries and implication for prove queries.
|
||||
--
|
||||
-- For safety properties, we want to add them as an additional goal
|
||||
-- when we do prove queries, and an additional assumption when we do
|
||||
-- sat queries. In both cases, the safety property is combined with
|
||||
-- the main goal via a conjunction.
|
||||
prepareQuery ::
|
||||
Eval.EvalOpts ->
|
||||
M.ModuleEnv ->
|
||||
ProverCommand ->
|
||||
IO (Either String ([FinType], SBV.Symbolic SBV.SVal))
|
||||
prepareQuery evo modEnv ProverCommand{..} =
|
||||
do let extDgs = M.allDeclGroups modEnv ++ pcExtraDecls
|
||||
|
||||
-- The `tyFn` creates variables that are treated as 'forall'
|
||||
-- or 'exists' bound, depending on the sort of query we are doing.
|
||||
let tyFn = case pcQueryType of
|
||||
SatQuery _ -> existsFinType
|
||||
ProveQuery -> forallFinType
|
||||
|
||||
-- The `addAsm` function is used to combine assumptions that
|
||||
-- arise from the types of symbolic variables (e.g. Z n values
|
||||
-- are assumed to be integers in the range `0 <= x < n`) with
|
||||
-- the main content of the query. We use conjunction or implication
|
||||
-- depending on the type of query.
|
||||
let addAsm = case pcQueryType of
|
||||
ProveQuery -> \x y -> SBV.svOr (SBV.svNot x) y
|
||||
SatQuery _ -> \x y -> SBV.svAnd x y
|
||||
|
||||
let ?evalPrim = evalPrim
|
||||
case predArgTypes pcSchema of
|
||||
Left msg -> return (Nothing, ProverError msg)
|
||||
Right ts -> do when pcVerbose $ lPutStrLn "Simulating..."
|
||||
(_,v) <- doSBVEval evo $
|
||||
do env <- Eval.evalDecls SBV extDgs mempty
|
||||
Eval.evalExpr SBV env pcExpr
|
||||
prims <- M.getPrimMap
|
||||
runRes <- runFn $ do
|
||||
Left msg -> return (Left msg)
|
||||
Right ts ->
|
||||
do when pcVerbose $ logPutStrLn (Eval.evalLogger evo) "Simulating..."
|
||||
pure $ Right $ (ts,
|
||||
do -- Compute the symbolic inputs, and any domain constraints needed
|
||||
-- according to their types.
|
||||
(args, asms) <- runWriterT (mapM tyFn ts)
|
||||
(_,b) <- doSBVEval evo (Eval.fromVBit <$>
|
||||
foldM Eval.fromVFun v (map pure args))
|
||||
return (foldr addAsm b asms)
|
||||
let (firstProver, results) = runRes
|
||||
esatexprs <- case results of
|
||||
-- Run the main symbolic computation. First we populate the
|
||||
-- evaluation environment, then we compute the value, finally
|
||||
-- we apply it to the symbolic inputs.
|
||||
(safety,b) <- doSBVEval evo $
|
||||
do env <- Eval.evalDecls SBV extDgs mempty
|
||||
v <- Eval.evalExpr SBV env pcExpr
|
||||
Eval.fromVBit <$> foldM Eval.fromVFun v (map pure args)
|
||||
return (foldr addAsm (SBV.svAnd safety b) asms))
|
||||
|
||||
|
||||
-- | Turn the SMT results from SBV into a @ProverResult@ that is ready for the Cryptol REPL.
|
||||
-- There may be more than one result if we made a multi-sat query.
|
||||
processResults ::
|
||||
Eval.EvalOpts ->
|
||||
ProverCommand ->
|
||||
[FinType] {- ^ Types of the symbolic inputs -} ->
|
||||
[SBV.SMTResult] {- ^ Results from the solver -} ->
|
||||
M.ModuleT IO ProverResult
|
||||
processResults evo ProverCommand{..} ts results =
|
||||
do let isSat = case pcQueryType of
|
||||
ProveQuery -> False
|
||||
SatQuery _ -> True
|
||||
|
||||
prims <- M.getPrimMap
|
||||
|
||||
case results of
|
||||
-- allSat can return more than one as long as
|
||||
-- they're satisfiable
|
||||
(SBV.Satisfiable {} : _) -> do
|
||||
@ -211,42 +289,58 @@ satProve ProverCommand {..} =
|
||||
panic "Cryptol.Symbolic.sat"
|
||||
[ "unable to make assignment into expression" ]
|
||||
Just tevs -> return $ tevs
|
||||
|
||||
-- prove returns only one
|
||||
[SBV.Unsatisfiable {}] ->
|
||||
return $ ThmResult (unFinType <$> ts)
|
||||
|
||||
-- unsat returns empty
|
||||
[] -> return $ ThmResult (unFinType <$> ts)
|
||||
|
||||
-- otherwise something is wrong
|
||||
_ -> return $ ProverError (rshow results)
|
||||
where rshow | isSat = show . SBV.AllSatResult . (False,False,False,)
|
||||
| otherwise = show . SBV.ThmResult . head
|
||||
|
||||
-- | Execute a symbolic ':prove' or ':sat' command.
|
||||
--
|
||||
-- This command returns a pair: the first element is the name of the
|
||||
-- solver that completes the given query (if any) along with the result
|
||||
-- of executing the query.
|
||||
satProve :: ProverCommand -> M.ModuleCmd (Maybe String, ProverResult)
|
||||
satProve pc@ProverCommand {..} =
|
||||
protectStack proverError $ \(evo,modEnv) ->
|
||||
|
||||
M.runModuleM (evo,modEnv) $ do
|
||||
|
||||
M.io (prepareQuery evo modEnv pc) >>= \case
|
||||
Left msg -> return (Nothing, ProverError msg)
|
||||
Right (ts, q) ->
|
||||
do (firstProver, results) <- runProver pc q
|
||||
esatexprs <- processResults evo pc ts results
|
||||
return (firstProver, esatexprs)
|
||||
|
||||
-- | Execute a symbolic ':prove' or ':sat' command when the prover is
|
||||
-- set to offline. This only prepares the SMT input file for the
|
||||
-- solver and does not actually invoke the solver.
|
||||
--
|
||||
-- This method returns either an error message or the text of
|
||||
-- the SMT input file corresponding to the given prover command.
|
||||
satProveOffline :: ProverCommand -> M.ModuleCmd (Either String String)
|
||||
satProveOffline ProverCommand {..} =
|
||||
satProveOffline pc@ProverCommand {..} =
|
||||
protectStack (\msg (_,modEnv) -> return (Right (Left msg, modEnv), [])) $
|
||||
\(evOpts,modEnv) -> do
|
||||
let isSat = case pcQueryType of
|
||||
ProveQuery -> False
|
||||
SatQuery _ -> True
|
||||
let extDgs = M.allDeclGroups modEnv ++ pcExtraDecls
|
||||
let tyFn = if isSat then existsFinType else forallFinType
|
||||
let addAsm = if isSat then SBV.svAnd else \x y -> SBV.svOr (SBV.svNot x) y
|
||||
let ?evalPrim = evalPrim
|
||||
case predArgTypes pcSchema of
|
||||
|
||||
prepareQuery evOpts modEnv pc >>= \case
|
||||
Left msg -> return (Right (Left msg, modEnv), [])
|
||||
Right ts ->
|
||||
do when pcVerbose $ logPutStrLn (Eval.evalLogger evOpts) "Simulating..."
|
||||
(_,v) <- doSBVEval evOpts $
|
||||
do env <- Eval.evalDecls SBV extDgs mempty
|
||||
Eval.evalExpr SBV env pcExpr
|
||||
smtlib <- SBV.generateSMTBenchmark isSat $ do
|
||||
(args, asms) <- runWriterT (mapM tyFn ts)
|
||||
(_,b) <- doSBVEval evOpts
|
||||
(Eval.fromVBit <$> foldM Eval.fromVFun v (map pure args))
|
||||
return (foldr addAsm b asms)
|
||||
Right (_ts, q) ->
|
||||
do smtlib <- SBV.generateSMTBenchmark isSat q
|
||||
return (Right (Right smtlib, modEnv), [])
|
||||
|
||||
|
||||
protectStack :: (String -> M.ModuleCmd a)
|
||||
-> M.ModuleCmd a
|
||||
-> M.ModuleCmd a
|
||||
@ -257,12 +351,18 @@ protectStack mkErr cmd modEnv =
|
||||
msg = "Symbolic evaluation failed to terminate."
|
||||
handler () = mkErr msg modEnv
|
||||
|
||||
-- | Given concrete values from the solver and a collection of finite types,
|
||||
-- reconstruct Cryptol concrete values, and return any unused solver
|
||||
-- values.
|
||||
parseValues :: [FinType] -> [SBV.CV] -> ([Concrete.Value], [SBV.CV])
|
||||
parseValues [] cvs = ([], cvs)
|
||||
parseValues (t : ts) cvs = (v : vs, cvs'')
|
||||
where (v, cvs') = parseValue t cvs
|
||||
(vs, cvs'') = parseValues ts cvs'
|
||||
|
||||
-- | Parse a single value of a finite type by consuming some number of
|
||||
-- solver values. The parsed Cryptol values is returned along with
|
||||
-- any solver values not consumed.
|
||||
parseValue :: FinType -> [SBV.CV] -> (Concrete.Value, [SBV.CV])
|
||||
parseValue FTBit [] = panic "Cryptol.Symbolic.parseValue" [ "empty FTBit" ]
|
||||
parseValue FTBit (cv : cvs) = (Eval.VBit (SBV.cvToBool cv), cvs)
|
||||
|
@ -324,7 +324,7 @@ instantiateExpr :: [Type] -> Int -> Expr -> SpecM Expr
|
||||
instantiateExpr [] 0 e = return e
|
||||
instantiateExpr [] n (EProofAbs _ e) = instantiateExpr [] (n - 1) e
|
||||
instantiateExpr (t : ts) n (ETAbs param e) =
|
||||
instantiateExpr ts n (apSubst (singleSubst (tpVar param) t) e)
|
||||
instantiateExpr ts n (apSubst (singleTParamSubst param t) e)
|
||||
instantiateExpr _ _ _ = fail "instantiateExpr: wrong number of type/proof arguments"
|
||||
|
||||
|
||||
|
@ -9,7 +9,7 @@ import Control.Monad(guard)
|
||||
import Cryptol.TypeCheck.Type
|
||||
import Cryptol.TypeCheck.SimpType(tMax,tWidth)
|
||||
import Cryptol.TypeCheck.Error(Warning(..))
|
||||
import Cryptol.TypeCheck.Subst(Subst,apSubst,listSubst,substBinds,singleSubst)
|
||||
import Cryptol.TypeCheck.Subst(Subst,apSubst,listSubst,substBinds,uncheckedSingleSubst)
|
||||
import Cryptol.TypeCheck.InferTypes(Goal,goal,Goals(..),goalsFromList)
|
||||
import Cryptol.TypeCheck.Solver.SMT(Solver,tryGetModel,shrinkModel)
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
@ -152,7 +152,7 @@ improveByDefaultingWithPure as ps =
|
||||
let ty = case ts of
|
||||
[] -> tNum (0::Int)
|
||||
_ -> foldr1 tMax ts
|
||||
su1 = singleSubst x ty
|
||||
su1 = uncheckedSingleSubst x ty
|
||||
in ( (x,ty) : [ (y,apSubst su1 t) | (y,t) <- yes ]
|
||||
, no -- We know that `x` does not appear here
|
||||
, otherFree -- We know that `x` did not appear here either
|
||||
|
@ -550,13 +550,7 @@ extendSubst su =
|
||||
, "Type: " ++ show (pp ty)
|
||||
]
|
||||
TVFree _ _ tvs _ ->
|
||||
do let bounds tv =
|
||||
case tv of
|
||||
TVBound tp -> Set.singleton tp
|
||||
TVFree _ _ tps _ -> tps
|
||||
let vars = Set.unions (map bounds (Set.elems (fvs ty)))
|
||||
-- (Set.filter isBoundTV (fvs ty))
|
||||
let escaped = Set.difference vars tvs
|
||||
do let escaped = Set.difference (freeParams ty) tvs
|
||||
if Set.null escaped then return () else
|
||||
panic "Cryptol.TypeCheck.Monad.extendSubst"
|
||||
[ "Escaped quantified variables:"
|
||||
|
@ -17,7 +17,7 @@ module Cryptol.TypeCheck.Sanity
|
||||
|
||||
import Cryptol.Parser.Position(thing)
|
||||
import Cryptol.TypeCheck.AST
|
||||
import Cryptol.TypeCheck.Subst (apSubst, singleSubst)
|
||||
import Cryptol.TypeCheck.Subst (apSubst, singleTParamSubst)
|
||||
import Cryptol.TypeCheck.Monad(InferInput(..))
|
||||
import Cryptol.Utils.Ident
|
||||
|
||||
@ -221,7 +221,7 @@ exprSchema expr =
|
||||
let k' = kindOf a
|
||||
unless (k == k') $ reportError $ KindMismatch k' k
|
||||
|
||||
let su = singleSubst (tpVar a) t
|
||||
let su = singleTParamSubst a t
|
||||
return $ Forall as (apSubst su ps) (apSubst su t1)
|
||||
|
||||
Forall [] _ _ -> reportError BadInstantiation
|
||||
|
@ -51,7 +51,7 @@ improveLit impSkol prop =
|
||||
(_,b) <- aSeq t
|
||||
a <- aTVar b
|
||||
unless impSkol $ guard (isFreeTV a)
|
||||
let su = singleSubst a tBit
|
||||
let su = uncheckedSingleSubst a tBit
|
||||
return (su, [])
|
||||
|
||||
|
||||
@ -66,13 +66,15 @@ improveEq impSkol fins prop =
|
||||
where
|
||||
rewrite this other =
|
||||
do x <- aTVar this
|
||||
guard (considerVar x && x `Set.notMember` fvs other)
|
||||
return (singleSubst x other, [])
|
||||
guard (considerVar x)
|
||||
case singleSubst x other of
|
||||
Left _ -> mzero
|
||||
Right su -> return (su, [])
|
||||
<|>
|
||||
do (v,s) <- isSum this
|
||||
guard (v `Set.notMember` fvs other)
|
||||
return (singleSubst v (Mk.tSub other s), [ other >== s ])
|
||||
|
||||
case singleSubst v (Mk.tSub other s) of
|
||||
Left _ -> mzero
|
||||
Right su -> return (su, [ other >== s ])
|
||||
|
||||
isSum t = do (v,s) <- matches t (anAdd, aTVar, __)
|
||||
valid v s
|
||||
|
@ -14,7 +14,10 @@
|
||||
module Cryptol.TypeCheck.Subst
|
||||
( Subst
|
||||
, emptySubst
|
||||
, SubstError(..)
|
||||
, singleSubst
|
||||
, singleTParamSubst
|
||||
, uncheckedSingleSubst
|
||||
, (@@)
|
||||
, defaultingSubst
|
||||
, listSubst
|
||||
@ -47,12 +50,22 @@ import Cryptol.Utils.Misc(anyJust)
|
||||
-- | A 'Subst' value represents a substitution that maps each 'TVar'
|
||||
-- to a 'Type'.
|
||||
--
|
||||
-- Invariant: If there is a mapping from @TVFree _ _ tps _@ to a type
|
||||
-- @t@, then @t@ must not mention (directly or indirectly) any type
|
||||
-- parameter that is not in @tps@. In particular, if @t@ contains a
|
||||
-- variable @TVFree _ _ tps2 _@, then @tps2@ must be a subset of
|
||||
-- Invariant 1: If there is a mapping from @TVFree _ _ tps _@ to a
|
||||
-- type @t@, then @t@ must not mention (directly or indirectly) any
|
||||
-- type parameter that is not in @tps@. In particular, if @t@ contains
|
||||
-- a variable @TVFree _ _ tps2 _@, then @tps2@ must be a subset of
|
||||
-- @tps@. This ensures that applying the substitution will not permit
|
||||
-- any type parameter to escape from its scope.
|
||||
--
|
||||
-- Invariant 2: The substitution must be idempotent, in that applying
|
||||
-- a substitution to any 'Type' in the map should leave that 'Type'
|
||||
-- unchanged. In other words, 'Type' values in the range of a 'Subst'
|
||||
-- should not mention any 'TVar' in the domain of the 'Subst'. In
|
||||
-- particular, this implies that a substitution must not contain any
|
||||
-- recursive variable mappings.
|
||||
--
|
||||
-- Invariant 3: The substitution must be kind correct: Each 'TVar' in
|
||||
-- the substitution must map to a 'Type' of the same kind.
|
||||
|
||||
data Subst = S { suFreeMap :: !(IntMap.IntMap (TVar, Type))
|
||||
, suBoundMap :: !(IntMap.IntMap (TVar, Type))
|
||||
@ -67,18 +80,42 @@ emptySubst =
|
||||
, suDefaulting = False
|
||||
}
|
||||
|
||||
singleSubst :: TVar -> Type -> Subst
|
||||
singleSubst v@(TVFree i _ _tps _) t =
|
||||
-- | Reasons to reject a single-variable substitution.
|
||||
data SubstError
|
||||
= SubstRecursive
|
||||
-- ^ 'TVar' maps to a type containing the same variable.
|
||||
| SubstEscaped [TParam]
|
||||
-- ^ 'TVar' maps to a type containing one or more out-of-scope bound variables.
|
||||
| SubstKindMismatch Kind Kind
|
||||
-- ^ 'TVar' maps to a type with a different kind.
|
||||
|
||||
singleSubst :: TVar -> Type -> Either SubstError Subst
|
||||
singleSubst x t
|
||||
| kindOf x /= kindOf t = Left (SubstKindMismatch (kindOf x) (kindOf t))
|
||||
| x `Set.member` fvs t = Left SubstRecursive
|
||||
| not (Set.null escaped) = Left (SubstEscaped (Set.toList escaped))
|
||||
| otherwise = Right (uncheckedSingleSubst x t)
|
||||
where
|
||||
escaped =
|
||||
case x of
|
||||
TVBound _ -> Set.empty
|
||||
TVFree _ _ scope _ -> freeParams t `Set.difference` scope
|
||||
|
||||
uncheckedSingleSubst :: TVar -> Type -> Subst
|
||||
uncheckedSingleSubst v@(TVFree i _ _tps _) t =
|
||||
S { suFreeMap = IntMap.singleton i (v, t)
|
||||
, suBoundMap = IntMap.empty
|
||||
, suDefaulting = False
|
||||
}
|
||||
singleSubst v@(TVBound tp) t =
|
||||
uncheckedSingleSubst v@(TVBound tp) t =
|
||||
S { suFreeMap = IntMap.empty
|
||||
, suBoundMap = IntMap.singleton (tpUnique tp) (v, t)
|
||||
, suDefaulting = False
|
||||
}
|
||||
|
||||
singleTParamSubst :: TParam -> Type -> Subst
|
||||
singleTParamSubst tp t = uncheckedSingleSubst (TVBound tp) t
|
||||
|
||||
(@@) :: Subst -> Subst -> Subst
|
||||
s2 @@ s1
|
||||
| isEmptySubst s2 =
|
||||
@ -327,4 +364,3 @@ instance TVars DeclDef where
|
||||
|
||||
instance TVars Module where
|
||||
apSubst su m = m { mDecls = apSubst su (mDecls m) }
|
||||
|
||||
|
@ -677,6 +677,12 @@ pError msg = TCon (TError KProp msg) []
|
||||
noFreeVariables :: FVS t => t -> Bool
|
||||
noFreeVariables = all (not . isFreeTV) . Set.toList . fvs
|
||||
|
||||
freeParams :: FVS t => t -> Set TParam
|
||||
freeParams x = Set.unions (map params (Set.toList (fvs x)))
|
||||
where
|
||||
params (TVFree _ _ tps _) = tps
|
||||
params (TVBound tp) = Set.singleton tp
|
||||
|
||||
class FVS t where
|
||||
fvs :: t -> Set TVar
|
||||
|
||||
@ -827,9 +833,10 @@ instance PP (WithNames Type) where
|
||||
(PEqual, [t1,t2]) -> go 0 t1 <+> text "==" <+> go 0 t2
|
||||
(PNeq , [t1,t2]) -> go 0 t1 <+> text "!=" <+> go 0 t2
|
||||
(PGeq, [t1,t2]) -> go 0 t1 <+> text ">=" <+> go 0 t2
|
||||
(PFin, [t1]) -> text "fin" <+> (go 4 t1)
|
||||
(PFin, [t1]) -> optParens (prec > 3) $ text "fin" <+> (go 4 t1)
|
||||
(PHas x, [t1,t2]) -> ppSelector x <+> text "of"
|
||||
<+> go 0 t1 <+> text "is" <+> go 0 t2
|
||||
(PAnd, [t1,t2]) -> parens (commaSep (map (go 0) (t1 : pSplitAnd t2)))
|
||||
|
||||
(PRing, [t1]) -> pp pc <+> go 4 t1
|
||||
(PField, [t1]) -> pp pc <+> go 4 t1
|
||||
@ -840,7 +847,7 @@ instance PP (WithNames Type) where
|
||||
(PSignedCmp, [t1]) -> pp pc <+> go 4 t1
|
||||
(PLiteral, [t1,t2]) -> pp pc <+> go 4 t1 <+> go 4 t2
|
||||
|
||||
(_, _) -> pp pc <+> fsep (map (go 4) ts)
|
||||
(_, _) -> optParens (prec > 3) $ pp pc <+> fsep (map (go 4) ts)
|
||||
|
||||
TCon f ts -> optParens (prec > 3)
|
||||
$ pp f <+> fsep (map (go 4) ts)
|
||||
|
@ -68,7 +68,7 @@ fastSchemaOf tyenv expr =
|
||||
ETApp e t -> case fastSchemaOf tyenv e of
|
||||
Forall (tparam : tparams) props ty
|
||||
-> Forall tparams (map (plainSubst s) props) (plainSubst s ty)
|
||||
where s = singleSubst (tpVar tparam) t
|
||||
where s = singleTParamSubst tparam t
|
||||
_ -> panic "Cryptol.TypeCheck.TypeOf.fastSchemaOf"
|
||||
[ "ETApp body with no type parameters" ]
|
||||
-- When calling 'fastSchemaOf' on a
|
||||
|
@ -110,22 +110,21 @@ bindVar v@(TVBound {}) t
|
||||
| otherwise = uniError $ UniKindMismatch k (kindOf t)
|
||||
where k = kindOf v
|
||||
|
||||
bindVar x@(TVFree _ _ xscope _) (TVar y@(TVFree _ _ yscope _))
|
||||
| xscope `Set.isProperSubsetOf` yscope = return (singleSubst y (TVar x), [])
|
||||
bindVar x@(TVFree _ xk xscope _) (tNoUser -> TVar y@(TVFree _ yk yscope _))
|
||||
| xscope `Set.isProperSubsetOf` yscope, xk == yk =
|
||||
return (uncheckedSingleSubst y (TVar x), [])
|
||||
-- In this case, we can add the reverse binding y ~> x to the
|
||||
-- substitution, but the instantiation x ~> y would be forbidden
|
||||
-- because it would allow y to escape from its scope.
|
||||
|
||||
bindVar x@(TVFree _ k inScope _d) t
|
||||
| not (k == kindOf t) = uniError $ UniKindMismatch k (kindOf t)
|
||||
| recTy && k == KType = uniError $ UniRecursive x t
|
||||
| not (Set.null escaped) = uniError $ UniNonPolyDepends x $ Set.toList escaped
|
||||
| recTy = return (emptySubst, [TVar x =#= t])
|
||||
| otherwise = return (singleSubst x t, [])
|
||||
where
|
||||
escaped = freeParams t `Set.difference` inScope
|
||||
recTy = x `Set.member` fvs t
|
||||
|
||||
|
||||
freeParams :: FVS t => t -> Set.Set TParam
|
||||
freeParams x = Set.unions (map params (Set.toList (fvs x)))
|
||||
where
|
||||
params (TVFree _ _ tps _) = tps
|
||||
params (TVBound tp) = Set.singleton tp
|
||||
bindVar x t =
|
||||
case singleSubst x t of
|
||||
Left SubstRecursive
|
||||
| kindOf x == KType -> uniError $ UniRecursive x t
|
||||
| otherwise -> return (emptySubst, [TVar x =#= t])
|
||||
Left (SubstEscaped tps) ->
|
||||
uniError $ UniNonPolyDepends x tps
|
||||
Left (SubstKindMismatch k1 k2) ->
|
||||
uniError $ UniKindMismatch k1 k2
|
||||
Right su ->
|
||||
return (su, [])
|
||||
|
@ -4,10 +4,12 @@ it : {result : Bit, arg1 : [4]}
|
||||
|
||||
Run-time error: no counterexample available
|
||||
True
|
||||
Counterexample
|
||||
f 0xc = False
|
||||
it : {result : Bit, arg1 : [4]}
|
||||
{arg1 = 0xc, result = False}
|
||||
False
|
||||
Satisfiable
|
||||
f 0x3 = True
|
||||
it : {result : Bit, arg1 : [4]}
|
||||
{arg1 = 0x3, result = True}
|
||||
@ -16,17 +18,21 @@ Unsatisfiable
|
||||
it : {result : Bit, arg1 : [4]}
|
||||
|
||||
Run-time error: no satisfying assignment available
|
||||
Counterexample
|
||||
g {x = 0xffffffff, y = 0x00000000} = False
|
||||
it : {result : Bit, arg1 : {x : [32], y : [32]}}
|
||||
{arg1 = {x = 0xffffffff, y = 0x00000000}, result = False}
|
||||
Satisfiable
|
||||
g {x = 0x00000000, y = 0x00000000} = True
|
||||
it : {result : Bit, arg1 : {x : [32], y : [32]}}
|
||||
{arg1 = {x = 0x00000000, y = 0x00000000}, result = True}
|
||||
Counterexample
|
||||
h 0x00 0x00 = False
|
||||
it : {result : Bit, arg1 : [8], arg2 : [8]}
|
||||
{arg1 = 0x00, arg2 = 0x00, result = False}
|
||||
0x00
|
||||
0x00
|
||||
Satisfiable
|
||||
h 0x00 0x01 = True
|
||||
it : {result : Bit, arg1 : [8], arg2 : [8]}
|
||||
{arg1 = 0x00, arg2 = 0x01, result = True}
|
||||
|
@ -1,6 +1,9 @@
|
||||
Loading module Cryptol
|
||||
Satisfiable
|
||||
it : {result : Bit, arg1 : [4]}
|
||||
Satisfiable
|
||||
it : [11]{result : Bit, arg1 : [4]}
|
||||
must be an integer > 0 or "all"
|
||||
must be an integer > 0 or "all"
|
||||
Satisfiable
|
||||
it : [3]{result : Bit, arg1 : [4]}
|
||||
|
@ -19,12 +19,16 @@ Testing... f0 = False
|
||||
:prove t2
|
||||
Q.E.D.
|
||||
:prove f0
|
||||
Counterexample
|
||||
f0 = False
|
||||
:sat t0
|
||||
Satisfiable
|
||||
t0 = True
|
||||
:sat t1
|
||||
Satisfiable
|
||||
t1 0x00000000 = True
|
||||
:sat t2
|
||||
Satisfiable
|
||||
t2 0xfffffffe 0xffffffff = True
|
||||
:sat f0
|
||||
Unsatisfiable
|
||||
|
@ -1,3 +1,4 @@
|
||||
Loading module Cryptol
|
||||
Satisfiable
|
||||
(\(x : Bit) (y : Bit) -> x < y) False True = True
|
||||
Q.E.D.
|
||||
|
@ -1,4 +1,5 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
Satisfiable
|
||||
(\(e : [64]) -> (e @@ [8 .. 24]) != zero) 0x00feff8000000000 = True
|
||||
|
@ -3,6 +3,7 @@ Loading module Cryptol
|
||||
[False, False, False, False, True, ...],
|
||||
[False, False, True, True, False, ...],
|
||||
[False, True, False, True, False, ...]]
|
||||
Counterexample
|
||||
(\(x : [4]) -> (transpose [x ...]) @ 0 @ 0 == False) 0x8 = False
|
||||
Q.E.D.
|
||||
Q.E.D.
|
||||
|
@ -1,2 +1,3 @@
|
||||
Loading module Cryptol
|
||||
Satisfiable
|
||||
(\x -> mapped x == 'N') 0x41 = True
|
||||
|
@ -1,5 +1,7 @@
|
||||
Loading module Cryptol
|
||||
Satisfiable
|
||||
(\(x : {b : Bit, a : Bit}) -> x.a && x.b)
|
||||
{a = True, b = True} = True
|
||||
Satisfiable
|
||||
(\(x : {b : [8], a : Bit}) -> x.b == 0 /\ x.a)
|
||||
{a = True, b = 0x00} = True
|
||||
|
7
tests/issues/issue723.cry
Normal file
7
tests/issues/issue723.cry
Normal file
@ -0,0 +1,7 @@
|
||||
f : {n} (fin n) => [n] -> [n]
|
||||
f x = g x
|
||||
where
|
||||
m1 = zero # x
|
||||
|
||||
g : {k} (fin k) => [k] -> [k]
|
||||
g m0 = m0 ^ m1
|
1
tests/issues/issue723.icry
Normal file
1
tests/issues/issue723.icry
Normal file
@ -0,0 +1 @@
|
||||
:l issue723.cry
|
20
tests/issues/issue723.icry.stdout
Normal file
20
tests/issues/issue723.icry.stdout
Normal file
@ -0,0 +1,20 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
[warning] at issue723.cry:4:10--4:18:
|
||||
Defaulting type argument 'front' of '(#)' to 0
|
||||
|
||||
[error] at issue723.cry:7:5--7:19:
|
||||
Failed to validate user-specified signature.
|
||||
in the definition of 'Main::g', at issue723.cry:7:5--7:6,
|
||||
we need to show that
|
||||
for any type k
|
||||
assuming
|
||||
• fin k
|
||||
the following constraints hold:
|
||||
• k >= n`908
|
||||
arising from
|
||||
matching types
|
||||
at issue723.cry:7:17--7:19
|
||||
where
|
||||
n`908 is signature variable 'n' at issue723.cry:1:6--1:7
|
14
tests/issues/issue725.icry
Normal file
14
tests/issues/issue725.icry
Normal file
@ -0,0 +1,14 @@
|
||||
:set show-examples = no
|
||||
:set prover-stats=no
|
||||
|
||||
:set prover=z3
|
||||
|
||||
:prove \(n:Integer, p : Bit) -> p ==> (x != x where x = 2 ^^ n)
|
||||
:sat \(a:[8], b:[8]) -> a == ~zero /\ a@b == False
|
||||
:prove \(a:[8], b:[8]) -> a == zero ==> a@b == False
|
||||
|
||||
:set prover=w4-z3
|
||||
|
||||
:prove \(n:Integer, p : Bit) -> p ==> (x != x where x = 2 ^^ n)
|
||||
:sat \(a:[8], b:[8]) -> a == ~zero /\ a@b == False
|
||||
:prove \(a:[8], b:[8]) -> a == zero ==> a@b == False
|
9
tests/issues/issue725.icry.stdout
Normal file
9
tests/issues/issue725.icry.stdout
Normal file
@ -0,0 +1,9 @@
|
||||
Loading module Cryptol
|
||||
|
||||
operation can not be supported on symbolic values: integer exponentiation
|
||||
Unsatisfiable
|
||||
Counterexample
|
||||
|
||||
operation can not be supported on symbolic values: integer exponentiation
|
||||
Unsatisfiable
|
||||
Counterexample
|
7
tests/issues/issue731.cry
Normal file
7
tests/issues/issue731.cry
Normal file
@ -0,0 +1,7 @@
|
||||
type constraint T n = (fin n, n >= 1)
|
||||
|
||||
type constraint Both p q = (p, q)
|
||||
|
||||
type constraint Fin2 i j = Both (fin i) (fin j)
|
||||
|
||||
type constraint i <=> j = (i <= j, i >= j)
|
2
tests/issues/issue731.icry
Normal file
2
tests/issues/issue731.icry
Normal file
@ -0,0 +1,2 @@
|
||||
:l issue731.cry
|
||||
:browse Main
|
14
tests/issues/issue731.icry.stdout
Normal file
14
tests/issues/issue731.icry.stdout
Normal file
@ -0,0 +1,14 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
Constraint Synonyms
|
||||
===================
|
||||
|
||||
Public
|
||||
------
|
||||
|
||||
type constraint (<=>) i j = (i <= j, i >= j)
|
||||
type constraint Both p q = (p, q)
|
||||
type constraint Fin2 i j = Both (fin i) (fin j)
|
||||
type constraint T n = (fin n, n >= 1)
|
||||
|
@ -2,5 +2,6 @@ Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
Q.E.D.
|
||||
Counterexample
|
||||
av1 0xfdffffe0 0x7fffffe0 = False
|
||||
Q.E.D.
|
||||
|
@ -1,4 +1,6 @@
|
||||
Loading module Cryptol
|
||||
Loading module r03
|
||||
Satisfiable
|
||||
True
|
||||
Counterexample
|
||||
False
|
||||
|
Loading…
Reference in New Issue
Block a user