[Dijkstra] CIP-159-05: Update UTxO rules for direct deposits and balance intervals (#1117)

CIP-159 changes the transaction balancing rules and introduces Phase-1
balance interval validation.  This commit updates the UTxO transition
system accordingly.

`Utxo.lagda.md`:
+  Add accountBalances : Rewards field to UTxOEnv and SubUTxOEnv for
   pre-batch account balance lookups;
+  Add HasAccountBalances type class and instances;
+  Update producedTx to include direct deposit amounts on the produced
   side of the preservation-of-value equation;
+  Add direct deposit registration premise to UTXO and SUBUTXO
   (`dom DirectDepositsOf ⊆ dom AccountBalancesOf`);
+  Add balance interval validation premise to UTXO and SUBUTXO
   (∀ (c,interval) ∈ BalanceIntervalsOf, InBalanceInterval using
   pre-batch account balances).

`Utxo/Properties/Computational.lagda.md`:
+  Update Computational-UTXO for new premise tuple arity (19+h → 21+h)

`Ledger.lagda.md`:
+  Add accountBalances field to SubLedgerEnv;
+  Populate accountBalances in SUBLEDGER-V, SUBLEDGER-I, LEDGER-V,
   LEDGER-I using RewardsOf certState₀ (pre-batch balances).

Author: williamdemeo

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

@@ -506,7 +506,6 @@ data _⊢_⇀⦇_,SUBUTXO⦈_ : SubUTxOEnv → UTxOState → SubLevelTx → UTxO
     ∙ MaybeNetworkIdOf txSub ~ just NetworkId
     ∙ CurrentTreasuryOf txSub ~ just (TreasuryOf Γ)
     ∙ dom (DirectDepositsOf txSub) ⊆ dom (AccountBalancesOf Γ)
-    ∙ dom (BalanceIntervalsOf txSub) ⊆ dom (AccountBalancesOf Γ)
     ∙ ∀[ (c , interval) ∈ BalanceIntervalsOf txSub ˢ ]
         (InBalanceInterval (maybe id 0 (lookupᵐ? (AccountBalancesOf Γ) c)) interval)
       ────────────────────────────────