← All specifications

Goal Contract — accomplish these things, subject to these policies (v0.2)

Status: design spec. Refines Trace Spec §18 (Goals & Acceptance) and complements Goal Faithfulness v0.1, Policy Spec v0.2, and the Apply Formal Methods Pack. Additive and backward-compatible — existing text-bound acceptance items keep resolving (§8). Driven by the CodeLogician Desktop goal loop (declare_goal → per-session active goal → ponens trace enrich).

v0.2 adds composable acceptance (§9). Criteria compose with and/or/not/⇒ and quantify (forall/exists) over component selectors (glob/module/scope/tag), with a per-atom role (met | governed) that selects which axis (§2) it is judged on. The atomic criterion of §3 is the leaf of this language, so legacy single-criterion goals are unchanged — they are the implicit Atom case and resolve exactly as before.

1. Motivation — two unstructured seams

§18 makes acceptance rigorous once an item binds to evidence. But the binding for the two kinds that carry the load is a fuzzy text query, and evidence rigor/provenance is implicit:

1. Binding by description text. A property item binds via {symbol?, property?} where property is “a keyword expected in the goal description”. Resolution is “does this keyword appear in the VG’s description string.” When the agent proves rank_transitivity but the VG description reads “rank transitivity”, the substring misses and the criterion silently stays Not checked even though it is proved. (This is the desktop’s “goal never ticks” bug — a structural defect, not a UI one.)
2. Provenance is unspecified. “A test suite” and “a test suite generated from an exhaustive region decomposition” resolve identically, though one is far stronger. Rigor lives nowhere.

This spec fixes both by making the goal a contract with two explicit halves:

Accomplish these things — typed acceptance criteria over code components, resolved by artifact lineage (not text). Subject to these policies — the rigor/governance bar, declared on the goal with sensible defaults.

2. Three orthogonal axes (all declared in the goal)

Trustworthy done = met ∧ governed ∧ certified. Each is independent and separately reported. A criterion can be met but not governed — evidence exists but is too weak for the goal’s pack — which today reads silently as “done” and here becomes a first-class, surfaced state.

This refines Faithfulness v0.1 §6: evidence strength/provenance moves out of faithfulness grading and into the governed axis (policies over lineage). Faithfulness keeps rightness — coverage, review, non-retrofit; policy owns rigor.

3. Acceptance criterion = a required evidence artifact

A criterion names a code component and the artifact that serves as its evidence. That is all it encodes. It does not say whether the artifact is good enough — proved, autoformalized, passing, decomposition-backed. That is entirely the policies’ job (§5). Keeping the two apart removes the overlap between “grading” and “policy”: met = the evidence exists; governed = the evidence is good enough.

type evidence_req = {
  artifact : string;   (* the artifact TYPE required in the component's lineage —
                          VerificationResult | Decomp | Tests | Diff | Documentation | … *)
}

type acceptance_criterion = {
  id        : string;
  statement : string;                       (* human "what must be true" — for reading + certification *)
  component : { function_ : string; file : string option };
  evidence  : evidence_req;
  required  : bool;                         (* Faithfulness v0.1 *)
  covers    : string list;                  (* intent clauses it covers — Faithfulness v0.1 §5 *)
}

Any artifact type is valid evidence — formal (a VerificationResult, a Decomp) or informal (a Diff, a generated Tests suite, a Documentation note). A weaker artifact is not rejected here; a policy decides whether it suffices for this component (e.g. “a high-stakes component’s evidence must include a proof”). “Tests were generated” and “tests passed” are no longer two evidence kinds — they are one criterion (Tests present) plus a policy (Tests must pass) that a stricter bar turns on.

4. Resolution by lineage (the #1 fix)

A criterion resolves to met when the trace holds an artifact of the required type whose lineage roots in component.function_ — read from structured provenance (target_symbol, derived_from, payload.symbols), never a description string. When several match, the latest by producer action is the evidence pointer (evidence_ref on the enriched item).

That is the whole rule. There is no per-type pass condition (no expect, min, min_regions, all_pass): a refuted VerificationResult still exists, so its criterion is met — whether the result had to be proved is the refuted_results_must_be_reproved policy on the governed axis. Quality of derivation lives in exactly one place.

Component precision. An artifact that declares its own target_symbol (a VG, a Decomp, a targeted Diff) is about that component — not every symbol the shared IMLModel happens to formalize. Only when nothing in the lineage names a target do we fall back to the model’s symbol list. (Without this, a decomposition of fee_tier would look like it roots in every symbol of the shared model.)

Recommended (airtight): the verify/decompose/gen-test tools may stamp each produced artifact with satisfies: <criterion_id> — a back-reference — so resolution is by exact id with no matching at all. Optional; lineage matching is the floor.

5. Subject to policies — governance on the goal

A goal declares the packs/policies that govern it. Governance is layered, so a goal that names nothing still has a floor, and a regulated project raises the bar in one place:

type goal_policies = {
  packs    : string list;   (* e.g. ["apply_formal_methods"], ["do_178c"] *)
  policies : string list;   (* individual policy ids, additive *)
  disabled : string list;   (* pack/policy ids turned OFF at this layer — recorded, never silent (§6) *)
}
(* effective set = (goal.packs ∪ project_default_packs ∪ GLOBAL_BASELINE) \ disabled(any layer) *)

Proposed by the agent, selected by a human

The agent MAY propose packs/policies — the high-stakes scan flags money math → it suggests apply_formal_methods. A proposal is recorded on the goal but is not effective on its own.

Normative rule. The party that meets a goal must not be the sole party that sets its rigor bar — parallel to Faithfulness v0.1’s rule for the definition of done.

The effective set is what a human has sanctioned: the global baseline (this spec) and the project default (a prior org decision) are already human-set and apply from the start; per-goal additions the agent proposes take effect only once a human (a party ≠ the doer) approves them. The trace records proposed vs approved, so the audit shows whether the human raised, lowered, or rubber-stamped the bar. Approving the effective set is part of certification (§6) — you certify the criteria and the bar they were held to.

Governed = no effective error-severity policy fails unwaived over the goal’s relevance cone (the trace region the goal touches — §18); see §6 for blocking + overrides. The trace records, per goal: { criteria, effective_policies, disabled, evidence, per-policy verdict, waivers } — a complete, reproducible contract.

The provenance rigor the criterion deliberately omits is exactly what these policies assert over lineage — and most of it already exists in apply_formal_methods:

• high-stakes code is backed by a proof or a decomposition in its lineage;
• verification targets an autoformalized model (not hand-authored IML);
• a result offered as evidence must be proved, not left refuted (refuted_results_must_be_reproved);
• refuted goals get fixed; decompositions produce tests; generated tests trace back to a decomposition.

So “tests must be decomposition-backed” or “the proof must actually hold” are not criterion fields — they are policies the goal opts into.

6. Composition, blocking & overrides

Per goal: met (all required criteria resolved), governed, certified (Faithfulness v0.1).

Severity decides blocking. A policy is error (Red) or warning (Amber):

• an error policy failing over the cone → blocks “done” (the goal is met but not governed, and NOT done);
• a warning failing → annotates, does not block.

So Done = met ∧ governed, where governed = no error-severity policy fails unwaived over the cone.

Overrides are explicit and recorded — never silent. You can proceed past an error, but only by turning the rule off in the record:

A disabled policy does not evaluate; a waived failure does not block — but the trace shows both. So “done” always names the rules that were turned off and the risks accepted, and by whom. There is no path to a green goal that hides a bypassed error — that invariant is the entire point of blocking by default.

Certification sees the overrides. Certifying a goal certifies its effective bar: a goal certified with apply_formal_methods disabled is a visibly weaker claim than one certified with it enforced. The reviewer approves the definition and the overrides, or rejects them.

The enriched goal exposes met / governed / certified plus the residuals that explain any gap:

• required criterion not met → open acceptance gap;
• criterion met but an error policy fails → blocking governance residual (until fixed or waived);
• criterion met but a warning policy fails → advisory governance residual;
• uncovered clause / retrofitted definition → faithfulness residuals (v0.1).

7. Backward compatibility & migration

• Legacy property/change items (text bindings) still resolve via the §18 path; new typed criteria resolve via §4. enrich accepts both; a criterion is typed iff it carries component + evidence.
• The JS resolver (viewer/core/faithfulness.mjs) and the Python resolver (cli/ponens/goals.py) must move together — the parity harness gates it.
• Goals with no policies behave as today plus the global baseline (§5) — no behavior change unless a baseline policy actually bites.

8. What changes where

9. Composable acceptance — the property language (v0.2)

§3 gives one criterion = one required artifact over one component (the atomic case). v0.2 lets criteria compose and quantify, so a goal can state “every payments function is proved and decomposition-backed” in a single acceptance item. The atomic criterion is unchanged; it becomes the leaf of a small formula language evaluated by the same lineage resolution (§4).

9.1 Formula

type formula =
  | Atom    of acceptance_criterion            (* §3 — resolves by lineage (§4) *)
  | And     of formula list
  | Or      of formula list
  | Not     of formula
  | Implies of formula * formula
  | Forall  of { in_ : selector; as_ : string; holds : formula }
  | Exists  of { in_ : selector; as_ : string; holds : formula }
  (* optional `role`, inherited down a subtree — how strictly each atom is judged (§9.2) *)

An acceptance item MAY carry a formula in place of a bare binding. An item without one is exactly today’s atomic criterion (an implicit Atom), so legacy goals resolve unchanged (§7).

9.2 Roles — met vs governed, per atom

A role on a formula (inherited by its subtree) selects which axis of §2 an atom is judged on:

Roles make the met/governed split of §2 addressable inside a single criterion.

9.3 Quantifiers & selectors

Forall/Exists range a bound variable over a selector — a component set drawn from data the trace already carries (component_ids §7.1, per-model symbols, high_stakes_paths):

A body atom names the bound component as { component = var "f" } (substituted per element). Forall is And over the set; Exists is Or. An empty selector resolves todo, never a vacuous done — an empty match is almost always a mis-spec, and false-green is the dangerous direction.

9.4 Status lattice

Combinators compose the four resolved statuses (not booleans), so a contested or partial branch stays visible instead of collapsing to true/false:

Evaluation is additive to §4 and mirrored across the Python (cli/ponens/goals.py) and JS resolvers under the parity harness (§7).

10. Open questions

1. Component cardinality — Resolved (v0.2, §9.3): a criterion may quantify over a component set via Forall/Exists over a selector; the singular criterion remains the atomic (Atom) case.
2. Disambiguating within a component — Partially addressed (v0.2). The selector language pins which components a criterion ranges over, but within a single component the latest artifact of the required type is still taken (§4). An optional per-atom artifact filter (pin which of two proved properties) is deferred until a real case needs it.
3. Baseline contents — exactly which rules are non-optional global baseline vs. opt-in pack.
4. satisfies back-reference — adopt now (airtight) or defer behind lineage matching.
5. A symbol→tag index — tag(...) (§9.3) is best-effort over high_stakes_paths today; a first-class tag index would make tag selectors precise.