feat(protocol): address ai review
Signed-off-by: cryptodj413 <[email protected]>
Signed-off-by: cryptodj413 <[email protected]>
After direct-deposit application moved from LEDGER-V/SUBLEDGER-V into the
POST-CERT rule, the Certs preservation-of-value proofs needed to account for
the `getCoin (DirectDepositsOf Γ)` increase that POST-CERT now produces via
`rewards ∪⁺ directDeposits`.
Statement changes:
- POST-CERT-pov: getCoin s ≡ getCoin s'
→ getCoin s + getCoin (DirectDepositsOf Γ) ≡ getCoin s'
- sts-pov: gains a `+ getCoin (DirectDepositsOf Γ)` term on the LHS
- CERTS-pov: becomes the symmetric "consumed = produced" form
getCoin s₁ + getCoin (DirectDepositsOf Γ)
≡ getCoin sₙ + getCoin (WithdrawalsOf Γ)
Structural changes:
- POST-CERT-pov and sts-pov move into the parameterized `Certs-Pov-lemmas`
sub-module (alongside PRE-CERT-pov), since they now require a fourth
module parameter:
indexedSumᵛ'-∪⁺ : ∀ (m m' : Rewards) → getCoin (m ∪⁺ m') ≡ getCoin m + getCoin m'
This is the natural ∪⁺ analogue of the existing `indexedSumᵛ'-∪` lemma for
`∪ˡ` on disjoint domains, but unconditional because `∪⁺` adds (rather than
drops) values at shared keys. TODO: upstream to agda-sets.
- `Certs-PoV` (in PoV.lagda.md) gains the same parameter and forwards it.
CERT-pov and PRE-CERT-pov are unchanged: the CERT and PRE-CERT rules did
not change in this refactor.
Closes part of #1185.
Following the merge of CIP-159 PR #1197 (DirectDeposits keyed by RewardAddress; applyDirectDeposits and applyWithdrawals refactored through a shared applyToRewards fold) and the agda-sets cleanup PR #1196 (Conway Equivalence.Map utilities moved into Ledger.Prelude), this commit updates the Dijkstra CERTS preservation-of-value proofs to compile against the new APIs. Main changes: + Rename `ApplyWithdrawals-PoV` sub-module to `ApplyToRewards-PoV`, since it now houses lemmas for both withdrawals and direct deposits. + Add `getCoin-∪ˡ-overwrite` bridge lemma: `getCoin (❴ c , v ❵ ∪ˡ acc) ≡ v + getCoin (acc ∣ ❴ c ❵ ᶜ)`. Encapsulates the listing-vs-replacement reconciliation between the new `❴ k , v ❵ ∪ˡ acc` form (used by `applyToRewards`) and the equivalent complement-restricted form used by the existing decomposition reasoning. + Factor `split-by-lookup` as a top-level lemma decomposing `getCoin acc` along a known lookup result. Used by both `applyOne-pov` (subtraction) and the new `applyOne-pov-add` (addition). + Add the additive parallel: `applyOne-pov-add`, `foldl-applyOne-pov-add`, and `applyDirectDeposits-pov`. Mirrors the existing withdrawal chain, sharing `getCoin-∪ˡ-overwrite` and `split-by-lookup`. + Strengthen the `setToList-Unique` module parameter with a `NetworkId` premise on the map's domain (the assumption no longer conflates withdrawals-specifically with general `RewardAddress ⇀ Coin` maps). + Replace the `∪ˡ-res-lookup-preserve` module parameter (which carried a no-longer-needed complement restriction on the right operand) with `∪ˡ-lookup-preserve`, stated against the new `❴ c , v ❵ ∪ˡ m` form. + Add a small top-level helper `∈-dom⇒¬lookup-nothing` to discharge the defensive `nothing` case of `foldl-applyOne-pov-add`. + Update `POST-CERT-pov` to use the new `applyDirectDeposits-pov`; the proof is `sym (applyDirectDeposits-pov ...)`. The CERT-post step's own `mapˢ stake (dom dd) ⊆ dom rewards` premise is extracted from the pattern rather than threaded as a separate parameter, since the pre-CERT* state's `dom rewards` is not preserved across `CERT` trace steps (in particular by `DELEG-dereg`). + Update `sts-pov` and `CERTS-pov` signatures accordingly: add the `DirectDeposits`-`NetworkId` premise, drop the membership-of-deposits premise. The proofs now typecheck on top of master.
Update conformance tests
Bumps [idna](https://github.com/kjd/idna) from 3.11 to 3.15. - [Release notes](https://github.com/kjd/idna/releases) - [Changelog](https://github.com/kjd/idna/blob/master/HISTORY.md) - [Commits](https://github.com/kjd/idna/compare/v3.11...v3.15) --- updated-dependencies: - dependency-name: idna dependency-version: '3.15' dependency-type: indirect ... Signed-off-by: dependabot[bot] <[email protected]>
Signed-off-by: cryptodj413 <[email protected]>
* meeting 134 merges * add CIP-0177 confirmed after post meeting waiting period
Signed-off-by: cryptodj413 <[email protected]>
Signed-off-by: Jonathan Lim <[email protected]>