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_mul_triple

Require Import ssreflect ssrbool eqtype.
Require Import Arith_ext ZArith_ext Lists_ext.
Require Import machine_int multi_int omegaz.
Import MachineInt.
Require Import mapstos mips_seplog mips_contrib mips_tactics.
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.


Formal separation-logic triple that specifies the Montgomery multiplication. In the post-condition, observe that the k+1 th word of storage is provided by the register C. The existence in memory of input-words and outputs-words is specified by a separation logic formula.
Lemma mont_mul_triple : forall k alpha x y z m one ext int_ X_ Y_ M_ Z_ quot C t s_ : reg,
  nodup(k, alpha, x, y, z, m, one, ext, int_, X_, Y_, M_, Z_, quot, C, t, s_, r0) ->
  forall nk valpha vx vy vm vz X Y M,
  u2Z (nth 0 M zero32) * u2Z valpha =m -1 {{ Zbeta 1 }} ->
  length X = nk -> length Y = nk -> length M = nk ->
  u2Z vz + 4 * Z_of_nat nk < Zbeta 1 ->
  Sum nk X < Sum nk M -> Sum nk Y < Sum nk M ->
{{ fun s h => [x]_s = vx /\ [y]_s = vy /\ [z]_s = vz /\ [m]_s = vm /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e y |--> Y ** var_e z |--> rep zero32 nk ** var_e m |--> M) s h /\
  store.multi_null s }}
montgomery k alpha x y z m one ext int_ X_ Y_ M_ Z_ quot C t s_
{{ fun s h => exists Z, length Z = nk /\
  [x]_s = vx /\ [y]_s = vy /\ [z]_s = vz /\ [m]_s = vm /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e y |--> Y ** 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 Y {{ 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 y z m one ext int_ X_ Y_ M_ Z_ quot C t s_
  Hset nk valpha vx vy vm vz X Y M Halpha Hx Hy Hm Hnz HX HY.
rewrite /montgomery.

addiu one r0 one16;

NextAddiu.
move=> s h [[r_x [r_y [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_y [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_y [r_z [r_m [r_k [rd_galpha [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 /\ [y]_s = vy /\ [z]_s = vz /\ [m]_s = vm /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e y |--> Y ** 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 Y + K * Sum nk M /\
    Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next)).

move=> s h [[[[r_x [r_y [r_z [r_m [r_k [r_alpha [Hmem Hmu]]]]]]] r_one] r_C] r_ext].

exists (rep zero32 nk), O; repeat (split; trivial).
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.
by case.
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 | assumption].

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

exists Z; do 8 (split; trivial).
case: Hinv => K [Hinv1 Hinv2].
split; first by exists K.
split.
- apply Zmult_gt_0_lt_reg_r with (Zbeta nk).
  by apply Zlt_gt, Zbeta_0.
  rewrite Zmult_comm Hinv1; exact Hinv2.
- 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 /\ [y]_s = vy /\ [z]_s = vz /\ [m]_s = vm /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e y |--> Y ** 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 Y + K * Sum nk M /\
    Sum next X * Sum nk Y + 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_y [r_z [r_m [r_k [r_alpha [Hmem [r_ext [Hextk' [Hone [Ht Hinv]]]]]]]]]]]]]] Hextk].
rewrite /= in Hextk; move/Zeq_boolP : Hextk => Hextk.
have {Hextk}Hextk : (next < nk)%nat.
  apply Z_of_nat_lt_inj. rewrite -r_ext -r_k. by apply Zle_neq_lt.

exists (nth next X zero32); split.
- Decompose_32 X next X1 X2 HlenX1 HX'; last by rewrite Hx.
  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; by apply inj_lt.

lw Y zero16 y;

apply hoare_lw_back_alt'' with (fun s h => exists Z, exists next, length Z = nk /\
  [x]_s = vx /\ [y]_s = vy /\ [z]_s = vz /\ [m]_s = vm /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e y |--> Y ** 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 Y + K * Sum nk M /\
    Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32 /\ [Y_]_s = nth O Y zero32).

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

destruct Y as [| hdy tly]; first by destruct nk.
exists hdy; split.
rewrite /= !assert_m.con_assoc_equiv assert_m.con_com_equiv assert_m.con_assoc_equiv in mem.
move: mem; apply monotony => ht //.
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 /\ [y]_s = vy /\ [z]_s = vz /\ [m]_s = vm /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e y |--> Y ** 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 Y + K * Sum nk M /\
    Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32 /\
  [Y_]_s = nth O Y zero32 /\ [Z_]_s = nth O Z zero32).

move=> s h [Z [next [HZ [r_x [r_y [r_z [r_m [r_k [r_alpha [mem [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 !assert_m.con_assoc_equiv assert_m.con_com_equiv !assert_m.con_assoc_equiv in mem.
move: mem; apply monotony => ht //.
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 /\ [y]_s = vy /\ [z]_s = vz /\ [m]_s = vm /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e y |--> Y ** 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 Y + K * Sum nk M /\
    Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32 /\ [Y_]_s = nth O Y 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 Y zero32)).

move=> s h [Z [next [HZ [r_x [r_y [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.

by rewrite store.utoZ_multu; 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 /\ [y]_s = vy /\ [z]_s = vz /\ [m]_s = vm /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e y |--> Y ** 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 Y + K * Sum nk M /\
    Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32 /\ [Y_]_s = nth O Y 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 Y zero32) /\ [M_]_s = nth O M zero32).

move=> s h [Z [next [HZ [r_x [r_y [r_z [r_m [r_k [r_alpha [mem [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 mem.
move: mem; 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 /\ [y]_s = vy /\ [z]_s = vz /\ [m]_s = vm /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e y |--> Y ** 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 Y + K * Sum nk M /\
    Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32 /\ [Y_]_s = nth O Y 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 Y zero32) + u2Z (nth O Z zero32) /\ [M_]_s = nth O M zero32).

move=> s h [Z [next [HZ [r_x [r_y [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).
  by apply Zle_lt_trans with ((Zbeta 1 - 1) * (Zbeta 1 - 1)).
repeat reg_upd.
do 8 (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.
  by apply Zle_minus_1; rewrite /Zbeta; 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 /\ [y]_s = vy /\ [z]_s = vz /\ [m]_s = vm /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e y |--> Y ** 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 Y + K * Sum nk M /\
    Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32 /\ [Y_]_s = nth O Y 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 Y zero32) + u2Z (nth O Z zero32) /\ [M_]_s = nth O M zero32 /\
  [t]_s = ((nth next X zero32 [.*] nth O Y zero32) [.+] zext 32 (nth O Z zero32)) [.%] 32).

move=> s h [Z [next [HZ [r_x [r_y [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; first by rewrite -plus_assoc; apply le_plus_r.
rewrite Hm2 u2Z_add // u2Z_umul 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.
rewrite -u2Z_umul; by apply max_u2Z_umul.
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 /\ [y]_s = vy /\ [z]_s = vz /\ [m]_s = vm /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e y |--> Y ** 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 Y + K * Sum nk M /\
    Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32 /\ [Y_]_s = nth O Y 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 Y zero32) + u2Z (nth O Z zero32) /\
  [M_]_s = nth O M zero32 /\
  [t]_s = ((nth next X zero32 [.*] nth O Y zero32) [.+] zext 32 (nth O Z zero32)) [.%] 32 /\
  u2Z ([s_]_s [.||] [t]_s) = u2Z (nth next X zero32) * u2Z (nth O Y zero32) + u2Z (nth O Z zero32)).

move=> s h [Z [next [HZ [r_x [r_y [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; by apply max_u2Z.
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; by [apply Zle_refl | apply Zpower_0].
rewrite -H u2Z_concat -Zbeta1_Zpower2 -Hm2; ring.

multu t alpha;

apply hoare_multu with (fun s h => exists Z, exists next, length Z = nk /\
  [x]_s = vx /\ [y]_s = vy /\ [z]_s = vz /\ [m]_s = vm /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e y |--> Y ** 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 Y + K * Sum nk M /\
    Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32 /\ [Y_]_s = nth O Y 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 Y zero32) [.+] zext 32 (nth O Z zero32)) [.%] 32 /\
  u2Z ([s_]_s [.||] [t]_s) = u2Z (nth next X zero32) * u2Z (nth O Y zero32) + u2Z (nth O Z zero32) /\
  store.utoZ s = u2Z [t]_s * u2Z [alpha]_s).

move=> s h [Z [next [HZ [r_x [r_y [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 7 (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 /\ [y]_s = vy /\ [z]_s = vz /\ [m]_s = vm /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e y |--> Y ** 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 Y + K * Sum nk M /\
    Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32 /\ [Y_]_s = nth O Y 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 Y zero32) [.+] zext 32 (nth O Z zero32)) [.%] 32 /\
  u2Z ([s_]_s [.||] [t]_s) = u2Z (nth next X zero32) * u2Z (nth O Y 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_y [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 /\ [y]_s = vy /\ [z]_s = vz /\ [m]_s = vm /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e y |--> Y ** 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 Y + K * Sum nk M /\
    Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32 /\
  [Y_]_s = nth O Y 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 Y zero32) [.+] zext 32 (nth O Z zero32)) [.%] 32 /\
  u2Z ([s_]_s [.||] [t]_s) = u2Z (nth next X zero32) * u2Z (nth O Y 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 Y zero32) [.+] (zext 32 (nth O Z zero32)) [.%] 32)
    [.*] [alpha]_s) [.%] 32).

move=> s h [Z [next [HZ [r_x [r_y [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 r_int_]]]]]]]]]]]]]]]]]]]]]]].
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 /\ [y]_s = vy /\ [z]_s = vz /\ [m]_s = vm /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e y |--> Y ** 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 Y + K * Sum nk M /\
    Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32 /\ [Y_]_s = nth O Y 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 Y zero32) [.+] zext 32 (nth O Z zero32)) [.%] 32 /\
  u2Z ([s_]_s [.||] [t]_s) = u2Z (nth next X zero32) * u2Z (nth O Y zero32) + u2Z (nth O Z zero32) /\
  [int_]_s = one32 /\
  [quot]_s = ((((nth next X zero32 [.*] nth O Y 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_y [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 [r_int_ 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 /\ [y]_s = vy /\ [z]_s = vz /\ [m]_s = vm /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e y |--> Y ** 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 Y + K * Sum nk M /\
    Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32 /\ [Y_]_s = nth O Y 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 Y zero32) [.+] zext 32 (nth O Z zero32)) [.%] 32 /\
  u2Z ([s_]_s [.||] [t]_s) = u2Z (nth next X zero32) * u2Z (nth O Y zero32) + u2Z (nth O Z zero32) /\
  [int_]_s = one32 /\
  [quot]_s = ((((nth next X zero32 [.*] nth O Y 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_y [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 [r_int_ [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 /\ [y]_s = vy /\ [z]_s = vz /\ [m]_s = vm /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e y |--> Y ** 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 Y + K * Sum nk M /\
    Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32 /\
  [Y_]_s = nth O Y zero32 /\ [Z_]_s = nth O Z zero32 /\
  [M_]_s = nth O M zero32 /\ [int_]_s = one32 /\
  [quot]_s = ((((nth next X zero32 [.*] nth O Y 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 Y zero32) + u2Z (nth O Z zero32) /\
  store.lo s = zero32).

move=> s h [Z [next [HZ [r_x [r_y [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 [r_int_ [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.
    by split; [apply Zle_refl | apply Zpower_0].
apply Zlt_le_trans with (Zbeta 2 * 1); first by done.
apply Zmult_le_compat_l.
  apply Zle_trans with (2 ^^ 8 - 1); first by done.
  apply Zminus_le_compat; by [apply Zpower_2_le, store.acx_size_min | apply Zbeta_0'].
by apply Zbeta_0'.

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.
  by 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.
- split; by [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 /\ [y]_s = vy /\ [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 y |--> Y ** 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 Y + K * Sum nk M /\
    Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32 /\
  [Y_]_s = nth O Y zero32 /\ [M_]_s = nth O M zero32 /\ [int_]_s = one32 /\
  [quot]_s = ((((nth next X zero32 [.*] nth O Y 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 Y zero32) + u2Z (nth O Z zero32) /\
  store.utoZ s < 2 * Zbeta 1 - 2).

move=> s h [Z [next [HZ [r_x [r_y [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.
reg_upd.
rewrite 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 /\ [y]_s = vy /\ [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 y |--> Y ** 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 Y + K * Sum nk M /\
    Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  (next < nk)%nat /\ [X_]_s = nth next X zero32 /\
  [Y_]_s = nth O Y zero32 /\ [M_]_s = nth O M zero32 /\ [int_]_s = one32 /\
  [quot]_s = ((((nth next X zero32 [.*] nth O Y 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 Y 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_y [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 /\ [y]_s = vy /\ [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 y |--> Y ** 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 Y + Sum nint_ Y * u2Z (nth next X zero32) * Zbeta next +
    Sum nint_ M * u2Z [quot]_s * Zbeta next + K * Sum nk M /\
    Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next)).

move=> s h [Z [next [HZ [r_x [r_y [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_ /one32 u2Z_Z2u.
rewrite r_int_ r_k /one32 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 Y zero32))).
- rewrite Hm2 [mult _ _]/= /zero32; ring.
- rewrite Sum_head_swap0 tail_app; last first.
    rewrite HZ; destruct nk => //; by 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 /\ [y]_s = vy /\ [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 y |--> Y ** 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 Y + Sum nint_ Y * u2Z (nth next X zero32) * Zbeta next +
    Sum nint_ M * u2Z [quot]_s * Zbeta next + K * Sum nk M /\
    Sum next X * Sum nk Y + 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 /\ [y]_s = vy /\ [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 y |--> Y ** 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 Y + Sum nint_ Y * u2Z (nth next X zero32) * Zbeta next +
    Sum nint_ M * u2Z [quot]_s * Zbeta next + K * Sum nk M /\
    Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  [Y_]_s = nth nint_ Y zero32).

move=> s h [ [Z [next [nint_ [HZ [r_x [r_y [r_z [r_m [Hone [r_k [r_alpha [mem [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.
have {Hint_k}Hint_k : (nint_ < nk)%nat.
  apply le_neq_lt.
  apply Z_of_nat_le_inj; by rewrite -r_int_ -r_k.
  rewrite r_int_ r_k in Hint_k; by apply Z_of_nat_inj_neq.

exists (nth nint_ Y zero32); split.
- Decompose_32 Y nint_ Y1 Y2 HlenY1 HY'; last by rewrite Hy.
  rewrite HY' (decompose_equiv _ _ _ _ _ HlenY1) !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 mem.
  move: mem; 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.

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 /\ [y]_s = vy /\ [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 y |--> Y ** 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 Y + Sum nint_ Y * u2Z (nth next X zero32) * Zbeta next +
    Sum nint_ M * u2Z [quot]_s * Zbeta next + K * Sum nk M /\
    Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next) /\
  [Y_]_s = nth nint_ Y zero32 /\ [Z_]_s = nth nint_ Z zero32).

move=> s h [Z [next [nint_ [HZ [r_x [r_y [r_z [r_m [Hone [r_k [r_alpha [mem [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 assert_m.con_com_equiv !assert_m.con_assoc_equiv in mem.
  move: mem; 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 /\ [y]_s = vy /\ [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 y |--> Y ** 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_ Y 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 Y +
    Sum nint_ Y * u2Z (nth next X zero32) * Zbeta next +
    Sum nint_ M * u2Z [quot]_s * Zbeta next +
    u2Z (nth next X zero32) * u2Z (nth nint_ Y zero32) * Zbeta (next + nint_) + K * Sum nk M /\
    Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next)).

move=> s h [Z [next [nint_ [HZ [r_x [r_y [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).
  apply Zlt_le_trans with (2 * Zbeta 1 - 1); first by done.
  apply Zle_trans with (Zbeta 2 * (2 ^^ 8 - 1)); first by done.
  apply Zmult_le_compat_l.
  apply Zminus_le_compat; by [apply Zpower_2_le, store.acx_size_min | apply Zbeta_0'].
  by apply Zbeta_0'.
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; last by done.
by apply max_u2Z_umul.
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 Y +
 Sum nint_ Y * 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_ Y zero32) * Zbeta (next + nint_)).
- rewrite store.utoZ_maddu // store.utoZ_def store.utoZ_acx_beta2 //.
  rewrite u2Z_Z2u //.
  rewrite -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_ Y zero32))) Zmult_plus_distr_l Zmult_plus_distr_l.
  f_equal.
  by rewrite Zmult_plus_distr_l Zplus_comm.
  by apply Zlt_le_trans with (2 * Zbeta 1 - 1).
- 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 /\ [y]_s = vy /\ [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 y |--> Y ** 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_ Y 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 Y +
    Sum nint_ Y * u2Z (nth next X zero32) * Zbeta next +
    Sum nint_ M * u2Z [quot]_s * Zbeta next +
    u2Z (nth next X zero32) * u2Z (nth nint_ Y zero32) * Zbeta (next + nint_) + K * Sum nk M /\
    Sum next X * Sum nk Y + 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_y [r_z [r_m [Hone [r_k [r_alpha [mem [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 mem.
  move: mem; 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 /\ [y]_s = vy /\ [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 y |--> Y ** 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_ Y 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 Y +
    Sum nint_ Y * u2Z (nth next X zero32) * Zbeta next +
    Sum nint_ M * u2Z [quot]_s * Zbeta next +
    u2Z (nth next X zero32) * u2Z (nth nint_ Y zero32) * Zbeta (next + nint_) +
    u2Z (nth nint_ Z zero32) * Zbeta (next + nint_) + K * Sum nk M /\
    Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next)).

move=> s h [Z [next [nint_ [HZ [r_x [r_y [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).
  apply Zlt_le_trans with (Zbeta 2 * 1); first by done.
  rewrite Zmult_1_r.
  apply Zle_trans with (Zbeta 2 * (2 ^^ 8 - 1)); first by done.
  apply Zmult_le_compat_l; [by apply Zminus_le_compat, Zpower_2_le, store.acx_size_min | done].
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 //; by apply Zle_minus_1, 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 /\ [y]_s = vy /\ [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 y |--> Y ** 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_ Y 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 Y +
    Sum nint_ Y * u2Z (nth next X zero32) * Zbeta next +
    Sum nint_ M * u2Z [quot]_s * Zbeta next +
    u2Z (nth next X zero32) * u2Z (nth nint_ Y 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 Y + K * Sum nk M < 2 * Sum nk M * Zbeta next)).

move=> s h [Z [next [nint_ [HZ [r_x [r_y [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).
  apply Zlt_le_trans with (Zbeta 2 + Zbeta 1 - 1); first by done.
  apply Zle_trans with (Zbeta 2 * (2 ^^ 8 - 1)); first by done.
  by apply Zmult_le_compat_l.

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 /\ [y]_s = vy /\ [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 y |--> Y ** 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 Y +
    Sum (nint_ - 1) Y * 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) Y 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 Y + K * Sum nk M < 2 * Sum nk M * Zbeta next)).

move=> s h [Z [next [nint_ [HZ [r_x [r_y [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.
- eapply Zle_lt_trans; last by apply Hnz.
  apply Zle_trans with (Z_of_nat nk).
  + rewrite r_int_' (_ : 1 = Z_of_nat 1) // -inj_plus plus_comm; by apply inj_le.
  + apply Zle_plus_trans; first by apply min_u2Z.
    rewrite Zmult_comm. apply Zle_scale; by [apply Zle_0_nat | done].

apply le_n_S; exact Hint_.

rewrite Z_S [Zmult]lock /= -lock r_t; ring.

case: Hinv => K [Hinv1 Hinv2].
exists K; split; last by done. rewrite minus_Sn_1 plus_minus_assoc; last by apply le_n_S, le_O_n.
rewrite minus_Sn_1 Hinv1; ring.

mflhxu Z;

apply hoare_mflhxu with (fun s h => exists Z, exists next, exists nint_, length Z = nk /\
  [x]_s = vx /\ [y]_s = vy /\ [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 y |--> Y ** 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 Y +
    Sum (nint_-1) Y * 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) Y 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 Y + K * Sum nk M < 2 * Sum nk M * Zbeta next)).

move=> s h [Z [next [nint_ [HZ [r_x [r_y [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 reg_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.
  apply le_trans with 2%nat; [by apply le_n_S, le_O_n | exact Hint_].
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 /\ [y]_s = vy /\ [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 y |--> Y ** 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 Y +
    Sum (nint_-1) Y * 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) Y 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 Y + K * Sum nk M < 2 * Sum nk M * Zbeta next)).

move=> s h [Z [next [nint_ [HZ [r_x [r_y [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 r_t -Zbeta1_Zpower2.
  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; apply Zmult_le_compat_l; last by done.
  rewrite -Zplus_assoc; apply Zle_plus_trans_L => //; by apply inj_le.

sw Z mfour16 t

apply hoare_sw_back'.

move=> s h [Z [next [nint_ [HZ [r_x [r_y [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 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.
by apply le_trans with 2%nat; auto.
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.
    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_.
    destruct nint_ as [|nint_]; first by done.
    rewrite /=. apply not_eq_S. 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.

apply trans_eq with ((Sum (nint_ - 1) Y * u2Z (nth next X zero32) * Zbeta next +
 u2Z (nth next X zero32) * u2Z (nth (nint_ - 1) Y 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 Y
 + u2Z (nth (nint_ - 1) Z zero32) * Zbeta (next + nint_ - 1)).
ring.

apply trans_eq with (Sum nint_ Y * u2Z (nth next X zero32) * Zbeta next +
 Sum nint_ M * u2Z [quot]_s * Zbeta next
 + K * Sum nk M + Sum next X * Sum nk Y
 + (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) Y + u2Z (nth (nint_ - 1) Y 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 /\ [y]_s = vy /\ [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 y |--> Y ** 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 Y + Sum nk Y * u2Z (nth next X zero32) * Zbeta next +
    Sum nk M * u2Z [quot]_s * Zbeta next + K * Sum nk M /\
    Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next)).

move=> s h [[Z [next [nint_ [HZ [r_x [r_y [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).
  apply Zlt_le_trans with (2 * Zbeta 1 - 1); first by done.
  by apply Zle_trans with (Zbeta 2 * (2 ^^ 8 - 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.
by apply Zle_minus_1, max_u2Z.

case: Hinv => K [Hinv1 Hinv2].
exists K; split; last by done. rewrite -Hinv1 store.utoZ_maddu // Hone umul_1 (@u2Z_zext 32) Zmult_plus_distr_l Zplus_assoc /Sum_hole //.
rewrite minus_Sn_1 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 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; by rewrite -HZ plus_comm /= -minus_n_O.
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 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 /\ [y]_s = vy /\ [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 y |--> Y ** 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 Y +
    Sum nk Y * u2Z (nth next X zero32) * Zbeta next +
    Sum nk M * u2Z [quot]_s * Zbeta next + K * Sum nk M /\
    Sum next X * Sum nk Y + K * Sum nk M < 2 * Sum nk M * Zbeta next)).

move=> s h [Z [next [HZ [r_x [r_y [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 reg_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).
reg_upd; ring.

addiu ext ext one16;

apply hoare_addiu with (fun s h => exists Z, exists next, length Z = nk /\
  [x]_s = vx /\ [y]_s = vy /\ [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 y |--> Y ** 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 Y +
    Sum nk Y * 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 Y + 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_y [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.
- rewrite minus_Sn_1 -Hinv1 plus_Snm_nSm plus_minus_assoc; last by apply le_n_S, le_O_n.
  by rewrite minus_Sn_1 -plus_assoc -(plus_comm 1).
-
  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 Y +
    (Zbeta 1 - 1) * Zbeta (S next - 1) * Sum nk M).
  apply Zplus_lt_le_compat; last by rewrite -Zmult_assoc; apply Zle_refl.
  rewrite -Zbeta_power (Zmult_comm (Zbeta next)) /zero32 Zplus_comm Zplus_assoc;
    by apply Zplus_lt_le_compat; [rewrite Zplus_comm | apply Zle_refl].
  apply Zle_trans with (2 * Sum nk M * Zbeta next + (Zbeta 1 - 1) * Zbeta next * Sum nk Y +
    (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; by apply max_u2Z.
  apply Zmult_le_0_compat; by [apply Zbeta_0' | apply min_Sum].
  rewrite -Zplus_assoc [minus _ _]/= -minus_n_O.
  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 /\ [y]_s = vy /\ [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 y |--> Y ** 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 Y + Sum nk Y * 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 Y + 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_y [r_z [r_m [Hone [rk [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; by case: Hextk'.
have Hlenlst1 : length lst1 = (nk - 1)%nat by rewrite -HZ H0 app_length /= plus_minus_assoc.
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; case: Hextk'.
  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 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), next.

repeat (split; trivial).
by apply len_update_list.
rewrite H0 update_list_app Hlenlst1 // -minus_n_n /= (_ : lst1 ++ [Z_]_s :: nil = lst1 ++ ([Z_]_s :: nil) ++ nil) // (decompose_equiv _ _ _ _ _ Hlenlst1).
simpl assert_m.mapstos.
assoc_comm H'.
by move: H'; 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 => //; by 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_y [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 //.
apply le_trans with next; by case: Hextk'.

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 Y + 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.