Library multi_add_inplace_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 zarith_ext_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.

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

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

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

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

move=> s h [[[H [r_a [r_b [r_k mem]]]] r_j] r_t].
rewrite /wp_multu.
repeat reg_upd.
rewrite umul_0 /store.multi_null store.utoZ_multu u2Z_Z2u //.
repeat (split => //).
by rewrite r_j add_com add_0 sext_Z2u // u2Z_Z2u.
by rewrite r_t sext_Z2u // add_0 r_b.
by Assert_upd.

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

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

move=> s h [[nj [B' [H [H3 [H2 [H4 [H5 [H6 [H7 [H8 [H9 [H10 [H11 Hnth]]]]]]]]]]]]] H1];
  rewrite /= in H1. move/negPn : H1; move/Zeq_boolP => H1.
exists B'; 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 H7 H5 in H1; by apply Z_of_nat_inj.

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

move=> s h [ [nj [B' [HlenC [Hone [r_a [r_b [r_k [mem [r_j [Hjk2 [Hm [r_t [Hinv Hnth]]]]]]]]]]]]] Hjk];
  rewrite /= r_j r_k in Hjk.
  move/Zeq_boolP : Hjk. move/Z_of_nat_inj_neq. move/(le_neq_lt _ _ Hjk2) => Hjk.
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 mem.
  move: mem; apply monotony => // h'.
  apply mapsto_ext => //.
  by rewrite [mult]lock /= -lock shl_Z2u inj_mult [Zpower _ _]/= r_j Zmult_comm.
- exists nj, B'; repeat reg_upd; repeat (split; trivial).
  by Assert_upd.

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

move=> s h [nj [B' [HlenC [Hone [r_a [r_b [r_k [Hmem [r_j [Hjk [Hm [r_t [Hinv [Hnth r_a0]]]]]]]]]]]]]].

exists nj, B'; 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 r_a0 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 B',
  length B' = nk /\ [one]_s = one32 /\ [a]_s = va /\
  [b]_s = vb /\ u2Z [k]_s = Z_of_nat nk /\
  (var_e a |--> A ** var_e b |--> B') s h /\
  u2Z [j]_s = Z_of_nat nj /\ (nj < nk)%nat /\
  store.utoZ s <= 2 ^^ 32 /\ u2Z [t]_s = u2Z vb + 4 * Z_of_nat nj /\
  Sum nj B' + store.utoZ s * Zbeta nj = Sum (S nj) A + Sum nj B /\
  skipn nj B = skipn nj B' /\ [a0]_s = nth nj B zero32).

move=> s h [nj [B' [HlenC [Hone [Hrega [Hregb [Hregk [Hmem [Hregj [Hjk [Hm [Hregt [Hinv Hnth]]]]]]]]]]]]].
exists (nth nj B' zero32); split.
- Decompose_32 B' nj B'1 B'2 HlenB1 HB'; last by rewrite HlenC.
  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 Hregj [Zmult]lock /= -lock Zmult_comm.
- exists nj, B'; repeat reg_upd; repeat (split; trivial).
  + by Assert_upd.
  + rewrite (skipn_S zero32) in Hnth; last by rewrite Hb.
    symmetry in Hnth.
    rewrite (skipn_S zero32) in Hnth; last by rewrite HlenC.
    by case: Hnth.

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

move=> s h [nj [B' [HlenC [Hone [r_a [r_b [r_k [Hmem [r_j [Hjk [Hm [r_t [Hinv [Hnth r_a0]]]]]]]]]]]]]].

exists nj, B'; 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 r_a0 (Sum_remove_last _ B) -/zero32 -/(Zbeta nj) Zplus_assoc -Hinv u2Z_zext /=; ring.

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

move=> s h [nj [B' [HlenC [Hone [Hrega [Hregb [Hregk [Hmem [Hregj [Hjk [Hm [Hregt [Hinv Hnth]]]]]]]]]]]]].

exists nj, B'; repeat reg_upd; repeat (split; trivial).
- by Assert_upd.
- rewrite store.mflhxu_upd store.utoZ_upd.
  apply store.mflhxu_kbeta1_utoZ.
  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 B',
  length B' = nk /\ [one]_s = one32 /\ [a]_s = va /\
  [b]_s = vb /\ u2Z [k]_s = Z_of_nat nk /\
  (var_e a |--> A ** var_e b |--> B') s h /\
  nth nj B' zero32 = [a0]_s /\ u2Z [j]_s = Z_of_nat nj /\ (nj < nk)%nat /\
  store.utoZ s < 2 /\ u2Z [t]_s = u2Z vb + 4 * Z_of_nat nj /\
  Sum (S nj) B' + store.utoZ s * Zbeta (S nj) = Sum (S nj) A + Sum (S nj) B /\
  skipn (S nj) B = skipn (S nj) B').

move=> s h [nj [B' [HlenC [Hone [r_a [r_b [r_k [Hmem [r_j [Hjk [Hm [r_t [Hinv Hnth]]]]]]]]]]]]].

have Htmp : [ add_e (var_e b) (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 r_b r_t.
  rewrite inj_mult -Zbeta1_Zpower2 r_b; simpl Z_of_nat.
  eapply Zlt_trans; last by apply Hnb.
  apply Zplus_lt_compat_l, Zmult_lt_compat_l => //.
  by apply inj_lt.

Decompose_32 B' nj B'1 B'2 HlenB1 HB'; last by rewrite HlenC.

rewrite HB' assert_m.con_com_equiv (decompose_equiv _ _ _ _ _ HlenB1) !assert_m.con_assoc_equiv
  assert_m.con_com_equiv !assert_m.con_assoc_equiv in Hmem.
exists (int_e (nth nj B' zero32)).
move: Hmem; apply monotony => ht.
by apply mapsto_ext.
apply currying => h' H'; simpl app in H'.
exists nj, (update_list B' nj [a0]_s).
repeat (split; trivial).
by apply len_update_list.
rewrite HB' update_list_app HlenB1 // -minus_n_n /= (_ : [a0]_s :: B'2 = ([a0]_s ::nil) ++ B'2) //
  (decompose_equiv _ _ _ _ _ HlenB1).
assoc_comm H'.
by move: H'; apply mapsto_ext.

by rewrite nth_update_list // HlenC.

rewrite Sum_remove_last -/(Zbeta nj) nth_update_list; last by rewrite HlenC.
rewrite -Hinv.
have -> : Sum nj (update_list B' nj [a0]_s) = Sum nj B'.
  rewrite {1}HB' update_list_app; last by rewrite HlenB1.
  by rewrite -Sum_beyond // HB' -Sum_beyond.
ring.

rewrite skipn_update_list //.
rewrite (skipn_S zero32) in Hnth; last by rewrite Hb.
symmetry in Hnth. rewrite (skipn_S zero32) in Hnth; last by rewrite HlenC.
by case: Hnth.

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

move=> s h [nj [B' [HlenC [Hone [r_a [r_b [r_k [Hmem [r_ctmp [r_j [Hjk [Hm [r_t [Hinv Hnth]]]]]]]]]]]]]].

exists nj, B'; repeat reg_upd; repeat (split; trivial).
by Assert_upd.
rewrite u2Z_add // r_t sext_Z2u // u2Z_Z2u //.
- ring.
- rewrite -Zbeta1_Zpower2; eapply Zle_lt_trans; last by apply Hnb.
  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 [B' [len_C [Hone [r_a [r_b [r_k [Hmem [r_j [Hjk [Hm [r_t [Hinv Hnth]]]]]]]]]]]]].
exists (S nj), B'; rewrite Z_S.
repeat reg_upd; repeat (split; trivial).
- by Assert_upd.
- rewrite u2Z_add // sext_Z2u // r_j u2Z_Z2u // -Zbeta1_Zpower2.
  eapply Zle_lt_trans; last by apply Hnb.
  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; auto.
- apply Zle_minus_1 in Hm; exact Hm.
Qed.