UInt64 bug, possibly due to C coercion rules after a constant fold

[BarryBo]

This is non-blocking. I have a workaround.

In F* code, if I write U64.(0UL -^ 1UL), I expect the result to be 64-bit 0xff...ffUL.

But in the extracted C code, I see the expression is constant-folded to (uint64_t)-1U;

However, it looks like both gcc and MSVC extend this by first converting -1 to a uint32 (0xffffffff) then unsigned-extending to 64-bit, to get 0x00000000ffffffff.

The generated code from gcc is:
; load 0xffffffff into 32-bit eax, which is zero-extended by the hw to 0x00000000ffffffff
1a: b8 ff ff ff ff mov $0xffffffff,%eax
; pass the value onward
1f: 48 89 45 f8 mov %rax,-0x8(%rbp)

Attached is a test.fst that repros the problem. Its comment block has the kremlin and gcc command lines needed to repro.
test.txt