val encode_point:
    #s:field_spec
  -> o:lbuffer uint8 32ul
  -> i:point s
  -> Stack unit
    (requires fun h0 ->
      live h0 o /\ live h0 i /\ disjoint o i /\
      state_inv_t h0 (get_x i) /\ state_inv_t h0 (get_z i))
    (ensures  fun h0 _ h1 -> modifies (loc o) h0 h1 /\
      as_seq h1 o == S.encodePoint (fget_x h0 i, fget_z h0 i))
let encode_point #s o i =
  push_frame();
  let x : felem s = sub i 0ul (nlimb s) in
  let z : felem s = sub i (nlimb s) (nlimb s) in
  let tmp = create_felem s in
  let u64s = create 4ul (u64 0) in
  let tmp_w = create (2ul `FStar.UInt32.mul` ((nwide s) <: FStar.UInt32.t)) (wide_zero s) in
  let h0 = ST.get () in
  finv tmp z tmp_w;
  fmul tmp tmp x tmp_w;
  let h1 = ST.get () in
  assert (feval h1 tmp == S.fmul (S.fpow (feval h0 z) (pow2 255 - 21)) (feval h0 x));
  assert (feval h1 tmp == S.fmul (feval h0 x) (S.fpow (feval h0 z) (pow2 255 - 21)));
  store_felem u64s tmp;
  let h2 = ST.get () in
  assert (as_seq h2 u64s == BSeq.nat_to_intseq_le 4 (feval h1 tmp));
  uints_to_bytes_le #U64 4ul o u64s;
  let h3 = ST.get () in
  BSeq.uints_to_bytes_le_nat_lemma #U64 #SEC 4 (feval h1 tmp);
  assert (as_seq h3 o == BSeq.nat_to_bytes_le 32 (feval h1 tmp));
  pop_frame()
val encode_point:
    #s:field_spec
  -> o:lbuffer uint8 32ul
  -> i:point s
  -> Stack unit
    (requires fun h0 ->
      live h0 o /\ live h0 i /\ disjoint o i /\
      state_inv_t h0 (get_x i) /\ state_inv_t h0 (get_z i))
    (ensures  fun h0 _ h1 -> modifies (loc o) h0 h1 /\
      as_seq h1 o == S.encodePoint (fget_x h0 i, fget_z h0 i))
let encode_point #s o i =
push_frame ();
let x:felem s = sub i 0ul (nlimb s) in
let z:felem s = sub i (nlimb s) (nlimb s) in
let tmp = create_felem s in
let u64s = create 4ul (u64 0) in
let tmp_w = create (2ul `FStar.UInt32.mul` ((nwide s) <: FStar.UInt32.t)) (wide_zero s) in
let h0 = ST.get () in
finv tmp z tmp_w;
fmul tmp tmp x tmp_w;
let h1 = ST.get () in
assert (feval h1 tmp == S.fmul (S.fpow (feval h0 z) (pow2 255 - 21)) (feval h0 x));
assert (feval h1 tmp == S.fmul (feval h0 x) (S.fpow (feval h0 z) (pow2 255 - 21)));
store_felem u64s tmp;
let h2 = ST.get () in
assert (as_seq h2 u64s == BSeq.nat_to_intseq_le 4 (feval h1 tmp));
uints_to_bytes_le #U64 4ul o u64s;
let h3 = ST.get () in
BSeq.uints_to_bytes_le_nat_lemma #U64 #SEC 4 (feval h1 tmp);
assert (as_seq h3 o == BSeq.nat_to_bytes_le 32 (feval h1 tmp));
pop_frame ()
Hacl.Impl.Curve25519.Generic.fst.checked
Spec.Curve25519.fst.checked prims.fst.checked Meta.Attribute.fst.checked LowStar.Monotonic.Buffer.fsti.checked Lib.Sequence.fsti.checked Lib.Loops.fsti.checked Lib.LoopCombinators.fst.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.Curve25519.Field64.Lemmas.fst.checked Hacl.Spec.Curve25519.AddAndDouble.fst.checked Hacl.Impl.Curve25519.Finv.fst.checked Hacl.Impl.Curve25519.Fields.Core.fsti.checked Hacl.Impl.Curve25519.Fields.fst.checked Hacl.Impl.Curve25519.AddAndDouble.fst.checked FStar.UInt32.fsti.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
Hacl.Impl.Curve25519.Generic.fst
Hacl.Impl.Curve25519.Fields.Core.field_spec Lib.Buffer.lbuffer Lib.IntTypes.uint8 FStar.UInt32.__uint_to_t Hacl.Impl.Curve25519.AddAndDouble.point FStar.HyperStack.ST.pop_frame Prims.unit Prims._assert Prims.eq2 Lib.Sequence.seq Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Prims.l_or Prims.l_and Prims.nat Lib.Sequence.length Prims.b2t Prims.op_LessThan Prims.pow2 FStar.Mul.op_Star Lib.IntTypes.bits Hacl.Impl.Curve25519.Fields.Core.feval Lib.ByteSequence.nat_from_intseq_le FStar.Seq.Base.length Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.Buffer.as_seq Lib.Buffer.MUT Lib.ByteSequence.nat_to_bytes_le Lib.ByteSequence.uints_to_bytes_le_nat_lemma Lib.IntTypes.U64 FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Lib.ByteBuffer.uints_to_bytes_le Lib.IntTypes.uint64 Lib.ByteSequence.nat_to_intseq_le Hacl.Impl.Curve25519.Fields.store_felem Spec.Curve25519.elem Spec.Curve25519.fmul Spec.Curve25519.fpow Prims.op_Subtraction Hacl.Impl.Curve25519.Fields.Core.fmul Hacl.Impl.Curve25519.Finv.finv Lib.Buffer.lbuffer_t Lib.IntTypes.int_t Lib.IntTypes.U128 FStar.UInt32.mul FStar.UInt32.uint_to_t FStar.UInt32.t Lib.Buffer.create Hacl.Impl.Curve25519.Fields.Core.wide Hacl.Impl.Curve25519.Fields.Core.nwide Hacl.Impl.Curve25519.Fields.Core.wide_zero Lib.IntTypes.u64 Hacl.Impl.Curve25519.Fields.Core.felem Hacl.Impl.Curve25519.Fields.create_felem Lib.Buffer.sub Hacl.Impl.Curve25519.Fields.Core.limb Lib.IntTypes.op_Plus_Bang Hacl.Impl.Curve25519.Fields.Core.nlimb FStar.HyperStack.ST.push_frame
module Hacl.Impl.Curve25519.Generic

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

open Lib.IntTypes
open Lib.Buffer
open Lib.ByteBuffer

open Hacl.Impl.Curve25519.Fields

include Hacl.Impl.Curve25519.Finv
include Hacl.Impl.Curve25519.AddAndDouble

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

module C = Hacl.Impl.Curve25519.Fields.Core

module S = Spec.Curve25519
module M = Hacl.Spec.Curve25519.AddAndDouble
module Lemmas = Hacl.Spec.Curve25519.Field64.Lemmas

friend Lib.LoopCombinators

#reset-options "--z3rlimit 200 --max_fuel 2 --using_facts_from '* -FStar.Seq -Hacl.Spec.*' --record_options"
//#set-options "--debug Hacl.Impl.Curve25519.Generic --debug_level ExtractNorm"

inline_for_extraction noextract
let scalar = lbuffer uint8 32ul

inline_for_extraction noextract
val scalar_bit:
    s:scalar
  -> n:size_t{v n < 256}
  -> Stack uint64
    (requires fun h0 -> live h0 s)
    (ensures  fun h0 r h1 -> h0 == h1 /\
      r == S.ith_bit (as_seq h0 s) (v n) /\ v r <= 1)
let scalar_bit s n =
  let h0 = ST.get () in
  mod_mask_lemma ((LSeq.index (as_seq h0 s) (v n / 8)) >>. (n %. 8ul)) 1ul;
  assert_norm (1 = pow2 1 - 1);
  assert (v (mod_mask #U8 #SEC 1ul) == v (u8 1));
  to_u64 ((s.(n /. 8ul) >>. (n %. 8ul)) &. u8 1)

inline_for_extraction noextract
val decode_point:
    #s:field_spec
  -> o:point s
  -> i:lbuffer uint8 32ul
  -> Stack unit
    (requires fun h0 -> live h0 o /\ live h0 i /\ disjoint o i)
    (ensures fun h0 _ h1 -> modifies (loc o) h0 h1 /\
      state_inv_t h1 (get_x o) /\ state_inv_t h1 (get_z o) /\
      fget_x h1 o == S.decodePoint (as_seq h0 i) /\ fget_z h1 o == 1)
[@ Meta.Attribute.specialize ]
let decode_point #s o i =
  push_frame();
  let tmp = create 4ul (u64 0) in
  let h0 = ST.get () in
  uints_from_bytes_le #U64 tmp i;
  let h1 = ST.get () in
  BSeq.uints_from_bytes_le_nat_lemma #U64 #SEC #4 (as_seq h0 i);
  assert (BSeq.nat_from_intseq_le (as_seq h1 tmp) == BSeq.nat_from_bytes_le (as_seq h0 i));
  let tmp3 = tmp.(3ul) in
  tmp.(3ul) <- tmp3 &. u64 0x7fffffffffffffff;
  mod_mask_lemma tmp3 63ul;
  assert_norm (0x7fffffffffffffff = pow2 63 - 1);
  assert (v (mod_mask #U64 #SEC 63ul) == v (u64 0x7fffffffffffffff));
  let h2 = ST.get () in
  assert (v (LSeq.index (as_seq h2 tmp) 3) < pow2 63);
  Lemmas.lemma_felem64_mod255 (as_seq h1 tmp);
  assert (BSeq.nat_from_intseq_le (as_seq h2 tmp) == BSeq.nat_from_bytes_le (as_seq h0 i) % pow2 255);
  let x : felem s = sub o 0ul (nlimb s) in
  let z : felem s = sub o (nlimb s) (nlimb s) in
  set_one z;
  load_felem x tmp;
  pop_frame()

val encode_point:
    #s:field_spec
  -> o:lbuffer uint8 32ul
  -> i:point s
  -> Stack unit
    (requires fun h0 ->
      live h0 o /\ live h0 i /\ disjoint o i /\
      state_inv_t h0 (get_x i) /\ state_inv_t h0 (get_z i))
    (ensures  fun h0 _ h1 -> modifies (loc o) h0 h1 /\
      as_seq h1 o == S.encodePoint (fget_x h0 i, fget_z h0 i))
[@ Meta.Attribute.specialize ]
val encode_point:
    #s:field_spec
  -> o:lbuffer uint8 32ul
  -> i:point s
  -> Stack unit
    (requires fun h0 ->
      live h0 o /\ live h0 i /\ disjoint o i /\
      state_inv_t h0 (get_x i) /\ state_inv_t h0 (get_z i))
    (ensures  fun h0 _ h1 -> modifies (loc o) h0 h1 /\
      as_seq h1 o == S.encodePoint (fget_x h0 i, fget_z h0 i))
o: Lib.Buffer.lbuffer Lib.IntTypes.uint8 32ul -> i: Hacl.Impl.Curve25519.AddAndDouble.point s
  -> FStar.HyperStack.ST.Stack Prims.unit