Library begcd_mips_reset

Require Import Epsilon.
Require Import ssreflect ssrbool eqtype.
Require Import Arith_ext ZArith_ext Lists_ext.
Require Import machine_int multi_int encode_decode integral_type nodup.
Import MachineInt.
Require Import mips_bipl mips_tactics mips_syntax.
Import mips_bipl.expr_m.
Require Import simu.
Import simu.simu_m.
Require Import begcd.
Require Import pick_sign_prg.
Require Import multi_negate_prg.
Require Import begcd_mips_init.
Require Import library_interfaces.

Local Open Scope machine_int_scope.
Local Open Scope zarith_ext_scope.
Local Open Scope heap_scope.
Local Open Scope nodup_scope.
Local Open Scope assoc_scope.

Definition reset_mips rk ru rv ru1 ru2 ru3 rv1 rv2 rv3 rt1 rt2 rt3 a0 a1 a2 a3 a4 a5 a6 a7 :=
  (pick_sign rt3 a0 a1;
  while.ifte (bgez a1)
  (copy_signed_signed ru1 rt1 a0 a1 a2 a3 a4 ;
   copy_signed_signed ru2 rt2 a0 a1 a2 a3 a4 ;
   copy_signed_signed ru3 rt3 a0 a1 a2 a3 a4)
  ((multi_sub_signed_signed_unsigned rk rv1 rt1 rv a0 a1 a2 a3 a4 a5 a6 a7;
    negate rv1 a0) ;
   (multi_add_signed_signed_unsigned rk rv2 rt2 ru a0 a1 a2 a3 a4 a5 a6 a7;
    negate rv2 a0) ;
   copy_signed_signed rv3 rt3 a0 a1 a2 a3 a4;
   negate rv3 a0
  ))%mips_cmd.

Lemma fwd_sim_begcd_reset : forall vu vv g u v u1 u2 u3 v1 v2 v3 t1 t2 t3 L
  rk rg ru rv ru1 ru2 ru3 rv1 rv2 rv3 rt1 rt2 rt3 a0 a1 a2 a3 a4 a5 a6 a7,
  nodup(g,u,v,u1,u2,u3,v1,v2,v3,t1,t2,t3) ->
  nodup(rk,rg,ru,rv,ru1,ru2,ru3,rv1,rv2,rv3,rt1,rt2,rt3,a0,a1,a2,a3,a4,a5,a6,a7,r0) ->
  0 < vu -> 0 < vv ->
  fwd_sim (state_mint
    (g |=> unsign rk rg \U+ (u |=> unsign rk ru \U+ (v |=> unsign rk rv \U+
    (u1 |=> signed L ru1 \U+ (u2 |=> signed L ru2 \U+ (u3 |=> signed L ru3 \U+
    (v1 |=> signed L rv1 \U+ (v2 |=> signed L rv2 \U+ (v3 |=> signed L rv3 \U+
    (t1 |=> signed L rt1 \U+ (t2 |=> signed L rt2 \U+ t3 |=> signed L rt3))))))))))))
  (fun s st _ => (EGCD.C2 vu vv u v g s /\
    (Zodd ([u ]_ s) \/ Zodd ([v ]_ s)) /\
    EGCD.CVectors u v u1 u2 u3 v1 v2 v3 t1 t2 t3 s /\
    EGCD.C4 u3 v3 t3 s /\
    EGCD.C5 u3 v3 s /\
    Zgcd vu vv = ([g ]_ s) * Zgcd ([u3 ]_ s) ([v3 ]_ s) /\
    EGCD.uivi_bounds u v u1 v1 u2 v2 u3 v3 s /\
    EGCD.ti_bounds u v t1 t2 t3 s /\ Zodd ([t3 ]_ s)) /\
  uv_bound rk st u v s L)%seplog_expr
  (EGCD.TAOCP.reset u v u1 u2 u3 v1 v2 v3 t1 t2 t3)
  (reset_mips rk ru rv ru1 ru2 ru3 rv1 rv2 rv3 rt1 rt2 rt3 a0 a1 a2 a3 a4 a5 a6 a7).
Proof.
move=> vu vv g u v u1 u2 u3 v1 v2 v3 t1 t2 t3 L
rk rg ru rv ru1 ru2 ru3 rv1 rv2 rv3 rt1 rt2 rt3 a0 a1 a2 a3 a4 a5 a6 a7 Hvars Hregs Hvu Hvv.
rewrite /EGCD.TAOCP.reset /reset_mips.
apply fwd_sim_ifte => //.
- rewrite /inv_R => s st h s_st_h st' h' exec_asm; split.
  + eapply state_mint_invariant; [idtac | idtac | apply s_st_h | apply exec_asm] => //.
    Disj_f_cdom2list Permutation_mints_regs.
    rewrite [mips_frame.modified_regs _]/=.
    Disj_remove_dup.
    apply: nodup.nodup_disj. rewrite [List.app _ _]/=. by Nodup_nodup r0.
  + rewrite /uv_bound.
    have <- : ([rk]_st = [rk]_ st')%mips_expr.
      mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
    tauto.
- assoc_put_in_front t3.
  apply fwd_sim_b_pick_sign; by Nodup_nodup r0.
- apply fwd_sim_seq with (fun s st h => True) => //.
  + assoc_put_in_front t1.
    assoc_put_in_front u1.
    apply pfwd_sim_fwd_sim; last by apply safe_termination_copy_signed_signed; Nodup_nodup r0.
    apply pfwd_sim_copy_signed_signed.
    - by Nodup_nodup r0.
    - Disj_f_cdom2list Permutation_mints_regs.
      Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
    - apply/seq_ext.inP.
      Not_In_dom2list.
      apply not_In_mint_ptr. rewrite [mint_ptr _]/= [map _ _]/=. by Nodup_not_In.
    - apply/seq_ext.inP.
      Not_In_dom2list.
      apply not_In_mint_ptr. rewrite [mint_ptr _]/= [map _ _]/=. by Nodup_not_In.
  + apply fwd_sim_seq with (fun s st h => True) => //.
    * assoc_put_in_front t2.
      assoc_put_in_front u2.
      apply pfwd_sim_fwd_sim; last by apply safe_termination_copy_signed_signed; Nodup_nodup r0.
      apply pfwd_sim_copy_signed_signed.
      - by Nodup_nodup r0.
      - Disj_f_cdom2list Permutation_mints_regs.
        Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
      - apply/seq_ext.inP.
        Not_In_dom2list.
        apply not_In_mint_ptr. rewrite [mint_ptr _]/= [map _ _]/=. by Nodup_not_In.
      - apply/seq_ext.inP.
        Not_In_dom2list.
        apply not_In_mint_ptr. rewrite [mint_ptr _]/= [map _ _]/=. by Nodup_not_In.
    * assoc_put_in_front t3.
      assoc_put_in_front u3.
      apply pfwd_sim_fwd_sim; last by apply safe_termination_copy_signed_signed; Nodup_nodup r0.
      apply pfwd_sim_copy_signed_signed.
      - by Nodup_nodup r0.
      - Disj_f_cdom2list Permutation_mints_regs.
        Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
      - apply/seq_ext.inP.
        Not_In_dom2list.
        apply not_In_mint_ptr. rewrite [mint_ptr _]/= [map _ _]/=. by Nodup_not_In.
      - apply/seq_ext.inP.
        Not_In_dom2list.
        apply not_In_mint_ptr. rewrite [mint_ptr _]/= [map _ _]/=. by Nodup_not_In.
- apply fwd_sim_seq with (fun s st h => ([rk ]_ st)%mips_expr <> zero32 /\
   u2Z ([rk ]_ st)%mips_expr < 2 ^^ 31 /\
   L <> 0%nat /\
   L = Zabs_nat (u2Z ([rk ]_ st)%mips_expr) /\
   Zabs ([t2 ]_ s)%seplog_expr < Zbeta (L - 1) /\
   0 <= ([u ]_ s)%seplog_expr < Zbeta (L - 1)) => //.
  + rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm.
    have <- : ([rk]_st = [rk]_ st')%mips_expr.
      mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
    rewrite /uv_bound in Hcond.
    split.
      move=> abs; rewrite abs u2Z_Z2u // in Hcond.
      omega.
    repeat (split; first by tauto).
    rewrite /EGCD.ti_bounds in Hcond.
    local_Var_unchanged t2 s.
    rewrite Zabs_non_eq; last by omega.
    local_Var_unchanged u s.
    omega.
  + apply fwd_sim_pcode_equiv with (v1 <- var_e t1 .-e var_e v ; v1 <- .--e var_e v1)%seplog_expr%seplog_cmd; last first.
    apply equivalent_pseudo_code_trans with (v1 <- .--e (var_e t1 .-e var_e v))%seplog_expr%seplog_cmd.
    by apply equivalent_pseudo_code_example3.
    apply equivalent_pseudo_code_expr => s; rewrite /= /ZIT.t_minus; ring.
    apply fwd_sim_seq with (fun s st h => True) => //.
    * assoc_put_in_front v.
      assoc_put_in_front t1.
      assoc_put_in_front v1.
      apply pfwd_sim_fwd_sim; last by apply safe_termination_multi_sub_signed_signed_unsigned; Nodup_nodup r0.
      apply pfwd_sim_stren with (fun s st _ => [rk ]_ st <> zero32 /\
        u2Z ([rk ]_ st) < 2 ^^ 31 /\
        L <> O /\
        L = Zabs_nat (u2Z ([rk ]_ st)) /\
        Zabs ([t1 ]_ s)%seplog_expr < Zbeta (L - 1) /\
        0 <= ([v ]_ s)%seplog_expr < Zbeta (L - 1))%mips_expr.
        move=> s st h H.
        rewrite /uv_bound in H.
        split.
          move=> abs; rewrite abs u2Z_Z2u // in H; omega.
        repeat (split; first by tauto).
        rewrite /EGCD.ti_bounds in H.
        rewrite Zabs_eq; last by omega.
        omega.
      apply pfwd_sim_multi_sub_signed_signed_unsigned_wo_overflow.
      - rewrite [Equality.sort _]/= in Hvars *. by Nodup_nodup O.
      - by Nodup_nodup r0.
      - Disj_f_cdom2list Permutation_mints_regs.
        Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
      - apply/seq_ext.inP.
        Not_In_dom2list; by Nodup_not_In.
      - apply/seq_ext.inP.
        Not_In_dom2list; by Nodup_not_In.
      - apply/seq_ext.inP.
        Not_In_dom2list.
        by Nodup_not_In.
      - apply/seq_ext.inP.
        Not_In_dom2list.
        apply not_In_mint_ptr. rewrite [mint_ptr _]/= [List.map _ _]/=. by Nodup_not_In.
      - apply/seq_ext.inP.
        Not_In_dom2list.
        apply not_In_mint_ptr. rewrite [mint_ptr _]/= [List.map _ _]/=. by Nodup_not_In.
      - apply/seq_ext.inP.
        Not_In_dom2list.
        apply not_In_mint_ptr. rewrite [mint_ptr _]/= [List.map _ _]/=. by Nodup_not_In.
    * assoc_put_in_front v1.
      apply pfwd_sim_fwd_sim; last by apply safe_termination_negate; Nodup_nodup r0.
      apply pfwd_sim_negate.
      - by Nodup_nodup r0.
      - Disj_f_cdom2list Permutation_mints_regs.
        Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
      - apply/seq_ext.inP.
        Not_In_dom2list; by Nodup_not_In.
      - apply/seq_ext.inP.
        Not_In_dom2list.
        apply not_In_mint_ptr. simpl mint_ptr. simpl List.map. by Nodup_not_In.
  + apply fwd_sim_seq with (fun s st h => True) => //.
    * apply fwd_sim_pcode_equiv with (v2 <- var_e t2 +e var_e u ; v2 <- .--e var_e v2)%seplog_expr%seplog_cmd; last first.
      apply equivalent_pseudo_code_trans with (v2 <- var_e u +e var_e t2 ; v2 <- .--e var_e v2)%seplog_expr%seplog_cmd.
      apply equivalent_pseudo_code_seq; last by done.
      apply equivalent_pseudo_code_expr => s /=; rewrite /ZIT.t_plus; ring.
      by apply equivalent_pseudo_code_example3.
      apply fwd_sim_seq with (fun s st h => True) => //.
      - assoc_put_in_front u.
        assoc_put_in_front t2.
        assoc_put_in_front v2.
        apply pfwd_sim_fwd_sim; last by apply safe_termination_multi_add_signed_signed_unsigned; Nodup_nodup r0.
        apply pfwd_sim_multi_add_signed_signed_unsigned_wo_overflow.
        - rewrite [Equality.sort _]/= in Hvars *. by Nodup_nodup O.
        - by Nodup_nodup r0.
        - Disj_f_cdom2list Permutation_mints_regs.
          Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
        - apply/seq_ext.inP.
          Not_In_dom2list; by Nodup_not_In.
        - apply/seq_ext.inP.
          Not_In_dom2list; by Nodup_not_In.
        - apply/seq_ext.inP.
          Not_In_dom2list.
          by Nodup_not_In.
        - apply/seq_ext.inP.
          Not_In_dom2list.
          apply not_In_mint_ptr. rewrite [mint_ptr _]/= [List.map _ _]/=. by Nodup_not_In.
        - apply/seq_ext.inP.
          Not_In_dom2list.
          apply not_In_mint_ptr. rewrite [mint_ptr _]/= [List.map _ _]/=. by Nodup_not_In.
        - apply/seq_ext.inP.
          Not_In_dom2list.
          apply not_In_mint_ptr. rewrite [mint_ptr _]/= [List.map _ _]/=. by Nodup_not_In.
      - assoc_put_in_front v2.
        apply pfwd_sim_fwd_sim; last by apply safe_termination_negate; Nodup_nodup r0.
        apply pfwd_sim_negate.
        + by Nodup_nodup r0.
        + Disj_f_cdom2list Permutation_mints_regs.
          Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
        + apply/seq_ext.inP.
          Not_In_dom2list; by Nodup_not_In.
        + apply/seq_ext.inP.
          Not_In_dom2list.
          apply not_In_mint_ptr. simpl mint_ptr. simpl List.map. by Nodup_not_In.
    * apply fwd_sim_pcode_equiv with (v3 <- var_e t3 ; v3 <- .--e var_e v3)%seplog_expr%seplog_cmd; last first.
      by apply equivalent_pseudo_code_example3.
      apply fwd_sim_seq with (fun s st h => True) => //.
      - assoc_put_in_front t3.
        assoc_put_in_front v3.
        apply pfwd_sim_fwd_sim; last by apply safe_termination_copy_signed_signed; Nodup_nodup r0.
        apply pfwd_sim_copy_signed_signed.
        - by Nodup_nodup r0.
        - Disj_f_cdom2list Permutation_mints_regs.
          Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
        - apply/seq_ext.inP.
          Not_In_dom2list.
          apply not_In_mint_ptr. rewrite [mint_ptr _]/= [map _ _]/=. by Nodup_not_In.
        - apply/seq_ext.inP.
          Not_In_dom2list.
          apply not_In_mint_ptr. rewrite [mint_ptr _]/= [map _ _]/=. by Nodup_not_In.
      - assoc_put_in_front v3.
        apply pfwd_sim_fwd_sim; last by apply safe_termination_negate; Nodup_nodup r0.
        apply pfwd_sim_negate.
        - by Nodup_nodup r0.
        - Disj_f_cdom2list Permutation_mints_regs.
          Disj_remove_dup. apply: nodup.nodup_disj; rewrite [List.app _ _]/=; by Nodup_nodup r0.
        - apply/seq_ext.inP.
          Not_In_dom2list; by Nodup_not_In.
        - apply/seq_ext.inP.
          Not_In_dom2list.
          apply not_In_mint_ptr. simpl mint_ptr. simpl List.map. by Nodup_not_In.
Qed.