merge Group.Scalarmult into MontgomeryLadder, use in x25519_base #1843
Conversation
| @@ -200,7 +214,7 @@ Definition garagedoor_iteration : state -> list (lightbulb_spec.OP _) -> state - | |||
| (TracePredicate.one ("st", lightbulb_spec.GPIO_DATA_ADDR _, action))) ioh | |||
| /\ ( | |||
| let m := firstn 16 garagedoor_payload in | |||
| let v := le_split 32 (F.to_Z (x25519_gallina (le_combine sk) (Field.feval_bytes(FieldRepresentation:=frep25519) garageowner))) in | |||
| let v := le_split 32 (M.X0 (Curve25519.M.scalarmult (le_combine sk mod 2^255) garageowner_P)) in | |||
| exists set0 set1 : Naive.word32, | |||
There was a problem hiding this comment.
Does plain M refer to the same M as Curve25519.M? For readability, it would be good to be consistent within this line about how fully-qualified the names are.
There was a problem hiding this comment.
👍 ; the two are definitionally equal anyway. I intend to do another spec-cleanup pass anyway.
| @@ -220,7 +234,7 @@ Definition garagedoor_iteration : state -> list (lightbulb_spec.OP _) -> state - | |||
| udp_local ++ udp_remote ++ | |||
| be2 udp_length ++ be2 0 ++ | |||
| garagedoor_header ++ | |||
| le_split 32 (F.to_Z (x25519_gallina (le_combine sk) (F.of_Z _ 9))))) | |||
| le_split 32 (M.X0 (Curve25519.M.scalarmult (le_combine sk mod 2^255) Curve25519.M.B)))) | |||
There was a problem hiding this comment.
memrep below guarantees that sk is of length 32, so if you le_combine it, it should not be bigger than 2^256, but you have a mod 2^255, so what's going on with that one bit? Is this the intended spec? Or could you require in the pre and post of loopfn that this bit is 0? Or could it actually be 1? Would the scalar multiplication implementation really not work for scalars between 2^255 and 2^256?
There was a problem hiding this comment.
Yes, the ladder blatantly ignores that bit. There is no reason to use scalar this large, so this is a free fraction-1/256 speedup that has become a part of the spec. Currently the code does not actually clear this bit before calling the ladder, so memrep change would need a code change. (BoringSSL even sets that bit to have ladders that don't ignore it break in testing...).
There was a problem hiding this comment.
Ok, so it looks like everything on this line is actually required. And it appears twice in almost the same form, so could you factor that out into a definition? Would be nice if the code snippet we'll show in the paper and on slides is actually literally what curious readers will find in the source. I could imagine one function taking a list of bytes representing a scalar and a highlevel Curve25519.M.point, and returning a curve point represented as a list of bytes, or two functions, one to convert from byte list to truncated scalar, and one converting from curve point to list of bytes. [end of gardening 🌷🌹🌻😉]
No description provided.