Integer refinement type

Issue stacks-network/reference#2 proposes to make uint a subtype of int, with the type checker and runtime system verifying that these are nonnegative integers. Subtyping integers can be generalized in integer refinement types.

Integers can be refined by specifying their range with a low and/or high boundary. A simple syntax borrowed from Common Lisp is (int low high). For example, here are some refined integer subtypes:

• Digit is an integer from 0 to 9: (int 0 9)
• Months are numbered from 1 to 12: (int 1 12)
• Cents are bound between 0 and 99: (int 0 99)
• Sign is -1, 0 or 1: (int -1 1)
• Nonnegative integers (uint) go from 0 and up: (int 0)
• Positive integers go from 1 and up: (int 1)

Integer refinement subtypes informs the type system about the potential range of integers. This can make Clarity code more succinct, opening for automatically verifying that integers stay in range, rather than require developers to implement defensive code that checks the boundary assertions. It also opens for more powerful type inference, where the possible boundaries of integer expressions can be determined during analytics.

Currently, integers are allocated 16 bytes (2^128), which can be wasteful. Knowing the range of integers allows the system to pack integers, only using the actually required amount of bytes in storage.

Start by reviewing stacks-network/reference#2 and the existing type checker and runtime system, which the issue identifies as the affected entry points. Define how (int low high) and its open-ended forms should express ranges, then determine how range verification, inference, and storage packing fit together. Done means integer refinement subtypes are supported consistently across those areas.