Cryptol.Eval.Generic

Documentation

mkLit :: Backend sym => sym -> TValue -> Integer -> SEval sym (GenValue sym)

Make a numeric literal value at the given type.

ecNumberV :: Backend sym => sym -> GenValue sym

Make a numeric constant.

intV :: Backend sym => sym -> SInteger sym -> TValue -> SEval sym (GenValue sym)

ratioV :: Backend sym => sym -> GenValue sym

ecFractionV :: Backend sym => sym -> GenValue sym

fromZV :: Backend sym => sym -> GenValue sym

type Binary sym = TValue -> GenValue sym -> GenValue sym -> SEval sym (GenValue sym)

binary :: Backend sym => Binary sym -> GenValue sym

type Unary sym = TValue -> GenValue sym -> SEval sym (GenValue sym)

unary :: Backend sym => Unary sym -> GenValue sym

type BinWord sym = Integer -> SWord sym -> SWord sym -> SEval sym (SWord sym)

ringBinary :: forall sym. Backend sym => sym -> BinWord sym -> (SInteger sym -> SInteger sym -> SEval sym (SInteger sym)) -> (Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)) -> (SRational sym -> SRational sym -> SEval sym (SRational sym)) -> (SFloat sym -> SFloat sym -> SEval sym (SFloat sym)) -> Binary sym

type UnaryWord sym = Integer -> SWord sym -> SEval sym (SWord sym)

ringUnary :: forall sym. Backend sym => sym -> UnaryWord sym -> (SInteger sym -> SEval sym (SInteger sym)) -> (Integer -> SInteger sym -> SEval sym (SInteger sym)) -> (SRational sym -> SEval sym (SRational sym)) -> (SFloat sym -> SEval sym (SFloat sym)) -> Unary sym

ringNullary :: forall sym. Backend sym => sym -> (Integer -> SEval sym (SWord sym)) -> SEval sym (SInteger sym) -> (Integer -> SEval sym (SInteger sym)) -> SEval sym (SRational sym) -> (Integer -> Integer -> SEval sym (SFloat sym)) -> TValue -> SEval sym (GenValue sym)

integralBinary :: forall sym. Backend sym => sym -> BinWord sym -> (SInteger sym -> SInteger sym -> SEval sym (SInteger sym)) -> Binary sym

fromIntegerV :: Backend sym => sym -> GenValue sym

Convert an unbounded integer to a value in Ring

addV :: Backend sym => sym -> Binary sym

subV :: Backend sym => sym -> Binary sym

negateV :: Backend sym => sym -> Unary sym

mulV :: Backend sym => sym -> Binary sym

divV :: Backend sym => sym -> Binary sym

expV :: Backend sym => sym -> GenValue sym

computeExponent :: Backend sym => sym -> TValue -> GenValue sym -> [SBit sym] -> SEval sym (GenValue sym)

modV :: Backend sym => sym -> Binary sym

toIntegerV :: Backend sym => sym -> GenValue sym

Convert a word to a non-negative integer.

recipV :: Backend sym => sym -> GenValue sym

fieldDivideV :: Backend sym => sym -> GenValue sym

roundOp :: Backend sym => sym -> String -> (SRational sym -> SEval sym (SInteger sym)) -> (SFloat sym -> SEval sym (SInteger sym)) -> Unary sym

floorV :: Backend sym => sym -> Unary sym

ceilingV :: Backend sym => sym -> Unary sym

truncV :: Backend sym => sym -> Unary sym

roundAwayV :: Backend sym => sym -> Unary sym

roundToEvenV :: Backend sym => sym -> Unary sym

andV :: Backend sym => sym -> Binary sym

orV :: Backend sym => sym -> Binary sym

xorV :: Backend sym => sym -> Binary sym

complementV :: Backend sym => sym -> Unary sym

lg2V :: Backend sym => sym -> GenValue sym

sdivV :: Backend sym => sym -> GenValue sym

smodV :: Backend sym => sym -> GenValue sym

cmpValue :: Backend sym => sym -> (SBit sym -> SBit sym -> SEval sym a -> SEval sym a) -> (SWord sym -> SWord sym -> SEval sym a -> SEval sym a) -> (SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a) -> (Integer -> SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a) -> (SRational sym -> SRational sym -> SEval sym a -> SEval sym a) -> (SFloat sym -> SFloat sym -> SEval sym a -> SEval sym a) -> TValue -> GenValue sym -> GenValue sym -> SEval sym a -> SEval sym a

bitLessThan :: Backend sym => sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)

bitGreaterThan :: Backend sym => sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)

valEq :: Backend sym => sym -> TValue -> GenValue sym -> GenValue sym -> SEval sym (SBit sym)

valLt :: Backend sym => sym -> TValue -> GenValue sym -> GenValue sym -> SBit sym -> SEval sym (SBit sym)

valGt :: Backend sym => sym -> TValue -> GenValue sym -> GenValue sym -> SBit sym -> SEval sym (SBit sym)

eqCombine :: Backend sym => sym -> SEval sym (SBit sym) -> SEval sym (SBit sym) -> SEval sym (SBit sym)

lexCombine :: Backend sym => sym -> SEval sym (SBit sym) -> SEval sym (SBit sym) -> SEval sym (SBit sym) -> SEval sym (SBit sym)

eqV :: Backend sym => sym -> Binary sym

distinctV :: Backend sym => sym -> Binary sym

lessThanV :: Backend sym => sym -> Binary sym

lessThanEqV :: Backend sym => sym -> Binary sym

greaterThanV :: Backend sym => sym -> Binary sym

greaterThanEqV :: Backend sym => sym -> Binary sym

signedLessThanV :: Backend sym => sym -> Binary sym

zeroV :: forall sym. Backend sym => sym -> TValue -> SEval sym (GenValue sym)

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

joinWords :: forall sym. Backend sym => sym -> Integer -> Integer -> SeqMap sym -> SEval sym (GenValue sym)

joinSeq :: Backend sym => sym -> Nat' -> Integer -> TValue -> SeqMap sym -> SEval sym (GenValue sym)

joinV :: Backend sym => sym -> Nat' -> Integer -> TValue -> GenValue sym -> SEval sym (GenValue sym)

Join a sequence of sequences into a single sequence.

splitWordVal :: Backend sym => sym -> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym, WordValue sym)

splitAtV :: Backend sym => sym -> Nat' -> Nat' -> TValue -> GenValue sym -> SEval sym (GenValue sym)

extractWordVal :: Backend sym => sym -> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)

Extract a subsequence of bits from a WordValue. 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 `extractWordVal n i w` is equivalent to first shifting w right by i bits, and then truncating to n bits.

ecSplitV :: Backend sym => sym -> GenValue sym

Split implementation.

reverseV :: forall sym. Backend sym => sym -> GenValue sym -> SEval sym (GenValue sym)

transposeV :: Backend sym => sym -> Nat' -> Nat' -> TValue -> GenValue sym -> SEval sym (GenValue sym)

ccatV :: Backend sym => sym -> Nat' -> Nat' -> TValue -> GenValue sym -> GenValue sym -> SEval sym (GenValue sym)

wordValLogicOp :: Backend sym => sym -> (SBit sym -> SBit sym -> SEval sym (SBit sym)) -> (SWord sym -> SWord sym -> SEval sym (SWord sym)) -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)

logicBinary :: forall sym. Backend sym => sym -> (SBit sym -> SBit sym -> SEval sym (SBit sym)) -> (SWord sym -> SWord sym -> SEval sym (SWord sym)) -> Binary sym

Merge two values given a binop. This is used for and, or and xor.

wordValUnaryOp :: Backend sym => (SBit sym -> SEval sym (SBit sym)) -> (SWord sym -> SEval sym (SWord sym)) -> WordValue sym -> SEval sym (WordValue sym)

logicUnary :: forall sym. Backend sym => sym -> (SBit sym -> SEval sym (SBit sym)) -> (SWord sym -> SEval sym (SWord sym)) -> Unary sym

bitsValueLessThan

Arguments

:: Backend sym

=> sym

-> Integer

bit-width

-> [SBit sym]

big-endian list of index bits

-> Integer

Upper bound to test against

-> SEval sym (SBit sym)

assertIndexInBounds

Arguments

:: Backend sym

=> sym

-> Nat'

Sequence size bounds

-> Either (SInteger sym) (WordValue sym)

Index value

-> SEval sym ()

indexPrim :: Backend sym => sym -> (Nat' -> TValue -> SeqMap sym -> TValue -> SInteger sym -> SEval sym (GenValue sym)) -> (Nat' -> TValue -> SeqMap sym -> TValue -> [SBit sym] -> SEval sym (GenValue sym)) -> (Nat' -> TValue -> SeqMap sym -> TValue -> SWord sym -> SEval sym (GenValue sym)) -> GenValue sym

Indexing operations.

updatePrim :: Backend sym => sym -> (Nat' -> TValue -> WordValue sym -> Either (SInteger sym) (WordValue sym) -> SEval sym (GenValue sym) -> SEval sym (WordValue sym)) -> (Nat' -> TValue -> SeqMap sym -> Either (SInteger sym) (WordValue sym) -> SEval sym (GenValue sym) -> SEval sym (SeqMap sym)) -> GenValue sym

fromToV :: Backend sym => sym -> GenValue sym

fromThenToV :: Backend sym => sym -> GenValue sym

infFromV :: Backend sym => sym -> GenValue sym

infFromThenV :: Backend sym => sym -> GenValue sym

barrelShifter

Arguments

:: Backend sym

=> sym

-> (SeqMap sym -> Integer -> SEval sym (SeqMap sym))

concrete shifting operation

-> SeqMap sym

initial value

-> [SBit sym]

bits of shift amount, in big-endian order

-> SEval sym (SeqMap sym)

shiftLeftReindex :: Nat' -> Integer -> Integer -> Maybe Integer

shiftRightReindex :: Nat' -> Integer -> Integer -> Maybe Integer

rotateLeftReindex :: Nat' -> Integer -> Integer -> Maybe Integer

rotateRightReindex :: Nat' -> Integer -> Integer -> Maybe Integer

enumerateIntBits :: Backend sym => sym -> Nat' -> TValue -> SInteger sym -> SEval sym [SBit sym]

Compute the list of bits in an integer in big-endian order. Fails if neither the sequence length nor the type value provide an upper bound for the integer.

enumerateIntBits' :: Backend sym => sym -> Integer -> SInteger sym -> SEval sym [SBit sym]

Compute the list of bits in an integer in big-endian order. The integer argument is a concrete upper bound for the symbolic integer.

logicShift

Arguments

:: Backend sym

=> sym

-> String

-> (sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym))

operation for range reduction on integers

-> (SWord sym -> SWord sym -> SEval sym (SWord sym))

word shift operation for positive indices

-> (SWord sym -> SWord sym -> SEval sym (SWord sym))

word shift operation for negative indices

-> (Nat' -> Integer -> Integer -> Maybe Integer)

reindexing operation for positive indices (sequence size, starting index, shift amount

-> (Nat' -> Integer -> Integer -> Maybe Integer)

reindexing operation for negative indices (sequence size, starting index, shift amount

-> GenValue sym

Generic implementation of shifting. Uses the provided word-level operation to perform the shift, when possible. Otherwise falls back on a barrel shifter that uses the provided reindexing operation to implement the concrete shifting operations. The reindex operation is given the size of the sequence, the requested index value for the new output sequence, and the amount to shift. The return value is an index into the original sequence if in bounds, and Nothing otherwise.

intShifter :: Backend sym => sym -> String -> (SWord sym -> SWord sym -> SEval sym (SWord sym)) -> (Nat' -> Integer -> Integer -> Maybe Integer) -> Nat' -> TValue -> TValue -> GenValue sym -> SInteger sym -> SEval sym (GenValue sym)

wordShifter :: Backend sym => sym -> String -> (SWord sym -> SWord sym -> SEval sym (SWord sym)) -> (Nat' -> Integer -> Integer -> Maybe Integer) -> Nat' -> TValue -> GenValue sym -> WordValue sym -> SEval sym (GenValue sym)

shiftShrink :: Backend sym => sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)

rotateShrink :: Backend sym => sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)

errorV :: forall sym. Backend sym => sym -> TValue -> String -> SEval sym (GenValue sym)

valueToChar :: Backend sym => sym -> GenValue sym -> SEval sym Char

Expect a word value. Mask it to an 8-bits ASCII value and return the associated character, if it is concrete. Otherwise, return a ? character

valueToString :: Backend sym => sym -> GenValue sym -> SEval sym String

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

mergeWord :: Backend sym => sym -> SBit sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)

mergeWord' :: Backend sym => sym -> SBit sym -> SEval sym (WordValue sym) -> SEval sym (WordValue sym) -> SEval sym (WordValue sym)

mergeValue' :: 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)

mergeSeqMap :: Backend sym => sym -> SBit sym -> SeqMap sym -> SeqMap sym -> SeqMap sym

foldlV :: Backend sym => sym -> GenValue sym

foldl'V :: Backend sym => sym -> GenValue sym

randomV :: Backend sym => sym -> TValue -> Integer -> SEval sym (GenValue sym)

Produce a random value with the given seed. If we do not support making values of the given type, return zero of that type. TODO: do better than returning zero

parmapV :: Backend sym => sym -> GenValue sym

sparkParMap :: Backend sym => sym -> (SEval sym (GenValue sym) -> SEval sym (GenValue sym)) -> Integer -> SeqMap sym -> SEval sym (SeqMap sym)

fpBinArithV :: Backend sym => sym -> FPArith2 sym -> GenValue sym

Make a Cryptol value for a binary arithmetic function.

fpRndMode :: Backend sym => sym -> SEval sym (SWord sym)

Rounding mode used in FP operations that do not specify it explicitly.

fpRndRNE :: Backend sym => sym -> SEval sym (SWord sym)

Rounding mode used in FP operations that do not specify it explicitly.

fpRndRNA :: Backend sym => sym -> SEval sym (SWord sym)

Rounding mode used in FP operations that do not specify it explicitly.

fpRndRTP :: Backend sym => sym -> SEval sym (SWord sym)

Rounding mode used in FP operations that do not specify it explicitly.

fpRndRTN :: Backend sym => sym -> SEval sym (SWord sym)

Rounding mode used in FP operations that do not specify it explicitly.

fpRndRTZ :: Backend sym => sym -> SEval sym (SWord sym)

Rounding mode used in FP operations that do not specify it explicitly.