Use this before starting the workflow to check whether a spec's input set (`controlled_spec.md` / `deps.yaml` / `tests.md`) is sufficient and self-consistent to run `Spec -> Compile -> Generate -> Build -> Validate`. It detects missing required items, cross-file contradictions, ambiguous statements, unresolvable dependencies, and declared tests that cannot reach their `expected_outcome` as written, and reports them as proposals. It never modifies the spec.
Install
npx skillscat add seiya/atmofab/spec-input-check Install via the SkillsCat registry.
Spec Input Check
Purpose
Inspect the input set of a single spec (controlled_spec.md, deps.yaml, tests.md) and report whether the input is sufficient and self-consistent to start the core workflow, before any workflow phase runs. The output is a proposal that points out problems; this skill does not fix, complete, or rewrite the spec.
This skill is a pre-Compile advisory check. It is not a workflow phase, does not run inside the orchestration agent, and produces no workflow artifact (spec.ir.yaml / *_meta.json / verdict.json). It applies the principle "treat a shortage as an error and forbid implicit completion" (docs/CONTROLLED_SPEC.md) at the input boundary, so that a deficiency is surfaced before it stops a phase mid-run.
Scope
- the three input files of one target
specdirectory:spec/<spec_kind>/<domain>/<family>/<spec_id>/controlled_spec.mdspec/<spec_kind>/<domain>/<family>/<spec_id>/deps.yamlspec/<spec_kind>/<domain>/<family>/<spec_id>/tests.md
- the registry
spec/registry/spec_catalog.yaml, read-only, for registration and dependency-resolution checks. - the
deps.yamlof each declared dependencyspec, read-only, for resolvability checks.
Out of scope:
- modifying, completing, or reformatting any file (proposal only).
- judging physical / scientific validity (that is delegated to the
Validateexecution result). - the optional flows
Tune/Promote.
Canonical sources for the rules
This skill does not restate the spec format. The judgment rules are owned by:
docs/CONTROLLED_SPEC.md— required meta and required sections ofcontrolled_spec.mdperspec_kind, and the ambiguity-elimination rules.docs/TESTS.md— required meta, required sections, and coverage rules oftests.mdperspec_kind.docs/SPEC.md—spechierarchy, naming rules (including thespec_idlength bound),deps.yamldeclaration rules, and registry consistency.docs/GLOSSARY.md— the alloweddomain/familyclassification vocabulary, and thedeps.yamldeclaration vocabulary (component_id/profile_id; noinfrastructure_id— the harness is the target profile's).docs/workflow/phases/phase_01_compile.md— the node-identity preconditionsCompilecannot repair by re-authoring, so they must be caught here:spec_id≤ 55 characters, and noinfrastructuredependency declared indeps.yaml, on everyspecwhatever its kind (the harness is the target profile's,docs/SPEC.mdreq. 9; aprofileis checked at its adopter instead — check F.6). Also theinfrastructure§5 / §5.1 public-API pin, and the rule that the runner emits every numeric judgment already reduced to a field, so predicates do no arithmetic.docs/workflow/RUNNER_OUTPUT_CONTRACT.md— thediagnostics.json/perf.json/raw/shapes the runner emits, and theraw/metrics_basis.jsonper-(test_id,case_id) index.docs/workflow/CHECKS_MODULE_CONTRACT.md— what a metric is (one dotted address carries one scalar), and the rule that a cross-case reduction (a convergence order, a symmetry residual) is emitted as a per-case metric of the case where it first becomes computable, the earlier cases omitting it.tools/verdict_evaluator.py— the predicate DSL that decides each per-test verdict. This canonical source is code, not prose: it fixes how a predicaterefresolves (only thechecks/verdictheads are nested paths; every otherrefis a whole-string key of the case's flatmetricsmap) and which per-case container shapes are accepted.
When a check below and a canonical source disagree, the canonical source wins; report the divergence rather than guessing.
Input
- The target is given as a
spec_ref: either a spec directory path (spec/<spec_kind>/<domain>/<family>/<spec_id>/), a path to one of its files, or a barespec_idthat is resolved againstspec/registry/spec_catalog.yaml. - When the
spec_refcannot be resolved to exactly one spec directory, stop and report that as the first finding (do not proceed to other checks against a guessed directory).
Requirements (checks to perform)
Group findings by severity:
blocker— the workflow cannot start or a phase will stop withfail(missing file, missing required meta/section, cross-file contradiction, unresolvable dependency).warning— the input is likely to cause a downstreamfailor an ambiguous result (subjective wording, placeholder, missing unit/threshold, coverage gap).info— a non-blocking observation worth the author's attention.
A. File presence and structure
- All three files (
controlled_spec.md,deps.yaml,tests.md) exist at the resolved spec directory. A missing file is ablocker. Except aprofile, which has TWO files and notests.md(docs/SPEC.mdreq. 5, issue #175): nothing is generated or executed for aprofile, so atests.mdpresent there is ablockerin the other direction. deps.yamlparses as YAML;controlled_spec.md(andtests.md, where the kind has one) parse as Markdown with a readable meta block.- At most one
tests.mdexists for the spec (docs/SPEC.md: only 1 file per spec), and exactly one on every kind butprofile.
B. Meta information
controlled_spec.md §0states all ofspec_id,spec_version,status,spec_kind,domain,family. A missing field is ablocker.deps.yamlstatesspec_idandspec_kind.tests.md §0statestest_profile_id,test_profile_version,status, and thespec_reffields (spec_kind,spec_id,spec_version,controlled_spec_path). Skipped for aprofile, which has notests.md(A.1).spec_idmatches the form^[a-z][a-z0-9_]{2,63}$and is at most 55 characters (docs/SPEC.mdreq. 4). An over-lengthspec_idis ablocker, and one worth reporting first: the bound is enforced at spec-input, so the workflow rejects the target — and every member of a--with-depsclosure — before any phase runs, and no re-authoring of theIRor the source can repair it. Only a rename can, which also touches the directory,spec_catalog.yaml, and every dependent'sdeps.yaml. For acomponentspec, also check the recommended form<domain>_<family>_<operator>_<dim>d_<scheme>(recommendation →info, not ablocker).spec_kindis one ofproblem/component/profile/infrastructure(infrastructure= the R1 harness node kind).domain/familymatch the classification vocabulary indocs/GLOSSARY.md.
C. Cross-file consistency (contradictions)
Every check in this group that reads tests.md is SKIPPED for a profile, which has none (A.1) — C.1 and C.2 compare the two files it does have, C.3 and C.4 do not apply at all, and C.5 requires tests_path to be ABSENT from its catalog entry rather than to agree.
spec_idis identical acrosscontrolled_spec.md §0,deps.yaml, and — on every kind butprofile—tests.md(spec_ref.spec_id).spec_kindis identical across the three files (the two, for aprofile).tests.md spec_ref.spec_versionequalscontrolled_spec.md §0 spec_version. A mismatch is ablocker(the test profile targets a different spec version).tests.md spec_ref.controlled_spec_pathresolves to the actualcontrolled_spec.mdof this spec directory.spec/registry/spec_catalog.yamlregisters this spec, and itsspec_kind/spec_version/domain/family/controlled_spec_path/tests_path/deps_pathagree with the files. An unregistered spec, or any field mismatch, is ablocker(docs/SPEC.md: unregistered dependencies are not allowed). For aprofilethe entry carries NOtests_path, and one present there is the mismatch.- The directory path encodes the same
spec_kind/domain/family/spec_idas the meta declares.
D. controlled_spec.md required sections (per spec_kind)
Confirm every required section for the declared spec_kind exists and is non-empty, per docs/CONTROLLED_SPEC.md:
problem: sections 1–10 (Problem definition; Variables and coordinates; Domain and boundary-condition types; Dependentcomponentand adoptedprofile; Integration algorithm; Model parameters and runtime input contract; Prohibitions; Traceability; tests reference; AD preparation information).component: sections 1–9 (Responsibility and scope; input/output contract; Operation definition; Failure conditions and constraints; Public API and compatibility; Prohibitions; Traceability; tests reference; AD preparation information).profile: sections 1–5 (Targetcomponentand compatibility range; Application conditions; Parameter constraints; Fallback rules; Traceability). There is no tests-reference section — aprofilehas notests.md.infrastructure(R1 harness): sections 1–8 — thecomponentshape minus section 9 (AD preparation information), since a harness carries no physics: Responsibility and scope; input/output contract (including thediagnostics.json/perf.json/raw/*shapes it emits); Operation definition (the<spec_id>__*operations physics-node runners call); Failure conditions and constraints; Public API and compatibility; Prohibitions; Traceability; tests reference.
A missing required section is a blocker. A section present but empty or a stub is a warning.
The section numbers are load-bearing for an infrastructure spec — the Compile gate reads the published surface out of ## 5. and ### 5.1 by number — so check them literally, not just by title:
## 5.(Public API and compatibility) lists the publishedoperation_ids exhaustively ("the publishedoperation_ids are exactly: ...") and the published derived types, each as a backtick span carrying the<spec_id>__prefix.Compilepins theIR'spublic_apito this list by set equality, so a helper emitter that no test exercises but a consuming runner still calls must be listed here. An operation named in section 3 but absent from section 5 (or the reverse) is ablocker.### 5.1(Canonical interface block) exists as a subsection of section 5 and contains exactly one fenced code block, giving every published type and operation signature (argument names, order, types, ranks,intents,resultnames, derived-type component layouts) plus the module-levelparameterdeclarations the signatures reference. A missing### 5.1, a missing fence, or more than one fence inside### 5.1is ablocker— each failsCompileclosed.- The symbol set of
### 5.1equals the name lists of## 5.. A mismatch is ablocker. - Section 5.1 is what carries the signatures into the
IR, becauseGenerate.generatecannot readcontrolled_spec.md; treat a signature stated only in prose (section 3) and absent from the### 5.1fence as ablocker, not a stylistic gap. - Section 2 states which record component carries the
case_id, since themetrics_basis.jsonindex is keyed by (test_id,case_id). Absence is awarning.
E. tests.md required content (per spec_kind)
This whole group is SKIPPED for a profile, which has no tests.md (A.1). Do not report its absence here — A.1 owns that, and reporting it twice sends the author looking for two defects.
- The required sections of
docs/TESTS.md §Description format(0–8) exist; an unnecessary section statesN/Awith a reason rather than being omitted. - At least one
L0test is defined (docs/SPEC.mdreq. 13,docs/TESTS.md). Absence is ablocker. - Each test's judgment condition is stated per
node_keyand does not implicitly reference a dependencynode's state. - Coverage rules per
spec_kind:component: each publishedoperationhas at least one normal case and one guard case (fail/xfail).problem: execution control, case expansion, judgment expressions, and pass/fail aggregation rules are defined; a non-applicable validity item definesN/Aandreason_na.infrastructure(R1 harness): each published harness operation has at least one normal case and one guard case (fail/xfail) — e.g. numeric-round-trip, boolean-literal, case fan-out → per-case snapshot naming, missing---casesguard, per-test index completeness.
- Every
xfaildefines bothxfail_conditionandpass_when. - Where
tests.mdnames case identifiers literally (rather than deriving them from a sweep rule), each must survive theCompilecase gate: at most 64 characters, matching[A-Za-z0-9._][A-Za-z0-9._-]*(a leading-is refused: the id reaches the runner's argv), containing no.., and pairwise distinct (docs/workflow/phases/phase_01_compile.md). Acase_idis concatenated into the per-case snapshot path and rendered as a Fortranselect caselabel, so an over-long one is truncated until no label can ever match and every run aborts despite compiling cleanly. Report a violation as awarning, sinceCompile— nottests.md— fixes the finalcase_idset; state that the check applies only to the literally-named ids.
F. deps.yaml and dependency resolvability
deps.yamldeclares thedependenciesblock, whose keys are drawn from exactlycomponents/profiles. Both are required in everydeps.yaml, aninfrastructurespec's own included (there both are empty lists); empty lists are likewise valid for a leafcomponent, and for aproblemwhose wholecomponentset comes from an adoptedprofile. Aninfrastructure:key is refused by name (check 6). Any other key underdependenciesis ablocker— the closure build rejects the wholedeps.yamlas malformed, so a typo likecomponent:stops the run.- A
problemspec has a directcomponentset — declared in its owncomponents, selected by aprofileit adopts, or both (docs/SPEC.mdreq. 10). Aproblemwith NEITHER is ablocker. Acomponentthat appears in both places is also ablocker: acomponenthas exactly one source, and the closure resolver refuses the duplicate (profile_component_declared_twice). - Each declared
component_id/profile_idcarries aversion_constraint. - Each declared dependency is registered in
spec/registry/spec_catalog.yamlunder the matchingspec_kind, and its files exist on disk. An unregistered or missing dependency is ablocker(docs/SPEC.mdreq. 11). - Each dependency's catalog
spec_versionsatisfies the declaredversion_constraint. A violation is ablocker. (The harness version is the target profile'sharness.version_constraint, which the launch gate resolves; it is not adeps.yamlentry.) - No
infrastructureentry in anydeps.yaml, whatever the spec's kind (docs/SPEC.mdreq. 9). The harness is an attribute of the target profile (spec/targets/<target_id>.yamlharness), and the host adds the target's harness as a direct dependency of every non-infrastructurenode it builds for that target, so a node with a host-rendered runner (anM3cnode) needs no declaration. One or more entries is ablocker: the workflow rejects such a spec at spec-input, before any phase runs, and rejects it for every member of a--with-depsclosure, so a violating spec never reachesCompile. The two capture points emit different envelopes, so do not look for one literal string: a plain (no--with-deps) run rejects its target inside the conductor withspec-input rejected: infrastructure_dependency_declared_in_deps: …, while a--with-depsrun resolves the closure first and reports any member — the target included — as{"reason": "dependency_closure_unresolved", "reason_code": "infrastructure_dependency_declared_in_deps", …}(the violated rule is inreason_code, notreason). A--resumere-resolves the node through the same gate, so an already-started run cannot be resumed past the defect either; the remedy is to delete theinfrastructure:section and start a new run. Aprofileis the one case neither envelope applies to: it is not a run target and is expanded away before it is visited as a closure member, so an entry there is ablockerwhose refusal arrives one phase later, at the Compile start of every ADOPTING node, asprofile_declares_infrastructure. (Until R4-a PR-3, issue #284, the rule was the reverse — exactly one entry on every spec that builds,infra_dep_count_invalid— so an older spec that still carries aninfrastructure:section is exactly the shape this check refuses.) controlled_spec.md §4(for aproblem) names the sameprofile_ids thatdeps.yamldeclares, and thecomponent_ids of its direct set — thosedeps.yamldeclares directly PLUS those the adoptedprofile's owndeps.yamlselects — neither side referencing anidthe other omits. A discrepancy is ablocker(contradiction between the prose contract and the machine-readable dependency set).- For a
profilespec, thetarget component_idincontrolled_spec.md §1is exactly what its owndeps.yaml#componentsdeclares. Compatibility between an adoptedprofileand the components an adoptingproblemdeclares directly is the host resolver's job (profile_component_declared_twice/profile_component_conflict), not a prose check here (cross-spec consistency → report what is checkable from the given files; mark unverifiable itemsinfo). - No direct path reference / relative
importis used in place of adeps.yamldeclaration (docs/SPEC.mdreq. 9).
G. Ambiguity and insufficiency (forbid implicit completion)
- Flag subjective expressions that the spec format forbids: "appropriate", "sufficiently small", "as needed", "etc." used where a value or rule is required (
docs/CONTROLLED_SPEC.md §Ambiguity-elimination rules). →warning. - Flag unresolved placeholders:
TBD,TODO,<...>,???, blank required values. →blockerwhen in a required field, elsewarning. - Flag parameters stated without a unit, a numeric value, or an allowed range where the format requires them (model parameters, thresholds, default values). →
warning. - Flag a judgment threshold referenced in
tests.mdthat is not numerically defined. →blocker. - Flag any place that offers multiple options without a stated selection rule (priority or fixed value). →
warning. - Flag prose outside the
### 5.1subsection (its prose and its fenced block alike) that names how one implementation language binds, nests, scopes, stores or annotates a procedure or a datum — a nesting or scoping construct, a storage or association attribute, an execution-space qualifier, a compiler directive — rather than what the procedure or quantity reads and returns. AControlled Specis language-neutral throughout (docs/CONTROLLED_SPEC.md§Purpose), so such a statement either cannot be met on another target or is read as a requirement on how the source is bound rather than on what it computes; which words are such constructs is each language backend's knowledge, so this check judges the role of a word, not a list. The neutral signature vocabulary that document itself defines (type,kind,rank,intent, an explicit shape and itsdims, a procedure-typed argument and its prototype) is not such a construct, and its use in prose is not flagged. Remedy: state what the procedure or quantity reads and returns, and leave the construct that binds it to the language backend. →warning.
H. Executability of the declared tests
Group G asks whether a statement is ambiguous. This group asks a different question: whether the tests tests.md declares can execute and decide at all when sections 2–5 are executed exactly as written. A defect here is a blocker, not a warning: it does not risk a downstream fail, it guarantees one, and no leaf can repair it by re-authoring — the input itself makes the declared outcome unreachable. A tests.md that is structurally complete and free of ambiguity can still carry such a defect and fail every attempt, so this group runs even when groups A–G are clean.
No dangling case dimension. Every parameter the case-expansion rules sweep or fix (§4) is consumed by a rule in the input-defaulting rules (§2), the execution-control rules (§3), or the diagnostics contract (§5). A swept parameter that no rule reads is a
blocker: the cases it distinguishes are numerically identical, so every test that depends on the distinction is decided on the wrong data. Conversely, a rule referencing a parameter that §4 never fixes is ablocker(the leaf must invent its value).- The failure is silent in every other check group: the parameter is present, spelled correctly, carries a numeric value, is encoded in the
case_id, and is named in a judgment — it is simply never applied. Trace each parameter from §4 to its point of use, and report the ones with no point of use. - The same holds for each runtime input
controlled_spec.md§6 requires: an input that no statement ofcontrolled_spec.md(its algorithm included) and no rule, test or metric oftests.mdreads is ablocker, because Compile V9 demands a route for it and there is none to give, so the leaf invents one and the reviewer judges the invention both ways. A provenance input is exempt, as it is from V9. Recorded instance: issue #401,output_schedule.
- The failure is silent in every other check group: the parameter is present, spelled correctly, carries a numeric value, is encoded in the
Every test can reach its
expected_outcome. For eachtest_id, confirm a path exists from the case-expansion rules to the declared outcome.- For an
xfail, some case parameter must makexfail_conditiontrue. Anxfailwhose condition no case-expansion parameter forces is ablocker— the test can never satisfyxfail_rule, sosuite.pass_rulecan never hold. - For a
pass, the judged metric must be computable for every target case (see H.3), and a threshold must not be contradicted by the case's own parameters. - A quantity a judgment reads that the runner itself supplies — a
perf.jsonfield, a writer argument, not a captured state variable — and that no rule oftests.md§2–§5 or ofcontrolled_spec.mdfixes is ablockerwhen some value the inputs admit makes the judgment undefined (a division by it or by a value derived from it, a logarithm of it): the leaf chooses the value, and the outcome follows the choice. Recorded instance: issue #394, the harness self-test'scells_updatedunder a residual divided by the throughput.
- For an
Every judged metric resolves to a declared diagnostics field. A predicate does no arithmetic (
phase_01_compile.md;verdict_evaluator._resolve_predicate_ref), so every metric name a judgment references must be carried by a field the diagnostics contract declares. A judged metric that exists only as a formula — one the runner would have to reduce under an address the spec never declares — is ablocker; the predicate resolves to a structural absence and the test fails on shape, not on physics.- A derived metric (a drift ratio, a convergence order, a symmetry residual) is not exempt: it is emitted under its own field address, already reduced to a scalar. State that address in the diagnostics contract.
- A cross-case reduction is a per-case field of the case where it first becomes computable (
CHECKS_MODULE_CONTRACT.md); state which case carries it, and over which cases it accumulates. An accumulator whose scope is unstated can be poisoned by an unrelated case that happens to share the sweep key. - A metric emitted only for some cases (a pair residual, an analytic error valid only under one profile) states its
N/Arule and which case slice carries the value. Absence is ablocker, because the evaluator must otherwise guess the slice. - An array-valued field cannot be a metric (one address carries one scalar). Report a declared field that is a time series or a vector.
- The cross-target judgment is the one exception (
docs/TESTS.md§Cross-target judgment).cross_target_state_agreementis evaluated by the host from the captured state against another target's run, never emitted by the runner, so it has no diagnostics field by design and is not reported here. Check instead that §5 defines it, that the judgment names the state variables it compares and a finite threshold, and that noxfailtest applies it. - Precedence over Operations Rule 8. When the certified sibling carries the identical construct and certified with it, the pipeline demonstrably tolerates the construct —
Compileresolves the address from the prose. Report it as awarningthat names the inference the author can remove, not as ablocker. Reserveblockerfor a construct with no certified precedent, or one the numbers prove unresolvable. H.1 and H.2 admit no such precedence: a dangling case dimension and an unreachable outcome are proved from the input set alone.
Every judged quantity has a primary-evidence path. For each metric a §6 judgment references, decide from its §5 definition whether a captured state variable (
docs/TESTS.mdrequirement 9 defines the term) enters it. If none does — the value is fixed by the §2-§4 inputs, the constants and the §3 time step alone (a CFL number over a prescribed speed) — §5 must carry the primary-evidence statementdocs/TESTS.mdrequirement 9 requires. Its absence is ablocker:Compile.generatecannot author aprimary_predicatesentry that both reads the state and transcribes the definition (phase_01_compile.md, theprimary_predicatesrule of the schema block and V3 (ii)), so the run ends atCompile(phase_01_compile.md§1-1). The absence is read offtests.mdwith no computation, and what makes it fatal is the leaf-read contract, which no deterministic gate implements; so thisblockeris the one exception Operations Rules 7 and 9 and the Decision Criteria name, and it needs neither a number nor an implementation behind it. Rule 7 still applies to evaluating a statement that is present (below).- Evaluate the statement numerically under Operations Rule 7: its state term must sit inside the threshold in every
passcase. For eachxfailcase, state whether the state term stays inside (the guard then leaves no state fact and is decided by the input term), and confirm the statement says so. - A metric that a captured state variable enters (a CFL number over a wave speed the state carries, a mass drift, a step count tests.md declares a state variable of the case) needs no statement. A snapshot variable that only echoes an input-fixed value (a certified sibling IR's
dt) does not count. Thexfail_conditionof a guard test over the inputs (nx < 2,dt <= 0) is not a judged quantity and is outside this item: the IR's corroborant for it is the state fact the guard leaves behind, whichCompilewrites whether or not §6 spells it out. - H.4 admits no precedence under Operations Rule 8 either. A certified sibling IR that carries a state read for such a quantity shows only that a reviewer passed it:
Compile.verifyV3 (ii) names those forms (a cell count padded with a state read, a bound the leaf added) as non-transcriptions.
- Evaluate the statement numerically under Operations Rule 7: its state term must sit inside the threshold in every
Operations Rules
- Read-only operation. Use the
Readtool,grep, YAML/Markdown parsing, and local computation for inspection only. Do not callEdit/Writeon any spec file, registry, or workspace artifact. Do not runtools/run_workflow.pyor any workflow phase. - Resolve the target spec directory first (see Input). If resolution is ambiguous or fails, report only that and stop.
- Run the checks A–H in order. Continue through all groups even after the first finding, so the author gets a complete list in one pass.
- This check is heuristic for the Markdown-prose parts (sections D, E, G): a section or rule expressed in unusual wording may be miscounted. State assumptions, and prefer reporting a
warning"could not confirm X" over silently passing or silently failing. - Do not invent or assume default values for a missing item. A missing required item is reported as a deficiency, never completed.
- The output is advisory. Do not claim the spec "passed the workflow" or "is ready to merge"; state only that the input check found / did not find the listed problems.
- Evaluate group H numerically whenever the input set fixes the constants it needs. When the
specset fixes the physical constants, the discretization, and the thresholds, do not reason about reachability in prose — compute it. Derive each case's parameters through the §3 procedure exactly as written, evaluate each judgment against its threshold, and report the resulting value. A dangling case dimension is proved by two cases that differ in the sweep and agree in every judged metric; an unreachablexfailis proved by its condition evaluating false. A runner-supplied quantity of H.2 that the inputs leave open is evaluated at every value they admit, the boundary value (zero) included. A group-H finding backed by a number is ablocker; the same suspicion unbacked is awarningstating what could not be computed. The exception is H.4's missing primary-evidence statement, ablockerthat states the quantity and needs no number. - Diff against the certified sibling. When a
specof the samespec_kindand comparable structure has already been certified (its artifacts exist underworkspace/ir/), read its input set and compare construct by construct. It is the canonical evidence of what the pipeline accepts: a construct that deviates from it warrants a finding, and a construct identical to it is evidence that the construct is tolerated, so do not report the certified idiom as a defect. Where the target must deviate (a different normalizer, a different case topology), state the reason the sibling's form does not transfer. A certified sibling'sprimary_predicatesentry for a quantity no state variable enters is not such evidence (H.4). - Verify a claim about runtime behavior against the code that implements it, never against prose alone. Before reporting a
blockerthat rests on how a phase, a gate, or the predicate evaluator behaves, read that implementation (tools/verdict_evaluator.py,tools/host_render.pyand the language backend it dispatches to,tools/validate_pipeline_semantics.py). Prose documents state requirements, not the full set of accepted shapes; ablockerinferred from a document's silence is a false positive waiting to happen. If the implementation cannot be located, downgrade to awarningthat names the unverified assumption. H.4's missing primary-evidence statement is the exception: the behaviour it rests on isphase_01_compile.md§1-1, a contract the Compile leaf reads, and no code implements it.
Output format
Produce a single report with:
- A one-line summary: the resolved spec (
spec_id,spec_kind, path) and the count of findings by severity. - A
blockerlist, then awarninglist, then aninfolist. Each finding states: the file and location (section / line / key), what is missing or contradictory, the canonical-source rule it relates to, and a concrete proposed fix for the author to apply. - A closing note that this is a proposal only and no file was modified.
When no findings exist, state that the input set passed all A–H checks and is structurally sufficient to start the workflow, while noting that physical validity is still decided at Validate. State which group-H checks were evaluated numerically and which could not be, so the author knows how far the "no findings" result was actually proved.
Decision Criteria
- A
blockercount of zero means the input set is structurally sufficient and self-consistent to startCompile; it does not assert physical correctness. - Any
blockermeans the workflow should not be started until the author resolves it. - A group-H
blockeris a proof, not a risk estimate: it states the value a judgment takes and the outcome that value forecloses (H.4's missing primary-evidence statement states instead the quantity that has none, and the Compile fail that forecloses the run). A structurally complete, fully unambiguous input set can still carry one, so a clean A–G result is not a substitute for running group H. - Every finding cites the file location and the canonical-source rule, so the author can verify the basis independently.
- No spec, registry, or workspace file was written or modified during the check.