Currently we have three binaries, and the arguments are slightly different:
./src/ExtractionOCaml/word_by_word_montgomery curve_description m machine_wordsize [function_to_synthesize*]
curve_description A string which will be prefixed to every function name generated
m The prime (e.g., '2^434 - (2^216*3^137 - 1)')
machine_wordsize The machine bitwidth (e.g., 32 or 64)
function_to_synthesize A list of functions that should be synthesized. If no functions are given, all functions are synthesized.
Valid options are mul, square, add, sub, opp, from_montgomery, nonzero, selectznz, to_bytes, from_bytes
./src/ExtractionOCaml/unsaturated_solinas curve_description n s c machine_wordsize [function_to_synthesize*]
curve_description A string which will be prefixed to every function name generated
n The number of limbs
s The largest component of the prime (e.g., '2^255' in '2^255-19')
c The semi-colon separated list of taps, each of which is specified as weight,value (no parentheses) (e.g., '2^96,1;1,-1' in '2^224 - 2^96 + 1')
machine_wordsize The machine bitwidth (e.g., 32 or 64)
function_to_synthesize A list of functions that should be synthesized. If no functions are given, all functions are synthesized.
Valid options are carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, or 'carry_scmul' followed by a decimal literal
./src/ExtractionOCaml/saturated_solinas curve_description s c machine_wordsize [function_to_synthesize*]
curve_description A string which will be prefixed to every function name generated
s The largest component of the prime (e.g., '2^255' in '2^255-19')
c The semi-colon separated list of taps, each of which is specified as weight,value (no parentheses) (e.g., '2^96,1;1,-1' in '2^224 - 2^96 + 1')
machine_wordsize The machine bitwidth (e.g., 32 or 64)
function_to_synthesize A list of functions that should be synthesized. If no functions are given, all functions are synthesized.
Valid options are mul
Each of these takes a different set of arguments. We also have three different PRs (#390, #391, #393) which update the bounds heuristics and/or command line arguments, in sometimes incompatible ways.
Things we might want to do:
Accept some options from some of the PRs as optional command-line arguments, somehow? I have a version of a thing that mostly satisfies OCaml's Arg module interface, which I wrote when I was considering doing optional command line arguments. But then we should decide on the right format / names / etc to use, and how to fill in defaults in the right way.
Combine the various binaries, or make a synthsize program whose code is something like
#!/usr/bin/env bash
if [ $# -eq 0 ]; then
cd ./src/ExtractionOCaml
OPTIONS="$(find * -mindepth 0 -executable -type f)"
if [ -z "$OPTIONS" ]; then
echo "ERROR: No executables found. Did you forget to 'make standalone'?"
else
echo "ERROR: Expected an argument. One of:"
echo "$OPTIONS"
fi
exit 1
fi
PROG="$1"
shift
"./src/ExtractionOCaml/$PROG" "$@"
so that the user can pass the type of synthesis as the first command-line option. Or, if the choice is heuristic, actually combine the binaries and do the heuristic in Coq.
- Parse the TAPs from the prime number. This should not be too hard, given that we have `String.replace`, `String.split`, `String.concat`. In fact, here is a fragment of code that can be dropped in `CLI.v` to parse the TAPs:
Above the section open:
```coq
Require Import Coq.Sorting.Mergesort.
Require Import Coq.MSets.MSetPositive.
Require Import Crypto.Util.ListUtil.
Require Import Crypto.Util.Prod.
Require Import Crypto.Util.OptionList.
Module TAPOrder <: Orders.TotalLeBool.
Local Coercion is_true : bool >-> Sortclass.
Definition t := (Z * Z)%type.
Definition leb (x y : t) := Z.leb (snd x) (snd y).
Infix "<=?" := leb.
Theorem leb_total : forall a1 a2, a1 <=? a2 \/ a2 <=? a1.
Proof.
intros; cbv [is_true leb]; rewrite !Z.leb_le; omega.
Qed.
End TAPOrder.
Module TAPSort := Sort TAPOrder.
In the section:
(** Translated from https://github.com/mit-plv/fiat-crypto/blob/c60b1d2556a72c37f4bc7444204e9ddc0791ce4f/generate_parameters.py#L89-L113 *)
(** given a string representing one term or "tap" in a prime,
returns a pair of integers representing the weight and
coefficient of that tap
- "2 ^ y" -> [1, y]
- "x * 2 ^ y" -> [x, y]
- "x * y" -> [x*y,0]
- "x" -> [x,0] *)
Definition parse_term (t : string) : option (Z * Z)
:= (if negb (String.contains 0 "*" t) && negb (String.contains 0 "^" t)
then (t <- parseZ_arith t;
Some (t, 1))
else ab <- if String.contains 0 "*" t
then
match String.split "*" t with
| [a; b]
=> a <- parse_Z a;
Some (a, b)
| [a1; a2; b] (* this occurs when e.g. [w - x * y] has been turned into [w + -1 * x * y] *)
=> a1 <- parse_Z a1;
a2 <- parse_Z a2;
Some (a1 * a2, b)
| _ => None
end
else
Some (1, t);
let '(a, b) := ab in
if negb (String.contains 0 "^" b)
then
b <- parse_Z b;
Some (a * b, 1)
else
match String.split "^" b with
| [b; e]
=> b <- parse_Z b;
e <- parse_Z e;
if (b =? 2)%Z (* should we drop this check? *)
then Some (a, 2^e)
else None
| _ => None
end)%option.
(** Translated from https://github.com/mit-plv/fiat-crypto/blob/c60b1d2556a72c37f4bc7444204e9ddc0791ce4f/generate_parameters.py#L116-L121 *)
(** expects prime to be a string and expressed as sum/difference of
products of two with small coefficients (e.g. '2^448 - 2^224 -
1', '2^255 - 19') *)
Definition parse_prime (prime : string) : option (list (Z * Z))
:= let prime := String.replace "+-2^" "+-1*2^" (String.replace " " "" (String.replace "-" "+ -" prime)) in
let terms := String.split "+" prime in
(terms <-- List.map parse_term terms;
Some terms).
(** Translated from https://github.com/mit-plv/fiat-crypto/blob/c60b1d2556a72c37f4bc7444204e9ddc0791ce4f/generate_parameters.py#L123-L140 *)
(** check that the parsed prime makes sense *)
Definition sanity_check (p : list (Z * Z)) : bool
:= fold_right
andb
true
[(* are there at least 2 terms? *)
(1 <? List.length p)%nat
; (* are terms are in order (most to least significant)? *)
list_beq _ (prod_beq _ _ Z.eqb Z.eqb) p (List.rev (TAPSort.sort p))
; (* does the least significant term have weight 2^0=1? *)
(snd (List.hd (0, 1) (List.rev p)) =? 1)%Z
; (* are all the exponents non-negative and the coefficients nonzero? *)
forallb (fun t => negb (fst t =? 0) && (snd t >=? 1))%Z p
; (* is second-most-significant term negative? *)
(fst (nth_default (0, 1) p 1) <? 0)%Z
; (* are any exponents repeated? *)
(PositiveSet.cardinal
(List.fold_right
PositiveSet.add
PositiveSet.empty
(List.map (fun t => Z.to_pos (1 + snd t (* 1+ so that 1 and 0 get mapped to different things *))) p))
=? List.length p)%nat].
I have tested it on a couple of the primes in the list, and it seems to work. We could even check that arithmetic-parsing the prime (which is a bit simpler than this, I think, and more robust) gives the same value as evaluating the taps.
Currently we have three binaries, and the arguments are slightly different:
Each of these takes a different set of arguments. We also have three different PRs (#390, #391, #393) which update the bounds heuristics and/or command line arguments, in sometimes incompatible ways.
Things we might want to do:
synthsize
program whose code is something likeif [ $# -eq 0 ]; then cd ./src/ExtractionOCaml OPTIONS="$(find * -mindepth 0 -executable -type f)" if [ -z "$OPTIONS" ]; then echo "ERROR: No executables found. Did you forget to 'make standalone'?" else echo "ERROR: Expected an argument. One of:" echo "$OPTIONS" fi exit 1 fi
PROG="$1" shift
"./src/ExtractionOCaml/$PROG" "$@"
In the section:
I have tested it on a couple of the primes in the list, and it seems to work. We could even check that arithmetic-parsing the prime (which is a bit simpler than this, I think, and more robust) gives the same value as evaluating the taps.