val carry_pass_store: f:felem ->
  Stack unit
  (requires fun h -> live h f)
  (ensures fun h0 _ h1 ->
    modifies (loc f) h0 h1 /\
    as_seq h1 f == SC.carry_pass_store (as_seq h0 f))
let carry_pass_store f =
  let f3 = f.(3ul) in
  let top_bit = f3 >>. 63ul in
  f.(3ul) <- f3 &. u64 0x7fffffffffffffff;
  let h0 = ST.get () in
  let carry = add1 f f (u64 19 *! top_bit) in
  let h1 = ST.get () in
  assert (as_nat h1 f + v carry * pow2 256 == as_nat h0 f + 19 * v top_bit);
  S.bn_v_is_as_nat (as_seq h1 f);
  S.bn_v_is_as_nat (as_seq h0 f);
  let cr = Ghost.hide (Hacl.Spec.Curve25519.Field64.Core.add1 (as_seq h0 f) (u64 19 *! top_bit)) in
  SD.bn_eval_bound (snd cr) 4;
  assert (v (fst cr) == v carry /\ SD.bn_v (snd cr) == as_nat h1 f);
  SD.bn_eval_inj 4 (snd cr) (as_seq h1 f);
  ()
val carry_pass_store: f:felem ->
  Stack unit
  (requires fun h -> live h f)
  (ensures fun h0 _ h1 ->
    modifies (loc f) h0 h1 /\
    as_seq h1 f == SC.carry_pass_store (as_seq h0 f))
let carry_pass_store f =
let f3 = f.(3ul) in
let top_bit = f3 >>. 63ul in
f.(3ul) <- f3 &. u64 0x7fffffffffffffff;
let h0 = ST.get () in
let carry = add1 f f (u64 19 *! top_bit) in
let h1 = ST.get () in
assert (as_nat h1 f + v carry * pow2 256 == as_nat h0 f + 19 * v top_bit);
S.bn_v_is_as_nat (as_seq h1 f);
S.bn_v_is_as_nat (as_seq h0 f);
let cr = Ghost.hide (Hacl.Spec.Curve25519.Field64.Core.add1 (as_seq h0 f) (u64 19 *! top_bit)) in
SD.bn_eval_bound (snd cr) 4;
assert (v (fst cr) == v carry /\ SD.bn_v (snd cr) == as_nat h1 f);
SD.bn_eval_inj 4 (snd cr) (as_seq h1 f);
()
Hacl.Impl.Curve25519.Field64.fst.checked
Spec.Curve25519.fst.checked prims.fst.checked Meta.Attribute.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.Curve25519.Field64.Definition.fst.checked Hacl.Spec.Curve25519.Field64.Core.fst.checked Hacl.Spec.Curve25519.Field64.fst.checked Hacl.Spec.Bignum.Definitions.fst.checked Hacl.Impl.Curve25519.Lemmas.fst.checked Hacl.Impl.Curve25519.Fields.Core.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
Hacl.Impl.Curve25519.Field64.fst
Hacl.Impl.Curve25519.Field64.felem Prims.unit Hacl.Spec.Bignum.Definitions.bn_eval_inj Lib.IntTypes.U64 FStar.Pervasives.Native.snd Lib.IntTypes.uint64 Hacl.Spec.Curve25519.Field64.Core.felem FStar.Ghost.reveal FStar.Pervasives.Native.tuple2 Lib.Buffer.as_seq Lib.Buffer.MUT FStar.UInt32.__uint_to_t Prims._assert Prims.l_and Prims.eq2 Lib.IntTypes.range_t Lib.IntTypes.v Lib.IntTypes.SEC FStar.Pervasives.Native.fst Prims.nat Hacl.Spec.Bignum.Definitions.bn_v Hacl.Impl.Curve25519.Field64.as_nat Hacl.Spec.Bignum.Definitions.bn_eval_bound FStar.Ghost.erased Lib.IntTypes.int_t Hacl.Spec.Bignum.Definitions.lbignum FStar.Ghost.hide Hacl.Spec.Curve25519.Field64.Core.add1 Lib.IntTypes.op_Star_Bang Lib.IntTypes.u64 Hacl.Spec.Curve25519.Field64.Definition.bn_v_is_as_nat Prims.int Prims.op_Addition FStar.Mul.op_Star Prims.pow2 FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Hacl.Impl.Curve25519.Fields.Core.add1 Lib.Buffer.op_Array_Assignment Lib.IntTypes.op_Amp_Dot Lib.IntTypes.op_Greater_Greater_Dot Lib.Buffer.op_Array_Access
module Hacl.Impl.Curve25519.Field64

open FStar.HyperStack
open FStar.HyperStack.All
open FStar.Mul

open Lib.Sequence
open Lib.IntTypes
open Lib.Buffer

open Hacl.Impl.Curve25519.Fields.Core

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

module P = Spec.Curve25519
module S = Hacl.Spec.Curve25519.Field64.Definition
module SC = Hacl.Spec.Curve25519.Field64
module SD = Hacl.Spec.Bignum.Definitions

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

let u256 = lbuffer uint64 4ul
let u512 = lbuffer uint64 8ul
let u1024 = lbuffer uint64 16ul

let felem = lbuffer uint64 4ul
let felem2 = lbuffer uint64 8ul

noextract
let as_nat (h:mem) (e:felem) : GTot nat =
  let s = as_seq h e in
  let s0 = s.[0] in
  let s1 = s.[1] in
  let s2 = s.[2] in
  let s3 = s.[3] in
  S.as_nat4 (s0, s1, s2, s3)

noextract
let fevalh (h:mem) (f:felem) : GTot P.elem = (as_nat h f) % P.prime


inline_for_extraction noextract
val create_felem: unit ->
  StackInline felem
  (requires fun _ -> True)
  (ensures  fun h0 f h1 ->
    stack_allocated f h0 h1 (Seq.create 4 (u64 0)) /\
    as_nat h1 f == 0)

let create_felem () = create 4ul (u64 0)


inline_for_extraction noextract
val load_felem:
    f:felem
  -> u64s:lbuffer uint64 4ul ->
  Stack unit
  (requires fun h ->
    live h u64s /\ live h f /\ disjoint u64s f)
  (ensures  fun h0 _ h1 ->
    modifies (loc f) h0 h1 /\
    as_nat h1 f == BSeq.nat_from_intseq_le (as_seq h0 u64s))

let load_felem f u64s =
  let h0 = ST.get () in
  Hacl.Impl.Curve25519.Lemmas.lemma_nat_from_uints64_le_4 (as_seq h0 u64s);
  f.(0ul) <- u64s.(0ul);
  f.(1ul) <- u64s.(1ul);
  f.(2ul) <- u64s.(2ul);
  f.(3ul) <- u64s.(3ul)


val carry_pass_store: f:felem ->
  Stack unit
  (requires fun h -> live h f)
  (ensures fun h0 _ h1 ->
    modifies (loc f) h0 h1 /\
    as_seq h1 f == SC.carry_pass_store (as_seq h0 f))
val carry_pass_store: f:felem ->
  Stack unit
  (requires fun h -> live h f)
  (ensures fun h0 _ h1 ->
    modifies (loc f) h0 h1 /\
    as_seq h1 f == SC.carry_pass_store (as_seq h0 f))
f: Hacl.Impl.Curve25519.Field64.felem -> FStar.HyperStack.ST.Stack Prims.unit