Library mont_exp_triple

Require Import ssreflect ssrbool eqtype.
Require Import ZArith_ext Lists_ext.
Require Import machine_int multi_int.
Import MachineInt.
Require Import mips_seplog mips_frame mips_contrib mips_tactics mapstos.
Require Import mont_mul_strict_prg mont_exp_prg.
Require Import mont_mul_strict_init_triple mont_square_strict_init_triple.

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_exp_specif : forall k alpha x a' x' i l a ei e one' m one ext int_ X_ Y_ M_ Z_ quot C t s_ : reg,
  nodup(k, alpha, x, a, a', m, one, ext, int_, X_, Y_, M_, Z_, quot, C, x', t, s_, i, e, ei, l, one', r0) ->
  forall nk valpha M, u2Z (nth 0 M zero32) * u2Z valpha =m -1 {{ Zbeta 1 }} ->
  forall ve vl, u2Z ve < 2 ^^ vl -> (vl < 32)%nat ->
  forall va (A : list (int 32)) va' (A' : list (int 32)) vx X vx' vone' ONE' vm,
  length A = nk -> length A' = nk -> length X = nk -> length ONE' = nk -> length M = nk ->
  u2Z va + 4 * Z_of_nat (S nk) < Zbeta 1 ->
  u2Z va' + 4 * Z_of_nat (S nk) < Zbeta 1 ->
  u2Z vx' + 4 * Z_of_nat (S nk) < Zbeta 1 ->
  Sum nk A =m Zbeta nk {{ Sum nk M }} -> Sum nk A' =m Zbeta (2 * nk) {{ Sum nk M }} ->
  Sum nk X < Sum nk M -> Sum nk A < Sum nk M -> Sum nk A' < Sum nk M -> Sum nk ONE' < Sum nk M ->
  Sum nk ONE' = 1 -> Zodd (Sum nk M) ->
  {{ fun s h => exists X', length X' = nk /\ [x]_s = vx /\ [a']_s = va' /\
    [x']_s = vx' /\ [m]_s = vm /\ u2Z ([k]_s) = Z_of_nat nk /\ [alpha]_s = valpha /\
    [e]_s = ve /\ [l]_s = Z2s 32 (Z_of_nat vl) /\ [a]_s = va /\ [one']_s = vone' /\
    (var_e x |--> X ** var_e a |--> A ++ zero32 :: nil ** var_e a' |--> A' ++ zero32 :: nil **
      var_e x' |--> X' ++ zero32 :: nil ** var_e one' |--> ONE' ** var_e m |--> M ++ zero32 :: nil) s h}}
  mont_exp k alpha x a' x' i l a ei e one' m one ext int_ X_ Y_ M_ Z_ quot C t s_
  {{ fun s h => exists A, exists A', exists X', exists new_va, exists new_va',
    length A = nk /\ length A' = nk /\ length X' = nk /\ u2Z [k]_s = Z_of_nat nk /\
    [alpha]_s = valpha /\ [e]_s = ve /\ [l]_s = Z2s 32 (Z_of_nat vl) /\
    [a]_s = new_va /\ u2Z new_va + 4 * Z_of_nat (S nk) < Zbeta 1 /\
    [a']_s = new_va' /\ u2Z new_va' + 4 * Z_of_nat (S nk) < Zbeta 1 /\
    [x]_s = vx /\ [x']_s = vx' /\ [one']_s = vone' /\ [m]_s = vm /\
    (var_e a |--> A ++ zero32 :: nil ** var_e a' |--> A' ++ zero32 :: nil ** var_e x |--> X **
      var_e x' |--> X' ++ zero32 :: nil ** var_e one' |--> ONE' ** var_e m |--> M ++ zero32 :: nil) s h /\
    Sum nk A' =m (Sum nk X) ^^ Zabs_nat (u2Z [e]_s) {{ Sum nk M }} }}.
Proof.
move=> k alpha x a' x' i l a ei e one' m one ext int_ X_ Y_ M_ Z_ quot C t s_
  Hset nk valpha M Halpha ve vl Hvevl Hvl va A va' A' vx X
  vx' vone' ONE' vm HlenA HlenA' HlenX HlenONE' HlenM
  Hna Hna' Hxn' HA HA' HSumXSumM HSumA HSumA'SumM HSumONE' HSumONE'_is_1 HZoddM.
rewrite /mont_exp.

apply hoare_prop_m.hoare_stren with ((fun s h => exists X', length X' = nk /\
  [x]_s = vx /\ [a']_s = va' /\ [x']_s = vx' /\ [m]_s = vm /\
  u2Z ([k]_s) = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e a' |--> A' ** var_e x' |--> X' ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil) s h) **
(fun s h => [e]_s = ve /\ [l]_s = Z2s 32 (Z_of_nat vl) /\ [a]_s = va /\ [one']_s = vone' /\
  (var_e a |--> A ++ zero32 :: nil **
  add_e (var_e a') (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32 ** var_e one' |--> ONE') s h)).

move=> s h [X' [HlenX' [r_x [r_a' [r_x' [r_m [r_k [r_alpha [r_e [r_l [r_a [r_one' Hmem]]]]]]]]]]]].

have {Hmem}Hmem :
  ((var_e x |--> X ** var_e a' |--> A' ** var_e x' |--> X' ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil) **
   (var_e a |--> A ++ zero32 :: nil ** add_e (var_e a') (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32 ** var_e one' |--> ONE')) s h.
  rewrite (decompose_last_equiv _ A') HlenA' in Hmem.
  by assoc_comm Hmem.
case: Hmem => h1 [h2 [Hdisj [Hunion [Hmem1 Hmem2]]]].
exists h1, h2; repeat (split; trivial).
by exists X'.

apply while.hoare_seq with ((fun s h => exists X', length X' = nk /\ [x]_s = vx /\
  [a']_s = va' /\ [x']_s = vx' /\ [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\
  [alpha]_s = valpha /\
  (var_e x |--> X ** var_e a' |--> A' ** var_e x' |--> X' ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil) s h /\
  Sum nk X' =m Sum nk X * Zbeta nk {{ Sum nk M }} /\ Sum nk X' < Sum nk M) **
(fun s h => [e]_s = ve /\ [l]_s = Z2s 32 (Z_of_nat vl) /\ [a]_s = va /\
  [one']_s = vone' /\
  (var_e a |--> A ++ zero32 :: nil ** (add_e (var_e a') (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32) ** var_e one' |--> ONE') s h)).


apply frame_rule.
- apply hoare_prop_m.hoare_weak with (fun s h => exists X', length X' = nk /\
    [x]_s = vx /\ [a']_s = va' /\ [x']_s = vx' /\ [m]_s = vm /\
    u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
    (var_e x |--> X ** var_e a' |--> A' ** var_e x' |--> X' ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil) s h /\
    Zbeta nk * Sum nk X' =m Sum nk X * Sum nk A' {{ Sum nk M }} /\ Sum nk X' < Sum nk M).
  move=> s h [X' [HlenX' [r_x [r_a' [r_x' [r_m [r_k [r_alpha [Hmem [Sum_X'1 Sum_X'2]]]]]]]]]].
  exists X'; repeat (split; trivial).
  apply: (eqmod_reg_mult' _ _ (Zbeta nk)).
  apply Zis_gcd_sym; rewrite Zbeta_power; by apply Zis_gcd_Zpower_odd.
  rewrite Zmult_comm.
  eapply eqmod_trans; first by apply Sum_X'1.
  rewrite -Zmult_assoc.
  apply eqmod_reg_mult_l.
  rewrite -Zbeta_is_exp.
  suff : (nk + nk = 2 * nk)%nat by move=> ->.
  ring.
  eapply mont_mul_strict_init_triple; eauto.
  by Nodup_nodup r0.
- by Inde_frame.
- move=> ?; by Inde_mult.

apply pull_out_exists_con => X'.

apply hoare_prop_m.hoare_stren with ((fun s h => (length X' = nk /\
  Sum nk X' =m Sum nk X * Zbeta nk {{Sum nk M}} /\ Sum nk X' < Sum nk M) /\ h = heap.emp) **
(fun s h => [x]_s = vx /\ [a]_s = va /\ [a']_s = va' /\ [x']_s = vx' /\
  [m]_s = vm /\ [one']_s = vone' /\ [l]_s = Z2s 32 (Z_of_nat vl) /\
  [e]_s = ve /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e a |--> A ++ zero32 :: nil ** var_e a' |--> A' ++ zero32::nil ** var_e x' |--> X' ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil ** var_e one' |--> ONE') s h)).

move=> s h [h1 [h2 [Hdisj [Hunion [[HlenX' [r_x [r_a' [r_x' [r_m [r_k [r_alpha [Hmem1 [Sum_X'1 Sum_X'2]]]]]]]]] [r_e [r_l [r_a [r_one' Hmem2]]]]]]]]].
exists heap.emp, (h1 +++ h2); repeat (split; trivial).
by map_tac_m.Disj.
by map_tac_m.Equal.
move: {Hmem1 Hmem2}(assert_m.con_cons _ _ _ _ _ Hdisj Hmem1 Hmem2) => Hmem.
rewrite (decompose_last_equiv _ A') HlenA'.
by abstract assoc_comm Hmem.

apply pull_out_and; case=> HlenX' [HSumX'1 HSumX'2].

apply hoare_prop_m.hoare_stren with ((fun s h => u2Z [k]_s = Z_of_nat nk /\
  [alpha]_s = valpha /\ [e]_s = ve /\ [l]_s = Z2s 32 (Z_of_nat vl) /\
  [a]_s = va /\ [a']_s = va' /\ [x']_s = vx' /\ [m]_s = vm /\
  (var_e a|-->A ++ zero32 :: nil ** var_e a'|-->A' ++ zero32 :: nil ** var_e x'|-->X' ** var_e m |-->M ++ zero32 :: nil) s h) **
(fun s h => [x]_s = vx /\ [one']_s = vone' /\
  (var_e x|-->X ** add_e (var_e x') (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32 ** var_e one' |--> ONE') s h)).

move=> s h [r_x [r_a [r_a' [r_x' [r_m [r_one' [r_l [r_e [r_k [r_alpha Hmem]]]]]]]]]].

have {Hmem}Hmem : ((var_e a |--> A ++ zero32 :: nil ** var_e a' |--> A' ++ zero32 :: nil ** var_e x' |--> X' ** var_e m |--> M ++ zero32 :: nil) ** (var_e x|--> X ** add_e (var_e x') (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32 ** var_e one' |--> ONE')) s h.
  rewrite (decompose_last_equiv _ X') HlenX' in Hmem.
  by abstract assoc_comm Hmem.
case: Hmem => h1 [h2 [Hdisj [Hunion [Hmem1 Hmem2]]]].
by exists h1, h2.

apply while.hoare_seq with ((fun s h => exists A, exists A', exists new_va, exists new_va',
  length A = nk /\ length A' = nk /\ u2Z [k]_s = Z_of_nat nk /\
  [alpha]_s = valpha /\ [e]_s = ve /\ [l]_s = Z2s 32 (Z_of_nat vl) /\
  [a]_s = new_va /\ u2Z new_va + 4 * Z_of_nat (S nk) < Zbeta 1 /\
  [a']_s = new_va' /\ u2Z new_va' + 4 * Z_of_nat (S nk) < Zbeta 1 /\
  [x']_s = vx' /\ [m]_s = vm /\
  (var_e a|-->A ++ zero32 :: nil ** var_e a'|-->A' ++ zero32::nil ** var_e x'|-->X' ** var_e m|-->M ++ zero32 :: nil) s h /\
    Sum nk A =m Sum nk X ^^ (Zabs_nat (u2Z ve)) * Zbeta nk {{ Sum nk M }} /\ Sum nk A < Sum nk M) **
(fun s h => [x]_s = vx /\ [one']_s = vone' /\
  (var_e x|-->X ** add_e (var_e x') (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32 ** var_e one' |--> ONE') s h)).

apply frame_rule.

apply hoare_addiu with (fun s h => u2Z [k]_s = Z_of_nat nk /\
  [alpha]_s = valpha /\ [e]_s = ve /\ [l]_s = Z2s 32 (Z_of_nat vl) /\
  [i]_s = Z2s 32 (Z_of_nat vl) /\ [a]_s = va /\ [a']_s = va' /\ [x']_s = vx' /\
  [m]_s = vm /\
  (var_e a|-->A ++ zero32 :: nil ** var_e a'|-->A' ++ zero32 :: nil ** var_e x'|-->X' ** var_e m |-->M ++ zero32 :: nil) s h).

move=> s h [r_k [r_alpha [r_e [r_l [r_a [r_a' [r_x' [r_m Hmem]]]]]]]].
rewrite /wp_addiu.
repeat reg_upd.
repeat (split; trivial).
by rewrite sext_0 add_0.
by Assert_upd.

apply hoare_prop_m.hoare_while_invariant with (fun s h =>
  (exists A0, exists A'0, exists new_va, exists new_va', exists ni,
  length A0 = nk /\ length A'0 = nk /\ u2Z [k]_s = Z_of_nat nk /\
  [alpha]_s = valpha /\ [e]_s = ve /\ [l]_s = Z2s 32 (Z_of_nat vl) /\
  [a]_s = new_va /\ u2Z new_va + 4 * Z_of_nat (S nk) < Zbeta 1 /\
  [a']_s = new_va' /\ u2Z new_va' + 4 * Z_of_nat (S nk) < Zbeta 1 /\
  [x']_s = vx' /\ [m]_s = vm /\ s2Z [i]_s = ni /\ -1 <= ni <= Z_of_nat vl /\
  (var_e a |--> A0 ++ zero32::nil ** var_e a' |--> A'0 ++ zero32::nil ** var_e x' |--> X' ** var_e m |--> M ++ zero32::nil) s h /\
  Sum nk A0 =m Sum nk X ^^ Zabs_nat (u2Z (ve[.>>]Zabs_nat (ni+1))) * Zbeta nk {{ Sum nk M }} /\ Sum nk A0 < Sum nk M)).

move=> s h [r_k [r_alpha [r_e [r_l [r_i [r_a [r_a' [r_x' [r_m Hmem]]]]]]]]].
exists A, A', va, va', (Z_of_nat vl); repeat (split; trivial).
rewrite r_i s2Z_Z2s //.
split.
  apply Zle_trans with 0; [done | by apply Zle_0_nat].
apply Zle_lt_trans with 32; last by done.
rewrite (_ : 32 = Z_of_nat 32) //; by apply inj_le, lt_le_weak.
apply Zle_trans with 0; [done | by apply Zle_0_nat].
by apply Zle_refl.

have -> : ve [.>>] Zabs_nat (Z_of_nat vl + 1) = zero32.
  rewrite shrl_overflow // Zabs_nat_plus_pos //; last by apply Zle_0_nat.
  rewrite plus_comm [plus _ _]/= Zabs_nat_Z_of_nat.
  apply Zlt_trans with (2 ^^ vl); [done | by apply Zpower_2_lt].
by rewrite u2Z_Z2u // [Zmult]lock /= -lock Zmult_1_l.

clear Hna'.
move=> s h [[A0 [A0' [new_va [new_va' [ni [HlenA0 [HlenA0' [r_k [r_alpha [r_e [r_l [r_a [Hnew_na [r_a' [Hna' [r_x' [r_m [r_i [Hi [Hmem [HSumA01 HSumA02]]]]]]]]]]]]]]]]]]]]] r_i'];
  rewrite /= in r_i'. move/Zle_boolP : r_i' => r_i'.

have {r_i'}r_i' : s2Z [i]_s < 0.
 apply Znot_ge_lt; contradict r_i'; by apply Zge_le.
exists A0, A0', new_va, new_va'; repeat (split; trivial).
have Hni : ni = -1.
  rewrite r_i in r_i'; case: Hi => Hi _; omega.
by rewrite Hni //= shrl_0 in HSumA01.

clear HlenA HA A HSumA HlenA' A' HA' HSumA'SumM va Hna va' Hna'.

apply hoare_prop_m.hoare_stren with (fun s h =>
  (exists A0, exists ni, exists new_va, exists new_va', exists A'0,
    length A0 = nk /\ length A'0 = nk /\ u2Z [k]_s = Z_of_nat nk /\
    [alpha]_s = valpha /\ [e]_s = ve /\ [l]_s = Z2s 32 (Z_of_nat vl) /\
    [a]_s = new_va /\ u2Z new_va + 4 * Z_of_nat (S nk) < Zbeta 1 /\
    [a']_s = new_va' /\ u2Z new_va' + 4 * Z_of_nat (S nk) < Zbeta 1 /\
    [x']_s = vx' /\ [m]_s = vm /\ s2Z [i]_s = ni /\ 0 <= ni <= Z_of_nat vl /\
    (var_e a |--> A0 ++ zero32 :: nil ** var_e a' |--> A'0 ++ zero32 :: nil ** var_e x' |--> X' ** var_e m |--> M ++ zero32 :: nil) s h /\
    Sum nk A0 =m Sum nk X ^^ Zabs_nat (u2Z (ve[.>>]Zabs_nat (ni + 1))) * Zbeta nk {{Sum nk M}} /\ Sum nk A0 < Sum nk M)).

move=> s h [ [A [A' [va [va' [ni [HlenA [HlenA' [r_k [r_alpha [r_e [r_l [r_a [Hna [r_a' [Hna' [r_x' [r_m [Hni [Hni' [Hmem [HSumA1 HSumA2]]]]]]]]]]]]]]]]]]]]] Hi];
  rewrite /= in Hi. move/Zle_is_le_bool : Hi => Hi.
exists A, ni, va, va', A'; repeat (split; trivial).
by rewrite -Hni.
by case: Hni'.

apply pull_out_exists => A.
apply pull_out_exists => ni.
apply pull_out_exists => va.
apply pull_out_exists => va'.

apply hoare_prop_m.hoare_stren with ((fun s h => (length A = nk /\
  Sum nk A =m Sum nk X ^^ Zabs_nat (u2Z (ve [.>>] Zabs_nat (ni + 1))) * Zbeta nk {{ Sum nk M }} /\
  Sum nk A < Sum nk M /\ 0 <= ni <= Z_of_nat vl /\
  u2Z va + 4 * Z_of_nat (S nk) < Zbeta 1 /\
  u2Z va' + 4 * Z_of_nat (S nk) < Zbeta 1) /\ h = heap.emp) **
(fun s h => (exists A'0, length A'0 = nk /\ u2Z [k]_s = Z_of_nat nk /\
  [alpha]_s = valpha /\ [e]_s = ve /\ [l]_s = Z2s 32 (Z_of_nat vl) /\
  [a]_s = va /\ [a']_s = va' /\ [x']_s = vx' /\ [m]_s = vm /\ s2Z [i]_s = ni /\
  (var_e a |--> A ++ zero32 :: nil ** var_e a' |--> A'0 ++ zero32 :: nil ** var_e x' |--> X' ** var_e m |--> M ++ zero32 :: nil) s h))).

move=> s h [A' [HlenA [HlenA' [r_k [r_alpha [r_e [r_l [r_a [Hna [r_a' [Hna' [r_x' [r_m [r_i [Hni [Hmem [HSumA1 HsumA2]]]]]]]]]]]]]]]]].
exists heap.emp, h; repeat (split; trivial).
by map_tac_m.Disj.
by map_tac_m.Equal.
by exists A'.

apply pull_out_and; case=> HlenA [HSumA1 [HSumA2 [Hni [Hna Hna']]]].

apply while.hoare_seq with ((fun s h => exists A'0, length A'0 = nk /\ [a]_s = va /\ [a']_s = va' /\
  [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e a|-->A ** var_e a'|-->A'0 ++ zero32 :: nil ** var_e m|-->M ++ zero32 :: nil) s h /\
  Zbeta nk * Sum nk A'0 =m Sum nk A * Sum nk A {{ Sum nk M }} /\ Sum nk A'0 < Sum nk M) **
((fun s h => s2Z [i]_s = ni /\ [x']_s = vx' /\
  [e]_s = ve /\ [l]_s = Z2s 32 (Z_of_nat vl)) //\\
(var_e x'|-->X' ** add_e (var_e a) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32))).

apply hoare_prop_m.hoare_stren with ((fun s h => exists A'0, length A'0 = nk /\ [a]_s = va /\
  [a']_s = va' /\ [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e a |--> A ** var_e a' |--> A'0 ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil) s h) **
((fun s h => s2Z [i]_s = ni /\ [x']_s = vx' /\ [e]_s = ve /\ [l]_s = Z2s 32 (Z_of_nat vl)) //\\
  (var_e x' |--> X' ** add_e (var_e a) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32))).

move=> s h [A' [HlenA' [r_k [r_alpha [r_e [r_l [r_a [r_a' [r_x' [r_m [r_i Hmem]]]]]]]]]]].

have {Hmem}Hmem : ((var_e a |--> A ** var_e a' |--> A' ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil) **
  (var_e x' |--> X' ** add_e (var_e a) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32)) s h.
  rewrite (decompose_last_equiv _ A) HlenA in Hmem.
  by abstract assoc_comm Hmem.
case: Hmem => h1 [h2 [Hdisj [Hunion [H1 H2]]]].
exists h1, h2; repeat (split; trivial).
by exists A'.

apply frame_rule.
- eapply mont_square_strict_init_triple => //.
  by abstract Nodup_nodup r0.
- by Inde_frame.
- move=> ?; by Inde_mult.

apply pull_out_exists_con => A'.

apply hoare_prop_m.hoare_stren with ((fun s h => (length A' = nk /\
  Zbeta nk * Sum nk A' =m Sum nk A * Sum nk A {{Sum nk M}} /\ Sum nk A' < Sum nk M) /\ h = heap.emp) **
(fun s h => exists A, length A = nk /\ [a']_s = va' /\ [x']_s = vx' /\ [a]_s = va /\
  [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e a' |--> A' ++ zero32 :: nil ** var_e x' |--> X' ** var_e a |--> A ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil) s h /\
  s2Z [i]_s = ni /\ [e]_s = ve /\ [l]_s = Z2s 32 (Z_of_nat vl))).

move=> s h [h1 [h2 [Hdisj [Hunion [[HlenA' [r_a [r_a' [r_m [r_k [r_alpha [Hmem [HSumA'1 HSumA'2]]]]]]]] [[r_i [r_x' [r_e H1]]] Hmem2]]]]]].

exists heap.emp, (h1 +++ h2); repeat (split; trivial).
by map_tac_m.Disj.
by map_tac_m.Equal.

exists A; repeat (split; trivial).
move: {Hmem Hmem2}(assert_m.con_cons _ _ _ _ _ Hdisj Hmem Hmem2) => Hmem.
rewrite (decompose_last_equiv _ A) HlenA.
by abstract assoc_comm Hmem.

apply pull_out_and; case=> HlenA' [HSumA'1 HSumA'2].
apply eqmod_sym in HSumA'1.
move: {HSumA'1}(eqmod_rewrite _ _ _ _ _ HSumA1 HSumA'1) => HSumA'1.
rewrite Zmult_comm in HSumA'1.
move: {HSumA1 HSumA'1}(eqmod_rewrite _ _ _ _ _ HSumA1 HSumA'1) => HSumA'1.
apply eqmod_sym in HSumA'1.
rewrite Zmult_comm Zmult_assoc in HSumA'1.
apply eqmod_reg_mult' in HSumA'1; last first.
  apply Zis_gcd_sym; rewrite Zbeta_power; by apply Zis_gcd_Zpower_odd.
rewrite -(Zmult_comm (Zbeta nk)) -Zmult_assoc -Zpower_b_is_exp in HSumA'1.
rewrite (_ : forall x, x + x = 2 * x)%nat in HSumA'1; last first.
  move=> x0; by rewrite (_ : 2 = 1 + 1)%nat // mult_plus_distr_r mult_1_l.
rewrite Zmult_comm in HSumA'1.

clear A HlenA HSumA2.

apply hoare_srlv with (fun s h => exists A, length A = nk /\ [a']_s = va' /\
  [x']_s = vx' /\ [a]_s = va /\ [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\
  [alpha]_s = valpha /\
  (var_e a' |--> A' ++ zero32 :: nil ** var_e x' |--> X' ** var_e a |--> A ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil) s h /\
  s2Z [i]_s = ni /\ [e]_s = ve /\ [l]_s = Z2s 32 (Z_of_nat vl) /\ [ei]_s = ve [.>>] (Zabs_nat ni)).

move=> s h [A [HlenA [r_a' [r_x' [r_a [r_m [r_k [r_alpha [Hmem [r_i [r_e r_l]]]]]]]]]]].
rewrite /wp_srlv.
repeat reg_upd.
exists A; repeat (split; trivial).

by Assert_upd.
rewrite u2Z_rem' //; last first.
  rewrite -s2Z_u2Z_pos /= r_i.
  apply Zle_lt_trans with (Z_of_nat vl); first by case: Hni.
  apply Zlt_le_trans with (Z_of_nat 32); [by apply inj_lt | done].
by case: Hni.
rewrite -s2Z_u2Z_pos; last by rewrite r_i; case: Hni.
by rewrite r_i r_e.

apply hoare_andi with (fun s h => exists A, length A = nk /\ [a']_s = va' /\
  [x']_s = vx' /\ [a]_s = va /\ [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\
  [alpha]_s = valpha /\
  (var_e a' |--> A' ++ zero32 :: nil ** var_e x' |--> X' ** var_e a |--> A ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil) s h /\
  s2Z [i]_s = ni /\ [e]_s = ve /\ [l]_s = Z2s 32 (Z_of_nat vl) /\
  u2Z [ei]_s + 2 * u2Z (ve[.>>]Zabs_nat (ni + 1)) = u2Z (ve [.>>] Zabs_nat ni) /\
  ([ei]_s = zero32 \/ [ei]_s = one32)).

move=> s h [A [HlenA [r_a' [r_x' [r_a [r_m [r_k [r_alpha [Hmem [r_i [r_e [r_l r_ei]]]]]]]]]]]].
rewrite /wp_andi.
repeat reg_upd.
exists A; repeat (split; trivial).
by Assert_upd.

rewrite r_ei /one16 zext_Z2u // int_and_rem_1 Zabs_nat_plus_pos //; last by exact (proj1 Hni).
rewrite -shrl_comp Zmult_comm Zplus_comm u2Z_shrl //; rewrite (_ : Zabs_nat 1 = 1%nat) //; by repeat constructor.
rewrite zext_Z2u //.
case: (Zeven_odd_dec (u2Z [ei]_s)).
- move/int_even_and_1 => ->; by left.
- move/int_odd_and_1 => ->; by right.

apply while.hoare_seq with (fun s h => exists A, exists A', exists new_va, exists new_va',
  length A = nk /\ length A' = nk /\ [a']_s = new_va' /\
  u2Z new_va' + 4 * Z_of_nat (S nk) < Zbeta 1 /\
  [x']_s = vx' /\ [a]_s = new_va /\ u2Z new_va + 4 * Z_of_nat (S nk) < Zbeta 1 /\
  [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e a |--> A ++ zero32::nil ** var_e x' |--> X' ** var_e a' |--> A' ++ zero32::nil ** var_e m |--> M ++ zero32 :: nil) s h /\
  Sum nk A =m Sum nk X ^^ Zabs_nat ((2 * u2Z (ve[.>>]Zabs_nat (ni+1))) + u2Z((ve[.>>]Zabs_nat ni)[.&]one32)) * Zbeta nk {{ Sum nk M }} /\
  Sum nk A < Sum nk M /\ s2Z [i]_s = ni /\ [e]_s = ve /\ [l]_s = Z2s 32 (Z_of_nat vl) /\
  u2Z [ei]_s + 2 * u2Z (ve[.>>]Zabs_nat (ni + 1)) = u2Z (ve[.>>]Zabs_nat ni)).

apply while.hoare_ifte.

apply hoare_xor with (fun s h => exists A, length A = nk /\ [a']_s = va' /\
  [x']_s = vx' /\ [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (((var_e a' |--> A' ++ zero32 :: nil ** var_e x' |--> X') ** int_e va |--> A ++ zero32 :: nil) ** var_e m |--> M ++ zero32 :: nil) s h /\
  s2Z [i]_s = ni /\ [e]_s = ve /\ [l]_s = Z2s 32 (Z_of_nat vl) /\
  u2Z [ei]_s + 2 * u2Z (ve[.>>]Zabs_nat (ni + 1)) = u2Z (ve[.>>]Zabs_nat ni) /\
  [ei]_s = zero32 /\ [a]_s = va [.(+)] va').

move=> s h [[A [HlenA [r_a' [r_x' [r_a [r_m [r_k [r_alpha [Hmem [r_i [r_e [r_l [r_ei r_ei']]]]]]]]]]]]] Heqei0];
  rewrite /= in Heqei0. move/Zeq_boolP : Heqei0 => Heqei0.

rewrite /wp_xor.
repeat reg_upd.
exists A; repeat (split; trivial).
Assert_upd.
assoc_comm Hmem.
move: Hmem.
by apply mapstos_ext.
by move/u2Z_inj : Heqei0.
by rewrite -r_a -r_a'.

apply hoare_xor with (fun s h => exists A, length A = nk /\ [x']_s = vx' /\ [m]_s = vm /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (((int_e va' |--> A' ++ zero32 :: nil ** var_e x' |--> X') ** int_e va |--> A ++ zero32 :: nil) ** var_e m |--> M ++ zero32 :: nil) s h /\
  s2Z [i]_s = ni /\ [e]_s = ve /\ [l]_s = Z2s 32 (Z_of_nat vl) /\
  u2Z [ei]_s + 2 * u2Z (ve[.>>]Zabs_nat (ni + 1)) = u2Z (ve[.>>]Zabs_nat ni) /\
  [ei]_s = zero32 /\ [a]_s = va [.(+)] va' /\ [a']_s = va' [.(+)] (va [.(+)] va')).

move=> s h [A [HlenA [r_a' [r_x' [r_m [r_k [r_alpha [Hmem [r_i [r_e [r_l [r_ei [r_ei' r_a]]]]]]]]]]]]].

rewrite /wp_xor.
repeat reg_upd.
exists A; repeat (split; trivial).
Assert_upd.
assoc_comm Hmem.
by move: Hmem; apply mapstos_ext.
by rewrite r_a r_a' int_xor_comm.

apply hoare_xor'.

move=> s h [A [HlenA [r_x' [r_m [r_k [r_alpha [Hmem [r_i [r_e [r_l [r_ei [r_ei' [r_a r_a']]]]]]]]]]]]].

rewrite /wp_xor.
repeat reg_upd.
exists A', A, va', va; repeat (split; trivial).
by rewrite r_a' int_xor_comm int_xor_assoc int_xor_self int_xor_0.
by rewrite r_a' r_a int_xor_comm int_xor_assoc int_xor_self int_xor_0.

move: Hmem.
apply monotony => h'.
apply monotony => h''.
apply monotony => h'''.
apply mapstos_ext => //=.
reg_upd.
by rewrite r_a r_a' /= int_xor_comm int_xor_assoc int_xor_self int_xor_0.
apply mapstos_ext => //=.
by reg_upd.
apply mapstos_ext => //=.
reg_upd.
by rewrite /= r_a' int_xor_comm int_xor_assoc int_xor_self int_xor_0.
apply mapstos_ext => //=.
by reg_upd.

rewrite Zabs_nat_plus_pos; last 2 first.
  apply Zmult_le_0_compat => //; by apply min_u2Z.
  by apply min_u2Z.
apply: (eqmod_trans _ _ _ _ HSumA'1).
apply eqmod_reg_mult.
rewrite Zabs_nat_mult (_ : Zabs_nat 2 = 2%nat); last by done.
rewrite int_even_and_1; last first.
  rewrite -r_ei r_ei' u2Z_Z2u // Zplus_0_l; by apply Zeven_2.
rewrite u2Z_Z2u // [Zabs_nat 0]/= plus_0_r.
by apply eqmod_refl.

apply hoare_prop_m.hoare_stren with ((fun s h => exists A, length A = nk /\
  [a']_s = va' /\ [x']_s = vx' /\ [a]_s = va /\ [m]_s = vm /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e a' |--> A' ** var_e x' |--> X' ** var_e a |--> A ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil) s h) **
((fun s _ => s2Z [i]_s = ni /\ [e]_s = ve /\ [l]_s = Z2s 32 (Z_of_nat vl) /\
  u2Z [ei]_s + 2 * u2Z (ve [.>>] Zabs_nat (ni + 1)) = u2Z (ve [.>>] Zabs_nat ni) /\ [ei]_s = one32) //\\
 (add_e (var_e a') (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32))).

move=> s h [ [A [HlenA [r_a' [r_x' [r_a [r_m [r_k [r_alpha [Hmem [r_i [r_e [r_l [r_ei r_ei']]]]]]]]]]]]] Hbneei0];
  rewrite /= in Hbneei0. move/Zeq_boolP : Hbneei0 => Hbneei0.

have {Hmem}Hmem : ((((var_e a' |--> A' ** var_e x' |--> X') ** var_e a |--> A ++ zero32 :: nil) ** var_e m |--> M ++ zero32 :: nil) ** (add_e (var_e a') (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32)) s h.
  rewrite (decompose_last_equiv _ A') HlenA' in Hmem.
  by abstract assoc_comm Hmem.
case: Hmem => h1 [h2 [Hdisj [Hunion [Hmem1 Hmem2]]]].
exists h1, h2; repeat (split; trivial).
exists A; repeat (split; trivial).
case: r_ei' => r_ei' //.
by rewrite store.get_r0 r_ei' in Hbneei0.

apply hoare_prop_m.hoare_weak with ((fun s h => exists A, length A = nk /\
  [a']_s = va' /\ [x']_s = vx' /\ [a]_s = va /\ [m]_s = vm /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e a' |--> A' ** var_e x' |--> X' ** var_e a |--> A ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil) s h /\
  Zbeta nk * Sum nk A =m Sum nk A' * Sum nk X' {{ Sum nk M }} /\ Sum nk A < Sum nk M) **
((fun s m => s2Z [i]_s = ni /\ [e]_s = ve /\ [l]_s = Z2s 32 (Z_of_nat vl) /\
  u2Z [ei]_s + 2 * u2Z (ve[.>>]Zabs_nat (ni + 1)) = u2Z (ve[.>>]Zabs_nat ni) /\ [ei]_s = one32) //\\
 (add_e (var_e a') (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32))).

move=> s h [h1 [h2 [Hdisj [Hunion [[A [HlenA [r_a' [r_x' [r_a [r_m [r_k [r_alpha [Hmem1 [Sum_A1 Sum_A2]]]]]]]]]] [[r_i [r_e [r_l [r_ei r_ei']]]] Hmem2]]]]]].

exists A, A', va, va'; repeat (split; trivial).
rewrite (decompose_last_equiv _ A') HlenA'.
move: {Hmem1 Hmem2}(assert_m.con_cons _ _ _ _ _ Hdisj Hmem1 Hmem2) => Hmem.
rewrite -Hunion in Hmem.
by abstract assoc_comm Hmem.

apply: (eqmod_reg_mult_beta_odd _ _ nk _ HZoddM).
apply: (eqmod_trans _ _ _ _ Sum_A1).
apply eqmod_sym in HSumA'1; apply: (eqmod_rewrite _ _ _ _ _ HSumA'1).
rewrite Zmult_comm.
apply eqmod_sym in HSumX'1; apply: (eqmod_rewrite _ _ _ _ _ HSumX'1).

rewrite Zmult_assoc Zmult_comm.

apply eqmod_reg_mult_l.
rewrite Zmult_comm Zmult_assoc.
apply eqmod_reg_mult.
rewrite Zmult_comm -Zpower_S int_odd_and_1; last first.
  rewrite -r_ei r_ei' u2Z_Z2u // Zplus_comm.
  by apply Zodd_1.
rewrite u2Z_Z2u //.
apply eqmod_sym.
rewrite Zabs_nat_plus_pos //; last first.
  apply Zmult_le_0_compat; [done | by apply min_u2Z].
rewrite Zabs_nat_mult plus_comm.
by apply eqmod_refl.

apply frame_rule.
- eapply mont_mul_strict_init_triple => //.
  by abstract Nodup_nodup r0.
- by Inde_frame.
- move=> ?; by Inde_mult.

clear HSumA'1 HSumA'2 HlenA' A'.

apply pull_out_exists => A.
apply pull_out_exists => A'.
clear va Hna va' Hna'.
apply pull_out_exists => va.
apply pull_out_exists => va'.

apply hoare_prop_m.hoare_stren with ((fun s h => (length A = nk /\ length A' = nk /\
    u2Z va + 4 * Z_of_nat (S nk) < Zbeta 1 /\ u2Z va' + 4 * Z_of_nat (S nk) < Zbeta 1 /\
    Sum nk A =m Sum nk X ^^ Zabs_nat (2 * u2Z (ve [.>>] Zabs_nat (ni + 1)) + u2Z ((ve [.>>] Zabs_nat ni) [.&] one32)) * Zbeta nk {{Sum nk M}} /\
    Sum nk A < Sum nk M) /\ h = heap.emp) **
(fun s h => [a']_s = va' /\ [x']_s = vx' /\ [a]_s = va /\
  [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  s2Z [i]_s = ni /\ [e]_s = ve /\ [l]_s = Z2s 32 (Z_of_nat vl) /\
  u2Z [ei]_s + 2 * u2Z (ve [.>>] Zabs_nat (ni + 1)) = u2Z (ve [.>>] Zabs_nat ni) /\
  ((((var_e a' |--> A' ** var_e x' |--> X') ** var_e a |--> A ++ zero32 :: nil) ** var_e m |--> M ++ zero32 :: nil) **
    (add_e (var_e a') (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32)) s h)).

move=> s h [HlenA [HlenA' [r_a' [Hna' [r_x' [r_a [Hna [r_m [r_k [r_alpha [Hmem [Sum_A1 [Sum_A2 [r_i [Hgpe [r_l r_ei]]]]]]]]]]]]]]]].
exists heap.emp, h; repeat (split; trivial).
by map_tac_m.Disj.
by map_tac_m.Equal.
rewrite (decompose_last_equiv _ A') HlenA' in Hmem.
by abstract assoc_comm Hmem.

apply pull_out_and; case => HlenA [HlenA' [Hna [Hna' [HSumA1 HSumA2]]]].