Commit f6f0b35a authored by Lennard Gäher's avatar Lennard Gäher
Browse files

lang: time-credits (JH's later) and W.ref

parent 145abe3c
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting.
From refinedc.lang Require Export lang ghost_state notation.
From refinedc.lang Require Export lang ghost_state time notation.
From refinedc.lang Require Import tactics.
Set Default Proof Using "Type".
Import uPred.
Class refinedcG Σ := RefinedCG {
refinedcG_invG : invGS Σ;
refinedcG_gen_heapG :> heapG Σ
refinedcG_gen_heapG :> heapG Σ;
refinedcG_timeGS :> timeGS Σ;
}.
Instance c_irisG `{!refinedcG Σ} : irisGS c_lang Σ := {
Program Instance c_irisG `{!refinedcG Σ} : irisGS c_lang Σ := {
iris_invG := refinedcG_invG;
state_interp σ κs _ _ := state_ctx σ;
state_interp σ n κs _ := (state_ctx σ time_interp n)%I;
fork_post _ := True%I;
num_laters_per_step _ := 0%nat;
state_interp_mono _ _ _ _ := fupd_intro _ _;
num_laters_per_step n := n%nat;
}.
Next Obligation.
intros. simpl. iIntros "[$ Htime]".
iMod (time_interp_step with "Htime") as "$"; done.
Qed.
Global Opaque iris_invG.
Instance into_val_val v : IntoVal (to_rtexpr (Val v)) v.
......@@ -49,6 +53,65 @@ Proof. solve_atomic. Qed.
Section lifting.
Context `{!refinedcG Σ}.
(** steps related to time receipts *)
(** lemmas taken from https://gitlab.mpi-sws.org/iris/lambda-rust/-/blob/masters/rusthornbelt/theories/lang/lifting.v *)
Lemma wp_step_fupdN_time_receipt n m E1 E2 e P Φ :
TCEq (to_val e) None E2 E1 timeN E1
time_ctx - ptime n -
(ctime m ((|={E1E2,}=> |={}=>^(S (n + m)) |={,E1E2}=> P)
WP e @ E2 {{ v, P ={E1}= Φ v }})) -
WP e @ E1 {{ Φ }}.
Proof.
iIntros (???) "#TIME #Hn H".
iApply (wp_step_fupdN (S (n + m)) _ _ E2)=>//. iSplit.
- iIntros "* [_ Ht]". iMod (time_receipt_le with "TIME Ht Hn [H]") as "[% ?]"=>//.
+ iDestruct "H" as "[$ _]".
+ iApply fupd_mask_weaken; [|iIntros "_ !> !% /="; lia]; set_solver+.
- iDestruct "H" as "[_ $]".
Qed.
Lemma wp_step_fupdN_persistent_time_receipt n E1 E2 e P Φ :
TCEq (to_val e) None E2 E1 timeN E1
time_ctx - ptime n - (|={E1E2,}=> |={}=>^(S n) |={, E1E2}=> P) -
WP e @ E2 {{ v, P ={E1}= Φ v }} -
WP e @ E1 {{ Φ }}.
Proof.
iIntros (???) "#TIME #Hn HP Hwp".
iApply (wp_step_fupdN_time_receipt _ _ E1 E2 with "TIME Hn [> -]")=>//.
iMod cumulative_time_receipt_0 as "$". iFrame. by rewrite -plus_n_O.
Qed.
(* FIXME : we need to unfold WP *)
Lemma wp_cumulative_time_receipt E e Φ :
TCEq (to_val e) None timeN E
time_ctx -
WP e @ (E∖↑timeN) {{ v, ctime 1 - Φ v }} -
WP e @ E {{ Φ }}.
Proof.
rewrite !wp_unfold /wp_pre /=. iIntros (-> ?) "#TIME Hwp".
iIntros (?????) "[Hσ Ht]".
iMod (step_cumulative_time_receipt with "TIME Ht") as "[Ht Hclose]"=>//.
iMod ("Hwp" $! _ _ _ [] 0%nat with "[$]") as "[$ Hwp]".
iIntros "!>" (e2 σ2 efs stp). iMod ("Hwp" $! e2 σ2 efs stp) as "Hwp".
iIntros "!> !>". iMod "Hwp". iModIntro.
iApply (step_fupdN_wand with "Hwp"). iIntros ">([$ Ht] & Hwp & $)".
iMod ("Hclose" with "Ht") as "[$ ?]".
iApply (wp_wand with "[Hwp]"); [iApply (wp_mask_mono with "Hwp"); solve_ndisj|].
iIntros "!> % H". by iApply "H".
Qed.
Lemma wp_persistent_time_receipt n E e Φ :
TCEq (to_val e) None timeN E
time_ctx -
ptime n - WP e @ (E∖↑timeN) {{ v, ptime (S n) - Φ v }} -
WP e @ E {{ Φ }}.
Proof.
iIntros. iApply wp_fupd. iApply wp_cumulative_time_receipt=>//.
iApply (wp_wand with "[$]"). iIntros (?) "HΦ ?". iApply "HΦ".
by iApply (cumulative_persistent_time_receipt _ 1 with "[//] [$]").
Qed.
Lemma wp_alloc_failed E Φ:
WP AllocFailed @ E {{ Φ }}.
Proof.
......@@ -70,7 +133,7 @@ Section lifting.
Proof.
iIntros (He ?) "HWP".
iApply wp_lift_head_step_fupd => //.
iIntros (σ1 κ κs n ?) "[[% Hhctx] Hfnctx]".
iIntros (σ1 ns κ κs nt) "([[% Hhctx] Hfnctx] & Htime)".
iMod ("HWP" $! σ1 with "[$Hhctx $Hfnctx//]") as (Hstep) "HWP".
iModIntro. iSplit. {
iPureIntro. destruct Hstep as (?&?&?&?&?).
......@@ -83,7 +146,9 @@ Section lifting.
all: try match goal with | H : to_rtexpr ?e = to_rtstmt _ _ |- _ => destruct e; discriminate end.
all: iMod ("HWP" with "[//] [%]") as "HWP"; first naive_solver.
all: do 2 iModIntro.
all: iMod "HWP" as (->) "[$ HWP]"; iModIntro => /=; by rewrite right_id.
all: iMod "HWP" as (->) "[$ HWP]".
all: iMod (time_interp_step with "Htime") as "$".
all: iModIntro => /=; by rewrite right_id.
Qed.
Lemma wp_lift_expr_step_fupd E (e : expr) Φ:
......
From stdpp Require Import fin_maps.
From refinedc.lang Require Export notation.
From refinedc.lang Require Export notation rust.
Set Default Proof Using "Type".
Module W.
......@@ -34,6 +34,7 @@ Inductive expr :=
| LocInfoE (a : location_info) (e : expr)
| StructInit (ly : struct_layout) (fs : list (string * expr))
| MacroE (m : list lang.expr lang.expr) (es : list expr) (wf : MacroWfSubst m)
| Borrow (m : mutability) (κn : string) (e : expr)
(* for opaque expressions*)
| Expr (e : lang.expr)
.
......@@ -66,10 +67,11 @@ Lemma expr_ind (P : expr → Prop) :
( (a : location_info) (e : expr), P e P (LocInfoE a e))
( (ly : struct_layout) (fs : list (string * expr)), Forall P fs.*2 P (StructInit ly fs))
( (m : list lang.expr lang.expr) (es : list expr) (wf : MacroWfSubst m), Forall P es P (MacroE m es wf))
( (m : mutability) (κn : string) (e : expr), P e P (Borrow m κn e))
( (e : lang.expr), P (Expr e)) (e : expr), P e.
Proof.
move => *. generalize dependent P => P. match goal with | e : expr |- _ => revert e end.
fix FIX 1. move => [ ^e] => ???????? Hcall Hconcat ?????????????? Hstruct Hmacro ?.
fix FIX 1. move => [ ^e] => ???????? Hcall Hconcat ?????????????? Hstruct Hmacro Hbor ?.
9: {
apply Hcall; [ |apply Forall_true => ?]; by apply: FIX.
}
......@@ -113,6 +115,7 @@ Fixpoint to_expr (e : expr) : lang.expr :=
| OffsetOf s m => notation.OffsetOf s m
| OffsetOfUnion ul m => notation.OffsetOfUnion ul m
| MacroE m es _ => notation.MacroE m (to_expr <$> es)
| Borrow m κn e => rust.Ref m κn (to_expr e)
| Expr e => e
end.
......@@ -133,6 +136,8 @@ Ltac of_expr e :=
let e := of_expr e in constr:(AnnotExpr n a e)
| notation.MacroE ?m ?es =>
let es := of_expr es in constr:(MacroE m es _)
| rust.Ref ?m ?κn ?e =>
let e := of_expr e in constr:(Borrow m κn e)
| notation.LocInfo ?a ?e =>
let e := of_expr e in constr:(LocInfoE a e)
| notation.StructInit ?ly ?fs =>
......@@ -210,6 +215,7 @@ Inductive ectx_item :=
| LValueCtx
| AnnotExprCtx (n : nat) {A} (a : A)
| LocInfoECtx (a : location_info)
| BorrowCtx (m : mutability) (κn : string)
(* the following would not work, thus we don't have a context, but prove a specialized bind rule*)
(*| StructInitCtx (ly : struct_layout) (vfs : list (string * val)) (id : string) (efs : list (string * expr))*)
| GetMemberCtx (s : struct_layout) (m : var_name)
......@@ -237,6 +243,7 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
| LValueCtx => LValue e
| AnnotExprCtx n a => AnnotExpr n a e
| LocInfoECtx a => LocInfoE a e
| BorrowCtx m κn => Borrow m κn e
| GetMemberCtx s m => GetMember e s m
| GetMemberUnionCtx ul m => GetMemberUnion e ul m
end.
......@@ -298,6 +305,8 @@ Fixpoint find_expr_fill (e : expr) (bind_val : bool) : option (list ectx_item *
Some (Ks ++ [AnnotExprCtx n a], e') else Some ([], e)
| LocInfoE a e1 => if find_expr_fill e1 bind_val is Some (Ks, e') then
Some (Ks ++ [LocInfoECtx a], e') else Some ([], e)
| Borrow m κn e1 => if find_expr_fill e1 bind_val is Some (Ks, e') then
Some (Ks ++ [BorrowCtx m κn], e') else Some ([], e)
| StructInit _ _ => None
| GetMember e1 s m => if find_expr_fill e1 bind_val is Some (Ks, e') then
Some (Ks ++ [GetMemberCtx s m], e') else Some ([], e)
......@@ -339,10 +348,11 @@ Proof.
apply: []|
apply: (replicate n lang.SkipECtx)|
apply: []|
apply: []|
apply: [lang.BinOpRCtx _ _ _ _]|
apply: []|..
]).
move: K => [|||||||||||||||||n|||] * //=.
move: K => [|||||||||||||||||n||||] * //=.
- (** Call *)
do 2 f_equal.
rewrite !fmap_app !fmap_cons. repeat f_equal; eauto.
......@@ -547,6 +557,7 @@ Fixpoint subst_l (xs : list (var_name * val)) (e : expr) : expr :=
| OffsetOf s m => OffsetOf s m
| OffsetOfUnion ul m => OffsetOfUnion ul m
| MacroE m es wf => MacroE m (subst_l xs <$> es) wf
| Borrow m κn e => Borrow m κn (subst_l xs e)
| Expr e => Expr (lang.subst_l xs e)
end.
......
(** Adapted from the RustHornBelt development by Matsushita et al,
https://gitlab.mpi-sws.org/iris/lambda-rust/-/blob/masters/rusthornbelt/theories/lang/time.v
*)
From iris.algebra Require Import lib.mono_nat numbers.
From iris.base_logic Require Import lib.own.
From iris.base_logic.lib Require Export invariants.
From iris.proofmode Require Import tactics.
(*From lrust.lang Require Export lang.*)
Set Default Proof Using "Type".
Import uPred.
Class timeGS Σ := TimeGS {
time_mono_nat_inG :> inG Σ mono_natR;
time_nat_inG :> inG Σ (authR natUR);
time_global_name : gname;
time_persistent_name : gname;
time_cumulative_name : gname;
}.
Class timePreGS Σ := TimePreGS {
time_preG_mono_nat_inG :> inG Σ mono_natR;
time_preG_nat_inG :> inG Σ (authR natUR);
}.
Definition timeΣ : gFunctors :=
#[GFunctor (constRF mono_natR); GFunctor (constRF (authR natUR))].
Instance subG_timePreGS Σ : subG timeΣ Σ timePreGS Σ.
Proof. solve_inG. Qed.
Definition timeN : namespace := nroot .@ "lft_usr" .@ "time".
Section definitions.
Context `{!timeGS Σ}.
(** persistent time receipt *)
Definition persistent_time_receipt (n : nat) :=
own time_persistent_name (mono_nat_lb n).
(** cumulative time receipt *)
Definition cumulative_time_receipt (n : nat) :=
own time_cumulative_name ( n).
(** invariant *)
Definition time_ctx `{!invGS Σ} :=
inv timeN ( n m,
own time_global_name (mono_nat_lb (n + m))
own time_cumulative_name ( n)
own time_persistent_name (mono_nat_auth 1 m)).
(** authority *)
Definition time_interp (n: nat) : iProp Σ :=
own time_global_name (mono_nat_auth 1 n).
End definitions.
Typeclasses Opaque persistent_time_receipt cumulative_time_receipt.
Instance: Params (@persistent_time_receipt) 2 := {}.
Instance: Params (@cumulative_time_receipt) 2 := {}.
Notation "'ptime' n" := (persistent_time_receipt n)
(at level 1, format "ptime n") : bi_scope.
Notation "'ctime' n" := (cumulative_time_receipt n)
(at level 1, format "ctime n") : bi_scope.
Section time.
Context `{!timeGS Σ}.
Implicit Types P Q : iProp Σ.
Global Instance persistent_time_receipt_timeless n : Timeless (ptime n).
Proof. unfold persistent_time_receipt. apply _. Qed.
Global Instance persistent_time_receipt_persistent n : Persistent (ptime n).
Proof. unfold persistent_time_receipt. apply _. Qed.
Global Instance cumulative_time_receipt_timeless n : Timeless (ctime n).
Proof. unfold cumulative_time_receipt. apply _. Qed.
Lemma time_interp_step n :
time_interp n == time_interp (S n).
Proof. eapply own_update, mono_nat_update. lia. Qed.
Lemma persistent_time_receipt_mono n m :
(n m)%nat ptime m - ptime n.
Proof.
intros ?. unfold persistent_time_receipt. by apply own_mono, mono_nat_lb_mono.
Qed.
Lemma cumulative_time_receipt_mono n m :
(n m)%nat ctime m - ctime n.
Proof.
intros ?. unfold cumulative_time_receipt.
by apply own_mono, auth_frag_mono, nat_included.
Qed.
Lemma persistent_time_receipt_sep n m : ptime (n `max` m) ptime n ptime m.
Proof. by rewrite /persistent_time_receipt -mono_nat_lb_op own_op. Qed.
Lemma cumulative_time_receipt_sep n m : ctime (n + m) ctime n ctime m.
Proof. by rewrite /cumulative_time_receipt -nat_op auth_frag_op own_op. Qed.
Global Instance persistent_time_receipt_from_sep n m : FromSep ptime (n `max` m) ptime n ptime m.
Proof. rewrite /FromSep. by rewrite persistent_time_receipt_sep. Qed.
Global Instance persistent_time_receipt_into_sep n m : IntoSep ptime (n `max` m) ptime n ptime m.
Proof. rewrite /IntoSep. by rewrite persistent_time_receipt_sep. Qed.
Global Instance cumulative_time_receipt_from_sep n m : FromSep ctime (n + m) ctime n ctime m.
Proof. rewrite /FromSep. by rewrite cumulative_time_receipt_sep. Qed.
Global Instance cumulative_time_receipt_into_sep n m : IntoSep ctime (n + m) ctime n ctime m.
Proof. rewrite /IntoSep. by rewrite cumulative_time_receipt_sep. Qed.
Lemma persistent_time_receipt_0 : |==> ptime 0.
Proof. rewrite /persistent_time_receipt. apply own_unit. Qed.
Lemma cumulative_time_receipt_0 : |==> ctime 0.
Proof. rewrite /cumulative_time_receipt. apply own_unit. Qed.
Lemma cumulative_persistent_time_receipt `{!invGS Σ} E n m :
timeN E time_ctx - ctime n - ptime m ={E}= ptime (n + m).
Proof.
iIntros (?) "#TIME Hn #Hm".
unfold persistent_time_receipt, cumulative_time_receipt.
iInv "TIME" as (n' m') ">(Hglob & Hn' & Hm')".
iDestruct (own_valid_2 with "Hn' Hn")
as %[?%nat_included _]%auth_both_valid_discrete.
iDestruct (own_valid_2 with "Hm' Hm") as %?%mono_nat_both_valid.
iMod (own_update_2 with "Hn' Hn") as "Hnn'".
{ apply (auth_update_dealloc _ _ (n'-n)%nat), nat_local_update.
rewrite -plus_n_O. lia. }
iMod (own_update with "Hm'") as "Hm'n".
{ apply (mono_nat_update (m'+n)%nat); lia. }
iDestruct (own_mono _ _ (mono_nat_lb _) with "Hm'n") as "#$".
{ rewrite <-mono_nat_included. apply mono_nat_lb_mono. lia. }
iModIntro; iSplitL; [|done]. iExists _, _. iFrame.
rewrite (_:(n'+m')%nat = ((n'-n) + (m'+n))%nat); [done|lia].
Qed.
Lemma step_cumulative_time_receipt `{!invGS Σ} E n :
timeN E
time_ctx - time_interp n ={E, E∖↑timeN}= time_interp n
(time_interp (S n) ={E∖↑timeN, E}= time_interp (S n) ctime 1).
Proof.
iIntros (?) "#TIME Hn". iInv "TIME" as (n' m') ">(Hglob & Hn' & Hm')" "Hclose".
iDestruct (own_valid_2 with "Hn Hglob") as %?%mono_nat_both_valid.
iModIntro. iFrame. iIntros "HSn". unfold cumulative_time_receipt.
iMod (own_update with "Hn'") as "[HSn' $]".
{ apply auth_update_alloc, nat_local_update. by rewrite -plus_n_O. }
iDestruct (own_mono _ _ (mono_nat_lb _) with "HSn") as "#H'Sn".
{ apply mono_nat_included. }
iFrame. iApply "Hclose". iExists _, _. iFrame.
iApply (own_mono with "H'Sn"). apply mono_nat_lb_mono. lia.
Qed.
Lemma time_receipt_le `{!invGS Σ} E n m m' :
timeN E
time_ctx - time_interp n - ptime m - ctime m' ={E}=
m+m' n%nat time_interp n ctime m'.
Proof.
iIntros (?) "#TIME Hn Hm Hm'". iInv "TIME" as (m'0 m0) ">(Hglob & Hm'0 & Hm0)".
iDestruct (own_valid_2 with "Hn Hglob") as %?%mono_nat_both_valid.
iDestruct (own_valid_2 with "Hm0 Hm") as %?%mono_nat_both_valid.
iDestruct (own_valid_2 with "Hm'0 Hm'")
as %[?%nat_included _]%auth_both_valid_discrete.
iModIntro. iFrame. iSplitL; auto with iFrame lia.
Qed.
End time.
Lemma time_init `{!invGS Σ, !timePreGS Σ} E : timeN E
|={E}=> _ : timeGS Σ, time_ctx time_interp 0.
Proof.
intros ?.
iMod (own_alloc (mono_nat_auth 1 0 mono_nat_lb 0)) as (time_global_name) "[??]";
[by apply mono_nat_both_valid|].
iMod (own_alloc (mono_nat_auth 1 0)) as (time_persistent_name) "?";
[by apply mono_nat_auth_valid|].
iMod (own_alloc ( 0%nat)) as (time_cumulative_name) "?"; [by apply auth_auth_valid|].
iExists (TimeGS _ _ _ time_global_name time_persistent_name time_cumulative_name).
iFrame. iApply inv_alloc. iExists 0%nat, 0%nat. iFrame.
Qed.
Supports Markdown
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