Ed25519: Point-based separation logic for doubling#2122
Conversation
|
@andres-erbsen Can you take a look, please? There's still some small things I want to fix, maybe you can help get these right (see TODO's in the file). Also feel free to suggest some changes to make this usable for the rest of the file. |
miriampolzer
force-pushed
the
point_struct_squashed
branch
from
e76c5da to
1f4824f
Compare
| Definition felem_size := Eval compute in felem_size_term. | ||
|
|
||
| (* TODO how do we call these points? I call them normal points in my head :D *) | ||
| Notation "A .x" := (expr.op Syntax.bopname.add A (0*felem_size)) (in custom bedrock_expr at level 3, left associativity). |
There was a problem hiding this comment.
level 3 seems like it would bind less tightly than negation. Maybe it was a mistake to put negation at level 1. But perhaps 0 works here?
There was a problem hiding this comment.
Level 0 doesn't work because level 0 is right associative. On the other hand I suppose we don't chain these so we could ignore having the wrong associativity? Still could lead to hard-to-find errors...
There was a problem hiding this comment.
which leaves us with the mystery of why level 0 is right-associative. But okay, make it level 2 and then we can move - to 3 later, perhaps roughly following c++.
| subst Pz Py Px Pta Ptb. | ||
| extract_ex1_and_emp_in H87. | ||
|
|
||
| (* Now we need to convert scalar to ptsto, because straightline_dealloc can't handle scalar yet. *) |
There was a problem hiding this comment.
The code below looks as expected, but are there actually scalar-s being deallocated, or only Bignums? either way we'd want to automate this, but slightly different steps may be needed for each.
There was a problem hiding this comment.
I think I found a tactic that will work for the other proofs too.
| remember (Bignum.Bignum felem_size_in_words (p_out.+0) x10) as Px in H92. | ||
| remember (Bignum.Bignum felem_size_in_words (p_out.+120) x8) as Pta in H92. | ||
| remember (Bignum.Bignum felem_size_in_words (p_out.+160) x6) as Ptb in H92. | ||
| do 7 (seprewrite_in @Bignum.Bignum_to_bytes H92). |
There was a problem hiding this comment.
does repeat run too long here or otherwise mess up?
There was a problem hiding this comment.
It does, but only because we weren't remembering enough values. I think I can fix this and create a generic tactic.
There was a problem hiding this comment.
I turned it around and created a tactic that finds the addresses that need to be converted into byteformat. Much easier than telling the tactic to remember a certain set of addresses we still need.
miriampolzer
force-pushed
the
point_struct_squashed
branch
2 times, most recently
from
50c082a to
041df02
Compare
Convert the doubling function to a point based format, the rest of the functions will follow. Add a tactic for deallocation, to be used in other proofs too.
miriampolzer
force-pushed
the
point_struct_squashed
branch
from
041df02 to
d6cf8f9
Compare
|
From my side, this is ready to be merged. I'll work on a follow-up to convert the rest of the file to new notations. |
2 participants
Convert the doubling function to a point based format, the rest of the functions will follow.