Library multi_sub_signed_unsigned_triple

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

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

Require Import multi_sub_signed_unsigned_prg.
Require Import multi_add_signed_unsigned_triple pick_sign_triple copy_triple multi_is_zero_triple.

Lemma multi_sub_s_u'_triple : forall k a b a0 a1 a2 a3 a4 ret X,
nodup(k, a, b, a0, a1, a2, a3, a4, ret, 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_sub_s_u' k a b a0 a1 a2 a3 a4 ret 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 ret X Hregs nk va vb ptr Hnk Hnk' ptr_fit A B len_A len_B nk_B slen slen_not_weird.
rewrite /multi_sub_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 /\ 0 = Zsgn (s2Z slen) /\
  ((var_e a |--> slen :: ptr :: List.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/u2Z_inj in Ha1.
rewrite store.get_r0 /= in Ha1.
rewrite -a1_slen Ha1 s2Z_u2Z_pos'; by rewrite 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 /\ [a3]_s = zero32 /\
  0 = Zsgn (s2Z slen) /\
  ((var_e a |--> slen :: ptr :: nil ** int_e ptr |--> B) ** var_e b |--> B) s h).
move=> s h [Ha [Hb [Hk [HX [Hslen mem]]]]].
rewrite /wp_addiu.
repeat reg_upd.
repeat (split=> //).
by rewrite sext_Z2u // add_0.
by Assert_upd.

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

move=> s h [Ha [Hb [Hk [HX [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''.
repeat (split => //).
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 [apply Zle_0_nat |(eapply Zlt_le_trans; [apply Hnk'|])].

apply hoare_prop_m.hoare_weak with (fun s h =>
  [a ]_ s = va /\ [b ]_ s = vb /\
  Zsgn (- Z_of_nat nk) = Zsgn (Zsgn (s2Z slen) * Sum nk A - Sum nk B) /\
  ((var_e a |--> Z2s 32 (- Z_of_nat nk) :: ptr :: nil ** int_e ptr |--> B) ** var_e b |--> B) s h /\
  u2Z [a3 ]_ s <= 1 /\ 0 = Zsgn (s2Z slen) /\
  Zsgn (- Z_of_nat nk) * (Sum nk B + u2Z [a3 ]_ s * Zbeta nk) = Zsgn (s2Z slen) * Sum nk A - Sum nk B).
move=> s h [Ha [Hb [Hsgn [mem [Ha3 [Hslen HSum]]]]]].
exists B, (Z2s 32 (- Z_of_nat nk)).
repeat (split=> //).

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

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

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

move=> s h [Ha [Hb [Hk [HX [Ha3 [Hsgn mem]]]]]].
case: mem => h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
Compose_sepcon h1 h2; first by exact Hh1.
repeat (split=> //).
by rewrite Ha3 u2Z_Z2u.
rewrite -Hsgn Zmult_0_l /= Ha3 u2Z_Z2u // Zmult_0_l Zplus_0_r (proj2 (Zsgn_pos (Z_of_nat nk))) //; omega.

move=> s h [h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]]].
case: Hh2 => [Ha [Hb [hSgn [Ha3 [Hslen HSum]]]]].
repeat (split => //).
rewrite -Hslen Zmult_0_l /= in HSum *.
rewrite (proj2 (Zsgn_neg (- Z_of_nat nk))); last by omega.
rewrite (proj2 (Zsgn_neg (- Sum nk B))); omega.
Compose_sepcon h1 h2; last by done.
rewrite (_ : Z2s 32 (- Z_of_nat nk) = cplt2 (Z2s 32 (Z_of_nat nk))) //.
apply s2Z_inj.
rewrite s2Z_cplt2; last first.
  rewrite weirdE2 s2Z_Z2s; omega.
rewrite s2Z_Z2s; last by omega.
rewrite s2Z_Z2s //; omega.
rewrite (proj2 (Zsgn_pos (Z_of_nat nk))) in HSum; last by omega.
rewrite (proj2 (Zsgn_neg (- Z_of_nat nk))); last by omega.
rewrite -HSum; ring.

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 A < Sum nk B /\ [ret]_s = one32 /\ [a2]_s = zero32) \/
   (Sum nk A > Sum nk B /\ [ret]_s = zero32 /\ [a2]_s = one32) \/
   (Sum nk A = Sum nk B /\ [ret]_s = zero32 /\ [a2]_s = zero32))).

eapply (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 /\ [X ]_ s = ptr /\ [b ]_ s = vb /\
    (var_e X |--> A ** var_e b |--> B) s h )
  (fun s h =>u2Z ([k ]_ s) = Z_of_nat nk /\ [X ]_ s = ptr /\ [b ]_ s = vb /\
    (((Sum nk A < Sum nk B /\ [ret]_s = one32 /\ [a2]_s = zero32) \/
      (Sum nk A > Sum nk B /\ [ret]_s = zero32 /\ [a2]_s = one32) \/
      (Sum nk A = Sum nk B /\ [ret]_s = zero32 /\ [a2]_s = zero32)) /\
    (var_e X |--> A ** var_e b |--> B) s h))).

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

rewrite /while.entails => s h [[[Ha [Hb [Hk [HX [Ha0 [HZsgn [Ha1 Hmem]]]]]]] Ha1''] Ha1'].
move/Zle_boolP in Ha1''. rewrite /= in Ha1'. move/eqP in Ha1'.
rewrite store.get_r0 u2Z_Z2u // in Ha1'.
case: Ha1 => Ha1.
  by rewrite s2Z_u2Z_pos // in Ha1.
case: Ha1 => Ha1; last first.
  rewrite Ha1 in Ha1''. by move/Zle_boolP : 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=> //).
move: Hh2; apply monotony => // h'; by apply mapstos_ext.
repeat (split=> //).
by rewrite -HZsgn Ha1.

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

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 A = Sum nk B).

move=> s h [ [ [ [Ha [Hb [Hk [HX [Hslen [mem HSum]]]]]] Hret] Ha2] ].
rewrite /wp_addiu.
repeat reg_upd.
repeat (split => //).
by rewrite sext_Z2u // add_0.
by Assert_upd.
rewrite /= in Hret Ha2.
move/eqP/u2Z_inj in Hret.
move/eqP/u2Z_inj in Ha2.
rewrite store.get_r0 in Hret Ha2.
case: HSum => Hsum.
  rewrite Hret Ha2 in Hsum.
  case: Hsum => _ [Hsum _].
  by apply Z2u_dis in Hsum.
case: Hsum => Hsum; last by tauto.
rewrite Ha2 in Hsum.
case: Hsum => _ [_ 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 Zmult_1_l HSum Zminus_diag.

rewrite con_com_equiv in Hh''.
rewrite !con_assoc_equiv /=.
move: Hh''; apply monotony => // h3.
apply mapsto_ext => /=.
by rewrite sext_Z2u // add_0.
rewrite store.get_r0.
apply u2Z_inj.
by rewrite u2Z_Z2s_pos // u2Z_Z2u.
by rewrite Ha3 u2Z_Z2u.
by rewrite s2Z_Z2s //= Hslen Zmult_1_l HSum Zminus_diag.

apply hoare_prop_m.hoare_stren with (fun s h => Sum nk A > Sum nk B /\
  [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 [HZsgn [Hmem HSum]]]]]] Hret] Ha2].
rewrite /= store.get_r0 u2Z_Z2u // in Hret.
move/eqP : Hret => Hret.
case: HSum => HSum.
  case: HSum => _ [HSum _].
  by rewrite HSum u2Z_Z2u in Hret.
split; last by done.
rewrite /= in Ha2.
move/eqP in Ha2.
rewrite store.get_r0 u2Z_Z2u // in Ha2.
case: HSum => HSum; first by tauto.
case: HSum => _ [_ HSum].
by rewrite HSum u2Z_Z2u in Ha2.

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

rewrite /while.entails => s h [Ha [Hb [Hk [HX [HZsgn 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 [h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]]].
case: Hh1 => A' [A'_nk [Hb [HX [Hk [Ha3 [Hh1 HSum]]]]]].
case: Hh2 => [Ha [HZsgn Hh2]].
exists A', slen.
rewrite Ha3 u2Z_Z2u // HZsgn !Zmult_1_l Zmult_0_l Zplus_0_r.
repeat (split => //).

rewrite slen_not_weird HZsgn; ring.

rewrite (proj2 (Zsgn_pos (Sum nk A - Sum nk B))) //; omega.
rewrite con_assoc_equiv.
Compose_sepcon h2 h1; first by done.
move: Hh1. apply monotony => // h'; by apply mapstos_ext.

apply hoare_prop_m.hoare_stren with (fun s h => Sum nk A < Sum nk B /\
  [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 [HZsgn [Hmem HSum]]]]]] Hret].
rewrite /= store.get_r0 u2Z_Z2u // in Hret.
move/eqP in Hret.
case: HSum => HSum; last first.
  have {HSum}HSum : [ret ]_ s = zero32 by tauto.
  by rewrite HSum u2Z_Z2u in Hret.
split; [tauto | done].

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 /\ 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 A < Sum nk B /\ [a3]_s = zero32 /\
  Sum nk A' = Sum nk B - Sum nk A).

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.
by apply Zlt_le_weak.

move=> s h [Ha [Hb [Hk [HX [HZsgn 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.

move=> s h [h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]]].
case: Hh1 => A' [A'_nk [Hb [HX [Hk [Ha3 [Hh1 HSum]]]]]].
case: Hh2 => Ha [HZsgn Hh2].
exists A'; repeat (split => //).
rewrite con_assoc_equiv.
Compose_sepcon h2 h1; first by done.
rewrite con_com_equiv.
move: Hh1; apply monotony => h' //; by apply mapstos_ext.

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

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

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

move=> s h [A'_nk [Ha [Hb [Hk [HX [Hsgn [Hmem [B_A [Ha3 HSum]]]]]]]]].
case: Hmem => h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
Compose_sepcon h1 h2; first by done.
repeat (split => //).
by apply Zlt_gt.

move=> s h [h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]]].
case : Hh2 => A'_nk [Ha [Hb [Hk [HX [HZsgn [Hh2 [B_A [Ha3 HSum']]]]]]]].
exists (cplt2 slen).
rewrite s2Z_cplt2; last first.
  rewrite weirdE2 slen_not_weird HZsgn; omega.
rewrite Zsgn_Zopp Ha3 u2Z_Z2u // Zmult_0_l Zplus_0_r.
repeat (split => //).
rewrite slen_not_weird HZsgn Zmult_1_l (proj2 (Zsgn_pos (Z_of_nat nk))) //; omega.
rewrite HZsgn Zmult_1_l (proj2 (Zsgn_neg (Sum nk A - Sum nk B))) //; omega.
by Compose_sepcon h1 h2.
rewrite HZsgn Zmult_1_l HSum'; ring.

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 slen) = - 1 /\ [a3]_s = one32 /\
  ((var_e a |--> slen :: ptr :: nil ** int_e ptr |--> A) ** var_e b |--> B) s h).

move=> s h /= [[Ha [Hb [Hk [HX [Ha0 [Ha1' [Ha1'' Hmem]]]]]]] Ha1].
move/Zle_boolP : Ha1 => Ha1.
rewrite /wp_addiu.
repeat reg_upd; repeat (split => //).
case: Ha1'' => Ha1''.
omega.
case: Ha1'' => Ha1''.
omega.
by rewrite -Ha1' Ha1''.
by rewrite add_com add_0 sext_Z2u.
Assert_upd.
move=> s' h' x v /= [] // ?; subst a3; by reg_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 /\
  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 (store.lo s) <= 1 /\
  Zsgn (s2Z slen') * (Sum nk A' + u2Z (store.lo 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 :: List.nil) s h)
  (fun s h => [a3]_s = one32 /\ [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 /\
    (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 B + Sum nk A)).

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

move=> s h /= [Ha [Hb [Hk [HX [Ha0 [Ha1' [Ha3 Hmem]]]]]]].
case: Hmem => h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
case: Hh1 => h11 [h12 [h11_d_h12 [h11_U_h12 [Hh11 Hh12]]]].
Compose_sepcon (h12 +++ h2) h11.
repeat (split=> //).
Compose_sepcon h2 h12; first by done.
move: Hh12. by apply assert_m.mapstos_ext.
done.

move=> s h [h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]]].
case: Hh1 => A' [A'_nk [r_b [HX [Hh1 [Hm HSum]]]]].
case: Hh2 => Ha [HZsgn Hh2].
exists A', slen; repeat (split => //).
rewrite HZsgn Zopp_eq_mult_neg_1_L (proj2 (Zsgn_neg (- Sum nk A - Sum nk B))) //.
move: (min_Sum A nk) => ?; omega.
rewrite con_assoc_equiv .
Compose_sepcon h2 h1; first by done.
rewrite con_com_equiv.
move: Hh1; apply assert_m.monotony => // h'; by apply assert_m.mapstos_ext.
rewrite HZsgn HSum; ring.

apply hoare_mflo'.
move=> s h /= [A' [slen' [A'_nk [r_a [r_b [slen'_nk [HZsgn [Hmem [Hlo HSum]]]]]]]]].
rewrite /wp_mflo.
exists A', slen'.
repeat reg_upd.
repeat (split => //).
Assert_upd.
move=> s' h' x v /= [] // ?; subst a3; by reg_upd.
Qed.

Lemma multi_sub_s_u_triple : forall k a b a0 a1 a2 a3 a4 ret X,
nodup(k, a, b, a0, a1, a2, a3, a4, ret, 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_sub_s_u k a b a0 a1 a2 a3 a4 ret 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 ret X Hregs nk va vb ptr Hnk Hnk' ptr_fit vb_fit A B
  len_A len_B slen slen_no_weird valid_A.
rewrite /multi_sub_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]]]].
by Compose_sepcon h2 h1.

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 Hret]]]] Ha2].
rewrite /= in Ha2.
move/eqP in Ha2.
move: (min_Sum B nk).
case/Z_le_lt_eq_dec => Hsum.
apply (proj2 Hret) in Hsum.
by rewrite Hsum u2Z_Z2u // store.get_r0 u2Z_Z2u // in Ha2.
exists A, slen.
repeat reg_upd; repeat (split => //).
rewrite -Hsum Zminus_0_r; exact valid_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 Hret]]]] Ha2].
rewrite /= negb_involutive in Ha2.
move/Zeq_boolP/u2Z_inj in Ha2.
move: (min_Sum B nk).
case/Z_le_lt_eq_dec => Hsum; last first.
 apply (proj1 Hret) 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_sub_s_u'_triple.
Qed.