diff options
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) |