proposition: Theorem regalloc_correct_terminating: forall s c s', cexec s c s' -> forall L s1, agree' (live c L) s s1 -> correct_allocation c L = true -> exists s1', cexec s1 (regalloc c L) s1' /\ agree' L s' s1'.
proof: Proof. induction 1; intros L s1 AG CORR. - exists s1; split. constructor. auto. - cbn in *. destruct (IdentSet.mem x L) eqn:is_live. + destruct (expr_is_var a) as [y|] eqn:is_var. * apply expr_is_var_correct in is_var. subst a. assert (NONINTF: forall z, IdentSet.In z L -> z <> x -> z <> y -> f z <> f x). { apply IdentSet.for_all_2 in CORR. - intros. apply CORR in H. destruct (String.eqb_spec z x). congruence. destruct (String.eqb_spec z y). congruence. destruct (String.eqb_spec (f z) (f x)). discriminate. auto. - hnf. intros; congruence. } destruct (string_dec (f x) (f y)). ** econstructor; split. apply cexec_skip. apply agree'_update_coalesced_move; auto. ** econstructor; split. apply cexec_assign. apply agree'_update_move; auto. * assert (EVAL: aeval a s = aeval (rename_aexp a) s1) by (eapply aeval_agree'; eapply agree'_mon; eauto; fsetdec). assert (NONINTF: forall z, IdentSet.In z L -> z <> x -> f z <> f x). { apply IdentSet.for_all_2 in CORR. - intros. apply CORR in H. destruct (String.eqb_spec z x). congruence. destruct (String.eqb_spec (f z) (f x)). discriminate. auto. - hnf. intros; congruence. } econstructor; split. apply cexec_assign. rewrite <- EVAL. apply agree'_update_live; auto. eapply agree'_mon; eauto. fsetdec. + econstructor; split. apply cexec_skip. apply agree'_update_dead. auto. red; intros. assert (IdentSet.mem x L = true) by (apply IdentSet.mem_1; auto). congruence. - cbn in *. apply andb_prop in CORR; destruct CORR as [CORR1 CORR2]. destruct (IHcexec1 _ _ AG CORR1) as (s1' & EXEC1 & AG1). destruct (IHcexec2 _ _ AG1 CORR2) as (s2' & EXEC2 & AG2). exists s2'; split. apply cexec_seq with s1'; auto. auto. - cbn in *. apply andb_prop in CORR; destruct CORR as [CORR1 CORR2]. assert (EVAL: beval b s = beval (rename_bexp b) s1) by (eapply beval_agree'; eapply agree'_mon; eauto; fsetdec). destruct (IHcexec L s1) as (s1' & EXEC' & AG'). eapply agree_mon; eauto. destruct (beval b s); fsetdec. destruct (beval b s); auto. exists s1'; split. apply cexec_ifthenelse. rewrite <- EVAL. destruct (beval b s); auto. auto. - Local Opaque live. cbn in *. destruct (live_while_charact b c L) as (P & Q & R). assert (EVAL: beval b s = beval (rename_bexp b) s1) by (eapply beval_agree'; eapply agree'_mon; eauto; fsetdec). exists s1; split. apply cexec_while_done. congruence. eapply agree_mon; eauto. - cbn in *. destruct (live_while_charact b c L) as (P & Q & R). assert (EVAL: beval b s = beval (rename_bexp b) s1) by (eapply beval_agree'; eapply agree'_mon; eauto; fsetdec). destruct (IHcexec1 (live (WHILE b c) L) s1) as (s1' & EXEC1 & AG1). eapply agree_mon; eauto. auto. destruct (IHcexec2 L s1') as (s2' & EXEC2 & AG2). auto. auto. exists s2'; split. apply cexec_while_loop with s1'; auto. congruence. auto. Local Transparent live. Qed.
imports: Coq(ZArith Psatz Bool String Program.Equality FSets Wellfounded) CDF(Sequences IMP Simulation)