relecture sylvain

avec TODOs pour refactoring #90

8 files changed, 353 insertions, 505 deletions

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 3bcb321d..0f65b1d0 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -33,13 +33,234 @@ Require Import Conventions.
 Require Import Errors.
 Require Export Asmvliw.
 
+
+(** * Auxiliary utilies on basic blocks *)
+
+(** ** A unified view of Kalray instructions *)
+
+Inductive instruction : Type :=
+  | PBasic    (i: basic)
+  | PControl  (i: control)
+.
+
+Coercion PBasic:    basic >-> instruction.
+Coercion PControl:  control >-> instruction.
+
+Definition code := list instruction.
+Definition bcode := list basic.
+
+Fixpoint basics_to_code (l: list basic) :=
+  match l with
+  | nil => nil
+  | bi::l => (PBasic bi)::(basics_to_code l)
+  end.
+
+Fixpoint code_to_basics (c: code) :=
+  match c with
+  | (PBasic i)::c =>
+    match code_to_basics c with
+    | None => None
+    | Some l => Some (i::l)
+    end
+  | _::c => None
+  | nil => Some nil
+  end.
+
+Lemma code_to_basics_id: forall c, code_to_basics (basics_to_code c) = Some c.
+Proof.
+  intros. induction c as [|i c]; simpl; auto.
+  rewrite IHc. auto.
+Qed.
+
+Lemma code_to_basics_dist:
+  forall c c' l l',
+  code_to_basics c = Some l ->
+  code_to_basics c' = Some l' ->
+  code_to_basics (c ++ c') = Some (l ++ l').
+Proof.
+  induction c as [|i c]; simpl; auto.
+  - intros. inv H. simpl. auto.
+  - intros. destruct i; try discriminate. destruct (code_to_basics c) eqn:CTB; try discriminate.
+    inv H. erewrite IHc; eauto. auto.
+Qed.
+
+(** 
+  Asmblockgen will have to translate a Mach control into a list of instructions of the form
+   i1 :: i2 :: i3 :: ctl :: nil ; where i1..i3 are basic instructions, ctl is a control instruction
+  These functions provide way to extract the basic / control instructions
+*)
+
+Fixpoint extract_basic (c: code) :=
+  match c with
+  | nil => nil
+  | PBasic i :: c => i :: (extract_basic c)
+  | PControl i :: c => nil
+  end.
+
+Fixpoint extract_ctl (c: code) :=
+  match c with
+  | nil => None
+  | PBasic i :: c => extract_ctl c
+  | PControl i :: nil => Some i
+  | PControl i :: _ => None (* if the first found control instruction isn't the last *)
+  end.
+
+(** ** Wellformness of basic blocks *)
+
+Ltac exploreInst :=
+  repeat match goal with
+  | [ H : match ?var with | _ => _ end = _ |- _ ] => destruct var
+  | [ H : OK _ = OK _ |- _ ] => monadInv H
+  | [ |- context[if ?b then _ else _] ] => destruct b
+  | [ |- context[match ?m with | _ => _ end] ] => destruct m
+  | [ |- context[match ?m as _ return _ with | _ => _ end]] => destruct m
+  | [ H : bind _ _ = OK _ |- _ ] => monadInv H
+  | [ H : Error _ = OK _ |- _ ] => inversion H
+  end.
+
+Definition non_empty_bblock (body: list basic) (exit: option control): Prop
+ := body <> nil \/ exit <> None.
+
+Lemma non_empty_bblock_refl:
+  forall body exit,
+  non_empty_bblock body exit <->
+  Is_true (non_empty_bblockb body exit).
+Proof.
+  intros. split.
+  - destruct body; destruct exit.
+    all: simpl; auto. intros. inversion H; contradiction.
+  - destruct body; destruct exit.
+    all: simpl; auto.
+    all: intros; try (right; discriminate); try (left; discriminate).
+    contradiction.
+Qed.
+
+Definition builtin_alone (body: list basic) (exit: option control) := forall ef args res,
+  exit = Some (PExpand (Pbuiltin ef args res)) -> body = nil.
+
+
+Lemma builtin_alone_refl:
+  forall body exit,
+  builtin_alone body exit <-> Is_true (builtin_aloneb body exit).
+Proof.
+  intros. split.
+  - destruct body; destruct exit.
+    all: simpl; auto.
+    all: exploreInst; simpl; auto.
+    unfold builtin_alone. intros. assert (Some (Pbuiltin e l b0) = Some (Pbuiltin e l b0)); auto.
+    assert (b :: body = nil). eapply H; eauto. discriminate.
+  - destruct body; destruct exit.
+    all: simpl; auto; try constructor.
+    + exploreInst; try discriminate.
+        simpl. contradiction.
+    + intros. discriminate.
+Qed.
+
+Definition wf_bblock (body: list basic) (exit: option control) :=
+  non_empty_bblock body exit /\ builtin_alone body exit.
+
+Lemma wf_bblock_refl:
+  forall body exit,
+  wf_bblock body exit <-> Is_true (wf_bblockb body exit).
+Proof.
+  intros. split.
+  - intros. inv H. apply non_empty_bblock_refl in H0. apply builtin_alone_refl in H1.
+    apply andb_prop_intro. auto.
+  - intros. apply andb_prop_elim in H. inv H.
+    apply non_empty_bblock_refl in H0. apply builtin_alone_refl in H1.
+    unfold wf_bblock. split; auto.
+Qed.
+
+Ltac bblock_auto_correct := (apply non_empty_bblock_refl; try discriminate; try (left; discriminate); try (right; discriminate)).
+(* Local Obligation Tactic := bblock_auto_correct. *)
+
+Lemma Istrue_proof_irrelevant (b: bool): forall (p1 p2:Is_true b), p1=p2.
+Proof.
+  destruct b; simpl; auto.
+  - destruct p1, p2; auto.
+  - destruct p1.
+Qed.
+
+Lemma bblock_equality bb1 bb2: header bb1=header bb2 -> body bb1 = body bb2 -> exit bb1 = exit bb2 -> bb1 = bb2.
+Proof.
+  destruct bb1 as [h1 b1 e1 c1], bb2 as [h2 b2 e2 c2]; simpl.
+  intros; subst.
+  rewrite (Istrue_proof_irrelevant _ c1 c2).
+  auto.
+Qed.
+
+Program Definition bblock_single_inst (i: instruction) :=
+  match i with
+  | PBasic b => {| header:=nil; body:=(b::nil); exit:=None |}
+  | PControl ctl => {| header:=nil; body:=nil; exit:=(Some ctl) |}
+  end.
+Next Obligation.
+  apply wf_bblock_refl. constructor.
+    right. discriminate.
+    constructor.
+Qed.
+
+Lemma length_nonil {A: Type} : forall l:(list A), l <> nil -> (length l > 0)%nat.
+Proof.
+  intros. destruct l; try (contradict H; auto; fail).
+  simpl. omega.
+Qed.
+
+Lemma to_nat_pos : forall z:Z, (Z.to_nat z > 0)%nat -> z > 0.
+Proof.
+  intros. destruct z; auto.
+  - contradict H. simpl. apply gt_irrefl.
+  - apply Zgt_pos_0.
+  - contradict H. simpl. apply gt_irrefl.
+Qed.
+
+Lemma size_positive (b:bblock): size b > 0.
+Proof.
+  unfold size. destruct b as [hd bdy ex cor]. simpl.
+  destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; simpl; omega).
+  inversion cor; contradict H; simpl; auto.
+Qed.
+
+
+Program Definition no_header (bb : bblock) := {| header := nil; body := body bb; exit := exit bb |}.
+Next Obligation.
+  destruct bb; simpl. assumption.
+Defined.
+
+Lemma no_header_size:
+  forall bb, size (no_header bb) = size bb.
+Proof.
+  intros. destruct bb as [hd bdy ex COR]. unfold no_header. simpl. reflexivity.
+Qed.
+
+Program Definition stick_header (h : list label) (bb : bblock) := {| header := h; body := body bb; exit := exit bb |}.
+Next Obligation.
+  destruct bb; simpl. assumption.
+Defined.
+
+Lemma stick_header_size:
+  forall h bb, size (stick_header h bb) = size bb.
+Proof.
+  intros. destruct bb. unfold stick_header. simpl. reflexivity.
+Qed.
+
+Lemma stick_header_no_header:
+  forall bb, stick_header (header bb) (no_header bb) = bb.
+Proof.
+  intros. destruct bb as [hd bdy ex COR]. simpl. unfold no_header; unfold stick_header; simpl. reflexivity.
+Qed.
+
+
+
+
+(** * Sequential Semantics of basic blocks *)
 Section RELSEM.
 
 (** Execution of arith instructions *)
 
 Variable ge: genv.
 
-
+(* TODO: delete this or define it as [parexec_arith_instr ge ai rs rs] *)
 Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   match ai with
   | PArithR n d => rs#d <- (arith_eval_r ge n)
@@ -68,7 +289,7 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
 
 (** Auxiliaries for memory accesses *)
 
-
+(* TODO: delete this or define it as [parexec_load_offset ge chunk rs rs m m d a ofs] *)
 Definition exec_load_offset (chunk: memory_chunk) (rs: regset) (m: mem) (d a: ireg) (ofs: offset) :=
   match (eval_offset ge ofs) with
   | OK ptr => match Mem.loadv chunk m (Val.offset_ptr (rs a) ptr) with
@@ -78,12 +299,14 @@ Definition exec_load_offset (chunk: memory_chunk) (rs: regset) (m: mem) (d a: ir
   | _ => Stuck
   end.
 
+(* TODO: delete this or define it as [parexec_load_reg ge chunk rs rs m m d a ro] *)
 Definition exec_load_reg (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: ireg) :=
   match Mem.loadv chunk m (Val.addl (rs a) (rs ro)) with
   | None => Stuck
   | Some v => Next (rs#d <- v) m
   end.
 
+(* TODO: delete this as define it as ... *)
 Definition exec_store_offset (chunk: memory_chunk) (rs: regset) (m: mem) (s a: ireg) (ofs: offset) :=
   match (eval_offset ge ofs) with
   | OK ptr => match Mem.storev chunk m (Val.offset_ptr (rs a) ptr) (rs s) with
@@ -93,6 +316,7 @@ Definition exec_store_offset (chunk: memory_chunk) (rs: regset) (m: mem) (s a: i
   | _ => Stuck
   end.
 
+(* TODO: delete this as define it as ... *)
 Definition exec_store_reg (chunk: memory_chunk) (rs: regset) (m: mem) (s a ro: ireg) :=
   match Mem.storev chunk m (Val.addl (rs a) (rs ro)) (rs s) with
   | None => Stuck
@@ -103,6 +327,7 @@ Definition exec_store_reg (chunk: memory_chunk) (rs: regset) (m: mem) (s a ro: i
 
 (** * basic instructions *)
 
+(* TODO: define this [parexec_basic_instr ge bi rs rs m m] *)
 Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome :=
   match bi with
   | PArith ai => Next (exec_arith_instr ai rs) m
@@ -157,12 +382,9 @@ Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome :=
      end
   end.
 
+(** * control-flow instructions *)
 
-
-(** Position corresponding to a label *)
-
-
-
+(* TODO: delete this or define it as [par_goto_label ge f lbl rs rs m] *)
 Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) : outcome :=
   match label_pos lbl 0 (fn_blocks f) with
   | None => Stuck
@@ -173,11 +395,7 @@ Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) : outcome
       end
   end.
 
-(** Evaluating a branch 
-
-Warning: in m PC is assumed to be already pointing on the next instruction !
-
-*)
+(* TODO: delete this or define it as [par_eval_branch ge f l rs rs m res] *)
 Definition eval_branch (f: function) (l: label) (rs: regset) (m: mem) (res: option bool) : outcome :=
   match res with
     | Some true  => goto_label f l rs m
@@ -185,23 +403,7 @@ Definition eval_branch (f: function) (l: label) (rs: regset) (m: mem) (res: opti
     | None => Stuck
   end.
 
-
-(** Execution of a single control-flow instruction [i] in initial state [rs] and
-    [m].  Return updated state.
-
-    As above: PC is assumed to be incremented on the next block before the control-flow instruction
-
-    For instructions that correspond tobuiltin
-    actual RISC-V instructions, the cases are straightforward
-    transliterations of the informal descriptions given in the RISC-V
-    user-mode specification.  For pseudo-instructions, refer to the
-    informal descriptions given above.
-
-    Note that we set to [Vundef] the registers used as temporaries by
-    the expansions of the pseudo-instructions, so that the RISC-V code
-    we generate cannot use those registers to hold values that must
-    survive the execution of the pseudo-instruction. *)
-
+(* TODO: delete this or define it as [parexec_control ge f oc rs rs m] *)
 Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem) : outcome :=
   match oc with
   | Some ic =>
@@ -252,32 +454,30 @@ Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem)
   | None => Next rs m
 end.
 
+(* TODO: change [exec_bblock] for a definition like this one: 
+
+Definition exec_exit (f: function) ext size_b (rs: regset) (m: mem) 
+  := parexec_exit ge f ext size_b rs rs m.
+
 Definition exec_bblock (f: function) (b: bblock) (rs0: regset) (m: mem) : outcome :=
   match exec_body (body b) rs0 m with
-  | Next rs' m' =>
-    let rs1 := nextblock b rs' in exec_control f (exit b) rs1 m'
+  | Next rs' m' => exec_exit f (exit b) (Ptrofs.repr (size b)) rs' m'
   | Stuck => Stuck
   end.
 
-(** Translation of the LTL/Linear/Mach view of machine registers to
-  the RISC-V view.  Note that no LTL register maps to [X31].  This
-  register is reserved as temporary, to be used by the generated RV32G
-  code.  *)
-
-
-
-
+*)
 
+Definition exec_bblock (f: function) (b: bblock) (rs0: regset) (m: mem) : outcome :=
+  match exec_body (body b) rs0 m with
+  | Next rs' m' =>
+    let rs1 := nextblock b rs' in exec_control f (exit b) rs1 m'
+  | Stuck => Stuck
+  end.
 
 
 (** Execution of the instruction at [rs PC]. *)
 
 
-(** TODO
- * For now, we consider a builtin is alone in a basic block.
- * Perhaps there is a way to avoid that ?
- *)
-
 Inductive step: state -> trace -> state -> Prop :=
   | exec_step_internal:
       forall b ofs f bi rs m rs' m',
@@ -318,68 +518,6 @@ End RELSEM.
 Definition semantics (p: program) :=
   Semantics step (initial_state p) final_state (Genv.globalenv p).
 
-(* Useless
-
-Remark extcall_arguments_determ:
-  forall rs m sg args1 args2,
-  extcall_arguments rs m sg args1 -> extcall_arguments rs m sg args2 -> args1 = args2.
-Proof.
-  intros until m.
-  assert (A: forall l v1 v2,
-             extcall_arg rs m l v1 -> extcall_arg rs m l v2 -> v1 = v2).
-  { intros. inv H; inv H0; congruence. }
-  assert (B: forall p v1 v2,
-             extcall_arg_pair rs m p v1 -> extcall_arg_pair rs m p v2 -> v1 = v2).
-  { intros. inv H; inv H0. 
-    eapply A; eauto.
-    f_equal; eapply A; eauto. }
-  assert (C: forall ll vl1, list_forall2 (extcall_arg_pair rs m) ll vl1 ->
-             forall vl2, list_forall2 (extcall_arg_pair rs m) ll vl2 -> vl1 = vl2).
-  {
-    induction 1; intros vl2 EA; inv EA.
-    auto.
-    f_equal; eauto. }
-  intros. eapply C; eauto.
-Qed.
-
-Lemma semantics_determinate: forall p, determinate (semantics p).
-Proof.
-Ltac Equalities :=
-  match goal with
-  | [ H1: ?a = ?b, H2: ?a = ?c |- _ ] =>
-      rewrite H1 in H2; inv H2; Equalities
-  | _ => idtac
-  end.
-  intros; constructor; simpl; intros.
-- (* determ *)
-  inv H; inv H0; Equalities.
-  + split. constructor. auto.
-  + unfold exec_bblock in H4. destruct (exec_body _ _ _ _); try discriminate.
-    rewrite H9 in H4. discriminate.
-  + unfold exec_bblock in H13. destruct (exec_body _ _ _ _); try discriminate.
-    rewrite H4 in H13. discriminate.
-  + assert (vargs0 = vargs) by (eapply eval_builtin_args_determ; eauto). subst vargs0.
-    exploit external_call_determ. eexact H6. eexact H13. intros [A B].
-    split. auto. intros. destruct B; auto. subst. auto.
-  + assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0.
-    exploit external_call_determ. eexact H3. eexact H8. intros [A B].
-    split. auto. intros. destruct B; auto. subst. auto.
-- (* trace length *)
-  red; intros. inv H; simpl.
-  omega.
-  eapply external_call_trace_length; eauto.
-  eapply external_call_trace_length; eauto.
-- (* initial states *)
-  inv H; inv H0. f_equal. congruence.
-- (* final no step *)
-  assert (NOTNULL: forall b ofs, Vnullptr <> Vptr b ofs).
-  { intros; unfold Vnullptr; destruct Archi.ptr64; congruence. }
-  inv H. unfold Vzero in H0. red; intros; red; intros.
-  inv H; rewrite H0 in *; eelim NOTNULL; eauto.
-- (* final states *)
-  inv H; inv H0. congruence.
-Qed.
-*)
 
 Definition data_preg (r: preg) : bool :=
   match r with
@@ -390,65 +528,3 @@ Definition data_preg (r: preg) : bool :=
   | PC     => false
   end.
 
-(** Determinacy of the [Asm] semantics. *)
-
-(* Useless.
-
-Remark extcall_arguments_determ:
-  forall rs m sg args1 args2,
-  extcall_arguments rs m sg args1 -> extcall_arguments rs m sg args2 -> args1 = args2.
-Proof.
-  intros until m.
-  assert (A: forall l v1 v2,
-             extcall_arg rs m l v1 -> extcall_arg rs m l v2 -> v1 = v2).
-  { intros. inv H; inv H0; congruence. }
-  assert (B: forall p v1 v2,
-             extcall_arg_pair rs m p v1 -> extcall_arg_pair rs m p v2 -> v1 = v2).
-  { intros. inv H; inv H0. 
-    eapply A; eauto.
-    f_equal; eapply A; eauto. }
-  assert (C: forall ll vl1, list_forall2 (extcall_arg_pair rs m) ll vl1 ->
-             forall vl2, list_forall2 (extcall_arg_pair rs m) ll vl2 -> vl1 = vl2).
-  {
-    induction 1; intros vl2 EA; inv EA.
-    auto.
-    f_equal; eauto. }
-  intros. eapply C; eauto.
-Qed.
-
-Lemma semantics_determinate: forall p, determinate (semantics p).
-Proof.
-Ltac Equalities :=
-  match goal with
-  | [ H1: ?a = ?b, H2: ?a = ?c |- _ ] =>
-      rewrite H1 in H2; inv H2; Equalities
-  | _ => idtac
-  end.
-  intros; constructor; simpl; intros.
-- (* determ *)
-  inv H; inv H0; Equalities.
-  split. constructor. auto.
-  discriminate.
-  discriminate.
-  assert (vargs0 = vargs) by (eapply eval_builtin_args_determ; eauto). subst vargs0.
-  exploit external_call_determ. eexact H5. eexact H11. intros [A B].
-  split. auto. intros. destruct B; auto. subst. auto.
-  assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0.
-  exploit external_call_determ. eexact H3. eexact H8. intros [A B].
-  split. auto. intros. destruct B; auto. subst. auto.
-- (* trace length *)
-  red; intros. inv H; simpl.
-  omega.
-  eapply external_call_trace_length; eauto.
-  eapply external_call_trace_length; eauto.
-- (* initial states *)
-  inv H; inv H0. f_equal. congruence.
-- (* final no step *)
-  assert (NOTNULL: forall b ofs, Vnullptr <> Vptr b ofs).
-  { intros; unfold Vnullptr; destruct Archi.ptr64; congruence. }
-  inv H. unfold Vzero in H0. red; intros; red; intros.
-  inv H; rewrite H0 in *; eelim NOTNULL; eauto.
-- (* final states *)
-  inv H; inv H0. congruence.
-Qed.
-*)
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 32e5e5bb..01f5ca20 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -910,7 +910,7 @@ Theorem forward_simu_control_gen ge fn ex b rs m s:
 Proof.
   intros. destruct ex; simpl; inv H0.
   - destruct c; destruct i; simpl; rewrite (H2 PC); auto.
-    all: try (eexists; split; try split; Simpl; intros rr; destruct rr; unfold nextblock; Simpl).
+    all: try (eexists; split; try split; Simpl; intros rr; destruct rr; unfold nextblock, incrPC; Simpl).
 
     (* Pjumptable *)
     + Simpl. rewrite (H2 r). destruct (rs r); simpl; auto. destruct (list_nth_z _ _); simpl; auto.
@@ -922,18 +922,18 @@ Proof.
 
     (* Pj_l *)
     + Simpl. unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto.
-      unfold nextblock. Simpl. destruct (Val.offset_ptr _ _); simpl; auto.
+      unfold nextblock, incrPC. Simpl. destruct (Val.offset_ptr _ _); simpl; auto.
       eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
 
     (* Pcb *)
     + Simpl. destruct (cmp_for_btest _); simpl; auto. rewrite (H2 r). destruct o; simpl; auto. destruct i; unfold eval_branch; unfold eval_branch_deps.
       ++ destruct (Val.cmp_bool _ _ _); simpl; auto. destruct b0.
-         +++ unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock; Simpl.
+         +++ unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock, incrPC; Simpl.
              destruct (Val.offset_ptr _ _); simpl; auto.
              eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
          +++ simpl. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
       ++ destruct (Val.cmpl_bool _ _ _); simpl; auto. destruct b0.
-         +++ unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock; Simpl.
+         +++ unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock, incrPC; Simpl.
              destruct (Val.offset_ptr _ _); simpl; auto.
              eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
          +++ simpl. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
@@ -941,12 +941,12 @@ Proof.
     (* Pcbu *)
     + Simpl. destruct (cmpu_for_btest _); simpl; auto. rewrite (H2 r). destruct o; simpl; auto. destruct i; unfold eval_branch; unfold eval_branch_deps.
       ++ destruct (Val_cmpu_bool _ _ _); simpl; auto. destruct b0.
-         +++ unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock; Simpl.
+         +++ unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock, incrPC; Simpl.
              destruct (Val.offset_ptr _ _); simpl; auto.
              eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
          +++ simpl. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
       ++ destruct (Val_cmplu_bool _ _ _); simpl; auto. destruct b0.
-         +++ unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock; Simpl.
+         +++ unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock, incrPC; Simpl.
              destruct (Val.offset_ptr _ _); simpl; auto.
              eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
          +++ simpl. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
@@ -1813,31 +1813,31 @@ Theorem forward_simu_par_control_gen ge fn rsr rsw mr mw sr sw sz ex:
   Ge = Genv ge fn ->
   match_states (State rsr mr) sr ->
   match_states (State rsw mw) sw ->
-  match_outcome (parexec_control ge fn ex (par_nextblock (Ptrofs.repr sz) rsr) rsw mw) (inst_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr).
+  match_outcome (parexec_control ge fn ex (incrPC (Ptrofs.repr sz) rsr) rsw mw) (inst_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr).
 Proof.
   intros GENV MSR MSW.
   simpl in *. inv MSR. inv MSW.
   destruct ex.
   - destruct c; destruct i; try discriminate; simpl.
-    all: try (rewrite (H0 PC); eexists; split; try split; Simpl; intros rr; destruct rr; unfold par_nextblock; Simpl).
+    all: try (rewrite (H0 PC); eexists; split; try split; Simpl; intros rr; destruct rr; unfold incrPC; Simpl).
 
     (* Pjumptable *)
-    + rewrite (H0 PC). Simpl. rewrite (H0 r). unfold par_nextblock. Simpl.
+    + rewrite (H0 PC). Simpl. rewrite (H0 r). unfold incrPC. Simpl.
       destruct (rsr r); simpl; auto. destruct (list_nth_z _ _); simpl; auto.
       unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl.
       destruct (Val.offset_ptr _ _); simpl; auto.
-      eexists; split; try split; Simpl. intros rr; destruct rr; unfold par_nextblock; Simpl.
+      eexists; split; try split; Simpl. intros rr; destruct rr; unfold incrPC; Simpl.
       destruct (preg_eq g GPR62). rewrite e. Simpl.
       destruct (preg_eq g GPR63). rewrite e. Simpl. Simpl.
 
     (* Pj_l *)
     + rewrite (H0 PC). Simpl. unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto.
-      unfold par_nextblock. Simpl. destruct (Val.offset_ptr _ _); simpl; auto.
-      eexists; split; try split; Simpl. intros rr; destruct rr; unfold par_nextblock; Simpl.
+      unfold incrPC. Simpl. destruct (Val.offset_ptr _ _); simpl; auto.
+      eexists; split; try split; Simpl. intros rr; destruct rr; unfold incrPC; Simpl.
 
     (* Pcb *)
     + rewrite (H0 PC). Simpl. rewrite (H0 r). destruct (cmp_for_btest _); simpl; auto. destruct o; simpl; auto.
-      unfold par_eval_branch. unfold eval_branch_deps. unfold par_nextblock. Simpl. destruct i.
+      unfold par_eval_branch. unfold eval_branch_deps. unfold incrPC. Simpl. destruct i.
       ++ destruct (Val.cmp_bool _ _ _); simpl; auto. destruct b.
          +++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl.
              destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl.
@@ -1851,7 +1851,7 @@ Proof.
 
     (* Pcbu *)
     + rewrite (H0 PC). Simpl. rewrite (H0 r). destruct (cmpu_for_btest _); simpl; auto. destruct o; simpl; auto.
-      unfold par_eval_branch. unfold eval_branch_deps. unfold par_nextblock. Simpl. destruct i.
+      unfold par_eval_branch. unfold eval_branch_deps. unfold incrPC. Simpl. destruct i.
       ++ destruct (Val_cmpu_bool _ _ _); simpl; auto. destruct b.
          +++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl.
              destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl.
@@ -1864,14 +1864,14 @@ Proof.
          +++ repeat (econstructor; eauto). intros rr; destruct rr; Simpl.
 
   - simpl in *. rewrite (H0 PC). eexists; split; try split; Simpl.
-    intros rr; destruct rr; unfold par_nextblock; Simpl.
+    intros rr; destruct rr; unfold incrPC; Simpl.
 Qed.
 
 Theorem forward_simu_par_control ge fn rsr rsw mr mw sr sw sz rs' ex m':
   Ge = Genv ge fn ->
   match_states (State rsr mr) sr ->
   match_states (State rsw mw) sw ->
-  parexec_control ge fn ex (par_nextblock (Ptrofs.repr sz) rsr) rsw mw = Next rs' m' ->
+  parexec_control ge fn ex (incrPC (Ptrofs.repr sz) rsr) rsw mw = Next rs' m' ->
   exists s',
      inst_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr = Some s'
   /\ match_states (State rs' m') s'.
@@ -1885,7 +1885,7 @@ Lemma forward_simu_par_control_Stuck ge fn rsr rsw mr mw sr sw sz ex:
   Ge = Genv ge fn ->
   match_states (State rsr mr) sr ->
   match_states (State rsw mw) sw ->
-  parexec_control ge fn ex (par_nextblock (Ptrofs.repr sz) rsr) rsw mw = Stuck ->
+  parexec_control ge fn ex (incrPC (Ptrofs.repr sz) rsr) rsw mw = Stuck ->
   inst_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr = None.
 Proof.
   intros. exploit forward_simu_par_control_gen. 3: eapply H1. 2: eapply H0. all: eauto. 
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index a071a9f8..d93afba5 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -839,7 +839,7 @@ Proof.
       exploit find_label_goto_label.

         eauto. eauto.

         instantiate (2 := rs2').

-        { subst. unfold nextblock. Simpl. unfold Val.offset_ptr. rewrite PCeq. eauto. }

+        { subst. unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq. eauto. }

         eauto.

       intros (tc' & rs' & GOTO & AT2 & INV).

 

@@ -847,7 +847,7 @@ Proof.
         rewrite H6. simpl extract_basic. simpl. eauto.

         rewrite H7. simpl extract_ctl. simpl. rewrite <- Heqrs2'. eauto.

       econstructor; eauto.

-        rewrite Heqrs2' in INV. unfold nextblock in INV.

+        rewrite Heqrs2' in INV. unfold nextblock, incrPC in INV.

         eapply agree_exten; eauto with asmgen.

         assert (forall r : preg, r <> PC -> rs' r = rs2 r).

         { intros. destruct r.

@@ -886,7 +886,7 @@ Proof.
         econstructor; eauto.

           eapply agree_exten with rs2; eauto with asmgen.

           { intros. destruct r; try destruct g; try discriminate.

-            all: rewrite Hrs3; try discriminate; unfold nextblock; Simpl. }

+            all: rewrite Hrs3; try discriminate; unfold nextblock, incrPC; Simpl. }

         intros. discriminate.

 

       * (* MBcond false *)

@@ -912,10 +912,10 @@ Proof.
           rewrite H7. rewrite <- BTC. rewrite extract_ctl_basics_to_code. simpl extract_ctl. rewrite B. eauto.

 

         econstructor; eauto.

-          unfold nextblock. Simpl. unfold Val.offset_ptr. rewrite PCeq. econstructor; eauto.

+          unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq. econstructor; eauto.

           eapply agree_exten with rs2; eauto with asmgen.

           { intros. destruct r; try destruct g; try discriminate.

-            all: rewrite <- C; try discriminate; unfold nextblock; Simpl. }

+            all: rewrite <- C; try discriminate; unfold nextblock, incrPC; Simpl. }

         intros. discriminate.

     + (* MBjumptable *)

       destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.

@@ -926,7 +926,7 @@ Proof.
       generalize (transf_function_no_overflow _ _ TRANSF0); intro NOOV.

       assert (f1 = f) by congruence. subst f1.

       exploit find_label_goto_label. 4: eapply H16. 1-2: eauto. instantiate (2 := (nextblock tbb rs2) # GPR62 <- Vundef # GPR63 <- Vundef).

-        unfold nextblock. Simpl. unfold Val.offset_ptr. rewrite PCeq. reflexivity.

+        unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq. reflexivity.

       exploit functions_transl. eapply FIND0. eapply TRANSF0. intros FIND3. assert (fn = tf) by congruence. subst fn.

 

       intros [tc' [rs' [A [B C]]]].

@@ -959,7 +959,7 @@ Proof.
         rewrite H6. simpl extract_basic. eauto.

         rewrite H7. simpl extract_ctl. simpl. reflexivity.

       econstructor; eauto.

-        unfold nextblock. repeat apply agree_set_other; auto with asmgen.

+        unfold nextblock, incrPC. repeat apply agree_set_other; auto with asmgen.

 

   - inv MCS. inv MAS. simpl in *. subst. inv Hpstate. inv Hcur.

 (*     exploit transl_blocks_distrib; eauto. (* rewrite <- H2. discriminate. *)

@@ -969,7 +969,7 @@ Proof.
     monadInv TBC. monadInv TIC. simpl in *. rewrite H5. rewrite H6.

     simpl. repeat eexists.

     econstructor. 4: instantiate (3 := false). all:eauto.

-      unfold nextblock. Simpl. unfold Val.offset_ptr. rewrite PCeq.

+      unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq.

       assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned).

         eapply transf_function_no_overflow; eauto.

       assert (f = f0) by congruence. subst f0. econstructor; eauto.

@@ -1398,7 +1398,7 @@ Proof.
     eapply exec_step_internal; eauto. eapply find_bblock_tail; eauto.

     unfold exec_bblock. simpl. eauto.

     econstructor. eauto. eauto. eauto.

-    unfold nextblock. Simpl. unfold Val.offset_ptr. rewrite <- H.

+    unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite <- H.

     assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned).

       eapply transf_function_no_overflow; eauto.

     econstructor; eauto.

@@ -1581,7 +1581,7 @@ Proof.
     eauto.

   econstructor; eauto.

     instantiate (2 := tf); instantiate (1 := x0).

-    unfold nextblock. rewrite Pregmap.gss.

+    unfold nextblock, incrPC. rewrite Pregmap.gss.

     rewrite set_res_other. rewrite undef_regs_other_2. rewrite Pregmap.gso by congruence. 

     rewrite <- H. simpl. econstructor; eauto.

     eapply code_tail_next_int; eauto.

diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 5ccea246..a43b228e 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -745,7 +745,7 @@ Proof.
     * constructor.
     * split; auto. simpl. intros.
       assert (rs r1 = (nextblock tbb rs) r1).
-        unfold nextblock. Simpl. rewrite H1 in H0.
+        unfold nextblock, incrPC. Simpl. rewrite H1 in H0.
       (*assert (Val.cmp_bool Ceq (rs r1) (Vint (Int.repr 0)) = Some b) as EVAL'S.
       { rewrite <- H2. rewrite <- H0. rewrite <- H1. auto. }*)
       auto;
@@ -772,7 +772,7 @@ Proof.
     * constructor.
     * split; auto. simpl. intros.
       assert (rs r1 = (nextblock tbb rs) r1).
-        unfold nextblock. Simpl. rewrite H1 in H0.
+        unfold nextblock, incrPC. Simpl. rewrite H1 in H0.
       auto;
       unfold eval_branch. rewrite H0. auto.
   - (* c = Clt *) contradict H; unfold select_comp; destruct (Int.eq n Int.zero);
@@ -821,7 +821,7 @@ Proof.
     * constructor.
     * split; auto. simpl. intros.
       assert (rs r1 = (nextblock tbb rs) r1).
-        unfold nextblock. Simpl. rewrite H1 in H0.
+        unfold nextblock, incrPC. Simpl. rewrite H1 in H0.
       auto;
       unfold eval_branch. rewrite H0; auto.
   - (* c = Cne *)
@@ -846,7 +846,7 @@ Proof.
     * constructor.
     * split; auto. simpl. intros.
       assert (rs r1 = (nextblock tbb rs) r1).
-        unfold nextblock. Simpl. rewrite H1 in H0.
+        unfold nextblock, incrPC. Simpl. rewrite H1 in H0.
       auto;
       unfold eval_branch. rewrite H0; auto.
   - (* c = Clt *) contradict H; unfold select_compl; destruct (Int64.eq n Int64.zero);
@@ -903,7 +903,7 @@ Proof.
     * constructor.
     * split; auto.
       assert (rs x = (nextblock tbb rs) x).
-        unfold nextblock. Simpl. rewrite H0 in EVAL'. clear H0.
+        unfold nextblock, incrPC. Simpl. rewrite H0 in EVAL'. clear H0.
       destruct c0; simpl; auto;
       unfold eval_branch; rewrite <- H; rewrite EVAL'; auto.
   + exploit (loadimm32_correct RTMP n); eauto. intros (rs' & A & B & C).
@@ -966,7 +966,7 @@ Proof.
     * constructor.
     * split; auto.
       assert (rs x = (nextblock tbb rs) x).
-        unfold nextblock. Simpl. rewrite H0 in EVAL'. clear H0.
+        unfold nextblock, incrPC. Simpl. rewrite H0 in EVAL'. clear H0.
       destruct c0; simpl; auto;
       unfold eval_branch; rewrite <- H; rewrite EVAL'; auto.
   + exploit (loadimm64_correct RTMP n); eauto. intros (rs' & A & B & C).
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index d56a7a84..6c18ac32 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -15,7 +15,9 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** Abstract syntax and semantics for K1c assembly language. *)
+(** Abstract syntax and semantics for VLIW semantics of K1c assembly language. *)
+
+(* FIXME: develop/fix the comments in this file *)
 
 Require Import Coqlib.
 Require Import Maps.
@@ -35,6 +37,12 @@ Require Import Sorting.Permutation.
 
 (** * Abstract syntax *)
 
+(** A K1c program is syntactically given as a list of functions. 
+    Each function is associated to a list of bundles of type [bblock] below.
+    Hence, syntactically, we view each bundle as a basic block:
+    this view induces our sequential semantics of bundles defined in [Asmblock].
+*)
+
 (** General Purpose registers.
 *)
 
@@ -481,21 +489,7 @@ Coercion PExpand:   ex_instruction >-> control.
 Coercion PCtlFlow:  cf_instruction >-> control.
 
 
-(** * Definition of a bblock *)
-
-Ltac exploreInst :=
-  repeat match goal with
-  | [ H : match ?var with | _ => _ end = _ |- _ ] => destruct var
-  | [ H : OK _ = OK _ |- _ ] => monadInv H
-  | [ |- context[if ?b then _ else _] ] => destruct b
-  | [ |- context[match ?m with | _ => _ end] ] => destruct m
-  | [ |- context[match ?m as _ return _ with | _ => _ end]] => destruct m
-  | [ H : bind _ _ = OK _ |- _ ] => monadInv H
-  | [ H : Error _ = OK _ |- _ ] => inversion H
-  end.
-
-Definition non_empty_bblock (body: list basic) (exit: option control): Prop
- := body <> nil \/ exit <> None.
+(** * Definition of a bblock (ie a bundle) *)
 
 Definition non_empty_body (body: list basic): bool :=
   match body with
@@ -511,23 +505,11 @@ Definition non_empty_exit (exit: option control): bool :=
 
 Definition non_empty_bblockb (body: list basic) (exit: option control): bool := non_empty_body body || non_empty_exit exit.
 
-Lemma non_empty_bblock_refl:
-  forall body exit,
-  non_empty_bblock body exit <->
-  Is_true (non_empty_bblockb body exit).
-Proof.
-  intros. split.
-  - destruct body; destruct exit.
-    all: simpl; auto. intros. inversion H; contradiction.
-  - destruct body; destruct exit.
-    all: simpl; auto.
-    all: intros; try (right; discriminate); try (left; discriminate).
-    contradiction.
-Qed.
-
-Definition builtin_alone (body: list basic) (exit: option control) := forall ef args res,
-  exit = Some (PExpand (Pbuiltin ef args res)) -> body = nil.
 
+(** TODO
+ * For now, we consider a builtin is alone in a bundle (and a basic block).
+ * Is there a way to avoid that ?
+ *)
 Definition builtin_aloneb (body: list basic) (exit: option control) :=
   match exit with
   | Some (PExpand (Pbuiltin _ _ _)) =>
@@ -538,41 +520,9 @@ Definition builtin_aloneb (body: list basic) (exit: option control) :=
   | _ => true
   end.
 
-Lemma builtin_alone_refl:
-  forall body exit,
-  builtin_alone body exit <-> Is_true (builtin_aloneb body exit).
-Proof.
-  intros. split.
-  - destruct body; destruct exit.
-    all: simpl; auto.
-    all: exploreInst; simpl; auto.
-    unfold builtin_alone. intros. assert (Some (Pbuiltin e l b0) = Some (Pbuiltin e l b0)); auto.
-    assert (b :: body = nil). eapply H; eauto. discriminate.
-  - destruct body; destruct exit.
-    all: simpl; auto; try constructor.
-    + exploreInst; try discriminate.
-        simpl. contradiction.
-    + intros. discriminate.
-Qed.
-
 Definition wf_bblockb (body: list basic) (exit: option control) :=
   (non_empty_bblockb body exit) && (builtin_aloneb body exit).
 
-Definition wf_bblock (body: list basic) (exit: option control) :=
-  non_empty_bblock body exit /\ builtin_alone body exit.
-
-Lemma wf_bblock_refl:
-  forall body exit,
-  wf_bblock body exit <-> Is_true (wf_bblockb body exit).
-Proof.
-  intros. split.
-  - intros. inv H. apply non_empty_bblock_refl in H0. apply builtin_alone_refl in H1.
-    apply andb_prop_intro. auto.
-  - intros. apply andb_prop_elim in H. inv H.
-    apply non_empty_bblock_refl in H0. apply builtin_alone_refl in H1.
-    unfold wf_bblock. split; auto.
-Qed.
-
 (** A bblock is well-formed if he contains at least one instruction,
     and if there is a builtin then it must be alone in this bblock. *)
 
@@ -583,26 +533,7 @@ Record bblock := mk_bblock {
   correct: Is_true (wf_bblockb body exit)
 }.
 
-Ltac bblock_auto_correct := (apply non_empty_bblock_refl; try discriminate; try (left; discriminate); try (right; discriminate)).
-(* Local Obligation Tactic := bblock_auto_correct. *)
-
-Lemma Istrue_proof_irrelevant (b: bool): forall (p1 p2:Is_true b), p1=p2.
-Proof.
-  destruct b; simpl; auto.
-  - destruct p1, p2; auto.
-  - destruct p1.
-Qed.
-
-Lemma bblock_equality bb1 bb2: header bb1=header bb2 -> body bb1 = body bb2 -> exit bb1 = exit bb2 -> bb1 = bb2.
-Proof.
-  destruct bb1 as [h1 b1 e1 c1], bb2 as [h2 b2 e2 c2]; simpl.
-  intros; subst.
-  rewrite (Istrue_proof_irrelevant _ c1 c2).
-  auto.
-Qed.
-
-
-(* FIXME: redundant with definition in Machblock *)
+(* FIXME? redundant with definition in Machblock *)
 Definition length_opt {A} (o: option A) : nat :=
   match o with
   | Some o => 1
@@ -614,66 +545,6 @@ Definition length_opt {A} (o: option A) : nat :=
    The result is in Z to be compatible with operations on PC
 *)
 Definition size (b:bblock): Z := Z.of_nat (length (body b) + length_opt (exit b)).
-(*   match (body b, exit b) with
-  | (nil, None) => 1
-  | _ => 
-  end.
- *)
-
-Lemma length_nonil {A: Type} : forall l:(list A), l <> nil -> (length l > 0)%nat.
-Proof.
-  intros. destruct l; try (contradict H; auto; fail).
-  simpl. omega.
-Qed.
-
-Lemma to_nat_pos : forall z:Z, (Z.to_nat z > 0)%nat -> z > 0.
-Proof.
-  intros. destruct z; auto.
-  - contradict H. simpl. apply gt_irrefl.
-  - apply Zgt_pos_0.
-  - contradict H. simpl. apply gt_irrefl.
-Qed.
-
-Lemma size_positive (b:bblock): size b > 0.
-Proof.
-  unfold size. destruct b as [hd bdy ex cor]. simpl.
-  destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; simpl; omega).
-  inversion cor; contradict H; simpl; auto.
-(*     rewrite eq. (* inversion COR. *) (* inversion H. *)
-  - assert ((length b > 0)%nat). apply length_nonil. auto.
-    omega.
-  - destruct e; simpl; try omega. contradict H; simpl; auto.
- *)Qed.
-
-
-Program Definition no_header (bb : bblock) := {| header := nil; body := body bb; exit := exit bb |}.
-Next Obligation.
-  destruct bb; simpl. assumption.
-Defined.
-
-Lemma no_header_size:
-  forall bb, size (no_header bb) = size bb.
-Proof.
-  intros. destruct bb as [hd bdy ex COR]. unfold no_header. simpl. reflexivity.
-Qed.
-
-Program Definition stick_header (h : list label) (bb : bblock) := {| header := h; body := body bb; exit := exit bb |}.
-Next Obligation.
-  destruct bb; simpl. assumption.
-Defined.
-
-Lemma stick_header_size:
-  forall h bb, size (stick_header h bb) = size bb.
-Proof.
-  intros. destruct bb. unfold stick_header. simpl. reflexivity.
-Qed.
-
-Lemma stick_header_no_header:
-  forall bb, stick_header (header bb) (no_header bb) = bb.
-Proof.
-  intros. destruct bb as [hd bdy ex COR]. simpl. unfold no_header; unfold stick_header; simpl. reflexivity.
-Qed.
-
 
 Definition bblocks := list bblock.
 
@@ -689,103 +560,6 @@ Record function : Type := mkfunction { fn_sig: signature; fn_blocks: bblocks }.
 Definition fundef := AST.fundef function.
 Definition program := AST.program fundef unit.
 
-Inductive instruction : Type :=
-  | PBasic    (i: basic)
-  | PControl  (i: control)
-.
-
-Coercion PBasic:    basic >-> instruction.
-Coercion PControl:  control >-> instruction.
-
-Definition code := list instruction.
-Definition bcode := list basic.
-
-Fixpoint basics_to_code (l: list basic) :=
-  match l with
-  | nil => nil
-  | bi::l => (PBasic bi)::(basics_to_code l)
-  end.
-
-Fixpoint code_to_basics (c: code) :=
-  match c with
-  | (PBasic i)::c =>
-    match code_to_basics c with
-    | None => None
-    | Some l => Some (i::l)
-    end
-  | _::c => None
-  | nil => Some nil
-  end.
-
-Lemma code_to_basics_id: forall c, code_to_basics (basics_to_code c) = Some c.
-Proof.
-  intros. induction c as [|i c]; simpl; auto.
-  rewrite IHc. auto.
-Qed.
-
-Lemma code_to_basics_dist:
-  forall c c' l l',
-  code_to_basics c = Some l ->
-  code_to_basics c' = Some l' ->
-  code_to_basics (c ++ c') = Some (l ++ l').
-Proof.
-  induction c as [|i c]; simpl; auto.
-  - intros. inv H. simpl. auto.
-  - intros. destruct i; try discriminate. destruct (code_to_basics c) eqn:CTB; try discriminate.
-    inv H. erewrite IHc; eauto. auto.
-Qed.
-
-(** 
-  Asmblockgen will have to translate a Mach control into a list of instructions of the form
-   i1 :: i2 :: i3 :: ctl :: nil ; where i1..i3 are basic instructions, ctl is a control instruction
-  These functions provide way to extract the basic / control instructions
-*)
-
-Fixpoint extract_basic (c: code) :=
-  match c with
-  | nil => nil
-  | PBasic i :: c => i :: (extract_basic c)
-  | PControl i :: c => nil
-  end.
-
-Fixpoint extract_ctl (c: code) :=
-  match c with
-  | nil => None
-  | PBasic i :: c => extract_ctl c
-  | PControl i :: nil => Some i
-  | PControl i :: _ => None (* if the first found control instruction isn't the last *)
-  end.
-
-(** * Utility for Asmblockgen *)
-
-Program Definition bblock_single_inst (i: instruction) :=
-  match i with
-  | PBasic b => {| header:=nil; body:=(b::nil); exit:=None |}
-  | PControl ctl => {| header:=nil; body:=nil; exit:=(Some ctl) |}
-  end.
-Next Obligation.
-  apply wf_bblock_refl. constructor.
-    right. discriminate.
-    constructor.
-Qed.
-
-(** This definition is not used anymore *)
-(* Program Definition bblock_basic_ctl (c: list basic) (i: option control) :=
-  match i with
-  | Some i => {| header:=nil; body:=c; exit:=Some i |}
-  | None =>
-    match c with
-    | _::_ => {| header:=nil; body:=c; exit:=None |}
-    | nil => {| header:=nil; body:=Pnop::nil; exit:=None |}
-    end
-  end.
-Next Obligation.
-  bblock_auto_correct.
-Qed. Next Obligation.
-  bblock_auto_correct.
-Qed. *)
-
-
 (** * Operational semantics *)
 
 (** The semantics operates over a single mapping from registers
@@ -841,6 +615,8 @@ Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
 
 Local Open Scope asm.
 
+(** * Parallel Semantics of bundles *)
+
 Section RELSEM.
 
 (** Execution of arith instructions *)
@@ -855,10 +631,8 @@ Variable ge: genv.
 
 Inductive outcome: Type :=
   | Next (rs:regset) (m:mem)
-  | Stuck.
-(* Arguments outcome: clear implicits. *)
-
-
+  | Stuck
+.
 
 (** ** Arithmetic Expressions (including comparisons) *)
 
@@ -1216,22 +990,18 @@ Definition arith_eval_arrr n v1 v2 v3 :=
   match n with
   | Pmaddw => Val.add v1 (Val.mul v2 v3)
   | Pmaddl => Val.addl v1 (Val.mull v2 v3)
-  end.                    
+  end.
 
 Definition arith_eval_arri32 n v1 v2 v3 :=
   match n with
   | Pmaddiw => Val.add v1 (Val.mul v2 (Vint v3))
-  end.                    
+  end.
 
 Definition arith_eval_arri64 n v1 v2 v3 :=
   match n with
   | Pmaddil => Val.addl v1 (Val.mull v2 (Vlong v3))
-  end.                    
+  end.
 
-(* TODO: on pourrait mettre ça dans Asmblock pour factoriser le code
-   en définissant 
-    exec_arith_instr ai rs := parexec_arith_instr ai rs rs
-*)
 Definition parexec_arith_instr (ai: ar_instruction) (rsr rsw: regset): regset :=
   match ai with
   | PArithR n d => rsw#d <- (arith_eval_r n)
@@ -1264,7 +1034,6 @@ Definition eval_offset (ofs: offset) : res ptrofs :=
 
 (** * load/store *)
 
-(* TODO: factoriser ? *)
 Definition parexec_load_offset (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a: ireg) (ofs: offset) :=
   match (eval_offset ofs) with
   | OK ptr => match Mem.loadv chunk mr (Val.offset_ptr (rsr a) ptr) with
@@ -1321,11 +1090,8 @@ Definition store_chunk n :=
   | Pfsd => Mfloat64
   end.
 
-(* rem: parexec_store = exec_store *)
-
 (** * basic instructions *)
 
-(* TODO: factoriser ? *)
 Definition parexec_basic_instr (bi: basic) (rsr rsw: regset) (mr mw: mem) :=
   match bi with
   | PArith ai => Next (parexec_arith_instr ai rsr rsw) mw
@@ -1381,15 +1147,7 @@ Fixpoint parexec_wio_body (body: list basic) (rsr rsw: regset) (mr mw: mem) :=
      end
   end.
 
-(** Manipulations over the [PC] register: continuing with the next
-  instruction ([nextblock]) or branching to a label ([goto_label]). *)
-
-(* TODO: factoriser ? *)
-Definition par_nextblock size_b (rs: regset) :=
-  rs#PC <- (Val.offset_ptr rs#PC size_b).
-
-
-(** TODO: redundant w.r.t Machblock *)
+(** TODO: redundant w.r.t Machblock ?? *)
 Lemma in_dec (lbl: label) (l: list label):  { List.In lbl l } + { ~(List.In lbl l) }.
 Proof.
   apply List.in_dec.
@@ -1423,7 +1181,6 @@ Fixpoint label_pos (lbl: label) (pos: Z) (lb: bblocks) {struct lb} : option Z :=
   | b :: lb' => if is_label lbl b then Some pos else label_pos lbl (pos + (size b)) lb'
   end.
 
-(* TODO: factoriser ? *)
 Definition par_goto_label (f: function) (lbl: label) (rsr rsw: regset) (mw: mem) :=
   match label_pos lbl 0 (fn_blocks f) with
   | None => Stuck
@@ -1439,7 +1196,7 @@ Definition par_goto_label (f: function) (lbl: label) (rsr rsw: regset) (mw: mem)
 Warning: in m PC is assumed to be already pointing on the next instruction !
 
 *)
-(* TODO: factoriser ? *)
+
 Definition par_eval_branch (f: function) (l: label) (rsr rsw: regset) (mw: mem) (res: option bool) :=
   match res with
     | Some true  => par_goto_label f l rsr rsw mw
@@ -1448,6 +1205,8 @@ Definition par_eval_branch (f: function) (l: label) (rsr rsw: regset) (mw: mem)
   end.
 
 
+(* FIXME: comment not up-to-date for parallel semantics *)
+
 (** Execution of a single control-flow instruction [i] in initial state [rs] and
     [m].  Return updated state.
 
@@ -1514,18 +1273,19 @@ Definition parexec_control (f: function) (oc: option control) (rsr rsw: regset)
 end.
 
 
-Definition parexec_wio_bblock_aux (f: function) bdy ext size_b (rsr rsw: regset) (mr mw: mem): outcome :=
+Definition incrPC size_b (rs: regset) :=
+  rs#PC <- (Val.offset_ptr rs#PC size_b).
+
+(** parallel execution of the exit instruction of a bundle *)
+Definition parexec_exit (f: function) ext size_b (rsr rsw: regset) (mw: mem) 
+  := parexec_control f ext (incrPC size_b rsr) rsw mw.
+
+Definition parexec_wio_bblock_aux f bdy ext size_b (rsr rsw: regset) (mr mw: mem): outcome :=
   match parexec_wio_body bdy rsr rsw mr mw with
-  | Next rsw mw =>
-    let rsr := par_nextblock size_b rsr in 
-    parexec_control f ext rsr rsw mw
+  | Next rsw mw => parexec_exit f ext size_b rsr rsw mw
   | Stuck => Stuck
   end.
 
-(** parallel in-order writes execution of bundles *)
-Definition parexec_wio_bblock (f: function) (b: bblock) (rs: regset) (m: mem): outcome :=
-  parexec_wio_bblock_aux f (body b) (exit b) (Ptrofs.repr (size b)) rs rs m m.
-
 (** non-deterministic (out-of-order writes) parallel execution of bundles *)
 Definition parexec_bblock (f: function) (bundle: bblock) (rs: regset) (m: mem) (o: outcome): Prop :=
    exists bdy1 bdy2, Permutation (bdy1++bdy2) (body bundle) /\ 
@@ -1534,30 +1294,19 @@ Definition parexec_bblock (f: function) (bundle: bblock) (rs: regset) (m: mem) (
       | Stuck => Stuck
       end.
 
-Lemma parexec_bblock_write_in_order f b rs m:
-   parexec_bblock f b rs m (parexec_wio_bblock f b rs m).
-Proof.
-   exists (body b). exists nil.
-   constructor 1.
-   - rewrite app_nil_r; auto.
-   - unfold parexec_wio_bblock.
-     destruct (parexec_wio_bblock_aux f _ _ _ _ _); simpl; auto.
-Qed.
-
 (** deterministic parallel (out-of-order writes) execution of bundles *)
 Definition det_parexec (f: function) (bundle: bblock) (rs: regset) (m: mem) rs' m': Prop :=
    forall o, parexec_bblock f bundle rs m o -> o = Next rs' m'.
 
 
-Local Hint Resolve parexec_bblock_write_in_order.
+(* FIXME: comment not up-to-date *)
+(** Translation of the LTL/Linear/Mach view of machine registers to
+  the RISC-V view.  Note that no LTL register maps to [X31].  This
+  register is reserved as temporary, to be used by the generated RV32G
+  code.  *)
 
-Lemma det_parexec_write_in_order f b rs m rs' m':
-   det_parexec f b rs m rs' m' -> parexec_wio_bblock f b rs m = Next rs' m'.
-Proof.
-   unfold det_parexec; auto.
-Qed.
 
-  (* FIXME - R16 and R32 are excluded *)
+(* FIXME - R16 and R32 are excluded *)
 Definition preg_of (r: mreg) : preg :=
   match r with
   | R0  => GPR0  | R1  => GPR1  | R2  => GPR2  | R3  => GPR3  | R4  => GPR4
@@ -1584,7 +1333,7 @@ Definition undef_caller_save_regs (rs: regset) : regset :=
     then rs r
     else Vundef.
 
-
+(* FIXME: comment not up-to-date *)
 (** Extract the values of the arguments of an external call.
     We exploit the calling conventions from module [Conventions], except that
     we use RISC-V registers instead of locations. *)
@@ -1615,11 +1364,6 @@ Definition extcall_arguments
 Definition loc_external_result (sg: signature) : rpair preg :=
   map_rpair preg_of (loc_result sg).
 
-(** Manipulations over the [PC] register: continuing with the next
-  instruction ([nextblock]) or branching to a label ([goto_label]). *)
-
-Definition nextblock (b:bblock) (rs: regset) :=
-  rs#PC <- (Val.offset_ptr rs#PC (Ptrofs.repr (size b))).
 
 (** Looking up bblocks in a code sequence by position. *)
 Fixpoint find_bblock (pos: Z) (lb: bblocks) {struct lb} : option bblock :=
@@ -1635,6 +1379,8 @@ Fixpoint find_bblock (pos: Z) (lb: bblocks) {struct lb} : option bblock :=
 Inductive state: Type :=
   | State: regset -> mem -> state.
 
+Definition nextblock (b:bblock) (rs: regset) :=
+  incrPC (Ptrofs.repr (size b)) rs.
 
 Inductive step: state -> trace -> state -> Prop :=
   | exec_step_internal:
@@ -1667,6 +1413,31 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State rs m) t (State rs' m')
   .
 
+
+(** parallel in-order writes execution of bundles *)
+Definition parexec_wio_bblock (f: function) (b: bblock) (rs: regset) (m: mem): outcome :=
+  parexec_wio_bblock_aux f (body b) (exit b) (Ptrofs.repr (size b)) rs rs m m.
+
+
+Lemma parexec_bblock_write_in_order f b rs m:
+   parexec_bblock f b rs m (parexec_wio_bblock f b rs m).
+Proof.
+   exists (body b). exists nil.
+   constructor 1.
+   - rewrite app_nil_r; auto.
+   - unfold parexec_wio_bblock.
+     destruct (parexec_wio_bblock_aux f _ _ _ _ _); simpl; auto.
+Qed.
+
+
+Local Hint Resolve parexec_bblock_write_in_order.
+
+Lemma det_parexec_write_in_order f b rs m rs' m':
+   det_parexec f b rs m rs' m' -> parexec_wio_bblock f b rs m = Next rs' m'.
+Proof.
+   unfold det_parexec; auto.
+Qed.
+
 End RELSEM.
 
 (** Execution of whole programs. *)
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 6e2539e3..8c68deea 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -1,4 +1,5 @@
 open Asmvliw
+open Asmblock
 open Printf
 open Camlcoq
 open InstructionScheduler
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index 599a4024..f7ada92b 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -226,7 +226,7 @@ Proof.
   repeat eexists.
     unfold exec_bblock. rewrite EXEB1. rewrite EXA. simpl. eauto.
     exploit exec_body_pc. eapply EXEB1. intros. rewrite <- H. auto.
-    unfold exec_bblock. unfold nextblock. erewrite exec_body_pc_var; eauto.
+    unfold exec_bblock. unfold nextblock, incrPC. erewrite exec_body_pc_var; eauto.
     rewrite <- H1. unfold nextblock in EXEB. rewrite regset_double_set_id.
     assert (size bb = size a + size b).
     { unfold size. rewrite H0. rewrite H1. rewrite app_length. rewrite EXA. simpl. rewrite Nat.add_0_r.
@@ -234,8 +234,8 @@ Proof.
     clear EXA H0 H1. rewrite H in EXEB.
     assert (rs1 PC = rs0 PC). { apply exec_body_pc in EXEB2. auto. }
     rewrite H0. rewrite <- pc_set_add; auto.
-    exploit AB.size_positive. instantiate (1 := a). intro. omega.
-    exploit AB.size_positive. instantiate (1 := b). intro. omega.
+    exploit size_positive. instantiate (1 := a). intro. omega.
+    exploit size_positive. instantiate (1 := b). intro. omega.
 Qed.
 
 Lemma concat_all_exec_bblock (ge: Genv.t fundef unit) (f: function) :
@@ -731,9 +731,9 @@ Proof.
   destruct bb as [h bdy ext H]; simpl.
   intros; subst. destruct i.
   generalize H.
-  rewrite <- AB.wf_bblock_refl in H.
+  rewrite <- wf_bblock_refl in H.
   destruct H as [H H0].
-  unfold AB.builtin_alone in H0. erewrite H0; eauto.
+  unfold builtin_alone in H0. erewrite H0; eauto.
 Qed.
 
 Local Hint Resolve verified_schedule_nob_checks_alls_bundles.
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v
index 8a83521c..fa920a8c 100644
--- a/mppa_k1c/lib/Asmblockgenproof0.v
+++ b/mppa_k1c/lib/Asmblockgenproof0.v
@@ -1006,7 +1006,7 @@ Lemma exec_straight_through_singleinst:
 Proof.
   intros. subst. constructor 1. unfold exec_bblock. simpl body. erewrite exec_straight_body; eauto.
   simpl. auto.
-  simpl; auto. unfold nextblock; simpl. Simpl. erewrite exec_straight_pc; eauto.
+  simpl; auto. unfold nextblock, incrPC; simpl. Simpl. erewrite exec_straight_pc; eauto.
 Qed.
 
 (** The following lemmas show that straight-line executions