cryptol-2.6.0: Cryptol: The Language of Cryptography

Copyright(c) 2013-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellNone
LanguageHaskell2010

Cryptol.Symbolic

Description

 
Synopsis

Documentation

type EvalEnv = GenEvalEnv SBool SWord Source #

proverConfigs :: [(String, SMTConfig)] Source #

proverNames :: [String] Source #

lookupProver :: String -> SMTConfig Source #

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

data SatNum Source #

Constructors

AllSat 
SomeSat Int 
Instances
Show SatNum Source # 
Instance details

Defined in Cryptol.Symbolic

Methods

showsPrec :: Int -> SatNum -> ShowS #

show :: SatNum -> String #

showList :: [SatNum] -> ShowS #

data QueryType Source #

Constructors

SatQuery SatNum 
ProveQuery 
Instances
Show QueryType Source # 
Instance details

Defined in Cryptol.Symbolic

Methods

showsPrec :: Int -> QueryType -> ShowS #

show :: QueryType -> String #

showList :: [QueryType] -> ShowS #

data ProverCommand Source #

Constructors

ProverCommand 

Fields

type ProverStats = NominalDiffTime Source #

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 [Type] 
EmptyResult 
ProverError String 

satSMTResults :: SatResult -> [SMTResult] Source #

allSatSMTResults :: AllSatResult -> [SMTResult] Source #

thmSMTResults :: ThmResult -> [SMTResult] Source #

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

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

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

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

parseValues :: [FinType] -> [CW] -> ([Value], [CW]) Source #

parseValue :: FinType -> [CW] -> (Value, [CW]) Source #

allDeclGroups :: ModuleEnv -> [DeclGroup] Source #

data FinType Source #

Constructors

FTBit 
FTInteger 
FTIntMod Integer 
FTSeq Int FinType 
FTTuple [FinType] 
FTRecord [(Ident, FinType)] 

numType :: Integer -> Maybe Int Source #

finType :: TValue -> Maybe FinType Source #

unFinType :: FinType -> Type Source #

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

inBoundsIntMod :: Integer -> SInteger -> SBool Source #

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

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