/*

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

////////////////////////////////////////////////////////////

type Dom n = { lo : [n], sz : [n] }

interval : {n} (fin n) => [n] -> [n] -> Dom n
interval l s = { lo = l, sz = s }

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 = 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.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 = 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 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

////////////////////////////////////////////////////////////

zero_ext : {m, n} (fin m, m >= n) => Dom n -> Dom m
zero_ext a = 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 = 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 = 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 =
  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 =
  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 =
  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 = 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 = interval (~ ah) a.sz
  where ah = a.lo + a.sz

mul : {n} (fin n) => Dom n -> Dom n -> Dom n
mul a b =
  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 = 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 =
  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 =
  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 =
  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 =
  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 = 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 = 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.sz == ~0 /\ b.sz == ~0) \/ (a == b)

infix 5 <==>

(<==>) : Bit -> Bit -> Bit
(<==>) = (==)

////////////////////////////////////////////////////////////
// Soundness properties

correct_top : {n} (fin n) => [n] -> Bit
correct_top x = mem top x

correct_ubounds : {n} (fin n) => Dom n -> [n] -> Bit
correct_ubounds a x =
  mem a x ==> umem (ubounds a) x

correct_sbounds : {n} (fin n, n >= 1) => Dom n -> [n] -> Bit
correct_sbounds a x =
  mem a x ==> smem (sbounds a) x

correct_singleton : {n} (fin n) => [n] -> [n] -> Bit
correct_singleton x y =
  mem (singleton x) y <==> x == y

correct_overlap : {n} (fin n) => Dom n -> Dom n -> [n] -> Bit
correct_overlap a b x =
  mem a x ==> mem b x ==> overlap a b

correct_overlap_inv : {n} (fin n) => Dom n -> Dom n -> Bit
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] -> Bit
correct_union a b x =
  (mem a x \/ mem b x) ==> mem (union a b) x

correct_zero_ext : {m, n} (fin m, m >= n) => Dom n -> [n] -> Bit
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] -> Bit
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] -> Bit
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] -> Bit
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] -> Bit
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] -> Bit
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] -> Bit
correct_neg a x =
  mem a x <==> mem (neg a) (- x)

correct_mul : {n} (fin n) => Dom n -> Dom n -> [n] -> [n] -> Bit
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] -> Bit
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] -> Bit
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] -> Bit
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] -> Bit
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] -> Bit
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] -> Bit
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] -> Bit
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] -> Bit
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] -> Bit
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] -> Bit
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] -> Bit
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] -> Bit
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] -> Bit
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] -> Bit
correct_ule a b x y =
  ule a b ==> mem a x ==> mem b y ==> x <= y

correct_ult_sum_common_equiv :
  {n} (fin n, n >= 1) => Dom n -> Dom n -> Dom n -> [n] -> [n] -> [n] -> Bit
correct_ult_sum_common_equiv 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_bnot : {n} (fin n) => Dom n -> [n] -> Bit
correct_bnot a x =
  mem a x <==> mem (bnot a) (~ x)

correct_isSingleton : {n} (fin n) => Dom n -> Bit
correct_isSingleton a =
  isSingleton a ==> a == singleton a.lo

correct_unknowns : {n} (fin n, n >= 1) => Dom n -> [n] -> [n] -> Bit
correct_unknowns a x y =
  mem a x ==> mem a y ==> (x || unknowns a) == (y || unknowns a)

property p1 = correct_top`{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_isSingleton`{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_bnot`{16}
property a9 = correct_sdivRange`{6}

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_ult_sum_common_equiv`{4}

////////////////////////////////////////////////////////////
// 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}

////////////////////////////////////////////////////////////
// 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 =
  union a b == top \/ (union a b).lo == a.lo \/ (union a b).lo == b.lo

/* 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 == 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}