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)
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)
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.Generic.scalar Lib.IntTypes.size_t Prims.b2t Prims.op_LessThan Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.IntTypes.to_u64 Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.IntTypes.uint64 Lib.IntTypes.int_t Prims.l_or Lib.IntTypes.range Lib.IntTypes.U64 Lib.IntTypes.op_Amp_Dot Lib.IntTypes.u8 Lib.IntTypes.op_Greater_Greater_Dot Lib.IntTypes.op_Percent_Dot FStar.UInt32.__uint_to_t Lib.Buffer.op_Array_Access Lib.Buffer.MUT Lib.IntTypes.uint8 Lib.IntTypes.op_Slash_Dot Prims.unit Prims._assert Prims.eq2 Lib.IntTypes.range_t Lib.IntTypes.mod_mask FStar.Pervasives.assert_norm Prims.op_Equality Prims.int Prims.op_Subtraction Prims.pow2 Lib.IntTypes.mod_mask_lemma Lib.Sequence.index Lib.Buffer.as_seq Prims.op_Division FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get
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 /\
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)
s: Hacl.Impl.Curve25519.Generic.scalar -> n: Lib.IntTypes.size_t{Lib.IntTypes.v n < 256}
  -> FStar.HyperStack.ST.Stack Lib.IntTypes.uint64