Commit 8f6100ac authored by Ralf Jung's avatar Ralf Jung

update dependencies; fix for Iris notation/coercion change

parent c3ed7269
......@@ -9,7 +9,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/FP/iris-examples.git"
synopsis: "A collection of case studies for Iris"
depends: [
"coq-iris" { (= "dev.2020-03-12.1.9f19f1ab") | (= "dev") }
"coq-iris" { (= "dev.2020-03-16.0.62be0a86") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
......
......@@ -37,7 +37,7 @@ Section client.
iApply (wp_wand with "[]"). iApply "Hf". by iIntros (v) "_".
Qed.
Lemma client_safe : WP client {{ _, True }}%I.
Lemma client_safe : WP client {{ _, True }}.
Proof.
iIntros ""; rewrite /client. wp_alloc y as "Hy". wp_let.
wp_apply (newbarrier_spec N (y_inv 1 y) with "[//]").
......
......@@ -11,11 +11,11 @@ Context `{!heapG Σ, !barrierG Σ}.
Lemma barrier_spec (N : namespace) :
recv send : loc iPropO Σ -n> iPropO Σ,
( P, {{ True }} newbarrier #()
( P, {{ True }} newbarrier #()
{{ v, l : loc, v = #l recv l P send l P }})
( l P, {{ send l P P }} signal #l {{ _, True }})
( l P, {{ recv l P }} wait #l {{ _, P }})
( l P Q, recv l (P Q) ={N}=> recv l P recv l Q)
( l P, {{ send l P P }} signal #l {{ _, True }})
( l P, {{ recv l P }} wait #l {{ _, P }})
( l P Q, recv l (P Q) ={N}= recv l P recv l Q)
( l P Q, (P - Q) - recv l P - recv l Q).
Proof.
exists (λ l, OfeMor (recv N l)), (λ l, OfeMor (send N l)).
......@@ -24,7 +24,7 @@ Proof.
iNext. eauto.
- iIntros (l P) "!# [Hl HP]". iApply (signal_spec with "[$Hl $HP]"). by eauto.
- iIntros (l P) "!# Hl". iApply (wait_spec with "Hl"). eauto.
- iIntros (l P Q) "!#". by iApply recv_split.
- iIntros (l P Q). by iApply recv_split.
- apply recv_weaken.
Qed.
End spec.
......@@ -40,22 +40,22 @@ Proof.
split; [done | apply _].
Qed.
Lemma new_INIT `{saG Σ} : (|==> γ, INIT γ 1%Qp)%I.
Lemma new_INIT `{saG Σ} : |==> γ, INIT γ 1%Qp.
Proof. by apply own_alloc. Qed.
Lemma INIT_not_SET_RES `{saG Σ} γ q q' v :
(INIT γ q - SET_RES γ q' v - False)%I.
INIT γ q - SET_RES γ q' v - False.
Proof.
iIntros "Hs Hp".
iDestruct (own_valid_2 with "Hs Hp") as %[].
Qed.
Lemma INIT_not_FIN `{saG Σ} γ q v :
(INIT γ q - FIN γ v - False)%I.
INIT γ q - FIN γ v - False.
Proof.
iIntros "Hs Hp".
iDestruct (own_valid_2 with "Hs Hp") as %[].
Qed.
Lemma SET_RES_not_FIN `{saG Σ} γ q v v' :
(SET_RES γ q v - FIN γ v' - False)%I.
SET_RES γ q v - FIN γ v' - False.
Proof.
iIntros "Hs Hp".
iDestruct (own_valid_2 with "Hs Hp") as %[].
......
......@@ -14,7 +14,7 @@ Proof. solve_inG. Qed.
Definition pending `{oneshotG Σ} γ q := own γ (Cinl q%Qp).
Definition shot `{oneshotG Σ} γ (v: val) := own γ (Cinr (to_agree v)).
Lemma new_pending `{oneshotG Σ} : (|==> γ, pending γ 1%Qp)%I.
Lemma new_pending `{oneshotG Σ} : |==> γ, pending γ 1%Qp.
Proof. by apply own_alloc. Qed.
Lemma shoot `{oneshotG Σ} (v: val) γ : pending γ 1%Qp == shot γ v.
Proof.
......
......@@ -260,7 +260,7 @@ Section example_1.
(* Prove that incr is safe w.r.t. data race. TODO: prove a stronger post-condition *)
Lemma incr_2_safe:
(x: Z), (WP incr_2 #x {{ _, True }})%I.
(x: Z), WP incr_2 #x {{ _, True }}.
Proof.
iIntros (x).
rewrite /incr_2 /=.
......
......@@ -133,7 +133,7 @@ Section factorial_client.
if: "x" = #0 then #0 else "y" + "times" ("x" - #1) "y".
Lemma times_spec_aux (m : Z):
( n Φ , Φ (# (n * m)) - WP times #n #m {{ Φ }})%I.
n Φ , Φ (# (n * m)) - WP times #n #m {{ Φ }}.
Proof.
iLöb as "IH".
iIntros (n Φ) "ret".
......@@ -176,9 +176,9 @@ Section factorial_client.
really does implement the mathematical factorial function. *)
Lemma myfac_spec (n: Z):
(0 n)
{{{ True}}}
{{{ True }}}
myfac #n
{{{v, RET v; v = #(fac_int n)}}}.
{{{ v, RET v; v = #(fac_int n) }}}.
Proof.
iIntros (Hleq Φ) "_ ret"; simplify_eq. unfold myfac. wp_pures.
iApply (myrec_spec (fun v => m' : Z, 0 m' to_val v = Some #m'%I)
......
......@@ -149,7 +149,7 @@ Implicit Types pvs : list nat.
(** Operations for the CMRA representing the logical contents of the queue. *)
Lemma new_elts l : (|==> γe, own γe ( Excl' l) own γe ( Excl' l))%I.
Lemma new_elts l : |==> γe, own γe ( Excl' l) own γe ( Excl' l).
Proof.
iMod (own_alloc ( Excl' l Excl' l)) as (γe) "[H● H◯]".
- by apply auth_both_valid.
......@@ -186,7 +186,7 @@ Proof. iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %?. Qed.
Definition back_value γb n := own γb ( (n : mnatUR) : backUR).
Definition back_lower_bound γb n := own γb ( (n : mnatUR) : backUR).
Lemma new_back : (|==> γb, back_value γb 0%nat)%I.
Lemma new_back : |==> γb, back_value γb 0%nat.
Proof.
iMod (own_alloc ( (0%nat : mnatUR) : backUR)) as (γb) "H●".
- by rewrite auth_auth_valid.
......@@ -194,21 +194,21 @@ Proof.
Qed.
Lemma back_incr γb n :
(back_value γb n == back_value γb (S n)%nat)%I.
back_value γb n == back_value γb (S n)%nat.
Proof.
iIntros "H●". iMod (own_update with "H●") as "[$ _]"; last done.
apply auth_update_alloc, (mnat_local_update _ _ (S n)). by lia.
Qed.
Lemma back_snapshot γb n :
(back_value γb n == back_value γb n back_lower_bound γb n)%I.
back_value γb n == back_value γb n back_lower_bound γb n.
Proof.
iIntros "H●". rewrite -own_op. iApply (own_update with "H●").
by apply auth_update_alloc, mnat_local_update.
Qed.
Lemma back_le γb n1 n2 :
(back_value γb n1 - back_lower_bound γb n2 - n2 n1%nat)%I.
back_value γb n1 - back_lower_bound γb n2 - n2 n1%nat.
Proof.
iIntros "H1 H2". iCombine "H1 H2" as "H".
iDestruct (own_valid with "H") as %Hvalid. iPureIntro.
......@@ -226,14 +226,14 @@ Definition no_contra_wit γi n := back_lower_bound γi n.
Lemma i2_lower_bound_update γi n m :
(n m)%nat
(i2_lower_bound γi n == i2_lower_bound γi m)%I.
i2_lower_bound γi n == i2_lower_bound γi m.
Proof.
iIntros (H) "H●". iMod (own_update with "H●") as "[$ _]"; last done.
apply auth_update_alloc, (mnat_local_update _ _ m). by lia.
Qed.
Lemma i2_lower_bound_snapshot γi n :
(i2_lower_bound γi n == i2_lower_bound γi n no_contra_wit γi n)%I.
i2_lower_bound γi n == i2_lower_bound γi n no_contra_wit γi n.
Proof.
iIntros "H●". rewrite -own_op. iApply (own_update with "H●").
by apply auth_update_alloc, mnat_local_update.
......@@ -249,18 +249,18 @@ Definition no_contra γc :=
Definition contra γc (i1 i2 : nat) :=
own γc (Cinr (to_agree (i1, i2))).
Lemma new_no_contra : (|==> γc, no_contra γc)%I.
Lemma new_no_contra : |==> γc, no_contra γc.
Proof. by apply own_alloc. Qed.
Lemma to_contra i1 i2 γc : no_contra γc == contra γc i1 i2.
Proof. apply own_update. by apply cmra_update_exclusive. Qed.
Lemma contra_not_no_contra i1 i2 γc :
(no_contra γc - contra γc i1 i2 - False)%I.
no_contra γc - contra γc i1 i2 - False.
Proof. iIntros "HnoC HC". iDestruct (own_valid_2 with "HnoC HC") as %[]. Qed.
Lemma contra_agree i1 i2 i1' i2' γc :
(contra γc i1 i2 - contra γc i1' i2' - i1' = i1 i2' = i2)%I.
contra γc i1 i2 - contra γc i1' i2' - i1' = i1 i2' = i2.
Proof.
iIntros "HC HC'". iDestruct (own_valid_2 with "HC HC'") as %H.
iPureIntro. apply agree_op_invL' in H. by inversion H.
......@@ -378,7 +378,7 @@ Definition slot_writing_tok γs i :=
own γs ( {[i := (None, None, None, None, not_shot)]} : slotUR).
(* Initial slot data, with not allocated slots. *)
Lemma new_slots : (|==> γs, own γs ( ))%I.
Lemma new_slots : |==> γs, own γs ( ).
Proof.
iMod (own_alloc ( )) as (γs) "[H● _]".
- by apply auth_both_valid.
......@@ -431,9 +431,9 @@ Proof.
Qed.
Lemma use_val_wit γs slots i l :
(own γs ( (of_slot_data <$> slots) : slotUR) -
own γs ( (of_slot_data <$> slots) : slotUR) -
slot_val_wit γs i l -
val_of <$> slots !! i = Some l)%I.
val_of <$> slots !! i = Some l.
Proof.
iIntros "H● Hwit". iDestruct (own_valid_2 with "H● Hwit") as %H.
iPureIntro. apply auth_both_valid in H as [H%singleton_included _].
......@@ -461,9 +461,9 @@ Proof.
Qed.
Lemma use_name_tok γs slots i γ :
(own γs ( (of_slot_data <$> slots) : slotUR) -
own γs ( (of_slot_data <$> slots) : slotUR) -
slot_name_tok γs i γ -
name_of <$> slots !! i = Some (Some γ))%I.
name_of <$> slots !! i = Some (Some γ).
Proof.
iIntros "H● Hwit". iDestruct (own_valid_2 with "H● Hwit") as %H.
iPureIntro. apply auth_both_valid in H as [H%singleton_included _].
......@@ -527,9 +527,9 @@ Proof.
Qed.
Lemma use_committed_wit γs slots i :
(own γs ( (of_slot_data <$> slots) : slotUR) -
own γs ( (of_slot_data <$> slots) : slotUR) -
slot_committed_wit γs i -
was_committed <$> slots !! i = Some true)%I.
was_committed <$> slots !! i = Some true.
Proof.
iIntros "H● Hwit". iDestruct (own_valid_2 with "H● Hwit") as %H.
iPureIntro. apply auth_both_valid in H as [H%singleton_included _].
......@@ -550,9 +550,9 @@ Proof.
Qed.
Lemma use_written_wit γs slots i :
(own γs ( (of_slot_data <$> slots) : slotUR) -
own γs ( (of_slot_data <$> slots) : slotUR) -
slot_written_wit γs i -
was_written <$> slots !! i = Some true)%I.
was_written <$> slots !! i = Some true.
Proof.
iIntros "H● Hwit". iDestruct (own_valid_2 with "H● Hwit") as %H.
iPureIntro. apply auth_both_valid in H as [H%singleton_included _].
......@@ -1401,12 +1401,12 @@ Qed.
Lemma big_lemma γe γs (ls : list loc) slots (p : list nat) :
NoDup p
( i, i p was_committed <$> slots !! i = Some false)
(own γs ( (of_slot_data <$> slots) : slotUR) -
own γs ( (of_slot_data <$> slots) : slotUR) -
([ map] i d slots, per_slot_own γe γs i d) -
own γe ( (Excl' ls)) ={ N}=
own γs ( (of_slot_data <$> map_imap (helped p) slots) : slotUR)
([ map] i d map_imap (helped p) slots, per_slot_own γe γs i d)
own γe ( (Excl' (ls ++ get_values slots p))))%I.
own γe ( (Excl' (ls ++ get_values slots p))).
Proof.
revert p. iIntros (p).
iInduction p as [|n ps] "IH" forall (slots ls); iIntros (HNoDup H) "Hs● Hbig He●".
......
......@@ -112,7 +112,7 @@ Section to_gc_map.
End to_gc_map.
Lemma gc_init `{!invG Σ, !heapG Σ, !gcPreG Σ} E:
(|==> _ : gcG Σ, |={E}=> gc_inv)%I.
|==> _ : gcG Σ, |={E}=> gc_inv.
Proof.
iMod (own_alloc ( (to_gc_map ))) as (γ) "H●".
{ rewrite auth_auth_valid. exact: to_gc_map_valid. }
......
......@@ -97,9 +97,9 @@ Section proof.
Qed.
Lemma push_atomic_spec (s: loc) (x: val) :
<<< (xs : list val), is_stack s xs >>>
push #s x @
<<< is_stack s (x::xs), RET #() >>>.
<<< (xs : list val), is_stack s xs >>>
push #s x @
<<< is_stack s (x::xs), RET #() >>>.
Proof.
unfold is_stack.
iIntros (Φ) "HP". iLöb as "IH". wp_rec.
......@@ -123,11 +123,11 @@ Section proof.
Qed.
Lemma pop_atomic_spec (s: loc) :
<<< (xs : list val), is_stack s xs >>>
pop #s @
<<< match xs with [] => is_stack s []
| x::xs' => is_stack s xs' end,
RET match xs with [] => NONEV | x :: _ => SOMEV x end >>>.
<<< (xs : list val), is_stack s xs >>>
pop #s @
<<< match xs with [] => is_stack s []
| x::xs' => is_stack s xs' end,
RET match xs with [] => NONEV | x :: _ => SOMEV x end >>>.
Proof.
unfold is_stack.
iIntros (Φ) "HP". iLöb as "IH". wp_rec.
......
......@@ -161,7 +161,7 @@ Section logrel.
rewrite lookup_zip_with; by simplify_option_eq.
Qed.
Lemma interp_env_nil Δ : ( [] * Δ [])%I.
Lemma interp_env_nil Δ : [] * Δ [].
Proof. iSplit; rewrite ?zip_with_nil_r; auto. Qed.
Lemma interp_env_cons Δ Γ vs τ v :
τ :: Γ * Δ (v :: vs) τ Δ v Γ * Δ vs.
......
......@@ -176,7 +176,7 @@ Section logrel.
rewrite lookup_zip_with; by simplify_option_eq.
Qed.
Lemma interp_env_nil Δ : ( [] * Δ [])%I.
Lemma interp_env_nil Δ : [] * Δ [].
Proof. iSplit; simpl; auto. Qed.
Lemma interp_env_cons Δ Γ vs τ v :
τ :: Γ * Δ (v :: vs) τ Δ v Γ * Δ vs.
......
......@@ -211,7 +211,7 @@ Section logrel.
rewrite lookup_zip_with; by simplify_option_eq.
Qed.
Lemma interp_env_nil Δ : [] * Δ [].
Lemma interp_env_nil Δ : [] * Δ [].
Proof. iSplit; simpl; auto. Qed.
Lemma interp_env_cons Δ Γ vvs τ vv :
τ :: Γ * Δ (vv :: vvs) τ Δ vv Γ * Δ vvs.
......
......@@ -223,7 +223,7 @@ Section logrel.
rewrite lookup_zip_with; by simplify_option_eq.
Qed.
Lemma interp_env_nil Δ : [] * Δ [].
Lemma interp_env_nil Δ : [] * Δ [].
Proof. iSplit; simpl; auto. Qed.
Lemma interp_env_cons Δ Γ vvs τ vv :
τ :: Γ * Δ (vv :: vvs) τ Δ vv Γ * Δ vvs.
......
......@@ -179,7 +179,7 @@ Section logrel.
rewrite lookup_zip_with; by simplify_option_eq.
Qed.
Lemma interp_env_nil Δ : [] * Δ [].
Lemma interp_env_nil Δ : [] * Δ [].
Proof. iSplit; simpl; auto. Qed.
Lemma interp_env_cons Δ Γ vs τ v :
τ :: Γ * Δ (v :: vs) τ Δ v Γ * Δ vs.
......
......@@ -36,7 +36,7 @@ Notation "⟦ Γ ⟧*" := (interp_env Γ).
Global Instance interp_env_persistent Γ vs :
Persistent ( Γ * vs) := _.
Lemma interp_env_nil : ( [] * [])%I.
Lemma interp_env_nil : [] * [].
Proof. iSplit; simpl; auto. Qed.
Lemma interp_env_cons Γ vs τ v :
τ :: Γ * (v :: vs) τ v Γ * vs.
......
......@@ -2,7 +2,7 @@ From iris_examples.logrel.stlc Require Export fundamental.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Import adequacy.
Lemma wp_soundness `{irisG stlc_lang Σ} e τ : [] e : τ (WP e {{ τ }})%I.
Lemma wp_soundness `{irisG stlc_lang Σ} e τ : [] e : τ WP e {{ τ }}.
Proof.
iIntros (?).
replace e with e.[env_subst[]] by by asimpl.
......
......@@ -37,7 +37,7 @@ Section symbol_ghosts.
Global Instance symbol_persistent γ n : Persistent (symbol γ n).
Proof. apply _. Qed.
Lemma counter_alloc n : (|==> γ, counter γ n)%I.
Lemma counter_alloc n : |==> γ, counter γ n.
Proof.
iMod (own_alloc ( (n:mnat) (n:mnat))) as (γ) "[Hγ Hγf]";
first by apply auth_both_valid.
......@@ -71,7 +71,7 @@ Section ltyped_symbol_adt.
Definition lty_symbol (γ : gname) : lty Σ := Lty (λ w,
n : nat, w = #n symbol γ n)%I.
Lemma ltyped_symbol_adt Γ : Γ symbol_adt : symbol_adt_ty.
Lemma ltyped_symbol_adt Γ : Γ symbol_adt : symbol_adt_ty.
Proof.
iIntros (vs) "!# _ /=". iApply wp_value.
iIntros "!#" (v ->). wp_lam. wp_alloc l as "Hl"; wp_pures.
......
......@@ -103,7 +103,7 @@ Definition ltyped `{heapG Σ}
(Γ : gmap string (lty Σ)) (e : expr) (A : lty Σ) : iProp Σ :=
( vs, env_ltyped Γ vs - WP subst_map vs e {{ A }})%I.
Notation "Γ ⊨ e : A" := (ltyped Γ e A)
(at level 100, e at next level, A at level 200).
(at level 100, e at next level, A at level 200) : bi_scope.
(* To unfold a recursive type, we need to take a step. We thus define the
unfold operator to be the identity function. *)
......@@ -194,18 +194,18 @@ Section types_properties.
Qed.
(* The semantic typing rules *)
Lemma ltyped_var Γ (x : string) A : Γ !! x = Some A Γ x : A.
Lemma ltyped_var Γ (x : string) A : Γ !! x = Some A Γ x : A.
Proof.
iIntros (HΓx vs) "!# #HΓ /=".
iDestruct (env_ltyped_lookup with "HΓ") as (v ->) "HA"; first done.
by iApply wp_value.
Qed.
Lemma ltyped_unit Γ : Γ #() : ().
Lemma ltyped_unit Γ : Γ #() : ().
Proof. iIntros (vs) "!# _ /=". by iApply wp_value. Qed.
Lemma ltyped_bool Γ (b : bool) : Γ #b : lty_bool.
Lemma ltyped_bool Γ (b : bool) : Γ #b : lty_bool.
Proof. iIntros (vs) "!# _ /=". iApply wp_value. rewrite /lty_car /=. eauto. Qed.
Lemma ltyped_int Γ (n : Z) : Γ #n : lty_int.
Lemma ltyped_int Γ (n : Z) : Γ #n : lty_int.
Proof. iIntros (vs) "!# _ /=". iApply wp_value. rewrite /lty_car /=. eauto. Qed.
Lemma ltyped_rec Γ f x e A1 A2 :
......
......@@ -3,7 +3,7 @@ From iris.heap_lang Require Import adequacy.
From iris.heap_lang Require Import proofmode.
Lemma ltyped_safety `{heapPreG Σ} e σ es σ' e' :
( `{heapG Σ}, A, e : A)
( `{heapG Σ}, A, e : A)
rtc erased_step ([e], σ) (es, σ') e' es
is_Some (to_val e') reducible e' σ'.
Proof.
......
......@@ -41,11 +41,11 @@ Record TypedProph := mkTypedProph
; typed_proph_inj_prop :
x, typed_proph_from_val (typed_proph_to_val x) = Some x
; typed_proph_prop : proph_id list typed_proph_type iProp
; typed_proph_prop_excl : ( p l1 l2, typed_proph_prop p l1 typed_proph_prop p l2 - False)%I
; typed_proph_prop_excl : p l1 l2, typed_proph_prop p l1 typed_proph_prop p l2 - False
; typed_proph_wp_new_proph s E :
{{{ True }}}
NewProph @ s; E
{{{ pvs p, RET (LitV (LitProphecy p)); typed_proph_prop p pvs }}}%I
{{{ pvs p, RET (LitV (LitProphecy p)); typed_proph_prop p pvs }}}
; typed_proph_wp_resolve s E e Φ p v w pvs :
Atomic StronglyAtomic e
to_val e = None
......@@ -56,11 +56,11 @@ Record TypedProph := mkTypedProph
; typed_proph1_prop `{Inhabited typed_proph_type}
: proph_id typed_proph_type iProp
; typed_proph1_prop_excl `{!Inhabited typed_proph_type}
: ( p o1 o2, typed_proph1_prop p o1 typed_proph1_prop p o2 - False)%I
: p o1 o2, typed_proph1_prop p o1 typed_proph1_prop p o2 - False
; typed_proph_wp_new_proph1 `{!Inhabited typed_proph_type} s E :
{{{ True }}}
NewProph @ s; E
{{{ v p, RET #p; typed_proph1_prop p v }}}%I
{{{ v p, RET #p; typed_proph1_prop p v }}}
; typed_proph_wp_resolve1 `{!Inhabited typed_proph_type} s E e Φ p w v1 v2 :
Atomic StronglyAtomic e
to_val e = None
......@@ -89,7 +89,7 @@ Next Obligation.
Qed.
Next Obligation.
intros spec.
iIntros (s E Φ). iIntros "!> _ HΦ". wp_apply wp_new_proph; first done.
iIntros (s E Φ) "_ HΦ". wp_apply wp_new_proph; first done.
iIntros (pvs p) "Hp". iApply "HΦ". iExists pvs. by iFrame.
Qed.
Next Obligation.
......@@ -109,7 +109,7 @@ Next Obligation.
Qed.
Next Obligation.
intros spec ?.
iIntros (s E Φ). iIntros "!> _ HΦ". wp_apply wp_new_proph; first done.
iIntros (s E Φ) "_ HΦ". wp_apply wp_new_proph; first done.
iIntros (pvs p) "Hp". iApply "HΦ". iExists pvs. by iFrame.
Qed.
Next Obligation.
......
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