RFC: Function stubbing

[aaronbembenek-aws]

This is a tracking issue for the RFC function_stubbing.

The goal is to allow users to specify that some functions should be replaced by mock functions (stubs) during verification. Although the current focus is on functions, the hope is that this mechanism might in the future be extended to other features (like methods and types).

The need for stubs is twofold:

1. Users might need to stub functions containing features that Kani does not support, such as inline assembly.
2. Users might need to stub functions containing code that Kani supports in principle, but which in practice leads to bad verification performance.

There are questions to resolve:

1. What should be the user experience? How and where should users specify which stubs to use?
2. Should stubs be applied consistently across all harnesses or should they be specific to a harness (i.e., different harnesses can use different stubs)?

[weaversa]

Would your stubbing support the following use-case?

Say I have (omitting unimportant bits):

fn F (...) -> ... {
   // Body for F, optimized algorithm
}

fn F'(...) -> ... {
  // Body for F', reference algorithm
}

and I prove w/ Kani that assert_eq!(F(x), F'(x)) for all x.

It should be safe to stub F' in for F, and vice verse anywhere else in the codebase I'd like to do proofs about.

So, say I also have

fn G (...) -> ... {
   // Body for G, optimized algorithm, calls F
}

fn G'(...) -> ... {
  // Body for G', reference algorithm, calls F'
}

Now I want to assert_eq!(G(x), G'(x)) for all x. I understand your stubbing mechanism will allow me to replace F with F' inside of the proof, which will speed up the proof because now G and G' both call F'. However, what if the definitions of F and F' are not consequential to the equivalence of G and G'? I imagine the proof then could be sped up even more by replacing both F and F' with return kani::any(), but we would also need a way to enforce that F and F' are equivalent -- both should return the same values when given the same input. That is, I believe your stubbing mechanism can be used to uninterpret F and F', but not set them equvialent (so called EUF). Is this possible?

A simpler example could involve wanting to uninterpret a single deterministic function that is called multiple times. Stubbing the definition to kani::any() is not quite equivalent to uninterpreting the function because we would also want to say that the function is deterministic (that every call to this function returns the same outputs on the same inputs).

[aaronbembenek-aws]

If I understand your use case correctly, you want to be able to say, "Here is a function f; given the same input, it should always return the same output; otherwise, we put no restrictions on its output." We are not currently planning to have explicit support for this (which I would describe as uninterpreted functions).

However, in some cases, it is possible to achieve this effect by lazily constructing the mapping for f in the function body and keeping track of it in a global variable:

lazy_static! {
    static ref MY_MAP: HashMap<u32, u32> = HashMap::new();
}

fn f(n: u32) -> u32 {
    unsafe { *MY_MAP.entry(n).or_insert_with(|| kani::any()) }
}

The trick would be using a data structure for the map that is verification friendly (so HashMap is not actually a good choice here).

[weaversa]

If I understand your use case correctly, you want to be able to say, "Here is a function f; given the same input, it should always return the same output; otherwise, we put no restrictions on its output." We are not currently planning to have explicit support for this (which I would describe as uninterpreted functions).

However, in some cases, it is possible to achieve this effect by lazily constructing the mapping for f in the function body and keeping track of it in a global variable:

lazy_static! {
    static ref MY_MAP: HashMap<u32, u32> = HashMap::new();
}

fn f(n: u32) -> u32 {
    unsafe { *MY_MAP.entry(n).or_insert_with(|| kani::any()) }
}

The trick would be using a data structure for the map that is verification friendly (so HashMap is not actually a good choice here).

Thanks @aaronbembenek-aws for your response. As a developer interested in assurance, I'm familiar with standard assurance tools such as SAT/SMT, uninterpreted functions, proof reuse, rewriting, and so on. If there are tricks for emulating these tools using Kani, it would be nice, from a user perspective, for Kani to transparently provide them.

As well, I'm trying to understand, in a formal way, what the function stubbing technique accomplishes. It seems like stubbing is equivalent to uninterpreting a function and then adding preconditions that constrain the function's output (which may be quite specific) inside a property. Why take a narrow approach here when you could instead implement standard assurance tools (uninterpreted functions w/ equality and pre/post conditions) and gain much more?

[danielsn]

CBMC actually supports uninterpreted functions: we probably should too http://www.cprover.org/cprover-manual/modeling/nondeterminism/

[weaversa]

CBMC actually supports uninterpreted functions: we probably should too http://www.cprover.org/cprover-manual/modeling/nondeterminism/

If Kani supported uninterpreted functions, could the example in the RFC be reworked to something like this?

#[cfg(kani)]
fn mock_random<T: kani::Arbitrary>() -> T {
    kani::any()
}

#[cfg(kani)]
#[kani::proof]
#[kani::uninterpret(rand::random)]
fn random_cannot_be_zero() {
    kani::assume(rand::random::<u32>() == mock_random<u32>());
    assert_ne!(rand::random::<u32>(), 0);
}  // This should fail

Maybe at that point one could do away with mock_random and add preconditions to avoid bad behavior, like:

#[cfg(kani)]
#[kani::proof]
#[kani::uninterpret(rand::random)]
fn random_cannot_be_zero() {
    kani::assume(rand::random::<u32>() != 0);
    assert_ne!(rand::random::<u32>(), 0);
}  // This should succeed

[aaronbembenek-aws]

If Kani supported uninterpreted functions, could the example in the RFC be reworked to something like this?

Yes, I believe these examples would work, and I agree you can do away with mock_random in that case. In general, I suspect that people would not want to make rand::random uninterpreted, since doing so would mean that every invocation returns the same value, when typically we'd expect this assertion to fail:

assert_eq!(rand::random::<u32>(), rand::random::<u32>()); // never fails if rand::random is uninterpreted

If there are tricks for emulating these tools using Kani, it would be nice, from a user perspective, for Kani to transparently provide them.

Agreed -- stubs are relatively low-level, and it would be good to provide higher-level verification abstractions. We've started compiling a list here of different types of stubs we might want to automatically support.

It seems like stubbing is equivalent to uninterpreting a function and then adding preconditions that constrain the function's output (which may be quite specific) inside a property. Why take a narrow approach here when you could instead implement standard assurance tools (uninterpreted functions w/ equality and pre/post conditions) and gain much more?

Stubbing is more general than uninterpreted functions, since we can simulate uninterpreted functions using stubbing, but there are stubs that cannot be faithfully captured as uninterpreted functions (e.g., if the stub can return different outputs for the same input). It is also possible to give stubs pre- and postconditions. Granted, these pre- and postconditions are written in Rust. This has some potential advantages over using a custom constraint DSL (as is often used with function contracts): it's not necessary for users to learn a new syntax, and Rust code naturally captures some information that might have to be given explicitly in a logical constraint (like which memory is written). Of course, there might also be times when using logical constraints is more convenient.

[weaversa]

In general, I suspect that people would not want to make rand::random uninterpreted, since doing so would mean that every invocation returns the same value

You're right. I chose a poor example here :-)

Stubbing is more general than uninterpreted functions

The info in the CBMC link was pretty helpful. To sum up -- a stub is nondeterministic ("separate calls to the function can return different results, even for the same inputs"), whereas uninterpreting is deterministic ("different invocations will return the same value if their inputs are the same"). A stub can be made deterministic by using memoization, though it would be best if Kani supported this natively, rather than a user having to determine how to best memoize.

As well, I'm perfectly happy writing pre- and postconditions in Rust where it makes sense.

This capability seems like a first step towards rewriting (now only at a function boundary, I think, am I wrong here?), which is nice to see.

[aaronbembenek-aws]

This capability seems like a first step towards rewriting (now only at a function boundary, I think, am I wrong here?), which is nice to see.

Right - it'd enable rewriting only at the unit of entire functions/methods.