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_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
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
Prims.unit Spec.K256.PointOps.point_at_inf Spec.K256.Lemmas.to_aff_point_at_infinity_lemma Spec.K256.PointOps.proj_point
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
val point_at_inf_c: SE.one_st proj_point mk_to_k256_comm_monoid
Spec.Exponentiation.one_st Spec.K256.PointOps.proj_point Spec.K256.mk_to_k256_comm_monoid