Commit cc2708c6 authored by William Mansky's avatar William Mansky

Started LARA specs for kvnode.

parent b6afa51f
This diff is collapsed.
From iris.base_logic Require Import lib.invariants.
From iris.algebra Require Import list.
From gpfsl.logic Require Export lifting proofmode.
From gpfsl.gps Require Export surface protocols simpl_model.
From gpfsl.examples Require Export snapshot kvnode_helpers kvnode_code.
Implicit Types (L: gmap nat (list Z)) (γ: gname).
Canonical Structure histProtocol : protocolT :=
Build_protocolT (gmap nat Z) _ _ _ map_subseteq _.
Definition historyR := snapR (gmapUR nat (agreeR (listC ZC))).
Definition kvnodeN (n: loc) := nroot .@ "kvnodeN" .@ n.
Lemma to_agree_map_included L1 L2 :
to_agree <$> L1 to_agree <$> L2 L1 L2.
Proof.
move => /lookup_included => INCL i. move : (INCL i). rewrite 2!lookup_fmap.
destruct (L1 !! i) as [l1|] eqn:Eq1, (L2 !! i) as [l2|] eqn:Eq2; simpl; auto.
- by rewrite Some_included_total => /to_agree_included /leibniz_equiv_iff.
- rewrite option_included. naive_solver.
Qed.
(* The existing version of this requires A to be a cmra, which is completely unnecessary. *)
Global Instance gmap_unit {K} {E : EqDecision K} {C : Countable K} {A : ofeT} : Unit (gmap K A) := ( : gmap K A).
Section Interpretation.
Context `{!noprolG Σ,
histG : inG Σ historyR,
gpGv: !gpsG Σ natProtocol,
gpGd: !gpsG Σ histProtocol}.
Local Notation vProp := (vProp Σ).
(* TODO: it's not clear what is the order to instantiate dataP and versionP *)
Definition dataP (n: loc) γv : interpC Σ histProtocol :=
(λ _ _ _ _ s v, (z: Z) ver, v = #z log_latest s ver z t,
GPS_SWReader (Prtcl:=natProtocol) (n >> version) t
(ver - 1)%nat #(ver - 1)%nat γv)%I.
Definition hist_snapshot γh L : vProp :=
own γh (# (to_agree <$> L) : historyR)%I.
Definition hist_master q γh L : vProp :=
own γh (#{q} (to_agree <$> L) : historyR)%I.
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.
Context `{!gpsSimplG Σ (nat * list Z) Prtcl}.
(* added data-structure-level protocol assertion *)
Definition versionP (n: loc) γh γs γm : interpC Σ natProtocol :=
(λ _ _ γv _ s v, v = #(Z.of_nat s)
if even s then
( L vs, map_size L Nd log_latest L s vs
hist_snapshot γh L dataObs n L γs γv t st, sGPS_SWWriter t st (s, vs) γm)
else True)%I.
Definition versionPC : interpCasC Σ natProtocol := (λ _ _ _ _ _, True)%I.
Definition dataPC : interpCasC Σ histProtocol := (λ _ _ _ _ _, True)%I.
End Interpretation.
......@@ -19,7 +19,7 @@ Instance: Params (@master) 1.
Instance: Params (@snapshot) 1.
Notation "◯# a" := (Snap None a) (at level 15).
Notation "●#{ q } a" := (Snap (Some (q, to_agree a)) ε) (at level 15, format "●#{ q } a").
Notation "●#{ q } a" := (Snap (Some (q%Qp, to_agree a)) ε) (at level 15, format "●#{ q } a").
Notation "●# a" := (Snap (Some (1%Qp, to_agree a)) ε) (at level 15).
(* COFE *)
......
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