WIP -- [Dijkstra] CIP-159-11a: Prove CERTS preservation of value (#1185) by williamdemeo · Pull Request #1210 · IntersectMBO/formal-ledger-specifications

williamdemeo · 2026-05-28T04:46:45Z

Description

Closes #1185. Stacked on #1189 (base: 1186-dijkstra-utxo-and-utxow-pov); GitHub retargets it as the PRs below merge.

Discharges all five Certs-side parameters of the LEDGER-PoV contract (#1203), with statements matching the parameter block verbatim and nothing left open on the Certs side.

What lands

Certs.Properties.PoV: CERTS-rewards-pov, CERTS-deposits-pov, CERTS-deposits-registered, CERTS-new-thread, refundCertDeposits-++.
Certs.Properties.PoVLemmas: the per-CERT-step accounting and the newCertDeposits/refundCertDeposits fold algebra.
Ledger.Prelude (append-only): getCoin-∪⁺-singleton, getCoin-remove, dom-∪ˡ-singleton, plus private scaffolding.
Property catalog: dijkstra-certs-pov now derives as proved.
Ledger.Properties.PoV rewiring: the five Certs parameters are deleted and the facts imported from Certs.Properties.PoV (contract from 17 to 12 parameters).

Key points for review

PoolDepositsRegistered is used exactly once, in the POOL-reg case: the rule's left-biased pot update needs the key fresh in the pot, and the invariant transports the rule's freshness premise there. It is preserved because the rule extends pot and pool map by the same key.
The fold lemmas reach newCertDeposits's private step function through seed certificates; see the preamble of Certs.Properties.PoVLemmas.
No CHANGELOG entry: property modules and Prelude lemmas only, no semantic spec change.

Verification

The rewired Ledger.Properties.PoV typechecks with the five parameters deleted, which verifies the discharge by construction.
agda src/Ledger.lagda.md and scan_properties.py --check both green.

Checklist

Commit sequence broadly makes sense and commits have useful messages
Any semantic changes to the specifications are documented in CHANGELOG.md (none in this PR)
Code is formatted according to CONTRIBUTING.md
Self-reviewed the diff

🤖 AI-assisted development: Claude Fable 5 (Anthropic)

Records the precise, ordered steps to make this PR faithful to the top-down plan: delete the Certs-PoV provider modules (Certs/Properties/PoV and PoVLemmas, which are #1210's work), drop their imports from Certs/Properties, and lift the facts they provide (CERTS-pov, and later CERTS-coinFromDeposits-updateCertDeposits) to module parameters in Entities.Properties.PoV and the LEDGER-PoV module. Notes that Utxo/Utxow-PoV are already absent (deferred to #1189) and already parameterized, flags the Conway-side touches to re-check, and cross-references the separate coinFromGovDeposit re-derivation. Prose only; to be executed in a session with the Agda toolchain so each step can be typechecked. https://claude.ai/code/session_0174ZBS1RKAGSbBXDsESUwoA

The LEDGER-pov `UTXOW-batch-balance-coin` parameter previously baked the chain's post-batch cert states cs₁/cs₂ into the (#1186) UTxO obligation via the two-level posPart/negPart deposit form, leaving free cert-state implicits that #1186 cannot discharge. Restate it as the pure closed-form coin projection of the spec's `consumedBatch ≡ producedBatch` premise: cert deposits as `refundCertDeposits`/`newCertDeposits` over `allDCerts tx` from the pre-batch cert state, with no post-batch `cs₂`. This is a clean, purely-UTxO #1186 obligation. `bat'` now converts that closed form to the chain's two-level form via: - a new `batch-cert-deposits-bridge` module parameter (deferred to #1210): `depositsChange pp cs₀ (allDCerts tx) ≡ coinFromDeposits cs₂ ⊖ coinFromDeposits cs₀`, the batch-wide cert-deposit accounting reconciling the spec's closed-form cert deposits with the actual post-ENTITIES cert state; and - `convert`/`net-arith`, combining the bridge with `posNeg-deposits` (two-level) and `posPart-negPart-sym` (net level) by cancelling `D₀ + posPart(net)`. This cleanly separates the UTxO batch balance (#1186) from cert-deposit evolution (#1210); all cert-specific facts remain deferred as module parameters. Typechecks under --safe. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01We2YdXX2ozJAdAbCrRwi6r

Records the precise, ordered steps to make this PR faithful to the top-down plan: delete the Certs-PoV provider modules (Certs/Properties/PoV and PoVLemmas, which are #1210's work), drop their imports from Certs/Properties, and lift the facts they provide (CERTS-pov, and later CERTS-coinFromDeposits-updateCertDeposits) to module parameters in Entities.Properties.PoV and the LEDGER-PoV module. Notes that Utxo/Utxow-PoV are already absent (deferred to #1189) and already parameterized, flags the Conway-side touches to re-check, and cross-references the separate coinFromGovDeposit re-derivation. Prose only; to be executed in a session with the Agda toolchain so each step can be typechecked. https://claude.ai/code/session_0174ZBS1RKAGSbBXDsESUwoA

Prove `LEDGER-pov` for the Dijkstra LEDGER rule: getCoin s ≡ getCoin s', where getCoin (LedgerState) sums UTxO coin, the rewards balance, the three cert-deposit pots, and the gov-action deposits. Typechecks under --safe with no postulates or holes. Top-down plan: the supporting Certs / UTxO / Gov facts are module parameters of `Ledger.Properties.PoV`, forming the frozen contract for the follow-up PRs (#1186 utxo/utxow, #1210 certs, and a future Gov PoV). New modules: - Ledger/Properties/PoV: LEDGER-pov. The LEDGER-V case is a single LedgerState-level equational chain; direct-deposit value cancels between the UTxO and CertState sides, gov-deposit growth is matched against the produced-side govProposalsDeposits, and `bat'` converts the closed-form batch balance (#1186 shape) to the chain's two-level posPart/negPart deposit form via the batch-cert-deposits-bridge (#1210 shape) and net-arith. - Entities/Properties/PoV: ENTITIES-pov and SUBENTITIES-pov, the value-flow equations for the post-#1256 tx-signal rules. NetworkId and domain facts come from the rules' own premises; the no-truncation bound (withdrawal amount ≤ input-state balance) is an explicit hypothesis — the phantom-withdrawal gap flagged in the #1256 review, provided at the LEDGER level by the ENTITIES/SUBENTITIES-wdrls-bounded parameters. - Entities/Properties/ApplyToRewardsPoV: applyWithdrawals-pov and applyDirectDeposits-pov fold lemmas. Spec changes: - Ledger: getCoin (LedgerState) gains a coinFromGovDeposit summand (gov-action deposits live in GovActionState.deposit, not GState.deposits, yet the UTXO batch balance charges govProposalsDeposits on the produced side). - Certs: getCoin (CertState) is now total (rewards + deposit pots), with coinFromRewards / coinFromDeposits projections. - Prelude: era-independent sum lemmas (+-interleave, sum-map-+). Squash of the pre-rebase branch (13 WIP commits, head f677e1b), rebased onto master and adapted to #1250 (explicit cert deposits, closed-form newCertDeposits/refundCertDeposits), #1253/#1256 (EntitiesEnv, SUBENTITIES, tx-signal ENTITIES), #1262 (legacyMode threading), and #1263/#1265 (UTXOW premise changes). Master absorbed this branch's deposit sign-swap fix in #1250, so it is no longer part of the diff. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Prove `LEDGER-pov` for the Dijkstra LEDGER rule: getCoin s ≡ getCoin s', where getCoin (LedgerState) sums UTxO coin, the rewards balance, the three cert-deposit pots, and the gov-action deposits. Typechecks under --safe with no postulates or holes. Top-down plan: the supporting Certs / UTxO / Gov facts are module parameters of `Ledger.Properties.PoV`, forming the frozen contract for the follow-up PRs (#1186 utxo/utxow, #1210 certs, and a future Gov PoV). New modules: - Ledger/Properties/PoV: LEDGER-pov. The LEDGER-V case is a single LedgerState-level equational chain; direct-deposit value cancels between the UTxO and CertState sides, gov-deposit growth is matched against the produced-side govProposalsDeposits, and `bat'` converts the closed-form batch balance (#1186 shape) to the chain's two-level posPart/negPart deposit form via the batch-cert-deposits-bridge (#1210 shape) and net-arith. - Entities/Properties/PoV: ENTITIES-pov and SUBENTITIES-pov, the value-flow equations for the post-#1256 tx-signal rules. NetworkId and domain facts come from the rules' own premises; the no-truncation bound (withdrawal amount ≤ input-state balance) is an explicit hypothesis — the phantom-withdrawal gap flagged in the #1256 review, provided at the LEDGER level by the ENTITIES/SUBENTITIES-wdrls-bounded parameters. - Entities/Properties/ApplyToRewardsPoV: applyWithdrawals-pov and applyDirectDeposits-pov fold lemmas. Spec changes: - Ledger: getCoin (LedgerState) gains a coinFromGovDeposit summand (gov-action deposits live in GovActionState.deposit, not GState.deposits, yet the UTXO batch balance charges govProposalsDeposits on the produced side). - Certs: getCoin (CertState) is now total (rewards + deposit pots), with coinFromRewards / coinFromDeposits projections. - Prelude: era-independent sum lemmas (+-interleave, sum-map-+). Squash of the pre-rebase branch (13 WIP commits, head f677e1b), rebased onto master and adapted to #1250 (explicit cert deposits, closed-form newCertDeposits/refundCertDeposits), #1253/#1256 (EntitiesEnv, SUBENTITIES, tx-signal ENTITIES), #1262 (legacyMode threading), and deposit sign-swap fix in #1250, so it is no longer part of the diff. AI-assisted: Claude Fable 5 (Anthropic)

Prove `LEDGER-pov` for the Dijkstra LEDGER rule: getCoin s ≡ getCoin s', where getCoin (LedgerState) sums UTxO coin, the rewards balance, the three cert-deposit pots, and the gov-action deposits. Typechecks under --safe with no postulates or holes. Top-down plan: the supporting Certs / UTxO / Gov facts are module parameters of `Ledger.Properties.PoV`, forming the frozen contract for the follow-up PRs (#1186 utxo/utxow, #1210 certs, and a future Gov PoV). New modules: - Ledger/Properties/PoV: LEDGER-pov. The LEDGER-V case is a single LedgerState-level equational chain; direct-deposit value cancels between the UTxO and CertState sides, gov-deposit growth is matched against the produced-side govProposalsDeposits, and `bat'` converts the closed-form batch balance (#1186 shape) to the chain's two-level posPart/negPart deposit form via the batch-cert-deposits-bridge (#1210 shape) and net-arith. - Entities/Properties/PoV: ENTITIES-pov and SUBENTITIES-pov, the value-flow equations for the post-#1256 tx-signal rules. NetworkId and domain facts come from the rules' own premises; the no-truncation bound (withdrawal amount ≤ input-state balance) is an explicit hypothesis — the phantom-withdrawal gap flagged in the #1256 review, provided at the LEDGER level by the ENTITIES/SUBENTITIES-wdrls-bounded parameters. - Entities/Properties/ApplyToRewardsPoV: applyWithdrawals-pov and applyDirectDeposits-pov fold lemmas. Spec changes: - Ledger: getCoin (LedgerState) gains a coinFromGovDeposit summand (gov-action deposits live in GovActionState.deposit, not GState.deposits, yet the UTXO batch balance charges govProposalsDeposits on the produced side). - Certs: getCoin (CertState) is now total (rewards + deposit pots), with coinFromRewards / coinFromDeposits projections. - Prelude: era-independent sum lemmas (+-interleave, sum-map-+). Squash of the pre-rebase branch (13 WIP commits, head f677e1b), rebased onto master and adapted to #1250 (explicit cert deposits, closed-form newCertDeposits/refundCertDeposits), #1253/#1256 (EntitiesEnv, SUBENTITIES, tx-signal ENTITIES), #1262 (legacyMode threading), and deposit sign-swap fix in #1250, so it is no longer part of the diff. AI-assistend development: Claude Fable 5 <noreply@anthropic.com>

Prove `LEDGER-pov` for the Dijkstra LEDGER rule: getCoin s ≡ getCoin s', where getCoin (LedgerState) sums UTxO coin, the rewards balance, the three cert-deposit pots, and the gov-action deposits. Typechecks under --safe with no postulates or holes. Top-down plan: the supporting Certs / UTxO / Gov facts are module parameters of `Ledger.Properties.PoV`, forming the frozen contract for the follow-up PRs (#1186 utxo/utxow, #1210 certs, and a future Gov PoV). New modules: - Ledger/Properties/PoV: LEDGER-pov. The LEDGER-V case is a single LedgerState-level equational chain; direct-deposit value cancels between the UTxO and CertState sides, gov-deposit growth is matched against the produced-side govProposalsDeposits, and `bat'` converts the closed-form batch balance (#1186 shape) to the chain's two-level posPart/negPart deposit form via the batch-cert-deposits-bridge (#1210 shape) and net-arith. - Entities/Properties/PoV: ENTITIES-pov and SUBENTITIES-pov, the value-flow equations for the post-#1256 tx-signal rules. NetworkId and domain facts come from the rules' own premises; the no-truncation bound (withdrawal amount ≤ input-state balance) is an explicit hypothesis — the phantom-withdrawal gap flagged in the #1256 review, provided at the LEDGER level by the ENTITIES/SUBENTITIES-wdrls-bounded parameters. - Entities/Properties/ApplyToRewardsPoV: applyWithdrawals-pov and applyDirectDeposits-pov fold lemmas. Spec changes: - Ledger: getCoin (LedgerState) gains a coinFromGovDeposit summand (gov-action deposits live in GovActionState.deposit, not GState.deposits, yet the UTXO batch balance charges govProposalsDeposits on the produced side). - Certs: getCoin (CertState) is now total (rewards + deposit pots), with coinFromRewards / coinFromDeposits projections. - Prelude: era-independent sum lemmas (+-interleave, sum-map-+). Squash of the pre-rebase branch (13 WIP commits, head f677e1b), rebased onto master and adapted to #1250 (explicit cert deposits, closed-form newCertDeposits/refundCertDeposits), #1253/#1256 (EntitiesEnv, SUBENTITIES, tx-signal ENTITIES), #1262 (legacyMode threading), and deposit sign-swap fix in #1250, so it is no longer part of the diff. AI-assisted: Claude Fable 5 (Anthropic)

Prove `LEDGER-pov` for the Dijkstra LEDGER rule: getCoin s ≡ getCoin s', where getCoin (LedgerState) sums UTxO coin, the rewards balance, the three cert-deposit pots, and the gov-action deposits. Typechecks under --safe with no postulates or holes. Top-down plan: the supporting Certs / UTxO / Gov facts are module parameters of `Ledger.Properties.PoV`, forming the frozen contract for the follow-up PRs (#1186 utxo/utxow, #1210 certs, and a future Gov PoV). New modules: - Ledger/Properties/PoV: LEDGER-pov. The LEDGER-V case is a single LedgerState-level equational chain; direct-deposit value cancels between the UTxO and CertState sides, gov-deposit growth is matched against the produced-side govProposalsDeposits, and `bat'` converts the closed-form batch balance (#1186 shape) to the chain's two-level posPart/negPart deposit form via the batch-cert-deposits-bridge (#1210 shape) and net-arith. - Entities/Properties/PoV: ENTITIES-pov and SUBENTITIES-pov, the value-flow equations for the post-#1256 tx-signal rules. NetworkId and domain facts come from the rules' own premises; the no-truncation bound (withdrawal amount ≤ input-state balance) is an explicit hypothesis — the phantom-withdrawal gap flagged in the #1256 review, provided at the LEDGER level by the ENTITIES/SUBENTITIES-wdrls-bounded parameters. - Entities/Properties/ApplyToRewardsPoV: applyWithdrawals-pov and applyDirectDeposits-pov fold lemmas. Spec changes: - Ledger: getCoin (LedgerState) gains a coinFromGovDeposit summand (gov-action deposits live in GovActionState.deposit, not GState.deposits, yet the UTXO batch balance charges govProposalsDeposits on the produced side). - Certs: getCoin (CertState) is now total (rewards + deposit pots), with coinFromRewards / coinFromDeposits projections. - Prelude: era-independent sum lemmas (+-interleave, sum-map-+). Squash of the pre-rebase branch (13 WIP commits, head f677e1b), rebased onto master and adapted to #1250 (explicit cert deposits, closed-form newCertDeposits/refundCertDeposits), #1253/#1256 (EntitiesEnv, SUBENTITIES, tx-signal ENTITIES), #1262 (legacyMode threading), and deposit sign-swap fix in #1250, so it is no longer part of the diff. AI-assistend development: Claude Fable 5 <noreply@anthropic.com>

Prove `LEDGER-pov` for the Dijkstra LEDGER rule: getCoin s ≡ getCoin s', where getCoin (LedgerState) sums UTxO coin, the rewards balance, the three cert-deposit pots, and the gov-action deposits. Typechecks under --safe with no postulates or holes. Top-down plan: the supporting Certs / UTxO / Gov facts are module parameters of `Ledger.Properties.PoV`, forming the frozen contract for the follow-up PRs (#1186 utxo/utxow, #1210 certs, and a future Gov PoV). New modules: - Ledger/Properties/PoV: LEDGER-pov. The LEDGER-V case is a single LedgerState-level equational chain; direct-deposit value cancels between the UTxO and CertState sides, gov-deposit growth is matched against the produced-side govProposalsDeposits, and `bat'` converts the closed-form batch balance (#1186 shape) to the chain's two-level posPart/negPart deposit form via the batch-cert-deposits-bridge (#1210 shape) and net-arith. - Entities/Properties/PoV: ENTITIES-pov and SUBENTITIES-pov, the value-flow equations for the post-#1256 tx-signal rules. NetworkId and domain facts come from the rules' own premises; the no-truncation bound (withdrawal amount ≤ input-state balance) is an explicit hypothesis — the phantom-withdrawal gap flagged in the #1256 review, provided at the LEDGER level by the ENTITIES/SUBENTITIES-wdrls-bounded parameters. - Entities/Properties/ApplyToRewardsPoV: applyWithdrawals-pov and applyDirectDeposits-pov fold lemmas. Spec changes: - Ledger: getCoin (LedgerState) gains a coinFromGovDeposit summand (gov-action deposits live in GovActionState.deposit, not GState.deposits, yet the UTXO batch balance charges govProposalsDeposits on the produced side). - Certs: getCoin (CertState) is now total (rewards + deposit pots), with coinFromRewards / coinFromDeposits projections. - Prelude: era-independent sum lemmas (+-interleave, sum-map-+). Squash of the pre-rebase branch (13 WIP commits, head f677e1b), rebased onto master and adapted to #1250 (explicit cert deposits, closed-form newCertDeposits/refundCertDeposits), #1253/#1256 (EntitiesEnv, SUBENTITIES, tx-signal ENTITIES), #1262 (legacyMode threading), and deposit sign-swap fix in #1250, so it is no longer part of the diff. AI-assisted: Claude Fable 5 (Anthropic)

Prove `LEDGER-pov` for the Dijkstra LEDGER rule: getCoin s ≡ getCoin s', where getCoin (LedgerState) sums UTxO coin, the rewards balance, the three cert-deposit pots, and the gov-action deposits. Typechecks under --safe with no postulates or holes. Top-down plan: the supporting Certs / UTxO / Gov facts are module parameters of `Ledger.Properties.PoV`, forming the frozen contract for the follow-up PRs (#1186 utxo/utxow, #1210 certs, and a future Gov PoV). New modules: - Ledger/Properties/PoV: LEDGER-pov. The LEDGER-V case is a single LedgerState-level equational chain; direct-deposit value cancels between the UTxO and CertState sides, gov-deposit growth is matched against the produced-side govProposalsDeposits, and `bat'` converts the closed-form batch balance (#1186 shape) to the chain's two-level posPart/negPart deposit form via the batch-cert-deposits-bridge (#1210 shape) and net-arith. - Entities/Properties/PoV: ENTITIES-pov and SUBENTITIES-pov, the value-flow equations for the post-#1256 tx-signal rules. NetworkId and domain facts come from the rules' own premises; the no-truncation bound (withdrawal amount ≤ input-state balance) is an explicit hypothesis — the phantom-withdrawal gap flagged in the #1256 review, provided at the LEDGER level by the ENTITIES/SUBENTITIES-wdrls-bounded parameters. - Entities/Properties/ApplyToRewardsPoV: applyWithdrawals-pov and applyDirectDeposits-pov fold lemmas. Spec changes: - Ledger: getCoin (LedgerState) gains a coinFromGovDeposit summand (gov-action deposits live in GovActionState.deposit, not GState.deposits, yet the UTXO batch balance charges govProposalsDeposits on the produced side). - Certs: getCoin (CertState) is now total (rewards + deposit pots), with coinFromRewards / coinFromDeposits projections. - Prelude: era-independent sum lemmas (+-interleave, sum-map-+). Squash of the pre-rebase branch (13 WIP commits, head f677e1b), rebased onto master and adapted to #1250 (explicit cert deposits, closed-form newCertDeposits/refundCertDeposits), #1253/#1256 (EntitiesEnv, SUBENTITIES, tx-signal ENTITIES), #1262 (legacyMode threading), and deposit sign-swap fix in #1250, so it is no longer part of the diff. AI-assistend development: Claude Fable 5 <noreply@anthropic.com>

…and entry removal Adds getCoin-remove (splitting off a known entry), getCoin-∪⁺-singleton (getCoin (m ∪⁺ ❴ c , d ❵) ≡ getCoin m + d) with its private value-level scaffolding, resᶜ-singleton-∉, ∈-∪⁺-singleton(-∉), ∪⁺-singleton-resᶜ, and dom-∪ˡ-singleton. Consumed by the Dijkstra Certs PoV proofs. AI-assisted development: Claude Fable 5 (Anthropic)

…ters Certs.Properties.PoVLemmas proves the per-CERT-step facts: rewards preservation, closed-form deposit accounting under PoolDepositsRegistered, preservation of that invariant, and the pool-set tracking of the newCertDeposits fold (via seed-certificate shift lemmas, a ∷-split, and ≡ᵉ-congruence in the pool-set argument), plus refundCertDeposits-++. Certs.Properties.PoV lifts these along the reflexive-transitive closure, with statements matching the LEDGER-PoV module parameters verbatim: CERTS-rewards-pov, CERTS-deposits-pov, CERTS-deposits-registered, CERTS-new-thread, refundCertDeposits-++. Adapted to the current Certs spec: PoolEnv is now an epoch-carrying record, the POOL rules carry premise tuples (VRF freshness, reward-account network id, minPoolCost, retirement window), and GOVCERT acts on the whole CertState (DRep deregistration also prunes vote delegations); the per-step case analyses follow the new constructor shapes, and the five exported statements are unchanged. AI-assisted development: Claude Fable 5 (Anthropic)

…heir parameters The five Certs-side obligations (CERTS-rewards-pov, CERTS-deposits-pov, CERTS-deposits-registered, CERTS-new-thread, refundCertDeposits-++) are theorems on this branch, so LEDGER-PoV now imports Certs.Properties.PoV instead of assuming them; the ENTITIES-PoV instantiation consumes the imported facts unchanged. AI-assisted development: Claude Fable 5 (Anthropic)

williamdemeo self-assigned this May 28, 2026

williamdemeo linked an issue May 28, 2026 that may be closed by this pull request

[Dijkstra] Certs PoV #1185

Open

4 tasks

williamdemeo mentioned this pull request May 28, 2026

[Dijkstra] (DEPRECATED) CIP-159-11a: Prove Certs preservation of value (#1185) #1188

Closed

4 tasks

williamdemeo force-pushed the 1185-dijkstra-NEW-ENTITIES-certs-pov branch from dbba0a9 to d09ddaa Compare May 28, 2026 05:03

williamdemeo changed the title ~~[Dijkstra] Certs PoV: per-step coin-form bridge and RTC lift (#1185)~~ [Dijkstra] CIP-159-11a: Certs PoV (per-step coin bridge + RTC lift) (#1185) May 28, 2026

williamdemeo force-pushed the 1185-dijkstra-NEW-ENTITIES-certs-pov branch from d09ddaa to 09a5de0 Compare May 28, 2026 05:34

williamdemeo force-pushed the 1185-dijkstra-NEW-ENTITIES-certs-pov branch from 09a5de0 to fca589f Compare June 15, 2026 22:41

williamdemeo mentioned this pull request Jun 16, 2026

[Dijkstra] CIP-159-11c: Prove LEDGER preservation of value (#1187) #1203

Merged

4 tasks

williamdemeo mentioned this pull request Jun 23, 2026

[Dijkstra] LEDGER-pov: complete the proof — gov re-derivation; Certs/Utxo/Utxow facts as parameters #1223

Merged

4 tasks

williamdemeo changed the title ~~[Dijkstra] CIP-159-11a: Certs PoV (per-step coin bridge + RTC lift) (#1185)~~ WIP -- [Dijkstra] CIP-159-11a: Certs PoV (per-step coin bridge + RTC lift) (#1185) Jun 23, 2026

This was referenced Jul 29, 2026

[Dijkstra] CIP-159-11b: Prove UTxO and UTxOW preservation of value (#1186) #1189

Open

[Dijkstra] Rewire LEDGER-pov to consume the proved PoV modules and drop the discharged parameters #1277

Open

williamdemeo assigned carlostome and unassigned williamdemeo Jul 29, 2026

williamdemeo unassigned carlostome Aug 5, 2026

williamdemeo force-pushed the 1185-dijkstra-NEW-ENTITIES-certs-pov branch from fca589f to 614d902 Compare August 5, 2026 07:09

williamdemeo changed the title ~~WIP -- [Dijkstra] CIP-159-11a: Certs PoV (per-step coin bridge + RTC lift) (#1185)~~ [Dijkstra] CIP-159-11a: Prove CERTS preservation of value (#1185) Aug 5, 2026

williamdemeo changed the base branch from master to 1187-dijkstra-NEW-ENTITIES-ledger-pov August 5, 2026 07:09

williamdemeo force-pushed the 1185-dijkstra-NEW-ENTITIES-certs-pov branch from 614d902 to a5f86e2 Compare August 6, 2026 00:51

williamdemeo mentioned this pull request Aug 6, 2026

[Dijkstra] Certs PoV #1185

Open

4 tasks

Base automatically changed from 1187-dijkstra-NEW-ENTITIES-ledger-pov to master September 4, 2026 03:21

williamdemeo changed the base branch from master to 1186-dijkstra-NEW-ENTITIES-utxo-utxow-pov September 8, 2026 19:16

williamdemeo changed the base branch from 1186-dijkstra-NEW-ENTITIES-utxo-utxow-pov to master September 8, 2026 19:17

williamdemeo force-pushed the 1185-dijkstra-NEW-ENTITIES-certs-pov branch from 0e600f0 to a5d4885 Compare September 8, 2026 19:17

williamdemeo changed the base branch from master to 1186-dijkstra-utxo-and-utxow-pov September 8, 2026 19:19

williamdemeo force-pushed the 1185-dijkstra-NEW-ENTITIES-certs-pov branch from a5d4885 to c9aca5b Compare September 8, 2026 20:20

williamdemeo force-pushed the 1185-dijkstra-NEW-ENTITIES-certs-pov branch from c9aca5b to f481664 Compare September 8, 2026 21:16

williamdemeo force-pushed the 1185-dijkstra-NEW-ENTITIES-certs-pov branch from ade1172 to e8318ec Compare September 8, 2026 22:47

williamdemeo mentioned this pull request Sep 8, 2026

WIP -- [Dijkstra] CIP-159: Prove Gov preservation-of-value facts (#1276) #1278

Draft

4 tasks

williamdemeo force-pushed the 1185-dijkstra-NEW-ENTITIES-certs-pov branch 2 times, most recently from 8d3fbd8 to 7ed36a1 Compare September 9, 2026 02:26

williamdemeo added 4 commits September 9, 2026 14:01

update properties catalog and dashboard

f1098fe

Navigation Menu

Uh oh!

WIP -- [Dijkstra] CIP-159-11a: Prove CERTS preservation of value (#1185) - #1210

WIP -- [Dijkstra] CIP-159-11a: Prove CERTS preservation of value (#1185)#1210
williamdemeo wants to merge 4 commits into
1186-dijkstra-utxo-and-utxow-povfrom
1185-dijkstra-NEW-ENTITIES-certs-pov

williamdemeo commented May 28, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

williamdemeo commented May 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Description

What lands

Key points for review

Verification

Checklist

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

williamdemeo commented May 28, 2026 •

edited

Loading