Merge PR coq#18159: Make Coq_Micromega.witness_list tail recursive.

Reviewed-by: ppedrot
Co-authored-by: ppedrot <[email protected]>

doc/changelog/04-tactics/18159-janno-xwitness-tail-rec.rst

@@ -0,0 +1,5 @@
+- **Fixed:**
+  A stack overflow due to a non-tail recursive function in `lia`
+  (`#18159 <https://github.com/coq/coq/pull/18159>`_,
+  fixes `#18158 <https://github.com/coq/coq/issues/18158>`_,
+  by Jan-Oliver Kaiser and Rodolphe Lepigre).

plugins/micromega/coq_micromega.ml

@@ -1595,20 +1595,16 @@ let find_witness p polys1 =
   *)
 
 let witness_list prover l =
-  let rec xwitness_list l =
-    match l with
-    | [] -> Prf []
-    | e :: l -> (
-      match xwitness_list l with
-      | Model (m, e) -> Model (m, e)
+  let rec xwitness_list stack l =
+    match stack with
+    | [] -> Prf l
+    | e :: stack ->
+      match find_witness prover e with
+      | Model m -> (Model (m, e))
       | Unknown -> Unknown
-      | Prf l -> (
-        match find_witness prover e with
-        | Model m -> Model (m, e)
-        | Unknown -> Unknown
-        | Prf w -> Prf (w :: l) ) )
+      | Prf w -> xwitness_list stack (w :: l)
   in
-  xwitness_list l
+  xwitness_list (List.rev l) []
 
 (*  let t1 = System.get_time () in
   let res = witness_list p g in

test-suite/micromega/bug_18158.v

@@ -0,0 +1,91 @@
+Require Import ZArith.
+Import Coq.micromega.Lia.
+Open Scope Z_scope.
+
+Lemma shiftr_lbound a n:
+   0 <= a -> True -> 0 <= (Z.shiftr a n).
+Proof. now intros; apply Z.shiftr_nonneg. Qed.
+
+
+Lemma shiftr_ubound a n b :
+   0 <= n -> 0 <= a < b -> (Z.shiftr a n) < b.
+Proof.
+  intros.
+  rewrite -> Z.shiftr_div_pow2 by assumption.
+
+  apply Zdiv.Zdiv_lt_upper_bound.
+  - now apply Z.pow_pos_nonneg.
+  -
+    eapply Z.lt_le_trans.
+    2: apply Z.le_mul_diag_r; try lia.
+    lia.
+Qed.
+
+Lemma shiftrContractive8 v r :
+   0 <= v < 2 ^ 8 -> 0 <= r -> (Z.shiftr v r) <  2 ^ 8.
+Proof.
+  intros; apply shiftr_ubound; assumption.
+Qed.
+
+
+Lemma shiftrContractive16 v r :
+   0 <= v < 2 ^ 16 -> 0 <= r -> (Z.shiftr v r) <  2 ^ 16.
+Proof.
+  intros; apply shiftr_ubound; assumption.
+Qed.
+
+Lemma shiftrContractive32 v r :
+   0 <= v < 2 ^ 32 -> 0 <= r -> (Z.shiftr v r) <  2 ^ 32.
+Proof.
+  intros; apply shiftr_ubound; assumption.
+Qed.
+
+#[global] Instance sat_shiftr_lbound : ZifyClasses.Saturate BinIntDef.Z.shiftr :=
+  {|
+    ZifyClasses.PArg1 := fun a => 0 <= a;
+    ZifyClasses.PArg2 := fun b => True;
+    ZifyClasses.PRes := fun a b ab => 0 <= ab;
+    ZifyClasses.SatOk := shiftr_lbound
+  |}.
+Add Zify Saturate sat_shiftr_lbound.
+
+#[global] Instance sat_shiftr_contr_8 : ZifyClasses.Saturate BinIntDef.Z.shiftr :=
+  {|
+    ZifyClasses.PArg1 := fun a => 0 <= a < 2 ^ 8;
+    ZifyClasses.PArg2 := fun b => 0 <= b;
+    ZifyClasses.PRes := fun a b ab => ab < 2 ^ 8;
+    ZifyClasses.SatOk := shiftrContractive8
+  |}.
+Add Zify Saturate sat_shiftr_contr_8.
+
+#[global] Instance sat_shiftr_contr_16 : ZifyClasses.Saturate BinIntDef.Z.shiftr :=
+  {|
+    ZifyClasses.PArg1 := fun a => 0 <= a < 2 ^ 16;
+    ZifyClasses.PArg2 := fun b => 0 <= b;
+    ZifyClasses.PRes := fun a b ab => ab < 2 ^ 16;
+    ZifyClasses.SatOk := shiftrContractive16
+  |}.
+Add Zify Saturate sat_shiftr_contr_16.
+
+
+#[global] Instance sat_shiftr_contr_32 : ZifyClasses.Saturate BinIntDef.Z.shiftr :=
+  {|
+    ZifyClasses.PArg1 := fun a => 0 <= a < 2 ^ 32;
+    ZifyClasses.PArg2 := fun b => 0 <= b;
+    ZifyClasses.PRes := fun a b ab => ab < 2 ^ 32;
+    ZifyClasses.SatOk := shiftrContractive32
+  |}.
+Add Zify Saturate sat_shiftr_contr_32.
+
+
+Goal forall x y ,
+    Z.le (Z.shiftr x 16) 255
+    -> Z.le (Z.shiftr x 8) 255
+    -> Z.le (Z.shiftr x 0 ) 255
+    -> Z.le (Z.shiftr y 8) 255
+    -> Z.le (Z.shiftr x 24) 255.
+  intros.
+  Zify.zify_saturate.
+  (* [xlia zchecker] used to raise a [Stack overflow] error. It is supposed to fail normally. *)
+  assert_fails (xlia zchecker).
+Abort.