val read_u32 (b: B.buffer Secret.uint8)
    : HST.Stack Secret.uint32
      (requires (fun h -> B.live h b /\ 4 <= B.length b))
      (ensures
        (fun h res h' ->
            B.modifies B.loc_none h h' /\
            (match LP.parse LP.parse_u32 (Seq.seq_reveal (B.as_seq h b)) with
              | Some (v, _) -> Secret.v res == U32.v v
              | None -> False)))
let read_u32
  (b: B.buffer Secret.uint8)
: HST.Stack Secret.uint32
  (requires (fun h ->
    B.live h b /\
    4 <= B.length b
  ))
  (ensures (fun h res h' ->
    B.modifies B.loc_none h h' /\
    begin match LP.parse LP.parse_u32 (Seq.seq_reveal (B.as_seq h b)) with
    | Some (v, _) -> Secret.v res == U32.v v
    | None -> False
    end
  ))
= 
  let h = HST.get () in
  LP.parse_u32_spec (Seq.seq_reveal (B.as_seq h b));
  be_to_n_4_eq (Seq.slice (Seq.seq_reveal (B.as_seq h b)) 0 4);
  let b3 = B.index b 3ul in
  let b2 = B.index b 2ul in
  let b1 = B.index b 1ul in
  let b0 = B.index b 0ul in
  Secret.to_u32 b3 `Secret.add` (Secret.to_u32 256ul `Secret.mul` (
  Secret.to_u32 b2 `Secret.add` (Secret.to_u32 256ul `Secret.mul` (  
  Secret.to_u32 b1 `Secret.add` (Secret.to_u32 256ul `Secret.mul` (  
  Secret.to_u32 b0
  ))))))
val read_u32 (b: B.buffer Secret.uint8)
    : HST.Stack Secret.uint32
      (requires (fun h -> B.live h b /\ 4 <= B.length b))
      (ensures
        (fun h res h' ->
            B.modifies B.loc_none h h' /\
            (match LP.parse LP.parse_u32 (Seq.seq_reveal (B.as_seq h b)) with
              | Some (v, _) -> Secret.v res == U32.v v
              | None -> False)))
let read_u32 (b: B.buffer Secret.uint8)
    : HST.Stack Secret.uint32
      (requires (fun h -> B.live h b /\ 4 <= B.length b))
      (ensures
        (fun h res h' ->
            B.modifies B.loc_none h h' /\
            (match LP.parse LP.parse_u32 (Seq.seq_reveal (B.as_seq h b)) with
              | Some (v, _) -> Secret.v res == U32.v v
              | None -> False))) =
let h = HST.get () in
LP.parse_u32_spec (Seq.seq_reveal (B.as_seq h b));
be_to_n_4_eq (Seq.slice (Seq.seq_reveal (B.as_seq h b)) 0 4);
let b3 = B.index b 3ul in
let b2 = B.index b 2ul in
let b1 = B.index b 1ul in
let b0 = B.index b 0ul in
(Secret.to_u32 b3)
`Secret.add`
((Secret.to_u32 256ul)
  `Secret.mul`
  ((Secret.to_u32 b2)
    `Secret.add`
    ((Secret.to_u32 256ul)
      `Secret.mul`
      ((Secret.to_u32 b1) `Secret.add` ((Secret.to_u32 256ul) `Secret.mul` (Secret.to_u32 b0))))))
QUIC.Impl.PacketNumber.fst.checked
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
LowStar.Buffer.buffer Lib.IntTypes.uint8 Lib.IntTypes.add Lib.IntTypes.U32 Lib.IntTypes.SEC Lib.IntTypes.to_u32 Lib.IntTypes.U8 Lib.IntTypes.mul Lib.IntTypes.PUB FStar.UInt32.__uint_to_t Lib.IntTypes.uint32 Lib.IntTypes.int_t LowStar.Monotonic.Buffer.index LowStar.Buffer.trivial_preorder Prims.unit QUIC.Impl.PacketNumber.be_to_n_4_eq FStar.Seq.Base.slice Lib.IntTypes.uint_t QUIC.Secret.Seq.seq_reveal LowStar.Monotonic.Buffer.as_seq LowParse.Spec.Int.parse_u32_spec FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Prims.l_and LowStar.Monotonic.Buffer.live Prims.b2t Prims.op_LessThanOrEqual LowStar.Monotonic.Buffer.length LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_none LowParse.Spec.Base.parse FStar.UInt32.t LowParse.Spec.Int.parse_u32 LowParse.Spec.Base.consumed_length Prims.eq2 Prims.int Prims.l_or Lib.IntTypes.range FStar.UInt.size FStar.UInt32.n QUIC.Secret.Int.Base.v FStar.UInt32.v Prims.l_False Prims.logical
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

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)

#push-options "--z3rlimit 64"

let read_u32
  (b: B.buffer Secret.uint8)
: HST.Stack Secret.uint32
  (requires (fun h ->
    B.live h b /\
    4 <= B.length b
  ))
  (ensures (fun h res h' ->
    B.modifies B.loc_none h h' /\
    begin match LP.parse LP.parse_u32 (Seq.seq_reveal (B.as_seq h b)) with
    | Some (v, _) -> Secret.v res == U32.v v
    | None -> False
    end
val read_u32 (b: B.buffer Secret.uint8)
    : HST.Stack Secret.uint32
      (requires (fun h -> B.live h b /\ 4 <= B.length b))
      (ensures
        (fun h res h' ->
            B.modifies B.loc_none h h' /\
            (match LP.parse LP.parse_u32 (Seq.seq_reveal (B.as_seq h b)) with
              | Some (v, _) -> Secret.v res == U32.v v
              | None -> False)))
b: LowStar.Buffer.buffer Lib.IntTypes.uint8 -> FStar.HyperStack.ST.Stack Lib.IntTypes.uint32