Skip to main content

axiom/WrapNat16

Reference for mo:core/axiom/WrapNat16 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/WrapNat16

Status​

  • Spec-only axiom module

Public API​

Types​

  • Nat16

Lemmas​

wrapSpec(x : Nat16) : ()​

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

Contract

ensures toNat(x) == toNat(x) % 65536;

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

add(a : Nat16, b : Nat16) : ()​

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

Contract

ensures toNat(Nat16.addWrap(a, b)) == (toNat(a) + toNat(b)) % 65536;

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

sub(a : Nat16, b : Nat16) : ()​

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

Contract

ensures toNat(Nat16.subWrap(a, b)) == (toNat(a) + 65536 - toNat(b)) % 65536;

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

mul(a : Nat16, b : Nat16) : ()​

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

Contract

ensures toNat(Nat16.mulWrap(a, b)) == (toNat(a) * toNat(b)) % 65536;

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

noOverflowAdd(a : Nat16, b : Nat16) : ()​

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

Contract

requires toNat(a) + toNat(b) < 65536;
ensures toNat(Nat16.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 : Nat16, b : Nat16) : ()​

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

Contract

requires toNat(a) * toNat(b) < 65536;
ensures toNat(Nat16.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/WrapNat16.
  • Exposes 6 trusted lemmas.