axiom/NatDivMod

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

Status

• Spec-only axiom module

Public API

Types

• Nat

Lemmas

divModDecomp(a : Nat, c : Nat) : ()

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.

modNonneg(a : Nat, c : Nat) : ()

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

Contract

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

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

modLt(a : Nat, c : Nat) : ()

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.

divChar(a : Nat, c : Nat, q : Nat) : ()

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

Contract

requires c > 0;
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.

modAddMulInvariant(a : Nat, c : Nat, k : Nat) : ()

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

Contract

requires c > 0;
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 : Nat, c : Nat, k : Nat) : ()

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

Contract

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

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

modIfLt(a : Nat, c : Nat) : ()

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

Contract

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

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

divMonoNum(a : Nat, b : Nat, c : Nat) : ()

Establishes a / c <= b / c in the current proof context.

Contract

requires c > 0;
requires a <= b;
ensures a / c <= b / c;

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/NatDivMod.
• Exposes 8 trusted lemmas.