Skip to content

Commit

Permalink
Remove constructor from UTxOState
Browse files Browse the repository at this point in the history
  • Loading branch information
@carlostome
carlostome committed Jan 29, 2025
1 parent 93aa91c commit b08b87f
Show file tree
Hide file tree
Showing 10 changed files with 63 additions and 48 deletions.
7 changes: 4 additions & 3 deletions src/Ledger/Conway/Conformance/Epoch.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -97,7 +97,7 @@ applyRUpd : RewardUpdate → EpochState → EpochState
applyRUpd ⟦ Δt , Δr , Δf , rs ⟧ʳᵘ
⟦ ⟦ treasury , reserves ⟧ᵃ
, ss
, ⟦ ⟦ utxo , fees , deposits , donations ⟧ᵘ
, ⟦ utxoSt
, govSt
, ⟦ ⟦ voteDelegs , stakeDelegs , rewards , dDeposits ⟧ᵈ , pState , gState ⟧ᶜˢ ⟧ˡ
, es
Expand All @@ -106,12 +106,13 @@ applyRUpd ⟦ Δt , Δr , Δf , rs ⟧ʳᵘ
⟦ ⟦ posPart (ℤ.+ treasury ℤ.+ Δt ℤ.+ ℤ.+ unregRU')
, posPart (ℤ.+ reserves ℤ.+ Δr) ⟧ᵃ
, ss
, ⟦ ⟦ utxo , posPart (ℤ.+ fees ℤ.+ Δf) , deposits , donations ⟧ᵘ
, ⟦ ⟦ utxo , posPart (ℤ.+ fees ℤ.+ Δf) , deposits , donations ⟧
, govSt
, ⟦ ⟦ voteDelegs , stakeDelegs , rewards ∪⁺ regRU , dDeposits ⟧ᵈ , pState , gState ⟧ᶜˢ ⟧ˡ
, es
, fut ⟧ᵉ'
where
open UTxOState utxoSt
regRU = rs ∣ dom rewards
unregRU = rs ∣ dom rewards ᶜ
unregRU' = ∑[ x ← unregRU ] x
Expand Down Expand Up @@ -177,7 +178,7 @@ data _⊢_⇀⦇_,EPOCH⦈_ : ⊤ → EpochState → Epoch → EpochState → Ty
⟧ᵛ
⟧ᶜˢ

utxoSt' = ⟦ utxoSt .utxo , utxoSt .fees , utxoSt .deposits ∣ mapˢ (proj₁ ∘ proj₂) removedGovActions ᶜ , 0 ⟧ᵘ
utxoSt' = ⟦ utxoSt .utxo , utxoSt .fees , utxoSt .deposits ∣ mapˢ (proj₁ ∘ proj₂) removedGovActions ᶜ , 0 ⟧

acnt' = record acnt
{ treasury = acnt .treasury ∸ totWithdrawals + utxoSt .donations + unclaimed }
Expand Down
6 changes: 3 additions & 3 deletions src/Ledger/Conway/Conformance/Equivalence.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -148,7 +148,7 @@ instance
ledger' : Γ C.⊢ (getCertDeps* cdeposits ⊢conv s) ⇀⦇ tx ,LEDGER⦈ C.⟦ utxoStC' , govSt' , certStateC' ⟧ˡ
ledger' = C.LEDGER-V⋯ refl utxow' certs' gov'
utxoEq : utxoStC' ≡ utxoSt'
utxoEq = cong (λ • → L.⟦ _ , _ , • , _ ⟧ᵘ)
utxoEq = cong (λ • → ⟦ _ , _ , • , _ ⟧)
(lemUpdateDeposits refl utxow)
ddeps = getCertDeps* cdeposits .proj₁
gdeps = getCertDeps* cdeposits .proj₂
Expand All @@ -160,7 +160,7 @@ instance
-- LEDGERToConf {Γ} {s} {tx} {s'} .convⁱ (cdeps , cdeps-eq) r@(L.LEDGER-I⋯ refl utxow) =
LEDGERToConf {Γ} {s} {tx} {s'} .convⁱ _ r@(L.LEDGER-I⋯ refl utxow) =
certDeposits s , lem-cert-deposits-invalid refl r ,
subst (λ • → Γ C.⊢ _ ⊢conv s ⇀⦇ tx ,LEDGER⦈ C.⟦ C.⟦ _ , _ , • , _ ⟧ᵘ , _ , _ ⟧ˡ)
subst (λ • → Γ C.⊢ _ ⊢conv s ⇀⦇ tx ,LEDGER⦈ C.⟦ ⟦ _ , _ , • , _ ⟧ , _ , _ ⟧ˡ)
(lemInvalidDepositsL refl utxow)
(C.LEDGER-I⋯ refl (conv utxow))

Expand Down Expand Up @@ -248,7 +248,7 @@ instance
utxow' = inj₂ valid-deps ⊢conv utxow

eqUtxo : setDeposits (utxowDeposits utxow) utxoSt' ≡ utxoSt'
eqUtxo = cong (λ • → L.⟦ _ , _ , • , _ ⟧ᵘ) (lemUtxowDeposits refl utxow)
eqUtxo = cong (λ • → ⟦ _ , _ , • , _ ⟧) (lemUtxowDeposits refl utxow)

ledger' : Γ L.⊢ conv s ⇀⦇ tx ,LEDGER⦈ L.⟦ setDeposits (utxowDeposits utxow) utxoSt'
, govSt'
Expand Down
4 changes: 2 additions & 2 deletions src/Ledger/Conway/Conformance/Equivalence/Utxo.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,10 +20,10 @@ module Ledger.Conway.Conformance.Equivalence.Utxo
open import Ledger.Conway.Conformance.Equivalence.Base txs abs

setDeposits : L.Deposits → L.UTxOState → L.UTxOState
setDeposits deposits L.⟦ utxo , fees , _ , donations ⟧ᵘ = L.⟦ utxo , fees , deposits , donations ⟧ᵘ
setDeposits deposits utxoSt = record utxoSt { deposits = deposits }

withDepositsFrom : L.UTxOState → L.UTxOState → L.UTxOState
withDepositsFrom L.⟦ _ , _ , deposits , _ ⟧ᵘ = setDeposits deposits
withDepositsFrom utxoSt = setDeposits (L.UTxOState.deposits utxoSt)

instance

Expand Down
6 changes: 3 additions & 3 deletions src/Ledger/Conway/Conformance/Utxo.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ open PParams
instance
_ = +-0-monoid

open L public using (UTxOEnv; UTxOState; ⟦_,_,_,_⟧ᵘ)
open L public using (UTxOEnv; UTxOState)

private variable
Γ : UTxOEnv
Expand All @@ -56,7 +56,7 @@ data _⊢_⇀⦇_,UTXOS⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Typ
, fees + txfee
, deposits
, donations + txdonation
⟧ᵘ
⟧

Scripts-No :
∀ {Γ} {s} {tx}
Expand All @@ -72,7 +72,7 @@ data _⊢_⇀⦇_,UTXOS⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Typ
, fees + L.cbalance (utxo ∣ collateral)
, deposits
, donations
⟧ᵘ
⟧

unquoteDecl Scripts-Yes-premises = genPremises Scripts-Yes-premises (quote Scripts-Yes)
unquoteDecl Scripts-No-premises = genPremises Scripts-No-premises (quote Scripts-No)
Expand Down
7 changes: 4 additions & 3 deletions src/Ledger/Epoch.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -126,7 +126,7 @@ applyRUpd : RewardUpdate → EpochState → EpochState
applyRUpd ⟦ Δt , Δr , Δf , rs ⟧ʳᵘ
⟦ ⟦ treasury , reserves ⟧ᵃ
, ss
, ⟦ ⟦ utxo , fees , deposits , donations ⟧ᵘ
, ⟦ utxoSt
, govSt
, ⟦ stᵈ , pState , gState ⟧ᶜˢ ⟧ˡ
, es
Expand All @@ -135,12 +135,13 @@ applyRUpd ⟦ Δt , Δr , Δf , rs ⟧ʳᵘ
⟦ ⟦ posPart (ℤ.+ treasury ℤ.+ Δt ℤ.+ ℤ.+ unregRU')
, posPart (ℤ.+ reserves ℤ.+ Δr) ⟧ᵃ
, ss
, ⟦ ⟦ utxo , posPart (ℤ.+ fees ℤ.+ Δf) , deposits , donations ⟧ᵘ
, ⟦ ⟦ utxo , posPart (ℤ.+ fees ℤ.+ Δf) , deposits , donations ⟧
, govSt
, ⟦ ⟦ voteDelegs , stakeDelegs , rewards ∪⁺ regRU ⟧ , pState , gState ⟧ᶜˢ ⟧ˡ
, es
, fut ⟧ᵉ'
where
open UTxOState utxoSt
open DState stᵈ
regRU = rs ∣ dom rewards
unregRU = rs ∣ dom rewards ᶜ
Expand Down Expand Up @@ -255,7 +256,7 @@ its results by carrying out each of the following tasks.
, ⟦ (if null govSt' then mapValues (1 +_) (gState .dreps) else (gState .dreps))
, (gState .ccHotKeys) ∣ ccCreds (es .cc) ⟧ ⟧ᶜˢ

utxoSt' = ⟦ utxoSt .utxo , utxoSt .fees , utxoSt .deposits ∣ mapˢ (proj₁ ∘ proj₂) removedGovActions ᶜ , 0 ⟧ᵘ
utxoSt' = ⟦ utxoSt .utxo , utxoSt .fees , utxoSt .deposits ∣ mapˢ (proj₁ ∘ proj₂) removedGovActions ᶜ , 0 ⟧

acnt' = record acnt
{ treasury = acnt .treasury ∸ totWithdrawals + utxoSt .donations + unclaimed }
Expand Down
24 changes: 14 additions & 10 deletions src/Ledger/Ledger/Properties.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -156,16 +156,20 @@ module _
getCoin utxoSt' + getCoin certState'
∎

LEDGER-pov s@{s = ⟦ ⟦ utxo , fees , deposits , donations ⟧ᵘ , govSt , ⟦ dState , pState , gState ⟧ᶜˢ ⟧ˡ}
s'@{s' = ⟦ ⟦ utxo' , fees' , deposits' , donations' ⟧ᵘ , govSt' , ⟦ dState' , pState' , gState' ⟧ᶜˢ ⟧ˡ}
h (LEDGER-I {utxoSt' = utxoSt'} (invalid , UTXOW⇒UTXO st)) = cong (_+ rewardsBalance dState)
LEDGER-pov s@{s = ⟦ utxoSt , govSt , ⟦ dState , pState , gState ⟧ᶜˢ ⟧ˡ}
s'@{s' = ⟦ utxoSt' , govSt' , ⟦ dState' , pState' , gState' ⟧ᶜˢ ⟧ˡ}
h (LEDGER-I {utxoSt' = utxoSt''} (invalid , UTXOW⇒UTXO st)) =
let open UTxOState utxoSt
open UTxOState utxoSt' renaming (utxo to utxo'; fees to fees'
; deposits to deposits'; donations to donations') in
cong (_+ rewardsBalance dState)
( begin
getCoin ⟦ utxo , fees , deposits , donations ⟧ᵘ
≡˘⟨ +-identityʳ (getCoin ⟦ utxo , fees , deposits , donations ⟧ᵘ) ⟩
getCoin ⟦ utxo , fees , deposits , donations ⟧ᵘ + 0
≡˘⟨ cong (λ x → getCoin ⟦ utxo , fees , deposits , donations ⟧ᵘ + φ(getCoin txwdrls , x)) invalid ⟩
getCoin ⟦ utxo , fees , deposits , donations ⟧ᵘ + φ(getCoin txwdrls , isValid) ≡⟨ pov h st ⟩
getCoin ⟦ utxo' , fees' , deposits' , donations' ⟧ᵘ ∎ )
getCoin ⟦ utxo , fees , deposits , donations ⟧
≡˘⟨ +-identityʳ (getCoin ⟦ utxo , fees , deposits , donations ⟧) ⟩
getCoin ⟦ utxo , fees , deposits , donations ⟧ + 0
≡˘⟨ cong (λ x → getCoin ⟦ utxo , fees , deposits , donations ⟧ + φ(getCoin txwdrls , x)) invalid ⟩
getCoin ⟦ utxo , fees , deposits , donations ⟧ + φ(getCoin txwdrls , isValid) ≡⟨ pov h st ⟩
getCoin ⟦ utxo' , fees' , deposits' , donations' ⟧ ∎ )
where open ≡-Reasoning


Expand Down Expand Up @@ -542,7 +546,7 @@ module SetoidProperties (tx : Tx) (Γ : LEnv) (s : LState) where
LEDGER-govDepsMatch (LEDGER-I⋯ refl (UTXOW-UTXOS (Scripts-No _))) aprioriMatch = aprioriMatch

LEDGER-govDepsMatch s'@{⟦ .(⟦ ((UTxOState.utxo (LState.utxoSt s) ∣ txins ᶜ) ∪ˡ (outs txb))
, _ , updateDeposits pp txb (UTxOState.deposits (LState.utxoSt s)) , _ ⟧ᵘ)
, _ , updateDeposits pp txb (UTxOState.deposits (LState.utxoSt s)) , _ ⟧)
, govSt' , certState' ⟧ˡ}
utxosts@(LEDGER-V⋯ tx-valid (UTXOW-UTXOS (Scripts-Yes x)) _ GOV-sts) aprioriMatch = begin
filterˢ isGADeposit (dom (updateDeposits pp txb utxoDeps))
Expand Down
13 changes: 10 additions & 3 deletions src/Ledger/Utxo.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,8 @@ open import Ledger.ScriptValidation txs abs
open import Ledger.Fees txs using (scriptsCost)
open import Ledger.Certs govStructure

open import Data.Product.Nary.NonDependent using (uncurryₙ)

instance
_ = +-0-monoid

Expand Down Expand Up @@ -163,7 +165,6 @@ record UTxOEnv : Type where
record UTxOState : Type where
\end{code}
\begin{code}[hide]
constructor ⟦_,_,_,_⟧ᵘ
field
\end{code}
\begin{code}
Expand All @@ -172,6 +173,12 @@ record UTxOState : Type where
deposits : Deposits
donations : Coin
\end{code}
\begin{code}[hide]
instance
ToRecord-UTxOState : ToRecord (UTxO × Coin × Deposits × Coin) UTxOState
ToRecord-UTxOState = record { ⟦_⟧ = uncurryₙ 4 λ z z₁ z₂ z₃ →
record { utxo = z ; fees = z₁ ; deposits = z₂ ; donations = z₃ } }
\end{code}
\begin{NoConway}
\emph{UTxO transitions}

Expand Down Expand Up @@ -486,7 +493,7 @@ data _⊢_⇀⦇_,UTXOS⦈_ where
∙ evalScripts tx sLst ≡ isValid
∙ isValid ≡ true
────────────────────────────────
Γ ⊢ s ⇀⦇ tx ,UTXOS⦈ ⟦ (utxo ∣ txins ᶜ) ∪ˡ (outs txb) , fees + txfee , updateDeposits pp txb deposits , donations + txdonation ⟧ᵘ
Γ ⊢ s ⇀⦇ tx ,UTXOS⦈ ⟦ (utxo ∣ txins ᶜ) ∪ˡ (outs txb) , fees + txfee , updateDeposits pp txb deposits , donations + txdonation ⟧

Scripts-No :
∀ {Γ} {s} {tx}
Expand All @@ -498,7 +505,7 @@ data _⊢_⇀⦇_,UTXOS⦈_ where
∙ evalScripts tx sLst ≡ isValid
∙ isValid ≡ false
────────────────────────────────
Γ ⊢ s ⇀⦇ tx ,UTXOS⦈ ⟦ utxo ∣ collateral ᶜ , fees + cbalance (utxo ∣ collateral) , deposits , donations ⟧ᵘ
Γ ⊢ s ⇀⦇ tx ,UTXOS⦈ ⟦ utxo ∣ collateral ᶜ , fees + cbalance (utxo ∣ collateral) , deposits , donations ⟧
\end{code}
\caption{UTXOS rule}
\label{fig:utxos-conway}
Expand Down
30 changes: 15 additions & 15 deletions src/Ledger/Utxo/Properties.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -287,15 +287,15 @@ module DepositHelpers
{donations donations' : Coin}
{tx : Tx} (let open Tx tx renaming (body to txb); open TxBody txb)
{Γ : UTxOEnv}
(step : Γ ⊢ ⟦ utxo , fees , deposits , donations ⟧ᵘ ⇀⦇ tx ,UTXO⦈
⟦ utxo' , fees' , deposits' , donations' ⟧ᵘ)
(step : Γ ⊢ ⟦ utxo , fees , deposits , donations ⟧ ⇀⦇ tx ,UTXO⦈
⟦ utxo' , fees' , deposits' , donations' ⟧)
(h' : txid ∉ mapˢ proj₁ (dom utxo))
where
open Tactic.EquationalReasoning.≡-Reasoning {A = ℕ} (solve-macro (quoteTerm +-0-monoid))

private
stepS : Γ ⊢ ⟦ utxo , fees , deposits , donations ⟧ᵘ ⇀⦇ tx ,UTXOS⦈
⟦ utxo' , fees' , deposits' , donations' ⟧ᵘ
stepS : Γ ⊢ ⟦ utxo , fees , deposits , donations ⟧ ⇀⦇ tx ,UTXOS⦈
⟦ utxo' , fees' , deposits' , donations' ⟧
stepS = case step of λ where
(UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ h) → h

Expand All @@ -308,22 +308,22 @@ module DepositHelpers
Δdep : ℤ
Δdep = depositsChange pp txb deposits
utxoSt : UTxOState
utxoSt = ⟦ utxo , fees , deposits , donations ⟧ᵘ
utxoSt = ⟦ utxo , fees , deposits , donations ⟧
ref tot : Coin
ref = depositRefunds pp utxoSt txb
wdls = getCoin txwdrls
tot = newDeposits pp utxoSt txb
h : disjoint (dom (utxo ∣ txins ᶜ)) (dom (outs txb))
h = λ h₁ h₂ → ∉-∅ $ proj₁ (newTxid⇒disj {txb} {utxo} h')
$ to ∈-∩ (res-comp-domᵐ h₁ , h₂)
newBal' : Γ ⊢ ⟦ utxo , fees , deposits , donations ⟧ᵘ ⇀⦇ tx ,UTXO⦈
⟦ utxo' , fees' , deposits' , donations' ⟧ᵘ
newBal' : Γ ⊢ ⟦ utxo , fees , deposits , donations ⟧ ⇀⦇ tx ,UTXO⦈
⟦ utxo' , fees' , deposits' , donations' ⟧
→ consumed pp utxoSt txb ≡ produced pp utxoSt txb
newBal' (UTXO-inductive⋯ _ _ _ _ _ _ _ _ x _ _ _ _ _ _ _ _ _ _ _) = x
newBal : consumed pp utxoSt txb ≡ produced pp utxoSt txb
newBal = newBal' step
noMintAda' : Γ ⊢ ⟦ utxo , fees , deposits , donations ⟧ᵘ ⇀⦇ tx ,UTXO⦈
⟦ utxo' , fees' , deposits' , donations' ⟧ᵘ
noMintAda' : Γ ⊢ ⟦ utxo , fees , deposits , donations ⟧ ⇀⦇ tx ,UTXO⦈
⟦ utxo' , fees' , deposits' , donations' ⟧
→ coin (mint) ≡ 0
noMintAda' (UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ x _ _ _ _ _ _ _ _ _ _) = x
noMintAda : coin mint ≡ 0
Expand Down Expand Up @@ -565,17 +565,17 @@ and
→
\end{code}
\begin{code}
Γ ⊢ ⟦ utxo , fees , deposits , donations ⟧ᵘ ⇀⦇ tx ,UTXO⦈
⟦ utxo' , fees' , deposits' , donations' ⟧ᵘ
Γ ⊢ ⟦ utxo , fees , deposits , donations ⟧ ⇀⦇ tx ,UTXO⦈
⟦ utxo' , fees' , deposits' , donations' ⟧
\end{code}

then
\begin{code}[hide]
→
\end{code}
\begin{code}
getCoin ⟦ utxo , fees , deposits , donations ⟧ᵘ + φ(getCoin txwdrls , isValid)
≡ getCoin ⟦ utxo' , fees' , deposits' , donations' ⟧ᵘ
getCoin ⟦ utxo , fees , deposits , donations ⟧ + φ(getCoin txwdrls , isValid)
≡ getCoin ⟦ utxo' , fees' , deposits' , donations' ⟧
\end{code}
\begin{code}[hide]
pov {deposits' = deposits'} h'
Expand Down Expand Up @@ -691,8 +691,8 @@ module _ -- ASSUMPTION --
open UTxOState utxoState
renaming (utxo to st; fees to fs; deposits to deps; donations to dons)
in
Γ ⊢ ⟦ st , fs , deps , dons ⟧ᵘ ⇀⦇ tx ,UTXO⦈
⟦ utxo' , fees' , deposits' , donations' ⟧ᵘ
Γ ⊢ ⟦ st , fs , deps , dons ⟧ ⇀⦇ tx ,UTXO⦈
⟦ utxo' , fees' , deposits' , donations' ⟧

→ noRefundCert txcerts -- FINAL ASSUMPTION --

Expand Down
5 changes: 3 additions & 2 deletions src/ScriptVerification/HelloWorld.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ open import ScriptVerification.LedgerImplementation String String scriptImp
open import ScriptVerification.Lib String String scriptImp
open import Ledger.ScriptValidation SVTransactionStructure SVAbstractFunctions
open import Data.Empty
open import ToRecord
open import Ledger.Conway.Conformance.Utxo SVTransactionStructure SVAbstractFunctions
open import Ledger.Transaction
open TransactionStructure SVTransactionStructure
Expand Down Expand Up @@ -147,14 +148,14 @@ opaque

-- Compute the result of running the UTXO rules on the succeedTx transaction
succeedExample : ComputationResult String UTxOState
succeedExample = UTXO-step initEnv ⟦ initState , 0 , ∅ , 0 ⟧ᵘ succeedTx
succeedExample = UTXO-step initEnv ⟦ initState , 0 , ∅ , 0 ⟧ succeedTx

_ : isSuccess succeedExample ≡ true
_ = refl

-- Compute the result of running the UTXO rules on the failTx transaction
failExample : ComputationResult String UTxOState
failExample = UTXO-step initEnv ⟦ initState , 0 , ∅ , 0 ⟧ᵘ failTx
failExample = UTXO-step initEnv ⟦ initState , 0 , ∅ , 0 ⟧ failTx

_ : isFailure failExample
_ = _ , refl
9 changes: 5 additions & 4 deletions src/ScriptVerification/SucceedIfNumber.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ open import ScriptVerification.LedgerImplementation ℕ ℕ scriptImp
open import ScriptVerification.Lib ℕ ℕ scriptImp
open import Ledger.ScriptValidation SVTransactionStructure SVAbstractFunctions
open import Data.Empty
open import ToRecord
open import Ledger.Conway.Conformance.Utxo SVTransactionStructure SVAbstractFunctions
open import Ledger.Transaction
open TransactionStructure SVTransactionStructure
Expand Down Expand Up @@ -167,29 +168,29 @@ opaque

-- Compute the result of running the UTXO rules on the succeedTx transaction
succeedExample : ComputationResult String UTxOState
succeedExample = UTXO-step initEnv ⟦ initStateDatum , 0 , ∅ , 0 ⟧ᵘ succeedTx
succeedExample = UTXO-step initEnv ⟦ initStateDatum , 0 , ∅ , 0 ⟧ succeedTx

_ : isSuccess succeedExample ≡ true
_ = refl

-- Compute the result of running the UTXO rules on the failTx transaction
failExample : ComputationResult String UTxOState
failExample = UTXO-step initEnv ⟦ initStateRedeemer , 0 , ∅ , 0 ⟧ᵘ failTx
failExample = UTXO-step initEnv ⟦ initStateRedeemer , 0 , ∅ , 0 ⟧ failTx

_ : isFailure failExample
_ = _ , refl

-- Note that the UTXOS rule succeeds but the UTXO rule fails for failTx
failExampleS : Bool
failExampleS = case compute Computational-UTXOS initEnv ⟦ initStateRedeemer , 0 , ∅ , 0 ⟧ᵘ failTx of λ where
failExampleS = case compute Computational-UTXOS initEnv ⟦ initStateRedeemer , 0 , ∅ , 0 ⟧ failTx of λ where
(success x) → true
(failure x) → false

_ : failExampleS ≡ true
_ = refl

failExampleU : Bool
failExampleU = case compute Computational-UTXO initEnv ⟦ initStateRedeemer , 0 , ∅ , 0 ⟧ᵘ failTx of λ where
failExampleU = case compute Computational-UTXO initEnv ⟦ initStateRedeemer , 0 , ∅ , 0 ⟧ failTx of λ where
(success x) → true
(failure x) → false

Expand Down

0 comments on commit b08b87f

Please sign in to comment.