val reverse_slice1: #t:limb_t -> #len:size_pos -> b:lbignum t len ->
  Lemma (slice (reverse b) 1 len == reverse (slice b 0 (len - 1)))
let reverse_slice1 #t #len b =
  let lemma_aux (i:nat{i < len - 1}) :
    Lemma ((slice (reverse b) 1 len).[i] == (reverse (slice b 0 (len - 1))).[i]) = () in

  Classical.forall_intro lemma_aux;
  eq_intro (slice (reverse b) 1 len) (reverse (slice b 0 (len - 1)))
val reverse_slice1: #t:limb_t -> #len:size_pos -> b:lbignum t len ->
  Lemma (slice (reverse b) 1 len == reverse (slice b 0 (len - 1)))
let reverse_slice1 #t #len b =
let lemma_aux (i: nat{i < len - 1})
    : Lemma ((slice (reverse b) 1 len).[ i ] == (reverse (slice b 0 (len - 1))).[ i ]) =
  ()
in
Classical.forall_intro lemma_aux;
eq_intro (slice (reverse b) 1 len) (reverse (slice b 0 (len - 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_pos Hacl.Spec.Bignum.Definitions.lbignum Lib.Sequence.eq_intro Hacl.Spec.Bignum.Definitions.limb Prims.op_Subtraction Lib.Sequence.slice Hacl.Spec.Bignum.Convert.reverse Prims.unit FStar.Classical.forall_intro Prims.nat Prims.b2t Prims.op_LessThan Prims.eq2 Prims.l_or FStar.Seq.Base.index Lib.Sequence.to_seq Lib.Sequence.op_String_Access Prims.l_True Prims.squash Lib.Sequence.index Prims.Nil FStar.Pervasives.pattern
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)

let bn_to_bytes_be_f #t len b i () =
  (), uint_to_bytes_be b.[len - i - 1]


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

let bn_to_bytes_be_ #t len b =
  let a_spec (i:nat{i <= len}) = unit in
  let _, o = generate_blocks (numbytes t) len len a_spec
    (bn_to_bytes_be_f len b) () in
  o


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

let bn_to_bytes_be #t len b =
  let bnLen = blocks len (numbytes t) in
  let tmpLen = numbytes t * bnLen in
  let tmp = bn_to_bytes_be_ bnLen b in
  sub tmp (tmpLen - len) len


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

let bn_to_bytes_le #t len b =
  let bnLen = blocks len (numbytes t) in
  let tmpLen = numbytes t * bnLen in
  let tmp = uints_to_bytes_le b in
  sub tmp 0 len

///
///  Lemmas
///

val reverse: #t:limb_t -> #len:size_nat -> b:lbignum t len -> lbignum t len
let reverse #t #len b = createi len (fun i -> b.[len - i - 1])


val twice_reverse: #t:limb_t -> #len:size_nat -> b:lbignum t len -> Lemma (reverse (reverse b) == b)
let twice_reverse #t #len b =
  let lemma_aux (i:nat{i < len}) : Lemma ((reverse (reverse b)).[i] == b.[i]) = () in

  Classical.forall_intro lemma_aux;
  eq_intro (reverse (reverse b)) b


val reverse_slice1: #t:limb_t -> #len:size_pos -> b:lbignum t len ->
val reverse_slice1: #t:limb_t -> #len:size_pos -> b:lbignum t len ->
  Lemma (slice (reverse b) 1 len == reverse (slice b 0 (len - 1)))
b: Hacl.Spec.Bignum.Definitions.lbignum t len
  -> FStar.Pervasives.Lemma
    (ensures
      Lib.Sequence.slice (Hacl.Spec.Bignum.Convert.reverse b) 1 len ==
      Hacl.Spec.Bignum.Convert.reverse (Lib.Sequence.slice b 0 (len - 1)))