The core Plugin

See also

mim::plug::core

Dependencies

plugin mem;

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;
}

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;

idx_unsafe

Creates a literal of type Idx ⊤.

axm idx_unsafe: Nat → Idx ⊤:Nat, normalize_idx_unsafe;

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 (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 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:

• arithmetic shift right
• logical 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 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 (0:(Idx s), 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 a mem.M.

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

axm abs: {s a: Nat} → [mem.M a, Idx s] → [mem.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;

bitcast

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

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;
}

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:

Module	Domain
core.ops.n	Nat
core.ops.s.w	signed Idx s, wrap around
core.ops.s.nw	signed Idx s, core.mode.nsw
core.ops.u.w	unsigned Idx s, wrap around
core.ops.u.nw	unsigned Idx s, core.mode.nuw

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 a mem.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;
    }
 
    mod eq {
        pub let `== = icmp.e;
        pub let `!= = icmp.ne;
    }
 
    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;
    }
 
    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;
    }
 
    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;
        }
 
        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;
        }
    }
 
    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;
        }
 
        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;
        }
    }
}