Library multi_zero_triple

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

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

Section multi_zero.

Variables k z ext Z_ : reg.

Lemma multi_zero_triple : nodup(k, z, ext, Z_, r0) ->
  forall nk Z vz, length Z = nk -> u2Z vz + 4 * Z_of_nat nk < Zbeta 1 ->
  {{ fun s h => [z]_s = vz /\ u2Z [k]_s = Z_of_nat nk /\ (var_e z |--> Z) s h }}
    multi_zero k z ext Z_
  {{ fun s h => [z]_s = vz /\ u2Z [k]_s = Z_of_nat nk /\
   (var_e z |--> rep zero32 nk) s h }}.
Proof.
move=> Hset nk Z vz HlenZ Hnz.
rewrite /multi_zero.

NextAddiu.
move=> s h [r_z [r_k Hmem]].
rewrite /wp_addiu; repeat reg_upd; repeat (split; trivial).
by Assert_upd.

NextAddiu.
move=> s h [[r_z [r_k Hmem]] r_ext].
rewrite /wp_addiu; repeat reg_upd; repeat (split; trivial).
by Assert_upd.

apply hoare_prop_m.hoare_while_invariant with (fun s h => exists Z, exists next,
  length Z = next /\ u2Z [ext]_s = Z_of_nat next /\ u2Z [k]_s = Z_of_nat nk /\
  (next <= nk)%nat /\ u2Z [Z_]_s = u2Z [z]_s + 4 * Z_of_nat (nk - next) /\
  [z]_s = vz /\ (var_e z |--> rep zero32 (nk - next) ++ Z) s h).

move=> s h [[[r_z [r_k Hmem]] r_Z] r_ext].
exists Z, nk; repeat (split; trivial).
by rewrite r_ext sext_0 add_0.
by rewrite -minus_n_n Zmult_0_r r_Z sext_0 add_0 // Zplus_0_r.
by rewrite -minus_n_n.

move=> {Z HlenZ} s h [[Z [next [len_Z [Hnext [r_k [Hextnk [r_Z [r_z Hmem]]]]]]]] Hext]; rewrite /= in Hext.
repeat (split; trivial).
have {Hext}Hext : next = O.
  move/negPn : Hext; move/Zeq_boolP.
  rewrite Hnext store.get_r0 /zero32 u2Z_Z2u //; by apply Z_of_nat_0.
subst next.
destruct Z; last by done.
by rewrite Hext -minus_n_O -app_nil_end in Hmem.

clear Z HlenZ.

apply hoare_prop_m.hoare_stren with (fun s h => exists Z, exists next,
  length Z = next /\ (O < next <= nk)%nat /\ u2Z [ext]_s = Z_of_nat next /\
  u2Z [k]_s = Z_of_nat nk /\ u2Z [Z_]_s = u2Z [z]_s + 4 * Z_of_nat (nk - next) /\
  [z]_s = vz /\ (var_e z |--> rep zero32 (nk - next) ++ Z) s h).

move=> s h [[Z [next [HlenZ [Hnext [r_k [r_Z [Hextnk [r_z Hmem]]]]]]]] Hext]; rewrite /= in Hext.
have {Hext}Hext : (O < next)%nat.
  move/Zeq_boolP : Hext.
  rewrite Hnext store.get_r0 /zero32 u2Z_Z2u // => Hext.
  apply neq_0_lt.
  contradict Hext; by rewrite -Hext.
by exists Z, next; repeat (split; trivial).

apply hoare_sw_back'' with (fun s h => exists Z, exists next,
  length Z = (next - 1)%nat /\ (O < next <= nk)%nat /\ u2Z [ext]_s = Z_of_nat next /\
  u2Z [k]_s = Z_of_nat nk /\ u2Z [Z_]_s = u2Z [z]_s + 4 * Z_of_nat (nk - next) /\
  [z]_s = vz /\ (var_e z |--> rep zero32 (S nk - next) ++ Z) s h).

move=> s h [Z [next [HlenZ [[Hnext1 Hnext2] [r_ext [r_k [r_Z [r_z Hmem]]]]]]]].

destruct Z as [|hd tl].
rewrite -HlenZ /= in Hnext1; move: (lt_irrefl O); contradiction.

have Htmp : [ add_e (var_e Z_) (int_e (sext 16 zero16)) ]e_ s =
            [ add_e (var_e z) (int_e (Z2u 32 (Z_of_nat (4 * (nk - next))))) ]e_ s.
  rewrite [mult]lock /= -lock sext_0 add_0; apply u2Z_inj.
  rewrite u2Z_add_Z_of_nat.
  by rewrite inj_mult.
  rewrite -Zbeta1_Zpower2 inj_mult inj_minus1 // Zmult_minus_distr_l [Zmult]lock /= -lock r_z; move: (min_u2Z vz) => ?; omega.

exists (int_e hd).

rewrite (decompose_equiv _ _ _ _ _ (len_rep _ _)) // !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'.
exists tl, next; repeat (split; trivial).
by rewrite -HlenZ /= -minus_n_O.
have -> : rep zero32 (S nk - next) = rep zero32 (nk - next) ++ zero32 :: nil by rewrite -rep_last minus_Sn_m.
rewrite app_ass (decompose_equiv _ _ _ _ _ (len_rep _ _)).
assoc_comm H'.
move: H'; apply mapsto_ext => //.
by rewrite /= store.get_r0.

apply hoare_addiu with (fun s h => exists Z, exists next,
  length Z = (next - 1)%nat /\ (O < next <= nk)%nat /\ u2Z [ext]_s = Z_of_nat next /\
  u2Z [k]_s = Z_of_nat nk /\ u2Z [Z_]_s = u2Z [z]_s + 4 * Z_of_nat (S nk - next) /\
  [z]_s = vz /\ (var_e z |--> rep zero32 (S nk - next) ++ Z) s h).

move=> s h [Z [next [HlenZ [Hnext [r_ext [r_k [r_Z [r_z Hmem]]]]]]]].
rewrite /wp_addiu; repeat reg_upd.
exists Z, next; repeat (split; trivial).
rewrite sext_Z2u // u2Z_add_Z2u //.
- rewrite inj_minus1 in r_Z; last by case : Hnext.
- by omegaz.
rewrite -Zbeta1_Zpower2 r_Z r_z inj_minus1; omega.
by Assert_upd.

apply hoare_addiu'.
move=> s h [Z [next [len_Z [[Hnext1 Hnext2] [r_ext [r_k [r_Z [r_z Hmem]]]]]]]].

rewrite /wp_addiu; exists Z, (next - 1)%nat; repeat reg_upd.
rewrite (_ : nk - (next - 1) = S nk - next)%nat; last first.
  destruct next; by [ inversion Hnext1| rewrite /= -minus_n_O].
repeat (split; trivial).

rewrite sext_Z2s // u2Z_add_Z2s //.
by rewrite inj_minus1 // r_ext.
rewrite r_ext.
destruct next; by [ inversion Hnext1| rewrite Z_S /= -Zplus_assoc Zplus_opp_r Zplus_0_r; apply Zle_0_nat].
by apply le_minus_trans.
by Assert_upd.
Qed.

End multi_zero.