Commit 63eda220 authored by Robbert Krebbers's avatar Robbert Krebbers

Clean up namespace stuff.

parent 57c68486
From iris.program_logic Require Import lifting.
From iris.algebra Require Import upred_big_op.
From iris_logrel.F_mu Require Import lang typing rules logrel.
Import uPred.
From iris_logrel.F_mu Require Export logrel.
From iris.proofmode Require Import tactics.
From iris_logrel.F_mu Require Import rules.
From iris.algebra Require Export upred_big_op.
Section typed_interp.
Context {Σ : iFunctor}.
......@@ -16,7 +16,7 @@ Section typed_interp.
Lemma typed_interp (Δ : varC -n> valC -n> iProp lang Σ) Γ vs e τ
(Htyped : typed Γ e τ) (HΔ : x v, PersistentP (Δ x v)) :
List.length Γ = List.length vs
length Γ = length vs
[] zip_with (λ τ, interp τ Δ) Γ vs WP e.[env_subst vs] {{ interp τ Δ }}.
Proof.
revert Δ HΔ vs. induction Htyped; iIntros {Δ HΔ vs Hlen} "#HΓ"; cbn.
......
Require Export iris_logrel.prelude.base.
Require Import iris.program_logic.language.
From iris_logrel.prelude Require Export base.
From iris.program_logic Require Import language.
Module lang.
Inductive expr :=
......
Require Import iris.program_logic.lifting.
Require Import iris.algebra.upred_big_op.
Require Import iris_logrel.F_mu.lang iris_logrel.F_mu.typing
iris_logrel.F_mu.rules.
From iris.program_logic Require Export weakestpre.
From iris_logrel.F_mu Require Export lang typing.
Import uPred.
(** interp : is a unary logical relation. *)
......
Require Import iris.program_logic.lifting.
Require Import iris.algebra.upred_big_op.
Require Import iris_logrel.F_mu.lang.
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import lifting.
From iris_logrel.F_mu Require Export lang.
Section lang_rules.
Context {Σ : iFunctor}.
......@@ -123,7 +123,7 @@ Section lang_rules.
intros <-%of_to_val.
rewrite -(wp_lift_pure_det_step (Case (InjL _) _ _) (e1.[of_val v0/]) None) //=; auto.
- rewrite right_id; auto using uPred.later_mono, wp_value'.
Qed.
Qed.
Lemma wp_case_inr E e0 v0 e1 e2 Q :
to_val e0 = Some v0
......
Require Import iris.proofmode.tactics.
Require Import iris.program_logic.lifting.
Require Import iris.algebra.upred_big_op.
Require Import iris_logrel.F_mu.lang iris_logrel.F_mu.typing
iris_logrel.F_mu.rules iris_logrel.F_mu.logrel
iris_logrel.F_mu.fundamental.
Require Import iris.program_logic.adequacy.
Import uPred.
From iris_logrel.F_mu Require Export fundamental.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Import adequacy.
Section Soundness.
Definition Σ := #[].
Lemma empty_env_subst e : e.[env_subst []] = e.
Proof.
replace (env_subst []) with (@ids expr _) by reflexivity.
asimpl; trivial.
Qed.
Proof. change (env_subst []) with (@ids expr _). by asimpl. Qed.
Definition free_type_context : varC -n> valC -n> iProp lang (globalF Σ) :=
λne x y, True%I.
......
Require Import iris_logrel.prelude.base.
Require Import iris_logrel.F_mu.lang.
From iris_logrel.F_mu Require Export lang.
Inductive type :=
| TUnit : type
......@@ -44,11 +43,11 @@ Inductive typed (Γ : list type) : expr → type → Prop :=
.
Local Hint Extern 1 =>
match goal with [H : context [List.length (map _ _)] |- _] => rewrite map_length in H end
match goal with [H : context [length (map _ _)] |- _] => rewrite map_length in H end
: typed_subst_invariant.
Lemma typed_subst_invariant Γ e τ s1 s2 :
typed Γ e τ ( x, x < List.length Γ s1 x = s2 x) e.[s1] = e.[s2].
typed Γ e τ ( x, x < length Γ s1 x = s2 x) e.[s1] = e.[s2].
Proof.
intros Htyped; revert s1 s2.
assert ( {A} `{Ids A} `{Rename A}
......@@ -61,7 +60,7 @@ Definition env_subst (vs : list val) (x : var) : expr :=
from_option id (Var x) (of_val <$> vs !! x).
Lemma typed_subst_head_simpl Δ τ e w ws :
typed Δ e τ -> List.length Δ = S (List.length ws)
typed Δ e τ -> length Δ = S (length ws)
e.[# w .: env_subst ws] = e.[env_subst (w :: ws)].
Proof.
intros H1 H2.
......
Require Import iris.program_logic.lifting.
Require Import iris.algebra.upred_big_op.
Require Import iris_logrel.F_mu_ref.lang iris_logrel.F_mu_ref.typing
iris_logrel.F_mu_ref.rules iris_logrel.F_mu_ref.logrel.
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.tactics iris.proofmode.invariants.
Import uPred.
From iris_logrel.F_mu_ref Require Export logrel.
From iris.proofmode Require Import tactics pviewshifts invariants.
From iris_logrel.F_mu_ref Require Import rules.
From iris.algebra Require Export upred_big_op.
Section typed_interp.
Context {Σ : gFunctors} `{i : heapG Σ} {L : namespace}.
......@@ -24,7 +18,7 @@ Section typed_interp.
(HNLdisj : l : loc, N L .@ l)
(Htyped : typed Γ e τ)
(HΔ : x v, PersistentP (Δ x v)) :
List.length Γ = List.length vs
length Γ = length vs
heap_ctx N [] zip_with (λ τ, interp L τ Δ) Γ vs
WP e.[env_subst vs] {{ interp L τ Δ }}.
Proof.
......@@ -104,7 +98,7 @@ Section typed_interp.
rewrite fixpoint_unfold.
iIntros "#Hv"; cbn.
change (fixpoint _) with (interp L (TRec τ) Δ).
iDestruct "Hv" as {w} "[% #Hw]"; rewrite H.
iDestruct "Hv" as {w} "[% #Hw]"; subst.
iApply wp_Fold; cbn; auto using to_of_val.
rewrite -interp_subst; auto.
- (* Alloc *)
......@@ -112,8 +106,7 @@ Section typed_interp.
iApply wp_atomic; cbn; trivial; [rewrite to_of_val; auto|].
iPvsIntro.
iApply wp_alloc; auto 1 using to_of_val.
iFrame "Hheap". iNext.
iIntros {l} "Hl". iPvsIntro.
iFrame "Hheap". iNext. iIntros {l} "Hl". iPvsIntro.
iPvs (inv_alloc _ with "[Hl]") as "HN";
[| | iPvsIntro; iExists _; iSplit; trivial]; eauto.
- (* Load *)
......
Require Export iris_logrel.prelude.base.
Require Import iris.prelude.gmap.
Require Import iris.program_logic.language.
From iris_logrel.prelude Require Export base.
From iris.program_logic Require Import language.
From iris.prelude Require Import gmap.
Module lang.
Definition loc := positive.
......
Require Import iris.program_logic.lifting.
Require Import iris.algebra.upred_big_op.
Require Import iris_logrel.F_mu_ref.lang iris_logrel.F_mu_ref.typing
iris_logrel.F_mu_ref.rules.
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.
From iris.program_logic Require Export weakestpre.
From iris_logrel.F_mu_ref Require Export rules typing.
Import uPred.
(** interp : is a unary logical relation. *)
......
Require Import iris.program_logic.lifting.
Require Import iris.algebra.upred_big_op.
Require Import iris_logrel.F_mu_ref.lang.
From iris.program_logic Require Export lifting.
From iris.program_logic Require Export weakestpre global_functor invariants.
From iris.program_logic Require Import lifting.
From iris.algebra Require Import upred_big_op frac dec_agree.
From iris.program_logic Require Export invariants ghost_ownership.
From iris.proofmode Require Import weakestpre.
From iris.program_logic Require Import ownership auth.
Require Import iris.proofmode.tactics iris.proofmode.invariants.
From iris_logrel.F_mu_ref Require Export lang.
From iris.proofmode Require Import tactics weakestpre invariants.
Import uPred.
Definition heapUR : ucmraT := gmapUR loc (prodR fracR (dec_agreeR val)).
......
Require Import iris.proofmode.weakestpre iris.proofmode.tactics.
Require Import iris.program_logic.lifting.
Require Import iris.algebra.auth.
Require Import iris_logrel.F_mu_ref.lang iris_logrel.F_mu_ref.typing
iris_logrel.F_mu_ref.rules iris_logrel.F_mu_ref.logrel
iris_logrel.F_mu_ref.fundamental.
Require Import iris.program_logic.adequacy.
Import uPred.
From iris_logrel.F_mu_ref Require Export fundamental.
From iris.proofmode Require Import tactics pviewshifts.
From iris.program_logic Require Import adequacy.
Section Soundness.
Definition Σ := #[ auth.authGF heapUR ].
Lemma empty_env_subst e : e.[env_subst []] = e.
Proof.
replace (env_subst []) with (@ids expr _) by reflexivity.
asimpl; trivial.
Qed.
Proof. change (env_subst []) with (@ids expr _). by asimpl. Qed.
Definition free_type_context: varC -n> valC -n> iPropG lang Σ :=
λne x y, True%I.
Lemma wp_soundness e τ :
typed [] e τ
ownership.ownP WP e {{ v, H, @interp Σ H (nroot .@ "Fμ,ref" .@ 1)
τ free_type_context v}}.
ownership.ownP WP e {{ v, H : heapG Σ,
interp (nroot .@ "Fμ,ref" .@ 1) τ free_type_context v}}.
Proof.
iIntros {H1} "Hemp".
iDestruct (heap_alloc (nroot .@ "Fμ,ref" .@ 2) _ _ _ _ with "Hemp") as "Hp".
iPvs "Hp" as {H} "[Hheap Hemp]".
iPvs (heap_alloc (nroot .@ "Fμ,ref" .@ 2) _ _ _ _ with "Hemp") as {H} "[Hheap Hemp]".
iApply wp_wand_l. iSplitR.
{ iIntros {v} "HΦ". iExists H. iExact "HΦ". }
rewrite -(empty_env_subst e).
......
Require Import iris_logrel.prelude.base.
Require Import iris_logrel.F_mu_ref.lang.
From iris_logrel.F_mu_ref Require Export lang.
Inductive type :=
| TUnit : type
......@@ -67,7 +66,7 @@ Definition env_subst (vs : list val) (x : var) : expr :=
from_option id (Var x) (of_val <$> vs !! x).
Lemma typed_subst_head_simpl Δ τ e w ws :
typed Δ e τ -> List.length Δ = S (List.length ws)
typed Δ e τ length Δ = S (length ws)
e.[# w .: env_subst ws] = e.[env_subst (w :: ws)].
Proof.
intros H1 H2.
......
Require Import iris_logrel.prelude.base.
From iris_logrel.F_mu_ref_par Require Import lang typing rules_binary
rules logrel_binary fundamental_binary.
Local Notation expr := (expr lang).
From iris_logrel.F_mu_ref_par Require Export fundamental_binary.
Inductive context_item : Type :=
| CTX_Lam
......@@ -183,8 +179,8 @@ Proof.
Qed.
Lemma typed_context_n_closed K Γ τ Γ' τ' e :
( f, e.[iter (List.length Γ) up f] = e) typed_context K Γ τ Γ' τ'
f, (fill_ctx K e).[iter (List.length Γ') up f] = (fill_ctx K e).
( f, e.[base.iter (length Γ) up f] = e) typed_context K Γ τ Γ' τ'
f, (fill_ctx K e).[base.iter (length Γ') up f] = (fill_ctx K e).
Proof.
intros H1 H2; induction H2; simpl; auto.
(induction H => f); asimpl; simpl in *;
......@@ -206,8 +202,8 @@ Section bin_log_related_under_typed_context.
Implicit Types Δ : varC -n> bivalC -n> iPropG lang Σ.
Lemma bin_log_related_under_typed_context Γ e e' τ Γ' τ' K :
( f, e.[iter (List.length Γ) up f] = e)
( f, e'.[iter (List.length Γ) up f] = e')
( f, e.[base.iter (length Γ) up f] = e)
( f, e'.[base.iter (length Γ) up f] = e')
typed_context K Γ τ Γ' τ'
( Δ {HΔ : x vw, PersistentP (Δ x vw)},
@bin_log_related _ _ _ N Δ Γ e e' τ HΔ)
......
From iris.proofmode Require Import invariants ghost_ownership tactics.
From iris_logrel.F_mu_ref_par Require Import lang examples.lock typing
logrel_binary fundamental_binary rules_binary rules
soundness_binary context_refinement.
Import uPred.
From iris_logrel.F_mu_ref_par Require Export examples.lock.
From iris_logrel.F_mu_ref_par Require Import soundness_binary.
Definition CG_increment (x : expr) : expr :=
Lam (Store x.[ren (+ 2)] (BinOp Add ( 1) (Load x.[ren (+ 2)]))).
......@@ -201,8 +199,7 @@ Section CG_Counter.
constructor. apply CG_counter_body_type; by constructor.
Qed.
Lemma CG_counter_closed f :
CG_counter.[f] = CG_counter.
Lemma CG_counter_closed f : CG_counter.[f] = CG_counter.
Proof.
asimpl; rewrite CG_locked_increment_subst counter_read_subst; by asimpl.
Qed.
......
From iris.proofmode Require Import invariants ghost_ownership tactics.
From iris_logrel.F_mu_ref_par Require Import lang rules rules_binary typing.
Import uPred.
From iris_logrel.F_mu_ref_par Require Export rules_binary typing.
Definition newlock : expr := Alloc ( false).
Definition acquire : expr :=
......
From iris.proofmode Require Import invariants ghost_ownership tactics.
From iris_logrel.F_mu_ref_par Require Import lang examples.lock typing
rules_binary rules.
From iris_logrel.F_mu_ref_par Require Import examples.lock.
Import uPred.
Definition CG_StackType τ :=
......
From iris.program_logic Require Import language.
From iris_logrel.F_mu_ref_par Require Import lang typing rules.
From iris_logrel.F_mu_ref_par Require Import typing.
Definition FG_StackType τ :=
TRec (Tref (TSum TUnit (TProd τ.[ren (+1)] (TVar 0)))).
......@@ -111,8 +110,6 @@ Definition FG_stack : expr :=
(Alloc (Fold (Alloc (InjL Unit))))).
Section FG_stack.
Context {Σ : gFunctors} {iI : heapIG Σ}.
(* Fine-grained push *)
Lemma FG_push_folding (st : expr) :
FG_push st =
......
From iris.program_logic Require Import auth.
From iris_logrel.F_mu_ref_par Require Import soundness_binary.
From iris_logrel.F_mu_ref_par.examples Require Import lock.
From iris_logrel.F_mu_ref_par.examples.stack Require Import
CG_stack FG_stack stack_rules.
From iris.proofmode Require Import invariants ghost_ownership tactics.
From iris.program_logic Require Import auth namespaces.
From iris_logrel.F_mu_ref_par Require Import lang examples.lock
examples.stack.CG_stack examples.stack.FG_stack examples.stack.stack_rules
typing logrel_binary fundamental_binary rules_binary rules
context_refinement soundness_binary.
Import uPred.
Section Stack_refinement.
Context {Σ : gFunctors} {iS : cfgSG Σ} {iI : heapIG Σ}
......
From iris.proofmode Require Import invariants ghost_ownership tactics.
From iris_logrel.F_mu_ref_par Require Import lang rules logrel_binary.
From iris.algebra Require Import gmap dec_agree auth upred_big_op.
From iris.program_logic Require Import ownership auth.
From iris_logrel.F_mu_ref_par Require Import logrel_binary.
From iris.algebra Require Import gmap dec_agree.
From iris.program_logic Require Import auth.
Import uPred.
Definition stackUR : ucmraT := gmapUR loc (dec_agreeR val).
......
Require Import iris.program_logic.lifting.
Require Import iris.algebra.upred_big_op.
Require Import iris_logrel.F_mu_ref_par.lang iris_logrel.F_mu_ref_par.typing
iris_logrel.F_mu_ref_par.rules iris_logrel.F_mu_ref_par.rules_binary
iris_logrel.F_mu_ref_par.logrel_binary.
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.tactics iris.proofmode.invariants.
Import uPred.
From iris_logrel.F_mu_ref_par Require Export logrel_binary.
From iris.proofmode Require Import tactics pviewshifts invariants.
From iris_logrel.F_mu_ref_par Require Import rules_binary.
From iris.algebra Require Export upred_big_op.
Section typed_interp.
Context {Σ : gFunctors} {iI : heapIG Σ} {iS : cfgSG Σ} {N : namespace}.
......@@ -34,7 +27,7 @@ Section typed_interp.
Qed.
Definition bin_log_related Δ Γ e e' τ {HΔ : x vw, PersistentP (Δ x vw)} :=
vs, List.length Γ = List.length vs
vs, length Γ = length vs
ρ j K,
heapI_ctx (N .@ 2) Spec_ctx (N .@ 3) ρ
[] zip_with (λ τ, interp (N .@ 1) τ Δ) Γ vs
......@@ -70,7 +63,7 @@ Section typed_interp.
(IHHtyped : Δ Γ e log e' TProd τ1 τ2) :
Δ Γ Fst e log Fst e' τ1.
Proof.
intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
iIntros {vs Hlen ρ j K} "(#Hheap & #Hspec & #HΓ & Htr)"; cbn.
smart_wp_bind (FstCtx) v v' "[Hv #Hiv]"
(IHHtyped _ _ _ j (K ++ [FstCtx])); cbn.
iDestruct "Hiv" as {w1 w2} "#[% [Hiv2 Hiv3]]"; simplify_eq.
......@@ -86,7 +79,7 @@ Section typed_interp.
(IHHtyped : Δ Γ e log e' TProd τ1 τ2) :
Δ Γ Snd e log Snd e' τ2.
Proof.
intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
iIntros {vs Hlen ρ j K} "(#Hheap & #Hspec & #HΓ & Htr)"; cbn.
smart_wp_bind (SndCtx) v v' "[Hv #Hiv]"
(IHHtyped _ _ _ j (K ++ [SndCtx])); cbn.
iDestruct "Hiv" as {w1 w2} "#[% [Hiv2 Hiv3]]".
......@@ -103,7 +96,7 @@ Section typed_interp.
(IHHtyped : Δ Γ e log e' τ1) :
Δ Γ InjL e log InjL e' (TSum τ1 τ2).
Proof.
intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
iIntros {vs Hlen ρ j K} "(#Hheap & #Hspec & #HΓ & Htr)"; cbn.
smart_wp_bind (InjLCtx) v v' "[Hv #Hiv]"
(IHHtyped _ _ _ j (K ++ [InjLCtx])); cbn.
value_case. iExists (InjLV v'); iFrame "Hv".
......@@ -116,7 +109,7 @@ Section typed_interp.
(IHHtyped : Δ Γ e log e' τ2) :
Δ Γ InjR e log InjR e' TSum τ1 τ2.
Proof.
intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
intros vs Hlen ρ j K. iIntros "(#Hheap & #Hspec & #HΓ & Htr)"; cbn.
smart_wp_bind (InjRCtx) v v' "[Hv #Hiv]"
(IHHtyped _ _ _ j (K ++ [InjRCtx])); cbn.
value_case. iExists (InjRV v'); iFrame "Hv".
......@@ -127,10 +120,10 @@ Section typed_interp.
Lemma typed_binary_interp_Case Δ Γ (e0 e1 e2 e0' e1' e2' : expr) τ1 τ2 τ3
{HΔ : ✓✓ Δ}
(Hclosed2 : f, e1.[iter (S (List.length Γ)) up f] = e1)
(Hclosed3 : f, e2.[iter (S (List.length Γ)) up f] = e2)
(Hclosed2' : f, e1'.[iter (S (List.length Γ)) up f] = e1')
(Hclosed3' : f, e2'.[iter (S (List.length Γ)) up f] = e2')
(Hclosed2 : f, e1.[iter (S (length Γ)) up f] = e1)
(Hclosed3 : f, e2.[iter (S (length Γ)) up f] = e2)
(Hclosed2' : f, e1'.[iter (S (length Γ)) up f] = e1')
(Hclosed3' : f, e2'.[iter (S (length Γ)) up f] = e2')
(IHHtyped1 : Δ Γ e0 log e0' TSum τ1 τ2)
(IHHtyped2 : Δ τ1 :: Γ e1 log e1' τ3)
(IHHtyped3 : Δ τ2 :: Γ e2 log e2' τ3) :
......@@ -205,8 +198,8 @@ Section typed_interp.
Qed.
Lemma typed_binary_interp_Lam Δ Γ (e e' : expr) τ1 τ2 {HΔ : ✓✓ Δ}
(Hclosed : f, e.[iter (S (S (List.length Γ))) up f] = e)
(Hclosed' : f, e'.[iter (S (S (List.length Γ))) up f] = e')
(Hclosed : f, e.[iter (S (S (length Γ))) up f] = e)
(Hclosed' : f, e'.[iter (S (S (length Γ))) up f] = e')
(IHHtyped : Δ TArrow τ1 τ2 :: τ1 :: Γ e log e' τ2) :
Δ Γ Lam e log Lam e' TArrow τ1 τ2.
Proof.
......
Require Import iris.program_logic.lifting.
Require Import iris.algebra.upred_big_op.
Require Import iris_logrel.F_mu_ref_par.lang iris_logrel.F_mu_ref_par.typing
iris_logrel.F_mu_ref_par.rules iris_logrel.F_mu_ref_par.logrel_unary.
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.tactics iris.proofmode.invariants.
Import uPred.
From iris_logrel.F_mu_ref_par Require Export logrel_unary.
From iris_logrel.F_mu_ref_par Require Import rules.
From iris.algebra Require Export upred_big_op.
From iris.proofmode Require Import tactics pviewshifts invariants.
Section typed_interp.
Context {Σ : gFunctors} `{i : heapIG Σ} `{L : namespace}.
......@@ -23,7 +17,7 @@ Section typed_interp.
Lemma typed_interp N (Δ : varC -n> valC -n> iPropG lang Σ) Γ vs e τ
(HNLdisj : l : loc, N L .@ l)
(Htyped : typed Γ e τ) (HΔ : x v, PersistentP (Δ x v)) :
List.length Γ = List.length vs
length Γ = length vs
heapI_ctx N [] zip_with (λ τ, interp L τ Δ) Γ vs
WP e.[env_subst vs] {{ interp L τ Δ }}.
Proof.
......@@ -166,12 +160,12 @@ Section typed_interp.
destruct (val_dec_eq v2 w) as [|Hneq]; subst.
+ iApply (wp_cas_suc N); eauto using to_of_val.
specialize (HNLdisj l); set_solver_ndisj.
iFrame "Hheap Hw1". iIntros "> Hw1"; iPvsIntro.
iIntros "{$Hheap $Hw1} > Hw1"; iPvsIntro.
iSplitL; [|iPvsIntro]; eauto.
+ 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". iIntros "> Hw1". iPvsIntro. iSplitL; [|iPvsIntro]; eauto.
iIntros "{$Hheap $Hw1} > Hw1". iPvsIntro. iSplitL; [|iPvsIntro]; eauto.
Qed.
End typed_interp.
Require Export iris_logrel.prelude.base.
Require Import iris.prelude.gmap.
Require Import iris.program_logic.language.
From iris_logrel.prelude Require Export base.
From iris.program_logic Require Import language.
From iris.prelude Require Import gmap.
Module lang.
Definition loc := positive.
......@@ -9,8 +9,8 @@ Module lang.
Inductive binop := Add | Sub | Eq | Le | Lt.
Instance Natbinop_dec_eq (op op' : binop) : Decision (op = op').
Proof. unfold Decision. decide equality. Qed.
Instance binop_dec_eq (op op' : binop) : Decision (op = op').
Proof. solve_decision. Defined.
Inductive expr :=
| Var (x : var)
......
Require Import iris.program_logic.lifting.
Require Import iris.algebra.upred_big_op.
Require Import iris_logrel.F_mu_ref_par.lang iris_logrel.F_mu_ref_par.typing
iris_logrel.F_mu_ref_par.rules iris_logrel.F_mu_ref_par.rules_binary.
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.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris_logrel.F_mu_ref_par Require Export rules_binary typing.
Import uPred.
(** interp : is a unary logical relation. *)
......@@ -452,25 +446,17 @@ Section logrel.
{HΔ : x vw, PersistentP (Δ x vw)} :
interp τ Δ (v, v') (v = v').
Proof.
revert v v'; induction H => v v'; iIntros "#H1".
- simpl; iDestruct "H1" as "[% %]"; subst; trivial.
- simpl; iDestruct "H1" as {n} "[% %]"; subst; trivial.
- simpl; iDestruct "H1" as {b} "[% %]"; subst; trivial.
- iDestruct "H1" as {w1 w2} "[% [H1 H2]]".
destruct w1; destruct w2; simpl in *.
inversion H1; subst.
revert v v'; induction H; iIntros {v v'} "#H1 /=".
- by iDestruct "H1" as "[% %]"; subst.
- by iDestruct "H1" as {n} "[% %]"; subst.
- by iDestruct "H1" as {b} "[% %]"; subst.
- iDestruct "H1" as { [??] [??] } "[% [H1 H2]]"; simplify_eq/=.
rewrite IHEqType1 IHEqType2.
iDestruct "H1" as "%". iDestruct "H2" as "%". subst; trivial.
by iDestruct "H1" as "%"; iDestruct "H2" as "%"; subst.
- 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.
+ iDestruct "H1" as { [??] } "[% H1]"; simplify_eq/=.
rewrite IHEqType1. by iDestruct "H1" as "%"; subst.
+ iDestruct "H1" as { [??] } "[% H1]"; simplify_eq/=.
rewrite IHEqType2. by iDestruct "H1" as "%"; subst.
Qed.
End logrel.
From iris.program_logic Require Import lifting.
From iris_logrel.F_mu_ref_par Require Import lang typing rules.
From iris.algebra Require Import upred_big_op frac dec_agree upred_big_op.
From iris.program_logic Require Export invariants ghost_ownership.
From iris.program_logic Require Import ownership auth.
From iris.program_logic Require Export weakestpre.
From iris_logrel.F_mu_ref_par Require Export rules typing.
Import uPred.
(** interp : is a unary logical relation. *)
......
Require Import iris.program_logic.lifting.
Require Import iris.algebra.upred_big_op.
Require Import iris_logrel.F_mu_ref_par.lang.
From iris.program_logic Require Export lifting.
From iris.algebra Require Import upred_big_op frac dec_agree list.
From iris.program_logic Require Export invariants ghost_ownership.
From iris.proofmode Require Import tactics weakestpre invariants.
From iris.program_logic Require Export weakestpre global_functor invariants.
From iris.program_logic Require Import lifting.
From iris.algebra Require Import upred_big_op frac dec_agree.
From iris.program_logic Require Import ownership auth.
From iris.proofmode Require Import weakestpre.
Require Import iris.proofmode.tactics iris.proofmode.invariants.
From iris_logrel.F_mu_ref_par Require Export lang.
Import uPred.
Definition heapUR : ucmraT := gmapUR loc (prodR fracR (dec_agreeR val)).
......
From iris.program_logic Require Import auth lifting.
From iris_logrel.F_mu_ref_par Require Import lang rules.
From iris.algebra Require Import upred_big_op frac dec_agree list upred_big_op.
From iris.program_logic Require Export invariants ghost_ownership.
From iris.proofmode Require Import tactics invariants.
From iris.program_logic Require Import lifting.
From iris.algebra Require Import upred_big_op frac dec_agree.
From iris.program_logic Require Import ownership auth.
From iris_logrel.F_mu_ref_par Require Export rules.
From iris.proofmode Require Import tactics weakestpre invariants.
Import uPred.
(** The CMRA for the heap of the specification. *)
......@@ -136,7 +136,7 @@ Section cfg.
({[ j := Excl' e ]} tp) l1 l2,
( e', of_tpool ({[ j := Excl' e' ]} tp) = l1 ++ e' :: l2)
( e' k e'',
j < k List.length tp < k
j < k length tp < k
of_tpool ({[ j := Excl' e' ]} {[ k := Excl' e'' ]} tp) =
l1 ++ e' :: l2 ++ [e'']).
Proof.
......@@ -198,7 +198,7 @@ Section cfg.
Qed.
Lemma thread_alloc_safe k j (e e' : exprC) (tp : tpoolUR) :
j < k List.length tp < k
j < k length tp < k
({[j := Excl' e ]} tp)
({[j := Excl' e ]} {[k := Excl' e' ]} tp).
Proof.
......@@ -211,7 +211,7 @@ Section cfg.
Qed.
Lemma thread_alloc_update k j e e' h ρ :
j < k List.length (ρ.1) < k
j < k length (ρ.1) < k
(({[j := Excl' e ]}, h) ρ)
(({[j := Excl' e ]}, h) ρ : cfgUR) ({[j := Excl' e]}, h)
~~> (({[j := Excl' e]} {[k := Excl' e']}, h) ρ)
......@@ -587,7 +587,7 @@ Section cfg.
Proof. apply step_pure => σ; econstructor. Qed.
Lemma step_fork_base k j K e h ρ :
j < k List.length (ρ.1) < k
j < k length (ρ.1) < k
(({[j := Excl' (fill K (Fork e))]}, h) ρ)
step (of_cfg (({[j := Excl' (fill K (Fork e))]}, h) ρ))
(of_cfg (({[j := Excl' (fill K Unit)]} {[k := Excl' e]}, h) ρ)).
......@@ -614,9 +614,9 @@ Section cfg.
iDestruct "Hstep" as %Hstep.
iPvs (own_update with "Hown") as "Hown".
rewrite comm; apply (thread_update _ _ (fill K Unit)); trivial.
set (k := S (max (List.length (ρ''.1)) j)).
set (k := S (max (length (ρ''.1)) j)).
assert (Hx1 : k > j) by (unfold k; lia).
assert (Hx2 : k > List.length (ρ''.1)) by (unfold k; lia).