bedrock2 extraction tracker issue #524
Comments
|
The second pass should be possible as a rewriter pass. The third pass probably wants something like CStringification / the translation to fancy |
|
I totally forgot about to today, but I'd like to brainstorm how to do the second pass (perhaps using the new and glorious lemma reification interface once it is working enough). |
|
We probably need a special identity identifier which is Definition assemble (x y : Z) : Z := ((x << 32) + y).
Definition break (x : Z) : Z * Z := (ident.cast word32 (x >> 32), ident.cast word32 (x mod 2^32)).
ident.cast word64 x = dlet yz := break x in inline (assemble (ident.cast word32 (fst yz)) (ident.cast word32 (snd yz))
break (inline (assemble (ident.cast word32 x) (ident.cast word32 y))) = (ident.cast word32 x, ident.cast word32 y)
(inline (assemble (ident.cast word32 x1) (ident.cast word32 x2)) + inline (assemble (ident.cast word32 y1) (ident.cast word32 y2)) = stuff involving addcBasically, the idea I have is that we first replace all of the things known to be word64 with |
|
Note that there is some work-in-progress on this at master...JasonGross:split-mul It is mostly untested, and I probably won't get much of a chance to work on it before the end of the summer. |
|
I have now put a bit more work into it and tested it, and it seems to mostly work well. For 64-bit 25519 mulmod, we get code like fiat-crypto/src/SlowPrimeSynthesisExamples.v Lines 79 to 321 in 79356b0 The only remaining |
|
this looks awesome. could we just a rewrite rule that moves the uint128->uint64 conversion inside the &, and then inside the <<, and then cancel the uint64->uint128 conversation? |
You're asking for something like Note that the >> | << & construct comes directly from the rewrite rule, so we can make it whatever we want as long as it's sound. |
|
okay. could we have this rule after bounds analysis? having truncating cast also sounds fine though. in bedrock2 we have only one word type anyway.
|
|
This entire pass already runs after bounds analysis (which doesn't guarantee boundedness, only that the overall behavior is independent of what you choose to do when something is out of bounds. Presumably we should fix this oversight some day.) Do you want to see an explicit truncating cast, or are you fine with just recognizing |
|
just to state it explicitly: either option is fine by me |
|
Let's do |
|
the common type pass is not verified, right? I think I should branch off before it. also whatever I do well only work if there is only one integer type remaining in the code. |
That's correct
So you want the carry bits to be stored in uint64_t? We can just tell bounds relaxation to not support 1-bit values. Then we can expect code to end up with only one integer type. |
|
Actually, hm, I think we might want to add an explicitly truncating left-shift, which we can just define as |
|
I'm currently looking at a 32bit target, but yes, even carry bits in the same type as other integers. truncating shift sounds fine as well. |
|
I will soon have a PR that adds |
See mit-plv#524 for discussion and justification.
See mit-plv#524 for discussion and justification.
See mit-plv#524 for discussion and justification.
See mit-plv#524 for discussion and justification.
See #524 for discussion and justification.
|
I have mostly gotten the rewrite to truncating_shiftl to work. There is still a strange issue with Anyway, the current code (master...JasonGross:split-mul) is fiat-crypto/src/SlowPrimeSynthesisExamples.v Lines 666 to 908 in 5dc4f71 Modulo the |
|
I have tracked down the issue with Line 846 in 16b657a Line 879 in 16b657a Currently, we error if you try to store the carry in anything other than a uint1. I can parameterize this part of the pipeline on an argument (I'm tempted to make it a typeclass) controlling the width of the carry argument, and then pipe that through from the higher levels. But it's starting to feel a lot like spaghetti code, and I'd appreciate sitting down with you sometime and figuring out how we should structure the options related to this pass. Anyway, other than this one issue, I believe the code is ready to have work done on translating from the IR we target (for C and Rust) to Bedrock. |
See mit-plv#524 (comment) for discussion of remaining issues
See mit-plv#524 (comment) for discussion of remaining issues
|
We should be bottoming out in phoas, not the C "IR". |
This adds a rewriting pass (disabled by default) which can split apart multiplications to emit code in a single integer type. Note that we can emit PHOAS code with only a single integer type, but to emit C code, we must also allow uint1; see mit-plv#524 (comment) for more details. We leave it like this because the bedrock2 translation will be coming from PHOAS. Note that we must still permit wider integer types during bounds analysis, because otherwise we'll fail to assign bounds before we even get to the point of splitting multipliciations. Note that this rewriting pass is still admitted, so this commit adds a dependency on an axiom to the overall pass. (We could create a separate pipeline if we wanted the code we're extracting to not depend on this admitted proof.) The interesting files to look at here are `src/RewriterRules.v` (defining the rewriting rules) and `src/SlowPrimeSynthesisExamples.v` giving examples. The admitted proof is in `src/RewriterRulesProofs.v`.
This adds a rewriting pass (disabled by default) which can split apart multiplications to emit code in a single integer type. Note that we can emit PHOAS code with only a single integer type, but to emit C code, we must also allow uint1; see #524 (comment) for more details. We leave it like this because the bedrock2 translation will be coming from PHOAS. Note that we must still permit wider integer types during bounds analysis, because otherwise we'll fail to assign bounds before we even get to the point of splitting multipliciations. Note that this rewriting pass is still admitted, so this commit adds a dependency on an axiom to the overall pass. (We could create a separate pipeline if we wanted the code we're extracting to not depend on this admitted proof.) The interesting files to look at here are `src/RewriterRules.v` (defining the rewriting rules) and `src/SlowPrimeSynthesisExamples.v` giving examples. The admitted proof is in `src/RewriterRulesProofs.v`.
|
Some work on translating to bedrock2 in the bedrock-integration1 branch. I got it to work on Curve25519 64-bit, but 32-bit fails because in some places the code uses [0] https://github.com/mit-plv/fiat-crypto/blob/bedrock-integration1/src/Bedrock/CompilerTest.v#L1702 |
|
The issue is that for some reason we are not picking up the pattern that is supposed to remove |
|
I thought some of the more recent changes were supposed to fix this issue, but it's still there, so poke @JasonGross |
|
Ah, we did make more progress this time, now there is a different issue. The issue is that inlining is not happening correctly, because the rewriter can't inline complex combine_at_bitwidth statements, only simple ones. The solution is to add let-bindings in the final >> rewrite rule as in the addition ones, i.e., change ; (forall xl xh offset,
0 < offset < bitwidth
-> doublewidth (cstZsingle_to_double xl xh >> singlewidth ('offset))
= cstZsingle_to_double
(Z.lor (singlewidth (singlewidth xl >> singlewidth ('offset)))
(singlewidth
(Z.truncating_shiftl
(singlewidth ('bitwidth))
(singlewidth xh)
(singlewidth ('(bitwidth - offset))))))
(singlewidth xh >> singlewidth ('offset)))to ; (forall xl xh offset,
0 < offset < bitwidth
-> doublewidth (cstZsingle_to_double xl xh >> singlewidth ('offset))
= dlet outl := singlewidth (Z.lor (singlewidth (singlewidth xl >> singlewidth ('offset)))
(singlewidth
(Z.truncating_shiftl
(singlewidth ('bitwidth))
(singlewidth xh)
(singlewidth ('(bitwidth - offset)))))) in
dlet outh := singlewidth (singlewidth xh >> singlewidth ('offset)) in
cstZsingle_to_double outl outh(Sorry for the atrocious indentation; I typed this on my phone) |
|
I've updated #614 / #615 @jadephilipoom and now all the |
|
Should we close this issue? There are still a couple of kinks to work out, like #750, but at this point it's more polishing than feature-adding. If there are no objections, I'll consider myself free to close it. |
It would be cool to generate bedrock2 code from fiat-crypto. I think it might go roughly as follows:
bedrock2.Syntax.cmdThe text was updated successfully, but these errors were encountered: