Pipe through carry_add function

[bMacSwigg]

carry_add has tighter bounds on the results than the basic add function. The source already exists in PushButtonSynthesis. This defines & specs the function in Field.v, proves the correctness of the existing source relative to that spec, and then derives the Field25519 and Field1305 versions.

A later PR will replace the mul-by-2 in #1622 with carry_add instead.

[bMacSwigg]

Hm. Tried to reproduce the failed CI checks locally by running make src/Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo. Hit a different error:

File "./src/Bedrock/Field/Common/Util.v", line 1038, characters 6-37:
Error: Expected a single focused goal but 3 goals are focused.

which I could reproduce on my main branch without these changes (see issue #1636).

[JasonGross]

Hm. Tried to reproduce the failed CI checks locally by running make src/Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo. Hit a different error:

Try git submodule update --recursive?

[JasonGross]

Why "dontuse"?

[andres-erbsen]

I think this is because there isn't a particularly satisfying implementation of this function in montgomery domain. Having it be an alias for add would be fine, though. (We could consider calling this function "add", and the other one "add_limbwise" or "unreduced_add" or "unsafe_add"...)

[bMacSwigg]

Correct, there's no existing implementation; and in fact, the existing add function in Montgomery already guarantees tight_bounds, so it doesn't look like there would be any benefit to the carry_add function.

However, as an unfortunate consequence of the way FieldParameters is defined right now, any function in the spec must be defined (or "defined" by just providing an arbitrary string) everywhere that uses the spec, even if it's not needed.

(See for example fe1305_scmul1_dontuse in RupicolaCrypto/Low.v.)

[bMacSwigg]

What I said about Montgomery add guaranteeing tight_bounds isn't really accurate; I was misremembering. But it guarantees montgomery_domain_bounds, i.e. that the result is in the Montgomery domain, which I think is analogous?

fiat-crypto/src/PushButtonSynthesis/WordByWordMontgomery.v

Lines 319 to 326 in 63a6ba4

	Definition add
	:= Pipeline.BoundsPipeline
	true (* subst01 *)
	possible_values
	(reified_add_gen
	@ GallinaReify.Reify (machine_wordsize:Z) @ GallinaReify.Reify n @ GallinaReify.Reify m)
	(Some montgomery_domain_bounds, (Some montgomery_domain_bounds, tt))
	(Some montgomery_domain_bounds).

[bMacSwigg]

Hm. Tried to reproduce the failed CI checks locally by running make src/Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo. Hit a different error:

Try git submodule update --recursive?

That worked :) I was able to reproduce the failed CI and pushed a couple fixes. Re-running CI now 🤞