From 66e60de152ccc1f21baa2dabcb53230596e9fa31 Mon Sep 17 00:00:00 2001 From: Jared Corduan Date: Mon, 9 Dec 2019 16:32:07 -0500 Subject: [PATCH] consumed does not use rewards param --- shelley/chain-and-ledger/formal-spec/utxo.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/shelley/chain-and-ledger/formal-spec/utxo.tex b/shelley/chain-and-ledger/formal-spec/utxo.tex index f5110e65ac0..8f4e793b1ae 100644 --- a/shelley/chain-and-ledger/formal-spec/utxo.tex +++ b/shelley/chain-and-ledger/formal-spec/utxo.tex @@ -102,9 +102,9 @@ \subsection{UTxO Transitions} & \text{withdrawal balance} \\ & \fun{wbalance} ~ ws = \sum_{(\wcard\mapsto c)\in\var{ws}} c \nextdef - & \fun{consumed} \in \PParams \to \UTxO \to \StakeCreds \to \Wdrl \to \Tx \to \Coin + & \fun{consumed} \in \PParams \to \UTxO \to \StakeCreds \to \Tx \to \Coin & \text{value consumed} \\ - & \consumed{pp}{utxo}{stkCreds}{rewards}~{tx} = \\ + & \consumed{pp}{utxo}{stkCreds}{tx} = \\ & ~~\ubalance{(\txins{tx} \restrictdom \var{utxo})} + \fun{wbalance}~(\fun{txwdrls}~{tx}) \\ & ~~ + \keyRefunds{pp}{stkCreds}{tx} \\