Commit 831a56f3 authored by Paul's avatar Paul
Browse files

fix spinlock_proof.v

parent 86d9bb5f
Pipeline #52843 passed with stage
in 17 minutes and 38 seconds
......@@ -84,7 +84,7 @@ Section proofs.
- (* #1 First loop (after the initial run), checking if we got the ticket. *)
destruct s.
+ repeat liRStep; liShow. iIntros "Hb".
repeat liRStep; liShow. 2: { destruct b => //. iFrame. }
repeat liRStep; liShow.
iDestruct select (hyp_spinlock_t_invariant _ _ _) as (owner next) "([%%]&?&?&?&?&?&?)".
repeat liRStep; liShow.
liInst Hevar next.
......@@ -93,7 +93,7 @@ Section proofs.
liInst Hevar owner. liInst Hevar0 next.
repeat liRStep; liShow.
+ repeat liRStep; liShow. iIntros "Hb".
repeat liRStep; liShow. 2: { destruct b => //. iFrame. }
repeat liRStep; liShow.
iExists (Shr, tytrue); iSplitR; first by simpl.
iDestruct select (inv _ _) as "#Hinv".
iInv "Hinv" as ">Inv".
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment