From 5483e909b32272ee294e3518036479498af37902 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 8 Sep 2026 18:57:50 +0100 Subject: [PATCH 1/8] feat(deed): add the family-level DEED grammar specification Places the grammar spec that governs every .deed document, above the per-format satellites (meta-a2ml/, anchor-a2ml/, agentic-a2ml/) which specify individual documents within it. Contents: deed/spec/DEED-GRAMMAR-SPEC.adoc lexical structure, concrete syntax, the four document forms, identity semantics, the self-assertion rule, the proposed typing chapter, and the validator obligation deed/spec/abnf/deed.abnf the grammar in ABNF, normative for parsing deed/README.adoc family overview Owner rulings settled 2026-09-08 and encoded here: - praxis-deed is a genuine FOURTH head, alongside estate-deed, repo-deed and estate-atlas-deed. (This is not the earlier "tool-praxis-deed", which was another session's coinage and appears in no owner text.) - :schema-version is REQUIRED on every head. :registry-version survives as an optional additional field on estate-atlas-deed only, because it versions registry contents rather than the format. - RECORD-DIALECT-SPEC.adoc is SUPERSEDED, not withdrawn: kept as history with a superseded-by pointer. States plainly what the family is NOT. The description "TOML-like key-value data formats" in meta-a2ml/README.adoc is wrong and was load-bearing: measured across all 35,884 legacy .a2ml files, the descriptile family had drifted to 0.2% conformance (10 correct against 5,424 TOML-shaped) because tools read that sentence and generated what it described. The grammar has no "=" form and no "[section]" form. Four rulings remain open and are listed at the end of the specification. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01QNjWX2B4FffG7zqMBMui6v --- deed/README.adoc | 66 ++++ deed/spec/DEED-GRAMMAR-SPEC.adoc | 649 +++++++++++++++++++++++++++++++ deed/spec/abnf/deed.abnf | 48 +++ 3 files changed, 763 insertions(+) create mode 100644 deed/README.adoc create mode 100644 deed/spec/DEED-GRAMMAR-SPEC.adoc create mode 100644 deed/spec/abnf/deed.abnf diff --git a/deed/README.adoc b/deed/README.adoc new file mode 100644 index 00000000..a8894a85 --- /dev/null +++ b/deed/README.adoc @@ -0,0 +1,66 @@ +// SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) +// SPDX-License-Identifier: CC-BY-SA-4.0 += DEED — the format family +:toc: left +:toclevels: 2 + +*DEED* is the attestation format for this estate. One extension, `.deed`. + +This directory holds the *family-level* specification — the grammar every deed +shares. The per-format satellites (`meta-a2ml/`, `anchor-a2ml/`, +`agentic-a2ml/`, …) specify individual documents *within* that grammar and are +subordinate to it. + +== Read this first + +[cols="1,3"] +|=== +| Document | What it settles + +| `spec/DEED-GRAMMAR-SPEC.adoc` | Lexical structure, concrete syntax, the four document forms, identity semantics, the self-assertion rule, and the proposed typing chapter. +| `spec/abnf/deed.abnf` | The grammar in ABNF, normative for parsing. +|=== + +== What DEED is not + +[WARNING] +==== +*DEED is an s-expression format. It is not TOML, and it is not "TOML-like".* + +Older text in this repository described the family as "A2ML (Annotated Markup +Language) TOML-like key-value data formats". That description is *wrong* and it +is not merely cosmetic: measured across all 35,884 legacy `.a2ml` files, the +descriptile family had drifted to *0.2%* conformance (10 correct against 5,424 +TOML-shaped), because successive tools read that sentence and generated what it +described. + +The grammar has *no* `key = value` form and *no* `[section]` form. The only +bracket is `(`. A file using `=` is not a deed. + +`RECORD-DIALECT-SPEC.adoc` in `hyperpolymath/a2ml`, which specified that +key/value surface, is SUPERSEDED by this specification. +==== + +== The four document forms + +[cols="1,1,2"] +|=== +| Stem | Head | Meaning + +| `estate_chora.deed` | `(estate-deed` | The estate's vocabulary. One per estate. +| `*_chora.deed` | `(repo-deed` | What a repo IS. +| `ATLAS.deed` | `(estate-atlas-deed` | The registry of all deeds. +| `*_praxis.deed` | `(praxis-deed` | What a tool DOES. +|=== + +Every head requires `:schema-version`. + +== Status + +v0.1.0 DRAFT. Three rulings were settled by the owner on 2026-09-08 (the +fourth head, the version field, and the record-dialect supersession); four +remain open and are listed at the end of the specification. + +== Licence + +Specification text: CC-BY-SA-4.0. See `LICENSE` files at the repository root. diff --git a/deed/spec/DEED-GRAMMAR-SPEC.adoc b/deed/spec/DEED-GRAMMAR-SPEC.adoc new file mode 100644 index 00000000..6b1c4c7c --- /dev/null +++ b/deed/spec/DEED-GRAMMAR-SPEC.adoc @@ -0,0 +1,649 @@ +// SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) +// SPDX-License-Identifier: CC-BY-SA-4.0 += DEED Grammar Specification +:revnumber: 0.1.0 +:revdate: 2026-09-08 +:status: DRAFT +:media-type: application/vnd.deed +:toc: +:toclevels: 3 +:sectnums: + +[IMPORTANT] +==== +*Status: DRAFT, not ratified. Nothing in this document is deployed.* + +Prepared 2026-09-08. This is the specification the owner asked for as top +priority. It is deliberately scoped to the *surface and its identity rule*, +because that is what unblocks the `.a2ml` -> `.deed` conversion (#64) and the +downstream consumers. The typing chapter (<>) is marked PROPOSED +throughout and is not part of the v0.1 conformance surface. + +Placement: this belongs in `standards`. It was drafted outside that repo +because at time of writing `standards` is on branch `e2/747-work` with 17 +uncommitted `dependabot.yml` modifications that are not this session's work. +Landing it is the owner's call. +==== + +== Why this document exists + +Three measured facts, 2026-09-08, motivate every decision below. + +*Fact 1 — the only runnable gate cannot read a deed.* `validate-a2ml.sh` +recognises four identity forms and no more: + +[source,bash] +---- +if [[ "$line" =~ ^[[:space:]]*(agent[-_]id|name|project|spec_id)[[:space:]]*= ]] \ + || [[ "$line" =~ ^[[:space:]]*name[[:space:]]*: ]] \ + || [[ "$line" =~ ^\[(metadata|scorecard)\] ]] \ + || [[ "$line" =~ ^@abstract ]]; then + has_identity=true +---- + +TOML `key =`, YAML `name:`, INI `[metadata]`, markup `@abstract`. A file +written in the owner's own deed form fails on both the leading parenthesis and +the absent `=`. Measured under `INPUT_STRICT=true`: + +---- +::error:: No identity found (agent-id/name/project/spec_id field, + [metadata] or [scorecard] section, or @abstract directive) +::error:: Missing version or schema_version field +rc=1 +---- + +*Fact 2 — `.deed` is invisible.* `grep -ci deed validate-a2ml.sh` returns *0* +against *20* occurrences of `a2ml`. No tool in the estate scans a `.deed` file +today. + +*Fact 3 — the identity primitive already exists, compiles, and is decidable.* +`src/A2ML/BaseVocab.idr` builds clean (11/11 modules, `%default total`) and its +own header states its purpose: "the anti-desync primitive: one neutral shape +for a thing that can be identified, located, attributed, and integrity-checked. +It names no downstream consumer." + +The gap is therefore not a missing grammar. It is that a *typed, total, +surface-neutral* identity core exists in Idris2, and a *weaker, rival* identity +rule exists in shell regex, and neither knows about `.deed`. This document +closes that by defining the deed surface in terms of the typed core, and by +specifying the single change the validator needs. + +== Scope and non-goals + +In scope: lexical structure, concrete syntax, the document forms, the identity +rule, the conformance modes, and the validator obligation. + +Not in scope for v0.1: the `action-parsing-rules` / `on-encounter` sub-language +of praxis deeds (owner has flagged the existing draft syntax as a strawman); +the vocabulary content of any particular chora; the conversion campaign itself. + +== Lexical structure + +A deed is a sequence of UTF-8 bytes. Parsers MUST be deterministic given +identical input bytes. + +[cols="1,3"] +|=== +| `COMMENT` | `;;` to end of line. A single `;` is also a comment; `;;` is the + convention for a whole-line comment and `;` for a trailing one. +| `WS` | space, tab, CR, LF. Insignificant except as a token separator. +| `SYMBOL` | `[A-Za-z][A-Za-z0-9.*/<>=!?+-]*`. Dots are structural: `Type.Software.Library` + is one symbol whose dotted segments are meaningful to the type resolver. +| `KEYWORD` | `:` followed by a `SYMBOL`. Hyphen, never underscore: `:schema-version`. +| `STRING` | `"` … `"`, with `\\`, `\"`, `\n`, `\t` escapes. No other escape is valid. +| `INTEGER` | `-?[0-9]+` +| `BOOLEAN` | `#t` or `#f`. No other spelling is accepted — not `true`, not `yes`. +| `UUID5` | `#u5"` STRING-body `"`. The body is the *name* input to RFC 4122 §4.3, + under the estate namespace. See <>. +| `QUOTED` | `'` followed by a `SYMBOL` or a list. Suppresses evaluation; used for + symbol data and for lists of symbols. +| `(` `)` | The only bracket. No `[` or `{` forms exist in this grammar. +|=== + +NOTE: The estate's earlier markup dialect used square brackets. Those are +*not* part of the deed grammar. A `[section]` header in a `.deed` file is a +speciation artefact, not a deed. + +== Concrete syntax + +[source] +---- +Deed ::= Header COMMENT* Form +Header ::= SpdxLine+ ; see Section 4.1 +Form ::= "(" DocHead VersionField Field* Clause* ")" +DocHead ::= "estate-deed" | "repo-deed" | "estate-atlas-deed" + | "praxis-deed" +VersionField ::= ":schema-version" STRING ; REQUIRED on every head + +Field ::= KEYWORD Value +Value ::= STRING | SYMBOL | INTEGER | BOOLEAN | UUID5 + | QUOTED | List +List ::= "(" Value* ")" + +Clause ::= "(" SYMBOL Field* Clause* ")" +---- + +A *Field* is a keyword/value pair. A *Clause* is a named sub-form that may +itself carry fields and nested clauses. This is the whole grammar; everything +else in a deed is vocabulary, not syntax. + +=== Required header + +Every deed MUST begin with SPDX lines as `;;` comments, before the opening +parenthesis: + +[source,lisp] +---- +;; SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) +;; SPDX-License-Identifier: CC-BY-SA-4.0 +---- + +The existing validator already requires `SPDX-License-Identifier` within the +first 10 lines and reports its absence. That check carries over unchanged. + +=== Order is not semantic + +Fields and clauses are order-free. A canonical ordering is a *lint convention +for diffability*, never a parse rule. Where precedence genuinely matters — the +rules inside a praxis deed — it is carried by an explicit `:priority` INTEGER, +never by file position. + +Rationale, and this is the estate's signature failure mode: with first-match-wins, +a broad rule inserted above a narrow one silently shadows it. No error is +raised; the narrow rule simply stops firing. With `:priority`, shadowing shows +up in a diff as a number changing, and the file stays sortable, formattable and +merge-safe. + +Lint obligations that follow: + +* `:priority` values MUST be unique within a single rules block. +* A rule whose guard is implied by a lower-priority rule's guard SHOULD warn. + +[#document-forms] +== The four document forms + +One extension, `.deed`. The form is selected by the filename *stem*, not by a +second extension. + +[cols="1,1,2"] +|=== +| Stem pattern | Head form | Meaning + +| `estate_chora.deed` | `estate-deed` | *Noun.* The estate's vocabulary. One per estate. +| `*_chora.deed` | `repo-deed` | *Noun.* What a repo IS. A record. +| `ATLAS.deed` | `estate-atlas-deed` | *Noun.* The registry of all deeds. +| `*_praxis.deed` | `praxis-deed` | *Verb.* What a tool DOES. Rules. +|=== + +*RULED 2026-09-08 by the owner:* `praxis-deed` is a genuine fourth head, not a +facet of `repo-deed`. A tool carries obligations a repo does not — what it +invokes, what it emits, what it may refuse — and those are a distinct document +form, so they get a distinct production rather than being smuggled in as +optional fields on a record. + +NOTE: This is *not* the earlier `tool-praxis-deed`, which was another session's +coinage and was removed from this spec because it appeared in no owner text. +The owner's own three heads were `estate-deed`, `repo-deed` and +`estate-atlas-deed`; `praxis-deed` is a deliberate addition ruled on +2026-09-08, and the name is *two* words, not three. + +[#version-field] +=== `:schema-version` is required on every head + +*RULED 2026-09-08 by the owner.* The owner's original text was not uniform: +`estate-deed` carried `:schema-version`, `estate-atlas-deed` carried +`:registry-version`, and `repo-deed` carried neither. The grammar normalises +this: + +* `:schema-version` STRING is *REQUIRED* on all four heads. It versions the + *format*, so a consumer can refuse a file it cannot parse. +* `:registry-version` STRING remains available on `estate-atlas-deed` as an + *optional additional* field. It versions the *registry's contents*, which is + a different thing from the format version, so nothing is lost by keeping both. + +[source,lisp] +---- +(estate-atlas-deed + :schema-version "1.0.0" ; REQUIRED — the format + :registry-version "3" ; optional — the contents + ...) +---- + +This is the field the current validator cannot see. Its regex is: + +[source,subs="none"] +---- +^[[:space:]]*(version|schema_version)[[:space:]]*[=:] +---- + +That matches the *underscore* spelling with no leading colon, so +` :schema-version "1.0.0"` FAILS and ` schema_version = "1.0"` PASSES — +directly tested. See <>. + +Rationale for a single extension: the grammar is identical and only the +structure differs. An extension should track what *parses* a file, not what it +means — `.rs` covers both a library and a binary. `find -name '*_chora.deed'` +costs exactly what `find -name '*.chora'` costs, so a second extension buys +nothing a stem glob does not already give, while doubling every discovery +pattern across the estate *during* an in-flight `.a2ml` -> `.deed` sweep. Two +interleaved estate-wide sweeps is how this goes wrong. The existing validator +already dispatches on basename, so stem dispatch is proven in current tooling. + +[#praxis-form] +=== The `praxis-deed` form + +A praxis deed states what a tool *does*. Three fields are required, and they +follow from rules already established elsewhere in this document rather than +from taste: + +[source,lisp] +---- +;; SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) +;; SPDX-License-Identifier: CC-BY-SA-4.0 +(praxis-deed + :schema-version "1.0.0" ; REQUIRED — every head (<>) + :canonical-name "cadastre" ; REQUIRED — identity (<>) + :beholding-chora #u5"estate/chora" ; REQUIRED — one declaration site + + (rules + (rule :priority 10 :when … :then …) + (rule :priority 20 :when … :then …))) +---- + +* `:beholding-chora` is required *because* of <>: a tool + may not declare its own vocabulary, so it must name the chora it reads. A + UUID, never a bare filename — a bare filename resolves against nothing. +* `:priority` is required on each rule *because* of order-independence: rule + precedence is carried by an explicit integer, never by file position. + +WARNING: *Provisional for v0.1.* The owner ruled on 2026-09-08 that +`praxis-deed` is a genuine fourth head. The owner did *not* rule on which +fields beyond these three a praxis deed must carry — candidates such as +`:invokes`, `:emits` and `:may-refuse` are *not* specified here, because +inventing them is precisely the failure this document exists to stop. A tool +deed conforms in v0.1 on the three fields above; anything further is a v0.2 +question. + +`estate-atlas-deed` is *not* folded into this form. The atlas is a registry — +a noun, a record of what exists — and keeps its own head. A praxis deed is a +verb. + +[#one-declaration-site] +=== One declaration site + +Vocabulary — types, tropes, lattices — is declared in `estate_chora.deed` and +*nowhere else*. Every other deed references it. This is the owner's ruling of +2026-09-04, verbatim: "it should be referrring to the chora". + +A praxis deed names the vocabulary it reads via `:beholding-chora `. A +repo chora names its estate via `:beholding-estate `. Both take a UUID, +never a bare filename — a bare filename resolves against nothing. + +This rule exists because the first draft declared its own parallel type +universe in a tool deed, and the dependency then ran backwards: a lattice was +declared in the tool and consumed by the chora, while every repo beheld the +chora. Two universes with no precedence between them is not a layering +problem, it is an ambiguity. + +=== The chora is not a layer + +.... + estate_chora.deed THE VOCABULARY (noun, estate-wide) + types · tropes · lattice · universal invariants + | + | every layer below resolves its names here + | + +-------------+---------------------------------------+ + | | + v v + TOOL PRAXIS DEEDS REPO CHORAS + _praxis.deed repo_chora.deed + rules: guard -> action local facts, history, names + | ^ + | the cadastre reads every repo chora -->| + | derives · validates · maps + v + EMISSIONS topoindex · veracity-ledger · attenuation-census + | + v + OPERATIONAL TOOLS — read the MAPS; they do not re-parse repo choras +.... + +[#uuid-semantics] +=== UUID semantics — state the claim honestly + +`#u5"…"` is a UUIDv5: SHA-1 over a public namespace and a public name. Any +cloner can recompute it correctly. It therefore *cannot* establish that a +document is unfalsified, and no rule may claim that it does. + +What it does establish is real and worth checking: a clone that copied a deed +verbatim without re-running repo initialisation will carry the *parent's* +UUID, which will not match its own name. That is lazy copy-paste, and this +catches it. The check is named `enforce-uuid-provenance` for that reason and +MUST NOT be named or described as an unfalsifiability guarantee. + +== Semantics: identity, and the self-assertion rule + +[#identity] +=== Identity maps onto BaseRecord + +A deed's identity is not a new invention. It is the already-typed +`BaseVocab.BaseRecord`, whose required fields are `id`, `sourceSpan`, `hash` +(`sha256:` + 64 lowercase hex), `provenance` (`author`, `tool` as `name@version`, +`kind` ∈ {`human`,`ai`,`mechanical`}, optional `agent`), `timestamp` (RFC 3339 +UTC) and `artefactRef`. `canonicalNode`, `agent` and `profileDecl` are optional +and do not affect base validity. + +In the deed surface, a document is *identified* when it carries: + +[cols="1,3"] +|=== +| `:schema-version STRING` | *REQUIRED on every deed* — RULED by the owner 2026-09-08; see <>. Note this is a *change to existing files*, not a description of them: the owner's source text carried `:schema-version` on `estate-deed`, `:registry-version` on `estate-atlas-deed`, and nothing on `repo-deed`. `:registry-version` is a DISTINCT field (it versions registry contents, not the format) and survives as optional on the atlas. +| `:canonical-name STRING` or an explicit identity keyword | REQUIRED. +| `:estate-uuid` / `:repo-uuid` UUID5 | REQUIRED on chora forms. +|=== + +The head symbol (`estate-deed`, `repo-deed`, `estate-atlas-deed`, `praxis-deed`) is itself +identifying: a file whose first form is one of the four declared heads is a +deed of that kind, and a validator MAY treat the head as satisfying the +structural half of identity. + +[#self-assertion] +=== A self-declaration is an input, never a conclusion + +This is the load-bearing semantic rule of the whole format, and it generalises +a specific defect found in the first draft. + +That draft had a repo declare `:p-falsifying #f :p-misbinding #f +:p-conflating #f`, and had the enforcing rule read those same fields back to +decide whether the repo was deceptive. *A liar declares `#f`.* The rule was +vacuous — it could only ever confirm what it was told. + +The general rule: + +[NOTE] +==== +*A deed's self-assertions are INPUTS to an audit. They are never its +conclusions.* Any derived judgement about a repo MUST be computed by an +external observer from observed state, MUST be recorded in a distinct +`:derived-state` position, and MUST carry a witness naming the deriving tool. +A rule that reads a self-assertion and emits a judgement of the same +proposition is ill-formed and MUST be rejected by the linter. +==== + +Consequently a repo states a `warrant` (<> — the owner's own term, +replacing the coinage `veracity-claim`); it does not state a +veracity *state*. The cadastre derives the state and emits a witness. A +bare symbol that a repo writes about itself is not a witness. + +[#typechecking] +== Typechecking — PROPOSED, pending the typed core + +[IMPORTANT] +==== +Everything in this section is PROPOSED. It is recorded so the design is not +lost, not because it is settled. `TypedCore.idr` currently types the *prose* +document model (sections, refs, figures) and has no record/deed node. Bridging +it is real work, not a rename. +==== + +=== What already exists and is total + +`BaseVocab` provides `baseValidB : BaseRecord -> Bool`, the proposition +`BaseValid r = baseValidB r = True`, a decision procedure +`baseValidDec : (r : BaseRecord) -> Dec (BaseValid r)`, and structured +diagnostics `baseRecordIssues` enumerating errors first and the +`AiMissingAgent` advisory last. This is the model to follow for every deed +check: a decidable Boolean, a proposition, a decision procedure, and a +*structured* issue list rather than a string. + +[#four-type-systems] +=== Four type systems, measured against what the estate already proves + +The owner asked whether tropical, choreographic, echo or epistemic typing can +be incorporated usefully into `.deed`, and if necessary into k9. These are not +textbook theories to be imported: all four are mechanised in the owner's own +`_TYPES _SET/` repos. Each verdict below says which layer it touches — +*grammar*, *semantics*, or *k9* — because most of them touch no grammar at all. + +The honest summary: *one changes a name, one is a k9 proposal, two are naming +for shapes this spec already has.* None requires a new production. + +==== Epistemic — adopt the vocabulary, change nothing else + +`_TYPES _SET/epistemic-types` (Agda, MPL-2.0) builds a modality spectrum in +which `FactiveModality` carries `reflect : E κ A -> A` (knowledge implies +truth) and `BeliefModality` *intentionally omits* `reflect`. That omission is +<> stated formally: a repo's declaration +inhabits a non-factive modality, so no rule can extract truth from it. The +distinction is proved structural, not asserted by a linter. + +It also already has the word this draft coined. The repo defines +`Warrant κ A` as "the type of evidence tokens for `A`", explicitly recording +"the *type of evidence* for a claim without assuming the evidence is valid", +and separates "I have a receipt for A" from "A is true" — with `SoundWarrant` +as a *separate* interface adding `evidence -> A`, not assumed by default. + +*Ruling proposed:* withdraw the coinage `veracity-claim` from the open rulings +and use *warrant* for a repo's non-authoritative self-assertion, and *receipt* +for a claim transported across a repo boundary. The owner already has the +terms, mechanised, with the exact semantics this format needs. Coining a rival +word would repeat the `tool-praxis-deed` error in vocabulary rather than syntax. + +*Layer:* semantics and naming. No grammar change. No new field. + +==== Tropical — the only one that belongs in k9, and it has a consumer + +`_TYPES _SET/tropical-types` formalises the max-plus semiring over +`ℕ ∪ {-∞}` in `Tropical.thy` (Isabelle 2025-1, `comm_semiring_1` proved +through a seven-step typeclass chain, dioid proved separately), and +`TropicalSessionTypes.lean` proves that a static tropical grade equals the +dynamic wall-clock span, with a QTT refinement showing the tropical grade +bounds sequential billing. + +The discriminator for "useful" is whether anything declares a budget today. +*Measured across both canonical trees:* `timeout_seconds | Number | default = +300` occurs in *133* Nickel files across *63 repos* — but those files carry +only three basenames (`_base.ncl` x68, `trust.ncl` x60, `echidnabot.ncl` x5), +so this is *one shared contractile-runner template stamped estate-wide*, not +133 independent decisions. `_base.ncl` is the base imported by every verb +runner and the field sits in its `run_defaults`. Alongside it, +`timeout_honouring = 'strict` occurs in *48* files, and `'timeout` is one of +nine declared failure classes (175 occurrences). + +That the template is shared is what makes this tractable: a per-step bound is +already declared in one place for the whole estate. What does not exist +anywhere is a rule for *composing* those bounds. A pipeline of six steps each +bounded at 300s has no declared total, so a runner cannot say in advance +whether the pipeline can finish inside its own bound. + +That composition rule is exactly the tropical semiring: sequential composition +is ⊗ (addition of grades), a parallel or alternative fan-out is ⊕ (max of +grades, giving the span). The Lean result is the soundness story — the +statically computed grade *is* the wall-clock span. Note the direction of the +claim when it is applied here: `timeout_seconds` declares a *bound*, not a +measured duration, so the composed value *bounds* the pipeline's span rather +than equalling it. That is still enough for a runner to refuse a pipeline +whose composed bound exceeds its own. + +*Ruling proposed:* this belongs in the *Nickel runner layer*, never in +`.deed`. Be precise about where that is: of the *147* `.ncl` files declaring +`timeout_seconds`, *141* sit in the contractile-runner layer — *133* of those +under just three basenames (`_base.ncl`, `trust.ncl`, `echidnabot.ncl`), the +other 8 miscellaneous — and *6* are k9 configs +(`fleet-config.k9.ncl`, `mcp-server-config-schema.k9.ncl`). *No `.k9` file +declares it at all* — 250 exist and none carry the field — so "k9 already has +timeouts" is true of `*.k9.ncl` Nickel configs, not of the `.k9` surface. +Propose a composed bound in the runner base alongside the existing per-step +field, so a pipeline's declared total is checkable against its parts. This is +task #76 (the must/intend/trust/adjust/bust/dust runners), not a grammar task. + +*Do not* add a `:budget` field to `.deed`. Nothing reads it. A field no tool +consumes is how the TOML speciation started. + +*Layer:* the Nickel runner layer only (task #76). No grammar change, no new `.deed` field. + +==== Echo — the name for what ANCHOR is + +`_TYPES _SET/echo-types` (Agda, `--safe --without-K`, no postulates) proves +the fiber laws for `Echo f` and the total-space equivalence +`A ≃ Σ B (Echo f)`. Read against this format: a deed is a *projection* of a +repo's actual state; the fiber over a declaration is everything the projection +lost. The equivalence then says the declaration plus its fiber recovers the +repo — which is the precise statement of what ANCHOR is for (task #22, ruled +2026-09-08 to be *both* descriptile and contractile, the is/ought join). +Declared state is the projection; observed drift is the fiber; ANCHOR is the +point where the two are forced back together. + +Two caveats carried verbatim from the repo, because they bound the claim. +The equivalence "is not novel" — it is the standard HoTT total-space-of-fibers +result — and "the repo's contribution is the *emphasis*", treating it as the +foundation for a structured-loss account. And the factorization is +*domain-replacement*, not image factorization; the repo admits +`EchoImageFactorization` is a misnomer and gives a weak factorization system, +with orthogonality (unique diagonal fills) *not yet proved*. + +*Ruling proposed:* adopt echo as the vocabulary for the ANCHOR spec — +projection, fiber, structured loss — and cite it as naming a shape, not as +machinery that computes anything. Nothing here validates a file. + +*Layer:* semantics, and the ANCHOR spec (#22). No grammar change. + +==== Choreographic — already the estate/repo split, but its keystone is open + +`_TYPES _SET/choreographic-types` is not a fourth independent system: it +*fuses* the previous two. A global choreographic type `G` is read as a partial +causal order and projected to local types by endpoint projection, with each +edge graded by an echo loss-grade and an epistemic standpoint-warrant. A *cut* +is a consistent frontier (antichain) across that order. + +That is the topology this spec already describes. `estate_chora.deed` is the +global type; `repo_chora.deed` is its endpoint projection; the +one-declaration-site rule (<>) is the projection discipline — +vocabulary is declared once globally and projected, never re-declared locally. +Naming it as endpoint projection turns "an operational tool does not read a +source it is not a party to" from a prose invariant into a statable property. + +*The load-bearing caveat:* the repo's central artefact, K-CUT — "the +conjecture that grading and transport commute with projection across a +consistent frontier" — is described by the repo itself as *open*. This spec +must not depend on it. Use the vocabulary; do not claim the theorem. + +*Ruling proposed:* adopt choreography/endpoint-projection as the description +of the estate/repo relation in <>. Record K-CUT as an open dependency +if any future rule is ever derived from commuting projection. + +*Layer:* semantics and terminology. No grammar change. + +== Conformance and the validator obligation + +=== Modes + +[cols="1,3"] +|=== +| `lax` | Structure only. Identity and version absent are warnings. +| `strict` | Identity and version absent are ERRORS. Unknown clauses are errors. +| `attested` | strict, plus every derived judgement must carry a witness. +|=== + +*For `.deed` files, `strict` is the DEFAULT and `lax` MUST be opt-in.* + +This inverts current behaviour and is deliberate. Today, identity and version +are `report_issue "warning"`, so a file with no identity at all scores +rc=0 and prints "validation passed" unless `INPUT_STRICT=true` is set. Any CI +job citing the validator without that variable is a formality, not a gate. +That default is how the speciation regenerated unnoticed, and it must not +carry over to `.deed`. + +[#validator-change] +=== The single change the validator needs + +Add a fifth identity form — the s-expression head — and accept hyphenated +keyword versions: + +[source,bash] +---- +# identity: accept a deed document head +|| [[ "$line" =~ ^[[:space:]]*\((estate-deed|repo-deed|estate-atlas-deed|praxis-deed)([[:space:]]|$) ]] +# identity: accept keyword-style identity fields +|| [[ "$line" =~ ^[[:space:]]*:(canonical-name|estate-authority|agent-id)[[:space:]] ]] + +# version: accept hyphenated keyword form alongside version/schema_version +|| [[ "$line" =~ ^[[:space:]]*:schema-version[[:space:]] ]] +|| [[ "$line" =~ ^[[:space:]]*:registry-version[[:space:]] ]] +---- + +A SECOND, separate gap was measured in the same script. Version detection reads: + +[source,bash] +---- +if [[ "$line" =~ ^[[:space:]]*(version|schema_version)[[:space:]]*[=:] ]]; then + has_version=true +---- + +That pattern requires the field name at the start of the line with no leading +colon, and spells it with an underscore. The deed surface writes +`:schema-version` — leading colon, hyphen. Verified by direct test: the line +` :schema-version "1.0.0"` does NOT match, while ` schema_version = "1.0"` +does. So a conforming deed fails BOTH the identity check and the version check, +for two independent reasons. Both must be patched together or the fix is half a +fix. + + +Note the patterns are anchored to optional *leading whitespace only*, so an +indented head still matches. This matters: the owner's own `estate_chora.deed` +indents its fields, and a form anchored to column zero would reject it. + +=== Exemptions carry over unchanged + +The existing identity exemptions remain: basenames containing `AI-MANIFEST`; +`AI.a2ml` (and its successor `AI.deed`); any basename containing `template`; +any file with unfilled placeholders; and any path under a configured design +tree. These exist because a template legitimately has no identity of its own. + +== Rulings settled, and rulings still open + +=== Settled by the owner, 2026-09-08 + +. *The record dialect — SUPERSEDED.* `RECORD-DIALECT-SPEC.adoc` (v1.0.0, + Draft, in `hyperpolymath/a2ml`) specified `[section]` + `key = value`. That + is the TOML-family surface the owner's own instruction targets ("many AIs + have speciated the a2ml/k9s into json type and toml type … I did not ask for + it"), and measurement over all 35,884 `.a2ml` files found the grammar has no + `=` form. *Ruled:* keep the file as history, stamped SUPERSEDED with a + `superseded-by` pointer to this document. It is no longer live guidance. + +. *A praxis deed gets its own head — `praxis-deed`.* See + <>. Four heads, not three. `estate-atlas-deed` remains the + head for the registry specifically; `praxis-deed` is the general tool form. + +. *Version field — `:schema-version`, required everywhere.* See + <>. `:registry-version` survives as an optional additional + field on the atlas only. + +=== Still open + +. *Echo typing — ANSWERED, ratification needed.* <> gives a + reading grounded in `_TYPES _SET/echo-types`: a deed is a projection, the + fiber over it is the drift, and `A ≃ Σ B (Echo f)` is why ANCHOR (#22) is the + point that rejoins them. *Ratify or reject that reading* — and note the repo + itself calls the equivalence non-novel and has not proved orthogonality. + +. *The warrant/receipt swap — proposed, unratified.* <> + withdraws the coinage `veracity-claim` in favour of *warrant* (evidence + recorded without assuming soundness) and *receipt* (a claim transported + across a boundary), both already mechanised in + `_TYPES _SET/epistemic-types`. Confirm the swap. + +. *Where pillar-specific vocabulary lives.* One-declaration-site removes the + duplicate universe; it does not decide where genuinely tool-specific types + belong. Two options: put them in the universal chora (bloats it with + vocabulary only one tool matches on), or add an explicit + `(extends-vocabulary :base …)` form in the praxis deed — + subordinate by construction, so it cannot recreate the two-universe defect. + +. *Slot/assembly vocabulary has no declaration site at all.* A downstream + consumer wanting to express a multi-slot assembly as a deed cannot do so + today, and under one-declaration-site it may not invent the vocabulary + locally. Either the estate chora gains it, or `extends-vocabulary` lands. + (Task #75.) diff --git a/deed/spec/abnf/deed.abnf b/deed/spec/abnf/deed.abnf new file mode 100644 index 00000000..17f442ae --- /dev/null +++ b/deed/spec/abnf/deed.abnf @@ -0,0 +1,48 @@ +; SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) +; SPDX-License-Identifier: CC-BY-SA-4.0 +; +; DEED grammar, v0.1.0 DRAFT +; Normative for parsing. Prose and rationale: ../DEED-GRAMMAR-SPEC.adoc +; +; NOTE: there is no "key = value" production and no "[section]" production. +; The only bracket is "(". A file using "=" is not a deed. + +deed = header *comment form + +header = 1*spdx-line +spdx-line = ";;" SP "SPDX-" 1*(VCHAR / SP) CRLF + +form = "(" doc-head version-field *field *clause ")" +doc-head = "estate-deed" / "repo-deed" / "estate-atlas-deed" / "praxis-deed" +version-field = ":schema-version" 1*WSP string ; REQUIRED on every head + +field = keyword value +clause = "(" symbol *field *clause ")" + +keyword = ":" symbol +value = string / symbol / integer / boolean / uuid5 / quoted / list +list = "(" *value ")" +quoted = "'" ( symbol / list ) + +symbol = ALPHA *( ALPHA / DIGIT / "." / "*" / "/" / "<" / ">" + / "=" / "!" / "?" / "+" / "-" ) + ; "." is STRUCTURAL: Type.Software.Library is ONE symbol + ; whose dotted segments are meaningful to the type resolver. + ; "=" may appear INSIDE a symbol (e.g. a comparison operator); + ; it is never a field separator. + +string = DQUOTE *( str-char / escape ) DQUOTE +str-char = %x20-21 / %x23-5B / %x5D-10FFFF ; any char except " and \ +escape = "\" ( DQUOTE / "\" / "n" / "t" ) ; no other escape is valid + +integer = [ "-" ] 1*DIGIT +boolean = "#t" / "#f" ; never "true", never "yes" +uuid5 = "#u5" string ; body is the NAME input to + ; RFC 4122 4.3 under the + ; estate namespace +comment = ";" *( VCHAR / SP ) CRLF + +; Order is not semantic. Fields and clauses are order-free; a canonical +; ordering is a lint convention for diffability, never a parse rule. +; Where precedence matters (rules in a praxis deed) it is carried by an +; explicit :priority INTEGER, never by file position. From fdd54cf0d1643a1060147159e1d9ced46402a1a1 Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Tue, 8 Sep 2026 18:41:30 +0000 Subject: [PATCH 2/8] Clarify deed separators, UTF-8 strings, line endings, and filename dispatch --- deed/README.adoc | 5 ++++- deed/spec/DEED-GRAMMAR-SPEC.adoc | 37 ++++++++++++++++---------------- deed/spec/abnf/deed.abnf | 27 ++++++++++++++++------- 3 files changed, 41 insertions(+), 28 deletions(-) diff --git a/deed/README.adoc b/deed/README.adoc index a8894a85..391fe897 100644 --- a/deed/README.adoc +++ b/deed/README.adoc @@ -48,11 +48,14 @@ key/value surface, is SUPERSEDED by this specification. | Stem | Head | Meaning | `estate_chora.deed` | `(estate-deed` | The estate's vocabulary. One per estate. -| `*_chora.deed` | `(repo-deed` | What a repo IS. +| `*_chora.deed` (except `estate_chora.deed`) | `(repo-deed` | What a repo IS. | `ATLAS.deed` | `(estate-atlas-deed` | The registry of all deeds. | `*_praxis.deed` | `(praxis-deed` | What a tool DOES. |=== +The repository pattern explicitly excludes `estate_chora.deed`; dispatchers +MUST apply the exact estate filename rule before the repository pattern. + Every head requires `:schema-version`. == Status diff --git a/deed/spec/DEED-GRAMMAR-SPEC.adoc b/deed/spec/DEED-GRAMMAR-SPEC.adoc index 6b1c4c7c..a8c876e2 100644 --- a/deed/spec/DEED-GRAMMAR-SPEC.adoc +++ b/deed/spec/DEED-GRAMMAR-SPEC.adoc @@ -27,7 +27,7 @@ Landing it is the owner's call. == Why this document exists -Three measured facts, 2026-09-08, motivate every decision below. +Two measured facts, 2026-09-08, motivate the decisions below. *Fact 1 — the only runnable gate cannot read a deed.* `validate-a2ml.sh` recognises four identity forms and no more: @@ -56,17 +56,9 @@ rc=1 against *20* occurrences of `a2ml`. No tool in the estate scans a `.deed` file today. -*Fact 3 — the identity primitive already exists, compiles, and is decidable.* -`src/A2ML/BaseVocab.idr` builds clean (11/11 modules, `%default total`) and its -own header states its purpose: "the anti-desync primitive: one neutral shape -for a thing that can be identified, located, attributed, and integrity-checked. -It names no downstream consumer." - -The gap is therefore not a missing grammar. It is that a *typed, total, -surface-neutral* identity core exists in Idris2, and a *weaker, rival* identity -rule exists in shell regex, and neither knows about `.deed`. This document -closes that by defining the deed surface in terms of the typed core, and by -specifying the single change the validator needs. +The gap is therefore that the existing shell validator knows neither the deed +surface nor `.deed` files. This document closes that by defining the deed +surface and specifying the single change the validator needs. == Scope and non-goals @@ -86,7 +78,7 @@ identical input bytes. |=== | `COMMENT` | `;;` to end of line. A single `;` is also a comment; `;;` is the convention for a whole-line comment and `;` for a trailing one. -| `WS` | space, tab, CR, LF. Insignificant except as a token separator. +| `WS` | space, tab, CRLF, or LF. Insignificant except as a token separator. | `SYMBOL` | `[A-Za-z][A-Za-z0-9.*/<>=!?+-]*`. Dots are structural: `Type.Software.Library` is one symbol whose dotted segments are meaningful to the type resolver. | `KEYWORD` | `:` followed by a `SYMBOL`. Hyphen, never underscore: `:schema-version`. @@ -110,17 +102,21 @@ speciation artefact, not a deed. ---- Deed ::= Header COMMENT* Form Header ::= SpdxLine+ ; see Section 4.1 -Form ::= "(" DocHead VersionField Field* Clause* ")" +Form ::= "(" DocHead TokenSep VersionField + (TokenSep (Field | Clause))* TokenSep? ")" DocHead ::= "estate-deed" | "repo-deed" | "estate-atlas-deed" | "praxis-deed" -VersionField ::= ":schema-version" STRING ; REQUIRED on every head +VersionField ::= ":schema-version" TokenSep STRING ; REQUIRED on every head -Field ::= KEYWORD Value +Field ::= KEYWORD TokenSep Value Value ::= STRING | SYMBOL | INTEGER | BOOLEAN | UUID5 | QUOTED | List -List ::= "(" Value* ")" +List ::= "(" (Value (TokenSep Value)*)? TokenSep? ")" -Clause ::= "(" SYMBOL Field* Clause* ")" +Clause ::= "(" SYMBOL (TokenSep (Field | Clause))* TokenSep? ")" +TokenSep ::= (WSP | LineEnd | Comment)+ +LineEnd ::= CRLF | LF +Comment ::= ";" (VCHAR | SP)* LineEnd ---- A *Field* is a keyword/value pair. A *Clause* is a named sub-form that may @@ -170,11 +166,14 @@ second extension. | Stem pattern | Head form | Meaning | `estate_chora.deed` | `estate-deed` | *Noun.* The estate's vocabulary. One per estate. -| `*_chora.deed` | `repo-deed` | *Noun.* What a repo IS. A record. +| `*_chora.deed` (except `estate_chora.deed`) | `repo-deed` | *Noun.* What a repo IS. A record. | `ATLAS.deed` | `estate-atlas-deed` | *Noun.* The registry of all deeds. | `*_praxis.deed` | `praxis-deed` | *Verb.* What a tool DOES. Rules. |=== +The repository pattern explicitly excludes `estate_chora.deed`; dispatchers +MUST apply the exact estate filename rule before the repository pattern. + *RULED 2026-09-08 by the owner:* `praxis-deed` is a genuine fourth head, not a facet of `repo-deed`. A tool carries obligations a repo does not — what it invokes, what it emits, what it may refuse — and those are a distinct document diff --git a/deed/spec/abnf/deed.abnf b/deed/spec/abnf/deed.abnf index 17f442ae..840bec43 100644 --- a/deed/spec/abnf/deed.abnf +++ b/deed/spec/abnf/deed.abnf @@ -10,18 +10,19 @@ deed = header *comment form header = 1*spdx-line -spdx-line = ";;" SP "SPDX-" 1*(VCHAR / SP) CRLF +spdx-line = ";;" SP "SPDX-" 1*(VCHAR / SP) line-end -form = "(" doc-head version-field *field *clause ")" +form = "(" doc-head token-sep version-field + *(token-sep (field / clause)) [token-sep] ")" doc-head = "estate-deed" / "repo-deed" / "estate-atlas-deed" / "praxis-deed" -version-field = ":schema-version" 1*WSP string ; REQUIRED on every head +version-field = ":schema-version" token-sep string ; REQUIRED on every head -field = keyword value -clause = "(" symbol *field *clause ")" +field = keyword token-sep value +clause = "(" symbol *(token-sep (field / clause)) [token-sep] ")" keyword = ":" symbol value = string / symbol / integer / boolean / uuid5 / quoted / list -list = "(" *value ")" +list = "(" [value *(token-sep value)] [token-sep] ")" quoted = "'" ( symbol / list ) symbol = ALPHA *( ALPHA / DIGIT / "." / "*" / "/" / "<" / ">" @@ -32,15 +33,25 @@ symbol = ALPHA *( ALPHA / DIGIT / "." / "*" / "/" / "<" / ">" ; it is never a field separator. string = DQUOTE *( str-char / escape ) DQUOTE -str-char = %x20-21 / %x23-5B / %x5D-10FFFF ; any char except " and \ +str-char = %x20-21 / %x23-5B / %x5D-7E / UTF8-2 / UTF8-3 / UTF8-4 + ; any char except " and \ escape = "\" ( DQUOTE / "\" / "n" / "t" ) ; no other escape is valid +UTF8-2 = %xC2-DF UTF8-tail +UTF8-3 = %xE0 %xA0-BF UTF8-tail / %xE1-EC 2UTF8-tail + / %xED %x80-9F UTF8-tail / %xEE-EF 2UTF8-tail +UTF8-4 = %xF0 %x90-BF 2UTF8-tail / %xF1-F3 3UTF8-tail + / %xF4 %x80-8F 2UTF8-tail +UTF8-tail = %x80-BF + integer = [ "-" ] 1*DIGIT boolean = "#t" / "#f" ; never "true", never "yes" uuid5 = "#u5" string ; body is the NAME input to ; RFC 4122 4.3 under the ; estate namespace -comment = ";" *( VCHAR / SP ) CRLF +token-sep = 1*(WSP / line-end / comment) +line-end = CRLF / LF +comment = ";" *( VCHAR / SP ) line-end ; Order is not semantic. Fields and clauses are order-free; a canonical ; ordering is a lint convention for diffability, never a parse rule. From be39d4eac8653672120843ad9bc715bad8fca05c Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Tue, 8 Sep 2026 20:02:21 +0100 Subject: [PATCH 3/8] =?UTF-8?q?=F0=9F=94=A7=20CodeRabbit=20CI=20Fix:=20Fix?= =?UTF-8?q?=20failing=20Hypatia=20GitHub=20Check=20CI=20job=20(#755)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit CI failure fixes was requested by @hyperpolymath. * https://github.com/hyperpolymath/standards/pull/752#issuecomment-5589559458 The following files were modified: * `deed/spec/DEED-GRAMMAR-SPEC.adoc` Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com> --- deed/spec/DEED-GRAMMAR-SPEC.adoc | 37 ++++++++++++++++---------------- 1 file changed, 19 insertions(+), 18 deletions(-) diff --git a/deed/spec/DEED-GRAMMAR-SPEC.adoc b/deed/spec/DEED-GRAMMAR-SPEC.adoc index a8c876e2..e05b49cc 100644 --- a/deed/spec/DEED-GRAMMAR-SPEC.adoc +++ b/deed/spec/DEED-GRAMMAR-SPEC.adoc @@ -27,7 +27,7 @@ Landing it is the owner's call. == Why this document exists -Two measured facts, 2026-09-08, motivate the decisions below. +Three measured facts, 2026-09-08, motivate every decision below. *Fact 1 — the only runnable gate cannot read a deed.* `validate-a2ml.sh` recognises four identity forms and no more: @@ -56,9 +56,17 @@ rc=1 against *20* occurrences of `a2ml`. No tool in the estate scans a `.deed` file today. -The gap is therefore that the existing shell validator knows neither the deed -surface nor `.deed` files. This document closes that by defining the deed -surface and specifying the single change the validator needs. +*Fact 3 — the identity primitive already exists, compiles, and is decidable.* +`a2ml/src/A2ML/BaseVocab.idr` builds clean (11/11 modules, `%default total`) and its +own header states its purpose: "the anti-desync primitive: one neutral shape +for a thing that can be identified, located, attributed, and integrity-checked. +It names no downstream consumer." + +The gap is therefore not a missing grammar. It is that a *typed, total, +surface-neutral* identity core exists in Idris2, and a *weaker, rival* identity +rule exists in shell regex, and neither knows about `.deed`. This document +closes that by defining the deed surface in terms of the typed core, and by +specifying the single change the validator needs. == Scope and non-goals @@ -78,7 +86,7 @@ identical input bytes. |=== | `COMMENT` | `;;` to end of line. A single `;` is also a comment; `;;` is the convention for a whole-line comment and `;` for a trailing one. -| `WS` | space, tab, CRLF, or LF. Insignificant except as a token separator. +| `WS` | space, tab, CR, LF. Insignificant except as a token separator. | `SYMBOL` | `[A-Za-z][A-Za-z0-9.*/<>=!?+-]*`. Dots are structural: `Type.Software.Library` is one symbol whose dotted segments are meaningful to the type resolver. | `KEYWORD` | `:` followed by a `SYMBOL`. Hyphen, never underscore: `:schema-version`. @@ -102,21 +110,17 @@ speciation artefact, not a deed. ---- Deed ::= Header COMMENT* Form Header ::= SpdxLine+ ; see Section 4.1 -Form ::= "(" DocHead TokenSep VersionField - (TokenSep (Field | Clause))* TokenSep? ")" +Form ::= "(" DocHead VersionField Field* Clause* ")" DocHead ::= "estate-deed" | "repo-deed" | "estate-atlas-deed" | "praxis-deed" -VersionField ::= ":schema-version" TokenSep STRING ; REQUIRED on every head +VersionField ::= ":schema-version" STRING ; REQUIRED on every head -Field ::= KEYWORD TokenSep Value +Field ::= KEYWORD Value Value ::= STRING | SYMBOL | INTEGER | BOOLEAN | UUID5 | QUOTED | List -List ::= "(" (Value (TokenSep Value)*)? TokenSep? ")" +List ::= "(" Value* ")" -Clause ::= "(" SYMBOL (TokenSep (Field | Clause))* TokenSep? ")" -TokenSep ::= (WSP | LineEnd | Comment)+ -LineEnd ::= CRLF | LF -Comment ::= ";" (VCHAR | SP)* LineEnd +Clause ::= "(" SYMBOL Field* Clause* ")" ---- A *Field* is a keyword/value pair. A *Clause* is a named sub-form that may @@ -166,14 +170,11 @@ second extension. | Stem pattern | Head form | Meaning | `estate_chora.deed` | `estate-deed` | *Noun.* The estate's vocabulary. One per estate. -| `*_chora.deed` (except `estate_chora.deed`) | `repo-deed` | *Noun.* What a repo IS. A record. +| `*_chora.deed` | `repo-deed` | *Noun.* What a repo IS. A record. | `ATLAS.deed` | `estate-atlas-deed` | *Noun.* The registry of all deeds. | `*_praxis.deed` | `praxis-deed` | *Verb.* What a tool DOES. Rules. |=== -The repository pattern explicitly excludes `estate_chora.deed`; dispatchers -MUST apply the exact estate filename rule before the repository pattern. - *RULED 2026-09-08 by the owner:* `praxis-deed` is a genuine fourth head, not a facet of `repo-deed`. A tool carries obligations a repo does not — what it invokes, what it emits, what it may refuse — and those are a distinct document From 4f85a1b7fd2a6dda80872e28ccd1c426ece01b36 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 9 Sep 2026 01:08:45 +0100 Subject: [PATCH 4/8] spec(deed): land the chora dispatch exclusion and fix the cross-repo citation Two review findings on #752 that the owner ruled on and that the bot's own follow-up commits did not close. 1. Filename dispatch was ambiguous. `estate_chora.deed` is a literal that ALSO matches the glob `*_chora.deed`, so a naive glob dispatches the estate vocabulary as a repo record. Adds [#chora-dispatch-exclusion] to the spec and a `deed-filename` production to the ABNF, both stating the exclusion. ABNF has no negation, so the exclusion is carried as an explicit normative SIDE CONDITION in both documents rather than pretended into the grammar. Owner ruling on #752: "yes, let's adopt this, good idea, the chora replaces the clade of course." 2. Hypatia SD022 flagged `src/A2ML/` as a nonexistent directory. It is a false positive with a real cause: the path is in the *a2ml* repository, not this one, and the citation did not say so. Verified present at hyperpolymath/a2ml@main:src/A2ML/BaseVocab.idr (11 modules). The citation is now written as an explicit cross-repo reference. Verified: asciidoctor renders with 0 warnings and the new section appears in the output; the ABNF block is comment-and-rule only and adds no production to the `deed` start rule. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01QNjWX2B4FffG7zqMBMui6v --- deed/spec/DEED-GRAMMAR-SPEC.adoc | 20 +++++++++++++++++++- deed/spec/abnf/deed.abnf | 19 +++++++++++++++++++ 2 files changed, 38 insertions(+), 1 deletion(-) diff --git a/deed/spec/DEED-GRAMMAR-SPEC.adoc b/deed/spec/DEED-GRAMMAR-SPEC.adoc index e05b49cc..663ad68f 100644 --- a/deed/spec/DEED-GRAMMAR-SPEC.adoc +++ b/deed/spec/DEED-GRAMMAR-SPEC.adoc @@ -57,7 +57,8 @@ against *20* occurrences of `a2ml`. No tool in the estate scans a `.deed` file today. *Fact 3 — the identity primitive already exists, compiles, and is decidable.* -`a2ml/src/A2ML/BaseVocab.idr` builds clean (11/11 modules, `%default total`) and its +`hyperpolymath/a2ml@main:src/A2ML/BaseVocab.idr` — a path in the *a2ml* +repository, not in this one — builds clean (11/11 modules, `%default total`) and its own header states its purpose: "the anti-desync primitive: one neutral shape for a thing that can be identified, located, attributed, and integrity-checked. It names no downstream consumer." @@ -175,6 +176,23 @@ second extension. | `*_praxis.deed` | `praxis-deed` | *Verb.* What a tool DOES. Rules. |=== +[#chora-dispatch-exclusion] +*Dispatch is exact-stem-first, and `*_chora.deed` EXCLUDES `estate_chora.deed`.* +The two stem patterns overlap: the literal string `estate_chora.deed` also +matches the glob `*_chora.deed`, so a naive glob dispatches the estate +vocabulary as a repo record. A conforming implementation MUST test the exact +stem `estate_chora` before testing the `*_chora` pattern, and MUST NOT parse +`estate_chora.deed` as a `repo-deed`. Equivalently, the repo form is +`_chora.deed` where `` is any non-empty stem other than the +exact string `estate`. + +NOTE: ABNF cannot express negation, so this exclusion is carried as a side +condition in both this document and `abnf/deed.abnf`. The side condition is +normative: the grammar alone is not sufficient to dispatch a filename. + +*RULED 2026-09-09 by the owner* on standards#752 — "yes, let's adopt this, good +idea, the chora replaces the clade of course." + *RULED 2026-09-08 by the owner:* `praxis-deed` is a genuine fourth head, not a facet of `repo-deed`. A tool carries obligations a repo does not — what it invokes, what it emits, what it may refuse — and those are a distinct document diff --git a/deed/spec/abnf/deed.abnf b/deed/spec/abnf/deed.abnf index 840bec43..5634bb82 100644 --- a/deed/spec/abnf/deed.abnf +++ b/deed/spec/abnf/deed.abnf @@ -17,6 +17,25 @@ form = "(" doc-head token-sep version-field doc-head = "estate-deed" / "repo-deed" / "estate-atlas-deed" / "praxis-deed" version-field = ":schema-version" token-sep string ; REQUIRED on every head +; --- Filename dispatch ------------------------------------------------- +; The document form is selected by the filename STEM before parsing begins. +; This production grammars the NAME, not the contents. + +deed-filename = estate-file / atlas-file / praxis-file / repo-file +estate-file = "estate_chora.deed" ; -> estate-deed +atlas-file = "ATLAS.deed" ; -> estate-atlas-deed +praxis-file = stem "_praxis.deed" ; -> praxis-deed +repo-file = stem "_chora.deed" ; -> repo-deed +stem = 1*( ALPHA / DIGIT / "-" / "." ) + +; SIDE CONDITION (normative, and NOT expressible in ABNF, which has no +; negation): in repo-file, MUST NOT be the exact string "estate". +; The literal "estate_chora.deed" also matches repo-file, so a conforming +; implementation MUST test estate-file BEFORE repo-file and MUST NOT parse +; estate_chora.deed as a repo-deed. Dispatch is exact-stem-first. +; See ../DEED-GRAMMAR-SPEC.adoc#chora-dispatch-exclusion. +; RULED 2026-09-09 by the owner on standards#752. + field = keyword token-sep value clause = "(" symbol *(token-sep (field / clause)) [token-sep] ")" From 3c616d0c3b519cff42ee675fa113bd86c05a77a0 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 9 Sep 2026 01:19:46 +0100 Subject: [PATCH 5/8] spec(deed): close the third unimplemented ruling, and fix a grammar that rejected its own spec MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Follow-up to 4f85a1b7. That commit said two of the six owner-ruled findings on #752 were left unimplemented by CodeRabbit's follow-up commits. Re-measured against the files rather than the commit titles: it was THREE. 1. Finding SPEC.adoc:113 is UNCLOSED IN THE EBNF LAYER, both halves. The ABNF was fixed; the concrete-syntax EBNF beside it was not, so the two normative layers contradicted each other — exactly what the finding said. - Order-freedom: ABNF had `*(token-sep (field / clause))` (interleaved); EBNF still had `Field* Clause*` (fields, THEN clauses). Now interleaved in both, and the prose says so. - Comments: ABNF had `token-sep = 1*(WSP / line-end / comment)`, so comments are legal anywhere a separator is; EBNF had `Deed ::= Header COMMENT* Form` — comments ONLY before the form, never inside it. The EBNF now carries an explicit `Sep ::= ( WS | COMMENT )+` that mirrors `token-sep` exactly. Owner ruling: "I think you are right, I am used to the enbf grammars, is this so for teh anbf, if so please fix." 2. NEW, found while verifying the above: the normative grammar rejected the specification's own mandated header. `spdx-line` and `comment` both admitted only `VCHAR / SP` (%x21-7E), but the header this spec MANDATES is `;; SPDX-FileCopyrightText: © 2026 ...` and that "©" is %xC2 %xA9. The lexical section already says "a deed is a sequence of UTF-8 bytes". Adds `text-char = VCHAR / SP / UTF8-2 / UTF8-3 / UTF8-4` and uses it in both. 3. `stem` excluded "_", so a repo whose name contains an underscore could not form a `_chora.deed` filename at all. 173 repo directories across the two canonical trees have an underscore in the name. "_" added. No ambiguity is introduced: the suffix is a literal anchored at end-of-name, so exactly one split matches. 4. The ruling date in 4f85a1b7 was wrong. I wrote "RULED 2026-09-09" into both normative documents without checking; the owner's replies are all 2026-09-08T18:38-18:51Z. Corrected in both. Verified: asciidoctor renders 0 warnings, 9

, and the anchor, "EXCLUDES", the interleaved repetition and the consistency prose all appear in the output. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01QNjWX2B4FffG7zqMBMui6v --- deed/spec/DEED-GRAMMAR-SPEC.adoc | 34 +++++++++++++++++++++++++------- deed/spec/abnf/deed.abnf | 14 +++++++++---- 2 files changed, 37 insertions(+), 11 deletions(-) diff --git a/deed/spec/DEED-GRAMMAR-SPEC.adoc b/deed/spec/DEED-GRAMMAR-SPEC.adoc index 663ad68f..4bb312ca 100644 --- a/deed/spec/DEED-GRAMMAR-SPEC.adoc +++ b/deed/spec/DEED-GRAMMAR-SPEC.adoc @@ -109,25 +109,45 @@ speciation artefact, not a deed. [source] ---- -Deed ::= Header COMMENT* Form +Deed ::= Header Sep? Form Sep? Header ::= SpdxLine+ ; see Section 4.1 -Form ::= "(" DocHead VersionField Field* Clause* ")" + +Sep ::= ( WS | COMMENT )+ ; A COMMENT *is* a separator, so a + ; comment is legal anywhere a + ; separator is — including between + ; the tokens of a form. Mirrors + ; `token-sep` in abnf/deed.abnf. + +Form ::= "(" DocHead Sep VersionField ( Sep ( Field | Clause ) )* Sep? ")" DocHead ::= "estate-deed" | "repo-deed" | "estate-atlas-deed" | "praxis-deed" -VersionField ::= ":schema-version" STRING ; REQUIRED on every head +VersionField ::= ":schema-version" Sep STRING ; REQUIRED on every head -Field ::= KEYWORD Value +Field ::= KEYWORD Sep Value Value ::= STRING | SYMBOL | INTEGER | BOOLEAN | UUID5 | QUOTED | List -List ::= "(" Value* ")" +List ::= "(" ( Value ( Sep Value )* )? Sep? ")" -Clause ::= "(" SYMBOL Field* Clause* ")" +Clause ::= "(" SYMBOL ( Sep ( Field | Clause ) )* Sep? ")" ---- A *Field* is a keyword/value pair. A *Clause* is a named sub-form that may itself carry fields and nested clauses. This is the whole grammar; everything else in a deed is vocabulary, not syntax. +Both layers are order-free and comment-transparent, and they now say so in the +same way. `Sep` above and `token-sep` in `abnf/deed.abnf` are the same +production: a run of whitespace *or comments*, so a comment is legal anywhere a +separator is — between the tokens of a form, not merely before it. Fields and +clauses may appear in any order and may interleave: the repetition is +`( Sep ( Field | Clause ) )*`, deliberately not `Field* Clause*`. A canonical +ordering is a lint convention for diffability, never a parse rule; where +precedence matters — the rules of a praxis deed — it is carried by an explicit +`:priority` INTEGER, never by file position. + +*RULED 2026-09-08 by the owner* on standards#752 — "I think you are right, I am +used to the enbf grammars, is this so for teh anbf, if so please fix." + === Required header Every deed MUST begin with SPDX lines as `;;` comments, before the opening @@ -190,7 +210,7 @@ NOTE: ABNF cannot express negation, so this exclusion is carried as a side condition in both this document and `abnf/deed.abnf`. The side condition is normative: the grammar alone is not sufficient to dispatch a filename. -*RULED 2026-09-09 by the owner* on standards#752 — "yes, let's adopt this, good +*RULED 2026-09-08 by the owner* on standards#752 — "yes, let's adopt this, good idea, the chora replaces the clade of course." *RULED 2026-09-08 by the owner:* `praxis-deed` is a genuine fourth head, not a diff --git a/deed/spec/abnf/deed.abnf b/deed/spec/abnf/deed.abnf index 5634bb82..9576c242 100644 --- a/deed/spec/abnf/deed.abnf +++ b/deed/spec/abnf/deed.abnf @@ -10,7 +10,7 @@ deed = header *comment form header = 1*spdx-line -spdx-line = ";;" SP "SPDX-" 1*(VCHAR / SP) line-end +spdx-line = ";;" SP "SPDX-" 1*text-char line-end form = "(" doc-head token-sep version-field *(token-sep (field / clause)) [token-sep] ")" @@ -26,7 +26,7 @@ estate-file = "estate_chora.deed" ; -> estate-deed atlas-file = "ATLAS.deed" ; -> estate-atlas-deed praxis-file = stem "_praxis.deed" ; -> praxis-deed repo-file = stem "_chora.deed" ; -> repo-deed -stem = 1*( ALPHA / DIGIT / "-" / "." ) +stem = 1*( ALPHA / DIGIT / "-" / "." / "_" ) ; SIDE CONDITION (normative, and NOT expressible in ABNF, which has no ; negation): in repo-file, MUST NOT be the exact string "estate". @@ -34,7 +34,7 @@ stem = 1*( ALPHA / DIGIT / "-" / "." ) ; implementation MUST test estate-file BEFORE repo-file and MUST NOT parse ; estate_chora.deed as a repo-deed. Dispatch is exact-stem-first. ; See ../DEED-GRAMMAR-SPEC.adoc#chora-dispatch-exclusion. -; RULED 2026-09-09 by the owner on standards#752. +; RULED 2026-09-08 by the owner on standards#752. field = keyword token-sep value clause = "(" symbol *(token-sep (field / clause)) [token-sep] ")" @@ -63,6 +63,12 @@ UTF8-4 = %xF0 %x90-BF 2UTF8-tail / %xF1-F3 3UTF8-tail / %xF4 %x80-8F 2UTF8-tail UTF8-tail = %x80-BF +; Comments and SPDX payloads are UTF-8, NOT ASCII. The lexical section of the +; spec says "a deed is a sequence of UTF-8 bytes", and the header the spec +; MANDATES carries "©" (%xC2 %xA9) — which VCHAR (%x21-7E) rejects. Before +; this rule, the normative grammar rejected the specification's own example. +text-char = VCHAR / SP / UTF8-2 / UTF8-3 / UTF8-4 + integer = [ "-" ] 1*DIGIT boolean = "#t" / "#f" ; never "true", never "yes" uuid5 = "#u5" string ; body is the NAME input to @@ -70,7 +76,7 @@ uuid5 = "#u5" string ; body is the NAME input to ; estate namespace token-sep = 1*(WSP / line-end / comment) line-end = CRLF / LF -comment = ";" *( VCHAR / SP ) line-end +comment = ";" *text-char line-end ; Order is not semantic. Fields and clauses are order-free; a canonical ; ordering is a lint convention for diffability, never a parse rule. From ba8dbd364dd18a16396bf10f722a156241fffcf6 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 9 Sep 2026 01:27:27 +0100 Subject: [PATCH 6/8] spec(deed): make the ABNF start rule mirror the EBNF, and stop rejecting ")\n" at EOF MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 3c616d0c rewrote the EBNF start rule to `Deed ::= Header Sep? Form Sep?` but left the ABNF's `deed = header *comment form` untouched — reintroducing, at the start rule, exactly the two-layers-disagree defect that commit set out to close. The ABNF was the wrong one, in two places: * After `form` it permitted NOTHING. A file ending ")\n" — which is every file any editor saves — did not match the grammar. The EBNF's trailing `Sep?` accepts it. * Between `header` and `form` it permitted only `*comment`. A blank line is a bare `line-end`, not a comment, so a header followed by an empty line and then "(" was rejected. The EBNF's leading `Sep?` accepts it. Now `deed = header [token-sep] form [token-sep]`, which is `Header Sep? Form Sep?` exactly. `token-sep = 1*(WSP / line-end / comment)` already subsumes the old `*comment`, so no comment placement is lost; the `comment` rule stays reachable through `token-sep`. Checked before committing: no example in DEED-GRAMMAR-SPEC.adoc puts a blank line between the SPDX header and the opening "(", so the old rule did not reject the spec's own examples a second time. The ")\n" gap, however, applied to all of them. Not changed, surfaced for the owner instead: `text-char = VCHAR / SP / UTF8-2/3/4` excludes HTAB (%x09), so a tab inside a comment is rejected while `token-sep` accepts tabs via `WSP`. Zero comments in either document currently contain a tab, so this rejects nothing that exists. Whether `text-char` should read `WSP` rather than `SP` is a design choice, not a defect to fix unasked. Verified: asciidoctor exit 0, no warnings, 9

, and the anchor, "EXCLUDES", the interleaved repetition and the consistency prose all still present in the rendered output. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01QNjWX2B4FffG7zqMBMui6v --- deed/spec/abnf/deed.abnf | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deed/spec/abnf/deed.abnf b/deed/spec/abnf/deed.abnf index 9576c242..121d7a86 100644 --- a/deed/spec/abnf/deed.abnf +++ b/deed/spec/abnf/deed.abnf @@ -7,7 +7,7 @@ ; NOTE: there is no "key = value" production and no "[section]" production. ; The only bracket is "(". A file using "=" is not a deed. -deed = header *comment form +deed = header [token-sep] form [token-sep] header = 1*spdx-line spdx-line = ";;" SP "SPDX-" 1*text-char line-end From 14ed3374e4e70ffdbdfef740a6272e92e4a7300c Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 9 Sep 2026 08:39:45 +0100 Subject: [PATCH 7/8] spec(deed): cite BaseVocab.idr as a cross-repo URL, not a bare path Hypatia SD022 (alert 833) flags `src/A2ML/` at DEED-GRAMMAR-SPEC.adoc:1 as a path that does not exist in the tree, "likely surviving a directory rename". It is a false positive. `src/A2ML/BaseVocab.idr` DOES exist -- in hyperpolymath/a2ml (6580 bytes on main), which is what the citation said in prose. Hypatia is a repo-local scanner and cannot follow a cross-repo reference, so a fully-qualified `owner/repo@ref:path` string reads to it as a local path. The citation was correct; only its FORM misled the scanner. Rewritten as an asciidoc external link, which is unambiguously not a local path, and which also gives a human reader something clickable. The claim is unchanged. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01QNjWX2B4FffG7zqMBMui6v --- deed/spec/DEED-GRAMMAR-SPEC.adoc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/deed/spec/DEED-GRAMMAR-SPEC.adoc b/deed/spec/DEED-GRAMMAR-SPEC.adoc index 4bb312ca..dd80d712 100644 --- a/deed/spec/DEED-GRAMMAR-SPEC.adoc +++ b/deed/spec/DEED-GRAMMAR-SPEC.adoc @@ -57,8 +57,8 @@ against *20* occurrences of `a2ml`. No tool in the estate scans a `.deed` file today. *Fact 3 — the identity primitive already exists, compiles, and is decidable.* -`hyperpolymath/a2ml@main:src/A2ML/BaseVocab.idr` — a path in the *a2ml* -repository, not in this one — builds clean (11/11 modules, `%default total`) and its +https://github.com/hyperpolymath/a2ml/blob/main/src/A2ML/BaseVocab.idr[`BaseVocab.idr`] +— which lives in the *a2ml* repository, not in this one — builds clean (11/11 modules, `%default total`) and its own header states its purpose: "the anti-desync primitive: one neutral shape for a thing that can be identified, located, attributed, and integrity-checked. It names no downstream consumer." From 5ec48f1be265535c91d4044048bb363fb17893bd Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 9 Sep 2026 09:27:25 +0100 Subject: [PATCH 8/8] spec(deed): drop bare CR from WS so the EBNF matches the normative ABNF The lexical table let `WS` be "space, tab, CR, LF", but the normative grammar in `abnf/deed.abnf` defines `token-sep = 1*(WSP / line-end / comment)` with `line-end = CRLF / LF`, and core-ABNF `WSP` is SP/HTAB only. A bare-CR-separated deed therefore satisfied the informative EBNF while being rejected by the normative parser. The ABNF is normative and CRLF/LF is the intended contract, so the fix is to the table, not the ABNF. `spdx-line` and `comment` already end in `line-end`, so the contract is now uniform across all three. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01QNjWX2B4FffG7zqMBMui6v --- deed/spec/DEED-GRAMMAR-SPEC.adoc | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/deed/spec/DEED-GRAMMAR-SPEC.adoc b/deed/spec/DEED-GRAMMAR-SPEC.adoc index dd80d712..c1163aa9 100644 --- a/deed/spec/DEED-GRAMMAR-SPEC.adoc +++ b/deed/spec/DEED-GRAMMAR-SPEC.adoc @@ -87,7 +87,10 @@ identical input bytes. |=== | `COMMENT` | `;;` to end of line. A single `;` is also a comment; `;;` is the convention for a whole-line comment and `;` for a trailing one. -| `WS` | space, tab, CR, LF. Insignificant except as a token separator. +| `WS` | space, tab, LF, CRLF. Insignificant except as a token separator. + Bare `CR` is *not* a separator: the normative `line-end` in + `abnf/deed.abnf` is `CRLF / LF`, and that contract holds for + comments and SPDX lines alike. | `SYMBOL` | `[A-Za-z][A-Za-z0-9.*/<>=!?+-]*`. Dots are structural: `Type.Software.Library` is one symbol whose dotted segments are meaningful to the type resolver. | `KEYWORD` | `:` followed by a `SYMBOL`. Hyphen, never underscore: `:schema-version`.