Skip to content

Commit e6ba69e

Browse files
carlostomecarlostome
authored
[Conway/Dijkstra] Move txIns ∩ refInputs ≡ ∅ to allowedLanguages (#1268)
* Move txIns ∩ refInputs ≡ ∅ to allowedLanguages * Refactor allowedLanguagesLegacy in Dijkstra * Add precondition for Plutus V4 to require disjoint tx inputs and ref. inputs * Use genErrors in UTXO
1 parent 79819cd commit e6ba69e

15 files changed

Lines changed: 121 additions & 120 deletions

File tree

‎CHANGELOG.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,7 @@
3333

3434
## Conway spec
3535

36+
- Move `txIns ∩ refInputs ≡ ∅` precondition to `allowedLanguages` to allow non-disjoint tx and ref. inputs for Plutus V1-V2
3637
- Require collateral inputs to be present in the UTxO set in the UTXO rule
3738
- State and prove the claim that a voter's (last) vote in a block is applied to the governance action (see #417)
3839
- Change `RwdAddr` to `RewardAddress`

‎src/Ledger/Conway/Conformance/Equivalence.lagda.md‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -50,26 +50,26 @@ lemInvalidDepositsL : ∀ {Γ utxoSt utxoSt' tx}
5050
→ Γ L.⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt'
5151
→ L.UTxOState.deposits utxoSt ≡ L.UTxOState.deposits utxoSt'
5252
lemInvalidDepositsL refl (L.UTXOW⇒UTXO
53-
(L.UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
53+
(L.UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
5454
(L.Scripts-No _))) = refl
5555
5656
lemInvalidDepositsC : ∀ {Γ utxoSt utxoSt' tx}
5757
→ isValid tx ≡ false
5858
→ (h : Γ C.⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt')
5959
→ utxowDeposits h ≡ L.UTxOState.deposits utxoSt'
6060
lemInvalidDepositsC refl (C.UTXOW⇒UTXO
61-
(C.UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
61+
(C.UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
6262
(C.Scripts-No _))) = refl
6363
6464
-- The UTXOW rule doesn't change the deposits in Conformance
6565
lemDepositsC : ∀ {Γ utxoSt utxoSt' tx}
6666
→ (h : Γ C.⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt')
6767
→ L.UTxOState.deposits utxoSt ≡ L.UTxOState.deposits utxoSt'
6868
lemDepositsC (C.UTXOW⇒UTXO
69-
(C.UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
69+
(C.UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
7070
(C.Scripts-Yes _))) = refl
7171
lemDepositsC (C.UTXOW⇒UTXO
72-
(C.UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
72+
(C.UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
7373
(C.Scripts-No _))) = refl
7474
7575
lemUpdateDeposits : ∀ {Γ s tx s'} (open L.UTxOEnv Γ)
@@ -78,7 +78,7 @@ lemUpdateDeposits : ∀ {Γ s tx s'} (open L.UTxOEnv Γ)
7878
→ L.updateDeposits pparams (body tx) (L.UTxOState.deposits s) ≡ L.UTxOState.deposits s'
7979
lemUpdateDeposits refl
8080
(L.UTXOW⇒UTXO
81-
(L.UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
81+
(L.UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
8282
(L.Scripts-Yes _))) = refl
8383
8484
getValidCertDeposits : ∀ {Γ s tx s'}
@@ -90,7 +90,7 @@ getValidCertDeposits : ∀ {Γ s tx s'}
9090
→ L.ValidCertDeposits pparams deposits txCerts
9191
getValidCertDeposits refl
9292
(L.UTXOW⇒UTXO
93-
(L.UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
93+
(L.UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
9494
(L.Scripts-Yes (v , _)))) = v
9595
9696
makeCertDeps* : ∀ {Γ s tx s'}
@@ -231,7 +231,7 @@ lemUtxowDeposits : ∀ {Γ s s' tx}
231231
→ (r : Γ C.⊢ s ⇀⦇ tx ,UTXOW⦈ s')
232232
→ utxowDeposits r ≡ L.updateDeposits pparams (body tx) (C.UTxOState.deposits s')
233233
lemUtxowDeposits refl (C.UTXOW⇒UTXO
234-
(C.UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
234+
(C.UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
235235
(C.Scripts-Yes _))) = refl
236236
237237
instance

‎src/Ledger/Conway/Conformance/Equivalence/Utxo.lagda.md‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -57,7 +57,7 @@ module _ {Γ s tx s'} where
5757
utxoSDeposits (C.Scripts-No _) = deposits
5858
5959
utxoDeposits : Γ C.⊢ s ⇀⦇ tx ,UTXO⦈ s' → L.Deposits
60-
utxoDeposits (C.UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ h) = utxoSDeposits h
60+
utxoDeposits (C.UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ h) = utxoSDeposits h
6161
6262
utxowDeposits : Γ C.⊢ s ⇀⦇ tx ,UTXOW⦈ s' → L.Deposits
6363
utxowDeposits (C.UTXOW-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ h) = utxoDeposits h
@@ -84,8 +84,8 @@ instance
8484
-- deposits don't change! Why are they even part of the UTxOState?
8585
-- In conformance the update happens in GOVCERT (under CERT).
8686
UTXOToConf : ∀ {Γ s tx s'} → Γ L.⊢ s ⇀⦇ tx ,UTXO⦈ s' ⭆ Γ C.⊢ s ⇀⦇ tx ,UTXO⦈ (withDepositsFrom s s')
87-
UTXOToConf {s = s} {tx = tx} .convⁱ _ (L.UTXO-inductive (a , b , c , d , e , f , g , r , h , i , j , k , l , m , n , o , p , q , utxo)) =
88-
C.UTXO-inductive (a , b , c , d , e , f , g , r , h , i , j , k , l , m , n , o , p , q , conv utxo)
87+
UTXOToConf {s = s} {tx = tx} .convⁱ _ (L.UTXO-inductive (a , b , d , e , f , g , r , h , i , j , k , l , m , n , o , p , q , utxo)) =
88+
C.UTXO-inductive (a , b , d , e , f , g , r , h , i , j , k , l , m , n , o , p , q , conv utxo)
8989
9090
UTXOFromConf : ∀ {Γ s tx s'}
9191
(let open L.UTxOEnv Γ using () renaming (pparams to pp)
@@ -95,8 +95,8 @@ instance
9595
→ (isValid tx ≡ false ⊎ L.ValidCertDeposits pp deposits txCerts)
9696
⊢ Γ C.⊢ s ⇀⦇ tx ,UTXO⦈ s' ⭆ⁱ λ _ h →
9797
Γ L.⊢ s ⇀⦇ tx ,UTXO⦈ (setDeposits (utxoDeposits h) s')
98-
UTXOFromConf {s = s} {tx = tx} .convⁱ validCerts (C.UTXO-inductive (a , b , c , d , e , f , g , r , h , i , j , k , l , m , n , o , p , q , utxo)) =
99-
L.UTXO-inductive (a , b , c , d , e , f , g , r , h , i , j , k , l , m , n , o , p , q , (validCerts ⊢conv utxo))
98+
UTXOFromConf {s = s} {tx = tx} .convⁱ validCerts (C.UTXO-inductive (a , b , d , e , f , g , r , h , i , j , k , l , m , n , o , p , q , utxo)) =
99+
L.UTXO-inductive (a , b , d , e , f , g , r , h , i , j , k , l , m , n , o , p , q , (validCerts ⊢conv utxo))
100100
101101
UTXOWToConf : ∀ {Γ s tx s'} → Γ L.⊢ s ⇀⦇ tx ,UTXOW⦈ s' ⭆ Γ C.⊢ s ⇀⦇ tx ,UTXOW⦈ (withDepositsFrom s s')
102102
UTXOWToConf .convⁱ _ (L.UTXOW-inductive⋯ a b c d e f g h i j k l utxo) =

‎src/Ledger/Conway/Conformance/Utxo.lagda.md‎

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -92,10 +92,13 @@ data _⊢_⇀⦇_,UTXO⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Type
9292
txOutsʰ = (mapValues txOutHash txOuts)
9393
overhead = 160
9494
in
95-
∙ txIns ≢ ∅ ∙ txIns ∪ refInputs ∪ collateralInputs ⊆ dom utxo
96-
∙ txIns ∩ refInputs ≡ ∅ ∙ L.inInterval slot txVldt
97-
∙ L.minfee pp utxo tx ≤ txFee ∙ (txrdmrs ˢ ≢ ∅ → L.collateralCheck pp tx utxo)
98-
∙ consumed pp s txb ≡ produced pp s txb ∙ coin mint ≡ 0
95+
∙ txIns ≢ ∅
96+
∙ txIns ∪ refInputs ∪ collateralInputs ⊆ dom utxo
97+
∙ L.inInterval slot txVldt
98+
∙ L.minfee pp utxo tx ≤ txFee
99+
∙ (txrdmrs ˢ ≢ ∅ → L.collateralCheck pp tx utxo)
100+
∙ consumed pp s txb ≡ produced pp s txb
101+
∙ coin mint ≡ 0
99102
∙ (∅ᵐ ≢ᵐ txrdmrs × nothing ≢ proj₂ txVldt →
100103
map epochInfoSlotToUTCTime (proj₂ txVldt) ≢ nothing
101104
)
@@ -116,7 +119,7 @@ data _⊢_⇀⦇_,UTXO⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Type
116119
────────────────────────────────
117120
Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s'
118121
119-
pattern UTXO-inductive⋯ tx Γ s x y z w k l m c d v j n o p q r t u h
120-
= UTXO-inductive {tx}{Γ}{s} (x , y , z , w , k , l , m , c , d , v , j , n , o , p , q , r , t , u , h)
122+
pattern UTXO-inductive⋯ tx Γ s x y w k l m c d v j n o p q r t u h
123+
= UTXO-inductive {tx}{Γ}{s} (x , y , w , k , l , m , c , d , v , j , n , o , p , q , r , t , u , h)
121124
unquoteDecl UTXO-premises = genPremises UTXO-premises (quote UTXO-inductive)
122125
```

‎src/Ledger/Conway/Conformance/Utxo/Properties.lagda.md‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -71,16 +71,16 @@ instance
7171
renaming (computeProof to computeProof'; completeness to completeness')
7272
7373
computeProofH : Dec H → ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s')
74-
computeProofH (yes (x , y , z , e , k , l , m , c , d , v , j , n , o , p , q , r , t , u)) =
75-
map₂′ (UTXO-inductive⋯ _ _ _ x y z e k l m c d v j n o p q r t u) <$> computeProof' Γ s tx
74+
computeProofH (yes (x , y , e , k , l , m , c , d , v , j , n , o , p , q , r , t , u)) =
75+
map₂′ (UTXO-inductive⋯ _ _ _ x y e k l m c d v j n o p q r t u) <$> computeProof' Γ s tx
7676
computeProofH (no ¬p) = failure $ genErrors ¬p
7777
7878
computeProof : ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s')
7979
computeProof = computeProofH H?
8080
8181
completeness : ∀ s' → Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s' → map proj₁ computeProof ≡ success s'
82-
completeness s' (UTXO-inductive⋯ _ _ _ x y z e k l m c d v j n o p q r t u h) with H?
83-
... | no ¬p = ⊥-elim $ ¬p (x , y , z , e , k , l , m , c , d , v , j , n , o , p , q , r , t , u )
82+
completeness s' (UTXO-inductive⋯ _ _ _ x y e k l m c d v j n o p q r t u h) with H?
83+
... | no ¬p = ⊥-elim $ ¬p (x , y , e , k , l , m , c , d , v , j , n , o , p , q , r , t , u )
8484
... | yes _ with computeProof' Γ s tx | completeness' _ _ _ _ h
8585
... | success _ | refl = refl
8686

‎src/Ledger/Conway/Specification/Ledger/Properties/Base.lagda.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -71,7 +71,7 @@ In the remainder of this section, we show some utility lemmas without proofs.
7171
<!--
7272
```agda
7373
module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence {DepositPurpose})
74-
pattern UTXOW-UTXOS x = UTXOW⇒UTXO (UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ x)
74+
pattern UTXOW-UTXOS x = UTXOW⇒UTXO (UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ x)
7575
7676
open Equivalence
7777
```

‎src/Ledger/Conway/Specification/Ledger/Properties/PoV.lagda.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ module _
4343
→ InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s )
4444
where
4545
46-
pattern UTXO-induction r = UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ r _ _ _
46+
pattern UTXO-induction r = UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ r _ _ _
4747
```
4848
-->
4949

‎src/Ledger/Conway/Specification/Utxo.lagda.md‎

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -541,10 +541,13 @@ data _⊢_⇀⦇_,UTXO⦈_ where
541541
txOutsʰ = mapValues txOutHash txOuts
542542
overhead = 160
543543
in
544-
∙ txIns ≢ ∅ ∙ txIns ∪ refInputs ∪ collateralInputs ⊆ dom utxo
545-
∙ txIns ∩ refInputs ≡ ∅ ∙ inInterval slot txVldt
546-
∙ minfee pp utxo tx ≤ txFee ∙ (txrdmrs ˢ ≢ ∅ → collateralCheck pp tx utxo)
547-
∙ consumed pp s txb ≡ produced pp s txb ∙ coin mint ≡ 0
544+
∙ txIns ≢ ∅
545+
∙ txIns ∪ refInputs ∪ collateralInputs ⊆ dom utxo
546+
∙ inInterval slot txVldt
547+
∙ minfee pp utxo tx ≤ txFee
548+
∙ (txrdmrs ˢ ≢ ∅ → collateralCheck pp tx utxo)
549+
∙ consumed pp s txb ≡ produced pp s txb
550+
∙ coin mint ≡ 0
548551
∙ (∅ᵐ ≢ᵐ txrdmrs × nothing ≢ proj₂ txVldt →
549552
map epochInfoSlotToUTCTime (proj₂ txVldt) ≢ nothing
550553
)
@@ -567,8 +570,8 @@ data _⊢_⇀⦇_,UTXO⦈_ where
567570

568571
<!--
569572
```agda
570-
pattern UTXO-inductive⋯ tx Γ s x y z w k l m c d v j n o p q r t u h
571-
= UTXO-inductive {Γ = Γ} {s = s} {tx = tx} (x , y , z , w , k , l , m , c , d , v , j , n , o , p , q , r , t , u , h)
573+
pattern UTXO-inductive⋯ tx Γ s x y w k l m c d v j n o p q r t u h
574+
= UTXO-inductive {Γ = Γ} {s = s} {tx = tx} (x , y , w , k , l , m , c , d , v , j , n , o , p , q , r , t , u , h)
572575
unquoteDecl UTXO-premises = genPremises UTXO-premises (quote UTXO-inductive)
573576
```
574577
-->

‎src/Ledger/Conway/Specification/Utxo/Properties/Base.lagda.md‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -186,7 +186,7 @@ module _
186186
stepS : Γ ⊢ ⟦ utxo , fees , deposits , donations ⟧ ⇀⦇ tx ,UTXOS⦈
187187
⟦ utxo' , fees' , deposits' , donations' ⟧
188188
stepS = case step of λ where
189-
(UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ h) → h
189+
(UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ h) → h
190190
191191
pp : PParams
192192
pp = UTxOEnv.pparams Γ
@@ -208,13 +208,13 @@ module _
208208
newBal' : Γ ⊢ ⟦ utxo , fees , deposits , donations ⟧ ⇀⦇ tx ,UTXO⦈
209209
⟦ utxo' , fees' , deposits' , donations' ⟧
210210
→ consumed pp utxoSt txb ≡ produced pp utxoSt txb
211-
newBal' (UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ x _ _ _ _ _ _ _ _ _ _ _ _) = x
211+
newBal' (UTXO-inductive⋯ _ _ _ _ _ _ _ _ x _ _ _ _ _ _ _ _ _ _ _ _) = x
212212
newBal : consumed pp utxoSt txb ≡ produced pp utxoSt txb
213213
newBal = newBal' step
214214
noMintAda' : Γ ⊢ ⟦ utxo , fees , deposits , donations ⟧ ⇀⦇ tx ,UTXO⦈
215215
⟦ utxo' , fees' , deposits' , donations' ⟧
216216
→ coin (mint) ≡ 0
217-
noMintAda' (UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ x _ _ _ _ _ _ _ _ _ _ _) = x
217+
noMintAda' (UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ x _ _ _ _ _ _ _ _ _ _ _) = x
218218
noMintAda : coin mint ≡ 0
219219
noMintAda = noMintAda' step
220220
remDepTot : Coin

‎src/Ledger/Conway/Specification/Utxo/Properties/Computational.lagda.md‎

Lines changed: 6 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,7 @@ open import Ledger.Prelude hiding (≤-trans; ≤-antisym; All); open Properties
2727
open import Tactic.Cong using (cong!)
2828
open import Tactic.EquationalReasoning using (module ≡-Reasoning)
2929
open import stdlib-meta.Tactic.MonoidSolver.NonNormalising using (solve-macro)
30+
open import stdlib-meta.Tactic.GenError
3031
3132
open import Ledger.Conway.Specification.Utxo txs abs
3233
open import Ledger.Conway.Specification.Script.Validation txs abs
@@ -73,60 +74,17 @@ instance
7374
open Computational Computational-UTXOS
7475
renaming (computeProof to computeProof'; completeness to completeness')
7576
76-
genErr : ¬ H → String
77-
genErr ¬p = case dec-de-morgan ¬p of λ where
78-
(inj₁ a) → "¬ TxBody.txIns (Tx.body tx) ≢ ∅"
79-
(inj₂ b) → case dec-de-morgan b of λ where
80-
(inj₁ a₁) → "¬ txIns ∪ refInputs ∪ collateralInputs ⊆ dom (UTxOOf s)"
81-
(inj₂ b₁) → case dec-de-morgan b₁ of λ where
82-
(inj₁ a₁') → "¬ txIns ∩ refInputs ≡ ∅"
83-
(inj₂ b₂') → case dec-de-morgan b₂' of λ where
84-
(inj₁ a₂) → "¬ inInterval (UTxOEnv.slot Γ) (txvldt (Tx.body tx))"
85-
(inj₂ b₂) → case dec-de-morgan b₂ of λ where
86-
(inj₁ a₃) → "¬ minfee pp utxo tx ≤ txFee"
87-
(inj₂ b₃) → case dec-de-morgan b₃ of λ where
88-
(inj₁ a₄) → "¬ (txrdmrs ˢ ≢ ∅ → collateralCheck pp tx utxo)"
89-
(inj₂ b₄) → case dec-de-morgan b₄ of λ where
90-
(inj₁ a₅) →
91-
let
92-
pp = PParamsOf Γ
93-
txb = TxBodyOf tx
94-
con = consumed pp s txb
95-
prod = produced pp s txb
96-
showValue = show ∘ coin
97-
in
98-
( "¬consumed (UTxOEnv.pparams Γ) s (Tx.body tx) ≡ produced (PParamsOf Γ) s (Tx.body tx)"
99-
+ˢ "\n consumed =\t\t" +ˢ showValue con
100-
+ˢ "\n ins =\t\t" +ˢ showValue (balance (UTxOOf s ∣ txb .TxBody.txIns))
101-
+ˢ "\n mint =\t\t" +ˢ showValue (TxBody.mint txb)
102-
+ˢ "\n depositRefunds =\t" +ˢ showValue (inject (depositRefunds pp s txb))
103-
+ˢ "\n produced =\t\t" +ˢ showValue prod
104-
+ˢ "\n outs =\t\t" +ˢ showValue (balance $ outs txb)
105-
+ˢ "\n fee =\t\t" +ˢ show (FeesOf tx)
106-
+ˢ "\n newDeposits =\t" +ˢ show (newDeposits pp s txb)
107-
+ˢ "\n donation =\t\t" +ˢ show (DonationsOf txb)
108-
)
109-
(inj₂ b₅) → case dec-de-morgan b₅ of λ where
110-
(inj₁ a₆) → "¬ coin (TxBody.mint (Tx.body tx)) ≡ 0"
111-
(inj₂ b₆) → case dec-de-morgan b₆ of λ where
112-
(inj₁ a₇) → "¬ (∅ᵐ ≢ᵐ txrdmrs × nothing ≢ proj₂ txVldt → map epochInfoSlotToUTCTime (proj₂ txVldt) ≢ nothing)"
113-
(inj₂ b₇) → case dec-de-morgan b₇ of λ where
114-
(inj₁ a₈) → "¬ ((Tx.txsize tx) Data.Nat.Base.≤ maxTxSize (UTxOEnv.pparams Γ))"
115-
(inj₂ b₈) → case dec-de-morgan b₈ of λ where
116-
(inj₁ a₉) → "¬ refScriptsSize utxo tx ≤ maxRefScriptSizePerTx pp"
117-
(inj₂ _) → "something else broke"
118-
11977
computeProofH : Dec H → ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s')
120-
computeProofH (yes (x , y , z , e , k , l , m , c , d , v , j , n , o , p , q , r , t , u)) =
121-
map₂′ (UTXO-inductive⋯ _ _ _ x y z e k l m c d v j n o p q r t u) <$> computeProof' Γ s tx
122-
computeProofH (no ¬p) = failure $ genErr ¬p
78+
computeProofH (yes (x , y , e , k , l , m , c , d , v , j , n , o , p , q , r , t , u)) =
79+
map₂′ (UTXO-inductive⋯ _ _ _ x y e k l m c d v j n o p q r t u) <$> computeProof' Γ s tx
80+
computeProofH (no ¬p) = failure $ genErrors ¬p
12381
12482
computeProof : ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s')
12583
computeProof = computeProofH H?
12684
12785
completeness : ∀ s' → Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s' → map proj₁ computeProof ≡ success s'
128-
completeness s' (UTXO-inductive⋯ _ _ _ x y z w k l m c d v j n o p q r t u h) with H?
129-
... | no ¬p = ⊥-elim $ ¬p (x , y , z , w , k , l , m , c , d , v , j , n , o , p , q , r , t , u)
86+
completeness s' (UTXO-inductive⋯ _ _ _ x y w k l m c d v j n o p q r t u h) with H?
87+
... | no ¬p = ⊥-elim $ ¬p (x , y , w , k , l , m , c , d , v , j , n , o , p , q , r , t , u)
13088
... | yes _ with computeProof' Γ s tx | completeness' _ _ _ _ h
13189
... | success _ | refl = refl
13290

0 commit comments

Comments
 (0)