cryptol-3.0.0: Cryptol: The Language of Cryptography

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

Cryptol.Backend.WordValue

Contents

- WordValue

Description

Synopsis

- data WordValue sym
- wordVal :: SWord sym -> WordValue sym
- bitmapWordVal :: Backend sym => sym -> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
- asWordList :: forall sym. Backend sym => sym -> [WordValue sym] -> SEval sym (Maybe [SWord sym])
- asWordVal :: Backend sym => sym -> WordValue sym -> SEval sym (SWord sym)
- asBitsMap :: Backend sym => sym -> WordValue sym -> SeqMap sym (SBit sym)
- joinWordVal :: Backend sym => sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)
- takeWordVal :: Backend sym => sym -> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
- dropWordVal :: Backend sym => sym -> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
- extractWordVal :: Backend sym => sym -> Integer -> Integer -> WordValue sym -> SEval sym (WordValue sym)
- 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)
- wordValUnaryOp :: Backend sym => sym -> (SBit sym -> SEval sym (SBit sym)) -> (SWord sym -> SEval sym (SWord sym)) -> WordValue sym -> SEval sym (WordValue sym)
- assertWordValueInBounds :: Backend sym => sym -> Integer -> WordValue sym -> SEval sym ()
- enumerateWordValue :: Backend sym => sym -> WordValue sym -> SEval sym [SBit sym]
- enumerateWordValueRev :: Backend sym => sym -> WordValue sym -> SEval sym [SBit sym]
- enumerateIndexSegments :: Backend sym => sym -> WordValue sym -> SEval sym [IndexSegment sym]
- wordValueSize :: Backend sym => sym -> WordValue sym -> Integer
- indexWordValue :: Backend sym => sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
- updateWordValue :: Backend sym => sym -> WordValue sym -> Integer -> SEval sym (SBit sym) -> SEval sym (WordValue sym)
- delayWordValue :: Backend sym => sym -> Integer -> SEval sym (WordValue sym) -> SEval sym (WordValue sym)
- joinWords :: forall sym. Backend sym => sym -> Integer -> Integer -> SeqMap sym (WordValue sym) -> SEval sym (WordValue sym)
- shiftSeqByWord :: Backend sym => sym -> (SBit sym -> a -> a -> SEval sym a) -> (Integer -> Integer -> Maybe Integer) -> SEval sym a -> Nat' -> SeqMap sym a -> WordValue sym -> SEval sym (SeqMap sym a)
- shiftWordByInteger :: Backend sym => sym -> (SWord sym -> SWord sym -> SEval sym (SWord sym)) -> (Integer -> Integer -> Maybe Integer) -> WordValue sym -> SInteger sym -> SEval sym (WordValue sym)
- shiftWordByWord :: Backend sym => sym -> (SWord sym -> SWord sym -> SEval sym (SWord sym)) -> (Integer -> Integer -> Maybe Integer) -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)
- wordValAsLit :: Backend sym => sym -> WordValue sym -> SEval sym (Maybe Integer)
- reverseWordVal :: Backend sym => sym -> WordValue sym -> SEval sym (WordValue sym)
- forceWordValue :: Backend sym => WordValue sym -> SEval sym ()
- wordValueEqualsInteger :: forall sym. Backend sym => sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
- updateWordByWord :: Backend sym => sym -> IndexDirection -> WordValue sym -> WordValue sym -> SEval sym (SBit sym) -> SEval sym (WordValue sym)
- mergeWord :: Backend sym => sym -> SBit sym -> WordValue sym -> WordValue sym -> SEval sym (WordValue sym)
- mergeWord' :: Backend sym => sym -> SBit sym -> SEval sym (WordValue sym) -> SEval sym (WordValue sym) -> SEval sym (WordValue sym)

# WordValue

data WordValue sym Source #

For efficiency reasons, we handle finite sequences of bits as special cases in the evaluator. In cases where we know it is safe to do so, we prefer to used a "packed word" representation of bit sequences. This allows us to rely directly on Integer types (in the concrete evaluator) and SBV's Word types (in the symbolic simulator).

However, if we cannot be sure all the bits of the sequence will eventually be forced, we must instead rely on an explicit sequence of bits representation.

#### Instances

Instances details

Generic (WordValue sym) Source # |
Instance details Defined in Cryptol.Backend.WordValue Associated Types type Rep (WordValue sym) :: Type -> Type Source # Methods from :: WordValue sym -> Rep (WordValue sym) x Source # to :: Rep (WordValue sym) x -> WordValue sym Source #
type Rep (WordValue sym) Source # |

Instance details

Defined in Cryptol.Backend.WordValue

type Rep (WordValue sym) = D1 ('MetaData "WordValue" "Cryptol.Backend.WordValue" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "ThunkWordVal" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (SEval sym (WordValue sym)))) :+: (C1 ('MetaCons "WordVal" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (SWord sym))) :+: C1 ('MetaCons "BitmapVal" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Integer) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (SEval sym (SWord sym))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (SeqMap sym (SBit sym)))))))

wordVal :: SWord sym -> WordValue sym Source #

bitmapWordVal :: Backend sym => sym -> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym) Source #

asWordList :: forall sym. Backend sym => sym -> [WordValue sym] -> SEval sym (Maybe [SWord sym]) Source #

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

Force a word value into packed word form

asBitsMap :: Backend sym => sym -> WordValue sym -> SeqMap sym (SBit sym) Source #

Force a word value into a sequence of bits

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

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

dropWordVal :: Backend sym => sym -> Integer -> Integer -> WordValue sym -> SEval sym (WordValue 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.

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 #

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

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

enumerateWordValue :: Backend sym => sym -> WordValue sym -> SEval sym [SBit sym] Source #

Turn a word value into a sequence of bits, forcing each bit. The sequence is returned in big-endian order.

enumerateWordValueRev :: Backend sym => sym -> WordValue sym -> SEval sym [SBit sym] Source #

Turn a word value into a sequence of bits, forcing each bit. The sequence is returned in reverse of the usual order, which is little-endian order.

enumerateIndexSegments :: Backend sym => sym -> WordValue sym -> SEval sym [IndexSegment sym] Source #

wordValueSize :: Backend sym => sym -> WordValue sym -> Integer Source #

Compute the size of a word value TODO, can we get rid of this? If feels like it should be unnecessary.

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

Select an individual bit from a word value

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

Produce a new `WordValue` from the one given by updating the `i`th bit with the given bit value.

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

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

shiftSeqByWord Source #

Arguments

:: Backend sym |
=> sym |
-> (SBit sym -> a -> a -> SEval sym a) | ifthenelse operation of values
-> (Integer -> Integer -> Maybe Integer) | reindexing operation
-> SEval sym a | zero value
-> Nat' | size of the sequence
-> SeqMap sym a | sequence to shift
-> WordValue sym | shift amount
-> SEval sym (SeqMap sym a) |

shiftWordByInteger Source #

Arguments

:: Backend sym |
=> sym |
-> (SWord sym -> SWord sym -> SEval sym (SWord sym)) | operation on word values
-> (Integer -> Integer -> Maybe Integer) | reindexing operation
-> WordValue sym | word value to shift
-> SInteger sym | shift amount, assumed to be in range [0,len]
-> SEval sym (WordValue sym) |

shiftWordByWord Source #

Arguments

:: Backend sym |
=> sym |
-> (SWord sym -> SWord sym -> SEval sym (SWord sym)) | operation on word values
-> (Integer -> Integer -> Maybe Integer) | reindexing operation
-> WordValue sym | value to shift
-> WordValue sym | amount to shift
-> SEval sym (WordValue sym) |

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

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

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

Force the evaluation of a word value

wordValueEqualsInteger :: forall sym. Backend sym => sym -> WordValue sym -> Integer -> SEval sym (SBit sym) Source #

updateWordByWord Source #

Arguments

:: Backend sym |
=> sym |
-> IndexDirection |
-> WordValue sym | value to update
-> WordValue sym | index to update at
-> SEval sym (SBit sym) | fresh bit
-> SEval sym (WordValue sym) |

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 #