cryptol-2.8.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.Value

Contents

- Orphan instances

Description

Synopsis

- type SBool = SVal
- type SWord = SVal
- type SInteger = SVal
- literalSWord :: Int -> Integer -> SWord
- fromBitsLE :: [SBool] -> SWord
- forallBV_ :: Int -> Symbolic SWord
- existsBV_ :: Int -> Symbolic SWord
- forallSBool_ :: Symbolic SBool
- existsSBool_ :: Symbolic SBool
- forallSInteger_ :: Symbolic SBool
- existsSInteger_ :: Symbolic SBool
- type Value = GenValue SBool SWord SInteger
- data TValue
- isTBit :: TValue -> Bool
- tvSeq :: Nat' -> TValue -> TValue
- data GenValue b w i
  - = VRecord ![(Ident, Eval (GenValue b w i))]
  - | VTuple ![Eval (GenValue b w i)]
  - | VBit !b
  - | VInteger !i
  - | VSeq !Integer !(SeqMap b w i)
  - | VWord !Integer !(Eval (WordValue b w i))
  - | VStream !(SeqMap b w i)
  - | VFun (Eval (GenValue b w i) -> Eval (GenValue b w i))
  - | VPoly (TValue -> Eval (GenValue b w i))
  - | VNumPoly (Nat' -> Eval (GenValue b w i))
- lam :: (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
- tlam :: (TValue -> GenValue b w i) -> GenValue b w i
- toStream :: [GenValue b w i] -> Eval (GenValue b w i)
- toFinSeq :: BitWord b w i => Integer -> TValue -> [GenValue b w i] -> GenValue b w i
- toSeq :: BitWord b w i => Nat' -> TValue -> [GenValue b w i] -> Eval (GenValue b w i)
- fromVBit :: GenValue b w i -> b
- fromVFun :: GenValue b w i -> Eval (GenValue b w i) -> Eval (GenValue b w i)
- fromVPoly :: GenValue b w i -> TValue -> Eval (GenValue b w i)
- fromVTuple :: GenValue b w i -> [Eval (GenValue b w i)]
- fromVRecord :: GenValue b w i -> [(Ident, Eval (GenValue b w i))]
- lookupRecord :: Ident -> GenValue b w i -> Eval (GenValue b w i)
- fromSeq :: forall b w i. BitWord b w i => String -> GenValue b w i -> Eval (SeqMap b w i)
- fromVWord :: BitWord b w i => String -> GenValue b w i -> Eval w
- evalPanic :: String -> [String] -> a
- iteSValue :: SBool -> Value -> Value -> Eval Value
- mergeValue :: Bool -> SBool -> Value -> Value -> Eval Value
- mergeWord :: Bool -> SBool -> WordValue SBool SWord SInteger -> WordValue SBool SWord SInteger -> WordValue SBool SWord SInteger
- mergeBit :: Bool -> SBool -> SBool -> SBool -> SBool
- mergeBits :: Bool -> SBool -> Seq (Eval SBool) -> Seq (Eval SBool) -> Seq (Eval SBool)
- mergeSeqMap :: Bool -> SBool -> SeqMap SBool SWord SInteger -> SeqMap SBool SWord SInteger -> SeqMap SBool SWord SInteger
- mergeWord' :: Bool -> SBool -> Eval (WordValue SBool SWord SInteger) -> Eval (WordValue SBool SWord SInteger) -> Eval (WordValue SBool SWord SInteger)

# Documentation

type SBool = SVal Source #

type SWord = SVal Source #

type SInteger = SVal Source #

literalSWord :: Int -> Integer -> SWord Source #

fromBitsLE :: [SBool] -> SWord Source #

forallBV_ :: Int -> Symbolic SWord Source #

existsBV_ :: Int -> Symbolic SWord Source #

forallSBool_ :: Symbolic SBool Source #

existsSBool_ :: Symbolic SBool Source #

forallSInteger_ :: Symbolic SBool Source #

existsSInteger_ :: Symbolic SBool Source #

type Value = GenValue SBool SWord SInteger Source #

data TValue Source #

An evaluated type of kind *. These types do not contain type variables, type synonyms, or type functions.

#### Instances

Instances details

Show TValue Source # |
Instance details Defined in Cryptol.Eval.Type Methods showsPrec :: Int -> TValue -> ShowS Source # show :: TValue -> String Source # showList :: [TValue] -> ShowS Source #
Generic TValue Source # |
Instance details Defined in Cryptol.Eval.Type Associated Types type Rep TValue :: Type -> Type Source # Methods from :: TValue -> Rep TValue x Source # to :: Rep TValue x -> TValue Source #
NFData TValue Source # |
Instance details Defined in Cryptol.Eval.Type Methods rnf :: TValue -> () Source #
type Rep TValue Source # |

Instance details

Defined in Cryptol.Eval.Type

type Rep TValue = D1 ('MetaData "TValue" "Cryptol.Eval.Type" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" 'False) (((C1 ('MetaCons "TVBit" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TVInteger" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TVIntMod" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)) :+: C1 ('MetaCons "TVSeq" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TValue)))) :+: ((C1 ('MetaCons "TVStream" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TValue)) :+: C1 ('MetaCons "TVTuple" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TValue]))) :+: (C1 ('MetaCons "TVRec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Ident, TValue)])) :+: (C1 ('MetaCons "TVFun" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TValue) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TValue)) :+: C1 ('MetaCons "TVAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UserTC) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Either Nat' TValue]))))))

isTBit :: TValue -> Bool Source #

True if the evaluated value is `Bit`

tvSeq :: Nat' -> TValue -> TValue Source #

Produce a sequence type value

data GenValue b w i Source #

Generic value type, parameterized by bit and word types.

NOTE: we maintain an important invariant regarding sequence types. `VSeq` must never be used for finite sequences of bits. Always use the `VWord` constructor instead! Infinite sequences of bits are handled by the `VStream` constructor, just as for other types.

Constructors

VRecord ![(Ident, Eval (GenValue b w i))]

     { .. }

VTuple ![Eval (GenValue b w i)]

     ( .. )

VBit !b

     Bit

VInteger !i | `Integer` or `Z n`
VSeq !Integer !(SeqMap b w i) | `[n]a` Invariant: VSeq is never a sequence of bits

VWord !Integer !(Eval (WordValue b w i))

     [n]Bit

VStream !(SeqMap b w i)

     [inf]a

VFun (Eval (GenValue b w i) -> Eval (GenValue b w i)) | functions
VPoly (TValue -> Eval (GenValue b w i)) | polymorphic values (kind *)
VNumPoly (Nat' -> Eval (GenValue b w i)) | polymorphic values (kind #)

#### Instances

Instances details

(Show b, Show w, Show i) => Show (GenValue b w i) Source # |
Instance details Defined in Cryptol.Eval.Value Methods showsPrec :: Int -> GenValue b w i -> ShowS Source # show :: GenValue b w i -> String Source # showList :: [GenValue b w i] -> ShowS Source #
Generic (GenValue b w i) Source # |
Instance details Defined in Cryptol.Eval.Value Associated Types type Rep (GenValue b w i) :: Type -> Type Source # Methods from :: GenValue b w i -> Rep (GenValue b w i) x Source # to :: Rep (GenValue b w i) x -> GenValue b w i Source #
(NFData b, NFData i, NFData w) => NFData (GenValue b w i) Source # |
Instance details Defined in Cryptol.Eval.Value Methods rnf :: GenValue b w i -> () Source #
type Rep (GenValue b w i) Source # |

Instance details

Defined in Cryptol.Eval.Value

type Rep (GenValue b w i) = D1 ('MetaData "GenValue" "Cryptol.Eval.Value" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" 'False) (((C1 ('MetaCons "VRecord" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(Ident, Eval (GenValue b w i))])) :+: C1 ('MetaCons "VTuple" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Eval (GenValue b w i)]))) :+: (C1 ('MetaCons "VBit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 b)) :+: (C1 ('MetaCons "VInteger" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 i)) :+: C1 ('MetaCons "VSeq" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Integer) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (SeqMap b w i)))))) :+: ((C1 ('MetaCons "VWord" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Integer) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Eval (WordValue b w i)))) :+: C1 ('MetaCons "VStream" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (SeqMap b w i)))) :+: (C1 ('MetaCons "VFun" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Eval (GenValue b w i) -> Eval (GenValue b w i)))) :+: (C1 ('MetaCons "VPoly" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TValue -> Eval (GenValue b w i)))) :+: C1 ('MetaCons "VNumPoly" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Nat' -> Eval (GenValue b w i))))))))

lam :: (Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i Source #

tlam :: (TValue -> GenValue b w i) -> GenValue b w i Source #

A type lambda that expects a `Type`.

toStream :: [GenValue b w i] -> Eval (GenValue b w i) Source #

Generate a stream.

toFinSeq :: BitWord b w i => Integer -> TValue -> [GenValue b w i] -> GenValue b w i Source #

toSeq :: BitWord b w i => Nat' -> TValue -> [GenValue b w i] -> Eval (GenValue b w i) Source #

Construct either a finite sequence, or a stream. In the finite case, record whether or not the elements were bits, to aid pretty-printing.

fromVBit :: GenValue b w i -> b Source #

Extract a bit value.

fromVFun :: GenValue b w i -> Eval (GenValue b w i) -> Eval (GenValue b w i) Source #

Extract a function from a value.

fromVPoly :: GenValue b w i -> TValue -> Eval (GenValue b w i) Source #

Extract a polymorphic function from a value.

fromVTuple :: GenValue b w i -> [Eval (GenValue b w i)] Source #

Extract a tuple from a value.

fromVRecord :: GenValue b w i -> [(Ident, Eval (GenValue b w i))] Source #

Extract a record from a value.

lookupRecord :: Ident -> GenValue b w i -> Eval (GenValue b w i) Source #

Lookup a field in a record.

fromSeq :: forall b w i. BitWord b w i => String -> GenValue b w i -> Eval (SeqMap b w i) Source #

Extract a sequence.

fromVWord :: BitWord b w i => String -> GenValue b w i -> Eval w Source #

Extract a packed word.

evalPanic :: String -> [String] -> a Source #

iteSValue :: SBool -> Value -> Value -> Eval Value Source #

mergeValue :: Bool -> SBool -> Value -> Value -> Eval Value Source #

mergeWord :: Bool -> SBool -> WordValue SBool SWord SInteger -> WordValue SBool SWord SInteger -> WordValue SBool SWord SInteger Source #

mergeBit :: Bool -> SBool -> SBool -> SBool -> SBool Source #

mergeBits :: Bool -> SBool -> Seq (Eval SBool) -> Seq (Eval SBool) -> Seq (Eval SBool) Source #

mergeSeqMap :: Bool -> SBool -> SeqMap SBool SWord SInteger -> SeqMap SBool SWord SInteger -> SeqMap SBool SWord SInteger Source #

mergeWord' :: Bool -> SBool -> Eval (WordValue SBool SWord SInteger) -> Eval (WordValue SBool SWord SInteger) -> Eval (WordValue SBool SWord SInteger) Source #

# Orphan instances

BitWord SBool SWord SInteger Source # |

Instance details

Methods

ppBit :: SBool -> Doc Source #

ppWord :: PPOpts -> SWord -> Doc Source #

ppInteger :: PPOpts -> SInteger -> Doc Source #

wordAsChar :: SWord -> Maybe Char Source #

wordLen :: SWord -> Integer Source #

bitLit :: Bool -> SBool Source #

wordLit :: Integer -> Integer -> SWord Source #

integerLit :: Integer -> SInteger Source #

wordBit :: SWord -> Integer -> SBool Source #

wordUpdate :: SWord -> Integer -> SBool -> SWord Source #

packWord :: [SBool] -> SWord Source #

unpackWord :: SWord -> [SBool] Source #

joinWord :: SWord -> SWord -> SWord Source #

splitWord :: Integer -> Integer -> SWord -> (SWord, SWord) Source #

extractWord :: Integer -> Integer -> SWord -> SWord Source #

wordPlus :: SWord -> SWord -> SWord Source #

wordMinus :: SWord -> SWord -> SWord Source #

wordMult :: SWord -> SWord -> SWord Source #

wordToInt :: SWord -> SInteger Source #

intPlus :: SInteger -> SInteger -> SInteger Source #

intMinus :: SInteger -> SInteger -> SInteger Source #

intMult :: SInteger -> SInteger -> SInteger Source #

intModPlus :: Integer -> SInteger -> SInteger -> SInteger Source #

intModMinus :: Integer -> SInteger -> SInteger -> SInteger Source #

intModMult :: Integer -> SInteger -> SInteger -> SInteger Source #

wordFromInt :: Integer -> SInteger -> SWord Source #