NB: This Coq documentation contains a revised version of the Coq implementation of these papers [1], [2], [3], [4], and is also the support for ongoing research. A partial archive (14/01/2001) is available at here. Drop us a line if you are interested in a complete, up-to-date archive.

Library mont_square_triple

Require Import ssreflect ssrbool eqtype.
Require Import Arith_ext ZArith_ext Lists_ext.
Require Import machine_int multi_int.
Import MachineInt.
Require Import mips_seplog mips_contrib mips_tactics mapstos.
Require Import mont_mul_prg.

Local Open Scope machine_int_scope.
Local Open Scope eqmod_scope.
Local Open Scope zarith_ext_scope.
Local Open Scope heap_scope.
Import expr_m.
Local Open Scope mips_expr_scope.
Import assert_m.
Local Open Scope mips_assert_scope.
Local Open Scope mips_cmd_scope.
Local Open Scope mips_hoare_scope.
Local Open Scope nodup_scope.

Lemma mont_square_triple : forall k alpha x z m one ext int_ X_ Y_ M_ Z_ quot C t s_ : reg,
  nodup(k, alpha, x, z, m, one, ext, int_, X_, Y_, M_, Z_, quot, C, t, s_, r0) ->
  forall nk valpha vx vm vz X M,
    u2Z (nth 0 M zero32) * u2Z valpha =m -1 {{ Zbeta 1 }} ->
    length X = nk -> length M = nk -> u2Z vz + 4 * Z_of_nat nk < Zbeta 1 ->
    Sum nk X < Sum nk M ->
{{ fun s h => [x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> rep zero32 nk ** var_e m |--> M) s h /\ store.multi_null s }}
montgomery k alpha x x z m one ext int_ X_ Y_ M_ Z_ quot C t s_
{{ fun s h => exists Z, length Z = nk /\ [x]_s = vx /\ [z]_s = vz /\
  [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  Zbeta nk * Sum (S nk) (Z ++ [C]_s :: nil) =m Sum nk X * Sum nk X {{ Sum nk M }} /\
  Sum (S nk) (Z ++ [C]_s::nil) < 2 * Sum nk M /\
  u2Z [t]_s = u2Z vz + 4 * Z_of_nat (nk - 1) }}.
Proof.
move=> k alpha x z m one ext int_ X_ Y_ M_ Z_ quot C t s_
  Hset nk valpha vx vm vz X M Halpha Hx Hm Hnz HX.
rewrite /montgomery.

addiu one r0 one16;

NextAddiu.
move=> s h [r_x [r_z [r_m [r_k [r_alpha [Hmem Hmu]]]]]].
rewrite /wp_addiu.
repeat reg_upd; repeat (split; trivial).
by Assert_upd.
by rewrite store.multi_null_upd.

addiu C r0 zero16;

NextAddiu.
move=> s h [[[r_x [r_z [r_m [r_k [r_alpha [Hmem Hmu]]]]]]] r_one].
rewrite /wp_addiu.
repeat reg_upd; repeat (split; trivial).
by Assert_upd.
by rewrite store.multi_null_upd.

addiu ext r0 zero16;

NextAddiu.
move=> s h [[[[r_x [r_z [r_m [r_k [r_alpha [Hmem Hmu]]]]]]] r_one] r_C].
rewrite /wp_addiu.
repeat reg_upd; repeat (split; trivial).
by Assert_upd.
by rewrite store.multi_null_upd.

while (bne ext k)

apply hoare_prop_m.hoare_while_invariant with (fun s h => exists Z, exists next, length Z = nk /\
  [x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\
  [alpha]_s = valpha /\ (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  u2Z [ext]_s = Z_of_nat next /\ u2Z [ext]_s <= u2Z [k]_s /\ [one]_s = one32 /\
  (next <> O -> u2Z [t]_s = u2Z vz + 4 * Z_of_nat (nk - 1)) /\
  (exists K, Zbeta next * Sum (S nk) (Z ++ [C]_s :: nil) = Sum next X * Sum nk X + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next)).

move=> s h [[[[r_x [r_z [r_m [r_k [r_alpha [Hmem Hmu]]]]]] r_one] r_C] r_ext].
exists (rep zero32 nk), O; repeat (split => //).
by apply len_rep.
by rewrite r_ext sext_Z2u // add_0 store.get_r0 u2Z_Z2u.
rewrite r_ext sext_Z2u // add_0 store.get_r0 u2Z_Z2u //; by apply min_u2Z.
apply u2Z_inj; by rewrite r_one sext_Z2u // add_com store.get_r0 add_0 u2Z_Z2u.

exists 0.
have -> : rep zero32 nk ++ [C ]_ s :: nil = rep zero32 (S nk).
  rewrite rep_last; repeat f_equal.
  apply u2Z_inj; by rewrite r_C sext_Z2u // add_0 store.get_r0.
rewrite Sum_rep_0.
split; first by done.
rewrite Zmult_1_r !Zmult_0_l Zplus_0_l; apply Zmult_lt_0_compat; first by done.
apply Zle_lt_trans with (Sum nk X); [by apply min_Sum | done].

move=> s h [[Z [next [HZ [r_x [r_z [r_m [r_k [r_alpha [Hmem [Hext [Hextk' [Hone [Ht Hinv]]]]]]]]]]]]] Hextk].
rewrite /= r_k Hext in Hextk; move/negPn : Hextk; move/Zeq_boolP; move/Z_of_nat_inj => ?; subst next.

exists Z; do 7 (split; trivial).
case: Hinv => K [Hinv1 Hinv2].
split; first by exists K.
split.
apply Zmult_gt_0_lt_reg_r with (Zbeta nk).
apply Zlt_gt; by apply Zbeta_0.
by rewrite Zmult_comm Hinv1.
apply Ht; by destruct nk.

lwxs X ext x;

apply hoare_lwxs_back_alt'' with (fun s h => exists Z, exists next, length Z = nk /\
  [x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  u2Z [ext]_s = Z_of_nat next /\ u2Z [ext]_s < u2Z [k]_s /\ [one]_s = one32 /\
  (exists K, Zbeta next * Sum (S nk) (Z ++ [C]_s :: nil) = Sum next X * Sum nk X + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32).

move=> s h [ [Z [next [HZ [r_x [r_z [r_m [r_k [r_alpha [Hmem [r_ext [Hextk' [Hone [Ht Hinv]]]]]]]]]]]]] Hextk].
rewrite /= r_ext r_k in Hextk, Hextk'.
move/Zeq_boolP : Hextk => Hextk; move/Z_of_nat_le_inj : Hextk' => Hextk'.
have {Hextk}Hextk : next <> nk by contradict Hextk; rewrite Hextk.

exists (nth next X zero32); split.
- Decompose_32 X next X1 X2 HlenX1 HX'; last by rewrite Hx; apply le_neq_lt.
  rewrite HX' (decompose_equiv _ _ _ _ _ HlenX1) !assert_m.con_assoc_equiv assert_m.con_com_equiv !assert_m.con_assoc_equiv in Hmem.
  move: Hmem; apply monotony => // h'.
  apply mapsto_ext => //.
  by rewrite [mult]lock /= -lock shl_Z2u r_ext inj_mult Zmult_comm.
- rewrite /update_store_lwxs.
  exists Z, next; repeat reg_upd; repeat (split; trivial).
  by Assert_upd.
  rewrite r_ext r_k; apply inj_lt_iff; by apply le_neq_lt.
  by apply le_neq_lt.

lw Y zero16 y;

apply hoare_lw_back_alt'' with (fun s h => exists Z, exists next, length Z = nk /\
  [x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  u2Z [ext]_s = Z_of_nat next /\ u2Z [ext]_s < u2Z [k]_s /\ [one]_s = one32 /\
  (exists K, Zbeta next * Sum (S nk) (Z ++ [C]_s :: nil) = Sum next X * Sum nk X + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32 /\ [Y_]_s = nth O X zero32).

move=> s h [Z [next [HZ [r_x [r_z [r_m [r_k [r_alpha [Hmem [r_ext [Hextk' [Hone [Hinv [Hextk r_X_]]]]]]]]]]]]]].

destruct X as [| hdx tlx]; first by destruct nk.
exists hdx; split.
rewrite [assert_m.mapstos _ _]/= !assert_m.con_assoc_equiv in Hmem.
move: Hmem; apply monotony => // h'.
apply mapsto_ext => //=; by rewrite sext_0 add_0.

rewrite /update_store_lw.
exists Z, next; repeat reg_upd; repeat (split; trivial).
by Assert_upd.

lw Z zero16 z;

apply hoare_lw_back_alt'' with (fun s h => exists Z, exists next, length Z = nk /\
  [x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  u2Z [ext]_s = Z_of_nat next /\ u2Z [ext]_s < u2Z [k]_s /\ [one]_s = one32 /\
  (exists K, Zbeta next * Sum (S nk) (Z ++ [C]_s :: nil) = Sum next X * Sum nk X + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32 /\
  [Y_]_s = nth O X zero32 /\ [Z_]_s = nth O Z zero32).

move=> s h [Z [next [HZ [r_x [r_z [r_m [r_k [r_alpha [Hmem [r_ext [Hextk' [Hone [Hinv [Hextk [r_X_ r_Y_]]]]]]]]]]]]]]].

destruct Z as [| hdz tlz]; first by destruct nk.
exists hdz; split.
rewrite assert_m.con_assoc_equiv assert_m.con_com_equiv /= !assert_m.con_assoc_equiv in Hmem.
move: Hmem; apply monotony => // h'.
apply mapsto_ext => //=; by rewrite sext_0 add_0.
rewrite /update_store_lw.
exists (hdz :: tlz), next; repeat reg_upd; repeat (split; trivial).
by Assert_upd.

multu X Y;

apply hoare_multu with (fun s h => exists Z, exists next, length Z = nk /\
  [x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  u2Z [ext]_s = Z_of_nat next /\ u2Z [ext]_s < u2Z [k]_s /\ [one]_s = one32 /\
  (exists K, Zbeta next * Sum (S nk) (Z ++ [C]_s :: nil) = Sum next X * Sum nk X + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32 /\
  [Y_]_s = nth O X zero32 /\ [Z_]_s = nth O Z zero32 /\
  store.utoZ s <= (Zbeta 1 - 1) * (Zbeta 1 - 1) /\
  store.utoZ s = u2Z (nth next X zero32) * u2Z (nth O X zero32)).

move=> s h [Z [next [HZ [r_x [r_z [r_m [r_k [r_alpha [Hmem [r_ext [Hextk' [Hone [Hinv [Hextk [r_X_ [r_Y_ r_Z_]]]]]]]]]]]]]]]].

exists Z, next; repeat reg_upd; repeat (split; trivial).
by Assert_upd.
rewrite store.utoZ_multu; by apply max_u2Z_umul.

by rewrite store.utoZ_multu u2Z_umul r_X_ r_Y_.

lw M zero16 m;

apply hoare_lw_back_alt'' with (fun s h => exists Z, exists next, length Z = nk /\
  [x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  u2Z [ext]_s = Z_of_nat next /\ u2Z [ext]_s < u2Z [k]_s /\ [one]_s = one32 /\
  (exists K, Zbeta next * Sum (S nk) (Z ++ [C]_s :: nil) = Sum next X * Sum nk X + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32 /\ [Y_]_s = nth O X zero32 /\
  [Z_]_s = nth O Z zero32 /\ store.utoZ s <= (Zbeta 1 - 1) * (Zbeta 1 - 1) /\
  store.utoZ s = u2Z (nth next X zero32) * u2Z (nth O X zero32) /\
  [M_]_s = nth O M zero32).

move=> s h [Z [next [HZ [r_x [r_z [r_m [r_k [r_alpha [Hmem [r_ext [Hextk' [Hone [Hinv [Hextk [r_X_ [r_Y_ [r_Z_ [Hm1 Hm2]]]]]]]]]]]]]]]]]].
destruct M as [| hdm tlm]; first by destruct nk.
exists hdm; split.
rewrite assert_m.con_com_equiv /= !assert_m.con_assoc_equiv in Hmem.
move: Hmem; apply monotony => // h'.
apply mapsto_ext => //=; by rewrite sext_0 add_0.

exists Z, next; repeat reg_upd ;repeat (split; trivial).
by Assert_upd.

maddu Z one;

apply hoare_maddu with (fun s h => exists Z, exists next, length Z = nk /\ [x]_s = vx /\
  [z]_s = vz /\ [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  u2Z [ext]_s = Z_of_nat next /\ u2Z [ext]_s < u2Z [k]_s /\ [one]_s = one32 /\
  (exists K, Zbeta next * Sum (S nk) (Z ++ [C]_s :: nil) = Sum next X * Sum nk X + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32 /\ [Y_]_s = nth O X zero32 /\
  [Z_]_s = nth O Z zero32 /\ store.utoZ s <= Zbeta 1 * (Zbeta 1 - 1) /\
  store.utoZ s = u2Z (nth next X zero32) * u2Z (nth O X zero32) + u2Z (nth O Z zero32) /\
  [M_]_s = nth O M zero32).

move=> s h [Z [next [HZ [r_x [r_z [r_m [r_k [r_alpha [Hmem [r_ext [Hextk' [Hone [Hinv [Hextk [r_X_ [r_Y_ [r_Z_ [Hm1 [Hm2 r_M_]]]]]]]]]]]]]]]]]]].

exists Z, next.

have Htmp : store.utoZ s < Zbeta 2 * (2 ^^ store.acx_size - 1).
  apply Zle_lt_trans with ((Zbeta 1 - 1) * (Zbeta 1 - 1)); first by done.
  apply Zlt_le_trans with (Zbeta 2 * (2 ^^ 8 - 1)); first by done.
  apply Zmult_le_compat_l; last by apply Zbeta_0'.
  apply Zminus_le_compat.
  by apply Zpower_2_le, store.acx_size_min.

repeat reg_upd.
do 7 (split; trivial).
by Assert_upd.
do 8 (split; trivial).
split.

rewrite store.utoZ_maddu // Hone umul_1 u2Z_zext r_Z_.
apply Zle_trans with ((Zbeta 1 - 1) + (Zbeta 1 - 1) * (Zbeta 1 - 1)); last by done.
apply Zplus_le_compat.
apply Zle_minus_1; by apply max_u2Z.
rewrite Hm2 -u2Z_umul; by apply max_u2Z_umul.

by rewrite store.utoZ_maddu // Hone umul_1 u2Z_zext r_Z_ Hm2 Zplus_comm.

mflo t;

apply hoare_mflo with (fun s h => exists Z, exists next, length Z = nk /\ [x]_s = vx /\
  [z]_s = vz /\ [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  u2Z [ext]_s = Z_of_nat next /\ u2Z [ext]_s < u2Z [k]_s /\ [one]_s = one32 /\
  (exists K, Zbeta next * Sum (S nk) (Z ++ [C]_s :: nil) = Sum next X * Sum nk X + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32 /\ [Y_]_s = nth O X zero32 /\
  [Z_]_s = nth O Z zero32 /\ store.utoZ s <= Zbeta 1 * (Zbeta 1 - 1) /\
  store.utoZ s = u2Z (nth next X zero32) * u2Z (nth O X zero32) + u2Z (nth O Z zero32) /\
  [M_]_s = nth O M zero32 /\
  [t]_s = ((nth next X zero32 [.*] nth O X zero32) [.+] zext 32 (nth O Z zero32)) [.%] 32).

move=> s h [Z [next [HZ [r_x [r_z [r_m [r_k [r_alpha [Hmem [r_ext [Hextk' [Hone [Hinv [Hextk [r_X_ [r_Y_ [r_Z_ [Hm1 [Hm2 r_M_]]]]]]]]]]]]]]]]]]].

exists Z, next; repeat reg_upd; repeat (split; trivial).
by Assert_upd.

apply store.lo_remainder.
rewrite -plus_assoc; by apply le_plus_r.

rewrite Hm2 u2Z_add //.
by rewrite u2Z_umul u2Z_zext.
rewrite u2Z_zext Zpower_is_exp -Zbeta1_Zpower2 -Zbeta_is_exp /=.
apply Zle_lt_trans with ((Zbeta 1 - 1) * (Zbeta 1 - 1) + (Zbeta 1 - 1)); last by done.
apply Zplus_le_compat.
by apply (@max_u2Z_umul 32).
apply Zle_minus_1; by apply max_u2Z.

mfhi s;

apply hoare_mfhi with (fun s h => exists Z, exists next, length Z = nk /\ [x]_s = vx /\
  [z]_s = vz /\ [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  u2Z [ext]_s = Z_of_nat next /\ u2Z [ext]_s < u2Z [k]_s /\ [one]_s = one32 /\
  (exists K, Zbeta next * Sum (S nk) (Z ++ [C]_s :: nil) = Sum next X * Sum nk X + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32 /\ [Y_]_s = nth O X zero32 /\
  [Z_]_s = nth O Z zero32 /\ store.utoZ s <= Zbeta 1 * (Zbeta 1 - 1) /\
  store.utoZ s = u2Z (nth next X zero32) * u2Z (nth O X zero32) + u2Z (nth O Z zero32) /\
  [M_]_s = nth O M zero32 /\
  [t]_s = ((nth next X zero32 [.*] nth O X zero32) [.+] zext 32 (nth O Z zero32)) [.%] 32 /\
  u2Z ([s_]_s [.||] [t]_s) = u2Z (nth next X zero32) * u2Z (nth O X zero32) + u2Z (nth O Z zero32)).

move=> s h [Z [next [HZ [r_x [r_z [r_m [r_k [r_alpha [Hmem [r_ext [Hextk' [Hone [Hinv [Hextk [ r_X_ [r_Y_ [r_Z_ [Hm1 [Hm2 [r_M_ r_t]]]]]]]]]]]]]]]]]]]].

exists Z, next; repeat reg_upd; repeat (split; trivial).
by Assert_upd.

have H : store.lo s = [t]_s.
  rewrite r_t; apply store.lo_remainder.
  + rewrite -plus_assoc; by apply le_plus_r.
  + rewrite Hm2 -u2Z_umul u2Z_add.
    * by rewrite u2Z_zext.
    * rewrite u2Z_zext Zpower_is_exp -Zbeta1_Zpower2 -Zbeta_is_exp /=.
      apply Zle_lt_trans with ((Zbeta 1 - 1) * (Zbeta 1 - 1) + (Zbeta 1 - 1)); last by done.
      apply Zplus_le_compat; by [apply (@max_u2Z_umul 32) | apply Zle_minus_1, max_u2Z].

rewrite -H u2Z_concat -Zbeta1_Zpower2.
rewrite store.utoZ_def store.utoZ_acx_beta2 in Hm2; last by apply Zle_lt_trans with (Zbeta 1 * (Zbeta 1 - 1)).
rewrite u2Z_Z2u in Hm2; last by split; [apply Zle_refl | apply Zpower_0].
rewrite -Hm2; ring.

multu t alpha;

apply hoare_multu with (fun s h => exists Z, exists next, length Z = nk /\ [x]_s = vx /\
  [z]_s = vz /\ [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  u2Z [ext]_s = Z_of_nat next /\ u2Z [ext]_s < u2Z [k]_s /\ [one]_s = one32 /\
  (exists K, Zbeta next * Sum (S nk) (Z ++ [C]_s :: nil) = Sum next X * Sum nk X + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32 /\ [Y_]_s = nth O X zero32 /\
  [Z_]_s = nth O Z zero32 /\ store.utoZ s <= (Zbeta 1 - 1) * (Zbeta 1 - 1) /\ [M_]_s = nth O M zero32 /\
  [t]_s = ((nth next X zero32 [.*] nth O X zero32) [.+] zext 32 (nth O Z zero32)) [.%] 32 /\
  u2Z ([s_]_s [.||] [t]_s) = u2Z (nth next X zero32) * u2Z (nth O X zero32) + u2Z (nth O Z zero32) /\
  store.utoZ s = u2Z [t]_s * u2Z [alpha]_s).

move=> s h [Z [next [HZ [r_x [r_z [r_m [r_k [r_alpha [Hmem [r_ext [Hextk' [Hone [Hinv [Hextk [r_X_ [r_Y_ [r_Z_ [Hm1 [Hm2 [r_M_ [r_t Hconcat]]]]]]]]]]]]]]]]]]]]].

exists Z, next; repeat reg_upd.
do 6 (split; trivial).
split.
by Assert_upd.
do 8 (split; trivial).
split.
  rewrite store.utoZ_multu; by apply max_u2Z_umul.
do 3 (split; trivial).
by rewrite store.utoZ_multu -u2Z_umul.

addiu int r0 one16;

apply hoare_addiu with (fun s h => exists Z, exists next, length Z = nk /\ [x]_s = vx /\
  [z]_s = vz /\ [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  u2Z [ext]_s = Z_of_nat next /\ u2Z [ext]_s < u2Z [k]_s /\ [one]_s = one32 /\
  (exists K, Zbeta next * Sum (S nk) (Z ++ [C]_s :: nil) = Sum next X * Sum nk X + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32 /\ [Y_]_s = nth O X zero32 /\
  [Z_]_s = nth O Z zero32 /\ store.utoZ s <= (Zbeta 1 - 1) * (Zbeta 1 - 1) /\ [M_]_s = nth O M zero32 /\
  [t]_s = ((nth next X zero32 [.*] nth O X zero32) [.+] zext 32 (nth O Z zero32)) [.%] 32 /\
  u2Z ([s_]_s [.||] [t]_s) = u2Z (nth next X zero32) * u2Z (nth O X zero32) + u2Z (nth O Z zero32) /\
  store.utoZ s = u2Z [t]_s * u2Z [alpha]_s /\ [int_]_s = one32).

move=> s h [Z [next [HZ [r_x [r_z [r_m [r_k [r_alpha [Hmem [r_ext [Hextk' [Hone [Hinv [Hextk [ r_X_ [r_Y_ [r_Z_ [Hm1 [r_M_ [r_t [Hconcat Hm2]]]]]]]]]]]]]]]]]]]]].

exists Z, next; repeat reg_upd; repeat (split; trivial).
by Assert_upd.
by rewrite add_com add_0 // sext_Z2u.

mflo quot;

apply hoare_mflo with (fun s h => exists Z, exists next, length Z = nk /\ [x]_s = vx /\
  [z]_s = vz /\ [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  u2Z [ext]_s = Z_of_nat next /\ u2Z [ext]_s < u2Z [k]_s /\ [one]_s = one32 /\
  (exists K, Zbeta next * Sum (S nk) (Z ++ [C]_s :: nil) = Sum next X * Sum nk X + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\ (next < nk)%nat /\
  [X_]_s = nth next X zero32 /\ [Y_]_s = nth O X zero32 /\ [Z_]_s = nth O Z zero32 /\
  store.utoZ s <= (Zbeta 1 - 1) * (Zbeta 1 - 1) /\ [M_]_s = nth O M zero32 /\
  [t]_s = ((nth next X zero32 [.*] nth O X zero32) [.+] zext 32 (nth O Z zero32)) [.%] 32 /\
  u2Z ([s_]_s [.||] [t]_s) = u2Z (nth next X zero32) * u2Z (nth O X zero32) + u2Z (nth O Z zero32) /\
  store.utoZ s = u2Z [t]_s * u2Z [alpha]_s /\ [int_]_s = one32 /\
  [quot]_s = (((nth next X zero32 [.*] nth O X zero32) [.+] (zext 32 (nth O Z zero32)) [.%] 32)
    [.*] [alpha]_s) [.%] 32).

move=> s h [Z [next [HZ [r_x [r_z [r_m [r_k [r_alpha [Hmem [r_ext [Hextk' [Hone [Hinv [Hextk [ r_X_ [r_Y_ [ r_Z_ [Hm1 [r_M_ [r_t [Hconcat [Hm2 Hgrpint_]]]]]]]]]]]]]]]]]]]]]].

exists Z, next; repeat reg_upd; repeat (split; trivial).
by Assert_upd.

apply store.lo_remainder.
- rewrite -plus_assoc; by apply le_plus_r.
- by rewrite Hm2 r_t -u2Z_umul.

mthi s;

apply hoare_mthi with (fun s h => exists Z, exists next, length Z = nk /\ [x]_s = vx /\
  [z]_s = vz /\ [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  u2Z [ext]_s = Z_of_nat next /\ u2Z [ext]_s < u2Z [k]_s /\ [one]_s = one32 /\
  (exists K, Zbeta next * Sum (S nk) (Z ++ [C]_s :: nil) = Sum next X * Sum nk X + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\ (next < nk)%nat /\
  [X_]_s = nth next X zero32 /\ [Y_]_s = nth O X zero32 /\ [Z_]_s = nth O Z zero32 /\
  store.utoZ s < Zbeta 2 /\ [M_]_s = nth O M zero32 /\
  [t]_s = ((nth next X zero32 [.*] nth O X zero32) [.+] zext 32 (nth O Z zero32)) [.%] 32 /\
  u2Z ([s_]_s [.||] [t]_s) = u2Z (nth next X zero32) * u2Z (nth O X zero32) + u2Z (nth O Z zero32) /\
  [int_]_s = one32 /\
  [quot]_s = ((((nth next X zero32 [.*] nth O X zero32) [.+] zext 32 (nth O Z zero32)) [.%] 32)
    [.*] [alpha]_s) [.%] 32 /\ store.hi s = [s_]_s).

move=> s h [Z [next [HZ [r_x [r_z [r_m [r_k [r_alpha [Hmem [r_ext [Hextk' [Hone [Hinv [Hextk [r_X_ [r_Y_ [ r_Z_ [Hm1 [r_M_ [r_t [Hconcat [Hm2 [Hgrpint_ r_quot]]]]]]]]]]]]]]]]]]]]]]].

exists Z, next; repeat reg_upd; repeat (split; trivial).
by Assert_upd.
rewrite store.utoZ_def store.hi_mthi_op store.acx_mthi_op store.lo_mthi_op store.utoZ_acx_beta2; last first.
  rewrite Hm2.
  apply Zle_lt_trans with ((Zbeta 1 - 1) * (Zbeta 1 - 1)); last by done.
  rewrite -u2Z_umul; by apply max_u2Z_umul.
rewrite u2Z_Z2u // -Zplus_0_r_reverse.
apply Zle_lt_trans with ((Zbeta 1 - 1) + (Zbeta 1 - 1) * Zbeta 1); last by done.
apply Zplus_le_compat.
apply Zle_minus_1; by apply max_u2Z.
apply Zmult_le_compat_r.
apply Zle_minus_1; by apply max_u2Z.
by apply Zbeta_0'.

by apply store.hi_mthi_op.

mtlo t;

apply hoare_mtlo with (fun s h => exists Z, exists next, length Z = nk /\ [x]_s = vx /\
  [z]_s = vz /\ [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  u2Z [ext]_s = Z_of_nat next /\ u2Z [ext]_s < u2Z [k]_s /\ [one]_s = one32 /\
  (exists K, Zbeta next * Sum (S nk) (Z ++ [C]_s :: nil) = Sum next X * Sum nk X + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32 /\ [Y_]_s = nth O X zero32 /\
  [Z_]_s = nth O Z zero32 /\ store.utoZ s < Zbeta 2 /\ [M_]_s = nth O M zero32 /\
  [t]_s = ((nth next X zero32 [.*] nth O X zero32) [.+] zext 32 (nth O Z zero32)) [.%] 32 /\
  u2Z ([s_]_s [.||] [t]_s) = u2Z (nth next X zero32) * u2Z (nth O X zero32) + u2Z (nth O Z zero32) /\
  [int_]_s = one32 /\
  [quot]_s = ((((nth next X zero32 [.*] nth O X zero32) [.+] zext 32 (nth O Z zero32)) [.%] 32)
    [.*] [alpha]_s) [.%] 32 /\
  store.hi s = [s_]_s /\ store.lo s = [t]_s).

move=> s h [Z [next [HZ [r_x [r_z [r_m [r_k [r_alpha [Hmem [r_ext [Hextk' [Hone [Hinv [Hextk [ r_X_ [r_Y_ [r_Z_ [Hm1 [r_M_ [r_t [ Hconcat [Hgrpint_ [r_quot Hm2]]]]]]]]]]]]]]]]]]]]]]].

exists Z, next; repeat reg_upd; repeat (split; trivial).
by Assert_upd.

rewrite store.utoZ_def store.acx_mtlo_op store.lo_mtlo_op store.hi_mtlo_op store.utoZ_acx_beta2 // u2Z_Z2u //= -Zplus_0_r_reverse.
apply Zle_lt_trans with ((Zbeta 1 - 1) + (Zbeta 1 - 1) * Zbeta 1); last by done.
apply Zplus_le_compat.
apply Zle_minus_1; by apply max_u2Z.
apply Zmult_le_compat_r.
apply Zle_minus_1; by apply max_u2Z.
by apply Zbeta_0'.
rewrite -Hm2.
by apply store.hi_mtlo_op.
by apply store.lo_mtlo_op.

maddu quot M;

apply hoare_maddu with (fun s h => exists Z, exists next, length Z = nk /\ [x]_s = vx /\
  [z]_s = vz /\ [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  u2Z [ext]_s = Z_of_nat next /\ u2Z [ext]_s < u2Z [k]_s /\ [one]_s = one32 /\
  (exists K, Zbeta next * Sum (S nk) (Z ++ [C]_s :: nil) = Sum next X * Sum nk X + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32 /\
  [Y_]_s = nth O X zero32 /\ [Z_]_s = nth O Z zero32 /\
  [M_]_s = nth O M zero32 /\ [int_]_s = one32 /\
  [quot]_s = ((((nth next X zero32 [.*] nth O X zero32) [.+] zext 32 (nth O Z zero32)) [.%] 32)
    [.*] [alpha]_s) [.%] 32 /\
  store.utoZ s = u2Z [quot]_s * u2Z (nth O M zero32) +
  u2Z (nth next X zero32) * u2Z (nth O X zero32) + u2Z (nth O Z zero32) /\ store.lo s = zero32).

move=> s h [Z [next [HZ [r_x [r_z [r_m [r_k [r_alpha [Hmem [r_ext [Hextk' [Hone [Hinv [Hextk [r_X_ [r_Y_ [r_Z_ [Hm1 [r_M_ [r_t [Hconcat [Hgrpint_ [r_quot [Hm2 Hm3]]]]]]]]]]]]]]]]]]]]]]]].

exists Z, next; repeat reg_upd; repeat (split; trivial).
by Assert_upd.
rewrite store.utoZ_maddu.
rewrite r_M_ -u2Z_umul store.utoZ_def store.utoZ_acx_beta2 // u2Z_Z2u.
by rewrite Hm2 Hm3 (Zplus_comm (u2Z [t]_s)) -u2Z_concat Hconcat Zmult_0_l -Zplus_0_r_reverse Zplus_assoc.
split; by [apply Zle_refl | apply Zpower_0].
by apply Zlt_le_trans with (Zbeta 2 * 1).

rewrite r_quot; apply montgomery_lemma => //.
by rewrite r_M_ r_alpha.
rewrite store.utoZ_def store.utoZ_acx_beta2 // u2Z_Z2u.
rewrite Zmult_0_l -Zplus_0_r_reverse Zplus_comm -u2Z_concat Hm2 Hm3 Hconcat -u2Z_umul u2Z_add.
rewrite (@u2Z_zext 32) // u2Z_zext.
apply Zle_lt_trans with ((Zbeta 1 - 1) * (Zbeta 1 - 1) + (Zbeta 1 - 1)); last by done.
apply Zplus_le_compat.
by apply (@max_u2Z_umul 32).
rewrite (@u2Z_zext 32) //; apply Zle_minus_1; by apply max_u2Z.
by split; [apply Zle_refl | apply Zpower_0].

mflhxu Z;

apply hoare_mflhxu with (fun s h => exists Z, exists next, length Z = nk /\ [x]_s = vx /\
  [z]_s = vz /\ [m]_s = vm /\ [one]_s = one32 /\ u2Z [k]_s = Z_of_nat nk /\
  [alpha]_s = valpha /\ (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  u2Z [ext]_s = Z_of_nat next /\
  (exists K, Zbeta next * Sum (S nk) (Z ++ [C]_s :: nil) = Sum next X * Sum nk X + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32 /\
  [Y_]_s = nth O X zero32 /\ [M_]_s = nth O M zero32 /\ [int_]_s = one32 /\
  [quot]_s = ((((nth next X zero32 [.*] nth O X zero32) [.+] zext 32 (nth O Z zero32)) [.%] 32)
    [.*] [alpha]_s) [.%] 32 /\
  Zbeta 1 * u2Z (store.hi s [.||] store.lo s) =
  u2Z ([quot]_s) * u2Z (nth O M zero32) + u2Z (nth next X zero32) * u2Z (nth O X zero32) + u2Z (nth O Z zero32) /\
  store.utoZ s < 2 * Zbeta 1 - 2).

move=> s h [Z [next [HZ [r_x [r_z [r_m [r_k [r_alpha [Hmem [r_ext [Hextk' [Hone [Hinv [Hextk [ r_X_ [r_Y_ [r_Z_ [r_M_ [r_int_ [Hquot [Hm2 Hm3]]]]]]]]]]]]]]]]]]]]].

exists Z, next; repeat reg_upd; repeat (split; trivial).
by Assert_upd.

rewrite u2Z_concat store.hi_mflhxu_op store.lo_mflhxu_op -Hm2 store.utoZ_def.
have -> : Zbeta 2 = Zbeta 1 * Zbeta 1 by rewrite -Zbeta_is_exp.
rewrite u2Z_zext Hm3 u2Z_Z2u // -Zbeta1_Zpower2.
repeat reg_upd; ring.

apply store.mflhxu_kbeta1_utoZ.
apply Zle_lt_trans with ((Zbeta 1 - 1) * (Zbeta 1 - 1) + (Zbeta 1 - 1) * (Zbeta 1 - 1) + (Zbeta 1 - 1)); last by done.
rewrite store.utoZ_upd Hm2; apply Zplus_le_compat.
apply Zplus_le_compat; rewrite -u2Z_umul; by apply max_u2Z_umul.
by apply Zle_minus_1, max_u2Z.

addiu t z zero16;

apply hoare_addiu with (fun s h => exists Z, exists next, length Z = nk /\ [x]_s = vx /\
  [z]_s = vz /\ [m]_s = vm /\ [one]_s = one32 /\ u2Z [k]_s = Z_of_nat nk /\
  [alpha]_s = valpha /\ (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  u2Z [ext]_s = Z_of_nat next /\
  (exists K, Zbeta next * Sum (S nk) (Z ++ [C]_s :: nil) = Sum next X * Sum nk X + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32 /\
  [Y_]_s = nth O X zero32 /\ [M_]_s = nth O M zero32 /\ [int_]_s = one32 /\
  [quot]_s = ((((nth next X zero32 [.*] nth O X zero32) [.+] zext 32 (nth O Z zero32)) [.%] 32)
    [.*] [alpha]_s) [.%] 32 /\
  Zbeta 1 * u2Z (store.hi s [.||] store.lo s) =
  u2Z [quot]_s * u2Z (nth O M zero32) + u2Z (nth next X zero32) * u2Z (nth O X zero32) + u2Z (nth O Z zero32) /\
  store.utoZ s < 2 * Zbeta 1 - 2 /\ [t]_s = vz).

move=> s h [Z [next [HZ [r_x [r_z [r_m [Hone [r_k [r_alpha [Hmem [r_ext [Hinv [Hextk [r_X_ [r_Y_ [ [r_M_ [r_int_ [Hquot [ Hm2 Hm3]]]]]]]]]]]]]]]]]]]].

exists Z, next; repeat reg_upd; repeat (split; trivial).
by Assert_upd.

by rewrite sext_Z2u // add_0.

while (bne int k)

apply hoare_prop_m.hoare_stren with (fun s h => exists Z, exists next, exists nint_, length Z = nk /\
  [x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\ [one]_s = one32 /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  u2Z [ext]_s = Z_of_nat next /\ (next < nk)%nat /\ [X_]_s = nth next X zero32 /\
  u2Z [int_]_s = Z_of_nat nint_ /\ (1 <= nint_)%nat /\ u2Z [int_]_s <= u2Z [k]_s /\
  store.utoZ s < 2 * Zbeta 1 - 1 /\ u2Z [t]_s = u2Z vz + 4 * (Z_of_nat nint_ - 1) /\
  (exists K, Zbeta (S next) * Sum_hole (S nk) (nint_ - 1) (Z ++ [C]_s :: nil) +
    u2Z (store.hi s [.||] store.lo s) * Zbeta (next + nint_) =
    Sum next X * Sum nk X + Sum nint_ X * u2Z (nth next X zero32) * Zbeta next +
    Sum nint_ M * u2Z [quot]_s * Zbeta next + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next)).

move=> s h [Z [next [HZ [r_x [r_z [r_m [Hone [r_k [r_alpha [Hmem [r_ext [Hinv [Hextk [r_X_ [r_Y_ [ [r_M_ [r_int_ [Hquot [Hm2 [Hm3 r_t]]]]]]]]]]]]]]]]]]]]].

exists Z, next, 1%nat.
repeat (split; trivial).

by rewrite r_int_ u2Z_Z2u.
rewrite r_int_ r_k u2Z_Z2u // (_ : 1 = Z_of_nat 1) //.
by apply inj_le, (le_lt_trans _ _ _ (le_O_n next) Hextk).
by apply Zlt_le_trans with (2 * Zbeta 1 - 2).
rewrite r_t; ring.

case: Hinv => K [Hinv1 Hinv2].
exists K; split; last by done.
rewrite Sum_hole_last'; last by rewrite app_length /= HZ plus_comm.
have -> : u2Z (store.hi s [.||] store.lo s) * Zbeta (next + 1) =
  Zbeta next * (Zbeta 1 * u2Z (store.hi s [.||] store.lo s)) by rewrite Zbeta_is_exp; ring.
rewrite minus_Sn_1.
have -> : Zbeta (S next) * Sum nk (tail (Z ++ [C]_s :: nil)) =
  Zbeta next * (Zbeta 1 * Sum nk (tail (Z ++ [C]_s :: nil))) by rewrite Zbeta_S; ring.
rewrite Sum_Zpower_Zmult Hquot.
apply trans_eq with (Zbeta next *
  (Sum (S nk) (zero32 :: tail (Z ++ [C]_s :: nil)) + u2Z (nth 0 Z zero32)) +
  Zbeta next * (u2Z [quot]_s * u2Z (nth 0 M zero32) + u2Z (nth next X zero32) * u2Z (nth 0 X zero32))).
- rewrite Hm2 [mult _ _]/= /zero32; ring.
- rewrite Sum_head_swap0 tail_app; last by rewrite HZ; destruct nk => //; apply lt_O_Sn.
  rewrite app_comm_cons list_tail; last by rewrite HZ; destruct nk => //; apply lt_O_Sn.
  rewrite Hquot Hinv1 Sum_1 Sum_1 /zero32; ring.

apply while.hoare_seq with (fun s h => (exists Z, exists next, exists nint_, length Z = nk /\
  [x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\ [one]_s = one32 /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  u2Z [ext]_s = Z_of_nat next /\ (next < nk)%nat /\ [X_]_s = nth next X zero32 /\
  u2Z [int_]_s = Z_of_nat nint_ /\ (1 <= nint_)%nat /\ u2Z [int_]_s <= u2Z [k]_s /\
  store.utoZ s < 2 * Zbeta 1 - 1 /\ u2Z [t]_s = u2Z vz + 4 * (Z_of_nat nint_ - 1) /\
  (exists K, Zbeta (S next) * Sum_hole (S nk) (nint_-1) (Z ++ [C]_s :: nil) +
    u2Z (store.hi s [.||] store.lo s) * Zbeta (next + nint_) =
    Sum next X * Sum nk X + Sum nint_ X * u2Z (nth next X zero32) * Zbeta next +
    Sum nint_ M * u2Z [quot]_s * Zbeta next + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next))
/\ ~~ (eval_b (bne int_ k) s)).

apply while.hoare_while.

lwxs Y int y;

apply hoare_lwxs_back_alt'' with (fun s h => exists Z, exists next, exists nint_, length Z = nk /\
  [x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\
  [one]_s = one32 /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\ u2Z [ext]_s = Z_of_nat next /\
  (next < nk)%nat /\ (nint_ < nk)%nat /\ [X_]_s = nth next X zero32 /\
  u2Z [int_]_s = Z_of_nat nint_ /\ (1 <= nint_)%nat /\
  store.utoZ s < 2 * Zbeta 1 - 1 /\ u2Z [t]_s = u2Z vz + 4 * (Z_of_nat nint_ - 1) /\
  (exists K, Zbeta (S next) * Sum_hole (S nk) (nint_ - 1) (Z ++ [C]_s :: nil) +
    u2Z (store.hi s [.||] store.lo s) * Zbeta (next + nint_) =
    Sum next X * Sum nk X + Sum nint_ X * u2Z (nth next X zero32) * Zbeta next +
    Sum nint_ M * u2Z [quot]_s * Zbeta next + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  [Y_]_s = nth nint_ X zero32).

move=> s h [[Z [next [nint_ [HZ [r_x [r_z [r_m [Hone [r_k [r_alpha [Hmem [r_ext [Hextk' [r_X_ [r_int_ [Hint_ [r_int_' [Hm2 [r_t Hinv]]]]]]]]]]]]]]]]]]] Hint_k].
rewrite /= in Hint_k. move/Zeq_boolP : Hint_k => Hint_k; rewrite r_int_ r_k in Hint_k.
have {Hint_k}Hint_k : nint_ <> nk by contradict Hint_k; rewrite Hint_k.
rewrite r_int_ r_k in r_int_'; apply Z_of_nat_le_inj in r_int_'.

exists (nth nint_ X zero32); split.
- Decompose_32 X nint_ X1 X2 HlenX1 HX'; last by rewrite Hx; apply le_neq_lt.
  rewrite HX' (decompose_equiv _ _ _ _ _ HlenX1) !assert_m.con_assoc_equiv assert_m.con_com_equiv !assert_m.con_assoc_equiv in Hmem.
  move: Hmem; apply monotony => // h'.
  apply mapsto_ext => //.
  by rewrite [mult]lock /= -lock shl_Z2u r_int_ inj_mult Zmult_comm.
- rewrite /update_store_lwxs.
  exists Z, next, nint_; repeat reg_upd; repeat (split; trivial).
  by Assert_upd.
  by apply le_neq_lt.

lwxs Z int z;

apply hoare_lwxs_back_alt'' with (fun s h => exists Z, exists next, exists nint_, length Z = nk /\
  [x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\ [one]_s = one32 /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  u2Z [ext]_s = Z_of_nat next /\ (next < nk)%nat /\ (nint_ < nk)%nat /\
  [X_]_s = nth next X zero32 /\ u2Z [int_]_s = Z_of_nat nint_ /\ (1 <= nint_)%nat /\
  store.utoZ s < 2 * Zbeta 1 - 1 /\ u2Z [t]_s = u2Z [z]_s + 4 * (Z_of_nat nint_ - 1) /\
  (exists K, Zbeta (S next) * Sum_hole (S nk) (nint_ - 1) (Z ++ [C]_s :: nil) +
    u2Z (store.hi s [.||] store.lo s) * Zbeta (next + nint_) =
    Sum next X * Sum nk X + Sum nint_ X * u2Z (nth next X zero32) * Zbeta next +
    Sum nint_ M * u2Z [quot]_s * Zbeta next + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  [Y_]_s = nth nint_ X zero32 /\ [Z_]_s = nth nint_ Z zero32).

move=> s h [Z [next [nint_ [HZ [r_x [r_z [r_m [Hone [r_k [r_alpha [Hmem [r_ext [Hextk' [Hint_' [r_X_ [r_int_' [Hint_ [Hm2 [r_t [Hinv r_Y_]]]]]]]]]]]]]]]]]]]].

exists (nth nint_ Z zero32); split.
- Decompose_32 Z nint_ Z1 Z2 HlenZ1 HZ'; last by rewrite HZ.
  rewrite HZ' (decompose_equiv _ _ _ _ _ HlenZ1) !assert_m.con_assoc_equiv assert_m.con_com_equiv !assert_m.con_assoc_equiv assert_m.con_com_equiv !assert_m.con_assoc_equiv in Hmem.
  move: Hmem; apply monotony => // h'.
  apply mapsto_ext => //.
  by rewrite [mult]lock /= -lock shl_Z2u r_int_' inj_mult Zmult_comm.
- exists Z, next, nint_; repeat reg_upd; repeat (split; trivial).
  by Assert_upd.
  by rewrite r_t r_z.

maddu X Y;

apply hoare_maddu with (fun s h => exists Z, exists next, exists nint_, length Z = nk /\
  [x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\ [one]_s = one32 /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  u2Z [ext]_s = Z_of_nat next /\ (next < nk)%nat /\ (nint_ < nk)%nat /\
  [X_]_s = nth next X zero32 /\ u2Z [int_]_s = Z_of_nat nint_ /\ (1 <= nint_)%nat /\
  store.utoZ s < Zbeta 2 /\ u2Z [t]_s = u2Z vz + 4 * (Z_of_nat nint_ - 1) /\
  [Y_]_s = nth nint_ X zero32 /\ [Z_]_s = nth nint_ Z zero32 /\
  (exists K, Zbeta (S next) * Sum_hole (S nk) (nint_ - 1) (Z ++ [C]_s :: nil) +
    store.utoZ s * Zbeta (next + nint_) = Sum next X * Sum nk X +
    Sum nint_ X * u2Z (nth next X zero32) * Zbeta next +
    Sum nint_ M * u2Z [quot]_s * Zbeta next +
    u2Z (nth next X zero32) * u2Z (nth nint_ X zero32) * Zbeta (next + nint_) + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next)).

move=> s h [Z [next [nint_ [HZ [r_x [r_z [r_m [Hone [r_k [r_alpha [Hmem [r_ext [Hextk' [Hint_' [ r_X_ [r_int_' [Hint_ [Hm2 [r_t [Hinv [r_Y_ r_Z_]]]]]]]]]]]]]]]]]]]]].

exists Z, next, nint_.

have Htmp : store.utoZ s < Zbeta 2 * (2 ^^ store.acx_size - 1) by apply Zlt_le_trans with (2 * Zbeta 1 - 1).

repeat reg_upd; repeat (split; trivial).
by Assert_upd.
rewrite store.utoZ_maddu //.
apply Zlt_le_trans with ((Zbeta 1 - 1) * (Zbeta 1 - 1) + (2 * Zbeta 1 - 1)); last by done.
apply Zplus_le_lt_compat; [by apply max_u2Z_umul | done].

by rewrite r_t r_z.

case: Hinv => K [Hinv1 Hinv2].
exists K; split; last by done. apply trans_eq with (Sum next X * Sum nk X +
 Sum nint_ X * u2Z (nth next X zero32) * Zbeta next + Sum nint_ M * u2Z [quot]_s * Zbeta next +
 K * Sum nk M + u2Z (nth next X zero32) * u2Z (nth nint_ X zero32) * Zbeta (next + nint_)).
- rewrite store.utoZ_maddu // store.utoZ_def store.utoZ_acx_beta2 //; last first.
    by apply Zlt_le_trans with (2 * Zbeta 1 - 1).
  rewrite u2Z_Z2u // -u2Z_umul -Hinv1 u2Z_concat -Zplus_0_r_reverse r_Y_ r_X_ // -Zplus_assoc.
  f_equal.
  rewrite (Zplus_comm (u2Z (nth next X zero32 [.*] nth nint_ X zero32))) Zmult_plus_distr_l Zmult_plus_distr_l.
  f_equal.
  by rewrite Zmult_plus_distr_l Zplus_comm.
- ring.

lwxs M int m;

apply hoare_lwxs_back_alt'' with (fun s h => exists Z, exists next, exists nint_, length Z = nk /\
  [x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\ [one]_s = one32 /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  u2Z [ext]_s = Z_of_nat next /\ (next < nk)%nat /\ (nint_ < nk)%nat /\
  [X_]_s = nth next X zero32 /\ u2Z [int_]_s = Z_of_nat nint_ /\ (1 <= nint_)%nat /\
  store.utoZ s < Zbeta 2 /\ u2Z [t]_s = u2Z vz + 4 * (Z_of_nat nint_ - 1) /\
  [Y_]_s = nth nint_ X zero32 /\ [Z_]_s = nth nint_ Z zero32 /\
  (exists K, Zbeta (S next) * Sum_hole (S nk) (nint_ - 1) (Z ++ [C]_s :: nil) +
    store.utoZ s * Zbeta (next + nint_) = Sum next X * Sum nk X +
    Sum nint_ X * u2Z (nth next X zero32) * Zbeta next +
    Sum nint_ M * u2Z [quot]_s * Zbeta next +
    u2Z (nth next X zero32) * u2Z (nth nint_ X zero32) * Zbeta (next + nint_) + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next)
  /\ [M_]_s = nth nint_ M zero32 ).

move=> s h [Z [next [nint_ [HZ [r_x [r_z [r_m [Hone [r_k [r_alpha [Hmem [r_ext [Hextk' [Hint_' [r_X_ [r_int_' [Hint_ [Hm2 [r_t [r_Y_ [r_Z_ Hinv]]]]]]]]]]]]]]]]]]]]].

exists (nth nint_ M zero32); split.
- Decompose_32 M nint_ M1 M2 HlenM1 HM'; last by rewrite Hm.
  rewrite HM' (decompose_equiv _ _ _ _ _ HlenM1) assert_m.con_com_equiv !assert_m.con_assoc_equiv assert_m.con_com_equiv !assert_m.con_assoc_equiv in Hmem.
  move: Hmem; apply monotony => // h'.
  apply mapsto_ext => //.
  by rewrite [mult]lock /= -lock shl_Z2u r_int_' inj_mult Zmult_comm.
- exists Z, next, nint_; repeat reg_upd; repeat (split; trivial).
  by Assert_upd.

maddu Z one;

apply hoare_maddu with (fun s h => exists Z, exists next, exists nint_, length Z = nk /\
  [x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\ [one]_s = one32 /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  u2Z [ext]_s = Z_of_nat next /\ (next < nk)%nat /\ (nint_ < nk)%nat /\
  [X_]_s = nth next X zero32 /\ u2Z [int_]_s = Z_of_nat nint_ /\ (1 <= nint_)%nat /\
  store.utoZ s < Zbeta 2 + Zbeta 1 - 1 /\ u2Z [t]_s = u2Z vz + 4 * (Z_of_nat nint_ - 1) /\
  [Y_]_s = nth nint_ X zero32 /\ [Z_]_s = nth nint_ Z zero32 /\ [M_]_s = nth nint_ M zero32 /\
  (exists K, Zbeta (S next) * Sum_hole (S nk) (nint_ - 1) (Z ++ [C]_s :: nil) +
    store.utoZ s * Zbeta (next + nint_) = Sum next X * Sum nk X +
    Sum nint_ X * u2Z (nth next X zero32) * Zbeta next +
    Sum nint_ M * u2Z [quot]_s * Zbeta next +
    u2Z (nth next X zero32) * u2Z (nth nint_ X zero32) * Zbeta (next + nint_) +
    u2Z (nth nint_ Z zero32) * Zbeta (next + nint_) + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next)).

move=> s h [Z [next [nint_ [HZ [r_x [r_z [r_m [Hone [r_k [r_alpha [Hmem [r_ext [Hextk' [ Hint_' [r_X_ [r_int_' [Hint_ [Hm2 [r_t [r_Y_ [r_Z_ [Hinv r_M_]]]]]]]]]]]]]]]]]]]]]].

exists Z, next, nint_.

have Htmp : store.utoZ s < Zbeta 2 * (2 ^^ store.acx_size - 1) by apply Zlt_le_trans with (Zbeta 2 * 1).

repeat reg_upd; repeat (split; trivial).
by Assert_upd.
rewrite store.utoZ_maddu //.
apply Zlt_le_trans with ((Zbeta 1 - 1) + Zbeta 2); last by done.
apply Zplus_le_lt_compat; last by done.
rewrite Hone umul_1 u2Z_zext //.
apply Zle_minus_1; rewrite /Zbeta; by apply max_u2Z.

case: Hinv => K [Hinv1 Hinv2].
exists K; split; last by done. rewrite store.utoZ_maddu // Hone umul_1 u2Z_zext //.
apply trans_eq with (Zbeta (S next) * Sum_hole (S nk) (nint_ - 1) (Z ++ [C]_s :: nil) +
     store.utoZ s * Zbeta (next + nint_) + u2Z (nth nint_ Z zero32) * Zbeta (next + nint_)).
by rewrite -r_Z_ {1}(Zplus_comm (u2Z [Z_]_s)) Zmult_plus_distr_l Zplus_assoc.
rewrite Hinv1; ring.

maddu quot M;

apply hoare_maddu with (fun s h => exists Z, exists next, exists nint_, length Z = nk /\
  [x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\ [one]_s = one32 /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  u2Z [ext]_s = Z_of_nat next /\ (next < nk)%nat /\ (nint_ < nk)%nat /\
  [X_]_s = nth next X zero32 /\ u2Z [int_]_s = Z_of_nat nint_ /\ (1 <= nint_)%nat /\
  store.utoZ s < 2 * Zbeta 2 - Zbeta 1 /\ u2Z [t]_s = u2Z vz + 4 * (Z_of_nat nint_ - 1) /\
  [Y_]_s = nth nint_ X zero32 /\ [Z_]_s = nth nint_ Z zero32 /\ [M_]_s = nth nint_ M zero32 /\
  (exists K, Zbeta (S next) * Sum_hole (S nk) (nint_ - 1) (Z ++ [C]_s :: nil) +
    store.utoZ s * Zbeta (next + nint_) = Sum next X * Sum nk X +
    Sum nint_ X * u2Z (nth next X zero32) * Zbeta next +
    Sum nint_ M * u2Z [quot]_s * Zbeta next +
    u2Z (nth next X zero32) * u2Z (nth nint_ X zero32) * Zbeta (next + nint_) +
    u2Z (nth nint_ Z zero32) * Zbeta (next + nint_) +
    u2Z (nth nint_ M zero32) * u2Z [quot]_s * Zbeta (next + nint_) + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next)).

move=> s h [Z [next [nint_ [HZ [r_x [r_z [r_m [Hone [r_k [r_alpha [Hmem [r_ext [Hextk' [Hint_' [r_X_ [r_int_' [Hint_ [Hm2 [r_t [r_Y_ [r_Z_ [r_M_ Hinv]]]]]]]]]]]]]]]]]]]]]].
exists Z, next, nint_.

have Htmp : store.utoZ s < Zbeta 2 * (2 ^^ store.acx_size - 1) by apply Zlt_le_trans with (Zbeta 2 + Zbeta 1 - 1).

repeat reg_upd; repeat (split; trivial).
by Assert_upd.
repeat (split; trivial).

rewrite store.utoZ_maddu //.
apply Zlt_le_trans with ((Zbeta 1 - 1) * (Zbeta 1 - 1) + (Zbeta 2 + Zbeta 1 - 1)); last by done.
apply Zplus_le_lt_compat; [by apply max_u2Z_umul | done].

case: Hinv => K [Hinv1 Hinv2].
exists K; split; last by done. rewrite store.utoZ_maddu // Zmult_plus_distr_l.
apply trans_eq with (Zbeta (S next) * Sum_hole (S nk) (nint_ - 1) (Z ++ [C]_s :: nil) +
  store.utoZ s * Zbeta (next + nint_) + (u2Z ([quot]_s [.*] [M_]_s) * Zbeta (next + nint_))).
by rewrite (Zplus_comm (u2Z ([quot]_s [.*] [M_]_s) * Zbeta (next + nint_))) Zplus_assoc.
rewrite Hinv1 u2Z_umul r_M_; ring.

addiu int int one16;

apply hoare_addiu with (fun s h => exists Z, exists next, exists nint_, length Z = nk /\
  [x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\ [one]_s = one32 /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  u2Z [ext]_s = Z_of_nat next /\ (next < nk)%nat /\ (nint_ <= nk)%nat /\
  [X_]_s = nth next X zero32 /\ u2Z [int_]_s = Z_of_nat nint_ /\ (2 <= nint_)%nat /\
  store.utoZ s < 2 * Zbeta 2 - Zbeta 1 /\ u2Z [t]_s = u2Z vz + 4 * (Z_of_nat nint_ - 2) /\
  (exists K, Zbeta (S next) * Sum_hole (S nk) (nint_ - 2) (Z ++ [C]_s :: nil) +
    store.utoZ s * Zbeta (next + nint_ - 1) = Sum next X * Sum nk X +
    Sum (nint_-1) X * u2Z (nth next X zero32) * Zbeta next +
    Sum (nint_-1) M * u2Z [quot]_s * Zbeta next +
    u2Z (nth next X zero32) * u2Z (nth (nint_-1) X zero32) * Zbeta (next + nint_ - 1)+
    u2Z (nth (nint_-1) Z zero32) * Zbeta (next + nint_ - 1) +
    u2Z (nth (nint_-1) M zero32) * u2Z [quot]_s * Zbeta (next + nint_ - 1) + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next)).

move=> s h [Z [next [nint_ [HZ [r_x [r_z [r_m [Hone [r_k [r_alpha [Hmem [r_ext [Hextk' [Hint_' [r_X_ [r_int_' [Hint_ [Hm2 [r_t [r_Y_ [r_Z_ [r_M_ Hinv]]]]]]]]]]]]]]]]]]]]]].

exists Z, next, (S nint_); repeat reg_upd; repeat (split; trivial).
by Assert_upd.

rewrite sext_Z2u // u2Z_add_Z2u //.
- by rewrite r_int_' Z_S.
- rewrite r_int_'.
  apply Zle_lt_trans with (Z_of_nat nk).
  rewrite (_ : 1 = Z_of_nat 1) // -inj_plus plus_comm; by apply inj_le.
  eapply Zle_lt_trans; last by apply Hnz.
  apply Zle_plus_trans; first by apply min_u2Z.
  rewrite Zmult_comm; apply Zle_scale; last by done.
  by apply Zle_0_nat.
by apply le_n_S.

rewrite r_t Z_S; ring.

case: Hinv => K [Hinv1 Hinv2].
exists K; split; last by done. rewrite minus_Sn_1.
have -> : (next + S nint_ - 1 = next + nint_)%nat.
  rewrite plus_minus_assoc; by [rewrite minus_Sn_1 | apply le_n_S, le_O_n].
by rewrite Hinv1.

mflhxu Z;

apply hoare_mflhxu with (fun s h => exists Z, exists next, exists nint_, length Z = nk /\
  [x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\
  [one]_s = one32 /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\ u2Z [ext]_s = Z_of_nat next /\
  (next < nk)%nat /\ (nint_ <= nk)%nat /\ [X_]_s = nth next X zero32 /\
  u2Z [int_]_s = Z_of_nat nint_ /\ (2 <= nint_)%nat /\
  store.utoZ s < 2 * Zbeta 1 - 1 /\ u2Z [t]_s = u2Z vz + 4 * (Z_of_nat nint_ - 2) /\
  (exists K, Zbeta (S next) * Sum_hole (S nk) (nint_ - 2) (Z ++ [C]_s :: nil) +
    u2Z (store.hi s [.||] store.lo s) * Zbeta (next + nint_) +
    u2Z [Z_]_s * Zbeta (next + nint_ - 1) = Sum next X * Sum nk X +
    Sum (nint_-1) X * u2Z (nth next X zero32) * Zbeta next +
    Sum (nint_-1) M * u2Z [quot]_s * Zbeta next +
    u2Z (nth next X zero32) * u2Z (nth (nint_-1) X zero32) * Zbeta (next + nint_ - 1) +
    u2Z (nth (nint_-1) Z zero32) * Zbeta (next + nint_ - 1) +
    u2Z (nth (nint_-1) M zero32) * u2Z [quot]_s * Zbeta (next + nint_ - 1) + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next)).

move=> s h [Z [next [nint_ [HZ [r_x [r_z [r_m [Hone [r_k [r_alpha [Hmem [r_ext [Hextk' [Hint_' [r_X_ [r_int_' [Hint_ [Hm2 [r_t Hinv]]]]]]]]]]]]]]]]]]].

exists Z, next, nint_; repeat reg_upd; repeat (split; trivial).
by Assert_upd.

apply store.mflhxu_kbeta1_utoZ.
apply Zlt_le_trans with (2 * Zbeta 2 - Zbeta 1); [by rewrite store.utoZ_upd | done].
case: Hinv => K [Hinv1 Hinv2].
exists K; split; last by done.
rewrite -Hinv1 u2Z_concat store.hi_mflhxu_op store.lo_mflhxu_op u2Z_zext store.utoZ_def -Zplus_assoc.
f_equal.
rewrite -Zbeta1_Zpower2 3!Zmult_plus_distr_l -3!Zmult_assoc -3!Zbeta_is_exp.
rewrite le_plus_minus_r; last first.
  rewrite plus_comm. apply le_plus_trans. by apply le_trans with 2%nat; auto.
have -> : (2 + (next + nint_ - 1) = 1 + (next + nint_))%nat.
  rewrite -plus_minus_assoc; last first.
    rewrite plus_comm; apply le_plus_trans. by apply le_trans with 2%nat; auto.
  rewrite plus_comm plus_minus_assoc; by [rewrite /= -(plus_comm 1%nat) | auto].
repeat reg_upd; ring.

addiu t t four16;

apply hoare_addiu with (fun s h => exists Z, exists next, exists nint_, length Z = nk /\
  [x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\
  [one]_s = one32 /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  u2Z [ext]_s = Z_of_nat next /\ (next < nk)%nat /\ (nint_ <= nk)%nat /\
  [X_]_s = nth next X zero32 /\ u2Z [int_]_s = Z_of_nat nint_ /\ (2 <= nint_)%nat /\
  store.utoZ s < 2 * Zbeta 1 - 1 /\ u2Z [t]_s = u2Z vz + 4 * (Z_of_nat nint_-1) /\
  (exists K, Zbeta (S next) * Sum_hole (S nk) (nint_ - 2) (Z ++ [C]_s :: nil) +
    u2Z (store.hi s [.||] store.lo s) * Zbeta (next + nint_) +
    u2Z [Z_]_s * Zbeta (next + nint_ - 1) = Sum next X * Sum nk X +
    Sum (nint_-1) X * u2Z (nth next X zero32) * Zbeta next +
    Sum (nint_-1) M * u2Z [quot]_s * Zbeta next +
    u2Z (nth next X zero32) * u2Z (nth (nint_-1) X zero32) * Zbeta (next + nint_ - 1) +
    u2Z (nth (nint_-1) Z zero32) * Zbeta (next + nint_ - 1) +
    u2Z (nth (nint_-1) M zero32) * u2Z [quot]_s * Zbeta (next + nint_ - 1) + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next)).

move=> s h [Z [next [nint_ [HZ [r_x [r_z [r_m [Hone [r_k [r_alpha [Hmem [r_ext [Hextk' [Hint_' [r_X_ [r_int_' [Hint_ [Hm2 [r_t Hinv]]]]]]]]]]]]]]]]]]].

exists Z, next, nint_; repeat reg_upd; repeat (split; trivial).
by Assert_upd.

rewrite sext_Z2u // u2Z_add_Z2u //.
- rewrite r_t; ring.
- rewrite -Zbeta1_Zpower2 r_t.
  eapply Zle_lt_trans; last by apply Hnz.
  rewrite -Zplus_assoc; apply Zplus_le_compat_l.
  rewrite -{2}(Zmult_1_r 4) -Zmult_plus_distr_r -Zplus_assoc (_ : - 2 + 1 = - Z_of_nat 1) //.
  apply Zmult_le_compat => //.
  apply Zle_plus_trans_L => //; by apply inj_le.
  apply Zle_left, inj_le; by apply le_trans with 2%nat; auto.

sw Z mfour16 t

apply hoare_sw_back'.
move=> s h [Z [next [nint_ [HZ [r_x [r_z [r_m [Hone [r_k [r_alpha [Hmem [r_ext [Hextk' [Hint_' [r_X_ [r_int_' [Hint_ [Hm2 [r_t Hinv]]]]]]]]]]]]]]]]]]].

exists (int_e (nth (nint_ - 2) Z zero32)).

have Htmp: [z]_s [.+] Z2u 32 (Z_of_nat (4 * (nint_ - 2))) = [t]_s[.+]sext 16 mfour16.
  rewrite /mfour16 sext_Z2s // r_z; apply u2Z_inj.
  rewrite u2Z_add_Z2s //.
  rewrite u2Z_add_Z_of_nat.
  rewrite r_t inj_mult inj_minus1 //; ring.
  rewrite inj_mult inj_minus1 // -Zbeta1_Zpower2 [Z_of_nat _]/=.
  eapply Zle_lt_trans; last by apply Hnz.
  apply Zplus_le_compat_l, Zmult_le_compat_l; last by done.
  rewrite -inj_minus1 //.
  by apply inj_le, le_minus_trans.
  rewrite r_t -Zplus_assoc (_ : -4 = 4 * ( -1 )) // -Zmult_plus_distr_r.
  apply Zle_plus_trans; first by apply min_u2Z.
  rewrite Zmult_comm; apply Zmult_gt_0_le_0_compat; first by done.
  rewrite -Zplus_assoc /= (_ : -2 = - Z_of_nat 2) //.
  by apply Zle_left, inj_le.

Decompose_32 Z (nint_ - 2)%nat Z1 Z2 HlenZ1 HZ'; last first.
  rewrite HZ /lt.
  apply le_trans with nint_; last by done.
  rewrite minus_Sn_m //=; by apply le_minus_trans.
rewrite HZ' (decompose_equiv _ _ _ _ _ HlenZ1) !assert_m.con_assoc_equiv assert_m.con_com_equiv !assert_m.con_assoc_equiv assert_m.con_com_equiv !assert_m.con_assoc_equiv in Hmem.
move: Hmem; apply monotony => // ht.
by apply mapsto_ext.

apply currying => h' H'; simpl app in H'.

exists (update_list Z (nint_ - 2)%nat [Z_]_s), next, nint_; repeat (split; trivial).
by apply len_update_list.
rewrite HZ' update_list_app HlenZ1 // -minus_n_n /= (decompose_equiv _ _ _ _ _ HlenZ1).
assoc_comm H'.
move: H'; by apply mapsto_ext.

apply le_trans with 2%nat; [by repeat constructor | done].
rewrite r_int_' r_k; by apply inj_le.

case : Hinv => K [Hinv1 Hinv2].
exists K; split; last by done.



apply Zplus_reg_l with (Zbeta (S next) * u2Z (nth (nint_ - 1) Z zero32) * Zbeta (nint_ - 2)).
rewrite Zplus_assoc -Zmult_assoc -(Zmult_plus_distr_r (Zbeta (S next))).


rewrite (Zplus_comm (u2Z (nth (nint_ - 1) Z zero32) * Zbeta (nint_ - 2))).
have -> : Sum_hole (S nk) (nint_ - 1) (update_list Z (nint_ - 2) [Z_]_s ++ [C]_s :: nil) + u2Z (nth (nint_ - 1) Z zero32) * Zbeta (nint_ - 2) = Sum_hole (S nk) (nint_ - 2) (Z ++ [C]_s::nil) + u2Z [Z_]_s * Zbeta (nint_ - 2).
  have H_ : (length (update_list Z (nint_ - 2) [Z_]_s ++ [C]_s :: nil) = S nk)%nat.
    by rewrite app_length (len_update_list nk) //= plus_comm.
  have H1__ : (nint_ - 1 < nk)%nat.
    rewrite /lt minus_Sn_m; last by apply le_trans with 2%nat; auto.
    by rewrite /= -minus_n_O.
  have H1_ : (nint_ - 1 < S nk)%nat.
    apply le_trans with nk; [done | by apply le_S].
  have H1___ : (nint_ - 1 - 1 < nk)%nat.
    apply le_lt_trans with (nint_ - 1)%nat; last by done.
    by apply le_minus_trans, le_refl.
  move/(Sum_hole_shift _ _ H_ _) : H1_ => {H_}H_.
  rewrite app_nth1 in H_; last by rewrite (len_update_list nk).
  rewrite app_nth1 in H_; last by rewrite (len_update_list nk).
  rewrite nth_update_list' in H_; last first.
    destruct nint_; first by apply le_Sn_O in Hint_.
    destruct nint_; first by apply le_S_n, le_Sn_O in Hint_.
    rewrite /= -minus_n_O; by move: (n_Sn nint_); auto.
  rewrite (_ : nint_ - 1 - 1 = nint_ - 2)%nat in H_; last by rewrite minus_minus.
  rewrite nth_update_list in H_; last by rewrite HZ; rewrite minus_minus in H1___.
  have [->//] : Sum_hole (S nk) (nint_ - 2) (Z ++ [C]_s :: nil) =
    Sum_hole (S nk) (nint_ - 2) (update_list Z (nint_ - 2) [Z_]_s ++ [C]_s :: nil).
  rewrite -update_list_app'; last by rewrite HZ; rewrite minus_minus in H1___.
  rewrite -Sum_hole_update_list //.
  by rewrite app_length /= HZ plus_comm.
  by rewrite /Zbeta (mult_comm _ 32).


have Htmp2 : (S next + (nint_ - 2) = next + nint_ - 1)%nat.
  rewrite plus_Snm_nSm minus_Sn_m //= plus_minus_assoc //.
  by apply le_trans with 2%nat; auto.

apply trans_eq with (Zbeta (S next) * Sum_hole (S nk) (nint_ - 2) (Z ++ [C]_s :: nil) +
 u2Z (store.hi s [.||] store.lo s) * Zbeta (next + nint_) +
  u2Z [Z_]_s * (Zbeta (S next) * Zbeta (nint_ - 2))).
ring.

rewrite -Zbeta_is_exp Htmp2 Hinv1{Hinv1}.

apply trans_eq with ((Sum (nint_ - 1) X * u2Z (nth next X zero32) * Zbeta next +
  u2Z (nth next X zero32) * u2Z (nth (nint_ - 1) X zero32) * Zbeta (next + nint_ - 1)) +
(Sum (nint_ - 1) M * u2Z [quot]_s * Zbeta next +
  u2Z (nth (nint_ - 1) M zero32) * u2Z [quot]_s * Zbeta (next + nint_ - 1))
+ K * Sum nk M + Sum next X * Sum nk X
+ u2Z (nth (nint_ - 1) Z zero32) * Zbeta (next + nint_ - 1)).
ring.

apply trans_eq with (Sum nint_ X * u2Z (nth next X zero32) * Zbeta next +
  Sum nint_ M * u2Z [quot]_s * Zbeta next
  + K * Sum nk M + Sum next X * Sum nk X
  + (u2Z (nth (nint_ - 1) Z zero32) * (Zbeta (S next) * Zbeta (nint_ - 2))) ); last by ring.

f_equal; last by rewrite -Zbeta_is_exp Htmp2.

do 3 f_equal.
apply trans_eq with ((Sum (nint_ - 1) X + u2Z (nth (nint_ - 1) X zero32) *
  Zbeta (nint_ - 1)) * (u2Z (nth next X zero32) * Zbeta next)).
- rewrite plus_minus_assoc; last by apply le_trans with 2%nat; auto.
  rewrite Zbeta_is_exp; ring.
- rewrite (Zmult_comm _ (Zbeta (nint_ - 1))) {1}/Zbeta -Sum_remove_last.
  rewrite minus_Sn_m; last by apply le_Sn_le.
  by rewrite minus_Sn_1 Zmult_assoc.

apply trans_eq with ((Sum (nint_ - 1) M + u2Z (nth (nint_ - 1) M zero32) *
 Zbeta (nint_ - 1)) * (u2Z [quot]_s * Zbeta next)).
- rewrite plus_minus_assoc; last by apply le_trans with 2%nat; auto.
  rewrite Zbeta_is_exp; ring.
- rewrite (Zmult_comm _ (Zbeta (nint_ - 1))) {1}/Zbeta -Sum_remove_last minus_Sn_m; last by apply le_Sn_le.
  by rewrite minus_Sn_1 Zmult_assoc.

maddu C one;

apply hoare_maddu with (fun s h => exists Z, exists next, length Z = nk /\
  [x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\ [one]_s = one32 /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  u2Z [ext]_s = Z_of_nat next /\ (next < nk)%nat /\
  [X_]_s = nth next X zero32 /\ u2Z [int_]_s = Z_of_nat nk /\
  store.utoZ s < 3 * Zbeta 1 - 2 /\ u2Z [t]_s = u2Z vz + 4 * (Z_of_nat nk - 1) /\
  (exists K, Zbeta (S next) * Sum (nk - 1) Z + store.utoZ s * Zbeta (next + nk) =
    Sum next X * Sum nk X + Sum nk X * u2Z (nth next X zero32) * Zbeta next +
    Sum nk M * u2Z [quot]_s * Zbeta next + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next)).

move=> s h [[Z [next [nint_ [HZ [r_x [r_z [r_m [Hone [r_k [r_alpha [Hmem [r_ext [Hextk' [Hint_' [r_int_' [r_X_ [Hint_ [Hm2 [r_t Hinv]]]]]]]]]]]]]]]]]]] Hint_k].
rewrite /= r_int_' r_k in Hint_k.
move/negPn : Hint_k; move/Zeq_boolP; move/Z_of_nat_inj => ?; subst nint_.

exists Z, next.

have Htmp : store.utoZ s < Zbeta 2 * (2 ^^ store.acx_size - 1) by apply Zlt_le_trans with (2 * Zbeta 1 - 1).

repeat reg_upd; repeat (split; trivial).
by Assert_upd.
rewrite store.utoZ_maddu // Hone umul_1 u2Z_zext //.
apply Zlt_le_trans with ((Zbeta 1 - 1) + (2 * Zbeta 1 - 1)); last by done.
apply Zplus_le_lt_compat; last by done.
apply Zle_minus_1; by apply max_u2Z.

case : Hinv => K [Hinv1 Hinv2].
exists K; split; last by done. rewrite -Hinv1 store.utoZ_maddu // Hone umul_1 u2Z_zext [minus _ _]/=.
rewrite Zmult_plus_distr_l Zplus_assoc /Sum_hole // store.utoZ_def store.utoZ_acx_beta2; last by apply Zlt_le_trans with (2 * Zbeta 1 - 1).
rewrite u2Z_Z2u; last by split; by [apply Zle_refl | apply Zpower_0].
rewrite Zmult_0_l -Zplus_0_r_reverse u2Z_concat.
have [Z' [tl H ] ] : exists Z', exists tl, Z = Z' ++ tl :: nil.
  apply list_last. rewrite HZ. apply le_lt_trans with next; [by apply le_0_n | assumption].
rewrite {2}H app_ass.
have H0 : (length Z' = nk - 1)%nat.
  rewrite H app_length /= in HZ; apply plus_minus; by rewrite plus_comm.
rewrite (idel_app _ Z' H0 _ tl ([C]_s :: nil)) //.
move: (Sum_remove_last _ (Z' ++ [C]_s :: nil) (nk - 1)) => H1.
pattern (Sum (nk - 1) (Z' ++ [C]_s :: nil)) in H1.
rewrite <-Sum_beyond in H1; last by rewrite H0.
rewrite app_nth2 // in H1; last by rewrite H0.
rewrite (_ : nk - 1 - length Z' = 0)%nat in H1; last by rewrite H0 -minus_n_n.
rewrite (_ : S (nk - 1) = nk) in H1; last by rewrite minus_Sn_m //= -minus_n_O.
rewrite minus_Sn_1 H1 (Zmult_plus_distr_r (Zbeta (S next))).
have <- : Sum (nk - 1) Z = Sum (nk - 1) Z' by rewrite H -Sum_beyond.
rewrite -Zbeta_power Zmult_assoc -Zbeta_is_exp.
have -> : (S next + (nk - 1) = next + nk)%nat by rewrite plus_Snm_nSm minus_Sn_m // minus_Sn_1.
by rewrite (Zmult_comm (Zbeta (next + nk))) (Zplus_comm (u2Z (store.lo s))).

mflhxu Z;

apply hoare_mflhxu with (fun s h => exists Z, exists next, length Z = nk /\
  [x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\
  [one]_s = one32 /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\ u2Z [ext]_s = Z_of_nat next /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32 /\ store.utoZ s < 3 /\
  u2Z [t]_s = u2Z vz + 4 * (Z_of_nat nk - 1) /\
  (exists K, Zbeta (S next) * Sum (nk - 1) Z + u2Z (store.lo s) * Zbeta (next + nk + 1) +
    u2Z [Z_]_s * Zbeta (next + nk) = Sum next X * Sum nk X +
    Sum nk X * u2Z (nth next X zero32) * Zbeta next +
    Sum nk M * u2Z [quot]_s * Zbeta next + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M < 2 * Sum nk M * Zbeta next)).

move=> s h [Z [next [HZ [r_x [r_z [r_m [Hone [r_k [r_alpha [Hmem [r_ext [Hextk' [r_X_ [r_int_ [Hm2 [r_t Hinv]]]]]]]]]]]]]]]].

exists Z, next; repeat reg_upd; repeat (split; trivial).
by Assert_upd.
apply store.mflhxu_kbeta1_utoZ.
apply Zlt_trans with (3 * Zbeta 1 - 2); [by rewrite store.utoZ_upd | done].
case: Hinv => K [Hinv1 Hinv2].
exists K; split; last by done. rewrite -Hinv1 store.lo_mflhxu_op store.utoZ_def store.utoZ_acx_beta2; last by apply Zlt_le_trans with (3 * Zbeta 1 -2).
rewrite u2Z_Z2u; last by split; [apply Zle_refl | apply Zpower_0].
rewrite Zmult_0_l -Zplus_0_r_reverse Zmult_plus_distr_l -Zmult_assoc -Zbeta_is_exp (plus_comm 1).
repeat reg_upd; ring.

addiu ext ext one16;

apply hoare_addiu with (fun s h => exists Z, exists next, length Z = nk /\
  [x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\ [one]_s = one32 /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  u2Z [ext]_s = Z_of_nat next /\ (1 <= next <= nk)%nat /\
  store.utoZ s < 3 /\ u2Z [t]_s = u2Z vz + 4 * (Z_of_nat nk - 1) /\
  (exists K, Zbeta next * Sum (nk - 1) Z + u2Z (store.lo s) * Zbeta (next + nk) +
    u2Z [Z_]_s * Zbeta (next + nk - 1) = Sum (next-1) X * Sum nk X +
    Sum nk X * u2Z (nth (next-1) X zero32) * Zbeta (next-1) +
    Sum nk M * u2Z [quot]_s * Zbeta (next-1) + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M + (Zbeta 1 - 1) * (Zbeta (next - 1) * Sum nk M)
    < 2 * Sum nk M * Zbeta next)).

move=> s h [Z [next [HZ [r_x [r_z [r_m [Hone [r_k [r_alpha [Hmem [r_ext [Hextk' [r_X_ [Hm2 [r_t Hinv]]]]]]]]]]]]]]].

exists Z, (S next); repeat reg_upd; repeat (split; trivial).
by Assert_upd.
rewrite sext_Z2u // u2Z_add_Z2u // r_ext.
by rewrite Z_S.
apply Zle_lt_trans with (Z_of_nat nk).
rewrite (_ : 1 = Z_of_nat 1) // -inj_plus plus_comm; by apply inj_le.
rewrite -r_k; by apply max_u2Z.
by apply le_n_S, le_0_n.

case: Hinv => K [Hinv1 Hinv2].
exists K; split.
- by rewrite !minus_Sn_1 -Hinv1 -(plus_comm 1) plus_assoc -/(1 + next)%nat.
-
  rewrite Sum_remove_last Zmult_plus_distr_l.
  apply Zlt_le_trans with (2 * Sum nk M * Zbeta next + u2Z (nth next X zero32) * Zbeta next * Sum nk X +
    (Zbeta 1 - 1) * Zbeta (S next - 1) * Sum nk M).
  apply Zplus_lt_le_compat.
  rewrite -Zbeta_power (Zmult_comm (Zbeta next)) /zero32 Zplus_comm Zplus_assoc;
    by apply Zplus_lt_le_compat; [rewrite Zplus_comm | apply Zle_refl].
  rewrite Zmult_assoc; by apply Zle_refl.
  apply Zle_trans with (2 * Sum nk M * Zbeta next + (Zbeta 1 - 1) * Zbeta next * Sum nk X +
    (Zbeta 1 - 1) * Zbeta (S next - 1) * Sum nk M).
  apply Zplus_le_compat_r, Zplus_le_compat_l.
  rewrite -2!Zmult_assoc.
  apply Zmult_le_compat_r.
  apply Zle_minus_1; rewrite /Zbeta; by apply max_u2Z.
  apply Zmult_le_0_compat; by [apply Zbeta_0' | apply min_Sum].
  rewrite -Zplus_assoc !minus_Sn_1.
  apply Zle_trans with (2 * Sum nk M * Zbeta next +
    ((Zbeta 1 - 1) * Zbeta next * Sum nk M + (Zbeta 1 - 1) * Zbeta next * Sum nk M)).
  apply Zplus_le_compat_l, Zplus_le_compat_r, Zmult_le_compat_l.
  by apply Zlt_le_weak.
  apply Zmult_le_0_compat; [done | by apply Zbeta_0'].
  suff: 2 * Sum nk M * Zbeta next + ((Zbeta 1 - 1) * Zbeta next * Sum nk M + (Zbeta 1 - 1) * Zbeta next * Sum nk M)
    = 2 * Sum nk M * Zbeta (S next) by move=> ->; apply Zle_refl.
  rewrite (Zbeta_S next); ring.

sw Z zero16 t;

apply hoare_sw_back'' with (fun s h => exists Z, exists next, length Z = nk /\
  [x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\
  [one]_s = one32 /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  u2Z [ext]_s = Z_of_nat next /\ (1 <= next <= nk)%nat /\
  store.utoZ s < 3 /\ u2Z [t]_s = u2Z vz + 4 * (Z_of_nat nk - 1) /\
  (exists K, Zbeta next * Sum nk Z + u2Z (store.lo s) * Zbeta (next + nk) =
    Sum (next-1) X * Sum nk X + Sum nk X * u2Z (nth (next-1) X zero32) * Zbeta (next-1) +
    Sum nk M * u2Z [quot]_s * Zbeta (next-1) + K * Sum nk M /\
    Sum next X * Sum nk X + K * Sum nk M + (Zbeta 1 - 1)*(Zbeta (next - 1) * Sum nk M) < 2 * Sum nk M * Zbeta next)).

move=> s h [Z [next [HZ [r_x [r_z [r_m [Hone [r_k [r_alpha [Hmem [r_ext [Hextk' [Hm2 [r_t Hinv]]]]]]]]]]]]]].

have [lst1 [last H0 ] ] : exists Z', exists tl, Z = Z' ++ tl :: nil.
  apply list_last. rewrite HZ. apply le_trans with next; tauto.

have Hlenlst1 : length lst1 = (nk - 1)%nat by rewrite -HZ H0 app_length /= plus_comm minus_plus.

have Htmp : [ add_e (var_e t) (int_e (sext 16 zero16)) ]e_ s =
    [ add_e (var_e z) (int_e (Z2u 32 (Z_of_nat (4 * (nk - 1))))) ]e_ s.
  rewrite [mult]lock /= -lock sext_0 add_0; apply u2Z_inj.
  rewrite u2Z_add_Z_of_nat.
  rewrite inj_mult inj_minus1 //; last by destruct nk => //; by apply le_n_S, le_O_n.
  rewrite r_t r_z; simpl Z_of_nat; ring.
  rewrite inj_mult inj_minus1 //; last by destruct nk => //; by apply le_n_S, le_O_n.
  rewrite r_z; simpl Z_of_nat.
  eapply Zle_lt_trans; last by apply Hnz.
  apply Zplus_le_compat_l.
  apply Zmult_le_compat_l; last by done.
  rewrite (_ : 1 = Z_of_nat 1) // -inj_minus1 //; last by apply le_trans with next; tauto.
  by apply inj_le, le_minus_trans.

exists (int_e last).

rewrite H0 (decompose_equiv _ _ _ _ _ Hlenlst1) !assert_m.con_assoc_equiv assert_m.con_com_equiv !assert_m.con_assoc_equiv assert_m.con_com_equiv !assert_m.con_assoc_equiv in Hmem.
move: Hmem; apply monotony => // ht.
by apply mapsto_ext.
apply currying => h' H'; simpl assert_m.mapstos in H'.

exists (update_list Z (nk - 1) [Z_]_s); exists next.

repeat (split; trivial).
by apply len_update_list.
rewrite H0 update_list_app Hlenlst1 // -minus_n_n /= (decompose_equiv _ _ _ _ _ Hlenlst1).
simpl assert_m.mapstos.
assoc_comm H'.
move: H'; by apply mapsto_ext.

case: Hinv => K [Hinv1 Hinv2].
exists K; split; last by done. rewrite -Hinv1.
have -> : update_list Z (nk - 1) [Z_]_s = lst1 ++ [Z_]_s :: nil.
  rewrite H0 update_list_app /=.
  by rewrite Hlenlst1 -minus_n_n.
  by rewrite Hlenlst1.
rewrite (Sum_cut_last nk) //; last by rewrite app_length /= -HZ H0 app_length.
rewrite Zmult_plus_distr_r Zmult_assoc -Zbeta_is_exp plus_minus_assoc //; last by destruct nk => //; apply le_n_S, le_O_n.
rewrite H0 -(Sum_beyond 32 (nk - 1) lst1) //; ring.

mflhxu C

apply hoare_mflhxu'.

move=> s h [Z [next [HZ [r_x [r_z [r_m [Hone [r_k [r_alpha [Hmem [r_ext [Hextk' [Hm2 [r_t Hinv]]]]]]]]]]]]]].

exists Z, next; repeat reg_upd; repeat (split; trivial).
by Assert_upd.

rewrite r_ext r_k.

apply inj_le; by case: Hextk'.

rewrite inj_minus1 //; destruct nk => //; by apply le_n_S, le_O_n.

case: Hinv => K [Hinv1 Hinv2].
exists (K + u2Z [quot]_s * Zbeta (next - 1)); split.
- rewrite Sum_cut_last; last by rewrite app_length /= HZ plus_comm.
  rewrite !minus_Sn_1 Zmult_plus_distr_r Zmult_assoc -Zbeta_is_exp (Zmult_comm (Zbeta (next + nk))) Hinv1.
  have <- : Sum (next - 1) X + u2Z (nth (next - 1) X zero32) * Zbeta (next - 1) = Sum next X.
    rewrite -(Zmult_comm (Zbeta (next - 1))) /Zbeta -Sum_remove_last //.
    rewrite minus_Sn_m; last by case: Hextk'.
    by rewrite minus_Sn_1.
  ring.
- apply Zle_lt_trans with (Sum next X * Sum nk X + K * Sum nk M + ((Zbeta 1 - 1) * Zbeta (next - 1) * Sum nk M)); last by rewrite -Zmult_assoc.
  rewrite Zmult_plus_distr_l Zplus_assoc.
  apply Zplus_le_compat_l, Zmult_le_compat_r; last by apply min_Sum.
  apply Zmult_le_compat_r; last by apply Zbeta_0'.
  apply Zle_minus_1; by apply max_u2Z.
Qed.