Cryptol.Symbolic

Documentation

data ProverCommand

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

Constructors

SatQuery SatNum

ProveQuery

SafetyQuery

Instances

Show QueryType

Defined in Cryptol.Symbolic

Methods

showsPrec :: Int -> QueryType -> ShowS

show :: QueryType -> String

showList :: [QueryType] -> ShowS

data SatNum

Constructors

AllSat

SomeSat Int

Instances

Show SatNum

Defined in Cryptol.Symbolic

Methods

showsPrec :: Int -> SatNum -> ShowS

show :: SatNum -> String

showList :: [SatNum] -> ShowS

data ProverResult

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 [Type]

CounterExample CounterExampleType SatResult

EmptyResult

ProverError String

type ProverStats = NominalDiffTime

data CounterExampleType

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

Constructors

FTBit

FTInteger

FTIntMod Integer

FTRational

FTFloat Integer Integer

FTSeq Int FinType

FTTuple [FinType]

FTRecord (RecordMap Ident FinType)

finType :: TValue -> Maybe FinType

unFinType :: FinType -> Type

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

VarShape

data VarShape sym

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

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

computeModel :: PrimMap -> [FinType] -> [VarShape Concrete] -> [(Type, Expr, Value)]

data FreshVarFns sym

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)

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

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