cryptol-2.11.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

data ProverCommand Source #

Constructors

ProverCommand 

Fields

data QueryType Source #

Instances

Instances details
Show QueryType Source # 
Instance details

Defined in Cryptol.Symbolic

data SatNum Source #

Constructors

AllSat 
SomeSat Int 

Instances

Instances details
Show SatNum Source # 
Instance details

Defined in Cryptol.Symbolic

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.

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.

FinType

VarShape

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

data FreshVarFns sym Source #

Constructors

FreshVarFns 

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 #