AWS-Team-4 Modify and add documentation to run kani on proofs in the library

[QinyuanWu]

This PR adds to the documentation in the Verification Tools->Kani section of the challenge book.

Changes

• Step 1: add clarify on where to put the example code.
• Step 2: add -Z mem-predicate to avoid unstable feature errors.
• Step 4: new step to help kani user run specific proofs and identify harness fullnames.

❗ Issue

I tried to follow step 1 & 2 but kani could not find the harnesses in the example code. At this point there are many proofs in the library so I couldn't find the fullname of the harness in the example code by just running all proofs. I tried to move example.rs into library/core/src/ptr/ and use --harness ptr::verify::example or --harness dummy_proof but both got error: no harnesses matched the harness filter. Please let me know if you are successful or running into the same issue.

[danielhumanmod]

LGTM

[tautschnig]

Thank you for your contribution!

❗ Issue

I tried to follow step 1 & 2 but kani could not find the harnesses in the example code. At this point there are many proofs in the library so I couldn't find the fullname of the harness in the example code by just running all proofs. I tried to move example.rs into library/core/src/ptr/ and use --harness ptr::verify::example or --harness dummy_proof but both got error: no harnesses matched the harness filter. Please let me know if you are successful or running into the same issue.

Is this still true despite the "Step 4" that you added?

[QinyuanWu]

Thank you for your contribution!

❗ Issue

I tried to follow step 1 & 2 but kani could not find the harnesses in the example code. At this point there are many proofs in the library so I couldn't find the fullname of the harness in the example code by just running all proofs. I tried to move example.rs into library/core/src/ptr/ and use --harness ptr::verify::example or --harness dummy_proof but both got error: no harnesses matched the harness filter. Please let me know if you are successful or running into the same issue.

Is this still true despite the "Step 4" that you added?

@tautschnig Yes I get the same error message with this command. --harness works for other existing proof harnesses however, such as --harness ptr::unique::verify for all proofs in unique.rs.

[jaisnan]

Thank you for your contribution!

❗ Issue

I tried to follow step 1 & 2 but kani could not find the harnesses in the example code. At this point there are many proofs in the library so I couldn't find the fullname of the harness in the example code by just running all proofs. I tried to move example.rs into library/core/src/ptr/ and use --harness ptr::verify::example or --harness dummy_proof but both got error: no harnesses matched the harness filter. Please let me know if you are successful or running into the same issue.

Is this still true despite the "Step 4" that you added?

@tautschnig Yes I get the same error message with this command. --harness works for other existing proof harnesses however, such as --harness ptr::unique::verify for all proofs in unique.rs.

This might be because --harness and --harness --exact are for individual harnesses and exact harnesses. --harnesses can be used with prefixes, buts it does not verify all harness in a module if you specify it. This is very much an active design choice. If you'd like to change that to recognize all harness in a file or module, you can file a feature request on the kani page :)

Can you specify which exact harness you want to verify as opposed to stopping at the module, and see if that fixes the error? We can clarify that in the documentation.

[QinyuanWu]

@jaisnan I could not get Kani to locate any proofs in example.rs. If it works for you, could you please tell me where did you put example.rs(which is the sample code in the tutorial) and the complete command you used to locate and verify these proofs?

[jaisnan]

@jaisnan I could not get Kani to locate any proofs in example.rs. If it works for you, could you please tell me where did you put example.rs(which is the sample code in the tutorial) and the complete command you used to locate and verify these proofs?

I did not put these proofs in a new file no, I think the documentation should make it clear that you should try it out by putting the proofs inside an existing file like library/std/src/lib.rs. The starter code is outdated too, since we are now asking users to fork our repo with Kani already initiated in it, and not a fresh copy of the std library. The last section contains some

@QinyuanWu I've issued a PR that makes changes that should clarify the introduction and the --harness command. Once that's merged, you can still add your "step 4" section on top of my changes. Does that work for you?