Commit 3c36b147 authored by Dan Frumin's avatar Dan Frumin

Make some lemmas and tactics lamsubst-aware

- Twiggle with the burden of proof in log_related_arrow
- rel_rec_l/r returns a goal with an (unsimplified) lamsubst
  and can detect locked lambdas
- Fix some notational issues [hax.v]
- Rewrite the counter refinement proof to make greater use of lamsubst
parent 96aa3f7a
......@@ -68,7 +68,7 @@ Section CG_Counter.
{E1,E2;Γ} t log fill K (App (CG_increment (Loc x)) Unit) : τ.
Proof.
iIntros (?) "Hx Hlog".
unfold CG_increment. unlock.
unfold CG_increment. unlock; simpl.
rel_rec_r.
rel_rec_r.
rel_load_r.
......@@ -77,8 +77,6 @@ Section CG_Counter.
by iApply "Hlog".
Qed.
Global Opaque CG_increment.
Lemma CG_locked_increment_type Γ :
typed Γ CG_locked_increment (TArrow (Tref TNat) (TArrow LockType (TArrow TUnit TUnit))).
Proof.
......@@ -107,14 +105,6 @@ Section CG_Counter.
tp_rec j; tp_normalise j.
tp_apply j lock.steps_release with "Hl" as "$". (*TODO: remove steps_release from tactics.v *)
done.
(* tp_apply j (steps_with_lock _ _ _ K _ _ l _ _ UnitV UnitV) with "Hx Hl"; *)
(* last by iFrame. *)
(* { simpl. by rewrite decide_left. } *)
(* { iIntros (K') "#Hspec Hx Hj /=". *)
(* iApply fupd_trans. *)
(* iApply (steps_CG_increment E with "Hspec Hx"); auto. *)
(* tp_rec j; simpl. by rewrite !Closed_subst_id. *)
(* } *)
Qed.
Lemma bin_log_related_CG_locked_increment_r Γ K E1 E2 t τ x n l :
......@@ -123,7 +113,7 @@ Section CG_Counter.
(x ↦ₛ (#nv S n) - l ↦ₛ (#v false) -
({E1,E2;Γ} t log fill K (Lit Unit) : τ)) -
{E1,E2;Γ} t log fill K (((CG_locked_increment $/ (LocV x)) $/ (LocV l)) Unit)%E : τ)%I.
Proof.
Proof.
iIntros (?) "Hx Hl Hlog".
unfold CG_locked_increment. unlock. simpl.
rewrite !Closed_subst_id.
......@@ -138,8 +128,6 @@ Section CG_Counter.
by iApply "Hlog".
Qed.
Global Opaque CG_locked_increment.
Lemma counter_read_type Γ :
typed Γ counter_read (TArrow (Tref TNat) (TArrow TUnit TNat)).
Proof.
......@@ -162,8 +150,6 @@ Section CG_Counter.
by iFrame.
Qed.
Opaque counter_read.
Lemma CG_counter_body_type Γ :
typed Γ CG_counter_body
(TArrow (Tref TNat)
......@@ -225,8 +211,6 @@ Section CG_Counter.
by iApply "Hlog".
Qed.
Global Opaque FG_increment.
Lemma FG_counter_body_type Γ :
typed Γ FG_counter_body
(TArrow (Tref TNat)
......@@ -261,11 +245,10 @@ Section CG_Counter.
- {E1,E2;Γ} t log fill K (lamsubst counter_read (LocV x) #())%E : τ.
Proof.
iIntros "Hx Hlog".
Transparent counter_read. unfold counter_read. unlock. simpl.
unfold counter_read. unlock. simpl.
rel_rec_r.
rel_load_r.
by iApply "Hlog".
Opaque counter_read.
Qed.
(* A logically atomic specification for
......@@ -276,14 +259,12 @@ Section CG_Counter.
(( n, x ↦ᵢ (#nv n) R(n)) ={E2,E1}= True)
( m, x ↦ᵢ (#nv (S m)) R(m) -
{E2,E1;Γ} fill K (Lit Unit) log t : τ))
- ({E1,E1;Γ} fill K ((lamsubst FG_increment (LocV x)) Unit) log t : τ).
- ({E1,E1;Γ} fill K ((FG_increment $/ LocV x) Unit)%E log t : τ).
Proof.
iIntros "#H".
Transparent FG_increment. unfold FG_increment. unlock. simpl.
unfold FG_increment. unlock. simpl.
iLöb as "IH".
rel_rec_l.
Opaque FG_increment.
Opaque bin_log_related.
rel_bind_l (Load (Loc x)).
iPoseProof "H" as "H2". (* lolwhat *)
iApply (bin_log_related_load_l).
......@@ -322,54 +303,33 @@ Section CG_Counter.
(( n, x ↦ᵢ (#nv n) R(n)) ={E2,E1}= True)
( m, x ↦ᵢ (#nv m) R(m) -
{E2,E1;Γ} fill K (#n m) log t : τ))
- {E1,E1;Γ} fill K (lamsubst counter_read (LocV x) #())%E log t : τ.
- {E1,E1;Γ} fill K ((counter_read $/ LocV x) #())%E log t : τ.
Proof.
iIntros "#H".
Transparent counter_read. unfold counter_read. unlock. simpl.
unfold counter_read. unlock. simpl.
iApply (bin_log_related_rec_l _ E1 _); auto. iNext. simpl.
Opaque bin_log_related. (* TODO: why is this needed? *)
iApply (bin_log_related_load_l).
iMod "H" as (n) "[Hx [HR Hfin]]". iModIntro.
iExists _; iFrame "Hx".
iIntros "Hx".
rewrite ->uPred.and_elim_r. (* TODO: a tactic for this *)
iApply "Hfin". by iFrame.
Opaque counter_read.
Qed.
(* TODO: try to use with_lock rules *)
Lemma FG_CG_increment_refinement l cnt cnt' Γ :
inv counterN (counter_inv l cnt cnt') -
Γ FG_increment (Loc cnt) log CG_locked_increment (Loc cnt') (Loc l) : (TArrow TUnit TUnit).
Γ FG_increment $/ LocV cnt log CG_locked_increment $/ LocV cnt' $/ LocV l : TArrow TUnit TUnit.
Proof.
iIntros "#Hinv".
Transparent FG_increment.
unfold FG_increment. unlock.
iApply (bin_log_related_rec_l _ []); auto.
iNext. simpl.
Transparent CG_locked_increment.
unfold CG_locked_increment. unlock.
rel_rec_r.
rel_rec_r.
iApply bin_log_related_arrow.
{ unfold FG_increment. unlock; simpl. reflexivity. }
{ unfold CG_locked_increment. unlock; simpl. reflexivity. }
{ unfold FG_increment. unlock; simpl. solve_closed. (* TODO: add a clause to the reflection mechanism that reifies a [lambdasubst] expression as a closed one *) }
{ unfold CG_locked_increment. unlock; simpl.
rewrite !Closed_subst_id. solve_closed. }
iAlways. iIntros (Δ [v v']) "[% %]"; simpl in *; subst. clear Δ.
(* :( *)
replace (rec: "inc" <>
:= (λ: "c",
if: CAS #cnt "c" (BinOp Add (Nat 1) "c") then #() else "inc" #())
! #cnt)%E with (lamsubst FG_increment (LocV cnt)); last first.
{ unfold FG_increment. unlock. reflexivity. }
Opaque FG_increment.
replace (λ: <>,
acquire #l ;; (CG_increment #cnt') #() ;; release #l)%E
with (lamsubst (lamsubst CG_locked_increment (LocV cnt')) (LocV l)); last first.
{ unfold CG_locked_increment. unlock. simpl.
rewrite !Closed_subst_id. reflexivity. }
Opaque CG_locked_increment.
iApply (bin_log_FG_increment_logatomic (fun n => (l ↦ₛ (#v false)) cnt' ↦ₛ #nv n)%I _ _ _ [] cnt with "[Hinv]").
iAlways.
iInv counterN as ">Hcnt" "Hcl". iModIntro.
......@@ -391,22 +351,15 @@ Section CG_Counter.
Lemma counter_read_refinement l cnt cnt' Γ :
inv counterN (counter_inv l cnt cnt') -
Γ counter_read #cnt log counter_read #cnt' : TArrow TUnit TNat.
Γ counter_read $/ #cnt log counter_read $/ #cnt' : TArrow TUnit TNat.
Proof.
iIntros "#Hinv".
Transparent counter_read.
unfold counter_read. unlock.
rel_rec_r.
rel_rec_l.
iApply bin_log_related_arrow. iAlways.
iIntros (Δ [v v']) "[% %]"; simpl in *; subst. clear Δ.
(* :( *)
replace (λ: <>, ! #cnt)%E
with (lamsubst counter_read (LocV cnt)); last first.
{ unfold counter_read. unlock. reflexivity. }
replace (λ: <>, ! #cnt')%E
with (lamsubst counter_read (LocV cnt')); last first.
{ unfold counter_read. unlock. reflexivity. }
iApply bin_log_related_arrow.
{ unfold counter_read. unlock. simpl. reflexivity. }
{ unfold counter_read. unlock. simpl. reflexivity. }
{ unfold counter_read. unlock. simpl. solve_closed. }
{ unfold counter_read. unlock. simpl. solve_closed. }
iAlways. iIntros (Δ [v v']) "[% %]"; simpl in *; subst. clear Δ.
iApply (bin_log_counter_read_atomic_l (fun n => (l ↦ₛ (#v false)) cnt' ↦ₛ #nv n)%I _ _ _ [] cnt with "[Hinv]").
iAlways. iInv counterN as (n) "[>Hl [>Hcnt >Hcnt']]" "Hclose".
iModIntro.
......@@ -420,9 +373,9 @@ Section CG_Counter.
iIntros "Hcnt'".
iMod ("Hclose" with "[Hl Hcnt Hcnt']"); simpl.
{ iNext. iExists _. by iFrame. }
iApply (bin_log_related_val); intros; simpl; eauto.
iApply bin_log_related_val; intros; simpl; eauto.
Qed.
Lemma FG_CG_counter_refinement :
FG_counter log CG_counter : TProd (TArrow TUnit TUnit) (TArrow TUnit TNat).
Proof.
......@@ -434,7 +387,7 @@ Section CG_Counter.
rel_alloc_r as cnt' "Hcnt'".
rel_bind_l (Alloc _).
iApply (bin_log_related_alloc_l); auto; simpl. iModIntro.
iIntros (cnt) "Hcnt".
iIntros (cnt) "Hcnt".
rel_rec_r.
......@@ -451,8 +404,18 @@ Section CG_Counter.
iMod (inv_alloc counterN with "[Hinv]") as "#Hinv"; trivial.
iApply (bin_log_related_pair _ with "[]").
- iApply (FG_CG_increment_refinement with "Hinv").
- iApply (counter_read_refinement with "Hinv").
- rel_rec_l.
rel_rec_r.
unfold CG_locked_increment. unlock; simpl. rewrite !Closed_subst_id.
rel_rec_r.
replace (λ: <>, acquire #l ;; (CG_increment #cnt') #() ;; release #l)%E
with (CG_locked_increment $/ LocV cnt' $/ LocV l)%E.
iApply (FG_CG_increment_refinement with "Hinv").
{ unfold CG_locked_increment. unlock; simpl.
rewrite !Closed_subst_id. reflexivity. }
- rel_rec_l.
rel_rec_r.
iApply (counter_read_refinement with "Hinv").
Qed.
End CG_Counter.
......
......@@ -132,6 +132,11 @@ Section Refinement.
(* iIntros "Hx". *)
(* simpl. *)
(* rewrite ->uPred.and_elim_l. *)
Definition choice_inv' y y' x x' : iProp Σ :=
(( f, y ↦ᵢ (#v f) y' ↦ₛ (#v f))
( n, x ↦ᵢ (#nv n) x' ↦ₛ (#nv n)))%I.
Lemma prerefinement Γ x x' n ρ :
(spec_ctx ρ - x ↦ᵢ (#nv n) - x' ↦ₛ (#nv n) -
......@@ -193,7 +198,7 @@ Section Refinement.
Proof.
iIntros "#Hspec".
unfold lateChoice in *. unfold earlyChoice in *. unlock.
iApply bin_log_related_arrow.
iApply bin_log_related_arrow; eauto.
iAlways. iIntros (Δ (l,l')) "Hxx'". simpl.
iDestruct "Hxx'" as ([x x']) "[% #Hxx']". inversion H1; subst. simpl.
replace (λ: "x", "x" <- Nat 0 ;; rand #())%E
......@@ -203,6 +208,5 @@ Section Refinement.
with (of_val earlyChoice); last first.
{ unfold earlyChoice. unlock. reflexivity. }
Abort.
(* iApply prerefinement; eauto. *)
End Refinement.
......@@ -9,7 +9,8 @@ Definition lamsubst (e : expr) (v : val) : expr :=
| _ => e
end.
Notation "e $/ v" := (lamsubst e%E v%V) (at level 80) : expr_scope.
Notation "e $/ v" := (lamsubst e%E v%V) (at level 71, left associativity) : expr_scope.
(* ^ this should be left associative at a level lower than that of `bin_log_related` *)
Ltac inv_head_step :=
repeat match goal with
......@@ -28,15 +29,17 @@ Section hax.
Notation D := (prodC valC valC -n> iProp Σ).
Implicit Types Δ : listC D.
Lemma bin_log_related_arrow Γ E (f x f' x' : binder) (e e' : expr) (τ τ' : type)
(Hclosed : Closed (rec: f x := e)%E )
(Hclosed' : Closed (rec: f' x' := e')%E) :
Lemma bin_log_related_arrow Γ E (f x f' x' : binder) (e e' eb eb' : expr) (τ τ' : type) :
e = (rec: f x := eb)%E
e' = (rec: f' x' := eb')%E
Closed e
Closed e'
( Δ vv, τ Δ vv -
Γ App (Rec f x e) (of_val (vv.1)) log App (Rec f' x' e') (of_val (vv.2)) : τ') -
{E,E;Γ} (Rec f x e) log (Rec f' x' e') : TArrow τ τ'.
Γ App e (of_val (vv.1)) log App e' (of_val (vv.2)) : τ') -
{E,E;Γ} e log e' : TArrow τ τ'.
Proof.
iIntros "#H".
iIntros (????) "#H".
subst e e'.
rewrite bin_log_related_eq.
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj".
cbn-[subst_p].
......@@ -45,17 +48,17 @@ Section hax.
iApply wp_value.
{ simpl. erewrite decide_left. done. }
rewrite /env_subst Closed_subst_p_id.
iExists (RecV f' x' e').
iExists (RecV f' x' eb').
iFrame "Hj". iAlways. iIntros (vv) "Hvv".
iSpecialize ("H" $! Δ vv with "Hvv").
iSpecialize ("H" $! Δ with "Hs []").
{ iAlways. iApply "HΓ". }
Unshelve. all: trivial.
assert (Closed ((rec: f x := e) (vv.1))%E).
{ revert Hclosed. unfold Closed. simpl.
assert (Closed ((rec: f x := eb) (vv.1))%E).
{ unfold Closed in *. simpl.
intros. split_and?; auto. apply of_val_closed. }
assert (Closed ((rec: f' x' := e') (vv.2))%E).
{ revert Hclosed'. unfold Closed. simpl.
assert (Closed ((rec: f' x' := eb') (vv.2))%E).
{ unfold Closed in *. simpl.
intros. split_and?; auto. apply of_val_closed. }
rewrite /env_subst. rewrite !Closed_subst_p_id. done.
Qed.
......
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import coq_tactics sel_patterns.
From iris.proofmode Require Export tactics.
From iris_logrel.F_mu_ref_conc Require Import rules rules_binary.
From iris_logrel.F_mu_ref_conc Require Import rules rules_binary hax.
From iris_logrel.F_mu_ref_conc Require Export lang tactics logrel_binary relational_properties.
Set Default Proof Using "Type".
Import lang.
Lemma of_val_unlock v e : of_val v = e of_val (locked v) = e.
Proof. by unlock. Qed.
(* Applied to goals that are equalities of expressions. Will try to unlock the
LHS once if necessary, to get rid of the lock added by the syntactic sugar. *)
Ltac solve_of_val_unlock := try apply of_val_unlock; fast_done.
Lemma tac_rel_bind_gen `{heapIG Σ, !cfgSG Σ} Δ E1 E2 Γ e e' t t' τ :
e = e'
......@@ -78,13 +84,16 @@ Lemma tac_rel_rec_l `{heapIG Σ, !cfgSG Σ} Δ E1 Γ e K' f x ef e' efbody v ere
ef = Rec f x efbody
Closed (x :b: f :b: ) efbody
to_val e' = Some v
eres = subst' f ef (subst' x e' efbody)
eres = lamsubst ef v
(Δ bin_log_related E1 E1 Γ (fill K' eres) t τ)
(Δ bin_log_related E1 E1 Γ e t τ).
Proof.
intros ??????.
subst e ef eres.
rewrite -(bin_log_related_rec_l Γ E1); eassumption.
intros ????.
subst ef. simpl.
intros ?.
subst e eres.
rewrite -(bin_log_related_rec_l Γ E1); last by eassumption.
destruct f; simpl; rewrite (of_to_val e' v); eauto.
Qed.
Tactic Notation "rel_rec_l" :=
......@@ -93,8 +102,8 @@ Tactic Notation "rel_rec_l" :=
match eval hnf in e' with App ?e1 ?e2 =>
eapply (tac_rel_rec_l _ _ _ _ _ _ _ e1 e2);
[tac_bind_helper (* e = fill K' _ *)
|simpl; fast_done
|solve_closed
|solve_of_val_unlock
|try solve_closed
|fast_done (* to_val e' = Some v *)
|try fast_done (* eres = subst ... *)
|simpl; rewrite ?Closed_subst_id; iNext (* new goal *)]
......@@ -576,17 +585,20 @@ Tactic Notation "rel_cas_suc_r" :=
Lemma tac_rel_rec_r `{heapIG Σ, !cfgSG Σ} Δ E1 E2 Γ e K' f x ef e' efbody v eres t τ :
nclose specN E1
e = fill K' (App (Rec f x efbody) e')
e = fill K' (App ef e')
ef = Rec f x efbody
Closed (x :b: f :b: ) efbody
to_val e' = Some v
eres = subst' f ef (subst' x e' efbody)
eres = lamsubst ef v
(Δ bin_log_related E1 E2 Γ t (fill K' eres) τ)
(Δ bin_log_related E1 E2 Γ t e τ).
Proof.
intros ???????.
subst e ef eres.
rewrite -(bin_log_related_rec_r Γ E1 E2); eassumption.
intros ????.
subst ef. simpl.
intros ??.
subst e eres.
rewrite -(bin_log_related_rec_r Γ E1); try eassumption.
destruct f; simpl; rewrite (of_to_val e' v); eauto.
Qed.
Tactic Notation "rel_rec_r" :=
......@@ -596,8 +608,8 @@ Tactic Notation "rel_rec_r" :=
eapply (tac_rel_rec_r _ _ _ _ _ _ _ _ e1 e2);
[solve_ndisj || fail "rel_rec_r: cannot prove 'nclose specN ⊆ ?'"
|tac_bind_helper (* e = fill K' _ *)
|simpl; fast_done
|solve_closed
|solve_of_val_unlock
|try solve_closed
|fast_done (* to_val e' = Some v *)
|try fast_done (* eres = subst ... *)
|simpl; rewrite ?Closed_subst_id (* new goal *)]
......
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