Commit 9390d6a7 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Rebase on top of Iris step indexing branch

parent ece0bcb9
......@@ -34,6 +34,6 @@ Proof.
iModIntro. iExists NotStuck, _, [_], _, _. simpl.
iDestruct (Hwp (LRustG _ _ Hheap Htime) with "TIME") as "$".
iSplitL; first by auto with iFrame. iIntros ([|e' [|]]? -> ??) "//".
iIntros "[??] [?_] _". iApply fupd_mask_weaken; [done|]. iSplit; [|done].
iIntros (v2 t2'' [= -> <-]). by rewrite to_of_val.
iIntros "[??] [?_] _". iApply fupd_mask_weaken; [|iIntros "_ !>"]; [done|].
iSplit; [|done]. iIntros (v2 t2'' [= -> <-]). by rewrite to_of_val.
Qed.
......@@ -9,13 +9,13 @@ From lrust.lang Require Export lang.
Set Default Proof Using "Type".
Import uPred.
Definition lock_stateR : cmraT :=
Definition lock_stateR : cmra :=
csumR (exclR unitO) natR.
Definition heapUR : ucmraT :=
Definition heapUR : ucmra :=
gmapUR loc (prodR (prodR fracR lock_stateR) (agreeR valO)).
Definition heap_freeableUR : ucmraT :=
Definition heap_freeableUR : ucmra :=
gmapUR block (prodR fracR (gmapR Z (exclR unitO))).
Class heapG Σ := HeapG {
......
......@@ -274,12 +274,12 @@ Section arc.
{ apply auth_update_alloc, prod_local_update_1,
(op_local_update_discrete _ _ (Some (Cinl ((qq/2)%Qp, 1%positive, None))))
=>-[/= Hqa ?]. split;[split|]=>//=; last by rewrite left_id.
apply frac_valid'. rewrite -Hq comm_L.
apply frac_valid. rewrite -Hq comm_L.
by apply Qp_add_le_mono_l, Qp_div_le. }
iMod ("Hclose2" with "Hown") as "HP". iModIntro.
iMod ("Hclose1" with "[Hl Hw H● HP1']") as "_".
{ iExists _. iFrame. iExists _. rewrite /= [xH _]comm_L. iFrame.
rewrite [(qq / 2)%Qp _]comm frac_op' -[(_ + _)%Qp]assoc Qp_div_2 left_id_L. auto. }
rewrite [(qq / 2)%Qp _]comm frac_op -[(_ + _)%Qp]assoc Qp_div_2 left_id_L. auto. }
iModIntro. wp_case. iApply "HΦ". iFrame.
- wp_apply (wp_cas_int_fail with "Hl"); [congruence|]. iIntros "Hl".
iMod ("Hclose2" with "Hown") as "HP". iModIntro.
......@@ -405,10 +405,10 @@ Section arc.
{ apply auth_update_alloc. rewrite -[(_,0%nat)]right_id.
apply op_local_update_discrete=>Hv. constructor; last done.
split; last by rewrite /= left_id; apply Hv. split=>[|//].
apply frac_valid'. rewrite /= -Heq comm_L.
apply frac_valid. rewrite /= -Heq comm_L.
by apply Qp_add_le_mono_l, Qp_div_le. }
iFrame. iApply "Hclose1". iExists _. iFrame. iExists _. iFrame.
rewrite /= [xH _]comm_L frac_op' [(_ + c)%Qp]comm -[(_ + _)%Qp]assoc
rewrite /= [xH _]comm_L frac_op [(_ + c)%Qp]comm -[(_ + _)%Qp]assoc
Qp_div_2 left_id_L. auto with iFrame.
+ iIntros "Hl". iFrame. iApply ("Hclose1" with "[-]"). iExists _. iFrame.
iExists q. auto with iFrame.
......
......@@ -16,7 +16,7 @@ Program Instance lrustG_irisG `{!lrustG Σ} : irisG lrust_lang Σ := {
iris_invG := lrustG_invG;
state_interp σ stepcnt κs _ := (heap_ctx σ time_interp stepcnt)%I;
fork_post _ := True%I;
lsteps_per_pstep n := n
num_laters_per_step n := n
}.
Next Obligation.
intros. iIntros "/= [$ H]". by iMod (time_interp_step with "H") as "$".
......@@ -74,14 +74,17 @@ Implicit Types ef : option expr.
Lemma wp_step_fupdN_time_receipt n m E1 E2 e P Φ :
TCEq (to_val e) None E2 E1 timeN E1
time_ctx - n - m - (|={E1E2,}=> |={}=>^(S (n + m)) |={,E1E2}=> P) -
WP e @ E2 {{ v, m - P ={E1}= Φ v }} -
time_ctx - n -
(m ((|={E1E2,}=> |={}=>^(S (n + m)) |={,E1E2}=> P)
WP e @ E2 {{ v, P ={E1}= Φ v }})) -
WP e @ E1 {{ Φ }}.
Proof.
iIntros (???) "#TIME #Hn Hm HP Hwp".
iApply (wp_step_fupdN' with "[] Hm HP Hwp")=>//. iIntros (????) "Hm [_ Ht]".
iMod (time_receipt_le with "TIME Ht Hn Hm") as "[% ?]"=>//.
iApply fupd_mask_weaken; [set_solver+|]. iPureIntro. simpl. lia.
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 Φ :
......@@ -91,10 +94,8 @@ Lemma wp_step_fupdN_persistent_time_receipt n E1 E2 e P Φ :
WP e @ E1 {{ Φ }}.
Proof.
iIntros (???) "#TIME #Hn HP Hwp".
iApply (wp_step_fupdN_time_receipt _ _ E1 E2 with "TIME Hn [>] [HP] [Hwp]")=>//.
- by iMod cumulative_time_receipt_0 as "$".
- by rewrite -plus_n_O.
- iApply (wp_wand with "Hwp"). iIntros (?) "$". auto.
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 *)
......@@ -243,8 +244,7 @@ Proof.
iIntros (Φ) ">Hv HΦ". iApply wp_lift_head_step; auto.
iIntros (σ1 stepcnt κ κs n) "[Hσ Ht]".
iMod (heap_read_na with "Hσ Hv") as (m) "(% & Hσ & Hσclose)".
iMod (fupd_intro_mask' _ ) as "Hclose"; first set_solver.
iModIntro; iSplit; first by eauto.
iApply fupd_mask_intro; first set_solver. iIntros "Hclose". iSplit; first by eauto.
iNext; iIntros (e2 σ2 efs Hstep); inv_head_step. iMod "Hclose" as "_".
iMod (time_interp_step with "Ht") as "$". iIntros "!> {$Hσ}". iSplit; last done.
clear dependent σ1 n. iApply wp_lift_atomic_head_step_no_fork; auto.
......@@ -277,8 +277,7 @@ Proof.
iIntros (<- Φ) ">Hv HΦ".
iApply wp_lift_head_step; auto. iIntros (σ1 stepcnt κ κs n) "[Hσ Ht]".
iMod (heap_write_na with "Hσ Hv") as "(% & Hσ & Hσclose)".
iMod (fupd_intro_mask' _ ) as "Hclose"; first set_solver.
iModIntro; iSplit; first by eauto.
iApply (fupd_mask_intro _ ); first set_solver. iIntros "Hclose". iSplit; first by eauto.
iNext; iIntros (e2 σ2 efs Hstep); inv_head_step. iMod "Hclose" as "_".
iMod (time_interp_step with "Ht") as "$". iModIntro. iFrame "Hσ". iSplit; last done.
clear dependent σ1. iApply wp_lift_atomic_head_step_no_fork; auto.
......
From stdpp Require Import gmap.
From iris.program_logic Require Export hoare.
From iris.program_logic Require Import adequacy.
From lrust.lang Require Import tactics.
Set Default Proof Using "Type".
......
......@@ -84,7 +84,7 @@ Section time.
Proof. by rewrite /persistent_time_receipt -mono_nat_lb_op own_op. Qed.
Lemma cumulative_time_receipt_sep n m :
(n + m) n m.
Proof. by rewrite /cumulative_time_receipt -nat_op_plus auth_frag_op own_op. Qed.
Proof. by rewrite /cumulative_time_receipt -nat_op auth_frag_op own_op. Qed.
Lemma persistent_time_receipt_0 : |==> 0.
Proof. rewrite /persistent_time_receipt. apply own_unit. Qed.
......
......@@ -64,7 +64,7 @@ Section frac_bor.
- iLeft. iDestruct "Hφ" as (q) "(Hφ & Hγ & H)". iExists q. iFrame.
iIntros "!>Hφ". iApply "Hclose". iExists q. iFrame.
- iRight. iMod "Hclose" as "_". iMod (lft_incl_dead with "Hκκ' H†") as "$". done.
iApply fupd_intro_mask. set_solver. done.
iApply fupd_mask_subseteq. set_solver.
Qed.
Local Lemma frac_bor_trade1 γ κ' q :
......
......@@ -128,7 +128,7 @@ Proof.
iMod (slice_empty _ _ true with "Hs Hbox") as "[HP' Hbox]".
solve_ndisj. by rewrite lookup_fmap EQB.
iDestruct ("HPP'" with "HP'") as "$".
iMod fupd_intro_mask' as "Hclose"; last iIntros "!>HP'". solve_ndisj.
iApply fupd_mask_intro; [solve_ndisj|]. iIntros "Hclose HP'".
iDestruct ("HPP'" with "HP'") as "HP".
iMod "Hclose" as "_". iMod (slice_fill _ _ true with "Hs HP Hbox") as "Hbox".
solve_ndisj. by rewrite lookup_insert. iFrame.
......@@ -140,7 +140,7 @@ Proof.
iMod ("Hclose'" with "[-Hbor]") as "_".
+ iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''". eauto.
+ iMod (lft_incl_dead with "Hle H†"). done. iFrame.
iApply fupd_intro_mask'. solve_ndisj.
iApply fupd_mask_subseteq. solve_ndisj.
Qed.
(** Basic borrows *)
......@@ -234,7 +234,7 @@ Proof.
as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
iMod (slice_delete_full _ _ true with "Hs Hbox") as (Pb') "(HP' & EQ & Hbox)".
solve_ndisj. by rewrite lookup_fmap EQB. iDestruct ("HPP'" with "HP'") as "$".
iMod fupd_intro_mask' as "Hclose"; last iIntros "!>* HvsQ HQ". solve_ndisj.
iApply fupd_mask_intro; [solve_ndisj|]. iIntros "Hclose * HvsQ HQ".
iMod "Hclose" as "_". iDestruct (add_vs with "EQ Hvs [HvsQ]") as "Hvs".
{ iNext. iIntros "HQ H†". iApply "HPP'". iApply ("HvsQ" with "HQ H†"). }
iMod (slice_insert_full _ _ true with "HQ Hbox") as (j) "(% & #Hs' & Hbox)".
......@@ -259,6 +259,6 @@ Proof.
iMod ("Hclose'" with "[-Hbor]") as "_".
+ iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''". eauto.
+ iMod (lft_incl_dead with "Hle H†") as "$". done.
iApply fupd_intro_mask'. solve_ndisj.
iApply fupd_mask_subseteq. solve_ndisj.
Qed.
End accessors.
......@@ -94,7 +94,7 @@ Proof.
iExists Pb', Pi'. iFrame "Hvs' Hinh". rewrite /lft_bor_alive.
iExists (<[i:=Bor_in]>B'). rewrite /to_borUR !fmap_insert. iFrame.
rewrite -insert_delete big_sepM_insert ?lookup_delete //=. by iFrame. }
iModIntro. rewrite -[S n]Nat.add_1_l -nat_op_plus auth_frag_op own_cnt_op.
iModIntro. rewrite -[S n]Nat.add_1_l -nat_op auth_frag_op own_cnt_op.
by iFrame.
Qed.
......
......@@ -50,10 +50,10 @@ Section borrow.
[done..| |].
{ (* TODO : lemma for handling masks properly here. *)
rewrite difference_empty_L. iInduction depth3 as [|depth3] "IH"; simpl.
- iMod "H". iMod (fupd_intro_mask' ) as "Hclose"; [done|].
repeat iModIntro. iMod "Hclose" as "_". iApply "H".
- iMod "H". iMod (fupd_intro_mask' ) as "Hclose"; [done|].
iIntros "!> !> !>". iMod "Hclose" as "_". iMod "H". iApply ("IH" with "H"). }
- iMod "H". iApply fupd_mask_intro; [done|]. iIntros "Hclose !>!>!>!>!>!>".
iMod "Hclose" as "_". iApply "H".
- iMod "H". iApply fupd_mask_intro; [done|]. iIntros "Hclose !>!>!>".
iMod "Hclose" as "_". iMod "H". by iMod ("IH" with "H"). }
wp_seq. iIntros "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
rewrite /tctx_interp /= right_id. iExists _, _. iFrame "% Hshr".
iApply persistent_time_receipt_0.
......
......@@ -104,7 +104,9 @@ Section S.
Next Obligation.
intros. apply @limit_preserving.
- apply limit_preserving_entails; [solve_proper|].
intros ??? EQ. repeat (apply EQ || f_equiv).
intros ??? EQ. do 4 f_equiv; [do 2 f_equiv; apply EQ|].
induction depth as [|depth IH]; simpl; [|by rewrite IH].
do 2 f_equiv; apply EQ.
- intros n. by apply (Tn' _).(ty_share).
Qed.
Next Obligation.
......
......@@ -210,7 +210,7 @@ Section ofe.
- intros [[[[??] ?] ?] ?]. by constructor=>//;
eapply leibniz_equiv, (discrete_iff _ _).
Qed.
Canonical Structure typeO : ofeT := OfeT type type_ofe_mixin.
Canonical Structure typeO : ofe := Ofe type type_ofe_mixin.
Global Instance ty_size_ne n : Proper (dist n ==> eq) ty_size.
Proof. intros ?? EQ. apply EQ. Qed.
......@@ -286,7 +286,7 @@ Section ofe.
repeat eapply (EQ 0%nat) || f_equiv.
- split; apply EQ.
Qed.
Canonical Structure stO : ofeT := OfeT simple_type st_ofe_mixin.
Canonical Structure stO : ofe := Ofe simple_type st_ofe_mixin.
Global Instance st_own_ne n :
Proper (dist n ==> eq ==> eq ==> dist n) st_own.
......
Markdown is supported
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