Specify protected addresses and Receiving authorization in Dijkstra

[colll78]

Summary

Add proposed CIP-160 output-creation authorization to the Dijkstra executable model. Each protected Plutus output has a separate Receiving purpose with its original body-local index and resolved TxOut; identical outputs retain distinct executions, redeemers and budgets.

body ordinary output map
  protected keys/native scripts -> existing authorization/witness pools
  protected Plutus output at i  -> Receive(i, resolved output)
                                  pointer (Receive, i)
                                  its own redeemer + execution budget

Key/ordinary/native outputs do not renumber Plutus indexes. Parent and child purposes, redeemers and contexts remain independent; every declared invocation budget contributes to aggregate fees and transaction/block limits. Existing witness/reference-script availability is shared, while a newly created output cannot authorize itself through its own reference script.

Protection participates in address equality. Conway rejects protected outputs; proposed Dijkstra admission begins at protocol major 12 in each body. Supported contexts preserve protection, and legacy languages reject it where visible. Receiving introduces no implicit datum. Protected collateral returns always fail phase 1; accepted phase-2-invalid batches preserve ordinary inputs, create no ordinary outputs and apply only top-level collateral/return/fee effects.

This also fixes existing model discrepancies exposed by composed integration: hard-fork enactment synchronizes the authoritative and stored protocol-parameter versions while preserving update-chain identity; Leios selection includes registered zero-stake pools and enumerates each semantic pool ID once, even when multiple accounts delegate to it, without changing positive-stake fractional weights, ranking or pool-ID tie breaks. One committee seat per selected pool is separate from Receiving, which requires one execution per protected Plutus output. Companion ledger translation independently reconstructs committee pool IDs from snapshot ranking and checks weight, honored key and real proof-of-possession with actual runtime Globals, including key-age context.

CIP160.md documents model/API boundaries. This accompanies the Plutus V4 proposal and CIP-160/CIP-19 amendment. Per-output execution is our implementation decision, supported by CIP-160's per-output validation rule and lehins's resolved-TxOut comment. Exact raw indexes, Data fields and activation remain proposals requiring upstream review; those sources do not establish approval of every implementation detail.

Evidence

• Before: protected creation identity and Receiving do not exist in the model; collateral-return representation is insufficient for invalid-batch comparisons, stored parameters retain a stale hard-fork version, registered zero-stake pools are omitted from selection, and multiple delegators can duplicate a pool in committee enumeration.
  After: source rules define independent indexed authorization and collateral effects, synchronize hard-fork version state, retain registered zero-stake identities and select each semantic pool ID once. Regression assertions cover exact resulting states and committee selection boundaries.
• Signed and published source 87072fed43a085bbbaaeb5888a7792ec5f8a164a passes complete Agda specification/proof closure, historical examples/interface checks, the 39-entry property scanner and genuine signed-source Shake extraction. GHC compiled the actual extracted public API and passed 73/73 persistent runtime assertions: 56 Receiving, four hard-fork and 13 Leios, including four new composed-epoch single/split/equal-delegator and top-K checks.
• Published development artifact b747be78f6e001d41395974251cf0b42f45b68c4 contains 789 generated files, independently matched byte-for-byte to the extraction. Manifest SHA-256: 8d0d123d8eb3728884ad272c00f18169c1244fe43563df18af28d813c41ff535. Generated Haskell was not edited; Cabal/Nix pin the published artifact.
• The full ledger Dijkstra suite passes 1152 examples, zero failures and two inherited pending cases, with source/dependency equivalence receipts establishing applicability to the current ledger checkpoint. Full ledger API passes 291/0 (including Receiving 5/0); focused Receiving 63/0, independent interoperability 4/0, shared suite 58 examples / zero failures / five inherited pending cases. Plutus passes 450 public API and six compiled-plugin tests, with all five remote checks green; repeated genuine fixture generation is identical and preserves all 41 existing V1–V3 fixtures. Receiving benchmark smoke passes every 16/256/4096-output group and paired setup equality, without a statistical timing claim.
• Fresh strict integrated conformance compilation and the full conformance suite pass: 1263 examples, zero failures and 28 inherited pending cases, in 1773.8447 seconds (seed 2023, -N2) at ledger 77d85ec1dd18b548977ee9126b63d3d6d4e47f97 and artifact b747be78f6e001d41395974251cf0b42f45b68c4. All 1287 compiled Haskell/Cabal source hashes are unchanged, and the pending-case sequence matches the baseline. All four committee-selection failures are resolved by semantic pool-ID enumeration; the ledger's independently ranked adapter remains strict. Concrete execution results are separate from abstract model assertions.
• Evaluator limits remain explicit: the foreign evaluator uses the declared validity flag, contexts are abstract, values are Coin-only, and fees/integrity/size callbacks are abstracted. Structural conformance does not prove UPLC/context-byte correctness, datum/business rules, asset-level collateral equality or exact predicate-failure payloads. Concrete ledger tests provide those complementary checks. Foreign Leios globals fix key age at four epochs; arbitrary network-global agreement and endorser-block size are outside that premise.

Development source/artifact: 87072fed43a085bbbaaeb5888a7792ec5f8a164a / b747be78f6e001d41395974251cf0b42f45b68c4. Both are signed and published; integrated conformance passes. Upstream acceptance and artifact publication remain pending.

Checklist

• Model semantics and compatibility boundaries documented.
• Preservation properties and runtime regressions added or updated.
• Final source diff self-review and property dashboard verification complete.
• Tested final source passes full proof closure, historical examples and genuine extraction.
• All 73 persistent extracted runtime assertions pass.
• Final signed-source release extraction and checksum-verified development artifact publication complete.
• Matching full ledger conformance passes.
• Upstream artifact publication complete.

Merge Danger

Door: one-way after activation

Changes address and transaction representations in the extracted API. Activation requires coordinated agreement; matching ledger translation must consume the generated revision.

Blast Radius: Dijkstra

Shared address examples/translations must retain ordinary protection as false. The existing ledger CI gate requires the final generated dependency to be an ancestor of upstream master-artifacts; fork publication and local extraction/runtime passes alone cannot satisfy it.

[lehins]

Closing for the same reason: IntersectMBO/cardano-ledger#6153 (comment)

[colll78]

Kept protocol-parameter versions synchronized during hard forks; corrected committee eligibility for registered zero-stake versus unregistered pools; prevented duplicate committee seats; fixed execution-budget "≥" comparison that actually tested equality.

The above issues are unrelated to CIP-160 and probably should be reviewed as they are issues with the existing formalization.