@theoremts/contracts-bignumber

Theorem contracts for bignumber.js — formal verification for arbitrary-precision arithmetic.

Installation

npm install -D @theoremts/contracts-bignumber

Auto-discovered by Theorem — zero config needed.

What's included

Complete coverage of the bignumber.js API:

| Method | Z3 translation | |---|---| | .plus(b) / .minus(b) / .times(b) | a + b / a - b / a * b | | .dividedBy(b) / .div(b) | a / b (requires b !== 0) | | .idiv(b) | integer division (requires b !== 0) | | .modulo(b) / .mod(b) | modulo (requires b !== 0) | | .exponentiatedBy(b) / .pow(b) | a ** b | | .negated() | -a | | .absoluteValue() / .abs() | abs(a) | | .squareRoot() / .sqrt() | sqrt(a) (requires a >= 0) | | .isGreaterThan(b) / .gt(b) | a > b | | .isLessThan(b) / .lt(b) | a < b | | .isEqualTo(b) / .eq(b) | a === b | | .isZero() / .isPositive() / .isNegative() | a === 0 / a > 0 / a < 0 | | .isInteger() | integer(a) | | .integerValue() | result is integer | | .toNumber() | identity | | .shiftedBy(n) | a * 10^n | | BigNumber.max(a, b) | output >= a && output >= b | | BigNumber.min(a, b) | output <= a && output <= b | | BigNumber.sum(a, b) | a + b | | BigNumber.random() | 0 <= output < 1 |

Example

import BigNumber from 'bignumber.js'
import { requires, ensures, positive, output } from 'theoremts'

function safeTransfer(from: BigNumber, to: BigNumber, amount: BigNumber) {
  requires(amount.isPositive())
  requires(from.isGreaterThanOrEqualTo(amount))
  ensures(output().isGreaterThanOrEqualTo(0))

  return from.minus(amount)
}

License

MIT