Library multi_sub_inplace_right_triple

Require Import ssreflect ssrbool eqtype.
Require Import Arith_ext ZArith_ext Lists_ext.
Require Import machine_int multi_int.
Import MachineInt.
Require Import mips_seplog mips_tactics mips_contrib mips_tactics mapstos.
Require Import multi_sub_prg.

Local Open Scope machine_int_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.

Section multi_sub.

Variables k a b t j u bor atmp btmp' : reg.

Lemma multi_sub_inplace_right_triple : nodup(k, a, b, t, j, u, bor, atmp, btmp', 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 => [a ]_s = va /\ [b ]_s = vb /\
  u2Z [k ]_s = Z_of_nat nk /\ (var_e a |--> A ** var_e b |--> B) s h }}
multi_sub k a b b t j u bor atmp btmp'
{{ fun s h => exists B', length B' = nk /\ [a ]_s = va /\
  [b ]_s = vb /\ u2Z [k ]_s = Z_of_nat nk /\
  (var_e a |--> A ** var_e b |--> B') s h /\
  u2Z [bor ]_s <= 1 /\
  Sum nk B' = Sum nk A - Sum nk B + u2Z [bor ]_s * Zbeta nk }}.
Proof.
move=> Hset nk va vb Hnb A B Ha Hb; rewrite /multi_sub.

addiu j zero zero16;

NextAddiu.
move=> s h [Hra [Hrb [Hrk H]]].
rewrite /wp_addiu; repeat reg_upd; repeat (split; trivial).
by Assert_upd.

addi t c zero16

NextAddiu.
move=> s h [[Hra [Hrb [Hrk H]]] Hj].
rewrite /wp_addiu; repeat reg_upd; repeat (split; trivial).
by Assert_upd.

addi bor zero zero16;

NextAddiu.
move=> s h [[[Hra [Hrb [Hrk H]]] Hj] Ht].
rewrite /wp_addiu; repeat reg_upd; repeat (split; trivial).
by Assert_upd.

while (bne j k) (

apply hoare_prop_m.hoare_while_invariant with (fun s h => exists B', exists nj, exists nbor,
  length B' = nk /\ [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 /\
  u2Z [t ]_s = u2Z vb + 4 * Z_of_nat nj /\ u2Z [bor ]_s = nbor /\
  nbor <= 1 /\ Sum nj B' = Sum nj A - Sum nj B + nbor * Zbeta nj /\
  skipn nj B = skipn nj B').

move=> s h [[[[Hra [Hrb [Hrk H]]] Hj] Ht Hbor]].

exists B, O, 0; repeat (split => //).
by rewrite Hj store.get_r0 add_com add_0 sext_Z2u // u2Z_Z2u.
by apply le_O_n.
rewrite Ht sext_0 add_0 Hrb; ring.
by rewrite Hbor sext_0 add_0 store.get_r0 u2Z_Z2u.

move=> s h [[B' [nj [nbor [HlenC [Hra [Hrb [Hrk [Hmem [Hrj [Hjk2 [Hrt [Hrbor [Hnbor [HInv Hnth]]]]]]]]]]]]] Hjk]];
  rewrite /= in Hjk. move/negPn : Hjk; move/Zeq_boolP => Hjk.
exists B'; repeat (split; trivial).
by rewrite Hrbor.
have -> : nk = nj.
  rewrite Hrj Hrk in Hjk; by apply Z_of_nat_inj.
by rewrite Hrbor -HInv.

lwxs atmp j b;

apply hoare_lwxs_back_alt'' with (fun s h => exists B', exists nj, exists nbor,
  length B' = nk /\ [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 /\
  u2Z [t ]_s = u2Z vb + 4 * Z_of_nat nj /\ u2Z [bor ]_s = nbor /\ nbor <= 1 /\
  Sum nj B' = Sum nj A - Sum nj B + nbor * Zbeta nj /\ skipn nj B = skipn nj B' /\
  [atmp ]_s = nth nj B zero32).

move=> s h [[B' [nj [nbor [HlenC [Hra [Hrb [Hrk [Hmem [Hrj [Hjk2 [Hrt [Hrbor [Hnbor [HInv Hnth]]]]]]]]]]]]] Hjk]];
  rewrite /= in Hjk. move/Zeq_boolP : Hjk => Hjk.

have {Hjk}Hjk : (nj < nk)%nat.
  apply le_neq_lt; first by exact Hjk2.
  rewrite Hrj Hrk in Hjk.
  contradict Hjk; by rewrite Hjk.

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 Hrj inj_mult Zmult_comm.
- rewrite /update_store_lwxs.
  exists B', nj, nbor; 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.

addu btmp' atmp bor;

apply hoare_addu with (fun s h => exists B', exists nj, exists nbor,
  length B' = nk /\ [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 /\
  u2Z [t ]_s = u2Z vb + 4 * Z_of_nat nj /\ u2Z [bor ]_s = nbor /\
  nbor <= 1 /\ Sum nj B' = Sum nj A - Sum nj B + nbor * Zbeta nj /\
  skipn nj B = skipn nj B' /\
  [atmp ]_s = nth nj B zero32 /\ [btmp']_s = nth nj B zero32 [.+] [bor ]_s).

move=> s h [B' [nj [nbor [HlenC [Hra [Hrb [Hrk [Hmem [Hrj [Hjk2 [Hrt [Hrbor [Hnbor [HInv [Hnth Hratmp]]]]]]]]]]]]]]].
exists B', nj, nbor; repeat reg_upd; repeat (split; trivial).
by Assert_upd.
by rewrite -Hratmp.

sltu u btmp' atmp;

lwxs atmp j a;

apply hoare_lwxs_back_alt'' with (fun s h => exists B', exists nj, exists nbor,
  length B' = nk /\ [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 /\
  u2Z [t ]_s = u2Z vb + 4 * Z_of_nat nj /\ u2Z [bor ]_s = nbor /\ nbor <= 1 /\
  Sum nj B' = Sum nj A - Sum nj B + nbor * Zbeta nj /\
  skipn nj B = skipn nj B' /\ [atmp ]_s = nth nj A zero32 /\
  [btmp']_s = nth nj B zero32 [.+] [bor ]_s /\
  [u ]_s = if Zlt_bool (u2Z [btmp']_s) (u2Z (nth nj B zero32)) then one32 else zero32).

move=> s h [B' [nj [nbor [HlenC [Hra [Hrb [Hrk [Hmem [Hrj [Hjk2 [Hrt [Hrbor [Hnbor [HInv [Hnth [Hrbtmp' Hru]]]]]]]]]]]]]]]].

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 Hrj inj_mult Zmult_comm.
- rewrite /update_store_lwxs.
  exists B', nj, nbor; repeat reg_upd; repeat (split; trivial).
  by Assert_upd.

ifte_beq u, zero thendo

apply while.hoare_seq with (fun s h => exists B', exists nj, exists nbor,
  length B' = nk /\ [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 /\
  u2Z [t ]_s = u2Z vb + 4 * Z_of_nat nj /\
  skipn nj B = skipn nj B' /\ u2Z [bor ]_s = nbor /\ nbor <= 1 /\
  Sum nj B' + u2Z [atmp ]_s * Zbeta nj =
  Sum nj A - Sum nj B + u2Z (nth nj A zero32) * Zbeta nj - u2Z (nth nj B zero32) * Zbeta nj + nbor * Zbeta (S nj)).

apply while.hoare_ifte.

addiu u r0 one16;

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

move=> s h [[B' [nj [nbor [HlenC [Hra [Hrb [Hrk [Hmem [Hrj [Hjk2 [Hrt [Hrbor [Hnbor [HInv [Hnth [Hratmp [Hrbtmp' Hru]]]]]]]]]]]]]]]]] Huzero]; rewrite /= in Huzero.

exists B', nj, nbor; repeat reg_upd; repeat (split; trivial).
by Assert_upd.
by rewrite add_com add_0 sext_Z2u.
rewrite Hrbtmp' -Hrbor u2Z_add //.
have X : u2Z (nth nj B zero32) <= u2Z [btmp']_s.
  apply Znot_gt_le.
  move/Zgt_lt.
  move/Zlt_boolP => X.
  by rewrite Hru X /zero32 /one32 ?u2Z_Z2u in Huzero.
rewrite Hrbtmp' in X.
by apply u2Z_add_no_overflow in X.

multu atmp one;

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

move=> s h [B' [nj [nbor [HlenC [Hra [Hrb [Hrk [Hmem [Hrone [Hrj [Hjk2 [Hrt [Hrbor [Hnbor [HSum [Hnth [Hratmp [Hrbtmp' Hru]]]]]]]]]]]]]]]]]].

exists B', nj, nbor; repeat reg_upd; repeat (split; trivial).
by Assert_upd.
by rewrite store.utoZ_multu Hrone umul_1 u2Z_zext Hnth.

msubu btmp' one;

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

move=> s h [B' [nj [nbor [HlenC [Hra [Hrb [Hrk [Hmem [Hone [Hrj [Hjk [Hrt [Hrbor [Hnbor [Hinv [Hratmp [Hnth [Hrbtmp' [Hrbtmp'2 Hm]]]]]]]]]]]]]]]]]]].
exists B'; exists nj; exists nbor.
rewrite Hone umul_1.
repeat reg_upd; repeat (split; trivial).
by Assert_upd.
move=> H; rewrite store.msubu_utoZ Hm ?u2Z_zext //.
apply Zlt_trans with (Zbeta 1) => //.
by apply max_u2Z.
by apply Zle_ge.
move=> H; rewrite store.msubu_utoZ_overflow Hm ?u2Z_zext //.
apply Zlt_trans with (Zbeta 1) => //.
by apply max_u2Z.

sltu bor atmp btmp';

apply hoare_sltu with (fun s h => exists B', exists nj, exists nbor,
  length B' = nk /\ [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 /\
  u2Z [t ]_s = u2Z vb + 4 * Z_of_nat nj /\ nbor <= 1 /\
  Sum nj B' = Sum nj A - Sum nj B + nbor * Zbeta nj /\
  [atmp ]_s = nth nj A zero32 /\
  skipn nj B = skipn nj B' /\
  [btmp']_s = nth nj B zero32 [.+] Z2u 32 nbor /\
  u2Z [btmp']_s = u2Z (nth nj B zero32) + nbor /\
  (u2Z [btmp']_s <= u2Z (nth nj A zero32) -> store.utoZ s = u2Z (nth nj A zero32) - u2Z [btmp']_s ) /\
  (u2Z (nth nj A zero32) < u2Z [btmp']_s -> store.utoZ s = Zbeta 2 + u2Z (nth nj A zero32) - u2Z [btmp']_s ) /\
  [bor ]_s = if Zlt_bool (u2Z (nth nj A zero32)) (u2Z [btmp']_s) then one32 else zero32).

move=> s h [B' [nj [nbor [HlenC [Hra [Hrb [Hrk [Hmem [Hone [Hrj [Hjk [Hrt [Hrbor [Hnbor [Hinv [Hratmp [Hnth [Hrbtmp' [Hrbtmp'2 [Hinv1 Hinv2]]]]]]]]]]]]]]]]]]]].

exists B', nj, nbor; repeat reg_upd; repeat (split; trivial).
by Assert_upd.
by rewrite -Hrbor Z2u_u2Z.
by rewrite -Hratmp.

mflhxu atmp

apply hoare_mflhxu'.
move=> s h [B' [nj [nbor [HlenC [Hra [Hrb [Hrk [Hmem [Hrj [Hjk [Hrt [Hnbor [Hinv [Hratmp [Hnth [Hrbtmp' [Hrbtmp'2 [Hm1 [Hm2 Hrbor]]]]]]]]]]]]]]]]]]].

case: (Z_lt_le_dec (u2Z (nth nj A zero32)) (u2Z [btmp']_s)).
- move/Zlt_boolP => X.
  rewrite X in Hrbor.
  move/Zlt_boolP : X => X.
  exists B', nj, (u2Z one32).
  repeat reg_upd; repeat (split; trivial).
  by Assert_upd.
  by rewrite Hrbor.
  by rewrite u2Z_Z2u.
  move: {Hm1 Hm2}(Hm2 X) => Hm.
  have Hacx0 : store.acx s = Z2u store.acx_size 0.
    apply store.utoZ_acx_beta2.
    rewrite Hm; omega.
  rewrite store.utoZ_def Hacx0{Hacx0} u2Z_Z2u // in Hm.
  rewrite Zmult_0_l -Zplus_0_r_reverse in Hm.
  rewrite (_ : Zbeta 2 = Zbeta 1 * (Zbeta 1 - 1) + Zbeta 1) // Zplus_comm (Zmult_comm (Zbeta 1)) in Hm.
  rewrite (_ : forall a b c d, a + b + c - d = a + (b + c - d)) in Hm; last by (move=> *; ring).
  apply poly_eq_inv in Hm; last first.
    rewrite Zbeta1_Zpower2.
    split.
    by apply min_u2Z.
    split.
    by split; [apply min_u2Z | apply max_u2Z].
    split; first by done.
    move: (min_u2Z (nth nj A zero32)) (max_u2Z [btmp']_s) => X1 X2; omega.
  case: Hm => _ Hm.
  rewrite Hinv Hm (Zbeta_S nj) Hrbtmp'2 u2Z_Z2u //; ring.
- move/Zle_not_lt.
  move/Zlt_boolP.
  move/negbTE => X.
  rewrite X in Hrbor.
  move/Zlt_boolP : X.
  move/Znot_lt_le => X.
  exists B', nj, (u2Z zero32).
  repeat reg_upd; repeat (split; trivial).
  by Assert_upd.
  by rewrite Hrbor.
  by rewrite u2Z_Z2u.
  move: {Hm1 Hm2}(Hm1 X) => Hm.
  have H0 : store.utoZ s < Zbeta 1.
    move: (max_u2Z (nth nj A zero32)) (min_u2Z [btmp']_s).
    rewrite Hm -Zbeta1_Zpower2 => Y Z; omega.
  case/store.utoZ_lo_beta1 : H0 => _ [_ <-].
  rewrite Hinv Hm Hrbtmp'2 u2Z_Z2u //; ring.

nop);

apply hoare_nop'.

we are in the branch where btmp' = atmp + bor has overflowed

move=> s h [[B' [nj [nbor [HlenC [Hra [Hrb [Hrk [Hmem [Hrj [Hjk [Hrt [Hrbor [Hnbor [Hinv [Hnth [Hratmp [Hrbtmp' Hru]]]]]]]]]]]]]]]] Huzero]];
  rewrite /= in Huzero. move/negbTE : Huzero. move/Zeq_boolP => Huzero.
exists B'; exists nj; exists nbor.
repeat reg_upd.
repeat (split; trivial).
have [X1 X2] : nbor = 1 /\ u2Z (nth nj B zero32) = Zbeta 1 - 1.
  have H : u2Z [btmp']_s < u2Z (nth nj B zero32).
    apply/Zlt_boolP.
    apply: Bool.not_false_is_true => X.
    by rewrite Hru X in Huzero.
  rewrite Hrbtmp' in H.
  apply u2Z_add_overflow' in H; rewrite -Zbeta1_Zpower2 in H.
  move: (max_u2Z (nth nj B zero32)) => H'; rewrite -Zbeta1_Zpower2 in H'; omega.
rewrite Hratmp Hinv X1 X2 !Zmult_1_l (Zbeta_S nj); ring.

sw ctmp zero16 t;

apply hoare_sw_back'' with (fun s h => exists B', exists nj, exists nbor,
  length B' = nk /\ [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 /\
  u2Z [t ]_s = u2Z vb + 4 * Z_of_nat nj /\ u2Z [bor ]_s = nbor /\
  nbor <= 1 /\ Sum (S nj) B' = Sum (S nj) A - Sum (S nj) B + nbor * Zbeta (S nj) /\
  skipn (S nj) B = skipn (S nj) B').

move=> s h [B' [nj [nbor [HlenB' [Hra [Hrb [Hrk [Hmem [Hrj [Hjk [Hrt [Hnth [Hrbor [Hnbor Hinv]]]]]]]]]]]]]].

have Htmp : [ add_e (var_e t) (int_e (sext 16 zero16)) ]e_s =
            [ add_e (var_e b) (int_e (Z2u 32 (Z_of_nat (4 * nj)))) ]e_ s.
  rewrite [mult]lock /= -lock sext_Z2u // add_0.
  apply u2Z_inj.
  rewrite u2Z_add_Z_of_nat.
  rewrite inj_mult Hrt Hrb; ring.
  rewrite inj_mult -Zbeta1_Zpower2 Hrb; simpl Z_of_nat; omega.

exists (int_e (nth nj B' zero32)).

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

rewrite HB' (decompose_equiv _ _ _ _ _ HlenB'1) !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 => // ht.
by apply mapsto_ext.
apply currying => h' H'; simpl app in H'.
exists (update_list B' nj [atmp ]_s); exists nj; exists nbor.
repeat (split; trivial).
by apply len_update_list.
rewrite HB' update_list_app HlenB'1 // -minus_n_n /= (decompose_equiv _ _ _ _ _ HlenB'1).
assoc_comm H'.
by move: H'; apply mapsto_ext.

rewrite HB' app_comm_cons -app_ass update_list_app'; last first.
  rewrite app_length /= HlenB'1 plus_comm /=; by apply lt_n_Sn.
rewrite update_list_app; last first.
  rewrite HlenB'1; by apply le_refl.
rewrite HlenB'1 -minus_n_n; simpl update_list; simpl app; rewrite -Sum_beyond; last first.
  by rewrite app_length /= HlenB'1 plus_comm.
rewrite (Sum_cut nj B'1 HlenB'1 (S nj) (B'1 ++ [atmp ]_s :: nil) ([atmp ]_s :: nil)) //; last first.
  by rewrite app_length /= HlenB'1 plus_comm.
rewrite minus_Sn_n.

rewrite HB' -Sum_beyond // in Hinv.
rewrite -/(Zbeta nj) Zmult_comm Hinv.

Decompose_32 A nj A1 A2 HlenA1 HA'; last by rewrite Ha.

rewrite {3}HA' app_comm_cons -app_ass -Sum_beyond; last first.
  by rewrite app_length /= HlenA1 plus_comm.
rewrite (Sum_cut nj A1 HlenA1 (S nj) (A1 ++ nth nj A zero32 :: nil) (nth nj A zero32 :: nil)) //; last first.
  by rewrite app_length /= HlenA1 plus_comm.
rewrite minus_Sn_n.

Decompose_32 B nj B1 B2 HlenB1 HB_; last by rewrite Hb.
rewrite {3}HB_ app_comm_cons -app_ass -Sum_beyond; last first.
  by rewrite app_length /= HlenB1 plus_comm.
rewrite (Sum_cut nj B1 HlenB1 (S nj) ((B1 ++ nth nj B zero32 :: nil)) (nth nj B zero32 :: nil)) //; last first.
  by rewrite app_length /= HlenB1 plus_comm.
rewrite minus_Sn_n HA' -Sum_beyond // app_nth2; last by rewrite HlenA1.
rewrite HlenA1 -minus_n_n HB_ -Sum_beyond // app_nth2; last by rewrite HlenB1.
rewrite HlenB1 -minus_n_n -/(Zbeta nj) /=; 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 HlenB'.
by case: Hnth.

addiu t t four16;

apply hoare_addiu with (fun s h => exists B', exists nj, exists nbor,
length B' = nk /\ [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 /\
u2Z [t ]_s = u2Z vb + 4 * (Z_of_nat nj + 1) /\ u2Z [bor ]_s = nbor /\ nbor <= 1 /\
Sum (S nj) B' = Sum (S nj) A - Sum (S nj) B + nbor * Zbeta (S nj) /\ skipn (S nj) B = skipn (S nj) B').

move=> s h [B' [nj [nbor [HlenC [Hra [Hrb [Hrk [Hmem [Hrj [Hjk [Hrt [Hbor [Hnbor [Hinv Hnth]]]]]]]]]]]]]].

exists B', nj, nbor; repeat reg_upd; repeat (split; trivial).
by Assert_upd.
rewrite u2Z_add sext_Z2u // u2Z_Z2u //.
- omega.
- rewrite -Zbeta1_Zpower2; omega.

addiu j j one16

apply hoare_addiu'.
move=> s h [B' [nj [nbor [HlenC [Hra [Hrb [Hrk [Hmem [Hrj [Hjk [Hrt [Hbor [Hnbor [Hinv Hnth]]]]]]]]]]]]]].

exists B', (S nj), nbor.
rewrite Z_S.
repeat reg_upd; repeat (split; trivial).
by Assert_upd.

rewrite sext_Z2u // u2Z_add_Z2u //.
by rewrite Hrj.
move: (min_u2Z vb) => ?; rewrite -Zbeta1_Zpower2; omega.
Qed.

Lemma multi_sub_inplace_right_triple_B_le_A : nodup(k, a, b, t, j, u, bor, atmp, btmp', r0) ->
forall nk va vb, u2Z vb + 4 * Z_of_nat nk < Zbeta 1 ->
forall A B, length A = nk -> length B = nk -> Sum nk B <= Sum nk A ->
{{ fun s h =>
  [a ]_s = va /\ [b ]_s = vb /\
  u2Z [k ]_s = Z_of_nat nk /\ (var_e a |--> A ** var_e b |--> B) s h }}
multi_sub k a b b t j u bor atmp btmp'
{{ fun s h => exists B', length B' = nk /\ [a ]_s = va /\
  [b ]_s = vb /\ u2Z [k ]_s = Z_of_nat nk /\ [bor ]_s = zero32 /\
  (var_e a |--> A ** var_e b |--> B') s h /\
  Sum nk B' = Sum nk A - Sum nk B }}.
Proof.
move=> Hset nk va vb Hna A B Ha Hb HAB.
eapply hoare_prop_m.hoare_weak; last by eapply multi_sub_inplace_right_triple; eauto.
move=> s h [A' [HlenA [Hra [Hrb [Hrk [Hmem [Hbor Hsum]]]]]]].
have X : u2Z [bor ]_s = 0.
  have {Hsum}Hsum : u2Z [bor ]_ s * Zbeta nk + (Sum nk A - Sum nk B - Sum nk A') = 0 * Zbeta nk + 0.
    rewrite Hsum; ring.
  apply poly_eq0_inv in Hsum.
  tauto.
  by apply Zpower_0'.
  move: (min_Sum B nk) (min_Sum A' nk) (Sum_max 32 nk A) (Sum_max 32 nk A') => HB HA' HA_ HA_'.
  rewrite Zbeta_power; omega.
exists A'; repeat (split => //).
rewrite (_ : 0 = u2Z zero32) in X; last by rewrite u2Z_Z2u.
by move/u2Z_inj : X.
rewrite Hsum X Zmult_0_l Zplus_0_r; reflexivity.
Qed.

End multi_sub.