MimIR
MimIR is my Intermediate Representation
Loading...
Searching...
No Matches
The core Plugin

Table of Contents

See also
mim::plug::core

Dependencies

plugin mem;

Nat Operations

%core.nat

Standard arithmetic operations on Nats.
%core.nat.sub (a, b) yields 0, if a < b.

axm %core.nat(add, sub, mul): «2; Nat» → Nat, normalize_nat;

%core.ncmp

Nat comparison is made of 3 disjoint relations:

  • Greater
  • Less
  • Equal
Subtag Alias G L E Meaning
gle f o o o always false
glE e o o x equal
gLe l o x o less
gLE le o x x less or equal
Gle g x o o greater
GlE ge x o x greater or equal
GLe ne x x o not equal
GLE t x x x always true
axm %core.ncmp(gle = f, glE = e, gLe = l, gLE = le,
Gle = g, GlE = ge, GLe = ne, GLE = t):
«2; Nat» → Bool, normalize_ncmp;

Integer Operations

Integer operations use Idx s as type. This is per se neither signed nor unsigned. Instead, the operations themselves exhibit signed or unsigned behavior.

For Idx s,

  • unsigned interpretation is the canonical carrier order on the finite set / $ \{ 0, \dots, s-1 \} $.
  • signed interpretation is defined by choosing, for each residue class modulo $s$, / its canonical signed representative.

Concretely, a value $x : \mathrm{Idx}\;s$ is considered non-negative iff / $ x \le \lfloor (s-1)/2 \rfloor $, and negative otherwise. Hence the signed range is $ \big[ -\lfloor s/2 \rfloor,\; \lceil s/2 \rceil - 1 \big] $. For powers of two, i.e. $ s = 2^w $, this coincides exactly with the usual $w$-bit two's-complement interpretation.

Mode

A common problem when dealing with integer operations is overflow. All operations that may overflow have an additional parameter m - mode - of type Nat that determines the exact desired behavior in the case of an overflow.

let %core.mode.us = 0b00; // wrap around - both signed and unsigned
let %core.mode.uS = 0b01; // no signed wrap around
let %core.mode.Us = 0b10; // no unsigned wrap around
let %core.mode.US = 0b11; // no signed and unsigned wrap around
let %core.mode.nsw = %core.mode.uS;
let %core.mode.nuw = %core.mode.Us;
let %core.mode.nsuw = %core.mode.US;

%core.idx

Creates a literal of type Idx s from l while obeying mode m.

axm %core.idx: [s: Nat] → [m: Nat] → [l: Nat] → Idx s, normalize_idx;

Creates a literal of type Idx ⊤.

axm %core.idx_unsafe: Nat → Idx ⊤:Nat, normalize_idx_unsafe;

%core.bit1

This unary bitwise operations offers all 4 possible operations as summarized in the following table:

Subtag A a Comment
f o o always false
neg o x negate
id x o identity
t x x always true
Todo
Add type constraint that bit1 is only allowed for powers of two.
axm %core.bit1(f, neg, id, t): {s: Nat} → [m: Nat] → Idx s → Idx s, normalize_bit1;

%core.bit2

This binary bitwise operations offers all 16 possible operations as summarized in the following table:

Subtag AB Ab aB ab Comment
f o o o o always false
nor o o o x not or
nciff o o x o not converse implication
nfst o o x x not first argument
niff o x o o not implication
nsnd o x o x not second argument
xor_ o x x o exclusive or
nand o x x x not and
and_ x o o o and
nxor x o o x not exclusive or
snd x o x o second argument
iff x o x x implication (if and only if)
fst x x o o first argument
ciff x x o x converse implication
or_ x x x o or
t x x x x always true
Todo
Add type constraint that bit2 is only allowed for powers of two.
axm %core.bit2( f, nor, nciff, nfst, niff, nsnd, xor_, nand,
and_, nxor, snd, iff, fst, ciff, or_, t):
{s: Nat} → [m: Nat] → «2; Idx s» → Idx s , normalize_bit2;

%core.shr

Shift right:

For Idx s, the shift count must be smaller than the minimal bit width needed to encode the carrier. For Idx ⊤, this width is 64; otherwise it is max(1, ceil(log2(s))). Larger counts are undefined behavior.

  • shr.l divides the unsigned representative by 2^b.
  • shr.a divides the signed representative by 2^b, rounding toward -∞.
axm %core.shr(a, l): {s: Nat} → «2; Idx s» → Idx s, normalize_shr;

%core.wrap

Integer operations that may overflow. You can specify the desired behavior in the case of an overflow with the curried argument just in front of the actual argument by providing a mim::plug::core::Mode as Nat.

shl uses the same shift-count rule as %core.shr. It multiplies the unsigned representative by 2^b and then wraps modulo s. nuw and nsw check the unwrapped unsigned and signed results, respectively.

axm %core.wrap(add, sub, mul, shl): {s: Nat} → [m: Nat] → «2; Idx s» → Idx s, normalize_wrap;
lam %core.minus {s: Nat} (m: Nat) (a: Idx s): Idx s = %core.wrap.sub m (0:(Idx s), a);

%core.div

Signed and unsigned Integer division/remainder.

Warning
Division by zero is undefined behavior and a visible side effect. For this reason, these axioms expect a %mem.M.
axm %core.div(sdiv, udiv, srem, urem):
{s: Nat} → [%mem.M 0, «2; Idx s»] → [%mem.M 0, Idx s], normalize_div;

%core.icmp

Integer comparison is made of 5 disjoint relations:

  • X: first operand plus, second minus
  • Y: first operand minus, second plus
  • G: greater with same sign
  • L: less with same sign
  • E: equal

Here is the complete picture for %core.icmp.xygle x, y for 3 bit wide integers:

x y
binary 000 001 010 011 100 101 110 111
unsigned 0 1 2 3 4 5 6 7
signed 0 1 2 3 -4 -3 -2 -1
000 0 0 E L L L X X X X
001 1 1 G E L L X X X X
010 2 2 G G E L X X X X
011 3 3 G G G E X X X X
100 4 -4 Y Y Y Y E L L L
101 5 -3 Y Y Y Y G E L L
110 6 -2 Y Y Y Y G G E L
111 7 -1 Y Y Y Y G G G E

And here is the overview of all possible combinations of relations. Note the aliases you can use for the common integer comparisions front-ends typically want to use:

Subtag Alias X Y G L E Meaning
xygle f o o o o o always false
xyglE e o o o o x equal
xygLe o o o x o less (same sign)
xyglE o o o x x less or equal
xyGle o o x o o greater (same sign)
xyGlE o o x o x greater or equal
xyGLe o o x x o greater or less
xyGLE o o x x x greater or less or equal == same sign
xYgle o x o o o minus plus
xYglE o x o o x minus plus or equal
xYgLe sl o x o x o signed less
xYglE sle o x o x x signed less or equal
xYGle ug o x x o o unsigned greater
xYGlE uge o x x o x unsigned greater or equal
xYGLe o x x x o minus plus or greater or less
xYGLE o x x x x not plus minus
Xygle x o o o o plus minus
XyglE x o o o x plus minus or equal
XygLe ul x o o x o unsigned less
XyglE ule x o o x x unsigned less or equal
XyGle sg x o x o o signed greater
XyGlE sge x o x o x signed greater or equal
XyGLe x o x x o greater or less or plus minus
XyGLE x o x x x not minus plus
XYgle x x o o o different sign
XYglE x x o o x different sign or equal
XYgLe x x o x o signed or unsigned less
XYglE x x o x x signed or unsigned less or equal == not greater
XYGle x x x o o signed or unsigned greater
XYGlE x x x o x signed or unsigned greater or equal == not less
XYGLe ne x x x x o not equal
XYGLE t x x x x x always true
axm %core.icmp(xygle = f, xyglE = e, xygLe, xygLE,
xyGle, xyGlE, xyGLe, xyGLE,
xYgle, xYglE, xYgLe = sl, xYgLE = sle,
xYGle = ug, xYGlE = uge, xYGLe, xYGLE,
Xygle, XyglE, XygLe = ul, XygLE = ule,
XyGle = sg, XyGlE = sge, XyGLe, XyGLE,
XYgle, XYglE, XYgLe, XYgLE,
XYGle, XYGlE, XYGLe = ne, XYGLE = t):
{s: Nat} → «2; Idx s» → Bool , normalize_icmp;

%core.extrema

Minimum and Maximum of two Integers

  • unsigned or Signed
  • minimum or Maximum
axm %core.extrema(sm=umin, sM=umax, Sm=smin, SM=smax): {s: Nat} → «2; Idx s» → Idx s, normalize_extrema;

%core.abs

Absolute value of an int

Warning
Computing the absolute value of an Integer with the lowest possible value leads to undefined behavior, which is why this axiom expects a %mem.M
axm %core.abs: {s: Nat} → [%mem.M 0, Idx s] → [%mem.M 0, Idx s], normalize_abs;

Conversions

%core.conv

Conversion between index types - both signed and unsigned - of different sizes.

  • conv.u preserves the unsigned representative modulo the destination carrier.
  • conv.s preserves the signed representative modulo the destination carrier.
axm %core.conv(s, u): {ss: Nat} → [ds: Nat] → Idx ss → Idx ds, normalize_conv;

%core.bitcast

Bitcast to reinterpret a value as another type. Can be used for pointer / integer conversions as well as integer / nat conversions.

axm %core.bitcast: {S: *} → [D: *] → S → D, normalize_bitcast;

Other Operations

%core.trait

Yields the size or align of a type.

axm %core.trait(size, align): * → Nat, normalize_trait;

%core.pe

Steers the partial evaluator.

axm %core.pe(hlt, run): {T: *} → T → T, normalize_pe;
axm %core.pe(is_closed): {T: *} → T → Bool, normalize_pe;

%core.select

More readable shorthand to create a select/if:

lam %core.select {T: *} (cond: Bool, t: T, f: T): T = (f, t)#cond;