cryptol-2.4.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 | Haskell98

Cryptol.Symbolic

Description

Synopsis

- 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 [(Ident, FinType)]
- numType :: Integer -> Maybe Int
- finType :: TValue -> Maybe FinType
- unFinType :: FinType -> Type
- predArgTypes :: Schema -> Either String [FinType]
- forallFinType :: FinType -> Symbolic Value
- existsFinType :: FinType -> Symbolic Value
- data Env = Env {
  - envVars :: Map Name Value
  - envTypes :: Map TVar (Either Nat' TValue)
  }
- bindVar :: (Name, Value) -> Env -> Env
- lookupVar :: Name -> Env -> Maybe Value
- bindType :: TVar -> Either Nat' TValue -> Env -> Env
- lookupType :: TVar -> Env -> Maybe (Either Nat' TValue)
- evalExpr :: Env -> Expr -> Value
- evalValType :: Env -> Type -> TValue
- evalNumType :: Env -> Type -> Nat'
- evalSel :: Selector -> Value -> Value
- evalDecls :: Env -> [DeclGroup] -> Env
- evalDeclGroup :: Env -> DeclGroup -> Env
- evalDecl :: Env -> Decl -> (Name, 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

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

data QueryType Source #

Constructors

SatQuery SatNum |
ProveQuery |

Instances

Show QueryType Source # |
Methods showsPrec :: Int -> QueryType -> ShowS # show :: QueryType -> String # showList :: [QueryType] -> ShowS #

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 [(Ident, FinType)] |

numType :: Integer -> Maybe Int Source #

finType :: TValue -> 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 Name Value
- envTypes :: Map TVar (Either Nat' TValue)

Instances

Monoid Env Source # |
Methods mempty :: Env # mappend :: Env -> Env -> Env # mconcat :: [Env] -> Env #

bindVar :: (Name, Value) -> Env -> Env Source #

Bind a variable in the evaluation environment.

lookupVar :: Name -> Env -> Maybe Value Source #

Lookup a variable in the environment.

bindType :: TVar -> Either Nat' TValue -> Env -> Env Source #

Bind a type variable of kind *.

lookupType :: TVar -> Env -> Maybe (Either Nat' TValue) Source #

Lookup a type variable.

evalExpr :: Env -> Expr -> Value Source #

evalValType :: Env -> Type -> TValue Source #

evalNumType :: Env -> Type -> Nat' Source #

evalSel :: Selector -> Value -> Value Source #

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

evalDeclGroup :: Env -> DeclGroup -> Env Source #

evalDecl :: Env -> Decl -> (Name, 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.