Cardano Updates

Per-oracle validator parameters produce different script hashes, breaking
the offchain indexer which scans a single deterministic address. Moving
time params into the State datum (like max_fee) preserves one address for
all oracle configurations.

- Add process_time and retract_time fields to State type
- Change Retract(OutputReference) to reference State UTxO via reference_inputs
- Enforce time param immutability in Modify and Reject outputs
- Add readState helper for safe datum extraction from inputs
- Update all tests to match new signatures

Closes #22

Model tokenFromValue, valueFromToken, quantity, and fromAsset as
Lean 4 definitions over a flat Value type, with 7 machine-checked
theorems mirroring the Aiken unit tests:

- valueFromToken_roundtrip
- tokenFromValue_ada_only
- tokenFromValue_multi_policy
- tokenFromValue_multi_asset
- quantity_present
- quantity_wrong_policy
- quantity_valueFromToken

- Fix quantity_wrong_policy to prove = none (not contradiction)
- Add quantity_wrong_asset theorem (mirrors Aiken test)
- Add quantity_valueFromToken Aiken unit test
- Add lib.props.ak with 6 fuzz property tests mirroring Lean theorems

Each Lean docstring and Aiken property comment now follows the
cage.props.ak pattern: mathematical statement, validator context,
and security consequence if the property were violated.

Each Lean docstring and Aiken property comment now follows the
cage.props.ak pattern: mathematical statement, validator context,
and security consequence if the property were violated.

- Fix quantity_wrong_policy to prove = none (not contradiction)
- Add quantity_wrong_asset theorem (mirrors Aiken test)
- Add quantity_valueFromToken Aiken unit test
- Add lib.props.ak with 6 fuzz property tests mirroring Lean theorems

Model tokenFromValue, valueFromToken, quantity, and fromAsset as
Lean 4 definitions over a flat Value type, with 7 machine-checked
theorems mirroring the Aiken unit tests:

- valueFromToken_roundtrip
- tokenFromValue_ada_only
- tokenFromValue_multi_policy
- tokenFromValue_multi_asset
- quantity_present
- quantity_wrong_policy
- quantity_valueFromToken

Move unit and property tests out of cage.ak and lib.ak into dedicated
test modules (cage.props.ak, lib.tests.ak) for better organization.

Phase property tests (6 fuzz tests mirroring Lean theorems) moved to
cage.props.ak. Library tests (12 tests) moved to lib.tests.ak.
Validator-level tests remain in cage.ak since validators cannot be
imported across modules.

All 73 tests pass. plutus.json unchanged (pure refactor).

Move unit and property tests out of cage.ak and lib.ak into dedicated
test modules (cage.props.ak, lib.tests.ak) for better organization.

Phase property tests (6 fuzz tests mirroring Lean theorems) moved to
cage.props.ak. Library tests (12 tests) moved to lib.tests.ak.
Validator-level tests remain in cage.ak since validators cannot be
imported across modules.

All 73 tests pass. plutus.json unchanged (pure refactor).

Add Lean 4 proofs for the three-phase request lifecycle:

- Phases 1, 2, 3 are pairwise mutually exclusive
- Honest requests in Phase 1/2 are not rejectable
- Phase coverage: every honest time point falls in exactly one phase

All proofs close via omega (linear arithmetic).
Build: nix shell nixpkgs#lean4 -c lake build

6 property-based tests using aiken/fuzz that verify the same phase
exclusivity and coverage properties proven formally in MpfsCage/Phases.lean:
- phase1_phase2_exclusive
- phase1_phase3_exclusive
- phase2_phase3_exclusive
- phase1_honest_not_rejectable
- phase2_honest_not_rejectable
- phase_coverage_point

6 property-based tests using aiken/fuzz that verify the same phase
exclusivity and coverage properties proven formally in MpfsCage/Phases.lean:
- phase1_phase2_exclusive
- phase1_phase3_exclusive
- phase2_phase3_exclusive
- phase1_honest_not_rejectable
- phase2_honest_not_rejectable
- phase_coverage_point

Add Lean 4 proofs for the three-phase request lifecycle:

- Phases 1, 2, 3 are pairwise mutually exclusive
- Honest requests in Phase 1/2 are not rejectable
- Phase coverage: every honest time point falls in exactly one phase

All proofs close via omega (linear arithmetic).
Build: nix shell nixpkgs#lean4 -c lake build

Yaci DevKit instant-forwards through a synthetic pre-Conway era,
causing on-chain POSIX times to be systematically ahead of wall-clock
by ~600 seconds. Compute this offset from the Shelley genesis
systemStart and apply it to submitted_at in request datums.

Also: add 20% ExUnit margin to Ogmios evaluation, add validTo to
reject transactions, and increase test time params to 10 minutes.

Three exclusive time phases per request prevent DDoS by eliminating
race conditions between oracle and requester:
- Phase 1: oracle-only Modify
- Phase 2: requester-only Retract
- Phase 3: oracle Reject (cleanup expired/dishonest requests)

Add process_time and retract_time as immutable validator parameters,
submitted_at field in Request datum, phase enforcement in
Contribute/Modify/Retract, and batch Reject with refund verification.

Fix pre-existing TypeScript errors (@types/node, Data typing) and add
typecheck CI job.

Lucid Evolution's SLOT_CONFIG_NETWORK["Custom"] defaults to
slotLength: 0, causing division-by-zero (Infinity) when validFrom/
validTo convert POSIX time to slots. Query the Blockfrost-compatible
/genesis endpoint for system_start and slot_length.

Also adds spec/CageDatum.lean with formal Lean 4 property spec.

- overview: add phase timeline (gantt), Reject in system/sequence
  diagrams, updated lifecycle state machine, transaction table
- types: add max_fee to State, fee/submitted_at to Request,
  Migrating to MintRedeemer, Reject to UpdateRedeemer, fix
  Plutus encoding examples
- validators: add Validator Parameters section, Migration section,
  Reject section, phase constraints on Modify/Contribute/Retract
- properties: 16 categories / 67 tests (was 12 / 44), add
  time-gated phases, reject, fee enforcement, migration categories
- Fix source links to cardano-mpfs-onchain repo