Copyright	(c) 2013-2016 Galois Inc.
License	BSD3
Maintainer	cryptol@galois.com
Stability	provisional
Portability	portable
Safe Haskell	None
Language	Haskell2010

Cryptol.Symbolic

Contents

FinType
VarShape

Description

Synopsis

data ProverCommand = ProverCommand {
- pcQueryType :: QueryType
- pcProverName :: String
- pcVerbose :: Bool
- pcValidate :: Bool
- pcProverStats :: !(IORef ProverStats)
- pcExtraDecls :: [DeclGroup]
- pcSmtFile :: Maybe FilePath
- pcExpr :: Expr
- pcSchema :: Schema
- pcIgnoreSafety :: Bool
}
data QueryType
- = SatQuery SatNum
- | ProveQuery
- | SafetyQuery
data SatNum
- = AllSat
- | SomeSat Int
data ProverResult
- = AllSatResult [SatResult]
- | ThmResult [TValue]
- | CounterExample CounterExampleType SatResult
- | EmptyResult
- | ProverError String
type ProverStats = NominalDiffTime
data CounterExampleType
- = SafetyViolation
- | PredicateFalsified
data FinType
- = FTBit
- | FTInteger
- | FTIntMod Integer
- | FTRational
- | FTFloat Integer Integer
- | FTSeq Integer FinType
- | FTTuple [FinType]
- | FTRecord (RecordMap Ident FinType)
- | FTNewtype Newtype [Either Nat' TValue] (RecordMap Ident FinType)
finType :: TValue -> Maybe FinType
unFinType :: FinType -> TValue
predArgTypes :: QueryType -> Schema -> Either String [FinType]
data VarShape sym
- = VarBit (SBit sym)
- | VarInteger (SInteger sym)
- | VarRational (SInteger sym) (SInteger sym)
- | VarFloat (SFloat sym)
- | VarWord (SWord sym)
- | VarFinSeq Integer [VarShape sym]
- | VarTuple [VarShape sym]
- | VarRecord (RecordMap Ident (VarShape sym))
varShapeToValue :: Backend sym => sym -> VarShape sym -> GenValue sym
freshVar :: Backend sym => FreshVarFns sym -> FinType -> IO (VarShape sym)
computeModel :: PrimMap -> [FinType] -> [VarShape Concrete] -> [(TValue, Expr, Value)]
data FreshVarFns sym = FreshVarFns {
- freshBitVar :: IO (SBit sym)
- freshWordVar :: Integer -> IO (SWord sym)
- freshIntegerVar :: Maybe Integer -> Maybe Integer -> IO (SInteger sym)
- freshFloatVar :: Integer -> Integer -> IO (SFloat sym)
}
modelPred :: Backend sym => sym -> [VarShape sym] -> [VarShape Concrete] -> SEval sym (SBit sym)
varModelPred :: Backend sym => sym -> (VarShape sym, VarShape Concrete) -> SEval sym (SBit sym)
varToExpr :: PrimMap -> FinType -> VarShape Concrete -> Expr

Documentation

data ProverCommand Source #

Constructors

ProverCommand

Fields

pcQueryType :: QueryType
The type of query to run
pcProverName :: String
Which prover to use (one of the strings in proverConfigs)
pcVerbose :: Bool
Verbosity flag passed to SBV
pcValidate :: Bool
Model validation flag passed to SBV
pcProverStats :: !(IORef ProverStats)
Record timing information here
pcExtraDecls :: [DeclGroup]
Extra declarations to bring into scope for symbolic simulation
pcSmtFile :: Maybe FilePath
Optionally output the SMTLIB query to a file
pcExpr :: Expr
The typechecked expression to evaluate
pcSchema :: Schema
The Schema of pcExpr
pcIgnoreSafety :: Bool
Should we ignore safety predicates?

data QueryType Source #

Constructors

SatQuery SatNum
ProveQuery
SafetyQuery

Instances

Instances details

Show QueryType Source #
Instance details Defined in Cryptol.Symbolic Methods showsPrec :: Int -> QueryType -> ShowS # show :: QueryType -> String # showList :: [QueryType] -> ShowS #

data SatNum Source #

Constructors

AllSat
SomeSat Int

Instances

Instances details

Show SatNum Source #
Instance details Defined in Cryptol.Symbolic Methods showsPrec :: Int -> SatNum -> ShowS # show :: SatNum -> String # showList :: [SatNum] -> ShowS #

data ProverResult Source #

A prover result is either an error message, an empty result (eg for the offline prover), a counterexample or a lazy list of satisfying assignments.

Constructors

AllSatResult [SatResult]
ThmResult [TValue]
CounterExample CounterExampleType SatResult
EmptyResult
ProverError String

type ProverStats = NominalDiffTime Source #

data CounterExampleType Source #

A :prove command can fail either because some input causes the predicate to violate a safety assertion, or because the predicate returns false for some input.

Constructors

SafetyViolation
PredicateFalsified

FinType

data FinType Source #

Constructors

FTBit
FTInteger
FTIntMod Integer
FTRational
FTFloat Integer Integer
FTSeq Integer FinType
FTTuple [FinType]
FTRecord (RecordMap Ident FinType)
FTNewtype Newtype [Either Nat' TValue] (RecordMap Ident FinType)

finType :: TValue -> Maybe FinType Source #

unFinType :: FinType -> TValue Source #

predArgTypes :: QueryType -> Schema -> Either String [FinType] Source #

VarShape

data VarShape sym Source #

Constructors

VarBit (SBit sym)
VarInteger (SInteger sym)
VarRational (SInteger sym) (SInteger sym)
VarFloat (SFloat sym)
VarWord (SWord sym)
VarFinSeq Integer [VarShape sym]
VarTuple [VarShape sym]
VarRecord (RecordMap Ident (VarShape sym))

varShapeToValue :: Backend sym => sym -> VarShape sym -> GenValue sym Source #

freshVar :: Backend sym => FreshVarFns sym -> FinType -> IO (VarShape sym) Source #

computeModel :: PrimMap -> [FinType] -> [VarShape Concrete] -> [(TValue, Expr, Value)] Source #

data FreshVarFns sym Source #

Constructors

FreshVarFns
Fields freshBitVar :: IO (SBit sym) freshWordVar :: Integer -> IO (SWord sym) freshIntegerVar :: Maybe Integer -> Maybe Integer -> IO (SInteger sym) freshFloatVar :: Integer -> Integer -> IO (SFloat sym)

modelPred :: Backend sym => sym -> [VarShape sym] -> [VarShape Concrete] -> SEval sym (SBit sym) Source #

varModelPred :: Backend sym => sym -> (VarShape sym, VarShape Concrete) -> SEval sym (SBit sym) Source #

varToExpr :: PrimMap -> FinType -> VarShape Concrete -> Expr Source #