Module memory

This file defines values, the memory and some operations on it. The definitions of values and memory are still rather simple in this version of the development: the memory is a finite map from naturals to values, and a value is either a pointer to a memory cell, an unbounded integer, or the special void value.
Furthermore, this file defines a hint database mem that contains useful facts on the memory, and defines some tactics to simplify goals involving propositions on the memory.
Require Export nmap.

Values

We define indexes into the memory as binary naturals and use the Nmap implementation to obtain efficient finite maps with these indexes as keys.
Definition index := N.
Definition indexmap := Nmap.

Instance index_dec: ∀ i1 i2 : index, Decision (i1 = i2) := decide_rel (=).
Instance index_fresh_`{FinCollection index C} : Fresh index C := _.
Instance index_fresh_spec `{FinCollection index C} : FreshSpec index C := _.
Instance index_inhabited: Inhabited index := populate 0%N.

Instance indexmap_dec {A} `{∀ a1 a2 : A, Decision (a1 = a2)} :
  ∀ m1 m2 : indexmap A, Decision (m1 = m2) := decide_rel (=).
Instance indexmap_empty {A} : Empty (indexmap A) := @empty (Nmap A) _.
Instance indexmap_lookup {A} : Lookup index A (indexmap A) :=
  @lookup _ _ (Nmap A) _.
Instance indexmap_partial_alter {A} : PartialAlter index A (indexmap A) :=
  @partial_alter _ _ (Nmap A) _.
Instance indexmap_to_list {A} : FinMapToList index A (indexmap A) :=
  @finmap_to_list _ _ (Nmap A) _.
Instance indexmap_merge {A} : Merge A (indexmap A) := @merge _ (Nmap A) _.
Instance indexmap_fmap: FMap indexmap := λ A B f, @fmap Nmap _ _ f _.
Instance: FinMap index indexmap := _.

Typeclasses Opaque index indexmap.

A value is inductively defined to be either a special void value (used for functions without return value), an unbounded integer, or a pointer represented by an index into the memory. This index is optional so as to model the NULL pointer.
Inductive value :=
  | VVoid : value
  | VInt : Zvalue
  | VPtr : option indexvalue.

Instance value_eq_dec (v1 v2 : value) : Decision (v1 = v2).
Proof. solve_decision. Defined.
Instance value_inhabited: Inhabited value := populate VVoid.

We define better readable notations for values in the scope value_scope.
Delimit Scope value_scope with V.
Bind Scope value_scope with value.
Notation "'void'" := VVoid : value_scope.
Notation "'int' x" := (VInt x) (at level 10) : value_scope.
Notation "'ptr' b" := (VPtr (Some b)) (at level 10) : value_scope.
Notation "'null'" := (VPtr None) : value_scope.

Truth and falsehood of values is defined in the C-like way.
Definition value_true (v : value) : Prop :=
  match v with
  | void => False
  | int x => (x ≠ 0)%Z
  | ptr b => True
  | null => False
  end%V.
Definition value_false (v : value) : Prop :=
  match v with
  | void => True
  | int x => (x = 0)%Z
  | ptr b => False
  | null => True
  end%V.

Definition value_true_false_dec v : { value_true v } + { value_false v }.
Proof.
 by refine (
  match v as v return { value_true v } + { value_false v } with
  | void => right I
  | int x => cast_if_not (decide (x = 0%Z))
  | ptr b => left I
  | null => right I
  end%V).
Defined.


Lemma value_true_false v : value_true vvalue_false vFalse.
Proof. destruct v as [| |[]]; simpl; auto. Qed.

Definition is_ptr (v : value) : option index :=
  match v with
  | ptr a => Some a
  | _ => None
  end%V.
Lemma is_ptr_Some v a : is_ptr v = Some av = (ptr a)%V.
Proof.
  split.
  * by destruct v as [| | [?|]]; intro; simplify_equality.
  * intro. by simplify_equality.
Qed.


Definition of the memory

Notation mem := (indexmap value).

Hint Resolve (lookup_singleton (M:=indexmap)) : mem.
Hint Resolve (lookup_insert (M:=indexmap)) : mem.
Hint Resolve finmap_disjoint_empty_l finmap_disjoint_empty_r : mem.
Hint Resolve finmap_disjoint_singleton_l_2 finmap_disjoint_singleton_r_2 : mem.
Hint Constructors list_disjoint : mem.
Hint Resolve lookup_union_Some_l lookup_union_Some_r : mem.
Hint Resolve finmap_subseteq_union_l finmap_subseteq_union_r : mem.
Hint Resolve finmap_disjoint_union_l_2 finmap_disjoint_union_r_2 : mem.
Hint Resolve finmap_disjoint_insert_l_2 finmap_disjoint_insert_r_2 : mem.
Hint Resolve finmap_disjoint_delete_l finmap_disjoint_delete_r : mem.
Hint Resolve finmap_disjoint_of_list_zip_l_2 finmap_disjoint_of_list_zip_r_2 : mem.
Hint Resolve finmap_disjoint_union_list_l_2 finmap_disjoint_union_list_r_2 : mem.
Hint Resolve finmap_disjoint_delete_list_l finmap_disjoint_delete_list_r : mem.
Hint Resolve finmap_list_disjoint_delete_vec : mem.
Hint Resolve finmap_list_disjoint_insert_vec : mem.
Hint Resolve finmap_disjoint_difference_l finmap_disjoint_difference_r : mem.
Hint Resolve Forall_vlookup_2 : mem.
Hint Resolve Forall_delete : mem.
Hint Extern 1 (__) => done : mem.

Ltac solve_mem_disjoint :=
  solve [decompose_map_disjoint; auto with mem].

Tactic Notation "simplify_mem_equality" "by" tactic3(tac) := repeat
  match goal with
  | _ => progress (simplify_map_equality by tac)
  | H : ?m_ = ?m_ |- _ =>
    apply finmap_union_cancel_r in H; [| solve[tac] | solve [tac]]
  | H : _ ∪ ?m = _ ∪ ?m |- _ =>
    apply finmap_union_cancel_l in H; [| solve[tac] | solve [tac]]
  | H : context[ (?m1 ∪ ?m2) !! ?a ] |- _ =>
    let v := fresh in evar (v:value);
    let v' := eval unfold v in v in clear v;
    let Hv := fresh in
    assert ((m1m2) !! a = Some v') as Hv
      by (clear H; by eauto with mem);
    rewrite Hv in H; clear Hv
  end.
Tactic Notation "simplify_mem_equality" :=
  simplify_mem_equality by solve_mem_disjoint.

Free indexes in a memory

A memory index is free if it contains no contents.
Definition is_free (m : mem) (b : index) : Prop := m !! b = None.

Lemma is_free_lookup_None m b :
  is_free m bm !! b = None.
Proof. done. Qed.
Hint Resolve is_free_lookup_None : mem.

Lemma is_free_Forall_lookup_None m bs :
  Forall (is_free m) bsForallb, m !! b = None) bs.
Proof. done. Qed.
Hint Resolve is_free_Forall_lookup_None : mem.

Lemma is_free_lookup_Some m b v :
  is_free m b → ¬(m !! b = Some v).
Proof. unfold is_free. congruence. Qed.

Lemma is_free_dom C `{Collection index C} m b :
  bdom C mis_free m b.
Proof. apply (not_elem_of_dom _). Qed.

Lemma is_free_subseteq (m1 m2 : mem) b :
  is_free m2 bm1m2is_free m1 b.
Proof. apply lookup_weaken_None. Qed.
Hint Immediate is_free_subseteq : mem.

Lemma is_free_union m1 m2 b :
  is_free (m1m2) bis_free m1 bis_free m2 b.
Proof. apply lookup_union_None. Qed.

Lemma is_free_union_2 m1 m2 b :
  is_free m1 bis_free m2 bis_free (m1m2) b.
Proof. by rewrite is_free_union. Qed.
Hint Resolve is_free_union_2 : mem.

Lemma is_free_insert m b b' v :
  is_free (<[b':=v]>m) bis_free m bb' ≠ b.
Proof. apply lookup_insert_None. Qed.
Lemma is_free_insert_2 b b' v m :
  is_free m bb' ≠ bis_free (<[b':=v]>m) b.
Proof. rewrite is_free_insert. auto. Qed.
Hint Resolve is_free_insert_2 : mem.

We lift the notion of free indexes to lists of indexes.
Inductive is_free_list (m : mem) : list indexProp :=
  | is_free_nil :
     is_free_list m []
  | is_free_cons b bs :
     bbsis_free m bis_free_list m bsis_free_list m (b :: bs).
Hint Constructors is_free_list : mem.

We prove that the inductive definition is_free_list m bs is equivalent to all bs being free, and the list bs containing no duplicates.
Lemma is_free_list_nodup m bs : is_free_list m bsNoDup bs.
Proof. induction 1; by constructor. Qed.
Lemma is_free_list_free m bs : is_free_list m bsForall (is_free m) bs.
Proof. induction 1; firstorder. Qed.
Hint Resolve is_free_list_nodup is_free_list_free : mem.
Lemma is_free_list_make m bs :
  NoDup bsForall (is_free m) bsis_free_list m bs.
Proof. induction 1; inversion 1; auto with mem. Qed.

Lemma is_free_list_subseteq m1 m2 bs :
  m1m2is_free_list m2 bsis_free_list m1 bs.
Proof. induction 2; eauto with mem. Qed.

Lemma is_free_insert_list m b l :
  bfst <$> lis_free m bis_free (insert_list l m) b.
Proof.
  induction l; simpl; [done|].
  * rewrite elem_of_cons, is_free_insert. intuition.
Qed.

Hint Resolve is_free_insert_list : mem.

A memory cell is writable if it contains contents. In future versions this notion will also take permissions into account.
Definition is_writable (m : mem) (b : index) : Prop := is_Some (m !! b).

The following definitions allow to generate fresh memory indexes, or lists of fresh memory indexes.
Definition fresh_index (m : mem) : index := fresh (dom (listset index) m).
Definition fresh_indexes (m : mem) (n : nat) : list index :=
  fresh_list n (dom (listset index) m).

Lemma is_free_fresh_index m : is_free m (fresh_index m).
Proof.
  unfold fresh_index.
  apply (is_free_dom (listset _)). apply is_fresh.
Qed.

Hint Resolve is_free_fresh_index : mem.

Lemma fresh_indexes_length m n : length (fresh_indexes m n) = n.
Proof. apply fresh_list_length. Qed.
Lemma is_free_list_fresh_indexes n m : is_free_list m (fresh_indexes m n).
Proof.
  apply is_free_list_make.
  * apply fresh_list_nodup.
  * apply Forall_forall. intro.
    rewrite <-(is_free_dom (listset _)).
    apply fresh_list_is_fresh.
Qed.

Hint Resolve is_free_list_fresh_indexes : mem.

Lemma is_free_list_union m1 m2 bs :
  is_free_list (m1m2) bsis_free_list m1 bsis_free_list m2 bs.
Proof.
  induction bs.
  * intuition constructor.
  * split.
    + inversion_clear 1. rewrite is_free_union in *.
      repeat constructor; intuition.
    + intros []. do 2 inversion_clear 1.
      constructor; rewrite ?is_free_union; intuition.
Qed.

Lemma is_free_list_union_2 m1 m2 bs :
  is_free_list m1 bsis_free_list m2 bsis_free_list (m1m2) bs.
Proof. by rewrite is_free_list_union. Qed.
Hint Resolve is_free_list_union_2 : mem.

The tactic simplify_is_free simplifies assumptions of the shape is_free involving the union or insert operation.
Ltac decompose_is_free := repeat
  match goal with
  | H : is_free (__) _ |- _ => apply is_free_union in H; destruct H
  | H : is_free (<[_:=_]>_) _ |- _ => apply is_free_insert in H; destruct H
  | H : is_free_list (__) _ |- _ => apply is_free_list_union in H; destruct H
  end.

Allocation of parameters

We define allocation of the parameters of a function inductively and prove that it is equivalent to an alternative formulation that is used for the soundness proof of the axiomatic semantics.
Inductive alloc_params (m : mem) : list indexlist valuememProp :=
  | alloc_params_nil : alloc_params m [] [] m
  | alloc_params_cons b bs v vs m2 :
     is_free m2 b
     alloc_params m bs vs m2
     alloc_params m (b :: bs) (v :: vs) (<[b:=v]>m2).

Lemma alloc_params_same_length m1 bs m2 vs :
  alloc_params m1 bs vs m2same_length bs vs.
Proof. induction 1; by constructor. Qed.

Lemma alloc_params_lookup m1 bs vs m2 b v i :
  alloc_params m1 bs vs m2
  bs !! i = Some bvs !! i = Some vm2 !! b = Some v.
Proof.
  intros Halloc. revert i.
  induction Halloc; intros [|i] ??; simpl; simplify_map_equality; trivial.
  feed pose proof (IHHalloc i); auto.
  rewrite lookup_insert_ne; auto.
  intro. subst. edestruct is_free_lookup_Some; eauto.
Qed.


Lemma alloc_params_subseteq m1 bs vs m2 :
  alloc_params m1 bs vs m2m1m2.
Proof. induction 1; eauto using insert_subseteq_r with mem. Qed.
Lemma alloc_params_is_free m1 bs vs m2 b :
  alloc_params m1 bs vs m2is_free m2 bis_free m1 b.
Proof. eauto using is_free_subseteq, alloc_params_subseteq. Qed.

Lemma alloc_params_free m1 bs vs m2 :
  alloc_params m1 bs vs m2is_free_list m1 bs.
Proof.
  induction 1; constructor; simpl; auto with mem.
  * rewrite elem_of_list_lookup. intros [i ?].
    feed inversion (same_length_lookup bs vs i) as [v'];
     eauto using alloc_params_same_length.
    destruct (is_free_lookup_Some m2 b v');
      eauto using alloc_params_lookup.
  * eauto using alloc_params_is_free.
Qed.


Lemma alloc_params_insert_list_1 m1 bs vs m2 :
  alloc_params m1 bs vs m2m2 = insert_list (zip bs vs) m1.
Proof. induction 1; simpl; by f_equal. Qed.
Lemma alloc_params_insert_list_2 m bs vs :
  same_length bs vs
  is_free_list m bs
  alloc_params m bs vs (insert_list (zip bs vs) m).
Proof.
  induction 1; inversion_clear 1; simpl; constructor; auto.
  apply is_free_insert_list; auto.
  by rewrite zip_fst.
Qed.


Lemma alloc_params_insert_list m1 bs vs m2 :
  alloc_params m1 bs vs m2
   ↔ m2 = insert_list (zip bs vs) m1is_free_list m1 bssame_length bs vs.
Proof.
  split.
  * intuition eauto using alloc_params_insert_list_1,
     alloc_params_free, alloc_params_same_length.
  * intros [?[??]]. subst. by apply alloc_params_insert_list_2.
Qed.


Lemma alloc_params_weaken m1 bs vs m2 m3 :
  m1m3
  m2m3
  alloc_params (m1m3) bs vs (m2m3) →
  alloc_params m1 bs vs m2.
Proof.
  rewrite !alloc_params_insert_list, !insert_list_union.
  intuition idtac.
  * apply finmap_union_cancel_l with m3.
    + done.
    + decompose_is_free.
      apply finmap_disjoint_union_l_2; [|done].
      apply finmap_disjoint_of_list_zip_l; auto with mem.
    + by rewrite <-(associative_eq (∪)).
  * by decompose_is_free.
Qed.