Floating Point

IEEE 754 double-precision floating point with Float. Use sparingly in verified code because the verifier treats Float as an uninterpreted type.

Overview

Float represents 64-bit IEEE 754 double-precision floating-point numbers. At runtime, Float supports the full range of arithmetic operations, comparisons, and mathematical functions. However, for verification purposes, Float is modeled as a backend Float sort with opaque operations. Equality and expression identity are useful, but Sector9 does not provide IEEE arithmetic, rounding, NaN, infinity, or ordering axioms to the prover.

float-basic.sr9

// Basic Float operations - IEEE 754 double-precision floating point

module {
  // Float literals in decimal notation
  public func constants() : (Float, Float, Float) {
    let pi = 3.141592653589793;
    let small = 0.001;
    let scientific = 1.5e-10;  // Scientific notation
    (pi, small, scientific)
  };

  // Basic arithmetic operations
  public func arithmetic(a : Float, b : Float) : Float {
    let sum = a + b;
    let diff = a - b;
    let prod = a * b;
    sum
  };

  // Comparison operations
  public func compare(x : Float, y : Float) : Bool {
    x < y or x == y or x > y
  };
}

Literal Syntax

Float literals use decimal notation with optional exponential form:

let a = 3.14;              // Decimal with fractional part
let b = 1.0;               // Must include decimal point
let c = 1e-10;             // Scientific notation (1 × 10⁻¹⁰)
let d = 2.5e3;             // 2500.0
let e = -0.5;              // Negative literal

Float literals require a decimal point or exponent to distinguish them from integers.

Runtime Operations

At runtime, Float supports comprehensive arithmetic and mathematical operations:

Arithmetic

Operation	Syntax	Description
Addition	a + b	Sum
Subtraction	a - b	Difference
Multiplication	a * b	Product
Division	a / b	Quotient
Modulo	a % b	Remainder
Power	a ** b	Exponentiation
Negation	-a	Sign flip

Comparisons

Operation	Syntax
Equal	a == b
Not equal	a != b
Less than	a < b
Greater than	a > b
Less or equal	a <= b
Greater or equal	a >= b

Standard Library Functions

The core library provides a Float module. Prefer this over Prim:

import Float "mo:core/Float";

Float wraps the same runtime operations as Prim, but keeps user code off the low-level primitives:

Float.abs(x)        // Absolute value
Float.sqrt(x)       // Square root
Float.ceil(x)       // Round up
Float.floor(x)      // Round down
Float.trunc(x)      // Truncate toward zero
Float.nearest(x)    // Round to nearest
Float.min(x, y)     // Minimum
Float.max(x, y)     // Maximum

Float.sin(x)        // Sine
Float.cos(x)        // Cosine
Float.tan(x)        // Tangent
Float.arcsin(x)     // Arc sine
Float.arccos(x)     // Arc cosine
Float.arctan(x)     // Arc tangent

Float.exp(x)        // e^x
Float.log(x)        // Natural logarithm

Float.toInt(x)      // Float to Int (truncates)
Float.fromInt(n)    // Int to Float

The Prim module provides the low-level equivalents:

Prim.floatAbs(x)      // Absolute value
Prim.floatSqrt(x)     // Square root
Prim.floatCeil(x)     // Round up
Prim.floatFloor(x)    // Round down
Prim.floatTrunc(x)    // Truncate toward zero
Prim.floatNearest(x)  // Round to nearest
Prim.floatMin(x, y)   // Minimum
Prim.floatMax(x, y)   // Maximum

// Trigonometric
Prim.sin(x)           // Sine
Prim.cos(x)           // Cosine
Prim.tan(x)           // Tangent
Prim.arcsin(x)        // Arc sine
Prim.arccos(x)        // Arc cosine
Prim.arctan(x)        // Arc tangent

// Exponential/Logarithmic
Prim.exp(x)           // e^x
Prim.log(x)           // Natural logarithm

// Conversions
Prim.floatToInt(x)    // Float to Int (truncates)
Prim.intToFloat(n)    // Int to Float

Verification Model

In Sector9's verification, Float operations are deliberately opaque. This means:

• Equality is verified: The verifier reasons about == and != on floats
• Expression identity is verified: returning a + b can satisfy ensures result == a + b, because both sides are the same symbolic expression
• Arithmetic facts are not verified: operations like +, -, *, / do not give the prover algebraic facts such as monotonicity, identities, associativity, or bounds
• Ordering is opaque: comparisons like <, <=, >, >= are modeled but have no IEEE ordering theory
• No IEEE semantics: Special values (NaN, Infinity), rounding, and precision are not modeled

What Works in Verification

Contracts involving Float equality verify correctly:

float-equality.sr9

// Float equality in verification - the only verified operation

module {
  // Equality comparison is verified
  public func compareFloat(a : Float, b : Float) : Bool
    ensures result == (a == b);
  {
    a == b
  };

  // Reflexivity holds for all floats
  public func floatSelfEqual(f : Float) : Bool
    ensures result == true;
  {
    f == f
  };

  // Identity preserves value
  public func identityFloat(f : Float) : Float
    ensures result == f;
  {
    f
  };

  // Conditional selection works with floats
  public func selectFloat(cond : Bool, a : Float, b : Float) : Float
    ensures cond ==> result == a;
    ensures (not cond) ==> result == b;
  {
    if (cond) { a } else { b }
  };
}

What Does Not Work

The verifier cannot prove meaningful properties about Float arithmetic:

Equality (Works)

public func identity(f : Float) : Float
ensures result == f;  // Equality: verified
{ f }

Arithmetic (Fails)

float-unverified_unsat.sr9

// Float arithmetic has no useful IEEE arithmetic theory in verification

module {
  // WRONG: The verifier cannot prove arithmetic facts about a + b.
  public func additionIsIdentity(a : Float, b : Float) : Float
    ensures result == a;
  {
    a + b
  };
}

The arithmetic example fails verification because a + b produces an opaque value; Sector9 cannot prove it equals a for all b. For verified arithmetic properties, prefer Nat, Int, fixed-width integers, or fixed-point encodings over integers.

Why Uninterpreted?

Modeling IEEE 754 semantics precisely is complex:

• Special values: NaN, positive/negative infinity, positive/negative zero
• Rounding modes: Nearest, toward zero, toward positive/negative infinity
• Precision limits: Operations may lose precision
• Non-associativity: (a + b) + c may not equal a + (b + c)

Rather than model these incompletely or unsoundly, Sector9 takes the conservative approach of treating Float as uninterpreted. This means:

• Verified properties are sound (never falsely claim correctness)
• You cannot verify IEEE arithmetic properties on floats
• Use integer arithmetic when you need verified numeric reasoning

When to Use Float

Use Float when:

• You need floating-point math at runtime but not in contracts
• Contracts only check Float equality or identity
• You're interfacing with external systems expecting IEEE 754

Avoid Float when:

• You need verified arithmetic properties
• Precision and rounding matter for correctness
• You can use fixed-point or integer arithmetic instead

Alternative Approaches

When you need verified numeric properties, consider these alternatives:

Fixed-Point with Integers

Use integers with an implicit decimal point:

// Represent dollars as cents (2 decimal places)
var balance : Nat = 10050;  // $100.50

public func addCents(amount : Nat) : async Nat
  modifies balance
  ensures balance == old(balance) + amount
{
  balance += amount;
  balance
}

Bounded Rational Approximations

For ratios, use pairs of integers:

// Represent ratio as numerator/denominator
public func percentage(part : Nat, whole : Nat) : async Nat
  entry_requires whole > 0;
  requires whole > 0;
  ensures result == (part * 100) / whole;
{
  (part * 100) / whole
}

Float in Spec Collections

Float values can be stored in spec collections (Map, Set, Seq, Multiset) because they are immutable primitives. The verifier can reason about collection membership and equality:

module {
  public ghost func remember(seen : Set<Float>, f : Float) : Set<Float>
    ensures Set.contains(f, result);
  {
    Set.union(seen, Set.singleton(f))
  };
}

Common Patterns

Runtime Float with Verified Guards

Use entry_requires for equality-style Float guards on exported methods:

public func safeDivide(a : Float, b : Float) : async Float
  entry_requires b != 0.0;
  requires b != 0.0;
{
  a / b
}

The verifier can use the equality guard, but it still does not prove IEEE arithmetic facts about the division result.

Float as Opaque Data

When Float is just data passing through, verification works:

var stored : Float = 0.0;

public func setFloat(f : Float) : async ()
  modifies stored
  ensures stored == f
{
  stored := f;
}

public func getFloat() : async Float
  reads stored
  ensures result == stored
{
  stored
}

Summary

• Float is IEEE 754 double-precision floating point
• Literals use decimal notation: 3.14, 1e-10, -0.5
• Runtime supports full arithmetic, comparisons, and math functions
• Verification treats Float as uninterpreted - only equality is reasoned about
• Arithmetic contracts on Float values will not verify
• Use integers or fixed-point arithmetic when you need verified numeric properties
• Float can be used in spec collections and passed as opaque data