val fmul2_: fmul2_t M64 True
let fmul2_ out f1 f2 tmp =
  let out1 = B.sub out 0ul 4ul in
  let out2 = B.sub out 4ul 4ul in
  let f11 = B.sub f1 0ul 4ul in
  let f12 = B.sub f1 4ul 4ul in
  let f21 = B.sub f2 0ul 4ul in
  let f22 = B.sub f2 4ul 4ul in
  fmul_ out1 f11 f21 tmp;
  fmul_ out2 f12 f22 tmp
val fmul2_: fmul2_t M64 True
let fmul2_ out f1 f2 tmp =
let out1 = B.sub out 0ul 4ul in
let out2 = B.sub out 4ul 4ul in
let f11 = B.sub f1 0ul 4ul in
let f12 = B.sub f1 4ul 4ul in
let f21 = B.sub f2 0ul 4ul in
let f22 = B.sub f2 4ul 4ul in
fmul_ out1 f11 f21 tmp;
fmul_ out2 f12 f22 tmp
Hacl.Impl.Curve25519.Field64.Hacl.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.Loops.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.Bignum.Lib.fst.checked Hacl.Spec.Bignum.Definitions.fst.checked Hacl.Spec.Bignum.fsti.checked Hacl.Bignum.Definitions.fst.checked Hacl.Bignum.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.Impl.Curve25519.Field64.Hacl.fst
Hacl.Impl.Curve25519.Fields.Core.felem2 Hacl.Impl.Curve25519.Fields.Core.M64 Hacl.Impl.Curve25519.Fields.Core.felem_wide2 Hacl.Impl.Curve25519.Field64.Hacl.fmul_ Prims.unit Lib.Buffer.lbuffer_t Lib.Buffer.MUT Lib.IntTypes.int_t Lib.IntTypes.U64 Lib.IntTypes.SEC FStar.UInt32.uint_to_t FStar.UInt32.t Lib.Buffer.sub Hacl.Impl.Curve25519.Fields.Core.limb Lib.IntTypes.op_Plus_Dot Lib.IntTypes.U32 Lib.IntTypes.PUB Hacl.Impl.Curve25519.Fields.Core.nlimb FStar.UInt32.__uint_to_t
module Hacl.Impl.Curve25519.Field64.Hacl

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

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

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

module CD = Hacl.Spec.Curve25519.Field64.Definition
module CC = Hacl.Spec.Curve25519.Field64.Core

module BN = Hacl.Bignum
module BD = Hacl.Bignum.Definitions
module SB = Hacl.Spec.Bignum
module SD = Hacl.Spec.Bignum.Definitions

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


[@CInline]
let add1_ out f1 f2 =
  let h0 = ST.get () in
  let c = BN.bn_add1 4ul f1 f2 out in
  let h1 = ST.get () in
  assert (let c1, r1 = CC.add1 (as_seq h0 f1) f2 in c == c1 /\ as_seq h1 out == r1);
  CD.bn_v_is_as_nat (as_seq h0 f1);
  CD.bn_v_is_as_nat (as_seq h1 out);
  c


[@CInline]
let fadd_ out f1 f2 =
  let h0 = ST.get () in
  let c0 = BN.bn_add_eq_len 4ul f1 f2 out in
  let c = BN.bn_add1 4ul out (c0 *. u64 38) out in
  out.(0ul) <- out.(0ul) +. c *. u64 38;
  let h1 = ST.get () in
  assert (as_seq h1 out == CC.fadd4 (as_seq h0 f1) (as_seq h0 f2));
  CD.bn_v_is_as_nat (as_seq h0 f1);
  CD.bn_v_is_as_nat (as_seq h0 f2);
  CD.bn_v_is_as_nat (as_seq h1 out)


[@CInline]
let fsub_ out f1 f2 =
  let h0 = ST.get () in
  let c0 = BN.bn_sub_eq_len 4ul f1 f2 out in
  let c = BN.bn_sub1 4ul out (c0 *! u64 38) out in
  out.(0ul) <- out.(0ul) -. c *. u64 38;
  let h1 = ST.get () in
  assert (as_seq h1 out == CC.fsub4 (as_seq h0 f1) (as_seq h0 f2));
  CD.bn_v_is_as_nat (as_seq h0 f1);
  CD.bn_v_is_as_nat (as_seq h0 f2);
  CD.bn_v_is_as_nat (as_seq h1 out)


[@CInline]
let fmul_ out f1 f2 tmp =
  let h0 = ST.get () in
  let tmp0 = sub tmp 0ul 8ul in
  BN.bn_mul 4ul 4ul f1 f2 tmp0;
  let c0 = BN.bn_mul1_lshift_add_in_place 4ul (sub tmp0 4ul 4ul) (u64 38) 4ul 0ul (sub tmp0 0ul 4ul) in
  let c = BN.bn_add1 4ul (sub tmp0 0ul 4ul) (c0 *. u64 38) out in
  out.(0ul) <- out.(0ul) +. c *. u64 38;
  let h1 = ST.get () in
  assert (as_seq h1 out == CC.fmul4 (as_seq h0 f1) (as_seq h0 f2));
  CD.bn_v_is_as_nat (as_seq h0 f1);
  CD.bn_v_is_as_nat (as_seq h0 f2);
  CD.bn_v_is_as_nat (as_seq h1 out)
val fmul2_: fmul2_t M64 True
Hacl.Impl.Curve25519.Fields.Core.fmul2_t Hacl.Impl.Curve25519.Fields.Core.M64 Prims.l_True