From 9b74954477b9b1e5b75fbdd15215fc09941f72e4 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 1 Jun 2021 12:18:51 +0200 Subject: Lemma liveness_checker_correct --- scheduling/BTL_Livecheck.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'scheduling') diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v index 62833dc3..6015d91f 100644 --- a/scheduling/BTL_Livecheck.v +++ b/scheduling/BTL_Livecheck.v @@ -126,6 +126,18 @@ Definition liveness_checker (f: BTL.function): res unit := | false => Error (msg "BTL_Livecheck: liveness_checker failed") end. +Lemma liveness_checker_correct f n ibf: + liveness_checker f = OK tt -> + f.(fn_code)!n = Some ibf -> + iblock_checker f.(fn_code) ibf.(entry) ibf.(input_regs) = Some tt. +Proof. + unfold liveness_checker. + destruct list_iblock_checker eqn:EQL; try congruence. + intros _ P. exploit list_iblock_checker_correct; eauto. + - eapply PTree.elements_correct; eauto. + - simpl; auto. +Qed. + Definition liveness_ok_function (f: BTL.function): Prop := liveness_checker f = OK tt. (** TODO: adapt stuff RTLpathLivegenproof *) -- cgit