Library multi_mul2_triple

Require Import Arith_ext ZArith_ext Lists_ext.
Require Import ssreflect ssrbool.
Require Import machine_int multi_int.
Import MachineInt.
Require Import mips_seplog mips_tactics mips_contrib mapstos.
Require Import multi_mul2_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.

Section multi_mul2.

Variables k a i tmp prev next : reg.

Lemma multi_mul2_triple : nodup(k, a, i, tmp, prev, next, r0) ->
forall nk va, u2Z va + 4 * Z_of_nat nk < Zbeta 1 ->
forall A, length A = nk ->
  {{ fun s h => [a]_s = va /\ u2Z [k]_s = Z_of_nat nk /\ (var_e a |--> A) s h }}
  multi_mul2 k a i tmp prev next
  {{ fun s h => exists A', length A' = nk /\ [a]_s = va /\ u2Z [k]_s = Z_of_nat nk /\
     (var_e a |--> A') s h /\ Sum nk A' + u2Z [prev]_s * 2 ^^ (nk * 32) = 2 * Sum nk A }}.
Proof.
move=> Hset nk va Hna A HA; rewrite /multi_mul2.

apply hoare_addiu with (fun s h => [a]_s = va /\ u2Z [k]_s = Z_of_nat nk /\
  u2Z [i]_s = 0 /\ (var_e a |--> A) s h).

move=> s h [Hra [Hri Hmem]]; rewrite /wp_addiu.
repeat reg_upd; repeat (split; trivial).
by rewrite sext_0 add_0 u2Z_Z2u.
by Assert_upd.

apply hoare_addiu with (fun s h => [a]_s = va /\ u2Z [k]_s = Z_of_nat nk /\
  u2Z [i]_s = 0 /\ [prev]_s = zero32 /\ (var_e a |--> A) s h).

move=> s h [Hra [Hri [Hrk Hmem]]]; rewrite /wp_addiu.
repeat reg_upd; repeat (split; trivial).
by rewrite sext_0 add_0.
by Assert_upd.

apply hoare_prop_m.hoare_while_invariant with (fun s h => exists A', exists ni, length A' = nk /\
  [a ]_ s = va /\ u2Z [k]_s = Z_of_nat nk /\
  u2Z [i ]_ s = Z_of_nat ni /\
  ([prev]_s = zero32 \/ [prev]_s = one32) /\
  (ni <= nk)%nat /\
  (var_e a |--> A') s h /\
  skipn ni A' = skipn ni A /\
  Sum ni (firstn ni A') + u2Z [prev]_s * 2 ^^ (ni * 32) = 2 * Sum ni (firstn ni A)).

move=> s h [Hra [Hrk [Hri [Hrprev Hmem]]]].
exists A, O; repeat (split; trivial).
by rewrite Hrprev; left.
by apply le_0_n.
by rewrite /= Hrprev u2Z_Z2u.

move=> s h [[A' [ni [HlenA' [Hra [Hrk [Hri [Hprev [Hik [Hmem [Hinv1 Hinv2]]]]]]]]]] Hri'].
rewrite /= in Hri'. move/negPn : Hri'; move/Zeq_boolP => Hri'.
have {Hri'} ? : ni = nk by rewrite /= Hrk Hri in Hri'; apply Z_of_nat_inj.
subst ni.
rewrite firstn_all // in Hinv2; last by rewrite HlenA'.
rewrite firstn_all // in Hinv2; last by rewrite HA.
by exists A'.

apply hoare_lwxs_back_alt'' with (fun s h => exists A', exists ni, length A' = nk /\
  [a ]_ s = va /\ u2Z [k]_s = Z_of_nat nk /\
  u2Z [i ]_ s = Z_of_nat ni /\
  ([prev]_s = zero32 \/ [prev]_s = one32) /\
  (ni < nk)%nat /\
  (var_e a |--> A') s h /\
  skipn ni A' = skipn ni A /\
  Sum ni (firstn ni A') + u2Z [prev ]_ s * 2 ^^ (ni * 32) = 2 * Sum ni (firstn ni A) /\
  [tmp]_s = nth ni A' zero32).

move=> s h [[A' [ni [HlenA' [Hra [Hrk [Hri [Hprev [Hik [Hmem [Hinv1 Hinv2]]]]]]]]]] Hik'].
rewrite /= in Hik'; move/Zeq_boolP : Hik' => Hik'.
have {Hik'}Hik' : (ni < nk)%nat.
  apply le_neq_lt; first by exact Hik.
  rewrite Hrk Hri in Hik'; contradict Hik'; by rewrite Hik'.
exists (nth ni A' zero32); split.
Decompose_32 A' ni A1 A2 HlenA1 HA'; last by rewrite HlenA'.
rewrite HA' (decompose_equiv _ _ _ _ _ HlenA1) !con_assoc_equiv con_com_equiv !con_assoc_equiv in Hmem.
move: Hmem; apply monotony => // h'.
apply mapsto_ext => //.
by rewrite [mult]lock /= -lock shl_Z2u inj_mult Hri [Zmult]lock /= -lock Zmult_comm.

rewrite /update_store_lwxs.
exists A', ni; repeat reg_upd; repeat (split; trivial).
by Assert_upd.

apply hoare_srl with (fun s h => exists A', exists ni, length A' = nk /\
  [a ]_ s = va /\ u2Z [k]_s = Z_of_nat nk /\
  u2Z [i ]_ s = Z_of_nat ni /\
  ([prev]_s = zero32 \/ [prev]_s = one32) /\
  (ni < nk)%nat /\
  (var_e a |--> A') s h /\
  skipn ni A' = skipn ni A /\
  Sum ni (firstn ni A') + u2Z ([prev ]_ s) * 2 ^^ (ni * 32) = 2 * Sum ni (firstn ni A) /\
  [tmp]_s = nth ni A' zero32 /\
  [next]_s = (nth ni A' zero32) [.>>] 31).

move=> s h [A' [ni [HlenA' [Hra [Hrk [Hri [Hprev [Hik [Hmem [Hinv1 [Hinv2 Htmp]]]]]]]]]]].
exists A', ni; repeat reg_upd; repeat (split; trivial).
by Assert_upd.
by rewrite Htmp u2Z_Z2u.

apply hoare_sll with (fun s h => exists A', exists ni, length A' = nk /\
  [a ]_ s = va /\ u2Z [k]_s = Z_of_nat nk /\
  u2Z [i ]_ s = Z_of_nat ni /\
  ([prev]_s = zero32 \/ [prev]_s = one32) /\
  (ni < nk)%nat /\
  (var_e a |--> A') s h /\
  skipn ni A' = skipn ni A /\
  Sum ni (firstn ni A') + u2Z ([prev ]_ s) * 2 ^^ (ni * 32) = 2 * Sum ni (firstn ni A) /\
  [tmp]_s = (nth ni A' zero32) [.<<] 1 /\
  [next]_s = (nth ni A' zero32) [.>>] 31).

move=> s h [A' [ni [HlenA' [Hra [Hrk [Hri [Hprev [Hik [Hmem [Hinv1 [Hinv2 [Htmp Hnext]]]]]]]]]]]].
exists A', ni; repeat reg_upd; repeat (split; trivial).
by Assert_upd.
by rewrite Htmp u2Z_Z2u.

apply hoare_or with (fun s h => exists A', exists ni, length A' = nk /\
  [a ]_ s = va /\ u2Z [k]_s = Z_of_nat nk /\
  u2Z [i ]_ s = Z_of_nat ni /\
  ([prev]_s = zero32 \/ [prev]_s = one32) /\
  (ni < nk)%nat /\
  (var_e a |--> A') s h /\
  skipn ni A' = skipn ni A /\
  Sum ni (firstn ni A') + u2Z ([prev ]_ s) * 2 ^^ (ni * 32) = 2 * Sum ni (firstn ni A) /\
  [tmp]_s = ((nth ni A' zero32) [.<<] 1) [.|] [prev]_s /\
  [next]_s = (nth ni A' zero32) [.>>] 31).

move=> s h [A' [ni [HlenA' [Hra [Hrk [Hri [Hprev [Hik [Hmem [Hinv1 [Hinv2 [Htmp Hnext]]]]]]]]]]]].
exists A', ni; repeat reg_upd; repeat (split; trivial).
by Assert_upd.
by rewrite Htmp.

apply hoare_addiu with (fun s h => exists A', exists ni, length A' = nk /\
  [a ]_ s = va /\ u2Z [k]_s = Z_of_nat nk /\
  u2Z [i ]_ s = Z_of_nat ni /\
  ([prev]_s = zero32 \/ [prev]_s = one32) /\
  (ni < nk)%nat /\
  (var_e a |--> A') s h /\
  skipn ni A' = skipn ni A /\
  Sum ni (firstn ni A') + u2Z ([tmp]_s [.%] 1) * 2 ^^ (ni * 32) = 2 * Sum ni (firstn ni A) /\
  [tmp]_s [.>>] 1 = (nth ni A' zero32 [.<<] 1) [.>>] 1 /\
  [prev]_s = nth ni A' zero32 [.>>] 31).

move=> s h [A' [ni [HlenA' [Hra [Hrk [Hri [Hprev [Hik [Hmem [Hinv1 [Hinv2 [Htmp Hnext]]]]]]]]]]]].
rewrite /wp_addiu; exists A', ni.
repeat reg_upd; repeat (split; trivial).
- rewrite sext_0 add_0 Hnext.
  move: (shrl_lt (nth ni A' zero32) 31) => /=.
  move X : (u2Z _) => x Hx.
  have [Y|Y] : x = 0 \/ x = 1.
    move: (min_u2Z (nth ni A' zero32[.>>]31)) => Hy; omega.
  subst x.
  rewrite (_ : 0 = u2Z (Z2u 32 0)) in Y; last by rewrite u2Z_Z2u.
  apply u2Z_inj in Y.
  rewrite Y; by auto.
  subst x.
  rewrite (_ : 1 = u2Z (Z2u 32 1)) in Y; last by rewrite u2Z_Z2u.
  move/u2Z_inj : Y => ->; by right.
- by Assert_upd.
- rewrite Htmp.
  have X : u2Z (((nth ni A' zero32[.<<]1) [.|] [prev ]_ s) [.%] 1) = u2Z ([prev ]_ s).
    rewrite rem_distr_or shl_rem_m; last by repeat constructor.
    rewrite int_or_comm int_or_0 u2Z_rem' //.
    case: Hprev => ->; by rewrite u2Z_Z2u.
  by rewrite X.
- rewrite Htmp shrl_distr_or (shrl_overflow ([prev]_s) 1).
  by rewrite int_or_0.
  by case: Hprev => ->; rewrite u2Z_Z2u.
- by rewrite sext_Z2u // add_0.

apply hoare_sll with (fun s h => exists A', exists ni, length A' = nk /\
  [a ]_ s = va /\ u2Z [k]_s = Z_of_nat nk /\
  u2Z [i ]_ s = Z_of_nat ni /\
  ([prev]_s = zero32 \/ [prev]_s = one32) /\
  (ni < nk)%nat /\
  (var_e a |--> A') s h /\
  skipn ni A' = skipn ni A /\
  Sum (ni) (firstn ni A') + u2Z ([tmp]_s [.%] 1) * 2 ^^ (ni * 32) = 2 * Sum ni (firstn ni A) /\
  [tmp]_s [.>>] 1 = ((nth ni A' zero32) [.<<] 1) [.>>] 1 /\
  [prev]_s = (nth ni A' zero32) [.>>] 31 /\
  u2Z [next]_s = 4 * Z_of_nat ni).

move=> s h [A' [ni [HlenA' [Hra [Hrk [Hri [Hprev [Hik [Hmem [Hinv1 [Hinv2 [Htmp Hnext]]]]]]]]]]]].
exists A', ni; repeat reg_upd; repeat (split; trivial).
by Assert_upd.
rewrite u2Z_Z2u // (_ : Zabs_nat 2 = 2%nat) // (u2Z_shl 2 _ 30) //.
- rewrite Hri [Zpower _ _]/=; ring.
- rewrite (_ : Zbeta 1 = 4 * 2 ^^ 30) in Hna; last by rewrite Zbeta1_Zpower2.
  move: (min_u2Z va) => ?; omega.

apply hoare_addu with (fun s h => exists A', exists ni, length A' = nk /\
  [a ]_ s = va /\ u2Z [k]_s = Z_of_nat nk /\
  u2Z [i ]_ s = Z_of_nat ni /\
  ([prev]_s = zero32 \/ [prev]_s = one32) /\
  (ni < nk)%nat /\
  (var_e a |--> A') s h /\
  skipn ni A' = skipn ni A /\
  Sum ni (firstn ni A') + u2Z ([tmp]_s [.%] 1) * 2 ^^ (ni * 32) = 2 * Sum ni (firstn ni A) /\
  [tmp]_s [.>>] 1 = ((nth ni A' zero32) [.<<] 1) [.>>] 1 /\
  [prev]_s = nth ni A' zero32 [.>>] 31 /\
  u2Z [next]_s = u2Z va + 4 * Z_of_nat ni).

move=> s h [A' [ni [HlenA' [Hra [Hrk [Hri [Hprev [Hik [Hmem [Hinv1 [Hinv2 [Htmp [Hprev2 Hnext]]]]]]]]]]]]].
exists A', ni; repeat reg_upd; repeat (split; trivial).
- by Assert_upd.
- rewrite u2Z_add.
  + rewrite Hra Hnext; ring.
  + rewrite (_ : Zbeta 1 = 4 * 2 ^^ 30) in Hna; last by rewrite Zbeta1_Zpower2.
    rewrite (_ : 2 ^^ 32 = 4 * 2 ^^ 30) // Hnext Hra; omega.

apply hoare_sw_back'' with (fun s h => exists A', exists ni, length A' = nk /\
  [a ]_ s = va /\ u2Z [k]_s = Z_of_nat nk /\
  u2Z [i ]_ s = Z_of_nat ni /\
  ([prev]_s = zero32 \/ [prev]_s = one32) /\
  (ni < nk)%nat /\
  (var_e a |--> A') s h /\
  skipn (S ni) A' = skipn (S ni) A /\
  Sum (S ni) (firstn (S ni) A') + u2Z ([prev]_s) * 2 ^^ ((S ni) * 32) = 2 * Sum (S ni) (firstn (S ni) A) /\
  u2Z [next]_s = u2Z va + 4 * Z_of_nat ni).

move=> s h [A' [ni [HlenA' [Hra [Hrk [Hri [Hprev [Hik [Hmem [Hinv1 [Hinv2 [Hrtmp [Hprev2 Hrnext]]]]]]]]]]]]].

have Htmp : [ add_e (var_e next) (int_e (sext 16 zero16)) ]e_ s =
    [ add_e (var_e a) (int_e (Z2u 32 (Z_of_nat (4 * ni)))) ]e_ s.
  rewrite [mult]lock /= -lock sext_0 // add_0.
  apply u2Z_inj.
  rewrite u2Z_add_Z_of_nat.
  rewrite inj_mult Hra Hrnext //; ring.
  rewrite inj_mult -Zbeta1_Zpower2 Hra; simpl Z_of_nat; omega.

Decompose_32 A' ni A'1 A'2 HlenA1 HA'; last by rewrite HlenA'.
rewrite HA' (decompose_equiv _ _ _ _ _ HlenA1) !con_assoc_equiv con_com_equiv !con_assoc_equiv in Hmem.
exists (int_e (nth ni A' zero32)).
move: Hmem; apply monotony => ht.
by apply mapsto_ext.
apply currying => h' H'; simpl app in H'.
exists (update_list A' ni [tmp]_s), ni.
repeat (split; trivial).

- by apply len_update_list.
- rewrite HA' update_list_app HlenA1 // -minus_n_n /= (decompose_equiv _ _ _ _ _ HlenA1).
  assoc_comm H'.
  by move: H'; apply mapsto_ext.
- by rewrite skipn_update_list // !skipn_tail Hinv1.
- rewrite (firstn_S zero32); last by rewrite (len_update_list nk).
  rewrite (Sum_cut ni (firstn ni (update_list A' ni [tmp ]_ s)) _ (S ni) _ _ _ (refl_equal _)) //; last 2 first.
    apply len_firstn with nk => //; by [apply len_update_list | apply lt_le_weak].
    rewrite app_length /= plus_comm /=; f_equal.
    apply len_firstn with nk => //; by [apply len_update_list | apply lt_le_weak].
  rewrite minus_Sn_n [Sum 1 _]/= nth_update_list; last by rewrite HlenA'.
  rewrite firstn_update_list (firstn_S zero32); last by rewrite HA.
  rewrite (Sum_cut ni (firstn ni A) _ (S ni) _ _ _ (refl_equal _)) //; last 2 first.
    apply len_firstn with nk => //; by apply lt_le_weak.
    rewrite app_length /= plus_comm /=; f_equal.
    apply len_firstn with nk => //; by apply lt_le_weak.
  rewrite minus_Sn_n [Sum 1 _]/= Zmult_plus_distr_r -Hinv2 -!Zplus_assoc.
  f_equal.
  have X : u2Z ([tmp ]_ s) = u2Z (([tmp]_s [.%] 1)) + u2Z (([tmp]_s [.>>] 1) [.<<] 1).
    have X3 : (1 <= 32)%nat by repeat constructor.
    rewrite {1}(@or_sh_rem _ ([tmp]_s) _ X3).
    have X1 : u2Z (cast_le_plus_minus_r2 X3 (zext 31 ([tmp ]_ s[.%]1))) < 2 ^^ 1.
      rewrite u2Z_cast u2Z_zext -int_and_rem_1.
      case: (Zeven_odd_dec (u2Z ([tmp ]_ s))) => X.
      + apply int_even_and_1 in X; by rewrite X u2Z_Z2u.
      + apply int_odd_and_1 in X; by rewrite X u2Z_Z2u.
    have X2 : (([tmp ]_ s[.>>]1)[.<<]1) [.%] 1 = Z2u 1 0 by rewrite shl_rem_m.
    rewrite (@or_concat _ _ _ _ X3 X1 X2) /cast_le_plus_minus_r2 u2Z_cast u2Z_concat Zplus_comm.
    f_equal.
    by rewrite u2Z_rem' // u2Z_cast u2Z_zext.
    rewrite u2Z_shr_shrink' //.
    by rewrite shl_rem_m // u2Z_Z2u // Zminus_0_r.
  rewrite X Zmult_plus_distr_r -!Zplus_assoc.
  f_equal.
  by apply Zmult_comm.
  rewrite Hrtmp Hprev2.
  have -> : ((nth ni A' zero32 [.<<] 1) [.>>] 1) [.<<] 1 = (nth ni A' zero32[.<<]1).
    rewrite shrl_shl // shl_rem_m //.
    by repeat constructor.
  have <- : nth ni A zero32 = nth ni A' zero32.
    rewrite (skipn_S zero32) in Hinv1; last by rewrite HlenA'.
    symmetry in Hinv1.
    rewrite (skipn_S zero32) in Hinv1; last by rewrite HA.
    by case: Hinv1.
  have U : 2 * u2Z (nth ni A zero32) = u2Z (nth ni A zero32[.<<]1) + 2 ^^ 32 * u2Z (nth ni A zero32[.>>]31).
    case: (Z_lt_le_dec (u2Z (nth ni A zero32)) (2 ^^ 31)) => V.
    * by rewrite (u2Z_shl 1 _ 31) // shrl_overflow // u2Z_Z2u // Zmult_0_r Zplus_0_r Zmult_comm.
    * rewrite -(@u2Z_shrl _ (nth ni A zero32) 31) //; last by repeat constructor.
      rewrite Zmult_plus_distr_r Zplus_comm.
      f_equal.
      - by rewrite u2Z_shl_rem.
      - by rewrite Zmult_comm -Zmult_assoc Zmult_comm -Zmult_assoc.
  symmetry.
  rewrite Zmult_comm -Zmult_assoc -(Zmult_comm 2) U Zmult_plus_distr_r.
  rewrite (_ : (S ni) * 32 = ni * 32 + 32)%nat; last by omega.
  rewrite Zpower_b_is_exp; ring.

apply hoare_addiu'.
move=> s m [A' [ni [HlenA' [Hra [Hrk [Hri [Hprev [Hik [Hmem [Hinv1 [Hinv2 Hnext]]]]]]]]]]].
rewrite /wp_addiu.
exists A', (S ni).
rewrite sext_Z2u //.
repeat reg_upd; repeat (split; trivial).
- rewrite u2Z_add_Z2u //.
  + by rewrite Z_S Hri.
  + rewrite Hri -Zbeta1_Zpower2.
    move: (min_u2Z va) => ?; omega.
- by Assert_upd.
Qed.

End multi_mul2.