Why DeFi Needs Deterministic Arithmetic
Financial protocols assume arithmetic is exact. It is not.
IEEE 754 floating-point produces different results depending on the platform, compiler optimizations, and instruction ordering. A health factor calculation that returns 1.0001 on x86 might return 0.9999 on ARM — the difference between a solvent position and a liquidation.
The Problem
Consider a lending protocol calculating a user's health factor:
let collateral_value = collateral_amount * collateral_price;
let debt_value = debt_amount * debt_price;
let health_factor = collateral_value / debt_value;With f64, this calculation is non-deterministic. The result depends on:
- Platform: x86 uses 80-bit extended precision internally; ARM uses 64-bit
- Compiler flags:
-ffast-mathreorders operations, changing rounding - WASM vs native: Different intermediate precision guarantees
A ZK proof generated on one platform cannot be verified on another if the arithmetic disagrees.
The Solution
Keystone's precision-core crate provides 128-bit decimal arithmetic with 28 significant digits. Every operation is deterministic — the same inputs produce the same output regardless of target architecture.
use precision_core::Decimal;
let collateral = Decimal::new(15000, 2); // 150.00
let debt = Decimal::new(10000, 2); // 100.00
let health_factor = collateral / debt; // 1.5000000000000000000000000000
// Same result on x86, ARM, WASM, and inside SP1 zkVMKey properties:
- 28 significant digits — sufficient for any financial calculation
- 7 rounding modes — including banker's rounding (IEEE 754 default)
- no_std compatible — runs in smart contracts, ZK VMs, and embedded systems
- Overflow-safe — checked operations prevent silent precision loss
On-Chain: Arbitrum Stylus
Keystone ships 5 Stylus smart contracts demonstrating precision arithmetic on Arbitrum:
- Lending — health factor, liquidation price, max borrow
- AMM — constant product swaps, price impact, liquidity math
- Vault — ERC4626 share pricing, compound yield, APY conversion
- Options — Black-Scholes pricing, Greeks, implied volatility
- Oracle — RedStone price feeds, TWAP, deviation detection
Each contract converts between Solidity's U256 fixed-point and Keystone's Decimal type, performs the calculation with full precision, then converts back.
Verifiable
Keystone arithmetic is formally verified with Kani model checking (17 proof harnesses) and provable inside Succinct's SP1 zkVM. A calculation performed on-chain can be independently verified with a zero-knowledge proof — the prover and verifier agree on the result because the arithmetic is deterministic.
This is the foundation for verifiable financial computation.