Provenance & Trust

Every value in Sema carries a trust label, and that label follows the value through computation. This is the type-level mechanism behind one of Sema’s sharpest guarantees:

A prompt-injected simulate can emit text, but nothing it produces can ever run.

This page is the conceptual governance treatment of trust labels and information flow. It is not the same thing as the provenance stdlib module (a small citation-id mapping utility) — see the cross-links at the end for those.

The trust lattice

Trust labels form a three-point lattice, ordered from least to most trusted:

untrusted  <  validated  <  trusted

untrusted is the bottom. Because sources are language constructs in Sema, labeling is nearly annotation-free — the compiler knows where a value came from:

Born label	Sources
untrusted	simulate outputs, network reads, file reads, FFI returns
trusted	string literals, pure computation over trusted inputs

You rarely write a label by hand; the language derives it from provenance.

Propagation takes the meet — taint is sticky

The load-bearing rule: any value computed from mixed inputs carries the least trusted label among them. Combining a trusted literal with an untrusted model output yields an untrusted result. This is the lattice meet, and it makes taint sticky: no sequence of operations can launder a label upward. Concatenation, formatting, arithmetic, struct construction — all take the meet.

Mutation obeys the same rule. Writing a field re-labels the aggregate with the meet of its old label and the written value’s label, so mutating a trusted struct with an untrusted value lowers the whole aggregate. Mutation can only lower trust, never launder it.

Sinks require trust

Sinks are the dangerous operations — the places where a value becomes action —- and they demand a sufficient label:

• code.exec, proc.spawn (execution)
• SQL identifiers and fragments
• tool dispatch
• ported splice-in

These require trusted. Some sinks accept validated; code.exec never does without an explicit policy grant. Because a simulate output is born untrusted and cannot be laundered, it can never reach code.exec — this is the “emit text but never run” guarantee, enforced by the type system rather than by a sandbox you hope is configured correctly.

Endorsement: the only two doors upward

Moving a label up the lattice is called endorsement, and it has exactly two doors — both audited, both journaled:

1. Passing contracts / a sound verifier → validated. When an untrusted value passes a blocking contract or a sound (not statistical) verifier, it is endorsed to validated.
2. The audited human.approve effect → trusted. A human explicitly approving a value endorses it to trusted. This is the audited human-approval effect, and it is the only way to reach trusted for a value that did not start there.

A statistical verifier cannot endorse to trusted

A statistical verifier — a calibrated judge, a passing semantics() guard — can endorse only to validated, never higher. No error bound converts a statistical verdict into trusted. A statistical(α) guarantee is a bounded false-verdict rate, not a proof, so it can vouch for a value’s validity but not grant it execution authority. This distinction is why a semantic guard can gate a display but not a shell.

Explicit endorsement uses the endorse operation, which is itself policy-gated and journaled. Capability values (Cap[R]), narrowing, and one-shot grants build on this lattice; their operational rules live in the governance spec and defer here for the lattice and the doors.

Worked example: injection becomes a dead end

Consider a service that ingests hostile public text. The report body is a file/network read, so it is born untrusted. Any simulate summary derived from it is untrusted too (meet of untrusted input and untrusted model output). If an attacker embeds "; rm -rf /" in the report hoping to reach a shell:

report = fs.read_text(path)              # untrusted (file read)
summary = summarize(report)              # untrusted (simulate output over untrusted input)
# code.exec(summary)                     # COMPILE ERROR / policy denial: untrusted -> code.exec

The verified crisis-logistics policies encode this at the capability layer too — its examples: explicitly assert that executing a report body is denied:

examples:
    deny:
        code.exec(Report.body)
        proc.spawn("sh", ["-c", Report.body])

Trust labels are the type-level half of that story, and policies are the capability half. Together, “the report can influence text, never authority” is enforced by construction, not by review.

Interaction with policies and events

• Policies can refine on the label. A policy where label(data) rule restricts a grant by the trust label of the flowing data — for example, admit a sink only for trusted inputs.
• Emitting endorses nothing. An event payload’s label is the meet of its fields at emission and travels with delivery: an untrusted simulate output emitted as an event is still untrusted in every handler.
• Healers hold zero endorsement power. A heal runs with a patch-scoped capability and no ability to endorse, so a prompt-injection- driven heal is an escalation-proof dead end.

Two meanings of “provenance” — don’t confuse them

The word “provenance” appears in two distinct places in Sema, and this page owns only the first:

1. Trust labels / information flow (this page) — the governance concept: where a value came from, how its label propagates, and where it may flow. This is a type- system mechanism.
2. The std.provenance module — a small utility library for citation-id mapping: assigning each unique source URL a stable global id and rewriting a result’s local [n] citation markers to those global ids. It is pure (!{}) and has nothing to do with the trust lattice.

For the module, see:

• std.provenance — the module introduction.
• stdlib API: provenance — the generated API reference (Cit, Doc, build_url_to_id, rewrite).

Failure modes

• An untrusted/validated value reaching a trusted-only sink → compile error or policy denial; taint cannot be laundered.
• Trying to endorse to trusted via a statistical verifier → rejected; only human.approve reaches trusted.
• A field write on a trusted aggregate with an untrusted value → the aggregate is re-labelled down to untrusted.
• endorse under a policy that forbids it → denied and journaled.

How it’s checked

• Trust labels are inferred from source constructs and propagated by the type system; sink checks are enforced at compile time.
• endorse and human.approve are journaled, so every upward move is auditable.
• Policies with where label(data) refinements make label-conditioned grants explicit and analyzable.

See also

• Effects & Capabilities — human.approve and the sink effects.
• Policies — where label(data) and the capability half of information-flow control.
• Verification — sound vs statistical verifiers and the guarantee lattice.
• std.provenance / stdlib API — the citation-mapping module (a different “provenance”).