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.Eval.Value

Contents

- GenericValue
  - Value introduction operations
  - Value eliminators
  - Pretty printing
- Merge and ifthenelse

Description

Synopsis

- data GenValue sym
  - = VRecord !(RecordMap Ident (SEval sym (GenValue sym)))
  - | VTuple ![SEval sym (GenValue sym)]
  - | VBit !(SBit sym)
  - | VInteger !(SInteger sym)
  - | VRational !(SRational sym)
  - | VFloat !(SFloat sym)
  - | VSeq !Integer !(SeqMap sym (GenValue sym))
  - | VWord !Integer !(WordValue sym)
  - | VStream !(SeqMap sym (GenValue sym))
  - | VFun CallStack (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
  - | VPoly CallStack (TValue -> SEval sym (GenValue sym))
  - | VNumPoly CallStack (Nat' -> SEval sym (GenValue sym))
- forceValue :: Backend sym => GenValue sym -> SEval sym ()
- class MonadIO (SEval sym) => Backend sym where
  - type SBit sym :: Type
  - type SWord sym :: Type
  - type SInteger sym :: Type
  - type SFloat sym :: Type
  - type SEval sym :: Type -> Type
  - isReady :: sym -> SEval sym a -> SEval sym (Maybe a)
  - sDeclareHole :: sym -> String -> SEval sym (SEval sym a, SEval sym a -> SEval sym ())
  - sDelayFill :: sym -> SEval sym a -> Maybe (SEval sym a) -> String -> SEval sym (SEval sym a)
  - sSpark :: sym -> SEval sym a -> SEval sym (SEval sym a)
  - sPushFrame :: sym -> Name -> Range -> SEval sym a -> SEval sym a
  - sWithCallStack :: sym -> CallStack -> SEval sym a -> SEval sym a
  - sModifyCallStack :: sym -> (CallStack -> CallStack) -> SEval sym a -> SEval sym a
  - sGetCallStack :: sym -> SEval sym CallStack
  - mergeEval :: sym -> (SBit sym -> a -> a -> SEval sym a) -> SBit sym -> SEval sym a -> SEval sym a -> SEval sym a
  - assertSideCondition :: sym -> SBit sym -> EvalError -> SEval sym ()
  - raiseError :: sym -> EvalError -> SEval sym a
  - bitAsLit :: sym -> SBit sym -> Maybe Bool
  - wordLen :: sym -> SWord sym -> Integer
  - wordAsLit :: sym -> SWord sym -> Maybe (Integer, Integer)
  - wordAsChar :: sym -> SWord sym -> Maybe Char
  - integerAsLit :: sym -> SInteger sym -> Maybe Integer
  - fpAsLit :: sym -> SFloat sym -> Maybe BF
  - bitLit :: sym -> Bool -> SBit sym
  - wordLit :: sym -> Integer -> Integer -> SEval sym (SWord sym)
  - integerLit :: sym -> Integer -> SEval sym (SInteger sym)
  - fpLit :: sym -> Integer -> Integer -> Rational -> SEval sym (SFloat sym)
  - fpExactLit :: sym -> BF -> SEval sym (SFloat sym)
  - iteBit :: sym -> SBit sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
  - iteWord :: sym -> SBit sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
  - iteInteger :: sym -> SBit sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
  - iteFloat :: sym -> SBit sym -> SFloat sym -> SFloat sym -> SEval sym (SFloat sym)
  - bitEq :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
  - bitOr :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
  - bitAnd :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
  - bitXor :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
  - bitComplement :: sym -> SBit sym -> SEval sym (SBit sym)
  - wordBit :: sym -> SWord sym -> Integer -> SEval sym (SBit sym)
  - wordUpdate :: sym -> SWord sym -> Integer -> SBit sym -> SEval sym (SWord sym)
  - packWord :: sym -> [SBit sym] -> SEval sym (SWord sym)
  - unpackWord :: sym -> SWord sym -> SEval sym [SBit sym]
  - wordFromInt :: sym -> Integer -> SInteger sym -> SEval sym (SWord sym)
  - joinWord :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
  - splitWord :: sym -> Integer -> Integer -> SWord sym -> SEval sym (SWord sym, SWord sym)
  - extractWord :: sym -> Integer -> Integer -> SWord sym -> SEval sym (SWord sym)
  - wordOr :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
  - wordAnd :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
  - wordXor :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
  - wordComplement :: sym -> SWord sym -> SEval sym (SWord sym)
  - wordPlus :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
  - wordMinus :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
  - wordMult :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
  - wordDiv :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
  - wordMod :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
  - wordSignedDiv :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
  - wordSignedMod :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
  - wordShiftLeft :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
  - wordShiftRight :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
  - wordSignedShiftRight :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
  - wordRotateLeft :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
  - wordRotateRight :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
  - wordNegate :: sym -> SWord sym -> SEval sym (SWord sym)
  - wordLg2 :: sym -> SWord sym -> SEval sym (SWord sym)
  - wordEq :: sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
  - wordSignedLessThan :: sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
  - wordLessThan :: sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
  - wordGreaterThan :: sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
  - wordToInt :: sym -> SWord sym -> SEval sym (SInteger sym)
  - wordToSignedInt :: sym -> SWord sym -> SEval sym (SInteger sym)
  - intPlus :: sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
  - intNegate :: sym -> SInteger sym -> SEval sym (SInteger sym)
  - intMinus :: sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
  - intMult :: sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
  - intDiv :: sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
  - intMod :: sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
  - intEq :: sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
  - intLessThan :: sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
  - intGreaterThan :: sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
  - intToZn :: sym -> Integer -> SInteger sym -> SEval sym (SInteger sym)
  - znToInt :: sym -> Integer -> SInteger sym -> SEval sym (SInteger sym)
  - znPlus :: sym -> Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
  - znNegate :: sym -> Integer -> SInteger sym -> SEval sym (SInteger sym)
  - znMinus :: sym -> Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
  - znMult :: sym -> Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
  - znEq :: sym -> Integer -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
  - znRecip :: sym -> Integer -> SInteger sym -> SEval sym (SInteger sym)
  - fpEq :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
  - fpLessThan :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
  - fpGreaterThan :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
  - fpLogicalEq :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
  - fpNaN :: sym -> Integer -> Integer -> SEval sym (SFloat sym)
  - fpPosInf :: sym -> Integer -> Integer -> SEval sym (SFloat sym)
  - fpPlus, fpMinus, fpMult, fpDiv :: FPArith2 sym
  - fpNeg, fpAbs :: sym -> SFloat sym -> SEval sym (SFloat sym)
  - fpSqrt :: sym -> SWord sym -> SFloat sym -> SEval sym (SFloat sym)
  - fpFMA :: sym -> SWord sym -> SFloat sym -> SFloat sym -> SFloat sym -> SEval sym (SFloat sym)
  - fpIsZero, fpIsNeg, fpIsNaN, fpIsInf, fpIsNorm, fpIsSubnorm :: sym -> SFloat sym -> SEval sym (SBit sym)
  - fpToBits :: sym -> SFloat sym -> SEval sym (SWord sym)
  - fpFromBits :: sym -> Integer -> Integer -> SWord sym -> SEval sym (SFloat sym)
  - fpToInteger :: sym -> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym)
  - fpFromInteger :: sym -> Integer -> Integer -> SWord sym -> SInteger sym -> SEval sym (SFloat sym)
  - fpToRational :: sym -> SFloat sym -> SEval sym (SRational sym)
  - fpFromRational :: sym -> Integer -> Integer -> SWord sym -> SRational sym -> SEval sym (SFloat sym)
- asciiMode :: PPOpts -> Integer -> Bool
- data EvalOpts = EvalOpts {
  - evalLogger :: Logger
  - evalPPOpts :: PPOpts
  }
- word :: Backend sym => sym -> Integer -> Integer -> SEval sym (GenValue sym)
- lam :: Backend sym => sym -> (SEval sym (GenValue sym) -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
- flam :: Backend sym => sym -> (SFloat sym -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
- tlam :: Backend sym => sym -> (TValue -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
- nlam :: Backend sym => sym -> (Nat' -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
- ilam :: Backend sym => sym -> (Integer -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
- mkSeq :: Backend sym => sym -> Nat' -> TValue -> SeqMap sym (GenValue sym) -> SEval sym (GenValue sym)
- fromVBit :: GenValue sym -> SBit sym
- fromVInteger :: GenValue sym -> SInteger sym
- fromVRational :: GenValue sym -> SRational sym
- fromVFloat :: GenValue sym -> SFloat sym
- fromVSeq :: GenValue sym -> SeqMap sym (GenValue sym)
- fromSeq :: Backend sym => String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
- fromWordVal :: Backend sym => String -> GenValue sym -> WordValue sym
- asIndex :: Backend sym => sym -> String -> TValue -> GenValue sym -> Either (SInteger sym) (WordValue sym)
- fromVWord :: Backend sym => sym -> String -> GenValue sym -> SEval sym (SWord sym)
- vWordLen :: Backend sym => GenValue sym -> Maybe Integer
- tryFromBits :: Backend sym => sym -> [SEval sym (GenValue sym)] -> SEval sym (Maybe (SWord sym))
- fromVFun :: Backend sym => sym -> GenValue sym -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
- fromVPoly :: Backend sym => sym -> GenValue sym -> TValue -> SEval sym (GenValue sym)
- fromVNumPoly :: Backend sym => sym -> GenValue sym -> Nat' -> SEval sym (GenValue sym)
- fromVTuple :: GenValue sym -> [SEval sym (GenValue sym)]
- fromVRecord :: GenValue sym -> RecordMap Ident (SEval sym (GenValue sym))
- lookupRecord :: Ident -> GenValue sym -> SEval sym (GenValue sym)
- defaultPPOpts :: PPOpts
- ppValue :: forall sym. Backend sym => sym -> PPOpts -> GenValue sym -> SEval sym Doc
- iteValue :: Backend sym => sym -> SBit sym -> SEval sym (GenValue sym) -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
- mergeValue :: Backend sym => sym -> SBit sym -> GenValue sym -> GenValue sym -> SEval sym (GenValue sym)

# GenericValue

data GenValue sym Source #

Generic value type, parameterized by bit and word types.

NOTE: we maintain an important invariant regarding sequence types. `VSeq` must never be used for finite sequences of bits. Always use the `VWord` constructor instead! Infinite sequences of bits are handled by the `VStream` constructor, just as for other types.

Constructors

VRecord !(RecordMap Ident (SEval sym (GenValue sym)))

     { .. }

VTuple ![SEval sym (GenValue sym)]

     ( .. )

VBit !(SBit sym)

     Bit

VInteger !(SInteger sym) | `Integer` or `Z n`

VRational !(SRational sym)

     Rational

VFloat !(SFloat sym) |
VSeq !Integer !(SeqMap sym (GenValue sym)) | `[n]a` Invariant: VSeq is never a sequence of bits

VWord !Integer !(WordValue sym)

     [n]Bit

VStream !(SeqMap sym (GenValue sym))

     [inf]a

VFun CallStack (SEval sym (GenValue sym) -> SEval sym (GenValue sym)) | functions
VPoly CallStack (TValue -> SEval sym (GenValue sym)) | polymorphic values (kind *)
VNumPoly CallStack (Nat' -> SEval sym (GenValue sym)) | polymorphic values (kind #)

#### Instances

Instances details

Generic (GenValue sym) Source # |
Instance details Defined in Cryptol.Eval.Value Associated Types type Rep (GenValue sym) :: Type -> Type Source # Methods from :: GenValue sym -> Rep (GenValue sym) x Source # to :: Rep (GenValue sym) x -> GenValue sym Source #
Show (GenValue sym) Source # |
Instance details Defined in Cryptol.Eval.Value Methods showsPrec :: Int -> GenValue sym -> ShowS Source # show :: GenValue sym -> String Source # showList :: [GenValue sym] -> ShowS Source #
type Rep (GenValue sym) Source # |

Instance details

Defined in Cryptol.Eval.Value

type Rep (GenValue sym) = D1 ('MetaData "GenValue" "Cryptol.Eval.Value" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (((C1 ('MetaCons "VRecord" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (RecordMap Ident (SEval sym (GenValue sym))))) :+: (C1 ('MetaCons "VTuple" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [SEval sym (GenValue sym)])) :+: C1 ('MetaCons "VBit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (SBit sym))))) :+: (C1 ('MetaCons "VInteger" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (SInteger sym))) :+: (C1 ('MetaCons "VRational" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (SRational sym))) :+: C1 ('MetaCons "VFloat" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (SFloat sym)))))) :+: ((C1 ('MetaCons "VSeq" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Integer) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (SeqMap sym (GenValue sym)))) :+: (C1 ('MetaCons "VWord" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Integer) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (WordValue sym))) :+: C1 ('MetaCons "VStream" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (SeqMap sym (GenValue sym)))))) :+: (C1 ('MetaCons "VFun" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CallStack) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (SEval sym (GenValue sym) -> SEval sym (GenValue sym)))) :+: (C1 ('MetaCons "VPoly" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CallStack) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TValue -> SEval sym (GenValue sym)))) :+: C1 ('MetaCons "VNumPoly" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CallStack) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Nat' -> SEval sym (GenValue sym))))))))

forceValue :: Backend sym => GenValue sym -> SEval sym () Source #

Force the evaluation of a value

class MonadIO (SEval sym) => Backend sym where Source #

This type class defines a collection of operations on bits, words and integers that are necessary to define generic evaluator primitives that operate on both concrete and symbolic values uniformly.

Minimal complete definition

isReady, sDeclareHole, sDelayFill, sSpark, sModifyCallStack, sGetCallStack, mergeEval, assertSideCondition, raiseError, bitAsLit, wordLen, wordAsLit, wordAsChar, integerAsLit, fpAsLit, bitLit, wordLit, integerLit, fpLit, fpExactLit, iteBit, iteWord, iteInteger, iteFloat, bitEq, bitOr, bitAnd, bitXor, bitComplement, wordBit, wordUpdate, packWord, unpackWord, wordFromInt, joinWord, splitWord, extractWord, wordOr, wordAnd, wordXor, wordComplement, wordPlus, wordMinus, wordMult, wordDiv, wordMod, wordSignedDiv, wordSignedMod, wordShiftLeft, wordShiftRight, wordSignedShiftRight, wordRotateLeft, wordRotateRight, wordNegate, wordLg2, wordEq, wordSignedLessThan, wordLessThan, wordGreaterThan, wordToInt, wordToSignedInt, intPlus, intNegate, intMinus, intMult, intDiv, intMod, intEq, intLessThan, intGreaterThan, intToZn, znToInt, znPlus, znNegate, znMinus, znMult, znEq, znRecip, fpEq, fpLessThan, fpGreaterThan, fpLogicalEq, fpNaN, fpPosInf, fpPlus, fpMinus, fpMult, fpDiv, fpNeg, fpAbs, fpSqrt, fpFMA, fpIsZero, fpIsNeg, fpIsNaN, fpIsInf, fpIsNorm, fpIsSubnorm, fpToBits, fpFromBits, fpToInteger, fpFromInteger, fpToRational, fpFromRational

Associated Types

type SBit sym :: Type Source #

type SWord sym :: Type Source #

type SInteger sym :: Type Source #

type SFloat sym :: Type Source #

type SEval sym :: Type -> Type Source #

Methods

isReady :: sym -> SEval sym a -> SEval sym (Maybe a) Source #

Check if an operation is "ready", which means its evaluation will be trivial.

sDeclareHole :: sym -> String -> SEval sym (SEval sym a, SEval sym a -> SEval sym ()) Source #

Produce a thunk value which can be filled with its associated computation after the fact. A preallocated thunk is returned, along with an operation to fill the thunk with the associated computation. This is used to implement recursive declaration groups.

sDelayFill :: sym -> SEval sym a -> Maybe (SEval sym a) -> String -> SEval sym (SEval sym a) Source #

Delay the given evaluation computation, returning a thunk which will run the computation when forced. Run the `retry` computation instead if the resulting thunk is forced during its own evaluation.

sSpark :: sym -> SEval sym a -> SEval sym (SEval sym a) Source #

Begin evaluating the given computation eagerly in a separate thread and return a thunk which will await the completion of the given computation when forced.

sPushFrame :: sym -> Name -> Range -> SEval sym a -> SEval sym a Source #

Push a call frame on to the current call stack while evaluating the given action

sWithCallStack :: sym -> CallStack -> SEval sym a -> SEval sym a Source #

Use the given call stack while evaluating the given action

sModifyCallStack :: sym -> (CallStack -> CallStack) -> SEval sym a -> SEval sym a Source #

Apply the given function to the current call stack while evaluating the given action

sGetCallStack :: sym -> SEval sym CallStack Source #

Retrieve the current evaluation call stack

mergeEval Source #

Arguments

:: sym |
-> (SBit sym -> a -> a -> SEval sym a) | A merge operation on values
-> SBit sym | The condition
-> SEval sym a | The "then" computation
-> SEval sym a | The "else" computation
-> SEval sym a |

Merge the two given computations according to the predicate.

assertSideCondition :: sym -> SBit sym -> EvalError -> SEval sym () Source #

Assert that a condition must hold, and indicate what sort of error is indicated if the condition fails.

raiseError :: sym -> EvalError -> SEval sym a Source #

Indiciate that an error condition exists

bitAsLit :: sym -> SBit sym -> Maybe Bool Source #

Determine if this symbolic bit is a boolean literal

wordLen :: sym -> SWord sym -> Integer Source #

The number of bits in a word value.

wordAsLit :: sym -> SWord sym -> Maybe (Integer, Integer) Source #

Determine if this symbolic word is a literal. If so, return the bit width and value.

wordAsChar :: sym -> SWord sym -> Maybe Char Source #

Attempt to render a word value as an ASCII character. Return `Nothing` if the character value is unknown (e.g., for symbolic values).

integerAsLit :: sym -> SInteger sym -> Maybe Integer Source #

Determine if this symbolic integer is a literal

fpAsLit :: sym -> SFloat sym -> Maybe BF Source #

Determine if this symbolic floating-point value is a literal

bitLit :: sym -> Bool -> SBit sym Source #

Construct a literal bit value from a boolean.

wordLit Source #

Arguments

:: sym |
-> Integer | Width
-> Integer | Value
-> SEval sym (SWord sym) |

Construct a literal word value given a bit width and a value.

integerLit Source #

Arguments

:: sym |
-> Integer | Value
-> SEval sym (SInteger sym) |

Construct a literal integer value from the given integer.

fpLit Source #

Arguments

:: sym |
-> Integer | exponent bits
-> Integer | precision bits
-> Rational | The rational
-> SEval sym (SFloat sym) |

Construct a floating point value from the given rational.

fpExactLit :: sym -> BF -> SEval sym (SFloat sym) Source #

Construct a floating point value from the given bit-precise floating-point representation.

iteBit :: sym -> SBit sym -> SBit sym -> SBit sym -> SEval sym (SBit sym) Source #

iteWord :: sym -> SBit sym -> SWord sym -> SWord sym -> SEval sym (SWord sym) Source #

iteInteger :: sym -> SBit sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym) Source #

iteFloat :: sym -> SBit sym -> SFloat sym -> SFloat sym -> SEval sym (SFloat sym) Source #

bitEq :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym) Source #

bitOr :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym) Source #

bitAnd :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym) Source #

bitXor :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym) Source #

bitComplement :: sym -> SBit sym -> SEval sym (SBit sym) Source #

wordBit Source #

Arguments

:: sym |
-> SWord sym |
-> Integer | Bit position to extract
-> SEval sym (SBit sym) |

Extract the numbered bit from the word.

NOTE: this assumes that the sequence of bits is big-endian and finite, so the bit numbered 0 is the most significant bit.

wordUpdate Source #

Arguments

:: sym |
-> SWord sym |
-> Integer | Bit position to update
-> SBit sym |
-> SEval sym (SWord sym) |

Update the numbered bit in the word.

NOTE: this assumes that the sequence of bits is big-endian and finite, so the bit numbered 0 is the most significant bit.

packWord :: sym -> [SBit sym] -> SEval sym (SWord sym) Source #

Construct a word value from a finite sequence of bits. NOTE: this assumes that the sequence of bits is big-endian and finite, so the first element of the list will be the most significant bit.

unpackWord :: sym -> SWord sym -> SEval sym [SBit sym] Source #

Deconstruct a packed word value in to a finite sequence of bits. NOTE: this produces a list of bits that represent a big-endian word, so the most significant bit is the first element of the list.

wordFromInt Source #

Arguments

:: sym |
-> Integer | bit-width
-> SInteger sym |
-> SEval sym (SWord sym) |

Construct a packed word of the specified width from an integer value.

joinWord :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym) Source #

Concatenate the two given word values. NOTE: the first argument represents the more-significant bits

splitWord Source #

Arguments

:: sym |
-> Integer | left width
-> Integer | right width
-> SWord sym |
-> SEval sym (SWord sym, SWord sym) |

Take the most-significant bits, and return those bits and the remainder. The first element of the pair is the most significant bits. The two integer sizes must sum to the length of the given word value.

extractWord Source #

Arguments

:: sym |
-> Integer | Number of bits to take
-> Integer | starting bit
-> SWord sym |
-> SEval sym (SWord sym) |

Extract a subsequence of bits from a packed word value. The first integer argument is the number of bits in the resulting word. The second integer argument is the number of less-significant digits to discard. Stated another way, the operation `extractWord n i w` is equivalent to first shifting `w` right by `i` bits, and then truncating to `n` bits.

wordOr :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym) Source #

Bitwise OR

wordAnd :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym) Source #

Bitwise AND

wordXor :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym) Source #

Bitwise XOR

wordComplement :: sym -> SWord sym -> SEval sym (SWord sym) Source #

Bitwise complement

wordPlus :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym) Source #

2's complement addition of packed words. The arguments must have equal bit width, and the result is of the same width. Overflow is silently discarded.

wordMinus :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym) Source #

2's complement subtraction of packed words. The arguments must have equal bit width, and the result is of the same width. Overflow is silently discarded.

wordMult :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym) Source #

2's complement multiplication of packed words. The arguments must have equal bit width, and the result is of the same width. The high bits of the multiplication are silently discarded.

wordDiv :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym) Source #

2's complement unsigned division of packed words. The arguments must have equal bit width, and the result is of the same width. It is illegal to call with a second argument concretely equal to 0.

wordMod :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym) Source #

2's complement unsigned modulus of packed words. The arguments must have equal bit width, and the result is of the same width. It is illegal to call with a second argument concretely equal to 0.

wordSignedDiv :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym) Source #

2's complement signed division of packed words. The arguments must have equal bit width, and the result is of the same width. It is illegal to call with a second argument concretely equal to 0.

wordSignedMod :: sym -> SWord sym -> SWord sym -> SEval sym (SWord sym) Source #

2's complement signed modulus of packed words. The arguments must have equal bit width, and the result is of the same width. It is illegal to call with a second argument concretely equal to 0.

wordShiftLeft Source #

Arguments

:: sym |
-> SWord sym | value to shift
-> SWord sym | amount to shift by
-> SEval sym (SWord sym) |

Shift a bitvector left by the specified amount. The shift amount is considered as an unsigned value. Shifting by more than the word length results in 0.

wordShiftRight Source #

Arguments

:: sym |
-> SWord sym | value to shift
-> SWord sym | amount to shift by
-> SEval sym (SWord sym) |

Shift a bitvector right by the specified amount. This is a logical shift, which shifts in 0 values on the left. The shift amount is considered as an unsigned value. Shifting by more than the word length results in 0.

wordSignedShiftRight Source #

Arguments

:: sym |
-> SWord sym | value to shift
-> SWord sym | amount to shift by
-> SEval sym (SWord sym) |

Shift a bitvector right by the specified amount. This is an arithmetic shift, which shifts in copies of the high bit on the left. The shift amount is considered as an unsigned value. Shifting by more than the word length results in filling the bitvector with the high bit.

wordRotateLeft Source #

Arguments

:: sym |
-> SWord sym | value to rotate
-> SWord sym | amount to rotate by
-> SEval sym (SWord sym) |

wordRotateRight Source #

Arguments

:: sym |
-> SWord sym | value to rotate
-> SWord sym | amount to rotate by
-> SEval sym (SWord sym) |

wordNegate :: sym -> SWord sym -> SEval sym (SWord sym) Source #

2's complement negation of bitvectors

wordLg2 :: sym -> SWord sym -> SEval sym (SWord sym) Source #

Compute rounded-up log-2 of the input

wordEq :: sym -> SWord sym -> SWord sym -> SEval sym (SBit sym) Source #

Test if two words are equal. Arguments must have the same width.

wordSignedLessThan :: sym -> SWord sym -> SWord sym -> SEval sym (SBit sym) Source #

Signed less-than comparison on words. Arguments must have the same width.

wordLessThan :: sym -> SWord sym -> SWord sym -> SEval sym (SBit sym) Source #

Unsigned less-than comparison on words. Arguments must have the same width.

wordGreaterThan :: sym -> SWord sym -> SWord sym -> SEval sym (SBit sym) Source #

Unsigned greater-than comparison on words. Arguments must have the same width.

wordToInt :: sym -> SWord sym -> SEval sym (SInteger sym) Source #

Construct an integer value from the given packed word.

wordToSignedInt :: sym -> SWord sym -> SEval sym (SInteger sym) Source #

Construct a signed integer value from the given packed word.

intPlus :: sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym) Source #

Addition of unbounded integers.

intNegate :: sym -> SInteger sym -> SEval sym (SInteger sym) Source #

Negation of unbounded integers

intMinus :: sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym) Source #

Subtraction of unbounded integers.

intMult :: sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym) Source #

Multiplication of unbounded integers.

intDiv :: sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym) Source #

Integer division, rounding down. It is illegal to call with a second argument concretely equal to 0. Same semantics as Haskell's `div` operation.

intMod :: sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym) Source #

Integer modulus, with division rounding down. It is illegal to call with a second argument concretely equal to 0. Same semantics as Haskell's `mod` operation.

intEq :: sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym) Source #

Equality comparison on integers

intLessThan :: sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym) Source #

Less-than comparison on integers

intGreaterThan :: sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym) Source #

Greater-than comparison on integers

intToZn Source #

Arguments

:: sym |
-> Integer | modulus
-> SInteger sym |
-> SEval sym (SInteger sym) |

Turn an integer into a value in Z_n

znToInt Source #

Arguments

:: sym |
-> Integer | modulus
-> SInteger sym |
-> SEval sym (SInteger sym) |

Transform a Z_n value into an integer, ensuring the value is properly reduced modulo n

znPlus Source #

Arguments

:: sym |
-> Integer | modulus
-> SInteger sym |
-> SInteger sym |
-> SEval sym (SInteger sym) |

Addition of integers modulo n, for a concrete positive integer n.

znNegate Source #

Arguments

:: sym |
-> Integer | modulus
-> SInteger sym |
-> SEval sym (SInteger sym) |

Additive inverse of integers modulo n

znMinus Source #

Arguments

:: sym |
-> Integer | modulus
-> SInteger sym |
-> SInteger sym |
-> SEval sym (SInteger sym) |

Subtraction of integers modulo n, for a concrete positive integer n.

znMult Source #

Arguments

:: sym |
-> Integer | modulus
-> SInteger sym |
-> SInteger sym |
-> SEval sym (SInteger sym) |

Multiplication of integers modulo n, for a concrete positive integer n.

znEq Source #

Arguments

:: sym |
-> Integer | modulus
-> SInteger sym |
-> SInteger sym |
-> SEval sym (SBit sym) |

Equality test of integers modulo n

znRecip Source #

Arguments

:: sym |
-> Integer | modulus
-> SInteger sym |
-> SEval sym (SInteger sym) |

Multiplicative inverse in (Z n). PRECONDITION: the modulus is a prime

fpEq :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym) Source #

fpLessThan :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym) Source #

fpGreaterThan :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym) Source #

fpLogicalEq :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym) Source #

fpNaN Source #

Arguments

:: sym |
-> Integer | exponent bits
-> Integer | precision bits
-> SEval sym (SFloat sym) |

fpPosInf Source #

Arguments

:: sym |
-> Integer | exponent bits
-> Integer | precision bits
-> SEval sym (SFloat sym) |

fpPlus :: FPArith2 sym Source #

fpMinus :: FPArith2 sym Source #

fpMult :: FPArith2 sym Source #

fpDiv :: FPArith2 sym Source #

fpNeg :: sym -> SFloat sym -> SEval sym (SFloat sym) Source #

fpAbs :: sym -> SFloat sym -> SEval sym (SFloat sym) Source #

fpSqrt :: sym -> SWord sym -> SFloat sym -> SEval sym (SFloat sym) Source #

fpFMA :: sym -> SWord sym -> SFloat sym -> SFloat sym -> SFloat sym -> SEval sym (SFloat sym) Source #

fpIsZero :: sym -> SFloat sym -> SEval sym (SBit sym) Source #

fpIsNeg :: sym -> SFloat sym -> SEval sym (SBit sym) Source #

fpIsNaN :: sym -> SFloat sym -> SEval sym (SBit sym) Source #

fpIsInf :: sym -> SFloat sym -> SEval sym (SBit sym) Source #

fpIsNorm :: sym -> SFloat sym -> SEval sym (SBit sym) Source #

fpIsSubnorm :: sym -> SFloat sym -> SEval sym (SBit sym) Source #

fpToBits :: sym -> SFloat sym -> SEval sym (SWord sym) Source #

fpFromBits Source #

Arguments

:: sym |
-> Integer | exponent bits
-> Integer | precision bits
-> SWord sym |
-> SEval sym (SFloat sym) |

fpToInteger Source #

Arguments

:: sym |
-> String | Name of the function for error reporting
-> SWord sym | Rounding mode
-> SFloat sym |
-> SEval sym (SInteger sym) |

fpFromInteger Source #

Arguments

:: sym |
-> Integer | exp width
-> Integer | prec width
-> SWord sym | rounding mode
-> SInteger sym | the integer to use
-> SEval sym (SFloat sym) |

fpToRational :: sym -> SFloat sym -> SEval sym (SRational sym) Source #

fpFromRational Source #

Arguments

:: sym |
-> Integer | exp width
-> Integer | prec width
-> SWord sym | rounding mode
-> SRational sym |
-> SEval sym (SFloat sym) |

#### Instances

Instances details

Backend Concrete Source # |

Instance details

Defined in Cryptol.Backend.Concrete

Associated Types

type SBit Concrete Source #

type SWord Concrete Source #

type SInteger Concrete Source #

type SFloat Concrete Source #

type SEval Concrete :: Type -> Type Source #

Methods

isReady :: Concrete -> SEval Concrete a -> SEval Concrete (Maybe a) Source #

sDeclareHole :: Concrete -> String -> SEval Concrete (SEval Concrete a, SEval Concrete a -> SEval Concrete ()) Source #

sDelayFill :: Concrete -> SEval Concrete a -> Maybe (SEval Concrete a) -> String -> SEval Concrete (SEval Concrete a) Source #

sSpark :: Concrete -> SEval Concrete a -> SEval Concrete (SEval Concrete a) Source #

sPushFrame :: Concrete -> Name -> Range -> SEval Concrete a -> SEval Concrete a Source #

sWithCallStack :: Concrete -> CallStack -> SEval Concrete a -> SEval Concrete a Source #

sModifyCallStack :: Concrete -> (CallStack -> CallStack) -> SEval Concrete a -> SEval Concrete a Source #

sGetCallStack :: Concrete -> SEval Concrete CallStack Source #

mergeEval :: Concrete -> (SBit Concrete -> a -> a -> SEval Concrete a) -> SBit Concrete -> SEval Concrete a -> SEval Concrete a -> SEval Concrete a Source #

assertSideCondition :: Concrete -> SBit Concrete -> EvalError -> SEval Concrete () Source #

raiseError :: Concrete -> EvalError -> SEval Concrete a Source #

bitAsLit :: Concrete -> SBit Concrete -> Maybe Bool Source #

wordLen :: Concrete -> SWord Concrete -> Integer Source #

wordAsLit :: Concrete -> SWord Concrete -> Maybe (Integer, Integer) Source #

wordAsChar :: Concrete -> SWord Concrete -> Maybe Char Source #

integerAsLit :: Concrete -> SInteger Concrete -> Maybe Integer Source #

fpAsLit :: Concrete -> SFloat Concrete -> Maybe BF Source #

bitLit :: Concrete -> Bool -> SBit Concrete Source #

wordLit :: Concrete -> Integer -> Integer -> SEval Concrete (SWord Concrete) Source #

integerLit :: Concrete -> Integer -> SEval Concrete (SInteger Concrete) Source #

fpLit :: Concrete -> Integer -> Integer -> Rational -> SEval Concrete (SFloat Concrete) Source #

fpExactLit :: Concrete -> BF -> SEval Concrete (SFloat Concrete) Source #

iteBit :: Concrete -> SBit Concrete -> SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete) Source #

iteWord :: Concrete -> SBit Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source #

iteInteger :: Concrete -> SBit Concrete -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete) Source #

iteFloat :: Concrete -> SBit Concrete -> SFloat Concrete -> SFloat Concrete -> SEval Concrete (SFloat Concrete) Source #

bitEq :: Concrete -> SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete) Source #

bitOr :: Concrete -> SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete) Source #

bitAnd :: Concrete -> SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete) Source #

bitXor :: Concrete -> SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete) Source #

bitComplement :: Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete) Source #

wordBit :: Concrete -> SWord Concrete -> Integer -> SEval Concrete (SBit Concrete) Source #

wordUpdate :: Concrete -> SWord Concrete -> Integer -> SBit Concrete -> SEval Concrete (SWord Concrete) Source #

packWord :: Concrete -> [SBit Concrete] -> SEval Concrete (SWord Concrete) Source #

unpackWord :: Concrete -> SWord Concrete -> SEval Concrete [SBit Concrete] Source #

wordFromInt :: Concrete -> Integer -> SInteger Concrete -> SEval Concrete (SWord Concrete) Source #

joinWord :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source #

splitWord :: Concrete -> Integer -> Integer -> SWord Concrete -> SEval Concrete (SWord Concrete, SWord Concrete) Source #

extractWord :: Concrete -> Integer -> Integer -> SWord Concrete -> SEval Concrete (SWord Concrete) Source #

wordOr :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source #

wordAnd :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source #

wordXor :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source #

wordComplement :: Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source #

wordPlus :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source #

wordMinus :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source #

wordMult :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source #

wordDiv :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source #

wordMod :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source #

wordSignedDiv :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source #

wordSignedMod :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source #

wordShiftLeft :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source #

wordShiftRight :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source #

wordSignedShiftRight :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source #

wordRotateLeft :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source #

wordRotateRight :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source #

wordNegate :: Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source #

wordLg2 :: Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete) Source #

wordEq :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SBit Concrete) Source #

wordSignedLessThan :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SBit Concrete) Source #

wordLessThan :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SBit Concrete) Source #

wordGreaterThan :: Concrete -> SWord Concrete -> SWord Concrete -> SEval Concrete (SBit Concrete) Source #

wordToInt :: Concrete -> SWord Concrete -> SEval Concrete (SInteger Concrete) Source #

wordToSignedInt :: Concrete -> SWord Concrete -> SEval Concrete (SInteger Concrete) Source #

intPlus :: Concrete -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete) Source #

intNegate :: Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete) Source #

intMinus :: Concrete -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete) Source #

intMult :: Concrete -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete) Source #

intDiv :: Concrete -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete) Source #

intMod :: Concrete -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete) Source #

intEq :: Concrete -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SBit Concrete) Source #

intLessThan :: Concrete -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SBit Concrete) Source #

intGreaterThan :: Concrete -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SBit Concrete) Source #

intToZn :: Concrete -> Integer -> SInteger Concrete -> SEval Concrete (SInteger Concrete) Source #

znToInt :: Concrete -> Integer -> SInteger Concrete -> SEval Concrete (SInteger Concrete) Source #

znPlus :: Concrete -> Integer -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete) Source #

znNegate :: Concrete -> Integer -> SInteger Concrete -> SEval Concrete (SInteger Concrete) Source #

znMinus :: Concrete -> Integer -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete) Source #

znMult :: Concrete -> Integer -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete) Source #

znEq :: Concrete -> Integer -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SBit Concrete) Source #

znRecip :: Concrete -> Integer -> SInteger Concrete -> SEval Concrete (SInteger Concrete) Source #

fpEq :: Concrete -> SFloat Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete) Source #

fpLessThan :: Concrete -> SFloat Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete) Source #

fpGreaterThan :: Concrete -> SFloat Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete) Source #

fpLogicalEq :: Concrete -> SFloat Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete) Source #

fpNaN :: Concrete -> Integer -> Integer -> SEval Concrete (SFloat Concrete) Source #

fpPosInf :: Concrete -> Integer -> Integer -> SEval Concrete (SFloat Concrete) Source #

fpPlus :: FPArith2 Concrete Source #

fpMinus :: FPArith2 Concrete Source #

fpMult :: FPArith2 Concrete Source #

fpDiv :: FPArith2 Concrete Source #

fpNeg :: Concrete -> SFloat Concrete -> SEval Concrete (SFloat Concrete) Source #

fpAbs :: Concrete -> SFloat Concrete -> SEval Concrete (SFloat Concrete) Source #

fpSqrt :: Concrete -> SWord Concrete -> SFloat Concrete -> SEval Concrete (SFloat Concrete) Source #

fpFMA :: Concrete -> SWord Concrete -> SFloat Concrete -> SFloat Concrete -> SFloat Concrete -> SEval Concrete (SFloat Concrete) Source #

fpIsZero :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete) Source #

fpIsNeg :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete) Source #

fpIsNaN :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete) Source #

fpIsInf :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete) Source #

fpIsNorm :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete) Source #

fpIsSubnorm :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete) Source #

fpToBits :: Concrete -> SFloat Concrete -> SEval Concrete (SWord Concrete) Source #

fpFromBits :: Concrete -> Integer -> Integer -> SWord Concrete -> SEval Concrete (SFloat Concrete) Source #

fpToInteger :: Concrete -> String -> SWord Concrete -> SFloat Concrete -> SEval Concrete (SInteger Concrete) Source #

fpFromInteger :: Concrete -> Integer -> Integer -> SWord Concrete -> SInteger Concrete -> SEval Concrete (SFloat Concrete) Source #

fpToRational :: Concrete -> SFloat Concrete -> SEval Concrete (SRational Concrete) Source #

fpFromRational :: Concrete -> Integer -> Integer -> SWord Concrete -> SRational Concrete -> SEval Concrete (SFloat Concrete) Source #

Backend SBV Source # |

Instance details

Defined in Cryptol.Backend.SBV

Associated Types

type SBit SBV Source #

type SWord SBV Source #

type SInteger SBV Source #

type SFloat SBV Source #

type SEval SBV :: Type -> Type Source #

Methods

isReady :: SBV -> SEval SBV a -> SEval SBV (Maybe a) Source #

sDeclareHole :: SBV -> String -> SEval SBV (SEval SBV a, SEval SBV a -> SEval SBV ()) Source #

sDelayFill :: SBV -> SEval SBV a -> Maybe (SEval SBV a) -> String -> SEval SBV (SEval SBV a) Source #

sSpark :: SBV -> SEval SBV a -> SEval SBV (SEval SBV a) Source #

sPushFrame :: SBV -> Name -> Range -> SEval SBV a -> SEval SBV a Source #

sWithCallStack :: SBV -> CallStack -> SEval SBV a -> SEval SBV a Source #

sModifyCallStack :: SBV -> (CallStack -> CallStack) -> SEval SBV a -> SEval SBV a Source #

sGetCallStack :: SBV -> SEval SBV CallStack Source #

mergeEval :: SBV -> (SBit SBV -> a -> a -> SEval SBV a) -> SBit SBV -> SEval SBV a -> SEval SBV a -> SEval SBV a Source #

assertSideCondition :: SBV -> SBit SBV -> EvalError -> SEval SBV () Source #

raiseError :: SBV -> EvalError -> SEval SBV a Source #

bitAsLit :: SBV -> SBit SBV -> Maybe Bool Source #

wordLen :: SBV -> SWord SBV -> Integer Source #

wordAsLit :: SBV -> SWord SBV -> Maybe (Integer, Integer) Source #

wordAsChar :: SBV -> SWord SBV -> Maybe Char Source #

integerAsLit :: SBV -> SInteger SBV -> Maybe Integer Source #

fpAsLit :: SBV -> SFloat SBV -> Maybe BF Source #

bitLit :: SBV -> Bool -> SBit SBV Source #

wordLit :: SBV -> Integer -> Integer -> SEval SBV (SWord SBV) Source #

integerLit :: SBV -> Integer -> SEval SBV (SInteger SBV) Source #

fpLit :: SBV -> Integer -> Integer -> Rational -> SEval SBV (SFloat SBV) Source #

fpExactLit :: SBV -> BF -> SEval SBV (SFloat SBV) Source #

iteBit :: SBV -> SBit SBV -> SBit SBV -> SBit SBV -> SEval SBV (SBit SBV) Source #

iteWord :: SBV -> SBit SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

iteInteger :: SBV -> SBit SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source #

iteFloat :: SBV -> SBit SBV -> SFloat SBV -> SFloat SBV -> SEval SBV (SFloat SBV) Source #

bitEq :: SBV -> SBit SBV -> SBit SBV -> SEval SBV (SBit SBV) Source #

bitOr :: SBV -> SBit SBV -> SBit SBV -> SEval SBV (SBit SBV) Source #

bitAnd :: SBV -> SBit SBV -> SBit SBV -> SEval SBV (SBit SBV) Source #

bitXor :: SBV -> SBit SBV -> SBit SBV -> SEval SBV (SBit SBV) Source #

bitComplement :: SBV -> SBit SBV -> SEval SBV (SBit SBV) Source #

wordBit :: SBV -> SWord SBV -> Integer -> SEval SBV (SBit SBV) Source #

wordUpdate :: SBV -> SWord SBV -> Integer -> SBit SBV -> SEval SBV (SWord SBV) Source #

packWord :: SBV -> [SBit SBV] -> SEval SBV (SWord SBV) Source #

unpackWord :: SBV -> SWord SBV -> SEval SBV [SBit SBV] Source #

wordFromInt :: SBV -> Integer -> SInteger SBV -> SEval SBV (SWord SBV) Source #

joinWord :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

splitWord :: SBV -> Integer -> Integer -> SWord SBV -> SEval SBV (SWord SBV, SWord SBV) Source #

extractWord :: SBV -> Integer -> Integer -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordOr :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordAnd :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordXor :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordComplement :: SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordPlus :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordMinus :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordMult :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordDiv :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordMod :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordSignedDiv :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordSignedMod :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordShiftLeft :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordShiftRight :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordSignedShiftRight :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordRotateLeft :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordRotateRight :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordNegate :: SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordLg2 :: SBV -> SWord SBV -> SEval SBV (SWord SBV) Source #

wordEq :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SBit SBV) Source #

wordSignedLessThan :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SBit SBV) Source #

wordLessThan :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SBit SBV) Source #

wordGreaterThan :: SBV -> SWord SBV -> SWord SBV -> SEval SBV (SBit SBV) Source #

wordToInt :: SBV -> SWord SBV -> SEval SBV (SInteger SBV) Source #

wordToSignedInt :: SBV -> SWord SBV -> SEval SBV (SInteger SBV) Source #

intPlus :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source #

intNegate :: SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source #

intMinus :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source #

intMult :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source #

intDiv :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source #

intMod :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source #

intEq :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SBit SBV) Source #

intLessThan :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SBit SBV) Source #

intGreaterThan :: SBV -> SInteger SBV -> SInteger SBV -> SEval SBV (SBit SBV) Source #

intToZn :: SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV) Source #

znToInt :: SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV) Source #

znPlus :: SBV -> Integer -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source #

znNegate :: SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV) Source #

znMinus :: SBV -> Integer -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source #

znMult :: SBV -> Integer -> SInteger SBV -> SInteger SBV -> SEval SBV (SInteger SBV) Source #

znEq :: SBV -> Integer -> SInteger SBV -> SInteger SBV -> SEval SBV (SBit SBV) Source #

znRecip :: SBV -> Integer -> SInteger SBV -> SEval SBV (SInteger SBV) Source #

fpEq :: SBV -> SFloat SBV -> SFloat SBV -> SEval SBV (SBit SBV) Source #

fpLessThan :: SBV -> SFloat SBV -> SFloat SBV -> SEval SBV (SBit SBV) Source #

fpGreaterThan :: SBV -> SFloat SBV -> SFloat SBV -> SEval SBV (SBit SBV) Source #

fpLogicalEq :: SBV -> SFloat SBV -> SFloat SBV -> SEval SBV (SBit SBV) Source #

fpNaN :: SBV -> Integer -> Integer -> SEval SBV (SFloat SBV) Source #

fpPosInf :: SBV -> Integer -> Integer -> SEval SBV (SFloat SBV) Source #

fpPlus :: FPArith2 SBV Source #

fpMinus :: FPArith2 SBV Source #

fpMult :: FPArith2 SBV Source #

fpDiv :: FPArith2 SBV Source #

fpNeg :: SBV -> SFloat SBV -> SEval SBV (SFloat SBV) Source #

fpAbs :: SBV -> SFloat SBV -> SEval SBV (SFloat SBV) Source #

fpSqrt :: SBV -> SWord SBV -> SFloat SBV -> SEval SBV (SFloat SBV) Source #

fpFMA :: SBV -> SWord SBV -> SFloat SBV -> SFloat SBV -> SFloat SBV -> SEval SBV (SFloat SBV) Source #

fpIsZero :: SBV -> SFloat SBV -> SEval SBV (SBit SBV) Source #

fpIsNeg :: SBV -> SFloat SBV -> SEval SBV (SBit SBV) Source #

fpIsNaN :: SBV -> SFloat SBV -> SEval SBV (SBit SBV) Source #

fpIsInf :: SBV -> SFloat SBV -> SEval SBV (SBit SBV) Source #

fpIsNorm :: SBV -> SFloat SBV -> SEval SBV (SBit SBV) Source #

fpIsSubnorm :: SBV -> SFloat SBV -> SEval SBV (SBit SBV) Source #

fpToBits :: SBV -> SFloat SBV -> SEval SBV (SWord SBV) Source #

fpFromBits :: SBV -> Integer -> Integer -> SWord SBV -> SEval SBV (SFloat SBV) Source #

fpToInteger :: SBV -> String -> SWord SBV -> SFloat SBV -> SEval SBV (SInteger SBV) Source #

fpFromInteger :: SBV -> Integer -> Integer -> SWord SBV -> SInteger SBV -> SEval SBV (SFloat SBV) Source #

fpToRational :: SBV -> SFloat SBV -> SEval SBV (SRational SBV) Source #

fpFromRational :: SBV -> Integer -> Integer -> SWord SBV -> SRational SBV -> SEval SBV (SFloat SBV) Source #

IsSymExprBuilder sym => Backend (What4 sym) Source # |

Instance details

Defined in Cryptol.Backend.What4

Associated Types

type SBit (What4 sym) Source #

type SWord (What4 sym) Source #

type SInteger (What4 sym) Source #

type SFloat (What4 sym) Source #

type SEval (What4 sym) :: Type -> Type Source #

Methods

isReady :: What4 sym -> SEval (What4 sym) a -> SEval (What4 sym) (Maybe a) Source #

sDeclareHole :: What4 sym -> String -> SEval (What4 sym) (SEval (What4 sym) a, SEval (What4 sym) a -> SEval (What4 sym) ()) Source #

sDelayFill :: What4 sym -> SEval (What4 sym) a -> Maybe (SEval (What4 sym) a) -> String -> SEval (What4 sym) (SEval (What4 sym) a) Source #

sSpark :: What4 sym -> SEval (What4 sym) a -> SEval (What4 sym) (SEval (What4 sym) a) Source #

sPushFrame :: What4 sym -> Name -> Range -> SEval (What4 sym) a -> SEval (What4 sym) a Source #

sWithCallStack :: What4 sym -> CallStack -> SEval (What4 sym) a -> SEval (What4 sym) a Source #

sModifyCallStack :: What4 sym -> (CallStack -> CallStack) -> SEval (What4 sym) a -> SEval (What4 sym) a Source #

sGetCallStack :: What4 sym -> SEval (What4 sym) CallStack Source #

mergeEval :: What4 sym -> (SBit (What4 sym) -> a -> a -> SEval (What4 sym) a) -> SBit (What4 sym) -> SEval (What4 sym) a -> SEval (What4 sym) a -> SEval (What4 sym) a Source #

assertSideCondition :: What4 sym -> SBit (What4 sym) -> EvalError -> SEval (What4 sym) () Source #

raiseError :: What4 sym -> EvalError -> SEval (What4 sym) a Source #

bitAsLit :: What4 sym -> SBit (What4 sym) -> Maybe Bool Source #

wordLen :: What4 sym -> SWord (What4 sym) -> Integer Source #

wordAsLit :: What4 sym -> SWord (What4 sym) -> Maybe (Integer, Integer) Source #

wordAsChar :: What4 sym -> SWord (What4 sym) -> Maybe Char Source #

integerAsLit :: What4 sym -> SInteger (What4 sym) -> Maybe Integer Source #

fpAsLit :: What4 sym -> SFloat (What4 sym) -> Maybe BF Source #

bitLit :: What4 sym -> Bool -> SBit (What4 sym) Source #

wordLit :: What4 sym -> Integer -> Integer -> SEval (What4 sym) (SWord (What4 sym)) Source #

integerLit :: What4 sym -> Integer -> SEval (What4 sym) (SInteger (What4 sym)) Source #

fpLit :: What4 sym -> Integer -> Integer -> Rational -> SEval (What4 sym) (SFloat (What4 sym)) Source #

fpExactLit :: What4 sym -> BF -> SEval (What4 sym) (SFloat (What4 sym)) Source #

iteBit :: What4 sym -> SBit (What4 sym) -> SBit (What4 sym) -> SBit (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

iteWord :: What4 sym -> SBit (What4 sym) -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

iteInteger :: What4 sym -> SBit (What4 sym) -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

iteFloat :: What4 sym -> SBit (What4 sym) -> SFloat (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SFloat (What4 sym)) Source #

bitEq :: What4 sym -> SBit (What4 sym) -> SBit (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

bitOr :: What4 sym -> SBit (What4 sym) -> SBit (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

bitAnd :: What4 sym -> SBit (What4 sym) -> SBit (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

bitXor :: What4 sym -> SBit (What4 sym) -> SBit (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

bitComplement :: What4 sym -> SBit (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

wordBit :: What4 sym -> SWord (What4 sym) -> Integer -> SEval (What4 sym) (SBit (What4 sym)) Source #

wordUpdate :: What4 sym -> SWord (What4 sym) -> Integer -> SBit (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

packWord :: What4 sym -> [SBit (What4 sym)] -> SEval (What4 sym) (SWord (What4 sym)) Source #

unpackWord :: What4 sym -> SWord (What4 sym) -> SEval (What4 sym) [SBit (What4 sym)] Source #

wordFromInt :: What4 sym -> Integer -> SInteger (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

joinWord :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

splitWord :: What4 sym -> Integer -> Integer -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym), SWord (What4 sym)) Source #

extractWord :: What4 sym -> Integer -> Integer -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordOr :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordAnd :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordXor :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordComplement :: What4 sym -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordPlus :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordMinus :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordMult :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordDiv :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordMod :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordSignedDiv :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordSignedMod :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordShiftLeft :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordShiftRight :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordSignedShiftRight :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordRotateLeft :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordRotateRight :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordNegate :: What4 sym -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordLg2 :: What4 sym -> SWord (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

wordEq :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

wordSignedLessThan :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

wordLessThan :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

wordGreaterThan :: What4 sym -> SWord (What4 sym) -> SWord (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

wordToInt :: What4 sym -> SWord (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

wordToSignedInt :: What4 sym -> SWord (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

intPlus :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

intNegate :: What4 sym -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

intMinus :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

intMult :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

intDiv :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

intMod :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

intEq :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

intLessThan :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

intGreaterThan :: What4 sym -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

intToZn :: What4 sym -> Integer -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

znToInt :: What4 sym -> Integer -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

znPlus :: What4 sym -> Integer -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

znNegate :: What4 sym -> Integer -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

znMinus :: What4 sym -> Integer -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

znMult :: What4 sym -> Integer -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

znEq :: What4 sym -> Integer -> SInteger (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

znRecip :: What4 sym -> Integer -> SInteger (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

fpEq :: What4 sym -> SFloat (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

fpLessThan :: What4 sym -> SFloat (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

fpGreaterThan :: What4 sym -> SFloat (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

fpLogicalEq :: What4 sym -> SFloat (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

fpNaN :: What4 sym -> Integer -> Integer -> SEval (What4 sym) (SFloat (What4 sym)) Source #

fpPosInf :: What4 sym -> Integer -> Integer -> SEval (What4 sym) (SFloat (What4 sym)) Source #

fpPlus :: FPArith2 (What4 sym) Source #

fpMinus :: FPArith2 (What4 sym) Source #

fpMult :: FPArith2 (What4 sym) Source #

fpDiv :: FPArith2 (What4 sym) Source #

fpNeg :: What4 sym -> SFloat (What4 sym) -> SEval (What4 sym) (SFloat (What4 sym)) Source #

fpAbs :: What4 sym -> SFloat (What4 sym) -> SEval (What4 sym) (SFloat (What4 sym)) Source #

fpSqrt :: What4 sym -> SWord (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SFloat (What4 sym)) Source #

fpFMA :: What4 sym -> SWord (What4 sym) -> SFloat (What4 sym) -> SFloat (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SFloat (What4 sym)) Source #

fpIsZero :: What4 sym -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

fpIsNeg :: What4 sym -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

fpIsNaN :: What4 sym -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

fpIsInf :: What4 sym -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

fpIsNorm :: What4 sym -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

fpIsSubnorm :: What4 sym -> SFloat (What4 sym) -> SEval (What4 sym) (SBit (What4 sym)) Source #

fpToBits :: What4 sym -> SFloat (What4 sym) -> SEval (What4 sym) (SWord (What4 sym)) Source #

fpFromBits :: What4 sym -> Integer -> Integer -> SWord (What4 sym) -> SEval (What4 sym) (SFloat (What4 sym)) Source #

fpToInteger :: What4 sym -> String -> SWord (What4 sym) -> SFloat (What4 sym) -> SEval (What4 sym) (SInteger (What4 sym)) Source #

fpFromInteger :: What4 sym -> Integer -> Integer -> SWord (What4 sym) -> SInteger (What4 sym) -> SEval (What4 sym) (SFloat (What4 sym)) Source #

fpToRational :: What4 sym -> SFloat (What4 sym) -> SEval (What4 sym) (SRational (What4 sym)) Source #

fpFromRational :: What4 sym -> Integer -> Integer -> SWord (What4 sym) -> SRational (What4 sym) -> SEval (What4 sym) (SFloat (What4 sym)) Source #

asciiMode :: PPOpts -> Integer -> Bool Source #

data EvalOpts Source #

Some options for evalutaion

Constructors

EvalOpts |

Fields

- evalLogger :: Logger

  Where to print stuff (e.g., for `trace`)

- evalPPOpts :: PPOpts

  How to pretty print things.

## Value introduction operations

word :: Backend sym => sym -> Integer -> Integer -> SEval sym (GenValue sym) Source #

Create a packed word of n bits.

lam :: Backend sym => sym -> (SEval sym (GenValue sym) -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym) Source #

Construct a function value

flam :: Backend sym => sym -> (SFloat sym -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym) Source #

Functions that assume floating point inputs

tlam :: Backend sym => sym -> (TValue -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym) Source #

A type lambda that expects a `Type`.

nlam :: Backend sym => sym -> (Nat' -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym) Source #

A type lambda that expects a `Type` of kind #.

ilam :: Backend sym => sym -> (Integer -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym) Source #

A type lambda that expects a finite numeric type.

mkSeq :: Backend sym => sym -> Nat' -> TValue -> SeqMap sym (GenValue sym) -> SEval sym (GenValue sym) Source #

Construct either a finite sequence, or a stream. In the finite case, record whether or not the elements were bits, to aid pretty-printing.

## Value eliminators

fromVBit :: GenValue sym -> SBit sym Source #

Extract a bit value.

fromVInteger :: GenValue sym -> SInteger sym Source #

Extract an integer value.

fromVRational :: GenValue sym -> SRational sym Source #

Extract a rational value.

fromVFloat :: GenValue sym -> SFloat sym Source #

fromVSeq :: GenValue sym -> SeqMap sym (GenValue sym) Source #

Extract a finite sequence value.

fromSeq :: Backend sym => String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym)) Source #

Extract a sequence.

fromWordVal :: Backend sym => String -> GenValue sym -> WordValue sym Source #

asIndex :: Backend sym => sym -> String -> TValue -> GenValue sym -> Either (SInteger sym) (WordValue sym) Source #

fromVWord :: Backend sym => sym -> String -> GenValue sym -> SEval sym (SWord sym) Source #

Extract a packed word.

vWordLen :: Backend sym => GenValue sym -> Maybe Integer Source #

tryFromBits :: Backend sym => sym -> [SEval sym (GenValue sym)] -> SEval sym (Maybe (SWord sym)) Source #

If the given list of values are all fully-evaluated thunks containing bits, return a packed word built from the same bits. However, if any value is not a fully-evaluated bit, return `Nothing`.

fromVFun :: Backend sym => sym -> GenValue sym -> SEval sym (GenValue sym) -> SEval sym (GenValue sym) Source #

Extract a function from a value.

fromVPoly :: Backend sym => sym -> GenValue sym -> TValue -> SEval sym (GenValue sym) Source #

Extract a polymorphic function from a value.

fromVNumPoly :: Backend sym => sym -> GenValue sym -> Nat' -> SEval sym (GenValue sym) Source #

Extract a polymorphic function from a value.

fromVTuple :: GenValue sym -> [SEval sym (GenValue sym)] Source #

Extract a tuple from a value.

fromVRecord :: GenValue sym -> RecordMap Ident (SEval sym (GenValue sym)) Source #

Extract a record from a value.

lookupRecord :: Ident -> GenValue sym -> SEval sym (GenValue sym) Source #

Lookup a field in a record.

## Pretty printing

defaultPPOpts :: PPOpts Source #

ppValue :: forall sym. Backend sym => sym -> PPOpts -> GenValue sym -> SEval sym Doc Source #

# Merge and ifthenelse

iteValue :: Backend sym => sym -> SBit sym -> SEval sym (GenValue sym) -> SEval sym (GenValue sym) -> SEval sym (GenValue sym) Source #

mergeValue :: Backend sym => sym -> SBit sym -> GenValue sym -> GenValue sym -> SEval sym (GenValue sym) Source #