[scripts] use HashMap construction

IntersectMBO · Sep 22, 2023 · e4b187e · e4b187e
1 parent 7f5fb02
commit e4b187e
Show file tree

Hide file tree

Showing 9 changed files with 214 additions and 191 deletions.
diff --git a/src/Ledger/Crypto.lagda b/src/Ledger/Crypto.lagda
@@ -4,7 +4,6 @@
 module Ledger.Crypto where
 
 open import Ledger.Prelude hiding (T)
-open import Interface.Hashable public
 
 record isHashableSet (T : Set) : Set₁ where
   constructor mkIsHashableSet

diff --git a/src/Ledger/Prelude.agda b/src/Ledger/Prelude.agda
@@ -15,118 +15,18 @@ open import Prelude public
 
 open import Ledger.Prelude.Base public
 
+open import Data.Product.Ext public
 open import Data.Maybe.Properties.Ext public
-open import Relation.Nullary public
-open import Relation.Unary using () renaming (Decidable to Decidable¹) public
+
 open import Interface.DecEq.Ext public
 open import Interface.HasAdd public
 open import Interface.HasAdd.Instance public
 open import Interface.HasSubtract public
 open import Interface.HasSubtract.Instance public
 open import Interface.Decidable.Instance public
+open import Interface.Hashable public
 open import Interface.ComputationalRelation public
-open import Ledger.Interface.HasCoin public
 open import MyDebugOptions public
 
---------------------------------------------------------------------------------
--- Set theory
-
-open import Axiom.Set
-import Axiom.Set.List as L
-
-abstract
-  List-Model : Theory {0ℓ}
-  List-Model = L.List-Model
-  List-Modelᶠ : Theoryᶠ
-  List-Modelᶠ = L.List-Modelᶠ
-  List-Modelᵈ : Theoryᵈ
-  List-Modelᵈ = L.List-Modelᵈ
-
-open Theoryᵈ List-Modelᵈ renaming (Set to ℙ_; filter to filterˢ) public
-
-abstract
-  open import Axiom.Set.Properties th using (card-≡ᵉ)
-
-  to-sp : {A : Set} {P : A → Set} → Decidable¹ P → specProperty P
-  to-sp = id
-
-  finiteness : ∀ {A} (X : Theory.Set th A) → finite X
-  finiteness = Theoryᶠ.finiteness List-Modelᶠ
-
-  lengthˢ : ∀ {A} ⦃ _ : DecEq A ⦄ (X : Theory.Set th A) → ℕ
-  lengthˢ = Theoryᶠ.lengthˢ List-Modelᶠ
-
-  lengthˢ-≡ᵉ : ∀ {A} ⦃ _ : DecEq A ⦄ (X Y : Theory.Set th A)
-    → X ≡ᵉ Y
-    → lengthˢ X ≡ lengthˢ Y
-  lengthˢ-≡ᵉ X Y X≡Y =
-    card-≡ᵉ (X , Theoryᶠ.DecEq⇒strongly-finite List-Modelᶠ X)
-            (Y , Theoryᶠ.DecEq⇒strongly-finite List-Modelᶠ Y) X≡Y
-
-  lengthˢ-∅ : ∀ {A} ⦃ _ : DecEq A ⦄ → lengthˢ {A} ∅ ≡ 0
-  lengthˢ-∅ = refl
-
-  setToList : {A : Set} → ℙ A → List A
-  setToList = id
-
-  setFromList : {A : Set} → List A → ℙ A
-  setFromList = id
-
-  ≟-∅ : {A : Set} ⦃ _ : DecEq A ⦄ → {X : ℙ A} → Dec (X ≡ ∅)
-  ≟-∅ = L.Decˡ.≟-∅
-
-open import Axiom.Set.Rel th public
-  hiding (_∣'_; _↾'_)
-
-open import Axiom.Set.Map th public
-  renaming (Map to infixr 1 _⇀_)
-
-open import Axiom.Set.TotalMap th public
-open import Axiom.Set.TotalMapOn th
-
-open L.Decˡ public
-  hiding (_∈?_; ≟-∅)
-
-open import Axiom.Set.Sum th public
-open import Axiom.Set.Map.Dec List-Modelᵈ public
-open import Axiom.Set.Factor List-Model public
-
-module _ {A : Set} ⦃ _ : DecEq A ⦄ where
-  open Restriction {A} ∈-sp public
-    renaming (_∣_ to _∣ʳ_; _∣_ᶜ to _∣ʳ_ᶜ)
-
-  open Corestriction {A} ∈-sp public
-    hiding (_↾_; _↾_ᶜ) public
-
-  open Restrictionᵐ {A} ∈-sp public
-  open Corestrictionᵐ {A} ∈-sp public
-  open Unionᵐ {A} ∈-sp public
-  open Intersection {A} ∈-sp public
-  open Lookupᵐ {A} ∈-sp public
-  open Lookupᵐᵈ {A} ∈-sp public
-
-module _ {A B : Set} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq B ⦄ where
-  open Intersectionᵐ {A} {B} ∈-sp public
-
-  open import Algebra using (CommutativeMonoid)
-
-  module _ ⦃ M : CommutativeMonoid 0ℓ 0ℓ ⦄ where
-    open IndexedSumUnionᵐ {A} {B} ∈-sp (_∈? _) public
-
-module Properties where
-  open import Axiom.Set.Properties th public
-  module _ {A : Set} ⦃ _ : DecEq A ⦄ where
-    open Intersectionᵖ {A} ∈-sp public
-
-_ᶠᵐ : {A B : Set} → A ⇀ B → FinMap A B
-(R , uniq) ᶠᵐ = (R , uniq , finiteness _)
-
-open import Data.Product.Ext
-open import Interface.Hashable
-
-setToHashRel : ∀ {A B : Set} → {{Hashable A B}} -> ℙ A -> ℙ (B × A)
-setToHashRel x = mapˡ hash (map ×-dup x)
-
-setToHashMap : ∀ {A B : Set} → {{Hashable A B}} -> ℙ A → B ⇀ A
-setToHashMap x = setToHashRel x ᵐ
-  where instance _ = record { isLeftUnique = mapˡ∘map⦅×-dup⦆-uniq hashInj }
+open import Ledger.Interface.HasCoin public
+open import Ledger.Set public
diff --git a/src/Ledger/ScriptValidation.agda b/src/Ledger/ScriptValidation.agda
@@ -1,63 +1,48 @@
 {-# OPTIONS --safe #-}
-{-# OPTIONS --overlapping-instances #-}
-
-open import Algebra using (CommutativeMonoid)
-open import Algebra.Structures
-open import Data.Integer using (ℤ; _⊖_)
-open import Data.Integer.Ext
-open import Data.List as List hiding (map)
-open import Data.Maybe
-open import Data.Nat using (_≤?_; _≤_)
-open import Data.Nat.Properties using (+-0-monoid ; +-0-commutativeMonoid)
-open import Data.Sign using (Sign)
-open import Data.Bool using (_∧_)
-open import Relation.Nullary.Decidable using (⌊_⌋)
+
+import Data.Maybe as M
 
 open import Interface.Decidable.Instance
 open import Tactic.AnyOf
 open import Tactic.Assumption
 open import Tactic.Defaults
 open import Tactic.Helpers
 
-open import Ledger.Prelude renaming (map to mapSet)
+open import Ledger.Prelude; open Properties
 open import Ledger.Transaction
 open import Ledger.Abstract
 open import Ledger.Script
 open import Ledger.Crypto
 
-open Properties
 
 module Ledger.ScriptValidation
   (txs : _) (open TransactionStructure txs)
   (abs : AbstractFunctions txs) (open AbstractFunctions abs) (open indexOf indexOfImp)
   where
 
-open TxBody
-open TxWitnesses
-open Tx
-
 -- Because of missing macro hygiene, we have to copy&paste this. https://github.com/agda/agda/issues/3819
 private macro
   ∈⇒P = anyOfⁿᵗ (quote ∈-filter⁻' ∷ quote ∈-∪⁻ ∷ quote ∈-map⁻' ∷ quote ∈-fromList⁻ ∷ [])
   P⇒∈ = anyOfⁿᵗ (quote ∈-filter⁺' ∷ quote ∈-∪⁺ ∷ quote ∈-map⁺' ∷ quote ∈-fromList⁺ ∷ [])
   ∈⇔P = anyOfⁿᵗ (quote ∈-filter⁻' ∷ quote ∈-∪⁻ ∷ quote ∈-map⁻' ∷ quote ∈-fromList⁻ ∷ quote ∈-filter⁺' ∷ quote ∈-∪⁺ ∷ quote ∈-map⁺' ∷ quote ∈-fromList⁺ ∷ [])
 
 data ScriptPurpose : Set where
-  Cert  : DCert → ScriptPurpose
-  Rwrd : RwdAddr → ScriptPurpose
+  Cert  : DCert      → ScriptPurpose
+  Rwrd  : RwdAddr    → ScriptPurpose
   Mint  : ScriptHash → ScriptPurpose
-  Spend : TxIn → ScriptPurpose
+  Spend : TxIn       → ScriptPurpose
 
 rdptr : TxBody → ScriptPurpose → Maybe RdmrPtr
-rdptr txb (Cert h) = map (λ x → Cert , x) (indexOfDCert h (txcerts txb))
-rdptr txb (Rwrd h) = map (λ x → Rewrd , x) (indexOfRwdAddr h (txwdrls txb))
-rdptr txb (Mint h) = map (λ x → Mint , x) (indexOfPolicyId h (policies (mint txb)))
-rdptr txb (Spend h) = map (λ x → Spend , x) (indexOfTxIn h (txins txb))
+rdptr txb = λ where
+  (Cert h)  → M.map (Cert  ,_) $ indexOfDCert    h txcerts
+  (Rwrd h)  → M.map (Rewrd ,_) $ indexOfRwdAddr  h txwdrls
+  (Mint h)  → M.map (Mint  ,_) $ indexOfPolicyId h (policies mint)
+  (Spend h) → M.map (Spend ,_) $ indexOfTxIn     h txins
+ where open TxBody txb
 
 indexedRdmrs : Tx → ScriptPurpose → Maybe (Redeemer × ExUnits)
-indexedRdmrs tx sp = maybe (λ x → lookupᵐ? (txrdmrs (wits tx)) x ⦃ _ ∈? _ ⦄)
-                            nothing
-                            (rdptr (body tx) sp)
+indexedRdmrs tx sp = maybe (λ x → lookupᵐ? txrdmrs x ⦃ _ ∈? _ ⦄) nothing (rdptr body sp)
+  where open Tx tx; open TxWitnesses wits
 
 -- Abstract Script Validation Functions
 
@@ -69,12 +54,14 @@ indexedRdmrs tx sp = maybe (λ x → lookupᵐ? (txrdmrs (wits tx)) x ⦃ _ ∈?
 -- Notation
 
 getDatum : Tx → UTxO → ScriptPurpose → List Datum
-getDatum tx utxo (Spend txin) = maybe (λ { (_ , _ , just x) → maybe (λ x₁ → [ x₁ ])
-                                                              []
-                                                              (lookupᵐ? (txdats (wits tx)) x ⦃ _ ∈? _ ⦄)
-                                          ; (_ , _ , nothing) → []})
-                                          []
-                                          ((lookupᵐ? utxo txin ⦃ _ ∈? _ ⦄))
+getDatum tx utxo (Spend txin) = let open Tx tx; open TxWitnesses wits in
+  maybe
+    (λ { (_ , _ , just x) →
+         maybe (λ x₁ → [ x₁ ]) [] (lookupᵐ? txdats x ⦃ _ ∈? _ ⦄)
+       ; (_ , _ , nothing) → []
+       })
+    []
+    (lookupᵐ? utxo txin ⦃ _ ∈? _ ⦄)
 getDatum tx utxo _ = []
 
 
@@ -95,19 +82,13 @@ txInfo : Language → PParams
                   → Tx
                   → TxInfo
 txInfo l pp utxo tx = record
-                        { realizedInputs = utxo ∣ (txins txb)
-                        ; txouts = txouts txb
-                        ; fee = inject (txfee txb)
-                        ; mint = mint txb
-                        ; txcerts = txcerts txb
-                        ; txwdrls = txwdrls txb
-                        ; txvldt = txvldt txb
-                        ; vkKey = reqSigHash txb
-                        ; txdats = txdats (wits tx)
-                        ; txid = txid txb
-                        }
-  where
-    txb = body tx
+  { TxBody body
+  ; TxWitnesses wits
+  ; realizedInputs = utxo ∣ txins
+  ; fee = inject txfee
+  ; mint = mint
+  ; vkKey = reqSigHash
+  } where open Tx tx; open TxBody body
 
 DelegateOrDeReg : DCert → Set
 DelegateOrDeReg (delegate x x₁ x₂ x₃) = ⊤
@@ -154,39 +135,45 @@ certScripts (deregdrep (inj₁ x)) | yes p = nothing
 certScripts (deregdrep (inj₂ y)) | yes p = just (Cert (deregdrep (inj₂ y)) , y)
 
 scriptsNeeded : UTxO → TxBody → ℙ (ScriptPurpose × ScriptHash)
-scriptsNeeded utxo txb = mapPartial (λ x → spendScripts x (scriptOutsWithHash utxo)) (txins txb)
-                         ∪ mapPartial (λ x → rwdScripts x) (dom $ proj₁ $ (txwdrls txb))
-                         ∪ mapPartial (λ x → certScripts x) (setFromList $ txcerts txb)
-                         ∪ mapSet (λ x → (Mint x) , x) (policies (mint txb))
+scriptsNeeded utxo txb
+  = mapPartial (λ x → spendScripts x (scriptOutsWithHash utxo)) txins
+  ∪ mapPartial (λ x → rwdScripts x) (dom $ txwdrls .proj₁)
+  ∪ mapPartial (λ x → certScripts x) (setFromList txcerts)
+  ∪ map (λ x → (Mint x) , x) (policies mint)
+  where open TxBody txb
+
 
 -- We need to add toData to define this
 valContext : TxInfo → ScriptPurpose → Data
 valContext txinfo sp = toData (txinfo , sp)
 
 
 scriptHashInTx : ScriptHash → Tx → Bool
-scriptHashInTx sh tx = ⌊ any? (λ s → hash s ≟ sh) (tx .Tx.wits .TxWitnesses.scripts) ⌋
+scriptHashInTx sh tx = ⌊ sh ∈? map proj₁ (m ˢ) ⌋
+  where m = setToHashMap $ TxWitnesses.scripts (Tx.wits tx)
 
 -- need to get map from language script ↦ cm
 -- need to update costmodels to add the language map in order to check
 -- (Language ↦ CostModel) ∈ costmdls ↦ (Language ↦ CostModel)
 
-collectPhaseTwoScriptInputs' : PParams → Tx
-                                      → UTxO
-                                      → (ScriptPurpose × ScriptHash)
-                                      → Maybe (Script × List Data × ExUnits × CostModel)
-collectPhaseTwoScriptInputs' pp tx utxo (sp , sh) with lookupScriptHash sh tx
+collectPhaseTwoScriptInputs' : PParams → Tx → UTxO → (ScriptPurpose × ScriptHash)
+  → Maybe (Script × List Data × ExUnits × CostModel)
+collectPhaseTwoScriptInputs' pp tx utxo (sp , sh)
+  with lookupScriptHash sh tx
 ... | nothing = nothing
-... | just s with isInj₂ s | indexedRdmrs tx sp
-... | just p2s | just (rdmr , eu) = just (s , (((getDatum tx utxo sp)
-                                                ++ rdmr
-                                                ∷ valContext (txInfo (language p2s) pp utxo tx) sp ∷ [])
-                                                , eu
-                                                , PParams.costmdls pp))
+... | just s
+  with isInj₂ s | indexedRdmrs tx sp
+... | just p2s | just (rdmr , eu)
+    = just (s ,
+        ( (getDatum tx utxo sp ++ rdmr ∷ valContext (txInfo (language p2s) pp utxo tx) sp ∷ [])
+        , eu
+        , PParams.costmdls pp)
+      )
 ... | x | y = nothing
 
-collectPhaseTwoScriptInputs : PParams → Tx
-                                      → UTxO
-                                      → List (Script × List Data × ExUnits × CostModel)
-collectPhaseTwoScriptInputs pp tx utxo with scriptsNeeded utxo (body tx)
-... | ans = setToList $ mapPartial (λ { z → collectPhaseTwoScriptInputs' pp tx utxo z}) ans
+collectPhaseTwoScriptInputs : PParams → Tx → UTxO
+  → List (Script × List Data × ExUnits × CostModel)
+collectPhaseTwoScriptInputs pp tx utxo
+  = setToList
+  $ mapPartial (collectPhaseTwoScriptInputs' pp tx utxo)
+  $ scriptsNeeded utxo (tx .Tx.body)
diff --git a/src/Ledger/Set.agda b/src/Ledger/Set.agda
@@ -0,0 +1,6 @@
+{-# OPTIONS --safe #-}
+
+module Ledger.Set where
+
+open import Ledger.Set.Theory public
+open import Ledger.Set.HashMap public
diff --git a/src/Ledger/Set/HashMap.agda b/src/Ledger/Set/HashMap.agda
@@ -0,0 +1,17 @@
+{-# OPTIONS --safe #-}
+
+module Ledger.Set.HashMap where
+
+open import Prelude
+open import Data.Product.Ext
+open import Interface.Hashable
+open import Ledger.Set.Theory
+
+module _ {A B : Set} ⦃ _ : Hashable A B ⦄ (X : ℙ A) where
+
+  setToHashRel : ℙ (B × A)
+  setToHashRel = mapˡ hash (map ×-dup X)
+
+  setToHashMap : B ⇀ A
+  setToHashMap = setToHashRel ᵐ
+    where instance _ = record { isLeftUnique = mapˡ∘map⦅×-dup⦆-uniq hashInj }