val lemma_load_64_bytes (k: lbytes 64) (b0 b1 b2 b3 b4 b5 b6 b7 b8 b9: uint64)
    : Lemma
      (requires
        v b0 == nat_from_bytes_le (Seq.slice k 0 7) /\ v b1 == nat_from_bytes_le (Seq.slice k 7 14) /\
        v b2 == nat_from_bytes_le (Seq.slice k 14 21) /\
        v b3 == nat_from_bytes_le (Seq.slice k 21 28) /\
        v b4 == nat_from_bytes_le (Seq.slice k 28 35) /\
        v b5 == nat_from_bytes_le (Seq.slice k 35 42) /\
        v b6 == nat_from_bytes_le (Seq.slice k 42 49) /\
        v b7 == nat_from_bytes_le (Seq.slice k 49 56) /\
        v b8 == nat_from_bytes_le (Seq.slice k 56 63) /\ v b9 == v (Seq.index k 63))
      (ensures S56.wide_as_nat5 (b0, b1, b2, b3, b4, b5, b6, b7, b8, b9) == nat_from_bytes_le k)
let lemma_load_64_bytes (k:lbytes 64) (b0 b1 b2 b3 b4 b5 b6 b7 b8 b9:uint64) : Lemma
  (requires
    v b0 == nat_from_bytes_le (Seq.slice k 0 7) /\
    v b1 == nat_from_bytes_le (Seq.slice k 7 14) /\
    v b2 == nat_from_bytes_le (Seq.slice k 14 21) /\
    v b3 == nat_from_bytes_le (Seq.slice k 21 28) /\
    v b4 == nat_from_bytes_le (Seq.slice k 28 35) /\
    v b5 == nat_from_bytes_le (Seq.slice k 35 42) /\
    v b6 == nat_from_bytes_le (Seq.slice k 42 49) /\
    v b7 == nat_from_bytes_le (Seq.slice k 49 56) /\
    v b8 == nat_from_bytes_le (Seq.slice k 56 63) /\
    v b9 == v (Seq.index k 63)
    )
  (ensures S56.wide_as_nat5 (b0, b1, b2, b3, b4, b5, b6, b7, b8, b9) == nat_from_bytes_le k)
  =
  lemma_nat_from_bytes_le_append (Seq.slice k 0 7) (Seq.slice k 7 14);
  lemma_nat_from_bytes_le_append (Seq.slice k 0 14) (Seq.slice k 14 21);
  lemma_nat_from_bytes_le_append (Seq.slice k 0 21) (Seq.slice k 21 28);
  lemma_nat_from_bytes_le_append (Seq.slice k 0 28) (Seq.slice k 28 35);
  lemma_nat_from_bytes_le_append (Seq.slice k 0 35) (Seq.slice k 35 42);
  lemma_nat_from_bytes_le_append (Seq.slice k 0 42) (Seq.slice k 42 49);
  lemma_nat_from_bytes_le_append (Seq.slice k 0 49) (Seq.slice k 49 56);
  lemma_nat_from_bytes_le_append (Seq.slice k 0 56) (Seq.slice k 56 63);
  lemma_nat_from_bytes_le_append (Seq.slice k 0 63) (Seq.create 1 (Seq.index k 63));
  assert (Seq.append (Seq.slice k 0 7) (Seq.slice k 7 14) `Seq.equal` Seq.slice k 0 14);
  assert (Seq.append (Seq.slice k 0 14) (Seq.slice k 14 21) `Seq.equal` Seq.slice k 0 21);
  assert (Seq.append (Seq.slice k 0 21) (Seq.slice k 21 28) `Seq.equal` Seq.slice k 0 28);
  assert (Seq.append (Seq.slice k 0 28) (Seq.slice k 28 35) `Seq.equal` Seq.slice k 0 35);
  assert (Seq.append (Seq.slice k 0 35) (Seq.slice k 35 42) `Seq.equal` Seq.slice k 0 42);
  assert (Seq.append (Seq.slice k 0 42) (Seq.slice k 42 49) `Seq.equal` Seq.slice k 0 49);
  assert (Seq.append (Seq.slice k 0 49) (Seq.slice k 49 56) `Seq.equal` Seq.slice k 0 56);
  assert (Seq.append (Seq.slice k 0 56) (Seq.slice k 56 63) `Seq.equal` Seq.slice k 0 63);
  assert (Seq.append (Seq.slice k 0 63) (Seq.create 1 (Seq.index k 63)) `Seq.equal` k);
  nat_from_intseq_le_lemma0 (Seq.create 1 (Seq.index k 63));
  assert_norm (pow2 56 == 0x100000000000000);
  assert_norm (pow2 112 == 0x10000000000000000000000000000);
  assert_norm (pow2 168 == 0x1000000000000000000000000000000000000000000);
  assert_norm (pow2 224 == 0x100000000000000000000000000000000000000000000000000000000);
  assert_norm (pow2 280 == 0x10000000000000000000000000000000000000000000000000000000000000000000000);
  assert_norm (pow2 336 == 0x1000000000000000000000000000000000000000000000000000000000000000000000000000000000000);
  assert_norm (pow2 392 == 0x100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000);
  assert_norm (pow2 448 == 0x10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000);
  assert_norm (pow2 504 == 0x1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)
val lemma_load_64_bytes (k: lbytes 64) (b0 b1 b2 b3 b4 b5 b6 b7 b8 b9: uint64)
    : Lemma
      (requires
        v b0 == nat_from_bytes_le (Seq.slice k 0 7) /\ v b1 == nat_from_bytes_le (Seq.slice k 7 14) /\
        v b2 == nat_from_bytes_le (Seq.slice k 14 21) /\
        v b3 == nat_from_bytes_le (Seq.slice k 21 28) /\
        v b4 == nat_from_bytes_le (Seq.slice k 28 35) /\
        v b5 == nat_from_bytes_le (Seq.slice k 35 42) /\
        v b6 == nat_from_bytes_le (Seq.slice k 42 49) /\
        v b7 == nat_from_bytes_le (Seq.slice k 49 56) /\
        v b8 == nat_from_bytes_le (Seq.slice k 56 63) /\ v b9 == v (Seq.index k 63))
      (ensures S56.wide_as_nat5 (b0, b1, b2, b3, b4, b5, b6, b7, b8, b9) == nat_from_bytes_le k)
let lemma_load_64_bytes (k: lbytes 64) (b0 b1 b2 b3 b4 b5 b6 b7 b8 b9: uint64)
    : Lemma
      (requires
        v b0 == nat_from_bytes_le (Seq.slice k 0 7) /\ v b1 == nat_from_bytes_le (Seq.slice k 7 14) /\
        v b2 == nat_from_bytes_le (Seq.slice k 14 21) /\
        v b3 == nat_from_bytes_le (Seq.slice k 21 28) /\
        v b4 == nat_from_bytes_le (Seq.slice k 28 35) /\
        v b5 == nat_from_bytes_le (Seq.slice k 35 42) /\
        v b6 == nat_from_bytes_le (Seq.slice k 42 49) /\
        v b7 == nat_from_bytes_le (Seq.slice k 49 56) /\
        v b8 == nat_from_bytes_le (Seq.slice k 56 63) /\ v b9 == v (Seq.index k 63))
      (ensures S56.wide_as_nat5 (b0, b1, b2, b3, b4, b5, b6, b7, b8, b9) == nat_from_bytes_le k) =
lemma_nat_from_bytes_le_append (Seq.slice k 0 7) (Seq.slice k 7 14);
lemma_nat_from_bytes_le_append (Seq.slice k 0 14) (Seq.slice k 14 21);
lemma_nat_from_bytes_le_append (Seq.slice k 0 21) (Seq.slice k 21 28);
lemma_nat_from_bytes_le_append (Seq.slice k 0 28) (Seq.slice k 28 35);
lemma_nat_from_bytes_le_append (Seq.slice k 0 35) (Seq.slice k 35 42);
lemma_nat_from_bytes_le_append (Seq.slice k 0 42) (Seq.slice k 42 49);
lemma_nat_from_bytes_le_append (Seq.slice k 0 49) (Seq.slice k 49 56);
lemma_nat_from_bytes_le_append (Seq.slice k 0 56) (Seq.slice k 56 63);
lemma_nat_from_bytes_le_append (Seq.slice k 0 63) (Seq.create 1 (Seq.index k 63));
assert ((Seq.append (Seq.slice k 0 7) (Seq.slice k 7 14)) `Seq.equal` (Seq.slice k 0 14));
assert ((Seq.append (Seq.slice k 0 14) (Seq.slice k 14 21)) `Seq.equal` (Seq.slice k 0 21));
assert ((Seq.append (Seq.slice k 0 21) (Seq.slice k 21 28)) `Seq.equal` (Seq.slice k 0 28));
assert ((Seq.append (Seq.slice k 0 28) (Seq.slice k 28 35)) `Seq.equal` (Seq.slice k 0 35));
assert ((Seq.append (Seq.slice k 0 35) (Seq.slice k 35 42)) `Seq.equal` (Seq.slice k 0 42));
assert ((Seq.append (Seq.slice k 0 42) (Seq.slice k 42 49)) `Seq.equal` (Seq.slice k 0 49));
assert ((Seq.append (Seq.slice k 0 49) (Seq.slice k 49 56)) `Seq.equal` (Seq.slice k 0 56));
assert ((Seq.append (Seq.slice k 0 56) (Seq.slice k 56 63)) `Seq.equal` (Seq.slice k 0 63));
assert ((Seq.append (Seq.slice k 0 63) (Seq.create 1 (Seq.index k 63))) `Seq.equal` k);
nat_from_intseq_le_lemma0 (Seq.create 1 (Seq.index k 63));
assert_norm (pow2 56 == 0x100000000000000);
assert_norm (pow2 112 == 0x10000000000000000000000000000);
assert_norm (pow2 168 == 0x1000000000000000000000000000000000000000000);
assert_norm (pow2 224 == 0x100000000000000000000000000000000000000000000000000000000);
assert_norm (pow2 280 == 0x10000000000000000000000000000000000000000000000000000000000000000000000);
assert_norm (pow2 336 ==
    0x1000000000000000000000000000000000000000000000000000000000000000000000000000000000000);
assert_norm (pow2 392 ==
    0x100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
  );
assert_norm (pow2 448 ==
    0x10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
  );
assert_norm (pow2 504 ==
    0x1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
  )
Hacl.Impl.Load56.fst.checked
prims.fst.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.BignumQ.Definitions.fst.checked Hacl.Impl.BignumQ.Mul.fsti.checked Hacl.Bignum25519.fsti.checked FStar.UInt32.fsti.checked FStar.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.Calc.fsti.checked
Hacl.Impl.Load56.fst
Lib.ByteSequence.lbytes Lib.IntTypes.uint64 FStar.Pervasives.assert_norm Prims.eq2 Prims.int Prims.pow2 Prims.unit Lib.ByteSequence.nat_from_intseq_le_lemma0 Lib.IntTypes.U8 Lib.IntTypes.SEC FStar.Seq.Base.create Lib.IntTypes.uint_t FStar.Seq.Base.index Prims._assert FStar.Seq.Base.equal FStar.Seq.Base.append FStar.Seq.Base.slice Hacl.Impl.Load56.lemma_nat_from_bytes_le_append Prims.l_and Prims.l_or Lib.IntTypes.range Lib.IntTypes.U64 Prims.b2t Prims.op_GreaterThanOrEqual Prims.op_LessThan FStar.Mul.op_Star Lib.Sequence.length Lib.IntTypes.v Lib.ByteSequence.nat_from_bytes_le Prims.squash Prims.nat Hacl.Spec.BignumQ.Definitions.wide_as_nat5 FStar.Pervasives.Native.Mktuple10 Prims.Nil FStar.Pervasives.pattern
module Hacl.Impl.Load56

module ST = FStar.HyperStack.ST
open FStar.HyperStack.All
open FStar.Mul

open Lib.IntTypes
open Lib.ByteSequence
open Lib.Buffer
open Lib.ByteBuffer

module F56 = Hacl.Impl.BignumQ.Mul
module S56 = Hacl.Spec.BignumQ.Definitions

#reset-options "--z3rlimit 50 --max_fuel 0 --max_ifuel 0"

inline_for_extraction noextract
val hload56_le:
    b:lbuffer uint8 64ul
  -> off:size_t{v off <= 56} ->
  Stack uint64
    (requires fun h -> live h b)
    (ensures fun h0 z h1 -> h0 == h1 /\
      v z < 0x100000000000000 /\
      v z == nat_from_bytes_le (Seq.slice (as_seq h0 b) (v off) (v off + 7))
    )

let hload56_le b off =
  let h0 = ST.get() in
  let b8 = sub b off 8ul in
  let z  = uint_from_bytes_le b8 in
  let z' = z &. u64 0xffffffffffffff in
  assert_norm (0xffffffffffffff == pow2 56 - 1);
  assert_norm (0x100000000000000 == pow2 56 );
  calc (==) {
    v z' <: nat;
    (==) { }
    v (z &. u64 0xffffffffffffff);
    (==) { logand_spec z (u64 0xffffffffffffff) }
    v z `logand_v` 0xffffffffffffff;
    (==) { assert_norm(pow2 56 - 1 == 0xffffffffffffff); UInt.logand_mask (UInt.to_uint_t 64 (v z)) 56 }
    (v z % pow2 56);
    (==) { lemma_reveal_uint_to_bytes_le #U64 #SEC (as_seq h0 b8) }
    nat_from_bytes_le (as_seq h0 b8) % pow2 56;
    (==) { nat_from_intseq_le_slice_lemma (as_seq h0 b8) 7 }
    (nat_from_bytes_le (Seq.slice (as_seq h0 b8) 0 7) +
      pow2 (7 * 8) * nat_from_bytes_le (Seq.slice (as_seq h0 b8) 7 8)) % pow2 56;
    (==) { FStar.Math.Lemmas.lemma_mod_plus_distr_r
      (nat_from_bytes_le (Seq.slice (as_seq h0 b8) 0 7))
      (pow2 (7 * 8) * nat_from_bytes_le (Seq.slice (as_seq h0 b8) 7 8))
      (pow2 56);
      FStar.Math.Lemmas.swap_mul (pow2 (7 * 8)) (nat_from_bytes_le (Seq.slice (as_seq h0 b8) 7 8));
        FStar.Math.Lemmas.cancel_mul_mod (nat_from_bytes_le (Seq.slice (as_seq h0 b8) 7 8)) (pow2 56) }
    nat_from_bytes_le (Seq.slice (as_seq h0 b8) 0 7) <: nat;
  };
  assert (Seq.equal
        (Seq.slice (as_seq h0 b) (v off) (v off + 7))
        (Seq.slice (as_seq h0 b8) 0 7));
  z'


let lemma_nat_from_bytes_le_append (k1 k2:bytes) : Lemma
  (requires Seq.length k1 + Seq.length k2 <= max_size_t)
  (ensures nat_from_bytes_le (Seq.append k1 k2) ==
  nat_from_bytes_le k1 + pow2 (Seq.length k1 * 8) * nat_from_bytes_le k2) =
  let k = Seq.append k1 k2 in
  let n = Seq.length k1 + Seq.length k2 in
  nat_from_intseq_le_slice_lemma #U8 #SEC #n k (Seq.length k1);
  assert (k1 `Seq.equal` Seq.slice k 0 (Seq.length k1));
  assert (k2 `Seq.equal` Seq.slice k (Seq.length k1) n)

#push-options "--z3rlimit 100"

let lemma_load_64_bytes (k:lbytes 64) (b0 b1 b2 b3 b4 b5 b6 b7 b8 b9:uint64) : Lemma
  (requires
    v b0 == nat_from_bytes_le (Seq.slice k 0 7) /\
    v b1 == nat_from_bytes_le (Seq.slice k 7 14) /\
    v b2 == nat_from_bytes_le (Seq.slice k 14 21) /\
    v b3 == nat_from_bytes_le (Seq.slice k 21 28) /\
    v b4 == nat_from_bytes_le (Seq.slice k 28 35) /\
    v b5 == nat_from_bytes_le (Seq.slice k 35 42) /\
    v b6 == nat_from_bytes_le (Seq.slice k 42 49) /\
    v b7 == nat_from_bytes_le (Seq.slice k 49 56) /\
    v b8 == nat_from_bytes_le (Seq.slice k 56 63) /\
    v b9 == v (Seq.index k 63)
    )
  (ensures S56.wide_as_nat5 (b0, b1, b2, b3, b4, b5, b6, b7, b8, b9) == nat_from_bytes_le k)
val lemma_load_64_bytes (k: lbytes 64) (b0 b1 b2 b3 b4 b5 b6 b7 b8 b9: uint64)
    : Lemma
      (requires
        v b0 == nat_from_bytes_le (Seq.slice k 0 7) /\ v b1 == nat_from_bytes_le (Seq.slice k 7 14) /\
        v b2 == nat_from_bytes_le (Seq.slice k 14 21) /\
        v b3 == nat_from_bytes_le (Seq.slice k 21 28) /\
        v b4 == nat_from_bytes_le (Seq.slice k 28 35) /\
        v b5 == nat_from_bytes_le (Seq.slice k 35 42) /\
        v b6 == nat_from_bytes_le (Seq.slice k 42 49) /\
        v b7 == nat_from_bytes_le (Seq.slice k 49 56) /\
        v b8 == nat_from_bytes_le (Seq.slice k 56 63) /\ v b9 == v (Seq.index k 63))
      (ensures S56.wide_as_nat5 (b0, b1, b2, b3, b4, b5, b6, b7, b8, b9) == nat_from_bytes_le k)

    k: Lib.ByteSequence.lbytes 64 ->
    b0: Lib.IntTypes.uint64 ->
    b1: Lib.IntTypes.uint64 ->
    b2: Lib.IntTypes.uint64 ->
    b3: Lib.IntTypes.uint64 ->
    b4: Lib.IntTypes.uint64 ->
    b5: Lib.IntTypes.uint64 ->
    b6: Lib.IntTypes.uint64 ->
    b7: Lib.IntTypes.uint64 ->
    b8: Lib.IntTypes.uint64 ->
    b9: Lib.IntTypes.uint64
  -> FStar.Pervasives.Lemma
      (requires
        Lib.IntTypes.v b0 == Lib.ByteSequence.nat_from_bytes_le (FStar.Seq.Base.slice k 0 7) /\
        Lib.IntTypes.v b1 == Lib.ByteSequence.nat_from_bytes_le (FStar.Seq.Base.slice k 7 14) /\
        Lib.IntTypes.v b2 == Lib.ByteSequence.nat_from_bytes_le (FStar.Seq.Base.slice k 14 21) /\
        Lib.IntTypes.v b3 == Lib.ByteSequence.nat_from_bytes_le (FStar.Seq.Base.slice k 21 28) /\
        Lib.IntTypes.v b4 == Lib.ByteSequence.nat_from_bytes_le (FStar.Seq.Base.slice k 28 35) /\
        Lib.IntTypes.v b5 == Lib.ByteSequence.nat_from_bytes_le (FStar.Seq.Base.slice k 35 42) /\
        Lib.IntTypes.v b6 == Lib.ByteSequence.nat_from_bytes_le (FStar.Seq.Base.slice k 42 49) /\
        Lib.IntTypes.v b7 == Lib.ByteSequence.nat_from_bytes_le (FStar.Seq.Base.slice k 49 56) /\
        Lib.IntTypes.v b8 == Lib.ByteSequence.nat_from_bytes_le (FStar.Seq.Base.slice k 56 63) /\
        Lib.IntTypes.v b9 == Lib.IntTypes.v (FStar.Seq.Base.index k 63))
      (ensures
        Hacl.Spec.BignumQ.Definitions.wide_as_nat5 (b0, b1, b2, b3, b4, b5, b6, b7, b8, b9) ==
        Lib.ByteSequence.nat_from_bytes_le k)