:prove exhausts memory on a small number of cases

[msaaltink]

Not a bug, but surprising: you'd think that :prove could handle something that :exhaust says has 4 cases, or 8 cases, but on my machine it just exhausts all avaliable memory. Here's the code, a pointless attempt to implement 2-adic arithmetic in infinite lists:

// 2-adics, as infinite little-endian streams of bits
type two_adic = [inf]
to_2: {n} (fin n) => [n] -> two_adic
to_2 x = (reverse x) # zero 
from_2: {n} (fin n) => two_adic -> [n]
from_2 x = reverse (take x)
zero_2: two_adic
zero_2 = zero
one_2: two_adic
one_2 = [True] # zero_2
neg_one_2: two_adic
neg_one_2 = ~ zero_2

inc_2: two_adic -> two_adic
inc_2 x = y where
  y = [b != carry | b <- x | carry <- cs]
  cs = [True] # [b && carry | b <- x | carry <- cs]
incOK: {n} (fin n, n>=1) => [n] -> Bit
property incOK x = from_2 (inc_2 (to_2 x)) == x+1

neg_2 x = inc_2 (~ x)
negOK: {n} (fin n, n>=1) => [n] -> Bit
property negOK x = - x == from_2 (neg_2 (to_2 x))

double_2 x = [False] # x

add_2 x y = z where
  z = [xor3 a b c | a <- x | b <- y | c <- cs]
  cs = [False] # [maj3 a b c | a <- x | b <- y | c <- cs]
  xor3 b1 b2 b3 = b1 != (b2 != b3)
  maj3 b1 b2 b3 = if b1 then b2||b3 else b2&&b3
addOK: {n} (fin n, n>=1) => [n] -> [n] -> Bit
property addOK x y = (x+y) == from_2 (add_2 (to_2 x) (to_2 y))

sub_2 x y = add_2 x (neg_2 y)
subOK: {n} (fin n, n>=1) => [n] -> [n] -> Bit
property subOK x y = (x-y) == from_2 (sub_2 (to_2 x) (to_2 y))

times_2: two_adic -> two_adic -> two_adic
times_2 ([b] # x) y =
  if b then [y@0] # ( add_2 (tail y) (times_2 x y) )
   else double_2 (times_2 x y)

timesOK: {n} (fin n, n>=1) => [n] -> [n] -> Bit
property timesOK x y = (x*y) == from_2 (times_2 (to_2 x) (to_2 y))

// can divide by any odd number
divide_2: two_adic -> two_adic -> two_adic
divide_2 z y = if y@0 then f z else zero_2 // was undefined, but :check hates that
  where
tl_y = tail y
f ([b] # x) = [b] # (if b then f (sub_2 x tl_y) else f x)

divideOK: {n} (fin n, n>=1) => [n] -> [n-1] -> Bit
property divideOK x y' =
  y * (from_2 (divide_2 (to_2 x) (to_2 y))) == x
  where y = y' # [True] // y must be odd.  y = 2y' + 1

Now

:exhaust timesOK`{1}

works fine,with 2 cases, and I can exhaust or check small instances. Similarly for dividesOK; with small n there is a smallish number of cases and exhaust and check work fine. Computation with these definitions is also fine. However,

:prove timesOK`{1}

and

:prove dividesOK`{2}

just gobble up all available memory - about 6GB on my machine. This seems odd! I'll guess there's something funny about how :prove deals with recursions.

[weaversa]

I haven't looked into this in any detail, but, it could be a symbolic termination problem. I am guessing this because subtract is definitely not symbolically terminating.

[brianhuffman]

This might be a symbolic termination problem, as you say, or it might be that the data structures and algorithms used by the symbolic simulator for infinite streams are too strict. I'll have a closer look the next time I'm in the office.

[weaversa]

I've looked over the code again and I don't think this is a symbolic termination problem. If it were, setting iteSolver=on should be enough to get these small proofs to go through. I tried the proofs again w/ this extra setting and the proofs still hang.

[brianhuffman]

Here's the minimal example I came up with:

copy : [inf] -> [inf]
copy ([b] # x) = if b then [True] # copy x else [False] # copy x

property ok = copy ([True] # zero) @ 0

[brianhuffman]

Fixed in fde77d7. Added regression test in 234aa32.