val 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 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)
val 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 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))
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.bytes Prims._assert FStar.Seq.Base.equal Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC FStar.Seq.Base.slice FStar.Seq.Base.length Prims.unit Lib.ByteSequence.nat_from_intseq_le_slice_lemma Prims.int Prims.op_Addition FStar.Seq.Base.seq Lib.IntTypes.int_t FStar.Seq.Base.append Prims.b2t Prims.op_LessThanOrEqual Lib.IntTypes.max_size_t Prims.squash Prims.eq2 Lib.ByteSequence.nat_from_bytes_le FStar.Mul.op_Star Prims.pow2 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)
val 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)
k1: Lib.ByteSequence.bytes -> k2: Lib.ByteSequence.bytes
  -> FStar.Pervasives.Lemma
      (requires FStar.Seq.Base.length k1 + FStar.Seq.Base.length k2 <= Lib.IntTypes.max_size_t)
      (ensures
        Lib.ByteSequence.nat_from_bytes_le (FStar.Seq.Base.append k1 k2) ==
        Lib.ByteSequence.nat_from_bytes_le k1 +
        Prims.pow2 (FStar.Seq.Base.length k1 * 8) * Lib.ByteSequence.nat_from_bytes_le k2)