Merge branch 'master' into 467-preservation-of-value-for-ledger

src/Interface/Hashable.agda

@@ -3,7 +3,6 @@ module Interface.Hashable where
 
 open import Agda.Builtin.Equality
 open import Agda.Primitive using () renaming (Set to Type)
-open import Function.Definitions using (Injective)
 
 record Hashable (T THash : Type) : Type where
   field hash    : T → THash

src/Ledger/Certs/Properties.agda

@@ -15,7 +15,7 @@ open import Ledger.GovernanceActions gs hiding (yes; no)
 open import Ledger.Certs gs
 
 open import Data.Nat.Properties using (+-0-monoid; +-0-commutativeMonoid; +-identityʳ; +-identityˡ)
-open import Axiom.Set.Properties
+open import Axiom.Set.Properties th
 open import Relation.Binary using (IsEquivalence)
 open Computational ⦃...⦄
 
@@ -183,87 +183,89 @@ module _  { indexedSumᵛ'-∪ :  {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ C
     (CERT-deleg (DELEG-dereg {c = c} {rwds} {vDelegs = vDelegs}{sDelegs} x)) = begin
     getCoin ⟦ ⟦ vDelegs , sDelegs , rwds ⟧ᵈ , stᵖ , stᵍ ⟧ᶜˢ
       ≡˘⟨ ≡ᵉ-getCoin rwds-∪ˡ-decomp rwds
-          ( ≡ᵉ.trans rwds-∪ˡ-∪ (≡ᵉ.trans (∪-sym th) (res-ex-∪ (Dec-∈-singleton th))) ) ⟩
+          ( ≡ᵉ.trans rwds-∪ˡ-∪ (≡ᵉ.trans ∪-sym (res-ex-∪ Dec-∈-singleton)) ) ⟩
     getCoin rwds-∪ˡ-decomp
       ≡⟨ ≡ᵉ-getCoin rwds-∪ˡ-decomp ((rwds ∣ ❴ c ❵ ᶜ) ∪ˡ ❴ (c , 0) ❵ᵐ) rwds-∪ˡ≡sing-∪ˡ  ⟩
     getCoin ((rwds ∣ ❴ c ❵ ᶜ) ∪ˡ ❴ (c , 0) ❵ᵐ )
       ≡⟨ ∪ˡsingleton0≡ (rwds ∣ ❴ c ❵ ᶜ) ⟩
     getCoin ⟦ ⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ ⟧ᵈ , stᵖ' , stᵍ' ⟧ᶜˢ
       ∎
     where
-    module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence th  {Credential × Coin})
+    module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin})
     rwds-∪ˡ-decomp = (rwds ∣ ❴ c ❵ ᶜ) ∪ˡ (rwds ∣ ❴ c ❵ )
 
     rwds-∪ˡ-∪ : rwds-∪ˡ-decomp ˢ ≡ᵉ (rwds ∣ ❴ c ❵ ᶜ)ˢ ∪ (rwds ∣ ❴ c ❵)ˢ
-    rwds-∪ˡ-∪ = disjoint-∪ˡ-∪ (disjoint-sym th res-ex-disjoint)
+    rwds-∪ˡ-∪ = disjoint-∪ˡ-∪ (disjoint-sym res-ex-disjoint)
 
     disj : disjoint (dom ((rwds ∣ ❴ c ❵ˢ ᶜ) ˢ)) (dom (❴ c , 0 ❵ᵐ ˢ))
     disj {a} a∈res a∈dom  = res-comp-dom a∈res (dom-single→single a∈dom)
 
     rwds-∪ˡ≡sing-∪ˡ : rwds-∪ˡ-decomp ˢ ≡ᵉ ((rwds ∣ ❴ c ❵ ᶜ) ∪ˡ ❴ (c , 0) ❵ᵐ )ˢ
     rwds-∪ˡ≡sing-∪ˡ = ≡ᵉ.trans rwds-∪ˡ-∪
-                              ( ≡ᵉ.trans (∪-cong th ≡ᵉ.refl (res-singleton'{m = rwds} $ proj₁ x))
+                              ( ≡ᵉ.trans (∪-cong ≡ᵉ.refl (res-singleton'{m = rwds} $ proj₁ x))
                                          (≡ᵉ.sym $ disjoint-∪ˡ-∪ disj) )
   CERT-pov (CERT-pool x) = refl
   CERT-pov (CERT-vdel x) = refl
 
   module _
-    -- TODO: prove some or all of the following assumptions, needed for proof of `CERTBASE-pov`.
-    {sumConstZero  :  {A : Type} ⦃ _ : DecEq A ⦄ {X : ℙ A} → ∑[ x ← constMap X 0 ] x ≡ 0}
-    {res-decomp    :  {A : Type} ⦃ _ : DecEq A ⦄ {m m' : A ⇀ Coin }
-                      → ((m ∪ˡ m')ˢ) ≡ᵉ ((m ∪ˡ (m' ∣ (dom (m ˢ)) ᶜ))ˢ) }
-    {getCoin-cong  :  ∀ {A} → ⦃ _ : DecEq A ⦄ (s : A ⇀ Coin) (s' : ℙ (A × Coin))
-                      → s ˢ ≡ᵉ s' → indexedSum' proj₂ (s ˢ) ≡ indexedSum' proj₂ s' }
-    {≡ᵉ-getCoinˢ   :  {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin))
-                      {f : A → A'} {injOn : InjectiveOn (dom s) f }
-                      → getCoin (mapˢ (map₁ f) s) ≡ getCoin s }
-    {injOn         :  {wdls : RwdAddr ⇀ Coin} → InjectiveOn (dom (wdls ˢ)) RwdAddr.stake}
-    {decCC         :  {X : ℙ (Credential × Coin)} → Decidable¹ (λ x → _∈_ {B = Credential} x (dom X))}
+    -- TODO: prove some or all of the following assumptions, used in roof of `CERTBASE-pov`.
+    ( sumConstZero : {A : Type} ⦃ _ : DecEq A ⦄ {X : ℙ A} → getCoin (constMap X 0) ≡ 0 )
+
+    ( res-decomp : {A : Type} ⦃ _ : DecEq A ⦄ {m m' : A ⇀ Coin}
+                   → (m ∪ˡ m')ˢ ≡ᵉ (m ∪ˡ (m' ∣ dom (m ˢ) ᶜ))ˢ )
+
+    ( getCoin-cong : {A : Type} → ⦃ _ : DecEq A ⦄ (s : A ⇀ Coin) (s' : ℙ (A × Coin))
+                     → s ˢ ≡ᵉ s' → indexedSum' proj₂ (s ˢ) ≡ indexedSum' proj₂ s' )
+
+    ( ≡ᵉ-getCoinˢ : {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'}
+                    → InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s )
+
+    ( injOn : {wdls : RwdAddr ⇀ Coin} → InjectiveOn (dom (wdls ˢ)) RwdAddr.stake )
     where
 
-    CERTBASE-pov : {s s' : CertState} → Γ ⊢ s ⇀⦇ _ ,CERTBASE⦈ s' → getCoin s ≡ getCoin s' + getCoin (CertEnv.wdrls Γ)
+    CERTBASE-pov :  {s s' : CertState} → Γ ⊢ s ⇀⦇ _ ,CERTBASE⦈ s'
+                    → getCoin s ≡ getCoin s' + getCoin (CertEnv.wdrls Γ)
 
-    CERTBASE-pov  {Γ = Γ}{s = ⟦ ⟦ voteDelegs , stakeDelegs , rewards ⟧ᵈ , stᵖ , ⟦ dreps , ccHotKeys ⟧ᵛ ⟧ᶜˢ}
-                  {⟦ ⟦ voteDelegs , stakeDelegs , rewards' ⟧ᵈ , stᵖ , stᵍ ⟧ᶜˢ}
+    CERTBASE-pov  {s  = ⟦ ⟦ _ , _ , rewards  ⟧ᵈ , stᵖ , ⟦ dreps , ccHotKeys ⟧ᵛ ⟧ᶜˢ}
+                  {s' = ⟦ ⟦ _ , _ , rewards' ⟧ᵈ , stᵖ , stᵍ ⟧ᶜˢ}
                   (CERT-base {pp}{vs}{e}{dreps}{wdrls} (_ , wdrlsCC⊆rwds)) =
       let
-        module ≡ᵉ       = IsEquivalence (≡ᵉ-isEquivalence th  {Credential × Coin})
+        module ≡ᵉ       = IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin})
         wdrlsCC         = mapˢ (map₁ RwdAddr.stake) (wdrls ˢ)
-        wdrlsCC≡wdrls   = ≡ᵉ-getCoinˢ (wdrls ˢ) {RwdAddr.stake} {injOn{wdls = wdrls}}
-        domWdrls∣stake  = mapˢ RwdAddr.stake (dom wdrls)
-        zeroMap         = (constMap domWdrls∣stake 0)
+        zeroMap         = constMap (mapˢ RwdAddr.stake (dom wdrls)) 0
         rwds-∪ˡ-decomp  = (rewards ∣ dom wdrlsCC ᶜ) ∪ˡ (rewards ∣ dom wdrlsCC)
-        disj            = disjoint-sym th res-ex-disjoint
       in
         begin
           getCoin rewards
             ≡˘⟨ ≡ᵉ-getCoin rwds-∪ˡ-decomp rewards
-                ( ≡ᵉ.trans (disjoint-∪ˡ-∪ disj) (≡ᵉ.trans (∪-sym th) (res-ex-∪ decCC)) ) ⟩
+                ( ≡ᵉ.trans (disjoint-∪ˡ-∪ (disjoint-sym res-ex-disjoint))
+                           (≡ᵉ.trans ∪-sym (res-ex-∪ (_∈? dom wdrlsCC))) ) ⟩
           getCoin rwds-∪ˡ-decomp
-            ≡⟨ indexedSumᵛ'-∪ (rewards ∣ dom wdrlsCC ᶜ) (rewards ∣ dom wdrlsCC) disj ⟩
-          getCoin ((rewards ∣ dom wdrlsCC ᶜ)) + getCoin (rewards ∣ dom wdrlsCC )
-            ≡⟨ cong (getCoin ((rewards ∣ dom wdrlsCC ᶜ)) +_)
+            ≡⟨ indexedSumᵛ'-∪ (rewards ∣ dom wdrlsCC ᶜ) (rewards ∣ dom wdrlsCC)
+                              (disjoint-sym res-ex-disjoint) ⟩
+          getCoin (rewards ∣ dom wdrlsCC ᶜ) + getCoin (rewards ∣ dom wdrlsCC )
+            ≡⟨ cong (getCoin (rewards ∣ dom wdrlsCC ᶜ) +_)
                ( getCoin-cong (rewards ∣ dom wdrlsCC) wdrlsCC (res-subset{m = rewards} wdrlsCC⊆rwds) ) ⟩
-          getCoin ((rewards ∣ dom wdrlsCC ᶜ)) + getCoin wdrlsCC
-            ≡⟨ cong (getCoin ((rewards ∣ dom wdrlsCC ᶜ)) +_) wdrlsCC≡wdrls ⟩
-          getCoin ((rewards ∣ dom wdrlsCC ᶜ)) + getCoin wdrls
+          getCoin (rewards ∣ dom wdrlsCC ᶜ) + getCoin wdrlsCC
+            ≡⟨ cong (getCoin (rewards ∣ dom wdrlsCC ᶜ) +_) (≡ᵉ-getCoinˢ (wdrls ˢ) (injOn {wdrls})) ⟩
+          getCoin (rewards ∣ dom wdrlsCC ᶜ) + getCoin wdrls
             ≡˘⟨ cong (_+ getCoin wdrls)
                 ( begin
                   getCoin (zeroMap ∪ˡ rewards)
                     ≡⟨ ≡ᵉ-getCoin (zeroMap ∪ˡ rewards) (zeroMap ∪ˡ (rewards ∣ dom zeroMap ᶜ))
                                   (res-decomp {m = zeroMap}{rewards}) ⟩
-                  getCoin (zeroMap ∪ˡ (rewards ∣ (dom zeroMap) ᶜ))
-                    ≡⟨ indexedSumᵛ'-∪  zeroMap (rewards ∣ (dom zeroMap) ᶜ)
-                                       (disjoint-sym th res-comp-dom) ⟩
-                  getCoin zeroMap + getCoin (rewards ∣ (dom zeroMap) ᶜ)
-                    ≡⟨ cong (λ u → u + getCoin (rewards ∣ (dom zeroMap) ᶜ)) sumConstZero ⟩
+                  getCoin (zeroMap ∪ˡ (rewards ∣ dom zeroMap ᶜ))
+                    ≡⟨ indexedSumᵛ'-∪ zeroMap (rewards ∣ dom zeroMap ᶜ)
+                                      (disjoint-sym res-comp-dom) ⟩
+                  getCoin zeroMap + getCoin (rewards ∣ dom zeroMap ᶜ)
+                    ≡⟨ cong (λ u → u + getCoin (rewards ∣ dom zeroMap ᶜ)) sumConstZero ⟩
                   0 + getCoin (rewards ∣ (dom zeroMap) ᶜ)
-                    ≡⟨ +-identityˡ (getCoin (rewards ∣ (dom zeroMap) ᶜ)) ⟩
+                    ≡⟨ +-identityˡ (getCoin (rewards ∣ dom zeroMap ᶜ)) ⟩
                   getCoin (rewards ∣ dom zeroMap ᶜ)
-                    ≡⟨ ≡ᵉ-getCoin (rewards ∣ (dom zeroMap) ᶜ) (rewards ∣ dom wdrlsCC ᶜ)
+                    ≡⟨ ≡ᵉ-getCoin (rewards ∣ dom zeroMap ᶜ) (rewards ∣ dom wdrlsCC ᶜ)
                        ( res-comp-cong
-                         ( ⊆-Transitive th (proj₁ constMap-dom) (proj₂ dom-mapˡ≡map-dom)
-                         , ⊆-Transitive th (proj₁ dom-mapˡ≡map-dom) (proj₂ constMap-dom) ) ) ⟩
+                         ( ⊆-Transitive (proj₁ constMap-dom) (proj₂ dom-mapˡ≡map-dom)
+                         , ⊆-Transitive (proj₁ dom-mapˡ≡map-dom) (proj₂ constMap-dom) ) ) ⟩
                   getCoin (rewards ∣ dom wdrlsCC ᶜ)
                     ∎ ) ⟩
           getCoin (zeroMap ∪ˡ rewards) + getCoin wdrls

src/Ledger/Conway/Conformance/Foreign/HSLedger/Core.agda

@@ -130,20 +130,20 @@ instance
   HSScriptStructure : ScriptStructure
   HSScriptStructure = record
     { hashRespectsUnion = hashRespectsUnion
-    ; ps = HSP2ScriptStructure }
+    ; ps = HSP2ScriptStructure
+    }
     where
-    postulate
-      instance Hashable-Timelock : Hashable Timelock ℕ
-
       hashRespectsUnion : ∀ {A B ℍ}
         → Hashable A ℍ → Hashable B ℍ
         → Hashable (A ⊎ B) ℍ
-
-    HSP2ScriptStructure : PlutusStructure
-    HSP2ScriptStructure = record
-      { Implementation
-      ; validPlutusScript = λ _ _ _ _ → ⊤
-      }
+      hashRespectsUnion a _ .hash (inj₁ x) = hash ⦃ a ⦄ x
+      hashRespectsUnion _ b .hash (inj₂ y) = hash ⦃ b ⦄ y
+
+      HSP2ScriptStructure : PlutusStructure
+      HSP2ScriptStructure = record
+        { Implementation
+        ; validPlutusScript = λ _ _ _ _ → ⊤
+        }
 
 open import Ledger.Conway.Conformance.PParams it it it hiding (Acnt; DrepThresholds; PoolThresholds)
 

src/Ledger/Conway/Conformance/Foreign/HSLedger/Transaction.agda

@@ -17,6 +17,9 @@ instance
   {-# TERMINATING #-}
   Conv-Timelock = autoConvert Timelock
 
+  HsTy-HashedTimelock = autoHsType HashedTimelock
+  Conv-HashedTimelock = autoConvert HashedTimelock
+
   HsTy-TxWitnessess = autoHsType TxWitnesses ⊣ withConstructor "MkTxWitnesses"
   Conv-TxWitnessess = autoConvert TxWitnesses
 

src/Ledger/Conway/Conformance/Foreign/HSLedger/Utxo.agda

@@ -1,5 +1,7 @@
 module Ledger.Conway.Conformance.Foreign.HSLedger.Utxo where
 
+open import Data.String.Base renaming (_++_ to _+ˢ_) hiding (show; length)
+
 open import Ledger.Conway.Conformance.Foreign.HSLedger.Address
 open import Ledger.Conway.Conformance.Foreign.HSLedger.BaseTypes
 open import Ledger.Conway.Conformance.Foreign.HSLedger.Certs
@@ -31,3 +33,26 @@ utxow-step : HsType (UTxOEnv → UTxOState → Tx → ComputationResult String U
 utxow-step = to (compute Computational-UTXOW)
 
 {-# COMPILE GHC utxow-step as utxowStep #-}
+
+utxo-debug : HsType (UTxOEnv → UTxOState → Tx → String)
+utxo-debug env st tx =
+  let open Tx (from tx)
+      open TxBody body
+      open UTxOState (from st)
+      open UTxOEnv (from env)
+   in unlines $
+        "Consumed:" ∷
+        ("\tInputs:      \t" +ˢ show (balance (utxo ∣ txins))) ∷
+        ("\tMint:        \t" +ˢ show mint) ∷
+        ("\tRefunds:     \t" +ˢ show (inject (depositRefunds pparams (from st) body))) ∷
+        ("\tWithdrawals: \t" +ˢ show (inject (getCoin txwdrls))) ∷
+        ("\tTotal:       \t" +ˢ show (consumed pparams (from st) body)) ∷
+        "Produced:" ∷
+        ("\tOutputs:     \t" +ˢ show (balance (outs body))) ∷
+        ("\tDonations:   \t" +ˢ show (inject txdonation)) ∷
+        ("\tDeposits:    \t" +ˢ show (inject (newDeposits pparams (from st) body))) ∷
+        ("\tFees:        \t" +ˢ show (inject txfee)) ∷
+        ("\tTotal:       \t" +ˢ show (produced pparams (from st) body)) ∷
+        []
+
+{-# COMPILE GHC utxo-debug as utxoDebug #-}

src/Ledger/Conway/Conformance/Script.lagda

@@ -152,20 +152,31 @@ instance
         (RequireTimeExpire a) → mapDec evalTEx evalTEx˘ dec
         (RequireMOf m xs)     → mapDec evalMOf evalMOf˘ (MOf-go? m xs)
 
-P1ScriptStructure-TL : ⦃ Hashable Timelock ScriptHash ⦄ → P1ScriptStructure
+record HashedTimelock : Type where
+  field
+    timelock : Timelock
+    storedHash : ScriptHash
+
+instance
+  Hashable-HashedTimelock : Hashable HashedTimelock ScriptHash
+  Hashable-HashedTimelock .hash = HashedTimelock.storedHash
+
+unquoteDecl DecEq-HashedTimelock = derive-DecEq ((quote HashedTimelock , DecEq-HashedTimelock) ∷ [])
+
+P1ScriptStructure-TL : P1ScriptStructure
 P1ScriptStructure-TL = record
-  { P1Script = Timelock
-  ; validP1Script = evalTimelock }
+  { P1Script = HashedTimelock
+  ; validP1Script = λ x y → evalTimelock x y ∘ HashedTimelock.timelock }
 
 record ScriptStructure : Type₁ where
-  field hashRespectsUnion :
-          {A B Hash : Type} → Hashable A Hash → Hashable B Hash → Hashable (A ⊎ B) Hash
-        ⦃ Hash-Timelock ⦄ : Hashable Timelock ScriptHash
-
   p1s : P1ScriptStructure
   p1s = P1ScriptStructure-TL
   open P1ScriptStructure p1s public
 
+  field hashRespectsUnion :
+          {A B Hash : Type} → Hashable A Hash → Hashable B Hash → Hashable (A ⊎ B) Hash
+        ⦃ Hash-Timelock ⦄ : Hashable P1Script ScriptHash
+
   field ps : PlutusStructure
   open PlutusStructure ps public
     renaming ( PlutusScript       to P2Script

src/Ledger/Conway/Conformance/ScriptValidation.agda

@@ -180,5 +180,5 @@ open Tx
 evalScripts : Tx → List (Script × List Data × ExUnits × CostModel) → Bool
 evalScripts tx [] = true
 evalScripts tx ((inj₁ tl , d , eu , cm) ∷ Γ) =
-  ¿ evalTimelock (reqSigHash (body tx)) (txvldt (body tx)) tl ¿ᵇ ∧ evalScripts tx Γ
+  ¿ evalTimelock (reqSigHash (body tx)) (txvldt (body tx)) (HashedTimelock.timelock tl) ¿ᵇ ∧ evalScripts tx Γ
 evalScripts tx ((inj₂ ps , d , eu , cm) ∷ Γ) = ⟦ ps ⟧, cm , eu , d ∧ evalScripts tx Γ

src/Ledger/Conway/Conformance/Utxo.agda

@@ -30,6 +30,8 @@ instance
 
 certDepositUtxo : DCert → PParams → DepositPurpose ⇀ Coin
 certDepositUtxo (regpool kh _)     pp  = ❴ PoolDeposit kh , pp .poolDeposit ❵
+-- This is how RegDeleg certificates are translated in conformance testing
+certDepositUtxo (delegate c nothing nothing v) pp = ❴ CredentialDeposit c , pp .keyDeposit ❵
 certDepositUtxo _                  _   = ∅
 -- -- Handle the following two cases in Certs.Haskell module:
 -- certDeposit (delegate c _ _ v) _   = ❴ CredentialDeposit c , v ❵
@@ -241,6 +243,7 @@ module _ (let open UTxOState; open TxBody) where
     =  balance (st .utxo ∣ txb .txins)
     +  txb .mint
     +  inject (depositRefunds pp st txb)
+    +  inject (getCoin (txb .txwdrls))
 
   produced : PParams → UTxOState → TxBody → Value
   produced pp st txb

src/Ledger/Conway/Conformance/Utxo/Properties.agda

@@ -76,3 +76,18 @@ instance
 
 open Computational ⦃...⦄
 
+private variable
+  tx                               : Tx
+  utxo utxo'                       : UTxO
+  Γ                                : UTxOEnv
+  utxoState utxoState'             : UTxOState
+  fees fees' donations donations'  : Coin
+  deposits deposits'               : DepositPurpose ⇀ Coin
+
+UTXO-step : UTxOEnv → UTxOState → Tx → ComputationResult String UTxOState
+UTXO-step = compute ⦃ Computational-UTXO ⦄
+
+UTXO-step-computes-UTXO  :  UTXO-step Γ utxoState tx ≡ success utxoState'
+                         ⇔  Γ ⊢ utxoState ⇀⦇ tx ,UTXO⦈ utxoState'
+UTXO-step-computes-UTXO = ≡-success⇔STS ⦃ Computational-UTXO ⦄
+

src/Ledger/Set/Theory.agda

@@ -17,7 +17,7 @@ opaque
   List-Modelᵈ = L.List-Modelᵈ
 
 private variable
-  A B C : Set
+  A A' B C : Set
 
 open Theoryᵈ List-Modelᵈ public
   renaming (Set to ℙ_; filter to filterˢ?; map to mapˢ)
@@ -133,7 +133,7 @@ indexedSum' f s = indexedSum ⦃ fromCommMonoid' it ⦄ f (s ᶠˢ)
 syntax indexedSumᵛ' (λ a → x) m = ∑[ a ← m ] x
 syntax indexedSum'  (λ a → x) m = ∑ˢ[ a ← m ] x
 
-opaque
+opaque 
   unfolding List-Model
 
   singleton-≢-∅ : ∀ {a} {x : a} → ⦃ DecEq a ⦄ → singleton x ≢ ∅

src/Ledger/hs-src/Lib.hs

@@ -11,7 +11,8 @@ import MAlonzo.Code.Ledger.Conway.Conformance.Foreign.HSLedger.PParams     as X
   (DrepThresholds(..), PoolThresholds(..), Acnt(..), PParams(..), PParamsUpdate(..))
 import MAlonzo.Code.Ledger.Conway.Conformance.Foreign.HSLedger.Transaction as X
   ( Tag(..), Timelock(..), TxWitnesses(..), TxBody(..), Tx(..), TxId, Ix, TxIn, P1Script, P2Script
-  , Script, Datum, DataHash, Value, TxOut, RdmrPtr, ScriptHash, AuxiliaryData, Wdrl)
+  , Script, Datum, DataHash, Value, TxOut, RdmrPtr, ScriptHash, AuxiliaryData, Wdrl
+  , HashedTimelock(..))
 import MAlonzo.Code.Ledger.Conway.Conformance.Foreign.HSLedger.Cert        as X
   (certStep, certsStep, CertState(..))
 import MAlonzo.Code.Ledger.Conway.Conformance.Foreign.HSLedger.Chain       as X
@@ -33,7 +34,7 @@ import MAlonzo.Code.Ledger.Conway.Conformance.Foreign.HSLedger.NewEpoch    as X
 import MAlonzo.Code.Ledger.Conway.Conformance.Foreign.HSLedger.Ratify      as X
   (StakeDistrs(..), RatifyEnv(..), RatifyState(..), ratifyStep, ratifyDebug)
 import MAlonzo.Code.Ledger.Conway.Conformance.Foreign.HSLedger.Utxo        as X
-  (UTxOEnv(..), UTxOState(..), UTxO, utxoStep, utxowStep, Redeemer)
+  (UTxOEnv(..), UTxOState(..), UTxO, utxoStep, utxowStep, Redeemer, utxoDebug)
 import MAlonzo.Code.Ledger.Conway.Conformance.Foreign.HSLedger.BaseTypes   as X
   (Coin, ExUnits, Epoch)
 

src/ScriptVerification/HelloWorld.agda

@@ -10,16 +10,16 @@ scriptImp = record { serialise = id ;
 
 open import ScriptVerification.LedgerImplementation String String scriptImp
 open import ScriptVerification.Lib String String scriptImp
-open import Ledger.ScriptValidation SVTransactionStructure SVAbstractFunctions
+open import Ledger.Conway.Conformance.ScriptValidation SVTransactionStructure SVAbstractFunctions
 open import Data.Empty
-open import Ledger.Utxo SVTransactionStructure SVAbstractFunctions
-open import Ledger.Transaction
+open import Ledger.Conway.Conformance.Utxo SVTransactionStructure SVAbstractFunctions
+open import Ledger.Conway.Conformance.Transaction
 open TransactionStructure SVTransactionStructure
-open import Ledger.Types.Epoch
+open import Ledger.Conway.Conformance.Types.Epoch
 open EpochStructure SVEpochStructure
 open Implementation
-open import Ledger.Utxo.Properties SVTransactionStructure SVAbstractFunctions
-open import Ledger.Utxow.Properties SVTransactionStructure SVAbstractFunctions
+open import Ledger.Conway.Conformance.Utxo.Properties SVTransactionStructure SVAbstractFunctions
+open import Ledger.Conway.Conformance.Utxow.Properties SVTransactionStructure SVAbstractFunctions
 
 -- true if redeemer is "Hello World"
 helloWorld' : Maybe String → Maybe String → Bool
@@ -127,7 +127,6 @@ evalFailScript = evalScripts failTx failState
 opaque
   unfolding collectPhaseTwoScriptInputs
   unfolding setToList
-  unfolding Computational-UTXO
   unfolding outs
 
   _ : notEmpty succeedState ≡ ⊤
@@ -157,5 +156,5 @@ opaque
   failExample : ComputationResult String UTxOState
   failExample = UTXO-step initEnv ⟦ initState , 0 , ∅ , 0 ⟧ᵘ  failTx
 
-  _ : failExample ≡ failure "¬ feesOK pp tx utxo ≡ true"
-  _ = refl
+  _ : isFailure failExample
+  _ = _ , refl