Project Candidate Interface Delta v1
September 10, 2026 · View on GitHub
Status: implemented bounded profile; HOSTED GREEN under the v0.4.0 release baseline. Historical local, authoring-time, ignored, or separately provisioned observations below retain their narrower scope; public promotion and broader product completion remain separately gated.
Audience: compiler contributors and agents reviewing immutable Project candidates.
This additive report compares source-backed static protocol conformance across an entire candidate's original base and final admitted Project revision. It exposes changed required signatures, implementation bindings, and the functions behind those bindings without requiring an agent to guess which individual stable IDs to query. It leaves the selected Semantic Delta v1 and image/runtime graph schemas unchanged.
API and exact binding
pub fn interface_delta(&self, expected_candidate: &str)
-> Result<String, Vec<Diagnostic>>;
pub fn verify_interface_delta(&self, expected_candidate: &str, bytes: &[u8])
-> Result<String, Vec<Diagnostic>>;
The report schema is semaprax.project-candidate-interface-delta.v1; verification
uses semaprax.project-candidate-interface-delta-verification.v1. Reports bind
the exact candidate digest, both Project and Workspace revisions, and complete
ordered source bindings on both sides. Each source binding contains its path,
source revision, and source digest. Equal display names in different modules
never substitute for persistent declaration identity or source provenance.
Verification independently replays the complete candidate history and canonical candidate evidence, regenerates this report, and compares all submitted bytes. Recomputing public fact digests around a modified payload cannot authenticate that payload. Submitted JSON is never deserialized as trusted HIR or treated as permission to publish. A stale selector, different candidate, changed report, or noncanonical encoding fails closed.
Whole-candidate comparison
protocols contains affected protocol identities and their comparison.
implementations contains affected implementation identities, their
comparison, and the union of before/after required member identities. Every
member of an affected implementation remains present, including siblings whose
facts did not change. This distinguishes an unchanged requirement from a
missing implementation member.
A comparison contains its change classification, exact and separately
provenance-insensitive equality flags, before/after fact digests, and complete
base and candidate values. Absence is explicit null. Classification is
added, removed, modified, provenance_only, or unchanged; it is compiler
projection comparison, not proof of equivalent runtime behavior.
Provenance-insensitive comparison recursively removes only provenance,
span, source_span, source_revision, source_digest, expression_id, and
exact_digest. Declaration/body digests, parameter names, resolved type IDs,
ownership modes, requirements, contracts, and plan projection digests remain.
Dependency fact digests use this normalization so unchanged helper source
does not appear semantically changed solely because its source provenance moved.
Member facts bind the actual required signature, selected function identity,
source and typed function facts, and static reachable callable dependencies.
Consequently a function body, display name, permitted postcondition, or reachable
helper edit can affect the report even when the method-to-function mapping is
unchanged. Dependencies retain stable IDs, available fact digests, source
provenance, an explicit availability reason, and the evidence owner/class; static
reachability does not establish path feasibility or execution coverage.
fact_availability distinguishes retained_source_callable from
external_or_unretained_callable; unavailable body facts and provenance are
explicit null. Function facts retain sorted direct_calls identities, so equal
reachable sets cannot conceal different direct-call bindings.
The compact inventory gives before/after protocol and implementation counts
and counts of unchanged protocols and implementations. Entire unchanged
implementations are omitted from the detailed inventory, while complete source
bindings remain available. Ordinary targets with no static conformance do not
acquire invented protocol nodes or runtime dispatch edges.
Admission and authority
Facts derive only from canonical sources of already admitted immutable Project
revisions. implement_interface still requires a complete local member table
with distinct compatible local functions. This report does not add cross-module
implementation bindings, dynamic dispatch, runtime witness tables, interface
editing syntax, or new candidate operations. Independent source modules can
carry independent local conformance, and callable dependency provenance may
cross module boundaries through ordinary authenticated imports.
A function display rename preserves persistent bindings. Permitted body or postcondition changes remain subject to ordinary source verification and full candidate admission. Incompatible signatures or stronger preconditions reject before a new candidate/report is admitted; the old candidate and original source remain unchanged. This report does not make unsupported signature transformations available or weaken their ownership rules.
Reports and verification do not execute tests, interpreters, or emitted targets. They do not prove behavioral contracts, runtime equivalence, dynamic reachability, or backend-specific dispatch. They grant no filesystem, source publication, Git, cache, or commit authority. Separate host-selected publication mechanisms retain their existing independent checks.
Bounds and evidence
V5 exposes candidate/interface-delta only when the host enables candidate
preparation. Required parameters are image_revision and candidate_revision;
optional offset is 0–8 MiB and chunk_bytes is 1,024–65,536 (default 16,384).
Offsets must lie on a UTF-8 boundary in the report. The
semaprax.image-interface-delta-chunk.v1 envelope binds both request revisions,
the report schema, offset, total bytes, chunk, nullable next offset and
source_authority:false. Candidate immutability fixes all chunk contents.
The session authenticates live source before and after preparation; this route
does not mutate candidates. The
parallel retained-read extension shares
the same pure handler with only the selected candidate. V1–v4
method sets remain unchanged. Transport/discovery evidence is authored in
tests/image_transport_v5/workspace.rs and the v5 discovery module.
Reports are deterministic compact JSON with recursively lexical object keys, canonical array order, and one terminal LF. The report is bounded to 8 MiB; inventories to 65,536 items; collected direct-call occurrences and dependency closure walks to 1,048,576 each; HIR expression visits to 1,048,576 and depth to 256; retained/cloned fact-work accounting to 32 MiB. Existing source, retained-HIR, Project, and candidate bounds remain in force. Overflow rejects instead of silently dropping members. These are structural/output bounds, not peak heap or latency guarantees.
Fact, source-fragment, and report digests use the domains
semaprax.candidate-interface-delta.fact.v1,
semaprax.candidate-interface-delta.source.v1, and
semaprax.candidate-interface-delta.report.v1, respectively, each followed by
NUL. The preimage is that domain, the little-endian u64 byte length, and exact
bytes. Canonical JSON facts/reports include their final LF; source fragments
use their exact authenticated span bytes. Cleanup and loan facts retain
separate exact and provenance-normalized projection digests.
SPX-G310 rejects inconsistent source-backed inventories, SPX-G311 rejects
capacity overflow, and SPX-G312 rejects exact replay mismatch. Existing stale
candidate, source, conformance, and Project diagnostics propagate unchanged.
tests/project_candidate/interface_delta.rs authors addition with complete
member tables, independent modules with identical display names, exact source
provenance, changed bound-function facts with unchanged sibling retention,
imported-helper edits affecting a binding whose own source is unchanged,
normal source rejection of incompatible requirements, replay tampering and
stale selection, deterministic output, and source preservation.
The implemented release regression corpus is HOSTED GREEN. Broader support and the broader graph-operational programme remain outstanding.