From 2b0c8766b4e99772777763e96e13747454672814 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Tue, 2 Jun 2020 17:21:06 +0100
Subject: Add proof for initial state

---
 src/translation/HTLgen.v      |  8 +++++++-
 src/translation/HTLgenproof.v | 22 ++++++++++++++++++++--
 2 files changed, 27 insertions(+), 3 deletions(-)

(limited to 'src')

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index aa965fc..78b1864 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -371,7 +371,13 @@ Definition max_state (f: function) : state :=
 Definition transl_module (f : function) : Errors.res module :=
   run_mon (max_state f) (transf_module f).
 
-Definition transl_fundef := transf_partial_fundef transl_module.
+Definition transl_fundef (f : RTL.fundef) : Errors.res HTL.fundef :=
+  match f with
+  | Internal f' =>
+    Errors.bind (transl_module f')
+                (fun f'' => Errors.OK (Internal f''))
+  | _ => Errors.Error (Errors.msg "External function could not be translated.")
+  end.
 
 (** Translation of a whole program. *)
 
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 5cdddb2..3dd645e 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -51,7 +51,11 @@ Inductive match_states : RTL.state -> HTL.state -> Prop :=
                  (HTL.State m st assoc)
 | match_returnstate : forall v v' stack m,
     val_value_lessdef v v' ->
-    match_states (RTL.Returnstate stack v m) (HTL.Returnstate v').
+    match_states (RTL.Returnstate stack v m) (HTL.Returnstate v')
+| match_initial_call :
+    forall f m m0 st
+    (TF : tr_module f m),
+      match_states (RTL.Callstate nil (AST.Internal f) nil m0) (HTL.State m st empty_assocmap).
 Hint Constructors match_states : htlproof.
 
 Definition match_prog (p: RTL.program) (tp: HTL.program) :=
@@ -450,7 +454,21 @@ Section CORRECTNESS.
       Smallstep.initial_state (RTL.semantics prog) s1 ->
       exists s2 : Smallstep.state (HTL.semantics tprog),
         Smallstep.initial_state (HTL.semantics tprog) s2 /\ match_states s1 s2.
-  Proof. Admitted.
+  Proof.
+    induction 1.
+    exploit function_ptr_translated; eauto.
+    intros [tf [A B]].
+    unfold transl_fundef, Errors.bind in B.
+    repeat (unfold_match B). inversion B. subst.
+    econstructor; split. econstructor.
+    apply (Genv.init_mem_transf_partial TRANSL); eauto.
+    replace (AST.prog_main tprog) with (AST.prog_main prog).
+    rewrite symbols_preserved; eauto.
+    symmetry; eapply Linking.match_program_main; eauto.
+    eexact A. trivial.
+    constructor.
+    apply transl_module_correct. auto.
+  Qed.
   Hint Resolve transl_initial_states : htlproof.
 
   Lemma transl_final_states :
-- 
cgit