Create macro to generate harnesses for contract

[celinval]

Requested feature: Add a macro gen_proof_for_contract.
Use case: Contact harnesses are usually trivial and repetitive. Add a macro to go the work for now.
Link to relevant documentation (Rust reference, Nomicon, RFC):

Instead of:

#[kani::proof_for_contract(target_fn)]
fn check_target_fn() {
    let _ = target_fn(kani::any(), kani::any());
}

Maybe we can at least provide a macro:

kani::gen_proof_for_contract!(target_fn, args=2);

The macro should also support specifying instantiation parameters, fn safety, and extra harness attributes.

[tautschnig]

Could that perhaps be an attribute place on a function so that we have target_fn as well as its signature readily available? Would then only require the desired name of the harness (I think that name is important as otherwise users don't know how to specifically target that harness).

[celinval]

I thought about it, but I have mixed feelings about it. On the one hand, it is nice to keep it local, on the other hand, this can increase the number of annotations in the function and there is no separation of concerns.

Note that in that case, the code would be expanded as a harness inside the target function or at least inside the module where the function is defined. This would also make further harness configuration pollute the function preamble.

I think the macro is a good compromise for now until we figure out a more permanent / stable mechanism to auto-generate harnesses.

Regarding the function name, I'm OK with either adding a prefix / suffix to the function name or just adding it as an extra argument to the macro.

What do you think?

[tautschnig]

I thought about it, but I have mixed feelings about it. On the one hand, it is nice to keep it local, on the other hand, this can increase the number of annotations in the function and there is no separation of concerns.

Note that in that case, the code would be expanded as a harness inside the target function or at least inside the module where the function is defined. This would also make further harness configuration pollute the function preamble.

I understand and share those concerns.

I think the macro is a good compromise for now until we figure out a more permanent / stable mechanism to auto-generate harnesses.

What about having a Kani command-line argument instead of the macro? This would avoid polluting the source code, yet the implementation would likely be very similar to the macro (either way we'd have to look up the function name).

Regarding the function name, I'm OK with either adding a prefix / suffix to the function name or just adding it as an extra argument to the macro.

What do you think?

Whatever we build will be an improvement over the current state. The only reason I'm trying to argue in favour of those slightly different approaches is that I'd like to reduce cluttering the source code as much as possible, so my personal order of preference is command-line argument over attribute over macro.

[celinval]

Interesting... command line is my least favorite. 😆 The reason being that it's easier to forget, and harder to maintain.

I agree with you though that an annotation is the best solution. In the long run, I would like Kani to automatically verify all contracts if finds except those marked with #[kani::skip_contract] or via command line option. This solution would require way more engineering though, and I don't think we currently have the bandwidth for that.

I think the macro is a good stopgap. It doesn't change the current user flow, it reduce a lot of the verbosity of our harnesses, and it will work with concrete playback, with extra harness configurations without any extra work.

[celinval]

Ok... I gave this an extra thought. I think you are right, and we shouldn't bother adding this solution to our library. Maybe we can add this quick and dirty work around to the verify-rust-std repository, and we can spend time adding the correct solution to Kani.

If that's OK for you, I'll create a PR on the other repository, close this issue and create a new one for auto-verification of contracts.