Issue using with latest F*

[obicons]

Hi team,

I'm trying to use vale for a project. Unfortunately, I've run into a problem: I can't make F* build at 9f2cb7e2c9934b0134b46d5c83a5a5c074d8463b for some reason, although I can build more recent commits. So, using F* at version 9f2cb7e2c9934b0134b46d5c83a5a5c074d8463b seems like a non-option for new users.

But recent versions of F* do not work with Vale. In particular, when I run scons --FSTAR --FSTAR-PATH=[path to my fstar] --FSTAR-MY-VERSION, I see this error:

##### Verification error
Printing contents of obj/fstar/specs/defs/Words.Two_s.fsti.verified.stderr #####
fstar/specs/defs/Words.Two_s.fsti(27,6-27,17): (Error 114) Type of pattern (Words_s.two (Words_s.natN (Words_s.pow2_norm size))) does not match type of scrutinee (Words_s.two (Words_s.natN (match size with
        | 0 -> 1
        | _ -> 2 * Prims.pow2 (size - 1)))); parameter Words_s.natN (Words_s.pow2_norm size) <> parameter Words_s.natN (match size with
    | 0 -> 1
    | _ -> 2 * Prims.pow2 (size - 1))
1 error was reported (see above)

I looked deeper into this issue. The problem is in this definition:

unfold
let two_to_nat_unfold (size:nat) (x:two (natN (pow2_norm size))) : natN (pow2_norm (2 * size)) =
  let n1 = pow2_norm size in
  let n2 = pow2_norm (2 * size) in
  let Mktwo x0 x1 = x in
  int_to_natN n2 (x0 + x1 * n1)

The types seem correct to me. I tried adding fuel (#push-options "--max_fuel 256") in a fruitless attempt to get F* to normalize, but that didn't help. I noticed this recent PR in F* -- at a first glance, I think it's possible this introduced the issue. But I'm not an expert, so take it with a grain of salt.

[Chris-Hawblitzel]

Ok, I updated to the latest F* version, so hopefully it should work now.