Skip to content

[Dijkstra] CIP-159-05: Update UTxO for direct deposits and balance intervals (#1117) #1160

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

Open
williamdemeo wants to merge 2 commits into
base: master
Choose a base branch
from
+67 −24
Open

[Dijkstra] CIP-159-05: Update UTxO for direct deposits and balance intervals (#1117) #1160

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
389d947
[Dijkstra] CIP-159-05: Update UTxO rules for direct deposits and bala…
williamdemeo Apr 11, 2026
5a93035
Address PR review change request.
williamdemeo Apr 24, 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
22 changes: 14 additions & 8 deletions src/Ledger/Dijkstra/Specification/Ledger.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,7 @@ record SubLedgerEnv : Type where
utxo₀ : UTxO
isTopLevelValid : Bool
allScripts : ℙ Script
accountBalances : Rewards

record LedgerEnv : Type where
field
Expand Down Expand Up @@ -78,6 +79,10 @@ instance

HasTreasury-SubLedgerEnv : HasTreasury SubLedgerEnv
HasTreasury-SubLedgerEnv .TreasuryOf = SubLedgerEnv.treasury

HasAccountBalances-SubLedgerEnv : HasAccountBalances SubLedgerEnv
HasAccountBalances-SubLedgerEnv .AccountBalancesOf = SubLedgerEnv.accountBalances

```
-->
```agda
Expand Down Expand Up @@ -213,6 +218,7 @@ private variable
treasury : Treasury
isTopLevelValid : Bool
allScripts : ℙ Script
accountBalances : Rewards
```
-->

Expand Down Expand Up @@ -279,17 +285,17 @@ data _⊢_⇀⦇_,SUBLEDGER⦈_ : SubLedgerEnv → LedgerState → SubLevelTx

SUBLEDGER-V :
∙ isTopLevelValid ≡ true
∙ ⟦ slot , pp , treasury , utxo₀ , isTopLevelValid , allScripts ⟧ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₁
∙ ⟦ slot , pp , treasury , utxo₀ , isTopLevelValid , allScripts , accountBalances ⟧ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₁
∙ ⟦ epoch slot , pp , ListOfGovVotesOf stx , WithdrawalsOf stx , allColdCreds govState₀ enactState ⟧ ⊢ certState₀ ⇀⦇ DCertsOf stx ,CERTS⦈ certState₁
∙ ⟦ TxIdOf stx , epoch slot , pp , ppolicy , enactState , certState₁ , dom (RewardsOf certState₁) ⟧ ⊢ govState₀ ⇀⦇ GovProposals+Votes stx ,GOVS⦈ govState₁
────────────────────────────────
⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , isTopLevelValid , allScripts ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState₁ , govState₁ , certState₁ ⟧
⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , isTopLevelValid , allScripts , accountBalances ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState₁ , govState₁ , certState₁ ⟧

SUBLEDGER-I :
∙ isTopLevelValid ≡ false
∙ ⟦ slot , pp , treasury , utxo₀ , isTopLevelValid , allScripts ⟧ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₀
∙ ⟦ slot , pp , treasury , utxo₀ , isTopLevelValid , allScripts , accountBalances ⟧ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₀
────────────────────────────────
⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , isTopLevelValid , allScripts ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState₀ , govState₀ , certState₀ ⟧
⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , isTopLevelValid , allScripts , accountBalances ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState₀ , govState₀ , certState₀ ⟧

_⊢_⇀⦇_,SUBLEDGERS⦈_ : SubLedgerEnv → LedgerState → List SubLevelTx → LedgerState → Type
_⊢_⇀⦇_,SUBLEDGERS⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,SUBLEDGER⦈_}
Expand All @@ -308,10 +314,10 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LedgerState → TopLevelTx → Ledg
depositsChange = calculateDepositsChange certState₀ certState₁ certState₂
in
∙ IsValidFlagOf tx ≡ true
∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , IsValidFlagOf tx , allScripts ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoState₁ , govState₁ , certState₁ ⟧
∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , IsValidFlagOf tx , allScripts , RewardsOf certState₀ ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoState₁ , govState₁ , certState₁ ⟧
∙ ⟦ epoch slot , pp , ListOfGovVotesOf tx , WithdrawalsOf tx , allColdCreds govState₁ enactState ⟧ ⊢ certState₁ ⇀⦇ DCertsOf tx ,CERTS⦈ certState₂
∙ ⟦ TxIdOf tx , epoch slot , pp , ppolicy , enactState , certState₂ , dom (RewardsOf certState₂) ⟧ ⊢ govState₁ ⇀⦇ GovProposals+Votes tx ,GOVS⦈ govState₂
∙ ⟦ slot , pp , treasury , utxo₀ , depositsChange , allScripts ⟧ ⊢ utxoState₁ ⇀⦇ tx ,UTXOW⦈ utxoState₂
∙ ⟦ slot , pp , treasury , utxo₀ , depositsChange , allScripts , RewardsOf certState₀ ⟧ ⊢ utxoState₁ ⇀⦇ tx ,UTXOW⦈ utxoState₂
────────────────────────────────
⟦ slot , ppolicy , pp , enactState , treasury ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ tx ,LEDGER⦈ ⟦ utxoState₂ , rmOrphanDRepVotes certState₂ govState₂ , certState₂ ⟧

Expand All @@ -324,8 +330,8 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LedgerState → TopLevelTx → Ledg
allScripts = getAllScripts tx utxo₀
in
∙ IsValidFlagOf tx ≡ false
∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , IsValidFlagOf tx , allScripts ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoState₀ , govState₀ , certState₀ ⟧
∙ ⟦ slot , pp , treasury , utxo₀ , ⟦ 0ℤ , 0ℤ ⟧ , allScripts ⟧ ⊢ utxoState₀ ⇀⦇ tx ,UTXOW⦈ utxoState₁
∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , IsValidFlagOf tx , allScripts , RewardsOf certState₀ ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoState₀ , govState₀ , certState₀ ⟧
∙ ⟦ slot , pp , treasury , utxo₀ , ⟦ 0ℤ , 0ℤ ⟧ , allScripts , RewardsOf certState₀ ⟧ ⊢ utxoState₀ ⇀⦇ tx ,UTXOW⦈ utxoState₁
────────────────────────────────
⟦ slot , ppolicy , pp , enactState , treasury ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ tx ,LEDGER⦈ ⟦ utxoState₁ , govState₀ , certState₀ ⟧

Expand Down
13 changes: 8 additions & 5 deletions src/Ledger/Dijkstra/Specification/Ledger/Properties/Computational.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -92,7 +92,7 @@ instance

-- Helper env constructors (avoid `let ... in with ...` parse issues)
subUtxoΓ : SubLedgerEnv → SubUTxOEnv
subUtxoΓ Γ = ⟦ slot , pparams , treasury , utxo₀ , isTopLevelValid , allScripts ⟧
subUtxoΓ Γ = ⟦ slot , pparams , treasury , utxo₀ , isTopLevelValid , allScripts , accountBalances ⟧
where open SubLedgerEnv Γ

certΓ : SubLedgerEnv → LedgerState → SubLevelTx → CertEnv
Expand All @@ -117,7 +117,7 @@ instance
let open SubLedgerEnv Γ
open LedgerState s
subUtxoΓ : SubUTxOEnv
subUtxoΓ = ⟦ slot , pparams , treasury , utxo₀ , isTopLevelValid , allScripts ⟧
subUtxoΓ = ⟦ slot , pparams , treasury , utxo₀ , isTopLevelValid , allScripts , accountBalances ⟧
certΓ : CertEnv
certΓ = ⟦ epoch slot , pparams , ListOfGovVotesOf stx , WithdrawalsOf stx
, allColdCreds govSt enactState ⟧
Expand All @@ -140,7 +140,7 @@ instance
isI : isTopLevelValid ≡ false
isI = ¬-not ¬isV
subUtxoΓ : SubUTxOEnv
subUtxoΓ = ⟦ slot , pparams , treasury , utxo₀ , isTopLevelValid , allScripts ⟧
subUtxoΓ = ⟦ slot , pparams , treasury , utxo₀ , isTopLevelValid , allScripts , accountBalances ⟧
in case computeSubutxow subUtxoΓ utxoSt stx of λ where
(failure e) → failure e
(success (utxoSt' , utxoStep)) →
Expand Down Expand Up @@ -225,6 +225,7 @@ instance
, utxo₀Of s
, IsValidFlagOf tx
, allScriptsOf tx s
, RewardsOf (CertStateOf s)
⟧

certΓOf : LedgerEnv → TopLevelTx → GovState → CertEnv
Expand Down Expand Up @@ -256,6 +257,7 @@ instance
, utxo₀Of s
, depositsChange
, allScriptsOf tx s
, RewardsOf (CertStateOf s)
⟧

utxoΓ-invalid : LedgerEnv → LedgerState → TopLevelTx → UTxOEnv
Expand All @@ -266,6 +268,7 @@ instance
, utxo₀Of s
, ⟦ 0ℤ , 0ℤ ⟧
, allScriptsOf tx s
, RewardsOf (CertStateOf s)
⟧
```
-->
Expand All @@ -286,7 +289,7 @@ instance
allScripts = getAllScripts txTop utxo₀
subΓ : SubLedgerEnv
subΓ = ⟦ slot , ppolicy , pparams , enactState , treasury
, utxo₀ , IsValidFlagOf txTop , allScripts ⟧
, utxo₀ , IsValidFlagOf txTop , allScripts , RewardsOf certState ⟧
in
case IsValidFlagOf txTop ≟ true of λ where
(yes isV) →
Expand All @@ -313,7 +316,7 @@ instance
depositsChange : DepositsChange
depositsChange = calculateDepositsChange certState₀ certState₁ certSt₂
utxoΓ : UTxOEnv
utxoΓ = ⟦ slot , pparams , treasury , utxo₀ , depositsChange , allScripts ⟧
utxoΓ = ⟦ slot , pparams , treasury , utxo₀ , depositsChange , allScripts , RewardsOf certState ⟧
in
-- UTXOW must run from the post-SUBLEDGERS UTxOState (utxoSt₁)
computeUtxow utxoΓ utxoSt₁ txTop >>= λ where
Expand Down
40 changes: 37 additions & 3 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 @@ -82,6 +82,7 @@ record UTxOEnv : Type where
utxo₀ : UTxO
depositsChange : DepositsChange
allScripts : ℙ Script
accountBalances : Rewards

record SubUTxOEnv : Type where
field
Expand All @@ -91,6 +92,7 @@ record SubUTxOEnv : Type where
utxo₀ : UTxO
isTopLevelValid : Bool
allScripts : ℙ Script
accountBalances : Rewards
```

The `UTxOEnv`{.AgdaRecord} carries
Expand Down Expand Up @@ -147,6 +149,10 @@ record HasDataPool {a} (A : Type a) : Type a where
field DataPoolOf : A → DataHash ⇀ Datum
open HasDataPool ⦃...⦄ public

record HasAccountBalances {a} (A : Type a) : Type a where
field AccountBalancesOf : A → Rewards
open HasAccountBalances ⦃...⦄ public

record HasSlot {a} (A : Type a) : Type a where
field SlotOf : A → Slot
open HasSlot ⦃...⦄ public
Expand All @@ -170,6 +176,9 @@ instance
HasScriptPool-UTxOEnv : HasScriptPool UTxOEnv
HasScriptPool-UTxOEnv .ScriptPoolOf = UTxOEnv.allScripts

HasAccountBalances-UTxOEnv : HasAccountBalances UTxOEnv
HasAccountBalances-UTxOEnv .AccountBalancesOf = UTxOEnv.accountBalances

HasSlot-SubUTxOEnv : HasSlot SubUTxOEnv
HasSlot-SubUTxOEnv .SlotOf = SubUTxOEnv.slot

Expand All @@ -188,6 +197,9 @@ instance
HasScriptPool-SubUTxOEnv : HasScriptPool SubUTxOEnv
HasScriptPool-SubUTxOEnv .ScriptPoolOf = SubUTxOEnv.allScripts

HasAccountBalances-SubUTxOEnv : HasAccountBalances SubUTxOEnv
HasAccountBalances-SubUTxOEnv .AccountBalancesOf = SubUTxOEnv.accountBalances

HasUTxO-UTxOState : HasUTxO UTxOState
HasUTxO-UTxOState .UTxOOf = UTxOState.utxo

Expand Down Expand Up @@ -319,9 +331,19 @@ module _ (depositsChange : DepositsChange) where
consumedBatch txTop utxo = consumed txTop utxo
+ ∑ˡ[ stx ← SubTransactionsOf txTop ] (consumedTx stx utxo)
+ inject depositRefundsSub
```

Direct deposits represent value that flows from the transaction into account
addresses. In the preservation-of-value equation, direct deposits appear on the
*produced* side: value leaves the UTxO and enters account balances. The
`getCoin (DirectDepositsOf tx)` term sums the ADA of all direct deposits in
the transaction.

```agda
producedTx : Tx ℓ → Value
producedTx tx = balance (outs tx) + inject (DonationsOf tx)
producedTx tx = balance (outs tx)
+ inject (DonationsOf tx)
+ inject (getCoin (DirectDepositsOf tx))

produced : TopLevelTx → Value
produced txTop = producedTx txTop
Expand Down Expand Up @@ -422,6 +444,12 @@ The [CIP][1] states:
words, spending inputs across all top- and sub-level transactions
are disjoint.

4. Direct deposit targets must be registered accounts (their credentials
must appear in `dom accountBalances`).

5. Each balance interval assertion must hold against the pre-batch account
balances; this is a Phase-1 validity condition.

```agda
data _⊢_⇀⦇_,SUBUTXO⦈_ : SubUTxOEnv → UTxOState → SubLevelTx → UTxOState → Type where

Expand All @@ -444,6 +472,9 @@ data _⊢_⇀⦇_,SUBUTXO⦈_ : SubUTxOEnv → UTxOState → SubLevelTx → UTxO
∙ ∀[ a ∈ dom (WithdrawalsOf txSub)] (NetworkIdOf a ≡ NetworkId)
∙ MaybeNetworkIdOf txSub ~ just NetworkId
∙ CurrentTreasuryOf txSub ~ just (TreasuryOf Γ)
∙ dom (DirectDepositsOf txSub) ⊆ dom (AccountBalancesOf Γ)
∙ ∀[ (c , interval) ∈ BalanceIntervalsOf txSub ˢ ]
c ∈ dom (AccountBalancesOf Γ ˢ) × InBalanceInterval (maybe id 0 (lookupᵐ? (AccountBalancesOf Γ) c)) interval
Comment on lines +476 to +477
Copy link
Copy Markdown
Collaborator

@carlostome carlostome Apr 24, 2026

Choose a reason for hiding this comment

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

In hindsight, maybe it'd be clearer (given the other precondition above) to add a separate precondition:

    ∙ dom (BalanceIntervalsOf txSub) ⊆ dom (AccountBalancesOf Γ)

────────────────────────────────
let
s₁ = if IsTopLevelValidFlagOf Γ
Expand Down Expand Up @@ -503,6 +534,9 @@ data _⊢_⇀⦇_,UTXO⦈_ : UTxOEnv × Bool → UTxOState → TopLevelTx → UT
∙ ∀[ a ∈ dom (WithdrawalsOf txTop)] NetworkIdOf a ≡ NetworkId
∙ MaybeNetworkIdOf txTop ~ just NetworkId
∙ CurrentTreasuryOf txTop ~ just (TreasuryOf Γ)
∙ dom (DirectDepositsOf txTop) ⊆ dom (AccountBalancesOf Γ)
∙ ∀[ (c , interval) ∈ BalanceIntervalsOf txTop ˢ ]
InBalanceInterval (maybe id 0 (lookupᵐ? (AccountBalancesOf Γ) c)) interval
∙ Γ ⊢ _ ⇀⦇ txTop ,UTXOS⦈ _
────────────────────────────────
let
Expand All @@ -515,8 +549,8 @@ data _⊢_⇀⦇_,UTXO⦈_ : UTxOEnv × Bool → UTxOState → TopLevelTx → UT
<!--
```agda
unquoteDecl UTXO-premises = genPremises UTXO-premises (quote UTXO)
pattern UTXO-⋯ p₀ p₁ p₂ p₃ p₄ p₅ p₆ p₇ p₈ p₉ p₁₀ p₁₁ p₁₂ p₁₃ p₁₄ p₁₅ p₁₆ p₁₇ p₁₈ h
= UTXO (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , p₁₇ , p₁₈ , h)
pattern UTXO-⋯ p₀ p₁ p₂ p₃ p₄ p₅ p₆ p₇ p₈ p₉ p₁₀ p₁₁ p₁₂ p₁₃ p₁₄ p₁₅ p₁₆ p₁₇ p₁₈ p₁₉ p₂₀ h
= UTXO (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , p₁₇ , p₁₈ , p₁₉ , p₂₀ , h)
```
-->

Expand Down
16 changes: 8 additions & 8 deletions src/Ledger/Dijkstra/Specification/Utxo/Properties/Computational.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -130,30 +130,30 @@ instance
... | false | [ refl ]
with H?
... | (no ¬p) = failure "UTXO" -- (genErrors ¬p)
... | yes (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , p₁₇ , p₁₈)
... | yes (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , p₁₇ , p₁₈ , p₁₉ , p₂₀)
with UTXOS.computeProof (Γ,legacyMode .proj₁) tt txTop
... | success h = success (-, UTXO (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , p₁₇ , p₁₈ , proj₂ h))
... | success h = success (-, UTXO (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , p₁₇ , p₁₈ , p₁₉ , p₂₀ , proj₂ h))
... | failure ¬h = failure "UTXOS"
computeProof | true | [ refl ]
with H?
... | (no ¬p) = failure "UTXO" -- (genErrors ¬p)
... | yes (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , p₁₇ , p₁₈)
... | yes (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , p₁₇ , p₁₈ , p₁₉ , p₂₀)
with UTXOS.computeProof (Γ,legacyMode .proj₁) tt txTop
... | success h = success (-, UTXO (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , p₁₇ , p₁₈ , proj₂ h))
... | success h = success (-, UTXO (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , p₁₇ , p₁₈ , p₁₉ , p₂₀ , proj₂ h))
... | failure ¬h = failure "UTXOS"

completeness : ∀ s₁ → Γ,legacyMode ⊢ s₀ ⇀⦇ txTop ,UTXO⦈ s₁ → map proj₁ computeProof ≡ success s₁
completeness s₁ (UTXO-⋯ p₀ p₁ p₂ p₃ p₄ p₅ p₆ p₇ p₈ p₉ p₁₀ p₁₁ p₁₂ p₁₃ p₁₄ p₁₅ p₁₆ p₁₇ p₁₈ h)
completeness s₁ (UTXO-⋯ p₀ p₁ p₂ p₃ p₄ p₅ p₆ p₇ p₈ p₉ p₁₀ p₁₁ p₁₂ p₁₃ p₁₄ p₁₅ p₁₆ p₁₇ p₁₈ p₁₉ p₂₀ h)
with IsValidFlagOf txTop | inspect IsValidFlagOf txTop
... | false | [ refl ]
with H?
... | no ¬p = ⊥-elim (¬p ((p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , p₁₇ , p₁₈)))
... | no ¬p = ⊥-elim (¬p ((p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , p₁₇ , p₁₈ , p₁₉ , p₂₀)))
... | yes _
with UTXOS.computeProof (Γ,legacyMode .proj₁) tt txTop | UTXOS.completeness _ _ _ _ h
... | success h | refl = refl
completeness s₁ (UTXO-⋯ p₀ p₁ p₂ p₃ p₄ p₅ p₆ p₇ p₈ p₉ p₁₀ p₁₁ p₁₂ p₁₃ p₁₄ p₁₅ p₁₆ p₁₇ p₁₈ h) | true | [ refl ]
completeness s₁ (UTXO-⋯ p₀ p₁ p₂ p₃ p₄ p₅ p₆ p₇ p₈ p₉ p₁₀ p₁₁ p₁₂ p₁₃ p₁₄ p₁₅ p₁₆ p₁₇ p₁₈ p₁₉ p₂₀ h) | true | [ refl ]
with H?
... | no ¬p = ⊥-elim (¬p ((p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , p₁₇ , p₁₈)))
... | no ¬p = ⊥-elim (¬p ((p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , p₁₇ , p₁₈ , p₁₉ , p₂₀)))
... | yes _
with UTXOS.computeProof (Γ,legacyMode .proj₁) tt txTop | UTXOS.completeness _ _ _ _ h
... | success h | refl = refl
Expand Down
Loading