val point_mul_double_g (a1 a2: qelem) (p: proj_point) : proj_point
let point_mul_double_g (a1:qelem) (a2:qelem) (p:proj_point) : proj_point =
  point_mul_double a1 g a2 p
val point_mul_double_g (a1 a2: qelem) (p: proj_point) : proj_point
let point_mul_double_g (a1 a2: qelem) (p: proj_point) : proj_point =
point_mul_double a1 g a2 p
Spec.K256.fst.checked
Spec.K256.PointOps.fst.checked Spec.K256.Lemmas.fsti.checked Spec.Hash.Definitions.fst.checked Spec.Exponentiation.fsti.checked Spec.Agile.Hash.fsti.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.NatMod.fsti.checked Lib.IntTypes.fsti.checked Lib.Exponentiation.fsti.checked Lib.ByteSequence.fsti.checked FStar.UInt8.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Spec.K256.fst
Spec.K256.PointOps.qelem Spec.K256.PointOps.proj_point Spec.K256.point_mul_double Spec.K256.PointOps.g
module Spec.K256

open FStar.Mul
open Lib.IntTypes
open Lib.Sequence
open Lib.ByteSequence

module M = Lib.NatMod
module LE = Lib.Exponentiation
module SE = Spec.Exponentiation
module KL = Spec.K256.Lemmas

include Spec.K256.PointOps

#set-options "--z3rlimit 30 --fuel 0 --ifuel 0"

(**
 K256: https://en.bitcoin.it/wiki/Secp256k1
 ECDSA: https://en.bitcoin.it/wiki/Elliptic_Curve_Digital_Signature_Algorithm
 https://www.hyperelliptic.org/EFD/g1p/auto-shortw.html
*)

let mk_k256_comm_monoid : LE.comm_monoid aff_point = {
  LE.one = aff_point_at_inf;
  LE.mul = aff_point_add;
  LE.lemma_one = KL.aff_point_at_inf_lemma;
  LE.lemma_mul_assoc = KL.aff_point_add_assoc_lemma;
  LE.lemma_mul_comm = KL.aff_point_add_comm_lemma;
}

let mk_k256_abelian_group : LE.abelian_group aff_point = {
  LE.cm = mk_k256_comm_monoid;
  LE.inverse = aff_point_negate;
  LE.lemma_inverse = KL.aff_point_negate_lemma;
}

let mk_to_k256_comm_monoid : SE.to_comm_monoid proj_point = {
  SE.a_spec = aff_point;
  SE.comm_monoid = mk_k256_comm_monoid;
  SE.refl = to_aff_point;
}

val point_at_inf_c: SE.one_st proj_point mk_to_k256_comm_monoid
let point_at_inf_c _ =
  KL.to_aff_point_at_infinity_lemma ();
  point_at_inf

val point_add_c : SE.mul_st proj_point mk_to_k256_comm_monoid
let point_add_c p q =
  KL.to_aff_point_add_lemma p q;
  point_add p q

val point_double_c : SE.sqr_st proj_point mk_to_k256_comm_monoid
let point_double_c p =
  KL.to_aff_point_double_lemma p;
  point_double p

let mk_k256_concrete_ops : SE.concrete_ops proj_point = {
  SE.to = mk_to_k256_comm_monoid;
  SE.one = point_at_inf_c;
  SE.mul = point_add_c;
  SE.sqr = point_double_c;
}

// [a]P in affine coordinates
let aff_point_mul (a:nat) (p:aff_point) : aff_point =
  LE.pow mk_k256_comm_monoid p a

// [a]P
let point_mul (a:qelem) (p:proj_point) : proj_point =
  SE.exp_fw mk_k256_concrete_ops p 256 a 4

// [a1]P1 + [a2]P2
let point_mul_double (a1:qelem) (p1:proj_point) (a2:qelem) (p2:proj_point) : proj_point =
  SE.exp_double_fw mk_k256_concrete_ops p1 256 a1 p2 a2 5

// [a]G
let point_mul_g (a:qelem) : proj_point = point_mul a g

// [a1]G + [a2]P
val point_mul_double_g (a1 a2: qelem) (p: proj_point) : proj_point
a1: Spec.K256.PointOps.qelem -> a2: Spec.K256.PointOps.qelem -> p: Spec.K256.PointOps.proj_point
  -> Spec.K256.PointOps.proj_point