From e95d311a70fa4c2806f83ca112b11514a1ad159a Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 28 May 2023 19:21:41 +0100 Subject: Finish max predicate proof --- src/hls/GibleSeq.v | 79 +++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 78 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/hls/GibleSeq.v b/src/hls/GibleSeq.v index c9d7ab2..61a77e7 100644 --- a/src/hls/GibleSeq.v +++ b/src/hls/GibleSeq.v @@ -149,13 +149,90 @@ Qed. #[local] Open Scope positive. +Lemma max_pred_instr_lt : + forall y a, + y <= max_pred_instr y a. +Proof. + unfold max_pred_instr; intros. + destruct a; try destruct o; lia. +Qed. + +Lemma max_pred_instr_fold_lt : + forall b y, + y <= fold_left max_pred_instr b y. +Proof. + induction b; crush. + transitivity (max_pred_instr y a); auto. + apply max_pred_instr_lt. +Qed. + +Lemma max_pred_block_lt : + forall y a b, + y <= max_pred_block y a b. +Proof. + unfold max_pred_block, SeqBB.foldl; intros. + apply max_pred_instr_fold_lt. +Qed. + +Lemma max_fold_left_initial : + forall l y, + y <= fold_left (fun (a : positive) (p0 : positive * SeqBB.t) => max_pred_block a (fst p0) (snd p0)) l y. +Proof. + induction l; crush. + transitivity (max_pred_block y (fst a) (snd a)); eauto. + apply max_pred_block_lt. +Qed. + +Lemma max_pred_in_max : + forall y p i, + In p (pred_uses i) -> + p <= max_pred_instr y i. +Proof. + intros. unfold max_pred_instr. destruct i; try destruct o; cbn in *; try easy. + - eapply predicate_lt in H; lia. + - eapply predicate_lt in H; lia. + - eapply predicate_lt in H; lia. + - inv H; try lia. eapply predicate_lt in H0; lia. + - eapply predicate_lt in H; lia. +Qed. + +Lemma fold_left_in_max : + forall bb p y i, + In i bb -> + In p (pred_uses i) -> + p <= fold_left max_pred_instr bb y. +Proof. + induction bb; crush. inv H; eauto. + transitivity (max_pred_instr y i); [|eapply max_pred_instr_fold_lt]. + apply max_pred_in_max; auto. +Qed. + +Lemma max_pred_function_use' : + forall l pc bb p i y, + In (pc, bb) l -> + In i bb -> + In p (pred_uses i) -> + p <= fold_left (fun (a : positive) (p0 : positive * SeqBB.t) => max_pred_block a (fst p0) (snd p0)) l y. +Proof. + induction l; crush. inv H; eauto. + transitivity (max_pred_block y (fst (pc, bb)) (snd (pc, bb))); eauto; + [|eapply max_fold_left_initial]. + cbn. unfold SeqBB.foldl. + eapply fold_left_in_max; eauto. +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. +Proof. + unfold max_pred_function; intros. + rewrite PTree.fold_spec. + eapply max_pred_function_use'; eauto. + eapply PTree.elements_correct; eauto. +Qed. Ltac truthy_falsy := match goal with -- cgit