/*
This file contains a Cryptol implementation of the arithmetic
bitvector abstract domain operations from module What4.Utils.Domain in what4.
In addition to the algorithms themselves, this file also contains
specifications of correctness for each of the operations. All of the
correctness properties can be formally proven (each at some specific
bit width) by loading this file in cryptol and entering ":prove".
*/
module arithdomain where
////////////////////////////////////////////////////////////
// Library
bit : {i, n} (fin n, n > i) => [n]
bit = 1 # (0 : [i])
mask : {i, n} (fin n, n >= i) => [n]
mask = 0 # (~ 0 : [i])
/** Checked unsigned addition, asserted not to overflow. */
infixl 80 .+.
(.+.) : {n} (fin n) => [n] -> [n] -> [n]
x .+. y = if carry x y then error "overflow" else x + y
/** Checked unsigned subtraction, asserted not to underflow. */
infixl 80 .-.
(.-.) : {n} (fin n) => [n] -> [n] -> [n]
x .-. y = if x < y then error "underflow" else x - y
/** Minimum of two signed values. */
smin : {a} (SignedCmp a) => a -> a -> a
smin x y = if x <$ y then x else y
/** Maximum of two signed values. */
smax : {a} (SignedCmp a) => a -> a -> a
smax x y = if x >$ y then x else y
////////////////////////////////////////////////////////////
/** A `Dom n` is either an interval `{lo, sz}` of width-`n` bitvectors
where `x` is a member iff `x - lo <= sz`, or the empty domain (when
`isBot` is set). The `isBot` flag plays the role of the separate
`BVDAny`/improper-interval sentinel in the Haskell implementation,
allowing bottom to be distinguished from top in this fixed-width
encoding. */
type Dom n = { lo : [n], sz : [n], isBot : Bit }
// Alias used to mark predicates that are intended to be checked as
// properties. The TestCoverage Haskell test uses this alias to
// identify which Cryptol functions correspond to PBT properties.
type Property = Bit
interval : {n} (fin n) => [n] -> [n] -> Dom n
interval l s = { lo = l, sz = s, isBot = False }
/** Mark a domain as bottom if the given flag is set. Used to propagate
bottom through abstract operations. */
withBot : {n} (fin n) => Bit -> Dom n -> Dom n
withBot b a = { lo = a.lo, sz = a.sz, isBot = b \/ a.isBot }
range : {n} (fin n) => [n] -> [n] -> Dom n
range lo hi = interval lo (hi - lo)
/** Membership predicate that defines the set of concrete values
represented by an abstract domain element. */
mem : {n} (fin n) => Dom n -> [n] -> Bit
mem a x = ~ a.isBot /\ x - a.lo <= a.sz
umem : {n} (fin n) => ([n], [n]) -> [n] -> Bit
umem (lo, hi) x = lo <= x /\ x <= hi
smem : {n} (fin n, n >= 1) => ([n], [n]) -> [n] -> Bit
smem (lo, hi) x = lo <=$ x /\ x <=$ hi
top : {n} (fin n) => Dom n
top = interval 0 (~ 0)
singleton : {n} (fin n) => [n] -> Dom n
singleton x = interval x 0
isSingleton : {n} (fin n) => Dom n -> Bit
isSingleton a = ~ a.isBot /\ a.sz == 0
ubounds : {n} (fin n) => Dom n -> ([n], [n])
ubounds a =
if carry a.lo a.sz then (0, ~0) else (a.lo, a.lo + a.sz)
sbounds : {n} (fin n, n >= 1) => Dom n -> ([n], [n])
sbounds a = (lo - delta, hi - delta)
where
delta = reverse 1
(lo, hi) = ubounds (interval (a.lo + delta) a.sz)
/** Nonzero signed values in a domain with the least and greatest
reciprocals. Note that this coincides with the greatest and least
nonzero values using the unsigned ordering. */
rbounds : {n} (fin n, n >= 1) => Dom n -> ([n], [n])
rbounds a =
if a.lo == 0 then (a_hi, 1) else
if a_hi == 0 then (-1, a.lo) else
if a_hi < a.lo then (-1, 1) else
(a_hi, a.lo)
where a_hi = a.lo + a.sz
overlap : {n} (fin n) => Dom n -> Dom n -> Bit
overlap a b = ~ a.isBot /\ ~ b.isBot /\ (diff <= b.sz \/ carry diff a.sz)
where diff = a.lo - b.lo
// To compute the union of two intervals, we choose representatives of
// the endpoints modulo 2^n such that their midpoints are no more than
// 2^(n-1) apart. In the code below, am and bm are equal to twice the
// midpoints of intervals a and b, respectively.
union : {n} (fin n) => Dom n -> Dom n -> Dom n
union a b =
if a.isBot /\ b.isBot then bottom
else if a.isBot then b
else if b.isBot then a
else if cw >= size then top else interval (drop`{2} cl) (drop`{2} cw)
where
size : [n+2]
size = bit`{n}
am = 2 * zext a.lo .+. zext a.sz
bm = 2 * zext b.lo .+. zext b.sz
al' = if am .+. size < bm then zext a.lo .+. size else zext a.lo
bl' = if bm .+. size < am then zext b.lo .+. size else zext b.lo
ah' = al' .+. zext a.sz
bh' = bl' .+. zext b.sz
cl = min al' bl'
ch = max ah' bh'
cw = ch .-. cl
////////////////////////////////////////////////////////////
// Lattice operations
/** Bottom element of the lattice: the empty domain. */
bottom : {n} (fin n) => Dom n
bottom = { lo = 0, sz = 0, isBot = True }
/** Lattice join (least upper bound). Synonym for `union`. */
join : {n} (fin n) => Dom n -> Dom n -> Dom n
join = union
/** Lattice meet (greatest lower bound) - intersection of two intervals. */
meet : {n} (fin n) => Dom n -> Dom n -> Dom n
meet a b =
if a.isBot \/ b.isBot then bottom
else if a.sz == ~0 then b
else if b.sz == ~0 then a
else if a == b then a
else if cl > ch then bottom
else { lo = cl, sz = ch - cl, isBot = False }
where
(al, ah) = ubounds a
(bl, bh) = ubounds b
cl = max al bl
ch = min ah bh
/** Lattice ordering: every element of `a` is also in `b`. */
leq : {n} (fin n) => Dom n -> Dom n -> Bit
leq a b =
if a.isBot then True // bottom is below everything
else if b.isBot then False // a is non-bottom, b is bottom
else if b.sz == ~0 then True // b is top: contains everything
else if a.sz == ~0 then False // a is top, b is not
else a.sz <= b.sz /\ d <= b.sz - a.sz
where d = a.lo - b.lo
////////////////////////////////////////////////////////////
zero_ext : {m, n} (fin m, m >= n) => Dom n -> Dom m
zero_ext a = withBot a.isBot (interval (zext lo) (zext (hi .-. lo)))
where (lo, hi) = ubounds a
sign_ext : {m, n} (fin m, m >= n, n >= 1) => Dom n -> Dom m
sign_ext a = withBot a.isBot (interval (sext lo) (zext (hi - lo)))
where (lo, hi) = sbounds a
concat : {m, n} (fin m, fin n) => Dom m -> Dom n -> Dom (m + n)
concat a b = withBot (a.isBot \/ b.isBot) (interval (a.lo # lo) (a.sz # sz))
where
(lo, hi) = ubounds b
sz = hi .-. lo
shrink : {m, n} (fin m, fin n) => Dom (m + n) -> Dom m
shrink a = withBot a.isBot
(if b_sz >= size then top
else interval (tail b_lo) (tail b_sz))
where
size : [1 + m]
size = bit`{m}
b_lo, b_hi, b_sz : [1 + m]
b_lo = take`{back=n} (zext a.lo)
b_hi = take`{back=n} (zext a.lo .+. zext a.sz)
b_sz = b_hi .-. b_lo
trunc : {m, n} (fin m, fin n) => Dom (m + n) -> Dom n
trunc a = withBot a.isBot
(if a.sz > mask`{n} then top
else interval (drop`{m} a.lo) (drop`{m} a.sz))
////////////////////////////////////////////////////////////
// Arithmetic operations
add : {n} (fin n) => Dom n -> Dom n -> Dom n
add a b = withBot (a.isBot \/ b.isBot)
(if carry a.sz b.sz then top
else interval (a.lo + b.lo) (a.sz .+. b.sz))
neg : {n} (fin n) => Dom n -> Dom n
neg a = withBot a.isBot (interval (- (a.lo + a.sz)) a.sz)
// Turns out, bitwise complement is easy to specify
// in this domain also
bnot : {n} (fin n) => Dom n -> Dom n
bnot a = withBot a.isBot (interval (~ ah) a.sz)
where ah = a.lo + a.sz
mul : {n} (fin n) => Dom n -> Dom n -> Dom n
mul a b = withBot (a.isBot \/ b.isBot)
(if sz >= bit`{n} then top
else interval (drop lo) (drop sz))
where
(lo, hi) = mulRange (zbounds a) (zbounds b)
sz = hi - lo
zbounds : {n} (fin n) => Dom n -> ([1 + n], [1 + n])
zbounds a = (lo', lo' + zext a.sz)
where
size : [2 + n]
size = bit`{n}
lo' = if 2 * zext a.lo .+. zext a.sz >= size then 0b1 # a.lo else 0b0 # a.lo
mulRange : {m, n} (fin m, fin n, m >= 1, n >= 1) => ([m], [m]) -> ([n], [n]) -> ([m+n], [m+n])
mulRange (xl, xh) (yl, yh) = (zl, zh)
where
(xlyl, xlyh) = scaleRange xl (yl, yh)
(xhyl, xhyh) = scaleRange xh (yl, yh)
zl = smin xlyl xhyl
zh = smax xlyh xhyh
scaleRange : {m, n} (fin m, fin n, m >= 1, n >= 1) => [m] -> ([n], [n]) -> ([m+n], [m+n])
scaleRange k (lo, hi) = if k <$ 0 then (hi', lo') else (lo', hi')
where
lo' = sext k * sext lo
hi' = sext k * sext hi
udiv : {n} (fin n, n >= 1) => Dom n -> Dom n -> Dom n
udiv a b = withBot (a.isBot \/ b.isBot) (range cl ch)
where
(al, ah) = ubounds a
(bl, bh) = ubounds b
bl' = max 1 bl // assume that division by 0 does not happen
bh' = max 1 bh // assume that division by 0 does not happen
cl = al / bh'
ch = ah / bl'
urem : {n} (fin n, n >= 1) => Dom n -> Dom n -> Dom n
urem a b = withBot (a.isBot \/ b.isBot)
(if ql == qh then range rl rh
else interval 0 (bh - 1))
where
(al, ah) = ubounds a
(bl, bh) = ubounds b
bl' = max 1 bl // assume that division by 0 does not happen
bh' = max 1 bh
(ql, rl) = (al / bh', al % bh')
(qh, rh) = (ah / bl', ah % bl')
// The first argument is an ordinary signed interval, but the second
// argument is a reciaprocal interval: The arguments should satisfy 'al
// <=$ ah' (signed) and '1/bl <= 1/bh' (signed), or equivalently, 'bh
// <= bl' (unsigned).
sdivRange : {n} (fin n, n >= 1) => ([n], [n]) -> ([n], [n]) -> ([1+n], [1+n])
sdivRange (al, ah) (bl, bh) = (ql, qh)
where
(ql1, qh1) = shrinkRange (al, ah) bh
(ql2, qh2) = shrinkRange (al, ah) bl
ql = smin ql1 ql2
qh = smax qh1 qh2
// Extra bit of output is to handle the 'INTMIN / -1' overflow case.
shrinkRange : {n} (fin n, n >= 1) => ([n], [n]) -> [n] -> ([1+n], [1+n])
shrinkRange (lo, hi) k =
if k >$ 0 then (lo ./. k, hi ./. k) else
if k <$ 0 then (hi ./. k, lo ./. k) else (sext lo, sext hi)
where
x ./. y = sext x /$ sext y
sdiv : {n} (fin n, n >= 1) => Dom n -> Dom n -> Dom n
sdiv a b = withBot (a.isBot \/ b.isBot)
(if sz >= bit`{n} then top
else interval (drop lo) (drop sz))
where
(lo, hi) = sdivRange (sbounds a) (rbounds b)
sz = hi - lo
srem : {n} (fin n, n >= 1) => Dom n -> Dom n -> Dom n
srem a b = withBot (a.isBot \/ b.isBot)
(if ql == qh then
(if ql <$ 0
then range (al - drop ql * bl) (ah - drop ql * bh)
else range (al - drop ql * bh) (ah - drop ql * bl))
else range rl rh)
where
(al, ah) = sbounds a
(bl, bh) = sbounds b
(ql, qh) = sdivRange (al, ah) (rbounds b)
rl = if al <$ 0 then smin (bl+1) (-bh+1) else 0
rh = if ah >$ 0 then smax (-bl-1) (bh-1) else 0
////////////////////////////////////////////////////////////
// Shifts
shl : {n} (fin n) => Dom n -> Dom n -> Dom n
shl a b = withBot (a.isBot \/ b.isBot)
(if sz > mask`{n} then top
else interval (drop lo) (drop sz))
where
al, ah : [n + 1]
(al, ah) = zbounds a
bl, bh : [n]
(bl, bh) = ubounds b
// [n + 2] is enough to avoid signed overflow in shift
cl, ch : [n + 2]
cl = if bl < `n then 1 << bl else bit`{n}
ch = if bh < `n then 1 << bh else bit`{n}
(lo, hi) = mulRange (al, ah) (cl, ch)
sz = hi - lo
lshr : {n} (fin n) => Dom n -> Dom n -> Dom n
lshr a b = withBot (a.isBot \/ b.isBot) (interval cl (ch - cl))
where
(al, ah) = ubounds a
(bl, bh) = ubounds b
cl = al >> bh
ch = ah >> bl
ashr : {n} (fin n, n >= 1) => Dom n -> Dom n -> Dom n
ashr a b = withBot (a.isBot \/ b.isBot) (interval cl (ch - cl))
where
(al, ah) = sbounds a
(bl, bh) = ubounds b
cl = al >>$ (if al <$ 0 then bl else bh)
ch = ah >>$ (if ah <$ 0 then bh else bl)
////////////////////////////////////////////////////////////
// Comparisons
ult : {n} (fin n) => Dom n -> Dom n -> Bit
ult a b = (ubounds a).1 < (ubounds b).0
ule : {n} (fin n) => Dom n -> Dom n -> Bit
ule a b = (ubounds a).1 <= (ubounds b).0
slt : {n} (fin n, n >= 1) => Dom n -> Dom n -> Bit
slt a b = (sbounds a).1 <$ (sbounds b).0
sle : {n} (fin n, n >= 1) => Dom n -> Dom n -> Bit
sle a b = (sbounds a).1 <=$ (sbounds b).0
ult_sum_common_equiv : {n} (fin n) => Dom n -> Dom n -> Dom n -> Bit
ult_sum_common_equiv a b c =
if al == ah /\ bl == bh /\ al == bl
then True
else if ~(carry cl c.sz)
then check_same_wrap_interval cl ch
else check_same_wrap_interval cl mask`{n} /\ check_same_wrap_interval 0 ch
where
(cl, ch) = (c.lo, c.lo + c.sz)
(al, ah) = ubounds a
(bl, bh) = ubounds b
check_same_wrap_interval lo hi =
~(carry ah hi) /\ ~(carry bh hi) \/ carry al lo /\ carry bl lo
// A bitmask indicating which bits cannot be determined
// given the interval information in the given domain
unknowns : {n} (fin n, n >= 1) => Dom n -> [n]
unknowns a = if carry a.lo a.sz then ~0 else bits
where
bits = fillright diff
diff = a.lo ^ (a.lo + a.sz)
fillright : {n} (fin n, n >= 1) => [n] -> [n]
fillright x = tail (scanl (||) False x)
fillright_alt : {n} (fin n, n >= 1) => [n] -> [n]
fillright_alt x = x || ((1 << lg2 x) - 1)
property fillright_equiv x = fillright`{16} x == fillright_alt x
////////////////////////////////////////////////////////////
///////////////////////////////////////////////////////////
// Correctness properties
infix 20 =@=
/** Equivalence of bitvector domains. */
(=@=) : {n} (fin n) => Dom n -> Dom n -> Bit
a =@= b = (a.isBot /\ b.isBot)
\/ (~ a.isBot /\ ~ b.isBot /\ a.sz == ~0 /\ b.sz == ~0)
\/ (a == b)
infix 5 <==>
(<==>) : Bit -> Bit -> Bit
(<==>) = (==)
////////////////////////////////////////////////////////////
// Soundness properties
correct_any : {n} (fin n) => [n] -> Property
correct_any x = mem top x
correct_ubounds : {n} (fin n) => Dom n -> [n] -> Property
correct_ubounds a x =
mem a x ==> umem (ubounds a) x
correct_sbounds : {n} (fin n, n >= 1) => Dom n -> [n] -> Property
correct_sbounds a x =
mem a x ==> smem (sbounds a) x
correct_singleton : {n} (fin n) => [n] -> [n] -> Property
correct_singleton x y =
mem (singleton x) y <==> x == y
correct_overlap : {n} (fin n) => Dom n -> Dom n -> [n] -> Property
correct_overlap a b x =
mem a x ==> mem b x ==> overlap a b
correct_overlap_inv : {n} (fin n) => Dom n -> Dom n -> Property
correct_overlap_inv a b =
overlap a b ==> (mem a witness /\ mem b witness)
where
witness = if mem a b.lo then b.lo else a.lo
correct_union : {n} (fin n) => Dom n -> Dom n -> [n] -> Property
correct_union a b x =
(mem a x \/ mem b x) ==> mem (union a b) x
correct_join : {n} (fin n) => Dom n -> Dom n -> [n] -> Property
correct_join a b x =
(mem a x \/ mem b x) ==> mem (join a b) x
correct_meet : {n} (fin n) => Dom n -> Dom n -> [n] -> Property
correct_meet a b x =
(mem a x /\ mem b x) ==> mem (meet a b) x
correct_leq : {n} (fin n) => Dom n -> Dom n -> [n] -> Property
correct_leq a b x =
(leq a b /\ mem a x) ==> mem b x
// Lattice laws
join_commutative : {n} (fin n) => Dom n -> Dom n -> [n] -> Property
join_commutative a b x =
mem (join a b) x == mem (join b a) x
join_idempotent : {n} (fin n) => Dom n -> [n] -> Property
join_idempotent a x =
mem (join a a) x == mem a x
meet_commutative : {n} (fin n) => Dom n -> Dom n -> [n] -> Property
meet_commutative a b x =
mem (meet a b) x == mem (meet b a) x
meet_idempotent : {n} (fin n) => Dom n -> [n] -> Property
meet_idempotent a x =
mem (meet a a) x == mem a x
join_top : {n} (fin n) => Dom n -> [n] -> Property
join_top a x = mem (join a top) x
join_bottom : {n} (fin n) => Dom n -> [n] -> Property
join_bottom a x =
mem (join a bottom) x == mem a x
meet_top : {n} (fin n) => Dom n -> [n] -> Property
meet_top a x =
mem (meet a top) x == mem a x
meet_bottom : {n} (fin n) => Dom n -> [n] -> Property
meet_bottom a x =
~ (mem (meet a bottom) x)
leq_reflexive : {n} (fin n) => Dom n -> Property
leq_reflexive a = leq a a
leq_transitive : {n} (fin n) => Dom n -> Dom n -> Dom n -> Property
leq_transitive a b c =
(leq a b /\ leq b c) ==> leq a c
join_upper_bound : {n} (fin n) => Dom n -> Dom n -> Property
join_upper_bound a b = leq a (join a b)
// `join` preserves non-emptiness: the union of two non-empty domains
// is non-empty.
join_proper : {n} (fin n) => Dom n -> Dom n -> Property
join_proper a b = (~ a.isBot /\ ~ b.isBot) ==> ~ (join a b).isBot
// `meet` cannot conjure elements: if the meet is non-empty, both
// inputs must have been.
meet_proper : {n} (fin n) => Dom n -> Dom n -> Property
meet_proper a b = ~ (meet a b).isBot ==> (~ a.isBot /\ ~ b.isBot)
correct_zero_ext : {m, n} (fin m, m >= n) => Dom n -> [n] -> Property
correct_zero_ext a x =
mem a x ==> mem (zero_ext`{m} a) (zext`{m} x)
correct_sign_ext : {m, n} (fin m, m >= n, n >= 1) => Dom n -> [n] -> Property
correct_sign_ext a x =
mem a x ==> mem (sign_ext`{m} a) (sext`{m} x)
correct_concat : {m, n} (fin m, fin n) => Dom m -> Dom n -> [m] -> [n] -> Property
correct_concat a b x y =
mem a x ==> mem b y ==> mem (concat a b) (x # y)
correct_shrink : {m, n} (fin m, fin n) => Dom (m + n) -> [m + n] -> Property
correct_shrink a x =
mem a x ==> mem (shrink`{m} a) (take`{m} x)
correct_trunc : {m, n} (fin m, fin n) => Dom (m + n) -> [m + n] -> Property
correct_trunc a x =
mem a x ==> mem (trunc`{m} a) (drop`{m} x)
correct_add : {n} (fin n) => Dom n -> Dom n -> [n] -> [n] -> Property
correct_add a b x y =
mem a x ==> mem b y ==> mem (add a b) (x + y)
correct_neg : {n} (fin n) => Dom n -> [n] -> Property
correct_neg a x =
mem a x <==> mem (neg a) (- x)
correct_mul : {n} (fin n) => Dom n -> Dom n -> [n] -> [n] -> Property
correct_mul a b x y =
mem a x ==> mem b y ==> mem (mul a b) (x * y)
correct_mulRange : {n} (fin n, n >= 1) => ([n], [n]) -> ([n], [n]) -> [n] -> [n] -> Property
correct_mulRange a b x y =
smem a x ==> smem b y ==> smem (mulRange a b) (sext x * sext y)
correct_udiv : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Property
correct_udiv a b x y =
mem a x ==> mem b y ==> y != 0 ==> mem (udiv a b) (x / y)
correct_urem : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Property
correct_urem a b x y =
mem a x ==> mem b y ==> y != 0 ==> mem (urem a b) (x % y)
correct_sdivRange : {n} (fin n, n >= 1) => ([n], [n]) -> ([n], [n]) -> [n] -> [n] -> Property
correct_sdivRange a b x y =
smem a x ==> umem b y ==> y != 0 ==> smem (sdivRange a (b.1, b.0)) (sext x /$ sext y)
correct_shrinkRange : {n} (fin n, n >= 1) => ([n], [n]) -> [n] -> [n] -> Property
correct_shrinkRange a x y =
smem a x ==> y != 0 ==> smem (shrinkRange a y) (sext x /$ sext y)
correct_sdiv : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Property
correct_sdiv a b x y =
mem a x ==> mem b y ==> y != 0 ==> mem (sdiv a b) (x /$ y)
correct_srem : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Property
correct_srem a b x y =
mem a x ==> mem b y ==> y != 0 ==> mem (srem a b) (x %$ y)
correct_shl : {n} (fin n) => Dom n -> Dom n -> [n] -> [n] -> Property
correct_shl a b x y =
mem a x ==> mem b y ==> mem (shl a b) (x << y)
correct_lshr : {n} (fin n) => Dom n -> Dom n -> [n] -> [n] -> Property
correct_lshr a b x y =
mem a x ==> mem b y ==> mem (lshr a b) (x >> y)
correct_ashr : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Property
correct_ashr a b x y =
mem a x ==> mem b y ==> mem (ashr a b) (x >>$ y)
correct_slt : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Property
correct_slt a b x y =
slt a b ==> mem a x ==> mem b y ==> x <$ y
correct_sle : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Property
correct_sle a b x y =
sle a b ==> mem a x ==> mem b y ==> x <=$ y
correct_ult : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Property
correct_ult a b x y =
ult a b ==> mem a x ==> mem b y ==> x < y
correct_ule : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Property
correct_ule a b x y =
ule a b ==> mem a x ==> mem b y ==> x <= y
correct_isUltSumCommonEquiv :
{n} (fin n, n >= 1) => Dom n -> Dom n -> Dom n -> [n] -> [n] -> [n] -> Property
correct_isUltSumCommonEquiv a b c x y z =
ult_sum_common_equiv a b c ==>
mem a x ==> mem b y ==> mem c z ==>
(x + z < y + z <==> x < y)
correct_not : {n} (fin n) => Dom n -> [n] -> Property
correct_not a x =
mem a x <==> mem (bnot a) (~ x)
correct_asSingleton : {n} (fin n) => Dom n -> Property
correct_asSingleton a =
isSingleton a ==> a == singleton a.lo
correct_unknowns : {n} (fin n, n >= 1) => Dom n -> [n] -> [n] -> Property
correct_unknowns a x y =
mem a x ==> mem a y ==> (x || unknowns a) == (y || unknowns a)
property p1 = correct_any`{16}
property p2 = correct_ubounds`{16}
property p3 = correct_sbounds`{16}
property p4 = correct_singleton`{16}
property p5 = correct_overlap`{16}
property p5_inv = correct_overlap_inv`{16}
property p6 = correct_union`{8}
property p7 = correct_zero_ext`{32, 16}
property p8 = correct_sign_ext`{32, 16}
property p9 = correct_concat`{16, 16}
property p10 = correct_shrink`{8, 8}
property p11 = correct_trunc`{8, 8}
property p12 = correct_unknowns`{16}
property p13 = correct_asSingleton`{16}
property a1 = correct_add`{8}
property a2 = correct_neg`{16}
property a3 = correct_mul`{4}
property a4 = correct_udiv`{8}
property a5 = correct_urem`{6}
property a6 = correct_sdiv`{6}
property a7 = correct_srem`{6}
property a8 = correct_not`{16}
property a9 = correct_sdivRange`{6}
property a10 = correct_mulRange`{4}
property a11 = correct_shrinkRange`{8}
property s1 = correct_shl`{8}
property s2 = correct_lshr`{8}
property s3 = correct_ashr`{8}
property o1 = correct_slt`{16}
property o2 = correct_sle`{16}
property o3 = correct_ult`{16}
property o4 = correct_ule`{16}
property o5 = correct_isUltSumCommonEquiv`{4}
property lat1 = correct_join`{8}
property lat2 = correct_meet`{8}
property lat3 = correct_leq`{8}
property lat4 = join_commutative`{8}
property lat5 = join_idempotent`{8}
property lat6 = meet_commutative`{8}
property lat7 = meet_idempotent`{8}
property lat8 = join_top`{8}
property lat9 = join_bottom`{8}
property lat10 = meet_top`{8}
property lat11 = meet_bottom`{8}
property lat12 = leq_reflexive`{8}
property lat13 = join_upper_bound`{8}
property lat14 = leq_transitive`{8}
property lat15 = join_proper`{8}
property lat16 = meet_proper`{8}
////////////////////////////////////////////////////////////
// Operations preserve singletons
singleton_overlap : {n} (fin n) => [n] -> [n] -> Bit
singleton_overlap x y =
overlap (singleton x) (singleton y) == (x == y)
singleton_zero_ext : {m, n} (fin m, m >= n) => [n] -> Bit
singleton_zero_ext x =
zero_ext`{m} (singleton x) == singleton (zext`{m} x)
singleton_sign_ext : {m, n} (fin m, m >= n, n >= 1) => [n] -> Bit
singleton_sign_ext x =
sign_ext`{m} (singleton x) == singleton (sext`{m} x)
singleton_concat : {m, n} (fin m, fin n) => [m] -> [n] -> Bit
singleton_concat x y =
concat (singleton x) (singleton y) == singleton (x # y)
singleton_shrink : {m, n} (fin m, fin n) => [m + n] -> Bit
singleton_shrink x =
shrink`{m} (singleton x) == singleton (take`{m} x)
singleton_trunc : {m, n} (fin m, fin n) => [m + n] -> Bit
singleton_trunc x =
trunc`{m} (singleton x) == singleton (drop`{m} x)
singleton_add : {n} (fin n) => [n] -> [n] -> Bit
singleton_add x y =
add (singleton x) (singleton y) == singleton (x + y)
singleton_neg : {n} (fin n) => [n] -> Bit
singleton_neg x =
neg (singleton x) == singleton (- x)
singleton_mul : {n} (fin n) => [n] -> [n] -> Bit
singleton_mul x y =
mul (singleton x) (singleton y) == singleton (x * y)
singleton_mulRange : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
singleton_mulRange x y =
mulRange (x, x) (y, y) == (sext x * sext y, sext x * sext y)
singleton_udiv : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
singleton_udiv x y =
y != 0 ==> udiv (singleton x) (singleton y) == singleton (x / y)
singleton_urem : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
singleton_urem x y =
y != 0 ==> urem (singleton x) (singleton y) == singleton (x % y)
singleton_sdiv : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
singleton_sdiv x y =
y != 0 ==> sdiv (singleton x) (singleton y) == singleton (x /$ y)
singleton_srem : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
singleton_srem x y =
y != 0 ==> srem (singleton x) (singleton y) == singleton (x %$ y)
singleton_shl : {n} (fin n) => [n] -> [n] -> Bit
singleton_shl x y =
shl (singleton x) (singleton y) == singleton (x << y)
singleton_lshr : {n} (fin n) => [n] -> [n] -> Bit
singleton_lshr x y =
lshr (singleton x) (singleton y) == singleton (x >> y)
singleton_ashr : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
singleton_ashr x y =
ashr (singleton x) (singleton y) == singleton (x >>$ y)
singleton_slt : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
singleton_slt x y =
slt (singleton x) (singleton y) == (x <$ y)
singleton_sle : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
singleton_sle x y =
sle (singleton x) (singleton y) == (x <=$ y)
singleton_ult : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
singleton_ult x y =
ult (singleton x) (singleton y) == (x < y)
singleton_ule : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
singleton_ule x y =
ule (singleton x) (singleton y) == (x <= y)
property i01 = singleton_overlap`{16}
property i02 = singleton_zero_ext`{32, 16}
property i03 = singleton_sign_ext`{32, 16}
property i04 = singleton_concat`{16, 16}
property i05 = singleton_shrink`{8, 8}
property i06 = singleton_trunc`{8, 8}
property i07 = singleton_add`{8}
property i08 = singleton_neg`{16}
property i09 = singleton_mul`{4}
property i10 = singleton_udiv`{8}
property i11 = singleton_urem`{8}
property i12 = singleton_sdiv`{8}
property i13 = singleton_srem`{8}
property i14 = singleton_shl`{8}
property i15 = singleton_lshr`{8}
property i16 = singleton_ashr`{8}
property i17 = singleton_slt`{16}
property i18 = singleton_sle`{16}
property i19 = singleton_ult`{16}
property i20 = singleton_ule`{16}
property i21 = singleton_mulRange`{4}
////////////////////////////////////////////////////////////
// Associativity/commutativity properties
comm_overlap : {n} (fin n) => Dom n -> Dom n -> Bit
comm_overlap a b = overlap a b <==> overlap b a
comm_add : {n} (fin n) => Dom n -> Dom n -> Bit
comm_add a b = add a b == add b a
assoc_add : {n} (fin n) => Dom n -> Dom n -> Dom n -> Bit
assoc_add a b c = add a (add b c) =@= add (add a b) c
comm_mul : {n} (fin n) => Dom n -> Dom n -> Bit
comm_mul a b = mul a b == mul b a
/* mul is not associative! */
assoc_mul : {n} (fin n) => Dom n -> Dom n -> Dom n -> Bit
assoc_mul a b c = mul a (mul b c) =@= mul (mul a b) c
comm_mulRange :
{i, j} (fin i, fin j, i >= 1, j >= 1) => ([i], [i]) -> ([j], [j]) -> Bit
comm_mulRange a b =
a.0 <=$ a.1 ==> b.0 <=$ b.1 ==> mulRange a b == mulRange b a
assoc_mulRange :
{i, j, k} (fin i, fin j, fin k, i >= 1, j >= 1, k >= 1) =>
([i], [i]) -> ([j], [j]) -> ([k], [k]) -> Bit
assoc_mulRange a b c =
a.0 <=$ a.1 ==>
b.0 <=$ b.1 ==>
c.0 <=$ c.1 ==>
mulRange a (mulRange b c) == mulRange (mulRange a b) c
property c1 = comm_overlap`{16}
property c2 = comm_add`{16}
property c3 = assoc_add`{16}
property c4 = comm_mul`{4}
property c5 = comm_mulRange`{4,4}
property c6 = assoc_mulRange`{3,3,3}
////////////////////////////////////////////////////////////
// Additional properties about union
comm_union : {n} (fin n) => Dom n -> Dom n -> Bit
comm_union a b = union a b == union b a
/* union is actually not associative! */
assoc_union : {n} (fin n) => Dom n -> Dom n -> Dom n -> Bit
assoc_union a b c = union a (union b c) == union (union a b) c
/* union always has a lower bound equal to one of the input lower bounds */
lo_union : {n} (fin n) => Dom n -> Dom n -> Bit
lo_union a b =
c.isBot \/ c =@= top \/ c.lo == a.lo \/ c.lo == b.lo
where c = union a b
/* union always has an upper bound equal to one of the input upper bounds */
hi_union : {n} (fin n) => Dom n -> Dom n -> Bit
hi_union a b = c.isBot \/ c =@= top \/ c_hi == a_hi \/ c_hi == b_hi
where
c = union a b
a_hi = a.lo + a.sz
b_hi = b.lo + b.sz
c_hi = c.lo + c.sz
/* union doesn't return top unless necessary */
nontriv_union : {n} (fin n) => Dom n -> Dom n -> [n] -> Bit
nontriv_union a b x =
union a b =@= top ==> mem a x \/ mem b x
/* union of opposite intervals prefers to exclude zero */
nonzero_union : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
nonzero_union lo sz =
mem (union a b) half /\
(~ mem a 0 ==> ~ mem b 0 ==> ~ mem (union a b) 0)
where
half : [n]
half = reverse 1
a = interval lo sz
b = interval (lo + half) sz
property u1 = comm_union`{16}
property u2 = lo_union`{16}
property u3 = hi_union`{16}
property u4 = nontriv_union`{8}
property u5 = nonzero_union`{16}