...
 
Commits (42)
......@@ -43,8 +43,14 @@ Changes in heap_lang:
typically provided in systems languages (C, C++, Rust).
The comparison by this operation also got weakened to be efficiently
implementable: CmpXchg may only be used to compare "unboxed" values that can
be represented in a single machine word.
* Implement prophecy variables using the new support for "observations".
be represented in a single machine word. It is sufficient if one of the two
compared values is unboxed.
* For consistency, the restrictions CmpXchg imposes on comparison also apply to
the `=` binary operator. This also fixes the long-standing problem that that
operator allowed compared closures with each other.
* Implement prophecy variables using the new support for "observations". The
erasure theorem (showing that prophecy variables do not alter program
behavior) can be found [in the iris/examples repository](https://gitlab.mpi-sws.org/iris/examples/blob/3f33781fe6e19cfdb25259c8194d34403f1134d5/theories/logatom/proph_erasure.v).
* heap_lang now uses right-to-left evaluation order. This makes it
significantly easier to write specifications of curried functions.
* heap_lang values are now injected in heap_lang expressions via a specific
......@@ -56,10 +62,6 @@ Changes in heap_lang:
* heap_lang now has support for allocating, accessing and reasoning about arrays
(continuously allocated regions of memory).
* One can now assign "meta" data to heap_lang locations.
* For comparison operation (the binary operator and CmpXchg), all closures are
"normalized" to the same. This makes all closures indistinguishable from each
other while remaining unqueal to anything else. We also use the same
"normalization" to make sure all prophecy variables seem equal to `()`.
Changes in Coq:
......
......@@ -105,6 +105,12 @@ Further tactics:
There is no tactic for `Fork`, just do `wp_apply wp_fork`.
To verify a recursive function, use `iLöb`. Make sure you do `wp_pures` before
running `iLöb`; otherwise the induction hypothesis will likely not be applicable
when you need it. (This makes sure that all administrative redexes are reduced
in your induction hypothesis, just like we state our `WP` specifications with
all of the redexes reduced.)
## Notation and lemmas for derived notions involving a thunk
Sometimes, it is useful to define a derived notion in HeapLang that involves
......
......@@ -12,5 +12,5 @@ install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
"coq" { (= "8.7.2") | (= "8.8.2") | (>= "8.9" & < "8.11~") | (= "dev") }
"coq-stdpp" { (= "dev.2019-06-25.0.4ff965b2") | (= "dev") }
"coq-stdpp" { (= "dev.2019-07-08.0.2e0bf441") | (= "dev") }
]
......@@ -76,8 +76,9 @@ Section tests.
Definition heap_e6 : val := λ: "v", "v" = "v".
Lemma heap_e6_spec (v : val) : (WP heap_e6 v {{ w, w = #true }})%I.
Proof. wp_lam. wp_op. by case_bool_decide. Qed.
Lemma heap_e6_spec (v : val) :
val_is_unboxed v (WP heap_e6 v {{ w, w = #true }})%I.
Proof. intros ?. wp_lam. wp_op. by case_bool_decide. Qed.
Definition heap_e7 : val := λ: "v", CmpXchg "v" #0 #1.
......
......@@ -362,8 +362,23 @@ Proof.
exists a'. split; [done|]. split; [|done]. exists bf2.
by rewrite left_id -assoc.
Qed.
Lemma auth_update_alloc a a' b' : (a,ε) ~l~> (a',b') a ~~> a' b'.
Proof. intros. rewrite -(right_id _ _ ( a)). by apply auth_update. Qed.
Lemma auth_update_auth a a' b' : (a,ε) ~l~> (a',b') a ~~> a'.
Proof.
intros. etrans; first exact: auth_update_alloc.
exact: cmra_update_op_l.
Qed.
Lemma auth_update_core_id a b `{!CoreId b} :
b a a ~~> a b.
Proof.
intros Hincl. apply: auth_update_alloc.
rewrite -(left_id ε _ b). apply: core_id_local_update. done.
Qed.
Lemma auth_update_dealloc a b a' : (a,b) ~l~> (a',ε) a b ~~> a'.
Proof. intros. rewrite -(right_id _ _ ( a')). by apply auth_update. Qed.
......
......@@ -76,6 +76,7 @@ Structure cmraT := CmraT' {
cmra_validN : ValidN cmra_car;
cmra_ofe_mixin : OfeMixin cmra_car;
cmra_mixin : CmraMixin cmra_car;
(* always same as [cmra_car], but by also having this as last field unification sometimes gets faster *)
_ : Type
}.
Arguments CmraT' _ {_ _ _ _ _ _} _ _ _.
......@@ -362,10 +363,6 @@ Proof.
intros Hv Hx%cmra_pcore_l. move: Hv; rewrite -Hx. apply cmra_valid_op_l.
Qed.
(** ** CoreId elements *)
Lemma core_id_dup x `{!CoreId x} : x x x.
Proof. by apply cmra_pcore_dup' with x. Qed.
(** ** Exclusive elements *)
Lemma exclusiveN_l n x `{!Exclusive x} y : {n} (x y) False.
Proof. intros. eapply (exclusive0_l x y), cmra_validN_le; eauto with lia. Qed.
......@@ -462,11 +459,28 @@ Proof.
by rewrite Hx1 Hx2.
Qed.
(** ** CoreId elements *)
Lemma core_id_dup x `{!CoreId x} : x x x.
Proof. by apply cmra_pcore_dup' with x. Qed.
Lemma core_id_extract x y `{!CoreId x} :
x y y y x.
Proof.
intros ?.
destruct (cmra_pcore_mono' x y x) as (cy & Hcy & [x' Hx']); [done|exact: core_id|].
rewrite -(cmra_pcore_r y) //. rewrite Hx' -!assoc. f_equiv.
rewrite [x' x]comm assoc -core_id_dup. done.
Qed.
(** ** Total core *)
Section total_core.
Local Set Default Proof Using "Type*".
Context `{CmraTotal A}.
Lemma cmra_pcore_core x : pcore x = Some (core x).
Proof.
rewrite /core /core'. destruct (cmra_total x) as [cx ->]. done.
Qed.
Lemma cmra_core_l x : core x x x.
Proof.
destruct (cmra_total x) as [cx Hcx]. by rewrite /core /= Hcx cmra_pcore_l.
......@@ -1127,6 +1141,13 @@ Section prod.
Lemma pair_valid (a : A) (b : B) : (a, b) a b.
Proof. done. Qed.
Lemma pair_core `{!CmraTotal A, !CmraTotal B} (a : A) (b : B) :
core (a, b) = (core a, core b).
Proof.
rewrite /core /core' {1}/pcore /=.
rewrite (cmra_pcore_core a) /= (cmra_pcore_core b). done.
Qed.
Global Instance prod_cmra_total : CmraTotal A CmraTotal B CmraTotal prodR.
Proof.
intros H1 H2 [a b]. destruct (H1 a) as [ca ?], (H2 b) as [cb ?].
......
......@@ -189,6 +189,10 @@ Proof.
+ exists (Cinl c); by constructor.
+ exists (Cinr c); by constructor.
Qed.
Lemma Cinl_included a a' : Cinl a Cinl a' a a'.
Proof. rewrite csum_included. naive_solver. Qed.
Lemma Cinr_included b b' : Cinr b Cinr b' b b'.
Proof. rewrite csum_included. naive_solver. Qed.
Lemma csum_includedN n x y :
x {n} y y = CsumBot ( a a', x = Cinl a y = Cinl a' a {n} a')
......
......@@ -61,19 +61,23 @@ Section gmultiset.
Lemma gmultiset_update X Y : X ~~> Y.
Proof. done. Qed.
Lemma gmultiset_local_update_alloc X Y X' : (X,Y) ~l~> (X X', Y X').
Lemma gmultiset_local_update X Y X' Y' : X Y' = X' Y (X,Y) ~l~> (X', Y').
Proof.
rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
split. done. rewrite !gmultiset_op_disj_union.
by rewrite -!assoc (comm _ Z' X').
intros HXY. rewrite local_update_unital_discrete=> Z' _. intros ->%leibniz_equiv.
split; first done. apply leibniz_equiv_iff, (inj ( Y)).
rewrite -HXY !gmultiset_op_disj_union.
by rewrite -(comm_L _ Y) (comm_L _ Y') assoc_L.
Qed.
Lemma gmultiset_local_update_alloc X Y X' : (X,Y) ~l~> (X X', Y X').
Proof. apply gmultiset_local_update. by rewrite (comm_L _ Y) assoc_L. Qed.
Lemma gmultiset_local_update_dealloc X Y X' :
X' X X' Y (X,Y) ~l~> (X X', Y X').
X' Y (X,Y) ~l~> (X X', Y X').
Proof.
intros ->%gmultiset_disj_union_difference ->%gmultiset_disj_union_difference.
rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
split. done. rewrite !gmultiset_op_disj_union=> x.
intros ->%gmultiset_disj_union_difference. apply local_update_total_valid.
intros _ _ ->%gmultiset_included%gmultiset_disj_union_difference.
apply gmultiset_local_update. apply gmultiset_eq=> x.
repeat (rewrite multiplicity_difference || rewrite multiplicity_disj_union).
lia.
Qed.
......
......@@ -59,6 +59,14 @@ Section updates.
destruct mz as [z|]; [|done]. by destruct (id_freeN_r n n x z).
Qed.
Lemma core_id_local_update x y z `{!CoreId y} :
y x (x, z) ~l~> (x, z y).
Proof.
intros Hincl n mf ? Heq; simpl in *; split; first done.
rewrite [x]core_id_extract // Heq. destruct mf as [f|]; last done.
simpl. rewrite -assoc [f y]comm assoc //.
Qed.
Lemma local_update_discrete `{!CmraDiscrete A} (x y x' y' : A) :
(x,y) ~l~> (x',y') mz, x x y ? mz x' x' y' ? mz.
Proof.
......
......@@ -1301,7 +1301,7 @@ Section sigT.
on the first component.
*)
Instance sigT_dist : Dist (sigT P) := λ n x1 x2,
eq : projT1 x1 = projT1 x2, rew eq in projT2 x1 {n} projT2 x2.
Heq : projT1 x1 = projT1 x2, rew Heq in projT2 x1 {n} projT2 x2.
(**
Usually we'd give a direct definition, and show it equivalent to
......@@ -1319,11 +1319,11 @@ Section sigT.
reflexivity _.
Definition sigT_dist_eq x1 x2 n : (x1 {n} x2)
eq : projT1 x1 = projT1 x2, (rew eq in projT2 x1) {n} projT2 x2 :=
Heq : projT1 x1 = projT1 x2, (rew Heq in projT2 x1) {n} projT2 x2 :=
reflexivity _.
Definition sigT_dist_proj1 n {x y} : x {n} y projT1 x = projT1 y := proj1_ex.
Definition sigT_equiv_proj1 x y : x y projT1 x = projT1 y := λ H, proj1_ex (H 0).
Definition sigT_equiv_proj1 {x y} : x y projT1 x = projT1 y := λ H, proj1_ex (H 0).
Definition sigT_ofe_mixin : OfeMixin (sigT P).
Proof.
......@@ -1342,16 +1342,47 @@ Section sigT.
Canonical Structure sigTO : ofeT := OfeT (sigT P) sigT_ofe_mixin.
Lemma sigT_equiv_eq_alt `{! a b : A, ProofIrrel (a = b)} x1 x2 :
x1 x2
Heq : projT1 x1 = projT1 x2, rew Heq in projT2 x1 projT2 x2.
Proof.
setoid_rewrite equiv_dist; setoid_rewrite sigT_dist_eq; split => Heq.
- move: (Heq 0) => [H0eq1 _].
exists H0eq1 => n. move: (Heq n) => [] Hneq1.
by rewrite (proof_irrel H0eq1 Hneq1).
- move: Heq => [Heq1 Heqn2] n. by exists Heq1.
Qed.
(** [projT1] is non-expansive and proper. *)
Global Instance projT1_ne : NonExpansive (projT1 : sigTO leibnizO A).
Proof. solve_proper. Qed.
Global Instance projT1_proper : Proper (() ==> ()) (projT1 : sigTO leibnizO A).
Proof. apply ne_proper, projT1_ne. Qed.
(** [projT2] is "non-expansive"; the properness lemma [projT2_ne] requires UIP. *)
Lemma projT2_ne n (x1 x2 : sigTO) (Heq : x1 {n} x2) :
rew (sigT_dist_proj1 n Heq) in projT2 x1 {n} projT2 x2.
Proof. by destruct Heq. Qed.
Lemma projT2_proper `{! a b : A, ProofIrrel (a = b)} (x1 x2 : sigTO) (Heqs : x1 x2):
rew (sigT_equiv_proj1 Heqs) in projT2 x1 projT2 x2.
Proof.
move: x1 x2 Heqs => [a1 x1] [a2 x2] Heqs.
case: (proj1 (sigT_equiv_eq_alt _ _) Heqs) => /=. intros ->.
rewrite (proof_irrel (sigT_equiv_proj1 Heqs) eq_refl) /=. done.
Qed.
(** [existT] is "non-expansive" — general, dependently-typed statement. *)
Lemma existT_ne n {i1 i2} {v1 : P i1} {v2 : P i2} :
(eq : i1 = i2), (rew f_equal P eq in v1 {n} v2)
(Heq : i1 = i2), (rew f_equal P Heq in v1 {n} v2)
existT i1 v1 {n} existT i2 v2.
Proof. intros ->; simpl. exists eq_refl => /=. done. Qed.
Lemma existT_proper {i1 i2} {v1 : P i1} {v2 : P i2} :
(eq : i1 = i2), (rew f_equal P eq in v1 v2)
(Heq : i1 = i2), (rew f_equal P Heq in v1 v2)
existT i1 v1 existT i2 v2.
Proof. intros eq Heq n. apply (existT_ne n eq), equiv_dist, Heq. Qed.
Proof. intros Heq Heqv n. apply (existT_ne n Heq), equiv_dist, Heqv. Qed.
(** [existT] is "non-expansive" — non-dependently-typed version. *)
Global Instance existT_ne_2 a : NonExpansive (@existT A P a).
......@@ -1374,17 +1405,6 @@ Section sigT.
Lemma sigT_chain_const_proj1 c n : projT1 (c n) = projT1 (c 0).
Proof. refine (sigT_dist_proj1 _ (chain_cauchy c 0 n _)). lia. Qed.
Lemma sigT_equiv_eq_alt `{! a b : A, ProofIrrel (a = b)} x1 x2 :
x1 x2
eq : projT1 x1 = projT1 x2, rew eq in projT2 x1 projT2 x2.
Proof.
setoid_rewrite equiv_dist; setoid_rewrite sigT_dist_eq; split => Heq.
- move: (Heq 0) => [H0eq1 _].
exists H0eq1 => n. move: (Heq n) => [] Hneq1.
by rewrite (proof_irrel H0eq1 Hneq1).
- move: Heq => [Heq1 Heqn2] n. by exists Heq1.
Qed.
(* For this COFE construction we need UIP (Uniqueness of Identity Proofs)
on [A] (i.e. [∀ x y : A, ProofIrrel (x = y)]. UIP is most commonly obtained
from decidable equality (by Hedberg’s theorem, see
......
......@@ -74,7 +74,7 @@ Section ufrac_auth.
Proof.
rewrite auth_both_validN=> -[Hincl Hvalid].
move: Hincl=> /Some_includedN=> -[[_ ? //]|[[[p' ?] ?] [/=]]].
move=> /discrete_iff /leibniz_equiv_iff; rewrite ufrac_op'=> [/Qp_eq/=].
rewrite -discrete_iff leibniz_equiv_iff. rewrite ufrac_op'=> [/Qp_eq/=].
rewrite -{1}(Qcplus_0_r p)=> /(inj (Qcplus p))=> ?; by subst.
Qed.
Lemma ufrac_auth_agree p a b : (U{p} a U{p} b) a b.
......
......@@ -47,6 +47,11 @@ Qed.
Lemma cmra_updateP_weaken (P Q : A Prop) x :
x ~~>: P ( y, P y Q y) x ~~>: Q.
Proof. eauto using cmra_updateP_compose, cmra_updateP_id. Qed.
Lemma cmra_update_exclusive `{!Exclusive x} y:
y x ~~> y.
Proof. move=>??[z|]=>[/exclusiveN_l[]|_]. by apply cmra_valid_validN. Qed.
(** Updates form a preorder. *)
Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
Proof.
split.
......@@ -54,9 +59,6 @@ Proof.
- intros x y z. rewrite !cmra_update_updateP.
eauto using cmra_updateP_compose with subst.
Qed.
Lemma cmra_update_exclusive `{!Exclusive x} y:
y x ~~> y.
Proof. move=>??[z|]=>[/exclusiveN_l[]|_]. by apply cmra_valid_validN. Qed.
Lemma cmra_updateP_op (P1 P2 Q : A Prop) x1 x2 :
x1 ~~>: P1 x2 ~~>: P2 ( y1 y2, P1 y1 P2 y2 Q (y1 y2))
......
......@@ -335,6 +335,16 @@ Section sep_list2.
[by rewrite left_id|by rewrite left_id|apply False_elim|].
by rewrite IH -assoc.
Qed.
Lemma big_sepL2_app_inv Φ l1 l2 l1' l2' :
length l1 = length l1'
([ list] ky1;y2 l1 ++ l2; l1' ++ l2', Φ k y1 y2) -
([ list] ky1;y2 l1; l1', Φ k y1 y2)
([ list] ky1;y2 l2; l2', Φ (length l1 + k)%nat y1 y2).
Proof.
revert Φ l1'. induction l1 as [|x1 l1 IH]=> Φ -[|x1' l1'] //= ?; simplify_eq.
- by rewrite left_id.
- by rewrite -assoc IH.
Qed.
Lemma big_sepL2_mono Φ Ψ l1 l2 :
( k y1 y2, l1 !! k = Some y1 l2 !! k = Some y2 Φ k y1 y2 Ψ k y1 y2)
......@@ -400,6 +410,17 @@ Section sep_list2.
by f_equiv; f_equiv=> k [??].
Qed.
Lemma big_sepL2_reverse_2 (Φ : A B PROP) l1 l2 :
([ list] y1;y2 l1;l2, Φ y1 y2) ([ list] y1;y2 reverse l1;reverse l2, Φ y1 y2).
Proof.
revert l2. induction l1 as [|x1 l1 IH]; intros [|x2 l2]; simpl; auto using False_elim.
rewrite !reverse_cons (comm bi_sep) IH.
by rewrite (big_sepL2_app _ _ [x1] _ [x2]) big_sepL2_singleton wand_elim_l.
Qed.
Lemma big_sepL2_reverse (Φ : A B PROP) l1 l2 :
([ list] y1;y2 reverse l1;reverse l2, Φ y1 y2) ([ list] y1;y2 l1;l2, Φ y1 y2).
Proof. apply (anti_symm _); by rewrite big_sepL2_reverse_2 ?reverse_involutive. Qed.
Lemma big_sepL2_sep Φ Ψ l1 l2 :
([ list] ky1;y2 l1;l2, Φ k y1 y2 Ψ k y1 y2)
([ list] ky1;y2 l1;l2, Φ k y1 y2) ([ list] ky1;y2 l1;l2, Ψ k y1 y2).
......
......@@ -61,7 +61,7 @@ Open Scope Z_scope.
Definition proph_id := positive.
Inductive base_lit : Set :=
| LitInt (n : Z) | LitBool (b : bool) | LitUnit
| LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitErased
| LitLoc (l : loc) | LitProphecy (p: proph_id).
Inductive un_op : Set :=
| NegOp | MinusUnOp.
......@@ -151,38 +151,33 @@ Ignoring (as usual) the fact that we have to fit the infinite Z/loc into 61
bits, this means every value is machine-word-sized and can hence be atomically
read and written. Also notice that the sets of boxed and unboxed values are
disjoint. *)
Definition lit_is_unboxed (l: base_lit) : Prop :=
match l with
(** Disallow comparing (erased) prophecies with (erased) prophecies, by
considering them boxed. *)
| LitProphecy _ | LitErased => False
| _ => True
end.
Definition val_is_unboxed (v : val) : Prop :=
match v with
| LitV _ => True
| InjLV (LitV _) => True
| InjRV (LitV _) => True
| LitV l => lit_is_unboxed l
| InjLV (LitV l) => lit_is_unboxed l
| InjRV (LitV l) => lit_is_unboxed l
| _ => False
end.
(** CmpXchg just compares the word-sized representation of two values, it cannot
look into boxed data. This works out fine if at least one of the to-be-compared
Instance lit_is_unboxed_dec l : Decision (lit_is_unboxed l).
Proof. destruct l; simpl; exact (decide _). Defined.
Instance val_is_unboxed_dec v : Decision (val_is_unboxed v).
Proof. destruct v as [ | | | [] | [] ]; simpl; exact (decide _). Defined.
(** We just compare the word-sized representation of two values, without looking
into boxed data. This works out fine if at least one of the to-be-compared
values is unboxed (exploiting the fact that an unboxed and a boxed value can
never be equal because these are disjoint sets). *)
Definition vals_cmpxchg_compare_safe (vl v1 : val) : Prop :=
Definition vals_compare_safe (vl v1 : val) : Prop :=
val_is_unboxed vl val_is_unboxed v1.
Arguments vals_cmpxchg_compare_safe !_ !_ /.
(** We don't compare the logical program values, but we first normalize them
to make sure that prophecies are treated like unit.
Also all functions become the same, but still distinct from anything else. *)
Definition lit_for_compare (l : base_lit) : base_lit :=
match l with
| LitProphecy p => LitUnit
| l => l
end.
Fixpoint val_for_compare (v : val) : val :=
match v with
| LitV l => LitV (lit_for_compare l)
| PairV v1 v2 => PairV (val_for_compare v1) (val_for_compare v2)
| InjLV v => InjLV (val_for_compare v)
| InjRV v => InjRV (val_for_compare v)
| RecV f x e => RecV BAnon BAnon (Val $ LitV $ LitUnit)
end.
Arguments vals_compare_safe !_ !_ /.
(** The state: heaps of vals. *)
Record state : Type := {
......@@ -263,12 +258,18 @@ Proof. solve_decision. Defined.
Instance base_lit_countable : Countable base_lit.
Proof.
refine (inj_countable' (λ l, match l with
| LitInt n => (inl (inl n), None) | LitBool b => (inl (inr b), None)
| LitUnit => (inr (inl ()), None) | LitLoc l => (inr (inr l), None)
| LitProphecy p => (inr (inl ()), Some p)
| LitInt n => (inl (inl n), None)
| LitBool b => (inl (inr b), None)
| LitUnit => (inr (inl false), None)
| LitErased => (inr (inl true), None)
| LitLoc l => (inr (inr l), None)
| LitProphecy p => (inr (inl false), Some p)
end) (λ l, match l with
| (inl (inl n), None) => LitInt n | (inl (inr b), None) => LitBool b
| (inr (inl ()), None) => LitUnit | (inr (inr l), None) => LitLoc l
| (inl (inl n), None) => LitInt n
| (inl (inr b), None) => LitBool b
| (inr (inl false), None) => LitUnit
| (inr (inl true), None) => LitErased
| (inr (inr l), None) => LitLoc l
| (_, Some p) => LitProphecy p
end) _); by intros [].
Qed.
......@@ -519,7 +520,10 @@ Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit :=
Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
if decide (op = EqOp) then
(* Crucially, this compares the same way as [CmpXchg]! *)
Some $ LitV $ LitBool $ bool_decide (val_for_compare v1 = val_for_compare v2)
if decide (vals_compare_safe v1 v2) then
Some $ LitV $ LitBool $ bool_decide (v1 = v2)
else
None
else
match v1, v2 with
| LitV (LitInt n1), LitV (LitInt n2) => LitV <$> bin_op_eval_int op n1 n2
......@@ -635,10 +639,10 @@ Inductive head_step : expr → state → list observation → expr → state →
(Val $ LitV LitUnit) (state_upd_heap <[l:=v]> σ)
[]
| CmpXchgS l v1 v2 vl σ b :
vals_cmpxchg_compare_safe vl v1
σ.(heap) !! l = Some vl
(* Crucially, this compares the same way as [EqOp]! *)
b = bool_decide (val_for_compare vl = val_for_compare v1)
vals_compare_safe vl v1
b = bool_decide (vl = v1)
head_step (CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ
[]
(Val $ PairV vl (LitV $ LitBool b)) (if b then state_upd_heap <[l:=v2]> σ else σ)
......@@ -681,7 +685,7 @@ Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
Proof. revert Ki1. induction Ki2, Ki1; naive_solver eauto with f_equal. Qed.
Lemma alloc_fresh v n σ :
let l := fresh_locs (dom (gset loc) σ.(heap)) n in
let l := fresh_locs (dom (gset loc) σ.(heap)) in
0 < n
head_step (AllocN ((Val $ LitV $ LitInt $ n)) (Val v)) σ []
(Val $ LitV $ LitLoc l) (state_init_heap l n v σ) [].
......
......@@ -37,8 +37,8 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
cmpxchg_spec (l : loc) (w1 w2 : val) :
val_is_unboxed w1
<<< v, mapsto l 1 v >>> cmpxchg #l w1 w2 @
<<< if decide (val_for_compare v = val_for_compare w1) then mapsto l 1 w2 else mapsto l 1 v,
RET (v, #if decide (val_for_compare v = val_for_compare w1) then true else false) >>>;
<<< if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v,
RET (v, #if decide (v = w1) then true else false) >>>;
}.
Arguments atomic_heap _ {_}.
......@@ -68,8 +68,8 @@ Section derived.
Lemma cas_spec (l : loc) (w1 w2 : val) :
val_is_unboxed w1
<<< v, mapsto l 1 v >>> CAS #l w1 w2 @
<<< if decide (val_for_compare v = val_for_compare w1) then mapsto l 1 w2 else mapsto l 1 v,
RET #if decide (val_for_compare v = val_for_compare w1) then true else false >>>.
<<< if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v,
RET #if decide (v = w1) then true else false >>>.
Proof.
iIntros (? Φ) "AU". awp_apply cmpxchg_spec; first done.
iApply (aacc_aupd_commit with "AU"); first done.
......@@ -119,12 +119,12 @@ Section proof.
val_is_unboxed w1
<<< (v : val), l v >>>
primitive_cmpxchg #l w1 w2 @
<<< if decide (val_for_compare v = val_for_compare w1) then l w2 else l v,
RET (v, #if decide (val_for_compare v = val_for_compare w1) then true else false) >>>.
<<< if decide (v = w1) then l w2 else l v,
RET (v, #if decide (v = w1) then true else false) >>>.
Proof.
iIntros (? Φ) "AU". wp_lam. wp_pures.
iMod "AU" as (v) "[H↦ [_ Hclose]]".
destruct (decide (val_for_compare v = val_for_compare w1)) as [Heq|Hne];
destruct (decide (v = w1)) as [Heq|Hne];
[wp_cmpxchg_suc|wp_cmpxchg_fail];
iMod ("Hclose" with "H↦") as "HΦ"; done.
Qed.
......
......@@ -161,8 +161,19 @@ Instance pure_unop op v v' :
Proof. solve_pure_exec. Qed.
Instance pure_binop op v1 v2 v' :
PureExec (bin_op_eval op v1 v2 = Some v') 1 (BinOp op (Val v1) (Val v2)) (Val v').
PureExec (bin_op_eval op v1 v2 = Some v') 1 (BinOp op (Val v1) (Val v2)) (Val v') | 10.
Proof. solve_pure_exec. Qed.
(* Higher-priority instance for EqOp. *)
Instance pure_eqop v1 v2 :
PureExec (vals_compare_safe v1 v2) 1
(BinOp EqOp (Val v1) (Val v2))
(Val $ LitV $ LitBool $ bool_decide (v1 = v2)) | 1.
Proof.
intros Hcompare.
cut (bin_op_eval EqOp v1 v2 = Some $ LitV $ LitBool $ bool_decide (v1 = v2)).
{ intros. revert Hcompare. solve_pure_exec. }
rewrite /bin_op_eval /= decide_True //.
Qed.
Instance pure_if_true e1 e2 : PureExec True 1 (If (Val $ LitV $ LitBool true) e1 e2) e1.
Proof. solve_pure_exec. Qed.
......@@ -375,7 +386,7 @@ Proof.
Qed.
Lemma wp_cmpxchg_fail s E l q v' v1 v2 :
val_for_compare v' val_for_compare v1 vals_cmpxchg_compare_safe v' v1
v' v1 vals_compare_safe v' v1
{{{ l {q} v' }}} CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
{{{ RET PairV v' (LitV $ LitBool false); l {q} v' }}}.
Proof.
......@@ -386,7 +397,7 @@ Proof.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
Lemma twp_cmpxchg_fail s E l q v' v1 v2 :
val_for_compare v' val_for_compare v1 vals_cmpxchg_compare_safe v' v1
v' v1 vals_compare_safe v' v1
[[{ l {q} v' }]] CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
[[{ RET PairV v' (LitV $ LitBool false); l {q} v' }]].
Proof.
......@@ -398,7 +409,7 @@ Proof.
Qed.
Lemma wp_cmpxchg_suc s E l v1 v2 v' :
val_for_compare v' = val_for_compare v1 vals_cmpxchg_compare_safe v' v1
v' = v1 vals_compare_safe v' v1
{{{ l v' }}} CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
{{{ RET PairV v' (LitV $ LitBool true); l v2 }}}.
Proof.
......@@ -410,7 +421,7 @@ Proof.
iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
Qed.
Lemma twp_cmpxchg_suc s E l v1 v2 v' :
val_for_compare v' = val_for_compare v1 vals_cmpxchg_compare_safe v' v1
v' = v1 vals_compare_safe v' v1
[[{ l v' }]] CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
[[{ RET PairV v' (LitV $ LitBool true); l v2 }]].
Proof.
......@@ -534,7 +545,7 @@ Proof.
Qed.
Lemma wp_resolve_cmpxchg_suc s E l (p : proph_id) (pvs : list (val * val)) v1 v2 v :
vals_cmpxchg_compare_safe v1 v1
vals_compare_safe v1 v1
{{{ proph p pvs l v1 }}}
Resolve (CmpXchg #l v1 v2) #p v @ s; E
{{{ RET (v1, #true) ; pvs', pvs = ((v1, #true)%V, v)::pvs' proph p pvs' l v2 }}}.
......@@ -547,7 +558,7 @@ Proof.
Qed.
Lemma wp_resolve_cmpxchg_fail s E l (p : proph_id) (pvs : list (val * val)) q v' v1 v2 v :
val_for_compare v' val_for_compare v1 vals_cmpxchg_compare_safe v' v1
v' v1 vals_compare_safe v' v1
{{{ proph p pvs l {q} v' }}}
Resolve (CmpXchg #l v1 v2) #p v @ s; E
{{{ RET (v', #false) ; pvs', pvs = ((v', #false)%V, v)::pvs' proph p pvs' l {q} v' }}}.
......@@ -582,7 +593,7 @@ Proof.
Qed.
Lemma wp_load_offset_vec s E l sz (off : fin sz) (vs : vec val sz) :
{{{ l ↦∗ vs }}} ! #(l + off) @ s; E {{{ RET (vs !!! off); l ↦∗ vs }}}.
{{{ l ↦∗ vs }}} ! #(l + off) @ s; E {{{ RET vs !!! off; l ↦∗ vs }}}.
Proof. apply wp_load_offset. by apply vlookup_lookup. Qed.
Lemma wp_store_offset s E l off vs v :
......@@ -604,8 +615,8 @@ Qed.
Lemma wp_cmpxchg_suc_offset s E l off vs v' v1 v2 :
vs !! off = Some v'
val_for_compare v' = val_for_compare v1
vals_cmpxchg_compare_safe v' v1
v' = v1
vals_compare_safe v' v1
{{{ l ↦∗ vs }}}
CmpXchg #(l + off) v1 v2 @ s; E
{{{ RET (v', #true); l ↦∗ <[off:=v2]> vs }}}.
......@@ -617,8 +628,8 @@ Proof.
Qed.
Lemma wp_cmpxchg_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
val_for_compare (vs !!! off) = val_for_compare v1
vals_cmpxchg_compare_safe (vs !!! off) v1
vs !!! off = v1
vals_compare_safe (vs !!! off) v1
{{{ l ↦∗ vs }}}
CmpXchg #(l + off) v1 v2 @ s; E
{{{ RET (vs !!! off, #true); l ↦∗ vinsert off v2 vs }}}.
......@@ -629,8 +640,8 @@ Qed.
Lemma wp_cmpxchg_fail_offset s E l off vs v0 v1 v2 :
vs !! off = Some v0
val_for_compare v0 val_for_compare v1
vals_cmpxchg_compare_safe v0 v1
v0 v1
vals_compare_safe v0 v1
{{{ l ↦∗ vs }}}
CmpXchg #(l + off) v1 v2 @ s; E
{{{ RET (v0, #false); l ↦∗ vs }}}.
......@@ -644,8 +655,8 @@ Proof.
Qed.
Lemma wp_cmpxchg_fail_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
val_for_compare (vs !!! off) val_for_compare v1
vals_cmpxchg_compare_safe (vs !!! off) v1
vs !!! off v1
vals_compare_safe (vs !!! off) v1
{{{ l ↦∗ vs }}}
CmpXchg #(l + off) v1 v2 @ s; E
{{{ RET (vs !!! off, #false); l ↦∗ vs }}}.
......
......@@ -30,13 +30,13 @@ Proof. destruct l; rewrite /loc_add /=; f_equal; lia. Qed.
Instance loc_add_inj l : Inj eq eq (loc_add l).
Proof. destruct l; rewrite /Inj /loc_add /=; intros; simplify_eq; lia. Qed.
Definition fresh_locs (ls : gset loc) (n : Z) : loc :=
Definition fresh_locs (ls : gset loc) : loc :=
{| loc_car := set_fold (λ k r, (1 + loc_car k) `max` r)%Z 1%Z ls |}.
Lemma fresh_locs_fresh ls n i :
(0 i)%Z (i < n)%Z fresh_locs ls n + i ls.
Lemma fresh_locs_fresh ls i :
(0 i)%Z fresh_locs ls + i ls.
Proof.
intros Hi _. cut ( l, l ls loc_car l < loc_car (fresh_locs ls n) + i)%Z.
intros Hi. cut ( l, l ls loc_car l < loc_car (fresh_locs ls) + i)%Z.
{ intros help Hf%help. simpl in *. lia. }
apply (set_fold_ind_L (λ r ls, l, l ls (loc_car l < r + i)%Z));
set_solver by eauto with lia.
......
......@@ -65,6 +65,12 @@ Ltac wp_finish :=
pm_prettify. (* prettify ▷s caused by [MaybeIntoLaterNEnvs] and
λs caused by wp_value *)
Ltac solve_vals_compare_safe :=
(* The first branch is for when we have [vals_compare_safe] in the context.
The other two branches are for when either one of the branches reduces to
[True] or we have it in the context. *)
fast_done || (left; fast_done) || (right; fast_done).
(** The argument [efoc] can be used to specify the construct that should be
reduced. For example, you can write [wp_pure (EIf _ _ _)], which will search
for an [EIf _ _ _] in the expression, and reduce it.
......@@ -81,7 +87,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
unify e' efoc;
eapply (tac_wp_pure _ _ _ _ (fill K e'));
[iSolveTC (* PureExec *)
|try fast_done (* The pure condition for PureExec *)
|try solve_vals_compare_safe (* The pure condition for PureExec -- handles trivial goals, including [vals_compare_safe] *)
|iSolveTC (* IntoLaters *)
|wp_finish (* new goal *)
])
......@@ -282,15 +288,15 @@ Lemma tac_wp_cmpxchg Δ Δ' Δ'' s E i K l v v1 v2 Φ :
MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ' = Some Δ''
vals_cmpxchg_compare_safe v v1
(val_for_compare v = val_for_compare v1
vals_compare_safe v v1
(v = v1
envs_entails Δ'' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E {{ Φ }}))
(val_for_compare v val_for_compare v1
(v v1
envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E {{ Φ }}))
envs_entails Δ (WP fill K (CmpXchg (LitV l) (Val v1) (Val v2)) @ s; E {{ Φ }}).
Proof.
rewrite envs_entails_eq=> ???? Hsuc Hfail.
destruct (decide (val_for_compare v = val_for_compare v1)) as [Heq|Hne].
destruct (decide (v = v1)) as [Heq|Hne].
- rewrite -wp_bind. eapply wand_apply.
{ eapply wp_cmpxchg_suc; eauto. }
rewrite into_laterN_env_sound -later_sep /= {1}envs_simple_replace_sound //; simpl.
......@@ -303,15 +309,15 @@ Qed.
Lemma tac_twp_cmpxchg Δ Δ' s E i K l v v1 v2 Φ :
envs_lookup i Δ = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ = Some Δ'
vals_cmpxchg_compare_safe v v1
(val_for_compare v = val_for_compare v1
vals_compare_safe v v1
(v = v1
envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E [{ Φ }]))
(val_for_compare v val_for_compare v1
(v v1
envs_entails Δ (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E [{ Φ }]))
envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]).
Proof.
rewrite envs_entails_eq=> ??? Hsuc Hfail.
destruct (decide (val_for_compare v = val_for_compare v1)) as [Heq|Hne].
destruct (decide (v = v1)) as [Heq|Hne].
- rewrite -twp_bind. eapply wand_apply.
{ eapply twp_cmpxchg_suc; eauto. }
rewrite /= {1}envs_simple_replace_sound //; simpl.
......@@ -325,7 +331,7 @@ Qed.
Lemma tac_wp_cmpxchg_fail Δ Δ' s E i K l q v v1 v2 Φ :
MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l {q} v)%I
val_for_compare v val_for_compare v1 vals_cmpxchg_compare_safe v v1
v v1 vals_compare_safe v v1
envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E {{ Φ }})
envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E {{ Φ }}).
Proof.
......@@ -336,7 +342,7 @@ Proof.
Qed.
Lemma tac_twp_cmpxchg_fail Δ s E i K l q v v1 v2 Φ :
envs_lookup i Δ = Some (false, l {q} v)%I
val_for_compare v val_for_compare v1 vals_cmpxchg_compare_safe v v1
v v1 vals_compare_safe v v1
envs_entails Δ (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E [{ Φ }])
envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]).
Proof.
......@@ -349,7 +355,7 @@ Lemma tac_wp_cmpxchg_suc Δ Δ' Δ'' s E i K l v v1 v2 Φ :
MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ' = Some Δ''
val_for_compare v = val_for_compare v1 vals_cmpxchg_compare_safe v v1
v = v1 vals_compare_safe v v1
envs_entails Δ'' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E {{ Φ }})
envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E {{ Φ }}).
Proof.
......@@ -362,7 +368,7 @@ Qed.
Lemma tac_twp_cmpxchg_suc Δ Δ' s E i K l v v1 v2 Φ :
envs_lookup i Δ = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ = Some Δ'
val_for_compare v = val_for_compare v1 vals_cmpxchg_compare_safe v v1
v = v1 vals_compare_safe v v1
envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E [{ Φ }])
envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]).
Proof.
......@@ -530,12 +536,6 @@ Tactic Notation "wp_store" :=
| _ => fail "wp_store: not a 'wp'"
end.
Ltac solve_vals_cmpxchg_compare_safe :=
(* The first branch is for when we have [vals_cmpxchg_compare_safe] in the context.
The other two branches are for when either one of the branches reduces to
[True] or we have it in the context. *)
fast_done || (left; fast_done) || (right; fast_done).
Tactic Notation "wp_cmpxchg" "as" simple_intropattern(H1) "|" simple_intropattern(H2) :=
let solve_mapsto _ :=
let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
......@@ -549,7 +549,7 @@ Tactic Notation "wp_cmpxchg" "as" simple_intropattern(H1) "|" simple_intropatter
[iSolveTC
|solve_mapsto ()
|pm_reflexivity
|try solve_vals_cmpxchg_compare_safe
|try solve_vals_compare_safe
|intros H1; wp_finish
|intros H2; wp_finish]
| |- envs_entails _ (twp ?E ?e ?Q) =>
......@@ -558,7 +558,7 @@ Tactic Notation "wp_cmpxchg" "as" simple_intropattern(H1) "|" simple_intropatter
|fail 1 "wp_cmpxchg: cannot find 'CmpXchg' in" e];
[solve_mapsto ()
|pm_reflexivity
|try solve_vals_cmpxchg_compare_safe
|try solve_vals_compare_safe
|intros H1; wp_finish
|intros H2; wp_finish]
| _ => fail "wp_cmpxchg: not a 'wp'"
......@@ -577,7 +577,7 @@ Tactic Notation "wp_cmpxchg_fail" :=
[iSolveTC
|solve_mapsto ()
|try (simpl; congruence) (* value inequality *)
|try solve_vals_cmpxchg_compare_safe
|try solve_vals_compare_safe
|wp_finish]
| |- envs_entails _ (twp ?s ?E ?e ?Q) =>
first
......@@ -585,7 +585,7 @@ Tactic Notation "wp_cmpxchg_fail" :=
|fail 1 "wp_cmpxchg_fail: cannot find 'CmpXchg' in" e];
[solve_mapsto ()
|try (simpl; congruence) (* value inequality *)
|try solve_vals_cmpxchg_compare_safe
|try solve_vals_compare_safe
|wp_finish]
| _ => fail "wp_cmpxchg_fail: not a 'wp'"
end.
......@@ -604,7 +604,7 @@ Tactic Notation "wp_cmpxchg_suc" :=
|solve_mapsto ()
|pm_reflexivity
|try (simpl; congruence) (* value equality *)
|try solve_vals_cmpxchg_compare_safe
|try solve_vals_compare_safe
|wp_finish]
| |- envs_entails _ (twp ?s ?E ?e ?Q) =>
first
......@@ -613,7 +613,7 @@ Tactic Notation "wp_cmpxchg_suc" :=
[solve_mapsto ()
|pm_reflexivity
|try (simpl; congruence) (* value equality *)
|try solve_vals_cmpxchg_compare_safe
|try solve_vals_compare_safe
|wp_finish]
| _ => fail "wp_cmpxchg_suc: not a 'wp'"
end.
......
......@@ -112,8 +112,8 @@ Section lemmas.
(* Sequential triples with a persistent precondition and no initial quantifier
are atomic. *)
Lemma seq_wp_atomic e Eo (α : [tele] iProp) (β : [tele] TB iProp)
(f : [tele] TB val Λ) {HP : .. x, Persistent (α x)} :
( Φ, .. x, α x - (.. y, β x y - Φ (f x y)) - WP e {{ Φ }}) -
(f : [tele] TB val Λ) {HP : Persistent (α [tele_arg])} :
( Φ, α [tele_arg] - (.. y, β [tele_arg] y - Φ (f [tele_arg] y)) - WP e {{ Φ }}) -
atomic_wp e Eo α β f.
Proof.
simpl in HP. iIntros "Hwp" (Φ) "HΦ". iApply fupd_wp.
......
......@@ -151,8 +151,23 @@ Section ectx_language.
Lemma not_head_reducible e σ : ¬head_reducible e σ head_irreducible e σ.
Proof. unfold head_reducible, head_irreducible. naive_solver. Qed.
Lemma fill_prim_step K e1 σ1 κ e2 σ2 efs :
prim_step e1 σ1 κ e2 σ2 efs prim_step (fill K e1) σ1 κ (fill K e2) σ2 efs.
Proof.
destruct 1 as [K' e1' e2' -> ->].
rewrite !fill_comp. by econstructor.
Qed.
Lemma fill_reducible K e σ : reducible e σ reducible (fill K e) σ.
Proof.
intros (κ&e'&σ'&efs&?). exists κ, (fill K e'), σ', efs.
by apply fill_prim_step.
Qed.
Lemma head_prim_reducible e σ : head_reducible e σ reducible e σ.
Proof. intros (κ&e'&σ'&efs&?). eexists κ, e', σ', efs. by apply head_prim_step. Qed.
Lemma head_prim_fill_reducible e K σ :
head_reducible e σ reducible (fill K e) σ.
Proof. intro. by apply fill_reducible, head_prim_reducible. Qed.
Lemma head_prim_reducible_no_obs e σ : head_reducible_no_obs e σ reducible_no_obs e σ.
Proof. intros (e'&σ'&efs&?). eexists e', σ', efs. by apply head_prim_step. Qed.
Lemma head_prim_irreducible e σ : irreducible e σ head_irreducible e σ.
......
This diff is collapsed.