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

What4.SemiRing

Contents

Semiring datakinds
Semiring representations
Semiring coefficients
Semiring product occurrences

Description

The algebraic assumptions we make about our semirings are that:

addition is commutative and associative, with a unit called zero,
multiplication is commutative and associative, with a unit called one,
one and zero are distinct values,
multiplication distributes through addition, and
multiplication by zero gives zero.

Note that we do not assume the existence of additive inverses (hence, semirings), but we do assume commutativity of multiplication.

Note, moreover, that bitvectors can be equipped with two different semirings (the usual arithmetic one and the XOR/AND boolean ring imposed by the boolean algebra structure), which occasionally requires some care.

In addition, some semirings are "ordered" semirings. These are equipped with a total ordering relation such that addition is both order-preserving and order-reflecting; that is, x <= y iff x + z <= y + z. Moreover ordered semirings satisfy: 0 <= x and 0 <= y implies 0 <= x*y.

Synopsis

data SemiRing
type SemiRingInteger = 'SemiRingInteger
type SemiRingReal = 'SemiRingReal
type SemiRingBV = 'SemiRingBV
data BVFlavor
type BVBits = 'BVBits
type BVArith = 'BVArith
data SemiRingRepr (sr :: SemiRing) where
- SemiRingIntegerRepr :: SemiRingRepr SemiRingInteger
- SemiRingRealRepr :: SemiRingRepr SemiRingReal
- SemiRingBVRepr :: 1 <= w => !(BVFlavorRepr fv) -> !(NatRepr w) -> SemiRingRepr (SemiRingBV fv w)
data OrderedSemiRingRepr (sr :: SemiRing) where
- OrderedSemiRingIntegerRepr :: OrderedSemiRingRepr SemiRingInteger
- OrderedSemiRingRealRepr :: OrderedSemiRingRepr SemiRingReal
data BVFlavorRepr (fv :: BVFlavor) where
- BVArithRepr :: BVFlavorRepr BVArith
- BVBitsRepr :: BVFlavorRepr BVBits
type family SemiRingBase (sr :: SemiRing) :: BaseType where ...
semiRingBase :: SemiRingRepr sr -> BaseTypeRepr (SemiRingBase sr)
orderedSemiRing :: OrderedSemiRingRepr sr -> SemiRingRepr sr
type family Coefficient (sr :: SemiRing) :: Type where ...
zero :: SemiRingRepr sr -> Coefficient sr
one :: SemiRingRepr sr -> Coefficient sr
add :: SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Coefficient sr
mul :: SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Coefficient sr
eq :: SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Bool
le :: OrderedSemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Bool
lt :: OrderedSemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Bool
sr_compare :: SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Ordering
sr_hashWithSalt :: SemiRingRepr sr -> Int -> Coefficient sr -> Int
type family Occurrence (sr :: SemiRing) :: Type where ...
occ_add :: SemiRingRepr sr -> Occurrence sr -> Occurrence sr -> Occurrence sr
occ_one :: SemiRingRepr sr -> Occurrence sr
occ_eq :: SemiRingRepr sr -> Occurrence sr -> Occurrence sr -> Bool
occ_hashWithSalt :: SemiRingRepr sr -> Int -> Occurrence sr -> Int
occ_compare :: SemiRingRepr sr -> Occurrence sr -> Occurrence sr -> Ordering
occ_count :: SemiRingRepr sr -> Occurrence sr -> Natural

Semiring datakinds

data SemiRing Source #

Data-kind representing the semirings What4 supports.

Instances

Instances details

TestEquality OrderedSemiRingRepr Source #
Instance details Defined in What4.SemiRing Methods testEquality :: forall (a :: k) (b :: k). OrderedSemiRingRepr a -> OrderedSemiRingRepr b -> Maybe (a :~: b) #
TestEquality SemiRingRepr Source #
Instance details Defined in What4.SemiRing Methods testEquality :: forall (a :: k) (b :: k). SemiRingRepr a -> SemiRingRepr b -> Maybe (a :~: b) #
OrdF OrderedSemiRingRepr Source #
Instance details Defined in What4.SemiRing Methods compareF :: forall (x :: k) (y :: k). OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> Bool # ltF :: forall (x :: k) (y :: k). OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> Bool # geqF :: forall (x :: k) (y :: k). OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> Bool # gtF :: forall (x :: k) (y :: k). OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> Bool #
OrdF SemiRingRepr Source #
Instance details Defined in What4.SemiRing Methods compareF :: forall (x :: k) (y :: k). SemiRingRepr x -> SemiRingRepr y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). SemiRingRepr x -> SemiRingRepr y -> Bool # ltF :: forall (x :: k) (y :: k). SemiRingRepr x -> SemiRingRepr y -> Bool # geqF :: forall (x :: k) (y :: k). SemiRingRepr x -> SemiRingRepr y -> Bool # gtF :: forall (x :: k) (y :: k). SemiRingRepr x -> SemiRingRepr y -> Bool #
HashableF OrderedSemiRingRepr Source #
Instance details Defined in What4.SemiRing Methods hashWithSaltF :: forall (tp :: k). Int -> OrderedSemiRingRepr tp -> Int # hashF :: forall (tp :: k). OrderedSemiRingRepr tp -> Int #
HashableF SemiRingRepr Source #
Instance details Defined in What4.SemiRing Methods hashWithSaltF :: forall (tp :: k). Int -> SemiRingRepr tp -> Int # hashF :: forall (tp :: k). SemiRingRepr tp -> Int #
OrdF f => TestEquality (SemiRingProduct f :: SemiRing -> Type) Source #
Instance details Defined in What4.Expr.WeightedSum Methods testEquality :: forall (a :: k) (b :: k). SemiRingProduct f a -> SemiRingProduct f b -> Maybe (a :~: b) #
OrdF f => TestEquality (WeightedSum f :: SemiRing -> Type) Source #
Instance details Defined in What4.Expr.WeightedSum Methods testEquality :: forall (a :: k) (b :: k). WeightedSum f a -> WeightedSum f b -> Maybe (a :~: b) #

type SemiRingInteger Source #

Arguments

= 'SemiRingInteger

:: SemiRing

type SemiRingReal Source #

Arguments

= 'SemiRingReal

:: SemiRing

type SemiRingBV Source #

Arguments

= 'SemiRingBV

:: BVFlavor -> Nat -> SemiRing

data BVFlavor Source #

Data-kind indicating the two flavors of bitvector semirings. The ordinary arithmetic semiring consists of addition and multiplication, and the "bits" semiring consists of bitwise xor and bitwise and.

Instances

Instances details

TestEquality BVFlavorRepr Source #
Instance details Defined in What4.SemiRing Methods testEquality :: forall (a :: k) (b :: k). BVFlavorRepr a -> BVFlavorRepr b -> Maybe (a :~: b) #
OrdF BVFlavorRepr Source #
Instance details Defined in What4.SemiRing Methods compareF :: forall (x :: k) (y :: k). BVFlavorRepr x -> BVFlavorRepr y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). BVFlavorRepr x -> BVFlavorRepr y -> Bool # ltF :: forall (x :: k) (y :: k). BVFlavorRepr x -> BVFlavorRepr y -> Bool # geqF :: forall (x :: k) (y :: k). BVFlavorRepr x -> BVFlavorRepr y -> Bool # gtF :: forall (x :: k) (y :: k). BVFlavorRepr x -> BVFlavorRepr y -> Bool #
HashableF BVFlavorRepr Source #
Instance details Defined in What4.SemiRing Methods hashWithSaltF :: forall (tp :: k). Int -> BVFlavorRepr tp -> Int # hashF :: forall (tp :: k). BVFlavorRepr tp -> Int #

type BVBits Source #

Arguments

= 'BVBits

:: BVFlavor

type BVArith Source #

Arguments

= 'BVArith

:: BVFlavor

Semiring representations

data SemiRingRepr (sr :: SemiRing) where Source #

Constructors

SemiRingIntegerRepr :: SemiRingRepr SemiRingInteger
SemiRingRealRepr :: SemiRingRepr SemiRingReal
SemiRingBVRepr :: 1 <= w => !(BVFlavorRepr fv) -> !(NatRepr w) -> SemiRingRepr (SemiRingBV fv w)

Instances

Instances details

TestEquality SemiRingRepr Source #
Instance details Defined in What4.SemiRing Methods testEquality :: forall (a :: k) (b :: k). SemiRingRepr a -> SemiRingRepr b -> Maybe (a :~: b) #
OrdF SemiRingRepr Source #
Instance details Defined in What4.SemiRing Methods compareF :: forall (x :: k) (y :: k). SemiRingRepr x -> SemiRingRepr y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). SemiRingRepr x -> SemiRingRepr y -> Bool # ltF :: forall (x :: k) (y :: k). SemiRingRepr x -> SemiRingRepr y -> Bool # geqF :: forall (x :: k) (y :: k). SemiRingRepr x -> SemiRingRepr y -> Bool # gtF :: forall (x :: k) (y :: k). SemiRingRepr x -> SemiRingRepr y -> Bool #
HashableF SemiRingRepr Source #
Instance details Defined in What4.SemiRing Methods hashWithSaltF :: forall (tp :: k). Int -> SemiRingRepr tp -> Int # hashF :: forall (tp :: k). SemiRingRepr tp -> Int #
Hashable (SemiRingRepr sr) Source #
Instance details Defined in What4.SemiRing Methods hashWithSalt :: Int -> SemiRingRepr sr -> Int # hash :: SemiRingRepr sr -> Int #

data OrderedSemiRingRepr (sr :: SemiRing) where Source #

The subset of semirings that are equipped with an appropriate (order-respecting) total order.

Constructors

OrderedSemiRingIntegerRepr :: OrderedSemiRingRepr SemiRingInteger
OrderedSemiRingRealRepr :: OrderedSemiRingRepr SemiRingReal

Instances

Instances details

TestEquality OrderedSemiRingRepr Source #
Instance details Defined in What4.SemiRing Methods testEquality :: forall (a :: k) (b :: k). OrderedSemiRingRepr a -> OrderedSemiRingRepr b -> Maybe (a :~: b) #
OrdF OrderedSemiRingRepr Source #
Instance details Defined in What4.SemiRing Methods compareF :: forall (x :: k) (y :: k). OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> Bool # ltF :: forall (x :: k) (y :: k). OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> Bool # geqF :: forall (x :: k) (y :: k). OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> Bool # gtF :: forall (x :: k) (y :: k). OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> Bool #
HashableF OrderedSemiRingRepr Source #
Instance details Defined in What4.SemiRing Methods hashWithSaltF :: forall (tp :: k). Int -> OrderedSemiRingRepr tp -> Int # hashF :: forall (tp :: k). OrderedSemiRingRepr tp -> Int #
Hashable (OrderedSemiRingRepr sr) Source #
Instance details Defined in What4.SemiRing Methods hashWithSalt :: Int -> OrderedSemiRingRepr sr -> Int # hash :: OrderedSemiRingRepr sr -> Int #

data BVFlavorRepr (fv :: BVFlavor) where Source #

Constructors

BVArithRepr :: BVFlavorRepr BVArith
BVBitsRepr :: BVFlavorRepr BVBits

Instances

Instances details

TestEquality BVFlavorRepr Source #
Instance details Defined in What4.SemiRing Methods testEquality :: forall (a :: k) (b :: k). BVFlavorRepr a -> BVFlavorRepr b -> Maybe (a :~: b) #
OrdF BVFlavorRepr Source #
Instance details Defined in What4.SemiRing Methods compareF :: forall (x :: k) (y :: k). BVFlavorRepr x -> BVFlavorRepr y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). BVFlavorRepr x -> BVFlavorRepr y -> Bool # ltF :: forall (x :: k) (y :: k). BVFlavorRepr x -> BVFlavorRepr y -> Bool # geqF :: forall (x :: k) (y :: k). BVFlavorRepr x -> BVFlavorRepr y -> Bool # gtF :: forall (x :: k) (y :: k). BVFlavorRepr x -> BVFlavorRepr y -> Bool #
HashableF BVFlavorRepr Source #
Instance details Defined in What4.SemiRing Methods hashWithSaltF :: forall (tp :: k). Int -> BVFlavorRepr tp -> Int # hashF :: forall (tp :: k). BVFlavorRepr tp -> Int #
Hashable (BVFlavorRepr fv) Source #
Instance details Defined in What4.SemiRing Methods hashWithSalt :: Int -> BVFlavorRepr fv -> Int # hash :: BVFlavorRepr fv -> Int #

type family SemiRingBase (sr :: SemiRing) :: BaseType where ... Source #

Equations

SemiRingBase SemiRingInteger = BaseIntegerType
SemiRingBase SemiRingReal = BaseRealType
SemiRingBase (SemiRingBV fv w) = BaseBVType w

semiRingBase :: SemiRingRepr sr -> BaseTypeRepr (SemiRingBase sr) Source #

Compute the base type of the given semiring.

orderedSemiRing :: OrderedSemiRingRepr sr -> SemiRingRepr sr Source #

Compute the semiring corresponding to the given ordered semiring.

Semiring coefficients

type family Coefficient (sr :: SemiRing) :: Type where ... Source #

The constant values in the semiring.

Equations

Coefficient SemiRingInteger = Integer
Coefficient SemiRingReal = Rational
Coefficient (SemiRingBV fv w) = BV w

zero :: SemiRingRepr sr -> Coefficient sr Source #

one :: SemiRingRepr sr -> Coefficient sr Source #

add :: SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Coefficient sr Source #

mul :: SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Coefficient sr Source #

eq :: SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Bool Source #

le :: OrderedSemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Bool Source #

lt :: OrderedSemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Bool Source #

sr_compare :: SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Ordering Source #

sr_hashWithSalt :: SemiRingRepr sr -> Int -> Coefficient sr -> Int Source #

Semiring product occurrences

type family Occurrence (sr :: SemiRing) :: Type where ... Source #

The Occurrence family counts how many times a term occurs in a product. For most semirings, this is just a natural number representing the exponent. For the boolean ring of bitvectors, however, it is unit because the lattice operations are idempotent.

Equations

Occurrence SemiRingInteger = Natural
Occurrence SemiRingReal = Natural
Occurrence (SemiRingBV BVArith w) = Natural
Occurrence (SemiRingBV BVBits w) = ()

occ_add :: SemiRingRepr sr -> Occurrence sr -> Occurrence sr -> Occurrence sr Source #

occ_one :: SemiRingRepr sr -> Occurrence sr Source #

occ_eq :: SemiRingRepr sr -> Occurrence sr -> Occurrence sr -> Bool Source #

occ_hashWithSalt :: SemiRingRepr sr -> Int -> Occurrence sr -> Int Source #

occ_compare :: SemiRingRepr sr -> Occurrence sr -> Occurrence sr -> Ordering Source #

occ_count :: SemiRingRepr sr -> Occurrence sr -> Natural Source #