The idea is to allow more stringent range checking for cast expressions and assert a lack of overflow for arithmetic expressions.
- Arithmetic constraints ensure that the final type does not overflow the modulus (in positive direction) or zero (in negative direction)
- The "cast" expression will be checked to recombine properly into the indicated type, being statically guaranteed to fit in the target limbs
- In addition, to support external knowledge and proofs (such as $b \cdot x + (1 - b) \cdot y \in [\min(x, y), \max(x, y)]$), we introduce a new type of cast (e.g.
cast! or fits, tbd) that delegates the responsibility of validating the correct fit to an external entity (the writers and reviewers), while still ensuring the structure is a proper match (as CastExpr does now)
The idea is to allow more stringent range checking for cast expressions and assert a lack of overflow for arithmetic expressions.
cast!orfits, tbd) that delegates the responsibility of validating the correct fit to an external entity (the writers and reviewers), while still ensuring the structure is a proper match (asCastExprdoes now)