F*: pattern matching is disallowed on `usize`s, `isize`s (+`u128`/`i128`)

[W95Psp]

Currently we do not support matching on usize in the F* backend.

This is because of our encoding of usize: a usize is defined as an opaque type being maybe a u16, a u32, or maybe a u64. This encoding is important since the size of usizes varies according to the architecture being targetted.

Solutions:

• rewrite matches
• define usize as a x: u64 {range (v x) u16_inttype \/ range (v x) u32_inttype \/ range (v x) u64_inttype} (wdyt about this @karthikbhargavan?)

[W95Psp]

The issue is that we do not know the size of usize on the target platform. So, it is better to cast the usize into u8or u16 or whatever in the pattern match:

match (x as u8) {.
  0 => ...
} ```

Originally posted by @karthikbhargavan in https://github.com/hacspec/hax/issues/598#issuecomment-2049382155

[franziskuskiefer]

There's a design in #806 that needs to get implemented.