val lemma_nat_from_bytes_be_zeroes: len:size_nat -> b:lseq uint8 len -> Lemma
  (requires (forall (i:nat). i < len ==> b.[i] == u8 0))
  (ensures  nat_from_intseq_be b == 0)
let rec lemma_nat_from_bytes_be_zeroes len b =
  if len = 0 then ()
  else begin
    nat_from_intseq_be_slice_lemma #U8 #SEC #len b 1;
    nat_from_intseq_be_lemma0 (slice b 0 1);
    lemma_nat_from_bytes_be_zeroes (len-1) (slice b 1 len) end
val lemma_nat_from_bytes_be_zeroes: len:size_nat -> b:lseq uint8 len -> Lemma
  (requires (forall (i:nat). i < len ==> b.[i] == u8 0))
  (ensures  nat_from_intseq_be b == 0)
let rec lemma_nat_from_bytes_be_zeroes len b =
if len = 0
then ()
else
  (nat_from_intseq_be_slice_lemma #U8 #SEC #len b 1;
    nat_from_intseq_be_lemma0 (slice b 0 1);
    lemma_nat_from_bytes_be_zeroes (len - 1) (slice b 1 len))
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
Lib.IntTypes.size_nat Lib.Sequence.lseq Lib.IntTypes.uint8 Prims.op_Equality Prims.int Prims.bool Hacl.Spec.Bignum.Convert.lemma_nat_from_bytes_be_zeroes Prims.op_Subtraction Lib.Sequence.slice Prims.unit Lib.ByteSequence.nat_from_intseq_be_lemma0 Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.ByteSequence.nat_from_intseq_be_slice_lemma
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 ->
  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 bn_from_bytes_be_is_uints_from_bytes_be_reverse:
    #t:limb_t
  -> len:size_nat{numbytes t * len <= max_size_t}
  -> b:lseq uint8 (numbytes t * len) ->
  Lemma (bn_from_bytes_be_ len b == reverse (uints_from_bytes_be b))

let bn_from_bytes_be_is_uints_from_bytes_be_reverse #t len b =
  let lemma_aux (i:nat{i < len}) :
    Lemma ((bn_from_bytes_be_ len b).[i] == (reverse #t #len (uints_from_bytes_be b)).[i])
  =
    index_uints_from_bytes_be #t #SEC #len b (len - i - 1) in

  Classical.forall_intro lemma_aux;
  eq_intro (bn_from_bytes_be_ len b) (reverse (uints_from_bytes_be b))


val bn_v_is_nat_from_intseq_be_lemma: #t:limb_t -> len:size_nat -> b:lbignum t len ->
  Lemma (bn_v b == nat_from_intseq_be (reverse b))

let rec bn_v_is_nat_from_intseq_be_lemma #t len b =
  if len = 0 then bn_eval0 b
  else begin
    let b1 = slice b 0 (len - 1) in
    bn_v_is_nat_from_intseq_be_lemma (len - 1) b1;
    assert (bn_v b1 == nat_from_intseq_be (reverse b1));

    bn_eval_split_i #t #len b (len - 1);
    bn_eval_unfold_i #t #1 (slice b (len - 1) len) 1;
    bn_eval0 #t #1 (slice b (len - 1) len);
    assert (bn_v (slice b (len - 1) len) == v b.[len - 1]);
    assert (bn_v b == nat_from_intseq_be (reverse b1) + pow2 (bits t * (len - 1)) * v b.[len - 1]);

    nat_from_intseq_be_slice_lemma (reverse b) 1;
    reverse_slice1 #t #len b;
    assert ((reverse b).[0] == b.[len - 1]);
    nat_from_intseq_be_lemma0 (slice (reverse b) 0 1);
    assert (nat_from_intseq_be (slice (reverse b) 0 1) == v b.[len - 1]);
    assert  (bn_v b == nat_from_intseq_be (reverse b));
    () end


val bn_from_bytes_be_lemma_:
    #t:limb_t
  -> len:size_nat{numbytes t * len <= max_size_t}
  -> b:lseq uint8 (numbytes t * len) ->
  Lemma (bn_v (bn_from_bytes_be_ len b) == nat_from_bytes_be b)

let bn_from_bytes_be_lemma_ #t len b =
  bn_v_is_nat_from_intseq_be_lemma len (bn_from_bytes_be_ len b);
  bn_from_bytes_be_is_uints_from_bytes_be_reverse len b;
  twice_reverse (uints_from_bytes_be #t #SEC #len b);
  assert (bn_v (bn_from_bytes_be_ len b) == nat_from_intseq_be (uints_from_bytes_be #t #SEC #len b));
  uints_from_bytes_be_nat_lemma #t #SEC #len b;
  assert (nat_from_intseq_be (uints_from_bytes_be #t #SEC #len b) == nat_from_bytes_be b)


val lemma_nat_from_bytes_be_zeroes: len:size_nat -> b:lseq uint8 len -> Lemma
  (requires (forall (i:nat). i < len ==> b.[i] == u8 0))
  (ensures  nat_from_intseq_be b == 0)
val lemma_nat_from_bytes_be_zeroes: len:size_nat -> b:lseq uint8 len -> Lemma
  (requires (forall (i:nat). i < len ==> b.[i] == u8 0))
  (ensures  nat_from_intseq_be b == 0)
len: Lib.IntTypes.size_nat -> b: Lib.Sequence.lseq Lib.IntTypes.uint8 len
  -> FStar.Pervasives.Lemma
      (requires forall (i: Prims.nat). i < len ==> b.[ i ] == Lib.IntTypes.u8 0)
      (ensures Lib.ByteSequence.nat_from_intseq_be b == 0)