Cardano Updates

Reflect the changes from PR #23:
- Validator params reduced from 3 to 1 (version only)
- process_time/retract_time now in State datum
- Retract redeemer takes OutputReference for reference inputs
- Modify/Reject enforce time param immutability
- Test count updated from 67 to 80

Reflect the changes from PR #23:
- Validator params reduced from 3 to 1 (version only)
- process_time/retract_time now in State datum
- Retract redeemer takes OutputReference for reference inputs
- Modify/Reject enforce time param immutability
- Test count updated from 67 to 80

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

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