Skip to content

feat(verification): classify and gate policy words in the mechanism surface #80

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wefio wants to merge 1 commit into from
Closed

feat(verification): classify and gate policy words in the mechanism surface #80

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions agent-context.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -153,6 +153,7 @@ routes:
- complexity:gate
- verify:packages
- glossary:check
- check:policy-words
- rtm:check
- test:product
advisory: [verify:research, verify:chaos]
Expand Down
2 changes: 1 addition & 1 deletion docs/decisions/implemented/2026-09-20-the-program-answers-legality.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@

**Status:** implemented
**Approved:** explicit
**Relates to:** [Mechanism, not policy](../proposed/2026-09-21-mechanism-not-policy.md), [Board governance and capability addressing](2026-09-06-board-governance-addressing.md), [Name the collaboration protocol and its task-unit sub-protocol](2026-09-20-name-the-collaboration-protocol.md), [Task unit semantics](../../design/task-unit-semantics.md), [The contract's obligations](../../design/task-unit-semantics-obligations.md), [Protocol-governed collaboration: the parts, the gaps](../../design/protocol-governed-collaboration.md)
**Relates to:** [Mechanism, not policy](2026-09-21-mechanism-not-policy.md), [Board governance and capability addressing](2026-09-06-board-governance-addressing.md), [Name the collaboration protocol and its task-unit sub-protocol](2026-09-20-name-the-collaboration-protocol.md), [Task unit semantics](../../design/task-unit-semantics.md), [The contract's obligations](../../design/task-unit-semantics-obligations.md), [Protocol-governed collaboration: the parts, the gaps](../../design/protocol-governed-collaboration.md)

## Problem

Expand Down
2 changes: 1 addition & 1 deletion docs/decisions/implemented/2026-09-20-the-program-answers-legality.zh-CN.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@

**Status:** implemented
**Approved:** explicit
**Relates to:** [机制，不是策略](../proposed/2026-09-21-mechanism-not-policy.zh-CN.md)、[黑板治理与能力寻址](2026-09-06-board-governance-addressing.zh-CN.md)、[给协作协议及其任务单元子协议命名](2026-09-20-name-the-collaboration-protocol.zh-CN.md)、[任务单元语义](../../design/task-unit-semantics.md)、[契约的义务](../../design/task-unit-semantics-obligations.md)、[协议化协作：组成部分与空缺](../../design/protocol-governed-collaboration.zh-CN.md)
**Relates to:** [机制，不是策略](2026-09-21-mechanism-not-policy.zh-CN.md)、[黑板治理与能力寻址](2026-09-06-board-governance-addressing.zh-CN.md)、[给协作协议及其任务单元子协议命名](2026-09-20-name-the-collaboration-protocol.zh-CN.md)、[任务单元语义](../../design/task-unit-semantics.md)、[契约的义务](../../design/task-unit-semantics-obligations.md)、[协议化协作：组成部分与空缺](../../design/protocol-governed-collaboration.zh-CN.md)

## 问题

Expand Down
113 changes: 67 additions & 46 deletions ...oposed/2026-09-21-mechanism-not-policy.md → ...mented/2026-09-21-mechanism-not-policy.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,12 +2,13 @@

[中文](2026-09-21-mechanism-not-policy.zh-CN.md)

**Status:** proposed
**Relates to:** [The program answers legality](../implemented/2026-09-20-the-program-answers-legality.md), [The frame, its data format, and its storage](2026-09-21-the-frame-and-its-storage.md), [Board governance and capability addressing](../implemented/2026-09-06-board-governance-addressing.md), [Protocol-governed collaboration: the parts, the gaps](../../design/protocol-governed-collaboration.md), [Task unit semantics](../../design/task-unit-semantics.md)
**Status:** implemented
**Approved:** explicit
**Relates to:** [The program answers legality](2026-09-20-the-program-answers-legality.md), [The frame, its data format, and its storage](../proposed/2026-09-21-the-frame-and-its-storage.md), [Board governance and capability addressing](../implemented/2026-09-06-board-governance-addressing.md), [Protocol-governed collaboration: the parts, the gaps](../../design/protocol-governed-collaboration.md), [Task unit semantics](../../design/task-unit-semantics.md)

## Problem

Two proposed records each need the same sentence, and neither states it. The legality record says what the
The legality and frame/storage records need the same ownership rule. The legality record says what the
program does and what it refuses to decide. The frame and storage record says what the core knows and what
it never parses. Those are the same division, seen from the side of the decision and from the side of the
data, and because nothing names it, the division has to be re-argued every time a field or a rule appears.
Expand All @@ -21,7 +22,7 @@ The split also needs to be sharp enough to settle an argument rather than to ser
out of the core" does not decide whether `effect` or `operation` may be a column, or whether a legality rule
may live in the program at all.

## Proposal
## Decision

Take Hydra's principle - a kernel provides mechanisms and refuses policy - and state it as two contracts.

Expand All @@ -44,11 +45,29 @@ Take Hydra's principle - a kernel provides mechanisms and refuses policy - and s
**The decision procedure.** For each field, type and code path, ask whether it is mechanism or policy. A
rule's _check_ is mechanism; the rule's _name, wording and enablement_ are policy.

**The mechanically checkable rule.** No policy word may appear in the mechanism layer's code, type
declarations or schema paths. The list is maintained - `patch`, `editable`, `files`, `instruction`,
`checks`, `repair-first` - and a hit is a leak rather than a style question. The list may grow, and adding
a word is recorded. A word alone is not enough to judge: `files` is a policy word in a ticket type and a
mechanism word at a filesystem boundary, so the check carries the path.
**The mechanically checkable rule.** Every vocabulary hit on the declared mechanism surface is
classified as `mechanism`, `policy`, or `undecided`, with a rationale and an exact occurrence count.
[The maintained list and classification table](../../../tools/policy-word-list.ts) own the vocabulary,
scan paths, and classifications. A word alone does not decide its role: `files` can name a ticket payload
or a filesystem boundary. Roles are not files.

[`check:policy-words`](../../../tools/policy-word-check.ts) is blocking in the shared static contract.
It scans TypeScript identifiers and string/template literals, including SQL, but ignores TypeScript
comments. Camel, snake and kebab spellings count; `dispatch` does not count as `patch`. Each record is
keyed by repository path, enclosing named declaration/method chain (or `<module>`), and word. Line
numbers are diagnostic only; a multiline literal is located at its starting line. Whitespace and
comment changes do not change a record's identity. `npm run check:policy-words -- --list` prints the
classified sites, observed locations and reasons.

Existing policy hits are explicitly grandfathered, not declared clean. A new site, a count change in
either direction, a stale or duplicate record, invalid classification, invalid TypeScript or missing
scan path fails the check. Removing a leak requires retiring or reducing its record. New occurrences
require an explicit classification and rationale in the same reviewed change; the checker never
refreshes counts automatically. Vocabulary additions are recorded here with their rationale.

The scope is bounded by the maintained path list, not all source, tests or drivers. Source imports and
schema literals on those paths count too. This implements the approved classification and static-check
slice (original Plan 2–3), not the work-shape conversion. The frame/storage proposal remains proposed.

**Rows deliberately left undecided**, so that they are not settled by accident:

Expand All @@ -58,7 +77,12 @@ mechanism word at a filesystem boundary, so the check carries the path.
but whether an input carries content or only a digest is a separate question.
- `operation`, which may be policy.

## What this makes of the work shape
## Deferred

### Work-shape boundary

The work-shape conversion (original Plan 5) is not part of the approved slice. The patch assumptions
below remain; their classification does not assert that an opaque adapter seam has been implemented.

A work shape is not a core concept. It is the policy layer's name for the declaration-and-artifact pair
that the core carries without understanding it. The six sites where the patch assumption lives classify as
Expand All @@ -69,8 +93,8 @@ follows.
| `BoardTicket.patch?: FrozenPatchTask & { digest }` | policy | the ticket carries an opaque `declaration` with a digest |
| `patchFrozen()` calling `preparePatchWork`, and the `not a patch task` throw | policy inside the core | freezing and field validation move into the shape adapter; the core only hands back the opaque declaration |
| `refuseWidening` reading `parent.patch.editable` | check is mechanism, wording and enablement are policy | permission closure becomes a declared constraint the program enforces and reports reasons for |
| the ten `FrozenPatchWork` signatures in the session mechanism | mixed | rendering a declaration into a prompt and submitting an artifact are policy; session lifecycle, metrics and cancellation are mechanism |
| `task_run_tasks.patch_files` / `patch_editable`, parsed in the store | policy in the schema | belongs in the payload document; the mechanism part is the run, task, revision, input, dependency and operation columns |
| `FrozenPatchWork` signatures in the session mechanism | mixed | rendering a declaration into a prompt and submitting an artifact are policy; session lifecycle, metrics and cancellation are mechanism |
| `task_run_tasks.patch_files` / `patch_editable`, parsed in the store | policy in the schema | belongs in the payload document; run, task and revision are mechanism, while input/dependency granularity and operation remain undecided |
| drivers asserting `ticket.patch!.digest` | policy assertion | the mechanism assertion is that a declaration carries a digest, that a claim binds the attempt, and that a delivery binds the digest |

The legality rule found today is the clearest case of the refinement this record adds: its check belongs to
Expand All @@ -80,34 +104,35 @@ shape of fix as step 3 of the legality record, which landed on 2026-09-23: repai
constraint rather than shared planning policy. Two independent fixes taking the same shape is evidence that the classification
is the right one.

### Field experiments and separation evidence

- `task_run_tasks.effect`, input/dependency granularity and `operation` remain undecided. Their owning
field must be exercised under an alternative declaration before deciding ownership; this gate does
not include those words or resolve them.
- The `files` groups in schema migration and `TaskUnit` are marked `undecided`: a group combines
patch-specific paths with another role. Resolve them by separating the DDL subjects or exercising
an alternative input declaration, not by relabelling the entire group mechanism.
- The remaining permission-closure name/enablement coupling needs a declared constraint while its
check continues to execute in the program and return reasons.
- Zero policy hits and a second work shape requiring no mechanism changes are unverified separation
goals, not consequences of passing this ratchet. The draft's [second-shape experiment](../../design/mechanism-in-the-middle.md#results)
remains evidence of coupling, not a completed adapter migration.

## Alternatives considered

- **Keep the slogan and decide case by case.** Rejected: that is what produced six sites, and it offers no
test to apply.
- **Put the principle in the frame record.** Rejected: the principle is wider than the frame - it also
governs the program's share of decisions - so the frame record would become the owner of a rule about the
program.
- **Put it in the legality record.** Rejected for the same reason in reverse: that record is narrower, being
about the program's decisions, and what the core may know is not a legality question.
- **A plugin framework with a registry above the core.** Rejected: no second policy exists to justify the
machinery; one default adapter plus one other shape tests the seam.
- **Decide the undecided rows now.** Rejected: choosing them by preference is precisely what this record
replaces with evidence.

## Acceptance criteria

- The classification covers every site that mentions a policy word, each row marked mechanism, policy, or
undecided.
- No policy word appears in the mechanism layer's read and write paths, type declarations, or schema paths,
from a maintained list and checked mechanically.
- A legality rule's name and enablement come from a declaration, while its check runs in the program and
returns a reason per unit.
- Adding a second work shape changes no mechanism code, demonstrated by the value work the data-check
runner already performs.
- Every undecided row is marked as undecided and is resolved by an experiment rather than by preference.
- The legality record and the frame record both point here, so the division has one home.

## Risks
- **Put the principle in either narrower record.** Rejected: it governs both what the core knows and the
program's share of decisions; neither the frame nor legality record owns the full rule.
- **A plugin framework above the core.** Rejected: one default adapter plus one other shape can test the
seam without building a registry framework.
- **Decide undecided rows by preference.** Rejected: the field experiments remain the deciding evidence.
- **Fail every existing policy hit immediately.** Rejected: the approved slice inventories the debt;
it does not authorize a big-bang work-shape rewrite.
- **A file-level word exemption or a maximum count.** Rejected: it silently admits replacement sites or
leaves dead exemptions. Named-scope exact counts expose moves and reductions for review.

## Consequences

- **Gutting the core.** Hydra's lesson cuts both ways: a kernel with no default policy is unusable. The
practical form is that the core may carry one default policy, patch work, and must not require it.
Expand All @@ -117,13 +142,9 @@ is the right one.
policy nobody declared.
- **A policy word may legitimately remain for a release.** This record does not require a big-bang rename; it
requires that each remaining occurrence is listed.
- **A grep check can be gamed by synonyms.** The check is a floor, not a proof of separation.

## Plan

1. This record. No code.
2. The classification table, with the undecided rows marked.
3. The check: a maintained policy-word list plus a script, wired into the static set.
4. Both records point here.
5. Then the work-shape slice: the mechanism side carries an opaque declaration, with patch as the default
adapter rather than a type.
- **The ratchet can be gamed.** Synonyms and same-count replacements within one named scope can evade it.
Classifications and scope changes need review. The check is a floor, not proof of separation.
- **Exact counts cost maintenance.** Intentional code moves and removals require updating the table;
this prevents silent growth but does not prohibit a reviewed policy change.
- The legality and frame/storage records link here for this shared ownership rule. Neither link approves
the separate frame/storage migration.
Loading
Loading