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 -> Prim sym

Make a numeric constant.

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

ratioV :: Backend sym => sym -> Prim sym

ecFractionV :: Backend sym => sym -> Prim sym

fromZV :: Backend sym => sym -> Prim sym

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

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

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

unary :: Backend sym => Unary sym -> Prim 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 -> Prim 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 -> Prim sym

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

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

toIntegerV :: Backend sym => sym -> Prim sym

Convert a word to a non-negative integer.

recipV :: Backend sym => sym -> Prim sym

fieldDivideV :: Backend sym => sym -> Prim 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 -> Prim sym

sdivV :: Backend sym => sym -> Prim sym

smodV :: Backend sym => sym -> Prim sym

toSignedIntegerV :: Backend sym => sym -> Prim 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)

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

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

Join a sequence of sequences into a single sequence.

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

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

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

Split implementation.

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

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

ccatV :: Backend sym => sym -> Integer -> Nat' -> TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym) -> SEval sym (GenValue 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.

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

assertIndexInBounds

Arguments

:: Backend sym

=> sym

-> Nat'

Sequence size bounds

-> Either (SInteger sym) (WordValue sym)

Index value

-> SEval sym ()

indexPrim :: Backend sym => sym -> IndexDirection -> (Nat' -> TValue -> SeqMap sym (GenValue sym) -> TValue -> SInteger sym -> SEval sym (GenValue sym)) -> (Nat' -> TValue -> SeqMap sym (GenValue sym) -> TValue -> Integer -> [IndexSegment sym] -> SEval sym (GenValue sym)) -> Prim 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 (GenValue sym) -> Either (SInteger sym) (WordValue sym) -> SEval sym (GenValue sym) -> SEval sym (SeqMap sym (GenValue sym))) -> Prim sym

fromToV :: Backend sym => sym -> Prim sym

fromThenToV :: Backend sym => sym -> Prim sym

fromToLessThanV :: Backend sym => sym -> Prim sym

fromToByV :: Backend sym => sym -> Prim sym

fromToByLessThanV :: Backend sym => sym -> Prim sym

fromToDownByV :: Backend sym => sym -> Prim sym

fromToDownByGreaterThanV :: Backend sym => sym -> Prim sym

infFromV :: Backend sym => sym -> Prim sym

infFromThenV :: Backend sym => sym -> Prim 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

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

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

sshrV :: Backend sym => sym -> Prim 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

foldlV :: Backend sym => sym -> Prim sym

foldl'V :: Backend sym => sym -> Prim 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 -> Prim sym

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

fpConst :: Backend sym => (Integer -> Integer -> SEval sym (SFloat sym)) -> Prim sym

A helper for definitng floating point constants.

fpBinArithV :: Backend sym => sym -> FPArith2 sym -> Prim 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.

genericFloatTable :: Backend sym => sym -> Map PrimIdent (Prim sym)

genericPrimTable :: Backend sym => sym -> IO EvalOpts -> Map PrimIdent (Prim sym)