From 9cbbbe486e3becf9385fe56de4d4d72fab2c28dc Mon Sep 17 00:00:00 2001 From: "Vinzent \"Jellix\" Saranen" Date: Thu, 18 Jun 2020 21:03:12 +0200 Subject: [PATCH 1/4] * Implemented Max_(Success_)Proof_Time also for Files. --- src/spat-spark_info.adb | 70 +++++++++++++++++++++++++++++++++++++++++ src/spat-spark_info.ads | 17 ++++++++++ 2 files changed, 87 insertions(+) diff --git a/src/spat-spark_info.adb b/src/spat-spark_info.adb index f56c6ce..438f816 100644 --- a/src/spat-spark_info.adb +++ b/src/spat-spark_info.adb @@ -778,6 +778,39 @@ package body SPAT.Spark_Info is return Sentinel.Cache.Max_Proof_Time; end Max_Proof_Time; + --------------------------------------------------------------------------- + -- Max_Proof_Time + --------------------------------------------------------------------------- + not overriding + function Max_Proof_Time (This : in T; + File : in File_Name) return Duration + is + Result : Duration := -1.0; + File_Cursor : constant File_Sets.Cursor := This.Files.Find (Item => File); + use type File_Sets.Cursor; + begin + -- FIXME: We shouldn't need to iterate through all entities each time + -- this subprogram is called. + for Position in This.Entities.Iterate loop + if + Analyzed_Entities.Element (Position => Position).SPARK_File = + File_Cursor + then + declare + Reference : constant Analyzed_Entities.Constant_Reference_Type := + This.Entities.Constant_Reference (Position => Position); + Sentinel : constant Proofs_Sentinel := + Get_Sentinel (Node => Reference); + begin + Result := Duration'Max (Result, + Sentinel.Cache.Max_Proof_Time); + end; + end if; + end loop; + + return Result; + end Max_Proof_Time; + --------------------------------------------------------------------------- -- Max_Success_Proof_Time --------------------------------------------------------------------------- @@ -792,6 +825,43 @@ package body SPAT.Spark_Info is return Sentinel.Cache.Max_Success_Proof_Time; end Max_Success_Proof_Time; + --------------------------------------------------------------------------- + -- Max_Success_Proof_Time + --------------------------------------------------------------------------- + not overriding + function Max_Success_Proof_Time (This : in T; + File : in File_Name) return Duration + is + Result : Duration := -1.0; + File_Cursor : constant File_Sets.Cursor := This.Files.Find (Item => File); + use type File_Sets.Cursor; + begin + -- FIXME: We shouldn't need to iterate through all entities each time + -- this subprogram is called. + for Position in This.Entities.Iterate loop + if + Analyzed_Entities.Element (Position => Position).SPARK_File = + File_Cursor + then + declare + Reference : constant Analyzed_Entities.Constant_Reference_Type := + This.Entities.Constant_Reference (Position => Position); + Sentinel : constant Proofs_Sentinel := + Get_Sentinel (Node => Reference); + begin + if Sentinel.Cache.Has_Unproved_Attempts then + null; -- Unproved, so skip. + else + Result := Duration'Max (Result, + Sentinel.Cache.Max_Success_Proof_Time); + end if; + end; + end if; + end loop; + + return Result; + end Max_Success_Proof_Time; + --------------------------------------------------------------------------- -- Num_Flows --------------------------------------------------------------------------- diff --git a/src/spat-spark_info.ads b/src/spat-spark_info.ads index 1b426d8..5ead0c0 100644 --- a/src/spat-spark_info.ads +++ b/src/spat-spark_info.ads @@ -103,6 +103,23 @@ package SPAT.Spark_Info is function Proof_Time (This : in T; File : in File_Name) return Duration; + --------------------------------------------------------------------------- + -- Max_Proof_Time + --------------------------------------------------------------------------- + not overriding + function Max_Proof_Time (This : in T; + File : in File_Name) return Duration; + + --------------------------------------------------------------------------- + -- Max_Success_Proof_Time + -- + -- Reported time for the longest successful proof. + -- If the time returned is -1.0, then nothing is proven. + --------------------------------------------------------------------------- + not overriding + function Max_Success_Proof_Time (This : in T; + File : in File_Name) return Duration; + --------------------------------------------------------------------------- -- Max_Proof_Time -- From 8138cca701482180ae01f31260e9d49386e620ce Mon Sep 17 00:00:00 2001 From: "Vinzent \"Jellix\" Saranen" Date: Thu, 18 Jun 2020 21:03:45 +0200 Subject: [PATCH 2/4] * Summary output like with entities (max_success/max/total). --- src/run_spat-print_summary.adb | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) diff --git a/src/run_spat-print_summary.adb b/src/run_spat-print_summary.adb index 974ecd7..56f0a7f 100644 --- a/src/run_spat-print_summary.adb +++ b/src/run_spat-print_summary.adb @@ -37,6 +37,8 @@ begin for File of Files loop -- Can't use Files.Max_Length here, because we use the Simple_Name, not -- the actual string stored. + -- FIXME: This assumes that everything is displayed, the actual output + -- might be less and the tabulation is a bit wide. Second_Column := Ada.Text_IO.Count'Max (Second_Column, Ada.Directories.Simple_Name @@ -66,10 +68,20 @@ begin New_Line => False); Ada.Text_IO.Set_Col (File => Ada.Text_IO.Standard_Output, To => Third_Column); - SPAT.Log.Message - (Message => - "Proof => " & - SPAT.Image (Value => Info.Proof_Time (File => File)) & ")"); + + declare + Max_Success_Proof_Time : constant Duration := + Info.Max_Success_Proof_Time (File => File); + begin + SPAT.Log.Message + (Message => + "Proof => " & + (if Max_Success_Proof_Time = -1.0 -- nothing valid found + then "--" + else SPAT.Image (Value => Max_Success_Proof_Time)) & "/" & + SPAT.Image (Value => Info.Max_Proof_Time (File => File)) & "/" & + SPAT.Image (Value => Info.Proof_Time (File => File)) & ")"); + end; end if; end loop; From ab4a4ae040a56615bd55ff194d8ac828323da425 Mon Sep 17 00:00:00 2001 From: "Vinzent \"Jellix\" Saranen" Date: Thu, 18 Jun 2020 21:04:04 +0200 Subject: [PATCH 3/4] * Updated templates. --- test/spat.test-issues.sca.template | 2 +- test/spat.test-issues.scs.template | 2 +- test/spat.test-issues.sct.template | 2 +- test/spat.test-issues.sdca.template | 2 +- test/spat.test-issues.sdcs.template | 2 +- test/spat.test-issues.sdct.template | 2 +- test/spat.test-issues.sraca.template | 2 +- test/spat.test-issues.sracs.template | 2 +- test/spat.test-issues.sract.template | 2 +- test/spat.test-issues.sradca.template | 2 +- test/spat.test-issues.sradcs.template | 2 +- test/spat.test-issues.sradct.template | 2 +- test/spat.test-issues.srfca.template | 2 +- test/spat.test-issues.srfcs.template | 2 +- test/spat.test-issues.srfct.template | 2 +- test/spat.test-issues.srfdca.template | 2 +- test/spat.test-issues.srfdcs.template | 2 +- test/spat.test-issues.srfdct.template | 2 +- test/spat.test-issues.srjca.template | 2 +- test/spat.test-issues.srjcs.template | 2 +- test/spat.test-issues.srjct.template | 2 +- test/spat.test-issues.srjdca.template | 2 +- test/spat.test-issues.srjdcs.template | 2 +- test/spat.test-issues.srjdct.template | 2 +- test/spat.test-issues.sruca.template | 2 +- test/spat.test-issues.srucs.template | 2 +- test/spat.test-issues.sruct.template | 2 +- test/spat.test-issues.srudca.template | 2 +- test/spat.test-issues.srudcs.template | 2 +- test/spat.test-issues.srudct.template | 2 +- test/spat.test-saatana.sca.template | 10 ++++----- test/spat.test-saatana.scs.template | 10 ++++----- test/spat.test-saatana.sct.template | 10 ++++----- test/spat.test-saatana.sdca.template | 10 ++++----- test/spat.test-saatana.sdcs.template | 10 ++++----- test/spat.test-saatana.sdct.template | 10 ++++----- test/spat.test-saatana.sraca.template | 10 ++++----- test/spat.test-saatana.sracs.template | 10 ++++----- test/spat.test-saatana.sract.template | 10 ++++----- test/spat.test-saatana.sradca.template | 10 ++++----- test/spat.test-saatana.sradcs.template | 10 ++++----- test/spat.test-saatana.sradct.template | 10 ++++----- test/spat.test-saatana.srfca.template | 10 ++++----- test/spat.test-saatana.srfcs.template | 10 ++++----- test/spat.test-saatana.srfct.template | 10 ++++----- test/spat.test-saatana.srfdca.template | 10 ++++----- test/spat.test-saatana.srfdcs.template | 10 ++++----- test/spat.test-saatana.srfdct.template | 10 ++++----- test/spat.test-saatana.srjca.template | 10 ++++----- test/spat.test-saatana.srjcs.template | 10 ++++----- test/spat.test-saatana.srjct.template | 10 ++++----- test/spat.test-saatana.srjdca.template | 10 ++++----- test/spat.test-saatana.srjdcs.template | 10 ++++----- test/spat.test-saatana.srjdct.template | 10 ++++----- test/spat.test-saatana.sruca.template | 10 ++++----- test/spat.test-saatana.srucs.template | 10 ++++----- test/spat.test-saatana.sruct.template | 10 ++++----- test/spat.test-saatana.srudca.template | 10 ++++----- test/spat.test-saatana.srudcs.template | 10 ++++----- test/spat.test-saatana.srudct.template | 10 ++++----- test/spat.test-sparknacl.sca.template | 28 ++++++++++++------------ test/spat.test-sparknacl.scs.template | 28 ++++++++++++------------ test/spat.test-sparknacl.sct.template | 28 ++++++++++++------------ test/spat.test-sparknacl.sdca.template | 28 ++++++++++++------------ test/spat.test-sparknacl.sdcs.template | 28 ++++++++++++------------ test/spat.test-sparknacl.sdct.template | 28 ++++++++++++------------ test/spat.test-sparknacl.sraca.template | 28 ++++++++++++------------ test/spat.test-sparknacl.sracs.template | 28 ++++++++++++------------ test/spat.test-sparknacl.sract.template | 28 ++++++++++++------------ test/spat.test-sparknacl.sradca.template | 28 ++++++++++++------------ test/spat.test-sparknacl.sradcs.template | 28 ++++++++++++------------ test/spat.test-sparknacl.sradct.template | 28 ++++++++++++------------ test/spat.test-sparknacl.srfca.template | 28 ++++++++++++------------ test/spat.test-sparknacl.srfcs.template | 28 ++++++++++++------------ test/spat.test-sparknacl.srfct.template | 28 ++++++++++++------------ test/spat.test-sparknacl.srfdca.template | 28 ++++++++++++------------ test/spat.test-sparknacl.srfdcs.template | 28 ++++++++++++------------ test/spat.test-sparknacl.srfdct.template | 28 ++++++++++++------------ test/spat.test-sparknacl.srjca.template | 28 ++++++++++++------------ test/spat.test-sparknacl.srjcs.template | 28 ++++++++++++------------ test/spat.test-sparknacl.srjct.template | 28 ++++++++++++------------ test/spat.test-sparknacl.srjdca.template | 28 ++++++++++++------------ test/spat.test-sparknacl.srjdcs.template | 28 ++++++++++++------------ test/spat.test-sparknacl.srjdct.template | 28 ++++++++++++------------ test/spat.test-sparknacl.sruca.template | 28 ++++++++++++------------ test/spat.test-sparknacl.srucs.template | 28 ++++++++++++------------ test/spat.test-sparknacl.sruct.template | 28 ++++++++++++------------ test/spat.test-sparknacl.srudca.template | 28 ++++++++++++------------ test/spat.test-sparknacl.srudcs.template | 28 ++++++++++++------------ test/spat.test-sparknacl.srudct.template | 28 ++++++++++++------------ 90 files changed, 600 insertions(+), 600 deletions(-) diff --git a/test/spat.test-issues.sca.template b/test/spat.test-issues.sca.template index 2ae7ac7..fd863eb 100644 --- a/test/spat.test-issues.sca.template +++ b/test/spat.test-issues.sca.template @@ -1,2 +1,2 @@ rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) diff --git a/test/spat.test-issues.scs.template b/test/spat.test-issues.scs.template index f1e5fb6..06319a6 100644 --- a/test/spat.test-issues.scs.template +++ b/test/spat.test-issues.scs.template @@ -1,3 +1,3 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) diff --git a/test/spat.test-issues.sct.template b/test/spat.test-issues.sct.template index f1e5fb6..06319a6 100644 --- a/test/spat.test-issues.sct.template +++ b/test/spat.test-issues.sct.template @@ -1,3 +1,3 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) diff --git a/test/spat.test-issues.sdca.template b/test/spat.test-issues.sdca.template index 2ae7ac7..fd863eb 100644 --- a/test/spat.test-issues.sdca.template +++ b/test/spat.test-issues.sdca.template @@ -1,2 +1,2 @@ rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) diff --git a/test/spat.test-issues.sdcs.template b/test/spat.test-issues.sdcs.template index f1e5fb6..06319a6 100644 --- a/test/spat.test-issues.sdcs.template +++ b/test/spat.test-issues.sdcs.template @@ -1,3 +1,3 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) diff --git a/test/spat.test-issues.sdct.template b/test/spat.test-issues.sdct.template index f1e5fb6..06319a6 100644 --- a/test/spat.test-issues.sdct.template +++ b/test/spat.test-issues.sdct.template @@ -1,3 +1,3 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) diff --git a/test/spat.test-issues.sraca.template b/test/spat.test-issues.sraca.template index 6149b7f..35b773c 100644 --- a/test/spat.test-issues.sraca.template +++ b/test/spat.test-issues.sraca.template @@ -1,5 +1,5 @@ rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) RFLX.RFLX_Types => 0.0 s/0.0 s/0.0 s RFLX.RFLX_Types.Byte_Index => 10.0 ms/10.0 ms/30.0 ms RFLX.RFLX_Types.First_Bit_Index => 0.0 s/0.0 s/0.0 s diff --git a/test/spat.test-issues.sracs.template b/test/spat.test-issues.sracs.template index 673a609..a5e52b1 100644 --- a/test/spat.test-issues.sracs.template +++ b/test/spat.test-issues.sracs.template @@ -1,6 +1,6 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) RFLX.RFLX_Types.U64_Insert => 54.2 s/120.0 s/1.6 ks RFLX.RFLX_Types.U64_Extract => 37.9 s/120.0 s/1.8 ks RFLX.RFLX_Types.U64_Extract_Remaining => 10.1 s/120.0 s/376.5 s diff --git a/test/spat.test-issues.sract.template b/test/spat.test-issues.sract.template index 0c62a0c..bb111ff 100644 --- a/test/spat.test-issues.sract.template +++ b/test/spat.test-issues.sract.template @@ -1,6 +1,6 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) RFLX.RFLX_Types.U64_Extract => 37.9 s/120.0 s/1.8 ks RFLX.RFLX_Types.U64_Insert => 54.2 s/120.0 s/1.6 ks RFLX.RFLX_Types.U64_Extract_Intermediate => 6.7 s/120.0 s/617.3 s diff --git a/test/spat.test-issues.sradca.template b/test/spat.test-issues.sradca.template index 91cc8da..1296bb7 100644 --- a/test/spat.test-issues.sradca.template +++ b/test/spat.test-issues.sradca.template @@ -1,5 +1,5 @@ rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) RFLX.RFLX_Types => 0.0 s/0.0 s/0.0 s RFLX.RFLX_Types.Byte_Index => 10.0 ms/10.0 ms/30.0 ms `-VC_DIVISION_CHECK rflx-rflx_generic_types.ads:36:36 => 10.0 ms/10.0 ms/10.0 ms diff --git a/test/spat.test-issues.sradcs.template b/test/spat.test-issues.sradcs.template index a404f59..65d1095 100644 --- a/test/spat.test-issues.sradcs.template +++ b/test/spat.test-issues.sradcs.template @@ -1,6 +1,6 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) RFLX.RFLX_Types.U64_Insert => 54.2 s/120.0 s/1.6 ks `-VC_PRECONDITION rflx-rflx_generic_types.adb:221:39 => 5.2 s/120.0 s/490.6 s `-CVC4: 120.0 s (Timeout,-1 steps) diff --git a/test/spat.test-issues.sradct.template b/test/spat.test-issues.sradct.template index 2183dca..d8a5f08 100644 --- a/test/spat.test-issues.sradct.template +++ b/test/spat.test-issues.sradct.template @@ -1,6 +1,6 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) RFLX.RFLX_Types.U64_Extract => 37.9 s/120.0 s/1.8 ks `-VC_PRECONDITION rflx-rflx_generic_types.adb:131:29 => 37.9 s/120.0 s/1.1 ks `-Z3: 120.0 s (Timeout,-1 steps) diff --git a/test/spat.test-issues.srfca.template b/test/spat.test-issues.srfca.template index 436aa9e..3f6ce94 100644 --- a/test/spat.test-issues.srfca.template +++ b/test/spat.test-issues.srfca.template @@ -1,5 +1,5 @@ rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) RFLX.RFLX_Types.U64_Extract => 37.9 s/120.0 s/1.8 ks RFLX.RFLX_Types.U64_Extract.D => 4.7 s/9.5 s/70.6 s RFLX.RFLX_Types.U64_Extract_Intermediate => 6.7 s/120.0 s/617.3 s diff --git a/test/spat.test-issues.srfcs.template b/test/spat.test-issues.srfcs.template index 458322b..c9f8526 100644 --- a/test/spat.test-issues.srfcs.template +++ b/test/spat.test-issues.srfcs.template @@ -1,6 +1,6 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) RFLX.RFLX_Types.U64_Insert => 54.2 s/120.0 s/1.6 ks RFLX.RFLX_Types.U64_Extract => 37.9 s/120.0 s/1.8 ks RFLX.RFLX_Types.U64_Extract_Remaining => 10.1 s/120.0 s/376.5 s diff --git a/test/spat.test-issues.srfct.template b/test/spat.test-issues.srfct.template index 42f9517..ecdd8b5 100644 --- a/test/spat.test-issues.srfct.template +++ b/test/spat.test-issues.srfct.template @@ -1,6 +1,6 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) RFLX.RFLX_Types.U64_Extract => 37.9 s/120.0 s/1.8 ks RFLX.RFLX_Types.U64_Insert => 54.2 s/120.0 s/1.6 ks RFLX.RFLX_Types.U64_Extract_Intermediate => 6.7 s/120.0 s/617.3 s diff --git a/test/spat.test-issues.srfdca.template b/test/spat.test-issues.srfdca.template index 85bc036..578b1ad 100644 --- a/test/spat.test-issues.srfdca.template +++ b/test/spat.test-issues.srfdca.template @@ -1,5 +1,5 @@ rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) RFLX.RFLX_Types.U64_Extract => 37.9 s/120.0 s/1.8 ks `-VC_PRECONDITION rflx-rflx_generic_types.adb:131:29 => 37.9 s/120.0 s/1.1 ks `-Z3: 120.0 s (Timeout,-1 steps) diff --git a/test/spat.test-issues.srfdcs.template b/test/spat.test-issues.srfdcs.template index 1d5c0c6..6ec47fd 100644 --- a/test/spat.test-issues.srfdcs.template +++ b/test/spat.test-issues.srfdcs.template @@ -1,6 +1,6 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) RFLX.RFLX_Types.U64_Insert => 54.2 s/120.0 s/1.6 ks `-VC_PRECONDITION rflx-rflx_generic_types.adb:221:39 => 5.2 s/120.0 s/490.6 s `-CVC4: 120.0 s (Timeout,-1 steps) diff --git a/test/spat.test-issues.srfdct.template b/test/spat.test-issues.srfdct.template index 9d3b803..b4bb2f5 100644 --- a/test/spat.test-issues.srfdct.template +++ b/test/spat.test-issues.srfdct.template @@ -1,6 +1,6 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) RFLX.RFLX_Types.U64_Extract => 37.9 s/120.0 s/1.8 ks `-VC_PRECONDITION rflx-rflx_generic_types.adb:131:29 => 37.9 s/120.0 s/1.1 ks `-Z3: 120.0 s (Timeout,-1 steps) diff --git a/test/spat.test-issues.srjca.template b/test/spat.test-issues.srjca.template index 2ae7ac7..fd863eb 100644 --- a/test/spat.test-issues.srjca.template +++ b/test/spat.test-issues.srjca.template @@ -1,2 +1,2 @@ rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) diff --git a/test/spat.test-issues.srjcs.template b/test/spat.test-issues.srjcs.template index f1e5fb6..06319a6 100644 --- a/test/spat.test-issues.srjcs.template +++ b/test/spat.test-issues.srjcs.template @@ -1,3 +1,3 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) diff --git a/test/spat.test-issues.srjct.template b/test/spat.test-issues.srjct.template index f1e5fb6..06319a6 100644 --- a/test/spat.test-issues.srjct.template +++ b/test/spat.test-issues.srjct.template @@ -1,3 +1,3 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) diff --git a/test/spat.test-issues.srjdca.template b/test/spat.test-issues.srjdca.template index 2ae7ac7..fd863eb 100644 --- a/test/spat.test-issues.srjdca.template +++ b/test/spat.test-issues.srjdca.template @@ -1,2 +1,2 @@ rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) diff --git a/test/spat.test-issues.srjdcs.template b/test/spat.test-issues.srjdcs.template index f1e5fb6..06319a6 100644 --- a/test/spat.test-issues.srjdcs.template +++ b/test/spat.test-issues.srjdcs.template @@ -1,3 +1,3 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) diff --git a/test/spat.test-issues.srjdct.template b/test/spat.test-issues.srjdct.template index f1e5fb6..06319a6 100644 --- a/test/spat.test-issues.srjdct.template +++ b/test/spat.test-issues.srjdct.template @@ -1,3 +1,3 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) diff --git a/test/spat.test-issues.sruca.template b/test/spat.test-issues.sruca.template index 2ae7ac7..fd863eb 100644 --- a/test/spat.test-issues.sruca.template +++ b/test/spat.test-issues.sruca.template @@ -1,2 +1,2 @@ rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) diff --git a/test/spat.test-issues.srucs.template b/test/spat.test-issues.srucs.template index f1e5fb6..06319a6 100644 --- a/test/spat.test-issues.srucs.template +++ b/test/spat.test-issues.srucs.template @@ -1,3 +1,3 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) diff --git a/test/spat.test-issues.sruct.template b/test/spat.test-issues.sruct.template index f1e5fb6..06319a6 100644 --- a/test/spat.test-issues.sruct.template +++ b/test/spat.test-issues.sruct.template @@ -1,3 +1,3 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) diff --git a/test/spat.test-issues.srudca.template b/test/spat.test-issues.srudca.template index 2ae7ac7..fd863eb 100644 --- a/test/spat.test-issues.srudca.template +++ b/test/spat.test-issues.srudca.template @@ -1,2 +1,2 @@ rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) diff --git a/test/spat.test-issues.srudcs.template b/test/spat.test-issues.srudcs.template index f1e5fb6..06319a6 100644 --- a/test/spat.test-issues.srudcs.template +++ b/test/spat.test-issues.srudcs.template @@ -1,3 +1,3 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) diff --git a/test/spat.test-issues.srudct.template b/test/spat.test-issues.srudct.template index f1e5fb6..06319a6 100644 --- a/test/spat.test-issues.srudct.template +++ b/test/spat.test-issues.srudct.template @@ -1,3 +1,3 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. rflx-rflx_types.spark => (Flow => 7.2 ms, - Proof => 4.5 ks) + Proof => 54.2 s/120.0 s/4.5 ks) diff --git a/test/spat.test-saatana.sca.template b/test/spat.test-saatana.sca.template index 2e53304..02041a3 100644 --- a/test/spat.test-saatana.sca.template +++ b/test/spat.test-saatana.sca.template @@ -1,10 +1,10 @@ saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) diff --git a/test/spat.test-saatana.scs.template b/test/spat.test-saatana.scs.template index 2a5530b..7ccbefa 100644 --- a/test/spat.test-saatana.scs.template +++ b/test/spat.test-saatana.scs.template @@ -1,11 +1,11 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) diff --git a/test/spat.test-saatana.sct.template b/test/spat.test-saatana.sct.template index 2a5530b..7ccbefa 100644 --- a/test/spat.test-saatana.sct.template +++ b/test/spat.test-saatana.sct.template @@ -1,11 +1,11 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) diff --git a/test/spat.test-saatana.sdca.template b/test/spat.test-saatana.sdca.template index 2e53304..02041a3 100644 --- a/test/spat.test-saatana.sdca.template +++ b/test/spat.test-saatana.sdca.template @@ -1,10 +1,10 @@ saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) diff --git a/test/spat.test-saatana.sdcs.template b/test/spat.test-saatana.sdcs.template index 2a5530b..7ccbefa 100644 --- a/test/spat.test-saatana.sdcs.template +++ b/test/spat.test-saatana.sdcs.template @@ -1,11 +1,11 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) diff --git a/test/spat.test-saatana.sdct.template b/test/spat.test-saatana.sdct.template index 2a5530b..7ccbefa 100644 --- a/test/spat.test-saatana.sdct.template +++ b/test/spat.test-saatana.sdct.template @@ -1,11 +1,11 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) diff --git a/test/spat.test-saatana.sraca.template b/test/spat.test-saatana.sraca.template index 32a7839..a9c4d34 100644 --- a/test/spat.test-saatana.sraca.template +++ b/test/spat.test-saatana.sraca.template @@ -1,13 +1,13 @@ saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) Saatana => 0.0 s/0.0 s/0.0 s Saatana.Crypto => 0.0 s/0.0 s/0.0 s Saatana.Crypto.Lemmas => 210.0 ms/210.0 ms/700.0 ms diff --git a/test/spat.test-saatana.sracs.template b/test/spat.test-saatana.sracs.template index 6196737..5cd36e3 100644 --- a/test/spat.test-saatana.sracs.template +++ b/test/spat.test-saatana.sracs.template @@ -1,14 +1,14 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) Saatana.Crypto.Phelix.Encrypt_Bytes => 174.3 s/174.3 s/189.0 s Saatana.Crypto.Phelix.H => 6.0 s/6.0 s/6.0 s Saatana.Crypto.Phelix.Decrypt_Bytes => 4.0 s/4.0 s/18.6 s diff --git a/test/spat.test-saatana.sract.template b/test/spat.test-saatana.sract.template index 5727441..f63992e 100644 --- a/test/spat.test-saatana.sract.template +++ b/test/spat.test-saatana.sract.template @@ -1,14 +1,14 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) Saatana.Crypto.Phelix.Setup_Key => 640.0 ms/206.4 s/219.2 s Saatana.Crypto.Phelix.Encrypt_Bytes => 174.3 s/174.3 s/189.0 s Saatana.Crypto.Phelix.Decrypt_Bytes => 4.0 s/4.0 s/18.6 s diff --git a/test/spat.test-saatana.sradca.template b/test/spat.test-saatana.sradca.template index ec35ba6..fbf7b43 100644 --- a/test/spat.test-saatana.sradca.template +++ b/test/spat.test-saatana.sradca.template @@ -1,13 +1,13 @@ saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) Saatana => 0.0 s/0.0 s/0.0 s Saatana.Crypto => 0.0 s/0.0 s/0.0 s Saatana.Crypto.Lemmas => 210.0 ms/210.0 ms/700.0 ms diff --git a/test/spat.test-saatana.sradcs.template b/test/spat.test-saatana.sradcs.template index d26cde3..6b95648 100644 --- a/test/spat.test-saatana.sradcs.template +++ b/test/spat.test-saatana.sradcs.template @@ -1,14 +1,14 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) Saatana.Crypto.Phelix.Encrypt_Bytes => 174.3 s/174.3 s/189.0 s `-VC_RANGE_CHECK saatana-crypto-phelix.adb:231:19 => 174.3 s/174.3 s/175.0 s `-Z3: 174.3 s (Valid, 8585912 steps) diff --git a/test/spat.test-saatana.sradct.template b/test/spat.test-saatana.sradct.template index d35622c..6bb57a1 100644 --- a/test/spat.test-saatana.sradct.template +++ b/test/spat.test-saatana.sradct.template @@ -1,14 +1,14 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) Saatana.Crypto.Phelix.Setup_Key => 640.0 ms/206.4 s/219.2 s `-VC_RANGE_CHECK saatana-crypto-phelix.adb:466:44 => 640.0 ms/206.4 s/207.1 s `-Z3: 206.4 s (Unknown (unknown), 105312169 steps) diff --git a/test/spat.test-saatana.srfca.template b/test/spat.test-saatana.srfca.template index 8706023..bb004f4 100644 --- a/test/spat.test-saatana.srfca.template +++ b/test/spat.test-saatana.srfca.template @@ -1,11 +1,11 @@ saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) Saatana.Crypto.Phelix.Setup_Key => 640.0 ms/206.4 s/219.2 s diff --git a/test/spat.test-saatana.srfcs.template b/test/spat.test-saatana.srfcs.template index 7beb262..997747b 100644 --- a/test/spat.test-saatana.srfcs.template +++ b/test/spat.test-saatana.srfcs.template @@ -1,12 +1,12 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) Saatana.Crypto.Phelix.Setup_Key => 640.0 ms/206.4 s/219.2 s diff --git a/test/spat.test-saatana.srfct.template b/test/spat.test-saatana.srfct.template index 7beb262..997747b 100644 --- a/test/spat.test-saatana.srfct.template +++ b/test/spat.test-saatana.srfct.template @@ -1,12 +1,12 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) Saatana.Crypto.Phelix.Setup_Key => 640.0 ms/206.4 s/219.2 s diff --git a/test/spat.test-saatana.srfdca.template b/test/spat.test-saatana.srfdca.template index 54149c9..5732d7d 100644 --- a/test/spat.test-saatana.srfdca.template +++ b/test/spat.test-saatana.srfdca.template @@ -1,13 +1,13 @@ saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) Saatana.Crypto.Phelix.Setup_Key => 640.0 ms/206.4 s/219.2 s `-VC_RANGE_CHECK saatana-crypto-phelix.adb:466:44 => 640.0 ms/206.4 s/207.1 s `-Z3: 206.4 s (Unknown (unknown), 105312169 steps) diff --git a/test/spat.test-saatana.srfdcs.template b/test/spat.test-saatana.srfdcs.template index 2370978..a87c469 100644 --- a/test/spat.test-saatana.srfdcs.template +++ b/test/spat.test-saatana.srfdcs.template @@ -1,14 +1,14 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) Saatana.Crypto.Phelix.Setup_Key => 640.0 ms/206.4 s/219.2 s `-VC_RANGE_CHECK saatana-crypto-phelix.adb:466:44 => 640.0 ms/206.4 s/207.1 s `-Z3: 206.4 s (Unknown (unknown), 105312169 steps) diff --git a/test/spat.test-saatana.srfdct.template b/test/spat.test-saatana.srfdct.template index 2370978..a87c469 100644 --- a/test/spat.test-saatana.srfdct.template +++ b/test/spat.test-saatana.srfdct.template @@ -1,14 +1,14 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) Saatana.Crypto.Phelix.Setup_Key => 640.0 ms/206.4 s/219.2 s `-VC_RANGE_CHECK saatana-crypto-phelix.adb:466:44 => 640.0 ms/206.4 s/207.1 s `-Z3: 206.4 s (Unknown (unknown), 105312169 steps) diff --git a/test/spat.test-saatana.srjca.template b/test/spat.test-saatana.srjca.template index 2e53304..02041a3 100644 --- a/test/spat.test-saatana.srjca.template +++ b/test/spat.test-saatana.srjca.template @@ -1,10 +1,10 @@ saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) diff --git a/test/spat.test-saatana.srjcs.template b/test/spat.test-saatana.srjcs.template index 2a5530b..7ccbefa 100644 --- a/test/spat.test-saatana.srjcs.template +++ b/test/spat.test-saatana.srjcs.template @@ -1,11 +1,11 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) diff --git a/test/spat.test-saatana.srjct.template b/test/spat.test-saatana.srjct.template index 2a5530b..7ccbefa 100644 --- a/test/spat.test-saatana.srjct.template +++ b/test/spat.test-saatana.srjct.template @@ -1,11 +1,11 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) diff --git a/test/spat.test-saatana.srjdca.template b/test/spat.test-saatana.srjdca.template index 2e53304..02041a3 100644 --- a/test/spat.test-saatana.srjdca.template +++ b/test/spat.test-saatana.srjdca.template @@ -1,10 +1,10 @@ saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) diff --git a/test/spat.test-saatana.srjdcs.template b/test/spat.test-saatana.srjdcs.template index 2a5530b..7ccbefa 100644 --- a/test/spat.test-saatana.srjdcs.template +++ b/test/spat.test-saatana.srjdcs.template @@ -1,11 +1,11 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) diff --git a/test/spat.test-saatana.srjdct.template b/test/spat.test-saatana.srjdct.template index 2a5530b..7ccbefa 100644 --- a/test/spat.test-saatana.srjdct.template +++ b/test/spat.test-saatana.srjdct.template @@ -1,11 +1,11 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) diff --git a/test/spat.test-saatana.sruca.template b/test/spat.test-saatana.sruca.template index 2e53304..02041a3 100644 --- a/test/spat.test-saatana.sruca.template +++ b/test/spat.test-saatana.sruca.template @@ -1,10 +1,10 @@ saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) diff --git a/test/spat.test-saatana.srucs.template b/test/spat.test-saatana.srucs.template index 2a5530b..7ccbefa 100644 --- a/test/spat.test-saatana.srucs.template +++ b/test/spat.test-saatana.srucs.template @@ -1,11 +1,11 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) diff --git a/test/spat.test-saatana.sruct.template b/test/spat.test-saatana.sruct.template index 2a5530b..7ccbefa 100644 --- a/test/spat.test-saatana.sruct.template +++ b/test/spat.test-saatana.sruct.template @@ -1,11 +1,11 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) diff --git a/test/spat.test-saatana.srudca.template b/test/spat.test-saatana.srudca.template index 2e53304..02041a3 100644 --- a/test/spat.test-saatana.srudca.template +++ b/test/spat.test-saatana.srudca.template @@ -1,10 +1,10 @@ saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) diff --git a/test/spat.test-saatana.srudcs.template b/test/spat.test-saatana.srudcs.template index 2a5530b..7ccbefa 100644 --- a/test/spat.test-saatana.srudcs.template +++ b/test/spat.test-saatana.srudcs.template @@ -1,11 +1,11 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) diff --git a/test/spat.test-saatana.srudct.template b/test/spat.test-saatana.srudct.template index 2a5530b..7ccbefa 100644 --- a/test/spat.test-saatana.srudct.template +++ b/test/spat.test-saatana.srudct.template @@ -1,11 +1,11 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) diff --git a/test/spat.test-sparknacl.sca.template b/test/spat.test-sparknacl.sca.template index 803ae8a..d48173a 100644 --- a/test/spat.test-sparknacl.sca.template +++ b/test/spat.test-sparknacl.sca.template @@ -1,28 +1,28 @@ random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) diff --git a/test/spat.test-sparknacl.scs.template b/test/spat.test-sparknacl.scs.template index 45b4be0..cb34931 100644 --- a/test/spat.test-sparknacl.scs.template +++ b/test/spat.test-sparknacl.scs.template @@ -1,29 +1,29 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) diff --git a/test/spat.test-sparknacl.sct.template b/test/spat.test-sparknacl.sct.template index 45b4be0..cb34931 100644 --- a/test/spat.test-sparknacl.sct.template +++ b/test/spat.test-sparknacl.sct.template @@ -1,29 +1,29 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) diff --git a/test/spat.test-sparknacl.sdca.template b/test/spat.test-sparknacl.sdca.template index 803ae8a..d48173a 100644 --- a/test/spat.test-sparknacl.sdca.template +++ b/test/spat.test-sparknacl.sdca.template @@ -1,28 +1,28 @@ random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) diff --git a/test/spat.test-sparknacl.sdcs.template b/test/spat.test-sparknacl.sdcs.template index 45b4be0..cb34931 100644 --- a/test/spat.test-sparknacl.sdcs.template +++ b/test/spat.test-sparknacl.sdcs.template @@ -1,29 +1,29 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) diff --git a/test/spat.test-sparknacl.sdct.template b/test/spat.test-sparknacl.sdct.template index 45b4be0..cb34931 100644 --- a/test/spat.test-sparknacl.sdct.template +++ b/test/spat.test-sparknacl.sdct.template @@ -1,29 +1,29 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) diff --git a/test/spat.test-sparknacl.sraca.template b/test/spat.test-sparknacl.sraca.template index 123b03a..98f70ca 100644 --- a/test/spat.test-sparknacl.sraca.template +++ b/test/spat.test-sparknacl.sraca.template @@ -1,31 +1,31 @@ random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) Random => 0.0 s/0.0 s/0.0 s Random.Random_Byte => 0.0 s/0.0 s/0.0 s SPARKNaCl => 80.0 ms/80.0 ms/260.0 ms diff --git a/test/spat.test-sparknacl.sracs.template b/test/spat.test-sparknacl.sracs.template index d990ce7..8476166 100644 --- a/test/spat.test-sparknacl.sracs.template +++ b/test/spat.test-sparknacl.sracs.template @@ -1,32 +1,32 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) SPARKNaCl.Sign.ModL.Eliminate_Limbs_62_To_32 => 9.2 s/9.2 s/148.2 s SPARKNaCl.Sign.Sign => --/57.6 s/489.2 s SPARKNaCl.Sign.ModL.Finalize => 2.1 s/2.1 s/27.1 s diff --git a/test/spat.test-sparknacl.sract.template b/test/spat.test-sparknacl.sract.template index abdf40e..389810d 100644 --- a/test/spat.test-sparknacl.sract.template +++ b/test/spat.test-sparknacl.sract.template @@ -1,32 +1,32 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) SPARKNaCl.Sign.Sign => --/57.6 s/489.2 s SPARKNaCl.Sign.ModL.Eliminate_Limbs_62_To_32 => 9.2 s/9.2 s/148.2 s SPARKNaCl.Omultiply => 700.0 ms/19.1 s/28.6 s diff --git a/test/spat.test-sparknacl.sradca.template b/test/spat.test-sparknacl.sradca.template index f873423..033817f 100644 --- a/test/spat.test-sparknacl.sradca.template +++ b/test/spat.test-sparknacl.sradca.template @@ -1,31 +1,31 @@ random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) Random => 0.0 s/0.0 s/0.0 s Random.Random_Byte => 0.0 s/0.0 s/0.0 s SPARKNaCl => 80.0 ms/80.0 ms/260.0 ms diff --git a/test/spat.test-sparknacl.sradcs.template b/test/spat.test-sparknacl.sradcs.template index 43228cd..0a3d4ed 100644 --- a/test/spat.test-sparknacl.sradcs.template +++ b/test/spat.test-sparknacl.sradcs.template @@ -1,32 +1,32 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) SPARKNaCl.Sign.ModL.Eliminate_Limbs_62_To_32 => 9.2 s/9.2 s/148.2 s `-VC_RANGE_CHECK sparknacl-sign.adb:433:54 => 9.2 s/9.2 s/11.3 s `-CVC4: 9.2 s (Valid, 157187 steps) diff --git a/test/spat.test-sparknacl.sradct.template b/test/spat.test-sparknacl.sradct.template index 19c2029..263d270 100644 --- a/test/spat.test-sparknacl.sradct.template +++ b/test/spat.test-sparknacl.sradct.template @@ -1,32 +1,32 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) SPARKNaCl.Sign.Sign => --/57.6 s/489.2 s `-VC_OVERFLOW_CHECK sparknacl-sign.adb:890:36 => --/57.6 s/238.7 s `-CVC4: 57.6 s (Unknown (unknown), 505002 steps) diff --git a/test/spat.test-sparknacl.srfca.template b/test/spat.test-sparknacl.srfca.template index 5b7fb7d..2862b07 100644 --- a/test/spat.test-sparknacl.srfca.template +++ b/test/spat.test-sparknacl.srfca.template @@ -1,31 +1,31 @@ random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) SPARKNaCl.ASR_16 => --/5.7 s/5.9 s SPARKNaCl.ASR_4 => --/1.2 s/1.4 s SPARKNaCl.ASR_8 => --/3.3 s/3.5 s diff --git a/test/spat.test-sparknacl.srfcs.template b/test/spat.test-sparknacl.srfcs.template index eab7a28..10bab37 100644 --- a/test/spat.test-sparknacl.srfcs.template +++ b/test/spat.test-sparknacl.srfcs.template @@ -1,32 +1,32 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) SPARKNaCl.Sign.Sign => --/57.6 s/489.2 s SPARKNaCl.Car.Nearlynormal_To_Normal => --/1.4 s/17.5 s SPARKNaCl.Omultiply => 700.0 ms/19.1 s/28.6 s diff --git a/test/spat.test-sparknacl.srfct.template b/test/spat.test-sparknacl.srfct.template index eb0b7ed..f2e40a5 100644 --- a/test/spat.test-sparknacl.srfct.template +++ b/test/spat.test-sparknacl.srfct.template @@ -1,32 +1,32 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) SPARKNaCl.Sign.Sign => --/57.6 s/489.2 s SPARKNaCl.Omultiply => 700.0 ms/19.1 s/28.6 s SPARKNaCl.Car.Nearlynormal_To_Normal => --/1.4 s/17.5 s diff --git a/test/spat.test-sparknacl.srfdca.template b/test/spat.test-sparknacl.srfdca.template index b9c2bd6..33effc0 100644 --- a/test/spat.test-sparknacl.srfdca.template +++ b/test/spat.test-sparknacl.srfdca.template @@ -1,31 +1,31 @@ random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) SPARKNaCl.ASR_16 => --/5.7 s/5.9 s `-VC_POSTCONDITION sparknacl.ads:355:35 => --/5.7 s/5.8 s `-Z3: 5.7 s (Unknown (unknown), 11650768 steps) diff --git a/test/spat.test-sparknacl.srfdcs.template b/test/spat.test-sparknacl.srfdcs.template index a9e932c..c6a25a6 100644 --- a/test/spat.test-sparknacl.srfdcs.template +++ b/test/spat.test-sparknacl.srfdcs.template @@ -1,32 +1,32 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) SPARKNaCl.Sign.Sign => --/57.6 s/489.2 s `-VC_OVERFLOW_CHECK sparknacl-sign.adb:890:36 => --/57.6 s/238.7 s `-CVC4: 57.6 s (Unknown (unknown), 505002 steps) diff --git a/test/spat.test-sparknacl.srfdct.template b/test/spat.test-sparknacl.srfdct.template index ee0d3c4..15ca175 100644 --- a/test/spat.test-sparknacl.srfdct.template +++ b/test/spat.test-sparknacl.srfdct.template @@ -1,32 +1,32 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) SPARKNaCl.Sign.Sign => --/57.6 s/489.2 s `-VC_OVERFLOW_CHECK sparknacl-sign.adb:890:36 => --/57.6 s/238.7 s `-CVC4: 57.6 s (Unknown (unknown), 505002 steps) diff --git a/test/spat.test-sparknacl.srjca.template b/test/spat.test-sparknacl.srjca.template index 02a6365..d379350 100644 --- a/test/spat.test-sparknacl.srjca.template +++ b/test/spat.test-sparknacl.srjca.template @@ -1,30 +1,30 @@ random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) SPARKNaCl.Car.Nearlynormal_To_Normal => --/1.4 s/17.5 s SPARKNaCl.Sign.Sign => --/57.6 s/489.2 s diff --git a/test/spat.test-sparknacl.srjcs.template b/test/spat.test-sparknacl.srjcs.template index d90efc5..f69d7bb 100644 --- a/test/spat.test-sparknacl.srjcs.template +++ b/test/spat.test-sparknacl.srjcs.template @@ -1,31 +1,31 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) SPARKNaCl.Sign.Sign => --/57.6 s/489.2 s SPARKNaCl.Car.Nearlynormal_To_Normal => --/1.4 s/17.5 s diff --git a/test/spat.test-sparknacl.srjct.template b/test/spat.test-sparknacl.srjct.template index d90efc5..f69d7bb 100644 --- a/test/spat.test-sparknacl.srjct.template +++ b/test/spat.test-sparknacl.srjct.template @@ -1,31 +1,31 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) SPARKNaCl.Sign.Sign => --/57.6 s/489.2 s SPARKNaCl.Car.Nearlynormal_To_Normal => --/1.4 s/17.5 s diff --git a/test/spat.test-sparknacl.srjdca.template b/test/spat.test-sparknacl.srjdca.template index 17c6fef..e0b06ea 100644 --- a/test/spat.test-sparknacl.srjdca.template +++ b/test/spat.test-sparknacl.srjdca.template @@ -1,31 +1,31 @@ random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) SPARKNaCl.Car.Nearlynormal_To_Normal => --/1.4 s/17.5 s `-VC_LOOP_INVARIANT_PRESERV sparknacl-car.adb:324:13 => --/1.4 s/1.9 s `-CVC4: 1.4 s (Unknown (unknown), 13011 steps) diff --git a/test/spat.test-sparknacl.srjdcs.template b/test/spat.test-sparknacl.srjdcs.template index 06d1579..869384a 100644 --- a/test/spat.test-sparknacl.srjdcs.template +++ b/test/spat.test-sparknacl.srjdcs.template @@ -1,32 +1,32 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) SPARKNaCl.Sign.Sign => --/57.6 s/489.2 s `-VC_OVERFLOW_CHECK sparknacl-sign.adb:890:36 => --/57.6 s/238.7 s `-CVC4: 51.6 s (Unknown (unknown), 505013 steps) diff --git a/test/spat.test-sparknacl.srjdct.template b/test/spat.test-sparknacl.srjdct.template index 06d1579..869384a 100644 --- a/test/spat.test-sparknacl.srjdct.template +++ b/test/spat.test-sparknacl.srjdct.template @@ -1,32 +1,32 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) SPARKNaCl.Sign.Sign => --/57.6 s/489.2 s `-VC_OVERFLOW_CHECK sparknacl-sign.adb:890:36 => --/57.6 s/238.7 s `-CVC4: 51.6 s (Unknown (unknown), 505013 steps) diff --git a/test/spat.test-sparknacl.sruca.template b/test/spat.test-sparknacl.sruca.template index 4f18a90..7511bfb 100644 --- a/test/spat.test-sparknacl.sruca.template +++ b/test/spat.test-sparknacl.sruca.template @@ -1,31 +1,31 @@ random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) SPARKNaCl.ASR_16 => --/5.7 s/5.9 s SPARKNaCl.ASR_4 => --/1.2 s/1.4 s SPARKNaCl.ASR_8 => --/3.3 s/3.5 s diff --git a/test/spat.test-sparknacl.srucs.template b/test/spat.test-sparknacl.srucs.template index daf02cb..1aef2a5 100644 --- a/test/spat.test-sparknacl.srucs.template +++ b/test/spat.test-sparknacl.srucs.template @@ -1,32 +1,32 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) SPARKNaCl.Sign.Sign => --/57.6 s/489.2 s SPARKNaCl.Car.Nearlynormal_To_Normal => --/1.4 s/17.5 s SPARKNaCl.ASR_16 => --/5.7 s/5.9 s diff --git a/test/spat.test-sparknacl.sruct.template b/test/spat.test-sparknacl.sruct.template index daf02cb..1aef2a5 100644 --- a/test/spat.test-sparknacl.sruct.template +++ b/test/spat.test-sparknacl.sruct.template @@ -1,32 +1,32 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) SPARKNaCl.Sign.Sign => --/57.6 s/489.2 s SPARKNaCl.Car.Nearlynormal_To_Normal => --/1.4 s/17.5 s SPARKNaCl.ASR_16 => --/5.7 s/5.9 s diff --git a/test/spat.test-sparknacl.srudca.template b/test/spat.test-sparknacl.srudca.template index 1dc551c..c218f78 100644 --- a/test/spat.test-sparknacl.srudca.template +++ b/test/spat.test-sparknacl.srudca.template @@ -1,31 +1,31 @@ random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) SPARKNaCl.ASR_16 => --/5.7 s/5.9 s `-VC_POSTCONDITION sparknacl.ads:355:35 => --/5.7 s/5.8 s `-Z3: 5.7 s (Unknown (unknown), 11650768 steps) diff --git a/test/spat.test-sparknacl.srudcs.template b/test/spat.test-sparknacl.srudcs.template index e869dc0..5c0bd83 100644 --- a/test/spat.test-sparknacl.srudcs.template +++ b/test/spat.test-sparknacl.srudcs.template @@ -1,32 +1,32 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) SPARKNaCl.Sign.Sign => --/57.6 s/489.2 s `-VC_OVERFLOW_CHECK sparknacl-sign.adb:890:36 => --/57.6 s/238.7 s `-CVC4: 51.6 s (Unknown (unknown), 505013 steps) diff --git a/test/spat.test-sparknacl.srudct.template b/test/spat.test-sparknacl.srudct.template index e869dc0..5c0bd83 100644 --- a/test/spat.test-sparknacl.srudct.template +++ b/test/spat.test-sparknacl.srudct.template @@ -1,32 +1,32 @@ Warning: Sorting files by success time not implemented yet, falling back to maximum time. sparknacl-sign.spark => (Flow => 253.6 ms, - Proof => 764.5 s) + Proof => 9.2 s/57.6 s/764.5 s) sparknacl-car.spark => (Flow => 86.1 ms, - Proof => 59.0 s) + Proof => 950.0 ms/1.4 s/59.0 s) sparknacl.spark => (Flow => 164.3 ms, - Proof => 57.3 s) + Proof => 700.0 ms/19.1 s/57.3 s) sparknacl-hashing.spark => (Flow => 70.5 ms, - Proof => 43.8 s) + Proof => 500.0 ms/500.0 ms/43.8 s) sparknacl-scalar.spark => (Flow => 62.5 ms, - Proof => 22.1 s) + Proof => 550.0 ms/550.0 ms/22.1 s) sparknacl-stream.spark => (Flow => 72.6 ms, - Proof => 21.2 s) + Proof => 210.0 ms/210.0 ms/21.2 s) sparknacl-utils.spark => (Flow => 49.8 ms, - Proof => 17.4 s) + Proof => 900.0 ms/900.0 ms/17.4 s) sparknacl-secretbox.spark => (Flow => 7.6 ms, - Proof => 10.3 s) + Proof => 270.0 ms/270.0 ms/10.3 s) sparknacl-core.spark => (Flow => 351.9 ms, - Proof => 8.9 s) + Proof => 120.0 ms/120.0 ms/8.9 s) sparknacl-mac.spark => (Flow => 58.0 ms, - Proof => 8.0 s) + Proof => 340.0 ms/340.0 ms/8.0 s) sparknacl-cryptobox.spark => (Flow => 69.2 ms, - Proof => 4.9 s) + Proof => 70.0 ms/70.0 ms/4.9 s) sparknacl-pdebug.spark => (Flow => 2.2 ms, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) random.spark => (Flow => 517.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) sparknacl-debug.spark => (Flow => 469.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) SPARKNaCl.Sign.Sign => --/57.6 s/489.2 s `-VC_OVERFLOW_CHECK sparknacl-sign.adb:890:36 => --/57.6 s/238.7 s `-CVC4: 51.6 s (Unknown (unknown), 505013 steps) From 987ad6b6f76f5b99a50f773c2a19f42b99c559af Mon Sep 17 00:00:00 2001 From: "Vinzent \"Jellix\" Saranen" Date: Thu, 18 Jun 2020 21:04:23 +0200 Subject: [PATCH 4/4] * Updated documentation. --- README.md | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index 9fb6343..380e52d 100644 --- a/README.md +++ b/README.md @@ -142,15 +142,15 @@ Typical output would look like this: ``` saatana-crypto.spark => (Flow => 9.0 ms, - Proof => 6.8 s) + Proof => 80.0 ms/80.0 ms/6.8 s) saatana-crypto-phelix.spark => (Flow => 206.5 ms, - Proof => 568.7 s) + Proof => 174.3 s/206.4 s/568.7 s) saatana.spark => (Flow => 464.0 µs, - Proof => 0.0 s) + Proof => 0.0 s/0.0 s/0.0 s) saatana-crypto-lemmas.spark => (Flow => 2.1 ms, - Proof => 2.2 s) + Proof => 210.0 ms/210.0 ms/2.2 s) test_phelix_api.spark => (Flow => 14.4 ms, - Proof => 23.1 s) + Proof => 240.0 ms/240.0 ms/23.1 s) ``` You can use the `--sort-by` option with `--summary`, either for an alphabetical @@ -160,6 +160,8 @@ so files with the most time needed by the provers come first). The option warning that what you requested has not been implemented yet. By default, no particular order is imposed on the output. +For the meaning of the three timings after `Proof =>`, please see below. + *Note* that the `--details` option has no effect on the output here, this option is designed to work with the `--report-mode` option only.