From aba0e740f25ffa5c338dfa76cab71144802cebc2 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 21 Jun 2020 18:22:00 +0200 Subject: Replace `omega` tactic with `lia` Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`. --- backend/Allocproof.v | 6 +- backend/Asmgenproof0.v | 32 ++--- backend/Bounds.v | 8 +- backend/CSEproof.v | 58 ++++----- backend/CleanupLabelsproof.v | 2 +- backend/Cminor.v | 4 +- backend/CminorSel.v | 8 +- backend/Constpropproof.v | 4 +- backend/Conventions.v | 14 +-- backend/Deadcodeproof.v | 20 +-- backend/Inlining.v | 14 +-- backend/Inliningproof.v | 174 +++++++++++++------------- backend/Inliningspec.v | 110 ++++++++-------- backend/Linearizeproof.v | 8 +- backend/Locations.v | 20 +-- backend/NeedDomain.v | 90 ++++++------- backend/RTL.v | 42 +++---- backend/RTLgenproof.v | 2 +- backend/SelectDivproof.v | 186 +++++++++++++-------------- backend/Selectionproof.v | 18 +-- backend/SplitLongproof.v | 30 ++--- backend/Stackingproof.v | 26 ++-- backend/Tailcallproof.v | 52 ++++---- backend/Tunnelingproof.v | 8 +- backend/Unusedglobproof.v | 22 ++-- backend/ValueAnalysis.v | 22 ++-- backend/ValueDomain.v | 292 +++++++++++++++++++++---------------------- 27 files changed, 636 insertions(+), 636 deletions(-) (limited to 'backend') diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 51755912..3fdbacbe 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -548,7 +548,7 @@ Proof. unfold select_reg_l; intros. destruct H. red in H. congruence. rewrite Pos.leb_le in *. red in H. destruct H as [A | [A B]]. - red in A. zify; omega. + red in A. zify; lia. rewrite <- A; auto. Qed. @@ -560,7 +560,7 @@ Proof. unfold select_reg_h; intros. destruct H. red in H. congruence. rewrite Pos.leb_le in *. red in H. destruct H as [A | [A B]]. - red in A. zify; omega. + red in A. zify; lia. rewrite A; auto. Qed. @@ -568,7 +568,7 @@ Remark select_reg_charact: forall r q, select_reg_l r q = true /\ select_reg_h r q = true <-> ereg q = r. Proof. unfold select_reg_l, select_reg_h; intros; split. - rewrite ! Pos.leb_le. unfold reg; zify; omega. + rewrite ! Pos.leb_le. unfold reg; zify; lia. intros. rewrite H. rewrite ! Pos.leb_refl; auto. Qed. diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index 3638c465..5e8acd6f 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -473,7 +473,7 @@ Inductive code_tail: Z -> code -> code -> Prop := Lemma code_tail_pos: forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0. Proof. - induction 1. omega. omega. + induction 1. lia. lia. Qed. Lemma find_instr_tail: @@ -484,8 +484,8 @@ Proof. induction c1; simpl; intros. inv H. destruct (zeq pos 0). subst pos. - inv H. auto. generalize (code_tail_pos _ _ _ H4). intro. omegaContradiction. - inv H. congruence. replace (pos0 + 1 - 1) with pos0 by omega. + inv H. auto. generalize (code_tail_pos _ _ _ H4). intro. extlia. + inv H. congruence. replace (pos0 + 1 - 1) with pos0 by lia. eauto. Qed. @@ -494,8 +494,8 @@ Remark code_tail_bounds_1: code_tail ofs fn c -> 0 <= ofs <= list_length_z fn. Proof. induction 1; intros; simpl. - generalize (list_length_z_pos c). omega. - rewrite list_length_z_cons. omega. + generalize (list_length_z_pos c). lia. + rewrite list_length_z_cons. lia. Qed. Remark code_tail_bounds_2: @@ -505,8 +505,8 @@ Proof. assert (forall ofs fn c, code_tail ofs fn c -> forall i c', c = i :: c' -> 0 <= ofs < list_length_z fn). induction 1; intros; simpl. - rewrite H. rewrite list_length_z_cons. generalize (list_length_z_pos c'). omega. - rewrite list_length_z_cons. generalize (IHcode_tail _ _ H0). omega. + rewrite H. rewrite list_length_z_cons. generalize (list_length_z_pos c'). lia. + rewrite list_length_z_cons. generalize (IHcode_tail _ _ H0). lia. eauto. Qed. @@ -531,7 +531,7 @@ Lemma code_tail_next_int: Proof. intros. rewrite Ptrofs.add_unsigned, Ptrofs.unsigned_one. rewrite Ptrofs.unsigned_repr. apply code_tail_next with i; auto. - generalize (code_tail_bounds_2 _ _ _ _ H0). omega. + generalize (code_tail_bounds_2 _ _ _ _ H0). lia. Qed. (** [transl_code_at_pc pc fb f c ep tf tc] holds if the code pointer [pc] points @@ -654,7 +654,7 @@ Opaque transl_instr. exists (Ptrofs.repr ofs). red; intros. rewrite Ptrofs.unsigned_repr. congruence. exploit code_tail_bounds_1; eauto. - apply transf_function_len in TF. omega. + apply transf_function_len in TF. lia. + exists Ptrofs.zero; red; intros. congruence. Qed. @@ -663,7 +663,7 @@ End RETADDR_EXISTS. 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: @@ -671,8 +671,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. @@ -713,13 +713,13 @@ Proof. case (is_label lbl a). intro EQ; injection EQ; intro; subst c'. exists (pos + 1). split. auto. split. - replace (pos + 1 - pos) with (0 + 1) by omega. constructor. constructor. - rewrite list_length_z_cons. generalize (list_length_z_pos c). omega. + replace (pos + 1 - pos) with (0 + 1) by lia. constructor. constructor. + rewrite list_length_z_cons. generalize (list_length_z_pos c). lia. intros. generalize (IHc (pos + 1) c' H). intros [pos' [A [B C]]]. exists pos'. split. auto. split. - replace (pos' - pos) with ((pos' - (pos + 1)) + 1) by omega. + replace (pos' - pos) with ((pos' - (pos + 1)) + 1) by lia. constructor. auto. - rewrite list_length_z_cons. omega. + rewrite list_length_z_cons. lia. Qed. (** Helper lemmas to reason about diff --git a/backend/Bounds.v b/backend/Bounds.v index fa695234..4231d861 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -163,7 +163,7 @@ Proof. intros until valu. unfold max_over_list. assert (forall l z, fold_left (fun x y => Z.max x (valu y)) l z >= z). induction l; simpl; intros. - omega. apply Zge_trans with (Z.max z (valu a)). + lia. apply Zge_trans with (Z.max z (valu a)). auto. apply Z.le_ge. apply Z.le_max_l. auto. Qed. @@ -307,7 +307,7 @@ Proof. let f := fold_left (fun x y => Z.max x (valu y)) c z in z <= f /\ (In x c -> valu x <= f)). induction c; simpl; intros. - split. omega. tauto. + split. lia. tauto. elim (IHc (Z.max z (valu a))); intros. split. apply Z.le_trans with (Z.max z (valu a)). apply Z.le_max_l. auto. intro H1; elim H1; intro. @@ -446,12 +446,12 @@ Lemma size_callee_save_area_rec_incr: Proof. Local Opaque mreg_type. induction l as [ | r l]; intros; simpl. -- omega. +- lia. - eapply Z.le_trans. 2: apply IHl. generalize (AST.typesize_pos (mreg_type r)); intros. apply Z.le_trans with (align ofs (AST.typesize (mreg_type r))). apply align_le; auto. - omega. + lia. Qed. Lemma size_callee_save_area_incr: diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 03c7ecfc..a2a1b461 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -128,9 +128,9 @@ Proof. exists valu2; splitall. + constructor; simpl; intros. * constructor; simpl; intros. - apply wf_equation_incr with (num_next n). eauto with cse. xomega. + apply wf_equation_incr with (num_next n). eauto with cse. extlia. rewrite PTree.gsspec in H0. destruct (peq r0 r). - inv H0; xomega. + inv H0; extlia. apply Plt_trans_succ; eauto with cse. rewrite PMap.gsspec in H0. destruct (peq v (num_next n)). replace r0 with r by (simpl in H0; intuition). rewrite PTree.gss. subst; auto. @@ -142,8 +142,8 @@ Proof. rewrite peq_false. eauto with cse. apply Plt_ne; eauto with cse. + unfold valu2. rewrite peq_true; auto. + auto. -+ xomega. -+ xomega. ++ extlia. ++ extlia. Qed. Lemma valnum_regs_holds: @@ -158,7 +158,7 @@ Lemma valnum_regs_holds: /\ Ple n.(num_next) n'.(num_next). Proof. induction rl; simpl; intros. -- inv H0. exists valu1; splitall; auto. red; auto. simpl; tauto. xomega. +- inv H0. exists valu1; splitall; auto. red; auto. simpl; tauto. extlia. - destruct (valnum_reg n a) as [n1 v1] eqn:V1. destruct (valnum_regs n1 rl) as [n2 vs] eqn:V2. inv H0. @@ -169,9 +169,9 @@ Proof. exists valu3; splitall. + auto. + simpl; f_equal; auto. rewrite R; auto. - + red; intros. transitivity (valu2 v); auto. apply R. xomega. - + simpl; intros. destruct H0; auto. subst v1; xomega. - + xomega. + + red; intros. transitivity (valu2 v); auto. apply R. extlia. + + simpl; intros. destruct H0; auto. subst v1; extlia. + + extlia. Qed. Lemma find_valnum_rhs_charact: @@ -327,11 +327,11 @@ Proof. { red; intros. unfold valu2. apply peq_false. apply Plt_ne; auto. } exists valu2; constructor; simpl; intros. + constructor; simpl; intros. - * destruct H3. inv H3. simpl; split. xomega. + * destruct H3. inv H3. simpl; split. extlia. red; intros. apply Plt_trans_succ; eauto. - apply wf_equation_incr with (num_next n). eauto with cse. xomega. + apply wf_equation_incr with (num_next n). eauto with cse. extlia. * rewrite PTree.gsspec in H3. destruct (peq r rd). - inv H3. xomega. + inv H3. extlia. apply Plt_trans_succ; eauto with cse. * apply update_reg_charact; eauto with cse. + destruct H3. inv H3. @@ -495,10 +495,10 @@ Lemma store_normalized_range_sound: Proof. intros. unfold Val.load_result; remember Archi.ptr64 as ptr64. destruct chunk; simpl in *; destruct v; auto. -- inv H. rewrite is_sgn_sign_ext in H4 by omega. rewrite H4; auto. -- inv H. rewrite is_uns_zero_ext in H4 by omega. rewrite H4; auto. -- inv H. rewrite is_sgn_sign_ext in H4 by omega. rewrite H4; auto. -- inv H. rewrite is_uns_zero_ext in H4 by omega. rewrite H4; auto. +- inv H. rewrite is_sgn_sign_ext in H4 by lia. rewrite H4; auto. +- inv H. rewrite is_uns_zero_ext in H4 by lia. rewrite H4; auto. +- inv H. rewrite is_sgn_sign_ext in H4 by lia. rewrite H4; auto. +- inv H. rewrite is_uns_zero_ext in H4 by lia. rewrite H4; auto. - destruct ptr64; auto. - destruct ptr64; auto. - destruct ptr64; auto. @@ -557,7 +557,7 @@ Proof. simpl. rewrite negb_false_iff in H8. eapply Mem.load_storebytes_other. eauto. - rewrite H6. rewrite Z2Nat.id by omega. + rewrite H6. rewrite Z2Nat.id by lia. eapply pdisjoint_sound. eauto. unfold aaddressing. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto. erewrite <- regs_valnums_sound by eauto. eauto with va. @@ -578,39 +578,39 @@ Proof. set (n1 := i - ofs1). set (n2 := size_chunk chunk). set (n3 := sz - (n1 + n2)). - replace sz with (n1 + (n2 + n3)) in H by (unfold n3, n2, n1; omega). + replace sz with (n1 + (n2 + n3)) in H by (unfold n3, n2, n1; lia). exploit Mem.loadbytes_split; eauto. - unfold n1; omega. - unfold n3, n2, n1; omega. + unfold n1; lia. + unfold n3, n2, n1; lia. intros (bytes1 & bytes23 & LB1 & LB23 & EQ). clear H. exploit Mem.loadbytes_split; eauto. - unfold n2; omega. - unfold n3, n2, n1; omega. + unfold n2; lia. + unfold n3, n2, n1; lia. intros (bytes2 & bytes3 & LB2 & LB3 & EQ'). subst bytes23; subst bytes. exploit Mem.load_loadbytes; eauto. intros (bytes2' & A & B). assert (bytes2' = bytes2). - { replace (ofs1 + n1) with i in LB2 by (unfold n1; omega). unfold n2 in LB2. congruence. } + { replace (ofs1 + n1) with i in LB2 by (unfold n1; lia). unfold n2 in LB2. congruence. } subst bytes2'. exploit Mem.storebytes_split; eauto. intros (m1 & SB1 & SB23). clear H0. exploit Mem.storebytes_split; eauto. intros (m2 & SB2 & SB3). clear SB23. assert (L1: Z.of_nat (length bytes1) = n1). - { erewrite Mem.loadbytes_length by eauto. apply Z2Nat.id. unfold n1; omega. } + { erewrite Mem.loadbytes_length by eauto. apply Z2Nat.id. unfold n1; lia. } assert (L2: Z.of_nat (length bytes2) = n2). - { erewrite Mem.loadbytes_length by eauto. apply Z2Nat.id. unfold n2; omega. } + { erewrite Mem.loadbytes_length by eauto. apply Z2Nat.id. unfold n2; lia. } rewrite L1 in *. rewrite L2 in *. assert (LB': Mem.loadbytes m2 b2 (ofs2 + n1) n2 = Some bytes2). { rewrite <- L2. eapply Mem.loadbytes_storebytes_same; eauto. } assert (LB'': Mem.loadbytes m' b2 (ofs2 + n1) n2 = Some bytes2). { rewrite <- LB'. eapply Mem.loadbytes_storebytes_other; eauto. - unfold n2; omega. - right; left; omega. } + unfold n2; lia. + right; left; lia. } exploit Mem.load_valid_access; eauto. intros [P Q]. rewrite B. apply Mem.loadbytes_load. - replace (i + (ofs2 - ofs1)) with (ofs2 + n1) by (unfold n1; omega). + replace (i + (ofs2 - ofs1)) with (ofs2 + n1) by (unfold n1; lia). exact LB''. apply Z.divide_add_r; auto. Qed. @@ -655,9 +655,9 @@ Proof with (try discriminate). Mem.loadv chunk m (Vptr sp ofs) = Some v -> Mem.loadv chunk m' (Vptr sp (Ptrofs.repr j)) = Some v). { - simpl; intros. rewrite Ptrofs.unsigned_repr by omega. + simpl; intros. rewrite Ptrofs.unsigned_repr by lia. unfold j, delta. eapply load_memcpy; eauto. - apply Zmod_divide; auto. generalize (align_chunk_pos chunk); omega. + apply Zmod_divide; auto. generalize (align_chunk_pos chunk); lia. } inv H2. + inv H3. exploit eval_addressing_Ainstack_inv; eauto. intros [E1 E2]. diff --git a/backend/CleanupLabelsproof.v b/backend/CleanupLabelsproof.v index e92be2b4..fb8e57b7 100644 --- a/backend/CleanupLabelsproof.v +++ b/backend/CleanupLabelsproof.v @@ -286,7 +286,7 @@ Proof. constructor. econstructor; eauto with coqlib. (* eliminated *) - right. split. simpl. omega. split. auto. econstructor; eauto with coqlib. + right. split. simpl. lia. split. auto. econstructor; eauto with coqlib. (* Lgoto *) left; econstructor; split. econstructor. eapply find_label_translated; eauto. red; auto. diff --git a/backend/Cminor.v b/backend/Cminor.v index 91a4c104..cf0ba314 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -588,7 +588,7 @@ Proof. exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. exists (Returnstate vres2 k m2). econstructor; eauto. (* trace length *) - red; intros; inv H; simpl; try omega; eapply external_call_trace_length; eauto. + red; intros; inv H; simpl; try lia; eapply external_call_trace_length; eauto. Qed. (** This semantics is determinate. *) @@ -645,7 +645,7 @@ Proof. intros (A & B). split; intros; auto. apply B in H; destruct H; congruence. - (* single event *) - red; simpl. destruct 1; simpl; try omega; + red; simpl. destruct 1; simpl; try lia; eapply external_call_trace_length; eauto. - (* initial states *) inv H; inv H0. unfold ge0, ge1 in *. congruence. diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 96cb8ae6..5cbdc249 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -522,9 +522,9 @@ Lemma insert_lenv_lookup1: nth_error le' n = Some v. Proof. induction 1; intros. - omegaContradiction. + extlia. destruct n; simpl; simpl in H0. auto. - apply IHinsert_lenv. auto. omega. + apply IHinsert_lenv. auto. lia. Qed. Lemma insert_lenv_lookup2: @@ -536,8 +536,8 @@ Lemma insert_lenv_lookup2: Proof. induction 1; intros. simpl. assumption. - simpl. destruct n. omegaContradiction. - apply IHinsert_lenv. exact H0. omega. + simpl. destruct n. extlia. + apply IHinsert_lenv. exact H0. lia. Qed. Lemma eval_lift_expr: diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index a5d08a0f..a3592c4d 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -364,7 +364,7 @@ Proof. - (* Inop, skipped over *) assert (s0 = pc') by congruence. subst s0. - right; exists n; split. omega. split. auto. + right; exists n; split. lia. split. auto. apply match_states_intro; auto. - (* Iop *) @@ -528,7 +528,7 @@ Opaque builtin_strength_reduction. - (* Icond, skipped over *) rewrite H1 in H; inv H. - right; exists n; split. omega. split. auto. + right; exists n; split. lia. split. auto. econstructor; eauto. - (* Ijumptable *) diff --git a/backend/Conventions.v b/backend/Conventions.v index 14ffb587..8910ee49 100644 --- a/backend/Conventions.v +++ b/backend/Conventions.v @@ -60,9 +60,9 @@ Remark fold_max_outgoing_above: forall l n, fold_left max_outgoing_2 l n >= n. Proof. assert (A: forall n l, max_outgoing_1 n l >= n). - { intros; unfold max_outgoing_1. destruct l as [_ | []]; xomega. } + { intros; unfold max_outgoing_1. destruct l as [_ | []]; extlia. } induction l; simpl; intros. - - omega. + - lia. - eapply Zge_trans. eauto. destruct a; simpl. apply A. eapply Zge_trans; eauto. Qed. @@ -80,14 +80,14 @@ Lemma loc_arguments_bounded: Proof. intros until ty. assert (A: forall n l, n <= max_outgoing_1 n l). - { intros; unfold max_outgoing_1. destruct l as [_ | []]; xomega. } + { intros; unfold max_outgoing_1. destruct l as [_ | []]; extlia. } assert (B: forall p n, In (S Outgoing ofs ty) (regs_of_rpair p) -> ofs + typesize ty <= max_outgoing_2 n p). { intros. destruct p; simpl in H; intuition; subst; simpl. - - xomega. - - eapply Z.le_trans. 2: apply A. xomega. - - xomega. } + - extlia. + - eapply Z.le_trans. 2: apply A. extlia. + - extlia. } assert (C: forall l n, In (S Outgoing ofs ty) (regs_of_rpairs l) -> ofs + typesize ty <= fold_left max_outgoing_2 l n). @@ -168,7 +168,7 @@ Proof. unfold loc_argument_acceptable. destruct l; intros. auto. destruct sl; try contradiction. destruct H1. generalize (loc_arguments_bounded _ _ _ H0). - generalize (typesize_pos ty). omega. + generalize (typesize_pos ty). lia. Qed. diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index 2edc0395..7aa6ff88 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -67,7 +67,7 @@ Lemma mextends_agree: forall m1 m2 P, Mem.extends m1 m2 -> magree m1 m2 P. Proof. intros. destruct H. destruct mext_inj. constructor; intros. -- replace ofs with (ofs + 0) by omega. eapply mi_perm; eauto. auto. +- replace ofs with (ofs + 0) by lia. eapply mi_perm; eauto. auto. - eauto. - exploit mi_memval; eauto. unfold inject_id; eauto. rewrite Z.add_0_r. auto. @@ -99,15 +99,15 @@ Proof. induction n; intros; simpl. constructor. rewrite Nat2Z.inj_succ in H. constructor. - apply H. omega. - apply IHn. intros; apply H; omega. + apply H. lia. + apply IHn. intros; apply H; lia. } Local Transparent Mem.loadbytes. unfold Mem.loadbytes; intros. destruct H. destruct (Mem.range_perm_dec m1 b ofs (ofs + n) Cur Readable); inv H0. rewrite pred_dec_true. econstructor; split; eauto. apply GETN. intros. rewrite Z_to_nat_max in H. - assert (ofs <= i < ofs + n) by xomega. + assert (ofs <= i < ofs + n) by extlia. apply ma_memval0; auto. red; intros; eauto. Qed. @@ -146,11 +146,11 @@ Proof. (ZMap.get q (Mem.setN bytes2 p c2))). { induction 1; intros; simpl. - - apply H; auto. simpl. omega. + - apply H; auto. simpl. lia. - simpl length in H1; rewrite Nat2Z.inj_succ in H1. apply IHlist_forall2; auto. intros. rewrite ! ZMap.gsspec. destruct (ZIndexed.eq i p). auto. - apply H1; auto. unfold ZIndexed.t in *; omega. + apply H1; auto. unfold ZIndexed.t in *; lia. } intros. destruct (Mem.range_perm_storebytes m2 b ofs bytes2) as [m2' ST2]. @@ -211,8 +211,8 @@ Proof. - rewrite (Mem.storebytes_mem_contents _ _ _ _ _ H0). rewrite PMap.gsspec. destruct (peq b0 b). + subst b0. rewrite Mem.setN_outside. eapply ma_memval; eauto. eapply Mem.perm_storebytes_2; eauto. - destruct (zlt ofs0 ofs); auto. destruct (zle (ofs + Z.of_nat (length bytes1)) ofs0); try omega. - elim (H1 ofs0). omega. auto. + destruct (zlt ofs0 ofs); auto. destruct (zle (ofs + Z.of_nat (length bytes1)) ofs0); try lia. + elim (H1 ofs0). lia. auto. + eapply ma_memval; eauto. eapply Mem.perm_storebytes_2; eauto. - rewrite (Mem.nextblock_storebytes _ _ _ _ _ H0). eapply ma_nextblock; eauto. @@ -966,7 +966,7 @@ Ltac UseTransfer := intros. eapply nlive_remove; eauto. unfold adst, vanalyze; rewrite AN; eapply aaddr_arg_sound_1; eauto. erewrite Mem.loadbytes_length in H1 by eauto. - rewrite Z2Nat.id in H1 by omega. auto. + rewrite Z2Nat.id in H1 by lia. auto. eauto. intros (tm' & A & B). econstructor; split. @@ -993,7 +993,7 @@ Ltac UseTransfer := intros (bc & A & B & C). intros. eapply nlive_contains; eauto. erewrite Mem.loadbytes_length in H0 by eauto. - rewrite Z2Nat.id in H0 by omega. auto. + rewrite Z2Nat.id in H0 by lia. auto. + (* annot *) destruct (transfer_builtin_args (kill_builtin_res res ne, nm) _x2) as (ne1, nm1) eqn:TR. InvSoundState. diff --git a/backend/Inlining.v b/backend/Inlining.v index f7ee4166..7eb0f0fa 100644 --- a/backend/Inlining.v +++ b/backend/Inlining.v @@ -71,12 +71,12 @@ Inductive sincr (s1 s2: state) : Prop := Remark sincr_refl: forall s, sincr s s. Proof. - intros; constructor; xomega. + intros; constructor; extlia. Qed. Lemma sincr_trans: forall s1 s2 s3, sincr s1 s2 -> sincr s2 s3 -> sincr s1 s3. Proof. - intros. inv H; inv H0. constructor; xomega. + intros. inv H; inv H0. constructor; extlia. Qed. (** Dependently-typed state monad, ensuring that the final state is @@ -111,7 +111,7 @@ Program Definition set_instr (pc: node) (i: instruction): mon unit := (mkstate s.(st_nextreg) s.(st_nextnode) (PTree.set pc i s.(st_code)) s.(st_stksize)) _. Next Obligation. - intros; constructor; simpl; xomega. + intros; constructor; simpl; extlia. Qed. Program Definition add_instr (i: instruction): mon node := @@ -121,7 +121,7 @@ Program Definition add_instr (i: instruction): mon node := (mkstate s.(st_nextreg) (Pos.succ pc) (PTree.set pc i s.(st_code)) s.(st_stksize)) _. Next Obligation. - intros; constructor; simpl; xomega. + intros; constructor; simpl; extlia. Qed. Program Definition reserve_nodes (numnodes: positive): mon positive := @@ -130,7 +130,7 @@ Program Definition reserve_nodes (numnodes: positive): mon positive := (mkstate s.(st_nextreg) (Pos.add s.(st_nextnode) numnodes) s.(st_code) s.(st_stksize)) _. Next Obligation. - intros; constructor; simpl; xomega. + intros; constructor; simpl; extlia. Qed. Program Definition reserve_regs (numregs: positive): mon positive := @@ -139,7 +139,7 @@ Program Definition reserve_regs (numregs: positive): mon positive := (mkstate (Pos.add s.(st_nextreg) numregs) s.(st_nextnode) s.(st_code) s.(st_stksize)) _. Next Obligation. - intros; constructor; simpl; xomega. + intros; constructor; simpl; extlia. Qed. Program Definition request_stack (sz: Z): mon unit := @@ -148,7 +148,7 @@ Program Definition request_stack (sz: Z): mon unit := (mkstate s.(st_nextreg) s.(st_nextnode) s.(st_code) (Z.max s.(st_stksize) sz)) _. Next Obligation. - intros; constructor; simpl; xomega. + intros; constructor; simpl; extlia. Qed. Program Definition ptree_mfold {A: Type} (f: positive -> A -> mon unit) (t: PTree.t A): mon unit := diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index cc84b1cc..0434a4a4 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -67,21 +67,21 @@ Qed. Remark sreg_below_diff: forall ctx r r', Plt r' ctx.(dreg) -> sreg ctx r <> r'. Proof. - intros. zify. unfold sreg; rewrite shiftpos_eq. xomega. + intros. zify. unfold sreg; rewrite shiftpos_eq. extlia. Qed. Remark context_below_diff: forall ctx1 ctx2 r1 r2, context_below ctx1 ctx2 -> Ple r1 ctx1.(mreg) -> sreg ctx1 r1 <> sreg ctx2 r2. Proof. - intros. red in H. zify. unfold sreg; rewrite ! shiftpos_eq. xomega. + intros. red in H. zify. unfold sreg; rewrite ! shiftpos_eq. extlia. Qed. Remark context_below_lt: forall ctx1 ctx2 r, context_below ctx1 ctx2 -> Ple r ctx1.(mreg) -> Plt (sreg ctx1 r) ctx2.(dreg). Proof. intros. red in H. unfold Plt; zify. unfold sreg; rewrite shiftpos_eq. - xomega. + extlia. Qed. (* @@ -89,7 +89,7 @@ Remark context_below_le: forall ctx1 ctx2 r, context_below ctx1 ctx2 -> Ple r ctx1.(mreg) -> Ple (sreg ctx1 r) ctx2.(dreg). Proof. intros. red in H. unfold Ple; zify. unfold sreg; rewrite shiftpos_eq. - xomega. + extlia. Qed. *) @@ -105,7 +105,7 @@ Definition val_reg_charact (F: meminj) (ctx: context) (rs': regset) (v: val) (r: Remark Plt_Ple_dec: forall p q, {Plt p q} + {Ple q p}. Proof. - intros. destruct (plt p q). left; auto. right; xomega. + intros. destruct (plt p q). left; auto. right; extlia. Qed. Lemma agree_val_reg_gen: @@ -149,7 +149,7 @@ Proof. repeat rewrite Regmap.gsspec. destruct (peq r0 r). subst r0. rewrite peq_true. auto. rewrite peq_false. auto. apply shiftpos_diff; auto. - rewrite Regmap.gso. auto. xomega. + rewrite Regmap.gso. auto. extlia. Qed. Lemma agree_set_reg_undef: @@ -184,7 +184,7 @@ Proof. unfold agree_regs; intros. destruct H. split; intros. rewrite H0. auto. apply shiftpos_above. - eapply Pos.lt_le_trans. apply shiftpos_below. xomega. + eapply Pos.lt_le_trans. apply shiftpos_below. extlia. apply H1; auto. Qed. @@ -272,7 +272,7 @@ Lemma range_private_invariant: range_private F1 m1 m1' sp lo hi. Proof. intros; red; intros. exploit H; eauto. intros [A B]. split; auto. - intros; red; intros. exploit H0; eauto. omega. intros [P Q]. + intros; red; intros. exploit H0; eauto. lia. intros [P Q]. eelim B; eauto. Qed. @@ -293,12 +293,12 @@ Lemma range_private_alloc_left: range_private F1 m1 m' sp' (base + Z.max sz 0) hi. Proof. intros; red; intros. - exploit (H ofs). generalize (Z.le_max_r sz 0). omega. intros [A B]. + exploit (H ofs). generalize (Z.le_max_r sz 0). lia. intros [A B]. split; auto. intros; red; intros. exploit Mem.perm_alloc_inv; eauto. destruct (eq_block b sp); intros. subst b. rewrite H1 in H4; inv H4. - rewrite Zmax_spec in H3. destruct (zlt 0 sz); omega. + rewrite Zmax_spec in H3. destruct (zlt 0 sz); lia. rewrite H2 in H4; auto. eelim B; eauto. Qed. @@ -313,21 +313,21 @@ Proof. intros; red; intros. destruct (zlt ofs (base + Z.max sz 0)) as [z|z]. red; split. - replace ofs with ((ofs - base) + base) by omega. + replace ofs with ((ofs - base) + base) by lia. eapply Mem.perm_inject; eauto. eapply Mem.free_range_perm; eauto. - rewrite Zmax_spec in z. destruct (zlt 0 sz); omega. + rewrite Zmax_spec in z. destruct (zlt 0 sz); lia. intros; red; intros. destruct (eq_block b b0). subst b0. rewrite H1 in H4; inv H4. - eelim Mem.perm_free_2; eauto. rewrite Zmax_spec in z. destruct (zlt 0 sz); omega. + eelim Mem.perm_free_2; eauto. rewrite Zmax_spec in z. destruct (zlt 0 sz); lia. exploit Mem.mi_no_overlap; eauto. apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. eapply Mem.free_range_perm. eauto. - instantiate (1 := ofs - base). rewrite Zmax_spec in z. destruct (zlt 0 sz); omega. + instantiate (1 := ofs - base). rewrite Zmax_spec in z. destruct (zlt 0 sz); lia. eapply Mem.perm_free_3; eauto. - intros [A | A]. congruence. omega. + intros [A | A]. congruence. lia. - exploit (H ofs). omega. intros [A B]. split. auto. + exploit (H ofs). lia. intros [A B]. split. auto. intros; red; intros. eelim B; eauto. eapply Mem.perm_free_3; eauto. Qed. @@ -607,39 +607,39 @@ Proof. (* cons *) apply match_stacks_cons with (fenv := fenv) (ctx := ctx); auto. eapply match_stacks_inside_invariant; eauto. - intros; eapply INJ; eauto; xomega. - intros; eapply PERM1; eauto; xomega. - intros; eapply PERM2; eauto; xomega. - intros; eapply PERM3; eauto; xomega. + intros; eapply INJ; eauto; extlia. + intros; eapply PERM1; eauto; extlia. + intros; eapply PERM2; eauto; extlia. + intros; eapply PERM3; eauto; extlia. eapply agree_regs_incr; eauto. eapply range_private_invariant; eauto. (* untailcall *) apply match_stacks_untailcall with (ctx := ctx); auto. eapply match_stacks_inside_invariant; eauto. - intros; eapply INJ; eauto; xomega. - intros; eapply PERM1; eauto; xomega. - intros; eapply PERM2; eauto; xomega. - intros; eapply PERM3; eauto; xomega. + intros; eapply INJ; eauto; extlia. + intros; eapply PERM1; eauto; extlia. + intros; eapply PERM2; eauto; extlia. + intros; eapply PERM3; eauto; extlia. eapply range_private_invariant; eauto. induction 1; intros. (* base *) eapply match_stacks_inside_base; eauto. eapply match_stacks_invariant; eauto. - intros; eapply INJ; eauto; xomega. - intros; eapply PERM1; eauto; xomega. - intros; eapply PERM2; eauto; xomega. - intros; eapply PERM3; eauto; xomega. + intros; eapply INJ; eauto; extlia. + intros; eapply PERM1; eauto; extlia. + intros; eapply PERM2; eauto; extlia. + intros; eapply PERM3; eauto; extlia. (* inlined *) apply match_stacks_inside_inlined with (fenv := fenv) (ctx' := ctx'); auto. apply IHmatch_stacks_inside; auto. - intros. apply RS. red in BELOW. xomega. + intros. apply RS. red in BELOW. extlia. apply agree_regs_incr with F; auto. apply agree_regs_invariant with rs'; auto. - intros. apply RS. red in BELOW. xomega. + intros. apply RS. red in BELOW. extlia. eapply range_private_invariant; eauto. - intros. split. eapply INJ; eauto. xomega. eapply PERM1; eauto. xomega. - intros. eapply PERM2; eauto. xomega. + intros. split. eapply INJ; eauto. extlia. eapply PERM1; eauto. extlia. + intros. eapply PERM2; eauto. extlia. Qed. Lemma match_stacks_empty: @@ -668,7 +668,7 @@ Lemma match_stacks_inside_set_reg: match_stacks_inside F m m' stk stk' f' ctx sp' (rs'#(sreg ctx r) <- v). Proof. intros. eapply match_stacks_inside_invariant; eauto. - intros. apply Regmap.gso. zify. unfold sreg; rewrite shiftpos_eq. xomega. + intros. apply Regmap.gso. zify. unfold sreg; rewrite shiftpos_eq. extlia. Qed. Lemma match_stacks_inside_set_res: @@ -717,11 +717,11 @@ Proof. subst b1. rewrite H1 in H4. inv H4. eelim Plt_strict; eauto. (* inlined *) eapply match_stacks_inside_inlined; eauto. - eapply IHmatch_stacks_inside; eauto. destruct SBELOW. omega. + eapply IHmatch_stacks_inside; eauto. destruct SBELOW. lia. eapply agree_regs_incr; eauto. eapply range_private_invariant; eauto. intros. exploit Mem.perm_alloc_inv; eauto. destruct (eq_block b0 b); intros. - subst b0. rewrite H2 in H5; inv H5. elimtype False; xomega. + subst b0. rewrite H2 in H5; inv H5. elimtype False; extlia. rewrite H3 in H5; auto. Qed. @@ -753,25 +753,25 @@ Lemma min_alignment_sound: Proof. intros; red; intros. unfold min_alignment in H. assert (2 <= sz -> (2 | n)). intros. - destruct (zle sz 1). omegaContradiction. + destruct (zle sz 1). extlia. destruct (zle sz 2). auto. destruct (zle sz 4). apply Z.divide_trans with 4; auto. exists 2; auto. apply Z.divide_trans with 8; auto. exists 4; auto. assert (4 <= sz -> (4 | n)). intros. - destruct (zle sz 1). omegaContradiction. - destruct (zle sz 2). omegaContradiction. + destruct (zle sz 1). extlia. + destruct (zle sz 2). extlia. destruct (zle sz 4). auto. apply Z.divide_trans with 8; auto. exists 2; auto. assert (8 <= sz -> (8 | n)). intros. - destruct (zle sz 1). omegaContradiction. - destruct (zle sz 2). omegaContradiction. - destruct (zle sz 4). omegaContradiction. + destruct (zle sz 1). extlia. + destruct (zle sz 2). extlia. + destruct (zle sz 4). extlia. auto. destruct chunk; simpl in *; auto. apply Z.divide_1_l. apply Z.divide_1_l. - apply H2; omega. - apply H2; omega. + apply H2; lia. + apply H2; lia. Qed. (** Preservation by external calls *) @@ -803,19 +803,19 @@ Proof. inv MG. constructor; intros; eauto. destruct (F1 b1) as [[b2' delta']|] eqn:?. exploit INCR; eauto. intros EQ; rewrite H0 in EQ; inv EQ. eapply IMAGE; eauto. - exploit SEP; eauto. intros [A B]. elim B. red. xomega. + exploit SEP; eauto. intros [A B]. elim B. red. extlia. eapply match_stacks_cons; eauto. - eapply match_stacks_inside_extcall; eauto. xomega. + eapply match_stacks_inside_extcall; eauto. extlia. eapply agree_regs_incr; eauto. - eapply range_private_extcall; eauto. red; xomega. - intros. apply SSZ2; auto. apply MAXPERM'; auto. red; xomega. + eapply range_private_extcall; eauto. red; extlia. + intros. apply SSZ2; auto. apply MAXPERM'; auto. red; extlia. eapply match_stacks_untailcall; eauto. - eapply match_stacks_inside_extcall; eauto. xomega. - eapply range_private_extcall; eauto. red; xomega. - intros. apply SSZ2; auto. apply MAXPERM'; auto. red; xomega. + eapply match_stacks_inside_extcall; eauto. extlia. + eapply range_private_extcall; eauto. red; extlia. + intros. apply SSZ2; auto. apply MAXPERM'; auto. red; extlia. induction 1; intros. eapply match_stacks_inside_base; eauto. - eapply match_stacks_extcall; eauto. xomega. + eapply match_stacks_extcall; eauto. extlia. eapply match_stacks_inside_inlined; eauto. eapply agree_regs_incr; eauto. eapply range_private_extcall; eauto. @@ -829,7 +829,7 @@ Lemma align_unchanged: forall n amount, amount > 0 -> (amount | n) -> align n amount = n. Proof. intros. destruct H0 as [p EQ]. subst n. unfold align. decEq. - apply Zdiv_unique with (b := amount - 1). omega. omega. + apply Zdiv_unique with (b := amount - 1). lia. lia. Qed. Lemma match_stacks_inside_inlined_tailcall: @@ -849,10 +849,10 @@ Proof. (* inlined *) assert (dstk ctx <= dstk ctx'). rewrite H1. apply align_le. apply min_alignment_pos. eapply match_stacks_inside_inlined; eauto. - red; intros. destruct (zlt ofs (dstk ctx)). apply PAD; omega. apply H3. inv H4. xomega. + red; intros. destruct (zlt ofs (dstk ctx)). apply PAD; lia. apply H3. inv H4. extlia. congruence. - unfold context_below in *. xomega. - unfold context_stack_call in *. omega. + unfold context_below in *. extlia. + unfold context_stack_call in *. lia. Qed. (** ** Relating states *) @@ -1014,12 +1014,12 @@ Proof. + (* inlined *) assert (EQ: fd = Internal f0) by (eapply find_inlined_function; eauto). subst fd. - right; split. simpl; omega. split. auto. + right; split. simpl; lia. split. auto. econstructor; eauto. eapply match_stacks_inside_inlined; eauto. - red; intros. apply PRIV. inv H13. destruct H16. xomega. + red; intros. apply PRIV. inv H13. destruct H16. extlia. apply agree_val_regs_gen; auto. - red; intros; apply PRIV. destruct H16. omega. + red; intros; apply PRIV. destruct H16. lia. - (* tailcall *) exploit match_stacks_inside_globalenvs; eauto. intros [bound G]. @@ -1032,9 +1032,9 @@ Proof. assert (X: { m1' | Mem.free m'0 sp' 0 (fn_stacksize f') = Some m1'}). apply Mem.range_perm_free. red; intros. destruct (zlt ofs f.(fn_stacksize)). - replace ofs with (ofs + dstk ctx) by omega. eapply Mem.perm_inject; eauto. - eapply Mem.free_range_perm; eauto. omega. - inv FB. eapply range_private_perms; eauto. xomega. + replace ofs with (ofs + dstk ctx) by lia. eapply Mem.perm_inject; eauto. + eapply Mem.free_range_perm; eauto. lia. + inv FB. eapply range_private_perms; eauto. extlia. destruct X as [m1' FREE]. left; econstructor; split. eapply plus_one. eapply exec_Itailcall; eauto. @@ -1045,12 +1045,12 @@ Proof. intros. eapply Mem.perm_free_3; eauto. intros. eapply Mem.perm_free_1; eauto with ordered_type. intros. eapply Mem.perm_free_3; eauto. - erewrite Mem.nextblock_free; eauto. red in VB; xomega. + erewrite Mem.nextblock_free; eauto. red in VB; extlia. eapply agree_val_regs; eauto. eapply Mem.free_right_inject; eauto. eapply Mem.free_left_inject; eauto. (* show that no valid location points into the stack block being freed *) - intros. rewrite DSTK in PRIV'. exploit (PRIV' (ofs + delta)). omega. intros [P Q]. - eelim Q; eauto. replace (ofs + delta - delta) with ofs by omega. + intros. rewrite DSTK in PRIV'. exploit (PRIV' (ofs + delta)). lia. intros [P Q]. + eelim Q; eauto. replace (ofs + delta - delta) with ofs by lia. apply Mem.perm_max with k. apply Mem.perm_implies with p; auto with mem. + (* turned into a call *) left; econstructor; split. @@ -1065,7 +1065,7 @@ Proof. + (* inlined *) assert (EQ: fd = Internal f0) by (eapply find_inlined_function; eauto). subst fd. - right; split. simpl; omega. split. auto. + right; split. simpl; lia. split. auto. econstructor; eauto. eapply match_stacks_inside_inlined_tailcall; eauto. eapply match_stacks_inside_invariant; eauto. @@ -1074,7 +1074,7 @@ Proof. eapply Mem.free_left_inject; eauto. red; intros; apply PRIV'. assert (dstk ctx <= dstk ctx'). red in H14; rewrite H14. apply align_le. apply min_alignment_pos. - omega. + lia. - (* builtin *) exploit tr_funbody_inv; eauto. intros TR; inv TR. @@ -1124,10 +1124,10 @@ Proof. assert (X: { m1' | Mem.free m'0 sp' 0 (fn_stacksize f') = Some m1'}). apply Mem.range_perm_free. red; intros. destruct (zlt ofs f.(fn_stacksize)). - replace ofs with (ofs + dstk ctx) by omega. eapply Mem.perm_inject; eauto. - eapply Mem.free_range_perm; eauto. omega. + replace ofs with (ofs + dstk ctx) by lia. eapply Mem.perm_inject; eauto. + eapply Mem.free_range_perm; eauto. lia. inv FB. eapply range_private_perms; eauto. - generalize (Zmax_spec (fn_stacksize f) 0). destruct (zlt 0 (fn_stacksize f)); omega. + generalize (Zmax_spec (fn_stacksize f) 0). destruct (zlt 0 (fn_stacksize f)); lia. destruct X as [m1' FREE]. left; econstructor; split. eapply plus_one. eapply exec_Ireturn; eauto. @@ -1137,19 +1137,19 @@ Proof. intros. eapply Mem.perm_free_3; eauto. intros. eapply Mem.perm_free_1; eauto with ordered_type. intros. eapply Mem.perm_free_3; eauto. - erewrite Mem.nextblock_free; eauto. red in VB; xomega. + erewrite Mem.nextblock_free; eauto. red in VB; extlia. destruct or; simpl. apply agree_val_reg; auto. auto. eapply Mem.free_right_inject; eauto. eapply Mem.free_left_inject; eauto. (* show that no valid location points into the stack block being freed *) intros. inversion FB; subst. assert (PRIV': range_private F m' m'0 sp' (dstk ctx) f'.(fn_stacksize)). rewrite H8 in PRIV. eapply range_private_free_left; eauto. - rewrite DSTK in PRIV'. exploit (PRIV' (ofs + delta)). omega. intros [A B]. - eelim B; eauto. replace (ofs + delta - delta) with ofs by omega. + rewrite DSTK in PRIV'. exploit (PRIV' (ofs + delta)). lia. intros [A B]. + eelim B; eauto. replace (ofs + delta - delta) with ofs by lia. apply Mem.perm_max with k. apply Mem.perm_implies with p; auto with mem. + (* inlined *) - right. split. simpl. omega. split. auto. + right. split. simpl. lia. split. auto. econstructor; eauto. eapply match_stacks_inside_invariant; eauto. intros. eapply Mem.perm_free_3; eauto. @@ -1165,7 +1165,7 @@ Proof. { eapply tr_function_linkorder; eauto. } inversion TR; subst. exploit Mem.alloc_parallel_inject. eauto. eauto. apply Z.le_refl. - instantiate (1 := fn_stacksize f'). inv H1. xomega. + instantiate (1 := fn_stacksize f'). inv H1. extlia. intros [F' [m1' [sp' [A [B [C [D E]]]]]]]. left; econstructor; split. eapply plus_one. eapply exec_function_internal; eauto. @@ -1187,13 +1187,13 @@ Proof. rewrite H5. apply agree_regs_init_regs. eauto. auto. inv H1; auto. congruence. auto. eapply Mem.valid_new_block; eauto. red; intros. split. - eapply Mem.perm_alloc_2; eauto. inv H1; xomega. + eapply Mem.perm_alloc_2; eauto. inv H1; extlia. intros; red; intros. exploit Mem.perm_alloc_inv. eexact H. eauto. destruct (eq_block b stk); intros. - subst. rewrite D in H9; inv H9. inv H1; xomega. + subst. rewrite D in H9; inv H9. inv H1; extlia. rewrite E in H9; auto. eelim Mem.fresh_block_alloc. eexact A. eapply Mem.mi_mappedblocks; eauto. auto. - intros. exploit Mem.perm_alloc_inv; eauto. rewrite dec_eq_true. omega. + intros. exploit Mem.perm_alloc_inv; eauto. rewrite dec_eq_true. lia. - (* internal function, inlined *) inversion FB; subst. @@ -1203,19 +1203,19 @@ Proof. (* sp' is valid *) instantiate (1 := sp'). auto. (* offset is representable *) - instantiate (1 := dstk ctx). generalize (Z.le_max_r (fn_stacksize f) 0). omega. + instantiate (1 := dstk ctx). generalize (Z.le_max_r (fn_stacksize f) 0). lia. (* size of target block is representable *) - intros. right. exploit SSZ2; eauto with mem. inv FB; omega. + intros. right. exploit SSZ2; eauto with mem. inv FB; lia. (* we have full permissions on sp' at and above dstk ctx *) intros. apply Mem.perm_cur. apply Mem.perm_implies with Freeable; auto with mem. - eapply range_private_perms; eauto. xomega. + eapply range_private_perms; eauto. extlia. (* offset is aligned *) - replace (fn_stacksize f - 0) with (fn_stacksize f) by omega. + replace (fn_stacksize f - 0) with (fn_stacksize f) by lia. inv FB. apply min_alignment_sound; auto. (* nobody maps to (sp, dstk ctx...) *) - intros. exploit (PRIV (ofs + delta')); eauto. xomega. + intros. exploit (PRIV (ofs + delta')); eauto. extlia. intros [A B]. eelim B; eauto. - replace (ofs + delta' - delta') with ofs by omega. + replace (ofs + delta' - delta') with ofs by lia. apply Mem.perm_max with k. apply Mem.perm_implies with p; auto with mem. intros [F' [A [B [C D]]]]. exploit tr_moves_init_regs; eauto. intros [rs'' [P [Q R]]]. @@ -1224,7 +1224,7 @@ Proof. econstructor. eapply match_stacks_inside_alloc_left; eauto. eapply match_stacks_inside_invariant; eauto. - omega. + lia. eauto. auto. apply agree_regs_incr with F; auto. auto. auto. auto. @@ -1245,7 +1245,7 @@ Proof. eapply match_stacks_extcall with (F1 := F) (F2 := F1) (m1 := m) (m1' := m'0); eauto. intros; eapply external_call_max_perm; eauto. intros; eapply external_call_max_perm; eauto. - xomega. + extlia. eapply external_call_nextblock; eauto. auto. auto. @@ -1267,14 +1267,14 @@ Proof. eauto. auto. apply agree_set_reg; auto. auto. auto. auto. - red; intros. destruct (zlt ofs (dstk ctx)). apply PAD; omega. apply PRIV; omega. + red; intros. destruct (zlt ofs (dstk ctx)). apply PAD; lia. apply PRIV; lia. auto. auto. - (* return from inlined function *) inv MS0; try congruence. rewrite RET0 in RET; inv RET. unfold inline_return in AT. assert (PRIV': range_private F m m' sp' (dstk ctx' + mstk ctx') f'.(fn_stacksize)). - red; intros. destruct (zlt ofs (dstk ctx)). apply PAD. omega. apply PRIV. omega. + red; intros. destruct (zlt ofs (dstk ctx)). apply PAD. lia. apply PRIV. lia. destruct or. + (* with a result *) left; econstructor; split. diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v index c345c942..477f883a 100644 --- a/backend/Inliningspec.v +++ b/backend/Inliningspec.v @@ -73,7 +73,7 @@ Qed. Lemma shiftpos_eq: forall x y, Zpos (shiftpos x y) = (Zpos x + Zpos y) - 1. Proof. intros. unfold shiftpos. zify. try rewrite Pos2Z.inj_sub. auto. - zify. omega. + zify. lia. Qed. Lemma shiftpos_inj: @@ -82,7 +82,7 @@ Proof. intros. assert (Zpos (shiftpos x n) = Zpos (shiftpos y n)) by congruence. rewrite ! shiftpos_eq in H0. - assert (Z.pos x = Z.pos y) by omega. + assert (Z.pos x = Z.pos y) by lia. congruence. Qed. @@ -95,25 +95,25 @@ Qed. Lemma shiftpos_above: forall x n, Ple n (shiftpos x n). Proof. - intros. unfold Ple; zify. rewrite shiftpos_eq. xomega. + intros. unfold Ple; zify. rewrite shiftpos_eq. extlia. Qed. Lemma shiftpos_not_below: forall x n, Plt (shiftpos x n) n -> False. Proof. - intros. generalize (shiftpos_above x n). xomega. + intros. generalize (shiftpos_above x n). extlia. Qed. Lemma shiftpos_below: forall x n, Plt (shiftpos x n) (Pos.add x n). Proof. - intros. unfold Plt; zify. rewrite shiftpos_eq. omega. + intros. unfold Plt; zify. rewrite shiftpos_eq. lia. Qed. Lemma shiftpos_le: forall x y n, Ple x y -> Ple (shiftpos x n) (shiftpos y n). Proof. - intros. unfold Ple in *; zify. rewrite ! shiftpos_eq. omega. + intros. unfold Ple in *; zify. rewrite ! shiftpos_eq. lia. Qed. @@ -219,9 +219,9 @@ Proof. induction srcs; simpl; intros. monadInv H. auto. destruct dsts; monadInv H. auto. - transitivity (st_code s0)!pc. eapply IHsrcs; eauto. monadInv EQ; simpl. xomega. + transitivity (st_code s0)!pc. eapply IHsrcs; eauto. monadInv EQ; simpl. extlia. monadInv EQ; simpl. apply PTree.gso. - inversion INCR0; simpl in *. xomega. + inversion INCR0; simpl in *. extlia. Qed. Lemma add_moves_spec: @@ -234,13 +234,13 @@ Proof. monadInv H. apply tr_moves_nil; auto. destruct dsts; monadInv H. apply tr_moves_nil; auto. apply tr_moves_cons with x. eapply IHsrcs; eauto. - intros. inversion INCR. apply H0; xomega. + intros. inversion INCR. apply H0; extlia. monadInv EQ. rewrite H0. erewrite add_moves_unchanged; eauto. simpl. apply PTree.gss. - simpl. xomega. - xomega. - inversion INCR; inversion INCR0; simpl in *; xomega. + simpl. extlia. + extlia. + inversion INCR; inversion INCR0; simpl in *; extlia. Qed. (** ** Relational specification of CFG expansion *) @@ -386,9 +386,9 @@ Proof. monadInv H. unfold inline_function in EQ. monadInv EQ. transitivity (s2.(st_code)!pc'). eauto. transitivity (s5.(st_code)!pc'). eapply add_moves_unchanged; eauto. - left. inversion INCR5. inversion INCR3. monadInv EQ1; simpl in *. xomega. + left. inversion INCR5. inversion INCR3. monadInv EQ1; simpl in *. extlia. transitivity (s4.(st_code)!pc'). eapply rec_unchanged; eauto. - simpl. monadInv EQ; simpl. monadInv EQ1; simpl. xomega. + simpl. monadInv EQ; simpl. monadInv EQ1; simpl. extlia. simpl. monadInv EQ1; simpl. auto. monadInv EQ; simpl. monadInv EQ1; simpl. auto. (* tailcall *) @@ -397,9 +397,9 @@ Proof. monadInv H. unfold inline_tail_function in EQ. monadInv EQ. transitivity (s2.(st_code)!pc'). eauto. transitivity (s5.(st_code)!pc'). eapply add_moves_unchanged; eauto. - left. inversion INCR5. inversion INCR3. monadInv EQ1; simpl in *. xomega. + left. inversion INCR5. inversion INCR3. monadInv EQ1; simpl in *. extlia. transitivity (s4.(st_code)!pc'). eapply rec_unchanged; eauto. - simpl. monadInv EQ; simpl. monadInv EQ1; simpl. xomega. + simpl. monadInv EQ; simpl. monadInv EQ1; simpl. extlia. simpl. monadInv EQ1; simpl. auto. monadInv EQ; simpl. monadInv EQ1; simpl. auto. (* return *) @@ -422,7 +422,7 @@ Proof. destruct a as [pc1 instr1]; simpl in *. monadInv H. inv H3. transitivity ((st_code s0)!pc). - eapply IHl; eauto. destruct INCR; xomega. destruct INCR; xomega. + eapply IHl; eauto. destruct INCR; extlia. destruct INCR; extlia. eapply expand_instr_unchanged; eauto. Qed. @@ -438,7 +438,7 @@ Proof. exploit ptree_mfold_spec; eauto. intros [INCR' ITER]. eapply iter_expand_instr_unchanged; eauto. subst s0; auto. - subst s0; simpl. xomega. + subst s0; simpl. extlia. red; intros. exploit list_in_map_inv; eauto. intros [pc1 [A B]]. subst pc. unfold spc in H1. eapply shiftpos_not_below; eauto. apply PTree.elements_keys_norepet. @@ -464,7 +464,7 @@ Remark min_alignment_pos: forall sz, min_alignment sz > 0. Proof. intros; unfold min_alignment. - destruct (zle sz 1). omega. destruct (zle sz 2). omega. destruct (zle sz 4); omega. + destruct (zle sz 1). lia. destruct (zle sz 2). lia. destruct (zle sz 4); lia. Qed. Ltac inv_incr := @@ -501,20 +501,20 @@ Proof. apply tr_call_inlined with (pc1 := x0) (ctx' := ctx') (f := f); auto. eapply BASE; eauto. eapply add_moves_spec; eauto. - intros. rewrite S1. eapply set_instr_other; eauto. unfold node; xomega. - xomega. xomega. + intros. rewrite S1. eapply set_instr_other; eauto. unfold node; extlia. + extlia. extlia. eapply rec_spec; eauto. red; intros. rewrite PTree.grspec in H. destruct (PTree.elt_eq id0 id); try discriminate. auto. - simpl. subst s2; simpl in *; xomega. - simpl. subst s3; simpl in *; xomega. - simpl. xomega. + simpl. subst s2; simpl in *; extlia. + simpl. subst s3; simpl in *; extlia. + simpl. extlia. simpl. apply align_divides. apply min_alignment_pos. - assert (dstk ctx + mstk ctx <= dstk ctx'). simpl. apply align_le. apply min_alignment_pos. omega. - omega. + assert (dstk ctx + mstk ctx <= dstk ctx'). simpl. apply align_le. apply min_alignment_pos. lia. + lia. intros. simpl in H. rewrite S1. - transitivity (s1.(st_code)!pc0). eapply set_instr_other; eauto. unfold node in *; xomega. - eapply add_moves_unchanged; eauto. unfold node in *; xomega. xomega. - red; simpl. subst s2; simpl in *. xomega. + transitivity (s1.(st_code)!pc0). eapply set_instr_other; eauto. unfold node in *; extlia. + eapply add_moves_unchanged; eauto. unfold node in *; extlia. extlia. + red; simpl. subst s2; simpl in *. extlia. red; simpl. split. auto. apply align_le. apply min_alignment_pos. (* tailcall *) destruct (can_inline fe s1) as [|id f P Q]. @@ -532,20 +532,20 @@ Proof. apply tr_tailcall_inlined with (pc1 := x0) (ctx' := ctx') (f := f); auto. eapply BASE; eauto. eapply add_moves_spec; eauto. - intros. rewrite S1. eapply set_instr_other; eauto. unfold node; xomega. xomega. xomega. + intros. rewrite S1. eapply set_instr_other; eauto. unfold node; extlia. extlia. extlia. eapply rec_spec; eauto. red; intros. rewrite PTree.grspec in H. destruct (PTree.elt_eq id0 id); try discriminate. auto. - simpl. subst s3; simpl in *. subst s2; simpl in *. xomega. - simpl. subst s3; simpl in *; xomega. - simpl. xomega. + simpl. subst s3; simpl in *. subst s2; simpl in *. extlia. + simpl. subst s3; simpl in *; extlia. + simpl. extlia. simpl. apply align_divides. apply min_alignment_pos. - assert (dstk ctx <= dstk ctx'). simpl. apply align_le. apply min_alignment_pos. omega. - omega. + assert (dstk ctx <= dstk ctx'). simpl. apply align_le. apply min_alignment_pos. lia. + lia. intros. simpl in H. rewrite S1. - transitivity (s1.(st_code))!pc0. eapply set_instr_other; eauto. unfold node in *; xomega. - eapply add_moves_unchanged; eauto. unfold node in *; xomega. xomega. + transitivity (s1.(st_code))!pc0. eapply set_instr_other; eauto. unfold node in *; extlia. + eapply add_moves_unchanged; eauto. unfold node in *; extlia. extlia. red; simpl. -subst s2; simpl in *; xomega. +subst s2; simpl in *; extlia. red; auto. (* builtin *) eapply tr_builtin; eauto. destruct b; eauto. @@ -577,31 +577,31 @@ Proof. destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr. assert (A: Ple ctx.(dpc) s0.(st_nextnode)). assert (B: Plt (spc ctx pc) (st_nextnode s)) by eauto. - unfold spc in B. generalize (shiftpos_above pc (dpc ctx)). xomega. + unfold spc in B. generalize (shiftpos_above pc (dpc ctx)). extlia. destruct H9. inv H. (* same pc *) eapply expand_instr_spec; eauto. - omega. + lia. intros. transitivity ((st_code s')!pc'). - apply H7. auto. xomega. + apply H7. auto. extlia. eapply iter_expand_instr_unchanged; eauto. red; intros. rewrite list_map_compose in H9. exploit list_in_map_inv; eauto. intros [[pc0 instr0] [P Q]]. simpl in P. - assert (Plt (spc ctx pc0) (st_nextnode s)) by eauto. xomega. + assert (Plt (spc ctx pc0) (st_nextnode s)) by eauto. extlia. transitivity ((st_code s')!(spc ctx pc)). eapply H8; eauto. eapply iter_expand_instr_unchanged; eauto. - assert (Plt (spc ctx pc) (st_nextnode s)) by eauto. xomega. + assert (Plt (spc ctx pc) (st_nextnode s)) by eauto. extlia. red; intros. rewrite list_map_compose in H. exploit list_in_map_inv; eauto. intros [[pc0 instr0] [P Q]]. simpl in P. assert (pc = pc0) by (eapply shiftpos_inj; eauto). subst pc0. elim H12. change pc with (fst (pc, instr0)). apply List.in_map; auto. (* older pc *) inv_incr. eapply IHl; eauto. - intros. eapply Pos.lt_le_trans. eapply H2. right; eauto. xomega. + intros. eapply Pos.lt_le_trans. eapply H2. right; eauto. extlia. intros; eapply Ple_trans; eauto. - intros. apply H7; auto. xomega. + intros. apply H7; auto. extlia. Qed. Lemma expand_cfg_rec_spec: @@ -629,16 +629,16 @@ Proof. intros. assert (Ple pc0 (max_pc_function f)). eapply max_pc_function_sound. eapply PTree.elements_complete; eauto. - eapply Pos.lt_le_trans. apply shiftpos_below. subst s0; simpl; xomega. + eapply Pos.lt_le_trans. apply shiftpos_below. subst s0; simpl; extlia. subst s0; simpl; auto. - intros. apply H8; auto. subst s0; simpl in H11; xomega. + intros. apply H8; auto. subst s0; simpl in H11; extlia. intros. apply H8. apply shiftpos_above. assert (Ple pc0 (max_pc_function f)). eapply max_pc_function_sound. eapply PTree.elements_complete; eauto. - eapply Pos.lt_le_trans. apply shiftpos_below. inversion i; xomega. + eapply Pos.lt_le_trans. apply shiftpos_below. inversion i; extlia. apply PTree.elements_correct; auto. auto. auto. auto. - inversion INCR0. subst s0; simpl in STKSIZE; xomega. + inversion INCR0. subst s0; simpl in STKSIZE; extlia. Qed. End EXPAND_INSTR. @@ -721,12 +721,12 @@ Opaque initstate. apply funenv_program_compat. eapply expand_cfg_spec with (fe := fenv); eauto. red; auto. - unfold ctx; rewrite <- H1; rewrite <- H2; rewrite <- H3; simpl. xomega. - unfold ctx; rewrite <- H0; rewrite <- H1; simpl. xomega. - simpl. xomega. + unfold ctx; rewrite <- H1; rewrite <- H2; rewrite <- H3; simpl. extlia. + unfold ctx; rewrite <- H0; rewrite <- H1; simpl. extlia. + simpl. extlia. simpl. apply Z.divide_0_r. - simpl. omega. - simpl. omega. + simpl. lia. + simpl. lia. simpl. split; auto. destruct INCR2. destruct INCR1. destruct INCR0. destruct INCR. - simpl. change 0 with (st_stksize initstate). omega. + simpl. change 0 with (st_stksize initstate). lia. Qed. diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index 10a3d8b2..b065238c 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -642,7 +642,7 @@ Proof. (* Lbranch *) assert ((reachable f)!!pc = true). apply REACH; simpl; auto. - right; split. simpl; omega. split. auto. simpl. econstructor; eauto. + right; split. simpl; lia. split. auto. simpl. econstructor; eauto. (* Lcond *) assert (REACH1: (reachable f)!!pc1 = true) by (apply REACH; simpl; auto). @@ -659,12 +659,12 @@ Proof. rewrite eval_negate_condition. rewrite H. auto. eauto. rewrite DC. econstructor; eauto. (* cond is false: branch is taken *) - right; split. simpl; omega. split. auto. rewrite <- DC. econstructor; eauto. + right; split. simpl; lia. split. auto. rewrite <- DC. econstructor; eauto. rewrite eval_negate_condition. rewrite H. auto. (* branch if cond is true *) destruct b. (* cond is true: branch is taken *) - right; split. simpl; omega. split. auto. econstructor; eauto. + right; split. simpl; lia. split. auto. econstructor; eauto. (* cond is false: no branch *) left; econstructor; split. apply plus_one. eapply exec_Lcond_false. eauto. eauto. @@ -673,7 +673,7 @@ Proof. (* Ljumptable *) assert (REACH': (reachable f)!!pc = true). apply REACH. simpl. eapply list_nth_z_in; eauto. - right; split. simpl; omega. split. auto. econstructor; eauto. + right; split. simpl; lia. split. auto. econstructor; eauto. (* Lreturn *) left; econstructor; split. diff --git a/backend/Locations.v b/backend/Locations.v index c437df5d..2a3ae1d7 100644 --- a/backend/Locations.v +++ b/backend/Locations.v @@ -157,7 +157,7 @@ Module Loc. forall l, ~(diff l l). Proof. destruct l; unfold diff; auto. - red; intros. destruct H; auto. generalize (typesize_pos ty); omega. + red; intros. destruct H; auto. generalize (typesize_pos ty); lia. Qed. Lemma diff_not_eq: @@ -184,7 +184,7 @@ Module Loc. left; auto. destruct (zle (pos0 + typesize ty0) pos). left; auto. - right; red; intros [P | [P | P]]. congruence. omega. omega. + right; red; intros [P | [P | P]]. congruence. lia. lia. left; auto. Defined. @@ -497,7 +497,7 @@ Module OrderedLoc <: OrderedType. destruct x. eelim Plt_strict; eauto. destruct H. eelim OrderedSlot.lt_not_eq; eauto. red; auto. - destruct H. destruct H0. omega. + destruct H. destruct H0. lia. destruct H0. eelim OrderedTyp.lt_not_eq; eauto. red; auto. Qed. Definition compare : forall x y : t, Compare lt eq x y. @@ -545,18 +545,18 @@ Module OrderedLoc <: OrderedType. { destruct H. apply not_eq_sym. apply Plt_ne; auto. apply Plt_ne; auto. } congruence. - assert (RANGE: forall ty, 1 <= typesize ty <= 2). - { intros; unfold typesize. destruct ty0; omega. } + { intros; unfold typesize. destruct ty0; lia. } destruct H. + destruct H. left. apply not_eq_sym. apply OrderedSlot.lt_not_eq; auto. destruct H. right. - destruct H0. right. generalize (RANGE ty'); omega. + destruct H0. right. generalize (RANGE ty'); lia. destruct H0. assert (ty' = Tint \/ ty' = Tsingle \/ ty' = Tany32). { unfold OrderedTyp.lt in H1. destruct ty'; auto; compute in H1; congruence. } - right. destruct H2 as [E|[E|E]]; subst ty'; simpl typesize; omega. + right. destruct H2 as [E|[E|E]]; subst ty'; simpl typesize; lia. + destruct H. left. apply OrderedSlot.lt_not_eq; auto. destruct H. right. - destruct H0. left; omega. + destruct H0. left; lia. destruct H0. exfalso. destruct ty'; compute in H1; congruence. Qed. @@ -572,14 +572,14 @@ Module OrderedLoc <: OrderedType. - destruct (OrderedSlot.compare sl sl'); auto. destruct H. contradiction. destruct H. - right; right; split; auto. left; omega. + right; right; split; auto. left; lia. left; right; split; auto. assert (EITHER: typesize ty' = 1 /\ OrderedTyp.lt ty' Tany64 \/ typesize ty' = 2). { destruct ty'; compute; auto. } destruct (zlt ofs' (ofs - 1)). left; auto. destruct EITHER as [[P Q] | P]. - right; split; auto. omega. - left; omega. + right; split; auto. lia. + left; lia. Qed. End OrderedLoc. diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v index d9e9e025..d3c6ed75 100644 --- a/backend/NeedDomain.v +++ b/backend/NeedDomain.v @@ -240,9 +240,9 @@ Proof. destruct (zlt i (Int.unsigned n)). - auto. - generalize (Int.unsigned_range n); intros. - apply H. omega. rewrite Int.bits_shru by omega. - replace (i - Int.unsigned n + Int.unsigned n) with i by omega. - rewrite zlt_true by omega. auto. + apply H. lia. rewrite Int.bits_shru by lia. + replace (i - Int.unsigned n + Int.unsigned n) with i by lia. + rewrite zlt_true by lia. auto. Qed. Lemma iagree_shru: @@ -252,9 +252,9 @@ Proof. intros; red; intros. autorewrite with ints; auto. destruct (zlt (i + Int.unsigned n) Int.zwordsize). - generalize (Int.unsigned_range n); intros. - apply H. omega. rewrite Int.bits_shl by omega. - replace (i + Int.unsigned n - Int.unsigned n) with i by omega. - rewrite zlt_false by omega. auto. + apply H. lia. rewrite Int.bits_shl by lia. + replace (i + Int.unsigned n - Int.unsigned n) with i by lia. + rewrite zlt_false by lia. auto. - auto. Qed. @@ -266,7 +266,7 @@ Proof. intros; red; intros. rewrite <- H in H2. rewrite Int.bits_shru in H2 by auto. rewrite ! Int.bits_shr by auto. destruct (zlt (i + Int.unsigned n) Int.zwordsize). -- apply H0; auto. generalize (Int.unsigned_range n); omega. +- apply H0; auto. generalize (Int.unsigned_range n); lia. - discriminate. Qed. @@ -281,11 +281,11 @@ Proof. then i + Int.unsigned n else Int.zwordsize - 1). assert (0 <= j < Int.zwordsize). - { unfold j; destruct (zlt (i + Int.unsigned n) Int.zwordsize); omega. } + { unfold j; destruct (zlt (i + Int.unsigned n) Int.zwordsize); lia. } apply H; auto. autorewrite with ints; auto. apply orb_true_intro. unfold j; destruct (zlt (i + Int.unsigned n) Int.zwordsize). -- left. rewrite zlt_false by omega. - replace (i + Int.unsigned n - Int.unsigned n) with i by omega. +- left. rewrite zlt_false by lia. + replace (i + Int.unsigned n - Int.unsigned n) with i by lia. auto. - right. reflexivity. Qed. @@ -303,7 +303,7 @@ Proof. mod Int.zwordsize) with i. auto. apply eqmod_small_eq with Int.zwordsize; auto. apply eqmod_trans with ((i - Int.unsigned amount) + Int.unsigned amount). - apply eqmod_refl2; omega. + apply eqmod_refl2; lia. eapply eqmod_trans. 2: apply eqmod_mod; auto. apply eqmod_add. apply eqmod_mod; auto. @@ -330,12 +330,12 @@ Lemma eqmod_iagree: Proof. intros. set (p := Z.to_nat (Int.size m)). generalize (Int.size_range m); intros RANGE. - assert (EQ: Int.size m = Z.of_nat p). { symmetry; apply Z2Nat.id. omega. } + assert (EQ: Int.size m = Z.of_nat p). { symmetry; apply Z2Nat.id. lia. } rewrite EQ in H; rewrite <- two_power_nat_two_p in H. red; intros. rewrite ! Int.testbit_repr by auto. destruct (zlt i (Int.size m)). - eapply same_bits_eqmod; eauto. omega. - assert (Int.testbit m i = false) by (eapply Int.bits_size_2; omega). + eapply same_bits_eqmod; eauto. lia. + assert (Int.testbit m i = false) by (eapply Int.bits_size_2; lia). congruence. Qed. @@ -348,11 +348,11 @@ Lemma iagree_eqmod: Proof. intros. set (p := Z.to_nat (Int.size m)). generalize (Int.size_range m); intros RANGE. - assert (EQ: Int.size m = Z.of_nat p). { symmetry; apply Z2Nat.id. omega. } + assert (EQ: Int.size m = Z.of_nat p). { symmetry; apply Z2Nat.id. lia. } rewrite EQ; rewrite <- two_power_nat_two_p. - apply eqmod_same_bits. intros. apply H. omega. - unfold complete_mask. rewrite Int.bits_zero_ext by omega. - rewrite zlt_true by omega. rewrite Int.bits_mone by omega. auto. + apply eqmod_same_bits. intros. apply H. lia. + unfold complete_mask. rewrite Int.bits_zero_ext by lia. + rewrite zlt_true by lia. rewrite Int.bits_mone by lia. auto. Qed. Lemma complete_mask_idem: @@ -363,12 +363,12 @@ Proof. + assert (Int.unsigned m <> 0). { red; intros; elim n. rewrite <- (Int.repr_unsigned m). rewrite H; auto. } assert (0 < Int.size m). - { apply Zsize_pos'. generalize (Int.unsigned_range m); omega. } + { apply Zsize_pos'. generalize (Int.unsigned_range m); lia. } generalize (Int.size_range m); intros. f_equal. apply Int.bits_size_4. tauto. - rewrite Int.bits_zero_ext by omega. rewrite zlt_true by omega. - apply Int.bits_mone; omega. - intros. rewrite Int.bits_zero_ext by omega. apply zlt_false; omega. + rewrite Int.bits_zero_ext by lia. rewrite zlt_true by lia. + apply Int.bits_mone; lia. + intros. rewrite Int.bits_zero_ext by lia. apply zlt_false; lia. Qed. (** ** Abstract operations over value needs. *) @@ -676,12 +676,12 @@ Proof. destruct x; simpl in *. - auto. - unfold Val.zero_ext; InvAgree. - red; intros. autorewrite with ints; try omega. + red; intros. autorewrite with ints; try lia. destruct (zlt i1 n); auto. apply H; auto. - autorewrite with ints; try omega. rewrite zlt_true; auto. + autorewrite with ints; try lia. rewrite zlt_true; auto. - unfold Val.zero_ext; InvAgree; auto. apply Val.lessdef_same. f_equal. - Int.bit_solve; try omega. destruct (zlt i1 n); auto. apply H; auto. - autorewrite with ints; try omega. apply zlt_true; auto. + Int.bit_solve; try lia. destruct (zlt i1 n); auto. apply H; auto. + autorewrite with ints; try lia. apply zlt_true; auto. Qed. Definition sign_ext (n: Z) (x: nval) := @@ -700,25 +700,25 @@ Proof. unfold sign_ext; intros. destruct x; simpl in *. - auto. - unfold Val.sign_ext; InvAgree. - red; intros. autorewrite with ints; try omega. + red; intros. autorewrite with ints; try lia. set (j := if zlt i1 n then i1 else n - 1). assert (0 <= j < Int.zwordsize). - { unfold j; destruct (zlt i1 n); omega. } + { unfold j; destruct (zlt i1 n); lia. } apply H; auto. - autorewrite with ints; try omega. apply orb_true_intro. + autorewrite with ints; try lia. apply orb_true_intro. unfold j; destruct (zlt i1 n). left. rewrite zlt_true; auto. - right. rewrite Int.unsigned_repr. rewrite zlt_false by omega. - replace (n - 1 - (n - 1)) with 0 by omega. reflexivity. - generalize Int.wordsize_max_unsigned; omega. + right. rewrite Int.unsigned_repr. rewrite zlt_false by lia. + replace (n - 1 - (n - 1)) with 0 by lia. reflexivity. + generalize Int.wordsize_max_unsigned; lia. - unfold Val.sign_ext; InvAgree; auto. apply Val.lessdef_same. f_equal. - Int.bit_solve; try omega. + Int.bit_solve; try lia. set (j := if zlt i1 n then i1 else n - 1). assert (0 <= j < Int.zwordsize). - { unfold j; destruct (zlt i1 n); omega. } - apply H; auto. rewrite Int.bits_zero_ext; try omega. + { unfold j; destruct (zlt i1 n); lia. } + apply H; auto. rewrite Int.bits_zero_ext; try lia. rewrite zlt_true. apply Int.bits_mone; auto. - unfold j. destruct (zlt i1 n); omega. + unfold j. destruct (zlt i1 n); lia. Qed. (** The needs of a memory store concerning the value being stored. *) @@ -778,11 +778,11 @@ Proof. - apply sign_ext_sound with (v := Vint i) (w := Vint i0) (x := All) (n := 8). auto. compute; auto. - apply zero_ext_sound with (v := Vint i) (w := Vint i0) (x := All) (n := 8). - auto. omega. + auto. lia. - apply sign_ext_sound with (v := Vint i) (w := Vint i0) (x := All) (n := 16). auto. compute; auto. - apply zero_ext_sound with (v := Vint i) (w := Vint i0) (x := All) (n := 16). - auto. omega. + auto. lia. Qed. (** The needs of a comparison *) @@ -1014,9 +1014,9 @@ Proof. unfold zero_ext_redundant; intros. destruct x; try discriminate. - auto. - simpl in *; InvAgree. simpl. InvBooleans. rewrite <- H. - red; intros; autorewrite with ints; try omega. + red; intros; autorewrite with ints; try lia. destruct (zlt i1 n). apply H0; auto. - rewrite Int.bits_zero_ext in H3 by omega. rewrite zlt_false in H3 by auto. discriminate. + rewrite Int.bits_zero_ext in H3 by lia. rewrite zlt_false in H3 by auto. discriminate. Qed. Definition sign_ext_redundant (n: Z) (x: nval) := @@ -1036,10 +1036,10 @@ Proof. unfold sign_ext_redundant; intros. destruct x; try discriminate. - auto. - simpl in *; InvAgree. simpl. InvBooleans. rewrite <- H. - red; intros; autorewrite with ints; try omega. + red; intros; autorewrite with ints; try lia. destruct (zlt i1 n). apply H0; auto. rewrite Int.bits_or; auto. rewrite H3; auto. - rewrite Int.bits_zero_ext in H3 by omega. rewrite zlt_false in H3 by auto. discriminate. + rewrite Int.bits_zero_ext in H3 by lia. rewrite zlt_false in H3 by auto. discriminate. Qed. (** * Neededness for register environments *) @@ -1300,13 +1300,13 @@ Proof. split; simpl; auto; intros. rewrite PTree.gsspec in H6. destruct (peq id0 id). + inv H6. destruct H3. congruence. destruct gl!id as [iv0|] eqn:NG. - unfold iv'; rewrite ISet.In_add. intros [P|P]. omega. eelim GL; eauto. - unfold iv'; rewrite ISet.In_interval. omega. + unfold iv'; rewrite ISet.In_add. intros [P|P]. lia. eelim GL; eauto. + unfold iv'; rewrite ISet.In_interval. lia. + eauto. - (* Stk ofs *) split; simpl; auto; intros. destruct H3. elim H3. subst b'. eapply bc_stack; eauto. - rewrite ISet.In_add. intros [P|P]. omega. eapply STK; eauto. + rewrite ISet.In_add. intros [P|P]. lia. eapply STK; eauto. Qed. (** Test (conservatively) whether some locations in the range delimited diff --git a/backend/RTL.v b/backend/RTL.v index 9599a24a..a022f55a 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -352,7 +352,7 @@ Proof. exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. exists (Returnstate s0 vres2 m2). econstructor; eauto. (* trace length *) - red; intros; inv H; simpl; try omega. + red; intros; inv H; simpl; try lia. eapply external_call_trace_length; eauto. eapply external_call_trace_length; eauto. Qed. @@ -450,8 +450,8 @@ Proof. rewrite PTree.gempty. congruence. (* inductive case *) intros. rewrite PTree.gsspec in H2. destruct (peq pc k). - inv H2. xomega. - apply Ple_trans with a. auto. xomega. + inv H2. extlia. + apply Ple_trans with a. auto. extlia. Qed. (** Maximum pseudo-register mentioned in a function. All results or arguments @@ -489,9 +489,9 @@ Proof. assert (X: forall l n, Ple m n -> Ple m (fold_left Pos.max l n)). { induction l; simpl; intros. auto. - apply IHl. xomega. } - destruct i; simpl; try (destruct s0); repeat (apply X); try xomega. - destruct o; xomega. + apply IHl. extlia. } + destruct i; simpl; try (destruct s0); repeat (apply X); try extlia. + destruct o; extlia. Qed. Remark max_reg_instr_def: @@ -499,12 +499,12 @@ Remark max_reg_instr_def: Proof. intros. assert (X: forall l n, Ple r n -> Ple r (fold_left Pos.max l n)). - { induction l; simpl; intros. xomega. apply IHl. xomega. } + { induction l; simpl; intros. extlia. apply IHl. extlia. } destruct i; simpl in *; inv H. -- apply X. xomega. -- apply X. xomega. -- destruct s0; apply X; xomega. -- destruct b; inv H1. apply X. simpl. xomega. +- apply X. extlia. +- apply X. extlia. +- destruct s0; apply X; extlia. +- destruct b; inv H1. apply X. simpl. extlia. Qed. Remark max_reg_instr_uses: @@ -514,14 +514,14 @@ Proof. assert (X: forall l n, In r l \/ Ple r n -> Ple r (fold_left Pos.max l n)). { induction l; simpl; intros. tauto. - apply IHl. destruct H0 as [[A|A]|A]. right; subst; xomega. auto. right; xomega. } + apply IHl. destruct H0 as [[A|A]|A]. right; subst; extlia. auto. right; extlia. } destruct i; simpl in *; try (destruct s0); try (apply X; auto). - contradiction. -- destruct H. right; subst; xomega. auto. -- destruct H. right; subst; xomega. auto. -- destruct H. right; subst; xomega. auto. -- intuition. subst; xomega. -- destruct o; simpl in H; intuition. subst; xomega. +- destruct H. right; subst; extlia. auto. +- destruct H. right; subst; extlia. auto. +- destruct H. right; subst; extlia. auto. +- intuition. subst; extlia. +- destruct o; simpl in H; intuition. subst; extlia. Qed. Lemma max_reg_function_def: @@ -539,7 +539,7 @@ Proof. + inv H3. eapply max_reg_instr_def; eauto. + apply Ple_trans with a. auto. apply max_reg_instr_ge. } - unfold max_reg_function. xomega. + unfold max_reg_function. extlia. Qed. Lemma max_reg_function_use: @@ -557,7 +557,7 @@ Proof. + inv H3. eapply max_reg_instr_uses; eauto. + apply Ple_trans with a. auto. apply max_reg_instr_ge. } - unfold max_reg_function. xomega. + unfold max_reg_function. extlia. Qed. Lemma max_reg_function_params: @@ -567,8 +567,8 @@ Proof. assert (X: forall l n, In r l \/ Ple r n -> Ple r (fold_left Pos.max l n)). { induction l; simpl; intros. tauto. - apply IHl. destruct H0 as [[A|A]|A]. right; subst; xomega. auto. right; xomega. } + apply IHl. destruct H0 as [[A|A]|A]. right; subst; extlia. auto. right; extlia. } assert (Y: Ple r (fold_left Pos.max f.(fn_params) 1%positive)). { apply X; auto. } - unfold max_reg_function. xomega. + unfold max_reg_function. extlia. Qed. diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index b94ec22f..88f7fe53 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -1145,7 +1145,7 @@ Proof. Qed. Ltac Lt_state := - apply lt_state_intro; simpl; try omega. + apply lt_state_intro; simpl; try lia. Lemma lt_state_wf: well_founded lt_state. diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v index c57d3652..9d581ec9 100644 --- a/backend/SelectDivproof.v +++ b/backend/SelectDivproof.v @@ -44,55 +44,55 @@ Proof. set (r := n mod d). intro EUCL. assert (0 <= r <= d - 1). - unfold r. generalize (Z_mod_lt n d d_pos). omega. + unfold r. generalize (Z_mod_lt n d d_pos). lia. assert (0 <= m). apply Zmult_le_0_reg_r with d. auto. - exploit (two_p_gt_ZERO (N + l)). omega. omega. + exploit (two_p_gt_ZERO (N + l)). lia. lia. set (k := m * d - two_p (N + l)). assert (0 <= k <= two_p l). - unfold k; omega. + unfold k; lia. assert ((m * n - two_p (N + l) * q) * d = k * n + two_p (N + l) * r). unfold k. rewrite EUCL. ring. assert (0 <= k * n). - apply Z.mul_nonneg_nonneg; omega. + apply Z.mul_nonneg_nonneg; lia. assert (k * n <= two_p (N + l) - two_p l). apply Z.le_trans with (two_p l * n). - apply Z.mul_le_mono_nonneg_r; omega. - replace (N + l) with (l + N) by omega. + apply Z.mul_le_mono_nonneg_r; lia. + replace (N + l) with (l + N) by lia. rewrite two_p_is_exp. replace (two_p l * two_p N - two_p l) with (two_p l * (two_p N - 1)) by ring. - apply Z.mul_le_mono_nonneg_l. omega. exploit (two_p_gt_ZERO l). omega. omega. - omega. omega. + apply Z.mul_le_mono_nonneg_l. lia. exploit (two_p_gt_ZERO l). lia. lia. + lia. lia. assert (0 <= two_p (N + l) * r). apply Z.mul_nonneg_nonneg. - exploit (two_p_gt_ZERO (N + l)). omega. omega. - omega. + exploit (two_p_gt_ZERO (N + l)). lia. lia. + lia. assert (two_p (N + l) * r <= two_p (N + l) * d - two_p (N + l)). replace (two_p (N + l) * d - two_p (N + l)) with (two_p (N + l) * (d - 1)) by ring. apply Z.mul_le_mono_nonneg_l. - omega. - exploit (two_p_gt_ZERO (N + l)). omega. omega. + lia. + exploit (two_p_gt_ZERO (N + l)). lia. lia. assert (0 <= m * n - two_p (N + l) * q). apply Zmult_le_reg_r with d. auto. - replace (0 * d) with 0 by ring. rewrite H2. omega. + replace (0 * d) with 0 by ring. rewrite H2. lia. assert (m * n - two_p (N + l) * q < two_p (N + l)). - apply Zmult_lt_reg_r with d. omega. + apply Zmult_lt_reg_r with d. lia. rewrite H2. apply Z.le_lt_trans with (two_p (N + l) * d - two_p l). - omega. - exploit (two_p_gt_ZERO l). omega. omega. + lia. + exploit (two_p_gt_ZERO l). lia. lia. symmetry. apply Zdiv_unique with (m * n - two_p (N + l) * q). - ring. omega. + ring. lia. Qed. Lemma Zdiv_unique_2: forall x y q, y > 0 -> 0 < y * q - x <= y -> Z.div x y = q - 1. Proof. intros. apply Zdiv_unique with (x - (q - 1) * y). ring. - replace ((q - 1) * y) with (y * q - y) by ring. omega. + replace ((q - 1) * y) with (y * q - y) by ring. lia. Qed. Lemma Zdiv_mul_opp: @@ -110,42 +110,42 @@ Proof. set (r := n mod d). intro EUCL. assert (0 <= r <= d - 1). - unfold r. generalize (Z_mod_lt n d d_pos). omega. + unfold r. generalize (Z_mod_lt n d d_pos). lia. assert (0 <= m). apply Zmult_le_0_reg_r with d. auto. - exploit (two_p_gt_ZERO (N + l)). omega. omega. + exploit (two_p_gt_ZERO (N + l)). lia. lia. cut (Z.div (- (m * n)) (two_p (N + l)) = -q - 1). - omega. + lia. apply Zdiv_unique_2. - apply two_p_gt_ZERO. omega. + apply two_p_gt_ZERO. lia. replace (two_p (N + l) * - q - - (m * n)) with (m * n - two_p (N + l) * q) by ring. set (k := m * d - two_p (N + l)). assert (0 < k <= two_p l). - unfold k; omega. + unfold k; lia. assert ((m * n - two_p (N + l) * q) * d = k * n + two_p (N + l) * r). unfold k. rewrite EUCL. ring. split. - apply Zmult_lt_reg_r with d. omega. - replace (0 * d) with 0 by omega. + apply Zmult_lt_reg_r with d. lia. + replace (0 * d) with 0 by lia. rewrite H2. - assert (0 < k * n). apply Z.mul_pos_pos; omega. + assert (0 < k * n). apply Z.mul_pos_pos; lia. assert (0 <= two_p (N + l) * r). - apply Z.mul_nonneg_nonneg. exploit (two_p_gt_ZERO (N + l)); omega. omega. - omega. - apply Zmult_le_reg_r with d. omega. + apply Z.mul_nonneg_nonneg. exploit (two_p_gt_ZERO (N + l)); lia. lia. + lia. + apply Zmult_le_reg_r with d. lia. rewrite H2. assert (k * n <= two_p (N + l)). - rewrite Z.add_comm. rewrite two_p_is_exp; try omega. - apply Z.le_trans with (two_p l * n). apply Z.mul_le_mono_nonneg_r; omega. - apply Z.mul_le_mono_nonneg_l. omega. exploit (two_p_gt_ZERO l). omega. omega. + rewrite Z.add_comm. rewrite two_p_is_exp; try lia. + apply Z.le_trans with (two_p l * n). apply Z.mul_le_mono_nonneg_r; lia. + apply Z.mul_le_mono_nonneg_l. lia. exploit (two_p_gt_ZERO l). lia. lia. assert (two_p (N + l) * r <= two_p (N + l) * d - two_p (N + l)). replace (two_p (N + l) * d - two_p (N + l)) with (two_p (N + l) * (d - 1)) by ring. - apply Z.mul_le_mono_nonneg_l. exploit (two_p_gt_ZERO (N + l)). omega. omega. omega. - omega. + apply Z.mul_le_mono_nonneg_l. exploit (two_p_gt_ZERO (N + l)). lia. lia. lia. + lia. Qed. (** This is theorem 5.1 from Granlund and Montgomery, PLDI 1994. *) @@ -159,13 +159,13 @@ Lemma Zquot_mul: Z.quot n d = Z.div (m * n) (two_p (N + l)) + (if zlt n 0 then 1 else 0). Proof. intros. destruct (zlt n 0). - exploit (Zdiv_mul_opp m l H H0 (-n)). omega. + exploit (Zdiv_mul_opp m l H H0 (-n)). lia. replace (- - n) with n by ring. replace (Z.quot n d) with (- Z.quot (-n) d). - rewrite Zquot_Zdiv_pos by omega. omega. - rewrite Z.quot_opp_l by omega. ring. - rewrite Z.add_0_r. rewrite Zquot_Zdiv_pos by omega. - apply Zdiv_mul_pos; omega. + rewrite Zquot_Zdiv_pos by lia. lia. + rewrite Z.quot_opp_l by lia. ring. + rewrite Z.add_0_r. rewrite Zquot_Zdiv_pos by lia. + apply Zdiv_mul_pos; lia. Qed. End Z_DIV_MUL. @@ -194,11 +194,11 @@ Proof with (try discriminate). destruct (zlt p1 32)... intros EQ; inv EQ. split. auto. split. auto. intros. - replace (32 + p') with (31 + (p' + 1)) by omega. - apply Zquot_mul; try omega. - replace (31 + (p' + 1)) with (32 + p') by omega. omega. + replace (32 + p') with (31 + (p' + 1)) by lia. + apply Zquot_mul; try lia. + replace (31 + (p' + 1)) with (32 + p') by lia. lia. change (Int.min_signed <= n < Int.half_modulus). - unfold Int.max_signed in H. omega. + unfold Int.max_signed in H. lia. Qed. Lemma divu_mul_params_sound: @@ -223,7 +223,7 @@ Proof with (try discriminate). destruct (zlt p1 32)... intros EQ; inv EQ. split. auto. split. auto. intros. - apply Zdiv_mul_pos; try omega. assumption. + apply Zdiv_mul_pos; try lia. assumption. Qed. Lemma divs_mul_shift_gen: @@ -237,25 +237,25 @@ Proof. exploit divs_mul_params_sound; eauto. intros (A & B & C). split. auto. split. auto. unfold Int.divs. fold n; fold d. rewrite C by (apply Int.signed_range). - rewrite two_p_is_exp by omega. rewrite <- Zdiv_Zdiv. + rewrite two_p_is_exp by lia. rewrite <- Zdiv_Zdiv. rewrite Int.shru_lt_zero. unfold Int.add. apply Int.eqm_samerepr. apply Int.eqm_add. rewrite Int.shr_div_two_p. apply Int.eqm_unsigned_repr_r. apply Int.eqm_refl2. rewrite Int.unsigned_repr. f_equal. rewrite Int.signed_repr. rewrite Int.modulus_power. f_equal. ring. cut (Int.min_signed <= n * m / Int.modulus < Int.half_modulus). - unfold Int.max_signed; omega. - apply Zdiv_interval_1. generalize Int.min_signed_neg; omega. apply Int.half_modulus_pos. + unfold Int.max_signed; lia. + apply Zdiv_interval_1. generalize Int.min_signed_neg; lia. apply Int.half_modulus_pos. apply Int.modulus_pos. split. apply Z.le_trans with (Int.min_signed * m). - apply Z.mul_le_mono_nonpos_l. generalize Int.min_signed_neg; omega. omega. - apply Z.mul_le_mono_nonneg_r. omega. unfold n; generalize (Int.signed_range x); tauto. + apply Z.mul_le_mono_nonpos_l. generalize Int.min_signed_neg; lia. lia. + apply Z.mul_le_mono_nonneg_r. lia. unfold n; generalize (Int.signed_range x); tauto. apply Z.le_lt_trans with (Int.half_modulus * m). - apply Z.mul_le_mono_nonneg_r. tauto. generalize (Int.signed_range x); unfold n, Int.max_signed; omega. - apply Zmult_lt_compat_l. generalize Int.half_modulus_pos; omega. tauto. - assert (32 < Int.max_unsigned) by (compute; auto). omega. + apply Z.mul_le_mono_nonneg_r. tauto. generalize (Int.signed_range x); unfold n, Int.max_signed; lia. + apply Zmult_lt_compat_l. generalize Int.half_modulus_pos; lia. tauto. + assert (32 < Int.max_unsigned) by (compute; auto). lia. unfold Int.lt; fold n. rewrite Int.signed_zero. destruct (zlt n 0); apply Int.eqm_unsigned_repr. - apply two_p_gt_ZERO. omega. - apply two_p_gt_ZERO. omega. + apply two_p_gt_ZERO. lia. + apply two_p_gt_ZERO. lia. Qed. Theorem divs_mul_shift_1: @@ -269,7 +269,7 @@ Proof. intros. exploit divs_mul_shift_gen; eauto. instantiate (1 := x). intros (A & B & C). split. auto. rewrite C. unfold Int.mulhs. rewrite Int.signed_repr. auto. - generalize Int.min_signed_neg; unfold Int.max_signed; omega. + generalize Int.min_signed_neg; unfold Int.max_signed; lia. Qed. Theorem divs_mul_shift_2: @@ -305,18 +305,18 @@ Proof. split. auto. rewrite Int.shru_div_two_p. rewrite Int.unsigned_repr. unfold Int.divu, Int.mulhu. f_equal. rewrite C by apply Int.unsigned_range. - rewrite two_p_is_exp by omega. rewrite <- Zdiv_Zdiv by (apply two_p_gt_ZERO; omega). + rewrite two_p_is_exp by lia. rewrite <- Zdiv_Zdiv by (apply two_p_gt_ZERO; lia). f_equal. rewrite (Int.unsigned_repr m). rewrite Int.unsigned_repr. f_equal. ring. cut (0 <= Int.unsigned x * m / Int.modulus < Int.modulus). - unfold Int.max_unsigned; omega. - apply Zdiv_interval_1. omega. compute; auto. compute; auto. - split. simpl. apply Z.mul_nonneg_nonneg. generalize (Int.unsigned_range x); omega. omega. + unfold Int.max_unsigned; lia. + apply Zdiv_interval_1. lia. compute; auto. compute; auto. + split. simpl. apply Z.mul_nonneg_nonneg. generalize (Int.unsigned_range x); lia. lia. apply Z.le_lt_trans with (Int.modulus * m). - apply Zmult_le_compat_r. generalize (Int.unsigned_range x); omega. omega. - apply Zmult_lt_compat_l. compute; auto. omega. - unfold Int.max_unsigned; omega. - assert (32 < Int.max_unsigned) by (compute; auto). omega. + apply Zmult_le_compat_r. generalize (Int.unsigned_range x); lia. lia. + apply Zmult_lt_compat_l. compute; auto. lia. + unfold Int.max_unsigned; lia. + assert (32 < Int.max_unsigned) by (compute; auto). lia. Qed. (** Same, for 64-bit integers *) @@ -343,11 +343,11 @@ Proof with (try discriminate). destruct (zlt p1 64)... intros EQ; inv EQ. split. auto. split. auto. intros. - replace (64 + p') with (63 + (p' + 1)) by omega. - apply Zquot_mul; try omega. - replace (63 + (p' + 1)) with (64 + p') by omega. omega. + replace (64 + p') with (63 + (p' + 1)) by lia. + apply Zquot_mul; try lia. + replace (63 + (p' + 1)) with (64 + p') by lia. lia. change (Int64.min_signed <= n < Int64.half_modulus). - unfold Int64.max_signed in H. omega. + unfold Int64.max_signed in H. lia. Qed. Lemma divlu_mul_params_sound: @@ -372,13 +372,13 @@ Proof with (try discriminate). destruct (zlt p1 64)... intros EQ; inv EQ. split. auto. split. auto. intros. - apply Zdiv_mul_pos; try omega. assumption. + apply Zdiv_mul_pos; try lia. assumption. Qed. Remark int64_shr'_div_two_p: forall x y, Int64.shr' x y = Int64.repr (Int64.signed x / two_p (Int.unsigned y)). Proof. - intros; unfold Int64.shr'. rewrite Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); omega. + intros; unfold Int64.shr'. rewrite Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); lia. Qed. Lemma divls_mul_shift_gen: @@ -392,25 +392,25 @@ Proof. exploit divls_mul_params_sound; eauto. intros (A & B & C). split. auto. split. auto. unfold Int64.divs. fold n; fold d. rewrite C by (apply Int64.signed_range). - rewrite two_p_is_exp by omega. rewrite <- Zdiv_Zdiv. + rewrite two_p_is_exp by lia. rewrite <- Zdiv_Zdiv. rewrite Int64.shru_lt_zero. unfold Int64.add. apply Int64.eqm_samerepr. apply Int64.eqm_add. rewrite int64_shr'_div_two_p. apply Int64.eqm_unsigned_repr_r. apply Int64.eqm_refl2. rewrite Int.unsigned_repr. f_equal. rewrite Int64.signed_repr. rewrite Int64.modulus_power. f_equal. ring. cut (Int64.min_signed <= n * m / Int64.modulus < Int64.half_modulus). - unfold Int64.max_signed; omega. - apply Zdiv_interval_1. generalize Int64.min_signed_neg; omega. apply Int64.half_modulus_pos. + unfold Int64.max_signed; lia. + apply Zdiv_interval_1. generalize Int64.min_signed_neg; lia. apply Int64.half_modulus_pos. apply Int64.modulus_pos. split. apply Z.le_trans with (Int64.min_signed * m). - apply Z.mul_le_mono_nonpos_l. generalize Int64.min_signed_neg; omega. omega. + apply Z.mul_le_mono_nonpos_l. generalize Int64.min_signed_neg; lia. lia. apply Z.mul_le_mono_nonneg_r. tauto. unfold n; generalize (Int64.signed_range x); tauto. apply Z.le_lt_trans with (Int64.half_modulus * m). - apply Zmult_le_compat_r. generalize (Int64.signed_range x); unfold n, Int64.max_signed; omega. tauto. - apply Zmult_lt_compat_l. generalize Int64.half_modulus_pos; omega. tauto. - assert (64 < Int.max_unsigned) by (compute; auto). omega. + apply Zmult_le_compat_r. generalize (Int64.signed_range x); unfold n, Int64.max_signed; lia. tauto. + apply Zmult_lt_compat_l. generalize Int64.half_modulus_pos; lia. tauto. + assert (64 < Int.max_unsigned) by (compute; auto). lia. unfold Int64.lt; fold n. rewrite Int64.signed_zero. destruct (zlt n 0); apply Int64.eqm_unsigned_repr. - apply two_p_gt_ZERO. omega. - apply two_p_gt_ZERO. omega. + apply two_p_gt_ZERO. lia. + apply two_p_gt_ZERO. lia. Qed. Theorem divls_mul_shift_1: @@ -424,7 +424,7 @@ Proof. intros. exploit divls_mul_shift_gen; eauto. instantiate (1 := x). intros (A & B & C). split. auto. rewrite C. unfold Int64.mulhs. rewrite Int64.signed_repr. auto. - generalize Int64.min_signed_neg; unfold Int64.max_signed; omega. + generalize Int64.min_signed_neg; unfold Int64.max_signed; lia. Qed. Theorem divls_mul_shift_2: @@ -453,7 +453,7 @@ Qed. Remark int64_shru'_div_two_p: forall x y, Int64.shru' x y = Int64.repr (Int64.unsigned x / two_p (Int.unsigned y)). Proof. - intros; unfold Int64.shru'. rewrite Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); omega. + intros; unfold Int64.shru'. rewrite Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); lia. Qed. Theorem divlu_mul_shift: @@ -466,18 +466,18 @@ Proof. split. auto. rewrite int64_shru'_div_two_p. rewrite Int.unsigned_repr. unfold Int64.divu, Int64.mulhu. f_equal. rewrite C by apply Int64.unsigned_range. - rewrite two_p_is_exp by omega. rewrite <- Zdiv_Zdiv by (apply two_p_gt_ZERO; omega). + rewrite two_p_is_exp by lia. rewrite <- Zdiv_Zdiv by (apply two_p_gt_ZERO; lia). f_equal. rewrite (Int64.unsigned_repr m). rewrite Int64.unsigned_repr. f_equal. ring. cut (0 <= Int64.unsigned x * m / Int64.modulus < Int64.modulus). - unfold Int64.max_unsigned; omega. - apply Zdiv_interval_1. omega. compute; auto. compute; auto. - split. simpl. apply Z.mul_nonneg_nonneg. generalize (Int64.unsigned_range x); omega. omega. + unfold Int64.max_unsigned; lia. + apply Zdiv_interval_1. lia. compute; auto. compute; auto. + split. simpl. apply Z.mul_nonneg_nonneg. generalize (Int64.unsigned_range x); lia. lia. apply Z.le_lt_trans with (Int64.modulus * m). - apply Zmult_le_compat_r. generalize (Int64.unsigned_range x); omega. omega. - apply Zmult_lt_compat_l. compute; auto. omega. - unfold Int64.max_unsigned; omega. - assert (64 < Int.max_unsigned) by (compute; auto). omega. + apply Zmult_le_compat_r. generalize (Int64.unsigned_range x); lia. lia. + apply Zmult_lt_compat_l. compute; auto. lia. + unfold Int64.max_unsigned; lia. + assert (64 < Int.max_unsigned) by (compute; auto). lia. Qed. (** * Correctness of the smart constructors for division and modulus *) @@ -515,7 +515,7 @@ Proof. replace (Int.ltu (Int.repr p) Int.iwordsize) with true in Q. inv Q. rewrite B. auto. unfold Int.ltu. rewrite Int.unsigned_repr. rewrite zlt_true; auto. tauto. - assert (32 < Int.max_unsigned) by (compute; auto). omega. + assert (32 < Int.max_unsigned) by (compute; auto). lia. Qed. Theorem eval_divuimm: @@ -630,7 +630,7 @@ Proof. simpl in LD. inv LD. assert (RANGE: 0 <= p < 32 -> Int.ltu (Int.repr p) Int.iwordsize = true). { intros. unfold Int.ltu. rewrite Int.unsigned_repr. rewrite zlt_true by tauto. auto. - assert (32 < Int.max_unsigned) by (compute; auto). omega. } + assert (32 < Int.max_unsigned) by (compute; auto). lia. } destruct (zlt M Int.half_modulus). - exploit (divs_mul_shift_1 x); eauto. intros [A B]. exploit eval_shrimm. eexact X. instantiate (1 := Int.repr p). intros [v1 [Z LD]]. @@ -768,7 +768,7 @@ Proof. simpl in B1; inv B1. simpl in B2. replace (Int.ltu (Int.repr p) Int64.iwordsize') with true in B2. inv B2. rewrite B. assumption. unfold Int.ltu. rewrite Int.unsigned_repr. rewrite zlt_true; auto. tauto. - assert (64 < Int.max_unsigned) by (compute; auto). omega. + assert (64 < Int.max_unsigned) by (compute; auto). lia. Qed. Theorem eval_divlu: @@ -847,10 +847,10 @@ Proof. exploit eval_addl. auto. eexact A5. eexact A3. intros (v6 & A6 & B6). assert (RANGE: forall x, 0 <= x < 64 -> Int.ltu (Int.repr x) Int64.iwordsize' = true). { intros. unfold Int.ltu. rewrite Int.unsigned_repr. rewrite zlt_true by tauto. auto. - assert (64 < Int.max_unsigned) by (compute; auto). omega. } + assert (64 < Int.max_unsigned) by (compute; auto). lia. } simpl in B1; inv B1. simpl in B2; inv B2. - simpl in B3; rewrite RANGE in B3 by omega; inv B3. + simpl in B3; rewrite RANGE in B3 by lia; inv B3. destruct (zlt M Int64.half_modulus). - exploit (divls_mul_shift_1 x); eauto. intros [A B]. simpl in B5; rewrite RANGE in B5 by auto; inv B5. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 987926aa..4755ab79 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -531,7 +531,7 @@ Lemma sel_switch_correct: (XElet arg (sel_switch make_cmp_eq make_cmp_ltu make_sub make_to_int O t)) (switch_target i dfl cases). Proof. - intros. exploit validate_switch_correct; eauto. omega. intros [A B]. + intros. exploit validate_switch_correct; eauto. lia. intros [A B]. econstructor. eauto. eapply sel_switch_correct_rec; eauto. Qed. @@ -564,7 +564,7 @@ Proof. inv R. unfold Val.cmp in B. simpl in B. revert B. predSpec Int.eq Int.eq_spec n0 (Int.repr n); intros B; inv B. rewrite Int.unsigned_repr. unfold proj_sumbool; rewrite zeq_true; auto. - unfold Int.max_unsigned; omega. + unfold Int.max_unsigned; lia. unfold proj_sumbool; rewrite zeq_false; auto. red; intros; elim H1. rewrite <- (Int.repr_unsigned n0). congruence. - intros until n; intros EVAL R RANGE. @@ -573,7 +573,7 @@ Proof. inv R. unfold Val.cmpu in B. simpl in B. unfold Int.ltu in B. rewrite Int.unsigned_repr in B. destruct (zlt (Int.unsigned n0) n); inv B; auto. - unfold Int.max_unsigned; omega. + unfold Int.max_unsigned; lia. - intros until n; intros EVAL R RANGE. exploit eval_sub. eexact EVAL. apply (INTCONST (Int.repr n)). intros (vb & A & B). inv R. simpl in B. inv B. econstructor; split; eauto. @@ -581,7 +581,7 @@ Proof. with (Int.unsigned (Int.sub n0 (Int.repr n))). constructor. unfold Int.sub. rewrite Int.unsigned_repr_eq. f_equal. f_equal. - apply Int.unsigned_repr. unfold Int.max_unsigned; omega. + apply Int.unsigned_repr. unfold Int.max_unsigned; lia. - intros until i0; intros EVAL R. exists v; split; auto. inv R. rewrite Z.mod_small by (apply Int.unsigned_range). constructor. - constructor. @@ -599,12 +599,12 @@ Proof. eapply eval_cmpl. eexact EVAL. apply eval_longconst with (n := Int64.repr n). inv R. unfold Val.cmpl. simpl. f_equal; f_equal. unfold Int64.eq. rewrite Int64.unsigned_repr. destruct (zeq (Int64.unsigned n0) n); auto. - unfold Int64.max_unsigned; omega. + unfold Int64.max_unsigned; lia. - intros until n; intros EVAL R RANGE. eapply eval_cmplu; auto. eexact EVAL. apply eval_longconst with (n := Int64.repr n). inv R. unfold Val.cmplu. simpl. f_equal; f_equal. unfold Int64.ltu. rewrite Int64.unsigned_repr. destruct (zlt (Int64.unsigned n0) n); auto. - unfold Int64.max_unsigned; omega. + unfold Int64.max_unsigned; lia. - intros until n; intros EVAL R RANGE. exploit eval_subl; auto; try apply HF'. eexact EVAL. apply eval_longconst with (n := Int64.repr n). intros (vb & A & B). @@ -613,7 +613,7 @@ Proof. with (Int64.unsigned (Int64.sub n0 (Int64.repr n))). constructor. unfold Int64.sub. rewrite Int64.unsigned_repr_eq. f_equal. f_equal. - apply Int64.unsigned_repr. unfold Int64.max_unsigned; omega. + apply Int64.unsigned_repr. unfold Int64.max_unsigned; lia. - intros until i0; intros EVAL R. exploit eval_lowlong. eexact EVAL. intros (vb & A & B). inv R. simpl in B. inv B. econstructor; split; eauto. @@ -1295,7 +1295,7 @@ Proof. eapply match_cont_call with (cunit := cunit) (hf := hf); eauto. + (* turned into Sbuiltin *) intros EQ. subst fd. - right; left; split. simpl; omega. split; auto. econstructor; eauto. + right; left; split. simpl; lia. split; auto. econstructor; eauto. - (* Stailcall *) exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]]. erewrite <- stackspace_function_translated in P by eauto. @@ -1413,7 +1413,7 @@ Proof. apply plus_one; econstructor. econstructor; eauto. destruct optid; simpl; auto. apply set_var_lessdef; auto. - (* return of an external call turned into a Sbuiltin *) - right; left; split. simpl; omega. split. auto. econstructor; eauto. + right; left; split. simpl; lia. split. auto. econstructor; eauto. Qed. Lemma sel_initial_states: diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v index 18c1f18d..1e50b1c2 100644 --- a/backend/SplitLongproof.v +++ b/backend/SplitLongproof.v @@ -335,7 +335,7 @@ Proof. fold (Int.testbit i i0). destruct (zlt i0 Int.zwordsize). auto. - rewrite Int.bits_zero. rewrite Int.bits_above by omega. auto. + rewrite Int.bits_zero. rewrite Int.bits_above by lia. auto. Qed. Theorem eval_longofint: unary_constructor_sound longofint Val.longofint. @@ -352,13 +352,13 @@ Proof. apply Int64.same_bits_eq; intros. rewrite Int64.testbit_repr by auto. rewrite Int64.bits_ofwords by auto. - rewrite Int.bits_signed by omega. + rewrite Int.bits_signed by lia. destruct (zlt i0 Int.zwordsize). auto. assert (Int64.zwordsize = 2 * Int.zwordsize) by reflexivity. - rewrite Int.bits_shr by omega. + rewrite Int.bits_shr by lia. change (Int.unsigned (Int.repr 31)) with (Int.zwordsize - 1). - f_equal. destruct (zlt (i0 - Int.zwordsize + (Int.zwordsize - 1)) Int.zwordsize); omega. + f_equal. destruct (zlt (i0 - Int.zwordsize + (Int.zwordsize - 1)) Int.zwordsize); lia. Qed. Theorem eval_negl: unary_constructor_sound negl Val.negl. @@ -545,24 +545,24 @@ Proof. { red; intros. elim H. rewrite <- (Int.repr_unsigned n). rewrite H0. auto. } destruct (Int.ltu n Int.iwordsize) eqn:LT. exploit Int.ltu_iwordsize_inv; eauto. intros RANGE. - assert (0 <= Int.zwordsize - Int.unsigned n < Int.zwordsize) by omega. + assert (0 <= Int.zwordsize - Int.unsigned n < Int.zwordsize) by lia. apply A1. auto. auto. unfold Int.ltu, Int.sub. rewrite Int.unsigned_repr_wordsize. - rewrite Int.unsigned_repr. rewrite zlt_true; auto. omega. - generalize Int.wordsize_max_unsigned; omega. + rewrite Int.unsigned_repr. rewrite zlt_true; auto. lia. + generalize Int.wordsize_max_unsigned; lia. unfold Int.ltu. rewrite zlt_true; auto. change (Int.unsigned Int64.iwordsize') with 64. - change Int.zwordsize with 32 in RANGE. omega. + change Int.zwordsize with 32 in RANGE. lia. destruct (Int.ltu n Int64.iwordsize') eqn:LT'. exploit Int.ltu_inv; eauto. change (Int.unsigned Int64.iwordsize') with (Int.zwordsize * 2). intros RANGE. assert (Int.zwordsize <= Int.unsigned n). unfold Int.ltu in LT. rewrite Int.unsigned_repr_wordsize in LT. - destruct (zlt (Int.unsigned n) Int.zwordsize). discriminate. omega. + destruct (zlt (Int.unsigned n) Int.zwordsize). discriminate. lia. apply A2. tauto. unfold Int.ltu, Int.sub. rewrite Int.unsigned_repr_wordsize. - rewrite Int.unsigned_repr. rewrite zlt_true; auto. omega. - generalize Int.wordsize_max_unsigned; omega. + rewrite Int.unsigned_repr. rewrite zlt_true; auto. lia. + generalize Int.wordsize_max_unsigned; lia. auto. Qed. @@ -918,19 +918,19 @@ Proof. rewrite Int.bits_zero. rewrite Int.bits_or by auto. symmetry. apply orb_false_intro. transitivity (Int64.testbit (Int64.ofwords h l) (i + Int.zwordsize)). - rewrite Int64.bits_ofwords by omega. rewrite zlt_false by omega. f_equal; omega. + rewrite Int64.bits_ofwords by lia. rewrite zlt_false by lia. f_equal; lia. rewrite H0. apply Int64.bits_zero. transitivity (Int64.testbit (Int64.ofwords h l) i). - rewrite Int64.bits_ofwords by omega. rewrite zlt_true by omega. auto. + rewrite Int64.bits_ofwords by lia. rewrite zlt_true by lia. auto. rewrite H0. apply Int64.bits_zero. symmetry. apply Int.eq_false. red; intros; elim H0. apply Int64.same_bits_eq; intros. rewrite Int64.bits_zero. rewrite Int64.bits_ofwords by auto. destruct (zlt i Int.zwordsize). assert (Int.testbit (Int.or h l) i = false) by (rewrite H1; apply Int.bits_zero). - rewrite Int.bits_or in H3 by omega. exploit orb_false_elim; eauto. tauto. + rewrite Int.bits_or in H3 by lia. exploit orb_false_elim; eauto. tauto. assert (Int.testbit (Int.or h l) (i - Int.zwordsize) = false) by (rewrite H1; apply Int.bits_zero). - rewrite Int.bits_or in H3 by omega. exploit orb_false_elim; eauto. tauto. + rewrite Int.bits_or in H3 by lia. exploit orb_false_elim; eauto. tauto. Qed. Lemma eval_cmpl_eq_zero: diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index ffd9b227..7724c5d6 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -58,7 +58,7 @@ Lemma slot_outgoing_argument_valid: Proof. intros. exploit loc_arguments_acceptable_2; eauto. intros [A B]. unfold slot_valid. unfold proj_sumbool. - rewrite zle_true by omega. + rewrite zle_true by lia. rewrite pred_dec_true by auto. auto. Qed. @@ -126,7 +126,7 @@ Proof. destruct (wt_function f); simpl negb. destruct (zlt Ptrofs.max_unsigned (fe_size (make_env (function_bounds f)))). intros; discriminate. - intros. unfold fe. unfold b. omega. + intros. unfold fe. unfold b. lia. intros; discriminate. Qed. @@ -200,7 +200,7 @@ Next Obligation. - exploit H4; eauto. intros (v & A & B). exists v; split; auto. eapply Mem.load_unchanged_on; eauto. simpl; intros. rewrite size_type_chunk, typesize_typesize in H8. - split; auto. omega. + split; auto. lia. Qed. Next Obligation. eauto with mem. @@ -215,7 +215,7 @@ Remark valid_access_location: Proof. intros; split. - red; intros. apply Mem.perm_implies with Freeable; auto with mem. - apply H0. rewrite size_type_chunk, typesize_typesize in H4. omega. + apply H0. rewrite size_type_chunk, typesize_typesize in H4. lia. - rewrite align_type_chunk. apply Z.divide_add_r. apply Z.divide_trans with 8; auto. exists (8 / (4 * typealign ty)); destruct ty; reflexivity. @@ -233,7 +233,7 @@ Proof. intros. destruct H as (D & E & F & G & H). exploit H; eauto. intros (v & U & V). exists v; split; auto. unfold load_stack; simpl. rewrite Ptrofs.add_zero_l, Ptrofs.unsigned_repr; auto. - unfold Ptrofs.max_unsigned. generalize (typesize_pos ty). omega. + unfold Ptrofs.max_unsigned. generalize (typesize_pos ty). lia. Qed. Lemma set_location: @@ -252,19 +252,19 @@ Proof. { red; intros; eauto with mem. } exists m'; split. - unfold store_stack; simpl. rewrite Ptrofs.add_zero_l, Ptrofs.unsigned_repr; eauto. - unfold Ptrofs.max_unsigned. generalize (typesize_pos ty). omega. + unfold Ptrofs.max_unsigned. generalize (typesize_pos ty). lia. - simpl. intuition auto. + unfold Locmap.set. destruct (Loc.eq (S sl ofs ty) (S sl ofs0 ty0)); [|destruct (Loc.diff_dec (S sl ofs ty) (S sl ofs0 ty0))]. * (* same location *) inv e. rename ofs0 into ofs. rename ty0 into ty. exists (Val.load_result (chunk_of_type ty) v'); split. - eapply Mem.load_store_similar_2; eauto. omega. + eapply Mem.load_store_similar_2; eauto. lia. apply Val.load_result_inject; auto. * (* different locations *) exploit H; eauto. intros (v0 & X & Y). exists v0; split; auto. rewrite <- X; eapply Mem.load_store_other; eauto. - destruct d. congruence. right. rewrite ! size_type_chunk, ! typesize_typesize. omega. + destruct d. congruence. right. rewrite ! size_type_chunk, ! typesize_typesize. lia. * (* overlapping locations *) destruct (Mem.valid_access_load m' (chunk_of_type ty0) sp (pos + 4 * ofs0)) as [v'' LOAD]. apply Mem.valid_access_implies with Writable; auto with mem. @@ -273,7 +273,7 @@ Proof. + apply (m_invar P) with m; auto. eapply Mem.store_unchanged_on; eauto. intros i; rewrite size_type_chunk, typesize_typesize. intros; red; intros. - eelim C; eauto. simpl. split; auto. omega. + eelim C; eauto. simpl. split; auto. lia. Qed. Lemma initial_locations: @@ -933,8 +933,8 @@ Local Opaque mreg_type. { unfold pos1. apply Z.divide_trans with sz. unfold sz; rewrite <- size_type_chunk. apply align_size_chunk_divides. apply align_divides; auto. } - apply range_drop_left with (mid := pos1) in SEP; [ | omega ]. - apply range_split with (mid := pos1 + sz) in SEP; [ | omega ]. + apply range_drop_left with (mid := pos1) in SEP; [ | lia ]. + apply range_split with (mid := pos1 + sz) in SEP; [ | lia ]. unfold sz at 1 in SEP. rewrite <- size_type_chunk in SEP. apply range_contains in SEP; auto. exploit (contains_set_stack (fun v' => Val.inject j (ls (R r)) v') (rs r)). @@ -1073,7 +1073,7 @@ Local Opaque b fe. instantiate (1 := fe_stack_data fe). tauto. reflexivity. instantiate (1 := fe_stack_data fe + bound_stack_data b). rewrite Z.max_comm. reflexivity. - generalize (bound_stack_data_pos b) size_no_overflow; omega. + generalize (bound_stack_data_pos b) size_no_overflow; lia. tauto. tauto. clear SEP. intros (j' & SEP & INCR & SAME). @@ -1607,7 +1607,7 @@ Proof. + simpl in SEP. unfold parent_sp. assert (slot_valid f Outgoing pos ty = true). { destruct H0. unfold slot_valid, proj_sumbool. - rewrite zle_true by omega. rewrite pred_dec_true by auto. reflexivity. } + rewrite zle_true by lia. rewrite pred_dec_true by auto. reflexivity. } assert (slot_within_bounds (function_bounds f) Outgoing pos ty) by eauto. exploit frame_get_outgoing; eauto. intros (v & A & B). exists v; split. diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index 9ec89553..7a5be5ed 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -47,11 +47,11 @@ Proof. intro f. assert (forall n pc, (return_measure_rec n f pc <= n)%nat). induction n; intros; simpl. - omega. - destruct (f!pc); try omega. - destruct i; try omega. - generalize (IHn n0). omega. - generalize (IHn n0). omega. + lia. + destruct (f!pc); try lia. + destruct i; try lia. + generalize (IHn n0). lia. + generalize (IHn n0). lia. intros. unfold return_measure. apply H. Qed. @@ -61,11 +61,11 @@ Remark return_measure_rec_incr: (return_measure_rec n1 f pc <= return_measure_rec n2 f pc)%nat. Proof. induction n1; intros; simpl. - omega. - destruct n2. omegaContradiction. assert (n1 <= n2)%nat by omega. - simpl. destruct f!pc; try omega. destruct i; try omega. - generalize (IHn1 n2 n H0). omega. - generalize (IHn1 n2 n H0). omega. + lia. + destruct n2. extlia. assert (n1 <= n2)%nat by lia. + simpl. destruct f!pc; try lia. destruct i; try lia. + generalize (IHn1 n2 n H0). lia. + generalize (IHn1 n2 n H0). lia. Qed. Lemma is_return_measure_rec: @@ -75,13 +75,13 @@ Lemma is_return_measure_rec: Proof. induction n; simpl; intros. congruence. - destruct n'. omegaContradiction. simpl. + destruct n'. extlia. simpl. destruct (fn_code f)!pc; try congruence. destruct i; try congruence. - decEq. apply IHn with r. auto. omega. + decEq. apply IHn with r. auto. lia. destruct (is_move_operation o l); try congruence. destruct (Reg.eq r r1); try congruence. - decEq. apply IHn with r0. auto. omega. + decEq. apply IHn with r0. auto. lia. Qed. (** ** Relational characterization of the code transformation *) @@ -117,22 +117,22 @@ Proof. generalize H. simpl. caseEq ((fn_code f)!pc); try congruence. intro i. caseEq i; try congruence. - intros s; intros. eapply is_return_nop; eauto. eapply IHn; eauto. omega. + intros s; intros. eapply is_return_nop; eauto. eapply IHn; eauto. lia. unfold return_measure. rewrite <- (is_return_measure_rec f (S n) niter pc rret); auto. rewrite <- (is_return_measure_rec f n niter s rret); auto. - simpl. rewrite H2. omega. omega. + simpl. rewrite H2. lia. lia. intros op args dst s EQ1 EQ2. caseEq (is_move_operation op args); try congruence. intros src IMO. destruct (Reg.eq rret src); try congruence. subst rret. intro. exploit is_move_operation_correct; eauto. intros [A B]. subst. - eapply is_return_move; eauto. eapply IHn; eauto. omega. + eapply is_return_move; eauto. eapply IHn; eauto. lia. unfold return_measure. rewrite <- (is_return_measure_rec f (S n) niter pc src); auto. rewrite <- (is_return_measure_rec f n niter s dst); auto. - simpl. rewrite EQ2. omega. omega. + simpl. rewrite EQ2. lia. lia. intros or EQ1 EQ2. destruct or; intros. assert (r = rret). eapply proj_sumbool_true; eauto. subst r. @@ -407,7 +407,7 @@ Proof. eapply exec_Inop; eauto. constructor; auto. - (* eliminated nop *) assert (s0 = pc') by congruence. subst s0. - right. split. simpl. omega. split. auto. + right. split. simpl. lia. split. auto. econstructor; eauto. - (* op *) @@ -421,7 +421,7 @@ Proof. econstructor; eauto. apply set_reg_lessdef; auto. - (* eliminated move *) rewrite H1 in H. clear H1. inv H. - right. split. simpl. omega. split. auto. + right. split. simpl. lia. split. auto. econstructor; eauto. simpl in H0. rewrite PMap.gss. congruence. - (* load *) @@ -455,13 +455,13 @@ Proof. + (* call turned tailcall *) assert ({ m'' | Mem.free m' sp0 0 (fn_stacksize (transf_function f)) = Some m''}). apply Mem.range_perm_free. rewrite stacksize_preserved. rewrite H7. - red; intros; omegaContradiction. + red; intros; extlia. destruct X as [m'' FREE]. left. exists (Callstate s' (transf_fundef fd) (rs'##args) m''); split. eapply exec_Itailcall; eauto. apply sig_preserved. constructor. eapply match_stackframes_tail; eauto. apply regs_lessdef_regs; auto. eapply Mem.free_right_extends; eauto. - rewrite stacksize_preserved. rewrite H7. intros. omegaContradiction. + rewrite stacksize_preserved. rewrite H7. intros. extlia. + (* call that remains a call *) left. exists (Callstate (Stackframe res (transf_function f) (Vptr sp0 Ptrofs.zero) pc' rs' :: s') (transf_fundef fd) (rs'##args) m'); split. @@ -514,22 +514,22 @@ Proof. - (* eliminated return None *) assert (or = None) by congruence. subst or. - right. split. simpl. omega. split. auto. + right. split. simpl. lia. split. auto. constructor. auto. simpl. constructor. eapply Mem.free_left_extends; eauto. - (* eliminated return Some *) assert (or = Some r) by congruence. subst or. - right. split. simpl. omega. split. auto. + right. split. simpl. lia. split. auto. constructor. auto. simpl. auto. eapply Mem.free_left_extends; eauto. - (* internal call *) exploit Mem.alloc_extends; eauto. - instantiate (1 := 0). omega. - instantiate (1 := fn_stacksize f). omega. + instantiate (1 := 0). lia. + instantiate (1 := fn_stacksize f). lia. intros [m'1 [ALLOC EXT]]. assert (fn_stacksize (transf_function f) = fn_stacksize f /\ fn_entrypoint (transf_function f) = fn_entrypoint f /\ @@ -559,7 +559,7 @@ Proof. right. split. unfold measure. simpl length. change (S (length s) * (niter + 2))%nat with ((niter + 2) + (length s) * (niter + 2))%nat. - generalize (return_measure_bounds (fn_code f) pc). omega. + generalize (return_measure_bounds (fn_code f) pc). lia. split. auto. econstructor; eauto. rewrite Regmap.gss. auto. diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index 4f95ac9b..c612995b 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -87,7 +87,7 @@ Proof. * (* The new instruction *) rewrite (U.repr_union_2 u pc s); auto. rewrite U.repr_union_3. unfold measure_edge. destruct (peq (U.repr u s) pc). auto. right. split. auto. - rewrite PC. rewrite peq_true. omega. + rewrite PC. rewrite peq_true. lia. * (* An old instruction *) assert (U.repr u pc' = pc' -> U.repr (U.union u pc s) pc' = pc'). @@ -96,7 +96,7 @@ Proof. intros [P | [P Q]]. left; auto. right. split. apply U.sameclass_union_2. auto. unfold measure_edge. destruct (peq (U.repr u s) pc). auto. - rewrite P. destruct (peq (U.repr u s0) pc). omega. auto. + rewrite P. destruct (peq (U.repr u s0) pc). lia. auto. Qed. Definition record_gotos' (f: function) := @@ -420,7 +420,7 @@ Proof. generalize (record_gotos_correct f pc). rewrite H. destruct bb; auto. destruct i; auto. intros [A | [B C]]. auto. - right. split. simpl. omega. + right. split. simpl. lia. split. auto. rewrite B. econstructor; eauto. @@ -487,7 +487,7 @@ Proof. eapply exec_Lbranch; eauto. fold (branch_target f pc). econstructor; eauto. - (* Lbranch (eliminated) *) - right; split. simpl. omega. split. auto. constructor; auto. + right; split. simpl. lia. split. auto. constructor; auto. - (* Lcond *) simpl tunneled_block. diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v index 680daba7..3216ec50 100644 --- a/backend/Unusedglobproof.v +++ b/backend/Unusedglobproof.v @@ -982,7 +982,7 @@ Proof. intros. exploit G; eauto. intros [U V]. assert (Mem.valid_block m sp0) by (eapply Mem.valid_block_inject_1; eauto). assert (Mem.valid_block tm tsp) by (eapply Mem.valid_block_inject_2; eauto). - unfold Mem.valid_block in *; xomega. + unfold Mem.valid_block in *; extlia. apply set_res_inject; auto. apply regset_inject_incr with j; auto. - (* cond *) @@ -1036,7 +1036,7 @@ Proof. apply match_stacks_bound with (Mem.nextblock m) (Mem.nextblock tm). apply match_stacks_incr with j; auto. intros. exploit G; eauto. intros [P Q]. - unfold Mem.valid_block in *; xomega. + unfold Mem.valid_block in *; extlia. eapply external_call_nextblock; eauto. eapply external_call_nextblock; eauto. @@ -1063,7 +1063,7 @@ Proof. - apply IHl. unfold Genv.add_global, P; simpl. intros LT. apply Plt_succ_inv in LT. destruct LT. + rewrite PTree.gso. apply H; auto. apply Plt_ne; auto. + rewrite H0. rewrite PTree.gss. exists g1; auto. } - apply H. red; simpl; intros. exfalso; xomega. + apply H. red; simpl; intros. exfalso; extlia. Qed. *) @@ -1123,10 +1123,10 @@ Lemma Mem_getN_forall2: P (ZMap.get i c1) (ZMap.get i c2). Proof. induction n; simpl Mem.getN; intros. -- simpl in H1. omegaContradiction. +- simpl in H1. extlia. - inv H. rewrite Nat2Z.inj_succ in H1. destruct (zeq i p0). + congruence. -+ apply IHn with (p0 + 1); auto. omega. omega. ++ apply IHn with (p0 + 1); auto. lia. lia. Qed. Lemma init_mem_inj_1: @@ -1143,7 +1143,7 @@ Proof. + intros (P2 & Q2 & R2 & S2) (P1 & Q1 & R1 & S1). apply Q1 in H0. destruct H0. subst. apply Mem.perm_cur. eapply Mem.perm_implies; eauto. - apply P2. omega. + apply P2. lia. - exploit init_meminj_invert; eauto. intros (A & id & B & C). subst delta. apply Z.divide_0_r. - exploit init_meminj_invert_strong; eauto. intros (A & id & gd & B & C & D & E & F). @@ -1162,8 +1162,8 @@ Local Transparent Mem.loadbytes. rewrite Z.add_0_r. apply Mem_getN_forall2 with (p := 0) (n := Z.to_nat (init_data_list_size (gvar_init v))). rewrite H3, H4. apply bytes_of_init_inject. auto. - omega. - rewrite Z2Nat.id by (apply Z.ge_le; apply init_data_list_size_pos). omega. + lia. + rewrite Z2Nat.id by (apply Z.ge_le; apply init_data_list_size_pos). lia. Qed. Lemma init_mem_inj_2: @@ -1181,18 +1181,18 @@ Proof. exploit init_meminj_invert. eexact H1. intros (A2 & id2 & B2 & C2). destruct (ident_eq id1 id2). congruence. left; eapply Genv.global_addresses_distinct; eauto. - exploit init_meminj_invert; eauto. intros (A & id & B & C). subst delta. - split. omega. generalize (Ptrofs.unsigned_range_2 ofs). omega. + split. lia. generalize (Ptrofs.unsigned_range_2 ofs). lia. - exploit init_meminj_invert_strong; eauto. intros (A & id & gd & B & C & D & E & F). exploit (Genv.init_mem_characterization_gen p); eauto. exploit (Genv.init_mem_characterization_gen tp); eauto. destruct gd as [f|v]. + intros (P2 & Q2) (P1 & Q1). - apply Q2 in H0. destruct H0. subst. replace ofs with 0 by omega. + apply Q2 in H0. destruct H0. subst. replace ofs with 0 by lia. left; apply Mem.perm_cur; auto. + intros (P2 & Q2 & R2 & S2) (P1 & Q1 & R1 & S1). apply Q2 in H0. destruct H0. subst. left. apply Mem.perm_cur. eapply Mem.perm_implies; eauto. - apply P1. omega. + apply P1. lia. Qed. End INIT_MEM. diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index b0ce019c..f7e4f0ed 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -544,8 +544,8 @@ Proof. eapply SM; auto. eapply mmatch_top; eauto. + (* below *) red; simpl; intros. rewrite NB. destruct (eq_block b sp). - subst b; rewrite SP; xomega. - exploit mmatch_below; eauto. xomega. + subst b; rewrite SP; extlia. + exploit mmatch_below; eauto. extlia. - (* unchanged *) simpl; intros. apply dec_eq_false. apply Plt_ne. auto. - (* values *) @@ -1147,11 +1147,11 @@ Proof. - constructor. - assert (Plt sp bound') by eauto with va. eapply sound_stack_public_call; eauto. apply IHsound_stack; intros. - apply INV. xomega. rewrite SAME; auto with ordered_type. xomega. auto. auto. + apply INV. extlia. rewrite SAME; auto with ordered_type. extlia. auto. auto. - assert (Plt sp bound') by eauto with va. eapply sound_stack_private_call; eauto. apply IHsound_stack; intros. - apply INV. xomega. rewrite SAME; auto with ordered_type. xomega. auto. auto. - apply bmatch_ext with m; auto. intros. apply INV. xomega. auto. auto. auto. + apply INV. extlia. rewrite SAME; auto with ordered_type. extlia. auto. auto. + apply bmatch_ext with m; auto. intros. apply INV. extlia. auto. auto. auto. Qed. Lemma sound_stack_inv: @@ -1210,8 +1210,8 @@ Lemma sound_stack_new_bound: Proof. intros. inv H. - constructor. -- eapply sound_stack_public_call with (bound' := bound'0); eauto. xomega. -- eapply sound_stack_private_call with (bound' := bound'0); eauto. xomega. +- eapply sound_stack_public_call with (bound' := bound'0); eauto. extlia. +- eapply sound_stack_private_call with (bound' := bound'0); eauto. extlia. Qed. Lemma sound_stack_exten: @@ -1224,12 +1224,12 @@ Proof. - constructor. - assert (Plt sp bound') by eauto with va. eapply sound_stack_public_call; eauto. - rewrite H0; auto. xomega. - intros. rewrite H0; auto. xomega. + rewrite H0; auto. extlia. + intros. rewrite H0; auto. extlia. - assert (Plt sp bound') by eauto with va. eapply sound_stack_private_call; eauto. - rewrite H0; auto. xomega. - intros. rewrite H0; auto. xomega. + rewrite H0; auto. extlia. + intros. rewrite H0; auto. extlia. Qed. (** ** Preservation of the semantic invariant by one step of execution *) diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index c132ce7c..45894bfc 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -45,10 +45,10 @@ Qed. Hint Extern 2 (_ = _) => congruence : va. Hint Extern 2 (_ <> _) => congruence : va. -Hint Extern 2 (_ < _) => xomega : va. -Hint Extern 2 (_ <= _) => xomega : va. -Hint Extern 2 (_ > _) => xomega : va. -Hint Extern 2 (_ >= _) => xomega : va. +Hint Extern 2 (_ < _) => extlia : va. +Hint Extern 2 (_ <= _) => extlia : va. +Hint Extern 2 (_ > _) => extlia : va. +Hint Extern 2 (_ >= _) => extlia : va. Section MATCH. @@ -595,17 +595,17 @@ Hint Extern 1 (vmatch _ _) => constructor : va. Lemma is_uns_mon: forall n1 n2 i, is_uns n1 i -> n1 <= n2 -> is_uns n2 i. Proof. - intros; red; intros. apply H; omega. + intros; red; intros. apply H; lia. Qed. Lemma is_sgn_mon: forall n1 n2 i, is_sgn n1 i -> n1 <= n2 -> is_sgn n2 i. Proof. - intros; red; intros. apply H; omega. + intros; red; intros. apply H; lia. Qed. Lemma is_uns_sgn: forall n1 n2 i, is_uns n1 i -> n1 < n2 -> is_sgn n2 i. Proof. - intros; red; intros. rewrite ! H by omega. auto. + intros; red; intros. rewrite ! H by lia. auto. Qed. Definition usize := Int.size. @@ -616,7 +616,7 @@ Lemma is_uns_usize: forall i, is_uns (usize i) i. Proof. unfold usize; intros; red; intros. - apply Int.bits_size_2. omega. + apply Int.bits_size_2. lia. Qed. Lemma is_sgn_ssize: @@ -628,10 +628,10 @@ Proof. rewrite <- (negb_involutive (Int.testbit i (Int.zwordsize - 1))). f_equal. generalize (Int.size_range (Int.not i)); intros RANGE. - rewrite <- ! Int.bits_not by omega. - rewrite ! Int.bits_size_2 by omega. + rewrite <- ! Int.bits_not by lia. + rewrite ! Int.bits_size_2 by lia. auto. -- rewrite ! Int.bits_size_2 by omega. +- rewrite ! Int.bits_size_2 by lia. auto. Qed. @@ -639,8 +639,8 @@ Lemma is_uns_zero_ext: forall n i, is_uns n i <-> Int.zero_ext n i = i. Proof. intros; split; intros. - Int.bit_solve. destruct (zlt i0 n); auto. symmetry; apply H; auto. omega. - rewrite <- H. red; intros. rewrite Int.bits_zero_ext by omega. rewrite zlt_false by omega. auto. + Int.bit_solve. destruct (zlt i0 n); auto. symmetry; apply H; auto. lia. + rewrite <- H. red; intros. rewrite Int.bits_zero_ext by lia. rewrite zlt_false by lia. auto. Qed. Lemma is_sgn_sign_ext: @@ -649,18 +649,18 @@ Proof. intros; split; intros. Int.bit_solve. destruct (zlt i0 n); auto. transitivity (Int.testbit i (Int.zwordsize - 1)). - apply H0; omega. symmetry; apply H0; omega. - rewrite <- H0. red; intros. rewrite ! Int.bits_sign_ext by omega. - f_equal. transitivity (n-1). destruct (zlt m n); omega. - destruct (zlt (Int.zwordsize - 1) n); omega. + apply H0; lia. symmetry; apply H0; lia. + rewrite <- H0. red; intros. rewrite ! Int.bits_sign_ext by lia. + f_equal. transitivity (n-1). destruct (zlt m n); lia. + destruct (zlt (Int.zwordsize - 1) n); lia. Qed. Lemma is_zero_ext_uns: forall i n m, is_uns m i \/ n <= m -> is_uns m (Int.zero_ext n i). Proof. - intros. red; intros. rewrite Int.bits_zero_ext by omega. - destruct (zlt m0 n); auto. destruct H. apply H; omega. omegaContradiction. + intros. red; intros. rewrite Int.bits_zero_ext by lia. + destruct (zlt m0 n); auto. destruct H. apply H; lia. extlia. Qed. Lemma is_zero_ext_sgn: @@ -668,9 +668,9 @@ Lemma is_zero_ext_sgn: n < m -> is_sgn m (Int.zero_ext n i). Proof. - intros. red; intros. rewrite ! Int.bits_zero_ext by omega. - transitivity false. apply zlt_false; omega. - symmetry; apply zlt_false; omega. + intros. red; intros. rewrite ! Int.bits_zero_ext by lia. + transitivity false. apply zlt_false; lia. + symmetry; apply zlt_false; lia. Qed. Lemma is_sign_ext_uns: @@ -679,8 +679,8 @@ Lemma is_sign_ext_uns: is_uns m i -> is_uns m (Int.sign_ext n i). Proof. - intros; red; intros. rewrite Int.bits_sign_ext by omega. - apply H0. destruct (zlt m0 n); omega. destruct (zlt m0 n); omega. + intros; red; intros. rewrite Int.bits_sign_ext by lia. + apply H0. destruct (zlt m0 n); lia. destruct (zlt m0 n); lia. Qed. Lemma is_sign_ext_sgn: @@ -690,9 +690,9 @@ Lemma is_sign_ext_sgn: Proof. intros. apply is_sgn_sign_ext; auto. destruct (zlt m n). destruct H1. apply is_sgn_sign_ext in H1; auto. - rewrite <- H1. rewrite (Int.sign_ext_widen i) by omega. apply Int.sign_ext_idem; auto. - omegaContradiction. - apply Int.sign_ext_widen; omega. + rewrite <- H1. rewrite (Int.sign_ext_widen i) by lia. apply Int.sign_ext_idem; auto. + extlia. + apply Int.sign_ext_widen; lia. Qed. Hint Resolve is_uns_mon is_sgn_mon is_uns_sgn is_uns_usize is_sgn_ssize : va. @@ -701,8 +701,8 @@ Lemma is_uns_1: forall n, is_uns 1 n -> n = Int.zero \/ n = Int.one. Proof. intros. destruct (Int.testbit n 0) eqn:B0; [right|left]; apply Int.same_bits_eq; intros. - rewrite Int.bits_one. destruct (zeq i 0). subst i; auto. apply H; omega. - rewrite Int.bits_zero. destruct (zeq i 0). subst i; auto. apply H; omega. + rewrite Int.bits_one. destruct (zeq i 0). subst i; auto. apply H; lia. + rewrite Int.bits_zero. destruct (zeq i 0). subst i; auto. apply H; lia. Qed. (** Tracking leakage of pointers through arithmetic operations. @@ -958,13 +958,13 @@ Hint Resolve vge_uns_uns' vge_uns_i' vge_sgn_sgn' vge_sgn_i' : va. Lemma usize_pos: forall n, 0 <= usize n. Proof. - unfold usize; intros. generalize (Int.size_range n); omega. + unfold usize; intros. generalize (Int.size_range n); lia. Qed. Lemma ssize_pos: forall n, 0 < ssize n. Proof. unfold ssize; intros. - generalize (Int.size_range (if Int.lt n Int.zero then Int.not n else n)); omega. + generalize (Int.size_range (if Int.lt n Int.zero then Int.not n else n)); lia. Qed. Lemma vge_lub_l: @@ -975,12 +975,12 @@ Proof. unfold vlub; destruct x, y; eauto using pge_lub_l with va. - predSpec Int.eq Int.eq_spec n n0. auto with va. destruct (Int.lt n Int.zero || Int.lt n0 Int.zero). - apply vge_sgn_i'. generalize (ssize_pos n); xomega. eauto with va. - apply vge_uns_i'. generalize (usize_pos n); xomega. eauto with va. + apply vge_sgn_i'. generalize (ssize_pos n); extlia. eauto with va. + apply vge_uns_i'. generalize (usize_pos n); extlia. eauto with va. - destruct (Int.lt n Int.zero). - apply vge_sgn_i'. generalize (ssize_pos n); xomega. eauto with va. - apply vge_uns_i'. generalize (usize_pos n); xomega. eauto with va. -- apply vge_sgn_i'. generalize (ssize_pos n); xomega. eauto with va. + apply vge_sgn_i'. generalize (ssize_pos n); extlia. eauto with va. + apply vge_uns_i'. generalize (usize_pos n); extlia. eauto with va. +- apply vge_sgn_i'. generalize (ssize_pos n); extlia. eauto with va. - destruct (Int.lt n0 Int.zero). eapply vge_trans. apply vge_sgn_sgn'. apply vge_trans with (Sgn p (n + 1)); eauto with va. @@ -1269,12 +1269,12 @@ Proof. destruct (Int.ltu n Int.iwordsize) eqn:LTU; auto. exploit Int.ltu_inv; eauto. intros RANGE. inv H; auto with va. -- apply vmatch_uns'. red; intros. rewrite Int.bits_shl by omega. - destruct (zlt m (Int.unsigned n)). auto. apply H1; xomega. +- apply vmatch_uns'. red; intros. rewrite Int.bits_shl by lia. + destruct (zlt m (Int.unsigned n)). auto. apply H1; extlia. - apply vmatch_sgn'. red; intros. zify. - rewrite ! Int.bits_shl by omega. - rewrite ! zlt_false by omega. - rewrite H1 by omega. symmetry. rewrite H1 by omega. auto. + rewrite ! Int.bits_shl by lia. + rewrite ! zlt_false by lia. + rewrite H1 by lia. symmetry. rewrite H1 by lia. auto. - destruct v; constructor. Qed. @@ -1306,13 +1306,13 @@ Proof. assert (DEFAULT2: forall i, vmatch (Vint (Int.shru i n)) (uns (provenance x) (Int.zwordsize - Int.unsigned n))). { intros. apply vmatch_uns. red; intros. - rewrite Int.bits_shru by omega. apply zlt_false. omega. + rewrite Int.bits_shru by lia. apply zlt_false. lia. } inv H; auto with va. - apply vmatch_uns'. red; intros. zify. - rewrite Int.bits_shru by omega. + rewrite Int.bits_shru by lia. destruct (zlt (m + Int.unsigned n) Int.zwordsize); auto. - apply H1; omega. + apply H1; lia. - destruct v; constructor. Qed. @@ -1345,22 +1345,22 @@ Proof. assert (DEFAULT2: forall i, vmatch (Vint (Int.shr i n)) (sgn (provenance x) (Int.zwordsize - Int.unsigned n))). { intros. apply vmatch_sgn. red; intros. - rewrite ! Int.bits_shr by omega. f_equal. + rewrite ! Int.bits_shr by lia. f_equal. destruct (zlt (m + Int.unsigned n) Int.zwordsize); destruct (zlt (Int.zwordsize - 1 + Int.unsigned n) Int.zwordsize); - omega. + lia. } assert (SGN: forall q i p, is_sgn p i -> 0 < p -> vmatch (Vint (Int.shr i n)) (sgn q (p - Int.unsigned n))). { intros. apply vmatch_sgn'. red; intros. zify. - rewrite ! Int.bits_shr by omega. + rewrite ! Int.bits_shr by lia. transitivity (Int.testbit i (Int.zwordsize - 1)). destruct (zlt (m + Int.unsigned n) Int.zwordsize). - apply H0; omega. + apply H0; lia. auto. symmetry. destruct (zlt (Int.zwordsize - 1 + Int.unsigned n) Int.zwordsize). - apply H0; omega. + apply H0; lia. auto. } inv H; eauto with va. @@ -1418,12 +1418,12 @@ Proof. assert (UNS: forall i j n m, is_uns n i -> is_uns m j -> is_uns (Z.max n m) (Int.or i j)). { intros; red; intros. rewrite Int.bits_or by auto. - rewrite H by xomega. rewrite H0 by xomega. auto. + rewrite H by extlia. rewrite H0 by extlia. auto. } assert (SGN: forall i j n m, is_sgn n i -> is_sgn m j -> is_sgn (Z.max n m) (Int.or i j)). { - intros; red; intros. rewrite ! Int.bits_or by xomega. - rewrite H by xomega. rewrite H0 by xomega. auto. + intros; red; intros. rewrite ! Int.bits_or by extlia. + rewrite H by extlia. rewrite H0 by extlia. auto. } intros. unfold or, Val.or; inv H; eauto with va; inv H0; eauto with va. Qed. @@ -1443,12 +1443,12 @@ Proof. assert (UNS: forall i j n m, is_uns n i -> is_uns m j -> is_uns (Z.max n m) (Int.xor i j)). { intros; red; intros. rewrite Int.bits_xor by auto. - rewrite H by xomega. rewrite H0 by xomega. auto. + rewrite H by extlia. rewrite H0 by extlia. auto. } assert (SGN: forall i j n m, is_sgn n i -> is_sgn m j -> is_sgn (Z.max n m) (Int.xor i j)). { - intros; red; intros. rewrite ! Int.bits_xor by xomega. - rewrite H by xomega. rewrite H0 by xomega. auto. + intros; red; intros. rewrite ! Int.bits_xor by extlia. + rewrite H by extlia. rewrite H0 by extlia. auto. } intros. unfold xor, Val.xor; inv H; eauto with va; inv H0; eauto with va. Qed. @@ -1466,7 +1466,7 @@ Lemma notint_sound: Proof. assert (SGN: forall n i, is_sgn n i -> is_sgn n (Int.not i)). { - intros; red; intros. rewrite ! Int.bits_not by omega. + intros; red; intros. rewrite ! Int.bits_not by lia. f_equal. apply H; auto. } intros. unfold Val.notint, notint; inv H; eauto with va. @@ -1492,13 +1492,13 @@ Proof. inv H; auto with va. - apply vmatch_uns. red; intros. rewrite Int.bits_rol by auto. generalize (Int.unsigned_range n); intros. - rewrite Z.mod_small by omega. - apply H1. omega. omega. + rewrite Z.mod_small by lia. + apply H1. lia. lia. - destruct (zlt n0 Int.zwordsize); auto with va. - apply vmatch_sgn. red; intros. rewrite ! Int.bits_rol by omega. + apply vmatch_sgn. red; intros. rewrite ! Int.bits_rol by lia. generalize (Int.unsigned_range n); intros. - rewrite ! Z.mod_small by omega. - rewrite H1 by omega. symmetry. rewrite H1 by omega. auto. + rewrite ! Z.mod_small by lia. + rewrite H1 by lia. symmetry. rewrite H1 by lia. auto. - destruct (zlt n0 Int.zwordsize); auto with va. Qed. @@ -1674,8 +1674,8 @@ Proof. generalize (Int.unsigned_range_2 j); intros RANGE. assert (Int.unsigned j <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned j). rewrite H0. auto. } - exploit (Z_mod_lt (Int.unsigned i) (Int.unsigned j)). omega. intros MOD. - unfold Int.modu. rewrite Int.unsigned_repr. omega. omega. + exploit (Z_mod_lt (Int.unsigned i) (Int.unsigned j)). lia. intros MOD. + unfold Int.modu. rewrite Int.unsigned_repr. lia. lia. } intros. destruct v; destruct w; try discriminate; simpl in H1. destruct (Int.eq i0 Int.zero) eqn:Z; inv H1. @@ -2084,12 +2084,12 @@ Lemma zero_ext_sound: Proof. assert (DFL: forall nbits i, is_uns nbits (Int.zero_ext nbits i)). { - intros; red; intros. rewrite Int.bits_zero_ext by omega. apply zlt_false; auto. + intros; red; intros. rewrite Int.bits_zero_ext by lia. apply zlt_false; auto. } intros. inv H; simpl; auto with va. apply vmatch_uns. red; intros. zify. - rewrite Int.bits_zero_ext by omega. - destruct (zlt m nbits); auto. apply H1; omega. + rewrite Int.bits_zero_ext by lia. + destruct (zlt m nbits); auto. apply H1; lia. Qed. Definition sign_ext (nbits: Z) (v: aval) := @@ -2109,7 +2109,7 @@ Proof. intros. apply vmatch_sgn. apply is_sign_ext_sgn; auto with va. } intros. unfold sign_ext. destruct (zle nbits 0). -- destruct v; simpl; auto with va. constructor. omega. +- destruct v; simpl; auto with va. constructor. lia. rewrite Int.sign_ext_below by auto. red; intros; apply Int.bits_zero. - inv H; simpl; auto with va. + destruct (zlt n nbits); eauto with va. @@ -2514,26 +2514,26 @@ Proof. intros c [lo hi] x n; simpl; intros R. destruct c; unfold zcmp, proj_sumbool. - (* eq *) - destruct (zlt n lo). rewrite zeq_false by omega. constructor. - destruct (zlt hi n). rewrite zeq_false by omega. constructor. + destruct (zlt n lo). rewrite zeq_false by lia. constructor. + destruct (zlt hi n). rewrite zeq_false by lia. constructor. constructor. - (* ne *) constructor. - (* lt *) - destruct (zlt hi n). rewrite zlt_true by omega. constructor. - destruct (zle n lo). rewrite zlt_false by omega. constructor. + destruct (zlt hi n). rewrite zlt_true by lia. constructor. + destruct (zle n lo). rewrite zlt_false by lia. constructor. constructor. - (* le *) - destruct (zle hi n). rewrite zle_true by omega. constructor. - destruct (zlt n lo). rewrite zle_false by omega. constructor. + destruct (zle hi n). rewrite zle_true by lia. constructor. + destruct (zlt n lo). rewrite zle_false by lia. constructor. constructor. - (* gt *) - destruct (zlt n lo). rewrite zlt_true by omega. constructor. - destruct (zle hi n). rewrite zlt_false by omega. constructor. + destruct (zlt n lo). rewrite zlt_true by lia. constructor. + destruct (zle hi n). rewrite zlt_false by lia. constructor. constructor. - (* ge *) - destruct (zle n lo). rewrite zle_true by omega. constructor. - destruct (zlt hi n). rewrite zle_false by omega. constructor. + destruct (zle n lo). rewrite zle_true by lia. constructor. + destruct (zlt hi n). rewrite zle_false by lia. constructor. constructor. Qed. @@ -2567,10 +2567,10 @@ Lemma uintv_sound: forall n v, vmatch (Vint n) v -> fst (uintv v) <= Int.unsigned n <= snd (uintv v). Proof. intros. inv H; simpl; try (apply Int.unsigned_range_2). -- omega. +- lia. - destruct (zlt n0 Int.zwordsize); simpl. -+ rewrite is_uns_zero_ext in H2. rewrite <- H2. rewrite Int.zero_ext_mod by omega. - exploit (Z_mod_lt (Int.unsigned n) (two_p n0)). apply two_p_gt_ZERO; auto. omega. ++ rewrite is_uns_zero_ext in H2. rewrite <- H2. rewrite Int.zero_ext_mod by lia. + exploit (Z_mod_lt (Int.unsigned n) (two_p n0)). apply two_p_gt_ZERO; auto. lia. + apply Int.unsigned_range_2. Qed. @@ -2582,8 +2582,8 @@ Proof. intros. simpl. replace (Int.cmpu c n1 n2) with (zcmp c (Int.unsigned n1) (Int.unsigned n2)). apply zcmp_intv_sound; apply uintv_sound; auto. destruct c; simpl; auto. - unfold Int.ltu. destruct (zle (Int.unsigned n1) (Int.unsigned n2)); [rewrite zlt_false|rewrite zlt_true]; auto; omega. - unfold Int.ltu. destruct (zle (Int.unsigned n2) (Int.unsigned n1)); [rewrite zlt_false|rewrite zlt_true]; auto; omega. + unfold Int.ltu. destruct (zle (Int.unsigned n1) (Int.unsigned n2)); [rewrite zlt_false|rewrite zlt_true]; auto; lia. + unfold Int.ltu. destruct (zle (Int.unsigned n2) (Int.unsigned n1)); [rewrite zlt_false|rewrite zlt_true]; auto; lia. Qed. Lemma cmpu_intv_sound_2: @@ -2610,22 +2610,22 @@ Lemma sintv_sound: forall n v, vmatch (Vint n) v -> fst (sintv v) <= Int.signed n <= snd (sintv v). Proof. intros. inv H; simpl; try (apply Int.signed_range). -- omega. +- lia. - destruct (zlt n0 Int.zwordsize); simpl. + rewrite is_uns_zero_ext in H2. rewrite <- H2. - assert (Int.unsigned (Int.zero_ext n0 n) = Int.unsigned n mod two_p n0) by (apply Int.zero_ext_mod; omega). + assert (Int.unsigned (Int.zero_ext n0 n) = Int.unsigned n mod two_p n0) by (apply Int.zero_ext_mod; lia). exploit (Z_mod_lt (Int.unsigned n) (two_p n0)). apply two_p_gt_ZERO; auto. intros. replace (Int.signed (Int.zero_ext n0 n)) with (Int.unsigned (Int.zero_ext n0 n)). - rewrite H. omega. + rewrite H. lia. unfold Int.signed. rewrite zlt_true. auto. assert (two_p n0 <= Int.half_modulus). { change Int.half_modulus with (two_p (Int.zwordsize - 1)). - apply two_p_monotone. omega. } - omega. + apply two_p_monotone. lia. } + lia. + apply Int.signed_range. - destruct (zlt n0 (Int.zwordsize)); simpl. + rewrite is_sgn_sign_ext in H2 by auto. rewrite <- H2. - exploit (Int.sign_ext_range n0 n). omega. omega. + exploit (Int.sign_ext_range n0 n). lia. lia. + apply Int.signed_range. Qed. @@ -2637,8 +2637,8 @@ Proof. intros. simpl. replace (Int.cmp c n1 n2) with (zcmp c (Int.signed n1) (Int.signed n2)). apply zcmp_intv_sound; apply sintv_sound; auto. destruct c; simpl; rewrite ? Int.eq_signed; auto. - unfold Int.lt. destruct (zle (Int.signed n1) (Int.signed n2)); [rewrite zlt_false|rewrite zlt_true]; auto; omega. - unfold Int.lt. destruct (zle (Int.signed n2) (Int.signed n1)); [rewrite zlt_false|rewrite zlt_true]; auto; omega. + unfold Int.lt. destruct (zle (Int.signed n1) (Int.signed n2)); [rewrite zlt_false|rewrite zlt_true]; auto; lia. + unfold Int.lt. destruct (zle (Int.signed n2) (Int.signed n1)); [rewrite zlt_false|rewrite zlt_true]; auto; lia. Qed. Lemma cmp_intv_sound_2: @@ -2823,7 +2823,7 @@ Proof. assert (DEFAULT: vmatch (Val.of_optbool ob) (Uns Pbot 1)). { destruct ob; simpl; auto with va. - destruct b; constructor; try omega. + destruct b; constructor; try lia. change 1 with (usize Int.one). apply is_uns_usize. red; intros. apply Int.bits_zero. } @@ -2942,27 +2942,27 @@ Proof. - destruct (zlt n 8); constructor; auto with va. apply is_sign_ext_uns; auto. apply is_sign_ext_sgn; auto with va. -- constructor. xomega. apply is_zero_ext_uns. apply Z.min_case; auto with va. +- constructor. extlia. apply is_zero_ext_uns. apply Z.min_case; auto with va. - destruct (zlt n 16); constructor; auto with va. apply is_sign_ext_uns; auto. apply is_sign_ext_sgn; auto with va. -- constructor. xomega. apply is_zero_ext_uns. apply Z.min_case; auto with va. +- constructor. extlia. apply is_zero_ext_uns. apply Z.min_case; auto with va. - destruct (zlt n 8); auto with va. - destruct (zlt n 16); auto with va. -- constructor. xomega. apply is_sign_ext_sgn; auto with va. apply Z.min_case; auto with va. -- constructor. omega. apply is_zero_ext_uns; auto with va. -- constructor. xomega. apply is_sign_ext_sgn; auto with va. apply Z.min_case; auto with va. -- constructor. omega. apply is_zero_ext_uns; auto with va. +- constructor. extlia. apply is_sign_ext_sgn; auto with va. apply Z.min_case; auto with va. +- constructor. lia. apply is_zero_ext_uns; auto with va. +- constructor. extlia. apply is_sign_ext_sgn; auto with va. apply Z.min_case; auto with va. +- constructor. lia. apply is_zero_ext_uns; auto with va. - destruct ptr64; auto with va. - destruct ptr64; auto with va. - destruct ptr64; auto with va. - destruct ptr64; auto with va. - destruct ptr64; auto with va. - destruct ptr64; auto with va. -- constructor. omega. apply is_sign_ext_sgn; auto with va. -- constructor. omega. apply is_zero_ext_uns; auto with va. -- constructor. omega. apply is_sign_ext_sgn; auto with va. -- constructor. omega. apply is_zero_ext_uns; auto with va. +- constructor. lia. apply is_sign_ext_sgn; auto with va. +- constructor. lia. apply is_zero_ext_uns; auto with va. +- constructor. lia. apply is_sign_ext_sgn; auto with va. +- constructor. lia. apply is_zero_ext_uns; auto with va. - destruct ptr64; auto with va. - destruct ptr64; auto with va. - destruct ptr64; auto with va. @@ -2977,13 +2977,13 @@ Proof. intros. exploit Mem.load_cast; eauto. exploit Mem.load_type; eauto. destruct chunk; simpl; intros. - (* int8signed *) - rewrite H2. destruct v; simpl; constructor. omega. apply is_sign_ext_sgn; auto with va. + rewrite H2. destruct v; simpl; constructor. lia. apply is_sign_ext_sgn; auto with va. - (* int8unsigned *) - rewrite H2. destruct v; simpl; constructor. omega. apply is_zero_ext_uns; auto with va. + rewrite H2. destruct v; simpl; constructor. lia. apply is_zero_ext_uns; auto with va. - (* int16signed *) - rewrite H2. destruct v; simpl; constructor. omega. apply is_sign_ext_sgn; auto with va. + rewrite H2. destruct v; simpl; constructor. lia. apply is_sign_ext_sgn; auto with va. - (* int16unsigned *) - rewrite H2. destruct v; simpl; constructor. omega. apply is_zero_ext_uns; auto with va. + rewrite H2. destruct v; simpl; constructor. lia. apply is_zero_ext_uns; auto with va. - (* int32 *) auto. - (* int64 *) @@ -3025,9 +3025,9 @@ Proof with (auto using provenance_monotone with va). apply is_sign_ext_sgn... - constructor... apply is_zero_ext_uns... apply Z.min_case... - unfold provenance; destruct (va_strict tt)... -- destruct (zlt n1 8). rewrite zlt_true by omega... +- destruct (zlt n1 8). rewrite zlt_true by lia... destruct (zlt n2 8)... -- destruct (zlt n1 16). rewrite zlt_true by omega... +- destruct (zlt n1 16). rewrite zlt_true by lia... destruct (zlt n2 16)... - constructor... apply is_sign_ext_sgn... apply Z.min_case... - constructor... apply is_zero_ext_uns... @@ -3148,7 +3148,7 @@ Function inval_after (lo: Z) (hi: Z) (c: ZTree.t acontent) { wf (Zwf lo) hi } : then inval_after lo (hi - 1) (ZTree.remove hi c) else c. Proof. - intros; red; omega. + intros; red; lia. apply Zwf_well_founded. Qed. @@ -3163,7 +3163,7 @@ Function inval_before (hi: Z) (lo: Z) (c: ZTree.t acontent) { wf (Zwf_up hi) lo then inval_before hi (lo + 1) (inval_if hi lo c) else c. Proof. - intros; red; omega. + intros; red; lia. apply Zwf_up_well_founded. Qed. @@ -3201,7 +3201,7 @@ Remark loadbytes_load_ext: Proof. intros. exploit Mem.load_loadbytes; eauto. intros [bytes [A B]]. exploit Mem.load_valid_access; eauto. intros [C D]. - subst v. apply Mem.loadbytes_load; auto. apply H; auto. generalize (size_chunk_pos chunk); omega. + subst v. apply Mem.loadbytes_load; auto. apply H; auto. generalize (size_chunk_pos chunk); lia. Qed. Lemma smatch_ext: @@ -3212,7 +3212,7 @@ Lemma smatch_ext: Proof. intros. destruct H. split; intros. eapply H; eauto. eapply loadbytes_load_ext; eauto. - eapply H1; eauto. apply H0; eauto. omega. + eapply H1; eauto. apply H0; eauto. lia. Qed. Lemma smatch_inv: @@ -3247,19 +3247,19 @@ Proof. + rewrite (Mem.loadbytes_empty m b ofs sz) in LOAD by auto. inv LOAD. contradiction. + exploit (Mem.loadbytes_split m b ofs 1 (sz - 1) bytes). - replace (1 + (sz - 1)) with sz by omega. auto. - omega. - omega. + replace (1 + (sz - 1)) with sz by lia. auto. + lia. + lia. intros (bytes1 & bytes2 & LOAD1 & LOAD2 & CONCAT). subst bytes. exploit Mem.loadbytes_length. eexact LOAD1. change (Z.to_nat 1) with 1%nat. intros LENGTH1. rewrite in_app_iff in IN. destruct IN. * destruct bytes1; try discriminate. destruct bytes1; try discriminate. simpl in H. destruct H; try contradiction. subst m0. - exists ofs; split. omega. auto. - * exploit (REC (sz - 1)). red; omega. eexact LOAD2. auto. + exists ofs; split. lia. auto. + * exploit (REC (sz - 1)). red; lia. eexact LOAD2. auto. intros (ofs' & A & B). - exists ofs'; split. omega. auto. + exists ofs'; split. lia. auto. Qed. Lemma smatch_loadbytes: @@ -3285,13 +3285,13 @@ Proof. - apply Zwf_well_founded. - intros sz REC ofs bytes LOAD LOAD1 IN. exploit (Mem.loadbytes_split m b ofs 1 (sz - 1) bytes). - replace (1 + (sz - 1)) with sz by omega. auto. - omega. - omega. + replace (1 + (sz - 1)) with sz by lia. auto. + lia. + lia. intros (bytes1 & bytes2 & LOAD3 & LOAD4 & CONCAT). subst bytes. rewrite in_app_iff. destruct (zeq ofs ofs'). + subst ofs'. rewrite LOAD1 in LOAD3; inv LOAD3. left; simpl; auto. -+ right. eapply (REC (sz - 1)). red; omega. eexact LOAD4. auto. omega. ++ right. eapply (REC (sz - 1)). red; lia. eexact LOAD4. auto. lia. Qed. Lemma storebytes_provenance: @@ -3309,10 +3309,10 @@ Proof. destruct (eq_block b' b); auto. destruct (zle (ofs' + 1) ofs); auto. destruct (zle (ofs + Z.of_nat (length bytes)) ofs'); auto. - right. split. auto. omega. + right. split. auto. lia. } destruct EITHER as [A | (A & B)]. -- right. rewrite <- H0. symmetry. eapply Mem.loadbytes_storebytes_other; eauto. omega. +- right. rewrite <- H0. symmetry. eapply Mem.loadbytes_storebytes_other; eauto. lia. - subst b'. left. eapply loadbytes_provenance; eauto. eapply Mem.loadbytes_storebytes_same; eauto. @@ -3457,7 +3457,7 @@ Remark inval_after_outside: forall i lo hi c, i < lo \/ i > hi -> (inval_after lo hi c)##i = c##i. Proof. intros until c. functional induction (inval_after lo hi c); intros. - rewrite IHt by omega. apply ZTree.gro. unfold ZTree.elt, ZIndexed.t; omega. + rewrite IHt by lia. apply ZTree.gro. unfold ZTree.elt, ZIndexed.t; lia. auto. Qed. @@ -3468,18 +3468,18 @@ Remark inval_after_contents: Proof. intros until c. functional induction (inval_after lo hi c); intros. destruct (zeq i hi). - subst i. rewrite inval_after_outside in H by omega. rewrite ZTree.grs in H. discriminate. - exploit IHt; eauto. intros [A B]. rewrite ZTree.gro in A by auto. split. auto. omega. - split. auto. omega. + subst i. rewrite inval_after_outside in H by lia. rewrite ZTree.grs in H. discriminate. + exploit IHt; eauto. intros [A B]. rewrite ZTree.gro in A by auto. split. auto. lia. + split. auto. lia. Qed. Remark inval_before_outside: forall i hi lo c, i < lo \/ i >= hi -> (inval_before hi lo c)##i = c##i. Proof. intros until c. functional induction (inval_before hi lo c); intros. - rewrite IHt by omega. unfold inval_if. destruct (c##lo) as [[chunk av]|]; auto. + rewrite IHt by lia. unfold inval_if. destruct (c##lo) as [[chunk av]|]; auto. destruct (zle (lo + size_chunk chunk) hi); auto. - apply ZTree.gro. unfold ZTree.elt, ZIndexed.t; omega. + apply ZTree.gro. unfold ZTree.elt, ZIndexed.t; lia. auto. Qed. @@ -3490,21 +3490,21 @@ Remark inval_before_contents_1: Proof. intros until c. functional induction (inval_before hi lo c); intros. - destruct (zeq lo i). -+ subst i. rewrite inval_before_outside in H0 by omega. ++ subst i. rewrite inval_before_outside in H0 by lia. unfold inval_if in H0. destruct (c##lo) as [[chunk0 v0]|] eqn:C; try congruence. destruct (zle (lo + size_chunk chunk0) hi). rewrite C in H0; inv H0. auto. rewrite ZTree.grs in H0. congruence. -+ exploit IHt. omega. auto. intros [A B]; split; auto. ++ exploit IHt. lia. auto. intros [A B]; split; auto. unfold inval_if in A. destruct (c##lo) as [[chunk0 v0]|] eqn:C; auto. destruct (zle (lo + size_chunk chunk0) hi); auto. rewrite ZTree.gro in A; auto. -- omegaContradiction. +- extlia. Qed. Lemma max_size_chunk: forall chunk, size_chunk chunk <= 8. Proof. - destruct chunk; simpl; omega. + destruct chunk; simpl; lia. Qed. Remark inval_before_contents: @@ -3513,12 +3513,12 @@ Remark inval_before_contents: c##j = Some (ACval chunk' av') /\ (j + size_chunk chunk' <= i \/ i <= j). Proof. intros. destruct (zlt j (i - 7)). - rewrite inval_before_outside in H by omega. - split. auto. left. generalize (max_size_chunk chunk'); omega. + rewrite inval_before_outside in H by lia. + split. auto. left. generalize (max_size_chunk chunk'); lia. destruct (zlt j i). - exploit inval_before_contents_1; eauto. omega. tauto. - rewrite inval_before_outside in H by omega. - split. auto. omega. + exploit inval_before_contents_1; eauto. lia. tauto. + rewrite inval_before_outside in H by lia. + split. auto. lia. Qed. Lemma ablock_store_contents: @@ -3534,7 +3534,7 @@ Proof. right. rewrite ZTree.gso in H by auto. exploit inval_before_contents; eauto. intros [A B]. exploit inval_after_contents; eauto. intros [C D]. - split. auto. omega. + split. auto. lia. Qed. Lemma chunk_compat_true: @@ -3604,7 +3604,7 @@ Proof. unfold ablock_storebytes; simpl; intros. exploit inval_before_contents; eauto. clear H. intros [A B]. exploit inval_after_contents; eauto. clear A. intros [C D]. - split. auto. xomega. + split. auto. extlia. Qed. Lemma ablock_storebytes_sound: @@ -3627,7 +3627,7 @@ Proof. exploit ablock_storebytes_contents; eauto. intros [A B]. assert (Mem.load chunk' m b ofs' = Some v'). { rewrite <- LOAD'; symmetry. eapply Mem.load_storebytes_other; eauto. - rewrite U. rewrite LENGTH. rewrite Z_to_nat_max. right; omega. } + rewrite U. rewrite LENGTH. rewrite Z_to_nat_max. right; lia. } exploit BM2; eauto. unfold ablock_load. rewrite A. rewrite COMPAT. auto. Qed. @@ -3755,7 +3755,7 @@ Proof. apply bmatch_inv with m; auto. + intros. eapply Mem.loadbytes_store_other; eauto. left. red; intros; subst b0. elim (C ofs). apply Mem.perm_cur_max. - apply P. generalize (size_chunk_pos chunk); omega. + apply P. generalize (size_chunk_pos chunk); lia. - intros; red; intros; elim (C ofs0). eauto with mem. Qed. @@ -4184,7 +4184,7 @@ Proof. - apply bmatch_ext with m; eauto with va. - apply smatch_ext with m; auto with va. - apply smatch_ext with m; auto with va. -- red; intros. exploit mmatch_below0; eauto. xomega. +- red; intros. exploit mmatch_below0; eauto. extlia. Qed. Lemma mmatch_free: @@ -4195,7 +4195,7 @@ Lemma mmatch_free: Proof. intros. apply mmatch_ext with m; auto. intros. eapply Mem.loadbytes_free_2; eauto. - erewrite <- Mem.nextblock_free by eauto. xomega. + erewrite <- Mem.nextblock_free by eauto. extlia. Qed. Lemma mmatch_top': @@ -4419,7 +4419,7 @@ Proof. { Local Transparent Mem.loadbytes. unfold Mem.loadbytes. rewrite pred_dec_true. reflexivity. - red; intros. replace ofs0 with ofs by omega. auto. + red; intros. replace ofs0 with ofs by lia. auto. } destruct mv; econstructor. destruct v; econstructor. apply inj_of_bc_valid. @@ -4440,7 +4440,7 @@ Proof. auto. - (* overflow *) intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. - rewrite Z.add_0_r. split. omega. apply Ptrofs.unsigned_range_2. + rewrite Z.add_0_r. split. lia. apply Ptrofs.unsigned_range_2. - (* perm inv *) intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. rewrite Z.add_0_r in H2. auto. -- cgit