1 files changed, 44 insertions, 0 deletions
diff --git a/backend/Tunnelingtyping.v b/backend/Tunnelingtyping.v
new file mode 100644
index 0000000..29b74f1
--- /dev/null
+++ b/backend/Tunnelingtyping.v
@@ -0,0 +1,44 @@
+(** Type preservation for the Tunneling pass *)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import AST.
+Require Import Values.
+Require Import Mem.
+Require Import Globalenvs.
+Require Import Op.
+Require Import Locations.
+Require Import LTL.
+Require Import LTLtyping.
+Require Import Tunneling.
+
+(** Tunneling preserves typing. *)
+
+Lemma wt_tunnel_block:
+  forall f b,
+  wt_block f b ->
+  wt_block (tunnel_function f) (tunnel_block f b).
+Proof.
+  induction 1; simpl; econstructor; eauto.
+Qed.
+
+Lemma wt_tunnel_function:
+  forall f, wt_function f -> wt_function (tunnel_function f).
+Proof.
+  unfold wt_function; intros until b.
+  simpl. rewrite PTree.gmap. unfold option_map. 
+  caseEq (fn_code f)!pc. intros b0 AT EQ. 
+  injection EQ; intros; subst b. 
+  apply wt_tunnel_block. eauto. 
+  intros; discriminate.
+Qed.
+
+Lemma program_typing_preserved:
+  forall (p: LTL.program),
+  wt_program p -> wt_program (tunnel_program p).
+Proof.
+  intros; red; intros.
+  generalize (transform_program_function tunnel_function p i f H0).
+  intros [f0 [IN TRANSF]].
+  subst f. apply wt_tunnel_function. eauto.
+Qed.