Library multi_lt_triple

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

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

Section multi_lt.

Variables k a b i flag ret ret2 a0 a1 : reg.

Lemma multi_lt_triple : nodup(k, a, b, i, flag, ret, ret2, a0, a1, r0) ->
  forall nk A B va vb, length A = nk -> length B = nk ->
  {{ fun s h => u2Z [ k ]_s = Z_of_nat nk /\ [ a ]_s = va /\ [ b ]_s = vb /\
     (var_e a |--> A ** var_e b |--> B) s h }}
  multi_lt k a b i flag ret ret2 a0 a1
  {{ fun s h => u2Z [ k ]_s = Z_of_nat nk /\ [ a ]_s = va /\ [ b ]_s = vb /\
    (((Sum nk A < Sum nk B /\ [ret]_s = one32 /\ [ret2]_s = zero32) \/
      (Sum nk A > Sum nk B /\ [ret]_s = zero32 /\ [ret2]_s = one32) \/
      (Sum nk A = Sum nk B /\ [ret]_s = zero32 /\ [ret2]_s = zero32)) /\
    (var_e a |--> A ** var_e b |--> B) s h) }}.
Proof.
move=> Hset nk A B va vb HlenA HlenB.
rewrite /multi_lt.

apply hoare_addiu with (fun s h => u2Z [k]_s = Z_of_nat nk /\ [a]_s = va /\
  [b]_s = vb /\ (var_e a |--> A ** var_e b |--> B) s h /\ [i]_s = [k]_s).

move => s h [r_k [r_a [r_b Hmem]]].
rewrite /wp_addiu; repeat reg_upd; repeat (split; trivial).
by Assert_upd.
by rewrite sext_0 add_0.

apply hoare_addiu with (fun s h => u2Z [k]_s = Z_of_nat nk /\ [a]_s = va /\
  [b]_s = vb /\ (var_e a |--> A ** var_e b |--> B) s h /\
  [i]_s = [k]_s /\ [flag]_s = one32).

move=> s h [r_k [r_a [r_b [Hmem r_i]]]].
rewrite /wp_addiu; repeat reg_upd; repeat (split; trivial).
by Assert_upd.
by rewrite add_com add_0 sext_Z2u.

apply while.hoare_ifte.

apply hoare_addiu with (fun s h => u2Z [k]_s = Z_of_nat nk /\ [a]_s = va /\
  [b]_s = vb /\ (var_e a |--> A ** var_e b |--> B) s h /\
  [i]_s = [k]_s /\ [flag]_s = one32 /\ [i]_s = zero32 /\ [ret]_s = zero32).

rewrite /wp_addiu => s h [[r_k [r_a [r_b [Hmem [r_i r_flag]]]]] r_i'].
repeat reg_upd.
have {r_i'}r_i' : [i]_s = zero32.
  move/Zeq_boolP : r_i' => /=.
  move/u2Z_inj => ->.
  by rewrite store.get_r0.
repeat (split; trivial).
by Assert_upd.
by rewrite sext_Z2u // add_0.

apply hoare_addiu'.
move => s h [r_k [r_a [r_b [Hmem [r_i [r_flag [r_i' r_ret]]]]]]].
rewrite /wp_addiu; repeat reg_upd; repeat (split; trivial).
- right; right.
  rewrite -r_i r_i' u2Z_Z2u // in r_k.
  destruct nk; last by done.
  by rewrite sext_Z2u // add_0.
- by Assert_upd.

apply hoare_prop_m.hoare_while_invariant with (fun s h => u2Z [k]_s = Z_of_nat nk /\ [a]_s = va /\
  [b]_s = vb /\ (var_e a |--> A ** var_e b |--> B) s h /\
  exists ni, u2Z [i]_s = Z_of_nat ni /\
    (ni <= nk)%nat /\
    (([flag]_s <> zero32 /\ [i]_s <> zero32 /\
      Sum (nk - ni) (skipn ni A) = Sum (nk - ni) (skipn ni B)) \/
     [flag]_s = zero32 /\
     (([ret]_s = one32 /\ [ret2]_s = zero32 /\
       Sum (nk - ni) (skipn ni A) < Sum (nk - ni) (skipn ni B)) \/
      ([ret]_s = zero32 /\ [ret2]_s = one32 /\
        Sum (nk - ni) (skipn ni A) > Sum (nk - ni) (skipn ni B)) \/
      ([ret]_s = zero32 /\ [i]_s = zero32 /\ [ret2]_s = zero32 /\
       Sum (nk - ni) (skipn ni A) = Sum (nk - ni) (skipn ni B))))).

move=> s h [[r_k [r_a [r_b [Hmem [r_i r_flag]]]]] r_i'].
rewrite /= store.get_r0 u2Z_Z2u // in r_i'; move/Zeq_boolP : r_i' => r_i'.
repeat (split; trivial).
exists nk; split; first by rewrite r_i r_k.
split; first by apply le_refl.
left; split.
- rewrite r_flag; by apply Z2u_dis.
- split.
  + contradict r_i'; by rewrite r_i' u2Z_Z2u.
  + by rewrite -minus_n_n.

move=> s h [ [r_k [r_a [r_b [Hmem [ni [r_i [Hnink [
  [r_flag [r_ret2 Hsum]] |
  [ r_flag [ [r_ret [r_ret2 Hsum] ] |
  [ [r_ret [r_ret2 Hsum]] |
  [gprret [r_i' [r_ret2 Hsum]]]]]]]]]]]]]] Hneq]; rewrite /= in Hneq.
- have {Hneq}Hneq : u2Z [flag]_s = u2Z zero32.
    move/negPn : Hneq; move/Zeq_boolP.
    by rewrite store.get_r0.
  apply u2Z_inj in Hneq; contradiction.
- repeat (split; trivial).
  left; split; last by done.
  by eapply Sum_skipn; eauto.
- repeat (split; trivial).
  right; left; split; last by done.
  apply Zlt_gt.
  apply Zgt_lt in Hsum.
  by eapply Sum_skipn; eauto.
- repeat (split; trivial).
  right; right; split; last by done.
  have ni_O : ni = O .
    symmetry in r_i; move: r_i.
    rewrite r_i' /zero32 u2Z_Z2u //; by move/Z_of_nat_0.
  by rewrite ni_O -minus_n_O in Hsum.

apply hoare_addiu with (fun s h => u2Z [k]_s = Z_of_nat nk /\ [a]_s = va /\
  [b]_s = vb /\ (var_e a |--> A ** var_e b |--> B) s h /\
  exists ni, u2Z [i]_s = Z_of_nat ni /\ (ni < nk)%nat /\
    ([flag]_s <> zero32 /\
      Sum (nk - S ni) (skipn (S ni) A) = Sum (nk - S ni) (skipn (S ni) B))).

move=> s h [ [r_k [ r_a [r_b [Hmem [ni [r_i [Hnink [
  [r_flag [r_i' Hsum] ] |
  [ r_flag [ [r_ret Hsum] |
  [ [r_ret Hsum] |
  [r_ret [r_i' Hsum]]]]]]]]]]]]] Hneq]; rewrite /= in Hneq.
- have X : (1 <= ni)%nat.
    apply not_ge; contradict r_i'.
    apply u2Z_inj; rewrite r_i u2Z_Z2u //.
    apply le_n_0_eq in r_i'; by subst ni.
  rewrite /wp_addiu; repeat reg_upd; repeat (split; trivial).
  + by Assert_upd.
  + exists (ni - 1)%nat; repeat (split; trivial).
    * rewrite sext_Z2s // u2Z_add_Z2s //.
      by rewrite r_i inj_minus1.
      rewrite r_i.
      apply Zle_trans with (1 + -1); first by done.
        apply Zplus_le_compat_r.
        rewrite (_ 1 : 1 = Z_of_nat 1) //.
        by apply inj_le.
    * destruct ni.
      by apply le_Sn_0 in X.
      by rewrite /= -minus_n_O.
    * by rewrite minus_Sn_m //= -minus_n_O.
- move/Zeq_boolP: Hneq; by rewrite r_flag store.get_r0.
- move/Zeq_boolP: Hneq; by rewrite r_flag store.get_r0.
- move/Zeq_boolP: Hneq; by rewrite r_flag store.get_r0.

apply hoare_lwxs_back_alt'' with (fun s h => u2Z [k]_s = Z_of_nat nk /\
  [a]_s = va /\ [b]_s = vb /\ (var_e a |--> A ** var_e b |--> B) s h /\
  exists ni, u2Z [i]_s = Z_of_nat ni /\ (ni < nk)%nat /\
    ([flag]_s <> zero32 /\
      Sum (nk - S ni) (skipn (S ni) A) = Sum (nk - S ni) (skipn (S ni) B)) /\
    [a0]_s = nth ni A zero32).

move=> s h [r_k [r_a [r_b [Hmem [ni [r_i [ni_nk [r_flag Hsum]]]]]]]].
exists (nth ni A zero32); split.
- Decompose_32 A ni A1 A2 HlenA1 HA'; last by rewrite HlenA.
  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 r_i inj_mult Zmult_comm.
- rewrite /update_store_lwxs; repeat reg_upd; repeat (split; trivial).
  by Assert_upd.
  by exists ni.

apply hoare_lwxs_back_alt'' with (fun s h => u2Z [k]_s = Z_of_nat nk /\
  [a]_s = va /\ [b]_s = vb /\ (var_e a |--> A ** var_e b |--> B) s h /\
  exists ni, u2Z [i]_s = Z_of_nat ni /\ (ni < nk)%nat /\
    ([flag]_s <> zero32 /\
      Sum (nk - S ni) (skipn (S ni) A) = Sum (nk - S ni) (skipn (S ni) B)) /\
    [a0]_s = nth ni A zero32 /\ [a1]_s = nth ni B zero32).

move=> s h [r_k [r_a [r_b [Hmem [ni [r_i [ni_nk [[r_flag Hsum] r_a0]]]]]]]].
exists (nth ni B zero32); split.
- Decompose_32 B ni B1 B2 HlenB1 HB'; last by rewrite HlenB.
  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 r_i inj_mult Zmult_comm.
- rewrite /update_store_lwxs; repeat reg_upd; repeat (split; trivial).
  by Assert_upd.
  by exists ni.

apply hoare_sltu with (fun s h => u2Z [k]_s = Z_of_nat nk /\ [a]_s = va /\
  [b]_s = vb /\ (var_e a |--> A ** var_e b |--> B) s h /\
  exists ni, u2Z [i]_s = Z_of_nat ni /\ (ni < nk)%nat /\
    ([flag]_s <> zero32 /\
      Sum (nk - S ni) (skipn (S ni) A) = Sum (nk - S ni) (skipn (S ni) B)) /\
    [a0]_s = nth ni A zero32 /\ [a1]_s = nth ni B zero32 /\
    (([ret]_s = one32 /\ u2Z [a0]_s < u2Z [a1]_s) \/
      ([ret]_s = zero32 /\ u2Z [a0]_s >= u2Z [a1]_s))).

move=> s h [r_k [r_a [r_b [Hmem [ni [r_i [ni_nk [[r_flag [Hsum [r_a0 r_a1]]]]]]]]]]].
rewrite /wp_sltu; repeat reg_upd; repeat (split; trivial).
- by Assert_upd.
- exists ni; repeat (split; trivial).
  case: ifP; move/Zlt_boolP.
  by move=> ?; left.
  by move/Znot_lt_ge; right.

apply hoare_movn with (fun s h => u2Z [k]_s = Z_of_nat nk /\ [a]_s = va /\
  [b]_s = vb /\ (var_e a |--> A ** var_e b |--> B) s h /\
  exists ni, u2Z [i]_s = Z_of_nat ni /\ (ni < nk)%nat /\
    (Sum (nk - S ni) (skipn (S ni) A) = Sum (nk - S ni) (skipn (S ni) B)) /\
    [a0]_s = nth ni A zero32 /\ [a1]_s = nth ni B zero32 /\
    (([ret]_s = one32 /\ [flag]_s = zero32 /\
      u2Z [a0]_s < u2Z [a1]_s) \/
     ([ret]_s = zero32 /\ [flag]_s <> zero32 /\
      u2Z [a0]_s >= u2Z [a1]_s))).

move=> s h [r_k [r_a [r_b [Hmem [ni [r_i [ni_nk [[r_flag HSum]]]]]]]] [r_a0 [r_a1 [ [X1 X2] | [X1 X2]]]]].
- rewrite /wp_movn; repeat reg_upd; split => Hr_ret.
  + repeat (split; trivial).
    * by Assert_upd.
    * exists ni; repeat (split; trivial); by left.
  + rewrite X1 in Hr_ret.
    have {Hr_ret}: u2Z one32 = u2Z zero32 by rewrite Hr_ret.
    by rewrite ?u2Z_Z2u.
- rewrite /wp_movn; repeat reg_upd; split => Hr_ret.
  + done.
  + repeat (split; trivial).
    exists ni; repeat (split; trivial).
    by right.

apply hoare_sltu with (fun s h => u2Z [k]_s = Z_of_nat nk /\ [a]_s = va /\
  [b]_s = vb /\ (var_e a |--> A ** var_e b |--> B) s h /\
  exists ni, u2Z [i]_s = Z_of_nat ni /\ (ni < nk)%nat /\
    Sum (nk - S ni) (skipn (S ni) A) = Sum (nk - S ni) (skipn (S ni) B) /\
    [a0]_s = nth ni A zero32 /\ [a1]_s = nth ni B zero32 /\
    (([ret]_s = one32 /\ [ret2]_s = zero32 /\
        [flag]_s = zero32 /\ u2Z [a0]_s < u2Z [a1]_s) \/
     ([ret]_s = zero32 /\ [ret2]_s = one32 /\
        [flag]_s <> zero32 /\ u2Z [a0]_s > u2Z [a1]_s) \/
     ([ret]_s = zero32 /\ [ret2]_s = zero32 /\
        [flag]_s <> zero32 /\ u2Z [a0]_s = u2Z [a1]_s))).

move=> s h [r_k [r_a [r_b [Hmem [ni [r_i [ni_nk [Hsum [r_a0 [r_a1 [
  [r_ret [r_flag Hneq] ] |
  [r_ret [r_flag Hneq]]]]]]]]]]]]].
- rewrite /wp_sltu; repeat reg_upd; repeat (split; trivial).
  by Assert_upd.
  exists ni; repeat (split; trivial).
  left; split; first by done.
  rewrite Zlt_bool_false //; by apply Zle_ge, Zlt_le_weak.
- rewrite /wp_sltu; repeat reg_upd; repeat (split; trivial).
  by Assert_upd.
  exists ni; repeat (split; trivial).
  right.
  move/Zge_le : Hneq; case/Zle_lt_or_eq => Hneq.
  * left; repeat (split; trivial).
    by rewrite Zlt_bool_true.
    by apply Zlt_gt.
  * right; repeat (split => //).
    rewrite Hneq Zlt_bool_false //; by apply Zle_ge, Zle_refl.

apply hoare_movn with (fun s h => u2Z [k]_s = Z_of_nat nk /\ [a]_s = va /\
  [b]_s = vb /\ (var_e a |--> A ** var_e b |--> B) s h /\
  exists ni, u2Z [i]_s = Z_of_nat ni /\ (ni < nk)%nat /\
    Sum (nk - S ni) (skipn (S ni) A) = Sum (nk -S ni) (skipn (S ni) B) /\
    [a0]_s = nth ni A zero32 /\ [a1]_s = nth ni B zero32 /\
    (([ret]_s = one32 /\ [ret2]_s = zero32 /\ [flag]_s = zero32 /\ u2Z [a0]_s < u2Z [a1]_s) \/
     ([ret]_s = zero32 /\ [ret2]_s = one32 /\ [flag]_s = zero32 /\ u2Z [a0]_s > u2Z [a1]_s) \/
     ([ret]_s = zero32 /\ [ret2]_s = zero32 /\ [flag]_s <> zero32 /\ u2Z [a0]_s = u2Z [a1]_s))).

move=> s h [r_k [r_a [r_b [Hmem [ni [r_i [ni_nk [Hsum [r_a0 [r_a1 [
[r_ret [r_ret2 [r_flag Hneq] ] ] |
[[r_ret [r_ret2 [r_flag Hneq] ] ] |
[r_ret [r_ret2 [r_flag Hneq]]]]]]]]]]]]]]].
- rewrite /wp_movn; repeat reg_upd; split=> r_ret2'.
  + by rewrite r_ret2 in r_ret2'.
  + repeat (split; trivial).
    exists ni; repeat (split; trivial).
    by left.
- rewrite /wp_movn; repeat reg_upd; split=> r_ret2'.
  + repeat (split; trivial).
    by Assert_upd.
    exists ni; repeat (split; trivial).
    by right; left.
  + rewrite r_ret2 in r_ret2'.
    have {r_ret2'} : u2Z one32 = u2Z zero32 by rewrite r_ret2'.
    by rewrite ?u2Z_Z2u.
- rewrite /wp_movn; repeat reg_upd; split => r_ret2'.
  + by rewrite r_ret2 in r_ret2'.
  + repeat (split; trivial).
    exists ni; repeat (split; trivial).
    by right; right.

apply hoare_movz'.

move=> s h [r_k [r_a [r_b [Hmem [ni [r_i [Hnink [Hsum [r_a0 [r_a1 [ [r_ret [r_ret2 [r_flag Hneq]] ] |
[ [r_ret [r_ret2 [r_flag Hneq]] ] |
[r_ret [r_ret2 [r_flag Hneq] ]]]]]]]]]]]]]].
- rewrite /wp_movz; repeat reg_upd; split => r_i'.
  + repeat (split; trivial).
    by Assert_upd.
    exists ni; repeat (split; trivial).
    by apply lt_le_weak.
    right; split; first by done.
    left; split; first by done.
    have ? : ni = O.
      symmetry in r_i; move: r_i.
      rewrite r_i' u2Z_Z2u //; by move/Z_of_nat_0.
    subst ni.
    rewrite -minus_n_O /=.
    destruct nk as [|nk].
    * by move: (lt_irrefl O).
    * split; first by assumption.
      destruct A => //; destruct B => //.
      rewrite /= -minus_n_O in Hsum.
      rewrite /= in r_a0 r_a1.
      rewrite 2!Sum_S Hsum -r_a0 -r_a1; by apply Zplus_lt_compat_r.
  + repeat (split; trivial).
    exists ni; repeat (split; trivial).
    by apply lt_le_weak.
    right; split; first by done.
    left; split; first by done.
    destruct nk as [|nk].
    * by apply lt_n_O in Hnink.
    * split; first by assumption; rewrite /= in Hsum.
      rewrite -minus_Sn_m; last by apply lt_n_Sm_le.
      rewrite (skipn_S zero32); last by rewrite HlenA.
      apply Zgt_lt.
      rewrite -r_a0 Sum_S [skipn _ _]/= (skipn_S zero32); last by rewrite HlenB.
      rewrite [skipn _ _]/= -r_a1 Sum_S Hsum; by apply Zlt_gt, Zplus_lt_compat_r.
- rewrite /wp_movz; repeat reg_upd; split => r_i'.
  + repeat (split; trivial).
    by Assert_upd.
    exists ni; split; first by done.
    split; first by apply lt_le_weak.
    right; split; first by done.
    right; left; split; first by done.
    have ? : ni = O.
      symmetry in r_i; move: r_i.
      rewrite r_i' u2Z_Z2u //; by move/Z_of_nat_0.
    subst ni.
    rewrite /= -minus_n_O.
    rewrite /= in Hsum.
    destruct A.
    * by rewrite -HlenA in Hnink; apply lt_n_O in Hnink.
    * destruct B.
      - by rewrite -HlenB in Hnink; apply lt_n_O in Hnink.
      - rewrite /= in Hsum.
        destruct nk.
        + by apply gt_irrefl in Hnink.
        + split; first by done.
          rewrite /= -minus_n_O in Hsum.
          rewrite /= in r_a0 r_a1.
          rewrite 2!Sum_S Hsum -r_a0 -r_a1; by apply Zlt_gt, Zplus_lt_compat_r, Zgt_lt.
  + repeat (split; trivial).
    exists ni; split; trivial.
    split; first by apply lt_le_weak.
    right; split; first by done.
    right; left; split; first by done.
    rewrite /= in Hsum.
    destruct A.
    * rewrite -HlenA in Hnink; by apply lt_n_O in Hnink.
    * destruct B.
      - rewrite -HlenB in Hnink; by apply lt_n_O in Hnink.
      - split; first by assumption.
        rewrite /= in Hsum.
        rewrite (skipn_S zero32); last by rewrite HlenA.
        apply Zlt_gt.
        rewrite (skipn_S zero32); last by rewrite HlenB.
        have -> : (nk - ni = S (nk - S ni))%nat by rewrite minus_Sn_m.
        simpl skipn; rewrite 2!Sum_S Hsum -r_a0 -r_a1; by apply Zplus_lt_compat_r, Zgt_lt.
- rewrite /wp_movz; repeat reg_upd; split=> r_i'.
  + repeat (split; trivial).
    by Assert_upd.
    exists ni; split; trivial.
    split; first by apply lt_le_weak.
    right; split; first by done.
    right; right; split; first by done.
    split; first by done.
    have ? : ni = O.
      rewrite r_i' u2Z_Z2u // in r_i.
      symmetry in r_i; by move/Z_of_nat_0 : r_i.
    subst ni.
    rewrite /= -minus_n_O.
    rewrite /= in Hsum.
    destruct nk => //; destruct A => //; destruct B => //.
    rewrite /= -minus_n_O in Hsum.
    rewrite /= in r_a0 r_a1.
    by rewrite 2!Sum_S Hsum -r_a0 -r_a1 Hneq.
  + repeat (split; trivial).
    exists ni; split; first by done.
    split; first by apply lt_le_weak.
    left; split; first by done.
    split; first by done.
    rewrite /= in Hsum.
    destruct nk as [|nk].
    * by apply lt_n_O in Hnink.
    * destruct A => //; destruct B => //.
      rewrite /= in Hsum.
      rewrite -minus_Sn_m; last by apply lt_n_Sm_le.
      rewrite (skipn_S zero32); last by rewrite HlenA.
      symmetry.
      rewrite (skipn_S zero32); last by rewrite HlenB.
      rewrite 2!Sum_S Hsum; simpl skipn; by rewrite -r_a0 -r_a1 Hneq.
Qed.

End multi_lt.