val print_bytes (k: bytes) : ML unit
val print_bytes (k: bytes) : ML unit
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)
(* 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"
/
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
k: Lib.ByteSequence.bytes -> FStar.All.ML Prims.unit
Lib.ByteSequence.bytes FStar.List.iter Lib.IntTypes.uint8 FStar.IO.print_uint8_hex_pad Lib.RawIntTypes.u8_to_UInt8 Prims.unit Lib.Sequence.to_list Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC
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)