cryptol-2.8.0: Cryptol: The Language of Cryptography

Copyright(c) 2013-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellNone
LanguageHaskell2010

Cryptol.Symbolic.Value

Contents

Description

 
Synopsis

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
Show TValue Source # 
Instance details

Defined in Cryptol.Eval.Type

Methods

showsPrec :: Int -> TValue -> ShowS #

show :: TValue -> String #

showList :: [TValue] -> ShowS #

Generic TValue Source # 
Instance details

Defined in Cryptol.Eval.Type

Associated Types

type Rep TValue :: Type -> Type #

Methods

from :: TValue -> Rep TValue x #

to :: Rep TValue x -> TValue #

NFData TValue Source # 
Instance details

Defined in Cryptol.Eval.Type

Methods

rnf :: TValue -> () #

type Rep TValue Source # 
Instance details

Defined in Cryptol.Eval.Type

type Rep TValue = D1 (MetaData "TValue" "Cryptol.Eval.Type" "cryptol-2.8.0-Jl4xQKR0B4Q8VTNDfmeSo7" 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
(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 #

show :: GenValue b w i -> String #

showList :: [GenValue b w i] -> ShowS #

Generic (GenValue b w i) Source # 
Instance details

Defined in Cryptol.Eval.Value

Associated Types

type Rep (GenValue b w i) :: Type -> Type #

Methods

from :: GenValue b w i -> Rep (GenValue b w i) x #

to :: Rep (GenValue b w i) x -> GenValue b w i #

(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 -> () #

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-Jl4xQKR0B4Q8VTNDfmeSo7" 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