sbv-5.7: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright(c) Brian Huffman
Safe HaskellNone



Demonstrates how new sizes of word/int types can be defined and used with SBV.



newtype Word4 Source

Word4 as a newtype. Invariant: Word4 x should satisfy x < 16.


Word4 Word8 


Bounded Word4 Source

Bounded instance; from 0 to 255

Enum Word4 Source

Enum instance, trivial definitions.

Eq Word4 Source 
Integral Word4 Source

Integral instance, again using Word8 instance and casting. NB. we do not need to use the smart constructor here as neither the quotient nor the remainder can overflow a Word4.

Data Word4 Source 
Num Word4 Source

Num instance, merely lifts underlying 8-bit operation and casts back

Ord Word4 Source 
Read Word4 Source

Read instance. We read as an 8-bit word, and coerce

Real Word4 Source

Real instance simply uses the Word8 instance

Show Word4 Source

Show instance

Bits Word4 Source

Bits instance

Random Word4 Source

Random instance, used in quick-check

HasKind Word4 Source

HasKind instance; simply returning the underlying kind for the type

SymWord Word4 Source

SymWord instance, allowing this type to be used in proofs/sat etc.

SatModel Word4 Source

SatModel instance, merely uses the generic parsing method.

SDivisible SWord4 Source

SDvisible instance, using default methods

SDivisible Word4 Source

SDvisible instance, using 0-extension

SIntegral Word4 Source

SIntegral instance, using default methods

FromBits SWord4 Source

Conversion from bits

Splittable Word8 Word4 Source

Joiningsplitting tofrom Word8

word4 :: Word8 -> Word4 Source

Smart constructor; simplifies conversion from Word8

type SWord4 = SBV Word4 Source

SWord4 type synonym