Commit aba0e740 authored by Xavier Leroy's avatar Xavier Leroy
Browse files

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`.
parent 2e202e2b
......@@ -41,7 +41,7 @@ DIRS += MenhirLib
COQINCLUDES += -R MenhirLib MenhirLib
endif
COQCOPTS ?= -w -undeclared-scope -w -omega-is-deprecated
COQCOPTS ?= -w -undeclared-scope
COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS)
COQDEP="$(COQBIN)coqdep" $(COQINCLUDES)
COQDOC="$(COQBIN)coqdoc"
......
......@@ -1293,7 +1293,7 @@ Ltac Equalities :=
split. auto. intros. destruct B; auto. subst. auto.
- (* trace length *)
red; intros. inv H; simpl.
omega.
lia.
eapply external_call_trace_length; eauto.
eapply external_call_trace_length; eauto.
- (* initial states *)
......
......@@ -67,7 +67,7 @@ Lemma transf_function_no_overflow:
transf_function f = OK tf -> list_length_z tf.(fn_code) <= Ptrofs.max_unsigned.
Proof.
intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0.
omega.
lia.
Qed.
Lemma exec_straight_exec:
......@@ -424,8 +424,8 @@ Proof.
split. unfold goto_label. rewrite P. rewrite H1. auto.
split. rewrite Pregmap.gss. constructor; auto.
rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q.
auto. omega.
generalize (transf_function_no_overflow _ _ H0). omega.
auto. lia.
generalize (transf_function_no_overflow _ _ H0). lia.
intros. apply Pregmap.gso; auto.
Qed.
......@@ -949,10 +949,10 @@ Local Transparent destroyed_by_op.
rewrite <- (sp_val _ _ _ AG). rewrite F. reflexivity.
reflexivity.
eexact U. }
exploit exec_straight_steps_2; eauto using functions_transl. omega. constructor.
exploit exec_straight_steps_2; eauto using functions_transl. lia. constructor.
intros (ofs' & X & Y).
left; exists (State rs3 m3'); split.
eapply exec_straight_steps_1; eauto. omega. constructor.
eapply exec_straight_steps_1; eauto. lia. constructor.
econstructor; eauto.
rewrite X; econstructor; eauto.
apply agree_exten with rs2; eauto with asmgen.
......@@ -981,7 +981,7 @@ Local Transparent destroyed_at_function_entry. simpl.
- (* return *)
inv STACKS. simpl in *.
right. split. omega. split. auto.
right. split. lia. split. auto.
rewrite <- ATPC in H5.
econstructor; eauto. congruence.
Qed.
......
......@@ -81,8 +81,8 @@ Local Opaque Zzero_ext.
induction N as [ | N]; simpl; intros.
- constructor.
- set (frag := Zzero_ext 16 (Z.shiftr n p)) in *. destruct (Z.eqb frag 0).
+ apply IHN. omega.
+ econstructor. reflexivity. omega. apply IHN; omega.
+ apply IHN. lia.
+ econstructor. reflexivity. lia. apply IHN; lia.
Qed.
Fixpoint recompose_int (accu: Z) (l: list (Z * Z)) : Z :=
......@@ -100,43 +100,43 @@ Lemma decompose_int_correct:
if zlt i p then Z.testbit accu i else Z.testbit n i).
Proof.
induction N as [ | N]; intros until accu; intros PPOS ABOVE i RANGE.
- simpl. rewrite zlt_true; auto. xomega.
- simpl. rewrite zlt_true; auto. extlia.
- rewrite inj_S in RANGE. simpl.
set (frag := Zzero_ext 16 (Z.shiftr n p)).
assert (FRAG: forall i, p <= i < p + 16 -> Z.testbit n i = Z.testbit frag (i - p)).
{ unfold frag; intros. rewrite Zzero_ext_spec by omega. rewrite zlt_true by omega.
rewrite Z.shiftr_spec by omega. f_equal; omega. }
{ unfold frag; intros. rewrite Zzero_ext_spec by lia. rewrite zlt_true by lia.
rewrite Z.shiftr_spec by lia. f_equal; lia. }
destruct (Z.eqb_spec frag 0).
+ rewrite IHN.
* destruct (zlt i p). rewrite zlt_true by omega. auto.
* destruct (zlt i p). rewrite zlt_true by lia. auto.
destruct (zlt i (p + 16)); auto.
rewrite ABOVE by omega. rewrite FRAG by omega. rewrite e, Z.testbit_0_l. auto.
* omega.
* intros; apply ABOVE; omega.
* xomega.
rewrite ABOVE by lia. rewrite FRAG by lia. rewrite e, Z.testbit_0_l. auto.
* lia.
* intros; apply ABOVE; lia.
* extlia.
+ simpl. rewrite IHN.
* destruct (zlt i (p + 16)).
** rewrite Zinsert_spec by omega. unfold proj_sumbool.
rewrite zlt_true by omega.
** rewrite Zinsert_spec by lia. unfold proj_sumbool.
rewrite zlt_true by lia.
destruct (zlt i p).
rewrite zle_false by omega. auto.
rewrite zle_true by omega. simpl. symmetry; apply FRAG; omega.
** rewrite Z.ldiff_spec, Z.shiftl_spec by omega.
change 65535 with (two_p 16 - 1). rewrite Ztestbit_two_p_m1 by omega.
rewrite zlt_false by omega. rewrite zlt_false by omega. apply andb_true_r.
* omega.
* intros. rewrite Zinsert_spec by omega. unfold proj_sumbool.
rewrite zle_true by omega. rewrite zlt_false by omega. simpl.
apply ABOVE. omega.
* xomega.
rewrite zle_false by lia. auto.
rewrite zle_true by lia. simpl. symmetry; apply FRAG; lia.
** rewrite Z.ldiff_spec, Z.shiftl_spec by lia.
change 65535 with (two_p 16 - 1). rewrite Ztestbit_two_p_m1 by lia.
rewrite zlt_false by lia. rewrite zlt_false by lia. apply andb_true_r.
* lia.
* intros. rewrite Zinsert_spec by lia. unfold proj_sumbool.
rewrite zle_true by lia. rewrite zlt_false by lia. simpl.
apply ABOVE. lia.
* extlia.
Qed.
Corollary decompose_int_eqmod: forall N n,
eqmod (two_power_nat (N * 16)%nat) (recompose_int 0 (decompose_int N n 0)) n.
Proof.
intros; apply eqmod_same_bits; intros.
rewrite decompose_int_correct. apply zlt_false; omega.
omega. intros; apply Z.testbit_0_l. xomega.
rewrite decompose_int_correct. apply zlt_false; lia.
lia. intros; apply Z.testbit_0_l. extlia.
Qed.
Corollary decompose_notint_eqmod: forall N n,
......@@ -145,8 +145,8 @@ Corollary decompose_notint_eqmod: forall N n,
Proof.
intros; apply eqmod_same_bits; intros.
rewrite Z.lnot_spec, decompose_int_correct.
rewrite zlt_false by omega. rewrite Z.lnot_spec by omega. apply negb_involutive.
omega. intros; apply Z.testbit_0_l. xomega. omega.
rewrite zlt_false by lia. rewrite Z.lnot_spec by lia. apply negb_involutive.
lia. intros; apply Z.testbit_0_l. extlia. lia.
Qed.
Lemma negate_decomposition_wf:
......@@ -156,7 +156,7 @@ Proof.
instantiate (1 := (Z.lnot m)).
apply equal_same_bits; intros.
rewrite H. change 65535 with (two_p 16 - 1).
rewrite Z.lxor_spec, !Zzero_ext_spec, Z.lnot_spec, Ztestbit_two_p_m1 by omega.
rewrite Z.lxor_spec, !Zzero_ext_spec, Z.lnot_spec, Ztestbit_two_p_m1 by lia.
destruct (zlt i 16).
apply xorb_true_r.
auto.
......@@ -167,7 +167,7 @@ Lemma Zinsert_eqmod:
eqmod (two_power_nat n) x1 x2 ->
eqmod (two_power_nat n) (Zinsert x1 y p l) (Zinsert x2 y p l).
Proof.
intros. apply eqmod_same_bits; intros. rewrite ! Zinsert_spec by omega.
intros. apply eqmod_same_bits; intros. rewrite ! Zinsert_spec by lia.
destruct (zle p i && zlt i (p + l)); auto.
apply same_bits_eqmod with n; auto.
Qed.
......@@ -178,12 +178,12 @@ Lemma Zinsert_0_l:
Z.shiftl (Zzero_ext l y) p = Zinsert 0 (Zzero_ext l y) p l.
Proof.
intros. apply equal_same_bits; intros.
rewrite Zinsert_spec by omega. unfold proj_sumbool.
destruct (zlt i p); [rewrite zle_false by omega|rewrite zle_true by omega]; simpl.
rewrite Zinsert_spec by lia. unfold proj_sumbool.
destruct (zlt i p); [rewrite zle_false by lia|rewrite zle_true by lia]; simpl.
- rewrite Z.testbit_0_l, Z.shiftl_spec_low by auto. auto.
- rewrite Z.shiftl_spec by omega.
- rewrite Z.shiftl_spec by lia.
destruct (zlt i (p + l)); auto.
rewrite Zzero_ext_spec, zlt_false, Z.testbit_0_l by omega. auto.
rewrite Zzero_ext_spec, zlt_false, Z.testbit_0_l by lia. auto.
Qed.
Lemma recompose_int_negated:
......@@ -193,12 +193,12 @@ Proof.
induction 1; intros accu; simpl.
- auto.
- rewrite <- IHwf_decomposition. f_equal. apply equal_same_bits; intros.
rewrite Z.lnot_spec, ! Zinsert_spec, Z.lxor_spec, Z.lnot_spec by omega.
rewrite Z.lnot_spec, ! Zinsert_spec, Z.lxor_spec, Z.lnot_spec by lia.
unfold proj_sumbool.
destruct (zle p i); simpl; auto.
destruct (zlt i (p + 16)); simpl; auto.
change 65535 with (two_p 16 - 1).
rewrite Ztestbit_two_p_m1 by omega. rewrite zlt_true by omega.
rewrite Ztestbit_two_p_m1 by lia. rewrite zlt_true by lia.
apply xorb_true_r.
Qed.
......@@ -219,7 +219,7 @@ Proof.
(Zinsert accu n p 16))
as (rs' & P & Q & R).
Simpl. rewrite ACCU. simpl. f_equal. apply Int.eqm_samerepr.
apply Zinsert_eqmod. auto. omega. apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
apply Zinsert_eqmod. auto. lia. apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
exists rs'; split.
eapply exec_straight_opt_step_opt. simpl; eauto. auto. exact P.
split. exact Q. intros; Simpl. rewrite R by auto. Simpl.
......@@ -244,7 +244,7 @@ Proof.
unfold rs1; Simpl.
exists rs2; split.
eapply exec_straight_opt_step; eauto.
simpl. unfold rs1. do 5 f_equal. unfold accu0. rewrite H. apply Zinsert_0_l; omega.
simpl. unfold rs1. do 5 f_equal. unfold accu0. rewrite H. apply Zinsert_0_l; lia.
reflexivity.
split. exact Q.
intros. rewrite R by auto. unfold rs1; Simpl.
......@@ -272,7 +272,7 @@ Proof.
exists rs2; split.
eapply exec_straight_opt_step; eauto.
simpl. unfold rs1. do 5 f_equal.
unfold accu0. f_equal. rewrite H. apply Zinsert_0_l; omega.
unfold accu0. f_equal. rewrite H. apply Zinsert_0_l; lia.
reflexivity.
split. unfold accu0 in Q; rewrite recompose_int_negated in Q by auto. exact Q.
intros. rewrite R by auto. unfold rs1; Simpl.
......@@ -302,8 +302,8 @@ Proof.
apply Int.eqm_samerepr. apply decompose_notint_eqmod.
apply Int.repr_unsigned. }
destruct Nat.leb.
+ rewrite <- A. apply exec_loadimm_z_w. apply decompose_int_wf; omega.
+ rewrite <- B. apply exec_loadimm_n_w. apply decompose_int_wf; omega.
+ rewrite <- A. apply exec_loadimm_z_w. apply decompose_int_wf; lia.
+ rewrite <- B. apply exec_loadimm_n_w. apply decompose_int_wf; lia.
Qed.
Lemma exec_loadimm_k_x:
......@@ -323,7 +323,7 @@ Proof.
(Zinsert accu n p 16))
as (rs' & P & Q & R).
Simpl. rewrite ACCU. simpl. f_equal. apply Int64.eqm_samerepr.
apply Zinsert_eqmod. auto. omega. apply Int64.eqm_sym; apply Int64.eqm_unsigned_repr.
apply Zinsert_eqmod. auto. lia. apply Int64.eqm_sym; apply Int64.eqm_unsigned_repr.
exists rs'; split.
eapply exec_straight_opt_step_opt. simpl; eauto. auto. exact P.
split. exact Q. intros; Simpl. rewrite R by auto. Simpl.
......@@ -348,7 +348,7 @@ Proof.
unfold rs1; Simpl.
exists rs2; split.
eapply exec_straight_opt_step; eauto.
simpl. unfold rs1. do 5 f_equal. unfold accu0. rewrite H. apply Zinsert_0_l; omega.
simpl. unfold rs1. do 5 f_equal. unfold accu0. rewrite H. apply Zinsert_0_l; lia.
reflexivity.
split. exact Q.
intros. rewrite R by auto. unfold rs1; Simpl.
......@@ -376,7 +376,7 @@ Proof.
exists rs2; split.
eapply exec_straight_opt_step; eauto.
simpl. unfold rs1. do 5 f_equal.
unfold accu0. f_equal. rewrite H. apply Zinsert_0_l; omega.
unfold accu0. f_equal. rewrite H. apply Zinsert_0_l; lia.
reflexivity.
split. unfold accu0 in Q; rewrite recompose_int_negated in Q by auto. exact Q.
intros. rewrite R by auto. unfold rs1; Simpl.
......@@ -406,8 +406,8 @@ Proof.
apply Int64.eqm_samerepr. apply decompose_notint_eqmod.
apply Int64.repr_unsigned. }
destruct Nat.leb.
+ rewrite <- A. apply exec_loadimm_z_x. apply decompose_int_wf; omega.
+ rewrite <- B. apply exec_loadimm_n_x. apply decompose_int_wf; omega.
+ rewrite <- A. apply exec_loadimm_z_x. apply decompose_int_wf; lia.
+ rewrite <- B. apply exec_loadimm_n_x. apply decompose_int_wf; lia.
Qed.
(** Add immediate *)
......@@ -426,14 +426,14 @@ Lemma exec_addimm_aux_32:
Proof.
intros insn sem SEM ASSOC; intros. unfold addimm_aux.
set (nlo := Zzero_ext 12 (Int.unsigned n)). set (nhi := Int.unsigned n - nlo).
assert (E: Int.unsigned n = nhi + nlo) by (unfold nhi; omega).
assert (E: Int.unsigned n = nhi + nlo) by (unfold nhi; lia).
rewrite <- (Int.repr_unsigned n).
destruct (Z.eqb_spec nhi 0); [|destruct (Z.eqb_spec nlo 0)].
- econstructor; split. apply exec_straight_one. apply SEM. Simpl.
split. Simpl. do 3 f_equal; omega.
split. Simpl. do 3 f_equal; lia.
intros; Simpl.
- econstructor; split. apply exec_straight_one. apply SEM. Simpl.
split. Simpl. do 3 f_equal; omega.
split. Simpl. do 3 f_equal; lia.
intros; Simpl.
- econstructor; split. eapply exec_straight_two.
apply SEM. apply SEM. Simpl. Simpl.
......@@ -484,14 +484,14 @@ Lemma exec_addimm_aux_64:
Proof.
intros insn sem SEM ASSOC; intros. unfold addimm_aux.
set (nlo := Zzero_ext 12 (Int64.unsigned n)). set (nhi := Int64.unsigned n - nlo).
assert (E: Int64.unsigned n = nhi + nlo) by (unfold nhi; omega).
assert (E: Int64.unsigned n = nhi + nlo) by (unfold nhi; lia).
rewrite <- (Int64.repr_unsigned n).
destruct (Z.eqb_spec nhi 0); [|destruct (Z.eqb_spec nlo 0)].
- econstructor; split. apply exec_straight_one. apply SEM. Simpl.
split. Simpl. do 3 f_equal; omega.
split. Simpl. do 3 f_equal; lia.
intros; Simpl.
- econstructor; split. apply exec_straight_one. apply SEM. Simpl.
split. Simpl. do 3 f_equal; omega.
split. Simpl. do 3 f_equal; lia.
intros; Simpl.
- econstructor; split. eapply exec_straight_two.
apply SEM. apply SEM. Simpl. Simpl.
......
......@@ -391,7 +391,7 @@ Proof.
Int.bit_solve. destruct (zlt i0 n0).
replace (Int.testbit n i0) with (negb (Int.testbit Int.zero i0)).
rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto.
rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto.
rewrite <- EQ. rewrite Int.bits_zero_ext by lia. rewrite zlt_true by auto.
rewrite Int.bits_not by auto. apply negb_involutive.
rewrite H6 by auto. auto.
econstructor; split; eauto. auto.
......
......@@ -274,33 +274,33 @@ Proof.
assert (ALP: forall ofs ty, ofs >= 0 -> align ofs (typesize ty) >= 0).
{ intros.
assert (ofs <= align ofs (typesize ty)) by (apply align_le; apply typesize_pos).
omega. }
lia. }
assert (ALD: forall ofs ty, ofs >= 0 -> (typealign ty | align ofs (typesize ty))).
{ intros. apply Z.divide_trans with (typesize ty). apply typealign_typesize. apply align_divides. apply typesize_pos. }
assert (ALP2: forall ofs, ofs >= 0 -> align ofs 2 >= 0).
{ intros.
assert (ofs <= align ofs 2) by (apply align_le; omega).
omega. }
assert (ofs <= align ofs 2) by (apply align_le; lia).
lia. }
assert (ALD2: forall ofs ty, ofs >= 0 -> (typealign ty | align ofs 2)).
{ intros. eapply Z.divide_trans with 2.
exists (2 / typealign ty). destruct ty; reflexivity.
apply align_divides. omega. }
apply align_divides. lia. }
assert (STK: forall tyl ofs,
ofs >= 0 -> OK (loc_arguments_stack tyl ofs)).
{ induction tyl as [ | ty tyl]; intros ofs OO; red; simpl; intros.
- contradiction.
- destruct H.
+ subst p. split. auto. simpl. apply Z.divide_1_l.
+ apply IHtyl with (ofs := ofs + 2). omega. auto.
+ apply IHtyl with (ofs := ofs + 2). lia. auto.
}
assert (A: forall ty ri rf ofs f,
OKF f -> ofs >= 0 -> OK (stack_arg ty ri rf ofs f)).
{ intros until f; intros OF OO; red; unfold stack_arg; intros.
destruct Archi.abi; destruct H.
- subst p; simpl; auto.
- eapply OF; [|eauto]. apply ALP2 in OO. omega.
- eapply OF; [|eauto]. apply ALP2 in OO. lia.
- subst p; simpl; auto.
- eapply OF; [|eauto]. apply (ALP ofs ty) in OO. generalize (typesize_pos ty). omega.
- eapply OF; [|eauto]. apply (ALP ofs ty) in OO. generalize (typesize_pos ty). lia.
}
assert (B: forall ty ri rf ofs f,
OKF f -> ofs >= 0 -> OK (int_arg ty ri rf ofs f)).
......@@ -332,7 +332,7 @@ Lemma loc_arguments_acceptable:
In p (loc_arguments s) -> forall_rpair loc_argument_acceptable p.
Proof.
unfold loc_arguments; intros.
eapply loc_arguments_rec_charact; eauto. omega.
eapply loc_arguments_rec_charact; eauto. lia.
Qed.
Hint Resolve loc_arguments_acceptable: locs.
......
......@@ -957,25 +957,25 @@ End SHIFT_AMOUNT.
Program Definition mk_amount32 (n: int): amount32 :=
{| a32_amount := Int.zero_ext 5 n |}.
Next Obligation.
apply mk_amount_range. omega. reflexivity.
apply mk_amount_range. lia. reflexivity.
Qed.
Lemma mk_amount32_eq: forall n,
Int.ltu n Int.iwordsize = true -> a32_amount (mk_amount32 n) = n.
Proof.
intros. eapply mk_amount_eq; eauto. omega. reflexivity.
intros. eapply mk_amount_eq; eauto. lia. reflexivity.
Qed.
Program Definition mk_amount64 (n: int): amount64 :=
{| a64_amount := Int.zero_ext 6 n |}.
Next Obligation.
apply mk_amount_range. omega. reflexivity.
apply mk_amount_range. lia. reflexivity.
Qed.
Lemma mk_amount64_eq: forall n,
Int.ltu n Int64.iwordsize' = true -> a64_amount (mk_amount64 n) = n.
Proof.
intros. eapply mk_amount_eq; eauto. omega. reflexivity.
intros. eapply mk_amount_eq; eauto. lia. reflexivity.
Qed.
(** Recognition of move operations. *)
......
......@@ -225,8 +225,8 @@ Proof.
intros. unfold Int.ltu; apply zlt_true.
apply Int.ltu_inv in H. apply Int.ltu_inv in H0.
change (Int.unsigned Int64.iwordsize') with Int64.zwordsize in *.
unfold Int.sub; rewrite Int.unsigned_repr. omega.
assert (Int64.zwordsize < Int.max_unsigned) by reflexivity. omega.
unfold Int.sub; rewrite Int.unsigned_repr. lia.
assert (Int64.zwordsize < Int.max_unsigned) by reflexivity. lia.
Qed.
Theorem eval_shrluimm:
......@@ -242,13 +242,13 @@ Local Opaque Int64.zwordsize.
+ destruct (Int.ltu n a) eqn:L2.
* assert (L3: Int.ltu (Int.sub a n) Int64.iwordsize' = true).
{ apply sub_shift_amount; auto using a64_range.
apply Int.ltu_inv in L2. omega. }
apply Int.ltu_inv in L2. lia. }
econstructor; split. EvalOp.
destruct v1; simpl; auto. rewrite mk_amount64_eq, L3, a64_range by auto.
simpl. rewrite L. rewrite Int64.shru'_shl', L2 by auto using a64_range. auto.
* assert (L3: Int.ltu (Int.sub n a) Int64.iwordsize' = true).
{ apply sub_shift_amount; auto using a64_range.
unfold Int.ltu in L2. destruct zlt in L2; discriminate || omega. }
unfold Int.ltu in L2. destruct zlt in L2; discriminate || lia. }
econstructor; split. EvalOp.
destruct v1; simpl; auto. rewrite mk_amount64_eq, L3, a64_range by auto.
simpl. rewrite L. rewrite Int64.shru'_shl', L2 by auto using a64_range. auto.
......@@ -261,11 +261,11 @@ Local Opaque Int64.zwordsize.
* econstructor; split. EvalOp. rewrite mk_amount64_eq by auto.
destruct v1; simpl; auto. rewrite ! L; simpl.
set (s' := s - Int.unsigned n).
replace s with (s' + Int.unsigned n) by (unfold s'; omega).
rewrite Int64.shru'_zero_ext. auto. unfold s'; omega.
replace s with (s' + Int.unsigned n) by (unfold s'; lia).
rewrite Int64.shru'_zero_ext. auto. unfold s'; lia.
* econstructor; split. EvalOp.
destruct v1; simpl; auto. rewrite ! L; simpl.
rewrite Int64.shru'_zero_ext_0 by omega. auto.
rewrite Int64.shru'_zero_ext_0 by lia. auto.
+ econstructor; eauto using eval_shrluimm_base.
- intros; TrivialExists.
Qed.
......@@ -290,13 +290,13 @@ Proof.
+ destruct (Int.ltu n a) eqn:L2.
* assert (L3: Int.ltu (Int.sub a n) Int64.iwordsize' = true).
{ apply sub_shift_amount; auto using a64_range.
apply Int.ltu_inv in L2. omega. }
apply Int.ltu_inv in L2. lia. }
econstructor; split. EvalOp.
destruct v1; simpl; auto. rewrite mk_amount64_eq, L3, a64_range by auto.
simpl. rewrite L. rewrite Int64.shr'_shl', L2 by auto using a64_range. auto.
* assert (L3: Int.ltu (Int.sub n a) Int64.iwordsize' = true).
{ apply sub_shift_amount; auto using a64_range.
unfold Int.ltu in L2. destruct zlt in L2; discriminate || omega. }
unfold Int.ltu in L2. destruct zlt in L2; discriminate || lia. }
econstructor; split. EvalOp.
destruct v1; simpl; auto. rewrite mk_amount64_eq, L3, a64_range by auto.
simpl. rewrite L. rewrite Int64.shr'_shl', L2 by auto using a64_range. auto.
......@@ -309,8 +309,8 @@ Proof.
* InvBooleans. econstructor; split. EvalOp. rewrite mk_amount64_eq by auto.
destruct v1; simpl; auto. rewrite ! L; simpl.
set (s' := s - Int.unsigned n).
replace s with (s' + Int.unsigned n) by (unfold s'; omega).
rewrite Int64.shr'_sign_ext. auto. unfold s'; omega. unfold s'; omega.
replace s with (s' + Int.unsigned n) by (unfold s'; lia).
rewrite Int64.shr'_sign_ext. auto. unfold s'; lia. unfold s'; lia.
* econstructor; split; [|eauto]. apply eval_shrlimm_base; auto. EvalOp.
+ econstructor; eauto using eval_shrlimm_base.
- intros; TrivialExists.
......@@ -392,7 +392,7 @@ Proof.
- TrivialExists.
- destruct (zlt (Int.unsigned a0) sz).
+ econstructor; split. EvalOp. destruct v1; simpl; auto. rewrite a64_range; simpl.
apply Val.lessdef_same. f_equal. rewrite Int64.shl'_zero_ext by omega. f_equal. omega.
apply Val.lessdef_same. f_equal. rewrite Int64.shl'_zero_ext by lia. f_equal. lia.
+ TrivialExists.
- TrivialExists.
Qed.
......
......@@ -243,8 +243,8 @@ Remark sub_shift_amount:
Proof.
intros. unfold Int.ltu; apply zlt_true. rewrite Int.unsigned_repr_wordsize.
apply Int.ltu_iwordsize_inv in H. apply Int.ltu_iwordsize_inv in H0.
unfold Int.sub; rewrite Int.unsigned_repr. omega.
generalize Int.wordsize_max_unsigned; omega.
unfold Int.sub; rewrite Int.unsigned_repr. lia.
generalize Int.wordsize_max_unsigned; lia.
Qed.
Theorem eval_shruimm:
......@@ -260,13 +260,13 @@ Local Opaque Int.zwordsize.
+ destruct (Int.ltu n a) eqn:L2.
* assert (L3: Int.ltu (Int.sub a n) Int.iwordsize = true).
{ apply sub_shift_amount; auto using a32_range.
apply Int.ltu_inv in L2. omega. }
apply Int.ltu_inv in L2. lia. }
econstructor; split. EvalOp.
destruct v1; simpl; auto. rewrite mk_amount32_eq, L3, a32_range by auto.
simpl. rewrite L. rewrite Int.shru_shl, L2 by auto using a32_range. auto.
* assert (L3: Int.ltu (Int.sub n a) Int.iwordsize = true).
{ apply sub_shift_amount; auto using a32_range.
unfold Int.ltu in L2. destruct zlt in L2; discriminate || omega. }
unfold Int.ltu in L2. destruct zlt in L2; discriminate || lia. }
econstructor; split. EvalOp.
destruct v1; simpl; auto. rewrite mk_amount32_eq, L3, a32_range by auto.
simpl. rewrite L. rewrite Int.shru_shl, L2 by auto using a32_range. auto.
......@@ -279,11 +279,11 @@ Local Opaque Int.zwordsize.
* econstructor; split. EvalOp. rewrite mk_amount32_eq by auto.
destruct v1; simpl; auto. rewrite ! L; simpl.
set (s' := s - Int.unsigned n).
replace s with (s' + Int.unsigned n) by (unfold s'; omega).
rewrite Int.shru_zero_ext. auto. unfold s'; omega.
replace s with (s' + Int.unsigned n) by (unfold s'; lia).
rewrite Int.shru_zero_ext. auto. unfold s'; lia.
* econstructor; split. EvalOp.
destruct v1; simpl; auto. rewrite ! L; simpl.
rewrite Int.shru_zero_ext_0 by omega. auto.
rewrite Int.shru_zero_ext_0 by lia. auto.
+ econstructor; eauto using eval_shruimm_base.
- intros; TrivialExists.
Qed.
......@@ -308,13 +308,13 @@ Proof.
+ destruct (Int.ltu n a) eqn:L2.
* assert (L3: Int.ltu (Int.sub a n) Int.iwordsize = true).
{ apply sub_shift_amount; auto using a32_range.
apply Int.ltu_inv in L2. omega. }
apply Int.ltu_inv in L2. lia. }
econstructor; split. EvalOp.
destruct v1; simpl; auto. rewrite mk_amount32_eq, L3, a32_range by auto.
simpl. rewrite L. rewrite Int.shr_shl, L2 by auto using a32_range. auto.
* assert (L3: Int.ltu (Int.sub n a) Int.iwordsize = true).
{ apply sub_shift_amount; auto using a32_range.
unfold Int.ltu in L2. destruct zlt in L2; discriminate || omega. }
unfold Int.ltu in L2. destruct zlt in L2; discriminate || lia. }
econstructor; split. EvalOp.
destruct v1; simpl; auto. rewrite mk_amount32_eq, L3, a32_range by auto.
simpl. rewrite L. rewrite Int.shr_shl, L2 by auto using a32_range. auto.
......@@ -327,8 +327,8 @@ Proof.
* InvBooleans. econstructor; split. EvalOp. rewrite mk_amount32_eq by auto.
destruct v1; simpl; auto. rewrite ! L; simpl.
set (s' := s - Int.unsigned n).
replace s with (s' + Int.unsigned n) by (unfold s'; omega).
rewrite Int.shr_sign_ext. auto. unfold s'; omega. unfold s'; omega.
replace s with (s' + Int.unsigned n) by (unfold s'; lia).
rewrite Int.shr_sign_ext. auto. unfold s'; lia. unfold s'; lia.
* econstructor; split; [|eauto]. apply eval_shrimm_base; auto. EvalOp.
+ econstructor; eauto using eval_shrimm_base.
- intros; TrivialExists.
......@@ -399,20 +399,20 @@ Proof.
change (Int.ltu (Int.repr 32) Int64.iwordsize') with true; simpl.
apply Val.lessdef_same. f_equal.
transitivity (Int.repr (Z.shiftr (Int.signed i * Int.signed i0) 32)).
unfold Int.mulhs; f_equal. rewrite Zshiftr_div_two_p by omega. reflexivity.
unfold Int.mulhs; f_equal. rewrite Zshiftr_div_two_p by lia. reflexivity.
apply Int.same_bits_eq; intros n N.
change Int.zwordsize with 32 in *.
assert (N1: 0 <= n < 64) by omega.
assert (N1: 0 <= n < 64) by lia.
rewrite Int64.bits_loword by auto.
rewrite Int64.bits_shr' by auto.
change (Int.unsigned (Int.repr 32)) with 32. change Int64.zwordsize with 64.
rewrite zlt_true by omega.
rewrite zlt_true by lia.
rewrite Int.testbit_repr by auto.
unfold Int64.mul. rewrite Int64.testbit_repr by (change Int64.zwordsize with 64; omega).
unfold Int64.mul. rewrite Int64.testbit_repr by (change Int64.zwordsize with 64; lia).
transitivity (Z.testbit (Int.signed i * Int.signed i0) (n + 32)).
rewrite Z.shiftr_spec by omega. auto.
rewrite Z.shiftr_spec by lia. auto.
apply Int64.same_bits_eqm. apply Int64.eqm_mult; apply Int64.eqm_unsigned_repr.
change Int64.zwordsize with 64; omega.
change Int64.zwordsize with 64; lia.
Qed.
Theorem eval_mulhu: binary_constructor_sound mulhu Val.mulhu.
......@@ -425,20 +425,20 @@ Proof.
change (Int.ltu (Int.repr 32) Int64.iwordsize') with true; simpl.
apply Val.lessdef_same. f_equal.
transitivity (Int.repr (Z.shiftr (Int.unsigned i * Int.unsigned i0) 32)).
unfold Int.mulhu; f_equal. rewrite Zshiftr_div_two_p by omega. reflexivity.