Rename adaOnly -> isAdaOnly in spec

IntersectMBO · Feb 24, 2022 · c4685da · c4685da
1 parent c4fec53
commit c4685da
Show file tree

Hide file tree

Showing 5 changed files with 11 additions and 8 deletions.
diff --git a/eras/alonzo/formal-spec/utxo.tex b/eras/alonzo/formal-spec/utxo.tex
@@ -19,7 +19,7 @@ \section{UTxO}
     & \fun{feesOK}~\var{pp}~tx~utxo~= \\
     &~~      \minfee{pp}~{tx} \leq \txfee{txb} \wedge (\fun{txrdmrs}~tx \neq \emptyset \Rightarrow \\
     &~~~~~~((\forall (a, \wcard, \wcard) \in \fun{range}~(\fun{collateral}~{txb} \restrictdom \var{utxo}), a \in \AddrVKey) \\
-    &~~~~~~\wedge~ \fun{adaOnly}~\var{balance} \\
+    &~~~~~~\wedge~ \fun{isAdaOnly}~\var{balance} \\
     &~~~~~~\wedge~ \var{balance}*100 \geq \txfee{txb} * (\fun{collateralPercent}~pp) \\
     &~~~~~~\wedge~ \fun{collateral}~{tx} \neq \emptyset) \\
     &~~      \where \\

diff --git a/eras/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxo.hs b/eras/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxo.hs
@@ -324,7 +324,7 @@ validateCollateral pp txb utxoCollateral bal =
       validateScriptsNotPaidUTxO utxoCollateral,
       -- Part 4: balance ∗ 100 ≥ txfee txb ∗ (collateralPercent pp)
       validateInsufficientCollateral pp txb bal,
-      -- Part 5: adaOnly balance
+      -- Part 5: isAdaOnly balance
       validateCollateralContainsNonADA bal,
       -- Part 6: (∀(a,_,_) ∈ range (collateral txb ◁ utxo), a ∈ Addrvkey)
       failureIf (null utxoCollateral) NoCollateralInputs
@@ -358,13 +358,13 @@ validateInsufficientCollateral pp txb bal =
     txfee = getField @"txfee" txb -- Coin supplied to pay fees
     collPerc = getField @"_collateralPercentage" pp
 
--- > adaOnly balance
+-- > isAdaOnly balance
 validateCollateralContainsNonADA ::
   Val.Val (Core.Value era) =>
   Core.Value era ->
   Validation (NonEmpty (UtxoPredicateFailure era)) ()
 validateCollateralContainsNonADA bal =
-  failureUnless (Val.inject (Val.coin bal) == bal) $ CollateralContainsNonADA bal
+  failureUnless (Val.isAdaOnly bal) $ CollateralContainsNonADA bal
 
 -- | If tx has non-native scripts, end of validity interval must translate to time
 --

diff --git a/eras/shelley-ma/formal-spec/utxo.tex b/eras/shelley-ma/formal-spec/utxo.tex
@@ -33,13 +33,13 @@ \subsection*{UTxO Helper Functions}
     & \fun{ubalance} \in \UTxO \to \hldiff{\ValMonoid} \\
     & \fun{ubalance} ~ utxo = \hldiff{\sum_{\wcard\mapsto\var{u}\in~\var{utxo}} \fun{getValue}~\var{u}}
     \nextdef
-    & \fun{adaOnly} ~\in~ \mathsf{ValType} \to \Bool \\
-    & \fun{adaOnly}~v = v \in \range \fun{inject}
+    & \fun{isAdaOnly} ~\in~ \mathsf{ValType} \to \Bool \\
+    & \fun{isAdaOnly}~v = v \in \range \fun{inject}
     \nextdef
     & \fun{scaledMinDeposit} \in \ValMonoid \to \Coin \to \Coin \\
     & \fun{scaledMinDeposit}~\var{v}~\var{mv} ~=~
     \begin{cases}
-      \var{mv} & \fun{adaOnly}~v \\
+      \var{mv} & \fun{isAdaOnly}~v \\
       \fun{max}~(\var{mv},~\fun{utxoEntrySize}~{v} * \fun{coinsPerUTxOWord}~mv)) & \text{otherwise}
     \end{cases}
   \end{align*}

diff --git a/eras/shelley-ma/formal-spec/value-size.tex b/eras/shelley-ma/formal-spec/value-size.tex
@@ -107,7 +107,7 @@ \subsection{Min UTxO Value}
     & \fun{size} \in \Value_C \to \MemoryEstimate \\
     & \fun{size}~\var{vl} ~=~
     \begin{cases}
-      k_0 & \fun{adaOnly}~vl\\
+      k_0 & \fun{isAdaOnly}~vl\\
       k_1 + \lfloor~ (((\fun{numAssets}~vl) * k_2) + (\fun{sumALs}~vl) & \\
       ~~~~~~ + ((\fun{numPids}~vl) * k_3) + (k_4 - 1)))~ /~ k_4~\rfloor & \text{otherwise} \\
     \end{cases} \\

diff --git a/libs/cardano-ledger-core/src/Cardano/Ledger/Val.hs b/libs/cardano-ledger-core/src/Cardano/Ledger/Val.hs
@@ -67,6 +67,9 @@ class
   -- | If a quantity is stored in only one of 'v1' or 'v2', we use 0 for the missing quantity.
   pointwise :: (Integer -> Integer -> Bool) -> t -> t -> Bool
 
+  -- | Check if value contains only ADA. Must hold property:
+  --
+  -- > inject (coin v) == v
   isAdaOnly :: t -> Bool
 
   isAdaOnlyCompact :: CompactForm t -> Bool