Separate world ownership from clients and expose authored source inspection

README.md

@@ -41,7 +41,7 @@ fn main() -> Result<(), String> {
 
 `ProgramInstance::execute` takes an operation name and JSON arguments and returns a result or semantic error. It has no JSON-RPC envelope or connection lifetime. MCP delegates to this same admission path, including immutable pins, exported ports and registered request restrictions. A caller owns and drops each independent instance. Give independent backends distinct build directories.
 
-`Backend` is the lower-level compilation/execution interface. `Backend::install_composition(&registry, &manifest)` validates exact registry pins and typed bindings, then installs the composition and returns its `CompositionResolution` with generated input/output relation names. Use `ProgramInstance` for public-interface enforcement or registered operations. Existing MCP queries and deltas contain DDlog row text; library callers can use `Backend::query_typed` and `export_inputs` for typed rows. `why` returns direct rule-variable witnesses, not recursive proof trees or confidence/provenance.
+`Backend` is the lower-level compilation/execution interface. `Backend::install_composition(&registry, &manifest)` validates exact registry pins and typed bindings, then installs the composition and returns its `CompositionResolution` with generated input/output relation names. Use `ProgramInstance` for public-interface enforcement or registered operations. Existing MCP queries and deltas contain DDlog row text; library callers can use `Backend::query_typed` and `export_inputs` for typed rows. `why` returns direct rule-variable witnesses, not recursive proof trees or confidence/provenance. Generated text has a numbered lowering version (`docs/worlds.md`, "Lowering versions"): library instances build version 1 (rule witnesses, every derived relation exported) unless `set_lowering_version(2)` selects the lean form that managed worlds build; registered records and their hashes are verified under their own recorded version either way.
 
 For large maintained outputs, use `Backend::query_typed_bounded` with exact positional filters, row/JSON-byte limits and an explicit continuation. It streams only the selected relation and drains its native dump with bounded host accumulation. `apply_without_deltas` acknowledges mutations without transporting unrelated derived changes. See [bounded output reads](docs/bounded-reads.md) for limits and scan costs.
 

crates/syntax/src/ast.rs

@@ -82,12 +82,19 @@ enum Tok {
     Punct(&'static str), // :- , ( ) . ! < =< >= > \= : _
 }
 
-fn tokenize(src: &str) -> Result<Vec<Tok>, ParseError> {
+type TokenSpans = (Vec<Tok>, Vec<(usize, usize)>);
+
+fn tokenize_spanned(src: &str) -> Result<TokenSpans, ParseError> {
+    let mut spans = Vec::new();
+    let mut offsets: Vec<_> = src.char_indices().map(|(offset, _)| offset).collect();
+    offsets.push(src.len());
     let mut toks = Vec::new();
     let b: Vec<char> = src.chars().collect();
     let mut i = 0;
     let n = b.len();
     while i < n {
+        let start = i;
+        let previous = toks.len();
         let c = b[i];
         if c.is_whitespace() {
             i += 1;
@@ -152,14 +159,17 @@ fn tokenize(src: &str) -> Result<Vec<Tok>, ParseError> {
             i += punct.len();
             toks.push(Tok::Punct(punct));
         }
+        if toks.len() > previous {
+            spans.push((offsets[start], offsets[i]));
+        }
     }
-    Ok(toks)
+    Ok((toks, spans))
 }
 
 // ------------------------------------------------------------------- parser
 
 pub fn parse_program(src: &str) -> Result<Vec<Clause>, ParseError> {
-    let toks = tokenize(src)?;
+    let (toks, _) = tokenize_spanned(src)?;
     let mut p = Parser { toks, pos: 0 };
     let mut clauses = Vec::new();
     while p.pos < p.toks.len() {
@@ -168,6 +178,31 @@ pub fn parse_program(src: &str) -> Result<Vec<Clause>, ParseError> {
     Ok(clauses)
 }
 
+/// An authored clause and its exact UTF-8 byte range, excluding leading comments.
+#[derive(Debug, Clone)]
+pub struct SpannedClause {
+    pub clause: Clause,
+    pub start: usize,
+    pub end: usize,
+}
+
+/// Parse source for inspection without lowering or native execution.
+pub fn parse_program_spanned(src: &str) -> Result<Vec<SpannedClause>, ParseError> {
+    let (toks, spans) = tokenize_spanned(src)?;
+    let mut parser = Parser { toks, pos: 0 };
+    let mut result = Vec::new();
+    while parser.pos < parser.toks.len() {
+        let start = spans[parser.pos].0;
+        let clause = parser.clause()?;
+        result.push(SpannedClause {
+            clause,
+            start,
+            end: spans[parser.pos - 1].1,
+        });
+    }
+    Ok(result)
+}
+
 struct Parser {
     toks: Vec<Tok>,
     pos: usize,

docs/inspection.md

@@ -23,7 +23,9 @@ port indexes, not layout port IDs. Live validation requires a matching channel i
 the stated direction. Unconnected ports cannot be verified from channel data and
 must have no native mapping until supporting observations exist.
 
-Version 1 groups are flat and disjoint: overlapping native membership is rejected.
+Version 1 groups without a `kind` are flat and disjoint boxes: overlapping native
+membership is rejected. `kind: "module"` groups are blocks (below): they may nest
+and a block's members repeat those of its nested blocks.
 Registered definitions may have no native member IDs or mappings; registration is
 not execution. Live bindings are execution-specific and must be revalidated after
 recompilation or restart. Clients still decide whether a group can be laid out
@@ -61,10 +63,58 @@ by `resolve(graph)` when a snapshot is taken, deterministically:
    observed on channels in the stated direction).
 
 A snapshot reports the resolved metadata (`authoredGroups[*].memberIds` are the
-resolved ids, `ports[*].native_ports` include the matched binding) and
-`mapping_error: null`, or the authored metadata unchanged with the error text.
-Resolution is a pure function of the metadata and the observed graph; it never
-consults the registry or invents operators.
+resolved ids, `ports[*].native_ports` include the matched binding, plus a
+`mapping_report`) and `mapping_error: null`, or the authored metadata unchanged
+with the error text. Resolution is a pure function of the metadata and the observed
+graph; it never consults the registry or invents operators.
+
+## Module groups (blocks) and neighbour propagation
+
+An `AuthoredGroup` may carry `kind: "module"` and its `member_match` may carry
+`propagate: true`; both are omitted from the wire form when absent, so existing
+definitions keep their content hash. A module group is a **block, not a box**:
+
+- It skips the layout invariants (whole native subtree, one native parent) and
+  the zero-match rule: a block whose pattern matches nothing resolves to an empty
+  `memberIds` (its report shows `matched: 0`) instead of a mapping error, because
+  the runtime synthesizes blocks without knowing which generated relations the
+  DDlog compiler keeps as named operators. Viewers never draw blocks as boxes.
+- Blocks nest by id: `<parent>/<child>` is a nested block of `<parent>` when both
+  have `kind: module`; a parent is declared before its children and its resolved
+  `memberIds` include every nested block's members. Other groups stay disjoint.
+- `validate()` requires a module group to declare `member_match` or `memberIds`.
+
+**Propagation.** After steps 1–2 above, every unclaimed operator adopts the group
+with the most channel neighbours (source or target of any observed channel, self
+loops ignored) among groups whose `member_match.propagate` is `true`; groups
+without the flag never vote, so a box never grows through propagation. Ties go to
+the lowest group index (declaration order). Rounds are synchronous — every adoption
+of a round is computed from the previous round's owners — and repeat until nothing
+changes or 16 rounds have run (`PROPAGATION_ROUNDS`); an operator whose neighbours
+are still unowned after that stays outside every group. Propagation happens before
+the nested-block aggregation, so an operator adopts the deepest block that reached
+it and its ancestors list it too.
+
+Resolved metadata carries the report:
+
+```json
+"mapping_report": {"groups": {"<group id>": {"matched": 3, "propagated": 5}},
+                   "unattributed": 2}
+```
+
+`matched` counts operators claimed by `memberIds`, `scope_name` or `debug_pattern`,
+`propagated` those adopted through neighbours, both for the group that owns the
+operator directly (a nested block's members are not re-counted on its parent), so the
+sum over groups plus `unattributed` is the number of native operators. Every group
+is listed, including boxes (`propagated: 0`). The retained capture stores the
+resolved blocks and the report like any other resolved metadata.
+
+Worlds built from a composition receive synthesized module groups from the world
+manager (`worlds.md`): one per composition node matching the generated relation
+prefix (`\bR_Module<index>_`, `\bR_Composite<index>_` for a nested composition,
+whose own nodes become `<alias>/<child>`), plus `$inputs` (`\bR_Input_`) and
+`$outputs` (`\bR_Output_`), all with `propagate: true`. Hand-authored groups keep
+today's semantics and precedence.
 
 ## Native capture build hook
 

docs/operations.md

@@ -7,7 +7,7 @@
 | `lemmalog_install_rules` | Validate typed rules/operators, compile a candidate, replay retained input, then replace the active unpinned program |
 | `apply_changes` | Transactional insert/delete batch with input set semantics |
 | `lemmalog_query` | Dump one declared or exported output at the last completed transaction |
-| `lemmalog_why` | Direct variable-binding witnesses for an ordinary zero-based rule index; compositions include origin metadata |
+| `lemmalog_why` | Direct variable-binding witnesses for an ordinary zero-based rule index; compositions include origin metadata. Only under lowering version 1: a version 2 build answers with an explicit "Explanations were not compiled for this instance" error |
 | `processor_create`, `processor_publish`, `processor_fork` | Save immutable validated definitions; publication uses an expected version |
 | `processor_get`, `processor_list`, `processor_search` | Inspect exact/current definitions and discover stable identities |
 | `processor_archive`, `processor_restore` | Conditional lifecycle changes using expected version and lifecycle revision |
@@ -27,3 +27,5 @@ A public interface restricts ordinary mutations/queries to its exported names an
 The language supports positive recursion and safe stratified negation. Negative cycles, cycles through native transformers, aggregation, arithmetic, clock builtins and inline facts are rejected before activation. Schemas use signed 64-bit integers or strings; mixed-value columns are unsupported. Control characters unsupported by the pinned DDlog CLI are rejected. Retained inputs require compatible input schemas; derived schemas may change during program replacement.
 
 `why` is not a memory proof tree. Registry content versions, generated source hashes, native implementation hashes, executable hashes and live instance IDs identify different things. Preserve them separately.
+
+Generated text has a numbered **lowering version** (`docs/worlds.md`, "Lowering versions"): version 1, the library default, explains every rule through an `Evidence` relation and exports every derived relation; version 2 (`ProgramInstance::set_lowering_version(2)`, or `lowering_version` on `processor_install`) is the lean form worlds build. `processor_create`/`processor_publish` accept `lowering_version` to record a composition's resolution under version 2; records without the field are version 1 and stay valid. Public relation names and contents do not depend on the version; `instance_info` and the install result report the version built.

docs/worlds.md

@@ -46,7 +46,9 @@ autostart. The operator chooses when to run this owner.
   Imported definitions are named from `names`, an existing association, or derived.
 - `create` takes a `label`, exact `processor` reference, optional `purpose`
   (`instance`, the default, or `test`) and, for tests, non-empty `scenarios`. It does
-  not start a process. Scenarios are validated at creation.
+  not start a process. Scenarios are validated at creation. The world's inspection
+  metadata is the pinned definition's authored metadata; for a composition it also
+  gains synthesized **module groups** (below).
 - `start` takes `id`, records `starting`, then compiles/installs asynchronously.
   Poll `status`, `inspect`, or `inventory` to collect completion or failure.
 - `stop` takes `id`. It cancels managed compiler/native process groups. A pending
@@ -57,7 +59,7 @@ autostart. The operator chooses when to run this owner.
 - `execute` takes world `id`, an inner `operation`, and inner `args`. Definition
   installation/registry mutations are rejected here; world definitions stay pinned.
   Beyond the existing program operations it offers:
-  - `instance_info` adds `revision`, `program_version` and `source_sha256` (sha256 of
+  - `instance_info` adds `revision`, `program_version`, `lowering_version` and `source_sha256` (sha256 of
     the lowered `program.dl`) while the instance is healthy.
   - `apply_changes` adds `revision`.
   - `relations` `{}` → `{revision, relations: [{name, input, fields, count}]}` over the
@@ -153,6 +155,72 @@ through `member_match`/`native_match` resolved at snapshot time (`inspection.md`
 source/debug labels are never converted into fabricated membership. Consumers must
 show lifecycle state alongside captured topology.
 
+**Module groups (A13).** A world pinned to a composition gets one `kind: "module"`
+authored group per node of the pinned `CompositionResolution`, without any
+hand-authored metadata: `{id: "<alias>", name: <library association name of the
+child pin, else the alias>, kind: "module", member_key: "<alias>", member_match:
+{debug_pattern: "\bR_Module<index>_", propagate: true}, provenance: {repository:
+<child processor_id>, revision: <child version>}}`. `<index>` is the node's index in
+the resolution, read from the generated relation prefix (`Module<index>_<relation>`
+for a program node, `Composite<index>_Output_<name>` for a nested composition, whose
+pattern is `\bR_Composite<index>_` and whose own nodes follow it as
+`<alias>/<child alias>`); groups are listed in index order, parent before child,
+then `$inputs` (`\bR_Input_`, name "Inputs") and `$outputs` (`\bR_Output_`,
+name "Outputs"), whose provenance is the world's own pin. Synthesized groups are
+appended after the definition's hand-authored groups; on an `id` or `member_key`
+collision the hand-authored group wins and the synthesized one is dropped. The
+groups are re-derived from the immutable pin on every `start`, so a renamed
+association shows on restart and worlds recorded before this rule gain them; the
+result is persisted in `world.json` and resolved at snapshot time (`inspection.md`:
+propagation, nesting, `mapping_report`), and the retained capture stores the
+resolved blocks like any other group. Programs get no synthesized groups.
+
+**Lowering versions (A14).** The generated DDlog text of a definition has a numbered
+lowering version; public relation names and contents are identical under every
+version, only the text, its hash and the operator count differ.
+- **Version 1** (`LoweringOptions::VERSION_1`, the library default and the form every
+  registered `CompositionResolution` records unless `lowering_version: 2` was passed to
+  `processor_create`/`processor_publish` or `ProcessorRegistry::create_versioned`):
+  every rule is explained through an `Evidence<n>` relation plus a copy rule, every
+  derived relation is an `output relation`, and every composition binding is a copy
+  rule through the bound input's own relation.
+- **Version 2** (`LoweringOptions::VERSION_2`, `{explain: false, export_internal: false,
+  alias_bindings: true}`): no `Evidence` relations (`lemmalog_why` answers with an
+  explicit "Explanations were not compiled for this instance" error); only the
+  composition's external outputs and the relations they copy directly stay `output
+  relation` (a program with an interface keeps its interface outputs; one without keeps
+  everything); and a bound target input is rewritten to its single source relation, so
+  its copy rule and relation disappear. The resolution's `relations` map records each
+  aliased target as `"alias_of": "<generated source relation>"` (resolved through nested
+  `Composite<n>_Input_*` chains), aliased bindings generate no `rules` entry, and the
+  `inputs`/`outputs` maps and `public_relations` are unchanged.
+- `CompositionResolution.lowering_version` (absent, i.e. 1, in records written before
+  this rule) says which text `generated_source_sha256` hashes; `processor_get`, imports
+  and nested references verify a record under its own recorded version, so registered
+  compositions stay valid and are never rewritten. A build selects its version
+  independently of the record: `ProgramInstance::set_lowering_version(2)` (or a
+  `lowering_version` argument to `processor_install`) builds version 2 text from a
+  version 1 pin; the install result and `instance_info` carry `lowering_version`, and
+  `instance_info.source_sha256`, `program_source` and `instance_info.composition`
+  describe the text actually built. Library users keep version 1 unless they opt in.
+- Measured on the X0 composed agent (3 nodes, 126 authored rules, 22 external inputs,
+  30 external outputs, 33 bindings): version 1 lowers to 260 relations (22 input, 112
+  output, 126 `Evidence`) and 252 rules, and its native graph has 2,495 operators
+  (`Operates` events in the capture: 266 Input, 276 AsCollection, 279 Concatenate,
+  241 Consolidate, 239 Probe, 238 InspectBatch, 68 Join, 40 ThresholdTotal, ...);
+  version 2 lowers to 101 relations (22 input, 60 output, 19 internal; the 33 bound
+  inputs are aliased) and 93 rules, and its graph has 1,095 operators (108 Input,
+  96 AsCollection, 119 Concatenate, 62 Consolidate, 61 Probe, 60 InspectBatch, 67 Join,
+  35 ThresholdTotal, ...), 44% of the version 1 count, with the same 52 public
+  relations. Reproduce with
+  `tests/lowering_v2.rs::measure_registered_composition_lowerings` (ignored; takes the
+  registry, processor and version from `DDLOG_LOWERING_*`, the native driver from
+  `DDLOG_RUNTIME_NATIVE_BUILD` and counts the capture named by `DDLOG_OBSERVER_FILE`).
+  `tests/lowering_v2.rs` proves the public relation contents identical at every
+  revision under both versions with the native driver
+  (`native_public_relations_are_identical_under_both_lowerings`, ignored without
+  `DDLOG_RUNTIME_NATIVE_BUILD`).
+
 **Tailer.** Each `start` spawns one capture tailer thread for the new generation. It
 polls the capture file every 100 ms, ingests at most 4 MiB per poll into the shared
 state that `status`/`inspect` snapshot, and exits on `stop`, on owner drop (both
@@ -168,7 +236,8 @@ hold that state without a thread; `inventory {summary: true}` never reads a capt
 `<BUILD_ROOT>/captures/<processor_id>/<version-hex>.json`:
 `{schema_version: 1, processor: {processor_id, version}, world_id, generation,
 captured_at_unix_ms, unresolved_channels, graph: {nodes, edges}, metadata,
-mapping_error}` — topology and resolved authored metadata only, no activity. A later
+mapping_error}` — topology and resolved authored metadata (module groups and
+`mapping_report` included) only, no activity. A later
 generation of any world pinned to that version replaces it. `world.json` records
 `capture_generation` so a recovered world does not capture the same generation twice.