Skip to main content

axiom/IntDivMod

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

Status​

  • Spec-only axiom module

Public API​

Types​

  • Int

Lemmas​

divModDecomp(a : Int, c : Int) : ()​

Establishes a == (a / c) * c + (a % c) in the current proof context.

Contract

requires c != 0;
ensures a == (a / c) * c + (a % c);

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

modNonnegPos(a : Int, c : Int) : ()​

Establishes 0 <= a % c in the current proof context.

Contract

requires c > 0;
requires 0 <= a;
ensures 0 <= a % c;

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

modLtPos(a : Int, c : Int) : ()​

Establishes a % c < c in the current proof context.

Contract

requires c > 0;
ensures a % c < c;

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

divCharPos(a : Int, c : Int, q : Int) : ()​

Establishes (a / c == q) <==> (q * c <= a and a < (q + 1) * c) in the current proof context.

Contract

requires c > 0;
requires 0 <= a;
ensures (a / c == q) <==> (q * c <= a and a < (q + 1) * c);

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

divNegDenomExact(a : Int, c : Int) : ()​

Establishes a / (-c) == -(a / c) in the current proof context.

Contract

requires c > 0;
requires a % c == 0;
ensures a / (-c) == -(a / c);

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

modNegDenomExact(a : Int, c : Int) : ()​

Establishes a % (-c) == a % c in the current proof context.

Contract

requires c > 0;
requires a % c == 0;
ensures a % (-c) == a % c;

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

modAddMulInvariant(a : Int, c : Int, k : Int) : ()​

Establishes (a + k * c) % c == a % c in the current proof context.

Contract

requires c > 0;
requires 0 <= a;
requires 0 <= a + k * c;
ensures (a + k * c) % c == a % c;

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

divAddMulInvariant(a : Int, c : Int, k : Int) : ()​

Establishes (a + k * c) / c == a / c + k in the current proof context.

Contract

requires c > 0;
requires 0 <= a;
requires 0 <= a + k * c;
ensures (a + k * c) / c == a / c + k;

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

modIfRangePos(a : Int, c : Int) : ()​

Establishes a % c == a in the current proof context.

Contract

requires c > 0;
requires 0 <= a;
requires a < c;
ensures a % c == a;

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/IntDivMod.
  • Exposes 9 trusted lemmas.