The host reasons about grammarless packages in two states no manifest can produce — Manifest.grammar is not Option #227
Labels
No labels
code-review
correctness
dos
performance
security
severity/high
severity/low
severity/medium
tech-debt
Kind/Breaking
Kind/Bug
Kind/Documentation
Kind/Enhancement
Kind/Feature
Kind/Security
Kind/Testing
Priority
Critical
Priority
High
Priority
Low
Priority
Medium
Reviewed
Confirmed
Reviewed
Duplicate
Reviewed
Invalid
Reviewed
Won't Fix
Status
Abandoned
Status
Blocked
Status
Need More Info
No milestone
No project
No assignees
1 participant
Notifications
Due date
No due date set.
Dependencies
No dependencies set
Reference
h-dv/code-index#227
Loading…
Reference in a new issue
No description provided.
Delete branch "%!s()"
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?
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:The host has two first-class states for it, in
crates/plugin-host/src/worker.rs:60-78:NoGrammaris constructed at three sites (:156,:231, and theNonearm), andClaimedWithoutGrammarcarries a reasoned reversal of an earlier design explaining why it is deliberately not refused — including an argument about construction order inmain.rs.And no manifest can reach any of it.
crates/package/src/manifest.rs:118:Not
Option<Grammar>. Every package must declare a grammar, sotree_lenis never zero in production,NoGrammaris only reachable through internal construction, andClaimedWithoutGrammar'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 cost of leaving it is the ordinary cost of unreachable reasoned code: the next person to touch
KindTableStatuswill 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
ClaimedWithoutGrammarrationale 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 exercisestree_len == 0end to end — the ABI guarantee is currently untested because nothing can produce the input.NoGrammarandClaimedWithoutGrammarthen 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
KindTableStatusvariant 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
grammaroptional 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).ClaimedWithoutGrammarwhile leaving the guide paragraph → a test pinning the guide's ABI claims to the host's states must go RED.Provenance note
The reporter first cited this as "the guest ABI supports
tree_len == 0but no manifest can express it", which I could not confirm — my grep covered_prdoc/specs/andcrates/guestand 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.REFUTED in its conclusion, with the counterexample pinned — but the vocabulary WAS rotten, and that is fixed in
31cad14What the issue got right
No manifest can declare no grammar.
Manifest.grammaris notOption, andmanifest_schema.rs'severy_required_field_is_requiredalready grades removal of the whole[grammar]table and demandsmanifest.missing_field. Confirmed.The honest answer to the issue's "show
Manifest::validaterefuses it" turns out to be that it never gets that far: serde refuses at deserialization, one step earlier and stronger than validation. Pinned asa_manifest_cannot_declare_no_grammar(kind_table_guard.rs:641), with mutation M9 — adding#[serde(default)]+DefaultonGrammar— going RED (left: PackagePathUnsafevsright: 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:125callsGuestRuntime::loadwith grammarNone, and only thenattach_grammarat:147. Every package traversesNoGrammarorClaimedWithoutGrammaron the shipped two-step path. And every first-party package traversesClaimedWithoutGrammarspecifically, because the guest build scripts inject a kind-table digest:Verified independently in the tree before acting on the refutation.
So refusing at
ClaimedWithoutGrammar— which is what deleting the variant means — would exitEXIT_KIND_TABLE_MISMATCHon 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.grammarfield, and_prdoc/guides/80-extractor-abi.md:43all 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#227section;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 fiveKindTableStatusstates from real.cips that went throughManifest::from_container, on the shipped two-step path, compared for set equality againstALL_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_grammarhalf) → RED, missingNotClaimed/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_guardpass 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.
plugin enablefails on a project holding ONLY files the package claims — the package's own grant is minted while the build runs, so the gate admits nothing #233