From 9b9adfa6437439cf133da6f062b0b6050a691cdf Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 24 Jan 2019 15:35:49 -0500 Subject: Also display the carry chain in a comment --- curve25519_32.c | 3 +++ curve25519_64.c | 3 +++ p448_solinas_64.c | 3 +++ p521_32.c | 3 +++ p521_64.c | 3 +++ src/CLI.v | 17 ++++++++++------- src/PushButtonSynthesis/Primitives.v | 7 ++++--- src/PushButtonSynthesis/SaturatedSolinas.v | 4 ++-- src/PushButtonSynthesis/UnsaturatedSolinas.v | 6 +++++- src/PushButtonSynthesis/WordByWordMontgomery.v | 4 ++-- 10 files changed, 38 insertions(+), 15 deletions(-) diff --git a/curve25519_32.c b/curve25519_32.c index 820a5c9bb..83453d82b 100644 --- a/curve25519_32.c +++ b/curve25519_32.c @@ -6,6 +6,9 @@ /* c = [(1, 19)] (from "1,19") */ /* machine_wordsize = 32 (from "32") */ +/* Computed values: */ +/* carry_chain = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 0, 1] */ + #include typedef unsigned char fiat_25519_uint1; typedef signed char fiat_25519_int1; diff --git a/curve25519_64.c b/curve25519_64.c index 23bf361d8..59beaf93a 100644 --- a/curve25519_64.c +++ b/curve25519_64.c @@ -6,6 +6,9 @@ /* c = [(1, 19)] (from "1,19") */ /* machine_wordsize = 64 (from "64") */ +/* Computed values: */ +/* carry_chain = [0, 1, 2, 3, 4, 0, 1] */ + #include typedef unsigned char fiat_25519_uint1; typedef signed char fiat_25519_int1; diff --git a/p448_solinas_64.c b/p448_solinas_64.c index af57a7611..37cb13e10 100644 --- a/p448_solinas_64.c +++ b/p448_solinas_64.c @@ -6,6 +6,9 @@ /* c = [(26959946667150639794667015087019630673637144422540572481103610249216, 1), (1, 1)] (from "2^224,1;1,1") */ /* machine_wordsize = 64 (from "64") */ +/* Computed values: */ +/* carry_chain = [3, 7, 4, 0, 5, 1, 6, 2, 7, 3, 4, 0] */ + #include typedef unsigned char fiat_p448_uint1; typedef signed char fiat_p448_int1; diff --git a/p521_32.c b/p521_32.c index 7d929b584..6bc3ae0b4 100644 --- a/p521_32.c +++ b/p521_32.c @@ -6,6 +6,9 @@ /* c = [(1, 1)] (from "1,1") */ /* machine_wordsize = 32 (from "32") */ +/* Computed values: */ +/* carry_chain = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 0, 1] */ + #include typedef unsigned char fiat_p521_uint1; typedef signed char fiat_p521_int1; diff --git a/p521_64.c b/p521_64.c index 503368e0d..971aee4c3 100644 --- a/p521_64.c +++ b/p521_64.c @@ -6,6 +6,9 @@ /* c = [(1, 1)] (from "1,1") */ /* machine_wordsize = 64 (from "64") */ +/* Computed values: */ +/* carry_chain = [0, 1, 2, 3, 4, 5, 6, 7, 8, 0, 1] */ + #include typedef unsigned char fiat_p521_uint1; typedef signed char fiat_p521_int1; diff --git a/src/CLI.v b/src/CLI.v index 32cc3fd1e..41a705cc2 100644 --- a/src/CLI.v +++ b/src/CLI.v @@ -222,7 +222,7 @@ Module ForExtraction. ; ("c", c, parse_c c:Dyn)] with | inr errs => inr errs | inl (n, machine_wordsize, s, c) - => let '(res, types_used) + => let '(extra_comment_header, res, types_used) := UnsaturatedSolinas.Synthesize n s c machine_wordsize prefix requests in let header := ((["/* Autogenerated */"; @@ -233,8 +233,9 @@ Module ForExtraction. "/* c = " ++ show false c ++ " (from """ ++ str_c ++ """) */"; "/* machine_wordsize = " ++ show false machine_wordsize ++ " (from """ ++ str_machine_wordsize ++ """) */"; ""]%string) - ++ ToString.C.String.typedef_header prefix types_used - ++ [""])%list in + ++ extra_comment_header + ++ ToString.C.String.typedef_header prefix types_used + ++ [""])%list in inl ([("check_args" ++ NewLine ++ String.concat NewLine header, UnsaturatedSolinas.check_args @@ -323,7 +324,7 @@ Module ForExtraction. ("m", m, parse_m m:Dyn)] with | inr errs => inr errs | inl (machine_wordsize, m) - => let '(res, types_used) + => let '(extra_comment_header, res, types_used) := WordByWordMontgomery.Synthesize m machine_wordsize prefix requests in let header := ((["/* Autogenerated */"; @@ -339,8 +340,9 @@ Module ForExtraction. "/* All functions also ensure that these two properties are true of */"; "/* return values. */"; ""]%string) - ++ ToString.C.String.typedef_header prefix types_used - ++ [""])%list in + ++ extra_comment_header + ++ ToString.C.String.typedef_header prefix types_used + ++ [""])%list in inl ([("check_args" ++ NewLine ++ String.concat NewLine header, WordByWordMontgomery.check_args @@ -424,7 +426,7 @@ Module ForExtraction. ; ("c", c, parse_c c:Dyn)] with | inr errs => inr errs | inl (machine_wordsize, s, c) - => let '(res, types_used) + => let '(extra_comment_header, res, types_used) := SaturatedSolinas.Synthesize s c machine_wordsize prefix requests in let header := ((["/* Autogenerated */"; @@ -434,6 +436,7 @@ Module ForExtraction. "/* c = " ++ show false c ++ " (from """ ++ str_c ++ """) */"; "/* machine_wordsize = " ++ show false machine_wordsize ++ " (from """ ++ str_machine_wordsize ++ """) */"; ""]%string) + ++ extra_comment_header ++ ToString.C.String.typedef_header prefix types_used ++ [""])%list in inl diff --git a/src/PushButtonSynthesis/Primitives.v b/src/PushButtonSynthesis/Primitives.v index 4afa64433..f36f4cb9c 100644 --- a/src/PushButtonSynthesis/Primitives.v +++ b/src/PushButtonSynthesis/Primitives.v @@ -369,15 +369,16 @@ Section __. (** Note: If you change the name or type signature of this function, you will need to update the code in CLI.v *) - Definition Synthesize (function_name_prefix : string) (requests : list string) - : list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *) + Definition Synthesize (comment_header : list string) (function_name_prefix : string) (requests : list string) + : list string (* comment header *) * list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *) := let ls := match requests with | nil => List.map (fun '(_, sr) => sr function_name_prefix) known_functions | requests => List.map (synthesize_of_name function_name_prefix) requests end in let infos := aggregate_infos ls in let '(extra_ls, extra_bit_widths) := extra_synthesis function_name_prefix infos in - (extra_ls ++ List.map (fun '(name, res) => (name, (res <- res; Success (fst res))%error)) ls, + (comment_header, + extra_ls ++ List.map (fun '(name, res) => (name, (res <- res; Success (fst res))%error)) ls, PositiveSet.union extra_bit_widths (ToString.C.bitwidths_used infos)). End for_stringification. End __. diff --git a/src/PushButtonSynthesis/SaturatedSolinas.v b/src/PushButtonSynthesis/SaturatedSolinas.v index bcb93c4a1..334c2a475 100644 --- a/src/PushButtonSynthesis/SaturatedSolinas.v +++ b/src/PushButtonSynthesis/SaturatedSolinas.v @@ -176,9 +176,9 @@ Section __. (** Note: If you change the name or type signature of this function, you will need to update the code in CLI.v *) Definition Synthesize (function_name_prefix : string) (requests : list string) - : list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *) + : list string * list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *) := Primitives.Synthesize machine_wordsize valid_names known_functions (fun _ => nil) - function_name_prefix requests. + [] function_name_prefix requests. End for_stringification. End __. diff --git a/src/PushButtonSynthesis/UnsaturatedSolinas.v b/src/PushButtonSynthesis/UnsaturatedSolinas.v index cd70771d2..8923aa10e 100644 --- a/src/PushButtonSynthesis/UnsaturatedSolinas.v +++ b/src/PushButtonSynthesis/UnsaturatedSolinas.v @@ -13,6 +13,7 @@ Require Import Crypto.Util.ListUtil.FoldBool. Require Import Crypto.Util.Strings.Decimal. Require Import Crypto.Util.Strings.Equality. Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.Strings.Show. Require Import Crypto.Util.ZUtil.Definitions. Require Import Crypto.Util.ZUtil.Zselect. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. @@ -623,9 +624,12 @@ else: (** Note: If you change the name or type signature of this function, you will need to update the code in CLI.v *) Definition Synthesize (function_name_prefix : string) (requests : list string) - : list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *) + : list string * list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *) := Primitives.Synthesize machine_wordsize valid_names known_functions (extra_special_synthesis function_name_prefix) + ["/* Computed values: */"; + "/* carry_chain = " ++ show false idxs ++ " */"; + ""]%string function_name_prefix requests. End for_stringification. End __. diff --git a/src/PushButtonSynthesis/WordByWordMontgomery.v b/src/PushButtonSynthesis/WordByWordMontgomery.v index 3b28329c5..a97c829e2 100644 --- a/src/PushButtonSynthesis/WordByWordMontgomery.v +++ b/src/PushButtonSynthesis/WordByWordMontgomery.v @@ -754,9 +754,9 @@ Section __. (** Note: If you change the name or type signature of this function, you will need to update the code in CLI.v *) Definition Synthesize (function_name_prefix : string) (requests : list string) - : list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *) + : list string * list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *) := Primitives.Synthesize machine_wordsize valid_names known_functions (fun _ => nil) - function_name_prefix requests. + [] function_name_prefix requests. End for_stringification. End __. -- cgit v1.2.3