cryptol-2.4.0: Cryptol: The Language of Cryptography

Copyright | (c) 2013-2016 Galois Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | None
Language | Haskell98

Cryptol.Symbolic.Prims

Description

Synopsis

- traverseSnd :: Functor f => (a -> f b) -> (t, a) -> f (t, b)
- evalPrim :: Decl -> Value
- primTable :: Map Ident Value
- selectV :: (Integer -> Value) -> Value -> Value
- asWordList :: [Value] -> Maybe [SWord]
- atV_list :: Bool -> Bool -> Value -> [Value] -> Value -> Value
- atV :: Bool -> Value -> [Value] -> Value -> Value
- iteAtV :: Value -> [Value] -> Value -> Value
- replicateV :: Integer -> TValue -> Value -> Value
- nth :: a -> [a] -> Int -> a
- nthV :: Value -> Value -> Integer -> Value
- mapV :: Bool -> (Value -> Value) -> Value -> Value
- catV :: Value -> Value -> Value
- dropV :: Integer -> Value -> Value
- takeV :: Integer -> Value -> Value
- ecDemoteV :: Value
- type Binary = TValue -> Value -> Value -> Value
- type Unary = TValue -> Value -> Value
- arithBinary :: (SWord -> SWord -> SWord) -> Binary
- arithUnary :: (SWord -> SWord) -> Unary
- sExp :: SWord -> SWord -> SWord
- sLg2 :: SWord -> SWord
- cmpValue :: (SBool -> SBool -> a -> a) -> (SWord -> SWord -> a -> a) -> Value -> Value -> a -> a
- cmpEq :: SWord -> SWord -> SBool -> SBool
- cmpNotEq :: SWord -> SWord -> SBool -> SBool
- cmpLt :: SWord -> SWord -> SBool -> SBool
- cmpGt :: SWord -> SWord -> SBool -> SBool
- cmpLtEq :: SWord -> SWord -> SBool -> SBool
- cmpGtEq :: SWord -> SWord -> SBool -> SBool
- cmpBinary :: (SBool -> SBool -> SBool -> SBool) -> (SWord -> SWord -> SBool -> SBool) -> SBool -> Binary
- errorV :: String -> TValue -> Value
- zeroV :: TValue -> Value
- joinV :: Nat' -> Nat' -> TValue -> Value -> Value
- ecSplitV :: Value
- infChunksOf :: Integer -> [a] -> [[a]]
- finChunksOf :: Integer -> Integer -> [a] -> [[a]]
- logicBinary :: (SBool -> SBool -> SBool) -> (SWord -> SWord -> SWord) -> Binary
- logicUnary :: (SBool -> SBool) -> (SWord -> SWord) -> Unary
- fromThenV :: Value
- fromToV :: Value
- fromThenToV :: Value
- addPoly :: [SBool] -> [SBool] -> [SBool]
- ites :: SBool -> [SBool] -> [SBool] -> [SBool]
- degree :: [SBool] -> Int
- mdp :: [SBool] -> [SBool] -> ([SBool], [SBool])
- idx :: [SBool] -> Int -> SBool
- divx :: Int -> Int -> [SBool] -> [SBool] -> ([SBool], [SBool])

# Documentation

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

evalPrim :: Decl -> Value Source #

primTable :: Map Ident Value Source #

selectV :: (Integer -> Value) -> Value -> Value Source #

asWordList :: [Value] -> Maybe [SWord] Source #

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

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

iteAtV :: Value -> [Value] -> Value -> Value Source #

replicateV Source #

Arguments

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

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

nthV :: Value -> Value -> Integer -> Value Source #

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

catV :: Value -> Value -> Value Source #

dropV :: Integer -> Value -> Value Source #

takeV :: Integer -> Value -> Value Source #

ecDemoteV :: Value Source #

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

type Binary = TValue -> Value -> Value -> Value Source #

type Unary = TValue -> Value -> Value Source #

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`

sExp :: SWord -> SWord -> SWord Source #

sLg2 :: SWord -> SWord Source #

Ceiling (log_2 x)

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

cmpEq :: SWord -> SWord -> SBool -> SBool Source #

cmpNotEq :: SWord -> SWord -> SBool -> SBool Source #

cmpLt :: SWord -> SWord -> SBool -> SBool Source #

cmpGt :: SWord -> SWord -> SBool -> SBool Source #

cmpLtEq :: SWord -> SWord -> SBool -> SBool Source #

cmpGtEq :: SWord -> SWord -> SBool -> SBool Source #

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

errorV :: String -> TValue -> Value Source #

zeroV :: TValue -> Value Source #

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

Join a sequence of sequences into a single sequence.

ecSplitV :: Value Source #

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.

logicUnary :: (SBool -> SBool) -> (SWord -> SWord) -> Unary Source #

fromThenV :: Value Source #

fromToV :: Value Source #

fromThenToV :: Value Source #

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

Add two polynomials

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

degree :: [SBool] -> Int Source #

mdp :: [SBool] -> [SBool] -> ([SBool], [SBool]) Source #

idx :: [SBool] -> Int -> SBool Source #

divx :: Int -> Int -> [SBool] -> [SBool] -> ([SBool], [SBool]) Source #