working on utxo property proofs

IntersectMBO · Apr 12, 2024 · aec2b47 · aec2b47
1 parent 22999d5
commit aec2b47
Show file tree

Hide file tree

Showing 4 changed files with 48 additions and 552 deletions.
diff --git 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
@@ -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
@@ -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'
       ────────────────────────────────