Coverage policies¶

How a trusted layer states which guarantees an agent should or must make about a domain it uses, and how the result reaches the user. This is the "meta-reasoning" layer: it reasons about the set of guarantees attached to a program, not about the program's traces.

The problem: silent omission¶

A program can import several trusted domains — email, a database, a bank — and attach a strong guarantee to one while saying nothing about another. An absent guarantee and an explicit no_guarantees() look the same to a user skimming the approval dialog: in both cases the domain is unconstrained. no_guarantees() exists to make weakness visible, but nothing forces the agent to write it.

Coverage policies close that gap. They let the Trusted Layer Engineer (TLE) declare, per domain, which contracts matter — and the prover and approval service then surface (or enforce) the difference between stated and used.

The manifest¶

A trusted root may contain a policy.py exposing a module-level POLICY — a DomainPolicy (or a sequence of them):

# tools/email/trusted/policy.py
from clauz3.policy import domain_policy

POLICY = domain_policy(
    when_used="send_email",                  # trusted fn that activates the domain
    recommended=["only", "unique_recipients"],
    required=[],                             # nullary invariants (see below)
    label="email",
)

A policy names contracts by their bare @contract name (only, unique_recipients). It is plain data: loading it runs no agent code and adds no solver work for the recommended/silent checks. The loader finds it via the same trusted-root discovery used for effects and contracts, so no extra configuration is needed — dropping a policy.py into a trusted root is enough.

Because policies live in the trusted root, only the TLE can write them. Agent code is forbidden from declaring its own obligations, exactly as it is forbidden from writing @clauz3.trusted, @contract, or @clauz3.solver.

`recommended` vs `required`¶

These are two different mechanisms, not two severities of one:

Tier	Meaning	Effect
`recommended`	the agent should state this	a coverage flag in the approval UI; never blocks the proof
`required`	the agent's program must satisfy this	a proof obligation conjoined into the proof; a violation rejects the program before approval

recommended is the genuine meta-reasoning: a lint over the guarantee set. required is closer to assume/guarantee reasoning — the TLE contributes a guarantee that holds whenever the effect is reachable, whether or not the agent mentioned it.

How "used" is determined¶

A domain counts as used when the selected entry or a helper it calls contains a call to its when_used function. Required-contract injection and approval coverage use the same call analysis, including custom entry targets. This remains a static over-approximation: a send_email call in a dead branch still counts. Merely defining an unused function or class does not contribute calls.

Import aliases resolve in the scope of each call. Both module imports and local imports in called helpers are supported; an import in an unused function or class cannot rename the entry's calls or remove a required obligation. Simple callable aliases such as deliver = send_email; deliver(...) and called nested helpers are followed too. Duplicate module helpers use the final binding; duplicate definitions of the selected entry are refused.

Imported ordinary helpers are followed through their source files under the configured import roots, including aliases and relative re-exports. A trusted effect stops this traversal at its declared boundary; its implementation is not part of the agent's symbolic call graph. Merely placing an ordinary helper under a trusted root does not make it a boundary.

Call discovery reads source without executing imports and keeps its module cache local to that analysis. It does not search ambient sys.path. Missing source, unresolved exports, wildcard imports, and source requiring attribute assignment inference use the conservative fallback below. This can activate unrelated policies, including for external library helpers whose source is outside the configured roots.

Vetted, modelled math and re calls (and known math scalar constants) do not activate unrelated policies when their loaded module has a verified standard-library origin. Configured source modules with those names take precedence, and unsupported or unverified modules keep the conservative fallback. Import permission alone does not establish that a callable is pure; frameworks and arbitrary library callbacks receive no blanket exemption.

For a callable reassigned inside a function, the analysis retains its possible local bindings. This conservatively covers later loop iterations and calls through closures, and can trigger a policy even when one binding is never used.

When lexical lookup cannot determine a call target, every domain policy under the supplied trusted roots is considered used. This includes calls through callback parameters, returned functions, subscripts, and conditional callees. All required contracts are then conjoined into the proof, and approval coverage reports every potentially used domain. A dynamically selected pure function can therefore trigger obligations for unrelated domains; this conservative fallback prevents an unresolved callable from silently removing an obligation. Known callable values are also followed when passed as arguments, returned, or stored in containers. This keeps an escaping nested function's effects in the analysis even when an imported helper makes the eventual call. Resolved builtin constructors such as str() and range() do not trigger the fallback. A callback or agent-defined class with the same name still requires conservative analysis; the binding, rather than its spelling, determines this.

Coverage statuses¶

For each used domain, compute_coverage() reports one status, derived from the agent's guarantee expressions (matched to a domain by resolving the guarantee's import alias back to the trusted package):

Status	Condition
`covered`	all recommended/required contracts are stated
`recommended_gap`	the domain is addressed, but a recommended contract is missing
`silent_gap`	the domain is used, but the agent stated no guarantee about it
`required_gap`	a required contract is missing

Direct callers can select an entry with target="task"; the default is main. Pass import_roots and trusted_roots to compute_coverage() (or transitive_calls()) to resolve imported helpers and trusted boundaries. Without those roots, imported callees use the conservative fallback. The CLI and runner supply the same roots for required proofs and approval coverage. If that module-level function is absent, compute_coverage() raises ValueError instead of returning a report that suggests no domain is used.

Alias resolution is what stops a false silent_gap when the agent used a real but unlisted contract such as emails.only(...). Guarantee names resolve through module imports, including renamed contract helpers; local imports in function or class bodies cannot change which domain an entry guarantee covers.

The report is attached to the approval request under a coverage key, alongside guarantees and proofs. The approval service renders it as a Coverage section on the request detail page — gaps sorted above covered domains, with silent_gap and required_gap styled loudest — and a per-request badge on the index showing the worst status, so a reviewer sees a flag at a glance.

How `required` is enforced¶

When a target function uses a required contract's triggering effect, the prover conjoins that contract into the proof. It does this by rewriting only the proved copy of the source: it adds a @clauz3.guarantee(<contract>()) decorator (and the import it needs) so the obligation resolves through the same inference-and-registry path as an agent-written guarantee. The executed program and the approval request keep the original, unmodified source.

Conjoining is sound even for domains that are not used: a relational contract over an empty fact set (all, distinct, empty, bounded count/sum) is vacuously true. Gating on use keeps the behaviour predictable and matches the "obligation triggered by use" intent.

Because the TLE cannot know agent-supplied arguments, required contracts must be nullary invariants — unique_recipients(), not only([...]). A required name that is non-nullary or not a registered @contract raises a ProverConfigError.

Limitations and future work¶

Coverage is mention-level, not entailment-level. A recommendation is "covered" when the agent states a contract of that name, not when the proved guarantee logically implies it. Entailment-strength coverage would need a subsumption check in Z3 — the same machinery as the subsumption-over-policies future work.
required_gap labelling. With enforcement on, a required_gap reaching the UI means "we enforced it for you and it held" (a violation would have been rejected earlier). A future label could distinguish auto-enforced from missing.
when_used names trusted effects. It could once name a @deal.has marker, resolving to whichever functions carried the string — facts with non-uniform shapes, and a set the policy could not see. A token that names no trusted effect is now a configuration error, so a typo (or a marker) fails closed instead of quietly disabling enforcement. So is a token that is both an effect's name and a marker other effects carry, since it used to reach them all and now reaches one: name every effect the policy covers.

This is checked for every policy, recommended-only ones included. What such a policy loses is quieter than a dropped obligation and no less serious — it stops matching, so its domain leaves the coverage report altogether instead of showing up there as a silent_gap, and the person approving the run is never told the program touched it.