cryptol-2.6.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 | Haskell2010

Cryptol.Symbolic.Prims

Contents

- Orphan instances

Description

Synopsis

- traverseSnd :: Functor f => (a -> f b) -> (t, a) -> f (t, b)
- primTable :: Map Ident Value
- shifter :: Monad m => (SBool -> a -> a -> a) -> (a -> Integer -> m a) -> a -> [SBool] -> m a
- logicShift :: String -> (SWord -> SWord -> SWord) -> (Nat' -> Integer -> Integer -> Maybe Integer) -> Value
- selectV :: forall a. (SBool -> Eval a -> Eval a -> Eval a) -> WordValue SBool SWord SInteger -> (Integer -> Eval a) -> Eval a
- indexFront :: Maybe Integer -> TValue -> SeqMap SBool SWord SInteger -> SWord -> Eval Value
- indexBack :: Maybe Integer -> TValue -> SeqMap SBool SWord SInteger -> SWord -> Eval Value
- indexFront_bits :: Maybe Integer -> TValue -> SeqMap SBool SWord SInteger -> Seq SBool -> Eval Value
- indexBack_bits :: Maybe Integer -> TValue -> SeqMap SBool SWord SInteger -> Seq SBool -> Eval Value
- updateFrontSym :: Nat' -> TValue -> SeqMap SBool SWord SInteger -> WordValue SBool SWord SInteger -> Eval (GenValue SBool SWord SInteger) -> Eval (SeqMap SBool SWord SInteger)
- updateFrontSym_word :: Nat' -> TValue -> WordValue SBool SWord SInteger -> WordValue SBool SWord SInteger -> Eval (GenValue SBool SWord SInteger) -> Eval (WordValue SBool SWord SInteger)
- updateBackSym :: Nat' -> TValue -> SeqMap SBool SWord SInteger -> WordValue SBool SWord SInteger -> Eval (GenValue SBool SWord SInteger) -> Eval (SeqMap SBool SWord SInteger)
- updateBackSym_word :: Nat' -> TValue -> WordValue SBool SWord SInteger -> WordValue SBool SWord SInteger -> Eval (GenValue SBool SWord SInteger) -> Eval (WordValue SBool SWord SInteger)
- asBitList :: [Eval SBool] -> Maybe [SBool]
- asWordList :: [WordValue SBool SWord SInteger] -> Maybe [SWord]
- liftBinArith :: (SWord -> SWord -> SWord) -> BinArith SWord
- liftBin :: (a -> b -> c) -> a -> b -> Eval c
- liftModBin :: (SInteger -> SInteger -> a) -> Integer -> SInteger -> SInteger -> Eval a
- sExp :: Integer -> SWord -> SWord -> Eval SWord
- sModExp :: Integer -> SInteger -> SInteger -> Eval SInteger
- sLg2 :: Integer -> SWord -> Eval SWord
- svLg2 :: SInteger -> Eval SInteger
- svModLg2 :: Integer -> SInteger -> Eval SInteger
- cmpEq :: SWord -> SWord -> Eval SBool -> Eval SBool
- cmpNotEq :: SWord -> SWord -> Eval SBool -> Eval SBool
- cmpSignedLt :: SWord -> SWord -> Eval SBool -> Eval SBool
- cmpLt :: SWord -> SWord -> Eval SBool -> Eval SBool
- cmpGt :: SWord -> SWord -> Eval SBool -> Eval SBool
- cmpLtEq :: SWord -> SWord -> Eval SBool -> Eval SBool
- cmpGtEq :: SWord -> SWord -> Eval SBool -> Eval SBool
- cmpMod :: (SInteger -> SInteger -> Eval SBool -> Eval SBool) -> Integer -> SInteger -> SInteger -> Eval SBool -> Eval SBool
- cmpModEq :: Integer -> SInteger -> SInteger -> Eval SBool -> Eval SBool
- cmpModNotEq :: Integer -> SInteger -> SInteger -> Eval SBool -> Eval SBool
- svDivisible :: Integer -> SInteger -> SBool
- cmpBinary :: (SBool -> SBool -> Eval SBool -> Eval SBool) -> (SWord -> SWord -> Eval SBool -> Eval SBool) -> (SInteger -> SInteger -> Eval SBool -> Eval SBool) -> (Integer -> SInteger -> SInteger -> Eval SBool -> Eval SBool) -> SBool -> Binary SBool SWord SInteger
- signedQuot :: SWord -> SWord -> SWord
- signedRem :: SWord -> SWord -> SWord
- sshrV :: Value
- carry :: SWord -> SWord -> Eval Value
- scarry :: SWord -> SWord -> Eval Value

# Documentation

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

primTable :: Map Ident Value Source #

shifter :: Monad m => (SBool -> a -> a -> a) -> (a -> Integer -> m a) -> a -> [SBool] -> m a Source #

Barrel-shifter algorithm. Takes a list of bits in big-endian order.

logicShift :: String -> (SWord -> SWord -> SWord) -> (Nat' -> Integer -> Integer -> Maybe Integer) -> Value Source #

selectV Source #

Arguments

:: (SBool -> Eval a -> Eval a -> Eval a) | Mux function on `a`s
-> WordValue SBool SWord SInteger | Symbolic index value
-> (Integer -> Eval a) | Function from concrete indices to answers
-> Eval a | overall answer

indexFront :: Maybe Integer -> TValue -> SeqMap SBool SWord SInteger -> SWord -> Eval Value Source #

indexBack :: Maybe Integer -> TValue -> SeqMap SBool SWord SInteger -> SWord -> Eval Value Source #

indexFront_bits :: Maybe Integer -> TValue -> SeqMap SBool SWord SInteger -> Seq SBool -> Eval Value Source #

indexBack_bits :: Maybe Integer -> TValue -> SeqMap SBool SWord SInteger -> Seq SBool -> Eval Value Source #

updateFrontSym :: Nat' -> TValue -> SeqMap SBool SWord SInteger -> WordValue SBool SWord SInteger -> Eval (GenValue SBool SWord SInteger) -> Eval (SeqMap SBool SWord SInteger) Source #

updateFrontSym_word :: Nat' -> TValue -> WordValue SBool SWord SInteger -> WordValue SBool SWord SInteger -> Eval (GenValue SBool SWord SInteger) -> Eval (WordValue SBool SWord SInteger) Source #

updateBackSym :: Nat' -> TValue -> SeqMap SBool SWord SInteger -> WordValue SBool SWord SInteger -> Eval (GenValue SBool SWord SInteger) -> Eval (SeqMap SBool SWord SInteger) Source #

updateBackSym_word :: Nat' -> TValue -> WordValue SBool SWord SInteger -> WordValue SBool SWord SInteger -> Eval (GenValue SBool SWord SInteger) -> Eval (WordValue SBool SWord SInteger) Source #

asBitList :: [Eval SBool] -> Maybe [SBool] Source #

asWordList :: [WordValue SBool SWord SInteger] -> Maybe [SWord] Source #

liftBinArith :: (SWord -> SWord -> SWord) -> BinArith SWord Source #

liftBin :: (a -> b -> c) -> a -> b -> Eval c Source #

liftModBin :: (SInteger -> SInteger -> a) -> Integer -> SInteger -> SInteger -> Eval a Source #

sExp :: Integer -> SWord -> SWord -> Eval SWord Source #

sModExp :: Integer -> SInteger -> SInteger -> Eval SInteger Source #

sLg2 :: Integer -> SWord -> Eval SWord Source #

Ceiling (log_2 x)

svLg2 :: SInteger -> Eval SInteger Source #

Ceiling (log_2 x)

svModLg2 :: Integer -> SInteger -> Eval SInteger Source #

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

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

cmpSignedLt :: SWord -> SWord -> Eval SBool -> Eval SBool Source #

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

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

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

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

cmpMod :: (SInteger -> SInteger -> Eval SBool -> Eval SBool) -> Integer -> SInteger -> SInteger -> Eval SBool -> Eval SBool Source #

cmpModEq :: Integer -> SInteger -> SInteger -> Eval SBool -> Eval SBool Source #

cmpModNotEq :: Integer -> SInteger -> SInteger -> Eval SBool -> Eval SBool Source #

svDivisible :: Integer -> SInteger -> SBool Source #

cmpBinary :: (SBool -> SBool -> Eval SBool -> Eval SBool) -> (SWord -> SWord -> Eval SBool -> Eval SBool) -> (SInteger -> SInteger -> Eval SBool -> Eval SBool) -> (Integer -> SInteger -> SInteger -> Eval SBool -> Eval SBool) -> SBool -> Binary SBool SWord SInteger Source #

signedQuot :: SWord -> SWord -> SWord Source #

signedRem :: SWord -> SWord -> SWord Source #

sshrV :: Value Source #

carry :: SWord -> SWord -> Eval Value Source #

scarry :: SWord -> SWord -> Eval Value Source #

# Orphan instances

EvalPrims SBool SWord SInteger Source # |
Instance details Methods evalPrim :: Decl -> GenValue SBool SWord SInteger Source # iteValue :: SBool -> Eval (GenValue SBool SWord SInteger) -> Eval (GenValue SBool SWord SInteger) -> Eval (GenValue SBool SWord SInteger) Source #