Let a PR beat earn CLEAN from a run the gateway signed for

README.md

@@ -85,6 +85,15 @@ was: `CLEAN` is reserved for a command whose output would have differed were the
 false, and a claim that was read or inferred opens `UNVERIFIED`, which is where your own
 reading goes. A risk appears only on a flag, with a decision beside it.
 
+A PR session can still earn `CLEAN` when the host runs a proof gateway. The walk picks a
+command, such as one test module, and predicts its exit code. `proofctl.py prove` hands
+it to the execution gateway, which runs it on the gateway's own copy of the frozen head
+inside its sandbox and signs a receipt only if the command exits as predicted. The
+store accepts `proof_kind: attested` only beside a verified receipt for that beat, and
+writes the signed command, exit code and the last lines it printed onto the card itself,
+so the walk's `PROOF` line cannot pass for the run. A flag can carry its failing run the
+same way. A wrong prediction yields no receipt and proves nothing.
+
 Beats stay that size because the store makes them. A slot over 25 words, a claim over 20,
 a fourth filled slot on a clean beat, or an eleventh quoted line is refused at write time,
 with the offending slot and its count named, as is a clean verdict on a read proof or a
@@ -147,6 +156,13 @@ static readers, but it does not check out the head, install, build, test, lint,
 scripts or interpreters, or invoke Git hooks and filters. Review comments, report
 inclusions, notes, navigation, and recorded decisions still work.
 
+A proof never changes the session's `no_exec` policy. This machine never runs the head;
+the gateway does, in a sandbox with no network or credentials, from its own quarantine of
+the frozen bundle. It happens only on a host that opted in twice: a proof configuration
+for the controller, and `proofArguments` in the gateway's own configuration. Even then
+the gateway runs the profile's fixed command with at most 16 bounded arguments after it.
+The receipt is evidence for one beat and authorizes nothing.
+
 The host execution protocol is documented in
 [`docs/host-execution-protocol.md`](docs/host-execution-protocol.md). Its
 [`execution_receipt.py`](skills/underwrite/scripts/execution_receipt.py) module checks a
@@ -282,6 +298,8 @@ implementations/<link-id>/  one linked child, nested below the source session
     output.bundle           verified output transport
     stdout                  complete captured standard output
     stderr                  complete captured standard error
+proof-evidence/<proof>/     one verified attested proof: request, both signed
+                            envelopes, and both complete streams
 ```
 
 The scripts are Python 3 stdlib, with no dependencies. `serve.py` runs the walk and

docs/host-execution-protocol.md

@@ -273,6 +273,11 @@ execution attempt to the authoritative queued action and finding beat. A retry u
 attempt and a new challenge unless it is a byte-identical replay of an already recorded
 result.
 
+An attested proof uses the same coordinates differently. `action.seq` is the proof's
+number within the source session, `action.beat` is the beat the proof may back, and
+`action.attempt` is `1`. A proof never retries under the same number: after a definite
+failure the controller reserves a new proof with a new number and challenge.
+
 ### Job
 
 `job.argv` is a nonempty array of UTF-8 strings without NUL characters. `argv[0]` is
@@ -778,6 +783,16 @@ The reference implementation supplies that supervised path only through a separa
 `gateway_attested` child. Protocol conformance alone remains insufficient, and no receipt
 authorizes a review publication or push.
 
+An attested proof is the one use a source session makes of a receipt, and it applies
+nothing. The request is the trusted profile's job with at most 16 bounded arguments
+appended and an exit code the controller predicts; a gateway accepts that shape only when
+its own configuration sets `proofArguments`. The controller verifies the receipt exactly
+as it verifies an implementation receipt, with the reserved request's job and exit code as
+the expected values, verifies the returned output bundle against the signed output tree,
+and then discards it. What it records is that one command exited as predicted on the
+frozen head and printed the signed streams. The source session stays `no_exec`, its
+audience and deliveries are untouched, and the receipt authorizes no effect.
+
 ## Limitations
 
 - Current Codex and Claude Code plugin, skill, and hook interfaces do not issue this

gateway/README.md

@@ -243,11 +243,12 @@ exits. The configuration is version 1 with exactly these fields:
 
 The embedded `profile` is the exact separately provisioned profile later given to
 `implementationctl.py`. Its key ID must match the configured key pair, and its executor ID
-must match the policy derived from this deployment. The request's complete `job`, `sandbox`,
-and `exitCode` must match it. The `docker`, `openssl`, and `git` values are explicit absolute
-host executable paths. They must be trusted regular executables owned by root or the gateway
-account and not writable by group or other. The job executable is instead an absolute path
-inside the pinned runtime image.
+must match the policy derived from this deployment. The request's complete `job`,
+`sandbox`, and `exitCode` must match it, except as **Proof deployments** below allows. The
+`docker`, `openssl`, and `git` values are explicit absolute host executable paths. They
+must be trusted regular executables owned by root or the gateway account and not writable
+by group or other. The job executable is instead an absolute path inside the pinned runtime
+image.
 
 Preprovision `storeRoot` as a gateway-owned `0700` directory. Separately, provision the
 immediate outbox parent as gateway-owned, group-owned by `consumerGid`, and exactly `0710`.
@@ -330,3 +331,43 @@ local branch. After `implementationctl.py consume` durably succeeds, the gateway
 supervisor may delete the final transport directory. The consumer cannot and must not
 delete it through the `0710` parent. Neither the adapter nor the gateway checks out the
 branch, pushes it, opens a pull request, or publishes a review.
+
+### Proof deployments
+
+A deployment may also run walk claims for source review sessions, through
+`proofctl.py`. It opts in with one more configuration field, `"proofArguments": N`, an
+integer from 1 to 16. With it, a request may differ from the profile in exactly two ways:
+its `job.argv` may append 1 to `N` arguments after the profile's own argv, each non-empty
+printable text of at most 512 UTF-8 bytes, and its `exitCode` may be any integer from 0 to
+255. The executable, environment, working directory, closed stdin and sandbox stay the
+profile's. A request equal to the profile's job is still held to the profile's exit
+code, so the same deployment keeps serving implementation children unchanged. Without
+the field, every request must equal the profile exactly, as before.
+
+The predicted exit code is what makes a run a proof. The broker already signs a receipt
+only when the target exits with the request's `exitCode`, so a mismatch ends the attempt
+as `failed` with no receipt, and the controller records that nothing was proven. Choose a
+profile whose fixed argv names what a proof may run, such as
+`["/usr/local/bin/python3", "-I", "-B", "-m", "unittest"]`. A proof runs head code in the
+sandbox by design: that is what the network denial, the seccomp filter, the single
+process, the `noexec` read-only layout, and the resource limits are for. Do not enable
+`proofArguments` on a host whose sandbox you would not trust with the head.
+
+The controller reaches the adapter through its own proof configuration, kept outside every
+repository and session:
+
+```json
+{
+  "version": 1,
+  "profile": "/etc/underwrite/proof-profile.json",
+  "publicKey": "/etc/underwrite/signing-public.pem",
+  "adapter": ["/usr/local/bin/underwrite-proof-adapter"],
+  "evidenceRoot": "/srv/underwrite-handoff/outbox"
+}
+```
+
+`proofctl.py prove` appends `--request`, `--source-bundle` and `--evidence-dir` to
+`adapter` and reads the handled JSON result. When the gateway runs as another account, as
+it should, `adapter` names a supervisor wrapper that stages the request and the session's
+`pr.bundle` where the gateway may read them and then runs the adapter. The evidence
+directory is `<evidenceRoot>/underwrite-<session id>-proof-<n>`.

gateway/adapter.py

@@ -63,6 +63,12 @@ class AdapterError(RuntimeError):
     "maxSourceBundleBytes",
     "profile",
 }
+# Opt-in: a proof deployment lets a request append at most this many arguments to the
+# profile's command and predict its own exit code. Without it, every request must be
+# the profile's job exactly, as an implementation deployment requires.
+_PROOF_FIELD = "proofArguments"
+_MAX_PROOF_ARGUMENTS = 16
+_MAX_PROOF_ARGUMENT_BYTES = 512
 _EVIDENCE_FILES = (
     "request.json",
     "capability.dsse.json",
@@ -423,9 +429,22 @@ def load_configuration(path):
         ),
         "gateway configuration",
     )
-    _exact(value, _CONFIG_FIELDS, "gateway configuration")
+    _exact(
+        value,
+        _CONFIG_FIELDS | ({_PROOF_FIELD} if _PROOF_FIELD in value else set()),
+        "gateway configuration",
+    )
     if type(value["version"]) is not int or value["version"] != 1:
         raise AdapterError("gateway configuration version must be 1")
+    if _PROOF_FIELD in value:
+        limit = value[_PROOF_FIELD]
+        if (
+            type(limit) is not int
+            or not 1 <= limit <= _MAX_PROOF_ARGUMENTS
+        ):
+            raise AdapterError(
+                f"{_PROOF_FIELD} must be an integer from 1 to {_MAX_PROOF_ARGUMENTS}"
+            )
     value["consumerGid"] = _consumer_gid(value["consumerGid"])
     try:
         value["profile"] = validate_execution_profile(value["profile"])
@@ -812,12 +831,50 @@ def publish_evidence(stored, content, destination, consumer_gid=None):
         os.close(parent)
 
 
-def _request(path, policy, profile):
+def _proof_request(request, profile, limit):
+    """A proof runs the profile's command with a bounded tail and its predicted exit.
+
+    Everything else stays the profile's: executable, environment, working directory,
+    stdin and sandbox. The broker signs only when the run exits as predicted."""
+    job = request.get("job")
+    if not isinstance(job, dict):
+        raise AdapterError("execution request job does not match the trusted profile")
+    for field in ("cwd", "environment", "executable", "stdin"):
+        if job.get(field) != profile["job"][field]:
+            raise AdapterError(
+                f"execution request job {field} does not match the trusted profile"
+            )
+    if request.get("sandbox") != profile["sandbox"]:
+        raise AdapterError("execution request sandbox does not match the trusted profile")
+    prefix = profile["job"]["argv"]
+    argv = job.get("argv")
+    if not isinstance(argv, list) or argv[: len(prefix)] != prefix:
+        raise AdapterError("proof command does not extend the trusted profile command")
+    tail = argv[len(prefix):]
+    if not 1 <= len(tail) <= limit:
+        raise AdapterError(f"proof appends 1 to {limit} arguments to the trusted command")
+    for argument in tail:
+        if (
+            not isinstance(argument, str)
+            or not argument
+            or any(ord(character) < 32 or ord(character) == 127 for character in argument)
+            or len(argument.encode("utf-8")) > _MAX_PROOF_ARGUMENT_BYTES
+        ):
+            raise AdapterError("proof argument is not bounded printable text")
+    exit_code = request.get("exitCode")
+    if type(exit_code) is not int or not 0 <= exit_code <= 255:
+        raise AdapterError("proof exit code must be an integer from 0 to 255")
+
+
+def _request(path, policy, profile, proof_arguments=None):
     request = _load_json(
         _read_regular_file(path, "execution request", _MAX_REQUEST_BYTES),
         "execution request",
     )
     ExecutionRequest(request, policy)
+    if proof_arguments is not None and request.get("job") != profile["job"]:
+        _proof_request(request, profile, proof_arguments)
+        return request
     for field in ("job", "sandbox", "exitCode"):
         if request.get(field) != profile[field]:
             raise AdapterError(
@@ -834,7 +891,9 @@ def run(config_path, request_path, source_bundle, evidence_dir):
     profile = configuration["profile"]
     if policy.executor_id != profile["executorId"]:
         raise AdapterError("gateway policy does not match the trusted profile")
-    request = _request(request_path, policy, profile)
+    request = _request(
+        request_path, policy, profile, configuration.get(_PROOF_FIELD)
+    )
     source_bundle = _inspect_regular_file(source_bundle, "source bundle")
     evidence_dir = _preflight_destination(
         evidence_dir,