Library multi_zero_signed_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_frame mips_tactics mips_contrib mapstos.
Require Import multi_zero_prg multi_zero_triple.

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

Lemma multi_zero_signed_triple : forall rx a0 a1 a2 a3, nodup(rx, a0, a1, a2, a3, r0) ->
  forall nk X vx ptr, length X = nk ->
    u2Z vx + 4 * 2 < Zbeta 1 ->
    u2Z ptr + 4 * Z_of_nat nk < Zbeta 1 ->
  {{ fun s h => [ rx ]_s = vx /\
     (var_e rx |--> Z2u 32 (Z_of_nat nk) :: ptr :: nil ** int_e ptr |--> X) s h }}
  multi_zero_signed rx a0 a1 a2 a3
  {{ fun s h => [ rx ]_s = vx /\
     (var_e rx |--> Z2u 32 (Z_of_nat nk) :: ptr :: nil ** int_e ptr |--> rep zero32 nk) s h }}.
Proof.
move=> rx a0 a1 a2 a3 regs nk X vx ptr len_X vx_fit ptr_fit.
rewrite /multi_zero_signed.

apply mips_contrib.hoare_lw_back_alt'' with (fun s h => [rx ]_ s = vx /\
  (var_e rx |--> Z2u 32 (Z_of_nat nk) :: ptr :: nil ** int_e ptr |--> X) s h /\
  u2Z [ a0 ]_ s = Z_of_nat nk).
move=> s h [Hx mem].
exists (Z2u 32 (Z_of_nat nk)); split.
- rewrite /= assert_m.con_assoc_equiv in mem.
  move: mem; apply assert_m.monotony => // h'.
  apply assert_m.mapsto_ext => //.
  by rewrite sext_Z2u //= add_0.
- rewrite /mips_contrib.update_store_lw.
  repeat reg_upd.
  repeat (split=> //).
  move: mem; apply assert_m.monotony => // h'.
  apply assert_m.mapstos_ext => //=.
  by reg_upd.
  apply assert_m.mapstos_ext => //.
  rewrite u2Z_Z2u // -Zbeta1_Zpower2.
  split; first by apply Zle_0_nat.
  move: (min_u2Z ptr) => ?; omega.

apply mips_contrib.hoare_lw_back_alt'' with (fun s h => [rx ]_ s = vx /\
  (var_e rx |--> Z2u 32 (Z_of_nat nk) :: ptr :: List.nil ** int_e ptr |--> X) s h /\
  u2Z [ a0 ]_ s = Z_of_nat nk /\ [ a1 ]_ s = ptr).
move=> s h [Hx [mem Ha0]].
exists ptr; split.
- rewrite /= assert_m.con_assoc_equiv assert_m.con_com_equiv assert_m.con_assoc_equiv in mem.
  move: mem; apply assert_m.monotony => // h' mem.
  case: mem => h1 [h2 [Hdisj [Hunion [Hh1 [Hh2 H']]]]].
  rewrite /assert_m.emp in H'; subst h2.
  rewrite heap.union_emp_R in Hunion; subst h'.
  move: Hh1; apply assert_m.mapsto_ext => //=.
  by rewrite sext_Z2u //.
- rewrite /mips_contrib.update_store_lw.
  repeat reg_upd.
  repeat (split => //).
  move: mem; apply assert_m.monotony => // h'.
  apply assert_m.mapstos_ext => //=.
  by reg_upd.
  by apply assert_m.mapstos_ext.

apply (before_frame
  (fun s h => [rx ]_ s = vx /\ (var_e rx |--> Z2u 32 (Z_of_nat nk) :: ptr :: nil) s h)
  (fun s h => [a1]_s = ptr /\ u2Z [a0]_s = Z_of_nat nk /\ (var_e a1 |--> X) s h)
  (fun s h => [a1]_s = ptr /\ u2Z [a0]_s = Z_of_nat nk /\ (var_e a1 |--> rep zero32 nk) s h)).

- apply mips_frame.frame_rule.
  apply multi_zero_triple => //; by Nodup_nodup r0.
  by Inde_frame.
  by move=> ?; Inde_mult.
- rewrite /while.entails => s h [Hx [mem [Ha0 Ha1]]].
  case: mem => h1 [h2 [Hdisj [Hunion [Hh1 Hh2]]]].
  Compose_sepcon h2 h1.
  repeat (split=> //).
  move: Hh2; by apply assert_m.mapstos_ext.
  by repeat (split=> //).
- rewrite /while.entails => s h mem.
  case: mem => h1 [h2 [Hdisj [Hunion [[Ha1 [Ha0 Hh1]] [Hrx Hh2]]]]].
  split; first by assumption.
  Compose_sepcon h2 h1; first by done.
  move: Hh1; by apply assert_m.mapstos_ext.
Qed.