NB: This Coq documentation contains a revised version of the Coq implementation of these papers [1], [2], [3], [4], and is also the support for ongoing research. A partial archive (14/01/2001) is available at here. Drop us a line if you are interested in a complete, up-to-date archive.

Library encode_decode

Require Import ssreflect ssrbool eqtype.
Require Import Arith_ext ZArith_ext Lists_ext.
Require Import machine_int multi_int.
Import MachineInt.
Require Import mips_bipl mapstos.
Import mips_bipl.expr_m.
Import mips_bipl.assert_m.

Local Open Scope machine_int_scope.
Local Open Scope heap_scope.
Local Open Scope mips_assert_scope.

construct a heap from a list of int 32's

Definition list2heap (a : nat) (l : list (int 32)) : heap.t :=
  map_prop_m.mk_finmap (seq_ext.l2s (combine (List.seq a (length l)) l)).

Lemma dom_list2heap : forall l x,
  heap.dom (list2heap x l) = seq_ext.l2s (List.seq x (length l)).
Proof.
move=> l x.
rewrite /list2heap -heap.elts_dom map_prop_m.elts_mk_finmap; last first.
  rewrite seq_ext.unzip1_l2s /= map_fst_split combine_split /=; last by rewrite seq_length.
  by apply ordset.ordered_seq.
by rewrite -seq_ext.l2s_map map_fst_split combine_split // seq_length.
Qed.

Lemma cdom_list2heap : forall l x, heap.cdom (list2heap x l) = seq_ext.l2s l.
Proof.
move=> l x.
rewrite /list2heap -heap.elts_cdom map_prop_m.elts_mk_finmap; last first.
  rewrite seq_ext.unzip1_l2s map_fst_split combine_split /=; last by rewrite seq_length.
  by apply ordset.ordered_seq.
by rewrite -seq_ext.l2s_map map_snd_split combine_split // seq_length.
Qed.

Lemma disj_list2heap : forall l n h,
  disj (List.seq n (length l)) (seq_ext.s2l (heap.dom h)) ->
  list2heap n l # h.
Proof.
move=> l n h H; rewrite heap.disjE; apply/seq_ext.disP.
by rewrite dom_list2heap // seq_ext.s2l2s.
Qed.

Local Open Scope zarith_ext_scope.
Local Open Scope mips_expr_scope.

Lemma mapstos_list2heap : forall l n e s, u2Z ( [ e ]e_ s ) = 4 * Z_of_nat n ->
  u2Z ( [ e ]e_ s ) + 4 * (Z_of_nat (length l) - 1) < Zbeta 1 ->
  (e |--> l) s (list2heap n l).
Proof.
elim=> [n e s e_mod e_fit | hd tl IH v n0 s Hv Hn /=].
- split; last by done.
  apply Zdivide_mod.
  exists (Z_of_nat n); by rewrite Zmult_comm.
- destruct tl as [|i tl].
  + rewrite /list2heap /= heap.union_emp_R.
    exists (heap.sing v hd), heap.emp; split; first by apply heap.disj_emp_R.
    split; first by rewrite heap.union_emp_R.
    split.
    * by exists v.
    * split; last by done.
      apply u2Z_add_mod => //.
      apply Zdivide_mod.
      exists (Z_of_nat v); by rewrite Zmult_comm.
  + rewrite [i :: _]lock /list2heap /= -lock.
    apply assert_m.con_cons.
    * apply heap.disj_sym, disj_list2heap.
      rewrite heap.dom_sing.
      apply disj_seq_singl.
      rewrite Z_S; omega.
    * by exists v.
    * apply (mapstos_ext _ s _ _ (int_e ([ n0 ]e_s [.+] four32))) => //.
      apply IH.
      - rewrite u2Z_add_Z2u //; last first.
          rewrite (_ : Z_of_nat _ - 1 = 1 + Z_of_nat (length tl)) in Hn; last first.
            rewrite [length _]/= !Z_S; ring.
          rewrite -Zbeta1_Zpower2; omega.
        rewrite Z_S Hv; ring.
      - rewrite u2Z_add_Z2u //; last first.
          rewrite !Z_S in Hn; rewrite -Zbeta1_Zpower2; omega.
        rewrite (_ : Z_of_nat _ - 1 = Z_of_nat (length (i :: tl))) in Hn; last first.
          rewrite [length _]/= !Z_S; ring.
        omega.
Qed.

Lemma mapstos_inv_list2heap : forall l e s h, (e |--> l) s h ->
  u2Z ( [ e ]e_ s) + 4 * Z_of_nat (length l) < Zbeta 1 ->
  h = list2heap (Zabs_nat (u2Z ( [ e ]e_ s [.>>] 2))) l.
Proof.
elim=> [e s h Hmem Hfit /= | hd tl IH e s h].
- rewrite /= in Hmem.
  by case: Hmem.
- rewrite [assert_m.mapstos _ _]/=.
  case=> h1 [h2 [Hdisj [Hunion [Hmem1 Hmem2]]]] Hinmem.
  case: Hmem1 => loc [H1 H2].
  rewrite /= in H2 *.
  have -> : Zabs_nat (u2Z ( [ e ]e_ s [.>>] 2)) = loc.
    rewrite (@shrl_2 _ (Z_of_nat loc)) // u2Z_Z2u //.
    by rewrite Zabs_nat_Z_of_nat.
    split; first by apply Zle_0_nat.
    move: (max_u2Z ( [ e ]e_ s)).
    rewrite H1 (_ : 2 ^^ 32 = 2 ^^ 30 * 4) // Zmult_comm => X.
    apply Zmult_gt_0_lt_reg_r in X => //; omega.
  rewrite /list2heap /=.
  have <- : Zabs_nat (u2Z ([ e ]e_ s [.+] four32 [.>>] 2)) = S loc.
    move: (@u2Z_shrl _ ([ e ]e_ s [.+] four32) 2) => // X.
    rewrite [Zpower _ _]/= (@u2Z_rem'' _ _ _ (1 + Z_of_nat loc)) in X; last first.
      rewrite u2Z_add_Z2u // H1.
      + rewrite [Zpower _ _]/=; ring.
      + rewrite Z_S in Hinmem; rewrite -Zbeta1_Zpower2; omega.
    rewrite Zplus_0_r u2Z_add_Z2u // in X; last first.
      rewrite Z_S in Hinmem; rewrite -Zbeta1_Zpower2; omega.
    have -> : u2Z (eval e s [.+] four32 [.>>] 2) = 1 + Z_of_nat loc by omega.
    rewrite Zabs_nat_plus_pos //; last by apply Zle_0_nat.
    by rewrite Zabs_nat_Z_of_nat.
  move: {IH}(IH _ _ _ Hmem2).
  rewrite /list2heap.
  move=> <- //; last first.
    rewrite [eval _ _]/= u2Z_add_Z2u //.
    + rewrite [length _]/= Z_S in Hinmem; omega.
    + rewrite Z_S in Hinmem; rewrite -Zbeta1_Zpower2; omega.
  by rewrite -H2.
Qed.

Local Close Scope zarith_ext_scope.

extract a list of contiguous int 32's from a heap

Definition heap2list (b : heap.l) (n : nat) (h : heap.t) : list heap.v :=
  seq_ext.s2l (heap.cdom (heap.proj h (seq_ext.ran b n))).

Lemma len_heap2list : forall (n : nat) (a : heap.l) h,
  incl (seq a n) (seq_ext.s2l (heap.dom h)) -> length (heap2list a n h) = n.
Proof.
move=> n a h H.
have {H}H : seq_ext.inc (seq_ext.ran a n) (heap.dom h).
  apply/seq_ext.incP; by rewrite -seq_ext.l2s_seq seq_ext.s2l2s.
apply heap.dom_proj_exact in H; last first.
  rewrite -seq_ext.l2s_seq; by apply ordset.ordered_seq.
by rewrite seq_ext.len_s2l heap.size_cdom_dom H seq_ext.size_ran.
Qed.

Lemma heap2list2heap : forall n z l, length l = n ->
  heap2list z n (list2heap z l) = l.
Proof.
elim => [z [] //= _ | n IH z [|h t] // [len_t] ].
- by rewrite /heap2list heap.proj_emp heap.cdom_emp.
- rewrite /heap2list /list2heap /= heap.proj_union_sing; last first.
    by rewrite seq.in_cons eqxx.
  rewrite heap.cdom_union_sing /=.
  + f_equal.
    rewrite heap.dom_proj_cons.
    * by apply IH.
    * rewrite dom_list2heap //.
      apply/negP; move/seq_ext.inP. rewrite seq_ext.s2l2s.
      move/In_seq_inv => ?; omega.
  + move=> m.
    case/heap.in_dom_proj_inter => Hm1 Hm2.
    rewrite dom_list2heap // in Hm1.
    rewrite /heap.ltl /order.NatOrder.ltA.
    apply/ssrnat.ltP.
    move/seq_ext.inP : Hm1. rewrite seq_ext.s2l2s.
    move/In_seq_inv => ?; omega.
Qed.

Lemma heap2list_list2heap_union : forall n z l h, length l = n ->
  list2heap z l # h ->
  heap2list z n (list2heap z l +++ h) = heap2list z n (list2heap z l).
Proof.
move=> n z lst h Hn Hdisj.
rewrite /heap2list -seq_ext.l2s_seq.
move: (dom_list2heap lst z).
rewrite Hn => <-.
by rewrite heap.proj_union_L // heap.proj_itself.
Qed.