[Dijkstra] phase 1 requiredTopLevelGuards
#1010
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
5 tasks
4 tasks
4 tasks
williamdemeo
commented
Jan 5, 2026
williamdemeo
changed the base branch from
master
to
1001-dijkstra-subtxbody-redesign
williamdemeo
changed the title
requiredTopLevelGuards (stacked PR)requiredTopLevelGuards
williamdemeo
force-pushed
the
1001-dijkstra-subtxbody-redesign
branch
from
c5accc8 to
3c15d84
Compare
williamdemeo
force-pushed
the
1002-dijkstra-phase-1-requiredtoplevelguards-stacked
branch
from
29516cc to
2ba8844
Compare
williamdemeo
force-pushed
the
1001-dijkstra-subtxbody-redesign
branch
from
b0d5934 to
1b1144b
Compare
williamdemeo
force-pushed
the
1002-dijkstra-phase-1-requiredtoplevelguards-stacked
branch
from
deeb8ad to
df6879c
Compare
williamdemeo
force-pushed
the
1001-dijkstra-subtxbody-redesign
branch
from
1b1144b to
05daaae
Compare
williamdemeo
force-pushed
the
1002-dijkstra-phase-1-requiredtoplevelguards-stacked
branch
2 times, most recently
from
43ce03e to
ec362bc
Compare
williamdemeo
force-pushed
the
1001-dijkstra-subtxbody-redesign
branch
from
42b6d12 to
1ab3ec6
Compare
williamdemeo
force-pushed
the
1002-dijkstra-phase-1-requiredtoplevelguards-stacked
branch
from
ec362bc to
5a88696
Compare
carlostome
approved these changes
Jan 8, 2026
Collaborator
carlostome
left a comment
carlostome
left a comment
There was a problem hiding this comment.
LGTM! I left a minor comment that we can address later on if necessary
Comment on lines
+494
to
+501
| -- Phase-1 condition (CIP-0118): | ||
| -- every credential required by a subTx body must appear in the top-level txGuards set. | ||
| requiredTopLevelGuardsSatisfied : TopLevelTx → List SubLevelTx → Type | ||
| requiredTopLevelGuardsSatisfied topTx subTxs = requiredCreds ⊆ TxBody.txGuards (TxBodyOf topTx) | ||
| where | ||
| concatMapˡ : {A B : Type} → (A → ℙ B) → List A → ℙ B | ||
| concatMapˡ f as = proj₁ $ unions (fromList (map f as)) | ||
| -- (maybe move concatMapˡ to src-lib-exts or agda-sets) |
Collaborator
There was a problem hiding this comment.
Maybe this simple condition can be inlined somehow in the rule?
+ a minimal `UTXOS` rule as a stub/hook (so `UTXO` can call something), + a minimal `UTXO` rule with just the new phase-1 premise (plus an explicit "calls UTXOS"), + a minimal `UTXOW`; just a wrapper over `UTXO` for now.
williamdemeo
force-pushed
the
1002-dijkstra-phase-1-requiredtoplevelguards-stacked
branch
from
5a88696 to
2dbea3f
Compare
github-project-automation
bot
moved this from In Progress
to Done
in Dijkstra formal spec
williamdemeo
deleted the
1002-dijkstra-phase-1-requiredtoplevelguards-stacked
branch
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Description
Stacked PR. The branch for this PR should be rebased on master once #1009 is merged.
This PR closes issue #1002 by introducing a predicate for testing that required top-level guards are present among the top-level guards and
UTXOSrule as a stub/hook (soUTXOcan call something),UTXOrule with just the new phase-1 premise (plus an explicit "calls UTXOS"),UTXOW; just a wrapper overUTXOfor now.Copilot-generated Description (manually reviewed and revised)
This pull request introduces minimal "skeleton" modules for the Dijkstra-era UTxO and UTxOW transition systems, setting up the structure for future development of phase-1 checks and witnessing logic. It also adds a phase-1 structural check (CIP-0118) to ensure that all credentials required by subtransactions are present in the top-level transaction. The changes include new files, imports, and some refactoring of helper functions to support these checks.
New Dijkstra UTxO and UTxOW skeleton modules:
src/Ledger/Dijkstra/Specification/Utxo.lagda.mdas a minimal skeleton for the Dijkstra UTxO transition system, including the new phase-1 structural check (requiredTopLevelGuardsSatisfied) to enforce that all subTx-required credentials are present in the top-level transaction.src/Ledger/Dijkstra/Specification/Utxow.lagda.mdas a minimal skeleton for the Dijkstra witnessing layer, currently acting as a wrapper around UTxO with no additional premises.Phase-1 structural check and helper refactoring:
src/Ledger/Dijkstra/Specification/Transaction.lagda.md, refactored and added helper functions (subTxTaggedGuards,subTxGuardCredentials) and implemented therequiredTopLevelGuardsSatisfiedcondition for phase-1 validation.Documentation and import updates:
src/Ledger/Dijkstra/Specification.lagda.md..mdextensions. [1] [2]Checklist
CHANGELOG.md