Library multi_is_even_triple

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

Local Open Scope machine_int_scope.
Local Open Scope heap_scope.
Local Open Scope zarith_ext_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_cmd_scope.
Local Open Scope mips_hoare_scope.

Lemma multi_is_even_triple : forall k a ret, nodup(k, a, ret, r0) ->
  forall nk A va, length A = nk ->
  {{ fun s h => u2Z [ k ]_s = Z_of_nat nk /\ [a]_s = va /\ (var_e a |--> A) s h }}
  multi_is_even k a ret
  {{ fun s h =>
    u2Z [ k ]_s = Z_of_nat nk /\ [a]_s = va /\ (var_e a |--> A) s h /\
    (Zeven (Sum nk A) -> [ret]_s = one32) /\ (Zodd (Sum nk A) -> [ret]_s = zero32) }}.
Proof.
move=> k a ret Hset nk A va HlenA.
rewrite /multi_is_even.

apply while.hoare_ifte.

apply hoare_addiu'.
rewrite /wp_addiu => s h [[Hk [Hva Hmem]] /= Hk'].
destruct nk; last by rewrite Hk store.get_r0 u2Z_Z2u in Hk'.
repeat reg_upd; repeat (split => //).
by Assert_upd.
move=> _; by rewrite sext_Z2u // add_com add_0.

apply hoare_lw_back_alt'' with (fun s h => u2Z [k ]_ s = Z_of_nat nk /\ [a ]_ s = va /\
  (var_e a |--> A) s h /\ [ret]_s = List.hd zero32 A).

move=> [s m] h [[Hk [Hva Hpre]] Hk'].
exists (List.hd zero32 A); split.
- rewrite sext_0.
  destruct A as [|hdA tlA].
  + destruct nk => //.
    by rewrite /= Hk u2Z_Z2u in Hk'.
  + rewrite /= in Hpre *.
    case: Hpre => h1 [h2 [Hdisj [Hunion [Hh1 Hh2]]]].
    exists h1, h2; split; first by done.
    split; first by done.
    split; last by done.
    move: Hh1; apply mapsto_ext; last by done.
    by rewrite /= add_0.
- rewrite /update_store_lw; repeat reg_upd; repeat (split; trivial).
  by Assert_upd.

apply hoare_andi with (fun s h =>
  u2Z [k ]_ s = Z_of_nat nk /\ [a ]_ s = va /\ (var_e a |--> A) s h /\
  (Zeven (Sum nk A) -> [ret]_s = zero32) /\ (Zodd (Sum nk A) -> [ret]_s = one32)).

move => [s m] h [Hh [Hva [mem Hret]]].
rewrite /wp_andi; repeat reg_upd.
repeat (split; trivial).
- by Assert_upd.
- move => Hparity.
  have {Hparity}Hparity : Zeven (u2Z [ret]_(s,m)).
    destruct nk => //.
    + rewrite Hret.
      destruct A => //.
      by rewrite u2Z_Z2u.
    + apply Zeven_Sum in Hparity; last by apply lt_O_Sn.
      rewrite -hd_nth_0 in Hparity; last first.
        rewrite HlenA; by apply lt_O_Sn.
      by rewrite -Hret in Hparity.
  apply int_even_and_1 in Hparity.
  by rewrite zext_Z2u.
- move=> Hparity.
  have {Hparity}Hparity : Zodd (u2Z [ret]_(s,m)).
    apply Zodd_Sum in Hparity.
    rewrite Hret hd_nth_0 //.
    destruct nk.
    + destruct A => //.
      by rewrite /= u2Z_Z2u in Hparity.
    + by rewrite HlenA; apply lt_O_Sn.
  apply int_odd_and_1 in Hparity.
  by rewrite zext_Z2u.

apply hoare_xori'.

move=> [s m] h [Hk [Ha [mem [Hpre1 Hpre2]]]].
rewrite /wp_xori; repeat reg_upd; repeat (split; trivial).
- by Assert_upd.
- move/Hpre1 => ->; by rewrite int_xor_comm int_xor_0 zext_Z2u.
- move/Hpre2 => ->; by rewrite zext_Z2u // int_xor_self.
Qed.