Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL

16 files changed, 192 insertions, 164 deletions

diff --git a/kvx/Asmblock.v b/kvx/Asmblock.v
index 64b2c535..17ebac32 100644
--- a/kvx/Asmblock.v
+++ b/kvx/Asmblock.v
@@ -29,6 +29,7 @@ Require Stacklayout.
 Require Import Conventions.
 Require Import Errors.
 Require Export Asmvliw.
+Require Import Lia.
 
 (* Notations necessary to hook Asmvliw definitions *)
 Notation undef_caller_save_regs := Asmvliw.undef_caller_save_regs.
@@ -212,7 +213,7 @@ Qed.
 Lemma length_nonil {A: Type} : forall l:(list A), l <> nil -> (length l > 0)%nat.
 Proof.
   intros. destruct l; try (contradict H; auto; fail).
-  cbn. omega.
+  cbn. lia.
 Qed.
 
 Lemma to_nat_pos : forall z:Z, (Z.to_nat z > 0)%nat -> z > 0.
@@ -226,7 +227,7 @@ Qed.
 Lemma size_positive (b:bblock): size b > 0.
 Proof.
   unfold size. destruct b as [hd bdy ex cor]. cbn.
-  destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; cbn; omega).
+  destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; cbn; lia).
   inversion cor; contradict H; cbn; auto.
 Qed.
 
diff --git a/kvx/Asmblockgenproof.v b/kvx/Asmblockgenproof.v
index df1a070f..6e3029d8 100644
--- a/kvx/Asmblockgenproof.v
+++ b/kvx/Asmblockgenproof.v
@@ -21,6 +21,7 @@ Require Import Values Memory Events Globalenvs Smallstep.
 Require Import Op Locations Machblock Conventions Asmblock.
 Require Import Asmblockgen Asmblockgenproof0 Asmblockgenproof1 Asmblockprops.
 Require Import Axioms.
+Require Import Lia.
 
 Module MB := Machblock.
 Module AB := Asmvliw.
@@ -72,7 +73,7 @@ Lemma transf_function_no_overflow:
   transf_function f = OK tf -> size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned.
 Proof.
   intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0.
-  omega.
+  lia.
 Qed.
 
 Section TRANSL_LABEL. (* Lemmas on translation of MB.is_label into AB.is_label *)
@@ -247,8 +248,8 @@ Proof.
   split. unfold goto_label. unfold par_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.
 
@@ -1374,7 +1375,7 @@ Lemma mbsize_eqz:
 Proof.
   intros. destruct bb as [hd bdy ex]; simpl in *. unfold mbsize in H.
   remember (length _) as a. remember (length_opt _) as b.
-  assert (a = 0%nat) by omega. assert (b = 0%nat) by omega. subst. clear H.
+  assert (a = 0%nat) by lia. assert (b = 0%nat) by lia. subst. clear H.
   inv H0. inv H1. destruct bdy; destruct ex; auto.
   all: try discriminate.
 Qed.
@@ -1706,11 +1707,11 @@ Proof.
       + contradiction.
   } destruct EXEC_PROLOGUE as (rs3' & EXEC_PROLOGUE & Heqrs3').
   exploit exec_straight_steps_2; eauto using functions_transl.
-  simpl fn_blocks. simpl fn_blocks in g. omega. constructor.
+  simpl fn_blocks. simpl fn_blocks in g. lia. constructor.
   intros (ofs' & X & Y).                    
   left; exists (State rs3' m3'); split.
   eapply exec_straight_steps_1; eauto.
-  simpl fn_blocks. simpl fn_blocks in g. omega.
+  simpl fn_blocks. simpl fn_blocks in g. lia.
   constructor.
   econstructor; eauto.
   rewrite X; econstructor; eauto. 
@@ -1756,7 +1757,7 @@ Local Transparent destroyed_at_function_entry.
 - (* return *) 
   inv MS.
   inv STACKS. simpl in *.
-  right. split. omega. split. auto.
+  right. split. lia. split. auto.
   rewrite <- ATPC in H5.
   econstructor; eauto. congruence.
 Qed.
diff --git a/kvx/Asmblockgenproof0.v b/kvx/Asmblockgenproof0.v
index 12bb863a..83b574e7 100644
--- a/kvx/Asmblockgenproof0.v
+++ b/kvx/Asmblockgenproof0.v
@@ -37,6 +37,7 @@ Require Import Asmblockgen.
 Require Import Conventions1.
 Require Import Axioms.
 Require Import Asmblockprops.
+Require Import Lia.
 
 Module MB:=Machblock.
 Module AB:=Asmblock.
@@ -410,7 +411,7 @@ Inductive code_tail: Z -> bblocks -> bblocks -> Prop :=
 Lemma code_tail_pos:
   forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0.
 Proof.
-  induction 1. omega. generalize (size_positive bi); intros; omega.
+  induction 1. lia. generalize (size_positive bi); intros; lia.
 Qed.
 
 Lemma find_bblock_tail:
@@ -420,10 +421,10 @@ Lemma find_bblock_tail:
 Proof.
   induction c1; simpl; intros.
   inversion H.  
-  destruct (zlt pos 0). generalize (code_tail_pos _ _ _ H); intro; omega.
+  destruct (zlt pos 0). generalize (code_tail_pos _ _ _ H); intro; lia.
   destruct (zeq pos 0). subst pos.
-  inv H. auto. generalize (size_positive a) (code_tail_pos _ _ _ H4). intro; omega.
-  inv H. congruence. replace (pos0 + size a - size a) with pos0 by omega.
+  inv H. auto. generalize (size_positive a) (code_tail_pos _ _ _ H4). intro; lia.
+  inv H. congruence. replace (pos0 + size a - size a) with pos0 by lia.
   eauto.
 Qed.
 
@@ -438,13 +439,13 @@ Proof.
   induction 1; intros.
   - subst; eauto.
   - replace (pos + size bi + size bi0) with ((pos + size bi0) + size bi); eauto.
-    omega.
+    lia.
 Qed.
 
 Lemma size_blocks_pos c: 0 <= size_blocks c.
 Proof.
-  induction c as [| a l ]; simpl; try omega.
-  generalize (size_positive a); omega.
+  induction c as [| a l ]; simpl; try lia.
+  generalize (size_positive a); lia.
 Qed.
 
 Remark code_tail_positive:
@@ -452,15 +453,15 @@ Remark code_tail_positive:
   code_tail ofs fn c -> 0 <= ofs.
 Proof.
   induction 1; intros; simpl.
-  - omega.
-  - generalize (size_positive bi). omega.
+  - lia.
+  - generalize (size_positive bi). lia.
 Qed.
 
 Remark code_tail_size:
   forall fn ofs c,
   code_tail ofs fn c -> size_blocks fn = ofs + size_blocks c.
 Proof.
-  induction 1; intros; simpl; try omega.
+  induction 1; intros; simpl; try lia.
 Qed.
 
 Remark code_tail_bounds fn ofs c:
@@ -469,7 +470,7 @@ Proof.
   intro H; 
   exploit code_tail_size; eauto.
   generalize (code_tail_positive _ _ _ H), (size_blocks_pos c).
-  omega.
+  lia.
 Qed.
 
 Local Hint Resolve code_tail_next: core.
@@ -486,8 +487,8 @@ Proof.
   intros.
   rewrite Ptrofs.add_unsigned, Ptrofs.unsigned_repr.
   - rewrite Ptrofs.unsigned_repr; eauto.
-    omega.
-  - rewrite Ptrofs.unsigned_repr; omega.
+    lia.
+  - rewrite Ptrofs.unsigned_repr; lia.
 Qed.
 
 (** Predictor for return addresses in generated Asm code.
@@ -566,7 +567,7 @@ Proof.
     exists (Ptrofs.repr ofs). red; intros.
     rewrite Ptrofs.unsigned_repr. congruence.
     exploit code_tail_bounds; eauto.
-    intros; apply transf_function_len in TF. omega.
+    intros; apply transf_function_len in TF. lia.
   + exists Ptrofs.zero; red; intros. congruence.
 Qed.
 
@@ -590,7 +591,7 @@ Inductive transl_code_at_pc (ge: MB.genv):
 Remark code_tail_no_bigger:
   forall pos c1 c2, code_tail pos c1 c2 -> (length c2 <= length c1)%nat.
 Proof.
-  induction 1; simpl; omega.
+  induction 1; simpl; lia.
 Qed.
 
 Remark code_tail_unique:
@@ -598,8 +599,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.
 
@@ -638,12 +639,12 @@ Proof.
   simpl; intros until c'.
   case (is_label lbl a).
   - intros. inv H. exists pos. split; auto. split.
-    replace (pos - pos) with 0 by omega. constructor. constructor; try omega.
-    generalize (size_blocks_pos c). generalize (size_positive a). omega.
+    replace (pos - pos) with 0 by lia. constructor. constructor; try lia.
+    generalize (size_blocks_pos c). generalize (size_positive a). lia.
   - intros. generalize (IHc (pos+size a) c' H). intros [pos' [A [B C]]].
   exists pos'. split. auto. split.
-  replace (pos' - pos) with ((pos' - (pos + (size a))) + (size a)) by omega.
-  constructor. auto. generalize (size_positive a). omega.
+  replace (pos' - pos) with ((pos' - (pos + (size a))) + (size a)) by lia.
+  constructor. auto. generalize (size_positive a). lia.
 Qed.
 
 (** Helper lemmas to reason about
diff --git a/kvx/Asmblockgenproof1.v b/kvx/Asmblockgenproof1.v
index c6ad70ab..a65bd5bc 100644
--- a/kvx/Asmblockgenproof1.v
+++ b/kvx/Asmblockgenproof1.v
@@ -20,6 +20,7 @@ Require Import AST Integers Floats Values Memory Globalenvs.
 Require Import Op Locations Machblock Conventions.
 Require Import Asmblock Asmblockgen Asmblockgenproof0 Asmblockprops.
 Require Import Chunks.
+Require Import Lia.
 
 Import PArithCoercions.
 
@@ -1466,7 +1467,7 @@ Proof.
   change (Int.unsigned Int.zero) with 0.
   pose proof (Int.unsigned_range x) as RANGE.
   unfold zlt, zeq.
-  destruct (Z_lt_dec _ _); destruct (Z.eq_dec _ _); trivial; omega.
+  destruct (Z_lt_dec _ _); destruct (Z.eq_dec _ _); trivial; lia.
 Qed.
 
 Lemma int64_ltu_to_neq:
@@ -1478,7 +1479,7 @@ Proof.
   change (Int64.unsigned Int64.zero) with 0.
   pose proof (Int64.unsigned_range x) as RANGE.
   unfold zlt, zeq.
-  destruct (Z_lt_dec _ _); destruct (Z.eq_dec _ _); trivial; omega.
+  destruct (Z_lt_dec _ _); destruct (Z.eq_dec _ _); trivial; lia.
 Qed.
 
 Ltac splitall := repeat match goal with |- _ /\ _ => split end.
diff --git a/kvx/Asmexpand.ml b/kvx/Asmexpand.ml
index 1e76a355..35c980bb 100644
--- a/kvx/Asmexpand.ml
+++ b/kvx/Asmexpand.ml
@@ -103,7 +103,7 @@ let fixup_variadic_call pos tyl = assert false
 *)
         
 let fixup_call sg =
-  if sg.sig_cc.cc_vararg then fixup_variadic_call 0 sg.sig_args
+  if sg.sig_cc.cc_vararg <> None then fixup_variadic_call 0 sg.sig_args
 
 (* Handling of annotations *)
 
@@ -501,7 +501,7 @@ let expand_instruction instr =
   | Pallocframe (sz, ofs) ->
       let sg = get_current_function_sig() in
       emit (Pmv (Asmvliw.GPR17, stack_pointer));
-      if sg.sig_cc.cc_vararg then begin
+      if sg.sig_cc.cc_vararg <> None then begin
         let n = arguments_size sg in
         let extra_sz = if n >= _nbregargs_ then 0 else (* align _alignment_ *) ((_nbregargs_ - n) * wordsize) in
         let full_sz = Z.add sz (Z.of_uint extra_sz) in
@@ -524,7 +524,7 @@ let expand_instruction instr =
   | Pfreeframe (sz, ofs) ->
      let sg = get_current_function_sig() in
      let extra_sz =
-      if sg.sig_cc.cc_vararg then begin
+      if sg.sig_cc.cc_vararg <> None then begin
         let n = arguments_size sg in
         if n >= _nbregargs_ then 0 else (* align _alignment_ *) ((_nbregargs_ - n) * wordsize)
       end else 0 in
diff --git a/kvx/Asmvliw.v b/kvx/Asmvliw.v
index 8afe8d07..aa2e0885 100644
--- a/kvx/Asmvliw.v
+++ b/kvx/Asmvliw.v
@@ -32,6 +32,7 @@ Require Import Conventions.
 Require Import Errors.
 Require Import Sorting.Permutation.
 Require Import Chunks.
+Require Import Lia.
 
 (** * Abstract syntax *)
 
@@ -1709,7 +1710,7 @@ Ltac Det_WIO X :=
     split. auto. intros. destruct B; auto. subst. auto.
 - (* trace length *)
   red; intros. inv H; cbn.
-  omega.
+  lia.
   eapply external_call_trace_length; eauto.
   eapply external_call_trace_length; eauto.
 - (* initial states *)
diff --git a/kvx/ConstpropOpproof.v b/kvx/ConstpropOpproof.v
index ffd35bcc..f67b8a4e 100644
--- a/kvx/ConstpropOpproof.v
+++ b/kvx/ConstpropOpproof.v
@@ -19,6 +19,7 @@ Require Import Coqlib Compopts.
 Require Import Integers Floats Values Memory Globalenvs Events.
 Require Import Op Registers RTL ValueDomain.
 Require Import ConstpropOp.
+Require Import Lia.
 
 Section STRENGTH_REDUCTION.
 
@@ -336,7 +337,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. cbn. 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.
diff --git a/kvx/Conventions1.v b/kvx/Conventions1.v
index 0b2cf406..d8eff34e 100644
--- a/kvx/Conventions1.v
+++ b/kvx/Conventions1.v
@@ -240,11 +240,18 @@ Fixpoint loc_arguments_rec (va: bool)
 *)
   end.
 
+(* FIX Sylvain: not sure to understand what I have done... *)
+Definition has_va (s: signature) : bool :=
+  match s.(sig_cc).(cc_vararg) with
+  | Some n => true
+  | None => false
+  end.
+
 (** [loc_arguments s] returns the list of locations where to store arguments
   when calling a function with signature [s].  *)
 
 Definition loc_arguments (s: signature) : list (rpair loc) :=
-  loc_arguments_rec s.(sig_cc).(cc_vararg) s.(sig_args) 0 0.
+  loc_arguments_rec (has_va s) s.(sig_args) 0 0.
 
 (** [size_arguments s] returns the number of [Outgoing] slots used
   to call a function with signature [s]. *)
@@ -287,11 +294,11 @@ Proof.
   assert (AL: forall ofs ty, ofs >= 0 -> align ofs (typealign ty) >= 0).
   { intros. 
     assert (ofs <= align ofs (typealign ty)) by (apply align_le; apply typealign_pos).
-    omega. }
+    lia. }
   assert (SK: (if Archi.ptr64 then 2 else 1) > 0).
-  { destruct Archi.ptr64; omega. }
+  { destruct Archi.ptr64; lia. }
   assert (SKK: forall ty, (if Archi.ptr64 then 2 else typesize ty) > 0).
-  { intros. destruct Archi.ptr64. omega. apply typesize_pos.  }
+  { intros. destruct Archi.ptr64. lia. apply typesize_pos.  }
   assert (A: forall regs rn ofs ty f,
              OKREGS regs -> OKF f -> ofs >= 0 -> OK (one_arg regs rn ofs ty f)).
   { intros until f; intros OR OF OO; red; unfold one_arg; intros.
@@ -300,7 +307,7 @@ Proof.
   - eapply OF; eauto. 
   - subst p; cbn. auto using align_divides, typealign_pos.
   - eapply OF; [idtac|eauto].
-    generalize (AL ofs ty OO) (SKK ty); omega.
+    generalize (AL ofs ty OO) (SKK ty); lia.
   }
   assert (B: forall regs rn ofs f,
              OKREGS regs -> OKF f -> ofs >= 0 -> OK (two_args regs rn ofs f)).
@@ -312,8 +319,8 @@ Proof.
                      :: f rn' (ofs' + 2))).
     { red; cbn; intros. destruct H.
     - subst p; cbn. 
-      repeat split; auto using Z.divide_1_l. omega.
-    - eapply OF; [idtac|eauto]. omega.
+      repeat split; auto using Z.divide_1_l. lia.
+    - eapply OF; [idtac|eauto]. lia.
     }
     destruct (list_nth_z regs rn') as [r1|] eqn:NTH1;
     destruct (list_nth_z regs (rn' + 1)) as [r2|] eqn:NTH2;
@@ -330,7 +337,7 @@ Proof.
   - subst p; cbn. apply OR. eapply list_nth_z_in; eauto. 
   - eapply OF; eauto. 
   - subst p; cbn. rewrite OTY. split. apply (AL ofs Tlong OO). apply Z.divide_1_l. 
-  - eapply OF; [idtac|eauto]. generalize (AL ofs Tlong OO); cbn; omega.
+  - eapply OF; [idtac|eauto]. generalize (AL ofs Tlong OO); cbn; lia.
   }
   assert (D: OKREGS param_regs).
   { red. decide_goal. }
@@ -359,7 +366,7 @@ Lemma loc_arguments_acceptable:
   forall (s: signature) (p: rpair loc),
   In p (loc_arguments s) -> forall_rpair loc_argument_acceptable p.
 Proof.
-  unfold loc_arguments; intros. eapply loc_arguments_rec_charact; eauto. omega.
+  unfold loc_arguments; intros. eapply loc_arguments_rec_charact; eauto. lia.
 Qed.
 
 (** The offsets of [Outgoing] arguments are below [size_arguments s]. *)
@@ -368,9 +375,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 [_ | []]; lia. }
   induction l; cbn; intros. 
-  - omega.
+  - lia.
   - eapply Zge_trans. eauto.
     destruct a; cbn. apply A. eapply Zge_trans; eauto.
 Qed.
@@ -388,14 +395,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 [_ | []]; lia. }
   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; cbn in H; intuition; subst; cbn.
-  - xomega.
-  - eapply Z.le_trans. 2: apply A. xomega.
-  - xomega. }
+  - lia.
+  - eapply Z.le_trans. 2: apply A. lia.
+  - lia. }
   assert (C: forall l n,
              In (S Outgoing ofs ty) (regs_of_rpairs l) ->
              ofs + typesize ty <= fold_left max_outgoing_2 l n).
@@ -415,4 +422,10 @@ Proof.
 Qed.
 
 
-Definition return_value_needs_normalization (t: rettype) : bool := false.
+(** ** Normalization of function results and parameters *)
+
+(** No normalization needed. *)
+
+Definition return_value_needs_normalization (t: rettype): bool := false.
+Definition parameter_needs_normalization (t: rettype): bool := false.
+
diff --git a/kvx/ExtValues.v b/kvx/ExtValues.v
index a0c10ddd..b4e14898 100644
--- a/kvx/ExtValues.v
+++ b/kvx/ExtValues.v
@@ -17,6 +17,7 @@ Require Import Coqlib.
 Require Import Integers.
 Require Import Values.
 Require Import Floats ExtFloats.
+Require Import Lia.
 
 Open Scope Z_scope.
 
@@ -31,9 +32,9 @@ Proof.
   unfold Z.leb.
   pose proof (Z.compare_spec x y) as Hspec.
   inv Hspec.
-  - rewrite Z.abs_eq; omega.
-  - rewrite Z.abs_neq; omega.
-  - rewrite Z.abs_eq; omega.
+  - rewrite Z.abs_eq; lia.
+  - rewrite Z.abs_neq; lia.
+  - rewrite Z.abs_eq; lia.
 Qed.
 
 Inductive shift1_4 : Type :=
@@ -202,9 +203,9 @@ Proof.
   intros i H.
   destruct H as [Hlow Hhigh].
   apply Int64.unsigned_repr.
-  split. { omega. }
+  split. { lia. }
   pose proof modulus_fits_64.
-  omega.
+  lia.
 Qed.
   
 Theorem divu_is_divlu: forall v1 v2 : val,
@@ -237,7 +238,7 @@ Proof.
   {subst i0_val.
    pose proof modulus_fits_64.
    rewrite Zdiv_1_r.
-   omega.
+   lia.
   }
   destruct (Z.eq_dec i_val 0).
   { subst i_val. compute.
@@ -245,11 +246,11 @@ Proof.
     intro ABSURD;
     discriminate ABSURD. }
   assert ((i_val / i0_val) < i_val).
-  { apply Z_div_lt; omega. }
+  { apply Z_div_lt; lia. }
   split.
-  { apply Z_div_pos; omega. }
+  { apply Z_div_pos; lia. }
   pose proof modulus_fits_64.
-  omega.
+  lia.
 Qed.
   
 Theorem modu_is_modlu: forall v1 v2 : val,
@@ -280,12 +281,12 @@ Proof.
   reflexivity.
   assert((i_val mod i0_val) < i0_val).
   apply Z_mod_lt.
-  omega.
+  lia.
   split.
   { apply Z_mod_lt.
-    omega. }
+    lia. }
   pose proof modulus_fits_64.
-  omega.
+  lia.
 Qed.
 
 Remark if_zlt_0_half_modulus :
@@ -332,7 +333,7 @@ Proof.
   set (y := Int64.unsigned (Int64.repr x)) in *.
   rewrite H64.
   clear H64.
-  omega.
+  lia.
 Qed.
 
 (*
@@ -375,15 +376,15 @@ Proof.
     destruct (zlt i0_val Int.half_modulus) as [Hlt_half | Hge_half].
     {
       replace Int.half_modulus with 2147483648 in * by reflexivity.
-      rewrite Int64.unsigned_repr by (change Int64.max_unsigned with 18446744073709551615; omega).
-      destruct (zeq _ _) as [ | Hneq0]; try omega. clear Hneq0.
+      rewrite Int64.unsigned_repr by (change Int64.max_unsigned with 18446744073709551615; lia).
+      destruct (zeq _ _) as [ | Hneq0]; try lia. clear Hneq0.
       unfold Val.loword.
       f_equal.
       unfold Int64.divs, Int.divs, Int64.loword.
       unfold Int.signed, Int64.signed. cbn.      
       rewrite if_zlt_min_signed_half_modulus.
       change Int.half_modulus with 2147483648 in *.
-      destruct (zlt _ _) as [discard|]; try omega. clear discard.
+      destruct (zlt _ _) as [discard|]; try lia. clear discard.
       change (Int64.unsigned
                   (Int64.repr
                      (Int.unsigned (Int.repr Int.min_signed) - Int.modulus)))
@@ -391,8 +392,8 @@ Proof.
       change Int64.half_modulus with 9223372036854775808.
       change Int64.modulus with 18446744073709551616.
       cbn.
-      rewrite (Int64.unsigned_repr i0_val) by (change Int64.max_unsigned with 18446744073709551615; omega).
-      destruct (zlt i0_val 9223372036854775808) as [discard |]; try omega.
+      rewrite (Int64.unsigned_repr i0_val) by (change Int64.max_unsigned with 18446744073709551615; lia).
+      destruct (zlt i0_val 9223372036854775808) as [discard |]; try lia.
       clear discard.
       change (Int.unsigned (Int.repr Int.min_signed) - Int.modulus) with  (-2147483648).
       destruct (Z.eq_dec i0_val 1) as [H1 | Hnot1].
@@ -418,14 +419,14 @@ Proof.
       set (delta := (i0_val - Int.modulus)) in *.
       assert (delta = Int64.modulus*(delta/Int64.modulus)) as Hdelta.
       { apply Z_div_exact_full_2.
-        compute. omega.
+        compute. lia.
         assumption. }
       set (k := (delta / Int64.modulus)) in *.
       change Int64.modulus with 18446744073709551616 in *.
       change Int.modulus with 4294967296 in *.
       change Int.half_modulus with 2147483648 in *.
       change (Int.unsigned Int.mone) with 4294967295 in *.
-      omega.
+      lia.
     }
     unfold Int.divs, Int64.divs, Val.loword, Int64.loword.
     change (Int.unsigned (Int.repr Int.min_signed)) with 2147483648.
@@ -451,7 +452,7 @@ Proof.
   intro BIG.
   unfold Int.signed, Int.unsigned in *. cbn in *.
   destruct (zlt _ _).
-  omega.
+  lia.
   trivial.
 Qed.
 
@@ -476,11 +477,11 @@ Proof.
     subst.
     rewrite Z.quot_0_l.
     auto with zarith.
-    omega.
+    lia.
   }
   assert ((Z.quot a b) < a).
   {
-    apply Z.quot_lt; omega.
+    apply Z.quot_lt; lia.
   }
   auto with zarith.
 Qed.
@@ -516,9 +517,9 @@ Proof.
       change (Int.unsigned (Int.repr Int.min_signed)) with (2147483648) in *.
       rewrite big_unsigned_signed.
       change Int.modulus with 4294967296.
-      omega.
+      lia.
       change Int.half_modulus with 2147483648.
-      omega.
+      lia.
     }
     unfold Int.eq in EXCEPTION.
     destruct (zeq _ _) in EXCEPTION; try discriminate.
@@ -552,8 +553,8 @@ Lemma Z_quot_pos_pos_bound: forall a b m,
 Proof.
   intros.
   split.
-  { rewrite <- (Z.quot_0_l b) by omega.
-    apply Z_quot_monotone; omega.
+  { rewrite <- (Z.quot_0_l b) by lia.
+    apply Z_quot_monotone; lia.
   }
   apply Z.le_trans with (m := a).
   {
@@ -566,10 +567,10 @@ Lemma Z_quot_neg_pos_bound: forall a b m,
   intros.
   assert (0 <= - (a ÷ b) <= -m).
   {
-    rewrite <- Z.quot_opp_l by omega.
-    apply Z_quot_pos_pos_bound; omega.
+    rewrite <- Z.quot_opp_l by lia.
+    apply Z_quot_pos_pos_bound; lia.
   }
-  omega.
+  lia.
 Qed.
 
 Lemma Z_quot_signed_pos_bound: forall a b,
@@ -580,7 +581,7 @@ Proof.
   destruct (Z_lt_ge_dec a 0).
   {
     split.
-    { apply Z_quot_neg_pos_bound; omega. }
+    { apply Z_quot_neg_pos_bound; lia. }
     { eapply Z.le_trans with (m := 0).
       { apply Z_quot_neg_pos_bound with (m := Int.min_signed); trivial.
         split. tauto. auto with zarith.
@@ -592,9 +593,9 @@ Proof.
     { eapply Z.le_trans with (m := 0).
       discriminate.
       apply Z_quot_pos_pos_bound with (m := Int.max_signed); trivial.
-      split. omega. tauto.
+      split. lia. tauto.
     }
-    { apply Z_quot_pos_pos_bound; omega.
+    { apply Z_quot_pos_pos_bound; lia.
     }
   }
 Qed.
@@ -608,42 +609,42 @@ Proof.
   intros.
 
   replace b with (-(-b)) by auto with zarith.
-  rewrite Z.quot_opp_r by omega.
+  rewrite Z.quot_opp_r by lia.
   assert (-2147483647 <= (a ÷ - b) <= 2147483648).
-  2: omega.
+  2: lia.
   
   destruct (Z_lt_ge_dec a 0).
   {
     replace a with (-(-a)) by auto with zarith.
-    rewrite Z.quot_opp_l by omega.
+    rewrite Z.quot_opp_l by lia.
     assert (-2147483648 <= - a ÷ - b <= 2147483647).
-    2: omega.
+    2: lia.
     split.
     {
-      rewrite Z.quot_opp_l by omega.
+      rewrite Z.quot_opp_l by lia.
       assert (a ÷ - b <= 2147483648).
-      2: omega.
+      2: lia.
       {
         apply Z.le_trans with (m := 0).
-        rewrite <- (Z.quot_0_l (-b)) by omega.
-        apply Z_quot_monotone; omega.
+        rewrite <- (Z.quot_0_l (-b)) by lia.
+        apply Z_quot_monotone; lia.
         discriminate.
       }
     }
     assert (- a ÷ - b < -a ).
-    2: omega.
-    apply Z_quot_lt; omega.
+    2: lia.
+    apply Z_quot_lt; lia.
   }
   {
     split.
     { apply Z.le_trans with (m := 0).
       discriminate.
-      rewrite <- (Z.quot_0_l (-b)) by omega.
-      apply Z_quot_monotone; omega.
+      rewrite <- (Z.quot_0_l (-b)) by lia.
+      apply Z_quot_monotone; lia.
     }
     { apply Z.le_trans with (m := a).
       apply Z_quot_le.
-      all: omega.
+      all: lia.
     }
   }
 Qed.
diff --git a/kvx/NeedOp.v b/kvx/NeedOp.v
index f636336d..4578b4e8 100644
--- a/kvx/NeedOp.v
+++ b/kvx/NeedOp.v
@@ -18,6 +18,7 @@ Require Import AST Integers Floats.
 Require Import Values Memory Globalenvs.
 Require Import Op RTL.
 Require Import NeedDomain.
+Require Import Lia.
 
 (** Neededness analysis for RISC-V operators *)
 
@@ -405,8 +406,8 @@ Lemma operation_is_redundant_sound:
   vagree v arg1' nv.
 Proof.
   intros. destruct op; cbn in *; try discriminate; inv H1; FuncInv; subst.
-- apply sign_ext_redundant_sound; auto. omega.
-- apply sign_ext_redundant_sound; auto. omega.
+- apply sign_ext_redundant_sound; auto. lia.
+- apply sign_ext_redundant_sound; auto. lia.
 - apply andimm_redundant_sound; auto.
 - apply orimm_redundant_sound; auto.
 Qed.
diff --git a/kvx/PostpassScheduling.v b/kvx/PostpassScheduling.v
index 1f1f238a..08e640c6 100644
--- a/kvx/PostpassScheduling.v
+++ b/kvx/PostpassScheduling.v
@@ -18,6 +18,7 @@ Require Import Coqlib Errors AST Integers.
 Require Import Asmblock Axioms Memory Globalenvs.
 Require Import Asmblockdeps Asmblockgenproof0 Asmblockprops.
 Require Peephole.
+Require Import Lia.
 
 Local Open Scope error_monad_scope.
 
@@ -87,8 +88,8 @@ Lemma concat2_zlt_size:
 Proof.
   intros. monadInv H.
   split.
-  - unfold check_size in EQ. destruct (zlt Ptrofs.max_unsigned (size a)); monadInv EQ. omega.
-  - unfold check_size in EQ1. destruct (zlt Ptrofs.max_unsigned (size b)); monadInv EQ1. omega.
+  - unfold check_size in EQ. destruct (zlt Ptrofs.max_unsigned (size a)); monadInv EQ. lia.
+  - unfold check_size in EQ1. destruct (zlt Ptrofs.max_unsigned (size b)); monadInv EQ1. lia.
 Qed.
 
 Lemma concat2_noexit:
@@ -436,7 +437,7 @@ Lemma verified_schedule_size:
 Proof.
   intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i.
   all: try (apply verified_schedule_nob_size; auto; fail).
-  inv H. simpl. omega.
+  inv H. simpl. lia.
 Qed.
 
 Lemma verified_schedule_no_header_in_middle:
diff --git a/kvx/PostpassSchedulingproof.v b/kvx/PostpassSchedulingproof.v
index c290387b..937b3be6 100644
--- a/kvx/PostpassSchedulingproof.v
+++ b/kvx/PostpassSchedulingproof.v
@@ -20,6 +20,7 @@ Require Import Asmblockgenproof0 Asmblockprops.
 Require Import PostpassScheduling.
 Require Import Asmblockgenproof.
 Require Import Axioms.
+Require Import Lia.
 
 Local Open Scope error_monad_scope.
 
@@ -93,12 +94,12 @@ Proof.
     rewrite <- H1. unfold nextblock in EXEB. rewrite regset_double_set_id.
     assert (size bb = size a + size b).
     { unfold size. rewrite H0. rewrite H1. rewrite app_length. rewrite EXA. simpl. rewrite Nat.add_0_r.
-      repeat (rewrite Nat2Z.inj_add). omega. }
+      repeat (rewrite Nat2Z.inj_add). lia. }
     clear EXA H0 H1. rewrite H in EXEB.
     assert (rs1 PC = rs0 PC). { apply exec_body_pc in EXEB2. auto. }
     rewrite H0. rewrite <- pc_set_add; auto.
-    exploit size_positive. instantiate (1 := a). intro. omega.
-    exploit size_positive. instantiate (1 := b). intro. omega.
+    exploit size_positive. instantiate (1 := a). intro. lia.
+    exploit size_positive. instantiate (1 := b). intro. lia.
 Qed.
 
 Lemma concat_all_exec_bblock (ge: Genv.t fundef unit) (f: function) :
@@ -140,7 +141,7 @@ Lemma transf_function_no_overflow:
   transf_function f = OK tf -> size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned.
 Proof.
   intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0.
-  omega.
+  lia.
 Qed.
 
 Lemma symbols_preserved:
@@ -224,7 +225,7 @@ Proof.
     + apply IHlbb in H. destruct H as (c & TAIL). exists c.
       enough (pos = pos - size a + size a) as ->.
       apply code_tail_S; auto.
-      omega.
+      lia.
 Qed.
 
 Lemma code_tail_head_app:
@@ -291,7 +292,7 @@ Lemma verified_schedule_not_empty:
   verified_schedule bb = OK lbb -> lbb <> nil.
 Proof.
   intros. apply verified_schedule_size in H.
-  pose (size_positive bb). assert (size_blocks lbb > 0) by omega. clear H g.
+  pose (size_positive bb). assert (size_blocks lbb > 0) by lia. clear H g.
   destruct lbb; simpl in *; discriminate.
 Qed.
 
@@ -356,7 +357,7 @@ Proof.
   induction tc.
   - intros. simpl in H. discriminate.
   - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL.
-    + inv H. assert (k = k') by omega. subst. reflexivity.
+    + inv H. assert (k = k') by lia. subst. reflexivity.
     + pose (IHtc l p p' k (k' + size a)). repeat (rewrite Z.add_assoc in e). auto.
 Qed.
 
diff --git a/kvx/SelectLongproof.v b/kvx/SelectLongproof.v
index fb38bbce..c3abdbc7 100644
--- a/kvx/SelectLongproof.v
+++ b/kvx/SelectLongproof.v
@@ -23,6 +23,7 @@ Require Import OpHelpers OpHelpersproof.
 Require Import SelectOp SelectOpproof SplitLong SplitLongproof.
 Require Import SelectLong.
 Require Import DecBoolOps.
+Require Import Lia.
 
 Local Open Scope cminorsel_scope.
 Local Open Scope string_scope.
@@ -408,14 +409,14 @@ Proof.
          rewrite BOUNDS.
          destruct v1; try (simpl; apply Val.lessdef_undef).
         replace (Z.sub Int64.zwordsize
-                         (Z.add (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1) by omega.
+                         (Z.add (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1) by lia.
         replace (Z.sub Int64.zwordsize
              (Z.sub
                 (Z.add (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)
                 (Z.sub
                    (Z.add
                       (Z.add (Int.unsigned n) (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)))
-                      Z.one) Int64.zwordsize))) with (Int.unsigned n) by omega.
+                      Z.one) Int64.zwordsize))) with (Int.unsigned n) by lia.
         simpl.
         destruct (Int.ltu n1 Int64.iwordsize') eqn:Hltu_n1; simpl; trivial.
         destruct (Int.ltu n Int64.iwordsize') eqn:Hltu_n; simpl; trivial.
@@ -460,14 +461,14 @@ Proof.
          rewrite BOUNDS.
          destruct v1; try (simpl; apply Val.lessdef_undef).
         replace (Z.sub Int64.zwordsize
-                         (Z.add (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1) by omega.
+                         (Z.add (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1) by lia.
         replace (Z.sub Int64.zwordsize
              (Z.sub
                 (Z.add (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)
                 (Z.sub
                    (Z.add
                       (Z.add (Int.unsigned n) (Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one)))
-                      Z.one) Int64.zwordsize))) with (Int.unsigned n) by omega.
+                      Z.one) Int64.zwordsize))) with (Int.unsigned n) by lia.
         simpl.
         destruct (Int.ltu n1 Int64.iwordsize') eqn:Hltu_n1; simpl; trivial.
         destruct (Int.ltu n Int64.iwordsize') eqn:Hltu_n; simpl; trivial.
@@ -708,9 +709,9 @@ Proof.
                rewrite Int64.shl'_zero.
                reflexivity.
            *** simpl. unfold Int.max_unsigned. unfold Int.modulus.
-               simpl. omega.
+               simpl. lia.
         ** unfold Int.max_unsigned. unfold Int.modulus.
-               simpl. omega.
+               simpl. lia.
       * TrivialExists.
     + TrivialExists.
 - TrivialExists.
diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v
index 7a301929..a7169881 100644
--- a/kvx/SelectOpproof.v
+++ b/kvx/SelectOpproof.v
@@ -34,6 +34,7 @@ Require Import Events.
 Require Import OpHelpers.
 Require Import OpHelpersproof.
 Require Import DecBoolOps.
+Require Import Lia.
 
 Local Open Scope cminorsel_scope.
 Local Open Scope string_scope.
@@ -465,14 +466,14 @@ Proof.
          rewrite BOUNDS.
          destruct v1; try (simpl; apply Val.lessdef_undef).
         replace (Z.sub Int.zwordsize
-                         (Z.add (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1) by omega.
+                         (Z.add (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1) by lia.
         replace (Z.sub Int.zwordsize
              (Z.sub
                 (Z.add (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)
                 (Z.sub
                    (Z.add
                       (Z.add (Int.unsigned n) (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)))
-                      Z.one) Int.zwordsize))) with (Int.unsigned n) by omega.
+                      Z.one) Int.zwordsize))) with (Int.unsigned n) by lia.
         rewrite Int.repr_unsigned.
         rewrite Int.repr_unsigned.
         simpl.
@@ -522,14 +523,14 @@ Proof.
          rewrite BOUNDS.
          destruct v1; try (simpl; apply Val.lessdef_undef).
         replace (Z.sub Int.zwordsize
-                         (Z.add (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1) by omega.
+                         (Z.add (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1) by lia.
         replace (Z.sub Int.zwordsize
              (Z.sub
                 (Z.add (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)
                 (Z.sub
                    (Z.add
                       (Z.add (Int.unsigned n) (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)))
-                      Z.one) Int.zwordsize))) with (Int.unsigned n) by omega.
+                      Z.one) Int.zwordsize))) with (Int.unsigned n) by lia.
         rewrite Int.repr_unsigned.
         rewrite Int.repr_unsigned.
         simpl.
@@ -618,20 +619,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 Zbits.Zshiftr_div_two_p by omega. reflexivity.
+  unfold Int.mulhs; f_equal. rewrite Zbits.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.
 - TrivialExists.
 Qed.
 
@@ -646,20 +647,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 Zbits.Zshiftr_div_two_p by omega. reflexivity.
+  unfold Int.mulhu; f_equal. rewrite Zbits.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_shru' 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.unsigned i * Int.unsigned 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.
 - TrivialExists.
 Qed.
 
@@ -811,10 +812,10 @@ Proof.
         *** simpl.
             unfold Int.max_unsigned, Int.modulus.
             simpl.
-            omega.
+            lia.
         ** unfold Int.max_unsigned, Int.modulus.
            simpl.
-           omega.
+           lia.
       * apply DEFAULT.
     + apply DEFAULT.
   - apply DEFAULT.
diff --git a/kvx/Stacklayout.v b/kvx/Stacklayout.v
index 81ffcebb..05cfa1d7 100644
--- a/kvx/Stacklayout.v
+++ b/kvx/Stacklayout.v
@@ -18,6 +18,7 @@
 Require Import Coqlib.
 Require Import AST Memory Separation.
 Require Import Bounds.
+Require Import Lia.
 
 Local Open Scope sep_scope.
 
@@ -71,15 +72,15 @@ Local Opaque Z.add Z.mul sepconj range.
   set (ol :=  align (size_callee_save_area b ocs) 8).
   set (ostkdata := align (ol + 4 * b.(bound_local)) 8).
   replace (size_chunk Mptr) with w by (rewrite size_chunk_Mptr; auto).
-  assert (0 < w) by (unfold w; destruct Archi.ptr64; omega).
+  assert (0 < w) by (unfold w; destruct Archi.ptr64; lia).
   generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros.
-  assert (0 <= 4 * b.(bound_outgoing)) by omega.
-  assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega).
-  assert (olink + w <= oretaddr) by (unfold oretaddr; omega).
-  assert (oretaddr + w <= ocs) by (unfold ocs; omega).
+  assert (0 <= 4 * b.(bound_outgoing)) by lia.
+  assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; lia).
+  assert (olink + w <= oretaddr) by (unfold oretaddr; lia).
+  assert (oretaddr + w <= ocs) by (unfold ocs; lia).
   assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). 
-  assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega).
-  assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega).
+  assert (size_callee_save_area b ocs <= ol) by (apply align_le; lia).
+  assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; lia).
 (* Reorder as:
      outgoing
      back link
@@ -92,11 +93,11 @@ Local Opaque Z.add Z.mul sepconj range.
   rewrite sep_swap45.
 (* Apply range_split and range_split2 repeatedly *)
   unfold fe_ofs_arg.
-  apply range_split_2. fold olink; omega. omega.
-  apply range_split. omega.
-  apply range_split. omega.
-  apply range_split_2. fold ol. omega. omega.
-  apply range_drop_right with ostkdata. omega.
+  apply range_split_2. fold olink; lia. lia.
+  apply range_split. lia.
+  apply range_split. lia.
+  apply range_split_2. fold ol. lia. lia.
+  apply range_drop_right with ostkdata. lia.
   eapply sep_drop2. eexact H.
 Qed.
 
@@ -112,16 +113,16 @@ Proof.
   set (ocs := oretaddr + w).
   set (ol :=  align (size_callee_save_area b ocs) 8).
   set (ostkdata := align (ol + 4 * b.(bound_local)) 8).
-  assert (0 < w) by (unfold w; destruct Archi.ptr64; omega).
+  assert (0 < w) by (unfold w; destruct Archi.ptr64; lia).
   generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros.
-  assert (0 <= 4 * b.(bound_outgoing)) by omega.
-  assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega).
-  assert (olink + w <= oretaddr) by (unfold oretaddr; omega).
-  assert (oretaddr + w <= ocs) by (unfold ocs; omega).
+  assert (0 <= 4 * b.(bound_outgoing)) by lia.
+  assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; lia).
+  assert (olink + w <= oretaddr) by (unfold oretaddr; lia).
+  assert (oretaddr + w <= ocs) by (unfold ocs; lia).
   assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). 
-  assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega).
-  assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega).
-  split. omega. apply align_le. omega. 
+  assert (size_callee_save_area b ocs <= ol) by (apply align_le; lia).
+  assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; lia).
+  split. lia. apply align_le. lia. 
 Qed.
 
 Lemma frame_env_aligned:
@@ -140,11 +141,11 @@ Proof.
   set (ocs := oretaddr + w).
   set (ol :=  align (size_callee_save_area b ocs) 8).
   set (ostkdata := align (ol + 4 * b.(bound_local)) 8).
-  assert (0 < w) by (unfold w; destruct Archi.ptr64; omega).
+  assert (0 < w) by (unfold w; destruct Archi.ptr64; lia).
   replace (align_chunk Mptr) with w by (rewrite align_chunk_Mptr; auto).
   split. apply Z.divide_0_r.
-  split. apply align_divides; omega.
-  split. apply align_divides; omega.
-  split. apply align_divides; omega.
-  apply Z.divide_add_r. apply align_divides; omega. apply Z.divide_refl.
+  split. apply align_divides; lia.
+  split. apply align_divides; lia.
+  split. apply align_divides; lia.
+  apply Z.divide_add_r. apply align_divides; lia. apply Z.divide_refl.
 Qed.
diff --git a/kvx/TargetPrinter.ml b/kvx/TargetPrinter.ml
index 5b6230ca..9e2e3776 100644
--- a/kvx/TargetPrinter.ml
+++ b/kvx/TargetPrinter.ml
@@ -201,14 +201,16 @@ module Target (*: TARGET*) =
 
     let name_of_section = function
       | Section_text         -> ".text"
-      | Section_data(true, true) ->
+      | Section_data(Init, true) ->
          ".section .tdata,\"awT\",@progbits"
-      | Section_data(false, true) ->        
+      | Section_data(Uninit, true) ->        
          ".section .tbss,\"awT\",@nobits"
+      | Section_data(Init_reloc, true) ->
+         failwith "Sylvain does not how to fix this"
       | Section_data(i, false) | Section_small_data(i) ->
-         (if i then ".data" else "COMM")
+         variable_section ~sec:".data" ~bss:".bss" i
       | Section_const i | Section_small_const i ->
-          if i then ".section	.rodata" else "COMM"
+         variable_section ~sec:".section       .rodata" i
       | Section_string       -> ".section	.rodata"
       | Section_literal      -> ".section	.rodata"
       | Section_jumptable    -> ".section	.rodata"