Require Import ZArith.
Require Import List.
Require Import util.
Require Import machine_int.
Import MachineInt.
Require Import machine_int_spec.
Require Import sum.
Require Import state.
Require Import mips.
Require Import mapstos.
Require Import mips_contrib.

Open Local Scope asm_heap_scope.
Open Local Scope mips_scope.
Open Local Scope Z_scope.

(*********************** definition of the montgomery function ********************************************)

Definition montgomery (k alpha x y z m int_ ext X Y M Z one zero quot C t s:gp_reg) :=
  addiu one zero one16;
  addiu C zero zero16;
  addiu ext zero zero16;
  
  while_bne ext k (
    lwxs X ext x;
    lw Y zero16 y;
    lw Z zero16 z;
    
    multu X Y;
    lw M zero16 m;
    maddu Z one;
    mflo t;
    mfhi s;
    
    multu t alpha;
    addiu int_ zero one16;
    mflo quot;
    
    mthi s;
    mtlo t;
    
    maddu quot M;
    mflhxu Z;
    
    addiu t z zero16;
    
    while_bne int_ k (
      lwxs Y int_ y;
      lwxs Z int_ z;
      
      maddu X Y;
      lwxs M int_ m;
      maddu Z one;
      maddu quot M;
      addiu int_ int_ one16;
      mflhxu Z;
      
      addiu t t four16;
      sw Z mfour16 t (* NB: appear syntactically after the branch in the original code *)
    );
    
    maddu C one;
    mflhxu Z;
    addiu ext ext one16;
    
    sw Z zero16 t;
    mflhxu C (* NB: appear syntactically after the branch in the original code *)
  ).

Definition x := gpr_a0.
Definition y := gpr_a1.
Definition z := gpr_a2.
Definition alpha := gpr_a3.
Definition m := gpr_s6.
Definition one := gpr_t0.
Definition int_ := gpr_t1.
Definition ext := gpr_t2.
Definition X_ := gpr_t4.
Definition Y_ := gpr_t5.
Definition M_ := gpr_t6.
Definition Z_ := gpr_t7.
Definition quot := gpr_s1.
Definition C := gpr_s2.
Definition t := gpr_s3.
Definition s := gpr_s4.
Definition k := gpr_s5.

(*********************** montgomery lemma ******************************************)

Lemma montgomery_lemma : forall alpha m0, u2Z m0 * u2Z alpha == -1 [[ Zbeta 1 ]] ->
  forall (A:int 64) mu,
    multiplier.utoZ mu < Zbeta 2 -> multiplier.utoZ mu = u2Z A ->
    multiplier.lo 
    (multiplier.maddu_op (((A % 32 (.) alpha) % 32) (.) m0) mu) = 
    zero32.
  intros.

  apply lo_remainder_zero.

  rewrite multiplier.maddu_utoZ.
  rewrite H1.

  inversion_clear H as [K].

  exists (
    (K * (u2Z A)) -
    (K * (Zbeta 1) * (u2Z (shr_shrink 32 A))) + 
    (u2Z (shr_shrink 32 A)) -
    ((u2Z m0) * (u2Z (shr_shrink 32 (umul (rem 32 A) alpha0))))
  ).

  rewrite (@umul_u2Z 32).
  rewrite rem_u2Z.
  rewrite (@umul_u2Z 32).
  rewrite rem_u2Z.
  rewrite <-Zbeta_power1.
  ring.
  rewrite (Zmult_assoc (u2Z m0)).
  rewrite (Zmult_comm (u2Z m0)).
  rewrite <-Zmult_assoc.
  ring.
  ring.
  ring.
  ring.
  rewrite H2.
  ring.

  omega.
  omega.

  assert (1 <= Zpower 2 multiplier.acx_size - 1).

  assert ( Zpower 2 8 <= Zpower 2 multiplier.acx_size ).
  apply Zpower_2_le.
  apply multiplier.acx_size_min.
  simpl in H2.
  omega.
  apply Zlt_le_trans with (Zbeta 2); auto.

  apply Zle_trans with (Zbeta 2 * 1).
  rewrite Zmult_1_r.
  omega.

  apply Zmult_le_compat.
  omega.
  assumption.
  generalize (Zbeta_1 2); omega.
  omega.
Qed.

(********************* identites remarquables sur nat (not used any more) ***************************)

(*
 * about square
 *) 

(*
Definition sq := fun a => a * a.

Lemma sq_increase : forall a, a <= sq a. 
  destruct a.
  constructor.
  unfold sq.
  apply scale_le.
  apply le_n_S.
  apply le_O_n.
Qed.

Lemma sq_monotonic' : forall a b, a < b -> sq a < sq b. 
  induction a.
  intros.
  unfold sq.
  destruct b.
  inversion H.
  simpl.
  apply lt_O_Sn.
  intros.
  destruct b.
  inversion H.
  assert (a<b).
  apply lt_S_n.
  assumption.
  unfold sq.
  simpl.
  apply lt_n_S.
  rewrite (mult_comm a).
  rewrite (mult_comm b).
  simpl.
  generalize (IHa _ H0); intros.
  unfold sq in H1.
  apply plus_lt_compat.
  assumption.
  apply plus_lt_compat.
  assumption.
  assumption.
Qed.

Lemma sq_monotonic : forall a b, a <= b -> sq a <= sq b. 
  intros.
  generalize (eq_nat_dec a b); intro.
  inversion_clear H0.
  subst b; constructor.
  assert (a<b).
  omega.
  generalize (sq_monotonic' _ _ H0); intro.
  omega.
Qed.

Lemma sq_plus : forall a, a >= 2 -> a + a <= sq a. 
  induction a.
  auto.
  intros.
  assert (a = 1 \/ a >= 2).
  omega.
  inversion_clear H0.
  subst a.
  auto.
  unfold sq.
  simpl.
  rewrite mult_comm.
  simpl.
  rewrite plus_comm.
  simpl.
  generalize (IHa H1); intro.
  unfold sq in H0.
  omega.
Qed.

(*
 * identites remarquables
 *)

Lemma my_id_rem : forall n,
  2 <= n ->
  sq (n - 1) = sq n - 2 * n + 1.
intros.
unfold sq.
rewrite mult_minus_distr_r; try omega.
rewrite mult_1_l.
rewrite mult_minus_distr_l; try omega.
rewrite mult_1_r.
cutrewrite (2=1+1).
rewrite mult_plus_distr_r.
rewrite mult_1_l.

assert (n + n <= n * n).
fold (sq n).
apply sq_plus.
red.
assumption.
generalize H0; clear H0.
generalize (n*n).
intros.
omega.
auto.
Qed.

Lemma my_id_rem2 : forall n,
  2 <= n ->
  sq (n-1) + sq (n-1) + (n-1) = 2 * sq n - 3 * n + 1.
intros.
symmetry.
apply minus_plus_comm.

apply le_trans with (n+n+n).
simpl.
rewrite <-plus_n_O.
rewrite plus_assoc.
constructor.
simpl.
apply plus_le_compat.
apply sq_plus.
red; assumption.
rewrite <-plus_n_O.
apply sq_increase.

symmetry.
apply plus_minus.
rewrite my_id_rem.
repeat rewrite <-plus_assoc.
rewrite le_plus_minus_r.
ring.
rewrite mult_minus_distr_l.
cutrewrite (2*(2*n)=4*n).
ring.
symmetry.
apply minus_plus_comm.

apply le_trans with ((n+n)+(n+n)).
simpl.
rewrite <-plus_n_O.
rewrite plus_assoc.
constructor.
simpl.
rewrite <-plus_n_O.
apply plus_le_compat.
apply sq_plus.
red; assumption.
apply sq_plus.
red; assumption.

symmetry.
apply plus_minus.
rewrite plus_comm.
reflexivity.
ring.
red.
apply le_trans with (n+n).
simpl.
rewrite <-plus_n_O.
constructor.
apply sq_plus.
red; assumption.
apply le_trans with 2; try assumption||auto.
assumption.
Qed.

Lemma my_id_rem3 : forall n,
  2 <= n ->
  sq (n - 1) + (2 * n - 1) = sq n.
  intros.
  rewrite my_id_rem.
  assert ( sq n - 2 * n + 1 + (2 * n - 1) = sq n - 2 * n + (1 + (2 * n - 1)) ).
  rewrite plus_assoc.
  reflexivity.
  rewrite H0; clear H0.
  apply minus_plus_comm.
  apply le_trans with (n+n).
  simpl.
  rewrite <-plus_n_O.
  constructor.
  apply sq_plus.
  red.
  assumption.
  rewrite le_plus_minus_r.
  symmetry.
  apply plus_minus.
  unfold sq.
  rewrite plus_comm.
  reflexivity.
  apply le_trans with (2*1).
  simpl.
  auto.
  apply mult_le_compat_l.
  apply le_trans with 2.
  auto.
  assumption.
  assumption.
Qed.

Lemma my_id_rem4 : forall a,
  2 <= a ->
  sq (a-1) + (sq a + a - 1) = 2 * sq a - a.
  intros.
  rewrite my_id_rem.
  rewrite <-plus_assoc.
  apply minus_plus_comm.
  simpl.
  rewrite <-plus_n_O.
  apply sq_plus.
  assumption.
  rewrite le_plus_minus_r.
  symmetry.
  apply plus_minus.
  simpl.
  rewrite <-plus_n_O.
  rewrite <-plus_n_O.
  rewrite <-plus_assoc.
  rewrite le_plus_minus_r.
  ring.
  apply le_plus_trans.
  apply sq_increase.
  rewrite plus_comm.
  apply le_plus_trans.
  apply le_trans with 2.
  auto.
  assumption.
  assumption.
Qed.

Lemma my_id_rem5 : forall a,
  1 <= a ->
  a - 1 + (2 * a - 1) = 3 * a - 2.
  destruct a.
  intros.
  inversion H.
  intros.
  simpl.
  repeat rewrite <-minus_n_O.
  repeat rewrite <-plus_n_O.
  repeat rewrite <-plus_n_Sm.
  simpl.
  reflexivity.
Qed.

Lemma my_lt_rem : forall a b,
  1 < a ->
  3 * a < b ->
  b - 3 * a + 1 < b - 2 * a.
  intros.
  cutrewrite (3=2+1).
  rewrite mult_plus_distr_r.
  rewrite mult_1_l.

  assert ( b - (2 * a + a) + 1 = b + 1 - (2 * a + a) ).
  apply minus_plus_comm.
  apply le_trans with (3*a).
  simpl.
  rewrite <-plus_n_O.
  rewrite plus_assoc.
  constructor.
  apply lt_le_weak.
  assumption.
  reflexivity.
  rewrite H1; clear H1.

  apply plus_lt_minus'.
  red.

  apply plus_lt_minus.
  simpl.
  rewrite <-plus_n_O.
  apply lt_trans with (3*a).
  simpl.
  rewrite <-plus_n_O.
  apply plus_lt_compat_l.
  apply lt_trans with (a+1).
  red.
  rewrite S_to_plus_one.
  rewrite plus_comm.
  constructor.
  apply plus_lt_compat_l.
  assumption.
  assumption.

  assert ( b - 2 * a + (2 * a + a) =  b + (2 * a + a) - 2 * a ).
  apply minus_plus_comm.
  apply le_trans with (2*a).
  rewrite mult_comm.
  constructor.
  apply lt_le_weak.
  apply lt_trans with (3*a).
  apply mult_lt_compat_r.
  auto.
  apply lt_trans with 1.
  auto.
  assumption.
  assumption.
  reflexivity.
  rewrite H1; clear H1.

  rewrite plus_minus_assoc.
  
  assert ( 2 * a + a - 2 * a = a ).
  simpl.
  rewrite <-plus_n_O.
  apply minus_plus.
  rewrite H1; clear H1.

  apply plus_lt_compat_l.
  assumption.
  red.
  apply le_plus_trans.
  constructor.
  auto.
Qed.

Lemma my_lt_rem2 : forall a b,
  a < b -> 
  a >= 1 ->
  a - 1 + (b - a) < b.
  intros.
  assert ( a - 1 + (b - a) = a + (b - a) - 1 ).
  apply minus_plus_comm.
  assumption.
  reflexivity.
  rewrite H1; clear H1.
  rewrite le_plus_minus_r.
  apply lt_minus.
  apply le_trans with a.
  assumption.
  apply lt_le_weak.
  assumption.
  auto.
  auto.
  apply lt_le_weak.
  assumption.
Qed.

*)