Skip to content
Snippets Groups Projects
Unverified Commit 1bfc4b36 authored by Lennard Gäher's avatar Lennard Gäher
Browse files

improve statics

parent 1e8d90e4
No related branches found
No related tags found
No related merge requests found
This commit is part of merge request !27. Comments created here will be created in the context of that merge request.
Hide whitespace changes
Inline Side-by-side
case_studies/minivec/output/minivec/interface.rrlib deleted 100644 → 0
+ 0
− 137
View file @ 1e8d90e4
{
"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
+ 40
− 4
View file @ 1bfc4b36
......@@ -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
+ 69
− 16
View file @ 1bfc4b36
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.
......
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