axiom/WrapNat64

Reference for mo:core/axiom/WrapNat64 in the core library.

This page lists trusted proof lemmas. Calling one adds its ensures facts after its requires clauses are proven; the lemma body itself is part of the trusted base, not a verifier-checked derivation. Use these when ordinary SMT arithmetic needs a precise algebraic step.

Import

mo:core/axiom/WrapNat64

Status

• Spec-only axiom module

Public API

Types

• Nat64

Functions

toNatSpec(x : Nat64) : Nat

Converts between the module type and the target representation.

Use when: crossing between this module's value and another representation.

toNat(x : Nat64) : Nat

Converts between the module type and the target representation.

Contract

ensures result == toNatSpec(x);

Use when: crossing between this module's value and another representation.

addWrap(a : Nat64, b : Nat64) : Nat64

Returns wrapping addition for the fixed-width type.

Contract

ensures toNat(result) == (toNat(a) + toNat(b)) % 18_446_744_073_709_551_616;

Use when: the postcondition must relate the updated value to the previous one.

subWrap(a : Nat64, b : Nat64) : Nat64

Returns wrapping subtraction for the fixed-width type.

Contract

ensures toNat(result) == (toNat(a) + 18_446_744_073_709_551_616 - toNat(b)) % 18_446_744_073_709_551_616;

Use when: code or specifications need this operation with the documented contract.

mulWrap(a : Nat64, b : Nat64) : Nat64

Returns wrapping multiplication for the fixed-width type.

Contract

ensures toNat(result) == (toNat(a) * toNat(b)) % 18_446_744_073_709_551_616;

Use when: code or specifications need this operation with the documented contract.

Lemmas

wrapSpec(x : Nat64) : ()

Establishes toNat(x) == toNat(x) % 18_446_744_073_709_551_616 in the current proof context.

Contract

ensures toNat(x) == toNat(x) % 18_446_744_073_709_551_616;

Use when: a proof needs this fact explicitly and the solver has not derived it automatically.

add(a : Nat64, b : Nat64) : ()

Establishes toNat(addWrap(a, b)) == (toNat(a) + toNat(b)) % 18_446_744_073_709_551_616 in the current proof context.

Contract

ensures toNat(addWrap(a, b)) == (toNat(a) + toNat(b)) % 18_446_744_073_709_551_616;

Use when: a proof needs this fact explicitly and the solver has not derived it automatically.

sub(a : Nat64, b : Nat64) : ()

Establishes toNat(subWrap(a, b)) == (toNat(a) + 18_446_744_073_709_551_616 - toNat(b)) % 18_446_744_073_709_551_616 in the current proof context.

Contract

ensures toNat(subWrap(a, b)) == (toNat(a) + 18_446_744_073_709_551_616 - toNat(b)) % 18_446_744_073_709_551_616;

Use when: a proof needs this fact explicitly and the solver has not derived it automatically.

mul(a : Nat64, b : Nat64) : ()

Establishes toNat(mulWrap(a, b)) == (toNat(a) * toNat(b)) % 18_446_744_073_709_551_616 in the current proof context.

Contract

ensures toNat(mulWrap(a, b)) == (toNat(a) * toNat(b)) % 18_446_744_073_709_551_616;

Use when: a proof needs this fact explicitly and the solver has not derived it automatically.

noOverflowAdd(a : Nat64, b : Nat64) : ()

Establishes toNat(addWrap(a, b)) == toNat(a) + toNat(b) in the current proof context.

Contract

requires toNat(a) + toNat(b) < 18_446_744_073_709_551_616;
ensures toNat(addWrap(a, b)) == toNat(a) + toNat(b);

Use when: a proof needs this fact explicitly and the solver has not derived it automatically.

noOverflowMul(a : Nat64, b : Nat64) : ()

Establishes toNat(mulWrap(a, b)) == toNat(a) * toNat(b) in the current proof context.

Contract

requires toNat(a) * toNat(b) < 18_446_744_073_709_551_616;
ensures toNat(mulWrap(a, b)) == toNat(a) * toNat(b);

Use when: a proof needs this fact explicitly and the solver has not derived it automatically.

Summary

• Spec-only axiom module under mo:core/axiom/WrapNat64.
• Exposes 5 public functions.
• Exposes 6 trusted lemmas.