cryptol-3.0.0: Cryptol: The Language of Cryptography

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

Cryptol.Symbolic

Contents

- FinType
- VarShape

Description

Synopsis

- data ProverCommand = ProverCommand {
  - pcQueryType :: QueryType
  - pcProverName :: String
  - pcVerbose :: Bool
  - pcValidate :: Bool
  - pcProverStats :: !(IORef ProverStats)
  - pcExtraDecls :: [DeclGroup]
  - pcSmtFile :: Maybe FilePath
  - pcExpr :: Expr
  - pcSchema :: Schema
  - pcIgnoreSafety :: Bool
  }
- data QueryType
  - = SatQuery SatNum
  - | ProveQuery
  - | SafetyQuery
- data SatNum
  - = AllSat
  - | SomeSat Int
- data ProverResult
  - = AllSatResult [SatResult]
  - | ThmResult [TValue]
  - | CounterExample CounterExampleType SatResult
  - | EmptyResult
  - | ProverError String
- type ProverStats = NominalDiffTime
- data CounterExampleType
  - = SafetyViolation
  - | PredicateFalsified
- data FinType
  - = FTBit
  - | FTInteger
  - | FTIntMod Integer
  - | FTRational
  - | FTFloat Integer Integer
  - | FTSeq Integer FinType
  - | FTTuple [FinType]
  - | FTRecord (RecordMap Ident FinType)
  - | FTNewtype Newtype [Either Nat' TValue] (RecordMap Ident FinType)
- finType :: TValue -> Maybe FinType
- unFinType :: FinType -> TValue
- predArgTypes :: QueryType -> Schema -> Either String [FinType]
- data VarShape sym
  - = VarBit (SBit sym)
  - | VarInteger (SInteger sym)
  - | VarRational (SInteger sym) (SInteger sym)
  - | VarFloat (SFloat sym)
  - | VarWord (SWord sym)
  - | VarFinSeq Integer [VarShape sym]
  - | VarTuple [VarShape sym]
  - | VarRecord (RecordMap Ident (VarShape sym))
- varShapeToValue :: Backend sym => sym -> VarShape sym -> GenValue sym
- freshVar :: Backend sym => FreshVarFns sym -> FinType -> IO (VarShape sym)
- computeModel :: PrimMap -> [FinType] -> [VarShape Concrete] -> [(TValue, Expr, Value)]
- data FreshVarFns sym = FreshVarFns {
  - freshBitVar :: IO (SBit sym)
  - freshWordVar :: Integer -> IO (SWord sym)
  - freshIntegerVar :: Maybe Integer -> Maybe Integer -> IO (SInteger sym)
  - freshFloatVar :: Integer -> Integer -> IO (SFloat sym)
  }
- modelPred :: Backend sym => sym -> [VarShape sym] -> [VarShape Concrete] -> SEval sym (SBit sym)
- varModelPred :: Backend sym => sym -> (VarShape sym, VarShape Concrete) -> SEval sym (SBit sym)
- varToExpr :: PrimMap -> FinType -> VarShape Concrete -> Expr
- flattenShape :: VarShape sym -> [VarShape sym] -> [VarShape sym]
- flattenShapes :: [VarShape sym] -> [VarShape sym] -> [VarShape sym]

# Documentation

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

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

- pcIgnoreSafety :: Bool

  Should we ignore safety predicates?

data QueryType Source #

Constructors

SatQuery SatNum |
ProveQuery |
SafetyQuery |

#### Instances

Instances details

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

data SatNum Source #

Constructors

AllSat |
SomeSat Int |

#### Instances

Instances details

Show SatNum Source # |
Instance details Defined in Cryptol.Symbolic Methods showsPrec :: Int -> SatNum -> ShowS Source # show :: SatNum -> String Source # showList :: [SatNum] -> ShowS 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 [TValue] |
CounterExample CounterExampleType SatResult |
EmptyResult |
ProverError String |

type ProverStats = NominalDiffTime Source #

data CounterExampleType Source #

A `:prove` command can fail either because some input causes the predicate to violate a safety assertion, or because the predicate returns false for some input.

Constructors

SafetyViolation |
PredicateFalsified |

# FinType

data FinType Source #

Constructors

FTBit |
FTInteger |
FTIntMod Integer |
FTRational |
FTFloat Integer Integer |
FTSeq Integer FinType |
FTTuple [FinType] |
FTRecord (RecordMap Ident FinType) |
FTNewtype Newtype [Either Nat' TValue] (RecordMap Ident FinType) |

finType :: TValue -> Maybe FinType Source #

unFinType :: FinType -> TValue Source #

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

# VarShape

data VarShape sym Source #

Constructors

VarBit (SBit sym) |
VarInteger (SInteger sym) |
VarRational (SInteger sym) (SInteger sym) |
VarFloat (SFloat sym) |
VarWord (SWord sym) |
VarFinSeq Integer [VarShape sym] |
VarTuple [VarShape sym] |
VarRecord (RecordMap Ident (VarShape sym)) |

varShapeToValue :: Backend sym => sym -> VarShape sym -> GenValue sym Source #

freshVar :: Backend sym => FreshVarFns sym -> FinType -> IO (VarShape sym) Source #

computeModel :: PrimMap -> [FinType] -> [VarShape Concrete] -> [(TValue, Expr, Value)] Source #

data FreshVarFns sym Source #

Constructors

FreshVarFns |

Fields

- freshBitVar :: IO (SBit sym)
- freshWordVar :: Integer -> IO (SWord sym)
- freshIntegerVar :: Maybe Integer -> Maybe Integer -> IO (SInteger sym)
- freshFloatVar :: Integer -> Integer -> IO (SFloat sym)

modelPred :: Backend sym => sym -> [VarShape sym] -> [VarShape Concrete] -> SEval sym (SBit sym) Source #

varModelPred :: Backend sym => sym -> (VarShape sym, VarShape Concrete) -> SEval sym (SBit sym) Source #

varToExpr :: PrimMap -> FinType -> VarShape Concrete -> Expr Source #

flattenShape :: VarShape sym -> [VarShape sym] -> [VarShape sym] Source #

flattenShapes :: [VarShape sym] -> [VarShape sym] -> [VarShape sym] Source #

Flatten structured shapes (like tuples and sequences), leaving only a sequence of variable shapes of base type.