diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-04 10:42:08 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-04 10:42:08 +0200 |
| commit | d44d44c8fffbd85d501e30b7dfdf93683ed9bb4d (patch) | |
| tree | 37a2a1e1a5ae3262f73d55a08a3bdc9c99cb34b9 /scheduling/BTLtoRTLproof.v | |
| parent | 0ed3ee91bad8dc17a77d742ed9c43742c0a833ba (diff) | |
| download | compcert-kvx-d44d44c8fffbd85d501e30b7dfdf93683ed9bb4d.tar.gz compcert-kvx-d44d44c8fffbd85d501e30b7dfdf93683ed9bb4d.zip | |
proof for Icond in iblock_istep
Diffstat (limited to 'scheduling/BTLtoRTLproof.v')
| -rw-r--r-- | scheduling/BTLtoRTLproof.v | 32 |
1 files changed, 31 insertions, 1 deletions
diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 31652697..8df8ef1e 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -179,7 +179,37 @@ Proof. eapply plus_trans; eauto. - inv MIB. destruct b; exploit IHIBIS; eauto. -Admitted. + + (* taking ifso *) + destruct ofin; simpl. + * (* ofin is Some final *) + intros (isfst' & pc1 & MI & STAR). + repeat eexists; eauto. + eapply css_plus_trans. + eapply plus_one. eapply exec_Icond; eauto. + eauto. + * (* ofin is None *) + intros (pc1 & OPC & PLUS). inv OPC. + inv H10; eexists; split; eauto. + all: + eapply plus_trans; + [ eapply plus_one; eapply exec_Icond; eauto + | eauto | eauto ]. + + (* taking ifnot *) + destruct ofin; simpl. + * (* ofin is Some final *) + intros (isfst' & pc1 & MI & STAR). + repeat eexists; eauto. + eapply css_plus_trans. + eapply plus_one. eapply exec_Icond; eauto. + eauto. + * (* ofin is None *) + intros (pc1 & OPC & PLUS). inv OPC. + inv H10; eexists; split; eauto. + all: + eapply plus_trans; + [ eapply plus_one; eapply exec_Icond; eauto + | eauto | eauto ]. +Qed. Lemma iblock_step_simulation sp dupmap stack stack' f f' ib rs0 m0 rs1 m1 pc0 fin t s (STACKS: list_forall2 match_stackframes stack stack') |