Function query_at 

pub fn query_at(
    path: &str,
    rule: &Rule,
    model: &Model,
    width: u32,
) -> Result<String, Error>

The same question asked at a width somebody chose.

This is what a bounded proof is made of: the rule’s own claim, in narrower bitvectors than the ones it will run in. Every width in the rule scales by the one ratio, so a rule that converts between widths still converts between them here.

Errors

Anything the model cannot write out, which is any term nobody has said the meaning of, and anything whose widths do not fit together.