Support for mixed sign and size in integer type conversions

[rod-chapman]

Currently, it appears that Verus does not "know" the semantics of integer type conversions that change the signedness of the argument, or its size (either truncating or expanding the representation.) Verus currently issues a "truncating warning", and nothing can be proven about the result of the conversion.

Rust Reference 8.2.4 says that these conversions are well-defined, so they should be supported. They are also common in cryptographic code.

The work could be broken down into several PR's. For example.

1. Same size, changing sign (e.g. i32 <-> u32 and so on)
2. Expanding, same sign (e.g. u8 -> u16, i16 -> i32)
3. Truncating, same sign (e.g. u16 -> u8, i32 -> i16)
4. Expanding, mixed signedness (e.g. i8 -> u16, u16 -> i32)
5. Truncating, mixed signedness (e.h. u32 -> i8, i16 -> u8)

Did I miss any cases?

[tjhance]

These semantics are not exported in Verus's default prover mode, but they are available in other modes such as 'bit_vector' or 'compute'.

Relevant docs:

• https://verus-lang.github.io/verus/guide/bitvec.html#integer-wrapping-and-truncation
• https://verus-lang.github.io/verus/guide/reference-as.html

[tjhance]

You can also silence the warnings using the truncate attribute: https://verus-lang.github.io/verus/guide/reference-attributes.html#verifiertruncate

[mmcloughlin]

Broadly, as @tjhance says I think Verus can reason about this with the help of bit_vector proofs. Some lemmas may make it easier though.

For case 1 above, some lemmas for properties of sign casts: #1855

[Chris-Hawblitzel]

Since all the conversions have simple and well-defined semantics, maybe we should support them all without the need for bit_vector. @tjhance points:

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.

Even the other truncations, like u16 -> u8, are still linear arithmetic, although the mod by a constant can be more expensive than + and -. Currently, the verifier::truncate attribute provides two levels of handling cast truncation: recommends-warn if a truncation is uninterpreted, and no warning (truncation is still uninterpreted). How about if we add a third level (via an additional attribute like verifier::truncate(exact)): no warning, and cast truncation is interpreted according to Rust semantics, using the most efficient operation available (either add/subtract, or mod by a constant). Furthermore, how about if we allow verifier::truncate (and the new third-level attribute) to be applied to functions, modules, and crates, so the attributes don't have to appear separately on every individual arithmetic expression?

Proposed names for the three levels:

• verifier::truncate(warn) is the default -- it leaves truncation uninterpreted and warns in recommends checking if truncation happens
• verifier::truncate(allow) means allow uninterpreted truncation with no warning (and is the same as verifier::truncate, for backwards compatibility)
• verifier::truncate(exact) means don't warn and compute the exact interpreted result of truncation

[tjhance]

I'm a fan of making the attribute hierarchical, like loop_isolation, though I don't quite how you're planning to encode the optional-interpretedness aspect. Like, the operation is already defined in Verus according to Rust semantics, you just have to opt-in to the definition (by employing the right prover mode). I don't understand what it would mean to opt-in on an operation-by-operation basis. Like if you do:

let a = #[verifier::truncate(allow)] x as u32;
let b = #[verifier::truncate(exact)] x as u32;
assert(a == b);

What happens?

[Chris-Hawblitzel]

if you do:

let a = #[verifier::truncate(allow)] x as u32;
let b = #[verifier::truncate(exact)] x as u32;
assert(a == b);

What happens?

That's a good point. My original thought was something like:

axiom forall|x| #[trigger] truncate_interpreted(x) == x % ...;
axiom forall|x| #[trigger] truncate_interpreted(x) == truncate_uninterpreted(x)
...
let a = truncate_uninterpreted(x);
let b = truncate_interpreted(x);
assert(a == b); // succeeds

but after thinking about it more I worry that this triggering could lead to instability. So, yes, I would rather have something more like opting in to the interpreted definition in particular contexts. broadcast use could work for this if we allow triggering on specific fixed-width possibly-truncating integer casts (e.g. triggering specifically on u32->u16 casts or on i32->u32 casts). An attribute could also work, although this might involve reinventing some of what broadcast use already does.

[tjhance]

I wonder if we're overthinking this, and we should just enable it always. Like you said, it's linear arithmetic.

[rod-chapman]

I agree... the semantics are well-defined so always model them.

Optionally issue a suppressible warning for the non-obvious cases where changing sign and/or truncating might result in the user not getting what they expected.

[tjhance]

I think there are 2 common cases:

1. Truncation isn't desired. You expect the integer to be in-bounds and want the truncation to just be the identity function integers.
2. Truncation is desired, in which case you probably care about the exact semantics.

I think Case 3, where truncation is desired, but you either don't care about the exact semantics (or find that modulo-consting makes the query too expensive) is probably not that common.

And I wonder if we're not serving Case 1 that well either. If the user wants the operation to be in-bounds, should we be doing something stronger than a recommends check?

So maybe the thing to be toggled should not be the semantics of truncation, but whether it's allowed or denied.

[Chris-Hawblitzel]

I wouldn't want to enable the mod computation by default, even if it is just linear arithmetic, because mod gets expensive, especially for large numbers. Some of our most notorious timeouts in past verification projects were in lemmas about 4-bytes-to-u32 and u32-to-4-bytes conversions, or even worse, 8-bytes-to-u64 and u64-to-8-bytes conversions, even thought these were entirely linear arithmetic implemented out of add, multiply, divide, and mod. The special case of signed-to-unsigned or unsigned-to-signed that doesn't require mod would be fine. But I think you should have to explicitly opt in to more general cases, and I think this is easy to achieve with broadcast. I've pasted my proposed library for this below.

I did a couple experiments, the first of which didn't go well and the second of which worked fine. First, regarding:

if we allow triggering on specific fixed-width possibly-truncating integer casts (e.g. triggering specifically on u32->u16 casts or on i32->u32 casts)

Right now, there's just one AIR operator (uClip 32 ...) representing all casts to u32 (similarly for other u* types) and one operator (iClip 32 ...) representing all casts to i32 (similarly for other i* types). So a trigger on (uClip 32 x) actually matches all casts to u32, including u64 -> u32, i32 -> u32, etc. So first, I tried an experiment of adding more specific wrappers around uClip and iClip to make it possible to pattern match just on a specific cast like i32 -> u32:

        (declare-fun [u_clip] (Int Int) Int)
        (declare-fun [i_clip] (Int Int) Int)
...
        (declare-fun [u_cast] (Int [typ] [typ] Int) Int)
        (declare-fun [i_cast] (Int [typ] [typ] Int) Int)

        (axiom (forall ((bits Int) (from [typ]) (to [typ]) (i Int)) (!
            (= ([u_cast] bits from to i) ([u_clip] bits i))
            :pattern (([u_cast] bits from to i))
        )))
        (axiom (forall ((bits Int) (from [typ]) (to [typ]) (i Int)) (!
            (= ([i_cast] bits from to i) ([i_clip] bits i))
            :pattern (([i_cast] bits from to i))
        )))

where an i32 -> u32 cast, for example, is translated into the uCast wrapper, with specific from = i32 and to = u32 arguments, instead of into uClip directly. Even though this is a very thin wrapper, this change broke a surprising amount of existing code, often having to do with the awkward boundary between linear and nonlinear arithmetic (especially in the presence of Rust consts). Based on this outcome, I'm not enthusiastic about complicating uClip and iClip.

Second, regarding:

So, yes, I would rather have something more like opting in to the interpreted definition in particular contexts. broadcast use could work for this if

I used the existing uClip and iClip as triggers for a simple and complete library of integer casts in the style of #1855 :

pub broadcast proof fn clip_u8(i: int)
    ensures
        #[trigger] (i as u8) == i % 0x100,
{
    admit();
}

pub broadcast proof fn clip_u16(i: int)
    ensures
        #[trigger] (i as u16) == i % 0x1_0000,
{
    admit();
}

pub broadcast proof fn clip_u32(i: int)
    ensures
        #[trigger] (i as u32) == i % 0x1_0000_0000,
{
    admit();
}

pub broadcast proof fn clip_u64(i: int)
    ensures
        #[trigger] (i as u64) == i % 0x1_0000_0000_0000_0000,
{
    admit();
}

pub broadcast proof fn clip_u128(i: int)
    ensures
        #[trigger] (i as u128) == i % (u128::MAX + 1),
{
    admit();
}

pub broadcast proof fn clip_i8(i: int)
    ensures
        #![trigger (i as i8)]
        i % 0x100 < 0x80 ==> (i as i8) == i % 0x100,
        i % 0x100 >= 0x80 ==> (i as i8) == i % 0x100 - 0x100,
{
    admit();
}

pub broadcast proof fn clip_i16(i: int)
    ensures
        #![trigger (i as i16)]
        i % 0x1_0000 < 0x8000 ==> (i as i16) == i % 0x1_0000,
        i % 0x1_0000 >= 0x8000 ==> (i as i16) == i % 0x1_0000 - 0x1_0000,
{
    admit();
}

pub broadcast proof fn clip_i32(i: int)
    ensures
        #![trigger (i as i32)]
        i % 0x1_0000_0000 < 0x8000_0000 ==> (i as i32) == i % 0x1_0000_0000,
        i % 0x1_0000_0000 >= 0x8000_0000 ==> (i as i32) == i % 0x1_0000_0000 - 0x1_0000_0000,
{
    admit();
}

pub broadcast proof fn clip_i64(i: int)
    ensures
        #![trigger (i as i64)]
        i % 0x1_0000_0000_0000_0000 < 0x8000_0000_0000_0000 ==> (i as i64) == i % 0x1_0000_0000_0000_0000,
        i % 0x1_0000_0000_0000_0000 >= 0x8000_0000_0000_0000 ==> (i as i64) == i % 0x1_0000_0000_0000_0000 - 0x1_0000_0000_0000_0000,
{
    admit();
}

pub broadcast proof fn clip_i128(i: int)
    ensures
        #![trigger (i as i128)]
        i % (u128::MAX + 1) < (u128::MAX + 1) / 2 ==> (i as i128) == i % (u128::MAX + 1),
        i % (u128::MAX + 1) >= (u128::MAX + 1) / 2 ==> (i as i128) == i % (u128::MAX + 1) - (u128::MAX + 1),
{
    admit();
}

broadcast group exact_integer_casts {
    clip_u8,
    clip_u16,
    clip_u32,
    clip_u64,
    clip_u128,
    clip_i8,
    clip_i16,
    clip_i32,
    clip_i64,
    clip_i128,
}

proof fn test() {
    broadcast use exact_integer_casts;
    assert(0x120u32 as u8 == 0x20u8);
    assert(0x12000u32 as u16 == 0x2000u16);
    assert(0x20u8 as i8 == 0x20i8);
    assert(0xf0u8 as i8 == -0x10i8);
    assert(-0x40i8 as u8 == 0xc0u8);
}

These generate broadcasts that look like:

;; Broadcast scratch::clip_u8
(axiom (=>
  (fuel_bool fuel%scratch!clip_u8.)
  (forall ((i! Int)) (!
    (= (uClip 8 i!) (EucMod i! 256))
    :pattern ((uClip 8 i!))
))))

(I tried running what I could through assert-by-bit_vector on i: u128 before changing everything to i: int and using admit. Hopefully, I didn't make any mistakes.)