The host reasons about grammarless packages in two states no manifest can produce — Manifest.grammar is not Option #227

Closed
opened 2026-09-08 15:54:54 +02:00 by buildagent · 1 comment
Member

Reported by an external package author (the TimeLine plugin team) while building a second package against our manifest. They have no stake in the outcome — their package ships a grammar — and filed it because "a state the host reasons about and no input can produce is the kind of thing that rots." I verified every part below in the tree at ea74dbc.

The contradiction

The ABI defines behaviour for a grammarless package. _prdoc/guides/80-extractor-abi.md:43:

tree_len is ZERO when the package declares no grammar. An extractor that wants a tree and is given none sees a length of nothing rather than a pointer into somebody else's bytes.

The host has two first-class states for it, in crates/plugin-host/src/worker.rs:60-78:

pub enum KindTableStatus {
    /// The package declares no grammar, so there are no ids to name and
    /// no claim to check. `tree_len` is zero for every request.
    NoGrammar,
    …
    /// The guest names a kind table and the package declares no
    /// grammar, so there is nothing to hold it against.
    ///
    /// NOT REFUSED, and the reason is worth stating because refusing
    /// was the first design. This guest is handed `tree_len` of zero on
    /// every request, so its compiled-in ids are never used and no fact
    /// it emits can be wrong BECAUSE OF THEM …
    ClaimedWithoutGrammar,
}

NoGrammar is constructed at three sites (:156, :231, and the None arm), and ClaimedWithoutGrammar carries a reasoned reversal of an earlier design explaining why it is deliberately not refused — including an argument about construction order in main.rs.

And no manifest can reach any of it. crates/package/src/manifest.rs:118:

pub grammar: Grammar,

Not Option<Grammar>. Every package must declare a grammar, so tree_len is never zero in production, NoGrammar is only reachable through internal construction, and ClaimedWithoutGrammar's carefully argued non-refusal can never fire.

Why this is worth fixing rather than leaving

One of the two layers is dead, and it is not obvious which. Either:

  • the manifest is wrong — grammarless packages are a legitimate shape (a pure-text extractor, a metadata claimant) that the host already supports and the manifest forbids by accident; or
  • the host is wrong — grammarless packages were designed out, and two enum variants, three construction sites, a paragraph of design rationale and an ABI guarantee are dead code that will be maintained forever by readers who assume they matter.

The cost of leaving it is the ordinary cost of unreachable reasoned code: the next person to touch KindTableStatus will preserve behaviour that cannot occur, and the next person to read the ABI guide will design against a guarantee they cannot use. That is what the reporter meant by "rots".

I do not know which way it should go, and that is the point of filing rather than fixing. Deciding needs someone who knows whether a grammarless package was ever intended — the ClaimedWithoutGrammar rationale reads like it was.

What a fix must do, whichever direction

If grammarless packages are legitimate: make the field Option<Grammar>, and add a fixture that actually exercises tree_len == 0 end to end — the ABI guarantee is currently untested because nothing can produce the input. NoGrammar and ClaimedWithoutGrammar then need their own graded cases.

If they are not: delete both variants and their construction sites, delete the guide paragraph, and say in the manifest why a grammar is mandatory. A reader should not be able to find a documented behaviour the product refuses to allow.

Either way, add the gate that would have caught this: a test asserting that every KindTableStatus variant is reachable from some manifest, not merely from some constructor. That is the generic form of the defect — a state machine whose inputs are narrower than its states.

Mutations

  • Make grammar optional but ship no grammarless fixture → the reachability test must go RED (a variant reachable in principle but exercised by nothing is the same defect one step along).
  • Delete ClaimedWithoutGrammar while leaving the guide paragraph → a test pinning the guide's ABI claims to the host's states must go RED.
  • Keep both and change nothing → the reachability test must go RED today, on the current tree. If it passes as written, it is not measuring reachability from a manifest.

Provenance note

The reporter first cited this as "the guest ABI supports tree_len == 0 but no manifest can express it", which I could not confirm — my grep covered _prdoc/specs/ and crates/guest and missed _prdoc/guides/. They then pointed at the host code instead, which is the stronger evidence and reframed the issue from "a documentation inconsistency" into "two enum variants nothing can construct". Worth recording because the second framing is the one that makes it actionable.

Reported by an external package author (the TimeLine plugin team) while building a second package against our manifest. They have no stake in the outcome — their package ships a grammar — and filed it because "a state the host reasons about and no input can produce is the kind of thing that rots." I verified every part below in the tree at `ea74dbc`. ## The contradiction **The ABI defines behaviour for a grammarless package.** `_prdoc/guides/80-extractor-abi.md:43`: > `tree_len` is **ZERO** when the package declares no grammar. An extractor that wants a tree and is given none sees a length of nothing rather than a pointer into somebody else's bytes. **The host has two first-class states for it**, in `crates/plugin-host/src/worker.rs:60-78`: ```rust pub enum KindTableStatus { /// The package declares no grammar, so there are no ids to name and /// no claim to check. `tree_len` is zero for every request. NoGrammar, … /// The guest names a kind table and the package declares no /// grammar, so there is nothing to hold it against. /// /// NOT REFUSED, and the reason is worth stating because refusing /// was the first design. This guest is handed `tree_len` of zero on /// every request, so its compiled-in ids are never used and no fact /// it emits can be wrong BECAUSE OF THEM … ClaimedWithoutGrammar, } ``` `NoGrammar` is constructed at three sites (`:156`, `:231`, and the `None` arm), and `ClaimedWithoutGrammar` carries a *reasoned reversal of an earlier design* explaining why it is deliberately not refused — including an argument about construction order in `main.rs`. **And no manifest can reach any of it.** `crates/package/src/manifest.rs:118`: ```rust pub grammar: Grammar, ``` Not `Option<Grammar>`. Every package must declare a grammar, so `tree_len` is never zero in production, `NoGrammar` is only reachable through internal construction, and `ClaimedWithoutGrammar`'s carefully argued non-refusal can never fire. ## Why this is worth fixing rather than leaving One of the two layers is dead, and it is not obvious which. Either: * **the manifest is wrong** — grammarless packages are a legitimate shape (a pure-text extractor, a metadata claimant) that the host already supports and the manifest forbids by accident; or * **the host is wrong** — grammarless packages were designed out, and two enum variants, three construction sites, a paragraph of design rationale and an ABI guarantee are dead code that will be maintained forever by readers who assume they matter. The cost of leaving it is the ordinary cost of unreachable reasoned code: the next person to touch `KindTableStatus` will preserve behaviour that cannot occur, and the next person to read the ABI guide will design against a guarantee they cannot use. That is what the reporter meant by "rots". **I do not know which way it should go**, and that is the point of filing rather than fixing. Deciding needs someone who knows whether a grammarless package was ever intended — the `ClaimedWithoutGrammar` rationale reads like it was. ## What a fix must do, whichever direction **If grammarless packages are legitimate**: make the field `Option<Grammar>`, and add a fixture that actually exercises `tree_len == 0` end to end — the ABI guarantee is currently untested because nothing can produce the input. `NoGrammar` and `ClaimedWithoutGrammar` then need their own graded cases. **If they are not**: delete both variants and their construction sites, delete the guide paragraph, and say in the manifest why a grammar is mandatory. A reader should not be able to find a documented behaviour the product refuses to allow. Either way, add the gate that would have caught this: a test asserting that every `KindTableStatus` variant is reachable from some *manifest*, not merely from some constructor. That is the generic form of the defect — a state machine whose inputs are narrower than its states. ## Mutations * Make `grammar` optional but ship no grammarless fixture → the reachability test must go RED (a variant reachable in principle but exercised by nothing is the same defect one step along). * Delete `ClaimedWithoutGrammar` while leaving the guide paragraph → a test pinning the guide's ABI claims to the host's states must go RED. * Keep both and change nothing → the reachability test must go RED today, on the current tree. If it passes as written, it is not measuring reachability from a manifest. ## Provenance note The reporter first cited this as "the guest ABI supports `tree_len == 0` but no manifest can express it", which I could not confirm — my grep covered `_prdoc/specs/` and `crates/guest` and missed `_prdoc/guides/`. They then pointed at the host code instead, which is the stronger evidence and reframed the issue from "a documentation inconsistency" into "two enum variants nothing can construct". Worth recording because the second framing is the one that makes it actionable.
Author
Member

REFUTED in its conclusion, with the counterexample pinned — but the vocabulary WAS rotten, and that is fixed in 31cad14

What the issue got right

No manifest can declare no grammar. Manifest.grammar is not Option, and manifest_schema.rs's every_required_field_is_required already grades removal of the whole [grammar] table and demands manifest.missing_field. Confirmed.

The honest answer to the issue's "show Manifest::validate refuses it" turns out to be that it never gets that far: serde refuses at deserialization, one step earlier and stronger than validation. Pinned as a_manifest_cannot_declare_no_grammar (kind_table_guard.rs:641), with mutation M9 — adding #[serde(default)] + Default on Grammar — going RED (left: PackagePathUnsafe vs right: ManifestMissingField), and taking the pre-existing schema test red with it.

What it got wrong, and the measurement that shows it

The conclusion — that these are states no input can produce, and that ClaimedWithoutGrammar's non-refusal can therefore never fire — is false.

main.rs:125 calls GuestRuntime::load with grammar None, and only then attach_grammar at :147. Every package traverses NoGrammar or ClaimedWithoutGrammar on the shipped two-step path. And every first-party package traverses ClaimedWithoutGrammar specifically, because the guest build scripts inject a kind-table digest:

crates/guest/ruby/build.sh:175      --src-offset "$SRC_OFFSET" --kind-table-digest "$DIGEST"
crates/guest/timeline/build.sh:64   --src-offset "$SRC_OFFSET" --kind-table-digest "$DIGEST"

Verified independently in the tree before acting on the refutation.

So refusing at ClaimedWithoutGrammar — which is what deleting the variant means — would exit EXIT_KIND_TABLE_MISMATCH on every first-party package, before the grammar it should be checked against has been read.

Mutation M7 is the measurement: replacing the worker's two-step load with a one-step load_with_grammar(Some(..)) reaches only [NotClaimed, Unreadable, Verified] — the two states this issue calls unreachable drop out precisely when you remove the two-step path that the shipped host actually uses. Had the issue been implemented as filed, the guard would have been deleted and the packages would have broken.

What was actually rotten: the names

Two variants, the GuestRuntime.grammar field, and _prdoc/guides/80-extractor-abi.md:43 all named a package state that cannot exist, rather than the runtime state that does. That is a real defect and it is what made the issue look correct. Fixed:

  • crates/plugin-host/src/worker.rs:54, 97, 122 — renamed to name the runtime state, with an enum-level #227 section;
  • crates/package/src/manifest.rs:141 — says why a grammar is mandatory and what that means for the host's states;
  • 80-extractor-abi.md:43 — corrected, with a "do not design against this" note so the next reader does not refile this.

The gate the issue asked for, built to be non-vacuous

every_kind_table_state_is_reachable_from_a_manifest (kind_table_guard.rs:564) drives all five KindTableStatus states from real .cips that went through Manifest::from_container, on the shipped two-step path, compared for set equality against ALL_STATUSES (:531) — so a state nothing reaches fails, and a demanded state that no longer exists fails too. status_name (:517) has no _ arm, so a sixth variant cannot compile without being named.

Mutations: M6 (drop the attach_grammar half) → RED, missing NotClaimed/Verified. M7 as above. M8 (demand a name no variant produces) → RED on set inequality.

Closing as refuted-and-corrected

The unreachable-state claim is wrong and the counterexample is now a test, so it cannot be quietly re-implemented. The naming defect underneath it is fixed. Verified: 14 tests in kind_table_guard pass on an independent run.

Related: #230, fixed in the same commit — the two share a property (a surface's state space must equal what its inputs can produce) broken in opposite directions, which is why one mechanism could not serve both.

## REFUTED in its conclusion, with the counterexample pinned — but the vocabulary WAS rotten, and that is fixed in `31cad14` ### What the issue got right **No manifest can declare no grammar.** `Manifest.grammar` is not `Option`, and `manifest_schema.rs`'s `every_required_field_is_required` already grades removal of the whole `[grammar]` table and demands `manifest.missing_field`. Confirmed. The honest answer to the issue's *"show `Manifest::validate` refuses it"* turns out to be that **it never gets that far**: serde refuses at deserialization, one step earlier and stronger than validation. Pinned as `a_manifest_cannot_declare_no_grammar` (`kind_table_guard.rs:641`), with mutation **M9** — adding `#[serde(default)]` + `Default` on `Grammar` — going RED (`left: PackagePathUnsafe` vs `right: ManifestMissingField`), and taking the pre-existing schema test red with it. ### What it got wrong, and the measurement that shows it The conclusion — that these are states *no input can produce*, and that `ClaimedWithoutGrammar`'s non-refusal can therefore never fire — **is false.** `main.rs:125` calls `GuestRuntime::load` with grammar `None`, and only *then* `attach_grammar` at `:147`. **Every package traverses `NoGrammar` or `ClaimedWithoutGrammar` on the shipped two-step path.** And every first-party package traverses `ClaimedWithoutGrammar` specifically, because the guest build scripts inject a kind-table digest: ``` crates/guest/ruby/build.sh:175 --src-offset "$SRC_OFFSET" --kind-table-digest "$DIGEST" crates/guest/timeline/build.sh:64 --src-offset "$SRC_OFFSET" --kind-table-digest "$DIGEST" ``` Verified independently in the tree before acting on the refutation. So refusing at `ClaimedWithoutGrammar` — which is what deleting the variant means — would exit `EXIT_KIND_TABLE_MISMATCH` on **every first-party package**, *before the grammar it should be checked against has been read.* **Mutation M7 is the measurement:** replacing the worker's two-step load with a one-step `load_with_grammar(Some(..))` reaches only `[NotClaimed, Unreadable, Verified]` — the two states this issue calls unreachable drop out precisely when you remove the two-step path that the shipped host actually uses. Had the issue been implemented as filed, the guard would have been deleted and the packages would have broken. ### What was actually rotten: the names Two variants, the `GuestRuntime.grammar` field, and `_prdoc/guides/80-extractor-abi.md:43` all named a **package** state that cannot exist, rather than the **runtime** state that does. That is a real defect and it is what made the issue look correct. Fixed: * `crates/plugin-host/src/worker.rs:54, 97, 122` — renamed to name the runtime state, with an enum-level `#227` section; * `crates/package/src/manifest.rs:141` — says why a grammar is mandatory and what that means for the host's states; * `80-extractor-abi.md:43` — corrected, with a "do not design against this" note so the next reader does not refile this. ### The gate the issue asked for, built to be non-vacuous `every_kind_table_state_is_reachable_from_a_manifest` (`kind_table_guard.rs:564`) drives all five `KindTableStatus` states from real `.cip`s that went through `Manifest::from_container`, on the shipped two-step path, compared for **set equality** against `ALL_STATUSES` (`:531`) — so a state nothing reaches fails, *and* a demanded state that no longer exists fails too. `status_name` (`:517`) has no `_` arm, so a sixth variant cannot compile without being named. Mutations: **M6** (drop the `attach_grammar` half) → RED, missing `NotClaimed`/`Verified`. **M7** as above. **M8** (demand a name no variant produces) → RED on set inequality. ### Closing as refuted-and-corrected The unreachable-state claim is wrong and the counterexample is now a test, so it cannot be quietly re-implemented. The naming defect underneath it is fixed. Verified: 14 tests in `kind_table_guard` pass on an independent run. Related: #230, fixed in the same commit — the two share a *property* (a surface's state space must equal what its inputs can produce) broken in **opposite** directions, which is why one mechanism could not serve both.
Sign in to join this conversation.
No milestone
No project
No assignees
1 participant
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference
h-dv/code-index#227
No description provided.