Perform bool to uint8_t conversion at the notation level

[davidben]

For @JasonGross, by way of a discussion with me and @andres-erbsen. Any mistakes in the transcription are mine.

The synthesized code works with one-bit integers a lot for carries and the like. This is nominally a bool, but C didn't get support for this until C99, so instead things got rounded up to uint8_t at some point down the line. This was done by way of making TWord 3 a uint8_t while leaving TWord 0 a bool, then somewhere telling the bounds-checker to round to TWord 3 instead of TWord 0.

This has two problems. First, the unused TWord 0 notations are not actually correct. Adding two bools together is not addition mod 2. It is actually saturating. It's because C first casts the two bools to int, adds them, and casts back down to bool by checking 2 != 0.

Second, converting to TWord 3 forces AddWithCarry and SubWithBorrow implementations to be pessimistic. They must take in a full 8 bits of precision in the carry bit and output 8 bits. This means one can't use the real compiler intrinsics, which treat any non-zero input as a 1. Also, for instance, this subborrow_u64 implementation isn't correct.

The effect is particularly pronounced for, say, addcarryx_u26 and subborrow_u26. In theory, these could be implemented as:

static uint8_t addcarryx_u26(uint8_t c, uint32_t a, uint32_t b, uint32_t *low) {
  uint32_t x = a + b + c;
  *low = x & ((1 << 26) - 1);
  return (x >> 26) & 1;
}

static uint8_t subborrow_u26(uint8_t c, uint32_t a, uint32_t b, uint32_t *low) {
  uint32_t x = a - b - c;
  *low = x & ((1 << 26) - 1);
  return x >> 31;
}

These functions need only extract 26+1 = 27 bits of output, so a uint32_t is a sufficient temporary. However, if the uint8_t output is treated as a true uint8_t, rather than a stand-in for a uint1_t, we need 26+8 = 34 bits of output, and we must go up a word size, even though that's not actually necessary.

Proposal:

1. Fix the TWord 0 notations to, rather than using bool, which doesn't work, use uint8_t with manual truncations. So, adding two bools would be uint8_t c = (a + b)&1. (Though I'd be surprised if you ever emitted that one.)

2. Remove the TWord 0 to TWord 3 conversion and leave all TWord 0s as-is.

3. Remove the TWord 3 notation cases for addcarryx and subborrow. Only select those intrinsics when the carry bits are TWord 0.

[davidben]

Oh, I forgot to add, this would also help with this cmovznz32 line here.

fiat-crypto/src/Specific/solinas32_2e255m19_10limbs/freeze.c

Line 22 in 8d465a7

{ uint32_t x49 = cmovznz32(x48, 0x0, 0xffffffff);

x48 is actually 1-bit, so this could be transformed into uint32_t x49 = 0u - (uint32_t)x48, but if _subborrow_u25 is not known to only output 0/1, this needs to be slightly more conservative.

[JasonGross]

Let me see if I understand.

1. For addition only, have Add (TWord 0) (TWord 0) (TWord 0) x y be rendered as (x + y) & 1. Additionally, replace bool with uint8_t, and replace (bool)x with 1&(uint8_t)x. (Rendering this way so that I can preserve the fact that casts are all prefix, which simplifies the python code a decent amount.)
2. For solinas freeze and for all montgomery operations, forbid TWord 3 and permit TWord 0
3. Drop the addcarryx and subborrowx notations that reference TWord 3.

Is this correct?

[davidben]

Re 1: arithmetic on (TWord 0) in general, and not just Add I think? I guess multiplication doesn't need it. I'm not sure what operations you have, so wherever you need it? Most of the time, the C integer size matches the modulus, so we "implicitly" get those bitmasks. But if we use uint8_t where we want uint1_t, we need to put them in because it'll only automatically reduce mode 256 instead of 2. If we use bool, we don't have the width mismatch, but then the implicit operation is the wrong one (!= 0 instead of & 1).

Otherwise, I think that's right? I suppose there's no particular reason not to permit TWord 3, but I can't imagine you'll ever actually emit it. My expectation is that the actual generated code will end up unchanged since you're not actually doing any operations on carry bits here. It's just so Fiat will give the intrinsics tighter assumptions to work with.

(Alternatively, I suppose one could massage bool into it by using ^ instead of +, & instead of *, etc. That might even help the compiler out in realizing it's got a one-bit number. But I don't know how widespread or reliable bool support is in C compilers. I remember some weird stuff going on from BarnOwl days with ancient C compilers, NCurses, and Perl, but thankfully BoringSSL doesn't care about those! :-) I'd suggest maybe start with uint8_t and we can toy with bool later?)

[andres-erbsen]

I don't think there is any reason to forbid uint8_t. If you want to distinguish bool from it, a /*comment*/ should work.

[JasonGross]

I suppose there's no particular reason not to permit TWord 3, but I can't imagine you'll ever actually emit it.

We do, in fact, emit TWord 3 in places where we add two carry bits without a guarantee that one will be zero. This also mandates handling addcarryx taking in a 1-bit carry, an 8-bit x, and a 32-bit y.

[JasonGross]

Doing number 1 is a pain, because it means I have to code 1-bit operations separately from all of the other widths, and have to duplicate the code to do that. I'm probably going to leave in the existing notations and override the boolean ones afterwards, because that's a bit simpler, I think.

[davidben]

We do, in fact, emit TWord 3 in places where we add two carry bits without a guarantee that one will be zero.

Huh. I didn't know that was in there. Where do you add carry bits?

This also mandates handling addcarryx taking in a 1-bit carry, an 8-bit x, and a 32-bit y

That's just the same as a 32-bit x, right? We'd just pass the 8-bit x into the normal 32-bit function and not really care[*]. You can widen the inputs for free, just not the outputs[**], since there might have been a modulus in there.

How was this case handled before?

[*] Maybe at some point the system should know what width of intrinsics exist, and widen as needed with proof, so you don't need to add lots of different cases to the notation, and that assertion is actually checked.

[**] Although if you changed the intermediate language from wrapping on overflow to forbidden it, I think you can widen either. But then you need to prove overflow doesn't happen. Which I assume is secretly true...

[JasonGross]

Huh. I didn't know that was in there. Where do you add carry bits?

NISTP256/AMD64/femul

That's just the same as a 32-bit x, right?

Yes. At least, in C it is. In Coq notations, not necessarily.

How was this case handled before?

I had one-off notations for "you passed in a carry bit as x" and "you passed in a carry bit as y" and "you passed in a carry bit both for x and for y". Yes, the notations here are very, very kludgy.

Maybe at some point the system should know what width of intrinsics exist, and widen as needed with proof, so you don't need to add lots of different cases to the notation, and that assertion is actually checked.

At some point we should stop using a 300-line python script that generates 12500 lines of Coq Notation directives and use a saner encoding that supports things like if and < and >. (The way that I currently encode n >= k for concrete k is by matching n with k applications of S to _. The way I encode n < k is either by swapping which notation is "default" so that I can encode ~(n >= k), or by writing out k-1 notations, one for each value of n < k.)

But then you need to prove overflow doesn't happen. Which I assume is secretly true...

It's true because the input language is in Z, and the only way to use overflow is to start off with it in the input language. But it's not entirely clear how to encode "forbidden"; that seems like a pretty deep change (maybe push option through the entire interpretation...)

[davidben]

It's true because the input language is in Z, and the only way to use overflow is to start off with it in the input language. But it's not entirely clear how to encode "forbidden"; that seems like a pretty deep change (maybe push option through the entire interpretation...)

Right. Yeah, that was more an off-hand musing than anything else. (I figure if I practice attempting to make statements about this system that type-check correctly, I'll eventually figure out how it works!) Though it is interesting to note that the only reason we need the &1 is because we aren't guaranteed by the language that wrapping around never happens.

[davidben]

Dumb question for future: if you need a Python script to post-process it anyway, why not just emit some intermediate language that's not C-like at all and easy to parse, and then the Python script, where you don't need to fight with the notations system, just translates that to C? It's trusted code either way.

[JasonGross]

Because every time we've added something, it's been easier to add one more small thing to the notation system than to rewrite the conversion from scratch in Python (or in Coq to produce a string, or OCaml, or whatever)?