Module assertions

Judgments in a Hoare logic are triples {{P}} s {{Q}}, where s is a statement, and P and Q are assertions called the pre and postcondition of s, respectively. The intuitive reading of such a triple is: if P holds for the state before execution of s, and execution of s terminates, then Q will hold afterwards. Like (Appel/Blazy, 2007), we define assertions using a shallow embedding. That is, assertions are predicates over the contents of the stack and memory.
This file defines the data type of assertions, the usual connectives of Hoare logic (, , ¬, , and ), the connectives of separation logic (emp, , , -★), and other connectives that are more specific to our development. We overload the usual notations in assert_scope to obtain nicely looking assertions. Furthermore, we prove various properties to make reasoning about assertions easier.
Require Import SetoidList.
Require Export expressions.

Definition of assertions

We pack assertions into a record so we can register the projection assert_holds as Proper for the setoid rewriting mechanism.
Record assert := Assert {
  assert_holds :> stackmemProp
}.

Delimit Scope assert_scope with A.
Bind Scope assert_scope with assert.
Arguments assert_holds _%A _ _.
Definition assert_as_Prop (P : assert) : Prop := ∀ ρ m, P ρ m.
Coercion assert_as_Prop : assert >-> Sortclass.

By defining a pre-order on assertions we automatically obtain the desired equality from the generic setoid equality on pre-orders.
Instance assert_subseteq: SubsetEq assert := λ P Q, ∀ ρ m, P ρ mQ ρ m.
Instance: PreOrder assert_subseteq.
Proof. firstorder. Qed.
Instance: Proper ((⊆) ==> (=) ==> (=) ==> impl) assert_holds.
Proof. repeat intro; subst; firstorder. Qed.
Instance: Proper ((≡) ==> (=) ==> (=) ==> iff) assert_holds.
Proof. split; subst; firstorder. Qed.

Subclasses of assertions

The following type classes collect important subclasses of assertions. This file contains instances of these type classes for the various connectives. We use instance resolution to automatically compose these instances to prove the above properties for composite assertions.
Class StackIndep (P : assert) : Prop :=
  stack_indep: ∀ ρ1 ρ2 m, P ρ1 mP ρ2 m.
Class MemIndep (P : assert) : Prop :=
  mem_indep: ∀ ρ m1 m2, P ρ m1P ρ m2.
Class MemExt (P : assert) : Prop :=
  mem_ext: ∀ ρ m1 m2, P ρ m1m1m2P ρ m2.

Instance mem_indep_ext P : MemIndep PMemExt P.
Proof. firstorder. Qed.

Invoke type class resolution when auto or eauto has to solve these constraints.
Hint Extern 100 (StackIndep _) => apply _.
Hint Extern 100 (MemIndep _) => apply _.
Hint Extern 100 (MemExt _) => apply _.

Allow it to solve more complex assertions automatically.
Hint Extern 1000 (MemIndep (match ?x with _ => _ end)) =>
  destruct x : typeclass_instances.
Hint Extern 1000 (MemExt (match ?x with _ => _ end)) =>
  destruct x : typeclass_instances.
Hint Extern 1000 (StackIndep (match ?x with _ => _ end)) =>
  destruct x : typeclass_instances.

Tactics

The tactic solve_assert will be used to automatically prove simple properties about assertions. It unfolds assertions using the unfold hint database assert and uses the naive_solver tactic to finish the proof.
Hint Unfold
  assert_as_Prop
  StackIndep MemIndep MemExt
  equiv preorder_equiv subseteq subseteq assert_subseteq : assert.

In most situations we do not want simpl to unfold assertions and expose their internal definition. However, as the behavior of simpl cannot be changed locally using Ltac we block unfolding of assert_holds by simpl and define a custom tactic to perform this unfolding instead. Unfortunately, it does not work properly for occurrences of assert_hold under binders.
Arguments assert_holds _ _ _ : simpl never.

Tactic Notation "unfold_assert" "in" hyp(H) :=
  repeat (progress (unfold assert_holds in H; simpl in H));
  repeat match type of H with
  | context C [let (x) := ?Q in x] =>
    let X := context C [assert_holds Q] in change X in H
  end.
Tactic Notation "unfold_assert" :=
  repeat (progress (unfold assert_holds; simpl));
  repeat match goal with
  | |- context C [let (x) := ?Q in x] =>
    let X := context C [assert_holds Q] in change X
  end.
Tactic Notation "unfold_assert" "in" "*" :=
  unfold_assert;
  repeat match goal with H : _ |- _ => progress unfold_assert in H end.

Hint Extern 100 (__) => solve_mem_disjoint : assert.

Ltac solve_assert :=
  repeat intro;
  intuition;
  repeat autounfold with assert in *;
  unfold_assert in *;
  naive_solver (eauto with assert; congruence).

Hoare logic connectives

Definitions and notations of the usual connectives of Hoare logic.
Definition Prop_as_assert (P : Prop) : assert := Assert $ λ _ _, P.
Notation "⌜ P ⌝" := (Prop_as_assert P) (format "⌜ P ⌝") : assert_scope.
Notation "'True'" := (Prop_as_assert True) : assert_scope.
Notation "'False'" := (Prop_as_assert False) : assert_scope.
Definition assert_impl (P Q : assert) : assert := Assert $ λ ρ m, P ρ mQ ρ m.
Infix "→" := assert_impl : assert_scope.
Notation "(→)" := assert_impl (only parsing) : assert_scope.
Notation "( P →)" := (assert_impl P) (only parsing) : assert_scope.
Notation "(→ Q )" := (λ P, assert_impl P Q) (only parsing) : assert_scope.

Definition assert_and (P Q : assert) : assert := Assert $ λ ρ m, P ρ mQ ρ m.
Infix "∧" := assert_and : assert_scope.
Notation "(∧)" := assert_and (only parsing) : assert_scope.
Notation "( P ∧)" := (assert_and P) (only parsing) : assert_scope.
Notation "(∧ Q )" := (λ P, assert_and P Q) (only parsing) : assert_scope.

Definition assert_or (P Q : assert) : assert := Assert $ λ ρ m, P ρ mQ ρ m.
Infix "∨" := assert_or : assert_scope.
Notation "(∨)" := assert_or (only parsing) : assert_scope.
Notation "( P ∨)" := (assert_or P) (only parsing) : assert_scope.
Notation "(∨ Q )" := (λ P, assert_or P Q) (only parsing) : assert_scope.

Definition assert_iff (P Q : assert) : assert := ((PQ) ∧ (QP))%A.
Infix "↔" := assert_iff : assert_scope.
Notation "(↔)" := assert_iff (only parsing) : assert_scope.
Notation "( P ↔)" := (assert_iff P) (only parsing) : assert_scope.
Notation "(↔ Q )" := (λ P, assert_iff P Q) (only parsing) : assert_scope.

Definition assert_not (P : assert) : assert := Assert $ λ ρ m, ¬P ρ m.
NotationP" := (assert_not P) : assert_scope.

Definition assert_forall {A} (P : Aassert) : assert :=
  Assert $ λ ρ m, ∀ x, P x ρ m.
Notation "∀ x .. y , P" :=
  (assert_forallx, .. (assert_forally, P)) ..)) : assert_scope.
Definition assert_exist {A} (P : Aassert) : assert :=
  Assert $ λ ρ m, ∃ x, P x ρ m.
Notation "∃ x .. y , P" :=
  (assert_existx, .. (assert_existy, P)) ..)) : assert_scope.

Compatibility of the connectives with respect to order and setoid equality.
Instance: Proper ((⊆) ==> impl) assert_as_Prop.
Proof. solve_assert. Qed.
Instance: Proper ((≡) ==> iff) assert_as_Prop.
Proof. solve_assert. Qed.
Instance: Proper (impl ==> (⊆)) Prop_as_assert.
Proof. solve_assert. Qed.
Instance: Proper (iff ==> (≡)) Prop_as_assert.
Proof. solve_assert. Qed.

Instance: Proper (flip (⊆) ==> (⊆) ==> (⊆)) (→)%A.
Proof. solve_assert. Qed.
Instance: Proper ((≡) ==> (≡) ==> (≡)) (→)%A.
Proof. solve_assert. Qed.
Instance: Proper ((≡) ==> (≡) ==> (≡)) (↔)%A.
Proof. solve_assert. Qed.
Instance: Proper ((≡) ==> (≡) ==> (≡)) (∧)%A.
Proof. solve_assert. Qed.
Instance: Proper ((⊆) ==> (⊆) ==> (⊆)) (∧)%A.
Proof. solve_assert. Qed.
Instance: Proper ((≡) ==> (≡) ==> (≡)) (∨)%A.
Proof. solve_assert. Qed.
Instance: Proper ((⊆) ==> (⊆) ==> (⊆)) (∨)%A.
Proof. solve_assert. Qed.
Instance: Proper ((≡) ==> (≡)) assert_not.
Proof. solve_assert. Qed.
Instance: Proper (flip (⊆) ==> (⊆)) assert_not.
Proof. solve_assert. Qed.
Instance: Proper (pointwise_relation _ (≡) ==> (≡)) (@assert_forall A).
Proof. unfold pointwise_relation. solve_assert. Qed.
Instance: Proper (pointwise_relation _ (⊆) ==> (⊆)) (@assert_forall A).
Proof. unfold pointwise_relation. solve_assert. Qed.
Instance: Proper (pointwise_relation _ (≡) ==> (≡)) (@assert_exist A).
Proof. unfold pointwise_relation. solve_assert. Qed.
Instance: Proper (pointwise_relation _ (⊆) ==> (⊆)) (@assert_exist A).
Proof. unfold pointwise_relation. solve_assert. Qed.

Instances of the type classes for stack independence, memory independence, and memory extensibility.
Instance Prop_as_assert_stack_indep P : StackIndep (⌜ P ⌝).
Proof. solve_assert. Qed.
Instance assert_impl_stack_indep :
  StackIndep PStackIndep QStackIndep (PQ).
Proof. solve_assert. Qed.
Instance assert_and_stack_indep :
  StackIndep PStackIndep QStackIndep (PQ).
Proof. solve_assert. Qed.
Instance assert_or_stack_indep :
  StackIndep PStackIndep QStackIndep (PQ).
Proof. solve_assert. Qed.
Instance assert_not_stack_indep :
  StackIndep PStackIndepP).
Proof. solve_assert. Qed.
Instance assert_forall_stack_indep A :
  (∀ x : A, StackIndep (P x)) → StackIndep (assert_forall P).
Proof. solve_assert. Qed.
Instance assert_exist_stack_indep A :
  (∀ x : A, StackIndep (P x)) → StackIndep (assert_exist P).
Proof. solve_assert. Qed.
Instance assert_iff_stack_indep :
  StackIndep PStackIndep QStackIndep (PQ).
Proof. solve_assert. Qed.

Instance Prop_as_assert_mem_indep P : MemIndep (⌜ P ⌝).
Proof. solve_assert. Qed.
Instance assert_impl_mem_indep : MemIndep PMemIndep QMemIndep (PQ).
Proof. solve_assert. Qed.
Instance assert_and_mem_indep : MemIndep PMemIndep QMemIndep (PQ).
Proof. solve_assert. Qed.
Instance assert_or_mem_indep : MemIndep PMemIndep QMemIndep (PQ).
Proof. solve_assert. Qed.
Instance assert_not_mem_indep : MemIndep PMemIndepP).
Proof. solve_assert. Qed.
Instance assert_forall_mem_indep A :
  (∀ x : A, MemIndep (P x)) → MemIndep (assert_forall P).
Proof. solve_assert. Qed.
Instance assert_exist_mem_indep A :
  (∀ x : A, MemIndep (P x)) → MemIndep (assert_exist P).
Proof. solve_assert. Qed.
Instance assert_iff_mem_indep : MemIndep PMemIndep QMemIndep (PQ).
Proof. solve_assert. Qed.

Instance assert_impl_mem_ext : MemIndep PMemExt QMemExt (PQ).
Proof. solve_assert. Qed.
Instance assert_and_mem_ext : MemExt PMemExt QMemExt (PQ).
Proof. solve_assert. Qed.
Instance assert_or_mem_ext : MemExt PMemExt QMemExt (PQ).
Proof. solve_assert. Qed.
Instance assert_forall_mem_ext A :
  (∀ x : A, MemExt (P x)) → MemExt (assert_forall P).
Proof. solve_assert. Qed.
Instance assert_exist_mem_ext A :
  (∀ x : A, MemExt (P x)) → MemExt (assert_exist P).
Proof. solve_assert. Qed.

Proofs of other useful properties.
Instance: Commutative (≡) (↔)%A.
Proof. solve_assert. Qed.
Instance: Commutative (≡) (∧)%A.
Proof. solve_assert. Qed.
Instance: Associative (≡) (∧)%A.
Proof. solve_assert. Qed.
Instance: Idempotent (≡) (∧)%A.
Proof. solve_assert. Qed.
Instance: Commutative (≡) (∨)%A.
Proof. solve_assert. Qed.
Instance: Associative (≡) (∨)%A.
Proof. solve_assert. Qed.
Instance: Idempotent (≡) (∨)%A.
Proof. solve_assert. Qed.

Instance: LeftId (≡) True%A (∧)%A.
Proof. solve_assert. Qed.
Instance: RightId (≡) True%A (∧)%A.
Proof. solve_assert. Qed.
Instance: LeftAbsorb (≡) False%A (∧)%A.
Proof. solve_assert. Qed.
Instance: RightAbsorb (≡) False%A (∧)%A.
Proof. solve_assert. Qed.

Instance: LeftId (≡) False%A (∨)%A.
Proof. solve_assert. Qed.
Instance: RightId (≡) False%A (∨)%A.
Proof. solve_assert. Qed.
Instance: LeftAbsorb (≡) True%A (∨)%A.
Proof. solve_assert. Qed.
Instance: RightAbsorb (≡) True%A (∨)%A.
Proof. solve_assert. Qed.

Instance: LeftId (≡) True%A (→)%A.
Proof. solve_assert. Qed.
Instance: RightAbsorb (≡) True%A (→)%A.
Proof. intros ?. solve_assert. Qed.

Lemma Prop_as_assert_impl (P Q : Prop) : ⌜ PQ ⌝%A ≡ (⌜P⌝ → ⌜Q⌝)%A.
Proof. solve_assert. Qed.
Lemma Prop_as_assert_not (P : Prop) : ⌜ ¬P ⌝%A ≡ (¬⌜P⌝)%A.
Proof. solve_assert. Qed.
Lemma Prop_as_assert_and (P Q : Prop) : ⌜ PQ ⌝%A ≡ (⌜P⌝ ∧ ⌜Q⌝)%A.
Proof. solve_assert. Qed.
Lemma Prop_as_assert_or (P Q : Prop) : ⌜ PQ ⌝%A ≡ (⌜P⌝ ∨ ⌜Q⌝)%A.
Proof. solve_assert. Qed.

Lemma assert_true_intro (P : assert) : PTrue%A.
Proof. solve_assert. Qed.
Lemma assert_false_elim (P : assert) : False%AP.
Proof. solve_assert. Qed.

Lemma assert_and_l (P Q : assert) : (PQ)%AP.
Proof. solve_assert. Qed.
Lemma assert_and_r (P Q : assert) : (PQ)%AQ.
Proof. solve_assert. Qed.
Lemma assert_and_intro P Q1 Q2 : PQ1PQ2P ⊆ (Q1Q2)%A.
Proof. solve_assert. Qed.
Lemma assert_and_elim_l P1 P2 Q : P1Q → (P1P2)%AQ.
Proof. solve_assert. Qed.
Lemma assert_and_elim_r P1 P2 Q : P2Q → (P1P2)%AQ.
Proof. solve_assert. Qed.

Lemma assert_forall_intro {A} P (Q : Aassert) :
  (∀ x, PQ x) → P ⊆ (∀ x, Q x)%A.
Proof. solve_assert. Qed.
Lemma assert_forall_specialize {A} (P : Aassert) Q x :
  (P xQ) → (∀ x, P x)%AQ.
Proof. solve_assert. Qed.

Lemma assert_exists_intro {A} P (Q : Aassert) x :
  PQ xP ⊆ (∃ x, Q x)%A.
Proof. solve_assert. Qed.
Lemma assert_exists_elim {A} (P : Aassert) Q :
  (∀ x, P xQ) → (∃ x, P x)%AQ.
Proof. solve_assert. Qed.

Lemma assert_or_l (P Q : assert) : P ⊆ (PQ)%A.
Proof. solve_assert. Qed.
Lemma assert_or_r (P Q : assert) : P ⊆ (PQ)%A.
Proof. solve_assert. Qed.
Lemma assert_or_elim (P Q R : assert) :
  PRQR → (PQ)%AR.
Proof. solve_assert. Qed.

Lemma assert_and_exists {A} P (Q : Aassert) :
  (P ∧ ∃ x, Q x)%A ≡ (∃ x, PQ x)%A.
Proof. solve_assert. Qed.
Lemma assert_exists_and {A} (P : Aassert) Q :
  ((∃ x, P x) ∧ Q)%A ≡ (∃ x, P xQ)%A.
Proof. solve_assert. Qed.

The assertion ev asserts that the expression e evaluates to v and e ⇓ - asserts that the expression e evaluates to an arbitrary value (in other words, e does not impose undefined behavior).
Notation vassert := (valueassert).

Definition assert_expr (e : expr) : vassert := λ v,
  Assert $ λ ρ m, ⟦ e ⟧ ρ m = Some v.
Infix "⇓" := assert_expr (at level 60) : assert_scope.
Notation "(⇓)" := assert_expr (only parsing) : assert_scope.
Notation "( e ⇓)" := (assert_expr e) (only parsing) : assert_scope.
Notation "(⇓ v )" := (λ e, assert_expr e v) (only parsing) : assert_scope.

Notation "e ⇓ -" := (∃ v, ev)%A
  (at level 60, format "e '⇓' '-'") : assert_scope.
Notation "(⇓ - )" := assert_expr (only parsing) : assert_scope.

Instance assert_expr_mem_ext e v : MemExt (ev).
Proof. red. unfold_assert. eauto using expr_eval_weaken_mem. Qed.

Instance assert_expr_mem_indep e :
  expr_load_free e
  MemIndep (ev).
Proof.
  intros ?? ρ m1 m2. unfold_assert.
  by rewrite !(expr_load_free_mem_indep ρ m1 m2).
Qed.

Instance assert_expr_mem_indep_ e :
  expr_load_free e
  MemIndep (e ⇓ -).
Proof.
  intros ? ρ m1 m2 [v ?]. exists v. unfold_assert in *.
  by rewrite !(expr_load_free_mem_indep ρ m2 m1).
Qed.


Instance assert_expr_stack_indep e v :
  expr_vars e ≡ ∅ →
  StackIndep (ev).
Proof.
  intros ? ρ1 ρ2 m. unfold_assert.
  by rewrite !(expr_var_free_stack_indep ρ2 ρ1).
Qed.

Instance assert_expr_stack_indep_ e :
  expr_vars e ≡ ∅ →
  StackIndep (e ⇓ -).
Proof.
  intros ? ρ1 ρ2 m. unfold_assert.
  by rewrite !(expr_var_free_stack_indep ρ2 ρ1).
Qed.


Lemma assert_expr_load e p v :
  (load epload (val p) ⇓ v)%A ⊆ (load (load e) ⇓ v)%A.
Proof. intros ρ m [He ?]. unfold_assert in *. by rewrite He. Qed.
Lemma assert_expr_forget e v : (ev)%A ⊆ (e ⇓ -)%A.
Proof. solve_assert. Qed.

Notation "e ⇓ 'true'" := (∃ v, ev ∧ ⌜ value_true v ⌝)%A
  (at level 60, format "e '⇓' 'true'") : assert_scope.
Notation "e ⇓ 'false'" := (∃ v, ev ∧ ⌜ value_false v ⌝)%A
  (at level 60, format "e '⇓' 'false'") : assert_scope.

Definition assert_is_true (Pv : vassert) : assert :=
  (∃ v, Pv v ∧ ⌜ value_true v ⌝)%A.
Definition assert_is_false (Pv : vassert) : assert :=
  (∃ v, Pv v ∧ ⌜ value_false v ⌝)%A.

Definition assert_subst (a : index) (v : value) (P : assert) :=
  Assert $ λ ρ m, P ρ (<[a:=v]>m).
Notation "<[ a := v ]>" := (assert_subst a v) : assert_scope.

Instance: ∀ a v, Proper ((≡) ==> (≡)) (assert_subst a v).
Proof. solve_assert. Qed.

Lemma assert_subst_mem_indep P `{MemIndep P} a v:
  (<[a:=v]>P)%AP.
Proof. solve_assert. Qed.
Lemma assert_subst_impl P Q a v :
  (<[a:=v]>(PQ))%A ≡ (<[a:=v]>P → <[a:=v]>Q)%A.
Proof. solve_assert. Qed.
Lemma assert_subst_not P a v : (<[a:=v]>(¬P))%A ≡ (¬<[a:=v]>P)%A.
Proof. solve_assert. Qed.
Lemma assert_subst_and P Q a v :
  (<[a:=v]>(PQ))%A ≡ (<[a:=v]>P ∧ <[a:=v]>Q)%A.
Proof. solve_assert. Qed.
Lemma assert_subst_or P Q a v :
  (<[a:=v]>(PQ))%A ≡ (<[a:=v]>P ∨ <[a:=v]>Q)%A.
Proof. solve_assert. Qed.
Lemma assert_subst_forall `(P : Aassert) a v :
  (<[a:=v]>(∀ x, P x))%A ≡ (∀ x, <[a:=v]>(P x))%A.
Proof. solve_assert. Qed.
Lemma assert_subst_exists `(P : Aassert) a v :
  (<[a:=v]>(∃ x, P x))%A ≡ (∃ x, <[a:=v]>(P x))%A.
Proof. solve_assert. Qed.

Separation logic connectives

The assertion emp asserts that the memory is empty. The assertion PQ (called separating conjunction) asserts that the memory can be split into two disjoint parts such that P holds in the one part, and Q in the other. The assertion P -★ Q (called separating implication or magic wand) asserts that if an arbitrary memory is extended with a disjoint part in which P holds, then Q holds in the extended memory.
Definition assert_emp : assert := Assert $ λ ρ m, m = ∅.
Notation "'emp'" := assert_emp : assert_scope.

Definition assert_sep (P Q : assert) : assert := Assert $ λ ρ m, ∃ m1 m2,
  m1m2 = mm1m2P ρ m1Q ρ m2.
Infix "★" := assert_sep (at level 80, right associativity) : assert_scope.
Notation "(★)" := assert_sep (only parsing) : assert_scope.
Notation "( P ★)" := (assert_sep P) (only parsing) : assert_scope.
Notation "(★ Q )" := (λ P, assert_sep P Q) (only parsing) : assert_scope.

Definition assert_wand (P Q : assert) : assert := Assert $ λ ρ m1, ∀ m2,
  m1m2P ρ m2Q ρ (m1m2).
Infix "-★" := assert_wand (at level 90) : assert_scope.
Notation "(-★)" := assert_wand (only parsing) : assert_scope.
Notation "( P -★)" := (assert_wand P) (only parsing) : assert_scope.
Notation "(-★ Q )" := (λ P, assert_wand P Q) (only parsing) : assert_scope.

Compatibility of the separation logic connectives with respect to order and equality.
Instance: Proper ((⊆) ==> (⊆) ==> (⊆)) (★)%A.
Proof. solve_assert. Qed.
Instance: Proper ((≡) ==> (≡) ==> (≡)) (★)%A.
Proof. solve_assert. Qed.
Instance: Proper (flip (⊆) ==> (⊆) ==> (⊆)) (-★)%A.
Proof. solve_assert. Qed.
Instance: Proper ((≡) ==> (≡) ==> (≡)) (-★)%A.
Proof. solve_assert. Qed.

Basic properties.
Lemma assert_sep_comm_1 P Q : (PQ)%A ⊆ (QP)%A.
Proof.
  intros ? m (m1 & m2 & ? & ? & HP & HQ).
  exists m2 m1. by rewrite finmap_union_comm.
Qed.

Instance: Commutative (≡) (★)%A.
Proof. split; apply assert_sep_comm_1. Qed.

Lemma assert_sep_left_id_1 P : (empP)%AP.
Proof.
  intros ? m (m1 & m2 & H & Hm1 & Hm2 & Hm3).
  unfold_assert in *. subst.
  by rewrite (left_id ∅ (∪)).
Qed.

Lemma assert_sep_left_id_2 P : P ⊆ (empP)%A.
Proof.
  intros ? m ?. exists (∅ : mem) m. repeat split.
  * apply (left_id _ _).
  * solve_mem_disjoint.
  * done.
Qed.

Instance: LeftId (≡) emp%A (★)%A.
Proof. split. apply assert_sep_left_id_1. apply assert_sep_left_id_2. Qed.
Instance: RightId (≡) emp%A (★)%A.
Proof. intros ?. rewrite (commutative _). apply (left_id _ _). Qed.

Instance: LeftAbsorb (≡) False%A (★)%A.
Proof. solve_assert. Qed.
Instance: RightAbsorb (≡) False%A (★)%A.
Proof. solve_assert. Qed.

Lemma assert_sep_assoc_1 P Q R : ((PQ) ★ R)%A ⊆ (P ★ (QR))%A.
Proof.
  intros ?? (? & mR & ? & ? & (mP & mQ & ?) & ?). intuition. subst.
  exists mP (mQmR). repeat split.
  * apply (associative _).
  * solve_mem_disjoint.
  * done.
  * exists mQ mR. solve_mem_disjoint.
Qed.

Lemma assert_sep_assoc_2 P Q R : (P ★ (QR))%A ⊆ ((PQ) ★ R)%A.
Proof.
  intros ?? (mP & ? & ? & ? & ? & mQ & mR & ?). intuition. subst.
  exists (mPmQ) mR. repeat split.
  * by rewrite (associative _).
  * solve_mem_disjoint.
  * exists mP mQ. solve_mem_disjoint.
  * done.
Qed.

Instance: Associative (≡) (★)%A.
Proof. split. apply assert_sep_assoc_2. apply assert_sep_assoc_1. Qed.

Lemma assert_wand_1 (P Q R S : assert) : (PQ)%ARP ⊆ (Q -★ R)%A.
Proof. solve_assert. Qed.
Lemma assert_wand_2 (P Q : assert) : (P ★ (P -★ Q))%AQ.
Proof. rewrite (commutative (★))%A. solve_assert. Qed.

Lemma assert_and_sep_assoc (P Q R : assert) :
  MemIndep P
  (P ∧ (QR))%A ≡ ((PQ) ★ R)%A.
Proof. solve_assert. Qed.
Lemma assert_sep_and_assoc (P Q R : assert) :
  MemIndep R
  ((PQ) ∧ R)%A ≡ (P ★ (QR))%A.
Proof. solve_assert. Qed.

The separation conjunction allows us to give an alternative formulation of memory extensibility.
Lemma mem_ext_sep_true `{MemExt P} : P ≡ (PTrue)%A.
Proof.
  split.
  * intros ? m ?. exists m (∅ : mem).
    repeat split. apply (right_id _ _). solve_mem_disjoint. done.
  * intros ? ? (m1 & m2 & ? & ? & ? & ?). subst.
    eauto using mem_ext, finmap_subseteq_union_l.
Qed.

Lemma assert_sep_true_mem_ext P : P ≡ (PTrue)%AMemExt P.
Proof.
  intros H ρ m1 m2 ??. rewrite H.
  exists m1 (m2m1). repeat split; auto.
  * by rewrite <-finmap_union_difference.
  * by apply finmap_disjoint_difference_r.
Qed.

Lemma mem_ext_sep_true_iff P : P ≡ (PTrue)%AMemExt P.
Proof.
  split; intros. by apply assert_sep_true_mem_ext. by apply mem_ext_sep_true.
Qed.


Other type class instances for stack independence, memory independence, and memory extensibility.
Instance assert_emp_stack_indep : StackIndep emp.
Proof. solve_assert. Qed.
Instance assert_sep_stack_indep :
  StackIndep PStackIndep QStackIndep (PQ).
Proof. solve_assert. Qed.
Instance assert_sep_mem_indep :
  MemIndep PMemIndep QMemIndep (PQ).
Proof.
  intros ???? ? m1 m2 (m2' & m2'' & ? & ? & ?). subst.
  exists m2 (∅ : mem). repeat split.
  * by apply (right_id _ _).
  * solve_mem_disjoint.
  * solve_assert.
  * solve_assert.
Qed.

Instance assert_sep_mem_ext_2 : MemExt QMemExt (PQ).
Proof.
  intros ??? ? m1 m2 (m2' & m2'' & ? & ? & ? & ?) ?; subst.
  exists m2' (m2'' ∪ m2 ∖ (m2' ∪ m2'')). repeat split.
  * by rewrite (associative _), <-finmap_union_difference.
  * solve_mem_disjoint.
  * done.
  * apply mem_ext with m2''; auto with mem.
Qed.

Instance assert_sep_mem_ext_l : MemExt PMemExt (PQ).
Proof.
  intros P Q ????. rewrite !(commutative (★) P)%A.
  by apply assert_sep_mem_ext_2.
Qed.


Proofs of other useful properties.
Lemma assert_and_sep_emp_l (P Q : assert) :
  MemIndep P
  (PQ)%A ≡ ((Pemp) ★ Q)%A.
Proof. intro. by rewrite <-assert_and_sep_assoc, (left_id emp (★))%A. Qed.
Lemma assert_and_sep_emp_r (P Q : assert) :
  MemIndep Q
  (PQ)%A ≡ (P ★ (Qemp))%A.
Proof. intro. by rewrite !(commutative _ P), assert_and_sep_emp_l. Qed.

Lemma assert_sep_elim_l P1 P2 Q :
  MemExt Q
  P1Q → (P1P2)%AQ.
Proof. intros ? H. by rewrite mem_ext_sep_true, H, <-assert_true_intro. Qed.
Lemma assert_sep_elim_r P1 P2 Q :
  MemExt Q
  P2Q → (P1P2)%AQ.
Proof. rewrite (commutative (★))%A. apply assert_sep_elim_l. Qed.

The assertion Π Ps states that the memory can be split into disjoint parts such that for each part the corresponding assertion in Ps holds.
Definition assert_sep_list : list assertassert :=
  foldr (★)%A emp%A.
Notation "'Π' Ps" := (assert_sep_list Ps)
  (at level 20, formatPs") : assert_scope.

Lemma assert_sep_list_alt (Ps : list assert) ρ m :
  (Π Ps)%A ρ m ↔ ∃ ms,
    m = ⋃ ms
  ∧ list_disjoint ms
  ∧ Forall2 (λ (P : assert) m, P ρ m) Ps ms.
Proof.
  split.
  * revert m. induction Ps as [|P Ps IH].
    + eexists []. by repeat constructor.
    + intros ? (m1 & m2 & ? & ? & ? & ?); subst.
      destruct (IH m2) as (ms & ? & ? & ?); trivial; subst.
      exists (m1 :: ms). repeat constructor; trivial.
      by apply finmap_disjoint_union_list_r.
  * intros (m2 & ? & Hdisjoint & Hassert); subst.
    revert Hdisjoint.
    induction Hassert as [|P m Ps ms IH]; inversion_clear 1.
    + done.
    + exists m (⋃ ms). rewrite finmap_disjoint_union_list_r.
      intuition.
Qed.


Lemma assert_sep_list_alt_vec {n} (Ps : vec assert n) ρ m :
  (Π Ps)%A ρ m ↔ ∃ ms : vec mem n,
    m = ⋃ ms
  ∧ list_disjoint ms
  ∧ ∀ i, (Ps !!! i) ρ (ms !!! i).
Proof.
  rewrite assert_sep_list_alt. split.
  * intros (ms & ? & ? & Hms).
    assert (n = length ms); subst.
    { by erewrite <-Forall2_length, vec_to_list_length by eauto. }
    exists (list_to_vec ms).
    rewrite ?vec_to_list_of_list.
    by rewrite <-(vec_to_list_of_list ms), Forall2_vlookup in Hms.
  * intros [ms ?]. exists ms. by rewrite Forall2_vlookup.
Qed.


Lemma assert_sep_list_alt_vec_2 {n} (Ps : vec assert n) ρ (ms : vec mem n) :
  list_disjoint ms
  (∀ i, (Ps !!! i) ρ (ms !!! i)) →
  (Π Ps)%A ρ (⋃ ms).
Proof. intros. apply assert_sep_list_alt_vec. by exists ms. Qed.

Instance: Proper (eqlistA (≡) ==> (≡)) assert_sep_list.
Proof. induction 1; simpl; by f_equiv. Qed.

The assertion e1e2 asserts that the memory consists of exactly one cell at address e1 with contents e2 and the assertion e1 ↦ - asserts that the memory consists of exactly one cell at address e1 with arbitrary contents.
Definition assert_singleton (e1 e2 : expr) : assert := Assert $ λ ρ m, ∃ a v,
  ⟦ e1 ⟧ ρ m = Some (ptr a)%V ∧ ⟦ e2 ⟧ ρ m = Some vm = {[(a, v)]}.
Notation "e1e2" := (assert_singleton e1 e2)%A (at level 20) : assert_scope.
Definition assert_singleton_ (e : expr) : assert := Assert $ λ ρ m, ∃ a v,
  ⟦ e ⟧ ρ m = Some (ptr a)%Vm = {[(a, v)]}.
Notation "e ↦ -" := (assert_singleton_ e)%A
  (at level 20, format "e '↦' '-'") : assert_scope.

Lemma assert_singleton_forget e1 e2 : (e1e2)%A ⊆ (e1 ↦ -)%A.
Proof. solve_assert. Qed.

Instance assert_singleton_stack_indep e1 e2 :
  expr_vars e1 ≡ ∅ →
  expr_vars e2 ≡ ∅ →
  StackIndep (e1e2).
Proof.
  intros ?? ρ1 ρ2 m (a & v & ?). exists a v.
  by rewrite !(expr_var_free_stack_indep ρ2 ρ1).
Qed.

Instance assert_singleton_stack_indep_ e :
  expr_vars e ≡ ∅ →
  StackIndep (e ↦ -).
Proof.
  intros ? ρ1 ρ2 m (a & v & ?). exists a v.
  by rewrite !(expr_var_free_stack_indep ρ2 ρ1).
Qed.


Lemma assert_singleton_eval_l e1 v1 e2 :
  (e1v1val v1e2)%A ⊆ (e1e2)%A.
Proof. solve_assert. Qed.
Lemma assert_singleton_eval_r e1 v2 e2 :
  (e1val v2e2v2)%A ⊆ (e1e2)%A.
Proof. solve_assert. Qed.
Lemma assert_singleton_eval_ e v :
  (evval v ↦ -)%A ⊆ (e ↦ -)%A.
Proof. solve_assert. Qed.

Definition assert_assign (e1 e2 : expr) : assert := Assert $ λ ρ m, ∃ a v,
  ⟦ e1 ⟧ ρ m = Some (ptr a)%V ∧ ⟦ e2 ⟧ ρ m = Some vm !! a = Some v.
Notation "ev" := (assert_assign e v)%A (at level 20) : assert_scope.
Definition assert_assign_ (e : expr) : assert := Assert $ λ ρ m, ∃ a v,
  ⟦ e ⟧ ρ m = Some (ptr a)%Vm !! a = Some v.
Notation "e ↪ -" := (assert_assign_ e)%A
  (at level 20, format "e '↪' '-'") : assert_scope.

Lemma assert_assign_forget e1 e2 : (e1e2)%A ⊆ (e1 ↪ -)%A.
Proof. solve_assert. Qed.
Lemma assert_singleton_assign e1 e2 : (e1e2)%A ⊆ (e1e2)%A.
Proof.
  intros ρ ? (a&v&?&?&?); subst.
  exists a v. by rewrite lookup_singleton.
Qed.

Lemma assert_singleton_assign_ e : (e ↦ -)%A ⊆ (e ↪ -)%A.
Proof.
  intros ρ ? (a&v&?&?); subst.
  exists a v. by rewrite lookup_singleton.
Qed.


Lemma assert_assign_eval_l e1 v1 e2 :
  (e1v1val v1e2)%A ⊆ (e1e2)%A.
Proof. solve_assert. Qed.
Lemma assert_assign_eval_r e1 v2 e2 :
  (e1val v2e2v2)%A ⊆ (e1e2)%A.
Proof. solve_assert. Qed.
Lemma assert_assign_eval_ e v :
  (evval v ↪ -)%A ⊆ (e ↪ -)%A.
Proof. solve_assert. Qed.

Instance assert_assign_stack_indep e1 e2 :
  expr_vars e1 ≡ ∅ →
  expr_vars e2 ≡ ∅ →
  StackIndep (e1e2).
Proof.
  intros ?? ρ1 ρ2 m (a & v & ?). exists a v.
  by rewrite !(expr_var_free_stack_indep ρ2 ρ1).
Qed.

Instance assert_assign_stack_indep_ e :
  expr_vars e ≡ ∅ →
  StackIndep (e ↪ -).
Proof.
  intros ? ρ1 ρ2 m (a & v & ?). exists a v.
  by rewrite !(expr_var_free_stack_indep ρ2 ρ1).
Qed.

Instance assert_assign_mem_ext e1 e2 :
  MemExt (e1e2).
Proof.
  intros ρ m1 m2 (a & v & ? &?&?) ?. exists a v.
  repeat split; eauto using expr_eval_weaken_mem, lookup_weaken.
Qed.

Instance assert_assign_mem_ext_ e :
  MemExt (e ↪ -).
Proof.
  intros ρ m1 m2 (a & v & ? &?) ?. exists a v.
  repeat split; eauto using expr_eval_weaken_mem, lookup_weaken.
Qed.


Lemma assert_assign_assign_alt e1 e2 :
  expr_load_free e1expr_load_free e2
  (e1e2)%A ≡ (e1e2True)%A.
Proof.
  split.
  * intros ρ m (a & v &?&?&?). eexists {[ (a,v) ]}, (delete a m).
    repeat split.
    + by rewrite <-insert_union_singleton_l, insert_delete.
    + by apply finmap_disjoint_singleton_l, lookup_delete.
    + exists a v. by rewrite !(expr_load_free_mem_indep _ {[(a, v)]} m).
  * rewrite assert_singleton_assign. apply mem_ext_sep_true.
Qed.

Lemma assert_assign_assign_alt_ e :
  expr_load_free e
  (e ↪ -)%A ≡ (e ↦ - ★ True)%A.
Proof.
  split.
  * intros ρ m (a & v &?&?). eexists {[ (a,v) ]}, (delete a m).
    repeat split.
    + by rewrite <-insert_union_singleton_l, insert_delete.
    + by apply finmap_disjoint_singleton_l, lookup_delete.
    + exists a v. by rewrite !(expr_load_free_mem_indep _ {[(a, v)]} m).
  * rewrite assert_singleton_assign_. apply mem_ext_sep_true.
Qed.


Lemma assert_assign_load e v :
  (eval v)%A ≡ (load ev)%A.
Proof.
  split.
  * intros ρ m (a&v'&Ha&?&?). simplify_equality.
    unfold_assert. by rewrite Ha.
  * intros ρ m ?. unfold_assert in *.
    by destruct (⟦ e ⟧ ρ m) as [[| |[|]]|]; simpl in *; eauto.
Qed.

Lemma assert_assign_load_ e :
  (e ↪ -)%A ≡ (load e ⇓ -)%A.
Proof.
  split.
  * intros ρ m (a&v'&Ha&?). simplify_equality.
    unfold_assert. exists v'. by rewrite Ha.
  * intros ρ m [v ?]. unfold_assert in *.
    by destruct (⟦ e ⟧ ρ m) as [[| |[|]]|]; simpl in *; eauto.
Qed.


Lemma assert_singleton_load e v :
  (eval v)%A ⊆ (load ev)%A.
Proof. rewrite <-assert_assign_load. apply assert_singleton_assign. Qed.
Lemma assert_singleton_load_ e :
  (e ↦ -)%A ⊆ (load e ⇓ -)%A.
Proof. rewrite <-assert_assign_load_. apply assert_singleton_assign_. Qed.

The assertion P asserts that P holds if the stack is cleared. This connective allows us to specify stack independence in an alternative way.
Definition assert_clear_stack (P : assert) : assert := Assert $ λ _ m, P [] m.
Notation "P ↡" := (assert_clear_stack P) (at level 20) : assert_scope.

Instance assert_clear_stack_clear_stack_indep: StackIndep (P↡).
Proof. solve_assert. Qed.
Lemma stack_indep_clear_stack `{StackIndep P} : (P↡)%AP.
Proof. solve_assert. Qed.
Lemma stack_indep_clear_stack_iff P : StackIndep P ↔ (P↡)%AP.
Proof. solve_assert. Qed.

Lemma assert_clear_stack_impl P Q : ((PQ)↡)%A ≡ (P↡ → Q↡)%A.
Proof. solve_assert. Qed.
Lemma assert_clear_stack_not P : ((¬P)↡)%A ≡ (¬P↡)%A.
Proof. solve_assert. Qed.
Lemma assert_clear_stack_and P Q : ((PQ)↡)%A ≡ (P↡ ∧ Q↡)%A.
Proof. solve_assert. Qed.
Lemma assert_clear_stack_or P Q : ((PQ)↡)%A ≡ (P↡ ∨ Q↡)%A.
Proof. solve_assert. Qed.
Lemma assert_clear_stack_sep P Q : ((PQ)↡)%A ≡ (P↡ ★ Q↡)%A.
Proof. solve_assert. Qed.

Instance: Proper ((⊆) ==> (⊆)) assert_clear_stack.
Proof. solve_assert. Qed.
Instance: Proper ((≡) ==> (≡)) assert_clear_stack.
Proof. solve_assert. Qed.

To deal with block scope variables we need to lift an assertion such that the De Bruijn indexes of its variables are increased. We define the lifting P of an assertion P semantically, and prove that it indeed behaves as expected.
Definition assert_lift (P : assert) : assert := Assert $ λ ρ, P (tail ρ).
Notation "P ↑" := (assert_lift P) (at level 20) : assert_scope.

Lemma assert_lift_expr e v : ((ev)↑)%A ≡ ((e↑) ⇓ v)%A.
Proof. by split; intros ??; unfold_assert; rewrite expr_eval_lift. Qed.
Lemma assert_lift_expr_ e : ((e ⇓ -)↑)%A ≡ ((e↑) ⇓ -)%A.
Proof. by split; intros ??; unfold_assert; rewrite expr_eval_lift. Qed.
Lemma assert_lift_singleton e1 e2 : ((e1e2)↑)%A ≡ ((e1↑) ↦ (e2↑))%A.
Proof. by split; intros ??; unfold_assert; setoid_rewrite expr_eval_lift. Qed.
Lemma assert_lift_singleton_ e : ((e ↦ -)↑)%A ≡ ((e↑) ↦ -)%A.
Proof. by split; intros ??; unfold_assert; setoid_rewrite expr_eval_lift. Qed.
Lemma assert_lift_impl P Q : ((PQ)↑)%A ≡ (P↑ → Q↑)%A.
Proof. solve_assert. Qed.
Lemma assert_lift_not P : ((¬P)↑)%A ≡ (¬P↑)%A.
Proof. solve_assert. Qed.
Lemma assert_lift_and P Q : ((PQ)↑)%A ≡ (P↑ ∧ Q↑)%A.
Proof. solve_assert. Qed.
Lemma assert_lift_or P Q : ((PQ)↑)%A ≡ (P↑ ∨ Q↑)%A.
Proof. solve_assert. Qed.
Lemma assert_lift_sep P Q : ((PQ)↑)%A ≡ (P↑ ★ Q↑)%A.
Proof. solve_assert. Qed.
Lemma assert_lift_forall `(P : Aassert) : ((∀ x, P x)↑)%A ≡ (∀ x, P x↑)%A.
Proof. solve_assert. Qed.
Lemma assert_lift_exists `(P : Aassert) : ((∃ x, P x)↑)%A ≡ (∃ x, P x↑)%A.
Proof. solve_assert. Qed.

Instance: Proper ((⊆) ==> (⊆)) assert_lift.
Proof. solve_assert. Qed.
Instance: Proper ((≡) ==> (≡)) assert_lift.
Proof. solve_assert. Qed.

Instance assert_lift_stack_indep: StackIndep PStackIndep (P↑).
Proof. solve_assert. Qed.
Lemma stack_indep_lift `{StackIndep P} : (P↑)%AP.
Proof. solve_assert. Qed.

The assertion assert_forall2 P xs ys asserts that P x y holds for each corresponding pair x and y of elements of xs and ys.
Definition assert_forall2 `(P : ABassert) : list Alist Bassert :=
  fix go xs ys :=
  match xs, ys with
  | [], [] => True
  | x :: xs, y :: ys => P x ygo xs ys
  | _, _ => False
  end%A.

An alternative semantic formulation of the above assertion.
Lemma assert_forall2_correct `(P : ABassert) xs ys ρ m :
  assert_forall2 P xs ys ρ mForall2x y, P x y ρ m) xs ys.
Proof.
  split.
  * revert ys. induction xs; intros [|??]; solve_assert.
  * induction 1; solve_assert.
Qed.


The rule for blocks is of the shape { var 0 ↦ - * P↑ } blk s { var 0 ↦ - * Q↑ } implies {P} s {Q}. We prove that this pre and postcondition is correct with respect to allocation of a local variable when entering a block and freeing a local variable when leaving a block.
Lemma assert_alloc (P : assert) (b : index) (v : value) (ρ : stack) m :
  is_free m b
  P ρ m
  (var 0 ↦ - ★ P↑)%A (b :: ρ) (<[b:=v]>m).
Proof.
  intros ??. eexists {[(b, v)]}, m. repeat split.
  * by rewrite insert_union_singleton_l.
  * solve_mem_disjoint.
  * by exists b v.
  * done.
Qed.


Lemma assert_free (P : assert) (b : index) (ρ : stack) m :
  (var 0 ↦ - ★ P↑)%A (b :: ρ) m
  P ρ (delete b m) ∧ ∃ v, m !! b = Some v.
Proof.
  intros (m1 & m2 & ? & ? & (a & v & ? & ?) & ?); simplify_equality.
  rewrite <-insert_union_singleton_l, delete_insert by solve_mem_disjoint.
  simplify_map_equality; eauto.
Qed.


We prove some properties related to allocation of local variables when calling a function, and to freeing these when returning from the function call.
Lemma assert_alloc_params (P : assert) (ρ : stack) m1 bs vs m2 :
  StackIndep P
  alloc_params m1 bs vs m2
  P ρ m1
  (Π imapi v, var ival v) vsP)%A (bs ++ ρ) m2.
Proof.
  intros ? Halloc ?. cut (∀ bs',
    (Π imap_goi v, var ival v) (length bs') vsP)%A
      (bs' ++ bs ++ ρ) m2).
  { intros aux. by apply (aux []). }
  induction Halloc as [| b bs v vs m2 ?? IH ]; intros bs'; simpl.
  * rewrite (left_id emp (★))%A. by apply (stack_indep ρ).
  * rewrite <-(associative (★))%A. eexists {[(b, v)]}, m2. repeat split.
    + by rewrite insert_union_singleton_l.
    + solve_mem_disjoint.
    + exists b v. repeat split. simpl.
      by rewrite list_lookup_middle.
    + specialize (IH (bs' ++ [b])).
      rewrite app_length in IH. simpl in IH.
      by rewrite NPeano.Nat.add_1_r, <-app_assoc in IH.
Qed.


Lemma assert_alloc_params_alt (P : assert) (ρ : stack) m bs vs :
  StackIndep P
  same_length bs vs
  is_free_list m bs
  P ρ m
  (Π imapi v, var ival v) vsP)%A (bs ++ ρ)
    (insert_list (zip bs vs) m).
Proof. eauto using assert_alloc_params, alloc_params_insert_list_2. Qed.

Lemma assert_free_params (P : assert) (ρ : stack) m (bs : list index)
    (vs : list value) :
  StackIndep P
  same_length bs vs
  NoDup bs
  (Π imapi _, var i ↦ -) vsP)%A (bs ++ ρ) m
  P ρ (delete_list bs m) ∧ Forallb, ∃ v, m !! b = Some v) bs.
Proof.
  intros ? Hlength. revert m. cut (∀ bs' m,
    NoDup bs
    (Π imap_goi _, var i ↦ -) (length bs') vsP)%A
      (bs' ++ bs ++ ρ) m
    P ρ (delete_list bs m) ∧ Forallb, ∃ v, m !! b = Some v) bs).
  { intros aux. by apply (aux []). }
  induction Hlength as [|b v bs vs ? IH];
    intros bs' m; simpl; inversion_clear 1.
  * rewrite (left_id emp (★))%A. split.
    + by apply (stack_indep (bs' ++ ρ)).
    + done.
  * rewrite <-(associative (★))%A.
    intros (m1 & m2 & ? & ? & (b' & v' & Heval & ?) & ?).
    simplify_equality. simpl in Heval.
    rewrite list_lookup_middle in Heval. simplify_equality.
    rewrite <-insert_union_singleton_l, delete_list_insert_comm by done.
    feed destruct (IH (bs' ++ [b']) m2) as [??]; trivial.
    { by rewrite app_length, NPeano.Nat.add_1_r, <-app_assoc. }
    split.
    + rewrite delete_insert; [done |].
      rewrite lookup_delete_list_not_elem_of by done.
      solve_mem_disjoint.
    + constructor; simplify_mem_equality; eauto.
      apply Forall_impl withb, ∃ v, m2 !! b = Some v); trivial.
      intros b [??].
      destruct (decide (b = b')); simplify_mem_equality; eauto.
Qed.