[#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 over the real commitment_core entrypoints.

This PR changes test wiring and test/model code only. The lib.rs change only registers the test module. No production contract behavior, public API, workflow, dependency, lockfile, deployment, or release configuration is changed.

Modeled state mirrors the 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, exact owner-index contents and order, the all-ID index, and the reentrancy guard.

Commands are bound 1:1 to the real entrypoints:

Issue command	Actual API	Notes
create + fund	create_commitment(owner, amount, asset, rules)	funding is atomic inside create; tokens move in and the creation fee is split off
value update	update_value(caller, id, new_value)	may persist violated on a max-loss breach
settle	settle(id)	permissionless; requires now >= expires_at
cancel	early_exit(id, caller)	owner-only; penalty is added to collected fees
partial release	allocate(caller, id, pool, amount)	allocator-only
fee operations	set_creation_fee_bps / set_fee_recipient / withdraw_fees	treasurer/admin
expiry	ledger timestamp advancement	drives settle eligibility

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

Invalid variants are generated explicitly, including wrong state, nonexistent slots, wrong actors, duplicate terminal operations, signed and zero amounts, overdraft allocation, excess fee withdrawal, insufficient funding, and settle-before-expiry.

After every executed command—valid or invalid—the harness re-reads observable contract and token state and compares it with the model. Rejected operations must preserve the complete observable state.

Independent Max-mode hardening pass

A second independent audit was completed against the original PR head:

0b8e009877607eaad5f0f9202389526307256a24

The audit did not trust the original model or its reported invariants. It independently reviewed command-to-entrypoint mapping, model arithmetic, observable-state comparison, invalid-operation rollback, deterministic seeds, failure minimization, replay behavior, terminal absorption, fee accounting, ownership/index consistency, and cross-commitment custody interactions.

The resulting test/model-only hardening commit is:

c782c4d84910fcc6d5696ecd53c1061330519dab

Safe recovery coverage

The hardened generator no longer treats unbounded value markup as a valid recovery scenario.

For each slot:

own_remaining_principal = amount - released

A generated upward recovery is accepted only when:

status == active
authorized updater
old_value < new_value
new_value <= own_remaining_principal
new_value >= 0

Final deterministic coverage:

• accepted downward updates: 71;
• accepted upward recoveries: 41;
• accepted same-value updates: 13;
• unsafe upward updates generated: 0;
• rejected or terminal/invalid updates: 76.

The recovery path is deterministic and replayable:

Create
→ MildMarkdown
→ RecoverWithinOwnPrincipal

The minimizer preserves this causal prefix when it is required to reproduce an upward-recovery failure.

Hardened validation result

• lifecycle-model tests: 20/20 passed in parallel;
• lifecycle-model tests: 20/20 passed sequentially;
• full commitment_core unit suite: 182 passed, with the same 3 pre-existing master failures;
• integration suite: 248 passed / 0 failed / 4 ignored;
• changed file: rustfmt-clean;
• focused clippy: PASS;
• ContractGraph-QA exact-subject and durable verification: 36/36 passed;
• deterministic positive replay: byte-identical across two runs;
• negative controls: 8/8 detected;
• RecoverWithoutOwnPrincipalCap mutant: detected;
• no PR-introduced regression was identified.

The hardening remains test/model-only. No production contract behavior, dependency, lockfile, workflow, deployment configuration, or public API was changed.

CI truth

The GitHub CI run for exact head c782c4d84910fcc6d5696ecd53c1061330519dab is RED, but its first relevant failures reproduce on exact upstream base:

fb8349e63d7cfd78d68151b4b15d249b6b358b47

The failure occurs before the new lifecycle model executes and is associated with the existing ethnum 1.5.2 / current Rust stable incompatibility. The workflow also contains a separate pre-existing Ubuntu/brew installation problem.

Therefore:

BASE_CI_BLOCKER_REPRODUCED
PR_INTRODUCED_REGRESSION_NOT_CONFIRMED

This PR does not modify the toolchain, dependencies, lockfile, or workflows to conceal that blocker. CI is not represented as GREEN.

Separate production finding

The independent audit identified a separate potentially security-relevant ownership-isolation/custody behavior outside the implementation scope of #554.

No production fix and no detailed public reproduction are included in this PR. The evidence is retained pending maintainer guidance on the preferred private or maintainer-reviewed disclosure channel.

Invariants

• I1 Principal conservation: contract custody is compared with the sum of each slot’s remaining principal plus collected fees. Global tracked-token conservation is also checked.
• I2 Fee conservation: collected fees equal creation fees plus early-exit penalties minus withdrawals, including truncation and zero boundaries.
• I3 Ownership/auth matrix: only permitted actors succeed for owner-, updater-, allocator-, treasurer-, and admin-gated operations.
• I4 Terminal immutability: terminal commitments reject active-only flows, and duplicate terminal operations do not move principal or fees.
• I5 Invalid-command atomicity: every rejected operation preserves all modeled fields, balances, counters, fees, indexes, and guard state.
• I6 Determinism: seeds, addresses, command encoding, replay, and failure minimization are deterministic.

Reproducibility

Every failure report contains the seed, failing step and reason, original command sequence, and minimized sequence.

Single-seed replay:

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

The minimizer runs only on the failure path and preserves the causal command prefix and failure dimension needed for reproduction.

ContractGraph-QA

ContractGraph-QA is used as an independent external lifecycle oracle and is not a production dependency of this repository. No ContractGraph-QA code, configuration, dependency, or lockfile change is committed here.

Exact-subject and durable verification passes 36/36. All 8/8 negative controls are detected, including the RecoverWithoutOwnPrincipalCap mutant. Deterministic positive replay is byte-identical across two runs.

No PR-introduced regression was identified within the test/model scope. The separate out-of-scope production finding is handled only through the disclosure note above.

CI budget

Execution is deterministic and bounded: 40 seeds × 20 commands, with full observable-state verification after each step, plus focused regression, replay, minimization, and negative-control coverage. The focused lifecycle-model suite contains 20 tests and has no wall-clock, network, or unseeded-randomness dependency.

Validation

Check	Result
lifecycle model, parallel	PASS: 20/20
lifecycle model, sequential	PASS: 20/20
full commitment_core unit suite	182 passed / 3 baseline failures
integration suite	248 passed / 0 failed / 4 ignored
changed-file rustfmt	PASS
focused clippy	PASS
ContractGraph-QA exact-subject and durable verification	PASS: 36/36
deterministic positive replay	PASS: byte-identical across two runs
negative controls	PASS: 8/8 detected

The exact baseline unit failures are:

• emergency_tests::test_emergency_mode_toggle_emits_events;
• tests::test_create_commitment_event;
• tests::test_create_commitment_updates_storage_layout.

Acceptance criteria

#554 criterion	Where
Generated sequences preserve principal, fee, ownership, and terminal invariants	deterministic seeded sequences with full verification after every command
Invalid sequences fail safely with no partial mutation	outcome prediction plus complete before/after observable-state comparison
Failure reports are replayable and minimized	seed, exact command-token replay, and cause-preserving minimization
Deterministic and bounded	fixed seeds and addresses, bounded command count, byte-identical positive replay
Existing CI/CD behavior assessed	Exact base and PR reproduce the same pre-test toolchain/dependency blocker; no PR-introduced regression was identified. CI is not represented as GREEN.
PR explains model, design, evidence, and limitations	this document

Design choices and tradeoffs

• The reference model duplicates the relevant arithmetic instead of calling production helpers, preserving its role as an independent oracle.
• Custody is checked using remaining principal rather than treating current_value as newly created backing.
• Upward recovery generation is capped by each slot’s own remaining principal.
• Deterministic command tokens support exact replay without adding a shrinking-framework dependency.
• The mock NFT keeps this model focused on core lifecycle economics; existing cross-contract tests cover broader NFT behavior.

Limitations

• Exploration is bounded evidence, not a proof over every possible sequence.
• The model uses one asset per scenario; broader multi-asset isolation remains outside this PR.
• Mock authorization verifies actor and role predicates but is not a proof of every production require_auth call.
• Native resource-budget measurements are not a production resource-budget proof.
• Event history, rate-limit internals, downstream NFT storage, and crash/recovery adapters remain outside the model.
• The separate potentially security-relevant production finding is intentionally not reproduced or fixed in this PR.

[safal207]

Independent Max-mode verification and model hardening are complete on exact head c782c4d84910fcc6d5696ecd53c1061330519dab.

The hardened lifecycle suite passes 20/20 in both parallel and sequential execution. The full commitment_core suite reports 182 passed with the same three failures reproduced on exact master, and the integration suite reports 248 passed / 0 failed / 4 ignored. ContractGraph-QA durable verification passes 36/36, with 8/8 negative controls detected.

The generator now covers bounded per-slot value recovery without classifying unbounded markup as valid: 71 accepted downward updates, 41 accepted upward recoveries, and zero unsafe generated upward updates.

The GitHub CI failure is not introduced by this PR: the same ethnum 1.5.2 / current-stable toolchain failure reproduces on base fb8349e63d7cfd78d68151b4b15d249b6b358b47 before the new lifecycle tests run. I have not changed dependencies or workflows to mask it.

The audit also identified a separate potentially security-relevant ownership-isolation/custody behavior outside #554. I have kept the detailed reproduction out of this PR. Please advise the preferred private or maintainer-reviewed disclosure channel.