Cardano Updates

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

* `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]>