default to magnitude 8->1 in Dettman multiplication

[andres-erbsen]

See bitcoin-core/secp256k1#1319 (review) and https://github.com/bitcoin-core/secp256k1/blob/26392da2fb7153addae0bd604495eb96f995d76c/src/field_impl.h#L329-L334

[OwenConoly]

Looks good to me. I didn’t realize the output bounds could be set so tight.

I think it would be better to write input_magnitude := 8 * (Option.value inbounds_multiplier 1) to be consistent with the documentation here:

fiat-crypto/src/CLI.v

Lines 442 to 446 in 60efd19

	Definition default_inbounds_multiplier := 1.
	Definition inbounds_multiplier_spec : named_argT
	:= ([Arg.long_key "inbounds-multiplier"],
	Arg.String,
	["The (improper) fraction by which the bounds of each input limb are scaled (default: " ++ show default_inbounds_multiplier ++ ")"]).

[andres-erbsen]

Hmm, I think what we actually want is to change default_inbounds_multiplier for this implementation only. Do you see a satisfying way to do this?

[JasonGross]

default_inbounds_multiplier should not live in CLI.v but in whichever file does Option.value (if this is multiple files, we should make a new Heuristics file), to guarantee that the doc stays in sync.

Then just make an alternate version of the spec that uses the different default, and stick that in

fiat-crypto/src/CLI.v

Line 1197 in 60efd19

{| Arg.named_args := [inbounds_multiplier_spec]

[andres-erbsen]

Two files do Option.value. But perhaps they shouldn't share the option? I am not sure I understand the overall architecture here, or your suggestion wrt Heuristics.

[JasonGross]

Two files do Option.value. But perhaps they shouldn't share the option?

I think insofar as they have different default values, this is an indication that they are maybe doing at least slightly different things conceptually? I'm not sure though.

I am not sure I understand the overall architecture here, or your suggestion wrt Heuristics.

My suggestion is that CLI should be describing default values to the user, and providing the PushButtonSynthesis / BoundsPipeline levels with the values the user provides when invoking them. Whether CLI fills in defaults or passes along option to the lower levels is immaterial, but I think the default values should be defined in some constant by some level below CLI, and CLI should display the default to the user by stringifying this constant. I was suggesting Heuristics for the default value location, but it seems fine to instead define the default next to the typeclass definition, or in each PushButtonSynthesis file that uses the option, or elsewhere. But the default value should not be defined in CLI.

I guess if you define a constant for the default value in each PushButtonSynthesis file, you could parametrize the spec doc over the default value, and then pass it in when declaring the parameter for each pipeline.