Module ext 

Extension operations: host-defined, total, multi-output operators.

A host whose instruction set has operations bitwright does not model as a composition of its own (a flags bundle, a funnel shift, a vendor-specific count) registers them as ExtOps. An extension call takes one to three arguments and has one to eight outputs; each output is a node of its own, hash-consed by the operation, the output and the arguments, so its value is a function of its arguments like any other node. Evaluation, facts, sampled verification and SMT-LIB export go through the operation’s own methods; to the rules and the passes an extension node is an opaque atom (its arguments are still simplified, unless the operation asks otherwise).

Operations are collected into an immutable Registry before a context uses it (Context::with_registry). Registering one runs a contract self-test: declared widths, determinism, known-bits soundness against eval, expand ≡ eval, and invertibility declarations against invert, at a battery of widths.

An output that is injective or bijective in one argument (the others fixed) can say so (ExtOp::invertible, ExtOp::invert): the simplifier then cancels the call on both sides of an equality and solves it at a constant, and Query::Injective sees through it.

An operation that must not be merged with another call on the same arguments (an occurrence), takes a fresh symbol as one of its arguments.

use std::sync::Arc;
use bitwright::ext::{ExtOp, ExtSig, Registry};
use bitwright::{BitVec, BinOp, Context, ContextConfig, Width};

/// Unsigned average rounding down, without overflow.
struct AvgU;
impl ExtOp for AvgU {
    fn name(&self) -> &str { "acme.avgu" }
    fn signature(&self, args: &[Width]) -> Result<ExtSig, String> {
        match args {
            [a, b] if a == b => Ok(ExtSig::new(&[("avg", *a)])),
            _ => Err("two operands of one width".into()),
        }
    }
    fn eval(&self, args: &[BitVec], out: &mut [BitVec]) {
        let (a, b) = (&args[0], &args[1]);
        let both = BitVec::apply_bin(BinOp::And, a, b).unwrap();
        let either = BitVec::apply_bin(BinOp::Xor, a, b).unwrap();
        let one = BitVec::one(a.width());
        let half = BitVec::apply_bin(BinOp::LShr, &either, &one).unwrap();
        out[0] = BitVec::apply_bin(BinOp::Add, &both, &half).unwrap();
    }
}

let registry = Arc::new(Registry::builder().register(AvgU)?.build());
let mut cx = Context::with_registry(ContextConfig::default(), registry.clone());
let avg = registry.id("acme.avgu").unwrap();
let x = cx.symbol("x", Width::W8)?;
let c = cx.constant_u64(Width::W8, 200)?;
let d = cx.constant_u64(Width::W8, 100)?;
let folded = cx.ext(avg, &[c, d])?;
assert_eq!(cx.as_const(folded[0])?.and_then(|v| v.to_u64()), Some(150));
let open = cx.ext(avg, &[x, d])?;
assert_eq!(cx.display(open[0]).to_string(), "@acme.avgu(x, 100:8)");

Structs

ExtArgs

The arguments of an extension call (1 to 3).

ExtId

An operation in a Registry: its position, and a tag of its name and revision, so an id used with a registry that has another operation at that position is refused.

ExtInverse

The operation that undoes an output of another in one argument (see ExtOp::inverse).

ExtSig

The outputs of an extension operation at some argument widths: a role name and a width each.

ExtTraits

Properties of an extension operation the builder and simplifier may use.

Registry

An immutable set of extension operations.

RegistryBuilder

Collects operations into a Registry.

Enums

ExtError

Why an operation was refused by RegistryBuilder::register.

InverseArg

An argument of an inverse call (see ExtOp::inverse).

Invertible

How an output of an extension operation depends on one argument when the others are fixed (see ExtOp::invertible).

Constants

MAX_ARGS

The most arguments an extension call takes.

MAX_OPS

The most operations a registry holds.

MAX_OUTPUTS

The most outputs an extension operation has.

Traits

ExtOp

A host-defined operation. Every method must be deterministic; eval must be total.

Functions

check

The contract self-test RegistryBuilder::register runs (see the module docs): Ok if the sampled checks found no breach. For hosts that register with register_unchecked and test their operations once.