Library multi_add_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_tactics mips_contrib mapstos.
Require Import multi_add_prg.

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

Lemma multi_add_triple : forall k one a b c t j atmp,
  nodup(k, one, a, b, c, t, j, atmp, r0) ->
 forall nk va vb vc, u2Z vc + 4 * Z_of_nat nk < Zbeta 1 ->
 forall A B, length A = nk -> length B = nk ->
 {{ fun s h => exists C, length C = nk /\ [one]_s = one32 /\
    [a]_s = va /\ [b]_s = vb /\ [c]_s = vc /\
    u2Z [k]_s = Z_of_nat nk /\
    (var_e a |--> A ** var_e b |--> B ** var_e c |--> C) s h }}
 multi_add k one a b c t j atmp
 {{ fun s h => exists C, length C = nk /\ (var_e a |--> A ** var_e b |--> B ** var_e c |--> C) s h /\
    u2Z (store.lo s) <= 1 /\
    Sum nk C + u2Z (store.lo s) * Zbeta nk = Sum nk A + Sum nk B }}.
Proof.
move=> k one a b c t j atmp Hset nk va vb vc Hnc A B Ha Hb; rewrite /multi_add.

NextAddiu.
move=> s h [C [H [H2 [H1 [H3 [H4 [H5 H6]]]]]]]; rewrite /wp_addiu; repeat reg_upd.
split; last by reflexivity.
exists C; repeat (split; trivial).
by Assert_upd.

NextAddiu.
move=> s h [[C [H0 [H3 [H2 [H4 [H5 [H6 H7]]]]]]] H1].
rewrite /wp_addiu; repeat reg_upd; repeat (split; trivial).
exists C; repeat (split; trivial).
by Assert_upd.

apply hoare_multu with (fun s h => exists C,
  length C = nk /\ [one]_s = one32 /\ [a]_s = va /\
  [b]_s = vb /\ [c]_s = vc /\ u2Z [k]_s = Z_of_nat nk /\
  u2Z [j]_s = 0 /\ u2Z [t]_s = u2Z vc /\ store.multi_null s /\
  (var_e a |--> A ** var_e b |--> B ** var_e c |--> C) s h ).

move=> s h [[[C [H [H4 [H3 [H5 [H6 [H7 H10]]]]]]] H2] H1].
rewrite /wp_multu.
exists C; repeat reg_upd.
rewrite umul_0 /store.multi_null store.utoZ_multu u2Z_Z2u //.
repeat (split => //).
by rewrite H2 add_com add_0 sext_Z2u // u2Z_Z2u.
by rewrite H1 sext_Z2u // add_0 H6.
by Assert_upd.

apply hoare_prop_m.hoare_while_invariant with (fun s h => exists nj, exists C,
  length C = nk /\ [one]_s = one32 /\ [a]_s = va /\
  [b]_s = vb /\ [c]_s = vc /\ u2Z [k]_s = Z_of_nat nk /\
  (var_e a |--> A ** var_e b |--> B ** var_e c |--> C) s h /\
  u2Z [j]_s = Z_of_nat nj /\ (nj <= nk)%nat /\
  store.utoZ s <= 1 /\ u2Z [t]_s = u2Z vc + 4 * Z_of_nat nj /\
  Sum nj C + u2Z (store.lo s) * Zbeta nj = Sum nj A + Sum nj B).

move=> s h [C [len_C [r_one [r_a [r_b [r_c [r_k [r_j [r_t [Hm mem]]]]]]]]]].
exists O, C; repeat (split; trivial).
by apply le_O_n.
by rewrite Hm.
by rewrite r_t /= Zplus_0_r.
by rewrite store.multi_null_lo // u2Z_Z2u.

move=> s h [[nj [C [H [H3 [H2 [H4 [H5 [H6 [H7 [H8 [H9 [H10 [H11 H13]]]]]]]]]]]]] /=].
move/negPn; move/Zeq_boolP => H1.
exists C; repeat (split; trivial).
have : store.utoZ s < Zbeta 1 by apply Zle_lt_trans with 1.
by case/store.utoZ_lo_beta1=> _ [] _ <-.
suff : nk = nj by move ->.
rewrite H8 H6 in H1; by apply Z_of_nat_inj.

apply hoare_lwxs_back_alt'' with (fun s h => exists nj, exists C,
  length C = nk /\ [one]_s = one32 /\ [a]_s = va /\
  [b]_s = vb /\ [c]_s = vc /\ u2Z [k]_s = Z_of_nat nk /\
  (var_e a |--> A ** var_e b |--> B ** var_e c |--> C) s h /\
  u2Z [j]_s = Z_of_nat nj /\ (nj < nk)%nat /\
  store.utoZ s <= 1 /\ u2Z [t]_s = u2Z vc + 4 * Z_of_nat nj /\
  Sum nj C + u2Z (store.lo s) * Zbeta nj = Sum nj A + Sum nj B /\
  [atmp]_s = nth nj A zero32).

move=> s h [[nj [C [HlenC [Hone [Hra [Hrb [Hrc [Hrk [Hmem [Hrj [Hjk2 [Hm [Hrt Hinv]]]]]]]]]]]]] Hjk];
  rewrite /= in Hjk; move/Zeq_boolP : Hjk => Hjk.
have {Hjk}Hjk : (nj < nk)%nat.
  apply (le_neq_lt _ _ Hjk2), Z_of_nat_inj_neq; by rewrite -Hrj -Hrk.
exists (nth nj A zero32); split.
- Decompose_32 A nj A1 A2 HlenA1 HA'; last by rewrite Ha.
  rewrite HA' (decompose_equiv _ _ _ _ _ HlenA1) !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 inj_mult Hrj [Zmult]lock /= -lock Zmult_comm.
- rewrite /update_store_lwxs.
  exists nj, C; repeat reg_upd; repeat (split; trivial).
  by Assert_upd.

apply hoare_maddu with (fun s h => exists nj, exists C,
  length C = nk /\ [one]_s = one32 /\ [a]_s = va /\
  [b]_s = vb /\ [c]_s = vc /\ u2Z [k]_s = Z_of_nat nk /\
  (var_e a |--> A ** var_e b |--> B ** var_e c |--> C) s h /\
  u2Z [j]_s = Z_of_nat nj /\ (nj < nk)%nat /\
  store.utoZ s <= 2 ^^ 32 /\ u2Z [t]_s = u2Z vc + 4 * Z_of_nat nj /\
  Sum nj C + store.utoZ s * Zbeta nj = Sum (S nj) A + Sum nj B).

move=> s h [nj [C [HlenC [Hone [Hra [Hrb [Hrc [Hrk [Hmem [Hrj [Hjk [Hm [Hrt [Hinv Hratmp]]]]]]]]]]]]]].

exists nj, C; rewrite Hone umul_1; repeat reg_upd; repeat (split; trivial).
by Assert_upd.
rewrite store.utoZ_maddu.
- rewrite u2Z_zext.
  rewrite (_ : 2 ^^ 32 = 2 ^^ 32 - 1 + 1) //.
  apply Zplus_le_compat => //.
  by apply Zle_minus_1, max_u2Z.
  by apply Zle_lt_trans with 1.
- rewrite store.utoZ_maddu; last by apply Zle_lt_trans with 1.
  rewrite Sum_remove_last -/(Zbeta nj) -/zero32 (Zplus_comm (Sum nj A)) -Zplus_assoc -Hinv Hratmp u2Z_zext store.acxhi_zero; last first.
    by apply Zle_lt_trans with 1.
  ring_simplify.
  rewrite -2!Zplus_assoc; f_equal; by rewrite Zmult_comm Zplus_comm.

apply hoare_lwxs_back_alt'' with (fun s h => exists nj, exists C,
  length C = nk /\ [one]_s = one32 /\ [a]_s = va /\
  [b]_s = vb /\ [c]_s = vc /\ u2Z [k]_s = Z_of_nat nk /\
  (var_e a |--> A ** var_e b |--> B ** var_e c |--> C) s h /\
  u2Z [j]_s = Z_of_nat nj /\ (nj < nk)%nat /\
  store.utoZ s <= 2 ^^ 32 /\ u2Z [t]_s = u2Z vc + 4 * Z_of_nat nj /\
  Sum nj C + store.utoZ s * Zbeta nj = Sum (S nj) A + Sum nj B /\
  [atmp]_s = nth nj B zero32).

move=> s h [nj [C [HlenC [Hone [Hra [Hrb [Hrc [Hrk [Hmem [Hrj [Hjk [Hm [Hrt Hinv]]]]]]]]]]]]].
exists (nth nj B zero32); split.
- Decompose_32 B nj B1 B2 HlenB1 HB'; last by rewrite Hb.
  rewrite HB' (decompose_equiv _ _ _ _ _ HlenB1) !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'.
  apply mapsto_ext => //.
  by rewrite [mult]lock /= -lock shl_Z2u inj_mult Hrj [Zmult]lock /= -lock Zmult_comm.
- rewrite /update_store_lwxs.
  exists nj, C; repeat reg_upd; repeat (split; trivial).
  by Assert_upd.

apply hoare_maddu with (fun s h => exists nj, exists C,
  length C = nk /\ [one]_s = one32 /\ [a]_s = va /\
  [b]_s = vb /\ [c]_s = vc /\ u2Z [k]_s = Z_of_nat nk /\
  (var_e a |--> A ** var_e b |--> B ** var_e c |--> C) s h /\
  u2Z [j]_s = Z_of_nat nj /\ (nj < nk)%nat /\
  store.utoZ s <= 2 ^^ 33 - 1 /\ u2Z [t]_s = u2Z vc + 4 * Z_of_nat nj /\
  Sum nj C + store.utoZ s * Zbeta nj = Sum (S nj) A + Sum (S nj) B).

move=> s h [nj [C [HlenC [Hone [Hra [Hrb [Hrc [Hrk [Hmem [Hrj [Hjk [Hm [Hrt [Hinv Hratmp]]]]]]]]]]]]]].

exists nj, C; rewrite Hone umul_1; repeat reg_upd; repeat (split; trivial).
by Assert_upd.
rewrite store.utoZ_maddu.
rewrite u2Z_zext (_ : 2 ^^ 33 - 1 = 2 ^^ 32 - 1 + 2 ^^ 32) //.
apply Zplus_le_compat => //.
by apply Zle_minus_1, max_u2Z.
eapply Zle_lt_trans; [by apply Hm | done].
rewrite store.utoZ_maddu; last first.
  eapply Zle_lt_trans; [by apply Hm | done].
rewrite Hratmp (Sum_remove_last _ B) -/zero32 -/(Zbeta nj) Zplus_assoc -Hinv u2Z_zext /=; ring.

apply hoare_mflhxu with (fun s h => exists nj, exists C,
  length C = nk /\ [one]_s = one32 /\ [a]_s = va /\
  [b]_s = vb /\ [c]_s = vc /\ u2Z [k]_s = Z_of_nat nk /\
  (var_e a |--> A ** var_e b |--> B ** var_e c |--> C) s h /\
  u2Z [j]_s = Z_of_nat nj /\ (nj < nk)%nat /\
  store.utoZ s < 2 /\ u2Z [t]_s = u2Z vc + 4 * Z_of_nat nj /\
  u2Z [atmp]_s * Zbeta nj + Sum nj C + store.utoZ s * Zbeta (S nj) = Sum (S nj) A + Sum (S nj) B).

move=> s h [nj [C [HlenC [Hone [Hra [Hrb [Hrc [Hrk [Hmem [Hrj [Hjk [Hm [Hrt Hinv]]]]]]]]]]]]].

exists nj, C; repeat reg_upd; repeat (split; trivial).
- by Assert_upd.
- rewrite store.mflhxu_upd store.utoZ_upd.
  apply store.mflhxu_kbeta1_utoZ.
  rewrite (_ : Zbeta 1 * 2 = 2 ^^ 33) //.
  eapply Zle_lt_trans; [by apply Hm | done].
- rewrite -Hinv (store.mflhxu_utoZ s) Zbeta_S store.mflhxu_upd // store.utoZ_upd; ring.

apply hoare_sw_back'' with (fun s h => exists nj, exists C,
  length C = nk /\ [one]_s = one32 /\ [a]_s = va /\
  [b]_s = vb /\ [c]_s = vc /\ u2Z [k]_s = Z_of_nat nk /\
  (var_e a |--> A ** var_e b |--> B ** var_e c |--> C) s h /\
  nth nj C zero32 = [atmp]_s /\
  u2Z [j]_s = Z_of_nat nj /\ (nj < nk)%nat /\
  store.utoZ s < 2 /\ u2Z [t]_s = u2Z vc + 4 * Z_of_nat nj /\
  Sum (S nj) C + store.utoZ s * Zbeta (S nj) = Sum (S nj) A + Sum (S nj) B).

move=> s h [nj [C [HlenC [Hone [Hra [Hrb [Hrc [Hrk [Hmem [Hrj [Hjk [Hm [Hrt Hinv]]]]]]]]]]]]].

have Htmp : [ add_e (var_e c) (int_e (Z2u 32 (Z_of_nat (4 * nj)))) ]e_s =
            [ add_e (var_e t) (int_e (sext 16 zero16)) ]e_ s.
  rewrite [mult]lock /= -lock sext_0 // add_0.
  apply u2Z_inj.
  rewrite u2Z_add_Z_of_nat.
  by rewrite inj_mult Hrc Hrt.
  rewrite inj_mult -Zbeta1_Zpower2 Hrc; simpl Z_of_nat.
  eapply Zlt_trans; last by apply Hnc.
  apply Zplus_lt_compat_l, Zmult_lt_compat_l => //.
  by apply inj_lt.

Decompose_32 C nj C1 C2 HlenC1 HC'; last by rewrite HlenC.
rewrite HC' assert_m.con_com_equiv (decompose_equiv _ _ _ _ _ HlenC1) !assert_m.con_assoc_equiv
  assert_m.con_com_equiv !assert_m.con_assoc_equiv in Hmem.
exists (int_e (nth nj C zero32)).
move: Hmem; apply monotony => ht.
by apply mapsto_ext.
apply currying => h' H'; simpl app in H'.
exists nj, (update_list C nj [atmp]_s).
repeat (split; trivial).
by apply len_update_list.
rewrite HC' update_list_app HlenC1 // -minus_n_n /= (decompose_equiv _ _ _ _ _ HlenC1).
assoc_comm H'.
move: H'; by apply mapsto_ext.

rewrite nth_update_list // HC' app_length /= - plus_Snm_nSm HlenC1; by apply lt_plus_trans, lt_n_Sn.

rewrite Sum_remove_last -/(Zbeta nj) nth_update_list; last by rewrite HlenC //.
rewrite -Hinv.
have -> : Sum nj (update_list C nj [atmp]_s) = Sum nj C.
  rewrite {1}HC' update_list_app; last by rewrite HlenC1 //.
  by rewrite -Sum_beyond // HC' -Sum_beyond.
ring.

apply hoare_addiu with (fun s h => exists nj, exists C,
  length C = nk /\ [one]_s = one32 /\ [a]_s = va /\
  [b]_s = vb /\ [c]_s = vc /\ u2Z [k]_s = Z_of_nat nk /\
  (var_e a |--> A ** var_e b |--> B ** var_e c |--> C) s h /\
  u2Z [j]_s = Z_of_nat nj /\ (S nj <= nk)%nat /\
  store.utoZ s < 2 /\ u2Z [t]_s = u2Z vc + 4 * (Z_of_nat nj + 1) /\
  Sum (S nj) C + u2Z (store.lo s) * Zbeta (S nj) = Sum (S nj) A + Sum (S nj) B).

move=> s h [nj [C [HlenC [Hone [Hra [Hrb [Hrc [Hrk [Hmem [Hratmp [Hrj [Hjk [Hm [Hrt Hinv]]]]]]]]]]]]]].

exists nj, C; repeat reg_upd; repeat (split; trivial).
- by Assert_upd.
- rewrite u2Z_add // Hrt sext_Z2u // u2Z_Z2u //.
  + ring.
  + rewrite -Zbeta1_Zpower2; eapply Zle_lt_trans; last by apply Hnc.
    rewrite -Zplus_assoc -{2}(Zmult_1_r 4) -Zmult_plus_distr_r.
    apply Zplus_le_compat_l, Zmult_le_compat_l => //.
    rewrite -Z_S; by apply inj_le.
    rewrite store.acxhi_zero // in Hinv.
    by apply Zlt_trans with 2.

apply hoare_addiu'.
move=> s h [nj [C [HlenC [Hone [Hra [Hrb [Hrc [Hrk [Hmem [Hrj [Hjk [Hm [Hrt Hinv]]]]]]]]]]]]].

exists (S nj), C; repeat reg_upd.
rewrite Z_S.
repeat (split; trivial).
- by Assert_upd.
- rewrite u2Z_add // sext_Z2u // Hrj u2Z_Z2u // -Zbeta1_Zpower2.
  eapply Zle_lt_trans; last by apply Hnc.
  apply Zle_plus_trans; first by apply min_u2Z.
  rewrite -Z_S (_ : 4 = Z_of_nat 4) // -inj_mult.
  apply inj_le, le_trans with nk => //.
  by apply scale_le; repeat constructor.
- apply Zle_minus_1 in Hm; exact Hm.
Qed.