input-output-hk / implementation-decisions

A repository for all concrete decisions made about how to implement the formal specs
Other
5 stars 5 forks source link

Add initial RFC decription for elementary functions #13

Open mgudemann opened 5 years ago

NicolasDP commented 5 years ago

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.

commandodev commented 5 years ago

@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)?

mgudemann commented 5 years ago

@NicolasDP sure, no problem, I can just remove the last commit, the idea was to point to the existing prototype and its test suite. What would be a better way?

NicolasDP commented 5 years ago

I am happy for you to:

  1. put the non-integer haskell package in an open source github repo of yours (but this is only me, talk with your manager about that);
  2. link in the RFC to that github repo (as in code of reference if you like);
  3. include the implementation details in the RFC. It is a bit duplicating the content as it is already another repository. Here, we need to have something that is not Haskell only compatible. Something that is Universal (that any dev can ready and say : ok I know how to write that in ~php~ ~python~ ~javascript~ rust).
NicolasDP commented 5 years ago

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).

NicolasDP commented 5 years ago

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.

mgudemann commented 5 years ago

@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.

NicolasDP commented 5 years ago

I thought the haskell code you were referring to was your reference implementation ?

commandodev commented 5 years ago

Anything I can help to resolve/move forward here @NicolasDP and @mgudemann?

dcoutts commented 5 years ago

@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.

mgudemann commented 5 years ago

@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 PercentStake

mgudemann commented 5 years ago

@NicolasDP golden tests input-output-hk/cardano-ledger-specs#449