program_logic · da0246959370faab004ce1cc8b7e88a2753c3d99 · Simcha van Collem / Iris

Forked from Iris / Iris

6629 commits behind the upstream repository.

Prove another lemma to open invariants that we only know by namespace.

Ralf Jung authored 8 years ago

The good news is, this one works without FSAs, and it can be applied around the "view shift with a step"-thing.
Furthermore, the FSA lemma can be derived from the new one.
The bad news is, the FSA lemma proof doesn't even get shorter in doing this change.

da024695

History

da024695 8 years ago

History

Name	Last commit	Last update
..
adequacy.v
auth.v
ectx_language.v
ectx_lifting.v
ectxi_language.v
ghost_ownership.v
global_functor.v
hoare.v
hoare_lifting.v
invariants.v
language.v
lifting.v
model.v
namespaces.v
ownership.v
pviewshifts.v
resources.v
saved_one_shot.v
saved_prop.v
sts.v
viewshifts.v
weakestpre.v
weakestpre_fix.v
wsat.v