FStar.UInt discrepancy

[wintersteiger]

This is really more of a request for comments than an actual bug report and issues related to mine have been discussed before (e.g., #357) and this is probably hard to fix with only minor benefits for everybody who's not me.

In my current Windows/F#/.NET setup FStar.UInt.fst currently fails to verify, while the same goes through fine in my Ubuntu/OCaml setup. The core of the issue is this:

module Bug

let _ = 
  assert_norm (pow2 31 == 2147483648)

fails via F#, but verifies via OCaml.

I suppose this is related to the 2^31 limited OCaml ints, but my immediate consequence is that I get different queries into Z3, when I really expect the same. There are too many steps between the input and the Z3 query for me to comprehend all of them, but superficially it looks to me like via F# we get additional constraints because pure_return and pure_null_wp are instantiated for the pow2 call, while they are not added via OCaml. My guess is that OCaml (or our .ml files) propagates the constant and simplifies the pow2 call before any constraints are generated, while F# thinks that 31 is big enough not to compute the result at compile time. (The consequence is that Z3 sees six extra quantifiers that make it bail out early.)

In general, what's the strategy regarding this and similar examples? Is the goal to get both toolchains behave exactly the same, or is it okay if one of them can't prove something the other can prove?

[catalin-hritcu]

Tough one. Making the two toolchains behave as close as possible is a worthy goal. Given this kind of example, do you think there is any chance we can make both toolchains behave exactly the same?

[catalin-hritcu]

The same code also appears in ulib/FStar.Int (copy pasted?) and fails in the same way.

[catalin-hritcu]

Found yet another place where this code was copied: micro-benchmarks/Normalization.fst

[A-Manning]

Regarding ulib failing to build with the F# build of F* -

If I understand this issue correctly, F# does not optimise pow2 31 to a constant, since the recursion is too deep here.
Would it suffice to just use a more efficient algorithm for pow2? It's possible to compute pow2 n in logarithmic recursive depth in n, rather than linear in n, through something like

val pow2': nat -> pos
let pow2' n = let open FStar.Mul in
    let rec aux (x:pos) (n:nat) (acc:pos)
        : Tot pos (decreases n) =
        match n with
        | 0 -> acc
        | _ -> if n%2=0 then aux (x*x) (n/2) acc
                        else aux (x*x) (n/2) (acc*x)
    in
    aux 2 n 1

Edit: a better solution, if this were the problem, would be to prove that pow2 (m*n) = powx (pow2 m) n
which would allow us to do, for example, assert_norm (powx (pow2 8) 8 == 18446744073709551616) as the proof for the pow2 64 case - using 16 recursive unfoldings, rather than 64.

[catalin-hritcu]

@A-Manning worth giving this a try

[A-Manning]

This bug is not being caused by differences in F# vs OCaml compiler optimisation.

It's a result of the F# build using int32 arithmetic.
The following will verify with an F# build -

val pow2_values: x:nat -> Lemma
  (requires True)
  (ensures (let p = pow2 x in
   match x with
   ...
   //| 31 -> p= 2147483648
   | 32 -> p=0
   | 63 -> p=0
   | 64 -> p=0
   | _  -> True))
let pow2_values x = match x with
   ...
   //| 31 -> assert_norm (pow2 31 == 2147483648)
   | 32 -> assert_norm (pow2 32 == 0)
   | 63 -> assert_norm (pow2 63 == 0)
   | 64 -> assert_norm (pow2 64 == 0)
   | _  -> ()

If we add the 31 case back in, it fails even with the 'correct' 32 bit arithmetic, because the F# build does not parse -2147483648 correctly. This is odd, since in F# the max int32 is 2147483647, and the min is -2147483648, but the F# build can parse 2147483648 and not -2147483648.

...
  (ensures (let p = pow2 x in   
  match x with
   ...
   | 31  -> p= -2147483648
  ...
let pow2_values x = match x with
   ...
   | 31  -> assert_norm (pow2 31 == -2147483648)

Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
int_of_string

[A-Manning]

Fixed in #1283