Skip to main content

axiom/WrapInt64

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

Status​

  • Spec-only axiom module

Public API​

Types​

  • Int64

Functions​

toBitsNatSpec(x : Int64) : Nat​

Converts between the module type and the target representation.

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

bits(x : Int64) : Nat​

Performs the corresponding bit-level operation.

Contract

ensures result == toBitsNatSpec(x);

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

toSigned(x : Int64) : Int​

Converts between the module type and the target representation.

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

addWrap(a : Int64, b : Int64) : Int64​

Returns wrapping addition for the fixed-width type.

Contract

ensures -9_223_372_036_854_775_808 <= result;
ensures result <= 9_223_372_036_854_775_807;
ensures bits(result) == (bits(a) + bits(b)) % 18_446_744_073_709_551_616;

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

subWrap(a : Int64, b : Int64) : Int64​

Returns wrapping subtraction for the fixed-width type.

Contract

ensures -9_223_372_036_854_775_808 <= result;
ensures result <= 9_223_372_036_854_775_807;
ensures bits(result) == (bits(a) + 18_446_744_073_709_551_616 - bits(b)) % 18_446_744_073_709_551_616;

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

mulWrap(a : Int64, b : Int64) : Int64​

Returns wrapping multiplication for the fixed-width type.

Contract

ensures -9_223_372_036_854_775_808 <= result;
ensures result <= 9_223_372_036_854_775_807;
ensures bits(result) == (bits(a) * bits(b)) % 18_446_744_073_709_551_616;

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

Lemmas​

wrapSpec(x : Int64) : ()​

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

Contract

ensures bits(x) == bits(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 : Int64, b : Int64) : ()​

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

Contract

ensures bits(addWrap(a, b)) == (bits(a) + bits(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 : Int64, b : Int64) : ()​

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

Contract

ensures bits(subWrap(a, b)) == (bits(a) + 18_446_744_073_709_551_616 - bits(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 : Int64, b : Int64) : ()​

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

Contract

ensures bits(mulWrap(a, b)) == (bits(a) * bits(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 : Int64, b : Int64) : ()​

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

Contract

requires -9_223_372_036_854_775_808 <= toSigned(a) + toSigned(b);
requires toSigned(a) + toSigned(b) <= 9_223_372_036_854_775_807;
ensures toSigned(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 : Int64, b : Int64) : ()​

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

Contract

requires -9_223_372_036_854_775_808 <= toSigned(a) * toSigned(b);
requires toSigned(a) * toSigned(b) <= 9_223_372_036_854_775_807;
ensures toSigned(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/WrapInt64.
  • Exposes 6 public functions.
  • Exposes 6 trusted lemmas.