Library multi_sub_signed_signed_triple

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

Require Import multi_sub_signed_signed_prg.
Require Import pick_sign_triple multi_add_signed_unsigned_triple multi_sub_signed_unsigned_triple.

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

Lemma multi_sub_s_s_triple : forall rk rx ry a0 a1 a2 a3 a4 ret X Y,
  nodup(rk, rx, ry, a0, a1, a2, a3, a4, ret, X, Y, r0) ->
  forall nk vx vy ptr ptrB, nk <> O -> Z_of_nat nk < 2 ^^ 31 ->
    u2Z ptr + 4 * Z_of_nat nk < Zbeta 1 -> u2Z ptrB + 4 * Z_of_nat nk < Zbeta 1 ->
  forall A B, length A = nk -> length B = nk -> forall slen slenB,
    s2Z slen = Zsgn (s2Z slen) * Z_of_nat nk -> s2Z slenB = Zsgn (s2Z slenB) * Z_of_nat nk ->
    Zsgn (s2Z slen) = Zsgn (Zsgn (s2Z slen) * Sum nk A) ->
    Zsgn (s2Z slenB) = Zsgn (Zsgn (s2Z slenB) * Sum nk B) ->
{{ fun s h => [rx]_s = vx /\ [ry]_s = vy /\ u2Z [rk]_s = Z_of_nat nk /\
    ((var_e rx |--> slen :: ptr :: nil ** int_e ptr |--> A) **
      var_e ry |--> slenB :: ptrB :: nil ** int_e ptrB |--> B) s h }}
 multi_sub_s_s rk rx ry a0 a1 a2 a3 a4 ret X Y
 {{ fun s h => exists A', exists slen', length A' = nk /\
   s2Z slen' = Zsgn (s2Z slen') * Z_of_nat nk /\
   Zsgn (s2Z slen') = Zsgn (Zsgn (s2Z slen) * Sum nk A - Zsgn (s2Z slenB) * Sum nk B) /\
   (var_e rx |--> slen' :: ptr :: nil ** int_e ptr |--> A' **
    var_e ry |--> slenB :: ptrB :: nil ** int_e ptrB |--> B) s h /\
   u2Z ([a3]_ s) <= 1 /\
   Zsgn (s2Z slen') * (Sum nk A' + u2Z ([a3]_ s) * Zbeta nk) =
   Zsgn (s2Z slen) * Sum nk A - Zsgn (s2Z slenB) * Sum nk B }}.
Proof.
move=> rk rx ry a0 a1 a2 a3 a4 ret X Y Hregs nk vx vy ptr ptrB Hnk Hnk' Hptr HptrB
  A B len_A len_B slen slenB Hslen HslenB valid_A valid_B.
rewrite /multi_sub_s_s.

apply hoare_lw_back_alt'' with (fun s h => [rx ]_ s = vx /\ [ry ]_ s = vy /\
  u2Z [rk ]_ s = Z_of_nat nk /\ [Y ]_s = ptrB /\
  (((var_e rx |--> slen :: ptr :: nil ** int_e ptr |--> A) **
    var_e ry |--> slenB :: ptrB :: nil) ** int_e ptrB |--> B) s h).

move=> s h [r_x [r_y [r_k mem]]].
exists ptrB; split.
- rewrite con_assoc_equiv con_com_equiv -mapsto2_mapstos !con_assoc_equiv
    con_com_equiv con_assoc_equiv in mem.
  move: mem. 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 => [rx ]_ s = vx /\ [ry ]_ s = vy /\
  u2Z [rk ]_ s = Z_of_nat nk /\
  [Y ]_s = ptrB /\ [a0]_s = slenB /\ Zsgn (s2Z [a1]_s) = Zsgn (s2Z slenB) /\
  (s2Z [a1]_s = 0 \/ s2Z [a1]_s = 1 \/ s2Z [a1]_s = -1) /\
  (((var_e rx |--> slen :: ptr :: nil ** int_e ptr |--> A) **
    var_e ry |--> slenB :: ptrB :: nil) ** int_e ptrB |--> B) s h).

eapply while.hoare_conseq; last first.

apply (pick_sign_triple _ _ _
  (fun s h => [rx ]_ s = vx /\ u2Z [rk ]_ s = Z_of_nat nk /\ [Y ]_s = ptrB)
  (((var_e rx |--> slen :: ptr :: nil ** int_e ptr |--> A) **
    (add_e (var_e ry) (int_e four32)) |--> ptrB :: nil) ** int_e ptrB |--> B) vy slenB).
by Nodup_nodup r0.
Inde.
apply inde_mapstos => /=; apply nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
by Inde.

move=> s h /= [Hrx [Hry [Rk [HY mem]]]].
rewrite !con_assoc_equiv in mem *.
repeat (split=> //).
by assoc_comm mem.

move=> s h /= [Hry [Ha0 [Ha1 [Ha1' [mem [Hrx [Hrk HY]]]]]]].
rewrite !con_assoc_equiv in mem *.
repeat (split=> //).
by assoc_comm mem.

apply while.hoare_ifte.

apply while.hoare_ifte.

apply hoare_addiu'.

move=> s h [[[r_x [r_y [r_k [r_Y [r_A0 [r_a1 [a0_a1 mem]]]]]]] _] Ha1].
rewrite /= in Ha1.
move/eqP/u2Z_inj in Ha1.
rewrite store.get_r0 in Ha1.
rewrite Ha1 s2Z_u2Z_pos' in r_a1; last by rewrite u2Z_Z2u.
rewrite u2Z_Z2u //= in r_a1.
rewrite /wp_addiu.
exists A, slen.
repeat reg_upd.
rewrite -r_a1 Zmult_0_l Zminus_0_r.
repeat (split => //).
by Assert_upd.
by rewrite add_com add_0 sext_Z2u // u2Z_Z2u.
by rewrite add_com add_0 sext_Z2u // u2Z_Z2u // Zmult_0_l Zplus_0_r.

apply (before_frame
  (fun s h => [ry ]_ s = vy /\ Zsgn (s2Z slenB) = 1 /\
  (var_e ry |--> slenB :: ptrB :: nil) s h )
  (fun s h => [rx ]_ s = vx /\ [Y ]_ s = ptrB /\ u2Z [rk ]_ s = Z_of_nat nk /\
  ((var_e rx |--> slen :: ptr :: nil ** int_e ptr |--> A) ** var_e Y |--> B) s h)
  (fun s h => exists A', exists slen', length A' = nk /\
    [rx ]_ s = vx /\ [Y ]_ s = ptrB /\ s2Z slen' = Zsgn (s2Z slen') * Z_of_nat nk /\
   Zsgn (s2Z slen') = Zsgn (Zsgn (s2Z slen) * Sum nk A - Sum nk B) /\
   (var_e rx |--> slen' :: ptr :: nil ** int_e ptr |--> A' ** var_e Y |--> 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)).

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

move=> s h [[[r_x [r_y [r_k [r_Y [r_A0 [r_a1 [a0_a1 mem]]]]]]] Ha1'] Ha1].
rewrite /= in Ha1'.
move/Zle_boolP in Ha1'.
rewrite /= in Ha1.
move/eqP in Ha1.
rewrite store.get_r0 u2Z_Z2u // in Ha1.
rewrite con_com_equiv -con_assoc_equiv con_com_equiv in mem.
case: mem => h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
Compose_sepcon h2 h1.
repeat (split=> //).
rewrite con_com_equiv in Hh2.
move: Hh2; apply monotony => // h'; by apply mapstos_ext.
repeat (split => //).
case: a0_a1 => a0_a1.
rewrite (_ : 0 = s2Z (Z2s 32 0)) in a0_a1; last by rewrite s2Z_Z2s.
apply s2Z_inj in a0_a1.
by rewrite a0_a1 u2Z_Z2s_pos in Ha1.
case: a0_a1 => a0_a1.
by rewrite -r_a1 a0_a1.
rewrite a0_a1 in Ha1'; omega.

move=> s h.
case=> h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
case: Hh1 => [A' [slen' [len_A' [r_x [r_Y [slen'_nk [HZsgn [mem [Ha3 HSum]]]]]]]]].
case: Hh2 => [r_y [Zsgn_slenB Hh2]].
exists A', slen'.
repeat (split => //).
rewrite HZsgn Zsgn_slenB. f_equal. f_equal. ring.
rewrite con_assoc_equiv con_com_equiv con_assoc_equiv.
Compose_sepcon h2 h1; first by done.
rewrite con_com_equiv.
move: mem; apply monotony => // h'; by apply mapstos_ext.
rewrite HSum Zsgn_slenB. f_equal. ring.

apply (before_frame
  (fun s h => [ry ]_ s = vy /\ Zsgn (s2Z slenB) = -1 /\
  (var_e ry |--> slenB :: ptrB :: nil) s h )
  (fun s h => [rx ]_ s = vx /\ [Y ]_ s = ptrB /\ u2Z [rk ]_ s = Z_of_nat nk /\
  ((var_e rx |--> slen :: ptr :: nil ** int_e ptr |--> A) ** var_e Y |--> B) s h)
  (fun s h => exists A', exists slen', length A' = nk /\ [rx ]_ s = vx /\ [Y ]_ s = ptrB /\
    s2Z slen' = Zsgn (s2Z slen') * Z_of_nat nk /\
    Zsgn (s2Z slen') = Zsgn (Zsgn (s2Z slen) * Sum nk A + Sum nk B) /\
    (var_e rx |--> slen' :: ptr :: nil ** int_e ptr |--> A' ** var_e Y |--> 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)).

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

move=> s h [[r_x [r_y [r_k [r_Y [r_A0 [r_a1 [a0_a1 mem]]]]]]] Ha1].
rewrite /= in Ha1.
move/Zle_boolP in Ha1.
case: a0_a1 => a0_a1.
rewrite a0_a1 in Ha1.
by move: (Ha1 (Zle_refl _)).
case: a0_a1 => a0_a1.
rewrite a0_a1 in Ha1.
exfalso; omega.
rewrite con_com_equiv -con_assoc_equiv con_com_equiv in mem.
case: mem => h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
Compose_sepcon h2 h1.
repeat (split=> //).
rewrite con_com_equiv in Hh2.
move: Hh2; apply monotony => // h'; by apply mapstos_ext.
repeat (split => //).
by rewrite -r_a1 a0_a1.

move=> s h [h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]]].
case: Hh1 => [A' [slen' [len_A' [r_x [r_Y [slen'_nk [HZsgn [mem [Ha3 HSum]]]]]]]]].
case: Hh2 => [r_y [Zsgn_slenB Hh2]].
exists A', slen'; repeat (split => //).
rewrite Zsgn_slenB HZsgn; f_equal. ring.

rewrite con_com_equiv -con_assoc_equiv.
Compose_sepcon h1 h2; last by done.
rewrite con_com_equiv.
move: mem; apply monotony => // h'; by apply mapstos_ext.
rewrite Zsgn_slenB HSum; ring.
Qed.