Commit fdb975a5 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump Iris (⊢ changes).

parent 03c65e92
......@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
depends: [
"coq-iris" { (= "dev.2020-01-23.2.e2f65bbd") | (= "dev") }
"coq-iris" { (= "dev.2020-03-16.0.62be0a86") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
......@@ -32,7 +32,7 @@ Section bit_refinement.
( b : bool, v1 = #b v2 = #(bitf b)))%I.
Lemma bit_refinement Δ :
REL bit_bool << bit_nat : interp bitτ Δ.
REL bit_bool << bit_nat : interp bitτ Δ.
Proof.
unfold bit_bool, bit_nat.
unfold bitτ. simpl.
......
......@@ -56,7 +56,7 @@ Section cell_refinement.
cellInt R r1 r2 r3 l r)%I.
Lemma cell2_cell1_refinement :
REL cell2 << cell1 : α, β, (α β) * (β α) * (β α ()).
REL cell2 << cell1 : α, β, (α β) * (β α) * (β α ()).
Proof.
unfold cell1, cell2.
iApply refines_forall. iIntros "!#" (R).
......
......@@ -64,7 +64,7 @@ Section proofs.
(b:bool), cl SOMEV #b ce ↦ₛ #b))%I.
Lemma coin_lazy'_eager_refinement :
REL coin2' << coin1 : (() lrel_bool) * (() ()).
REL coin2' << coin1 : (() lrel_bool) * (() ()).
Proof.
unfold coin1, coin2'.
rel_rec_r. rel_alloc_r ce as "Hce". do 2 rel_pure_r.
......@@ -120,7 +120,7 @@ Section proofs.
(** Eager coin refines lazy coin (with prophecies).
This part is easier. *)
Lemma coin_eager_lazy'_refinement :
REL coin1 << coin2' : (() lrel_bool) * (() ()).
REL coin1 << coin2' : (() lrel_bool) * (() ()).
Proof.
unfold coin1, coin2'.
rel_rec_l. rel_alloc_l ce as "Hce". do 2 rel_pure_l.
......@@ -179,7 +179,7 @@ Section proofs.
(** Finally we show that we can get rid of prophecy instrumentation. *)
Lemma coin_lazy'_lazy_refinement :
REL coin2' << coin2 : (() lrel_bool) * (() ()).
REL coin2' << coin2 : (() lrel_bool) * (() ()).
Proof.
unfold coin2, coin2'.
rel_rec_l. rel_pure_l. rel_alloc_l c' as "Hc'".
......@@ -239,7 +239,7 @@ Section proofs.
Qed.
Lemma coin_lazy_lazy'_refinement :
REL coin2 << coin2' : (() lrel_bool) * (() ()).
REL coin2 << coin2' : (() lrel_bool) * (() ()).
Proof.
unfold coin2, coin2'.
rel_rec_l. rel_pure_l. rel_alloc_l c as "Hc".
......
......@@ -69,7 +69,7 @@ Section proof.
end.
Lemma late'_early_choice :
REL lateChoice' << earlyChoice : ref lrel_int lrel_bool.
REL lateChoice' << earlyChoice : ref lrel_int lrel_bool.
Proof.
unfold lateChoice', earlyChoice.
iApply refines_arrow_val.
......@@ -91,7 +91,7 @@ Section proof.
Qed.
Lemma early_late_choice :
REL earlyChoice << lateChoice : ref lrel_int lrel_bool.
REL earlyChoice << lateChoice : ref lrel_int lrel_bool.
Proof.
unfold lateChoice, earlyChoice.
iApply refines_arrow_val.
......@@ -108,7 +108,7 @@ Section proof.
Qed.
Lemma late_late'_choice :
REL lateChoice << lateChoice' : ref lrel_int lrel_bool.
REL lateChoice << lateChoice' : ref lrel_int lrel_bool.
Proof.
unfold lateChoice, lateChoice'.
iApply refines_arrow_val.
......
......@@ -39,7 +39,7 @@ Section namegen_refinement.
end)%I.
Lemma nameGen_ref1 :
REL nameGen1 << nameGen2 : α, (() α) * (α α lrel_bool).
REL nameGen1 << nameGen2 : α, (() α) * (α α lrel_bool).
Proof.
unfold nameGen1, nameGen2.
rel_alloc_r c as "Hc".
......
......@@ -188,7 +188,7 @@ Section proof.
inv (stackN .@ (stk,stk')) (sinv A stk stk' l))%I.
Lemma stack_refinement :
REL FG_stack << CG_stack : A, B, (() B) * (B () + A) * (B A ()).
REL FG_stack << CG_stack : A, B, (() B) * (B () + A) * (B A ()).
Proof.
unfold CG_stack, FG_stack.
iApply refines_forall. iIntros (A). iAlways.
......
......@@ -87,7 +87,7 @@ Section rules.
Qed.
Lemma conjure_0 :
(|==> own γ ( (O : mnat)))%I.
|==> own γ ( (O : mnat)).
Proof. by apply own_unit. Qed.
Lemma inc_size (n : nat) :
......@@ -117,7 +117,7 @@ Section proof.
Context `{!relocG Σ, !msizeG Σ, !lockG Σ}.
Lemma eqKey_refinement γ :
REL eqKey << eqKey : tableR γ tableR γ lrel_bool.
REL eqKey << eqKey : tableR γ tableR γ lrel_bool.
Proof.
unfold eqKey.
iApply refines_arrow_val.
......@@ -216,7 +216,7 @@ Section proof.
Qed.
Lemma refinement1 :
REL symbol1 << symbol2 : () lrel_symbol.
REL symbol1 << symbol2 : () lrel_symbol.
Proof.
iApply refines_arrow_val.
iAlways. iIntros (? ?) "[% %]"; simplify_eq/=.
......@@ -295,7 +295,7 @@ Section proof.
Qed.
Lemma refinement2 :
REL symbol2 << symbol1 : () lrel_symbol.
REL symbol2 << symbol1 : () lrel_symbol.
Proof.
iApply refines_arrow_val.
iAlways. iIntros (? ?) "[% %]"; simplify_eq/=.
......
......@@ -49,7 +49,7 @@ Section refinement.
set_solver.
Qed.
Lemma newIssuedTickets : (|==> γ, issuedTickets γ 0)%I.
Lemma newIssuedTickets : |==> γ, issuedTickets γ 0.
Proof.
iMod (own_alloc ( (GSet ))) as (γ) "Hγ"; [|by eauto].
by apply auth_auth_valid.
......@@ -102,7 +102,7 @@ Section refinement.
(* Allocating a new lock *)
Lemma newlock_refinement :
REL newlock << reloc.lib.lock.newlock : () lockInt.
REL newlock << reloc.lib.lock.newlock : () lockInt.
Proof.
rel_arrow_val.
iIntros (? ?) "/= [% %]"; simplify_eq.
......@@ -207,7 +207,7 @@ Section refinement.
Qed.
Lemma acquire_refinement :
REL acquire << reloc.lib.lock.acquire : lockInt ().
REL acquire << reloc.lib.lock.acquire : lockInt ().
Proof.
rel_arrow_val.
iIntros (? lk) "/= #Hl".
......@@ -239,7 +239,7 @@ Section refinement.
Qed.
Lemma acquire_refinement_direct :
REL acquire << reloc.lib.lock.acquire : lockInt ().
REL acquire << reloc.lib.lock.acquire : lockInt ().
Proof.
rel_arrow_val.
iIntros (? ?) "/= #Hl".
......@@ -305,7 +305,7 @@ Section refinement.
Qed.
Lemma release_refinement :
REL release << reloc.lib.lock.release : lockInt ().
REL release << reloc.lib.lock.release : lockInt ().
Proof.
rel_arrow_val.
iIntros (? lk) "/= #Hl".
......@@ -339,7 +339,7 @@ Section refinement.
Qed.
Lemma ticket_lock_refinement :
REL (newlock, acquire, release)
REL (newlock, acquire, release)
<<
(reloc.lib.lock.newlock, reloc.lib.lock.acquire, reloc.lib.lock.release)
: lrel_lock.
......
......@@ -17,7 +17,7 @@ Section proofs.
Context `{relocG Σ}.
Lemma refinement1 :
REL
REL
let: "x" := ref #1 in
(λ: "f", "f" #();; !"x")
<<
......@@ -43,7 +43,7 @@ Section proofs.
Definition pending γ `{oneshotG Σ} := own γ (Cinl (Excl ())).
Definition shot γ `{oneshotG Σ} := own γ (Cinr (to_agree ())).
Lemma new_pending `{oneshotG Σ} : (|==> γ, pending γ)%I.
Lemma new_pending `{oneshotG Σ} : |==> γ, pending γ.
Proof. by apply own_alloc. Qed.
Lemma shoot γ `{oneshotG Σ} : pending γ == shot γ.
Proof.
......@@ -61,7 +61,7 @@ Section proofs.
Qed.
Lemma refinement2 `{oneshotG Σ} :
REL
REL
let: "x" := ref #0 in
(λ: "f", "x" <- #1;; "f" #();; !"x")
<<
......@@ -113,7 +113,7 @@ Section proofs.
Qed.
Lemma refinement25 `{oneshotG Σ} :
REL
REL
(λ: "f", "f" #();; #1)
<<
(let: "x" := ref #0 in
......@@ -164,7 +164,7 @@ Section proofs.
Definition i3n := nroot .@ "i3".
Lemma refinement3 :
REL
REL
let: "b" := ref #true in
let: "x" := ref #0 in
(λ: "f", if: CAS "b" #true #false
......@@ -269,7 +269,7 @@ Section proofs.
Without locking in the first expression, the callback can reenter
the body in a forked thread to change the value of x *)
Lemma refinement4 `{!lockG Σ}:
REL
REL
(let: "x" := ref #1 in
let: "l" := newlock #() in
λ: "f", acquire "l";;
......@@ -314,7 +314,7 @@ Section proofs.
(** "Single return" example *)
Lemma refinement5 :
REL
REL
(λ: "f", let: "x" := ref #0 in
let: "y" := ref #0 in
"f" #();;
......@@ -456,10 +456,10 @@ Section proofs.
Qed.
Lemma close_i6 c1 c2 γ γ' `{oneshotG Σ} `{inG Σ (exclR unitR)} :
(( n : nat, c1 #n
( n : nat, c1 #n
(c2 ↦ₛ #n pending γ
c2 ↦ₛ #(n - 1) shot γ own γ' (Excl ()) 1 n))
- i6 c1 c2 γ γ')%I.
- i6 c1 c2 γ γ'.
Proof.
iDestruct 1 as (m) "[Hc1 Hc2]".
iDestruct "Hc2" as "[[Hc2 Hp] | (Hc2 & Hs & Ht & %)]";
......@@ -510,7 +510,7 @@ Section proofs.
Qed.
Lemma refinement6 `{oneshotG Σ} `{inG Σ (exclR unitR)} :
REL
REL
(λ: "f" "g" "f'",
let: "pg" := p "g" in
let: "g'" := Fst "pg" in
......
......@@ -189,7 +189,7 @@ Section refinement.
end)%I.
Lemma offerInv_empty (st' : val) :
offerInv st'.
offerInv st'.
Proof. by rewrite /offerInv big_sepM_empty. Qed.
Lemma offerInv_excl (N : offerReg) (st' : val) (o : loc) (v : val) :
......@@ -251,7 +251,7 @@ Section refinement.
end%I).
Proof. apply (fixpoint_unfold (stack_link_pre A)). Qed.
Lemma stack_link_empty A : stack_link A None NILV.
Lemma stack_link_empty A : stack_link A None NILV.
Proof. rewrite stack_link_unfold; by iPureIntro. Qed.
Lemma stack_link_cons A l h h' t t' q :
......@@ -597,7 +597,7 @@ Section refinement.
Qed.
Lemma refinement A :
REL mk_stack #() << CG_mkstack #() :
REL mk_stack #() << CG_mkstack #() :
(() () + A) * (A ()).
Proof.
rel_rec_r. rel_pures_r. rel_rec_r.
......
......@@ -22,7 +22,7 @@ Section contents.
Context `{relocG Σ}.
Lemma bot_l K t A :
REL fill K (bot #()) << t : A.
REL fill K (bot #()) << t : A.
Proof.
iLöb as "IH".
rel_rec_l.
......@@ -30,7 +30,7 @@ Section contents.
Qed.
Lemma Y_semtype A :
REL Y << Y : (A A) A.
REL Y << Y : (A A) A.
Proof.
unfold Y.
iApply refines_arrow.
......@@ -45,7 +45,7 @@ Section contents.
Qed.
Lemma FIX_semtype A :
REL F << F : (A A) A.
REL F << F : (A A) A.
Proof.
unfold F.
iApply refines_arrow.
......@@ -58,7 +58,7 @@ Section contents.
(** Landin's knot is equivalent to the Y combinator *)
Lemma KNOT_Y A :
REL Knot << Y : (A A) A.
REL Knot << Y : (A A) A.
Proof.
unfold Y, Knot.
iApply refines_arrow.
......@@ -75,7 +75,7 @@ Section contents.
Qed.
Lemma Y_KNOT A :
REL Y << Knot : (A A) A.
REL Y << Knot : (A A) A.
Proof.
unfold Y, Knot.
iApply refines_arrow.
......@@ -93,7 +93,7 @@ Section contents.
(** Native recursion is equivalent to the Y-combinator *)
Lemma FIX_Y A :
REL F << Y : (A A) A.
REL F << Y : (A A) A.
Proof.
unfold Y, F.
iApply refines_arrow.
......@@ -106,7 +106,7 @@ Section contents.
Qed.
Lemma Y_FIX A :
REL Y << F : (A A) A.
REL Y << F : (A A) A.
Proof.
unfold Y, F.
iApply refines_arrow.
......
......@@ -34,10 +34,10 @@ Section CG_Counter.
Lemma CG_increment_r K E t A (x : loc) (lk : val) (n : nat) :
nclose specN E
(x ↦ₛ # n - is_locked_r lk false -
x ↦ₛ # n - is_locked_r lk false -
(x ↦ₛ # (n + 1) - is_locked_r lk false -
(REL t << fill K (of_val #n) @ E : A)) -
REL t << fill K (CG_increment #x lk) @ E : A)%I.
REL t << fill K (CG_increment #x lk) @ E : A.
Proof.
iIntros (?) "Hx Hl Hlog".
rel_rec_r.
......@@ -66,10 +66,10 @@ Section CG_Counter.
Lemma FG_increment_r K E t A (x : loc) (n : nat) :
nclose specN E
(x ↦ₛ # n -
x ↦ₛ # n -
(x ↦ₛ #(n + 1) -
REL t << fill K (of_val #n) @ E : A) -
REL t << fill K (FG_increment #x) @ E : A)%I.
REL t << fill K (FG_increment #x) @ E : A.
Proof.
iIntros (?) "Hx Hlog".
rel_rec_r. repeat rel_pure_r.
......@@ -192,7 +192,7 @@ Section CG_Counter.
Qed.
Lemma FG_CG_counter_refinement :
REL FG_counter << CG_counter : () (() lrel_int) * (() lrel_int).
REL FG_counter << CG_counter : () (() lrel_int) * (() lrel_int).
Proof.
unfold FG_counter, CG_counter.
iApply refines_arrow_val.
......
......@@ -53,7 +53,7 @@ Proof.
Qed.
Lemma lrel_list_nil `{relocG Σ} A :
lrel_list A NILV NILV.
lrel_list A NILV NILV.
Proof.
rewrite lrel_list_unfold.
iNext. by iLeft.
......@@ -114,7 +114,7 @@ Proof.
Qed.
Lemma nth_int_typed `{relocG Σ} :
REL nth << nth : lrel_list lrel_int lrel_int lrel_int.
REL nth << nth : lrel_list lrel_int lrel_int lrel_int.
(* XXX derive this from the fundamental property *)
Proof.
unfold nth.
......
......@@ -22,7 +22,7 @@ Lemma refines_adequate Σ `{relocPreG Σ}
(A : `{relocG Σ}, lrel Σ)
(P : val val Prop) e e' σ :
( `{relocG Σ}, v v', A v v' - pure_lrel P v v')
( `{relocG Σ}, REL e << e' : A)
( `{relocG Σ}, REL e << e' : A)
adequate NotStuck e σ
(λ v _, thp' h v', rtc erased_step ([e'], σ) (of_val v' :: thp', h)
P v v').
......@@ -65,7 +65,7 @@ Qed.
Theorem refines_typesafety Σ `{relocPreG Σ} e e' e1
(A : `{relocG Σ}, lrel Σ) thp σ σ' :
( `{relocG Σ}, REL e << e' : A)
( `{relocG Σ}, REL e << e' : A)
rtc erased_step ([e], σ) (thp, σ') e1 thp
not_stuck e1 σ'.
Proof.
......
......@@ -211,8 +211,7 @@ Section related_facts.
(* We need this to be able to open and closed invariants in front of logrels *)
Lemma fupd_refines E1 E2 e e' A :
((|={E1,E2}=> REL e << e' @ E2 : A)
- (REL e << e' @ E1 : A))%I.
(|={E1,E2}=> REL e << e' @ E2 : A) - REL e << e' @ E1 : A.
Proof.
rewrite refines_eq /refines_def.
iIntros "H". iIntros (j K) "#Hs Hj /=".
......
......@@ -63,7 +63,7 @@ Section logic.
Global Instance BIJ_timeless γ L : Timeless (BIJ γ L).
Proof. rewrite BIJ_eq /BIJ_def. apply _. Qed.
Lemma alloc_empty_bij : (|==> γ, BIJ γ )%I.
Lemma alloc_empty_bij : |==> γ, BIJ γ .
Proof.
rewrite BIJ_eq /BIJ_def.
iMod (own_alloc ( ( : bijUR))) as (γ) "H".
......
......@@ -26,7 +26,7 @@ Section fundamental.
Lemma bin_log_related_var Δ Γ x τ :
Γ !! x = Some τ
{Δ;Γ} Var x log Var x : τ.
{Δ;Γ} Var x log Var x : τ.
Proof.
iIntros (Hx). iIntros (vs) "#Hvs". simpl.
rewrite (env_ltyped2_lookup _ vs x); last first.
......@@ -36,13 +36,13 @@ Section fundamental.
by iApply refines_ret.
Qed.
Lemma bin_log_related_unit Δ Γ : {Δ;Γ} #() log #() : TUnit.
Lemma bin_log_related_unit Δ Γ : {Δ;Γ} #() log #() : TUnit.
Proof. value_case. Qed.
Lemma bin_log_related_nat Δ Γ (n : nat) : {Δ;Γ} #n log #n : TNat.
Lemma bin_log_related_nat Δ Γ (n : nat) : {Δ;Γ} #n log #n : TNat.
Proof. value_case. Qed.
Lemma bin_log_related_bool Δ Γ (b : bool) : {Δ;Γ} #b log #b : TBool.
Lemma bin_log_related_bool Δ Γ (b : bool) : {Δ;Γ} #b log #b : TBool.
Proof. value_case. Qed.
Lemma bin_log_related_pair Δ Γ e1 e2 e1' e2' (τ1 τ2 : type) :
......@@ -471,7 +471,7 @@ Section fundamental.
Qed.
Theorem binary_fundamental Δ Γ e τ :
Γ e : τ ({Δ;Γ} e log e : τ)%I.
Γ e : τ {Δ;Γ} e log e : τ.
Proof.
intros Ht. iInduction Ht as [] "IH" forall (Δ).
- by iApply bin_log_related_var.
......@@ -505,7 +505,7 @@ Section fundamental.
Theorem refines_typed τ Δ e :
e : τ
REL e << e : (interp τ Δ ).
REL e << e : interp τ Δ.
Proof.
move=> /binary_fundamental Hty.
iPoseProof (Hty Δ with "[]") as "H".
......
......@@ -212,7 +212,7 @@ Section env_typed.
Qed.
Lemma env_ltyped2_empty :
* .
* .
Proof. apply big_sepM2_empty'. Qed.
Lemma env_ltyped2_empty_inv vs :
......
......@@ -6,7 +6,7 @@ From reloc.typing Require Export contextual_refinement.
Lemma logrel_adequate Σ `{relocPreG Σ}
e e' τ (σ : state) :
( `{relocG Σ} Δ, {⊤;Δ;} e log e' : τ)
( `{relocG Σ} Δ, {⊤;Δ;} e log e' : τ)
adequate NotStuck e σ (λ v _, thp' h v', rtc erased_step ([e'], σ) (of_val v' :: thp', h)
(ObsType τ v = v')).
Proof.
......@@ -25,7 +25,7 @@ Proof.
Qed.
Theorem logrel_typesafety Σ `{relocPreG Σ} e e' τ thp σ σ' :
( `{relocG Σ} Δ, {⊤;Δ;} e log e : τ)
( `{relocG Σ} Δ, {⊤;Δ;} e log e : τ)
rtc erased_step ([e], σ) (thp, σ') e' thp
not_stuck e' σ'.
Proof.
......@@ -46,7 +46,7 @@ Qed.
Lemma logrel_simul Σ `{relocPreG Σ}
e e' τ v thp hp σ :
( `{relocG Σ} Δ, {⊤;Δ;} e log e' : τ)
( `{relocG Σ} Δ, {⊤;Δ;} e log e' : τ)
rtc erased_step ([e], σ) (of_val v :: thp, hp)
( thp' hp' v', rtc erased_step ([e'], σ) (of_val v' :: thp', hp') (ObsType τ v = v')).
Proof.
......@@ -57,7 +57,7 @@ Proof.
Qed.
Lemma logrel_ctxequiv Σ `{relocPreG Σ} Γ e e' τ :
( `{relocG Σ} Δ, {⊤;Δ;Γ} e log e' : τ)
( `{relocG Σ} Δ, {⊤;Δ;Γ} e log e' : τ)
Γ e ctx e' : τ.
Proof.
intros Hlog K thp σ₀ σ₁ v τ' ? Htyped Hstep.
......@@ -70,7 +70,7 @@ Proof.
Qed.
Lemma refines_sound Σ `{relocPreG Σ} e e' τ :
( `{relocG Σ} Δ, REL e << e' : (interp τ Δ))
( `{relocG Σ} Δ, REL e << e' : (interp τ Δ))
e ctx e' : τ.
Proof.
intros Hlog. eapply logrel_ctxequiv. apply _.
......
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