[#554] Add stateful invariant coverage for commitment flows

[safal207]

Closes #554

Model

contracts/commitment_core/src/lifecycle_model_tests.rs adds a bounded deterministic stateful reference model for the core commitment lifecycle (Soroban, native Rust test suite — no new dependencies).

Modeled state mirrors only economically relevant fields of commitment_core: per-commitment {owner, net principal (amount), current_value, released, expires_at, max_loss, penalty, status}, plus TVL, collected fees, creation-fee bps, ledger time, token custody balances (owners / contract / fee recipient / pool), and owner-index list lengths.

Commands are bound 1:1 to the real entrypoints (issue terms → actual API):

Issue command	Actual API	Notes
create + fund	create_commitment(owner, amount, asset, rules)	funding is atomic inside create: tokens move in, creation fee split off
value update (oracle)	update_value(caller, id, new_value)	may persist violated on max-loss breach
settle (expiry)	settle(id)	permissionless, requires now >= expires_at
cancel	early_exit(id, caller)	owner-only, penalty → CollectedFees
partial release	allocate(caller, id, pool, amount)	allocator-only
fee	set_creation_fee_bps / set_fee_recipient / withdraw_fees	treasurer/admin
expiry	ledger timestamp advance (AdvanceTime{days})	drives settle eligibility

The lifecycle graph follows docs/commitment_core/SEMANTICS.md exactly: active → {active, violated, settled, early_exit}; violated, settled, early_exit are terminal/absorbing.

Invalid variants are generated explicitly: wrong state (terminal/nonexistent slots), wrong actor (outsider vs admin/updater/allocator/treasurer/owner), duplicate terminal operations (double settle, repeat exit), boundary amounts (zero/negative, overdraft allocate, excess withdraw), insufficient funding creates, settle-before-expiry.

After every executed command — valid or invalid — the harness re-reads the full observable contract state and compares it against the model (apply() → verify()), so any divergence is caught at the exact step where it appears.

Invariants

• I1 Principal conservation (flow form): token.balance(core) == Σ_slots (amount − released) + collected_fees, where released accumulates settle payouts, exit returns+penalties, and allocations. A naive form balance == Σ current_value does not hold on this codebase because oracle markdowns via update_value leave principal in custody until payout; the flow form is the exact conservation law. Additionally: global supply conservation — all tracked balances always sum to the minted supply.
• I2 Fee conservation: collected_fees == Σ creation_fees + Σ early-exit penalties − withdrawals; zero-penalty truncation boundary covered.
• I3 Ownership/auth matrix: only permitted actors succeed per operation (owner-only exit, updater/admin valuation, allocator-only allocation, treasurer-only fee ops); every rejection is asserted atomic.
• I4 Terminal immutability: violated/settled/early_exit reject all active-only flows; repeated terminal operations move neither principal nor fees; owner-index removal happens only on settle (mirrored exactly).
• I5 Invalid-command atomicity: after each invalid command, state-after == state-before for every modeled field (status, values, TVL, fees, counters, all balances, index lists).
• I6 Determinism: fixed seeds (xorshift64*), fixed StrKey contract addresses, no entropy sources.

Reproducibility

Every failure panics with a report containing: seed, failing step + reason, the original command sequence, and a greedy minimized sequence (leave-one-out delta debugging over commands). Single-seed replay:

CGQA_LIFECYCLE_SEED=<seed> cargo test -p commitment_core --lib lifecycle_model

No shrinking framework dependency was added (repo has no proptest/arbitrary in this crate; shared_utils' proptest is feature-gated and unused here) — minimization is implemented inline and runs only on the failure path.

ContractGraph-QA

https://github.com/safal207/ContractGraph-QA was used as an independent external lifecycle oracle; it is not a production dependency of this repo (no code, config, or lockfile from it is committed).

Three reachability models were authored strictly from the current production semantics (lib.rs, SEMANTICS.md) — duplicate settlement, terminal resurrection, fee double-counting. Each yields a deterministic evidence path showing which guard boundary protects the invariant (terminal-status-guard, active-only-entrypoints, fee-accounting; model SHA-256 recorded in output). A negative control with no violated assumptions returns not_found_within_bound. Every capability path the oracle flags maps to a native regression script that proves the guard holds against the real contract:

• duplicate-settle path → regression_duplicate_settle_pays_exactly_once
• terminal-resurrection path → regression_terminal_states_absorbing
• fee-drift path → regression_fee_accounting_conservation

No counterexample against the real contract was found by either layer.

CI budget

Deterministic and bounded: 40 seeds × 20 commands (800 generated steps, each followed by full-state verification) + 8 hand-written regression scripts + determinism/replay tests. No wall-clock, RNG, or network dependence; identical output on every run. Measured locally: the whole lifecycle_model filter runs in ~50 s; total -p commitment_core --lib suite ~125 s. The suite adds no CI workflow changes and cannot flake (no unseeded randomness).

Validation

Real results, Windows MSVC toolchain (cargo +stable-x86_64-pc-windows-msvc; default GNU toolchain linker on this machine is broken):

• cargo test -p commitment_core --lib → 173 passed; 3 failed — the 3 failures are pre-existing on upstream master (tests::test_create_commitment_updates_storage_layout expects old c_0 ids vs current COMMIT_0; tests::test_create_commitment_event; emergency_tests::test_emergency_mode_toggle_emits_events). Verified identical before my change (baseline run at fb8349e). All 11 new tests pass.
• Integration tests (CI job): cd tests/integration && cargo test → 124 passed; 0 failed; 2 ignored.
• cargo fmt --check: repo has extensive pre-existing fmt diffs (not touched); lifecycle_model_tests.rs itself is rustfmt-clean.
• cargo clippy -p commitment_core --lib --tests: no warnings from the new module.
• Not run locally (CI-only steps): WASM build target, Stellar CLI build, benchmarks job.

Acceptance criteria

#554 criterion	Where
Generated sequences preserve principal/fee/ownership/terminal invariants	lifecycle_model_seeded_sequences_hold_invariants (40 seeded sequences), checked after every step
Invalid sequences fail safely, no partial mutation	outcome-prediction matching + full-state compare after every invalid command; regression_wrong_actor_matrix_is_atomic, regression_insufficient_create_is_atomic, regression_settle_ordering_guards
Failure prints replayable seed + minimized sequence	failure_report() + greedy minimize() + CGQA_LIFECYCLE_SEED replay entrypoint
Deterministic, within CI runtime budget	fixed seeds/addresses, bounded case count, ~50 s measured
Existing CI stays green	integration tests green; no workflow changes; pre-existing master failures unchanged
PR explains model/design/tradeoffs/evidence/limitations	this document

Design choices & tradeoffs

• Reference model duplicates arithmetic semantics (fee_from_bps, loss_percent, penalty) instead of calling into shared_utils, keeping the oracle independent of the code under test; ranges are chosen to avoid overflow branches, which existing fuzz shapes already cover.
• Custody invariant uses the flow (released) form — stricter and actually true under markdowns; documented above.
• Mock NFT (same shape as existing unit/fuzz mocks) keeps the model focused on core economics; NFT mirroring is covered by existing cross-contract tests.

Limitations

• Single asset per scenario (multi-asset custody not modeled).
• Pause/emergency/rate-limit paths intentionally left out (separate suites exist); rate limiter is unconfigured (no-op) here.
• Bounded exploration: passing seeds are evidence within the modeled space, not proof of correctness.
• The observed asymmetry "settle removes the owner-index entry, early_exit/violated do not" and "allocate/settle can pay out marked-up value funded by other commitments' custody (failing atomically when custody is short)" are mirrored as-is, not changed.