Eliminate Boolean properties

src/Ledger/Conway/Conformance/Utxo.agda

@@ -88,7 +88,7 @@ data _⊢_⇀⦇_,UTXO⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Type
     in
     ∙ txins ≢ ∅                              ∙ txins ∪ refInputs ⊆ dom utxo
     ∙ txins ∩ refInputs ≡ ∅                  ∙ L.inInterval slot txvldt
-    ∙ L.feesOK pp tx utxo ≡ true             ∙ L.consumed pp s txb ≡ L.produced pp s txb
+    ∙ L.feesOK pp tx utxo                    ∙ L.consumed pp s txb ≡ L.produced pp s txb
     ∙ coin mint ≡ 0                          ∙ txsize ≤ maxTxSize pp
     ∙ L.refScriptsSize utxo tx ≤ pp .maxRefScriptSizePerTx
 

src/Ledger/Transaction.lagda

@@ -235,8 +235,12 @@ Ingredients of the transaction body introduced in the Conway era are the followi
 \end{NoConway}
 
 \begin{code}[hide]
-  isP2Script : Script → Bool
-  isP2Script = is-just ∘ isInj₂
+  isP2Script : Script → Type
+  isP2Script = From-inj₂
+
+  isP2Script? : ∀ {s} → isP2Script s ⁇
+  isP2Script? {inj₁ x} .dec = true because ofʸ (lift tt)
+  isP2Script? {inj₂ y} .dec = true because ofʸ y
 
   instance
     HasCoin-TxOut : HasCoin TxOut

src/Ledger/Utxo.lagda

@@ -43,14 +43,24 @@ q *↓ n = ℤ.∣ ℚ.⌊ q ℚ.* (ℤ.+ n ℚ./ 1) ⌋ ∣
 \begin{NoConway}
 \begin{figure*}[h]
 \begin{code}
-isTwoPhaseScriptAddress : Tx → UTxO → Addr → Bool
+isTwoPhaseScriptAddress : Tx → UTxO → Addr → Type
 isTwoPhaseScriptAddress tx utxo a =
   if isScriptAddr a then
     (λ {p} → if lookupScriptHash (getScriptHash a p) tx utxo
                  then (λ {s} → isP2Script s)
-                 else false)
+                 else ⊥)
   else
-    false
+    ⊥
+\end{code}
+\begin{code}[hide]
+isTwoPhaseScriptAddress? : ∀ {tx utxo a} → isTwoPhaseScriptAddress tx utxo a ⁇
+isTwoPhaseScriptAddress? {tx} {utxo} {a} .dec
+  with decide (isScriptAddr a)
+... | inj₂ _ = false because ofⁿ λ ()
+... | inj₁ p
+  with decide (lookupScriptHash (getScriptHash a p) tx utxo)
+... | inj₂ _ = false because ofⁿ λ ()
+... | inj₁ s = isP2Script? {s} .dec
 \end{code}
 \begin{code}[hide]
 opaque
@@ -61,8 +71,9 @@ opaque
 
   getInputHashes : Tx → UTxO → ℙ DataHash
   getInputHashes tx utxo = getDataHashes
-    (filterˢ (λ (a , _ ) → isTwoPhaseScriptAddress tx utxo a ≡ true)
-            (range (utxo ∣ txins)))
+    (filterˢ (λ (a , _ ) → isTwoPhaseScriptAddress tx utxo a)
+             ⦃ λ {(a , _)} → isTwoPhaseScriptAddress? {tx} {utxo} {a} ⦄
+             (range (utxo ∣ txins)))
     where open Tx; open TxBody (tx .body)
 
 totExUnits : Tx → ExUnits
@@ -377,37 +388,22 @@ instance
                                + getCoin (UTxOState.deposits s)
                                + UTxOState.donations s
 
--- Boolean implication
-_=>ᵇ_ : Bool → Bool → Bool
-a =>ᵇ b = if a then b else true
-
--- Boolean-valued inequalities on natural numbers
-_≤ᵇ_ _≥ᵇ_ : ℕ → ℕ → Bool
-m ≤ᵇ n = ¿ m ≤ n ¿ᵇ
-_≥ᵇ_ = flip _≤ᵇ_
-
-≟-∅ᵇ : {A : Type} ⦃ _ : DecEq A ⦄ → (X : ℙ A) → Bool
-≟-∅ᵇ X = ¿ X ≡ ∅ ¿ᵇ
-
 coinPolicies : ℙ ScriptHash
 coinPolicies = policies (inject 1)
 
-isAdaOnlyᵇ : Value → Bool
-isAdaOnlyᵇ v = toBool (policies v ≡ᵉ coinPolicies)
-
--- TODO: this could be a regular property
--- TODO: using this in UTxO rule below
+isAdaOnlyᵇ : Value → Type
+isAdaOnlyᵇ v = policies v ≡ᵉ coinPolicies
 \end{code}
 \begin{code}
-
-feesOK : PParams → Tx → UTxO → Bool
-feesOK pp tx utxo =  (  minfee pp utxo tx ≤ᵇ txfee ∧ not (≟-∅ᵇ (txrdmrs ˢ))
-                        =>ᵇ  ( allᵇ (λ (addr , _) → ¿ isVKeyAddr addr ¿) collateralRange
-                             ∧ isAdaOnlyᵇ bal
-                             ∧ (coin bal * 100) ≥ᵇ (txfee * pp .collateralPercentage)
-                             ∧ not (≟-∅ᵇ collateral)
-                             )
-                     )
+feesOK : PParams → Tx → UTxO → Type
+feesOK pp tx utxo = ( minfee pp utxo tx ≤ txfee × (txrdmrs ˢ ≢ ∅
+                      → ( All (λ (addr , _) → isVKeyAddr addr) collateralRange
+                        × isAdaOnlyᵇ bal
+                        × coin bal * 100 ≥ txfee * pp .collateralPercentage
+                        × collateral ≢ ∅
+                        )
+                      )
+                    )
   where
     open Tx tx; open TxBody body; open TxWitnesses wits; open PParams pp
     collateralRange  = range    ((mapValues txOutHash utxo) ∣ collateral)
@@ -538,7 +534,7 @@ data _⊢_⇀⦇_,UTXO⦈_ where
     in
     ∙ txins ≢ ∅                              ∙ txins ∪ refInputs ⊆ dom utxo
     ∙ txins ∩ refInputs ≡ ∅                  ∙ inInterval slot txvldt
-    ∙ feesOK pp tx utxo ≡ true               ∙ consumed pp s txb ≡ produced pp s txb
+    ∙ feesOK pp tx utxo                      ∙ consumed pp s txb ≡ produced pp s txb
     ∙ coin mint ≡ 0                          ∙ txsize ≤ maxTxSize pp
     ∙ refScriptsSize utxo tx ≤ pp .maxRefScriptSizePerTx
 

src/Ledger/Utxo/Properties.lagda

@@ -92,7 +92,7 @@ instance
                 (inj₂ b₂') → case dec-de-morgan b₂' of λ where
                   (inj₁ a₂) → "¬ inInterval (UTxOEnv.slot Γ) (txvldt (Tx.body tx))"
                   (inj₂ b₂) → case dec-de-morgan b₂ of λ where
-                    (inj₁ a₃) → "¬ feesOK pp tx utxo ≡ true"
+                    (inj₁ a₃) → "¬ feesOK pp tx utxo"
                     (inj₂ b₃) → case dec-de-morgan b₃ of λ where
                         (inj₁ a₄) →
                           let