From 545a7ebbd4172d4a5b6b3d113f207d15e3a37232 Mon Sep 17 00:00:00 2001 From: Kinflou Date: Mon, 9 Nov 2026 17:02:03 +0800 Subject: [PATCH 1/3] Proposals: a shared vocabulary, and granular @unverified A catalog of the names several programs agree on (encodings, guarantees, facts and their values, conformance features, annotations, diagnostic codes, CI targets), with sets as queries over it. And an optional keyed @unverified that names each guarantee with its own reason, at the scope the guarantee has, checked against what core computes. Both draft. --- docs/docs/proposals/index.md | 15 ++ .../proposals/shared-vocabulary/catalog.md | 160 ++++++++++++++++++ .../shared-vocabulary/granular-unverified.md | 122 +++++++++++++ .../docs/proposals/shared-vocabulary/index.md | 98 +++++++++++ docs/mkdocs.yml | 4 + 5 files changed, 399 insertions(+) create mode 100644 docs/docs/proposals/shared-vocabulary/catalog.md create mode 100644 docs/docs/proposals/shared-vocabulary/granular-unverified.md create mode 100644 docs/docs/proposals/shared-vocabulary/index.md diff --git a/docs/docs/proposals/index.md b/docs/docs/proposals/index.md index 20f228c..7d4ce18 100755 --- a/docs/docs/proposals/index.md +++ b/docs/docs/proposals/index.md @@ -121,6 +121,21 @@ to the same shape: - [Proposal D — keep `@unchecked`](guarantee-marker/unchecked.md): the original name. *rejected: says neither who nor what.* +#### [A shared vocabulary](shared-vocabulary/index.md) + +One catalog of the names several programs agree on (encodings, guarantees, +facts and their values, conformance features, annotations, diagnostic codes, +CI targets), with sets as queries over it, read by core, the runtimes, the +generators, the language server, the Observatory and the docs. Two parts, +read in order: + +- [The catalog](shared-vocabulary/catalog.md): entries, kinds, sets, + relations, and where the catalog lives. *draft.* +- [Granular `@unverified`](shared-vocabulary/granular-unverified.md): an + optional keyed form naming each guarantee with its own reason, at the + scope that guarantee has, checked against what core computes. Revisits part + of the guarantee-marker decision. *draft.* + ### Connections - [Connections](connections.md): what a connection carries beyond one client diff --git a/docs/docs/proposals/shared-vocabulary/catalog.md b/docs/docs/proposals/shared-vocabulary/catalog.md new file mode 100644 index 0000000..b87b3e3 --- /dev/null +++ b/docs/docs/proposals/shared-vocabulary/catalog.md @@ -0,0 +1,160 @@ +# The catalog + +Status: **draft** · part of [A shared vocabulary](index.md) + +**The idea:** every name that more than one program needs to agree on is an +entry in one catalog. Code refers to an entry by its id, and each set of names +is a query over the catalog rather than a hand-kept list. + +## An entry + +```cue +facts: struct_fields: { + kind: "fact" + applies_to: "format" + title: "struct fields" + description: "How a struct's fields are written: in declaration order, or by name." + values: { + by_position: "fields back to back, in declaration order" + by_name: "each field keyed by its name" + } + proven_by: "vectors" + since: "spec-0.6" + status: "stable" +} + +encodings: "jsonrpc@1": { + kind: "framing" + aliases: ["jsonrpc", "json-rpc"] + facts: {calls: "by_name", directions: "both", payload: "json"} + vectors: true + tags: ["official"] + status: "stable" +} + +guarantees: bounded_size: { + kind: "guarantee" + title: "bounded size" + description: "Every value has a maximum size, so a decoder refuses an oversized one before allocating it." + scopes: ["protocol", "function", "argument", "type"] +} +``` + +Illustrative, in CUE since the conformance specs already use it. The model is +what matters, not the syntax. + +| Field | Meaning | +|---|---| +| **id** | The stable name. For a wire name it is the published spelling and never changes; a rename adds an entry and deprecates the old one. | +| **kind** | `format`, `framing`, `handshake`, `guarantee`, `fact`, `feature`, `annotation`, `setting`, `diagnostic`, `fuzz-target`, `bench`, `report`, and more as needed. | +| **tags** | Free labels that sets are built from: `official`, `nightly`, `1.0`, `no_std`, `experimental`. | +| **title, description** | One source for hover text, docs tables, diagnostics and generated comments. | +| **values** | For a fact or setting, the value domain, each value with its meaning. | +| **aliases** | Other accepted spellings, resolved to the id (`json-rpc` → `jsonrpc@1`). | +| **status, since** | `experimental`, `stable` or `deprecated (use X)`, and the catalog or spec version it arrived in. | +| **relations** | References to other entries: an encoding's facts, the guarantees a handshake establishes, the scopes a guarantee applies at. | + +## Kinds worth covering + +Every kind where one source would remove copies. In rough order of value: + +1. **Encodings, handshakes, their facts and value domains.** These are the + most duplicated, and the most dangerous to get wrong. +2. **Guarantees.** Core's `Guarantee`, the `accept_unverified` lists, the + language server's acceptance code, the docs and granular `@unverified`. +3. **Conformance features and report keys.** `features.json`, the spec + versions, and the Observatory's expected reports. +4. **Annotations and settings keys.** Today unknown ones are silently ignored + (core#171, core#178). With entries they can be refused, completed in the + editor and documented from one place. +5. **Diagnostic codes**, with explanations for the CLI and the language + server. +6. **Fuzz, bench and other CI targets.** The CI matrices, the Observatory's + `expect:` lists and the READMEs are generated from a set. + +## Sets + +A set is a query, so it can't drift from the entries (illustrative): + +```cue +sets: { + wire_formats: [for id, e in encodings if e.kind == "format" {id}] + nightly_fuzz: [for id, e in targets if e.kind == "fuzz-target" && list.Contains(e.tags, "nightly") {id}] + format_facts: [for id, f in facts if f.applies_to == "format" {id}] + "spec-0.10": [for id, f in features if f.since <= "spec-0.10" {id}] +} +``` + +A consumer asks for a set by name. Generated code exposes the sets that code +needs as constants: a `&[&str]`, an enum, a TypeScript union. + +## Relations + +This is the open question with the most at stake. The catalog could stop at +*what exists*, or it could also state the rules that connect entries: + +- a handshake **establishes** guarantees (`comline@1` → schema and encoding agreement); +- an encoding with vectors **keeps** `encoding_conformance`; +- a framing's `payload` must **fit** a format's `output` (the encoding-pair rule); +- `comline@2`'s `same_version_differs = warn` **gives up** `version_honesty`. + +Today each of these is code in core (`unverified::causes`, `misfit`), and +some are repeated in the generators. Stating them as data means the compiler, +the conformance engine, the language server and the docs all apply one set of +rules, and a third party's declarations get the same rules. The cost is that +the rule language has to stay small. **Suggested:** state the relations that are +plain references (establishes, keeps, gives up, applies to), and keep logic +that compares values (`fit`) in code that reads the catalog. + +## Where it lives + +Undecided. The options: + +| | A. Its own repository (`comline-vocabulary`) | B. In `core` | C. In `docs` | +|---|---|---|---| +| Who depends on it | everyone, and it depends on nothing | everyone already pins core | nobody pins docs today | +| Fits the dependency order | yes: it sits below core, runtime and the generators | runtime and generators already depend on core, so no new edges, but runtime would pin core for names alone | it would need a published artifact | +| Third-party view | clearly the vocabulary, not one program's | reads as core's internals | reads as documentation | +| Cost | one more repository, rev and CI | lowest | low, but odd for code to depend on | + +**Suggested: A**, a small repository holding the CUE sources and the +generated outputs (a `no_std` Rust crate, a TypeScript module, JSON for +anything else), versioned on its own. Everything pins it the way the +generators pin core today. B is the fallback if one more repository isn't +worth it yet. + +**Format: CUE as the source.** It is already used for the conformance specs, +it validates (a fact's value must be in its domain), it computes sets, and it +exports JSON. Generated outputs are committed and checked in CI, the same way +`comline.h` is checked against cbindgen. + +## How each consumer reads it + +| Consumer | Reads | Replaces | +|---|---|---| +| **core** | Generated Rust: guarantees, facts, value domains, official encodings, aliases, annotations, settings keys, diagnostic codes. At build time, a package's own encoding declarations merge in with the same shape. | `Guarantee::name`, `encodings/profile.rs`, `official.rs`'s tables, `official_units.json` | +| **runtime** | Generated Rust constants: `FORMAT_*`, `FRAMING_*`, `HANDSHAKE_*`, the conformance `Fact` names, feature ids. | `contract/names.rs`, `Fact::name`, `features.json` | +| **conformance specs** | The CUE directly. | the fact domains in `profile.cue` | +| **generators** | Generated Rust/TS: names, plus titles for generated docs. | strings in `generation`, comline-rust and comline-typescript | +| **language server** | Generated Rust: completion, hover and quick fixes, deprecations with replacements. | its own lists and acceptance strings | +| **Observatory** | JSON: the expected report keys per set. | `expect:` lists in workflows | +| **CI** | Generated matrices (fuzz targets, bench targets). | hand-kept YAML lists | +| **docs** | Generated tables (encodings, facts, guarantees, features). | hand-kept tables | + +## The case for it + +- **One edit per change.** Adding a fact value, deprecating an alias or adding + a fuzz target touches the catalog and nothing else. +- **Unknown names become errors.** Typos in annotations, settings keys and + acceptances stop passing silently. +- **Tooling for free.** The language server and docs get descriptions and + deprecations without separate upkeep. +- **Third parties are judged by the same rules,** as with the encoding-pair facts. + +## The case against + +- **One more thing to version and pin,** in a project where revs already cascade + across repositories. +- **Generated code in every repository** needs a regeneration check in CI. +- **Rules as data** can grow into a language of its own if relations aren't + kept to plain references. diff --git a/docs/docs/proposals/shared-vocabulary/granular-unverified.md b/docs/docs/proposals/shared-vocabulary/granular-unverified.md new file mode 100644 index 0000000..16926f7 --- /dev/null +++ b/docs/docs/proposals/shared-vocabulary/granular-unverified.md @@ -0,0 +1,122 @@ +# Granular `@unverified` + +Status: **draft** · part of [A shared vocabulary](index.md) · revisits part +of [Marking a given-up guarantee](../guarantee-marker/index.md) + +**The question.** `@unverified = "reason"` marks a whole protocol, with one +reason, and core works out which guarantees it gives up. Should the author +be able to name the guarantees, give each its own reason, and mark less than +a whole protocol? + +## What was decided, and what it already covers + +[Proposal C](../guarantee-marker/unverified.md) was chosen over naming the +guarantees ([A](../guarantee-marker/waives.md), [B](../guarantee-marker/assumes.md)), +because naming them "would only repeat" what core computes. Two refinements +closed most of the risk: + +- a consumer's `accept_unverified` records the **set** core worked out, so a + dependency that gives up one more guarantee needs a new acceptance; +- the set is **frozen** into the compiled schema, so the author's own version + comparison reports it growing as a major change. + +Those stay. This proposal doesn't reopen *whether* core computes the set. + +## What it doesn't cover + +1. **One reason for everything.** A protocol that gives up + `encoding_conformance` (a framing without vectors) and `bounded_size` (an + unbounded `bytes` argument) explains both in one string. Generated docs and + hover text can't say which reason belongs to which guarantee, and for a + third-party encoding they can't name the cause at all (generation#93). +2. **The scope is always the protocol.** `bounded_size` comes from a type: one + unbounded argument anywhere a protocol reaches marks the whole protocol, + and the diagnostic says only "a string, list or nesting it reaches has no + maximum". Marking that one argument would say where, and would leave the + rest of the protocol verified. +3. **The schema text doesn't say what's given up.** This was accepted for C, + on the grounds that tooling shows it. With a shared vocabulary the cost of + writing it drops, and a reviewer reading a diff sees it without tooling. +4. **The author's acknowledgement is implicit.** The version comparison catches + the set growing *between releases*. While a change is being developed, a + marker written for one guarantee silently covers a second. + +## Proposal + +**Keep `@unverified = "reason"`, and allow a keyed form that names +guarantees, at the scope each guarantee has.** Core still computes the set, +and checks the author's form against it. + +```ids +@framing = "com.acme.f@1" +@unverified(encoding_conformance = "com.acme.f@1 ships no vectors yet") +protocol Billing { + function charge(order: Order) -> Receipt; + + function upload( + @unverified(bounded_size = "legacy gateway blob, sized by the gateway") + data: bytes + ); +} +``` + +- **The plain form stays valid.** It acknowledges whatever core computes, + exactly as today, so nothing existing breaks. +- **The keyed form names guarantees.** Each key is a guarantee from the + vocabulary and each value is its reason. Core computes the set as today, and: + - a computed guarantee the author didn't name is an **error** ("`Billing` + also gives up `schema_agreement`: handshake `none`"); + - a named guarantee core doesn't find given up is a **warning**, like a + needless marker today; + - an unknown key is an **error**, with the vocabulary's spellings suggested. +- **Scopes come from the vocabulary.** Each guarantee lists where it can be + marked. `schema_agreement`, `encoding_agreement` and `version_honesty` come + from the handshake, so they apply to a protocol (or a package's defaults). + `encoding_conformance` comes from the encodings, so a protocol. + `bounded_size` comes from types, so a protocol, a function, an argument, a + field or a type. Marking at the wrong scope is an error. +- **What's frozen** is each given-up guarantee with its scope (`Billing`, + `Billing.upload(data)`) and its reason. Acceptances and the version + comparison work on that, so narrowing a marker is visible and widening one + is a major change. +- **Acceptance stays per protocol** (`accept_unverified = { Billing = [...] }`). + A consumer accepts the protocol's whole set, inner scopes included. Whether + acceptance should also name scopes is an open question below. + +## Options considered + +| | A. Today, plus narrower scopes | B. Plain or keyed (proposed) | C. Keyed only | +|---|---|---|---| +| Existing schemas | unchanged | unchanged | all must be rewritten | +| Says what's given up, in the text | no | when keyed | always | +| A reason per guarantee | no | yes | yes | +| Catches a second guarantee while developing | no | when keyed | yes | +| Grammar work | an annotation on arguments and fields | keyed annotation values (core#124), plus A's | same as B | +| Repeats what core computes | no | only where the author chooses | always, which was the objection to the earlier Proposal A | + +**B** lets a package that wants precision have it, and costs nothing to a +package that doesn't. A `settings` switch (`annotations.unverified.keyed = +"required"`) could let a package or an organisation require the keyed form, +which gives C's guarantees where they're wanted. + +## Depends on + +- **The vocabulary**, for guarantee names, descriptions and scopes, so + core, the language server, diagnostics and generated docs agree. +- **Keyed annotation values** (core#124). Today an annotation's value is a + scalar, and a list is parsed as validator calls. +- **Annotations on arguments and fields.** `bounded_size` at argument scope + needs a marker there. Check this against how bounds attach today (core#98). + +## Open questions + +- **Acceptance by scope:** should `accept_unverified` be able to accept + `Billing.upload` alone, or is accepting the protocol's whole set enough? +- **Package-level defaults:** whether `config.idp` can carry a keyed marker for + every protocol in the package (for example, a package-wide `handshake = + "none"`). +- **Inheritance:** whether a function-scope marker covers every argument, and + whether a type-scope marker covers every use of the type. +- **The word.** The keyed form is close to the earlier Proposal A + (`@waives(…)`). Keeping `@unverified` for both forms means one marker to + learn, and that is the assumption here. diff --git a/docs/docs/proposals/shared-vocabulary/index.md b/docs/docs/proposals/shared-vocabulary/index.md new file mode 100644 index 0000000..5aa6776 --- /dev/null +++ b/docs/docs/proposals/shared-vocabulary/index.md @@ -0,0 +1,98 @@ +# A shared vocabulary + +Status: **draft** · two parts, read in order: +[the catalog](catalog.md), then [granular `@unverified`](granular-unverified.md) + +**The question.** Comline names many things that several programs have to +agree on: encodings, handshakes, guarantees, facts and their values, +conformance features, annotations, settings keys, diagnostic codes, and fuzz, +bench and report targets. Every repository that needs a name writes it out +as a string and keeps its own list of the sets it belongs to. **Can those names, +and the sets made from them, be defined once and shared by core, the compiler, +the runtimes, the generators, the language server, the Observatory and the +docs?** + +A second question depends on the first. `@unverified` marks a protocol as +giving up guarantees, but the author can't say *which* ones, give each its +own reason, or mark less than a whole protocol. Once guarantees are entries in +a shared vocabulary, a marker can refer to them. + +## What it looks like today + +A name is a literal, copied wherever it's needed: + +| Name | Kind | Written in | +|---|---|---| +| `packed@1`, `comline@2` | encoding, handshake | runtime (~46 files), core (~20), docs (~40), language server | +| `framing-datagram` | conformance feature | runtime, core, comline-typescript, docs | +| `struct_fields`, `unknown_variant` | fact | core's `encodings/profile.rs`, runtime's conformance `profile.rs` (an enum and a hand-written `match` to strings), the conformance CUE specs, docs | +| `schema_agreement`, `bounded_size` | guarantee | core's `Guarantee` (an enum and a `match`), `config.idp` acceptances, the language server, docs | +| `packed_canonical` | fuzz target | the fuzz `Cargo.toml`, two lists in `fuzz.yml`, the fuzz README, the seed generator | + +Sets are kept by hand too. *Which fuzz targets exist*, *which features a spec +version covers*, *which values `calls` can take* and *which names are wire +formats* each live in a CI matrix, a JSON file, a `match` arm or a completion +list. Adding or renaming a name means finding every copy, and nothing checks +that the copies agree. + +Some of the structure already exists. The conformance specs' `profile.cue` +gives each fact its value domain and how it is proven. Core's +`encodings/profile.rs` lists the same facts again, and resolves aliases +(`jsonrpc`, `json-rpc`) in `official.rs`. + +## What this proposes + +1. **[A catalog](catalog.md):** every shared name becomes an entry with a + stable id, a kind, tags, metadata and, where it applies, a value domain, + aliases, a status and relations to other entries. Sets are queries over + kinds and tags. Each consumer reads the catalog, or code generated from it, + instead of keeping its own copy. Official entries and a package's own + declarations (`com.acme.f@1`) have the same shape. +2. **[Granular `@unverified`](granular-unverified.md):** the marker may name + the guarantees it covers, each with its own reason, and may apply at the + scope a guarantee naturally has (a protocol, a function, an argument). + Core keeps working out what is given up, and checks it against what the + author wrote. This revisits part of the + [guarantee-marker decision](../guarantee-marker/index.md); that page's + last open question asks for exactly this fixed vocabulary of guarantees. + +## Rules that hold whatever the details + +- **A published wire name never changes.** `packed@1` and `comline@2` are hashed + into the handshake, so their spelling is protocol. A rename is a new entry, + with the old one deprecated. +- **Third parties are first-class.** Anything the catalog can say about an + official encoding, a package can say about its own, and the same rules + judge both (as for the encoding-pair facts). +- **Nothing new at run time.** The catalog feeds compilers, generators, + tooling and CI. Runtimes keep compile-time constants, with no lookup on the + call path. +- **One change, every consumer.** Adding a name, a value or a set member is an + edit to the catalog plus regeneration. Hand-kept copies are a bug. + +## Rollout + +In stages, each useful on its own, in the order the encoding-facts work used: + +1. **Catalog format and home** decided ([catalog → where it lives](catalog.md#where-it-lives)). + Seed it from `profile.cue`, core's `Guarantee` and the official encodings. +2. **Core reads it:** guarantees, facts, value domains, aliases and official + encodings come from the catalog. Unknown annotation names, settings keys + and diagnostic codes are refused (core#171, core#178). +3. **The runtime and conformance read it:** fact names, conformance + features, and the fuzz and bench target sets. The CI matrices and the + Observatory's expected reports are generated from it. +4. **Granular `@unverified`** in core: grammar, check and freezing. This + needs keyed annotation values (core#124). +5. **Tooling reads it:** language server completion and hover, generated + `@unverified` docs (generation#93), and the docs tables. + +## Open questions + +- Where the catalog lives, and in what format (see [the catalog](catalog.md#where-it-lives)). +- How far relations go: whether the catalog states only *what exists*, or also + rules such as *handshake H establishes guarantee G* and *framing payload + must fit format output*, so `causes()` and `misfit()` stop being written per + repository. +- How catalog versions relate to conformance spec versions and to the IR + format (core#146). diff --git a/docs/mkdocs.yml b/docs/mkdocs.yml index f97f52d..18fe4b0 100755 --- a/docs/mkdocs.yml +++ b/docs/mkdocs.yml @@ -225,6 +225,10 @@ nav: - 'Proposal B': 'proposals/guarantee-marker/assumes.md' - 'Proposal C': 'proposals/guarantee-marker/unverified.md' - 'Proposal D': 'proposals/guarantee-marker/unchecked.md' + - 'A shared vocabulary': + - 'proposals/shared-vocabulary/index.md' + - 'The catalog': 'proposals/shared-vocabulary/catalog.md' + - 'Granular @unverified': 'proposals/shared-vocabulary/granular-unverified.md' extra_css: - stylesheets/nav.css?v=23 # bump on every nav.css change — it is not cache-busted otherwise From 07dde62d029c9fa5a1d10fb4105340f0488e2b4f Mon Sep 17 00:00:00 2001 From: Kinflou Date: Mon, 9 Nov 2026 18:04:08 +0800 Subject: [PATCH 2/3] Shared vocabulary: record the leanings so far The catalog lives in a spec repository with the conformance specs and vectors, in CUE, with relations as plain references. Granular @unverified gets scopes per guarantee, outer-covers-inner with a strict opt-in, acknowledgement once per package along a chain, pinned to the chain, acceptance per protocol, failing closed, and the tests that prove the invariant. --- .../proposals/shared-vocabulary/catalog.md | 49 +++-- .../shared-vocabulary/granular-unverified.md | 184 +++++++++++++----- .../docs/proposals/shared-vocabulary/index.md | 34 ++-- 3 files changed, 190 insertions(+), 77 deletions(-) diff --git a/docs/docs/proposals/shared-vocabulary/catalog.md b/docs/docs/proposals/shared-vocabulary/catalog.md index b87b3e3..e7e9f0d 100644 --- a/docs/docs/proposals/shared-vocabulary/catalog.md +++ b/docs/docs/proposals/shared-vocabulary/catalog.md @@ -90,8 +90,8 @@ needs as constants: a `&[&str]`, an enum, a TypeScript union. ## Relations -This is the open question with the most at stake. The catalog could stop at -*what exists*, or it could also state the rules that connect entries: +**Leaning: plain references.** The catalog could stop at *what exists*, or it +could also state the rules that connect entries: - a handshake **establishes** guarantees (`comline@1` → schema and encoding agreement); - an encoding with vectors **keeps** `encoding_conformance`; @@ -102,26 +102,41 @@ Today each of these is code in core (`unverified::causes`, `misfit`), and some are repeated in the generators. Stating them as data means the compiler, the conformance engine, the language server and the docs all apply one set of rules, and a third party's declarations get the same rules. The cost is that -the rule language has to stay small. **Suggested:** state the relations that are -plain references (establishes, keeps, gives up, applies to), and keep logic -that compares values (`fit`) in code that reads the catalog. +the rule language has to stay small. So the catalog states the relations that +are plain references (establishes, keeps, gives up, applies to, scopes), and +logic that compares values (`fit`) stays in code that reads the catalog. ## Where it lives -Undecided. The options: +**Leaning: a spec repository.** Third parties never edit the catalog: they +declare their own entries (`com.acme.f@1`) in `config.idp`, in the same shape. +What they need from it is what they implement against: the names, the facts +and their domains, and the conformance cases that prove them. That is the +spec, and today its other half, the conformance specs and vectors, sits in +`runtime/conformance`, although a Go or Swift runtime implements against those +and not against the Rust runtime. -| | A. Its own repository (`comline-vocabulary`) | B. In `core` | C. In `docs` | +So the vocabulary lives in **one spec repository** with: + +- the catalog (CUE); +- the conformance specs (`profile.cue`, `features.json`) and vectors, moved out + of `runtime/conformance`; +- compiler conformance cases (see [granular `@unverified`](granular-unverified.md#testing-the-invariant)); +- generated outputs: a `no_std` Rust crate, a TypeScript module, and JSON for + everything else. + +It is versioned as the spec ("spec 0.10" is already how the conformance +corpus is versioned). Everyone, this project's own core, runtime and +generators included, pins the spec the way a third party would. The Rust +conformance engine and reference stay in `runtime`. + +The options that were weighed: + +| | Spec repository | Vocabulary-only repository | In `core` | |---|---|---|---| -| Who depends on it | everyone, and it depends on nothing | everyone already pins core | nobody pins docs today | -| Fits the dependency order | yes: it sits below core, runtime and the generators | runtime and generators already depend on core, so no new edges, but runtime would pin core for names alone | it would need a published artifact | -| Third-party view | clearly the vocabulary, not one program's | reads as core's internals | reads as documentation | -| Cost | one more repository, rev and CI | lowest | low, but odd for code to depend on | - -**Suggested: A**, a small repository holding the CUE sources and the -generated outputs (a `no_std` Rust crate, a TypeScript module, JSON for -anything else), versioned on its own. Everything pins it the way the -generators pin core today. B is the fallback if one more repository isn't -worth it yet. +| What a third party pins | the whole spec: names, facts, vectors and cases | the names, and the vectors separately from `runtime` | a Rust compiler's repository, and every core release | +| Language-neutral | yes: CUE and JSON | yes | no | +| Cost | one more repository, plus moving the conformance corpus | one more repository | lowest | **Format: CUE as the source.** It is already used for the conformance specs, it validates (a fact's value must be in its domain), it computes sets, and it diff --git a/docs/docs/proposals/shared-vocabulary/granular-unverified.md b/docs/docs/proposals/shared-vocabulary/granular-unverified.md index 16926f7..01bd085 100644 --- a/docs/docs/proposals/shared-vocabulary/granular-unverified.md +++ b/docs/docs/proposals/shared-vocabulary/granular-unverified.md @@ -6,7 +6,7 @@ of [Marking a given-up guarantee](../guarantee-marker/index.md) **The question.** `@unverified = "reason"` marks a whole protocol, with one reason, and core works out which guarantees it gives up. Should the author be able to name the guarantees, give each its own reason, and mark less than -a whole protocol? +a whole protocol, without making it any easier to lose a guarantee unnoticed? ## What was decided, and what it already covers @@ -32,20 +32,33 @@ Those stay. This proposal doesn't reopen *whether* core computes the set. 2. **The scope is always the protocol.** `bounded_size` comes from a type: one unbounded argument anywhere a protocol reaches marks the whole protocol, and the diagnostic says only "a string, list or nesting it reaches has no - maximum". Marking that one argument would say where, and would leave the - rest of the protocol verified. + maximum". 3. **The schema text doesn't say what's given up.** This was accepted for C, - on the grounds that tooling shows it. With a shared vocabulary the cost of - writing it drops, and a reviewer reading a diff sees it without tooling. + on the grounds that tooling shows it. With a shared vocabulary, writing it + costs little, and a reviewer reading a diff sees it without tooling. 4. **The author's acknowledgement is implicit.** The version comparison catches the set growing *between releases*. While a change is being developed, a marker written for one guarantee silently covers a second. +5. **Chains across packages aren't explicit.** When package A's type gives up a + guarantee, B uses it, and C uses B, nothing requires B and C to see A's + cause and acknowledge it themselves. + +## The safety invariant + +Everything below serves one rule, which has to hold with no exceptions: + +> **If a package compiles, every guarantee given up anywhere a protocol +> reaches, through any chain of types and packages, has been acknowledged in +> that package and accepted by every consumer of that protocol. Every +> acknowledgement and acceptance is pinned to the exact causes it covered, +> so any change upstream asks again.** ## Proposal -**Keep `@unverified = "reason"`, and allow a keyed form that names -guarantees, at the scope each guarantee has.** Core still computes the set, -and checks the author's form against it. +### Two forms, at any scope + +`@unverified = "reason"` stays valid. An optional keyed form names +guarantees. Both can be written at any scope a given-up guarantee allows: ```ids @framing = "com.acme.f@1" @@ -60,63 +73,136 @@ protocol Billing { } ``` -- **The plain form stays valid.** It acknowledges whatever core computes, - exactly as today, so nothing existing breaks. -- **The keyed form names guarantees.** Each key is a guarantee from the - vocabulary and each value is its reason. Core computes the set as today, and: - - a computed guarantee the author didn't name is an **error** ("`Billing` - also gives up `schema_agreement`: handshake `none`"); - - a named guarantee core doesn't find given up is a **warning**, like a - needless marker today; - - an unknown key is an **error**, with the vocabulary's spellings suggested. -- **Scopes come from the vocabulary.** Each guarantee lists where it can be - marked. `schema_agreement`, `encoding_agreement` and `version_honesty` come - from the handshake, so they apply to a protocol (or a package's defaults). - `encoding_conformance` comes from the encodings, so a protocol. - `bounded_size` comes from types, so a protocol, a function, an argument, a - field or a type. Marking at the wrong scope is an error. -- **What's frozen** is each given-up guarantee with its scope (`Billing`, - `Billing.upload(data)`) and its reason. Acceptances and the version - comparison work on that, so narrowing a marker is visible and widening one - is a major change. -- **Acceptance stays per protocol** (`accept_unverified = { Billing = [...] }`). - A consumer accepts the protocol's whole set, inner scopes included. Whether - acceptance should also name scopes is an open question below. +- **Plain:** acknowledges whatever core computes at that scope, as today. +- **Keyed:** each key is a guarantee from the vocabulary, each value its + reason. Against what core computes: + - a computed guarantee that isn't named is an **error**; + - a named guarantee that isn't given up is a **warning**, like a needless + marker today; + - an unknown key is an **error**, with spellings suggested from the vocabulary. + +### Scopes come from each guarantee + +A guarantee's scopes follow from where its cause sits, and are stated in its +catalog entry. A new guarantee declares its own scopes, and core needs no +special case for it. + +| Guarantee | Comes from | Scopes | +|---|---|---| +| `schema_agreement`, `encoding_agreement` | the handshake | package, protocol | +| `version_honesty` | `comline@2` policies | package, protocol | +| `encoding_conformance` | the format and framing | package, protocol | +| `bounded_size` | types | protocol, function, argument, field, type | + +A marker at a scope its guarantee doesn't allow is an error. + +### Coverage: outer covers inner, strict on request + +By default a marker covers causes inside it: a protocol-level `bounded_size` +covers one unbounded argument, exactly as today, so nothing existing breaks. +Tooling suggests the narrower placement. + +A package can opt into **strict** (`annotations.unverified.strict = true`). The +keyed form is then required, and each marker must sit at the innermost scope +where its cause is. That suits packages that want every given-up guarantee +named where it happens. + +### Chains: once per package, never inherited + +Computing stays transitive, and **a marker never subtracts** from it. Core +walks every type a protocol reaches, into dependencies' frozen IR, and finds +every cause. A marker only acknowledges. + +Acknowledgement is **per package, never inherited:** + +```text +A::Blob = bytes A marks it: @unverified(bounded_size = "legacy gateway") +B::Upload { data: A::Blob } B must acknowledge it (on Upload, the field, or a protocol reaching it) +C::Order { blob: B::Upload } C must acknowledge it too +``` + +- Each package whose types or protocols reach a cause acknowledges it **once**, + anywhere on the path inside that package. Within one package the author + already sees the path; every package boundary asks again. +- A's reason travels along as the **origin**, and is shown at every hop, but + A's marker satisfies only A. +- Diagnostics, `inspect`, hover and generated docs show the whole chain: + *"`C::Orders` gives up `bounded_size`: `C::Order.blob` → `B::Upload.data` → + `A::Blob` (`bytes` without a maximum). A's reason: 'legacy gateway'."* + +### Pinned to the causes + +An acknowledgement, and a consumer's acceptance, records what it covered: each +guarantee with the **chain to each cause**. If A adds a second unbounded field, +or B swaps `A::Blob` for another unverified type, the record no longer +matches, and B, C and every consumer get an error until they acknowledge +again. A guarantee can't be lost by reuse, however many packages it passes +through. + +What's frozen is therefore (guarantee, scope path, chain to the cause, +reason). Narrowing a marker is not a major change, since nothing more is +given up. Widening one, or adding a cause, is. + +### Acceptance stays per protocol + +`accept_unverified = { Billing = [...] }` accepts the protocol's whole frozen +set, inner scopes and chains included. It is pinned like an acknowledgement, +so a new inner cause still asks for re-acceptance. + +### Fail closed + +If the build can't see a dependency's declarations or IR, it counts the +guarantee as given up and refuses. An editor's incomplete view can show a +warning instead, but a build never judges with less than the full picture. +Any path that does is a safety bug. Known today: `compat` and `diff` don't see +a dependency's encoding declarations (core#206). + +## Testing the invariant + +Today there are unit tests (`core/tests/package/unverified.rs`), fuzz targets +for parsing and compiling robustness, and runtime vectors proving that decoders +refuse values over a bound. Nothing tests the invariant across package graphs. +This proposal adds: + +1. **A property test with an independent oracle,** in core. It generates + random package graphs (bounded and unbounded types, chains across + packages, markers at random scopes, acceptances, upstream changes) and checks + that *the build succeeds exactly when the oracle says every hop acknowledged + and every consumer accepted*. It's the same differential idea as the + runtime's `ffi_vs_core`. +2. **A fuzz target** running the same check over arbitrary graphs, in core's + nightly fuzz CI. +3. **Compiler conformance cases** in the spec repository: schema graphs with + their expected given-up sets, chains and errors, as data. Any compiler, the + language server or another tool must reproduce them, the way runtimes must + reproduce bytes today. +4. **An audit** of every place that judges guarantees (the validator, + `compat`, `diff`, `inspect`, the language server) for any path that can see + less than the full picture. ## Options considered | | A. Today, plus narrower scopes | B. Plain or keyed (proposed) | C. Keyed only | |---|---|---|---| | Existing schemas | unchanged | unchanged | all must be rewritten | -| Says what's given up, in the text | no | when keyed | always | +| Says what's given up, in the text | no | when keyed, always under strict | always | | A reason per guarantee | no | yes | yes | -| Catches a second guarantee while developing | no | when keyed | yes | -| Grammar work | an annotation on arguments and fields | keyed annotation values (core#124), plus A's | same as B | +| Catches a second guarantee while developing | no | when keyed, and always under strict | yes | | Repeats what core computes | no | only where the author chooses | always, which was the objection to the earlier Proposal A | -**B** lets a package that wants precision have it, and costs nothing to a -package that doesn't. A `settings` switch (`annotations.unverified.keyed = -"required"`) could let a package or an organisation require the keyed form, -which gives C's guarantees where they're wanted. - ## Depends on -- **The vocabulary**, for guarantee names, descriptions and scopes, so - core, the language server, diagnostics and generated docs agree. +- **The vocabulary**, for guarantee names, descriptions and scopes. - **Keyed annotation values** (core#124). Today an annotation's value is a scalar, and a list is parsed as validator calls. -- **Annotations on arguments and fields.** `bounded_size` at argument scope - needs a marker there. Check this against how bounds attach today (core#98). +- **Markers on arguments and fields.** Check this against how bounds attach + today (core#98). ## Open questions -- **Acceptance by scope:** should `accept_unverified` be able to accept - `Billing.upload` alone, or is accepting the protocol's whole set enough? -- **Package-level defaults:** whether `config.idp` can carry a keyed marker for - every protocol in the package (for example, a package-wide `handshake = - "none"`). -- **Inheritance:** whether a function-scope marker covers every argument, and - whether a type-scope marker covers every use of the type. +- **Package-level markers:** how `config.idp` carries a marker for every + protocol in a package (for example, a package-wide `handshake = "none"`), and + how it counts toward per-package acknowledgement. - **The word.** The keyed form is close to the earlier Proposal A (`@waives(…)`). Keeping `@unverified` for both forms means one marker to learn, and that is the assumption here. diff --git a/docs/docs/proposals/shared-vocabulary/index.md b/docs/docs/proposals/shared-vocabulary/index.md index 5aa6776..6480017 100644 --- a/docs/docs/proposals/shared-vocabulary/index.md +++ b/docs/docs/proposals/shared-vocabulary/index.md @@ -74,25 +74,37 @@ gives each fact its value domain and how it is proven. Core's In stages, each useful on its own, in the order the encoding-facts work used: -1. **Catalog format and home** decided ([catalog → where it lives](catalog.md#where-it-lives)). - Seed it from `profile.cue`, core's `Guarantee` and the official encodings. +1. **The spec repository** ([catalog → where it lives](catalog.md#where-it-lives)): + the catalog in CUE, seeded from `profile.cue`, core's `Guarantee` and the + official encodings, with the conformance specs and vectors moved in from + `runtime/conformance`. 2. **Core reads it:** guarantees, facts, value domains, aliases and official encodings come from the catalog. Unknown annotation names, settings keys and diagnostic codes are refused (core#171, core#178). 3. **The runtime and conformance read it:** fact names, conformance features, and the fuzz and bench target sets. The CI matrices and the Observatory's expected reports are generated from it. -4. **Granular `@unverified`** in core: grammar, check and freezing. This - needs keyed annotation values (core#124). +4. **Granular `@unverified`** in core: grammar, scopes, per-package + acknowledgement pinned to each cause's chain, and freezing. It needs + keyed annotation values (core#124). It lands with its safety tests: a + property test against an oracle, a fuzz target, compiler conformance cases + in the spec repository, and an audit of every path that judges guarantees. 5. **Tooling reads it:** language server completion and hover, generated `@unverified` docs (generation#93), and the docs tables. +## Leanings so far + +- **Home:** a spec repository holding the catalog, the conformance specs and + vectors, and compiler conformance cases, versioned as the spec. +- **Format:** CUE as the source, with generated Rust, TypeScript and JSON. +- **Relations:** plain references only (establishes, keeps, gives up, applies + to, scopes); logic that compares values stays in code. +- **`@unverified`:** plain or keyed, at any scope a guarantee allows. Outer + covers inner, with a strict opt-in. Acknowledged once per package along a + chain, pinned to the chain, accepted per protocol, failing closed. + ## Open questions -- Where the catalog lives, and in what format (see [the catalog](catalog.md#where-it-lives)). -- How far relations go: whether the catalog states only *what exists*, or also - rules such as *handshake H establishes guarantee G* and *framing payload - must fit format output*, so `causes()` and `misfit()` stop being written per - repository. -- How catalog versions relate to conformance spec versions and to the IR - format (core#146). +- How spec versions relate to the IR format's version (core#146). +- Package-level `@unverified` markers in `config.idp` (see [granular + `@unverified`](granular-unverified.md#open-questions)). From 2e1d29f0686e05e69282c1c365402bdde53c936a Mon Sep 17 00:00:00 2001 From: Kinflou Date: Mon, 9 Nov 2026 18:24:15 +0800 Subject: [PATCH 3/3] Shared vocabulary: package defaults, spec upgrades, versions, the word Package-default causes are acknowledged in config.idp next to the setting, covering only that cause. A loss found by a newer spec asks again without a false major change. The spec and IR format versions stay independent, each frozen version recording its spec version, with the spec append-only. @unverified for both forms. The repository is named specification. --- .../proposals/shared-vocabulary/catalog.md | 17 ++++++- .../shared-vocabulary/granular-unverified.md | 50 ++++++++++++++++--- .../docs/proposals/shared-vocabulary/index.md | 16 ++++-- 3 files changed, 71 insertions(+), 12 deletions(-) diff --git a/docs/docs/proposals/shared-vocabulary/catalog.md b/docs/docs/proposals/shared-vocabulary/catalog.md index e7e9f0d..dc4284b 100644 --- a/docs/docs/proposals/shared-vocabulary/catalog.md +++ b/docs/docs/proposals/shared-vocabulary/catalog.md @@ -108,7 +108,7 @@ logic that compares values (`fit`) stays in code that reads the catalog. ## Where it lives -**Leaning: a spec repository.** Third parties never edit the catalog: they +**Leaning: a spec repository, `specification`.** Third parties never edit the catalog: they declare their own entries (`com.acme.f@1`) in `config.idp`, in the same shape. What they need from it is what they implement against: the names, the facts and their domains, and the conformance cases that prove them. That is the @@ -143,6 +143,21 @@ it validates (a fact's value must be in its domain), it computes sets, and it exports JSON. Generated outputs are committed and checked in CI, the same way `comline.h` is checked against cbindgen. +## Versioning + +The spec version and the IR format version stay **independent**: + +- **The spec version** (the vocabulary, the conformance corpus and the compiler + cases) says what implementations must agree on. +- **The IR format version** (`CURRENT_IR_FORMAT_VERSION` in core's CAS) changes + only when the frozen IR's *shape* changes. +- **Each frozen version records the spec version** it was frozen against. +- **The spec is append-only for anything frozen.** Wire names never change. + Guarantees, facts and values can be added and deprecated, but never removed + or redefined, so an old frozen version always reads correctly under a newer + spec. From 1.0 this is what lets a newer release read an older one's IR + (core#146). + ## How each consumer reads it | Consumer | Reads | Replaces | diff --git a/docs/docs/proposals/shared-vocabulary/granular-unverified.md b/docs/docs/proposals/shared-vocabulary/granular-unverified.md index 01bd085..870e4c7 100644 --- a/docs/docs/proposals/shared-vocabulary/granular-unverified.md +++ b/docs/docs/proposals/shared-vocabulary/granular-unverified.md @@ -143,12 +143,48 @@ What's frozen is therefore (guarantee, scope path, chain to the cause, reason). Narrowing a marker is not a major change, since nothing more is given up. Widening one, or adding a cause, is. +### Package-default causes: acknowledged next to the cause + +A package setting can give a guarantee up for every protocol that inherits +it, for example `handshake = "none"` in `config.idp`. Its acknowledgement sits +beside that setting: + +```text +handshake = "none" +unverified = { schema_agreement = "the gateway pins schemas by contract", + encoding_agreement = "the gateway pins schemas by contract" } +``` + +- It covers **only the causes that come from that setting**, and only for the + protocols that inherit it. A protocol with its own handshake isn't + covered, and neither is any other cause (an unbounded type, a framing + without vectors). +- Each covered protocol's frozen record says it was acknowledged at package + scope, with the reason. +- It is pinned like any other marker: if the setting changes, it no longer + matches and the build asks again. +- A blanket package marker covering everything in a package is ruled out. + That is exactly the gap this proposal closes. + ### Acceptance stays per protocol `accept_unverified = { Billing = [...] }` accepts the protocol's whole frozen set, inner scopes and chains included. It is pinned like an acknowledgement, so a new inner cause still asks for re-acceptance. +### A newer spec that finds an existing loss + +The spec can add a guarantee (say, a future "transport fit"), and an existing +protocol may turn out to give it up although its schema didn't change. + +- **Safety:** markers and acceptances are pinned to a set that no longer + matches, so the author and every consumer are asked again. Nothing passes + silently. +- **Version honesty:** `diff` recomputes both versions under the newer spec + before comparing, so the version comparison doesn't report a major change + the author didn't make. The frozen IR keeps the types and parameters this + needs. + ### Fail closed If the build can't see a dependency's declarations or IR, it counts the @@ -198,11 +234,11 @@ This proposal adds: - **Markers on arguments and fields.** Check this against how bounds attach today (core#98). -## Open questions +## The word -- **Package-level markers:** how `config.idp` carries a marker for every - protocol in a package (for example, a package-wide `handshake = "none"`), and - how it counts toward per-package acknowledgement. -- **The word.** The keyed form is close to the earlier Proposal A - (`@waives(…)`). Keeping `@unverified` for both forms means one marker to - learn, and that is the assumption here. +`@unverified` for both forms. The objection to the earlier `@waives(…)` was to +naming guarantees at all, not to the word. Now that naming is optional and +checked, the choice is about readability. `@unverified(bounded_size = "…")` +reads accurately: Comline doesn't verify it. And one word already runs through +the annotation, `accept_unverified`, `annotations.unverified` and the +`unverified::*` diagnostic codes. diff --git a/docs/docs/proposals/shared-vocabulary/index.md b/docs/docs/proposals/shared-vocabulary/index.md index 6480017..81a899b 100644 --- a/docs/docs/proposals/shared-vocabulary/index.md +++ b/docs/docs/proposals/shared-vocabulary/index.md @@ -94,7 +94,7 @@ In stages, each useful on its own, in the order the encoding-facts work used: ## Leanings so far -- **Home:** a spec repository holding the catalog, the conformance specs and +- **Home:** a spec repository, `specification`, holding the catalog, the conformance specs and vectors, and compiler conformance cases, versioned as the spec. - **Format:** CUE as the source, with generated Rust, TypeScript and JSON. - **Relations:** plain references only (establishes, keeps, gives up, applies @@ -103,8 +103,16 @@ In stages, each useful on its own, in the order the encoding-facts work used: covers inner, with a strict opt-in. Acknowledged once per package along a chain, pinned to the chain, accepted per protocol, failing closed. +- **Package defaults:** acknowledged in `config.idp` next to the setting that + causes the loss, covering only that cause. +- **Spec upgrades:** a loss found by a newer spec asks the author and consumers + again, and `diff` recomputes both versions under it, so it is never a false + major change. +- **Versions:** the spec version and the IR format version are independent, + with each frozen version recording its spec version, and the spec + append-only for anything frozen. +- **The word:** `@unverified` for both forms. + ## Open questions -- How spec versions relate to the IR format's version (core#146). -- Package-level `@unverified` markers in `config.idp` (see [granular - `@unverified`](granular-unverified.md#open-questions)). +None blocking. The next step is the `specification` repository (core#220).