improve statics

case_studies/minivec/output/minivec/interface.rrlib

-{
-  "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

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.

theories/rust_typing/static.v

 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.