cryptol-2.4.0: Cryptol: The Language of Cryptography

Cryptol.Symbolic.Prims

Description

Synopsis

# Documentation

traverseSnd :: Functor f => (a -> f b) -> (t, a) -> f (t, b) Source #

atV :: Bool -> Value -> [Value] -> Value -> Value Source #

Arguments

 :: Integer number of elements -> TValue type of element -> Value element -> Value

nth :: a -> [a] -> Int -> a Source #

mapV :: Bool -> (Value -> Value) -> Value -> Value Source #

Make a numeric constant. { val, bits } (fin val, fin bits, bits >= width val) => [bits]

arithBinary :: (SWord -> SWord -> SWord) -> Binary Source #

Models functions of type {a} (Arith a) => a -> a -> a

arithUnary :: (SWord -> SWord) -> Unary Source #

Models functions of type {a} (Arith a) => a -> a

Ceiling (log_2 x)

cmpValue :: (SBool -> SBool -> a -> a) -> (SWord -> SWord -> a -> a) -> Value -> Value -> a -> a Source #

cmpBinary :: (SBool -> SBool -> SBool -> SBool) -> (SWord -> SWord -> SBool -> SBool) -> SBool -> Binary Source #

joinV :: Nat' -> Nat' -> TValue -> Value -> Value Source #

Join a sequence of sequences into a single sequence.

Split implementation.

infChunksOf :: Integer -> [a] -> [[a]] Source #

Split into infinitely many chunks

finChunksOf :: Integer -> Integer -> [a] -> [[a]] Source #

Split into finitely many chunks

logicBinary :: (SBool -> SBool -> SBool) -> (SWord -> SWord -> SWord) -> Binary Source #

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

addPoly :: [SBool] -> [SBool] -> [SBool] Source #