Library mont_square_strict_triple

Require Import ssreflect ssrbool eqtype.
Require Import Arith_ext ZArith_ext Lists_ext.
Require Import machine_int multi_int.
Import MachineInt.
Require Import mips_seplog mips_frame mips_tactics mips_contrib mapstos.
Require Import mont_mul_strict_prg.
Require Import mont_square_triple multi_lt_triple multi_sub_inplace_left_triple.

Local Open Scope machine_int_scope.
Local Open Scope eqmod_scope.
Local Open Scope heap_scope.
Local Open Scope nodup_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.

Section mont_square_strict.

Variables k alpha x z m one ext int_ X_ Y_ M_ Z_ quot C t s_ : reg.

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

apply while.hoare_seq with ((fun s h => exists Z, length Z = nk /\
  [x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M) s h /\
  Zbeta nk * Sum (S nk) (Z ++ [C]_s :: nil) =m Sum nk X * Sum nk X {{ Sum nk M }} /\
  Sum (S nk) (Z ++ [C]_s :: nil) < 2 * Sum nk M /\
  u2Z [t]_s = u2Z vz + 4 * Z_of_nat (nk - 1)) **
(add_e (var_e z) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32
  ** add_e (var_e m) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32)).

apply hoare_prop_m.hoare_stren with ((fun s h => [x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e z |--> rep zero32 nk ** var_e m |--> M) s h /\ store.multi_null s) **
(add_e (var_e z) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32
  ** add_e (var_e m) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32)).

move=> s h [[r_x [r_z [r_m_ [r_k [r_alpha [Hmem Hmultiplier]]]]]]].

rewrite !assert_m.con_assoc_equiv assert_m.con_com_equiv !assert_m.con_assoc_equiv
  decompose_last_equiv len_rep !assert_m.con_assoc_equiv assert_m.con_com_equiv !assert_m.con_assoc_equiv in Hmem.

rewrite assert_m.con_com_equiv !assert_m.con_assoc_equiv.
move: Hmem; apply monotony=> // h' Hmem.
rewrite decompose_last_equiv HlenM in Hmem.
rewrite !assert_m.con_assoc_equiv assert_m.con_com_equiv !assert_m.con_assoc_equiv in Hmem.
by move: Hmem; apply monotony => // h'' Hmem.

apply frame_rule => //.
- eapply mont_square_triple; eauto.
  eapply Zlt_trans; last by apply Hnz.
  rewrite Z_S Zmult_plus_distr_r !Zplus_assoc -{1}[_ + _]Zplus_0_r; by apply Zplus_lt_compat_l.
- by Inde_frame.

apply pull_out_exists_con => Z.

apply hoare_prop_m.hoare_stren with ((fun s h => length Z = nk /\ h = heap.emp) **
  (fun s h => [x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\
    u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
    Zbeta nk * Sum (S nk) (Z ++ [C]_s :: nil) =m Sum nk X * Sum nk X {{ Sum nk M }} /\
    Sum (S nk) (Z ++ [C]_s :: nil) < 2 * Sum nk M /\ u2Z [t]_s = u2Z vz + 4 * Z_of_nat (nk - 1) /\
    ((var_e x |--> X ** var_e z |--> Z ** var_e m |--> M
      ** add_e (var_e z) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32
        ** add_e (var_e m) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32) s h))).

move=> s h [h1 [h2 [Hdisj [Hunion [[len_Z [r_x [r_z [r_m [r_k [r_alpha [Hmem [Sum_Z1 [Sum_Z2 r_t]]]]]]]]] Hmem2]]]]].
exists heap.emp, (h1 +++ h2); repeat (split; trivial).
by map_tac_m.Disj.
by map_tac_m.Equal.
rewrite assert_m.con_assoc_equiv; by Compose_sepcon h1 h2.

apply pull_out_and => len_Z.

apply while.hoare_ifte.

apply hoare_prop_m.hoare_stren with (fun s h =>
  (([x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\
    u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
    Zbeta nk * Sum (S nk) (Z ++ zero32 :: nil) =m Sum nk X * Sum nk X {{Sum nk M}}) /\
  Sum (S nk) (Z ++ zero32 :: nil) < 2 * Sum nk M /\
  u2Z [t]_s = u2Z vz + 4 * Z_of_nat (nk - 1) /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M **
    add_e (var_e z) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32 **
      add_e (var_e m) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32) s h)).

move=> s h [ [r_x [r_z [r_m [r_k [r_alpha [Sum_Z1 [Sum_Z2 [r_t Hmem]]]]]]]] HbeqC0].

rewrite /= store.get_r0 in HbeqC0; move/Zeq_boolP : HbeqC0; move/u2Z_inj => HbeqC0.
by rewrite HbeqC0 in Sum_Z1 Sum_Z2.

apply hoare_prop_m.hoare_stren with ((fun s h => (u2Z [k]_s = Z_of_nat nk /\
  [z]_s = vz /\ [m]_s = vm /\ (var_e z |--> Z ** var_e m |--> M) s h)) **
((fun s h => [x]_s = vx /\ [alpha]_s = valpha /\
  Zbeta nk * Sum (S nk) (Z ++ zero32 :: nil) =m Sum nk X * Sum nk X {{Sum nk M}} /\
  Sum (S nk) (Z ++ zero32 :: nil) < 2 * Sum nk M /\
  u2Z [t]_s = u2Z vz + 4 * Z_of_nat (nk - 1)) //\\
(var_e x |--> X ** add_e (var_e z) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32 **
  add_e (var_e m) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32))).

move=> s h [[r_x [r_z [r_m [r_k [r_alpha Sum_Z1]]]]] [Sum_Z2 [r_t Hmem]]].

have {Hmem}Hmem : ((var_e z |--> Z ** var_e m |--> M) **
  (var_e x |--> X ** add_e (var_e z) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32 **
    add_e (var_e m) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32)) s h.
  by assoc_comm Hmem.
case: Hmem => h1 [h2 [Hdisj [Hunion [H1 H2]]]].
by exists h1, h2.

apply while.hoare_seq with ((fun s h => u2Z [k]_s = Z_of_nat nk /\
  [z]_s = vz /\ [m]_s = vm /\
  ((Sum nk Z < Sum nk M /\ [int_]_s = one32 /\ [ext]_s = zero32) \/
    (Sum nk Z > Sum nk M /\ [int_]_s = zero32 /\ [ext]_s = one32) \/
    (Sum nk Z = Sum nk M /\ [int_]_s = zero32 /\ [ext]_s = zero32)) /\
  (var_e z |--> Z ** var_e m |--> M) s h) **
((fun s h => [x]_s = vx /\ [alpha]_s = valpha /\
  (Zbeta nk * Sum (S nk) (Z ++ zero32 :: nil) =m Sum nk X * Sum nk X {{Sum nk M}}) /\
  Sum (S nk) (Z ++ zero32 :: nil) < 2 * Sum nk M /\
  u2Z [t]_s = u2Z vz + 4 * Z_of_nat (nk - 1)) //\\
(var_e x |--> X ** add_e (var_e z) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32 **
  add_e (var_e m) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32))).

apply frame_rule.
- eapply multi_lt_triple; eauto.
  by Nodup_nodup r0.
- by Inde_frame.
- move=> ?; by Inde_mult.

apply while.hoare_ifte.

apply hoare_prop_m.hoare_stren with ((fun s h => Sum nk M <= Sum nk Z /\ h = heap.emp) **
  (fun s h => [z]_s = vz /\ [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\
    [x]_s = vx /\ [alpha]_s = valpha /\
    (Zbeta nk * Sum (S nk) (Z ++ zero32 :: nil) =m Sum nk X * Sum nk X {{Sum nk M}}) /\
    Sum (S nk) (Z ++ zero32 :: nil) < 2 * Sum nk M /\
    u2Z [t]_s = u2Z vz + 4 * Z_of_nat (nk - 1) /\
    ((var_e z |--> Z ** var_e m |--> M) **
      (var_e x |--> X ** add_e (var_e z) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32 **
        add_e (var_e m) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32)) s h)).

move=> s h [[h1 [h2 [Hdisj [Hunion [[r_k [r_z [r_m [Hor Hmem]]]] [[r_x [r_alpha [Sum_Z1 [Sum_Z2 r_t]]]] Hmem2]]]]]] Hbeqint0].

rewrite /= store.get_r0 in Hbeqint0; move/Zeq_boolP : Hbeqint0 => Hbeqint0.

exists heap.emp, (h1 +++ h2); repeat (split; trivial).
by map_tac_m.Disj.
by map_tac_m.Equal.
case : Hor.
- case => _ [Hor _]; by rewrite Hor /one32 /zero32 2?u2Z_Z2u in Hbeqint0.
- case; by [case=> H _; apply Zlt_le_weak, Zgt_lt | case=> -> _; apply Zle_refl].
- by exists h1, h2.

apply pull_out_and => HZM.

apply hoare_prop_m.hoare_stren with ((fun s h => ([z]_s = vz /\ [m]_s = vm /\
  u2Z [k]_s = Z_of_nat nk /\ (var_e z |--> Z ** var_e m |--> M) s h)) **
(fun s h => [x]_s = vx /\ [alpha]_s = valpha /\
  (Zbeta nk * Sum (S nk) (Z ++ zero32 :: nil) =m Sum nk X * Sum nk X {{Sum nk M}}) /\
  Sum (S nk) (Z ++ zero32 :: nil) < 2 * Sum nk M /\
  u2Z [t]_s = u2Z vz + 4 * Z_of_nat (nk - 1) /\
  (var_e x |--> X ** add_e (var_e z) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32 **
      add_e (var_e m) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32) s h)).

move=> s h [r_z [r_m [r_k [r_x [r_alpha [Sum_Z1 [Sum_Z2 [Hgpt Hmem]]]]]]]].

case: Hmem => h1 [h2 [Hdisj [Hunion [H1 H2]]]].
by exists h1, h2.

apply hoare_prop_m.hoare_weak with ((fun s h => exists Z', length Z' = nk /\ [z]_s = vz /\
  [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\ [C]_s = zero32 /\ (var_e z |--> Z' ** var_e m |--> M) s h /\
  Sum nk Z' = Sum nk Z - Sum nk M) **
(fun s h => [x]_s = vx /\ [alpha]_s = valpha /\
  (Zbeta nk * Sum (S nk) (Z ++ zero32 :: nil) =m Sum nk X * Sum nk X {{ Sum nk M }}) /\
  Sum (S nk) (Z ++ zero32 :: nil) < 2 * Sum nk M /\
  u2Z [t]_s = u2Z vz + 4 * Z_of_nat (nk - 1) /\
  (var_e x |--> X ** add_e (var_e z) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32 **
    add_e (var_e m) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32)s h)).

move=> s h [h1 [h2 [Hdisj [Hunion [[Z' [len_Z' [r_z [r_m [r_k [HC [Hmem1 HSumSub]]]]]]] [r_x [r_alpha [Sum_Z1 [Sum_Z2 [r_t Hmem2]]]]]]]]]].
exists Z'; repeat (split; trivial).

move: (assert_m.con_cons _ _ _ _ _ Hdisj Hmem1 Hmem2).
rewrite -Hunion => Htmp.
rewrite 2!decompose_last_equiv len_Z' HlenM; by assoc_comm Htmp.

rewrite HSumSub.
rewrite (Sum_cut _ _ len_Z (S nk) (Z ++ zero32 :: nil) (zero32 :: nil)) // in Sum_Z1; last by rewrite app_length /= len_Z plus_comm.
rewrite minus_Sn_n /= /zero32 u2Z_Z2u // Zmult_0_r // Zplus_0_r in Sum_Z1.
rewrite Zmult_minus_distr_l; by apply eqmod_minmod.

rewrite (Sum_cut _ _ len_Z (S nk) (Z ++ zero32 :: nil) (zero32 :: nil)) // in Sum_Z2; last by rewrite app_length /= len_Z plus_comm.
rewrite minus_Sn_n [Sum 1 _]/= /zero32 u2Z_Z2u // Zmult_0_r // in Sum_Z2.
rewrite HSumSub; omega.

apply frame_rule.
- eapply multi_sub_inplace_left_triple_B_le_A; eauto.
  + by Nodup_nodup r0.
  + eapply Zlt_trans; last by apply Hnz.
    rewrite Z_S Zmult_plus_distr_r !Zplus_assoc -{1}[_ + _]Zplus_0_r; by apply Zplus_lt_compat_l.
- by Inde_frame.
- move=> ?; by Inde_mult.

apply hoare_nop'.

move=> s h [ [h1 [h2 [Hdisj [Hunion [[r_k [r_z [r_m [Hor Hmem1]]]] [[r_x [r_alpha [Sum_Z1 [Sum_Z2 r_t]]]] Hmem2]]]]]] Hbneint0].
exists Z; repeat (split; trivial).

move: (assert_m.con_cons _ _ _ _ _ Hdisj Hmem1 Hmem2).
rewrite -Hunion => Htmp.
rewrite 2!decompose_last_equiv len_Z HlenM; by assoc_comm Htmp.

rewrite (Sum_cut _ _ len_Z (S nk) (Z ++ zero32 :: nil) (zero32 :: nil)) // in Sum_Z1; last by rewrite app_length /= len_Z plus_comm.
by rewrite minus_Sn_n /= /zero32 u2Z_Z2u // Zmult_0_r Zplus_0_r in Sum_Z1.
case: Hor.
- by case.
- rewrite /= store.get_r0 in Hbneint0; move/Zeq_boolP : Hbneint0 => Hbneint0.
  case.
  + case=> _ [Hor _]; by rewrite Hor in Hbneint0.
  + move=> [_ [Hor _]]; by rewrite Hor in Hbneint0.

apply hoare_addiu with (fun s h => ([x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (Zbeta nk * Sum (S nk) (Z ++ [C]_s :: nil) =m Sum nk X * Sum nk X {{Sum nk M}}) /\
  Sum (S nk) (Z ++ [C]_s :: nil) < 2 * Sum nk M /\
  u2Z [t]_s = u2Z vz + 4 * Z_of_nat nk /\ u2Z [C]_s <> u2Z (zero32) /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M **
    add_e (var_e z) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32 **
      add_e (var_e m) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32) s h)).

move=> s h [[r_x [r_z [r_m [r_k [r_alpha [Sum_Z1 [Sum_Z2 [r_t Hmem]]]]]]]] HbneC0].
rewrite /wp_addiu; repeat reg_upd; repeat (split; trivial).
- rewrite sext_Z2u // u2Z_add_Z2u //.
  + rewrite r_t inj_minus1 //; last by destruct nk => //; by apply le_n_S, le_O_n.
    ring.
  + rewrite r_t // inj_minus1; last by destruct nk => //; by apply le_n_S, le_O_n.
    rewrite -Zbeta1_Zpower2; rewrite Z_S in Hnz; omega.
- rewrite /= store.get_r0 // in HbneC0; by move/Zeq_boolP : HbneC0.
- by Assert_upd.

apply hoare_sw_back'' with (fun s h => ([x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  Zbeta nk * Sum (S nk) (Z ++ [C]_s :: nil) =m Sum nk X * Sum nk X {{Sum nk M}} /\
  Sum (S nk) (Z ++ [C]_s :: nil) < 2 * Sum nk M /\
  u2Z [t]_s = u2Z vz + 4 * Z_of_nat nk /\ u2Z [C]_s <> u2Z (zero32) /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M **
    add_e (var_e z) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e [C]_s **
      add_e (var_e m) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32) s h)).

move=> s h [r_x [r_z [r_m [r_k [r_alpha [Sum_Z1 [Sum_Z2 [r_t [r_C Hmem]]]]]]]]].

have Htmp : [t]_s [.+] sext 16 zero16 = [z]_s [.+] Z2u 32 (Z_of_nat (4 * nk)).
  rewrite sext_0 add_0; apply u2Z_inj.
  rewrite r_t u2Z_add_Z2u //.
  rewrite r_z inj_mult; ring.
  by apply Zle_0_nat.
  rewrite r_z -Zbeta1_Zpower2 inj_mult [Z_of_nat 4]/=.
  rewrite Z_S in Hnz; move: (min_u2Z vz) => ?; omega.

exists (int_e zero32).
rewrite !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 => // h'.
by apply mapsto_ext.

apply currying => h0 H0.

repeat (split; trivial).
assoc_comm H0.
move: H0; by apply mapsto_ext.


apply hoare_addiu with (fun s h => ([x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  Zbeta nk * Sum (S nk) (Z ++ [C]_s :: nil) =m Sum nk X * Sum nk X {{Sum nk M}} /\
  Sum (S nk) (Z ++ [C]_s :: nil) < 2 * Sum nk M /\
  u2Z [t]_s = u2Z vz + 4 * Z_of_nat nk /\ u2Z [C]_s <> u2Z (zero32) /\
  u2Z [ext]_s = Z_of_nat (S nk) /\
  (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M **
    add_e (var_e z) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e [C]_s **
      add_e (var_e m) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32) s h)).

move=> s h [r_x [r_z [r_m [r_k [r_alpha [Sum_Z1 [Sum_Z2 [r_t [r_C Hmem]]]]]]]]].
rewrite /wp_addiu; repeat reg_upd; repeat (split; trivial).
- rewrite sext_Z2u // u2Z_add_Z2u //.
  + rewrite r_k Z_S; ring.
  + rewrite r_k -Zbeta1_Zpower2.
    rewrite Z_S in Hnz; move: (min_u2Z vz) => ?; omega.
- by Assert_upd.

apply hoare_prop_m.hoare_stren with ((fun s h => exists Cint32,
  (Sum (S nk) (M ++ zero32 :: nil) <= Sum (S nk) (Z ++ Cint32 :: nil) /\ [C]_s = Cint32) /\ h = heap.emp) **
(fun s h => ([x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (Zbeta nk * Sum (S nk) (Z ++ [C]_s :: nil) =m Sum nk X * Sum nk X {{Sum nk M}}) /\
  Sum (S nk) (Z ++ [C]_s :: nil) < 2 * Sum nk M /\
  u2Z [t]_s = u2Z vz + 4 * Z_of_nat nk /\ u2Z [ext]_s = Z_of_nat (S nk) /\
  ((var_e x |--> X ** var_e z |--> Z ** var_e m |--> M **
    add_e (var_e z) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e [C]_s **
      add_e (var_e m) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32) s h)))).

move=> s h [r_x [r_z [r_m [r_k [r_alpha [Sum_Z1 [Sum_Z2 [r_t [r_C [r_ext Hmem]]]]]]]]]].
exists heap.emp, h; repeat (split; trivial).
by map_tac_m.Disj.
by map_tac_m.Equal.
exists ([C]_s); repeat (split; trivial).
rewrite Sum_cut_last; last by rewrite app_length /= HlenM plus_comm.
rewrite Sum_cut_last; last by rewrite app_length /= len_Z plus_comm.
rewrite /= -minus_n_O /zero32 u2Z_Z2u // Zmult_0_r Zplus_0_r.
move: (Sum_max 32 nk M); rewrite -Zbeta_power => Htmp.
move: (min_Sum Z nk) => Htmp2.
move: (min_Sum M nk) => Htmp3.
have Htmp4 : 0 < u2Z [C]_s.
  rewrite /zero32 u2Z_Z2u // in r_C.
  apply Zle_neq_lt; [by apply min_u2Z | contradict r_C; done].
apply Zle_trans with (Sum nk Z + Zbeta nk * 1); first by omega.
apply Zplus_le_compat_l, Zmult_le_compat_l; [omega | by apply Zbeta_0'].

apply pull_out_exists_con => Cint32.

apply hoare_prop_m.hoare_stren with (
  (fun s h => Sum (S nk) (M ++ zero32 :: nil) <= Sum (S nk) (Z ++ Cint32 :: nil) /\ h = heap.emp) **
  (fun s h => ([x]_s = vx /\ [z]_s = vz /\ [m]_s = vm /\
    u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\ [C]_s = Cint32 /\
    (Zbeta nk * Sum (S nk) (Z ++ [C]_s :: nil) =m Sum nk X * Sum nk X {{Sum nk M}}) /\
    Sum (S nk) (Z ++ [C]_s :: nil) < 2 * Sum nk M /\
    u2Z [t]_s = u2Z vz + 4 * Z_of_nat nk /\ u2Z [ext]_s = Z_of_nat (S nk) /\
    (var_e x |--> X ** var_e z |--> Z ** var_e m |--> M **
      add_e (var_e z) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e [C]_s **
        add_e (var_e m) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32) s h))).

move=> s h [h1 [h2 [Hdisj [Hunion [[[Sum_Z1 r_C] Hh1] [r_x [r_z [r_m [r_k [r_alpha [Sum_Z2 [Sum_Z3 [r_t [r_ext Hmem]]]]]]]]]]]]]].
by exists h1, h2.

apply pull_out_and => HZM.

apply hoare_prop_m.hoare_stren with ((fun s h => ([z]_s = vz /\
  [m]_s = vm /\ u2Z [ext]_s = Z_of_nat (S nk) /\
  (var_e z |--> (Z ++ Cint32 :: nil) ** var_e m |--> M ++ zero32 :: nil) s h)) **
(fun s h => [x]_s = vx /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (Zbeta nk * Sum (S nk) (Z ++ Cint32 :: nil) =m Sum nk X * Sum nk X {{Sum nk M}}) /\
  Sum (S nk) (Z ++ Cint32 :: nil) < 2 * Sum nk M /\
  u2Z [t]_s = u2Z vz + 4 * Z_of_nat nk /\ (var_e x |--> X) s h)).

move=> s h [r_x [r_z [r_m [r_k [r_alpha [r_C [Sum_Z1 [Sum_Z2 [r_t [r_ext Hmem]]]]]]]]]].

have {Hmem}Hmem : ((var_e z |--> Z ++ Cint32 :: nil ** var_e m |--> M ++ zero32 :: nil) ** (var_e x |--> X)) s h.
  rewrite 2!decompose_last_equiv len_Z HlenM.
  assoc_comm Hmem.
  by rewrite -r_C.
case: Hmem => h1 [h2 [Hdisj [Hunion [H1 H2]]]].
exists h1, h2; repeat (split; trivial).
by rewrite -r_C.
by rewrite -r_C.

apply hoare_prop_m.hoare_weak with ((fun s h => exists Z', length Z' = S nk /\ [z]_s = vz /\
  [m]_s = vm /\ u2Z [ext]_s = Z_of_nat (S nk) /\ [C]_s = zero32 /\
  (var_e z |--> Z' ** var_e m |--> M ++ zero32 :: nil) s h /\
  Sum (S nk) Z' = Sum (S nk) (Z ++ Cint32 :: nil) - Sum (S nk) (M ++ zero32 :: nil)) **
(fun s h => [x]_s = vx /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
    (Zbeta nk * Sum (S nk) (Z ++ Cint32 :: nil) =m Sum nk X * Sum nk X {{ Sum nk M }}) /\
    Sum (S nk) (Z ++ Cint32 :: nil) < 2 * Sum nk M /\
    u2Z [t]_s = u2Z vz + 4 * Z_of_nat nk /\ (var_e x |--> X) s h)).

move=> s h [h1 [h2 [Hdisj [Hunion [[Z' [len_Z' [r_z [r_m_ [r_ext [HC [Hmem1 Sum_Z']]]]]]] [r_x [r_k [r_alpha [HsumZC2 [HsumZC3 [r_t Hmem2]]]]]]]]]]].

have [Z'' [HlenZ'' HZ'Z'']] :
  exists Z'', length Z'' = nk /\ Z' = Z'' ++ zero32 :: nil.
  have Htmp : Sum (S nk) Z' < Sum (S nk) (M ++ zero32 :: nil).
    rewrite Sum_Z' (Sum_cut_last (S nk) M); last by rewrite app_length /= HlenM plus_comm.
    rewrite !minus_Sn_1 /zero32 u2Z_Z2u // Zmult_0_r Zplus_0_r.
    rewrite (Sum_cut_last (S nk) M) in HZM; last by rewrite app_length /= HlenM plus_comm.
    rewrite minus_Sn_1 /zero32 u2Z_Z2u // Zmult_0_r Zplus_0_r in HZM.
    apply Zlt_le_trans with (2 * Sum nk M - Sum nk M); [by apply Zminus_lt_compat_r | omega].
  have Htmp' : Sum (S nk) Z' < Zbeta nk.
    rewrite (Sum_cut _ _ HlenM (S nk) (M ++ zero32 :: nil) (zero32 :: nil)) // in Htmp; last by rewrite app_length /= HlenM plus_comm.
    rewrite minus_Sn_n [Sum 1 (zero32 :: nil)]/= /zero32 u2Z_Z2u // Zmult_0_r Zplus_0_r in Htmp.
    move: (Sum_max _ nk M); rewrite -Zbeta_power => ?; omega.
  rewrite (Sum_beyond_inv 32 (S nk) _ nk len_Z').
  exists (firstn nk Z'); split => //.
  by eapply len_firstn; eauto.
  by rewrite minus_Sn_n.
  by apply lt_n_Sn.
  by rewrite -Zbeta_power.

exists Z''; repeat (split; trivial).

rewrite -HZ'Z'' assert_m.con_assoc_equiv assert_m.con_com_equiv.

exists h1, h2; repeat (split => //).

rewrite HZ'Z'' (Sum_cut _ _ HlenZ'' (S nk) (Z'' ++ zero32 :: nil) (zero32 :: nil)) // in Sum_Z'; last by rewrite app_length /= HlenZ'' plus_comm.
rewrite minus_Sn_n (Sum_cut _ _ HlenM (S nk) (M ++ zero32 :: nil) (zero32 :: nil)) // in Sum_Z'; last by rewrite app_length /= HlenM plus_comm.
rewrite minus_Sn_n [Sum 1 (zero32 :: nil)]/= /zero32 u2Z_Z2u // Zmult_0_r 2!Zplus_0_r in Sum_Z'.
rewrite Sum_Z' Zmult_minus_distr_l; by apply eqmod_minmod.

rewrite HZ'Z'' (Sum_cut _ _ HlenZ'' (S nk) (Z'' ++ zero32 :: nil) (zero32 :: nil)) // in Sum_Z'; last by rewrite app_length /= HlenZ'' plus_comm.
rewrite minus_Sn_n (Sum_cut _ _ HlenM (S nk) (M ++ zero32 :: nil) (zero32 :: nil)) // in Sum_Z'; last by rewrite app_length /= HlenM plus_comm.
rewrite minus_Sn_n [Sum 1 (zero32 :: nil)]/= /zero32 u2Z_Z2u // Zmult_0_r 2!Zplus_0_r in Sum_Z'.
rewrite Sum_Z'.
apply Zlt_le_trans with (2 * Sum nk M - Sum nk M); [by apply Zminus_lt_compat_r | omega].

apply frame_rule.
- eapply multi_sub_inplace_left_triple_B_le_A; eauto.
  by Nodup_nodup r0.
  by rewrite app_length /= len_Z plus_comm.
  by rewrite app_length /= HlenM plus_comm.
- by Inde_frame.
- move=> ?; by Inde_mult.
Qed.

End mont_square_strict.