Law 8 at instantiation: a helper, a skill and a snippet are checked as documents

CHANGELOG.md

@@ -3,6 +3,27 @@
 What changed in PACT, newest first. Each entry says what an author can now write, or what now
 holds that did not; the commits are listed under it for whoever wants the detail.
 
+## 2026-11 — law 8 at the moment of instantiation: a helper, a skill and a snippet are checked as documents (13 November)
+
+Law 8 says anything a run creates passes the same checker before it can be asked, and names a
+`run-code` snippet, a `narrowed-new` helper and a skill a run wrote. The reference checked a
+learning proposal's `instructions:` and nothing a run instantiates. A second runtime (Bud Meta
+Harness) checks all three; the functions here are the rules it builds them by, so a definition
+checked there and here is the same document.
+
+- **`checking.with_helper(document, starter, instructions, description=, uses=)`**: the starter's
+  own entry under `<starter>-helper` (`-2`, `-3`… when taken), told `instructions`, on the
+  starter's model. `uses` may narrow it; anything the starter lacks raises `NotNarrower` with
+  `delegation.beyond_its_starter`'s sentence.
+- **`checking.with_skill(document, agent, name, description, content, use_when=)`**: a `skills:`
+  entry, named in the agent's `uses:` when it writes one.
+- **`checking.with_program(document, language, code, description=, runs_for_at_most_ms=)`**: a
+  nondeterministic program under `run-code-<12 hex of the code's sha256>`, its fuel the run's own
+  ceiling; a language with no engine raises `Uncheckable`. The code itself is recorded, never read.
+- **`checking.literal(text, document)`**: words a model wrote are checked as words. `{{` becomes
+  `\{{`; under `template-language: jinja` the text goes in raw blocks.
+- `check_document` on the result is the check.
+
 ## 2026-11 — the TypeScript port computes effects as the checker does
 
 `adapters/typescript/src/effects.ts` is `crates/pact-loader/src/effects.rs` (law 1) in TypeScript,

README.md

@@ -1000,11 +1000,11 @@ framework is an extra.
 |---|---|
 | **Design** | Thesis, 29 binding decisions, FRD (120 requirements), 60-row refusal ledger — complete |
 | **Research** | 14 source-grounded studies, ~15,750 lines, over 140 repos (~15 GB) + 57 papers |
-| **Code** | Loader, diagnostics, schema engine, CLI, harness, resolver, evals, SLO — **5026 tests (1679 Rust + 3347 adapter), clippy clean, TypeScript type-checked** |
+| **Code** | Loader, diagnostics, schema engine, CLI, harness, resolver, evals, SLO — **5034 tests (1679 Rust + 3355 adapter), clippy clean, TypeScript type-checked** |
 | **Adapters** | **All 7 named targets**, proven against one shared conformance suite |
 
 ```bash
-./scripts/test-all.sh          # 5026 tests, Rust + 7 adapters, fully offline
+./scripts/test-all.sh          # 5034 tests, Rust + 7 adapters, fully offline
 ```
 
 **What is still owed** is not hidden — it lives in

adapters/python/src/pact_adapters/checking.py

@@ -15,6 +15,7 @@
 from __future__ import annotations
 
 import copy
+import hashlib
 import shutil
 import subprocess
 import tempfile
@@ -253,3 +254,167 @@ def with_field(document: Mapping[str, Any], agent: str, field: str, value: Any)
     entry[field] = value
     agents[agent] = entry
     return proposed
+
+
+# ------------------------------------------------- what a run instantiates
+#
+# Law 8 is "anything created during a run must pass the *same* checker at the
+# moment it is instantiated" (97 §4, law 8): a `narrowed-new` helper, a skill
+# the run wrote, a `run-code` snippet. Each is put in front of the checker the
+# same way a proposal is: as the document it would make, the starter's own
+# closure with the one new definition added. The functions below build those
+# documents, and the same rules are what a second runtime builds them by, so a
+# definition checked here and one checked there are the same document.
+
+
+class NotNarrower(ValueError):
+    """A helper was described with something its starter does not have. The
+    message is `delegation.beyond_its_starter`'s, so the model reads the same
+    sentence whichever runtime refused it."""
+
+
+def _free_key(entries: Mapping[str, Any] | None, base: str) -> str:
+    """`base`, or `base-2`, `base-3`… the first key `entries` does not hold."""
+    taken = entries or {}
+    if base not in taken:
+        return base
+    n = 2
+    while f"{base}-{n}" in taken:
+        n += 1
+    return f"{base}-{n}"
+
+
+_END_RAW = "{% endraw %}"
+
+
+def literal(text: str, document: Mapping[str, Any]) -> str:
+    """Words a model wrote, as the checker must read them: literally.
+
+    A model's `{{ order }}` is an order number it typed, not a hole the run
+    fills. Under the default template language that is `\\{{`; under
+    `template-language: jinja` it is a raw block, and an `{% endraw %}` inside
+    the words is written between two raw blocks as a string.
+    """
+    if document.get("template-language") != "jinja":
+        out, i = [], 0
+        while True:
+            j = text.find("{{", i)
+            if j < 0:
+                out.append(text[i:])
+                return "".join(out)
+            out.append(text[i:j])
+            out.append("{{" if j > 0 and text[j - 1] == "\\" else "\\{{")
+            i = j + 2
+    if not any(mark in text for mark in ("{{", "{%", "{#")):
+        return text
+    between = "{{ '" + _END_RAW + "' }}"
+    return between.join("{% raw %}" + part + _END_RAW for part in text.split(_END_RAW))
+
+
+def _listed(raw: Any) -> list[str]:
+    if raw is None:
+        return []
+    return [str(x) for x in raw] if isinstance(raw, (list, tuple)) else [str(raw)]
+
+
+def with_helper(
+    document: Mapping[str, Any],
+    starter: str,
+    instructions: str,
+    *,
+    description: str | None = None,
+    uses: Sequence[str] | None = None,
+) -> dict[str, Any]:
+    """The document a `narrowed-new` helper makes: `starter`'s own entry under
+    the key `<starter>-helper`, told `instructions`, running with the
+    starter's `uses:` or the narrower `uses` given, on the starter's model.
+
+    Raises `NotNarrower` when `uses` names anything the starter lacks.
+    """
+    from .delegation import beyond_its_starter
+
+    agents = dict(document.get("agents") or {})
+    entry = {k: v for k, v in dict(agents.get(starter) or {}).items() if k != "name"}
+    if uses is not None:
+        refused = beyond_its_starter(starter, _listed(entry.get("uses")), list(uses))
+        if refused:
+            raise NotNarrower(refused)
+        entry["uses"] = list(uses)
+    said = description.strip() if description and description.strip() else entry.get("description")
+    if said is not None:
+        entry["description"] = literal(str(said), document)
+    entry["instructions"] = literal(instructions, document)
+    agents[_free_key(agents, f"{starter}-helper")] = entry
+    proposed = copy.deepcopy(dict(document))
+    proposed["agents"] = agents
+    return proposed
+
+
+def with_skill(
+    document: Mapping[str, Any],
+    agent: str,
+    name: str,
+    description: str,
+    content: str,
+    *,
+    use_when: str | None = None,
+) -> dict[str, Any]:
+    """The document a skill a run wrote makes: a `skills:` entry, named in
+    `agent`'s `uses:` when the agent writes one (an agent without `uses:`
+    reaches every skill already)."""
+    proposed = copy.deepcopy(dict(document))
+    skills = dict(proposed.get("skills") or {})
+    key = _free_key(skills, name)
+    skill: dict[str, Any] = {"name": name, "description": literal(description, document)}
+    if use_when is not None:
+        skill["use-when"] = literal(use_when, document)
+    skill["content"] = literal(content, document)
+    skills[key] = skill
+    proposed["skills"] = skills
+    agents = dict(proposed.get("agents") or {})
+    entry = agents.get(agent)
+    if isinstance(entry, Mapping) and entry.get("uses") is not None:
+        agents[agent] = {**entry, "uses": [*_listed(entry.get("uses")), key]}
+        proposed["agents"] = agents
+    return proposed
+
+
+#: The engine a snippet in each language runs as. A language with no engine
+#: here cannot be put in front of the checker, so it is not run.
+ENGINES = {"python": "python", "typescript": "typescript"}
+
+
+def with_program(
+    document: Mapping[str, Any],
+    language: str,
+    code: str,
+    *,
+    description: str | None = None,
+    runs_for_at_most_ms: int | None = None,
+) -> dict[str, Any]:
+    """The document a `run-code` snippet makes: a nondeterministic
+    `programs:` entry under `run-code-<first 12 hex of the code's sha256>`,
+    its ceiling the run's own. The body is recorded, never opened, by PACT,
+    so the snippet's words are not part of what is checked.
+
+    Raises `Uncheckable` for a language PACT has no engine for.
+    """
+    engine = ENGINES.get(language)
+    if engine is None:
+        raise Uncheckable(f"programs here run as {language!r}, which PACT has no engine for")
+    digest = hashlib.sha256(code.encode()).hexdigest()[:12]
+    said = (description or "").strip() or "A program the agent wrote during the run."
+    fuel: dict[str, Any] = {}
+    if runs_for_at_most_ms is not None:
+        fuel["runs-for-at-most"] = f"{runs_for_at_most_ms}ms"
+    fuel["when-it-runs-out"] = "stop-and-say-so"
+    proposed = copy.deepcopy(dict(document))
+    programs = dict(proposed.get("programs") or {})
+    programs[_free_key(programs, f"run-code-{digest}")] = {
+        "description": literal(said, document),
+        "engine": engine,
+        "determinism": "nondeterministic",
+        "fuel": fuel,
+    }
+    proposed["programs"] = programs
+    return proposed

adapters/python/tests/test_nothing_public_is_named_by_nothing.py

@@ -94,9 +94,19 @@
         "why a `may-start:` start is refused (`starts-at-most:`, `nests-at-most:`), "
         "for a runtime that brings agents in; the harness starts none"
     ),
-    "delegation.beyond_its_starter": (
-        "why a narrowed agent naming what its starter lacks is refused, for a "
-        "runtime that builds narrowed agents; the harness builds none"
+    # Law 8 at instantiation: the documents a run's own definitions are
+    # checked as. The reference harness instantiates none (it starts no
+    # helper, loads no skill a run wrote and runs a snippet in a room without
+    # a check); a runtime that does (Bud Meta Harness) builds these documents
+    # and holds them to `check_document`, so both check the same document.
+    "checking.with_helper": (
+        "the document a `narrowed-new` helper is checked as, for a runtime that starts one; the harness starts none"
+    ),
+    "checking.with_skill": (
+        "the document a skill a run wrote is checked as, for a runtime that loads one; the harness loads none"
+    ),
+    "checking.with_program": (
+        "the document a `run-code` snippet is checked as, for a runtime that checks one; the harness checks none"
     ),
     # The question a run-level wait puts, by its reason. The reference harness
     # asks through its own `Gate` (`asking.for_call`) and never needs the name;

adapters/python/tests/test_what_a_run_instantiates_passes_the_same_checker.py

@@ -0,0 +1,89 @@
+"""Law 8 at the moment of instantiation (97 §4, law 8): a `narrowed-new`
+helper, a skill a run wrote and a `run-code` snippet are each put in front of
+the checker the author's tree is held to, as the document they would make,
+before they can be asked."""
+
+from __future__ import annotations
+
+import sys
+from pathlib import Path
+
+import pytest
+
+sys.path.insert(0, str(Path(__file__).resolve().parents[1] / "src"))
+sys.path.insert(0, str(Path(__file__).resolve().parent))
+
+from pact_adapters.checking import (  # noqa: E402
+    NotNarrower,
+    Uncheckable,
+    check_document,
+    literal,
+    with_helper,
+    with_program,
+    with_skill,
+)
+from trees import shown  # noqa: E402
+
+REPO = Path(__file__).resolve().parents[3]
+PHASES = REPO / "examples" / "kernel" / "phases"
+
+
+def test_a_helper_described_on_the_spot_is_its_starter_told_something_else() -> None:
+    doc = shown(PHASES)
+    out = with_helper(doc, "builder", "Check the {{ order }} part.", description="Checks one part")
+    starter = {k: v for k, v in doc["agents"]["builder"].items() if k != "name"}
+    assert out["agents"]["builder-helper"] == {
+        **starter,
+        "description": "Checks one part",
+        "instructions": "Check the \\{{ order }} part.",
+    }
+    assert check_document(out) == []
+    assert "builder-helper" not in doc["agents"], "the starter's document is not changed"
+
+
+def test_a_helper_may_be_narrower_than_its_starter_and_never_wider() -> None:
+    doc = shown(PHASES)
+    has = list(doc["agents"]["builder"].get("uses") or [])
+    narrower = with_helper(doc, "builder", "Do one step.", uses=has[:1])
+    assert narrower["agents"]["builder-helper"]["uses"] == has[:1]
+    assert check_document(narrower) == []
+    with pytest.raises(NotNarrower, match="a narrowed agent may use only what 'builder' uses"):
+        with_helper(doc, "builder", "Pay out.", uses=[*has, "payments"])
+
+
+def test_a_second_helper_takes_the_next_free_key() -> None:
+    doc = shown(PHASES)
+    twice = with_helper(with_helper(doc, "builder", "One."), "builder", "Two.")
+    assert twice["agents"]["builder-helper-2"]["instructions"] == "Two."
+
+
+def test_a_skill_a_run_wrote_is_checked_and_one_that_says_nothing_is_refused() -> None:
+    doc = shown(PHASES)
+    out = with_skill(doc, "builder", "refund-note", "Writes a refund note.", "Two lines.", use_when="a refund is decided")
+    assert out["skills"]["refund-note"] == {
+        "name": "refund-note", "description": "Writes a refund note.", "use-when": "a refund is decided", "content": "Two lines.",
+    }
+    assert check_document(out) == []
+    refused = check_document(with_skill(doc, "builder", "blank", " ", "x"))
+    assert any("description" in line for line in refused), refused
+
+
+def test_a_snippet_is_a_program_with_the_runs_own_ceiling() -> None:
+    doc = shown(PHASES)
+    out = with_program(doc, "python", "print(1)", description="Adds the totals.", runs_for_at_most_ms=20_000)
+    assert out["programs"]["run-code-d287bb7f9d15"] == {
+        "description": "Adds the totals.", "engine": "python", "determinism": "nondeterministic",
+        "fuel": {"runs-for-at-most": "20000ms", "when-it-runs-out": "stop-and-say-so"},
+    }
+    assert check_document(out) == []
+    with pytest.raises(Uncheckable, match="no engine"):
+        with_program(doc, "ruby", "p 1")
+
+
+def test_words_a_model_wrote_are_read_literally_in_either_template_language() -> None:
+    assert literal("a {{ b }} and \\{{ c }}", {}) == "a \\{{ b }} and \\{{ c }}"
+    jinja = {"template-language": "jinja"}
+    assert literal("plain words", jinja) == "plain words"
+    assert literal("x {{ y }} {% endraw %} z", jinja) == (
+        "{% raw %}x {{ y }} {% endraw %}{{ '{% endraw %}' }}{% raw %} z{% endraw %}"
+    )

docs/90-REVIEW.md

@@ -81,7 +81,7 @@ them and changes nothing.
 |---|---|
 | Schema | **43 groups, 262 field entries, 207 distinct field names** (core 123, expert 69, both 15), 40 closed enums, 27 cross-reference constraints, **0 fields missing `tier:` or `surface:`** |
 | Rust | 5 crates, **1679 tests**, `unsafe_code = forbid`, clippy-deny, edition 2024 |
-| Python | **47 modules** (`find adapters/python/src -name "*.py" \| wc -l`), **3345 tests**, **nine transports** — seven model-bound (`anthropic`, `autogen`, `langchain`, `langgraph`, `ollama`, `openai_agents`, `pydantic_ai`), one bound to a remote *agent* (`a2a`), one deterministic mock; `_metering.py`, `_summarise.py` and `_tool_choice.py` are shared code the transports import, which is what the `_` says — offline by default |
+| Python | **47 modules** (`find adapters/python/src -name "*.py" \| wc -l`), **3353 tests**, **nine transports** — seven model-bound (`anthropic`, `autogen`, `langchain`, `langgraph`, `ollama`, `openai_agents`, `pydantic_ai`), one bound to a remote *agent* (`a2a`), one deterministic mock; `_metering.py`, `_summarise.py` and `_tool_choice.py` are shared code the transports import, which is what the `_` says — offline by default |
 | TypeScript | 5 modules, 2,305 lines, a second port of **the stepping, the ceilings and the stage path** (`harness.ts:15-21`: *"AC-5.3's bar is the stage path"*) — **not** of the loop entire: no interceptor chain, no durable suspension record, no ledger (`notDoneHere`; a park returns `halted: "suspended"` and writes nothing down). This row is load-bearing for the Phase 3 pricing below (E4) |
 | CLI | **6 verbs**: `check`, `show`, `waits`, `discover`, `card`, `help` |
 | Worked example | 42 files, 1128 lines, **132 distinct authored keys**, `pact check` → OK (498 settings) |

site-docs/index.md

@@ -47,7 +47,7 @@ so plainly rather than leaving it to be discovered.
 
 | | |
 |---|---|
-| Tests | **5,026** — 1679 Rust, 3347 adapter |
+| Tests | **5,034** — 1679 Rust, 3355 adapter |
 | Schema kinds | **69** |
 | Framework targets | **7**, over 2 runtimes |
 | Eve capabilities accounted for | **101 of 101** |

site-docs/status/verified.md

@@ -13,8 +13,8 @@ from an earlier document.
 | Claim | Value | How to check |
 |---|---|---|
 | Rust tests | **1679** | `cargo test --workspace` |
-| Adapter tests | **3345** | `cd adapters/python && uv run pytest tests/ -q` |
-| Total | **5,026** | both of the above |
+| Adapter tests | **3353** | `cd adapters/python && uv run pytest tests/ -q` |
+| Total | **5,034** | both of the above |
 | TypeScript type-checks | clean | `cd adapters/typescript && npx tsc --noEmit` |
 | Lints | clean | `cargo clippy --all-targets` |
 | Worked example loads | 498 settings | `cargo run -p pact-cli -- check examples/refund-desk` |