Make fe magnitude implied statically

real-or-random commented at 3:00 pm on October 28, 2021: contributor

See the discussion starting here: #943 (comment)

real-or-random cross-referenced this on Oct 28, 2021 from issue VERIFY_CHECK precondition for secp256k1_fe_set_int. by roconnor-blockstream

roconnor-blockstream commented at 3:51 pm on October 28, 2021: contributor

To be clear, all the instances of magnitude are currently statically implied because all those “variables” that are dynamic are currently only ever passed integer literal values.

peterdettman commented at 2:37 pm on October 30, 2021: contributor

@roconnor-blockstream Surely not, e.g. what about _fe_cmov?

roconnor-blockstream commented at 2:41 pm on October 30, 2021: contributor

I wasn’t aware of that one. (I’m less familiar with the non-verification related code.)

Make sense to patch that case by always setting the magnitude to the max of the two values?

peterdettman commented at 2:52 pm on October 30, 2021: contributor

Yes, which was already done, then patched out, so this time with more comments I think!

real-or-random commented at 12:43 pm on November 3, 2021: contributor

@peterdettman Can you elaborate a little bit more on the reasoning behind this suggestion?

I fully agree it’s conceptually nicer. But as long as we don’t have automated checks that prove that the magnitude is always low enough, does it really matter?

roconnor-blockstream commented at 1:57 pm on November 3, 2021: contributor

The whole point of the magnitude field is to have a check that the tested code paths would not overflow even if different values were used. It is a poor man’s abstract interpretation.

But when we, say, set the magnitude of the output of cmov, based on the flag value, and the value of that flag value is dependent on the specific initial value we are testing, then our “abstract interpretation” ends up being limited to only those value that would produce the same flag value at that call site.

I respect that our poor man’s abstract interpretation is imperfect. There are places were we explicitly branch on data (especially in the _var functions). But we can at least strive to make our abstraction as abstract as reasonably possible.

(For illustration: the opposite course of action would be to make the magnitude based more and more on concrete values, but there is no point in doing that. We already have a prefect measure of the a concrete magnitude: using the actual value itself!).

peterdettman commented at 1:58 pm on November 3, 2021: contributor

I thought of the magnitude verification AS the automated checks. It’s inherently worst-case, basically a static bounds check. That plus code coverage of all branches (and careful analysis of the very few loops) means there’s no overflows in the field arithmetic. Without that property you need to be sure you have test cases that exercise every code path at the maximum possible magnitude, which is just a harder-to-prove/understand version of the same thing.

peterdettman commented at 2:02 pm on November 3, 2021: contributor

We already have a prefect measure of the a concrete magnitude: using the actual value itself!

Bingo.

real-or-random commented at 2:25 pm on November 3, 2021: contributor

I thought of the magnitude verification AS the automated checks. It’s inherently worst-case, basically a static bounds check.

Oh sure, I missed this part!

(My thinking was: “it’s only dynamic analysis anyway”. But if the values are statically determined, then that’s indeed all we need…)

peterdettman commented at 2:42 pm on November 3, 2021: contributor

It sure would be nice to have a way of restricting a function argument to be a literal. Both to allow the obvious implementation for _mul_int, but also to restrict _fe_negate to specifying a literal for its ’m’ (magnitude) argument.

roconnor-blockstream commented at 3:52 pm on November 3, 2021: contributor

I’m moderately sure there is some horrible way to enforce this with macros. The specific solution I came across uses compound literals, but I suspect there are C89 ways too.

But I’m not sure that we really want to go down the horrible-macro route.

Edit: Maybe just casting through a one dimensional array somehow I’m not sure.

0#define foo(i) foo_do_not_call_directly((int[1+0*i])(int)(i)[0])

real-or-random commented at 3:59 pm on November 3, 2021: contributor

@roconnor-blockstream What about just appending u in the macro? That’s valid only for literals, and magnitude is anyway not negative.

roconnor-blockstream commented at 4:00 pm on November 3, 2021: contributor

appending u also works for the expression i + 1.

real-or-random commented at 4:06 pm on November 3, 2021: contributor

Oh indeed.

What about this?

0#define foo(i) foo_do_not_call_directly(sizeof(char[i]))?

edit: that doesn’t give an error in GCC. It just gives a warning, and you need -pedantic to trigger the warning (variable-length arrays are a GCC extension)

Here’s a better one:

0#define foo(i) do { switch (i) {  case i: foo_do_not_call(i) }} while (0)

(suggested by @roconnor-blockstream again)

Another way of doing it is to define a force_const macro like:

0#define force_const(i) (sizeof(struct{int a:i;}), i)

That only works up to the bitwidth of int, which is at least 16, so that’s enough for this particular purpose…

https://port70.net/~nsz/c/c89/c89-draft.html#45 is pretty useful here.

There’s also in https://gcc.gnu.org/onlinedocs/gcc/Other-Builtins.html#index-_005f_005fbuiltin_005fconstant_005fp in gcc.

real-or-random commented at 4:09 pm on November 3, 2021: contributor

An entirely different way to do this is the approach in #833.

peterdettman commented at 4:49 am on November 4, 2021: contributor

An entirely different way to do this is the approach in #833.

Does that allow something generic like requiring that for any function parameter named literal_* (just for example), at all call sites the argument must be an actual literal (after pre-processor stage, say)?

(Maybe the restriction is really to compile-time constant or something else more complicated, but we could just look at literals for the moment.)

real-or-random commented at 5:34 pm on November 4, 2021: contributor

An entirely different way to do this is the approach in #833.

Does that allow something generic like requiring that for any function parameter named literal_* (just for example), at all call sites the argument must be an actual literal (after pre-processor stage, say)?

I haven’t tried but I’m pretty sure that this is possible. Coupling it to the parameter name is a pretty nice idea!

real-or-random cross-referenced this on Dec 23, 2021 from issue Add _fe_half and use in _gej_add_ge and _gej_double by peterdettman

real-or-random cross-referenced this on Jan 4, 2022 from issue Separate magnitude/normalization/... checking/propagation from implementations by sipa

real-or-random cross-referenced this on Jan 5, 2022 from issue Document field functions assumptions and validate it using magnitude and `fe_verify` checks by siv2r

sipa cross-referenced this on Jan 29, 2022 from issue Abstract out and merge all the magnitude/normalized logic by sipa

sipa commented at 5:21 pm on February 1, 2022: contributor

So I think #1066 makes it very clear in what ways norm/mag are not compile-time known, as it puts all propagation logic for these fields together. I find:

fe_cmov (easily fixed: take the max)
set_b32 (which only produces a normalized result if the input is < p). If we want to fix this, I think we should split it into 2 functions:
- One that always sets normalized=0.
- One that always sets normalized=1, but in case the input is >= p, it returns an error value and resets the field value to 0 or so.
fe_mul_int’s integer argument (fixed by forcing it to be a constant)
fe_negate’s magnitude (fixed by forcing it to be a constant)
All the ways in which the code flow depends on values, in vartime algorithms, of course.

real-or-random cross-referenced this on Mar 15, 2022 from issue This may be superior to clang-query by real-or-random

real-or-random cross-referenced this on Mar 2, 2023 from issue Add secp256k1_fe_add_int function by sipa

real-or-random cross-referenced this on May 8, 2023 from issue Add simple static checker based on clang-query by real-or-random

sipa referenced this in commit c63ec88ebf on May 11, 2023

sipa cross-referenced this on May 15, 2023 from issue Make fe_cmov take max of magnitudes by sipa

sipa commented at 1:41 pm on May 15, 2023: contributor

The secp256k1_fe_set_f32 runtime dependency has been addressed through #1207.

See #1317 for the secp256k1_fe_cmov runtime dependency.

real-or-random referenced this in commit e9e4526a4e on May 19, 2023

real-or-random referenced this in commit be8ff3a02a on Jun 13, 2023

real-or-random cross-referenced this on Jun 13, 2023 from issue field: Static-assert that int args affecting magnitude are constant by real-or-random

real-or-random referenced this in commit 3aef6ab8e1 on Jun 27, 2023

real-or-random commented at 1:37 pm on July 11, 2023: contributor

One instance we have overlooked is fe_set_int. I missed that in #1345, but I think it should just set the magnitude to 1 always. We have fe_clear for setting to 0. (That one should probably be split in clear for nuking the memory, and fe_set_zero if you really want 0 with magnitude 0.)

real-or-random added the label assurance on Jul 11, 2023

real-or-random added the label refactor/smell on Jul 11, 2023

Make fe magnitude implied statically #1001