From 21c979fce33b068ce4b86e67d3d866b203411c6c Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 11 Jun 2021 11:37:41 +0200 Subject: proving the remaining lemma for sexec_rec_okpreserv --- scheduling/BTL_SEsimuref.v | 285 ++++++++++++++++++++++++++------------------- 1 file changed, 162 insertions(+), 123 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v index 852bced0..da680e63 100644 --- a/scheduling/BTL_SEsimuref.v +++ b/scheduling/BTL_SEsimuref.v @@ -31,7 +31,9 @@ Record ristate := ris_smem: smem; (** For the values in registers: 1) we store a list of sval evaluations - 2) we encode the symbolic regset by a PTree + a boolean indicating the default sval *) + 2) we encode the symbolic regset by a PTree + a boolean indicating the default sval + See [ris_sreg_get] below. + *) ris_input_init: bool; ok_rsval: list sval; ris_sreg:> PTree.t sval @@ -51,18 +53,32 @@ Record ris_ok ctx (ris: ristate) : Prop := { Local Hint Resolve OK_RMEM OK_RREG: core. Local Hint Constructors ris_ok: core. -(* TODO: Is it useful ? -Definition ris_abs (ris: ristate) : sistate := {| - si_pre := fun ctx => ris_ok ctx ris; - si_sreg := ris_sreg_get ris; - si_smem := ris.(ris_smem) -|}. -*) +(** + NOTE that this refinement relation *cannot* be decomposed into a abstraction function of type + ristate -> sistate & an equivalence relation on istate. + + Indeed, any [sis] satisfies [forall ctx r, si_ok ctx sis -> eval_sval ctx (sis r) <> None]. + whereas this is generally not true for [ris] that [forall ctx r, ris_ok ctx ris -> eval_sval ctx (ris r) <> None], + except when, precisely, [ris_refines ris sis]. + + An alternative design enabling to define ris_refines as the composition of an equivalence on sistate + and a abstraction function would consist in constraining sistate with an additional [wf] field: + Record sistate := + { si_pre: iblock_exec_context -> Prop; + si_sreg:> reg -> sval; + si_smem: smem; + si_wf: forall ctx, si_pre ctx -> si_smem <> None /\ forall r, si_sreg r <> None + }. + + Such a constraint should also appear in [ristate]. This is not clear whether this alternative design + would be really simpler. + +*) Record ris_refines ctx (ris: ristate) (sis: sistate): Prop := { OK_EQUIV: si_ok ctx sis <-> ris_ok ctx ris; MEM_EQ: ris_ok ctx ris -> eval_smem ctx ris.(ris_smem) = eval_smem ctx sis.(si_smem); - REG_EQ: ris_ok ctx ris -> forall r, eval_sval ctx (ris_sreg_get ris r) = eval_sval ctx (si_sreg sis r) + REG_EQ: ris_ok ctx ris -> forall r, eval_sval ctx (ris r) = eval_sval ctx (sis r) }. Local Hint Resolve OK_EQUIV MEM_EQ REG_EQ: core. Local Hint Constructors ris_refines: core. @@ -70,7 +86,7 @@ Local Hint Constructors ris_refines: core. Record ris_simu ris1 ris2: Prop := { SIMU_FAILS: forall sv, List.In sv ris2.(ok_rsval) -> List.In sv ris1.(ok_rsval); SIMU_MEM: ris1.(ris_smem) = ris2.(ris_smem); - SIMU_REG: forall r, ris_sreg_get ris1 r = ris_sreg_get ris2 r + SIMU_REG: forall r, ris1 r = ris2 r }. Local Hint Resolve SIMU_FAILS SIMU_MEM SIMU_REG: core. Local Hint Constructors ris_simu: core. @@ -186,7 +202,6 @@ Inductive rstate := | Rabort . - Record routcome := rout { _ris: ristate; _rfv: sfval; @@ -257,7 +272,7 @@ Proof. destruct b; simpl; auto. Qed. -Lemma rst_refines_outcome_down ctx rst st: +Lemma rst_refines_outcome_okpreserv ctx rst st: rst_refines ctx rst st -> forall sis sfv, get_soutcome ctx st = Some (sout sis sfv) -> @@ -280,7 +295,7 @@ Proof. intros sis1 sfv1 SOUT OK1. exploit REF1; eauto. clear REF1; intros REF1. - exploit rst_refines_outcome_down; eauto. clear REF1 SOUT. + exploit rst_refines_outcome_okpreserv; eauto. clear REF1 SOUT. intros (ris1 & rfv1 & ROUT1 & REFI1 & REFF1). rewrite OK_EQUIV in OK1; eauto. exploit REFF1; eauto. clear REFF1; intros REFF1. @@ -294,7 +309,114 @@ Proof. do 2 eexists; split; eauto. Qed. -(** * Refinement of the symbolic execution *) + +(** * Properties of the (abstract) operators involved in symbolic execution *) + +Lemma ok_set_mem ctx sm sis: + si_ok ctx (set_smem sm sis) + <-> (si_ok ctx sis /\ eval_smem ctx sm <> None). +Proof. + split; destruct 1; econstructor; simpl in *; eauto. + intuition eauto. +Qed. + +Lemma ok_set_sreg ctx r sv sis: + si_ok ctx (set_sreg r sv sis) + <-> (si_ok ctx sis /\ eval_sval ctx sv <> None). +Proof. + unfold set_sreg; split. + + intros [(SVAL & PRE) SMEM SREG]; simpl in *; split. + - econstructor; eauto. + intros r0; generalize (SREG r0); destruct (Pos.eq_dec r r0); try congruence. + - generalize (SREG r); destruct (Pos.eq_dec r r); try congruence. + + intros ([PRE SMEM SREG] & SVAL). + econstructor; simpl; eauto. + intros r0; destruct (Pos.eq_dec r r0); try congruence. +Qed. + +Lemma si_ok_op_okpreserv ctx op args dest sis: si_ok ctx (sexec_op op args dest sis) -> si_ok ctx sis. +Proof. + unfold sexec_op. rewrite ok_set_sreg. intuition. +Qed. + +Lemma si_ok_load_okpreserv ctx chunk addr args dest sis: si_ok ctx (sexec_load TRAP chunk addr args dest sis) -> si_ok ctx sis. +Proof. + unfold sexec_load. rewrite ok_set_sreg. intuition. +Qed. + +Lemma si_ok_store_okpreserv ctx chunk addr args src sis: si_ok ctx (sexec_store chunk addr args src sis) -> si_ok ctx sis. +Proof. + unfold sexec_store. rewrite ok_set_mem. intuition. +Qed. + +Lemma si_ok_tr_okpreserv ctx fi sis: si_ok ctx (tr_sis (cf ctx) fi sis) -> si_ok ctx sis. +Proof. + unfold tr_sis. intros OK; inv OK. simpl in *. intuition. +Qed. + +(* These lemmas are very bad for eauto: we put them into a dedicated basis. *) +Local Hint Resolve si_ok_tr_okpreserv si_ok_op_okpreserv si_ok_load_okpreserv si_ok_store_okpreserv: sis_ok. + +Lemma sexec_rec_okpreserv ctx ib: + forall k + (CONT: forall sis lsis sfv, get_soutcome ctx (k sis) = Some (sout lsis sfv) -> si_ok ctx lsis -> si_ok ctx sis) + sis lsis sfv + (SOUT: get_soutcome ctx (sexec_rec (cf ctx) ib sis k) = Some (sout lsis sfv)) + (OK: si_ok ctx lsis) + ,si_ok ctx sis. +Proof. + induction ib; simpl; try (autodestruct; simpl). + 1-6: try_simplify_someHyps; eauto with sis_ok. + - intros. eapply IHib1. 2-3: eauto. + eapply IHib2; eauto. + - intros k CONT sis lsis sfv. + do 2 autodestruct; eauto. +Qed. + +(* an alternative tr_sis *) + +Definition transfer_sis (inputs: list reg) (sis:sistate): sistate := + {| si_pre := fun ctx => (sis.(si_pre) ctx /\ forall r, eval_sval ctx (sis.(si_sreg) r) <> None); + si_sreg := transfer_sreg inputs sis; + si_smem := sis.(si_smem) |}. + +Lemma ok_transfer_sis ctx inputs sis: + si_ok ctx (transfer_sis inputs sis) + <-> (si_ok ctx sis). +Proof. + unfold transfer_sis. induction inputs as [|r l]; simpl. + + split; destruct 1; econstructor; simpl in *; intuition eauto. congruence. + + split. + * destruct 1; econstructor; simpl in *; intuition eauto. + * intros X; generalize X. rewrite <- IHl in X; clear IHl. + intros [PRE SMEM SREG]. + econstructor; simpl; eauto. + intros r0; destruct (Pos.eq_dec r r0); try congruence. + intros H; eapply OK_SREG; eauto. +Qed. + +Definition alt_tr_sis := poly_tr (fun f tbl or => transfer_sis (Regset.elements (pre_inputs f tbl or))). + +Lemma tr_sis_alt_def f fi sis: + alt_tr_sis f fi sis = tr_sis f fi sis. +Proof. + unfold tr_sis, str_inputs. destruct fi; simpl; auto. +Qed. + + +(** * Refinement of the symbolic execution (e.g. refinement of [sexec] into [rexec]). + +TODO: Est-ce qu'on garde cette vision purement fonctionnelle de l'implementation ? +=> ça pourrait être pratique quand on va compliquer encore le vérificateur ! + +Du coup, on introduirait une version avec hash-consing qui serait en correspondance +pour une relation d'equivalence sur les ristate ? + +Attention toutefois, il est possible que certaines parties de l'execution soient pénibles à formuler +en programmation fonctionnelle pure (exemple: usage de l'égalité de pointeur comme test d'égalité rapide!) + + +*) Local Hint Constructors rfv_refines optrsv_refines rsvident_refines rsvident_refines: core. @@ -361,14 +483,6 @@ Definition rset_smem rm (ris:ristate): ristate := ris_sreg:= ris.(ris_sreg) |}. -Lemma ok_set_mem ctx sm sis: - si_ok ctx (set_smem sm sis) - <-> (si_ok ctx sis /\ eval_smem ctx sm <> None). -Proof. - split; destruct 1; econstructor; simpl in *; eauto. - intuition eauto. -Qed. - Lemma ok_rset_mem ctx rm (ris: ristate): (eval_smem ctx ris.(ris_smem) = None -> eval_smem ctx rm = None) -> ris_ok ctx (rset_smem rm ris) @@ -414,20 +528,6 @@ Definition rset_sreg r rsv (ris:ristate): ristate := ris_sreg:= PTree.set r rsv ris.(ris_sreg) (* TODO: A CHANGER *) |}. -Lemma ok_set_sreg ctx r sv sis: - si_ok ctx (set_sreg r sv sis) - <-> (si_ok ctx sis /\ eval_sval ctx sv <> None). -Proof. - unfold set_sreg; split. - + intros [(SVAL & PRE) SMEM SREG]; simpl in *; split. - - econstructor; eauto. - intros r0; generalize (SREG r0); destruct (Pos.eq_dec r r0); try congruence. - - generalize (SREG r); destruct (Pos.eq_dec r r); try congruence. - + intros ([PRE SMEM SREG] & SVAL). - econstructor; simpl; eauto. - intros r0; destruct (Pos.eq_dec r r0); try congruence. -Qed. - Lemma ok_rset_sreg ctx r rsv ris: ris_ok ctx (rset_sreg r rsv ris) <-> (ris_ok ctx ris /\ eval_sval ctx rsv <> None). @@ -528,26 +628,6 @@ Fixpoint transfer_ris (inputs: list reg) (ris:ristate): ristate := | r::l => rseto_sreg r (ris_sreg_get ris r) (transfer_ris l ris) end. -Definition transfer_sis (inputs: list reg) (sis:sistate): sistate := - {| si_pre := fun ctx => (sis.(si_pre) ctx /\ forall r, eval_sval ctx (sis.(si_sreg) r) <> None); - si_sreg := transfer_sreg inputs sis; - si_smem := sis.(si_smem) |}. - -Lemma ok_transfer_sis ctx inputs sis: - si_ok ctx (transfer_sis inputs sis) - <-> (si_ok ctx sis). -Proof. - unfold transfer_sis. induction inputs as [|r l]; simpl. - + split; destruct 1; econstructor; simpl in *; intuition eauto. congruence. - + split. - * destruct 1; econstructor; simpl in *; intuition eauto. - * intros X; generalize X. rewrite <- IHl in X; clear IHl. - intros [PRE SMEM SREG]. - econstructor; simpl; eauto. - intros r0; destruct (Pos.eq_dec r r0); try congruence. - intros H; eapply OK_SREG; eauto. -Qed. - Lemma ok_transfer_ris ctx inputs ris: ris_ok ctx (transfer_ris inputs ris) <-> (ris_ok ctx ris). @@ -583,14 +663,6 @@ Proof. - rewrite ok_rseto_sreg, ok_transfer_ris. auto. Qed. -Definition alt_tr_sis := poly_tr (fun f tbl or => transfer_sis (Regset.elements (pre_inputs f tbl or))). - -Lemma tr_sis_alt_def f fi sis: - alt_tr_sis f fi sis = tr_sis f fi sis. -Proof. - unfold tr_sis, str_inputs. destruct fi; simpl; auto. -Qed. - Definition tr_ris := poly_tr (fun f tbl or => transfer_ris (Regset.elements (pre_inputs f tbl or))). Local Hint Resolve transfer_ris_correct ok_transfer_ris: core. @@ -603,14 +675,11 @@ Proof. destruct fi; simpl; eauto. Qed. -Lemma ok_tr_ris_imp ctx fi ris: - ris_ok ctx (tr_ris (cf ctx) fi ris) - -> (ris_ok ctx ris). +Lemma ris_ok_tr_okpreserv ctx fi ris: ris_ok ctx (tr_ris (cf ctx) fi ris) -> ris_ok ctx ris. Proof. rewrite ok_tr_ris; auto. Qed. - Lemma tr_ris_correct ctx fi ris sis: ris_refines ctx ris sis -> ris_refines ctx (tr_ris (cf ctx) fi ris) (tr_sis (cf ctx) fi sis). @@ -619,40 +688,6 @@ Proof. destruct fi; simpl; eauto. Qed. -Lemma si_ok_tr_down ctx fi sis: si_ok ctx (tr_sis (cf ctx) fi sis) -> si_ok ctx sis. -Admitted. - -Lemma si_ok_op_down ctx op args dest sis: si_ok ctx (sexec_op op args dest sis) -> si_ok ctx sis. -Admitted. - -Lemma si_ok_trap_down ctx chunk addr args dest sis: si_ok ctx (sexec_load TRAP chunk addr args dest sis) -> si_ok ctx sis. -Admitted. - -Lemma si_ok_store_down ctx chunk addr args src sis: si_ok ctx (sexec_store chunk addr args src sis) -> si_ok ctx sis. -Admitted. - -(* TODO: a revoir: ce n'est pas une bonne idee de mettre ça dans core => ça fait ramer "eauto" !!! *) -Local Hint Resolve si_ok_tr_down si_ok_op_down si_ok_trap_down si_ok_store_down: core. - -Lemma sexec_rec_down ctx ib: - forall k - (CONT: forall sis lsis sfv, get_soutcome ctx (k sis) = Some (sout lsis sfv) -> si_ok ctx lsis -> si_ok ctx sis) - sis lsis sfv - (SOUT: get_soutcome ctx (sexec_rec (cf ctx) ib sis k) = Some (sout lsis sfv)) - (OK: si_ok ctx lsis) - ,si_ok ctx sis. -Proof. - induction ib; simpl; try (autodestruct; simpl). - 1-6: try_simplify_someHyps. - - intros. eapply IHib1. 2-3: eauto. - eapply IHib2; eauto. - - intros k CONT sis lsis sfv. - do 2 autodestruct. - + intros; eapply IHib1; eauto. - + intros; eapply IHib2; eauto. -Qed. - - (** RAFFINEMENT EXEC SYMBOLIQUE **) Fixpoint rexec_rec f ib ris (k: ristate -> rstate): rstate := @@ -678,7 +713,7 @@ Fixpoint rexec_rec f ib ris (k: ristate -> rstate): rstate := Definition rexec f ib := rexec_rec f ib ris_init (fun _ => Rabort). -Local Hint Resolve ris_init_correct exec_final_refpreserv tr_ris_correct ok_tr_ris_imp +Local Hint Resolve ris_init_correct exec_final_refpreserv tr_ris_correct ris_ok_tr_okpreserv rexec_op_correct rexec_load_correct rexec_store_correct: core. Local Hint Constructors rst_refines: core. @@ -699,13 +734,13 @@ Proof. - (* seq *) intros; subst. eapply IHib1. 3-6: eauto. - + simpl. eapply sexec_rec_down; eauto. + + simpl. eapply sexec_rec_okpreserv; eauto. + intros; subst. eapply IHib2; eauto. - (* cond *) intros rk k CONTh CONT ris sis lsis sfv st REF EXEC OUT OK. subst. assert (rOK: ris_ok ctx ris). { erewrite <- OK_EQUIV. 2: eauto. - eapply sexec_rec_down with (ib:=(Bcond cond args ib1 ib2 iinfo)); simpl; eauto. + eapply sexec_rec_okpreserv with (ib:=(Bcond cond args ib1 ib2 iinfo)); simpl; eauto. } generalize OUT; clear OUT; simpl. autodestruct. @@ -725,22 +760,28 @@ Qed. (** COPIER-COLLER ... Y a-t-il moyen de l'eviter ? **) -Lemma ris_ok_tr_down ctx fi ris: ris_ok ctx (tr_ris (cf ctx) fi ris) -> ris_ok ctx ris. -Admitted. - -Lemma ris_ok_op_down ctx op args dest ris: ris_ok ctx (rexec_op op args dest ris) -> ris_ok ctx ris. -Admitted. +Lemma ris_ok_op_okpreserv ctx op args dest ris: ris_ok ctx (rexec_op op args dest ris) -> ris_ok ctx ris. +Proof. + unfold rexec_op. rewrite ok_rset_sreg. intuition. +Qed. -Lemma ris_ok_trap_down ctx chunk addr args dest ris: ris_ok ctx (rexec_load TRAP chunk addr args dest ris) -> ris_ok ctx ris. -Admitted. +Lemma ris_ok_load_okpreserv ctx chunk addr args dest ris: ris_ok ctx (rexec_load TRAP chunk addr args dest ris) -> ris_ok ctx ris. +Proof. + unfold rexec_load. rewrite ok_rset_sreg. intuition. +Qed. -Lemma ris_ok_store_down ctx chunk addr args src ris: ris_ok ctx (rexec_store chunk addr args src ris) -> ris_ok ctx ris. -Admitted. +Lemma ris_ok_store_okpreserv ctx chunk addr args src ris: ris_ok ctx (rexec_store chunk addr args src ris) -> ris_ok ctx ris. +Proof. + unfold rexec_store. rewrite ok_rset_mem; simpl. + + intuition. + + intros X; rewrite X; simpl. + repeat autodestruct. +Qed. -(* TODO: a revoir: ce n'est pas une bonne idee de mettre ça dans core => ça fait ramer "eauto" !!! *) -Local Hint Resolve ris_ok_tr_down ris_ok_op_down ris_ok_trap_down ris_ok_store_down: core. +(* These lemmas are very bad for eauto: we put them into a dedicated basis. *) +Local Hint Resolve ris_ok_store_okpreserv ris_ok_op_okpreserv ris_ok_load_okpreserv: ris_ok. -Lemma rexec_rec_down ctx ib: +Lemma rexec_rec_okpreserv ctx ib: forall k (CONT: forall ris lris rfv, get_routcome ctx (k ris) = Some (rout lris rfv) -> ris_ok ctx lris -> ris_ok ctx ris) ris lris rfv @@ -749,13 +790,11 @@ Lemma rexec_rec_down ctx ib: ,ris_ok ctx ris. Proof. induction ib; simpl; try (autodestruct; simpl). - 1-6: try_simplify_someHyps. + 1-6: try_simplify_someHyps; eauto with ris_ok. - intros. eapply IHib1. 2-3: eauto. eapply IHib2; eauto. - intros k CONT sis lsis sfv. - do 2 autodestruct. - + intros; eapply IHib1; eauto. - + intros; eapply IHib2; eauto. + do 2 autodestruct; eauto. Qed. Lemma rexec_rec_correct2 ctx ib: @@ -774,12 +813,12 @@ Proof. - (* seq *) intros; subst. eapply IHib1. 3-6: eauto. - + simpl. eapply rexec_rec_down; eauto. + + simpl. eapply rexec_rec_okpreserv; eauto. + intros; subst. eapply IHib2; eauto. - (* cond *) intros rk k CONTh CONT ris sis lsis sfv st REF EXEC OUT OK. subst. assert (OK0: ris_ok ctx ris). { - eapply rexec_rec_down with (ib:=(Bcond cond args ib1 ib2 iinfo)); simpl; eauto. + eapply rexec_rec_okpreserv with (ib:=(Bcond cond args ib1 ib2 iinfo)); simpl; eauto. } generalize OUT; clear OUT; simpl. autodestruct. -- cgit