Ver Fonte

doc/spec/contract/vesting: vesting formula calculations explanation and example added and fixed wrong forfeit check

skoupidi há 4 meses atrás
pai
commit
e85401b5ed

+ 121 - 0
doc/src/spec/contract/vesting/concepts.md

@@ -52,6 +52,127 @@ tracked.
 > concluded without access to the vesting information and/or the shared
 > secret address.
 
+### Vesting formulas
+
+Let $E, S, V, C, T$ be the vesting configuration parameters as defined
+in [Vesting Configuration](model.md#vesting-configuration).
+
+Let $t₀ = \t{BlockWindow} ∈ 𝔽ₚ$ be the current blockwindow as defined
+in [Blockwindow](model.md#blockwindow).
+
+Let $Bv ∈ ℕ₆₄$ be the burned coin.
+
+The core formula to compute amounts corresponding to the current block
+window is:
+
+$$ \begin{aligned}
+CurrentBlockwindow = CondSelect(BlockwindowCond, t₀, E); \\
+BlockwindowsPassed = CurrentBlockwindow - S; \\
+Available = (BlockwindowsPassed * V) + C; \\
+Withdrawn = T - Bv; \\
+WithdrawCoinValue = Available - Withdrawn; \\
+VestingChangeValue = T - (Withdrawn + WithdrawCoinValue);
+\end{aligned} $$
+
+The vesting schedule model says that any blockwindow $t$ where
+$S <= t <= E$, the total amount that should have been unlocked is:
+
+$$ \begin{aligned}
+Available(t) = (t - S) * V + C;
+\end{aligned} $$
+
+And we know from the vest proof's constraint that $T = (E-S) * V + C$,
+so $Available(E) = T$. The schedule is linear between $S$ and $E$ with
+a cliff C at the start.
+
+The burned vested coin has value $Bv$ which represents the remaining
+balance in the vested coin. Initially (right after vest) $Bv = T$.
+After each withdrawal it shrinks.
+
+So "total withdrawn so far" is $T - Bv$ and the formula computes how
+much new value the vestee can take:
+
+$$ \begin{aligned}
+WithdrawCoinValue = Available - (T - Bv) = Available - T + Bv; \\
+VestingChangeValue = Bv - WithdrawCoinValue;
+\end{aligned} $$
+
+Concrete example:
+
+Let:
+
+$$ \begin{aligned}
+T = 1000; \\
+C = 100; \\
+S = 10; \\
+E = 20; \\
+V = 90; \\
+(20 - 10) * 90 + 100 = 1000;
+\end{aligned} $$
+
+First withdrawal at $t = 12$ with $Bv = 100$ as the initial vested coin:
+
+$$ \begin{aligned}
+Available = (12 - 10) * 90 + 100 = 280; \\
+Withdrawn = 1000 - 1000 = 0; \\
+WithdrawCoinValue = 280 - 0 = 280; \\
+VestingChangeValue = 1000 - 280 = 720;
+\end{aligned} $$
+
+Conservation: $280 + 720 = 1000 = Bv$
+
+Second withdrawal at $t = 15$ with $Bv = 720$ from previous change coin:
+
+$$ \begin{aligned}
+Available = (15 - 10) * 90 + 100 = 550; \\
+Withdrawn = 1000 - 720 = 280; \\
+WithdrawCoinValue = 550 - 280 = 270; \\
+VestingChangeValue = 720 - 270 = 450;
+\end{aligned} $$
+
+Conservation: $270 + 450 = 720 = Bv$
+
+Cumulative withdrawn: $280 + 270 = 550 = Available(15)$
+
+Final withdrawal at $t = 20$ (end) with $Bv = 450$ from previous change
+coin:
+
+$$ \begin{aligned}
+Available = (20 - 10) * 90 + 100 = 1000; \\
+Withdrawn = 1000 - 450 = 550; \\
+WithdrawCoinValue = 1000 - 550 = 450; \\
+VestingChangeValue = 450 - 450 = 0;
+\end{aligned} $$
+
+Cumulative: $280 + 270 + 450 = 1000 = T$
+
+Expanding $VestingChangeValue$:
+
+$$ \begin{aligned}
+VestingChangeValue = Bv - WithdrawCoinValue; \\
+VestingChangeValue = Bv - (Available - T + Bv); \\
+VestingChangeValue = T - Available;
+\end{aligned} $$
+
+at $t = 12$, $change=1000-280=720$
+
+at $t = 15$, $change=1000-550=450$
+
+at $t = 20$, $change=1000-1000=0$
+
+^ This means $WithdrawCoinValue = Bv - (T - Available) = Bv -
+VestingChangeValue$ which is just the difference between what the coin
+held and what must remain locked.
+
+We can compute $VestingChangeValue = T - Available$ then derive
+$WithdrawCoinValue = Bv - VestingChangeValue$.
+
+Proof simplification:
+$$ \begin{aligned}
+VestingChangeValue = BaseSub(T, Available); \\
+WithdrawCoinValue = BaseSub(Bv, VestingChangeValue)
+\end{aligned} $$
+
 ## Forfeit
 
 With this call, a vesting authority is able to forfeit a specific

+ 6 - 3
doc/src/spec/contract/vesting/scheme.md

@@ -291,9 +291,12 @@ ForfeitValue, t, \t{CID}_\t{V}, \t{SH}_\t{V}, ℬ, b_\t{Coin})$
 **Burned vested coin nullifier integrity** &emsp; $\cN =
 \t{PoseidonHash}(x_c, BCoin)$
 
-**Minted coin integrity** &emsp; $Coin =
-\t{PoseidonHash}(\mathcal{X}(p.\t{SPK}), \mathcal{Y}(p.\t{SPK}),
-ForfeitValue, t, \t{CID}_\t{V}, \t{SH}_\t{V}, ℬ, b_\t{Coin})$
+**Minted coin integrity** &emsp;
+let $c.\t{CID}, c.\t{SH}, c.\t{UD}$ be the vesting authority
+chosen Contract ID, spend hook and user data for the minted coin,
+and verify $Coin = \t{PoseidonHash}(\mathcal{X}(p.\t{VAPK}),
+\mathcal{Y}(p.\t{VAPK}), ForfeitValue, t, \t{CID}, \t{SH},
+\t{UD}, b_\t{Coin})$
 
 ### Signatures