Skip to content

[Dijkstra] phase 1 requiredTopLevelGuards #1010

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
williamdemeo merged 4 commits into from
Jan 8, 2026
+184 −3
Merged

[Dijkstra] phase 1 requiredTopLevelGuards #1010

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
1dcf4d1
Add `requiredTopLevelGuardsSatisfied` predicate.
williamdemeo Dec 21, 2025
f2588ff
Add initial versions of Utxo and Utxow modules
williamdemeo Dec 21, 2025
ae423c8
rename and fix some guard functions
williamdemeo Jan 7, 2026
2dbea3f
correct code comment
williamdemeo Jan 7, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions src/Ledger/Conway/Specification/Utxo.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,8 @@
---
source_branch: master
source_path: src/Ledger/Conway/Specification/Utxo.lagda.md
---

# UTxO {#sec:utxo}

The UTxO transition system is built up from a number of smaller parts defined in this
Expand Down
2 changes: 1 addition & 1 deletion src/Ledger/Conway/Specification/Utxow.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
---
source_branch: master
source_path: src/Ledger/Conway/Specification/Utxow.lagda
source_path: src/Ledger/Conway/Specification/Utxow.lagda.md
---

# Witnessing {#sec:witnessing}
Expand Down
12 changes: 12 additions & 0 deletions src/Ledger/Dijkstra/Specification.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -63,3 +63,15 @@ import Ledger.Dijkstra.Specification.TokenAlgebra.Base
```agda
import Ledger.Dijkstra.Specification.Transaction
```

## <span class="AgdaModule">Utxo</span>

```agda
import Ledger.Dijkstra.Specification.Utxo
```

## <span class="AgdaModule">Utxow</span>

```agda
import Ledger.Dijkstra.Specification.Utxow
```
20 changes: 18 additions & 2 deletions src/Ledger/Dijkstra/Specification/Transaction.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -482,10 +482,26 @@ remaining helper functions of this section.
... | yes _ = (c , (tid , md) ∷ xs) ∷ rest
... | no _ = (c , xs) ∷ insertGuard (tid , cred , md) rest

subTxTopLevelGuards : SubLevelTx → ℙ TaggedTopLevelGuard
subTxTopLevelGuards subtx =
subTxTaggedGuards : SubLevelTx → ℙ TaggedTopLevelGuard
subTxTaggedGuards subtx =
mapˢ (λ (cred , md) → (TxIdOf subtx , cred , md))
(TxBody.txRequiredTopLevelGuards (TxBodyOf subtx))

-- Turn a subTx body's `txRequiredTopLevelGuards` into a set of guard credentials.
subTxGuardCredentials : SubLevelTx → ℙ Credential
subTxGuardCredentials = (mapˢ proj₁) ∘ (TxBody.txRequiredTopLevelGuards ∘ TxBodyOf)

-- 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)
Comment on lines +494 to +501
Copy link
Collaborator

@carlostome carlostome Jan 8, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe this simple condition can be inlined somehow in the rule?


requiredCreds : ℙ Credential
requiredCreds = concatMapˡ subTxGuardCredentials subTxs
```

## Changes to Transaction Validity
Expand Down
103 changes: 103 additions & 0 deletions src/Ledger/Dijkstra/Specification/Utxo.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,103 @@
---
source_branch: master
source_path: src/Ledger/Dijkstra/Specification/Utxo.lagda.md
---

# UTxO

(Dijkstra skeleton)

This is a **minimal skeleton** of the Dijkstra-era UTxO transition system.

It exists primarily to host **phase-1 structural checks** that are specific to
Dijkstra (CIP-0118 / CIP-0112), without yet committing to the full batch semantics
(issue #1007) or phase-2 execution model (issue #1006).

<!--
```agda
{-# OPTIONS --safe #-}

open import Ledger.Prelude
open import Ledger.Dijkstra.Specification.Abstract
open import Ledger.Dijkstra.Specification.Transaction

module Ledger.Dijkstra.Specification.Utxo
(txs : _) (open TransactionStructure txs)
(abs : AbstractFunctions txs) (open AbstractFunctions abs)
where

open import Ledger.Dijkstra.Specification.Certs govStructure
open import Ledger.Dijkstra.Specification.Script.Validation txs abs
```
-->

## Environments and states

(copied shape from Conway; semantics TBD)

```agda
record UTxOEnv : Type where
field
slot : Slot
pparams : PParams
treasury : Treasury

record UTxOState : Type where
field
utxo : UTxO
fees : Fees
deposits : Deposits
donations : Donations
```

<!--
```agda
private variable
Γ : UTxOEnv
s s' : UTxOState
tx : TopLevelTx
```
-->

## UTXOS

(skeleton/stub)

`UTXOS` will eventually process the batch (top-level tx + its subTxs) and handle
phase-2 success/failure behavior. For now it is merely a hook point.

```agda
data _⊢_⇀⦇_,UTXOS⦈_ : UTxOEnv → UTxOState → TopLevelTx → UTxOState → Type where
UTXOS-stub :
────────────────────────────────
Γ ⊢ s ⇀⦇ tx ,UTXOS⦈ s
```

## UTXO

(skeleton with the new phase-1 check)

This is the intended home of Dijkstra "phase-1 structural checks."

```agda
data _⊢_⇀⦇_,UTXO⦈_ : UTxOEnv → UTxOState → TopLevelTx → UTxOState → Type where

UTXO-inductive :
let txb = Tx.txBody tx
subTxs = TxBody.txSubTransactions txb
in
∙ requiredTopLevelGuardsSatisfied tx subTxs
∙ Γ ⊢ s ⇀⦇ tx ,UTXOS⦈ s'
────────────────────────────────
Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s'
```

**Note.** The premise `requiredTopLevelGuardsSatisfied tx subTxs`
is explicitly a **phase-1** condition (CIP-0118): every guard credential requested by
subTx bodies must appear in the top-level `txGuards` set.

A couple of details to notice:

- `txb` is computed via `Tx.txBody tx` (no reliance on `TxBodyOf` instances).
- `UTXOS-stub` returns the **same** state (so we can typecheck
everything without inventing semantics prematurely).
45 changes: 45 additions & 0 deletions src/Ledger/Dijkstra/Specification/Utxow.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
---
source_branch: master
source_path: src/Ledger/Dijkstra/Specification/Utxow.lagda.md
---

# UTxOW (Dijkstra skeleton)

This is a **minimal skeleton** of the Dijkstra-era witnessing layer.

It currently acts as a wrapper around `UTXO`, mirroring Conway's shape, but without
committing to full witnessing checks yet.

<!--
```agda
{-# OPTIONS --safe #-}

open import Ledger.Prelude
open import Ledger.Dijkstra.Specification.Abstract
open import Ledger.Dijkstra.Specification.Transaction

module Ledger.Dijkstra.Specification.Utxow
(txs : _) (open TransactionStructure txs)
(abs : AbstractFunctions txs) (open AbstractFunctions abs)
where

open import Ledger.Dijkstra.Specification.Utxo txs abs

private variable
Γ : UTxOEnv
s s' : UTxOState
tx : TopLevelTx
```
-->

```agda
data _⊢_⇀⦇_,UTXOW⦈_ : UTxOEnv → UTxOState → TopLevelTx → UTxOState → Type where

UTXOW-inductive :
∙ Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s'
────────────────────────────────
Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s'
```

This file intentionally contains **no** additional premises yet. As Dijkstra witnessing
evolves, this is where signature / script / datum / language constraints can be added.