Commit b6ec12b4 authored by Amin Timany's avatar Amin Timany

Finish binary fundamental lemma for Fμ,ref,par

We still need to prove the many admitted lemmas in rules_binary module.
parent 24464222
......@@ -74,8 +74,7 @@ Section typed_interp.
Lemma typed_binary_interp N Δ Γ vs e τ
(HNLdisj : l : loc * loc, N L .@ l)
(HSLdisj : l : loc * loc, N L .@ l)
(HSNdisj : S N)
(HSLdisj : l : loc * loc, S L .@ l)
(Htyped : typed Γ e τ)
(HΔ : context_interp_Persistent Δ)
: List.length Γ = List.length vs
......@@ -132,12 +131,12 @@ Section typed_interp.
smart_wp_bind (InjLCtx) v v' "[Hv #Hiv]"
(IHHtyped _ _ _ _ _ j (K ++ [InjLCtx])); cbn.
value_case. iExists (InjLV v'); iFrame "Hv".
iLeft; iExists _; iSplit; [|iNext; eauto]; simpl; trivial.
iLeft; iExists _; iSplit; [|eauto]; simpl; trivial.
- (* injr *)
smart_wp_bind (InjRCtx) v v' "[Hv #Hiv]"
(IHHtyped _ _ _ _ _ j (K ++ [InjRCtx])); cbn.
value_case. iExists (InjRV v'); iFrame "Hv".
iRight; iExists _; iSplit; [|iNext; eauto]; simpl; trivial.
iRight; iExists _; iSplit; [|eauto]; simpl; trivial.
- (* case *)
smart_wp_bind (CaseCtx _ _) v v' "[Hv #Hiv]"
(IHHtyped1 _ _ _ _ _ j (K ++ [CaseCtx _ _])); cbn.
......@@ -322,45 +321,49 @@ Section typed_interp.
(IHHtyped3
_ _ _ _ _ j (K ++ [CasRCtx _ _])).
iDestruct "Hiv" as {l} "[% Hinv]".
inversion H; subst.
inversion H0; subst.
iApply wp_atomic; trivial;
[cbn; eauto 10 using to_of_val|].
iPvsIntro.
iInv (L .@ l) as {z} "[Hw1 [Hw2 #Hw3]]".
eapply bool_decide_spec; eauto 10 using to_of_val.
destruct (val_dec_eq u w) as [|Hneq]; subst.
destruct z as [z1 z2]; simpl.
destruct (val_dec_eq z1 w) as [|Hneq]; subst.
+ iPvs (step_cas_suc _ _ _ j K (l.2) (# w') w' (# u') u' _ _ _
with "[Hu Hw2]") as "[Hw Hw2]".
iFrame "Hspec Hu".
smart_wp_bind (CasLCtx _ _) v1 "#Hv1" IHHtyped1; cbn.
smart_wp_bind (CasMCtx _ _) v2 "#Hv2" IHHtyped2; cbn.
smart_wp_bind (CasRCtx _ _) v3 "#Hv3" IHHtyped3; cbn. iClear "HΓ".
iDestruct "Hv1" as {l} "[% Hinv]"; subst.
iApply wp_atomic; cbn; eauto 10 using to_of_val.
iPvsIntro.
iInv (L .@ l) as {w} "[Hw1 #Hw2]"; [cbn; eauto 10 using to_of_val|].
destruct (val_dec_eq v2 w) as [|Hneq]; subst.
+ iApply (wp_cas_suc N); eauto using to_of_val.
with "[Hu Hw2]") as "[Hw Hw2]"; simpl.
{ iFrame "Hspec Hu". iNext.
rewrite ?EqType_related_eq; trivial.
iDestruct "Hiw" as "%". iDestruct "Hw3" as "%".
repeat subst; trivial. }
iApply (wp_cas_suc N); eauto using to_of_val.
specialize (HNLdisj l); set_solver_ndisj.
iFrame "Hheap Hw1".
iNext. iIntros "Hw1".
iSplitL.
* iNext; iExists _; iSplitL; trivial.
* iPvsIntro. iLeft; iExists _; auto with itauto.
+ iApply (wp_cas_fail N); eauto using to_of_val.
iSplitL "Hw1 Hw2".
* iNext; iExists (_, _); iFrame "Hw1 Hw2"; trivial.
* iPvsIntro. iExists TRUEV; iFrame "Hw".
iLeft; iExists (UnitV, UnitV); auto with itauto.
+ iPvs (step_cas_fail _ _ _ j K (l.2) 1 (z2) (# w') w' (# u') u' _ _ _
with "[Hu Hw2]") as "[Hw Hw2]"; simpl.
{ iFrame "Hspec Hu Hw2". iNext.
rewrite ?EqType_related_eq; trivial.
iDestruct "Hiw" as "%". iDestruct "Hw3" as "%".
repeat subst; trivial. }
iApply (wp_cas_fail N); eauto using to_of_val.
clear Hneq. specialize (HNLdisj l); set_solver_ndisj.
(* Weird that Hneq above makes set_solver_ndisj diverge or
take exceptionally long!?!? *)
iFrame "Hheap Hw1".
iNext. iIntros "Hw1".
iSplitL.
* iNext; iExists _; iSplitL; trivial.
* iPvsIntro. iRight; iExists _; auto with itauto.
(* unshelving *)
Unshelve.
cbn; typeclasses eauto.
iSplitL "Hw1 Hw2".
* iNext; iExists (_, _); iFrame "Hw1 Hw2"; trivial.
* iPvsIntro. iExists FALSEV; iFrame "Hw".
iRight; iExists (UnitV, UnitV); auto with itauto.
(* unshelving... *)
Unshelve.
all: auto using to_of_val.
simpl; typeclasses eauto.
all: clear - HSLdisj; specialize (HSLdisj l); set_solver_ndisj.
Qed.
End typed_interp.
\ No newline at end of file
......@@ -7,6 +7,7 @@ From iris.program_logic Require Export lifting.
From iris.algebra Require Import upred_big_op frac dec_agree.
From iris.program_logic Require Export invariants ghost_ownership.
From iris.program_logic Require Import ownership auth.
Require Import iris.proofmode.pviewshifts.
Import uPred.
(** interp : is a unary logical relation. *)
......@@ -105,7 +106,7 @@ Section logrel.
{|
cofe_mor_car :=
λ w, ( w1 w2, w = (PairV (w1.1) (w1.2), PairV (w2.1) (w2.2))
τ1i (w1.1, w2.1) τ2i (w1.2, w2.2))%I
τ1i (w1.1, w2.1) τ2i (w1.2, w2.2))%I
|}
|}
|}.
......@@ -137,8 +138,8 @@ Section logrel.
λ τ2i,
{|
cofe_mor_car :=
λ w, (( w1, w = (InjLV (w1.1), InjLV (w1.2)) τ1i w1)
( w2, w = (InjRV (w2.1), InjRV (w2.2)) τ2i w2))%I
λ w, (( w1, w = (InjLV (w1.1), InjLV (w1.2)) τ1i w1)
( w2, w = (InjRV (w2.1), InjRV (w2.2)) τ2i w2))%I
|}
|}
|}.
......@@ -668,4 +669,28 @@ Section logrel.
- apply IHΓ.
Qed.
Lemma EqType_related_eq τ {H : EqType τ} v v' Δ
{HΔ : context_interp_Persistent Δ} :
interp τ Δ (v, v') (v = v').
Proof.
revert v v'; induction H => v v'; iIntros "#H1".
- simpl; iDestruct "H1" as "[% %]"; subst; trivial.
- iDestruct "H1" as {w1 w2} "[% [H1 H2]]".
destruct w1; destruct w2; simpl in *.
inversion H1; subst.
rewrite IHEqType1 IHEqType2.
iDestruct "H1" as "%". iDestruct "H2" as "%". subst; trivial.
- iDestruct "H1" as "[H1|H1]".
+ iDestruct "H1" as {w} "[% H1]".
destruct w; simpl in *.
inversion H1; subst.
rewrite IHEqType1.
iDestruct "H1" as "%". subst; trivial.
+ iDestruct "H1" as {w} "[% H1]".
destruct w; simpl in *.
inversion H1; subst.
rewrite IHEqType2.
iDestruct "H1" as "%". subst; trivial.
Qed.
End logrel.
\ No newline at end of file
......@@ -321,16 +321,21 @@ Section lang_rules.
Admitted.
Lemma step_cas_fail N E ρ j K l q v' e1 v1 e2 v2:
to_val e1 = Some v1 to_val e2 = Some v2 v' v1 nclose N E
((Spec_ctx N ρ j (fill K (CAS (Loc l) e1 e2)) l ↦ₛ{q} v')%I)
|={E}=>(j (fill K (FALSE)) l ↦ₛ{q} v')%I.
to_val e1 = Some v1 to_val e2 = Some v2 nclose N E
((Spec_ctx N ρ j (fill K (CAS (Loc l) e1 e2))
( (v' v1)) l ↦ₛ{q} v')%I)
|={E}=>(j (fill K (FALSE)) l ↦ₛ{q} v')%I.
Proof.
iIntros {H1 H2 H3} "[#Hinv [Hj [#Heq Hpt]]]".
unfold Spec_ctx, auth_ctx, tpool_mapsto, auth_own.
iInv> N as {ρ'} "[Hown #Hstep]".
iTimeless "Heq". iDestruct "Heq" as "%".
Admitted.
Lemma step_cas_suc N E ρ j K l e1 v1 e2 v2:
to_val e1 = Some v1 to_val e2 = Some v2 nclose N E
((Spec_ctx N ρ j (fill K (CAS (Loc l) e1 e2)) l ↦ₛ v1)%I)
|={E}=>(j (fill K (TRUE)) l ↦ₛ v2)%I.
((Spec_ctx N ρ j (fill K (CAS (Loc l) e1 e2)) l ↦ₛ v1)%I)
|={E}=>(j (fill K (TRUE)) l ↦ₛ v2)%I.
Proof.
Admitted.
......
......@@ -17,6 +17,12 @@ Instance Rename_type : Rename type. derive. Defined.
Instance Subst_type : Subst type. derive. Defined.
Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
Inductive EqType : type Prop :=
| EqTUnit : EqType TUnit
| EqTProd τ τ' : EqType τ EqType τ' EqType (TProd τ τ')
| EqSum τ τ' : EqType τ EqType τ' EqType (TSum τ τ')
.
Notation TBOOL := (TSum TUnit TUnit).
Inductive typed (Γ : list type) : expr type Prop :=
......@@ -51,6 +57,7 @@ Inductive typed (Γ : list type) : expr → type → Prop :=
| TStore e e' τ :
typed Γ e (Tref τ) typed Γ e' τ typed Γ (Store e e') TUnit
| TCAS e1 e2 e3 τ :
EqType τ
typed Γ e1 (Tref τ) typed Γ e2 τ typed Γ e3 τ
typed Γ (CAS e1 e2 e3) TBOOL
.
......
......@@ -21,4 +21,5 @@ F_mu_ref_par/typing.v
F_mu_ref_par/logrel_unary.v
F_mu_ref_par/fundamental_unary.v
F_mu_ref_par/rules_binary.v
F_mu_ref_par/logrel_binary.v
\ No newline at end of file
F_mu_ref_par/logrel_binary.v
F_mu_ref_par/fundamental_binary.v
\ No newline at end of file
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