val read_bounded_integer (pn_len: packet_number_length_t) (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_bounded_integer (Secret.v pn_len))
                  (Seq.seq_reveal (B.as_seq h b))
              with
              | Some (v, _) -> Secret.v res == U32.v v
              | None -> False)))
val read_bounded_integer (pn_len: packet_number_length_t) (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_bounded_integer (Secret.v pn_len))
                  (Seq.seq_reveal (B.as_seq h b))
              with
              | Some (v, _) -> Secret.v res == U32.v v
              | None -> False)))
let read_bounded_integer
  (pn_len: packet_number_length_t)
  (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_bounded_integer (Secret.v pn_len)) (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_bounded_integer_spec (Secret.v pn_len) (Seq.seq_reveal (B.as_seq h b));
  LP.parse_u32_spec (Seq.seq_reveal (B.as_seq h b));
  E.bitfield_be_to_n_slice (Seq.slice (Seq.seq_reveal (B.as_seq h b)) 0 4) 0 (Secret.v pn_len);
  let x = read_u32 b in
  BF.get_bitfield_full #32 (Secret.v x);
  let pn_len_1 = Secret.to_u32 (pn_len `Secret.sub` Secret.to_u32 1ul) in
  ((pn_len_1 `Secret.secrets_are_equal_32_2` Secret.to_u32 0ul) `Secret.mul` Secret.get_bitfield x 24ul 32ul) `Secret.add`
  ((pn_len_1 `Secret.secrets_are_equal_32_2` Secret.to_u32 1ul) `Secret.mul` Secret.get_bitfield x 16ul 32ul) `Secret.add`
  ((pn_len_1 `Secret.secrets_are_equal_32_2` Secret.to_u32 2ul) `Secret.mul`
Secret.get_bitfield x 8ul 32ul) `Secret.add`
  ((pn_len_1 `Secret.secrets_are_equal_32_2` Secret.to_u32 3ul) `Secret.mul` x)
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
  ))
= 
  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
  ))))))

#pop-options

module BF = LowParse.BitFields

#push-options "--z3rlimit 16"

inline_for_extraction
/
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

    pn_len: QUIC.Spec.PacketNumber.Base.packet_number_length_t ->
    b: LowStar.Buffer.buffer Lib.IntTypes.uint8
  -> FStar.HyperStack.ST.Stack Lib.IntTypes.uint32
QUIC.Spec.PacketNumber.Base.packet_number_length_t LowStar.Buffer.buffer Lib.IntTypes.uint8 Lib.IntTypes.add Lib.IntTypes.U32 Lib.IntTypes.SEC Lib.IntTypes.mul QUIC.Secret.Int.secrets_are_equal_32_2 Lib.IntTypes.to_u32 Lib.IntTypes.PUB FStar.UInt32.__uint_to_t QUIC.Secret.Int.get_bitfield Lib.IntTypes.int_t Lib.IntTypes.sub Prims.unit LowParse.BitFields.get_bitfield_full QUIC.Secret.Int.Base.v Lib.IntTypes.uint32 QUIC.Impl.PacketNumber.read_u32 LowParse.Endianness.BitFields.bitfield_be_to_n_slice FStar.Seq.Base.slice Lib.IntTypes.uint_t Lib.IntTypes.U8 QUIC.Secret.Seq.seq_reveal LowStar.Monotonic.Buffer.as_seq LowStar.Buffer.trivial_preorder LowParse.Spec.Int.parse_u32_spec LowParse.Spec.BoundedInt.parse_bounded_integer_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 LowParse.Spec.BoundedInt.bounded_integer LowParse.Spec.BoundedInt.parse_bounded_integer LowParse.Spec.Base.consumed_length Prims.eq2 Prims.int Prims.l_or Lib.IntTypes.range FStar.UInt.size FStar.UInt32.n FStar.UInt32.v Prims.l_False Prims.logical
let read_bounded_integer (pn_len: packet_number_length_t) (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_bounded_integer (Secret.v pn_len))
                  (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_bounded_integer_spec (Secret.v pn_len) (Seq.seq_reveal (B.as_seq h b));
LP.parse_u32_spec (Seq.seq_reveal (B.as_seq h b));
E.bitfield_be_to_n_slice (Seq.slice (Seq.seq_reveal (B.as_seq h b)) 0 4) 0 (Secret.v pn_len);
let x = read_u32 b in
BF.get_bitfield_full #32 (Secret.v x);
let pn_len_1 = Secret.to_u32 (pn_len `Secret.sub` (Secret.to_u32 1ul)) in
((((pn_len_1 `Secret.secrets_are_equal_32_2` (Secret.to_u32 0ul))
      `Secret.mul`
      (Secret.get_bitfield x 24ul 32ul))
    `Secret.add`
    ((pn_len_1 `Secret.secrets_are_equal_32_2` (Secret.to_u32 1ul))
      `Secret.mul`
      (Secret.get_bitfield x 16ul 32ul)))
  `Secret.add`
  ((pn_len_1 `Secret.secrets_are_equal_32_2` (Secret.to_u32 2ul))
    `Secret.mul`
    (Secret.get_bitfield x 8ul 32ul)))
`Secret.add`
((pn_len_1 `Secret.secrets_are_equal_32_2` (Secret.to_u32 3ul)) `Secret.mul` x)