Add proof-irrelevant refinement type from Liquid Haskell

[mborland]

Liquid Haskell has integer types of the form {v:Int | P(v)} where P(v) is a compile time refinement predicate. A verified_u32 containing purely consteval construction and mathematical operations effective has P(v) = every operation that produced this value was statically checked for overflow. Basically the type becomes read-only at runtime

[mborland]

See also: https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2025/p3603r0.html