val used_in_not_unused_in_disjoint: Prims.unit
  -> HST.Stack unit
      (requires (fun _ -> True))
      (ensures (fun h _ h' -> h' == h /\ B.loc_disjoint (B.loc_unused_in h) (B.loc_not_unused_in h))
      )
val used_in_not_unused_in_disjoint: Prims.unit
  -> HST.Stack unit
      (requires (fun _ -> True))
      (ensures (fun h _ h' -> h' == h /\ B.loc_disjoint (B.loc_unused_in h) (B.loc_not_unused_in h))
      )
let used_in_not_unused_in_disjoint
  ()
: HST.Stack unit
  (requires (fun _ -> True))
  (ensures (fun h _ h' ->
    h' == h /\
    B.loc_disjoint (B.loc_unused_in h) (B.loc_not_unused_in h)
  ))
= let h = HST.get () in
  B.loc_unused_in_not_unused_in_disjoint h
module QUICTest
module B = LowStar.Buffer
module U62 = QUIC.UInt62
module U32 = FStar.UInt32
module U8 = FStar.UInt8
module HST = FStar.HyperStack.ST
module HS = FStar.HyperStack
module L = FStar.List.Tot
module Secret = QUIC.Secret.Int
module PN = QUIC.Spec.PacketNumber.Base
module Seq = QUIC.Secret.Seq
module Q = QUIC.State
module QS = QUIC.Spec

(* declassification for post tests *)
module ADMITDeclassify = Lib.RawIntTypes

let idx = {
  Q.hash_alg = Spec.Hash.Definitions.SHA2_256;
  Q.aead_alg = Spec.Agile.AEAD.CHACHA20_POLY1305;
}

inline_for_extraction
noextract
let _traffic_secret: list Secret.uint8 = [
  Secret.hide #Secret.U8 0x48uy; Secret.hide #Secret.U8 0xc4uy; Secret.hide #Secret.U8 0x30uy; Secret.hide #Secret.U8 0x9buy; Secret.hide #Secret.U8 0x5fuy; Secret.hide #Secret.U8 0x27uy; Secret.hide #Secret.U8 0x52uy; Secret.hide #Secret.U8 0xe8uy;
  Secret.hide #Secret.U8 0x12uy; Secret.hide #Secret.U8 0x7buy; Secret.hide #Secret.U8 0x1uy;  Secret.hide #Secret.U8 0x66uy; Secret.hide #Secret.U8 0x5uy;  Secret.hide #Secret.U8 0x5auy; Secret.hide #Secret.U8 0x9auy; Secret.hide #Secret.U8 0x56uy;
  Secret.hide #Secret.U8 0xe5uy; Secret.hide #Secret.U8 0xf9uy; Secret.hide #Secret.U8 0x6uy;  Secret.hide #Secret.U8 0x31uy; Secret.hide #Secret.U8 0xe0uy; Secret.hide #Secret.U8 0x84uy; Secret.hide #Secret.U8 0x85uy; Secret.hide #Secret.U8 0xe0uy;
  Secret.hide #Secret.U8 0xf8uy; Secret.hide #Secret.U8 0x9euy; Secret.hide #Secret.U8 0x9cuy; Secret.hide #Secret.U8 0xecuy; Secret.hide #Secret.U8 0x4auy; Secret.hide #Secret.U8 0xdeuy; Secret.hide #Secret.U8 0xb6uy; Secret.hide #Secret.U8 0x50uy;
]

inline_for_extraction
noextract
let traffic_secret_length = norm [delta; zeta; iota; primops] (L.length _traffic_secret)

let traffic_secret_length_correct : squash (traffic_secret_length == L.length _traffic_secret) =
  assert_norm (traffic_secret_length == L.length _traffic_secret)

inline_for_extraction
noextract
let _plain: list Secret.uint8 = [
  Secret.hide #Secret.U8 0uy;Secret.hide #Secret.U8 1uy;Secret.hide #Secret.U8 2uy;Secret.hide #Secret.U8 3uy;Secret.hide #Secret.U8 4uy;Secret.hide #Secret.U8 5uy;Secret.hide #Secret.U8 6uy;Secret.hide #Secret.U8 7uy;Secret.hide #Secret.U8 8uy;Secret.hide #Secret.U8 9uy;
]

inline_for_extraction
noextract
let plain_length = norm [delta; zeta; iota; primops] (L.length _plain)

let plain_length_correct : squash (plain_length == L.length _plain) =
  assert_norm (plain_length == L.length _plain)

module E = EverCrypt.Error
module PF = LowStar.Printf

let is_success_body (e: E.error_code) : HST.Stack bool
  (requires (fun _ -> True))
  (ensures (fun h r h' -> h == h' /\ r == (E.Success? e)))
= match e with
  | E.UnsupportedAlgorithm ->
    PF.print_string "unsupported algorithm\n";
    false
  | E.InvalidKey ->
    PF.print_string "invalid key\n";
    false
  | E.AuthenticationFailure ->
    PF.print_string "auth failure\n";
    false
  | E.InvalidIVLength ->
    PF.print_string "invalid IV length\n";
    false
  | E.DecodeError ->
    PF.print_string "decode error\n";
    false
  | E.Success ->
    PF.print_string "success\n";
    true
  | _ ->
    PF.print_string "unknown error\n";
    false

inline_for_extraction
noextract
let is_success (s: string) (e: E.error_code) : HST.Stack bool
  (requires (fun _ -> True))
  (ensures (fun h r h' -> h == h' /\ r == (E.Success? e)))
= PF.print_string "Performing ";
  PF.print_string s;
  PF.print_string ": ";
  is_success_body e

let check_is_true_body
  (e: bool)
: HST.Stack bool
  (requires (fun _ -> True))
  (ensures (fun h r h' -> h == h' /\ r == e))
= if e then PF.print_string "OK\n" else PF.print_string "KO\n";
  e

inline_for_extraction
noextract
let check_is_true
  (s: string)
  (e: bool)
: HST.Stack bool
  (requires (fun _ -> True))
  (ensures (fun h r h' -> h == h' /\ r == e))
= PF.print_string "Checking ";
  PF.print_string s;
  PF.print_string ": ";
  check_is_true_body e

assume (* implemented in main.c *)
val is_equal
  (b1: B.buffer U8.t)
  (b2: B.buffer Secret.uint8)
  (len: U32.t)
: HST.Stack bool
  (requires (fun h ->
    B.live h b1 /\
    B.live h b2 /\
    U32.v len <= B.length b1 /\
    U32.v len <= B.length b2
  ))
  (ensures (fun h res h' ->
    h' == h /\
    (res == true <==> Seq.slice (Seq.seq_hide #Secret.U8 (B.as_seq h b1)) 0 (U32.v len) == Seq.slice (B.as_seq h b2) 0 (U32.v len))
  ))

inline_for_extraction
/
Spec.Hash.Definitions.fst.checked Spec.Agile.AEAD.fsti.checked QUIC.UInt62.fst.checked QUIC.State.fsti.checked QUIC.Spec.PacketNumber.Base.fst.checked QUIC.Spec.fsti.checked QUIC.Secret.Seq.fsti.checked QUIC.Secret.Int.fsti.checked prims.fst.checked LowStar.Printf.fst.checked LowStar.Buffer.fst.checked Lib.RawIntTypes.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked EverCrypt.Error.fsti.checked C.fst.checked
QUICTest.fst
_: Prims.unit -> FStar.HyperStack.ST.Stack Prims.unit
Prims.unit LowStar.Monotonic.Buffer.loc_unused_in_not_unused_in_disjoint FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Prims.l_True Prims.l_and Prims.eq2 LowStar.Monotonic.Buffer.loc_disjoint LowStar.Monotonic.Buffer.loc_unused_in LowStar.Monotonic.Buffer.loc_not_unused_in
let used_in_not_unused_in_disjoint ()
    : HST.Stack unit
      (requires (fun _ -> True))
      (ensures (fun h _ h' -> h' == h /\ B.loc_disjoint (B.loc_unused_in h) (B.loc_not_unused_in h))
      ) =
  
let h = HST.get () in
B.loc_unused_in_not_unused_in_disjoint h