Allow successful verification with unimplemented code path

[CharlyCst]

Hi,

We are working on integrating Kani in a project where we want to prove the equivalence between our implementation and a reference specification. We are interested in proving correctness, but not necessarily completeness.
For that purpose we would like to able to terminate the verification successfully when some code path are reached, but todo!s and unimplemented!s cause Kani to fail. Does Kani provide an equivalent macro which would cause a panic! without Kani but doesn't cause the verification to fail?

To provide more context, the project in question is a RISC-V firmware that exposes a virtual M-mode. We translated the official RISC-V specification from Sail to Rust so we have two RISC-V emulators: one from our project, and one extracted from the official spec. We use Kani to show that executing an instruction with both emulators result in the same state and thus that our RISC-V emulation is correct.
We are not interested in implementing the full spec (which is a moving target), but we want to prove that the subset we implement is correct.

[zhassan-aws]

Hi @CharlyCst. Would it be possible to constrain the inputs to avoid the panic condition? Example:

let input1 = kani::any();
let input2 = kani::any();
...
kani::assume(satisfies_implemented_subset(input1, input2, ...));
spec_function(input1, input2, ...);
impl_function(input1, input2, ...);

where satisfies_implemented_subset is a predicate that returns true if the input values are within the subset that is implemented.

[zhassan-aws]

I see. The other possibility is to define your own macro that behaves differently depending on cfg(kani), e.g. something along the lines of:

macro_rules! non_kani_panic {
    ($($arg:tt)*) => {
        #[cfg(kani)] {}
        #[cfg(not(kani))] panic!($($arg)*)
    };
}

For example, using it in the following program:

#[cfg_attr(kani, kani::proof)]
fn main() {
    non_kani_panic!("panic");
}

it panics when run using cargo run:

 $ cargo run
   Compiling disc-3746 v0.1.0 (/home/ubuntu/examples/disc-3746)
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.09s
     Running `target/debug/disc-3746`
thread 'main' panicked at src/main.rs:10:5:
panic
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

but verification succeeds with Kani:

$ cargo kani
Kani Rust Verifier 0.56.0 (cargo plugin)
   Compiling disc-3746 v0.1.0 (/home/ubuntu/examples/disc-3746)
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.08s
Checking harness main...
...
VERIFICATION:- SUCCESSFUL
Verification Time: 0.021776784s

Complete - 1 successfully verified harnesses, 0 failures, 1 total.

[zhassan-aws]

Or:

macro_rules! non_kani_panic {
    ($($arg:tt)*) => {
        if !cfg!(kani) {
            panic!($($arg)*)
        }
    };
}

[CharlyCst]

Yes ideally we would like something like this, but we can't just do nothing with #[cfg(kani)] as the reference implementation will modify the state, and Kani will then detect a divergence (rightfully so).

Here is a toy example of the situation we are facing:

macro_rules! non_kani_panic {
   ($($arg:tt)*) => {
        if !cfg!(kani) {
            panic!($($arg)*)
        }
    };
}

#[derive(Debug, Clone, PartialEq, Eq)]
struct State {
    reg: usize,
}

#[derive(Clone, Copy)]
enum Instr {
    AddOne,
    AddTwo,
    Unknown,
}

fn decode(instr: u32) -> Instr {
    match instr {
        1 => Instr::AddOne,
        2 => Instr::AddTwo,
        _ => Instr::Unknown,
    }
}

// Our implementation
fn interpreter_impl(instr: u32, state: &mut State) {
    match decode(instr) {
        Instr::AddOne => state.reg = state.reg.wrapping_add(1),
        Instr::AddTwo => {
            // Here we do not want/can't implement the function, but would like
            // verification to succeed anyway.
            non_kani_panic!(); // <--- We don't have an implementation here, but we still want to check all the other branches.
        }
        Instr::Unknown => (),
    }
}

// Automatically generated from a spec
fn interpreter_ref(instr: u32, state: &mut State) {
    match decode(instr) {
        Instr::AddOne => state.reg = state.reg.wrapping_add(1),
        Instr::AddTwo => state.reg = state.reg.wrapping_add(2),
        Instr::Unknown => (),
    }
}

#[kani::proof]
fn check() {
    use kani;

    // Initialize symbolic state and instruction
    let instr: u32 = kani::any();
    let mut state_impl = State { reg: kani::any() };
    let mut state_ref = state_impl.clone();

    // Execute the instruction in both the implementation and the reference
    interpreter_impl(instr, &mut state_impl);
    interpreter_ref(instr, &mut state_ref);

    // Check that the implementation coincide with the spec
    assert_eq!(state_impl, state_ref);
}

The verification will fail because the behavior diverge in the Instr::AddTwo branch, but ideally we would like to be able to still verify the other branches.

Maybe our use-case is a bit too uncommon, but I was wondering if there was a way to achieve this with kani.

[zhassan-aws]

A branch/execution path can be blocked using kani::assume(false). So you can update the macro to be:

macro_rules! non_kani_panic {
   ($($arg:tt)*) => {
        if cfg!(kani) {
            kani::assume(false);
        } else {
            panic!($($arg)*)
        }
    };
}

One needs to be careful with assume(false) though because it may lead to vacuous proofs.

[CharlyCst]

Awesome, that looks like I was looking for, thanks a lot!

When you say that assume(false) can lead to vacuous proofs, is there anything we should be careful about assuming we only use it through the above macro? In particular can this "leak" to other execution paths under some conditions?

[zhassan-aws]

No, they cannot leak to other execution paths. If it's only used through the macro, you should be good.

[CharlyCst]

Awesome, thanks a lot 🙂