cryptol-2.6.0: Cryptol: The Language of Cryptography

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

Cryptol.Symbolic

Description

Synopsis

- type EvalEnv = GenEvalEnv SBool SWord
- proverConfigs :: [(String, SMTConfig)]
- proverNames :: [String]
- lookupProver :: String -> SMTConfig
- type SatResult = [(Type, Expr, Value)]
- data SatNum
  - = AllSat
  - | SomeSat Int
- data QueryType
  - = SatQuery SatNum
  - | ProveQuery
- data ProverCommand = ProverCommand {
  - pcQueryType :: QueryType
  - pcProverName :: String
  - pcVerbose :: Bool
  - pcProverStats :: !(IORef ProverStats)
  - pcExtraDecls :: [DeclGroup]
  - pcSmtFile :: Maybe FilePath
  - pcExpr :: Expr
  - pcSchema :: Schema
  }
- type ProverStats = NominalDiffTime
- data ProverResult
  - = 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] -> [CW] -> ([Value], [CW])
- parseValue :: FinType -> [CW] -> (Value, [CW])
- allDeclGroups :: ModuleEnv -> [DeclGroup]
- data FinType
  - = 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

# 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 Source # show :: SatNum -> String Source # showList :: [SatNum] -> ShowS Source #

data QueryType Source #

Constructors

SatQuery SatNum |
ProveQuery |

Instances

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

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

- 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 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 #