From 728888d8a3f70afd526f6c4454327f52ea4c4746 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 7 Jan 2021 17:47:55 +0100 Subject: Val_cmp* -> Val.mxcmp* --- aarch64/Asmgenproof.v | 243 ++++++++++++++++++++------------------------------ 1 file changed, 98 insertions(+), 145 deletions(-) (limited to 'aarch64/Asmgenproof.v') diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index cec8ea69..a33f90b3 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -23,7 +23,7 @@ Require Machblockgenproof Asmblockgenproof PostpassSchedulingproof. Require Import Asmgen. Require Import Axioms. Require Import IterList. -Require Import Ring. +Require Import Ring Lia. Module Asmblock_PRESERVATION. @@ -107,7 +107,7 @@ Proof. destruct (zlt _ _); try congruence. inv EQ. inv EQ0. eexists; intuition eauto. - omega. + lia. Qed. @@ -220,14 +220,14 @@ Proof. - inversion TRANSf. - unfold max_pos. assert (Asm.fn_code tf = c) as H. { inversion TRANSf as (H'); auto. } - rewrite H; omega. + rewrite H; lia. Qed. Lemma one_le_max_unsigned: 1 <= Ptrofs.max_unsigned. Proof. unfold Ptrofs.max_unsigned; simpl; unfold Ptrofs.wordsize; - unfold Wordsize_Ptrofs.wordsize; destruct Archi.ptr64; simpl; omega. + unfold Wordsize_Ptrofs.wordsize; destruct Archi.ptr64; simpl; lia. Qed. (* NB: does not seem useful anymore, with the [exec_header_simulation] proof below @@ -256,7 +256,7 @@ Proof. * apply one_le_max_unsigned. + split. * apply Z.ge_le; assumption. - * rewrite <- functions_bound_max_pos; eauto; omega. + * rewrite <- functions_bound_max_pos; eauto; lia. Qed. *) @@ -287,16 +287,16 @@ Lemma list_length_z_aux_increase A (l: list A): forall acc, list_length_z_aux l acc >= acc. Proof. induction l; simpl; intros. - - omega. - - generalize (IHl (Z.succ acc)). omega. + - lia. + - generalize (IHl (Z.succ acc)). lia. Qed. Lemma bblock_size_aux_pos bb: list_length_z (body bb) + Z.of_nat (length_opt (exit bb)) >= 1. Proof. destruct (bblock_non_empty bb), (body bb) as [|hd tl], (exit bb); simpl; - try (congruence || omega); + try (congruence || lia); unfold list_length_z; simpl; - generalize (list_length_z_aux_increase _ tl 1); omega. + generalize (list_length_z_aux_increase _ tl 1); lia. Qed. @@ -306,7 +306,7 @@ Proof. unfold list_length_z, list_length_z_aux. simpl. fold list_length_z_aux. rewrite (list_length_z_aux_shift l acc 0). - omega. + lia. Qed. Lemma list_length_z_cons A hd (tl : list A): @@ -315,14 +315,6 @@ Proof. unfold list_length_z; simpl; rewrite list_length_add_acc; reflexivity. Qed. -(*Lemma length_agree A (l : list A):*) - (*list_length_z l = Z.of_nat (length l).*) -(*Proof.*) - (*induction l as [| ? l IH]; intros.*) - (*- unfold list_length_z; reflexivity.*) - (*- simpl; rewrite list_length_z_cons, Zpos_P_of_succ_nat; omega.*) -(*Qed.*) - Lemma bblock_size_aux bb: size bb = list_length_z (header bb) + list_length_z (body bb) + Z.of_nat (length_opt (exit bb)). Proof. unfold size. @@ -335,14 +327,14 @@ Proof. rewrite bblock_size_aux. generalize (bblock_non_empty bb); intros NEMPTY; destruct NEMPTY as [HDR|EXIT]. - destruct (body bb); try contradiction; rewrite list_length_z_cons; - repeat rewrite list_length_z_nat; omega. - - destruct (exit bb); try contradiction; simpl; repeat rewrite list_length_z_nat; omega. + repeat rewrite list_length_z_nat; lia. + - destruct (exit bb); try contradiction; simpl; repeat rewrite list_length_z_nat; lia. Qed. Lemma body_size_le_block_size bb: list_length_z (body bb) <= size bb. Proof. - rewrite bblock_size_aux; repeat rewrite list_length_z_nat; omega. + rewrite bblock_size_aux; repeat rewrite list_length_z_nat; lia. Qed. @@ -351,7 +343,7 @@ Proof. rewrite (bblock_size_aux bb). generalize (bblock_size_aux_pos bb). generalize (list_length_z_pos (header bb)). - omega. + lia. Qed. Lemma unfold_car_cdr bb bbs tc: @@ -470,7 +462,7 @@ Lemma list_nth_z_neg A (l: list A): forall n, n < 0 -> list_nth_z l n = None. Proof. induction l; simpl; auto. - intros n H; destruct (zeq _ _); (try eapply IHl); omega. + intros n H; destruct (zeq _ _); (try eapply IHl); lia. Qed. Lemma find_bblock_neg bbs: forall pos, @@ -539,12 +531,12 @@ Proof. + inv FINDBB. exploit bblock_size_preserved; eauto; intros SIZE; rewrite SIZE. repeat (rewrite list_length_z_nat). rewrite app_length, Nat2Z.inj_add. - omega. + lia. + generalize (IHbbs tbbs' (pos - size bb) bb' FINDBB UNFOLD). intros IH. exploit bblock_size_preserved; eauto; intros SIZE. repeat (rewrite list_length_z_nat); rewrite app_length. rewrite Nat2Z.inj_add; repeat (rewrite <- list_length_z_nat). - omega. + lia. Qed. Lemma size_of_blocks_max_pos pos f tf bi: @@ -565,7 +557,7 @@ Lemma unfold_bblock_not_nil bb: Proof. intros. exploit bblock_size_preserved; eauto. unfold list_length_z; simpl. intros SIZE. - generalize (bblock_size_pos bb). intros SIZE'. omega. + generalize (bblock_size_pos bb). intros SIZE'. lia. Qed. (* same proof as list_nth_z_range (Coqlib) *) @@ -576,8 +568,8 @@ Proof. induction c; simpl; intros. discriminate. rewrite list_length_z_cons. destruct (zeq n 0). - generalize (list_length_z_pos c); omega. - exploit IHc; eauto. omega. + generalize (list_length_z_pos c); lia. + exploit IHc; eauto. lia. Qed. Lemma find_instr_tail: @@ -590,8 +582,8 @@ Proof. - intros. rewrite list_length_z_cons. simpl. destruct (zeq (pos + (list_length_z tbb + 1)) 0). + exploit find_instr_range; eauto. intros POS_RANGE. - generalize (list_length_z_pos tbb). omega. - + replace (pos + (list_length_z tbb + 1) - 1) with (pos + list_length_z tbb) by omega. + generalize (list_length_z_pos tbb). lia. + + replace (pos + (list_length_z tbb + 1) - 1) with (pos + list_length_z tbb) by lia. eapply IHtbb; eauto. Qed. @@ -604,7 +596,7 @@ Proof. intros (tf & _ & TRANSf). assert (pos + size bi <= max_pos tf). { eapply size_of_blocks_max_pos; eauto. } assert (max_pos tf <= Ptrofs.max_unsigned). { eapply functions_bound_max_pos; eauto. } - omega. + lia. Qed. Lemma find_instr_bblock_tail: @@ -619,10 +611,10 @@ Proof. destruct (zeq (pos + size bb) 0). + (* absurd *) exploit find_instr_range; eauto. intros POS_RANGE. - generalize (bblock_size_pos bb). intros SIZE. omega. + generalize (bblock_size_pos bb). intros SIZE. lia. + erewrite bblock_size_preserved; eauto. rewrite list_length_z_cons. - replace (pos + (list_length_z tbb + 1) - 1) with (pos + list_length_z tbb) by omega. + replace (pos + (list_length_z tbb + 1) - 1) with (pos + list_length_z tbb) by lia. apply find_instr_tail; auto. Qed. @@ -671,14 +663,14 @@ Lemma list_nth_z_find_bi_with_header: Proof. induction ll. - unfold list_length_z. simpl. intros. - replace (n - 0) with n in H by omega. eapply list_nth_z_find_bi; eauto. + replace (n - 0) with n in H by lia. eapply list_nth_z_find_bi; eauto. - intros. simpl. destruct (zeq n 0). + rewrite list_length_z_cons in H. rewrite e in H. - replace (0 - (list_length_z ll + 1)) with (-1 - (list_length_z ll)) in H by omega. + replace (0 - (list_length_z ll + 1)) with (-1 - (list_length_z ll)) in H by lia. generalize (list_length_z_pos ll). intros. - rewrite list_nth_z_neg in H; try omega. inversion H. + rewrite list_nth_z_neg in H; try lia. inversion H. + rewrite list_length_z_cons in H. - replace (n - (list_length_z ll + 1)) with (n -1 - (list_length_z ll)) in H by omega. + replace (n - (list_length_z ll + 1)) with (n -1 - (list_length_z ll)) in H by lia. eapply IHll; eauto. Qed. @@ -689,13 +681,13 @@ Lemma range_list_nth_z: exists x, list_nth_z l n = Some x. Proof. induction l. - - intros. unfold list_length_z in H. simpl in H. omega. + - intros. unfold list_length_z in H. simpl in H. lia. - intros n. destruct (zeq n 0). + intros. simpl. destruct (zeq n 0). { eauto. } contradiction. + intros H. rewrite list_length_z_cons in H. simpl. destruct (zeq n 0). { contradiction. } - replace (Z.pred n) with (n - 1) by omega. - eapply IHl; omega. + replace (Z.pred n) with (n - 1) by lia. + eapply IHl; lia. Qed. Lemma list_nth_z_n_too_big: @@ -705,17 +697,17 @@ Lemma list_nth_z_n_too_big: n >= list_length_z l. Proof. induction l. - - intros. unfold list_length_z. simpl. omega. + - intros. unfold list_length_z. simpl. lia. - intros. rewrite list_length_z_cons. simpl in H0. destruct (zeq n 0) as [N | N]. + inversion H0. + (* XXX there must be a more elegant way to prove this simple fact *) - assert (n > 0). { omega. } - assert (0 <= n - 1). { omega. } + assert (n > 0). { lia. } + assert (0 <= n - 1). { lia. } generalize (IHl (n - 1)). intros IH. assert (n - 1 >= list_length_z l). { auto. } - assert (n > list_length_z l); omega. + assert (n > list_length_z l); lia. Qed. Lemma find_instr_past_header: @@ -729,9 +721,9 @@ Proof. - intros. simpl. destruct (zeq n 0) as [N | N]. + rewrite N in H. inversion H. + rewrite list_length_z_cons. - replace (n - (list_length_z labels' + 1)) with (n - 1 - list_length_z labels') by omega. + replace (n - (list_length_z labels' + 1)) with (n - 1 - list_length_z labels') by lia. simpl in H. destruct (zeq n 0). { contradiction. } - replace (Z.pred n) with (n - 1) in H by omega. + replace (Z.pred n) with (n - 1) in H by lia. apply IH; auto. Qed. @@ -753,9 +745,9 @@ Proof. simpl; destruct (zeq n 0) as [N|N]. + rewrite N in NTH; inversion NTH. + rewrite list_length_z_cons. - replace (n - (list_length_z lbi + 1)) with (n - 1 - list_length_z lbi) by omega. + replace (n - (list_length_z lbi + 1)) with (n - 1 - list_length_z lbi) by lia. simpl in NTH. destruct (zeq n 0). { contradiction. } - replace (Z.pred n) with (n - 1) in NTH by omega. + replace (Z.pred n) with (n - 1) in NTH by lia. apply IHlbi; auto. Qed. @@ -767,15 +759,15 @@ Lemma n_beyond_body: n >= Z.of_nat (length (header bb) + length (body bb)). Proof. intros. - assert (0 <= n). { omega. } + assert (0 <= n). { lia. } generalize (list_nth_z_n_too_big label (header bb) n H2 H0). intros. generalize (list_nth_z_n_too_big _ (body bb) (n - list_length_z (header bb))). intros. unfold size in H. - assert (0 <= n - list_length_z (header bb)). { omega. } + assert (0 <= n - list_length_z (header bb)). { lia. } assert (n - list_length_z (header bb) >= list_length_z (body bb)). { apply H4; auto. } - assert (n >= list_length_z (header bb) + list_length_z (body bb)). { omega. } + assert (n >= list_length_z (header bb) + list_length_z (body bb)). { lia. } rewrite Nat2Z.inj_add. repeat (rewrite <- list_length_z_nat). assumption. Qed. @@ -910,20 +902,20 @@ Proof. repeat (rewrite Nat2Z.inj_add in UPPER). repeat (rewrite <- list_length_z_nat in UPPER). repeat (rewrite Nat2Z.inj_add in NGE). repeat (rewrite <- list_length_z_nat in NGE). simpl in UPPER. - assert (n = list_length_z (header bb) + list_length_z (body bb)). { omega. } + assert (n = list_length_z (header bb) + list_length_z (body bb)). { lia. } assert (n = size bb - 1). { unfold size. rewrite <- EXIT. simpl. - repeat (rewrite Nat2Z.inj_add). repeat (rewrite <- list_length_z_nat). simpl. omega. + repeat (rewrite Nat2Z.inj_add). repeat (rewrite <- list_length_z_nat). simpl. lia. } symmetry in EXIT. eexists; split. ** eapply is_nth_ctlflow; eauto. ** simpl. destruct (zeq (n - list_length_z (header bb) - list_length_z (body bb)) 0). { reflexivity. } - (* absurd *) omega. + (* absurd *) lia. ++ (* absurd *) unfold size in SIZE. rewrite <- EXIT in SIZE. simpl in SIZE. - destruct SIZE as (? & SIZE'). rewrite Nat.add_0_r in SIZE'. omega. + destruct SIZE as (? & SIZE'). rewrite Nat.add_0_r in SIZE'. lia. + unfold find_bblock in FINDBB; simpl in FINDBB; fold find_bblock in FINDBB. inversion UNFOLD as (UNFOLD'). apply bind_inversion in UNFOLD'. destruct UNFOLD' as (? & (UNFOLD_BBLOCK' & UNFOLD')). @@ -933,9 +925,9 @@ Proof. destruct IH as (? & (IH_is_nth & IH_find_instr)); eauto. eexists; split. * apply IH_is_nth. - * replace (Z.pos p + n) with (Z.pos p + n - size b + size b) by omega. + * replace (Z.pos p + n) with (Z.pos p + n - size b + size b) by lia. eapply find_instr_bblock_tail; try assumption. - replace (Z.pos p + n - size b) with (Z.pos p - size b + n) by omega. + replace (Z.pos p + n - size b) with (Z.pos p - size b + n) by lia. apply IH_find_instr. + (* absurd *) generalize (Pos2Z.neg_is_neg p). intros. exploit (find_bblock_neg (b :: lb)); eauto. @@ -963,11 +955,11 @@ Proof. + (* header one *) assert (Lhead: list_length_z (header bb) = 1). { rewrite EQhead; unfold list_length_z; simpl. auto. } exploit (find_instr_bblock 0); eauto. - { generalize (bblock_size_pos bb). omega. } + { generalize (bblock_size_pos bb). lia. } intros (i & NTH & FIND_INSTR). inv NTH. * rewrite EQhead in H; simpl in H. inv H. - replace (Ptrofs.unsigned ofs + 0) with (Ptrofs.unsigned ofs) in FIND_INSTR by omega. + replace (Ptrofs.unsigned ofs + 0) with (Ptrofs.unsigned ofs) in FIND_INSTR by lia. eexists. split. - eapply star_one. eapply Asm.exec_step_internal; eauto. @@ -975,12 +967,12 @@ Proof. - unfold list_length_z; simpl. split; eauto. intros r; destruct r; simpl; congruence || auto. * (* absurd case *) - erewrite list_nth_z_neg in * |-; [ congruence | rewrite Lhead; omega]. + erewrite list_nth_z_neg in * |-; [ congruence | rewrite Lhead; lia]. * (* absurd case *) - rewrite bblock_size_aux, Lhead in *. generalize (bblock_size_aux_pos bb). omega. + rewrite bblock_size_aux, Lhead in *. generalize (bblock_size_aux_pos bb). lia. + (* absurd case *) unfold list_length_z in BNDhead. simpl in *. - generalize (list_length_z_aux_increase _ l1 2); omega. + generalize (list_length_z_aux_increase _ l1 2); lia. Qed. Lemma eval_addressing_preserved a rs1 rs2: @@ -1406,57 +1398,18 @@ Proof. assert (tc' = tc) by congruence; subst. exploit (find_instr_bblock (list_length_z (header bb) + Z.of_nat n)); eauto. { unfold size; split. - - rewrite list_length_z_nat; omega. - - repeat (rewrite list_length_z_nat). repeat (rewrite Nat2Z.inj_add). omega. } + - rewrite list_length_z_nat; lia. + - repeat (rewrite list_length_z_nat). repeat (rewrite Nat2Z.inj_add). lia. } intros (i & NTH & FIND_INSTR). exists i; intros. inv NTH. - - (* absurd *) apply list_nth_z_range in H; omega. + - (* absurd *) apply list_nth_z_range in H; lia. - exists bi; rewrite Z.add_simpl_l in H; rewrite Z.add_assoc in FIND_INSTR; intuition. - (* absurd *) rewrite bblock_size_aux in H0; - rewrite H in H0; simpl in H0; repeat rewrite list_length_z_nat in H0; omega. -Qed. - -(** "is_tail" auxiliary lemma about is_tail to move in IterList ou Coqlib (déplacer aussi Machblockgenproof.is_tail_app_inv) ? *) - -Lemma is_tail_app_right A (l2 l1: list A): is_tail l1 (l2++l1). -Proof. - intros; eapply Machblockgenproof.is_tail_app_inv; econstructor. -Qed. - -Lemma is_tail_app_def A (l1 l2: list A): - is_tail l1 l2 -> exists l3, l2 = l3 ++ l1. -Proof. - induction 1 as [|x l1 l2]; simpl. - - exists nil; simpl; auto. - - destruct IHis_tail as (l3 & EQ); rewrite EQ. - exists (x::l3); simpl; auto. -Qed. - -Lemma is_tail_bound A (l1 l2: list A): - is_tail l1 l2 -> (length l1 <= length l2)%nat. -Proof. - intros H; destruct (is_tail_app_def _ _ _ H) as (l3 & EQ). - subst; rewrite app_length. - omega. -Qed. - -Lemma is_tail_list_nth_z A (l1 l2: list A): - is_tail l1 l2 -> list_nth_z l2 ((list_length_z l2) - (list_length_z l1)) = list_nth_z l1 0. -Proof. - induction 1; simpl. - - replace (list_length_z c - list_length_z c) with 0; omega || auto. - - assert (X: list_length_z (i :: c2) > list_length_z c1). - { rewrite !list_length_z_nat, <- Nat2Z.inj_gt. - exploit is_tail_bound; simpl; eauto. - omega. } - destruct (zeq (list_length_z (i :: c2) - list_length_z c1) 0) as [Y|Y]; try omega. - replace (Z.pred (list_length_z (i :: c2) - list_length_z c1)) with (list_length_z c2 - list_length_z c1); auto. - rewrite list_length_z_cons. - omega. + rewrite H in H0; simpl in H0; repeat rewrite list_length_z_nat in H0; lia. Qed. (* TODO: remplacer find_basic_instructions directement par ce lemme ? *) @@ -1474,9 +1427,9 @@ Lemma find_basic_instructions_alt b ofs f bb tc n: forall = Some i. Proof. intros; assert ((Z.to_nat n) < length (body bb))%nat. - { rewrite Nat2Z.inj_lt, <- list_length_z_nat, Z2Nat.id; try omega. } + { rewrite Nat2Z.inj_lt, <- list_length_z_nat, Z2Nat.id; try lia. } exploit find_basic_instructions; eauto. - rewrite Z2Nat.id; try omega. intros (i & bi & X). + rewrite Z2Nat.id; try lia. intros (i & bi & X). eexists; eexists; intuition eauto. Qed. @@ -1491,11 +1444,11 @@ Proof. assert (HBBPOS: list_length_z (header bb) >= 0) by eapply list_length_z_pos. assert (HBBSIZE: list_length_z (header bb) < size bb) by eapply header_size_lt_block_size. assert (OFSBOUND: 0 <= Ptrofs.unsigned ofs <= Ptrofs.max_unsigned) by eapply Ptrofs.unsigned_range_2. - assert (BBSIZE: size bb <= Ptrofs.max_unsigned) by omega. + assert (BBSIZE: size bb <= Ptrofs.max_unsigned) by lia. unfold size in BBSIZE. rewrite !Nat2Z.inj_add in BBSIZE. rewrite <- !list_length_z_nat in BBSIZE. - omega. + lia. Qed. (* A more general version of the exec_body_simulation_plus lemma below. @@ -1515,9 +1468,9 @@ Proof. induction li as [|a li]; simpl; try congruence. intros. assert (BDYLENPOS: 0 <= (list_length_z (body bb) - list_length_z (a::li)) < list_length_z (body bb)). { - assert (Z.of_nat O < list_length_z (a::li) <= list_length_z (body bb)); try omega. + assert (Z.of_nat O < list_length_z (a::li) <= list_length_z (body bb)); try lia. rewrite !list_length_z_nat; split. - - rewrite <- Nat2Z.inj_lt. simpl. omega. + - rewrite <- Nat2Z.inj_lt. simpl. lia. - rewrite <- Nat2Z.inj_le; eapply is_tail_bound; eauto. } exploit internal_functions_unfold; eauto. @@ -1549,18 +1502,18 @@ Proof. exploit (Asm.exec_step_internal tge b); eauto. { rewrite Ptrofs.add_unsigned. - repeat (rewrite Ptrofs.unsigned_repr); try omega. + repeat (rewrite Ptrofs.unsigned_repr); try lia. 2: { assert (BOUNDOFS: 0 <= Ptrofs.unsigned ofs <= Ptrofs.max_unsigned) by eapply Ptrofs.unsigned_range_2. assert (list_length_z (body bb) <= size bb) by eapply body_size_le_block_size. assert (list_length_z (header bb) <= 1). { eapply size_header; eauto. } - omega. } + lia. } try rewrite list_length_z_nat; try split; simpl; rewrite <- !list_length_z_nat; replace (Ptrofs.unsigned ofs + (list_length_z (header bb) + list_length_z (body bb) - list_length_z (a :: li))) with (Ptrofs.unsigned ofs + list_length_z (header bb) + - (list_length_z (body bb) - list_length_z (a :: li))) by omega; - try assumption; try omega. } + (list_length_z (body bb) - list_length_z (a :: li))) by lia; + try assumption; try lia. } (* This is our STEP hypothesis. *) intros STEP_NEXT. @@ -1574,18 +1527,18 @@ Proof. apply f_equal. apply f_equal. rewrite bblock_size_aux, list_length_z_cons; simpl. - omega. + lia. - exploit (IHli b ofs f bb rs1 m_next' (State rs_next' m_next')); congruence || eauto. + exploit is_tail_app_def; eauto. intros (l3 & EQ); rewrite EQ. - exploit (is_tail_app_right _ (l3 ++ a::nil)). + exploit (is_tail_app_right (l3 ++ a::nil)). rewrite <- app_assoc; simpl; eauto. + constructor; auto. rewrite ATPC_NEXT. apply f_equal. apply f_equal. rewrite! list_length_z_cons; simpl. - omega. + lia. + intros (s2' & LAST_STEPS & LAST_MATCHS). eexists. split; eauto. eapply plus_left'; eauto. @@ -1605,7 +1558,7 @@ Proof. exploit exec_body_simulation_plus_gen; eauto. - constructor. - replace (list_length_z (header bb) + list_length_z (body bb) - list_length_z (body bb)) with (list_length_z (header bb)); auto. - omega. + lia. Qed. Lemma exec_body_simulation_star b ofs f bb rs m s2 rs' m': forall @@ -1623,7 +1576,7 @@ Proof. eexists. split. eapply star_refl; eauto. assert (EQ: (size bb - Z.of_nat (length_opt (exit bb))) = list_length_z (header bb)). - { rewrite bblock_size_aux. rewrite Hbb; unfold list_length_z; simpl. omega. } + { rewrite bblock_size_aux. rewrite Hbb; unfold list_length_z; simpl. lia. } rewrite EQ; eauto. - exploit exec_body_simulation_plus; congruence || eauto. { rewrite Hbb; eauto. } @@ -1639,7 +1592,7 @@ Proof. intros N. remember (list_nth_z l n) as opt eqn:H. symmetry in H. destruct opt; auto. - exploit list_nth_z_range; eauto. omega. + exploit list_nth_z_range; eauto. lia. Qed. Lemma label_in_header_list lbl a: @@ -1651,9 +1604,9 @@ Proof. - eapply in_nil in H. contradiction. - rewrite list_length_z_cons in H0. assert (list_length_z l0 >= 0) by eapply list_length_z_pos. - assert (list_length_z l0 = 0) by omega. + assert (list_length_z l0 = 0) by lia. rewrite list_length_z_nat in H2. - assert (Datatypes.length l0 = 0%nat) by omega. + assert (Datatypes.length l0 = 0%nat) by lia. eapply length_zero_iff_nil in H3. subst. unfold In in H. destruct H. + subst; eauto. @@ -1684,7 +1637,7 @@ Proof. - intros. inversion HUNF; clear HUNF. monadInv H0. simpl in *. erewrite no_label_in_basic_inst; eauto. rewrite <- IHbdy; eauto. erewrite Zpos_P_of_succ_nat. - apply f_equal2; auto. omega. + apply f_equal2; auto. lia. Qed. Lemma asm_label_pos_header: forall z a x0 x1 lbl @@ -1696,7 +1649,7 @@ Proof. unfold size. rewrite <- plus_assoc. rewrite Nat2Z.inj_add. rewrite list_length_z_nat. - replace (z + (Z.of_nat (Datatypes.length (header a)) + Z.of_nat (Datatypes.length (body a) + length_opt (exit a)))) with (z + Z.of_nat (Datatypes.length (header a)) + Z.of_nat (Datatypes.length (body a) + length_opt (exit a))) by omega. + replace (z + (Z.of_nat (Datatypes.length (header a)) + Z.of_nat (Datatypes.length (body a) + length_opt (exit a)))) with (z + Z.of_nat (Datatypes.length (header a)) + Z.of_nat (Datatypes.length (body a) + length_opt (exit a))) by lia. eapply (label_pos_body (body a) x0 x1 (z + Z.of_nat (Datatypes.length (header a))) (exit a) lbl). auto. Qed. @@ -1707,8 +1660,8 @@ Proof. intros. destruct l1; try congruence. rewrite !list_length_z_cons in HSIZE. assert (list_length_z l1 >= 0) by eapply list_length_z_pos. - assert (list_length_z l1 + 1 + 1 >= 2) by omega. - assert (2 <= 1) by omega. contradiction H1. omega. + assert (list_length_z l1 + 1 + 1 >= 2) by lia. + assert (2 <= 1) by lia. contradiction H1. lia. Qed. Lemma label_pos_preserved_gen bbs: forall lbl c z @@ -1727,7 +1680,7 @@ Proof. unfold is_label in *. destruct (header a). * replace (z + list_length_z (@nil label)) with (z); eauto. - unfold list_length_z. simpl. omega. + unfold list_length_z. simpl. lia. * eapply header_size_cons_nil in l as HL1. subst. simpl in *. destruct (in_dec _ _); try congruence. simpl in *. @@ -1782,7 +1735,7 @@ Proof. intros; simpl in *; unfold incrPC in NEXT; inv_matchi; assert (size bb >= 1) by eapply bblock_size_pos; - assert (0 <= size bb - 1 <= Ptrofs.max_unsigned) by omega; + assert (0 <= size bb - 1 <= Ptrofs.max_unsigned) by lia; inversion NEXT; subst; eexists; eexists; split; eauto. assert (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size bb))) = Asm.nextinstr rs2). { @@ -1790,9 +1743,9 @@ Proof. intros x. destruct (PregEq.eq x PC). -- unfold Asm.nextinstr. rewrite <- AGPC. rewrite Val.offset_ptr_assoc. rewrite Ptrofs.add_unsigned. - rewrite (Ptrofs.unsigned_repr (size bb - 1)); try omega. + rewrite (Ptrofs.unsigned_repr (size bb - 1)); try lia. rewrite Ptrofs.unsigned_one. - replace (size bb - 1 + 1) with (size bb) by omega. + replace (size bb - 1 + 1) with (size bb) by lia. rewrite e. rewrite Pregmap.gss. reflexivity. -- eapply nextinstr_agree_but_pc; eauto. } @@ -1850,8 +1803,8 @@ Proof. * rewrite symbol_addresses_preserved. reflexivity. * destruct (PregEq.eq x X30). -- inv MATCHI. rewrite <- AGPC. rewrite Val.offset_ptr_assoc. - unfold Ptrofs.add, Ptrofs.one. repeat (rewrite Ptrofs.unsigned_repr); try omega. - replace (size bb - 1 + 1) with (size bb) by omega. reflexivity. + unfold Ptrofs.add, Ptrofs.one. repeat (rewrite Ptrofs.unsigned_repr); try lia. + replace (size bb - 1 + 1) with (size bb) by lia. reflexivity. -- inv MATCHI; rewrite AG; try assumption; reflexivity. } rewrite EQRS; inv MATCHI; reflexivity. - (* Pbs *) @@ -1877,7 +1830,7 @@ Proof. - destruct (PregEq.eq x X30) as [X' | X']. + inversion MATCHI; subst. rewrite <- AGPC. rewrite Val.offset_ptr_assoc. unfold Ptrofs.one. - rewrite Ptrofs.add_unsigned. rewrite Ptrofs.unsigned_repr; try omega. rewrite Ptrofs.unsigned_repr; try omega. + rewrite Ptrofs.add_unsigned. rewrite Ptrofs.unsigned_repr; try lia. rewrite Ptrofs.unsigned_repr; try lia. rewrite Z.sub_add; reflexivity. + inv_matchi. } rewrite EQRS. inv_matchi. @@ -1961,10 +1914,10 @@ Lemma last_instruction_cannot_be_label bb: list_nth_z (header bb) (size bb - 1) = None. Proof. assert (list_length_z (header bb) <= size bb - 1). { - rewrite bblock_size_aux. generalize (bblock_size_aux_pos bb). omega. + rewrite bblock_size_aux. generalize (bblock_size_aux_pos bb). lia. } remember (list_nth_z (header bb) (size bb - 1)) as label_opt; destruct label_opt; auto; - exploit list_nth_z_range; eauto; omega. + exploit list_nth_z_range; eauto; lia. Qed. Lemma pc_ptr_exec_step: forall ofs bb b rs m _rs _m @@ -1993,8 +1946,8 @@ Proof. with (Ptrofs.unsigned ofs + (size bb - 1)); try assumption. generalize (bblock_size_pos bb); generalize (Ptrofs.unsigned_range_2 ofs); intros. unfold Ptrofs.add. - rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr; try omega. - rewrite Ptrofs.unsigned_repr; omega. + rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr; try lia. + rewrite Ptrofs.unsigned_repr; lia. Qed. Lemma eval_builtin_arg_match: forall rs _m _rs a1 b1 @@ -2127,7 +2080,7 @@ Proof. intros (tc & FINDtf & TRANStf & _). exploit (find_instr_bblock (size bb - 1)); eauto. - { generalize (bblock_size_pos bb). omega. } + { generalize (bblock_size_pos bb). lia. } intros (i' & NTH & FIND_INSTR). inv NTH. @@ -2136,12 +2089,12 @@ Proof. rewrite bblock_size_aux in *. rewrite NEMPTY_EXIT' in *. simpl in *. (* XXX: Is there a better way to simplify this expression i.e. automatically? *) replace (list_length_z (header bb) + list_length_z (body bb) + 1 - 1 - - list_length_z (header bb)) with (list_length_z (body bb)) in H by omega. - rewrite list_nth_z_range_exceeded in H; try omega. discriminate. + list_length_z (header bb)) with (list_length_z (body bb)) in H by lia. + rewrite list_nth_z_range_exceeded in H; try lia. discriminate. + assert (Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned). { eapply size_of_blocks_bounds; eauto. } - assert (size bb <= Ptrofs.max_unsigned). { generalize (Ptrofs.unsigned_range_2 ofs); omega. } + assert (size bb <= Ptrofs.max_unsigned). { generalize (Ptrofs.unsigned_range_2 ofs); lia. } destruct cfi. * (* control flow instruction *) destruct s2. @@ -2179,9 +2132,9 @@ Proof. { rewrite <- AGPC. rewrite ATPC. unfold Val.offset_ptr. rewrite Ptrofs.add_assoc. unfold Ptrofs.add. assert (BBPOS: size bb >= 1) by eapply bblock_size_pos. - rewrite (Ptrofs.unsigned_repr (size bb - 1)); try omega. + rewrite (Ptrofs.unsigned_repr (size bb - 1)); try lia. rewrite Ptrofs.unsigned_one. - replace (size bb - 1 + 1) with (size bb) by omega. + replace (size bb - 1 + 1) with (size bb) by lia. reflexivity. } apply set_builtin_res_dont_move_pc_gen. -- erewrite !set_builtin_map_not_pc. @@ -2216,7 +2169,7 @@ Proof. apply functional_extensionality. intros x. destruct (PregEq.eq x PC) as [X|]. - rewrite X. rewrite <- AGPC. simpl. - replace (size bb - 0) with (size bb) by omega. reflexivity. + replace (size bb - 0) with (size bb) by lia. reflexivity. - rewrite AG; try assumption. reflexivity. } destruct X. -- cgit