From 5f082742d60df73e1a3f3e4fb7441a05cc8e6e1c Mon Sep 17 00:00:00 2001
From: dsac <arnaud@dabyseesaram.info>
Date: Sun, 14 Aug 2022 18:55:23 +0200
Subject: [PATCH] Instantiation and setup for the user (1 admit remains)
---
aneris/examples/crdt/statelib/STS/gst.v | 11 ++
aneris/examples/crdt/statelib/STS/lst.v | 8 +
.../crdt/statelib/proof/internal_specs.v | 55 +++++++
aneris/examples/crdt/statelib/proof/spec.v | 56 ++++---
.../crdt/statelib/proof/stlib_proof.v | 71 +-------
.../crdt/statelib/proof/stlib_proof_setup.v | 152 ++++++++++++++++++
.../crdt/statelib/resources/resources_inv.v | 11 +-
.../statelib/resources/resources_update.v | 2 +-
.../crdt/statelib/user_model/params.v | 4 +-
9 files changed, 267 insertions(+), 103 deletions(-)
create mode 100644 aneris/examples/crdt/statelib/proof/stlib_proof_setup.v
diff --git a/aneris/examples/crdt/statelib/STS/gst.v b/aneris/examples/crdt/statelib/STS/gst.v
index 08a840d..f5821ce 100644
--- a/aneris/examples/crdt/statelib/STS/gst.v
+++ b/aneris/examples/crdt/statelib/STS/gst.v
@@ -122,4 +122,15 @@ Section Gst_helper.
by apply gst_valid_inclusion with f.
Qed.
+ Lemma gst_init_valid:
+ Gst_Validity ((∅, vreplicate (length CRDT_Addresses) ∅): Gst Op).
+ Proof.
+ split; [ | | apply lst_init_valid | ].
+ - intros x. split; first by intros?.
+ intros[??].
+ by rewrite vlookup_replicate in H0.
+ - intros x. by intros?.
+ - intros ?; rewrite vlookup_replicate. apply lst_init_valid.
+ Qed.
+
End Gst_helper.
diff --git a/aneris/examples/crdt/statelib/STS/lst.v b/aneris/examples/crdt/statelib/STS/lst.v
index 01398fc..3fbde7d 100644
--- a/aneris/examples/crdt/statelib/STS/lst.v
+++ b/aneris/examples/crdt/statelib/STS/lst.v
@@ -74,4 +74,12 @@ Section Lst_helper.
Lemma Lst_Validity_implies_same_orig_comparable (s: Lst Op):
Lst_Validity s → event_set_same_orig_comparable s.
Proof. by intros []. Qed.
+
+
+ Lemma lst_init_valid:
+ Lst_Validity (∅: Lst Op).
+ Proof.
+ split; try done.
+ intros??. by left.
+ Qed.
End Lst_helper.
diff --git a/aneris/examples/crdt/statelib/proof/internal_specs.v b/aneris/examples/crdt/statelib/proof/internal_specs.v
index 1a406d6..1302788 100644
--- a/aneris/examples/crdt/statelib/proof/internal_specs.v
+++ b/aneris/examples/crdt/statelib/proof/internal_specs.v
@@ -29,6 +29,35 @@ From aneris.examples.crdt.statelib.proof
Instance timeinst : Log_Time := timestamp_time.
+
+
+Section SpecsPremiminary.
+
+ Context `{LogOp: Type, LogSt : Type,
+ !anerisG Mdl Σ, !EqDecision LogOp, !Countable LogOp,
+ !CRDT_Params, !Lattice LogSt, !StLib_Params LogOp LogSt,
+ !Internal_StLibG LogOp Σ, !StLib_GhostNames,
+ st_deser: val, stser: serialization}.
+
+ Notation princ_ev := (@principal (gset (Event LogOp)) cc_subseteq).
+
+ Definition locstate_tok i : iProp Σ :=
+ own (γ_loc_own !!! i) ((1/3)%Qp, to_agree ∅) ∗
+ own (γ_loc_sub !!! i) ((2/3)%Qp, to_agree ∅) ∗
+ own (γ_loc_cc !!! i) (◯ (princ_ev ∅)).
+
+ Definition lockinv_tok i : iProp Σ :=
+ own (γ_loc_own !!! i) ((1/3)%Qp, to_agree ∅) ∗
+ own (γ_loc_for !!! i) ((1/2)%Qp, to_agree ∅).
+
+ Definition stlib_init_token `{!StLib_GhostNames} i : iProp Σ :=
+ locstate_tok i ∗
+ lockinv_tok i.
+
+End SpecsPremiminary.
+
+
+
Section StateLib_InternalSpecs.
Context `{LogOp: Type, LogSt : Type,
@@ -90,5 +119,31 @@ Section StateLib_InternalSpecs.
{{{ RET #(); True }}}.
+ Definition internal_init_spec : iProp Σ :=
+ ∀ (repId : fRepId) addr fixed_addrs addrs_val crdt_val,
+ {{{ ⌜is_list CRDT_Addresses addrs_val⌠∗
+ ⌜CRDT_Addresses !! (fin_to_nat repId) = Some addr⌠∗
+ ⌜addr ∈ fixed_addrs⌠∗
+ fixed fixed_addrs ∗
+ ([∗ list] z ∈ CRDT_Addresses, z ⤇ socket_proto) ∗
+ addr ⤳ (∅, ∅) ∗
+ free_ports (ip_of_address addr) {[port_of_address addr]} ∗
+ (*locstate_tok repId ∗
+ lockinv_tok repId ∗*)
+ stlib_init_token repId ∗
+ crdt_fun_spec crdt_val
+ }}}
+ statelib_init StLib_StSerialization.(s_serializer).(s_ser)
+ StLib_StSerialization.(s_serializer).(s_deser)
+ addrs_val
+ #repId
+ crdt_val @[ip_of_address addr]
+ {{{ gs_val upd_val, RET (gs_val, upd_val);
+ StLib_OwnLocalState repId ∅ ∅ ∗
+ internal_get_state_spec gs_val repId addr ∗
+ internal_update_spec upd_val repId addr
+ }}}.
+
+
End StateLib_InternalSpecs.
diff --git a/aneris/examples/crdt/statelib/proof/spec.v b/aneris/examples/crdt/statelib/proof/spec.v
index f7dbf8c..ddbf9cd 100644
--- a/aneris/examples/crdt/statelib/proof/spec.v
+++ b/aneris/examples/crdt/statelib/proof/spec.v
@@ -118,44 +118,46 @@ Section Specification.
crdt_fun #() @[ip_of_address addr]
{{{ v, RET v; crdt_triplet_spec v }}}.
- Definition init_spec_for_specific_crdt (init : val) : iProp Σ :=
- ∀ (repId : nat) (addr : socket_address) (fixedAddrs : gset socket_address)
- (addrs_val : val),
- {{{ ⌜is_list CRDT_Addresses addrs_val⌠∗
- ⌜CRDT_Addresses !! repId = Some addr⌠∗
- ⌜addr ∈ fixedAddrs⌠∗
- fixed fixedAddrs ∗
- ([∗ list] i ↦ z ∈ CRDT_Addresses, z ⤇ StLib_SocketProto i) ∗
- addr ⤳ (∅, ∅) ∗
- free_ports (ip_of_address addr) {[port_of_address addr]} ∗
- StLib_InitToken repId
- }}}
- init addrs_val #repId @[ip_of_address addr]
- {{{ get_state_val mutator_val, RET (get_state_val, mutator_val);
- LocState repId ∅ ∅ ∗
- get_state_spec get_state_val repId addr (*∗
- ** TODO: mutator_spec mutator_val addr*)
- }}}.
-
+ (** TODO: discuss the differences.
Definition init_spec (init : val) : iProp Σ :=
∀ (repId : nat) (addr : socket_address) (fixedAddrs : gset socket_address)
- (addrs_val crdt_val : val),
+ (addrs_val crdt_val : val) (f: (repId < length CRDT_Addresses)%nat),
{{{ ⌜is_list CRDT_Addresses addrs_val⌠∗
⌜CRDT_Addresses !! repId = Some addr⌠∗
⌜addr ∈ fixedAddrs⌠∗
fixed fixedAddrs ∗
- ([∗ list] i ↦ z ∈ CRDT_Addresses, z ⤇ StLib_SocketProto i) ∗
+ ([∗ list] i ↦ z ∈ CRDT_Addresses, z ⤇ StLib_SocketProto) ∗
addr ⤳ (∅, ∅) ∗
free_ports (ip_of_address addr) {[port_of_address addr]} ∗
- StLib_InitToken repId ∗
+ StLib_InitToken (nat_to_fin f) ∗
crdt_fun_spec crdt_val
}}}
init addrs_val #repId crdt_val @[ip_of_address addr]
{{{ get_state_val mutator_val, RET (get_state_val, mutator_val);
LocState repId ∅ ∅ ∗
- get_state_spec get_state_val repId addr (*∗
- TODO: mutator_spec mutator_val repId addr*)
- }}}.
+ get_state_spec get_state_val repId addr ∗
+ update_spec mutator_val repId addr
+ }}}. *)
+
+ Definition init_spec (init: val) : iProp Σ :=
+ ∀ (repId : (fin(length CRDT_Addresses))) (addr : socket_address)
+ (fixedAddrs : gset socket_address) (addrs_val crdt_val : val),
+ {{{ ⌜is_list CRDT_Addresses addrs_val⌠∗
+ ⌜CRDT_Addresses !! (fin_to_nat repId) = Some addr⌠∗
+ ⌜addr ∈ fixedAddrs⌠∗
+ fixed fixedAddrs ∗
+ ([∗ list] z ∈ CRDT_Addresses, z ⤇ StLib_SocketProto) ∗
+ addr ⤳ (∅, ∅) ∗
+ free_ports (ip_of_address addr) {[port_of_address addr]} ∗
+ StLib_InitToken repId ∗
+ crdt_fun_spec crdt_val
+ }}}
+ init #repId crdt_val @[ip_of_address addr]
+ {{{ gs_val upd_val, RET (gs_val, upd_val);
+ LocState repId ∅ ∅ ∗
+ get_state_spec gs_val repId addr ∗
+ update_spec upd_val repId addr
+ }}}.
End Specification.
@@ -173,7 +175,9 @@ Section StLibSetup.
True ⊢ |={E}=> ∃ (Res : StLib_Res LogOp),
GlobInv ∗
GlobState ∅ ∗
- ([∗ list] i ↦ _ ∈ CRDT_Addresses, StLib_InitToken i) ∗
+ (∃ (S: gset (fin (length CRDT_Addresses))),
+ (∀ i, ⌜i ∈ SâŒ) ∗
+ [∗ set] i ∈ S, StLib_InitToken i) ∗
init_spec init.
End StLibSetup.
diff --git a/aneris/examples/crdt/statelib/proof/stlib_proof.v b/aneris/examples/crdt/statelib/proof/stlib_proof.v
index 113152c..77ed04c 100644
--- a/aneris/examples/crdt/statelib/proof/stlib_proof.v
+++ b/aneris/examples/crdt/statelib/proof/stlib_proof.v
@@ -755,45 +755,12 @@ Section StateLib_Proof.
(** +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+
| Speficication of [statelib_init] |
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+ **)
- Definition locstate_tok i : iProp Σ :=
- own (γ_loc_own !!! i) ((1/3)%Qp, to_agree ∅) ∗
- own (γ_loc_sub !!! i) ((2/3)%Qp, to_agree ∅) ∗
- own (γ_loc_cc !!! i) (◯ (princ_ev ∅)).
-
- Definition lockinv_tok i : iProp Σ :=
- own (γ_loc_own !!! i) ((1/3)%Qp, to_agree ∅) ∗
- own (γ_loc_for !!! i) ((1/2)%Qp, to_agree ∅).
-
- Definition internal_init_spec : iProp Σ :=
- ∀ (repId : fRepId) addr fixed_addrs addrs_val crdt_val,
- {{{ ⌜is_list CRDT_Addresses addrs_val⌠∗
- ⌜CRDT_Addresses !! (fin_to_nat repId) = Some addr⌠∗
- ⌜addr ∈ fixed_addrs⌠∗
- fixed fixed_addrs ∗
- ([∗ list] z ∈ CRDT_Addresses, z ⤇ socket_proto) ∗
- addr ⤳ (∅, ∅) ∗
- free_ports (ip_of_address addr) {[port_of_address addr]} ∗
- locstate_tok repId ∗
- lockinv_tok repId ∗
- crdt_fun_spec crdt_val
- }}}
- statelib_init StLib_StSerialization.(s_serializer).(s_ser)
- StLib_StSerialization.(s_serializer).(s_deser)
- addrs_val
- #repId
- crdt_val @[ip_of_address addr]
- {{{ gs_val upd_val, RET (gs_val, upd_val);
- StLib_OwnLocalState repId ∅ ∅ ∗
- internal_get_state_spec gs_val repId addr ∗
- internal_update_spec upd_val repId addr
- }}}.
-
Lemma internal_init_spec_holds :
StLib_GlobalInv -∗ internal_init_spec.
Proof.
iIntros "#Hinv" (i addr fixed_addr addrs_val crdt_val).
iModIntro.
- iIntros (φ) "(%Hislist&%Haddr&%Haddr_fixed&#Hfixed&#Hprotos&Hsoup&Hfree&Huser_tok&Hlock_tok&#Hcrdt_spec)Hφ".
+ iIntros (φ) "(%Hislist&%Haddr&%Haddr_fixed&#Hfixed&#Hprotos&Hsoup&Hfree&[Huser_tok Hlock_tok]&#Hcrdt_spec)Hφ".
wp_lam. wp_pures.
wp_apply "Hcrdt_spec"; first trivial.
iIntros (v) "(%init_st_fn & %mutator_fn & %merge_fn & -> &
@@ -861,39 +828,3 @@ Section StateLib_Proof.
End StateLib_Proof.
-
-
-Section StLibSetup.
-
-(** TODO: setup the library for aient to use:
- * From true, derive the existence of initial resources (using the above
- * section)
- * + init spec. *)
-
-End StLibSetup.
-
-Section Instantiation.
-
- (**TODO: adapt.
- Context {LogOp LogSt : Type}.
- Context `{!anerisG Mdl Σ, !EqDecision LogOp, !Countable LogOp,
- !CRDT_Params, !StLib_Params LogOp LogSt, !Internal_StLibG LogOp Σ,
- !RCBG Σ}.
-
- Global Instance init_fun_instance : StLib_Init_Function := { init := oplib_init ser_fun deser_fun }.
- Global Instance oplib_res_instance `{!RCB_resources Mdl Σ, !StLib_InvGhostNames} : StLib_Res LogOp := {
- StLib_InitToken := oplib_init_token;
- StLib_SocketProto := RCB_socket_proto;
- }.
-
- Program Global Instance oplib_setup_instance : StLibSetup.
- Next Obligation.
- iIntros (E) "_".
- iMod (oplib_setup with "[//]") as (res names) "(#Hinv & Hglob & Htoks & #Hinit)".
- iModIntro.
- iExists oplib_res_instance.
- simpl.
- iFrame "Hinv Hglob Htoks Hinit".
- Qed. *)
-
-End Instantiation.
diff --git a/aneris/examples/crdt/statelib/proof/stlib_proof_setup.v b/aneris/examples/crdt/statelib/proof/stlib_proof_setup.v
new file mode 100644
index 0000000..08421ed
--- /dev/null
+++ b/aneris/examples/crdt/statelib/proof/stlib_proof_setup.v
@@ -0,0 +1,152 @@
+From stdpp Require Import gmap.
+
+From iris.base_logic Require Import invariants bi.
+From iris.algebra Require Import agree auth excl gmap.
+
+From aneris.algebra Require Import monotone.
+From aneris.aneris_lang
+ Require Import lang network tactics proofmode lifting resources.
+From aneris.aneris_lang.lib
+ Require Import list_proof lock_proof vector_clock_proof serialization_proof
+ map_proof lock_proof network_util_proof inject.
+From aneris.aneris_lang.lib.serialization Require Import serialization_proof.
+From aneris.aneris_lang.lib.vector_clock Require Import vector_clock_proof.
+From aneris.aneris_lang.program_logic Require Import lightweight_atomic.
+From aneris.prelude Require Import misc time.
+
+From aneris.examples.crdt.spec
+ Require Import crdt_events crdt_resources crdt_denot crdt_time crdt_base.
+From aneris.examples.crdt.statelib.resources
+ Require Import resources_update resources utils resources_utils
+ resources_inv resources_local resources_global resources_lock
+ resources_allocation.
+
+From aneris.examples.crdt.statelib Require Import statelib_code.
+From aneris.examples.crdt.statelib.user_model
+ Require Import params model semi_join_lattices.
+From aneris.examples.crdt.statelib.time Require Import time.
+From aneris.examples.crdt.statelib.STS
+ Require Import utils gst lst mutation merge.
+From aneris.examples.crdt.statelib.proof
+ Require Import spec events utils
+ stlib_proof_utils internal_specs stlib_proof.
+
+Instance timeinst : Log_Time := timestamp_time.
+
+
+
+Section StLibSetup.
+
+ Context `{LogOp: Type, LogSt : Type,
+ !anerisG Mdl Σ, !EqDecision LogOp, !Countable LogOp,
+ !CRDT_Params, !Lattice LogSt, !StLib_Params LogOp LogSt,
+ !Internal_StLibG LogOp Σ}.
+
+ Notation princ_ev := (@principal (gset (Event LogOp)) cc_subseteq).
+
+ (* TODO: cleanup *)
+ Ltac rewrite_lookup := repeat (
+ match goal with
+ | [ H1 : _ !! ?i = Some ?v1, H2 : _ !! ?i = Some ?v2 |- _ ] =>
+ rewrite H1 in H2; inversion H2
+ end); subst.
+
+ (* The following lemma is inspired by the OpLib corresponding lemma *)
+ Lemma stlib_setup E :
+ True ⊢ |={E}=> ∃ (GNames : StLib_GhostNames),
+ StLib_GlobalInv ∗
+ StLib_OwnGlobalState ∅ ∗
+ (∃ (S: gset (fin (length CRDT_Addresses))),
+ (∀ i, ⌜i ∈ SâŒ)
+ ∗ [∗ set] f ∈ S, stlib_init_token f) ∗
+ internal_init_spec.
+ Proof.
+ iIntros (_).
+ iMod (alloc_loc_own with "[//]") as (γ_own) "(%S & %HS_def & HS_own0 & HS_own1 & HS_own2)".
+ iMod (alloc_loc_for with "[//]") as (γ_for) "(%S' & %HS'_def & HS_for0 & HS_for1)".
+ assert(S' = S) as ->; [ by apply set_eq | clear HS'_def ].
+ iMod (alloc_loc_sub with "[//]") as (γ_sub) "(%S' & %HS'_def & HS_sub0 & HS_sub1)".
+ assert(S' = S) as ->; [ by apply set_eq | clear HS'_def ].
+ iMod (alloc_loc_cc with "[//]") as (γ_cc) "(%S' & %HS'_def & HS_cc_auth & #HS_cc_frag)".
+ assert(S' = S) as ->; [ by apply set_eq | clear HS'_def ].
+ iMod (alloc_loc_cc' with "[//]") as (γ_cc') "(%S' & %HS'_def & HS_cc'_auth & #HS_cc'_frag)".
+ assert(S' = S) as ->; [ by apply set_eq | clear HS'_def ].
+ iMod (alloc_global with "[//]") as (γ_global) "[Hglobal Hglobal']".
+ iMod (alloc_global_snap with "[//]") as (γ_global_snap) "[Hglobal_snap_auth #Hglobal_snap_snap]".
+ set HNames := (Build_StLib_GhostNames γ_global γ_global_snap γ_own γ_for γ_sub γ_cc γ_cc').
+ iExists HNames.
+ iMod (inv_alloc CRDT_InvName _ (StLib_GlobalInv_prop)
+ with "[HS_own1 HS_for1 HS_sub1 HS_cc_auth HS_cc'_auth Hglobal' Hglobal_snap_auth]")
+ as "#Hinv".
+ { iNext. iExists (∅, vreplicate (length CRDT_Addresses) ∅).
+ iFrame.
+ iSplit; first (iPureIntro; apply gst_init_valid).
+ iExists S; first iFrame"%".
+ rewrite /StLib_GlibInv_local_part.
+ iDestruct (big_sepS_sep_2 with "HS_own1 HS_for1") as "HS".
+ iDestruct (big_sepS_sep_2 with "HS_sub1 HS") as "HS".
+ iDestruct (big_sepS_sep_2 with "HS_cc_auth HS") as "HS".
+ iDestruct (big_sepS_sep_2 with "HS_cc'_auth HS") as "HS".
+ iApply (big_sepS_mono with "HS").
+ iIntros (x Hx_in) "(H0 & H1 & H2 & H3 & H4)".
+ repeat iExists ∅. rewrite union_empty_R. iFrame.
+ iPureIntro.
+ by split; first by rewrite vlookup_replicate. }
+ iModIntro.
+ iFrame "Hinv".
+
+ iDestruct (internal_init_spec_holds with "Hinv") as "#Hinit".
+ iFrame "#". iFrame "Hglobal".
+
+ iExists S. iFrame "%".
+ rewrite/stlib_init_token/locstate_tok/lockinv_tok.
+ iDestruct (big_sepS_sep_2 with "HS_own0 HS_for0") as "HS".
+ iDestruct (big_sepS_sep_2 with "HS_own2 HS") as "HS".
+ iDestruct (big_sepS_sep_2 with "HS_sub0 HS") as "HS".
+ iDestruct (big_sepS_sep_2 with "HS_cc_frag HS") as "HS".
+ (*iDestruct (big_sepS_sep_2 with "HS_cc'_frag HS") as "HS".*)
+ iApply (big_sepS_mono with "HS").
+ iIntros (x Hx_in) "(H0 & H1 & H2 & H3 & H4)".
+ iFrame.
+ Qed.
+
+End StLibSetup.
+
+(** TODO: setup the library for aient to use:
+ * From true, derive the existence of initial resources (using the above
+ * section)
+ * + init spec. *)
+
+Section Instantiation.
+
+ Context {LogOp LogSt : Type}.
+ Context `{!anerisG Mdl Σ, !EqDecision LogOp, !Countable LogOp,
+ !CRDT_Params, !Lattice LogSt, !StLib_Params LogOp LogSt,
+ !Internal_StLibG LogOp Σ}.
+
+ Global Instance init_fun_instance : StLib_Init_Function := {
+ init := statelib_init
+ StLib_StSerialization.(s_serializer).(s_ser)
+ StLib_StSerialization.(s_serializer).(s_deser) }.
+
+ Global Instance stlib_res_instance `{!StLib_GhostNames}
+ : StLib_Res LogOp := {
+ StLib_InitToken := stlib_init_token;
+ StLib_SocketProto := socket_proto;
+ }.
+
+ (** TODO: ask Abel whether I should:
+ * - replace this by a proof obligation
+ * - Qed instead of defined
+ *)
+ Global Instance stlib_setup_instance : StLibSetup.
+ Proof.
+ iIntros (E) "_".
+ iMod (stlib_setup with "[//]") as (names) "(#Hinv & Hglob & Htoks & #Hinit)".
+ iModIntro.
+ iExists stlib_res_instance.
+ simpl.
+ iFrame "Hinv Hglob Htoks".
+ Admitted.
+
+End Instantiation.
diff --git a/aneris/examples/crdt/statelib/resources/resources_inv.v b/aneris/examples/crdt/statelib/resources/resources_inv.v
index 54f8f80..fd1871e 100644
--- a/aneris/examples/crdt/statelib/resources/resources_inv.v
+++ b/aneris/examples/crdt/statelib/resources/resources_inv.v
@@ -34,15 +34,18 @@ Section AboutGlobalInvariant.
own (γ_loc_cc !!! f) (◠princ_ev (h__local ∪ h__sub)) ∗
own (γ_loc_cc' !!! f) (◠princ_ev (h__local ∪ h__foreign)).
- Definition StLib_GlobalInv : iProp Σ :=
- inv CRDT_InvName
- (∃ (g: Gst CRDT_Op), own γ_global ((1/3)%Qp, to_agree g.1)
+ Definition StLib_GlobalInv_prop : iProp Σ :=
+ ∃ (g: Gst CRDT_Op), own γ_global ((1/3)%Qp, to_agree g.1)
∗ own γ_global_snap (◠g.1)
∗ ⌜ Gst_Validity g âŒ
∗ ∃ (S: gset (fRepId)),
(∀ (f: fRepId), ⌜f ∈ SâŒ)
∗ [∗ set] k ∈ S,
- StLib_GlibInv_local_part k g).
+ StLib_GlibInv_local_part k g.
+
+ Definition StLib_GlobalInv : iProp Σ :=
+ inv CRDT_InvName
+ StLib_GlobalInv_prop.
Global Instance StLib_GlobalInv_persistent : Persistent StLib_GlobalInv := _.
End AboutGlobalInvariant.
diff --git a/aneris/examples/crdt/statelib/resources/resources_update.v b/aneris/examples/crdt/statelib/resources/resources_update.v
index 5a75e47..a73f18e 100644
--- a/aneris/examples/crdt/statelib/resources/resources_update.v
+++ b/aneris/examples/crdt/statelib/resources/resources_update.v
@@ -500,7 +500,7 @@ Section Resources_updates.
repeat split; try done.
by rewrite vlookup_insert Hst_proj. }
iExists f. by iFrame.
- Admitted.
+ Qed.
End Resources_updates.
diff --git a/aneris/examples/crdt/statelib/user_model/params.v b/aneris/examples/crdt/statelib/user_model/params.v
index af8b0e7..e89b7e9 100644
--- a/aneris/examples/crdt/statelib/user_model/params.v
+++ b/aneris/examples/crdt/statelib/user_model/params.v
@@ -41,8 +41,8 @@ Section Params.
Class StLib_Res `{!CRDT_Params} := {
StLib_CRDT_Res :> CRDT_Res_Mixin Mdl Σ LogOp;
- StLib_InitToken : nat -> iProp Σ;
- StLib_SocketProto : nat -> socket_interp Σ;
+ StLib_InitToken : (fin (length CRDT_Addresses)) -> iProp Σ;
+ StLib_SocketProto : socket_interp Σ;
}.
End Params.
--
GitLab