From 1bfc4b36cc501206bcb072d1df7a358262dcfdbc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <lennard.gaeher@ibm.com>
Date: Wed, 20 Mar 2024 11:26:26 +0100
Subject: [PATCH] improve statics
---
.../minivec/output/minivec/interface.rrlib | 137 ------------------
stdlib/spin/theories/once/once_ghost_state.v | 44 +++++-
theories/rust_typing/static.v | 85 +++++++++--
3 files changed, 109 insertions(+), 157 deletions(-)
delete mode 100644 case_studies/minivec/output/minivec/interface.rrlib
diff --git a/case_studies/minivec/output/minivec/interface.rrlib b/case_studies/minivec/output/minivec/interface.rrlib
deleted file mode 100644
index d2bb2df4..00000000
--- a/case_studies/minivec/output/minivec/interface.rrlib
+++ /dev/null
@@ -1,137 +0,0 @@
-{
- "items": [
- {
- "kind": "adt",
- "path": [
- "Vec"
- ],
- "rtype": "Vec_inv_t_rt",
- "semtype": "Vec_inv_t",
- "syntype": "Vec_st"
- },
- {
- "kind": "adt",
- "path": [
- "RawVec"
- ],
- "rtype": "RawVec_inv_t_rt",
- "semtype": "RawVec_inv_t",
- "syntype": "RawVec_st"
- },
- {
- "kind": "method",
- "name": "RawVec_T_ptr",
- "path": [
- "ptr"
- ],
- "spec": "type_of_RawVec_T_ptr"
- },
- {
- "kind": "method",
- "name": "RawVec_T_cap",
- "path": [
- "cap"
- ],
- "spec": "type_of_RawVec_T_cap"
- },
- {
- "kind": "method",
- "name": "RawVec_T_new",
- "path": [
- "new"
- ],
- "spec": "type_of_RawVec_T_new"
- },
- {
- "kind": "method",
- "name": "RawVec_T_grow",
- "path": [
- "grow"
- ],
- "spec": "type_of_RawVec_T_grow"
- },
- {
- "kind": "method",
- "name": "Vec_T_len",
- "path": [
- "len"
- ],
- "spec": "type_of_Vec_T_len"
- },
- {
- "kind": "method",
- "name": "Vec_T_new",
- "path": [
- "new"
- ],
- "spec": "type_of_Vec_T_new"
- },
- {
- "kind": "method",
- "name": "Vec_T_push",
- "path": [
- "push"
- ],
- "spec": "type_of_Vec_T_push"
- },
- {
- "kind": "method",
- "name": "Vec_T_pop",
- "path": [
- "pop"
- ],
- "spec": "type_of_Vec_T_pop"
- },
- {
- "kind": "method",
- "name": "Vec_T_insert",
- "path": [
- "insert"
- ],
- "spec": "type_of_Vec_T_insert"
- },
- {
- "kind": "method",
- "name": "Vec_T_remove",
- "path": [
- "remove"
- ],
- "spec": "type_of_Vec_T_remove"
- },
- {
- "kind": "method",
- "name": "Vec_T_get_unchecked_mut",
- "path": [
- "get_unchecked_mut"
- ],
- "spec": "type_of_Vec_T_get_unchecked_mut"
- },
- {
- "kind": "method",
- "name": "Vec_T_get_mut",
- "path": [
- "get_mut"
- ],
- "spec": "type_of_Vec_T_get_mut"
- },
- {
- "kind": "method",
- "name": "Vec_T_get_unchecked",
- "path": [
- "get_unchecked"
- ],
- "spec": "type_of_Vec_T_get_unchecked"
- },
- {
- "kind": "method",
- "name": "Vec_T_get",
- "path": [
- "get"
- ],
- "spec": "type_of_Vec_T_get"
- }
- ],
- "refinedrust_module": "generated_specs_minivec",
- "refinedrust_name": "minivec",
- "refinedrust_path": "refinedrust.examples.minivec.generated"
-}
\ No newline at end of file
diff --git a/stdlib/spin/theories/once/once_ghost_state.v b/stdlib/spin/theories/once/once_ghost_state.v
index 603dc069..ef70524d 100644
--- a/stdlib/spin/theories/once/once_ghost_state.v
+++ b/stdlib/spin/theories/once/once_ghost_state.v
@@ -79,7 +79,7 @@ Section once.
iPureIntro. by apply to_agree_op_inv_L in Hv.
Qed.
- Global Instance once_init_tok_timeless γ a : Timeless (once_status_tok γ a).
+ Global Instance once_status_tok_timeless γ a : Timeless (once_status_tok γ a).
Proof. rewrite once_status_tok_eq; destruct a; apply _. Qed.
End once.
@@ -102,16 +102,51 @@ Section typing.
Definition FindOnceStatusTok γ : find_in_context_info :=
{| fic_A := option A; fic_Prop a := once_status_tok γ a |}.
Global Instance once_status_tok_related γ a : RelatedTo (once_status_tok γ a) := {| rt_fic := FindOnceStatusTok γ |}.
+
+ Lemma find_in_context_once_status_tok γ T :
+ (∃ r : option A, once_status_tok γ r ∗ T r)
+ ⊢ find_in_context (FindOnceStatusTok γ) T.
+ Proof. iDestruct 1 as (r) "[Hs HT]". iExists _ => /=. iFrame. Qed.
+ Global Instance find_in_context_once_status_tok_inst γ :
+ FindInContext (FindOnceStatusTok γ) FICSyntactic | 1 :=
+ λ T, i2p (find_in_context_once_status_tok γ T).
End typing.
(** Since a frequent use case of once is in conjunction with static variables, we provide some extra support for that *)
Section statics.
Context {A} `{!typeGS Σ} `{!staticGS Σ} `{!onceG Σ A}.
- Definition once_status π (s : string) (a : option A) : iProp Σ :=
- ∃ γ, once_status_tok γ a ∗ initialized π s γ.
- Global Typeclasses Opaque once_status.
+ (* Important for evar proofs: first determine the ghost name. *)
+ Definition once_status (s : string) (a : option A) : iProp Σ :=
+ ∃ γ, ⌜static_has_refinement s γ⌠∗ once_status_tok γ a.
+
+ Definition once_initialized π (s : string) (a : option A) : iProp Σ :=
+ ∃ γ, initialized π s γ ∗ once_status_tok γ a.
+
+
+ (* I guess in the beginning I allocate this for every global.
+
+ What agreements do I need?
+ - two instances of static_rfn agree
+ - initialized and static_rfn, they also agree by definition of initialized
+
+ Point: I created an indirection to get timeless knowledge of the refinement.
+ Only when I access it do I need the initialized.
+ I could also keep the initialized in there, I guess.
+ Question is where it comes from...
+ We could dispatch it at link time when doing adequacy for the main function.
+ But it's unclear how that would work for getting something for the other entry points.
+ For now, go with this. We can get something fancier later.
+ Only the ghost knowledge needs to stay around.
+
+ Use cases:
+ - I have static_rfn in my invariant
+ - then I actually go into a method where I get the layout
+ - and check that it's in range.
+ - here I need to have agreement.
+ *)
+ (*
Definition FindOnceStatus π s : find_in_context_info :=
{| fic_A := option A; fic_Prop a := once_status π s a |}.
Global Instance once_status_related π s a : RelatedTo (once_status π s a) := {| rt_fic := FindOnceStatus π s |}.
@@ -122,4 +157,5 @@ Section statics.
iIntros "(-> & HT)".
iIntros "$"; done.
Qed.
+ *)
End statics.
diff --git a/theories/rust_typing/static.v b/theories/rust_typing/static.v
index a963676d..0a28de1b 100644
--- a/theories/rust_typing/static.v
+++ b/theories/rust_typing/static.v
@@ -1,29 +1,63 @@
From refinedrust Require Import base type ltypes programs references.
From iris.base_logic Require Import ghost_map.
+Record btype `{!typeGS Σ} : Type := {
+ btype_rt : Type;
+ btype_ty : type btype_rt;
+ btype_r : btype_rt;
+}.
+
+Definition btype_to_rtype `{!typeGS Σ} (ty : btype) : sigT type :=
+ existT _ ty.(btype_ty).
+
(* TODO: should require that type is Send? *)
Class staticGS `{!typeGS Σ} := {
static_locs : gmap string loc;
- static_types : gmap string (sigT type);
+ static_types : gmap string btype;
}.
Global Arguments staticGS _ {_}.
-
Section statics.
Context `{!typeGS Σ} `{!staticGS Σ}.
+ Import EqNotations.
+
(** Assertion stating that the static with name [x] has been registered for location [l] and type [ty]. *)
(** We assume registration for the expected type and the location parameter in the context where we verify our code *)
Definition static_is_registered (x : string) (l : loc) (ty : sigT type) :=
- static_locs !! x = Some l ∧ static_types !! x = Some ty.
+ static_locs !! x = Some l ∧ btype_to_rtype <$> (static_types !! x) = Some ty.
- Import EqNotations.
+ (** In our specifications, we can use this assertion to assume a refinement for the static *)
+ Definition static_has_refinement (x : string) {rt} (r : rt) :=
+ ∃ ty, static_types !! x = Some ty ∧ ∃ (Heq : rt = ty.(btype_rt)), (rew [id] Heq in r) = ty.(btype_r).
+
+ Lemma static_has_refinement_inj {rt1 rt2} (r1 : rt1) (r2 : rt2) name :
+ static_has_refinement name r1 →
+ static_has_refinement name r2 →
+ ∃ (Heq : rt1 = rt2), rew Heq in r1 = r2.
+ Proof.
+ intros (ty1 & Hlook1 & Heq1 & Ha).
+ intros (ty2 & Hlook2 & Heq2 & Hb).
+ simplify_eq. exists eq_refl.
+ simpl in *. by subst.
+ Qed.
+
+ Global Instance simpl_and_static_has_refinement {rt} (x y : rt) `{!TCFastDone (static_has_refinement name x)} :
+ SimplBoth (static_has_refinement name y) (x = y).
+ Proof.
+ split; last naive_solver.
+ rename select (TCFastDone _) into Hs. unfold TCFastDone in Hs.
+ intros Ha. destruct (static_has_refinement_inj _ _ _ Hs Ha) as (Heq & <-).
+ rewrite (UIP_refl _ _ Heq).
+ done.
+ Qed.
(* The global variable "name" has been initialized with refinement "r" *)
Definition initialized {rt} (π : thread_id) (name : string) (r : rt) : iProp Σ :=
- ∃ (l : loc) (ty : sigT type), ⌜static_is_registered name l ty⌠∗
- ∃ (Heq : rt = projT1 ty),
- (l â—áµ¥{Ï€} (rew Heq in #r) @ shr_ref (projT2 ty) static)%I.
+ ∃ (l : loc) (ty : btype), ⌜static_locs !! name = Some l⌠∗ ⌜static_types !! name = Some ty⌠∗
+ ∃ (Heq : rt = ty.(btype_rt)),
+ ⌜(rew [id] Heq in r) = ty.(btype_r) ⌠∗
+ (l â—áµ¥{Ï€} (#ty.(btype_r)) @ shr_ref ty.(btype_ty) static)%I.
Global Instance initialized_persistent {rt} (Ï€ : thread_id) (name : string) (r : rt) :
Persistent (initialized π name r).
@@ -36,30 +70,45 @@ Section statics.
(* On introduction of `initialized`, destruct it *)
Lemma simplify_initialized_hyp {rt} π (x : rt) name ty l
`{!TCFastDone (static_is_registered name l ty)} T:
- (∃ (Heq : rt = projT1 ty), l â—áµ¥{Ï€} (rew Heq in #x) @ shr_ref (projT2 ty) static -∗ T)
+ (∃ (Heq : rt = projT1 ty), l â—áµ¥{Ï€} (rew Heq in #x) @ shr_ref (projT2 ty) static -∗ ⌜static_has_refinement name x⌠-∗ T)
⊢ simplify_hyp (initialized π name x) T.
Proof.
unfold TCFastDone in *. destruct ty as [rt' ty].
iDestruct 1 as (?) "HT". subst; simpl in *.
iIntros "Hinit".
- iDestruct "Hinit" as "(%l' & %ty' & %Hlook1' & %Heq & Hl)".
- destruct ty' as (rt & ty'). subst. simpl in *.
- repeat match goal with | H : static_is_registered _ _ _ |- _ => destruct H end.
- simplify_eq.
- match goal with | H : existT _ _ = existT _ _ |- _ => apply existT_inj in H end.
+ iDestruct "Hinit" as "(%l' & %ty' & %Hlook1 & %Hlook2 & %Heq & %Hrfn & Hl)".
+ subst. simpl in *. subst.
+ destruct ty'; simpl in *.
+ repeat match goal with | H : static_is_registered _ _ _ |- _ => destruct H as [H1 H2] end.
+ apply fmap_Some in H2 as ([] & H2 & Hb).
+ simplify_eq. unfold btype_to_rtype in Hb; simpl in *.
+ repeat match goal with | H : existT _ _ = existT _ _ |- _ => apply existT_inj in H end.
subst. iApply ("HT" with "Hl").
+ iPureIntro. eexists _. split; first done. exists eq_refl. done.
Qed.
Definition simplify_initialized_hyp_inst := [instance @simplify_initialized_hyp with 0%N].
Global Existing Instance simplify_initialized_hyp_inst.
Lemma initialized_intro {rt} π ty name l (x : rt) :
static_is_registered name l ty →
+ static_has_refinement name x →
(∃ (Heq : rt = projT1 ty), l â—áµ¥{Ï€} (rew Heq in #x) @ shr_ref (projT2 ty) static) -∗
initialized π name x.
- Proof. iIntros (?) "Hl". iExists _, _. by iFrame. Qed.
+ Proof.
+ iIntros ([Hl1 Hl2] (ty2 & Hl3 & Heq' & Hb)) "(%Heq & Hl)".
+ subst. destruct ty. destruct ty2. simpl in *.
+ apply fmap_Some in Hl2 as (bt & Hl2 & Ha). subst.
+ destruct bt. simpl in *.
+ unfold btype_to_rtype in Ha; simpl in *.
+ simplify_eq.
+ repeat match goal with | H : existT _ _ = existT _ _ |- _ => apply existT_inj in H end.
+ subst.
+ iExists _, _. iR. iR.
+ iExists eq_refl. simpl. iR. by iFrame.
+ Qed.
Lemma simplify_initialized_goal {rt} π (x : rt) name l ty
- `{!TCFastDone (static_is_registered name l ty)} T:
+ `{!TCFastDone (static_is_registered name l ty)} `{!TCFastDone (static_has_refinement name x)} T:
(∃ (Heq : rt = projT1 ty), l â—áµ¥{Ï€} (rew Heq in #x) @ shr_ref (projT2 ty) static ∗ T)
⊢ simplify_goal (initialized π name x) T.
Proof.
@@ -76,7 +125,6 @@ Section statics.
RelatedTo (initialized π name r) :=
{| rt_fic := FindInitialized π rt name|}.
- Set Printing Universes.
Lemma find_in_context_initialized π name rt (T : rt → iProp Σ):
(∃ x, initialized π name x ∗ T x)
⊢ find_in_context (FindInitialized π rt name) T.
@@ -93,6 +141,11 @@ Section statics.
Global Existing Instance subsume_initialized_inst.
End statics.
Global Typeclasses Opaque initialized.
+Global Typeclasses Opaque static_has_refinement.
+
+Global Arguments static_has_refinement : simpl never.
+Global Arguments static_is_registered : simpl never.
+
(* After calling adequacy:
we need to create initialized things.
--
GitLab