Trace visualizer

[feliperodri]

I'd love to have a way to see the trace (values for each variable) and walk it through step by step as I debug a proof. This would also help me to check coverage of a proof by telling me which branches I take or not.

[feliperodri]

Ideally, I’d like to see the value (from the counterexample) of a set of variables in a given context in the program.

So let’s say that I’m debugging the following program.

fn gcd(x: u64, y: u64) -> u64 {
    let mut x = x;
    let mut y = y;
    while y != 0 {
        let t = y;
        y = x % y;
        x = t;
    }
    x
}

fn foo(x: u64, y: u64, z: u64) {
    let coin : bool = kani::any();
    if coin {
        z = gcd(x,y);
    }
    assert!(!(gcd == 0) || (x == 0 && y == 0));
}

I want to see the value of t and x and y in every loop iteration without the noise of any out of context information (without the information of x and y outside the loop context.