cryptol-2.2.6: Cryptol: The Language of Cryptography

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

Cryptol.Symbolic

Description

Synopsis

- smtMode :: SMTLibVersion
- 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
  - pcExtraDecls :: [DeclGroup]
  - pcSmtFile :: Maybe FilePath
  - pcExpr :: Expr
  - pcSchema :: Schema
  }
- data ProverResult
  - = AllSatResult [SatResult]
  - | ThmResult [Type]
  - | EmptyResult
  - | ProverError String
- satSMTResults :: SatResult -> [SMTResult]
- allSatSMTResults :: AllSatResult -> [SMTResult]
- thmSMTResults :: ThmResult -> [SMTResult]
- proverError :: String -> ModuleCmd ProverResult
- satProve :: ProverCommand -> ModuleCmd 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
  - | FTSeq Int FinType
  - | FTTuple [FinType]
  - | FTRecord [(Name, FinType)]
- numType :: Type -> Maybe Int
- finType :: Type -> Maybe FinType
- unFinType :: FinType -> Type
- predArgTypes :: Schema -> Either String [FinType]
- forallFinType :: FinType -> Symbolic Value
- existsFinType :: FinType -> Symbolic Value
- data Env = Env {
  - envVars :: Map QName Value
  - envTypes :: Map TVar TValue
  }
- emptyEnv :: Env
- bindVar :: (QName, Value) -> Env -> Env
- lookupVar :: QName -> Env -> Maybe Value
- bindType :: TVar -> TValue -> Env -> Env
- lookupType :: TVar -> Env -> Maybe TValue
- evalExpr :: Env -> Expr -> Value
- evalType :: Env -> Type -> TValue
- evalSel :: Selector -> Value -> Value
- evalDecls :: Env -> [DeclGroup] -> Env
- evalDeclGroup :: Env -> DeclGroup -> Env
- evalDecl :: Env -> Decl -> (QName, Value)
- copyBySchema :: Env -> Schema -> Value -> Value
- copyByType :: Env -> TValue -> Value -> Value
- evalComp :: Env -> TValue -> Expr -> [[Match]] -> Value
- branchEnvs :: Env -> [Match] -> [Env]
- evalMatch :: Env -> Match -> [Env]

# Documentation

smtMode :: SMTLibVersion 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 |

data QueryType Source

Constructors

SatQuery SatNum |
ProveQuery |

Instances

Show QueryType 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

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`

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 ProverResult Source

satProve :: ProverCommand -> ModuleCmd 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 |
FTSeq Int FinType |
FTTuple [FinType] |
FTRecord [(Name, FinType)] |

numType :: Type -> Maybe Int Source

finType :: Type -> Maybe FinType Source

unFinType :: FinType -> Type Source

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

forallFinType :: FinType -> Symbolic Value Source

existsFinType :: FinType -> Symbolic Value Source

data Env Source

Constructors

Env |

Fields

envVars :: Map QName Value
envTypes :: Map TVar TValue

Instances

Monoid Env Source |

emptyEnv :: Env Source

bindVar :: (QName, Value) -> Env -> Env Source

Bind a variable in the evaluation environment.

lookupVar :: QName -> Env -> Maybe Value Source

Lookup a variable in the environment.

bindType :: TVar -> TValue -> Env -> Env Source

Bind a type variable of kind *.

lookupType :: TVar -> Env -> Maybe TValue Source

Lookup a type variable.

evalExpr :: Env -> Expr -> Value Source

evalType :: Env -> Type -> TValue Source

evalSel :: Selector -> Value -> Value Source

evalDecls :: Env -> [DeclGroup] -> Env Source

evalDeclGroup :: Env -> DeclGroup -> Env Source

evalDecl :: Env -> Decl -> (QName, Value) Source

copyBySchema :: Env -> Schema -> Value -> Value Source

Make a copy of the given value, building the spine based only on the type without forcing the value argument. This lets us avoid strictness problems when evaluating recursive definitions.

copyByType :: Env -> TValue -> Value -> Value Source

evalComp :: Env -> TValue -> Expr -> [[Match]] -> Value Source

Evaluate a comprehension.

branchEnvs :: Env -> [Match] -> [Env] Source

Turn a list of matches into the final environments for each iteration of the branch.

evalMatch :: Env -> Match -> [Env] Source

Turn a match into the list of environments it represents.