spec: bind successor observations without treating transcript.after as proof of closure

[altrudev]

Problem

The PIC/TRACE bridge currently binds the signed authorization to the declaration and exact executed tool call, and when a transcript is required it binds transcript.before.tool_call to that execution.

transcript.after, however, is only required to be a JSON object.

That establishes presence, not identity or evidentiary sufficiency. A verifier therefore cannot distinguish:

1. the actual successor observation produced for this execution,
2. a substituted or replayed object,
3. a self-asserted outcome supplied by the executor,
4. a valid observation that nevertheless is insufficient to establish the requested transition.

This boundary is already stated in docs/integration/pic-trace-bridge-v1.md: the bridge binds authorization to the call and execution evidence "without claiming that TRACE proves the real-world outcome of the call."

#332 confirmed that no existing normative mechanism closes this layer and identified transcript.after as the narrow surface worth addressing.

This issue proposes only that narrow change. It does not propose importing STBP wholesale, turning TRACE into an application-state store, or making real-world outcome claims from execution evidence alone.

Related: #332, #279.

Requirements

A successor-observation extension to the PIC/TRACE bridge should satisfy all of the following.

1. Bind the exact successor observation

When a profile elects to make a successor-state claim, the verifier MUST be able to establish the exact observation bytes to which the claim refers.

The identity relation should use the bridge's existing RFC 8785 / SHA-256 convention rather than host-language object equality.

A candidate minimal field is:

{
  "after": {
    "observation": { "...": "..." },
    "observation_digest": "sha256:..."
  }
}

The precise schema shape is intentionally open. A detached successor-observation artifact bound by digest may fit the existing bridge architecture better than embedding the complete object.

The requirement is the invariant, not that specific representation:

the bridge MUST bind the exact successor observation used by the verifier.

2. Keep observation integrity separate from observation sufficiency

Matching a digest proves identity of the observation. It does not prove that the observation is authoritative enough to establish the requested transition.

The verifier therefore MUST NOT equate:

successor observation is integrity-bound

with:

authorized transition is established

A successor observation may be correctly bound and still be insufficient because its source is untrusted, stale, incomplete, or otherwise outside the verifier's policy.

3. Make the not-established result first-class

This is an instance of the discipline tracked in #279.

Where a verifier evaluates a requested transition from predecessor/execution/successor evidence, the outcome needs three distinguishable states:

• established — sufficient trusted evidence establishes the requested transition;
• contradicted — sufficient trusted evidence establishes that the requested transition did not occur;
• not established — the available evidence is insufficient to justify either conclusion.

Names should follow the surface rather than introduce a repository-wide enum, consistent with #279.

Critically, absence or insufficiency of successor evidence MUST NOT fall through to a positive result.

4. Do not let self-certification silently become closure

A bound successor observation may be produced by the same principal that executed the action.

That is not universally invalid: some transitions can be established by deterministic local evidence. But for a transition whose verifier policy requires an independent successor observer, executor-supplied evidence is insufficient.

The profile therefore needs a way for the verifier to evaluate the observation source against policy.

This does not require a universal rule that executor and observer differ.

The rule is narrower:

when the applicable verification policy requires independent observation, evidence from the executing principal alone MUST NOT establish closure.

The resulting outcome is the surface's not-established state unless trusted contradictory evidence exists.

5. State what the verifier may conclude, and what it may not

The profile text should define the assurance boundary explicitly.

A successful successor-observation binding permits the verifier to conclude only that:

1. this is the exact observation associated with the bridge evaluation, and
2. its source/freshness/trust properties satisfy the configured verification policy.

A transition-level positive conclusion additionally requires a defined predicate over the relevant predecessor, action/execution, and successor evidence.

The bridge MUST NOT imply that a bound after object, by itself, proves a real-world outcome.

Candidate verification model

Conceptually:

signed authorization
       |
       | binds exact authorized call
       v
exact execution
       |
       v
successor observation
       |
       +-- exact observation bound?
       +-- observation source trusted?
       +-- freshness/policy satisfied?
       +-- independence satisfied when required?
       |
       v
transition predicate
       |
       +-- true  -> established
       +-- false -> contradicted
       +-- insufficient evidence -> not established

The transition predicate itself may be profile- or application-defined. TRACE does not need to understand arbitrary application state in order to enforce the evidence discipline around that predicate.

Why a digest alone is insufficient

Consider a Git-backed transition.

An authorized agent holds the push credential, performs the push, then supplies an after object saying that the repository is now at the desired commit.

Even if TRACE binds that after object perfectly, the evidence is still self-certified if the verifier has no trusted observation independent of the actor where independence is required.

The integrity problem and the closure problem are therefore different:

binding(after) solves substitution / identity
trust-policy(after) determines whether it is usable evidence
predicate(before, action, after) determines the transition result

Collapsing those steps would make a cryptographically intact claim indistinguishable from independently established closure.

Non-goals

This proposal does not require:

• TRACE to store application state;
• a universal predecessor/successor schema;
• a universal transition predicate language;
• independent observation for every transition;
• STBP as a TRACE dependency;
• a new repository-wide tri-state enum;
• replay/one-shot authorization semantics in this change.

Replay/uniqueness remains a separate concern noted in #332.

Suggested first implementation boundary

The smallest evaluable change appears to be:

1. define a canonical binding for the successor observation associated with transcript.after;
2. define the observer/trust metadata needed to evaluate that observation under verifier policy, or bind a detached artifact that carries it;
3. define the profile's positive / contradictory / not-established conclusion rules;
4. add adversarial fixtures for:
   • substituted after;
   • missing successor evidence;
   • malformed/non-canonical successor evidence;
   • stale successor observation;
   • self-observation where independence is required;
   • self-observation where independence is not required;
   • trusted successor evidence satisfying the predicate;
   • trusted successor evidence contradicting the predicate.

I would prefer to settle those semantics before proposing a schema or implementation diff, because the security boundary is in what a verifier is allowed to conclude, not merely in adding another digest field.

[github-actions]

🔴 Contributor Check: HIGH

Check	Result
Profile	HIGH
Credential	LOW
Overall	HIGH

Automated check by AgenTrust Contributor Check.

[altrudev]

I made the smallest implementation I could without choosing the wire format prematurely: #340. The prototype treats the expected digest as an external binding input, but binds the complete successor envelope (observation + observer + observed_at), then separately evaluates trust, freshness, independence policy, and the application predicate. It includes adversarial cases for observation substitution, observer relabelling, retiming, stale/untrusted evidence, self-observation with and without required independence, and the not-established path. It is ready for review; CI/CodeQL are currently running.

[imran-siddique]

Accepted, all five requirements. This is the narrow thing I asked for on #332 and it arrived narrower than I described it.

The sponsor rule does not apply here, which is the first thing to settle. Normative spec text in this repository needs an organisational sponsor. docs/integration/pic-trace-bridge-v1.md opens "This informative profile", and transcript.after lives in it and in intent_bridge, so nothing here is normative spec text. You can carry this yourself and I am not holding it for a sponsor.

Two places you improved on what I wrote.

My counterexample said the model breaks where the successor is observed by the party that executed. You turned it into a policy condition rather than a universal rule, and that is correct: some transitions are establishable by deterministic local evidence, and a blanket requirement that executor and observer differ would refuse those for no reason. The narrower rule is the right one.

Requirement 1 asks for the digest over the observation. #340 puts observer identity and observation timestamp inside the envelope the digest covers, which closes an attack the issue text does not name: a genuine observation relabelled to a different observer, or retimed after the fact. That is the stronger construction and it belongs in the profile text rather than only in the prototype.

I ran #340 rather than reading it. 21 tests pass, mypy --strict is clean, and the matrix behaves:

established      exact envelope, trusted observer, fresh, predicate affirms
REFUSED          observer relabelled to the executor
REFUSED          timestamp retimed by one second
REFUSED          observation content altered
not-established  absent successor
not-established  independence required, observer IS the executor
not-established  stale beyond max_age
not-established  predicate cannot decide
not-established  observer not in trusted set
contradicted     predicate contradicts

Three envelope mutations refuse outright rather than returning a status, five distinct insufficiency causes all land on not-established, and only an affirmative contradiction reaches contradicted. Absence never becomes a positive, which is the property #279 exists for. The set fails in both directions, so it discriminates.

On requirement 3. established / contradicted / not-established as a surface-local name is right, and do not widen it. Cite this surface in #279 as the second one reaching that shape independently: it strengthens that case more than a third restatement of the principle would.

What I would like next. Turn #340 into a real PR: the profile text for requirements 2, 4 and 5 in pic-trace-bridge-v1.md, and the binding in intent_bridge beside the transcript.before.tool_call comparison, which now compares canonical bytes for the same reason. Keep the prototype's envelope shape. I would like it open by 19 September; say so here if that is tight and it is not a problem.

One thing to decide while you write it: whether an absent after when a profile has elected to make a successor claim is not-established or a refusal. The prototype returns not-established, and I think that is right, because the bridge cannot tell a profile that elected the claim from one that did not. Make the profile text say which.

[imran-siddique]

Completed by #340, now merged. The signed authorization binds the complete successor envelope, and the separate evaluator applies trust, freshness, independence policy, and the transition predicate while preserving established, contradicted, and not-established outcomes.

The profile now states the absence boundary explicitly: a missing required transcript is refused by the bridge; absent evidence at the separate evaluator remains not-established. Local bridge/successor coverage passed all 71 tests, and removing the exact-envelope field guard made its regression test fail. Closing this implementation tracker as completed. The broader coordination and corpus work in #279 and #206 remain open.