refactor: harden runtime dispatch and measure contract coverage

.github/workflows/checks.yml

@@ -16,6 +16,7 @@ jobs:
       - name: Formatting and transport-free contracts
         run: |
           cargo fmt --all --check
+          cargo clippy --locked --workspace --all-targets --all-features -- -D warnings
           cargo test --locked --workspace
       - name: MCP and controlled worker contracts
         run: |

README.md

@@ -81,6 +81,9 @@ One registered operation consumes/returns strings, with explicit submission, cla
 
 ## Verification
 
+The [runtime contract](docs/specification.md) maps supported behavior to executable
+tests and distinguishes local checkpoints from unimplemented storage features.
+
 ```sh
 cargo fmt --all --check
 cargo test --locked --workspace

crates/syntax/src/lib.rs

@@ -2,9 +2,9 @@
 pub mod ast;
 pub use ast::{parse_program, Atom, Clause, CmpOp, Expr, Lit, ParseError};
 
-/// Aggregate functions usable in rule HEAD arguments only
-/// (`kit_count(P, count(K))`). Lowered internally to a temp relation plus
-/// a group-by fold; the head predicate completes before any reader.
+/// Aggregate syntax recognized in rule heads, such as `kit_count(P, count(K))`.
+/// This crate only parses the syntax; each consumer decides which constructs it
+/// supports. DDlog Runtime currently rejects aggregates during lowering.
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
 pub enum AggFn {
     Count,

docs/hardening.md

@@ -0,0 +1,75 @@
+# Hardening baseline — September 6, 2026
+
+Initially assessed `f763612129a0275e53b34869a428c12c1a5bf7a9`, then rebased and
+revalidated against merged `dc50b2f43c430ff406c6145e180afb0cf0584449`, including
+bounded reads. All work is in an isolated checkout. This is a measured baseline and targeted cleanup, not a
+production certification or a claim that all hotspots have been eliminated.
+
+## Changes and validation
+
+- Separated registry operations and pinned activation from semantic dispatch.
+  Existing health/pin admission guards remain in the shared dispatch path.
+- Added registered-request contracts for claim requirements, stale completion,
+  identical/conflicting completion, and lost native acknowledgment. They test
+  the real Rust admission implementation with explicitly simulated transport.
+- Added signed-integer extrema and whole-batch rejection checks relevant to M0.
+- Corrected syntax documentation that implied aggregate execution support.
+- Added the runtime specification with explicit tests and unsupported guarantees.
+- Simplified three Clippy findings without changing public APIs or generated code.
+- Final instrumented Rust suite: 75 passed, one native-compiler test ignored.
+- Final Python suite: 58 passed. Unix socket access required an escalation;
+  the initial sandbox denial occurred before any runtime test executed.
+- Strict all-target/all-feature Clippy passed. After checkpoint ownership was
+  released, a local type alias removed its test-only type-complexity warning.
+  CI now runs strict Clippy alongside the existing contract suites.
+
+## Measurement
+
+Tools: rustc 1.94.1, cargo-llvm-cov 0.9.1, Lizard 1.24.0. Runtime source line
+coverage is 2983/3275 = **91.08%** on the rebased product. On the earlier
+like-for-like baseline it improved from 2755/3065 = **89.89%** to 2795/3067 =
+**91.13%** before the bounded-read merge changed the measured population. These totals
+exclude integration tests, the separate syntax crate and generated/native engine
+code. Host subprocess profiles from the Python suite are included. Forced process
+termination can omit profiling data, so an uncovered function is a review target,
+not proof that no test executes it.
+
+The diagnostic uses Lizard's Rust cyclomatic complexity and executable-line
+coverage in each function's source range from LLVM LCOV. Formula:
+`CC² × (1 − coverage)³ + CC`. This is a line-based CRAP estimate, not branch
+coverage or formal correctness evidence. No hard score gate has been chosen.
+The main dispatch estimate changed from 163.2 (CC106) to 49.4 (CC45); responsibility
+extraction reduces local complexity but does not remove total system complexity.
+
+| Remaining hotspot | CC | Line coverage | CRAP estimate |
+| --- | ---: | ---: | ---: |
+| `src/instance.rs::execute` | 45 | 87.1% | 49.4 |
+| `src/host.rs::standalone` | 6 | 0.0% | 42.0 |
+| `src/lower.rs::lower_clauses_with_operators` | 41 | 92.3% | 41.8 |
+| `src/instance.rs::execute_registry` | 41 | 93.3% | 41.5 |
+| `src/instance.rs::install_processor` | 22 | 68.3% | 37.4 |
+| `src/composition.rs::manifest` | 35 | 92.4% | 35.5 |
+| `src/host.rs::host` | 32 | 88.8% | 33.4 |
+| `src/host.rs::connection` | 26 | 87.9% | 27.2 |
+
+## Reproduction
+
+Install cargo-llvm-cov 0.9.1 and Rust llvm-tools-preview. Run Rust coverage with
+`cargo llvm-cov --locked --workspace --all-features --no-report`. Run the Python
+suite against the instrumented `target/llvm-cov-target/debug/lemmalog-ddlog-mcp`
+by setting `LEMMALOG_DDLOG_MCP`, with `LLVM_PROFILE_FILE` pointing into that coverage
+target using distinct process/module placeholders `%p-%m.profraw`. Then export
+`cargo llvm-cov report --lcov --output-path coverage.lcov`. In an environment with
+Lizard 1.24.0, run `python scripts/complexity_coverage.py coverage.lcov`.
+
+Do not report Rust-only coverage as transport coverage. Do not report this fixture
+suite as native compilation or formal validation of a Lean-to-dataflow compiler.
+
+## Remaining work before a broad clean bill
+
+The bounded-read branch is now included. Review compiler, composition and host
+hotspots in context rather than splitting them merely to reduce a score. Make
+native compiler validation available as explicit evidence, and decide which
+coverage/complexity checks belong in CI after the baseline stabilizes. The current
+library has local pure checkpoints, not integrated generic Iceberg persistence.
+No world, ECS, mission, deployment or external-effect recovery features were added.

docs/specification.md

@@ -0,0 +1,62 @@
+# Runtime contract
+
+This document describes the supported runtime, not planned world or storage
+abstractions. The library and MCP expose the same program admission rules;
+transport does not define program semantics. Focused guides below describe
+wire shapes and operational prerequisites.
+
+| Boundary | Required behavior | Executable evidence |
+| --- | --- | --- |
+| Language | Explicit `int`/`string` schemas; positive recursion and safe stratified negation; reject unsupported constructs and negative cycles before compilation | `tests/ddlog_lowering.rs`, `tests/recursive_lowering.rs` |
+| Definitions | Immutable versions preserve identity and lineage; conditional pointer and lifecycle updates reject stale callers | `tests/processor_registry.rs` |
+| Composition | Resolve exact versions, isolate private names, validate bindings, and preserve public interfaces through nesting | `tests/processor_composition_registry.rs` |
+| Activation | Compile a candidate before replacement; compatible retained inputs replay; failed replacement preserves the prior usable program | `tests/memory_runtime.rs` |
+| Input changes | Validate the complete input transaction before execution; acknowledged state changes only after completion; uncertain native failure disables continued use | `tests/memory_runtime.rs` |
+| Bounded reads | Bound returned rows/bytes, bind continuation to the backend revision and request, drain selected native output after local limit errors; no indexed-query latency guarantee | `tests/memory_runtime.rs`, [bounded reads](bounded-reads.md) |
+| Registered requests | Claim before completion; preserve late results with explicit freshness; identical completion is idempotent; conflicting completion fails; uncertain settlement never implies permission to repeat provider work | `tests/registered_requests.rs` |
+| Shared access | Connections share one owner; disconnect does not stop it; pinned versions and exported ports remain enforced | `tests/test_shared_host.py`, `tests/upstream_compatibility.rs` |
+| Checkpoints | Explicit pure-backend checkpoint; integrity-checked restore into a fresh backend; reconstruct outputs from acknowledged inputs | `tests/memory_runtime.rs`, [checkpoint contract](checkpoints.md) |
+| Compatibility | Preserve previously published definition hashes, native source fixtures, and MCP tool schemas unless a deliberate compatibility change is declared | `tests/upstream_compatibility.rs` |
+
+## What an acknowledgment establishes
+
+A completed input operation means the native program acknowledged its transaction.
+It does not mean that inputs are durable, an external provider completed, or an
+Iceberg catalog published anything. Program installation version and backend
+revision are distinct; callers must not use a version number as a transaction ID.
+
+An explicit checkpoint has its own durability outcome. Directory-sync failure
+after replacement is uncertain publication and requires inspection before retry.
+Checkpoint integrity is corruption detection, not authentication. Caller metadata
+does not automatically reconstruct registry pins, public interfaces, or provider
+admission state. See [checkpoints](checkpoints.md) for supported contents and limits.
+
+## Deliberate limits
+
+- The parser recognizes more syntax than the runtime supports. Parsing is not
+  compilation, and compilation is not a mathematical correctness proof.
+- Registered-operation programs do not compose with ordinary program nodes.
+  Imported native operators and registered operations cannot use checkpoint
+  format 1. Ordinary inference state is session-local.
+- One host owns one graph instance. No fleet scheduling, world semantics,
+  automatic crash recovery, distributed transaction, or provider exactly-once
+  guarantee is supplied.
+- Generic Arrow/Iceberg persistence is not integrated. Separate experiments are
+  evidence for their scoped scenarios, not shipped runtime guarantees.
+- `why` provides direct rule witnesses, not a Lean proof, recursive provenance,
+  or a certificate for a source-to-dataflow compiler.
+
+## Validation scope
+
+Default Rust and Python suites validate runtime contracts using controlled native
+transport fixtures. They do not execute the actual DDlog compiler or certify the
+upstream engine. [Native acceptance](building.md#native-acceptance) is a separate
+configured run. Record whether native evidence is a fresh compilation or reuse of
+a hash-verified executable.
+
+Coverage must include the instrumented MCP binary exercised by Python, otherwise
+host coverage is understated. Generated native sources, Rust host code, syntax
+code, and Python worker coverage are separate populations. Report the population
+and skipped tests with any percentage. Complexity/coverage scores prioritize
+review; they do not prove correctness or justify splitting code solely to improve
+a metric.

scripts/complexity_coverage.py

@@ -0,0 +1,45 @@
+#!/usr/bin/env python3
+"""Diagnostic CRAP estimates from Lizard Rust complexity and LLVM LCOV lines.
+
+Requires lizard==1.24.0. Run from the repository root, passing an LCOV file.
+This uses executable-line coverage, not branch coverage. No score is invented
+for functions without coverage mapping. Generated native sources are excluded.
+"""
+import json
+from pathlib import Path
+import sys
+
+import lizard
+
+
+def report(path):
+    coverage = {}
+    current = None
+    for line in Path(path).read_text().splitlines():
+        if line.startswith("SF:"):
+            current = str(Path(line[3:]).resolve())
+            coverage.setdefault(current, {})
+        elif line.startswith("DA:") and current is not None:
+            number, hits, *_ = line[3:].split(",")
+            number, hits = int(number), int(hits)
+            coverage[current][number] = max(hits, coverage[current].get(number, 0))
+    rows = []
+    for source in sorted(Path("src").glob("*.rs")):
+        lines = coverage.get(str(source.resolve()), {})
+        for function in lizard.analyze_file(str(source)).function_list:
+            hits = [count for number, count in lines.items()
+                    if function.start_line <= number <= function.end_line]
+            fraction = sum(count > 0 for count in hits) / len(hits) if hits else None
+            complexity = function.cyclomatic_complexity
+            rows.append({
+                "file": str(source), "function": function.name,
+                "line": function.start_line, "complexity": complexity,
+                "line_coverage": fraction,
+                "crap_estimate": (complexity ** 2 * (1 - fraction) ** 3 + complexity
+                                  if fraction is not None else None),
+            })
+    return sorted(rows, key=lambda row: row["crap_estimate"] or 0, reverse=True)
+
+
+if __name__ == "__main__":
+    print(json.dumps(report(sys.argv[1]), indent=2))

src/composition.rs

@@ -100,7 +100,7 @@ pub fn validate_interface(program: &ProgramDefinition) -> Result<()> {
         if !outputs.insert(name.clone()) {
             return Err(format!("Duplicate interface output {name}"));
         }
-        if !schemas.get(name).is_some_and(|schema| !schema.input) {
+        if !matches!(schemas.get(name), Some(schema) if !schema.input) {
             return Err(format!(
                 "Interface output {name} must name a declared derived relation"
             ));