Library multi_add_signed_unsigned_triple

Require Import ssreflect ssrbool eqtype.
Require Import Arith_ext ZArith_ext Lists_ext.
Require Import nodup machine_int multi_int.
Import MachineInt.
Require Import mips_bipl mips_seplog mips_frame mips_contrib mips_tactics.
Import expr_m.
Import assert_m.

Require Import multi_add_signed_unsigned_prg.
Require Import pick_sign_triple multi_add_inplace_triple multi_lt_triple multi_sub_inplace_right_triple multi_sub_inplace_left_triple multi_negate_triple multi_is_zero_triple copy_triple.

Local Open Scope mips_expr_scope.
Local Open Scope mips_assert_scope.
Local Open Scope mips_hoare_scope.
Local Open Scope nodup_scope.
Local Open Scope zarith_ext_scope.
Local Open Scope machine_int_scope.

Lemma multi_add_s_u'_triple : forall k a b a0 a1 a2 a3 a4 a5 X,
  nodup(k, a, b, a0, a1, a2, a3, a4, a5, X, r0) ->
  forall nk va vb ptr, nk <> O -> Z_of_nat nk < 2 ^^ 31 ->
    u2Z ptr + 4 * Z_of_nat nk < Zbeta 1 ->
  forall A B, length A = nk -> length B = nk -> 0 < Sum nk B ->
  forall slen, s2Z slen = Zsgn (s2Z slen) * Z_of_nat nk ->
{{ fun s h => [ a ]_s = va /\ [ b ]_s = vb /\ u2Z [ k ]_s = Z_of_nat nk /\
   ((var_e a |--> slen :: ptr :: nil ** int_e ptr |--> A) ** var_e b |--> B) s h }}
 multi_add_s_u' k a b a0 a1 a2 a3 a4 a5 X
{{ fun s h => exists A', exists slen', length A' = nk /\
  [a]_s = va /\ [b]_s = vb /\ s2Z slen' = Zsgn (s2Z slen') * Z_of_nat nk /\
  Zsgn (s2Z slen') = Zsgn (Zsgn (s2Z slen) * Sum nk A + Sum nk B) /\
  (var_e a |--> slen' :: ptr :: nil ** int_e ptr |--> A' ** var_e b |--> B) s h /\
  u2Z ([a3]_ s) <= 1 /\
  Zsgn (s2Z slen') * (Sum nk A' + u2Z ([a3]_ s) * Zbeta nk) =
  Zsgn (s2Z slen) * Sum nk A + Sum nk B }}.
Proof.
move=> k a b a0 a1 a2 a3 a4 a5 X Hregs nk va vb ptr Hnk Hnk' ptr_fit A B
  len_A len_B nk_B slen slen_no_weird.
rewrite /multi_add_s_u'.

apply hoare_lw_back_alt'' with (fun s h => [a ]_ s = va /\ [b ]_ s = vb /\
  u2Z ([k ]_ s) = Z_of_nat nk /\ [X ]_s = ptr /\
  ((var_e a |--> slen :: ptr :: nil ** int_e ptr |--> A) ** var_e b |--> B) s h).

rewrite /while.entails => s h [r_a [r_b [r_k Hmem]]].
exists ptr; split.
- rewrite con_com_equiv !con_assoc_equiv con_com_equiv !con_assoc_equiv
    con_com_equiv !con_assoc_equiv in Hmem.
  move: Hmem; apply monotony => // h'; apply mapsto_ext => //; by rewrite sext_Z2u.
- rewrite /update_store_lw.
  repeat reg_upd; repeat (split => //).
  by Assert_upd.

apply while.hoare_seq with (fun s h => [a ]_ s = va /\ [b ]_ s = vb /\
  u2Z ([k ]_ s) = Z_of_nat nk /\ [X ]_s = ptr /\ [a0]_s = slen /\
  Zsgn (s2Z [a1]_s) = Zsgn (s2Z slen) /\ (s2Z [a1]_s = 0 \/ s2Z [a1]_s = 1 \/ s2Z [a1]_s = -1 ) /\
  ((var_e a |--> slen :: ptr :: nil ** int_e ptr |--> A) ** var_e b |--> B) s h).

eapply while.hoare_conseq; last first.
apply (pick_sign_triple _ _ _
  (fun s h => [b ]_ s = vb /\ u2Z [k ]_ s = Z_of_nat nk /\ [X ]_ s = ptr)
  (((add_e (var_e a) (int_e four32) |~> int_e ptr ** (fun st h0 =>
    u2Z (([a ]_ st [.+] four32) [.+] four32) mod 4 = 0 /\
    emp st h0)) ** int_e ptr |--> A) ** var_e b |--> B) va slen).

by Nodup_nodup r0.
Inde.
move=> s h x v /= [].
move=> ?; subst a1; by reg_upd.
case=> // ?; subst a0; by reg_upd.
by Inde.
move=> s h /= [Ha [Hb [Hk [HX Hmem]]]].
by rewrite !con_assoc_equiv in Hmem *.
move=> s h /= [Ha [Ha0 [Ha1 [Ha1' [Hmem [Hb [Hk HX]]]]]]].
by rewrite !con_assoc_equiv in Hmem *.

apply while.hoare_ifte.

apply while.hoare_ifte.

apply while.hoare_seq with (fun s h => [a ]_ s = va /\ [b ]_ s = vb /\
  u2Z [k ]_ s = Z_of_nat nk /\ [X ]_ s = ptr /\ [a0 ]_ s = slen /\
  Zsgn (s2Z slen) = 0 /\
  ((var_e a |--> slen :: ptr :: nil ** int_e ptr |--> B) ** var_e b |--> B) s h).

apply (before_frame
  (fun s h => [a ]_ s = va /\ [b ]_ s = vb /\ [a0 ]_ s = slen /\
    Zsgn (s2Z slen) = 0 /\ (var_e a |--> slen :: ptr :: nil) s h)
  (fun s h => [X]_s = ptr /\ u2Z [k]_s = Z_of_nat nk /\
    (var_e b |--> B ** var_e X |--> A) s h)
  (fun s h => [X]_s = ptr /\ u2Z [k]_s = Z_of_nat nk /\
    (var_e b |--> B ** var_e X |--> B) s h)).

apply frame_rule; last 2 first.
  by Inde_frame.
  move=> ?; by Inde_mult.

apply copy_triple => //; by Nodup_nodup r0.
move=> s h [ [[Ha [Hb [Hk [HX [Ha0 [a1_slen [Ha1' mem]]]]]]] _] Ha1].
rewrite con_assoc_equiv in mem.
case: mem => h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
exists h2, h1.
split; first by heap_tac_m.Disj.
split; first by heap_tac_m.Equal.
repeat (split => //).
rewrite con_com_equiv.
move: Hh2; apply monotony => // h'; by apply mapstos_ext.
rewrite /= in Ha1.
move/eqP in Ha1.
move/u2Z_inj in Ha1.
rewrite store.get_r0 in Ha1.
by rewrite -a1_slen Ha1 s2Z_u2Z_pos' // u2Z_Z2u.

move=> s h [h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]]].
case: Hh2 => [Ha [Hb [Ha0 [Ha1' Hh2]]]].
case: Hh1 => Hx [Hk Hh1].
repeat (split => //).
rewrite con_assoc_equiv.
exists h2, h1.
split; first by heap_tac_m.Disj.
split; first by heap_tac_m.Equal.
repeat (split => //).
rewrite con_com_equiv.
move: Hh1; apply monotony => h' //; by apply mapstos_ext.

apply hoare_addiu with (fun s h =>
  [a ]_ s = va /\ [b ]_ s = vb /\ u2Z [k ]_ s = Z_of_nat nk /\
  [X ]_ s = ptr /\ [a0 ]_ s = slen /\ [a3]_s = zero32 /\
  Zsgn (s2Z slen) = 0 /\
  ((var_e a |--> slen :: ptr :: nil ** int_e ptr |--> B) ** var_e b |--> B) s h).

move=> s h [Ha [Hb [Hk [HX [Ha0 [Ha1 mem]]]]]].
rewrite /wp_addiu.
repeat reg_upd; repeat (split => //).
by rewrite add_com add_0 sext_Z2u.
by Assert_upd.

apply hoare_sw_back'.
move=> s h [Ha [Hb [Hk [HX [Ha0 [Ha3 [Hslen mem]]]]]]].
exists (int_e slen).
rewrite !con_assoc_equiv /= in mem.
move: mem; apply monotony => // h'.
apply mapsto_ext => //; by rewrite /= sext_Z2u // add_0.
apply currying => h'' Hh''.
exists B, (Z2s 32 (Z_of_nat nk)).
repeat (split => //).

rewrite s2Z_Z2s //; last by omega.
rewrite (proj2 (Zsgn_pos (Z_of_nat nk))); omega.

rewrite s2Z_Z2s //; last by omega.
rewrite Hslen /= (proj2 (Zsgn_pos (Z_of_nat nk))); last by omega.
by rewrite (proj2 (Zsgn_pos (Sum nk B))).

rewrite con_com_equiv in Hh''.
rewrite /= !con_assoc_equiv.
move: Hh''; apply monotony => // h'''.
apply mapsto_ext => /=.
by rewrite sext_Z2u // add_0.
apply u2Z_inj.
rewrite Hk u2Z_Z2s_pos //.
split; by [omega | eapply Zlt_le_trans; [apply Hnk' | ]].
by rewrite Ha3 u2Z_Z2u.
rewrite s2Z_Z2s //; last by omega.
rewrite (proj2 (Zsgn_pos (Z_of_nat nk))); last by omega.
by rewrite Zmult_1_l Hslen /= Ha3 u2Z_Z2u // Zmult_0_l Zplus_0_r.

apply hoare_addiu with (fun s h => [a ]_ s = va /\ [b ]_ s = vb /\ u2Z [k ]_ s = Z_of_nat nk /\
  [X ]_ s = ptr /\ [a0 ]_ s = slen /\ Zsgn (s2Z [a1 ]_ s) = Zsgn (s2Z slen) /\
  s2Z [a1]_s = 1 /\ [a3]_s = one32 /\
  ((var_e a |--> slen :: ptr :: nil ** int_e ptr |--> A) ** var_e b |--> B) s h).

rewrite /wp_addiu => s h [[[Ha [Hb [Hk [HX [Ha0 [Ha1 [Ha1'' mem]]]]]]] Ha1'''] Ha1'].
repeat reg_upd.
rewrite /= in Ha1' Ha1'''.
move/Zle_boolP in Ha1'''.
rewrite store.get_r0 u2Z_Z2u // in Ha1'.
move/eqP in Ha1'.
repeat (split => //).
case: Ha1'' => [Ha1'' | [ // | Ha1'']].
rewrite (_ : 0 = s2Z zero32) in Ha1''; last first.
  by rewrite s2Z_u2Z_pos' u2Z_Z2u.
move/s2Z_inj in Ha1''.
by rewrite Ha1'' u2Z_Z2u // in Ha1'.
omega.
by rewrite add_com add_0 sext_Z2u.
by Assert_upd.

apply while.hoare_seq with (fun s h => exists A', exists slen', length A' = nk /\
  [a ]_ s = va /\ [b ]_ s = vb /\ s2Z slen' = Zsgn (s2Z slen') * Z_of_nat nk /\
  ((var_e a |--> slen' :: ptr :: nil ** int_e ptr |--> A') ** var_e b |--> B) s h /\
  u2Z (store.lo s) <= 1 /\
  Zsgn (s2Z slen') = Zsgn (Zsgn (s2Z slen) * Sum nk A + Sum nk B) /\
  Zsgn (s2Z slen') * (Sum nk A' + u2Z (store.lo s) * Zbeta nk) =
  Zsgn (s2Z slen) * Sum nk A + Sum nk B).

have : nodup(k, a3, b, X, a0, a1, a2, r0) by Nodup_nodup r0.
move/multi_add_inplace_triple.multi_add_inplace_triple.
move/(_ nk vb ptr ptr_fit _ _ len_B len_A) => Htmp.

apply (before_frame
  (fun s h => Zsgn (s2Z slen) = 1 /\ [a ]_ s = va /\ (var_e a |--> slen :: ptr :: nil) s h)
  (fun s h =>
    ([a3]_s = one32 /\ [b ]_ s = vb /\ [X ]_ s = ptr /\ u2Z ([k ]_ s) = Z_of_nat nk /\
      (var_e X |--> A ** var_e b |--> B) s h) /\
    [a ]_ s = va /\ [a0 ]_ s = slen /\ 0 <= Zsgn (s2Z slen) /\ eval_b (bgez a1) s)
  (fun s h => exists A',
    length A' = nk /\ [ b ]_s = vb /\ [X ]_ s = ptr /\ (var_e b |--> B ** var_e X |--> A') s h /\
    u2Z (store.lo s) <= 1 /\ Sum nk A' + u2Z (store.lo s) * Zbeta nk = Sum nk A + Sum nk B)).

apply frame_rule; last 2 first.
  by Inde_frame.
  move=> ?; by Inde_mult.
eapply while.hoare_conseq; last by apply Htmp.
by rewrite Zplus_comm.

rewrite /while.entails => s h [[Hone [Hb [HX [Hk Hmem]]]] [Ha [Ha0 [HZsgn Ha1]]]].
move/Zle_boolP in Ha1.
by rewrite con_com_equiv in Hmem.

rewrite /while.entails => s h [Ha [Hb [Hk [HX [Ha0 [Hsgn [Hsgn' [Ha3 Hmem]]]]]]]].
rewrite con_assoc_equiv in Hmem.
case: Hmem => h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
exists h2, h1.
split; first by heap_tac_m.Disj.
split; first by heap_tac_m.Equal.
repeat (split => //).
move: Hh2; apply monotony => h' //; by apply mapstos_ext.
rewrite -Hsgn; by case: Hsgn' => ->.
rewrite /=; apply/Zle_boolP; omega.
rewrite -Hsgn; by case: Hsgn' => ->.

rewrite /while.entails => s h [h1 [h2 [h1_d_h2 [h1_U_h2 [[A' [A'_nk [r_b [HX [Hh1 [Hlo Hsum]]]]]] [Hsgn [r_a Hh2]]]]]]].
exists A', slen.
repeat (split => //).
rewrite con_assoc_equiv.
exists h2, h1.
split; first by heap_tac_m.Disj.
split; first by heap_tac_m.Equal.
split; first by assumption.
rewrite con_com_equiv.
move: Hh1; apply monotony => h' //; by apply mapstos_ext.
rewrite Hsgn Zmult_1_l (proj2 (Zsgn_pos (Sum nk A + Sum nk B))) //.
move: (min_Sum A nk) => ?; omega.
by rewrite Hsgn 2!Zmult_1_l.

apply hoare_mflo'.

rewrite /while.entails => s h [A' [slen' [len_A' [r_a [r_b [slen'_nk [Hmem [Hlo [Hsgn Hsum]]]]]]]]].
rewrite /wp_mflo.
exists A', slen'.
repeat reg_upd; repeat (split => //).
move: Hmem. apply monotony => h' //.
apply monotony => h'' //.
apply mapstos_ext => //=; by reg_upd.
by apply mapstos_ext.
apply mapstos_ext => //=; by reg_upd.

apply while.hoare_seq with (fun s h =>
  ([a ]_ s = va /\ [b ]_ s = vb /\ u2Z ([k ]_ s) = Z_of_nat nk /\
    [X ]_ s = ptr /\ Zsgn (s2Z slen) = -1 /\
    ((var_e a |--> slen :: ptr :: nil ** int_e ptr |--> A) ** var_e b |--> B) s h) /\
  ((Sum nk B < Sum nk A /\ [a5]_s = one32 /\ [a2]_s = zero32 ) \/
   (Sum nk B > Sum nk A /\ [a5]_s = zero32 /\ [a2]_s = one32 ) \/
   (Sum nk B = Sum nk A /\ [a5]_s = zero32 /\ [a2]_s = zero32))).

apply (before_frame
  (fun s h => [a ]_ s = va /\ Zsgn (s2Z slen) = -1 /\ (var_e a |--> slen :: ptr :: nil) s h)
  (fun s h => u2Z [ k ]_s = Z_of_nat nk /\
    [ b ]_s = vb /\ [ X ]_s = ptr /\ (var_e b |--> B ** var_e X |--> A) s h)
  (fun s h => u2Z ([k ]_ s) = Z_of_nat nk /\ [b ]_ s = vb /\ [X ]_ s = ptr /\
    ((Sum nk B < Sum nk A /\ ([a5 ]_ s) = one32 /\ [a2]_s = zero32) \/
      (Sum nk B > Sum nk A /\ ([a5 ]_ s) = zero32 /\ [a2]_s = one32) \/
      (Sum nk B = Sum nk A /\ ([a5 ]_ s) = zero32 /\ [a2]_s = zero32)) /\
    (var_e b |--> B ** var_e X |--> A) s h)).

apply frame_rule; last 2 first.
  by Inde_frame.
  move=> ?; by Inde_mult.
apply multi_lt_triple.multi_lt_triple => //; by Nodup_nodup r0.

rewrite /while.entails => s h [[Ha [Hb [Hk [HX [Ha0 [HZgn [Hsgn' Hmem]]]]]]] Ha1].
rewrite con_assoc_equiv in Hmem.
case : Hmem => h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
Compose_sepcon h2 h1.
repeat (split => //).
rewrite con_com_equiv.
move: Hh2; apply monotony => // h'; by apply mapstos_ext.
repeat (split => //).
rewrite /= in Ha1.
move/Zle_boolP in Ha1.
case: Hsgn' => Hsgn'; first by omega.
case: Hsgn' => Hsgn'; first by omega.
by rewrite -HZgn Hsgn'.

rewrite /while.entails => s h [h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]]].
case: Hh1 => Hk [Hb [hX [Hsum Hh1]]].
case: Hh2 => Ha [Hsgn Hh2].
split.
- repeat (split => //).
  rewrite con_assoc_equiv.
  Compose_sepcon h2 h1 => //.
  rewrite con_com_equiv.
  move: Hh1; apply monotony => // h'; by apply mapstos_ext.
- case: Hsum => Hsum.
  left; tauto.
  by right.

apply while.hoare_ifte.

apply while.hoare_ifte.

apply hoare_addiu with (fun s h => [a ]_ s = va /\ [b ]_ s = vb /\
  u2Z [k ]_ s = Z_of_nat nk /\ [X ]_ s = ptr /\ [a3]_s = zero32 /\
  Zsgn (s2Z slen) = -1 /\
  ((var_e a |--> slen :: ptr :: nil ** int_e ptr |--> A) ** var_e b |--> B) s h /\
  Sum nk B = Sum nk A).

move=> s h [ [[ [Ha [Hb [Hk [HX [Hslen mem]]] ]] Hsum] Ha5] Ha2].
rewrite /wp_addiu.
repeat reg_upd; repeat (split => //).
by rewrite add_com add_0 sext_Z2u.
by Assert_upd.
rewrite /= in Ha5 Ha2.
move/Zeq_boolP/u2Z_inj in Ha5.
move/Zeq_boolP/u2Z_inj in Ha2.
case: Hsum => Hsum.
- rewrite Ha5 store.get_r0 in Hsum.
  case: Hsum => _ [Hsum _].
  by apply Z2u_dis in Hsum.
- case: Hsum => Hsum; last by tauto.
  case: Hsum => _ [_ Hsum].
  rewrite Ha2 store.get_r0 in Hsum.
  by apply Z2u_dis in Hsum.

apply hoare_sw_back'.
move=> s h [Ha [Hb [Hk [HX [Ha3 [Hslen [mem Hsum]]]]]]].
exists (int_e slen).
rewrite !con_assoc_equiv /= in mem.
move: mem; apply monotony => // h'.
apply mapsto_ext => //=; by rewrite sext_Z2u // add_0.
apply currying => h'' Hh''.
exists A , (Z2s 32 0).
repeat (split => //).
by rewrite s2Z_Z2s .

by rewrite s2Z_Z2s //= Hslen Hsum Zplus_comm Zopp_eq_mult_neg_1_L Zplus_opp_r.
rewrite con_com_equiv in Hh''.
rewrite !con_assoc_equiv /=.
move: Hh''; apply monotony => // h'''.
apply mapsto_ext => /=.
by rewrite sext_Z2u // add_0.
rewrite store.get_r0.
apply u2Z_inj.
by rewrite u2Z_Z2u // u2Z_Z2s_pos.
by rewrite Ha3 u2Z_Z2u.
rewrite s2Z_Z2s //= Hslen Hsum; ring.

apply hoare_prop_m.hoare_stren with (fun s h => Sum nk B > Sum nk A /\
  (([a ]_ s = va /\ [b ]_ s = vb /\ u2Z ([k ]_ s) = Z_of_nat nk /\
    [X ]_ s = ptr /\ Zsgn (s2Z slen) = -1 /\
    ((var_e a |--> slen :: ptr :: nil ** int_e ptr |--> A) ** var_e b |--> B) s h))).

rewrite /while.entails => s h [[[[Ha [Hb [Hk [HX [Hsgn Hmem]]]]] Hsum] Ha5] Ha2].
repeat (split => //).
rewrite /= store.get_r0 u2Z_Z2u // in Ha5.
move/Zeq_boolP in Ha5.
case: Hsum => Hsum.
- case: Hsum => _ [Hsum _].
  by rewrite Hsum u2Z_Z2u in Ha5.
- rewrite /= in Ha2.
  move/eqP in Ha2.
  case: Hsum => Hsum; first by tauto.
  case: Hsum => _ [_ Hsum].
  by rewrite Hsum u2Z_Z2u // store.get_r0 // u2Z_Z2u in Ha2.

apply (hoare_prop_m.pull_out_conjunction' hoare0_false) => HAB.

apply while.hoare_seq with (fun s h => exists A', length A' = nk /\
  [a ]_ s = va /\ [b ]_ s = vb /\ s2Z slen = Zsgn (s2Z slen) * Z_of_nat nk /\
  ((var_e a |--> slen :: ptr :: nil ** int_e ptr |--> A') ** var_e b |--> B) s h /\
  [a3]_s = zero32 /\ Zsgn (s2Z slen) = -1 /\
  - Zsgn (s2Z slen) * (Sum nk A' - u2Z ([a3 ]_ s) * Zbeta nk) =
  Zsgn (s2Z slen) * Sum nk A + Sum nk B).

apply (before_frame
  (fun s h => [a ]_ s = va /\ Zsgn (s2Z slen) = -1 /\ (var_e a |--> slen :: ptr :: nil) s h)
  (fun s h => [b]_s = vb /\ [X ]_ s = ptr /\ u2Z ([k ]_ s) = Z_of_nat nk /\
    (var_e b |--> B ** var_e X |--> A) s h)
  (fun s h => exists A', length A' = nk /\
    [b]_s = vb /\ [X ]_ s = ptr /\ u2Z ([k ]_ s) = Z_of_nat nk /\ [a3]_s = zero32 /\
    (var_e b |--> B ** var_e X |--> A') s h /\ Sum nk A' = Sum nk B - Sum nk A)).

apply frame_rule; last 2 first.
  by Inde_frame.
  move=> ?; by Inde_mult.

apply multi_sub_inplace_right_triple.multi_sub_inplace_right_triple_B_le_A => //.
by Nodup_nodup r0.
omega.

rewrite /while.entails => s h [Ha [Hb [Hk [HX [Hsgn Hmem]]]]].
rewrite con_assoc_equiv in Hmem.
case: Hmem => h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
Compose_sepcon h2 h1; last by done.
repeat (split => //).
rewrite con_com_equiv.
move: Hh2; apply monotony => h' //; by apply mapstos_ext.

rewrite /while.entails => s h [h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 [Hva [Hsgn Hh2]]]]]]].
case: Hh1 => A' [len_A' [Hb [HX [Hk [Ha3 [Hh1 Hsum]]]]]].
exists A'.
repeat (split => //).
rewrite con_assoc_equiv.
Compose_sepcon h2 h1 => //.
rewrite con_com_equiv.
move: Hh1; apply monotony => // h'; by apply mapstos_ext.
rewrite Hsgn -Zopp_mult_distr_l 2!Zopp_eq_mult_neg_1_L Zopp_involutive Hsum Ha3 u2Z_Z2u // Zmult_0_l Zminus_0_r; ring.

apply (hoare_prop_m.extract_exists extract_exists0) => A'.

apply (before_frame (fun s h => length A' = nk /\ [a ]_ s = va /\ [b ]_ s = vb /\
  s2Z slen = Zsgn (s2Z slen) * Z_of_nat nk /\
  (var_e b |--> B) s h /\ [a3 ]_ s = zero32 /\ Zsgn (s2Z slen) = -1 /\
  - Zsgn (s2Z slen) * (Sum nk A' - u2Z [a3 ]_ s * Zbeta nk) = Zsgn (s2Z slen) * Sum nk A + Sum nk B)
(var_e a |--> slen :: ptr :: nil ** int_e ptr |--> A')
(var_e a |--> cplt2 slen :: ptr :: nil ** int_e ptr |--> A')).

apply frame_rule.
- apply negate_triple; by Nodup_nodup r0.
- Inde_frame.
  rewrite /inde => s h x v /= [] // ?; subst x; by reg_upd.
- move=> ?; by Inde_mult.

rewrite /while.entails => s h [lenA' [r_a [r_b [slen'_nk [Hmem [Ha3 [Hsgn HSum]]]]]]].
move: Hmem; by apply monotony.

rewrite /while.entails => s h Hmem.
case: Hmem => h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
case: Hh2 => A'_nk [slen_nk_ [r_a [r_b [Hh2 [Ha3 [HZsgn HSum]]]]]].
exists (cplt2 slen).
rewrite s2Z_cplt2; last first.
  rewrite weirdE2 slen_no_weird HZsgn; omega.
rewrite Ha3 u2Z_Z2u // Zmult_0_l Zminus_0_r in HSum.
rewrite Ha3 u2Z_Z2u // Zmult_0_l Zplus_0_r Zsgn_Zopp.
repeat (split => //).

have Htmp : - Zsgn (s2Z slen) = 1 by rewrite HZsgn.
rewrite !Htmp HZsgn in HSum *.
rewrite r_b HZsgn; ring.

have Htmp : - Zsgn (s2Z slen) = 1 by rewrite HZsgn.
rewrite !Htmp HZsgn in HSum *.
rewrite Zmult_1_l in HSum.
rewrite -HSum (proj2 (Zsgn_pos (Sum nk A'))) //.
move: (min_Sum A nk) => ?.
rewrite HSum Zopp_eq_mult_neg_1_L; omega.
by Compose_sepcon h1 h2.

apply hoare_prop_m.hoare_stren with (fun s h => Sum nk B < Sum nk A /\
  ([a ]_ s = va /\ [b ]_ s = vb /\ u2Z ([k ]_ s) = Z_of_nat nk /\ [X ]_ s = ptr /\
    Zsgn (s2Z slen) = -1 /\
    ((var_e a |--> slen :: ptr :: nil ** int_e ptr |--> A) ** var_e b |--> B) s h)).

rewrite /while.entails => s h [[[Ha [Hb [Hk [HX [Hslen Hmem]]]]] Hsum] Ha5].
case: Hsum => Hsum; first by tauto.
rewrite /= in Ha5.
move/eqP in Ha5.
rewrite store.get_r0 in Ha5.
case: Hsum.
case=> _ [Hsum _].
by rewrite Hsum u2Z_Z2u in Ha5.
case=> _ [Hsum _].
by rewrite Hsum u2Z_Z2u in Ha5.

apply (hoare_prop_m.pull_out_conjunction' hoare0_false) => HAB.

apply (before_frame
  (fun s h => [a ]_ s = va /\ Zsgn (s2Z slen) = -1 /\ (var_e a |--> slen :: ptr :: nil) s h)
  (fun s h => [X]_s = ptr /\
  [b]_s = vb /\ u2Z ([k ]_ s) = Z_of_nat nk /\ (var_e X |--> A ** var_e b |--> B) s h)
  (fun s h => exists A', length A' = nk /\
    [X]_s = ptr /\ [b]_s = vb /\ u2Z ([k ]_ s) = Z_of_nat nk /\ [a3]_s = zero32 /\
    (var_e X |--> A' ** var_e b |--> B) s h /\ Sum nk A' = Sum nk A - Sum nk B)).

apply frame_rule; last 2 first.
  by Inde_frame.
  move=> ?; by Inde_mult.

apply multi_sub_inplace_left_triple.multi_sub_inplace_left_triple_B_le_A => //.
by Nodup_nodup r0.
by apply Zlt_le_weak.

rewrite /while.entails => s h [Ha [Hb [Hk [HX [Hslen Hmem]]]]].
rewrite con_assoc_equiv in Hmem.
case: Hmem => h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
Compose_sepcon h2 h1; last by done.
repeat (split => //).
move: Hh2; apply monotony => // h'; by apply mapstos_ext.

rewrite /while.entails => s h Hmem.
case: Hmem => h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
case: Hh1 => A' [len_A' [HX [Hb [Hk [Ha3 [Hh1 Hsum]]]]]].
case: Hh2 => Ha [Hsgn Hh2].
exists A', slen.
repeat (split => //).
rewrite Hsgn (proj2 (Zsgn_neg (-1 * Sum nk A + Sum nk B))) // Zplus_comm Zopp_eq_mult_neg_1_L Zplus_Zopp; omega.
rewrite con_assoc_equiv.
Compose_sepcon h2 h1; first by done.
move: Hh1; apply monotony => // h'.
by apply mapstos_ext.
by rewrite Ha3 u2Z_Z2u.
rewrite Hsgn 2!Zopp_eq_mult_neg_1_L Hsum Ha3 u2Z_Z2u // Zmult_0_l; ring.
Qed.

Lemma multi_add_s_u_triple : forall k a b a0 a1 a2 a3 a4 a5 X,
  nodup(k, a, b, a0, a1, a2, a3, a4, a5, X, r0) ->
  forall nk va vb ptr, nk <> O -> Z_of_nat nk < 2 ^^ 31 ->
    u2Z ptr + 4 * Z_of_nat nk < Zbeta 1 -> u2Z vb + 4 * Z_of_nat nk < Zbeta 1 ->
  forall A B, length A = nk -> length B = nk ->
  forall slen, s2Z slen = Zsgn (s2Z slen) * Z_of_nat nk ->
    Zsgn (s2Z slen) = Zsgn (Zsgn (s2Z slen) * Sum nk A) ->
{{ fun s h => [a]_s = va /\ [b]_s = vb /\
    u2Z [k]_s = Z_of_nat nk /\
    ((var_e a |--> slen :: ptr :: nil ** int_e ptr |--> A) ** var_e b |--> B) s h }}
 multi_add_s_u k a b a0 a1 a2 a3 a4 a5 X
 {{ fun s h => exists A', exists slen', length A' = nk /\
   [a]_s = va /\ [b]_s = vb /\ s2Z slen' = Zsgn (s2Z slen') * Z_of_nat nk /\
   Zsgn (s2Z slen') = Zsgn (Zsgn (s2Z slen) * Sum nk A + Sum nk B) /\
   (var_e a |--> slen' :: ptr :: nil ** int_e ptr |--> A' ** var_e b |--> B) s h /\
   u2Z ([a3]_ s) <= 1 /\
   Zsgn (s2Z slen') * (Sum nk A' + u2Z ([a3]_ s) * Zbeta nk) =
   Zsgn (s2Z slen) * Sum nk A + Sum nk B }}.
Proof.
move=> k a b a0 a1 a2 a3 a4 a5 X Hregs nk va vb ptr Hnk Hnk' ptr_fit vb_fit A B
  len_A len_B slen slen_no_weird slen_A.
rewrite /multi_add_s_u.

apply while.hoare_seq with (fun s h => [a]_s = va /\ [b]_s = vb /\
  u2Z [k]_s = Z_of_nat nk /\
  ((var_e a |--> slen :: ptr :: nil ** int_e ptr |--> A) ** var_e b |--> B) s h /\
  ((0 = Sum nk B -> [a2]_s = one32) /\ (0 < Sum nk B -> [a2]_s = zero32))).

apply (before_frame(fun s h => [a ]_ s = va /\
  (var_e a |--> slen :: ptr :: nil ** int_e ptr |--> A) s h)
  (fun s h => u2Z [ k ]_s = Z_of_nat nk /\ [b]_s = vb /\ (var_e b |--> B) s h)
  (fun s h => u2Z [ k ]_s = Z_of_nat nk /\ [b]_s = vb /\ (var_e b |--> B) s h /\
    ((0 = Sum nk B -> [a2]_s = one32) /\ (0 < Sum nk B -> [a2]_s = zero32)))).

apply frame_rule; last 2 first.
  by Inde_frame.
  move=> ?; by Inde_mult.
  apply multi_is_zero_triple => //.
  by Nodup_nodup r0.

move=> s h [Ha [Hb [Hk mem]]].
case: mem => h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
Compose_sepcon h2 h1.
by repeat (split => //).
by repeat (split => //).
move => s h [h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]]].
repeat (split; first by tauto).
split; last by tauto.
Compose_sepcon h2 h1; tauto.

apply while.hoare_ifte.

apply hoare_addiu'.
move=> s h [ [Ha [Hb [Hk [mem Ha5]]]] Ha2].
rewrite /= in Ha2.
move/eqP in Ha2.
move: (min_Sum B nk).
case/Z_le_lt_eq_dec => Hsum.
apply (proj2 Ha5) in Hsum.
by rewrite Hsum u2Z_Z2u // store.get_r0 u2Z_Z2u in Ha2.
exists A, slen.
repeat reg_upd; repeat (split => //).
rewrite -Hsum Zplus_0_r; exact slen_A.
by Assert_upd.
by rewrite sext_Z2u // add_0 u2Z_Z2u.
rewrite sext_Z2u // add_0 u2Z_Z2u // Zmult_0_l Zplus_0_r -Hsum; ring.

apply hoare_prop_m.hoare_stren with
  ((fun s h => (0 < Sum nk B /\ h = heap.emp )) **
    (fun s h => [a ]_ s = va /\ [b ]_ s = vb /\ u2Z [k ]_ s = Z_of_nat nk /\
      ((var_e a |--> slen :: ptr :: nil ** int_e ptr |--> A) ** var_e b |--> B) s h)).

move=> s h [[Ha [Hb [Hk [mem Ha2']]]] Ha2].
rewrite /= negb_involutive in Ha2.
move/eqP/u2Z_inj in Ha2.
move: (min_Sum B nk).
case/Z_le_lt_eq_dec => Hsum; last first.
   apply (proj1 Ha2') in Hsum.
   rewrite Hsum store.get_r0 in Ha2.
   by apply Z2u_dis in Ha2.
by Compose_sepcon heap.emp h.

apply pull_out_and => nk_B.
by apply multi_add_s_u'_triple.
Qed.