val bn_to_bytes_be_f:
    #t:limb_t
  -> len:size_nat
  -> lbignum t len
  -> i:nat{i < len}
  -> unit ->
  unit & lseq uint8 (numbytes t)
let bn_to_bytes_be_f #t len b i () =
  (), uint_to_bytes_be b.[len - i - 1]
val bn_to_bytes_be_f:
    #t:limb_t
  -> len:size_nat
  -> lbignum t len
  -> i:nat{i < len}
  -> unit ->
  unit & lseq uint8 (numbytes t)
let bn_to_bytes_be_f #t len b i () =
(), uint_to_bytes_be b.[ len - i - 1 ]
Hacl.Spec.Bignum.Convert.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Hacl.Spec.Bignum.Definitions.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Hacl.Spec.Bignum.Convert.fst
Hacl.Spec.Bignum.Definitions.limb_t Lib.IntTypes.size_nat Hacl.Spec.Bignum.Definitions.lbignum Prims.nat Prims.b2t Prims.op_LessThan Prims.unit FStar.Pervasives.Native.Mktuple2 Lib.Sequence.lseq Lib.IntTypes.uint8 Lib.IntTypes.numbytes Lib.ByteSequence.uint_to_bytes_be Lib.IntTypes.SEC Lib.Sequence.op_String_Access Hacl.Spec.Bignum.Definitions.limb Prims.op_Subtraction FStar.Pervasives.Native.tuple2
module Hacl.Spec.Bignum.Convert

open FStar.Mul

open Lib.IntTypes
open Lib.Sequence
open Lib.ByteSequence

open Hacl.Spec.Bignum.Definitions


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

val bn_from_uint: #t:limb_t -> len:size_pos -> x:limb t -> lbignum t len
let bn_from_uint #t len x =
  let b = create len (uint #t 0) in
  b.[0] <- x

val bn_from_uint_lemma: #t:limb_t -> len:size_pos -> x:limb t ->
  Lemma (bn_v (bn_from_uint len x) == uint_v x)

let bn_from_uint_lemma #t len x =
  let b = create len (uint #t 0) in
  let b = b.[0] <- x in
  bn_eval_split_i b 1;
  assert (bn_v b == bn_v (slice b 0 1) + pow2 (bits t) * bn_v (slice b 1 len));
  eq_intro (slice b 1 len) (create (len - 1) (uint #t 0));
  bn_eval_zeroes #t (len - 1) (len - 1);
  assert (bn_v b == bn_v (slice b 0 1));
  bn_eval1 (slice b 0 1)


val bn_from_bytes_be_f:
    #t:limb_t
  -> len:size_nat{numbytes t * len <= max_size_t}
  -> lseq uint8 (numbytes t * len)
  -> i:nat{i < len} ->
  limb t

let bn_from_bytes_be_f #t len b i =
  uint_from_bytes_be (sub b ((len - i - 1) * numbytes t) (numbytes t))


val bn_from_bytes_be_:
    #t:limb_t
  -> len:size_nat{numbytes t * len <= max_size_t}
  -> lseq uint8 (numbytes t * len) ->
  lbignum t len

let bn_from_bytes_be_ #t len b =
  createi len (bn_from_bytes_be_f len b)


val bn_from_bytes_be:
    #t:limb_t
  -> len:size_pos{numbytes t * blocks len (numbytes t) <= max_size_t}
  -> lseq uint8 len ->
  lbignum t (blocks len (numbytes t))

let bn_from_bytes_be #t len b =
  let bnLen = blocks len (numbytes t) in
  let tmpLen = numbytes t * bnLen in
  let tmp = create tmpLen (u8 0) in
  let tmp = update_sub tmp (tmpLen - len) len b in
  bn_from_bytes_be_ bnLen tmp


val bn_from_bytes_le:
    #t:limb_t
  -> len:size_pos{numbytes t * blocks len (numbytes t) <= max_size_t}
  -> lseq uint8 len ->
  lbignum t (blocks len (numbytes t))

let bn_from_bytes_le #t len b =
  let bnLen = blocks len (numbytes t) in
  let tmpLen = numbytes t * bnLen in
  let tmp = create tmpLen (u8 0) in
  let tmp = update_sub tmp 0 len b in
  uints_from_bytes_le tmp


val bn_to_bytes_be_f:
    #t:limb_t
  -> len:size_nat
  -> lbignum t len
  -> i:nat{i < len}
  -> unit ->
  unit & lseq uint8 (numbytes t)
val bn_to_bytes_be_f:
    #t:limb_t
  -> len:size_nat
  -> lbignum t len
  -> i:nat{i < len}
  -> unit ->
  unit & lseq uint8 (numbytes t)

    len: Lib.IntTypes.size_nat ->
    b: Hacl.Spec.Bignum.Definitions.lbignum t len ->
    i: Prims.nat{i < len} ->
    _: Prims.unit
  -> Prims.unit * Lib.Sequence.lseq Lib.IntTypes.uint8 (Lib.IntTypes.numbytes t)