val main: Prims.unit -> St C.exit_code
val main: Prims.unit -> St C.exit_code
let main () : St C.exit_code =
  match test_signatureSchemeListBytes() with
  | None ->
    C.EXIT_SUCCESS

  | Some (Inr (b0, b1)) ->
    print (Printf.sprintf "Failed to round trip: %s <> %s\n"
                           (Bytes.hex_of_bytes b0)
                           (Bytes.hex_of_bytes b1));
    C.EXIT_FAILURE

  | Some (Inl (b, ad, msg)) ->
    print (Printf.sprintf "Failed to round trip: %s, ad=%s, msg=%s\n"
                           (Bytes.hex_of_bytes b)
                           ad
                           msg);
    C.EXIT_FAILURE
module MiTLS.Test.TLSConstants
open MiTLS

open FStar.Error
open FStar.HyperStack.ST

open MiTLS.TLSError
open MiTLS.TLSConstants

#set-options "--admit_smt_queries true"

let test_signatureSchemeListBytes ()
  : Stack (option (either (FStar.Bytes.bytes * string * string)
                          (FStar.Bytes.bytes * FStar.Bytes.bytes)))
          (requires (fun _ -> True))
          (ensures (fun _ _ _ -> True)) =
  let algs = [
   Rsa_pkcs1_md5
  ; Rsa_pkcs1_sha1
  ; Ecdsa_md5
  ; Ecdsa_sha1
  ; Rsa_pkcs1_sha256
  ; Rsa_pkcs1_sha384
  ; Rsa_pkcs1_sha512
  ; Ecdsa_secp256r1_sha256
  ; Ecdsa_secp384r1_sha384
  ; Ecdsa_secp521r1_sha512
  ;Rsa_pss_rsae_sha256
  ; Rsa_pss_rsae_sha384
  ; Rsa_pss_rsae_sha512
  ; Ed25519
  ; Ed448
  ; Rsa_pss_pss_sha256
  ; Rsa_pss_pss_sha384
  ; Rsa_pss_pss_sha512
  ; Unknown_signatureScheme 0xFFFFus
  ] in
  let bytes = signatureSchemeListBytes algs in
  match parseSignatureSchemeList bytes with
  | Correct algs' ->
    let bytes' = signatureSchemeListBytes algs' in
    if bytes = bytes'
    then None //all ok
    else Some (Inr (bytes, bytes')) //failed to round trip
  | Error (ad, msg) ->
    Some (Inl (bytes, string_of_alert ad, msg)) //failed to parse back

let print s = FStar.HyperStack.IO.print_string s
/
prims.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked FStar.UInt16.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.IO.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked C.fst.checked
MiTLS.Test.TLSConstants.fst
_: Prims.unit -> FStar.HyperStack.ST.St C.exit_code
Prims.unit C.EXIT_SUCCESS C.exit_code FStar.Bytes.bytes C.EXIT_FAILURE MiTLS.Test.TLSConstants.print FStar.Printf.sprintf FStar.Bytes.hex_of_bytes Prims.string FStar.Pervasives.Native.option FStar.Pervasives.either FStar.Pervasives.Native.tuple3 FStar.Pervasives.Native.tuple2 MiTLS.Test.TLSConstants.test_signatureSchemeListBytes
let main () : St C.exit_code =
  
match test_signatureSchemeListBytes () with
| None -> C.EXIT_SUCCESS
| Some (Inr (b0, b1)) ->
  print (Printf.sprintf "Failed to round trip: %s <> %s\n"
        (Bytes.hex_of_bytes b0)
        (Bytes.hex_of_bytes b1));
  C.EXIT_FAILURE
| Some (Inl (b, ad, msg)) ->
  print (Printf.sprintf "Failed to round trip: %s, ad=%s, msg=%s\n" (Bytes.hex_of_bytes b) ad msg);
  C.EXIT_FAILURE