val write_u32 (x: Secret.uint32) (b: B.buffer Secret.uint8)
    : HST.Stack unit
      (requires (fun h -> B.live h b /\ 4 <= B.length b))
      (ensures
        (fun h _ h' ->
            let b' = B.gsub b 0ul 4ul in
            B.modifies (B.loc_buffer b') h h' /\
            (Seq.seq_reveal (B.as_seq h' b'))
            `Seq.equal`
            (LP.serialize (LP.serialize_u32) (U32.uint_to_t (Secret.v x)))))
let write_u32
  (x: Secret.uint32)
  (b: B.buffer Secret.uint8)
: HST.Stack unit
  (requires (fun h ->
    B.live h b /\
    4 <= B.length b
  ))
  (ensures (fun h _ h' ->
    let b' = B.gsub b 0ul 4ul in
    B.modifies (B.loc_buffer b') h h' /\
    Seq.seq_reveal (B.as_seq h' b') `Seq.equal` LP.serialize (LP.serialize_u32) (U32.uint_to_t (Secret.v x))
  ))
= serialize_u32_spec (U32.uint_to_t (Secret.v x));
  E.index_n_to_be 4 (Secret.v x) 0;
  E.index_n_to_be 4 (Secret.v x) 1;
  E.index_n_to_be 4 (Secret.v x) 2;
  E.index_n_to_be 4 (Secret.v x) 3;
  let b' = B.sub b 0ul 4ul in
  B.upd b' 0ul (Secret.to_u8 (x `Secret.shift_right` 24ul));
  B.upd b' 1ul (Secret.to_u8 (x `Secret.shift_right` 16ul));
  B.upd b' 2ul (Secret.to_u8 (x `Secret.shift_right` 8ul));
  B.upd b' 3ul (Secret.to_u8 x)
val write_u32 (x: Secret.uint32) (b: B.buffer Secret.uint8)
    : HST.Stack unit
      (requires (fun h -> B.live h b /\ 4 <= B.length b))
      (ensures
        (fun h _ h' ->
            let b' = B.gsub b 0ul 4ul in
            B.modifies (B.loc_buffer b') h h' /\
            (Seq.seq_reveal (B.as_seq h' b'))
            `Seq.equal`
            (LP.serialize (LP.serialize_u32) (U32.uint_to_t (Secret.v x)))))
let write_u32 (x: Secret.uint32) (b: B.buffer Secret.uint8)
    : HST.Stack unit
      (requires (fun h -> B.live h b /\ 4 <= B.length b))
      (ensures
        (fun h _ h' ->
            let b' = B.gsub b 0ul 4ul in
            B.modifies (B.loc_buffer b') h h' /\
            (Seq.seq_reveal (B.as_seq h' b'))
            `Seq.equal`
            (LP.serialize (LP.serialize_u32) (U32.uint_to_t (Secret.v x))))) =
serialize_u32_spec (U32.uint_to_t (Secret.v x));
E.index_n_to_be 4 (Secret.v x) 0;
E.index_n_to_be 4 (Secret.v x) 1;
E.index_n_to_be 4 (Secret.v x) 2;
E.index_n_to_be 4 (Secret.v x) 3;
let b' = B.sub b 0ul 4ul in
B.upd b' 0ul (Secret.to_u8 (x `Secret.shift_right` 24ul));
B.upd b' 1ul (Secret.to_u8 (x `Secret.shift_right` 16ul));
B.upd b' 2ul (Secret.to_u8 (x `Secret.shift_right` 8ul));
B.upd b' 3ul (Secret.to_u8 x)
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
Lib.IntTypes.uint32 LowStar.Buffer.buffer Lib.IntTypes.uint8 LowStar.Monotonic.Buffer.upd LowStar.Buffer.trivial_preorder FStar.UInt32.__uint_to_t Lib.IntTypes.to_u8 Lib.IntTypes.U32 Lib.IntTypes.SEC Prims.unit Lib.IntTypes.shift_right LowStar.Monotonic.Buffer.mbuffer Lib.IntTypes.int_t Lib.IntTypes.U8 LowStar.Buffer.sub FStar.Ghost.hide FStar.UInt32.t LowParse.Endianness.index_n_to_be QUIC.Secret.Int.Base.v QUIC.Impl.PacketNumber.serialize_u32_spec FStar.UInt32.uint_to_t FStar.Monotonic.HyperStack.mem Prims.l_and LowStar.Monotonic.Buffer.live Prims.b2t Prims.op_LessThanOrEqual LowStar.Monotonic.Buffer.length LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_buffer FStar.Seq.Base.equal Lib.IntTypes.uint_t Lib.IntTypes.PUB QUIC.Secret.Seq.seq_reveal LowStar.Monotonic.Buffer.as_seq LowParse.Spec.Base.serialize LowParse.Spec.Int.parse_u32_kind LowParse.Spec.Int.parse_u32 LowParse.Spec.Int.serialize_u32 LowStar.Buffer.gsub
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
noextract
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)

#pop-options

module U = FStar.UInt

#push-options "--z3rlimit 16"

[@"opaque_to_smt"]
let bound_npn
  (pn_len: packet_number_length_t)
: Tot (x: packet_number_t { Secret.v x == bound_npn' (Secret.v pn_len - 1) })
= let pn_len_1 = Secret.to_u64 (pn_len `Secret.sub` Secret.to_u32 1ul) in
  ((pn_len_1 `Secret.secrets_are_equal_64_2` Secret.to_u64 0ul) `Secret.mul` Secret.to_u64 256uL) `Secret.add`
  ((pn_len_1 `Secret.secrets_are_equal_64_2` Secret.to_u64 1ul) `Secret.mul` Secret.to_u64 65536uL) `Secret.add`
  ((pn_len_1 `Secret.secrets_are_equal_64_2` Secret.to_u64 2ul) `Secret.mul` Secret.to_u64 16777216uL) `Secret.add`
  ((pn_len_1 `Secret.secrets_are_equal_64_2` Secret.to_u64 3ul) `Secret.mul` Secret.to_u64 4294967296uL)

#pop-options

inline_for_extraction
let secret_bounded_integer (i: LP.integer_size) = (x: Secret.uint32 { LP.bounded_integer_prop i (U32.uint_to_t (Secret.v x)) })

#push-options "--max_fuel 2 --initial_fuel 2 --max_ifuel 2 --initial_ifuel 2 --z3rlimit 4096 --query_stats"

module U62 = QUIC.UInt62
module Lemmas = QUIC.Spec.PacketNumber.Lemmas

#restart-solver

[@"opaque_to_smt"]
inline_for_extraction
let expand_pn_aux
  (pn_len: packet_number_length_t)
  (last: last_packet_number_t)
  (npn: secret_bounded_integer (Secret.v pn_len))
: Tot (pn: Secret.uint64 { Secret.v pn == expand_pn' (Secret.v pn_len - 1) (Secret.v last) (Secret.v npn) })
= let open FStar.Mul in
  let open FStar.Math.Lemmas in
  let expected : U62.secret = last `Secret.add` Secret.to_u64 1uL in
  let bound = bound_npn pn_len in
  let bound_2 = bound `Secret.shift_right` 1ul in
  FStar.UInt.shift_right_value_lemma #64 (Secret.v bound) 1;
  assert (Secret.v bound_2 == Secret.v bound / 2);
  let candidate = Lemmas.replace_modulo expected (8 `Prims.op_Multiply` Secret.v pn_len) (bound `Secret.sub` Secret.to_u64 1uL) (Secret.to_u64 npn) in
  Lemmas.lemma_replace_modulo_bound (Secret.v expected) (8*(Secret.v pn_len)) (Secret.v npn) 62;
  let bound_2_le_expected = bound_2 `Secret.secret_is_le_64` expected in
  let cond_1 =
    bound_2_le_expected `Secret.logand_one_bit`
    (candidate `Secret.secret_is_le_64` ((bound_2_le_expected `Secret.mul` expected) `Secret.sub` (bound_2_le_expected `Secret.mul` bound_2))) `Secret.logand_one_bit`
    (candidate `Secret.secret_is_lt_64` (Secret.to_u64 U62.bound `Secret.sub` bound))
  in
  assert (Secret.v cond_1 == (
    if
      Secret.v bound_2 <= Secret.v expected &&
      Secret.v candidate <= (Secret.v expected - Secret.v bound_2) &&
      Secret.v candidate < U62.v U62.bound - Secret.v bound
    then 1
    else 0
  ));
  let cond_2 =
    Secret.lognot_one_bit cond_1 `Secret.logand_one_bit`
    ((expected `Secret.add` bound_2) `Secret.secret_is_lt_64` candidate) `Secret.logand_one_bit`
    (bound `Secret.secret_is_le_64` candidate)
  in
  assert (Secret.v cond_2 == (
    if
      Secret.v cond_1 = 0 &&
      Secret.v expected + Secret.v bound_2 < Secret.v candidate &&
      Secret.v bound <= Secret.v candidate
    then 1
    else 0
  ));
  (candidate `Secret.add` (cond_1 `Secret.mul` bound)) `Secret.sub` (cond_2 `Secret.mul` bound)

#pop-options

#push-options "--z3rlimit 32"

[@"opaque_to_smt"]
let expand_pn
  (pn_len: packet_number_length_t)
  (last: last_packet_number_t)
  (npn: secret_bounded_integer (Secret.v pn_len))
: Tot (pn: packet_number_t { pn == synth_packet_number last pn_len (U32.uint_to_t (Secret.v npn)) })
= expand_pn_aux pn_len last npn

#pop-options

let read_packet_number
  last pn_len b
= let h = HST.get () in
  LP.parse_synth_eq (LP.lift_parser (parse_reduced_pn pn_len)) (synth_packet_number last pn_len) (Seq.seq_reveal (B.as_seq h b));
  let npn = read_bounded_integer pn_len b in
  expand_pn pn_len last npn

#push-options "--z3rlimit 32"

#restart-solver

[@"opaque_to_smt"]
let reduce_pn
  (pn_len: packet_number_length_t)
  (pn: packet_number_t)
: Tot (b: secret_bounded_integer (Secret.v pn_len) { Secret.v b == reduce_pn' (Secret.v pn_len - 1) (Secret.v pn) })
= let mask = bound_npn pn_len `Secret.sub` Secret.to_u64 1uL in
  Secret.logand_spec pn mask;
  Lemmas.logand_mask #64 (Secret.v pn) (8 `Prims.op_Multiply` Secret.v pn_len);
  Secret.to_u32 (pn `Secret.logand` mask)

#pop-options

let serialize_u32_spec
  (x: U32.t)
: Lemma
  (LP.serialize LP.serialize_u32 x == E.n_to_be 4 (U32.v x))
= LP.parse_u32_spec (E.n_to_be 4 (U32.v x));
  LP.parse_injective LP.parse_u32 (LP.serialize LP.serialize_u32 x) (E.n_to_be 4 (U32.v x))

#push-options "--z3rlimit 16"

let write_u32
  (x: Secret.uint32)
  (b: B.buffer Secret.uint8)
: HST.Stack unit
  (requires (fun h ->
    B.live h b /\
    4 <= B.length b
  ))
  (ensures (fun h _ h' ->
    let b' = B.gsub b 0ul 4ul in
    B.modifies (B.loc_buffer b') h h' /\
    Seq.seq_reveal (B.as_seq h' b') `Seq.equal` LP.serialize (LP.serialize_u32) (U32.uint_to_t (Secret.v x))
val write_u32 (x: Secret.uint32) (b: B.buffer Secret.uint8)
    : HST.Stack unit
      (requires (fun h -> B.live h b /\ 4 <= B.length b))
      (ensures
        (fun h _ h' ->
            let b' = B.gsub b 0ul 4ul in
            B.modifies (B.loc_buffer b') h h' /\
            (Seq.seq_reveal (B.as_seq h' b'))
            `Seq.equal`
            (LP.serialize (LP.serialize_u32) (U32.uint_to_t (Secret.v x)))))
x: Lib.IntTypes.uint32 -> b: LowStar.Buffer.buffer Lib.IntTypes.uint8
  -> FStar.HyperStack.ST.Stack Prims.unit