diff options
Diffstat (limited to 'scheduling/BTL_SEimpl.v')
| -rw-r--r-- | scheduling/BTL_SEimpl.v | 29 |
1 files changed, 19 insertions, 10 deletions
diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v index 34f8eb1f..d6cdff59 100644 --- a/scheduling/BTL_SEimpl.v +++ b/scheduling/BTL_SEimpl.v @@ -1459,22 +1459,21 @@ Qed. Hint Resolve rst_simu_check_correct: wlp. Global Opaque rst_simu_check. -(* TODO do we really need both functions *) -Definition simu_check_single (f1 f2: function) (ib1 ib2: iblock): ?? unit := +Definition simu_check_single (f1 f2: function) (ibf1 ibf2: iblock_info): ?? unit := (* creating the hash-consing tables *) DO hC_sval <~ hCons hSVAL;; DO hC_list_hsval <~ hCons hLSVAL;; DO hC_hsmem <~ hCons hSMEM;; let hrexec := hrexec hC_sval.(hC) hC_list_hsval.(hC) hC_hsmem.(hC) in (* performing the hash-consed executions *) - DO hst1 <~ hrexec f1 ib1;; - DO hst2 <~ hrexec f2 ib2;; + DO hst1 <~ hrexec f1 ibf1.(entry);; + DO hst2 <~ hrexec f2 ibf2.(entry);; (* comparing the executions *) rst_simu_check hst1 hst2. -Lemma simu_check_single_correct (f1 f2: function) (ib1 ib2: iblock): - WHEN simu_check_single f1 f2 ib1 ib2 ~> _ THEN - symbolic_simu f1 f2 ib1 ib2. +Lemma simu_check_single_correct (f1 f2: function) (ibf1 ibf2: iblock_info): + WHEN simu_check_single f1 f2 ibf1 ibf2 ~> _ THEN + symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry). Proof. (* TODO *) unfold symbolic_simu; wlp_simplify. eapply rst_simu_correct; eauto. @@ -1487,12 +1486,12 @@ Global Hint Resolve simu_check_single_correct: wlp. Program Definition aux_simu_check (f1 f2: function) (ibf1 ibf2: iblock_info): ?? bool := DO r <~ (TRY - simu_check_single f1 f2 ibf1.(entry) ibf2.(entry);; + simu_check_single f1 f2 ibf1 ibf2;; RET true CATCH_FAIL s, _ => println ("simu_check_failure:" +; s);; RET false - ENSURE (fun b => b=true -> ibf1.(input_regs) = ibf2.(input_regs) -> symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry)));; + ENSURE (fun b => b=true -> symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry)));; RET (`r). Obligation 1. split; wlp_simplify. discriminate. @@ -1500,7 +1499,7 @@ Qed. Lemma aux_simu_check_correct (f1 f2: function) (ibf1 ibf2: iblock_info): WHEN aux_simu_check f1 f2 ibf1 ibf2 ~> b THEN - b=true -> ibf1.(input_regs) = ibf2.(input_regs) -> symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry). + b=true -> symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry). Proof. unfold aux_simu_check; wlp_simplify. destruct exta; simpl; auto. @@ -1515,3 +1514,13 @@ Definition simu_check (f1 f2: function) (ibf1 ibf2: iblock_info): res unit := | Some true => OK tt | _ => Error (msg "simu_check has failed") end. + +Lemma simu_check_correct f1 f2 ibf1 ibf2: + simu_check f1 f2 ibf1 ibf2 = OK tt -> + symbolic_simu f1 f2 ibf1.(entry) ibf2.(entry). +Proof. + unfold simu_check. + destruct (unsafe_coerce (aux_simu_check f1 f2 ibf1 ibf2)) as [[|]|] eqn:Hres; simpl; try discriminate. + intros; eapply aux_simu_check_correct; eauto. + eapply unsafe_coerce_not_really_correct; eauto. +Qed. |