Add verifier::shadow_data

[Chris-Hawblitzel]

This adds tracking of shadow data associated with exec function parameters, return values, and local variables. This is useful when the SMT encoding of these values omits some data that is irrelevant to ordinary Verus verification but that may be useful to lower-level code. In particular, while the SMT encoding of a shared reference &t is just the SMT encoding of t, with no underlying pointer information, the shadow data for a &t parameter, return value, or local variable can contain the extra pointer information.

To opt into this feature, a function uses the attribute #[verifier::shadow_data]. This creates extra shadow variables in the SST/AIR/SMT representation of that function. Non-shadow_data functions that call shadow_data functions pass in uninterpreted shadow data for parameters and ignore shadow data for return values. Likewise, when a shadow_data function calls a non-shadow_data function, the parameter shadow data is ignored and the return shadow data is uninterpreted.

In general, each parameter, return value, and local variable x of type t gets shadow data shadow_data(x) of the entirely abstract type ShadowData<t>. For example:

#[verifier::shadow_data]
fn ident(x: &u64) -> (r: &u64)
    ensures shadow_data(r) == shadow_data(x)
{
    x
}

#[verifier::shadow_data]
fn test_ident1(x: &u64, y: &u64) {
    let xx = ident(x);
    let yy = ident(y);
    assert(shadow_data(xx) == shadow_data(x));
    assert(shadow_data(yy) == shadow_data(y));
}

fn test_ident2(x: &u64, y: &u64) {
    let xx = ident(x);
    let yy = ident(y);
}

The shadow data feature is independent of any particular types -- it is not specialized in any way to &t types. To use shadow data to get pointer information in &t types, you can declare an uninterp spec function that extracts pointer information from the type ShadowData<&T> for all T.

You can just as easily have shadow data for values of types other than &t, like Option<&t> or (&t, &t). To use shadow data inside an Option, for example, you could do the following:

uninterp spec fn option_some_shadow_data<T>(s: ShadowData<T>) -> ShadowData<Option<T>>;
uninterp spec fn option_unwrap_shadow_data<T>(s: ShadowData<Option<T>>) -> ShadowData<T>;

#[verifier::shadow_data]
#[verifier::external_body]
fn option_some_with_shadow<T>(x: T) -> (r: Option<T>)
    ensures
        r == Some(x),
        shadow_data(r) == option_some_shadow_data(shadow_data(x)),
        // TODO: this should be a separate axiom:
        shadow_data(x) == option_unwrap_shadow_data(option_some_shadow_data(shadow_data(x))),
{
    Some(x)
}

#[verifier::shadow_data]
#[verifier::external_body]
fn option_unwrap_with_shadow<T>(x: Option<T>) -> (r: T)
    requires
        x.is_some(),
    ensures
        r == x.unwrap(),
        shadow_data(r) == option_unwrap_shadow_data(shadow_data(x)),
{
    x.unwrap()
}

#[verifier::shadow_data]
fn test_option(x: &u64) {
    let o = option_some_with_shadow(x);
    let y = option_unwrap_with_shadow(o);
    assert(shadow_data(y) == shadow_data(x));
}

The implementation of shadow data builds on #2560 , using extra SST parameters and return values to represent the shadow data values. For now, the call_requires and call_ensures axioms are disabled for any functions marked #[verifier::shadow_data]. Within a function, tracking of shadow data is currently very conservative: direct local variable assignment, function call arguments, and function call return values are tracked precisely, but all other operations generate uninterpreted shadow data.

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