Shrink the claim to a pure decision

The request and approval each carry a generation and an action hash. Admission returns true only when both fields match. The example uses bytes so the proof domain contains every pair of 8-bit values for each field.

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
struct Request {
    generation: u8,
    action_hash: u8,
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
struct Approval {
    generation: u8,
    action_hash: u8,
}

fn accepts(request: Request, approval: Approval) -> bool {
    request.generation == approval.generation && request.action_hash == approval.action_hash
}

#[cfg(kani)]
mod proofs {
    use super::{accepts, Approval, Request};

    #[kani::proof]
    pub fn accepted_receipt_matches_request() {
        let request = Request {
            generation: kani::any(),
            action_hash: kani::any(),
        };
        let approval = Approval {
            generation: kani::any(),
            action_hash: kani::any(),
        };

        if accepts(request, approval) {
            assert_eq!(request.generation, approval.generation);
            assert_eq!(request.action_hash, approval.action_hash);
        }
    }
}

Run the proof:

kani admission.rs

Kani reports one successfully verified harness. The harness asks: for every request and approval value, if accepts returns true, do the generation and action hash fields match? The proof covers corner values such as zero and 255 without writing one test per value.

Inject and read the failure

Temporarily remove the generation comparison from accepts. Run the proof again. Kani fails the proof and reports values that make the function accept while the generation assertion fails. Restore both comparisons before moving on.

The if accepts(...) block plays the role of a conditional proof. An equivalent harness could call kani::assume(accepts(...)) and then assert the field equalities. Assumptions narrow the proof domain. A mistaken assumption can make the domain empty, so a serious harness also needs a reachability or cover check when vacuity is plausible.

Name the proof boundary

The result proves a property of this compiled pure function for its modeled types. The result does not prove collision resistance of an 8-bit hash. The result does not prove that the UI displayed the same bytes, that a signature is authentic, that storage preserved the approval, or that concurrent code called the kernel with one coherent snapshot.

A production design can replace the byte with a cryptographic digest and keep the same equality law. Separate evidence must cover canonical serialization, signature verification, generation lifecycle, storage atomicity, and races. The next workshop addresses one local race.

Practice

1. Replace action_hash: u8 with two fields, tool and argument hash. Update the admission law.
2. Use kani::assume(request.generation > 0). State the values that leave the proof domain.
3. Name one temporal property that this pure harness cannot express naturally.

Worked answer

1. Admission must compare generation, tool, and argument hash. The proof asserts equality for all three fields after acceptance.
2. Every request with generation zero leaves the domain. The harness says nothing about those requests.
3. Example: an approval cannot be used after a later cancellation event. That claim depends on an event sequence and belongs in a state-machine model.

Lessons

• Kani checks Rust proof harnesses over symbolic values.
• A pure kernel creates a small proof surface near shipped code.
• Assumptions narrow the theorem and can create vacuity.
• Machine-word exhaustiveness does not verify the surrounding temporal protocol.
• Serialization, cryptography, storage, and concurrency need separate evidence.

References

1. Kani Project. “First Steps with Kani.” — proof harnesses, symbolic values, assumptions, and assertions.
2. Kani Project. “Using Kani.” — commands, harness selection, and verifier behavior.