diff options
Diffstat (limited to 'aarch64/Asmblockgenproof0.v')
-rw-r--r-- | aarch64/Asmblockgenproof0.v | 43 |
1 files changed, 22 insertions, 21 deletions
diff --git a/aarch64/Asmblockgenproof0.v b/aarch64/Asmblockgenproof0.v index 03d863a3..004cfd5c 100644 --- a/aarch64/Asmblockgenproof0.v +++ b/aarch64/Asmblockgenproof0.v @@ -38,6 +38,7 @@ Require Import Asmblockgen. Require Import Conventions1. Require Import Axioms. Require Import Asmblockprops. +Require Import Lia. Module MB:=Machblock. Module AB:=Asmblock. @@ -395,7 +396,7 @@ Inductive code_tail: Z -> bblocks -> bblocks -> Prop := Lemma code_tail_pos: forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0. Proof. - induction 1. omega. generalize (size_positive bi); intros; omega. + induction 1. lia. generalize (size_positive bi); intros; lia. Qed. Lemma find_bblock_tail: @@ -405,10 +406,10 @@ Lemma find_bblock_tail: Proof. induction c1; simpl; intros. inversion H. - destruct (zlt pos 0). generalize (code_tail_pos _ _ _ H); intro; omega. + destruct (zlt pos 0). generalize (code_tail_pos _ _ _ H); intro; lia. destruct (zeq pos 0). subst pos. - inv H. auto. generalize (size_positive a) (code_tail_pos _ _ _ H4). intro; omega. - inv H. congruence. replace (pos0 + size a - size a) with pos0 by omega. + inv H. auto. generalize (size_positive a) (code_tail_pos _ _ _ H4). intro; lia. + inv H. congruence. replace (pos0 + size a - size a) with pos0 by lia. eauto. Qed. @@ -422,13 +423,13 @@ Proof. induction 1; intros. - subst; eauto. - replace (pos + size bi + size bi0) with ((pos + size bi0) + size bi); eauto. - omega. + lia. Qed. Lemma size_blocks_pos c: 0 <= size_blocks c. Proof. - induction c as [| a l ]; simpl; try omega. - generalize (size_positive a); omega. + induction c as [| a l ]; simpl; try lia. + generalize (size_positive a); lia. Qed. Remark code_tail_positive: @@ -436,15 +437,15 @@ Remark code_tail_positive: code_tail ofs fn c -> 0 <= ofs. Proof. induction 1; intros; simpl. - - omega. - - generalize (size_positive bi). omega. + - lia. + - generalize (size_positive bi). lia. Qed. Remark code_tail_size: forall fn ofs c, code_tail ofs fn c -> size_blocks fn = ofs + size_blocks c. Proof. - induction 1; intros; simpl; try omega. + induction 1; intros; simpl; try lia. Qed. Remark code_tail_bounds fn ofs c: @@ -453,7 +454,7 @@ Proof. intro H; exploit code_tail_size; eauto. generalize (code_tail_positive _ _ _ H), (size_blocks_pos c). - omega. + lia. Qed. Local Hint Resolve code_tail_next: core. @@ -470,8 +471,8 @@ Proof. intros. rewrite Ptrofs.add_unsigned, Ptrofs.unsigned_repr. - rewrite Ptrofs.unsigned_repr; eauto. - omega. - - rewrite Ptrofs.unsigned_repr; omega. + lia. + - rewrite Ptrofs.unsigned_repr; lia. Qed. (** The [find_label] function returns the code tail starting at the @@ -505,12 +506,12 @@ Proof. simpl; intros until c'. case (is_label lbl a). - intros. inv H. exists pos. split; auto. split. - replace (pos - pos) with 0 by omega. constructor. constructor; try omega. - generalize (size_blocks_pos c). generalize (size_positive a). omega. + replace (pos - pos) with 0 by lia. constructor. constructor; try lia. + generalize (size_blocks_pos c). generalize (size_positive a). lia. - intros. generalize (IHc (pos+size a) c' H). intros [pos' [A [B C]]]. exists pos'. split. auto. split. - replace (pos' - pos) with ((pos' - (pos + (size a))) + (size a)) by omega. - constructor. auto. generalize (size_positive a). omega. + replace (pos' - pos) with ((pos' - (pos + (size a))) + (size a)) by lia. + constructor. auto. generalize (size_positive a). lia. Qed. (** Predictor for return addresses in generated Asm code. @@ -589,7 +590,7 @@ Proof. exists (Ptrofs.repr ofs). red; intros. rewrite Ptrofs.unsigned_repr. congruence. exploit code_tail_bounds; eauto. - intros; apply transf_function_len in TF. omega. + intros; apply transf_function_len in TF. lia. + exists Ptrofs.zero; red; intros. congruence. Qed. @@ -613,7 +614,7 @@ Inductive transl_code_at_pc (ge: MB.genv): Remark code_tail_no_bigger: forall pos c1 c2, code_tail pos c1 c2 -> (length c2 <= length c1)%nat. Proof. - induction 1; simpl; omega. + induction 1; simpl; lia. Qed. Remark code_tail_unique: @@ -621,8 +622,8 @@ Remark code_tail_unique: code_tail pos fn c -> code_tail pos' fn c -> pos = pos'. Proof. induction fn; intros until pos'; intros ITA CT; inv ITA; inv CT; auto. - generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega. - generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega. + generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; lia. + generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; lia. f_equal. eauto. Qed. |