Starts proof for `tunnel_step_correct`

1 files changed, 120 insertions, 15 deletions

diff --git a/backend/RTLTunnelingproof.v b/backend/RTLTunnelingproof.v
index f63c3b35..c54667a4 100644
--- a/backend/RTLTunnelingproof.v
+++ b/backend/RTLTunnelingproof.v
@@ -16,7 +16,7 @@
 
 Require Import Coqlib Maps Errors.
 Require Import AST Linking.
-Require Import Values Memory Events Globalenvs Smallstep.
+Require Import Values Memory Registers Events Globalenvs Smallstep.
 Require Import Op Locations RTL.
 Require Import RTLTunneling.
 Require Import Conventions1.
@@ -41,25 +41,29 @@ Qed.
   | TB_default (TB: target pc = pc) oi:
       target_bounds target bound pc oi
   | TB_nop s
-    (EQ: target pc = target s)
-    (DEC: bound s < bound pc):
-    target_bounds target bound pc (Some (Inop s))
+      (EQ: target pc = target s)
+      (DEC: bound s < bound pc):
+      target_bounds target bound pc (Some (Inop s))
   | TB_cond cond args ifso ifnot info
       (EQSO: target pc = target ifso)
       (EQNOT: target pc = target ifnot)
       (DECSO: bound ifso < bound pc)
       (DECNOT: bound ifnot < bound pc):
-      target_bounds target bound pc (Some (Icond cond args ifso ifnot info)).
+      target_bounds target bound pc (Some (Icond cond args ifso ifnot info))
+.
+Local Hint Resolve TB_default: core.
 
 Lemma target_None (td: UF) (pc: node): td!pc = None -> td pc = pc.
 Proof.
   unfold target, get. intro EQ. rewrite EQ. auto.
 Qed.
+Local Hint Resolve target_None Z.abs_nonneg: core.
 
 Lemma get_nonneg td pc t d: get td pc = (t,d) -> (0 <= d)%Z.
 Proof.
   unfold get. destruct td!pc as [(tpc,dpc)|]; intro H; inv H; lia.
 Qed.
+Local Hint Resolve get_nonneg: core.
 
 (**) Definition bound (td: UF) (pc: node) := Z.to_nat (snd (get td pc)).
 
@@ -93,6 +97,48 @@ Proof.
   - intros _. apply TB_default. unfold target. unfold get. rewrite EQ. auto.
 Qed.
 
+Definition check_code_spec (td:UF) (c:code) (ok: res unit) :=
+   ok = OK tt -> forall pc i, c!pc = Some i -> target_bounds (target td) (bound td) pc (Some i).
+
+Lemma check_code_correct (td:UF) c:
+   check_code_spec td c (check_code td c).
+Proof.
+  unfold check_code. apply PTree_Properties.fold_rec; unfold check_code_spec.
+  - intros. rewrite <- H in H2. apply H0; auto.
+  - intros. rewrite PTree.gempty in H0. congruence.
+  - intros m [[]|e] pc i N S IND; simpl; try congruence.
+    intros H pc0 i0. rewrite PTree.gsspec. destruct (peq _ _).
+    subst. intro. inv H0. apply check_instr_correct. apply H.
+    auto.
+Qed.
+
+Theorem branch_target_bounds:
+  forall f tf pc,
+  tunnel_function f = OK tf ->
+  target_bounds (branch_target f) (bound (branch_target f)) pc (f.(fn_code)!pc).
+Proof.
+(* ~old
+  intros t tf pc. unfold tunnel_function.
+  destruct (check_included _ _) eqn:HI; try congruence.
+  destruct (check_code _ _) eqn: HC.
+  - intros _. destruct ((fn_code t) ! pc) eqn:EQ.
+    + exploit check_code_correct; eauto.
+    replace tt with u. auto. {destruct u; auto. }
+    + exploit check_included_correct; eauto. rewrite HI. congruence.
+    intro. apply TB_default. unfold target. unfold get. rewrite H. debug auto.
+  - simpl. congruence.
+*)
+
+  intros. unfold tunnel_function in H.
+  destruct (check_included _ _) eqn:EQinc; try congruence.
+  monadInv H. rename EQ into EQcode.
+  destruct (_ ! _) eqn:EQ.
+  - exploit check_code_correct. destruct x. apply EQcode. apply EQ. auto.
+  - exploit check_included_correct.
+    rewrite EQinc. congruence.
+    apply EQ.
+    intro. apply TB_default. apply target_None. apply H.
+Qed.
 
 (** Preservation of semantics *)
 
@@ -137,7 +183,7 @@ Lemma function_ptr_translated:
   exists tf,
   Genv.find_funct_ptr tge v = Some tf /\ tunnel_fundef f = OK tf.
 Proof.
-  intros. exploit (Genv.find_funct_ptr_match TRANSL). 
+  intros. exploit (Genv.find_funct_ptr_match TRANSL).
   - apply H.
   - intros (cu & tf & A & B & C). exists tf. split. apply A. apply B.
 Qed.
@@ -170,7 +216,7 @@ Proof.
   - monadInv H. auto.
 Qed.
 
-(**) Lemma senv_preserved:
+Lemma senv_preserved:
   Senv.equiv ge tge.
 Proof.
   eapply (Genv.senv_match TRANSL). (* Il y a déjà une preuve de cette propriété très exactement, je ne vais pas réinventer la roue ici *)
@@ -216,32 +262,41 @@ Inductive match_states: state -> state -> Prop :=
         (Returnstate ts tv tm).
 
 (* TODO: il faut définir une bonne mesure *)
-(**) Definition measure (st: state) : nat :=
+(* (**) Definition measure (st: state) : nat :=
   match st with
   | State s f sp pc rs m =>
       match (fn_code f)!pc with
-      | Some (Inop pc) => (bound (branch_target f) pc) * 2 + 1
+      | Some (Inop pc') => (bound (branch_target f) pc') * 2 + 1
       | Some (Icond _ _ ifso ifnot _) => (max
                                     (bound (branch_target f) ifso)
                                     (bound (branch_target f) ifnot)
                                   ) * 2 + 1
-      | Some _ => 0
+      | Some _ => (bound (branch_target f) pc) * 2
       | None => 0
       end
   | Callstate s f v m => 0
   | Returnstate s v m => 0
   end.
+*)
+
+Definition measure (st: state): nat :=
+  match st with
+  | State s f sp pc rs m => bound (branch_target f) pc
+  | Callstate s f v m => 0
+  | Returnstate s v m => 0
+  end.
+
 
 (* rq: sans les lemmes définis au-dessus je ne vois pas trop comment j'aurais
  * fait... ni comment j'aurais eu l'idée d'en faire des lemmes ? *)
-Lemma transf_initial_states:
+(**) Lemma transf_initial_states:
   forall s1: state, initial_state prog s1 ->
   exists s2: state, initial_state tprog s2 /\ match_states s1 s2.
 Proof.
   intros. inversion H as [b f m0 ge0 MEM SYM PTR SIG CALL].
   exploit function_ptr_translated.
   - apply PTR.
-  - intros (tf & TPTR & TUN). 
+  - intros (tf & TPTR & TUN).
     exists (Callstate nil tf nil m0). split.
     + apply initial_state_intro with b.
       * apply (Genv.init_mem_match TRANSL). apply MEM.
@@ -256,7 +311,7 @@ Proof.
       * apply Mem.extends_refl.
 Qed.
 
-Lemma transf_final_states:
+(**) Lemma transf_final_states:
   forall (s1 : state)
   (s2 : state) (r : Integers.Int.int),
   match_states s1 s2 ->
@@ -268,6 +323,27 @@ Proof.
   intros. inv H0. inv H. inv VAL. inversion STK. apply final_state_intro.
 Qed.
 
+Lemma tunnel_function_unfold:
+  forall f tf pc,
+  tunnel_function f = OK tf ->
+  (fn_code tf) ! pc =
+  option_map (tunnel_instr (branch_target f)) (fn_code f) ! pc.
+Proof.
+  intros f tf pc.
+  unfold tunnel_function.
+  destruct (check_included _ _) eqn:EQinc; try congruence.
+  destruct (check_code _ _) eqn:EQcode; simpl; try congruence.
+  intro. inv H. simpl. rewrite PTree.gmap1. reflexivity.
+Qed.
+
+Lemma reglist_lessdef:
+  forall (rs trs: Registers.Regmap.t val) (args: list Registers.reg),
+  regs_lessdef rs trs -> Val.lessdef_list (rs##args) (trs##args).
+Proof.
+  intros. induction args; simpl; constructor.
+  apply H. apply IHargs.
+Qed.
+
 (* `Lemma tunnel_step_correct` correspond au diagramme "option simulation" *)
 Lemma tunnel_step_correct:
   forall st1 t st2, step ge st1 t st2 ->
@@ -275,8 +351,37 @@ Lemma tunnel_step_correct:
   (exists st2', step tge st1' t st2' /\ match_states st2 st2')
   \/ (measure st2 < measure st1 /\ t = E0 /\ match_states st2 st1')%nat.
 Proof.
-  intros st1 t st2 H. induction H; intros; inv MS.
-Admitted.
+  intros st1 t st2 H. induction H; intros; try (inv MS).
+  - (* Inop *)
+    exploit branch_target_bounds. apply TF.
+    rewrite H. intro. inv H0.
+    + (* TB_default *)
+      rewrite TB. left. eexists. split.
+      * apply exec_Inop. rewrite (tunnel_function_unfold f tf pc). rewrite H. simpl. eauto. apply TF.
+      * constructor; try assumption.
+    + (* TB_nop *)
+      simpl. right. repeat split. apply DEC.
+      rewrite EQ. apply match_states_intro; assumption.
+  - (* Iop *)
+    exploit eval_operation_lessdef; try eassumption.
+    apply reglist_lessdef. apply RS.
+    intros (tv & EVAL & LD).
+    left; eexists; split.
+    + eapply exec_Iop with (v:=tv).
+      assert ((fn_code tf) ! pc = Some (Iop op args res (branch_target f pc'))).
+      rewrite (tunnel_function_unfold f tf pc); eauto.
+      rewrite H. simpl. reflexivity.
+      (* TODO: refaire ça joliment *)
+      assert (target_bounds (branch_target f) (bound (branch_target f)) pc (fn_code f)! pc).
+      apply (branch_target_bounds) with tf. apply TF.
+      inv H2. rewrite TB. apply H1. rewrite H in H4. congruence.
+      rewrite H in H4. congruence.
+      rewrite <- EVAL. apply eval_operation_preserved. apply symbols_preserved.
+    + apply match_states_intro; eauto. apply set_reg_lessdef. apply LD. apply RS.
+  - (* Iload *)
+
+
+Qed.
 
 
 Theorem transf_program_correct: