Semantic Quota Constraints for Specification-Faithful Structured Generation

Grammar-constrained decoding guarantees syntax, not semantics: a valid program can still violate explicit quantitative requirements in its prompt. We study a decode-time quota layer for a synthetic AST-synthesis DSL. The layer tracks required counts and operators against the same parser state used by the grammar, adds no parameters, and is model-agnostic. For the implemented finite grammar we prove soundness (Theorem 1: any terminating rollout satisfies every parsed requirement) and certified termination (Theorem 2: a mechanically computed per-prompt bound for conforming rollouts). A seed-42 transformer attains 99.4% All-req on all 1,000 IID-test prompts; the full layer reaches 100.0% across seeds 42/43/44 on a 200-prompt sample; a frozen 0.49B LLM host reaches 66.5%. As an external-validity probe, 691/952 SchemaStore documents contain a cardinality keyword, and a scoped adapter closes all four isolated required/minProperties gaps under a pinned constrained decoder.