Library Tunnelingtyping

Type preservation for the Tunneling pass





Require Import Coqlib.

Require Import Maps.

Require Import UnionFind.

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.

Require Import Tunnelingproof.

Tunneling preserves typing.





Lemma branch_target_valid_1:

  forall f pc, wt_function f ->

  valid_successor f pc ->

  valid_successor f (branch_target f pc).






Lemma tunnel_valid_successor:

  forall f pc,

  valid_successor f pc -> valid_successor (tunnel_function f) pc.






Lemma branch_target_valid:

  forall f pc,

  wt_function f ->

  valid_successor f pc ->

  valid_successor (tunnel_function f) (branch_target f pc).






Lemma wt_tunnel_instr:

  forall f i,

  wt_function f ->

  wt_instr f i -> wt_instr (tunnel_function f) (tunnel_instr (record_gotos f) i).






Lemma wt_tunnel_function:

  forall f, wt_function f -> wt_function (tunnel_function f).






Lemma wt_tunnel_fundef:

  forall f, wt_fundef f -> wt_fundef (tunnel_fundef f).






Lemma program_typing_preserved:

  forall (p: LTL.program),

  wt_program p -> wt_program (tunnel_program p).