Cryptol.Eval.Value

GenericValue

data GenValue sym

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)

[n]a Invariant: VSeq is never a sequence of bits

VWord !Integer !(SEval sym (WordValue sym))

 [n]Bit

VStream !(SeqMap sym)

 [inf]a

VFun (SEval sym (GenValue sym) -> SEval sym (GenValue sym))

functions

VPoly (TValue -> SEval sym (GenValue sym))

polymorphic values (kind *)

VNumPoly (Nat' -> SEval sym (GenValue sym))

polymorphic values (kind #)

Instances

Backend sym => Show (GenValue sym)

Defined in Cryptol.Eval.Value

Methods

showsPrec :: Int -> GenValue sym -> ShowS

show :: GenValue sym -> String

showList :: [GenValue sym] -> ShowS

Generic (GenValue sym)

Defined in Cryptol.Eval.Value

Associated Types

type Rep (GenValue sym) :: Type -> Type

Methods

from :: GenValue sym -> Rep (GenValue sym) x

to :: Rep (GenValue sym) x -> GenValue sym

type Rep (GenValue sym)

Defined in Cryptol.Eval.Value

type Rep (GenValue sym) = D1 ('MetaData "GenValue" "Cryptol.Eval.Value" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" '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))) :+: (C1 ('MetaCons "VWord" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Integer) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (SEval sym (WordValue sym)))) :+: C1 ('MetaCons "VStream" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (SeqMap sym))))) :+: (C1 ('MetaCons "VFun" 'PrefixI 'False) (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 (TValue -> SEval sym (GenValue sym)))) :+: C1 ('MetaCons "VNumPoly" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Nat' -> SEval sym (GenValue sym))))))))

forceWordValue :: Backend sym => WordValue sym -> SEval sym ()

Force the evaluation of a word value

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

Force the evaluation of a value

class MonadIO (SEval sym) => Backend sym where

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.

Associated Types

type SBit sym :: Type

type SWord sym :: Type

type SInteger sym :: Type

type SFloat sym :: Type

type SEval sym :: Type -> Type

Methods

isReady :: sym -> SEval sym a -> Bool

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 ())

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 -> SEval sym a -> SEval sym (SEval sym a)

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)

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.

mergeEval

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 ()

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

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

Indiciate that an error condition exists

ppBit :: sym -> SBit sym -> Doc

Pretty-print an individual bit

ppWord :: sym -> PPOpts -> SWord sym -> Doc

Pretty-print a word value

ppInteger :: sym -> PPOpts -> SInteger sym -> Doc

Pretty-print an integer value

ppFloat :: sym -> PPOpts -> SFloat sym -> Doc

Pretty-print a floating-point value

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

Determine if this symbolic bit is a boolean literal

wordLen :: sym -> SWord sym -> Integer

The number of bits in a word value.

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

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

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

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

Determine if this symbolic integer is a literal

bitLit :: sym -> Bool -> SBit sym

Construct a literal bit value from a boolean.

wordLit

Arguments

:: sym

-> Integer

Width

-> Integer

Value

-> SEval sym (SWord sym)

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

integerLit

Arguments

:: sym

-> Integer

Value

-> SEval sym (SInteger sym)

Construct a literal integer value from the given integer.

fpLit

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)

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)

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

iteInteger :: sym -> SBit sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger 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

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

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)

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]

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

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)

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

splitWord

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

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)

Bitwise OR

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

Bitwise AND

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

Bitwise XOR

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

Bitwise complement

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

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)

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)

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)

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)

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)

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)

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.

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

2's complement negation of bitvectors

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

Compute rounded-up log-2 of the input

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

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

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

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

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

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

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

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

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

Construct an integer value from the given packed word.

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

Addition of unbounded integers.

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

Negation of unbounded integers

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

Subtraction of unbounded integers.

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

Multiplication of unbounded integers.

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

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)

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)

Equality comparison on integers

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

Less-than comparison on integers

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

Greater-than comparison on integers

intToZn

Arguments

:: sym

-> Integer

modulus

-> SInteger sym

-> SEval sym (SInteger sym)

Turn an integer into a value in Z_n

znToInt

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

Arguments

:: sym

-> Integer

modulus

-> SInteger sym

-> SInteger sym

-> SEval sym (SInteger sym)

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

znNegate

Arguments

:: sym

-> Integer

modulus

-> SInteger sym

-> SEval sym (SInteger sym)

Additive inverse of integers modulo n

znMinus

Arguments

:: sym

-> Integer

modulus

-> SInteger sym

-> SInteger sym

-> SEval sym (SInteger sym)

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

znMult

Arguments

:: sym

-> Integer

modulus

-> SInteger sym

-> SInteger sym

-> SEval sym (SInteger sym)

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

znEq

Arguments

:: sym

-> Integer

modulus

-> SInteger sym

-> SInteger sym

-> SEval sym (SBit sym)

Equality test of integers modulo n

znRecip

Arguments

:: sym

-> Integer

modulus

-> SInteger sym

-> SEval sym (SInteger sym)

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

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)

fpPlus :: FPArith2 sym

fpMinus :: FPArith2 sym

fpMult :: FPArith2 sym

fpDiv :: FPArith2 sym

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

fpToInteger

Arguments

:: sym

-> String

Name of the function for error reporting

-> SWord sym

Rounding mode

-> SFloat sym

-> SEval sym (SInteger sym)

fpFromInteger

Arguments

:: sym

-> Integer

-> Integer

-> SWord sym

rounding mode

-> SInteger sym

the integeer to use

-> SEval sym (SFloat sym)

Instances

Backend Concrete

Defined in Cryptol.Backend.Concrete

Associated Types

type SBit Concrete

type SWord Concrete

type SInteger Concrete

type SFloat Concrete

type SEval Concrete :: Type -> Type

Methods

isReady :: Concrete -> SEval Concrete a -> Bool

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

sDelayFill :: Concrete -> SEval Concrete a -> SEval Concrete a -> SEval Concrete (SEval Concrete a)

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

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

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

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

ppBit :: Concrete -> SBit Concrete -> Doc

ppWord :: Concrete -> PPOpts -> SWord Concrete -> Doc

ppInteger :: Concrete -> PPOpts -> SInteger Concrete -> Doc

ppFloat :: Concrete -> PPOpts -> SFloat Concrete -> Doc

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

wordLen :: Concrete -> SWord Concrete -> Integer

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

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

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

bitLit :: Concrete -> Bool -> SBit Concrete

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

fpPlus :: FPArith2 Concrete

fpMinus :: FPArith2 Concrete

fpMult :: FPArith2 Concrete

fpDiv :: FPArith2 Concrete

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

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

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

Backend SBV

Defined in Cryptol.Backend.SBV

Associated Types

type SBit SBV

type SWord SBV

type SInteger SBV

type SFloat SBV

type SEval SBV :: Type -> Type

Methods

isReady :: SBV -> SEval SBV a -> Bool

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

sDelayFill :: SBV -> SEval SBV a -> SEval SBV a -> SEval SBV (SEval SBV a)

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

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

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

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

ppBit :: SBV -> SBit SBV -> Doc

ppWord :: SBV -> PPOpts -> SWord SBV -> Doc

ppInteger :: SBV -> PPOpts -> SInteger SBV -> Doc

ppFloat :: SBV -> PPOpts -> SFloat SBV -> Doc

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

wordLen :: SBV -> SWord SBV -> Integer

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

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

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

bitLit :: SBV -> Bool -> SBit SBV

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

fpPlus :: FPArith2 SBV

fpMinus :: FPArith2 SBV

fpMult :: FPArith2 SBV

fpDiv :: FPArith2 SBV

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

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

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

IsSymExprBuilder sym => Backend (What4 sym)

Defined in Cryptol.Backend.What4

Associated Types

type SBit (What4 sym)

type SWord (What4 sym)

type SInteger (What4 sym)

type SFloat (What4 sym)

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

Methods

isReady :: What4 sym -> SEval (What4 sym) a -> Bool

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

sDelayFill :: What4 sym -> SEval (What4 sym) a -> SEval (What4 sym) a -> SEval (What4 sym) (SEval (What4 sym) a)

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

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

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

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

ppBit :: What4 sym -> SBit (What4 sym) -> Doc

ppWord :: What4 sym -> PPOpts -> SWord (What4 sym) -> Doc

ppInteger :: What4 sym -> PPOpts -> SInteger (What4 sym) -> Doc

ppFloat :: What4 sym -> PPOpts -> SFloat (What4 sym) -> Doc

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

fpPlus :: FPArith2 (What4 sym)

fpMinus :: FPArith2 (What4 sym)

fpMult :: FPArith2 (What4 sym)

fpDiv :: FPArith2 (What4 sym)

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

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

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

asciiMode :: PPOpts -> Integer -> Bool

Value introduction operations

word :: Backend sym => sym -> Integer -> Integer -> GenValue sym

Create a packed word of n bits.

lam :: (SEval sym (GenValue sym) -> SEval sym (GenValue sym)) -> GenValue sym

wlam :: Backend sym => sym -> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym

Functions that assume word inputs

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

Functions that assume floating point inputs

tlam :: Backend sym => (TValue -> GenValue sym) -> GenValue sym

A type lambda that expects a Type.

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

A type lambda that expects a Type of kind #.

ilam :: Backend sym => (Integer -> GenValue sym) -> GenValue sym

A type lambda that expects a finite numeric type.

toStream :: Backend sym => [GenValue sym] -> SEval sym (GenValue sym)

Generate a stream.

toFinSeq :: Backend sym => sym -> Integer -> TValue -> [GenValue sym] -> GenValue sym

toSeq :: Backend sym => sym -> Nat' -> TValue -> [GenValue sym] -> SEval sym (GenValue sym)

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

mkSeq :: Backend sym => Nat' -> TValue -> SeqMap sym -> GenValue sym

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

Extract a bit value.

fromVInteger :: GenValue sym -> SInteger sym

Extract an integer value.

fromVRational :: GenValue sym -> SRational sym

Extract a rational value.

fromVFloat :: GenValue sym -> SFloat sym

fromVSeq :: GenValue sym -> SeqMap sym

Extract a finite sequence value.

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

Extract a sequence.

fromWordVal :: Backend sym => String -> GenValue sym -> SEval sym (WordValue sym)

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

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

Extract a packed word.

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

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

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 :: GenValue sym -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)

Extract a function from a value.

fromVPoly :: GenValue sym -> TValue -> SEval sym (GenValue sym)

Extract a polymorphic function from a value.

fromVNumPoly :: GenValue sym -> Nat' -> SEval sym (GenValue sym)

Extract a polymorphic function from a value.

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

Extract a tuple from a value.

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

Extract a record from a value.

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

Lookup a field in a record.

Pretty printing

defaultPPOpts :: PPOpts

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

Sequence Maps

data SeqMap sym

A sequence map represents a mapping from nonnegative integer indices to values. These are used to represent both finite and infinite sequences.

Constructors

IndexSeqMap !(Integer -> SEval sym (GenValue sym))

UpdateSeqMap !(Map Integer (SEval sym (GenValue sym))) !(Integer -> SEval sym (GenValue sym))

lookupSeqMap :: SeqMap sym -> Integer -> SEval sym (GenValue sym)

finiteSeqMap :: Backend sym => sym -> [SEval sym (GenValue sym)] -> SeqMap sym

Generate a finite sequence map from a list of values

infiniteSeqMap :: Backend sym => [SEval sym (GenValue sym)] -> SEval sym (SeqMap sym)

Generate an infinite sequence map from a stream of values

enumerateSeqMap :: Integral n => n -> SeqMap sym -> [SEval sym (GenValue sym)]

Create a finite list of length n of the values from [0..n-1] in the given the sequence emap.

streamSeqMap :: SeqMap sym -> [SEval sym (GenValue sym)]

Create an infinite stream of all the values in a sequence map

reverseSeqMap

Arguments

:: Integer

Size of the sequence map

-> SeqMap sym

-> SeqMap sym

Reverse the order of a finite sequence map

updateSeqMap :: SeqMap sym -> Integer -> SEval sym (GenValue sym) -> SeqMap sym

dropSeqMap :: Integer -> SeqMap sym -> SeqMap sym

Drop the first n elements of the given SeqMap.

concatSeqMap :: Integer -> SeqMap sym -> SeqMap sym -> SeqMap sym

Concatenate the first n values of the first sequence map onto the beginning of the second sequence map.

splitSeqMap :: Integer -> SeqMap sym -> (SeqMap sym, SeqMap sym)

Given a number n and a sequence map, return two new sequence maps: the first containing the values from [0..n-1] and the next containing the values from n onward.

memoMap :: (MonadIO m, Backend sym) => SeqMap sym -> m (SeqMap sym)

Given a sequence map, return a new sequence map that is memoized using a finite map memo table.

zipSeqMap :: Backend sym => (GenValue sym -> GenValue sym -> SEval sym (GenValue sym)) -> SeqMap sym -> SeqMap sym -> SEval sym (SeqMap sym)

Apply the given evaluation function pointwise to the two given sequence maps.

mapSeqMap :: Backend sym => (GenValue sym -> SEval sym (GenValue sym)) -> SeqMap sym -> SEval sym (SeqMap sym)

Apply the given function to each value in the given sequence map

largeBitSize :: Integer

An arbitrarily-chosen number of elements where we switch from a dense sequence representation of bit-level words to SeqMap representation.

WordValue

data WordValue sym

For efficiency reasons, we handle finite sequences of bits as special cases in the evaluator. In cases where we know it is safe to do so, we prefer to used a "packed word" representation of bit sequences. This allows us to rely directly on Integer types (in the concrete evaluator) and SBV's Word types (in the symbolic simulator).

However, if we cannot be sure all the bits of the sequence will eventually be forced, we must instead rely on an explicit sequence of bits representation.

Constructors

WordVal !(SWord sym)

Packed word representation for bit sequences.

LargeBitsVal !Integer !(SeqMap sym)

A large bitvector sequence, represented as a SeqMap of bits.

Instances

Generic (WordValue sym)

Defined in Cryptol.Eval.Value

Associated Types

type Rep (WordValue sym) :: Type -> Type

Methods

from :: WordValue sym -> Rep (WordValue sym) x

to :: Rep (WordValue sym) x -> WordValue sym

type Rep (WordValue sym)

Defined in Cryptol.Eval.Value

type Rep (WordValue sym) = D1 ('MetaData "WordValue" "Cryptol.Eval.Value" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" 'False) (C1 ('MetaCons "WordVal" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (SWord sym))) :+: C1 ('MetaCons "LargeBitsVal" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Integer) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (SeqMap sym))))

asWordVal :: Backend sym => sym -> WordValue sym -> SEval sym (SWord sym)

Force a word value into packed word form

asBitsMap :: Backend sym => sym -> WordValue sym -> SeqMap sym

Force a word value into a sequence of bits

enumerateWordValue :: Backend sym => sym -> WordValue sym -> SEval sym [SBit sym]

Turn a word value into a sequence of bits, forcing each bit. The sequence is returned in big-endian order.

enumerateWordValueRev :: Backend sym => sym -> WordValue sym -> SEval sym [SBit sym]

Turn a word value into a sequence of bits, forcing each bit. The sequence is returned in reverse of the usual order, which is little-endian order.

wordValueSize :: Backend sym => sym -> WordValue sym -> Integer

Compute the size of a word value

indexWordValue :: Backend sym => sym -> WordValue sym -> Integer -> SEval sym (SBit sym)

Select an individual bit from a word value

updateWordValue :: Backend sym => sym -> WordValue sym -> Integer -> SEval sym (SBit sym) -> SEval sym (WordValue sym)

Produce a new WordValue from the one given by updating the ith bit with the given bit value.