Library mont_mul_strict_init_triple

Require Import ssreflect ssrbool.
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 multi_zero_prg mont_mul_strict_prg.
Require Import multi_zero_triple mont_mul_strict_triple.

Local Open Scope machine_int_scope.
Local Open Scope eqmod_scope.
Local Open Scope heap_scope.
Local Open Scope nodup_scope.
Local Open Scope mips_expr_scope.
Import expr_m.
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_init.

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

Lemma mont_mul_strict_init_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 => 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}}
  mont_mul_strict_init 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_init.

apply pull_out_exists => 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 /\
    (((var_e x |--> X ** var_e y |--> Y) ** var_e z |--> Z ++ zero32 :: nil) ** var_e m |--> M ++ zero32 :: nil) s h)).

move=> s h [HlenZ [Hrx [Hry [Hrz [Hrm_ [Hrk [Hralpha Hmem]]]]]]].
exists heap.emp, h; repeat (split => //).
by map_tac_m.Disj.
by map_tac_m.Equal.

apply pull_out_and => HlenZ.

apply hoare_prop_m.hoare_stren with
  ((fun s h => [z]_s = vz /\ u2Z [k]_s = Z_of_nat nk /\ (var_e z |--> Z) s h) **
    (fun s h => [x]_s = vx /\ [y]_s = vy /\ [m]_s = vm /\ [alpha]_s = valpha /\
      (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 **
        var_e m |--> M ++ zero32 :: nil) s h)).

move=> s h [Hrx [Hry [Hrz [Hrm_ [Hrk [Hralpha Hmem]]]]]].
rewrite decompose_last_equiv HlenZ !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.
case: Hmem => [h1 [h2 [Hdisj [Hunion [Hmem1 Hmem2]]]]].
exists h1, h2; repeat (split; trivial).
by assoc_comm Hmem2.

apply while.hoare_seq with
  ((fun s h => [z]_s = vz /\ u2Z [k]_s = Z_of_nat nk /\ (var_e z |--> rep zero32 nk) s h) **
    (fun s h => [x]_s = vx /\ [y]_s = vy /\ [m]_s = vm /\ [alpha]_s = valpha /\
      (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 **
        var_e m |--> M ++ zero32 :: nil) s h)).

apply frame_rule.
- eapply multi_zero_triple; eauto.
  + by Nodup_nodup r0.
  + rewrite Z_S in Hnz; omega.
- by Inde_frame.
- move=> ?; by Inde_mult.

apply while.hoare_seq 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 ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil) s h /\
  store.multi_null s).

apply hoare_mflhxu 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 ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil) s h /\
  store.acx s = Z2u store.acx_size 0).

move=> s h [h1 [h2 [Hdisj [Hunion [[Hrz [Hrk Hmem1]] [Hrx [Hry [Hrm_ [Hralpha Hmem2]]]]]]]]].
rewrite /wp_mflhxu.
repeat reg_upd; repeat (split; trivial).
move: {Hmem1 Hmem2}(assert_m.con_cons _ _ _ _ _ Hdisj Hmem1 Hmem2) => Hmem.
rewrite Hunion decompose_last_equiv len_rep store.upd_r0.

Assert_upd; by assoc_comm Hmem.

by apply store.acx_mflhxu_op.

apply hoare_mthi 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 ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil) s h /\
  store.acx s = Z2u store.acx_size 0 /\ store.hi s = zero32).

move=> {Z HlenZ} s h [Hrx [Hry [Hrz [Hrm_ [Hrk [Hralpha [mem Hacx]]]]]]].
rewrite /wp_mthi.
repeat reg_upd; repeat (split; trivial).
by Assert_upd.
by rewrite store.acx_mthi_op.
by rewrite store.hi_mthi_op.

apply hoare_mtlo'.

move=> {Z HlenZ} s h [[Hrx [Hry [Hrz [Hrm_ [Hrk [Hralpha [mem [Hacx Hhi]]]]]]]]].
rewrite /wp_mtlo.
repeat reg_upd; repeat (split; trivial).
by Assert_upd.
apply store.utoZ_multi_null.
by rewrite store.utoZ_def store.hi_mtlo_op store.acx_mtlo_op store.lo_mtlo_op Hacx Hhi /zero32 u2Z_Z2u // u2Z_Z2u.

by eapply mont_mul_strict_triple; eauto.
Qed.

End mont_mul_strict_init.