Library pick_sign_triple

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

Require Import pick_sign_prg.

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

Lemma pick_sign_triple : forall a a0 a1 P Q va slen, nodup(a, a0, a1, r0) ->
  inde (a1 :: a0 :: nil) Q ->
  inde (a1 :: a0 :: nil) P ->
  {{fun (s : store.t) (h : heap.t) =>
     [a ]_ s = va /\
     (var_e a |~> int_e slen ** Q) s h /\
     P s h}}
  pick_sign a a0 a1
   {{fun (s : store.t) (h : heap.t) =>
     [a ]_ s = va /\
     [a0 ]_ s = slen /\
     Zsgn (s2Z [a1 ]_ s) = Zsgn (s2Z slen) /\
     (s2Z [ a1 ]_ s = 0 \/ s2Z [ a1 ]_ s = 1 \/ s2Z [ a1 ]_s = - 1) /\
     (var_e a |~> int_e slen ** Q) s h /\ P s h
   }}.
Proof.
move=> a a0 a1 P Q va slen Hregs inde_Q inde_P.
rewrite /pick_sign.
apply hoare_lw_back_alt'' with (fun s h =>
  [a ]_ s = va /\ [a0]_s = slen /\ (var_e a |~> int_e slen ** Q) s h /\ P s h).

rewrite /while.entails => s h [r_a [Hmem HP]].
exists slen; split.
- move: Hmem; 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 => //).
  Assert_upd; apply (incl_inde _ _ _ inde_Q); by intuition.
  Assert_upd; apply (incl_inde _ _ _ inde_P); by intuition.

apply while.hoare_ifte.
- apply hoare_addiu' => s h [[a_va [a0_slen [mem HP]]] ].
  move/Zeq_boolP/u2Z_inj => /=.
  rewrite store.get_r0 => a0_0.
  rewrite /wp_addiu.
  repeat reg_upd; repeat (split => //).
  rewrite add_com add_0 -a0_slen a0_0; by rewrite sext_Z2u.
  left; rewrite add_com add_0 sext_Z2u // s2Z_u2Z_pos'; by rewrite u2Z_Z2u.
  Assert_upd. apply (incl_inde _ _ _ inde_Q); by intuition.
  rewrite /inde in inde_P.
  rewrite -(incl_inde _ _ _ inde_P) //.
  by apply incl_refl.
  rewrite /=; by auto.
- apply mips_contrib.hoare_srl with (fun s h => ([a ]_ s = va /\
  [a0 ]_ s = slen /\ bZsgn (u2Z [a1]_s) = Zsgn (s2Z slen) /\
  (var_e a |~> int_e slen ** Q) s h /\ P s h)).

  rewrite /while.entails => s h [[r_a [r_a0 [Hmem HP]]] a0_0].
  rewrite /mips_seplog.wp_srl.
  repeat reg_upd; repeat (split => //).
  rewrite r_a0 u2Z_Z2u // (_ : Zabs_nat 31 = power 2 5 - 1)%nat //.
  apply (@bZsgn_Zsgn_s2Z 5 slen).
  rewrite -r_a0.
  rewrite /= in a0_0.
  move/Zeq_boolP : a0_0.
  by rewrite store.get_r0 u2Z_Z2u //.
  Assert_upd. apply (incl_inde _ _ _ inde_Q); by intuition.
  rewrite /inde in inde_P.
  rewrite -(incl_inde _ _ _ inde_P) //.
  by apply incl_refl.
  rewrite /=; by auto.

  apply while.hoare_ifte.
  + apply hoare_addiu' => s h [[a_va [a0_slen [sgn_a1 [mem HP]]]] Ha1].
    rewrite /wp_addiu.
    repeat reg_upd; repeat (split => //).
    rewrite add_com add_0 sext_Z2u // s2Z_u2Z_pos'; last by rewrite u2Z_Z2u.
    rewrite u2Z_Z2u //=.
    rewrite /= in Ha1.
    move/Zeq_boolP : Ha1.
    by rewrite store.get_r0 u2Z_Z2u // => Ha1; rewrite Ha1 /bZsgn /= in sgn_a1.
    right; left.
    rewrite add_com add_0 sext_Z2u //.
    rewrite s2Z_u2Z_pos'; by rewrite u2Z_Z2u.
    Assert_upd. apply (incl_inde _ _ _ inde_Q); by intuition.
    rewrite /inde in inde_P.
    rewrite -(incl_inde _ _ _ inde_P) //.
    by apply incl_refl.
    rewrite /=; by auto.

  + apply hoare_addiu' => s h [[a_va [a0_slen [sgn_a1 [mem HP]]]] Ha1].
    rewrite /wp_addiu.
    repeat reg_upd; repeat (split => //).
    rewrite add_com add_0 sext_Z2s //.
    rewrite /= in Ha1.
    move/Zeq_boolP : Ha1.
    rewrite store.get_r0 u2Z_Z2u //.
    move/Zeq_boolP => Ha1.
    rewrite /bZsgn (negbTE Ha1) in sgn_a1.
    rewrite -sgn_a1.
    by rewrite s2Z_Z2s //.

    right; right.
    rewrite add_com add_0 sext_Z2s //.
    by rewrite s2Z_Z2s.
    Assert_upd. apply (incl_inde _ _ _ inde_Q); by intuition.
    rewrite /inde in inde_P.
    rewrite -(incl_inde _ _ _ inde_P) //.
    by apply incl_refl.
    rewrite /=; by auto.
Qed.