Cryptol.Backend.WordValue

WordValue

data WordValue sym

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

Generic (WordValue sym)

Defined in Cryptol.Backend.WordValue

Associated Types

type Rep (WordValue sym) :: Type -> Type

Methods

from :: WordValue sym -> Rep (WordValue sym) x

to :: Rep (WordValue sym) x -> WordValue sym

type Rep (WordValue sym)

Defined in Cryptol.Backend.WordValue

type Rep (WordValue sym) = D1 ('MetaData "WordValue" "Cryptol.Backend.WordValue" "cryptol-2.12.0-1cEC2pVyc8sLwNRndAigau" '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

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)

Force a word value into packed word form

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

Force a word value into a sequence of bits

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)

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)

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]

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]

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]

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

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)

Select an individual bit from a word value

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

Produce a new WordValue from the one given by updating the ith bit with the given bit value.

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

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

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

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)

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

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

Force the evaluation of a word value

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

updateWordByWord

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)

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