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

See also
mim::plug::core

Types

M

This type tracks all kinds of side effects in the given address space. The mem plugin re-exports it as mem.M.

axm M: Nat → *;

Ptr

Pointer type with pointee type T and address space a. At the moment, the address space is not really used and serves as a placeholder for future work. The mem plugin re-exports it as mem.Ptr.

axm Ptr: [*, Nat] → *;

Nat Operations

nat

Standard arithmetic operations on Nats:

  • core.nat.sub (a, b) yields 0 if a < b.
  • core.nat.div (a, b) yields 0 if b is 0.
  • core.nat.rem (a, b) yields a if b is 0. This holds both statically (literal folding) and dynamically (runtime lowering).
axm nat.(add, sub, mul, div, rem): «2; Nat» → Nat, normalize_nat;

ncmp

Nat comparison is composed 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 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 take a leading parameter m - mode - of type Nat that determines the exact desired behavior in the case of an overflow. It comes first so that currying it - core.wrap.add 0 - still yields a value polymorphic in s.

pub mod mode
anx let us = 0b00; // wrap around - both signed and unsigned
anx let uS = 0b01; // no signed wrap around
anx let Us = 0b10; // no unsigned wrap around
anx let US = 0b11; // neither signed nor unsigned wrap around
anx nsw = uS;
anx nuw = Us;
anx nsuw = US;
end

idx

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

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

bit1

These unary bitwise operations offer 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 bit1.(f, neg, id, t): [m: Nat] → {s: Nat} → Idx s → Idx s, normalize_bit1;

bit2

These binary bitwise operations offer 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
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 bit2.( f, nor, nciff, nfst, niff, nsnd, xor, nand,
and, nxor, snd, iff, fst, ciff, or, t):
[m: Nat] → {s: Nat} → «2; Idx s» → Idx s, normalize_bit2;

shr

Shift right:

For Idx s, the shift count must be smaller than the minimal bit width needed to encode the carrier: 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 shr.(a, l): {s: Nat} → «2; Idx s» → Idx s, normalize_shr;

wrap

Integer operations that may overflow. You can specify the desired behavior in the case of an overflow with the leading curried 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 wrap.(add, sub, mul, shl): [m: Nat] → {s: Nat} → «2; Idx s» → Idx s, normalize_wrap;
anx lam minus (m: Nat) {s: Nat} (a: Idx s): Idx s = wrap.sub m (idx 0 s 0, a);

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 an M.
axm div.(sdiv, udiv, srem, urem):
{s a: Nat} → [M a, «2; Idx s»] → [M a, Idx s], normalize_div;

icmp

Integer comparison is composed 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 comparisons 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 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;

extrema

Minimum and maximum of two integers:

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

abs

Absolute value of an integer.

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

Conversions

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 conv.(s, u): {ss: Nat} → [ds: Nat] → Idx ss → Idx ds, normalize_conv;

idx2nat

Yields the unsigned representative of an index as a Nat. In contrast to bitcast, this never truncates.

axm idx2nat: {s: Nat} → Idx s → Nat, normalize_idx2nat;

bitcast

Bitcast to reinterpret a value as another type. Can be used for pointer / integer conversions as well as integer / nat conversions. A value that does not fit into a target Idx s is truncated modulo s.

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

Other Operations

trait

Yields the size or align of a type.

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

pe

Steers the partial evaluator.

pub mod pe
axm hlt: {T: *} → T → T, normalize_pe;
axm run: {T: *} → T → T, normalize_pe;
axm is_closed: {T: *} → T → Bool, normalize_pe;
end

select

More readable shorthand to create a select/if:

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

Select

core.select one level up, to select between types.

anx lam Select {T: □} (cond: Bool, t f: T): T = (f, t)#cond;

Operators

Bindings for the infix operators, which are sugar for an application of the escaped name. use the module matching the domain at hand:

core.ops.s/core.ops.u offer only those operators that don't depend on the mode. Idx s has no / and %, since core.div expects an M.

pub mod ops
pub mod n
pub let `+ = nat.add;
pub let `- = nat.sub;
pub let `* = nat.mul;
pub let `/ = nat.div;
pub let `% = nat.rem;
pub let `== = ncmp.e;
pub let `!= = ncmp.ne;
pub let `< = ncmp.l;
pub let `<= = ncmp.le;
pub let `> = ncmp.g;
pub let `>= = ncmp.ge;
end
mod eq
pub let `== = icmp.e;
pub let `!= = icmp.ne;
end
mod signed
pub use eq;
pub let `>> = shr.a;
pub let `< = icmp.sl;
pub let `<= = icmp.sle;
pub let `> = icmp.sg;
pub let `>= = icmp.sge;
end
mod unsigned
pub use eq;
pub let `>> = shr.l;
pub let `< = icmp.ul;
pub let `<= = icmp.ule;
pub let `> = icmp.ug;
pub let `>= = icmp.uge;
end
pub mod s
pub use signed;
pub mod w
pub use signed;
pub let `+ = wrap.add mode.us;
pub let `- = wrap.sub mode.us;
pub let `* = wrap.mul mode.us;
pub let `<< = wrap.shl mode.us;
end
pub mod nw
pub use signed;
pub let `+ = wrap.add mode.nsw;
pub let `- = wrap.sub mode.nsw;
pub let `* = wrap.mul mode.nsw;
pub let `<< = wrap.shl mode.nsw;
end
end
pub mod u
pub use unsigned;
pub mod w
pub use unsigned;
pub let `+ = wrap.add mode.us;
pub let `- = wrap.sub mode.us;
pub let `* = wrap.mul mode.us;
pub let `<< = wrap.shl mode.us;
end
pub mod nw
pub use unsigned;
pub let `+ = wrap.add mode.nuw;
pub let `- = wrap.sub mode.nuw;
pub let `* = wrap.mul mode.nuw;
pub let `<< = wrap.shl mode.nuw;
end
end
end