val felem_inv (a out:F.felem) : Stack unit
  (requires fun h ->
    live h a /\ live h out /\ disjoint a out /\
    F.inv_lazy_reduced2 h a)
  (ensures  fun h0 _ h1 -> modifies (loc out) h0 h1 /\
    F.inv_lazy_reduced2 h1 out /\
    F.feval h1 out == S.finv (F.feval h0 a))
let felem_inv a out =
  FI.finv out a
val felem_inv (a out:F.felem) : Stack unit
  (requires fun h ->
    live h a /\ live h out /\ disjoint a out /\
    F.inv_lazy_reduced2 h a)
  (ensures  fun h0 _ h1 -> modifies (loc out) h0 h1 /\
    F.inv_lazy_reduced2 h1 out /\
    F.feval h1 out == S.finv (F.feval h0 a))
let felem_inv a out =
FI.finv out a
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.Impl.K256.Finv.finv Prims.unit
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))

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


[@@ 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_sub (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.fsub (F.feval h0 a) (F.feval h0 b))

let felem_sub a b out =
  let h0 = ST.get () in
  BL.fsub5_lemma (1,1,1,1,2) (1,1,1,1,2) (F.as_felem5 h0 a) (F.as_felem5 h0 b) (u64 2);
  F.fsub out a b (u64 2);
  let h1 = ST.get () in
  assert (F.felem_fits5 (F.as_felem5 h1 out) (5,5,5,5,6));
  BL.normalize_weak5_lemma (5,5,5,5,6) (F.as_felem5 h1 out);
  F.fnormalize_weak out out


[@@ 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_mul (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.fmul (F.feval h0 a) (F.feval h0 b))

let felem_mul a b out =
  F.fmul out a b


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

  The argument `a`, 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` and `out` are either disjoint or equal"]
val felem_sqr (a out:F.felem) : Stack unit
  (requires fun h ->
    live h a /\ live h out /\ eq_or_disjoint out a /\
    F.inv_lazy_reduced2 h a)
  (ensures  fun h0 _ h1 -> modifies (loc out) h0 h1 /\
    F.inv_lazy_reduced2 h1 out /\
    F.feval h1 out == S.fmul (F.feval h0 a) (F.feval h0 a))

let felem_sqr a out =
  F.fsqr out a


[@@ Comment "Write `a ^ (p - 2) mod p` in `out`.

  The function computes modular multiplicative inverse if `a` <> zero.

  The argument `a`, 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` and `out` are disjoint"]
val felem_inv (a out:F.felem) : Stack unit
  (requires fun h ->
    live h a /\ live h out /\ disjoint a out /\
    F.inv_lazy_reduced2 h a)
  (ensures  fun h0 _ h1 -> modifies (loc out) h0 h1 /\
    F.inv_lazy_reduced2 h1 out /\
    F.feval h1 out == S.finv (F.feval h0 a))
val felem_inv (a out:F.felem) : Stack unit
  (requires fun h ->
    live h a /\ live h out /\ disjoint a out /\
    F.inv_lazy_reduced2 h a)
  (ensures  fun h0 _ h1 -> modifies (loc out) h0 h1 /\
    F.inv_lazy_reduced2 h1 out /\
    F.feval h1 out == S.finv (F.feval h0 a))
a: Hacl.K256.Field.felem -> out: Hacl.K256.Field.felem -> FStar.HyperStack.ST.Stack Prims.unit