[DeFi][FIN-03][M1] Freeze checked financial arithmetic, rounding and reference model #53

Implementation ownership — protocol-first, no finance-specific compiler feature

Primary implementation layer: general arithmetic library where needed, plus protocol-level financial mathematics and independent evidence. mulDivFloor, mulDivCeil and isqrt in this issue are candidate helper APIs, not new compiler operators, finance keywords or automatically accepted builtin intrinsics.

Implementation shape: keep AMM fee formulae, LP pricing and order entitlements in the protocol package. Build an independent arbitrary-precision model in host-side tests. First implement provably bounded checked operations through existing CellScript primitives and reusable library functions. Only if a concrete expression cannot be implemented safely within the admitted numeric domain, propose a separate business-neutral wide arithmetic or checked-conversion library/backend contract, supported by a non-DeFi example and precise checker, resource and ABI evidence.

Acceptance interpretation: model-to-VM agreement is required; shipping a new financial API surface or a domain-specific multiplication opcode is not an acceptance objective.

Compiler-change gate (all FIN work): This issue does not authorise finance-specific grammar, IR, opcodes, codegen branches or hidden protocol semantics. First try existing general CellScript constructs. Any genuinely missing general capability needs a minimal failing application, a non-financial use case, its own narrow issue and independent checker/ABI/resource/gate acceptance as required by #43 §2.2. Application correctness and builder convenience are distinct from language support.

Parent: #43, FIN-03/M1. Status: proposed; implementation/review/release not claimed.
Owner role: arithmetic/stdlib engineer; reviewer: unassigned until FIN-01/M0.

Dependencies

• Entry: [DeFi][Application/Protocol] EVM-class finance on CKB with CellScript #43 FIN-01/M0.
• Coupled protocol input: [DeFi][FIN-02][M1] Enforce authentic pool custody, asset identity and LP supply #52 FIN-02 must identify proposed reserve, asset, fee and LP numerical domains before arithmetic acceptance is frozen. Work in parallel; a fully closed FIN-02 is not required to begin.
• Unblocks FIN-04 pool and FIN-06 partial-fill orders. Reuse existing compiler arithmetic, [0.30][Runtime] Complete typed bounded CKB transaction-view and syscall adapters #24 transaction views and [0.30][Acceptance] Build the canonical Rust-comparable CKB business corpus #26 business fixtures.

Scope

1. Freeze operand, intermediate, aggregate and result widths; amount/reserve/share ceilings; allowed conversions; zero denominators; overflow, underflow, narrowing and first-failure semantics. Preserve current checked operations; no implicit change to existing editions.
2. Define reusable financial primitives/relations: checked arithmetic, mulDivFloor(a,b,d), mulDivCeil(a,b,d), nonnegative integer square-root floor, and exact product/product-sum comparisons. These names are design labels, not pre-existing CellScript spellings.
3. Account for u128 × u128 products and further fee scaling; prove every intermediate fits its selected representation or explicitly reject out-of-domain inputs. In particular, a multiplication overflow is not legitimised by a later division.
4. Build a separately implemented arbitrary-precision reference model with reproducible boundary and adversarial sequences, seeds and shrunk counterexamples. Compare builder, model and actual CKB-VM executions.
5. Evaluate direct full-width computation versus builder-provided quotient with on-chain exact floor/ceil relation checks; report cycles, ELF, witness bytes and tradeoffs. Do not commit to a global algorithm without evidence.
6. With [DeFi][FIN-02][M1] Enforce authentic pool custody, asset identity and LP supply #52 execute [DeFi][Application/Protocol] EVM-class finance on CKB with CellScript #43 §11.1's real two-asset pool → swap → LP withdrawal slice and bind observed values to independent calculations.

Acceptance

• Freeze versioned width/domain/rounding/fee contract and exact error cases, including zero/one/max/just-outside and non-representable but mathematically valid intermediate products.
• Model independently verifies floor/ceil quotient inequalities, square-root relations, conversion, reserve/share/fee conservation and sequence totals without reusing production helpers.
• Positive and hostile model/builder/whole-transaction cases agree for the admitted domains; zero denominator, incorrect quotient/remainder, rounding drift, overflow and unsafe narrowing reject at intended boundary.
• Any compiler/stdlib extension presents a concrete failing example, business-neutral general API, other non-financial use case, checker and compatibility impact; no action-name-based codegen.
• Joint FIN-02/03 executable slice, source/model/test identities, frozen preliminary budgets, independent checker mutations, relevant dev/backend/CI gates and scope-specific review disposition are recorded.

Non-goals: arbitrary-precision on-chain heap, generic fixed-point financial DSL, tick mathematics, lending-specific risk engines and protocol-specific compiler opcodes. Ref: #43 §§2.2, 4, 6, 11–12.

Dependency cross-links (confirmed GitHub issues)

Depends on: #43 FIN-01/M0 and the selected asset/reserve/share topology from #52 FIN-02. Co-develop with: #52; issue closure is not a prerequisite for starting arithmetic experiments. Required by: #54 FIN-04 and #56 FIN-06. Both FIN-02/03 own the joint §11.1 executable slice.

Umbrella dependency graph and authoritative financial acceptance: #43.