diff --git a/deno.jsonc b/deno.jsonc index d0b65b35..35230c9b 100644 --- a/deno.jsonc +++ b/deno.jsonc @@ -54,7 +54,7 @@ // chord_surface (reads the gitignored generated x8F20 migration plan, so it // is non-hermetic — present locally, absent in a fresh CI checkout). Safe to // run in the workspace-stripped CI checkout. Gated by ci.yml. - "test:unit": "deno test --allow-read --allow-write --allow-env --allow-run $(ls src/*_test.ts | grep -vE 'myc_proxy_test|import_map_test|chord_surface_test') probes/substrate-court-v0/ts/court_test.ts probes/receipt-envelope-encoder-v0/ts/test.ts probes/receipt-envelope-encoder-v0/ts/vendor_parity_test.ts probes/spore-runtime-adapter-v0/ts/adapter_test.ts probes/hsp-fast-path-debt-scope-v0/debt_scope_test.ts probes/cnp-0-seed-v0/ts/cnp0_test.ts probes/cnp-0-qwen-cleanroom-v0/ts/harness_test.ts conformance/cnp-0-jcs-v0/ts/kit_test.ts", + "test:unit": "deno test --allow-read --allow-write --allow-env --allow-run $(ls src/*_test.ts | grep -vE 'myc_proxy_test|import_map_test|chord_surface_test') probes/substrate-court-v0/ts/court_test.ts probes/receipt-envelope-encoder-v0/ts/test.ts probes/receipt-envelope-encoder-v0/ts/vendor_parity_test.ts probes/spore-runtime-adapter-v0/ts/adapter_test.ts probes/hsp-fast-path-debt-scope-v0/debt_scope_test.ts probes/cnp-0-seed-v0/ts/cnp0_test.ts probes/cnp-0-qwen-cleanroom-v0/ts/harness_test.ts conformance/cnp-0-jcs-v0/ts/kit_test.ts probes/typed-domain-kernel-v0/ts/kernel_test.ts", "ontology:coverage": "deno run -A src/x6300_ontology_coverage.ts", "cognition:phase-report": "deno run -A src/x2C00_cognition_phase_report.ts", "cognition:snapshot": "deno run -A src/x2400_cognition_snapshot.ts", diff --git a/probes/typed-domain-kernel-v0/README.md b/probes/typed-domain-kernel-v0/README.md new file mode 100644 index 00000000..b3d8ba05 --- /dev/null +++ b/probes/typed-domain-kernel-v0/README.md @@ -0,0 +1,268 @@ +--- +status: active +owner_voice: claude +next_verification: review the boundaries before anything is built on them — this is an interface/evidence package, not an implementation. The five proof obligations below are the output that matters; each is a normative question the RFC leaves open, and each blocks a different downstream tranche. +graduation_target: null +--- + +# typed-domain-kernel-v0 + +> **Interfaces and evidence, not implementations.** No production state domain, +> no translator, no runtime integration. Executable schemas, validators, +> positive fixtures and countermodels — so the boundaries can be reviewed before +> anything rests on them. + +Covers RFC-0003 Tranche B items **B1, B2, B3, B4, B5, B7, B8** as one package in +three layers. B6 (composite state) is out of scope and is the RFC's own open +question about associativity of composition (§6.5.3, §20.19). + +## What this package is FOR + +The RFC's §17.2 table says every primitive here has `existing source: none` and +gives each a "first executable test that fails today because the thing does not +exist". This package makes those tests runnable. It does not make them pass by +building the thing — it makes the **boundaries** checkable, so the thing gets +built against reviewed edges. + +The most useful output is not the types. It is the **five proof obligations**: +places where the RFC states a requirement whose terms it never defines, and +where an implementer's reasonable guess becomes a normative decision nobody +made. + +## Layers and dependency map + +``` +layer 1 domain / capabilities / delta B1 B3 + │ ContentAddress, Capability, DeltaDescriptor, ValidationReport + │ DomainDeclaration + validateDomain + ↓ +layer 2 invariants / context B4 B8 + │ Scope, CostClass, ContextSurface, Freshness + │ InvariantDefinition + InvariantEvaluation + admitEvaluation + │ (imports ContentAddress, ValidationReport, NotAssessedReason) + ↓ +layer 3 laws / policy / version DAG B2 B7 B5 + LawClaim, LawStatus, BoundaryPolicy, Release + decideLaw, decideComposition, validateVersionDag + (imports ContentAddress, PredicateRef, EvidenceRef, FixtureRef) +``` + +Dependencies run one way only. Layer 3 is where the seam is, and it is last +because it needs the reference types the lower layers define — not because law +evidence is downstream of invariants in the RFC's own structure. + +## Closed member sets + +Every enumeration is closed, and a control asserts each against this table. An +open enumeration is a place where "unknown" silently becomes "allowed". + +| set | members | +| --- | --- | +| `Capability` | `comparable` `ordered` `metric` `interpolable` `composable` `geometric` | +| `LawStatusKind` | `proved` `tested` `asserted` `falsified` | +| `Scope` | `state` `transition` `trace` | +| `CostClass` | `constant` `linear` `superlinear` `unbounded` | +| `ContextSurface` | `state` `transition` `trace` `world` `authority` `logical-step` | +| `BoundaryKind` | `local` `translation` `irreversible` `composition` | +| `NotAssessedReason` | `snapshot-stale` `snapshot-missing` `scope-not-available` `cost-class-exceeds-budget` `undeclared-surface-read` | + +`Capability`, `LawStatusKind`, `Scope` and `CostClass` are quoted from the RFC. +`ContextSurface`, `BoundaryKind` and `NotAssessedReason` are **proposed** — see +the ambiguity table. + +## Fail-closed boundary table + +Every refusal has a code. Nothing returns a bare boolean, and nothing falls +through to an accept. + +| boundary | refuses | code | +| --- | --- | --- | +| registry admission | capability declared, method absent | `capability-declared-not-implemented` | +| registry admission | method present, capability undeclared | `capability-implemented-not-declared` | +| registry admission | `move()` without a typed delta space | `geometric-without-delta-descriptor` | +| registry admission | `distance()` without metric axioms | `metric-without-axioms` | +| registry admission | forbidden operation with no reason | `forbidden-without-reason` | +| registry admission | any short handle used as a reference | `non-content-addressed-reference` | +| invariant definition | no falsifier fixture | `no-falsifier` | +| invariant definition | partially-held, no distortion measure | `partial-without-distortion-measure` | +| invariant evaluation | `transition` scope from one state | `missing-predecessor-for-transition` | +| invariant evaluation | `trace` scope from one state | `missing-trace-for-trace-scope` | +| invariant evaluation | `unbounded` gating a fast path | `unbounded-gates-fast-path` | +| invariant evaluation | a surface supplied that the definition never declared | `undeclared-surface-read` | +| law at any boundary | `falsified` — above policy, cannot be opted into | `falsified` | +| law at translation / irreversible | `asserted` — above policy | `asserted-across-boundary` | +| law at any boundary | `tested` with no generation domain | `generation-domain-unstated` | +| law at any boundary | law absent | `law-absent` | +| composition | the two sides declare the law at different scopes | `status-not-accepted` | +| version DAG | patch increment across a law weakening | `patch-across-law-weakening` | +| version DAG | cycle, orphan, or two roots | `cycle` `predecessor-unknown` `multiple-roots` | + +Two outcomes are deliberately **not** refusals — they are `not-assessed`: + +| condition | outcome | why | +| --- | --- | --- | +| cost class over the boundary's budget | `cost-class-exceeds-budget` | reporting it held would be a claim nobody paid for | +| snapshot staler than the freshness requirement | `snapshot-stale` | §6.1.2 rule 5: an invariant that held against a snapshot no longer current has not been shown to hold now | + +`held` / `failed` / `not-assessed` is three-valued because §6.1.2 rule 5 requires +it and the RFC never types `ValidationReport`. Collapsing it to a boolean is how +a boundary comes to believe an invariant held when nobody checked it. + +## Properties, by category + +Codex's warning is the method here, not just one fact: **typedness does not +confer associativity**, and the general form of that mistake is deriving a +property from a shape. Every property is labelled. + +### Structural — follows from the definitions + +| property | why | +| --- | --- | +| capability declaration and implementation agree in both directions | `validateDomain` compares two sets and refuses either asymmetry | +| a `geometric` domain has a content-addressed delta space | admission requires it; the converse is refused too | +| every reference is a full digest | one regex, one refusal code, checked on every reference in a declaration | +| a `transition`/`trace` invariant cannot be established from one state | the required surface is absent, and absence is checked before the predicate runs | +| `falsified` authorizes nothing | checked above policy, so a policy cannot opt in | +| a version DAG is a DAG | single root, no cycle, every predecessor present | + +### Requires a `LawClaim` — does NOT follow, must be declared with evidence + +| property | why not structural | +| --- | --- | +| delta composition is associative | see the countermodel: clamped translations are a well-typed delta space and are not associative | +| `distance` satisfies the triangle inequality | a similarity score is a function too; §6.2 rule 4 exists because naming a metric does not make one | +| `compose` is commutative or idempotent | nothing in the interface constrains it | +| `interpolate` at `t=0`/`t=1` returns the endpoints | not implied by the signature | + +### Has a countermodel — executable, in `fixtures/countermodels/` + +| claim | countermodel | +| --- | --- | +| "`proved` is stronger than `tested`" | `proved-narrower-than-tested.json` — a proof over a narrow precondition versus a test over a strictly wider generation domain. Neither dominates. | +| "a typed delta space composes associatively" | `delta-not-associative.json` — clamped translation, with the arithmetic witness | +| "scope widening preserves the report" | `scope-widening-unpinned.json` — same predicate and state, two legal world snapshots, two different reports | +| "a patch label is always admissible" | `patch-across-law-weakening.json` — the one conflict §6.2.1 rule 3 names | + +**This category is non-empty on purpose.** If a package like this reports no +countermodels, that is not evidence the design is sound; it is evidence nobody +looked. + +## The five proof obligations + +Each is a normative question. None is discharged here, and none is closed by +picking whichever reading is convenient to implement. + +### 1. `LawStatus` has no order, and §6.2 rule 2 requires a minimum over it + +§6.2 rule 2: *"A policy MUST state the minimum status each boundary requires."* +Part 03 repeats it at §7.1 three times. **§6.2 defines no order on `LawStatus`.** + +The text gives exactly two constraints — `falsified` below everything, +`asserted` below the evidenced kinds at translation and irreversible boundaries +— and never relates `proved` to `tested`. `LawClaim.scope`, `LawClaim.precondition` +and `tested.domain` make that gap load-bearing: a `proved` claim over a narrow +precondition and a `tested` claim over a strictly wider generation domain are +incomparable, and ranking `proved` first would let a boundary accept a proof +about a region it does not operate in over evidence about the region it does. + +**This is the same shape the Lean kernel already proved for suitability** — +`proofs/rfc-0003/HSP/Suitability.lean`, `no_meet`, finding C3: a document saying +"the lower of two levels" over an order with no meet. That precedent is why this +package does not invent a total order. + +*Obligation:* either state a partial order on `LawStatus` and prove every pair a +policy must compare has a greatest lower bound, **or** replace "minimum status" +with an accept-set formulation, which needs no order. This package implements +the second as `BoundaryPolicy.accepts` and **does not amend the RFC**. + +**This is the one seam where Lean would decide something**, and the argument for +it is that the analogous theorem already exists next door: `no_meet` is +four-valued, `LawStatus` is four-valued, and the failure mode is identical. The +theorem candidate is stated below. It is not written here, because the normative +question — which of the two repairs the RFC wants — is the steward's, and a +proof of the wrong one is wasted rigour. + +### 2. `InvariantDefinition` has no field for the surfaces §6.1.2 requires it to declare + +§6.1.2 rule 1 obligates the definition to declare which context surfaces its +predicate reads. The type at §6.1.1 has no such field. The obligation exists; +its carrier does not. `reads: ContextSurface[]` is **proposed** here. + +*Obligation:* add the field to §6.1.1's type, or state where else the +declaration lives. + +### 3. `DeltaDescriptor` is required and never defined + +§6 :127-131 requires it, with its own content address, or *"`move` is an untyped +hole in an otherwise typed contract"*. The RFC names the type three times and +never gives its shape. Proposed here as `{address, validate, encoding, +composition?}`, with `composition` optional and **not defaulted to associative**. + +*Obligation:* define it, and say explicitly whether an absent `composition` means +"no claim" (this package's reading) or "no law". + +### 4. The version-label projection is required and never specified + +§6.2.1 rule 2 requires `version` to be a projection of the DAG. Rule 3 requires a +registry to reject a label that "conflicts with its position in the DAG", and +gives exactly one example. Neither the projection function nor the general notion +of conflict is defined. This package checks DAG well-formedness and the one named +conflict, and reports the rest as open. + +*Obligation:* specify the projection, or state that only the named conflict is +normative and the label is otherwise unconstrained. + +### 5. Scope widening is neither permitted nor forbidden + +The RFC refuses checking at a **narrower** scope than declared. It says nothing +about wider. Widening is not obviously safe: a predicate declaring +`reads: [state, world]` evaluated inside a trace context may see a world snapshot +from a different logical step than the state it judges, and §6.1.2 rule 2's +reproducibility guarantee is then a claim about a pairing the RFC never pins. + +*Obligation:* state whether widening preserves reports, and under what constraint +on the logical step of each supplied surface. + +## Theorem candidate, if the steward takes repair (a) for obligation 1 + +``` +For the four-valued LawStatus with the two relations §6.2 rule 2 states, +and for LawClaim carrying scope and precondition: + + (i) the stated relation is a strict partial order; + (ii) `proved` and `tested` are incomparable in it; + (iii) therefore { proved, tested } has no greatest lower bound, + and "the minimum status" is undefined for any policy that must + compare a proved claim against a tested one. +``` + +(iii) is what makes it worth proving rather than asserting: it is the same +conclusion `Suitability.lean`'s `no_meet` reaches, and if it holds then repair +(a) is not available and (b) is forced. **If the steward takes repair (b), no +Lean is needed at all** — an accept set has no order to prove things about, and +adding theorems would be weight rather than evidence. + +## What this package does NOT establish + +- **Not an implementation.** No production domain exists; `validateDomain` + validates a *declaration*, not behaviour. +- **Not conformance.** Nothing here is a conformance result for anything. +- **Not ratification.** Tranche B is not ratified by this package and this + package does not ask for it. +- **Not a completeness claim** about capabilities or context surfaces. §6.4 says + the domain families are "examples, not a normative completeness claim"; the + same caution applies to every closed set here that is proposed rather than + quoted. +- **Not B6.** Composite state and coupling consistency are out of scope, and the + RFC's own open question about whether composition associates (§20.19) is + untouched. + +## Running it + +```sh +deno test --allow-read probes/typed-domain-kernel-v0/ts/kernel_test.ts +``` + +20 controls. Positive fixtures prove the validators admit something; +countermodels prove they refuse, and refuse with the stated code. A validator +that only ever passes is indistinguishable from one that checks nothing. diff --git a/probes/typed-domain-kernel-v0/fixtures/countermodels/delta-not-associative.json b/probes/typed-domain-kernel-v0/fixtures/countermodels/delta-not-associative.json new file mode 100644 index 00000000..d9f86664 --- /dev/null +++ b/probes/typed-domain-kernel-v0/fixtures/countermodels/delta-not-associative.json @@ -0,0 +1,22 @@ +{ + "note": "Typedness does not confer associativity. A DeltaDescriptor with no declared composition law supports NO claim about composing moves.", + "why": "Rotations in R3 compose associatively; a delta space of `clamped translations` (each move clipped to a bounding box) does not \u2014 clamping after each step differs from clamping after the sum. Both are well-typed delta spaces with valid content addresses.", + "delta": { + "address": "sha256:7fd0812e6e7956cf4026175f0a10910cea6135d7fa7348c81f9b70080bea01d7", + "validate": "sha256:05742b145988ec95e3de195b8b2a6b021cb5eaf2d1a31dfa57ba3967304ae099", + "encoding": "hsp-jcs@v0/delta-clamped" + }, + "witness": { + "box": [ + 0, + 10 + ], + "start": 8, + "d1": 5, + "d2": -5, + "left_assoc": "clamp(clamp(8+5)-5) = clamp(10-5) = 5", + "right_assoc": "clamp(8 + clamp(5-5)) = clamp(8+0) = 8", + "equal": false + }, + "expected": "A domain declaring this delta space MUST NOT be assumed composable; `composition` is absent, which means NO CLAIM, not `no law`." +} \ No newline at end of file diff --git a/probes/typed-domain-kernel-v0/fixtures/countermodels/patch-across-law-weakening.json b/probes/typed-domain-kernel-v0/fixtures/countermodels/patch-across-law-weakening.json new file mode 100644 index 00000000..08a54eb5 --- /dev/null +++ b/probes/typed-domain-kernel-v0/fixtures/countermodels/patch-across-law-weakening.json @@ -0,0 +1,19 @@ +{ + "note": "The one conflict \u00a76.2.1 rule 3 names, executable.", + "releases": [ + { + "address": "sha256:70456d3b030385c5d02e32037e45a3c704183a34d235a12ab3385c9e50b10896", + "predecessor": null, + "label": "1.0.0" + }, + { + "address": "sha256:1e1e43e535efe2b4f743dfd1c46de334f6ac7aae362511241acfc7b7639fc8a5", + "predecessor": "sha256:70456d3b030385c5d02e32037e45a3c704183a34d235a12ab3385c9e50b10896", + "label": "1.0.1" + } + ], + "weakened_laws": [ + "sha256:1e1e43e535efe2b4f743dfd1c46de334f6ac7aae362511241acfc7b7639fc8a5" + ], + "expected": "patch-across-law-weakening \u2014 a patch increment across a change that weakened a law." +} \ No newline at end of file diff --git a/probes/typed-domain-kernel-v0/fixtures/countermodels/proved-narrower-than-tested.json b/probes/typed-domain-kernel-v0/fixtures/countermodels/proved-narrower-than-tested.json new file mode 100644 index 00000000..df16ae53 --- /dev/null +++ b/probes/typed-domain-kernel-v0/fixtures/countermodels/proved-narrower-than-tested.json @@ -0,0 +1,26 @@ +{ + "note": "The pair that makes `minimum status` ill-defined. Neither claim dominates.", + "why": "A proved claim restricted to a narrow precondition establishes the law only inside it. A tested claim whose generation domain strictly contains that precondition has been checked over inputs the proof says nothing about. Ranking `proved` above `tested` would let a boundary accept a proof about a region it does not operate in, over evidence about the region it does.", + "proved_but_narrow": { + "status": { + "kind": "proved", + "proof": "sha256:73719a3aa32db1b70cbfb9cb773786579ef06911fff46d5274e3104d411a2927", + "checker": "sha256:92756188df03e3fb67c60f645e6f4b0240cf691482d8cbcc3498eed80a83c84a" + }, + "scope": "partial", + "precondition": "sha256:c6527138805b8a8027d13e540367c81b8a20cfbcdafa5823f6d8dacc9a834f64" + }, + "tested_but_wider": { + "status": { + "kind": "tested", + "generator": "sha256:7fcdb92d6ff95bd2a67002400b846e8d535539997edde12d7eb4a46b4ee6ee93", + "domain": "sha256:8359ed1f2701c13998926920e34da2b971469824d304e5afb07941e5efe8bb5d", + "cases": 100000, + "seed": "0x5eed", + "ref": "sha256:d75339fb68bd66bd83026576068cc62eaaf08873336bbf611a228fc9c7cd192e" + }, + "scope": "total" + }, + "boundary_operates_over": "sha256:8359ed1f2701c13998926920e34da2b971469824d304e5afb07941e5efe8bb5d", + "expected": "Neither is `the minimum`. A policy stating a threshold cannot express this; a policy stating an ACCEPT SET can." +} \ No newline at end of file diff --git a/probes/typed-domain-kernel-v0/fixtures/countermodels/scope-widening-unpinned.json b/probes/typed-domain-kernel-v0/fixtures/countermodels/scope-widening-unpinned.json new file mode 100644 index 00000000..5dd3dfcd --- /dev/null +++ b/probes/typed-domain-kernel-v0/fixtures/countermodels/scope-widening-unpinned.json @@ -0,0 +1,22 @@ +{ + "note": "Why this kernel neither permits nor forbids scope widening.", + "why": "A predicate declaring reads:[state,world] evaluated inside a trace context may see a world snapshot taken at a different logical step than the state it judges. \u00a76.1.2 rule 2 requires reproducibility; the pairing of surfaces to logical steps is never pinned.", + "definition": { + "scope": "state", + "reads": [ + "state", + "world" + ] + }, + "evaluation_a": { + "state_at_step": 7, + "world_snapshot_at_step": 7, + "result": "held" + }, + "evaluation_b": { + "state_at_step": 7, + "world_snapshot_at_step": 9, + "result": "failed" + }, + "expected": "Same predicate, same state, DIFFERENT world snapshot \u2014 both are legal evaluations under the text as written. Reproducibility is a claim about a pairing the RFC does not pin." +} \ No newline at end of file diff --git a/probes/typed-domain-kernel-v0/fixtures/positive/domain-euclidean.json b/probes/typed-domain-kernel-v0/fixtures/positive/domain-euclidean.json new file mode 100644 index 00000000..a76b8406 --- /dev/null +++ b/probes/typed-domain-kernel-v0/fixtures/positive/domain-euclidean.json @@ -0,0 +1,43 @@ +{ + "note": "A domain that declares what it implements and implements what it declares.", + "domain": { + "id": "euclidean-r3", + "address": "sha256:58ff6665bdc00c2f9300d92cd2e291c84e5b38c37acc057642a7a1d406902345", + "version": "0.1.0", + "capabilities": [ + "metric", + "interpolable", + "geometric" + ], + "implements": [ + "distance", + "interpolate", + "move", + "transport", + "deltaDescriptor" + ], + "supportedOperations": [ + { + "name": "move", + "address": "sha256:cdc1542682cf4a6e0b3c4cf59110a29a20984abb169633c31d4567a0800f8fe4" + } + ], + "forbiddenOperations": [ + { + "name": "average", + "reason": "an average of three points is not a point of this domain under any declared law" + } + ], + "invariants": [ + "sha256:b7865d368c65a54de447825863f548af2228019e7439fbd973282ebdd29af8aa" + ], + "deltaDescriptor": { + "address": "sha256:0ef3720916ab40c795bde93fed740e87e1f742d5117a73312a53fd1ca2f0a04d", + "validate": "sha256:928f7af05edc83b8822f2b6489dea8e6cb2ed0e50f56b9c2fe3486b6d9d28f51", + "encoding": "hsp-jcs@v0/delta-r3" + }, + "laws": { + "metricAxioms": "sha256:631d131eccce74c3a09435170b1bd48772cb73efc6f6d7ab8c16467ba9453a15" + } + } +} \ No newline at end of file diff --git a/probes/typed-domain-kernel-v0/ts/kernel_test.ts b/probes/typed-domain-kernel-v0/ts/kernel_test.ts new file mode 100644 index 00000000..71ace2c6 --- /dev/null +++ b/probes/typed-domain-kernel-v0/ts/kernel_test.ts @@ -0,0 +1,353 @@ +// The typed-domain kernel's own controls. Positive fixtures prove the +// validators admit something; countermodels prove they refuse, and refuse for +// the stated reason. A validator that only ever passes is indistinguishable +// from one that checks nothing. + +import { assert, assertEquals } from "@std/assert"; +import { + CAPABILITIES, + type DomainDeclaration, + DOMAIN_REFUSALS, + isContentAddress, + NOT_ASSESSED_REASONS, + validateDomain, +} from "./layer1_domain.ts"; +import { + admitEvaluation, + CONTEXT_SURFACES, + COST_CLASSES, + type InvariantDefinition, + type InvariantEvaluation, + SCOPES, + validateInvariantDefinition, +} from "./layer2_invariant.ts"; +import { + BOUNDARY_KINDS, + type BoundaryPolicy, + decideComposition, + decideLaw, + LAW_STATUS_KINDS, + type LawClaim, + statedBelow, + validateVersionDag, +} from "./layer3_law.ts"; + +const HERE = new URL(".", import.meta.url); +const load = async (p: string) => + JSON.parse(await Deno.readTextFile(new URL(`../fixtures/${p}`, HERE))); + +// --------------------------------------------------------------------------- +// Layer 1 +// --------------------------------------------------------------------------- + +Deno.test("layer1 - the positive fixture is admitted", async () => { + const { domain } = await load("positive/domain-euclidean.json"); + const v = validateDomain(domain as DomainDeclaration); + assert(v.ok, v.ok ? "" : `${v.code}: ${v.reason}`); +}); + +Deno.test("layer1 - capability mismatch is refused in BOTH directions", async () => { + const { domain } = await load("positive/domain-euclidean.json"); + const base = domain as DomainDeclaration; + + // declared, not implemented + const missing = { + ...base, + implements: base.implements.filter((m) => m !== "transport"), + }; + const a = validateDomain(missing); + assertEquals(a.ok, false); + if (!a.ok) assertEquals(a.code, "capability-declared-not-implemented"); + + // implemented, not declared — the direction a permissive registry skips + const extra = { ...base, implements: [...base.implements, "compose"] }; + const b = validateDomain(extra); + assertEquals(b.ok, false); + if (!b.ok) assertEquals(b.code, "capability-implemented-not-declared"); +}); + +Deno.test("layer1 - move() without a typed delta space is refused", async () => { + const { domain } = await load("positive/domain-euclidean.json"); + const d = { ...(domain as DomainDeclaration) }; + delete (d as { deltaDescriptor?: unknown }).deltaDescriptor; + const v = validateDomain(d); + assertEquals(v.ok, false); + if (!v.ok) assertEquals(v.code, "geometric-without-delta-descriptor"); +}); + +Deno.test("layer1 - distance() without metricAxioms is refused", async () => { + const { domain } = await load("positive/domain-euclidean.json"); + const d = { ...(domain as DomainDeclaration), laws: {} }; + const v = validateDomain(d); + assertEquals(v.ok, false); + if (!v.ok) assertEquals(v.code, "metric-without-axioms"); +}); + +Deno.test("layer1 - a short handle is not a reference", async () => { + const { domain } = await load("positive/domain-euclidean.json"); + const d = { ...(domain as DomainDeclaration), address: "sha256:deadbeef" }; + const v = validateDomain(d); + assertEquals(v.ok, false); + if (!v.ok) assertEquals(v.code, "non-content-addressed-reference"); + assert(!isContentAddress("sha256:deadbeef")); +}); + +// --------------------------------------------------------------------------- +// Layer 2 +// --------------------------------------------------------------------------- + +const inv = (over: Partial = {}): InvariantDefinition => ({ + id: "inv-1", + address: `sha256:${"a".repeat(64)}`, + scope: "state", + predicate: `sha256:${"b".repeat(64)}`, + costClass: "constant", + falsifier: [`sha256:${"c".repeat(64)}`], + reads: ["state"], + ...over, +}); + +const evaluation = ( + over: Partial = {}, +): InvariantEvaluation => ({ + predicate: `sha256:${"b".repeat(64)}`, + state: `sha256:${"d".repeat(64)}`, + worldSnapshot: "", + authoritySnapshot: "", + evaluatedAtLogicalStep: "", + result: { verdict: "held" }, + ...over, +}); + +Deno.test("layer2 - an invariant with no falsifier is refused", () => { + const v = validateInvariantDefinition(inv({ falsifier: [] })); + assertEquals(v.ok, false); + if (!v.ok) assertEquals(v.code, "no-falsifier"); +}); + +Deno.test("layer2 - partially-held without a distortion measure is refused", () => { + const v = validateInvariantDefinition(inv(), { canBePartiallyHeld: true }); + assertEquals(v.ok, false); + if (!v.ok) assertEquals(v.code, "partial-without-distortion-measure"); +}); + +Deno.test("layer2 - transition and trace scope cannot be checked from one state", () => { + const t = admitEvaluation( + inv({ scope: "transition", reads: ["state", "transition"] }), + evaluation(), + ); + assertEquals("ok" in t && t.ok, false); + if ("code" in t) assertEquals(t.code, "missing-predecessor-for-transition"); + + const r = admitEvaluation( + inv({ scope: "trace", reads: ["state", "trace"] }), + evaluation(), + ); + if ("code" in r) assertEquals(r.code, "missing-trace-for-trace-scope"); +}); + +Deno.test("layer2 - an undeclared surface supplied to the evaluation is refused", () => { + // The direction a permissive check skips: the predicate declared it reads + // only `state`, and the evaluation hands it a world snapshot anyway. + const v = admitEvaluation( + inv({ reads: ["state"] }), + evaluation({ worldSnapshot: `sha256:${"e".repeat(64)}` }), + ); + assertEquals("ok" in v && v.ok, false); + if ("code" in v) assertEquals(v.code, "undeclared-surface-read"); +}); + +Deno.test("layer2 - unbounded never gates a fast path", () => { + const v = admitEvaluation(inv({ costClass: "unbounded" }), evaluation(), { + fastPath: true, + }); + if ("code" in v) assertEquals(v.code, "unbounded-gates-fast-path"); +}); + +Deno.test("layer2 - over budget and stale are NOT-ASSESSED, never held", () => { + // The three-valued outcome the RFC requires and never types. Collapsing it to + // a boolean is how a boundary comes to believe an invariant held when nobody + // checked it. + const over = admitEvaluation(inv({ costClass: "superlinear" }), evaluation(), { + budget: "linear", + }); + assert("notAssessed" in over && over.notAssessed === "cost-class-exceeds-budget"); + + const stale = admitEvaluation(inv(), evaluation(), { + freshness: { maxLogicalStepsBehind: 1 }, + snapshotLogicalStepsBehind: 9, + }); + assert("notAssessed" in stale && stale.notAssessed === "snapshot-stale"); +}); + +// --------------------------------------------------------------------------- +// Layer 3 — the seam +// --------------------------------------------------------------------------- + +const claim = (over: Partial = {}): LawClaim => ({ + status: { kind: "asserted", author: "claude" }, + scope: "total", + ...over, +}); + +const policy = (over: Partial = {}): BoundaryPolicy => ({ + boundary: "local", + accepts: ["proved", "tested", "asserted"], + ...over, +}); + +Deno.test("layer3 - falsified authorizes nothing, even if a policy accepts it", () => { + const v = decideLaw( + claim({ status: { kind: "falsified", counterexample: `sha256:${"f".repeat(64)}` } }), + // A policy that tries to opt in. The floor is above policy. + policy({ accepts: [...LAW_STATUS_KINDS] }), + ); + assertEquals(v.admitted, false); + if (!v.admitted) assertEquals(v.code, "falsified"); +}); + +Deno.test("layer3 - asserted never crosses a translation or irreversible boundary", () => { + for (const b of ["translation", "irreversible"] as const) { + const v = decideLaw(claim(), policy({ boundary: b, accepts: ["asserted"] })); + assertEquals(v.admitted, false, `${b} admitted an asserted law`); + if (!v.admitted) assertEquals(v.code, "asserted-across-boundary"); + } + // ...and does cross a local one, if the policy says so. Otherwise the control + // above would be satisfied by refusing everything. + assert(decideLaw(claim(), policy({ accepts: ["asserted"] })).admitted); +}); + +Deno.test("layer3 - an absent law is no claim, not a weak claim", () => { + const v = decideLaw(undefined, policy()); + assertEquals(v.admitted, false); + if (!v.admitted) assertEquals(v.code, "law-absent"); +}); + +Deno.test("layer3 - a tested law without a generation domain is asserted with extra steps", () => { + const v = decideLaw( + claim({ + status: { + kind: "tested", + generator: `sha256:${"1".repeat(64)}`, + domain: "", + cases: 1000, + seed: "s", + ref: `sha256:${"2".repeat(64)}`, + }, + }), + policy({ accepts: ["tested"] }), + ); + assertEquals(v.admitted, false); + if (!v.admitted) assertEquals(v.code, "generation-domain-unstated"); +}); + +Deno.test("layer3 - THE SEAM: proved and tested are not ordered by the RFC", async () => { + // statedBelow returns null for "the text does not order these", which is a + // different answer from false and is the one a policy must act on. + assertEquals(statedBelow("falsified", "asserted"), true); + assertEquals(statedBelow("asserted", "proved"), true); + assertEquals(statedBelow("asserted", "tested"), true); + assertEquals(statedBelow("proved", "tested"), null); + assertEquals(statedBelow("tested", "proved"), null); + + // The countermodel that makes the gap load-bearing rather than cosmetic. + const cm = await load("countermodels/proved-narrower-than-tested.json"); + const provedNarrow = cm.proved_but_narrow as LawClaim; + const testedWide = cm.tested_but_wider as LawClaim; + assertEquals(provedNarrow.scope, "partial"); + assertEquals(testedWide.scope, "total"); + // Both are admissible at a boundary that accepts both kinds; neither is "the + // minimum", and a threshold policy cannot express the difference. + const p = policy({ boundary: "composition", accepts: ["proved", "tested"] }); + assert(decideLaw(provedNarrow, p).admitted); + assert(decideLaw(testedWide, p).admitted); +}); + +Deno.test("layer3 - composition refuses mismatched scope", () => { + const p = policy({ accepts: ["proved"] }); + const proved = (scope: "total" | "partial") => + claim({ + status: { + kind: "proved", + proof: `sha256:${"3".repeat(64)}`, + checker: `sha256:${"4".repeat(64)}`, + }, + scope, + }); + assert(decideComposition(proved("total"), proved("total"), p).admitted); + assertEquals( + decideComposition(proved("total"), proved("partial"), p).admitted, + false, + ); +}); + +Deno.test("layer3 - version DAG: the one conflict the RFC names", async () => { + const cm = await load("countermodels/patch-across-law-weakening.json"); + const v = validateVersionDag(cm.releases, new Set(cm.weakened_laws)); + assertEquals(v.ok, false); + if (!v.ok) assertEquals(v.code, "patch-across-law-weakening"); + + // Without the weakening, the same DAG is fine — so the control discriminates. + assert(validateVersionDag(cm.releases, new Set()).ok); +}); + +Deno.test("layer3 - version DAG: cycles and orphans are refused", () => { + const a = `sha256:${"5".repeat(64)}`, b = `sha256:${"6".repeat(64)}`; + const cyc = validateVersionDag([ + { address: a, predecessor: b, label: "1.0.0" }, + { address: b, predecessor: a, label: "1.0.1" }, + ]); + assertEquals(cyc.ok, false); + if (!cyc.ok) assertEquals(cyc.code, "multiple-roots"); + + const orphan = validateVersionDag([ + { address: a, predecessor: null, label: "1.0.0" }, + { address: b, predecessor: `sha256:${"9".repeat(64)}`, label: "1.0.1" }, + ]); + assertEquals(orphan.ok, false); + if (!orphan.ok) assertEquals(orphan.code, "predecessor-unknown"); +}); + +// --------------------------------------------------------------------------- +// Closed sets — every enumeration this kernel exports is closed on purpose. +// --------------------------------------------------------------------------- + +Deno.test("kernel - the exported member sets are exactly what the README documents", () => { + assertEquals([...CAPABILITIES].sort(), [ + "comparable", + "composable", + "geometric", + "interpolable", + "metric", + "ordered", + ]); + assertEquals([...LAW_STATUS_KINDS].sort(), [ + "asserted", + "falsified", + "proved", + "tested", + ]); + assertEquals([...SCOPES], ["state", "transition", "trace"]); + assertEquals([...COST_CLASSES], [ + "constant", + "linear", + "superlinear", + "unbounded", + ]); + assertEquals([...CONTEXT_SURFACES].sort(), [ + "authority", + "logical-step", + "state", + "trace", + "transition", + "world", + ]); + assertEquals([...BOUNDARY_KINDS].sort(), [ + "composition", + "irreversible", + "local", + "translation", + ]); + assert(DOMAIN_REFUSALS.length >= 9); + assert(NOT_ASSESSED_REASONS.length >= 5); +}); diff --git a/probes/typed-domain-kernel-v0/ts/layer1_domain.ts b/probes/typed-domain-kernel-v0/ts/layer1_domain.ts new file mode 100644 index 00000000..81c8aea4 --- /dev/null +++ b/probes/typed-domain-kernel-v0/ts/layer1_domain.ts @@ -0,0 +1,264 @@ +// Layer 1 — StateDomain, capability interfaces, typed delta. B1 / B3. +// +// Interfaces and validators only. No production domain, no translator, no +// runtime integration: this package exists so the boundaries can be reviewed +// before anything is built on them. +// +// Reuses what already exists rather than reinventing it: `ScopeKind`/`ScopeRef` +// come from probes/hsp-fast-path-debt-scope-v0, which already types RFC-0003 +// references and already carries the full-digest convention §19.10 requires +// ("short handles MUST NOT be load-bearing"). + +export type ContentAddress = string; // `sha256:` + 64 lowercase hex +export type DomainId = string; +export type InvariantId = string; +export type EvidenceRef = ContentAddress; +export type FixtureRef = ContentAddress; +export type PredicateRef = ContentAddress; +export type MeasureRef = ContentAddress; + +export const FULL_DIGEST = /^sha256:[0-9a-f]{64}$/; + +/** §19.10: short handles are not load-bearing. Every reference in this kernel + * is a full digest, and this is the one place that is enforced. */ +export function isContentAddress(v: unknown): v is ContentAddress { + return typeof v === "string" && FULL_DIGEST.test(v); +} + +// --------------------------------------------------------------------------- +// B3 — capabilities are a CLOSED set, declared and implemented together. +// --------------------------------------------------------------------------- + +export const CAPABILITIES = [ + "comparable", + "ordered", + "metric", + "interpolable", + "composable", + "geometric", +] as const; +export type Capability = (typeof CAPABILITIES)[number]; + +/** §6.3.1 requires the registry to reject BOTH directions: a declared + * capability that is absent, and an implemented one that was not declared. + * The second is the one that is easy to skip — an undeclared capability is a + * surface consumers cannot reason about, and it is still there. */ +export const CAPABILITY_METHODS: Record = { + comparable: ["compare"], + ordered: ["order"], + metric: ["distance"], + interpolable: ["interpolate"], + composable: ["compose"], + geometric: ["move", "transport", "deltaDescriptor"], +}; + +/** §6 :127-131 requires a domain exposing `move` to declare a DeltaDescriptor + * with its own content address, "otherwise `move` is an untyped hole in an + * otherwise typed contract". + * + * THE RFC NEVER GIVES ITS SHAPE. `DeltaDescriptor` appears at :111, :128 and in + * the revision history, and nowhere is defined. This is the minimum that makes + * the stated obligation checkable: the delta space needs the same canonical + * encoding and validation obligations as the point space, which means an + * address, a validator, and its own laws — a delta space with no laws cannot + * support any claim about composing moves. + * + * Proposed, not quoted. Marked as such in the README's ambiguity table. */ +export type DeltaDescriptor = { + address: ContentAddress; + /** The predicate a candidate delta must satisfy. Content-addressed for the + * same reason invariant predicates are: a validator nobody can name is a + * validator nobody can replay. */ + validate: PredicateRef; + /** Canonical encoding identifier for the delta space. Separate from the point + * space's: §5.1.1 rule 6 puts the encoding identifier inside the digest, and + * a delta that borrowed the point space's identifier would claim an encoding + * it does not use. */ + encoding: string; + /** Laws of delta composition, if the domain composes deltas at all. + * DELIBERATELY OPTIONAL and deliberately not defaulted to associative: + * typedness does not confer associativity, and assuming it is exactly the + * move §6.2 exists to prevent. Absent means "no claim", not "no law". */ + composition?: ContentAddress; +}; + +export type OperationDescriptor = { + name: string; + address: ContentAddress; +}; + +export type ForbiddenOperation = { + name: string; + /** §5 :232-234 — an operation without coherent meaning MUST be absent or + * explicitly forbidden. A reason is required so "forbidden" is a statement + * rather than a shrug. */ + reason: string; +}; + +/** §6.1.2 rule 5 requires an outcome distinct from held and from failed: + * a stale snapshot is `not assessed`. `ValidationReport` is never typed in the + * RFC, so this is the minimum shape that can express what rule 5 demands. */ +export type ValidationReport = + | { verdict: "held" } + | { verdict: "failed"; detail: string } + | { verdict: "not-assessed"; reason: NotAssessedReason }; + +export const NOT_ASSESSED_REASONS = [ + "snapshot-stale", + "snapshot-missing", + "scope-not-available", + "cost-class-exceeds-budget", + "undeclared-surface-read", +] as const; +export type NotAssessedReason = (typeof NOT_ASSESSED_REASONS)[number]; + +/** The declared surface of a state domain — everything §6.1 requires it to + * provide, as data rather than as methods, so a registry can check a + * declaration without instantiating anything. */ +export type DomainDeclaration = { + id: DomainId; + address: ContentAddress; + /** §6.2.1 rule 2: a projection of the version DAG, never an assertion. */ + version: string; + capabilities: readonly Capability[]; + /** Method names the implementation actually exposes. §6.3.1 compares this + * against `capabilities` in BOTH directions. */ + implements: readonly string[]; + supportedOperations: readonly OperationDescriptor[]; + forbiddenOperations: readonly ForbiddenOperation[]; + invariants: readonly ContentAddress[]; + /** Required if and only if `geometric` is declared (§6 :127-131). */ + deltaDescriptor?: DeltaDescriptor; + /** §6.2 rule 4: any domain exposing `distance` MUST declare metric axioms. + * Carried as addresses here; the claims themselves live in layer 3. */ + laws: Record; +}; + +export const DOMAIN_REFUSALS = [ + "capability-declared-not-implemented", + "capability-implemented-not-declared", + "geometric-without-delta-descriptor", + "delta-descriptor-without-geometric", + "metric-without-axioms", + "operation-both-supported-and-forbidden", + "forbidden-without-reason", + "non-content-addressed-reference", + "unknown-capability", +] as const; +export type DomainRefusal = (typeof DOMAIN_REFUSALS)[number]; + +export type DomainVerdict = + | { ok: true } + | { ok: false; code: DomainRefusal; reason: string }; + +/** Registry admission, §6.3.1. Fail closed in both directions. */ +export function validateDomain(d: DomainDeclaration): DomainVerdict { + const no = (code: DomainRefusal, reason: string): DomainVerdict => ({ + ok: false, + code, + reason, + }); + + for (const c of d.capabilities) { + if (!(CAPABILITIES as readonly string[]).includes(c)) { + return no("unknown-capability", `${c} is not a capability of this kernel`); + } + } + + const implemented = new Set(d.implements); + const declaredMethods = new Set(); + for (const c of d.capabilities) { + for (const m of CAPABILITY_METHODS[c]) { + declaredMethods.add(m); + if (!implemented.has(m)) { + return no( + "capability-declared-not-implemented", + `${c} is declared but ${m}() is absent — a promise that fails at the ` + + "worst moment (§6.3.1)", + ); + } + } + } + for (const m of implemented) { + if (!declaredMethods.has(m)) { + return no( + "capability-implemented-not-declared", + `${m}() is implemented but no declared capability covers it — an ` + + "undeclared surface consumers cannot reason about (§6.3.1)", + ); + } + } + + const geometric = d.capabilities.includes("geometric"); + if (geometric && !d.deltaDescriptor) { + return no( + "geometric-without-delta-descriptor", + "a domain exposing move() must declare a typed delta space, or move() is " + + "an untyped hole in a typed contract (§6 :127-131)", + ); + } + if (!geometric && d.deltaDescriptor) { + return no( + "delta-descriptor-without-geometric", + "a delta descriptor without the geometric capability describes a space " + + "nothing moves through", + ); + } + + if (d.capabilities.includes("metric") && !d.laws["metricAxioms"]) { + return no( + "metric-without-axioms", + "a domain exposing distance() must declare metricAxioms; a similarity " + + "score that violates the triangle inequality is not a metric (§6.2 rule 4)", + ); + } + + const supported = new Set(d.supportedOperations.map((o) => o.name)); + for (const f of d.forbiddenOperations) { + if (supported.has(f.name)) { + return no( + "operation-both-supported-and-forbidden", + `${f.name} is both supported and forbidden`, + ); + } + if (!f.reason.trim()) { + return no( + "forbidden-without-reason", + `${f.name} is forbidden without a reason; "forbidden" must be a ` + + "statement rather than a shrug (§5 :232-234)", + ); + } + } + + const refs: [string, string][] = [ + ["address", d.address], + ...d.supportedOperations.map((o): [string, string] => [ + `operation ${o.name}`, + o.address, + ]), + ...d.invariants.map((r, i): [string, string] => [`invariant[${i}]`, r]), + ...Object.entries(d.laws).map(([k, v]): [string, string] => [`law ${k}`, v]), + ...(d.deltaDescriptor + ? [ + ["deltaDescriptor.address", d.deltaDescriptor.address] as [ + string, + string, + ], + ["deltaDescriptor.validate", d.deltaDescriptor.validate] as [ + string, + string, + ], + ] + : []), + ]; + for (const [where, ref] of refs) { + if (!isContentAddress(ref)) { + return no( + "non-content-addressed-reference", + `${where} is ${JSON.stringify(ref)}, not a full sha256: digest (§19.10)`, + ); + } + } + + return { ok: true }; +} diff --git a/probes/typed-domain-kernel-v0/ts/layer2_invariant.ts b/probes/typed-domain-kernel-v0/ts/layer2_invariant.ts new file mode 100644 index 00000000..393f6b25 --- /dev/null +++ b/probes/typed-domain-kernel-v0/ts/layer2_invariant.ts @@ -0,0 +1,295 @@ +// Layer 2 — invariants: scope, cost class, and content-addressed context. +// B4 / B8. +// +// This layer closes a seam the RFC leaves open between its own two sections: +// §6.1.2 rule 1 says "An `InvariantDefinition` MUST declare which context +// surfaces its predicate reads", and the `InvariantDefinition` type at §6.1.1 +// has no field for them. The obligation exists and its carrier does not. The +// field is added here and marked as PROPOSED, not quoted. + +import { + type ContentAddress, + type InvariantId, + isContentAddress, + type MeasureRef, + type NotAssessedReason, + type PredicateRef, + type ValidationReport, +} from "./layer1_domain.ts"; + +export type FixtureRef = ContentAddress; +export type StateRef = ContentAddress; +export type TransitionRef = ContentAddress; +export type TraceRef = ContentAddress; +export type SnapshotRef = ContentAddress; +export type AuthorityRef = ContentAddress; +export type SequenceRef = string; + +export const SCOPES = ["state", "transition", "trace"] as const; +export type Scope = (typeof SCOPES)[number]; + +export const COST_CLASSES = [ + "constant", + "linear", + "superlinear", + "unbounded", +] as const; +export type CostClass = (typeof COST_CLASSES)[number]; + +/** The context surfaces a predicate may read. CLOSED set: §6.1.2 rule 1 makes + * an undeclared read non-conforming, and "checkable by evaluating it against a + * snapshot that omits the undeclared surface" is only checkable if the surfaces + * are enumerable. + * + * The RFC names `worldSnapshot`, `authoritySnapshot` and + * `evaluatedAtLogicalStep` in `InvariantEvaluation`; this list is those three + * plus the scope-carried inputs, so that a `state`-scope predicate reading a + * predecessor is caught as an undeclared read rather than as a scope error. */ +export const CONTEXT_SURFACES = [ + "state", + "transition", + "trace", + "world", + "authority", + "logical-step", +] as const; +export type ContextSurface = (typeof CONTEXT_SURFACES)[number]; + +/** §6.1.1's type, plus the `reads` field §6.1.2 rule 1 requires and §6.1.1 does + * not carry. PROPOSED — see the README ambiguity table. */ +export type InvariantDefinition = { + id: InvariantId; + address: ContentAddress; + scope: Scope; + predicate: PredicateRef; + costClass: CostClass; + /** Required if the invariant can be partially held (§6.1.1 rule 3), because + * §7.1.1 composes distortion by this measure's own rule. */ + distortionMeasure?: MeasureRef; + falsifier: readonly FixtureRef[]; + /** PROPOSED (§6.1.2 rule 1 obligation, §6.1.1 carrier absent). */ + reads: readonly ContextSurface[]; +}; + +export type InvariantEvaluation = { + predicate: PredicateRef; + state: StateRef; + transition?: TransitionRef; + trace?: TraceRef; + worldSnapshot: SnapshotRef; + authoritySnapshot: AuthorityRef; + evaluatedAtLogicalStep: SequenceRef; + result: ValidationReport; +}; + +/** A boundary's freshness requirement. §6.1.2 rule 5 requires boundaries to + * declare one and gives it no type, unit or comparison. Expressed here in + * LOGICAL STEPS rather than time, because rule 4 forbids a predicate from + * reading the clock and a freshness rule denominated in wall-clock would + * reintroduce the thing rule 4 removes. PROPOSED. */ +export type Freshness = { maxLogicalStepsBehind: number }; + +export const INVARIANT_REFUSALS = [ + "scope-narrower-than-declared", + "missing-predecessor-for-transition", + "missing-trace-for-trace-scope", + "unbounded-gates-fast-path", + "cost-class-exceeds-budget", + "partial-without-distortion-measure", + "undeclared-surface-read", + "surface-declared-not-available", + "unknown-surface", + "non-content-addressed-reference", + "no-falsifier", +] as const; +export type InvariantRefusal = (typeof INVARIANT_REFUSALS)[number]; + +export type InvariantVerdict = + | { ok: true } + | { ok: false; code: InvariantRefusal; reason: string }; + +const no = (code: InvariantRefusal, reason: string): InvariantVerdict => ({ + ok: false, + code, + reason, +}); + +/** Static checks on a definition, before any evaluation. */ +export function validateInvariantDefinition( + d: InvariantDefinition, + opts: { canBePartiallyHeld?: boolean } = {}, +): InvariantVerdict { + for (const s of d.reads) { + if (!(CONTEXT_SURFACES as readonly string[]).includes(s)) { + return no("unknown-surface", `${s} is not a context surface`); + } + } + if (opts.canBePartiallyHeld && !d.distortionMeasure) { + return no( + "partial-without-distortion-measure", + "an invariant that can be partially held must supply a distortionMeasure, " + + "because §7.1.1 composes distortion by that measure's own rule (§6.1.1 rule 3)", + ); + } + if (!d.falsifier.length) { + return no( + "no-falsifier", + "an invariant with no falsifier fixture cannot be shown to fail, and a " + + "check that cannot fail is not a check", + ); + } + for ( + const [where, ref] of [ + ["address", d.address], + ["predicate", d.predicate], + ...(d.distortionMeasure + ? [["distortionMeasure", d.distortionMeasure] as [string, string]] + : []), + ...d.falsifier.map((f, i): [string, string] => [`falsifier[${i}]`, f]), + ] as [string, string][] + ) { + if (!isContentAddress(ref)) { + return no( + "non-content-addressed-reference", + `${where} is not a full sha256: digest (§19.10)`, + ); + } + } + return { ok: true }; +} + +/** Which surfaces an evaluation actually makes available. A surface that is + * declared but absent from the evaluation is refused BEFORE the predicate + * runs, which is what makes §6.1.2 rule 1 checkable "by evaluating it against a + * snapshot that omits the undeclared surface". */ +export function availableSurfaces(e: InvariantEvaluation): Set { + const s = new Set(["state"]); + if (e.transition) s.add("transition"); + if (e.trace) s.add("trace"); + if (e.worldSnapshot) s.add("world"); + if (e.authoritySnapshot) s.add("authority"); + if (e.evaluatedAtLogicalStep) s.add("logical-step"); + return s; +} + +/** Admit or refuse ONE evaluation at a boundary. + * + * Fail closed everywhere, and distinguish `not-assessed` from `failed`: §6.1.2 + * rule 5 requires a stale snapshot to be "treated as `not assessed` rather than + * as `held`", which is a three-valued outcome the RFC never types. Collapsing + * it to a boolean is how a boundary comes to believe an invariant held when + * nobody checked it. */ +export function admitEvaluation( + d: InvariantDefinition, + e: InvariantEvaluation, + boundary: { + budget?: CostClass; + fastPath?: boolean; + freshness?: Freshness; + snapshotLogicalStepsBehind?: number; + } = {}, +): InvariantVerdict | { ok: false; notAssessed: NotAssessedReason; reason: string } { + // Scope first: an invariant checked at a narrower scope than declared and + // reported as held is the failure §6.1.1 rule 1 names. + if (d.scope === "transition" && !e.transition) { + return no( + "missing-predecessor-for-transition", + "a transition-scope invariant requires the predecessor and must not be " + + "checked from a state in isolation (§6.1.1 :168-169)", + ); + } + if (d.scope === "trace" && !e.trace) { + return no( + "missing-trace-for-trace-scope", + "a trace-scope invariant cannot be established by inspecting the state " + + "that arrived at a boundary; a gate claiming to enforce it from one " + + "state is not enforcing it (§6.1.1 :170-171)", + ); + } + + // §6.1.1 rule 2: unbounded never gates a fast path, and never sits at a + // boundary with a bounded budget. + if (d.costClass === "unbounded" && boundary.fastPath) { + return no( + "unbounded-gates-fast-path", + "an unbounded invariant must not gate a fast-path decision (§6.1.1 rule 2)", + ); + } + if (boundary.budget) { + const rank = (c: CostClass) => COST_CLASSES.indexOf(c); + if (rank(d.costClass) > rank(boundary.budget)) { + return { + ok: false, + notAssessed: "cost-class-exceeds-budget", + reason: + `the invariant is ${d.costClass}; this boundary budgets ` + + `${boundary.budget}. Not assessed — reporting it as held would be a ` + + "claim nobody paid for", + }; + } + } + + // §6.1.2 rule 1, in the direction that catches an undeclared read: every + // surface the definition declares must be present, and any surface present + // beyond what was declared is available to a predicate that never said it + // would read it. The second half is the one a permissive check skips. + const available = availableSurfaces(e); + for (const s of d.reads) { + if (!available.has(s)) { + return no( + "surface-declared-not-available", + `the definition declares it reads ${s}, which this evaluation does not ` + + "supply", + ); + } + } + for (const s of available) { + if (s === "state") continue; // always required + if (!d.reads.includes(s)) { + return no( + "undeclared-surface-read", + `the evaluation supplies ${s}, which the definition did not declare it ` + + "reads; a predicate that reads an undeclared surface is " + + "non-conforming (§6.1.2 rule 1)", + ); + } + } + + // §6.1.2 rule 5: staleness is not-assessed, never held. + if ( + boundary.freshness && + boundary.snapshotLogicalStepsBehind !== undefined && + boundary.snapshotLogicalStepsBehind > boundary.freshness.maxLogicalStepsBehind + ) { + return { + ok: false, + notAssessed: "snapshot-stale", + reason: + `the snapshot is ${boundary.snapshotLogicalStepsBehind} logical steps ` + + `behind; this boundary requires at most ` + + `${boundary.freshness.maxLogicalStepsBehind}. An invariant that held ` + + "against a snapshot no longer current has not been shown to hold now", + }; + } + + return { ok: true }; +} + +/** The proof obligation this layer does not discharge. */ +export const PROOF_OBLIGATION_SCOPE_MONOTONICITY = ` +This kernel refuses an invariant checked at a scope NARROWER than declared +(§6.1.1 rule 1). It does not establish the converse — that checking at a WIDER +scope is always sound — and the RFC does not state it either. + +It is not obviously true. A trace-scope evaluation supplies a trace; a +state-scope predicate that declared it reads only \`state\` will not see it, so +the wider evaluation is sound for THAT predicate. But a predicate declaring +\`reads: ["state","world"]\` evaluated inside a trace context may observe a world +snapshot taken at a different logical step than the state it is judging, and +§6.1.2 rule 2 (reproducibility) is then a claim about a pairing nobody pinned. + +Obligation: state whether scope widening preserves evaluation reports, and if so +under what constraint on the logical step of each supplied surface. Until it is +stated, this kernel neither permits nor forbids widening — it validates what was +supplied against what was declared, and nothing more. +`.trim(); diff --git a/probes/typed-domain-kernel-v0/ts/layer3_law.ts b/probes/typed-domain-kernel-v0/ts/layer3_law.ts new file mode 100644 index 00000000..e4e7b716 --- /dev/null +++ b/probes/typed-domain-kernel-v0/ts/layer3_law.ts @@ -0,0 +1,379 @@ +// Layer 3 — law evidence, boundary policy, version DAG. B2 / B7 / B5. +// +// The crux of this package is here, and it is a normative ambiguity rather than +// a missing type: §6.2 rule 2 says "a policy MUST state the minimum status each +// boundary requires", and the RFC never defines an order on `LawStatus`. +// "Minimum" over an unordered set is not a requirement anyone can implement the +// same way twice. Part 03 repeats the phrase three times (§7.1 :397, :540, :678) +// and never repairs it. +// +// This is the same defect the Lean kernel already proved for suitability — +// `Suitability.lean`'s `no_meet` — where the document said "the lower of two +// levels" over an order that has no meet. That precedent is why this package +// does not simply invent a total order and move on: an invented order is a +// normative decision wearing an implementation's clothes. + +import type { ContentAddress, EvidenceRef, FixtureRef, PredicateRef } from "./layer1_domain.ts"; + +export type AgentId = string; +export type GeneratorRef = ContentAddress; +export type OperationRef = ContentAddress; +export type OrderRef = ContentAddress; + +/** §6.2, verbatim in shape. The four variants are a CLOSED set. */ +export type LawStatus = + | { kind: "proved"; proof: EvidenceRef; checker: ContentAddress } + | { + kind: "tested"; + generator: GeneratorRef; + domain: PredicateRef; // what the generator actually covers + cases: number; + seed: string; + ref: EvidenceRef; + } + | { kind: "asserted"; author: AgentId } + | { kind: "falsified"; counterexample: FixtureRef }; + +export const LAW_STATUS_KINDS = [ + "proved", + "tested", + "asserted", + "falsified", +] as const; +export type LawStatusKind = (typeof LAW_STATUS_KINDS)[number]; + +export type LawClaim = { + status: LawStatus; + scope: "total" | "partial"; + precondition?: PredicateRef; +}; + +// --------------------------------------------------------------------------- +// The order that does not exist, and the one this package proposes instead. +// --------------------------------------------------------------------------- + +/** The RFC's stated floor, and NOTHING else, expressed as a partial order. + * + * §6.2 rule 2 gives exactly two constraints and no more: + * + * * `falsified` authorizes nothing, anywhere; + * * `asserted` does not authorize composition across a translation or + * irreversible boundary. + * + * From those, `falsified` is below everything and `asserted` is below the two + * evidenced kinds AT SUCH BOUNDARIES. The text never relates `proved` and + * `tested` to one another, and this package does NOT invent that relation — + * see `PROVED_TESTED_INCOMPARABLE` and the countermodel that motivates it. + * + * Returns `null` for "the RFC does not order these", which is different from + * `false` and is the distinction a policy has to act on. */ +export function statedBelow(a: LawStatusKind, b: LawStatusKind): boolean | null { + if (a === b) return false; + if (a === "falsified") return true; // below everything + if (b === "falsified") return false; + if (a === "asserted" && (b === "proved" || b === "tested")) return true; + if (b === "asserted" && (a === "proved" || a === "tested")) return false; + return null; // proved vs tested: unordered in the text +} + +/** Why `proved` and `tested` are left incomparable rather than ranked. + * + * Ranking them looks obvious and is not sound. A `LawClaim` carries `scope` + * and an optional `precondition`, and a `tested` status carries the DOMAIN its + * generator covered. So: + * + * * a `proved` claim with `scope: "partial"` and a narrow `precondition` + * establishes the law only inside that precondition; + * * a `tested` claim whose generation domain strictly contains that + * precondition has been checked over inputs the proof says nothing about. + * + * Neither dominates. Calling `proved` uniformly stronger would let a boundary + * accept a proof about a region it does not operate in, over evidence about the + * region it does. `fixtures/countermodels/proved-narrower-than-tested.json` is + * that pair, executable. + * + * This is a normative gap, not an implementation choice, and it is reported as + * one rather than closed by fiat. */ +export const PROVED_TESTED_INCOMPARABLE = + "§6.2 states no relation between `proved` and `tested`; a LawClaim's scope, " + + "precondition, and (for `tested`) generation domain can make either the " + + "stronger evidence for a given boundary. See PROOF_OBLIGATION_LAWSTATUS_ORDER."; + +export type BoundaryKind = + | "local" + | "translation" + | "irreversible" + | "composition"; + +export const BOUNDARY_KINDS: readonly BoundaryKind[] = [ + "local", + "translation", + "irreversible", + "composition", +] as const; + +/** A boundary policy. §6.2 rule 2 requires the MINIMUM to be stated per + * boundary; since the text supplies no order, a policy here states an explicit + * ACCEPT SET rather than a threshold. A set is expressible without an order, + * and it makes the policy's actual reach readable instead of inferred. */ +export type BoundaryPolicy = { + boundary: BoundaryKind; + accepts: readonly LawStatusKind[]; + /** Required when `tested` is accepted: the generation domain a boundary will + * take. Without it, §6.2 rule 3's "a test whose generation domain is unstated + * is `asserted` with extra steps" is unenforceable on the CONSUMING side. */ + requiresGenerationDomain?: PredicateRef; +}; + +export type LawDecision = + | { admitted: true; status: LawStatusKind } + | { admitted: false; reason: string; code: LawRefusal }; + +export const LAW_REFUSALS = [ + "falsified", + "status-not-accepted", + "asserted-across-boundary", + "generation-domain-unstated", + "generation-domain-not-accepted", + "law-absent", + "policy-accepts-nothing", +] as const; +export type LawRefusal = (typeof LAW_REFUSALS)[number]; + +/** Decide one law at one boundary. Fail closed: every path that is not an + * explicit accept is a refusal with a code. */ +export function decideLaw( + claim: LawClaim | undefined, + policy: BoundaryPolicy, +): LawDecision { + const no = (code: LawRefusal, reason: string): LawDecision => ({ + admitted: false, + code, + reason, + }); + + if (!policy.accepts.length) { + return no( + "policy-accepts-nothing", + `the ${policy.boundary} policy accepts no status; a policy that admits ` + + "nothing is a configuration error, not a strict policy", + ); + } + if (!claim) { + return no( + "law-absent", + "the law is not declared; an absent law is not a weak law, it is no claim", + ); + } + + const kind = claim.status.kind; + + // §6.2 rule 2 floor, checked before the policy: `falsified` authorizes + // nothing, so a policy cannot opt into it. + if (kind === "falsified") { + return no( + "falsified", + "the law is falsified; it authorizes nothing and fails closed wherever " + + "it is relied on (§6.2 rule 2)", + ); + } + + // The other half of the floor, also above policy: `asserted` never crosses a + // translation or irreversible boundary, whatever a policy says. + if ( + kind === "asserted" && + (policy.boundary === "translation" || policy.boundary === "irreversible") + ) { + return no( + "asserted-across-boundary", + `an asserted law must not authorize composition across a ` + + `${policy.boundary} boundary (§6.2 rule 2)`, + ); + } + + if (!policy.accepts.includes(kind)) { + return no( + "status-not-accepted", + `the ${policy.boundary} policy accepts ${policy.accepts.join("|")}; this ` + + `law is ${kind}`, + ); + } + + if (kind === "tested") { + // §6.2 rule 3, enforced at the consumer. The producing side declaring a + // generator is not enough: a boundary must be able to say which generation + // domains it will take, or "tested" is a word. + if (!claim.status.generator || !claim.status.domain) { + return no( + "generation-domain-unstated", + "a tested law must record its generator and the domain it covers; " + + "without both it is asserted with extra steps (§6.2 rule 3)", + ); + } + if ( + policy.requiresGenerationDomain && + policy.requiresGenerationDomain !== claim.status.domain + ) { + return no( + "generation-domain-not-accepted", + `this boundary requires generation domain ` + + `${policy.requiresGenerationDomain}; the claim covers ` + + `${claim.status.domain}`, + ); + } + } + + return { admitted: true, status: kind }; +} + +/** §6.2 rule 5: a composition is refused when either side declares the law + * `falsified`, or when the two sides declare INCOMPATIBLE laws for the + * operation in use. + * + * "Incompatible" is not defined by the RFC either. This package takes the + * narrow reading it can defend — one side declaring a law the other declares + * falsified, or the two declaring different `scope` for the same law — and + * reports the wider reading as an open obligation rather than guessing. */ +export function decideComposition( + left: LawClaim | undefined, + right: LawClaim | undefined, + policy: BoundaryPolicy, +): LawDecision { + const l = decideLaw(left, policy); + if (!l.admitted) return l; + const r = decideLaw(right, policy); + if (!r.admitted) return r; + if (left!.scope !== right!.scope) { + return { + admitted: false, + code: "status-not-accepted", + reason: + `the two domains declare the same law at different scopes ` + + `(${left!.scope} vs ${right!.scope}); §6.2 rule 5 refuses a ` + + "composition over incompatible law declarations", + }; + } + // Both admitted and scopes agree. The composite's status is NOT computed: + // that would require the order §6.2 does not state. A caller that needs one + // must consult both, which is what returning the pair-checked decision means. + return { admitted: true, status: l.status }; +} + +// --------------------------------------------------------------------------- +// B5 — version is a projection of the DAG, never an assertion. +// --------------------------------------------------------------------------- + +export type Release = { + address: ContentAddress; + predecessor: ContentAddress | null; // null only for the root release + label: string; +}; + +export const VERSION_REFUSALS = [ + "label-is-not-a-projection", + "predecessor-unknown", + "cycle", + "multiple-roots", + "patch-across-law-weakening", +] as const; +export type VersionRefusal = (typeof VERSION_REFUSALS)[number]; + +/** §6.2.1 rule 3: a registry MUST reject a domain whose label conflicts with + * its position in the DAG. The RFC gives ONE example of a conflict — "a label + * claiming a patch increment across a change that weakened a law" — and never + * defines the projection function or the general notion of conflict. + * + * So this validator checks what the text actually determines: the DAG is + * well-formed (single root, no cycle, every predecessor known), and the one + * named conflict is refused when law-weakening is supplied by the caller. + * Everything else about the projection is an open obligation, stated as one. */ +export function validateVersionDag( + releases: readonly Release[], + weakenedLaws: ReadonlySet = new Set(), +): { ok: true } | { ok: false; code: VersionRefusal; reason: string } { + const byAddress = new Map(releases.map((r) => [r.address, r])); + const roots = releases.filter((r) => r.predecessor === null); + if (roots.length !== 1) { + return { + ok: false, + code: "multiple-roots", + reason: `a version DAG has exactly one root; found ${roots.length}`, + }; + } + for (const r of releases) { + if (r.predecessor !== null && !byAddress.has(r.predecessor)) { + return { + ok: false, + code: "predecessor-unknown", + reason: `${r.address} names predecessor ${r.predecessor}, which is absent`, + }; + } + } + // Walk to the root from every node; a cycle is a walk that revisits. + for (const start of releases) { + const seen = new Set(); + let cur: Release | undefined = start; + while (cur) { + if (seen.has(cur.address)) { + return { + ok: false, + code: "cycle", + reason: `the version DAG cycles at ${cur.address}`, + }; + } + seen.add(cur.address); + cur = cur.predecessor === null + ? undefined + : byAddress.get(cur.predecessor); + } + } + // The one conflict §6.2.1 rule 3 names by example. + for (const r of releases) { + if (r.predecessor === null) continue; + if (!weakenedLaws.has(r.address)) continue; + const prev = byAddress.get(r.predecessor)!; + if (isPatchIncrement(prev.label, r.label)) { + return { + ok: false, + code: "patch-across-law-weakening", + reason: + `${r.address} claims a patch increment (${prev.label} → ${r.label}) ` + + "across a change that weakened a law (§6.2.1 rule 3)", + }; + } + } + return { ok: true }; +} + +/** Semver-shaped patch detection, used ONLY for the conflict §6.2.1 names. + * This is not a claim that labels are semver — the RFC does not say so, and + * nothing here verifies against a label (§6.2.1: "Nothing verifies against + * it"). It is a heuristic in service of one stated refusal. */ +function isPatchIncrement(before: string, after: string): boolean { + const p = /^(\d+)\.(\d+)\.(\d+)$/; + const a = p.exec(before), b = p.exec(after); + if (!a || !b) return false; + return a[1] === b[1] && a[2] === b[2] && Number(b[3]) === Number(a[3]) + 1; +} + +/** The proof obligation this package refuses to discharge by fiat. */ +export const PROOF_OBLIGATION_LAWSTATUS_ORDER = ` +§6.2 rule 2 requires a policy to state "the minimum status each boundary +requires". §6.2 defines no order on LawStatus, and a minimum over an unordered +set is not a requirement two implementers can satisfy identically. + +The two constraints the text DOES give — falsified below everything, asserted +below the evidenced kinds at translation and irreversible boundaries — leave +proved and tested unrelated, and LawClaim.scope, LawClaim.precondition and +tested.domain make that gap load-bearing rather than cosmetic. + +Obligation: either (a) state a partial order on LawStatus and prove that every +pair a policy must compare has a greatest lower bound in it, or (b) replace +"minimum status" in §6.2 rule 2 and Part 03 §7.1 with an accept-set formulation, +which needs no order. This package implements (b) as BoundaryPolicy.accepts and +does not amend the RFC. + +Prior art: proofs/rfc-0003/HSP/Suitability.lean proved the same shape for +SuitabilityLevel (no_meet, finding C3) — a document saying "the lower of two" +over an order that has no meet. +`.trim(); diff --git a/src/x7B88_evidence_report.myc.md b/src/x7B88_evidence_report.myc.md index f45de4ee..927b84ff 100644 --- a/src/x7B88_evidence_report.myc.md +++ b/src/x7B88_evidence_report.myc.md @@ -22,7 +22,7 @@ invariants._ | Core Claim | Claim Status | Contract | Contract Status | Command | Source | Live Evidence | | :---------------------------------------------------- | :------------------------ | :--------------------------------------------------------------------------------- | :------------------------ | :-------------------------------------------------------------------------------------- | :------------- | :--------------------------------------------------------------------------------- | | Substrate Health Check | **IMPLEMENTED** | [SUBSTRATE_HEALTH.v0.1.md](contracts/SUBSTRATE_HEALTH.v0.1.md) | **IMPLEMENTED** | `./t status` | `live` | environment-dependent (run the command for live evidence) | -| External Surfaces Tracking | **IMPLEMENTED** | [IN_LEDGER_SRC_PROJECTION.v0.2.md](contracts/IN_LEDGER_SRC_PROJECTION.v0.2.md) | **PARTIALLY_IMPLEMENTED** | `./t external-surfaces` | `live` | tracked: 964 items (56 ABI, 17 docs, 55 probes, 0 chords) | +| External Surfaces Tracking | **IMPLEMENTED** | [IN_LEDGER_SRC_PROJECTION.v0.2.md](contracts/IN_LEDGER_SRC_PROJECTION.v0.2.md) | **PARTIALLY_IMPLEMENTED** | `./t external-surfaces` | `live` | tracked: 965 items (56 ABI, 17 docs, 56 probes, 0 chords) | | Chord Decision Ledger | **IMPLEMENTED** | [PROCESS_OBJECTS.v0.1.md](contracts/PROCESS_OBJECTS.v0.1.md) | **PARTIALLY_IMPLEMENTED** | `./t decisions` | `live` | 836 chords parsed: 93 proposals, 87 decisions, 384 receipts, 24 critiques | | Contract Ref-Graph Audit | **PROTOTYPE** | [PROCESS_OBJECTS.v0.1.md](contracts/PROCESS_OBJECTS.v0.1.md) | **PARTIALLY_IMPLEMENTED** | `./t contract-audit` | `live` | 43 contracts classified; 0 need review; 0 safe-to-compost | | Ecosystem Submodule Federation | **PARTIALLY_IMPLEMENTED** | [SUBSTRATE_SELF_ABI.v0.1.md](contracts/SUBSTRATE_SELF_ABI.v0.1.md) | **PARTIALLY_IMPLEMENTED** | `git submodule status` | `live` | environment-dependent (run the command for live evidence) | diff --git a/src/x8F88_external_surfaces.myc.md b/src/x8F88_external_surfaces.myc.md index 1dcc7590..630f0892 100644 --- a/src/x8F88_external_surfaces.myc.md +++ b/src/x8F88_external_surfaces.myc.md @@ -13,10 +13,10 @@ documents, and local caches outside the core Deno flat-src code base._ | compatibility abi | 56 | | compost | 0 | | dynamic topology | 836 | -| experimental | 55 | +| experimental | 56 | | live chord | 0 | | local cache | 0 | -| **Total** | **964** | +| **Total** | **965** | ## Runtime Cache Diagnostics @@ -145,6 +145,7 @@ Run `./t external-surfaces --json` for live cache counts, or | experimental | [probes/spore-runtime-adapter-v0/SPEC.md](../probes/spore-runtime-adapter-v0/SPEC.md) | experimental | | keep | active experiment | | experimental | [probes/substrate-court-v0/SPEC.md](../probes/substrate-court-v0/SPEC.md) | experimental | | keep | active experiment | | experimental | [probes/swarm-action-density-v0/SPEC.md](../probes/swarm-action-density-v0/SPEC.md) | experimental | | keep | active experiment | +| experimental | [probes/typed-domain-kernel-v0/README.md](../probes/typed-domain-kernel-v0/README.md) | experimental | | keep | active experiment | | experimental | [probes/voice-memory-v0/README.md](../probes/voice-memory-v0/README.md) | experimental | | keep | active experiment | | experimental | [probes/voice-tick-v0/SPEC.md](../probes/voice-tick-v0/SPEC.md) | experimental | | keep | active experiment | | experimental | [probes/voices-routing-falsifier-v0/SPEC.md](../probes/voices-routing-falsifier-v0/SPEC.md) | experimental | | keep | active experiment |