No clear CEC functionality or cached operation

[TomMD]

I'm looking for some sort of CEC (like ABC's) and caching behavior to make CI PR runs cheap.

Should I dig and write documentation as I discover or are these features simply not there at present?

[TomMD]

Related to the CEC ask, long ago I used CEC and SAW to prove C code was equivalent before and after a change. This was possible because I could mangle the symbols after LLVM IR generation completed for compilation of each artifact pre and post compilation. Kani's use of Rust's MIR means the same solution isn't useable, but notionally there isn't much difference. Do you see obvious issues with using Kani to a similar end?

[zhassan-aws]

Hi @TomMD. Kani can be used for verifying the equivalence of two Rust functions. For example if you functions f1 and f2 that take, say an i32 and a char and return a bool:

fn f1(i: i32, c: char) -> bool

then you can write a harness to check their equivalence:

#[kani::proof]
fn check_f1_f2_equiv() {
    let i: i32 = kani::any();
    let c: char = kani::any();
    let b1 = f1(i, c);
    let b2 = f2(i, c);
    assert_eq!(b1, b2);
}

If the assertion passes, then f1 and f2 produce the same output value for all inputs.

Is this what you're looking for?

Regarding caching, if the source files didn't change, Kani won't recompile them. Perhaps saving the build artifacts across CI runs could help with the runtime?

[TomMD]

The caching is good to know about, thanks.

As for lack of CEC in particular, yes we can get functional equivalence in another way but it is slower for many interesting cases. IIRC (and I might not), it was CEC that could reasonably prove the new and old libsodium SHA512 function's equivalent while naive SAT embedding could not in a timely manner. It seems there is no support for ABC and thus the answer is 'no' in this case. Thanks.