encode25519_x32_20times.ml

type nat =
| O
| S of nat

(** val fst : ('a1 * 'a2) -> 'a1 **)

let fst = function
| (x, _) -> x

(** val snd : ('a1 * 'a2) -> 'a2 **)

let snd = function
| (_, y) -> y

(** val app : 'a1 list -> 'a1 list -> 'a1 list **)

let rec app l m =
  match l with
  | [] -> m
  | a :: l1 -> a :: (app l1 m)

type comparison =
| Eq
| Lt
| Gt

(** val compOpp : comparison -> comparison **)

let compOpp = function
| Eq -> Eq
| Lt -> Gt
| Gt -> Lt

(** val pred : nat -> nat **)

let pred n = match n with
| O -> n
| S u -> u

type positive =
| XI of positive
| XO of positive
| XH

type z =
| Z0
| Zpos of positive
| Zneg of positive

module Pos =
 struct
  (** val succ : positive -> positive **)

  let rec succ = function
  | XI p -> XO (succ p)
  | XO p -> XI p
  | XH -> XO XH

  (** val add : positive -> positive -> positive **)

  let rec add x y =
    match x with
    | XI p ->
      (match y with
       | XI q -> XO (add_carry p q)
       | XO q -> XI (add p q)
       | XH -> XO (succ p))
    | XO p ->
      (match y with
       | XI q -> XI (add p q)
       | XO q -> XO (add p q)
       | XH -> XI p)
    | XH -> (match y with
             | XI q -> XO (succ q)
             | XO q -> XI q
             | XH -> XO XH)

  (** val add_carry : positive -> positive -> positive **)

  and add_carry x y =
    match x with
    | XI p ->
      (match y with
       | XI q -> XI (add_carry p q)
       | XO q -> XO (add_carry p q)
       | XH -> XI (succ p))
    | XO p ->
      (match y with
       | XI q -> XO (add_carry p q)
       | XO q -> XI (add p q)
       | XH -> XO (succ p))
    | XH -> (match y with
             | XI q -> XI (succ q)
             | XO q -> XO (succ q)
             | XH -> XI XH)

  (** val pred_double : positive -> positive **)

  let rec pred_double = function
  | XI p -> XI (XO p)
  | XO p -> XI (pred_double p)
  | XH -> XH

  (** val mul : positive -> positive -> positive **)

  let rec mul x y =
    match x with
    | XI p -> add y (XO (mul p y))
    | XO p -> XO (mul p y)
    | XH -> y

  (** val iter : ('a1 -> 'a1) -> 'a1 -> positive -> 'a1 **)

  let rec iter f x = function
  | XI n' -> f (iter f (iter f x n') n')
  | XO n' -> iter f (iter f x n') n'
  | XH -> f x

  (** val compare_cont : comparison -> positive -> positive -> comparison **)

  let rec compare_cont r x y =
    match x with
    | XI p ->
      (match y with
       | XI q -> compare_cont r p q
       | XO q -> compare_cont Gt p q
       | XH -> Gt)
    | XO p ->
      (match y with
       | XI q -> compare_cont Lt p q
       | XO q -> compare_cont r p q
       | XH -> Gt)
    | XH -> (match y with
             | XH -> r
             | _ -> Lt)

  (** val compare : positive -> positive -> comparison **)

  let compare =
    compare_cont Eq

  (** val eqb : positive -> positive -> bool **)

  let rec eqb p q =
    match p with
    | XI p0 -> (match q with
                | XI q0 -> eqb p0 q0
                | _ -> false)
    | XO p0 -> (match q with
                | XO q0 -> eqb p0 q0
                | _ -> false)
    | XH -> (match q with
             | XH -> true
             | _ -> false)

  (** val of_succ_nat : nat -> positive **)

  let rec of_succ_nat = function
  | O -> XH
  | S x -> succ (of_succ_nat x)
 end

module Z =
 struct
  (** val double : z -> z **)

  let double = function
  | Z0 -> Z0
  | Zpos p -> Zpos (XO p)
  | Zneg p -> Zneg (XO p)

  (** val succ_double : z -> z **)

  let succ_double = function
  | Z0 -> Zpos XH
  | Zpos p -> Zpos (XI p)
  | Zneg p -> Zneg (Pos.pred_double p)

  (** val pred_double : z -> z **)

  let pred_double = function
  | Z0 -> Zneg XH
  | Zpos p -> Zpos (Pos.pred_double p)
  | Zneg p -> Zneg (XI p)

  (** val pos_sub : positive -> positive -> z **)

  let rec pos_sub x y =
    match x with
    | XI p ->
      (match y with
       | XI q -> double (pos_sub p q)
       | XO q -> succ_double (pos_sub p q)
       | XH -> Zpos (XO p))
    | XO p ->
      (match y with
       | XI q -> pred_double (pos_sub p q)
       | XO q -> double (pos_sub p q)
       | XH -> Zpos (Pos.pred_double p))
    | XH ->
      (match y with
       | XI q -> Zneg (XO q)
       | XO q -> Zneg (Pos.pred_double q)
       | XH -> Z0)

  (** val add : z -> z -> z **)

  let add x y =
    match x with
    | Z0 -> y
    | Zpos x' ->
      (match y with
       | Z0 -> x
       | Zpos y' -> Zpos (Pos.add x' y')
       | Zneg y' -> pos_sub x' y')
    | Zneg x' ->
      (match y with
       | Z0 -> x
       | Zpos y' -> pos_sub y' x'
       | Zneg y' -> Zneg (Pos.add x' y'))

  (** val opp : z -> z **)

  let opp = function
  | Z0 -> Z0
  | Zpos x0 -> Zneg x0
  | Zneg x0 -> Zpos x0

  (** val sub : z -> z -> z **)

  let sub m n =
    add m (opp n)

  (** val mul : z -> z -> z **)

  let mul x y =
    match x with
    | Z0 -> Z0
    | Zpos x' ->
      (match y with
       | Z0 -> Z0
       | Zpos y' -> Zpos (Pos.mul x' y')
       | Zneg y' -> Zneg (Pos.mul x' y'))
    | Zneg x' ->
      (match y with
       | Z0 -> Z0
       | Zpos y' -> Zneg (Pos.mul x' y')
       | Zneg y' -> Zpos (Pos.mul x' y'))

  (** val pow_pos : z -> positive -> z **)

  let pow_pos z0 =
    Pos.iter (mul z0) (Zpos XH)

  (** val pow : z -> z -> z **)

  let pow x = function
  | Z0 -> Zpos XH
  | Zpos p -> pow_pos x p
  | Zneg _ -> Z0

  (** val compare : z -> z -> comparison **)

  let compare x y =
    match x with
    | Z0 -> (match y with
             | Z0 -> Eq
             | Zpos _ -> Lt
             | Zneg _ -> Gt)
    | Zpos x' -> (match y with
                  | Zpos y' -> Pos.compare x' y'
                  | _ -> Gt)
    | Zneg x' -> (match y with
                  | Zneg y' -> compOpp (Pos.compare x' y')
                  | _ -> Lt)

  (** val leb : z -> z -> bool **)

  let leb x y =
    match compare x y with
    | Gt -> false
    | _ -> true

  (** val ltb : z -> z -> bool **)

  let ltb x y =
    match compare x y with
    | Lt -> true
    | _ -> false

  (** val eqb : z -> z -> bool **)

  let rec eqb x y =
    match x with
    | Z0 -> (match y with
             | Z0 -> true
             | _ -> false)
    | Zpos p -> (match y with
                 | Zpos q -> Pos.eqb p q
                 | _ -> false)
    | Zneg p -> (match y with
                 | Zneg q -> Pos.eqb p q
                 | _ -> false)

  (** val of_nat : nat -> z **)

  let of_nat = function
  | O -> Z0
  | S n0 -> Zpos (Pos.of_succ_nat n0)

  (** val pos_div_eucl : positive -> z -> z * z **)

  let rec pos_div_eucl a b =
    match a with
    | XI a' ->
      let (q, r) = pos_div_eucl a' b in
      let r' = add (mul (Zpos (XO XH)) r) (Zpos XH) in
      if ltb r' b
      then ((mul (Zpos (XO XH)) q), r')
      else ((add (mul (Zpos (XO XH)) q) (Zpos XH)), (sub r' b))
    | XO a' ->
      let (q, r) = pos_div_eucl a' b in
      let r' = mul (Zpos (XO XH)) r in
      if ltb r' b
      then ((mul (Zpos (XO XH)) q), r')
      else ((add (mul (Zpos (XO XH)) q) (Zpos XH)), (sub r' b))
    | XH -> if leb (Zpos (XO XH)) b then (Z0, (Zpos XH)) else ((Zpos XH), Z0)

  (** val div_eucl : z -> z -> z * z **)

  let div_eucl a b =
    match a with
    | Z0 -> (Z0, Z0)
    | Zpos a' ->
      (match b with
       | Z0 -> (Z0, Z0)
       | Zpos _ -> pos_div_eucl a' b
       | Zneg b' ->
         let (q, r) = pos_div_eucl a' (Zpos b') in
         (match r with
          | Z0 -> ((opp q), Z0)
          | _ -> ((opp (add q (Zpos XH))), (add b r))))
    | Zneg a' ->
      (match b with
       | Z0 -> (Z0, Z0)
       | Zpos _ ->
         let (q, r) = pos_div_eucl a' b in
         (match r with
          | Z0 -> ((opp q), Z0)
          | _ -> ((opp (add q (Zpos XH))), (sub b r)))
       | Zneg b' -> let (q, r) = pos_div_eucl a' (Zpos b') in (q, (opp r)))

  (** val div : z -> z -> z **)

  let div a b =
    let (q, _) = div_eucl a b in q

  (** val modulo : z -> z -> z **)

  let modulo a b =
    let (_, r) = div_eucl a b in r
 end

(** val rev : 'a1 list -> 'a1 list **)

let rec rev = function
| [] -> []
| x :: l' -> app (rev l') (x :: [])

(** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **)

let rec map f = function
| [] -> []
| a :: t -> (f a) :: (map f t)

(** val flat_map : ('a1 -> 'a2 list) -> 'a1 list -> 'a2 list **)

let rec flat_map f = function
| [] -> []
| x :: t -> app (f x) (flat_map f t)

(** val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1 **)

let rec fold_right f a0 = function
| [] -> a0
| b :: t -> f b (fold_right f a0 t)

(** val partition : ('a1 -> bool) -> 'a1 list -> 'a1 list * 'a1 list **)

let rec partition f = function
| [] -> ([], [])
| x :: tl ->
  let (g, d) = partition f tl in if f x then ((x :: g), d) else (g, (x :: d))

(** val combine : 'a1 list -> 'a2 list -> ('a1 * 'a2) list **)

let rec combine l l' =
  match l with
  | [] -> []
  | x :: tl -> (match l' with
                | [] -> []
                | y :: tl' -> (x, y) :: (combine tl tl'))

(** val seq : nat -> nat -> nat list **)

let rec seq start = function
| O -> []
| S len0 -> start :: (seq (S start) len0)

module List =
 struct
  (** val repeat : 'a1 -> nat -> 'a1 list **)

  let rec repeat x = function
  | O -> []
  | S k -> x :: (repeat x k)
 end

(** val update_nth : nat -> ('a1 -> 'a1) -> 'a1 list -> 'a1 list **)

let rec update_nth n f xs =
  match n with
  | O -> (match xs with
          | [] -> []
          | x' :: xs' -> (f x') :: xs')
  | S n' -> (match xs with
             | [] -> []
             | x' :: xs' -> x' :: (update_nth n' f xs'))

(** val let_In : 'a1 -> ('a1 -> 'a2) -> 'a2 **)

let let_In x f =
  f x

module Associational =
 struct
  (** val mul : (z * z) list -> (z * z) list -> (z * z) list **)

  let mul p q =
    flat_map (fun t ->
      map (fun t' -> ((Z.mul (fst t) (fst t')), (Z.mul (snd t) (snd t')))) q) p

  (** val split : z -> (z * z) list -> (z * z) list * (z * z) list **)

  let split s p =
    let hi_lo = partition (fun t -> Z.eqb (Z.modulo (fst t) s) Z0) p in
    ((snd hi_lo), (map (fun t -> ((Z.div (fst t) s), (snd t))) (fst hi_lo)))

  (** val reduce : z -> (z * z) list -> (z * z) list -> (z * z) list **)

  let reduce s c p =
    let lo_hi = split s p in app (fst lo_hi) (mul c (snd lo_hi))

  (** val carryterm : z -> z -> (z * z) -> (z * z) list **)

  let carryterm w fw t =
    if Z.eqb (fst t) w
    then let_In (snd t) (fun t2 ->
           let_In (Z.div t2 fw) (fun d2 ->
             let_In (Z.modulo t2 fw) (fun m2 -> ((Z.mul w fw), d2) :: ((w,
               m2) :: []))))
    else t :: []

  (** val carry : z -> z -> (z * z) list -> (z * z) list **)

  let carry w fw p =
    flat_map (carryterm w fw) p
 end

module Positional =
 struct
  (** val to_associational : (nat -> z) -> nat -> z list -> (z * z) list **)

  let to_associational weight n xs =
    combine (map weight (seq O n)) xs

  (** val zeros : nat -> z list **)

  let zeros n =
    List.repeat Z0 n

  (** val add_to_nth : nat -> z -> z list -> z list **)

  let add_to_nth i x ls =
    update_nth i (fun y -> Z.add x y) ls

  (** val place : (nat -> z) -> (z * z) -> nat -> nat * z **)

  let rec place weight t = function
  | O -> (O, (Z.mul (fst t) (snd t)))
  | S n ->
    let i0 = S n in
    if Z.eqb (Z.modulo (fst t) (weight i0)) Z0
    then (i0, (let c = Z.div (fst t) (weight i0) in Z.mul c (snd t)))
    else place weight t n

  (** val from_associational : (nat -> z) -> nat -> (z * z) list -> z list **)

  let from_associational weight n p =
    fold_right (fun t ls ->
      let_In (place weight t (pred n)) (fun p0 -> add_to_nth (fst p0) (snd p0) ls))
      (zeros n) p

  (** val carry : (nat -> z) -> nat -> nat -> nat -> z list -> z list **)

  let carry weight n m index p =
    from_associational weight m
      (Associational.carry (weight index)
        (Z.div (weight (S index)) (weight index)) (to_associational weight n p))

  (** val carry_reduce :
      (nat -> z) -> nat -> z -> (z * z) list -> nat -> z list -> z list **)

  let carry_reduce weight n s c index p =
    from_associational weight n
      (Associational.reduce s c
        (to_associational weight (S n) (carry weight n (S n) index p)))

  (** val chained_carries :
      (nat -> z) -> nat -> z -> (z * z) list -> z list -> nat list -> z list **)

  let chained_carries weight n s c p idxs =
    fold_right (fun a b -> carry_reduce weight n s c a b) p (rev idxs)

  (** val encode : (nat -> z) -> nat -> z -> (z * z) list -> z -> z list **)

  let encode weight n s c x =
    chained_carries weight n s c
      (from_associational weight n (((Zpos XH), x) :: [])) (seq O n)
 end

(** val foo : unit -> z list **)

let foo _ =
  Positional.encode (fun i ->
    Z.pow (Zpos (XO XH))
      (Z.opp
        (Z.div
          (Z.opp (Z.mul (Zpos (XI (XI (XI (XI (XI (XI (XI XH)))))))) (Z.of_nat i)))
          (Zpos (XO (XI (XO XH))))))) (S (S (S (S (S (S (S (S (S (S O))))))))))
    (Z.pow (Zpos (XO XH)) (Zpos (XI (XI (XI (XI (XI (XI (XI XH))))))))) (((Zpos
    XH), (Zpos (XI (XI (XO (XO XH)))))) :: [])
    (Z.sub (Z.pow (Zpos (XO XH)) (Zpos (XI (XI (XI (XI (XI (XI (XI XH)))))))))
      (Zpos XH))


let bar = foo () :: foo () :: foo () :: foo () :: foo () :: foo () :: foo () :: foo () :: foo () :: foo () :: foo () :: foo () :: foo () :: foo () :: foo () :: foo () :: foo () :: foo () :: foo () :: foo () :: []