diff options
Diffstat (limited to 'backend/RTLgenproof1.v')
| -rw-r--r-- | backend/RTLgenproof1.v | 1463 |
1 files changed, 1463 insertions, 0 deletions
diff --git a/backend/RTLgenproof1.v b/backend/RTLgenproof1.v new file mode 100644 index 0000000..4a8ad43 --- /dev/null +++ b/backend/RTLgenproof1.v @@ -0,0 +1,1463 @@ +(** Correctness proof for RTL generation: auxiliary results. *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Values. +Require Import Mem. +Require Import Globalenvs. +Require Import Op. +Require Import Registers. +Require Import Cminor. +Require Import RTL. +Require Import RTLgen. + +(** * Reasoning about monadic computations *) + +(** The tactics below simplify hypotheses of the form [f ... = OK x s] + where [f] is a monadic computation. For instance, the hypothesis + [(do x <- a; b) s = OK y s'] will generate the additional witnesses + [x], [s1] and the additional hypotheses + [a s = OK x s1] and [b x s1 = OK y s'], reflecting the fact that + both monadic computations [a] and [b] succeeded. +*) + +Ltac monadSimpl1 := + match goal with + | [ |- (bind ?F ?G ?S = OK ?X ?S') -> _ ] => + unfold bind at 1; + generalize (refl_equal (F S)); + pattern (F S) at -1 in |- *; + case (F S); + [ intro; intro; discriminate + | (let s := fresh "s" in + (let EQ := fresh "EQ" in + (intro; intros s EQ; + try monadSimpl1))) ] + | [ |- (bind2 ?F ?G ?S = OK ?X ?S') -> _ ] => + unfold bind2 at 1; unfold bind at 1; + generalize (refl_equal (F S)); + pattern (F S) at -1 in |- *; + case (F S); + [ intro; intro; discriminate + | let xy := fresh "xy" in + (let x := fresh "x" in + (let y := fresh "y" in + (let s := fresh "s" in + (let EQ := fresh "EQ" in + (intros xy s EQ; destruct xy as [x y]; simpl; + try monadSimpl1))))) ] + | [ |- (error _ _ = OK _ _) -> _ ] => + unfold error; monadSimpl1 + | [ |- (ret _ _ = OK _ _) -> _ ] => + unfold ret; monadSimpl1 + | [ |- (Error _ = OK _ _) -> _ ] => + intro; discriminate + | [ |- (OK _ _ = OK _ _) -> _ ] => + let h := fresh "H" in + (intro h; injection h; intro; intro; clear h) + end. + +Ltac monadSimpl := + match goal with + | [ |- (bind ?F ?G ?S = OK ?X ?S') -> _ ] => monadSimpl1 + | [ |- (bind2 ?F ?G ?S = OK ?X ?S') -> _ ] => monadSimpl1 + | [ |- (error _ _ = OK _ _) -> _ ] => monadSimpl1 + | [ |- (ret _ _ = OK _ _) -> _ ] => monadSimpl1 + | [ |- (Error _ = OK _ _) -> _ ] => monadSimpl1 + | [ |- (OK _ _ = OK _ _) -> _ ] => monadSimpl1 + | [ |- (?F _ _ _ _ _ _ _ = OK _ _) -> _ ] => unfold F; monadSimpl1 + | [ |- (?F _ _ _ _ _ _ = OK _ _) -> _ ] => unfold F; monadSimpl1 + | [ |- (?F _ _ _ _ _ = OK _ _) -> _ ] => unfold F; monadSimpl1 + | [ |- (?F _ _ _ _ = OK _ _) -> _ ] => unfold F; monadSimpl1 + | [ |- (?F _ _ _ = OK _ _) -> _ ] => unfold F; monadSimpl1 + | [ |- (?F _ _ = OK _ _) -> _ ] => unfold F; monadSimpl1 + | [ |- (?F _ = OK _ _) -> _ ] => unfold F; monadSimpl1 + end. + +Ltac monadInv H := + generalize H; monadSimpl. + +(** * Monotonicity properties of the state *) + +(** Operations over the global state satisfy a crucial monotonicity property: + nodes are only added to the CFG, but never removed nor their instructions + changed; similarly, fresh nodes and fresh registers are only consumed, + but never reused. This property is captured by the following predicate + over states, which we show is a partial order. *) + +Inductive state_incr: state -> state -> Prop := + state_incr_intro: + forall (s1 s2: state), + Ple s1.(st_nextnode) s2.(st_nextnode) -> + Ple s1.(st_nextreg) s2.(st_nextreg) -> + (forall pc, Plt pc s1.(st_nextnode) -> s2.(st_code)!pc = s1.(st_code)!pc) -> + state_incr s1 s2. + +Lemma instr_at_incr: + forall s1 s2 n i, + s1.(st_code)!n = i -> i <> None -> state_incr s1 s2 -> + s2.(st_code)!n = i. +Proof. + intros. inversion H1. + rewrite <- H. apply H4. elim (st_wf s1 n); intro. + assumption. elim H0. congruence. +Qed. + +Lemma state_incr_refl: + forall s, state_incr s s. +Proof. + intros. apply state_incr_intro. + apply Ple_refl. apply Ple_refl. intros; auto. +Qed. +Hint Resolve state_incr_refl: rtlg. + +Lemma state_incr_trans: + forall s1 s2 s3, state_incr s1 s2 -> state_incr s2 s3 -> state_incr s1 s3. +Proof. + intros. inversion H. inversion H0. apply state_incr_intro. + apply Ple_trans with (st_nextnode s2); assumption. + apply Ple_trans with (st_nextreg s2); assumption. + intros. transitivity (s2.(st_code)!pc). + apply H8. apply Plt_Ple_trans with s1.(st_nextnode); auto. + apply H3; auto. +Qed. +Hint Resolve state_incr_trans: rtlg. + +Lemma state_incr_trans2: + forall s1 s2 s3 s4, + state_incr s1 s2 -> state_incr s2 s3 -> state_incr s3 s4 -> + state_incr s1 s4. +Proof. + intros; eauto with rtlg. +Qed. + +Lemma state_incr_trans3: + forall s1 s2 s3 s4 s5, + state_incr s1 s2 -> state_incr s2 s3 -> state_incr s3 s4 -> state_incr s4 s5 -> + state_incr s1 s5. +Proof. + intros; eauto with rtlg. +Qed. + +Lemma state_incr_trans4: + forall s1 s2 s3 s4 s5 s6, + state_incr s1 s2 -> state_incr s2 s3 -> state_incr s3 s4 -> + state_incr s4 s5 -> state_incr s5 s6 -> + state_incr s1 s6. +Proof. + intros; eauto with rtlg. +Qed. + +Lemma state_incr_trans5: + forall s1 s2 s3 s4 s5 s6 s7, + state_incr s1 s2 -> state_incr s2 s3 -> state_incr s3 s4 -> + state_incr s4 s5 -> state_incr s5 s6 -> state_incr s6 s7 -> + state_incr s1 s7. +Proof. + intros; eauto 6 with rtlg. +Qed. + +Lemma state_incr_trans6: + forall s1 s2 s3 s4 s5 s6 s7 s8, + state_incr s1 s2 -> state_incr s2 s3 -> state_incr s3 s4 -> + state_incr s4 s5 -> state_incr s5 s6 -> state_incr s6 s7 -> + state_incr s7 s8 -> state_incr s1 s8. +Proof. + intros; eauto 7 with rtlg. +Qed. + +(** The following relation between two states is a weaker version of + [state_incr]. It permits changing the contents at an already reserved + graph node, but only from [None] to [Some i]. *) + +Definition state_extends (s1 s2: state): Prop := + forall pc, + s1.(st_code)!pc = None \/ s2.(st_code)!pc = s1.(st_code)!pc. + +Lemma state_incr_extends: + forall s1 s2, + state_incr s1 s2 -> state_extends s1 s2. +Proof. + unfold state_extends; intros. inversion H. + case (plt pc s1.(st_nextnode)); intro. + right; apply H2; auto. + left. elim (s1.(st_wf) pc); intro. + elim (n H5). auto. +Qed. +Hint Resolve state_incr_extends. + +(** A crucial property of states is the following: if an RTL execution + is possible (does not get stuck) in the CFG of a given state [s1] + the same execution is possible and leads to the same results in + the CFG of any state [s2] that extends [s1] in the sense of the + [state_extends] predicate. *) + +Section EXEC_INSTR_EXTENDS. + +Variable s1 s2: state. +Hypothesis EXT: state_extends s1 s2. + +Lemma exec_instr_not_halt: + forall ge c sp pc rs m pc' rs' m', + exec_instr ge c sp pc rs m pc' rs' m' -> c!pc <> None. +Proof. + induction 1; rewrite H; discriminate. +Qed. + +Lemma exec_instr_in_s2: + forall ge sp pc rs m pc' rs' m', + exec_instr ge s1.(st_code) sp pc rs m pc' rs' m' -> + s2.(st_code)!pc = s1.(st_code)!pc. +Proof. + intros. + elim (EXT pc); intro. + elim (exec_instr_not_halt _ _ _ _ _ _ _ _ _ H H0). + assumption. +Qed. + +Lemma exec_instr_extends_rec: + forall ge c sp pc rs m pc' rs' m', + exec_instr ge c sp pc rs m pc' rs' m' -> + forall c', c!pc = c'!pc -> + exec_instr ge c' sp pc rs m pc' rs' m'. +Proof. + induction 1; intros. + apply exec_Inop. congruence. + apply exec_Iop with op args. congruence. auto. + apply exec_Iload with chunk addr args a. congruence. auto. auto. + apply exec_Istore with chunk addr args src a. + congruence. auto. auto. + apply exec_Icall with sig ros args f; auto. congruence. + apply exec_Icond_true with cond args ifnot; auto. congruence. + apply exec_Icond_false with cond args ifso; auto. congruence. +Qed. + +Lemma exec_instr_extends: + forall ge sp pc rs m pc' rs' m', + exec_instr ge s1.(st_code) sp pc rs m pc' rs' m' -> + exec_instr ge s2.(st_code) sp pc rs m pc' rs' m'. +Proof. + intros. + apply exec_instr_extends_rec with (st_code s1). + assumption. + symmetry. eapply exec_instr_in_s2. eexact H. +Qed. + +Lemma exec_instrs_extends_rec: + forall ge c sp pc rs m pc' rs' m', + exec_instrs ge c sp pc rs m pc' rs' m' -> + c = s1.(st_code) -> + exec_instrs ge s2.(st_code) sp pc rs m pc' rs' m'. +Proof. + induction 1; intros. + apply exec_refl. + apply exec_one. apply exec_instr_extends; auto. rewrite <- H0; auto. + apply exec_trans with pc2 rs2 m2; auto. +Qed. + +Lemma exec_instrs_extends: + forall ge sp pc rs m pc' rs' m', + exec_instrs ge s1.(st_code) sp pc rs m pc' rs' m' -> + exec_instrs ge s2.(st_code) sp pc rs m pc' rs' m'. +Proof. + intros. + apply exec_instrs_extends_rec with (st_code s1); auto. +Qed. + +End EXEC_INSTR_EXTENDS. + +(** Since [state_incr s1 s2] implies [state_extends s1 s2], we also have + that any RTL execution possible in the CFG of [s1] is also possible + in the CFG of [s2], provided that [state_incr s1 s2]. + In particular, any RTL execution that is possible in a partially + constructed CFG remains possible in the final CFG obtained at + the end of the translation of the current function. *) + +Section EXEC_INSTR_INCR. + +Variable s1 s2: state. +Hypothesis INCR: state_incr s1 s2. + +Lemma exec_instr_incr: + forall ge sp pc rs m pc' rs' m', + exec_instr ge s1.(st_code) sp pc rs m pc' rs' m' -> + exec_instr ge s2.(st_code) sp pc rs m pc' rs' m'. +Proof. + intros. + apply exec_instr_extends with s1. + apply state_incr_extends; auto. + auto. +Qed. + +Lemma exec_instrs_incr: + forall ge sp pc rs m pc' rs' m', + exec_instrs ge s1.(st_code) sp pc rs m pc' rs' m' -> + exec_instrs ge s2.(st_code) sp pc rs m pc' rs' m'. +Proof. + intros. + apply exec_instrs_extends with s1. + apply state_incr_extends; auto. + auto. +Qed. + +End EXEC_INSTR_INCR. + +(** * Validity and freshness of registers *) + +(** An RTL pseudo-register is valid in a given state if it was created + earlier, that is, it is less than the next fresh register of the state. + Otherwise, the pseudo-register is said to be fresh. *) + +Definition reg_valid (r: reg) (s: state) : Prop := + Plt r s.(st_nextreg). + +Definition reg_fresh (r: reg) (s: state) : Prop := + ~(Plt r s.(st_nextreg)). + +Lemma valid_fresh_absurd: + forall r s, reg_valid r s -> reg_fresh r s -> False. +Proof. + intros r s. unfold reg_valid, reg_fresh; case r; tauto. +Qed. +Hint Resolve valid_fresh_absurd: rtlg. + +Lemma valid_fresh_different: + forall r1 r2 s, reg_valid r1 s -> reg_fresh r2 s -> r1 <> r2. +Proof. + unfold not; intros. subst r2. eauto with rtlg. +Qed. +Hint Resolve valid_fresh_different: rtlg. + +Lemma reg_valid_incr: + forall r s1 s2, state_incr s1 s2 -> reg_valid r s1 -> reg_valid r s2. +Proof. + intros r s1 s2 INCR. + inversion INCR. + unfold reg_valid. intros; apply Plt_Ple_trans with (st_nextreg s1); auto. +Qed. +Hint Resolve reg_valid_incr: rtlg. + +Lemma reg_fresh_decr: + forall r s1 s2, state_incr s1 s2 -> reg_fresh r s2 -> reg_fresh r s1. +Proof. + intros r s1 s2 INCR. inversion INCR. + unfold reg_fresh; unfold not; intros. + apply H4. apply Plt_Ple_trans with (st_nextreg s1); auto. +Qed. +Hint Resolve reg_fresh_decr: rtlg. + +(** * Well-formedness of compilation environments *) + +(** A compilation environment (mapping) is well-formed in a given state if + the following properties hold: +- The registers associated with Cminor local variables and let-bound variables + are valid in the state. +- Two distinct Cminor local variables are mapped to distinct pseudo-registers. +- A Cminor local variable and a let-bound variable are mapped to + distinct pseudo-registers. +*) + +Record map_wf (m: mapping) (s: state) : Prop := + mk_map_wf { + map_wf_var_valid: + (forall id r, m.(map_vars)!id = Some r -> reg_valid r s); + map_wf_letvar_valid: + (forall r, In r m.(map_letvars) -> reg_valid r s); + map_wf_inj: + (forall id1 id2 r, + m.(map_vars)!id1 = Some r -> m.(map_vars)!id2 = Some r -> id1 = id2); + map_wf_disj: + (forall id r, + m.(map_vars)!id = Some r -> In r m.(map_letvars) -> False) + }. +Hint Resolve map_wf_var_valid + map_wf_letvar_valid + map_wf_inj map_wf_disj: rtlg. + +Lemma map_wf_incr: + forall s1 s2 m, + state_incr s1 s2 -> map_wf m s1 -> map_wf m s2. +Proof. + intros. apply mk_map_wf; intros; eauto with rtlg. +Qed. +Hint Resolve map_wf_incr: rtlg. + +(** A register is ``in'' a mapping if it is associated with a Cminor + local or let-bound variable. *) + +Definition reg_in_map (m: mapping) (r: reg) : Prop := + (exists id, m.(map_vars)!id = Some r) \/ In r m.(map_letvars). + +Lemma reg_in_map_valid: + forall m s r, + map_wf m s -> reg_in_map m r -> reg_valid r s. +Proof. + intros. elim H0. + intros [id EQ]. eauto with rtlg. + intro IN. eauto with rtlg. +Qed. +Hint Resolve reg_in_map_valid: rtlg. + +(** A register is mutated if it is associated with a Cminor local variable + that belongs to the given set of mutated variables. *) + +Definition mutated_reg (map: mapping) (mut: list ident) (r: reg) : Prop := + exists id, In id mut /\ map.(map_vars)!id = Some r. + +Lemma mutated_reg_in_map: + forall map mut r, mutated_reg map mut r -> reg_in_map map r. +Proof. + intros. elim H. intros id [IN EQ]. + left. exists id; auto. +Qed. +Hint Resolve mutated_reg_in_map: rtlg. + +(** * Properties of basic operations over the state *) + +(** Properties of [add_instr]. *) + +Lemma add_instr_incr: + forall s1 s2 i n, + add_instr i s1 = OK n s2 -> state_incr s1 s2. +Proof. + intros until n; monadSimpl. + subst s2; apply state_incr_intro; simpl. + apply Ple_succ. + apply Ple_refl. + intros. apply PTree.gso; apply Plt_ne; auto. +Qed. +Hint Resolve add_instr_incr: rtlg. + +Lemma add_instr_at: + forall s1 s2 i n, + add_instr i s1 = OK n s2 -> s2.(st_code)!n = Some i. +Proof. + intros until n; monadSimpl. + subst n; subst s2; simpl. apply PTree.gss. +Qed. +Hint Resolve add_instr_at. + +(** Properties of [reserve_instr] and [update_instr]. *) + +Lemma reserve_instr_incr: + forall s1 s2 n, + reserve_instr s1 = OK n s2 -> state_incr s1 s2. +Proof. + intros until n; monadSimpl. subst s2. + apply state_incr_intro; simpl. + apply Ple_succ. + apply Ple_refl. + auto. +Qed. + +Lemma update_instr_incr: + forall s1 s2 s3 s4 i n t, + reserve_instr s1 = OK n s2 -> + state_incr s2 s3 -> + update_instr n i s3 = OK t s4 -> + state_incr s1 s4. +Proof. + intros. + monadInv H. + generalize H1; unfold update_instr. + case (plt n (st_nextnode s3)); intro. + monadSimpl. inversion H0. + subst s4; apply state_incr_intro; simpl. + apply Plt_Ple. apply Plt_Ple_trans with (st_nextnode s2). + subst s2; simpl; apply Plt_succ. assumption. + rewrite <- H3 in H7; simpl in H7. assumption. + intros. rewrite PTree.gso. + rewrite <- H3 in H8; simpl in H8. apply H8. + apply Plt_trans_succ; assumption. + subst n; apply Plt_ne; assumption. + intros; discriminate. +Qed. + +Lemma update_instr_extends: + forall s1 s2 s3 s4 i n t, + reserve_instr s1 = OK n s2 -> + state_incr s2 s3 -> + update_instr n i s3 = OK t s4 -> + state_extends s3 s4. +Proof. + intros. + monadInv H. + red; intros. + case (peq pc n); intro. + subst pc. left. inversion H0. rewrite H6. + rewrite <- H3; simpl. + elim (s1.(st_wf) n); intro. + rewrite <- H4 in H9. elim (Plt_strict _ H9). + auto. + rewrite <- H4. rewrite <- H3; simpl. apply Plt_succ. + generalize H1; unfold update_instr. + case (plt n s3.(st_nextnode)); intro; monadSimpl. + right; rewrite <- H5; simpl. apply PTree.gso; auto. +Qed. + +(** Properties of [new_reg]. *) + +Lemma new_reg_incr: + forall s1 s2 r, new_reg s1 = OK r s2 -> state_incr s1 s2. +Proof. + intros until r. monadSimpl. + subst s2; apply state_incr_intro; simpl. + apply Ple_refl. apply Ple_succ. auto. +Qed. +Hint Resolve new_reg_incr: rtlg. + +Lemma new_reg_valid: + forall s1 s2 r, + new_reg s1 = OK r s2 -> reg_valid r s2. +Proof. + intros until r. monadSimpl. subst s2; subst r. + unfold reg_valid; unfold reg_valid; simpl. + apply Plt_succ. +Qed. +Hint Resolve new_reg_valid: rtlg. + +Lemma new_reg_fresh: + forall s1 s2 r, + new_reg s1 = OK r s2 -> reg_fresh r s1. +Proof. + intros until r. monadSimpl. subst s2; subst r. + unfold reg_fresh; simpl. + exact (Plt_strict _). +Qed. +Hint Resolve new_reg_fresh: rtlg. + +Lemma new_reg_not_in_map: + forall s1 s2 m r, + new_reg s1 = OK r s2 -> map_wf m s1 -> ~(reg_in_map m r). +Proof. + unfold not; intros; eauto with rtlg. +Qed. +Hint Resolve new_reg_not_in_map: rtlg. + +Lemma new_reg_not_mutated: + forall s1 s2 m mut r, + new_reg s1 = OK r s2 -> map_wf m s1 -> ~(mutated_reg m mut r). +Proof. + unfold not; intros. + generalize (mutated_reg_in_map _ _ _ H1); intro. + exact (new_reg_not_in_map _ _ _ _ H H0 H2). +Qed. +Hint Resolve new_reg_not_mutated: rtlg. + +(** * Properties of operations over compilation environments *) + +Lemma init_mapping_wf: + forall s, map_wf init_mapping s. +Proof. + intro. unfold init_mapping; apply mk_map_wf; simpl; intros. + rewrite PTree.gempty in H; discriminate. + contradiction. + rewrite PTree.gempty in H; discriminate. + tauto. +Qed. + +(** Properties of [find_var]. *) + +Lemma find_var_incr: + forall s1 s2 map name r, + find_var map name s1 = OK r s2 -> state_incr s1 s2. +Proof. + intros until r. unfold find_var. + case (map_vars map)!name. + intro; monadSimpl. subst s2; auto with rtlg. + monadSimpl. +Qed. +Hint Resolve find_var_incr: rtlg. + +Lemma find_var_in_map: + forall s1 s2 map name r, + find_var map name s1 = OK r s2 -> map_wf map s1 -> reg_in_map map r. +Proof. + intros until r. unfold find_var; caseEq (map.(map_vars)!name). + intros r0 eq. monadSimpl; intros. subst r0. + left. exists name; auto. + intro; monadSimpl. +Qed. +Hint Resolve find_var_in_map: rtlg. + +Lemma find_var_valid: + forall s1 s2 map name r, + find_var map name s1 = OK r s2 -> map_wf map s1 -> reg_valid r s1. +Proof. + eauto with rtlg. +Qed. +Hint Resolve find_var_valid: rtlg. + +Lemma find_var_not_mutated: + forall s1 s2 map name r mut, + find_var map name s1 = OK r s2 -> + map_wf map s1 -> + ~(In name mut) -> + ~(mutated_reg map mut r). +Proof. + intros until mut. unfold find_var; caseEq (map.(map_vars)!name). + intros r0 EQ. monadSimpl; intros; subst r0. + red; unfold mutated_reg; intros [id [IN EQ2]]. + assert (name = id). eauto with rtlg. + subst id. contradiction. + intro; monadSimpl. +Qed. +Hint Resolve find_var_not_mutated: rtlg. + +(** Properties of [find_letvar]. *) + +Lemma find_letvar_incr: + forall s1 s2 map idx r, + find_letvar map idx s1 = OK r s2 -> state_incr s1 s2. +Proof. + intros until r. unfold find_letvar. + case (nth_error (map_letvars map) idx). + intro; monadSimpl. subst s2; auto with rtlg. + monadSimpl. +Qed. +Hint Resolve find_letvar_incr: rtlg. + +Lemma find_letvar_in_map: + forall s1 s2 map idx r, + find_letvar map idx s1 = OK r s2 -> map_wf map s1 -> reg_in_map map r. +Proof. + intros until r. unfold find_letvar. + caseEq (nth_error (map_letvars map) idx). + intros r0 EQ; monadSimpl. intros. right. + subst r0; apply nth_error_in with idx; auto. + intro; monadSimpl. +Qed. +Hint Resolve find_letvar_in_map: rtlg. + +Lemma find_letvar_valid: + forall s1 s2 map idx r, + find_letvar map idx s1 = OK r s2 -> map_wf map s1 -> reg_valid r s1. +Proof. + eauto with rtlg. +Qed. +Hint Resolve find_letvar_valid: rtlg. + +Lemma find_letvar_not_mutated: + forall s1 s2 map idx mut r, + find_letvar map idx s1 = OK r s2 -> + map_wf map s1 -> + ~(mutated_reg map mut r). +Proof. + intros until r. unfold find_letvar. + caseEq (nth_error (map_letvars map) idx). + intros r' NTH. monadSimpl. unfold not; unfold mutated_reg. + intros MWF (id, (IN, MV)). subst r'. eauto with rtlg coqlib. + intro; monadSimpl. +Qed. +Hint Resolve find_letvar_not_mutated: rtlg. + +(** Properties of [add_var]. *) + +Lemma add_var_valid: + forall s1 s2 map1 map2 name r, + add_var map1 name s1 = OK (r, map2) s2 -> reg_valid r s2. +Proof. + intros until r. monadSimpl. intro. subst r0; subst s. + eauto with rtlg. +Qed. + +Lemma add_var_incr: + forall s1 s2 map name rm, + add_var map name s1 = OK rm s2 -> state_incr s1 s2. +Proof. + intros until rm; monadSimpl. subst s2. eauto with rtlg. +Qed. +Hint Resolve add_var_incr: rtlg. + +Lemma add_var_wf: + forall s1 s2 map name r map', + add_var map name s1 = OK (r,map') s2 -> map_wf map s1 -> map_wf map' s2. +Proof. + intros until map'; monadSimpl; intros. + subst r0; subst s; subst map'; apply mk_map_wf; simpl. + + intros id r'. rewrite PTree.gsspec. + case (peq id name); intros. + injection H; intros; subst r'. eauto with rtlg. + eauto with rtlg. + eauto with rtlg. + + intros id1 id2 r'. + repeat (rewrite PTree.gsspec). + case (peq id1 name); case (peq id2 name); intros. + congruence. + rewrite <- H in H0. byContradiction; eauto with rtlg. + rewrite <- H0 in H. byContradiction; eauto with rtlg. + eauto with rtlg. + + intros id r'. case (peq id name); intro. + subst id. rewrite PTree.gss. intro E; injection E; intro; subst r'. + intro; eauto with rtlg. + + rewrite PTree.gso; auto. eauto with rtlg. +Qed. +Hint Resolve add_var_wf: rtlg. + +Lemma add_var_find: + forall s1 s2 map name r map', + add_var map name s1 = OK (r,map') s2 -> map'.(map_vars)!name = Some r. +Proof. + intros until map'. + monadSimpl. + intro; subst r0. + subst map'; simpl in |- *. + apply PTree.gss. +Qed. + +Lemma add_vars_incr: + forall names s1 s2 map r, + add_vars map names s1 = OK r s2 -> state_incr s1 s2. +Proof. + induction names; simpl. + intros until r; monadSimpl; intros. subst s2; eauto with rtlg. + intros until r; monadSimpl; intros. + subst s0; eauto with rtlg. +Qed. + +Lemma add_vars_valid: + forall namel s1 s2 map1 map2 rl, + add_vars map1 namel s1 = OK (rl, map2) s2 -> + forall r, In r rl -> reg_valid r s2. +Proof. + induction namel; simpl; intros. + monadInv H. intro. subst rl. elim H0. + monadInv H. intro EQ1. subst rl; subst s0; subst y0. elim H0. + intro; subst r. eapply add_var_valid. eexact EQ0. + intro. apply reg_valid_incr with s. eauto with rtlg. + eauto. +Qed. + +Lemma add_vars_wf: + forall names s1 s2 map map' rl, + add_vars map names s1 = OK (rl,map') s2 -> + map_wf map s1 -> map_wf map' s2. +Proof. + induction names; simpl. + intros until rl; monadSimpl; intros. + subst s2; subst map'; assumption. + intros until rl; monadSimpl; intros. subst y0; subst s0. + eapply add_var_wf. eexact EQ0. + eapply IHnames. eexact EQ. auto. +Qed. +Hint Resolve add_vars_wf: rtlg. + +Lemma add_var_letenv: + forall map1 i s1 r map2 s2, + add_var map1 i s1 = OK (r, map2) s2 -> + map2.(map_letvars) = map1.(map_letvars). +Proof. + intros until s2. monadSimpl. intro. subst map2; reflexivity. +Qed. + +(** Properties of [add_letvar]. *) + +Lemma add_letvar_wf: + forall map s r, + map_wf map s -> + reg_valid r s -> + ~(reg_in_map map r) -> + map_wf (add_letvar map r) s. +Proof. + intros. unfold add_letvar; apply mk_map_wf; simpl. + exact (map_wf_var_valid map s H). + intros r' [EQ| IN]. + subst r'; assumption. + eapply map_wf_letvar_valid; eauto. + exact (map_wf_inj map s H). + intros. elim H3; intro. + subst r0. apply H1. left. exists id; auto. + eapply map_wf_disj; eauto. +Qed. + +(** * Properties of [alloc_reg] and [alloc_regs] *) + +Lemma alloc_reg_incr: + forall a s1 s2 map mut r, + alloc_reg map mut a s1 = OK r s2 -> state_incr s1 s2. +Proof. + intros until r. unfold alloc_reg. + case a; eauto with rtlg. + intro i; case (In_dec ident_eq i mut); eauto with rtlg. +Qed. +Hint Resolve alloc_reg_incr: rtlg. + +Lemma alloc_reg_valid: + forall a s1 s2 map mut r, + map_wf map s1 -> + alloc_reg map mut a s1 = OK r s2 -> reg_valid r s2. +Proof. + intros until r. unfold alloc_reg. + case a; eauto with rtlg. + intro i; case (In_dec ident_eq i mut); eauto with rtlg. +Qed. +Hint Resolve alloc_reg_valid: rtlg. + +Lemma alloc_reg_fresh_or_in_map: + forall map mut a s r s', + map_wf map s -> + alloc_reg map mut a s = OK r s' -> + reg_in_map map r \/ reg_fresh r s. +Proof. + intros until s'. unfold alloc_reg. + destruct a; try (right; eauto with rtlg; fail). + case (In_dec ident_eq i mut); intros. + right; eauto with rtlg. + left; eauto with rtlg. + intros; left; eauto with rtlg. +Qed. + +Lemma add_vars_letenv: + forall il map1 s1 rl map2 s2, + add_vars map1 il s1 = OK (rl, map2) s2 -> + map2.(map_letvars) = map1.(map_letvars). +Proof. + induction il; simpl; intros. + monadInv H. intro. subst map2; reflexivity. + monadInv H. intro EQ1. transitivity (map_letvars y). + subst y0. eapply add_var_letenv; eauto. + eauto. +Qed. + +(** A register is an adequate target for holding the value of an + expression if +- either the register is associated with a Cminor let-bound variable + or a Cminor local variable that is not modified; +- or the register is valid and not associated with any Cminor variable. *) + +Inductive target_reg_ok: state -> mapping -> list ident -> expr -> reg -> Prop := + | target_reg_immut_var: + forall s map mut id r, + ~(In id mut) -> map.(map_vars)!id = Some r -> + target_reg_ok s map mut (Evar id) r + | target_reg_letvar: + forall s map mut idx r, + nth_error map.(map_letvars) idx = Some r -> + target_reg_ok s map mut (Eletvar idx) r + | target_reg_other: + forall s map mut a r, + ~(reg_in_map map r) -> + reg_valid r s -> + target_reg_ok s map mut a r. + +Lemma target_reg_ok_incr: + forall s1 s2 map mut e r, + state_incr s1 s2 -> + target_reg_ok s1 map mut e r -> + target_reg_ok s2 map mut e r. +Proof. + intros. inversion H0. + apply target_reg_immut_var; auto. + apply target_reg_letvar; auto. + apply target_reg_other; eauto with rtlg. +Qed. +Hint Resolve target_reg_ok_incr: rtlg. + +Lemma target_reg_valid: + forall s map mut e r, + map_wf map s -> + target_reg_ok s map mut e r -> + reg_valid r s. +Proof. + intros. inversion H0; eauto with rtlg coqlib. +Qed. +Hint Resolve target_reg_valid: rtlg. + +Lemma target_reg_not_mutated: + forall s map mut e r, + map_wf map s -> + target_reg_ok s map mut e r -> + ~(mutated_reg map mut r). +Proof. + unfold not; unfold mutated_reg; intros until r. + intros MWF TRG [id [IN MV]]. + inversion TRG. + assert (id = id0); eauto with rtlg. subst id0. contradiction. + assert (In r (map_letvars map)). eauto with coqlib. eauto with rtlg. + apply H. red. left; exists id; assumption. +Qed. +Hint Resolve target_reg_not_mutated: rtlg. + +Lemma alloc_reg_target_ok: + forall a s1 s2 map mut r, + map_wf map s1 -> + alloc_reg map mut a s1 = OK r s2 -> + target_reg_ok s2 map mut a r. +Proof. + intros until r; intro MWF. unfold alloc_reg. + case a; intros; try (eapply target_reg_other; eauto with rtlg; fail). + generalize H; case (In_dec ident_eq i mut); intros. + apply target_reg_other; eauto with rtlg. + apply target_reg_immut_var; auto. + generalize H0; unfold find_var. + case (map_vars map)!i. + intro. monadSimpl. congruence. + monadSimpl. + apply target_reg_letvar. + generalize H. unfold find_letvar. + case (nth_error (map_letvars map) n). + intro; monadSimpl; congruence. + monadSimpl. +Qed. +Hint Resolve alloc_reg_target_ok: rtlg. + +Lemma alloc_regs_incr: + forall al s1 s2 map mut rl, + alloc_regs map mut al s1 = OK rl s2 -> state_incr s1 s2. +Proof. + induction al; simpl; intros. + monadInv H. subst s2. eauto with rtlg. + monadInv H. subst s2. eauto with rtlg. +Qed. +Hint Resolve alloc_regs_incr: rtlg. + +Lemma alloc_regs_valid: + forall al s1 s2 map mut rl, + map_wf map s1 -> + alloc_regs map mut al s1 = OK rl s2 -> + forall r, In r rl -> reg_valid r s2. +Proof. + induction al; simpl; intros. + monadInv H0. subst rl. elim H1. + monadInv H0. subst rl; subst s0. + elim H1; intro. + subst r0. eauto with rtlg. + eauto with rtlg. +Qed. +Hint Resolve alloc_regs_valid: rtlg. + +Lemma alloc_regs_fresh_or_in_map: + forall map mut al s rl s', + map_wf map s -> + alloc_regs map mut al s = OK rl s' -> + forall r, In r rl -> reg_in_map map r \/ reg_fresh r s. +Proof. + induction al; simpl; intros. + monadInv H0. subst rl. elim H1. + monadInv H0. subst rl. elim (in_inv H1); intro. + subst r. + assert (MWF: map_wf map s0). eauto with rtlg. + elim (alloc_reg_fresh_or_in_map map mut e s0 r0 s1 MWF EQ0); intro. + left; assumption. right; eauto with rtlg. + eauto with rtlg. +Qed. + +Inductive target_regs_ok: state -> mapping -> list ident -> exprlist -> list reg -> Prop := + | target_regs_nil: + forall s map mut, + target_regs_ok s map mut Enil nil + | target_regs_cons: + forall s map mut a r al rl, + reg_in_map map r \/ ~(In r rl) -> + target_reg_ok s map mut a r -> + target_regs_ok s map mut al rl -> + target_regs_ok s map mut (Econs a al) (r :: rl). + +Lemma target_regs_ok_incr: + forall s1 map mut al rl, + target_regs_ok s1 map mut al rl -> + forall s2, + state_incr s1 s2 -> + target_regs_ok s2 map mut al rl. +Proof. + induction 1; intros. + apply target_regs_nil. + apply target_regs_cons; eauto with rtlg. +Qed. +Hint Resolve target_regs_ok_incr: rtlg. + +Lemma target_regs_valid: + forall s map mut al rl, + target_regs_ok s map mut al rl -> + map_wf map s -> + forall r, In r rl -> reg_valid r s. +Proof. + induction 1; simpl; intros. + contradiction. + elim H3; intro. + subst r0. eauto with rtlg. + auto. +Qed. +Hint Resolve target_regs_valid: rtlg. + +Lemma target_regs_not_mutated: + forall s map mut el rl, + target_regs_ok s map mut el rl -> + map_wf map s -> + forall r, In r rl -> ~(mutated_reg map mut r). +Proof. + induction 1; simpl; intros. + contradiction. + elim H3; intro. subst r0. eauto with rtlg. + auto. +Qed. +Hint Resolve target_regs_not_mutated: rtlg. + +Lemma alloc_regs_target_ok: + forall al s1 s2 map mut rl, + map_wf map s1 -> + alloc_regs map mut al s1 = OK rl s2 -> + target_regs_ok s2 map mut al rl. +Proof. + induction al; simpl; intros. + monadInv H0. subst rl; apply target_regs_nil. + monadInv H0. subst s0; subst rl. + apply target_regs_cons; eauto 6 with rtlg. + assert (MWF: map_wf map s). eauto with rtlg. + elim (alloc_reg_fresh_or_in_map map mut e s r s2 MWF EQ0); intro. + left; assumption. right; red; intro; eauto with rtlg. +Qed. +Hint Resolve alloc_regs_target_ok: rtlg. + +(** The following predicate is a variant of [target_reg_ok] used + to characterize registers that are adequate for holding the return + value of a function. *) + +Inductive return_reg_ok: state -> mapping -> option reg -> Prop := + | return_reg_ok_none: + forall s map, + return_reg_ok s map None + | return_reg_ok_some: + forall s map r, + ~(reg_in_map map r) -> reg_valid r s -> + return_reg_ok s map (Some r). + +Lemma return_reg_ok_incr: + forall s1 s2 map or, + state_incr s1 s2 -> + return_reg_ok s1 map or -> + return_reg_ok s2 map or. +Proof. + intros. inversion H0; constructor. + assumption. eauto with rtlg. +Qed. +Hint Resolve return_reg_ok_incr: rtlg. + +Lemma new_reg_return_ok: + forall s1 r s2 map sig, + new_reg s1 = OK r s2 -> + map_wf map s1 -> + return_reg_ok s2 map (ret_reg sig r). +Proof. + intros. unfold ret_reg. destruct (sig_res sig); constructor. + eauto with rtlg. eauto with rtlg. +Qed. + +(** * Correspondence between Cminor environments and RTL register sets *) + +(** An RTL register environment matches a Cminor local environment and + let-environment if the value of every local or let-bound variable in + the Cminor environments is identical to the value of the + corresponding pseudo-register in the RTL register environment. *) + +Record match_env + (map: mapping) (e: Cminor.env) (le: Cminor.letenv) (rs: regset) : Prop := + mk_match_env { + me_vars: + (forall id v, + e!id = Some v -> exists r, map.(map_vars)!id = Some r /\ rs#r = v); + me_letvars: + rs##(map.(map_letvars)) = le + }. + +Lemma match_env_find_reg: + forall map id s1 s2 r e le rs v, + find_var map id s1 = OK r s2 -> + match_env map e le rs -> + e!id = Some v -> + rs#r = v. +Proof. + intros until v. + unfold find_var. caseEq (map.(map_vars)!id). + intros r' EQ. monadSimpl. subst r'. intros. + generalize (me_vars _ _ _ _ H _ _ H1). intros [r' [EQ' RS]]. + rewrite EQ' in EQ; injection EQ; intro; subst r'. + assumption. + intro; monadSimpl. +Qed. +Hint Resolve match_env_find_reg: rtlg. + +Lemma match_env_invariant: + forall map e le rs rs', + match_env map e le rs -> + (forall r, (reg_in_map map r) -> rs'#r = rs#r) -> + match_env map e le rs'. +Proof. + intros. apply mk_match_env. + intros id v' E. + generalize (me_vars _ _ _ _ H _ _ E). intros (r', (M, R)). + exists r'. split. auto. rewrite <- R. apply H0. + left. exists id. auto. + transitivity rs ## (map_letvars map). + apply list_map_exten. intros. + symmetry. apply H0. right. auto. + exact (me_letvars _ _ _ _ H). +Qed. + +(** Matching between environments is preserved when an unmapped register + (not corresponding to any Cminor variable) is assigned in the RTL + execution. *) + +Lemma match_env_update_temp: + forall map e le rs r v, + match_env map e le rs -> + ~(reg_in_map map r) -> + match_env map e le (rs#r <- v). +Proof. + intros. apply match_env_invariant with rs; auto. + intros. case (Reg.eq r r0); intro. + subst r0; contradiction. + apply Regmap.gso; auto. +Qed. +Hint Resolve match_env_update_temp: rtlg. + +(** Matching between environments is preserved by simultaneous + assignment to a Cminor local variable (in the Cminor environments) + and to the corresponding RTL pseudo-register (in the RTL register + environment). *) + +Lemma match_env_update_var: + forall map e le rs rs' id r v s s', + map_wf map s -> + find_var map id s = OK r s' -> + match_env map e le rs -> + rs'#r = v -> + (forall x, x <> r -> rs'#x = rs#x) -> + match_env map (PTree.set id v e) le rs'. +Proof. + intros until s'; intro MWF. + unfold find_var in |- *. caseEq (map_vars map)!id. + intros. monadInv H0. subst r0. apply mk_match_env. + intros id' v' E. case (peq id' id); intros. + subst id'. rewrite PTree.gss in E. injection E; intro; subst v'. + exists r. split. auto. auto. + rewrite PTree.gso in E; auto. + elim (me_vars _ _ _ _ H1 _ _ E). intros r' (M, R). + exists r'. split. assumption. rewrite <- R; apply H3; auto. + red in |- *; intro. subst r'. apply n. eauto with rtlg. + transitivity rs ## (map_letvars map). + apply list_map_exten. intros. symmetry. apply H3. + red in |- *; intro. subst x. eauto with rtlg. + exact (me_letvars _ _ _ _ H1). + intro; monadSimpl. +Qed. + +Lemma match_env_letvar: + forall map e le rs r v, + match_env map e le rs -> + rs#r = v -> + match_env (add_letvar map r) e (v :: le) rs. +Proof. + intros. unfold add_letvar in |- *; apply mk_match_env; simpl in |- *. + exact (me_vars _ _ _ _ H). + rewrite H0. rewrite (me_letvars _ _ _ _ H). auto. +Qed. + +Lemma match_env_exten: + forall map e le rs1 rs2, + (forall r, rs2#r = rs1#r) -> + match_env map e le rs1 -> + match_env map e le rs2. +Proof. + intros. apply mk_match_env. + intros. generalize (me_vars _ _ _ _ H0 _ _ H1). intros (r, (M1, M2)). + exists r. split. assumption. subst v. apply H. + transitivity rs1 ## (map_letvars map). + apply list_map_exten. intros. symmetry in |- *. apply H. + exact (me_letvars _ _ _ _ H0). +Qed. + +Lemma match_env_empty: + forall map, + map.(map_letvars) = nil -> + match_env map (PTree.empty val) nil (Regmap.init Vundef). +Proof. + intros. apply mk_match_env. + intros. rewrite PTree.gempty in H0. discriminate. + rewrite H. reflexivity. +Qed. + +(** The assignment of function arguments to local variables (on the Cminor + side) and pseudo-registers (on the RTL side) preserves matching + between environments. *) + +Lemma match_set_params_init_regs: + forall il rl s1 map2 s2 vl, + add_vars init_mapping il s1 = OK (rl, map2) s2 -> + match_env map2 (set_params vl il) nil (init_regs vl rl) + /\ (forall r, reg_fresh r s2 -> (init_regs vl rl)#r = Vundef). +Proof. + induction il; simpl in |- *; intros. + + monadInv H. intro; subst rl; simpl in |- *. + split. apply match_env_empty. subst map2; auto. + intros. apply Regmap.gi. + + monadInv H. intro EQ1; subst s0; subst y0; subst rl. clear H. + monadInv EQ0. intro EQ2. subst x0; subst s0. simpl. + + assert (LV : map_letvars map2 = nil). + transitivity (map_letvars y). + eapply add_var_letenv; eauto. + transitivity (map_letvars init_mapping). + eapply add_vars_letenv; eauto. + reflexivity. + + destruct vl. + (* vl = nil *) + generalize (IHil _ _ _ _ nil EQ). intros [ME UNDEF]. split. + constructor. intros id v. subst map2. simpl. + repeat rewrite PTree.gsspec; case (peq id a); intros. + exists r; split. auto. rewrite Regmap.gi. congruence. + destruct (me_vars _ _ _ _ ME id v H) as (r', (MV, IR)). + exists r'. split. auto. + replace (init_regs nil x) with (Regmap.init Vundef) in IR. auto. + destruct x; reflexivity. + rewrite LV; reflexivity. + intros. apply Regmap.gi. + (* vl = v :: vl *) + generalize (IHil _ _ _ _ vl EQ). intros [ME UNDEF]. split. + constructor. intros id v1. subst map2. simpl. + repeat rewrite PTree.gsspec; case (peq id a); intros. + exists r; split. auto. rewrite Regmap.gss. congruence. + destruct (me_vars _ _ _ _ ME id v1 H) as (r', (MV, IR)). + exists r'. split. auto. rewrite Regmap.gso. auto. + apply valid_fresh_different with s. + assert (MWF : map_wf y s). + eapply add_vars_wf; eauto. apply init_mapping_wf. + eauto with rtlg. eauto with rtlg. + rewrite LV; reflexivity. + intros. rewrite Regmap.gso. apply UNDEF. eauto with rtlg. + apply sym_not_equal. eauto with rtlg. +Qed. + +Lemma match_set_locals: + forall map1 s1, + map_wf map1 s1 -> + forall il rl map2 s2 e le rs, + match_env map1 e le rs -> + (forall r, reg_fresh r s1 -> rs#r = Vundef) -> + add_vars map1 il s1 = OK (rl, map2) s2 -> + match_env map2 (set_locals il e) le rs. +Proof. + induction il; simpl in *; intros. + + monadInv H2. intros; subst map2; auto. + + monadInv H2. intros. subst s0; subst y0. + assert (match_env y (set_locals il e) le rs). + eapply IHil; eauto. + monadInv EQ0. intro. subst s0; subst x0. rewrite <- H7. + constructor. + intros id v. simpl. repeat rewrite PTree.gsspec. + case (peq id a); intros. + exists r. split. auto. injection H5; intro; subst v. + apply H1. apply reg_fresh_decr with s. + eapply add_vars_incr; eauto. + eauto with rtlg. + eapply me_vars; eauto. + simpl. eapply me_letvars; eauto. +Qed. + +Lemma match_init_env_init_reg: + forall params s0 rparams map1 s1 vars rvars map2 s2 vparams, + add_vars init_mapping params s0 = OK (rparams, map1) s1 -> + add_vars map1 vars s1 = OK (rvars, map2) s2 -> + match_env map2 (set_locals vars (set_params vparams params)) + nil (init_regs vparams rparams). +Proof. + intros. + generalize (match_set_params_init_regs _ _ _ _ _ vparams H). + intros [A B]. + eapply match_set_locals; eauto. + eapply add_vars_wf; eauto. apply init_mapping_wf. +Qed. + +(** * Monotonicity properties of the state for the translation functions *) + +(** We show that the translation functions modify the state monotonically + (in the sense of the [state_incr] relation). *) + +Lemma add_move_incr: + forall r1 r2 nd s ns s', + add_move r1 r2 nd s = OK ns s' -> + state_incr s s'. +Proof. + intros until s'. unfold add_move. + case (Reg.eq r1 r2); intro. + monadSimpl. subst s'; auto with rtlg. + intro; eauto with rtlg. +Qed. +Hint Resolve add_move_incr: rtlg. + +Scheme expr_ind3 := Induction for expr Sort Prop + with condexpr_ind3 := Induction for condexpr Sort Prop + with exprlist_ind3 := Induction for exprlist Sort Prop. + +Lemma expr_condexpr_exprlist_ind: +forall (P : expr -> Prop) (P0 : condexpr -> Prop) + (P1 : exprlist -> Prop), + (forall i : ident, P (Evar i)) -> + (forall (i : ident) (e : expr), P e -> P (Eassign i e)) -> + (forall (o : operation) (e : exprlist), P1 e -> P (Eop o e)) -> + (forall (m : memory_chunk) (a : addressing) (e : exprlist), + P1 e -> P (Eload m a e)) -> + (forall (m : memory_chunk) (a : addressing) (e : exprlist), + P1 e -> forall e0 : expr, P e0 -> P (Estore m a e e0)) -> + (forall (s : signature) (e : expr), + P e -> forall e0 : exprlist, P1 e0 -> P (Ecall s e e0)) -> + (forall c : condexpr, + P0 c -> + forall e : expr, + P e -> forall e0 : expr, P e0 -> P (Econdition c e e0)) -> + (forall e : expr, P e -> forall e0 : expr, P e0 -> P (Elet e e0)) -> + (forall n : nat, P (Eletvar n)) -> + P0 CEtrue -> + P0 CEfalse -> + (forall (c : condition) (e : exprlist), P1 e -> P0 (CEcond c e)) -> + (forall c : condexpr, + P0 c -> + forall c0 : condexpr, + P0 c0 -> forall c1 : condexpr, P0 c1 -> P0 (CEcondition c c0 c1)) -> + P1 Enil -> + (forall e : expr, + P e -> forall e0 : exprlist, P1 e0 -> P1 (Econs e e0)) -> + (forall e : expr, P e) /\ + (forall ce : condexpr, P0 ce) /\ + (forall el : exprlist, P1 el). +Proof. + intros. split. apply (expr_ind3 P P0 P1); assumption. + split. apply (condexpr_ind3 P P0 P1); assumption. + apply (exprlist_ind3 P P0 P1); assumption. +Qed. + +Definition transl_expr_incr_pred (a: expr) : Prop := + forall map mut rd nd s ns s', + transl_expr map mut a rd nd s = OK ns s' -> state_incr s s'. +Definition transl_condition_incr_pred (c: condexpr) : Prop := + forall map mut ntrue nfalse s ns s', + transl_condition map mut c ntrue nfalse s = OK ns s' -> state_incr s s'. +Definition transl_exprlist_incr_pred (al: exprlist) : Prop := + forall map mut rl nd s ns s', + transl_exprlist map mut al rl nd s = OK ns s' -> state_incr s s'. + +Lemma transl_expr_condition_exprlist_incr: + (forall a, transl_expr_incr_pred a) /\ + (forall c, transl_condition_incr_pred c) /\ + (forall al, transl_exprlist_incr_pred al). +Proof. + apply expr_condexpr_exprlist_ind; + unfold transl_expr_incr_pred, + transl_condition_incr_pred, + transl_exprlist_incr_pred; + simpl; intros; + try (monadInv H); try (monadInv H0); + try (monadInv H1); try (monadInv H2); + eauto 6 with rtlg. + + intro EQ2. + apply state_incr_trans3 with s0 s1 s2; eauto with rtlg. + + intro EQ4. + apply state_incr_trans4 with s1 s2 s3 s4; eauto with rtlg. + + subst s'; auto with rtlg. + subst s'; auto with rtlg. + destruct rl; monadInv H. subst s'; auto with rtlg. + destruct rl; monadInv H1. eauto with rtlg. +Qed. + +Lemma transl_expr_incr: + forall a map mut rd nd s ns s', + transl_expr map mut a rd nd s = OK ns s' -> state_incr s s'. +Proof (proj1 transl_expr_condition_exprlist_incr). + +Lemma transl_condition_incr: + forall a map mut ntrue nfalse s ns s', + transl_condition map mut a ntrue nfalse s = OK ns s' -> state_incr s s'. +Proof (proj1 (proj2 transl_expr_condition_exprlist_incr)). + +Lemma transl_exprlist_incr: + forall al map mut rl nd s ns s', + transl_exprlist map mut al rl nd s = OK ns s' -> state_incr s s'. +Proof (proj2 (proj2 transl_expr_condition_exprlist_incr)). + +Hint Resolve transl_expr_incr transl_condition_incr transl_exprlist_incr: rtlg. + +Scheme stmt_ind2 := Induction for stmt Sort Prop + with stmtlist_ind2 := Induction for stmtlist Sort Prop. + +Lemma stmt_stmtlist_ind: +forall (P : stmt -> Prop) (P0 : stmtlist -> Prop), + (forall e : expr, P (Sexpr e)) -> + (forall (c : condexpr) (s : stmtlist), + P0 s -> forall s0 : stmtlist, P0 s0 -> P (Sifthenelse c s s0)) -> + (forall s : stmtlist, P0 s -> P (Sloop s)) -> + (forall s : stmtlist, P0 s -> P (Sblock s)) -> + (forall n : nat, P (Sexit n)) -> + (forall o : option expr, P (Sreturn o)) -> + P0 Snil -> + (forall s : stmt, + P s -> forall s0 : stmtlist, P0 s0 -> P0 (Scons s s0)) -> + (forall s : stmt, P s) /\ + (forall sl : stmtlist, P0 sl). +Proof. + intros. split. apply (stmt_ind2 P P0); assumption. + apply (stmtlist_ind2 P P0); assumption. +Qed. + +Definition transl_stmt_incr_pred (a: stmt) : Prop := + forall map nd nexits nret rret s ns s', + transl_stmt map a nd nexits nret rret s = OK ns s' -> + state_incr s s'. +Definition transl_stmtlist_incr_pred (al: stmtlist) : Prop := + forall map nd nexits nret rret s ns s', + transl_stmtlist map al nd nexits nret rret s = OK ns s' -> + state_incr s s'. + +Lemma transl_stmt_stmtlist_incr: + (forall a, transl_stmt_incr_pred a) /\ + (forall al, transl_stmtlist_incr_pred al). +Proof. + apply stmt_stmtlist_ind; + unfold transl_stmt_incr_pred, + transl_stmtlist_incr_pred; + simpl; intros; + try (monadInv H); try (monadInv H0); + try (monadInv H1); try (monadInv H2); + eauto 6 with rtlg. + + generalize H1. case (more_likely c s s0); monadSimpl; eauto 6 with rtlg. + + subst s'. apply update_instr_incr with s1 s2 (Inop n0) n u; + eauto with rtlg. + + generalize H; destruct (nth_error nexits n); monadSimpl. + subst s'; auto with rtlg. + + generalize H. destruct o; destruct rret; try monadSimpl. + eauto with rtlg. + subst s'; auto with rtlg. + subst s'; auto with rtlg. +Qed. + +Lemma transl_stmt_incr: + forall a map nd nexits nret rret s ns s', + transl_stmt map a nd nexits nret rret s = OK ns s' -> + state_incr s s'. +Proof (proj1 transl_stmt_stmtlist_incr). + +Lemma transl_stmtlist_incr: + forall al map nd nexits nret rret s ns s', + transl_stmtlist map al nd nexits nret rret s = OK ns s' -> + state_incr s s'. +Proof (proj2 transl_stmt_stmtlist_incr). + +Hint Resolve transl_stmt_incr transl_stmtlist_incr: rtlg. + |