From 31e8c06b6f7508208b1a8217857f59c74d9a3d41 Mon Sep 17 00:00:00 2001
From: William DeMeo <williamdemeo@gmail.com>
Date: Sun, 18 Feb 2024 14:50:17 -0700
Subject: [PATCH] fixed one bug introduced by messing around with open

...still more to fix... maybe have to revert
---
 src/Ledger/Utxo.lagda | 17 ++++++++---------
 1 file changed, 8 insertions(+), 9 deletions(-)

diff --git a/src/Ledger/Utxo.lagda b/src/Ledger/Utxo.lagda
index ceb818862..b40617700 100644
--- a/src/Ledger/Utxo.lagda
+++ b/src/Ledger/Utxo.lagda
@@ -364,9 +364,6 @@ private variable
   s s' : UTxOState
   tx : Tx
 
-open UTxOState
-open UTxOEnv renaming (pparams to pp)
-
 data _⊢_⇀⦇_,UTXO⦈_ where
 \end{code}
 
@@ -375,16 +372,18 @@ data _⊢_⇀⦇_,UTXO⦈_ where
 \begin{code}
   UTXO-inductive :
     let open Tx tx renaming (body to txb); open TxBody txb
+        open UTxOEnv Γ renaming (pparams to pp)
+        open UTxOState s
     in
-    ∙ txins ≢ ∅                              ∙ txins ⊆ dom (s .utxo)
-    ∙ inInterval (Γ .slot) txvldt                 ∙ feesOK (Γ .pp) tx (s .utxo) ≡ true
-    ∙ consumed (Γ .pp) s txb ≡ produced (Γ .pp) s txb  ∙ coin mint ≡ 0
-    ∙ txsize ≤ maxTxSize (Γ .pp)
+    ∙ txins ≢ ∅                              ∙ txins ⊆ 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
+        inject (utxoEntrySize txout * minUTxOValue pp) ≤ᵗ getValue txout
     ∙ ∀[ (_ , txout) ∈ txouts .proj₁ ]
-        serSize (getValue txout) ≤ maxValSize (Γ .pp)
+        serSize (getValue txout) ≤ maxValSize pp
     ∙ ∀[ (a , _) ∈ range txouts ]
         Sum.All (const ⊤) (λ a → a .BootstrapAddr.attrsSize ≤ 64) a
     ∙ ∀[ (a , _) ∈ range txouts ]  netId a         ≡ networkId