-
Notifications
You must be signed in to change notification settings - Fork 5
Add initial RFC decription for elementary functions #13
base: master
Are you sure you want to change the base?
Add initial RFC decription for elementary functions #13
Conversation
I am not happy with changing the submodule at the same time as proposing a new RFC. This is too much at the same time and this is certainly the best way to miss something. |
@NicolasDP how would you suggest syncing these things up then? Perhaps include the commit to the ledger spec in the RFC, but do the submodule update separated (referring to the RFC in that commit)? |
@NicolasDP sure, no problem, I can just remove the last commit, the idea was to point to the existing prototype and its test suite. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for proposing the second proposal to the CIP. I haven't been able to review the content yet as the form is not really matching the requirements:
- this is for Haskell only. we need to be universal;
- There is technical explanation, what you have giving here is only fitting (ish) the Decision part.
- you are not giving us information regarding how efficient this proposal is. If feels like the performance is guestimated here
(i.e., `1 <= x/(e^n) < e`) using bisection. Using the identity `ln(x*y) = | ||
ln(x) + ln(y)` we get `ln(x) = ln(e^n * x / e^n) = ln(e^n) + ln(x/e^n)` where | ||
`ln(e^n) = n` and `x/e^n` is an element of `[1,e)`, for which the approximation | ||
converges well. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
all of this is not really helping to write the code. This part is more fitting for the Decision level. The technical explanation is what you have in that other file : NonIntegral.hs.
I'll remind you that line: It is reasonably clear how the feature would be implemented.
I know this is hard, but you write this not as an academic but as a software developer. We need to be very accessible here, to not leave any details unsaid : otherwise a developer might get this wrong and this could affect out crypto-currency ecosystem.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@NicolasDP would you prefer pseudo-code here ?
- The more standard way for the logarithm seems to be to calculate the binary | ||
logarithm and then use a pre-calculated constant `ln(2)` to scale the result | ||
accordingly. I do not see any advantage of this apart from being able to use | ||
shifts instead of multiplications, i.e., increased efficiency. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can you give us some comparison figures with this statement ?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@NicolasDP do you mean a comparison of computing ln
directly versus implementing lb
and comparing run time of both ?
text/0000-elementary-functions.md
Outdated
shifts instead of multiplications, i.e., increased efficiency. | ||
|
||
- Taylor series approximation of `ln` seem to converge extremely slow, continued | ||
fractions have been shown to be much faster in experiments. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can you prove this statements ? We also need the figures you have have found when computing this algorithm ? How long does it take to run this algorithm in the context of leader election (i.e. phi function)?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@NicolasDP I'll add some data for this, I'd say graphs would be best to show this?
I am happy for you to:
|
For example, you can see in the RFC0001 's reference implementation note how the rust code was linked to the RFC. Also I see property tests in your haskell package. This is great but we also need golden tests (or test vector). |
And if you can add some benchmark that would be great too. We need to be able to have a very precise feeling about the time this can be computed too. The window to check if we have enough stake to write propose a block is very small, nano seconds matter here. |
@NicolasDP I am happy to provide a reference implementation (preferable in C which should be accessible from almost any language via FFI), currently we have not finalized which fractional / real representation we want to use, so this is not yet possible. |
I thought the haskell code you were referring to was your reference implementation ? |
9f3dc21
to
6b3f52a
Compare
6b3f52a
to
adbc889
Compare
Anything I can help to resolve/move forward here @NicolasDP and @mgudemann? |
@mgudemann has done lots of updates and conducted a design review with the formal methods team. The consensus from that review is to pursue the approach based on fixed point calculations and iterative approximation. In particular the team is convinced the approaches based on IEEE floating point or rationals will not be acceptable. The floating point approach has too high a danger of loss of consensus and the rational approach has unacceptable runtime. His latest work includes graphs showing the error levels with two different approximation methods, with different numbers of iterations. The formal methods team have asked for criterion benchmarks to evaluate the runtime vs precision tradeoff. His latest update includes two reference implementations of the fixed point method that agree with each other exactly. One in Haskell and one in C. He can also generate gigabytes of test vectors. This should address the concern expressed by @NicolasDP about clarity on how to implement the specification. Once these requested updates are ready we will request re-review here. |
@NicolasDP here is the link to the document which includes the design rationale and timig information for the Haskell implementation on a recent amd64. https://hydra.iohk.io/build/779843/download/1/non-integer-calculations.pdf As we talked about in Miami, the C reference implementation performs reasonably well even on the Rock Pi boards. For Jörmungandr, it should be relatively easy to implement simple FFI calls (1 to precompute from the active slot coefficient, 1 to actually return a Boolean value for being in the leader set) where all parameters are of integral type fitting in 64 bits, e.g., having the relative stake as nominator / denominator pair as in |
@NicolasDP golden tests IntersectMBO/cardano-ledger#449 |
No description provided.