Skip to content

Commit

Permalink
updating utxo proofs to remove script decidability
Browse files Browse the repository at this point in the history
  • Loading branch information
@Ali-Hill
Ali-Hill committed Apr 16, 2024
1 parent 62869d7 commit bdab128
Show file tree
Hide file tree
Showing 10 changed files with 164 additions and 120 deletions.
66 changes: 41 additions & 25 deletions src/Axiom/Set/Map.agda
View file
Expand Up @@ -20,6 +20,7 @@ open import Data.Product.Properties using (×-≡,≡→≡; ×-≡,≡←≡)
open import Data.Maybe.Properties using (just-injective)
open import Relation.Unary using (Decidable)
import Relation.Binary.PropositionalEquality as I
import Relation.Binary.Reasoning.Setoid as SetoidReasoning

open Equivalence

Expand Down Expand Up @@ -152,28 +153,6 @@ singletonᵐ a b = ❴ (a , b) ❵
❴_❵ᵐ : A × B → Map A B
❴ k , v ❵ᵐ = singletonᵐ k v

module Unionᵐ (sp-∈ : spec-∈ A) where
infixr 6 _∪ˡ_

_∪ˡ'_ : Rel A B → Rel A B → Rel A B
m ∪ˡ' m' = m ∪ filter (sp-∘ (sp-¬ (sp-∈ {dom m})) proj₁) m'

_∪ˡ_ : Map A B → Map A B → Map A B
m ∪ˡ m' = disj-∪ m (filterᵐ (sp-∘ (sp-¬ sp-∈) proj₁) m')
(∈⇔P -⟨ (λ where x (_ , refl , hy) → proj₁ (∈⇔P hy) (∈⇔P x)) ⟩- ∈⇔P)

disjoint-∪ˡ-∪ : (H : disjoint (dom R) (dom R')) → R ∪ˡ' R' ≡ᵉ R ∪ R'
disjoint-∪ˡ-∪ disj = from ≡ᵉ⇔≡ᵉ' λ _ → mk⇔
(∈-∪⁺ ∘′ ⊎.map₂ (proj₂ ∘′ ∈⇔P) ∘′ ∈⇔P)
(∈⇔P ∘′ ⊎.map₂ (to ∈-filter ∘′ (λ h → (flip disj (∈-map⁺'' h)) , h)) ∘ ∈⇔P)

insert : Map A B → A → B → Map A B
insert m a b = ❴ a , b ❵ᵐ ∪ˡ m

insertIfJust : ⦃ DecEq A ⦄ → A → Maybe B → Map A B → Map A B
insertIfJust x nothing m = m
insertIfJust x (just y) m = insert m x y

disj-dom : ∀ {m m₁ m₂ : Map A B}
→ (m ˢ) ≡ (m₁ ˢ) ⨿ (m₂ ˢ)
→ disjoint (dom (m₁ ˢ)) (dom (m₂ ˢ))
Expand Down Expand Up @@ -212,6 +191,46 @@ mapKeys : (f : A → A') → (m : Map A B)
→ Map A' B
mapKeys f (R , uniq) {inj} = mapˡ f R , mapˡ-uniq {inj = inj} uniq

mapValues : (B → B') → Map A B → Map A B'
mapValues f (R , uniq) = mapʳ f R , mapʳ-uniq uniq

module Unionᵐ (sp-∈ : spec-∈ A) where
infixr 6 _∪ˡ_

_∪ˡ'_ : Rel A B → Rel A B → Rel A B
m ∪ˡ' m' = m ∪ filter (sp-∘ (sp-¬ (sp-∈ {dom m})) proj₁) m'

_∪ˡ_ : Map A B → Map A B → Map A B
m ∪ˡ m' = disj-∪ m (filterᵐ (sp-∘ (sp-¬ sp-∈) proj₁) m')
(∈⇔P -⟨ (λ where x (_ , refl , hy) → proj₁ (∈⇔P hy) (∈⇔P x)) ⟩- ∈⇔P)

disjoint-∪ˡ-∪ : (H : disjoint (dom R) (dom R')) → R ∪ˡ' R' ≡ᵉ R ∪ R'
disjoint-∪ˡ-∪ disj = from ≡ᵉ⇔≡ᵉ' λ _ → mk⇔
(∈-∪⁺ ∘′ ⊎.map₂ (proj₂ ∘′ ∈⇔P) ∘′ ∈⇔P)
(∈⇔P ∘′ ⊎.map₂ (to ∈-filter ∘′ (λ h → (flip disj (∈-map⁺'' h)) , h)) ∘ ∈⇔P)

insert : Map A B → A → B → Map A B
insert m a b = ❴ a , b ❵ᵐ ∪ˡ m

insertIfJust : ⦃ DecEq A ⦄ → A → Maybe B → Map A B → Map A B
insertIfJust x nothing m = m
insertIfJust x (just y) m = insert m x y

disjoint-∪ˡ-mapValues : {M M' : Map A B}
(f : B → C)
→ (H : disjoint (dom (M ˢ)) (dom (M' ˢ)))
→ (mapValues f (M ∪ˡ M')) ˢ ≡ᵉ (mapValues f M ∪ˡ mapValues f M') ˢ
disjoint-∪ˡ-mapValues {M = M} {M'} f disj = begin
proj₁ (mapValues f (M ∪ˡ M'))
≈⟨ map-≡ᵉ (disjoint-∪ˡ-∪ disj) ⟩
(mapʳ f ((proj₁ M) ∪ (proj₁ M')))
≈⟨ map-∪ _ ⟩
(mapʳ f (proj₁ M) ∪ mapʳ f (proj₁ M'))
≈˘⟨ disjoint-∪ˡ-∪ (λ x₁ x₂ → disj (dom-mapʳ⊆ x₁) (dom-mapʳ⊆ x₂)) ⟩
proj₁ (mapValues f M ∪ˡ mapValues f M')
∎
where open SetoidReasoning ≡ᵉ-Setoid

map⦅×-dup⦆-uniq : ∀ {x : Set A} → left-unique (mapˢ ×-dup x)
map⦅×-dup⦆-uniq x y with ∈-map⁻' x | ∈-map⁻' y
... | fst , refl , _ | .fst , refl , _ = refl
Expand All @@ -224,9 +243,6 @@ mapˡ∘map⦅×-dup⦆-uniq {inj = inj} = mapˡ-uniq {inj = λ _ _ → inj} map
idMap : Set A → Map A A
idMap s = -, map⦅×-dup⦆-uniq {x = s}

mapValues : (B → B') → Map A B → Map A B'
mapValues f (R , uniq) = mapʳ f R , mapʳ-uniq uniq

mapFromFun : (A → B) → Set A → Map A B
mapFromFun f s = mapValues f (idMap s)

Expand Down
25 changes: 22 additions & 3 deletions src/Axiom/Set/Properties.agda
View file
Expand Up @@ -11,6 +11,8 @@ open Theory th
import Data.List
import Data.Sum
import Function.Related.Propositional as R
import Relation.Binary.Lattice.Properties.BoundedJoinSemilattice as Bounded∨Semilattice
import Relation.Binary.Lattice.Properties.JoinSemilattice as ∨Semilattice
import Relation.Nullary.Decidable
open import Data.List.Ext.Properties using (_×-cong_; _⊎-cong_)
open import Data.List.Membership.DecPropositional using () renaming (_∈?_ to _∈ˡ?_)
Expand All @@ -21,12 +23,12 @@ open import Data.List.Relation.Binary.Subset.Propositional using () renaming (_
open import Data.List.Relation.Unary.Any using (here; there)
open import Data.List.Relation.Unary.Unique.Propositional.Properties.WithK using (unique∧set⇒bag)
open import Data.Product using (map₂)
open import Data.Product.Properties.Ext
open import Data.Relation.Nullary.Decidable.Ext using (map′⇔)
open import Function.Related.TypeIsomorphisms
open import Relation.Binary hiding (_⇔_)
open import Relation.Binary.Lattice
import Relation.Binary.Lattice.Properties.BoundedJoinSemilattice as Bounded∨Semilattice
import Relation.Binary.Lattice.Properties.JoinSemilattice as ∨Semilattice
open import Relation.Binary.Morphism using (IsOrderHomomorphism)
open import Data.Relation.Nullary.Decidable.Ext using (map′⇔)

open Equivalence

Expand Down Expand Up @@ -173,6 +175,23 @@ map-≡ᵉ (x⊆y , y⊆x) = map-⊆ x⊆y , map-⊆ y⊆x
map-∅ : {X : Set A} {f : A → B} → map f ∅ ≡ᵉ ∅
map-∅ = ∅-least λ x∈map → case ∈-map⁻' x∈map of λ where (_ , _ , h) → ⊥-elim (∉-∅ h)

map-∪ : {X Y : Set A} → (f : A → B) → map f (X ∪ Y) ≡ᵉ map f X ∪ map f Y
map-∪ {X = X} {Y} f = from ≡ᵉ⇔≡ᵉ' λ b →
b ∈ map f (X ∪ Y)
∼⟨ R.SK-sym ∈-map ⟩
(∃[ a ] b ≡ f a × a ∈ X ∪ Y)
∼⟨ ∃-cong′ (R.K-refl ×-cong R.SK-sym ∈-∪) ⟩
(∃[ a ] b ≡ f a × (a ∈ X ⊎ a ∈ Y))
↔⟨ ∃-cong′ ×-distribˡ-⊎' ⟩
(∃[ a ] (b ≡ f a × a ∈ X ⊎ b ≡ f a × a ∈ Y))
↔⟨ ∃-distrib-⊎' ⟩
(∃[ a ] b ≡ f a × a ∈ X ⊎ ∃[ a ] b ≡ f a × a ∈ Y)
∼⟨ ∈-map ⊎-cong ∈-map ⟩
(b ∈ map f X ⊎ b ∈ map f Y)
∼⟨ ∈-∪ ⟩
b ∈ map f X ∪ map f Y ∎
where open R.EquationalReasoning

mapPartial-∅ : {f : A → Maybe B} → mapPartial f ∅ ≡ᵉ ∅
mapPartial-∅ {f = f} = ∅-least λ x∈map → case from (∈-mapPartial {f = f}) x∈map of λ where
(_ , h , _) → ⊥-elim (∉-∅ h)
Expand Down
28 changes: 24 additions & 4 deletions src/Data/Product/Properties/Ext.agda
View file
Expand Up @@ -7,11 +7,16 @@ open import Data.Product.Function.Dependent.Propositional using (cong)
open import Function
open import Function.Related.Propositional
open import Level
open import Relation.Binary.PropositionalEquality hiding (cong)
open import Relation.Binary.PropositionalEquality hiding (cong; [_])
open import Data.Product.Base as Prod
open import Data.Sum.Base
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)

private
variable a a₁ a₂ b₁ b₂ : Level
k : Kind
private variable
ℓ : Level
A B C : Set ℓ
a a₁ a₂ b₁ b₂ : Level
k : Kind

∃-cong : {A₁ : Set a₁} {A₂ : Set a₂} {B₁ : A₁ → Set b₁} {B₂ : A₂ → Set b₂} (A₁↔A₂ : A₁ ↔ A₂)
→ (∀ {x} → B₁ x ∼[ k ] B₂ (Inverse.to A₁↔A₂ x))
Expand All @@ -25,3 +30,18 @@ private

∃-≡ : ∀ {A : Set a₁} (P : A → Set a₂) {x} → P x ⇔ (∃[ y ] y ≡ x × P y)
∃-≡ P {x} = mk⇔ (λ Px → x , refl , Px) (λ where (y , (refl , Py)) → Py)

-- the version in Function.Related.TypeIsomorphisms isn't level-polymorphic enough
×-distribˡ-⊎' : (A × (B ⊎ C)) ↔ (A × B ⊎ A × C)
×-distribˡ-⊎' = mk↔ₛ′
(uncurry λ x → [ inj₁ ∘′ (x ,_) , inj₂ ∘′ (x ,_) ]′)
[ Prod.map₂ inj₁ , Prod.map₂ inj₂ ]′
[ (λ _ → P.refl) , (λ _ → P.refl) ]
(uncurry λ _ → [ (λ _ → P.refl) , (λ _ → P.refl) ])

∃-distrib-⊎' : {P Q : A → Set ℓ} → (∃[ a ] (P a ⊎ Q a)) ↔ (∃[ a ] P a ⊎ ∃[ a ] Q a)
∃-distrib-⊎' = mk↔ₛ′
(uncurry λ x → [ inj₁ ∘′ (x ,_) , inj₂ ∘′ (x ,_) ]′)
[ Prod.map₂ inj₁ , Prod.map₂ inj₂ ]′
[ (λ _ → P.refl) , (λ _ → P.refl) ]
(uncurry λ _ → [ (λ _ → P.refl) , (λ _ → P.refl) ])
2 changes: 1 addition & 1 deletion src/Ledger/Script.lagda
View file
Expand Up @@ -34,7 +34,7 @@ record PlutusStructure : Set₁ where
Language PlutusScript CostModel Prices LangDepView ExUnits : Set
⦃ ExUnit-CommutativeMonoid ⦄ : IsCommutativeMonoid' 0ℓ 0ℓ ExUnits
⦃ Hashable-PlutusScript ⦄ : Hashable PlutusScript ScriptHash
⦃ DecEq-PlutusScript ⦄ : DecEq PlutusScript
-- ⦃ DecEq-PlutusScript ⦄ : DecEq PlutusScript
⦃ DecEq-CostModel ⦄ : DecEq CostModel
⦃ DecEq-LangDepView ⦄ : DecEq LangDepView

Expand Down
8 changes: 8 additions & 0 deletions src/Ledger/Transaction.lagda
View file
Expand Up @@ -164,6 +164,14 @@ the transaction body are:
getValue : TxOut → Value
getValue (_ , v , _) = v

TxOutʰ = Addr × Value × Maybe (Datum ⊎ DataHash) × Maybe ScriptHash

txOutHash : TxOut → TxOutʰ
txOutHash (a , v , d , s) = a , (v , (d , M.map hash s))

getValueʰ : TxOutʰ → Value
getValueʰ (_ , v , _) = v

txinsVKey : ℙ TxIn → UTxO → ℙ TxIn
txinsVKey txins utxo = txins ∩ dom (utxo ↾' (isVKeyAddr ∘ proj₁))

Expand Down
21 changes: 11 additions & 10 deletions src/Ledger/Utxo.lagda
View file
Expand Up @@ -78,8 +78,8 @@ totExUnits tx = ∑[ (_ , eu) ← tx .wits .txrdmrs ] eu
utxoEntrySizeWithoutVal : MemoryEstimate
utxoEntrySizeWithoutVal = 8

utxoEntrySize : TxOut → MemoryEstimate
utxoEntrySize o = utxoEntrySizeWithoutVal + size (getValue o)
utxoEntrySize : TxOutʰ → MemoryEstimate
utxoEntrySize o = utxoEntrySizeWithoutVal + size (getValueʰ o)


open PParams
Expand Down Expand Up @@ -117,7 +117,7 @@ module _ (let open Tx; open TxBody; open TxWitnesses) where opaque
outs tx = mapKeys (tx .txid ,_) (tx .txouts)

balance : UTxO → Value
balance utxo = ∑[ x ← utxo ] getValue x
balance utxo = ∑[ x ← mapValues txOutHash utxo ] getValueʰ x

cbalance : UTxO → Coin
cbalance utxo = coin (balance utxo)
Expand Down Expand Up @@ -239,7 +239,7 @@ feesOK pp tx utxo = minfee pp utxo tx ≤ᵇ txfee
)
where
open Tx tx; open TxBody body; open TxWitnesses wits; open PParams pp
collateralRange = range (utxo ∣ collateral)
collateralRange = range ((mapValues txOutHash utxo) ∣ collateral)
bal = balance (utxo ∣ collateral)
\end{code}
\end{AgdaMultiCode}
Expand Down Expand Up @@ -391,19 +391,20 @@ data _⊢_⇀⦇_,UTXO⦈_ where
let open Tx tx renaming (body to txb); open TxBody txb
open UTxOEnv Γ renaming (pparams to pp)
open UTxOState s
txoutsʰ = (mapValues txOutHash txouts)
in
∙ txins ≢ ∅ ∙ txins ⊆ dom utxo
∙ refInputs ⊆ dom utxo ∙ inInterval slot txvldt
∙ feesOK pp tx utxo ≡ true ∙ consumed pp s txb ≡ produced pp s txb
∙ coin mint ≡ 0 ∙ txsize ≤ maxTxSize pp

∙ ∀[ (_ , txout) ∈ txouts .proj₁ ]
inject (utxoEntrySize txout * minUTxOValue pp) ≤ᵗ getValue txout
∙ ∀[ (_ , txout) ∈ txouts .proj₁ ]
serSize (getValue txout) ≤ maxValSize pp
∙ ∀[ (a , _) ∈ range txouts ]
∙ ∀[ (_ , txout) ∈ txoutsʰ .proj₁ ]
inject (utxoEntrySize txout * minUTxOValue pp) ≤ᵗ getValueʰ txout
∙ ∀[ (_ , txout) ∈ txoutsʰ .proj₁ ]
serSize (getValueʰ txout) ≤ maxValSize pp
∙ ∀[ (a , _) ∈ range txoutsʰ ]
Sum.All (const ⊤) (λ a → a .BootstrapAddr.attrsSize ≤ 64) a
∙ ∀[ (a , _) ∈ range txouts ] netId a ≡ networkId
∙ ∀[ (a , _) ∈ range txoutsʰ ] netId a ≡ networkId
∙ ∀[ a ∈ dom txwdrls ] a .RwdAddr.net ≡ networkId
∙ Γ ⊢ s ⇀⦇ tx ,UTXOS⦈ s'
────────────────────────────────
Expand Down
83 changes: 42 additions & 41 deletions src/Ledger/Utxo/Properties.lagda
View file
Expand Up @@ -86,40 +86,42 @@ instance
(inj₂ b) → case dec-de-morgan b of λ where
(inj₁ a₁) → "¬ TxBody.txins (Tx.body tx) ⊆ dom (UTxOState.utxo s)"
(inj₂ b₁) → case dec-de-morgan b₁ of λ where
(inj₁ a₂) → "¬ inInterval (UTxOEnv.slot Γ) (txvldt (Tx.body tx))"
(inj₂ b₂) → case dec-de-morgan b₂ of λ where
(inj₁ a₃) → "¬ feesOK pp tx utxo ≡ true"
(inj₂ b₃) → case dec-de-morgan b₃ of λ where
(inj₁ a₄) →
let
pp = UTxOEnv.pparams Γ
txb = Tx.body tx
con = consumed pp s txb
prod = produced pp s txb
showValue = show ∘ coin
in
( "¬consumed (UTxOEnv.pparams Γ) s (Tx.body tx) ≡ produced (UTxOEnv.pparams Γ) s (Tx.body tx)"
+ˢ "\n consumed =\t\t" +ˢ showValue con
+ˢ "\n ins =\t\t" +ˢ showValue (balance (s .UTxOState.utxo ∣ txb .TxBody.txins))
+ˢ "\n mint =\t\t" +ˢ showValue (TxBody.mint txb)
+ˢ "\n depositRefunds =\t" +ˢ showValue (inject (depositRefunds pp s txb))
+ˢ "\n produced =\t\t" +ˢ showValue prod
+ˢ "\n outs =\t\t" +ˢ showValue (balance $ outs txb)
+ˢ "\n fee =\t\t" +ˢ show (txb .TxBody.txfee)
+ˢ "\n newDeposits =\t" +ˢ show (newDeposits pp s txb)
+ˢ "\n donation =\t\t" +ˢ show (txb .TxBody.txdonation)
)
(inj₂ b₄) → case dec-de-morgan b₄ of λ where
(inj₁ a₅) → "¬ coin (TxBody.mint (Tx.body tx)) ≡ 0"
(inj₂ b₅) → case dec-de-morgan b₅ of λ where
(inj₁ a₆) → "¬(TxBody.txsize (Tx.body tx) Data.Nat.Base.≤ maxTxSize (UTxOEnv.pparams Γ))"
(inj₂ b₆) → case dec-de-morgan b₆ of λ where
(inj₁ a₇) → "∀[ (_ , txout) ∈ txouts .proj₁ ] inject (utxoEntrySize txout * minUTxOValue pp) ≤ᵗ getValue txout"
(inj₂ b₇) → case dec-de-morgan b₇ of λ where
(inj₁ a₈) → "∀[ (_ , txout) ∈ txouts .proj₁ ] serSize (getValue txout) ≤ maxValSize pp"
(inj₂ b₈) → case dec-de-morgan b₈ of λ where
(inj₁ a₉) → "∀[ (a , _) ∈ range txouts ] Sum.All (const ⊤) (λ a → a .BootstrapAddr.attrsSize ≤ 64) a"
(inj₂ _) → "something else broke"
(inj₁ a₁') → "¬ refInputs ⊆ dom utxo "
(inj₂ b₂') → case dec-de-morgan b₂' of λ where
(inj₁ a₂) → "¬ inInterval (UTxOEnv.slot Γ) (txvldt (Tx.body tx))"
(inj₂ b₂) → case dec-de-morgan b₂ of λ where
(inj₁ a₃) → "¬ feesOK pp tx utxo ≡ true"
(inj₂ b₃) → case dec-de-morgan b₃ of λ where
(inj₁ a₄) →
let
pp = UTxOEnv.pparams Γ
txb = Tx.body tx
con = consumed pp s txb
prod = produced pp s txb
showValue = show ∘ coin
in
( "¬consumed (UTxOEnv.pparams Γ) s (Tx.body tx) ≡ produced (UTxOEnv.pparams Γ) s (Tx.body tx)"
+ˢ "\n consumed =\t\t" +ˢ showValue con
+ˢ "\n ins =\t\t" +ˢ showValue (balance (s .UTxOState.utxo ∣ txb .TxBody.txins))
+ˢ "\n mint =\t\t" +ˢ showValue (TxBody.mint txb)
+ˢ "\n depositRefunds =\t" +ˢ showValue (inject (depositRefunds pp s txb))
+ˢ "\n produced =\t\t" +ˢ showValue prod
+ˢ "\n outs =\t\t" +ˢ showValue (balance $ outs txb)
+ˢ "\n fee =\t\t" +ˢ show (txb .TxBody.txfee)
+ˢ "\n newDeposits =\t" +ˢ show (newDeposits pp s txb)
+ˢ "\n donation =\t\t" +ˢ show (txb .TxBody.txdonation)
)
(inj₂ b₄) → case dec-de-morgan b₄ of λ where
(inj₁ a₅) → "¬ coin (TxBody.mint (Tx.body tx)) ≡ 0"
(inj₂ b₅) → case dec-de-morgan b₅ of λ where
(inj₁ a₆) → "¬(TxBody.txsize (Tx.body tx) Data.Nat.Base.≤ maxTxSize (UTxOEnv.pparams Γ))"
(inj₂ b₆) → case dec-de-morgan b₆ of λ where
(inj₁ a₇) → "∀[ (_ , txout) ∈ txouts .proj₁ ] inject (utxoEntrySize txout * minUTxOValue pp) ≤ᵗ getValue txout"
(inj₂ b₇) → case dec-de-morgan b₇ of λ where
(inj₁ a₈) → "∀[ (_ , txout) ∈ txouts .proj₁ ] serSize (getValue txout) ≤ maxValSize pp"
(inj₂ b₈) → case dec-de-morgan b₈ of λ where
(inj₁ a₉) → "∀[ (a , _) ∈ range txouts ] Sum.All (const ⊤) (λ a → a .BootstrapAddr.attrsSize ≤ 64) a"
(inj₂ _) → "something else broke"

computeProofH : Dec H → ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s')
computeProofH (yes (x , y , z , e , k , l , m , v , n , o , p , q , r)) =
Expand Down Expand Up @@ -157,7 +159,7 @@ private
opaque
unfolding balance
balance-cong : proj₁ utxo ≡ᵉ proj₁ utxo' → balance utxo ≈ balance utxo'
balance-cong {utxo} {utxo'} = indexedSumᵐ-cong {x = utxo ᶠᵐ} {utxo' ᶠᵐ}
balance-cong {utxo} {utxo'} eq = indexedSumᵐ-cong {x = (mapValues txOutHash utxo) ᶠᵐ} {(mapValues txOutHash utxo') ᶠᵐ} (map-≡ᵉ eq)

balance-cong-coin : proj₁ utxo ≡ᵉ proj₁ utxo' → cbalance utxo ≡ cbalance utxo'
balance-cong-coin {utxo} {utxo'} x =
Expand All @@ -169,12 +171,13 @@ opaque
balance-∪ {utxo} {utxo'} h = begin
cbalance (utxo ∪ˡ utxo')
≡⟨ ⟦⟧-cong coinIsMonoidHomomorphism
$ indexedSumᵐ-cong {x = (utxo ∪ˡ utxo') ᶠᵐ} {(utxo ᶠᵐ) ∪ˡᶠ (utxo' ᶠᵐ)} (id , id)
$ indexedSumᵐ-cong {x = (mapValues txOutHash (utxo ∪ˡ utxo')) ᶠᵐ} {((mapValues txOutHash utxo) ᶠᵐ) ∪ˡᶠ ((mapValues txOutHash utxo') ᶠᵐ)} (disjoint-∪ˡ-mapValues {M = utxo} {utxo'} _ h)
⟩
coin (indexedSumᵐ _ ((utxo ᶠᵐ) ∪ˡᶠ (utxo' ᶠᵐ)))
coin (indexedSumᵐ _ (((mapValues txOutHash utxo) ᶠᵐ) ∪ˡᶠ ((mapValues txOutHash utxo') ᶠᵐ)))
≡⟨ ⟦⟧-cong coinIsMonoidHomomorphism
$ indexedSumᵐ-∪ {X = utxo ᶠᵐ} {utxo' ᶠᵐ} h
⟩
$ indexedSumᵐ-∪ {X = (mapValues txOutHash utxo) ᶠᵐ} {(mapValues txOutHash utxo') ᶠᵐ}
(λ x x₁ → h (dom-mapʳ⊆ x) (dom-mapʳ⊆ x₁))
⟩
coin (balance utxo + balance utxo')
≡⟨ ∙-homo-Coin _ _ ⟩
cbalance utxo + cbalance utxo'
Expand Down Expand Up @@ -718,7 +721,5 @@ module _
balIn balOut : Value
balIn = balance (st ∣ txins)
balOut = balance (outs txb)

\end{code}
\end{property}

0 comments on commit bdab128

Please sign in to comment.