Library Linearizetyping

Type preservation for the Linearize pass





Require Import Coqlib.

Require Import Maps.

Require Import Errors.

Require Import AST.

Require Import Op.

Require Import Locations.

Require Import LTL.

Require Import LTLtyping.

Require Import LTLin.

Require Import Linearize.

Require Import LTLintyping.

Require Import Conventions.

Type preservation for the linearization pass





Lemma wt_add_instr:

  forall f i k, wt_instr f i -> wt_code f k -> wt_code f (i :: k).






Lemma wt_add_branch:

  forall f s k, wt_code f k -> wt_code f (add_branch s k).






Lemma wt_linearize_instr:

  forall f instr,

  LTLtyping.wt_instr f instr ->

  forall k,

  wt_code f.(LTL.fn_sig) k ->

  wt_code f.(LTL.fn_sig) (linearize_instr instr k).






Lemma wt_linearize_body:

  forall f,

  (forall pc instr, 

     f.(LTL.fn_code)!pc = Some instr -> LTLtyping.wt_instr f instr) ->

  forall enum,

  wt_code f.(LTL.fn_sig) (linearize_body f enum).






Lemma wt_transf_function:

  forall f tf,

  LTLtyping.wt_function f ->

  transf_function f = OK tf ->

  wt_function tf.






Lemma wt_transf_fundef:

  forall f tf,

  LTLtyping.wt_fundef f ->

  transf_fundef f = OK tf ->

  wt_fundef tf.






Lemma program_typing_preserved:

  forall (p: LTL.program) (tp: LTLin.program),

  LTLtyping.wt_program p ->

  transf_program p = OK tp ->

  LTLintyping.wt_program tp.