diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-09 11:34:35 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-09 11:34:35 +0100 |
| commit | 79c039d7b33878d00f22ad8542dc30a78aa8b70a (patch) | |
| tree | 21f23b7ba1dff669281f618fc9aaadd91654908c /backend/CSE3proof.v | |
| parent | a0529ae7a4eb991c39f258a8dbc003dd83ad3d36 (diff) | |
| download | compcert-kvx-79c039d7b33878d00f22ad8542dc30a78aa8b70a.tar.gz compcert-kvx-79c039d7b33878d00f22ad8542dc30a78aa8b70a.zip | |
CSE3 + conditions proof
Diffstat (limited to 'backend/CSE3proof.v')
| -rw-r--r-- | backend/CSE3proof.v | 67 |
1 files changed, 34 insertions, 33 deletions
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index cc4ab686..50a32d56 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -352,6 +352,23 @@ Qed. Hint Resolve rel_ge : cse3. +Lemma relb_ge: + forall inv inv' + (GE : RB.ge inv' inv) + ctx sp rs m + (REL: sem_rel_b sp ctx inv rs m), + sem_rel_b sp ctx inv' rs m. +Proof. + intros. + destruct inv; cbn in *. + 2: contradiction. + destruct inv'; cbn in *. + 2: assumption. + eapply rel_ge; eassumption. +Qed. + +Hint Resolve relb_ge : cse3. + Lemma sem_rhs_sop : forall sp op rs args m v, eval_operation ge sp op rs ## args m = Some v -> @@ -946,23 +963,15 @@ Proof. rewrite andb_true_iff in IND_step_me. destruct IND_step_me as [IND_so [IND_not ZOT]]. clear ZOT. - destruct (invs # ifso) as [inv_so | ] eqn:INV_so; cbn in *. - 2: discriminate. - destruct (invs # ifnot) as [inv_not | ] eqn:INV_not; cbn in *. - 2: discriminate. - rewrite rel_leb_correct in IND_so. - rewrite rel_leb_correct in IND_not. + rewrite relb_leb_correct in IND_so. + rewrite relb_leb_correct in IND_not. + destruct b. - { - rewrite INV_so. - cbn. - eapply rel_ge; eauto. - } - { - rewrite INV_not. - cbn. - eapply rel_ge; eauto. - } + { eapply relb_ge. eassumption. apply apply_cond_sound; auto. } + eapply relb_ge. eassumption. apply apply_cond_sound; trivial. + rewrite eval_negate_condition. + rewrite H0. + reflexivity. (* END INVARIANT *) } unfold sem_rel_b in REL. @@ -1048,23 +1057,15 @@ Proof. rewrite andb_true_iff in IND_step_me. destruct IND_step_me as [IND_so [IND_not ZOT]]. clear ZOT. - destruct (invs # ifso) as [inv_so | ] eqn:INV_so; cbn in *. - 2: discriminate. - destruct (invs # ifnot) as [inv_not | ] eqn:INV_not; cbn in *. - 2: discriminate. - rewrite rel_leb_correct in IND_so. - rewrite rel_leb_correct in IND_not. + rewrite relb_leb_correct in IND_so. + rewrite relb_leb_correct in IND_not. + destruct b. - { - rewrite INV_so. - cbn. - eapply rel_ge; eauto. - } - { - rewrite INV_not. - cbn. - eapply rel_ge; eauto. - } + { eapply relb_ge. eassumption. apply apply_cond_sound; auto. } + eapply relb_ge. eassumption. apply apply_cond_sound; trivial. + rewrite eval_negate_condition. + rewrite H0. + reflexivity. (* END INVARIANT *) - (* Ijumptable *) @@ -1171,7 +1172,7 @@ Proof. apply wt_regset_assign; trivial. rewrite WTRES0. exact WTRES. -Admitted. +Qed. Lemma transf_initial_states: forall S1, RTL.initial_state prog S1 -> |