(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(** Correctness proof for code linearization *)

Require Import FSets.
Require Import Coqlib Maps Ordered Errors Lattice Kildall Integers.
Require Import AST Linking.
Require Import Values Memory Events Globalenvs Smallstep.
Require Import Op Locations LTL Linear.
Require Import Linearize.

Module NodesetFacts := FSetFacts.Facts(Nodeset).

Definition match_prog (p: LTL.program) (tp: Linear.program) :=
  match_program (fun ctx f tf => transf_fundef f = OK tf) eq p tp.

Lemma transf_program_match:
  forall p tp, transf_program p = OK tp -> match_prog p tp.
Proof.
(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  intros. eapply match_transform_partial_program; eauto.
Qed.

Section LINEARIZATION.

Variable prog: LTL.program.
Variable tprog: Linear.program.

Hypothesis TRANSF: match_prog prog tprog.

Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Lemma functions_translated:
  forall v f,
  Genv.find_funct ge v = Some f ->
  exists tf,
  Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf.
Proof (Genv.find_funct_transf_partial TRANSF).

Lemma function_ptr_translated:
  forall v f,
  Genv.find_funct_ptr ge v = Some f ->
  exists tf,
  Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf.
Proof (Genv.find_funct_ptr_transf_partial TRANSF).

Lemma symbols_preserved:
  forall id,
  Genv.find_symbol tge id = Genv.find_symbol ge id.
Proof (Genv.find_symbol_transf_partial TRANSF).

Lemma senv_preserved:
  Senv.equiv ge tge.
Proof (Genv.senv_transf_partial TRANSF).

Lemma sig_preserved:
  forall f tf,
  transf_fundef f = OK tf ->
  Linear.funsig tf = LTL.funsig f.
Proof.
(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  unfold transf_fundef, transf_partial_fundef; intros.
(* Goal: @eq signature (funsig tf) (LTL.funsig f) *)
  destruct f. monadInv H. monadInv EQ. reflexivity.
(* Goal: @eq signature (funsig (@External function e)) (LTL.funsig (@External LTL.function e)) *)
  inv H. reflexivity.
Qed.

Lemma stacksize_preserved:
  forall f tf,
  transf_function f = OK tf ->
  Linear.fn_stacksize tf = LTL.fn_stacksize f.
Proof.
(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  intros. monadInv H. auto.
Qed.

Lemma find_function_translated:
  forall ros ls f,
  LTL.find_function ge ros ls = Some f ->
  exists tf,
  find_function tge ros ls = Some tf /\ transf_fundef f = OK tf.
Proof.
(* Goal: forall (ros : sum mreg ident) (ls : LTL.locset) (f : LTL.fundef) (_ : @eq (option LTL.fundef) (LTL.find_function ge ros ls) (@Some LTL.fundef f)), @ex fundef (fun tf : fundef => and (@eq (option fundef) (find_function tge ros ls) (@Some fundef tf)) (@eq (res fundef) (transf_fundef f) (@OK fundef tf))) *)
  unfold LTL.find_function; intros; destruct ros; simpl.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  apply functions_translated; auto.
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main LTL.fundef unit prog)) (@Some block b) *)
(* Goal: @eq signature (funsig tf) signature_main *)
(* Goal: match_states (LTL.Callstate (@nil LTL.stackframe) f (Locmap.init Vundef) m0) (Callstate (@nil stackframe) tf (Locmap.init Vundef) m0) *)
  rewrite symbols_preserved. destruct (Genv.find_symbol ge i).
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  apply function_ptr_translated; auto.
(* Goal: @eq code k (linearize_block b k') *)
  congruence.
Qed.

(** * Correctness of reachability analysis *)

(** The entry point of the function is reachable. *)

Lemma reachable_entrypoint:
  forall f, (reachable f)!!(f.(fn_entrypoint)) = true.
Proof.
(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  intros. unfold reachable.
(* Goal: forall (pc : positive) (pc' : node) (b : bblock) (_ : @eq (option bblock) (@PTree.get bblock pc (LTL.fn_code f)) (@Some bblock b)) (_ : @In node pc' (successors_block b)) (_ : @eq bool (@PMap.get bool pc match reachable_aux f with | Some rs => rs | None => @PMap.init bool true end) true), @eq bool (@PMap.get bool pc' match reachable_aux f with | Some rs => rs | None => @PMap.init bool true end) true *)
  caseEq (reachable_aux f).
  unfold reachable_aux; intros reach A.
  assert (LBoolean.ge reach!!(f.(fn_entrypoint)) true).
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  eapply DS.fixpoint_entry. eexact A. auto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  unfold LBoolean.ge in H. tauto.
(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  intros. apply PMap.gi.
Qed.

(** The successors of a reachable instruction are reachable. *)

Lemma reachable_successors:
  forall f pc pc' b,
  f.(LTL.fn_code)!pc = Some b -> In pc' (successors_block b) ->
  (reachable f)!!pc = true ->
  (reachable f)!!pc' = true.
Proof.
(* Goal: forall (pc : positive) (pc' : node) (b : bblock) (_ : @eq (option bblock) (@PTree.get bblock pc (LTL.fn_code f)) (@Some bblock b)) (_ : @In node pc' (successors_block b)) (_ : @eq bool (@PMap.get bool pc (reachable f)) true), @eq bool (@PMap.get bool pc' (reachable f)) true *)
  intro f. unfold reachable.
(* Goal: forall (pc : positive) (pc' : node) (b : bblock) (_ : @eq (option bblock) (@PTree.get bblock pc (LTL.fn_code f)) (@Some bblock b)) (_ : @In node pc' (successors_block b)) (_ : @eq bool (@PMap.get bool pc match reachable_aux f with | Some rs => rs | None => @PMap.init bool true end) true), @eq bool (@PMap.get bool pc' match reachable_aux f with | Some rs => rs | None => @PMap.init bool true end) true *)
  caseEq (reachable_aux f).
(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  unfold reachable_aux. intro reach; intros.
(* Goal: @eq bool (@PMap.get bool pc' reach) true *)
(* Goal: forall (_ : @eq (option (PMap.t bool)) (reachable_aux f) (@None (PMap.t bool))) (pc : positive) (pc' : node) (b : bblock) (_ : @eq (option bblock) (@PTree.get bblock pc (LTL.fn_code f)) (@Some bblock b)) (_ : @In node pc' (successors_block b)) (_ : @eq bool (@PMap.get bool pc (@PMap.init bool true)) true), @eq bool (@PMap.get bool pc' (@PMap.init bool true)) true *)
  assert (LBoolean.ge reach!!pc' reach!!pc).
(* Goal: LBoolean.ge (@PMap.get bool pc' reach) (@PMap.get bool pc reach) *)
(* Goal: @eq bool (@PMap.get bool pc' reach) true *)
(* Goal: forall (_ : @eq (option (PMap.t bool)) (reachable_aux f) (@None (PMap.t bool))) (pc : positive) (pc' : node) (b : bblock) (_ : @eq (option bblock) (@PTree.get bblock pc (LTL.fn_code f)) (@Some bblock b)) (_ : @In node pc' (successors_block b)) (_ : @eq bool (@PMap.get bool pc (@PMap.init bool true)) true), @eq bool (@PMap.get bool pc' (@PMap.init bool true)) true *)
  change (reach!!pc) with ((fun pc r => r) pc (reach!!pc)).
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  eapply DS.fixpoint_solution; eauto. intros; apply DS.L.eq_refl.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  elim H3; intro. congruence. auto.
(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  intros. apply PMap.gi.
Qed.

(** * Properties of node enumeration *)

(** An enumeration of CFG nodes is correct if the following conditions hold:
- All nodes for reachable basic blocks must be in the list.
- The list is without repetition (so that no code duplication occurs).

We prove that the result of the [enumerate] function satisfies both
conditions. *)

Lemma nodeset_of_list_correct:
  forall l s s',
  nodeset_of_list l s = OK s' ->
  list_norepet l
  /\ (forall pc, Nodeset.In pc s' <-> Nodeset.In pc s \/ In pc l)
  /\ (forall pc, In pc l -> ~Nodeset.In pc s).
Proof.
(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  induction l; simpl; intros.
(* Goal: final_state st2 r *)
  inv H. split. constructor. split. intro; tauto. intros; tauto.
(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  generalize H; clear H; caseEq (Nodeset.mem a s); intros.
(* Goal: final_state st2 r *)
  inv H0.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  exploit IHl; eauto. intros [A [B C]].
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  split. constructor; auto. red; intro. elim (C a H1). apply Nodeset.add_1. hnf. auto.
(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  split. intros. rewrite B. rewrite NodesetFacts.add_iff.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  unfold Nodeset.E.eq. unfold OrderedPositive.eq. tauto.
(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  intros. destruct H1. subst pc. rewrite NodesetFacts.not_mem_iff. auto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  generalize (C pc H1). rewrite NodesetFacts.add_iff. tauto.
Qed.

Lemma check_reachable_correct:
  forall f reach s pc i,
  check_reachable f reach s = true ->
  f.(LTL.fn_code)!pc = Some i ->
  reach!!pc = true ->
  Nodeset.In pc s.
Proof.
  intros f reach s.
  assert (forall l ok,
    List.fold_left (fun a p => check_reachable_aux reach s a (fst p) (snd p)) l ok = true ->
    ok = true /\
    (forall pc i,
     In (pc, i) l ->
     reach!!pc = true ->
     Nodeset.In pc s)).
(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  induction l; simpl; intros.
(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  split. auto. intros. destruct H0.
  destruct a as [pc1 i1]. simpl in H.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  exploit IHl; eauto. intros [A B].
  unfold check_reachable_aux in A.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  split. destruct (reach!!pc1). elim (andb_prop _ _ A). auto. auto.
(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  intros. destruct H0. inv H0. rewrite H1 in A. destruct (andb_prop _ _ A).
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  apply Nodeset.mem_2; auto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  eauto.

(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  intros pc i. unfold check_reachable. rewrite PTree.fold_spec. intros.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  exploit H; eauto. intros [A B]. eapply B; eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  apply PTree.elements_correct. eauto.
Qed.

Lemma enumerate_complete:
  forall f enum pc i,
  enumerate f = OK enum ->
  f.(LTL.fn_code)!pc = Some i ->
  (reachable f)!!pc = true ->
  In pc enum.
Proof.
(* Goal: forall (f : LTL.function) (enum : list node) (pc : positive) (i : bblock) (_ : @eq (res (list node)) (enumerate f) (@OK (list node) enum)) (_ : @eq (option bblock) (@PTree.get bblock pc (LTL.fn_code f)) (@Some bblock i)) (_ : @eq bool (@PMap.get bool pc (reachable f)) true), @In positive pc enum *)
  intros until i. unfold enumerate.
(* Goal: forall _ : @eq (res (list node)) (@bind Nodeset.t (list node) (nodeset_of_list (enumerate_aux f (reachable f)) Nodeset.empty) (fun s : Nodeset.t => if check_reachable f (reachable f) s then @OK (list node) (enumerate_aux f (reachable f)) else @Error (list node) (msg (String (Ascii.Ascii false false true true false false true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false true true true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false true false false true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false true false true true true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false true false true true true false false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true true false true true true false) (String (Ascii.Ascii false true false false true true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii false true true true false true true false) (String (Ascii.Ascii true true true false false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false true true true false true true false) (String (Ascii.Ascii true false true false true true true false) (String (Ascii.Ascii true false true true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false true false false true true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false false true false true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii false true true true false true true false) EmptyString))))))))))))))))))))))))))))))) (@OK (list node) enum), @list_norepet node enum *)
  set (reach := reachable f).
(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  intros. monadInv H.
(* Goal: @list_norepet node enum *)
  generalize EQ0; clear EQ0. caseEq (check_reachable f reach x); intros; inv EQ0.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  exploit check_reachable_correct; eauto. intro.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  exploit nodeset_of_list_correct; eauto. intros [A [B C]].
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  rewrite B in H2. destruct H2. elim (Nodeset.empty_1 H2). auto.
Qed.

Lemma enumerate_norepet:
  forall f enum,
  enumerate f = OK enum ->
  list_norepet enum.
Proof.
(* Goal: forall _ : @eq (res (list node)) (enumerate f) (@OK (list node) enum), @list_norepet node enum *)
  intros until enum. unfold enumerate.
(* Goal: forall _ : @eq (res (list node)) (@bind Nodeset.t (list node) (nodeset_of_list (enumerate_aux f (reachable f)) Nodeset.empty) (fun s : Nodeset.t => if check_reachable f (reachable f) s then @OK (list node) (enumerate_aux f (reachable f)) else @Error (list node) (msg (String (Ascii.Ascii false false true true false false true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false true true true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false true false false true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false true false true true true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false true false true true true false false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true true false true true true false) (String (Ascii.Ascii false true false false true true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii false true true true false true true false) (String (Ascii.Ascii true true true false false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false true true true false true true false) (String (Ascii.Ascii true false true false true true true false) (String (Ascii.Ascii true false true true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false true false false true true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false false true false true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii false true true true false true true false) EmptyString))))))))))))))))))))))))))))))) (@OK (list node) enum), @list_norepet node enum *)
  set (reach := reachable f).
(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  intros. monadInv H.
(* Goal: @list_norepet node enum *)
  generalize EQ0; clear EQ0. caseEq (check_reachable f reach x); intros; inv EQ0.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  exploit nodeset_of_list_correct; eauto. intros [A [B C]]. auto.
Qed.

(** * Properties related to labels *)

(** If labels are globally unique and the Linear code [c] contains
  a subsequence [Llabel lbl :: c1], then [find_label lbl c] returns [c1].
*)

Fixpoint unique_labels (c: code) : Prop :=
  match c with
  | nil => True
  | Llabel lbl :: c => ~(In (Llabel lbl) c) /\ unique_labels c
  | i :: c => unique_labels c
  end.

Lemma find_label_unique:
  forall lbl c1 c2 c3,
  is_tail (Llabel lbl :: c1) c2 ->
  unique_labels c2 ->
  find_label lbl c2 = Some c3 ->
  c1 = c3.
Proof.
(* Goal: forall (lbl : label) (c1 c2 : list instruction) (c3 : code) (_ : @is_tail instruction (@cons instruction (Llabel lbl) c1) c2) (_ : unique_labels c2) (_ : @eq (option code) (find_label lbl c2) (@Some code c3)), @eq (list instruction) c1 c3 *)
  induction c2.
(* Goal: forall (c2 : list instruction) (c3 : code) (s : list stackframe) (f : function) (sp : val) (ls : locset) (m : Mem.mem) (_ : @is_tail instruction (@nil instruction) c2) (_ : unique_labels c2) (_ : @eq bool (starts_with lbl (@nil instruction)) true) (_ : @eq (option code) (find_label lbl c2) (@Some code c3)), @plus genv state step tge (State s f sp (@nil instruction) ls m) E0 (State s f sp c3 ls m) *)
(* Goal: forall (c2 : list instruction) (c3 : code) (s : list stackframe) (f : function) (sp : val) (ls : locset) (m : Mem.mem) (_ : @is_tail instruction (@cons instruction a c1) c2) (_ : unique_labels c2) (_ : @eq bool (starts_with lbl (@cons instruction a c1)) true) (_ : @eq (option code) (find_label lbl c2) (@Some code c3)), @plus genv state step tge (State s f sp (@cons instruction a c1) ls m) E0 (State s f sp c3 ls m) *)
  simpl; intros; discriminate.
(* Goal: forall (c3 : code) (_ : @is_tail instruction (@cons instruction (Llabel lbl) c1) (@cons instruction a c2)) (_ : unique_labels (@cons instruction a c2)) (_ : @eq (option code) (find_label lbl (@cons instruction a c2)) (@Some code c3)), @eq (list instruction) c1 c3 *)
  intros c3 TAIL UNIQ. simpl.
(* Goal: forall _ : @eq (option code) (if is_label lbl a then @Some (list instruction) c2 else find_label lbl c2) (@Some code c3), @eq (list instruction) c1 c3 *)
  generalize (is_label_correct lbl a). case (is_label lbl a); intro ISLBL.
(* Goal: @eq code k (linearize_block b k') *)
  subst a. intro. inversion TAIL. congruence.
(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  elim UNIQ; intros. elim H4. apply is_tail_in with c1; auto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  inversion TAIL. congruence. apply IHc2. auto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  destruct a; simpl in UNIQ; tauto.
Qed.

(** Correctness of the [starts_with] test. *)

Lemma starts_with_correct:
  forall lbl c1 c2 c3 s f sp ls m,
  is_tail c1 c2 ->
  unique_labels c2 ->
  starts_with lbl c1 = true ->
  find_label lbl c2 = Some c3 ->
  plus step tge (State s f sp c1 ls m)
             E0 (State s f sp c3 ls m).
Proof.
(* Goal: forall (lbl : label) (c1 c2 : list instruction) (c3 : code) (s : list stackframe) (f : function) (sp : val) (ls : locset) (m : Mem.mem) (_ : @is_tail instruction c1 c2) (_ : unique_labels c2) (_ : @eq bool (starts_with lbl c1) true) (_ : @eq (option code) (find_label lbl c2) (@Some code c3)), @plus genv state step tge (State s f sp c1 ls m) E0 (State s f sp c3 ls m) *)
  induction c1.
(* Goal: forall (c2 : list instruction) (c3 : code) (s : list stackframe) (f : function) (sp : val) (ls : locset) (m : Mem.mem) (_ : @is_tail instruction (@nil instruction) c2) (_ : unique_labels c2) (_ : @eq bool (starts_with lbl (@nil instruction)) true) (_ : @eq (option code) (find_label lbl c2) (@Some code c3)), @plus genv state step tge (State s f sp (@nil instruction) ls m) E0 (State s f sp c3 ls m) *)
(* Goal: forall (c2 : list instruction) (c3 : code) (s : list stackframe) (f : function) (sp : val) (ls : locset) (m : Mem.mem) (_ : @is_tail instruction (@cons instruction a c1) c2) (_ : unique_labels c2) (_ : @eq bool (starts_with lbl (@cons instruction a c1)) true) (_ : @eq (option code) (find_label lbl c2) (@Some code c3)), @plus genv state step tge (State s f sp (@cons instruction a c1) ls m) E0 (State s f sp c3 ls m) *)
  simpl; intros; discriminate.
(* Goal: forall (c2 : list instruction) (c3 : code) (s : list stackframe) (f : function) (sp : val) (ls : locset) (m : Mem.mem) (_ : @is_tail instruction (@cons instruction a c1) c2) (_ : unique_labels c2) (_ : @eq bool (starts_with lbl (@cons instruction a c1)) true) (_ : @eq (option code) (find_label lbl c2) (@Some code c3)), @plus genv state step tge (State s f sp (@cons instruction a c1) ls m) E0 (State s f sp c3 ls m) *)
  simpl starts_with. destruct a; try (intros; discriminate).
(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  intros.
(* Goal: @plus genv state step tge (State s f sp (@cons instruction (Llabel l) c1) ls m) E0 (State s f sp c3 ls m) *)
  apply plus_left with E0 (State s f sp c1 ls m) E0.
(* Goal: @list_forall2 LTL.stackframe stackframe match_stackframes (@nil LTL.stackframe) (@nil stackframe) *)
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  simpl. constructor.
(* Goal: @star genv state step tge (State s f sp c1 ls m) E0 (State s f sp c3 ls m) *)
(* Goal: @eq trace E0 (Eapp E0 E0) *)
  destruct (peq lbl l).
(* Goal: @list_forall2 LTL.stackframe stackframe match_stackframes (@nil LTL.stackframe) (@nil stackframe) *)
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  subst l. replace c3 with c1. constructor.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  apply find_label_unique with lbl c2; auto.
(* Goal: @star genv state step tge (State s f sp c1 ls m) E0 (State s f sp c3 ls m) *)
(* Goal: @eq trace E0 (Eapp E0 E0) *)
  apply plus_star.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  apply IHc1 with c2; auto. eapply is_tail_cons_left; eauto.
(* Goal: @eq trace E0 (Eapp E0 E0) *)
  traceEq.
Qed.

(** Connection between [find_label] and linearization. *)

Lemma find_label_add_branch:
  forall lbl k s,
  find_label lbl (add_branch s k) = find_label lbl k.
Proof.
(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  intros. unfold add_branch. destruct (starts_with s k); auto.
Qed.

Lemma find_label_lin_block:
  forall lbl k b,
  find_label lbl (linearize_block b k) = find_label lbl k.
Proof.
(* Goal: forall _ : @eq (option code) (find_label lbl c1) (@Some code c2), @is_tail instruction c2 (@cons instruction a c1) *)
  intros lbl k. generalize (find_label_add_branch lbl k); intro.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  induction b; simpl; auto. destruct a; simpl; auto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  case (starts_with s1 k); simpl; auto.
Qed.

Remark linearize_body_cons:
  forall f pc enum,
  linearize_body f (pc :: enum) =
  match f.(LTL.fn_code)!pc with
  | None => linearize_body f enum
  | Some b => Llabel pc :: linearize_block b (linearize_body f enum)
  end.
Proof.
(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  intros. unfold linearize_body. rewrite list_fold_right_eq.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  unfold linearize_node. destruct (LTL.fn_code f)!pc; auto.
Qed.

Lemma find_label_lin_rec:
  forall f enum pc b,
  In pc enum ->
  f.(LTL.fn_code)!pc = Some b ->
  exists k, find_label pc (linearize_body f enum) = Some (linearize_block b k).
Proof.
(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  induction enum; intros.
(* Goal: @ex code (fun k : code => @eq (option code) (find_label pc (linearize_body f (@nil positive))) (@Some code (linearize_block b k))) *)
(* Goal: @ex code (fun k : code => @eq (option code) (find_label pc (linearize_body f (@cons positive a enum))) (@Some code (linearize_block b k))) *)
  elim H.
(* Goal: forall _ : @list_norepet node (@cons node a enum), unique_labels (linearize_body f (@cons node a enum)) *)
  rewrite linearize_body_cons.
(* Goal: @ex code (fun k : code => @eq (option code) (find_label pc match @PTree.get bblock a (LTL.fn_code f) with | Some b => @cons instruction (Llabel a) (linearize_block b (linearize_body f enum)) | None => linearize_body f enum end) (@Some code (linearize_block b k))) *)
  destruct (peq a pc).
(* Goal: @ex code (fun k : code => @eq (option code) (find_label pc match @PTree.get bblock a (LTL.fn_code f) with | Some b => @cons instruction (Llabel a) (linearize_block b (linearize_body f enum)) | None => linearize_body f enum end) (@Some code (linearize_block b k))) *)
(* Goal: @ex code (fun k : code => @eq (option code) (find_label pc match @PTree.get bblock a (LTL.fn_code f) with | Some b => @cons instruction (Llabel a) (linearize_block b (linearize_body f enum)) | None => linearize_body f enum end) (@Some code (linearize_block b k))) *)
  subst a. exists (linearize_body f enum).
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  rewrite H0. simpl. rewrite peq_true. auto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  assert (In pc enum). simpl in H. tauto.
(* Goal: @ex code (fun k : code => @eq (option code) (find_label pc match @PTree.get bblock a (LTL.fn_code f) with | Some b => @cons instruction (Llabel a) (linearize_block b (linearize_body f enum)) | None => linearize_body f enum end) (@Some code (linearize_block b k))) *)
  destruct (IHenum pc b H1 H0) as [k FIND].
(* Goal: @ex code (fun k : code => @eq (option code) (find_label pc match @PTree.get bblock a (LTL.fn_code f) with | Some b => @cons instruction (Llabel a) (linearize_block b (linearize_body f enum)) | None => linearize_body f enum end) (@Some code (linearize_block b k))) *)
  exists k. destruct (LTL.fn_code f)!a.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  simpl. rewrite peq_false. rewrite find_label_lin_block. auto. auto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  auto.
Qed.

Lemma find_label_lin:
  forall f tf pc b,
  transf_function f = OK tf ->
  f.(LTL.fn_code)!pc = Some b ->
  (reachable f)!!pc = true ->
  exists k,
  find_label pc (fn_code tf) = Some (linearize_block b k).
Proof.
(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  intros. monadInv H. simpl.
(* Goal: @ex code (fun k : code => @eq (option code) (find_label pc (add_branch (fn_entrypoint f) (linearize_body f x))) (@Some code (linearize_block b k))) *)
  rewrite find_label_add_branch. apply find_label_lin_rec.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  eapply enumerate_complete; eauto. auto.
Qed.

Lemma find_label_lin_inv:
  forall f tf pc b k,
  transf_function f = OK tf ->
  f.(LTL.fn_code)!pc = Some b ->
  (reachable f)!!pc = true ->
  find_label pc (fn_code tf) = Some k ->
  exists k', k = linearize_block b k'.
Proof.
(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  intros. exploit find_label_lin; eauto. intros [k' FIND].
(* Goal: @eq code k (linearize_block b k') *)
  exists k'. congruence.
Qed.

(** Unique label property for linearized code. *)

Lemma label_in_add_branch:
  forall lbl s k,
  In (Llabel lbl) (add_branch s k) -> In (Llabel lbl) k.
Proof.
(* Goal: @plus genv state step tge (State s tf sp (add_branch lbl k) ls m) E0 (State s tf sp c ls m) *)
  intros until k; unfold add_branch.
(* Goal: @eq code k (linearize_block b k') *)
  destruct (starts_with s k); simpl; intuition congruence.
Qed.

Lemma label_in_lin_block:
  forall lbl k b,
  In (Llabel lbl) (linearize_block b k) -> In (Llabel lbl) k.
Proof.
(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  induction b; simpl; intros. auto.
(* Goal: @In instruction (Llabel lbl) k *)
  destruct a; simpl in H; try (intuition congruence).
(* Goal: @eq code k (linearize_block b k') *)
  apply label_in_add_branch with s; intuition congruence.
(* Goal: @In positive pc enum *)
(* Goal: @ex code (fun k : code => @eq (option code) (find_label pc match @PTree.get bblock a (LTL.fn_code f) with | Some b => @cons instruction (Llabel a) (linearize_block b (linearize_body f enum)) | None => linearize_body f enum end) (@Some code (linearize_block b k))) *)
  destruct (starts_with s1 k); simpl in H.
(* Goal: @eq code k (linearize_block b k') *)
  apply label_in_add_branch with s1; intuition congruence.
(* Goal: @eq code k (linearize_block b k') *)
  apply label_in_add_branch with s2; intuition congruence.
Qed.

Lemma label_in_lin_rec:
  forall f lbl enum,
  In (Llabel lbl) (linearize_body f enum) -> In lbl enum.
Proof.
(* Goal: forall (f : LTL.function) (enum : list node) (_ : @list_norepet node enum), unique_labels (linearize_body f enum) *)
  induction enum.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  simpl; auto.
(* Goal: forall _ : @list_norepet node (@cons node a enum), unique_labels (linearize_body f (@cons node a enum)) *)
  rewrite linearize_body_cons. destruct (LTL.fn_code f)!a.
(* Goal: @eq code k (linearize_block b k') *)
  simpl. intros [A|B]. left; congruence.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  right. apply IHenum. eapply label_in_lin_block; eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  intro; right; auto.
Qed.

Lemma unique_labels_add_branch:
  forall lbl k,
  unique_labels k -> unique_labels (add_branch lbl k).
Proof.
(* Goal: @plus genv state step tge (State s tf sp (add_branch lbl k) ls m) E0 (State s tf sp c ls m) *)
  intros; unfold add_branch.
(* Goal: unique_labels (if starts_with lbl k then k else @cons instruction (Lgoto lbl) k) *)
  destruct (starts_with lbl k); simpl; intuition.
Qed.

Lemma unique_labels_lin_block:
  forall k b,
  unique_labels k -> unique_labels (linearize_block b k).
Proof.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  induction b; intros; simpl. auto.
(* Goal: unique_labels match a with | LTL.Lop op args res => @cons instruction (Lop op args res) (linearize_block b k) | LTL.Lload chunk addr args dst => @cons instruction (Lload chunk addr args dst) (linearize_block b k) | LTL.Lgetstack sl ofs ty dst => @cons instruction (Lgetstack sl ofs ty dst) (linearize_block b k) | LTL.Lsetstack src sl ofs ty => @cons instruction (Lsetstack src sl ofs ty) (linearize_block b k) | LTL.Lstore chunk addr args src => @cons instruction (Lstore chunk addr args src) (linearize_block b k) | LTL.Lcall sig ros => @cons instruction (Lcall sig ros) (linearize_block b k) | LTL.Ltailcall sig ros => @cons instruction (Ltailcall sig ros) k | LTL.Lbuiltin ef args res => @cons instruction (Lbuiltin ef args res) (linearize_block b k) | Lbranch s => add_branch s k | LTL.Lcond cond args s1 s2 => if starts_with s1 k then @cons instruction (Lcond (negate_condition cond) args s2) (add_branch s1 k) else @cons instruction (Lcond cond args s1) (add_branch s2 k) | LTL.Ljumptable arg tbl => @cons instruction (Ljumptable arg tbl) k | LTL.Lreturn => @cons instruction Lreturn k end *)
  destruct a; auto; try (apply unique_labels_add_branch; auto).
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  case (starts_with s1 k); simpl; apply unique_labels_add_branch; auto.
Qed.

Lemma unique_labels_lin_rec:
  forall f enum,
  list_norepet enum ->
  unique_labels (linearize_body f enum).
Proof.
(* Goal: forall (f : LTL.function) (enum : list node) (_ : @list_norepet node enum), unique_labels (linearize_body f enum) *)
  induction enum.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  simpl; auto.
(* Goal: forall _ : @list_norepet node (@cons node a enum), unique_labels (linearize_body f (@cons node a enum)) *)
  rewrite linearize_body_cons.
(* Goal: forall _ : @eq (option code) (find_label lbl c1) (@Some code c2), @is_tail instruction c2 (@cons instruction a c1) *)
  intro. destruct (LTL.fn_code f)!a.
(* Goal: and (not (@In instruction (Llabel a) (linearize_block b (linearize_body f enum)))) (unique_labels (linearize_block b (linearize_body f enum))) *)
(* Goal: unique_labels (linearize_body f enum) *)
  simpl. split. red. intro. inversion H. elim H3.
(* Goal: @In node a enum *)
(* Goal: unique_labels (linearize_block b (linearize_body f enum)) *)
(* Goal: unique_labels (linearize_body f enum) *)
  apply label_in_lin_rec with f.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  apply label_in_lin_block with b. auto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  apply unique_labels_lin_block. apply IHenum. inversion H; auto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  apply IHenum. inversion H; auto.
Qed.

Lemma unique_labels_transf_function:
  forall f tf,
  transf_function f = OK tf ->
  unique_labels (fn_code tf).
Proof.
(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  intros. monadInv H. simpl.
(* Goal: unique_labels (add_branch (fn_entrypoint f) (linearize_body f x)) *)
  apply unique_labels_add_branch.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  apply unique_labels_lin_rec. eapply enumerate_norepet; eauto.
Qed.

(** Correctness of [add_branch]. *)

Lemma is_tail_find_label:
  forall lbl c2 c1,
  find_label lbl c1 = Some c2 -> is_tail c2 c1.
Proof.
(* Goal: unique_labels (fn_code (mkfunction (LTL.fn_sig f) (LTL.fn_stacksize f) (add_branch (fn_entrypoint f) (linearize_body f x)))) *)
  induction c1; simpl.
(* Goal: forall _ : @eq (option code) (@None code) (@Some code c2), @is_tail instruction c2 (@nil instruction) *)
(* Goal: forall _ : @eq (option code) (if is_label lbl a then @Some (list instruction) c1 else find_label lbl c1) (@Some code c2), @is_tail instruction c2 (@cons instruction a c1) *)
  intros; discriminate.
(* Goal: forall _ : @eq (option code) (find_label lbl c1) (@Some code c2), @is_tail instruction c2 (@cons instruction a c1) *)
  case (is_label lbl a). intro. injection H; intro. subst c2.
(* Goal: @list_forall2 LTL.stackframe stackframe match_stackframes (@nil LTL.stackframe) (@nil stackframe) *)
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  constructor. constructor.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  intro. constructor. auto.
Qed.

Lemma is_tail_add_branch:
  forall lbl c1 c2, is_tail (add_branch lbl c1) c2 -> is_tail c1 c2.
Proof.
(* Goal: @plus genv state step tge (State s tf sp (add_branch lbl k) ls m) E0 (State s tf sp c ls m) *)
  intros until c2. unfold add_branch. destruct (starts_with lbl c1).
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  auto. eauto with coqlib.
Qed.

Lemma is_tail_lin_block:
  forall b c1 c2,
  is_tail (linearize_block b c1) c2 -> is_tail c1 c2.
Proof.
(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  induction b; simpl; intros.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  auto.
(* Goal: forall _ : @is_tail instruction (@cons instruction (Lgoto lbl) c1) c2, @is_tail instruction c1 c2 *)
  destruct a; eauto with coqlib.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  eapply is_tail_add_branch; eauto.
(* Goal: forall _ : @is_tail instruction (@cons instruction (Lgoto lbl) c1) c2, @is_tail instruction c1 c2 *)
  destruct (starts_with s1 c1); eapply is_tail_add_branch; eauto with coqlib.
Qed.

Lemma add_branch_correct:
  forall lbl c k s f tf sp ls m,
  transf_function f = OK tf ->
  is_tail k tf.(fn_code) ->
  find_label lbl tf.(fn_code) = Some c ->
  plus step tge (State s tf sp (add_branch lbl k) ls m)
             E0 (State s tf sp c ls m).
Proof.
(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  intros. unfold add_branch.
(* Goal: @plus genv state step tge (State s tf sp (if starts_with lbl k then k else @cons instruction (Lgoto lbl) k) ls m) E0 (State s tf sp c ls m) *)
  caseEq (starts_with lbl k); intro SW.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  eapply starts_with_correct; eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  eapply unique_labels_transf_function; eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  apply plus_one. apply exec_Lgoto. auto.
Qed.

(** * Correctness of linearization *)

(** The proof of semantic preservation is a simulation argument of the "star" kind:
<<
           st1 --------------- st2
            |                   |
           t|                  t| + or ( 0 \/ |st1'| < |st1| )
            |                   |
            v                   v
           st1'--------------- st2'
>>
  The invariant (horizontal lines above) is the [match_states]
  predicate defined below.  It captures the fact that the flow
  of data is the same in the source and linearized codes.
  Moreover, whenever the source state is at node [pc] in its
  control-flow graph, the transformed state is at a code
  sequence [c] that starts with the label [pc]. *)

Inductive match_stackframes: LTL.stackframe -> Linear.stackframe -> Prop :=
  | match_stackframe_intro:
      forall f sp bb ls tf c,
      transf_function f = OK tf ->
      (forall pc, In pc (successors_block bb) -> (reachable f)!!pc = true) ->
      is_tail c tf.(fn_code) ->
      match_stackframes
        (LTL.Stackframe f sp ls bb)
        (Linear.Stackframe tf sp ls (linearize_block bb c)).

Inductive match_states: LTL.state -> Linear.state -> Prop :=
  | match_states_add_branch:
      forall s f sp pc ls m tf ts c
        (STACKS: list_forall2 match_stackframes s ts)
        (TRF: transf_function f = OK tf)
        (REACH: (reachable f)!!pc = true)
        (TAIL: is_tail c tf.(fn_code)),
      match_states (LTL.State s f sp pc ls m)
                   (Linear.State ts tf sp (add_branch pc c) ls m)
  | match_states_cond_taken:
      forall s f sp pc ls m tf ts cond args c
        (STACKS: list_forall2 match_stackframes s ts)
        (TRF: transf_function f = OK tf)
        (REACH: (reachable f)!!pc = true)
        (JUMP: eval_condition cond (reglist ls args) m = Some true),
      match_states (LTL.State s f sp pc (undef_regs (destroyed_by_cond cond) ls) m)
                   (Linear.State ts tf sp (Lcond cond args pc :: c) ls m)
  | match_states_jumptable:
      forall s f sp pc ls m tf ts arg tbl c n
        (STACKS: list_forall2 match_stackframes s ts)
        (TRF: transf_function f = OK tf)
        (REACH: (reachable f)!!pc = true)
        (ARG: ls (R arg) = Vint n)
        (JUMP: list_nth_z tbl (Int.unsigned n) = Some pc),
      match_states (LTL.State s f sp pc (undef_regs destroyed_by_jumptable ls) m)
                   (Linear.State ts tf sp (Ljumptable arg tbl :: c) ls m)
  | match_states_block:
      forall s f sp bb ls m tf ts c
        (STACKS: list_forall2 match_stackframes s ts)
        (TRF: transf_function f = OK tf)
        (REACH: forall pc, In pc (successors_block bb) -> (reachable f)!!pc = true)
        (TAIL: is_tail c tf.(fn_code)),
      match_states (LTL.Block s f sp bb ls m)
                   (Linear.State ts tf sp (linearize_block bb c) ls m)
  | match_states_call:
      forall s f ls m tf ts,
      list_forall2 match_stackframes s ts ->
      transf_fundef f = OK tf ->
      match_states (LTL.Callstate s f ls m)
                   (Linear.Callstate ts tf ls m)
  | match_states_return:
      forall s ls m ts,
      list_forall2 match_stackframes s ts ->
      match_states (LTL.Returnstate s ls m)
                   (Linear.Returnstate ts ls m).

Definition measure (S: LTL.state) : nat :=
  match S with
  | LTL.State s f sp pc ls m => 0%nat
  | LTL.Block s f sp bb ls m => 1%nat
  | _ => 0%nat
  end.

Remark match_parent_locset:
  forall s ts, list_forall2 match_stackframes s ts -> parent_locset ts = LTL.parent_locset s.
Proof.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  induction 1; simpl. auto. inv H; auto.
Qed.

Theorem transf_step_correct:
  forall s1 t s2, LTL.step ge s1 t s2 ->
  forall s1' (MS: match_states s1 s1'),
  (exists s2', plus Linear.step tge s1' t s2' /\ match_states s2 s2')
  \/ (measure s2 < measure s1 /\ t = E0 /\ match_states s2 s1')%nat.
Proof.
  induction 1; intros; try (inv MS).

  (* start of block, at an [add_branch] *)
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  exploit find_label_lin; eauto. intros [k F].
(* Goal: and (not (@In instruction (Llabel a) (linearize_block b (linearize_body f enum)))) (unique_labels (linearize_block b (linearize_body f enum))) *)
(* Goal: unique_labels (linearize_body f enum) *)
  left; econstructor; split.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  eapply add_branch_correct; eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  econstructor; eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  intros; eapply reachable_successors; eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  eapply is_tail_lin_block; eauto. eapply is_tail_find_label; eauto.

  (* start of block, target of an [Lcond] *)
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  exploit find_label_lin; eauto. intros [k F].
(* Goal: and (not (@In instruction (Llabel a) (linearize_block b (linearize_body f enum)))) (unique_labels (linearize_block b (linearize_body f enum))) *)
(* Goal: unique_labels (linearize_body f enum) *)
  left; econstructor; split.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  apply plus_one. eapply exec_Lcond_true; eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  econstructor; eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  intros; eapply reachable_successors; eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  eapply is_tail_lin_block; eauto. eapply is_tail_find_label; eauto.

  (* start of block, target of an [Ljumptable] *)
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  exploit find_label_lin; eauto. intros [k F].
(* Goal: and (not (@In instruction (Llabel a) (linearize_block b (linearize_body f enum)))) (unique_labels (linearize_block b (linearize_body f enum))) *)
(* Goal: unique_labels (linearize_body f enum) *)
  left; econstructor; split.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  apply plus_one. eapply exec_Ljumptable; eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  econstructor; eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  intros; eapply reachable_successors; eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  eapply is_tail_lin_block; eauto. eapply is_tail_find_label; eauto.

  (* Lop *)
(* Goal: and (not (@In instruction (Llabel a) (linearize_block b (linearize_body f enum)))) (unique_labels (linearize_block b (linearize_body f enum))) *)
(* Goal: unique_labels (linearize_body f enum) *)
  left; econstructor; split. simpl.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  apply plus_one. econstructor; eauto.
  instantiate (1 := v); rewrite <- H; apply eval_operation_preserved.
  exact symbols_preserved.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  econstructor; eauto.

  (* Lload *)
(* Goal: and (not (@In instruction (Llabel a) (linearize_block b (linearize_body f enum)))) (unique_labels (linearize_block b (linearize_body f enum))) *)
(* Goal: unique_labels (linearize_body f enum) *)
  left; econstructor; split. simpl.
(* Goal: @list_forall2 LTL.stackframe stackframe match_stackframes (@nil LTL.stackframe) (@nil stackframe) *)
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  apply plus_one. econstructor.
  instantiate (1 := a). rewrite <- H; apply eval_addressing_preserved.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  exact symbols_preserved. eauto. eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  econstructor; eauto.

  (* Lgetstack *)
(* Goal: and (not (@In instruction (Llabel a) (linearize_block b (linearize_body f enum)))) (unique_labels (linearize_block b (linearize_body f enum))) *)
(* Goal: unique_labels (linearize_body f enum) *)
  left; econstructor; split. simpl.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  apply plus_one. econstructor; eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  econstructor; eauto.

  (* Lsetstack *)
(* Goal: and (not (@In instruction (Llabel a) (linearize_block b (linearize_body f enum)))) (unique_labels (linearize_block b (linearize_body f enum))) *)
(* Goal: unique_labels (linearize_body f enum) *)
  left; econstructor; split. simpl.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  apply plus_one. econstructor; eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  econstructor; eauto.

  (* Lstore *)
(* Goal: and (not (@In instruction (Llabel a) (linearize_block b (linearize_body f enum)))) (unique_labels (linearize_block b (linearize_body f enum))) *)
(* Goal: unique_labels (linearize_body f enum) *)
  left; econstructor; split. simpl.
(* Goal: @list_forall2 LTL.stackframe stackframe match_stackframes (@nil LTL.stackframe) (@nil stackframe) *)
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  apply plus_one. econstructor.
  instantiate (1 := a). rewrite <- H; apply eval_addressing_preserved.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  exact symbols_preserved. eauto. eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  econstructor; eauto.

  (* Lcall *)
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  exploit find_function_translated; eauto. intros [tfd [A B]].
(* Goal: and (not (@In instruction (Llabel a) (linearize_block b (linearize_body f enum)))) (unique_labels (linearize_block b (linearize_body f enum))) *)
(* Goal: unique_labels (linearize_body f enum) *)
  left; econstructor; split. simpl.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  apply plus_one. econstructor; eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  symmetry; eapply sig_preserved; eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  econstructor; eauto. constructor; auto. econstructor; eauto.

  (* Ltailcall *)
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  exploit find_function_translated; eauto. intros [tfd [A B]].
(* Goal: and (not (@In instruction (Llabel a) (linearize_block b (linearize_body f enum)))) (unique_labels (linearize_block b (linearize_body f enum))) *)
(* Goal: unique_labels (linearize_body f enum) *)
  left; econstructor; split. simpl.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  apply plus_one. econstructor; eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  rewrite (match_parent_locset _ _ STACKS). eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  symmetry; eapply sig_preserved; eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  rewrite (stacksize_preserved _ _ TRF); eauto.
  rewrite (match_parent_locset _ _ STACKS).
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  econstructor; eauto.

  (* Lbuiltin *)
(* Goal: and (not (@In instruction (Llabel a) (linearize_block b (linearize_body f enum)))) (unique_labels (linearize_block b (linearize_body f enum))) *)
(* Goal: unique_labels (linearize_body f enum) *)
  left; econstructor; split. simpl.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  apply plus_one. eapply exec_Lbuiltin; eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  econstructor; eauto.

  (* Lbranch *)
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  assert ((reachable f)!!pc = true). apply REACH; simpl; auto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  right; split. simpl; omega. split. auto. simpl. econstructor; eauto.

  (* Lcond *)
  assert (REACH1: (reachable f)!!pc1 = true) by (apply REACH; simpl; auto).
  assert (REACH2: (reachable f)!!pc2 = true) by (apply REACH; simpl; auto).
  simpl linearize_block.
  destruct (starts_with pc1 c).
  (* branch if cond is false *)
  assert (DC: destroyed_by_cond (negate_condition cond) = destroyed_by_cond cond).
(* Goal: @eq signature (funsig (@External function e)) (LTL.funsig (@External LTL.function e)) *)
    destruct cond; reflexivity.
  destruct b.
  (* cond is true: no branch *)
(* Goal: and (not (@In instruction (Llabel a) (linearize_block b (linearize_body f enum)))) (unique_labels (linearize_block b (linearize_body f enum))) *)
(* Goal: unique_labels (linearize_body f enum) *)
  left; econstructor; split.
(* Goal: @plus genv state step tge (State s tf sp (@cons instruction (Lgoto lbl) k) ls m) E0 (State s tf sp c ls m) *)
  apply plus_one. eapply exec_Lcond_false.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  rewrite eval_negate_condition. rewrite H. auto. eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  rewrite DC. econstructor; eauto.
  (* cond is false: branch is taken *)
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  right; split. simpl; omega. split. auto.  rewrite <- DC. econstructor; eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  rewrite eval_negate_condition. rewrite H. auto.
  (* branch if cond is true *)
  destruct b.
  (* cond is true: branch is taken *)
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  right; split. simpl; omega. split. auto. econstructor; eauto.
  (* cond is false: no branch *)
(* Goal: and (not (@In instruction (Llabel a) (linearize_block b (linearize_body f enum)))) (unique_labels (linearize_block b (linearize_body f enum))) *)
(* Goal: unique_labels (linearize_body f enum) *)
  left; econstructor; split.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  apply plus_one. eapply exec_Lcond_false. eauto. eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  econstructor; eauto.

  (* Ljumptable *)
  assert (REACH': (reachable f)!!pc = true).
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
    apply REACH. simpl. eapply list_nth_z_in; eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  right; split. simpl; omega. split. auto. econstructor; eauto.

  (* Lreturn *)
(* Goal: and (not (@In instruction (Llabel a) (linearize_block b (linearize_body f enum)))) (unique_labels (linearize_block b (linearize_body f enum))) *)
(* Goal: unique_labels (linearize_body f enum) *)
  left; econstructor; split.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  simpl. apply plus_one. econstructor; eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  rewrite (stacksize_preserved _ _ TRF). eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  rewrite (match_parent_locset _ _ STACKS). econstructor; eauto.

  (* internal functions *)
  assert (REACH: (reachable f)!!(LTL.fn_entrypoint f) = true).
    apply reachable_entrypoint.
  monadInv H7.
(* Goal: and (not (@In instruction (Llabel a) (linearize_block b (linearize_body f enum)))) (unique_labels (linearize_block b (linearize_body f enum))) *)
(* Goal: unique_labels (linearize_body f enum) *)
  left; econstructor; split.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  apply plus_one. eapply exec_function_internal; eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  rewrite (stacksize_preserved _ _ EQ). eauto.
(* Goal: unique_labels (fn_code (mkfunction (LTL.fn_sig f) (LTL.fn_stacksize f) (add_branch (fn_entrypoint f) (linearize_body f x)))) *)
  generalize EQ; intro EQ'; monadInv EQ'. simpl.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  econstructor; eauto. simpl. eapply is_tail_add_branch. constructor.

  (* external function *)
(* Goal: and (not (@In instruction (Llabel a) (linearize_block b (linearize_body f enum)))) (unique_labels (linearize_block b (linearize_body f enum))) *)
(* Goal: unique_labels (linearize_body f enum) *)
  monadInv H8. left; econstructor; split.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  apply plus_one. eapply exec_function_external; eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  econstructor; eauto.

  (* return *)
  inv H3. inv H1.
(* Goal: and (not (@In instruction (Llabel a) (linearize_block b (linearize_body f enum)))) (unique_labels (linearize_block b (linearize_body f enum))) *)
(* Goal: unique_labels (linearize_body f enum) *)
  left; econstructor; split.
(* Goal: @list_forall2 LTL.stackframe stackframe match_stackframes (@nil LTL.stackframe) (@nil stackframe) *)
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  apply plus_one. econstructor.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  econstructor; eauto.
Qed.

Lemma transf_initial_states:
  forall st1, LTL.initial_state prog st1 ->
  exists st2, Linear.initial_state tprog st2 /\ match_states st1 st2.
Proof.
(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  intros. inversion H.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  exploit function_ptr_translated; eauto. intros [tf [A B]].
(* Goal: and (not (@In instruction (Llabel a) (linearize_block b (linearize_body f enum)))) (unique_labels (linearize_block b (linearize_body f enum))) *)
(* Goal: unique_labels (linearize_body f enum) *)
  exists (Callstate nil tf (Locmap.init Vundef) m0); split.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  econstructor; eauto. eapply (Genv.init_mem_transf_partial TRANSF); eauto.
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig tf) signature_main *)
(* Goal: match_states (LTL.Callstate (@nil LTL.stackframe) f (Locmap.init Vundef) m0) (Callstate (@nil stackframe) tf (Locmap.init Vundef) m0) *)
  rewrite (match_program_main TRANSF).
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  rewrite symbols_preserved. eauto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  rewrite <- H3. apply sig_preserved. auto.
(* Goal: @eq (res fundef) (transf_fundef f) (@OK fundef tf) *)
  constructor. constructor. auto.
Qed.

Lemma transf_final_states:
  forall st1 st2 r,
  match_states st1 st2 -> LTL.final_state st1 r -> Linear.final_state st2 r.
Proof.
(* Goal: forall (st1 : LTL.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : LTL.final_state st1 r), final_state st2 r *)
  intros. inv H0. inv H. inv H5. econstructor; eauto.
Qed.

Theorem transf_program_correct:
  forward_simulation (LTL.semantics prog) (Linear.semantics tprog).
Proof.
  eapply forward_simulation_star.
  apply senv_preserved.
  eexact transf_initial_states.
  eexact transf_final_states.
  eexact transf_step_correct.
Qed.

End LINEARIZATION.
