val be_to_n_4_eq (b: Seq.lseq U8.t 4)
    : Lemma
    (E.be_to_n b ==
      U8.v (Seq.index b 3) +
      (256
        `Prims.op_Multiply`
        (U8.v (Seq.index b 2) +
          (256
            `Prims.op_Multiply`
            (U8.v (Seq.index b 1) + (256 `Prims.op_Multiply` (U8.v (Seq.index b 0))))))))
val be_to_n_4_eq (b: Seq.lseq U8.t 4)
    : Lemma
    (E.be_to_n b ==
      U8.v (Seq.index b 3) +
      (256
        `Prims.op_Multiply`
        (U8.v (Seq.index b 2) +
          (256
            `Prims.op_Multiply`
            (U8.v (Seq.index b 1) + (256 `Prims.op_Multiply` (U8.v (Seq.index b 0))))))))
let be_to_n_4_eq
  (b: Seq.lseq U8.t 4)
: Lemma
  (E.be_to_n b ==
    U8.v (Seq.index b 3) + (256 `Prims.op_Multiply` (
    U8.v (Seq.index b 2) + (256 `Prims.op_Multiply` (
    U8.v (Seq.index b 1) + (256 `Prims.op_Multiply` (
    U8.v (Seq.index b 0)
  )))))))
= assert_norm (pow2 8 == 256);
  E.reveal_be_to_n b;
  let b3 = Seq.slice b 0 3 in
  E.reveal_be_to_n b3;
  let b2 = Seq.slice b3 0 2 in
  E.reveal_be_to_n b2;
  let b1 = Seq.slice b2 0 1 in
  E.reveal_be_to_n b1;
  E.reveal_be_to_n (Seq.slice b1 0 0)
module QUIC.Impl.PacketNumber
open QUIC.Spec.PacketNumber

module U64 = FStar.UInt64
module U32 = FStar.UInt32
module HST = FStar.HyperStack.ST
module B = LowStar.Buffer
module HS = FStar.HyperStack
module Secret = QUIC.Secret.Int
module SecretBuffer = QUIC.Secret.Buffer
module LP = LowParse.Spec
module Seq = QUIC.Secret.Seq

friend QUIC.Spec.PacketNumber
module Spec = QUIC.Spec.PacketNumber

module Cast = FStar.Int.Cast
module U32 = FStar.UInt32
module U16 = FStar.UInt16
module U8 = FStar.UInt8

module E = LowParse.Endianness.BitFields
/
QUIC.UInt62.fst.checked QUIC.Spec.PacketNumber.Lemmas.fst.checked QUIC.Spec.PacketNumber.fst.checked QUIC.Spec.PacketNumber.fst.checked QUIC.Secret.Seq.fsti.checked QUIC.Secret.Int.fsti.checked QUIC.Secret.Buffer.fsti.checked prims.fst.checked LowStar.Buffer.fst.checked LowParse.Spec.fst.checked LowParse.Endianness.BitFields.fst.checked LowParse.BitFields.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.UInt.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Classical.fsti.checked
QUIC.Impl.PacketNumber.fst
b: FStar.Seq.Properties.lseq FStar.UInt8.t 4
  -> FStar.Pervasives.Lemma
    (ensures
      FStar.Endianness.be_to_n b ==
      FStar.UInt8.v (FStar.Seq.Base.index b 3) +
      256 *
      (FStar.UInt8.v (FStar.Seq.Base.index b 2) +
        256 *
        (FStar.UInt8.v (FStar.Seq.Base.index b 1) + 256 * FStar.UInt8.v (FStar.Seq.Base.index b 0)))
    )
FStar.Seq.Properties.lseq FStar.UInt8.t FStar.Endianness.reveal_be_to_n FStar.Seq.Base.slice Prims.unit FStar.Seq.Base.seq FStar.Pervasives.assert_norm Prims.eq2 Prims.int Prims.pow2 Prims.l_True Prims.squash FStar.Endianness.be_to_n Prims.op_Addition FStar.UInt8.v FStar.Seq.Base.index Prims.op_Multiply Prims.Nil FStar.Pervasives.pattern
let be_to_n_4_eq (b: Seq.lseq U8.t 4)
    : Lemma
    (E.be_to_n b ==
      U8.v (Seq.index b 3) +
      (256
        `Prims.op_Multiply`
        (U8.v (Seq.index b 2) +
          (256
            `Prims.op_Multiply`
            (U8.v (Seq.index b 1) + (256 `Prims.op_Multiply` (U8.v (Seq.index b 0)))))))) =
  
assert_norm (pow2 8 == 256);
E.reveal_be_to_n b;
let b3 = Seq.slice b 0 3 in
E.reveal_be_to_n b3;
let b2 = Seq.slice b3 0 2 in
E.reveal_be_to_n b2;
let b1 = Seq.slice b2 0 1 in
E.reveal_be_to_n b1;
E.reveal_be_to_n (Seq.slice b1 0 0)