let add_and_double1 q nq nqp1 =
  let x_1, z_1 = q in
  let x_2, z_2 = nq in
  let a = x_2 +% z_2 in
  let b = x_2 -% z_2 in
  let nqp1 = add_and_double1_0 a b nqp1 in
  let (x_2, z_2), (x_3, z_3) = add_and_double1_1 a b nqp1 in
  let z_3 = z_3 *% x_1 in
  (x_2, z_2), (x_3, z_3)
let add_and_double1 q nq nqp1 =
let x_1, z_1 = q in
let x_2, z_2 = nq in
let a = x_2 +% z_2 in
let b = x_2 -% z_2 in
let nqp1 = add_and_double1_0 a b nqp1 in
let (x_2, z_2), (x_3, z_3) = add_and_double1_1 a b nqp1 in
let z_3 = z_3 *% x_1 in
(x_2, z_2), (x_3, z_3)
Hacl.Spec.Curve25519.AddAndDouble.fst.checked
Spec.Curve25519.fst.checked prims.fst.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Hacl.Spec.Curve25519.AddAndDouble.fst
FStar.Pervasives.Native.tuple2 Spec.Curve25519.elem FStar.Pervasives.Native.Mktuple2 Spec.Curve25519.op_Star_Percent Hacl.Spec.Curve25519.AddAndDouble.add_and_double1_1 Hacl.Spec.Curve25519.AddAndDouble.add_and_double1_0 Spec.Curve25519.op_Subtraction_Percent Spec.Curve25519.op_Plus_Percent
module Hacl.Spec.Curve25519.AddAndDouble

open FStar.Mul
open Lib.IntTypes
open Spec.Curve25519

let add_and_double1_0 a b nqp1 =
  let x_3, z_3 = nqp1 in
  let c = x_3 +% z_3 in
  let d = x_3 -% z_3 in

  let da = d *% a in
  let cb = c *% b in
  let x_3 = da +% cb in
  let z_3 = da -% cb in
  (x_3, z_3)

let add_and_double1_1 a b nqp1 =
  let x_3, z_3 = nqp1 in
  let aa = a *% a in
  let bb = b *% b in

  let x_3 = x_3 *% x_3 in
  let z_3 = z_3 *% z_3 in

  let e = aa -% bb in
  let e121665 = e *% 121665 in
  let aa_e121665 = e121665 +% aa in
  let x_2 = aa *% bb in
  let z_2 = e *% aa_e121665 in
  (x_2, z_2), (x_3, z_3)
val add_and_double1 : q: (Spec.Curve25519.elem * _) ->
    nq: (Spec.Curve25519.elem * Spec.Curve25519.elem) ->
    nqp1: (Spec.Curve25519.elem * Spec.Curve25519.elem)
  -> (Spec.Curve25519.elem * Spec.Curve25519.elem) * (Spec.Curve25519.elem * Spec.Curve25519.elem)

    q: (Spec.Curve25519.elem * _) ->
    nq: (Spec.Curve25519.elem * Spec.Curve25519.elem) ->
    nqp1: (Spec.Curve25519.elem * Spec.Curve25519.elem)
  -> (Spec.Curve25519.elem * Spec.Curve25519.elem) * (Spec.Curve25519.elem * Spec.Curve25519.elem)