Closed andres-erbsen closed 3 years ago
I haven't looked under the FElem interface much, but looking at frep
, it seems pretty fine to work with its implementation directly in any of the code that I've touched. Even if there is some code that wants to differentiate FElem
and Bignum
, which I haven't seen, we could probably reduce it to a local alias rather than a fully opaque class.
As far as ordering, I would like to prioritize the parameter changes so that I'm not working on two Rupicola branches longer than necessary. On the other hand, it probably makes sense to make this change, if we're going to, before trying to move any additional code to a unified predicate like we were considering since it will have some effect on that.
Hmm, I think it's a useful layer of abstraction. frep
already exposes things like Bignum
and list_Z_bounded_by
for bounds that the group layer should really not be unfolding; the FieldRepresentation interface basically enforces that rule. Sure, if we trust that everyone who ever writes anything at the group level will know better than to ever unfold frep
, it wouldn't be an issue, but that seems more fragile to me.
The other argument is that right now, the whole Specs
folder has minimal dependencies on the rest of fiat-crypto (really just the algebra library and a couple of number-theory lemmas). However, frep
requires a lot more, including depending on Arithmetic.Core
and COperationSpecifications
. I think you need to be much more familiar with the codebase to understand what's happening in frep
than you do for FieldRepresentation
; if someone is mostly working at the group level, that familiarity isn't needed otherwise, so it might be preferable to read an interface that doesn't require anything more than algebra fundamentals.
Also, I believe @RasmusHoldsbjergCSAU is working on a Montgomery pipeline that uses a different instance than frep
because the bounds interface in frep
doesn't quite fit the needs of word-by-word Montgomery (although I did originally intend for both Barrett and wbw to use frep
, so the solution here might be adjusting frep
so they both can use it).
I get the argument about minimal dependencies (proposal below), but maybe we could achieve something similar with a more transparent interface? First, why more transparent? The group layer needs more information about than currently revealed in this interface. We could try to extend the interface, but it is not clear what to do.
For example, the group layer wants to use conditional memcpy
to select field elements -- so either this interface would need to have a conditional select function, or we should reveal that FElem
are in fact just bytes (and can be converted back and forth). The latter would be easy if we just revelealed that FElem is an array (Bignum). And I imagine we'll want a multi-select soon, for tables.
Separately, this admit seems unprovable without knowing more about bytes_in_bounds
-- and the obvious solution to me would be to reveal the relevant definition from Representation
.
Here is a variant of Representation.v that does not directly depend on the files you mentioned; I have not looked at what Bignum.v
depends on yet but I believe that could be minimized as well. Would a file like this be acceptable as an interface decoupling clients of the field library from rest of fiat-crypto. (porting note: all definitions in the new file should be convertible with the previous ones except for ModOps.weight which I simplified).
@jadephilipoom wdyt?
Is this related to the admitted we have at https://github.com/mit-plv/fiat-crypto/blob/ce3374cbce20d9668241baf5bfd1b87167af9911/src/Bedrock/Field/Synthesis/New/UnsaturatedSolinas.v#L432-L455 from 050b87a51186e3e3978f92a0cf4efea1f867cd3d / #991 ?
Yes, it's the same one I mentioned in my previous message in this thread.
wdyt?
The Representation.v you linked to seems reasonable to me. If the group level geniunely needs more information and obscuring the data layout causes problems, then it makes sense to provide more information in that interface. But I'm still a little nervous about specializing the interface without a working wbw Montgomery pipeline -- could easily end up accidentally specializing to an interface Montgomery can't fulfill.
I kind of like the option you alluded to of creating a way to convert the field element to bytes as a no-op operation that just lets you treat it as some array of bytes for use cases like this (and another no-op to convert it back to the usual felem representation). But I think that's more a matter of personal preference, also happy with the solution you proposed.
I dug into the remaining admit and :
FElemBytes
should probably include bytes_in_bounds
(which says there aren't more bits than in the prime) so that an admit of this implication can be proven, or alternatively from_bytes
should take bytes_in_bounds
as a separate precondition.spec_of_to_bytes
should uniquely specify the output bytes as a function of eval of input like COperationSpecifications does so that X25519 can have a deterministic specification, which will require changes at whatever place connects COperationSpecifications to bedrock2 specs which I haven't found yet@jadephilipoom @DIJamner do you have advice or preference on either question?
I haven't looked much at working with from_bytes
and to_bytes
or at this admit, so I don't have a preference on this one.
alternatively
from_bytes
should takebytes_in_bounds
as a separate precondition.
~This one sounds better to me -- hesitant to mix in a proof if we don't have to.~ Never mind, this is the separation logic condition and not the data representation -- I think it makes sense to add in bytes_in_bounds
to FElemBytes.
whatever place connects COperationSpecifications to bedrock2 specs which I haven't found yet
This line is where the COperationSpecifications proof is used to prove the bedrock2 specs:
Basically there are existing proofs in PushButtonSynthesis that say the pipeline result matches COperationSpecifications, and we use that to prove the pipeline result matches bedrock2 specs.
:+1: though note that the link is to from_byres
whereas I was also referring to changing to_bytes
spec and proof
My bad, fixed the link! It's very similar in all the proofs.
Pada Jum, 22 Okt 2021, 2:27 PG jadephilipoom @.***> menulis:
My bad, fixed the link! It's very similar in all the proofs.
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/mit-plv/fiat-crypto/issues/1022#issuecomment-948891176, or unsubscribe https://github.com/notifications/unsubscribe-auth/AUC4LS33AKNNCB2R4Y5CSDTUIBLPNANCNFSM5FBE3S7Q .
We might garbage-collect this interface at a later time, but the blocking issues here have been resolved.
I don't see us ever using a different implementation of
FieldRepresentation
thanfrep
inRepresentation.v
and thus I feel this interface serves no conceptual function. Can we remove it, or is it essential for preventing unfolding or something else? @jadephilipoom @DIJamnerFieldRepresentation_ok
saysFElem
has the same memory footprint as aPlaceholder
, which is defined right above asMemory.anybytes p felem_size_in_bytes
, which meansfelem_size_in_bytes
bytes. That count is further required to be 0 modwidth/8
; the corresponding quotient is exactly then
inRepresentation.v
. So we're definitely dealing with an array ofn
words -- and thefelem
type is in fact instantiated with a list of words.There is slightly more flexibility with other fields, perhaps most seriously
eval
could itself be a parameter instead of parametrizing over a weight function, but I still don't see a use case for different parameters, so I'd be inclined to squash it.Edit: And if we do want to do this, how should we order it wrt other planned refactorings?