From f2d2bbd4a759024b716cc7f802427fdb78edfb9d Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 25 Oct 2022 17:43:00 +0100 Subject: Add proofs for sem_pexpr and app_predicated --- src/common/NonEmpty.v | 1 + src/hls/GiblePargenproof.v | 312 ++++++++++++++++++++++++++++++++++++++------- 2 files changed, 270 insertions(+), 43 deletions(-) diff --git a/src/common/NonEmpty.v b/src/common/NonEmpty.v index 923a637..31adbda 100644 --- a/src/common/NonEmpty.v +++ b/src/common/NonEmpty.v @@ -62,6 +62,7 @@ Fixpoint non_empty_prod {A B} (l: non_empty A) (l': non_empty B) := Fixpoint of_list {A} (l: list A): option (non_empty A) := match l with + | a::nil => Some (singleton a) | a::b => match of_list b with | Some b' => Some (a ::| b') diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v index 4597b4d..980ea22 100644 --- a/src/hls/GiblePargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -475,15 +475,202 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. rewrite eval_predf_negate. rewrite H0. auto. Qed. - Lemma sem_pred_expr_updated : - forall A ctx f_p y x v p n ps, + Lemma sem_pexpr_negate : + forall A ctx p b, + sem_pexpr ctx p b -> + @sem_pexpr A ctx (¬ p) (negb b). + Proof. + induction p; crush. + - destruct_match. destruct b0; crush. inv Heqp0. + constructor. inv H. rewrite negb_involutive. auto. + constructor. inv H. auto. + - inv H. constructor. + - inv H. constructor. + - inv H. eapply IHp1 in H2. eapply IHp2 in H4. rewrite negb_andb. + constructor; auto. + - inv H. rewrite negb_orb. constructor; auto. + Qed. + + Lemma sem_pexpr_evaluable : + forall A ctx f_p ps, + (forall x, sem_pexpr ctx (get_forest_p' x f_p) ps !! x) -> + forall p, exists b, @sem_pexpr A ctx (from_pred_op f_p p) b. + Proof. + induction p; crush. + - destruct_match. inv Heqp0. destruct b. econstructor. eauto. + econstructor. eapply sem_pexpr_negate. eauto. + - econstructor. constructor. + - econstructor. constructor. + - econstructor. constructor; eauto. + - econstructor. constructor; eauto. + Qed. + + Lemma sem_pexpr_eval1 : + forall A ctx f_p ps, + (forall x, sem_pexpr ctx (get_forest_p' x f_p) ps !! x) -> + forall p, + eval_predf ps p = false -> + @sem_pexpr A ctx (from_pred_op f_p p) false. + Proof. + induction p; crush. + - destruct_match. inv Heqp0. + destruct b. + + cbn in H0. rewrite <- H0. + rewrite Pos2Nat.id. eauto. + + replace false with (negb true) by auto. + apply sem_pexpr_negate. cbn in H0. + apply negb_true_iff in H0. rewrite negb_involutive in H0. + rewrite <- H0. rewrite Pos2Nat.id. + eauto. + - constructor. + - rewrite eval_predf_Pand in H0. + apply andb_false_iff in H0. inv H0. eapply IHp1 in H1. + pose proof (sem_pexpr_evaluable _ _ _ _ H p2) as EVAL. + inversion_clear EVAL as [x EVAL2]. + replace false with (false && x) by auto. + constructor; auto. + eapply IHp2 in H1. + pose proof (sem_pexpr_evaluable _ _ _ _ H p1) as EVAL. + inversion_clear EVAL as [x EVAL2]. + replace false with (x && false) by eauto with bool. + constructor; auto. + - rewrite eval_predf_Por in H0. + apply orb_false_iff in H0. inv H0. + replace false with (false || false) by auto. + constructor; auto. + Qed. + + Lemma sem_pexpr_eval2 : + forall A ctx f_p ps, + (forall x, sem_pexpr ctx (get_forest_p' x f_p) ps !! x) -> + forall p, + eval_predf ps p = true -> + @sem_pexpr A ctx (from_pred_op f_p p) true. + Proof. + induction p; crush. + - destruct_match. inv Heqp0. + destruct b. + + cbn in H0. rewrite <- H0. + rewrite Pos2Nat.id. eauto. + + replace true with (negb false) by auto. + apply sem_pexpr_negate. cbn in H0. + apply negb_true_iff in H0. + rewrite <- H0. rewrite Pos2Nat.id. + eauto. + - constructor. + - rewrite eval_predf_Pand in H0. + apply andb_true_iff in H0. inv H0. + replace true with (true && true) by auto. + constructor; auto. + - rewrite eval_predf_Por in H0. + apply orb_true_iff in H0. inv H0. eapply IHp1 in H1. + pose proof (sem_pexpr_evaluable _ _ _ _ H p2) as EVAL. + inversion_clear EVAL as [x EVAL2]. + replace true with (true || x) by auto. + constructor; auto. + eapply IHp2 in H1. + pose proof (sem_pexpr_evaluable _ _ _ _ H p1) as EVAL. + inversion_clear EVAL as [x EVAL2]. + replace true with (x || true) by eauto with bool. + constructor; auto. + Qed. + + Lemma sem_pexpr_eval : + forall A ctx f_p ps b, + (forall x, sem_pexpr ctx (get_forest_p' x f_p) ps !! x) -> + forall p, + eval_predf ps p = b -> + @sem_pexpr A ctx (from_pred_op f_p p) b. + Proof. + intros; destruct b; eauto using sem_pexpr_eval1, sem_pexpr_eval2. + Qed. + + Lemma sem_pred_expr_NEapp : + forall A f_p ctx a b v, + sem_pred_expr f_p sem_value ctx a v -> + @sem_pred_expr A _ _ f_p sem_value ctx (NE.app a b) v. + Proof. + induction a; crush. + - inv H. constructor; auto. + - inv H. constructor; eauto. + eapply sem_pred_expr_cons_false; eauto. + Qed. + + Lemma sem_pred_expr_NEapp2 : + forall A f_p ctx a b v ps, + (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) -> + (forall x, NE.In x a -> eval_predf ps (fst x) = false) -> + sem_pred_expr f_p sem_value ctx b v -> + @sem_pred_expr A _ _ f_p sem_value ctx (NE.app a b) v. + Proof. + induction a; crush. + - assert (IN: NE.In a (NE.singleton a)) by constructor. + specialize (H0 _ IN). destruct a. + eapply sem_pred_expr_cons_false; eauto. cbn [fst] in *. + eapply sem_pexpr_eval; eauto. + - assert (NE.In a (NE.cons a a0)) by (constructor; tauto). + apply H0 in H2. + destruct a. cbn [fst] in *. + eapply sem_pred_expr_cons_false. + eapply sem_pexpr_eval; eauto. eapply IHa; eauto. + intros. eapply H0. constructor; tauto. + Qed. + + Lemma sem_pred_expr_map_not : + forall A p ps y x0, + eval_predf ps p = false -> + NE.In x0 (NE.map (fun x => (p ∧ fst x, snd x)) y) -> + eval_predf ps (@fst _ A x0) = false. + Proof. + induction y; crush. + - inv H0. simplify. rewrite eval_predf_Pand. rewrite H. auto. + - inv H0. inv H2. cbn -[eval_predf]. rewrite eval_predf_Pand. + rewrite H. auto. eauto. + Qed. + + Lemma sem_pred_expr_map_Pand : + forall A ctx f_p ps x v p, + (forall x : positive, sem_pexpr ctx (get_forest_p' x f_p) ps !! x) -> + eval_predf ps p = true -> + sem_pred_expr f_p sem_value ctx x v -> + @sem_pred_expr A _ _ f_p sem_value ctx + (NE.map (fun x0 => (p ∧ fst x0, snd x0)) x) v. + Proof. + induction x; crush. + inv H1. simplify. constructor; eauto. + simplify. replace true with (true && true) by auto. + constructor; auto. + eapply sem_pexpr_eval; eauto. + inv H1. simplify. constructor; eauto. + simplify. replace true with (true && true) by auto. + constructor; auto. + eapply sem_pexpr_eval; eauto. + eapply sem_pred_expr_cons_false. cbn. + replace false with (true && false) by auto. constructor; auto. + eapply sem_pexpr_eval; eauto. eauto. + Qed. + + Lemma sem_pred_expr_app_predicated : + forall A ctx f_p y x v p ps, sem_pred_expr f_p sem_value ctx x v -> (forall x, sem_pexpr ctx (get_forest_p' x f_p) (ps !! x)) -> eval_predf ps p = true -> - prune_predicated (app_predicated p y x) = Some n -> - @sem_pred_expr A _ _ f_p sem_value ctx n v. + @sem_pred_expr A _ _ f_p sem_value ctx (app_predicated p y x) v. Proof. - intros * SEM EVAL PRUNE. Admitted. + intros * SEM PS EVAL. unfold app_predicated. + eapply sem_pred_expr_NEapp2; eauto. + intros. eapply sem_pred_expr_map_not; eauto. + rewrite eval_predf_negate. rewrite EVAL. auto. + eapply sem_pred_expr_map_Pand; eauto. + Qed. + + Lemma sem_pred_expr_prune_predicated : + forall A ctx f_p y x v, + sem_pred_expr f_p sem_value ctx x v -> + prune_predicated x = Some y -> + @sem_pred_expr A _ _ f_p sem_value ctx y v. + Proof. + intros * SEM PRUNE. Admitted. Lemma sem_merge_list : forall A ctx f rs ps m args, @@ -491,7 +678,8 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. @sem_pred_expr A _ _ (forest_preds f) sem_val_list ctx (merge (list_translation args f)) (rs ## args). Proof. - intros. inv H. inv H6. inv H7. Admitted. + induction args; crush. cbn. constructor; constructor. + unfold merge. cbn. Inductive sem_ident {B A: Type} (c: @ctx B) (a: A): A -> Prop := | sem_ident_intro : sem_ident c a a. @@ -723,9 +911,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. } { destruct_match; crush. setoid_rewrite H in Heqb0; eauto. - rewrite H0 in Heqb0. rewrite H1 in Heqb0; crush. - } - } + rewrite H0 in Heqb0. rewrite H1 in Heqb0; crush. } } { destruct_match; crush. { destruct_match; crush. setoid_rewrite H in H0; eauto. @@ -734,10 +920,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. } { destruct_match; crush. setoid_rewrite H in Heqb0; eauto. - rewrite H0 in Heqb0. rewrite H1 in Heqb0; crush. - } - } - } + rewrite H0 in Heqb0. rewrite H1 in Heqb0; crush. } } } Qed. Lemma storev_eval_condition : @@ -789,34 +972,19 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. Proof. intros. destruct p; cbn; inv H; auto. Qed. Lemma sem_update_Iop_top: - forall (f : forest) (sp : val) (p : pred_op) (i : instr_state) (p' : pred_op) (f' : forest) (rs : Regmap.t val) - (m : mem) (pr : predset) (op : Op.operation) (res : Registers.reg) (args : list positive) (p0 : option Gible.pred_op) - (v : val), - Op.eval_operation ge sp op rs ## args m = Some v -> + forall A f p p' f' rs m pr op res args p0 v state, + Op.eval_operation (ctx_ge state) (ctx_sp state) op rs ## args m = Some v -> truthy pr p0 -> - valid_mem (is_mem i) (is_mem state') -> - sem state f (state', None) -> + valid_mem (is_mem (ctx_is state)) m -> + sem state f ((mk_instr_state rs pr m), None) -> update (p, f) (RBop p0 op args res) = Some (p', f') -> - eval_predf (is_ps state') p = true -> - sem state f' ({| is_rs := rs # res <- v; Gible.is_ps := pr; Gible.is_mem := m |}, None). + eval_predf pr p = true -> + @sem A state f' (mk_instr_state (rs # res <- v) pr m, None). Proof. - intros f sp p i p' f' rs m pr op res args p0 v EVAL_OP TRUTHY VALID SEM UPD EVAL_PRED. - - Lemma sem_update_instr : - forall f i' i'' a sp p i p' f', - step_instr ge sp (Iexec i') a (Iexec i'') -> - valid_mem (is_mem i) (is_mem i') -> - sem (mk_ctx i sp ge) f (i', None) -> - update (p, f) a = Some (p', f') -> - eval_predf (is_ps i') p = true -> - sem (mk_ctx i sp ge) f' (i'', None). - Proof. - inversion 1; subst; clear H; intros VALID SEM UPD EVAL_PRED; pose proof SEM as SEM2. - - inv UPD; auto. - - - inversion UPD as [PRUNE]. unfold Option.bind in PRUNE. + intros * EVAL_OP TRUTHY VALID SEM UPD EVAL_PRED. + pose proof SEM as SEM2. + inversion UPD as [PRUNE]. unfold Option.bind in PRUNE. destr. inversion_clear PRUNE. - rename H3 into EVAL_OP. rename H5 into TRUTHY. rename Heqo into PRUNE. inversion_clear SEM as [? ? ? ? ? ? REG PRED MEM EXIT]. cbn [is_ps] in *. constructor. @@ -824,7 +992,8 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. destruct f as [fr fp fe]. cbn [forest_preds set_forest] in *. destruct (peq x res); subst. * rewrite forest_reg_gss in *. rewrite Regmap.gss in *. - eapply sem_pred_expr_updated; [| | |eauto]. + eapply sem_pred_expr_prune_predicated; eauto. + eapply sem_pred_expr_app_predicated; [| |eauto]. replace fp with (forest_preds {| forest_regs := fr; forest_preds := fp; forest_exit := fe |}) by auto. eapply sem_update_Iop; eauto. cbn in *. eapply eval_operation_valid_pointer; eauto. @@ -837,17 +1006,32 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. + constructor; intros. inv PRED. rewrite forest_reg_pred. auto. + rewrite forest_reg_gso; auto; discriminate. + auto. - - inversion UPD as [PRUNE]. unfold Option.bind in PRUNE. destr. + Qed. + + Lemma sem_update_Iload_top: + forall A f p p' f' rs m pr res args p0 v state addr a chunk, + Op.eval_addressing (ctx_ge state) (ctx_sp state) addr rs ## args = Some a -> + Mem.loadv chunk m a = Some v -> + truthy pr p0 -> + valid_mem (is_mem (ctx_is state)) m -> + sem state f ((mk_instr_state rs pr m), None) -> + update (p, f) (RBload p0 chunk addr args res) = Some (p', f') -> + eval_predf pr p = true -> + @sem A state f' (mk_instr_state (rs # res <- v) pr m, None). + Proof. + intros * EVAL_OP LOAD TRUTHY VALID SEM UPD EVAL_PRED. + pose proof SEM as SEM2. + inversion UPD as [PRUNE]. unfold Option.bind in PRUNE. destr. inversion_clear PRUNE. - rename H2 into EVAL_OP. rename H4 into LOAD. rename H6 into TRUTHY. rename Heqo into PRUNE. inversion_clear SEM as [? ? ? ? ? ? REG PRED MEM EXIT]. cbn [is_ps] in *. constructor. + constructor; intro x. inversion_clear REG as [? ? ? REG']. specialize (REG' x). destruct f as [fr fp fe]. cbn [forest_preds set_forest] in *. - destruct (peq x dst); subst. + destruct (peq x res); subst. * rewrite forest_reg_gss in *. rewrite Regmap.gss in *. - eapply sem_pred_expr_updated; [| | |eauto]. + eapply sem_pred_expr_prune_predicated; eauto. + eapply sem_pred_expr_app_predicated; [| |eauto]. replace fp with (forest_preds {| forest_regs := fr; forest_preds := fp; forest_exit := fe |}) by auto. eapply sem_update_Iload; eauto. inversion_clear PRED; eauto. @@ -858,7 +1042,49 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. + constructor; intros. inv PRED. rewrite forest_reg_pred. auto. + rewrite forest_reg_gso; auto; discriminate. + auto. - - + Qed. + + Lemma sem_update_Istore_top: + forall A f p p' f' rs m pr res args p0 state addr a chunk m', + Op.eval_addressing (ctx_ge state) (ctx_sp state) addr rs ## args = Some a -> + Mem.storev chunk m a rs !! res = Some m' -> + truthy pr p0 -> + valid_mem (is_mem (ctx_is state)) m -> + sem state f ((mk_instr_state rs pr m), None) -> + update (p, f) (RBstore p0 chunk addr args res) = Some (p', f') -> + eval_predf pr p = true -> + @sem A state f' (mk_instr_state rs pr m', None). + Proof. + intros * EVAL_OP STORE TRUTHY VALID SEM UPD EVAL_PRED. + pose proof SEM as SEM2. + inversion UPD as [PRUNE]. unfold Option.bind in PRUNE. destr. + inversion_clear PRUNE. + rename Heqo into PRUNE. + inversion_clear SEM as [? ? ? ? ? ? REG PRED MEM EXIT]. + cbn [is_ps] in *. constructor. + + constructor; intros. inv REG. rewrite forest_reg_gso; eauto. discriminate. + + constructor; intros. inv PRED. rewrite forest_reg_pred. auto. + + destruct f as [fr fp fm]; cbn -[seq_app] in *. admit. + + auto. + Admitted. + + Lemma sem_update_instr : + forall f i' i'' a sp p i p' f', + step_instr ge sp (Iexec i') a (Iexec i'') -> + valid_mem (is_mem i) (is_mem i') -> + sem (mk_ctx i sp ge) f (i', None) -> + update (p, f) a = Some (p', f') -> + eval_predf (is_ps i') p = true -> + sem (mk_ctx i sp ge) f' (i'', None). + Proof. + inversion 1; subst; clear H; intros VALID SEM UPD EVAL_PRED; pose proof SEM as SEM2. + - inv UPD; auto. + - eauto using sem_update_Iop_top. + - eauto using sem_update_Iload_top. + - eauto using sem_update_Istore_top. + - admit. + - admit. + Admitted. Lemma Pand_true_left : forall ps a b, -- cgit