From e00ce94cee21fa42f6cba44914c010a49709cbb8 Mon Sep 17 00:00:00 2001 From: "macstudio-3[bot]" <315372789+macstudio-3[bot]@users.noreply.github.com> Date: Wed, 4 Nov 2026 07:40:32 +0800 Subject: [PATCH] fix(sshx): ground delegation and blocking in current authority and evidence --- README.md | 24 +- README.zh-CN.md | 24 +- skills/sshx/CODEX_WORKER_SPEC.md | 14 + skills/sshx/SKILL.md | 84 ++- skills/sshx/formal/README.md | 88 ++- .../sshx/formal/Sshx/Behavior/Invariant.lean | 47 +- skills/sshx/formal/Sshx/Behavior/Model.lean | 81 ++- .../sshx/formal/Sshx/Behavior/Scenarios.lean | 641 +++++++++++++++--- skills/sshx/formal/Sshx/Blocking.lean | 133 +++- skills/sshx/formal/Sshx/Carrier.lean | 3 +- .../sshx/formal/Sshx/Clauses/Boundaries.lean | 21 +- skills/sshx/formal/Sshx/Clauses/Contract.lean | 50 +- .../sshx/formal/Sshx/Clauses/Delegation.lean | 24 + .../sshx/formal/Sshx/Reasoning/Authority.lean | 57 +- .../formal/Sshx/Reasoning/Convergence.lean | 34 +- .../formal/Sshx/Reasoning/Discipline.lean | 6 +- skills/sshx/formal/Sshx/Reasoning/Guards.lean | 12 +- skills/sshx/formal/Sshx/Reasoning/Panel.lean | 27 +- skills/sshx/formal/Sshx/Reasoning/Repair.lean | 52 +- skills/sshx/formal/Sshx/Reasoning/Review.lean | 35 +- .../formal/Sshx/Reasoning/Termination.lean | 18 +- skills/sshx/formal/Sshx/Records.lean | 11 + skills/sshx/scripts/run-codex-worker.sh | 8 +- skills/sshx/tests/test_run_codex_worker.py | 41 ++ skills/sshx/tests/test_skill_distribution.py | 84 +++ skills/sshx/tests/test_sshx_contract.py | 295 ++++++-- 26 files changed, 1506 insertions(+), 408 deletions(-) create mode 100644 skills/sshx/tests/test_skill_distribution.py diff --git a/README.md b/README.md index 14778303..d3ae5d8c 100644 --- a/README.md +++ b/README.md @@ -2,9 +2,9 @@ English canonical public documentation. [Chinese companion](./README.zh-CN.md). -`consensus-rnd` publishes Agent Skills for Claude Code, Codex, Cursor, and Gemini. Its `sshx` skill brings isolated worker perspectives to a high-risk decision or implementation task, converges on a concrete plan, and checks the result through independent review. The deliverable is a prompt contract and its supporting files, shared across platform manifests. +`consensus-rnd` publishes Agent Skills for Claude Code, Codex, Cursor, and Gemini. Its `sshx` skill brings isolated worker perspectives to an authorized decision or implementation task, converges on a concrete plan, and checks the result through independent review. The deliverable is a prompt contract and its supporting files, shared across platform manifests. -Use it when product, architecture, correctness, safety, or cost risks justify separate perspectives. Routine one-step answers whose outcome would not change do not justify the protocol's cost. See the [trigger and exclusions](./skills/sshx/SKILL.md#trigger). +Activate it only for an explicit request for consensus, multi-angle thinking or delegated review, or an applicable host/repository mandate. Risk alone and a generic architecture review request do not activate it; within authorization, weigh whether separate perspectives justify the cost. See the [trigger and exclusions](./skills/sshx/SKILL.md#trigger). ## What It Provides @@ -57,6 +57,8 @@ The [review triplet](./skills/sshx/SKILL.md#review-triplet) applies the [review A [termination gate](./skills/sshx/SKILL.md#termination-gate) applies inside the final stage only when the host has positively declared a goal-driven continuation mechanism in the [goal contract](./skills/sshx/SKILL.md#goal-contract), and an affirmative satisfaction claim is being considered. It is not an eighth stage and grants no control over the host mechanism. +Only confirmed defects against the current goal or an existing contract enter automatic repairs. Findings retain `evidence_status` and `user_goal_basis`; uncertain changes to product or permission semantics go to their owner for clarification. A user correction cancels dependent stale plan, review and repair authority while preserving history and active-job protection. See [goal corrections](./skills/sshx/SKILL.md#goal-contract) and [admission](./skills/sshx/SKILL.md#reasoning-discipline). + ## Risks and Limits - **Broad execution access:** the Codex runner defaults to `danger-full-access`. Read the [invocation contract](./skills/sshx/CODEX_WORKER_SPEC.md#invocation) and [threat model](./skills/sshx/CODEX_WORKER_SPEC.md#threat-model) before supplying a work target. @@ -106,6 +108,24 @@ The plugin identity is declared in the [marketplace](./.claude-plugin/marketplac The [Codex](./.codex-plugin/plugin.json) and [Cursor](./.cursor-plugin/plugin.json) manifests both declare `"skills": "./skills/"`. Use the platform's plugin support to load the repository and read the [skill contract](./skills/sshx/SKILL.md); installation and invocation details depend on the host. +### Verify the effective copy and refresh manually + +Before dispatch, [worker delegation](./skills/sshx/SKILL.md#worker-delegation) records the actually read skill path, SHA-256, available checkout revision/dirty state, and current Heca policy in existing gate evidence. A manifest version or upstream release cannot identify a copied or locally edited skill, or prove an open session adopted it. Explicit user disable wins opt-in on every route, including retry, fallback, repair and resume; tools alone never opt in. + +Inspect the path reported by the host, following any symlink, rather than assuming an installation directory. For a checkout, these read-only commands distinguish bytes from revision and manifest metadata: + +```bash +shasum -a 256 /SKILL.md +git -C rev-parse HEAD +git -C status --short +``` + +Compare the effective file with the intended checkout's `skills/sshx/SKILL.md` using `diff`; also compare supporting files because the whole skill directory is the distribution unit. A copied installation may have no Git revision: report that limitation and keep the content hash. None of these observations proves current-session adoption. Confirm the newly read path/hash and policy in the next run; if the host cannot expose that association, label adoption `ASSUMED-UNVERIFIED`. + +Manual refresh is an owner action, never automatic sshx behavior. For a direct-folder installation, refresh the entire resolved skill directory from a verified checkout using the host's supported skill installation procedure, then compare again. [Official Codex skills guidance](https://developers.openai.com/codex/skills/) documents discovery locations, symlink support and automatic change detection; restart Codex if an update does not appear. When multiple copies exist, verify the selected path. This does not assert that a legacy `~/.codex/skills` copy is the selected source or that an existing session reloaded it. + +For the Claude marketplace installation above, [official plugin guidance](https://code.claude.com/docs/en/discover-plugins#update-plugins-now) documents `claude plugin update consensus-rnd@consensus-rnd`, then `/reload-plugins` to apply updated disk content to the session. Use the installed host's supported UI if that command is unavailable. For Cursor and Gemini, use their installed plugin/extension manager and confirm the effective source again; no reload command or adoption behavior is claimed here. These official owner procedures were not exercised on this host: local refresh/reload remains `ASSUMED-UNVERIFIED`. The skill executes no refresh or host/global setting change. + ### Gemini CLI The [extension manifest](./gemini-extension.json) selects `GEMINI.md` as its context file. [GEMINI.md](./GEMINI.md) lists the available skill and directs the agent to read its contract on demand. diff --git a/README.zh-CN.md b/README.zh-CN.md index 2c608537..56de1e59 100644 --- a/README.zh-CN.md +++ b/README.zh-CN.md @@ -2,9 +2,9 @@ 中文公开文档。英文 canonical：[README.md](./README.md)。 -`consensus-rnd` 为 Claude Code、Codex、Cursor 和 Gemini 发布 Agent Skills。`sshx` 用隔离的 worker 视角处理高风险决策或实现任务，收敛出具体方案，再由独立 review 检查产物。交付物是 prompt 合同及其配套文件，由各平台清单共享。 +`consensus-rnd` 为 Claude Code、Codex、Cursor 和 Gemini 发布 Agent Skills。`sshx` 用隔离的 worker 视角处理获授权的决策或实现任务，收敛出具体方案，再由独立 review 检查产物。交付物是 prompt 合同及其配套文件，由各平台清单共享。 -当产品、架构、正确性、安全或成本风险值得投入多个视角时使用。若常规一步式回答不会因增加视角而改变结果，就不值得承担协议成本。详见[触发条件与排除项](./skills/sshx/SKILL.md#trigger)。 +仅在用户明确要求共识、多角度思考或委派 review，或适用的 host/仓库规则要求该流程时激活。风险或一般架构 review 请求本身不构成授权；获得授权后，再判断多个视角是否值得其成本。详见[触发条件与排除项](./skills/sshx/SKILL.md#trigger)。 ## 提供什么 @@ -57,6 +57,8 @@ 只有 host 在[目标合同](./skills/sshx/SKILL.md#goal-contract)中明确声明了目标驱动的继续执行机制，且 caller 正准备肯定目标已满足时，最后阶段内部才适用[终止闸门](./skills/sshx/SKILL.md#termination-gate)。它不是第八阶段，也不授予控制 host 机制的权限。 +只有违反当前目标或既有合同的已确认缺陷进入自动修复。发现项保留 `evidence_status` 与 `user_goal_basis`；涉及产品或权限语义的不确定改动向 owner 澄清。用户纠正立即撤销依赖旧方案的 plan、review 与 repair 权限，同时保留历史及 active job 保护。详见[目标纠正](./skills/sshx/SKILL.md#goal-contract)与[准入](./skills/sshx/SKILL.md#reasoning-discipline)。 + ## 风险与限制 - **宽执行权限：** Codex runner 默认使用 `danger-full-access`。提供工作目标前，请阅读[调用合同](./skills/sshx/CODEX_WORKER_SPEC.md#invocation)和[威胁模型](./skills/sshx/CODEX_WORKER_SPEC.md#threat-model)。 @@ -106,6 +108,24 @@ Host 必须为 runner 派发提供带完成通知的后台执行、超时和整 [Codex](./.codex-plugin/plugin.json) 与 [Cursor](./.cursor-plugin/plugin.json) 清单都声明 `"skills": "./skills/"`。通过平台插件支持加载仓库并阅读 [skill 合同](./skills/sshx/SKILL.md)；安装与调用细节取决于 host。 +### 核对有效副本与手动刷新 + +派发前，[worker delegation](./skills/sshx/SKILL.md#worker-delegation) 在已有 gate 证据中记录实际读取的 skill 路径、SHA-256、可用的 checkout 修订/脏状态与本轮 Heca 政策。清单版本或上游 release 不能标识复制或本地修改的副本，也不能证明当前会话已经采用。用户明确禁用优先于 opt-in，覆盖重试、fallback、修复与恢复；仅工具暴露永不构成 opt-in。 + +检查 host 报告的路径并跟随符号链接，不预设安装目录。对于 checkout，可用以下只读命令区分内容、修订与清单元数据： + +```bash +shasum -a 256 /SKILL.md +git -C rev-parse HEAD +git -C status --short +``` + +用 `diff` 将有效文件与目标 checkout 的 `skills/sshx/SKILL.md` 比较，同时核对配套文件：整个 skill 目录才是分发单位。复制安装可能没有 Git 修订，应报告此限制并保留内容 hash。这些观察均不能证明当前会话已采用；下一次运行须确认新读取的路径/hash 和政策。host 无法提供这一关联时，采用状态标为 `ASSUMED-UNVERIFIED`。 + +手动刷新由 owner 执行，不是 sshx 自动行为。直接目录安装应通过 host 支持的 skill 安装流程，从已核对的 checkout 刷新整个已解析目录，然后重新比较。[Codex 官方 skills 文档](https://developers.openai.com/codex/skills/) 说明发现位置、符号链接支持与自动检测变更；更新未出现时重启 Codex。存在多个副本时，须确认选中的路径；这不意味着旧 `~/.codex/skills` 副本就是有效来源，也不证明已有会话已重载。 + +上述 Claude marketplace 安装的[官方 plugin 文档](https://code.claude.com/docs/en/discover-plugins#update-plugins-now) 给出 `claude plugin update consensus-rnd@consensus-rnd`，再用 `/reload-plugins` 将磁盘更新应用到会话；所装 host 无此命令时使用其支持的 UI。Cursor 与 Gemini 使用已安装的 plugin/extension manager，再核对有效来源；此处不声明其重载命令或采用行为。上述官方 owner 流程未在本 host 实测，本地刷新/重载仍为 `ASSUMED-UNVERIFIED`；skill 不执行刷新命令，不修改 host/全局设置。 + ### Gemini CLI [扩展清单](./gemini-extension.json)选择 `GEMINI.md` 作为上下文文件。[GEMINI.md](./GEMINI.md) 列出可用 skill，并指示 agent 按需读取合同。 diff --git a/skills/sshx/CODEX_WORKER_SPEC.md b/skills/sshx/CODEX_WORKER_SPEC.md index cd55907c..2a2d20b3 100644 --- a/skills/sshx/CODEX_WORKER_SPEC.md +++ b/skills/sshx/CODEX_WORKER_SPEC.md @@ -142,6 +142,20 @@ atomic rename for those artifacts. It also states the envelope's structural acceptance conditions and includes one runner-rendered, stage-specific minimum valid envelope example. +The actual injected brief must convey exclusive ownership: worker writes only result, +sentinel and their same-directory publication temporaries; stdout/stderr/last-message, +brief/status/exit and their temporaries are runner-owned and must not be created, +overwritten, appended, repaired, normalized or forged by the worker. `log_ref` is copied +as an opaque reference to the existing diagnostic sink, without opening its body or +creating a narrative log; another existing reference needs explicit task supply. +All work/checks precede publication. The last worker tool action atomically publishes +result then sentinel, and the worker immediately returns its compact final reply with +no further tool, artifact inspection or rewrite. These prompt obligations do not impose +same-user filesystem protection. Simulation may demonstrate violations; it does not +prove real workers comply, nor establish timeout causality. A post-sentinel rewrite or +log overwrite cannot replace successful terminal carrier observation. The runner does +not audit write history or strengthen/weaken the completion predicate to do so. + Launch receipts and pure queries are the only sanctioned path discovery mechanisms for the batch, status-read, cleanup, and sweep scripts and for the oracle runner. Those scripts contain no run-layout formula, attempt naming rule, or artifact basename and do not parse diff --git a/skills/sshx/SKILL.md b/skills/sshx/SKILL.md index b4fbdf8c..e7468932 100644 --- a/skills/sshx/SKILL.md +++ b/skills/sshx/SKILL.md @@ -1,6 +1,6 @@ --- name: sshx -description: Use when a high-risk or multi-angle decision needs worker-delegated inline consensus with isolated perspectives, fixed truth tables, and no skill-owned daemon, GitHub, git, label, or release orchestration. +description: Use when an explicit request for consensus, multi-angle thinking or delegated review, or an applicable host mandate authorizes isolated workers and no skill-owned runtime or lifecycle authority. --- # sshx @@ -9,14 +9,9 @@ description: Use when a high-risk or multi-angle decision needs worker-delegated ## Trigger -Use this skill when: +Activate only for explicit user consensus, multi-angle thinking or delegated review, or a sourced applicable host/repository mandate. Record that authority at intake. Risk, importance, tools, budget or generic implementation/architecture review alone never activate sshx; use ordinary work. -- a decision has meaningful product, architecture, correctness, safety, or cost risk; -- the user asks for multi-angle thinking, consensus, or review without starting a long-running work-unit loop; -- a concrete plan should be tested against independent perspectives before implementation; -- a finished change should pass a same-shape review gate before declaring done. - -Do not use this skill for routine one-step answers where no separate perspectives would change the outcome, and do not run it when the decision's stakes cannot justify the protocol's cost: whether to run it follows decision risk, not available budget. +Within authorization, require perspectives that can change the outcome and stakes that justify cost. Risk informs proportionality, never supplies authorization. ## Goal Contract @@ -38,7 +33,7 @@ Do not use this skill for routine one-step answers where no separate perspective - `trust_boundary`: which roles are trusted and which are untrusted. The trusted declaration is **non-adversarial, not infallible**: failures, omissions, and uncertainty by a trusted party remain fully in review scope; - `decision_ownership`: product, governance, and boundary decisions; engineering judgments; and orchestration judgments, each assigned to its owner. -During `intake`, the caller resolves them from current user input, repository rules, existing authorizations, and available execution context, recording sources and explicitly labelling minimal engineering assumptions. It must not ask a startup boundary or harness confirmation question. Explicit user boundaries and permission decisions remain authoritative; routine missing detail is resolved with the smallest task-relevant assumption. +During `intake`, the caller resolves them from current user input, repository rules, existing authorizations, and available execution context, recording sources and explicitly labelling minimal engineering assumptions. It must not ask a routine startup boundary or harness confirmation question. Explicit user boundaries and permission decisions remain authoritative; routine missing detail is resolved with the smallest task-relevant assumption. At intake, preserve sourced owner blocking restrictions, scope and meaning in `constraints` and `harness.trust_boundary`, hence every brief/retry/repair/resume; issue proposals and censuses create no owner policy. `revisions` is an append-only list whose each item contains exactly these three sub-items: @@ -48,11 +43,11 @@ During `intake`, the caller resolves them from current user input, repository ru A revision item missing any one of these sub-items is invalid and fails closed. -Any explicit correction to `GoalArtifact` or `harness` must append one such revision item before routing continues. +Any explicit correction to `GoalArtifact` or `harness` must append one such revision item before routing continues. Corrections immediately supersede dependent pending/active/completed plan/review/repair authority: cancel stale assignments/obligations, preserve history and unrelated valid evidence, reroute corrected scope through existing direction/design gates. Active jobs stay protected until host completion/confirmed teardown; invalidation proves no completion or takeover authority. Revisions never rewrite an earlier target or recompute an earlier settlement. A correction is appended after the settlement it supersedes, and only a later settlement may consume the corrected target. -The caller must write and complete `harness` during `intake`, before any worker dispatch. A routine record gap is repaired from the sources above and recorded as an assumption; only a true requirement, governance, or permission change uses existing owner routing. Silence or routine ambiguity never creates a startup questionnaire or pause. +The caller must write and complete `harness` during `intake`, before any worker dispatch. A routine record gap is repaired from the sources above and recorded as an assumption; only a true requirement, governance, or permission change uses existing owner routing. Silence or routine ambiguity never creates a startup questionnaire or pause. Ask the declared owner about uncertain material product/architecture/permission semantics before dependent changes; independent authorized work may continue. The boundary owner may declare a host-provided goal-driven continuation mechanism only in `harness.provided_capabilities`; the skill must not discover or infer an external mechanism. The termination gate is triggered only by an existing positive authoritative entry declaring such a mechanism. Silence is not absence and does not trigger a confirmation question. Ambiguous or unconfirmed claim-specific authority constrains an affirmative claim and is recorded as an assumption or limitation; it does not pause routine startup or invent a mechanism. When a complete `provided_capabilities` value contains no positive entry, the gate is inapplicable without asserting that the host mechanism is absent. @@ -88,7 +83,7 @@ Each thinking, review, or termination record must include these fields: Thinking, implementation, review, and termination-gate work are worker dispatches. The caller context may intake, choose worker mode, dispatch workers, meta-judge returned `SshxResultEnvelope.conclusion` values, and aggregate and report conclusions only, retaining `log_ref` references. -Each `visible_inputs` value must include the complete `GoalArtifact` (including `harness`) and must not include same-round peer outputs. +Each `visible_inputs` includes complete `GoalArtifact`/`harness`, never same-round peer output. ## Worker Delegation @@ -102,7 +97,7 @@ Each `visible_inputs` value must include the complete `GoalArtifact` (including 4. `isolated-token-subagent` 5. `abstain` -`codex-cli` is an out-of-process worker carrier. Non-mutating means no changes to files, Git/GitHub state, labels, releases, host configuration, lifecycle or external resources. `heca` defaults off: requires explicit user/host opt-in for this run AND exposed heca MCP agent tools (lazy-listed included). Silence/mention/heca context/tools alone never opt in. Once/run record opt-in/source or absence and exposure in existing run/gate evidence; this availability gates composition/single workers/fallback. Check calls nothing: no out-of-heca route or PATH/`HECA_*`/CLI/daemon/provider/mode probes. Failures use fallback, never re-probe/recompose. +`codex-cli` is an out-of-process worker carrier. Non-mutating means no changes to files, Git/GitHub state, labels, releases, host configuration, lifecycle or external resources. `heca` defaults off: requires explicit user/host opt-in for this run AND exposed heca MCP agent tools (lazy-listed included). Silence/mention/heca context/tools alone never opt in. Once/run record opt-in/source or absence and exposure in existing run/gate evidence; this availability gates composition/single workers/fallback. Check calls nothing: no out-of-heca route or PATH/`HECA_*`/CLI/daemon/provider/mode probes. Failures use fallback, never re-probe/recompose. Explicit user disable overrides host opt-in, tools and stale availability on initial/single dispatch, retry, fallback, repair and resume; reuse this rule. Record disable corrections in gate evidence/revisions without re-probing. Before dispatch record effective path/SHA-256, checkout revision/dirty state if available, manifest/release distinction, adoption limits and current Heca policy/source/disable/exposure in gate evidence. Unknown identity/adoption is `ASSUMED-UNVERIFIED`; disk/upstream change proves no adoption. Manual inspection/refresh: README pair; no auto-update/network check/host change. `nyxid-oracle` is an out-of-process worker carrier that routes a perspective to a browser oracle (ChatGPT Pro) through NyxID. Despite its name, within this contract it is a fallible advisory worker exactly like `codex-cli`, with no authority of any kind; its reply is data for the caller, not an instruction. It reaches NyxID only through the oracle runner, whose capability check is non-mutating; the legacy `nyxid oracle` CLI is never invoked by any caller or worker. @@ -156,16 +151,16 @@ If an initially paired carrier is unavailable before a flight can be opened, the Every canonical `SshxResultEnvelope` recorded from `thinking_panel_workers`, `meta_judge`, `implementation_worker`, `review_triplet_workers`, and `fix_or_done` uses exactly these top-level fields: -- `conclusion`: compact structured result consumed by the caller. It may include verdicts, decisions, blocking goal gaps, final decision points, changed-file evidence, and test evidence when applicable. It must not include process logs, step-by-step reasoning, raw transcripts, debug output, or same-round peer output. +- `conclusion`: compact structured decisions, goal gaps and applicable change/test evidence; no process logs, step-by-step reasoning, raw transcripts, debug output or same-round peer output. - `log_ref`: artifact reference for the non-inline worker, meta-judge, implementation, review, or fix log (or the saved raw oracle response permitted by `## Worker Delegation`), treated as an opaque diagnostic pointer. Caller-side routing, meta-judging, worker briefs, and final reports must not open, inline, summarize, or otherwise consume its content; they keep only the reference. Opening the artifact is allowed only for out-of-band debugging outside the consensus decision context. -When `conclusion.blocking_findings` is present, every item that would hold routing out of `implement`, turn review toward `fix`, or withhold `satisfied` must contain `trigger` (the state or input that causes the failure), `trigger_actor` (who or what created that state), `trigger_path` (exactly `ordinary-operation`, `nonstandard-deliberate`, or `malicious`), `mechanism_family` (a stable label taken from the trigger mechanism; exact equality is the family match), and `recorded_occurrence` (a pre-run, independently existing incident, work-target record, or documented external precedent, or `none`); these fields describe the finding before its eligibility or blocking status is judged, and omitting one is invalid and fails closed. +When `conclusion.blocking_findings` is present, candidates require `evidence_status` (exactly `confirmed`, `advisory`, `conditional`, or `unverified`), `user_goal_basis` (violated current goal/contract and source), `trigger`, `trigger_actor`, `trigger_path` (exactly `ordinary-operation`, `nonstandard-deliberate`, or `malicious`), `mechanism_family` (readable label, not exact-match identity), `family_basis` (property, cause, evidenced prior match or reason new), `input_evidence` (environment command/scope/count or `none`, sourced workflow derivation or `none`, owner rule/source or `none`), and `recorded_occurrence` (independent pre-run incident/target record/external precedent or `none`); missing fields fail closed. Describe before judging. `conclusion` is a structured JSON object, not a free-text string, and `log_ref` is a non-empty string reference. When a stage requires a verdict, it is the string at `conclusion.verdict`. -A caller-carried stage record wraps this envelope: it references the envelope's `conclusion` and `log_ref` and may add only the stage metadata named by `InlineConsensusProtocol` and the `## Transcript Template` (such as `role`, `bias`, `visible_inputs`, `worker_mode`, `worker_carrier`, `worker_flight_ref`, `verdict`, and the `meta_judge` and `fix_or_done` `exit`, `concrete_plan`, `goal_gap`, and `next_iteration_question`). The envelope payload itself stays exactly `conclusion` and `log_ref`. A stage record's `verdict` field, when present, is a read-only mirror of its envelope's `conclusion.verdict`; `conclusion.verdict` is the sole verdict source for routing, the two must be equal, and any mismatch fails closed. +Stage records reference envelope `conclusion`/`log_ref` and add only `InlineConsensusProtocol`/`## Transcript Template` metadata. The envelope payload itself stays exactly `conclusion` and `log_ref`. A stage record's `verdict` field, when present, is a read-only mirror of its envelope's `conclusion.verdict`; `conclusion.verdict` is the sole verdict source for routing, the two must be equal, and any mismatch fails closed. -Logs are not inline in caller context. Final reports aggregate `conclusion` values only and retain `log_ref` references for optional inspection. +Final reports aggregate only `conclusion` and opaque `log_ref`; never inline logs. ## Worker Completion Contract @@ -183,9 +178,7 @@ The caller context must not carry worker full reasoning or same-round peer outpu - `SshxResultEnvelope.log_ref` artifact references; - final reports that aggregate conclusions only. -Input isolation and prior sterility are separate dimensions. As a hard invariant, no worker may see a same-round peer output or caller-conversation transcript content outside its explicit dispatch brief or `GoalArtifact`; unavailable isolation requires `abstain`, never single-context roleplay. - -Each dispatch roster is an append-only role ledger ordered by the existing `worker_flights` and corresponding result order. An event may use only evidence in its recorded prefix. One event that uses out-of-prefix evidence invalidates that roster, not an unrelated earlier roster; later appends cannot change a frozen prefix or recompute an earlier settlement. +Input isolation and prior sterility are separate dimensions. As a hard invariant, no worker may see a same-round peer output or caller-conversation transcript content outside its explicit dispatch brief or `GoalArtifact`; unavailable isolation requires `abstain`, never single-context roleplay. Each dispatch roster is an append-only role ledger ordered by the existing `worker_flights` and corresponding result order. An event may use only evidence in its recorded prefix. One event that uses out-of-prefix evidence invalidates that roster, not an unrelated earlier roster; later appends cannot change a frozen prefix or recompute an earlier settlement. Prior sterility is weaker and none of the allowed carriers provides it: `codex-cli` inherits repository `CLAUDE.md` or `AGENTS.md` context, `heca` inherits those rules and unknown/uncontrollable provider user memory, `nyxid-oracle` may inherit unknown and uncontrollable account memory and project context, and `isolated-token-subagent` inherits `CLAUDE.md` and the caller's `MEMORY.md`. All carriers count as independent seats; none may be described as context-sterile or cited as evidence of independent priors. The oracle seat is permanently sterile-context-unverified. Each seat must disclose these inherited context sources in its existing `visible_inputs` value and state whether each source is unknown or uncontrollable, using `repo-prior-exposed` for `codex-cli` and `heca`, `external-prior-exposed` for `nyxid-oracle`, and `caller-prior-exposed` for `isolated-token-subagent`; these are disclosure labels, not new fields. @@ -195,7 +188,7 @@ Prior sterility is weaker and none of the allowed carriers provides it: `codex-c sshx's essence is independent context-isolated perspectives that oppose ugliness and waste to converge on an answer that is both beautiful and worth its cost. -Reference-frame: each thinking, review, or termination perspective identifies the applicable mature theory, engineering principle, industry best practice, mature industry case, mature pattern, or constraint framework governing this class of problem or implementation; surfaces the known-good shape; then re-checks each candidate conclusion, implementation interpretation, repair candidate, or termination judgment against it before settling the verdict. `no applicable mature theory found` is an acceptable explicit fallback; in that case the note says so and still records the root-cause and minimal-path re-check against `GoalArtifact`. +Reference-frame: each thinking, review or termination seat identifies the applicable mature theory/principle, industry practice/case/pattern or constraint framework and known-good shape; re-check every candidate, implementation interpretation, repair or termination judgment against it. If `no applicable mature theory found`, say so and still record root-cause/minimal-path re-check against `GoalArtifact`. Planning evidence must be gathered before a thinking seat settles a candidate plan: search relevant authoritative best-practice sources and inspect the current `work_target`, repository artifacts, history, and visible prior decisions for work that already covers the named `GoalArtifact` terms. Record the searched sources, applicable practice, inspected existing work, and overlap or uncovered delta in the existing dispatch brief or `SshxResultEnvelope.conclusion`. This is prompt-level evidence and adds no `GoalArtifact` field or envelope field. Reuse work that already covers a named `GoalArtifact` term and plan only the uncovered delta. A duplicate mechanism is not a concrete plan. Search scope is bounded by `GoalArtifact` and the assigned review focus; stop once the applicable practice and overlap or delta are settled instead of opening a generic improvement search. A source that cannot be reached or verified is `ASSUMED-UNVERIFIED` and may guide a candidate only as advisory. It cannot be called a best practice, block routing, or create a plan element by itself. Search results never create a `GoalArtifact` term or current consumer. @@ -213,18 +206,18 @@ Goal primacy: 忘记目标 (forgetting the goal), 因小失大 (losing the whole `CapabilityOverlap` is the candidate-solution boundary check: ask whether a candidate takes over a capability already declared in `harness.provided_capabilities`, or changes a decision assignment in `harness.decision_ownership`; either hit is an overlap and therefore out of bounds. `ThreatEligibility` is the review-finding boundary check: ask whether a finding would exist only if a role declared trusted by `harness.trust_boundary` deliberately acted maliciously; if so, the finding is ineligible. Trusted-party failure, omission, and uncertainty remain eligible for inputs on the `ordinary-operation` path. An omission that only matters after a trusted operator deliberately selects a `nonstandard-deliberate` trigger does not become eligible merely by being described as an implementation omission. These are independent checks that share the `harness` fact source. -`BlockingAuthority` is the single admissibility rule for every input that would hold a candidate out of `implement`, turn a review toward `fix`, or withhold `satisfied` — a plan objection, a review finding, or a termination difference. Advisory is the default; blocking is the exception, and the exception has exactly two conjuncts that the input itself must name: first, the `normalized_goal` clause, `constraints` item, or `success_criteria` item that the work as built fails; second, evidence in the work as built that shows the failure — a current call site or input path, an observed failure, a failing verification command, a wrong result — or, against a satisfaction claim, the absence of the evidence the named term demands. Protocol policy, not mathematics, defines these two conjuncts. A blocking finding must also pass the structured trigger check: if its `trigger_path` is not `ordinary-operation` and its `recorded_occurrence` is `none`, the finding is advisory even when both conjuncts are named. `recorded_occurrence` must have existed before this run and independently of the current review; a fixture, reproduction, or state deliberately created by a seat, caller, or repair worker during this run is reachability evidence only and is not a recorded occurrence. An input that names both is blocking, and stays blocking however expensive, inconvenient, or late the repair is after it passes the trigger check; a named basis that evidence shows to be false no longer counts as named, and a named basis whose correctness is disputed keeps its full blocking force until the dispute is settled against evidence — no one may call an input advisory because its named basis is unpersuasive. An input that names fewer than both is advisory: its downgrade record carries what it named, or that it named none, in its own words and never a paraphrase, and it is never the sole basis of a `revise`, `reject`, `abstain`, blocking finding, `unsatisfied`, or any element of a concrete plan; an input that fails the trigger check is advisory too, with the trigger decision recorded in the same words. The same two conjuncts admit a plan element: a defense, validation, abstraction, or compatibility path enters a plan only when it names the `GoalArtifact` term that demands it or a current consumer (an existing call site), and a test introduced together with it may corroborate that basis but never creates it. Findings and plan elements share this contextual chain: default to non-malicious ordinary use and mistakes, tracing actor, actual input path and goal-visible residue after declared recovery. Safety labels supply no evidence; ineligible or absorbed threats authorize no defense, validation or further repair. Failure is objective, not semantic: the rule asks only whether both conjuncts are named, never how well they are evidenced, while the trigger check is mechanical; it removes no actual defect on the `ordinary-operation` path, because a reachable failure, a trusted-party mistake, an omission, and a stated uncertainty each name both. +`BlockingAuthority` is the single admissibility rule for every input that would hold a candidate out of `implement`, turn a review toward `fix`, or withhold `satisfied`. Advisory is the default; blocking is the exception, with exactly two conjuncts the input itself must name: the failed `normalized_goal` clause, `constraints` item or `success_criteria` item, and evidence in the work as built (current call site/input path, observed failure, failing verification, wrong result, or absence of evidence the term demands). Protocol policy, not mathematics, defines these conjuncts. Admission additionally requires `evidence_status=confirmed` and a sourced `user_goal_basis`: Confirmed means an evidenced current-goal/contract defect, including absent required evidence. Advisory/conditional/unverified findings create no blockers or automatic repairs; product decisions belong to their owner. Dispute preserves confirmed defects; unsupported premises are not confirmed. A blocking finding must also pass the structured trigger check: `ordinary-operation` needs `input_evidence` tracing an actual workflow input or a sourced state derivation from the goal-described workflow, including ordinary mistakes/omissions. A tool manual or review fixture alone proves capability/reachability, never ordinary workflow input or occurrence. Without workflow grounding, require independent `recorded_occurrence`, else advisory. Apply sourced owner restrictions from `GoalArtifact`: actual-input-or-occurrence-only additionally requires observed actual input or independent occurrence; absent that rule, future ordinary workflow-produced inputs remain eligible. Missing/disputed provenance is an evidence gap, never an invented restriction. `recorded_occurrence` must have existed before this run and independently of the current review; deliberately constructed run fixtures/reproductions/states are reachability evidence only. After these admission checks, both named conjuncts block regardless of repair cost, inconvenience or lateness. Evidence showing a basis false removes it; a confirmed basis with disputed correctness retains full force until evidence settles it, never downgrade for being unpersuasive. Fewer than both, or a failed trigger check, is advisory: record its original words (including what it named or none) and trigger decision, never paraphrase, in the downgrade; never use it alone for `revise`, `reject`, `abstain`, `unsatisfied`, a blocker or a plan element. The same two conjuncts and evidence-status/goal-basis checks admit a plan element: name the demanding `GoalArtifact` term or current consumer (existing call site); a co-introduced test corroborates but cannot create that basis. Findings/plans trace non-malicious ordinary use/mistakes, actor, actual input path and goal-visible residue after declared recovery. Safety labels prove nothing; ineligible/absorbed threats authorize no defense, validation or repair. After evidence-status/goal-basis admission, force asks whether both conjuncts are named, not how persuasive they are; workflow grounding and owner-policy compliance remain trigger-check premises. A result offered as independent adjudication evidence is inadmissible when its recorded use to generate, tune, or select reaches the candidate's dependency closure. Enlarging that closure may only remove admission, never restore it. A shared model family, inherited repository prior, or disclosed prior alone does not prove contamination; only a recorded dependency path does. `BlockingAuthority` asks only whether a decision input may block; `ThreatEligibility` asks who the actor is; `parsimony` asks how much mechanism; `proportional-containment` asks how far it binds; `worth` asks whether to pay at all; and the aesthetic verdict asks whether the remaining form is coherent. It is a third independent check sharing the `GoalArtifact` and `harness` fact sources with the two above. Inputs that name no second conjunct include an imagined input; a hostile or extreme condition that ordinary operation does not exercise, unless a recorded occurrence — an incident in this work target's own evidence or a documented external precedent for the same mechanism — shows it; a fixture or reproduction constructed during this run is not such an occurrence; a harm that the declared recovery path already absorbs — a retry, a carrier fallback, a fail-closed stop, an honestly reported `abstain`, or an escalation to the declared owner — with no residue visible to `GoalArtifact`; a defect in this run's own transcript or records rather than in the work; and detail whose omission changes no `GoalArtifact` decision. A residue that escapes the recovery path is a second conjunct: a wrong result accepted as correct, a success or satisfaction claim that is not true, state left corrupted or unrecoverable, an unbounded work generator, a violated contract term that nothing detects, or a `GoalArtifact` success criterion the recovery path itself cannot satisfy; a recovery path that is itself missing, unreachable, or undeclared absorbs nothing. Absorption is decided from what the input names against the declared recovery path, never from how unlikely, inconvenient, expensive, or late the failure is. No per-case diagnosis, error taxonomy, or dedicated repair path is owed for an absorbed class: deciding which specific error occurred earns its place only when a `GoalArtifact`-named decision routes differently on that answer. That list is illustrative, not a closure, and enumeration is not itself an absorber. A Lawvere-style diagonal escapes a register only under verified theorem hypotheses, including the recorded finite domain, fixed-point-free constructor and admissible-input correspondence. An open or infinite label alone proves no impossibility, and enumeration alone proves no completeness. A uniform invariant, a verified complete finite treatment, or an already-authorized enforced boundary may establish class coverage; otherwise the class gate routes bounded revise or investigation, and unresolved coverage is reported honestly. Extending an enumeration over an absorbed class is an ugly defect under the aesthetic verdict, not diligence. -Each thinking, review, or termination worker must surface one compact free-form reasoning-discipline note in `SshxResultEnvelope.conclusion` naming the reference frame, stating the known-good shape and alignment, deviation, or revision status; stating the aesthetic verdict (美不美) with the specific ugly defect and beautiful form, or `no material defect found`, for each candidate materially weighed; stating the verified-premise or `ASSUMED-UNVERIFIED` status needed for the verdict; and naming any depth-bound stop that settled a judgment. This does not override `GoalArtifact`, assigned bias or review focus, truth tables, or allowed verdict sets. +Each thinking, review, or termination worker must surface one compact free-form reasoning-discipline note in `SshxResultEnvelope.conclusion` naming the reference frame, stating the known-good shape and alignment, deviation, or revision status; stating the aesthetic verdict (美不美) with the specific ugly defect and beautiful form, or `no material defect found`, for each candidate materially weighed; stating the verified-premise or `ASSUMED-UNVERIFIED` status needed for the verdict; and naming any depth-bound stop that settled a judgment. This never overrides `GoalArtifact`, bias/focus, truth tables or verdict sets. ## Thinking Panel -Protocol policy, not a mathematical consequence: run six whole-picture philosopher seats before choosing a plan — the same universal judgment lenses the consensus engine debates with. Each seat is one independent, context-isolated perspective that attacks from its own objective; the seats can and do disagree, and the meta-judge converges them: +Protocol policy, not a mathematical consequence: run six whole-picture philosopher seats before choosing a plan, with distinct objectives and independent, isolated context. They may disagree; meta-judge converges their judgments: - `teleology`: purpose and inevitability. What is this for, and is the form forced by that purpose? Attacks skipped-purpose and missing-inevitability. - `parsimony`: economy. Delete until nothing is left to delete; every element must prove its right to exist. Attacks magic numbers, symptom branches, and machinery that has not earned its place. @@ -233,9 +226,9 @@ Protocol policy, not a mathematical consequence: run six whole-picture philosoph - `proportional-containment`: locus dyad, containment pole. How far may this intervention rightfully bind, across scope, authority, and duration, given the evidence? Attacks over-hoisting, speculative abstraction, and turning a local fact into universal law. - `worth` (值不值 — is it worth it?): decision value. Compare doing nothing and the cheapest sufficient alternative; weigh incremental expected benefit toward `GoalArtifact` against total lifecycle cost — build and verification effort, recurring maintenance, complexity debt, failure and misuse risk, reversibility, delay, and opportunity cost. Include the work target's latency, throughput, and resource use when material to `GoalArtifact`. Attacks not-worth-it machinery, unneeded elegance, and cost that outruns benefit; it may reject a candidate every other seat finds beautiful and well-owned. It must not cut a capability `GoalArtifact.success_criteria` requires to save cost; state its best counterfactual and decisive cost/benefit assumption without fabricating numeric ROI. -`natural-ownership` and `proportional-containment` are a coupled **must-clash locus dyad**: they run together, each must answer the other pole's claim, and they converge on the natural owner layer — not the highest layer imaginable. Ownership pulls the fix toward the layer that owns the invariant; containment resists over-reaching past it. This is the "go upstream to the root, but not past the natural owner" balance expressed as two adversarial seats the meta-judge converges, rather than a single balanced checklist. +`natural-ownership` and `proportional-containment` are a coupled **must-clash locus dyad**: run together, each answers the other pole, converging on the natural owner layer, not the highest imaginable. Ownership pulls toward the invariant owner; containment resists overreach: "go upstream to the root, but not past the natural owner" is two adversarial seats for meta-judge convergence, not one balanced checklist. -`worth` (值不值) is an independent objective, not the aesthetic lens repeated: `parsimony` asks how much mechanism, `proportional-containment` asks where and how far it binds, and `worth` asks whether to pay for this at all, at this cost, now, versus the best alternative. A candidate can be minimal, beautiful, and properly contained yet still not worth doing, and a less minimal candidate can still be worth doing when the avoided downside justifies it. Because it is a seat rather than a cross-cutting lens, `worth` is judged once by its own perspective, so the panel is not homogenized into every seat re-deriving the same value verdict. +`worth` (值不值) is independent of aesthetics: `parsimony` asks how much mechanism, `proportional-containment` where/how far, `worth` whether to pay this cost now versus the best alternative. Minimal, beautiful, contained work may be unworthy; less minimal work may justify its cost. Only its own seat derives this verdict, preserving distinct objectives. Before proposing, revising, rejecting, or abstaining, each seat must apply `## Reasoning Discipline` to every candidate conclusion it weighs and surface the compact reasoning-discipline note in `SshxResultEnvelope.conclusion` before returning a verdict. @@ -269,15 +262,15 @@ The meta-judge applies this fixed thinking truth table: An `implement` exit requires the concrete plan to be both beautiful (per the `## Reasoning Discipline` aesthetic verdict) and worth its cost (per the `worth` seat). A concrete plan that fails the 值不值 (worth) judgment is an unclosed `GoalArtifact` goal gap: before `implement` the meta-judge must rebut the `worth` seat's factual premises, choose a cheaper sufficient alternative, show the omitted benefit clears the goal threshold, or record an explicit owner-level acceptance of the cost — otherwise the exit stays `meta-layer convergence` or `abstain/escalate with options`, never `implement`. Beauty and worth are a conditional challenge, not a forced clash: when the beautiful form carries a material elegance premium over the cheapest sufficient form, `worth` must justify or reject that premium; when `worth` prefers a cheaper, uglier form, the meta-judge records the accepted debt with its owner, containment boundary, and removal or expiry condition, since `temporary` without an expiry condition is not acceptable. -An `implement` exit also requires no unresolved harness overlap or authority gap. A goal and its harness mismatch when it presupposes missing host/controller execution capability or asks the skill to repeat a capability already declared by the harness; the skill's own judgment responsibilities are not a mismatch. Route a mismatch as a goal gap to the maintainer rather than implementing it. +An `implement` exit requires no unresolved harness overlap/authority gap: missing host/controller execution or repeating a provided capability is a mismatch; skill judgment duties are not. Route mismatches as goal gaps to the maintainer. At this existing `meta_judge` implement-exit gate, reflect on whether the goal or harness changed and whether current evidence has overturned the direction. Emit exactly one concrete action with its responsible party: `continue`, `revise`, `stop`, or `escalate`. -When a seat's `SshxResultEnvelope.conclusion` records both a dedicated-domain objection and its falsifiable causal prediction, and the meta-judge's proposed convergence has not refuted that causal chain, the meta-judge must run a `FocusedRound` before converging, provided the objection passes `BlockingAuthority`. An advisory objection does not trigger a `FocusedRound`; for this prerequisite, the meta-judge checks only whether the seat named both conjuncts and must not assess their persuasiveness. An objection that named a basis whose correctness is disputed still triggers the round because disputed is not absent. When the meta-judge declines a round on this ground, it records that decline in the existing `finding_downgrades` record under the same own-words requirement that governs downgrades. The three conditions must all hold simultaneously: the objection recorded in that conclusion is in that seat's exclusive domain (for example, mechanism necessity for `parsimony`, purpose-forced form for `teleology`, or cost worth for `worth`); the causal prediction recorded in that conclusion is falsifiable rather than a preference; and the meta-judge's proposed convergence has not answered that causal chain, including when it answers only a secondary point. In the focused round, all seats independently answer one question: "Does this causal chain hold, and if it does, how should the plan change?" The round preserves `## No Context Pollution`. +When a seat's `SshxResultEnvelope.conclusion` records both a dedicated-domain objection and its falsifiable causal prediction, and the meta-judge's proposed convergence has not refuted that causal chain, the meta-judge must run a `FocusedRound` before converging, provided the objection passes `BlockingAuthority`. An advisory objection does not trigger a `FocusedRound`; after admission checks, the meta-judge checks only whether both conjuncts are named, never their persuasiveness. An admitted confirmed basis disputed on correctness still triggers: disputed is not absent. When the meta-judge declines a round on this ground, it records that decline in the existing `finding_downgrades` record under the same own-words requirement that governs downgrades. The three conditions must all hold simultaneously: the objection recorded in that conclusion is in that seat's exclusive domain (for example, mechanism necessity for `parsimony`, purpose-forced form for `teleology`, or cost worth for `worth`); the causal prediction recorded in that conclusion is falsifiable rather than a preference; and the meta-judge's proposed convergence has not answered that causal chain, including when it answers only a secondary point. In the focused round, all seats independently answer one question: "Does this causal chain hold, and if it does, how should the plan change?" The round preserves `## No Context Pollution`. A causal chain triggers at most one focused round. If disagreement on that chain remains afterward, escalate to the maintainer rather than run it again. A later round is a genuine reopening only when independently changed sealed inputs — external new evidence, or an authorized `GoalArtifact` or harness correction, but never conclusions generated by the completed round itself — create a different grounded obligation. Replaying the same causal chain cannot reopen. The meta-judge records every grounded conflict and its resolution; presentation format is non-normative, and only an unresolved grounded conflict blocks `implement`. -An objection that fails `BlockingAuthority` is not an unclosed `GoalArtifact` goal gap and does not by itself hold the exit out of `implement`: the meta-judge records it as advisory in the existing `finding_downgrades` record as `BlockingAuthority` requires. Disputed grounding stays blocking. This is not permission to set aside a reachable defect. +An objection that fails `BlockingAuthority` is not an unclosed `GoalArtifact` goal gap and does not by itself hold the exit out of `implement`: the meta-judge records it as advisory in the existing `finding_downgrades` record as `BlockingAuthority` requires. Admitted confirmed disputed grounding stays blocking. This is not permission to set aside a reachable defect. The convergence question must be "what still differs from `GoalArtifact`?" expressed against the fixed normalized goal, constraints, and success criteria. Do not generalize the convergence pass beyond that goal gap. @@ -285,7 +278,7 @@ Material comparison coordinates form a product preorder: one candidate dominates ## Implementation Worker -Thinking-gate approval binds outcomes, scope and requirements before implementation. Send goal, verifiable acceptance, authorized scope/prohibitions and grounded context/evidence. Workers inspect the target and choose mechanics; compliant alternatives alone are not deviations. No caller recipes (steps, code/pseudocode, structures or algorithms), even as consensus, acceptance or prohibitions. Preserve user/host technical requirements with their sources. Report goal, authority or constraint changes before acting via existing correction, direction and class gates. +Thinking approval binds outcomes/scope/requirements. Send goal, verifiable acceptance, scope/prohibitions and grounded evidence. Workers inspect and choose mechanics; compliant alternatives are not deviations. No caller recipes (steps, code/pseudocode, structures/algorithms), even as consensus/acceptance/prohibitions. Preserve sourced user/host requirements; report goal/authority/constraint changes before acting through existing correction/direction/class gates. Implementation must be delegated to a worker using the stage's default carrier under `WorkerDelegationContract`. No lifecycle authority is granted. Exchange the brief for `conclusion` (changed files, checks) and opaque `log_ref`. @@ -325,15 +318,17 @@ The meta-judge applies this fixed review truth table: Advisory comments do not count as approval. A reject blocks done until the issue is fixed or explicitly converted into a non-blocking advisory by a bounded review pass. -Every blocking finding must name both `BlockingAuthority` conjuncts under `## Reasoning Discipline` and its failure, omission or uncertainty class within the trust boundary. It must carry the fields required by `## Result Envelope`. A blocking finding that fails `ThreatEligibility` or `BlockingAuthority` is downgraded by the meta-judge to an advisory with its reason recorded, then the remaining verdicts are routed again. Downgrade records and disputed grounding follow `BlockingAuthority`. Downgrade is allowed only for threat-model ineligibility or an advisory input, never because a finding is inconvenient, expensive, or late, and never sets aside a reachable defect. Harness gaps and claim authority follow `## Goal Contract` without startup confirmation. +Every blocking finding must name both `BlockingAuthority` conjuncts under `## Reasoning Discipline` and its failure, omission or uncertainty class within the trust boundary. It must carry the fields required by `## Result Envelope`. A blocking finding that fails `ThreatEligibility` or `BlockingAuthority` is downgraded by the meta-judge to an advisory with its reason recorded, then the remaining verdicts are routed again. Downgrade records and disputed grounding follow `BlockingAuthority`. Downgrade is allowed only for threat-model ineligibility or an advisory input, never because a finding is inconvenient, expensive, or late, and never sets aside a reachable defect. Harness gaps and claim authority follow `## Goal Contract`, including its material owner-clarification rule. ## Fix Or Done Before each fix or repeated review pass, use the existing gate to ask whether the goal or harness changed and whether evidence overturned the direction; emit exactly one concrete `continue`, `revise`, `stop`, or `escalate` action and name its responsible party. When that gate weighs whether evidence has overturned the direction across repeated passes on the same blocking goal gap, distinguish evidence that the gap is reachable by the current approach from evidence that it is not. Consecutive passes without improvement are, alone, evidence of neither: they do not prove the current approach is exhausted, and they do not license further identical passes as progress. Evidenced unreachability by the current approach routes through the gate's existing `revise`, `stop`, or `escalate` actions rather than respending `pass_budget` on an unchanged approach. -For `fix`, freeze admitted repairs as a finite batch under `## Implementation Worker` handoff, allowance and evidence rules; include findings and failure evidence. Delegate the smallest changes for what still differs from `GoalArtifact`; open a `SshxWorkerFlightRecord` per assignment and stay orchestration-only for the repair. Complete the batch before its one mandatory rerun review triplet; a chunk boundary never starts formal review. When a pass carries more than one blocking goal gap, repair them in goal-primacy rank, so the main path is repaired first. At zero units under an explicit finite cap, start no new pass and report remaining blockers honestly; finish the already-paid batch including its review. +For `fix`, freeze only confirmed current-goal/contract defects admitted by `BlockingAuthority` as a finite repair batch under `## Implementation Worker` handoff, allowance and evidence rules; include findings and failure evidence. Delegate the smallest changes for what still differs from `GoalArtifact`; do not add a permission, approval, transaction or execution system from an advisory/conditional concern; open a `SshxWorkerFlightRecord` per assignment and stay orchestration-only for the repair. Complete the batch before its one mandatory rerun review triplet; a chunk boundary never starts formal review. When a pass carries more than one blocking goal gap, repair them in goal-primacy rank, so the main path is repaired first. At zero units under an explicit finite cap, start no new pass and report remaining blockers honestly; finish the already-paid batch including its review. + +Before dispatching a repair after two consecutive passes whose blocking findings name the same `GoalArtifact` term and evidenced family (the same failed property and causal mechanism, even with different `mechanism_family` wording), or after earlier recorded evidence shows that member-by-member enumeration leaves the property unsupported, the existing gate makes one class-level decision. Record the goal/property, authorized domain, family, coverage basis, action/owner and falsifiable validation in the existing conclusion. Repair dispatch requires the recorded family and a verified coverage basis under `## Reasoning Discipline`. A sound abstraction may cover an infinite domain with recorded admissible-input correspondence and a falsifiable invariant. Unknown family or coverage routes bounded investigation under the intake scope; no supported path means honest unresolved stop, with only actual product, governance, boundary or permission decisions routed to their owner. A new fixture, recurrence, zero usage, or exhausted budget alone cannot authorize a member patch or narrow the domain. Domain or criterion changes require the existing owner authorization and append-only revision. -Before dispatching a repair after two consecutive passes whose blocking findings name the same `GoalArtifact` term and `mechanism_family`, or after earlier recorded evidence shows that member-by-member enumeration leaves the property unsupported, the existing gate makes one class-level decision. Record the goal/property, authorized domain, family, coverage basis, action/owner and falsifiable validation in the existing conclusion. Repair dispatch requires the recorded family and a verified coverage basis under `## Reasoning Discipline`. A sound abstraction may cover an infinite domain with recorded admissible-input correspondence and a falsifiable invariant. Unknown family or coverage routes bounded investigation under the intake scope; no supported path means honest unresolved stop, with only actual product, governance, boundary or permission decisions routed to their owner. A new fixture, recurrence, zero usage, or exhausted budget cannot authorize a member patch or narrow the domain. Domain or criterion changes require the existing owner authorization and append-only revision. +After collection meta-judge records labels, property/cause, evidenced prior match/distinct cause; same location/predicate is insufficient and paraphrase creates no new family. Later briefs/`visible_inputs` carry settled prior summaries/coverage limits, never same-round output; findings address correspondence. Unresolved correspondence routes bounded class investigation before member repair. State-space coverage reports actual workflow-domain measurements (command/scope/counts), limits/unavailability and future-input derivations. Census alone proves no coverage/restriction; apply sourced owner policy, changing it only with owner authorization/revision. On every review pass after the initial implementation, the review triplet must list each defense or validation element added since the previous pass and apply the plan-element admission rule to it. An element that names neither the `GoalArtifact` term that demands it nor an existing consumer is an advisory deletion candidate and cannot remain the sole reason to continue fixing. @@ -384,7 +379,7 @@ For this table, unanimous `satisfied` means one valid `satisfied` result from ea Roster means the dispatch-time recorded named role identities; a named role present without a valid result remains in the roster as a missing result. -The meta-judge has no termination verdict of its own and must not convert `abstain` or missing or invalid worker output into permission to claim success. Each termination seat applies `BlockingAuthority` itself before returning. An `unsatisfied` that names both conjuncts keeps its full force and may never be converted into permission by calling it unpersuasive. An `unsatisfied` that names no `GoalArtifact` term is advisory exactly as under `## Review Truth Table`: the meta-judge records it in `finding_downgrades` as `BlockingAuthority` requires, re-dispatches that seat once on the same sealed candidate with that record in its brief as part of the same evaluation, and then evaluates the table on the returned results, treating a repeated `unsatisfied` that again names no `GoalArtifact` term as `abstain`. +The meta-judge has no termination verdict of its own and must not convert `abstain` or missing or invalid worker output into permission to claim success. Each termination seat applies `BlockingAuthority` itself before returning. An admitted confirmed `unsatisfied` that names both conjuncts keeps its full force and may never be converted into permission by calling it unpersuasive. An `unsatisfied` that names no `GoalArtifact` term is advisory exactly as under `## Review Truth Table`: the meta-judge records it in `finding_downgrades` as `BlockingAuthority` requires, re-dispatches that seat once on the same sealed candidate with that record in its brief as part of the same evaluation, and then evaluates the table on the returned results, treating a repeated `unsatisfied` that again names no `GoalArtifact` term as `abstain`. The `withhold claim; continue against the named goal gap` exit routes that gap according to `harness.decision_ownership`. Only a work-target engineering correction assigned to the existing engineering path re-enters the review-`fix` path in `## Fix Or Done`, where its repair and required rerun review triplet must finish before any new termination candidate. Only caller-owned orchestration remains with the authorized caller, and only new evidence from that owner may form a later candidate. A maintainer-owned product, governance, or boundary gap stops and escalates; any later routing requires a maintainer-authorized correction under `## Goal Contract`. Any gap whose declared owner does not match a route above stops and escalates to that declared owner; absent, ambiguous, or otherwise invalid ownership stops and escalates with the unresolved ownership gap. @@ -422,16 +417,17 @@ Allowed worker carriers are limited to `codex-cli`, `heca`, `nyxid-oracle`, and ## Baseline Failure Mode -Without this skill, lightweight high-risk decisions tend to regress to these source-owned classes: +Source-owned no-skill failure classes: -- fake consensus: self-application, pseudo-isolation, missing worker-mode declaration, or caller self-certification in place of the fixed thinking, review, and termination rosters; -- false grounding: unverified premises, retrospective fit, imagined relevance, or a mathematical name whose hypotheses the recorded mechanism state does not instantiate; -- rabbit-holing: blocking by default, peripheral detail, repeated unchanged work, finite case registers, procedural findings against the run's own records, or per-case diagnosis after one declared absorber already determines the goal-visible route; +- fake consensus: self-application, pseudo-isolation, undeclared worker mode, self-certification; +- false grounding: unverified premises, retrospective fit, imagined relevance; +- rabbit-holing: default blocking, peripheral/repeated work, case registers, procedural findings; - goal loss: 忘记目标 drift to an unranked target, 因小失大 a part served at the whole's cost, or 买椟还珠 form held above substance; -- wrong convergence: beauty without worth, scalarized incomparable candidates, path-dependent gain on non-additive coordinates, or spawn acknowledgments, budget and lifecycle milestones presented as completion; -- contaminated adjudication: same-round peer evidence, an out-of-prefix ledger event, or dependency-reaching evidence presented as independent; -- boundary drift: carrier diversity over-claims, improvised worker mechanics, or daemon, GitHub, git, label, and release orchestration for an inline decision. -- forced intake confirmation: routine harness or boundary details turned into a startup question instead of a recorded, source-backed engineering assumption. +- wrong convergence: beauty without worth, scalarized incomparability, non-additive path gain, false completion proxies; +- contaminated adjudication: peer/out-of-prefix/dependency-reaching evidence presented as independent; +- boundary drift: diversity overclaims, improvised mechanics, unauthorized lifecycle; +- forced intake confirmation: routine questions replacing sourced assumptions; +- scope expansion: risk activation, uncertain repairs, stale obligations after correction. ## Transcript Template @@ -445,7 +441,7 @@ worker_delegation: worker_mode_gate: resolved_before_any_worker_dispatch: seat_rotation: # per multi-seat stage: the drawn seat-to-carrier assignment - reason: + reason: # effective source/adoption limits and Heca policy worker_flights: # ordered SshxWorkerFlightRecord entries thinking_panel_workers: # protocol-policy six named stage records meta_judge: # stage record plus concrete_plan and finding_downgrades @@ -464,6 +460,6 @@ fix_or_done: The contract for this skill is verified by `skills/sshx/tests/test_sshx_contract.py`. -Before adding or changing this skill, record the no-skill failure mode as source-owned contract or test evidence. When a new failure case appears, prefer widening or verifying the absorber that already covers its class to adding another case entry: when a verified finite construction hypothesis applies, its register cannot be completed, while an open or infinite domain still needs a class-coverage basis; every entry added must be held true by every later change. Do not track runtime artifacts as published skill source. +Before adding or changing this skill, record the no-skill failure mode as source-owned contract or test evidence. For new failures prefer verifying/widening the class absorber over case entries: verified finite-construction hypotheses defeat register closure; open/infinite domains still need class coverage, and every added entry binds later changes. Do not track runtime artifacts as published skill source. Before publishing or changing a claim about an external carrier or tool capability, verify the exact composed workflow end to end with the real tool. Fake carriers may supplement deterministic contract tests but must not be the sole evidence for a supported capability; when real verification is unavailable, mark the claim ASSUMED-UNVERIFIED and do not expose it as a supported option. diff --git a/skills/sshx/formal/README.md b/skills/sshx/formal/README.md index 5dbba34c..49708ecd 100644 --- a/skills/sshx/formal/README.md +++ b/skills/sshx/formal/README.md @@ -173,8 +173,67 @@ notification before one-shot result collection; a confirmed own-agent stop can i record failure without collecting a result. A notification grants collection authority, not completion. This adds no runtime interface, host capability, worker-record field or budget. The seven stages and per-flight completion predicate are unchanged. Batch progress is a -formal projection of existing worker conclusions, not a runtime scheduler. Trigger-aware -downgrade and plan admission retain the existing contextual evidence chain. +formal projection of existing worker conclusions, not a runtime scheduler. + +`DecisionBasis` retains `Input` and `TriggerRecord` together. `completeAdmission` +combines the named-conjunct/evidence-status/goal-basis force with the existing +workflow and sourced-owner trigger check. Review downgrade, plan admission, +generic admissibility/sole-basis questions, focused rounds and decline records, +goal-gap/convergence scope, blocking-finding well-formedness, residual differences +and termination-seat settlement all consume that judgment. Downgrade records +retain the original words and trigger decision. `force` alone remains a partial +conjunct judgment, never a complete blocking decision. + +`failed_trigger_rejected_by_every_consumer` checks the twenty existing decisions +for every supplied input with a failed trigger, independently of prose labels; +`admitted_basis_retained_by_every_consumer` retains every admitted basis that +requires neither trusted malice nor an owner decision. +Nine constructed evidence classes check the same decisions in both directions: +manual/fixture-only and sourced owner-restricted bases are refused; confirmed +ordinary workflow derivations, observed authorized inputs and independent +occurrences remain admitted. This is semantic model evidence in addition to +lexical clause traces. Provenance, workflow correspondence, confirmed status +and owner authority remain supplied premises; fixtures are not host incidents. + +The issues #1071–#1074 projections keep source, admission and recurrence at their +existing owners. `EffectiveSourceEvidence` separates content identity, optional checkout +facts, manifest/release and session adoption; disk facts alone never prove adoption. +Current explicit Heca disable flows through existing `carrierEnabled` consumers for +open, delegated launch (including retry/resume) and fallback; an authorized append-only +correction preserves that disable over stale exposure/opt-in evidence. Composition +uses the same current availability. These are interpreted policy/source premises, +not live Heca probes or a host cache detector. + +`TriggerRecord` requires `WorkflowInputEvidence` and `OwnerAdmissionPolicy`. +`triggerCheck`, the actual `downgrade`/`routeFindings` path and `planElementAdmitted` +consume observed actual inputs or sourced workflow derivations, independent occurrence +and any sourced owner restriction. A manual/constructed fixture alone is insufficient; +a zero census does not exclude future ordinary workflow states without an authorized +restriction. Observation truth, workflow derivability, source scope, non-fixture status +and owner authority are hypotheses, not an English classifier or an environment census. +A nonempty source is required to construct an owner restriction; malformed unsourced +policy is an evidence/collection gap, never authority to downgrade an ordinary defect. +Typed required projections do not prove an arbitrary JSON finding is structurally valid. + +`FamilyCorrespondence` projects the existing `family_basis` with a typed `FamilyHistory`: +an evidenced reason new has no predecessor fields, while a prior comparison preserves +its original label, property/cause judgments and settled-prior premise. Both require +evidence and peer-free inputs. `classGateActive` and the production `guardPass` consume +that same correspondence. An evidenced first family can take the initial review's +ordinary repair without a predecessor or inactive class-coverage obligation; an +unresolved prior comparison still routes bounded investigation before member repair. +Verified paraphrase recurrence and earlier unsupported enumeration still require class +coverage, while distinct causes remain distinct. `FamilyEvidence.recordComplete` +requires verified input correspondence and reported measurement limits/unavailability. +The model does not infer causal equivalence or complete domain coverage from a label, +location or measurement count. The new-family premise is interpreted evidence, not a +classifier or permission to relabel recurrence. Scenarios compose initial review, +first paid repair, whole-batch implementation and its included final review at zero +remaining budget, and distinguish unresolved comparisons at the same paid-pass consumer. +They also exercise the actual review/plan routes. Source-owned pre-fix compiled evidence +and the separately scoped real +Codex receipt-to-terminal proof live in `tests/test_sshx_contract.py`; simulated artifact +violations do not prove real compliance, timeout cause or filesystem isolation. The Codex identity adapter in `Clauses/Delegation.lean` pairs the protocol flight with pending or bound runner identity. The protocol's zero-based `attempt` counts consumed @@ -188,6 +247,31 @@ public record fields. Byte-level ID allocation, receipt ordering/delivery, path isolation, and batch recovery are behavior-tested in the scripts, not claimed as consequences of the abstract model. +The #1075 projections use the existing intake/admission/correction consumers. +`guardWriteGoal` consumes sourced `ActivationAuthority`: explicit consensus/multi-angle/ +delegated-review request or an applicable host mandate. Risk alone supplies neither. +Routine questions remain refused; a material owner question can be resolved before +its dependent intake is admitted. `Input.evidenceStatus` defaults to unverified and +`userGoalBasis` to empty. `force`, `downgrade`, `planElementAdmitted` and the actual +`guardPass` repair route require confirmed current-goal/contract evidence; repair plans +carry their admitted findings. An owner-decision requirement prevents automatic repair, +including when a confirmed goal gap still needs a product/permission decision. +Classification, sourced goal correspondence and owner authority remain interpreted +premises; this is no English classifier, runtime validator or new approval mechanism. + +An authorized revision's dependency projection revokes its dependent candidate batch +immediately and routes that scope back through design. It retains the flight/revision +history, pass allowance and unrelated evidence. `currentWorkStart` is a ghost cutoff +from that revision, not a runtime field: superseded pending/retry/fallback work cannot +launch; old completion cannot restore candidate readiness. Pending unlaunched work has +no host job to protect. Launched jobs remain protected through actual completion or +confirmed teardown; invalidation never manufactures terminal evidence. Correction +scenarios exercise the real consumers before dispatch, during an active job, after +implementation and after review, alongside unaffected-note preservation. Goal-scope invalidation advances the existing claim-authority ledger position even +when the host continuation declaration stays identical. Historical verdict/snapshot +remain recorded; stale evidence cannot be re-evaluated or reused for a later claim. The model does not prove a +host can cancel a running job or that a new plan's English follows the corrected goal. + ## What the model cannot verify The implementation/repair handoff in `Clauses/Contract.lean` projects the approved diff --git a/skills/sshx/formal/Sshx/Behavior/Invariant.lean b/skills/sshx/formal/Sshx/Behavior/Invariant.lean index 74978121..74753522 100644 --- a/skills/sshx/formal/Sshx/Behavior/Invariant.lean +++ b/skills/sshx/formal/Sshx/Behavior/Invariant.lean @@ -25,7 +25,7 @@ theorem never_poll (s : ProtocolState) (id : Nat) : ¬ allowed s (.pollArtifacts theorem never_lifecycle (s : ProtocolState) (op : LifecycleOp) : ¬ allowed s (.lifecycle op) := fun h => h --- SKILL[inv]: "Logs are not inline in caller context." +-- SKILL[inv]: "never inline logs" theorem never_carry_full_log (s : ProtocolState) (id : Nat) : ¬ allowed s (.carry (.fullLog id)) := by simp [allowed, guardCarry, ContextItem.permitted] @@ -325,7 +325,7 @@ theorem attempt_le_retry_budget {s : ProtocolState} (h : Reachable s) (f : Fligh (hf : f ∈ s.flights) : f.attempt ≤ f.retryBudget := (safe_of_reachable h).attemptLeBudget f hf --- SKILL[inv]: "Final reports aggregate `conclusion` values only and retain `log_ref` references for optional inspection." +-- SKILL[inv]: "Final reports aggregate only `conclusion` and opaque `log_ref`" theorem context_only_permitted {s : ProtocolState} (h : Reachable s) (item : ContextItem) (hi : item ∈ s.context) : item.permitted = true := (safe_of_reachable h).contextPermitted item hi @@ -379,9 +379,11 @@ def Stage.index : Stage → Nat | .fixOrDone => 6 -- SKILL[inv]: "A thinking-stage exhaustion in particular skips `meta_judge`, `implementation_worker`, `review_triplet_workers`, and `fix_or_done`." -theorem stage_never_regresses (s : ProtocolState) (a : Action) : +theorem stage_monotone_without_scope_correction (s : ProtocolState) (a : Action) + (hcorrection : ∀ r e, a = .appendRevision r e → e.invalidatesWork = false) : Stage.index s.stage ≤ Stage.index (step s a).stage := by cases a + case appendRevision r e => simp [step, hcorrection r e rfl] case advanceStage => simp only [step] cases s.stage <;> simp [Stage.next, Stage.index] @@ -435,15 +437,19 @@ of applicability values. -/ theorem authority_change_requires_correction (s : ProtocolState) (a : Action) (hg : s.goalWritten) (ha : allowed s a) (hc : (step s a).continuationAuthority ≠ s.continuationAuthority) : - ∃ r e source, a = .appendRevision r e ∧ e.valid r ∧ e.continuation = some source := by + ∃ r e, a = .appendRevision r e ∧ e.valid r ∧ + (e.continuation.isSome = true ∨ e.invalidatesWork = true) := by cases a case writeGoal g e => have hn : s.goal = none := ha.2.1 simp [ProtocolState.goalWritten, hn] at hg case appendRevision r e => cases he : e.continuation with - | none => simp [step, ProtocolState.correctedAuthority, he] at hc - | some source => exact ⟨r, e, source, rfl, ha.2, he⟩ + | none => + have changed : e.invalidatesWork = true := by + cases hw : e.invalidatesWork <;> simp_all [step, ProtocolState.correctedAuthority] + exact ⟨r, e, rfl, ha.2, Or.inr changed⟩ + | some source => exact ⟨r, e, rfl, ha.2, Or.inl (by simp [he])⟩ case fallbackFlight id carrier => simp only [step] at hc split at hc <;> exact (hc rfl).elim @@ -476,8 +482,10 @@ theorem authority_revision_in_ledger {s : ProtocolState} (h : Reachable s) : have hi := ih g hg cases he : e.continuation with | none => - simpa [step, ProtocolState.correctedAuthority, he, hg, GoalArtifact.correct] - using Nat.le_succ_of_le hi + cases hw : e.invalidatesWork + · simpa [step, ProtocolState.correctedAuthority, he, hw, hg, GoalArtifact.correct] + using Nat.le_succ_of_le hi + · simp [step, ProtocolState.correctedAuthority, he, hw, hg, GoalArtifact.correct] | some source => simp [step, ProtocolState.correctedAuthority, he, hg, GoalArtifact.correct] case fallbackFlight id carrier => @@ -561,11 +569,11 @@ theorem correction_rejects_prior_evidence {s : ProtocolState} (h : Reachable s) /-- An unrelated revision keeps the same admission rule, so usable evidence is not invalidated merely because the overall revision ledger grew. -/ theorem unrelated_revision_preserves_evaluation (s : ProtocolState) (r : Revision) - (re : RevisionEvidence) (hn : re.continuation = none) + (re : RevisionEvidence) (hn : re.continuation = none) (hw : re.invalidatesWork = false) (source : ClaimSource) (e : TerminationEvidence) : allowed (step s (.appendRevision r re)) (.evaluateTermination source e) ↔ allowed s (.evaluateTermination source e) := by - simp [allowed, guardEvaluateTermination, step, ProtocolState.correctedAuthority, hn, + simp [allowed, guardEvaluateTermination, step, ProtocolState.correctedAuthority, hn, hw, ProtocolState.gate, ProtocolState.reviewComplete, ProtocolState.reviewReady, ProtocolState.batchSettled, ProtocolState.batchFlights, ProtocolState.attemptSettled, ProtocolState.housekeepingFor, ProtocolState.allHecaHousekeepingSettled] @@ -632,13 +640,28 @@ theorem fallback_decreases_remaining (s : ProtocolState) (id : Nat) (c : Carrier ∃ f, s.flight id = some f ∧ ((step s (.fallbackFlight id c)).triedCarriers f.assignment).remaining < (s.triedCarriers f.assignment).remaining := by - obtain ⟨f, hf, _, _, hn⟩ := ha + obtain ⟨f, hf, _, _, _, hn⟩ := ha refine ⟨f, hf, ?_⟩ rw [fallback_records_tried s id c f hf] exact remaining_insert_lt _ (CarrierSet.mem_univ _) c (Carrier.mem_univ c) (nextCarrier_untried _ (CarrierSet.mem_univ _) _ (CarrierSet.mem_univ _) c (Carrier.mem_univ c) hn) +/-- Current disable is consumed even if old capability records still contain Heca. -/ +theorem disabled_heca_cannot_open (s : ProtocolState) (stage : FlightStage) (role : Role) + (target : String) (retries : Nat) (hd : s.hecaDisabled = true) : + ¬ allowed s (.openFlight stage role .heca target retries) := by + simp [allowed, guardOpenFlight, ProtocolState.carrierEnabled, hd] + +theorem disabled_heca_cannot_fallback (s : ProtocolState) (id : Nat) + (hd : s.hecaDisabled = true) : ¬ allowed s (.fallbackFlight id .heca) := by + intro h + obtain ⟨f, _, _, _, _, hn⟩ := h + have eligible := nextCarrier_eligible _ (CarrierSet.mem_univ _) _ (CarrierSet.mem_univ _) + .heca (Carrier.mem_univ .heca) hn + simpa [ProtocolState.eligibleCarriers, ProtocolState.carrierEnabled, CarrierSet.get, hd] + using eligible + /-- Review dispatch and fallback both apply the existing executable-carrier restriction. -/ theorem tests_dispatch_excludes_oracle (s : ProtocolState) (target : String) (retries : Nat) : ¬ allowed s (.openFlight .review .tests .nyxidOracle target retries) := by @@ -648,7 +671,7 @@ theorem tests_fallback_excludes_oracle (s : ProtocolState) (id : Nat) (f : Fligh (hf : s.flight id = some f) (hs : f.stage = .review) (hr : f.role = .tests) : ¬ allowed s (.fallbackFlight id .nyxidOracle) := by intro ha - obtain ⟨g, hg, _, _, hn⟩ := ha + obtain ⟨g, hg, _, _, _, hn⟩ := ha have heq : g = f := Option.some.inj (hg.symm.trans hf) subst g have eligible := nextCarrier_eligible _ (CarrierSet.mem_univ _) _ (CarrierSet.mem_univ _) diff --git a/skills/sshx/formal/Sshx/Behavior/Model.lean b/skills/sshx/formal/Sshx/Behavior/Model.lean index 35ebad4b..89002e30 100644 --- a/skills/sshx/formal/Sshx/Behavior/Model.lean +++ b/skills/sshx/formal/Sshx/Behavior/Model.lean @@ -114,12 +114,17 @@ structure IntakeEvidence where inventedAuthority : Bool startupQuestionAsked : Bool continuation : ContinuationEntry + activation : ActivationAuthority := .absent + materialOwnerQuestion : Bool := false + ownerClarified : Bool := false deriving DecidableEq, Repr +-- SKILL[ref]: "At intake, preserve sourced owner blocking restrictions, scope and meaning in `constraints` and `harness.trust_boundary`, hence every brief/retry/repair/resume; issue proposals and censuses create no owner policy." def IntakeEvidence.complete (e : IntakeEvidence) : Prop := e.sources ≠ [] ∧ e.assumptionsLabeled = true ∧ e.minimalTaskRelevantScope = true ∧ e.explicitBoundariesPreserved = true ∧ - e.inventedAuthority = false ∧ e.startupQuestionAsked = false + e.inventedAuthority = false ∧ e.activation.authorized = true ∧ + (e.startupQuestionAsked = false ∨ (e.materialOwnerQuestion = true ∧ e.ownerClarified = true)) /-- Current semantic projection of `harness.provided_capabilities`, supplied as evidence. The model does not parse English to establish correspondence or owner authority. -/ @@ -151,6 +156,9 @@ structure RevisionEvidence where ownerAuthorized : Bool sourceSupported : Bool continuation : Option ContinuationSource + hecaDisableCorrection : Bool := false + /-- Interpreted dependency on the corrected scope; unrelated notes leave work usable. -/ + invalidatesWork : Bool := false deriving DecidableEq, Repr def RevisionEvidence.valid (e : RevisionEvidence) (r : Revision) : Prop := @@ -178,12 +186,18 @@ structure HousekeepingRec where structure ImplementationPlan where obligations : List String flightAllowance : Nat + repairFindings : List Finding := [] deriving DecidableEq, Repr -- SKILL[def]: "Predeclare finite assignments and allowance in the approved plan's conclusion." def ImplementationPlan.valid (p : ImplementationPlan) : Prop := p.obligations ≠ [] ∧ 0 < p.flightAllowance +-- SKILL[ref]: "For `fix`, freeze only confirmed current-goal/contract defects admitted by `BlockingAuthority` as a finite repair batch" +def ImplementationPlan.repairsAdmitted (p : ImplementationPlan) : Bool := + !p.repairFindings.isEmpty && p.repairFindings.all fun f => + downgrade f == .reject && !f.requiresOwnerDecision + /-- Ghost projection of accumulated worker conclusions. `firstFlight` scopes the current candidate; it is also reset for an explicitly budgeted repeated review. -/ structure ImplementationBatch where @@ -204,6 +218,10 @@ structure ProtocolState where capabilityChecked : List Carrier /-- Once-per-run heca check, including a negative result; a ghost transcript projection. -/ hecaCheckRecorded : Bool := false + /-- Current explicit disable, including an authorized correction; never a new capability probe. -/ + hecaDisabled : Bool := false + /-- Ghost cutoff for flights superseded by a correction, not a new runtime field. -/ + currentWorkStart : Nat := 0 flights : List FlightRec context : List ContextItem passBudget : Option Nat @@ -285,11 +303,19 @@ def ProtocolState.gate (s : ProtocolState) : Applicability := def ProtocolState.correctedAuthority (s : ProtocolState) (e : RevisionEvidence) : ContinuationAuthority := match e.continuation with - | none => s.continuationAuthority + | none => if e.invalidatesWork then + ⟨s.continuationAuthority.source, (s.goal.map (·.revisions.length)).getD 0 + 1⟩ + else s.continuationAuthority | some source => ⟨source, (s.goal.map (·.revisions.length)).getD 0 + 1⟩ +/-- Cancelled pending work has no host job; launched work retains protection until +terminal observation/confirmed teardown, even after its authority is superseded. -/ +def ProtocolState.flightProtected (s : ProtocolState) (f : FlightRec) : Bool := + f.active && (f.launched || decide (s.currentWorkStart ≤ f.id)) + +-- SKILL[ref]: "Active jobs stay protected until host completion/confirmed teardown" def ProtocolState.activeOn (s : ProtocolState) (target : String) : Bool := - s.flights.any fun f => f.target == target && f.active + s.flights.any fun f => f.target == target && s.flightProtected f def ProtocolState.flight (s : ProtocolState) (id : Nat) : Option FlightRec := s.flights.find? fun f => f.id == id @@ -435,7 +461,8 @@ def guardReviewFlight (s : ProtocolState) (role : Role) (carrier : Carrier) : Pr def guardInspect (s : ProtocolState) : Prop := s.stage = .intake -- SKILL[guard]: "During `intake`, the caller resolves them from current user input, repository rules, existing authorizations, and available execution context, recording sources and explicitly labelling minimal engineering assumptions." --- SKILL[guard]: "It must not ask a startup boundary or harness confirmation question." +-- SKILL[guard]: "It must not ask a routine startup boundary or harness confirmation question." +-- SKILL[ref]: "Ask the declared owner about uncertain material product/architecture/permission semantics before dependent changes" -- SKILL[guard]: "Explicit user boundaries and permission decisions remain authoritative; routine missing detail is resolved with the smallest task-relevant assumption." -- SKILL[guard]: "The boundary owner may declare a host-provided goal-driven continuation mechanism only in `harness.provided_capabilities`; the skill must not discover or infer an external mechanism." -- SKILL[guard]: "`GoalArtifact` is written during `intake` before worker mode selection or any worker dispatch." @@ -460,9 +487,16 @@ def guardResolveMode (s : ProtocolState) (m : WorkerMode) : Prop := Carrier.codexCli ∈ s.capabilityChecked ∧ s.hecaCheckRecorded = true ∧ (m = .abstain ∨ ∃ c, m = .carrier c ∧ c ∈ s.capabilityChecked) +/-- All dispatch consumers share current enablement; stale capability exposure cannot +restore authority after an explicit disable. Existing running-agent recovery is unchanged. -/ +-- SKILL[guard]: "Explicit user disable overrides host opt-in, tools and stale availability on initial/single dispatch, retry, fallback, repair and resume; reuse this rule." +-- SKILL[ref]: "Record disable corrections in gate evidence/revisions without re-probing." +def ProtocolState.carrierEnabled (s : ProtocolState) (c : Carrier) : Bool := + s.capabilityChecked.contains c && !(c == .heca && s.hecaDisabled) + -- SKILL[guard]: "`WorkerModeGate` requires resolution before dispatch." def guardOpenFlight (s : ProtocolState) (stage : FlightStage) (role : Role) (carrier : Carrier) : Prop := - s.modeResolved ∧ ¬ s.abstained ∧ carrier ∈ s.capabilityChecked ∧ + s.modeResolved ∧ ¬ s.abstained ∧ s.carrierEnabled carrier = true ∧ match stage with | .implementation => role = .implementation ∧ guardImplementationFlight s | .review => guardReviewFlight s role carrier @@ -476,15 +510,15 @@ def guardOpenFlight (s : ProtocolState) (stage : FlightStage) (role : Role) (car -- SKILL[guard]: "Use `skills/sshx/scripts/run-codex-worker.sh` for every `codex-cli` launch and `skills/sshx/scripts/run-oracle-worker.py` for every `nyxid-oracle` launch." def guardLaunchViaRunner (s : ProtocolState) (id : Nat) : Prop := - ∃ f, s.flight id = some f ∧ f.launched = false ∧ + ∃ f, s.flight id = some f ∧ f.launched = false ∧ s.currentWorkStart ≤ f.id ∧ (runnerFor f.carrier).isSome = true /-- Host tool invocation for heca MCP or isolated subagent; no runner identity or paths. Carrier-specific isolation and heca evidence remain interpreted contract premises. -/ def guardLaunchDelegated (s : ProtocolState) (id : Nat) : Prop := - ∃ f, s.flight id = some f ∧ f.launched = false ∧ + ∃ f, s.flight id = some f ∧ f.launched = false ∧ s.currentWorkStart ≤ f.id ∧ s.attemptSettled f = true ∧ - runnerFor f.carrier = none + s.carrierEnabled f.carrier = true ∧ runnerFor f.carrier = none -- SKILL[guard]: "caller shell `&` is forbidden: detachment risks untracked init-adopted workers without notice." def guardNoShellBackground : Prop := False @@ -526,7 +560,7 @@ def ProtocolState.triedCarriers (s : ProtocolState) (assignment : Nat) : Carrier /-- Capability availability and the same per-seat restriction used at review admission. -/ def ProtocolState.eligibleCarriers (s : ProtocolState) (f : FlightRec) : CarrierSet := - let eligible := fun c => s.capabilityChecked.contains c && + let eligible := fun c => s.carrierEnabled c && (f.stage != .review || seatEligible f.role c) ⟨eligible .codexCli, eligible .heca, eligible .nyxidOracle, eligible .isolatedTokenSubagent⟩ @@ -534,7 +568,7 @@ def ProtocolState.eligibleCarriers (s : ProtocolState) (f : FlightRec) : Carrier /-- A replacement uses the existing finite selector for the entire failed assignment. An active or successful replacement closes fallback through any earlier flight id. -/ def guardFallback (s : ProtocolState) (id : Nat) (carrier : Carrier) : Prop := - ∃ f, s.flight id = some f ∧ f.status = .abstained ∧ + ∃ f, s.flight id = some f ∧ f.status = .abstained ∧ s.currentWorkStart ≤ f.id ∧ (s.flights.filter fun g => g.assignment == f.assignment).all (fun g => g.status == .abstained ∧ s.attemptSettled g = true) = true ∧ nextCarrier (s.eligibleCarriers f) (s.triedCarriers f.assignment) = some carrier @@ -567,18 +601,18 @@ def passContinuationAllowed (budget : Option Nat) (directionGate : Bool) : Bool | some remaining => directionGate && remaining > 0 -- SKILL[guard]: "The batch debit includes all bounded assignments and final review even at zero remaining units, with no subsequent pass authority under that finite cap." --- SKILL[guard]: "For `fix`, freeze admitted repairs as a finite batch under `## Implementation Worker` handoff, allowance and evidence rules;" +-- SKILL[guard]: "under `## Implementation Worker` handoff, allowance and evidence rules;" def guardPass (s : ProtocolState) (t : Transition) (e : Reasoning.FamilyEvidence) (plan : Option ImplementationPlan) : Prop := s.stage = .fixOrDone ∧ Reasoning.familyPassAllowed e t = true ∧ s.reviewComplete = true ∧ t ≠ .initialReviewTriplet ∧ (t.counted = true → s.passBudget = none ∨ ∃ b, s.passBudget = some b ∧ 0 < b) ∧ - (if t = .repairWithRerunReview then ∃ p, plan = some p ∧ p.valid else plan = none) + (if t = .repairWithRerunReview then ∃ p, plan = some p ∧ p.valid ∧ p.repairsAdmitted = true else plan = none) def guardAdvanceStage (s : ProtocolState) : Prop := s.stage.next.isSome = true ∧ (if s.stage = .intake then s.goalWritten else s.modeResolved ∧ ¬ s.abstained) ∧ - s.flights.all (fun f => !f.active) = true ∧ s.allHecaHousekeepingSettled = true ∧ + s.flights.all (fun f => !s.flightProtected f) = true ∧ s.allHecaHousekeepingSettled = true ∧ (s.stage = .implementation → s.reviewReady = true) ∧ (s.stage = .reviewTriplet → s.reviewComplete = true) @@ -631,6 +665,16 @@ def allowed (s : ProtocolState) : Action → Prop -- SKILL[ref]: "Include any non-blocking advisory feedback without inlining logs." abbrev advisoryWithoutLogs := @ContextItem.permitted +-- SKILL[ref]: "Confirmed means an evidenced current-goal/contract defect, including absent required evidence." +theorem unadmitted_repairs_cannot_pass (s : ProtocolState) (e : Reasoning.FamilyEvidence) + (p : ImplementationPlan) (h : p.repairsAdmitted = false) : + ¬ allowed s (.pass .repairWithRerunReview e (some p)) := by + intro ha + obtain ⟨_, _, _, _, _, q, hq, _, hadmit⟩ := ha + have hp : p = q := Option.some.inj hq + subst q + simp [h] at hadmit + -- SKILL[policy]: "Protocol policy, not a mathematical consequence: before the first pass after the initial review triplet, the caller may record one owner-precommitted finite integer `pass_budget`; by default it records no cap." abbrev passBudgetPrecommitment := @guardRecordPassBudget @@ -704,6 +748,7 @@ def reopenFlight (id : Nat) (carrier : Carrier) (f : FlightRec) : FlightRec := { f with id := id, carrier := carrier, status := .inFlight, attempt := 0, envelopeRef := none, sentinelRef := none, launched := false, notified := false } +-- SKILL[ref]: "Corrections immediately supersede dependent pending/active/completed plan/review/repair authority" def step (s : ProtocolState) : Action → ProtocolState | .inspectReadOnly => s | .writeGoal g e => @@ -714,11 +759,17 @@ def step (s : ProtocolState) : Action → ProtocolState | .appendRevision r e => { s with goal := s.goal.map (fun g => g.correct r), - continuationAuthority := s.correctedAuthority e } + continuationAuthority := s.correctedAuthority e, + hecaDisabled := s.hecaDisabled || e.hecaDisableCorrection, + currentWorkStart := if e.invalidatesWork then s.freshId else s.currentWorkStart, + batch := if e.invalidatesWork then none else s.batch, + stage := if e.invalidatesWork then .thinkingPanel else s.stage, + claimed := if e.invalidatesWork then false else s.claimed } | .capabilityCheck c => { s with capabilityChecked := c :: s.capabilityChecked } | .recordHecaCheck facts => { s with hecaCheckRecorded := true, + hecaDisabled := s.hecaDisabled || facts.explicitlyDisabled, capabilityChecked := if facts.detected then .heca :: s.capabilityChecked else s.capabilityChecked } | .resolveMode m => { s with mode := some m } | .openFlight stage role carrier target retryBudget => @@ -808,7 +859,7 @@ theorem archive_non_heca_refused (s : ProtocolState) (id : Nat) (f : FlightRec) theorem launch_requires_archive_after_collection (s : ProtocolState) (id : Nat) (f : FlightRec) (hf : s.flight id = some f) (_collected : s.attemptCollected f = true) (h : allowed s (.launchDelegated id)) : s.attemptSettled f = true := by - obtain ⟨g, hg, _, settled, _⟩ := h + obtain ⟨g, hg, _, _, settled, _⟩ := h have geq : g = f := Option.some.inj (hg.symm.trans hf) simpa [geq] using settled diff --git a/skills/sshx/formal/Sshx/Behavior/Scenarios.lean b/skills/sshx/formal/Sshx/Behavior/Scenarios.lean index dd723fc9..3e79a5fb 100644 --- a/skills/sshx/formal/Sshx/Behavior/Scenarios.lean +++ b/skills/sshx/formal/Sshx/Behavior/Scenarios.lean @@ -1,5 +1,7 @@ import Sshx.Behavior.Invariant import Sshx.Reasoning.Authority +import Sshx.Reasoning.Review +import Sshx.Reasoning.Termination import Sshx.Clauses.Delegation /-! @@ -16,14 +18,20 @@ private def goal : GoalArtifact := ⟨"repair", "correct ordinary use", [], ["verified"], "remaining gap?", ⟨["worker execution"], "non-malicious ordinary mistakes", "engineering owner"⟩, []⟩ private def intake (continuation : ContinuationEntry) : IntakeEvidence := - ⟨goal.harness, ["task", "repository rules"], true, true, true, false, false, continuation⟩ + ⟨goal.harness, ["task", "repository rules"], true, true, true, false, false, continuation, .hostMandate, false, false⟩ private def readyState : ProtocolState := { ProtocolState.initial with stage := .implementation, goal := some goal, mode := some (.carrier .codexCli), capabilityChecked := [.codexCli, .isolatedTokenSubagent], hecaCheckRecorded := true } -private def twoParts : ImplementationPlan := ⟨["contract", "verification"], 2⟩ +private def ordinary : Finding := + ⟨.reject, ⟨true, true, false, false, .confirmed, "goal S1 / existing contract source"⟩, false, + ⟨"ordinary typo", "user", .ordinaryOperation, "parsing", none, true, + ⟨none, "current parser input path", true⟩, .unrestricted, + ⟨"correct parsing", "ordinary parser typo", "new cause at initial review"⟩⟩, false⟩ + +private def twoParts : ImplementationPlan := ⟨["contract", "verification"], 2, [ordinary]⟩ private def begin := step readyState (.beginImplementation twoParts) private def opened := step begin (.openFlight .implementation .implementation .codexCli "target" 0) private def successful : Observation := ⟨true, true, true, true, true⟩ @@ -42,13 +50,13 @@ example : ¬ allowed partDone .advanceStage := by simp [allowed, guardAdvanceStage, partDone, returned, opened, begin, readyState, finish, step, updateFlight, collectEffect, done, successful, twoParts, ImplementationPlan.start, ProtocolState.initial, ProtocolState.reviewReady, ProtocolState.batchSettled, - ProtocolState.batchFlights, newFlight, ProtocolState.freshId, FlightRec.active, + ProtocolState.batchFlights, newFlight, ProtocolState.freshId, ProtocolState.flightProtected, FlightRec.active, ProtocolState.flight, ProtocolState.attemptSettled, ProtocolState.housekeepingFor, ProtocolState.allHecaHousekeepingSettled] -- The next approved assignment remains in implementation, with no review flight in between. example : allowed partDone (.openFlight .implementation .implementation .codexCli "target" 0) := by - simp [allowed, guardOpenFlight, guardImplementationFlight, ProtocolState.modeResolved, + simp [allowed, guardOpenFlight, ProtocolState.carrierEnabled, guardImplementationFlight, ProtocolState.modeResolved, ProtocolState.abstained, partDone, returned, opened, begin, readyState, finish, step, updateFlight, collectEffect, done, successful, twoParts, ImplementationPlan.start, ProtocolState.initial, ProtocolState.reviewStarted, ProtocolState.reviewReady, ProtocolState.batchSettled, ProtocolState.batchFlights, @@ -63,7 +71,7 @@ example : allowed complete .advanceStage := by readyState, finish, step, updateFlight, collectEffect, done, successful, twoParts, ImplementationPlan.start, ProtocolState.initial, ProtocolState.reviewReady, ProtocolState.batchSettled, ProtocolState.batchFlights, newFlight, ProtocolState.freshId, - FlightRec.active, Stage.next, ProtocolState.modeResolved, ProtocolState.abstained, + ProtocolState.flightProtected, FlightRec.active, Stage.next, ProtocolState.modeResolved, ProtocolState.abstained, ProtocolState.flight, ProtocolState.attemptSettled, ProtocolState.housekeepingFor, ProtocolState.allHecaHousekeepingSettled] @@ -73,11 +81,11 @@ private def quality := step architecture (.openFlight .review .quality .codexCli private def tests := step quality (.openFlight .review .tests .codexCli "target" 0) example : architecture.reviewReady = true := by decide example : allowed architecture (.openFlight .review .quality .codexCli "target" 0) := by - simp only [allowed, guardOpenFlight, guardReviewFlight, seatEligible, ProtocolState.modeResolved, + simp only [allowed, guardOpenFlight, ProtocolState.carrierEnabled, guardReviewFlight, seatEligible, ProtocolState.modeResolved, ProtocolState.abstained] decide example : allowed quality (.openFlight .review .tests .codexCli "target" 0) := by - simp only [allowed, guardOpenFlight, guardReviewFlight, seatEligible, canRunRepositoryCommands, ProtocolState.modeResolved, + simp only [allowed, guardOpenFlight, ProtocolState.carrierEnabled, guardReviewFlight, seatEligible, canRunRepositoryCommands, ProtocolState.modeResolved, ProtocolState.abstained] decide example : (tests.batchFlights.filter (fun f => f.stage == .review)).length = 3 := by decide @@ -89,9 +97,27 @@ example : reviewed.reviewComplete = true := by decide private def fix := step reviewed .advanceStage example : fix.stage = .fixOrDone := by decide +-- Initial-review evidence is shared by the review route and first-family repair. + +private def approval : Finding := { ordinary with verdict := .approve } + private def family : FamilyEvidence := ⟨"goal", "correct output", "ordinary inputs", "shared mechanism", "worker", "behavior check", - true, true, 2, false, .uniformInvariant true, false, false, false, false, none⟩ + true, ⟨"current paraphrase", "same property/cause evidence", true, + .priorComparison "prior label" true true true⟩, + 2, false, .uniformInvariant true, false, false, false, false, none, true, true⟩ + +-- The ordinary initial-review repair needs neither a predecessor nor class coverage. +private def firstFamily : FamilyEvidence := + { family with + property := ordinary.trigger.familyBasis.failedProperty + mechanismFamily := ordinary.trigger.mechanismFamily + sameGoalTerm := false + correspondence := ⟨ordinary.trigger.mechanismFamily, + ordinary.trigger.familyBasis.causalMechanism, true, + .newFamily ordinary.trigger.familyBasis.correspondenceEvidence⟩ + consecutivePasses := 1 + coverageBasis := .unknown } -- The default fix state carries no cap, so a direction-gated pass remains admissible -- and leaves the absent cap unchanged. @@ -101,20 +127,23 @@ example : allowed fix (.pass .repeatedReviewPass family none) := by have hr : fix.reviewComplete = true := by decide have hb : fix.passBudget = none := by decide simp [allowed, guardPass, hs, hr, hb, family, familyPassAllowed, familyRoute, - ownerAuthorizedDomainChange, classGateActive, FamilyEvidence.recordComplete, + ownerAuthorizedDomainChange, classGateActive, FamilyEvidence.recordComplete, FamilyCorrespondence.verified, FamilyCorrespondence.sameFamily, coverageBasisVerified, Transition.counted] private def defaultRepeated := step fix (.pass .repeatedReviewPass family none) example : defaultRepeated.passBudget = none := by decide private def funded := step fix (.recordPassBudget 1) -private def repair := step funded (.pass .repairWithRerunReview family (some twoParts)) -example : allowed funded (.pass .repairWithRerunReview family (some twoParts)) := by +private def repair := step funded (.pass .repairWithRerunReview firstFamily (some twoParts)) +private theorem firstRepairPassAdmitted : + allowed funded (.pass .repairWithRerunReview firstFamily (some twoParts)) := by have hs : funded.stage = .fixOrDone := by decide have hr : funded.reviewComplete = true := by decide have hb : funded.passBudget = some 1 := by decide - simp [allowed, guardPass, hs, hr, hb, family, familyPassAllowed, familyRoute, - ownerAuthorizedDomainChange, classGateActive, FamilyEvidence.recordComplete, - coverageBasisVerified, twoParts, ImplementationPlan.valid, Transition.counted] + simp [allowed, guardPass, hs, hr, hb, firstFamily, ordinary, family, familyPassAllowed, familyRoute, + ownerAuthorizedDomainChange, classGateActive, FamilyEvidence.recordComplete, FamilyCorrespondence.verified, FamilyCorrespondence.sameFamily, + coverageBasisVerified, twoParts, ImplementationPlan.valid, ImplementationPlan.repairsAdmitted, ordinary, downgrade, completeAdmission, eligible, triggerCheck, force, + WorkflowInputEvidence.ordinary, WorkflowInputEvidence.observed, occurrenceIsIndependent, + OwnerAdmissionPolicy.admits, Transition.counted] example : repair.passBudget = some 0 := by decide example : repair.stage = .fixOrDone := by decide private def repairedFirst := step (finish (step repair @@ -158,7 +187,7 @@ example : allowed funded (.pass .repeatedReviewPass family none) := by have hr : funded.reviewComplete = true := by decide have hb : funded.passBudget = some 1 := by decide simp [allowed, guardPass, hs, hr, hb, family, familyPassAllowed, familyRoute, - ownerAuthorizedDomainChange, classGateActive, FamilyEvidence.recordComplete, + ownerAuthorizedDomainChange, classGateActive, FamilyEvidence.recordComplete, FamilyCorrespondence.verified, FamilyCorrespondence.sameFamily, coverageBasisVerified, Transition.counted] example : repeated.reviewReady = true := by decide example : repeated.reviewComplete = false := by decide @@ -167,8 +196,8 @@ example : ¬ guardImplementationFlight repeated := by simp [guardImplementationFlight, hr] example : ¬ allowed funded (.pass .repairWithRerunReview { family with coverageBasis := .unsupportedMemberEnumeration } (some twoParts)) := by - simp [allowed, guardPass, familyPassAllowed, familyRoute, family, - classGateActive, ownerAuthorizedDomainChange, coverageBasisVerified] + exact unsupported_class_cannot_start_batch funded + { family with coverageBasis := .unsupportedMemberEnumeration } (some twoParts) rfl (by decide) -- Active, terminal-with-failed-checks, and exhausted incomplete assignments never admit review. example : opened.reviewReady = false := by decide @@ -186,7 +215,7 @@ example : ¬ guardImplementationFlight exhausted := by simp [guardImplementationFlight, hb] -- A single flight still goes directly to its one initial triplet after all checks. private def single := step (finish (step (step readyState - (.beginImplementation ⟨["all work"], 1⟩)) + (.beginImplementation ⟨["all work"], 1, []⟩)) (.openFlight .implementation .implementation .codexCli "target" 0)) 0 successful) (.recordImplementation 0 ["all work"] true) example : single.reviewReady = true := by decide @@ -199,6 +228,19 @@ private def admitted (s : ProtocolState) : List Action → Prop private def run (s : ProtocolState) (actions : List Action) : ProtocolState := actions.foldl step s +private theorem run_append (s : ProtocolState) (xs ys : List Action) : + run s (xs ++ ys) = run (run s xs) ys := by + simp only [run, List.foldl_append] + +private theorem admitted_append (s : ProtocolState) (xs ys : List Action) : + admitted s (xs ++ ys) ↔ admitted s xs ∧ admitted (run s xs) ys := by + induction xs generalizing s with + | nil => simp [admitted, run] + | cons a xs ih => + change (allowed s a ∧ admitted (step s a) (xs ++ ys)) ↔ + (allowed s a ∧ admitted (step s a) xs) ∧ admitted (run (step s a) xs) ys + simp only [ih, and_assoc] + private def implementationActions (firstId : Nat) : List Action := [.openFlight .implementation .implementation .codexCli "target" 0, .launchViaRunner firstId, .hostNotified firstId, .collect firstId successful, @@ -219,7 +261,7 @@ example : admitted readyState [.beginImplementation twoParts] := by simp [admitted, allowed, guardBeginImplementation, readyState, ProtocolState.initial, twoParts, ImplementationPlan.valid] example : admitted begin (implementationActions 0) := by - simp [admitted, implementationActions, allowed, guardOpenFlight, guardImplementationFlight, + simp [admitted, implementationActions, allowed, guardOpenFlight, ProtocolState.carrierEnabled, guardImplementationFlight, guardLaunchViaRunner, guardHostNotified, guardCollect, guardRecordImplementation, begin, readyState, twoParts, ProtocolState.initial, ProtocolState.modeResolved, ProtocolState.abstained, ProtocolState.reviewStarted, ProtocolState.reviewReady, @@ -227,49 +269,85 @@ example : admitted begin (implementationActions 0) := by ProtocolState.freshId, step, ImplementationPlan.start, newFlight, updateFlight, collectEffect, done, successful, FlightRec.active] example : run begin (implementationActions 0) = complete := rfl -example : admitted review (reviewActions 2) := by - simp [admitted, reviewActions, allowed, guardOpenFlight, guardReviewFlight, +private theorem initialReviewAdmitted : admitted review (reviewActions 2) := by + simp [admitted, reviewActions, allowed, guardOpenFlight, ProtocolState.carrierEnabled, guardReviewFlight, guardLaunchViaRunner, guardHostNotified, guardCollect, seatEligible, canRunRepositoryCommands, review, complete, second, partDone, returned, opened, begin, readyState, finish, twoParts, ProtocolState.initial, ProtocolState.modeResolved, ProtocolState.abstained, ProtocolState.reviewReady, ProtocolState.batchSettled, ProtocolState.batchFlights, ProtocolState.flight, ProtocolState.freshId, step, ImplementationPlan.start, newFlight, - updateFlight, collectEffect, done, successful, FlightRec.active, reviewRoles, Stage.next] -example : run review (reviewActions 2) = reviewed := rfl -example : allowed reviewed .advanceStage := by + updateFlight, collectEffect, done, successful, ProtocolState.flightProtected, FlightRec.active, reviewRoles, Stage.next] +private theorem initialReviewRun : run review (reviewActions 2) = reviewed := rfl +private theorem initialReviewAdvanceAdmitted : allowed reviewed .advanceStage := by simp only [allowed, guardAdvanceStage, ProtocolState.goalWritten, ProtocolState.modeResolved, ProtocolState.abstained] decide -example : allowed fix (.recordPassBudget 1) := by +private theorem firstRepairBudgetAdmitted : allowed fix (.recordPassBudget 1) := by simp only [allowed, guardRecordPassBudget] decide -- A paid repair uses identical whole-plan admission and still includes its review at zero. set_option maxRecDepth 4096 in -example : admitted repair (implementationActions 5) := by - simp [admitted, implementationActions, allowed, guardOpenFlight, guardImplementationFlight, +private theorem firstRepairImplementationAdmitted : admitted repair (implementationActions 5) := by + simp [admitted, implementationActions, allowed, guardOpenFlight, ProtocolState.carrierEnabled, guardImplementationFlight, guardLaunchViaRunner, guardHostNotified, guardCollect, guardRecordImplementation, repair, funded, fix, reviewed, tests, quality, architecture, review, complete, second, partDone, returned, opened, begin, readyState, finish, twoParts, ProtocolState.initial, ProtocolState.modeResolved, ProtocolState.abstained, ProtocolState.reviewStarted, ProtocolState.reviewReady, ProtocolState.batchSettled, ProtocolState.batchFlights, ProtocolState.flight, ProtocolState.freshId, step, ImplementationPlan.start, newFlight, - updateFlight, collectEffect, done, successful, FlightRec.active, Stage.next] -example : run repair (implementationActions 5) = repaired := rfl + updateFlight, collectEffect, done, successful, ProtocolState.flightProtected, FlightRec.active, Stage.next] +private theorem firstRepairImplementationRun : run repair (implementationActions 5) = repaired := rfl set_option maxRecDepth 4096 in -example : admitted repaired (reviewActions 7) := by - simp [admitted, reviewActions, allowed, guardOpenFlight, guardReviewFlight, +private theorem firstRepairReviewAdmitted : admitted repaired (reviewActions 7) := by + simp [admitted, reviewActions, allowed, guardOpenFlight, ProtocolState.carrierEnabled, guardReviewFlight, guardLaunchViaRunner, guardHostNotified, guardCollect, seatEligible, canRunRepositoryCommands, repaired, repairedFirst, repair, funded, fix, reviewed, tests, quality, architecture, review, complete, second, partDone, returned, opened, begin, readyState, finish, twoParts, ProtocolState.initial, ProtocolState.modeResolved, ProtocolState.abstained, ProtocolState.reviewReady, ProtocolState.batchSettled, ProtocolState.batchFlights, ProtocolState.flight, ProtocolState.freshId, step, ImplementationPlan.start, newFlight, - updateFlight, collectEffect, done, successful, FlightRec.active, reviewRoles, Stage.next] -example : run repaired (reviewActions 7) = repairReviewed := rfl + updateFlight, collectEffect, done, successful, ProtocolState.flightProtected, FlightRec.active, reviewRoles, Stage.next] +private theorem firstRepairReviewRun : run repaired (reviewActions 7) = repairReviewed := rfl + +private def firstRepairActions : List Action := + reviewActions 2 ++ ([.advanceStage, .recordPassBudget 1, + .pass .repairWithRerunReview firstFamily (some twoParts)] ++ + (implementationActions 5 ++ reviewActions 7)) + +-- Every production guard is checked from initial review through the first finite repair +-- and its included final triplet. The review route and family projection share evidence. +private theorem initial_review_new_family_repair : + routeFindings ordinary approval approval = .fix ∧ + classGateActive firstFamily = false ∧ admitted review firstRepairActions := by + refine ⟨by decide, by decide, ?_⟩ + rw [firstRepairActions, admitted_append] + refine ⟨initialReviewAdmitted, ?_⟩ + rw [initialReviewRun] + change allowed reviewed .advanceStage ∧ allowed fix (.recordPassBudget 1) ∧ + allowed funded (.pass .repairWithRerunReview firstFamily (some twoParts)) ∧ + admitted repair (implementationActions 5 ++ reviewActions 7) + refine ⟨initialReviewAdvanceAdmitted, firstRepairBudgetAdmitted, firstRepairPassAdmitted, ?_⟩ + rw [admitted_append, firstRepairImplementationRun] + exact ⟨firstRepairImplementationAdmitted, firstRepairReviewAdmitted⟩ + +private theorem firstRepairEntryRun : + run reviewed [.advanceStage, .recordPassBudget 1, + .pass .repairWithRerunReview firstFamily (some twoParts)] = repair := by + simp only [run, List.foldl_cons, List.foldl_nil, repair, funded, fix] + +private theorem firstRepairRun : run review firstRepairActions = repairReviewed := by + rw [firstRepairActions, run_append, initialReviewRun, run_append, firstRepairEntryRun, + run_append, firstRepairImplementationRun, firstRepairReviewRun] + +set_option maxRecDepth 4096 in +example : (run review firstRepairActions).reviewComplete = true ∧ + (run review firstRepairActions).passBudget = some 0 := by + rw [firstRepairRun] + decide private def recoveryActions (observation : Observation) : List Action := - [.beginImplementation ⟨["all work"], 1⟩, + [.beginImplementation ⟨["all work"], 1, []⟩, .openFlight .implementation .implementation .codexCli "target" 0, .launchViaRunner 0, .hostNotified 0, .collect 0 { successful with exitZero := false }, .fallbackFlight 0 .isolatedTokenSubagent, @@ -279,13 +357,13 @@ private def recoveryActions (observation : Observation) : List Action := private theorem recovery_admitted (observation : Observation) : admitted readyState (recoveryActions observation) := by simp [admitted, recoveryActions, allowed, guardBeginImplementation, ImplementationPlan.valid, - guardOpenFlight, guardImplementationFlight, guardLaunchViaRunner, guardLaunchDelegated, + guardOpenFlight, ProtocolState.carrierEnabled, guardImplementationFlight, guardLaunchViaRunner, guardLaunchDelegated, ProtocolState.carrierEnabled, guardHostNotified, guardCollect, guardFallback, readyState, ProtocolState.initial, ProtocolState.modeResolved, ProtocolState.abstained, ProtocolState.reviewStarted, ProtocolState.reviewReady, ProtocolState.batchSettled, ProtocolState.batchFlights, ProtocolState.flight, ProtocolState.freshId, ProtocolState.triedCarriers, - ProtocolState.eligibleCarriers, step, ImplementationPlan.start, newFlight, reopenFlight, - updateFlight, collectEffect, done, successful, FlightRec.active, nextCarrier, + ProtocolState.eligibleCarriers, ProtocolState.carrierEnabled, step, ImplementationPlan.start, newFlight, reopenFlight, + updateFlight, collectEffect, done, successful, ProtocolState.flightProtected, FlightRec.active, nextCarrier, Carrier.univ, CarrierSet.get] private def recoveryReturned := run readyState (recoveryActions successful) @@ -309,7 +387,7 @@ private def hecaReady (budget : Option Nat) : ProtocolState := private def ownStop : HecaStopEvidence := ⟨true, true, true⟩ private def hecaInitialActions (retries : Nat) : List Action := - [.beginImplementation ⟨["all work"], 1⟩, + [.beginImplementation ⟨["all work"], 1, []⟩, .openFlight .implementation .implementation .heca "target" retries, .launchDelegated 0] private def hecaInFlight (budget : Option Nat) (retries : Nat) := @@ -321,7 +399,7 @@ private def archiveFlight : FlightRec := private def archiveNotifiedState : ProtocolState := { ProtocolState.initial with stage := .implementation, goal := some goal, mode := some (.carrier .heca), - flights := [archiveFlight] } + capabilityChecked := [.heca], hecaCheckRecorded := true, flights := [archiveFlight] } private def archiveCollectedFlight : FlightRec := { archiveFlight with status := .terminal } private def archiveCollectedState : ProtocolState := @@ -356,13 +434,13 @@ example : allowed failedCollectedState (.archiveHecaAttempt 0 true .failedReport archiveNotifiedState, archiveFlight, ProtocolState.initial, newFlight, ProtocolState.pendingHousekeeping, ProtocolState.flight] example : ¬ allowed failedCollectedState (.launchDelegated 0) := by - simp [allowed, guardLaunchDelegated, failedCollectedState, failedArchiveFlight, + simp [allowed, guardLaunchDelegated, ProtocolState.carrierEnabled, failedCollectedState, failedArchiveFlight, archiveNotifiedState, archiveFlight, ProtocolState.initial, newFlight, ProtocolState.attemptSettled, ProtocolState.pendingHousekeeping, ProtocolState.flight] example : allowed (step failedCollectedState (.archiveHecaAttempt 0 true .archived)) (.launchDelegated 0) := by - simp [allowed, guardLaunchDelegated, failedCollectedState, failedArchiveFlight, + simp [allowed, guardLaunchDelegated, ProtocolState.carrierEnabled, failedCollectedState, failedArchiveFlight, archiveNotifiedState, archiveFlight, ProtocolState.initial, newFlight, step, ProtocolState.attemptSettled, ProtocolState.pendingHousekeeping, ProtocolState.flight, recordPendingArchive] @@ -381,15 +459,15 @@ example : ¬ allowed ProtocolState.batchFlights, ProtocolState.reviewStarted, ProtocolState.attemptSettled, ProtocolState.housekeepingFor, ProtocolState.allHecaHousekeepingSettled, ProtocolState.modeResolved, - ProtocolState.abstained, ProtocolState.flight, FlightRec.active, Stage.next] + ProtocolState.abstained, ProtocolState.flight, ProtocolState.flightProtected, FlightRec.active, Stage.next] theorem heca_first_implementation_admitted (budget : Option Nat) (retries : Nat) : admitted (hecaReady budget) (hecaInitialActions retries) := by simp [admitted, hecaInitialActions, hecaReady, allowed, guardBeginImplementation, - ImplementationPlan.valid, guardOpenFlight, guardImplementationFlight, - guardLaunchDelegated, readyState, ProtocolState.initial, ProtocolState.modeResolved, + ImplementationPlan.valid, guardOpenFlight, ProtocolState.carrierEnabled, guardImplementationFlight, + guardLaunchDelegated, ProtocolState.carrierEnabled, readyState, ProtocolState.initial, ProtocolState.modeResolved, ProtocolState.abstained, ProtocolState.reviewStarted, ProtocolState.reviewReady, ProtocolState.batchSettled, ProtocolState.batchFlights, ProtocolState.flight, - ProtocolState.freshId, step, ImplementationPlan.start, newFlight, FlightRec.active, + ProtocolState.freshId, step, ImplementationPlan.start, newFlight, ProtocolState.flightProtected, FlightRec.active, Carrier.univ] theorem heca_stopped_no_notice_failure_admitted (budget : Option Nat) (retries : Nat) : @@ -398,7 +476,7 @@ theorem heca_stopped_no_notice_failure_admitted (budget : Option Nat) (retries : simp [allowed, guardStoppedHecaFailure, hecaInFlight, run, hecaInitialActions, hecaReady, readyState, ProtocolState.initial, ProtocolState.flight, ProtocolState.freshId, step, ImplementationPlan.start, newFlight, updateFlight, - FlightRec.active, ownStop, HecaStopEvidence.confirmed] + ProtocolState.flightProtected, FlightRec.active, ownStop, HecaStopEvidence.confirmed] theorem heca_unnotified_success_refused (budget : Option Nat) (retries : Nat) : ¬ allowed (hecaInFlight budget retries) (.collect 0 successful) := by @@ -414,7 +492,7 @@ theorem heca_running_unnotified_failure_refused (budget : Option Nat) (retries : simp [allowed, guardStoppedHecaFailure, guardCollect, guardMutateTarget, hecaInFlight, run, hecaInitialActions, hecaReady, readyState, ProtocolState.initial, ProtocolState.flight, ProtocolState.freshId, ProtocolState.activeOn, step, - ImplementationPlan.start, newFlight, updateFlight, FlightRec.active, + ImplementationPlan.start, newFlight, updateFlight, ProtocolState.flightProtected, FlightRec.active, HecaStopEvidence.confirmed] private def hecaRetried (budget : Option Nat) := @@ -429,7 +507,7 @@ theorem heca_stopped_no_notice_retry (budget : Option Nat) : simp [hecaRetried, hecaInFlight, run, hecaInitialActions, hecaReady, readyState, ProtocolState.initial, ProtocolState.flight, ProtocolState.freshId, ProtocolState.activeOn, step, ImplementationPlan.start, newFlight, updateFlight, - collectEffect, stoppedHecaFailure, done, FlightRec.active, allowed, + collectEffect, stoppedHecaFailure, done, ProtocolState.flightProtected, FlightRec.active, allowed, guardStoppedHecaFailure, guardMutateTarget] private def hecaRecoveryActions : List Action := @@ -443,16 +521,16 @@ private def hecaRecoveryActions : List Action := theorem heca_stop_without_notice_recovery_admitted (budget : Option Nat) : admitted (hecaReady budget) hecaRecoveryActions := by simp [admitted, hecaRecoveryActions, hecaInitialActions, hecaReady, allowed, - guardBeginImplementation, ImplementationPlan.valid, guardOpenFlight, - guardImplementationFlight, guardLaunchViaRunner, guardLaunchDelegated, + guardBeginImplementation, ImplementationPlan.valid, guardOpenFlight, ProtocolState.carrierEnabled, + guardImplementationFlight, guardLaunchViaRunner, guardLaunchDelegated, ProtocolState.carrierEnabled, guardStoppedHecaFailure, ownStop, HecaStopEvidence.confirmed, guardHostNotified, guardCollect, guardFallback, guardRecordImplementation, guardAdvanceStage, readyState, ProtocolState.initial, ProtocolState.modeResolved, ProtocolState.abstained, ProtocolState.reviewStarted, ProtocolState.reviewReady, ProtocolState.batchSettled, ProtocolState.batchFlights, ProtocolState.flight, - ProtocolState.freshId, ProtocolState.triedCarriers, ProtocolState.eligibleCarriers, + ProtocolState.freshId, ProtocolState.triedCarriers, ProtocolState.eligibleCarriers, ProtocolState.carrierEnabled, step, ImplementationPlan.start, newFlight, reopenFlight, updateFlight, - collectEffect, stoppedHecaFailure, done, successful, FlightRec.active, + collectEffect, stoppedHecaFailure, done, successful, ProtocolState.flightProtected, FlightRec.active, nextCarrier, Carrier.univ, CarrierSet.get, Stage.next] private def hecaRecovered (budget : Option Nat) := run (hecaReady budget) hecaRecoveryActions @@ -470,7 +548,7 @@ theorem heca_stop_without_notice_recovery_settles (budget : Option Nat) : readyState, ProtocolState.initial, step, ImplementationPlan.start, newFlight, reopenFlight, updateFlight, collectEffect, stoppedHecaFailure, done, successful, ProtocolState.reviewReady, ProtocolState.batchSettled, ProtocolState.batchFlights, - ProtocolState.flight, ProtocolState.freshId, FlightRec.active, Stage.next] + ProtocolState.flight, ProtocolState.freshId, ProtocolState.flightProtected, FlightRec.active, Stage.next] example : admitted (hecaReady none) hecaRecoveryActions := heca_stop_without_notice_recovery_admitted none @@ -496,14 +574,14 @@ theorem heca_notified_unreadable_recovery_admitted (budget : Option Nat) (outcome : ArchiveOutcome := .archived) : admitted (hecaReady budget) (hecaUnreadableRecoveryActions outcome) := by cases outcome <;> simp [admitted, hecaUnreadableRecoveryActions, hecaInitialActions, hecaReady, allowed, - guardBeginImplementation, ImplementationPlan.valid, guardOpenFlight, - guardImplementationFlight, guardLaunchDelegated, guardHostNotified, guardCollect, + guardBeginImplementation, ImplementationPlan.valid, guardOpenFlight, ProtocolState.carrierEnabled, + guardImplementationFlight, guardLaunchDelegated, ProtocolState.carrierEnabled, guardHostNotified, guardCollect, guardArchiveHeca, guardStoppedHecaFailure, ownStop, HecaStopEvidence.confirmed, readyState, ProtocolState.initial, ProtocolState.modeResolved, ProtocolState.abstained, ProtocolState.reviewStarted, ProtocolState.reviewReady, ProtocolState.batchSettled, ProtocolState.batchFlights, ProtocolState.flight, ProtocolState.freshId, step, ImplementationPlan.start, newFlight, updateFlight, recordPendingArchive, - collectEffect, stoppedHecaFailure, unreadable, done, FlightRec.active, Carrier.univ] + collectEffect, stoppedHecaFailure, unreadable, done, ProtocolState.flightProtected, FlightRec.active, Carrier.univ] theorem heca_notice_window_archive_and_stop_refused (budget : Option Nat) (retries : Nat) : ¬ allowed (hecaNotified budget retries) (.archiveHecaAttempt 0 true .archived) ∧ @@ -531,12 +609,12 @@ theorem heca_unreadable_without_confirmation_refused (budget : Option Nat) (retr (.recordStoppedHecaFailure 0 ⟨true, true, false⟩) ∧ ¬ allowed (hecaUnreadableArchived budget retries outcome) (.mutateTarget "target") ∧ ¬ allowed (hecaUnreadableArchived budget retries outcome) (.collect 0 successful) := by - cases outcome <;> simp [allowed, guardLaunchDelegated, guardFallback, guardStoppedHecaFailure, + cases outcome <;> simp [allowed, guardLaunchDelegated, ProtocolState.carrierEnabled, guardFallback, guardStoppedHecaFailure, guardMutateTarget, guardCollect, hecaUnreadableArchived, hecaUnreadableCollected, hecaNotified, hecaInFlight, run, hecaInitialActions, hecaReady, readyState, ProtocolState.initial, step, ProtocolState.flight, ProtocolState.freshId, ImplementationPlan.start, newFlight, updateFlight, unreadable, recordPendingArchive, - ProtocolState.activeOn, FlightRec.active, HecaStopEvidence.confirmed] + ProtocolState.activeOn, ProtocolState.flightProtected, FlightRec.active, HecaStopEvidence.confirmed] theorem heca_unreadable_requires_archive_before_confirmation (budget : Option Nat) (retries : Nat) : @@ -571,7 +649,7 @@ theorem heca_unreadable_confirmed_exhaustion_admitted (budget : Option Nat) readyState, ProtocolState.initial, step, ProtocolState.flight, ProtocolState.freshId, ImplementationPlan.start, newFlight, updateFlight, unreadable, collectEffect, stoppedHecaFailure, done, recordPendingArchive, - ownStop, HecaStopEvidence.confirmed, FlightRec.active, ProtocolState.eligibleCarriers, + ownStop, HecaStopEvidence.confirmed, ProtocolState.flightProtected, FlightRec.active, ProtocolState.eligibleCarriers, ProtocolState.carrierEnabled, ProtocolState.triedCarriers, nextCarrier, Carrier.univ, CarrierSet.get] -- Both archive outcomes admit the complete retry trace; failed cleanup remains reported. @@ -587,15 +665,15 @@ private def hecaUnreadableExhaustionActions : List Action := theorem heca_reported_archive_exhausted_fallback_admitted (budget : Option Nat) : admitted (hecaReady budget) hecaUnreadableExhaustionActions := by simp [admitted, hecaUnreadableExhaustionActions, hecaInitialActions, hecaReady, allowed, - guardBeginImplementation, ImplementationPlan.valid, guardOpenFlight, - guardImplementationFlight, guardLaunchDelegated, guardHostNotified, guardCollect, + guardBeginImplementation, ImplementationPlan.valid, guardOpenFlight, ProtocolState.carrierEnabled, + guardImplementationFlight, guardLaunchDelegated, ProtocolState.carrierEnabled, guardHostNotified, guardCollect, guardArchiveHeca, guardStoppedHecaFailure, guardFallback, readyState, ProtocolState.initial, ProtocolState.modeResolved, ProtocolState.abstained, ProtocolState.reviewStarted, ProtocolState.reviewReady, ProtocolState.batchSettled, ProtocolState.batchFlights, ProtocolState.flight, ProtocolState.freshId, - ProtocolState.eligibleCarriers, ProtocolState.triedCarriers, + ProtocolState.eligibleCarriers, ProtocolState.carrierEnabled, ProtocolState.triedCarriers, step, ImplementationPlan.start, newFlight, updateFlight, recordPendingArchive, - collectEffect, stoppedHecaFailure, unreadable, done, FlightRec.active, + collectEffect, stoppedHecaFailure, unreadable, done, ProtocolState.flightProtected, FlightRec.active, nextCarrier, Carrier.univ, CarrierSet.get] theorem heca_reported_archive_exhaustion_preserves_report (budget : Option Nat) : @@ -623,12 +701,12 @@ private def hecaSuccessActions (outcome : ArchiveOutcome) : List Action := theorem heca_collection_admitted (budget : Option Nat) (o : Observation) : admitted (hecaReady budget) (hecaCollectionActions o) := by simp [admitted, hecaCollectionActions, hecaInitialActions, hecaReady, allowed, - guardBeginImplementation, ImplementationPlan.valid, guardOpenFlight, - guardImplementationFlight, guardLaunchDelegated, guardHostNotified, guardCollect, + guardBeginImplementation, ImplementationPlan.valid, guardOpenFlight, ProtocolState.carrierEnabled, + guardImplementationFlight, guardLaunchDelegated, ProtocolState.carrierEnabled, guardHostNotified, guardCollect, readyState, ProtocolState.initial, ProtocolState.modeResolved, ProtocolState.abstained, ProtocolState.reviewStarted, ProtocolState.reviewReady, ProtocolState.batchSettled, ProtocolState.batchFlights, ProtocolState.flight, ProtocolState.freshId, - step, ImplementationPlan.start, newFlight, updateFlight, FlightRec.active, Carrier.univ] + step, ImplementationPlan.start, newFlight, updateFlight, ProtocolState.flightProtected, FlightRec.active, Carrier.univ] theorem heca_success_collect_record_refused (budget : Option Nat) : ¬ allowed (hecaCollected budget successful) (.recordImplementation 0 ["all work"] true) := by @@ -653,13 +731,13 @@ theorem heca_success_archive_record_advance_admitted (budget : Option Nat) admitted (hecaReady budget) (hecaSuccessActions outcome) := by cases outcome <;> simp [admitted, hecaSuccessActions, hecaCollectionActions, hecaInitialActions, hecaReady, allowed, guardBeginImplementation, ImplementationPlan.valid, - guardOpenFlight, guardImplementationFlight, guardLaunchDelegated, guardHostNotified, + guardOpenFlight, ProtocolState.carrierEnabled, guardImplementationFlight, guardLaunchDelegated, ProtocolState.carrierEnabled, guardHostNotified, guardCollect, guardArchiveHeca, guardRecordImplementation, guardAdvanceStage, readyState, ProtocolState.initial, ProtocolState.modeResolved, ProtocolState.abstained, ProtocolState.reviewStarted, ProtocolState.reviewReady, ProtocolState.batchSettled, ProtocolState.batchFlights, ProtocolState.flight, ProtocolState.freshId, step, ImplementationPlan.start, newFlight, updateFlight, recordPendingArchive, - collectEffect, successful, done, FlightRec.active, Carrier.univ, Stage.next] + collectEffect, successful, done, ProtocolState.flightProtected, FlightRec.active, Carrier.univ, Stage.next] theorem heca_success_second_archive_refused (budget : Option Nat) : ¬ allowed (step (hecaCollected budget successful) (.archiveHecaAttempt 0 true .archived)) @@ -684,7 +762,7 @@ theorem heca_failed_collect_fallback_requires_archive (budget : Option Nat) : simp [allowed, guardFallback, hecaCollected, run, hecaCollectionActions, hecaInitialActions, hecaReady, readyState, ProtocolState.initial, step, ProtocolState.flight, ProtocolState.freshId, ImplementationPlan.start, - ProtocolState.eligibleCarriers, ProtocolState.triedCarriers, + ProtocolState.eligibleCarriers, ProtocolState.carrierEnabled, ProtocolState.triedCarriers, newFlight, updateFlight, collectEffect, successful, done, recordPendingArchive, nextCarrier, Carrier.univ, CarrierSet.get] @@ -700,7 +778,7 @@ example (id : Nat) (c : Carrier) : ¬ allowed carrierExhausted (.fallbackFlight ProtocolState.flight, ProtocolState.freshId, newFlight, reopenFlight, updateFlight, collectEffect, done, successful] at hf rcases hf with ⟨_, rfl⟩ | ⟨_, _, rfl⟩ <;> - simp [ProtocolState.eligibleCarriers, ProtocolState.triedCarriers, + simp [ProtocolState.eligibleCarriers, ProtocolState.carrierEnabled, ProtocolState.triedCarriers, carrierExhausted, run, recoveryActions, readyState, ProtocolState.initial, step, ProtocolState.flight, ProtocolState.freshId, newFlight, reopenFlight, updateFlight, collectEffect, done, successful, nextCarrier, Carrier.univ, CarrierSet.get] at hn @@ -718,7 +796,7 @@ example : allowed failed (.fallbackFlight 1 .isolatedTokenSubagent) := by simp [allowed, guardFallback, failed, finish, second, partDone, returned, opened, begin, readyState, step, updateFlight, collectEffect, done, successful, twoParts, ImplementationPlan.start, ProtocolState.initial, ProtocolState.flight, - ProtocolState.freshId, ProtocolState.triedCarriers, ProtocolState.eligibleCarriers, + ProtocolState.freshId, ProtocolState.triedCarriers, ProtocolState.eligibleCarriers, ProtocolState.carrierEnabled, newFlight, nextCarrier, Carrier.univ, CarrierSet.get] -- Test-seat restriction applies to initial, repeated, and included repair review alike. @@ -726,7 +804,7 @@ example : ¬ allowed { review with capabilityChecked := Carrier.univ } (.openFlight .review .tests .nyxidOracle "target" 0) := tests_dispatch_excludes_oracle _ _ _ example : allowed review (.openFlight .review .tests .isolatedTokenSubagent "target" 0) := by - simp only [allowed, guardOpenFlight, guardReviewFlight, ProtocolState.modeResolved, + simp only [allowed, guardOpenFlight, ProtocolState.carrierEnabled, guardReviewFlight, ProtocolState.modeResolved, ProtocolState.abstained] decide example : ¬ allowed repeated (.openFlight .review .tests .nyxidOracle "target" 0) := @@ -754,18 +832,18 @@ example : ¬ allowed recoveryReturned (.fallbackFlight 0 .isolatedTokenSubagent) newFlight, reopenFlight, updateFlight, collectEffect, done, successful] example : admitted readyState - [.beginImplementation ⟨["all work"], 1⟩, + [.beginImplementation ⟨["all work"], 1, []⟩, .openFlight .implementation .implementation .codexCli "target" 0, .launchViaRunner 0, .hostNotified 0, .collect 0 successful, .recordImplementation 0 ["all work"] true, .advanceStage] := by simp [admitted, allowed, guardBeginImplementation, ImplementationPlan.valid, - guardOpenFlight, guardImplementationFlight, guardLaunchViaRunner, guardHostNotified, + guardOpenFlight, ProtocolState.carrierEnabled, guardImplementationFlight, guardLaunchViaRunner, guardHostNotified, guardCollect, guardRecordImplementation, guardAdvanceStage, readyState, ProtocolState.initial, ProtocolState.modeResolved, ProtocolState.abstained, ProtocolState.reviewStarted, ProtocolState.reviewReady, ProtocolState.batchSettled, ProtocolState.batchFlights, ProtocolState.flight, ProtocolState.freshId, step, ImplementationPlan.start, newFlight, updateFlight, collectEffect, done, - successful, FlightRec.active, Stage.next] + successful, ProtocolState.flightProtected, FlightRec.active, Stage.next] private def testsReviewState := { review with capabilityChecked := [.codexCli, .nyxidOracle, .isolatedTokenSubagent] } private def testsRecoveryActions (observation : Observation) : List Action := @@ -777,13 +855,13 @@ private def testsRecoveryActions (observation : Observation) : List Action := example (observation : Observation) : admitted testsReviewState (testsRecoveryActions observation) := by simp [admitted, testsRecoveryActions, testsReviewState, review, complete, second, partDone, returned, opened, begin, readyState, finish, twoParts, successful, - allowed, guardOpenFlight, guardReviewFlight, seatEligible, canRunRepositoryCommands, - guardLaunchViaRunner, guardLaunchDelegated, guardHostNotified, guardCollect, guardFallback, + allowed, guardOpenFlight, ProtocolState.carrierEnabled, guardReviewFlight, seatEligible, canRunRepositoryCommands, + guardLaunchViaRunner, guardLaunchDelegated, ProtocolState.carrierEnabled, guardHostNotified, guardCollect, guardFallback, ProtocolState.initial, ProtocolState.modeResolved, ProtocolState.abstained, ProtocolState.reviewReady, ProtocolState.batchSettled, ProtocolState.batchFlights, ProtocolState.flight, ProtocolState.freshId, ProtocolState.triedCarriers, - ProtocolState.eligibleCarriers, step, ImplementationPlan.start, newFlight, reopenFlight, - updateFlight, collectEffect, done, FlightRec.active, nextCarrier, Carrier.univ, + ProtocolState.eligibleCarriers, ProtocolState.carrierEnabled, step, ImplementationPlan.start, newFlight, reopenFlight, + updateFlight, collectEffect, done, ProtocolState.flightProtected, FlightRec.active, nextCarrier, Carrier.univ, CarrierSet.get, reviewRoles, Stage.next] private def testsRecovered := run testsReviewState (testsRecoveryActions successful) example : (testsRecovered.flight 3).map (·.status) = some .terminal := by decide @@ -809,7 +887,7 @@ example : allowed oracleReview (.launchViaRunner 2) := by ProtocolState.initial, ProtocolState.flight, ProtocolState.freshId, step, ImplementationPlan.start, newFlight, updateFlight, collectEffect, done] example : ¬ allowed oracleReview (.launchDelegated 2) := by - simp [allowed, guardLaunchDelegated, oracleReview, testsReviewState, review, complete, second, + simp [allowed, guardLaunchDelegated, ProtocolState.carrierEnabled, oracleReview, testsReviewState, review, complete, second, partDone, returned, opened, begin, readyState, finish, twoParts, successful, ProtocolState.initial, ProtocolState.flight, ProtocolState.freshId, step, ImplementationPlan.start, newFlight, updateFlight, collectEffect, done] @@ -817,12 +895,12 @@ example : ¬ allowed oracleReview (.launchDelegated 2) := by private def scopeNote : Revision := ⟨"engineering scope note", "existing user authorization", "none"⟩ private def authorizedRevision (r : Revision) (source : Option ContinuationSource) : RevisionEvidence := - ⟨r, true, true, source⟩ + ⟨r, true, true, source, false, false⟩ private def startupActions (c : ContinuationEntry) : List Action := [.writeGoal goal (intake c), .appendRevision scopeNote (authorizedRevision scopeNote none), - .advanceStage, .capabilityCheck .codexCli, .recordHecaCheck ⟨false, .disabled⟩, .resolveMode (.carrier .codexCli), .advanceStage] + .advanceStage, .capabilityCheck .codexCli, .recordHecaCheck ⟨false, .disabled, false⟩, .resolveMode (.carrier .codexCli), .advanceStage] -- Every opt-in/exposure combination passes through the production check and consumers. -- Opt-in source is supplied evidence; these cases do not detect authority from English. private def optInCheckState : ProtocolState := @@ -831,7 +909,7 @@ private def optInCheckState : ProtocolState := hecaCheckRecorded := false, capabilityChecked := [.codexCli, .isolatedTokenSubagent] } private def optInState (source : HecaOptIn) (exposed : Bool) : ProtocolState := - { step optInCheckState (.recordHecaCheck ⟨exposed, source⟩) with + { step optInCheckState (.recordHecaCheck ⟨exposed, source, false⟩) with stage := .implementation, mode := some (.carrier .codexCli) } example (facts : HecaCapability) : allowed optInCheckState (.recordHecaCheck facts) := by @@ -841,7 +919,7 @@ example (facts : HecaCapability) : allowed optInCheckState (.recordHecaCheck fac private def optInFailed (source : HecaOptIn) (exposed : Bool) : ProtocolState := finish (step (step (optInState source exposed) - (.beginImplementation ⟨["all work"], 1⟩)) + (.beginImplementation ⟨["all work"], 1, []⟩)) (.openFlight .implementation .implementation .codexCli "target" 0)) 0 { successful with exitZero := false } @@ -854,18 +932,18 @@ theorem heca_opt_in_consumer_matrix : available = (source != .disabled && exposed) ∧ (Clauses.stageComposition 3 available).contains .heca = available ∧ (Clauses.stageComposition 1 available).contains .heca = available ∧ - (allowed (step s (.beginImplementation ⟨["all work"], 1⟩)) + (allowed (step s (.beginImplementation ⟨["all work"], 1, []⟩)) (.openFlight .implementation .implementation .heca "target" 0) ↔ available = true) ∧ (allowed (optInFailed source exposed) (.fallbackFlight 0 .heca) ↔ available = true) := by intro source _ exposed _ cases source <;> cases exposed <;> simp [optInState, optInCheckState, optInFailed, readyState, ProtocolState.initial, - finish, allowed, guardOpenFlight, guardImplementationFlight, guardFallback, + finish, allowed, guardOpenFlight, ProtocolState.carrierEnabled, guardImplementationFlight, guardFallback, guardBeginImplementation, ImplementationPlan.valid, admitted, guardLaunchViaRunner, guardHostNotified, guardCollect, ProtocolState.modeResolved, ProtocolState.abstained, step, ImplementationPlan.start, newFlight, ProtocolState.freshId, ProtocolState.flight, updateFlight, collectEffect, - done, successful, FlightRec.active, ProtocolState.eligibleCarriers, + done, successful, ProtocolState.flightProtected, FlightRec.active, ProtocolState.eligibleCarriers, ProtocolState.carrierEnabled, ProtocolState.triedCarriers, nextCarrier, Carrier.univ, CarrierSet.get, HecaCapability.detected, Clauses.stageComposition, ProtocolState.reviewStarted, ProtocolState.reviewReady, ProtocolState.batchSettled, @@ -876,18 +954,18 @@ theorem heca_opt_in_consumer_matrix : theorem opt_in_codex_failure_admitted : ∀ source ∈ [HecaOptIn.disabled, .user, .host], ∀ exposed ∈ [false, true], admitted (optInState source exposed) - [.beginImplementation ⟨["all work"], 1⟩, + [.beginImplementation ⟨["all work"], 1, []⟩, .openFlight .implementation .implementation .codexCli "target" 0, .launchViaRunner 0, .hostNotified 0, .collect 0 { successful with exitZero := false }] := by intro source _ exposed _ cases source <;> cases exposed <;> simp [optInState, optInCheckState, optInFailed, readyState, ProtocolState.initial, - finish, allowed, guardOpenFlight, guardImplementationFlight, guardFallback, + finish, allowed, guardOpenFlight, ProtocolState.carrierEnabled, guardImplementationFlight, guardFallback, guardBeginImplementation, ImplementationPlan.valid, admitted, guardLaunchViaRunner, guardHostNotified, guardCollect, ProtocolState.modeResolved, ProtocolState.abstained, step, ImplementationPlan.start, newFlight, ProtocolState.freshId, ProtocolState.flight, updateFlight, collectEffect, - done, successful, FlightRec.active, ProtocolState.eligibleCarriers, + done, successful, ProtocolState.flightProtected, FlightRec.active, ProtocolState.eligibleCarriers, ProtocolState.carrierEnabled, ProtocolState.triedCarriers, nextCarrier, Carrier.univ, CarrierSet.get, HecaCapability.detected, Clauses.stageComposition, ProtocolState.reviewStarted, ProtocolState.reviewReady, ProtocolState.batchSettled, @@ -902,12 +980,12 @@ theorem opt_in_unavailable_fallback : intro source _ exposed _ cases source <;> cases exposed <;> simp [optInState, optInCheckState, optInFailed, readyState, ProtocolState.initial, - finish, allowed, guardOpenFlight, guardImplementationFlight, guardFallback, + finish, allowed, guardOpenFlight, ProtocolState.carrierEnabled, guardImplementationFlight, guardFallback, guardBeginImplementation, ImplementationPlan.valid, admitted, guardLaunchViaRunner, guardHostNotified, guardCollect, ProtocolState.modeResolved, ProtocolState.abstained, step, ImplementationPlan.start, newFlight, ProtocolState.freshId, ProtocolState.flight, updateFlight, collectEffect, - done, successful, FlightRec.active, ProtocolState.eligibleCarriers, + done, successful, ProtocolState.flightProtected, FlightRec.active, ProtocolState.eligibleCarriers, ProtocolState.carrierEnabled, ProtocolState.triedCarriers, nextCarrier, Carrier.univ, CarrierSet.get, HecaCapability.detected, Clauses.stageComposition, ProtocolState.reviewStarted, ProtocolState.reviewReady, ProtocolState.batchSettled, @@ -918,25 +996,52 @@ theorem opt_in_unavailable_fallback : theorem opt_in_preserves_heca_lifecycle_fixture : ∀ source ∈ [HecaOptIn.user, .host], ∀ c ∈ Carrier.univ, c ∈ (step { readyState with capabilityChecked := [.codexCli, .nyxidOracle, .isolatedTokenSubagent] } - (.recordHecaCheck ⟨true, source⟩)).capabilityChecked ↔ + (.recordHecaCheck ⟨true, source, false⟩)).capabilityChecked ↔ c ∈ (hecaReady none).capabilityChecked := by decide +-- Explicit disable overrides even sourced opt-in and exposed tools. +example (source : HecaOptIn) (exposed : Bool) : + HecaCapability.detected ⟨exposed, source, true⟩ = false := by + simp [HecaCapability.detected] + +-- A source-supported correction reaches every dispatch consumer through existing enablement. +private def disableEvidence : RevisionEvidence := + { authorizedRevision scopeNote none with hecaDisableCorrection := true } +private def disabledAfterOptIn := step (optInState .host true) (.appendRevision scopeNote disableEvidence) +example : allowed (optInState .host true) (.appendRevision scopeNote disableEvidence) := by + simp [allowed, guardAppendRevision, RevisionEvidence.valid, disableEvidence, authorizedRevision, + ProtocolState.goalWritten, optInState, optInCheckState, readyState, ProtocolState.initial, step] +example : disabledAfterOptIn.carrierEnabled .heca = false := by decide +example : (Clauses.stageComposition 6 (disabledAfterOptIn.carrierEnabled .heca)).contains .heca = false := by decide +example : ¬ allowed (step disabledAfterOptIn (.beginImplementation ⟨["work"], 1, []⟩)) + (.openFlight .implementation .implementation .heca "target" 0) := by + simp [allowed, guardOpenFlight, disabledAfterOptIn, ProtocolState.carrierEnabled, step, + disableEvidence] +example : ¬ allowed (step (optInFailed .host true) (.appendRevision scopeNote disableEvidence)) + (.fallbackFlight 0 .heca) := by + exact disabled_heca_cannot_fallback _ _ (by simp [step, disableEvidence]) +-- Retry/resume cannot launch an existing Heca flight using stale capability records. +example (s : ProtocolState) (id : Nat) (f : FlightRec) + (hf : s.flight id = some f) (hc : f.carrier = .heca) (hd : s.hecaDisabled = true) : + ¬ allowed s (.launchDelegated id) := by + simp [allowed, guardLaunchDelegated, hf, hc, ProtocolState.carrierEnabled, hd] + -- Heca records even an absent check once; it cannot redraw availability later. example (s : ProtocolState) (first second : HecaCapability) : ¬ allowed (step s (.recordHecaCheck first)) (.recordHecaCheck second) := by simp [allowed, guardHecaCheck, step] example (s : ProtocolState) : - (step s (.recordHecaCheck ⟨false, .disabled⟩)).capabilityChecked = s.capabilityChecked := rfl + (step s (.recordHecaCheck ⟨false, .disabled, false⟩)).capabilityChecked = s.capabilityChecked := rfl example (s : ProtocolState) : - Carrier.heca ∈ (step s (.recordHecaCheck ⟨true, .user⟩)).capabilityChecked := by + Carrier.heca ∈ (step s (.recordHecaCheck ⟨true, .user, false⟩)).capabilityChecked := by simp [step, HecaCapability.detected] example : allowed { review with capabilityChecked := Carrier.univ } (.openFlight .review .tests .heca "target" 0) := by - simp only [allowed, guardOpenFlight, guardReviewFlight, ProtocolState.modeResolved, + simp only [allowed, guardOpenFlight, ProtocolState.carrierEnabled, guardReviewFlight, ProtocolState.modeResolved, ProtocolState.abstained] decide @@ -945,7 +1050,7 @@ example (c : ContinuationEntry) : admitted ProtocolState.initial (startupActions simp [admitted, startupActions, allowed, guardWriteGoal, guardAppendRevision, guardAdvanceStage, guardCapabilityCheck, guardHecaCheck, guardResolveMode, HecaCapability.detected, Harness.complete, authorizedRevision, RevisionEvidence.valid, - IntakeEvidence.complete, goal, intake, ProtocolState.initial, ProtocolState.goalWritten, + IntakeEvidence.complete, ActivationAuthority.authorized, goal, intake, ProtocolState.initial, ProtocolState.goalWritten, ProtocolState.modeResolved, ProtocolState.abstained, step, GoalArtifact.correct, Stage.next] example (c : ContinuationEntry) : (run ProtocolState.initial (startupActions c)).gate = applicability c := by rfl @@ -1044,8 +1149,8 @@ theorem heca_termination_collection_admitted : admitted (hecaReady none) hecaTerminationCollectionActions := by simp [admitted, hecaTerminationCollectionActions, hecaSuccessActions, hecaCollectionActions, reviewActions, hecaInitialActions, hecaReady, allowed, guardBeginImplementation, - ImplementationPlan.valid, guardOpenFlight, guardImplementationFlight, guardReviewFlight, - guardLaunchViaRunner, guardLaunchDelegated, guardHostNotified, guardCollect, + ImplementationPlan.valid, guardOpenFlight, ProtocolState.carrierEnabled, guardImplementationFlight, guardReviewFlight, + guardLaunchViaRunner, guardLaunchDelegated, ProtocolState.carrierEnabled, guardHostNotified, guardCollect, guardArchiveHeca, guardRecordImplementation, guardAdvanceStage, guardAppendRevision, guardRecordPassBudget, correctionAction, correctionEvidence, authorizedRevision, continuationRevision, RevisionEvidence.valid, ProtocolState.goalWritten, @@ -1054,7 +1159,7 @@ theorem heca_termination_collection_admitted : ProtocolState.batchSettled, ProtocolState.batchFlights, ProtocolState.flight, ProtocolState.freshId, reviewRoles, seatEligible, canRunRepositoryCommands, step, ImplementationPlan.start, newFlight, updateFlight, recordPendingArchive, - collectEffect, successful, done, FlightRec.active, Carrier.univ, Stage.next, + collectEffect, successful, done, ProtocolState.flightProtected, FlightRec.active, Carrier.univ, Stage.next, FlightStage.protocolStage] set_option maxRecDepth 4096 in @@ -1190,10 +1295,6 @@ example : admitted settled [.appendRevision scopeNote (authorizedRevision scopeN decide -- Actual review table retains ordinary defects (including deliberate test reproductions). -private def ordinary : Finding := - ⟨.reject, ⟨true, true, false, false⟩, false, - ⟨"ordinary typo", "user", .ordinaryOperation, "parsing", none, true⟩⟩ -private def approval : Finding := { ordinary with verdict := .approve } example : routeFindings ordinary approval approval = .fix := by decide private def invented := { ordinary with trigger := { ordinary.trigger with triggerPath := .nonstandardDeliberate } } example : routeFindings invented approval approval = .doneWithAdvisory := by decide @@ -1222,19 +1323,343 @@ example : familyPassAllowed { family with revision := some ⟨"scope", "owner authorization", "none"⟩ } .repairWithRerunReview = true := by decide example : familyRoute { family with noSupportedPath := true } = .honestStop := by decide +-- Workflow provenance is consumed by the actual review and plan-admission routes. +private def manualOnly := { ordinary with trigger := { ordinary.trigger with + inputEvidence := ⟨none, "tool manual describes an optional operation", false⟩ } } +example : routeFindings manualOnly approval approval = .doneWithAdvisory := by decide +example : planElementAdmitted ⟨"manual-only defense", manualOnly, false, true⟩ = false := by decide +private def fixtureOnly := { manualOnly with trigger := { manualOnly.trigger with + inputEvidence := ⟨some ⟨"fixture command", "outside target fixture", 1, false⟩, "", false⟩ } } +example : routeFindings fixtureOnly approval approval = .doneWithAdvisory := by decide +-- A census of zero is not a new restriction on future ordinary workflow states. +private def futureOrdinary := { ordinary with trigger := { ordinary.trigger with + inputEvidence := ⟨some ⟨"read-only census", "target", 0, true⟩, "workflow update path", true⟩ } } +example : routeFindings futureOrdinary approval approval = .fix := by decide +private def ownerRestricted := { futureOrdinary with trigger := { futureOrdinary.trigger with + ownerPolicy := .actualInputOrOccurrence ⟨"owner rule preserved in goal/harness", by decide⟩ } } +example : routeFindings ownerRestricted approval approval = .doneWithAdvisory := by decide +example : routeFindings { ownerRestricted with trigger := { ownerRestricted.trigger with + inputEvidence := ⟨some ⟨"read-only census", "target workflow inputs", 1, true⟩, "", false⟩ } } + approval approval = .fix := by decide +example : routeFindings { ownerRestricted with trigger := { ownerRestricted.trigger with + recordedOccurrence := some "independent incident", createdDuringRun := false } } + approval approval = .fix := by decide +-- A missing source cannot be interpreted as an owner restriction and downgrade a defect. +example : ¬ ∃ source : { s : String // s ≠ "" }, source.val = "" := by + rintro ⟨source, h⟩ + exact source.property h + +-- Every generic blocking route carries the same trigger-aware admission basis. +private def ordinaryBasis : DecisionBasis := ⟨ordinary.input, ordinary.trigger⟩ +private def manualBasis : DecisionBasis := ⟨manualOnly.input, manualOnly.trigger⟩ +example : completeAdmission ordinaryBasis = true := by decide +example : completeAdmission manualBasis = false := by decide +example : downgradeRecord manualBasis "manual-only trigger" = + some (.namedInOwnWords "manual-only trigger" false) := by decide +example : goalGapOf [manualBasis] = [] := by decide +example : goalGapOf [ordinaryBasis] = [ordinaryBasis] := by decide + +private def ordinaryObjection : Objection := + ⟨.parsimony, true, true, false, ordinary.input, ordinary.trigger, "ordinary objection"⟩ +private def manualObjection : Objection := + { ordinaryObjection with trigger := manualOnly.trigger } +example : focusedRoundRequired ordinaryObjection = true := by decide +example : focusedRoundRequired manualObjection = false := by decide + +private def ordinaryDifference : RemainingDifference := + ⟨"ordinary residual", "engineering", ordinary.input, ordinary.trigger, false⟩ +private def manualDifference : RemainingDifference := + ⟨"manual residual", "engineering", manualOnly.input, manualOnly.trigger, false⟩ +example : ordinaryDifference.counts = true := by decide +example : manualDifference.counts = false := by decide + +/-- Exercise existing consumers, not a second admission implementation. -/ +private def blockingConsumerDecisions (f : Finding) : List Bool := + let b : DecisionBasis := ⟨f.input, f.trigger⟩ + let objection : Objection := + ⟨.parsimony, true, true, false, f.input, f.trigger, "basis in its own words"⟩ + let difference : RemainingDifference := + ⟨"remaining goal gap", "engineering", f.input, f.trigger, false⟩ + ([.planObjection, .reviewFinding, .terminationDifference] : List DecisionInputKind).map + (fun k => admissibility k b) ++ + ([.revise, .reject, .abstain, .blockingFinding, .unsatisfied, .concretePlanElement] : + List SoleBasisDecision).map (fun d => mayBeSoleBasis b d) ++ + [routeFindings { f with verdict := .reject } approval approval == .fix, + planElementAdmitted ⟨"goal-required element", f, false, true⟩, + asksMayBlock b, focusedRoundRequired objection, + !(goalGapOf [b]).isEmpty, !(convergencePassScope [b]).isEmpty, + (downgradeRecord b "basis in its own words").isNone, + (declineRecord objection).isNone, + @decide (BlockingFinding.wellFormed ⟨f.input, f.trigger, "S3", .omission⟩) + (by unfold BlockingFinding.wellFormed; infer_instance), + difference.counts, seatAppliesAuthority .unsatisfied b true == .unsatisfied] + +-- A parametric statement covers every failed trigger, independent of label, input +-- conjuncts, owner policy, provenance and incident spelling supplied to the model. +theorem failed_trigger_rejected_by_every_consumer (f : Finding) + (h : triggerCheck f.trigger = false) : + blockingConsumerDecisions f = List.replicate 20 false := by + cases hg : f.input.namesGoalTerm <;> cases he : f.input.namesWorkEvidence <;> + simp [blockingConsumerDecisions, admissibility, mayBeSoleBasis, asksMayBlock, + routeFindings, reviewRoute, downgrade, completeAdmission, h, planElementAdmitted, + focusedRoundRequired, threeConditions, goalGapOf, convergencePassScope, + downgradeRecord, declineRecord, BlockingFinding.wellFormed, RemainingDifference.counts, + seatAppliesAuthority, settleSeat, approval, hg, he] + +theorem admitted_basis_retained_by_every_consumer (f : Finding) + (ha : completeAdmission ⟨f.input, f.trigger⟩ = true) + (hm : f.requiresTrustedMalice = false) (ho : f.requiresOwnerDecision = false) : + blockingConsumerDecisions f = List.replicate 20 true := by + have hf := completeAdmission_requires_force ⟨f.input, f.trigger⟩ ha + have ht : triggerCheck f.trigger = true := by + have hparts := ha + simp [completeAdmission] at hparts + exact hparts.2 + simp [blockingConsumerDecisions, admissibility, mayBeSoleBasis, asksMayBlock, + routeFindings, reviewRoute, downgrade, completeAdmission, hf, ht, hm, ho, + planElementAdmitted, focusedRoundRequired, threeConditions, goalGapOf, + convergencePassScope, downgradeRecord, declineRecord, BlockingFinding.wellFormed, + RemainingDifference.counts, seatAppliesAuthority, settleSeat, approval, threatEligible] + +private def observedRestricted : Finding := + { ownerRestricted with trigger := { ownerRestricted.trigger with + inputEvidence := ⟨some ⟨"read-only census", "target workflow inputs", 1, true⟩, "", false⟩ } } +private def independentRestricted : Finding := + { ownerRestricted with trigger := { ownerRestricted.trigger with + recordedOccurrence := some "independent incident", createdDuringRun := false } } + +-- Nine constructed evidence classes, each checked at all twenty decisions. These +-- fixtures establish model behavior, never observed host occurrence or provenance. +example : ([manualOnly, fixtureOnly, invented, ownerRestricted, + { invented with trigger := { invented.trigger with + recordedOccurrence := some "fixture made during this run" } }] : List Finding).all + (fun f => blockingConsumerDecisions f == List.replicate 20 false) = true := by decide +example : ([ordinary, futureOrdinary, observedRestricted, independentRestricted] : List Finding).all + (fun f => blockingConsumerDecisions f == List.replicate 20 true) = true := by decide + +-- Paraphrase reaches the production paid-pass guard, not a separate classifier. +private theorem fundedRepairAdmission (e : FamilyEvidence) : + allowed funded (.pass .repairWithRerunReview e (some twoParts)) ↔ + familyPassAllowed e .repairWithRerunReview = true := by + have hs : funded.stage = .fixOrDone := by decide + have hr : funded.reviewComplete = true := by decide + have hb : funded.passBudget = some 1 := by decide + simp [allowed, guardPass, hs, hr, hb, twoParts, ImplementationPlan.valid, ImplementationPlan.repairsAdmitted, ordinary, downgrade, completeAdmission, eligible, triggerCheck, force, + WorkflowInputEvidence.ordinary, WorkflowInputEvidence.observed, occurrenceIsIndependent, + OwnerAdmissionPolicy.admits, Transition.counted] + +-- Inactive recurrence alone cannot make an unresolved comparison a new family. +private def unresolvedComparison := { firstFamily with correspondence := + { firstFamily.correspondence with history := .priorComparison "candidate prior label" true true false } } +example : classGateActive unresolvedComparison = false ∧ + familyRoute unresolvedComparison = .reviseOrInvestigate := by decide +example : ¬ allowed funded (.pass .repairWithRerunReview unresolvedComparison (some twoParts)) := by + rw [fundedRepairAdmission] + decide +example : allowed funded (.pass .metaLayerConvergence unresolvedComparison none) := by + have hs : funded.stage = .fixOrDone := by decide + have hr : funded.reviewComplete = true := by decide + have hb : funded.passBudget = some 1 := by decide + simp [allowed, guardPass, hs, hr, hb, familyPassAllowed, familyRoute, + unresolvedComparison, firstFamily, ordinary, family, FamilyCorrespondence.verified, + ownerAuthorizedDomainChange, Transition.counted] + +-- Evidence for a genuinely new family is still required at the same repair consumer. +example : ¬ allowed funded (.pass .repairWithRerunReview + { firstFamily with correspondence := { firstFamily.correspondence with history := .newFamily "" } } + (some twoParts)) := by + rw [fundedRepairAdmission] + decide +example : ¬ allowed funded (.pass .repairWithRerunReview + { firstFamily with correspondence := { firstFamily.correspondence with evidence := "" } } + (some twoParts)) := by + rw [fundedRepairAdmission] + decide +example : ¬ allowed funded (.pass .repairWithRerunReview + { firstFamily with correspondence := { firstFamily.correspondence with peerFree := false } } + (some twoParts)) := by + rw [fundedRepairAdmission] + decide + +-- Earlier unsupported enumeration activates the existing gate even for a new family. +private def firstFamilyUnsupported := { firstFamily with earlierUnsupportedEnumeration := true } +example : classGateActive firstFamilyUnsupported = true := by decide +example : ¬ allowed funded (.pass .repairWithRerunReview firstFamilyUnsupported (some twoParts)) := by + rw [fundedRepairAdmission] + decide +example : allowed funded (.pass .repairWithRerunReview + { firstFamilyUnsupported with coverageBasis := .soundAbstraction true } (some twoParts)) := by + rw [fundedRepairAdmission] + decide +example : ¬ allowed funded (.pass .repairWithRerunReview + { firstFamily with changesDomainOrCriterion := true } (some twoParts)) := by + rw [fundedRepairAdmission] + decide + +private def paraphrasedFamily := { family with coverageBasis := .unsupportedMemberEnumeration } +example : paraphrasedFamily.correspondence.history = .priorComparison "prior label" true true true ∧ + paraphrasedFamily.correspondence.currentLabel = "current paraphrase" := by decide +example : classGateActive paraphrasedFamily = true := by decide +example : allowed funded (.pass .repairWithRerunReview family (some twoParts)) := by + rw [fundedRepairAdmission] + decide +example : ¬ allowed funded (.pass .repairWithRerunReview paraphrasedFamily (some twoParts)) := by + exact unsupported_class_cannot_start_batch funded paraphrasedFamily (some twoParts) rfl (by decide) +-- Supplied incident labels are evidence inputs, not independently replayed host events. +private def incidentLabels : List String := + ["lake_manifest_exemption_discards_dependency_local_state", + "nested-git-boundary bypass leaves dependency-owned submodule/worktree metadata outside local-history coverage", + "lake_dependency_recovery_roots_omit_reflogs", "unversioned_git_metadata", + "lake_dependency_metadata_content_outside_git_object_graph"] +example : ∀ label ∈ incidentLabels, + familyPassAllowed { paraphrasedFamily with correspondence := + { paraphrasedFamily.correspondence with currentLabel := label } } + .repairWithRerunReview = false := by decide + +-- Same location is immaterial; a different cause remains distinct. +private def distinctCause := { paraphrasedFamily with correspondence := + { paraphrasedFamily.correspondence with history := .priorComparison "prior label" true false true } } +example : classGateActive distinctCause = false := by decide +example : allowed funded (.pass .repairWithRerunReview distinctCause (some twoParts)) := by + have hs : funded.stage = .fixOrDone := by decide + have hr : funded.reviewComplete = true := by decide + have hb : funded.passBudget = some 1 := by decide + simp [allowed, guardPass, hs, hr, hb, distinctCause, paraphrasedFamily, family, + familyPassAllowed, familyRoute, ownerAuthorizedDomainChange, classGateActive, + FamilyCorrespondence.verified, FamilyCorrespondence.sameFamily, twoParts, + ImplementationPlan.valid, ImplementationPlan.repairsAdmitted, ordinary, downgrade, completeAdmission, eligible, triggerCheck, force, + WorkflowInputEvidence.ordinary, WorkflowInputEvidence.observed, occurrenceIsIndependent, + OwnerAdmissionPolicy.admits, Transition.counted] +example : familyPassAllowed { family with correspondence := + { family.correspondence with history := .priorComparison "prior label" true true false } } + .repairWithRerunReview = false := by decide +example : familyPassAllowed { family with correspondence := + { family.correspondence with peerFree := false } } .repairWithRerunReview = false := by decide + +example : familyPassAllowed { family with inputCorrespondenceVerified := false } + .repairWithRerunReview = false := by decide +example : familyPassAllowed { family with measurementLimitsReported := false } + .repairWithRerunReview = false := by decide +example : ¬ allowed funded (.pass .repairWithRerunReview + { family with inputCorrespondenceVerified := false } (some twoParts)) := by + rw [fundedRepairAdmission] + decide +example : ¬ allowed funded (.pass .repairWithRerunReview + { family with measurementLimitsReported := false } (some twoParts)) := by + rw [fundedRepairAdmission] + decide + -- Autonomous intake proceeds from honest sources even when continuation is silent/ambiguous. example : allowed ProtocolState.initial (.writeGoal goal (intake .silent)) := by - simp [allowed, guardWriteGoal, IntakeEvidence.complete, Harness.complete, ProtocolState.initial, intake, goal] + simp [allowed, guardWriteGoal, IntakeEvidence.complete, ActivationAuthority.authorized, Harness.complete, ProtocolState.initial, intake, goal] example : allowed ProtocolState.initial (.writeGoal goal (intake .ambiguous)) := by - simp [allowed, guardWriteGoal, IntakeEvidence.complete, Harness.complete, ProtocolState.initial, intake, goal] + simp [allowed, guardWriteGoal, IntakeEvidence.complete, ActivationAuthority.authorized, Harness.complete, ProtocolState.initial, intake, goal] example : ¬ allowed ProtocolState.initial (.writeGoal goal { intake .silent with startupQuestionAsked := true }) := by - simp [allowed, guardWriteGoal, IntakeEvidence.complete] + simp [allowed, guardWriteGoal, IntakeEvidence.complete, intake] example : ¬ allowed ProtocolState.initial (.writeGoal goal { intake .silent with explicitBoundariesPreserved := false }) := by - simp [allowed, guardWriteGoal, IntakeEvidence.complete] + simp [allowed, guardWriteGoal, IntakeEvidence.complete, intake] example : (step ProtocolState.initial (.writeGoal goal (intake .silent))).gate = .inapplicable := by decide example : (step ProtocolState.initial (.writeGoal goal (intake .ambiguous))).gate = .withholdClaim := by decide example : (step ProtocolState.initial (.writeGoal goal (intake .present))).gate = .applies := by decide +-- #1075: authority is consumed by actual intake; risk/importance alone supplies none. +example : ¬ allowed ProtocolState.initial (.writeGoal goal + { intake .silent with activation := .absent }) := by + simp [allowed, guardWriteGoal, IntakeEvidence.complete, ActivationAuthority.authorized] +example : allowed ProtocolState.initial (.writeGoal goal + { intake .silent with activation := .explicitRequest }) := by + simp [allowed, guardWriteGoal, IntakeEvidence.complete, ActivationAuthority.authorized, + Harness.complete, ProtocolState.initial, intake, goal] +-- A material owner question is permitted; dependent intake waits for its answer. +example : ¬ allowed ProtocolState.initial (.writeGoal goal + { intake .silent with startupQuestionAsked := true, materialOwnerQuestion := true }) := by + simp [allowed, guardWriteGoal, IntakeEvidence.complete, intake] +example : allowed ProtocolState.initial (.writeGoal goal + { intake .silent with + startupQuestionAsked := true + materialOwnerQuestion := true + ownerClarified := true }) := by + simp [allowed, guardWriteGoal, IntakeEvidence.complete, ActivationAuthority.authorized, + Harness.complete, ProtocolState.initial, intake, goal] + +private def uncertain (status : EvidenceStatus) : Finding := + { ordinary with input := { ordinary.input with evidenceStatus := status } } +example : ([.advisory, .conditional, .unverified] : List EvidenceStatus).all (fun status => + routeFindings (uncertain status) approval approval == .doneWithAdvisory && + !planElementAdmitted ⟨"new approval layer", uncertain status, true, true⟩) = true := by decide +example (status : EvidenceStatus) (h : status ≠ .confirmed) : + ¬ allowed funded (.pass .repairWithRerunReview firstFamily + (some { twoParts with repairFindings := [uncertain status] })) := by + apply unadmitted_repairs_cannot_pass + simp [ImplementationPlan.repairsAdmitted, uncertain, downgrade, completeAdmission, force, h, ordinary] +example : routeFindings { ordinary with input := { ordinary.input with userGoalBasis := "" } } + approval approval = .doneWithAdvisory := by decide +example : ¬ allowed funded (.pass .repairWithRerunReview firstFamily + (some { twoParts with repairFindings := [{ ordinary with requiresOwnerDecision := true }] })) := by + apply unadmitted_repairs_cannot_pass + decide +-- Confirmed ordinary defects, confirmed missing required evidence and confirmed disputed +-- interpretations retain the real review/repair path. A fixture alone still does not. +example : routeFindings { ordinary with input := { ordinary.input with basisDisputed := true } } + approval approval = .fix := by decide +example : allowed funded (.pass .repairWithRerunReview firstFamily (some twoParts)) := + (fundedRepairAdmission firstFamily).mpr (by decide) + +private def scopeCorrection : Revision := + ⟨"compose existing grants only; cancel dependent approval-system work", "current user", "dependent plan/reviews/repairs"⟩ +private def scopeCorrectionEvidence : RevisionEvidence := + { authorizedRevision scopeCorrection none with invalidatesWork := true } +private def scopeCorrected (s : ProtocolState) := + step s (.appendRevision scopeCorrection scopeCorrectionEvidence) +example : allowed funded (.appendRevision scopeCorrection scopeCorrectionEvidence) := by + refine ⟨?_, rfl, rfl, rfl⟩ + change funded.goal.isSome = true + decide +example (s : ProtocolState) : (scopeCorrected s).flights = s.flights ∧ + (scopeCorrected s).passBudget = s.passBudget ∧ (scopeCorrected s).batch = none := ⟨rfl, rfl, rfl⟩ +example : (scopeCorrected funded).reviewComplete = false := by decide +example : ¬ allowed (scopeCorrected funded) .claimSatisfied := by + simp [allowed, guardClaimSatisfied, scopeCorrected, step, scopeCorrectionEvidence] +example : ¬ allowed (scopeCorrected funded) (.pass .repairWithRerunReview firstFamily (some twoParts)) := by + simp [allowed, guardPass, scopeCorrected, step, scopeCorrectionEvidence] +example : ¬ allowed (scopeCorrected complete) (.openFlight .review .architecture .codexCli "target" 0) := by + simp [allowed, guardOpenFlight, guardReviewFlight, scopeCorrected, step, scopeCorrectionEvidence] +-- A pending old assignment cannot launch; an already launched job remains protected. +example : ¬ allowed (scopeCorrected opened) (.launchViaRunner 0) := by + simp [allowed, guardLaunchViaRunner, scopeCorrected, step, scopeCorrectionEvidence, + opened, begin, readyState, ProtocolState.initial, ProtocolState.freshId, + ProtocolState.flight, newFlight] +example : (scopeCorrected opened).activeOn "target" = false := by decide +private def activeOld := step opened (.launchViaRunner 0) +example : (scopeCorrected activeOld).activeOn "target" = true := by decide +example : ¬ allowed (scopeCorrected activeOld) (.mutateTarget "target") := by + simp only [allowed, guardMutateTarget] + decide +example : (scopeCorrected activeOld).stage = .thinkingPanel := rfl +example : ¬ allowed (scopeCorrected activeOld) .advanceStage := by + have protectionObserved : ((scopeCorrected activeOld).flights.all fun f => + !(scopeCorrected activeOld).flightProtected f) = false := by decide + simp [allowed, guardAdvanceStage, protectionObserved] +example : (scopeCorrected (finish opened 0 successful)).activeOn "target" = false := by decide +-- An unrelated sourced revision preserves valid candidate evidence and readiness. +example : (step complete (.appendRevision scopeNote (authorizedRevision scopeNote none))).reviewReady = true := by decide + +-- Goal corrections invalidate claim evidence even without changing the host declaration. +example : (scopeCorrected settled).gate = settled.gate := by decide +example : (scopeCorrected settled).terminationExit = settled.terminationExit ∧ + (scopeCorrected settled).terminationAuthority = settled.terminationAuthority := by + simpa only [scopeCorrected] using + correction_keeps_settlement settled scopeCorrection scopeCorrectionEvidence +example : (scopeCorrected settled).continuationAuthority ≠ settled.continuationAuthority := by decide +example (source : ClaimSource) (e : TerminationEvidence) + (old : e.authority = settled.continuationAuthority) : + ¬ allowed (scopeCorrected settled) (.evaluateTermination source e) := by + apply stale_evidence_cannot_evaluate + rw [old] + decide +example : ¬ allowed (scopeCorrected settled) (.recordImplementation 0 ["contract"] true) := by + simp [allowed, guardRecordImplementation, scopeCorrected, step, scopeCorrectionEvidence] + end Sshx.Behavior.Scenarios diff --git a/skills/sshx/formal/Sshx/Blocking.lean b/skills/sshx/formal/Sshx/Blocking.lean index 8b266ed7..8a1c6acf 100644 --- a/skills/sshx/formal/Sshx/Blocking.lean +++ b/skills/sshx/formal/Sshx/Blocking.lean @@ -9,6 +9,14 @@ downgrade sentence of `## Review Truth Table`. namespace Sshx +-- SKILL[def]: "Admission additionally requires `evidence_status=confirmed` and a sourced `user_goal_basis`" +inductive EvidenceStatus + | confirmed + | advisory + | conditional + | unverified + deriving DecidableEq, Repr + /-- What a decision input names, as `BlockingAuthority` reads it. -/ structure Input where /-- Conjunct 1: a `normalized_goal`, `constraints`, or `success_criteria` term the work fails. -/ @@ -19,6 +27,8 @@ structure Input where basisShownFalse : Bool /-- A disputed basis is not an absent basis. -/ basisDisputed : Bool + evidenceStatus : EvidenceStatus := .unverified + userGoalBasis : String := "" deriving DecidableEq, Repr inductive Force @@ -32,6 +42,52 @@ inductive TriggerPath | malicious deriving DecidableEq, Repr +/-- Projection of a read-only measurement of workflow inputs, not a review fixture. +Truth of provenance, scope and the workflow correspondence remains a supplied premise. -/ +structure EnvironmentObservation where + command : String + scope : String + count : Nat + actualWorkflowInput : Bool + deriving DecidableEq, Repr + +def EnvironmentObservation.establishesInput (o : EnvironmentObservation) : Bool := + o.command != "" && o.scope != "" && decide (0 < o.count) && o.actualWorkflowInput + +/-- A manual's capability statement is not a workflow derivation. The semantic +classification and owner source are interpreted evidence, not inferred from English. -/ +-- SKILL[def]: "A tool manual or review fixture alone proves capability/reachability, never ordinary workflow input or occurrence." +-- SKILL[ref]: "Missing/disputed provenance is an evidence gap, never an invented restriction." +structure WorkflowInputEvidence where + observation : Option EnvironmentObservation + workflowSource : String + workflowDerived : Bool + deriving DecidableEq, Repr + +def WorkflowInputEvidence.observed (e : WorkflowInputEvidence) : Bool := + e.observation.any (·.establishesInput) + +def WorkflowInputEvidence.ordinary (e : WorkflowInputEvidence) : Bool := + e.observed || (e.workflowSource != "" && e.workflowDerived) + +inductive OwnerAdmissionPolicy + | unrestricted + | actualInputOrOccurrence (source : { s : String // s ≠ "" }) + deriving DecidableEq, Repr + +def OwnerAdmissionPolicy.admits (p : OwnerAdmissionPolicy) (observed occurrence : Bool) : Bool := + match p with + | .unrestricted => true + | .actualInputOrOccurrence _ => observed || occurrence + +/-- Structured projection of family_basis; semantic correspondence is judged from +settled summaries by the existing class gate, never by the label string. -/ +structure FamilyBasis where + failedProperty : String + causalMechanism : String + correspondenceEvidence : String + deriving DecidableEq, Repr + structure TriggerRecord where trigger : String triggerActor : String @@ -39,36 +95,68 @@ structure TriggerRecord where mechanismFamily : String recordedOccurrence : Option String createdDuringRun : Bool + inputEvidence : WorkflowInputEvidence + ownerPolicy : OwnerAdmissionPolicy + familyBasis : FamilyBasis deriving DecidableEq, Repr --- SKILL[def]: "A blocking finding must also pass the structured trigger check" +-- SKILL[def]: "`recorded_occurrence` must have existed before this run" def occurrenceIsIndependent (recordedOccurrence : Option String) (createdDuringRun : Bool) : Bool := recordedOccurrence.isSome && !createdDuringRun --- SKILL[def]: "`recorded_occurrence` must have existed before this run" +-- SKILL[def]: "Without workflow grounding, require independent `recorded_occurrence`, else advisory." +-- SKILL[ref]: "Apply sourced owner restrictions from `GoalArtifact`: actual-input-or-occurrence-only additionally requires observed actual input or independent occurrence; absent that rule, future ordinary workflow-produced inputs remain eligible." +-- SKILL[def]: "A blocking finding must also pass the structured trigger check" def triggerCheck (record : TriggerRecord) : Bool := - match record.triggerPath with - | .ordinaryOperation => true - | .nonstandardDeliberate | .malicious => - occurrenceIsIndependent record.recordedOccurrence record.createdDuringRun + let occurrence := occurrenceIsIndependent record.recordedOccurrence record.createdDuringRun + let ordinary := record.triggerPath == .ordinaryOperation && record.inputEvidence.ordinary + (ordinary || occurrence) && record.ownerPolicy.admits record.inputEvidence.observed occurrence --- SKILL[thm]: "a fixture, reproduction, or state deliberately created by a seat, caller, or repair worker during this run is reachability evidence only" +-- SKILL[thm]: "deliberately constructed run fixtures/reproductions/states are reachability evidence only" theorem run_fixture_is_not_occurrence (createdDuringRun : Bool) : occurrenceIsIndependent none createdDuringRun = false := by simp [occurrenceIsIndependent] --- SKILL[def]: "Advisory is the default; blocking is the exception, and the exception has exactly two conjuncts that the input itself must name" +-- SKILL[def]: "Advisory is the default; blocking is the exception, with exactly two conjuncts the input itself must name" /-- `BlockingAuthority`: advisory is the default; blocking needs both named conjuncts. -/ def force (i : Input) : Force := - if i.namesGoalTerm && i.namesWorkEvidence && !i.basisShownFalse then .blocking else .advisory + if i.namesGoalTerm && i.namesWorkEvidence && !i.basisShownFalse && + i.evidenceStatus == .confirmed && i.userGoalBasis != "" then .blocking else .advisory + +/-- A decision basis keeps the trigger provenance beside the two conjuncts. Any +blocking consumer must use this projection rather than a bare `Input`. -/ +structure DecisionBasis where + input : Input + trigger : TriggerRecord + deriving DecidableEq, Repr + +-- SKILL[ref]: "workflow grounding and owner-policy compliance remain trigger-check premises" +def completeAdmission (b : DecisionBasis) : Bool := + force b.input == .blocking && triggerCheck b.trigger + +theorem completeAdmission_requires_force (b : DecisionBasis) + (h : completeAdmission b = true) : force b.input = .blocking := by + simp [completeAdmission] at h + exact h.1 + +theorem failed_trigger_is_not_admitted (b : DecisionBasis) + (h : triggerCheck b.trigger = false) : completeAdmission b = false := by + simp [completeAdmission, h] theorem force_blocking_iff (i : Input) : force i = .blocking ↔ - i.namesGoalTerm = true ∧ i.namesWorkEvidence = true ∧ i.basisShownFalse = false := by - cases i with - | mk a b c d => cases a <;> cases b <;> cases c <;> cases d <;> simp [force] + i.namesGoalTerm = true ∧ i.namesWorkEvidence = true ∧ i.basisShownFalse = false ∧ + i.evidenceStatus = .confirmed ∧ i.userGoalBasis ≠ "" := by + simp [force, Bool.and_eq_true, bne_iff_ne] + +-- SKILL[ref]: "Advisory/conditional/unverified findings create no blockers or automatic repairs" +theorem unconfirmed_is_advisory (i : Input) (h : i.evidenceStatus ≠ .confirmed) : + force i = .advisory := by + simp [force, h] /-- Disputed grounding is not absent grounding: the dispute flag never changes the force. -/ +-- SKILL[ref]: "Evidence showing a basis false removes it; a confirmed basis with disputed correctness retains full force until evidence settles it, never downgrade for being unpersuasive." +-- SKILL[ref]: "Dispute preserves confirmed defects; unsupported premises are not confirmed." theorem force_ignores_dispute (i : Input) (b : Bool) : force { i with basisDisputed := b } = force i := by simp [force] @@ -93,6 +181,7 @@ structure Finding where input : Input requiresTrustedMalice : Bool trigger : TriggerRecord + requiresOwnerDecision : Bool := false deriving DecidableEq, Repr -- SKILL[def]: "ask whether a finding would exist only if a role declared trusted by `harness.trust_boundary` deliberately acted maliciously; if so, the finding is ineligible" @@ -103,7 +192,8 @@ def eligible (f : Finding) : Bool := !f.requiresTrustedMalice && triggerCheck f. /-- `## Review Truth Table`: a blocking finding that fails either check is an advisory. -/ def downgrade (f : Finding) : ReviewVerdict := match f.verdict with - | .reject => if eligible f && (force f.input == .blocking) then .reject else .comment + | .reject => + if !f.requiresTrustedMalice && completeAdmission ⟨f.input, f.trigger⟩ then .reject else .comment | .approve => .approve | .comment => .comment @@ -112,28 +202,27 @@ theorem downgrade_reject_iff (f : Finding) : downgrade f = .reject ↔ f.verdict = .reject ∧ eligible f = true ∧ force f.input = .blocking := by cases f with - | mk v i m tr => + | mk v i m tr owner => cases v <;> cases m <;> cases hf : force i <;> cases ht : triggerCheck tr <;> - simp [downgrade, eligible, hf, ht] + simp [downgrade, completeAdmission, eligible, hf, ht] theorem downgrade_approve_iff (f : Finding) : downgrade f = .approve ↔ f.verdict = .approve := by cases f with - | mk v i m tr => cases v <;> cases m <;> cases hf : force i <;> cases ht : triggerCheck tr <;> - simp [downgrade, eligible, hf, ht] + | mk v i m tr owner => cases v <;> cases m <;> cases hf : force i <;> cases ht : triggerCheck tr <;> + simp [downgrade, completeAdmission, eligible, hf, ht] /-- Downgrade is idempotent: routing "again" after a downgrade changes nothing further. -/ theorem downgrade_idempotent (f : Finding) : downgrade { f with verdict := downgrade f } = downgrade f := by cases f with - | mk v i m tr => cases v <;> cases m <;> cases hf : force i <;> cases ht : triggerCheck tr <;> - simp [downgrade, eligible, hf, ht] + | mk v i m tr owner => cases v <;> cases m <;> cases hf : force i <;> cases ht : triggerCheck tr <;> + simp [downgrade, completeAdmission, eligible, hf, ht] theorem ordinary_reachable_finding_stays_blocking (f : Finding) (hv : f.verdict = .reject) (hi : force f.input = .blocking) (hm : f.requiresTrustedMalice = false) - (hp : f.trigger.triggerPath = .ordinaryOperation) : + (ht : triggerCheck f.trigger = true) : downgrade f = .reject := by - rw [downgrade] - simp [hv, hi, eligible, hm, triggerCheck, hp] + simp [downgrade, completeAdmission, hv, hi, hm, ht] end Sshx diff --git a/skills/sshx/formal/Sshx/Carrier.lean b/skills/sshx/formal/Sshx/Carrier.lean index 92f52085..9390dd57 100644 --- a/skills/sshx/formal/Sshx/Carrier.lean +++ b/skills/sshx/formal/Sshx/Carrier.lean @@ -23,10 +23,11 @@ inductive HecaOptIn structure HecaCapability where callerToolsExposed : Bool optIn : HecaOptIn := .disabled + explicitlyDisabled : Bool := false deriving DecidableEq, Repr def HecaCapability.detected (facts : HecaCapability) : Bool := - facts.optIn != .disabled && facts.callerToolsExposed + !facts.explicitlyDisabled && facts.optIn != .disabled && facts.callerToolsExposed /-- The closed carrier set of `## Boundaries`. -/ inductive Carrier diff --git a/skills/sshx/formal/Sshx/Clauses/Boundaries.lean b/skills/sshx/formal/Sshx/Clauses/Boundaries.lean index a6b49a32..48953e08 100644 --- a/skills/sshx/formal/Sshx/Clauses/Boundaries.lean +++ b/skills/sshx/formal/Sshx/Clauses/Boundaries.lean @@ -81,14 +81,14 @@ def carrierHasControllerAuthority (_ : Carrier) : Bool := false /-! ## Baseline failure modes -/ --- SKILL[def]: "Without this skill, lightweight high-risk decisions tend to regress to these source-owned classes:" --- SKILL[def]: "- fake consensus: self-application, pseudo-isolation, missing worker-mode declaration, or caller self-certification in place of the fixed thinking, review, and termination rosters;" --- SKILL[def]: "- false grounding: unverified premises, retrospective fit, imagined relevance, or a mathematical name whose hypotheses the recorded mechanism state does not instantiate;" --- SKILL[def]: "- rabbit-holing: blocking by default, peripheral detail, repeated unchanged work, finite case registers, procedural findings against the run's own records, or per-case diagnosis after one declared absorber already determines the goal-visible route;" +-- SKILL[def]: "Source-owned no-skill failure classes:" +-- SKILL[def]: "- fake consensus: self-application, pseudo-isolation, undeclared worker mode, self-certification;" +-- SKILL[def]: "- false grounding: unverified premises, retrospective fit, imagined relevance;" +-- SKILL[def]: "- rabbit-holing: default blocking, peripheral/repeated work, case registers, procedural findings;" -- SKILL[def]: "- goal loss: 忘记目标 drift to an unranked target, 因小失大 a part served at the whole's cost, or 买椟还珠 form held above substance;" --- SKILL[def]: "- wrong convergence: beauty without worth, scalarized incomparable candidates, path-dependent gain on non-additive coordinates, or spawn acknowledgments, budget and lifecycle milestones presented as completion;" --- SKILL[def]: "- contaminated adjudication: same-round peer evidence, an out-of-prefix ledger event, or dependency-reaching evidence presented as independent;" --- SKILL[def]: "- boundary drift: carrier diversity over-claims, improvised worker mechanics, or daemon, GitHub, git, label, and release orchestration for an inline decision." +-- SKILL[def]: "- wrong convergence: beauty without worth, scalarized incomparability, non-additive path gain, false completion proxies;" +-- SKILL[def]: "- contaminated adjudication: peer/out-of-prefix/dependency-reaching evidence presented as independent;" +-- SKILL[def]: "- boundary drift: diversity overclaims, improvised mechanics, unauthorized lifecycle;" inductive BaselineFailure | fakeConsensus | falseGrounding @@ -98,11 +98,14 @@ inductive BaselineFailure | contaminatedAdjudication | boundaryDrift | forcedIntakeConfirmation + | scopeExpansion deriving DecidableEq, Repr --- SKILL[def]: "- forced intake confirmation: routine harness or boundary details turned into a startup question instead of a recorded, source-backed engineering assumption." +-- SKILL[def]: "- forced intake confirmation: routine questions replacing sourced assumptions;" +-- SKILL[def]: "- scope expansion: risk activation, uncertain repairs, stale obligations after correction." /-- The model object that guards each baseline class. -/ def guardedBy : BaselineFailure → String + | .scopeExpansion => "Sshx.Behavior.guardWriteGoal, Sshx.force, Sshx.Behavior.guardAppendRevision" | .fakeConsensus => "Sshx.caller_never_consensus, Sshx.fake_roster_rejected" | .falseGrounding => "Sshx.Reasoning.analogy_has_no_force, Sshx.Reasoning.explicit_excludes_silent_reliance" | .rabbitHoling => "Sshx.force_blocking_iff, Sshx.Reasoning.shallowest_is_the_standard" @@ -136,7 +139,7 @@ def contractTestFile : String := "skills/sshx/tests/test_sshx_contract.py" -- SKILL[ref]: "Before adding or changing this skill, record the no-skill failure mode as source-owned contract or test evidence." abbrev noSkillFailureModes := BaselineFailure --- SKILL[ref]: "When a new failure case appears, prefer widening or verifying the absorber that already covers its class to adding another case entry: when a verified finite construction hypothesis applies, its register cannot be completed, while an open or infinite domain still needs a class-coverage basis; every entry added must be held true by every later change." +-- SKILL[ref]: "For new failures prefer verifying/widening the class absorber over case entries: verified finite-construction hypotheses defeat register closure; open/infinite domains still need class coverage, and every added entry binds later changes." abbrev registerCannotBeCompleted := @Semantics.every_register_escaped /-- What may be tracked as published skill source. -/ diff --git a/skills/sshx/formal/Sshx/Clauses/Contract.lean b/skills/sshx/formal/Sshx/Clauses/Contract.lean index b81182f7..966636c7 100644 --- a/skills/sshx/formal/Sshx/Clauses/Contract.lean +++ b/skills/sshx/formal/Sshx/Clauses/Contract.lean @@ -35,27 +35,15 @@ def sshxShape : SkillShape := ⟨true, true, true, true, true, false, false⟩ /-! ## Trigger -/ --- SKILL[def]: "Use this skill when:" --- SKILL[def]: "- a decision has meaningful product, architecture, correctness, safety, or cost risk;" --- SKILL[def]: "- the user asks for multi-angle thinking, consensus, or review without starting a long-running work-unit loop;" --- SKILL[def]: "- a concrete plan should be tested against independent perspectives before implementation;" --- SKILL[def]: "- a finished change should pass a same-shape review gate before declaring done." -inductive TriggerCondition - | meaningfulRisk - | multiAngleRequest - | planNeedsIndependentTest - | changeNeedsReviewGate - deriving DecidableEq, Repr - --- SKILL[def]: "Do not use this skill for routine one-step answers where no separate perspectives would change the outcome, and do not run it when the decision's stakes cannot justify the protocol's cost: whether to run it follows decision risk, not available budget." -/-- Whether to run follows decision risk and whether perspectives change the outcome; the -available budget is not an input. -/ -def shouldRun (triggered : Bool) (perspectivesChangeOutcome : Bool) (stakesJustifyCost : Bool) : - Bool := - triggered && perspectivesChangeOutcome && stakesJustifyCost +-- SKILL[def]: "Risk, importance, tools, budget or generic implementation/architecture review alone never activate sshx; use ordinary work." +-- SKILL[def]: "Within authorization, require perspectives that can change the outcome and stakes that justify cost." +-- SKILL[ref]: "Risk informs proportionality, never supplies authorization." +def shouldRun (authority : ActivationAuthority) (perspectivesChangeOutcome : Bool) + (stakesJustifyCost : Bool) : Bool := + authority.authorized && perspectivesChangeOutcome && stakesJustifyCost -theorem run_follows_risk_not_budget (t p s : Bool) (budget : Nat) : - shouldRun t p s = shouldRun t p s ∧ budget = budget := ⟨rfl, rfl⟩ +theorem risk_alone_never_activates (p s : Bool) : shouldRun .absent p s = false := by + simp [shouldRun, ActivationAuthority.authorized] /-! ## Goal contract: harness, gate entry, goal source, iteration question -/ @@ -134,7 +122,7 @@ inductive CallerDuty -- SKILL[def]: "The caller context may intake, choose worker mode, dispatch workers, meta-judge returned `SshxResultEnvelope.conclusion` values, and aggregate and report conclusions only, retaining `log_ref` references." def callerMay (_ : CallerDuty) : Bool := true --- SKILL[ref]: "Each `visible_inputs` value must include the complete `GoalArtifact` (including `harness`) and must not include same-round peer outputs." +-- SKILL[ref]: "Each `visible_inputs` includes complete `GoalArtifact`/`harness`, never same-round peer output." abbrev visibleInputsRule := @visible /-! ## Implementation worker -/ @@ -153,14 +141,14 @@ structure ImplementationRequirement where framing : String deriving DecidableEq, Repr --- SKILL[def]: "No caller recipes (steps, code/pseudocode, structures or algorithms), even as consensus, acceptance or prohibitions." --- SKILL[def]: "Preserve user/host technical requirements with their sources." +-- SKILL[def]: "No caller recipes (steps, code/pseudocode, structures/algorithms), even as consensus/acceptance/prohibitions." +-- SKILL[def]: "Preserve sourced user/host requirements" def ImplementationRequirement.binding (r : ImplementationRequirement) : Bool := r.source != .callerMechanics && r.sourceRef != "" /-- Semantic judgments supplied by evidence and independent review, not runtime fields. -/ --- SKILL[def]: "Send goal, verifiable acceptance, authorized scope/prohibitions and grounded context/evidence." --- SKILL[def]: "Workers inspect the target and choose mechanics;" +-- SKILL[def]: "Send goal, verifiable acceptance, scope/prohibitions and grounded evidence." +-- SKILL[def]: "Workers inspect and choose mechanics;" structure ImplementationBrief where planApprovedByThinkingGate : Bool goalAndAcceptancePassed : Bool @@ -171,7 +159,7 @@ structure ImplementationBrief where boundaryNarrow : Bool deriving DecidableEq, Repr --- SKILL[def]: "Thinking-gate approval binds outcomes, scope and requirements before implementation." +-- SKILL[def]: "Thinking approval binds outcomes/scope/requirements." def implementationAllowed (b : ImplementationBrief) : Bool := b.planApprovedByThinkingGate def implementationConforming (b : ImplementationBrief) : Bool := @@ -187,11 +175,11 @@ structure ImplementationChange where internalApproachChanged : Bool deriving DecidableEq, Repr --- SKILL[def]: "Report goal, authority or constraint changes before acting via existing correction, direction and class gates." +-- SKILL[def]: "report goal/authority/constraint changes before acting through existing correction/direction/class gates." def ImplementationChange.needsExistingGates (c : ImplementationChange) : Bool := c.goalsChanged || c.authorityChanged || c.constraintsChanged --- SKILL[thm]: "compliant alternatives alone are not deviations." +-- SKILL[thm]: "compliant alternatives are not deviations." theorem compliant_alternative_needs_no_new_gate (differentMechanics : Bool) : ImplementationChange.needsExistingGates ⟨false, false, false, differentMechanics⟩ = false := rfl @@ -203,7 +191,7 @@ theorem relabelling_preserves_requirement_authority (r : ImplementationRequireme { r with framing := label }.binding = r.binding := rfl -- SKILL[ref]: "Implementation must be delegated to a worker using the stage's default carrier under `WorkerDelegationContract`." --- SKILL[ref]: "Delegate the smallest changes for what still differs from `GoalArtifact`; open a `SshxWorkerFlightRecord` per assignment and stay orchestration-only for the repair." +-- SKILL[ref]: "Delegate the smallest changes for what still differs from `GoalArtifact`; do not add a permission, approval, transaction or execution system from an advisory/conditional concern; open a `SshxWorkerFlightRecord` per assignment and stay orchestration-only for the repair." abbrev implementationIsAFlight := @Behavior.guardOpenFlight /-- What crosses between caller and implementation worker. -/ @@ -267,7 +255,7 @@ inductive ConclusionContent | sameRoundPeerOutput deriving DecidableEq, Repr --- SKILL[def]: "- `conclusion`: compact structured result consumed by the caller. It may include verdicts, decisions, blocking goal gaps, final decision points, changed-file evidence, and test evidence when applicable. It must not include process logs, step-by-step reasoning, raw transcripts, debug output, or same-round peer output." +-- SKILL[def]: "- `conclusion`: compact structured decisions, goal gaps and applicable change/test evidence; no process logs, step-by-step reasoning, raw transcripts, debug output or same-round peer output." def ConclusionContent.permitted : ConclusionContent → Bool | .verdicts | .decisions | .blockingGoalGaps | .finalDecisionPoints | .changedFileEvidence | .testEvidence => true @@ -309,7 +297,7 @@ inductive StageMetadata | nextIterationQuestion deriving DecidableEq, Repr --- SKILL[def]: "A caller-carried stage record wraps this envelope: it references the envelope's `conclusion` and `log_ref` and may add only the stage metadata named by `InlineConsensusProtocol` and the `## Transcript Template` (such as `role`, `bias`, `visible_inputs`, `worker_mode`, `worker_carrier`, `worker_flight_ref`, `verdict`, and the `meta_judge` and `fix_or_done` `exit`, `concrete_plan`, `goal_gap`, and `next_iteration_question`)." +-- SKILL[def]: "Stage records reference envelope `conclusion`/`log_ref` and add only `InlineConsensusProtocol`/`## Transcript Template` metadata." def stageMetadataAllowed (_ : StageMetadata) : Bool := true -- SKILL[ref]: "`conclusion.verdict` is the sole verdict source for routing, the two must be equal, and any mismatch fails closed." diff --git a/skills/sshx/formal/Sshx/Clauses/Delegation.lean b/skills/sshx/formal/Sshx/Clauses/Delegation.lean index cd700663..de687c7f 100644 --- a/skills/sshx/formal/Sshx/Clauses/Delegation.lean +++ b/skills/sshx/formal/Sshx/Clauses/Delegation.lean @@ -23,6 +23,30 @@ namespace Sshx.Clauses open Sshx +/-- Existing gate evidence, not another runtime record. Hash authenticity, loaded-source +association, policy sources and revision correspondence are interpreted premises. -/ +-- SKILL[def]: "Before dispatch record effective path/SHA-256, checkout revision/dirty state if available, manifest/release distinction, adoption limits and current Heca policy/source/disable/exposure in gate evidence." +structure EffectiveSourceEvidence where + effectivePath : String + contentSha256 : String + checkoutRevision : Option String + dirty : Option Bool + manifestRelease : Option String + sessionAdoptionVerified : Bool + heca : HecaCapability + deriving DecidableEq, Repr + +-- SKILL[def]: "Unknown identity/adoption is `ASSUMED-UNVERIFIED`; disk/upstream change proves no adoption." +def EffectiveSourceEvidence.adoptionClaim (e : EffectiveSourceEvidence) : Bool := + e.effectivePath != "" && e.contentSha256 != "" && e.sessionAdoptionVerified + +example (e : EffectiveSourceEvidence) : + ({ e with sessionAdoptionVerified := false }).adoptionClaim = false := by + simp [EffectiveSourceEvidence.adoptionClaim] + +-- SKILL[policy]: "Manual inspection/refresh: README pair; no auto-update/network check/host change." +def automaticSkillRefreshAllowed : Bool := false + /-! ## Carriers and mode -/ -- SKILL[def]: "`WorkerDelegationContract` owns carrier selection/use." diff --git a/skills/sshx/formal/Sshx/Reasoning/Authority.lean b/skills/sshx/formal/Sshx/Reasoning/Authority.lean index 5851ec46..601bdd42 100644 --- a/skills/sshx/formal/Sshx/Reasoning/Authority.lean +++ b/skills/sshx/formal/Sshx/Reasoning/Authority.lean @@ -56,7 +56,7 @@ theorem boundary_checks_independent : /-! ## Blocking authority, extended -/ --- SKILL[def]: "`BlockingAuthority` is the single admissibility rule for every input that would hold a candidate out of `implement`, turn a review toward `fix`, or withhold `satisfied` — a plan objection, a review finding, or a termination difference." +-- SKILL[def]: "`BlockingAuthority` is the single admissibility rule for every input that would hold a candidate out of `implement`, turn a review toward `fix`, or withhold `satisfied`." inductive DecisionInputKind | planObjection | reviewFinding @@ -64,16 +64,16 @@ inductive DecisionInputKind deriving DecidableEq, Repr /-- Every kind of decision input passes through the same rule. -/ -def admissibility (_ : DecisionInputKind) (i : Input) : Force := force i +def admissibility (_ : DecisionInputKind) (b : DecisionBasis) : Bool := completeAdmission b -theorem one_rule_for_every_input (k k' : DecisionInputKind) (i : Input) : - admissibility k i = admissibility k' i := rfl +theorem one_rule_for_every_input (k k' : DecisionInputKind) (b : DecisionBasis) : + admissibility k b = admissibility k' b := rfl --- SKILL[policy]: "Protocol policy, not mathematics, defines these two conjuncts." +-- SKILL[policy]: "Protocol policy, not mathematics, defines these conjuncts." /-- The two conjuncts are policy constants of the contract, not derived. -/ def conjunctCount : Nat := 2 --- SKILL[thm]: "An input that names both is blocking, and stays blocking however expensive, inconvenient, or late the repair is after it passes the trigger check" +-- SKILL[thm]: "After these admission checks, both named conjuncts block regardless of repair cost, inconvenience or lateness." /-- Cost, inconvenience, lateness, and persuasiveness are not inputs of `force`. -/ theorem force_ignores_cost_and_persuasion (i : Input) (cost lateness persuasiveness : Nat) : force i = force i ∧ (cost, lateness, persuasiveness) = (cost, lateness, persuasiveness) := @@ -81,17 +81,16 @@ theorem force_ignores_cost_and_persuasion (i : Input) (cost lateness persuasiven /-- A downgrade record carries the input's own words, or that it named none. -/ inductive DowngradeRecord - | namedInOwnWords (words : String) - | namedNone + | namedInOwnWords (words : String) (triggerPassed : Bool) + | namedNone (triggerPassed : Bool) deriving DecidableEq, Repr --- SKILL[def]: "An input that names fewer than both is advisory: its downgrade record carries what it named, or that it named none, in its own words and never a paraphrase, and it is never the sole basis of a `revise`, `reject`, `abstain`, blocking finding, `unsatisfied`, or any element of a concrete plan" -def downgradeRecord (i : Input) (ownWords : String) : Option DowngradeRecord := - match force i with - | .blocking => none - | .advisory => - if i.namesGoalTerm || i.namesWorkEvidence then some (.namedInOwnWords ownWords) - else some (.namedNone) +-- SKILL[def]: "Fewer than both, or a failed trigger check, is advisory: record its original words (including what it named or none) and trigger decision, never paraphrase, in the downgrade" +def downgradeRecord (b : DecisionBasis) (ownWords : String) : Option DowngradeRecord := + if completeAdmission b then none + else if b.input.namesGoalTerm || b.input.namesWorkEvidence then + some (.namedInOwnWords ownWords (triggerCheck b.trigger)) + else some (.namedNone (triggerCheck b.trigger)) /-- The decisions an advisory input may never be the sole basis of. -/ inductive SoleBasisDecision @@ -103,10 +102,11 @@ inductive SoleBasisDecision | concretePlanElement deriving DecidableEq, Repr -def mayBeSoleBasis (i : Input) (_ : SoleBasisDecision) : Bool := force i == .blocking +def mayBeSoleBasis (b : DecisionBasis) (_ : SoleBasisDecision) : Bool := completeAdmission b -theorem advisory_never_sole_basis (i : Input) (h : force i = .advisory) (d : SoleBasisDecision) : - mayBeSoleBasis i d = false := by +theorem advisory_never_sole_basis (b : DecisionBasis) + (h : completeAdmission b = false) (d : SoleBasisDecision) : + mayBeSoleBasis b d = false := by simp [mayBeSoleBasis, h] /-- A plan element and what admits it. -/ @@ -117,24 +117,25 @@ structure PlanElement where onlyTestIntroducedWithIt : Bool deriving DecidableEq, Repr --- SKILL[def]: "The same two conjuncts admit a plan element: a defense, validation, abstraction, or compatibility path enters a plan only when it names the `GoalArtifact` term that demands it or a current consumer (an existing call site), and a test introduced together with it may corroborate that basis but never creates it." --- SKILL[def]: "Findings and plan elements share this contextual chain: default to non-malicious ordinary use and mistakes, tracing actor, actual input path and goal-visible residue after declared recovery." --- SKILL[def]: "Safety labels supply no evidence; ineligible or absorbed threats authorize no defense, validation or further repair." +-- SKILL[def]: "The same two conjuncts and evidence-status/goal-basis checks admit a plan element: name the demanding `GoalArtifact` term or current consumer (existing call site); a co-introduced test corroborates but cannot create that basis." +-- SKILL[def]: "Findings/plans trace non-malicious ordinary use/mistakes, actor, actual input path and goal-visible residue after declared recovery." +-- SKILL[def]: "Safety labels prove nothing; ineligible/absorbed threats authorize no defense, validation or repair." def planElementAdmitted (e : PlanElement) : Bool := let input := { e.basis.input with namesGoalTerm := e.basis.input.namesGoalTerm || e.namesCurrentConsumer } - downgrade { e.basis with verdict := .reject, input } == .reject + downgrade { e.basis with verdict := .reject, input } == .reject && !e.basis.requiresOwnerDecision theorem test_never_creates_admission (e : PlanElement) (h : e.basis.input.namesGoalTerm = false) (h' : e.namesCurrentConsumer = false) : planElementAdmitted e = false := by - simp [planElementAdmitted, downgrade, force, h, h'] + simp [planElementAdmitted, downgrade, completeAdmission, force, h, h'] --- SKILL[thm]: "Failure is objective, not semantic: the rule asks only whether both conjuncts are named, never how well they are evidenced, while the trigger check is mechanical" +-- SKILL[thm]: "After evidence-status/goal-basis admission, force asks whether both conjuncts are named, not how persuasive they are; workflow grounding and owner-policy compliance remain trigger-check premises." /-- An actual defect names both conjuncts, so the rule never removes it. -/ theorem actual_defect_stays_blocking (i : Input) (hterm : i.namesGoalTerm = true) - (hev : i.namesWorkEvidence = true) (hfalse : i.basisShownFalse = false) : + (hev : i.namesWorkEvidence = true) (hfalse : i.basisShownFalse = false) + (hstatus : i.evidenceStatus = .confirmed) (hbasis : i.userGoalBasis ≠ "") : force i = .blocking := - (force_blocking_iff i).mpr ⟨hterm, hev, hfalse⟩ + (force_blocking_iff i).mpr ⟨hterm, hev, hfalse, hstatus, hbasis⟩ /-! ## Advisory shapes and escaping residues -/ @@ -252,7 +253,7 @@ theorem no_constructor_no_escape : /-! ## Six independent questions -/ -- SKILL[def]: "`BlockingAuthority` asks only whether a decision input may block;" -def asksMayBlock (i : Input) : Force := force i +def asksMayBlock (b : DecisionBasis) : Bool := completeAdmission b -- SKILL[def]: "`ThreatEligibility` asks who the actor is;" def asksWhoTheActorIs (t : TrustedPartyConduct) : Bool := threatEligible t @@ -281,6 +282,6 @@ theorem three_checks_independent : ∃ i : Input, force i = .blocking ∧ ∃ c : CandidateSolution, capabilityOverlap c = false ∧ ∃ t : TrustedPartyConduct, threatEligible t = false := - ⟨⟨true, true, false, false⟩, rfl, ⟨false, false⟩, rfl, .deliberateMalice, rfl⟩ + ⟨⟨true, true, false, false, .confirmed, "current goal/contract source"⟩, rfl, ⟨false, false⟩, rfl, .deliberateMalice, rfl⟩ end Sshx.Reasoning diff --git a/skills/sshx/formal/Sshx/Reasoning/Convergence.lean b/skills/sshx/formal/Sshx/Reasoning/Convergence.lean index 28050722..23a772fc 100644 --- a/skills/sshx/formal/Sshx/Reasoning/Convergence.lean +++ b/skills/sshx/formal/Sshx/Reasoning/Convergence.lean @@ -72,7 +72,7 @@ def elegancePremiumChallenged (beautifulCost cheapestCost : Nat) : Bool := theorem no_premium_no_clash (c : Nat) : elegancePremiumChallenged c c = false := by simp [elegancePremiumChallenged] --- SKILL[thm]: "An `implement` exit also requires no unresolved harness overlap or authority gap." +-- SKILL[thm]: "An `implement` exit requires no unresolved harness overlap/authority gap" theorem harness_gap_blocks_implement (d : DesignInputs) (h : d.harnessOverlapOrAuthorityGap = true) : designRoute d ≠ .implement := no_implement_with_harness_gap d h @@ -84,7 +84,7 @@ structure GoalHarnessFit where usesOwnJudgmentResponsibilities : Bool deriving DecidableEq, Repr --- SKILL[def]: "A goal and its harness mismatch when it presupposes missing host/controller execution capability or asks the skill to repeat a capability already declared by the harness; the skill's own judgment responsibilities are not a mismatch." +-- SKILL[def]: "missing host/controller execution or repeating a provided capability is a mismatch; skill judgment duties are not." def harnessMismatch (g : GoalHarnessFit) : Bool := g.presupposesMissingHostCapability || g.repeatsDeclaredCapability @@ -93,7 +93,7 @@ theorem judgment_is_not_mismatch (g : GoalHarnessFit) harnessMismatch g = false := by simp [harnessMismatch, h1, h2] --- SKILL[def]: "Route a mismatch as a goal gap to the maintainer rather than implementing it." +-- SKILL[def]: "Route mismatches as goal gaps to the maintainer." inductive MismatchRoute | goalGapToMaintainer deriving DecidableEq, Repr @@ -139,6 +139,7 @@ structure Objection where causalPredictionFalsifiable : Bool convergenceAnsweredChain : Bool input : Input + trigger : TriggerRecord ownWords : String deriving DecidableEq, Repr @@ -148,22 +149,31 @@ def threeConditions (o : Objection) : Bool := -- SKILL[def]: "When a seat's `SshxResultEnvelope.conclusion` records both a dedicated-domain objection and its falsifiable causal prediction, and the meta-judge's proposed convergence has not refuted that causal chain, the meta-judge must run a `FocusedRound` before converging, provided the objection passes `BlockingAuthority`." def focusedRoundRequired (o : Objection) : Bool := - threeConditions o && (force o.input == .blocking) + threeConditions o && completeAdmission ⟨o.input, o.trigger⟩ --- SKILL[thm]: "An advisory objection does not trigger a `FocusedRound`; for this prerequisite, the meta-judge checks only whether the seat named both conjuncts and must not assess their persuasiveness." +-- SKILL[thm]: "An advisory objection does not trigger a `FocusedRound`; after admission checks, the meta-judge checks only whether both conjuncts are named, never their persuasiveness." theorem advisory_never_triggers (o : Objection) (h : force o.input = .advisory) : focusedRoundRequired o = false := by - simp [focusedRoundRequired, h] + have ha : completeAdmission ⟨o.input, o.trigger⟩ = false := by + simp [completeAdmission, h] + simp [focusedRoundRequired, ha] --- SKILL[thm]: "An objection that named a basis whose correctness is disputed still triggers the round because disputed is not absent." +theorem failed_trigger_never_triggers (o : Objection) + (h : triggerCheck o.trigger = false) : focusedRoundRequired o = false := by + have ha : completeAdmission ⟨o.input, o.trigger⟩ = false := by + simp [completeAdmission, h] + simp [focusedRoundRequired, ha] + +-- SKILL[thm]: "An admitted confirmed basis disputed on correctness still triggers: disputed is not absent." theorem disputed_still_triggers (o : Objection) (b : Bool) : focusedRoundRequired { o with input := { o.input with basisDisputed := b } } = focusedRoundRequired o := by - simp [focusedRoundRequired, threeConditions, force] + simp only [focusedRoundRequired, threeConditions, completeAdmission] + rw [force_ignores_dispute] -- SKILL[def]: "When the meta-judge declines a round on this ground, it records that decline in the existing `finding_downgrades` record under the same own-words requirement that governs downgrades." def declineRecord (o : Objection) : Option DowngradeRecord := - if focusedRoundRequired o then none else downgradeRecord o.input o.ownWords + if focusedRoundRequired o then none else downgradeRecord ⟨o.input, o.trigger⟩ o.ownWords -- SKILL[def]: "In the focused round, all seats independently answer one question: "Does this causal chain hold, and if it does, how should the plan change?" The round preserves `## No Context Pollution`." def focusedRoundQuestion : String := @@ -236,7 +246,7 @@ theorem only_unresolved_conflict_blocks (d : DesignInputs) (conflicts : List Gro -- SKILL[ref]: "An objection that fails `BlockingAuthority` is not an unclosed `GoalArtifact` goal gap and does not by itself hold the exit out of `implement`: the meta-judge records it as advisory in the existing `finding_downgrades` record as `BlockingAuthority` requires." abbrev advisoryObjectionRecord := @downgradeRecord --- SKILL[ref]: "Disputed grounding stays blocking." +-- SKILL[ref]: "Admitted confirmed disputed grounding stays blocking." abbrev disputedStaysBlocking := @force_ignores_dispute -- SKILL[ref]: "This is not permission to set aside a reachable defect." @@ -249,9 +259,9 @@ def convergenceQuestion : String := "what still differs from GoalArtifact?" -- SKILL[def]: "Do not generalize the convergence pass beyond that goal gap." /-- The convergence pass ranges over the goal gap only. -/ -def convergencePassScope (bases : List Input) : List Input := goalGapOf bases +def convergencePassScope (bases : List DecisionBasis) : List DecisionBasis := goalGapOf bases -theorem convergence_scope_is_the_goal_gap (bases : List Input) : +theorem convergence_scope_is_the_goal_gap (bases : List DecisionBasis) : convergencePassScope bases = goalGapOf bases := rfl /-- Whether an owner-sourced, versioned, scoped orientation is recorded. -/ diff --git a/skills/sshx/formal/Sshx/Reasoning/Discipline.lean b/skills/sshx/formal/Sshx/Reasoning/Discipline.lean index dd1c54d6..0afd1567 100644 --- a/skills/sshx/formal/Sshx/Reasoning/Discipline.lean +++ b/skills/sshx/formal/Sshx/Reasoning/Discipline.lean @@ -52,7 +52,7 @@ inductive Alignment | revision deriving DecidableEq, Repr --- SKILL[def]: "Reference-frame: each thinking, review, or termination perspective identifies the applicable mature theory, engineering principle, industry best practice, mature industry case, mature pattern, or constraint framework governing this class of problem or implementation; surfaces the known-good shape; then re-checks each candidate conclusion, implementation interpretation, repair candidate, or termination judgment against it before settling the verdict." +-- SKILL[def]: "Reference-frame: each thinking, review or termination seat identifies the applicable mature theory/principle, industry practice/case/pattern or constraint framework and known-good shape; re-check every candidate, implementation interpretation, repair or termination judgment against it." structure ReferenceFrame where kind : FrameKind name : String @@ -60,7 +60,7 @@ structure ReferenceFrame where alignment : Alignment deriving DecidableEq, Repr --- SKILL[def]: "`no applicable mature theory found` is an acceptable explicit fallback; in that case the note says so and still records the root-cause and minimal-path re-check against `GoalArtifact`." +-- SKILL[def]: "If `no applicable mature theory found`, say so and still record root-cause/minimal-path re-check against `GoalArtifact`." /-- Either a frame or the explicit fallback, which still carries the two re-checks. -/ inductive FrameRecord | frame (f : ReferenceFrame) @@ -518,7 +518,7 @@ theorem valid_note_has_no_silent_reliance (n : DisciplineNote) (weighed : List C (h : n.valid weighed) (m : MarkedPremise) (hm : m ∈ n.premises) : ¬ silentReliance m := h.2.2 m hm --- SKILL[prose]: "This does not override `GoalArtifact`, assigned bias or review focus, truth tables, or allowed verdict sets." +-- SKILL[prose]: "This never overrides `GoalArtifact`, bias/focus, truth tables or verdict sets." -- why: a precedence statement; the note is a component of a conclusion and the verdict alphabets and tables are separate definitions it cannot alter. end Sshx.Reasoning diff --git a/skills/sshx/formal/Sshx/Reasoning/Guards.lean b/skills/sshx/formal/Sshx/Reasoning/Guards.lean index fb8ded65..c49741a5 100644 --- a/skills/sshx/formal/Sshx/Reasoning/Guards.lean +++ b/skills/sshx/formal/Sshx/Reasoning/Guards.lean @@ -59,11 +59,8 @@ def unverifiedSourceCanRoute (sourceVerified : Bool) : Bool := sourceVerified def searchResultsCreateGrounding (sourceVerified : Bool) : Bool := false -- SKILL[def]: "When `conclusion.blocking_findings` is present" -structure BlockingFindingMetadata where - trigger : String - triggerActor : String - mechanismFamily : String - deriving DecidableEq, Repr +-- SKILL[ref]: "Describe before judging." +abbrev BlockingFindingMetadata := TriggerRecord -- SKILL[def]: "Trusted-party failure, omission, and uncertainty remain eligible" def ordinaryOperationKeepsTrustedFailureEligible (ordinaryPath : Bool) (trustedFailure : Bool) : Bool := @@ -100,7 +97,10 @@ def missingPlanningEvidenceBlocksImplement (evidenceVerified : Bool) : Bool := ! -- SKILL[def]: "It must carry the fields required by `## Result Envelope`." def findingMetadataShapeComplete (metadata : TriggerRecord) : Bool := - metadata.trigger != "" && metadata.triggerActor != "" && metadata.mechanismFamily != "" + metadata.trigger != "" && metadata.triggerActor != "" && metadata.mechanismFamily != "" && + metadata.familyBasis.failedProperty != "" && metadata.familyBasis.causalMechanism != "" && + metadata.familyBasis.correspondenceEvidence != "" + -- Typed input evidence and owner policy are mandatory in TriggerRecord. -- SKILL[def]: "On every review pass after the initial implementation, the review triplet must list each defense" def reviewListsNewDefenses (listed : Bool) : Bool := listed diff --git a/skills/sshx/formal/Sshx/Reasoning/Panel.lean b/skills/sshx/formal/Sshx/Reasoning/Panel.lean index e6f6292b..e5e894e9 100644 --- a/skills/sshx/formal/Sshx/Reasoning/Panel.lean +++ b/skills/sshx/formal/Sshx/Reasoning/Panel.lean @@ -31,7 +31,7 @@ structure Charter where attacks : List String deriving DecidableEq, Repr --- SKILL[policy]: "Protocol policy, not a mathematical consequence: run six whole-picture philosopher seats before choosing a plan — the same universal judgment lenses the consensus engine debates with." +-- SKILL[policy]: "Protocol policy, not a mathematical consequence: run six whole-picture philosopher seats before choosing a plan, with distinct objectives and independent, isolated context." def seatCount : Nat := 6 -- SKILL[def]: "- `teleology`: purpose and inevitability. What is this for, and is the form forced by that purpose? Attacks skipped-purpose and missing-inevitability." @@ -99,7 +99,7 @@ def WorthJudgment.wellFormed (w : WorthJudgment) : Prop := def worthVerdict (w : WorthJudgment) : Bool := w.incrementalBenefitClearsCost --- SKILL[def]: "Each seat is one independent, context-isolated perspective that attacks from its own objective; the seats can and do disagree, and the meta-judge converges them:" +-- SKILL[def]: "They may disagree; meta-judge converges their judgments:" def panel : List Charter := [teleology, parsimony, fidelity, naturalOwnership, proportionalContainment, worth] @@ -120,11 +120,11 @@ structure DyadExchange where highestLayerImaginable : Nat deriving DecidableEq, Repr --- SKILL[def]: "`natural-ownership` and `proportional-containment` are a coupled **must-clash locus dyad**: they run together, each must answer the other pole's claim, and they converge on the natural owner layer — not the highest layer imaginable." +-- SKILL[def]: "`natural-ownership` and `proportional-containment` are a coupled **must-clash locus dyad**: run together, each answers the other pole, converging on the natural owner layer, not the highest imaginable." def DyadExchange.mustClash (d : DyadExchange) : Prop := d.ownershipAnsweredContainment = true ∧ d.containmentAnsweredOwnership = true --- SKILL[def]: "Ownership pulls the fix toward the layer that owns the invariant; containment resists over-reaching past it." +-- SKILL[def]: "Ownership pulls toward the invariant owner; containment resists overreach" /-- The converged layer is the owner layer capped by containment, never the highest. -/ def dyadConverge (d : DyadExchange) : Nat := min d.ownershipClaimsLayer d.containmentAllowsUpTo @@ -138,12 +138,12 @@ theorem dyad_converges_to_owner_not_highest (d : DyadExchange) unfold dyadConverge omega --- SKILL[prose]: "This is the "go upstream to the root, but not past the natural owner" balance expressed as two adversarial seats the meta-judge converges, rather than a single balanced checklist." +-- SKILL[prose]: ""go upstream to the root, but not past the natural owner" is two adversarial seats for meta-judge convergence, not one balanced checklist." -- why: names the design intent of the dyad; the balance itself is `dyadConverge` and the two charters above. /-! ## Worth is its own seat -/ --- SKILL[thm]: "`worth` (值不值) is an independent objective, not the aesthetic lens repeated: `parsimony` asks how much mechanism, `proportional-containment` asks where and how far it binds, and `worth` asks whether to pay for this at all, at this cost, now, versus the best alternative." +-- SKILL[thm]: "`worth` (值不值) is independent of aesthetics: `parsimony` asks how much mechanism, `proportional-containment` where/how far, `worth` whether to pay this cost now versus the best alternative." /-- The three questions read different inputs: a mechanism count, a binding, and a benefit–cost pair; none is a function of another. -/ theorem worth_is_not_parsimony_or_containment : @@ -152,7 +152,7 @@ theorem worth_is_not_parsimony_or_containment : asksWhetherToPay benefit cost = false := ⟨1, ⟨1, 1, 1⟩, 0, 1, rfl, rfl, by decide⟩ --- SKILL[thm]: "A candidate can be minimal, beautiful, and properly contained yet still not worth doing, and a less minimal candidate can still be worth doing when the avoided downside justifies it." +-- SKILL[thm]: "Minimal, beautiful, contained work may be unworthy; less minimal work may justify its cost." theorem minimal_beautiful_contained_yet_not_worth : ∃ f : Form, ∃ w : WorthJudgment, f.beautiful = true ∧ f.size = 1 ∧ worthVerdict w = false := ⟨⟨1, true, false, true, true, true, true⟩, ⟨.doNothing, "no benefit", false, false, false⟩, @@ -163,7 +163,7 @@ theorem less_minimal_yet_worth : ⟨⟨2, true, false, true, true, true, true⟩, ⟨.cheapestSufficientAlternative, "avoided downside", true, false, false⟩, rfl, rfl⟩ --- SKILL[thm]: "Because it is a seat rather than a cross-cutting lens, `worth` is judged once by its own perspective, so the panel is not homogenized into every seat re-deriving the same value verdict." +-- SKILL[thm]: "Only its own seat derives this verdict, preserving distinct objectives." theorem worth_judged_once : (panel.filter fun c => c.lens == .worth).length = 1 := by decide /-! ## What every seat does before returning -/ @@ -184,7 +184,7 @@ structure SeatConclusion where rootCause : String answer : RootCauseAnswer capabilityOverlapHit : Bool - bases : List Input + bases : List DecisionBasis planElements : List PlanElement reviseGoalGap : Option String reviseNextIterationQuestion : Option String @@ -203,15 +203,16 @@ theorem overlap_never_implements (c : SeatConclusion) (h : c.capabilityOverlapHi -- SKILL[def]: "Each seat applies `BlockingAuthority` to every proposed plan element and every `propose`, `revise`, `reject`, or `abstain` basis, and states the `GoalArtifact` term and evidence that make each basis blocking, or the `GoalArtifact` term or current consumer that admits each plan element." def SeatConclusion.basesStated (c : SeatConclusion) : Prop := - (∀ i ∈ c.bases, force i = .blocking ∨ force i = .advisory) ∧ + (∀ b ∈ c.bases, completeAdmission b = true ∨ completeAdmission b = false) ∧ (∀ e ∈ c.planElements, planElementAdmitted e = true) -- SKILL[thm]: "An advisory basis is not a goal gap, must not by itself hold a candidate out of `implement`, and machinery that only defends against one must not enter a proposed plan." /-- A goal gap is a blocking basis; an advisory basis is never one. -/ -def goalGapOf (bases : List Input) : List Input := bases.filter fun i => force i == .blocking +def goalGapOf (bases : List DecisionBasis) : List DecisionBasis := + bases.filter fun b => completeAdmission b -theorem advisory_is_not_a_goal_gap (bases : List Input) (i : Input) (h : force i = .advisory) : - i ∉ goalGapOf bases := by +theorem advisory_is_not_a_goal_gap (bases : List DecisionBasis) (b : DecisionBasis) + (h : completeAdmission b = false) : b ∉ goalGapOf bases := by simp [goalGapOf, h] -- SKILL[def]: "Every seat must first identify the problem essence or root cause implied by `GoalArtifact`, then frame `propose`, `revise`, `reject`, or `abstain` as an answer to it: what satisfies it, what still differs from it, or why it cannot be satisfied." diff --git a/skills/sshx/formal/Sshx/Reasoning/Repair.lean b/skills/sshx/formal/Sshx/Reasoning/Repair.lean index 7a93065e..7efaa8f9 100644 --- a/skills/sshx/formal/Sshx/Reasoning/Repair.lean +++ b/skills/sshx/formal/Sshx/Reasoning/Repair.lean @@ -63,7 +63,36 @@ inductive FamilyRoute | ownerDecision deriving DecidableEq, Repr --- SKILL[def]: "A uniform invariant, a verified complete finite treatment, or an already-authorized enforced boundary may establish class coverage; otherwise the class gate routes bounded revise or investigation, and unresolved coverage is reported honestly." +/-- A reason new is evidence in its own right, not an unresolved prior comparison. +This projects existing conclusion evidence and introduces no runtime record or gate. -/ +-- SKILL[ref]: "`family_basis` (property, cause, evidenced prior match or reason new)" +inductive FamilyHistory + | newFamily (reason : String) + | priorComparison (priorLabel : String) (sameProperty sameCause settledPrior : Bool) + deriving DecidableEq, Repr + +/-- Evidence interpreting a new family or settled prior summaries. Label and location +equality have no authority; evidence truth and the peer boundary remain premises. -/ +structure FamilyCorrespondence where + currentLabel : String + evidence : String + peerFree : Bool + history : FamilyHistory + deriving DecidableEq, Repr + +-- SKILL[def]: "After collection meta-judge records labels, property/cause, evidenced prior match/distinct cause; same location/predicate is insufficient and paraphrase creates no new family." +-- SKILL[ref]: "Later briefs/`visible_inputs` carry settled prior summaries/coverage limits, never same-round output; findings address correspondence." +def FamilyCorrespondence.verified (c : FamilyCorrespondence) : Bool := + c.currentLabel != "" && c.evidence != "" && c.peerFree && + match c.history with + | .newFamily reason => reason != "" + | .priorComparison priorLabel _ _ settledPrior => priorLabel != "" && settledPrior + +def FamilyCorrespondence.sameFamily (c : FamilyCorrespondence) : Bool := + c.verified && + match c.history with + | .newFamily _ => false + | .priorComparison _ sameProperty sameCause _ => sameProperty && sameCause -- SKILL[def]: "Record the goal/property, authorized domain, family, coverage basis, action/owner and falsifiable validation in the existing conclusion." structure FamilyEvidence where @@ -74,7 +103,7 @@ structure FamilyEvidence where actionOwner : String falsifiableValidation : String sameGoalTerm : Bool - sameMechanismFamily : Bool + correspondence : FamilyCorrespondence consecutivePasses : Nat earlierUnsupportedEnumeration : Bool coverageBasis : ClassCoverageBasis @@ -83,40 +112,48 @@ structure FamilyEvidence where changesDomainOrCriterion : Bool ownerAuthorized : Bool revision : Option Revision + inputCorrespondenceVerified : Bool + measurementLimitsReported : Bool deriving DecidableEq, Repr -- SKILL[ref]: "Domain or criterion changes require the existing owner authorization and append-only revision." def ownerAuthorizedDomainChange (e : FamilyEvidence) : Bool := !e.changesDomainOrCriterion || (e.ownerAuthorized && e.revision.isSome) +-- SKILL[def]: "State-space coverage reports actual workflow-domain measurements (command/scope/counts), limits/unavailability and future-input derivations." +-- SKILL[ref]: "Census alone proves no coverage/restriction; apply sourced owner policy, changing it only with owner authorization/revision." def FamilyEvidence.recordComplete (e : FamilyEvidence) : Bool := e.goalTerm != "" && e.property != "" && e.authorizedInputDomain != "" && - e.mechanismFamily != "" && e.actionOwner != "" && e.falsifiableValidation != "" + e.mechanismFamily != "" && e.actionOwner != "" && e.falsifiableValidation != "" && + e.inputCorrespondenceVerified && e.measurementLimitsReported --- SKILL[def]: "Before dispatching a repair after two consecutive passes whose blocking findings name the same `GoalArtifact` term and `mechanism_family`, or after earlier recorded evidence shows that member-by-member enumeration leaves the property unsupported, the existing gate makes one class-level decision." +-- SKILL[def]: "Before dispatching a repair after two consecutive passes whose blocking findings name the same `GoalArtifact` term and evidenced family (the same failed property and causal mechanism, even with different `mechanism_family` wording), or after earlier recorded evidence shows that member-by-member enumeration leaves the property unsupported, the existing gate makes one class-level decision." def classGateActive (e : FamilyEvidence) : Bool := - (e.sameGoalTerm && e.sameMechanismFamily && decide (2 ≤ e.consecutivePasses)) || + (e.sameGoalTerm && e.correspondence.sameFamily && decide (2 ≤ e.consecutivePasses)) || e.earlierUnsupportedEnumeration -- SKILL[def]: "Repair dispatch requires the recorded family and a verified coverage basis under `## Reasoning Discipline`." -- The formal basis additionally admits a verified sound abstraction over an open or infinite -- domain when its admissible-input correspondence and falsifier are recorded. -- SKILL[def]: "A sound abstraction may cover an infinite domain with recorded admissible-input correspondence and a falsifiable invariant." +-- SKILL[def]: "A uniform invariant, a verified complete finite treatment, or an already-authorized enforced boundary may establish class coverage; otherwise the class gate routes bounded revise or investigation, and unresolved coverage is reported honestly." def coverageBasisVerified : ClassCoverageBasis → Bool | .uniformInvariant verified | .soundAbstraction verified | .completeFiniteTreatment verified => verified | .authorizedBoundary enforced authorized => enforced && authorized | .unsupportedMemberEnumeration | .unknown => false -- SKILL[def]: "Unknown family or coverage routes bounded investigation under the intake scope; no supported path means honest unresolved stop, with only actual product, governance, boundary or permission decisions routed to their owner." +-- SKILL[ref]: "Unresolved correspondence routes bounded class investigation before member repair." def familyRoute (e : FamilyEvidence) : FamilyRoute := if e.ownerDecisionRequired || (e.changesDomainOrCriterion && !e.ownerAuthorized) then .ownerDecision else if !ownerAuthorizedDomainChange e then .reviseOrInvestigate + else if !e.correspondence.verified then .reviseOrInvestigate else if !classGateActive e then .continue else if e.noSupportedPath then .honestStop else if e.recordComplete && coverageBasisVerified e.coverageBasis then .continue else .reviseOrInvestigate --- SKILL[def]: "A new fixture, recurrence, zero usage, or exhausted budget cannot authorize a member patch or narrow the domain." +-- SKILL[def]: "A new fixture, recurrence, zero usage, or exhausted budget alone cannot authorize a member patch or narrow the domain." /-- The actual caller pass guard consumes this route. Unsupported class coverage permits only a bounded investigation/convergence or review, never another member repair. -/ def familyPassAllowed (e : FamilyEvidence) (t : Transition) : Bool := @@ -133,7 +170,8 @@ theorem unsupported_class_never_dispatches (e : FamilyEvidence) simp only [familyPassAllowed, familyRoute, ha, h, coverageBasisVerified] unfold ownerAuthorizedDomainChange cases e.ownerDecisionRequired <;> cases e.changesDomainOrCriterion <;> - cases e.ownerAuthorized <;> cases e.noSupportedPath <;> cases e.revision <;> simp_all + cases e.ownerAuthorized <;> cases e.noSupportedPath <;> cases e.revision <;> + cases e.correspondence.verified <;> simp_all /-- Where a blocking gap sits in `GoalArtifact`; lower ranks are repaired first. -/ inductive GapRank diff --git a/skills/sshx/formal/Sshx/Reasoning/Review.lean b/skills/sshx/formal/Sshx/Reasoning/Review.lean index bf5c5db2..fd968a3e 100644 --- a/skills/sshx/formal/Sshx/Reasoning/Review.lean +++ b/skills/sshx/formal/Sshx/Reasoning/Review.lean @@ -102,39 +102,48 @@ theorem reject_blocks_done (a b c : ReviewVerdict) (h : a = .reject ∨ b = .rej reviewRoute a b c = .fix := by simp [reviewRoute, h] --- SKILL[def]: "Harness gaps and claim authority follow `## Goal Contract` without startup confirmation." +-- SKILL[def]: "Harness gaps and claim authority follow `## Goal Contract`, including its material owner-clarification rule." abbrev routineHarnessGapRecord := @Behavior.IntakeEvidence.complete /-- The only conversion of a reject into an advisory is the downgrade. -/ theorem conversion_is_downgrade (f : Finding) (h : f.verdict = .reject) - (hc : downgrade f = .comment) : eligible f = false ∨ force f.input = .advisory := by - by_contra hcontra - push_neg at hcontra - have hb : force f.input = .blocking := by - cases hf : force f.input - · rfl - · exact absurd hf hcontra.2 - have : downgrade f = .reject := - (downgrade_reject_iff f).mpr ⟨h, by simpa using hcontra.1, hb⟩ - simp [this] at hc + (hc : downgrade f = .comment) : eligible f = false ∨ + completeAdmission ⟨f.input, f.trigger⟩ = false := by + by_cases he : eligible f = false + · exact Or.inl he + by_cases ha : completeAdmission ⟨f.input, f.trigger⟩ = false + · exact Or.inr ha + exfalso + have he' : eligible f = true := by + cases h' : eligible f <;> simp_all + have ha' : completeAdmission ⟨f.input, f.trigger⟩ = true := by + cases h' : completeAdmission ⟨f.input, f.trigger⟩ <;> simp_all + have hb : force f.input = .blocking := + completeAdmission_requires_force ⟨f.input, f.trigger⟩ ha' + have hd : downgrade f = .reject := + (downgrade_reject_iff f).mpr ⟨h, he', hb⟩ + exact (by simpa [hd] using hc) /-- A blocking finding as the contract requires it to be stated. -/ structure BlockingFinding where input : Input + trigger : TriggerRecord goalTerm : String conduct : TrustedPartyConduct deriving DecidableEq, Repr -- SKILL[def]: "Every blocking finding must name both `BlockingAuthority` conjuncts under `## Reasoning Discipline` and its failure, omission or uncertainty class within the trust boundary." def BlockingFinding.wellFormed (b : BlockingFinding) : Prop := - force b.input = .blocking ∧ b.goalTerm ≠ "" ∧ threatEligible b.conduct = true + completeAdmission ⟨b.input, b.trigger⟩ = true ∧ b.goalTerm ≠ "" ∧ + threatEligible b.conduct = true -- SKILL[ref]: "Downgrade records and disputed grounding follow `BlockingAuthority`." abbrev objectiveDowngrade := @downgradeRecord -- SKILL[thm]: "Downgrade is allowed only for threat-model ineligibility or an advisory input, never because a finding is inconvenient, expensive, or late, and never sets aside a reachable defect." theorem downgrade_only_for_ineligible_or_advisory (f : Finding) (h : f.verdict = .reject) - (hc : downgrade f = .comment) : eligible f = false ∨ force f.input = .advisory := + (hc : downgrade f = .comment) : eligible f = false ∨ + completeAdmission ⟨f.input, f.trigger⟩ = false := conversion_is_downgrade f h hc end Sshx.Reasoning diff --git a/skills/sshx/formal/Sshx/Reasoning/Termination.lean b/skills/sshx/formal/Sshx/Reasoning/Termination.lean index 9c4deea2..ed23c0ff 100644 --- a/skills/sshx/formal/Sshx/Reasoning/Termination.lean +++ b/skills/sshx/formal/Sshx/Reasoning/Termination.lean @@ -67,16 +67,24 @@ structure RemainingDifference where difference : String responsibleParty : String input : Input + trigger : TriggerRecord broadensIntoImprovementSearch : Bool deriving DecidableEq, Repr -- SKILL[def]: "- `residual-gap`: adversarially falsify termination by answering the existing `iteration_question` with one concrete remaining difference from `GoalArtifact`, and name the responsible party for it. It must not broaden into a generic improvement search. The named difference must pass `BlockingAuthority`; an advisory worry is not a remaining difference." def RemainingDifference.counts (d : RemainingDifference) : Bool := - (force d.input == .blocking) && !d.broadensIntoImprovementSearch && (d.responsibleParty != "") + completeAdmission ⟨d.input, d.trigger⟩ && !d.broadensIntoImprovementSearch && + (d.responsibleParty != "") theorem advisory_worry_is_not_a_difference (d : RemainingDifference) (h : force d.input = .advisory) : d.counts = false := by - simp [RemainingDifference.counts, h] + have ha : completeAdmission ⟨d.input, d.trigger⟩ = false := by + simp [completeAdmission, h] + simp [RemainingDifference.counts, ha] + +theorem failed_trigger_is_not_a_difference (d : RemainingDifference) + (h : triggerCheck d.trigger = false) : d.counts = false := by + simp [RemainingDifference.counts, completeAdmission, h] /-- What `claim-integrity` refuses as evidence that an obligation is discharged. -/ inductive ProxyEvidence @@ -123,9 +131,11 @@ abbrev rosterIdentities := @Roster abbrev noPermissionFromNonSatisfied := @no_permission_from_nonsatisfied -- SKILL[ref]: "Each termination seat applies `BlockingAuthority` itself before returning." -abbrev seatAppliesAuthority := @settleSeat +def seatAppliesAuthority (v : TerminationSeat) (b : DecisionBasis) + (redispatchedAlready : Bool) : TerminationSeat := + settleSeat v (completeAdmission b) redispatchedAlready --- SKILL[ref]: "An `unsatisfied` that names both conjuncts keeps its full force and may never be converted into permission by calling it unpersuasive." +-- SKILL[ref]: "An admitted confirmed `unsatisfied` that names both conjuncts keeps its full force and may never be converted into permission by calling it unpersuasive." abbrev groundedUnsatisfiedKept := @grounded_unsatisfied_kept /-! ## Routing a withheld claim by ownership -/ diff --git a/skills/sshx/formal/Sshx/Records.lean b/skills/sshx/formal/Sshx/Records.lean index 7f94fcba..cda6a751 100644 --- a/skills/sshx/formal/Sshx/Records.lean +++ b/skills/sshx/formal/Sshx/Records.lean @@ -7,6 +7,17 @@ and the stage record mirror rule. namespace Sshx +/-- Sourced activation authority interpreted at intake, not a risk classifier. -/ +-- SKILL[def]: "Activate only for explicit user consensus, multi-angle thinking or delegated review, or a sourced applicable host/repository mandate." +inductive ActivationAuthority + | absent + | explicitRequest + | hostMandate + deriving DecidableEq, Repr + +-- SKILL[def]: "Record that authority at intake." +def ActivationAuthority.authorized (a : ActivationAuthority) : Bool := a != .absent + -- SKILL[def]: "`harness` is a prompt-level record containing exactly these three sub-items:" -- SKILL[def]: "- `provided_capabilities`: capabilities already supplied by the execution environment that the skill must not implement again;" -- SKILL[def]: "- `trust_boundary`: which roles are trusted and which are untrusted. The trusted declaration is **non-adversarial, not infallible**: failures, omissions, and uncertainty by a trusted party remain fully in review scope;" diff --git a/skills/sshx/scripts/run-codex-worker.sh b/skills/sshx/scripts/run-codex-worker.sh index d7153687..e686e2ec 100644 --- a/skills/sshx/scripts/run-codex-worker.sh +++ b/skills/sshx/scripts/run-codex-worker.sh @@ -317,8 +317,12 @@ The envelope must be strict JSON whose top-level value is an object containing e For the "thinking", "review", and "termination" stages, "conclusion.verdict" must be a JSON string and one of the values on the allowed verdict line above. The "implementation" stage does not require a verdict. Minimum structurally accepted envelope shape: $skeleton_json This example is only the minimum structurally accepted shape; the worker must populate "conclusion" with the complete structured result required by its task brief and must not submit this skeletal example unchanged. -The example uses this attempt's worker stdout log for "log_ref"; the worker may replace it with another non-empty reference. -Publish result.json.tmp then atomically rename it to result.json, then do the same for completion.sentinel. +Worker-owned: only result.json, completion.sentinel and their same-directory temporary publication files. +Runner-owned: brief.md, worker.stdout.log, worker.stderr.log, last-message.txt, status.json, carrier.exit and their temporary files. Do not create, overwrite, append to, repair, normalize or forge any runner-owned artifact. Do not read diagnostic log bodies for this task. +Copy the example's "log_ref" as an opaque diagnostic reference; it needs no creation, repair or narrative log. Another existing non-empty diagnostic reference is allowed only when the task explicitly supplies it. +Complete all work and verification BEFORE publication. Your LAST tool action must write result.json.tmp and atomically rename it to result.json, then write completion.sentinel.tmp and atomically rename it to completion.sentinel. +After publishing, immediately return your compact final reply. Do not run further tools, inspect artifacts or rewrite result/sentinel after publication. +These are worker obligations, not filesystem isolation; runner validation still requires successful carrier termination and never treats the sentinel alone as success. EOF : > "$stdout_ref" && : > "$stderr_ref" && : > "$last_message_ref" || return 1 if started_at=$(date -u '+%Y-%m-%dT%H:%M:%SZ' 2>/dev/null); then :; else started_at=; fi diff --git a/skills/sshx/tests/test_run_codex_worker.py b/skills/sshx/tests/test_run_codex_worker.py index 4a746c6c..d7e99de5 100644 --- a/skills/sshx/tests/test_run_codex_worker.py +++ b/skills/sshx/tests/test_run_codex_worker.py @@ -72,6 +72,26 @@ mv "$result_ref.tmp" "$result_ref" write_sentinel ;; + brief_contract) + ownership=false; opaque=false; final_action=false; immediate_return=false + case "$brief" in *"Worker-owned: only result.json, completion.sentinel"*"Runner-owned: brief.md, worker.stdout.log, worker.stderr.log, last-message.txt, status.json, carrier.exit"*"Do not create, overwrite, append to, repair, normalize or forge"*) ownership=true ;; esac + case "$brief" in *"Copy the example's"*"opaque diagnostic reference"*"no creation, repair or narrative log"*) opaque=true ;; esac + case "$brief" in *"Complete all work and verification BEFORE publication"*"LAST tool action"*"atomically rename"*) final_action=true ;; esac + case "$brief" in *"immediately return your compact final reply"*"Do not run further tools"*) immediate_return=true ;; esac + printf '{"conclusion":{"verdict":"%s","ownership":%s,"opaque":%s,"final_action":%s,"immediate_return":%s},"log_ref":"fake-log"}\n' "$verdict" "$ownership" "$opaque" "$final_action" "$immediate_return" > "$result_ref.tmp" + mv "$result_ref.tmp" "$result_ref"; write_sentinel + ;; + overwrite_and_rewrite_nonzero|overwrite_and_rewrite_zero) + # Deliberate simulated violation: prompt obligations are not an OS boundary. + printf '%s\n' forged > "$run_dir/worker.stdout.log" + write_result; write_sentinel + verdict=reject; write_result + [ "$FAKE_MODE" != overwrite_and_rewrite_nonzero ] || exit 9 + ;; + invalid_after_sentinel) + write_result; write_sentinel + printf '%s\n' '{"conclusion":' > "$result_ref" + ;; bad_verdict) verdict=unexpected; write_result; write_sentinel ;; missing_sentinel) write_result ;; stdout_only) printf '%s\n' '{"conclusion":{"verdict":"propose"},"log_ref":"fake-log"}'; printf '%s\n' 'completion marker' ;; @@ -381,6 +401,27 @@ def test_time_lookup_failure_is_diagnostic_only(self) -> None: self.assertIsNone(result.status["finished_at"]) self.assertIsNone(result.status["duration_seconds"]) + def test_received_brief_conveys_ownership_and_last_action_for_every_stage(self) -> None: + for stage, verdict in (("thinking", "propose"), ("implementation", "unused"), + ("review", "approve"), ("termination", "satisfied")): + with self.subTest(stage=stage): + result = self.run_worker("brief_contract", stage=stage, extra_env={"FAKE_VERDICT": verdict}) + self.assert_terminal(result, "COMPLETE") + conclusion = json.loads((result.run_dir / "result.json").read_text())["conclusion"] + self.assertTrue(all(conclusion[key] for key in + ("ownership", "opaque", "final_action", "immediate_return"))) + + def test_simulated_artifact_violations_do_not_replace_terminal_predicate(self) -> None: + failed = self.run_worker("overwrite_and_rewrite_nonzero") + self.assert_terminal(failed, "CARRIER_EXIT_NONZERO") + self.assertEqual((failed.run_dir / "worker.stdout.log").read_text(), "forged\n") + self.assertEqual(json.loads((failed.run_dir / "result.json").read_text())["conclusion"]["verdict"], "reject") + # Honest limit: no same-user write protection or write-history audit is claimed. + completed = self.run_worker("overwrite_and_rewrite_zero") + self.assert_terminal(completed, "COMPLETE") + self.assertEqual(completed.status["verdict"], "reject") + self.assert_terminal(self.run_worker("invalid_after_sentinel"), "ENVELOPE_INVALID") + def test_nonzero_carrier_wins_even_with_complete_artifacts(self) -> None: result = self.run_worker("nonzero_with_artifacts") self.assert_terminal(result, "CARRIER_EXIT_NONZERO") diff --git a/skills/sshx/tests/test_skill_distribution.py b/skills/sshx/tests/test_skill_distribution.py new file mode 100644 index 00000000..2c85f59f --- /dev/null +++ b/skills/sshx/tests/test_skill_distribution.py @@ -0,0 +1,84 @@ +"""Observe distribution bytes, independently of host discovery/session adoption. + +Temporary complete skill copies exercise the README's manual comparison boundary. +No installer, host settings, global copies, carrier or network service is invoked. +""" + +import hashlib +import json +import os +import shutil +import subprocess +import tempfile +import unittest +from pathlib import Path + + +ROOT = Path(__file__).resolve().parents[3] +SKILL = ROOT / "skills" / "sshx" + + +def directory_contents(root: Path) -> dict[str, str]: + """Observe published file bytes; build outputs and Python caches are not shipped.""" + contents: dict[str, str] = {} + for directory, subdirs, files in os.walk(root): + subdirs[:] = [name for name in subdirs if name not in {".lake", "__pycache__"}] + for name in files: + path = Path(directory) / name + contents[str(path.relative_to(root))] = hashlib.sha256(path.read_bytes()).hexdigest() + return contents + + + +class SkillDistributionTests(unittest.TestCase): + def test_complete_copy_symlink_edit_and_manual_refresh(self) -> None: + expected = directory_contents(SKILL) + self.assertIn("SKILL.md", expected) + self.assertIn("scripts/run-codex-worker.sh", expected) + self.assertIn("CODEX_WORKER_SPEC.md", expected) + manifest_version = json.loads((ROOT / "package.json").read_text())["version"] + revision = subprocess.check_output(["git", "rev-parse", "HEAD"], cwd=ROOT, text=True).strip() + self.assertEqual(len(revision), 40) + with tempfile.TemporaryDirectory(prefix="sshx-distribution-") as temp: + copied = Path(temp) / "copied" + shutil.copytree(SKILL, copied, ignore=shutil.ignore_patterns(".lake", "__pycache__")) + selected = Path(temp) / "selected" + selected.symlink_to(copied, target_is_directory=True) + self.assertEqual(selected.resolve(), copied.resolve()) + self.assertEqual(directory_contents(selected), expected) + observed = subprocess.check_output( + ["shasum", "-a", "256", str(selected / "SKILL.md")], text=True + ).split()[0] + self.assertEqual(observed, expected["SKILL.md"]) + + # Manifest/checkout metadata stays identical while copied content diverges. + with (copied / "SKILL.md").open("a") as stream: + stream.write("\nLocal distribution edit.\n") + self.assertNotEqual(directory_contents(selected)["SKILL.md"], observed) + self.assertEqual(json.loads((ROOT / "package.json").read_text())["version"], manifest_version) + self.assertEqual(subprocess.check_output( + ["git", "rev-parse", "HEAD"], cwd=ROOT, text=True + ).strip(), revision) + + # Refresh the whole unit in this fixture, including a divergent support file. + support = copied / "CODEX_WORKER_SPEC.md" + support.write_text("stale support file\n") + shutil.copytree(SKILL, copied, dirs_exist_ok=True, + ignore=shutil.ignore_patterns(".lake", "__pycache__")) + self.assertEqual(directory_contents(selected), expected) + support.write_text("locally changed support file\n") + changed = directory_contents(selected) + self.assertEqual(changed["SKILL.md"], observed) + self.assertNotEqual(changed, expected) # SKILL.md hash alone misses support drift. + + # Repointing a discovery link selects different bytes; no session reload is inferred. + alternate = Path(temp) / "alternate" + shutil.copytree(SKILL, alternate, ignore=shutil.ignore_patterns(".lake", "__pycache__")) + selected.unlink() + selected.symlink_to(alternate, target_is_directory=True) + self.assertEqual(selected.resolve(), alternate.resolve()) + self.assertEqual(directory_contents(selected), expected) + + +if __name__ == "__main__": + unittest.main() diff --git a/skills/sshx/tests/test_sshx_contract.py b/skills/sshx/tests/test_sshx_contract.py index dd29fc5f..39239fdc 100644 --- a/skills/sshx/tests/test_sshx_contract.py +++ b/skills/sshx/tests/test_sshx_contract.py @@ -313,6 +313,93 @@ existing consumers for all opt-in/exposure combinations; model evidence cannot prove live heca capability or change the earlier real-tool evidence cutoffs. +Issues #1071-#1074 incident-derived no-skill baseline (2026-10-31, recorded +before this batch's skill/spec/runner/model edits): the supplied issue reports are +untrusted historical evidence, not newly observed carrier behavior. #1071 reports a +beta.54 loaded copy and five unapproved Heca launches; #1072 reports stdout overwrite, +post-sentinel result rewrites and two interrupted carriers; #1073 reports synthetic +Git-state blockers and an owner restriction omitted from briefs; #1074 reports five +paraphrased family names across three passes. Installation cause, timeout causality, +the host census, historical incidents and counterfactual time savings are NOT replayed +or verified here. Without the proposed guidance, these incidents motivate the missing +boundaries; they do not establish what a fresh no-skill evaluator would do. +Newly observed pre-edit source evidence in this clean worktree: Heca already requires +current-run opt-in and exposed tools, and runner nonzero exit already fails closed. +The actual injected brief permits replacing log_ref without conveying runner-owned +stdout/stderr/last-message/brief/status/exit ownership or immediate final return. +BlockingAuthority accepts a self-labelled ordinary-operation without workflow/input +provenance or sourced owner admission restriction. mechanism_family explicitly uses +exact equality, and the class gate supplies no settled-prior family correspondence. +These are source observations, not live host failures. Preserve the completed opt-in +and terminal checks. Forward evidence must distinguish simulated runner regressions, +composed operational Lean guards, and any explicitly scoped real Codex invocation. +No fresh no-skill agent experiment, historical host access, global update, or Heca +probe is claimed. This baseline is source-owned; runtime logs remain untracked. + +ARCH-001 / QUALITY-1074-01 repair baseline (2026-10-31, before this repair's +implementation edits): a fresh ``lake env lean --stdin`` check imported the current +Behavior.Model and constructed a one-pass FamilyEvidence with no prior label, no +settled prior, an evidenced reason new, peer-free inputs, no earlier unsupported +enumeration, no owner/domain change and unknown class coverage. It compiled exit 0: +classGateActive=false, familyRoute=reviseOrInvestigate, and familyPassAllowed for +repairWithRerunReview=false. The same check proved universally that no ProtocolState +or ImplementationPlan can admit that repair through the production allowed/guardPass. +This records a current compiled contract/model mismatch, not a host stall or a new +no-skill evaluator experiment. SKILL.md already permits a family_basis reason new and +the initial review's finite repair; no contract or authorized domain change is needed. +The forward regression must compose the initial review, first paid repair, whole-batch +implementation and included review, while preserving unresolved comparison, verified +paraphrase recurrence, distinct-cause and class-coverage routes at the same consumers. + +Changed-runner real Codex evidence (2026-10-31, after baseline and runner edits): +installed codex-cli 0.161.0, changed sanctioned runner, standalone peer-free arithmetic +brief, temporary work target/run root, foreground supervised subprocess (no detachment +or active-artifact polling). One terminal collection through the sanctioned status +reader reported flight 6ae50ea40dc75dc5193fdea7 attempt 1 COMPLETE, carrier exit 0, +duration 30 seconds. The compact result reported assertion 2 + 2 = 4 passed and +received worker-only result/sentinel, runner-owned diagnostics, opaque log_ref, last +atomic publication and immediate-return obligations. Only terminal compact result and +status metadata were collected; no reasoning/log bodies or write-history audit. +This observes receipt-to-successful-terminal for this bounded run, not historical +incident replay, timeout causality, adversarial compliance or same-user isolation. +The brief-contract and deliberate overwrite/post-sentinel regressions are simulations, +not additional live carrier observations. No Heca or installation refresh was run. + +Issue #1075 / distribution follow-up baseline (2026-11-04, before this assignment's +contract/model/test edits; inherited dirty candidate on c97a7e03): source inspection +still finds risk-only Trigger activation, an unconditional startup-question ban, +and BlockingAuthority force from two named conjuncts without evidence_status or +user_goal_basis. appendRevision preserves batch, flights and stage: dependent +pending/review/repair authority is not revoked. These are observed source gaps; +the issue's permission-expansion incident is supplied historical evidence, not a +fresh no-skill evaluator result. A pre-edit Lean probe did NOT compile: the pinned +4.33.0 toolchain was unavailable and its automatic global download was interrupted. +No compiled-baseline or new real-carrier claim is made. Existing S1 identity tests +assert guidance but do not observe copied/symlinked/edited complete directories. +Forward evidence must exercise actual admission/revision consumers and read real +temporary distribution files; source hashes cannot establish session adoption. +The earlier #1071-#1074 baseline and caller-reported carrier evidence retain their +original scope and timing; they are not observations by this assignment. + +ARCH-001 / TEST-1073-01 frozen repair baseline (2026-11-04): before this batch, +the delegating caller supplied two independent compiled counterexamples against +the dirty candidate. A confirmed, goal-sourced input with a failed trigger was +advisory to review/plan admission but blocking to focusedRoundRequired, goalGapOf, +RemainingDifference.counts and mayBeSoleBasis; downgradeRecord returned no record. +These names map to the same cause: the generic Input projection lost trigger +provenance. The supplied baseline authorizes S3/C6/S6 correspondence repair only; +it is not a new live host incident or a baseline compiled by this repair worker. +Forward verification calls the existing consumers with one DecisionBasis and +checks failed-trigger rejection parametrically, plus ordinary/manual/fixture/ +owner-restricted evidence classes. Constructed fixtures prove formal behavior, +not actual workflow occurrence, provenance truth or real-carrier compliance. + +Official guidance checked read-only on 2026-11-04: fetched +https://developers.openai.com/codex/skills/ (symlink discovery, change detection, +restart if not visible) and https://code.claude.com/docs/en/discover-plugins.md +(plugin update and session reload). No installation/refresh/reload was exercised; +Cursor/Gemini procedures and session adoption remain ASSUMED-UNVERIFIED. + The behavior helpers below cover fixed truth tables and other load-bearing mechanical contracts, but do not infer English semantics. Files outside ``skills/sshx/SKILL.md`` are outside this positional boundary and remain governed @@ -509,14 +596,12 @@ "decision_ownership", "disown", "escalate", - "exit", "external-prior-exposed", "fidelity", "finding_downgrades", "fix", "fix_or_done", "flight_id", - "goal_gap", "harness", "harness.decision_ownership", "harness.provided_capabilities", @@ -531,9 +616,16 @@ "log_ref", "malicious", "mechanism_family", + "family_basis", + "input_evidence", + "evidence_status", + "confirmed", + "advisory", + "conditional", + "unverified", + "user_goal_basis", "meta_judge", "natural-ownership", - "next_iteration_question", "nohup", "none", "normalized_goal", @@ -605,7 +697,7 @@ "When a repair consumes the reserved capacity, the caller may add evaluation units after seeing " "the repair result so the mandatory rerun review and termination roster remain reachable." ) -CANONICAL_NORMATIVE_DOCUMENT_SHA256 = "3c919b7e5936a12ff48fb2f04307e37db9dd047b016baa978b80248684722e87" +CANONICAL_NORMATIVE_DOCUMENT_SHA256 = "f590f8a8529b03053cbcd63a2d9478ede828a1261af3d9976ddc57fd93a2f6f2" JsonValue: TypeAlias = None | bool | int | float | str | list["JsonValue"] | dict[str, "JsonValue"] GapOwnerAssignment: TypeAlias = tuple[JsonValue, JsonValue] @@ -905,9 +997,13 @@ def blocking_force( names_work_evidence: bool, basis_shown_false: bool, basis_disputed: bool, + evidence_status: str, + user_goal_basis: str, ) -> str: del basis_disputed - if basis_shown_false: + if evidence_status not in {"confirmed", "advisory", "conditional", "unverified"}: + raise ContractFailure("invalid evidence status") + if basis_shown_false or evidence_status != "confirmed" or not user_goal_basis: return "advisory" if names_goal_term and names_work_evidence: return "blocking" @@ -921,19 +1017,33 @@ def blocking_finding_force( basis_shown_false: bool, trigger_path: str, recorded_occurrence: str | None, + evidence_status: str, + user_goal_basis: str, fields: frozenset[str] | None = None, occurrence_pre_run: bool = True, + workflow_input_basis: bool = True, + observed_input: bool = False, + owner_actual_only: bool = False, + owner_rule_sourced: bool = True, ) -> str: required_fields = frozenset( - {"trigger", "trigger_actor", "trigger_path", "mechanism_family", "recorded_occurrence"} + {"trigger", "trigger_actor", "trigger_path", "mechanism_family", "family_basis", "input_evidence", "recorded_occurrence", "evidence_status", "user_goal_basis"} ) if fields is not None and fields != required_fields: raise ContractFailure("blocking finding metadata is incomplete") + if owner_actual_only and not owner_rule_sourced: + raise ContractFailure("owner admission restriction lacks a source") if trigger_path not in {"ordinary-operation", "nonstandard-deliberate", "malicious"}: raise ContractFailure("invalid trigger path") - if basis_shown_false or not (names_goal_term and names_work_evidence): + if blocking_force(names_goal_term=names_goal_term, names_work_evidence=names_work_evidence, + basis_shown_false=basis_shown_false, basis_disputed=False, + evidence_status=evidence_status, user_goal_basis=user_goal_basis) != "blocking": + return "advisory" + occurrence = recorded_occurrence is not None and occurrence_pre_run + ordinary = trigger_path == "ordinary-operation" and workflow_input_basis + if not (ordinary or occurrence): return "advisory" - if trigger_path != "ordinary-operation" and (recorded_occurrence is None or not occurrence_pre_run): + if owner_actual_only and not (observed_input or occurrence): return "advisory" return "blocking" @@ -1175,7 +1285,7 @@ def test_sshx_implementation_handoff_has_one_source_owner(self) -> None: text = read(SKILL) implementation = section(text, "## Implementation Worker", "## Review Triplet") repair = section(text, "## Fix Or Done", "## Termination Gate") - owner = "Send goal, verifiable acceptance, authorized scope/prohibitions" + owner = "Send goal, verifiable acceptance, scope/prohibitions" self.assertEqual(text.count(owner), 1) self.assertIn(owner, implementation) self.assertIn("under `## Implementation Worker` handoff, allowance and evidence rules", repair) @@ -1205,7 +1315,7 @@ def test_sshx_goal_iteration_behavior_contract(self) -> None: text = read(SKILL) self.assertIn("`intake` (write `GoalArtifact` and normalize the goal)", text) protocol_section = text[heading_index(text, "## InlineConsensusProtocol") : heading_index(text, "## Worker Delegation")] - for anchor in ["`visible_inputs`", "`GoalArtifact`", "`harness`", "same-round peer outputs"]: + for anchor in ["`visible_inputs`", "`GoalArtifact`", "`harness`", "same-round peer output"]: self.assertIn(anchor, protocol_section) self.assertIn( "`revise` must name the goal gap and a next iteration question; it must not open an unrelated design search", @@ -1244,7 +1354,7 @@ def test_sshx_harness_and_revisions_contract(self) -> None: self.assertIn("append-only list", goal_section) self.assertIn("missing any one of these sub-items is invalid and fails closed", goal_section) self.assertIn("before any worker dispatch", goal_section) - self.assertIn("must not ask a startup boundary or harness confirmation question", goal_section) + self.assertIn("must not ask a routine startup boundary or harness confirmation question", goal_section) self.assertIn("routine missing detail is resolved with the smallest task-relevant assumption", goal_section) self.assertNotIn("must ask the boundary owner", goal_section) self.assertIn("non-adversarial, not infallible", goal_section) @@ -1826,32 +1936,32 @@ def test_sshx_blocking_authority_contract(self) -> None: self.assertIn(definition, reasoning) for anchor in [ "Advisory is the default; blocking is the exception", - "exactly two conjuncts that the input itself must name", - "first, the `normalized_goal` clause, `constraints` item, or `success_criteria` item that the work as built fails", - "second, evidence in the work as built that shows the failure", - "a current call site or input path, an observed failure, a failing verification command, a wrong result", - "against a satisfaction claim, the absence of the evidence the named term demands", + "exactly two conjuncts the input itself must name", + "the failed `normalized_goal` clause, `constraints` item or `success_criteria` item", + "evidence in the work as built", + "current call site/input path, observed failure, failing verification, wrong result", + "absence of evidence the term demands", "A blocking finding must also pass the structured trigger check", - "if its `trigger_path` is not `ordinary-operation` and its `recorded_occurrence` is `none`, the finding is advisory", + "A tool manual or review fixture alone proves capability/reachability, never ordinary workflow input or occurrence", + "future ordinary workflow-produced inputs remain eligible", "recorded_occurrence` must have existed before this run and independently of the current review", - "a fixture, reproduction, or state deliberately created by a seat, caller, or repair worker during this run is reachability evidence only", - "An input that names both is blocking, and stays blocking however expensive, inconvenient, or late the repair is", - "a named basis that evidence shows to be false no longer counts as named", - "keeps its full blocking force until the dispute is settled against evidence", - "no one may call an input advisory because its named basis is unpersuasive", - "An input that names fewer than both is advisory", - "its downgrade record carries what it named, or that it named none, in its own words and never a paraphrase", - "never the sole basis of a `revise`, `reject`, `abstain`, blocking finding, `unsatisfied`, or any element of a concrete plan", - "The same two conjuncts admit a plan element", - "names the `GoalArtifact` term that demands it or a current consumer (an existing call site)", - "a test introduced together with it may corroborate that basis but never creates it", - "Failure is objective, not semantic", - "asks only whether both conjuncts are named, never how well they are evidenced", - "it removes no actual defect", - "a reachable failure, a trusted-party mistake, an omission, and a stated uncertainty each name both", + "deliberately constructed run fixtures/reproductions/states are reachability evidence only", + "After these admission checks, both named conjuncts block regardless of repair cost, inconvenience or lateness", + "Evidence showing a basis false removes it", + "disputed correctness retains full force until evidence settles it", + "never downgrade for being unpersuasive", + "Fewer than both, or a failed trigger check, is advisory", + "record its original words (including what it named or none) and trigger decision, never paraphrase", + "never use it alone for `revise`, `reject`, `abstain`, `unsatisfied`, a blocker or a plan element", + "The same two conjuncts and evidence-status/goal-basis checks admit a plan element", + "name the demanding `GoalArtifact` term or current consumer (existing call site)", + "a co-introduced test corroborates but cannot create that basis", + "force asks whether both conjuncts are named", + "not how persuasive they are", + "workflow grounding and owner-policy compliance remain trigger-check premises", ]: self.assertIn(anchor, reasoning) - self.assertEqual(text.count("The same two conjuncts admit a plan element"), 1) + self.assertEqual(text.count("The same two conjuncts and evidence-status/goal-basis checks admit a plan element"), 1) for forbidden in [ "an unverified path has no blocking force", "an unverified named basis loses blocking force", @@ -1879,6 +1989,7 @@ def test_sshx_blocking_authority_contract(self) -> None: names_work_evidence=evidence, basis_shown_false=shown_false, basis_disputed=disputed, + evidence_status="confirmed", user_goal_basis="current goal / contract source", ) for goal_term, evidence, shown_false, disputed in [ (True, True, False, False), @@ -1893,7 +2004,7 @@ def test_sshx_blocking_authority_contract(self) -> None: ) def test_sshx_trigger_metadata_mechanically_downgrades_local_fixtures(self) -> None: - fields = frozenset({"trigger", "trigger_actor", "trigger_path", "mechanism_family", "recorded_occurrence"}) + fields = frozenset({"trigger", "trigger_actor", "trigger_path", "mechanism_family", "family_basis", "input_evidence", "recorded_occurrence", "evidence_status", "user_goal_basis"}) self.assertEqual( ( blocking_finding_force( @@ -1903,6 +2014,7 @@ def test_sshx_trigger_metadata_mechanically_downgrades_local_fixtures(self) -> N trigger_path="ordinary-operation", recorded_occurrence=None, fields=fields, + evidence_status="confirmed", user_goal_basis="current goal / contract source", ), blocking_finding_force( names_goal_term=True, @@ -1911,6 +2023,7 @@ def test_sshx_trigger_metadata_mechanically_downgrades_local_fixtures(self) -> N trigger_path="nonstandard-deliberate", recorded_occurrence=None, fields=fields, + evidence_status="confirmed", user_goal_basis="current goal / contract source", ), blocking_finding_force( names_goal_term=True, @@ -1919,6 +2032,7 @@ def test_sshx_trigger_metadata_mechanically_downgrades_local_fixtures(self) -> N trigger_path="nonstandard-deliberate", recorded_occurrence="issue-1058", fields=fields, + evidence_status="confirmed", user_goal_basis="current goal / contract source", ), ), ("blocking", "advisory", "blocking"), @@ -1931,6 +2045,7 @@ def test_sshx_trigger_metadata_mechanically_downgrades_local_fixtures(self) -> N trigger_path="invented-path", recorded_occurrence=None, fields=fields, + evidence_status="confirmed", user_goal_basis="current goal / contract source", ) with self.assertRaises(ContractFailure): blocking_finding_force( @@ -1940,8 +2055,44 @@ def test_sshx_trigger_metadata_mechanically_downgrades_local_fixtures(self) -> N trigger_path="ordinary-operation", recorded_occurrence=None, fields=fields - {"trigger_actor"}, + evidence_status="confirmed", user_goal_basis="current goal / contract source", ) + def test_workflow_input_and_sourced_owner_restriction_projection(self) -> None: + # Projections of interpreted evidence; real operational review/repair guards are Lean-tested. + base = dict(names_goal_term=True, names_work_evidence=True, basis_shown_false=False, + trigger_path="ordinary-operation", recorded_occurrence=None, + evidence_status="confirmed", user_goal_basis="current goal / contract source") + cases = ( + ({"evidence_status": "advisory"}, "advisory"), + ({"evidence_status": "conditional"}, "advisory"), + ({"evidence_status": "unverified"}, "advisory"), + ({"user_goal_basis": ""}, "advisory"), + ({"workflow_input_basis": False}, "advisory"), # manual/fixture alone + ({"workflow_input_basis": True}, "blocking"), # future workflow input, no census hit + ({"owner_actual_only": True}, "advisory"), + ({"owner_actual_only": True, "observed_input": True}, "blocking"), + ({"owner_actual_only": True, "recorded_occurrence": "independent incident"}, "blocking"), + ({"owner_actual_only": True, "recorded_occurrence": "review fixture", "occurrence_pre_run": False}, "advisory"), + ) + for changes, expected in cases: + with self.subTest(changes=changes): + self.assertEqual(blocking_finding_force(**(base | changes)), expected) + with self.assertRaisesRegex(ContractFailure, "lacks a source"): + blocking_finding_force(**(base | {"owner_actual_only": True, "owner_rule_sourced": False})) + + def test_effective_source_and_current_policy_evidence_have_one_owner(self) -> None: + delegation = section(read(SKILL), "## Worker Delegation", "## Result Envelope") + for anchor in ("effective path/SHA-256", "manifest/release distinction", + "disk/upstream change proves no adoption", "Explicit user disable overrides host opt-in", + "retry, fallback, repair and resume", "without re-probing"): + self.assertIn(anchor, delegation) + for name in ("README.md", "README.zh-CN.md"): + guide = read(ROOT / name) + self.assertIn("shasum -a 256 /SKILL.md", guide) + self.assertIn("https://developers.openai.com/codex/skills/", guide) + self.assertIn("/reload-plugins", guide) + def test_sshx_issue_1058_controls_are_declared_at_their_owners(self) -> None: text = read(SKILL) goal = section(text, "## Goal Contract", "## InlineConsensusProtocol") @@ -1951,13 +2102,13 @@ def test_sshx_issue_1058_controls_are_declared_at_their_owners(self) -> None: fix_or_done = section(text, "## Fix Or Done", "## Termination Gate") self.assertIn("resolves them from current user input, repository rules", goal) self.assertIn("recording sources and explicitly labelling minimal engineering assumptions", goal) - self.assertIn("must not ask a startup boundary or harness confirmation question", goal) - for field in ["trigger", "trigger_actor", "trigger_path", "mechanism_family", "recorded_occurrence"]: + self.assertIn("must not ask a routine startup boundary or harness confirmation question", goal) + for field in ["trigger", "trigger_actor", "trigger_path", "mechanism_family", "family_basis", "input_evidence", "recorded_occurrence", "evidence_status", "user_goal_basis"]: self.assertIn(f"`{field}`", envelope) self.assertIn("fields required by `## Result Envelope`", review_truth) self.assertIn("Every review focus in a dispatch brief must name the `GoalArtifact` clause", review) self.assertIn("An unbounded request to find any mechanism that could make a result fail is invalid", review) - self.assertIn("after two consecutive passes whose blocking findings name the same `GoalArtifact` term and `mechanism_family`", fix_or_done) + self.assertIn("after two consecutive passes whose blocking findings name the same `GoalArtifact` term and evidenced family", fix_or_done) self.assertIn("member-by-member enumeration leaves the property unsupported", fix_or_done) self.assertIn("verified coverage basis under `## Reasoning Discipline`", fix_or_done) reasoning = section(text, "## Reasoning Discipline", "## Thinking Panel") @@ -1971,7 +2122,7 @@ def test_sshx_intake_and_class_gate_use_existing_owner_paths(self) -> None: formal = SKILL.parent / "formal" guards = read(formal / "Sshx" / "Reasoning" / "Guards.lean") repair = read(formal / "Sshx" / "Reasoning" / "Repair.lean") - self.assertIn("must not ask a startup boundary or harness confirmation question", text) + self.assertIn("must not ask a routine startup boundary or harness confirmation question", text) self.assertNotIn("IntakeScopeAnswers", guards) self.assertNotIn("intakeScopeComplete", guards) self.assertNotIn("repeatedFamilyRoute", guards) @@ -2109,7 +2260,7 @@ def test_sshx_enumeration_escape_requires_verified_construction(self) -> None: ), "no finite listing of cases is escape-free" not in reasoning, "the longer the list grows the likelier" not in reasoning, - "when a verified finite construction hypothesis applies, its register cannot be completed, while an open or infinite domain still needs a class-coverage basis" in verification, + "verified finite-construction hypotheses defeat register closure; open/infinite domains still need class coverage" in verification, finite_listing_closure_force( fixed_point_free_constructor_verified=True, finite_domain_completeness_proven=False, @@ -2186,7 +2337,7 @@ def test_sshx_depth_discipline_contract(self) -> None: ) trigger = section(text, "## Trigger", "## Goal Contract") self.assertIn( - "whether to run it follows decision risk, not available budget", + "Risk informs proportionality, never supplies authorization", trigger, ) @@ -2279,14 +2430,14 @@ def test_sshx_blocking_authority_stage_references_and_downgrade_guards(self) -> "the causal prediction recorded in that conclusion is falsifiable rather than a preference;", "provided the objection passes `BlockingAuthority`", "An advisory objection does not trigger a `FocusedRound`", - "checks only whether the seat named both conjuncts and must not assess their persuasiveness", - "named a basis whose correctness is disputed still triggers the round because disputed is not absent", + "after admission checks, the meta-judge checks only whether both conjuncts are named, never their persuasiveness", + "admitted confirmed basis disputed on correctness still triggers: disputed is not absent", "records that decline in the existing `finding_downgrades` record under the same own-words requirement that governs downgrades", ]: self.assertIn(anchor, focused_round) for anchor in [ "An objection that fails `BlockingAuthority` is not an unclosed `GoalArtifact` goal gap and does not by itself hold the exit out of `implement`: the meta-judge records it as advisory in the existing `finding_downgrades` record as `BlockingAuthority` requires.", - "Disputed grounding stays blocking", + "Admitted confirmed disputed grounding stays blocking", "not permission to set aside a reachable defect", ]: self.assertIn(anchor, design) @@ -2298,7 +2449,7 @@ def test_sshx_blocking_authority_stage_references_and_downgrade_guards(self) -> "never because a finding is inconvenient", "never sets aside a reachable defect", "Harness gaps and claim authority follow `## Goal Contract`", - "without startup confirmation", + "material owner-clarification rule", ]: self.assertIn(anchor, review) self.assertIn( @@ -2309,7 +2460,7 @@ def test_sshx_blocking_authority_stage_references_and_downgrade_guards(self) -> self.assertIn("an advisory worry is not a remaining difference", termination_gate) for anchor in [ "Each termination seat applies `BlockingAuthority` itself before returning", - "An `unsatisfied` that names both conjuncts keeps its full force and may never be converted into permission by calling it unpersuasive", + "An admitted confirmed `unsatisfied` that names both conjuncts keeps its full force and may never be converted into permission by calling it unpersuasive", "An `unsatisfied` that names no `GoalArtifact` term is advisory exactly as under `## Review Truth Table`", "the meta-judge records it in `finding_downgrades` as `BlockingAuthority` requires", "re-dispatches that seat once on the same sealed candidate with that record in its brief as part of the same evaluation", @@ -2334,12 +2485,12 @@ def test_sshx_triplets_require_reasoning_discipline_in_conclusion(self) -> None: for required in [ "Reference-frame", - "applicable mature theory, engineering principle, industry best practice", - "mature industry case, mature pattern", + "applicable mature theory/principle, industry practice/case/pattern", + "industry practice/case/pattern", "constraint framework", "known-good shape", "`no applicable mature theory found`", - "root-cause and minimal-path re-check against `GoalArtifact`", + "root-cause/minimal-path re-check against `GoalArtifact`", ]: self.assertIn(required, reasoning_section) self.assertEqual( @@ -2409,7 +2560,7 @@ def test_sshx_triplets_require_reasoning_discipline_in_conclusion(self) -> None: ]: self.assertIn(boundary, boundaries) self.assertIn( - "This does not override `GoalArtifact`, assigned bias or review focus, truth tables, or allowed verdict sets", + "This never overrides `GoalArtifact`, bias/focus, truth tables or verdict sets", reasoning_section, ) self.assertEqual(len(re.findall(r"^## Reasoning Discipline$", text, flags=re.MULTILINE)), 1) @@ -2457,15 +2608,15 @@ def test_sshx_triplets_require_reasoning_discipline_in_conclusion(self) -> None: review_section.index("Each reviewer returns one of:"), ) self.assertIn( - "applicable mature theory, engineering principle, industry best practice", + "applicable mature theory/principle, industry practice/case/pattern", reasoning_section, ) self.assertNotIn( - "applicable mature theory, engineering principle, industry best practice", + "applicable mature theory/principle, industry practice/case/pattern", thinking_section.lower(), ) self.assertNotIn( - "applicable mature theory, engineering principle, industry best practice", + "applicable mature theory/principle, industry practice/case/pattern", review_section.lower(), ) @@ -2499,11 +2650,11 @@ def test_sshx_thinking_panel_seats_and_anchors_root_cause(self) -> None: thinking_section, ) self.assertIn( - "`worth` (值不值) is an independent objective, not the aesthetic lens repeated", + "`worth` (值不值) is independent of aesthetics", thinking_section, ) self.assertIn( - "the panel is not homogenized into every seat re-deriving the same value verdict", + "Only its own seat derives this verdict, preserving distinct objectives", thinking_section, ) self.assertIn("must state whether it hits `CapabilityOverlap`", thinking_section) @@ -2523,7 +2674,7 @@ def test_sshx_cardinalities_relevance_and_pass_budget_are_protocol_policy(self) ( text.count("Protocol policy, not a mathematical consequence:"), "Carrier heterogeneity is this protocol's policy, not a theorem premise or consequence" in text, - "Protocol policy, not mathematics, defines these two conjuncts" in text, + "Protocol policy, not mathematics, defines these conjuncts" in text, "before the first pass after the initial review triplet, the caller may record one owner-precommitted finite integer `pass_budget`; by default it records no cap" in text, ), (6, True, True, True), @@ -2549,12 +2700,12 @@ def test_sshx_fixed_routing_units_and_reflection_actions(self) -> None: all( anchor in design_section for anchor in [ - "An `implement` exit also requires", + "An `implement` exit requires", "unresolved harness overlap", "authority gap", - "missing host/controller execution capability", - "repeat a capability already declared by the harness", - "goal gap to the maintainer", + "missing host/controller execution", + "repeating a provided capability", + "goal gaps to the maintainer", ] ), "missing Design Truth Table harness/authority implement route", @@ -2592,7 +2743,7 @@ def test_sshx_fixed_routing_units_and_reflection_actions(self) -> None: for anchor in [ "Harness gaps and claim authority follow `## Goal Contract`", "claim authority follow `## Goal Contract`", - "without startup confirmation", + "material owner-clarification rule", ] ), "missing autonomous intake authority guard", @@ -3474,14 +3625,14 @@ def test_sshx_result_envelope_contract(self) -> None: "Every canonical `SshxResultEnvelope` recorded from `thinking_panel_workers`, `meta_judge`, `implementation_worker`, `review_triplet_workers`, and `fix_or_done` uses exactly these top-level fields", text, ) - self.assertIn("A caller-carried stage record wraps this envelope", text) + self.assertIn("Stage records reference envelope `conclusion`/`log_ref`", text) self.assertIn("The envelope payload itself stays exactly `conclusion` and `log_ref`", text) self.assertIn("is a read-only mirror of its envelope's `conclusion.verdict`", text) self.assertIn( "`conclusion.verdict` is the sole verdict source for routing, the two must be equal, and any mismatch fails closed", text, ) - self.assertIn("`conclusion`: compact structured result consumed by the caller", text) + self.assertIn("`conclusion`: compact structured decisions", text) self.assertIn("`log_ref`: artifact reference for the non-inline worker", text) self.assertIn("treated as an opaque diagnostic pointer", text) self.assertIn("must not open, inline, summarize, or otherwise consume its content", text) @@ -3489,14 +3640,14 @@ def test_sshx_result_envelope_contract(self) -> None: self.assertNotIn("The caller may open the referenced artifact on demand", text) for forbidden_inline in [ "process logs", - "step-by-step reasoning", - "raw transcripts", - "debug output", + "reasoning", + "transcripts", + "debug", "same-round peer output", ]: self.assertIn(forbidden_inline, text) - self.assertIn("Logs are not inline in caller context", text) - self.assertIn("Final reports aggregate `conclusion` values only", text) + self.assertIn("never inline logs", text) + self.assertIn("Final reports aggregate only `conclusion`", text) self.assertIn("aggregate and report conclusions only, retaining `log_ref` references", text) self.assertIn("opaque `log_ref`", text) self.assertIn("without inlining logs", text) @@ -4098,13 +4249,13 @@ def test_worker_tool_spec_states_sweep_semantics(self) -> None: def test_sshx_baseline_evidence_is_source_owned(self) -> None: text = read(SKILL) for failure_mode in [ - "fake consensus: self-application, pseudo-isolation, missing worker-mode declaration, or caller self-certification", + "fake consensus: self-application, pseudo-isolation, undeclared worker mode, self-certification", "false grounding: unverified premises, retrospective fit, imagined relevance", - "rabbit-holing: blocking by default, peripheral detail, repeated unchanged work, finite case registers, procedural findings against the run's own records", + "rabbit-holing: default blocking, peripheral/repeated work, case registers, procedural findings", "goal loss: 忘记目标 drift to an unranked target, 因小失大 a part served at the whole's cost, or 买椟还珠 form held above substance", - "wrong convergence: beauty without worth, scalarized incomparable candidates", - "contaminated adjudication: same-round peer evidence, an out-of-prefix ledger event", - "boundary drift: carrier diversity over-claims, improvised worker mechanics", + "wrong convergence: beauty without worth, scalarized incomparability", + "contaminated adjudication: peer/out-of-prefix/dependency-reaching evidence", + "boundary drift: diversity overclaims, improvised mechanics", ]: self.assertIn(failure_mode, text) self.assertIn("source-owned contract or test evidence", text)