val mk_felem_one: f:F.felem -> Stack unit
  (requires fun h -> live h f)
  (ensures  fun h0 _ h1 -> modifies (loc f) h0 h1 /\
    F.inv_lazy_reduced2 h1 f /\ F.feval h1 f == S.one)
let mk_felem_one f =
  Math.Lemmas.small_mod S.one S.prime;
  F.set_one f
val mk_felem_one: f:F.felem -> Stack unit
  (requires fun h -> live h f)
  (ensures  fun h0 _ h1 -> modifies (loc f) h0 h1 /\
    F.inv_lazy_reduced2 h1 f /\ F.feval h1 f == S.one)
let mk_felem_one f =
Math.Lemmas.small_mod S.one S.prime;
F.set_one f
Hacl.EC.K256.fst.checked
Spec.K256.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.K256.Field52.Lemmas.fsti.checked Hacl.K256.Scalar.fsti.checked Hacl.K256.Field.fsti.checked Hacl.Impl.K256.PointMul.fsti.checked Hacl.Impl.K256.PointDouble.fst.checked Hacl.Impl.K256.PointAdd.fst.checked Hacl.Impl.K256.Point.fsti.checked Hacl.Impl.K256.Finv.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.EC.K256.fst
Hacl.K256.Field.felem Hacl.K256.Field.set_one Prims.unit FStar.Math.Lemmas.small_mod Spec.K256.PointOps.one Spec.K256.PointOps.prime
module Hacl.EC.K256

open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer

module ST = FStar.HyperStack.ST
module BSeq = Lib.ByteSequence

module S = Spec.K256

module F = Hacl.K256.Field
module Q = Hacl.K256.Scalar
module FI = Hacl.Impl.K256.Finv

module P = Hacl.Impl.K256.Point
module PA = Hacl.Impl.K256.PointAdd
module PD = Hacl.Impl.K256.PointDouble
module PM = Hacl.Impl.K256.PointMul

module BL = Hacl.Spec.K256.Field52.Lemmas

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

[@@ CPrologue
"/*******************************************************************************
  Verified field arithmetic modulo p = 2^256 - 0x1000003D1.

  This is a 64-bit optimized version, where a field element in radix-2^{52} is
  represented as an array of five unsigned 64-bit integers, i.e., uint64_t[5].
*******************************************************************************/\n";

Comment "Write the additive identity in `f`.

  The outparam `f` is meant to be 5 limbs in size, i.e., uint64_t[5]."]
val mk_felem_zero: f:F.felem -> Stack unit
  (requires fun h -> live h f)
  (ensures  fun h0 _ h1 -> modifies (loc f) h0 h1 /\
    F.inv_lazy_reduced2 h1 f /\ F.feval h1 f == S.zero)

let mk_felem_zero f =
  Math.Lemmas.small_mod S.zero S.prime;
  F.set_zero f


[@@ Comment "Write the multiplicative identity in `f`.

  The outparam `f` is meant to be 5 limbs in size, i.e., uint64_t[5]."]
val mk_felem_one: f:F.felem -> Stack unit
  (requires fun h -> live h f)
  (ensures  fun h0 _ h1 -> modifies (loc f) h0 h1 /\
    F.inv_lazy_reduced2 h1 f /\ F.feval h1 f == S.one)
val mk_felem_one: f:F.felem -> Stack unit
  (requires fun h -> live h f)
  (ensures  fun h0 _ h1 -> modifies (loc f) h0 h1 /\
    F.inv_lazy_reduced2 h1 f /\ F.feval h1 f == S.one)
f: Hacl.K256.Field.felem -> FStar.HyperStack.ST.Stack Prims.unit