The mechanism
Three pieces, and the third is a set intersection.- Every value declares a
surface— the set of images, and config keys, whose bytes can affect the claim. It is part of the value, declared once, beside the claim itself. - Every piece of evidence records the exact digests of that surface as they were when it ran. Not the release, not the date — the digests.
- At the next entry, the gate computes
changed_digests ∩ surface:
Digest equality is the right to reuse. No prose justification, no reviewer judgment, nothing anyone can argue with: evidence binds to digests, and an unchanged digest is the same bytes, so the claim is still literally true of them. A reuse that needs an argument is not a reuse — it is a new claim.
What re-proves, per dimension
That last row is the one that makes the model affordable. The human judgments are attached to a pull request, and a pull request does not change.
Two guards
Surfaces are declared conservatively. A value about a seam — an integration, a protocol boundary, anything whose failure mode is interaction — claims more images than a localized one. Over-claiming costs an occasional unnecessary re-prove. Under-claiming silently ships an unproven claim wearing a green tick, so the asymmetry decides the default. Statistical rows keep watching regardless. Soak evidence is a rate over a live window, so it goes on measuring in production no matter what the diff said. That is the net under the surface declarations: an interaction nobody declared shows up as the rate moving, not as silence.Worked example
An update ships a gateway auth change.- The diff touches the gateway image only. Transcription image digests are byte-identical to the previous entry.
- The human witness on “transcription quality is acceptable” declares a surface of the transcription images. The intersection is empty.
- The row inherits:
inherited from seq 6 — surface digests unchanged. Nobody is asked to listen to audio because an auth header changed.
- That digest is in the transcription value’s surface. The intersection is non-empty.
- The row drops to
unprovenand a witness session is queued. The diff summoned the human — not a calendar, not a release manager, and not the human’s own memory of when they last checked.
State: RULED, NOT BUILT. The
surface field on a value and the intersection check at the gate are decided and unimplemented. Evidence today attaches to the entry that produced it and is not inherited; the digests it would intersect against are already recorded in the candidate map. See the evidence model for the full per-element state.