Expand description
How much of the whole plan one node is, and why nobody can mint more.
The part crates/kernel/spec/Share.lean specifies this module.
A share exists in exactly two ways: it is the whole plan, or it is
one part of a share that was divided. Share::split takes its
input by value and hands back parts that add up to it exactly, so
conservation is not a rule that is checked — it is the only thing
the type can express. There is no constructor, no arithmetic, and
no Deserialize: a number read off a file cannot become a share
without being divided out of the whole first.
That is what settles the estimation problem. A resident that splits its own branch chooses how its own share is divided and cannot reach past it, so an over-eager estimate costs its neighbours nothing and the total stays 1. Capping replaces refereeing.
Billionths rather than a fraction: two shares compare and add the same way on every machine, repeated division never grows a denominator, and no float ever touches a decision path (ARCHITECTURE.md section 10 rule 6).
Structs§
- Share
- Billionths of the whole plan.
Constants§
- WHOLE_
PPB - The whole plan, in billionths. Public because a reader comparing a share against the total needs the same constant the split used.
Functions§
- gather
- Adds shares that were divided out of one whole.