Monday's work on RTLTunnelingproof

1 files changed, 153 insertions, 31 deletions

diff --git a/backend/RTLTunnelingproof.v b/backend/RTLTunnelingproof.v
index 57f14b9f..f63c3b35 100644
--- a/backend/RTLTunnelingproof.v
+++ b/backend/RTLTunnelingproof.v
@@ -23,6 +23,77 @@ Require Import Conventions1.
 
 Local Open Scope nat.
 
+(**) Definition check_included_spec (c:code) (td:UF) (ok: option instruction) :=
+  ok <> None -> forall pc, c!pc = None -> td!pc = None.
+
+Lemma check_included_correct (td:UF) (c:code):
+  check_included_spec c td (check_included td c).
+Proof.
+  apply PTree_Properties.fold_rec with (P:=check_included_spec c); unfold check_included_spec.
+  - intros m m' oi EQ IND N pc. rewrite <- EQ. apply IND. apply N.
+  - intros N pc. rewrite PTree.gempty. auto.
+  - intros m oi pc v N S IND. destruct oi.
+    + intros. rewrite PTree.gsspec. destruct (peq _ _); try congruence. apply IND. congruence. apply H0.
+    + contradiction.
+Qed.
+
+(**) Inductive target_bounds (target: node -> node) (bound: node -> nat) (pc: node) : option instruction -> Prop :=
+  | 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))
+  | 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)).
+
+Lemma target_None (td: UF) (pc: node): td!pc = None -> td pc = pc.
+Proof.
+  unfold target, get. intro EQ. rewrite EQ. auto.
+Qed.
+
+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.
+
+(**) Definition bound (td: UF) (pc: node) := Z.to_nat (snd (get td pc)).
+
+
+(* TODO: à réécrire proprement *)
+Lemma check_instr_correct (td: UF) (pc: node) (i: instruction):
+  check_instr td pc i = OK tt ->
+  target_bounds (target td) (bound td) pc (Some i).
+Proof.
+  unfold check_instr. destruct (td!pc) as [(tpc,dpc)|] eqn:EQ.
+  assert (DPC: snd (get td pc) = Z.abs dpc). { unfold get. rewrite EQ. auto. }
+  - destruct i; try congruence.
+    + destruct (get td n) as (ts,ds) eqn:EQs.
+      destruct (peq _ _); try congruence.
+      destruct (zlt _ _); try congruence. intros _.
+      apply TB_nop. replace (td pc) with tpc.
+      unfold target. rewrite EQs. auto.
+      unfold target. unfold get. rewrite EQ. auto.
+      unfold bound. rewrite DPC. rewrite EQs; simpl. apply Z2Nat.inj_lt; try lia. apply get_nonneg with td n ts. apply EQs.
+    + destruct (get td n) as (tso,dso) eqn:EQSO.
+      destruct (get td n0) as (tnot,dnot) eqn:EQNOT.
+      intro H.
+      repeat ((destruct (peq _ _) in H || destruct (zlt _ _) in H); try congruence).
+      apply TB_cond; subst.
+      * unfold target. replace (fst (get td pc)) with tnot. rewrite EQSO. auto.
+        unfold get. rewrite EQ. auto.
+      * unfold target. replace (fst (get td pc)) with tnot. rewrite EQNOT. auto.
+        unfold get. rewrite EQ. auto.
+      * unfold bound. rewrite DPC. apply Z2Nat.inj_lt; try lia. apply get_nonneg with td n tnot. rewrite EQSO. auto. rewrite EQSO. auto.
+      * unfold bound. rewrite DPC. apply Z2Nat.inj_lt; try lia. apply get_nonneg with td n0 tnot. rewrite EQNOT; auto. rewrite EQNOT; auto.
+  - intros _. apply TB_default. unfold target. unfold get. rewrite EQ. auto.
+Qed.
+
+
 (** Preservation of semantics *)
 
 Definition match_prog (p tp: program) :=
@@ -32,6 +103,8 @@ Definition match_prog (p tp: program) :=
    *     `p` et `tp` sont les programmes donc on doit dire s'ils match
    *)
 
+
+
 Section PRESERVATION.
 
 
@@ -41,14 +114,21 @@ Let ge := Genv.globalenv prog.
 Let tge := Genv.globalenv tprog.
 
 (* rq: pour les deux lemmes suivants, j'ai recopié les preuves, mais je ne les comprends pas du tout... D'où vient `exploit` ?? *)
+(* rq: `exploit` vient de Coqlib! Mais je comprends pas encore vraiment ce qui se passe... *)
 Lemma functions_translated:
   forall (v: val) (f: fundef),
   Genv.find_funct ge v = Some f ->
   exists tf, tunnel_fundef f = OK tf /\ Genv.find_funct tge v = Some tf.
 Proof.
-  intros. exploit (Genv.find_funct_match TRANSL). eauto.
+  intros.
+  exploit (Genv.find_funct_match TRANSL). apply H.
   intros (cu & tf & A & B & C).
-  repeat eexists; intuition eauto.
+  (* exists tf. split. apply B. apply A. *)
+  (* rq: on peut remplacer les `split` et `apply` par `eauto`, et ne pas spécifier le
+   * `exists`, avec un `eexists` *)
+  eexists. eauto.
+  (* rq: Je ne comprends pas à quoi sert le `intuition`... *)
+  (* repeat eexists; intuition eauto. *)
 Qed.
 
 Lemma function_ptr_translated:
@@ -57,30 +137,43 @@ 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_transf_partial TRANSL); eauto.
+  intros. exploit (Genv.find_funct_ptr_match TRANSL). 
+  - apply H.
+  - intros (cu & tf & A & B & C). exists tf. split. apply A. apply B.
 Qed.
 
 Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s.
 Proof.
-  rewrite (Genv.find_symbol_match TRANSL). auto.
+  apply (Genv.find_symbol_match TRANSL).
+  (* rq: ici pas de `exploit` mais un `apply` parce que `Genv.find_symbol_match
+   * prouve vraiment pile ce qu'on veut *)
 Qed.
 
 Lemma sig_preserved:
   forall f tf, tunnel_fundef f = OK tf -> funsig tf = funsig f.
 Proof.
-  intros. destruct f.
-  - simpl in H. monadInv H. (* rq: c'est une tactique maison... *)
+  intros. destruct f; simpl in H.
+  -
+    (*
+    unfold bind in H.
+    destruct (tunnel_function _) as [x|] eqn:EQ; try congruence.
+    inversion H.
     unfold tunnel_function in EQ.
-    destruct (check_included _ _) as [_|] in EQ; try congruence.
+    destruct (check_included _ _) in EQ; try congruence.
+    unfold bind in EQ. destruct (check_code _ _) in EQ; try congruence. inversion EQ. auto.
+    *)
+
+    monadInv H. (* rq: c'est une tactique maison... *)
+    unfold tunnel_function in EQ.
+    destruct (check_included _ _) in EQ; try congruence.
     monadInv EQ. auto.
-  - simpl in H. monadInv H. auto.
+  - 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, je ne vais pas réinventer la roue ici *)
+  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 *)
 Qed.
 
 (* TODO: vérifier s'il faut faire quelque chose avec le `res` ? *)
@@ -122,27 +215,47 @@ Inductive match_states: state -> state -> Prop :=
         (Returnstate s v m)
         (Returnstate ts tv tm).
 
+(* TODO: il faut définir une bonne mesure *)
+(**) 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 (Icond _ _ ifso ifnot _) => (max
+                                    (bound (branch_target f) ifso)
+                                    (bound (branch_target f) ifnot)
+                                  ) * 2 + 1
+      | Some _ => 0
+      | None => 0
+      end
+  | 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:
   forall s1: state, initial_state prog s1 ->
   exists s2: state, initial_state tprog s2 /\ match_states s1 s2.
 Proof.
-  intros. inversion H.
-  exploit function_ptr_translated; eauto.
-  intro Htf. destruct Htf as (tf & Htf & Hf).
-  exists (Callstate nil tf nil m0). split.
-  - econstructor.
-    + apply (Genv.init_mem_transf_partial TRANSL). auto.
-    + rewrite (match_program_main TRANSL).
-      rewrite symbols_preserved. eauto.
-    + apply Htf.
-    + rewrite <- H3. apply sig_preserved. apply Hf.
-  - constructor.
-    + constructor.
-    + apply Hf.
-    + constructor.
-    + apply Mem.extends_refl.
+  intros. inversion H as [b f m0 ge0 MEM SYM PTR SIG CALL].
+  exploit function_ptr_translated.
+  - apply PTR.
+  - 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.
+      * rewrite (match_program_main TRANSL).
+        rewrite symbols_preserved. apply SYM.
+      * apply TPTR.
+      * rewrite <- SIG. apply sig_preserved. apply TUN.
+    + apply match_states_call.
+      * apply list_forall2_nil.
+      * apply TUN.
+      * apply list_forall2_nil.
+      * apply Mem.extends_refl.
 Qed.
-  
+
 Lemma transf_final_states:
   forall (s1 : state)
   (s2 : state) (r : Integers.Int.int),
@@ -150,12 +263,22 @@ Lemma transf_final_states:
   final_state s1 r ->
   final_state s2 r.
 Proof.
-  intros s1 s2 r HM H1. inv H1. inv HM. inv STK. inv VAL. constructor.
+  (* rq: `inv` au lieu de `inversion` fait beaucoup de nettoyage dans les
+   * hypothèses, mais je sais pas trop ce que ça fait exactement *)
+  intros. inv H0. inv H. inv VAL. inversion STK. apply final_state_intro.
 Qed.
 
 (* `Lemma tunnel_step_correct` correspond au diagramme "option simulation" *)
+Lemma tunnel_step_correct:
+  forall st1 t st2, step ge st1 t st2 ->
+  forall st1' (MS: match_states st1 st1'),
+  (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.
+
 
-(*
 Theorem transf_program_correct:
   forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
 Proof.
@@ -163,8 +286,7 @@ Proof.
   apply senv_preserved.
   apply transf_initial_states.
   apply transf_final_states.
-  apply tunnel_step_correct.
+  exact tunnel_step_correct.
 Qed.
-*)
 
 End PRESERVATION.