Library multi_div2_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_div2_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_div2_triple : forall k a i tmp prev next, 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_div2 k a i tmp prev next
  {{ fun s h => exists A', length A' = nk /\
     (var_e a |--> A') s h /\ 2 * Sum nk A' + u2Z ([prev]_s [.>>] 31) = Sum nk A }}.
Proof.
move=> k a i tmp prev next Hset nk va Hna A HA; rewrite /multi_div2.

apply hoare_addiu with (fun s h => [a]_s = va /\ u2Z [k]_s = Z_of_nat nk /\
  u2Z [i]_s = Z_of_nat nk /\ (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.
by Assert_upd.

apply hoare_addiu with (fun s h => [a]_s = va /\ u2Z [k]_s = Z_of_nat nk /\
  u2Z [i]_s = Z_of_nat nk /\ [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 = Z2u 32 (2 ^^ 31)) /\
  (ni <= nk)%nat /\
  (var_e a |--> A') s h /\
  firstn ni A' = firstn ni A /\
  2 * Sum (nk - ni) (skipn ni A') + u2Z ([prev]_s [.>>] 31) = Sum (nk - ni) (skipn ni A)).

move=> s h [Hra [Hrk [Hri [Hrprev Hmem]]]].
exists A, nk; repeat (split; trivial).
by rewrite Hrprev; left.
by rewrite -minus_n_n /= Hrprev shrl_Z2u_0 // 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 = O.
  apply Z_of_nat_inj; by rewrite -Hri Hri' /= store.get_r0 u2Z_Z2u.
subst ni.
rewrite -minus_n_O ![skipn _ _]//= in Hinv2.
exists A'; by repeat (split; trivial).

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 = Z2u 32 (2 ^^ 31)) /\
  (ni < nk)%nat /\
  (var_e a |--> A') s h /\
  firstn (S ni) A' = firstn (S ni) A /\
  2 * Sum (nk - S ni) (skipn (S ni) A') + u2Z ([prev ]_ s [.>>] 31) = Sum (nk - S ni) (skipn (S ni) A)).

move=> s h [[A' [ni [HlenA' [Hra [Hrk [Hri [Hprev [Hik [Hmem [Hinv1 Hinv2]]]]]]]]]] Hri'].
rewrite /= store.get_r0 u2Z_Z2u // in Hri'.
move/Zeq_boolP : Hri' => Hri'.
exists A', (ni - 1)%nat.
repeat reg_upd.
rewrite Hri (_ : 0 = Z_of_nat 0) // in Hri'; apply Z_of_nat_inj_neq, not_eq_sym in Hri'.
rewrite minus_Sn_m; last by apply neq_0_lt.
rewrite minus_Sn_1.
repeat (split; trivial).
- rewrite sext_Z2s // u2Z_add_Z2s //; last first.
    rewrite Hri -(Zmult_1_l (-1)) -(Zopp_eq_mult_neg_1 1) (_ : 1 = Z_of_nat 1) //.
    by apply Zle_left, inj_le, neq_0_lt.
  rewrite inj_minus1 //; by [rewrite Hri | apply neq_0_lt].
- rewrite /lt minus_Sn_m //=; by [rewrite -minus_n_O | apply neq_0_lt].
- by Assert_upd.

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 = Z2u 32 (2 ^^ 31)) /\
  (ni < nk)%nat /\
  (var_e a |--> A') s h /\
  firstn (S ni) A' = firstn (S ni) A /\
  2 * Sum (nk - S ni) (skipn (S ni) A') + u2Z ([prev ]_ s [.>>] 31) = Sum (nk - S ni) (skipn (S ni) A) /\
  [tmp]_s = nth ni A' zero32).

move=> s h [A' [ni [HlenA' [Hra [Hrk [Hri [Hprev [Hik [Hmem [Hinv1 Hinv2]]]]]]]]]].
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_andi 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 = Z2u 32 (2 ^^ 31)) /\
  (ni < nk)%nat /\
  (var_e a |--> A') s h /\
  firstn (S ni) A' = firstn (S ni) A /\
  2 * Sum (nk - S ni) (skipn (S ni) A') + u2Z ([prev ]_ s [.>>] 31)= Sum (nk - S ni) (skipn (S ni) A) /\
  [tmp]_s = nth ni A' zero32 /\
  [next]_s = (nth ni A' zero32) [.&] one32).

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 zext_Z2u.

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 = Z2u 32 (2 ^^ 31)) /\
  (ni < nk)%nat /\
  (var_e a |--> A') s h /\
  firstn (S ni) A' = firstn (S ni) A /\
  2 * Sum (nk - S ni) (skipn (S ni) A') + u2Z ([prev ]_ s [.>>] 31) = Sum (nk - S ni) (skipn (S ni) A) /\
  [tmp]_s = (nth ni A' zero32) [.>>] 1 /\
  [next]_s = (nth ni A' zero32) [.&] one32).

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 = Z2u 32 (2 ^^ 31)) /\
  (ni < nk)%nat /\
  (var_e a |--> A') s h /\
  firstn (S ni) A' = firstn (S ni) A /\
  2 * Sum (nk - S ni) (skipn (S ni) A') + u2Z ([prev ]_ s [.>>] 31) = Sum (nk - S ni) (skipn (S ni) A) /\
  [tmp]_s = ((nth ni A' zero32) [.>>] 1) [.|] [prev]_s /\
  [next]_s = (nth ni A' zero32) [.&] one32).

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 /\
  firstn (S ni) A' = firstn (S ni) A /\
  2 ^^ 33 * Sum (nk - S ni) (skipn (S ni) A') + 2 * u2Z ([tmp]_s) + u2Z ([prev ]_ s) = Sum (nk - ni) (skipn ni A) /\
  [tmp]_s [.%] 31 = ((nth ni A' zero32) [.>>] 1) [.%] 31 /\
  [next]_s = (nth ni A' zero32) [.&] one32).

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.
  case: (Zeven_odd_dec (u2Z (nth ni A' zero32))).
  + move/int_even_and_1; by left.
  + move/int_odd_and_1; by right.
- by Assert_upd.
- rewrite (skipn_S zero32 A ni); last by rewrite HA.
  rewrite (_ : nk - ni = S (nk - S ni))%nat; last by rewrite minus_Sn_m.
  rewrite Sum_S Hnext Htmp.
  have -> : 2 * u2Z ((nth ni A' zero32[.>>]1) [.|] [prev ]_ s) =
    2 * u2Z (nth ni A' zero32[.>>]1) + 2 * u2Z ([prev ]_ s).
    case: Hprev => Hprev.
    - by rewrite Hprev u2Z_Z2u // Zmult_0_r Zplus_0_r int_or_0 //.
    - rewrite int_or_comm.
      have X_ : (31 <= 32)%nat by repeat constructor.
      rewrite (@or_concat _ _ _ _ X_); last 2 first.
        by move: (shrl_lt (nth ni A' zero32) 1).
        apply u2Z_inj.
        move: (@u2Z_rem'' _ ([prev ]_ s) 30 1).
        rewrite {1}Hprev u2Z_Z2u // => -> //; by rewrite u2Z_Z2u.
      rewrite /cast_le_plus_minus_r2 u2Z_cast u2Z_concat u2Z_shr_shrink' //.
      rewrite Hprev !u2Z_Z2u // rem_Zpower // !u2Z_Z2u //.
      ring_simplify.
      rewrite u2Z_rem' //.
      by move: (shrl_lt (nth ni A' zero32) 1).
  have -> : u2Z (nth ni A zero32) =
    2 * u2Z (nth ni A' zero32[.>>]1) + u2Z (nth ni A' zero32[.&]one32).
    rewrite -(@u2Z_shrl 32 _ 1); last by repeat constructor.
    rewrite [Zpower _ _]/=.
    ring_simplify.
    rewrite (firstn_S zero32 A' ni) // in Hinv1; last by rewrite HlenA'.
    rewrite (firstn_S zero32 A ni) // in Hinv1; last by rewrite HA.
    case/(@app_inj_tail (int 32)): Hinv1 => Hinv' Hinv''.
    by rewrite Hinv'' int_and_rem_1.
  rewrite -Hinv2.
  suff -> : 2 * u2Z ([prev ]_ s) = 2 ^^ 32 * u2Z ([prev ]_ s[.>>]31).
    rewrite Zmult_plus_distr_r Zpower_S sext_0 add_0; ring.
- case: Hprev => Hprev.
  + by rewrite Hprev u2Z_Z2u // Zmult_0_r shrl_Z2u_0 u2Z_Z2u.
  + by rewrite Hprev u2Z_Z2u // shrl_Zpower // -minus_n_n u2Z_Z2u.
- rewrite Htmp.
  case: Hprev => ->.
  + by rewrite int_or_0.
  + by rewrite rem_distr_or rem_Zpower // int_or_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 = Z2u 32 (2 ^^ 31)) /\
  (ni < nk)%nat /\
  (var_e a |--> A') s h /\
  firstn (S ni) A' = firstn (S ni) A /\
  2 ^^ 33 * Sum (nk - S ni) (skipn (S ni) A') + 2 * u2Z ([tmp]_s) + u2Z ([prev]_ s [.>>] 31) =
  Sum (nk - ni) (skipn ni A) /\
  [tmp]_s [.%] 31 = ((nth ni A' zero32) [.>>] 1) [.%] 31 /\
  [next]_s = (nth ni A' zero32) [.&] one32).

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).
- case : Hprev => ->.
  + rewrite shl_zero; by left.
  + rewrite u2Z_Z2u // shl_1; by right.
- by Assert_upd.
- case : Hprev => Hprev.
  + by rewrite Hprev shl_zero shrl_Z2u_0 u2Z_Z2u // -Hinv2 Hprev u2Z_Z2u.
  + rewrite u2Z_Z2u //.
    have X_ : (31 <= 32)%nat by repeat constructor.
    rewrite (_ : Zabs_nat 31 = 31%nat) //.
    by rewrite Hprev (shl_1 X_) shrl_Zpower // -Hinv2 -minus_n_n [2 ^^ 0]/= Hprev.

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 = Z2u 32 (2^^31)) /\
  (ni < nk)%nat /\
  (var_e a |--> A') s h /\
  firstn (S ni) A' = firstn (S ni) A /\
  2 ^^ 33 * Sum (nk - S ni) (skipn (S ni) A') + 2 * u2Z ([tmp]_s) + u2Z ([prev]_ s [.>>] 31) =
  Sum (nk - ni) (skipn ni A) /\
  [tmp]_s [.%] 31 = (nth ni A' zero32 [.>>] 1) [.%] 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) //.
- by rewrite Hri [Zpower _ _]/= Zmult_comm.
- 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 = Z2u 32 (2 ^^ 31)) /\
  (ni < nk)%nat /\
  (var_e a |--> A') s h /\
  firstn (S ni) A' = firstn (S ni) A /\
  2 ^^ 33 * Sum (nk - S ni) (skipn (S ni) A') + 2 * u2Z ([tmp]_s) + u2Z ([prev]_ s [.>>] 31) =
  Sum (nk - ni) (skipn ni A) /\
  [tmp]_s [.%] 31 = (nth ni A' zero32 [.>>] 1) [.%] 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 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'.

move=> s h [A' [ni [HlenA' [Hra [Hrk [Hri [Hprev [Hik [Hmem [Hinv1 [Hinv2 [Hrtmp 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.
- by apply lt_le_weak.
- rewrite HA' update_list_app HlenA1 // -minus_n_n /= (decompose_equiv _ _ _ _ _ HlenA1).
  assoc_comm H'.
  move: H'; by apply mapsto_ext.
- rewrite HA' update_list_app; last by rewrite HlenA1.
  rewrite firstn_app //.
  rewrite (firstn_S zero32 A' ni) // in Hinv1; last by rewrite HlenA'.
  rewrite (firstn_S zero32 A ni) // in Hinv1; last by rewrite HA.
  move/(@app_inj_tail (int 32)): Hinv1 => [Hinv' Hinv''].
  by rewrite -Hinv' HA' firstn_app.
- rewrite -Hinv2.
  f_equal.
  rewrite HA' update_list_app; last by rewrite HlenA1.
  rewrite skipn_app // HlenA1 -minus_n_n [update_list _ _ _]/=.
  have -> : (nk - ni = S (nk - (S ni)))%nat by rewrite minus_Sn_m.
  rewrite Sum_S app_comm_cons -app_ass skipn_app; last first.
    by rewrite app_length /= HlenA1 plus_comm.
  ring_simplify.
  f_equal.
  by rewrite -Zpower_S Zmult_comm.
Qed.