Skip to main content

axiom/IntPow

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

Status​

  • Spec-only axiom module

Public API​

Types​

  • Int

Lemmas​

powZeroExp(a : Int) : ()​

Establishes Int.pow(a, 0) == 1 in the current proof context.

Contract

ensures Int.pow(a, 0) == 1;

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

powStep(a : Int, n : Int) : ()​

Establishes Int.pow(a, n + 1) == Int.pow(a, n) * a in the current proof context.

Contract

requires n >= 0;
ensures Int.pow(a, n + 1) == Int.pow(a, n) * a;

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

powZeroBase(n : Int) : ()​

Establishes Int.pow(0, n + 1) == 0 in the current proof context.

Contract

requires n >= 0;
ensures Int.pow(0, n + 1) == 0;

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

powEvenNeg(a : Int, n : Int) : ()​

Establishes Int.pow(-a, 2 * n) == Int.pow(a, 2 * n) in the current proof context.

Contract

requires n >= 0;
ensures Int.pow(-a, 2 * n) == Int.pow(a, 2 * n);

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

powOddNeg(a : Int, n : Int) : ()​

Establishes Int.pow(-a, 2 * n + 1) == -Int.pow(a, 2 * n + 1) in the current proof context.

Contract

requires n >= 0;
ensures Int.pow(-a, 2 * n + 1) == -Int.pow(a, 2 * n + 1);

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

powMonoExp(a : Int, n : Int, m : Int) : ()​

Establishes Int.pow(a, n) <= Int.pow(a, m) in the current proof context.

Contract

requires a >= 1;
requires n >= 0;
requires m >= 0;
requires n <= m;
ensures Int.pow(a, n) <= Int.pow(a, m);

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

powAddExp(a : Int, n : Int, m : Int) : ()​

Establishes Int.pow(a, n + m) == Int.pow(a, n) * Int.pow(a, m) in the current proof context.

Contract

requires n >= 0;
requires m >= 0;
ensures Int.pow(a, n + m) == Int.pow(a, n) * Int.pow(a, m);

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