val print_opt_keypair (#nc: config) (okp: option (keypair nc)) : ML unit
val print_opt_keypair (#nc: config) (okp: option (keypair nc)) : ML unit
let print_opt_keypair (#nc : config) (okp : option (keypair nc)) : ML unit =
  match okp with
  | None -> IO.print_string "None"
  | Some kp -> print_keypair kp
(* TODO: I would like to change the name of the module (remove the 'Spec')
 * but then we need to create a special build rule in the Makefile, because
 * otherwise no .ml file is generated (and thus the tests can't be run). *)
module Spec.Noise.Utils

open Spec.Noise

open FStar.All
module IO = FStar.IO
module List = FStar.List

open Lib.IntTypes
open Lib.RawIntTypes
open Lib.Sequence
open Lib.ByteSequence

(* Utility functions for formatting *)
let print_separation () : ML unit = IO.print_string "==================\n\n"

(* Utility functions to print and compare *)
let print_bytes (k : bytes) : ML unit =
  List.iter (fun a -> IO.print_uint8_hex_pad (Lib.RawIntTypes.u8_to_UInt8 a)) (to_list k)

let print_named_bytes (s : string) (k : bytes) : ML unit =
  IO.print_string s;
  IO.print_string ": ";
  print_bytes k;
  IO.print_string "\n"

let print_opt_bytes (#n : size_nat) (ob : option (lbytes n)) : ML unit =
  match ob with
  | None -> IO.print_string "None"
  | Some b -> print_bytes b

let compare_bytes (#n : size_nat) (b1 b2 : lbytes n) : bool =
  lbytes_eq b1 b2

let compare_opt_bytes (#n : size_nat) (ob1 ob2 : option (lbytes n)) : bool =
  match ob1, ob2 with
  | None, None -> true
  | Some b1, Some b2 -> compare_bytes b1 b2
  | _ -> false

let print_compare_bytes (#n : size_nat) (result expected : lbytes n) : ML bool =
  let is_same  = compare_bytes result expected in
  IO.print_string "Result  : ";
  print_bytes result;
  IO.print_string "\nExpected: ";
  print_bytes expected;
  if is_same then IO.print_string "\nSucces: same values\n\n"
             else IO.print_string "\n[!] Failure: different values\n\n";
  is_same

let print_compare_opt_bytes (#n : size_nat) (result expected : option (lbytes n)) : ML bool =
  let is_same  = compare_opt_bytes result expected in
  IO.print_string "Result  : ";
  print_opt_bytes result;
  IO.print_string "\nExpected: ";
  print_opt_bytes expected;
  if is_same then IO.print_string "\nSucces: same values\n\n"
             else IO.print_string "\n[!] Failure: different values\n\n";
  is_same

let print_compare_named_bytes (#n : size_nat) (s : string) (result expected : lbytes n) : ML bool =
  let is_same  = compare_bytes result expected in
  IO.print_string s;
  IO.print_string "\n";
  print_compare_bytes result expected

let print_compare_named_opt_bytes (#n : size_nat) (s : string)
  (result expected : option (lbytes n)) : ML bool =
  let is_same  = compare_opt_bytes result expected in
  IO.print_string s;
  IO.print_string "\n";
  print_compare_opt_bytes result expected

let print_keypair (#nc : config) (kp : keypair nc) : ML unit =
  print_named_bytes "-pub " kp.pub;
  print_named_bytes "-priv" kp.priv;
  IO.print_string "\n"
/
Spec.Noise.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.UInt64.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.fst.checked FStar.IO.fst.checked FStar.All.fst.checked
Spec.Noise.Utils.fst
okp: FStar.Pervasives.Native.option (Spec.Noise.CryptoPrimitives.keypair nc)
  -> FStar.All.ML Prims.unit
Spec.Noise.CryptoPrimitives.config FStar.Pervasives.Native.option Spec.Noise.CryptoPrimitives.keypair FStar.IO.print_string Prims.unit Spec.Noise.Utils.print_keypair
let print_opt_keypair (#nc: config) (okp: option (keypair nc)) : ML unit =
  
match okp with
| None -> IO.print_string "None"
| Some kp -> print_keypair kp