Cardano Updates

No longer allow leftover bytes when decoding IPv4/IPv6 addresses regardless
of decoder version.

Clean up CddlSpec, fix `Datum` and `AccountBalanceIntervals` generators

ci/cd: add initial github actions workflow

The harness never actually ran in Antithesis. The upstream report for
run 44aa6d28...-50-7 shows:

    Container ogmios died during environment setup with exit code 127
    /bin/sh: error while loading shared libraries: libdl.so.2:
      cannot open shared object file: No such file or directory

cardanosolutions/ogmios is a busybox-based image whose /bin/sh is
dynamically linked. Locally glibc >= 2.34 folds libdl into libc so
loading /bin/sh succeeds; Antithesis's instrumented loader does not
satisfy that dependency and the shell fails at load time, before any
harness line runs. That is why no harness echo, no ogmios banner, and
no Started event ever reached Logs Explorer.

Fix: drop the harness wrapper entirely and invoke ogmios's native
entrypoint. Ogmios already polls for the node socket on its own
(that's where HealthFailedToConnect / HealthTick come from), so the
wait-for-socket loop the harness provided is redundant. The only
thing we lose is SIGTERM -> SIGINT translation at shutdown, which is
a cosmetic exit-code concern, not a correctness one.

Also pins to :v6.14.0 — :latest tracked nightly builds (confirmed by
'ogmios --version' reporting 'nightly (bdb1bad5)').

Removes now-unused components/n2c-harness/ and the bind-mounted
testnets/cardano_node_master/harness.sh.

Fixes #47

Initializes Spec-Driven Development tooling (speckit templates,
scripts, and Claude commands) and ratifies the project constitution.

The constitution is grounded in the actual code structure
(KnownEras + Era GADT + closed type families), distinguishing it
from cardano-balance-tx's typeclass-style approach. Core principles:

- Read-only library (no tx construction/submission)
- Closed-world era model (KnownEras enumerated in one place)
- TFs and GADTs over typeclasses for era dispatch
- Totality at era boundaries (no partial upgrade stubs)
- Mirror cardano-ledger-* types, do not redefine
- Minimal dependency surface (no cardano-api, no cardano-wallet-*)
- Version-bound hygiene on all cardano-ledger-* deps

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

Add batch-wide withdrawal bound check to prevent phantom asset attacks
when nested transactions combine deposits and withdrawals.

`Transaction.lagda.md`:
+  Define allWithdrawals batch aggregation helper (mirrors
   allDirectDeposits)

`Utxo.lagda.md`:
+  Define NoPhantomWithdrawals predicate using allWithdrawals
+  Add NoPhantomWithdrawals premise to UTXO rule
+  Document phantom asset attack and spend-side safety analogy

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

Add batch-wide withdrawal bound check to prevent phantom asset attacks
when nested transactions combine deposits and withdrawals.

`Transaction.lagda.md`:
+  Define allWithdrawals batch aggregation helper (mirrors
   allDirectDeposits)

`Utxo.lagda.md`:
+  Define NoPhantomWithdrawals predicate using allWithdrawals
+  Add NoPhantomWithdrawals premise to UTXO rule
+  Document phantom asset attack and spend-side safety analogy

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

Initializes Spec-Driven Development tooling (speckit templates,
scripts, and Claude commands) and ratifies the project constitution.

The constitution is grounded in the actual code structure
(KnownEras + Era GADT + closed type families), distinguishing it
from cardano-balance-tx's typeclass-style approach. Core principles:

- Read-only library (no tx construction/submission)
- Closed-world era model (KnownEras enumerated in one place)
- TFs and GADTs over typeclasses for era dispatch
- Totality at era boundaries (no partial upgrade stubs)
- Mirror cardano-ledger-* types, do not redefine
- Minimal dependency surface (no cardano-api, no cardano-wallet-*)
- Version-bound hygiene on all cardano-ledger-* deps

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

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

Signed-off-by: Chris Gianelloni <[email protected]>