diff --git a/src/Axiom/Set/Map.agda b/src/Axiom/Set/Map.agda index 9d9ae32f..973cf54b 100644 --- a/src/Axiom/Set/Map.agda +++ b/src/Axiom/Set/Map.agda @@ -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 @@ -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₂ ˢ)) @@ -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 @@ -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) diff --git a/src/Axiom/Set/Properties.agda b/src/Axiom/Set/Properties.agda index 2a336027..54584340 100644 --- a/src/Axiom/Set/Properties.agda +++ b/src/Axiom/Set/Properties.agda @@ -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 _∈ˡ?_) @@ -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 @@ -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) diff --git a/src/Data/Product/Properties/Ext.agda b/src/Data/Product/Properties/Ext.agda index 9969bfb1..50ba789d 100644 --- a/src/Data/Product/Properties/Ext.agda +++ b/src/Data/Product/Properties/Ext.agda @@ -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)) @@ -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) ]) diff --git a/src/Ledger/Script.lagda b/src/Ledger/Script.lagda index 1846b926..dd856006 100644 --- a/src/Ledger/Script.lagda +++ b/src/Ledger/Script.lagda @@ -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 diff --git a/src/Ledger/Transaction.lagda b/src/Ledger/Transaction.lagda index 17277814..15a39823 100644 --- a/src/Ledger/Transaction.lagda +++ b/src/Ledger/Transaction.lagda @@ -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₁)) diff --git a/src/Ledger/Utxo.lagda b/src/Ledger/Utxo.lagda index db58b478..5e2d7edd 100644 --- a/src/Ledger/Utxo.lagda +++ b/src/Ledger/Utxo.lagda @@ -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 @@ -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) @@ -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} @@ -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' ──────────────────────────────── diff --git a/src/Ledger/Utxo/Properties.lagda b/src/Ledger/Utxo/Properties.lagda index 6921a8cd..2eea7e85 100644 --- a/src/Ledger/Utxo/Properties.lagda +++ b/src/Ledger/Utxo/Properties.lagda @@ -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)) = @@ -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 = @@ -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' @@ -718,7 +721,5 @@ module _ balIn balOut : Value balIn = balance (st ∣ txins) balOut = balance (outs txb) - \end{code} \end{property} - diff --git a/src/ScriptVerification/HelloWorld.agda b/src/ScriptVerification/HelloWorld.agda index a32a2ac2..bdcdde9c 100644 --- a/src/ScriptVerification/HelloWorld.agda +++ b/src/ScriptVerification/HelloWorld.agda @@ -36,7 +36,7 @@ initTxOut : TxOut initTxOut = inj₁ (record { net = tt ; pay = inj₂ 777 ; stake = inj₂ 777 }) - , 10 , nothing + , 10 , nothing , nothing script : TxIn × TxOut script = (6 , 6) , initTxOut @@ -47,12 +47,13 @@ initState = fromList' (script ∷ (createInitUtxoState 5 1000000000000)) succeedTx : Tx succeedTx = record { body = record { txins = Ledger.Prelude.fromList ((6 , 6) ∷ (5 , 5) ∷ []) + ; refInputs = ∅ ; txouts = fromListIx ((6 , initTxOut) ∷ (5 , ((inj₁ (record { net = tt ; pay = inj₁ 5 ; stake = inj₁ 5 })) - , (1000000000000 - 10000000000) , nothing)) + , (1000000000000 - 10000000000) , nothing , nothing)) ∷ []) ; txfee = 10000000000 ; mint = 0 @@ -83,6 +84,7 @@ succeedTx = record { body = record failTx : Tx failTx = record { body = record { txins = Ledger.Prelude.fromList ((6 , 6) ∷ []) + ; refInputs = ∅ ; txouts = ∅ ; txfee = 10 ; mint = 0 @@ -126,6 +128,9 @@ opaque unfolding Computational-UTXO unfolding outs + _ : notEmpty succeedState ≡ ⊤ + _ = refl + -- need to check that the state is non-empty otherwise evalScripts will always return true _ : notEmpty succeedState ≡ ⊤ _ = refl diff --git a/src/ScriptVerification/Lib.agda b/src/ScriptVerification/Lib.agda index 0eaaeb0e..efdddcf7 100644 --- a/src/ScriptVerification/Lib.agda +++ b/src/ScriptVerification/Lib.agda @@ -70,11 +70,11 @@ createEnv s = record { slot = s ; createUTxO : (index : ℕ) → (wallet : ℕ) → (value : Value) - → (Maybe D) + → Maybe (D ⊎ DataHash) → TxIn × TxOut createUTxO index wallet value d = (index , index) , (inj₁ (record { net = tt ; pay = inj₁ wallet ; stake = inj₁ wallet }) - , value , d) + , value , d , nothing) createInitUtxoState : (wallets : ℕ) → (value : Value) diff --git a/src/ScriptVerification/SucceedIfNumber.agda b/src/ScriptVerification/SucceedIfNumber.agda index 2d9a696d..8248533c 100644 --- a/src/ScriptVerification/SucceedIfNumber.agda +++ b/src/ScriptVerification/SucceedIfNumber.agda @@ -45,14 +45,14 @@ initTxOut : TxOut initTxOut = inj₁ (record { net = tt ; pay = inj₂ 777 ; stake = inj₂ 777 }) - , 10 , just 99 + , 10 , just (inj₂ 99) , nothing -- initTxOut for script without datum reference initTxOut' : TxOut initTxOut' = inj₁ (record { net = tt ; pay = inj₂ 888 ; stake = inj₂ 888 }) - , 10 , nothing + , 10 , nothing , nothing scriptDatum : TxIn × TxOut scriptDatum = (6 , 6) , initTxOut @@ -66,43 +66,16 @@ initStateDatum = fromList' (scriptDatum ∷ (createInitUtxoState 5 1000000000000 initStateRedeemer : UTxO initStateRedeemer = fromList' (scriptRedeemer ∷ (createInitUtxoState 5 1000000000000)) -exTx : Tx -exTx = record { body = record - { txins = ∅ - ; txouts = fromListIx ((6 , initTxOut) ∷ []) - ; txfee = 10 - ; mint = 0 - ; txvldt = nothing , nothing - ; txcerts = [] - ; txwdrls = ∅ - ; txvote = [] - ; txprop = [] - ; txdonation = 0 - ; txup = nothing - ; txADhash = nothing - ; netwrk = just tt - ; txsize = 10 - ; txid = 6 - ; collateral = ∅ - ; reqSigHash = ∅ - ; scriptIntHash = nothing - } ; - wits = record { vkSigs = ∅ ; - scripts = ∅ ; - txdats = ∅ ; - txrdmrs = ∅ } ; - isValid = false ; - txAD = nothing } - succeedTx : Tx succeedTx = record { body = record { txins = Ledger.Prelude.fromList ((6 , 6) ∷ (5 , 5) ∷ []) + ; refInputs = ∅ ; txouts = fromListIx ((6 , initTxOut) ∷ (5 , ((inj₁ (record { net = tt ; pay = inj₁ 5 ; stake = inj₁ 5 })) - , (1000000000000 - 10000000000) , nothing)) + , (1000000000000 - 10000000000) , nothing , nothing)) ∷ []) ; txfee = 10000000000 ; mint = 0 @@ -137,6 +110,7 @@ exampleDatum = getDatum succeedTx initStateDatum (Spend (6 , 6)) failTx : Tx failTx = record { body = record { txins = Ledger.Prelude.fromList ((6 , 6) ∷ []) + ; refInputs = ∅ ; txouts = ∅ ; txfee = 10 ; mint = 0 @@ -175,7 +149,7 @@ opaque unfolding Computational-UTXO unfolding outs - gotScript : lookupScriptHash 777 succeedTx ≡ just (inj₂ succeedIf1Datum) + gotScript : lookupScriptHash 777 succeedTx initStateDatum ≡ just (inj₂ succeedIf1Datum) gotScript = refl _ : exampleDatum ≡ 1 ∷ []