From bc9aefec03c38caf5d0bc6f0c866159ce7ea4e24 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 25 Aug 2020 11:23:03 +0200 Subject: hfinal_refines depend on ge, sp, rs0, m0 --- kvx/lib/RTLpathSE_impl_junk.v | 98 +++++++++++++++++++++++++++++++++++-------- 1 file changed, 81 insertions(+), 17 deletions(-) (limited to 'kvx') diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v index 5009a91b..c2baa880 100644 --- a/kvx/lib/RTLpathSE_impl_junk.v +++ b/kvx/lib/RTLpathSE_impl_junk.v @@ -1168,12 +1168,75 @@ Definition hfinal_proj hfv := match hfv with | HSreturn oh => Sreturn (option_hsval_proj oh) end. -Definition hfinal_refines (hfv: hsfval) (fv: sfval) := (hfinal_proj hfv) = fv. +Section HFINAL_REFINES. + +Variable ge: RTL.genv. +Variable sp: val. +Variable rs0: regset. +Variable m0: mem. + +Definition sval_refines (hv: hsval) (sv: sval) := seval_hsval ge sp hv rs0 m0 = seval_sval ge sp sv rs0 m0. + +Definition sum_refines (hsi: hsval + ident) (si: sval + ident) := + match hsi, si with + | inl hv, inl sv => sval_refines hv sv + | inr id, inr id' => id = id' + | _, _ => False + end. + +Inductive list_refines: hlist_sval -> list_sval -> Prop := + | hsnil_ref: forall h, list_refines (HSnil h) Snil + | hscons_ref: forall lhv lsv hv sv h, + list_refines lhv lsv -> + sval_refines hv sv -> + list_refines (HScons hv lhv h) (Scons sv lsv). + +Inductive barg_refines: builtin_arg hsval -> builtin_arg sval -> Prop := + | hba_ref: forall hsv sv, sval_refines hsv sv -> barg_refines (BA hsv) (BA sv) + | hba_splitlong: forall bha1 bha2 ba1 ba2, + barg_refines bha1 ba1 -> barg_refines bha2 ba2 -> + barg_refines (BA_splitlong bha1 bha2) (BA_splitlong ba1 ba2) + | hba_addptr: forall bha1 bha2 ba1 ba2, + barg_refines bha1 ba1 -> barg_refines bha2 ba2 -> + barg_refines (BA_addptr bha1 bha2) (BA_addptr ba1 ba2) + | hba_int: forall i, barg_refines (BA_int i) (BA_int i) + | hba_long: forall l, barg_refines (BA_long l) (BA_long l) + | hba_float: forall f, barg_refines (BA_float f) (BA_float f) + | hba_single: forall s, barg_refines (BA_single s) (BA_single s) + | hba_loadstack: forall chk ptr, barg_refines (BA_loadstack chk ptr) (BA_loadstack chk ptr) + | hba_addrstack: forall ptr, barg_refines (BA_addrstack ptr) (BA_addrstack ptr) + | hba_loadglobal: forall chk id ptr, barg_refines (BA_loadglobal chk id ptr) (BA_loadglobal chk id ptr) + | hba_addrglobal: forall id ptr, barg_refines (BA_addrglobal id ptr) (BA_addrglobal id ptr). + +Definition option_refines ohsv osv := + match ohsv, osv with + | Some hsv, Some sv => sval_refines hsv sv + | None, None => True + | _, _ => False + end. + +Inductive hfinal_refines: hsfval -> sfval -> Prop := + | hsnone_ref: hfinal_refines HSnone Snone + | hscall_ref: forall hros ros hargs args s r pc, + sum_refines hros ros -> + list_refines hargs args -> + hfinal_refines (HScall s hros hargs r pc) (Scall s ros args r pc) + | hstailcall_ref: forall hros ros hargs args s, + sum_refines hros ros -> + list_refines hargs args -> + hfinal_refines (HStailcall s hros hargs) (Stailcall s ros args) + | hsbuiltin_ref: forall ef lbha lba br pc, + list_forall2 barg_refines lbha lba -> + hfinal_refines (HSbuiltin ef lbha br pc) (Sbuiltin ef lba br pc) + | hsjumptable_ref: forall hsv sv lpc, + sval_refines hsv sv -> hfinal_refines (HSjumptable hsv lpc) (Sjumptable sv lpc) + | hsreturn_ref: forall ohsv osv, + option_refines ohsv osv -> hfinal_refines (HSreturn ohsv) (Sreturn osv). Remark hfinal_refines_snone: hfinal_refines HSnone Snone. -Proof. - reflexivity. -Qed. +Proof. constructor. Qed. + +End HFINAL_REFINES. Definition final_simu_core (dm: PTree.t node) (f: RTLpath.function) (pc1 pc2: node) (f1 f2: sfval): Prop := match f1 with @@ -1216,12 +1279,13 @@ Qed. Theorem hfinal_simu_core_correct dm f ctx opc1 opc2 hf1 hf2 f1 f2: hfinal_simu_core dm f opc1 opc2 hf1 hf2 -> - hfinal_refines hf1 f1 -> - hfinal_refines hf2 f2 -> + hfinal_refines (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hf1 f1 -> + hfinal_refines (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hf2 f2 -> sfval_simu dm f opc1 opc2 ctx f1 f2. Proof. intros CORE FREF1 FREF2. - rewrite <- FREF1. rewrite <- FREF2. clear FREF1. clear FREF2. (* FIXME - to change when the refinement is more complex *) +Admitted. (* TODO - prove it *) +(* rewrite <- FREF1. rewrite <- FREF2. clear FREF1. clear FREF2. (* FIXME - to change when the refinement is more complex *) destruct hf1. (* Snone *) - destruct hf2; try contradiction. simpl. inv CORE. constructor. assumption. @@ -1243,7 +1307,7 @@ Proof. erewrite <- seval_preserved; [| eapply ctx]. constructor. (* Sreturn *) - destruct hf2; inv CORE. simpl. rewrite H0. constructor. -Qed. +Qed. *) Definition hsexec_final (i: instruction) (hst: PTree.t hsval): ?? hsfval := match i with @@ -1269,16 +1333,15 @@ Definition hsexec_final (i: instruction) (hst: PTree.t hsval): ?? hsfval := | _ => RET (HSnone) end. -(** TODO - figure out how to prove that stuff *) -Lemma hsexec_final_correct hsl sl i: - (forall ge sp rs0 m0, hsilocal_refines ge sp rs0 m0 hsl sl) -> +Lemma hsexec_final_correct ge sp rs0 m0 hsl sl i: + hsilocal_refines ge sp rs0 m0 hsl sl -> WHEN hsexec_final i hsl ~> hsf THEN - hfinal_refines hsf (sexec_final i sl). + hfinal_refines ge sp rs0 m0 hsf (sexec_final i sl). Proof. - destruct i; simpl; intros HLREF; try (wlp_simplify; apply hfinal_refines_snone). +(* destruct i; simpl; intros HLREF; try (wlp_simplify; apply hfinal_refines_snone). (* Scall *) - wlp_step_bind svos SVOS. wlp_step_bind sargs SARGS. wlp_intros hsf HSF. - apply mayRet_ret in HSF. subst. unfold hfinal_refines. simpl. + apply mayRet_ret in HSF. subst. unfold hfinal_refines. simpl. *) (* + intro. inv H. constructor; auto. @@ -1371,8 +1434,9 @@ Global Opaque hfinal_simu_core. Definition hsstate_refines (hst: hsstate) (st:sstate): Prop := hsistate_refines_stat (hinternal hst) (internal st) - /\ (forall ge sp rs0 m0, hsistate_refines_dyn ge sp rs0 m0 (hinternal hst) (internal st)) - /\ hfinal_refines (hfinal hst) (final st). + /\ (forall ge sp rs0 m0, hsistate_refines_dyn ge sp rs0 m0 (hinternal hst) (internal st) + /\ hfinal_refines ge sp rs0 m0 (hfinal hst) (final st)) +. Definition hsstate_simu_core (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) := hsistate_simu_core dm f (hinternal hst1) (hinternal hst2) @@ -1392,7 +1456,7 @@ Proof. assert (PCEQ: dm ! (hsi_pc hst2) = Some (hsi_pc hst1)) by apply SCORE. eapply hsistate_simu_core_correct in SCORE. eapply hfinal_simu_core_correct in FSIMU; eauto. - constructor; [apply SCORE; auto|]. + constructor; [apply SCORE; auto|]. 1-2: eassumption. destruct SREF1 as (PC1 & _). destruct SREF2 as (PC2 & _). rewrite <- PC1. rewrite <- PC2. eapply FSIMU. Qed. -- cgit