Semantic Models and Summaries

Bifrost inspects available source code directly. Real programs also depend on standard libraries, frameworks, generated APIs, and binary artifacts whose bodies may be unavailable. Semantic-model packs add structured declarations and procedure behavior at that boundary.

Model evidence retains its origin. Source-derived proof comes from analysis of the source itself.

Model layers

Layer	Purpose	Typical contents
Artifact identity	Say exactly which dependency the model applies to	ecosystem coordinates, version/range, digests, language and compatibility profiles
Declaration model	Name external types, fields, callables, and signatures	structured owner/member identity, kind, receiver shape, formals, returns
Procedure summary	Describe behavior across a procedure boundary	receiver/parameter/return transfers, heap locations, exceptional returns, effects
Provenance and coverage	Explain who asserted the model and what it covers	pack, model and summary IDs, origin, completeness, unresolved or conflicting rows
Activation	Bind an exact model set to one workspace analysis	selected manifests, source kinds, configuration and active-set digest

Artifact validity, applicability, declaration binding, and behavioral completeness are recorded independently.

Exact binding

A usable procedure summary must bind to a callable identity; display names are presentation data. Depending on the language, that identity can include an owner, namespace or module route, declaration kind, receiver presence, arity and formal positions, signature information, and source or dependency artifact identity.

Binding requires:

a callable identity complete enough to distinguish the intended library method from a common name such as exec;
owner and signature context sufficient to select one overload;
call binding that maps argument zero to a formal parameter before applying the summary; and
dependency-artifact identity within the model’s stated validity contract.

If the required identity is absent, ambiguous, conflicting, or only partially modeled, Bifrost preserves that boundary in the result.

Source and model precedence

Workspace source bodies are analyzed directly. An external summary can stand in for a missing body only after compatibility, declaration binding, and the requested proof/completeness policy are checked.

Source and model evidence also make different claims:

source-backed evidence can prove what the analyzed body contains;
an authored external model remains an authored claim, even when the pack declares that claim complete; and
a generated model remains tied to its producer and exact generation inputs.

Some reviewed external summaries may close a modeled call boundary under an explicit policy. That closure applies only to the modeled call boundary.

Summary identity and reuse

A reusable procedure summary is keyed by the semantic artifact, declaration locator, schema and semantics versions, context and behavior keys, origin, and the exact dependency closure it used. Recursive strongly connected components are validated and published as a unit. A partial component remains visibly incomplete in any cached form.

Domain-specific summaries extend that carrier identity with their own inputs:

taint summaries add the taint universe, propagation semantics, event matching, and entry facts;
typestate summaries add the compiled protocol, binding plan, and entry states; and
type-flow and policy-level retained results add their exact request and projection identities.

Reuse requires semantic equivalence across every part of that identity.

Catalog and activation lifecycle

Packs can come from installed, generated, pre-shipped, workspace-produced, embedded, or explicitly ephemeral sources. Catalog ingestion validates the pack before activation. The active set has its own digest, so changing one selected pack changes the analysis identity.

Generated dependency packs use the separate semantic-model object catalog. Its key includes exact inputs and producer identity. A producer change that can alter generated bytes or meaning must rotate the production-cache version; otherwise stale output could appear valid even though the generator changed.

Hosts supply or resolve an activation request for semantic packs. The ordinary analysis path loads that exact set, and the host retains activation diagnostics.

CSMI interoperability

Bifrost can import and export supported Code Semantic Model Interchange (CSMI) profiles. CSMI is the analyzer-neutral interchange specification targeted by the semantic-model roadmap. Producer-specific generation and consumer-specific interpretation sit around the neutral pack format. A schema-valid pack can still be semantically invalid, inapplicable to the current artifact, or unsupported by a consumer profile.

An interoperability test needs the exact artifact emitted by an independent producer and the analysis difference with that pack disabled and enabled. A hand-authored approximation cannot establish producer interoperability.

Current boundaries

Model coverage varies by pack. Coverage may close one procedure and leave the surrounding library catalog partial. Dynamic dispatch, reflection, callbacks, generated interfaces, native boundaries, and framework conventions remain visible boundaries after an exact call-summary binding.

Automatic dependency discovery and activation is a continuing direction. Its workflow keeps these steps independently diagnosable:

discover a dependency artifact;
acquire candidate packs;
validate and establish applicability;
activate an exact set;
bind declarations and procedure ports;
solve with the resulting evidence; and
report every boundary that remains.

Authoring and host integration details are in Semantic-Model Packs. Dataflow Engine and Evidence and Result Contract describe how model evidence affects flow results.