Rule catalog

The built-in rules: core.bwr, the local rules the engine links by default, and eqsat.bwr, the equations of the equality-saturation search. Every rule is checked (and recorded in the file’s proof ledger) and every example holds.

`core.bwr`

core.bitwise

`and_absorb_or` — rule

Absorption.

rule and_absorb_or<W>(x: W, y: W) { x & (x | y) => x }

(q | p) & p → p

`or_absorb_and` — rule

Absorption.

rule or_absorb_and<W>(x: W, y: W) { x | (x & y) => x }

(q & p) | p → p

`and_not_self` — rule

Complement.

rule and_not_self<W>(x: W) { x & ~x => 0 }

p & ~p → 0:8

`or_not_self` — rule

Complement.

rule or_not_self<W>(x: W) { x | ~x => ones }

p | ~p → 255:8

`xor_not_self` — rule

Complement.

rule xor_not_self<W>(x: W) { x ^ ~x => ones }

p ^ ~p → 255:8

`xor_and_or` — rule

The and and the or of two values differ exactly in their xor.

rule xor_and_or<W>(x: W, y: W) { (x & y) ^ (x | y) => x ^ y }

(p & q) ^ (p | q) → p ^ q

`and_mask_redundant` — rule

A mask that keeps every bit the value may have set.

rule and_mask_redundant<W>(x: W, c: const W) { x & c => x if zero_bits(x, ~c) }

(q & 15) & 0x3f → q & 15

`and_mask_disjoint` — rule

A mask that keeps none of the bits the value may have set.

rule and_mask_disjoint<W>(x: W, c: const W) { x & c => 0 if zero_bits(x, c) }

(q & 0xf0) & 15 → 0:8

`and_not_disjoint` — rule

Clearing bits the value does not have.

rule and_not_disjoint<W>(x: W, y: W) { ~x & y => y if disjoint(x, y) }

~(p & 15) & (q << 4) → q << 4

`or_known_ones` — rule

Setting bits that are already set.

rule or_known_ones<W>(x: W, c: const W) { x | c => x if one_bits(x, c) }

(q | 0x81) | 1 → q | 0x81

core.arith

`add_and_or` — identity (directed and search)

And plus or is plus.

identity add_and_or<W>(x: W, y: W) { (x & y) + (x | y) <=> x + y }

(p & q) + (p | q) → p + q

`add_xor_and` — identity (directed and search)

Xor plus twice the and is plus. (Twice is written as the shift mul_pow2 makes of it: patterns are written in normal form, or bottom-up rewriting never reaches them.)

identity add_xor_and<W>(x: W, y: W) { (x ^ y) + ((x & y) << 1) <=> x + y }

(p ^ q) + ((p & q) << 1) → p + q

`or_from_xor_and` — rule

Xor plus and is or (the two parts share no bits).

rule or_from_xor_and<W>(x: W, y: W) { (x ^ y) + (x & y) => x | y }

(p ^ q) + (p & q) → p | q

`sub_and` — rule

Removing the common bits.

rule sub_and<W>(x: W, y: W) { x - (x & y) => x & ~y }

p - (p & q) → p & ~q

`neg_not` — rule

-~x = x + 1.

rule neg_not<W>(x: W) { -(~x) => x + 1 }

-(~p) → p + 1

`not_neg` — rule

~-x = x - 1.

rule not_neg<W>(x: W) { ~(-x) => x - 1 }

~(-p) → p - 1

`neg_or_one` — rule

-(x + 1) = ~x, with the increment spelled as an or.

rule neg_or_one<W>(x: W) { -(x | 1) => ~x if zero_bits(x, 1) }

-((p << 1) | 1) → ~(p << 1)

`add_disjoint` — rule

An add without carries is an or.

rule add_disjoint<W>(x: W, y: W) { x + y => x | y if disjoint(x, y) }

(p & 0xf0) + (q & 15) → (p & 0xf0) | (q & 15)

`mul_pow2` — rule

Multiplying by a power of two is a shift.

rule mul_pow2<W>(x: W, c: const W) { x * c => x << k if is_pow2(c) let k: W = ctz(c) }

p * 8 → p << 3

`udiv_pow2` — rule

Unsigned division by a power of two is a shift.

rule udiv_pow2<W>(x: W, c: const W) { udiv(x, c) => x >>u k if is_pow2(c) let k: W = ctz(c) }

udiv(p, 16) → p >>u 4

`urem_pow2` — rule

Unsigned remainder by a power of two is a mask.

rule urem_pow2<W>(x: W, c: const W) { urem(x, c) => x & m if is_pow2(c) let m: W = c - 1 }

urem(p, 16) → p & 15

core.compare

`eq_sub_zero` — rule

A zero difference is equality.

rule eq_sub_zero<W>(a: W, b: W) { (a - b) == 0 => a == b }

p - q == 0 → p == q

`eq_xor_zero` — rule

A zero xor is equality.

rule eq_xor_zero<W>(a: W, b: W) { (a ^ b) == 0 => a == b }

(p ^ q) == 0 → p == q

`ne_xor_zero` — rule

A nonzero xor is inequality.

rule ne_xor_zero<W>(a: W, b: W) { (a ^ b) != 0 => a != b }

(p ^ q) != 0 → p != q

`slt_not_not` — rule

Complementing reverses the order (signed less-than).

rule slt_not_not<W>(x: W, y: W) { ~x <s ~y => y <s x }

~p <s ~q → q <s p

`slt_const_not` — rule

Complementing reverses the order against a constant (signed less-than).

rule slt_const_not<W>(x: W, c: const W) { c <s ~x => x <s k let k: W = ~c }

5 <s ~p → p <s 250

`slt_not_const` — rule

Complementing reverses the order against a constant (signed less-than).

rule slt_not_const<W>(x: W, c: const W) { ~x <s c => k <s x if c != 0 let k: W = ~c }

~p <s 5 → 250 <s p

`slt_not_zero` — rule

The complement is negative when the value is not (spelled as the compares pass does).

rule slt_not_zero<W>(x: W) { ~x <s 0 => 0 <=s x }

~p <s 0 → 0 <=s p

`sle_not_not` — rule

Complementing reverses the order (signed less-or-equal).

rule sle_not_not<W>(x: W, y: W) { ~x <=s ~y => y <=s x }

~p <=s ~q → q <=s p

`sle_const_not` — rule

Complementing reverses the order against a constant (signed less-or-equal).

rule sle_const_not<W>(x: W, c: const W) { c <=s ~x => x <=s k let k: W = ~c }

5 <=s ~p → p <=s 250

`sle_not_const` — rule

Complementing reverses the order against a constant (signed less-or-equal).

rule sle_not_const<W>(x: W, c: const W) { ~x <=s c => k <=s x let k: W = ~c }

~p <=s 5 → 250 <=s p

`ult_not_not` — rule

Complementing reverses the order (unsigned less-than).

rule ult_not_not<W>(x: W, y: W) { ~x <u ~y => y <u x }

~p <u ~q → q <u p

`ult_const_not` — rule

Complementing reverses the order against a constant (unsigned less-than).

rule ult_const_not<W>(x: W, c: const W) { c <u ~x => x <u k let k: W = ~c }

5 <u ~p → p <u 250

`ult_not_const` — rule

Complementing reverses the order against a constant (unsigned less-than).

rule ult_not_const<W>(x: W, c: const W) { ~x <u c => k <u x let k: W = ~c }

~p <u 5 → 250 <u p

`ule_not_not` — rule

Complementing reverses the order (unsigned less-or-equal).

rule ule_not_not<W>(x: W, y: W) { ~x <=u ~y => y <=u x }

~p <=u ~q → q <=u p

`ule_const_not` — rule

Complementing reverses the order against a constant (unsigned less-or-equal).

rule ule_const_not<W>(x: W, c: const W) { c <=u ~x => x <=u k let k: W = ~c }

5 <=u ~p → p <=u 250

`ule_not_const` — rule

Complementing reverses the order against a constant (unsigned less-or-equal).

rule ule_not_const<W>(x: W, c: const W) { ~x <=u c => k <=u x let k: W = ~c }

~p <=u 5 → 250 <=u p

`slt_or_common` — rule

Bits set in both operands, outside their masks, do not decide the order (signed less-than).

rule slt_or_common<W>(x: W, y: W, m: const W, c: const W) {
        ((x & m) | c) <s ((y & m) | c) => (x & m) <s (y & m) if (m & c) == 0
    }

((p & 0xfc) | 1) <s ((q & 0xfc) | 1) → (p & 0xfc) <s (q & 0xfc)

`sle_or_common` — rule

Bits set in both operands, outside their masks, do not decide the order (signed less-or-equal).

rule sle_or_common<W>(x: W, y: W, m: const W, c: const W) {
        ((x & m) | c) <=s ((y & m) | c) => (x & m) <=s (y & m) if (m & c) == 0
    }

((p & 0xfc) | 1) <=s ((q & 0xfc) | 1) → (p & 0xfc) <=s (q & 0xfc)

`ult_or_common` — rule

Bits set in both operands, outside their masks, do not decide the order (unsigned less-than).

rule ult_or_common<W>(x: W, y: W, m: const W, c: const W) {
        ((x & m) | c) <u ((y & m) | c) => (x & m) <u (y & m) if (m & c) == 0
    }

((p & 0xfc) | 1) <u ((q & 0xfc) | 1) → (p & 0xfc) <u (q & 0xfc)

`ule_or_common` — rule

Bits set in both operands, outside their masks, do not decide the order (unsigned less-or-equal).

rule ule_or_common<W>(x: W, y: W, m: const W, c: const W) {
        ((x & m) | c) <=u ((y & m) | c) => (x & m) <=u (y & m) if (m & c) == 0
    }

((p & 0xfc) | 1) <=u ((q & 0xfc) | 1) → (p & 0xfc) <=u (q & 0xfc)

`slt_zero_or_low` — rule

Low bits set outside the mask do not change the sign.

rule slt_zero_or_low<W>(x: W, m: const W, c: const W) {
        ((x & m) | c) <s 0 => (x & m) <s 0 if (m & c) == 0 && (c & smin_lit) == 0
    }

((p & 0xfc) | 1) <s 0 → (p & 0xfc) <s 0

`sle_zero_or_low` — rule

Low bits set outside the mask do not change the sign, and make the value nonzero.

rule sle_zero_or_low<W>(x: W, m: const W, c: const W) {
        ((x & m) | c) <=s 0 => (x & m) <s 0 if (m & c) == 0 && (c & smin_lit) == 0 && c != 0
    }

((p & 0xfc) | 1) <=s 0 → (p & 0xfc) <s 0

`zero_slt_or_low` — rule

Low bits set outside the mask do not change the sign, and make the value nonzero.

rule zero_slt_or_low<W>(x: W, m: const W, c: const W) {
        0 <s ((x & m) | c) => 0 <=s (x & m) if (m & c) == 0 && (c & smin_lit) == 0 && c != 0
    }

0 <s ((p & 0xfc) | 1) → 0 <=s (p & 0xfc)

`zero_sle_or_low` — rule

Low bits set outside the mask do not change the sign.

rule zero_sle_or_low<W>(x: W, m: const W, c: const W) {
        0 <=s ((x & m) | c) => 0 <=s (x & m) if (m & c) == 0 && (c & smin_lit) == 0
    }

0 <=s ((p & 0xfc) | 1) → 0 <=s (p & 0xfc)

`ult_one` — rule

Below one is zero.

rule ult_one<W>(x: W) { x <u 1 => x == 0 }

p <u 1 → p == 0

`eq_eq_distinct` — rule

A value cannot equal two provably different values.

rule eq_eq_distinct<W>(a: W, b: W, c: W) { (a == b) & (a == c) => false if proves(b != c) }

(p == 1) & (p == 2) → 0:1

`ult_zext` — rule

Unsigned comparison of zero-extended values is the narrow comparison.

rule ult_zext<W, U>(a: W, b: W) where W < U { zext<U>(a) <u zext<U>(b) => a <u b }

zext<16>(p) (q) → p <u q

`slt_sext` — rule

Signed comparison of sign-extended values is the narrow comparison.

rule slt_sext<W, U>(a: W, b: W) where W < U { sext<U>(a) <s sext<U>(b) => a <s b }

sext<16>(p) <s sext<16>(q) → p <s q

`eq_zext` — rule

Equality of extended values is equality.

rule eq_zext<W, U>(a: W, b: W) where W < U { zext<U>(a) == zext<U>(b) => a == b }

zext<16>(p) == zext<16>(q) → p == q

core.sign

`ne_signs` — rule

Two signs differ when their xor is negative.

rule ne_signs<W>(x: W, y: W) { (x <s 0) != (y <s 0) => (x ^ y) <s 0 }

(p <s 0) != (q <s 0) → (p ^ q) <s 0

`xor_signs` — rule

Two signs differ when their xor is negative.

rule xor_signs<W>(x: W, y: W) { (x <s 0) ^ (y <s 0) => (x ^ y) <s 0 }

(p <s 0) ^ (q <s 0) → (p ^ q) <s 0

`eq_signs` — rule

Two signs agree when their xor is not negative.

rule eq_signs<W>(x: W, y: W) { (x <s 0) == (y <s 0) => 0 <=s (x ^ y) }

(p <s 0) == (q <s 0) → 0 <=s (p ^ q)

`and_signs` — rule

Both are negative when their and is.

rule and_signs<W>(x: W, y: W) { (x <s 0) & (y <s 0) => (x & y) <s 0 }

(p <s 0) & (q <s 0) → (p & q) <s 0

`or_signs` — rule

Either is negative when their or is.

rule or_signs<W>(x: W, y: W) { (x <s 0) | (y <s 0) => (x | y) <s 0 }

(p <s 0) | (q <s 0) → (p | q) <s 0

`lshr_sign_eq_one` — rule

The sign bit shifted down is one when the value is negative.

rule lshr_sign_eq_one<W>(x: W) where 1 < W { x >>u (W - 1) == 1 => x <s 0 }

p >>u 7 == 1 → p <s 0

`lshr_sign_ne_zero` — rule

The sign bit shifted down is nonzero when the value is negative.

rule lshr_sign_ne_zero<W>(x: W) { x >>u (W - 1) != 0 => x <s 0 }

p >>u 7 != 0 → p <s 0

`xor_lshr_signs` — rule

The xor of two sign bits shifted down is the sign bit of the xor.

rule xor_lshr_signs<W>(x: W, y: W) {
        (x >>u (W - 1)) ^ (y >>u (W - 1)) => (x ^ y) >>u (W - 1)
    }

(p >>u 7) ^ (q >>u 7) → (p ^ q) >>u 7

`ne_sign_bits` — rule

Two sign bits differ when the xor’s sign bit is set.

rule ne_sign_bits<W>(x: W, y: W) {
        extract<W - 1, 1>(x) != extract<W - 1, 1>(y) => extract<W - 1, 1>(x ^ y)
    }

extract<7, 1>(p) != extract<7, 1>(q) → extract<7, 1>(p ^ q)

`xor_sign_bits` — rule

The xor of two sign bits is the sign bit of the xor.

rule xor_sign_bits<W>(x: W, y: W) {
        extract<W - 1, 1>(x) ^ extract<W - 1, 1>(y) => extract<W - 1, 1>(x ^ y)
    }

extract<7, 1>(p) ^ extract<7, 1>(q) → extract<7, 1>(p ^ q)

`slt_from_flags` — rule

SF != OF after a - b (x86 setl, AArch64 lt) is signed less-than.

rule slt_from_flags<W>(a: W, b: W) {
        ((a - b) ^ (((a - b) ^ a) & (a ^ b))) <s 0 => a <s b
    }

(p - q ^ ((p - q ^ p) & (p ^ q))) <s 0 → p <s q

`sge_from_flags` — rule

SF == OF after a - b (x86 setge, AArch64 ge) is signed greater-or-equal.

rule sge_from_flags<W>(a: W, b: W) {
        0 <=s ((a - b) ^ (((a - b) ^ a) & (a ^ b))) => b <=s a
    }

0 <=s (p - q ^ ((p - q ^ p) & (p ^ q))) → q <=s p

`slt_from_flags_const` — rule

SF != OF after a - k for a constant k (whose subtraction is built as a + -k).

rule slt_from_flags_const<W>(a: W, c: const W, k: const W) {
        ((a + c) ^ (((a + c) ^ a) & (a ^ k))) <s 0 => a <s k
        if c + k == 0
    }

(p + 0xfb ^ ((p + 0xfb ^ p) & (p ^ 5))) <s 0 → p <s 5

`sge_from_flags_const` — rule

SF == OF after a - k for a constant k.

rule sge_from_flags_const<W>(a: W, c: const W, k: const W) {
        0 <=s ((a + c) ^ (((a + c) ^ a) & (a ^ k))) => k <=s a
        if c + k == 0
    }

0 <=s (p + 0xfb ^ ((p + 0xfb ^ p) & (p ^ 5))) → 5 <=s p

`slt_from_flags_word` — rule

SF != OF as a 0 or 1 word.

rule slt_from_flags_word<W>(a: W, b: W) where 1 < W {
        ((a - b) ^ (((a - b) ^ a) & (a ^ b))) >>u (W - 1) => zext<W>(a <s b)
    }

(p - q ^ ((p - q ^ p) & (p ^ q))) >>u 7 → zext<8>(p <s q)

`slt_from_flag_bits` — rule

SF != OF as a bit.

rule slt_from_flag_bits<W>(a: W, b: W) {
        extract<W - 1, 1>((a - b) ^ (((a - b) ^ a) & (a ^ b))) => a <s b
    }

extract<7, 1>(p - q ^ ((p - q ^ p) & (p ^ q))) → p <s q

`sge_from_flag_bits` — rule

SF == OF as bits.

rule sge_from_flag_bits<W>(a: W, b: W) {
        extract<W - 1, 1>(a - b) == extract<W - 1, 1>(((a - b) ^ a) & (a ^ b)) => b <=s a
    }

extract<7, 1>(p - q) == extract<7, 1>((p - q ^ p) & (p ^ q)) → q <=s p

core.casts

`zext_trunc` — rule

Truncate, then zero-extend back: a mask.

rule zext_trunc<W, N>(x: W) where N < W { zext<W>(trunc<N>(x)) => x & lowmask(N) }

zext<8>(trunc<4>(p)) → p & 15

`sext_from_sign_word` — rule

Sign extension spelled as “value | (sign word << W)”. Needs U <= 2W to be exact.

rule sext_from_sign_word<W, U>(a: W) where W < U, U <= 2 * W {
        zext<U>(a) | (zext<U>(a >>s (W - 1)) << W) => sext<U>(a)
    }

zext<16>(p) | (zext<16>(p >>s 7) << 8) → sext<16>(p)

core.select

`select_one_zero` — rule

A condition selecting one or zero is its zero extension.

rule select_one_zero<W>(c: 1) where 1 < W { select(c, 1, 0) => zext<W>(c) }

select(p (p <u q)

`select_ones_zero` — rule

A condition selecting all ones or zero is its sign extension.

rule select_ones_zero<W>(c: 1) where 1 < W { select(c, ones, 0) => sext<W>(c) }

select(p (p <u q)

core.shift

`shl_shl` — rule

Two left shifts by constants that do not overflow the width.

rule shl_shl<W>(x: W, a: const W, b: const W) {
        (x << a) << b => x << k
        if (a <u W) && (b <u W) && (a + b <u W)
        let k: W = a + b
    }

(p << 2) << 3 → p << 5

`lshr_lshr` — rule

Two logical right shifts by constants that do not overflow the width.

rule lshr_lshr<W>(x: W, a: const W, b: const W) {
        (x >>u a) >>u b => x >>u k
        if (a <u W) && (b <u W) && (a + b <u W)
        let k: W = a + b
    }

(p >>u 2) >>u 3 → p >>u 5

`lshr_shl` — rule

Shifting right then left by the same amount clears the low bits.

rule lshr_shl<W>(x: W, c: const W) {
        (x >>u c) << c => x & m
        if c <u W
        let m: W = ones << c
    }

(p >>u 3) << 3 → p & 0xf8

`rotl_rotl` — rule

Two rotations by constants.

rule rotl_rotl<W>(x: W, a: const W, b: const W) {
        rotl(rotl(x, a), b) => rotl(x, k)
        let k: W = urem(urem(a, W) + urem(b, W), W)
    }

rotl(rotl(p, 3), 7) → rotl(p, 2)

`rotl_rotr` — rule

Rotating back by the same count, whatever it is.

rule rotl_rotr<W>(x: W, y: W) { rotl(rotr(x, y), y) => x }

rotl(rotr(p, q), q) → p

`rotr_rotl` — rule

Rotating back by the same count, whatever it is.

rule rotr_rotl<W>(x: W, y: W) { rotr(rotl(x, y), y) => x }

rotr(rotl(p, q), q) → p

core.recovery_arith

`xor_from_or_minus_and` — rule

rule xor_from_or_minus_and<W>(x: W, y: W) { (x | y) - (x & y) => x ^ y }

(p | q) - (p & q) → p ^ q

`xor_from_sum_double_and` — rule

rule xor_from_sum_double_and<W>(x: W, y: W) { (x + y) - ((x & y) << 1) => x ^ y }

(p + q) - ((p & q) << 1) → p ^ q

`or_from_sum_minus_and` — rule

rule or_from_sum_minus_and<W>(x: W, y: W) { (x + y) - (x & y) => x | y }

(p + q) - (p & q) → p | q

`and_from_sum_minus_or` — rule

rule and_from_sum_minus_or<W>(x: W, y: W) { (x + y) - (x | y) => x & y }

(p + q) - (p | q) → p & q

`and_from_or_minus_xor` — rule

rule and_from_or_minus_xor<W>(x: W, y: W) { (x | y) - (x ^ y) => x & y }

(p | q) - (p ^ q) → p & q

`xor_from_double_or_sum` — rule

rule xor_from_double_or_sum<W>(x: W, y: W) { ((x | y) << 1) - (x + y) => x ^ y }

((p | q) << 1) - (p + q) → p ^ q

`sum_from_double_or_xor` — rule

rule sum_from_double_or_xor<W>(x: W, y: W) { ((x | y) << 1) - (x ^ y) => x + y }

((p | q) << 1) - (p ^ q) → p + q

`negative_double` — rule

rule negative_double<W>(x: W) { -x - x => x * k let k: W = ones - 1 }

-p - p → p * 254

core.recovery_compare

`eq_complement` — rule

rule eq_complement<W>(x: W) { x == ~x => false }

p == ~p → 0:1

`ne_complement` — rule

rule ne_complement<W>(x: W) { x != ~x => true }

p != ~p → 1:1

`ule_add_carry` — rule

rule ule_add_carry<W>(x: W, y: W) { (x + y) <=u y => -x <=u y }

(p + q) <=u q → -p <=u q

`ugt_add_no_carry` — rule

rule ugt_add_no_carry<W>(x: W, y: W) { y <u (x + y) => y <u -x }

q <u (p + q) → q <u -p

`uge_add_no_carry` — rule

rule uge_add_no_carry<W>(x: W, y: W) { y <=u (x + y) => y <=u ~x }

q <=u (p + q) → q <=u ~p

`ule_sub_no_borrow` — rule

rule ule_sub_no_borrow<W>(x: W, y: W) { (x - y) <=u ~y => y <=u x }

(p - q) <=u ~q → q <=u p

`ugt_sub_borrow` — rule

rule ugt_sub_borrow<W>(x: W, y: W) { ~y <u (x - y) => x <u y }

~q <u (p - q) → p <u q

`ne_sub_zero` — rule

rule ne_sub_zero<W>(x: W, y: W) { (x - y) != 0 => x != y }

(p - q) != 0 → p != q

core.recovery_shift

`shl_lshr` — rule

rule shl_lshr<W>(x: W, c: const W) { (x << c) >>u c => x & m let m: W = ones >>u c }

(p << 1) >>u 1 → p & 127

`ashr_ashr` — rule

rule ashr_ashr<W>(x: W, a: const W, b: const W) {
        (x >>s a) >>s b => x >>s k
        let k: W = umin(umin(a, W - 1) + umin(b, W - 1), W - 1)
    }

(p >>s 7) >>s 7 → p >>s 7

`shl_xor_dead_constant` — rule

rule shl_xor_dead_constant<W>(x: W, c: const W, k: const W) {
        (x ^ c) << k => x << k if (c << k) == 0
    }

(p ^ 128) << 7 → p << 7

`lshr_xor_dead_constant` — rule

rule lshr_xor_dead_constant<W>(x: W, c: const W, k: const W) {
        (x ^ c) >>u k => x >>u k if (c >>u k) == 0
    }

(p ^ 1) >>u 1 → p >>u 1

`negate_sign_bit` — rule

rule negate_sign_bit<W>(x: W) { -(x >>u (W - 1)) => x >>s (W - 1) }

-(p >>u 7) → p >>s 7

`nonzero_from_sign_union` — rule

rule nonzero_from_sign_union<W>(x: W) where 1 < W {
        (x | -x) >>u (W - 1) => zext<W>(x != 0)
    }

(p | -p) >>u 7 → zext<8>(p != 0)

core.recovery_bmi2

`pdep_pext` — rule

rule pdep_pext<W>(x: W, m: W) { pdep(pext(x, m), m) => x & m }

pdep(pext(p, q), q) → p & q

`pext_pdep` — rule

rule pext_pdep<W>(x: W, m: const W) {
        pext(pdep(x, m), m) => x & k let k: W = ones >>u (W - popcnt(m))
    }

pext(pdep(p, 0x55), 0x55) → p & 15

`pdep_ones` — rule

rule pdep_ones<W>(m: W) { pdep(ones, m) => m }

pdep(255, p) → p

`pext_complement_mask` — rule

rule pext_complement_mask<W>(m: W) { pext(~m, m) => 0 }

pext(~p, p) → 0:8

`pdep_outside_mask` — rule

rule pdep_outside_mask<W>(x: W, m: W) { pdep(x, m) & ~m => 0 }

pdep(p, q) & ~q → 0:8

`pdep_inside_mask` — rule

rule pdep_inside_mask<W>(x: W, m: W) { pdep(x, m) & m => pdep(x, m) }

pdep(p, q) & q → pdep(p, q)

`pdep_pext_and` — rule

rule pdep_pext_and<W>(x: W, y: W, m: W) { pdep(pext(x, m) & pext(y, m), m) => (x & y) & m }

pdep(pext(p, r) & pext(q, r), r) → (p & q) & r

`pdep_pext_or` — rule

rule pdep_pext_or<W>(x: W, y: W, m: W) { pdep(pext(x, m) | pext(y, m), m) => (x | y) & m }

pdep(pext(p, r) | pext(q, r), r) → (p | q) & r

`pdep_pext_xor` — rule

rule pdep_pext_xor<W>(x: W, y: W, m: W) { pdep(pext(x, m) ^ pext(y, m), m) => (x ^ y) & m }

pdep(pext(p, r) ^ pext(q, r), r) → (p ^ q) & r

core.recovery_cast

`add_trunc_pair` — rule

rule add_trunc_pair<W, N>(x: W, y: W) where N < W {
        trunc<N>(x) + trunc<N>(y) => trunc<N>(x + y)
    }

trunc<4>(p) + trunc<4>(q) → trunc<4>(p + q)

`sub_trunc_pair` — rule

rule sub_trunc_pair<W, N>(x: W, y: W) where N < W {
        trunc<N>(x) - trunc<N>(y) => trunc<N>(x - y)
    }

trunc<4>(p) - trunc<4>(q) → trunc<4>(p - q)

`mul_trunc_pair` — rule

rule mul_trunc_pair<W, N>(x: W, y: W) where N < W {
        trunc<N>(x) * trunc<N>(y) => trunc<N>(x * y)
    }

trunc<4>(p) * trunc<4>(q) → trunc<4>(p * q)

core.recovery_select

`select_nonzero_self` — rule

rule select_nonzero_self<W>(x: W) { select(0 <u x, x, 0) => x }

select(0 <u p, p, 0) → p

`merge_complementary_select_or` — rule

rule merge_complementary_select_or<W>(c: 1, x: W, y: W) {
        select(c, x, 0) | select(c, 0, y) => select(c, x, y)
    }

select(p == 0, q, 0) | select(p == 0, 0, r) → select(p == 0, q, r)

`merge_complementary_select_add` — rule

rule merge_complementary_select_add<W>(c: 1, x: W, y: W) {
        select(c, x, 0) + select(c, 0, y) => select(c, x, y)
    }

select(p == 0, q, 0) + select(p == 0, 0, r) → select(p == 0, q, r)

`merge_complementary_zext_or` — rule

rule merge_complementary_zext_or<W>(c: 1, y: W) where 1 < W {
        zext<W>(c) | select(c, 0, y) => select(c, 1, y)
    }

zext<8>(p == 0) | select(p == 0, 0, r) → select(p == 0, 1:8, r)

`merge_complementary_zext_add` — rule

rule merge_complementary_zext_add<W>(c: 1, y: W) where 1 < W {
        zext<W>(c) + select(c, 0, y) => select(c, 1, y)
    }

zext<8>(p == 0) + select(p == 0, 0, r) → select(p == 0, 1:8, r)

`merge_complementary_sext_or` — rule

rule merge_complementary_sext_or<W>(c: 1, y: W) where 1 < W {
        sext<W>(c) | select(c, 0, y) => select(c, ones, y)
    }

sext<8>(p == 0) | select(p == 0, 0, r) → select(p == 0, 255:8, r)

`merge_complementary_sext_add` — rule

rule merge_complementary_sext_add<W>(c: 1, y: W) where 1 < W {
        sext<W>(c) + select(c, 0, y) => select(c, ones, y)
    }

sext<8>(p == 0) + select(p == 0, 0, r) → select(p == 0, 255:8, r)

core.recovery_canonical

`xor_sign_bit_add` — rule

rule xor_sign_bit_add<W>(x: W) { (x ^ bit(W - 1)) + bit(W - 1) => x }

(p ^ 128) + 128 → p

`ule_constant_borrow` — rule

rule ule_constant_borrow<W>(x: W, c: const W, m: const W) {
        (x + c) <=u m => k <=u x if m == c - 1 let k: W = -c
    }

p + 255 <=u 254 → 1 <=u p

`ugt_constant_borrow` — rule

rule ugt_constant_borrow<W>(x: W, c: const W, m: const W) {
        m <u (x + c) => x <u k if m == c - 1 let k: W = -c
    }

254 <u p + 255 → p <u 1

`pdep_pext_xor_constant` — rule

rule pdep_pext_xor_constant<W>(x: W, c: const W, m: const W) {
        pdep(pext(x, m) ^ c, m) => (x ^ k) & m let k: W = pdep(c, m)
    }

pdep(pext(p, 1) ^ 1, 1) → (p ^ 1) & 1

core.recovery_minmax

`smin_select_or` — rule

rule smin_select_or<W>(x: W, y: W) { select(x <=s y, x, 0) | select(y <s x, y, 0) => smin(x, y) }

select(p <=s q, p, 0) | select(q <s p, q, 0) → smin(p, q)

`smin_select_add` — rule

rule smin_select_add<W>(x: W, y: W) { select(x <=s y, x, 0) + select(y <s x, y, 0) => smin(x, y) }

select(p <=s q, p, 0) + select(q <s p, q, 0) → smin(p, q)

`smax_select_or` — rule

rule smax_select_or<W>(x: W, y: W) { select(y <=s x, x, 0) | select(x <s y, y, 0) => smax(x, y) }

select(q <=s p, p, 0) | select(p <s q, q, 0) → smax(p, q)

`smax_select_add` — rule

rule smax_select_add<W>(x: W, y: W) { select(y <=s x, x, 0) + select(x <s y, y, 0) => smax(x, y) }

select(q <=s p, p, 0) + select(p <s q, q, 0) → smax(p, q)

`umin_select_or` — rule

rule umin_select_or<W>(x: W, y: W) { select(x <=u y, x, 0) | select(y <u x, y, 0) => umin(x, y) }

select(p <=u q, p, 0) | select(q <u p, q, 0) → umin(p, q)

`umin_select_add` — rule

rule umin_select_add<W>(x: W, y: W) { select(x <=u y, x, 0) + select(y <u x, y, 0) => umin(x, y) }

select(p <=u q, p, 0) + select(q <u p, q, 0) → umin(p, q)

`umax_select_or` — rule

rule umax_select_or<W>(x: W, y: W) { select(y <=u x, x, 0) | select(x <u y, y, 0) => umax(x, y) }

select(q <=u p, p, 0) | select(p <u q, q, 0) → umax(p, q)

`umax_select_add` — rule

rule umax_select_add<W>(x: W, y: W) { select(y <=u x, x, 0) + select(x <u y, y, 0) => umax(x, y) }

select(q <=u p, p, 0) + select(p <u q, q, 0) → umax(p, q)

`umax_ones_sext_or` — rule

rule umax_ones_sext_or<W>(x: W) where 1 < W {
        sext<W>(x <u ones) | select(ones <=u x, x, 0) => ones
    }

sext<8>(p <u 255) | select(255 <=u p, p, 0) → 255:8

`umax_ones_sext_add` — rule

rule umax_ones_sext_add<W>(x: W) where 1 < W {
        sext<W>(x <u ones) + select(ones <=u x, x, 0) => ones
    }

sext<8>(p <u 255) + select(255 <=u p, p, 0) → 255:8

core.recovery_select_one

`smin_one_or` — rule

rule smin_one_or<W>(x: W) where 1 < W { zext<W>(1 <s x) | select(x <=s 1, x, 0) => smin(x, 1) }

zext<8>(1 <s p) | select(p <=s 1, p, 0) → smin(p, 1)

`smin_one_add` — rule

rule smin_one_add<W>(x: W) where 1 < W { zext<W>(1 <s x) + select(x <=s 1, x, 0) => smin(x, 1) }

zext<8>(1 <s p) + select(p <=s 1, p, 0) → smin(p, 1)

`smax_one_or` — rule

rule smax_one_or<W>(x: W) where 1 < W { zext<W>(x <s 1) | select(1 <=s x, x, 0) => smax(x, 1) }

zext<8>(p <s 1) | select(1 <=s p, p, 0) → smax(p, 1)

`smax_one_add` — rule

rule smax_one_add<W>(x: W) where 1 < W { zext<W>(x <s 1) + select(1 <=s x, x, 0) => smax(x, 1) }

zext<8>(p <s 1) + select(1 <=s p, p, 0) → smax(p, 1)

`umin_one_or` — rule

rule umin_one_or<W>(x: W) where 1 < W { zext<W>(1 <u x) | select(x <=u 1, x, 0) => umin(x, 1) }

zext<8>(1 <u p) | select(p <=u 1, p, 0) → umin(p, 1)

`umin_one_add` — rule

rule umin_one_add<W>(x: W) where 1 < W { zext<W>(1 <u x) + select(x <=u 1, x, 0) => umin(x, 1) }

zext<8>(1 <u p) + select(p <=u 1, p, 0) → umin(p, 1)

`umax_one_or` — rule

rule umax_one_or<W>(x: W) where 1 < W { zext<W>(x == 0) | select(1 <=u x, x, 0) => umax(x, 1) }

zext<8>(p == 0) | select(1 <=u p, p, 0) → umax(p, 1)

`umax_one_add` — rule

rule umax_one_add<W>(x: W) where 1 < W { zext<W>(x == 0) + select(1 <=u x, x, 0) => umax(x, 1) }

zext<8>(p == 0) + select(1 <=u p, p, 0) → umax(p, 1)

`smin_one_first_or` — rule

rule smin_one_first_or<W>(x: W) where 1 < W { zext<W>(1 <=s x) | select(x <s 1, x, 0) => smin(x, 1) }

zext<8>(1 <=s p) | select(p <s 1, p, 0) → smin(p, 1)

`smin_one_first_add` — rule

rule smin_one_first_add<W>(x: W) where 1 < W { zext<W>(1 <=s x) + select(x <s 1, x, 0) => smin(x, 1) }

zext<8>(1 <=s p) + select(p <s 1, p, 0) → smin(p, 1)

`smax_one_first_or` — rule

rule smax_one_first_or<W>(x: W) where 1 < W { zext<W>(x <=s 1) | select(1 <s x, x, 0) => smax(x, 1) }

zext<8>(p <=s 1) | select(1 <s p, p, 0) → smax(p, 1)

`smax_one_first_add` — rule

rule smax_one_first_add<W>(x: W) where 1 < W { zext<W>(x <=s 1) + select(1 <s x, x, 0) => smax(x, 1) }

zext<8>(p <=s 1) + select(1 <s p, p, 0) → smax(p, 1)

`umax_one_first_or` — rule

rule umax_one_first_or<W>(x: W) where 1 < W { zext<W>(x <=u 1) | select(1 <u x, x, 0) => select(1 <u x, x, 1) }

zext<8>(p <=u 1) | select(1 <u p, p, 0) → select(1 <u p, p, 1)

`umax_one_first_add` — rule

rule umax_one_first_add<W>(x: W) where 1 < W { zext<W>(x <=u 1) + select(1 <u x, x, 0) => select(1 <u x, x, 1) }

zext<8>(p <=u 1) + select(1 <u p, p, 0) → select(1 <u p, p, 1)

core.recovery_shuffle

`concat_low_zero` — rule

rule concat_low_zero<N, U>(x: N + U, z: const U) where N + U <= 512 {
        concat(trunc<N>(x), z) => x << U if z == 0
    }

concat(trunc<1>(p), 0:7) → p << 7

core.recovery_select_ones

`smin_ones_or` — rule

rule smin_ones_or<W>(x: W) where 1 < W { sext<W>(ones <s x) | select(x <=s ones, x, 0) => smin(x, ones) }

sext<8>(255 <s p) | select(p <=s 255, p, 0) → smin(p, 255)

`smin_ones_add` — rule

rule smin_ones_add<W>(x: W) where 1 < W { sext<W>(ones <s x) + select(x <=s ones, x, 0) => smin(x, ones) }

sext<8>(255 <s p) + select(p <=s 255, p, 0) → smin(p, 255)

`smax_ones_or` — rule

rule smax_ones_or<W>(x: W) where 1 < W { sext<W>(x <s ones) | select(ones <=s x, x, 0) => smax(x, ones) }

sext<8>(p <s 255) | select(255 <=s p, p, 0) → smax(p, 255)

`smax_ones_add` — rule

rule smax_ones_add<W>(x: W) where 1 < W { sext<W>(x <s ones) + select(ones <=s x, x, 0) => smax(x, ones) }

sext<8>(p <s 255) + select(255 <=s p, p, 0) → smax(p, 255)

`smin_ones_first_or` — rule

rule smin_ones_first_or<W>(x: W) where 1 < W { sext<W>(ones <=s x) | select(x <s ones, x, 0) => smin(x, ones) }

sext<8>(255 <=s p) | select(p <s 255, p, 0) → smin(p, 255)

`smin_ones_first_add` — rule

rule smin_ones_first_add<W>(x: W) where 1 < W { sext<W>(ones <=s x) + select(x <s ones, x, 0) => smin(x, ones) }

sext<8>(255 <=s p) + select(p <s 255, p, 0) → smin(p, 255)

`smax_ones_first_or` — rule

rule smax_ones_first_or<W>(x: W) where 1 < W { sext<W>(x <=s ones) | select(ones <s x, x, 0) => smax(x, ones) }

sext<8>(p <=s 255) | select(255 <s p, p, 0) → smax(p, 255)

`smax_ones_first_add` — rule

rule smax_ones_first_add<W>(x: W) where 1 < W { sext<W>(x <=s ones) + select(ones <s x, x, 0) => smax(x, ones) }

sext<8>(p <=s 255) + select(255 <s p, p, 0) → smax(p, 255)

`umin_ones_first_add` — rule

rule umin_ones_first_add<W>(x: W) where 1 < W { select(x <u ones, x, 0) + sext<W>(ones <=u x) => x }

select(p (255 <=u p) → p

`umin_ones_first_or` — rule

rule umin_ones_first_or<W>(x: W) where 1 < W { select(x <u ones, x, 0) | sext<W>(ones <=u x) => x }

select(p (255 <=u p) → p

core.guarded_recovery

`slt_neg_pair` — rule

rule slt_neg_pair<W>(x: W, y: W) {
        -x <s -y => y <s x if proves(x != bit(W - 1)) && proves(y != bit(W - 1))
    }

-((p & 252) | 2) <s -((q & 252) | 2) → ((q & 252) | 2) <s ((p & 252) | 2)

`sle_neg_pair` — rule

rule sle_neg_pair<W>(x: W, y: W) {
        -x <=s -y => y <=s x if proves(x != bit(W - 1)) && proves(y != bit(W - 1))
    }

-((p & 252) | 2) <=s -((q & 252) | 2) → ((q & 252) | 2) <=s ((p & 252) | 2)

`select_nonzero_value` — rule

rule select_nonzero_value<W>(x: W) { select(x != 0, x, 0) => x }

select(p != 0, p, 0) → p

`negate_boolean` — rule

rule negate_boolean(x: 1) { -x => x }

-p:1 → p:1

`increment_boolean` — rule

rule increment_boolean(x: 1) { x + 1 => ~x }

p:1 + 1:1 → ~p:1

`complementary_shift_rotate` — rule

rule complementary_shift_rotate<W>(x: W, a: const W, b: const W) {
        (x >>u a) | (x << b) => rotr(x, a)
        if (a <u W) && (b <u W) && (a + b == W)
    }

(p >>u 3) | (p << 5) → rotr(p, 3)

`xor_zext_lowmask` — rule

rule xor_zext_lowmask<W, U>(x: W) where W < U {
        zext<U>(x) ^ lowmask(W) => zext<U>(~x)
    }

zext<16>(p) ^ 255:16 → zext<16>(~p)

`xor_complement_mask` — rule

rule xor_complement_mask<W>(x: W, m: const W, n: const W) {
        (x & n) ^ m => x | m if n == ~m
    }

(p & 254) ^ 1 → p | 1

`mask_or_add_constant` — rule

rule mask_or_add_constant<W>(x: W, c: const W, m: const W, d: const W) {
        ((x | c) & m) + d => (x & kept) | k
        if (((c & m) + d) & (m & ~c)) == 0
        let kept: W = m & ~c
        let k: W = (c & m) + d
    }

((p | 3) & 15) + 255 → (p & 12) | 2

`mask_or_add_constant_carry` — rule

rule mask_or_add_constant_carry<W>(x: W, c: const W, m: const W, d: const W) {
        ((x | c) & m) + d => (x & kept) + k
        let kept: W = m & ~c
        let k: W = (c & m) + d
    }

((p | 127) & 0xf0) + 16 → (p & 128) + 128

`boolean_lowbit_mask_keep` — rule

rule boolean_lowbit_mask_keep<W>(x: W, y: W) where 1 < W {
        -(x & 1) & y => select(trunc<1>(x), y, 0)
    }

-(p & 1) & q → select(trunc<1>(p), q, 0)

`boolean_zext_mask_keep` — rule

rule boolean_zext_mask_keep<W>(x: 1, y: W) where 1 < W {
        -zext<W>(x) & y => select(x, y, 0)
    }

-zext<8>(p:1) & q → select(p:1, q, 0)

`split_mask_add` — rule

rule split_mask_add<W>(x: W, c: W, m: const W, n: const W) {
        (x & m) + ((x & n) + c) => (x & k) + c if (m & n) == 0 let k: W = m | n
    }

(p & 240) + ((p & 15) + q) → p + q

`split_mask_or_or` — rule

rule split_mask_or_or<W>(x: W, c: W, m: const W, n: const W) {
        (x & m) | ((x & n) | c) => (x & k) | c let k: W = m | n
    }

(p & 240) | ((p & 2) | 1) → (p & 242) | 1

`split_mask_sub` — rule

rule split_mask_sub<W>(x: W, c: W, m: const W, n: const W) {
        (x & m) + ((x & n) - c) => x - c if (m | n) == ones && (m & n) == 0
    }

(p & 240) + ((p & 15) - q) → p - q

`split_mask_increment` — rule

rule split_mask_increment<W>(x: W, m: const W, n: const W) {
        (x & m) - ~(x & n) => x + 1 if (m | n) == ones && (m & n) == 0
    }

(p & 240) - ~(p & 15) → p + 1

`recombine_shifted_field_or` — rule

rule recombine_shifted_field_or<W>(x: W, a: W, m: const W, k: const W) {
        (x & m) | (((x >>u k) + a) << k) => (x & keep) + (a << k)
        if (k <=u W) && (m & (ones << k)) == 0
        let keep: W = (ones << k) | m
    }

(p & 15) | (((p >>u 4) + q) << 4) → p + (q << 4)

core.guarded_recovery_canonical

`slt_neg_zero` — rule

rule slt_neg_zero<W>(x: W) { -x <s 0 => 0 <s x if proves(x != bit(W - 1)) }

-((p & 252) | 2) <s 0 → 0 <s ((p & 252) | 2)

`slt_zero_neg` — rule

rule slt_zero_neg<W>(x: W) { 0 <s -x => x <s 0 if proves(x != bit(W - 1)) }

0 <s -((p & 252) | 2) → ((p & 252) | 2) <s 0

`sle_neg_zero` — rule

rule sle_neg_zero<W>(x: W) { -x <=s 0 => 0 <=s x if proves(x != bit(W - 1)) }

-((p & 252) | 2) <=s 0 → 0 <=s ((p & 252) | 2)

`sle_zero_neg` — rule

rule sle_zero_neg<W>(x: W) { 0 <=s -x => x <=s 0 if proves(x != bit(W - 1)) }

0 <=s -((p & 252) | 2) → ((p & 252) | 2) <=s 0

`split_mask_or_add` — rule

rule split_mask_or_add<W>(x: W, c: W, m: const W, n: const W) {
        (x & m) + ((x & n) | c) => x + c
        if (m | n) == ones && (m & n) == 0 && zero_bits(c, n)
    }

(p & 240) + ((p & 15) | 128) → p + 128

core.guarded_recovery_shuffle

`recombine_extracted_field` — rule

rule recombine_extracted_field<N, K, M>(x: N + K, a: N + K) where M <= N, N + K <= 512 {
        concat(trunc<N>(zext<N + K>(extract<K, M>(x)) + a), trunc<K>(x))
        => (x & lowmask(K + M)) + (a << K)
    }

concat(trunc<4>(zext<8>(extract<4,3>(p)) + q), trunc<4>(p)) → (p & 127) + (q << 4)

`recombine_extracted_field_or` — rule

rule recombine_extracted_field_or<N, K, M>(x: N + K, a: N + K) where M <= N, N + K <= 512 {
        concat(trunc<N>(zext<N + K>(extract<K, M>(x)) | a), trunc<K>(x))
        => (x & lowmask(K + M)) | (a << K)
    }

concat(trunc<4>(zext<8>(extract<4,3>(p)) | q), trunc<4>(p)) → (p & 127) | (q << 4)

core.guarded_recovery_layout

`shifted_masked_add` — rule

rule shifted_masked_add<W>(x: W, a: W, s: const W, k: const W) {
        (((x >>u k) & s) + a) << k => (x & keep) + (a << k)
        let keep: W = s << k
    }

(((p >>u 4) & 8) + q) << 4 → (p & 128) + (q << 4)

`shifted_add_constant` — rule

rule shifted_add_constant<W>(x: W, c: const W, k: const W) {
        ((x >>u k) + c) << k => (x & keep) + d
        let keep: W = ones << k
        let d: W = c << k
    }

((p >>u 4) + 3) << 4 → (p & 240) + 48

`shifted_or_constant` — rule

rule shifted_or_constant<W>(x: W, c: const W, k: const W) {
        ((x >>u k) | c) << k => (x & keep) | d
        let keep: W = ones << k
        let d: W = c << k
    }

((p >>u 4) | 3) << 4 → (p & 240) | 48

`recombine_low_constant` — rule

rule recombine_low_constant<W>(x: W, a: W, c: const W, k: const W) {
        (((x >>u k) + a) << k) | c => (x | c) + (a << k)
        if (k <=u W) && c == ones >>u (W - k)
    }

(((p >>u 4) + q) << 4) | 15 → (p | 15) + (q << 4)

`split_or_masked_sum` — rule

rule split_or_masked_sum<W>(x: W, c: W, m: const W, n: const W) {
        (x & m) | ((x & n) + c) => (x & keep) + c
        if (n & prefix) == 0 && zero_bits(c, prefix)
        let prefix: W = ones >>u clz(m)
        let keep: W = m | n
    }

(p & 14) | ((p & 240) + (q << 4)) → (p & 254) + (q << 4)

`add_constant_to_concat` — rule

rule add_constant_to_concat<H, L>(x: H + L, c: const L, d: const H + L) where H + L <= 512 {
        concat(extract<L,H>(x), c) + d => (x & ~lowmask(L)) + k
        let k: H + L = zext<H + L>(c) + d
    }

concat(extract<7,1>(p), 112:7) + 16 → (p & 128) + 128

`or_constant_to_concat` — rule

rule or_constant_to_concat<H, L>(x: H + L, c: const L, d: const H + L) where H + L <= 512 {
        concat(extract<L,H>(x), c) | d => (x & ~lowmask(L)) | k
        let k: H + L = zext<H + L>(c) | d
    }

concat(extract<7,1>(p), 112:7) | 3 → (p & 128) | 115

core.guarded_recovery_mba_normalized

`xor_from_distributed_double_or` — rule

rule xor_from_distributed_double_or<W>(x: W, a: const W, c: const W) {
        ((x | a) << 1) - (x + c) => x ^ c if (a << 1) == (c << 1)
    }

((p | 1) << 1) - (p + 129) → p ^ 129

`sum_from_distributed_double_or` — rule

rule sum_from_distributed_double_or<W>(x: W, a: const W, c: const W) {
        ((x | a) << 1) - (x ^ c) => x + c if (a << 1) == (c << 1)
    }

((p | 1) << 1) - (p ^ 129) → p + 129

`sum_from_vanishing_double_mask` — rule

rule sum_from_vanishing_double_mask<W>(x: W, c: const W) {
        (x << 1) - (x ^ c) => x + c if (c << 1) == 0
    }

(p << 1) - (p ^ 128) → p + 128

core.guarded_recovery_concat

`add_aligned_to_concat` — rule

rule add_aligned_to_concat<H, L>(a: H + L, x: H + L, c: const L) where H + L <= 512 {
        (a << L) + concat(extract<L,H>(x), c)
        => concat(trunc<H>(a) + extract<L,H>(x), c)
    }

(q << 4) + concat(extract<4,4>(p), 15:4) → concat(trunc<4>(q) + extract<4,4>(p), 15:4)

core.shift_canonical

`shl_mask_dead` — rule

A mask that keeps every bit the shift keeps.

rule shl_mask_dead<W>(x: W, c: const W, k: const W) {
        (x & c) << k => x << k if (c | ~(ones >>u k)) == ones
    }

(p & 63) << 2 → p << 2

`and_shl_const` — rule

rule and_shl_const<W>(x: W, k: const W, m: const W) {
        (x << k) & m => (x & c) << k if one_use(x << k) let c: W = m >>u k
    }

(p << 2) & 60 → (p & 15) << 2

`and_double_const` — rule

rule and_double_const<W>(x: W, m: const W) {
        (x + x) & m => (x & c) << 1 if one_use(x + x) let c: W = m >>u 1
    }

(p + p) & 30 → (p & 15) << 1

`or_shl_const` — rule

An or or xor moves too when it sets no bit the shift clears.

rule or_shl_const<W>(x: W, k: const W, m: const W) {
        (x << k) | m => (x | c) << k if (m & ~(ones << k)) == 0 && one_use(x << k) let c: W = m >>u k
    }

(p << 2) | 12 → (p | 3) << 2

`xor_shl_const` — rule

rule xor_shl_const<W>(x: W, k: const W, m: const W) {
        (x << k) ^ m => (x ^ c) << k if (m & ~(ones << k)) == 0 && one_use(x << k) let c: W = m >>u k
    }

(p << 2) ^ 12 → (p ^ 3) << 2

`or_double_const` — rule

rule or_double_const<W>(x: W, m: const W) {
        (x + x) | m => (x | c) << 1 if (m & 1) == 0 && one_use(x + x) let c: W = m >>u 1
    }

(p + p) | 6 → (p | 3) << 1

`xor_double_const` — rule

rule xor_double_const<W>(x: W, m: const W) {
        (x + x) ^ m => (x ^ c) << 1 if (m & 1) == 0 && one_use(x + x) let c: W = m >>u 1
    }

(p + p) ^ 6 → (p ^ 3) << 1

core.factor

`shl_and` — rule

A left shift distributes over &, so the shift of the conjunction is one shift.

rule shl_and<W>(x: W, y: W, s: W) { (x << s) & (y << s) => (x & y) << s }

(p << 3) & (q << 3) → (p & q) << 3

`shl_or` — rule

Likewise over |.

rule shl_or<W>(x: W, y: W, s: W) { (x << s) | (y << s) => (x | y) << s }

(p << 3) | (q << 3) → (p | q) << 3

`shl_xor` — rule

Likewise over ^.

rule shl_xor<W>(x: W, y: W, s: W) { (x << s) ^ (y << s) => (x ^ y) << s }

(p << 3) ^ (q << 3) → (p ^ q) << 3

`shl_add` — rule

A left shift multiplies by a power of two (or by 0), which distributes over +.

rule shl_add<W>(x: W, y: W, s: W) { (x << s) + (y << s) => (x + y) << s }

(p << 3) + (q << 3) → (p + q) << 3

`shl_sub` — rule

And over -.

rule shl_sub<W>(x: W, y: W, s: W) { (x << s) - (y << s) => (x - y) << s }

(p << 3) - (q << 3) → (p - q) << 3

`lshr_and` — rule

A logical right shift moves every bit alike, so it distributes over &.

rule lshr_and<W>(x: W, y: W, s: W) { (x >>u s) & (y >>u s) => (x & y) >>u s }

(p >>u 3) & (q >>u 3) → (p & q) >>u 3

`lshr_or` — rule

Likewise over |.

rule lshr_or<W>(x: W, y: W, s: W) { (x >>u s) | (y >>u s) => (x | y) >>u s }

(p >>u 3) | (q >>u 3) → (p | q) >>u 3

`lshr_xor` — rule

Likewise over ^.

rule lshr_xor<W>(x: W, y: W, s: W) { (x >>u s) ^ (y >>u s) => (x ^ y) >>u s }

(p >>u 3) ^ (q >>u 3) → (p ^ q) >>u 3

`ashr_and` — rule

An arithmetic right shift copies the sign bit, a bit like the others, so it distributes over &.

rule ashr_and<W>(x: W, y: W, s: W) { (x >>s s) & (y >>s s) => (x & y) >>s s }

(p >>s 3) & (q >>s 3) → (p & q) >>s 3

`ashr_or` — rule

Likewise over |.

rule ashr_or<W>(x: W, y: W, s: W) { (x >>s s) | (y >>s s) => (x | y) >>s s }

(p >>s 3) | (q >>s 3) → (p | q) >>s 3

`ashr_xor` — rule

Likewise over ^.

rule ashr_xor<W>(x: W, y: W, s: W) { (x >>s s) ^ (y >>s s) => (x ^ y) >>s s }

(p >>s 3) ^ (q >>s 3) → (p ^ q) >>s 3

`not_ashr_not` — rule

An arithmetic right shift commutes with complement.

rule not_ashr_not<W>(x: W, s: W) { ~(~x >>s s) => x >>s s }

~(~p >>s 3) → p >>s 3

`rotl_and` — rule

A rotation moves every bit alike, so it distributes over &.

rule rotl_and<W>(x: W, y: W, s: W) { rotl(x, s) & rotl(y, s) => rotl(x & y, s) }

rotl(p, 3) & rotl(q, 3) → rotl(p & q, 3)

`rotl_or` — rule

Likewise over |.

rule rotl_or<W>(x: W, y: W, s: W) { rotl(x, s) | rotl(y, s) => rotl(x | y, s) }

rotl(p, 3) | rotl(q, 3) → rotl(p | q, 3)

`rotl_xor` — rule

Likewise over ^.

rule rotl_xor<W>(x: W, y: W, s: W) { rotl(x, s) ^ rotl(y, s) => rotl(x ^ y, s) }

rotl(p, 3) ^ rotl(q, 3) → rotl(p ^ q, 3)

`not_rotl_not` — rule

A rotation commutes with complement.

rule not_rotl_not<W>(x: W, s: W) { ~rotl(~x, s) => rotl(x, s) }

~rotl(~p, 3) → rotl(p, 3)

`zext_and` — rule

Zero extension distributes over &.

rule zext_and<W, U>(x: W, y: W) where W < U { zext<U>(x) & zext<U>(y) => zext<U>(x & y) }

zext<16>(p) & zext<16>(q) → zext<16>(p & q)

`zext_or` — rule

Likewise over |.

rule zext_or<W, U>(x: W, y: W) where W < U { zext<U>(x) | zext<U>(y) => zext<U>(x | y) }

zext<16>(p) | zext<16>(q) → zext<16>(p | q)

`zext_xor` — rule

Likewise over ^.

rule zext_xor<W, U>(x: W, y: W) where W < U { zext<U>(x) ^ zext<U>(y) => zext<U>(x ^ y) }

zext<16>(p) ^ zext<16>(q) → zext<16>(p ^ q)

`sext_and` — rule

Sign extension copies the top bit, a bit like the others: it distributes over &.

rule sext_and<W, U>(x: W, y: W) where W < U { sext<U>(x) & sext<U>(y) => sext<U>(x & y) }

sext<16>(p) & sext<16>(q) → sext<16>(p & q)

`sext_or` — rule

Likewise over |.

rule sext_or<W, U>(x: W, y: W) where W < U { sext<U>(x) | sext<U>(y) => sext<U>(x | y) }

sext<16>(p) | sext<16>(q) → sext<16>(p | q)

`sext_xor` — rule

Likewise over ^.

rule sext_xor<W, U>(x: W, y: W) where W < U { sext<U>(x) ^ sext<U>(y) => sext<U>(x ^ y) }

sext<16>(p) ^ sext<16>(q) → sext<16>(p ^ q)

`extract_and` — rule

A slice of each operand of & is the slice of the conjunction.

rule extract_and<W, N, L>(x: W, y: W) where N + L <= W, N < W {
        extract<L, N>(x) & extract<L, N>(y) => extract<L, N>(x & y)
    }

extract<4, 4>(p) & extract<4, 4>(q) → extract<4, 4>(p & q)

`extract_or` — rule

Likewise for |.

rule extract_or<W, N, L>(x: W, y: W) where N + L <= W, N < W {
        extract<L, N>(x) | extract<L, N>(y) => extract<L, N>(x | y)
    }

extract<4, 4>(p) | extract<4, 4>(q) → extract<4, 4>(p | q)

`extract_xor` — rule

Likewise for ^.

rule extract_xor<W, N, L>(x: W, y: W) where N + L <= W, N < W {
        extract<L, N>(x) ^ extract<L, N>(y) => extract<L, N>(x ^ y)
    }

extract<4, 4>(p) ^ extract<4, 4>(q) → extract<4, 4>(p ^ q)

`trunc_and` — rule

The low bits of each operand of & are the low bits of the conjunction.

rule trunc_and<W, N>(x: W, y: W) where N < W { trunc<N>(x) & trunc<N>(y) => trunc<N>(x & y) }

trunc<4>(p) & trunc<4>(q) → trunc<4>(p & q)

`trunc_or` — rule

Likewise for |.

rule trunc_or<W, N>(x: W, y: W) where N < W { trunc<N>(x) | trunc<N>(y) => trunc<N>(x | y) }

trunc<4>(p) | trunc<4>(q) → trunc<4>(p | q)

`trunc_xor` — rule

Likewise for ^.

rule trunc_xor<W, N>(x: W, y: W) where N < W { trunc<N>(x) ^ trunc<N>(y) => trunc<N>(x ^ y) }

trunc<4>(p) ^ trunc<4>(q) → trunc<4>(p ^ q)

core.select_idioms

`select_add` — rule

Both arms add the same term.

rule select_add<W>(c: 1, x: W, y: W, z: W) { select(c, x + z, y + z) => select(c, x, y) + z }

select(p <u q, p + r, q + r) → select(p <u q, p, q) + r

`select_xor` — rule

Both arms xor the same term.

rule select_xor<W>(c: 1, x: W, y: W, z: W) { select(c, x ^ z, y ^ z) => select(c, x, y) ^ z }

select(p <u q, p ^ r, q ^ r) → select(p <u q, p, q) ^ r

`select_swapped_add` — rule

Swapped arms under one condition, combined commutatively: the minimum plus the maximum is the sum.

rule select_swapped_add<W>(c: 1, x: W, y: W) { select(c, x, y) + select(c, y, x) => x + y }

select(p <u q, p, q) + select(p <u q, q, p) → p + q

`select_swapped_mul` — rule

Likewise for *.

rule select_swapped_mul<W>(c: 1, x: W, y: W) { select(c, x, y) * select(c, y, x) => x * y }

select(p <u q, p, q) * select(p <u q, q, p) → p * q

`select_swapped_and` — rule

Likewise for &.

rule select_swapped_and<W>(c: 1, x: W, y: W) { select(c, x, y) & select(c, y, x) => x & y }

select(p <u q, p, q) & select(p <u q, q, p) → p & q

`select_swapped_or` — rule

Likewise for |.

rule select_swapped_or<W>(c: 1, x: W, y: W) { select(c, x, y) | select(c, y, x) => x | y }

select(p <u q, p, q) | select(p <u q, q, p) → p | q

`select_swapped_xor` — rule

Likewise for ^.

rule select_swapped_xor<W>(c: 1, x: W, y: W) { select(c, x, y) ^ select(c, y, x) => x ^ y }

select(p <u q, p, q) ^ select(p <u q, q, p) → p ^ q

`select_not` — rule

Both arms complement.

rule select_not<W>(c: 1, x: W, y: W) { select(c, ~x, ~y) => ~select(c, x, y) }

select(p <u q, ~p, ~q) → ~select(p <u q, p, q)

`select_then_same` — rule

The same condition again in the chosen arm.

rule select_then_same<W>(c: 1, x: W, y: W, z: W) { select(c, select(c, x, y), z) => select(c, x, z) }

select(p <u q, select(p <u q, p, q), r) → select(p <u q, p, r)

`select_else_same` — rule

The same condition again in the other arm.

rule select_else_same<W>(c: 1, x: W, y: W, z: W) { select(c, x, select(c, y, z)) => select(c, x, z) }

select(p <u q, r, select(p <u q, p, q)) → select(p <u q, r, q)

`select_eq_then` — rule

Choosing x when it equals y, else y: always y (== is commutative, so this is also select(y == x, x, y)).

rule select_eq_then<W>(x: W, y: W) { select(x == y, x, y) => y }

select(p == q, p, q) → q
select(p == q, q, p) → p

`select_eq_difference` — rule

When x == y, x - y is 0.

rule select_eq_difference<W>(x: W, y: W) { select(x == y, x - y, 0) => 0 }

select(p == q, p - q, 0) → 0

`select_eq_offset` — rule

When x == c, x + d is c + d.

rule select_eq_offset<W>(x: W, c: const W, d: const W, e: const W) {
        select(x == c, x + d, e) => e if e == c + d
    }

select(p == 5, p + 1, 6) → 6

`select_zero_sum` — rule

When x == 0, x + y is y.

rule select_zero_sum<W>(x: W, y: W) { select(x == 0, x + y, y) => y }

select(p == 0, p + q, q) → q

`select_by_mask` — rule

Choosing by a mask: m all ones takes x, all zeros y.

rule select_by_mask<W>(c: 1, x: W, y: W) where 1 < W {
        (x & sext<W>(c)) | (y & ~sext<W>(c)) => select(c, x, y)
    }

(p & sext<8>(r:1)) | (q & ~sext<8>(r:1)) → select(r:1, p, q)

`select_by_xor_mask` — rule

Choosing by a mask with xor: y ^ ((x ^ y) & m).

rule select_by_xor_mask<W>(c: 1, x: W, y: W) where 1 < W {
        ((x ^ y) & sext<W>(c)) ^ y => select(c, x, y)
    }

q ^ ((p ^ q) & sext<8>(r:1)) → select(r:1, p, q)

`select_xor_zero` — rule

The xor-mask choice once the mask became a select.

rule select_xor_zero<W>(c: 1, x: W, y: W) { select(c, x ^ y, 0) ^ y => select(c, x, y) }

select(r:1, p ^ q, 0) ^ q → select(r:1, p, q)

`mask_by_decremented_bit` — rule

zext(c) - 1 is all ones when c is false and zero when it is true: a mask. (With the rules that make x & -zext(c) a select and merge complementary selects, the branchless choice (x & -zext(c)) | (y & (zext(c) - 1)) becomes select(c, x, y).)

rule mask_by_decremented_bit<W>(c: 1, y: W) where 1 < W {
        (zext<W>(c) + ones) & y => select(c, 0, y)
    }

(zext<8>(r:1) - 1) & q → select(r:1, 0, q)

core.division

`urem_self` — rule

x divided by itself leaves no remainder (and x mod 0 is x, which is 0 then too).

rule urem_self<W>(x: W) { urem(x, x) => 0 }

urem(p, p) → 0

`srem_self` — rule

Likewise signed.

rule srem_self<W>(x: W) { srem(x, x) => 0 }

srem(p, p) → 0

`urem_urem` — rule

A remainder is already reduced.

rule urem_urem<W>(x: W, y: W) { urem(urem(x, y), y) => urem(x, y) }

urem(urem(p, q), q) → urem(p, q)

`udiv_identity` — rule

Division identity: quotient times divisor plus remainder (a zero divisor included: its quotient is all ones, times 0, and its remainder is x).

rule udiv_identity<W>(x: W, y: W) { udiv(x, y) * y + urem(x, y) => x }

udiv(p, q) * q + urem(p, q) → p

`sdiv_identity` — rule

Likewise signed (for 0: a quotient of ±1 times 0, and the remainder x).

rule sdiv_identity<W>(x: W, y: W) { sdiv(x, y) * y + srem(x, y) => x }

sdiv(p, q) * q + srem(p, q) → p

`sdiv_pow2_identity` — rule

The same by a power of two, whose product mul_pow2 makes a shift.

rule sdiv_pow2_identity<W>(x: W, c: const W, k: const W) {
        (sdiv(x, c) << k) + srem(x, c) => x if is_pow2(c) && k == ctz(c)
    }

(sdiv(p, 8) << 3) + srem(p, 8) → p

`sdiv_nonnegative_pow2` — rule

Signed division of a value the facts show nonnegative by a positive power of two is a logical right shift.

rule sdiv_nonnegative_pow2<W>(x: W, c: const W) {
        sdiv(x, c) => x >>u k if is_pow2(c) && 0 <s c && proves(0 <=s x) let k: W = ctz(c)
    }

sdiv(p >>u 1, 8) → p >>u 1 >>u 3

core.sign_tests

`zext_negative` — rule

The sign bit of x as a word: x >>u (W - 1).

rule zext_negative<W>(x: W) where 1 < W { zext<W>(x <s 0) => x >>u (W - 1) }

zext<8>(p <s 0) → p >>u 7

`sext_negative` — rule

The sign mask of x: x >>s (W - 1).

rule sext_negative<W>(x: W) where 1 < W { sext<W>(x <s 0) => x >>s (W - 1) }

sext<8>(p <s 0) → p >>s 7

`sign_bit_clear` — rule

The sign bit is clear: x is nonnegative.

rule sign_bit_clear<W>(x: W) where 1 < W { (x >>u (W - 1)) == 0 => 0 <=s x }

(p >>u 7) == 0 → 0 <=s p

`sign_mask_zero` — rule

The sign mask is 0: x is nonnegative.

rule sign_mask_zero<W>(x: W) where 1 < W { (x >>s (W - 1)) == 0 => 0 <=s x }

(p >>s 7) == 0 → 0 <=s p

`sign_mask_ones` — rule

The sign mask is all ones: x is negative.

rule sign_mask_ones<W>(x: W) where 1 < W { (x >>s (W - 1)) == ones => x <s 0 }

(p >>s 7) == 0xff → p <s 0

`sign_by_mask` — rule

The sign bit tested through a mask.

rule sign_by_mask<W>(x: W) { (x & smin_lit) != 0 => x <s 0 }

(p & 0x80) != 0 → p <s 0

`sign_clear_by_mask` — rule

The sign bit clear, tested through a mask.

rule sign_clear_by_mask<W>(x: W) { (x & smin_lit) == 0 => 0 <=s x }

(p & 0x80) == 0 → 0 <=s p

`sign_mask_and_bit` — rule

The sign mask’s low bit is the sign bit.

rule sign_mask_and_bit<W>(x: W) where 1 < W { (x >>s (W - 1)) & (x >>u (W - 1)) => x >>u (W - 1) }

(p >>s 7) & (p >>u 7) → p >>u 7

`neg_sign_mask` — rule

The negated sign mask is the sign bit.

rule neg_sign_mask<W>(x: W) where 1 < W { -(x >>s (W - 1)) => x >>u (W - 1) }

-(p >>s 7) → p >>u 7

`ult_sign_flipped` — rule

Flipping both sign bits turns an unsigned comparison into a signed one.

rule ult_sign_flipped<W>(x: W, y: W) { (x ^ smin_lit) <u (y ^ smin_lit) => x <s y }

(p ^ 0x80) <u (q ^ 0x80) → p <s q

`slt_sign_flipped` — rule

And a signed one into an unsigned one.

rule slt_sign_flipped<W>(x: W, y: W) { (x ^ smin_lit) <s (y ^ smin_lit) => x <u y }

(p ^ 0x80) <s (q ^ 0x80) → p <u q

`ult_offset_by_smin` — rule

Adding the sign bit flips it (the builder’s form of x + smin).

rule ult_offset_by_smin<W>(x: W, y: W) { (x + smin_lit) <u (y + smin_lit) => x <s y }

(p + 0x80) <u (q + 0x80) → p <s q

`slt_offset_by_smin` — rule

Likewise signed.

rule slt_offset_by_smin<W>(x: W, y: W) { (x + smin_lit) <s (y + smin_lit) => x <u y }

(p + 0x80) <s (q + 0x80) → p <u q

`slt_zext` — rule

Zero-extended values are nonnegative, so their signed order is the unsigned one.

rule slt_zext<W, U>(x: W, y: W) where W < U { zext<U>(x) <s zext<U>(y) => x <u y }

zext<16>(p) <s zext<16>(q) → p <u q

core.bounds

`and_at_most` — rule

A conjunction is at most each operand (so is x & -x, its lowest set bit).

rule and_at_most<W>(x: W, y: W) { (x & y) <=u x => true }

(p & q) <=u p → true
(p & -p) <=u p → true

`and_not_above` — rule

No operand is below its conjunction with anything.

rule and_not_above<W>(x: W, y: W) { x <u (x & y) => false }

p <u (p & q) → false

`or_at_least` — rule

A disjunction is at least each operand.

rule or_at_least<W>(x: W, y: W) { x <=u (x | y) => true }

p <=u (p | q) → true

`or_not_below` — rule

No disjunction is below one of its operands.

rule or_not_below<W>(x: W, y: W) { (x | y) <u x => false }

(p | q) <u p → false

`and_at_most_or` — rule

A conjunction is at most the disjunction.

rule and_at_most_or<W>(x: W, y: W) { (x & y) <=u (x | y) => true }

(p & q) <=u (p | q) → true

`lshr_at_most` — rule

A logical right shift does not grow a value.

rule lshr_at_most<W>(x: W, s: W) { (x >>u s) <=u x => true }

(p >>u 1) <=u p → true

`udiv_at_most` — rule

Nor does unsigned division (by 0 it is all ones… except that x / 0 is all ones, so only by a divisor the facts show nonzero).

rule udiv_at_most<W>(x: W, y: W) { udiv(x, y) <=u x => true if proves(y != 0) }

udiv(p, q | 1) <=u p → true

`urem_at_most` — rule

A remainder is at most the dividend (by 0 it is the dividend).

rule urem_at_most<W>(x: W, y: W) { urem(x, y) <=u x => true }

urem(p, q) <=u p → true

`urem_below_divisor` — rule

A remainder is below its divisor, or (for 0) at most y - 1, all ones.

rule urem_below_divisor<W>(x: W, y: W) { urem(x, y) <=u (y + ones) => true }

urem(p, q) <=u q - 1 → true

`decrement_below` — rule

x - 1 < x except at 0, where it wraps.

rule decrement_below<W>(x: W) { (x + ones) <u x => x != 0 }

p - 1 <u p → p != 0

`increment_wraps` — rule

x + 1 < x only at all ones, where it wraps.

rule increment_wraps<W>(x: W) { (x + 1) <u x => x == ones }

p + 1 <u p → p == 0xff

`signed_increment_wraps` — rule

x + 1 <s x only at the signed maximum.

rule signed_increment_wraps<W>(x: W) { (x + 1) <s x => x == smax_lit }

p + 1 <s p → p == 0x7f

`signed_increment_grows` — rule

x <s x + 1 except at the signed maximum.

rule signed_increment_grows<W>(x: W) { x <s (x + 1) => x != smax_lit }

p <s p + 1 → p != 0x7f

`longer_shift_smaller` — rule

The larger of two shifts right by constants leaves the smaller value.

rule longer_shift_smaller<W>(x: W, a: const W, b: const W) {
        (x >>u a) <=u (x >>u b) => true if b <=u a
    }

(p >>u 3) <=u (p >>u 1) → true

`halves_sum_no_overflow` — rule

Halves of two values never overflow their sum.

rule halves_sum_no_overflow<W>(x: W, y: W) where 1 < W {
        ((x >>u 1) + (y >>u 1)) <u (x >>u 1) => false
    }

((p >>u 1) + (q >>u 1)) >u 1) → false

core.concat

`concat_and_low` — rule

& of concatenations with one low part: the low part stays.

rule concat_and_low<W, V>(x: W, y: V, z: W) { concat(x, y) & concat(z, y) => concat(x & z, y) }

concat(p, r:4) & concat(q, r:4) → concat(p & q, r:4)

`concat_and_high` — rule

Likewise with one high part.

rule concat_and_high<W, V>(x: W, y: V, z: V) { concat(x, y) & concat(x, z) => concat(x, y & z) }

concat(r:4, p) & concat(r:4, q) → concat(r:4, p & q)

`concat_or_low` — rule

| of concatenations with one low part.

rule concat_or_low<W, V>(x: W, y: V, z: W) { concat(x, y) | concat(z, y) => concat(x | z, y) }

concat(p, r:4) | concat(q, r:4) → concat(p | q, r:4)

`concat_or_high` — rule

Likewise with one high part.

rule concat_or_high<W, V>(x: W, y: V, z: V) { concat(x, y) | concat(x, z) => concat(x, y | z) }

concat(r:4, p) | concat(r:4, q) → concat(r:4, p | q)

`concat_xor_low` — rule

^ of concatenations with one low part: that part cancels.

rule concat_xor_low<W, V>(x: W, y: V, z: W) { concat(x, y) ^ concat(z, y) => concat(x ^ z, zero) }

concat(p, r:4) ^ concat(q, r:4) → concat(p ^ q, 0:4)

`concat_assoc` — rule

Concatenation associates; right nesting is the canonical one.

rule concat_assoc<A, B, C>(x: A, y: B, z: C) { concat(concat(x, y), z) => concat(x, concat(y, z)) }

concat(concat(p, q), r) → concat(p, concat(q, r))

`concat_ashr` — rule

An arithmetic shift right by the low part’s width sign-extends the high part.

rule concat_ashr<W, V>(x: W, y: V) { concat(x, y) >>s V => sext<W + V>(x) }

concat(p, q:4) >>s 4 → sext<12>(p)

`concat_lshr` — rule

A logical shift right by the low part’s width zero-extends the high part.

rule concat_lshr<W, V>(x: W, y: V) { concat(x, y) >>u V => zext<W + V>(x) }

concat(p, q:4) >>u 4 → zext<12>(p)

`concat_sign_word` — rule

A value above a sign-extended copy of its top bit is its sign extension.

rule concat_sign_word<W>(x: W) where 1 < W {
        concat(sext<W>(extract<W - 1, 1>(x)), x) => sext<W + W>(x)
    }

concat(sext<8>(extract<7, 1>(p)), p) → sext<16>(p)

`concat_or_zext` — rule

A zero low part with a zero-extended value in it is their concatenation (a sum of the two has no carries, so it is this | too).

rule concat_or_zext<W, V>(x: W, y: V) { concat(x, 0) | zext<W + V>(y) => concat(x, y) }

concat(p, 0:4) | zext<12>(q:4) → concat(p, q:4)

core.single_bit

`pow2_and_below` — rule

A power of two shares no bit with the value one below it (and 1 << s past the width is 0).

rule pow2_and_below<W>(s: W) { (one << s) & ((one << s) + ones) => 0 }

(1 << (q & 7)) & ((1 << (q & 7)) - 1) → 0

core.float

`div_pow2` — rule

Dividing by a power of two is multiplying by its reciprocal when that is a normal number: the two are the same real number, rounded once in the same mode, so every result (a NaN, an infinity, the sign of a zero, an underflow) is the same. Not by ½: the builder already writes x / ½ (and x · 2) as x + x.

rule div_pow2<E, S>(x: E + S, c: const E + S, r: rm) {
        fp.div.r<E, S>(x, c) => fp.mul.r<E, S>(x, k)
        if (c & lowmask(S - 1)) == 0 && (c & smax_lit) != 0 && (c & smax_lit) <u fp.inf<E, S>
            && m >=u fp.min_normal<E, S> && m != fp.two<E, S>
        let m: E + S = fp.one<E, S> + fp.one<E, S> - (c & smax_lit)
        let k: E + S = (c & smin_lit) | m
    }

fp.div.rne.f32(p:32, 0x40800000) → fp.mul.rne.f32(p:32, 0x3e800000)

`mul_one` — rule

x · 1 is x for every number.

rule mul_one<E, S>(x: E + S, r: rm) {
        fp.mul.r<E, S>(x, fp.one<E, S>) => x if fp.not_nan<E, S>(x)
    }

fp.mul.rne.f64(fp.from_sbv.rne.f64(i:32), 0x3ff0000000000000) → fp.from_sbv.rne.f64(i:32)

`mul_neg_one` — rule

x · −1 is −x for every number.

rule mul_neg_one<E, S>(x: E + S, r: rm) {
        fp.mul.r<E, S>(x, fp.none<E, S>) => fp.neg<E, S>(x) if fp.not_nan<E, S>(x)
    }

fp.mul.rtz.f64(fp.from_sbv.rne.f64(i:32), 0xbff0000000000000) → fp.from_sbv.rne.f64(i:32) ^ 0x8000000000000000

`add_zero` — rule

Adding +0 to a nonzero number changes nothing, in every mode.

rule add_zero<E, S>(x: E + S, r: rm) {
        fp.add.r<E, S>(x, fp.zero<E, S>) => x if fp.not_nan<E, S>(x) && fp.nonzero<E, S>(x)
    }

fp.add.rtp.f32(fp.from_ubv.rne.f32(i:8 | 1), 0) → fp.from_ubv.rne.f32(i:8 | 1)

`add_neg_zero` — rule

Adding −0 to a nonzero number changes nothing, in every mode.

rule add_neg_zero<E, S>(x: E + S, r: rm) {
        fp.add.r<E, S>(x, fp.nzero<E, S>) => x if fp.not_nan<E, S>(x) && fp.nonzero<E, S>(x)
    }

fp.add.rtn.f32(fp.from_ubv.rne.f32(i:8 | 1), 0x80000000) → fp.from_ubv.rne.f32(i:8 | 1)

`add_neg_zero_rne` — rule

To nearest even, adding −0 changes no number, a zero included (−0 + −0 is −0, +0 + −0 is +0): x − 0 is x.

rule add_neg_zero_rne<E, S>(x: E + S) {
        fp.add.rne<E, S>(x, fp.nzero<E, S>) => x if fp.not_nan<E, S>(x)
    }

fp.sub.rne.f64(fp.from_sbv.rne.f64(i:32), 0) → fp.from_sbv.rne.f64(i:32)

`eq_self` — rule

A number equals itself (a NaN does not).

rule eq_self<E, S>(x: E + S) { fp.eq<E, S>(x, x) => true if fp.not_nan<E, S>(x) }

fp.eq.f64(fp.from_sbv.rne.f64(i:32), fp.from_sbv.rne.f64(i:32)) → true

`le_self` — rule

A number is at most itself.

rule le_self<E, S>(x: E + S) { fp.le<E, S>(x, x) => true if fp.not_nan<E, S>(x) }

fp.le.f64(fp.from_sbv.rne.f64(i:32), fp.from_sbv.rne.f64(i:32)) → true

`min_self` — rule

A number is its own minimum and maximum.

rule min_self<E, S>(x: E + S) { fp.min<E, S>(x, x) => x if fp.not_nan<E, S>(x) }

fp.min.f64(fp.from_sbv.rne.f64(i:32), fp.from_sbv.rne.f64(i:32)) → fp.from_sbv.rne.f64(i:32)

`max_self` — rule

rule max_self<E, S>(x: E + S) { fp.max<E, S>(x, x) => x if fp.not_nan<E, S>(x) }

fp.max.f64(fp.from_sbv.rne.f64(i:32), fp.from_sbv.rne.f64(i:32)) → fp.from_sbv.rne.f64(i:32)

`div_self` — rule

A finite nonzero number divided by itself is exactly 1, in every mode.

rule div_self<E, S>(x: E + S, r: rm) {
        fp.div.r<E, S>(x, x) => fp.one<E, S> if fp.finite<E, S>(x) && fp.nonzero<E, S>(x)
    }

fp.div.rne.f64(fp.from_ubv.rne.f64(zext<32>(u:8) + 1), fp.from_ubv.rne.f64(zext<32>(u:8) + 1)) → 0x3ff0000000000000:64

`sub_self_rne` — rule

A finite number minus itself is +0 (the sum of opposites rounds to +0 except toward −∞).

rule sub_self_rne<E, S>(x: E + S) { fp.add.rne<E, S>(x, fp.neg<E, S>(x)) => fp.zero<E, S> if fp.finite<E, S>(x) }

fp.sub.rne.f64(fp.from_sbv.rne.f64(i:32), fp.from_sbv.rne.f64(i:32)) → 0:64

`sub_self_rna` — rule

Likewise to nearest, ties away.

rule sub_self_rna<E, S>(x: E + S) { fp.add.rna<E, S>(x, fp.neg<E, S>(x)) => fp.zero<E, S> if fp.finite<E, S>(x) }

fp.sub.rna.f64(fp.from_sbv.rne.f64(i:32), fp.from_sbv.rne.f64(i:32)) → 0:64

`sub_self_rtp` — rule

Likewise toward +∞.

rule sub_self_rtp<E, S>(x: E + S) { fp.add.rtp<E, S>(x, fp.neg<E, S>(x)) => fp.zero<E, S> if fp.finite<E, S>(x) }

fp.sub.rtp.f64(fp.from_sbv.rne.f64(i:32), fp.from_sbv.rne.f64(i:32)) → 0:64

`sub_self_rtz` — rule

Likewise toward 0.

rule sub_self_rtz<E, S>(x: E + S) { fp.add.rtz<E, S>(x, fp.neg<E, S>(x)) => fp.zero<E, S> if fp.finite<E, S>(x) }

fp.sub.rtz.f64(fp.from_sbv.rne.f64(i:32), fp.from_sbv.rne.f64(i:32)) → 0:64

`sub_self_rtn` — rule

Toward −∞, a finite number minus itself is −0.

rule sub_self_rtn<E, S>(x: E + S) { fp.add.rtn<E, S>(x, fp.neg<E, S>(x)) => fp.nzero<E, S> if fp.finite<E, S>(x) }

fp.sub.rtn.f64(fp.from_sbv.rne.f64(i:32), fp.from_sbv.rne.f64(i:32)) → 0x8000000000000000:64

`sqrt_square` — rule

The square root of a square is the magnitude when the square is a normal number (no overflow, no underflow), to nearest: |x| between 2^⌈emin/2⌉ and 2^⌊emax/2⌋.

rule sqrt_square<E, S>(x: E + S) {
        fp.sqrt.rne<E, S>(fp.mul.rne<E, S>(x, x)) => fp.abs<E, S>(x)
        if (proves(lo <=u x) && proves(x <u hi)) || (proves(nlo <=u x) && proves(x <u nhi))
        let b: E + S = (one << (E - 1)) - one
        let lo: E + S = (b - ((b - one) >>u 1)) << (S - 1)
        let hi: E + S = (b + (b >>u 1)) << (S - 1)
        let nlo: E + S = lo | smin_lit
        let nhi: E + S = hi | smin_lit
    }

fp.sqrt.rne.f64(fp.mul.rne.f64(fp.from_ubv.rne.f64(zext<32>(u:8) + 1), fp.from_ubv.rne.f64(zext<32>(u:8) + 1))) → fp.from_ubv.rne.f64(zext<32>(u:8) + 1) & 0x7fffffffffffffff

`widen_narrow` — rule

Widening and narrowing back is exact for numbers (every number of the narrower format is one of the wider).

rule widen_narrow<E, S, F, T>(x: E + S, r: rm, q: rm) where E <= F, S <= T {
        fp.convert.r<F, T, E, S>(fp.convert.q<E, S, F, T>(x)) => x if fp.not_nan<E, S>(x)
    }

fp.convert.rne.f64.f32(fp.convert.rne.f32.f64(fp.from_sbv.rne.f32(i:16))) → fp.from_sbv.rne.f32(i:16)

core.float_values

`mul_one` — rule (`#[float_values]`: equal as floats, applied only on request)

x · 1 is x as a float (a NaN’s product is the canonical NaN). With div_pow2, x / 1 is x too.

rule mul_one<E, S>(x: E + S, r: rm) { fp.mul.r<E, S>(x, fp.one<E, S>) => x }

fp.mul.rne.f32(p:32, 0x3f800000) → p:32

`mul_neg_one` — rule (`#[float_values]`: equal as floats, applied only on request)

x · −1 is −x as a float.

rule mul_neg_one<E, S>(x: E + S, r: rm) { fp.mul.r<E, S>(x, fp.none<E, S>) => fp.neg<E, S>(x) }

fp.mul.rne.f32(p:32, 0xbf800000) → p:32 ^ 0x80000000

`add_neg_zero_rne` — rule (`#[float_values]`: equal as floats, applied only on request)

x + (−0) is x as a float, to nearest (toward −∞, +0 + −0 is −0).

rule add_neg_zero_rne<E, S>(x: E + S) { fp.add.rne<E, S>(x, fp.nzero<E, S>) => x }

fp.add.rne.f32(p:32, 0x80000000) → p:32

`add_neg_zero_rna` — rule (`#[float_values]`: equal as floats, applied only on request)

Likewise to nearest, ties away.

rule add_neg_zero_rna<E, S>(x: E + S) { fp.add.rna<E, S>(x, fp.nzero<E, S>) => x }

fp.add.rna.f32(p:32, 0x80000000) → p:32

`add_neg_zero_rtp` — rule (`#[float_values]`: equal as floats, applied only on request)

Likewise toward +∞.

rule add_neg_zero_rtp<E, S>(x: E + S) { fp.add.rtp<E, S>(x, fp.nzero<E, S>) => x }

fp.add.rtp.f32(p:32, 0x80000000) → p:32

`add_neg_zero_rtz` — rule (`#[float_values]`: equal as floats, applied only on request)

Likewise toward 0.

rule add_neg_zero_rtz<E, S>(x: E + S) { fp.add.rtz<E, S>(x, fp.nzero<E, S>) => x }

fp.add.rtz.f32(p:32, 0x80000000) → p:32

`min_self` — rule (`#[float_values]`: equal as floats, applied only on request)

A value is its own minimum.

rule min_self<E, S>(x: E + S) { fp.min<E, S>(x, x) => x }

fp.min.f32(p:32, p:32) → p:32

`max_self` — rule (`#[float_values]`: equal as floats, applied only on request)

And its own maximum.

rule max_self<E, S>(x: E + S) { fp.max<E, S>(x, x) => x }

fp.max.f32(p:32, p:32) → p:32

`widen_narrow` — rule (`#[float_values]`: equal as floats, applied only on request)

Widening and narrowing back is x as a float.

rule widen_narrow<E, S, F, T>(x: E + S, r: rm, q: rm) where E <= F, S <= T {
        fp.convert.r<F, T, E, S>(fp.convert.q<E, S, F, T>(x)) => x
    }

fp.convert.rne.f64.f32(fp.convert.rne.f32.f64(p:32)) → p:32

identity add_assoc<W>(x: W, y: W, z: W) { (x + y) + z <=> x + (y + z) }

(p + q) + r → p + (q + r)

`mul_assoc` — identity (search only)

identity mul_assoc<W>(x: W, y: W, z: W) { (x * y) * z <=> x * (y * z) }

(p * q) * r → p * (q * r)

`and_assoc` — identity (search only)

identity and_assoc<W>(x: W, y: W, z: W) { (x & y) & z <=> x & (y & z) }

(p & q) & r → p & (q & r)

`or_assoc` — identity (search only)

identity or_assoc<W>(x: W, y: W, z: W) { (x | y) | z <=> x | (y | z) }

(p | q) | r → p | (q | r)

`xor_assoc` — identity (search only)

identity xor_assoc<W>(x: W, y: W, z: W) { (x ^ y) ^ z <=> x ^ (y ^ z) }

(p ^ q) ^ r → p ^ (q ^ r)

eqsat.distrib

`mul_add` — identity (search only)

identity mul_add<W>(x: W, y: W, z: W) { x * (y + z) <=> x * y + x * z }

p * (q + r) → p * q + p * r

eqsat.distrib_and

`and_or` — identity (search only)

identity and_or<W>(x: W, y: W, z: W) { x & (y | z) <=> (x & y) | (x & z) }

p & (q | r) → (p & q) | (p & r)

`and_xor` — identity (search only)

identity and_xor<W>(x: W, y: W, z: W) { x & (y ^ z) <=> (x & y) ^ (x & z) }

p & (q ^ r) → (p & q) ^ (p & r)

eqsat.distrib_or

`or_and` — identity (search only)

identity or_and<W>(x: W, y: W, z: W) { x | (y & z) <=> (x | y) & (x | z) }

p | (q & r) → (p | q) & (p | r)

eqsat.negation

`de_morgan_and` — identity (search only)

identity de_morgan_and<W>(x: W, y: W) { ~(x & y) <=> ~x | ~y }

~(p & q) → ~p | ~q

`de_morgan_or` — identity (search only)

identity de_morgan_or<W>(x: W, y: W) { ~(x | y) <=> ~x & ~y }

~(p | q) → ~p & ~q

`neg_add` — identity (search only)

identity neg_add<W>(x: W, y: W) { -(x + y) <=> -x + -y }

-(p + q) → -p + -q

`neg_mul` — identity (search only)

identity neg_mul<W>(x: W, y: W) { -(x * y) <=> -x * y }

-(p * q) → -p * q

`not_xor` — identity (directed and search)

identity not_xor<W>(x: W, y: W) { ~(x ^ y) <=> ~x ^ y }

~(p ^ q) → ~p ^ q

eqsat.cancel

`add_sub` — rule

rule add_sub<W>(x: W, y: W) { (x + y) - y => x }

(p + q) - q → p

`sub_add` — rule

rule sub_add<W>(x: W, y: W) { (x - y) + y => x }

(p - q) + q → p

`xor_xor` — rule

rule xor_xor<W>(x: W, y: W) { (x ^ y) ^ y => x }

(p ^ q) ^ q → p

`neg_neg` — rule

rule neg_neg<W>(x: W) { -(-x) => x }

`not_not` — rule

rule not_not<W>(x: W) { ~(~x) => x }

`add_neg` — rule

rule add_neg<W>(x: W) { x + -x => 0 }

p + -p → 0

`mul_one` — rule

rule mul_one<W>(x: W) { x * 1 => x }

`mul_zero` — rule

rule mul_zero<W>(x: W) { x * 0 => 0 }

`add_zero` — rule

rule add_zero<W>(x: W) { x + 0 => x }

Keyboard shortcuts

bitwright