Intent Authority and Formalization

C3-INTENT-001 — Two roles for natural language

Natural language is both authoring authority and, under intent-preview, an explicit runtime instruction kind. These roles coexist. Existing .zl.md implementation authority and .zli.md public-interface precedence remain as defined by Core-0 authority. Prose cannot weaken type, effect, ownership, or safety rules. Runtime Intent adds a resolution protocol; it does not give every comment execution semantics.

An authoritative intent identifies an immutable UTF-8 source document and selected byte ranges, typed inputs/output, requirement IDs, authorized context, and an acceptance policy. Source bytes are preserved exactly: whitespace, normalization, or wording changes are new authority content. A document may contain unrestricted prose; its English meaning is not defined by EBNF.

C3-INTENT-002 — Declaration and requirement coverage

An intent declaration is a named, typed specification, not a seventh callable domain. Its source header and requirement body use the Core-3 grammar. authority selects a manifest-closed source fragment; resolution seals the actual bytes, not just a mutable path. policy resolves an exact policy record. The mandatory effects { ... } clause bounds candidate execution effects; the host resolution call additionally has the intent effect. Each requirement has a unique local identifier and nonempty prose. A formalize id with name; entry names a proposed checked contract or obligation template; it is not approval of that interpretation.

public intent SortValues(values : Int64List) -> Int64List effects { alloc } {
  authority "sorting.zl.md#requirements";
  policy Package.SortPolicy;
  requirement ordered : "Return the values in nondecreasing order.";
  requirement permutation : "Preserve every input value and its multiplicity.";
  formalize ordered with Contracts.Ordered;
  formalize permutation with Contracts.Permutation;
}

The names above must resolve through the actual package; they are not new built-in runtime types. Every requirement receives an explicit mapping to one or more obligations, a recorded policy-admitted assumption, or an unresolved reason. No requirement disappears because it lacks an automatic formalization. A wholly empty request or a declaration without requirements is invalid.

C3-INTENT-003 — Formalization and endorsement

A formalization binds the authority/intent revision, all requirement mappings, typed formal contract, applicable proof/check/test/empirical obligations, assumptions, and exact environment. Requirements can map to multiple kinds of evidence. A proof-required requirement must have a formal statement and cannot be discharged solely by marking it an assumption or by approving its prose. Requirements outside a formal model remain visibly nonformal; their acceptance criteria still require explicit policy treatment.

The formalization records its authenticated proposing principal. This identity is provenance supplied by the host, not a name the generated text can choose. Approval is an endorsement of this exact interpretation by a policy-authorized principal, which may be a human or an autonomous agent. It binds the approving principal, delegated scope, policy identity, formalization identity, authority revision, and decision. There is no mandatory human gate. Delegation may allow one agent to propose and approve, but this fact must be explicit; a policy requiring independent approval must enforce distinct authorized principals.

Structural requirement coverage is not semantic faithfulness. A proof of a formalized statement does not prove that it captures the original English. Approval and mathematical proof are separately recorded and separately shown. Ambiguity may be resolved through policy-authorized, recorded assumptions; otherwise the request remains unresolved rather than inventing permission.

C3-INTENT-004 — Closed context and instruction hierarchy

Resolution receives a sealed, manifest-bounded context snapshot: source and interface authority, exact dependency artifacts, permitted retrieved inputs, generator configuration, and policy. Context records identify which inputs are instructions, which are authoritative contracts, and which are data. Retrieved pages, comments, generated text, examples, and tool output are data unless an already-authorized policy explicitly designates them as authority.

Such data cannot change the instruction hierarchy, approve itself, grant capabilities, replace the pinned formal challenge, weaken required evidence, or modify protected tests. A generator’s proposal is always subordinate to the approved contract and inherited language rules. Confidential context may be sent only to providers admitted by the live context-access policy; a content digest is not permission to disclose its preimage.

C3-INTENT-005 — Revisions and autonomy

Before approval, formalization may be revised within the resolution budget. After approval, all code/plan candidates and replans for that run must satisfy the same accepted contract, mappings, and assumption policy. Changing the authority, accepted meaning, required obligations, or delegated approval policy requires a new request/approval epoch. Old receipts remain immutable and must not be backdated or relabeled as approval of the new meaning.

New implementations of the same contract can be admitted as recorded revisions. Revocation or expiration of live authority prevents new execution even if the stored interpretation and proof remain valid. Autonomy means the protocol can resolve, approve, retry, and execute within explicit delegation; it is not a promise of successful synthesis or unlimited attempts.

C3-INTENT-006 — Evidence and assurance policy

Policies assign allowed evidence to each obligation, not one undifferentiated “verified” bit. The distinct kinds are proof, runtime-check, test, empirical, and trusted-assumption; interpretation approval is not one of these technical evidence kinds. Required proof must match the exact statement, kernel/environment, model/implementation dependencies, and permitted axioms.

Runtime-check policies must name executable checks and their enforcement point. Prechecks must pass before effects; postchecks can detect a failure after execution but do not make an irreversible effect disappear. A policy must not substitute a postcheck for a required pre-effect guarantee. Tests and empirical observations retain their coverage, bounds, uncertainty, and provenance.

Policy assurance entries are conjunctive requirements: every listed (requirement, evidence-kind) pair must have corresponding obligations of that kind, with duplicate identical pairs rejected. Listing proof and runtime-check for one requirement requires both; it does not offer a downgrade alternative. Every intent requirement must have a policy entry. Assumption-only mappings require an explicit trusted-assumption policy entry and cannot satisfy proof.

Every required obligation must meet its explicitly selected policy. Missing, failed, unsupported, or inconclusive proof cannot silently fall back to tests, approval, a smaller input domain, or a trusted assumption. Aggregate admission means “accepted under this policy,” not “everything proved.”