Val_cmp* -> Val.mxcmp*

11 files changed, 240 insertions, 254 deletions

diff --git a/Makefile b/Makefile
index 616c808f..de9da384 100644
--- a/Makefile
+++ b/Makefile
@@ -274,10 +274,14 @@ latexdoc:
 	@tools/ndfun $*.vp > $*.v || { rm -f $*.v; exit 2; }
 	@chmod a-w $*.v
 
+# this trick aims to allow extraction to depend on the target processor
+# (currently: export extra Coq-functions for OCaml code, depending on the target)
 extraction/extraction.v: Makefile extraction/extraction.vexpand
-	cat extraction/extraction.vexpand > extraction/extraction.v
-	echo "$(EXTRA_EXTRACTION)" >> extraction/extraction.v
-	echo "." >> extraction/extraction.v
+	(echo "(* WARNING: this file is generated from extraction.vexpand *)"; \
+	 echo "(* by the Makefile -- target \"extraction/extraction.v\"   *)\n"; \
+	 cat extraction/extraction.vexpand; \
+	 echo "$(EXTRA_EXTRACTION)"; \
+	 echo ".") > extraction/extraction.v
 
 driver/Compiler.v: driver/Compiler.vexpand tools/compiler_expand
 	tools/compiler_expand driver/Compiler.vexpand $@
diff --git a/aarch64/Asm.v b/aarch64/Asm.v
index 30bac2a4..dc1f025f 100644
--- a/aarch64/Asm.v
+++ b/aarch64/Asm.v
@@ -416,60 +416,6 @@ Definition outcome := option state.
 Definition Next rs m: outcome := Some (State rs m).
 Definition Stuck: outcome := None.
 
-
-(* a few lemma on comparisons of unsigned (e.g. pointers)
-
-TODO: these lemma are a copy/paste of kvx/Asmvliw.v (sharing to improve!)
-*)
-
-Definition Val_cmpu_bool cmp v1 v2: option bool :=
-  Val.cmpu_bool (fun _ _ => true) cmp v1 v2.
-
-Lemma Val_cmpu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b:
-   (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b
-   -> (Val_cmpu_bool cmp v1 v2) = Some b.
-Proof.
-  intros; eapply Val.cmpu_bool_lessdef; (econstructor 1 || eauto).
-Qed.
-
-Definition Val_cmpu cmp v1 v2 := Val.of_optbool (Val_cmpu_bool cmp v1 v2).
-
-Lemma Val_cmpu_correct (m:mem) (cmp: comparison) (v1 v2: val):
-   Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp v1 v2)
-               (Val_cmpu cmp v1 v2).
-Proof.
-  unfold Val.cmpu, Val_cmpu.
-  remember (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as ob.
-  destruct ob; simpl.
-  - erewrite Val_cmpu_bool_correct; eauto.
-    econstructor.
-  - econstructor.
-Qed.
-
-Definition Val_cmplu_bool (cmp: comparison) (v1 v2: val)
- := (Val.cmplu_bool (fun _ _ => true) cmp v1 v2).
-
-Lemma Val_cmplu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b:
-   (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b
-   -> (Val_cmplu_bool cmp v1 v2) = Some b.
-Proof.
-  intros; eapply Val.cmplu_bool_lessdef; (econstructor 1 || eauto).
-Qed.
-
-Definition Val_cmplu cmp v1 v2 := Val.of_optbool (Val_cmplu_bool cmp v1 v2).
-
-Lemma Val_cmplu_correct (m:mem) (cmp: comparison) (v1 v2: val):
-   Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp v1 v2))
-               (Val_cmplu cmp v1 v2).
-Proof.
-  unfold Val.cmplu, Val_cmplu.
-  remember (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) as ob.
-  destruct ob as [b|]; simpl.
-  - erewrite Val_cmplu_bool_correct; eauto.
-    simpl. econstructor.
-  - econstructor.
-Qed.
-
 (** Testing a condition *)
 
 Definition eval_testcond (c: testcond) (rs: regset) : option bool :=
@@ -540,8 +486,8 @@ Definition eval_testcond (c: testcond) (rs: regset) : option bool :=
 
 Definition eval_testzero (sz: isize) (v: val): option bool :=
   match sz with
-  | W => Val_cmpu_bool Ceq v (Vint Int.zero)
-  | X => Val_cmplu_bool Ceq v (Vlong Int64.zero)
+  | W => Val.mxcmpu_bool Ceq v (Vint Int.zero)
+  | X => Val.mxcmplu_bool Ceq v (Vlong Int64.zero)
   end.
 
 (** Integer "bit is set?" test *)
@@ -557,14 +503,14 @@ Definition eval_testbit (sz: isize) (v: val) (n: int): option bool :=
 
 Definition compare_int (rs: regset) (v1 v2: val) :=
   rs#CN <- (Val.negative (Val.sub v1 v2))
-    #CZ <- (Val_cmpu Ceq v1 v2)
-    #CC <- (Val_cmpu Cge v1 v2)
+    #CZ <- (Val.mxcmpu Ceq v1 v2)
+    #CC <- (Val.mxcmpu Cge v1 v2)
     #CV <- (Val.sub_overflow v1 v2).
 
 Definition compare_long (rs: regset) (v1 v2: val) :=
   rs#CN <- (Val.negativel (Val.subl v1 v2))
-    #CZ <- (Val_cmplu Ceq v1 v2)
-    #CC <- (Val_cmplu Cge v1 v2)
+    #CZ <- (Val.mxcmplu Ceq v1 v2)
+    #CC <- (Val.mxcmplu Cge v1 v2)
     #CV <- (Val.subl_overflow v1 v2).
 
 (** Semantics of [fcmp] instructions:
diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v
index 670a7d06..e1d591df 100644
--- a/aarch64/Asmblockdeps.v
+++ b/aarch64/Asmblockdeps.v
@@ -211,14 +211,14 @@ Coercion Control: control_op >-> op_wrap.
 
 Definition v_compare_int (v1 v2: val) : CRflags :=
   {| _CN := (Val.negative (Val.sub v1 v2));
-     _CZ := (Val_cmpu Ceq v1 v2);
-     _CC := (Val_cmpu Cge v1 v2);
+     _CZ := (Val.mxcmpu Ceq v1 v2);
+     _CC := (Val.mxcmpu Cge v1 v2);
      _CV := (Val.sub_overflow v1 v2) |}.
 
 Definition v_compare_long (v1 v2: val) : CRflags :=
   {| _CN := (Val.negativel (Val.subl v1 v2));
-     _CZ := (Val_cmplu Ceq v1 v2);
-     _CC := (Val_cmplu Cge v1 v2);
+     _CZ := (Val.mxcmplu Ceq v1 v2);
+     _CC := (Val.mxcmplu Cge v1 v2);
      _CV := (Val.subl_overflow v1 v2) |}.
 
 Definition v_compare_float (v1 v2: val) : CRflags :=
@@ -1842,8 +1842,8 @@ Proof.
            destruct (PregEq.eq r PC);
            [ rewrite e; destruct sz0; simpl; Simpl sr |
              destruct sz0; simpl; replace_pc; rewrite Pregmap.gso; auto; repeat Simpl_rep sr; try rewrite H0;
-             try (destruct (Val_cmpu_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
-             try (destruct (Val_cmplu_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
+             try (destruct (Val.mxcmpu_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
+             try (destruct (Val.mxcmplu_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
              try (destruct (Val.cmp_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
              try (destruct (Val.cmpl_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
              try (simpl; rewrite sr_update_overwrite; replace_pc; Simpl sr);
diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v
index b55a1195..acb5a1e6 100644
--- a/aarch64/Asmblockgen.v
+++ b/aarch64/Asmblockgen.v
@@ -1245,7 +1245,7 @@ Definition transf_function (f: Machblock.function) : res Asmblock.function :=
   else OK tf.
 
 Definition transf_fundef (f: Machblock.fundef) : res Asmblock.fundef :=
-  transf_partial_fundef transf_function f. (* TODO: do we need to check the size here ? (issue only in proofs) *)
+  transf_partial_fundef transf_function f.
 
 Definition transf_program (p: Machblock.program) : res Asmblock.program :=
   transform_partial_program transf_fundef p.
diff --git a/aarch64/Asmblockgenproof0.v b/aarch64/Asmblockgenproof0.v
index 4217f526..03d863a3 100644
--- a/aarch64/Asmblockgenproof0.v
+++ b/aarch64/Asmblockgenproof0.v
@@ -37,7 +37,6 @@ Require Import Asmblock.
 Require Import Asmblockgen.
 Require Import Conventions1.
 Require Import Axioms.
-Require Import Machblockgenproof. (* FIXME: only use to import [is_tail_app] and [is_tail_app_inv] *)
 Require Import Asmblockprops.
 
 Module MB:=Machblock.
diff --git a/aarch64/Asmblockgenproof1.v b/aarch64/Asmblockgenproof1.v
index 754b49d6..61d77881 100644
--- a/aarch64/Asmblockgenproof1.v
+++ b/aarch64/Asmblockgenproof1.v
@@ -896,8 +896,8 @@ Ltac TranslOpBase :=
 Lemma compare_int_spec: forall rs v1 v2,
   let rs' := compare_int rs v1 v2 in
      rs'#CN = (Val.negative (Val.sub v1 v2))
-  /\ rs'#CZ = (Val_cmpu Ceq v1 v2)
-  /\ rs'#CC = (Val_cmpu Cge v1 v2)
+  /\ rs'#CZ = (Val.mxcmpu Ceq v1 v2)
+  /\ rs'#CC = (Val.mxcmpu Cge v1 v2)
   /\ rs'#CV = (Val.sub_overflow v1 v2).
 Proof.
   intros; unfold rs'; auto.
@@ -912,7 +912,7 @@ Proof.
   unfold eval_testcond; rewrite B, C, D, E.
   destruct v1; try discriminate; destruct v2; try discriminate.
   simpl in H; inv H.
-  unfold Val_cmpu; simpl. destruct c; simpl.
+  unfold Val.mxcmpu; simpl. destruct c; simpl.
   - destruct (Int.eq i i0); auto.
   - destruct (Int.eq i i0); auto.
   - rewrite Int.lt_sub_overflow. destruct (Int.lt i i0); auto.
@@ -924,7 +924,7 @@ Proof.
 Qed.
 
 Lemma eval_testcond_compare_uint: forall c v1 v2 b rs,
-  Val_cmpu_bool c v1 v2 = Some b ->
+  Val.mxcmpu_bool c v1 v2 = Some b ->
   eval_testcond (cond_for_unsigned_cmp c) (compare_int rs v1 v2) = Some b.
 Proof.
   intros. generalize (compare_int_spec rs v1 v2). 
@@ -932,7 +932,7 @@ Proof.
   unfold eval_testcond; rewrite B, C, D, E.
   destruct v1; try discriminate; destruct v2; try discriminate.
   simpl in H; inv H.
-  unfold Val_cmpu; simpl. destruct c; simpl.
+  unfold Val.mxcmpu; simpl. destruct c; simpl.
   - destruct (Int.eq i i0); auto.
   - destruct (Int.eq i i0); auto.
   - destruct (Int.ltu i i0); auto.
@@ -944,8 +944,8 @@ Qed.
 Lemma compare_long_spec: forall rs v1 v2,
   let rs' := compare_long rs v1 v2 in
      rs'#CN = (Val.negativel (Val.subl v1 v2))
-  /\ rs'#CZ = (Val_cmplu Ceq v1 v2)
-  /\ rs'#CC = (Val_cmplu Cge v1 v2)
+  /\ rs'#CZ = (Val.mxcmplu Ceq v1 v2)
+  /\ rs'#CC = (Val.mxcmplu Cge v1 v2)
   /\ rs'#CV = (Val.subl_overflow v1 v2).
 Proof.
   intros; unfold rs'; auto.
@@ -977,7 +977,7 @@ Proof.
   unfold eval_testcond; rewrite B, C, D, E.
   destruct v1; try discriminate; destruct v2; try discriminate.
   simpl in H; inv H.
-  unfold Val_cmplu; simpl. destruct c; simpl.
+  unfold Val.mxcmplu; simpl. destruct c; simpl.
   - destruct (Int64.eq i i0); auto.
   - destruct (Int64.eq i i0); auto.
   - rewrite int64_sub_overflow. destruct (Int64.lt i i0); auto.
@@ -989,12 +989,12 @@ Proof.
 Qed.
 
 Lemma eval_testcond_compare_ulong: forall c v1 v2 b rs,
-  Val_cmplu_bool c v1 v2 = Some b ->
+  Val.mxcmplu_bool c v1 v2 = Some b ->
   eval_testcond (cond_for_unsigned_cmp c) (compare_long rs v1 v2) = Some b.
 Proof.
   intros. generalize (compare_long_spec rs v1 v2). 
   set (rs' := compare_long rs v1 v2). intros (B & C & D & E).
-  unfold eval_testcond; rewrite B, C, D, E; unfold Val_cmplu.
+  unfold eval_testcond; rewrite B, C, D, E; unfold Val.mxcmplu.
   destruct v1; try discriminate; destruct v2; try discriminate; simpl in H.
   - (* int-int *)
     inv H. destruct c; simpl.
@@ -1207,7 +1207,7 @@ Proof.
   - (* Ccomplu *)
     econstructor; split. apply exec_straight_one. simpl; eauto.
     split; intros. apply eval_testcond_compare_ulong; auto.
-    erewrite Val_cmplu_bool_correct; eauto.
+    erewrite Val.mxcmplu_bool_correct; eauto.
     destruct r; reflexivity || discriminate.
   - (* Ccomplimm *)
     destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))].
@@ -1228,19 +1228,19 @@ Proof.
     destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))].
     + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
       split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_ulong; auto.
-      erewrite Val_cmplu_bool_correct; eauto.
+      erewrite Val.mxcmplu_bool_correct; eauto.
       destruct r; reflexivity || discriminate.
     + econstructor; split.
       apply exec_straight_one. simpl. rewrite Int64.repr_unsigned, Int64.neg_involutive. eauto.
       split; intros. apply eval_testcond_compare_ulong; auto.
-      erewrite Val_cmplu_bool_correct; eauto.
+      erewrite Val.mxcmplu_bool_correct; eauto.
       destruct r; reflexivity || discriminate.
     + exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C).
       econstructor; split.
       eapply exec_straight_trans. eexact A. apply exec_straight_one.
       simpl. rewrite B, C by eauto with asmgen. eauto.
       split; intros. apply eval_testcond_compare_ulong; auto.
-      erewrite Val_cmplu_bool_correct; eauto. 
+      erewrite Val.mxcmplu_bool_correct; eauto. 
       transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
   - (* Ccomplshift *)
     econstructor; split. apply exec_straight_one. simpl; eauto.
@@ -1249,7 +1249,7 @@ Proof.
   - (* Ccomplushift *)
     econstructor; split. apply exec_straight_one. simpl; eauto.
     split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_ulong; auto.
-    erewrite Val_cmplu_bool_correct; eauto. 
+    erewrite Val.mxcmplu_bool_correct; eauto. 
     destruct r; reflexivity || discriminate.
   - (* Cmasklzero *)
     destruct (is_logical_imm64 n).
@@ -1368,7 +1368,7 @@ Local Opaque transl_cond transl_cond_branch_default.
     apply Int.same_if_eq in N0; subst n; ArgsInv.
     + (* Ccompuimm Cne 0 *)
       econstructor; split. econstructor.
-      split; auto. simpl. apply Val_cmpu_bool_correct in EV.
+      split; auto. simpl. apply Val.mxcmpu_bool_correct in EV.
       unfold incrPC. Simpl. rewrite EV. auto.
     + (* Ccompuimm Ceq 0 *)
       monadInv TR. ArgsInv. simpl in *.
@@ -1408,7 +1408,7 @@ Local Opaque transl_cond transl_cond_branch_default.
     apply Int64.same_if_eq in N0; subst n; ArgsInv.
     + (* Ccompluimm Cne 0 *)
       econstructor; split. econstructor.
-      split; auto. simpl. apply Val_cmplu_bool_correct in EV.
+      split; auto. simpl. apply Val.mxcmplu_bool_correct in EV.
       unfold incrPC. Simpl. rewrite EV. auto.
     + (* Ccompluimm Ceq 0 *)
       econstructor; split. econstructor.
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index cec8ea69..a33f90b3 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -23,7 +23,7 @@ Require Machblockgenproof Asmblockgenproof PostpassSchedulingproof.
 Require Import Asmgen.
 Require Import Axioms.
 Require Import IterList.
-Require Import Ring.
+Require Import Ring Lia.
 
 Module Asmblock_PRESERVATION.
 
@@ -107,7 +107,7 @@ Proof.
   destruct (zlt _ _); try congruence.
   inv EQ. inv EQ0.
   eexists; intuition eauto.
-  omega.
+  lia.
 Qed.
 
 
@@ -220,14 +220,14 @@ Proof.
   - inversion TRANSf.
   - unfold max_pos.
     assert (Asm.fn_code tf = c) as H. { inversion TRANSf as (H'); auto. }
-    rewrite H; omega.
+    rewrite H; lia.
 Qed.
 
 Lemma one_le_max_unsigned:
   1 <= Ptrofs.max_unsigned.
 Proof.
   unfold Ptrofs.max_unsigned; simpl; unfold Ptrofs.wordsize;
-  unfold Wordsize_Ptrofs.wordsize; destruct Archi.ptr64; simpl; omega.
+  unfold Wordsize_Ptrofs.wordsize; destruct Archi.ptr64; simpl; lia.
 Qed.
 
 (* NB: does not seem useful anymore, with the [exec_header_simulation] proof below
@@ -256,7 +256,7 @@ Proof.
       * apply one_le_max_unsigned.
     + split.
       * apply Z.ge_le; assumption.
-      * rewrite <- functions_bound_max_pos; eauto; omega.
+      * rewrite <- functions_bound_max_pos; eauto; lia.
 Qed.
 *)
 
@@ -287,16 +287,16 @@ Lemma list_length_z_aux_increase A (l: list A): forall acc,
   list_length_z_aux l acc >= acc.
 Proof.
   induction l; simpl; intros.
-  - omega.
-  - generalize (IHl (Z.succ acc)). omega.
+  - lia.
+  - generalize (IHl (Z.succ acc)). lia.
 Qed.
 
 Lemma bblock_size_aux_pos bb: list_length_z (body bb) + Z.of_nat (length_opt (exit bb)) >= 1.
 Proof.
   destruct (bblock_non_empty bb), (body bb) as [|hd tl], (exit bb); simpl;
-  try (congruence || omega);
+  try (congruence || lia);
   unfold list_length_z; simpl;
-  generalize (list_length_z_aux_increase _ tl 1); omega.
+  generalize (list_length_z_aux_increase _ tl 1); lia.
 Qed.
 
 
@@ -306,7 +306,7 @@ Proof.
     unfold list_length_z, list_length_z_aux. simpl.
     fold list_length_z_aux.
     rewrite (list_length_z_aux_shift l acc 0).
-    omega.
+    lia.
 Qed.
 
 Lemma list_length_z_cons A hd (tl : list A):
@@ -315,14 +315,6 @@ Proof.
   unfold list_length_z; simpl; rewrite list_length_add_acc; reflexivity.
 Qed.
 
-(*Lemma length_agree A (l : list A):*)
-  (*list_length_z l = Z.of_nat (length l).*)
-(*Proof.*)
-  (*induction l as [| ? l IH]; intros.*)
-  (*- unfold list_length_z; reflexivity.*)
-  (*- simpl; rewrite list_length_z_cons, Zpos_P_of_succ_nat; omega.*)
-(*Qed.*)
-
 Lemma bblock_size_aux bb: size bb = list_length_z (header bb) + list_length_z (body bb) + Z.of_nat (length_opt (exit bb)).
 Proof.
   unfold size.
@@ -335,14 +327,14 @@ Proof.
   rewrite bblock_size_aux.
   generalize (bblock_non_empty bb); intros NEMPTY; destruct NEMPTY as [HDR|EXIT].
   - destruct (body bb); try contradiction; rewrite list_length_z_cons;
-    repeat rewrite list_length_z_nat; omega.
-  - destruct (exit bb); try contradiction; simpl; repeat rewrite list_length_z_nat; omega.
+    repeat rewrite list_length_z_nat; lia.
+  - destruct (exit bb); try contradiction; simpl; repeat rewrite list_length_z_nat; lia.
 Qed.
 
 Lemma body_size_le_block_size bb:
   list_length_z (body bb) <= size bb.
 Proof.
-  rewrite bblock_size_aux; repeat rewrite list_length_z_nat; omega.
+  rewrite bblock_size_aux; repeat rewrite list_length_z_nat; lia.
 Qed.
 
 
@@ -351,7 +343,7 @@ Proof.
   rewrite (bblock_size_aux bb).
   generalize (bblock_size_aux_pos bb).
   generalize (list_length_z_pos (header bb)).
-  omega.
+  lia.
 Qed.
 
 Lemma unfold_car_cdr bb bbs tc:
@@ -470,7 +462,7 @@ Lemma list_nth_z_neg A (l: list A): forall n,
   n < 0 -> list_nth_z l n = None.
 Proof.
   induction l; simpl; auto.
-  intros n H; destruct (zeq _ _); (try eapply IHl); omega.
+  intros n H; destruct (zeq _ _); (try eapply IHl); lia.
 Qed.
 
 Lemma find_bblock_neg bbs: forall pos,
@@ -539,12 +531,12 @@ Proof.
     + inv FINDBB.
       exploit bblock_size_preserved; eauto; intros SIZE; rewrite SIZE.
       repeat (rewrite list_length_z_nat). rewrite app_length, Nat2Z.inj_add.
-      omega.
+      lia.
     + generalize (IHbbs tbbs' (pos - size bb) bb' FINDBB UNFOLD). intros IH.
       exploit bblock_size_preserved; eauto; intros SIZE.
       repeat (rewrite list_length_z_nat); rewrite app_length.
       rewrite Nat2Z.inj_add; repeat (rewrite <- list_length_z_nat).
-      omega.
+      lia.
 Qed.
 
 Lemma size_of_blocks_max_pos pos f tf bi:
@@ -565,7 +557,7 @@ Lemma unfold_bblock_not_nil bb:
 Proof.
   intros.
   exploit bblock_size_preserved; eauto. unfold list_length_z; simpl. intros SIZE.
-  generalize (bblock_size_pos bb). intros SIZE'. omega.
+  generalize (bblock_size_pos bb). intros SIZE'. lia.
 Qed.
 
 (* same proof as list_nth_z_range (Coqlib) *)
@@ -576,8 +568,8 @@ Proof.
   induction c; simpl; intros.
   discriminate.
   rewrite list_length_z_cons. destruct (zeq n 0).
-  generalize (list_length_z_pos c); omega.
-  exploit IHc; eauto. omega.
+  generalize (list_length_z_pos c); lia.
+  exploit IHc; eauto. lia.
 Qed.
 
 Lemma find_instr_tail:
@@ -590,8 +582,8 @@ Proof.
   - intros. rewrite list_length_z_cons. simpl.
     destruct (zeq (pos + (list_length_z tbb + 1)) 0).
     + exploit find_instr_range; eauto. intros POS_RANGE.
-      generalize (list_length_z_pos tbb). omega.
-    + replace (pos + (list_length_z tbb + 1) - 1) with (pos + list_length_z tbb) by omega.
+      generalize (list_length_z_pos tbb). lia.
+    + replace (pos + (list_length_z tbb + 1) - 1) with (pos + list_length_z tbb) by lia.
       eapply IHtbb; eauto.
 Qed.
 
@@ -604,7 +596,7 @@ Proof.
   intros (tf & _ & TRANSf).
   assert (pos + size bi <= max_pos tf). { eapply size_of_blocks_max_pos; eauto. }
   assert (max_pos tf <= Ptrofs.max_unsigned). { eapply functions_bound_max_pos; eauto. }
-  omega.
+  lia.
 Qed.
 
 Lemma find_instr_bblock_tail:
@@ -619,10 +611,10 @@ Proof.
      destruct (zeq (pos + size bb) 0).
      + (* absurd *)
        exploit find_instr_range; eauto. intros POS_RANGE.
-       generalize (bblock_size_pos bb). intros SIZE. omega.
+       generalize (bblock_size_pos bb). intros SIZE. lia.
      + erewrite bblock_size_preserved; eauto.
        rewrite list_length_z_cons.
-       replace (pos + (list_length_z tbb + 1) - 1) with (pos + list_length_z tbb) by omega.
+       replace (pos + (list_length_z tbb + 1) - 1) with (pos + list_length_z tbb) by lia.
        apply find_instr_tail; auto.
 Qed.
 
@@ -671,14 +663,14 @@ Lemma list_nth_z_find_bi_with_header:
 Proof.
   induction ll.
   - unfold list_length_z. simpl. intros.
-    replace (n - 0) with n in H by omega. eapply list_nth_z_find_bi; eauto.
+    replace (n - 0) with n in H by lia. eapply list_nth_z_find_bi; eauto.
   - intros. simpl. destruct (zeq n 0).
     + rewrite list_length_z_cons in H. rewrite e in H.
-      replace (0 - (list_length_z ll + 1)) with (-1 - (list_length_z ll)) in H by omega.
+      replace (0 - (list_length_z ll + 1)) with (-1 - (list_length_z ll)) in H by lia.
       generalize (list_length_z_pos ll). intros.
-      rewrite list_nth_z_neg in H; try omega. inversion H.
+      rewrite list_nth_z_neg in H; try lia. inversion H.
     + rewrite list_length_z_cons in H.
-      replace (n - (list_length_z ll + 1)) with (n -1 - (list_length_z ll)) in H by omega.
+      replace (n - (list_length_z ll + 1)) with (n -1 - (list_length_z ll)) in H by lia.
       eapply IHll; eauto.
 Qed.
 
@@ -689,13 +681,13 @@ Lemma range_list_nth_z:
   exists x, list_nth_z l n = Some x.
 Proof.
   induction l.
-  - intros. unfold list_length_z in H. simpl in H. omega.
+  - intros. unfold list_length_z in H. simpl in H. lia.
   - intros n. destruct (zeq n 0).
     + intros. simpl. destruct (zeq n 0). { eauto. } contradiction.
     + intros H. rewrite list_length_z_cons in H.
       simpl. destruct (zeq n 0). { contradiction. }
-      replace (Z.pred n) with (n - 1) by omega.
-      eapply IHl; omega.
+      replace (Z.pred n) with (n - 1) by lia.
+      eapply IHl; lia.
 Qed.
 
 Lemma list_nth_z_n_too_big:
@@ -705,17 +697,17 @@ Lemma list_nth_z_n_too_big:
   n >= list_length_z l.
 Proof.
   induction l.
-  - intros. unfold list_length_z. simpl. omega.
+  - intros. unfold list_length_z. simpl. lia.
   - intros. rewrite list_length_z_cons.
     simpl in H0.
     destruct (zeq n 0) as [N | N].
     + inversion H0.
     + (* XXX there must be a more elegant way to prove this simple fact *)
-      assert (n > 0). { omega. }
-      assert (0 <= n - 1). { omega. }
+      assert (n > 0). { lia. }
+      assert (0 <= n - 1). { lia. }
       generalize (IHl (n - 1)). intros IH.
       assert (n - 1 >= list_length_z l). { auto. }
-      assert (n > list_length_z l); omega.
+      assert (n > list_length_z l); lia.
 Qed.
 
 Lemma find_instr_past_header:
@@ -729,9 +721,9 @@ Proof.
   - intros. simpl. destruct (zeq n 0) as [N | N].
     + rewrite N in H. inversion H.
     + rewrite list_length_z_cons.
-      replace (n - (list_length_z labels' + 1)) with (n - 1 - list_length_z labels') by omega.
+      replace (n - (list_length_z labels' + 1)) with (n - 1 - list_length_z labels') by lia.
       simpl in H. destruct (zeq n 0). { contradiction. }
-      replace (Z.pred n) with (n - 1) in H by omega.
+      replace (Z.pred n) with (n - 1) in H by lia.
       apply IH; auto.
 Qed.
 
@@ -753,9 +745,9 @@ Proof.
     simpl; destruct (zeq n 0) as [N|N].
     + rewrite N in NTH; inversion NTH.
     + rewrite list_length_z_cons.
-      replace (n - (list_length_z lbi + 1)) with (n - 1 - list_length_z lbi) by omega.
+      replace (n - (list_length_z lbi + 1)) with (n - 1 - list_length_z lbi) by lia.
       simpl in NTH. destruct (zeq n 0). { contradiction. }
-      replace (Z.pred n) with (n - 1)  in NTH by omega.
+      replace (Z.pred n) with (n - 1)  in NTH by lia.
       apply IHlbi; auto.
 Qed.
 
@@ -767,15 +759,15 @@ Lemma n_beyond_body:
   n >= Z.of_nat (length (header bb) + length (body bb)).
 Proof.
   intros.
-  assert (0 <= n). { omega. }
+  assert (0 <= n). { lia. }
   generalize (list_nth_z_n_too_big label (header bb) n H2 H0). intros.
   generalize (list_nth_z_n_too_big _ (body bb) (n - list_length_z (header bb))). intros.
   unfold size in H.
 
-  assert (0 <= n - list_length_z (header bb)). { omega. }
+  assert (0 <= n - list_length_z (header bb)). { lia. }
   assert (n - list_length_z (header bb) >= list_length_z (body bb)). { apply H4; auto. }
 
-  assert (n >= list_length_z (header bb) + list_length_z (body bb)). { omega. }
+  assert (n >= list_length_z (header bb) + list_length_z (body bb)). { lia. }
   rewrite Nat2Z.inj_add.
   repeat (rewrite <- list_length_z_nat). assumption.
 Qed.
@@ -910,20 +902,20 @@ Proof.
               repeat (rewrite Nat2Z.inj_add in UPPER).
               repeat (rewrite <- list_length_z_nat in UPPER). repeat (rewrite Nat2Z.inj_add in NGE).
               repeat (rewrite <- list_length_z_nat in NGE). simpl in UPPER.
-              assert (n = list_length_z (header bb) + list_length_z (body bb)). { omega. }
+              assert (n = list_length_z (header bb) + list_length_z (body bb)). { lia. }
               assert (n = size bb - 1). {
                 unfold size. rewrite <- EXIT. simpl.
-                repeat (rewrite Nat2Z.inj_add). repeat (rewrite <- list_length_z_nat). simpl. omega.
+                repeat (rewrite Nat2Z.inj_add). repeat (rewrite <- list_length_z_nat). simpl. lia.
               }
               symmetry in EXIT.
               eexists; split.
               ** eapply is_nth_ctlflow; eauto.
               ** simpl.
                  destruct (zeq (n - list_length_z (header bb) - list_length_z (body bb)) 0). { reflexivity. }
-                 (* absurd *) omega.
+                 (* absurd *) lia.
            ++ (* absurd *)
               unfold size in SIZE. rewrite <- EXIT in SIZE. simpl in SIZE.
-              destruct SIZE as (? & SIZE'). rewrite Nat.add_0_r in SIZE'. omega.
+              destruct SIZE as (? & SIZE'). rewrite Nat.add_0_r in SIZE'. lia.
     + unfold find_bblock in FINDBB; simpl in FINDBB; fold find_bblock in FINDBB.
       inversion UNFOLD as (UNFOLD').
       apply bind_inversion in UNFOLD'. destruct UNFOLD' as (? & (UNFOLD_BBLOCK' & UNFOLD')).
@@ -933,9 +925,9 @@ Proof.
       destruct IH as (? & (IH_is_nth & IH_find_instr)); eauto.
       eexists; split.
       * apply IH_is_nth.
-      * replace (Z.pos p + n) with (Z.pos p + n - size b + size b) by omega.
+      * replace (Z.pos p + n) with (Z.pos p + n - size b + size b) by lia.
         eapply find_instr_bblock_tail; try assumption.
-        replace (Z.pos p + n - size b) with (Z.pos p - size b + n) by omega.
+        replace (Z.pos p + n - size b) with (Z.pos p - size b + n) by lia.
         apply IH_find_instr.
     + (* absurd *)
       generalize (Pos2Z.neg_is_neg p). intros. exploit (find_bblock_neg (b :: lb)); eauto.
@@ -963,11 +955,11 @@ Proof.
   + (* header one *)
     assert (Lhead: list_length_z (header bb) = 1). { rewrite EQhead; unfold list_length_z; simpl. auto. }
     exploit (find_instr_bblock 0); eauto.
-    { generalize (bblock_size_pos bb). omega. }
+    { generalize (bblock_size_pos bb). lia. }
     intros (i & NTH & FIND_INSTR).
     inv NTH.
     * rewrite EQhead in H; simpl in H. inv H.
-      replace (Ptrofs.unsigned ofs + 0) with (Ptrofs.unsigned ofs) in FIND_INSTR by omega.
+      replace (Ptrofs.unsigned ofs + 0) with (Ptrofs.unsigned ofs) in FIND_INSTR by lia.
       eexists. split.
       - eapply star_one.
         eapply Asm.exec_step_internal; eauto.
@@ -975,12 +967,12 @@ Proof.
       - unfold list_length_z; simpl. split; eauto.
         intros r; destruct r; simpl; congruence || auto.
     * (* absurd case *)
-      erewrite list_nth_z_neg in * |-; [ congruence | rewrite Lhead; omega].
+      erewrite list_nth_z_neg in * |-; [ congruence | rewrite Lhead; lia].
     * (* absurd case *)
-      rewrite bblock_size_aux, Lhead in *. generalize (bblock_size_aux_pos bb). omega.
+      rewrite bblock_size_aux, Lhead in *. generalize (bblock_size_aux_pos bb). lia.
   + (* absurd case *)
     unfold list_length_z in BNDhead. simpl in *.
-    generalize (list_length_z_aux_increase _ l1 2); omega.
+    generalize (list_length_z_aux_increase _ l1 2); lia.
 Qed.
 
 Lemma eval_addressing_preserved a rs1 rs2:
@@ -1406,57 +1398,18 @@ Proof.
   assert (tc' = tc) by congruence; subst.
     exploit (find_instr_bblock (list_length_z (header bb) + Z.of_nat n)); eauto.
     { unfold size; split.
-      - rewrite list_length_z_nat; omega.
-      - repeat (rewrite list_length_z_nat). repeat (rewrite Nat2Z.inj_add). omega. }
+      - rewrite list_length_z_nat; lia.
+      - repeat (rewrite list_length_z_nat). repeat (rewrite Nat2Z.inj_add). lia. }
     intros (i & NTH & FIND_INSTR).
     exists i; intros.
     inv NTH.
-    - (* absurd *) apply list_nth_z_range in H; omega.
+    - (* absurd *) apply list_nth_z_range in H; lia.
     - exists bi;
       rewrite Z.add_simpl_l in H;
       rewrite Z.add_assoc in FIND_INSTR;
       intuition.
     - (* absurd *) rewrite bblock_size_aux in H0;
-      rewrite H in H0; simpl in H0; repeat rewrite list_length_z_nat in H0; omega.
-Qed.
-
-(** "is_tail" auxiliary lemma about is_tail to move in IterList ou Coqlib (déplacer aussi Machblockgenproof.is_tail_app_inv) ? *)
-
-Lemma is_tail_app_right A (l2 l1: list A): is_tail l1 (l2++l1).
-Proof.
-  intros; eapply Machblockgenproof.is_tail_app_inv; econstructor.
-Qed.
-
-Lemma is_tail_app_def A (l1 l2: list A):
-  is_tail l1 l2 -> exists l3, l2 = l3 ++ l1.
-Proof.
-  induction 1 as [|x l1 l2]; simpl.
-  - exists nil; simpl; auto.
-  - destruct IHis_tail as (l3 & EQ); rewrite EQ.
-    exists (x::l3); simpl; auto.
-Qed.
-
-Lemma is_tail_bound A (l1 l2: list A):
-  is_tail l1 l2 -> (length l1 <= length l2)%nat.
-Proof.
-  intros H; destruct (is_tail_app_def _ _ _ H) as (l3 & EQ).
-  subst; rewrite app_length.
-  omega.
-Qed.
-
-Lemma is_tail_list_nth_z A (l1 l2: list A):
-  is_tail l1 l2 -> list_nth_z l2 ((list_length_z l2) - (list_length_z l1)) = list_nth_z l1 0.
-Proof.
-  induction 1; simpl.
-  - replace (list_length_z c - list_length_z c) with 0; omega || auto.
-  - assert (X: list_length_z (i :: c2) > list_length_z c1).
-    { rewrite !list_length_z_nat, <- Nat2Z.inj_gt.
-      exploit is_tail_bound; simpl; eauto.
-      omega. }
-    destruct (zeq (list_length_z (i :: c2) - list_length_z c1) 0) as [Y|Y]; try omega.
-    replace (Z.pred (list_length_z (i :: c2) - list_length_z c1)) with (list_length_z c2 - list_length_z c1); auto.
-    rewrite list_length_z_cons.
-    omega.
+      rewrite H in H0; simpl in H0; repeat rewrite list_length_z_nat in H0; lia.
 Qed.
 
 (* TODO: remplacer find_basic_instructions directement par ce lemme ? *)
@@ -1474,9 +1427,9 @@ Lemma find_basic_instructions_alt b ofs f bb tc n: forall
                      = Some i.
 Proof.
   intros; assert ((Z.to_nat n) < length (body bb))%nat.
-  { rewrite Nat2Z.inj_lt, <- list_length_z_nat, Z2Nat.id; try omega. }
+  { rewrite Nat2Z.inj_lt, <- list_length_z_nat, Z2Nat.id; try lia. }
   exploit find_basic_instructions; eauto.
-  rewrite Z2Nat.id; try omega. intros (i & bi & X).
+  rewrite Z2Nat.id; try lia. intros (i & bi & X).
   eexists; eexists; intuition eauto.
 Qed.
 
@@ -1491,11 +1444,11 @@ Proof.
   assert (HBBPOS: list_length_z (header bb) >= 0) by eapply list_length_z_pos.
   assert (HBBSIZE: list_length_z (header bb) < size bb) by eapply header_size_lt_block_size.
   assert (OFSBOUND: 0 <= Ptrofs.unsigned ofs <= Ptrofs.max_unsigned) by eapply Ptrofs.unsigned_range_2.
-  assert (BBSIZE: size bb <= Ptrofs.max_unsigned) by omega.
+  assert (BBSIZE: size bb <= Ptrofs.max_unsigned) by lia.
   unfold size in BBSIZE.
   rewrite !Nat2Z.inj_add in BBSIZE.
   rewrite <- !list_length_z_nat in BBSIZE.
-  omega.
+  lia.
 Qed.
 
 (* A more general version of the exec_body_simulation_plus lemma below.
@@ -1515,9 +1468,9 @@ Proof.
   induction li as [|a li]; simpl; try congruence.
   intros.
   assert (BDYLENPOS: 0 <= (list_length_z (body bb) - list_length_z (a::li)) < list_length_z (body bb)). {
-    assert (Z.of_nat O < list_length_z (a::li) <= list_length_z (body bb)); try omega.
+    assert (Z.of_nat O < list_length_z (a::li) <= list_length_z (body bb)); try lia.
     rewrite !list_length_z_nat; split.
-    - rewrite <- Nat2Z.inj_lt. simpl. omega.
+    - rewrite <- Nat2Z.inj_lt. simpl. lia.
     - rewrite <- Nat2Z.inj_le; eapply is_tail_bound; eauto.
   }
   exploit internal_functions_unfold; eauto.
@@ -1549,18 +1502,18 @@ Proof.
   exploit (Asm.exec_step_internal tge b); eauto.
   {
     rewrite Ptrofs.add_unsigned.
-    repeat (rewrite Ptrofs.unsigned_repr); try omega.
+    repeat (rewrite Ptrofs.unsigned_repr); try lia.
     2: {
       assert (BOUNDOFS: 0 <= Ptrofs.unsigned ofs <= Ptrofs.max_unsigned) by eapply Ptrofs.unsigned_range_2.
       assert (list_length_z (body bb) <= size bb) by eapply body_size_le_block_size.
       assert (list_length_z (header bb) <= 1). { eapply size_header; eauto. }
-      omega. }
+      lia. }
     try rewrite list_length_z_nat; try split;
     simpl; rewrite <- !list_length_z_nat;
     replace (Ptrofs.unsigned ofs + (list_length_z (header bb) + list_length_z (body bb) -
       list_length_z (a :: li))) with (Ptrofs.unsigned ofs + list_length_z (header bb) +
-      (list_length_z (body bb) - list_length_z (a :: li))) by omega;
-    try assumption; try omega. }
+      (list_length_z (body bb) - list_length_z (a :: li))) by lia;
+    try assumption; try lia. }
 
   (* This is our STEP hypothesis. *)
   intros STEP_NEXT.
@@ -1574,18 +1527,18 @@ Proof.
       apply f_equal.
       apply f_equal.
       rewrite bblock_size_aux, list_length_z_cons; simpl.
-      omega.
+      lia.
   - exploit (IHli b ofs f bb rs1 m_next' (State rs_next' m_next')); congruence || eauto.
     + exploit is_tail_app_def; eauto.
       intros (l3 & EQ); rewrite EQ.
-      exploit (is_tail_app_right _ (l3 ++ a::nil)).
+      exploit (is_tail_app_right (l3 ++ a::nil)).
       rewrite <- app_assoc; simpl; eauto.
     + constructor; auto.
       rewrite ATPC_NEXT.
       apply f_equal.
       apply f_equal.
       rewrite! list_length_z_cons; simpl.
-      omega.
+      lia.
     + intros (s2' & LAST_STEPS & LAST_MATCHS).
       eexists. split; eauto.
       eapply plus_left'; eauto.
@@ -1605,7 +1558,7 @@ Proof.
   exploit exec_body_simulation_plus_gen; eauto.
   - constructor.
   - replace (list_length_z (header bb) + list_length_z (body bb) - list_length_z (body bb)) with (list_length_z (header bb)); auto.
-    omega.
+    lia.
 Qed.
 
 Lemma exec_body_simulation_star b ofs f bb rs m s2 rs' m': forall
@@ -1623,7 +1576,7 @@ Proof.
     eexists. split.
     eapply star_refl; eauto.
     assert (EQ: (size bb - Z.of_nat (length_opt (exit bb))) = list_length_z (header bb)).
-    {  rewrite bblock_size_aux. rewrite Hbb; unfold list_length_z; simpl. omega. }
+    {  rewrite bblock_size_aux. rewrite Hbb; unfold list_length_z; simpl. lia. }
     rewrite EQ; eauto.
   - exploit exec_body_simulation_plus; congruence || eauto.
     { rewrite Hbb; eauto. }
@@ -1639,7 +1592,7 @@ Proof.
   intros N.
   remember (list_nth_z l n) as opt eqn:H. symmetry in H.
   destruct opt; auto.
-  exploit list_nth_z_range; eauto. omega.
+  exploit list_nth_z_range; eauto. lia.
 Qed.
 
 Lemma label_in_header_list lbl a:
@@ -1651,9 +1604,9 @@ Proof.
   - eapply in_nil in H. contradiction.
   - rewrite list_length_z_cons in H0.
     assert (list_length_z l0 >= 0) by eapply list_length_z_pos.
-    assert (list_length_z l0 = 0) by omega.
+    assert (list_length_z l0 = 0) by lia.
     rewrite list_length_z_nat in H2.
-    assert (Datatypes.length l0 = 0%nat) by omega.
+    assert (Datatypes.length l0 = 0%nat) by lia.
     eapply length_zero_iff_nil in H3. subst.
     unfold In in H. destruct H.
     + subst; eauto.
@@ -1684,7 +1637,7 @@ Proof.
   - intros. inversion HUNF; clear HUNF. monadInv H0. simpl in *.
     erewrite no_label_in_basic_inst; eauto. rewrite <- IHbdy; eauto.
     erewrite Zpos_P_of_succ_nat.
-    apply f_equal2; auto. omega.
+    apply f_equal2; auto. lia.
 Qed.
 
 Lemma asm_label_pos_header: forall z a x0 x1 lbl
@@ -1696,7 +1649,7 @@ Proof.
   unfold size.
   rewrite <- plus_assoc. rewrite Nat2Z.inj_add.
   rewrite list_length_z_nat.
-  replace (z + (Z.of_nat (Datatypes.length (header a)) + Z.of_nat (Datatypes.length (body a) + length_opt (exit a)))) with (z + Z.of_nat (Datatypes.length (header a)) + Z.of_nat (Datatypes.length (body a) + length_opt (exit a))) by omega.
+  replace (z + (Z.of_nat (Datatypes.length (header a)) + Z.of_nat (Datatypes.length (body a) + length_opt (exit a)))) with (z + Z.of_nat (Datatypes.length (header a)) + Z.of_nat (Datatypes.length (body a) + length_opt (exit a))) by lia.
   eapply (label_pos_body (body a) x0 x1 (z + Z.of_nat (Datatypes.length (header a))) (exit a) lbl). auto.
 Qed.
 
@@ -1707,8 +1660,8 @@ Proof.
   intros.
   destruct l1; try congruence. rewrite !list_length_z_cons in HSIZE.
   assert (list_length_z l1 >= 0) by eapply list_length_z_pos.
-  assert (list_length_z l1 + 1 + 1 >= 2) by omega.
-  assert (2 <= 1) by omega. contradiction H1. omega.
+  assert (list_length_z l1 + 1 + 1 >= 2) by lia.
+  assert (2 <= 1) by lia. contradiction H1. lia.
 Qed.
 
 Lemma label_pos_preserved_gen bbs: forall lbl c z
@@ -1727,7 +1680,7 @@ Proof.
       unfold is_label in *.
       destruct (header a).
       * replace (z + list_length_z (@nil label)) with (z); eauto.
-        unfold list_length_z. simpl. omega.
+        unfold list_length_z. simpl. lia.
       * eapply header_size_cons_nil in l as HL1.
         subst. simpl in *. destruct (in_dec _ _); try congruence.
         simpl in *.
@@ -1782,7 +1735,7 @@ Proof.
   intros; simpl in *; unfold incrPC in NEXT;
   inv_matchi;
   assert (size bb >= 1) by eapply bblock_size_pos;
-  assert (0 <= size bb - 1 <= Ptrofs.max_unsigned) by omega;
+  assert (0 <= size bb - 1 <= Ptrofs.max_unsigned) by lia;
   inversion NEXT; subst;
   eexists; eexists; split; eauto.
   assert (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size bb))) = Asm.nextinstr rs2). {
@@ -1790,9 +1743,9 @@ Proof.
     intros x. destruct (PregEq.eq x PC).
     -- unfold Asm.nextinstr. rewrite <- AGPC.
        rewrite Val.offset_ptr_assoc. rewrite Ptrofs.add_unsigned.
-       rewrite (Ptrofs.unsigned_repr (size bb - 1)); try omega.
+       rewrite (Ptrofs.unsigned_repr (size bb - 1)); try lia.
        rewrite Ptrofs.unsigned_one.
-       replace (size bb - 1 + 1) with (size bb) by omega.
+       replace (size bb - 1 + 1) with (size bb) by lia.
        rewrite e. rewrite Pregmap.gss.
        reflexivity.
     -- eapply nextinstr_agree_but_pc; eauto. }
@@ -1850,8 +1803,8 @@ Proof.
       * rewrite symbol_addresses_preserved. reflexivity.
       * destruct (PregEq.eq x X30).
         -- inv MATCHI. rewrite <- AGPC. rewrite Val.offset_ptr_assoc.
-           unfold Ptrofs.add, Ptrofs.one. repeat (rewrite Ptrofs.unsigned_repr); try omega.
-           replace (size bb - 1 + 1) with (size bb) by omega. reflexivity.
+           unfold Ptrofs.add, Ptrofs.one. repeat (rewrite Ptrofs.unsigned_repr); try lia.
+           replace (size bb - 1 + 1) with (size bb) by lia. reflexivity.
         -- inv MATCHI; rewrite AG; try assumption; reflexivity.
     } rewrite EQRS; inv MATCHI; reflexivity.
   - (* Pbs *)
@@ -1877,7 +1830,7 @@ Proof.
       - destruct (PregEq.eq x X30) as [X' | X'].
         + inversion MATCHI; subst. rewrite <- AGPC.
           rewrite Val.offset_ptr_assoc. unfold Ptrofs.one.
-          rewrite Ptrofs.add_unsigned. rewrite Ptrofs.unsigned_repr; try omega. rewrite Ptrofs.unsigned_repr; try omega.
+          rewrite Ptrofs.add_unsigned. rewrite Ptrofs.unsigned_repr; try lia. rewrite Ptrofs.unsigned_repr; try lia.
           rewrite Z.sub_add; reflexivity.
         + inv_matchi.
     } rewrite EQRS. inv_matchi.
@@ -1961,10 +1914,10 @@ Lemma last_instruction_cannot_be_label bb:
   list_nth_z (header bb) (size bb - 1) = None.
 Proof.
   assert (list_length_z (header bb) <= size bb - 1). {
-    rewrite bblock_size_aux. generalize (bblock_size_aux_pos bb). omega.
+    rewrite bblock_size_aux. generalize (bblock_size_aux_pos bb). lia.
   }
   remember (list_nth_z (header bb) (size bb - 1)) as label_opt; destruct label_opt; auto;
-  exploit list_nth_z_range; eauto; omega.
+  exploit list_nth_z_range; eauto; lia.
 Qed.
 
 Lemma pc_ptr_exec_step: forall ofs bb b rs m _rs _m
@@ -1993,8 +1946,8 @@ Proof.
           with (Ptrofs.unsigned ofs + (size bb - 1)); try assumption.
   generalize (bblock_size_pos bb); generalize (Ptrofs.unsigned_range_2 ofs); intros.
   unfold Ptrofs.add.
-  rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr; try omega.
-  rewrite Ptrofs.unsigned_repr; omega.
+  rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr; try lia.
+  rewrite Ptrofs.unsigned_repr; lia.
 Qed.
 
 Lemma eval_builtin_arg_match: forall rs _m _rs a1 b1
@@ -2127,7 +2080,7 @@ Proof.
   intros (tc & FINDtf & TRANStf & _).
 
   exploit (find_instr_bblock (size bb - 1)); eauto.
-  { generalize (bblock_size_pos bb). omega. }
+  { generalize (bblock_size_pos bb). lia. }
   intros (i' & NTH & FIND_INSTR).
 
   inv NTH.
@@ -2136,12 +2089,12 @@ Proof.
     rewrite bblock_size_aux in *. rewrite NEMPTY_EXIT' in *. simpl in *.
     (* XXX: Is there a better way to simplify this expression i.e. automatically? *)
     replace (list_length_z (header bb) + list_length_z (body bb) + 1 - 1 -
-       list_length_z (header bb)) with (list_length_z (body bb)) in H by omega.
-    rewrite list_nth_z_range_exceeded in H; try omega. discriminate.
+       list_length_z (header bb)) with (list_length_z (body bb)) in H by lia.
+    rewrite list_nth_z_range_exceeded in H; try lia. discriminate.
   + assert (Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned). {
       eapply size_of_blocks_bounds; eauto.
     }
-    assert (size bb <= Ptrofs.max_unsigned). { generalize (Ptrofs.unsigned_range_2 ofs); omega. }
+    assert (size bb <= Ptrofs.max_unsigned). { generalize (Ptrofs.unsigned_range_2 ofs); lia. }
     destruct cfi.
     * (* control flow instruction *)
       destruct s2.
@@ -2179,9 +2132,9 @@ Proof.
         { rewrite <- AGPC. rewrite ATPC. unfold Val.offset_ptr.
           rewrite Ptrofs.add_assoc. unfold Ptrofs.add.
           assert (BBPOS: size bb >= 1) by eapply bblock_size_pos.
-          rewrite (Ptrofs.unsigned_repr (size bb - 1)); try omega.
+          rewrite (Ptrofs.unsigned_repr (size bb - 1)); try lia.
           rewrite Ptrofs.unsigned_one.
-          replace (size bb - 1 + 1) with (size bb) by omega.
+          replace (size bb - 1 + 1) with (size bb) by lia.
           reflexivity. }
         apply set_builtin_res_dont_move_pc_gen.
         -- erewrite !set_builtin_map_not_pc.
@@ -2216,7 +2169,7 @@ Proof.
         apply functional_extensionality. intros x.
         destruct (PregEq.eq x PC) as [X|].
         - rewrite X. rewrite <- AGPC. simpl.
-          replace (size bb - 0) with (size bb) by omega. reflexivity.
+          replace (size bb - 0) with (size bb) by lia. reflexivity.
         - rewrite AG; try assumption. reflexivity.
     }
     destruct X.
diff --git a/common/Values.v b/common/Values.v
index 41138e8e..4146dd59 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -2613,6 +2613,55 @@ Qed.
 
 End VAL_INJ_OPS.
 
+(* Specializations of cmpu_bool, cmpu, cmplu_bool, and cmplu for maximal pointer validity *)
+
+Definition mxcmpu_bool cmp v1 v2: option bool :=
+  cmpu_bool (fun _ _ => true) cmp v1 v2.
+
+Lemma mxcmpu_bool_correct vptr (cmp: comparison) (v1 v2: val) b:
+   cmpu_bool vptr cmp v1 v2 = Some b
+   -> mxcmpu_bool cmp v1 v2 = Some b.
+Proof.
+  intros; eapply cmpu_bool_lessdef; (econstructor 1 || eauto).
+Qed.
+
+Definition mxcmpu cmp v1 v2 := of_optbool (mxcmpu_bool cmp v1 v2).
+
+Lemma mxcmpu_correct vptr (cmp: comparison) (v1 v2: val):
+   lessdef (cmpu vptr cmp v1 v2) (mxcmpu cmp v1 v2).
+Proof.
+  unfold cmpu, mxcmpu.
+  remember (cmpu_bool _ cmp v1 v2) as ob.
+  destruct ob; simpl.
+  - erewrite mxcmpu_bool_correct; eauto.
+    econstructor.
+  - econstructor.
+Qed.
+
+Definition mxcmplu_bool (cmp: comparison) (v1 v2: val)
+ := (cmplu_bool (fun _ _ => true) cmp v1 v2).
+
+Lemma mxcmplu_bool_correct vptr (cmp: comparison) (v1 v2: val) b:
+   (cmplu_bool vptr cmp v1 v2) = Some b
+   -> (mxcmplu_bool cmp v1 v2) = Some b.
+Proof.
+  intros; eapply cmplu_bool_lessdef; (econstructor 1 || eauto).
+Qed.
+
+Definition mxcmplu cmp v1 v2 := of_optbool (mxcmplu_bool cmp v1 v2).
+
+Lemma mxcmplu_correct vptr (cmp: comparison) (v1 v2: val):
+   lessdef (maketotal (cmplu vptr cmp v1 v2))
+               (mxcmplu cmp v1 v2).
+Proof.
+  unfold cmplu, mxcmplu.
+  remember (cmplu_bool _ cmp v1 v2) as ob.
+  destruct ob as [b|]; simpl.
+  - erewrite mxcmplu_bool_correct; eauto.
+    simpl. econstructor.
+  - econstructor.
+Qed.
+
 End Val.
 
 Notation meminj := Val.meminj.
diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 16d880fa..7a7261a3 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -1053,6 +1053,41 @@ Proof.
   induction 1; intros. auto. apply IHis_tail. eapply is_tail_cons_left; eauto.
 Qed.
 
+Lemma is_tail_app A (l1: list A): forall l2, is_tail l2 (l1 ++ l2).
+Proof.
+  induction l1; cbn; auto with coqlib.
+Qed.
+Hint Resolve is_tail_app: coqlib.
+
+Lemma is_tail_app_inv A (l1: list A): forall l2 l3, is_tail (l1 ++ l2) l3 -> is_tail l2 l3.
+Proof.
+  induction l1; cbn; auto with coqlib.
+  intros l2 l3 H; inversion H; eauto with coqlib.
+Qed.
+Hint Resolve is_tail_app_inv: coqlib.
+
+Lemma is_tail_app_right A (l2 l1: list A): is_tail l1 (l2++l1).
+Proof.
+  intros; eauto with coqlib.
+Qed.
+
+Lemma is_tail_app_def A (l1 l2: list A):
+  is_tail l1 l2 -> exists l3, l2 = l3 ++ l1.
+Proof.
+  induction 1 as [|x l1 l2]; simpl.
+  - exists nil; simpl; auto.
+  - destruct IHis_tail as (l3 & EQ); rewrite EQ.
+    exists (x::l3); simpl; auto.
+Qed.
+
+Lemma is_tail_bound A (l1 l2: list A):
+  is_tail l1 l2 -> (length l1 <= length l2)%nat.
+Proof.
+  intros H; destruct (is_tail_app_def H) as (l3 & EQ).
+  subst; rewrite app_length.
+  omega.
+Qed.
+
 (** [list_forall2 P [x1 ... xN] [y1 ... yM]] holds iff [N = M] and
   [P xi yi] holds for all [i]. *)
 
diff --git a/lib/IterList.v b/lib/IterList.v
index 49beb1c5..bde47068 100644
--- a/lib/IterList.v
+++ b/lib/IterList.v
@@ -94,3 +94,18 @@ Lemma list_length_nat_z (A: Type) (l: list A): length l = Z.to_nat (list_length_
 Proof.
   intros; rewrite list_length_z_nat, Nat2Z.id. auto.
 Qed.
+
+Lemma is_tail_list_nth_z A (l1 l2: list A):
+  is_tail l1 l2 -> list_nth_z l2 ((list_length_z l2) - (list_length_z l1)) = list_nth_z l1 0.
+Proof.
+  induction 1; simpl.
+  - replace (list_length_z c - list_length_z c) with 0; omega || auto.
+  - assert (X: list_length_z (i :: c2) > list_length_z c1).
+    { rewrite !list_length_z_nat, <- Nat2Z.inj_gt.
+      exploit is_tail_bound; simpl; eauto.
+      omega. }
+    destruct (zeq (list_length_z (i :: c2) - list_length_z c1) 0) as [Y|Y]; try omega.
+    replace (Z.pred (list_length_z (i :: c2) - list_length_z c1)) with (list_length_z c2 - list_length_z c1); auto.
+    rewrite list_length_z_cons.
+    omega.
+Qed.
diff --git a/scheduling/postpass_lib/Machblockgenproof.v b/scheduling/postpass_lib/Machblockgenproof.v
index fc722887..d121a54b 100644
--- a/scheduling/postpass_lib/Machblockgenproof.v
+++ b/scheduling/postpass_lib/Machblockgenproof.v
@@ -190,7 +190,7 @@ Proof.
   intros H H0 H1.
   unfold find_label.
   remember (is_label l _) as b.
-  cutrewrite (b = false); auto.
+  replace b with false; auto.
   subst; unfold is_label.
   destruct i; cbn in * |- *; try (destruct (in_dec l nil); intuition).
   inversion H.
@@ -286,7 +286,7 @@ Lemma find_label_preserved:
   Mach.find_label l (Mach.fn_code f) = Some c ->
   exists h, In l h /\ find_label l (fn_code (transf_function f)) = Some (concat h (trans_code c)).
 Proof.
-  intros. cutrewrite ((fn_code (transf_function f)) = trans_code (Mach.fn_code f)); eauto.
+  intros. replace (fn_code (transf_function f)) with (trans_code (Mach.fn_code f)); eauto.
   apply find_label_transcode_preserved; auto.
 Qed.
 
@@ -661,7 +661,7 @@ Proof.
     inversion H1; subst; clear H1.
     inversion_clear H0; cbn.
     - (* function_internal*)
-      cutrewrite (trans_code (Mach.fn_code f0) = fn_code (transf_function f0)); eauto.
+      replace (trans_code (Mach.fn_code f0)) with (fn_code (transf_function f0)); eauto.
       eapply exec_function_internal; eauto.
       rewrite <- parent_sp_preserved; eauto.
       rewrite <- parent_ra_preserved; eauto.
@@ -733,12 +733,12 @@ Proof.
   intro H; destruct c as [|i' c]. { inversion H. }
   remember (trans_inst i) as ti.
   destruct ti as [lbl|bi|cfi].
-  - (*i=lbl *) cutrewrite (i = Mlabel lbl). 2: ( destruct i; cbn in * |- *; try congruence ).
+  - (*i=lbl *) replace (i ) with (Mlabel lbl). 2: ( destruct i; cbn in * |- *; try congruence ).
     exists nil; cbn; eexists. eapply Tr_add_label; eauto.
   - (*i=basic*)
     destruct i'.
     10: { exists (add_to_new_bblock (MB_basic bi)::nil).  exists b. 
-      cutrewrite ((add_to_new_bblock (MB_basic bi) :: nil) ++ (b::l)=(add_to_new_bblock (MB_basic bi) :: (b::l)));eauto.
+      replace ((add_to_new_bblock (MB_basic bi) :: nil) ++ (b::l)) with ((add_to_new_bblock (MB_basic bi) :: (b::l)));eauto.
       rewrite Heqti.        
       eapply  Tr_end_block; eauto.
       rewrite <-Heqti.
@@ -748,7 +748,7 @@ Proof.
   - (*i=cfi*)
     destruct i; try(cbn in Heqti; congruence).
     all: exists (add_to_new_bblock (MB_cfi cfi)::nil);  exists b; 
-        cutrewrite ((add_to_new_bblock (MB_cfi cfi) :: nil) ++ (b::l)=(add_to_new_bblock (MB_cfi cfi) :: (b::l)));eauto;
+        replace ((add_to_new_bblock (MB_cfi cfi) :: nil) ++ (b::l)) with ((add_to_new_bblock (MB_cfi cfi) :: (b::l)));eauto;
         rewrite Heqti;        
         eapply  Tr_end_block; eauto;
         rewrite <-Heqti;
@@ -765,21 +765,6 @@ Proof.
     eauto.
 Qed.
 
-(* FIXME: these two lemma should go into [Coqlib.v] *) 
-Lemma is_tail_app A (l1: list A): forall l2, is_tail l2 (l1 ++ l2).
-Proof.
-  induction l1; cbn; auto with coqlib.
-Qed.
-Hint Resolve is_tail_app: coqlib.
-
-Lemma is_tail_app_inv A (l1: list A): forall l2 l3, is_tail (l1 ++ l2) l3 -> is_tail l2 l3.
-Proof.
-  induction l1; cbn; auto with coqlib.
-  intros l2 l3 H; inversion H; eauto with coqlib.
-Qed.
-Hint Resolve is_tail_app_inv: coqlib.
-
-
 Lemma Mach_Machblock_tail sg ros c c1 c2: c1=(Mcall sg ros :: c) -> is_tail c1 c2 -> 
   exists b, is_tail (b :: trans_code c) (trans_code c2).
 Proof.