val check_is_true (s: string) (e: bool)
    : HST.Stack bool (requires (fun _ -> True)) (ensures (fun h r h' -> h == h' /\ r == e))
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
val check_is_true (s: string) (e: bool)
    : HST.Stack bool (requires (fun _ -> True)) (ensures (fun h r h' -> h == h' /\ r == e))
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
QUICTest.fst.checked
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.string Prims.bool QUICTest.check_is_true_body Prims.unit LowStar.Printf.print_string FStar.Monotonic.HyperStack.mem Prims.l_True Prims.l_and Prims.eq2
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))
val check_is_true (s: string) (e: bool)
    : HST.Stack bool (requires (fun _ -> True)) (ensures (fun h r h' -> h == h' /\ r == e))
s: Prims.string -> e: Prims.bool -> FStar.HyperStack.ST.Stack Prims.bool