F# build of F* rejects 0ul as out of range

[catalin-hritcu]

It seems that @nikswamy's recent code for checking constant bounds (a8c1fbc#diff-0b9e97904ace9e5e55b6cdcd8e842211R642) does not work with the F# build. This appeared in a larger context (#1023 (comment)), but it can be simplified to just this:

let foo = 0ul

The error message is:

(Error) 0 is not in the expected range for FStar.UInt32

This works just fine with the OCaml build of F*.

[catalin-hritcu]

Ouch, this seems caused by integers in the F# build being bounded, and pow2 32 returning -1. Maybe time to fix this blatant unsoundness biting us back? :)

[nikswamy]

Sigh. Yes, the F# build of F* is not sound. We've known this for a long time, since we do not use bignums for representing mathematical integers in F#. As such, the F# build is mainly used for bootstrapping currently. Fixing it to use .net bignums should be possible, but it's tedious work. We should do it at some point.

[catalin-hritcu]

Removed the duplicate flag since there might be place for short term mitigations targeted only at this particular issue (while still punting on #1054). Personally, I would very much like if we could have the F# version to run all the regular regressions as well, so that we're forced to keep it up to date. And we didn't seem too far from this (#1023), until this came along at least.

[A-Manning]

This is fixed in #1283.

These overflow errors are quite annoying to debug when they pop up, perhaps the F# build should be compiled with the --checked flag?

[A-Manning]

Can this be closed now?