From 511b5489d3c3725e9b237dc7535168d468383cde Mon Sep 17 00:00:00 2001 From: usurobor Date: Wed, 12 Aug 2026 18:13:57 +0000 Subject: [PATCH 1/3] design: CM execution model with Sigma iterations I1-I4 applied MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Splits the execution model off PR #124 (which stays vision-only so M0 can promote) onto its own review surface, from live main 274342f, with the four iterations Pi accepted in msg-cn-pi-tsc-execution-model-iterations-accepted-18: I1 receipt discriminator bumped to tsc-measurement-receipt/0.2. The 0.1 string is already owned on main by the shipped coh-min receipt, whose core is structurally incompatible; reusing it would assert false compatibility and destroy format as a verifier discriminator. tsc-run-request/0.1 and tsc-sandbox-plan/0.1 keep their version — verified no live artifact claims either string. I2 new acceptance gate 9: a closed schema rejects extra fields but not absent ones. Measured with cue v0.9.2, deleting format, procedure, or result_contract still passes cue vet against #NormalizedCMIR while the runtime refuses all eight. Every canonical block must be provably required, the runtime and verifier must independently refuse absence, and the negative fixture set must carry one missing-block case per canonical top-level block. I3 fact-provenance invariant: any non-scheduler fact the result rule reads must originate in a declared typed step output or evidence predicate; scheduler facts are limited to status, principled skip/refusal/failure, and bounds/coverage. The Ascent-0 consequence is named in the implementation order — separating, pass count, tested-fiber size and the fiber/candidate counts must be republished through their producing steps' typed ports. I4 canonical subject-snapshot construction and digest algorithms are deferred with a fail-closed boundary: a subject kind is executable only when it names a versioned snapshot/digest scheme; unknown schemes refuse. --- .../cm-language/runtime/CM-EXECUTION-MODEL.md | 696 ++++++++++++++++++ 1 file changed, 696 insertions(+) create mode 100644 research/cm-language/runtime/CM-EXECUTION-MODEL.md diff --git a/research/cm-language/runtime/CM-EXECUTION-MODEL.md b/research/cm-language/runtime/CM-EXECUTION-MODEL.md new file mode 100644 index 0000000..b74987a --- /dev/null +++ b/research/cm-language/runtime/CM-EXECUTION-MODEL.md @@ -0,0 +1,696 @@ +# CM Execution Model: JSON Property Graph and `coh` Runtime + +Status: proposed foundational design; exact wire details may be clarified by implementation evidence before ABI freeze +Scope: executable JSON IR, linking, execution, evidence, and verification +Deferred: `.cm` surface syntax and compiler implementation +Authority: review candidate until accepted through the project-native review path + +## Decision + +TSC will make a JSON execution model work before extending the `.cm` compiler. +The compiler will later lower `.cm` into this model; it will not define a second +runtime ontology. + +The executable heart of a CM is a finite typed directed acyclic graph of +property checkers. Every checker has the same logical execution envelope, while +its input, output, configuration, evidence, capability, and bound contracts are +parametric and explicit. + +A complete CM is slightly more than that graph: + +> A CM is a governing question, a typed property-checker graph, a declarative +> result derivation, an evidence-bearing receipt contract, and any warrant +> obligations required to support its claims. + +This distinction is load-bearing. Checkers produce local facts and evidence. +They do not set the CM's final result. `coh` executes the graph, evaluates the +CM-owned result rule, and emits a `MeasurementReceipt` that a verifier can +recompute and accept or refuse. + +## Why this is the next boundary + +The repository contains two useful but incomplete execution witnesses: + +- `coh-min` loads a hand-authored `NormalizedCMIR`, links a small plan, executes + an input-sensitive `file.exists` check, and emits a verified receipt. Its + result derivation and checker dispatch are still CM-specific OCaml. +- Ascent-0 executes a seven-provider graph with retained alternatives, phase + ordering, oracle evidence, and result-specific receipt constraints. Its + runtime contracts are local to that CM family. + +Those witnesses constrain the general model from opposite directions. An +ordinary repository check proves that the model is usable. Ascent-0 proves that +it can retain alternatives, respect phase barriers, carry stronger evidence, +and discharge Core-grounded warrant obligations. Neither witness alone is a +sufficient ABI-freeze test. + +The immediate engineering objective is therefore: + +```text +JSON CM -> generic linker -> generic checker DAG runtime + -> declarative result evaluator -> MeasurementReceipt -> verifier +``` + +A CM must be addable as data plus provider implementations. Adding a second CM +must not require a `cm_id` branch, a new CM-specific classifier, or a hand-wired +execution pipeline in `coh`. + +## First principles + +### 1. Measurement, not mutation + +A CM may observe, calculate, judge, invoke a child CM, consult a bounded oracle, +or apply a pure transform. It does not admit, merge, release, repair, mutate the +measured project, or exercise project authority. Actors, CNOS, and CDS retain +those powers. + +### 2. Explicit dataflow + +Edges carry typed values or artifact references. Dependencies are derived from +input bindings, not hidden provider calls or shared mutable state. A node becomes +ready only when its required inputs are available. + +### 3. Bounded execution + +The v0 graph is finite and acyclic. Every checker declares its resource and +capability envelope. Recursion, mutation, unbounded loops, and unrestricted +general-purpose control flow are absent. Bounded collection operators may be +added only with explicit size and depth limits. + +### 4. Evidence before claim strength + +A result class may require warrant obligations. Providers must produce the +declared evidence; the runtime must retain it; the verifier must refuse a result +whose evidence does not discharge the required obligations. TSC Core supplies +the semantic and warrant foundation. It is not a separate runtime stage. + +### 5. Recomputable results + +The final result is a pure, total, bounded function of named run facts and +retained evidence predicates. Narrative derivation text is documentation, not +execution. + +### 6. Fail closed + +Missing bindings, undeclared capabilities, schema mismatches, digest mismatches, +unsupported strong claims, and non-recomputable derivations are refusal or +verification failure. They are never silently downgraded into success. + +## Core ontology + +| Concept | Owns | Does not own | +|---|---|---| +| Property | The local question or fact to be established | Provider selection | +| Checker requirement | Typed interface, capability class, schemas, evidence, bounds | Concrete implementation identity | +| Provider | One implementation of a checker capability | CM result authority | +| `NormalizedStep` | The check the normalized CM requires | Host-specific grants or paths | +| `SandboxPlanStep` | The selected provider, adapters, grants, and discharge proof | New methodology semantics | +| `RunRequest` | Exact CM, subject artifacts, parameters, profile, and ceilings | Host-local artifact identity | +| `CheckOutcome` | Local status, outputs, evidence, provenance, diagnostics | Final CM result | +| Result rule | Exactly one declared CM result from run facts | Provider effects | +| `MeasurementReceipt` | Request/IR/plan binding, trace, evidence, derivation witness, obligations | Mutation or admission authority | + +“Property checker” is the unifying runtime role. Mechanical tools, LLM-backed +judges, child CMs, oracle adapters, and pure transforms implement different +checker classes through one envelope; they are not forced to share one concrete +payload type. + +## Artifact pipeline + +```text +.cm source (later) + | + v +NormalizedCMIR JSON <---- authored directly during JSON-first phase + | + | + RunRequest + provider registry + host policy + v +linker + | + v +SandboxExecutionPlan + | + v +checker DAG runtime + | + v +pure result evaluator + | + v +MeasurementReceipt + | + v +receipt verifier +``` + +Normalization and linking are deliberately different moments: + +- normalization resolves source syntax, defaults, symbols, imports, and schemas + into concrete methodology requirements; +- linking selects concrete providers and host adapters for one `RunRequest`, then + proves that the plan satisfies the normalized requirements without granting + more authority than was declared. + +`CompiledCM` is not a second execution ontology. It is deferred. If later useful, +it may be a content-addressed cache/envelope around normalized IR and reusable +link metadata. The per-run `SandboxExecutionPlan` remains the only concrete +execution binding. + +## JSON document family + +The names and semantics below are the backbone for `tsc-cm-ir/0.2`. Field +spelling may be refined when the CUE schema and two-sided fixtures are built, but +implementations must preserve the boundaries between these objects. + +### `NormalizedCMIR` + +The normalized IR is closed, concrete, portable, and content-addressed. It +contains no measurement result and no concrete provider binding. + +```json +{ + "format": "tsc-cm-ir/0.2", + "cm": { + "id": "example.repo-basics", + "version": "0.1.0", + "source_digest": "sha256:..." + }, + "question": "Does the repository expose the required entry documentation?", + "inputs": {}, + "steps": [], + "result": {}, + "receipt": {}, + "permissions": {} +} +``` + +Required top-level semantics: + +- `cm` identifies the methodology and its source lineage. +- `question` is the governing measurement question. +- `inputs` declares named, typed subject inputs. +- `steps` is the finite checker DAG. +- `result` declares the result vocabulary, executable rules, and warrant + obligations. +- `receipt` selects one closed receipt family and its evidence contract. +- `permissions` is the maximum capability/resource envelope normalization allows + the linker to request. + +### `NormalizedStep` + +```json +{ + "id": "readme_exists", + "kind": "mechanical", + "checker": { + "capability": "fs.file-exists", + "interface": "tsc-checker/0.1" + }, + "inputs": { + "root": { + "from": { "input": "repository" }, + "schema": "tsc://schema/directory-artifact/0.1" + } + }, + "outputs": { + "present": { "schema": "tsc://schema/boolean/0.1" } + }, + "config": { "relative_path": "README.md" }, + "evidence": { + "schema": "tsc://schema/file-observation/0.1", + "required": true + }, + "capabilities": { + "request": ["subject.fs.read"] + }, + "bounds": { + "wall_time_ms": 1000, + "output_bytes": 4096 + }, + "failure_policy": { + "refused": "fact_unavailable", + "incomplete": "fact_unavailable", + "failed": "run_failed" + } +} +``` + +Rules: + +- `id` is unique within the CM. +- `kind` is one of `mechanical`, `semantic_judgment`, `invoke_cm`, `oracle`, or + `transform`. +- `checker.capability` identifies what must be implemented; it does not select + who implements it. +- Every input binds either a CM input or one named output port of another step. + Those bindings define the graph edges. +- Every input, output, and evidence payload has an explicit schema. +- `config` is methodology-owned and portable. Host locators, credentials, and + concrete provider configuration do not belong here. +- Requested capabilities and bounds are ceilings, not grants. +- `failure_policy` maps a checker outcome into run-fact availability or run + status. It must not directly select a CM result class. + +The existing `#TypedStep` and runtime-private step shapes mix requirement and +binding. They are migration sources, not the final executable step contract. +The existing `failure -> ResultClass` shortcut is superseded because it gives a +node hidden authority over the CM result. + +### `RunRequest` + +The run request is a first-class, canonical, content-addressed artifact. + +```json +{ + "format": "tsc-run-request/0.1", + "cm_ir": { "kind": "normalized_cm_ir", "digest": "sha256:..." }, + "subject": { + "repository": { "kind": "directory_snapshot", "digest": "sha256:..." } + }, + "profile": "default", + "parameters": {}, + "capability_ceiling": ["subject.fs.read"], + "bounds": { + "wall_time_ms": 10000, + "child_cm_depth": 4, + "child_cm_calls": 32, + "evidence_bytes": 10485760 + } +} +``` + +Artifact digests identify inputs. Local paths, mount points, URLs, credentials, +and process handles are locators supplied by the host during linking; they do +not replace content identity. Repeating the same request may create a new +execution id, but must not change the canonical request digest. + +### `SandboxExecutionPlan` + +The plan is the linker's closed, concrete answer for one request. + +```json +{ + "format": "tsc-sandbox-plan/0.1", + "request_digest": "sha256:...", + "cm_ir_digest": "sha256:...", + "steps": [ + { + "step_id": "readme_exists", + "provider": { + "id": "coh.fs.file-exists", + "version": "0.1.0", + "digest": "sha256:..." + }, + "adapters": { + "root": { "kind": "readonly_directory", "handle": "subject:repository" } + }, + "grants": ["subject.fs.read"], + "limits": { "wall_time_ms": 1000, "output_bytes": 4096 }, + "discharge": { + "checker_interface": true, + "input_schemas": true, + "output_schemas": true, + "evidence_schema": true, + "capability_subset": true, + "bounds_within_request": true + } + } + ] +} +``` + +The linker must establish all of the following before execution: + +1. every normalized step has exactly one binding; +2. the provider implements the required checker interface and capability class; +3. input, output, and evidence schemas are compatible; +4. grants are sufficient and do not exceed both the step request and the + `RunRequest` ceiling; +5. plan limits are within normalized and request bounds; +6. every artifact adapter is confined to its declared subject surface; +7. provider identities and executable artifacts are pinned by version and + digest. + +Any unproved obligation refuses linking. Missing capability and excess +capability are both errors. + +## Uniform checker contract + +The logical interface is: + +```text +execute(CheckRequest) -> CheckOutcome +``` + +`CheckRequest` contains only the step's declared view: + +```json +{ + "format": "tsc-check-request/0.1", + "execution_id": "...", + "step_id": "readme_exists", + "input_refs": {}, + "config": {}, + "bounds": {}, + "grants": [] +} +``` + +`CheckOutcome` has one closed status and typed payloads: + +```json +{ + "format": "tsc-check-outcome/0.1", + "status": "success", + "outputs": {}, + "evidence": [], + "provenance": { + "provider_digest": "sha256:...", + "request_digest": "sha256:..." + }, + "usage": {}, + "diagnostics": [] +} +``` + +The status is exactly one of: + +- `success`: declared outputs and required evidence are present and valid; +- `incomplete`: the checker ran but could not establish its contracted fact; +- `refused`: policy, capability, bound, or epistemic conditions lawfully + prevented the check; +- `failed`: the checker or adapter malfunctioned. + +Only `success` may populate normal output ports. All statuses may retain +diagnostic evidence. The runtime validates the outcome against the step +contracts before making any output available downstream. + +A provider cannot see undeclared subject data, grant itself capabilities, +invoke arbitrary peers, mutate shared state, or notarize the CM's final result. +If a provider returns a final result field, `coh` rejects or ignores it according +to the closed checker schema; it never treats it as authoritative. + +## Graph execution semantics + +1. The normalized graph must be finite and acyclic. Duplicate ids, unresolved + ports, and schema-incompatible edges fail validation. +2. A step is ready when every required input is available and its plan binding is + valid. +3. Ready steps may execute concurrently. Observable results must not depend on + scheduling order; receipts record actual ordering for audit. +4. A successful, schema-valid outcome publishes its named output ports as + immutable run facts. +5. `incomplete`, `refused`, and `failed` outcomes are retained as run facts and + processed through `failure_policy`. Required downstream inputs that cannot be + produced cause principled `skipped` trace entries, never fabricated values. +6. The runtime terminates when every step is terminal (`success`, `incomplete`, + `refused`, `failed`, or `skipped`) or a run-level bound is reached. +7. The result evaluator then runs exactly once over the immutable fact set. + +The initial model has no general conditional nodes. Conditional progress is +expressed by typed output availability: for example, a semantic checker may +withhold an `admissible_proposal` output, causing realization steps that require +it to be skipped. The result rule interprets that trace explicitly. + +## Declarative result semantics + +`result` declares a closed vocabulary and an ordered, total rule table: + +```json +{ + "classes": ["README_PRESENT", "README_ABSENT", "INCOMPLETE"], + "rules": [ + { + "id": "incomplete-run", + "when": { "not": { "step_status": ["readme_exists", "success"] } }, + "emit": "INCOMPLETE" + }, + { + "id": "present", + "when": { "eq": [{ "fact": "readme_exists.present" }, true] }, + "emit": "README_PRESENT" + } + ], + "default": { "id": "absent", "emit": "README_ABSENT" } +} +``` + +Semantics: + +- rules are evaluated in declaration order; +- the first matching rule emits the result class; +- exactly one terminal `default` is required, making evaluation total; +- every emitted class must be in `classes`; +- expressions are pure JSON ASTs over immutable run facts; +- the v0 algebra contains finite boolean operations, equality and ordered + comparisons, presence/status predicates, and bounded `count`, `all`, and `any`; +- provider calls, mutation, recursion, dynamic code, unbounded iteration, and + host access are forbidden; +- the evaluator records the matched rule id and the exact fact/evidence digests + it read; +- the verifier recomputes the result from the receipt and refuses a mismatch. + +**Fact provenance invariant.** Any non-scheduler fact the result rule reads must +originate in a **declared typed step output** or a **declared evidence predicate**. +Scheduler-owned facts are limited to execution status, principled +skip/refusal/failure, and bound/coverage facts. The generic evaluator must never +reach into runtime-private state. This is what keeps the evaluator generic: a fact +that exists only inside one runtime's internals cannot be referenced by a portable +rule, so a CM that needs it must publish it through a typed port. + +Ordered first-match plus a mandatory default is the foundational v0 choice. It +is intentionally smaller than a general expression language. Static linting +should warn about unreachable or shadowed rules, but the execution semantics are +unambiguous even before such linting is complete. + +## Warrant obligations + +A result class may declare obligations that are stronger than ordinary output +schema validity: + +```json +{ + "class": "LIFT_VALIDATED", + "requires": [ + "retained_alternatives.before_result", + "oracle.commit_before_reveal", + "oracle.separates_candidates", + "roundtrip.supported" + ] +} +``` + +The compiler or normalizer elaborates warrant-bearing language constructs into +these obligations. The linker proves that selected providers can produce the +required evidence. The runtime retains it. The verifier applies the closed +obligation rules. A strong class with absent or contradictory evidence is +invalid even if the result-rule AST would otherwise emit it. + +The initial obligation catalog should include only what the ordinary CM and +Ascent-0 fixtures exercise. It can grow under versioning; an unknown obligation +is not treated as discharged. + +## `MeasurementReceipt` + +The receipt is a closed common core plus one closed, discriminated family +extension. + +The format discriminator is **`/0.2`**, not `/0.1`. `tsc-measurement-receipt/0.1` +is already owned on `main` by the shipped `coh-min` receipt, whose core is +structurally incompatible with the shape below (`cm_id` / `source_digest` / +`plan_digest` / `sandbox_execution_plan` / `execution_trace` / `skipped_steps` +versus `request` / `cm_ir` / `plan` / `runtime` / `trace` / `obligations` / +`extension`). Reusing the string would assert a false compatibility and destroy +`format` as a verifier discriminator. `tsc-cm-ir` is bumped `0.1 → 0.2` for the +same reason. `tsc-run-request/0.1` and `tsc-sandbox-plan/0.1` keep their version: +no live artifact claims either string today. + +```json +{ + "format": "tsc-measurement-receipt/0.2", + "execution_id": "...", + "request": { "digest": "sha256:..." }, + "cm_ir": { "digest": "sha256:..." }, + "plan": { "digest": "sha256:..." }, + "runtime": { "id": "coh", "version": "...", "digest": "sha256:..." }, + "trace": [], + "evidence": [], + "result": { + "class": "README_PRESENT", + "rule_id": "present", + "fact_refs": [] + }, + "obligations": [], + "extension": { + "family": "repository_measurement", + "schema": "tsc://receipt/repository-measurement/0.1", + "value": {} + } +} +``` + +The common core binds: + +- exact request, normalized IR, plan, runtime, and provider identities; +- all step outcomes, principled skips, failures, refusals, and coverage; +- an evidence manifest with content digests and provenance; +- the runtime-derived result and derivation witness; +- declared obligations and their evidence-backed discharge state. + +The extension carries family-specific evidence. Ordinary repository +measurements and Ascent receipts share the core but use different closed +extensions. A loose map of optional blocks is forbidden: the result and family +discriminants determine which evidence is required. + +Receipt verification is a separate operation from receipt creation. It checks +schemas and digests, replays the pure result rule, validates trace/plan +consistency, and applies obligation rules. Static CUE validation alone is not a +runtime verification claim. + +## Child CMs and recursion + +`invoke_cm` is a checker kind. Its provider constructs a child `RunRequest` from +declared parent inputs and returns a child `MeasurementReceipt` as evidence. The +parent may consume only projections declared in the child checker's output +schema; it does not inherit the child's authority or bypass its verifier. + +Recursion is bounded by: + +- a maximum child depth and call count in the `RunRequest`; +- a digest stack that refuses direct or indirect cycles; +- explicit input/output schemas at every boundary; +- a requirement that recursive composition eventually reaches primitive + mechanical, judgment, oracle, or transform providers. + +## Provider linking and the useful part of Spring + +Spring's inversion-of-control model is a useful secondary analogy: the CM +declares what checker capability it needs, and the linker injects a concrete +provider. The plan is the explicit, immutable equivalent of the resulting +wiring. Profiles may influence selection, but the selected provider, version, +digest, adapters, and grants are recorded. + +The model deliberately does not inherit Spring's reflective autowiring, mutable +application context, lifecycle callbacks, AOP interception, implicit global +configuration, or circular dependencies. Reproducible measurement requires +explicit wiring and a closed plan. + +For the graph itself, the Common Workflow Language is the closer precedent: +typed ports, explicit dataflow, and bounded workflow execution. TSC adds the +parts a generic workflow model does not supply: methodology-owned judgment, +warrant obligations, fail-closed provider capabilities, retained evidence, and +independently verifiable measurement receipts. + +## Acceptance gates + +The execution model is not ready to freeze until all of these are executable: + +1. **Genericity:** two structurally different ordinary CMs run through the same + parser, linker, scheduler, result evaluator, receipt writer, and verifier + without `cm_id` dispatch or a CM-specific classifier. +2. **Graph behavior:** at least one CM contains independent steps and a dependent + step, proving typed edges, readiness, principled skip behavior, and + scheduling-independent results. +3. **Input sensitivity:** changing a measured subject changes retained evidence + and the verified result where the CM says it should. +4. **Link safety:** missing capabilities, excess grants, provider digest + mismatch, unresolved adapters, and schema-incompatible edges fail closed. +5. **Result honesty:** undeclared classes, non-total rules, result/witness + mismatch, and provider-supplied final results are rejected. +6. **Evidence honesty:** a strong result missing required evidence is rejected. +7. **Confinement:** path escape and undeclared subject access are denied and + retained in the trace. +8. **Two-sided ABI proof:** an ordinary check-style CM and Ascent-0 both run + through this artifact family before the shared ABI is frozen. +9. **Presence, not merely exactness.** A closed schema rejects *extra* fields; it + does not by itself reject an *absent* block. Measured on the shipped IR with + cue v0.9.2: deleting `format`, `procedure`, or `result_contract` still passes + `cue vet -d '#NormalizedCMIR'` — a concrete literal unifies to itself when + omitted, and an open struct or list is complete as `{}` / `[]`. The runtime + refuses all eight. Two obligations therefore bind independently: + - every canonical block and every runtime-consumed field must be **provably + required** by the schema (concrete-typed, not an open struct or list), not + merely protected against extras; + - the runtime and the verifier must **independently refuse absence**, so + neither mechanism is load-bearing alone. + + The negative fixture set must contain **one missing-block case per canonical + top-level block** for `NormalizedCMIR` and `MeasurementReceipt` — including the + selected closed receipt extension — and per runtime-consumed canonical block for + `RunRequest` and `SandboxExecutionPlan`. This is deliberately stronger than + `cue vet` alone. An IR declaring no work and no vocabulary must not validate. + +The Ascent gate is structural, not a claim that Ascent-0 proved blind-LLM +generative correctness. It historically proved firewall-safe mechanism-side +identification; that scope remains unchanged. + +## Implementation order + +1. Accept this execution model as the bounded design backbone for the M1 + contract work. +2. Define closed CUE/JSON schemas for `NormalizedCMIR`, `RunRequest`, + `SandboxExecutionPlan`, checker request/outcome, and `MeasurementReceipt`. +3. Convert the current README fixture and add a second structurally different + ordinary CM plus negative fixtures. +4. Implement one generic `coh` parser, linker, DAG scheduler, rule evaluator, + receipt writer, and verifier. Delete CM-specific result classification and + dispatch from the acceptance path. +5. Execute a proper multi-check repository CM from JSON. +6. Add the `.cm -> NormalizedCMIR` compiler against the proven JSON target. +7. Reproduce Ascent-0 through the same ABI, repair any lost evidence or phase + semantics, and only then freeze the shared contract. **This step is larger than + a port.** Ascent-0's result rule reads runtime-*derived* quantities that today + are computed inside its runtime and surface only in the receipt's `derivation` + block — `separating`, `pass_count`, `tested_fiber_size`, the identification + fiber size, the fitting-candidate count. Under the fact-provenance invariant + every one of these must be republished through its producing step's typed + output ports or evidence contract: `realization_quotient` publishes the fiber + size, `oracle_reveal_compare` publishes pass count and tested-fiber size, + `descent_predict` publishes separation. Re-shaping those steps — not the + scheduler — is the bulk of the work here, and it is what the generic evaluator + requires in order to classify Ascent-0 without privileged access. + +## Deferred decisions + +The following are intentionally outside the foundational v0 backbone: + +- exact `.cm` syntax and compiler architecture; +- package registry, dependency resolution, and remote distribution; +- remote provider transport and CNOS-host protocol; +- cross-run cache semantics; +- unrestricted scatter/gather or streaming collection dataflow; +- a complete Core warrant-obligation catalog; +- signature and transparency-log policy; +- whether a reusable `CompiledCM` cache is worth introducing; +- **canonical subject-snapshot construction and digest algorithms.** `RunRequest` + binds a subject by content digest, but how a snapshot of a given subject kind is + constructed and digested — a git tree object, a Merkle digest over a declared + file set, the treatment of ignored or untracked files — is not fixed here, and + fixing it for every future subject kind now would be guessing. The boundary is + fail-closed: **a subject kind is executable only when it names a versioned + snapshot/digest scheme; an unknown or unnamed scheme refuses.** Local paths + remain locators, never identity. The first repository-subject M1 fixture must + choose and name its exact scheme before it may make any reproducibility claim. + +Deferral does not make these free-form extension points. Until versioned, they +are absent and must fail closed if encountered. + +## Design invariants + +The implementation is conformant only while these statements remain true: + +- JSON is the executable IR; `.cm` is a later authoring language that lowers to + it. +- A CM's executable heart is a finite typed property-checker DAG. +- Every checker uses one logical envelope with explicit typed contracts. +- Properties and checker requirements are distinct from provider + implementations. +- Normalized requirements are distinct from linked plan bindings. +- Checkers produce facts and evidence; the CM-owned rule produces the result. +- Results are pure, total, bounded, and independently recomputable. +- Strong claims are limited by retained evidence and discharged obligations. +- `MeasurementReceipt` is the evidence-bearing output boundary. +- CMs measure; actors and project-native processes retain mutation and authority. +- Ordinary-CM usability and Ascent-0 evidence semantics jointly constrain the + ABI before freeze. + From 61ba4d2a13924a2fe0e097391ee9ec95d611fef9 Mon Sep 17 00:00:00 2001 From: usurobor Date: Thu, 13 Aug 2026 00:15:32 +0000 Subject: [PATCH 2/3] design: apply Pi's seven-point correction pass to the CM execution model 1. Required vs optional output ports. A success must publish every required output or the outcome is rejected; an optional output may lawfully be withheld, and a downstream required binding on an absent optional port becomes a principled skip naming the port. This resolves the contradiction between 'success publishes its declared outputs' and a semantic checker successfully withholding admissible_proposal. Withholding a required output is not a control mechanism. 2. Recursion. v0 forbids unbounded recursion and general control flow; bounded invoke_cm recursion is permitted only under the RunRequest's named child_cm_depth, child_cm_calls, and digest-cycle limits. Recursion with no named ceiling is not expressible. 3. The canonical RunRequest example names a versioned subject snapshot scheme (directory-merkle/0.1), and the text requires every subject entry to name one so a verifier can recompute identity rather than trust it. 4. Requiredness. Replaced the concrete-typed guidance, which pointed at the wrong lever: a concrete literal is the case that slips through, while cm_id: string is caught. Now requires CUE's field!: marker or a fixture-proved equivalent, plus a non-vacuity fixture so a schema cannot pass by validating nothing. 5. Ascent producer map completed with realization_fit publishing the fitting-candidate count, and a rule that any input without a named producing step is a gap to close rather than a fact the evaluator may reach for. 6. New gates 10 and 11: a digest-mismatch negative fixture per binding (request/IR/plan), and checker configuration schemas owned by the capability contract and validated at link time, with a negative fixture. 7. git diff --check clean. --- .../cm-language/runtime/CM-EXECUTION-MODEL.md | 96 +++++++++++++++---- 1 file changed, 79 insertions(+), 17 deletions(-) diff --git a/research/cm-language/runtime/CM-EXECUTION-MODEL.md b/research/cm-language/runtime/CM-EXECUTION-MODEL.md index b74987a..995ab59 100644 --- a/research/cm-language/runtime/CM-EXECUTION-MODEL.md +++ b/research/cm-language/runtime/CM-EXECUTION-MODEL.md @@ -73,9 +73,16 @@ ready only when its required inputs are available. ### 3. Bounded execution The v0 graph is finite and acyclic. Every checker declares its resource and -capability envelope. Recursion, mutation, unbounded loops, and unrestricted -general-purpose control flow are absent. Bounded collection operators may be -added only with explicit size and depth limits. +capability envelope. Mutation, unbounded loops, and unrestricted general-purpose +control flow are absent. Bounded collection operators may be added only with +explicit size and depth limits. + +**Unbounded recursion is forbidden; bounded `invoke_cm` recursion is permitted.** A +CM may invoke a child CM, and a child may do the same, but only under the limits the +`RunRequest` names — `child_cm_depth`, `child_cm_calls`, and a digest stack that +refuses direct or indirect cycles. Exceeding any limit, or re-entering a digest +already on the stack, refuses fail-closed. Recursion with no named ceiling is not +expressible: the ceiling is part of the request, not a runtime default. ### 4. Evidence before claim strength @@ -213,7 +220,7 @@ Required top-level semantics: } }, "outputs": { - "present": { "schema": "tsc://schema/boolean/0.1" } + "present": { "schema": "tsc://schema/boolean/0.1", "required": true } }, "config": { "relative_path": "README.md" }, "evidence": { @@ -265,7 +272,11 @@ The run request is a first-class, canonical, content-addressed artifact. "format": "tsc-run-request/0.1", "cm_ir": { "kind": "normalized_cm_ir", "digest": "sha256:..." }, "subject": { - "repository": { "kind": "directory_snapshot", "digest": "sha256:..." } + "repository": { + "kind": "directory_snapshot", + "scheme": "directory-merkle/0.1", + "digest": "sha256:..." + } }, "profile": "default", "parameters": {}, @@ -284,6 +295,12 @@ and process handles are locators supplied by the host during linking; they do not replace content identity. Repeating the same request may create a new execution id, but must not change the canonical request digest. +Every subject entry MUST name a versioned `scheme` alongside its `kind` and +`digest`. The scheme fixes how the snapshot is constructed and digested, so a +verifier can recompute identity rather than trust it. An absent or unrecognized +scheme refuses fail-closed — see §Deferred decisions, which defers the catalog of +schemes, not the requirement to name one. + ### `SandboxExecutionPlan` The plan is the linker's closed, concrete answer for one request. @@ -385,6 +402,20 @@ Only `success` may populate normal output ports. All statuses may retain diagnostic evidence. The runtime validates the outcome against the step contracts before making any output available downstream. +**Required and optional output ports.** Each declared output is `required: true` +(default) or `required: false`. A `success` outcome MUST publish every **required** +output; missing one is a contract violation and the outcome is rejected, not +downgraded. An **optional** output may be absent from a `success` outcome — this is +lawful withholding, not failure. A downstream step whose required input binds an +absent optional port is a principled `skipped` entry in the receipt trace, naming +the unpublished port. + +This is what makes conditional progress expressible without conditional nodes: a +semantic checker that declares `admissible_proposal` as an optional output can +succeed while withholding it, and the realization steps that require it skip +visibly. Without the required/optional distinction, "success publishes its declared +outputs" and "a successful checker may withhold a proposal" contradict each other. + A provider cannot see undeclared subject data, grant itself capabilities, invoke arbitrary peers, mutate shared state, or notarize the CM's final result. If a provider returns a final result field, `coh` rejects or ignores it according @@ -399,7 +430,9 @@ to the closed checker schema; it never treats it as authoritative. 3. Ready steps may execute concurrently. Observable results must not depend on scheduling order; receipts record actual ordering for audit. 4. A successful, schema-valid outcome publishes its named output ports as - immutable run facts. + immutable run facts. Every **required** output must be present or the outcome is + rejected; an absent **optional** output is lawful and publishes nothing for that + port. 5. `incomplete`, `refused`, and `failed` outcomes are retained as run facts and processed through `failure_policy`. Required downstream inputs that cannot be produced cause principled `skipped` trace entries, never fabricated values. @@ -408,9 +441,11 @@ to the closed checker schema; it never treats it as authoritative. 7. The result evaluator then runs exactly once over the immutable fact set. The initial model has no general conditional nodes. Conditional progress is -expressed by typed output availability: for example, a semantic checker may -withhold an `admissible_proposal` output, causing realization steps that require -it to be skipped. The result rule interprets that trace explicitly. +expressed by typed output availability: a semantic checker declaring +`admissible_proposal` as an **optional** output may succeed while withholding it, +causing realization steps that require it to skip. The result rule interprets that +trace explicitly. Withholding a **required** output is not available as a control +mechanism — it is a rejected outcome. ## Declarative result semantics @@ -607,10 +642,18 @@ The execution model is not ready to freeze until all of these are executable: cue v0.9.2: deleting `format`, `procedure`, or `result_contract` still passes `cue vet -d '#NormalizedCMIR'` — a concrete literal unifies to itself when omitted, and an open struct or list is complete as `{}` / `[]`. The runtime - refuses all eight. Two obligations therefore bind independently: - - every canonical block and every runtime-consumed field must be **provably - required** by the schema (concrete-typed, not an open struct or list), not - merely protected against extras; + refuses all eight. Note the direction: the **concrete literal is the case that + slips through** — it unifies to itself when omitted — while `cm_id: string` is + not concrete and *is* caught. Concreteness is therefore not the lever. Two + obligations bind independently: + - every canonical block and every runtime-consumed field must be **required by + construction**, using CUE's required-field marker `field!:` (or a mechanism + proved equivalent by fixture), not merely protected against extras. Measured + with cue v0.9.2: `format!:` / `procedure!:` / `result!:` reject exactly the + absences that `format:` / `procedure:` / `result:` admit. The schema must also + be **non-vacuous** — carry a fixture proving it rejects something it ought to + reject, so an accidentally-empty or misreferenced definition cannot pass by + validating nothing; - the runtime and the verifier must **independently refuse absence**, so neither mechanism is load-bearing alone. @@ -620,6 +663,22 @@ The execution model is not ready to freeze until all of these are executable: `RunRequest` and `SandboxExecutionPlan`. This is deliberately stronger than `cue vet` alone. An IR declaring no work and no vocabulary must not validate. +10. **Digest binding.** A receipt whose `request`, `cm_ir`, or `plan` digest does + not match the artifact it was produced from is refused by the verifier. Carry a + negative fixture per binding — a receipt with a mutated request digest, one with + a mutated IR digest, one with a mutated plan digest — each of which must fail + verification even though every field is individually well-typed. Digests that + are never checked are decoration. + +11. **Checker configuration schemas are owned and validated.** A step's `config` is + methodology-owned and portable, so its shape is owned by the **checker + capability contract**, not by the CM and not by the provider: the capability + declares a config schema, the linker validates the normalized step's `config` + against the schema of the capability it binds, and a config that does not + validate refuses at link time rather than reaching the provider. A provider may + narrow nothing and widen nothing. Carry a negative fixture: a step whose + `config` violates its capability's schema fails linking. + The Ascent gate is structural, not a claim that Ascent-0 proved blind-LLM generative correctness. It historically proved firewall-safe mechanism-side identification; that scope remains unchanged. @@ -644,11 +703,14 @@ identification; that scope remains unchanged. block — `separating`, `pass_count`, `tested_fiber_size`, the identification fiber size, the fitting-candidate count. Under the fact-provenance invariant every one of these must be republished through its producing step's typed - output ports or evidence contract: `realization_quotient` publishes the fiber - size, `oracle_reveal_compare` publishes pass count and tested-fiber size, - `descent_predict` publishes separation. Re-shaping those steps — not the + output ports or evidence contract: `realization_fit` publishes the + fitting-candidate count, `realization_quotient` publishes the identification + fiber size, `descent_predict` publishes separation, and `oracle_reveal_compare` + publishes pass count and tested-fiber size. Re-shaping those steps — not the scheduler — is the bulk of the work here, and it is what the generic evaluator - requires in order to classify Ascent-0 without privileged access. + requires in order to classify Ascent-0 without privileged access. Any rule input + with no producing step named here is a gap to close before conversion, not a + fact the evaluator may reach for. ## Deferred decisions From ecf3fbd9590449e131ef17f8799808f5f9caa30c Mon Sep 17 00:00:00 2001 From: usurobor Date: Sat, 22 Aug 2026 22:55:40 +0000 Subject: [PATCH 3/3] =?UTF-8?q?design:=20whitespace-only=20=E2=80=94=20str?= =?UTF-8?q?ip=20trailing=20spaces=20and=20the=20EOF=20blank=20line?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit No semantic change. Clears the one mechanical gate Pi held the #128 exact-head GO on: git diff --check reported trailing whitespace on the three metadata lines and a new blank line at EOF. --- research/cm-language/runtime/CM-EXECUTION-MODEL.md | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/research/cm-language/runtime/CM-EXECUTION-MODEL.md b/research/cm-language/runtime/CM-EXECUTION-MODEL.md index 995ab59..56678be 100644 --- a/research/cm-language/runtime/CM-EXECUTION-MODEL.md +++ b/research/cm-language/runtime/CM-EXECUTION-MODEL.md @@ -1,8 +1,8 @@ # CM Execution Model: JSON Property Graph and `coh` Runtime -Status: proposed foundational design; exact wire details may be clarified by implementation evidence before ABI freeze -Scope: executable JSON IR, linking, execution, evidence, and verification -Deferred: `.cm` surface syntax and compiler implementation +Status: proposed foundational design; exact wire details may be clarified by implementation evidence before ABI freeze +Scope: executable JSON IR, linking, execution, evidence, and verification +Deferred: `.cm` surface syntax and compiler implementation Authority: review candidate until accepted through the project-native review path ## Decision @@ -755,4 +755,3 @@ The implementation is conformant only while these statements remain true: - CMs measure; actors and project-native processes retain mutation and authority. - Ordinary-CM usability and Ascent-0 evidence semantics jointly constrain the ABI before freeze. -