https://github.com/project-everest/hacl-star
Tip revision: 7b9dcb77c58c1186d18fe2cefe299c21bb0d7217 authored by Nikhil Swamy on 26 September 2019, 04:09:27 UTC
switch back to using F* master
switch back to using F* master
Tip revision: 7b9dcb7
Lib.PrintSequence.fst
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)
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)
let print_label_compare_display flag s 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 ! ";
IO.print_string s)
else begin
IO.print_string "\nFailure ! ";
IO.print_string s;
IO.print_newline ();
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)
end;
r)
let print_label_compare_display_diff flag s 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 ! ";
IO.print_string s;
IO.print_newline ())
else begin
IO.print_string "\nFailure ! ";
IO.print_string s;
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)