val ladder_step:
    #s:field_spec
  -> k:scalar
  -> q:point s
  -> i:size_t{v i < 251}
  -> p01_tmp1_swap:lbuffer (limb s) (8ul *! nlimb s +! 1ul)
  -> tmp2:felem_wide2 s
  -> Stack unit
    (requires fun h0 ->
      live h0 k /\ live h0 q /\ live h0 p01_tmp1_swap /\ live h0 tmp2 /\
      LowStar.Monotonic.Buffer.all_disjoint [loc k; loc q; loc p01_tmp1_swap; loc tmp2] /\
     (let nq = gsub p01_tmp1_swap 0ul (2ul *! nlimb s) in
      let nq_p1 = gsub p01_tmp1_swap (2ul *! nlimb s) (2ul *! nlimb s) in
      let bit : lbuffer uint64 1ul = gsub p01_tmp1_swap (8ul *! nlimb s) 1ul in
      v (LSeq.index (as_seq h0 bit) 0) <= 1 /\
      state_inv_t h0 (get_x q) /\ state_inv_t h0 (get_z q) /\
      state_inv_t h0 (get_x nq) /\ state_inv_t h0 (get_z nq) /\
      state_inv_t h0 (get_x nq_p1) /\ state_inv_t h0 (get_z nq_p1)))
    (ensures  fun h0 _ h1 ->
      modifies (loc p01_tmp1_swap |+| loc tmp2) h0 h1 /\
     (let nq = gsub p01_tmp1_swap 0ul (2ul *! nlimb s) in
      let nq_p1 = gsub p01_tmp1_swap (2ul *! nlimb s) (2ul *! nlimb s) in
      let bit : lbuffer uint64 1ul = gsub p01_tmp1_swap (8ul *! nlimb s) 1ul in
      let (p0, p1, b) = S.ladder_step (as_seq h0 k) (fget_xz h0 q) (v i)
	(fget_xz h0 nq, fget_xz h0 nq_p1, LSeq.index (as_seq h0 bit) 0) in
      p0 == fget_xz h1 nq /\ p1 == fget_xz h1 nq_p1 /\
      b == LSeq.index (as_seq h1 bit) 0 /\
      v (LSeq.index (as_seq h1 bit) 0) <= 1 /\
      state_inv_t h1 (get_x q) /\ state_inv_t h1 (get_z q) /\
      state_inv_t h1 (get_x nq) /\ state_inv_t h1 (get_z nq) /\
      state_inv_t h1 (get_x nq_p1) /\ state_inv_t h1 (get_z nq_p1)))
let ladder_step #s k q i p01_tmp1_swap tmp2 =
  let p01_tmp1 = sub p01_tmp1_swap 0ul (8ul *! nlimb s) in
  let swap : lbuffer uint64 1ul = sub p01_tmp1_swap (8ul *! nlimb s) 1ul in
  let nq = sub p01_tmp1 0ul (2ul *! nlimb s) in
  let nq_p1 = sub p01_tmp1 (2ul *! nlimb s) (2ul *! nlimb s) in

  assert (gsub p01_tmp1_swap 0ul (2ul *! nlimb s) == nq);
  assert (gsub p01_tmp1_swap (2ul *! nlimb s) (2ul *! nlimb s) == nq_p1);
  assert (gsub p01_tmp1 0ul (2ul *! nlimb s) == nq);
  assert (gsub p01_tmp1 (2ul *! nlimb s) (2ul *! nlimb s) == nq_p1);
  assert (gsub p01_tmp1_swap 0ul (8ul *! nlimb s) == p01_tmp1);
  assert (gsub p01_tmp1_swap (8ul *! nlimb s) 1ul == swap);

  let h0 = ST.get () in
  let bit = scalar_bit k (253ul -. i) in
  assert (v bit == v (S.ith_bit (as_seq h0 k) (253 - v i)));
  let sw = swap.(0ul) ^. bit in
  logxor_lemma1 (LSeq.index (as_seq h0 swap) 0) bit;
  cswap2 #s sw nq nq_p1;
  point_add_and_double #s q p01_tmp1 tmp2;
  swap.(0ul) <- bit
val ladder_step:
    #s:field_spec
  -> k:scalar
  -> q:point s
  -> i:size_t{v i < 251}
  -> p01_tmp1_swap:lbuffer (limb s) (8ul *! nlimb s +! 1ul)
  -> tmp2:felem_wide2 s
  -> Stack unit
    (requires fun h0 ->
      live h0 k /\ live h0 q /\ live h0 p01_tmp1_swap /\ live h0 tmp2 /\
      LowStar.Monotonic.Buffer.all_disjoint [loc k; loc q; loc p01_tmp1_swap; loc tmp2] /\
     (let nq = gsub p01_tmp1_swap 0ul (2ul *! nlimb s) in
      let nq_p1 = gsub p01_tmp1_swap (2ul *! nlimb s) (2ul *! nlimb s) in
      let bit : lbuffer uint64 1ul = gsub p01_tmp1_swap (8ul *! nlimb s) 1ul in
      v (LSeq.index (as_seq h0 bit) 0) <= 1 /\
      state_inv_t h0 (get_x q) /\ state_inv_t h0 (get_z q) /\
      state_inv_t h0 (get_x nq) /\ state_inv_t h0 (get_z nq) /\
      state_inv_t h0 (get_x nq_p1) /\ state_inv_t h0 (get_z nq_p1)))
    (ensures  fun h0 _ h1 ->
      modifies (loc p01_tmp1_swap |+| loc tmp2) h0 h1 /\
     (let nq = gsub p01_tmp1_swap 0ul (2ul *! nlimb s) in
      let nq_p1 = gsub p01_tmp1_swap (2ul *! nlimb s) (2ul *! nlimb s) in
      let bit : lbuffer uint64 1ul = gsub p01_tmp1_swap (8ul *! nlimb s) 1ul in
      let (p0, p1, b) = S.ladder_step (as_seq h0 k) (fget_xz h0 q) (v i)
	(fget_xz h0 nq, fget_xz h0 nq_p1, LSeq.index (as_seq h0 bit) 0) in
      p0 == fget_xz h1 nq /\ p1 == fget_xz h1 nq_p1 /\
      b == LSeq.index (as_seq h1 bit) 0 /\
      v (LSeq.index (as_seq h1 bit) 0) <= 1 /\
      state_inv_t h1 (get_x q) /\ state_inv_t h1 (get_z q) /\
      state_inv_t h1 (get_x nq) /\ state_inv_t h1 (get_z nq) /\
      state_inv_t h1 (get_x nq_p1) /\ state_inv_t h1 (get_z nq_p1)))
let ladder_step #s k q i p01_tmp1_swap tmp2 =
let p01_tmp1 = sub p01_tmp1_swap 0ul (8ul *! nlimb s) in
let swap:lbuffer uint64 1ul = sub p01_tmp1_swap (8ul *! nlimb s) 1ul in
let nq = sub p01_tmp1 0ul (2ul *! nlimb s) in
let nq_p1 = sub p01_tmp1 (2ul *! nlimb s) (2ul *! nlimb s) in
assert (gsub p01_tmp1_swap 0ul (2ul *! nlimb s) == nq);
assert (gsub p01_tmp1_swap (2ul *! nlimb s) (2ul *! nlimb s) == nq_p1);
assert (gsub p01_tmp1 0ul (2ul *! nlimb s) == nq);
assert (gsub p01_tmp1 (2ul *! nlimb s) (2ul *! nlimb s) == nq_p1);
assert (gsub p01_tmp1_swap 0ul (8ul *! nlimb s) == p01_tmp1);
assert (gsub p01_tmp1_swap (8ul *! nlimb s) 1ul == swap);
let h0 = ST.get () in
let bit = scalar_bit k (253ul -. i) in
assert (v bit == v (S.ith_bit (as_seq h0 k) (253 - v i)));
let sw = swap.(0ul) ^. bit in
logxor_lemma1 (LSeq.index (as_seq h0 swap) 0) bit;
cswap2 #s sw nq nq_p1;
point_add_and_double #s q p01_tmp1 tmp2;
swap.(0ul) <- bit
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 Hacl.Impl.Curve25519.Generic.scalar Hacl.Impl.Curve25519.AddAndDouble.point Lib.IntTypes.size_t Prims.b2t Prims.op_LessThan Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.Buffer.lbuffer Hacl.Impl.Curve25519.Fields.Core.limb Lib.IntTypes.op_Plus_Bang Lib.IntTypes.op_Star_Bang FStar.UInt32.__uint_to_t Hacl.Impl.Curve25519.Fields.Core.nlimb Hacl.Impl.Curve25519.Fields.Core.felem_wide2 Lib.Buffer.op_Array_Assignment Lib.IntTypes.int_t Lib.IntTypes.U64 Lib.IntTypes.SEC FStar.UInt32.uint_to_t Prims.unit Hacl.Impl.Curve25519.AddAndDouble.point_add_and_double Hacl.Impl.Curve25519.Generic.cswap2 Lib.IntTypes.logxor_lemma1 Lib.Sequence.index Lib.Buffer.as_seq Lib.Buffer.MUT Lib.IntTypes.op_Hat_Dot Lib.Buffer.op_Array_Access Prims._assert Prims.eq2 Lib.IntTypes.range_t Spec.Curve25519.ith_bit Lib.IntTypes.uint8 Prims.op_Subtraction Hacl.Impl.Curve25519.Generic.scalar_bit Lib.IntTypes.op_Subtraction_Dot Lib.IntTypes.uint64 FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Lib.Buffer.buffer_t Prims.l_or Prims.int Prims.op_GreaterThanOrEqual Lib.IntTypes.range Lib.Buffer.length FStar.UInt32.t Lib.Buffer.gsub Lib.Buffer.lbuffer_t Lib.IntTypes.mul Lib.Buffer.sub
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 ]
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()

// TODO: why re-define the signature here?
val cswap2:
    #s:field_spec
  -> bit:uint64{v bit <= 1}
  -> p1:felem2 s
  -> p2:felem2 s
  -> Stack unit
    (requires fun h0 ->
      live h0 p1 /\ live h0 p2 /\ disjoint p1 p2)
    (ensures  fun h0 _ h1 ->
      modifies (loc p1 |+| loc p2) h0 h1 /\
      (v bit == 1 ==> as_seq h1 p1 == as_seq h0 p2 /\ as_seq h1 p2 == as_seq h0 p1) /\
      (v bit == 0 ==> as_seq h1 p1 == as_seq h0 p1 /\ as_seq h1 p2 == as_seq h0 p2) /\
      (fget_xz h1 p1, fget_xz h1 p2) == S.cswap2 bit (fget_xz h0 p1) (fget_xz h0 p2))
[@ Meta.Attribute.inline_ ]
let cswap2 #s bit p0 p1 =
  C.cswap2 #s bit p0 p1

#set-options "--z3rlimit 150 --fuel 0 --ifuel 1"

val ladder_step:
    #s:field_spec
  -> k:scalar
  -> q:point s
  -> i:size_t{v i < 251}
  -> p01_tmp1_swap:lbuffer (limb s) (8ul *! nlimb s +! 1ul)
  -> tmp2:felem_wide2 s
  -> Stack unit
    (requires fun h0 ->
      live h0 k /\ live h0 q /\ live h0 p01_tmp1_swap /\ live h0 tmp2 /\
      LowStar.Monotonic.Buffer.all_disjoint [loc k; loc q; loc p01_tmp1_swap; loc tmp2] /\
     (let nq = gsub p01_tmp1_swap 0ul (2ul *! nlimb s) in
      let nq_p1 = gsub p01_tmp1_swap (2ul *! nlimb s) (2ul *! nlimb s) in
      let bit : lbuffer uint64 1ul = gsub p01_tmp1_swap (8ul *! nlimb s) 1ul in
      v (LSeq.index (as_seq h0 bit) 0) <= 1 /\
      state_inv_t h0 (get_x q) /\ state_inv_t h0 (get_z q) /\
      state_inv_t h0 (get_x nq) /\ state_inv_t h0 (get_z nq) /\
      state_inv_t h0 (get_x nq_p1) /\ state_inv_t h0 (get_z nq_p1)))
    (ensures  fun h0 _ h1 ->
      modifies (loc p01_tmp1_swap |+| loc tmp2) h0 h1 /\
     (let nq = gsub p01_tmp1_swap 0ul (2ul *! nlimb s) in
      let nq_p1 = gsub p01_tmp1_swap (2ul *! nlimb s) (2ul *! nlimb s) in
      let bit : lbuffer uint64 1ul = gsub p01_tmp1_swap (8ul *! nlimb s) 1ul in
      let (p0, p1, b) = S.ladder_step (as_seq h0 k) (fget_xz h0 q) (v i)
	(fget_xz h0 nq, fget_xz h0 nq_p1, LSeq.index (as_seq h0 bit) 0) in
      p0 == fget_xz h1 nq /\ p1 == fget_xz h1 nq_p1 /\
      b == LSeq.index (as_seq h1 bit) 0 /\
      v (LSeq.index (as_seq h1 bit) 0) <= 1 /\
      state_inv_t h1 (get_x q) /\ state_inv_t h1 (get_z q) /\
      state_inv_t h1 (get_x nq) /\ state_inv_t h1 (get_z nq) /\
      state_inv_t h1 (get_x nq_p1) /\ state_inv_t h1 (get_z nq_p1)))
val ladder_step:
    #s:field_spec
  -> k:scalar
  -> q:point s
  -> i:size_t{v i < 251}
  -> p01_tmp1_swap:lbuffer (limb s) (8ul *! nlimb s +! 1ul)
  -> tmp2:felem_wide2 s
  -> Stack unit
    (requires fun h0 ->
      live h0 k /\ live h0 q /\ live h0 p01_tmp1_swap /\ live h0 tmp2 /\
      LowStar.Monotonic.Buffer.all_disjoint [loc k; loc q; loc p01_tmp1_swap; loc tmp2] /\
     (let nq = gsub p01_tmp1_swap 0ul (2ul *! nlimb s) in
      let nq_p1 = gsub p01_tmp1_swap (2ul *! nlimb s) (2ul *! nlimb s) in
      let bit : lbuffer uint64 1ul = gsub p01_tmp1_swap (8ul *! nlimb s) 1ul in
      v (LSeq.index (as_seq h0 bit) 0) <= 1 /\
      state_inv_t h0 (get_x q) /\ state_inv_t h0 (get_z q) /\
      state_inv_t h0 (get_x nq) /\ state_inv_t h0 (get_z nq) /\
      state_inv_t h0 (get_x nq_p1) /\ state_inv_t h0 (get_z nq_p1)))
    (ensures  fun h0 _ h1 ->
      modifies (loc p01_tmp1_swap |+| loc tmp2) h0 h1 /\
     (let nq = gsub p01_tmp1_swap 0ul (2ul *! nlimb s) in
      let nq_p1 = gsub p01_tmp1_swap (2ul *! nlimb s) (2ul *! nlimb s) in
      let bit : lbuffer uint64 1ul = gsub p01_tmp1_swap (8ul *! nlimb s) 1ul in
      let (p0, p1, b) = S.ladder_step (as_seq h0 k) (fget_xz h0 q) (v i)
	(fget_xz h0 nq, fget_xz h0 nq_p1, LSeq.index (as_seq h0 bit) 0) in
      p0 == fget_xz h1 nq /\ p1 == fget_xz h1 nq_p1 /\
      b == LSeq.index (as_seq h1 bit) 0 /\
      v (LSeq.index (as_seq h1 bit) 0) <= 1 /\
      state_inv_t h1 (get_x q) /\ state_inv_t h1 (get_z q) /\
      state_inv_t h1 (get_x nq) /\ state_inv_t h1 (get_z nq) /\
      state_inv_t h1 (get_x nq_p1) /\ state_inv_t h1 (get_z nq_p1)))

    k: Hacl.Impl.Curve25519.Generic.scalar ->
    q: Hacl.Impl.Curve25519.AddAndDouble.point s ->
    i: Lib.IntTypes.size_t{Lib.IntTypes.v i < 251} ->
    p01_tmp1_swap:
      Lib.Buffer.lbuffer (Hacl.Impl.Curve25519.Fields.Core.limb s)
        (8ul *! Hacl.Impl.Curve25519.Fields.Core.nlimb s +! 1ul) ->
    tmp2: Hacl.Impl.Curve25519.Fields.Core.felem_wide2 s
  -> FStar.HyperStack.ST.Stack Prims.unit