diff options
author | Yann Herklotz <git@yannherklotz.com> | 2022-10-11 16:39:13 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2022-10-11 16:39:13 +0100 |
commit | f8bd8cde25321a3a4a3195bf9189416194b3732e (patch) | |
tree | 7773d41eebb8ad6e26d545cc81ad51d24d2bd6a4 /src | |
parent | c35404c110b7616b30eeb48fc4051dcb33d84f40 (diff) | |
download | vericert-f8bd8cde25321a3a4a3195bf9189416194b3732e.tar.gz vericert-f8bd8cde25321a3a4a3195bf9189416194b3732e.zip |
Clean up proofs
Diffstat (limited to 'src')
-rw-r--r-- | src/common/Vericertlib.v | 31 | ||||
-rw-r--r-- | src/hls/Abstr.v | 10 | ||||
-rw-r--r-- | src/hls/Array.v | 6 | ||||
-rw-r--r-- | src/hls/GiblePargen.v | 76 | ||||
-rw-r--r-- | src/hls/GiblePargenproof.v | 42 | ||||
-rw-r--r-- | src/hls/GibleSeq.v | 2 | ||||
-rw-r--r-- | src/hls/HTLgenproof.v | 82 | ||||
-rw-r--r-- | src/hls/IfConversionproof.v | 14 | ||||
-rw-r--r-- | src/hls/Verilog.v | 56 |
9 files changed, 170 insertions, 149 deletions
diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v index 6f602fc..da046f3 100644 --- a/src/common/Vericertlib.v +++ b/src/common/Vericertlib.v @@ -74,8 +74,6 @@ Ltac solve_by_inverts n := Ltac solve_by_invert := solve_by_inverts 1. -Ltac invert x := inversion x; subst; clear x. - Ltac destruct_match := match goal with | [ |- context[match ?x with | _ => _ end ] ] => destruct x eqn:? @@ -86,10 +84,10 @@ Ltac auto_destruct x := destruct x eqn:?; simpl in *; try discriminate; try cong Ltac nicify_hypotheses := repeat match goal with - | [ H : ex _ |- _ ] => invert H - | [ H : Some _ = Some _ |- _ ] => invert H + | [ H : ex _ |- _ ] => inv H + | [ H : Some _ = Some _ |- _ ] => inv H | [ H : ?x = ?x |- _ ] => clear H - | [ H : _ /\ _ |- _ ] => invert H + | [ H : _ /\ _ |- _ ] => inv H end. Ltac nicify_goals := @@ -169,7 +167,7 @@ Ltac substpp := repeat match goal with | [ H1 : ?x = Some _, H2 : ?x = Some _ |- _ ] => let EQ := fresh "EQ" in - learn H1 as EQ; rewrite H2 in EQ; invert EQ + learn H1 as EQ; rewrite H2 in EQ; inv EQ | _ => idtac end. @@ -251,3 +249,24 @@ Lemma forall_ptree_true: Proof. apply ptree_forall. Qed. + +Ltac decomp_logicals h := + idtac;match type of h with + | @ex _ (fun x => _) => let x' := fresh x in let h1 := fresh in destruct h as [x' h1]; decomp_logicals h1 + | @sig _ (fun x => _) => let x' := fresh x in let h1 := fresh in destruct h as [x' h1]; decomp_logicals h1 + | @sig2 _ (fun x => _) (fun _ => _) => let x' := fresh x in + let h1 := fresh in + let h2 := fresh in + destruct h as [x' h1 h2]; + decomp_logicals h1; + decomp_logicals h2 + | @sigT _ (fun x => _) => let x' := fresh x in let h1 := fresh in destruct h as [x' h1]; decomp_logicals h1 + | @sigT2 _ (fun x => _) (fun _ => _) => let x' := fresh x in + let h1 := fresh in + let h2 := fresh in + destruct h as [x' h1 h2]; decomp_logicals h1; decomp_logicals h2 + | and _ _ => let h1 := fresh in let h2 := fresh in destruct h as [h1 h2]; decomp_logicals h1; decomp_logicals h2 + | iff _ _ => let h1 := fresh in let h2 := fresh in destruct h as [h1 h2]; decomp_logicals h1; decomp_logicals h2 + | or _ _ => let h' := fresh in destruct h as [h' | h']; [decomp_logicals h' | decomp_logicals h' ] + | _ => idtac + end. diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index 07a9649..5ce7c0a 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -1463,6 +1463,11 @@ Proof. rewrite RTree.gso; auto. Qed. +Lemma forest_reg_pred: + forall (f : forest) w dst dst', + (f #r dst <- w) #p dst' = f #p dst'. +Proof. auto. Qed. + Lemma forest_reg_gss: forall (f : forest) w dst, (f #r dst <- w) #r dst = w. @@ -1482,6 +1487,11 @@ Proof. rewrite PTree.gso; auto. Qed. +Lemma forest_pred_reg: + forall (f : forest) w dst dst', + (f #p dst <- w) #r dst' = f #r dst'. +Proof. auto. Qed. + Lemma forest_pred_gss: forall (f : forest) w dst, (f #p dst <- w) #p dst = w. diff --git a/src/hls/Array.v b/src/hls/Array.v index de74611..8b7d262 100644 --- a/src/hls/Array.v +++ b/src/hls/Array.v @@ -76,7 +76,7 @@ Lemma array_set_wf {A : Type} : Proof. induction l; intros; destruct i; auto. - invert H; crush. + inv H; crush. Qed. Definition array_set {A : Type} (i : nat) (x : A) (a : Array A) := @@ -272,10 +272,10 @@ Proof. (* This is actually a degenerate case, not an unprovable goal. *) pose proof (in_app_or (list_repeat' [] a n) ([a])). - apply H0 in H. invert H. + apply H0 in H. inv H. - eapply IHn in X; eassumption. - - invert H1; contradiction. + - inv H1; contradiction. Qed. Lemma list_repeat_head_tail {A : Type} : forall n (a : A), diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v index c2ed9e3..7c9a898 100644 --- a/src/hls/GiblePargen.v +++ b/src/hls/GiblePargen.v @@ -71,24 +71,6 @@ Fixpoint replicate {A} (n: nat) (l: A) := | S n => l :: replicate n l end. -Definition merge''' {A: Type} (x y: option (@Predicate.pred_op A)) := - match x, y with - | Some p1, Some p2 => Some (Pand p1 p2) - | Some p, None | None, Some p => Some p - | None, None => None - end. - -Definition merge'' {A: Type} x := - match x with - | ((a, e), (b, el)) => (@merge''' A a b, Econs e el) - end. - -Definition map_pred_op {A B P: Type} (pf: option (@Predicate.pred_op P) * (A -> B)) - (pa: option (@Predicate.pred_op P) * A): option (@Predicate.pred_op P) * B := - match pa, pf with - | (p, a), (p', f) => (merge''' p p', f a) - end. - Definition predicated_prod {A B: Type} (p1: predicated A) (p2: predicated B) := NE.map (fun x => match x with ((a, b), (c, d)) => (Pand a c, (b, d)) end) (NE.non_empty_prod p1 p2). @@ -96,33 +78,35 @@ Definition predicated_prod {A B: Type} (p1: predicated A) (p2: predicated B) := Definition predicated_map {A B: Type} (f: A -> B) (p: predicated A) : predicated B := NE.map (fun x => (fst x, f (snd x))) p. -(*map (fun x => (fst x, Econs (snd x) Enil)) pel*) -Definition merge' (pel: pred_expr) (tpel: predicated expression_list) := +Definition cons_pred_expr (pel: pred_expr) (tpel: predicated expression_list) := predicated_map (uncurry Econs) (predicated_prod pel tpel). -Fixpoint merge (pel: list pred_expr): predicated expression_list := +Fixpoint merge_old (pel: list pred_expr): predicated expression_list := match pel with | nil => NE.singleton (T, Enil) - | a :: b => merge' a (merge b) + | a :: b => cons_pred_expr a (merge_old b) + end. + +Definition merge (pel: list pred_expr): predicated expression_list := + match NE.of_list pel with + | Some npel => + NE.fold_right cons_pred_expr (NE.singleton (T, Enil)) npel + | None => NE.singleton (T, Enil) end. -Definition map_predicated {A B} (pf: predicated (A -> B)) (pa: predicated A) +Definition seq_app {A B} (pf: predicated (A -> B)) (pa: predicated A) : predicated B := predicated_map (fun x => (fst x) (snd x)) (predicated_prod pf pa). -Definition predicated_apply1 {A B} (pf: predicated (A -> B)) (pa: A) +Definition flap {A B} (pf: predicated (A -> B)) (pa: A) : predicated B := NE.map (fun x => (fst x, (snd x) pa)) pf. -Definition predicated_apply2 {A B C} (pf: predicated (A -> B -> C)) (pa: A) +Definition flap2 {A B C} (pf: predicated (A -> B -> C)) (pa: A) (pb: B): predicated C := NE.map (fun x => (fst x, (snd x) pa pb)) pf. -Definition predicated_apply3 {A B C D} (pf: predicated (A -> B -> C -> D)) - (pa: A) (pb: B) (pc: C): predicated D := - NE.map (fun x => (fst x, (snd x) pa pb pc)) pf. - -Definition predicated_from_opt {A: Type} (p: option pred_op) (a: A) := +Definition predicated_of_opt {A: Type} (p: option pred_op) (a: A) := match p with | Some p' => NE.singleton (p', a) | None => NE.singleton (T, a) @@ -131,24 +115,12 @@ Definition predicated_from_opt {A: Type} (p: option pred_op) (a: A) := #[local] Open Scope non_empty_scope. #[local] Open Scope pred_op. -Fixpoint NEfold_left {A B} (f: A -> B -> A) (l: NE.non_empty B) (a: A) : A := - match l with - | NE.singleton a' => f a a' - | a' ::| b => NEfold_left f b (f a a') - end. - -Fixpoint NEapp {A} (l m: NE.non_empty A) := - match l with - | NE.singleton a => a ::| m - | a ::| b => a ::| NEapp b m - end. - Definition app_predicated' {A: Type} (a b: predicated A) := - let negation := ¬ (NEfold_left (fun a b => a ∨ (fst b)) b ⟂) in - NEapp (NE.map (fun x => (negation ∧ fst x, snd x)) a) b. + let negation := ¬ (NE.fold_left (fun a b => a ∨ (fst b)) b ⟂) in + NE.app (NE.map (fun x => (negation ∧ fst x, snd x)) a) b. Definition app_predicated {A: Type} (p': pred_op) (a b: predicated A) := - NEapp (NE.map (fun x => (¬ p' ∧ fst x, snd x)) a) + NE.app (NE.map (fun x => (¬ p' ∧ fst x, snd x)) a) (NE.map (fun x => (p' ∧ fst x, snd x)) b). Definition prune_predicated {A: Type} (a: predicated A) := @@ -215,15 +187,15 @@ Definition update (fop : pred_op * forest) (i : instr): option (pred_op * forest prune_predicated (app_predicated (dfltp p ∧ pred) (f #r (Reg r)) - (map_predicated (pred_ret (Eop op)) (merge (list_translation rl f)))); + (seq_app (pred_ret (Eop op)) (merge (list_translation rl f)))); Some (pred, f #r (Reg r) <- pruned) | RBload p chunk addr rl r => do pruned <- prune_predicated (app_predicated (dfltp p ∧ pred) (f #r (Reg r)) - (map_predicated - (map_predicated (pred_ret (Eload chunk addr)) + (seq_app + (seq_app (pred_ret (Eload chunk addr)) (merge (list_translation rl f))) (f #r Mem))); Some (pred, f #r (Reg r) <- pruned) @@ -232,16 +204,16 @@ Definition update (fop : pred_op * forest) (i : instr): option (pred_op * forest prune_predicated (app_predicated (dfltp p ∧ pred) (f #r Mem) - (map_predicated - (map_predicated - (predicated_apply2 (map_predicated (pred_ret Estore) + (seq_app + (seq_app + (flap2 (seq_app (pred_ret Estore) (f #r (Reg r))) chunk addr) (merge (list_translation rl f))) (f #r Mem))); Some (pred, f #r Mem <- pruned) | RBsetpred p' c args p => let new_pred := (from_pred_op f.(forest_preds) (dfltp p' ∧ pred) - → from_predicated true f.(forest_preds) (map_predicated (pred_ret (PEsetpred c)) + → from_predicated true f.(forest_preds) (seq_app (pred_ret (PEsetpred c)) (merge (list_translation args f)))) in do _ <- is_initial_pred f p; diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v index 05467ed..3f8aeae 100644 --- a/src/hls/GiblePargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -44,6 +44,8 @@ Import OptionExtra. #[local] Opaque simplify. #[local] Opaque deep_simplify. +Ltac destr := destruct_match; try discriminate; []. + (*| ============== RTLPargenproof @@ -475,11 +477,25 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. Lemma sem_update_instr : forall f i' i'' a sp p i p' f', - sem (mk_ctx i sp ge) f (i', None) -> step_instr ge sp (Iexec i') a (Iexec 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. Admitted. + Proof. + inversion 1; subst; clear H; intros SEM UPD EVAL_PRED. + - inv UPD; auto. + - 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. + + admit. + + constructor; intros. inv PRED. rewrite forest_reg_pred. auto. + + rewrite forest_reg_gso; auto; discriminate. + + auto. + - Lemma truthy_dflt : forall ps p, @@ -495,6 +511,16 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. rewrite eval_predf_Pand. now rewrite H. Qed. + Lemma Pand_true_right : + forall ps a b, + eval_predf ps b = false -> + eval_predf ps (a ∧ b) = false. + Proof. + intros. + rewrite eval_predf_Pand. rewrite H. + eauto with bool. + Qed. + Lemma eval_predf_simplify : forall ps x, eval_predf ps (simplify x) = eval_predf ps x. @@ -516,8 +542,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. { rewrite eval_predf_negate. now rewrite negb_false_iff. } apply Pand_true_left with (b := p') in H0. rewrite <- eval_predf_simplify in H0. split; auto. - unfold "<-e". - destruct i''. + unfold "<-e". destruct i''. inv H. constructor; auto. admit. admit. simplify. Admitted. @@ -567,8 +592,6 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. sem (mk_ctx i sp ge) f' (i', cf). Proof. Admitted. - Ltac destr := destruct_match; try discriminate; []. - Lemma eval_predf_update_true : forall i i' curr_p next_p f f_next instr sp, update (curr_p, f) instr = Some (next_p, f_next) -> @@ -732,8 +755,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. exists R2, Smallstep.plus GiblePar.step tge R1 t R2 /\ match_states S2 R2. Proof. induction 1; repeat semantics_simpl. - { - exploit schedule_oracle_correct; eauto. constructor; eauto. simplify. + { exploit schedule_oracle_correct; eauto. constructor; eauto. simplify. destruct x0. pose proof H2 as X. eapply match_states_stepBB in X; eauto. exploit step_cf_correct; eauto. simplify. @@ -771,9 +793,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. Lemma transl_final_states: forall S R r, match_states S R -> GibleSeq.final_state S r -> GiblePar.final_state R r. - Proof. - intros. inv H0. inv H. inv STACKS. constructor. - Qed. + Proof. intros. inv H0. inv H. inv STACKS. constructor. Qed. Theorem transf_program_correct: Smallstep.forward_simulation (GibleSeq.semantics prog) (GiblePar.semantics tprog). diff --git a/src/hls/GibleSeq.v b/src/hls/GibleSeq.v index 793eb5d..4bb001b 100644 --- a/src/hls/GibleSeq.v +++ b/src/hls/GibleSeq.v @@ -143,7 +143,7 @@ Proof. exists x. exists (a :: x0). exists x1. simplify; auto. econstructor; eauto. - inv H3. - exists p. exists nil. exists bb. crush. + exists p. exists (@nil instr). exists bb. crush. constructor. Qed. diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index bf1ef1c..1089356 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -248,9 +248,9 @@ Proof. discriminate. destruct l2 eqn:EQl2. crush. - simpl in H. invert H. + simpl in H. inv H. destruct n; simpl in *. - invert H0. simpl. reflexivity. + inv H0. simpl. reflexivity. eauto. Qed. @@ -277,9 +277,9 @@ Proof. induction l1; intros; crush; auto. destruct l2 eqn:EQl2. crush. - simpl in H. invert H. + simpl in H. inv H. destruct n; simpl in *. - invert H0. simpl. reflexivity. + inv H0. simpl. reflexivity. eauto. Qed. @@ -1068,7 +1068,7 @@ rs assoc``. destruct (Pos.eq_dec s d) as [EQ|EQ]; [> rewrite EQ | rewrite Registers.Regmap.gso; auto] - | [ H : opt_val_value_lessdef _ _ |- _ ] => invert H + | [ H : opt_val_value_lessdef _ _ |- _ ] => inv H | [ H : context[Z.of_nat (Z.to_nat _)] |- _ ] => rewrite Z2Nat.id in H; [> solve crush |] | [ H : _ ! _ = Some _ |- _] => setoid_rewrite H end. @@ -1102,7 +1102,7 @@ rs assoc``. econstructor. econstructor. - all: invert MARR; big_tac. Abort. + all: inv MARR; big_tac. Abort. (* inv CONST; constructor; simplify; rewrite AssocMap.gso; auto; lia. @@ -1172,7 +1172,7 @@ rs assoc``. | [ _ : context[if ?x then _ else _] |- _ ] => let EQ := fresh "EQ" in destruct x eqn:EQ; simpl in * - | [ H : ret _ _ = _ |- _ ] => invert H + | [ H : ret _ _ = _ |- _ ] => inv H | [ _ : context[match ?x with | _ => _ end] |- _ ] => destruct x end. @@ -1270,7 +1270,7 @@ rs assoc``. inv_state. inv_arr_access. + (** Preamble *) - invert MARR. inv CONST. crush. + inv MARR. inv CONST. crush. unfold Op.eval_addressing in H0. destruct (Archi.ptr64) eqn:ARCHI; crush. @@ -1284,14 +1284,14 @@ rs assoc``. subst. pose proof MASSOC as MASSOC'. - invert MASSOC'. + inv MASSOC'. pose proof (H0 r0). assert (HPler0 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; crush; eauto). apply H0 in HPler0. - invert HPler0; try congruence. + inv HPler0; try congruence. rewrite EQr0 in H11. - invert H11. + inv H11. unfold check_address_parameter_signed in *; unfold check_address_parameter_unsigned in *; crush. @@ -1393,7 +1393,7 @@ rs assoc``. by (eapply RTL.max_reg_function_def; eauto; simpl; auto). unfold Ple in HPle. lia. + (** Preamble *) - invert MARR. inv CONST. crush. + inv MARR. inv CONST. crush. unfold Op.eval_addressing in H0. destruct (Archi.ptr64) eqn:ARCHI; crush. @@ -1410,7 +1410,7 @@ rs assoc``. clear RSBPr1. pose proof MASSOC as MASSOC'. - invert MASSOC'. + inv MASSOC'. pose proof (H0 r0). pose proof (H0 r1). assert (HPler0 : Ple r0 (RTL.max_reg_function f)) @@ -1419,10 +1419,10 @@ rs assoc``. by (eapply RTL.max_reg_function_use; eauto; simpl; auto). apply H8 in HPler0. apply H11 in HPler1. - invert HPler0; invert HPler1; try congruence. + inv HPler0; inv HPler1; try congruence. rewrite EQr0 in H13. rewrite EQr1 in H14. - invert H13. invert H14. + inv H13. inv H14. clear H0. clear H8. clear H11. unfold check_address_parameter_signed in *; @@ -1524,7 +1524,7 @@ rs assoc``. by (eapply RTL.max_reg_function_def; eauto; simpl; auto). unfold Ple in HPle. lia. - + invert MARR. inv CONST. crush. + + inv MARR. inv CONST. crush. unfold Op.eval_addressing in H0. destruct (Archi.ptr64) eqn:ARCHI; crush. @@ -1652,7 +1652,7 @@ rs assoc``. inv_state. inv_arr_access. + (** Preamble *) - invert MARR. inv CONST. crush. + inv MARR. inv CONST. crush. unfold Op.eval_addressing in H0. destruct (Archi.ptr64) eqn:ARCHI; crush. @@ -1666,14 +1666,14 @@ rs assoc``. subst. pose proof MASSOC as MASSOC'. - invert MASSOC'. + inv MASSOC'. pose proof (H0 r0). assert (HPler0 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; crush; eauto). apply H8 in HPler0. - invert HPler0; try congruence. + inv HPler0; try congruence. rewrite EQr0 in H11. - invert H11. + inv H11. clear H0. clear H8. unfold check_address_parameter_unsigned in *; @@ -1799,7 +1799,7 @@ rs assoc``. assert (HPle : Ple src (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto); apply H11 in HPle. - destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert HPle; eauto. + destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; inv HPle; eauto. rewrite <- array_set_len. unfold arr_repeat. crush. @@ -1897,7 +1897,7 @@ rs assoc``. right. apply ZExtra.mod_0_bounds; try lia. apply ZLib.Z_mod_mult'. - invert H11. + inv H11. apply Zmult_lt_compat_r with (p := 4) in H14; try lia. rewrite ZLib.div_mul_undo in H14; try lia. split; try lia. @@ -1919,7 +1919,7 @@ rs assoc``. crush. exploit (BOUNDS ptr); try lia. intros. crush. exploit (BOUNDS ptr v); try lia. intros. - invert H11. + inv H11. match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity. assert (Mem.valid_access m AST.Mint32 sp' (Integers.Ptrofs.unsigned @@ -1931,7 +1931,7 @@ rs assoc``. (Integers.Ptrofs.unsigned (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) (Integers.Ptrofs.repr ptr))) v). - apply X in H11. invert H11. congruence. + apply X in H11. inv H11. congruence. constructor; simplify. unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso. @@ -1941,7 +1941,7 @@ rs assoc``. assumption. lia. + (** Preamble *) - invert MARR. inv CONST. crush. + inv MARR. inv CONST. crush. unfold Op.eval_addressing in H0. destruct (Archi.ptr64) eqn:ARCHI; crush. @@ -1958,7 +1958,7 @@ rs assoc``. clear RSBPr1. pose proof MASSOC as MASSOC'. - invert MASSOC'. + inv MASSOC'. pose proof (H0 r0). pose proof (H0 r1). assert (HPler0 : Ple r0 (RTL.max_reg_function f)) @@ -1967,10 +1967,10 @@ rs assoc``. by (eapply RTL.max_reg_function_use; eauto; simpl; auto). apply H8 in HPler0. apply H11 in HPler1. - invert HPler0; invert HPler1; try congruence. + inv HPler0; inv HPler1; try congruence. rewrite EQr0 in H13. rewrite EQr1 in H14. - invert H13. invert H14. + inv H13. inv H14. clear H0. clear H8. clear H11. unfold check_address_parameter_signed in *; @@ -2100,7 +2100,7 @@ rs assoc``. assert (Ple src (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto); apply H14 in H15. - destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H15; eauto. + destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; inv H15; eauto. rewrite <- array_set_len. unfold arr_repeat. crush. @@ -2198,7 +2198,7 @@ rs assoc``. right. apply ZExtra.mod_0_bounds; try lia. apply ZLib.Z_mod_mult'. - invert H14. + inv H14. apply Zmult_lt_compat_r with (p := 4) in H16; try lia. rewrite ZLib.div_mul_undo in H16; try lia. split; try lia. @@ -2232,14 +2232,14 @@ rs assoc``. (Integers.Ptrofs.unsigned (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) (Integers.Ptrofs.repr ptr))) v). - apply X in H14. invert H14. congruence. + apply X in H14. inv H14. congruence. constructor; simplify. unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso. assumption. lia. unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso. assumption. lia. - + invert MARR. inv CONST. crush. + + inv MARR. inv CONST. crush. unfold Op.eval_addressing in H0. destruct (Archi.ptr64) eqn:ARCHI; crush. @@ -2366,7 +2366,7 @@ rs assoc``. assert (Ple src (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto); apply H0 in H8. - destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H8; eauto. + destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; inv H8; eauto. rewrite <- array_set_len. unfold arr_repeat. crush. @@ -2455,7 +2455,7 @@ rs assoc``. right. apply ZExtra.mod_0_bounds; try lia. apply ZLib.Z_mod_mult'. - invert H0. + inv H0. apply Zmult_lt_compat_r with (p := 4) in H11; try lia. rewrite ZLib.div_mul_undo in H11; try lia. split; try lia. @@ -2476,7 +2476,7 @@ rs assoc``. crush. exploit (BOUNDS ptr); try lia. intros. crush. exploit (BOUNDS ptr v); try lia. intros. - invert H0. + inv H0. match goal with | |- ?x = _ => destruct x eqn:?EQ end; try reflexivity. assert (Mem.valid_access m AST.Mint32 sp' (Integers.Ptrofs.unsigned @@ -2488,7 +2488,7 @@ rs assoc``. (Integers.Ptrofs.unsigned (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) (Integers.Ptrofs.repr ptr))) v). - apply X in H0. invert H0. congruence. + apply X in H0. inv H0. congruence. constructor; simplify. unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso. assumption. lia. @@ -2733,12 +2733,12 @@ rs assoc``. split. unfold Mem.alloc in H. - invert H. + inv H. crush. unfold Mem.load. intros. match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence. - invert v0. unfold Mem.range_perm in H4. + inv v0. unfold Mem.range_perm in H4. unfold Mem.perm in H4. crush. unfold Mem.perm_order' in H4. small_tac. @@ -2749,12 +2749,12 @@ rs assoc``. apply proj_sumbool_true in H10. lia. unfold Mem.alloc in H. - invert H. + inv H. crush. unfold Mem.store. intros. match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence. - invert v0. unfold Mem.range_perm in H4. + inv v0. unfold Mem.range_perm in H4. unfold Mem.perm in H4. crush. unfold Mem.perm_order' in H4. small_tac. @@ -2853,7 +2853,7 @@ rs assoc``. Smallstep.final_state (RTL.semantics prog) s1 r -> Smallstep.final_state (HTL.semantics tprog) s2 r. Proof. - intros. inv H0. inv H. inv H4. invert MF. constructor. reflexivity. + intros. inv H0. inv H. inv H4. inv MF. constructor. reflexivity. Qed. #[local] Hint Resolve transl_final_states : htlproof. diff --git a/src/hls/IfConversionproof.v b/src/hls/IfConversionproof.v index e13db00..2d8cfac 100644 --- a/src/hls/IfConversionproof.v +++ b/src/hls/IfConversionproof.v @@ -673,7 +673,7 @@ Section CORRECTNESS. /\ step_list2 (Gible.step_instr ge) sp (Iexec i) b (Iexec i'). Proof using. induction x0; simplify. - - inv H1. inv H. exists nil. exists b'0. + - inv H1. inv H. exists (@nil instr). exists b'0. split; [|constructor]. rewrite app_nil_l. replace (RBexit x cf :: b'0) with ((RBexit x cf :: nil) ++ b'0) by auto. f_equal. simplify. destruct cf; auto. @@ -761,7 +761,7 @@ Section CORRECTNESS. /\ step_list2 (Gible.step_instr ge) sp (Iexec i) b (Iexec i'). Proof using. induction x0; simplify. - - inv H1. inv H. exists nil. exists b'0. + - inv H1. inv H. exists (@nil instr). exists b'0. split; [|constructor]. rewrite app_nil_l. f_equal. simplify. apply wf_transition_block_opt_prop in H0. rewrite H0. rewrite Pos.eqb_refl. auto. @@ -809,7 +809,7 @@ Section CORRECTNESS. econstructor; eauto. constructor; auto. + exploit exec_if_conv2; eauto; simplify. exploit step_cf_eq; eauto; simplify. - apply sim_plus. exists None. exists x4. + apply sim_plus. exists (@None (list instr)). exists x4. split. apply plus_one. econstructor; eauto. apply append. exists (mki rs' pr' m'). split; auto. apply step_list_2_eq; auto. @@ -838,7 +838,7 @@ Section CORRECTNESS. rewrite IS_B in H0; simplify. exploit step_cf_eq; eauto; simplify. apply sim_plus. - exists None. exists x. + exists (@None (list instr)). exists x. split; auto. unfold sem_extrap in *. inv SIM. @@ -861,14 +861,14 @@ Section CORRECTNESS. - eauto using match_some_correct. - eauto using match_none_correct. - apply sim_plus. remember (transf_function l f) as tf. symmetry in Heqtf. func_info. - exists None. eexists. split. + exists (@None (list instr)). eexists. split. apply plus_one. constructor; eauto. rewrite <- H1. eassumption. rewrite <- H4. rewrite <- H2. econstructor; auto. - - apply sim_plus. exists None. eexists. split. + - apply sim_plus. exists (@None (list instr)). eexists. split. apply plus_one. constructor; eauto. constructor; auto. - apply sim_plus. remember (transf_function None f) as tf. symmetry in Heqtf. func_info. - exists None. inv STK. inv H7. eexists. split. apply plus_one. constructor. + exists (@None (list instr)). inv STK. inv H7. eexists. split. apply plus_one. constructor. econstructor; auto. Qed. diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v index 72140cd..56d7332 100644 --- a/src/hls/Verilog.v +++ b/src/hls/Verilog.v @@ -691,14 +691,14 @@ Proof. induction e; intros; repeat (try match goal with - | [ H : expr_runp _ _ _ (Vlit _) _ |- _ ] => invert H - | [ H : expr_runp _ _ _ (Vvar _) _ |- _ ] => invert H - | [ H : expr_runp _ _ _ (Vvari _ _) _ |- _ ] => invert H - | [ H : expr_runp _ _ _ (Vinputvar _) _ |- _ ] => invert H - | [ H : expr_runp _ _ _ (Vbinop _ _ _) _ |- _ ] => invert H - | [ H : expr_runp _ _ _ (Vunop _ _) _ |- _ ] => invert H - | [ H : expr_runp _ _ _ (Vternary _ _ _) _ |- _ ] => invert H - | [ H : expr_runp _ _ _ (Vrange _ _ _) _ |- _ ] => invert H + | [ H : expr_runp _ _ _ (Vlit _) _ |- _ ] => inv H + | [ H : expr_runp _ _ _ (Vvar _) _ |- _ ] => inv H + | [ H : expr_runp _ _ _ (Vvari _ _) _ |- _ ] => inv H + | [ H : expr_runp _ _ _ (Vinputvar _) _ |- _ ] => inv H + | [ H : expr_runp _ _ _ (Vbinop _ _ _) _ |- _ ] => inv H + | [ H : expr_runp _ _ _ (Vunop _ _) _ |- _ ] => inv H + | [ H : expr_runp _ _ _ (Vternary _ _ _) _ |- _ ] => inv H + | [ H : expr_runp _ _ _ (Vrange _ _ _) _ |- _ ] => inv H | [ H1 : forall asr asa v, expr_runp _ asr asa ?e v -> _, H2 : expr_runp _ _ _ ?e _ |- _ ] => @@ -720,7 +720,7 @@ Proof. induction 1; intros; repeat (try match goal with - | [ H : location_is _ _ _ _ _ |- _ ] => invert H + | [ H : location_is _ _ _ _ _ |- _ ] => inv H | [ H1 : expr_runp _ ?asr ?asa ?e _, H2 : expr_runp _ ?asr ?asa ?e _ |- _ ] => learn (expr_runp_determinate H1 H2) @@ -736,13 +736,13 @@ Lemma stmnt_runp_determinate : induction 1; intros; repeat (try match goal with - | [ H : stmnt_runp _ _ _ (Vseq _ _) _ _ |- _ ] => invert H - | [ H : stmnt_runp _ _ _ (Vnonblock _ _) _ _ |- _ ] => invert H - | [ H : stmnt_runp _ _ _ (Vblock _ _) _ _ |- _ ] => invert H - | [ H : stmnt_runp _ _ _ Vskip _ _ |- _ ] => invert H - | [ H : stmnt_runp _ _ _ (Vcond _ _ _) _ _ |- _ ] => invert H - | [ H : stmnt_runp _ _ _ (Vcase _ (Stmntcons _ _ _) _) _ _ |- _ ] => invert H - | [ H : stmnt_runp _ _ _ (Vcase _ Stmntnil _) _ _ |- _ ] => invert H + | [ H : stmnt_runp _ _ _ (Vseq _ _) _ _ |- _ ] => inv H + | [ H : stmnt_runp _ _ _ (Vnonblock _ _) _ _ |- _ ] => inv H + | [ H : stmnt_runp _ _ _ (Vblock _ _) _ _ |- _ ] => inv H + | [ H : stmnt_runp _ _ _ Vskip _ _ |- _ ] => inv H + | [ H : stmnt_runp _ _ _ (Vcond _ _ _) _ _ |- _ ] => inv H + | [ H : stmnt_runp _ _ _ (Vcase _ (Stmntcons _ _ _) _) _ _ |- _ ] => inv H + | [ H : stmnt_runp _ _ _ (Vcase _ Stmntnil _) _ _ |- _ ] => inv H | [ H1 : expr_runp _ ?asr ?asa ?e _, H2 : expr_runp _ ?asr ?asa ?e _ |- _ ] => @@ -766,7 +766,7 @@ Lemma mi_stepp_determinate : mi_stepp f asr0 asa0 m asr1' asa1' -> asr1' = asr1 /\ asa1' = asa1. Proof. - intros. destruct m; invert H; invert H0; + intros. destruct m; inv H; inv H0; repeat (try match goal with | [ H1 : stmnt_runp _ ?asr0 ?asa0 ?s _ _, @@ -782,7 +782,7 @@ Lemma mi_stepp_negedge_determinate : mi_stepp_negedge f asr0 asa0 m asr1' asa1' -> asr1' = asr1 /\ asa1' = asa1. Proof. - intros. destruct m; invert H; invert H0; + intros. destruct m; inv H; inv H0; repeat (try match goal with | [ H1 : stmnt_runp _ ?asr0 ?asa0 ?s _ _, @@ -801,8 +801,8 @@ Proof. induction 1; intros; repeat (try match goal with - | [ H : mis_stepp _ _ _ [] _ _ |- _ ] => invert H - | [ H : mis_stepp _ _ _ ( _ :: _ ) _ _ |- _ ] => invert H + | [ H : mis_stepp _ _ _ [] _ _ |- _ ] => inv H + | [ H : mis_stepp _ _ _ ( _ :: _ ) _ _ |- _ ] => inv H | [ H1 : mi_stepp _ ?asr0 ?asa0 ?s _ _, H2 : mi_stepp _ ?asr0 ?asa0 ?s _ _ |- _ ] => @@ -824,8 +824,8 @@ Proof. induction 1; intros; repeat (try match goal with - | [ H : mis_stepp_negedge _ _ _ [] _ _ |- _ ] => invert H - | [ H : mis_stepp_negedge _ _ _ ( _ :: _ ) _ _ |- _ ] => invert H + | [ H : mis_stepp_negedge _ _ _ [] _ _ |- _ ] => inv H + | [ H : mis_stepp_negedge _ _ _ ( _ :: _ ) _ _ |- _ ] => inv H | [ H1 : mi_stepp_negedge _ ?asr0 ?asa0 ?s _ _, H2 : mi_stepp_negedge _ ?asr0 ?asa0 ?s _ _ |- _ ] => @@ -841,15 +841,15 @@ Lemma semantics_determinate : forall (p: program), Smallstep.determinate (semantics p). Proof. intros. constructor; set (ge := Globalenvs.Genv.globalenv p); simplify. - - invert H; invert H0; constructor. (* Traces are always empty *) - - invert H; invert H0; crush. assert (f = f0) by (destruct f; destruct f0; auto); subst. + - inv H; inv H0; constructor. (* Traces are always empty *) + - inv H; inv H0; crush. assert (f = f0) by (destruct f; destruct f0; auto); subst. pose proof (mis_stepp_determinate H5 H15). simplify. inv H0. inv H4. pose proof (mis_stepp_negedge_determinate H6 H17). crush. - - constructor. invert H; crush. - - invert H; invert H0; unfold ge0, ge1 in *; crush. - - red; simplify; intro; invert H0; invert H; crush. - - invert H; invert H0; crush. + - constructor. inv H; crush. + - inv H; inv H0; unfold ge0, ge1 in *; crush. + - red; simplify; intro; inv H0; inv H; crush. + - inv H; inv H0; crush. Qed. Local Open Scope positive. |