val felem_add (a b out:F.felem) : Stack unit
  (requires fun h ->
    live h a /\ live h b /\ live h out /\
    eq_or_disjoint out a /\ eq_or_disjoint out b /\ eq_or_disjoint a b /\
    F.inv_lazy_reduced2 h a /\ F.inv_lazy_reduced2 h b)
  (ensures  fun h0 _ h1 -> modifies (loc out) h0 h1 /\
    F.inv_lazy_reduced2 h1 out /\
    F.feval h1 out == S.fadd (F.feval h0 a) (F.feval h0 b))
let felem_add a b out =
  let h0 = ST.get () in
  BL.fadd5_lemma (1,1,1,1,2) (1,1,1,1,2) (F.as_felem5 h0 a) (F.as_felem5 h0 b);
  F.fadd out a b;
  let h1 = ST.get () in
  assert (F.felem_fits5 (F.as_felem5 h1 out) (2,2,2,2,4));
  BL.normalize_weak5_lemma (2,2,2,2,4) (F.as_felem5 h1 out);
  F.fnormalize_weak out out
val felem_add (a b out:F.felem) : Stack unit
  (requires fun h ->
    live h a /\ live h b /\ live h out /\
    eq_or_disjoint out a /\ eq_or_disjoint out b /\ eq_or_disjoint a b /\
    F.inv_lazy_reduced2 h a /\ F.inv_lazy_reduced2 h b)
  (ensures  fun h0 _ h1 -> modifies (loc out) h0 h1 /\
    F.inv_lazy_reduced2 h1 out /\
    F.feval h1 out == S.fadd (F.feval h0 a) (F.feval h0 b))
let felem_add a b out =
let h0 = ST.get () in
BL.fadd5_lemma (1, 1, 1, 1, 2) (1, 1, 1, 1, 2) (F.as_felem5 h0 a) (F.as_felem5 h0 b);
F.fadd out a b;
let h1 = ST.get () in
assert (F.felem_fits5 (F.as_felem5 h1 out) (2, 2, 2, 2, 4));
BL.normalize_weak5_lemma (2, 2, 2, 2, 4) (F.as_felem5 h1 out);
F.fnormalize_weak out out
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.fnormalize_weak Prims.unit Hacl.Spec.K256.Field52.Lemmas.normalize_weak5_lemma FStar.Pervasives.Native.Mktuple5 Prims.nat Hacl.K256.Field.as_felem5 Prims._assert Hacl.Spec.K256.Field52.Definitions.felem_fits5 FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Hacl.K256.Field.fadd Hacl.Spec.K256.Field52.Lemmas.fadd5_lemma
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)

let mk_felem_one f =
  Math.Lemmas.small_mod S.one S.prime;
  F.set_one f


[@@ Comment "Write `a + b mod p` in `out`.

  The arguments `a`, `b`, and the outparam `out` are meant to be 5 limbs in size, i.e., uint64_t[5].

  Before calling this function, the caller will need to ensure that the following
  precondition is observed.
  • `a`, `b`, and `out` are either pairwise disjoint or equal"]
val felem_add (a b out:F.felem) : Stack unit
  (requires fun h ->
    live h a /\ live h b /\ live h out /\
    eq_or_disjoint out a /\ eq_or_disjoint out b /\ eq_or_disjoint a b /\
    F.inv_lazy_reduced2 h a /\ F.inv_lazy_reduced2 h b)
  (ensures  fun h0 _ h1 -> modifies (loc out) h0 h1 /\
    F.inv_lazy_reduced2 h1 out /\
    F.feval h1 out == S.fadd (F.feval h0 a) (F.feval h0 b))
val felem_add (a b out:F.felem) : Stack unit
  (requires fun h ->
    live h a /\ live h b /\ live h out /\
    eq_or_disjoint out a /\ eq_or_disjoint out b /\ eq_or_disjoint a b /\
    F.inv_lazy_reduced2 h a /\ F.inv_lazy_reduced2 h b)
  (ensures  fun h0 _ h1 -> modifies (loc out) h0 h1 /\
    F.inv_lazy_reduced2 h1 out /\
    F.feval h1 out == S.fadd (F.feval h0 a) (F.feval h0 b))
a: Hacl.K256.Field.felem -> b: Hacl.K256.Field.felem -> out: Hacl.K256.Field.felem
  -> FStar.HyperStack.ST.Stack Prims.unit