Library begcd_mips

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 multi_negate_prg.
Require Import pick_sign_prg.
Require Import begcd_mips_prelude_prg begcd_mips_prelude.
Require Import begcd_mips_init.
Require Import begcd_mips_halve.
Require Import begcd_mips_reset.
Require Import begcd_mips_subtract.
Require Import library_interfaces.

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

Require seq_ext.

Ltac local_Reg_unchanged st :=
  match goal with
    |- context [store.get ?rk ?st'] =>
      cutrewrite (store.get rk st' = store.get rk st) ;
        [ assumption |
          symmetry ;
          mips_syntax.Reg_unchanged ;
          simpl mips_frame.modified_regs ;
          Nodup_not_In ; fail ]
  end.

Definition begcd_mips rk rg ru rv ru1 ru2 ru3 rv1 rv2 rv3 rt1 rt2 rt3
  a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 :=
  (multi_one rk rg a0 a1 ;
  prelude_mips rk rg ru rv a0 a1 a2 a3 ;
  init_mips rk ru rv ru1 ru2 ru3 rv1 rv2 rv3 rt1 rt2 rt3 a0 a1 a2 a3 a4 a5 a6 ;
  pick_sign rt3 a0 a1 ;
  while.while (bne a1 r0)
  ( ( (multi_is_even_signed rt3 a0 a1 ;
    while.while (bne a1 r0)
    (halve_mips rk ru rv rt1 rt2 rt3 a0 a1 a2 a3 a4 a5 a6;
      multi_is_even_signed rt3 a0 a1)) ;
    reset_mips rk ru rv ru1 ru2 ru3 rv1 rv2 rv3 rt1 rt2 rt3 a0 a1 a2 a3 a4 a7 a8 a9 ;
    subtract_mips rk ru rv ru1 ru2 ru3 rv1 rv2 rv3 rt1 rt2 rt3 a0 a1 a2 a3 a4 a5 a6 a7 a8);
    pick_sign rt3 a0 a1)
)%mips_cmd.

Ltac local_Var_unchanged_forward v st :=
  match goal with
    | |- context [syntax_m.seplog_m.assert_m.expr_m.store.get v ?st'] =>
      cutrewrite (syntax_m.seplog_m.assert_m.expr_m.store.get v st' =
        syntax_m.seplog_m.assert_m.expr_m.store.get v st);
        [ idtac |
          Var_unchanged ;
          rewrite [syntax_m.seplog_m.modified_vars _]/= ;
          Nodup_not_In ; fail ]
  end.

Lemma begcd_simu : 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 a8 a9,
  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, a8, a9, r0) ->
  0 < vu -> 0 < vv -> vu < Zbeta L -> vv < Zbeta L ->
  sim (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 h => EGCD.uv_init vu vv u v s /\ uv_bound rk st u v s L)%seplog_expr
  (EGCD.TAOCP.begcd g u v u1 u2 u3 v1 v2 v3 t1 t2 t3)
  (begcd_mips rk rg ru rv ru1 ru2 ru3 rv1 rv2 rv3 rt1 rt2 rt3 a0 a1 a2 a3 a4 a5 a6 a7 a8 a9).
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 a8 a9
Hvars Hregs Hvu Hvv vu_max vv_max.
rewrite /sim /EGCD.TAOCP.begcd /begcd_mips.

apply fwd_sim_seq with (fun s st h => EGCD.C1 vu vv u v g s /\ uv_bound rk st u v s L) => //.
- rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm; split.
  + rewrite /EGCD.C1.
    rewrite /EGCD.uv_init in Hcond *.
    move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : exec_pseudo.
    case/syntax_m.seplog_m.exec0_assign_inv => _ ->.
    repeat syntax_m.seplog_m.assert_m.expr_m.Store_upd.
    tauto.
  + rewrite /uv_bound.
    repeat syntax_m.seplog_m.assert_m.expr_m.Store_upd.
    have <- : ([rk]_st = [rk]_ st')%mips_expr.
      mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
    local_Var_unchanged u s.
    local_Var_unchanged v s.
    rewrite /uv_bound in Hcond; tauto.
- apply pfwd_sim_fwd_sim; last by apply safe_termination_one; Nodup_nodup r0.
  rewrite /pfwd_sim => s st h s_st_h Hcond.
  apply pfwd_sim_one.
  + 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.
  + exact s_st_h.
  + exact I.

apply fwd_sim_stren with (fun s st _ => EGCD.C2 vu vv u v g s /\ uv_bound rk st u v s L).
  move=> s st h.
  rewrite /EGCD.C1 /EGCD.C2 /EGCD.uv_init.
  move=> [[[Hu Hv] Hg] Hcond].
  by rewrite Hu Hv Hg !Zmult_1_r.

apply fwd_sim_seq with (fun s st _ => (EGCD.C2 vu vv u v g s /\ EGCD.C3 vu vv u v g s) /\
  uv_bound rk st u v s L) => //.
- rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm.
  split.
    have Htmp : nodup(u,v,g) by rewrite [Equality.sort _]/= in Hvars *; Nodup_nodup O.
    move: (EGCD.TAOCP.prelude_verif2 _ _ _ _ _ Htmp Hvu Hvv) => {Htmp}.
    move/syntax_m.seplog_m.hoare_prop_m.soundness.
    rewrite /while.hoare_semantics.
    case/(_ s syntax_m.seplog_m.assert_m.heap.emp (proj1 Hcond)) => _.
    case/(_ _ _ exec_pseudo) => HC2 Hb.
    split; first by done.
    rewrite /EGCD.C3.
    split; last by apply/negP.
    rewrite /EGCD.C2 in HC2.
    case: HC2 => Hu [Hv [Hg [u_g v_g]]].
    rewrite -Zgcd_mult; last by omega.
    by rewrite Zmult_comm u_g Zmult_comm v_g.
  rewrite /uv_bound in Hcond *.
  have <- : ([rk]_st = [rk]_ st')%mips_expr.
    mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
  repeat (split; first by tauto).
  rewrite /EGCD.prelude in exec_pseudo.
  split.
  + have Hu0 : 0 < ([u ]_ s)%seplog_expr < Zbeta (L - 1) by tauto.
    apply (syntax_m.seplog_m.semop_prop_m.while_preserves _ _ (fun s => 0 < ([u ]_ s)%seplog_expr < Zbeta (L - 1)) _ _ _ _ Hu0 exec_pseudo) => {Hu0} s0 h0 s'0 h'0 Hu0 while_cond.
    case/syntax_m.seplog_m.hoare_prop_m.while_semop_prop_m.exec_seq_inv_Some.
    move=> [s1 h1] [Hs1 Hs'0].
    local_Var_unchanged u s1.
    move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : Hs1.
    case/syntax_m.seplog_m.exec0_assign_inv => ? ?; subst h1 s1.
    syntax_m.seplog_m.assert_m.expr_m.Store_upd.
    rewrite /= /ZIT.t_div; split.
    + apply Zlt_0_Zdiv => //.
      case/andP : while_cond => while_cond _.
      move/Zeq_boolP : while_cond.
      move/Zmod_2_Zeven.
      case/Zeven_ex => uhalf Huhalf.
      rewrite Huhalf in Hu0 *; omega.
    + apply Zle_lt_trans with ([u]_s0)%seplog_expr; last by tauto.
      apply Zdiv_le_upper_bound => //; omega.
  + have Hv0 : 0 < ([v ]_ s)%seplog_expr < Zbeta (L - 1) by tauto.
    apply (syntax_m.seplog_m.semop_prop_m.while_preserves _ _ (fun s => 0 < ([v ]_ s)%seplog_expr < Zbeta (L - 1)) _ _ _ _ Hv0 exec_pseudo) => {Hv0} s0 h0 s'0 h'0 Hv0 while_cond.
    move/syntax_m.seplog_m.semop_prop_m.exec_seq_assoc'.
    case/syntax_m.seplog_m.hoare_prop_m.while_semop_prop_m.exec_seq_inv_Some.
    move=> [s1 h1] [Hs1 Hs0].
    local_Var_unchanged v s1.
    case/syntax_m.seplog_m.hoare_prop_m.while_semop_prop_m.exec_seq_inv_Some : Hs1.
    move=> [s2 h2] [Hs2 Hs1].
    move/syntax_m.seplog_m.semop_prop_m.exec_cmd0_inv : Hs1.
    case/syntax_m.seplog_m.exec0_assign_inv => ? ?; subst h1 s1.
    syntax_m.seplog_m.assert_m.expr_m.Store_upd.
    rewrite /= /ZIT.t_div.
    local_Var_unchanged v s0.
    split.
    + apply Zlt_0_Zdiv => //.
      case/andP : while_cond => _.
      move/Zeq_boolP.
      move/Zmod_2_Zeven.
      case/Zeven_ex => uhalf Huhalf.
      rewrite Huhalf in Hv0 *; omega.
    + apply Zle_lt_trans with ([v]_s0)%seplog_expr; last by tauto.
      apply Zdiv_le_upper_bound => //; omega.
- eapply fwd_sim_stren; last first.
    apply sim_begcd_prelude.
    by rewrite [Equality.sort _]/= in Hvars *; Nodup_nodup O.
    by Nodup_nodup r0.
  move=> s st h [HC2 Hcond] /=.
  rewrite /EGCD.C2 in HC2.
  rewrite /uv_bound in Hcond.
  decompose [and] Hcond; clear Hcond.
  subst L.
  split; last by omega.
  case: HC2 => Hu [Hv [Hg [u_g v_g]]].
  by rewrite u_g.

apply fwd_sim_seq with (fun s st h => EGCD.C2 vu vv u v g s /\ EGCD.C3 vu vv u v g s /\
  EGCD.uivi_init u v u1 u2 u3 v1 v2 v3 s /\ EGCD.ti_init u v t1 t2 t3 s /\
  uv_bound rk st u v s L) => //.
- rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm.
  move: (EGCD.TAOCP.begcd_verif_init _ _ _ _ _ _ _ _ _ _ _ _ _ _ Hvars Hvu Hvv).
  move/syntax_m.seplog_m.hoare_prop_m.soundness.
  rewrite /while.hoare_semantics.
  move/(_ _ _ (proj1 Hcond)).
  move/(_ syntax_m.seplog_m.assert_m.heap.emp).
  case=> _.
  move/(_ _ _ exec_pseudo) => Hcond'.
  repeat (split; first by tauto).
  rewrite /uv_bound.
  have <- : ([rk]_st = [rk]_ st')%mips_expr.
    mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
  local_Var_unchanged u s.
  local_Var_unchanged v s.
  tauto.
- apply fwd_sim_begcd_init => //; by Nodup_nodup r0.

apply fwd_sim_stren with (fun s st h => (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 [u ]_ s [v ]_ 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) /\
uv_bound rk st u v s L)%seplog_expr.
  move=> s st h; split.
  - apply EGCD.TAOCP2.begcd_verif_intermediate_with_bounds_invariant_stren => //.
    exact syntax_m.seplog_m.assert_m.heap.emp.
    repeat (split; first by tauto).
    rewrite /EGCD.C2 in H; apply EGCD.init_bounds; tauto.
  - tauto.

apply fwd_sim_while => //.
- rewrite /inv_R => s st h [s_st_h Hcond] 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.
- rewrite /rela_hoare => s st h Hcond s' exec_pseudo st' h' exec_asm; split.
  + move: (EGCD.TAOCP2.begcd_verif_intermediate_with_bounds_invariant _ _ _ _ _ _ _ _ _ _ _ _ _ _ Hvars Hvu Hvv).
    move/syntax_m.seplog_m.hoare_prop_m.soundness.
    rewrite /while.hoare_semantics.
    move/(_ s syntax_m.seplog_m.assert_m.heap.emp).
    set tmp := (_ /\ _).
    have Htmp : tmp by rewrite /tmp {tmp}; tauto.
    case/(_ Htmp) => {Htmp} _.
    move/(_ _ _ exec_pseudo); tauto.
  + rewrite /uv_bound.
    have <- : ([rk]_st = [rk]_ st')%mips_expr.
      mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
    local_Var_unchanged u s.
    local_Var_unchanged v s.
    tauto.
- assoc_put_in_front t3.
  eapply fwd_sim_b_stren; last by apply fwd_sim_b_pick_sign_bne.
  move=> s st h [] H _; by apply H.

apply fwd_sim_seq with (fun s st h => (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 => //.
- rewrite /rela_hoare => s st h Hcond s' exec_p st' h' exec_c; split.
  + move: (EGCD.TAOCP2.begcd_while_halve _ _ _ _ _ _ _ _ _ _ _ _ _ _ Hvars Hvu Hvv).
    move/syntax_m.seplog_m.hoare_prop_m.soundness.
    rewrite /while.hoare_semantics.
    rewrite /=.
    move/(_ s syntax_m.seplog_m.assert_m.heap.emp).
    set tmp := (_ /\ _).
    have Htmp : tmp by rewrite /tmp {tmp}; tauto.
    case/(_ Htmp) => {Htmp} _.
    move/(_ _ _ exec_p); tauto.
  + rewrite /uv_bound.
    have <- : ([rk]_st = [rk]_ st')%mips_expr.
      mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
    local_Var_unchanged u s.
    local_Var_unchanged v s.
    tauto.
- apply fwd_sim_stren with (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 ([u ]_ s) ([v ]_ 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) /\ uv_bound rk st u v s L) /\
  ([var_e t3 <>e nat_e 0 ]b_ s))%seplog_expr.
  move=> s st h; tauto.
- apply fwd_sim_while => //.
  + rewrite /inv_R.
    move=> s st h [s_st_h Hcond] 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.
  + rewrite /rela_hoare => s st h Hcond s' exec_p st' h' exec_c.
    move: (EGCD.TAOCP2.begcd_while_halve_invariant _ _ _ _ _ _ _ _ _ _ _ _ _ _ Hvars Hvu Hvv).
    move/syntax_m.seplog_m.hoare_prop_m.soundness.
    rewrite /while.hoare_semantics.
    rewrite /=.
    move/(_ s syntax_m.seplog_m.assert_m.heap.emp).
    set tmp := (_ /\ _).
    have Htmp : tmp.
      rewrite /tmp {tmp}.
      split.
      * repeat (split; first by tauto).
        have {Hcond}Hcond : ([var_e t3 <>e nat_e 0 ]b_ s)%seplog_expr by tauto.
        rewrite /= in Hcond.
        by move/Zeq_boolP : Hcond.
      * tauto.
    case/(_ Htmp) => {Htmp} _.
    move/(_ _ _ exec_p) => Htmp.
    split.
      split.
      * tauto.
      * rewrite /uv_bound.
        have <- : ([rk]_st = [rk]_ st')%mips_expr.
          mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
        local_Var_unchanged u s.
        local_Var_unchanged v s.
        tauto.
    apply/Zeq_boolP; tauto.
- assoc_put_in_front t3.
  eapply fwd_sim_b_stren; last by apply fwd_sim_b_multi_is_even_signed.
  move=> s st h [] H _; by apply H.
- apply fwd_sim_stren with (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 ([u ]_ s) ([v ]_ 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) /\ uv_bound rk st u v s L) /\
  ([var_e t3 <>e nat_e 0 ]b_ s)) /\
  ([var_e t3 mode nat_e 2 =e nat_e 0 ]b_ s))%seplog_expr.
  move=> s st h; tauto.
  apply fwd_sim_begcd_halve => //; by Nodup_nodup r0.

apply fwd_sim_seq with (fun s st h =>(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 /\
  (0 <= [t3 ]_ s ->
    Zgcd vu vv = [g ]_ s * Zgcd [t3 ]_ s [v3 ]_ s /\
    Zodd [u3 ]_ s /\ [u3 ]_ s = [t3 ]_ s) /\
  ([t3 ]_ s < 0 ->
    Zgcd vu vv = [g ]_ s * Zgcd [u3 ]_ s [t3 ]_ s /\
    Zodd [v3 ]_ s /\ [v3 ]_ s = - [t3 ]_ s) /\
  EGCD.uivi_bounds u v u1 v1 u2 v2 u3 v3 s /\
  EGCD.ti_bounds u v t1 t2 t3 s /\ EGCD.C5 u3 v3 s) /\
  uv_bound rk st u v s L)%seplog_expr => //.
- rewrite /rela_hoare => s st h Hcond s' exec_p st' h' exec_c; split.
  + move: (EGCD.TAOCP2.begcd_reset _ _ _ _ _ _ _ _ _ _ _ _ _ _ Hvars Hvu Hvv).
    move/syntax_m.seplog_m.hoare_prop_m.soundness.
    rewrite /while.hoare_semantics.
    rewrite /=.
    move/(_ s syntax_m.seplog_m.assert_m.heap.emp).
    set tmp := (_ /\ _).
    have Htmp : tmp.
      rewrite /tmp {tmp}.
      tauto.
    case/(_ Htmp) => {Htmp} _.
    move/(_ _ _ exec_p) => Htmp.
    tauto.
  + rewrite /uv_bound.
    have <- : ([rk]_st = [rk]_ st')%mips_expr.
      mips_syntax.Reg_unchanged. rewrite [mips_frame.modified_regs _]/=; by Nodup_not_In.
    local_Var_unchanged u s.
    local_Var_unchanged v s.
    tauto.
- apply fwd_sim_begcd_reset => //; by Nodup_nodup r0.

apply fwd_sim_begcd_subtract => //; by Nodup_nodup r0.
Qed.