From a7e62465b8684714fb4658d4ac1d7b69051b9be4 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Mon, 24 Aug 2020 12:21:51 +0200 Subject: Avancement sur simu_check_single_correct --- kvx/lib/RTLpathSE_impl_junk.v | 51 ++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 50 insertions(+), 1 deletion(-) (limited to 'kvx') diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v index 2a759ebb..6170318b 100644 --- a/kvx/lib/RTLpathSE_impl_junk.v +++ b/kvx/lib/RTLpathSE_impl_junk.v @@ -1350,6 +1350,33 @@ Qed. Hint Resolve hsstate_simu_check_correct: wlp. Global Opaque hsstate_simu_core. +(** Correctness of hsexec *) + +(* Local Hint Resolve init_hsistate_correct_stat init_hsistate_correct_dyn hsexec_final_correct + hsiexec_inst_correct_dyn hsiexec_path_correct_dyn hfinal_refines_snone: core. *) + +Lemma hsexec_correct f pc: + WHEN hsexec f pc ~> hst THEN + exists st, sexec f pc = Some st /\ hsstate_refines hst st. +Proof. Admitted. +(* unfold hsexec. intro. explore_hyp. + unfold sexec. + rewrite EQ. + exploit hsiexec_path_correct_stat; eauto. + intros (st0 & SPATH & REF0). + generalize REF0; intros (PC0 & XREF0). rewrite SPATH. + erewrite <- PC0. rewrite EQ1. + destruct (hsiexec_inst i h) eqn:HINST. + + exploit hsiexec_inst_correct_stat; eauto. + intros (st1 & EQ2 & PC2 & REF2). + - split; eauto. + - rewrite EQ2. + repeat (econstructor; simpl; eauto). + + erewrite hsiexec_inst_correct_None; eauto. + repeat (econstructor; simpl; eauto). + unfold hfinal_refines. simpl; eauto. +Qed. *) + End CanonBuilding. Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) (m: node * node): ?? unit := @@ -1365,11 +1392,33 @@ Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpa (* comparing the executions *) hsstate_simu_check dm f hst1 hst2. +Ltac wlp_intros varname hname := apply wlp_unfold; intros varname hname. + +Ltac wlp_step_bind varname hname := apply wlp_bind; wlp_intros varname hname. + Lemma simu_check_single_correct dm tf f pc1 pc2: WHEN simu_check_single dm f tf (pc2, pc1) ~> _ THEN sexec_simu dm f tf pc1 pc2. Proof. - wlp_simplify. (* TODO *) + unfold simu_check_single. + wlp_step_bind hC_sval HSVAL. wlp_step_bind hC_hlist_sval HLSVAL. + wlp_step_bind hC_hsmem HSMEM. wlp_step_bind hst1 HSEXEC1. wlp_step_bind hst2 HSEXEC2. + wlp_intros u HSIMU. + unfold sexec_simu. intros st1 SEXEC. explore. + assert (TODO1: forall hs hsv rhsv, hdata hs = hsv -> hC hC_sval hs ~~> rhsv -> hsval_proj hsv = hsval_proj rhsv) + by admit. + assert (TODO2: forall hs hsv rhsv, hdata hs = hsv -> hC hC_hlist_sval hs ~~> rhsv -> hsval_list_proj hsv = hsval_list_proj rhsv) + by admit. + assert (TODO3: forall hs hsv rhsv, hdata hs = hsv -> hC hC_hsmem hs ~~> rhsv -> hsmem_proj hsv = hsmem_proj rhsv) + by admit. + exploit hsexec_correct; eauto. + intros (st2 & SEXEC2 & REF2). + exploit hsexec_correct. 4: eapply HSEXEC1. all: eauto. + intros (st0 & SEXEC1 & REF1). + rewrite SEXEC1 in SEXEC. inv SEXEC. + eexists. split; eauto. + intros ctx. eapply hsstate_simu_check_correct in HSIMU; eauto. + eapply hsstate_simu_core_correct; eauto. Admitted. Global Opaque simu_check_single. Global Hint Resolve simu_check_single_correct: wlp. -- cgit