[Dijkstra] UTXOW: Implement languages and allowedLanguages (#1038)

* Move getLanguage to Script

* Add allowedLanguages and languages

Author: carlostome

src-lib-exts/stdlib/Data/List.agda

@@ -0,0 +1,9 @@
+{-# OPTIONS --safe --without-K #-}
+module stdlib.Data.List where
+
+open import Data.List
+open import Data.List.Relation.Unary.All
+open import Data.Empty
+
+Is-[] : ∀ {A : Set} → List A → Set
+Is-[] = All (λ _ → ⊥)

src/Ledger/Conway/Specification/Script/Base.lagda.md

@@ -108,4 +108,7 @@ record ScriptStructure : Type₁ where
 
   toP2Script : Script → Maybe P2Script
   toP2Script = isInj₂
+
+  getLanguage : Script → Maybe Language
+  getLanguage s = toP2Script s <&> language
 ```

src/Ledger/Conway/Specification/Utxow.lagda.md

@@ -68,10 +68,6 @@ instance
 
 languages : Tx → UTxO → ℙ Language
 languages tx utxo = mapPartial getLanguage (txscripts tx utxo)
-  where
-    getLanguage : Script → Maybe Language
-    getLanguage (inj₁ _) = nothing
-    getLanguage (inj₂ s) = just (language s)
 ```
 -->
 

src/Ledger/Dijkstra/Specification/Utxow.lagda.md

@@ -30,12 +30,85 @@ private variable
 ```
 -->
 
+## Witnessing Functions {#sec:witnessing-functions}
+
 ```agda
-languages : Tx ℓ → UTxO → ℙ Language
-languages tx utxo = ∅ -- TODO
+module _ (tx : TopLevelTx) where
+  open Tx tx
+  open TxBody txBody
+
+  module _ (utxo : UTxO) where
+    UsesBootstrapAddress : Type
+    UsesBootstrapAddress = ∃[ o ∈ (range txOuts) ∪ range (utxo ∣ (txIns ∪ refInputs)) ] isBootstrapAddr (proj₁ o)
+
+    HasInlineDatum : TxOut → Type
+    HasInlineDatum txout = Is-just (txOutToDatum txout)
+
+    UsesV2Features : Type
+    UsesV2Features = ∃[ o ∈ (range txOuts) ∪ range (utxo ∣ (txIns ∪ refInputs)) ] HasInlineDatum o
+
+  data UsesV3Features : Set where
+    hasVotes     : ¬ (Is-[] txGovVotes)     → UsesV3Features
+    hasProposals : ¬ (Is-[] txGovProposals) → UsesV3Features
+    hasDonation  : NonZero txDonation       → UsesV3Features
+    hasTreasure  : Is-just currentTreasury  → UsesV3Features
+
+  data UsesV4Features : Set where
+    hasSubtransactions  : ¬ (Is-[] txSubTransactions) → UsesV4Features
+    hasGuards           : ¬ (Is-∅ txGuards)           → UsesV4Features
+```
 
-allowedLanguages : Tx ℓ → UTxO → ℙ Language
-allowedLanguages tx utxo = ∅ -- TODO
+<!--
+```agda
+module _ {tx : TopLevelTx} where
+  open Tx tx
+  open TxBody txBody
+
+  instance
+    Dec-UsesV3Features : UsesV3Features tx ⁇
+    Dec-UsesV3Features .dec
+      with ¿ ¬ (Is-[] txGovVotes) ¿ | ¿ ¬ (Is-[] txGovProposals) ¿
+         | ¿ NonZero txDonation   ¿ | ¿ Is-just currentTreasury  ¿
+    ... | yes p | _ | _ | _ = yes (hasVotes p)
+    ... | _ | yes p | _ | _ = yes (hasProposals p)
+    ... | _ | _ | yes p | _ = yes (hasDonation p)
+    ... | _ | _ | _ | yes p = yes (hasTreasure p)
+    ... | no p₁ | no p₂ | no p₃ | no p₄
+      = no λ { (hasVotes x) → p₁ x ; (hasProposals x) → p₂ x ; (hasDonation x) → p₃ x ; (hasTreasure x) → p₄ x}
+
+module _ {tx : TopLevelTx} where
+  open Tx tx
+  open TxBody txBody
+
+  instance
+    Dec-UsesV4Features : UsesV4Features tx ⁇
+    Dec-UsesV4Features .dec
+      with ¿ ¬ (Is-[] txSubTransactions) ¿ | ¿ ¬ (Is-∅ txGuards) ¿
+    ... | yes p | _ = yes (hasSubtransactions p)
+    ... | _ | yes p = yes (hasGuards p)
+    ... | no p₁ | no p₂
+      = no λ { (hasSubtransactions x) → p₁ x ; (hasGuards x) → p₂ x}
+```
+-->
+
+```agda
+languages :  ℙ P2Script → ℙ Language
+languages p2Scripts = mapˢ language p2Scripts
+
+allowedLanguages : TopLevelTx → UTxO → ℙ Language
+allowedLanguages tx utxo =
+  if UsesBootstrapAddress tx utxo
+    then ∅
+    else
+  if UsesV4Features tx
+    then fromList (PlutusV4 ∷ [])
+    else
+  if UsesV3Features tx
+    then fromList (PlutusV4 ∷ PlutusV3 ∷ [])
+    else
+  if UsesV2Features tx utxo
+    then fromList (PlutusV4 ∷ PlutusV3 ∷ PlutusV2 ∷ [])
+    else fromList (PlutusV4 ∷ PlutusV3 ∷ PlutusV2 ∷ PlutusV1 ∷ [])
 ```
 
 ```agda
@@ -78,7 +151,6 @@ data _⊢_⇀⦇_,SUBUTXOW⦈_ : UTxOEnv → UTxOState → SubLevelTx → UTxOSt
     ∙  neededVKeyHashes ⊆ witsKeyHashes
     ∙  neededScriptHashes ⊆ mapˢ hash p1Scripts ∪ mapˢ hash p2Scripts
     ∙  neededDataHashes ⊆ dom (Γ .globalData)
-    ∙  languages tx utxo ⊆ allowedLanguages tx utxo
     ∙  txADhash ≡ map hash txAuxData
     ∙ Γ ⊢ s ⇀⦇ stx ,SUBUTXO⦈ s'
       ────────────────────────────────
@@ -123,7 +195,7 @@ data _⊢_⇀⦇_,UTXOW⦈_ : UTxOEnv → UTxOState → TopLevelTx → UTxOState
     ∙  neededVKeyHashes ⊆ witsKeyHashes
     ∙  neededScriptHashes ⊆ mapˢ hash p1Scripts ∪ mapˢ hash p2Scripts
     ∙  neededDataHashes ⊆ dom (Γ .globalData)
-    ∙  languages tx utxo ⊆ allowedLanguages tx utxo
+    ∙  languages p2Scripts ⊆ allowedLanguages tx utxo
     ∙  txADhash ≡ map hash txAuxData
     ∙  Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s'
       ────────────────────────────────

src/Ledger/Prelude.lagda.md

@@ -90,4 +90,7 @@ lookupHash : ∀ {T H : Type} ⦃ _ : DecEq H ⦄ ⦃ _ : Hashable T H ⦄ → H
 lookupHash h s =
   if h ∈ mapˢ proj₁ (m ˢ) then just (lookupᵐ m h) else nothing
   where m = setToMap (mapˢ < hash , id > s)
+
+Is-∅ : {A : Type} → ℙ A → Type
+Is-∅ X = Is-[] (setToList X)
 ```

src/Prelude.lagda.md

@@ -21,6 +21,8 @@ open import Data.Bool.ListAction public
 open import Data.Empty public
 open import Data.List public
   hiding (all; and; any; align; alignWith; filter; fromMaybe; map; or; product; sum; zip; zipWith)
+open import stdlib.Data.List public
+  using (Is-[])
 open import Data.List.Membership.Propositional public
   using () renaming (_∈_ to _∈ˡ_; _∉_ to _∉ˡ_)
 open import Data.Maybe public
@@ -120,4 +122,9 @@ negPart x with sign x
 ∸≡posPart⊖ {zero} {ℕ.suc n} = _≡_.refl
 ∸≡posPart⊖ {ℕ.suc m} {zero} = _≡_.refl
 ∸≡posPart⊖ {ℕ.suc m} {ℕ.suc n} = trans (∸≡posPart⊖{m}{n}) (sym (cong posPart (([1+m]⊖[1+n]≡m⊖n m n))))
+
+instance
+  Dec-NonZero : ∀ {n} → NonZero n ⁇
+  Dec-NonZero {zero} .dec = no λ ()
+  Dec-NonZero {suc n} .dec = yes (record { nonZero = tt })
 ```