From 0ed65d7494cac34a11742e5512eb7d26a1cdbddf Mon Sep 17 00:00:00 2001 From: s0fractal Date: Thu, 27 Aug 2026 01:47:34 +0300 Subject: [PATCH] feat(typed-domain-kernel): Tranche B interface/evidence package, B1-B5/B7/B8 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Interfaces and evidence, not implementations. No production domain, no translator, no runtime integration — the point is that the boundaries get reviewed before anything rests on them. Three layers, one-way dependencies: domain/capabilities/delta (B1 B3); invariants/context (B4 B8); laws/policy/version DAG (B2 B7 B5). B6 is out of scope and remains the RFC's own open question. **The output that matters is five proof obligations** — places where the RFC states a requirement whose terms it never defines, and where an implementer's reasonable guess silently becomes a normative decision nobody made. The first is the seam. §6.2 rule 2 requires a policy to state "the minimum status each boundary requires", and §6.2 defines NO ORDER on LawStatus. Part 03 repeats the phrase three times without repairing it. The text relates falsified and asserted to the rest and never relates `proved` to `tested` — and LawClaim.scope, LawClaim.precondition and tested.domain make that gap load-bearing: a proof over a narrow precondition and a test 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. That is the same shape Suitability.lean already proved as `no_meet` (finding C3) — "the lower of two levels" over an order with no meet. Which is why this package does NOT invent a total order: an invented order is a normative decision wearing an implementation's clothes. `statedBelow` returns null for "the text does not order these", which is a different answer from false and is the one a policy has to act on. BoundaryPolicy states an accept SET, which needs no order. No Lean is included. The theorem candidate is stated exactly, and so is the condition for wanting it: it decides between the two available repairs, and if the steward takes the accept-set repair there is nothing left to prove. Adding theorems for the other repair before that choice is made would be weight rather than evidence. The other four obligations: InvariantDefinition has no field for the context surfaces §6.1.2 rule 1 requires it to declare; DeltaDescriptor is required with its own content address and never given a shape; the version-label projection is required and never specified; and scope widening is neither permitted nor forbidden. Properties are labelled structural / requires-a-LawClaim / has-a-countermodel, because the general form of Codex's warning is deriving a property from a shape. The countermodel category is non-empty on purpose — an empty one would mean nobody looked, not that the design is sound. Four are executable: a proof narrower than a test; clamped translations as a well-typed non-associative delta space, with the arithmetic witness; scope widening producing two different reports from two legal world snapshots; and the one version conflict §6.2.1 names. Fail-closed everywhere, with a code per refusal and nothing falling through to an accept. Two conditions are deliberately not-assessed rather than refused — over budget and stale snapshot — because §6.1.2 rule 5 requires an outcome distinct from held, and collapsing it to a boolean is how a boundary comes to believe an invariant held when nobody checked it. Reuses rather than reinvents: the full-digest convention and reference kinds come from the fast-path debt-scope probe, which already types RFC-0003 references. 20 controls. ./t check READY, 602 tests. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01DRHMVB9rUYNggn4wLmc1An --- deno.jsonc | 2 +- probes/typed-domain-kernel-v0/README.md | 268 +++++++++++++ .../countermodels/delta-not-associative.json | 22 + .../patch-across-law-weakening.json | 19 + .../proved-narrower-than-tested.json | 26 ++ .../scope-widening-unpinned.json | 22 + .../fixtures/positive/domain-euclidean.json | 43 ++ .../typed-domain-kernel-v0/ts/kernel_test.ts | 353 ++++++++++++++++ .../ts/layer1_domain.ts | 264 ++++++++++++ .../ts/layer2_invariant.ts | 295 ++++++++++++++ .../typed-domain-kernel-v0/ts/layer3_law.ts | 379 ++++++++++++++++++ src/x7B88_evidence_report.myc.md | 2 +- src/x8F88_external_surfaces.myc.md | 5 +- 13 files changed, 1696 insertions(+), 4 deletions(-) create mode 100644 probes/typed-domain-kernel-v0/README.md create mode 100644 probes/typed-domain-kernel-v0/fixtures/countermodels/delta-not-associative.json create mode 100644 probes/typed-domain-kernel-v0/fixtures/countermodels/patch-across-law-weakening.json create mode 100644 probes/typed-domain-kernel-v0/fixtures/countermodels/proved-narrower-than-tested.json create mode 100644 probes/typed-domain-kernel-v0/fixtures/countermodels/scope-widening-unpinned.json create mode 100644 probes/typed-domain-kernel-v0/fixtures/positive/domain-euclidean.json create mode 100644 probes/typed-domain-kernel-v0/ts/kernel_test.ts create mode 100644 probes/typed-domain-kernel-v0/ts/layer1_domain.ts create mode 100644 probes/typed-domain-kernel-v0/ts/layer2_invariant.ts create mode 100644 probes/typed-domain-kernel-v0/ts/layer3_law.ts 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 |