Cryptol.Symbolic

Documentation

type EvalEnv = GenEvalEnv SBool SWord

proverConfigs :: [(String, SMTConfig)]

proverNames :: [String]

lookupProver :: String -> SMTConfig

type SatResult = [(Type, Expr, Value)]

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 QueryType

Constructors

SatQuery SatNum

ProveQuery

Instances

Show QueryType

Defined in Cryptol.Symbolic

Methods

showsPrec :: Int -> QueryType -> ShowS

show :: QueryType -> String

showList :: [QueryType] -> ShowS

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

type ProverStats = NominalDiffTime

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]

EmptyResult

ProverError String

satSMTResults :: SatResult -> [SMTResult]

allSatSMTResults :: AllSatResult -> [SMTResult]

thmSMTResults :: ThmResult -> [SMTResult]

proverError :: String -> ModuleCmd (Maybe Solver, ProverResult)

satProve :: ProverCommand -> ModuleCmd (Maybe Solver, ProverResult)

satProveOffline :: ProverCommand -> ModuleCmd (Either String String)

protectStack :: (String -> ModuleCmd a) -> ModuleCmd a -> ModuleCmd a

parseValues :: [FinType] -> [CV] -> ([Value], [CV])

parseValue :: FinType -> [CV] -> (Value, [CV])

allDeclGroups :: ModuleEnv -> [DeclGroup]

data FinType

Constructors

FTBit

FTInteger

FTIntMod Integer

FTSeq Int FinType

FTTuple [FinType]

FTRecord [(Ident, FinType)]

numType :: Integer -> Maybe Int

finType :: TValue -> Maybe FinType

unFinType :: FinType -> Type

predArgTypes :: Schema -> Either String [FinType]

inBoundsIntMod :: Integer -> SInteger -> SBool

forallFinType :: FinType -> WriterT [SBool] Symbolic Value

existsFinType :: FinType -> WriterT [SBool] Symbolic Value