Cardano Updates

* `NonZero`
* `CompactForm Coin`
* `Credential`
* `KeyHash`
* `ScriptHash`
* and `StakeWithDelegation`

Revert decoders to a more efficient implementation

Flake lock file updates:

• Updated input 'advisory-db':
    'github:rustsec/advisory-db/ce9208c' (2025-10-03)
  → 'github:rustsec/advisory-db/d99f7b9' (2026-04-11)
• Updated input 'crane':
    'github:ipetkov/crane/a669fe7' (2025-09-18)
  → 'github:ipetkov/crane/7cf72d9' (2026-04-10)
• Updated input 'devshell':
    'github:numtide/devshell/7c9e793' (2025-03-08)
  → 'github:numtide/devshell/255a2b1' (2026-01-19)
• Updated input 'fenix':
    'github:nix-community/fenix/9ba6d89' (2026-03-03)
  → 'github:nix-community/fenix/6fbc54d' (2026-04-11)
• Updated input 'fenix/rust-analyzer-src':
    'github:rust-lang/rust-analyzer/3c4ae11' (2026-03-02)
  → 'github:rust-lang/rust-analyzer/9eb97ea' (2026-04-10)
• Updated input 'flake-compat':
    'github:edolstra/flake-compat/9100a0f' (2025-05-12)
  → 'github:edolstra/flake-compat/5edf11c' (2025-12-29)
• Updated input 'flake-parts':
    'github:hercules-ci/flake-parts/9305fe4' (2025-06-08)
  → 'github:hercules-ci/flake-parts/3107b77' (2026-04-01)
• Updated input 'flake-parts/nixpkgs-lib':
    'github:nix-community/nixpkgs.lib/656a641' (2025-06-01)
  → 'github:nix-community/nixpkgs.lib/333c4e0' (2026-03-29)
• Updated input 'nixpkgs':
    'github:nixos/nixpkgs/b43c397' (2025-06-29)
  → 'github:nixos/nixpkgs/ac62194' (2026-01-02)
• Updated input 'treefmt-nix':
    'github:numtide/treefmt-nix/337a4fe' (2026-02-04)
  → 'github:numtide/treefmt-nix/790751f' (2026-04-08)

JWT.verify did not validate the nbf (not before) claim, so JWTs with nbf in the future were incorrectly considered valid. This is a security issue per RFC 7519 Section 4.1.5.

Added an explicit nbf check after JWT decode: if nbf is present and the current time is before it, verify() returns false. JWTs without an nbf claim keep the previous behavior (no nbf enforced).

This is a sister fix to #489/#550 (which addressed the exp claim).

Closes #551

Signed-off-by: Seydi Charyyev <[email protected]>

JWT.verify did not validate the exp (expiration) claim, so expired JWTs were incorrectly considered valid. This is a security issue per RFC 7519 Section 4.1.4.

Added an explicit exp check after JWT decode: if exp is present and the current time is at or past it, verify() returns false. JWTs without an exp claim keep the previous behavior (no expiration enforced).

Closes #489

Signed-off-by: Seydi Charyyev <[email protected]>

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)

Signed-off-by: Seydi Charyyev <[email protected]>

Signed-off-by: Seydi Charyyev <[email protected]>

Signed-off-by: Seydi Charyyev <[email protected]>

CIP-159 changes withdrawal semantics from "all-or-nothing" (withdrawal
amount must equal the full account balance) to "partial" (any amount up
to the current balance may be withdrawn).

`Certs.lagda.md`:
+  Define _≤ᵐ_ relation and Dec-≤ᵐ decision procedure for comparing a
   Coin value against a Maybe Coin (just bal → amt ≤ bal; nothing → ⊥).
+  Define applyWithdrawals helper (fold-based pointwise subtraction of
   withdrawal amounts from account balances).
+  Relax PRE-CERT precondition to three premises: credential is a
   registered key hash, credential is in dom rewards, and withdrawal
   amount ≤ balance (via ≤ᵐ with lookupᵐ?).
+  Update PRE-CERT effect from zeroing withdrawn credentials to pointwise
   subtraction via applyWithdrawals.
+  Document partial withdrawal semantics and version restriction deferral.

`Certs/Properties/Computational.lagda.md`:
+  Add scoped ⁇-≤ᵐ instance (positioned after DELEG/POOL/GOVCERT/CERT
   proofs to avoid instance pollution).
+  Update Computational-PRE-CERT for the new three-premise precondition.

Rewrites the project README to reflect the full scope: node with Praos
consensus, React dashboard with SSE, standalone SolidJS Chrome extension
(Koios), scripts/tools, and funding info.

Co-Authored-By: Claude Opus 4.6 <[email protected]>

New extension-gerolamo Chrome extension:
- SolidJS + TanStack Solid Query + Tailwind + WXT
- Standalone mode using Koios API (free, no API key required)
- 9 tabs: Overview, Node, Blocks, Network, Explorer, Wallet, Pebble, Logs, Settings
- Background service worker polls Koios for live chain data
- Auto-connects on install, no configuration needed
- Wallet generation via @harmoniclabs/cardano-ledger-ts
- Pebble smart contract compiler (in-browser)
- Cyberpunk neon UI theme, 537KB zipped

Dashboard lint fixes:
- Fix empty catch blocks, `any` types, `require()` import, empty interfaces

Co-Authored-By: Claude Opus 4.6 <[email protected]>

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

Flake lock file updates:

• Updated input 'haskell-nix':
    'github:input-output-hk/haskell.nix/cad2645' (2026-01-03)
  → 'github:input-output-hk/haskell.nix/ed95c6b' (2026-04-11)
• Removed input 'haskell-nix/cabal-32'
• Updated input 'haskell-nix/hackage':
    'github:input-output-hk/hackage.nix/05797dd' (2026-01-03)
  → 'github:input-output-hk/hackage.nix/53d33dc' (2026-04-11)
• Updated input 'haskell-nix/hackage-for-stackage':
    'github:input-output-hk/hackage.nix/fba3874' (2026-01-03)
  → 'github:input-output-hk/hackage.nix/2da13a6' (2026-04-11)
• Added input 'haskell-nix/hls-2.12':
    'github:haskell/haskell-language-server/7d983de' (2025-09-24)
• Updated input 'haskell-nix/iserv-proxy':
    'github:stable-haskell/iserv-proxy/1506051' (2025-08-15)
  → 'github:stable-haskell/iserv-proxy/3f7b281' (2026-04-08)
• Updated input 'haskell-nix/stackage':
    'github:input-output-hk/stackage.nix/8a7333a' (2026-01-03)
  → 'github:input-output-hk/stackage.nix/d4d9969' (2026-04-11)