diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-03 13:55:15 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-03 13:55:15 +0200 |
| commit | cc5f8c4e4d71d824a4d1818745d6bf1015b98f98 (patch) | |
| tree | c690b6132bcb052856a2f43a9705c2f6a394f4ed /scheduling/BTLtoRTLproof.v | |
| parent | dcaec659404e11fd927b5e8af3e44958d4c6c950 (diff) | |
| download | compcert-kvx-cc5f8c4e4d71d824a4d1818745d6bf1015b98f98.tar.gz compcert-kvx-cc5f8c4e4d71d824a4d1818745d6bf1015b98f98.zip | |
une autre suggestion
Diffstat (limited to 'scheduling/BTLtoRTLproof.v')
| -rw-r--r-- | scheduling/BTLtoRTLproof.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 7f6f21c7..ab3cab69 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -106,6 +106,20 @@ Proof. intros. inv H0. inv H. inv STACKS. constructor. Qed. +(* suggestion *) +Lemma iblock_stepi_simulation sp dupmap stack' f' rs0 m0 ib rs1 m1 ofin + (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 ofin): + forall cfg' pc0 opc isfst + (MIB: match_iblock dupmap cfg' isfst pc0 ib opc) + , + match ofin with + | None => exists pc1,(opc = Some pc1) /\ plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1) + | Some fin => True (* TODO: A CHANGER *) + end. +Proof. + induction IBIS; simpl; auto. +Admitted. + Inductive iblock_istep_gen sp dupmap stack f rs0 m0 pc0 cfg: state -> trace -> bool -> option final -> option node -> Prop := | ibis_synced ib rs1 m1 opc pc1 (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 None) |