Skip to content

Add batch-level coin mint constraint to prevent Ada forgery #1023

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 6 commits into from
Jan 9, 2026
Merged

Add batch-level coin mint constraint to prevent Ada forgery #1023

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
f69f9f9
improvements
williamdemeo Jan 9, 2026
12d68c1
Initial plan
Copilot Jan 9, 2026
d8a8668
Add batchMintedCoin constraint to prevent Ada forgery
Copilot Jan 9, 2026
e417de8
Add documentation for batchMintedCoin security constraint
Copilot Jan 9, 2026
4b65e66
Use consistent aggregation syntax for batchMintedCoin
Copilot Jan 9, 2026
ffb6f06
bugfix
williamdemeo Jan 9, 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
12 changes: 0 additions & 12 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 @@ -414,18 +414,6 @@ could be either of them.
HasReferenceInputs-Tx : HasReferenceInputs (Tx txLevel)
HasReferenceInputs-Tx .ReferenceInputsOf = ReferenceInputsOf ∘ TxBodyOf

HasSpendInputs-TxBody : HasSpendInputs (TxBody txLevel)
HasSpendInputs-TxBody .SpendInputsOf = TxBody.txIns

HasSpendInputs-Tx : HasSpendInputs (Tx txLevel)
HasSpendInputs-Tx .SpendInputsOf = SpendInputsOf ∘ TxBodyOf

HasReferenceInputs-TxBody : HasReferenceInputs (TxBody txLevel)
HasReferenceInputs-TxBody .ReferenceInputsOf = TxBody.refInputs

HasReferenceInputs-Tx : HasReferenceInputs (Tx txLevel)
HasReferenceInputs-Tx .ReferenceInputsOf = ReferenceInputsOf ∘ TxBodyOf

HasIndexedOutputs-TxBody : HasIndexedOutputs (TxBody txLevel)
HasIndexedOutputs-TxBody .IndexedOutputsOf = TxBody.txOuts

Expand Down
12 changes: 12 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
Expand Up @@ -346,6 +346,12 @@ module _ (Γ : UTxOEnv) (s : UTxOState) where
batchPOV : Type
batchPOV = batchConsumed ≡ batchProduced

-- Total Ada minted across the entire batch (top-level tx + all sub-txs).
-- This must equal 0 to prevent Ada forgery and maintain the total Ada supply invariant.
-- Analogous to Conway's `coin mint ≡ 0` constraint, but generalized to batches.
batchMintedCoin : Coin
batchMintedCoin = coin (MintedValueOf txTop) + sum (map (λ txSub → coin (MintedValueOf txSub)) (SubTransactionsOf txTop))



module Batch (Γ : UTxOEnv) (s : UTxOState) (txTop : TopLevelTx) where
Expand Down Expand Up @@ -398,13 +404,18 @@ module Batch (Γ : UTxOEnv) (s : UTxOState) (txTop : TopLevelTx) where

## The <span class="AgdaDatatype">UTXOS</span> Rule


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

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

UTXO-scripts✓ :
Expand All @@ -414,6 +425,7 @@ data _⊢_⇀⦇_,UTXOS⦈_ : UTxOEnv → UTxOState → TopLevelTx → UTxOState
∙ Tx.isValid tx ≡ batchScripts✓ Γ s tx
∙ batchScripts✓ Γ s tx ≡ true
∙ batchPOV Γ s tx
∙ batchMintedCoin Γ s tx ≡ 0
────────────────────────────────
Γ ⊢ s ⇀⦇ tx ,UTXOS⦈ s'-scripts✓

Expand Down