rucc_verify/

model.rs

//! What the terms in a rule mean, in bitvectors.
//!
//! A rule relates an IR term to a machine term and claims the two compute the same thing. A
//! solver cannot check that claim without being told what the terms are, so every head a rule
//! uses needs an entry here. `spec/10-backend.md` calls this Crocus's stated tax and says to pay
//! it from the first rule rather than retrofitting it, which is why a head with no entry is an
//! error rather than an unchecked assumption.
//!
//! The model is written in the same language as the rules:
//!
//! ```text
//! (semantics (amode_base_index_scale base index scale) (bvadd base (bvmul index scale)))
//! (semantics (x64.lea address) address)
//! ```
//!
//! Anything the solver already knows is not written down. Those are the [`BUILTIN`] heads, and
//! they are spelled the way SMT-LIB spells them except for the comparisons, where a rule writes
//! `<` and the solver wants `bvslt`.
//!
//! # Widths
//!
//! Every term is some number of bits wide and [`Widths`] is what says how many. A head that ends
//! in `.iN` is N bits wide, anything else is as wide as the term it sits inside, and a name is as
//! wide as the place in the pattern that bound it. That is enough for a rule to convert between
//! widths, which is what `sext`, `zext` and `trunc` all are, and those conversions are written
//! the way `spec/10-backend.md` writes them: `(sign_extend 32 64 x)` and `(extract 31 0 x)`, with
//! the widths spelled out rather than left to be inferred.
//!
//! The widths are checked here rather than left to the solver, because a solver handed two
//! bitvectors of different sorts says so in its own words and at a place in generated text that
//! nobody wants to read.
//!
//! # Memory
//!
//! A rule with an effect is a claim about memory as well as about a value, so not everything a
//! term computes is a bitvector and [`Sort`] is what says which it is. Memory is one map from an
//! address to a byte, written as an SMT-LIB array, and the three heads that touch it are
//! [`MEMORY`]: `(mem)` is the memory a rule starts from, `select` reads one byte of it and
//! `store` writes one.
//!
//! Nothing wider than a byte is built in, which is deliberate. A load of four bytes is four
//! `select`s put together with `concat` and a store of four bytes is four nested `store`s, both
//! written out in the model file, so the byte order is a thing a reviewer reads rather than a
//! thing this file decides on their behalf. That is the one fact about memory access that no
//! amount of testing on one machine will catch.

use std::collections::{BTreeMap, HashMap};

use rucc_rules::{Error, Term, TermKind, parse_terms};

/// The heads the solver already understands, and what SMT-LIB calls them.
///
/// The comparisons written as symbols are the signed ones. An unsigned comparison in a rule has
/// to be written with the solver's own name for it, which is deliberate: a rule that means the
/// unsigned one should have to say so rather than depend on which way this table happens to read.
/// Both families are here under those names as well, so a rule that would rather be explicit
/// about the signed one can be.
const BUILTIN: [(&str, &str); 32] = [
    ("=", "="),
    ("and", "and"),
    ("or", "or"),
    ("not", "not"),
    ("<", "bvslt"),
    ("<=", "bvsle"),
    (">", "bvsgt"),
    (">=", "bvsge"),
    ("bvslt", "bvslt"),
    ("bvsle", "bvsle"),
    ("bvsgt", "bvsgt"),
    ("bvsge", "bvsge"),
    ("bvult", "bvult"),
    ("bvule", "bvule"),
    ("bvugt", "bvugt"),
    ("bvuge", "bvuge"),
    ("bvadd", "bvadd"),
    ("bvsub", "bvsub"),
    ("bvmul", "bvmul"),
    ("bvneg", "bvneg"),
    ("bvnot", "bvnot"),
    ("bvand", "bvand"),
    ("bvor", "bvor"),
    ("bvxor", "bvxor"),
    ("bvshl", "bvshl"),
    ("bvlshr", "bvlshr"),
    ("bvashr", "bvashr"),
    ("bvsdiv", "bvsdiv"),
    ("bvudiv", "bvudiv"),
    ("bvsrem", "bvsrem"),
    ("bvurem", "bvurem"),
    ("ite", "ite"),
];

/// The builtins that take a boolean somewhere, so their arguments are not all one width and
/// there is nothing to check between them.
const LOGICAL: [&str; 4] = ["and", "or", "not", "ite"];

/// The heads that change width. Their first two arguments are widths rather than values, which
/// is why they are written out here rather than sitting in [`BUILTIN`] with the rest: SMT-LIB
/// spells them as indexed operators and the index is a number this has to work out.
const CONVERSION: [&str; 3] = ["sign_extend", "zero_extend", "extract"];

/// The heads that touch memory, which are not in [`BUILTIN`] because their arguments are not all
/// the same sort and their results are not all the same sort either.
const MEMORY: [&str; 3] = ["mem", "select", "store"];

/// Putting bitvectors end to end, which is how a load of more than one byte is written. Not in
/// [`BUILTIN`] because its arguments are one width and its result is their total.
const CONCAT: &str = "concat";

/// How wide an address is.
///
/// Every target `spec/12-abi-and-runtime.md` implements for 1.0 is sixty four bit, so this is a
/// constant rather than something the model file says. When a thirty two bit target arrives it
/// becomes something the model file says, and the rules that read memory will be the ones that
/// notice.
pub const ADDRESS_WIDTH: u32 = 64;

/// How wide a byte is, which is the element of memory.
pub const BYTE_WIDTH: u32 = 8;

/// What the memory a rule starts from is called in the query.
///
/// A name no rule can bind, because a name in a rule comes out of a pattern and a pattern binds
/// what the selector matched, which is registers and constants and never memory.
pub const MEMORY_CONST: &str = "mem";

/// What kind of thing a term computes.
///
/// Almost everything is a bitvector, and the exception is the whole point of this type: a rule
/// with an effect relates one memory to another, and a memory is not a number however many bits
/// one is willing to spend on it.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum Sort {
    /// A bitvector this many bits wide.
    Bits(u32),
    /// The whole of memory, a map from an address to a byte.
    Memory,
}

impl Sort {
    /// How many bits wide it is, or nothing when it is not a bitvector at all.
    #[must_use]
    pub fn bits(self) -> Option<u32> {
        match self {
            Sort::Bits(width) => Some(width),
            Sort::Memory => None,
        }
    }

    /// What SMT-LIB calls it, at the widths this question is being asked at.
    #[must_use]
    pub fn write(self, widths: &Widths) -> String {
        match self {
            Sort::Bits(width) => format!("(_ BitVec {width})"),
            Sort::Memory => {
                format!("(Array (_ BitVec {}) (_ BitVec {}))", widths.address(), widths.byte())
            }
        }
    }

    /// How it reads in a message to somebody who has written a rule that does not fit together.
    fn describe(self) -> String {
        match self {
            Sort::Bits(width) => format!("{width} bits wide"),
            Sort::Memory => "the whole of memory".to_owned(),
        }
    }
}

/// What a rule works in when its opcode does not say. Every opcode in the IR does say, so this
/// is what a hand written test rule gets rather than something the real rule set relies on.
pub const DEFAULT_WIDTH: u32 = 64;

/// How wide each thing in one rule is.
///
/// A rule is written at one width, the one its pattern's opcode names, and the terms inside it
/// may say another: `(value.i64 x)` under an `add.i32` is a thirty two bit add of two sixty four
/// bit registers, which is the shape every `sext`, `zext` and `trunc` in a lowering has. What a
/// name stands at is fixed by the pattern, because the pattern is where a name is bound, and
/// everywhere else reads it from here.
///
/// A bounded proof asks the same rule at a narrower width, and that scales every width in the
/// rule by one ratio rather than flattening them all to one number. A rule that converts between
/// widths still converts between widths when it is asked at eight bits, which it would not do if
/// the narrow width were simply substituted everywhere.
#[derive(Debug, Clone, Default)]
pub struct Widths {
    /// The width the rule is written in.
    natural: u32,
    /// The width it is being asked at, which is the same number unless this is a bounded proof.
    asked: u32,
    /// What each name the pattern binds stands at, already scaled.
    at: BTreeMap<String, Sort>,
}

impl Widths {
    /// The widths one rule's pattern fixes, at the width the rule is written in.
    #[must_use]
    pub fn of(pattern: &Term) -> Widths {
        Widths::at(pattern, rule_width(pattern))
    }

    /// The same, scaled to a width somebody asked for. This is what a bounded proof is made of.
    #[must_use]
    pub fn at(pattern: &Term, asked: u32) -> Widths {
        let natural = rule_width(pattern);
        let mut widths = Widths { natural, asked, at: BTreeMap::new() };
        widths.bind(pattern, asked);
        widths
    }

    /// The width a term is at when nothing inside it says otherwise.
    #[must_use]
    pub fn width(&self) -> u32 {
        self.asked
    }

    /// The width the rule is written in, which is the one it will run at.
    #[must_use]
    pub fn natural(&self) -> u32 {
        self.natural
    }

    /// Every name the pattern binds and how wide it is, sorted.
    ///
    /// Sorted rather than in the order the pattern binds them, because the query is something a
    /// test pins and a diff is easier to read than it is to regenerate.
    pub fn names(&self) -> impl Iterator<Item = (&str, u32)> {
        self.at.iter().filter_map(|(name, sort)| Some((name.as_str(), sort.bits()?)))
    }

    /// These widths and one more name, which is how the replacement's own meaning gets a width
    /// once it has been substituted into the specification for `(result)`.
    ///
    /// A replacement that computes a memory is recorded as one, so that the specification which
    /// reads it back is checked against a memory rather than against a number of bits nobody
    /// meant.
    #[must_use]
    pub fn with(&self, name: &str, sort: Sort) -> Widths {
        let mut out = self.clone();
        out.at.insert(name.to_owned(), sort);
        out
    }

    /// How wide an address is here, scaled like everything else.
    #[must_use]
    pub fn address(&self) -> u32 {
        self.scale(ADDRESS_WIDTH)
    }

    /// How wide a byte is here, scaled like everything else.
    ///
    /// A bounded proof asks a rule in narrower bitvectors, and a byte narrows with them. It has
    /// to: the bytes a load puts together have to add up to the value the load produces, and a
    /// value that has been scaled and bytes that have not do not add up to anything.
    #[must_use]
    pub fn byte(&self) -> u32 {
        self.scale(BYTE_WIDTH)
    }

    /// What a name stands for, when the pattern bound it.
    fn of_name(&self, name: &str) -> Option<Sort> {
        self.at.get(name).copied()
    }

    /// The width a head names, scaled.
    fn suffix(&self, head: &str) -> Option<u32> {
        declared(head).map(|width| self.scale(width))
    }

    /// A width, in the proportion the question is being asked at. Never nothing: a width that
    /// scales to zero bits is a width the rule cannot be asked about at all.
    fn scale(&self, width: u32) -> u32 {
        if self.asked == self.natural || self.natural == 0 {
            return width;
        }
        self.index(width).max(1)
    }

    /// A bit position, in the same proportion. Zero stays zero, which is what separates this
    /// from [`Widths::scale`].
    fn index(&self, position: u32) -> u32 {
        if self.asked == self.natural || self.natural == 0 {
            return position;
        }
        let scaled = u64::from(position) * u64::from(self.asked) / u64::from(self.natural);
        u32::try_from(scaled).unwrap_or(position)
    }

    /// Walk the pattern and write down what each name it binds stands at.
    fn bind(&mut self, term: &Term, context: u32) {
        match &term.kind {
            TermKind::Var(name) => {
                self.at.insert(name.clone(), Sort::Bits(context));
            }
            TermKind::Int(_) => {}
            TermKind::App { head, args } => {
                let inner = self.suffix(head).unwrap_or(context);
                for arg in args {
                    self.bind(arg, inner);
                }
            }
        }
    }
}

/// The width a rule works in, taken from the suffix on its pattern's opcode.
#[must_use]
pub fn rule_width(pattern: &Term) -> u32 {
    match &pattern.kind {
        TermKind::App { head, .. } => declared(head).unwrap_or(DEFAULT_WIDTH),
        _ => DEFAULT_WIDTH,
    }
}

/// The width a head names, if it names one. `add.i32` does and `x64.lea` does not.
fn declared(head: &str) -> Option<u32> {
    head.rsplit_once('.')
        .and_then(|(_, suffix)| suffix.strip_prefix('i'))
        .and_then(|bits| bits.parse::<u32>().ok())
}

/// What one head means.
#[derive(Debug, Clone)]
struct Meaning {
    /// The names the body is written in terms of.
    params: Vec<String>,
    /// What it computes.
    body: Term,
}

/// Everything the rules are allowed to say, and what each of it means.
#[derive(Debug, Default)]
pub struct Model {
    heads: HashMap<String, Meaning>,
}

impl Model {
    /// Read a model from text.
    ///
    /// # Errors
    ///
    /// Anything that is not a well formed `(semantics (head params) body)` form, and any head
    /// given a meaning twice.
    pub fn read(path: &str, text: &str) -> Result<Model, Vec<Error>> {
        let terms = parse_terms(path, text)?;
        let mut model = Model::default();
        let mut errors = Vec::new();

        for term in terms {
            let TermKind::App { head, args } = &term.kind else {
                errors.push(fail(path, &term, "expected a `(semantics ...)` form".to_owned()));
                continue;
            };
            if head != "semantics" || args.len() != 2 {
                errors.push(fail(path, &term, "expected a `(semantics ...)` form".to_owned()));
                continue;
            }
            let TermKind::App { head: name, args: params } = &args[0].kind else {
                errors.push(fail(path, &args[0], "expected a head and its parameters".to_owned()));
                continue;
            };
            let mut names = Vec::new();
            for param in params {
                match &param.kind {
                    TermKind::Var(name) => names.push(name.clone()),
                    _ => errors.push(fail(path, param, "a parameter has to be a name".to_owned())),
                }
            }
            if known(name) {
                let said = format!("`{name}` is something the solver already knows");
                errors.push(fail(path, &args[0], said));
                continue;
            }
            let meaning = Meaning { params: names, body: args[1].clone() };
            if model.heads.insert(name.clone(), meaning).is_some() {
                let said = format!("`{name}` is given a meaning twice");
                errors.push(fail(path, &args[0], said));
            }
        }

        if errors.is_empty() { Ok(model) } else { Err(errors) }
    }

    /// Write one term out as SMT-LIB, expanding everything the model defines, and say how wide
    /// what it computes is.
    ///
    /// # Errors
    ///
    /// A head that is neither a builtin nor in the model, since that is a term nobody has said
    /// the meaning of, an application of the wrong number of arguments, and anything whose
    /// widths do not fit together.
    pub fn write(&self, path: &str, term: &Term, widths: &Widths) -> Result<(String, Sort), Error> {
        self.write_at(path, term, widths.width(), widths, &HashMap::new())
    }

    /// Whether reading this term reaches memory, following every head the model defines.
    ///
    /// A rule that reads memory needs a solver told about arrays and a constant to stand for the
    /// memory it starts from, and neither is worth putting in a query that does not. Nothing in a
    /// rule says `(mem)` directly: a load says `load.i32`, and it is the model entry for that head
    /// which reaches memory, so this expands what the model says rather than reading the surface.
    #[must_use]
    pub fn touches_memory(&self, term: &Term) -> bool {
        match &term.kind {
            TermKind::Var(_) | TermKind::Int(_) => false,
            TermKind::App { head, args } => {
                if MEMORY.contains(&head.as_str()) {
                    return true;
                }
                if args.iter().any(|arg| self.touches_memory(arg)) {
                    return true;
                }
                self.heads.get(head).is_some_and(|meaning| self.touches_memory(&meaning.body))
            }
        }
    }

    fn write_at(
        &self,
        path: &str,
        term: &Term,
        context: u32,
        widths: &Widths,
        bound: &HashMap<&str, (String, Sort)>,
    ) -> Result<(String, Sort), Error> {
        match &term.kind {
            TermKind::Var(name) => match bound.get(name.as_str()) {
                Some((already, sort)) => Ok((already.clone(), *sort)),
                None => Ok((name.clone(), widths.of_name(name).unwrap_or(Sort::Bits(context)))),
            },
            TermKind::Int(value) => Ok((literal(*value, context), Sort::Bits(context))),
            TermKind::App { head, args } => {
                if CONVERSION.contains(&head.as_str()) {
                    return self.convert(path, term, head, args, context, widths, bound);
                }
                if MEMORY.contains(&head.as_str()) {
                    return self.reach(path, term, head, args, context, widths, bound);
                }
                if head == CONCAT {
                    return self.join(path, term, args, context, widths, bound);
                }
                if let Some(name) = builtin(head) {
                    return self.combine(path, term, head, name, args, context, widths, bound);
                }
                let own = widths.suffix(head).unwrap_or(context);
                let mut written = Vec::with_capacity(args.len());
                for arg in args {
                    written.push(self.write_at(path, arg, own, widths, bound)?);
                }
                let Some(meaning) = self.heads.get(head) else {
                    let said = format!("nothing in the model says what `{head}` means");
                    return Err(fail(path, term, said));
                };
                if meaning.params.len() != written.len() {
                    let said = format!(
                        "`{head}` means something with {} arguments and this gives it {}",
                        meaning.params.len(),
                        written.len()
                    );
                    return Err(fail(path, term, said));
                }
                let inner: HashMap<&str, (String, Sort)> =
                    meaning.params.iter().map(String::as_str).zip(written).collect();
                let (text, sort) = self.write_at(path, &meaning.body, own, widths, &inner)?;
                // An opcode that names a width has to mean something that wide. This is the
                // model being held to what the rules say about it: `add.i32` over registers
                // that are sixty four bits wide means an add of their low halves, and a model
                // that leaves the truncation out says so here rather than in a proof that
                // quietly asks the wrong question.
                //
                // A head that means a memory is the one exception, and it is not a hole. The
                // width on `store.i32` is the width of what it wrote rather than of what it
                // computes, and that width is checked all the same, by the extracts in the
                // model entry having to come out of something that wide.
                if let (Some(said), Some(width)) = (widths.suffix(head), sort.bits()) {
                    if said != width {
                        let told = format!(
                            "`{head}` is written for {said} bits and means something {width} \
                             bits wide"
                        );
                        return Err(fail(path, term, told));
                    }
                }
                Ok((text, sort))
            }
        }
    }

    /// One of the heads the solver already knows, applied to arguments that all have to be the
    /// same width unless a boolean is involved.
    #[allow(clippy::too_many_arguments)]
    fn combine(
        &self,
        path: &str,
        term: &Term,
        head: &str,
        name: &str,
        args: &[Term],
        context: u32,
        widths: &Widths,
        bound: &HashMap<&str, (String, Sort)>,
    ) -> Result<(String, Sort), Error> {
        // A number has no width of its own and takes the width of what it sits beside. Every
        // rule written before memory arrived had one width throughout, so this changed nothing
        // for them, and it is what lets an offset added to an address in the model be as wide as
        // the address rather than as wide as the value being loaded through it.
        //
        // Not under a head that takes a boolean. What a number sits beside there is a
        // comparison, and a comparison has no width to lend: the one and the zero an `ite`
        // chooses between are as wide as the term the `ite` is in, which is what `context` is.
        let beside = if LOGICAL.contains(&head) {
            context
        } else {
            self.beside(path, args, context, widths, bound)?
        };
        let mut written = Vec::with_capacity(args.len());
        for arg in args {
            let at = if matches!(arg.kind, TermKind::Int(_)) { beside } else { context };
            written.push(self.write_at(path, arg, at, widths, bound)?);
        }
        let Some((_, first)) = written.first() else {
            return Err(fail(path, term, format!("`{head}` needs arguments")));
        };
        let first = *first;
        if !LOGICAL.contains(&head) {
            if let Some((_, other)) = written.iter().find(|(_, sort)| *sort != first) {
                let said = format!(
                    "`{head}` is given something {} and something {}, and those are not the \
                     same kind of thing",
                    first.describe(),
                    other.describe()
                );
                return Err(fail(path, term, said));
            }
        }
        // A comparison computes a boolean and its width is nobody's business, so saying it is
        // as wide as what it compared costs nothing and keeps every term having an answer.
        let sort = if head == "ite" && written.len() > 1 { written[1].1 } else { first };
        let texts: Vec<&str> = written.iter().map(|(text, _)| text.as_str()).collect();
        Ok((format!("({name} {})", texts.join(" ")), sort))
    }

    /// The width the numbers among a head's arguments should take, which is the width of the
    /// first argument that has one of its own. Nothing when they are all numbers, in which case
    /// the surrounding width is as good an answer as there is.
    fn beside(
        &self,
        path: &str,
        args: &[Term],
        context: u32,
        widths: &Widths,
        bound: &HashMap<&str, (String, Sort)>,
    ) -> Result<u32, Error> {
        if !args.iter().any(|arg| matches!(arg.kind, TermKind::Int(_))) {
            return Ok(context);
        }
        let Some(sized) = args.iter().find(|arg| !matches!(arg.kind, TermKind::Int(_))) else {
            return Ok(context);
        };
        let (_, sort) = self.write_at(path, sized, context, widths, bound)?;
        Ok(sort.bits().unwrap_or(context))
    }

    /// One of the three heads that touch memory.
    #[allow(clippy::too_many_arguments)]
    fn reach(
        &self,
        path: &str,
        term: &Term,
        head: &str,
        args: &[Term],
        context: u32,
        widths: &Widths,
        bound: &HashMap<&str, (String, Sort)>,
    ) -> Result<(String, Sort), Error> {
        // The memory a rule starts from, which is one constant and takes no arguments. It is
        // written `(mem)` for the reason `(result)` is: a head applied to nothing is still an
        // application, because a bare name is a variable.
        if head == "mem" {
            if !args.is_empty() {
                let said = "`mem` is the memory a rule starts from and takes nothing".to_owned();
                return Err(fail(path, term, said));
            }
            return Ok((MEMORY_CONST.to_owned(), Sort::Memory));
        }

        let wanted = if head == "select" { 2 } else { 3 };
        if args.len() != wanted {
            let said =
                format!("`{head}` takes {wanted} arguments and this gives it {}", args.len());
            return Err(fail(path, term, said));
        }
        let mut written = Vec::with_capacity(args.len());
        for arg in args {
            let at = if matches!(arg.kind, TermKind::Int(_)) { widths.address() } else { context };
            written.push(self.write_at(path, arg, at, widths, bound)?);
        }
        // The sorts of the three positions, which is the whole of what an array is: a memory, an
        // address into it, and for a store the byte that goes there.
        let expected = [Sort::Memory, Sort::Bits(widths.address()), Sort::Bits(widths.byte())];
        for (at, (_, got)) in written.iter().enumerate() {
            if *got != expected[at] {
                let said = format!(
                    "`{head}` takes something {} in position {at} and this is {}",
                    expected[at].describe(),
                    got.describe()
                );
                return Err(fail(path, term, said));
            }
        }
        let texts: Vec<&str> = written.iter().map(|(text, _)| text.as_str()).collect();
        let sort = if head == "select" { Sort::Bits(widths.byte()) } else { Sort::Memory };
        Ok((format!("({head} {})", texts.join(" ")), sort))
    }

    /// Bitvectors end to end, which is as wide as all of them together.
    ///
    /// The first argument is the high end, which is how SMT-LIB reads it and is the opposite of
    /// the order the bytes of a little endian load are at in memory. That is why a load in the
    /// model file counts down.
    fn join(
        &self,
        path: &str,
        term: &Term,
        args: &[Term],
        context: u32,
        widths: &Widths,
        bound: &HashMap<&str, (String, Sort)>,
    ) -> Result<(String, Sort), Error> {
        if args.len() < 2 {
            let said = format!("`concat` puts two or more things together and this gives it {}", {
                args.len()
            });
            return Err(fail(path, term, said));
        }
        let mut total = 0;
        let mut texts = Vec::with_capacity(args.len());
        for arg in args {
            let (text, sort) = self.write_at(path, arg, context, widths, bound)?;
            let Some(width) = sort.bits() else {
                let said = "`concat` puts bitvectors together and this is a memory".to_owned();
                return Err(fail(path, arg, said));
            };
            total += width;
            texts.push(text);
        }
        Ok((format!("(concat {})", texts.join(" ")), Sort::Bits(total)))
    }

    /// A conversion between widths, written as `spec/10-backend.md` writes it, with the widths
    /// as arguments rather than inferred from anything.
    #[allow(clippy::too_many_arguments)]
    fn convert(
        &self,
        path: &str,
        term: &Term,
        head: &str,
        args: &[Term],
        context: u32,
        widths: &Widths,
        bound: &HashMap<&str, (String, Sort)>,
    ) -> Result<(String, Sort), Error> {
        if args.len() != 3 {
            let said = format!("`{head}` takes two numbers and a value, and this gives it {}", {
                args.len()
            });
            return Err(fail(path, term, said));
        }
        // Two numbers, and which two they are depends on the head: the bit positions an extract
        // takes, and the widths an extension goes between.
        let (first, second) = (number(path, head, &args[0])?, number(path, head, &args[1])?);

        if head == "extract" {
            let (high, low) = (first, second);
            if high < low {
                let said = format!("`extract` takes bits {high} down to {low}, which is none");
                return Err(fail(path, term, said));
            }
            let width = widths.scale(high - low + 1);
            let bottom = widths.index(low);
            let top = bottom + width - 1;
            let (text, sort) = self.write_at(path, &args[2], context, widths, bound)?;
            let of = bits(path, head, &args[2], sort)?;
            if top >= of {
                let said = format!(
                    "`extract` takes bits {top} down to {bottom} of something {of} bits wide"
                );
                return Err(fail(path, term, said));
            }
            return Ok((format!("((_ extract {top} {bottom}) {text})"), Sort::Bits(width)));
        }

        let (from, to) = (widths.scale(first), widths.scale(second));
        if to < from {
            let said = format!("`{head}` goes from {from} bits to {to}, which is narrower");
            return Err(fail(path, term, said));
        }
        let (text, sort) = self.write_at(path, &args[2], from, widths, bound)?;
        let of = bits(path, head, &args[2], sort)?;
        if of != from {
            let said =
                format!("`{head}` goes from {from} bits and is given something {of} bits wide");
            return Err(fail(path, term, said));
        }
        // Extending by nothing is written as nothing rather than as an extension by zero,
        // because a bounded proof can scale two different widths onto the same one.
        if to == from {
            return Ok((text, Sort::Bits(to)));
        }
        Ok((format!("((_ {head} {}) {text})", to - from), Sort::Bits(to)))
    }
}

/// What SMT-LIB calls this head, if it already knows it.
fn builtin(head: &str) -> Option<&'static str> {
    BUILTIN.iter().find(|(name, _)| *name == head).map(|(_, smt)| *smt)
}

/// Whether the solver already knows this head, and so whether the model may not redefine it.
fn known(head: &str) -> bool {
    builtin(head).is_some()
        || CONVERSION.contains(&head)
        || MEMORY.contains(&head)
        || head == CONCAT
}

/// How wide something is, when it has to be a bitvector and the rule is wrong if it is not.
fn bits(path: &str, head: &str, term: &Term, sort: Sort) -> Result<u32, Error> {
    sort.bits().ok_or_else(|| {
        let said = format!("`{head}` works on bitvectors and this is {}", sort.describe());
        fail(path, term, said)
    })
}

/// One of the numbers a conversion is written with.
fn number(path: &str, head: &str, term: &Term) -> Result<u32, Error> {
    match &term.kind {
        TermKind::Int(value) => u32::try_from(*value).map_err(|_| {
            let said = format!("`{head}` is given {value} where it needs a number of bits");
            fail(path, term, said)
        }),
        _ => {
            let said = format!("`{head}` says which widths it goes between, in numbers");
            Err(fail(path, term, said))
        }
    }
}

/// A literal at the rule's width. Negative values are written as the bit pattern they are, since
/// SMT-LIB has no sign on a bitvector literal.
fn literal(value: i128, width: u32) -> String {
    let wrapped =
        if width >= 128 { value as u128 } else { (value as u128) & ((1u128 << width) - 1) };
    format!("(_ bv{wrapped} {width})")
}

fn fail(path: &str, term: &Term, message: String) -> Error {
    Error { path: path.to_owned(), line: term.line, column: term.column, message }
}