Commit 3af2e1f6 authored by William Mansky's avatar William Mansky

Can we prove this?

parent eb19a60c
......@@ -39,7 +39,7 @@ Section definitions.
((ver - 1)%nat, tsm) #(ver - 1)%nat γv)%I.
Global Instance dataP_persistent n γv b l tv s v :
Persistent (dataP n γv b l γv tv s v) := _.
Definition dataObs (n: loc) L γs γv:=
Definition dataObs (n: loc) L γs γv :=
([ list] i↦γi γs, ti vi,
GPS_iSP_Reader (kvnodeN n) (dataP n γv) (dataP n γv false)
(n >> data >> (Z.of_nat i)) ti (map_nth i L O) vi γi)%I.
......@@ -244,6 +244,7 @@ Qed.
End library_prots.
(* could quantify over gamma-v and gamma-s as well *)
Lemma kvnode_Readers_agree : forall n1 n2 t1 t2 s1 s2 v1 v2 E, N E ->
kvnode_prots_R n1 t1 s1 v1 - kvnode_prots_R n2 t2 s2 v2 ={E}= s1 s2 t1 t2 s2 s1 t2 t1.
Proof.
......@@ -254,6 +255,17 @@ Proof.
by iApply (sGPS_iSP_Readers_agree with "R1 R2").
Qed.
Lemma kvnode_Readers_agree' : forall n1 n2 t1 t2 s1 s2 v1 v2 E, N E -> s1 s2 ->
kvnode_prots_R n1 t1 s1 v1 - kvnode_prots_R n2 t2 s2 v2 ={E}=
kvnode_prots_R n1 t2 s2 v2.
Proof.
intros; unfold kvnode_prots_R.
iIntros "R1 R2".
iDestruct "R1" as (??) "(_ & _ & R1)".
iDestruct "R2" as (??) "(_ & _ & R2)".
by iApply (sGPS_iSP_Readers_agree with "R1 R2").
Qed.
(* kvnode_prots_W/R should be considered the "real" protocol assertions for kvnode,
and users should not use sGPS_iSP_Reader (since it doesn't include protocol assertions
on the component locations, which we're treating as "part of the write permission". *)
......
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