Commit 36b4deb5 authored by Dan Frumin's avatar Dan Frumin

Bump Iris/std++ version

parent 8294ac2d
......@@ -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 [6117c3e4a57307fd374780836a130ac86608d8cd](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/tree/6117c3e4a57307fd374780836a130ac86608d8cd)
- Iris version [c22e7b339288ee006eea1046abb80f65fc169a6f](https://gitlab.mpi-sws.org/FP/iris-coq/tree/c22e7b339288ee006eea1046abb80f65fc169a6f)
- std++ version [32570aa6e0d04633047d9fddb3cf8da1748d9695](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/tree/32570aa6e0d04633047d9fddb3cf8da1748d9695)
- Iris version [6117c3e4a57307fd374780836a130ac86608d8cd](https://gitlab.mpi-sws.org/FP/iris-coq/tree/6117c3e4a57307fd374780836a130ac86608d8cd)
# Compilation
......
......@@ -109,7 +109,7 @@ Tactic Notation "wp_bind" open_constr(efoc) :=
Lemma tac_wp_pure `{heapG Σ} K φ e1 e2 1 2 E Φ :
PureExec φ e1 e2
φ
IntoLaterNEnvs 1 1 2
MaybeIntoLaterNEnvs 1 1 2
envs_entails 2 (WP fill K e2 @ E {{ Φ }})
envs_entails 1 (WP fill K e1 @ E {{ Φ }}).
Proof.
......@@ -168,7 +168,7 @@ Implicit Types Δ : envs (iResUR Σ).
Import uPred.
Lemma tac_wp_alloc Δ Δ' E j e v Φ :
to_val e = Some v
IntoLaterNEnvs 1 Δ Δ'
MaybeIntoLaterNEnvs 1 Δ Δ'
( l, Δ'',
envs_app false (Esnoc Enil j (l ↦ᵢ v)) Δ' = Some Δ''
(envs_entails Δ'' (Φ (LitV (Loc l)))))
......@@ -181,7 +181,7 @@ Proof.
Qed.
Lemma tac_wp_load Δ Δ' E i l q v Φ :
IntoLaterNEnvs 1 Δ Δ'
MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l ↦ᵢ{q} v)%I
envs_entails Δ' (Φ v)
envs_entails Δ (WP Load (Lit (Loc l)) @ E {{ Φ }}).
......@@ -193,7 +193,7 @@ Qed.
Lemma tac_wp_store Δ Δ' Δ'' E i l v e v' Φ :
to_val e = Some v'
IntoLaterNEnvs 1 Δ Δ'
MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l ↦ᵢ v)%I
envs_simple_replace i false (Esnoc Enil i (l ↦ᵢ v')) Δ' = Some Δ''
envs_entails Δ'' (Φ (LitV LitUnit))
......@@ -206,7 +206,7 @@ Qed.
Lemma tac_wp_cas_fail Δ Δ' E i l q v e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2
IntoLaterNEnvs 1 Δ Δ'
MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l ↦ᵢ{q} v)%I v v1
envs_entails Δ' (Φ (LitV (Bool false)))
envs_entails Δ (WP CAS (Lit (Loc l)) e1 e2 @ E {{ Φ }}).
......@@ -218,7 +218,7 @@ Qed.
Lemma tac_wp_cas_suc Δ Δ' Δ'' E i l v e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2
IntoLaterNEnvs 1 Δ Δ'
MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l ↦ᵢ v)%I v = v1
envs_simple_replace i false (Esnoc Enil i (l ↦ᵢ v2)) Δ' = Some Δ''
envs_entails Δ'' (Φ (LitV (Bool true)))
......
......@@ -68,8 +68,7 @@ Section compatibility.
iMod "Hx1" as (?) "Hx1".
wp_store.
iApply "Hcl".
iNext. iRight. iExists _; iFrame.
iLeft. iFrame. }
iNext. iRight. iExists _; iFrame. }
{ iNext.
iModIntro. wp_let.
wp_bind (f2 #()). iApply (wp_wand with "Hf2").
......@@ -87,8 +86,7 @@ Section compatibility.
iDestruct "HΨ1" as "[HΨ1 | Ht']"; last first.
{ iDestruct (own_valid_2 with "Ht Ht'") as %[]. }
iMod ("Hcl" with "[Hx1 Ht]") as "_".
{ iNext. iRight. iExists _; iFrame.
iRight. iFrame. }
{ iNext. iRight. iExists _; iFrame. }
iModIntro. simpl. (* TODO: simpl is required here *) wp_case.
iSpecialize ("HΦ" with "[$HΨ1 $HΨ2]").
wp_let. by wp_value. }
......
......@@ -382,9 +382,9 @@ Section refinement.
iMod (inv_alloc stackN _ (stackInv γo st st' mb l') with "[-]") as "#Hinv".
{ iNext. unfold stackInv.
iExists _, _, _. iFrame.
iSplit; eauto. iApply stackRel_empty.
iSplitL; first eauto.
iApply offerInv_empty. }
iSplit; eauto.
- iApply stackRel_empty.
- iApply offerInv_empty. }
iApply bin_log_related_pair; last first.
(* * Push refinement *)
{ iApply bin_log_related_arrow_val; eauto.
......@@ -531,7 +531,7 @@ Section refinement.
rel_seq_l. rel_case_l.
rel_seq_l.
iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists _, _, _; iFrame. eauto. }
{ iNext. iExists _, _, _; iFrame. }
by iApply stack_pull_no_offer. (* TODO *)
- (* YES OFFER *)
iDestruct "Hmb" as (l v γ j K) "[Hmb >HNl]".
......
From iris.proofmode Require Export tactics.
From iris.base_logic Require Export namespaces invariants.
From iris.base_logic Require Export invariants.
From iris_logrel.F_mu_ref_conc Require Export lang notation tactics.
From iris_logrel.logrel Require Export fundamental_binary soundness_binary.
From iris_logrel.logrel.proofmode Require Export tactics_threadpool tactics_rel.
......@@ -259,7 +259,7 @@ Tactic Notation "rel_alloc_l_atomic" := rel_apply_l bin_log_related_alloc_l.
Lemma tac_rel_alloc_l_simp `{logrelG Σ} 1 2 Δ Γ e t e' v' K τ :
e = fill K (Alloc e')
IntoLaterNEnvs 1 1 2
MaybeIntoLaterNEnvs 1 1 2
to_val e' = Some v'
(envs_entails 2 ( l,
(l ↦ᵢ v' - bin_log_related Δ Γ (fill K (Lit (Loc l))) t τ)))
......@@ -275,7 +275,7 @@ Tactic Notation "rel_alloc_l" "as" ident(l) constr(H) :=
iStartProof;
eapply tac_rel_alloc_l_simp;
[tac_bind_helper (* e = fill K' .. *)
|apply _ (* IntoLaterNEnvs _ _ _ *)
|apply _ (* MaybeIntoLaterNEnvs _ _ _ *)
|solve_to_val (* to_val e' = Some v *)
|simpl; iIntros (l) H (* new goal *)].
......@@ -309,7 +309,7 @@ Tactic Notation "rel_load_l_atomic" := rel_apply_l bin_log_related_load_l.
Lemma tac_rel_load_l_simp `{logrelG Σ} 1 2 i1 Δ Γ (l : loc) q v K e t eres τ :
e = fill K (Load (# l))
IntoLaterNEnvs 1 1 2
MaybeIntoLaterNEnvs 1 1 2
envs_lookup i1 2 = Some (false, l ↦ᵢ{q} v)%I
eres = fill K (of_val v)
envs_entails 2 (bin_log_related Δ Γ eres t τ)
......@@ -367,7 +367,7 @@ Tactic Notation "rel_store_l_atomic" := rel_apply_l bin_log_related_store_l.
Lemma tac_rel_store_l_simp `{logrelG Σ} 1 2 3 i1 Δ Γ K (l : loc) v e' v' e t eres τ :
e = fill K (Store (# l) e')
to_val e' = Some v'
IntoLaterNEnvs 1 1 2
MaybeIntoLaterNEnvs 1 1 2
envs_lookup i1 2 = Some (false, l ↦ᵢ v)%I
envs_simple_replace i1 false (Esnoc Enil i1 (l ↦ᵢ v')) 2 = Some 3
eres = fill K Unit
......@@ -389,7 +389,7 @@ Tactic Notation "rel_store_l" :=
eapply (tac_rel_store_l_simp);
[tac_bind_helper (* e = fill K' .. *)
|solve_to_val (* to_val e' = Some v' *)
|apply _ (* IntoLaterNEnvs *)
|apply _ (* MaybeIntoLaterNEnvs *)
|iAssumptionCore || fail "rel_store_l: cannot find '? ↦ᵢ ?'"
|env_cbv; reflexivity || fail "rel_store_l: this should not happen"
|simpl; reflexivity (* eres = fill K () *)
......
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