Add batch-level coin mint constraint to prevent Ada forgery #1023
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
7 tasks
Copilot
AI
changed the title
[WIP] Address feedback on UTXOS rule with batch-level validity checking
Add batch-level coin mint constraint to prevent Ada forgery
Jan 9, 2026
williamdemeo
force-pushed
the
1007-dijkstra-utxos-batch-level-validity
branch
from
e43ee89 to
4f543af
Compare
Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com>
Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com>
Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com>
williamdemeo
force-pushed
the
copilot/sub-pr-1021
branch
from
b879849 to
4b65e66
Compare
williamdemeo
merged commit 03fc211
into
1007-dijkstra-utxos-batch-level-validity
1 check passed
williamdemeo
added a commit
that referenced
this pull request
Jan 9, 2026
* improvements * Initial plan * Add batchMintedCoin constraint to prevent Ada forgery Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> * Add documentation for batchMintedCoin security constraint Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> * Use consistent aggregation syntax for batchMintedCoin Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> --------- Co-authored-by: William DeMeo <williamdemeo@gmail.com> Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com>
williamdemeo
added a commit
that referenced
this pull request
Jan 9, 2026
* improvements * Initial plan * Add batchMintedCoin constraint to prevent Ada forgery Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> * Add documentation for batchMintedCoin security constraint Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> * Use consistent aggregation syntax for batchMintedCoin Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> --------- Co-authored-by: William DeMeo <williamdemeo@gmail.com> Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com>
williamdemeo
added a commit
that referenced
this pull request
Jan 10, 2026
* improvements * Initial plan * Add batchMintedCoin constraint to prevent Ada forgery Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> * Add documentation for batchMintedCoin security constraint Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> * Use consistent aggregation syntax for batchMintedCoin Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> --------- Co-authored-by: William DeMeo <williamdemeo@gmail.com> Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com>
williamdemeo
added a commit
that referenced
this pull request
Jan 12, 2026
* improvements * Initial plan * Add batchMintedCoin constraint to prevent Ada forgery Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> * Add documentation for batchMintedCoin security constraint Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> * Use consistent aggregation syntax for batchMintedCoin Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> --------- Co-authored-by: William DeMeo <williamdemeo@gmail.com> Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com>
williamdemeo
added a commit
that referenced
this pull request
Jan 13, 2026
* improvements * Initial plan * Add batchMintedCoin constraint to prevent Ada forgery Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> * Add documentation for batchMintedCoin security constraint Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> * Use consistent aggregation syntax for batchMintedCoin Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> --------- Co-authored-by: William DeMeo <williamdemeo@gmail.com> Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com>
williamdemeo
added a commit
that referenced
this pull request
Jan 16, 2026
* improvements * Initial plan * Add batchMintedCoin constraint to prevent Ada forgery Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> * Add documentation for batchMintedCoin security constraint Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> * Use consistent aggregation syntax for batchMintedCoin Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> --------- Co-authored-by: William DeMeo <williamdemeo@gmail.com> Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com>
williamdemeo
added a commit
that referenced
this pull request
Jan 19, 2026
* improvements * Initial plan * Add batchMintedCoin constraint to prevent Ada forgery Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> * Add documentation for batchMintedCoin security constraint Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> * Use consistent aggregation syntax for batchMintedCoin Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> --------- Co-authored-by: William DeMeo <williamdemeo@gmail.com> Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com>
williamdemeo
added a commit
that referenced
this pull request
Jan 24, 2026
* improvements * Initial plan * Add batchMintedCoin constraint to prevent Ada forgery Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> * Add documentation for batchMintedCoin security constraint Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> * Use consistent aggregation syntax for batchMintedCoin Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> --------- Co-authored-by: William DeMeo <williamdemeo@gmail.com> Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com>
williamdemeo
pushed a commit
that referenced
this pull request
Jan 24, 2026
+ Initial plan and improvements + Add batchMintedCoin constraint to prevent Ada forgery + Add documentation for batchMintedCoin security constraint + Use consistent aggregation syntax for batchMintedCoin Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> --------- Co-authored-by: William DeMeo <williamdemeo@gmail.com> Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> remove duplicate typeclass instance address PR change requests fix UTXOS and UTXO rules
williamdemeo
added a commit
that referenced
this pull request
Jan 27, 2026
+ Add batch-level coin mint constraint to prevent Ada forgery (#1023) + Initial plan and improvements + Add batchMintedCoin constraint to prevent Ada forgery + Add documentation for batchMintedCoin security constraint + Use consistent aggregation syntax for batchMintedCoin Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> --------- Co-authored-by: William DeMeo <williamdemeo@gmail.com> Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> remove duplicate typeclass instance address PR change requests fix UTXOS and UTXO rules Update src/Ledger/Dijkstra/Specification/Utxo.lagda.md Co-authored-by: Carlos Tomé Cortiñas <carlos.tome-cortinas@iohk.io>
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.
The Dijkstra UTXOS rule's preservation-of-value check (
batchPOV) allows Ada forgery: an attacker can mint Ada inMintedValueOf, create matching outputs, and pass validation despite increasing total Ada supply.Changes
Added
batchMintedCoinfunction: Computes total Ada minted across top-level transaction and all sub-transactions by extracting and summing coin components fromMintedValueOfvaluesAdded constraint to UTXO-scripts✓ rule:
batchMintedCoin Γ s tx ≡ 0enforces zero net Ada minting across the batch, analogous to Conway'scoin mint ≡ 0but generalized for batch semanticsThis prevents the forgery attack while preserving the batch-level preservation-of-value semantics.
💬 We'd love your input! Share your thoughts on Copilot coding agent in our 2 minute survey.