vstd: signedness casts preserve modulo

[mmcloughlin]

Prove that casts between iN and uN preserve the value modulo the integer
range.

Updates #1854

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[tjhance]

If we're casting from iN to uN or vice versa, there is a much easier way to express the relationship that does not involve mod, just a single if statement:

x as uN == (if x < 0 { x + uN::MAX + 1 } else { x })

For something fundamental like this, I think we should consider exporting it in the AIR prelude, where most of the other arithmetic axioms are. Right now, we don't export anything for truncations because we don't want to bring in nonlinear stuff by default, but an exception could be made for the truncations that don't require modulo.

[mmcloughlin]

For context, these lemmas help with some crypto proofs that depend arithmetic modulo 2^n,
and the fact that these casts preserve the value modulo word size. It may be useful to have them even if we extend the prelude as you describe.

To make sure I understand what you mean, we'd extend the prelude with a couple of new operators for sign casts? Verus would use them when it sees casts between iN and uN?

[Chris-Hawblitzel]

If we're casting from iN to uN or vice versa, there is a much easier way to express the relationship that does not involve mod, just a single if statement

Verus would use them when it sees casts between iN and uN?

I think there's a simple variant that takes advantage of this optimization:

pub broadcast proof fn u8_to_i8(u: u8)
    requires
        u >= 0x80
    ensures
        #[trigger] (u as i8) == u - 0x100,
{
    assert(u as i8 == u - 0x100) by(bit_vector) requires u >= 0x80;
}

proof fn test() {
    broadcast use u8_to_i8;
    assert(0x20u8 as i8 == 0x20i8);
    assert(0xf0u8 as i8 == -0x10i8);
}

In AIR, the broadcast looks like:

;; Broadcast crate::u8_to_i8
(axiom (=>
  (fuel_bool fuel%u8_to_i8.)
  (forall ((u! Int)) (!
    (=>
     (uInv 8 u!)
     (=>
      (>= u! 128)
      (= (iClip 8 u!) (Sub u! 256))
    ))
    :pattern ((iClip 8 u!))
))))

This takes advantage of the type invariant (uInv 8 u!) that gets added because u has type u8. Because of this type invariant, no mod operation is needed. Furthermore, the broadcast only needs to prove something about the u >= 0x80 case, because the clients already know the u < 0x80 case from the prelude's existing axioms about iClip.