Cardano Updates

After makeSignedInstaller produces a signed .pkg on the macOS signing
host, notarize and staple it via SSH before downloading. Credentials
are read from APPLE_NOTARY_USER, APPLE_NOTARY_PASS, and APPLE_TEAM_ID;
notarization is skipped with a message if any are unset.

Upgrade cardano-node from 10.6.2 to 10.7.1 and configure the V2LSM
ledger backend to reduce memory usage by storing UTxO data on disk
rather than in-heap. Also updates the cardano-playground config pin
and switches the config path to environments-pre/.

to fix the tests failing because of the new predicate failure

Add a `--testnet-config-dir` flag that auto-discovers the 4 infrastructure
parameters (socket path, signing key, node config file, target nodes) from
a `cardano-testnet` output directory.  Discovered infrastructure always
overrides user-provided values; all other config fields must be supplied
by the user.

Added check: if a balance interval constraint is specified for a
credential, then that credential belongs to the domain of
`AccountBalancesOf Γ`; see Carlos' comment:

https://github.com/IntersectMBO/formal-ledger-specifications/pull/1160#discussion_r3110584513

After all sub-rule transitions (`SUBLEDGERS`, `CERTS`, `GOVS`, `UTXOW`),
apply batch-wide direct deposits to the final CertState via
`applyDirectDeposits` and `allDirectDeposits`.

`Ledger.lagda.md`:
+  Update `LEDGER-V` output: compute `certStateFinal` by applying
   `allDirectDeposits` to `certState₂`, use `certStateFinal` in the
   output `LedgerState` and in `rmOrphanDRepVotes`;
+  `LEDGER-I` unchanged (invalid batches don't apply deposits);
+  Document direct deposit application ordering and phantom asset
   prevention rationale.

`Ledger/Properties/Computational.lagda.md`:
+  Update `computeProof` valid branch to compute `certStateFinal` and use
   it in the output `LedgerState`.

Signed-off-by: Ales Verbic <[email protected]>

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).