ADR-0016 — Execution evidence and result origin

Status: proposed
Date: 2026-08-31
Owners: ZeroProofML maintainers
Supersedes / superseded by: none

Context

An exact semantic profile, the source of a payload, and the floating runtime that computed a payload are different claims. The former result schema carried an optional floating profile identifier without its descriptor digest and did not state whether a finite value was asserted, observed, computed, or migrated. That allowed a caller-supplied label to look like execution evidence.

Decision

Schema-v2 scalar results and tensor snapshots carry a stable ResultOrigin: ASSERTED_INPUT, EXTERNAL_OBSERVATION, EXACT_COMPUTATION, FLOATING_COMPUTATION, DESERIALIZED_LEGACY, or UNKNOWN_UNQUALIFIED.

ExecutionEvidence is immutable and contains its schema version, a registered floating-profile ID, the registry-bound profile SHA-256, a qualification state, and an optional runtime/provider-contract SHA-256. Backend, dtype, and device/provider are resolved from the registered profile rather than repeated as independently editable fields.

The invariants are:

  • floating-computation origin requires validated execution evidence;
  • only floating-computation results may carry that evidence;
  • asserted and externally observed values do not invent floating evidence;
  • exact identity (profile_id) stays separate from floating evidence;
  • a result with no payload carries no payload-execution evidence; semantic dispatch is represented by exact or unqualified origin, not a backend label;
  • computed factories bind the observed carrier to the registered profile; and
  • schema-v1 migration is explicit and produces DESERIALIZED_LEGACY without synthesizing a historical profile hash.

The result object does not add a second “semantic dispatch runtime” identity. Load-bearing bundle/checkpoint semantics remain in SemanticIdentity; result execution evidence describes payload production only.

Consequences

The semantic-result schema major is 2. Arithmetic, decoding, lifting, and ONNX runtime reconstruction must use computed factories or explicit validated construction. Bare profile strings are compatibility projections only. Custom profiles require an explicit immutable registry and remain unqualified until a separate qualification process says otherwise. Compact custom evidence is loaded only when the caller supplies the same immutable registry; the default loader rejects it. Arbitrary callable composition cannot select the internal qualified execution context.

Threat model

This contract detects malformed serialized evidence, identifier collisions, and supported-object mutation at trust boundaries. It is validated provenance and artifact integrity, not protection from an attacker who can run arbitrary Python in the process or bypass constructors with object-memory tricks.

Alternatives considered

Making a profile mandatory for every finite value would invent execution for exact assertions. Keeping a bare optional ID would preserve the collision and label-laundering defects. Treating a no-core result as if a numeric payload had been produced would overload execution evidence.

Verification and rollout

The adversarial semantic tests cover constructor invariants, registry collisions, backend mismatch, known-plus-legacy composition, schema-v1 migration, and canonical schema-v2 round trips. Maintainer approval is required before changing this ADR from proposed to accepted.