Docs / Guides

contract corpus · 00-corpus.md · guide · card

Corpus law

The problem a corpus solves

Contributors build and test code against this specification, so a reader needs to find each obligation, know why it holds and see whether code meets it. Corpus law is the grammar that lets contextful-spec lint answer those questions; the corpus states no rule the checker leaves unenforced.

One clause, followed through

The example adds an error case, a condition returning a named error, to the store’s compaction operation fold.

A contract, such as store, owns one or more numbered files. Each file holds one ## section per operation, and a one-paragraph lede opens the section to say what the operation covers (ledecorpus.anatomy.ledeAn operation section opens with a lede: one paragraph stating what the operation covers. The lede is the operation's only description; its fragment entry carries no gloss.). The author writes one list item under ## fold: a backticked subject, partial-snapshot, then a statement of at most 40 words (statement-wordscorpus.anatomy.statement-wordsA clause statement holds at most 40 words, a {{id}} reference counting as one.).

The item’s address joins contract, operation and subject into store.fold.partial-snapshotstore.fold.partial-snapshotA reader observes a snapshot and every declared sidecar together or neither; a commit exposing one without the other raises StorePartialSnapshot. (clause-idcorpus.address.clause-idA clause id is three dot-separated segments — contract, operation, subject — each matching [a-z0-9-]+. A clause item writes the subject alone; its file and section supply the rest.). Tests, proofs and other clauses use that address, and splitting the file renames nothing.

The statement names the error, so the author registers the error in the contract’s registry fragment, spec/terms/store.toml, against this one clause (fragmentcorpus.registry.fragmentEach contract owns spec/terms/<contract>.toml, holding its operations, and its errors and named bounds each with a gloss.). A second clause that needs the same condition writes the clause id between double braces instead of restating it (pointercorpus.reference.pointer{{<clause id>}} is the one way a statement reaches a fact another clause owns. The lock file records every pointer as an edge.).

An indented italic line under the item carries its Why: a because of at most 30 words (why-cellcorpus.rationale.why-cellA clause's Why is absent, one or more record ids such as P3, A-store or A-topology#commit-lock, or because followed by at most 30 words stating the deciding criterion. A refusal carries a Why.), or a record id. Records under spec/adr/ hold the principles P1 to P8 and one decision file per contract, such as A-store, with the options each decision rejected.

Nobody labels the kind of a clause. The statement names a registered error, so the checker computes the kind refusal. A clause owning a bound is a limit, and every other clause is behavior (kind-is-computedcorpus.anatomy.kind-is-computedA clause is a refusal when its statement names an error its fragment assigns to it, a limit when its fragment assigns it a named bound, and a behavior otherwise. The checker writes the kind into spec/spec.lock.json.).

When the clause breaks a rule

Suppose a second clause also names the error. The checker raises a registry finding, because one error belongs to exactly one clause (one-error-one-clausecorpus.registry.one-error-one-clauseAn error entry names the one clause raising it. That clause's statement names the error, and no other clause statement does; a second site reaches the condition by {{id}}.). Suppose the statement carries a calendar date. The date fails lint, because no authored file states a date or a build state (dated-prosecorpus.render.dated-proseThe words planned, not yet, currently, today, shipped, implemented, previously, used to, legacy, TODO, FIXME and WIP, and an ISO date, raise SpecDatedProse in any authored file.).

Computed build state

contextful-spec state lists the new clause as committed and adds the error to the generated store card (cardcorpus.render.cardcontextful-spec state renders spec/cards/<contract>.md per contract: each operation with its lede and clause count, each refusal as error and gloss, each bound as value, unit and basis, all naming their clause.). A test tagged with the clause id and a digest of the statement supplies a pin (tag-pincorpus.state.tag-pinA line // spec: <id>@<rev> among the comments and attributes above a test function under crates/ or tools/ pins clause <id> to that test; <rev> is the first 8 hex digits of the statement's SHA-256., pincorpus.state.pinspec/pins.toml maps a clause id to one artifact: a test function path, a theorem constant under formal/ or an item path. A refusal or a limit takes a test or a theorem.).

An ignored test, an unfinished body or a stale tag computes broken (verdictcorpus.state.verdictAn unpinned clause computes committed; a pinned clause computes performed when its Rust, Lean or typescript-tag-pin artifact qualifies, and broken otherwise. A test carrying an #[ignore] attribute computes broken.). A reworded statement leaves the tag stale until someone checks the test against the new wording (stale-pincorpus.state.stale-pinA tag whose <rev> differs from the digest of its clause's current statement raises SpecStalePin, and its clause computes broken.).

Diagrams, targets and guides

A diagram is a fenced Mermaid block with one shape per kind of thing. Stores are cylinders, and a question is a decision with a labelled exit per outcome (shapecorpus.diagram.shapeA node labelled with a snake_case identifier or a phrase ending table, store, log or queue is a cylinder [( )], and a label ending ? is a decision { }. A breach raises SpecDiagramShape.). A deployment target file under spec/targets/ names the provider primitive filling each role, and the checker refuses a shape that leaves a role unfilled (incompletecorpus.targets.incompleteA shape leaving a role unfilled, or a target file marking other than one default shape, raises SpecTargetIncomplete, naming the provider, the shape and the role.).

Each contract has three views. The contract file is reference, and the checker generates the card from the fragment. The guide teaches the flow (filecorpus.guide.fileEach contract has one guide, spec/guide/<contract>.md: front matter contract, one # title equal to the contract's registry title, then prose outside diagrams of at most 400 words plus 20 words per operation its contract's fragment registers.) and reaches each rule only by pointer, so the contract file stays the only place stating a rule (non-normativecorpus.guide.non-normativeA guide holds no clause item and names no registered error. It reaches a rule by {{<clause id>}} and an operation by {{<contract>.<operation>}}, which resolves against that contract's fragment. No contract file links a guide.).

A guide reaches every operation of its contract (reachcorpus.guide.reachEach operation a contract's fragment registers appears in the contract's guide as an operation pointer or a pointer to one of its clauses; an operation the guide misses raises SpecGuideReach, naming it.). Each paragraph carries prose between its pointers, so a guide stays more than an index (pointer-densitycorpus.guide.pointer-densityA guide paragraph, list item or table row holds at most 3 pointers to clauses and at least 8 words of prose per clause pointer; a denser one raises SpecGuidePointerDensity.). A number equal to a bound value travels with that bound’s pointer (boundcorpus.guide.boundA guide sentence holding a number equal to a bound value in its contract's fragment also holds the pointer to a clause owning a bound of that value; a sentence without one raises SpecGuideBound.).

A question that spans contracts gets a topic page under spec/topics/: at most 600 words that point at the clauses answering it (filecorpus.topic.fileA topic page spec/topics/<slug>.md carries front matter topic, one # title equal to its entry's title in spec/terms/topic.toml, then prose of at most 600 words outside diagrams.).

The spec cites no literature; references/ points into the spec instead (no-literaturecorpus.reference.no-literatureA spec file carries no hyperlink to an external document and no path under references/; either raises SpecExternalLink. Literature lives in references/, which cites clause ids.).

contextful-spec slice store.fold packs one operation for an implementer: its lede and clauses, the clauses they reach, the cited records, and the errors and bounds they own.