Skip to main content

axiom/WrapInt32

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

Status​

  • Spec-only axiom module

Public API​

Types​

  • Int32

Lemmas​

wrapSpec(x : Int32) : ()​

Establishes bits(x) == bits(x) % 4294967296 in the current proof context.

Contract

ensures bits(x) == bits(x) % 4294967296;

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

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

Establishes bits(Int32.addWrap(a, b)) == (bits(a) + bits(b)) % 4294967296 in the current proof context.

Contract

ensures bits(Int32.addWrap(a, b)) == (bits(a) + bits(b)) % 4294967296;

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

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

Establishes bits(Int32.subWrap(a, b)) == (bits(a) + 4294967296 - bits(b)) % 4294967296 in the current proof context.

Contract

ensures bits(Int32.subWrap(a, b)) == (bits(a) + 4294967296 - bits(b)) % 4294967296;

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

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

Establishes bits(Int32.mulWrap(a, b)) == (bits(a) * bits(b)) % 4294967296 in the current proof context.

Contract

ensures bits(Int32.mulWrap(a, b)) == (bits(a) * bits(b)) % 4294967296;

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

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

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

Contract

requires -2147483648 <= toSigned(a) + toSigned(b);
requires toSigned(a) + toSigned(b) <= 2147483647;
ensures toSigned(Int32.addWrap(a, b)) == toSigned(a) + toSigned(b);

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

noOverflowMul(a : Int32, b : Int32) : ()​

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

Contract

requires -2147483648 <= toSigned(a) * toSigned(b);
requires toSigned(a) * toSigned(b) <= 2147483647;
ensures toSigned(Int32.mulWrap(a, b)) == toSigned(a) * toSigned(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/WrapInt32.
  • Exposes 6 trusted lemmas.