Reproducibility claim: deterministic re-execution as positive evidence for software-only producers

[chernistry]

Spec section affected

Claims model (spec/trace-v0.2.md) — a new optional claim member plus its interaction with appraisal. Normative, non-breaking.

Problem

Per the ruling in #231: software-only is currently defined by what it lacks, and there is no room in the claims model for deterministic re-execution as evidence. This issue proposes the primitive's shape, answering the four questions asked there from a working producer. It deliberately does not define any producer's journal layout — that is the annex, after this.

Proposed change

1. What is the claim, exactly?

A reproducibility claim states: re-executing a named deterministic function of the run — the producer's coordination logic, not the workload's side effects — over a pinned input closure yields a transcript whose canonical digest equals the claimed value. Three parts, all explicit in the record:

• the code identity re-executed: a resolvable artifact digest (for a producer that ships publicly, the same digest build_provenance already carries);
• the input closure: the complete content-addressed set of everything that function reads — initial configuration and every recorded external interaction, model calls included;
• the claimed transcript digest, over RFC 8785 canonical bytes — the canonicalization spec: parent_record_hash's preimage is stated only in a document that binds nothing #245 just ruled for record hashing, so a verifier carries exactly one.

A claim whose closure omits anything that can change the transcript is malformed. That is the definition of the claim, not a quality bar on it.

2. What must a verifier hold to re-run?

Three things, none supplied by the producer's environment: the implementation at the pinned digest (a public artifact), the input-closure blobs (each {id, digest, resolver}-addressable — the shape references already uses), and the claim itself. The rule follows from your framing: if re-execution requires any state only the producer's environment can supply, the claim must not be called reproduction — it is an assertion about that environment and belongs elsewhere. This is also why model interactions are inputs in the closure rather than something a verifier re-invokes: a model call is not deterministic, so the boundary of the deterministic function is drawn around it, and the recorded interaction is pinned by digest like any other input.

3. What is the honest failure mode?

Three statuses, never conflated:

• reproduced — re-run completed, digests equal;
• diverged — re-run completed, digests differ; the result records the verifier's observed digest, because divergence localizes nothing by itself (producer tampering, verifier drift, and an under-pinned closure all look identical until a third party can compare transcripts);
• not-attempted — any closure blob unresolvable, code identity unavailable, or the re-run not run to completion; carries the reason.

not-attempted must not be reportable as reproduced, and equally must not be reported as diverged: absent is not pass, and absent is not failure. Same discipline as TR-APR.

4. Where does it sit relative to appraisal?

The claim is producer-side. The re-execution result is an appraisal — made by a party who verified by re-running, with that party as the verifier. Proposal: an appraisal method discriminator (e.g. method: "re-execution") with the tri-state outcome scoped under it, leaving the existing appraisal.status enum untouched (aware that #190 holds that enum closed). If the editors prefer the outcome folded into status instead, the requirement is the tri-state; the placement is yours.

Explicitly out of scope: runtime.measurement stays as it is (its software-only scope is #240's question), and nothing here names a journal format.

Backward compatibility

• Non-breaking (new optional field, informative addition)
• Breaking (removes or changes required field, changes wire format, changes algorithm set)

Motivation

The answers above are lifted from a producer rather than designed on paper: our orchestrator keeps the coordination loop deterministic, records every model interaction as a content-addressed input, and signs the run journal; re-executing over the recorded closure reproduces the transcript digest. The part that does not re-execute — the model calls — is exactly what forced the input-closure discipline in (1) and (2). The vendor mapping (journal layout, how a closure is stored and resolved) is held back for the annex once this primitive has a shape.

Related issues or PRs

#231 (parent ruling and sequencing), #245 (canonicalization precedent), #240 (runtime.measurement scope — untouched here), #190 (appraisal enum — left closed).

[lywinged]

@chernistry The four answers land, and they answer what was asked rather than what would have been convenient. The boundary drawn around model calls, recorded interactions pinned by digest inside the closure rather than something a verifier re-invokes, is the piece that makes the claim decidable, and the verifier-holdings rule, nothing supplied by the producer's environment or it is not reproduction, is the same boundary stated from the other side. The tri-state does the right work: not-attempted reportable as neither pass nor failure is the discipline you point at in TR-APR, and the same line the gap-disclosure outcomes proposed in #260 draw for a different claim, so three places now hold the same line, which is worth more than any single member. And the method discriminator keeps #190's enum closed, which was the wall to respect.

One question worth settling while the shape is still soft. diverged bundles three causes you name as indistinguishable: producer tampering, verifier drift, an under-pinned closure. The result already records the verifier's observed digest. Would it also carry the verifier's implementation digest and a digest of the closure manifest as resolved? That gives the third-party comparison you point to a starting point, at the cost of two fields, and without them every diverged ends in a conversation rather than a comparison.

On process, stating it rather than assuming it. The rule as written on #245 is that normative text from an individual sits under the organizational-sponsor rule, and the #245 exemption was for fixing a defect in existing coverage, not adding an obligation. This adds a member rather than fixing a hole, so by my reading it sits on that gate, optional or not. Whether it proceeds as spec text, waits on a sponsor, or is carried is not a ruling I will make alone. Flagging it for @imran-siddique, together with the §4.4 annex-scope question from #231, which is still open and which the annex behind this issue is waiting on.

[chernistry]

Both, and they are not doing the same job — which is the reason to carry both rather than pick one.

Digest of the closure manifest as resolved is the one that actually discriminates, and it discriminates from a single result. If what the verifier resolved differs from what the producer declared, the closure did not pin what it claimed: under-pinned, decidable from the record alone, no second verifier required. If it matches and the output still diverges, under-pinning is excluded — which is the useful half, because it is the cause that is cheapest to fix and most likely.

The verifier's implementation digest discriminates nothing on its own: it is the verifier naming its own build, self-asserted, and a tampering producer would be equally happy to see it recorded. It earns its place only as a correlation key across results — two verifiers at different digests disagreeing on a closure whose resolved manifest matched is verifier drift, and that reading is unavailable without the field. Worth stating in the spec that it carries no weight singly, so nobody reads it as attestation.

So the enum stays closed (#190's wall) and the discrimination lives in the comparison, not in new outcomes:

resolved manifest	verifier impl	reading
≠ declared	any	under-pinned closure
= declared	differs, and results disagree	verifier drift
= declared	same, and results disagree	no benign explanation found

The third row is the only one that accuses, and it accuses on absence. I would have the spec say exactly that — "no reproducing verifier found a benign explanation" — rather than naming tampering, because the record cannot distinguish a tampering producer from a cause nobody has thought of yet.