cryptol-2.9.0: Cryptol: The Language of Cryptography

Copyright(c) 2013-2020 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe
LanguageHaskell2010

Cryptol.Eval.Generic

Description

 
Synopsis

Documentation

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

Make a numeric literal value at the given type.

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

Make a numeric constant.

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

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

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

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

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

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

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

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

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

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 Source #

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

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 Source #

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) Source #

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

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

Convert an unbounded integer to a value in Ring

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

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

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

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

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

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

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

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

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

Convert a word to a non-negative integer.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Join a sequence of sequences into a single sequence.

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

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

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

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 Source #

Split implementation.

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

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

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

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) Source #

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

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) Source #

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

bitsValueLessThan Source #

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 Source #

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 Source #

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 Source #

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

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

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

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

barrelShifter Source #

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 Source #

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

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

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

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

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] Source #

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 Source #

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) Source #

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) Source #

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

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

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

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

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 Source #

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

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

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

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

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

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

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

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

Make a Cryptol value for a binary arithmetic function.

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

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

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

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

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

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

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

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

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

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

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

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