• David Swasey's avatar
    Heading toward an improved robust_safety. · 1fe7ecef
    David Swasey authored
    Simplified adv, defining it with ownL.
    Proof of concept for a friendly interface that (if it works) lets the user
    set up an invariant and prove view shifts and atomic triples for primitive
    reductions, rather than work in the model. (It should work, but I have to
    merge my two proofs to make sure.)
iris_unsafe.v 15.5 KB