what4-1.6.3: Solver-agnostic symbolic values support for issuing queries

Copyright | (c) Galois Inc 2019-2020
License | BSD3
Maintainer | huffman@galois.com
Safe Haskell | None
Language | Haskell2010

What4.Utils.BVDomain

Contents

- Bitvector abstract domains
  - Domain transfer functions
  - Projection functions
- Operations
  - Shifts and rotates
  - Arithmetic
  - Bitwise
  - Misc
- Useful bitvector computations
- Correctness properties

Description

Provides an implementation of abstract domains for bitvectors. This abstract domain has essentially two modes: arithmetic and bitvector modes. The arithmetic mode is a fairly straightforward interval domain, albeit one that is carefully implemented to deal properly with intervals that "cross zero", as is relatively common when using 2's complement signed representations. The bitwise mode tracks the values of individual bits independently in a 3-valued logic (true, false or unknown). The abstract domain transitions between the two modes when necessary, but attempts to retain as much precision as possible.

The operations of these domains are formalized in the companion Cryptol files found together in this package under the "doc" directory, and their soundness properties stated and established.

Synopsis

- data BVDomain (w :: Nat)
  - = BVDArith !(Domain w)
  - | BVDBitwise !(Domain w)
- proper :: forall (w :: Nat). NatRepr w -> BVDomain w -> Bool
- member :: forall (w :: Nat). BVDomain w -> Integer -> Bool
- size :: forall (w :: Nat). BVDomain w -> Integer
- asArithDomain :: forall (w :: Nat). BVDomain w -> Domain w
- asBitwiseDomain :: forall (w :: Nat). BVDomain w -> Domain w
- asXorDomain :: forall (w :: Nat). BVDomain w -> Domain w
- fromXorDomain :: forall (w :: Nat). Domain w -> BVDomain w
- arithToXorDomain :: forall (w :: Nat). Domain w -> Domain w
- bitwiseToXorDomain :: forall (w :: Nat). Domain w -> Domain w
- xorToBitwiseDomain :: forall (w :: Nat). Domain w -> Domain w
- asSingleton :: forall (w :: Nat). BVDomain w -> Maybe Integer
- eq :: forall (w :: Nat). BVDomain w -> BVDomain w -> Maybe Bool
- slt :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> Maybe Bool
- ult :: forall (w :: Natural). 1 <= w => BVDomain w -> BVDomain w -> Maybe Bool
- testBit :: forall (w :: Nat). NatRepr w -> BVDomain w -> Natural -> Maybe Bool
- domainsOverlap :: forall (w :: Nat). BVDomain w -> BVDomain w -> Bool
- ubounds :: forall (w :: Nat). BVDomain w -> (Integer, Integer)
- sbounds :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w -> (Integer, Integer)
- isUltSumCommonEquiv :: forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w -> Bool
- arithDomainData :: forall (w :: Nat). Domain w -> Maybe (Integer, Integer)
- bitbounds :: forall (w :: Nat). Domain w -> (Integer, Integer)
- any :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w
- singleton :: forall (w :: Natural). (HasCallStack, 1 <= w) => NatRepr w -> Integer -> BVDomain w
- range :: forall (w :: Nat). NatRepr w -> Integer -> Integer -> BVDomain w
- fromAscEltList :: forall (w :: Natural). 1 <= w => NatRepr w -> [Integer] -> BVDomain w
- union :: forall (w :: Natural). 1 <= w => BVDomain w -> BVDomain w -> BVDomain w
- concat :: forall (u :: Nat) (v :: Nat). NatRepr u -> BVDomain u -> NatRepr v -> BVDomain v -> BVDomain (u + v)
- select :: forall (n :: Natural) (i :: Natural) (w :: Natural). (1 <= n, (i + n) <= w) => NatRepr i -> NatRepr n -> BVDomain w -> BVDomain n
- zext :: forall (w :: Natural) (u :: Natural). (1 <= w, (w + 1) <= u) => BVDomain w -> NatRepr u -> BVDomain u
- sext :: forall (w :: Natural) (u :: Natural). (1 <= w, (w + 1) <= u) => NatRepr w -> BVDomain w -> NatRepr u -> BVDomain u
- shl :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
- lshr :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
- ashr :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
- rol :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
- ror :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
- add :: forall (w :: Natural). 1 <= w => BVDomain w -> BVDomain w -> BVDomain w
- negate :: forall (w :: Natural). 1 <= w => BVDomain w -> BVDomain w
- scale :: forall (w :: Natural). 1 <= w => Integer -> BVDomain w -> BVDomain w
- mul :: forall (w :: Natural). 1 <= w => BVDomain w -> BVDomain w -> BVDomain w
- udiv :: forall (w :: Natural). 1 <= w => BVDomain w -> BVDomain w -> BVDomain w
- urem :: forall (w :: Natural). 1 <= w => BVDomain w -> BVDomain w -> BVDomain w
- sdiv :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
- srem :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
- not :: forall (w :: Nat). BVDomain w -> BVDomain w
- and :: forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w
- or :: forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w
- xor :: forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w
- popcnt :: forall (w :: Nat). NatRepr w -> BVDomain w -> BVDomain w
- clz :: forall (w :: Nat). NatRepr w -> BVDomain w -> BVDomain w
- ctz :: forall (w :: Nat). NatRepr w -> BVDomain w -> BVDomain w
- bitwiseRoundAbove :: Integer -> Integer -> Integer -> Integer
- bitwiseRoundBetween :: Integer -> Integer -> Integer -> Integer -> Integer
- genDomain :: forall (w :: Nat). NatRepr w -> Gen (BVDomain w)
- genElement :: forall (w :: Nat). BVDomain w -> Gen Integer
- genPair :: forall (w :: Nat). NatRepr w -> Gen (BVDomain w, Integer)
- correct_arithToBitwise :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property
- correct_bitwiseToArith :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property
- correct_bitwiseToXorDomain :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property
- correct_arithToXorDomain :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property
- correct_xorToBitwiseDomain :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property
- correct_asXorDomain :: forall (n :: Nat). NatRepr n -> (BVDomain n, Integer) -> Property
- correct_fromXorDomain :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property
- correct_bra1 :: forall (n :: Nat). NatRepr n -> Integer -> Integer -> Property
- correct_bra2 :: forall (n :: Nat). NatRepr n -> Integer -> Integer -> Integer -> Property
- correct_brb1 :: forall (n :: Nat). NatRepr n -> Integer -> Integer -> Integer -> Property
- correct_brb2 :: forall (n :: Nat). NatRepr n -> Integer -> Integer -> Integer -> Integer -> Property
- correct_any :: forall (n :: Natural). 1 <= n => NatRepr n -> Integer -> Property
- correct_ubounds :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Property
- correct_sbounds :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Property
- correct_singleton :: forall (n :: Natural). 1 <= n => NatRepr n -> Integer -> Integer -> Property
- correct_overlap :: forall (n :: Nat). BVDomain n -> BVDomain n -> Integer -> Property
- precise_overlap :: forall (n :: Nat). BVDomain n -> BVDomain n -> Property
- correct_union :: forall (n :: Natural). 1 <= n => NatRepr n -> BVDomain n -> BVDomain n -> Integer -> Property
- correct_zero_ext :: forall (w :: Natural) (u :: Natural). (1 <= w, (w + 1) <= u) => NatRepr w -> BVDomain w -> NatRepr u -> Integer -> Property
- correct_sign_ext :: forall (w :: Natural) (u :: Natural). (1 <= w, (w + 1) <= u) => NatRepr w -> BVDomain w -> NatRepr u -> Integer -> Property
- correct_concat :: forall (m :: Nat) (n :: Nat). NatRepr m -> (BVDomain m, Integer) -> NatRepr n -> (BVDomain n, Integer) -> Property
- correct_select :: forall (n :: Natural) (i :: Natural) (w :: Natural). (1 <= n, (i + n) <= w) => NatRepr i -> NatRepr n -> (BVDomain w, Integer) -> Property
- correct_add :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
- correct_neg :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Property
- correct_mul :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
- correct_scale :: forall (n :: Natural). 1 <= n => NatRepr n -> Integer -> (BVDomain n, Integer) -> Property
- correct_udiv :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
- correct_urem :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
- correct_sdiv :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
- correct_srem :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
- correct_shl :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
- correct_lshr :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
- correct_ashr :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
- correct_rol :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
- correct_ror :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
- correct_eq :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
- correct_ult :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
- correct_slt :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
- correct_and :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
- correct_or :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
- correct_not :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Property
- correct_xor :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property
- correct_testBit :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Natural -> Property
- correct_popcnt :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Property
- correct_clz :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Property
- correct_ctz :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Property

# Bitvector abstract domains

data BVDomain (w :: Nat) Source #

A value of type ``BVDomain` w` represents a set of bitvectors of width `w`. A BVDomain represents either an arithmetic interval, or a bitwise interval.

Constructors

BVDArith !(Domain w) |
BVDBitwise !(Domain w) |

#### Instances

Instances details

Show (BVDomain w) Source # |
Instance details Defined in What4.Utils.BVDomain Methods showsPrec :: Int -> BVDomain w -> ShowS Source # show :: BVDomain w -> String Source # showList :: [BVDomain w] -> ShowS Source #

proper :: forall (w :: Nat). NatRepr w -> BVDomain w -> Bool Source #

Test if the domain satisfies its invariants

member :: forall (w :: Nat). BVDomain w -> Integer -> Bool Source #

Test if the given integer value is a member of the abstract domain

size :: forall (w :: Nat). BVDomain w -> Integer Source #

Compute how many concrete elements are in the abstract domain

## Domain transfer functions

asArithDomain :: forall (w :: Nat). BVDomain w -> Domain w Source #

asBitwiseDomain :: forall (w :: Nat). BVDomain w -> Domain w Source #

asXorDomain :: forall (w :: Nat). BVDomain w -> Domain w Source #

fromXorDomain :: forall (w :: Nat). Domain w -> BVDomain w Source #

arithToXorDomain :: forall (w :: Nat). Domain w -> Domain w Source #

bitwiseToXorDomain :: forall (w :: Nat). Domain w -> Domain w Source #

xorToBitwiseDomain :: forall (w :: Nat). Domain w -> Domain w Source #

## Projection functions

asSingleton :: forall (w :: Nat). BVDomain w -> Maybe Integer Source #

Return value if this is a singleton.

eq :: forall (w :: Nat). BVDomain w -> BVDomain w -> Maybe Bool Source #

slt :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> Maybe Bool Source #

Check if all elements in one domain are less than all elements in other.

ult :: forall (w :: Natural). 1 <= w => BVDomain w -> BVDomain w -> Maybe Bool Source #

Check if all elements in one domain are less than all elements in other.

testBit Source #

Arguments

:: forall (w :: Nat). NatRepr w |
-> BVDomain w |
-> Natural | Index of bit (least-significant bit has index 0)
-> Maybe Bool |

Return `Just` if every bitvector in the domain has the same bit at the given index.

domainsOverlap :: forall (w :: Nat). BVDomain w -> BVDomain w -> Bool Source #

Return true if domains contain a common element.

ubounds :: forall (w :: Nat). BVDomain w -> (Integer, Integer) Source #

sbounds :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w -> (Integer, Integer) Source #

isUltSumCommonEquiv :: forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w -> Bool Source #

Check if (bvult (bvadd a c) (bvadd b c)) is equivalent to (bvult a b)

arithDomainData :: forall (w :: Nat). Domain w -> Maybe (Integer, Integer) Source #

Return the `(lo,sz)`, the low bound and size of the given arithmetic interval. A value `x` is in the set defined by this domain iff `(x - lo) `mod` w <= sz` holds. Returns `Nothing` if the domain contains all values.

bitbounds :: forall (w :: Nat). Domain w -> (Integer, Integer) Source #

Bitwise lower and upper bounds

# Operations

any :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w Source #

Represents all values

singleton :: forall (w :: Natural). (HasCallStack, 1 <= w) => NatRepr w -> Integer -> BVDomain w Source #

Create a bitvector domain representing the integer.

range :: forall (w :: Nat). NatRepr w -> Integer -> Integer -> BVDomain w Source #

`range w l u` returns domain containing all bitvectors formed from the `w` low order bits of some `i` in `[l,u]`. Note that per `testBit`, the least significant bit has index `0`.

fromAscEltList :: forall (w :: Natural). 1 <= w => NatRepr w -> [Integer] -> BVDomain w Source #

Create an abstract domain from an ascending list of elements. The elements are assumed to be distinct.

union :: forall (w :: Natural). 1 <= w => BVDomain w -> BVDomain w -> BVDomain w Source #

Return union of two domains.

concat :: forall (u :: Nat) (v :: Nat). NatRepr u -> BVDomain u -> NatRepr v -> BVDomain v -> BVDomain (u + v) Source #

`concat a y` returns domain where each element in `a` has been concatenated with an element in `y`. The most-significant bits are `a`, and the least significant bits are `y`.

select :: forall (n :: Natural) (i :: Natural) (w :: Natural). (1 <= n, (i + n) <= w) => NatRepr i -> NatRepr n -> BVDomain w -> BVDomain n Source #

`select i n a` selects `n` bits starting from index `i` from `a`.

zext :: forall (w :: Natural) (u :: Natural). (1 <= w, (w + 1) <= u) => BVDomain w -> NatRepr u -> BVDomain u Source #

sext :: forall (w :: Natural) (u :: Natural). (1 <= w, (w + 1) <= u) => NatRepr w -> BVDomain w -> NatRepr u -> BVDomain u Source #

## Shifts and rotates

shl :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w Source #

lshr :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w Source #

ashr :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w Source #

rol :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w Source #

ror :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w Source #

## Arithmetic

add :: forall (w :: Natural). 1 <= w => BVDomain w -> BVDomain w -> BVDomain w Source #

negate :: forall (w :: Natural). 1 <= w => BVDomain w -> BVDomain w Source #

scale :: forall (w :: Natural). 1 <= w => Integer -> BVDomain w -> BVDomain w Source #

mul :: forall (w :: Natural). 1 <= w => BVDomain w -> BVDomain w -> BVDomain w Source #

udiv :: forall (w :: Natural). 1 <= w => BVDomain w -> BVDomain w -> BVDomain w Source #

urem :: forall (w :: Natural). 1 <= w => BVDomain w -> BVDomain w -> BVDomain w Source #

sdiv :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w Source #

srem :: forall (w :: Natural). 1 <= w => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w Source #

## Bitwise

not :: forall (w :: Nat). BVDomain w -> BVDomain w Source #

Complement bits in range.

and :: forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w Source #

or :: forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w Source #

xor :: forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w Source #

## Misc

popcnt :: forall (w :: Nat). NatRepr w -> BVDomain w -> BVDomain w Source #

clz :: forall (w :: Nat). NatRepr w -> BVDomain w -> BVDomain w Source #

ctz :: forall (w :: Nat). NatRepr w -> BVDomain w -> BVDomain w Source #

# Useful bitvector computations

bitwiseRoundAbove Source #

Arguments

:: Integer | `bvmask`, based on the width of the bitvectors in question

-> Integer

    x

-> Integer

    lomask

-> Integer |

Precondition: `x <= lomask`. Find the (arithmetically) smallest `z` above `x` which is bitwise above `lomask`. In other words find the smallest `z` such that `x <= z` and `lomask .|. z == z`.

bitwiseRoundBetween Source #

Arguments

:: Integer | `bvmask`, based on the width of the bitvectors in question

-> Integer

    x

-> Integer

    lomask

-> Integer

    himask

-> Integer |

Precondition: `lomask <= x <= himask` and `lomask .|. himask == himask`. Find the (arithmetically) smallest `z` above `x` which is bitwise between `lomask` and `himask`. In other words, find the smallest `z` such that `x <= z` and `lomask .|. z = z` and `z .|. himask == himask`.

# Correctness properties

genDomain :: forall (w :: Nat). NatRepr w -> Gen (BVDomain w) Source #

Generate a random nonempty domain

genElement :: forall (w :: Nat). BVDomain w -> Gen Integer Source #

Generate a random element from a domain, which is assumed to be nonempty

genPair :: forall (w :: Nat). NatRepr w -> Gen (BVDomain w, Integer) Source #

Generate a random nonempty domain and an element contained in that domain.

correct_arithToBitwise :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property Source #

correct_bitwiseToArith :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property Source #

correct_bitwiseToXorDomain :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property Source #

correct_arithToXorDomain :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property Source #

correct_xorToBitwiseDomain :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property Source #

correct_asXorDomain :: forall (n :: Nat). NatRepr n -> (BVDomain n, Integer) -> Property Source #

correct_fromXorDomain :: forall (n :: Nat). NatRepr n -> (Domain n, Integer) -> Property Source #

correct_bra1 :: forall (n :: Nat). NatRepr n -> Integer -> Integer -> Property Source #

correct_bra2 :: forall (n :: Nat). NatRepr n -> Integer -> Integer -> Integer -> Property Source #

correct_brb1 :: forall (n :: Nat). NatRepr n -> Integer -> Integer -> Integer -> Property Source #

correct_brb2 :: forall (n :: Nat). NatRepr n -> Integer -> Integer -> Integer -> Integer -> Property Source #

correct_any :: forall (n :: Natural). 1 <= n => NatRepr n -> Integer -> Property Source #

correct_ubounds :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Property Source #

correct_sbounds :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Property Source #

correct_singleton :: forall (n :: Natural). 1 <= n => NatRepr n -> Integer -> Integer -> Property Source #

correct_overlap :: forall (n :: Nat). BVDomain n -> BVDomain n -> Integer -> Property Source #

precise_overlap :: forall (n :: Nat). BVDomain n -> BVDomain n -> Property Source #

correct_union :: forall (n :: Natural). 1 <= n => NatRepr n -> BVDomain n -> BVDomain n -> Integer -> Property Source #

correct_zero_ext :: forall (w :: Natural) (u :: Natural). (1 <= w, (w + 1) <= u) => NatRepr w -> BVDomain w -> NatRepr u -> Integer -> Property Source #

correct_sign_ext :: forall (w :: Natural) (u :: Natural). (1 <= w, (w + 1) <= u) => NatRepr w -> BVDomain w -> NatRepr u -> Integer -> Property Source #

correct_concat :: forall (m :: Nat) (n :: Nat). NatRepr m -> (BVDomain m, Integer) -> NatRepr n -> (BVDomain n, Integer) -> Property Source #

correct_select :: forall (n :: Natural) (i :: Natural) (w :: Natural). (1 <= n, (i + n) <= w) => NatRepr i -> NatRepr n -> (BVDomain w, Integer) -> Property Source #

correct_add :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_neg :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Property Source #

correct_mul :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_scale :: forall (n :: Natural). 1 <= n => NatRepr n -> Integer -> (BVDomain n, Integer) -> Property Source #

correct_udiv :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_urem :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_sdiv :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_srem :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_shl :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_lshr :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_ashr :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_rol :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_ror :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_eq :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_ult :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_slt :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_and :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_or :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_not :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Property Source #

correct_xor :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> (BVDomain n, Integer) -> Property Source #

correct_testBit :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Natural -> Property Source #

correct_popcnt :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Property Source #

correct_clz :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Property Source #

correct_ctz :: forall (n :: Natural). 1 <= n => NatRepr n -> (BVDomain n, Integer) -> Property Source #