1 min read
engineeringprecision

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:

health_factor.rs
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-math reorders 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.

deterministic.rs
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 zkVM

Key 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.