Skip to main content

Int8

Reference for mo:core/Int8 in the core library.

Int8 is a checked signed 8-bit surface. Use checked constructors and arithmetic when you want proof obligations for the valid range; use Wrap variants when wraparound behavior is the intended model.

Import​

mo:core/Int8

Status​

  • Runtime module

Public API​

Types​

  • Int8

Values​

  • minValue
  • maxValue

Functions​

toBitsNatSpec(x : Int8) : Nat​

Converts between the module type and the target representation.

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

toInt(x : Int8) : Int​

Converts between the module type and the target representation.

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

fromInt(x : Int) : Int8​

Converts between the module type and the target representation.

Contract

requires x >= -128;
requires x <= 127;

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

fromIntWrap(x : Int) : Int8​

Converts between the module type and the target representation.

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

fromInt16(x : Int16) : Int8​

Converts between the module type and the target representation.

Contract

requires x >= (-128 : Int16);
requires x <= (127 : Int16);

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

toInt16(x : Int8) : Int16​

Converts between the module type and the target representation.

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

fromNat8(x : Nat8) : Int8​

Converts between the module type and the target representation.

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

toNat8(x : Int8) : Nat8​

Converts between the module type and the target representation.

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

toText(x : Int8) : Text​

Converts between the module type and the target representation.

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

abs(x : Int8) : Int8​

Returns the absolute value.

Contract

requires x != minValue;
ensures result == (if (x < 0) { -x } else { x });

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

min(x : Int8, y : Int8) : Int8​

Returns the selected bound according to the module's ordering.

Contract

ensures result == (if (x < y) { x } else { y });

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

max(x : Int8, y : Int8) : Int8​

Returns the selected bound according to the module's ordering.

Contract

ensures result == (if (x < y) { y } else { x });

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

equal(x : Int8, y : Int8) : Bool​

Compares the supplied values and relates the result to the underlying order.

Contract

ensures result == (x == y);

Use when: code or contracts need an explicit comparison helper instead of an operator.

notEqual(x : Int8, y : Int8) : Bool​

Compares the supplied values and relates the result to the underlying order.

Contract

ensures result == (x != y);

Use when: code or contracts need an explicit comparison helper instead of an operator.

less(x : Int8, y : Int8) : Bool​

Compares the supplied values and relates the result to the underlying order.

Contract

ensures result == (x < y);

Use when: code or contracts need an explicit comparison helper instead of an operator.

lessOrEqual(x : Int8, y : Int8) : Bool​

Compares the supplied values and relates the result to the underlying order.

Contract

ensures result == (x <= y);

Use when: code or contracts need an explicit comparison helper instead of an operator.

greater(x : Int8, y : Int8) : Bool​

Compares the supplied values and relates the result to the underlying order.

Contract

ensures result == (x > y);

Use when: code or contracts need an explicit comparison helper instead of an operator.

greaterOrEqual(x : Int8, y : Int8) : Bool​

Compares the supplied values and relates the result to the underlying order.

Contract

ensures result == (x >= y);

Use when: code or contracts need an explicit comparison helper instead of an operator.

compare(x : Int8, y : Int8) : Types.Order​

Compares the supplied values and relates the result to the underlying order.

Contract

ensures result == #less ==> x < y;
ensures result == #equal ==> x == y;
ensures result == #greater ==> x > y;
ensures x < y ==> result == #less;
ensures x == y ==> result == #equal;
ensures x > y ==> result == #greater;

Use when: code or contracts need an explicit comparison helper instead of an operator.

neg(x : Int8) : Int8​

Returns the arithmetic negation.

Contract

requires x != (-128 : Int8);
ensures result == -x;
ensures inRange(result);

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

add(x : Int8, y : Int8) : Int8​

Returns the sum of the two operands.

Contract

requires (-128 : Int8) <= x + y;
requires x + y <= (127 : Int8);
ensures result == x + y;
ensures inRange(result);

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

sub(x : Int8, y : Int8) : Int8​

Returns the left operand minus the right operand.

Contract

requires (-128 : Int8) <= x - y;
requires x - y <= (127 : Int8);
ensures result == x - y;
ensures inRange(result);

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

mul(x : Int8, y : Int8) : Int8​

Returns the product of the two operands.

Contract

requires (-128 : Int8) <= x * y;
requires x * y <= (127 : Int8);
ensures result == x * y;
ensures inRange(result);

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

div(x : Int8, y : Int8) : Int8​

Returns the integer quotient, subject to the divisor precondition.

Contract

requires y != 0;
requires not (x == (-128 : Int8) and y == (-1 : Int8));
ensures y != 0 ==> result == x / y;
ensures inRange(result);

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

rem(x : Int8, y : Int8) : Int8​

Returns the integer remainder, subject to the divisor precondition.

Contract

requires y != 0;
ensures y != 0 ==> result == x % y;
ensures inRange(result);

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

pow(x : Int8, y : Int8) : Int8​

Returns the left operand raised to the supplied exponent.

Contract

requires y >= (0 : Int8);
requires y < (8 : Int8);
requires y <= (1 : Int8) or
(-128 <= Int.pow(toInt(x), toInt(y)) and Int.pow(toInt(x), toInt(y)) <= 127);
ensures (y >= 0 and y < (8 : Int8)) ==>
toBitsNatSpec(result) == Nat.pow(toBitsNatSpec(x), toBitsNatSpec(y)) % 256;
ensures y == 0 ==> result == 1;
ensures y == 1 ==> result == x;
ensures inRange(result);

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

bitnot(x : Int8) : Int8​

Performs the corresponding bit-level operation.

Contract

ensures inRange(result);

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

bitand(x : Int8, y : Int8) : Int8​

Performs the corresponding bit-level operation.

Contract

ensures inRange(result);

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

bitor(x : Int8, y : Int8) : Int8​

Performs the corresponding bit-level operation.

Contract

ensures inRange(result);

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

bitxor(x : Int8, y : Int8) : Int8​

Performs the corresponding bit-level operation.

Contract

ensures inRange(result);

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

bitshiftLeft(x : Int8, y : Int8) : Int8​

Performs the corresponding bit-level operation.

Contract

ensures inRange(result);
ensures y == 0 ==> result == x;

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

bitshiftRight(x : Int8, y : Int8) : Int8​

Performs the corresponding bit-level operation.

Contract

ensures inRange(result);
ensures y == 0 ==> result == x;

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

bitrotLeft(x : Int8, y : Int8) : Int8​

Performs the corresponding bit-level operation.

Contract

ensures inRange(result);
ensures y == 0 ==> result == x;

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

bitrotRight(x : Int8, y : Int8) : Int8​

Performs the corresponding bit-level operation.

Contract

ensures inRange(result);
ensures y == 0 ==> result == x;

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

bittest(x : Int8, p : Nat) : Bool​

Performs the corresponding bit-level operation.

Contract

ensures result == Prim.btstInt8(x, Prim.intToInt8(p));

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

bitset(x : Int8, p : Nat) : Int8​

Performs the corresponding bit-level operation.

Contract

ensures inRange(result);
ensures p >= 8 ==> result == x;

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

bitclear(x : Int8, p : Nat) : Int8​

Performs the corresponding bit-level operation.

Contract

ensures inRange(result);
ensures p >= 8 ==> result == x;

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

bitflip(x : Int8, p : Nat) : Int8​

Performs the corresponding bit-level operation.

Contract

ensures inRange(result);
ensures p >= 8 ==> result == x;

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

bitcountNonZero(x : Int8) : Int8​

Performs the corresponding bit-level operation.

Contract

ensures result == Prim.popcntInt8(x);
ensures inRange(result);

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

bitcountLeadingZero(x : Int8) : Int8​

Performs the corresponding bit-level operation.

Contract

ensures result == Prim.clzInt8(x);
ensures inRange(result);

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

bitcountTrailingZero(x : Int8) : Int8​

Performs the corresponding bit-level operation.

Contract

ensures result == Prim.ctzInt8(x);
ensures inRange(result);

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

addWrap(x : Int8, y : Int8) : Int8​

Returns wrapping addition for the fixed-width type.

Contract

ensures inRange(result);

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

subWrap(x : Int8, y : Int8) : Int8​

Returns wrapping subtraction for the fixed-width type.

Contract

ensures inRange(result);

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

mulWrap(x : Int8, y : Int8) : Int8​

Returns wrapping multiplication for the fixed-width type.

Contract

ensures inRange(result);

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

powWrap(x : Int8, y : Int8) : Int8​

Returns wrapping exponentiation for the fixed-width type.

Contract

ensures (y >= 0 and y < (8 : Int8)) ==>
toBitsNatSpec(result) == Nat.pow(toBitsNatSpec(x), toBitsNatSpec(y)) % 256;
ensures y == 0 ==> result == 1;
ensures y == 1 ==> result == x;
ensures inRange(result);

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

range(fromInclusive : Int8, toExclusive : Int8) : Iter.Iter<Int8>​

Creates an iterator over the requested numeric range or domain.

Contract

ensures Iter.Spec.forall<Int8>(pure func (k : Int8) : Bool =
Iter.Spec.contains<Int8>(result, k) ==> (k >= fromInclusive and k < toExclusive));
ensures Iter.Spec.forall<Int8>(pure func (k : Int8) : Bool =
(k >= fromInclusive and k < toExclusive) ==> Iter.Spec.contains<Int8>(result, k));

Use when: iteration boundaries should be explicit in code and examples.

rangeInclusive(from : Int8, to : Int8) : Iter.Iter<Int8>​

Creates an iterator over the requested numeric range or domain.

Contract

ensures (from > to) ==> Iter.Spec.forall<Int8>(pure func (k : Int8) : Bool = not Iter.Spec.contains<Int8>(result, k));
ensures (from <= to) ==> Iter.Spec.contains<Int8>(result, from);
ensures Iter.Spec.forall<Int8>(pure func (k : Int8) : Bool =
Iter.Spec.contains<Int8>(result, k) ==> (k >= from and k <= to));
ensures Iter.Spec.forall<Int8>(pure func (k : Int8) : Bool =
(k >= from and k <= to) ==> Iter.Spec.contains<Int8>(result, k));

Use when: iteration boundaries should be explicit in code and examples.

allValues() : Iter.Iter<Int8>​

Creates an iterator over the requested numeric range or domain.

Contract

ensures Iter.Spec.forall<Int8>(pure func (k : Int8) : Bool =
Iter.Spec.contains<Int8>(result, k) ==> (k >= minValue and k <= maxValue));
ensures Iter.Spec.forall<Int8>(pure func (k : Int8) : Bool =
(k >= minValue and k <= maxValue) ==> Iter.Spec.contains<Int8>(result, k));

Use when: iteration boundaries should be explicit in code and examples.

Summary​

  • Runtime module under mo:core/Int8.
  • Exposes 48 public functions.