diff options
Diffstat (limited to 'scheduling/BTLtoRTLproof.v')
| -rw-r--r-- | scheduling/BTLtoRTLproof.v | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 904b3814..97ac75fb 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 pc0 cfg ib: trace -> bool -> option final -> option node -> Prop := | ibis_synced opc pc1 (HOPC: opc = Some pc1) @@ -117,9 +131,6 @@ Inductive iblock_istep_gen sp dupmap stack f pc0 cfg ib: trace -> bool -> option (FS : final_step ge stack f sp rs1 m1 fin t s) : iblock_istep_gen sp dupmap stack f pc0 cfg ib t false ofin None. -(*Lemma iblock_istep_gen_correct *) -(*TODO *) - Lemma iblock_step_simulation sp dupmap stack stack' f f' rs0 m0 rs1 m1 ib ofin pc0 opc t s isfst (STACKS: list_forall2 match_stackframes stack stack') |