Commit 7bf3e041 authored by Dan Frumin's avatar Dan Frumin

bump iris version

parent b5638f38
......@@ -5,8 +5,8 @@ This version is known to compile with:
- Coq 8.6.1
- Ssreflect 1.6
- Autosubst branch [coq86-devel](https://github.com/uds-psl/autosubst/tree/coq86-devel)
- std++ version [5912d750ffe247b5a41f27cb42b98f23c571897d](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/tree/5912d750ffe247b5a41f27cb42b98f23c571897d)
- Iris version [6c7b99c2dd261fb7e67a339da89bdb12a3189678](https://gitlab.mpi-sws.org/FP/iris-coq/tree/6c7b99c2dd261fb7e67a339da89bdb12a3189678)
- std++ version [6117c3e4a57307fd374780836a130ac86608d8cd](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/tree/6117c3e4a57307fd374780836a130ac86608d8cd)
- Iris version [c22e7b339288ee006eea1046abb80f65fc169a6f](https://gitlab.mpi-sws.org/FP/iris-coq/tree/c22e7b339288ee006eea1046abb80f65fc169a6f)
# Compilation
......
......@@ -13,14 +13,12 @@ Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val].
Instance subG_heapPreG {Σ} : subG heapΣ Σ heapPreG Σ.
Proof. solve_inG. Qed.
Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
( `{heapG Σ}, True WP e {{ v, ⌜φ v }})
adequate e σ φ.
Definition heap_adequacy Σ `{heapPreG Σ} s e σ φ :
( `{heapG Σ}, WP e @ s; {{ v, ⌜φ v }}%I)
adequate s e σ φ.
Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "".
iMod (own_alloc ( to_gen_heap σ)) as (γ) "Hh".
{ apply: auth_auth_valid. exact: to_gen_heap_valid. }
iModIntro. iExists (λ σ, own γ ( to_gen_heap σ)); iFrame.
set (Hheap := GenHeapG loc val Σ _ _ _ γ).
by iApply (Hwp (HeapG _ _ _)).
iMod (gen_heap_init σ) as (?) "Hh".
iModIntro. iExists gen_heap_ctx. iFrame "Hh".
iApply (Hwp (HeapG _ _ _)).
Qed.
......@@ -484,10 +484,12 @@ Local Hint Resolve language.val_irreducible.
Local Hint Resolve to_of_val.
Local Hint Unfold language.irreducible.
Lemma is_atomic_correct e : is_atomic e Atomic e.
Lemma is_atomic_correct a e : is_atomic e Atomic a e.
Proof.
intros ?; apply ectx_language_atomic.
- destruct 1; simpl; eauto.
intros ?; apply strongly_atomic_atomic.
apply ectx_language_atomic.
- destruct 1; subst; simpl; eauto;
try by match goal with | [H : is_atomic _ |- _] => inversion H end.
- apply ectxi_language_sub_redexes_are_values=> /= Ki e' Hfill.
destruct e=> //; destruct Ki; repeat (simplify_eq/=; case_match=>//);
naive_solver eauto using to_val_is_Some.
......@@ -497,7 +499,7 @@ Ltac solve_atomic :=
apply is_atomic_correct; simpl; repeat split;
rewrite ?to_of_val; eapply mk_is_Some; fast_done.
Hint Extern 10 (Atomic _) => solve_atomic : typeclass_instances.
Hint Extern 10 (Atomic _ _) => solve_atomic : typeclass_instances.
(* Some other useful tactics *)
Ltac inv_head_step :=
......
......@@ -149,7 +149,7 @@ Section lang_rules.
Proof.
rewrite -(wp_lift_pure_det_head_step (Fork e) #() [e]) //=; eauto.
- (* TODO typeclass inference fail *)
erewrite <-(wp_value_fupd _ _ #()); eauto; last solve_to_val.
erewrite <-(wp_value_fupd _ _ _ #()); eauto; last solve_to_val.
by rewrite -step_fupd_intro // right_id later_sep.
- intros; inv_head_step; eauto.
Qed.
......
......@@ -97,9 +97,9 @@ Ltac wp_bind_core'' K :=
Tactic Notation "wp_bind" open_constr(efoc) :=
iStartProof;
lazymatch goal with
| |- envs_entails _ (wp ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
| |- envs_entails _ (wp _ ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
unify e' efoc; wp_bind_core K)
| |- envs_entails _ (|={?E1,?E2}=> wp ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
| |- envs_entails _ (|={?E1,?E2}=> wp _ ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
unify e' efoc; wp_bind_core'' K)
| _ => fail "wp_bind: not a 'wp'"
end.
......@@ -128,7 +128,7 @@ Ltac wp_value := eapply tac_wp_value; [apply _|lazy beta].
Tactic Notation "wp_pure" open_constr(efoc) :=
iStartProof;
lazymatch goal with
| |- envs_entails _ (wp ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
| |- envs_entails _ (wp _ ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
unify e' efoc;
eapply (tac_wp_pure K);
[apply _ (* PureExec *)
......@@ -233,7 +233,7 @@ End heap.
Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
iStartProof;
lazymatch goal with
| |- envs_entails _ (wp ?E ?e ?Q) =>
| |- envs_entails _ (wp _ ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with Alloc _ => wp_bind_core K end)
......@@ -255,7 +255,7 @@ Tactic Notation "wp_alloc" ident(l) :=
Tactic Notation "wp_load" :=
iStartProof;
lazymatch goal with
| |- envs_entails _ (wp ?E ?e ?Q) =>
| |- envs_entails _ (wp _ ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with Load _ => wp_bind_core K end)
......@@ -271,7 +271,7 @@ Tactic Notation "wp_load" :=
Tactic Notation "wp_store" :=
iStartProof;
lazymatch goal with
| |- envs_entails _ (wp ?E ?e ?Q) =>
| |- envs_entails _ (wp _ ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with Store _ _ => wp_bind_core K end)
......@@ -290,7 +290,7 @@ Tactic Notation "wp_store" :=
Tactic Notation "wp_cas_fail" :=
iStartProof;
lazymatch goal with
| |- envs_entails _ (wp ?E ?e ?Q) =>
| |- envs_entails _ (wp _ ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with CAS _ _ _ => wp_bind_core K end)
......@@ -311,7 +311,7 @@ Tactic Notation "wp_cas_fail" :=
Tactic Notation "wp_cas_suc" :=
iStartProof;
lazymatch goal with
| |- envs_entails _ (wp ?E ?e ?Q) =>
| |- envs_entails _ (wp _ ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with CAS _ _ _ => wp_bind_core K end)
......
......@@ -194,7 +194,7 @@ Section properties.
Qed.
Lemma bin_log_related_wp_atomic_l Δ Γ (E : coPset) K e1 e2 τ
(Hatomic : Atomic e1)
(Hatomic : Atomic WeaklyAtomic e1)
(Hclosed1 : Closed e1) :
(|={,E}=> WP e1 @ E {{ v,
{E;Δ;Γ} fill K (of_val v) log e2 : τ }})%I -
......
......@@ -16,11 +16,11 @@ Proof. solve_inG. Qed.
Lemma logrel_adequate Σ `{logrelPreG Σ}
Δ e e' τ σ :
( `{logrelG Σ}, {;Δ;} e log e' : τ)
adequate e σ (λ v, thp' h v', rtc step ([e'], ) (of_val v' :: thp', h)
adequate NotStuck e σ (λ v, thp' h v', rtc step ([e'], ) (of_val v' :: thp', h)
(ObsType τ v = v')).
Proof.
intros Hlog.
eapply (heap_adequacy Σ _); iIntros (Hinv) "_".
eapply (heap_adequacy Σ _); iIntros (Hinv).
iMod (own_alloc ( (to_tpool [e'], )
((to_tpool [e'] : tpoolUR, ) : cfgUR))) as (γc) "[Hcfg1 Hcfg2]".
{ apply auth_valid_discrete_2. split=>//. split=>//. apply to_tpool_valid. }
......@@ -58,7 +58,7 @@ Theorem logrel_typesafety Σ `{logrelPreG Σ} Δ e e' τ thp σ σ' :
is_Some (to_val e') reducible e' σ'.
Proof.
intros Hlog ??.
cut (adequate e σ (λ v, thp' h v', rtc step ([e], ) (of_val v' :: thp', h) (ObsType τ v = v'))); first (intros [_ ?]; eauto).
cut (adequate NotStuck e σ (λ v, thp' h v', rtc step ([e], ) (of_val v' :: thp', h) (ObsType τ v = v'))); first (intros [_ ?]; eauto).
eapply logrel_adequate; eauto.
Qed.
......@@ -80,7 +80,7 @@ Lemma logrel_simul Σ `{logrelPreG Σ}
( thp' hp' v', rtc step ([e'], ) (of_val v' :: thp', hp') (ObsType τ v = v')).
Proof.
intros Hlog Hsteps.
cut (adequate e (λ v, thp' h v', rtc step ([e'], ) (of_val v' :: thp', h) (ObsType τ v = v'))).
cut (adequate NotStuck e (λ v, thp' h v', rtc step ([e'], ) (of_val v' :: thp', h) (ObsType τ v = v'))).
{ destruct 1; naive_solver. }
eapply logrel_adequate; eauto.
Qed.
......
......@@ -19,7 +19,7 @@ Section liftings.
iAlways. iIntros "HP"; iSpecialize ("He" with "HP").
iIntros "Hlog".
iApply bin_log_related_wp_l.
iApply (wp_mask_mono E); first done.
iApply (wp_mask_mono _ E); first done.
by iApply (wp_wand with "He").
Qed.
......
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