fix(nview): Fix the lint error and nailway check failure
Signed-off-by: Akhil Repala <[email protected]>
Signed-off-by: Akhil Repala <[email protected]>
Signed-off-by: Akhil Repala <[email protected]>
After moving direct-deposit application from LEDGER-V into POST-CERT, CERTS-pov now produces a symmetric "consumed = produced" equation: getCoin s₁ + getCoin (DirectDepositsOf Γ) ≡ getCoin sₙ + getCoin (WithdrawalsOf Γ) Thread the direct-deposit term through the LEDGER-pov proof: * SUBLEDGERS-certs-pov gains "+ sum (map ddwl stxs)" on the LHS, where ddwl = getCoin ∘ DirectDepositsOf is the per-sub-tx direct-deposit total (analogous to wdrwl). * combined-certs gains "+ allDirectDeps" on the LHS, composing the per-sub CERTS-pov chain with the top-level call. * The main LEDGER-V chain wraps the result in +-cancelʳ-≡ to discharge the asymmetric "+ allDirectDeps" combined-certs introduces. Removed: * The certStateFinal local definition (LEDGER-V no longer applies applyDirectDeposits). * step-ii and the applyDirectDeposits-rewardsBalance module parameter (subsumed by indexedSumᵛ'-∪⁺ inside POST-CERT-pov). * The DD-split module parameter (subsumed by per-tx CERTS-pov chain). * Stale "Key Lemma" subsection and stale commented-out lines in bat'. * Unused imports +-identityʳ and +-0-monoid. * Redundant local aliases in bat's where-block. Documentation: rewrote "Key Differences from Conway" point 2 and the LEDGER-V Proof Outline to reflect the new architecture; clarified the LEDGER-I outline.