[DeFi][FIN-29] Differential financial state tests and cross-feature solvency assurance #79

Parent umbrella: #43. New FIN work-item: FIN-29. Planning only; no implementation is claimed.

Plain-language explanation

Individual maths functions may pass whilst their combination leaks value. The programme needs long realistic state sequences that independently calculate what every pool, position, claim and user should own.

Mermaid walkthrough

flowchart TD
A["Pinned protocol and mathematical reference"] --> B["Generate stateful scenarios"]
B --> C["Run CKB-VM / actual Script groups"]
C --> D["Compare prices, positions, deltas, claims"]
D --> E{"Conservation and authorised outcomes?"}
E -- No --> X["Shrink and archive counterexample"]
E -- Yes --> F["Signed acceptance evidence by scope"]

Implementation layer: Independent mathematical models, end-to-end harness and assurance evidence.

Dependencies / staging: #43 baseline, #53 reference arithmetic; start immediately; final integrated corpus consumes all chosen FIN-11–FIN-28 capabilities, #59 budgets and #60 independent acceptance.

Detailed design and security review

Independent correctness across entire economic lifecycles

Individual functions can agree with a mathematical model while their composition duplicates a claim, loses reserve capacity or allows two positions to collect the same fee. Establish an independently implemented ledger with clear asset ownership and liabilities; do not calculate expected results by invoking the same production library used to build the transaction.

Canonical state and reference design

Track actual authenticated assets, occupied/refundable CKB, each pool's principal reserve, active/tick liquidity, range position ownership and fee entitlement, protocol/hook charges, outstanding claims, signed intents and every unsettled per-owner currency delta. Explicitly define which balance sheets may offset each other, and prohibit silently cross-crediting unrelated users or asset identities. Reference profiles and numeric limits are pinned by source commit/contract, not by a marketing parity label.

Continuous test campaigns

1. Start at genesis with two enforced test assets and authenticated pool creation; add overlapping and disjoint positions, repeatedly cross ticks and collect fees.
2. Interleave donations, dynamic fees, custom-hook deltas, backed claims and native CKB capacity growth/closure.
3. Execute exact-output split/multihop routes, repeated-pool command plans, authorised migration and stale-state rebuilding under distinct signers.
4. Explore adversarial sequences: partial failure or omitted hook, unauthorised nonce reuse, unfulfilled balance obligation, fraudulent tick absence and mixed owner/fee credits.
5. Shrink every counterexample to a stable minimal source/transaction and retain the originally failing evidence even after a fix.

Mandatory financial properties

Evidence tiers and completion

Use a machine-readable status for every capability: planned, executable local-VM, stateful local-node, independently reproduced, reviewed, or deployed; no coercion from one tier to another. Re-run gates on the final exact source and full candidate bytes. #59 remains owner of real operational contention, while #60 owns independent application-level reproduction and publication disposition. This issue owns the mathematical and stateful differential oracle from day one, not just a final report.

End-to-end security flow

flowchart TD
    S["Frozen reference model and scenario seeds"] --> T["Construct stateful candidate transactions"]
    T --> V["Run all real CKB Script groups"]
    V --> C["Compare assets, ticks, fees, claims and liabilities"]
    C --> P{"All properties and budgets hold?"}
    P -- No --> X["Shrink and retain counterexample"]
    P -- Yes --> R["Advance evidence tier with exact identity"]

General audit and release criteria

• This work is confined to ordinary CellScript protocol packages, tested maths, authenticated state and existing off-chain SDK/adapter boundaries. No application action name can authorise a finance-specific grammar, VM or compiler feature.
• Freeze selected schema/domain/operation budget, accountable implementer, independent human review disposition and valid/late-invalid resource ceilings. Any missing generic language primitive must have its own small business-neutral issue and independent-machine verification.
• Execute authentic full CKB transactions with all required Lock and Type groups, preserve original state continuity and distinct off-chain/VM/node/deployment evidence. Retain exact source, compiler/checker, artifact, CellDep, transaction and chain identities. Never claim a deployed or audited result without that evidence.

Design and delivery

• Create a versioned capability/economic contract matrix with owning issue, reference model source pin, supported domain, explicit adaptations and unsupported rows.
• Run independent stateful property/differential campaigns on price maths, tick index, positions/fees, donations, native capacity, claims, hooks, ordered deltas, signed intents, route plans and failures.
• Enforce a non-overlapping solvency equation separating principal, LP/position rights, fee liabilities, protocol/hook charges, claims and capacity/fees. Test combined as well as isolated invariants.
• Preserve exact sequence seeds, shrunk counterexamples, compiler/checker/source/ELF/CellDep/transaction/node environment and budget outcomes; compare the same final serialized transaction.

Acceptance criteria

• Every admitted capability has executable positive, boundary, adversarial and integration cases linked to its owning issue.
• Composed scenarios include overlapping range fee accrual, multihop exact-output with claims/native CKB, same-pool repeated operations, custom deltas, stale deadline and hostile subscriber.
• No unbacked liability, double credit, stolen refund, illegitimate fee/principal conversion or hidden debt is missed by independent calculations.
• Failures preserve seeds and reproducible source/evidence; release/delivered scope is distinguished from development proof, node evidence, audits and deployment.

Security / scope boundary: Differential evidence is neither a universal correctness theorem nor an independent human audit; never silently shrink the tested domain or replace historical budgets.

General implementation and acceptance rules

• Issue status: proposed. Identify owners, reviewers and any actual review disposition explicitly; no release/deployment permission is implied.
• Deliver these semantics in ordinary CellScript protocol packages, standard library helpers or existing SDK boundaries. New compiler semantics require a separate demonstrably business-neutral failure case and checker/ABI/diagnostics contract.
• Freeze input/step/byte/cycle/capacity budgets, test genuine and hostile final CKB transactions with every required Script group, and archive pinned source/build/dependency/transaction/model identities and applicable gates.

Verified dependencies and implementation sequencing

Entry prerequisites: #43, #53.

Related evidence / integration owners: #59, #60.

Reason for this sequence: Start differential and financial-liability test tooling immediately. Later populate coverage from each selected #61–#78 capability; programme final acceptance is separately recorded in #60.

Dependency links are explanatory; they do not mark code as implemented, grant a reviewer waiver or set native GitHub issue blockers.