val print_compare_display_diff: display:bool -> len:size_nat -> expected:lbytes len -> result:lbytes len -> FStar.All.ML bool
let print_compare_display_diff flag len expected result =
  let r = for_all2 (fun a b -> uint_to_nat #U8 a = uint_to_nat #U8 b) expected result in
  if not flag then r
  else (
    let diff = map2 (fun a b -> a ^. b) expected result in
    if r then IO.print_string "\nSuccess !"
    else begin
      IO.print_string "\nFailure !";
      IO.print_newline ();
      IO.print_string "\nDiff: ";
      List.iter (fun a -> print_uint8_hex_pad a) (to_list diff);
      IO.print_newline ();
      IO.print_string "\nResult:   ";
      List.iter (fun a -> print_uint8_hex_pad a) (to_list result);
      IO.print_newline ();
      IO.print_string "\nExpected: ";
      List.iter (fun a -> print_uint8_hex_pad a) (to_list expected);
      IO.print_newline ()
    end;
    r)
val print_compare_display_diff: display:bool -> len:size_nat -> expected:lbytes len -> result:lbytes len -> FStar.All.ML bool
let print_compare_display_diff flag len expected result =
let r = for_all2 (fun a b -> uint_to_nat #U8 a = uint_to_nat #U8 b) expected result in
if not flag
then r
else
  (let diff = map2 (fun a b -> a ^. b) expected result in
    if r
    then IO.print_string "\nSuccess !"
    else
      (IO.print_string "\nFailure !";
        IO.print_newline ();
        IO.print_string "\nDiff: ";
        List.iter (fun a -> print_uint8_hex_pad a) (to_list diff);
        IO.print_newline ();
        IO.print_string "\nResult:   ";
        List.iter (fun a -> print_uint8_hex_pad a) (to_list result);
        IO.print_newline ();
        IO.print_string "\nExpected: ";
        List.iter (fun a -> print_uint8_hex_pad a) (to_list expected);
        IO.print_newline ());
    r)
Lib.PrintSequence.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.IO.fst.checked
Lib.PrintSequence.fst
Prims.bool Lib.IntTypes.size_nat Lib.ByteSequence.lbytes Prims.op_Negation Prims.unit FStar.IO.print_string FStar.IO.print_newline FStar.List.iter Lib.IntTypes.uint8 Lib.PrintSequence.print_uint8_hex_pad Lib.Sequence.to_list Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.IntTypes.int_t Lib.Sequence.lseq Prims.l_Forall Prims.nat Prims.l_imp Prims.b2t Prims.op_LessThan Prims.eq2 Lib.Sequence.index Lib.IntTypes.logxor Lib.Sequence.map2 Lib.IntTypes.op_Hat_Dot Lib.Sequence.for_all2 Prims.op_Equality Prims.l_or Prims.int Prims.op_GreaterThanOrEqual Lib.IntTypes.range Lib.IntTypes.uint_v Lib.RawIntTypes.uint_to_nat
module Lib.PrintSequence

open FStar.Mul
open Lib.IntTypes
open Lib.RawIntTypes
open Lib.Sequence
open Lib.ByteSequence
open Lib.LoopCombinators



let print_nat8_hex x =
  IO.print_uint8 (u8_to_UInt8 (u8 x))

let print_nat8_hex_pad x =
  IO.print_uint8_hex_pad (u8_to_UInt8 (u8 x))

let print_nat8_dec x =
  IO.print_uint8_dec (u8_to_UInt8 (u8 x))

let print_nat8_dec_pad x =
  IO.print_uint8_dec_pad (u8_to_UInt8 (u8 x))


let print_nat32_hex x =
  IO.print_uint32 (u32_to_UInt32 (u32 x))

let print_nat32_hex_pad x =
  IO.print_uint32_hex_pad (u32_to_UInt32 (u32 x))

let print_nat32_dec x =
  IO.print_uint32_dec (u32_to_UInt32 (u32 x))

let print_nat32_dec_pad x =
  IO.print_uint32_dec_pad (u32_to_UInt32 (u32 x))


let print_nat64_hex x =
  IO.print_uint64 (u64_to_UInt64 (u64 x))

let print_nat64_hex_pad x =
  IO.print_uint64_hex_pad (u64_to_UInt64 (u64 x))

let print_nat64_dec x =
  IO.print_uint64_dec (u64_to_UInt64 (u64 x))

let print_nat64_dec_pad x =
  IO.print_uint64_dec_pad (u64_to_UInt64 (u64 x))


let print_uint8_hex x =
  IO.print_uint8 (u8_to_UInt8 x)

let print_uint8_hex_pad x =
  IO.print_uint8_hex_pad (u8_to_UInt8 x)

let print_uint8_dec x =
  IO.print_uint8_dec (u8_to_UInt8 x)

let print_uint8_dec_pad x =
  IO.print_uint8_dec_pad (u8_to_UInt8 x)


let print_uint32_hex x =
  IO.print_uint32 (u32_to_UInt32 x)

let print_uint32_hex_pad x =
  IO.print_uint32_hex_pad (u32_to_UInt32 x)

let print_uint32_dec x =
  IO.print_uint32_dec (u32_to_UInt32 x)

let print_uint32_dec_pad x =
  IO.print_uint32_dec_pad (u32_to_UInt32 x)


let print_uint64_hex x =
  IO.print_uint64 (u64_to_UInt64 x)

let print_uint64_hex_pad x =
  IO.print_uint64_hex_pad (u64_to_UInt64 x)

let print_uint64_dec x =
  IO.print_uint64_dec (u64_to_UInt64 x)

let print_uint64_dec_pad x =
  IO.print_uint64_dec_pad (u64_to_UInt64 x)


let print_label_nat64 flag s x =
  if not flag then () else (
  IO.print_string s;
  IO.print_string ": ";
  print_nat64_dec x;
  IO.print_string "\n")

let print_label_uint8 flag s x =
  if not flag then () else (
  IO.print_string s;
  IO.print_string ": ";
  print_uint8_hex_pad x;
  IO.print_string "\n")

let print_label_uint32 flag s x =
  if not flag then () else (
  IO.print_string s;
  IO.print_string ": ";
  print_uint32_hex_pad x;
  IO.print_string "\n")

let print_label_uint64 flag s x =
  if not flag then () else (
  IO.print_string s;
  IO.print_string ": ";
  print_uint64_hex_pad x;
  IO.print_string "\n")


let print_list_nat64 flag l =
  if not flag then ()
  else (
  repeat_range_all_ml 0 (List.Tot.length l) (fun i _ ->
    print_nat64_dec (List.Tot.index l i);
    IO.print_string " "
  ) ())


let print_string flag s = if flag then IO.print_string s else ()

let print_lbytes flag len b =
  if not flag then () else (
  let q = 32 in
  let n = len / q in
  let r = len % q in
  if n = 0 then (
    List.iter (fun a -> print_uint8_hex_pad a) (to_list b))
  else (
  repeat_range_all_ml 0 n (fun i _ ->
    let sb = sub #uint8 #len b (i * q) q in
    List.iter (fun a -> print_uint8_hex_pad a) (to_list sb);
    (if i < n - 1 then IO.print_string "\n" else ())) ();
  (if r <> 0 then IO.print_newline ());
  let sb = sub #uint8 #len b (n * q) r in
  List.iter (fun a -> print_uint8_hex_pad a) (to_list sb)))

let print_label_lbytes flag label len b =
  if not flag then () else (
  IO.print_string label;
  IO.print_string ": \n";
  print_lbytes flag len b;
  IO.print_newline ())

let print_compare flag len expected result =
  let r:bool = for_all2 (fun a b -> uint_to_nat #U8 a = uint_to_nat #U8 b) expected result in
  if (not flag) then r else (
  IO.print_string "\nResult:   ";
  List.iter (fun a -> print_uint8_hex_pad a) (to_list result);
  IO.print_string "\nExpected: ";
  List.iter (fun a -> print_uint8_hex_pad a) (to_list expected);
  r)

let print_compare_display flag len expected result =
  let r = for_all2 (fun a b -> uint_to_nat #U8 a = uint_to_nat #U8 b) expected result in
  if not flag then r
  else (
    if r then IO.print_string "\nSuccess !"
    else begin
      IO.print_string "\nResult:   ";
      List.iter (fun a -> print_uint8_hex_pad a) (to_list result);
      IO.print_string "\nExpected: ";
      List.iter (fun a -> print_uint8_hex_pad a) (to_list expected);
      IO.print_string "\nFailure !"
    end;
    r)
val print_compare_display_diff: display:bool -> len:size_nat -> expected:lbytes len -> result:lbytes len -> FStar.All.ML bool

    display: Prims.bool ->
    len: Lib.IntTypes.size_nat ->
    expected: Lib.ByteSequence.lbytes len ->
    result: Lib.ByteSequence.lbytes len
  -> FStar.All.ML Prims.bool