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'
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'
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.Buffer.lbuffer Lib.IntTypes.uint8 FStar.UInt32.__uint_to_t Lib.IntTypes.size_t Prims.b2t Prims.op_LessThanOrEqual Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Prims.unit Prims._assert FStar.Seq.Base.equal FStar.Seq.Base.slice Lib.Buffer.as_seq Lib.Buffer.MUT Prims.op_Addition FStar.Calc.calc_finish Prims.nat Prims.eq2 Lib.IntTypes.U64 Lib.IntTypes.SEC Lib.ByteSequence.nat_from_bytes_le Prims.Cons FStar.Preorder.relation Prims.Nil FStar.Calc.calc_step Prims.op_Modulus FStar.Mul.op_Star Prims.pow2 Lib.IntTypes.logand_v Lib.IntTypes.op_Amp_Dot Lib.IntTypes.u64 FStar.Calc.calc_init FStar.Calc.calc_pack Prims.squash Lib.IntTypes.logand_spec FStar.UInt.logand_mask FStar.UInt.to_uint_t FStar.Pervasives.assert_norm Prims.int Prims.op_Subtraction Lib.ByteSequence.lemma_reveal_uint_to_bytes_le Lib.ByteSequence.nat_from_intseq_le_slice_lemma Lib.IntTypes.U8 FStar.Math.Lemmas.cancel_mul_mod FStar.Math.Lemmas.swap_mul FStar.Math.Lemmas.lemma_mod_plus_distr_r Lib.IntTypes.int_t Lib.IntTypes.uint64 Lib.ByteBuffer.uint_from_bytes_le Lib.IntTypes.uint_t Lib.Buffer.lbuffer_t FStar.UInt32.uint_to_t FStar.UInt32.t Lib.Buffer.sub FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get
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))
    )
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))
    )
b: Lib.Buffer.lbuffer Lib.IntTypes.uint8 64ul -> off: Lib.IntTypes.size_t{Lib.IntTypes.v off <= 56}
  -> FStar.HyperStack.ST.Stack Lib.IntTypes.uint64