squelette de preuve pour Machblockgenproof.v

3 files changed, 228 insertions, 21 deletions

diff --git a/mppa_k1c/Machblockgen.v b/mppa_k1c/Machblockgen.v
index a0786ac1..18abb927 100644
--- a/mppa_k1c/Machblockgen.v
+++ b/mppa_k1c/Machblockgen.v
@@ -38,11 +38,23 @@ Definition trans_inst (i:Mach.instruction) : Machblock_inst :=
   | Mlabel l => MB_label l
   end.
 
+Definition empty_bblock:={| header := nil; body := nil; exit := None |}.
+Extraction Inline empty_bblock.
+
+Definition add_label l bb:={| header := l::(header bb); body := (body bb); exit := (exit bb) |}. 
+Extraction Inline add_label.
+
+Definition add_basic bi bb :={| header := nil; body := bi::(body bb); exit := (exit bb) |}.
+Extraction Inline add_basic.
+
+Definition cfi_bblock cfi:={| header := nil; body := nil; exit := Some cfi |}.
+Extraction Inline cfi_bblock.
+
 Definition add_to_new_bblock (i:Machblock_inst) : bblock :=
   match i with
-  | MB_label l => {| header := l::nil; body := nil; exit := None |}
-  | MB_basic i => {| header := nil; body := i::nil; exit := None |}
-  | MB_cfi i => {| header := nil; body := nil; exit := Some i |}
+  | MB_label l => add_label l empty_bblock
+  | MB_basic i => add_basic i empty_bblock
+  | MB_cfi i => cfi_bblock i
   end.
 
 (* ajout d'une instruction en début d'une liste de blocks *)
@@ -53,15 +65,15 @@ Definition add_to_new_bblock (i:Machblock_inst) : bblock :=
 (* label -> /1\ (dans header)*)
 Definition add_to_code (i:Machblock_inst) (bl:code) : code :=
   match bl with
-  | h::bl0 => match i with
-              | MB_label l => {| header := l::(header h); body := (body h); exit := (exit h) |}::bl0
-              | MB_cfi i0 => add_to_new_bblock(i)::bl
-              | MB_basic i0 => match (header h) with
-                               |_::_ => (add_to_new_bblock i)::bl
-                               | nil => {| header := (header h); body := i0::(body h); exit := (exit h) |}::bl0
+  | bh::bl0 => match i with
+              | MB_label l => add_label l bh::bl0
+              | MB_cfi i0 => cfi_bblock i0::bl
+              | MB_basic i0 => match header bh with
+                               |_::_ => add_basic i0 empty_bblock::bl
+                               | nil => add_basic i0 bh::bl0
                                end
               end
-  | _ => (add_to_new_bblock i)::nil
+  | _ => add_to_new_bblock i::nil
   end.
   
 Fixpoint trans_code_rev (c: Mach.code) (bl:code) : code := 
@@ -74,6 +86,7 @@ Fixpoint trans_code_rev (c: Mach.code) (bl:code) : code :=
 Function trans_code (c: Mach.code) : code :=
   trans_code_rev (List.rev_append c nil) nil.
 
+
 (* à finir pour passer des Mach.function au function, etc. *)
 Definition transf_function (f: Mach.function) : function :=
   {| fn_sig:=Mach.fn_sig f;
@@ -88,3 +101,88 @@ Definition transf_fundef (f: Mach.fundef) : fundef :=
 
 Definition transf_program (src: Mach.program) : program :=
   transform_program transf_fundef src.
+
+
+(** Abstraction de trans_code *)
+
+Inductive is_end_block: Machblock_inst -> code -> Prop :=
+  | End_empty mbi: is_end_block mbi nil
+  | End_basic bi bh bl: header bh <> nil -> is_end_block (MB_basic bi) (bh::bl)
+  | End_cfi cfi bl: bl <> nil -> is_end_block (MB_cfi cfi) bl. 
+
+Local Hint Resolve End_empty End_basic End_cfi.
+
+Inductive is_trans_code: Mach.code -> code -> Prop :=
+  | Tr_nil: is_trans_code nil nil
+  | Tr_end_block i c bl:
+      is_trans_code c bl ->
+      is_end_block (trans_inst i) bl ->
+      is_trans_code (i::c) (add_to_new_bblock (trans_inst i)::bl)
+  | Tr_add_label i l bh c bl:
+      is_trans_code c (bh::bl) ->
+      i = Mlabel l ->
+      is_trans_code (i::c) (add_label l bh::bl)
+  | Tr_add_basic i bi bh c bl:
+      is_trans_code c (bh::bl) ->
+      trans_inst i = MB_basic bi ->
+      header bh = nil ->
+      is_trans_code (i::c) (add_basic bi bh::bl).
+
+Local Hint Resolve Tr_nil Tr_end_block.
+
+Lemma add_to_code_is_trans_code i c bl:
+  is_trans_code c bl ->
+  is_trans_code (i::c) (add_to_code (trans_inst i) bl).
+Proof.
+  destruct bl as [|bh0 bl]; simpl.
+  - intro H; inversion H; subst; eauto.
+  - remember (trans_inst i) as ti.
+    destruct ti as [l|bi|cfi].
+    + intros; eapply Tr_add_label; eauto. destruct i; simpl in * |- *; congruence.
+    + 
+Admitted. (* A FINIR *)
+
+Local Hint Resolve add_to_code_is_trans_code.
+
+Lemma trans_code_is_trans_code_rev c1: forall c2 mbi, 
+  is_trans_code c2 mbi ->
+  is_trans_code (rev_append c1 c2) (trans_code_rev c1 mbi).
+Proof.
+  induction c1 as [| i c1]; simpl; auto.
+Qed.
+
+Lemma trans_code_is_trans_code c: is_trans_code c (trans_code c).
+Proof.
+  unfold trans_code.
+  rewrite <- rev_alt.
+  rewrite <- (rev_involutive c) at 1.
+  rewrite rev_alt at 1.
+  apply trans_code_is_trans_code_rev; auto.
+Qed.
+
+Lemma add_to_code_is_trans_code_inv i c bl:
+  is_trans_code (i::c) bl -> exists bl0, is_trans_code c bl0 /\ bl = add_to_code (trans_inst i) bl0.
+Proof.
+  intro H; inversion H as [|H0 H1 bl0| | H0 bi bh H1 bl0]; clear H; subst; (repeat econstructor); eauto.
+  + (* case Tr_end_block *) inversion H3; subst; simpl; auto.
+     * destruct (header bh); congruence.
+     * destruct bl0; simpl; congruence.
+  + (* case Tr_add_basic *)
+Admitted. (* A FINIR *)
+
+Lemma trans_code_is_trans_code_rev_inv c1: forall c2 mbi, 
+  is_trans_code (rev_append c1 c2) mbi ->
+  exists mbi0, is_trans_code c2 mbi0 /\ mbi=trans_code_rev c1 mbi0.
+Proof.
+  induction c1 as [| i c1]; simpl; eauto.
+  intros; exploit IHc1; eauto.
+  intros (mbi0 & H1 & H2); subst.
+  exploit add_to_code_is_trans_code_inv; eauto.
+Admitted. (* A FINIR *)
+
+Local Hint Resolve trans_code_is_trans_code.
+
+Theorem is_trans_code_inv c bl: is_trans_code c bl <-> bl=(trans_code c).
+Proof.
+  constructor; intros; subst; auto.
+Admitted. (* A FINIR *)
diff --git a/mppa_k1c/Machblockgenproof.v b/mppa_k1c/Machblockgenproof.v
index 62c1e0ed..d7a5ed7d 100644
--- a/mppa_k1c/Machblockgenproof.v
+++ b/mppa_k1c/Machblockgenproof.v
@@ -39,7 +39,7 @@ Fixpoint trans_stack (mst: list Mach.stackframe) : list stackframe :=
   | msf :: mst0 => (trans_stackframe msf) :: (trans_stack mst0)
   end.
 
-Definition trans_state (ms: Mach.state) : state :=
+Definition trans_state (ms: Mach.state): state :=
   match ms with
   | Mach.State        s f sp c rs m => State        (trans_stack s) f sp (trans_code c) rs m
   | Mach.Callstate    s f rs m      => Callstate    (trans_stack s) f rs m
@@ -170,6 +170,8 @@ Definition concat (h: list label) (c: code): code :=
   | b::c' => {| header := h ++ (header b); body := body b; exit := exit b |}::c'
   end.
 
+(* VIELLES PREUVES -- UTILE POUR S'INSPIRER ??? 
+
 Lemma to_bblock_start_label i c l b c0: 
   (b, c0) = to_bblock (i :: c)
   -> In l (header b)
@@ -264,13 +266,23 @@ Proof.
   - destruct i; try (
       simpl in H; inversion H; subst; clear H; auto; fail).
 Qed.
+*)
+
+Axiom TODO: False. (* A ELIMINER *)
 
 Lemma find_label_transcode_preserved:
   forall l c c',
   Mach.find_label l c = Some c' ->
   exists h, In l h /\ find_label l (trans_code c) = Some (concat h (trans_code c')).
 Proof.
-  intros l c; induction c, (trans_code c) using trans_code_ind.
+  intros l c. remember (trans_code _) as bl.
+  rewrite <- is_trans_code_inv in * |-.
+  induction Heqbl;
+  elim TODO. (* A FAIRE *)
+Qed.
+
+(* VIELLE PREUVE -- UTILE POUR S'INSPIRER ??? 
+ induction c, (trans_code c) using trans_code_ind.
   - intros c' H; inversion H.
   - intros c' H. subst _x. destruct c as [| i c]; try tauto.
    unfold to_bblock in * |-.
@@ -290,7 +302,7 @@ Proof.
      erewrite (to_bblock_body_find_label c1 l c2); eauto.
      erewrite (to_bblock_exit_find_label c2 l c0); eauto.
 Qed.
-
+*)
 
 Lemma find_label_preserved:
   forall l f c,
@@ -311,7 +323,13 @@ Qed.
 Local Hint Resolve symbols_preserved senv_preserved init_mem_preserved prog_main_preserved functions_translated
                    parent_sp_preserved.
 
-Definition dist_end_block_code (c: Mach.code) := (size (fst (to_bblock c))-1)%nat.
+
+
+Definition dist_end_block_code (c: Mach.code) := 
+ match trans_code c with
+ | nil => 0
+ | bh::_ => (size bh-1)%nat
+ end.
 
 
 Definition dist_end_block (s: Mach.state): nat :=
@@ -323,6 +341,8 @@ Definition dist_end_block (s: Mach.state): nat :=
 Local Hint Resolve exec_nil_body exec_cons_body.
 Local Hint Resolve exec_MBgetstack exec_MBsetstack exec_MBgetparam exec_MBop exec_MBload exec_MBstore.
 
+(* VIELLES PREUVES -- UTILE POUR S'INSPIRER ??? 
+
 Ltac ExploitDistEndBlockCode :=
   match goal with
   | [ H : dist_end_block_code (Mlabel ?l :: ?c) <> 0%nat |- _ ] =>
@@ -377,11 +397,22 @@ Proof.
   - contradict H. destruct i; try discriminate.
     all: unfold dist_end_block_code; erewrite to_bblock_CFI; eauto; simpl; eauto.
 Qed.
+*)
+
+Lemma dist_end_block_code_simu_mid_block i c:
+  dist_end_block_code (i::c) <> 0 ->
+  (dist_end_block_code (i::c) = Datatypes.S (dist_end_block_code c)).
+Proof.
+  unfold dist_end_block_code.
+  remember (trans_code (i::c)) as bl.
+  rewrite <- is_trans_code_inv in * |-.
+  inversion Heqbl as [| | |]; subst.
+Admitted. (* A FAIRE *)
 
 Local Hint Resolve dist_end_block_code_simu_mid_block.
 
 Lemma step_simu_basic_step (i: Mach.instruction) (bi: basic_inst) (c: Mach.code) s f sp rs m (t:trace) (s':Mach.state):
-  to_basic_inst i = Some bi ->
+  trans_inst i = MB_basic bi ->
   Mach.step (inv_trans_rao rao) ge (Mach.State s f sp (i::c) rs m) t s' ->
   exists rs' m', s'=Mach.State s f sp c rs' m' /\ t=E0 /\ basic_step tge (trans_stack s) f sp rs m bi rs' m'.
 Proof.
@@ -400,6 +431,7 @@ Proof.
 Qed.
 
 
+(* VIELLE PREUVE -- UTILE POUR S'INSPIRER ??? 
 Lemma star_step_simu_body_step s f sp c:
  forall (p:bblock_body) c' rs m t s',
   to_bblock_body c = (p, c') ->
@@ -426,6 +458,7 @@ Proof.
      inversion_clear H; simpl.
      intros X; inversion_clear X. intuition eauto.
 Qed.
+*)
 
 Local Hint Resolve exec_MBcall exec_MBtailcall exec_MBbuiltin exec_MBgoto exec_MBcond_true exec_MBcond_false exec_MBjumptable exec_MBreturn exec_Some_exit exec_None_exit.
 Local Hint Resolve eval_builtin_args_preserved external_call_symbols_preserved find_funct_ptr_same.
@@ -433,6 +466,16 @@ Local Hint Resolve eval_builtin_args_preserved external_call_symbols_preserved f
 Lemma match_states_concat_trans_code st f sp c rs m h: 
   match_states (Mach.State st f sp c rs m) (State (trans_stack st) f sp (concat h (trans_code c)) rs m).
 Proof.
+  intros; remember (trans_code _) as bl.
+  rewrite <- is_trans_code_inv in * |-.
+  constructor 1; simpl.
+  + intros (t0 & s1' & H0) t s'. 
+    inversion Heqbl as [| | |]; subst; simpl;  (* inversion vs induction ?? *)
+    elim TODO. (* A FAIRE *)
+  + intros H r; constructor 1; intro X; inversion X.
+Qed.
+
+(* VIELLES PREUVES -- UTILE POUR S'INSPIRER ??? 
   constructor 1; simpl.
   + intros (t0 & s1' & H0) t s'. 
     rewrite! trans_code_equation.
@@ -486,7 +529,6 @@ Proof.
 Qed.
 
 
-
 Lemma step_simu_exit_step c e c' stk f sp rs m t s' b:
   to_bblock_exit c = (e, c') ->
   starN (Mach.step (inv_trans_rao rao)) (Genv.globalenv prog) (length_opt e) (Mach.State stk f sp c rs m) t s' ->
@@ -516,6 +558,7 @@ Proof.
      inversion H1; clear H1; subst; auto. autorewrite with trace_rewrite.
      exploit IHc; eauto.
 Qed. 
+*)
 
 Lemma simu_end_block:
   forall s1 t s1',
@@ -524,14 +567,23 @@ Lemma simu_end_block:
 Proof.
   destruct s1; simpl.
   + (* State *)
-    (* c cannot be nil *)
-    destruct c as [|i c]; simpl; try ( (* nil => absurd *)
+    unfold dist_end_block_code.
+    remember (trans_code _) as bl.
+    rewrite <- is_trans_code_inv in * |-.
+    intros t s1' H.
+    inversion Heqbl as [| | |]; subst; simpl in * |- *;  (* inversion vs induction ?? *)
+    elim TODO. (* A FAIRE *)
+ 
+  (* VIELLE PREUVE -- UTILE POUR S'INSPIRER ??? 
+
+   destruct c as [|i c]; simpl; try ( (* nil => absurd *)
       unfold dist_end_block_code; simpl;
       intros t s1' H; inversion_clear H;
       inversion_clear H0; fail
     ).
 
     intros t s1' H.
+
     remember (_::_) as c0. remember (trans_code c0) as tc0.
 
     (* tc0 cannot be nil *)
@@ -576,6 +628,7 @@ Proof.
     intros (s2' & H3 & H4).
     eapply ex_intro; intuition eauto.
     eapply exec_bblock; eauto.
+*)
   + (* Callstate *)
     intros t s1' H; inversion_clear H.
     eapply ex_intro; constructor 1; eauto.
@@ -604,8 +657,10 @@ Theorem transf_program_correct:
 Proof.
   apply forward_simulation_block_trans with (dist_end_block := dist_end_block) (trans_state := trans_state).
 (* simu_mid_block *)
-  - intros s1 t s1' H1.
+  - intros s1 t s1' H1. elim TODO. (* A FAIRE *)
+    (* VIELLE PREUVE -- UTILE POUR S'INSPIRER ??? 
     destruct H1; simpl; omega || (intuition auto).
+    *)
 (* public_preserved *)
   - apply senv_preserved.
 (* match_initial_states *)
@@ -618,10 +673,13 @@ Proof.
 (* match_final_states *)
   - intros. simpl. destruct H. split with (r := r); auto.
 (* final_states_end_block *)
-  - intros. simpl in H0. inversion H0.
-    inversion H; simpl; auto.
+  - intros. simpl in H0. elim TODO.
+  (* VIELLE PREUVE -- UTILE POUR S'INSPIRER ??? 
+    inversion H0.
+    inversion H; simpl; auto. 
     (* the remaining instructions cannot lead to a Returnstate *)
     all: subst; discriminate.
+  *)
 (* simu_end_block *)
   - apply simu_end_block.
 Qed.
diff --git a/mppa_k1c/lib/ForwardSimulationBlock.v b/mppa_k1c/lib/ForwardSimulationBlock.v
index dc8beb29..39dd2234 100644
--- a/mppa_k1c/lib/ForwardSimulationBlock.v
+++ b/mppa_k1c/lib/ForwardSimulationBlock.v
@@ -271,6 +271,7 @@ However, the Machblock state after a goto remains "equivalent" to the trans_stat
 
 *)
 
+
 Section ForwardSimuBlock_TRANS.
 
 Variable L1 L2: semantics.
@@ -320,3 +321,53 @@ Proof.
 Qed.
 
 End ForwardSimuBlock_TRANS.
+
+
+(* another version with a relation [trans_state_R] instead of a function [trans_state] *)
+Section ForwardSimuBlock_TRANS_R.
+
+Variable L1 L2: semantics.
+
+Variable trans_state_R: state L1 -> state L2 -> Prop.
+
+Definition match_states_R s1 s2: Prop :=
+  exists s2', trans_state_R s1 s2' /\ equiv_on_next_step _ (exists t s1', Step L1 s1 t s1') (exists r, final_state L1 s1 r) s2 s2'.
+
+Lemma match_states_trans_state_R s1 s2: trans_state_R s1 s2 -> match_states_R s1 s2.
+Proof.
+  unfold match_states, equiv_on_next_step. firstorder.
+Qed.
+
+Variable dist_end_block: state L1 -> nat.
+
+Hypothesis simu_mid_block:
+  forall s1 t s1', Step L1 s1 t s1' -> (dist_end_block s1)<>0 -> t = E0 /\ dist_end_block s1=S (dist_end_block s1').
+
+Hypothesis public_preserved:
+  forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id.
+
+Hypothesis match_initial_states:
+  forall s1, initial_state L1 s1 -> exists s2, match_states_R s1 s2 /\ initial_state L2 s2.
+
+Hypothesis match_final_states:
+  forall s1 s2 r, final_state L1 s1 r -> trans_state_R s1 s2 -> final_state L2 s2 r.
+
+Hypothesis final_states_end_block:
+  forall s1 t s1' r, Step L1 s1 t s1' -> final_state L1 s1' r -> dist_end_block s1 = 0.
+
+Hypothesis simu_end_block:
+  forall s1 t s1' s2, starN (step L1) (globalenv L1) (S (dist_end_block s1)) s1 t s1' -> trans_state_R s1 s2 -> exists s2', Step L2 s2 t s2' /\ match_states_R s1' s2'.
+
+Lemma forward_simulation_block_trans_R: forward_simulation L1 L2.
+Proof.
+  eapply forward_simulation_block_rel with (dist_end_block:=dist_end_block) (match_states:=match_states_R); try tauto.
+  + (* final_states *) intros s1 s2 r H1 (s2' & H2 & H3 & H4). rewrite H4; eauto.
+  + (* simu_end_block *)
+    intros s1 t s1' s2 H1 (s2' & H2 & H2a & H2b). exploit simu_end_block; eauto.
+    intros (x & Hx & (y & H3 & H4 & H5)). repeat (econstructor; eauto).
+    rewrite H2a; eauto.
+    inversion_clear H1. eauto.
+Qed.
+
+End ForwardSimuBlock_TRANS_R.
+