Library begcd

Require Import Psatz.
Require Import ssreflect ssrbool eqtype.
Require Import Arith_ext ZArith_ext Lists_ext.
Require Import integral_type nodup.

Ltac myomega := first [lia | omega].

Require Import simu.
Import simu.simu_m.

Ltac local_Var_unchanged 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 |
          symmetry;
          Var_unchanged ;
          rewrite [syntax_m.seplog_m.modified_vars _]/= ;
          Nodup_not_In ; fail ]
  end.

Ltac Not_In_dom2list :=
  match goal with
    | |- ~ In _ (seq_ext.s2l (assoc.dom _)) =>
      let hypo := fresh in
      assoc.From_dom_to_list hypo ;
      simpl in hypo ;
      apply (Permutation_notin _ _ _ hypo) ;
      clear hypo
    | |- ~ In _ (seq_ext.s2l (assoc.cdom _)) =>
      let hypo := fresh in
      assoc.From_cdom_to_list hypo ;
      simpl in hypo ;
      apply (Permutation_notin _ _ _ hypo) ;
      clear hypo
  end.

Ltac Disj_f_cdom2list K :=
  match goal with
    | |- Lists_ext.disj _ (?f (seq_ext.s2l (assoc.cdom _))) =>
      let hypo := fresh in
      assoc.From_cdom_to_list hypo ;
      simpl in hypo ;
      let subgoal := fresh in
      cut ( (Permutation_preserving f) );
        [ intro subgoal ;
          apply subgoal in hypo ;
          apply (Permutation_disj_R _ _ _ hypo) ;
          clear hypo ;
          simpl f
          |
            exact K
        ]
    | |- Lists_ext.disj (?f (seq_ext.s2l (assoc.cdom _))) _ =>
      let hypo := fresh in
      assoc.From_cdom_to_list hypo ;
      simpl in hypo ;
      let subgoal := fresh in
      cut (Permutation_preserving f) ;
        [ intro subgoal ;
          apply subgoal in hypo ;
          apply (Permutation_disj_L _ _ _ hypo) ;
          clear hypo ;
          simpl f
          |
            exact K
        ]
  end.

Module EGCD.

Import syntax_m.seplog_m.assert_m.expr_m.
Import syntax_m.seplog_m.assert_m.
Import syntax_m.seplog_m.

Local Open Scope seplog_cmd_scope.
Local Open Scope seplog_expr_scope.
Local Open Scope nodup_scope.
Local Open Scope zarith_ext_scope.

Lemma div_e_exact_full_2 : forall e s,
  [ e ]e_ s mod 2 = 0 -> 2 * [ e ./e nat_e 2 ]e_s = [ e ]e_s.

Definition prelude x y g :=
  while.while (var_e x mode nat_e 2 =e nat_e O &e var_e y mode nat_e 2 =e nat_e O) (
    x <- var_e x ./e nat_e 2 ;
    y <- var_e y ./e nat_e 2 ;
    g <- var_e g *e nat_e 2 ).

Local Open Scope seplog_hoare_scope.

Module BGCD_HAC.

Definition bgcd g x y t :=
  g <- nat_e 1 ;
  prelude x y g ;
  while.while (var_e x >> nat_e 0) (
    while.while (var_e x mode nat_e 2 =e nat_e 0) ( x <- var_e x ./e nat_e 2 ) ;
    while.while (var_e y mode nat_e 2 =e nat_e 0) ( y <- var_e y ./e nat_e 2 ) ;
    t <- (uop_e valabs_e (var_e x .-e var_e y)) ./e nat_e 2 ;
    ifte (var_e x >>= var_e y) thendo
      (x <- var_e t)
    elsedo
      (y <- var_e t)
  ).

Section bgcd_hac.

Variables x y g t : ssrnat.nat_eqType.
Variables vx vy : Z.

Lemma prelude_verif : nodup(x, y, g) -> 0 <= vx -> 0 <= vy ->
  {{ fun s _ => 0 <= [ x ]_s /\ 0 <= [ y ]_s /\ 0 <= [ g ]_s /\
    [ x ]_ s * [ g ]_ s = vx /\ [ y ]_ s * [ g ]_ s = vy }}
  prelude x y g
  {{ fun s _ => 0 <= [ x ]_ s /\ 0 <= [ y ]_ s /\ 0 <= [ g ]_ s /\
    [ x ]_ s * [ g ]_ s = vx /\ [ y ]_ s * [ g ]_ s = vy /\
    ~~ [ (var_e x mode nat_e 2 =e nat_e 0) &e (var_e y mode nat_e 2 =e nat_e 0) ]b_ s }}.
Proof.
move=> Hset Hvx Hvy.
apply hoare_prop_m.hoare_while_invariant with (fun s _ =>
  0 <= [ x ]_ s /\ 0 <= [ y ]_ s /\ 0 <= [ g ]_ s /\
  [ x ]_ s * [g ]_ s = vx /\ [ y ]_ s * [ g ]_ s = vy ).
by move=> s h /= [H1 [H2 [H3 [H4 H5]]]].
by move=> s h /= [[H1 [H2 [H3 [H4 H5]]]] H6].

apply hoare_assign with (fun s h => 0 <= [ x ]_s /\ 0 <= [ y ]_s /\ 0 <= [ g ]_s /\
  2 * [ x ]_s * [ g ]_s = vx /\ [ y ]_s * [ g ]_s = vy /\ [ y ]_s mod 2 = 0).
move=> s h [[H1 [H2 [H3 [H4 H5]]]] H6].
rewrite /wp_assign.
repeat Store_upd => //.
split; first by apply Z_div_pos.
repeat (split; first by assumption).
split.
- rewrite div_e_exact_full_2 //; by rewrite /hoare_m.eval_b in H6; omegab.
  split; first by assumption.
- by rewrite /hoare_m.eval_b in H6; omegab.

apply hoare_assign with (fun s h => 0 <= [ x ]_s /\ 0 <= [ y ]_s /\ 0 <= [ g ]_s /\
  2 * [ x ]_s * [ g ]_s = vx /\ 2 * [ y ]_s * [ g ]_ s = vy).
move=> s h [H1 [H2 [H3 [H4 [H5 H6]]]]].
rewrite /wp_assign; repeat Store_upd => //.
split; first by assumption.
split; first by apply Z_div_pos.
repeat (split; first by assumption).
by rewrite div_e_exact_full_2.

apply hoare_assign'.
move=> s h [H1 [H2 [H3 [H4 H5]]]].
rewrite /wp_assign; repeat Store_upd => //.
repeat (split; first by assumption).
split; first by apply Zmult_le_0_compat.
split; rewrite /= -?H4 -?H5 /ZIT.t_mult; ring.
Qed.

Lemma bgcd_verif : nodup(x, y, g, t) -> 0 <= vx -> 0 <= vy ->
  {{ fun s h => [x]_s = vx /\ [y]_s = vy }}
  bgcd g x y t
  {{ fun s h => 0 <= [ x ]_s /\ 0 <= [ y ]_s /\ 0 <= [ g ]_s /\
    Zis_gcd vx vy ([ g ]_s * [y]_s)}}.
Proof.
move=> Hset Hvx Hvy.
rewrite /bgcd.

apply hoare_assign with (fun s _ => [x ]_ s = vx /\ [y ]_ s = vy /\ [g ]_ s = 1).
move=> s h; rewrite /wp_assign; move=> [Hx Hy].
by repeat Store_upd => //.

apply while.hoare_seq with (fun s _ =>
  0 <= [x]_s /\ 0 <= [y]_s /\ 0 <= [g]_s /\
  Zgcd vx vy = [g]_s * Zgcd ([x]_s) ([y]_s) /\
  ~ [ ((var_e x mode nat_e 2) =e nat_e O) &e ((var_e y mode nat_e 2) =e nat_e O) ]b_ s).
have Hset' : nodup(x, y, g).
  rewrite [Equality.sort _]/= in Hset *; by Nodup_nodup O.
eapply while.hoare_conseq; last by apply (prelude_verif Hset' Hvx Hvy).
- move=> s h /= [H1 [H2 [H3 [H4 [H5 H6]]]]].
  repeat (split => //).
  + rewrite -H4 -H5.
    apply Zis_gcd_gcd; last first.
      rewrite (Zmult_comm [x]_s) (Zmult_comm [y]_s).
      by apply Zis_gcd_mult, Zgcd_is_gcd.
    apply Zmult_le_0_compat => //; by apply Zgcd_is_pos.
  + by move/negP: H6.
- move=> s h /= [-> [-> ->]]; by rewrite 2!Zmult_1_r.

apply hoare_prop_m.hoare_while_invariant with (fun s _ => 0 <= [x]_s /\ 0 <= [y]_s /\ 0 <= [g]_s /\
  (Zodd [x]_s \/ Zodd [y]_s) /\
  Zgcd vx vy = [g]_s * Zgcd ([x]_s) ([y]_s)).
- move=> s h [Hx_pos [Hy_pos [Hg_pos [H1 H2]]]].
  repeat (split => //).
  rewrite /= in H2.
  move/negP : H2.
  rewrite negb_and.
  case/orP ;
    move/Zeq_boolP ;
    move/not_Zmod_2_Zodd ;
    by auto.
- move=> s h [[Hx_pos [Hy_pos [Hg_pos [Hparity Hgcd]]]] Hx].
  repeat (split; first by assumption).
  have {Hx} : [x ]_ s = 0.
    move: Hx.
    rewrite /hoare_m.eval_b /= ZIT.t_gt_t_ge.
    move/ZIT.t_geb_true.
    rewrite /ZIT.t_ge => ?; by myomega.
  rewrite /= => Hx.
  rewrite Hx /= Zabs_eq // in Hgcd.
  rewrite -Hgcd.
  by apply Zgcd_is_gcd.

apply while.hoare_seq with (fun s _ => 0 <= [x ]_ s /\ 0 <= [y ]_ s /\ 0 <= [g ]_ s /\
  Zodd [x]_s /\
  Zgcd vx vy = [g ]_ s * Zgcd [x ]_ s [y ]_ s).
- apply hoare_prop_m.hoare_while_invariant with (fun s _ =>
    0 <= [x ]_ s /\ 0 <= [y ]_ s /\ 0 <= [g ]_ s /\
    (Zodd [x ]_ s \/ Zodd [y ]_ s) /\
    Zgcd vx vy = [g ]_ s * Zgcd [x ]_ s [y ]_ s).
  + by move=> s h /= [[H2 [H3 [H4 [H5 H6]]]] H1].
  + move=> s h /= [[H2 [H3 [H4 [H5 H6]]]]] //.
    move/Zeq_boolP.
    by move/not_Zmod_2_Zodd.
  + apply hoare_assign' => s h /= [[H2 [H3 [H4 [H5 H6]]]] H1].
    rewrite /wp_assign; repeat Store_upd => //.
    split; first by apply Z_div_pos.
    do 2 split => //.
    case: H5 => H5.
    * move/Zeq_boolP : H1.
      move/Zmod_2_Zeven.
      by move/Zeven_not_Zodd.
    * split; first by auto.
      rewrite /= -Zgcd_even_odd //.
      move/Zeq_boolP : H1.
      by move/Zmod_2_Zeven.
- apply while.hoare_seq with (fun s _ => 0 <= [x ]_ s /\ 0 <= [y ]_ s /\ 0 <= [g ]_ s /\
  Zodd [x ]_ s /\ Zodd [y]_s /\
  Zgcd vx vy = [g ]_ s * Zgcd [x ]_ s [y ]_ s).
  + apply hoare_prop_m.hoare_while_invariant with (fun s _ =>
    0 <= [x ]_ s /\ 0 <= [y ]_ s /\ 0 <= [g ]_ s /\
    Zodd [x ]_ s /\ Zgcd vx vy = [g ]_ s * Zgcd [x ]_ s [y ]_ s) => //.
    * move=> s h /= [[H2 [H3 [H4 [H5 H6]]]] H1].
      repeat (split => //).
      move/Zeq_boolP : H1.
      by move/not_Zmod_2_Zodd.
    * apply hoare_assign' => s h /= [[H2 [H3 [H4 [H5 H6]]]] H1].
      rewrite /wp_assign; repeat Store_upd => //.
      split; first by assumption.
      split; first by apply Z_div_pos.
      repeat (split; first by assumption).
      rewrite /= (Zgcd_sym [x]_s) -Zgcd_even_odd //.
      by rewrite (Zgcd_sym [y]_s).
      move/Zeq_boolP : H1; by move/Zmod_2_Zeven.
+ apply hoare_assign with (fun s _ => (0 <= [x ]_ s /\ 0 <= [y ]_ s /\ 0 <= [g ]_ s /\
    Zodd [x ]_ s /\ Zodd [y]_s /\
    Zgcd vx vy = [g ]_ s * Zgcd [x ]_ s [y ]_ s /\
    [t]_s = Zabs ([x]_s - [y]_s) / 2)).
  move=> s h /= [Hx_pos [Hy_pos [Hg_pos [Hx [Hy Hgcd]]]]].
  by rewrite /wp_assign; repeat Store_upd.
  apply while.hoare_ifte.
  + apply hoare_assign'.
    move=> s h /= [[Hx_pos [Hy_pos [Hg_pos [Hx [Hy [Hgcd Ht]]]]]] Hcond].
    rewrite /wp_assign; repeat Store_upd => //.
    split.
    * rewrite /= Ht.
      apply Z_div_pos => //; by apply Zabs_pos.
    * repeat (split; first by assumption).
      split; first by right.
      rewrite /= Ht Zabs_eq; last first.
        rewrite /ZIT.t_geb in Hcond.
        move/Zge_bool_true : Hcond => ?; by myomega.
      rewrite -Zgcd_even_odd //; last first.
        apply Zodd_plus_Zodd => //; by apply Zodd_opp.
      by rewrite -Zgcd_minus.
  - apply hoare_assign' => s h /= [[Hx_pos [Hy_pos [Hg_pos [Hx [Hy [Hgcd Ht]]]]]] Hcond].
    rewrite /wp_assign; repeat Store_upd => //.
    split; first by done.
    split.
    * rewrite /= Ht.
      apply Z_div_pos => //; by apply Zabs_pos.
    * split; first by done.
      split; first by left.
      rewrite /= Ht Zabs_non_eq; last first.
        rewrite /ZIT.t_geb in Hcond.
        move/negbTE : Hcond.
        move/Zge_bool_false => ?; by myomega.
      rewrite Zopp_plus_distr Zopp_involutive Zplus_comm (Zgcd_sym [x]_s) -Zgcd_even_odd //; last first.
        apply Zodd_plus_Zodd => //; by apply Zodd_opp.
      by rewrite -Zgcd_minus (Zgcd_sym [y]_s).
Qed.

End bgcd_hac.

End BGCD_HAC.

Module BEGCD_HAC.

Definition inner_loop u x y A B :=
  while.while (var_e u mode nat_e 2 =e nat_e O) (
    u <- var_e u ./e nat_e 2 ;
    ifte (var_e A mode nat_e 2 =e nat_e O &e var_e B mode nat_e 2 =e nat_e O) thendo
     ( A <- var_e A ./e nat_e 2 ;
       B <- var_e B ./e nat_e 2 )
    elsedo
     ( A <- (var_e A +e var_e y) ./e nat_e 2 ;
       B <- (var_e B .-e var_e x) ./e nat_e 2 )
    ).

Definition branch u v A B C D :=
  u <- var_e u .-e var_e v ;
  A <- var_e A .-e var_e C ;
  B <- var_e B .-e var_e D.

Definition outer_loop u v x y A B C D :=
  while.while (var_e u >> nat_e 0) (
    inner_loop u x y A B;
    inner_loop v x y C D;
    ifte (var_e u >>= var_e v) thendo
      branch u v A B C D
    elsedo
      branch v u C D A B
  ).

Definition begcd g x y u v A B C D :=
  g <- nat_e 1 ;
  prelude x y g ;
  u <- var_e x ;
  v <- var_e y ;
  A <- nat_e 1 ;
  B <- nat_e O ;
  C <- nat_e O ;
  D <- nat_e 1 ;
  outer_loop u v x y A B C D.

Lemma inner_loop_verif : forall (x y g u v : ssrnat.nat_eqType) vx vy (A B C D : bipl.var.v),
  nodup(x, y, g, u, v, A, B, C, D) ->
  {{fun s _ => 0 <= [x ]_ s /\ 0 <= [y ]_ s /\ 0 <= [g ]_ s /\ 0 <= [u ]_ s /\ 0 <= [v ]_ s /\
    [ x ]_ s * [ g ]_ s = vx /\ [y ]_ s * [g ]_ s = vy /\
    [ A ]_ s * [ x ]_ s + [B ]_ s * [y ]_ s = [u ]_ s /\
    [ C ]_ s * [ x ]_ s + [D ]_ s * [y ]_ s = [v ]_ s /\
    Zgcd vx vy = [g ]_ s * Zgcd [u ]_ s [v ]_ s /\
    (Zodd [x]_s \/ Zodd [y]_s) /\
    (Zodd [u]_s \/ Zodd [v]_s) }}
  inner_loop u x y A B
  {{fun s _ => 0 <= [x ]_ s /\ 0 <= [y ]_ s /\ 0 <= [g ]_ s /\ 0 <= [u ]_ s /\ 0 <= [v ]_ s /\
     [x ]_ s * [g ]_ s = vx /\ [y ]_ s * [g ]_ s = vy /\
    [ A ]_ s * [ x ]_ s + [B ]_ s * [y ]_ s = [u ]_ s /\
    [ C ]_ s * [ x ]_ s + [ D ]_ s * [y ]_ s = [v ]_ s /\
    Zgcd vx vy = [g ]_ s * Zgcd [u ]_ s [v ]_ s /\
    (Zodd [ x ]_s \/ Zodd [ y ]_s) /\
    Zodd [ u ]_s }}.
Proof.
move=> x y g u v vx vy A B C D Hset.
apply hoare_prop_m.hoare_while_invariant with (fun s _ =>
  0 <= [x ]_ s /\ 0 <= [y ]_ s /\ 0 <= [g ]_ s /\ 0 <= [u ]_ s /\ 0 <= [v ]_ s /\
  [x ]_ s * [g ]_ s = vx /\ [y ]_ s * [g ]_ s = vy /\
  [A ]_ s * [x ]_ s + [B ]_ s * [y ]_ s = [u ]_ s /\
  [C ]_ s * [x ]_ s + [D ]_ s * [y ]_ s = [v ]_ s /\
  Zgcd vx vy = [g ]_ s * Zgcd [u ]_ s [v ]_ s /\
  (Zodd [x]_s \/ Zodd [y]_s) /\
  (Zodd [u]_s \/ Zodd [v]_s)).
move=> s h /= [H2 [H3 [H4 [H5 [H6 [H7 [H8 [H9 [H10 [H11 [H12 H13]]]]]]]]]]].
by intuition.
move=> s h /= [[H2 [H3 [H4 [H5 [H6 [H7 [H8 [H9 [H10 [H11 [H12 H13]]]]]]]]]]] H1].
repeat (split => //).
move/ZIT.tP : H1.
by move/not_Zmod_2_Zodd.

apply hoare_assign with (fun s _ =>
  0 <= [x ]_ s /\ 0 <= [y ]_ s /\ 0 <= [g ]_ s /\ 0 <= [u ]_ s /\ 0 <= [v ]_ s /\
  [x ]_ s * [g ]_ s = vx /\ [y ]_ s * [g ]_ s = vy /\
  [A ]_ s * [x ]_ s + [B ]_ s * [y ]_ s = [u ]_ s * 2 /\
  [C ]_ s * [x ]_ s + [D ]_ s * [y ]_ s = [v ]_ s /\
  Zgcd vx vy = [g ]_ s * Zgcd [u ]_ s [v ]_ s /\
  (Zodd [x]_s \/ Zodd [y]_s) /\
  Zodd [v]_s).
move=> s h /= [[H2 [H3 [H4 [H5 [H6 [H7 [H8 [H9 [H10 [H11 [H12 H13]]]]]]]]]]] H1].
rewrite /wp_assign; repeat Store_upd.
move/Zeq_boolP : H1; move/Zmod_2_Zeven => H1.
repeat (split => //).
by apply Z_div_pos.
rewrite /= /ZIT.t_div.
case/Zeven_ex : H1 => u' H1.
by rewrite H1 (Zmult_comm 2) Z_div_mult_full // -(Zmult_comm 2) H9.
rewrite -Zgcd_even_odd //.
case: H13 => //.
by move/Zeven_not_Zodd.
case: H13 => //.
by move/Zeven_not_Zodd.

apply while.hoare_ifte.
-

  apply hoare_assign with (fun s _ =>
    0 <= [x ]_ s /\ 0 <= [y ]_ s /\ 0 <= [g ]_ s /\ 0 <= [u ]_ s /\ 0 <= [v ]_ s /\
    [x ]_ s * [g ]_ s = vx /\ [y ]_ s * [g ]_ s = vy /\
    [A ]_ s * [x ]_ s * 2 + [B ]_ s * [y ]_ s = [u ]_ s * 2 /\
    [C ]_ s * [x ]_ s + [D ]_ s * [y ]_ s = [v ]_ s /\
    Zgcd vx vy = [g ]_ s * Zgcd [u ]_ s [v ]_ s /\
    (Zodd [x]_s \/ Zodd [y]_s) /\
    Zodd [v ]_ s /\
    eval_b (var_e B mode nat_e 2 =e nat_e 0) s).
  move=> s h /= [[H2 [H3 [H4 [H5 [H6 [H7 [H8 [H9 [H10 [H11 [H12 H13]]]]]]]]]]] H1].
  rewrite /wp_assign.
  repeat Store_upd.
  repeat (split=> //).
  case/andP : H1.
  move/ZIT.tP; move/Zmod_2_Zeven; case/Zeven_ex=> a H1a.
  move/ZIT.tP; move/Zmod_2_Zeven; case/Zeven_ex=> b H1b.
  by rewrite /= /ZIT.t_div H1a (Zmult_comm 2) Z_div_mult_full //
    -H9 -(Zmult_comm 2) Zmult_assoc -H1a.
  by case/andP : H1.

  apply hoare_assign'.
  move=> s h /= [H2 [H3 [H4 [H5 [H6 [H7 [H8 [H9 [H10 [H11 [H12 [H13 H14]]]]]]]]]]]].
  rewrite /wp_assign.
  repeat Store_upd.
  repeat (split => //).
  move/ZIT.tP : H14; move/Zmod_2_Zeven; case/Zeven_ex=> a H14.
  rewrite H14 in H9.
  ring_simplify in H9.
  rewrite -!Zmult_assoc -Zmult_plus_distr_r in H9.
  rewrite /= /ZIT.t_div H14 (Zmult_comm 2) Z_div_mult_full //.
  by eapply Zmult_reg_l; eauto.
  by right.
-

apply hoare_assign with (fun s _ =>
    0 <= [x ]_ s /\ 0 <= [y ]_ s /\ 0 <= [g ]_ s /\ 0 <= [u ]_ s /\ 0 <= [v ]_ s /\
    [x ]_ s * [g ]_ s = vx /\ [y ]_ s * [g ]_ s = vy /\
    [A ]_ s * [x ]_ s * 2 - [y]_s * [x]_s + [B ]_ s * [y ]_ s = [u ]_ s * 2 /\
    [C ]_ s * [x ]_ s + [D ]_ s * [y ]_ s = [v ]_ s /\
    Zgcd vx vy = [g ]_ s * Zgcd [u ]_ s [v ]_ s /\
    (Zodd [x]_s \/ Zodd [y]_s) /\
    Zodd [v ]_ s /\
    (Zodd ([A]_s *2 - [y]_s) \/ Zodd ([B]_s))).
  move=> s h /= [[H2 [H3 [H4 [H5 [H6 [H7 [H8 [H9 [H10 [H11 [H12 H13]]]]]]]]]]] H1].
  rewrite /wp_assign; repeat Store_upd.
  repeat (split => //).
  + rewrite /= /ZIT.t_div /ZIT.t_plus.
    rewrite negb_and in H1.
    case/orP : H1.
    * move/ZIT.tP; move/not_Zmod_2_Zodd => H1.
      rewrite -H9.
      ring_simplify.
      f_equal.
      rewrite -Z_div_exact_full_2 //; first by ring.
      rewrite (Zmult_comm _ 2) in H9.
      move/Zmult_2_Zeven : H9.
      move/Zeven_plus_inv.
      case; case => Y1 Y2.
      - case: H12 => H12.
        + move: (Zodd_mult_Zodd _ _ H1 H12); by move/Zeven_not_Zodd.
        + by apply Zeven_Zmod_2, Zodd_plus_Zodd.
      - apply Zeven_Zmod_2.
        case: H12 => H12.
        + case/Zodd_mult_inv : Y2 => Y2 Y3; by apply Zodd_plus_Zodd.
        + by apply Zodd_plus_Zodd.
    * move/ZIT.tP. move/not_Zmod_2_Zodd => H1.
      rewrite -H9.
      ring_simplify.
      f_equal.
      rewrite -Z_div_exact_full_2 //; first by ring.
      rewrite (Zmult_comm _ 2) in H9.
      move/Zmult_2_Zeven : H9.
      move/Zeven_plus_inv.
      case; case=> Y1 Y2.
      - case: H12 => H12.
        + case/Zeven_mult_inv : Y1 => Y1; last by move/Zeven_not_Zodd : Y1.
          case/Zeven_mult_inv : Y2 => Y2; first by move/Zeven_not_Zodd : Y2.
          by apply Zeven_Zmod_2, Zeven_plus_Zeven.
        + move: (Zodd_mult_Zodd _ _ H1 H12).
          by move/Zodd_not_Zeven.
      - case: H12 => H12.
        + case/Zodd_mult_inv : Y1 => Y1 _.
          case/Zodd_mult_inv : Y2 => _ Y2'.
          by apply Zeven_Zmod_2, Zodd_plus_Zodd.
        + case/Zodd_mult_inv : Y1 => Y1 _.
          by apply Zeven_Zmod_2, Zodd_plus_Zodd.
  + rewrite negb_and in H1.
    rewrite /= /ZIT.t_div /ZIT.t_plus.
    case/orP : H1.
    - move/ZIT.tP. move/not_Zmod_2_Zodd => H1.
      case: H12 => H12.
      * case: (Zeven_odd_dec [B]_s) => X; auto.
        rewrite (Zmult_comm _ 2) in H9.
        move/Zmult_2_Zeven : H9.
        case/Zeven_plus_inv.
        - case=> Y1 Y2.
          move: (Zodd_mult_Zodd _ _ H1 H12).
          by move/Zodd_not_Zeven.
        - case=> Y1.
          case/Zodd_mult_inv.
          by move/Zodd_not_Zeven.
      * left.
        apply Zeven_plus_Zodd.
        - rewrite Zmult_comm; by apply Zeven_2p.
        - by apply Zodd_opp.
    - move/ZIT.tP; by move/not_Zmod_2_Zodd; auto.

apply hoare_assign'.
move=> s h /= [H2 [H3 [H4 [H5 [H6 [H7 [H8 [H9 [H10 [H11 [H12 [H13 H14]]]]]]]]]]]].
rewrite /wp_assign; repeat Store_upd.
repeat (split => //).
2: by right.
rewrite /= /ZIT.t_minus /ZIT.t_div.
have {H9}H9 : ([B ]_ s - [x ]_ s) * [y ]_ s = [u ]_ s * 2 - [A ]_ s * [x ]_ s * 2.
  rewrite -H9; ring.
rewrite -Zmult_minus_distr_r -(Zmult_comm 2) in H9.
case: H12 => H12.
+ case: (Zeven_odd_dec [y]_s) => X.
  * case: H14 => H14.
    - move: (Zeven_plus_Zeven _ _ (Zeven_2p [A]_s) (Zeven_opp _ X)).
      rewrite Zmult_comm.
      by move/Zeven_not_Zodd.
    - have Y : Zeven ([B]_s - [x]_s).
        apply Zodd_plus_Zodd => //.
        by apply Zodd_opp.
      case/Zeven_ex : Y => b' Y.
      rewrite Y -Zmult_assoc in H9.
      apply Zmult_reg_l in H9 => //.
      rewrite Y (Zmult_comm 2) Z_div_mult_full // H9; ring.
  * case: (Zeven_odd_dec ([B]_s - [x]_s)) => Y.
    - case/Zeven_ex : Y => b' Y.
      rewrite Y -Zmult_assoc in H9.
      apply Zmult_reg_l in H9 => //.
      rewrite Y (Zmult_comm 2) Z_div_mult_full // H9; ring.
    - have : Zodd ( ([B ]_ s - [x ]_ s) * [y ]_ s ).
      apply Zodd_mult_Zodd => //.
      rewrite H9.
      move: (Zeven_2p (([u ]_ s - [A ]_ s * [x ]_ s))).
      by move/Zeven_not_Zodd.
+ case: (Zeven_odd_dec ([B]_s - [x]_s)) => Y.
  * case/Zeven_ex : Y => b' Y.
    rewrite Y -Zmult_assoc in H9.
    apply Zmult_reg_l in H9 => //.
    rewrite Y (Zmult_comm 2) Z_div_mult_full // H9; ring.
  * have : Zodd ( ([B ]_ s - [x ]_ s) * [y ]_ s ) by apply Zodd_mult_Zodd.
    rewrite H9.
    move: (Zeven_2p (([u ]_ s - [A ]_ s * [x ]_ s))).
    by move/Zeven_not_Zodd.
Qed.

Lemma outer_loop_verif : forall (g x y u v A B C D :ssrnat.nat_eqType) vx vy,
  nodup(g, x, y, u, v, A, B, C, D) -> 0 <= vx -> 0 <= vy ->
  {{ (fun s _ => 0 <= [x ]_ s /\ 0 <= [y ]_ s /\ 0 <= [g ]_ s /\
      0 <= [u ]_ s /\ 0 <= [v ]_ s /\
      [x ]_ s * [g ]_ s = vx /\ [y ]_ s * [g ]_ s = vy /\
      [A ]_ s * [x ]_ s + [B ]_ s * [y ]_ s = [u ]_ s /\
      [C ]_ s * [x ]_ s + [D ]_ s * [y ]_ s = [v ]_ s /\
      Zgcd vx vy = [g ]_ s * Zgcd [u ]_ s [v ]_ s /\
      (Zodd [u ]_ s \/ Zodd [v ]_ s) /\ (Zodd [x ]_ s \/ Zodd [y ]_ s))}}
    outer_loop u v x y A B C D
    {{ (fun s h => (0 <= [x ]_ s /\ 0 <= [y ]_ s /\ 0 <= [g ]_ s /\
     0 <= [u ]_ s /\ 0 <= [v ]_ s /\
     [x ]_ s * [g ]_ s = vx /\ [y ]_ s * [g ]_ s = vy /\
     [A ]_ s * [x ]_ s + [B ]_ s * [y ]_ s = [u ]_ s /\
     [C ]_ s * [x ]_ s + [D ]_ s * [y ]_ s = [v ]_ s /\
     Zgcd vx vy = [g ]_ s * Zgcd [u ]_ s [v ]_ s /\
     (Zodd [u ]_ s \/ Zodd [v ]_ s) /\ (Zodd [x ]_ s \/ Zodd [y ]_ s)) /\
    ~~ hoare_m.eval_b (var_e u >> nat_e 0) (s, h)) }}.
Proof.
move=> g x y u v A B C D vx vy Hset Hvx Hvy.
rewrite /outer_loop.
apply while.hoare_while.

apply while.hoare_seq with (fun s _ =>
  0 <= [x ]_ s /\ 0 <= [y ]_ s /\ 0 <= [g ]_ s /\ 0 <= [u ]_ s /\ 0 <= [v ]_ s /\
  [x ]_ s * [g ]_ s = vx /\
  [y ]_ s * [g ]_ s = vy /\
  [A ]_ s * [x ]_ s + [B ]_ s * [y ]_ s = [u ]_ s /\
  [C ]_ s * [x ]_ s + [D ]_ s * [y ]_ s = [v ]_ s /\
  Zgcd vx vy = [g ]_ s * Zgcd [u ]_ s [v ]_ s /\
  (Zodd [x]_s \/ Zodd [y]_s) /\
  Zodd [u]_s).
eapply hoare_prop_m.hoare_stren; last first.
have Hset' : nodup(x, y, g, u, v, A, B, C, D).
  rewrite [Equality.sort _]/= in Hset *. by Nodup_nodup O.
by apply (inner_loop_verif x y g u v vx vy A B C D Hset').
move=> s h /= [[H2 [H3 [H4 [H5 [H6 [H7 [H8 [H9 [H10 [H11 H12]]]]]]]]]] H1]; by intuition.
apply hoare_prop_m.hoare_stren with (fun s _ =>
  (0 <= [x ]_ s /\ 0 <= [y ]_ s /\ 0 <= [g ]_ s /\ 0 <= [v ]_ s /\ 0 <= [u ]_ s /\
    [x ]_ s * [g ]_ s = vx /\ [y ]_ s * [g ]_ s = vy /\
    [C ]_ s * [x ]_ s + [D ]_ s * [y ]_ s = [v ]_ s /\
    [A ]_ s * [x ]_ s + [B ]_ s * [y ]_ s = [u ]_ s /\
    Zgcd vx vy = [g ]_ s * Zgcd [v ]_ s [u ]_ s) /\
  (Zodd [x]_s \/ Zodd [y]_s) /\
  (Zodd [v]_s \/ Zodd [u]_s)).
move=> s h /=.
rewrite (Zgcd_sym [u]_s); by intuition.
have {Hset}Hset' : nodup(x, y, g, v, u, C, D, A, B).
  rewrite [Equality.sort _]/= in Hset *; by Nodup_nodup O.
move: (inner_loop_verif x y g v u vx vy C D A B Hset') => Hi.
eapply while.hoare_seq.
eapply hoare_prop_m.hoare_stren; last by apply Hi.
move=> s h /=; by intuition.
apply while.hoare_ifte.
-

  apply hoare_assign with (fun s _ =>
    0 <= [x ]_ s /\ 0 <= [y ]_ s /\ 0 <= [g ]_ s /\ 0 <= [v ]_ s /\ 0 <= [u ]_ s /\
    [x ]_ s * [g ]_ s = vx /\ [y ]_ s * [g ]_ s = vy /\
    ([A ]_ s - [C]_s)* [x ]_ s + ([B ]_ s - [D]_s)* [y ]_ s = [u ]_ s /\
    [C ]_ s * [x ]_ s + [D ]_ s * [y ]_ s = [v ]_ s /\
    Zgcd vx vy = [g ]_ s * Zgcd [u ]_ s [v ]_ s /\
    (Zodd [x]_s \/ Zodd [y]_s) /\
    (Zodd [v]_s \/ Zodd [u]_s)).
  move=> s h /= [[H3 [H4 [H5 [H6 [H7 [H8 [H9 [H10 [H11 [H12 [H13 H14]]]]]]]]]]] H2].
  rewrite /wp_assign; repeat Store_upd => //.
  repeat (split => //).
  move/Zge_bool_true : H2 => H2.
  rewrite /=; by omegab.
  rewrite /= /ZIT.t_minus -H10 -H11; ring.
  by rewrite /= /ZIT.t_minus -Zgcd_minus (Zgcd_sym [u]_s).
  rewrite /= /ZIT.t_minus.
  case: (Zeven_odd_dec [v]_s) => Htmp; by auto.