From 84ddcd68504461bb2dee30ac38f0bb495b8aec38 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 1 Jun 2021 12:11:50 +0200 Subject: Lemma list_iblock_checker_correct --- scheduling/BTL_Livecheck.v | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) (limited to 'scheduling') diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v index 4d556711..62833dc3 100644 --- a/scheduling/BTL_Livecheck.v +++ b/scheduling/BTL_Livecheck.v @@ -100,6 +100,26 @@ Fixpoint list_iblock_checker (btl: code) (l: list (node*iblock_info)): bool := | (_, ibf) :: l' => iblock_checker btl ibf.(entry) ibf.(input_regs) &&& list_iblock_checker btl l' end. +Lemma lazy_and_Some_true A (o: option A) (b: bool): o &&& b = true <-> (exists v, o = Some v) /\ b = true. +Proof. + destruct o; simpl; intuition. + - eauto. + - firstorder. try_simplify_someHyps. +Qed. + +Lemma lazy_and_Some_tt_true (o: option unit) (b: bool): o &&& b = true <-> o = Some tt /\ b = true. +Proof. + intros; rewrite lazy_and_Some_true; firstorder. + destruct x; auto. +Qed. + +Lemma list_iblock_checker_correct btl l: + list_iblock_checker btl l = true -> forall e, List.In e l -> iblock_checker btl (snd e).(entry) (snd e).(input_regs) = Some tt. +Proof. + intros CHECKER e H; induction l as [|(n & ibf) l]; intuition. + simpl in * |- *. rewrite lazy_and_Some_tt_true in CHECKER. intuition (subst; auto). +Qed. + Definition liveness_checker (f: BTL.function): res unit := match list_iblock_checker f.(fn_code) (PTree.elements f.(fn_code)) with | true => OK tt -- cgit