Library mont_mul_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_contrib mips_tactics mapstos.
Require Import mont_mul_strict_prg mont_mul_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_mul_strict_triple.

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

Lemma mont_mul_strict_triple :
  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 (S 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 ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil) s h /\
    store.multi_null s }}
  mont_mul_strict 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 ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil) s h /\
    Zbeta nk * Sum nk Z =m Sum nk X * Sum nk Y {{ Sum nk M }} /\ Sum nk Z < Sum nk M }}.
Proof.
move=> Hset nk valpha vx vy vm vz X Y M Halpha HlenX HlenY HlenM Hnz HXM HYM.
rewrite /mont_mul_strict.

apply while.hoare_seq with ((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)) **
(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 /\ [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) **
(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_y [r_z [r_m_ [r_k [r_alpha [mem Hmultiplier]]]]]]]].

do 2 (rewrite !assert_m.con_assoc_equiv assert_m.con_com_equiv in mem).
rewrite !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 mem.
rewrite assert_m.con_com_equiv !assert_m.con_assoc_equiv.
move: mem; apply monotony => // h' mem.
rewrite decompose_last_equiv HlenM in mem.
rewrite !assert_m.con_assoc_equiv assert_m.con_com_equiv !assert_m.con_assoc_equiv in mem.
by move: mem; apply monotony => // h'' mem.

apply frame_rule.
- eapply mont_mul_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.
- move=> ?; by Inde_mult.

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 /\ [y]_s = vy /\ [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 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) /\
    (var_e x |--> X ** var_e y |--> Y ** 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_y [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.
move: {Hmem Hmem2}(assert_m.con_cons _ _ _ _ _ Hdisj Hmem Hmem2) => Hmem.
by assoc_comm Hmem.

apply pull_out_and => len_Z.

apply while.hoare_ifte.

apply hoare_prop_m.hoare_stren with (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 /\
    Zbeta nk * Sum (S nk) (Z ++ zero32 :: nil) =m Sum nk X * Sum nk Y {{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 y |--> Y ** 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_y [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.
rewrite HbeqC0 in Sum_Z1 Sum_Z2.
by repeat (split; trivial).

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 /\ [y]_s = vy /\ [alpha]_s = valpha /\
    Zbeta nk * Sum (S nk) (Z ++ zero32 :: nil) =m Sum nk X * Sum nk Y {{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 y |--> Y **
    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_y [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 ** var_e y |--> Y **
  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.
  assoc_comm Hmem; trivial.
case: Hmem => [h1 [h2 [Hdisj [Hunion [H1 H2]]]]].
exists h1, h2; repeat (split; trivial).

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 /\ [y]_s = vy /\ [alpha]_s = valpha /\
    (Zbeta nk * Sum (S nk) (Z ++ zero32 :: nil) =m Sum nk X * Sum nk Y {{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 y |--> Y **
    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 Z >= Sum nk M /\ h = heap.emp) **
  (fun s h => [z]_s = vz /\ [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\
    [x]_s = vx /\ [y]_s = vy /\ [alpha]_s = valpha /\
    (Zbeta nk * Sum (S nk) (Z ++ zero32 :: nil) =m Sum nk X * Sum nk Y {{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 ** var_e y |--> Y **
      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_y [r_alpha [Sum_Z1 [Sum_Z2 r_t]]]]] Hmem2]]]]]] Hbeqint0].

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

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 /\ [y]_s = vy /\ [alpha]_s = valpha /\
  (Zbeta nk * Sum (S nk) (Z ++ zero32 :: nil) =m Sum nk X * Sum nk Y {{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 y |--> Y ** 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_y [r_alpha [HSumZ1 [HSumZ2 [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 /\ [y]_s = vy /\ [alpha]_s = valpha /\
  (Zbeta nk * Sum (S nk) (Z ++ zero32 :: nil) =m Sum nk X * Sum nk Y {{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 y |--> Y **
    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' [HlenZ' [r_z [r_m [r_k [HC [Hmem1 HSumSub]]]]]]] [r_x [r_y [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 HlenZ' 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 /= plus_comm len_Z.
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 apply Zge_le.
- 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_y [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 /= plus_comm len_Z.
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.

apply hoare_addiu with (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 /\
  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 /\
  u2Z [C]_s <> u2Z (zero32) /\
  (var_e x |--> X ** var_e y |--> Y ** 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_y [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 /\ [y]_s = vy /\ [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 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 /\ u2Z [C]_s <> u2Z (zero32) /\
  (var_e x |--> X ** var_e y |--> Y ** 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_y [r_z [r_m [r_k [r_alpha [Sum_Z1 [Sum_Z2 [r_t [r_C mem]]]]]]]]]].

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 Z_S in Hnz.
  rewrite inj_mult r_z -Zbeta1_Zpower2 [Z_of_nat 4]/=; 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 assert_m.con_com_equiv !assert_m.con_assoc_equiv in mem.
move: mem; apply monotony => // ht.
by apply mapsto_ext.

apply currying => h' H'.

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

apply hoare_addiu with (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 /\
  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 /\
  u2Z [C]_s <> u2Z (zero32) /\ u2Z [ext]_s = Z_of_nat (S nk) /\
  (var_e x |--> X ** var_e y |--> Y ** 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_y [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 -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) (Z ++ Cint32 :: nil) >= Sum (S nk) (M ++ zero32 :: nil) /\ [C]_s = Cint32) /\ h = heap.emp) **
(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 /\
  (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 /\ u2Z [ext]_s = Z_of_nat (S nk) /\
  ((var_e x |--> X ** var_e y |--> Y ** 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_y [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 /= len_Z plus_comm.
rewrite Sum_cut_last; last by rewrite app_length /= HlenM 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; move: (min_u2Z [C]_s) => ?; omega.
apply Zle_ge.
apply Zle_trans with (Sum nk Z + Zbeta nk * 1); first by omega.
apply Zplus_le_compat_l, Zmult_le_compat_l; first by omega.
by apply Zbeta_0'.

apply pull_out_exists_con => Cint32.

apply hoare_prop_m.hoare_stren with (
  (fun s h => Sum (S nk) (Z ++ Cint32 :: nil) >= Sum (S nk) (M ++ zero32 :: nil) /\ h = heap.emp) **
  (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 /\ [C]_s = Cint32 /\
    (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 /\ u2Z [ext]_s = Z_of_nat (S nk) /\
    (var_e x |--> X ** var_e y |--> Y ** 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_y [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 /\ [y]_s = vy /\
    u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
    (Zbeta nk * Sum (S nk) (Z++Cint32::nil) =m Sum nk X * Sum nk Y {{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 ** var_e y |--> Y) s h)).

move=> s h [r_x [r_y [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 ** var_e y |--> Y)) 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=> //).
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 /\ [y]_s = vy /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (Zbeta nk * Sum (S nk) (Z ++ Cint32 :: nil) =m Sum nk X * Sum nk Y {{ 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 ** var_e y |--> Y) 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_y [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 -/(1 + nk)%nat plus_comm minus_plus.
  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; trivial).

rewrite HZ'Z'' in Sum_Z'.
rewrite (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'' in Sum_Z'.
rewrite (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 apply Zge_le.
- by Inde_frame.
- move=> ?; by Inde_mult.
Qed.

End mont_mul_strict_triple.