From 4a5f1db8abe7831649f6f15178958e0c57955a25 Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Wed, 4 Sep 2019 11:49:32 +0200
Subject: Duplicate: exec_function_internal

---
 backend/Duplicateproof.v | 36 ++++++++++++++++++++++++++++++++++--
 1 file changed, 34 insertions(+), 2 deletions(-)

(limited to 'backend/Duplicateproof.v')

diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v
index b30c2c14..69fc41ae 100644
--- a/backend/Duplicateproof.v
+++ b/backend/Duplicateproof.v
@@ -144,15 +144,47 @@ Theorem transf_final_states:
   forall s1 s2 r,
   match_states s1 s2 -> final_state s1 r -> final_state s2 r.
 Proof.
-Admitted.
+  intros. inv H0. inv H. inv STACKS. constructor.
+Qed.
 
 Theorem step_simulation:
   forall s1 t s1', step ge s1 t s1' ->
-  forall s2, match_states s1 s2 ->
+  forall s2 (MS: match_states s1 s2),
   exists s2',
      step tge s2 t s2'
   /\ match_states s1' s2'.
 Proof.
+  induction 1; intros; inv MS.
+(* Inop *)
+  - admit.
+(* Iop *)
+  - admit.
+(* Iload *)
+  - admit.
+(* Istore *)
+  - admit.
+(* Icall *)
+  - admit.
+(* Itailcall *)
+  - admit.
+(* Ibuiltin *)
+  - admit.
+(* Icond *)
+  - admit.
+(* Ijumptable *)
+  - admit.
+(* Ireturn *)
+  - admit.
+(* exec_function_internal *)
+  - monadInv TRANSF. eexists. split.
+    + econstructor. erewrite <- transf_function_fnstacksize; eauto.
+    + erewrite transf_function_fnentrypoint; eauto.
+      erewrite transf_function_fnparams; eauto.
+      econstructor; eauto. constructor.
+(* exec_function_external *)
+  - admit.
+(* exec_return *)
+  - admit.
 Admitted.
 
 Theorem transf_program_correct:
-- 
cgit