• 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.)
    1fe7ecef
Name
Last commit
Last update
lib/ModuRes Loading commit data...
.dir-locals.el Loading commit data...
.gitignore Loading commit data...
Makefile Loading commit data...
README.txt Loading commit data...
configure Loading commit data...
core_lang.v Loading commit data...
iris_core.v Loading commit data...
iris_meta.v Loading commit data...
iris_unsafe.v Loading commit data...
iris_vs.v Loading commit data...
iris_wp.v Loading commit data...
lang.v Loading commit data...
masks.v Loading commit data...
world_prop.v Loading commit data...