val mk_k256_comm_monoid:LE.comm_monoid aff_point
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;
}
val mk_k256_comm_monoid:LE.comm_monoid aff_point
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
}
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
Lib.Exponentiation.Definition.Mkcomm_monoid Spec.K256.PointOps.aff_point Spec.K256.PointOps.aff_point_at_inf Spec.K256.PointOps.aff_point_add Spec.K256.Lemmas.aff_point_at_inf_lemma Spec.K256.Lemmas.aff_point_add_assoc_lemma Spec.K256.Lemmas.aff_point_add_comm_lemma
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
*)
val mk_k256_comm_monoid:LE.comm_monoid aff_point
Lib.Exponentiation.Definition.comm_monoid Spec.K256.PointOps.aff_point