Constrained decoding

# The guarantee

Once the model emits calculate(, a pushdown automaton masks the logits at every step. Malformed JSON, a field that is not in the schema, an out-of-range number, a missing required key: none of them can be generated. Not validated after the fact, unrepresentable. Sampling runs after masking, so no sampling strategy can escape it.

# The guarantee is not tied to this engine

The constraint contract is three signatures over &mut [f32] and u32 living in tacet-kernel, naming no model, tokenizer, device or file. tacet-grammar implements it and depends on no inference crate, so you can take the guarantee without taking a GGUF loader with it.

cargo add tacet-grammar tacet-kernel
cargo run -p tacet-grammar --example no_engine

The example drives the automaton against a pretend runtime. The claim is checked from outside the checkout as well — a scratch crate that adds the two from crates.io, with cargo tree | grep -c tacet-engine at zero — because a decoupling claim verified only from inside the workspace is not verified.

# Where it arms, and therefore where it stops

The sentence used to read "invalid tool calls are impossible", and measuring it showed that was wider than the truth. The grammar arms after name(, so it says nothing about a call that never starts that way.

Running a real model over 115 cases, seven of the twenty-two failures were the right tool with the right arguments written in a shape nobody taught it: the call fenced inside a code block as tool read_document"path=report.md", or wrapped in <tool_call> read_document (path: "x") </tool_call>. Those are recovered now, by a layer that will only look behind a marker no prose contains. The underlying gap is real and is written down rather than papered over.

# A valid call also has to end

That is a second property, weaker than the first, and until recently not held at all: a valid prefix could wander forever. A model wrote a complete, correct calendar(...) call and then emitted whitespace for twelve minutes, because whitespace was legal at a structural position and legal again immediately.

Unrepresentable-invalid and always-terminating are different claims. The grammar now bounds consecutive whitespace and the length of a field the schema leaves open, and the engine caps a constrained generation at 2048 tokens, measured against a largest observed legitimate call of 1523.

# Reading the grammar for a tool

tacet grammar --tool calculate
tacet grammar --tool calculate --try-input 'calculate({"expression":"125*8"})'

The second form runs a candidate string against the automaton and says where it would have been refused, which is the fastest way to understand why a shape you expected to work does not.

# What it is worth

tacet bench gap runs the same calls twice, with the automaton on and off. Same prompt, same sampler, both columns capped at 256 tokens, so the mask is the only thing that differs.

Valid-if-started reaching exactly 100% is the front-page claim, measured. Without the automaton a 4B writes a malformed call one time in five and a 0.6B almost one in two; with it, neither ever does. The limit is just as clear: on the 4B the guarantee converts into correctness, 20.5 points of it, because when that model starts a call it usually had the right tool in mind. On the 0.6B the correct rate does not move at all, because the automaton fixes the syntax of a call to the wrong tool as faithfully as it fixes a right one. Valid is syntax, correct is judgement.

# One number is unexplained and left in

With the grammar on, the 0.6B starts fewer calls, 46% against 26%. It reproduces across Metal and CUDA, so it is not noise, and nobody knows why yet. It stays in the table because a result you cannot explain is still a result.