From 48d907ee56b39e7a8819700ae8a88af05c1b031e Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 5 Jun 2022 22:42:28 +0100 Subject: Fix many more lemmas --- src/hls/CondElim.v | 4 +- src/hls/CondElimproof.v | 415 +++++++++++++++++++++++++++++++++++------------- src/hls/Gible.v | 10 ++ src/hls/Predicate.v | 9 ++ 4 files changed, 329 insertions(+), 109 deletions(-) diff --git a/src/hls/CondElim.v b/src/hls/CondElim.v index b9bd1e9..9f51053 100644 --- a/src/hls/CondElim.v +++ b/src/hls/CondElim.v @@ -28,6 +28,8 @@ Require Import vericert.hls.GibleSeq. Require Import vericert.hls.Predicate. Require Import vericert.bourdoncle.Bourdoncle. +#[local] Open Scope positive. + Definition elim_cond_s (fresh: predicate) (i: instr) := match i with | RBexit p (RBcond c args n1 n2) => @@ -61,7 +63,7 @@ Definition elim_cond_fold (state: predicate * PTree.t SeqBB.t) (n: node) (b: Seq Definition transf_function (f: function) : function := mkfunction f.(fn_sig) f.(fn_params) f.(fn_stacksize) - (snd (PTree.fold elim_cond_fold f.(fn_code) (1%positive, PTree.empty _))) + (snd (PTree.fold elim_cond_fold f.(fn_code) (max_pred_function f + 1, PTree.empty _))) f.(fn_entrypoint). Definition transf_fundef (fd: fundef) : fundef := diff --git a/src/hls/CondElimproof.v b/src/hls/CondElimproof.v index ecc3538..8b2ce48 100644 --- a/src/hls/CondElimproof.v +++ b/src/hls/CondElimproof.v @@ -42,38 +42,53 @@ Require Import vericert.hls.Predicate. #[local] Open Scope positive. -Lemma cf_in_step : - forall A B ge sp is_ is_' bb cf, - @SeqBB.step A B ge sp (Iexec is_) bb (Iterm is_' cf) -> - exists p, In (RBexit p cf) bb - /\ Option.default true (Option.map (eval_predf (is_ps is_')) p) = true. - Proof. Admitted. - Lemma forbidden_term_trans : forall A B ge sp i c b i' c', ~ @SeqBB.step A B ge sp (Iterm i c) b (Iterm i' c'). Proof. induction b; unfold not; intros; inv H. Qed. -Lemma random1 : - forall A B ge sp is_ b is_' cf, - @SeqBB.step A B ge sp (Iexec is_) b (Iterm is_' cf) -> - exists p b', SeqBB.step ge sp (Iexec is_) (b' ++ (RBexit p cf) :: nil) (Iterm is_' cf) - /\ Forall2 eq (b' ++ (RBexit p cf) :: nil) b. +Lemma step_instr_false : + forall A B ge sp i c a i0, + ~ @step_instr A B ge sp (Iterm i c) a (Iexec i0). +Proof. destruct a; unfold not; intros; inv H. Qed. + +Lemma step_list2_false : + forall A B ge l0 sp i c i0', + ~ step_list2 (@step_instr A B ge) sp (Iterm i c) l0 (Iexec i0'). Proof. -Admitted. + induction l0; unfold not; intros. + inv H. inv H. destruct i1. eapply step_instr_false in H4. auto. + eapply IHl0; eauto. +Qed. + +Lemma append' : + forall A B l0 cf i0 i1 l1 sp ge i0', + step_list2 (@step_instr A B ge) sp (Iexec i0) l0 (Iexec i0') -> + @SeqBB.step A B ge sp (Iexec i0') l1 (Iterm i1 cf) -> + @SeqBB.step A B ge sp (Iexec i0) (l0 ++ l1) (Iterm i1 cf). +Proof. + induction l0; crush. inv H. eauto. inv H. destruct i3. + econstructor; eauto. eapply IHl0; eauto. + eapply step_list2_false in H7. exfalso; auto. +Qed. Lemma append : forall A B cf i0 i1 l0 l1 sp ge, (exists i0', step_list2 (@step_instr A B ge) sp (Iexec i0) l0 (Iexec i0') /\ @SeqBB.step A B ge sp (Iexec i0') l1 (Iterm i1 cf)) -> @SeqBB.step A B ge sp (Iexec i0) (l0 ++ l1) (Iterm i1 cf). -Proof. Admitted. +Proof. intros. simplify. eapply append'; eauto. Qed. Lemma append2 : - forall A B cf i0 i1 l0 l1 sp ge, + forall A B l0 cf i0 i1 l1 sp ge, @SeqBB.step A B ge sp (Iexec i0) l0 (Iterm i1 cf) -> @SeqBB.step A B ge sp (Iexec i0) (l0 ++ l1) (Iterm i1 cf). -Proof. Admitted. +Proof. + induction l0; crush. + inv H. + inv H. econstructor; eauto. eapply IHl0; eauto. + constructor; auto. +Qed. Definition to_cf c := match c with | Iterm _ cf => Some cf | _ => None end. @@ -89,7 +104,7 @@ Variant match_ps : positive -> predset -> predset -> Prop := Lemma eval_pred_under_match: forall rs m rs' m' ps tps tps' ps' v p1 rs'' ps'' m'', eval_pred (Some p1) (mki rs ps m) (mki rs' ps' m') (mki rs'' ps'' m'') -> - max_predicate p1 <= v -> + (forall p, In p (predicate_use p1) -> p <= v) -> match_ps v ps tps -> match_ps v ps' tps' -> exists tps'', @@ -105,10 +120,22 @@ Lemma eval_pred_eq_predset : ps' = ps. Proof. inversion 1; subst; crush. Qed. +Lemma predicate_lt : + forall p p0, + In p0 (predicate_use p) -> p0 <= max_predicate p. +Proof. + induction p; crush. + - destruct_match. inv H; try lia; contradiction. + - eapply Pos.max_le_iff. + eapply in_app_or in H. inv H; eauto. + - eapply Pos.max_le_iff. + eapply in_app_or in H. inv H; eauto. +Qed. + Lemma elim_cond_s_spec : forall A B ge sp rs m rs' m' ps tps ps' p a p0 l v, step_instr ge sp (Iexec (mki rs ps m)) a (Iexec (mki rs' ps' m')) -> - max_pred_instr v a <= v -> + (forall p, In p (pred_uses a) -> p <= v) -> match_ps v ps tps -> elim_cond_s p a = (p0, l) -> exists tps', @@ -136,14 +163,14 @@ Proof. + inv H18. econstructor. split. econstructor. econstructor; eauto. constructor; eauto. constructor. auto. - inv H2. destruct p'. - exploit eval_pred_under_match; eauto. lia. Admitted. + exploit eval_pred_under_match; eauto. Admitted. Definition wf_predicate (v: predicate) (p: predicate) := v < p. Lemma eval_predf_match_ps : forall p p' p0 v, match_ps v p p' -> - max_predicate p0 <= v -> + Forall (fun x => x <= v) (predicate_use p0) -> eval_predf p p0 = eval_predf p' p0. Admitted. @@ -162,7 +189,8 @@ Proof. inversion 1; subst; simplify; econstructor; eauto. Qed. Variant match_stackframe : stackframe -> stackframe -> Prop := | match_stackframe_init : forall res f tf sp pc rs p p' - (TF: transf_function f = tf), + (TF: transf_function f = tf) + (PS: match_ps (max_pred_function f) p p'), match_stackframe (Stackframe res f sp pc rs p) (Stackframe res tf sp pc rs p'). Variant match_states : state -> state -> Prop := @@ -208,7 +236,7 @@ Qed. Lemma eval_predf_in_ps : forall v ps ps' p1 b p tps, eval_predf ps p1 = true -> - max_predicate p1 <= v -> + Forall (fun x => x <= v) (predicate_use p1) -> wf_predicate v p -> match_ps v ps ps' -> eval_predf tps # p <- b (Pand (Plit (b, p)) p1) = true. @@ -217,7 +245,7 @@ Admitted. Lemma eval_predf_in_ps2 : forall v ps ps' p1 b b' p tps, eval_predf ps p1 = true -> - max_predicate p1 <= v -> + Forall (fun x => x <= v) (predicate_use p1) -> wf_predicate v p -> match_ps v ps ps' -> b <> b' -> @@ -235,13 +263,6 @@ Proof. rewrite PMap.gso; auto; lia. Qed. -Lemma transf_block_spec : - forall f pc b, - f.(fn_code) ! pc = Some b -> - exists p, - (transf_function f).(fn_code) ! pc - = Some (snd (replace_section elim_cond_s p b)). Admitted. - Definition match_prog (p: program) (tp: program) := Linking.match_program (fun cu f tf => tf = transf_fundef f) eq p tp. @@ -325,52 +346,6 @@ Section CORRECTNESS. inversion 2; crush. subst. inv H. inv STK. econstructor. Qed. - Lemma elim_cond_s_spec2 : - forall rs m rs' m' ps tps ps' p a p0 l v cf stk f sp pc t st, - step_instr ge sp (Iexec (mki rs ps m)) a (Iterm (mki rs' ps' m') cf) -> - step_cf_instr ge (State stk f sp pc rs' ps' m') cf t st -> - max_pred_instr v a <= v -> - match_ps v ps tps -> - wf_predicate v p -> - elim_cond_s p a = (p0, l) -> - exists tps' cf' st', - SeqBB.step tge sp (Iexec (mki rs tps m)) l (Iterm (mki rs' tps' m') cf') - /\ match_ps v ps' tps' - /\ step_cf_instr tge (State stk f sp pc rs' tps' m') cf' t st' - /\ match_states st st'. - Proof. - inversion 1; subst; simplify. - - destruct (eval_predf ps p1) eqn:?; [|discriminate]. inv H2. - destruct cf; inv H5; - try (do 3 econstructor; simplify; - [ constructor; apply step_instr_inv_exit; erewrite <- eval_predf_match_ps; eauto; lia - | auto - | eauto using step_cf_instr_ps_idem - | assert (ps' = ps'') by (eauto using step_cf_instr_ps_const); subst; auto ]). - do 3 econstructor; simplify. - constructor; apply step_instr_inv_exit; erewrite <- eval_predf_match_ps; eauto; lia. - auto. - (*inv H0; destruct b. - + do 3 econstructor; simplify. - econstructor. econstructor; eauto. eapply eval_pred_true. - erewrite <- eval_predf_match_ps; eauto. simpl. lia. - constructor. apply step_instr_inv_exit. simpl. - eapply eval_predf_in_ps; eauto. lia. - apply match_ps_set_gt; auto. - constructor; auto. - apply match_ps_set_gt; auto. - + do 3 econstructor; simplify. - econstructor. econstructor; eauto. eapply eval_pred_true. - erewrite <- eval_predf_match_ps; eauto. simpl. lia. - econstructor. apply step_instr_inv_exit2. simpl. - eapply eval_predf_in_ps2; eauto. lia. - constructor. apply step_instr_inv_exit. simpl. - eapply eval_predf_in_ps; eauto; lia. - apply match_ps_set_gt; auto. - constructor; auto. - apply match_ps_set_gt; auto. - -*) Admitted. - Lemma eval_op_eq: forall (sp0 : Values.val) (op : Op.operation) (vl : list Values.val) m, Op.eval_operation ge sp0 op vl m = Op.eval_operation tge sp0 op vl m. @@ -401,21 +376,35 @@ Section CORRECTNESS. try (rewrite <- eval_op_eq; auto); rewrite <- eval_addressing_eq; auto. Qed. + #[local] Hint Resolve eval_builtin_args_preserved : core. + #[local] Hint Resolve symbols_preserved : core. + #[local] Hint Resolve external_call_symbols_preserved : core. + #[local] Hint Resolve senv_preserved : core. + #[local] Hint Resolve find_function_translated : core. + #[local] Hint Resolve sig_transf_function : core. + Lemma step_cf_instr_ge : forall st cf t st' tst, step_cf_instr ge st cf t st' -> match_states st tst -> exists tst', step_cf_instr tge tst cf t tst' /\ match_states st' tst'. - Proof. + Proof using TRANSL. + inversion 1; subst; simplify; clear H; + match goal with H: context[match_states] |- _ => inv H end; + repeat (econstructor; eauto). + Qed. + + Lemma step_cf_instr_det : + forall ge st cf t st1 st2, + step_cf_instr ge st cf t st1 -> + step_cf_instr ge st cf t st2 -> + st1 = st2. + Proof using TRANSL. inversion 1; subst; simplify; clear H; - match goal with H: context[match_states] |- _ => inv H end. - - do 2 econstructor. rewrite <- sig_transf_function. econstructor; eauto. - eauto using find_function_translated. auto. - econstructor; auto. repeat (constructor; auto). - - do 2 econstructor. econstructor. eauto using find_function_translated. - eauto using sig_transf_function. eauto. - econstructor; auto. - - do 2 econstructor. + match goal with H: context[step_cf_instr] |- _ => inv H end; crush; + assert (vargs0 = vargs) by eauto using eval_builtin_args_determ; subst; + assert (vres = vres0 /\ m' = m'0) by eauto using external_call_deterministic; crush. + Qed. Lemma step_list2_ge : forall sp l i i', @@ -438,33 +427,233 @@ Section CORRECTNESS. - eauto using exec_RBterm, step_instr_ge. Qed. + Lemma max_pred_function_use : + forall f pc bb i p, + f.(fn_code) ! pc = Some bb -> + In i bb -> + In p (pred_uses i) -> + p <= max_pred_function f. + Proof. Admitted. + + Lemma elim_cond_s_wf_predicate : + forall a p p0 l v, + elim_cond_s p a = (p0, l) -> + wf_predicate v p -> + wf_predicate v p0. + Proof using. + destruct a; simplify; try match goal with H: (_, _) = (_, _) |- _ => inv H end; auto. + destruct c; simplify; try match goal with H: (_, _) = (_, _) |- _ => inv H end; auto. + unfold wf_predicate in *; lia. + Qed. + + Lemma replace_section_wf_predicate : + forall bb v p t0 p0, + replace_section elim_cond_s p bb = (p0, t0) -> + wf_predicate v p -> + wf_predicate v p0. + Proof using. + induction bb; crush; repeat (destruct_match; crush). + inv H. + exploit IHbb; eauto; simplify. + eapply elim_cond_s_wf_predicate in Heqp2; eauto. + Qed. + + Lemma elim_cond_s_spec2 : + forall rs m rs' m' ps tps ps' p a p0 l cf stk f sp pc t st tstk, + step_instr ge sp (Iexec (mki rs ps m)) a (Iterm (mki rs' ps' m') cf) -> + step_cf_instr ge (State stk f sp pc rs' ps' m') cf t st -> + Forall (fun p => p <= (max_pred_function f)) (pred_uses a) -> + match_ps (max_pred_function f) ps tps -> + wf_predicate (max_pred_function f) p -> + elim_cond_s p a = (p0, l) -> + Forall2 match_stackframe stk tstk -> + exists tps' cf' st', + SeqBB.step tge sp (Iexec (mki rs tps m)) l (Iterm (mki rs' tps' m') cf') + /\ match_ps (max_pred_function f) ps' tps' + /\ step_cf_instr tge (State tstk (transf_function f) sp pc rs' tps' m') cf' t st' + /\ match_states st st'. + Proof using TRANSL. + inversion 1; subst; simplify. + - destruct (eval_predf ps p1) eqn:?; [|discriminate]. inv H2. + destruct cf; inv H5; + try (exploit step_cf_instr_ge; eauto; econstructor; eauto; simplify; + do 3 econstructor; simplify; + [ constructor; apply step_instr_inv_exit; erewrite <- eval_predf_match_ps | | | ]); + eauto using step_cf_instr_ps_idem. + inv H0; destruct b. + + do 3 econstructor; simplify. + econstructor. econstructor; eauto. eapply eval_pred_true. + erewrite <- eval_predf_match_ps; eauto. simpl. + constructor. apply step_instr_inv_exit. simpl. + eapply eval_predf_in_ps; eauto. + apply match_ps_set_gt; auto. + constructor; auto. + constructor; auto. + apply match_ps_set_gt; auto. + + do 3 econstructor; simplify. + econstructor. econstructor; eauto. eapply eval_pred_true. + erewrite <- eval_predf_match_ps; eauto. + econstructor. apply step_instr_inv_exit2. simpl. + eapply eval_predf_in_ps2; eauto. + constructor. apply step_instr_inv_exit. simpl. + eapply eval_predf_in_ps; eauto. + apply match_ps_set_gt; auto. + constructor; auto. + constructor; auto. + apply match_ps_set_gt; auto. + - destruct cf; inv H4; exploit step_cf_instr_ge; eauto; try solve [econstructor; eauto]; simplify; + try (do 3 econstructor; simplify; eauto; eapply exec_RBterm; econstructor; eauto). + inv H0. destruct b. + + do 3 econstructor; simplify. + econstructor. econstructor; eauto. constructor. + constructor. apply step_instr_inv_exit. simplify. + unfold eval_predf. simplify. rewrite Pos2Nat.id. apply PMap.gss. + apply match_ps_set_gt; auto. + constructor; auto. + constructor; auto. + apply match_ps_set_gt; auto. + + do 3 econstructor; simplify. + econstructor. econstructor; eauto. constructor. + econstructor. apply step_instr_inv_exit2. simpl. + unfold eval_predf. simplify. rewrite Pos2Nat.id. apply PMap.gss. + constructor. apply step_instr_inv_exit. simpl. + unfold eval_predf. simplify. rewrite Pos2Nat.id. rewrite PMap.gss. auto. + apply match_ps_set_gt; auto. + constructor; auto. + constructor; auto. + apply match_ps_set_gt; auto. + Qed. + Lemma replace_section_spec : - forall sp bb rs ps m rs' ps' m' stk f t cf pc tps v n p p' bb' st st', + forall sp bb rs ps m rs' ps' m' stk f t cf pc tps p p' bb' st tstk, SeqBB.step ge sp (Iexec (mki rs ps m)) bb (Iterm (mki rs' ps' m') cf) -> step_cf_instr ge (State stk f sp pc rs' ps' m') cf t st -> - match_ps v ps tps -> - max_pred_block v n bb <= v -> + match_ps (max_pred_function f) ps tps -> + (forall p i, In i bb -> In p (pred_uses i) -> p <= max_pred_function f) -> + wf_predicate (max_pred_function f) p -> replace_section elim_cond_s p bb = (p', bb') -> - exists tps' cf', + Forall2 match_stackframe stk tstk -> + exists st' tps' cf', SeqBB.step tge sp (Iexec (mki rs tps m)) bb' (Iterm (mki rs' tps' m') cf') - /\ match_ps v ps' tps' - /\ step_cf_instr tge (State stk f sp pc rs' tps' m') cf' t st' + /\ match_ps (max_pred_function f) ps' tps' + /\ step_cf_instr tge (State tstk (transf_function f) sp pc rs' tps' m') cf' t st' /\ match_states st st'. - Proof. + Proof using TRANSL. induction bb; simplify; inv H. - - destruct state'. repeat destruct_match. inv H3. - exploit elim_cond_s_spec; eauto. admit. simplify. - exploit IHbb; eauto; simplify. admit. - do 2 econstructor. simplify. + - destruct state'. repeat destruct_match. inv H4. + exploit elim_cond_s_spec; eauto. simplify. + exploit IHbb; eauto; simplify. + do 3 econstructor. simplify. eapply append. econstructor; simplify. eapply step_list2_ge; eauto. eauto. eauto. eauto. eauto. - - repeat destruct_match; simplify. inv H3. - exploit elim_cond_s_spec2; eauto. admit. admit. simplify. - do 3 econstructor; simplify; eauto. - eapply append2; eauto using step_list2_ge. - Unshelve. exact 1. - Admitted. + - repeat destruct_match; simplify. inv H4. + exploit elim_cond_s_spec2. 6: { eauto. } eauto. eauto. + apply Forall_forall. eauto. eauto. + eapply replace_section_wf_predicate; eauto. eauto. + simplify. + exploit step_cf_instr_ge; eauto. constructor; eauto. simplify. + exists x1. eexists. exists x0. simplify. + eapply append2. eauto using step_list_ge. auto. auto. auto. + Qed. + + Definition lt_pred (c: code) (m: positive) := + forall pc bb n, + c ! pc = Some bb -> + m = max_pred_block m n bb \/ m < max_pred_block 1 n bb. + + Definition lt_pred2 (c: code) (m: positive) := + forall pc bb n, + c ! pc = Some bb -> + max_pred_block 1 n bb <= m. + + (* Lemma max_pred_block_lt: *) + (* forall v v0 n b k, *) + (* v0 <= b -> *) + (* max_pred_block v0 n v <= max_pred_block b k v. *) + (* Proof. Admitted. *) + + (* Lemma max_block_pred : *) + (* forall f, lt_pred f.(fn_code) (max_pred_function f). *) + (* Proof. *) + (* unfold max_pred_function; intros. *) + (* eapply PTree_Properties.fold_ind; unfold lt_pred; intros. *) + (* destruct (max_pred_block 1 n bb); crush. *) + (* destruct (peq pc k); subst; simplify. *) + (* - assert (v0 <= a \/ a < v0) by admit. *) + (* inv H3. left. eapply max_pred_block_lt; eauto. *) + (* right. *) + (* Abort. *) + + Lemma elim_cond_s_lt : + forall p a p0 l x, + elim_cond_s p a = (p0, l) -> + p0 <= x -> + p <= x. + Proof using. + destruct a; crush; destruct c; crush. + inv H. lia. + Qed. + + Lemma replace_section_lt : + forall t p1 p0 t2 x, + replace_section elim_cond_s p1 t = (p0, t2) -> + p0 <= x -> + p1 <= x. + Proof using. + induction t; crush; repeat destruct_match. inv H. + eapply IHt; eauto. + eapply elim_cond_s_lt; eauto. + Qed. + + Lemma pred_not_in : + forall l pc p t p' t' x, + ~ In pc (map fst l) -> + fold_left (fun a p => elim_cond_fold a (fst p) (snd p)) l (p, t) = (p', t') -> + t ! pc = x -> t' ! pc = x. + Proof using. + induction l; crush. + repeat destruct_match. + eapply IHl; eauto. rewrite PTree.gso; auto. + Qed. + + Lemma pred_greater : + forall l pc x v p' t', + In (pc, x) l -> + list_norepet (map fst l) -> + fold_left (fun a p => elim_cond_fold a (fst p) (snd p)) l v = (p', t') -> + exists p, t' ! pc = Some (snd (replace_section elim_cond_s p x)) + /\ (fst v) <= p. + Proof. + induction l; crush. + inv H0. destruct a; simplify. inv H. inv H0. + remember (elim_cond_fold v pc x). destruct p. + eapply pred_not_in in H1; eauto. symmetry in Heqp. + unfold elim_cond_fold in Heqp. repeat destruct_match. inv Heqp0. inv Heqp. + simplify. econstructor. split. rewrite PTree.gss in H1. + rewrite Heqp1. eauto. lia. + remember (elim_cond_fold v p t). destruct p0. symmetry in Heqp0. + unfold elim_cond_fold in Heqp0. repeat destruct_match. inv Heqp0. + exploit IHl; eauto; simplify. + econstructor; simplify. eauto. + eapply replace_section_lt; eauto. + Qed. + + Lemma transf_block_spec : + forall f pc x, + f.(fn_code) ! pc = Some x -> + forall p' t', + PTree.fold elim_cond_fold f.(fn_code) (max_pred_function f + 1, PTree.empty _) = (p', t') -> + exists p, + t' ! pc = Some (snd (replace_section elim_cond_s p x)) /\ max_pred_function f + 1 <= p. + Proof using. + intros. + replace (max_pred_function f + 1) with (fst (max_pred_function f + 1, PTree.empty SeqBB.t)); auto. + eapply pred_greater. + eapply PTree.elements_correct; eauto. + apply PTree.elements_keys_norepet. + rewrite <- PTree.fold_spec. eauto. + Qed. Lemma transf_step_correct: forall (s1 : state) (t : trace) (s1' : state), @@ -472,12 +661,23 @@ Section CORRECTNESS. forall s2 : state, match_states s1 s2 -> exists s2' : state, step tge s2 t s2' /\ match_states s1' s2'. - Proof. + Proof using TRANSL. induction 1; intros. - + inv H2. eapply cf_in_step in H0; simplify. - exploit transf_block_spec; eauto; simplify. - do 2 econstructor. econstructor; eauto. - simplify. Admitted. + + inv H2. + exploit transf_block_spec; eauto. + assert (X: forall A B (a: A * B), a = (fst a, snd a)). + { destruct a; auto. } eapply X. simplify. + remember (replace_section elim_cond_s x bb). destruct p. symmetry in Heqp. + exploit replace_section_spec; eauto. + solve [eauto using max_pred_function_use]. + unfold wf_predicate. lia. + simplify. econstructor. + simplify. econstructor; eauto. auto. + + inv H0. econstructor. + simplify. econstructor; eauto. constructor; eauto. constructor. auto. + + inv H0. do 3 econstructor; eauto. + + inv H. inv STK. inv H1. do 3 econstructor; eauto. + Qed. Theorem transf_program_correct: forward_simulation (semantics prog) (semantics tprog). @@ -489,5 +689,4 @@ Section CORRECTNESS. + apply transf_step_correct. Qed. - End CORRECTNESS. diff --git a/src/hls/Gible.v b/src/hls/Gible.v index e50fdc0..c51b250 100644 --- a/src/hls/Gible.v +++ b/src/hls/Gible.v @@ -613,4 +613,14 @@ type ~genv~ which was declared earlier. end ) b nil. + Definition pred_uses i := + match i with + | RBop (Some p) _ _ _ + | RBload (Some p) _ _ _ _ + | RBstore (Some p) _ _ _ _ + | RBexit (Some p) _ => predicate_use p + | RBsetpred (Some p) _ _ p' => p' :: predicate_use p + | _ => nil + end. + End Gible. diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v index 087b119..7a4ed60 100644 --- a/src/hls/Predicate.v +++ b/src/hls/Predicate.v @@ -508,6 +508,15 @@ Fixpoint max_predicate (p: pred_op) : positive := | Por a b => Pos.max (max_predicate a) (max_predicate b) end. +Fixpoint predicate_use (p: pred_op) : list positive := + match p with + | Plit (b, p) => p :: nil + | Ptrue => nil + | Pfalse => nil + | Pand a b => predicate_use a ++ predicate_use b + | Por a b => predicate_use a ++ predicate_use b + end. + Definition tseytin (p: pred_op) : {fm: formula | forall a, sat_predicate p a = true <-> satFormula fm a}. -- cgit