diff --git a/.claude-plugin/marketplace.json b/.claude-plugin/marketplace.json index 25f4d7f0..4ebb2c15 100644 --- a/.claude-plugin/marketplace.json +++ b/.claude-plugin/marketplace.json @@ -9,7 +9,7 @@ { "name": "consensus-rnd", "description": "worker-delegated inline consensus：隔离多视角、固定真值表，无 daemon、GitHub 或 git 编排", - "version": "1.0.0-beta.46", + "version": "1.0.0-beta.47", "source": "./", "author": { "name": "auric", diff --git a/.claude-plugin/plugin.json b/.claude-plugin/plugin.json index 270d4864..e6b991c3 100644 --- a/.claude-plugin/plugin.json +++ b/.claude-plugin/plugin.json @@ -1,7 +1,7 @@ { "name": "consensus-rnd", "description": "worker-delegated inline consensus skills：隔离多视角、固定真值表，无 daemon、GitHub 或 git 编排", - "version": "1.0.0-beta.46", + "version": "1.0.0-beta.47", "author": { "name": "auric", "email": "loning.ma@aelf.io" diff --git a/.codex-plugin/plugin.json b/.codex-plugin/plugin.json index 29d53ace..20acb5b4 100644 --- a/.codex-plugin/plugin.json +++ b/.codex-plugin/plugin.json @@ -1,6 +1,6 @@ { "name": "consensus-rnd", - "version": "1.0.0-beta.46", + "version": "1.0.0-beta.47", "description": "worker-delegated inline consensus skills：隔离多视角、固定真值表，无 daemon、GitHub 或 git 编排", "author": { "name": "auric", diff --git a/.cursor-plugin/plugin.json b/.cursor-plugin/plugin.json index 982efc0d..82d3614d 100644 --- a/.cursor-plugin/plugin.json +++ b/.cursor-plugin/plugin.json @@ -2,7 +2,7 @@ "name": "consensus-rnd", "displayName": "Consensus R&D", "description": "worker-delegated inline consensus skills：隔离多视角、固定真值表，无 daemon、GitHub 或 git 编排", - "version": "1.0.0-beta.46", + "version": "1.0.0-beta.47", "author": { "name": "auric", "email": "loning.ma@aelf.io" diff --git a/gemini-extension.json b/gemini-extension.json index 51f2ea7b..9a6cb911 100644 --- a/gemini-extension.json +++ b/gemini-extension.json @@ -1,6 +1,6 @@ { "name": "consensus-rnd", "description": "worker-delegated inline consensus skills：隔离多视角、固定真值表，无 daemon、GitHub 或 git 编排", - "version": "1.0.0-beta.46", + "version": "1.0.0-beta.47", "contextFileName": "GEMINI.md" } diff --git a/package.json b/package.json index e19f30a1..987a643c 100644 --- a/package.json +++ b/package.json @@ -1,6 +1,6 @@ { "name": "consensus-rnd", - "version": "1.0.0-beta.46", + "version": "1.0.0-beta.47", "description": "worker-delegated inline consensus skills：隔离多视角、固定真值表，无 daemon、GitHub 或 git 编排", "license": "MIT", "author": "auric ", diff --git a/skills/sshx/SKILL.md b/skills/sshx/SKILL.md index 2ba501e5..55b9b4c8 100644 --- a/skills/sshx/SKILL.md +++ b/skills/sshx/SKILL.md @@ -38,7 +38,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 must ask the boundary owner who consumes outputs produced by the execution environment and whether trusted operators' local state (configuration, indexes, and filesystem) is inside the review scope; the answers must be stated in the existing `harness.trust_boundary` and, where applicable, the declared recovery path in `harness.provided_capabilities`, and neither controller nor worker may infer an answer that was not confirmed by the boundary owner. +During `intake`, the caller resolves these sub-items from the user's current input, repository rules, existing authorizations, and available execution context; it records those sources and labels any minimal engineering assumptions explicitly. 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. `revisions` is an append-only list whose each item contains exactly these three sub-items: @@ -52,9 +52,9 @@ Any explicit correction to `GoalArtifact` or `harness` must append one such revi 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. If any `harness` sub-item is missing or ambiguous, or its source has not been confirmed by the boundary owner, stop and escalate to the maintainer; neither controller nor worker may infer or expand it. +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 boundary owner may declare a host-provided goal-driven continuation mechanism only in `harness.provided_capabilities`; the skill must not discover or infer whether one exists. The termination gate is triggered only by a positive, boundary-owner-confirmed entry declaring such a mechanism. When an otherwise complete, unambiguous, boundary-owner-confirmed `provided_capabilities` value contains no such entry, whether silent or explicitly negative, the gate is inapplicable without asserting that the host mechanism is absent. A purported continuation entry that is ambiguous or unconfirmed is governed by the existing harness rule above. +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. The user's current input is the only source for the goal. `sshx` must not discover or infer the goal from external lifecycle milestones, release state, runtime host configuration, GitHub issues, GitHub pull requests, labels, branches, or any other external lifecycle surface. @@ -212,12 +212,12 @@ 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. 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` — 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. 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. By the Lawvere fixed-point theorem, every finite listing of cases is escaped by a fixed-point-free self-application, and an adversarial seat's charter is such a constructor; so no extension of this or any register can complete it, and the defense against an unlisted case is the two-conjunct test together with the declared recovery path, never another entry. Extending an enumeration over an absorbed class is an ugly defect under the aesthetic verdict, not diligence. Without that construction hypothesis, a separately proven finite-domain completeness result remains admissible. +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. @@ -290,6 +290,11 @@ Implement only the concrete plan approved by the thinking gate. Keep the impleme Implementation must be delegated to a worker using the stage's default carrier under `WorkerDelegationContract`. The caller context may pass the approved concrete plan and constraints, then receive `conclusion` and `log_ref`; changed-file and test evidence belong in `conclusion`, and process logs stay behind `log_ref`. +An approved plan may span finite flights within `implementation_worker`; predeclare assignments and their allowance in its conclusion. Worker conclusions accumulate completed and remaining obligations and test evidence; terminal flight completion permits handoff only. Pending work or checks stay in implementation within the allowance; exhaustion or failure reports unresolved work. The local allowance is separate from `pass_budget` and carrier retry/fallback bounds. Scope changes retain the existing correction, direction and class gates. + +Admit the initial review triplet once all approved work and checks have worker evidence, with no active or unrecovered failed flight. Tests continue during implementation; routing never substitutes for independent review. + + ## Review Triplet Protocol policy, not a mathematical consequence: after implementation, run three review perspectives: @@ -322,29 +327,29 @@ 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` — the `GoalArtifact` term the work as built fails and the evidence in the work that shows it — and which class of failure, omission, or uncertainty within the declared trust boundary it addresses. It must also carry the structured `trigger`, `trigger_actor`, `trigger_path`, `mechanism_family`, and `recorded_occurrence` 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. A `BlockingAuthority` downgrade is objective: it is recorded as `BlockingAuthority` requires and never assesses persuasiveness; disputed grounding stays blocking. 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. A missing, ambiguous, or stale harness declaration is never a downgrade shield: pause routing and escalate to the maintainer instead of declaring done. +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. ## 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. -If review exits `fix`, ask what still differs from `GoalArtifact`, apply the smallest change that addresses that blocking goal gap by delegating it to a worker using the stage's default carrier exactly as `## Implementation Worker` requires - open a new `SshxWorkerFlightRecord` for the same `work_target` and stay orchestration-only for the repair - then rerun the review triplet on the worker's returned `conclusion`. When a pass carries more than one blocking goal gap, repair them in goal-primacy rank, so the main path is repaired first. Stop when `pass_budget` owned below is exhausted and report remaining blockers honestly. +If review exits `fix`, freeze admitted fixes as one finite batch using `## Implementation Worker` decomposition, allowance and evidence rules. 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, 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 `mechanism_family`, the gate must decide at the class level whether that failure family is inside the declared `harness.trust_boundary`; if the harness does not declare that family, stop and escalate to the boundary owner rather than continue by adding a more general defense. A class-level decision may use only the recorded findings and confirmed harness, not a new fixture created to justify another repair. +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. 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. If review exits `done with advisory surfaced`, treat that exit as a candidate for an affirmative success claim rather than the claim itself when `## Termination Gate` applies, and route the candidate through that gate before reporting success. Include any non-blocking advisory feedback without inlining logs. -If review exits `explicit user decision or another bounded review pass`, either run one more bounded pass with a concrete next iteration question tied to `GoalArtifact`, or ask the user to decide. Do not loop indefinitely. +If review exits `explicit user decision or another bounded review pass`, run one more bounded pass with a concrete next iteration question tied to `GoalArtifact`; when no bounded pass remains, report the unresolved evidence and route it to the declared owner. Do not pause for routine confirmation or ask the user to choose a method, and do not loop indefinitely. -After any explicit correction, use the existing correction 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 before further work. +After any explicit correction, repeat this section's direction gate before further work. -This section is the sole owner of `pass_budget`. Protocol policy, not a mathematical consequence: before the first pass after the initial review triplet, the caller records one owner-precommitted finite integer `pass_budget`. Each later pass — a `meta-layer convergence`, a `focused round`, a repair flight together with its mandatory rerun review triplet, a repeated review pass without a repair, or a termination-gate evaluation including one that exits `reject fake termination consensus` — consumes exactly one unit when it is dispatched. The budget is immutable for this run: no result, repair, or correction may add, replenish, reset, or replace units, and a unit is never refunded. Carrier retries and fallbacks are bounded by each flight's `retry_budget` and the finite eligible-untried-carrier set and consume no unit; the initial review triplet is the single occurrence fixed by the stage order and consumes none. Because `pass_budget` is a strictly decreasing natural number, the run terminates: reaching zero reports every unresolved blocker honestly and is never evidence of method stop or goal completion. A run with no recorded `pass_budget` has no pass authority: it stops at the initial review exit and reports that. +This section is the sole owner of `pass_budget`. Protocol policy, not a mathematical consequence: before the first pass after the initial review triplet, the caller records one owner-precommitted finite integer `pass_budget`. Each later pass — a `meta-layer convergence`, a `focused round`, a finite repair batch together with its mandatory rerun review triplet, a repeated review pass without a repair, or a termination-gate evaluation including one that exits `reject fake termination consensus` — consumes exactly one unit when it is dispatched. The batch debit includes all bounded assignments and final review even at zero remaining units, with no subsequent pass authority. The budget is immutable for this run: no result, repair, or correction may add, replenish, reset, or replace units, and a unit is never refunded. Carrier retries and fallbacks are bounded by each flight's `retry_budget` and the finite eligible-untried-carrier set and consume no unit; the initial review triplet is the single occurrence fixed by the stage order and consumes none. Because `pass_budget` is a strictly decreasing natural number, the run terminates: reaching zero reports every unresolved blocker honestly and is never evidence of method stop or goal completion. A run with no recorded `pass_budget` has no pass authority: it stops at the initial review exit and reports that. ## Termination Gate -`## Termination Gate` is a conditional subgate reached inside `fix_or_done`, never an additional `InlineConsensusProtocol` stage. It applies only when `## Goal Contract` supplies its positive, boundary-owner-confirmed `harness.provided_capabilities` entry and the caller is about to assert that `GoalArtifact` is satisfied. The gate permits only that `GoalArtifact`-scoped claim; it does not certify any broader host goal condition. +`## Termination Gate` is a conditional subgate reached inside `fix_or_done`, never an additional `InlineConsensusProtocol` stage. It applies only when an existing positive authoritative `harness.provided_capabilities` entry is present and the caller is about to assert that `GoalArtifact` is satisfied. Ambiguous or unconfirmed authority withholds or escalates that claim under the existing table; it never creates a startup confirmation question. The gate permits only that `GoalArtifact`-scoped claim; it does not certify any broader host goal condition. The gate binds every exit that carries an affirmative `GoalArtifact` satisfaction claim, wherever the claim appears — a final report, a `done with advisory surfaced` outcome used as success, or a `stop` action carrying the claim — and binds no exit that carries none; non-achievement exits keep their existing routing and must never be relabelled as goal satisfaction. `## Goal Contract` solely owns missing or invalid trigger-entry routing; this gate does not restate it. @@ -427,6 +432,7 @@ Without this skill, lightweight high-risk decisions tend to regress to these sou - wrong convergence: beauty without worth, scalarized incomparable candidates, path-dependent gain on non-additive coordinates, or 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. ## Transcript Template @@ -459,6 +465,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 the same verified construction hypothesis applies, the register cannot be completed, and 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. 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 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 b5dbc982..082a780c 100644 --- a/skills/sshx/formal/README.md +++ b/skills/sshx/formal/README.md @@ -14,7 +14,7 @@ No module contains `sorry`, `axiom`, `native_decide`, or a proposition defined a | Layer | Modules | What it formalizes | |---|---|---| | Mechanics | `Sshx/*.lean` | verdict alphabets, carriers and fallback, flight accounting, the completion predicate, `BlockingAuthority` and downgrade, the three truth tables (exhaustive, order-sensitive), `pass_budget`, gate applicability and binding, isolation, records, stage order | -| Behavior | `Sshx/Behavior/*.lean` | the caller as an operational model: `ProtocolState`, one `Action` per caller act, one guard per "must" clause, `step`, `Reachable`, and safety invariants over every reachable state | +| Behavior | `Sshx/Behavior/*.lean` | the caller as an operational model: `ProtocolState`, one `Action` per caller act, one guard per "must" clause, `step`, `Reachable`, finite implementation batches, shared whole-candidate review readiness, and safety invariants over every reachable state | | Reasoning | `Sshx/Reasoning/*.lean` | the reasoning logic every seat applies: reference frame, aesthetic verdict, seek truth from facts, mathematical applicability, prospective evidence, depth discipline, goal primacy, boundary checks, blocking authority in full, the six seats and the locus dyad, meta-judge convergence and the focused round, review downgrade, repair passes, termination seats and ownership routing | | Semantics | `Sshx/Semantics/*.lean` | the contract's concepts as instances of the kernel-frozen theorems of [trureturing](https://github.com/the-omega-institute/trureturing) (`D5`, pinned by commit in `lakefile.toml`); each instance discharges the theorem's premises with `sshx` structures | | Clauses | `Sshx/Clauses/*.lean` | the remaining definitional clauses: identity and trigger, goal contract records, protocol records, envelope, completion, context pollution, worker delegation mechanics, boundaries, baseline failure modes, verification | @@ -31,7 +31,7 @@ defined elsewhere; `prose` an explanatory sentence with no norm of its own, whic | `sshx` concept | trureturing object | instance | |---|---|---| -| register of advisory shapes; adversarial seat | listing `g : A → A → Force`, twist `flip` (no fixed point) | `every_register_escaped`, `register_diagonal_unlisted`, `every_register_counted` via `escape_all_of_fixfree`, `escaped_card_of_fixfree` | +| register of advisory shapes; adversarial seat | qualified finite listing `g : A → A → Force`, twist `flip` (no fixed point), with verified theorem hypotheses and an admissible-input correspondence | `every_register_escaped`, `register_diagonal_unlisted`, `every_register_counted` via `escape_all_of_fixfree`, `escaped_card_of_fixfree`; the abstract theorem does not establish a real counterexample without that correspondence | | written `GoalArtifact` vs user intent; goal gap | current concept `q`, target `T`, `defectRelation q T` | `goalGap` | | blocking findings joined over passes; `pass_budget` | countable check language `Γ`, unit cost, `finiteBudgetEnvelope` | `goal_gap_budget_envelope` via `budget_envelope_infimum_and_limit`: antitone in budget, never below the all-finite infimum of the same language | | independent adjudication evidence; dependency closure | `AdmissionContext`, `AdmissibleJudge`, `AdaptiveUse` | `enlarging_closure_only_removes_admission` via `dependency_closure_admission_antitone`; `adaptive_use_is_inadmissible` | @@ -52,6 +52,50 @@ Declared non-instances, with the reason each premise does not match `sshx`: `conclusion.verdict`; widen the absorber instead of adding a case) are modeled in the mechanics and reasoning layers only. +## Composed routes + +`Sshx/Behavior/Scenarios.lean` proves each action's actual `allowed` guard along composed +initial multi-flight, repair, included-last-unit-review, carrier recovery/exhaustion, +tests-seat fallback, autonomous-intake, and single-flight traces. Effect assertions also +check partial/active/failed/exhausted work. Approved-plan fixtures supply the prior thinking +settlement; these traces do not prove the truth of worker evidence or reviewer approval. + +Gate applicability is derived from one current continuation source. Intake records the +initial source; only an owner-authorized, source-supported append-only correction can +update it afterward. The correction evidence is a formal interpretation of the existing +revision, not a new runtime record or an English authority detector. The original target +and revision prefix remain intact. `TerminationEvidence` pairs the supplied roster with +its evaluated `ContinuationAuthority`, including the source's ledger position. The actual +evaluation guard requires that association to match current authority; its effect retains +the supplied association and applies the unchanged truth table to the roster. It does not +stamp old results with evaluation-time authority. A relevant correction preserves the old +verdict and snapshot, while both reevaluation and the claim guard refuse stale evidence, +even when applicability stays positive, the source payload repeats, or an earlier source +is restored. An unrelated note preserves usable evidence at both consumers. + +General guard/effect and reachable-state proofs connect each affirmative claim to an +admitted evaluation whose supplied evidence still matches current authority. Guarded +regressions distinguish old A1 evidence refused after an authorized A2 correction from +separately supplied current A2 evidence accepted with the same verdicts. They also cover +repeated/restored sources, unchanged authority, and unsupported/unowned corrections. +The association and semantic truth of external evidence remain premises; this is no +provenance authentication scheme or new runtime record. There is no independent declaration +action. + +Fallback uses the existing +`nextCarrier` selector against tried carriers projected from one assignment's flight history. +The original flight id is a ghost assignment link preserved by replacements, so distinct +approved assignments on the same target remain distinct. Every admitted fallback strictly +reduces that assignment's untried-carrier remainder. Draws, review dispatch and fallback +share the executable-carrier restriction for the tests seat. + +The model's `launchDelegated` action projects the existing direct oracle/subagent invocation; +Codex still requires `launchViaRunner`. Both paths require launch and host completion before +collection. 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. + ## What the model cannot verify The trace ties each clause to a Lean object, and the Lean kernel checks the object. Whether diff --git a/skills/sshx/formal/Sshx.lean b/skills/sshx/formal/Sshx.lean index 5f03713c..b5038ac5 100644 --- a/skills/sshx/formal/Sshx.lean +++ b/skills/sshx/formal/Sshx.lean @@ -14,6 +14,7 @@ import Sshx.Semantics.Adjudication import Sshx.Semantics.Stop import Sshx.Behavior.Model import Sshx.Behavior.Invariant +import Sshx.Behavior.Scenarios import Sshx.Reasoning.Discipline import Sshx.Reasoning.Authority import Sshx.Reasoning.Guards diff --git a/skills/sshx/formal/Sshx/Behavior/Invariant.lean b/skills/sshx/formal/Sshx/Behavior/Invariant.lean index cc0ff2e2..b7a356c5 100644 --- a/skills/sshx/formal/Sshx/Behavior/Invariant.lean +++ b/skills/sshx/formal/Sshx/Behavior/Invariant.lean @@ -102,10 +102,10 @@ theorem safe_step {s : ProtocolState} {a : Action} (hs : Safe s) (ha : allowed s obtain ⟨h1, h2, h4, h5, h6, h7, h8, h9⟩ := hs cases a with | inspectReadOnly => exact ⟨h1, h2, h4, h5, h6, h7, h8, h9⟩ - | writeGoal g => + | writeGoal g e => refine ⟨h1, ?_, h4, h5, h6, h7, h8, h9⟩ intro _; simp [step] - | appendRevision r => + | appendRevision r e => refine ⟨h1, ?_, h4, h5, h6, h7, h8, h9⟩ intro hm have := h2 hm @@ -144,7 +144,7 @@ theorem safe_step {s : ProtocolState} {a : Action} (hs : Safe s) (ha : allowed s rcases hf with hf | hf · exact h6 f hf · rw [hf]; simp [newFlight] - | launchViaRunner id => + | launchViaRunner id | launchDelegated id => have hu := refs_attempt_updateFlight (s := s) (id := id) (g := fun f => { f with launched := true }) (fun x _ hr => by simpa using h5 x ‹_› (by simpa using hr)) @@ -209,14 +209,15 @@ theorem safe_step {s : ProtocolState} {a : Action} (hs : Safe s) (ha : allowed s · rw [hi]; exact ha · exact h7 i hi | recordPassBudget units => exact ⟨h1, h2, h4, h5, h6, h7, h8, h9⟩ - | pass t => exact ⟨h1, h2, h4, h5, h6, h7, h8, h9⟩ + | beginImplementation p => exact ⟨h1, h2, h4, h5, h6, h7, h8, h9⟩ + | recordImplementation id completed checks => exact ⟨h1, h2, h4, h5, h6, h7, h8, h9⟩ + | pass t e p => exact ⟨h1, h2, h4, h5, h6, h7, h8, h9⟩ | advanceStage => exact ⟨h1, h2, h4, h5, h6, h7, h8, h9⟩ - | declareGate a => exact ⟨h1, h2, h4, h5, h6, h7, h8, h9⟩ - | evaluateTermination source roster => + | evaluateTermination source evidence => refine ⟨h1, h2, h4, h5, h6, h7, h8, ?_⟩ intro e he simp only [step, Option.some.injEq] at he - exact ⟨source, roster, he.symm⟩ + exact ⟨source, evidence.roster, he.symm⟩ | claimSatisfied => exact ⟨h1, h2, h4, h5, h6, h7, h8, h9⟩ | lifecycle op => exact ha.elim | oracleReference url isPublic pinned => exact ⟨h1, h2, h4, h5, h6, h7, h8, h9⟩ @@ -281,18 +282,19 @@ theorem termination_exit_from_table {s : ProtocolState} (h : Reachable s) (e : T -- SKILL[inv]: "The gate permits only that `GoalArtifact`-scoped claim; it does not certify any broader host goal condition." theorem claim_only_under_permitted_gate (s : ProtocolState) (ha : allowed s .claimSatisfied) : - s.gate = .applies → s.terminationExit = some .claimPermitted := - ha.2.2 + s.gate = .applies → s.terminationExit = some .claimPermitted ∧ + s.terminationAuthority = some s.continuationAuthority := + ha.2.2.1 -- SKILL[inv]: "Because `pass_budget` is a strictly decreasing natural number, the run terminates: reaching zero reports every unresolved blocker honestly and is never evidence of method stop or goal completion." theorem budget_never_increases (s : ProtocolState) (a : Action) (ha : allowed s a) (b b' : Nat) (hb : s.passBudget = some b) (hb' : (step s a).passBudget = some b') : b' ≤ b := by cases a case recordPassBudget units => obtain ⟨-, hnone⟩ := ha; simp [hnone] at hb - case pass t => + case pass t e p => simp only [step, hb, Option.bind_some] at hb' exact Sshx.step_le b t b' hb' - case evaluateTermination source roster => + case evaluateTermination source evidence => simp only [step, hb, Option.bind_some] at hb' exact Sshx.step_le b _ b' hb' case fallbackFlight id carrier => @@ -322,4 +324,236 @@ theorem stage_never_regresses (s : ProtocolState) (a : Action) : split <;> simp all_goals simp [step, updateFlight] +/-- Flight completion alone cannot open initial formal review. -/ +theorem initial_advance_needs_whole_candidate (s : ProtocolState) + (hs : s.stage = .implementation) (ha : allowed s .advanceStage) : + s.reviewReady = true := ha.2.2.2.1 hs + +/-- Both normal and included repair review consume the same readiness projection. -/ +-- SKILL[inv]: "Complete the batch before its one mandatory rerun review triplet; a chunk boundary never starts formal review." +theorem review_dispatch_needs_whole_candidate (s : ProtocolState) (role : Role) + (carrier : Carrier) (target : String) (retries : Nat) + (ha : allowed s (.openFlight .review role carrier target retries)) : + s.reviewReady = true := ha.2.2.2.2.1 + +/-- Each new assignment consumes one predeclared local slot; retries/fallback use their own bounds. -/ +-- SKILL[inv]: "The local allowance is separate from `pass_budget` and carrier retry/fallback bounds." +theorem implementation_consumes_local_slot (s : ProtocolState) (carrier : Carrier) + (target : String) (retries : Nat) (b : ImplementationBatch) (hb : s.batch = some b) : + (step s (.openFlight .implementation .implementation carrier target retries)).batch = + some { b with flightsLeft := b.flightsLeft - 1, checksPassed := false } := by + simp [step, hb] + +/-- The included review never debits the pass budget again. -/ +theorem included_review_preserves_budget (s : ProtocolState) (role : Role) + (carrier : Carrier) (target : String) (retries : Nat) : + (step s (.openFlight .review role carrier target retries)).passBudget = s.passBudget := rfl + +/-- Unsupported member enumeration cannot enter the actual paid repair dispatch. -/ +theorem unsupported_class_cannot_start_batch (s : ProtocolState) (e : Reasoning.FamilyEvidence) + (p : Option ImplementationPlan) (h : e.coverageBasis = .unsupportedMemberEnumeration) + (ha : Reasoning.classGateActive e = true) : + ¬ allowed s (.pass .repairWithRerunReview e p) := by + simp [allowed, guardPass, Reasoning.unsupported_class_never_dispatches e h ha] + +/-- After intake, only an authorized, source-supported append-only correction may +change the authority consumed by claims. This covers every source update, not one pair +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 + 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⟩ + case fallbackFlight id carrier => + simp only [step] at hc + split at hc <;> exact (hc rfl).elim + all_goals exact (hc rfl).elim + +/-- The source position is derived from the revision ledger, never selected by evidence. -/ +theorem authority_revision_in_ledger {s : ProtocolState} (h : Reachable s) : + ∀ g, s.goal = some g → s.continuationAuthority.revision ≤ g.revisions.length := by + induction h with + | initial => simp [ProtocolState.initial] + | @move s a _ ha ih => + clear ha + cases a + case writeGoal g e => simp [step] + case appendRevision r e => + intro g' hg' + cases hg : s.goal with + | none => simp [step, hg] at hg' + | some g => + have heq : g.correct r = g' := by simpa [step, hg] using hg' + subst g' + 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 + | some source => + simp [step, ProtocolState.correctedAuthority, he, hg, GoalArtifact.correct] + case fallbackFlight id carrier => + simp only [step] + split <;> exact ih + all_goals exact ih + +/-- Every relevant correction advances the source position, including identical payloads. -/ +theorem correction_advances_authority {s : ProtocolState} (h : Reachable s) + (r : Revision) (e : RevisionEvidence) (source : ContinuationSource) + (ha : allowed s (.appendRevision r e)) (he : e.continuation = some source) : + s.continuationAuthority.revision < + (step s (.appendRevision r e)).continuationAuthority.revision := by + cases hg : s.goal with + | none => simp [allowed, guardAppendRevision, ProtocolState.goalWritten, hg] at ha + | some g => + have hi := authority_revision_in_ledger h g hg + simp [step, ProtocolState.correctedAuthority, he, hg] + omega + +/-- The current gate always projects the current source, including all corrected entries. -/ +theorem correction_projects_current_source (s : ProtocolState) (r : Revision) + (e : RevisionEvidence) (source : ContinuationSource) (he : e.continuation = some source) : + (step s (.appendRevision r e)).gate = applicability source.entry := by + simp [step, ProtocolState.gate, ProtocolState.correctedAuthority, he] + +/-- Appending a correction keeps the recorded settlement frozen. Its authority snapshot +is checked by the later claim guard, rather than rewriting the old verdict. -/ +theorem correction_keeps_settlement (s : ProtocolState) (r : Revision) (e : RevisionEvidence) : + (step s (.appendRevision r e)).terminationExit = s.terminationExit ∧ + (step s (.appendRevision r e)).terminationAuthority = s.terminationAuthority := ⟨rfl, rfl⟩ + +theorem correction_keeps_revision_prefix (s : ProtocolState) (g : GoalArtifact) + (hg : s.goal = some g) (r : Revision) (e : RevisionEvidence) : + ∃ g', (step s (.appendRevision r e)).goal = some g' ∧ g.revisions <+: g'.revisions := by + exact ⟨g.correct r, by simp [step, hg], g.correct_prefix r⟩ + +/-- A changed authority cannot reuse a prior affirmative settlement, even if both +sources map to `applies`. Unrelated notes retain their authority and evidence. -/ +theorem stale_authority_cannot_claim (s : ProtocolState) (hg : s.gate = .applies) + (hs : s.terminationAuthority ≠ some s.continuationAuthority) : + ¬ allowed s .claimSatisfied := by + intro ha + exact hs ((claim_only_under_permitted_gate s ha hg).2) + +/-- Admission consumes the incoming evidence association; the effect retains it and +uses the unchanged truth table. No evaluation-time source stamp supplies provenance. -/ +theorem evaluation_preserves_evidence_source (s : ProtocolState) (source : ClaimSource) + (e : TerminationEvidence) (ha : allowed s (.evaluateTermination source e)) : + e.authority = s.continuationAuthority ∧ + (step s (.evaluateTermination source e)).terminationAuthority = some e.authority ∧ + (step s (.evaluateTermination source e)).terminationExit = + some (terminationRoute source e.roster) := ⟨ha.1, rfl, rfl⟩ + +/-- This rejection is independent of verdict values, presentation and remaining budget. -/ +theorem stale_evidence_cannot_evaluate (s : ProtocolState) (source : ClaimSource) + (e : TerminationEvidence) (hs : e.authority ≠ s.continuationAuthority) : + ¬ allowed s (.evaluateTermination source e) := fun ha => hs ha.1 + +/-- Every relevant correction rejects evidence for the earlier authority, including +an identical source payload or restoration. The ledger, not payload inequality, proves it. -/ +theorem correction_rejects_prior_evidence {s : ProtocolState} (h : Reachable s) + (r : Revision) (re : RevisionEvidence) (correctedSource : ContinuationSource) + (ha : allowed s (.appendRevision r re)) (he : re.continuation = some correctedSource) + (source : ClaimSource) (e : TerminationEvidence) (hs : e.authority = s.continuationAuthority) : + ¬ allowed (step s (.appendRevision r re)) (.evaluateTermination source e) := by + apply stale_evidence_cannot_evaluate + intro equal + have advance := correction_advances_authority h r re correctedSource ha he + have sameRevision := congrArg ContinuationAuthority.revision (hs.symm.trans equal) + omega + +/-- 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) + (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, + ProtocolState.gate, ProtocolState.reviewComplete, ProtocolState.reviewReady, + ProtocolState.batchSettled, ProtocolState.batchFlights] + +/-- A recorded settlement has an actual admitted evaluation with the same supplied +evidence/source association. Later corrections preserve that historical witness. -/ +theorem settlement_has_evidence_source {s : ProtocolState} (h : Reachable s) : + ∀ exit, s.terminationExit = some exit → + ∃ evaluated source e, Reachable evaluated ∧ + allowed evaluated (.evaluateTermination source e) ∧ + e.authority = evaluated.continuationAuthority ∧ + s.terminationAuthority = some e.authority ∧ exit = terminationRoute source e.roster := by + induction h with + | initial => simp [ProtocolState.initial] + | @move s a hr ha ih => + cases a + case evaluateTermination source e => + intro exit he + have hexit : exit = terminationRoute source e.roster := by + simpa [step] using he.symm + exact ⟨s, source, e, hr, ha, ha.1, rfl, hexit⟩ + case fallbackFlight id carrier => + simp only [step] + split <;> exact ih + all_goals exact ih + +/-- A reachable affirmative claim under an applicable gate has evidence that was +admitted for its own source and still corresponds to the current authority. -/ +theorem claim_has_current_evidence {s : ProtocolState} (h : Reachable s) + (ha : allowed s .claimSatisfied) (hg : s.gate = .applies) : + ∃ evaluated source e, Reachable evaluated ∧ + allowed evaluated (.evaluateTermination source e) ∧ + e.authority = evaluated.continuationAuthority ∧ + e.authority = s.continuationAuthority ∧ + terminationRoute source e.roster = .claimPermitted := by + obtain ⟨hexit, hcurrent⟩ := claim_only_under_permitted_gate s ha hg + obtain ⟨evaluated, source, e, hr, he, hs, hstored, hroute⟩ := + settlement_has_evidence_source h .claimPermitted hexit + exact ⟨evaluated, source, e, hr, he, hs, + Option.some.inj (hstored.symm.trans hcurrent), hroute.symm⟩ + +/-- The actual fallback effect updates the assignment's history, including when the caller +reuses an earlier abstained id. New implementation assignments get their own original id. -/ +theorem fallback_records_tried (s : ProtocolState) (id : Nat) (c : Carrier) (f : FlightRec) + (hf : s.flight id = some f) : + (step s (.fallbackFlight id c)).triedCarriers f.assignment = + (s.triedCarriers f.assignment).insert c := by + cases c <;> + simp [step, hf, ProtocolState.triedCarriers, reopenFlight, CarrierSet.insert, List.any_append] + +/-- A strict bound on the actual fallback consumer, not just the isolated selector. -/ +theorem fallback_decreases_remaining (s : ProtocolState) (id : Nat) (c : Carrier) + (ha : allowed s (.fallbackFlight id c)) : + ∃ 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 + 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) + +/-- 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 + simp [allowed, guardOpenFlight, guardReviewFlight, seatEligible, canRunRepositoryCommands] + +theorem tests_fallback_excludes_oracle (s : ProtocolState) (id : Nat) (f : FlightRec) + (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 + have heq : g = f := Option.some.inj (hg.symm.trans hf) + subst g + have eligible := nextCarrier_eligible _ (CarrierSet.mem_univ _) _ (CarrierSet.mem_univ _) + .nyxidOracle (Carrier.mem_univ _) hn + simp [ProtocolState.eligibleCarriers, CarrierSet.get, hs, hr, seatEligible, + canRunRepositoryCommands] at eligible + end Sshx.Behavior diff --git a/skills/sshx/formal/Sshx/Behavior/Model.lean b/skills/sshx/formal/Sshx/Behavior/Model.lean index d84d812b..a861d0f7 100644 --- a/skills/sshx/formal/Sshx/Behavior/Model.lean +++ b/skills/sshx/formal/Sshx/Behavior/Model.lean @@ -5,6 +5,7 @@ import Sshx.Gate import Sshx.Tables import Sshx.Records import Sshx.Protocol +import Sshx.Reasoning.Repair /-! # Behavior: the caller's operational model @@ -84,6 +85,9 @@ inductive LifecycleOp /-- One flight as the caller records it (`SshxWorkerFlightRecord` plus launch bookkeeping). -/ structure FlightRec where id : Nat + /-- Ghost link to the original flight of this assignment; fallback preserves it. + Derived from dispatch history, not an added worker record field. -/ + assignment : Nat stage : FlightStage role : Role carrier : Carrier @@ -97,9 +101,84 @@ structure FlightRec where notified : Bool deriving DecidableEq, Repr +/-- Semantic projection of the source/assumption record inside the existing harness. +These facts are review inputs, not inferred from nonempty text or a runtime schema. -/ +structure IntakeEvidence where + recordedHarness : Harness + sources : List String + assumptionsLabeled : Bool + minimalTaskRelevantScope : Bool + explicitBoundariesPreserved : Bool + inventedAuthority : Bool + startupQuestionAsked : Bool + continuation : ContinuationEntry + deriving DecidableEq, Repr + +def IntakeEvidence.complete (e : IntakeEvidence) : Prop := + e.sources ≠ [] ∧ e.assumptionsLabeled = true ∧ + e.minimalTaskRelevantScope = true ∧ e.explicitBoundariesPreserved = true ∧ + e.inventedAuthority = false ∧ e.startupQuestionAsked = false + +/-- Current semantic projection of `harness.provided_capabilities`, supplied as evidence. +The model does not parse English to establish correspondence or owner authority. -/ +structure ContinuationSource where + providedCapabilities : List String + entry : ContinuationEntry + deriving DecidableEq, Repr + +/-- The source's position in the existing append-only revision ledger, not a runtime field. -/ +structure ContinuationAuthority where + source : ContinuationSource + revision : Nat + deriving DecidableEq, Repr + +/-- The roster's evaluated continuation source, supplied with the sealed evidence. +This projects the existing versioned, scoped inputs; it is not a runtime schema or +an authenticity check. Evidence truth and its association are premises. Evaluation +must preserve this association, never manufacture it from the evaluation-time state. -/ +structure TerminationEvidence where + authority : ContinuationAuthority + roster : Roster + deriving DecidableEq, Repr + +/-- Interpretation of an existing revision and its authorization. `none` means the +revision does not change continuation authority. Support and ownership are independent +evidence inputs, never inferred from a nonempty authorization string. -/ +structure RevisionEvidence where + recordedRevision : Revision + ownerAuthorized : Bool + sourceSupported : Bool + continuation : Option ContinuationSource + deriving DecidableEq, Repr + +def RevisionEvidence.valid (e : RevisionEvidence) (r : Revision) : Prop := + e.recordedRevision = r ∧ e.ownerAuthorized = true ∧ e.sourceSupported = true + def FlightRec.active (f : FlightRec) : Bool := f.status == .inFlight || f.status == .retrying +/-- Finite decomposition in the existing approved plan/batch conclusion, not a runtime schema. -/ +structure ImplementationPlan where + obligations : List String + flightAllowance : Nat + deriving DecidableEq, Repr + +-- SKILL[def]: "An approved plan may span finite flights within `implementation_worker`; predeclare assignments and their allowance in its conclusion." +def ImplementationPlan.valid (p : ImplementationPlan) : Prop := + p.obligations ≠ [] ∧ 0 < p.flightAllowance + +/-- Ghost projection of accumulated worker conclusions. `firstFlight` scopes the current +candidate; it is also reset for an explicitly budgeted repeated review. -/ +structure ImplementationBatch where + remaining : List String + checksPassed : Bool + flightsLeft : Nat + firstFlight : Nat + deriving DecidableEq, Repr + +def ImplementationPlan.start (p : ImplementationPlan) (firstFlight : Nat) : ImplementationBatch := + ⟨p.obligations, false, p.flightAllowance, firstFlight⟩ + /-- The caller-side protocol state. -/ structure ProtocolState where stage : Stage @@ -109,8 +188,11 @@ structure ProtocolState where flights : List FlightRec context : List ContextItem passBudget : Option Nat - gate : Applicability + batch : Option ImplementationBatch + continuationAuthority : ContinuationAuthority terminationExit : Option TerminationExit + /-- Evaluated source retained from the evidence consumed by the settlement. -/ + terminationAuthority : Option ContinuationAuthority claimed : Bool /-- Every target mutation with whether a flight on that target was active at that moment. -/ mutationLog : List (String × Bool) @@ -118,18 +200,21 @@ structure ProtocolState where def ProtocolState.initial : ProtocolState := { stage := .intake, goal := none, mode := none, capabilityChecked := [], flights := [], - context := [], passBudget := none, gate := .inapplicable, terminationExit := none, + context := [], passBudget := none, batch := none, + continuationAuthority := ⟨⟨[], .silent⟩, 0⟩, + terminationExit := none, terminationAuthority := none, claimed := false, mutationLog := [] } /-- Every caller-side act the contract speaks about. `hostNotified` is an environment event. -/ inductive Action | inspectReadOnly - | writeGoal (g : GoalArtifact) - | appendRevision (r : Revision) + | writeGoal (g : GoalArtifact) (e : IntakeEvidence) + | appendRevision (r : Revision) (e : RevisionEvidence) | capabilityCheck (c : Carrier) | resolveMode (m : WorkerMode) | openFlight (stage : FlightStage) (role : Role) (carrier : Carrier) (target : String) (retryBudget : Nat) | launchViaRunner (flight : Nat) + | launchDelegated (flight : Nat) | launchViaShellBackground (flight : Nat) | pollArtifacts (flight : Nat) | hostNotified (flight : Nat) @@ -138,10 +223,11 @@ inductive Action | mutateTarget (target : String) | carry (item : ContextItem) | recordPassBudget (units : Nat) - | pass (t : Transition) + | beginImplementation (plan : ImplementationPlan) + | recordImplementation (flight : Nat) (completed : List String) (checksPassed : Bool) + | pass (t : Transition) (e : Reasoning.FamilyEvidence) (plan : Option ImplementationPlan) | advanceStage - | declareGate (a : Applicability) - | evaluateTermination (source : ClaimSource) (roster : Roster) + | evaluateTermination (source : ClaimSource) (evidence : TerminationEvidence) | claimSatisfied | lifecycle (op : LifecycleOp) | oracleReference (url : String) (isPublic : Bool) (pinned : Bool) @@ -154,6 +240,17 @@ def ProtocolState.goalWritten (s : ProtocolState) : Prop := s.goal.isSome = true def ProtocolState.modeResolved (s : ProtocolState) : Prop := s.mode.isSome = true def ProtocolState.abstained (s : ProtocolState) : Prop := s.mode = some .abstain +/-- Both intake and authorized corrections feed the same claim-routing projection. -/ +def ProtocolState.gate (s : ProtocolState) : Applicability := + applicability s.continuationAuthority.source.entry + +/-- The revision ledger supplies the position; evidence cannot choose or reuse it. -/ +def ProtocolState.correctedAuthority (s : ProtocolState) (e : RevisionEvidence) : + ContinuationAuthority := + match e.continuation with + | none => s.continuationAuthority + | some source => ⟨source, (s.goal.map (·.revisions.length)).getD 0 + 1⟩ + def ProtocolState.activeOn (s : ProtocolState) (target : String) : Bool := s.flights.any fun f => f.target == target && f.active @@ -163,7 +260,9 @@ def ProtocolState.flight (s : ProtocolState) (id : Nat) : Option FlightRec := def ProtocolState.freshId (s : ProtocolState) : Nat := s.flights.length -/-- `harness` is complete when every sub-item is non-empty. -/ +/-- `harness` is complete when every sub-item is non-empty; intake may fill routine gaps from +the task, repository rules, existing authorizations, and execution context, recording assumptions +without asking a startup boundary question. -/ def Harness.complete (h : Harness) : Prop := h.providedCapabilities ≠ [] ∧ h.trustBoundary ≠ "" ∧ h.decisionOwnership ≠ "" @@ -174,17 +273,70 @@ def FlightStage.protocolStage : FlightStage → Stage | .review => .reviewTriplet | .termination => .fixOrDone +/-- Flights belonging to this candidate, including eligible carrier fallback attempts. -/ +def ProtocolState.batchFlights (s : ProtocolState) : List FlightRec := + match s.batch with + | none => [] + | some b => s.flights.filter fun f => b.firstFlight ≤ f.id + +/-- A failed carrier may be absorbed by a later terminal replacement of the same assignment. +The scope evidence still has to cover the obligations; a bare failure supplies none. -/ +def ProtocolState.batchSettled (s : ProtocolState) : Bool := + (s.batchFlights.filter (fun f => f.stage == .implementation)).all fun f => f.status == .terminal || + (f.status == .abstained && s.batchFlights.any fun g => + f.id < g.id && f.assignment == g.assignment && + g.status == .terminal) + +-- SKILL[guard]: "Admit the initial review triplet once all approved work and checks have worker evidence, with no active or unrecovered failed flight." +/-- The sole candidate-readiness projection, shared by stage advance and review dispatch. +It is independent of the remaining pass budget: a repair has already paid for its review. -/ +def ProtocolState.reviewReady (s : ProtocolState) : Bool := + s.batch.any fun b => b.remaining.isEmpty && b.checksPassed && s.batchSettled + +def ProtocolState.reviewStarted (s : ProtocolState) : Bool := + s.batchFlights.any fun f => f.stage == .review + +def reviewRoles : List Role := [.architecture, .quality, .tests] + +def ProtocolState.reviewComplete (s : ProtocolState) : Bool := + s.reviewReady && reviewRoles.all fun role => + s.batchFlights.any fun f => f.stage == .review && f.role == role && f.status == .terminal + +-- SKILL[guard]: "Pending work or checks stay in implementation within the allowance; exhaustion or failure reports unresolved work." +def guardImplementationFlight (s : ProtocolState) : Prop := + (s.stage = .implementation ∨ s.stage = .fixOrDone) ∧ + s.reviewStarted = false ∧ s.reviewReady = false ∧ s.batchSettled = true ∧ + ∃ b, s.batch = some b ∧ 0 < b.flightsLeft + +/-- Shared per-seat constraint for the recorded draw, dispatch, and fallback. -/ +def seatEligible : Role → Carrier → Bool + | .tests, c => canRunRepositoryCommands c + | _, _ => true + +/-- One normal triplet per candidate; another review needs an explicit counted pass. -/ +def guardReviewFlight (s : ProtocolState) (role : Role) (carrier : Carrier) : Prop := + (s.stage = .reviewTriplet ∨ s.stage = .fixOrDone) ∧ s.reviewReady = true ∧ + role ∈ reviewRoles ∧ + (s.batchFlights.any fun f => f.stage == .review && f.role == role) = false ∧ + seatEligible role carrier = true + /-! ## Guards, one per clause -/ -- SKILL[guard]: "During `intake`, the caller may use its own read-only tools to inspect the user's input and write `GoalArtifact`; this caller-owned read-only intake is not worker dispatch." def guardInspect (s : ProtocolState) : Prop := s.stage = .intake +-- SKILL[guard]: "During `intake`, the caller resolves these sub-items from the user's current input, repository rules, existing authorizations, and available execution context; it records those sources and labels any minimal engineering assumptions explicitly." +-- SKILL[guard]: "It must not ask a startup boundary or harness confirmation question." +-- 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." -def guardWriteGoal (s : ProtocolState) (g : GoalArtifact) : Prop := - s.stage = .intake ∧ s.goal = none ∧ s.mode = none ∧ s.flights = [] ∧ Harness.complete g.harness +def guardWriteGoal (s : ProtocolState) (g : GoalArtifact) (e : IntakeEvidence) : Prop := + s.stage = .intake ∧ s.goal = none ∧ s.mode = none ∧ s.flights = [] ∧ + Harness.complete g.harness ∧ e.recordedHarness = g.harness ∧ e.complete -- SKILL[guard]: "Any explicit correction to `GoalArtifact` or `harness` must append one such revision item before routing continues." -def guardAppendRevision (s : ProtocolState) : Prop := s.goalWritten +def guardAppendRevision (s : ProtocolState) (r : Revision) (e : RevisionEvidence) : Prop := + s.goalWritten ∧ e.valid r -- SKILL[guard]: "Its capability check may confirm that a Codex CLI worker can be invoked, but it is non-mutating: everywhere in this contract, non-mutating means it changes no file, Git state, GitHub state, label, release, host configuration, lifecycle state, or other external resource." def guardCapabilityCheck (s : ProtocolState) : Prop := @@ -197,14 +349,22 @@ def guardResolveMode (s : ProtocolState) (m : WorkerMode) : Prop := (m = .abstain ∨ ∃ c, m = .carrier c ∧ c ∈ s.capabilityChecked) -- SKILL[guard]: "`WorkerModeGate` requires resolution before dispatch." -def guardOpenFlight (s : ProtocolState) (stage : FlightStage) (carrier : Carrier) : Prop := - s.modeResolved ∧ ¬ s.abstained ∧ s.stage = stage.protocolStage ∧ - carrier ∈ s.capabilityChecked +def guardOpenFlight (s : ProtocolState) (stage : FlightStage) (role : Role) (carrier : Carrier) : Prop := + s.modeResolved ∧ ¬ s.abstained ∧ carrier ∈ s.capabilityChecked ∧ + match stage with + | .implementation => role = .implementation ∧ guardImplementationFlight s + | .review => guardReviewFlight s role carrier + | _ => s.stage = stage.protocolStage -- SKILL[guard]: "Every formal `codex-cli` flight must use this runner rather than a parallel direct-launch path." def guardLaunchViaRunner (s : ProtocolState) (id : Nat) : Prop := ∃ f, s.flight id = some f ∧ f.launched = false ∧ f.carrier = .codexCli +/-- Existing direct oracle/subagent invocation, outside the Codex runner. This models +host dispatch only; carrier-specific isolation remains at its existing contract owner. -/ +def guardLaunchDelegated (s : ProtocolState) (id : Nat) : Prop := + ∃ f, s.flight id = some f ∧ f.launched = false ∧ f.carrier ≠ .codexCli + -- SKILL[guard]: "It must not use shell `&` to background the runner, because that detaches the process from host tracking and can leave an init-adopted carrier running without ever notifying the caller of completion." def guardNoShellBackground : Prop := False @@ -219,10 +379,25 @@ def guardHostNotified (s : ProtocolState) (id : Nat) : Prop := def guardCollect (s : ProtocolState) (id : Nat) : Prop := ∃ f, s.flight id = some f ∧ f.notified = true ∧ f.active = true +/-- Tried carriers come from all attempts of this assignment, including replacements. -/ +def ProtocolState.triedCarriers (s : ProtocolState) (assignment : Nat) : CarrierSet := + let tried := fun c => s.flights.any fun f => f.assignment == assignment && f.carrier == c + ⟨tried .codexCli, tried .nyxidOracle, tried .isolatedTokenSubagent⟩ + +/-- 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 && + (f.stage != .review || seatEligible f.role c) + ⟨eligible .codexCli, eligible .nyxidOracle, eligible .isolatedTokenSubagent⟩ + -- SKILL[guard]: "If any flight lacks terminal completion after its finite same-carrier retry budget is exhausted, the caller marks that flight `abstained` with empty `result_envelope_ref` and `completion_sentinel_ref`." +/-- 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 ∧ carrier ≠ f.carrier ∧ - carrier ∈ s.capabilityChecked + ∃ f, s.flight id = some f ∧ f.status = .abstained ∧ + (s.flights.filter fun g => g.assignment == f.assignment).all + (fun g => g.status == .abstained) = true ∧ + nextCarrier (s.eligibleCarriers f) (s.triedCarriers f.assignment) = some carrier -- SKILL[guard]: "While any `SshxWorkerFlightRecord` for the same `work_target` is `in-flight` or `retrying`, the caller is read-only for that target." def guardMutateTarget (s : ProtocolState) (target : String) : Prop := @@ -236,24 +411,42 @@ def guardRecordPassBudget (s : ProtocolState) : Prop := s.stage = .fixOrDone ∧ s.passBudget = none -- SKILL[guard]: "The budget is immutable for this run: no result, repair, or correction may add, replenish, reset, or replace units, and a unit is never refunded." -def guardPass (s : ProtocolState) (t : Transition) : Prop := - s.stage = .fixOrDone ∧ (t.counted = true → ∃ b, s.passBudget = some b ∧ 0 < b) +-- SKILL[guard]: "Worker conclusions accumulate completed and remaining obligations and test evidence; terminal flight completion permits handoff only." +def guardRecordImplementation (s : ProtocolState) (id : Nat) : Prop := + s.reviewStarted = false ∧ s.batch.isSome = true ∧ + ∃ f ∈ s.batchFlights, f.id = id ∧ f.stage = .implementation ∧ f.status = .terminal ∧ + (∀ g ∈ s.batchFlights, g.stage = .implementation → g.id ≤ id) + +def guardBeginImplementation (s : ProtocolState) (plan : ImplementationPlan) : Prop := + s.stage = .implementation ∧ s.batch = none ∧ plan.valid + +-- SKILL[guard]: "The batch debit includes all bounded assignments and final review even at zero remaining units, with no subsequent pass authority." +-- SKILL[guard]: "If review exits `fix`, freeze admitted fixes as one finite batch using `## Implementation Worker` decomposition, 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 → ∃ b, s.passBudget = some b ∧ 0 < b) ∧ + (if t = .repairWithRerunReview then ∃ p, plan = some p ∧ p.valid else plan = none) def guardAdvanceStage (s : ProtocolState) : Prop := - s.stage.next.isSome = true ∧ s.modeResolved ∧ ¬ s.abstained ∧ - s.flights.all (fun f => !f.active) = true - --- 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 whether one exists." -def guardDeclareGate (s : ProtocolState) : Prop := s.goalWritten + 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.stage = .implementation → s.reviewReady = true) ∧ + (s.stage = .reviewTriplet → s.reviewComplete = true) -- SKILL[guard]: "`## Termination Gate` is a conditional subgate reached inside `fix_or_done`, never an additional `InlineConsensusProtocol` stage." -def guardEvaluateTermination (s : ProtocolState) : Prop := - s.stage = .fixOrDone ∧ s.gate = .applies ∧ ∃ b, s.passBudget = some b ∧ 0 < b +def guardEvaluateTermination (s : ProtocolState) (e : TerminationEvidence) : Prop := + e.authority = s.continuationAuthority ∧ + s.stage = .fixOrDone ∧ s.reviewComplete = true ∧ s.gate = .applies ∧ + ∃ b, s.passBudget = some b ∧ 0 < b --- SKILL[guard]: "It applies only when `## Goal Contract` supplies its positive, boundary-owner-confirmed `harness.provided_capabilities` entry and the caller is about to assert that `GoalArtifact` is satisfied." +-- SKILL[guard]: "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." def guardClaimSatisfied (s : ProtocolState) : Prop := - s.stage = .fixOrDone ∧ s.gate ≠ .escalateToMaintainer ∧ - (s.gate = .applies → s.terminationExit = some .claimPermitted) + s.stage = .fixOrDone ∧ s.gate ≠ .withholdClaim ∧ + (s.gate = .applies → s.terminationExit = some .claimPermitted ∧ + s.terminationAuthority = some s.continuationAuthority) ∧ s.reviewComplete = true -- SKILL[guard]: "`sshx` does not grant permission to commit, push, merge, close issues, edit labels, publish releases, or mutate external lifecycle state." def guardNoLifecycle : Prop := False @@ -266,12 +459,13 @@ def guardNoPublishToLink : Prop := False /-- The conjunction of the clause guards, per action. -/ def allowed (s : ProtocolState) : Action → Prop | .inspectReadOnly => guardInspect s - | .writeGoal g => guardWriteGoal s g - | .appendRevision _ => guardAppendRevision s + | .writeGoal g e => guardWriteGoal s g e + | .appendRevision r e => guardAppendRevision s r e | .capabilityCheck _ => guardCapabilityCheck s | .resolveMode m => guardResolveMode s m - | .openFlight stage _ carrier _ _ => guardOpenFlight s stage carrier + | .openFlight stage role carrier _ _ => guardOpenFlight s stage role carrier | .launchViaRunner id => guardLaunchViaRunner s id + | .launchDelegated id => guardLaunchDelegated s id | .launchViaShellBackground _ => guardNoShellBackground | .pollArtifacts _ => guardNoPolling | .hostNotified id => guardHostNotified s id @@ -280,15 +474,22 @@ def allowed (s : ProtocolState) : Action → Prop | .mutateTarget target => guardMutateTarget s target | .carry item => guardCarry item | .recordPassBudget _ => guardRecordPassBudget s - | .pass t => guardPass s t + | .beginImplementation p => guardBeginImplementation s p + | .recordImplementation id _ _ => guardRecordImplementation s id + | .pass t e p => guardPass s t e p | .advanceStage => guardAdvanceStage s - | .declareGate _ => guardDeclareGate s - | .evaluateTermination _ _ => guardEvaluateTermination s + | .evaluateTermination _ e => guardEvaluateTermination s e | .claimSatisfied => guardClaimSatisfied s | .lifecycle _ => guardNoLifecycle | .oracleReference _ isPublic pinned => guardOracleReference isPublic pinned | .publishToMakeLinkable => guardNoPublishToLink +-- SKILL[ref]: "Include any non-blocking advisory feedback without inlining logs." +abbrev advisoryWithoutLogs := @ContextItem.permitted + +-- SKILL[policy]: "Protocol policy, not a mathematical consequence: before the first pass after the initial review triplet, the caller records one owner-precommitted finite integer `pass_budget`." +abbrev passBudgetPrecommitment := @guardRecordPassBudget + /-! ## Effects -/ def updateFlight (s : ProtocolState) (id : Nat) (f : FlightRec → FlightRec) : ProtocolState := @@ -308,6 +509,7 @@ def collectEffect (o : Observation) (f : FlightRec) : FlightRec := def newFlight (id : Nat) (stage : FlightStage) (role : Role) (carrier : Carrier) (target : String) (retryBudget : Nat) : FlightRec where id := id + assignment := id stage := stage role := role carrier := carrier @@ -327,13 +529,24 @@ def reopenFlight (id : Nat) (carrier : Carrier) (f : FlightRec) : FlightRec := def step (s : ProtocolState) : Action → ProtocolState | .inspectReadOnly => s - | .writeGoal g => { s with goal := some g } - | .appendRevision r => { s with goal := s.goal.map fun g => g.correct r } + | .writeGoal g e => + { s with + goal := some g, + continuationAuthority := ⟨⟨e.recordedHarness.providedCapabilities, e.continuation⟩, + g.revisions.length⟩ } + | .appendRevision r e => + { s with + goal := s.goal.map (fun g => g.correct r), + continuationAuthority := s.correctedAuthority e } | .capabilityCheck c => { s with capabilityChecked := c :: s.capabilityChecked } | .resolveMode m => { s with mode := some m } | .openFlight stage role carrier target retryBudget => - { s with flights := s.flights ++ [newFlight s.freshId stage role carrier target retryBudget] } - | .launchViaRunner id => updateFlight s id fun f => { f with launched := true } + { s with + flights := s.flights ++ [newFlight s.freshId stage role carrier target retryBudget], + batch := s.batch.map fun b => if stage = .implementation then + { b with flightsLeft := b.flightsLeft - 1, checksPassed := false } else b } + | .launchViaRunner id | .launchDelegated id => + updateFlight s id fun f => { f with launched := true } | .launchViaShellBackground _ => s | .pollArtifacts _ => s | .hostNotified id => updateFlight s id fun f => { f with notified := true } @@ -346,12 +559,20 @@ def step (s : ProtocolState) : Action → ProtocolState | .mutateTarget target => { s with mutationLog := (target, s.activeOn target) :: s.mutationLog } | .carry item => { s with context := item :: s.context } | .recordPassBudget units => { s with passBudget := some units } - | .pass t => - { s with passBudget := s.passBudget.bind fun b => Sshx.step b t } + | .beginImplementation p => { s with batch := some (p.start s.freshId) } + | .recordImplementation _ completed checksPassed => + { s with batch := s.batch.map fun b => + { b with remaining := b.remaining.filter (fun x => !completed.contains x), checksPassed := checksPassed } } + | .pass t _ plan => + { s with + passBudget := s.passBudget.bind fun b => Sshx.step b t, + batch := if t = .repairWithRerunReview then plan.map (·.start s.freshId) + else if t = .repeatedReviewPass then s.batch.map fun b => { b with firstFlight := s.freshId } + else s.batch } | .advanceStage => { s with stage := s.stage.next.getD s.stage } - | .declareGate a => { s with gate := a } - | .evaluateTermination source roster => - { s with terminationExit := some (terminationRoute source roster), + | .evaluateTermination source e => + { s with terminationExit := some (terminationRoute source e.roster), + terminationAuthority := some e.authority, passBudget := s.passBudget.bind fun b => Sshx.step b .terminationGateEvaluation } | .claimSatisfied => { s with claimed := true } | .lifecycle _ => s diff --git a/skills/sshx/formal/Sshx/Behavior/Scenarios.lean b/skills/sshx/formal/Sshx/Behavior/Scenarios.lean new file mode 100644 index 00000000..e4888fa7 --- /dev/null +++ b/skills/sshx/formal/Sshx/Behavior/Scenarios.lean @@ -0,0 +1,646 @@ +import Sshx.Behavior.Invariant +import Sshx.Reasoning.Authority + +/-! +Observable route regressions. These compose the production `step`, `allowed`, downgrade +and review table; there is no parallel test decision model. Worker evidence is an input, +not a proof of English semantics. Baselines are recorded in test_sshx_contract.py. +`admitted` below checks every guard of the composed traces; `run` applies their effects. +Approved-plan fixtures supply the prior thinking settlement as an input. +-/ +namespace Sshx.Behavior.Scenarios +open Sshx Sshx.Reasoning + +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⟩ + +private def readyState : ProtocolState := + { ProtocolState.initial with + stage := .implementation, goal := some goal, mode := some (.carrier .codexCli), + capabilityChecked := [.codexCli, .isolatedTokenSubagent] } + +private def twoParts : ImplementationPlan := ⟨["contract", "verification"], 2⟩ +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⟩ +private def finish (s : ProtocolState) (id : Nat) (o : Observation) : ProtocolState := + step (step (step s (.launchViaRunner id)) (.hostNotified id)) (.collect id o) +private def returned := finish opened 0 successful +private def partDone := step returned (.recordImplementation 0 ["contract"] true) +private def second := step partDone (.openFlight .implementation .implementation .codexCli "target" 0) +private def complete := step (finish second 1 successful) + (.recordImplementation 1 ["verification"] true) + +-- The first worker is terminal and its tests passed; remaining scope still blocks review. +example : (partDone.flight 0).map (·.status) = some .terminal := by decide +example : partDone.reviewReady = false := by decide +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] + +-- 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, + 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, + newFlight, ProtocolState.freshId] +example : complete.reviewReady = true := by decide +example : complete.reviewStarted = false := by decide +private def review := step complete .advanceStage +example : review.stage = .reviewTriplet := by decide +example : allowed complete .advanceStage := by + simp [allowed, guardAdvanceStage, complete, second, 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, Stage.next, ProtocolState.modeResolved, ProtocolState.abstained] + +-- Triplet seats can all dispatch independently; a second flight for the same seat cannot. +private def architecture := step review (.openFlight .review .architecture .codexCli "target" 0) +private def quality := step architecture (.openFlight .review .quality .codexCli "target" 0) +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, + ProtocolState.abstained] + decide +example : allowed quality (.openFlight .review .tests .codexCli "target" 0) := by + simp only [allowed, guardOpenFlight, guardReviewFlight, seatEligible, canRunRepositoryCommands, ProtocolState.modeResolved, + ProtocolState.abstained] + decide +example : (tests.batchFlights.filter (fun f => f.stage == .review)).length = 3 := by decide +example : ¬ guardReviewFlight tests .architecture .codexCli := by + have : (tests.batchFlights.any fun f => f.stage == .review && f.role == .architecture) = true := by decide + simp [guardReviewFlight, this] +private def reviewed := finish (finish (finish tests 2 successful) 3 successful) 4 successful +example : reviewed.reviewComplete = true := by decide +private def fix := step reviewed .advanceStage +example : fix.stage = .fixOrDone := by decide + +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⟩ +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 + 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] +example : repair.passBudget = some 0 := by decide +example : repair.stage = .fixOrDone := by decide +private def repairedFirst := step (finish (step repair + (.openFlight .implementation .implementation .codexCli "target" 0)) 5 successful) + (.recordImplementation 5 ["contract"] true) +example : repairedFirst.reviewReady = false := by decide +private def repaired := step (finish (step repairedFirst + (.openFlight .implementation .implementation .codexCli "target" 0)) 6 successful) + (.recordImplementation 6 ["verification"] true) +example : repaired.reviewReady = true := by decide +example : repaired.passBudget = some 0 := by decide +-- The last paid unit includes this final review, with no new unit or pass needed. +example : guardReviewFlight repaired .architecture .codexCli := by + have hs : repaired.stage = .fixOrDone := by decide + have hr : repaired.reviewReady = true := by decide + have hn : (repaired.batchFlights.any fun f => f.stage == .review && f.role == .architecture) = false := by decide + simp [guardReviewFlight, hs, hr, hn, reviewRoles, seatEligible] +example : ¬ allowed repaired (.pass .repairWithRerunReview family (some twoParts)) := by + have hb : repaired.passBudget = some 0 := by decide + simp [allowed, guardPass, Transition.counted, hb] + +private def repairReviews := step (step (step repaired + (.openFlight .review .architecture .codexCli "target" 0)) + (.openFlight .review .quality .codexCli "target" 0)) + (.openFlight .review .tests .codexCli "target" 0) +private def repairReviewed := finish (finish (finish repairReviews 7 successful) 8 successful) 9 successful +-- Kernel reduction traverses both full batches and their flight handshakes. +set_option maxRecDepth 4096 in +example : repairReviewed.reviewComplete = true := by decide +example : repairReviewed.passBudget = some 0 := by decide +example : ¬ allowed repairReviewed (.pass .repairWithRerunReview family (some twoParts)) := by + have hb : repairReviewed.passBudget = some 0 := by decide + simp [allowed, guardPass, Transition.counted, hb] +example : ¬ allowed repairReviewed (.pass .repeatedReviewPass family none) := by + have hb : repairReviewed.passBudget = some 0 := by decide + simp [allowed, guardPass, Transition.counted, hb] +-- A separately funded repeated review remains available and resets only the review window. +private def repeated := step funded (.pass .repeatedReviewPass family none) +example : allowed funded (.pass .repeatedReviewPass family 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, family, familyPassAllowed, familyRoute, + ownerAuthorizedDomainChange, classGateActive, FamilyEvidence.recordComplete, + coverageBasisVerified, Transition.counted] +example : repeated.reviewReady = true := by decide +example : repeated.reviewComplete = false := by decide +example : ¬ guardImplementationFlight repeated := by + have hr : repeated.reviewReady = true := by decide + simp [guardImplementationFlight, hr] +example : ¬ allowed funded (.pass .repairWithRerunReview + { family with coverageBasis := .unsupportedMemberEnumeration } (some twoParts)) := by + simp [allowed, guardPass, familyPassAllowed, familyRoute, family, + classGateActive, ownerAuthorizedDomainChange, coverageBasisVerified] + +-- Active, terminal-with-failed-checks, and exhausted incomplete assignments never admit review. +example : opened.reviewReady = false := by decide +private def unchecked := step (finish second 1 successful) + (.recordImplementation 1 ["verification"] false) +example : unchecked.reviewReady = false := by decide +private def failed := finish second 1 { successful with exitZero := false } +example : failed.batchSettled = false := by decide +example : failed.reviewReady = false := by decide +private def exhausted := step (finish second 1 successful) + (.recordImplementation 1 [] true) +example : exhausted.reviewReady = false := by decide +example : ¬ guardImplementationFlight exhausted := by + have hb : exhausted.batch = some ⟨["verification"], true, 0, 0⟩ := by decide + 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⟩)) + (.openFlight .implementation .implementation .codexCli "target" 0)) 0 successful) + (.recordImplementation 0 ["all work"] true) +example : single.reviewReady = true := by decide + +/-- A trace checks each production guard at the state produced by its preceding actions. -/ +private def admitted (s : ProtocolState) : List Action → Prop + | [] => True + | a :: rest => allowed s a ∧ admitted (step s a) rest + +private def run (s : ProtocolState) (actions : List Action) : ProtocolState := + actions.foldl step s + +private def implementationActions (firstId : Nat) : List Action := + [.openFlight .implementation .implementation .codexCli "target" 0, + .launchViaRunner firstId, .hostNotified firstId, .collect firstId successful, + .recordImplementation firstId ["contract"] true, + .openFlight .implementation .implementation .codexCli "target" 0, + .launchViaRunner (firstId + 1), .hostNotified (firstId + 1), .collect (firstId + 1) successful, + .recordImplementation (firstId + 1) ["verification"] true] +private def reviewActions (firstId : Nat) : List Action := + [.openFlight .review .architecture .codexCli "target" 0, + .openFlight .review .quality .codexCli "target" 0, + .openFlight .review .tests .codexCli "target" 0, + .launchViaRunner firstId, .hostNotified firstId, .collect firstId successful, + .launchViaRunner (firstId + 1), .hostNotified (firstId + 1), .collect (firstId + 1) successful, + .launchViaRunner (firstId + 2), .hostNotified (firstId + 2), .collect (firstId + 2) successful] + +-- The earlier effect projections also have complete guard admission, including handshakes. +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, + guardLaunchViaRunner, guardHostNotified, guardCollect, guardRecordImplementation, + begin, readyState, 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] +example : run begin (implementationActions 0) = complete := rfl +example : admitted review (reviewActions 2) := by + simp [admitted, reviewActions, allowed, guardOpenFlight, 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 + simp only [allowed, guardAdvanceStage, ProtocolState.goalWritten, ProtocolState.modeResolved, + ProtocolState.abstained] + decide +example : 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, + 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 +set_option maxRecDepth 4096 in +example : admitted repaired (reviewActions 7) := by + simp [admitted, reviewActions, allowed, guardOpenFlight, 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 + +private def recoveryActions (observation : Observation) : List Action := + [.beginImplementation ⟨["all work"], 1⟩, + .openFlight .implementation .implementation .codexCli "target" 0, + .launchViaRunner 0, .hostNotified 0, .collect 0 { successful with exitZero := false }, + .fallbackFlight 0 .isolatedTokenSubagent, + .launchDelegated 1, .hostNotified 1, .collect 1 observation] + +-- Both success and exhaustion traverse launch, notification and collection on each carrier. +private theorem recovery_admitted (observation : Observation) : + admitted readyState (recoveryActions observation) := by + simp [admitted, recoveryActions, allowed, guardBeginImplementation, ImplementationPlan.valid, + guardOpenFlight, guardImplementationFlight, guardLaunchViaRunner, guardLaunchDelegated, + 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, + Carrier.univ, CarrierSet.get] + +private def recoveryReturned := run readyState (recoveryActions successful) +example : allowed recoveryReturned (.recordImplementation 1 ["all work"] true) := by + simp [allowed, guardRecordImplementation, recoveryReturned, run, recoveryActions, + readyState, ProtocolState.initial, step, ProtocolState.reviewStarted, + ProtocolState.batchFlights, ProtocolState.flight, ProtocolState.freshId, + newFlight, reopenFlight, ImplementationPlan.start, updateFlight, collectEffect, done, successful] +private def recovered := step recoveryReturned (.recordImplementation 1 ["all work"] true) +example : recovered.reviewReady = true := by decide +example : allowed recovered .advanceStage := by + simp only [allowed, guardAdvanceStage, ProtocolState.goalWritten, ProtocolState.modeResolved, ProtocolState.abstained] + decide +example : recovered.passBudget = none := by decide + +private def carrierExhausted := run readyState + (recoveryActions { successful with exitZero := false }) +example : carrierExhausted.reviewReady = false := by decide +example : carrierExhausted.batchSettled = false := by decide +-- Reusing either failure id cannot duplicate or cycle a carrier; the actual selector abstains. +example (id : Nat) (c : Carrier) : ¬ allowed carrierExhausted (.fallbackFlight id c) := by + intro ha + obtain ⟨f, hf, _, _, hn⟩ := ha + simp [carrierExhausted, run, recoveryActions, readyState, ProtocolState.initial, step, + ProtocolState.flight, ProtocolState.freshId, newFlight, reopenFlight, updateFlight, + collectEffect, done, successful] at hf + rcases hf with ⟨_, rfl⟩ | ⟨_, _, rfl⟩ <;> + simp [ProtocolState.eligibleCarriers, 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 +example : resolveSeat (carrierExhausted.eligibleCarriers (newFlight 0 .implementation + .implementation .codexCli "target" 0)) (carrierExhausted.triedCarriers 0) = .abstain := by decide +example : ¬ allowed carrierExhausted .advanceStage := by + have h : carrierExhausted.reviewReady = false := by decide + have hs : carrierExhausted.stage = .implementation := by decide + simp [allowed, guardAdvanceStage, h, hs] + +-- A distinct approved assignment on the same target retains its own carrier history. +example : (second.flight 0).map (·.assignment) = some 0 := by decide +example : (second.flight 1).map (·.assignment) = some 1 := by decide +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, + newFlight, nextCarrier, Carrier.univ, CarrierSet.get] + +-- Test-seat restriction applies to initial, repeated, and included repair review alike. +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, + ProtocolState.abstained] + decide +example : ¬ allowed repeated (.openFlight .review .tests .nyxidOracle "target" 0) := + tests_dispatch_excludes_oracle _ _ _ +example : ¬ allowed repaired (.openFlight .review .tests .nyxidOracle "target" 0) := + tests_dispatch_excludes_oracle _ _ _ + +private def fallbackOpened := run readyState ((recoveryActions successful).take 6) +-- Direct collection cannot stand in for the carrier's launch and completion notification. +example : ¬ allowed fallbackOpened (.collect 1 successful) := by + simp [allowed, guardCollect, fallbackOpened, run, recoveryActions, readyState, + ProtocolState.initial, step, ProtocolState.flight, ProtocolState.freshId, + newFlight, reopenFlight, updateFlight, collectEffect, done, successful] +example : ¬ allowed fallbackOpened (.launchViaRunner 1) := by + simp [allowed, guardLaunchViaRunner, fallbackOpened, run, recoveryActions, readyState, + ProtocolState.initial, step, ProtocolState.flight, ProtocolState.freshId, + newFlight, reopenFlight, updateFlight, collectEffect, done, successful] +example : ¬ allowed fallbackOpened (.fallbackFlight 0 .isolatedTokenSubagent) := by + simp [allowed, guardFallback, fallbackOpened, run, recoveryActions, readyState, + ProtocolState.initial, step, ProtocolState.flight, ProtocolState.freshId, + newFlight, reopenFlight, updateFlight, collectEffect, done, successful] +example : ¬ allowed recoveryReturned (.fallbackFlight 0 .isolatedTokenSubagent) := by + simp [allowed, guardFallback, recoveryReturned, run, recoveryActions, readyState, + ProtocolState.initial, step, ProtocolState.flight, ProtocolState.freshId, + newFlight, reopenFlight, updateFlight, collectEffect, done, successful] + +example : admitted readyState + [.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, + 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] + +private def testsReviewState := { review with capabilityChecked := Carrier.univ } +private def testsRecoveryActions (observation : Observation) : List Action := + [.openFlight .review .tests .codexCli "target" 0, + .launchViaRunner 2, .hostNotified 2, .collect 2 { successful with exitZero := false }, + .fallbackFlight 2 .isolatedTokenSubagent, + .launchDelegated 3, .hostNotified 3, .collect 3 observation] +-- Oracle is capability-checked and higher priority than the subagent, but ineligible here. +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, + 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, + CarrierSet.get, reviewRoles, Stage.next] +private def testsRecovered := run testsReviewState (testsRecoveryActions successful) +example : (testsRecovered.flight 3).map (·.status) = some .terminal := by decide +example : (testsRecovered.flight 3).map (·.carrier) = some .isolatedTokenSubagent := by decide +example : testsRecovered.reviewComplete = false := by decide + +private def testsExhausted := run testsReviewState + (testsRecoveryActions { successful with exitZero := false }) +example : resolveSeat (testsExhausted.eligibleCarriers + (newFlight 2 .review .tests .codexCli "target" 0)) + (testsExhausted.triedCarriers 2) = .abstain := by decide +example : testsExhausted.reviewComplete = false := by decide +example : ¬ allowed testsExhausted .advanceStage := by + have hs : testsExhausted.stage = .reviewTriplet := by decide + have hr : testsExhausted.reviewComplete = false := by decide + simp [allowed, guardAdvanceStage, hs, hr] + +private def scopeNote : Revision := + ⟨"engineering scope note", "existing user authorization", "none"⟩ +private def authorizedRevision (r : Revision) (source : Option ContinuationSource) : RevisionEvidence := + ⟨r, true, true, source⟩ + +private def startupActions (c : ContinuationEntry) : List Action := + [.writeGoal goal (intake c), + .appendRevision scopeNote (authorizedRevision scopeNote none), + .advanceStage, .capabilityCheck .codexCli, .resolveMode (.carrier .codexCli), .advanceStage] +-- All authority states permit routine startup without a question, preserving revision support. +example (c : ContinuationEntry) : admitted ProtocolState.initial (startupActions c) := by + simp [admitted, startupActions, allowed, guardWriteGoal, guardAppendRevision, + guardAdvanceStage, guardCapabilityCheck, guardResolveMode, Harness.complete, + authorizedRevision, RevisionEvidence.valid, + IntakeEvidence.complete, 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 +example : (run ProtocolState.initial (startupActions .silent)).stage = .thinkingPanel := by decide +example : (run ProtocolState.initial (startupActions .ambiguous)).gate = .withholdClaim := by decide +example : (run ProtocolState.initial (startupActions .absent)).gate = .inapplicable := by decide +example : (run ProtocolState.initial (startupActions .unconfirmed)).gate = .withholdClaim := by decide +example : (run ProtocolState.initial (startupActions .present)).gate = .applies := by decide + +-- T-R1-CORRECTION: start after the composed, guarded implementation and review above. +-- The supplied evidence interprets an explicit owner correction; no English parsing or +-- caller-inferred continuation mechanism is claimed here. +private def continuationRevision : Revision := + ⟨"owner corrects harness.provided_capabilities to declare host continuation", + "explicit boundary-owner authorization", "earlier continuation projection"⟩ +private def continuationSource (entry : ContinuationEntry) : ContinuationSource := + ⟨["owner's corrected provided_capabilities"], entry⟩ +private def correctionEvidence (entry : ContinuationEntry) : RevisionEvidence := + authorizedRevision continuationRevision (some (continuationSource entry)) +private def correctionAction (entry : ContinuationEntry) : Action := + .appendRevision continuationRevision (correctionEvidence entry) +private def corrected (entry : ContinuationEntry) := step fix (correctionAction entry) + +-- All supplied source states follow the same update route, including withdrawal and +-- uncertainty; authority ownership/support, rather than a state-pair whitelist, guards it. +example (entry : ContinuationEntry) : allowed fix (correctionAction entry) := by + simp only [allowed, correctionAction, guardAppendRevision, ProtocolState.goalWritten, + RevisionEvidence.valid, correctionEvidence, authorizedRevision] + decide +example (entry : ContinuationEntry) : (corrected entry).gate = applicability entry := by + exact correction_projects_current_source fix continuationRevision + (correctionEvidence entry) (continuationSource entry) rfl +example : (corrected .present).goal = some (goal.correct continuationRevision) := by decide +example : (corrected .present).terminationExit = none := by decide +example : ¬ allowed (corrected .present) .claimSatisfied := by + simp only [allowed, guardClaimSatisfied] + decide +example : ¬ allowed (corrected .ambiguous) .claimSatisfied := by + simp only [allowed, guardClaimSatisfied] + decide +example : ¬ allowed (corrected .unconfirmed) .claimSatisfied := by + simp only [allowed, guardClaimSatisfied] + decide +example : allowed (corrected .absent) .claimSatisfied := by + simp only [allowed, guardClaimSatisfied] + decide +example : allowed (corrected .silent) .claimSatisfied := by + simp only [allowed, guardClaimSatisfied] + decide + +-- Nonempty revision text alone supplies neither ownership nor source support. +example (s : ProtocolState) : ¬ allowed s (.appendRevision continuationRevision + { correctionEvidence .present with ownerAuthorized := false }) := by + simp [allowed, guardAppendRevision, RevisionEvidence.valid] +example (s : ProtocolState) : ¬ allowed s (.appendRevision continuationRevision + { correctionEvidence .present with sourceSupported := false }) := by + simp [allowed, guardAppendRevision, RevisionEvidence.valid] +example (s : ProtocolState) : ¬ allowed s (.appendRevision scopeNote + (correctionEvidence .present)) := by + simp [allowed, guardAppendRevision, RevisionEvidence.valid, correctionEvidence, + authorizedRevision, continuationRevision, scopeNote] + +private def satisfiedRoster : Roster := ⟨true, .satisfied, .satisfied, .satisfied⟩ +-- These inputs represent separately obtained evidence for the named source revisions. +-- Equal seat verdicts do not establish freshness; their supplied authority association does. +private def evidenceA1 : TerminationEvidence := + ⟨⟨continuationSource .present, 1⟩, satisfiedRoster⟩ +private def evaluateA1 : Action := .evaluateTermination .terminationSeats evidenceA1 +private def correctionFunded := step (corrected .present) (.recordPassBudget 2) +private def settled := step correctionFunded evaluateA1 +-- Each action is guarded: evaluation consumes supplied evidence for the current source. +example : admitted fix [correctionAction .present, .recordPassBudget 2, evaluateA1, .claimSatisfied] := by + simp only [admitted, correctionAction, evaluateA1, allowed, guardAppendRevision, + RevisionEvidence.valid, guardRecordPassBudget, guardEvaluateTermination, + guardClaimSatisfied, ProtocolState.goalWritten] + decide +example : settled.terminationExit = some .claimPermitted := by decide +example : settled.terminationAuthority = some settled.continuationAuthority := by decide + +-- Even a correction that stays `present` changes the source generation. Keep the old +-- affirmative settlement, but refuse both direct claim and resubmission of the old roster. +private def sourceRevision : Revision := + ⟨"owner corrects the declared continuation's scope", "explicit boundary-owner authorization", + "termination evidence for the earlier continuation scope"⟩ +private def sourceCorrection : Action := + .appendRevision sourceRevision (authorizedRevision sourceRevision + (some ⟨["owner's corrected continuation scope"], .present⟩)) +private def superseded := step settled sourceCorrection +example : allowed settled sourceCorrection := by + simp only [sourceCorrection, allowed, guardAppendRevision, ProtocolState.goalWritten, + RevisionEvidence.valid, authorizedRevision] + decide +example : superseded.gate = settled.gate := by decide +example : superseded.continuationAuthority.revision = 2 := by decide +example : superseded.terminationExit = settled.terminationExit := by decide +example : superseded.terminationAuthority = settled.terminationAuthority := by decide +example : superseded.passBudget = settled.passBudget := by decide +example : superseded.goal = some ((goal.correct continuationRevision).correct sourceRevision) := by decide +example : ¬ allowed superseded .claimSatisfied := by + apply stale_authority_cannot_claim + · decide + · decide +-- A-F2-ROSTER-SOURCE: the exact A1 evidence cannot be rebound by reevaluation at A2. +example : ¬ allowed superseded evaluateA1 := by + apply stale_evidence_cannot_evaluate + decide +example : ¬ admitted superseded [evaluateA1, .claimSatisfied] := by + simp only [admitted, evaluateA1, allowed, guardEvaluateTermination, guardClaimSatisfied] + decide +-- Even an unguarded effect preserves A1 rather than manufacturing A2 provenance. +example : (step superseded evaluateA1).terminationAuthority = some evidenceA1.authority := rfl +example : ¬ allowed (step superseded evaluateA1) .claimSatisfied := by + apply stale_authority_cannot_claim + · decide + · decide + +private def evidenceA2 : TerminationEvidence := + ⟨⟨⟨["owner's corrected continuation scope"], .present⟩, 2⟩, satisfiedRoster⟩ +private def evaluateA2 : Action := .evaluateTermination .terminationSeats evidenceA2 +example : evidenceA1.roster = evidenceA2.roster := rfl +example : evidenceA1.authority ≠ evidenceA2.authority := by decide +-- Fresh A2 evidence with the same verdicts is admitted through the actual consumer. +example : admitted superseded [evaluateA2, .claimSatisfied] := by + simp only [admitted, evaluateA2, allowed, guardEvaluateTermination, guardClaimSatisfied] + decide +example : (step superseded evaluateA2).terminationAuthority = some evidenceA2.authority := rfl +example : (step superseded evaluateA2).passBudget = some 0 := by decide +example : (run superseded [evaluateA2, .claimSatisfied]).claimed = true := by decide + +-- A relevant repeated revision advances the ledger even with an identical source payload. +private def sourceRepeated := step settled (correctionAction .present) +private def repeatedEvidence : TerminationEvidence := + ⟨⟨continuationSource .present, 2⟩, satisfiedRoster⟩ +example : ¬ admitted sourceRepeated [evaluateA1, .claimSatisfied] := by + simp only [admitted, evaluateA1, allowed, guardEvaluateTermination, guardClaimSatisfied] + decide +example : admitted sourceRepeated [.evaluateTermination .terminationSeats repeatedEvidence, + .claimSatisfied] := by + simp only [admitted, allowed, guardEvaluateTermination, guardClaimSatisfied] + decide + +-- Changes away from positive authority update the actual consumer too; uncertainty +-- withholds, while an owner-supported withdrawal needs no continuation evidence. +example (entry : ContinuationEntry) : admitted settled [correctionAction entry] := by + simp only [admitted, correctionAction, allowed, guardAppendRevision, + ProtocolState.goalWritten, RevisionEvidence.valid, correctionEvidence, authorizedRevision] + decide +example : ¬ allowed (step settled (correctionAction .ambiguous)) .claimSatisfied := by + simp only [allowed, guardClaimSatisfied] + decide +example : allowed (step settled (correctionAction .absent)) .claimSatisfied := by + simp only [allowed, guardClaimSatisfied] + decide +-- Returning to an identical positive source cannot revive its earlier settlement or evidence. +example : admitted settled [correctionAction .absent, correctionAction .present] := by + simp only [admitted, correctionAction, allowed, guardAppendRevision, + ProtocolState.goalWritten, RevisionEvidence.valid, correctionEvidence, authorizedRevision] + decide +example : ¬ allowed (step (step settled (correctionAction .absent)) + (correctionAction .present)) .claimSatisfied := by + simp only [allowed, guardClaimSatisfied] + decide +private def restored := step (step settled (correctionAction .absent)) (correctionAction .present) +private def restoredEvidence : TerminationEvidence := + ⟨⟨continuationSource .present, 3⟩, satisfiedRoster⟩ +example : restored.continuationAuthority.source = evidenceA1.authority.source := by decide +example : ¬ admitted restored [evaluateA1, .claimSatisfied] := by + simp only [admitted, evaluateA1, allowed, guardEvaluateTermination, guardClaimSatisfied] + decide +example : admitted restored [.evaluateTermination .terminationSeats restoredEvidence, + .claimSatisfied] := by + simp only [admitted, allowed, guardEvaluateTermination, guardClaimSatisfied] + decide +-- A note unrelated to continuation leaves valid evidence usable at both consumers. +example : admitted settled [.appendRevision scopeNote (authorizedRevision scopeNote none), + .claimSatisfied] := by + simp only [admitted, allowed, guardAppendRevision, guardClaimSatisfied, + ProtocolState.goalWritten, RevisionEvidence.valid, authorizedRevision] + decide + +example : admitted settled [.appendRevision scopeNote (authorizedRevision scopeNote none), + evaluateA1, .claimSatisfied] := by + simp only [admitted, evaluateA1, allowed, guardAppendRevision, guardEvaluateTermination, + guardClaimSatisfied, ProtocolState.goalWritten, RevisionEvidence.valid, authorizedRevision] + 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 +example : routeFindings { ordinary with requiresTrustedMalice := true } approval approval = .doneWithAdvisory := by decide +example : routeFindings { invented with trigger := { invented.trigger with + recordedOccurrence := some "independent pre-run incident", createdDuringRun := false } } + approval approval = .fix := by decide +example : routeFindings { invented with trigger := { invented.trigger with + recordedOccurrence := some "fixture made during this run" } } approval approval = .doneWithAdvisory := by decide +-- Absorbed harms have no second conjunct; a goal-visible residue still blocks. +example : routeFindings { ordinary with input := shapeToInput .absorbedByRecoveryPath } + approval approval = .doneWithAdvisory := by decide +example : planElementAdmitted ⟨"defense", invented, false, true⟩ = false := by decide +example : planElementAdmitted ⟨"ordinary validation", ordinary, false, true⟩ = true := by decide +example : planElementAdmitted ⟨"integrity label", { ordinary with + input := shapeToInput .absorbedByRecoveryPath }, true, true⟩ = false := by decide + +example : familyPassAllowed { family with coverageBasis := .unsupportedMemberEnumeration } + .repairWithRerunReview = false := by decide +example : familyPassAllowed { family with coverageBasis := .soundAbstraction true } + .repairWithRerunReview = true := by decide +example : familyPassAllowed { family with changesDomainOrCriterion := true, ownerAuthorized := true } + .repairWithRerunReview = false := by decide +example : familyPassAllowed { family with + changesDomainOrCriterion := true, ownerAuthorized := true, + revision := some ⟨"scope", "owner authorization", "none"⟩ } .repairWithRerunReview = true := by decide +example : familyRoute { family with noSupportedPath := true } = .honestStop := by 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] +example : allowed ProtocolState.initial (.writeGoal goal (intake .ambiguous)) := by + simp [allowed, guardWriteGoal, IntakeEvidence.complete, Harness.complete, ProtocolState.initial, intake, goal] +example : ¬ allowed ProtocolState.initial (.writeGoal goal + { intake .silent with startupQuestionAsked := true }) := by + simp [allowed, guardWriteGoal, IntakeEvidence.complete] +example : ¬ allowed ProtocolState.initial (.writeGoal goal + { intake .silent with explicitBoundariesPreserved := false }) := by + simp [allowed, guardWriteGoal, IntakeEvidence.complete] +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 + +end Sshx.Behavior.Scenarios diff --git a/skills/sshx/formal/Sshx/Blocking.lean b/skills/sshx/formal/Sshx/Blocking.lean index 87a8f428..8b266ed7 100644 --- a/skills/sshx/formal/Sshx/Blocking.lean +++ b/skills/sshx/formal/Sshx/Blocking.lean @@ -26,6 +26,37 @@ inductive Force | advisory deriving DecidableEq, Repr +inductive TriggerPath + | ordinaryOperation + | nonstandardDeliberate + | malicious + deriving DecidableEq, Repr + +structure TriggerRecord where + trigger : String + triggerActor : String + triggerPath : TriggerPath + mechanismFamily : String + recordedOccurrence : Option String + createdDuringRun : Bool + deriving DecidableEq, Repr + +-- SKILL[def]: "A blocking finding must also pass the structured trigger check" +def occurrenceIsIndependent (recordedOccurrence : Option String) (createdDuringRun : Bool) : Bool := + recordedOccurrence.isSome && !createdDuringRun + +-- SKILL[def]: "`recorded_occurrence` must have existed before this run" +def triggerCheck (record : TriggerRecord) : Bool := + match record.triggerPath with + | .ordinaryOperation => true + | .nonstandardDeliberate | .malicious => + occurrenceIsIndependent record.recordedOccurrence record.createdDuringRun + +-- SKILL[thm]: "a fixture, reproduction, or state deliberately created by a seat, caller, or repair worker during this run is 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" /-- `BlockingAuthority`: advisory is the default; blocking needs both named conjuncts. -/ def force (i : Input) : Force := @@ -61,11 +92,12 @@ structure Finding where verdict : ReviewVerdict input : Input requiresTrustedMalice : Bool + trigger : TriggerRecord 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" /-- `ThreatEligibility`. -/ -def eligible (f : Finding) : Bool := !f.requiresTrustedMalice +def eligible (f : Finding) : Bool := !f.requiresTrustedMalice && triggerCheck f.trigger -- SKILL[def]: "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." /-- `## Review Truth Table`: a blocking finding that fails either check is an advisory. -/ @@ -80,17 +112,28 @@ 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 => - cases v <;> cases m <;> cases hf : force i <;> simp [downgrade, eligible, hf] + | mk v i m tr => + cases v <;> cases m <;> cases hf : force i <;> cases ht : triggerCheck tr <;> + simp [downgrade, eligible, hf, ht] theorem downgrade_approve_iff (f : Finding) : downgrade f = .approve ↔ f.verdict = .approve := by cases f with - | mk v i m => cases v <;> cases m <;> cases hf : force i <;> simp [downgrade, eligible, hf] + | mk v i m tr => cases v <;> cases m <;> cases hf : force i <;> cases ht : triggerCheck tr <;> + simp [downgrade, 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 => cases v <;> cases m <;> cases hf : force i <;> simp [downgrade, eligible, hf] + | mk v i m tr => cases v <;> cases m <;> cases hf : force i <;> cases ht : triggerCheck tr <;> + simp [downgrade, 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) : + downgrade f = .reject := by + rw [downgrade] + simp [hv, hi, eligible, hm, triggerCheck, hp] end Sshx diff --git a/skills/sshx/formal/Sshx/Budget.lean b/skills/sshx/formal/Sshx/Budget.lean index 3c872983..34d0618f 100644 --- a/skills/sshx/formal/Sshx/Budget.lean +++ b/skills/sshx/formal/Sshx/Budget.lean @@ -3,6 +3,8 @@ Source: `## Fix Or Done` (sole owner) and the charging sentences of `## Termination Gate`. One precommitted natural number; every counted pass decrements it; nothing refunds it. +`repairWithRerunReview` charges an entire finite repair batch, including its final review. +Behavior.Model carries that already-paid work inside fixOrDone, even at zero units. -/ namespace Sshx diff --git a/skills/sshx/formal/Sshx/Carrier.lean b/skills/sshx/formal/Sshx/Carrier.lean index 2c2be738..114a926a 100644 --- a/skills/sshx/formal/Sshx/Carrier.lean +++ b/skills/sshx/formal/Sshx/Carrier.lean @@ -27,6 +27,11 @@ def Carrier.univ : List Carrier := [.codexCli, .nyxidOracle, .isolatedTokenSubag theorem Carrier.mem_univ (c : Carrier) : c ∈ Carrier.univ := by cases c <;> decide +-- SKILL[def]: "A `tests` review seat must be assigned to a carrier capable of executing repository verification commands in the `work_target`, which is the per-seat constraint that keeps `nyxid-oracle` out of that seat's feasible draws." +def canRunRepositoryCommands : Carrier → Bool + | .codexCli | .isolatedTokenSubagent => true + | .nyxidOracle => false + /-- `WorkerMode` has exactly the three carriers plus `abstain`. -/ inductive WorkerMode | carrier (c : Carrier) diff --git a/skills/sshx/formal/Sshx/Clauses/Boundaries.lean b/skills/sshx/formal/Sshx/Clauses/Boundaries.lean index 94f2a901..a2ded803 100644 --- a/skills/sshx/formal/Sshx/Clauses/Boundaries.lean +++ b/skills/sshx/formal/Sshx/Clauses/Boundaries.lean @@ -108,8 +108,10 @@ inductive BaselineFailure | wrongConvergence | contaminatedAdjudication | boundaryDrift + | forcedIntakeConfirmation 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." /-- The model object that guards each baseline class. -/ def guardedBy : BaselineFailure → String | .fakeConsensus => "Sshx.caller_never_consensus, Sshx.fake_roster_rejected" @@ -119,6 +121,7 @@ def guardedBy : BaselineFailure → String | .wrongConvergence => "Sshx.no_implement_without_worth, Sshx.Semantics.candidate_dominance_is_preorder" | .contaminatedAdjudication => "Sshx.same_round_peer_invisible, Sshx.Semantics.enlarging_closure_only_removes_admission" | .boundaryDrift => "Sshx.fallback_forbids, Sshx.Behavior.never_lifecycle" + | .forcedIntakeConfirmation => "Sshx.Behavior.guardWriteGoal" /-! ## Transcript template -/ @@ -144,7 +147,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 the same verified construction hypothesis applies, the register cannot be completed, and every entry added must be held true by every later change." +-- 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." 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 f7d2b601..bf299e56 100644 --- a/skills/sshx/formal/Sshx/Clauses/Contract.lean +++ b/skills/sshx/formal/Sshx/Clauses/Contract.lean @@ -60,18 +60,23 @@ theorem run_follows_risk_not_budget (t p s : Bool) (budget : Nat) : /-! ## Goal contract: harness, gate entry, goal source, iteration question -/ --- SKILL[ref]: "If any `harness` sub-item is missing or ambiguous, or its source has not been confirmed by the boundary owner, stop and escalate to the maintainer; neither controller nor worker may infer or expand it." -abbrev incompleteHarnessEscalates := @applicability +-- SKILL[ref]: "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." +abbrev routineHarnessGapRouting := @Behavior.guardWriteGoal --- SKILL[thm]: "When an otherwise complete, unambiguous, boundary-owner-confirmed `provided_capabilities` value contains no such entry, whether silent or explicitly negative, the gate is inapplicable without asserting that the host mechanism is absent." +-- SKILL[ref]: "Silence or routine ambiguity never creates a startup questionnaire or pause." +abbrev routineSilenceNoPause := @Behavior.guardWriteGoal + +-- SKILL[thm]: "Silence is not absence and does not trigger a confirmation question." +abbrev silentContinuationEntry := @applicability + +-- SKILL[thm]: "When a complete `provided_capabilities` value contains no positive entry, the gate is inapplicable without asserting that the host mechanism is absent." theorem no_entry_is_inapplicable : - applicability true .absent = .inapplicable ∧ applicability true .silent = .inapplicable := + applicability .absent = .inapplicable ∧ applicability .silent = .inapplicable := ⟨rfl, rfl⟩ --- SKILL[thm]: "A purported continuation entry that is ambiguous or unconfirmed is governed by the existing harness rule above." -theorem ambiguous_entry_escalates : - applicability true .ambiguous = .escalateToMaintainer ∧ - applicability true .unconfirmed = .escalateToMaintainer := +theorem ambiguous_entry_withholds_claim : + applicability .ambiguous = .withholdClaim ∧ + applicability .unconfirmed = .withholdClaim := ⟨rfl, rfl⟩ /-- The only goal source. -/ @@ -146,10 +151,12 @@ structure ImplementationBrief where def implementationAllowed (b : ImplementationBrief) : Bool := b.planApprovedByThinkingGate -- SKILL[def]: "Keep the implementation boundary narrow and state any deviation before making it." +-- SKILL[ref]: "Scope changes retain the existing correction, direction and class gates." def implementationConforming (b : ImplementationBrief) : Bool := b.boundaryNarrow && b.deviationStatedBeforeMade -- 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." abbrev implementationIsAFlight := @Behavior.guardOpenFlight /-- What crosses between caller and implementation worker. -/ @@ -161,6 +168,7 @@ structure ImplementationExchange where deriving DecidableEq, Repr -- SKILL[def]: "The caller context may pass the approved concrete plan and constraints, then receive `conclusion` and `log_ref`; changed-file and test evidence belong in `conclusion`, and process logs stay behind `log_ref`." +-- SKILL[ref]: "Tests continue during implementation; routing never substitutes for independent review." def ImplementationExchange.conforming (e : ImplementationExchange) : Bool := e.planAndConstraintsPassed && e.changedFileEvidenceInConclusion && e.testEvidenceInConclusion && e.processLogsBehindLogRef diff --git a/skills/sshx/formal/Sshx/Clauses/Delegation.lean b/skills/sshx/formal/Sshx/Clauses/Delegation.lean index 46edf4f5..10f66533 100644 --- a/skills/sshx/formal/Sshx/Clauses/Delegation.lean +++ b/skills/sshx/formal/Sshx/Clauses/Delegation.lean @@ -122,11 +122,6 @@ theorem fallback_keeps_seat_and_role (id : Nat) (c : Carrier) (f : Behavior.Flig (Behavior.reopenFlight id c f).target = f.target := ⟨rfl, rfl, rfl⟩ --- SKILL[def]: "A `tests` review seat must be assigned to a carrier capable of executing repository verification commands in the `work_target`, which is the per-seat constraint that keeps `nyxid-oracle` out of that seat's feasible draws." -def canRunRepositoryCommands : Carrier → Bool - | .codexCli | .isolatedTokenSubagent => true - | .nyxidOracle => false - def testsSeatEligible (c : Carrier) : Bool := canRunRepositoryCommands c theorem oracle_cannot_hold_tests_seat : testsSeatEligible .nyxidOracle = false := rfl @@ -140,15 +135,10 @@ def SeatAssignment.seats (a : SeatAssignment) : List Behavior.Role := a.map Prod def SeatAssignment.carriers (a : SeatAssignment) : List Carrier := a.map Prod.snd -/-- The per-seat carrier constraint a draw must respect; only `tests` is restricted. -/ -def seatEligible : Behavior.Role → Carrier → Bool - | .tests, c => canRunRepositoryCommands c - | _, _ => true - -- SKILL[def]: "Which named seat holds which carrier rotates: at each stage dispatch the caller draws one assignment uniformly at random from every assignment that satisfies that composition and this stage's per-seat carrier constraints, so a named role holds a carrier only for the stage dispatch it was drawn for." def drawFeasible (seats : List Behavior.Role) (a : SeatAssignment) : Prop := a.seats = seats ∧ a.carriers.Perm (stageComposition seats.length) ∧ - ∀ p ∈ a, seatEligible p.1 p.2 = true + ∀ p ∈ a, Behavior.seatEligible p.1 p.2 = true /-- Rotation permutes seats over a fixed composition: every feasible draw carries exactly the same carrier counts as the composition, so randomizing seats never trades heterogeneity away. -/ @@ -167,7 +157,7 @@ theorem oracle_never_drawn_for_tests {seats : List Behavior.Role} {a : SeatAssig (h : drawFeasible seats a) : (Behavior.Role.tests, Carrier.nyxidOracle) ∉ a := by intro hmem have := h.2.2 _ hmem - simp [seatEligible, canRunRepositoryCommands] at this + simp [Behavior.seatEligible, canRunRepositoryCommands] at this /-- The review stage's named seats. -/ def reviewSeats : List Behavior.Role := [.architecture, .quality, .tests] diff --git a/skills/sshx/formal/Sshx/Gate.lean b/skills/sshx/formal/Sshx/Gate.lean index 1278d3a4..5e5e4f73 100644 --- a/skills/sshx/formal/Sshx/Gate.lean +++ b/skills/sshx/formal/Sshx/Gate.lean @@ -21,23 +21,23 @@ inductive ContinuationEntry inductive Applicability | applies | inapplicable - | escalateToMaintainer + | withholdClaim deriving DecidableEq, Repr --- SKILL[def]: "The termination gate is triggered only by a positive, boundary-owner-confirmed entry declaring such a mechanism." -/-- The gate is triggered only by a positive, boundary-owner-confirmed entry; a silent or +-- SKILL[def]: "The termination gate is triggered only by an existing positive authoritative entry declaring such a mechanism." +-- SKILL[def]: "It applies only when an existing positive authoritative `harness.provided_capabilities` entry is present and the caller is about to assert that `GoalArtifact` is satisfied." +-- SKILL[def]: "Ambiguous or unconfirmed authority withholds or escalates that claim under the existing table; it never creates a startup confirmation question." +/-- The gate is triggered only by an existing positive authoritative entry; a silent or explicitly negative complete harness makes the gate inapplicable without asserting the -mechanism is absent; anything else is the harness rule: stop and escalate. -/ -def applicability (harnessComplete : Bool) (e : ContinuationEntry) : Applicability := - if !harnessComplete then .escalateToMaintainer - else match e with - | .present => .applies - | .absent | .silent => .inapplicable - | .ambiguous | .unconfirmed => .escalateToMaintainer - -theorem applies_iff (h : Bool) (e : ContinuationEntry) : - applicability h e = .applies ↔ h = true ∧ e = .present := by - cases h <;> cases e <;> simp [applicability] +mechanism is absent. Ambiguous or unconfirmed authority is handled at claim evaluation. -/ +def applicability : ContinuationEntry → Applicability + | .present => .applies + | .absent | .silent => .inapplicable + | .ambiguous | .unconfirmed => .withholdClaim + +theorem applies_iff (e : ContinuationEntry) : + applicability e = .applies ↔ e = .present := by + cases e <;> simp [applicability] /-! ## Binding (`## Termination Gate`) -/ diff --git a/skills/sshx/formal/Sshx/Reasoning/Authority.lean b/skills/sshx/formal/Sshx/Reasoning/Authority.lean index 5aec5ab2..5851ec46 100644 --- a/skills/sshx/formal/Sshx/Reasoning/Authority.lean +++ b/skills/sshx/formal/Sshx/Reasoning/Authority.lean @@ -112,18 +112,22 @@ theorem advisory_never_sole_basis (i : Input) (h : force i = .advisory) (d : Sol /-- A plan element and what admits it. -/ structure PlanElement where kind : String - namesGoalTermThatDemandsIt : Bool + basis : Finding namesCurrentConsumer : Bool 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." def planElementAdmitted (e : PlanElement) : Bool := - e.namesGoalTermThatDemandsIt || e.namesCurrentConsumer + let input := { e.basis.input with + namesGoalTerm := e.basis.input.namesGoalTerm || e.namesCurrentConsumer } + downgrade { e.basis with verdict := .reject, input } == .reject -theorem test_never_creates_admission (e : PlanElement) (h : e.namesGoalTermThatDemandsIt = false) +theorem test_never_creates_admission (e : PlanElement) (h : e.basis.input.namesGoalTerm = false) (h' : e.namesCurrentConsumer = false) : planElementAdmitted e = false := by - simp [planElementAdmitted, h, h'] + simp [planElementAdmitted, downgrade, 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" /-- An actual defect names both conjuncts, so the rule never removes it. -/ @@ -217,7 +221,28 @@ theorem shape_list_is_not_a_closure {A : Type} [Fintype A] (register : A → A -- SKILL[def]: "Extending an enumeration over an absorbed class is an ugly defect under the aesthetic verdict, not diligence." def extendingAbsorbedEnumeration : UglyDefect := .specialCase --- SKILL[thm]: "Without that construction hypothesis, a separately proven finite-domain completeness result remains admissible." +-- SKILL[thm]: "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." +theorem verified_diagonal_escapes {A : Type} [Fintype A] (register : A → A → Force) : + diagonal Semantics.Force.flip register ∉ Set.range register := + Semantics.register_diagonal_unlisted register + +-- SKILL[def]: "An open or infinite label alone proves no impossibility, and enumeration alone proves no completeness." +structure DiagonalApplicationEvidence where + finiteRegisterRecorded : Bool + fixedPointFreeConstructor : Bool + theoremHypothesesVerified : Bool + admissibleInputCorrespondence : Bool + deriving DecidableEq, Repr + +def diagonalApplicationAdmitted (e : DiagonalApplicationEvidence) : Bool := + e.finiteRegisterRecorded && e.fixedPointFreeConstructor && + e.theoremHypothesesVerified && e.admissibleInputCorrespondence + +theorem diagonal_application_needs_correspondence (e : DiagonalApplicationEvidence) + (h : e.admissibleInputCorrespondence = false) : + diagonalApplicationAdmitted e = false := by + simp [diagonalApplicationAdmitted, h] + /-- Without a fixed-point-free constructor the escape argument does not apply: the identity twist has fixed points, so a listing may contain its own diagonal. -/ theorem no_constructor_no_escape : diff --git a/skills/sshx/formal/Sshx/Reasoning/Guards.lean b/skills/sshx/formal/Sshx/Reasoning/Guards.lean index 9f55605a..2c87eac0 100644 --- a/skills/sshx/formal/Sshx/Reasoning/Guards.lean +++ b/skills/sshx/formal/Sshx/Reasoning/Guards.lean @@ -3,24 +3,15 @@ import Sshx.Blocking /-! # Reasoning boundary and planning guards -These small predicates keep trigger provenance, pre-run occurrence, review-focus scope, -repeated-family routing, and planning evidence explicit. They are prompt-level evidence, not a -runtime schema. +These small predicates keep review-focus scope and planning evidence explicit. They are +prompt-level evidence, not a runtime schema. Trigger provenance and class repair routing live at +their decision owners so the guards cannot drift away from the blocking and repair paths. -/ namespace Sshx.Reasoning open Sshx --- SKILL[def]: "During `intake`, the caller must ask the boundary owner" -structure IntakeScopeAnswers where - outputConsumerConfirmed : Bool - localStateScopeConfirmed : Bool - deriving DecidableEq, Repr - -def intakeScopeComplete (answers : IntakeScopeAnswers) : Bool := - answers.outputConsumerConfirmed && answers.localStateScopeConfirmed - -- SKILL[def]: "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." structure PlanningEvidence where sourcesSearched : Bool @@ -82,51 +73,6 @@ def ordinaryOperationKeepsTrustedFailureEligible (ordinaryPath : Bool) (trustedF def nonstandardOmissionIsNotOrdinary (nonstandardPath : Bool) (omission : Bool) : Bool := nonstandardPath && omission --- SKILL[def]: "A blocking finding must also pass the structured trigger check" -inductive TriggerPath - | ordinaryOperation - | nonstandardDeliberate - | malicious - deriving DecidableEq, Repr - -structure TriggerRecord where - trigger : String - triggerActor : String - triggerPath : TriggerPath - mechanismFamily : String - recordedOccurrence : Option String - deriving DecidableEq, Repr - -def triggerCheck (record : TriggerRecord) : Bool := - match record.triggerPath with - | .ordinaryOperation => true - | .nonstandardDeliberate | .malicious => record.recordedOccurrence.isSome - --- SKILL[def]: "`recorded_occurrence` must have existed before this run" -def occurrenceIsIndependent (recordedOccurrence : Option String) (createdDuringRun : Bool) : Bool := - recordedOccurrence.isSome && !createdDuringRun - --- SKILL[thm]: "a fixture, reproduction, or state deliberately created by a seat, caller, or repair worker during this run is reachability evidence only" -theorem run_fixture_is_not_occurrence (createdDuringRun : Bool) : - occurrenceIsIndependent none createdDuringRun = false := by - simp [occurrenceIsIndependent] - --- SKILL[def]: "An input that names both is blocking" -def findingForce (input : Input) (record : TriggerRecord) : Force := - if force input == .blocking && triggerCheck record then .blocking else .advisory - --- SKILL[thm]: "An input that names fewer than both is advisory" -theorem missing_conjunct_is_advisory (input : Input) (record : TriggerRecord) - (h : input.namesGoalTerm = false ∨ input.namesWorkEvidence = false) : - findingForce input record = .advisory := by - rcases h with h | h <;> simp [findingForce, force, h] - --- SKILL[thm]: "Failure is objective, not semantic" -theorem ordinary_reachable_failure_stays_blocking (input : Input) (record : TriggerRecord) - (hi : force input = .blocking) (hp : record.triggerPath = .ordinaryOperation) : - findingForce input record = .blocking := by - simp [findingForce, hi, triggerCheck, hp] - -- SKILL[def]: "Inputs that name no second conjunct include an imagined input" def imaginedInputIsAdvisory : Bool := true @@ -152,26 +98,10 @@ def planNeedsPlanningEvidence (hasEvidence reusesCoveredWork namesUncoveredDelta -- SKILL[def]: "Missing or unverified planning evidence is `ASSUMED-UNVERIFIED` and cannot by itself justify `implement`." def missingPlanningEvidenceBlocksImplement (evidenceVerified : Bool) : Bool := !evidenceVerified --- SKILL[def]: "It must also carry the structured `trigger`, `trigger_actor`, `trigger_path`" +-- SKILL[def]: "It must carry the fields required by `## Result Envelope`." def findingMetadataShapeComplete (metadata : TriggerRecord) : Bool := metadata.trigger != "" && metadata.triggerActor != "" && metadata.mechanismFamily != "" --- SKILL[def]: "Before dispatching a repair after two consecutive passes whose blocking findings name the same" -inductive FamilyRoute - | continue - | escalateToBoundaryOwner - deriving DecidableEq, Repr - -def repeatedFamilyRoute (sameGoalTerm sameMechanismFamily familyDeclared : Bool) : FamilyRoute := - if sameGoalTerm && sameMechanismFamily && !familyDeclared then - .escalateToBoundaryOwner - else - .continue - --- SKILL[def]: "A class-level decision may use only the recorded findings and confirmed harness" -def classDecisionUsesRecordedInputs (recordedFindings confirmedHarness : Bool) : Bool := - recordedFindings && confirmedHarness - -- 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/Repair.lean b/skills/sshx/formal/Sshx/Reasoning/Repair.lean index 3496d5b3..521a2f00 100644 --- a/skills/sshx/formal/Sshx/Reasoning/Repair.lean +++ b/skills/sshx/formal/Sshx/Reasoning/Repair.lean @@ -1,7 +1,7 @@ import Mathlib.Tactic import Sshx.Budget import Sshx.Gate -import Sshx.Behavior.Model +import Sshx.Records import Sshx.Reasoning.Convergence /-! @@ -45,19 +45,95 @@ theorem unimproved_passes_prove_nothing (passesWithoutImprovement : Nat) : def identicalPassIsProgress : Bool := false -/-- One repair step as the contract shapes it. -/ -structure RepairStep where - askedWhatStillDiffers : Bool - smallestChange : Bool - delegatedToWorkerFlight : Bool - callerStayedOrchestrationOnly : Bool - rerunReviewTriplet : Bool +/-- Coverage judgments in the existing conclusion; these are review evidence, not new +runtime fields. A verified invariant or abstraction can cover an infinite domain. -/ +inductive ClassCoverageBasis + | uniformInvariant (verified : Bool) + | soundAbstraction (verified : Bool) + | completeFiniteTreatment (verified : Bool) + | authorizedBoundary (enforced authorized : Bool) + | unsupportedMemberEnumeration + | unknown deriving DecidableEq, Repr --- SKILL[def]: "If review exits `fix`, ask what still differs from `GoalArtifact`, apply the smallest change that addresses that blocking goal gap by delegating it to a worker using the stage's default carrier exactly as `## Implementation Worker` requires - open a new `SshxWorkerFlightRecord` for the same `work_target` and stay orchestration-only for the repair - then rerun the review triplet on the worker's returned `conclusion`." -def RepairStep.conforming (r : RepairStep) : Bool := - r.askedWhatStillDiffers && r.smallestChange && r.delegatedToWorkerFlight && - r.callerStayedOrchestrationOnly && r.rerunReviewTriplet +inductive FamilyRoute + | continue + | reviseOrInvestigate + | honestStop + | 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." + +-- SKILL[def]: "Record the goal/property, authorized domain, family, coverage basis, action/owner and falsifiable validation in the existing conclusion." +structure FamilyEvidence where + goalTerm : String + property : String + authorizedInputDomain : String + mechanismFamily : String + actionOwner : String + falsifiableValidation : String + sameGoalTerm : Bool + sameMechanismFamily : Bool + consecutivePasses : Nat + earlierUnsupportedEnumeration : Bool + coverageBasis : ClassCoverageBasis + noSupportedPath : Bool + ownerDecisionRequired : Bool + changesDomainOrCriterion : Bool + ownerAuthorized : Bool + revision : Option Revision + 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) + +def FamilyEvidence.recordComplete (e : FamilyEvidence) : Bool := + e.goalTerm != "" && e.property != "" && e.authorizedInputDomain != "" && + e.mechanismFamily != "" && e.actionOwner != "" && e.falsifiableValidation != "" + +-- 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." +def classGateActive (e : FamilyEvidence) : Bool := + (e.sameGoalTerm && e.sameMechanismFamily && 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." +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." +def familyRoute (e : FamilyEvidence) : FamilyRoute := + if e.ownerDecisionRequired || (e.changesDomainOrCriterion && !e.ownerAuthorized) then .ownerDecision + else if !ownerAuthorizedDomainChange e 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." +/-- 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 := + match t with + | .repairWithRerunReview => familyRoute e == .continue + | .repeatedReviewPass | .metaLayerConvergence | .focusedRound => + familyRoute e == .continue || familyRoute e == .reviseOrInvestigate + | _ => true + +theorem unsupported_class_never_dispatches (e : FamilyEvidence) + (h : e.coverageBasis = .unsupportedMemberEnumeration) + (ha : classGateActive e = true) : + familyPassAllowed e .repairWithRerunReview = false := by + 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 /-- Where a blocking gap sits in `GoalArtifact`; lower ranks are repaired first. -/ inductive GapRank @@ -91,44 +167,39 @@ theorem main_path_first (gaps : List GapRank) (h : .normalizedGoal ∈ gaps) : have hxeq : x = .normalizedGoal := by simpa using (List.mem_filter.mp hxmem).2 simp [hx, hxeq] --- SKILL[ref]: "Stop when `pass_budget` owned below is exhausted and report remaining blockers honestly." +-- SKILL[ref]: "At zero units, start no new pass and report remaining blockers honestly; finish the already-paid batch including its review." abbrev stopWhenExhausted := @Sshx.step_zero_counted inductive DoneRoute | claimCandidateThroughGate | reportDone + | withholdClaim deriving DecidableEq, Repr -- SKILL[def]: "If review exits `done with advisory surfaced`, treat that exit as a candidate for an affirmative success claim rather than the claim itself when `## Termination Gate` applies, and route the candidate through that gate before reporting success." def routeDoneExit : Applicability → DoneRoute | .applies => .claimCandidateThroughGate | .inapplicable => .reportDone - | .escalateToMaintainer => .claimCandidateThroughGate + | .withholdClaim => .withholdClaim theorem done_is_only_a_candidate_when_gate_applies : routeDoneExit .applies = .claimCandidateThroughGate := rfl --- SKILL[ref]: "Include any non-blocking advisory feedback without inlining logs." -abbrev advisoryWithoutLogs := @Behavior.ContextItem.permitted - inductive BoundedPassChoice | oneMoreBoundedPass (nextIterationQuestion : String) | askTheUser deriving DecidableEq, Repr --- SKILL[def]: "If review exits `explicit user decision or another bounded review pass`, either run one more bounded pass with a concrete next iteration question tied to `GoalArtifact`, or ask the user to decide." -def allCommentExitChoices (question : String) : List BoundedPassChoice := - [.oneMoreBoundedPass question, .askTheUser] +-- SKILL[def]: "If review exits `explicit user decision or another bounded review pass`, run one more bounded pass with a concrete next iteration question tied to `GoalArtifact`; when no bounded pass remains, report the unresolved evidence and route it to the declared owner." +def allCommentExitChoices (question : String) (needsOwnerDecision : Bool) : List BoundedPassChoice := + [.oneMoreBoundedPass question] ++ if needsOwnerDecision then [.askTheUser] else [] --- SKILL[ref]: "Do not loop indefinitely." +-- SKILL[ref]: "Do not pause for routine confirmation or ask the user to choose a method, and do not loop indefinitely." abbrev noIndefiniteLoop := @Sshx.counted_passes_bounded --- SKILL[ref]: "After any explicit correction, use the existing correction 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 before further work." +-- SKILL[ref]: "After any explicit correction, repeat this section's direction gate before further work." abbrev correctionGate := @reflect --- SKILL[policy]: "Protocol policy, not a mathematical consequence: before the first pass after the initial review triplet, the caller records one owner-precommitted finite integer `pass_budget`." -abbrev passBudgetPrecommitment := @Behavior.guardRecordPassBudget - -- SKILL[ref]: "Carrier retries and fallbacks are bounded by each flight's `retry_budget` and the finite eligible-untried-carrier set and consume no unit; the initial review triplet is the single occurrence fixed by the stage order and consumes none." abbrev uncountedTransitions := @Sshx.step_uncounted diff --git a/skills/sshx/formal/Sshx/Reasoning/Review.lean b/skills/sshx/formal/Sshx/Reasoning/Review.lean index 6cbcf2ea..39df87ca 100644 --- a/skills/sshx/formal/Sshx/Reasoning/Review.lean +++ b/skills/sshx/formal/Sshx/Reasoning/Review.lean @@ -2,6 +2,7 @@ import Mathlib.Tactic import Sshx.Tables import Sshx.Reasoning.Authority import Sshx.Reasoning.Discipline +import Sshx.Behavior.Model /-! # Reasoning: review @@ -101,6 +102,9 @@ 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." +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 @@ -121,11 +125,11 @@ structure BlockingFinding where conduct : TrustedPartyConduct deriving DecidableEq, Repr --- SKILL[def]: "Every blocking finding must name both `BlockingAuthority` conjuncts under `## Reasoning Discipline` — the `GoalArtifact` term the work as built fails and the evidence in the work that shows it — and which class of failure, omission, or uncertainty within the declared trust boundary it addresses." +-- 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 --- SKILL[ref]: "A `BlockingAuthority` downgrade is objective: it is recorded as `BlockingAuthority` requires and never assesses persuasiveness; disputed grounding stays blocking." +-- 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." @@ -133,26 +137,4 @@ theorem downgrade_only_for_ineligible_or_advisory (f : Finding) (h : f.verdict = (hc : downgrade f = .comment) : eligible f = false ∨ force f.input = .advisory := conversion_is_downgrade f h hc -/-- The state of the harness declaration at review time. -/ -inductive HarnessState - | declared - | missing - | ambiguous - | stale - deriving DecidableEq, Repr - -inductive HarnessRoute - | routeNormally - | pauseAndEscalateToMaintainer - deriving DecidableEq, Repr - --- SKILL[def]: "A missing, ambiguous, or stale harness declaration is never a downgrade shield: pause routing and escalate to the maintainer instead of declaring done." -def routeWithHarness : HarnessState → HarnessRoute - | .declared => .routeNormally - | .missing | .ambiguous | .stale => .pauseAndEscalateToMaintainer - -theorem defective_harness_never_shields (h : HarnessState) (hne : h ≠ .declared) : - routeWithHarness h = .pauseAndEscalateToMaintainer := by - cases h <;> simp_all [routeWithHarness] - end Sshx.Reasoning diff --git a/skills/sshx/formal/Sshx/Semantics/Register.lean b/skills/sshx/formal/Sshx/Semantics/Register.lean index f4d9265d..d5ce4342 100644 --- a/skills/sshx/formal/Sshx/Semantics/Register.lean +++ b/skills/sshx/formal/Sshx/Semantics/Register.lean @@ -4,15 +4,18 @@ import D5.S0.Diagonal.CaptureCount import Sshx.Blocking /-! -# Semantics: the advisory register is a Lawvere listing +# Semantics: the advisory register is a qualified Lawvere listing Source: `## Reasoning Discipline`, the enumeration paragraph after `BlockingAuthority`. Instance of the kernel-frozen escape theorems in `D5.S0.Diagonal.CaptureCount`. The contract's register of advisory shapes is a listing `g : A → A → Force`: each named -shape `a` classifies every shape. The adversarial seat's charter is the diagonal -`fun a => flip (g a a)`. Because `flip` has no fixed point, the diagonal is never a row -of the register: every finite register is escaped, whatever it lists. +shape `a` classifies every shape. When the domain is finite, the recorded constructor +`flip` is fixed-point-free, all other theorem hypotheses are verified, and the register is +evidenced to correspond to admissible inputs, the adversarial seat's charter is the diagonal +`fun a => flip (g a a)`, which escapes that register. The theorem does not apply to an open +or infinite label without those hypotheses, and an abstract escape does not by itself establish +a real admissible counterexample. -/ namespace Sshx.Semantics @@ -32,17 +35,15 @@ theorem flip_fixfree : Nat.card {y : Sshx.Force // Force.flip y = y} = 0 := by ⟨fun ⟨y, hy⟩ => by cases y <;> simp [Force.flip] at hy⟩ exact Nat.card_of_isEmpty --- SKILL[thm]: "every finite listing of cases is escaped by a fixed-point-free self-application" +-- SKILL[thm]: "A Lawvere-style diagonal escapes a register only under verified theorem hypotheses" /-- Every finite register of advisory shapes is escaped by its own diagonal (`escape_all_of_fixfree` instantiated at `Force` and `flip`). -/ theorem every_register_escaped {A : Type*} [Fintype A] (register : A → A → Sshx.Force) : IsEscaped Force.flip register := escape_all_of_fixfree Force.flip flip_fixfree register --- SKILL[thm]: "no extension of this or any register can complete it" -/-- The diagonal classification is never one of the register's rows: no extension of the -register lists it, because the escaped listings are all `2 ^ |A|²` listings -(`escaped_card_of_fixfree`). -/ +/-- Under the verified finite-domain and fixed-point-free hypotheses, the diagonal classification +is never one of the register's rows (`escaped_card_of_fixfree`). -/ theorem register_diagonal_unlisted {A : Type*} [Fintype A] (register : A → A → Sshx.Force) : diagonal Force.flip register ∉ Set.range register := every_register_escaped register diff --git a/skills/sshx/tests/test_sshx_contract.py b/skills/sshx/tests/test_sshx_contract.py index 3a103e2d..6776b2e6 100644 --- a/skills/sshx/tests/test_sshx_contract.py +++ b/skills/sshx/tests/test_sshx_contract.py @@ -36,8 +36,64 @@ legitimate edit requires both a synchronized digest update and Review Triplet judgment. ``pass_budget`` is the one counter the contract keeps; ``pass_budget_after`` and -``resolve_termination_claim`` model its decrement. No repair-rank or repair-sequence model exists -because the contract keeps none; English semantics stay with the Review Triplet absorber. +``resolve_termination_claim`` model its decrement. The Lean behavior model additionally projects finite implementation scope and its local flight +allowance from existing conclusions; this is not another global pass counter. English semantics +stay with the Review Triplet absorber. +Continuation baseline (recorded before batching edits): without whole-plan routing, +a completed first flight of a two-flight plan can enter review with approved work +remaining; repair passes have no operational route for their included rerun at zero +remaining units. Regression scenarios must exercise actual Lean allowed/step routes, +including partial, failed, exhausted and last-unit batches, not a second Python model. +The earlier worker reported pre-edit diagnostic evidence for forced startup questions, +detached intake/trigger/class gates and unconditional diagonal claims, but missed the +source-owned baseline timing requirement. This records that limitation, not a retroactive +claim that those earlier edits had a source-owned baseline. + +Repair R1-R4 baseline (2026-10-03, recorded before this repair's model edits): +without the corrections, writeGoal with silent/absent/ambiguous continuation followed +by declareGate present is allowed and changes gate to applies (guardDeclareGate reads +only goalWritten). An abstained flight can fallback to the same replacement carrier +repeatedly via its original id: guardFallback has no assignment-wide tried set. +The recovered scenario directly steps fallback/collect/recordImplementation without +launch or host notification, and its collect guard is false. A review-ready tests +seat accepts capability-checked nyxidOracle because guardOpenFlight has no per-seat +carrier constraint. These are current model/consumer discrepancies, not hostile +inputs. Repair evidence must use the production guards and effects and retain finite +assignment separation, autonomous intake, full-batch readiness and the paid final review. +The pre-repair Lean probe compiled these admissions and the rejected collection +against the unchanged model (lake env lean .lake/RepairBaseline.lean, exit 0). +This baseline belongs only to the admitted repair; the earlier timing limitation above +remains unchanged. + +T-R1-CORRECTION baseline (2026-10-03, before this correction's model edits): +the expressly surfaced tests-seat-held-out.lean probe compiled with the existing Lake +cache (lake env lean, exit 0). Its guarded implementation/review route accepts an +explicit boundary-owner continuation correction, but appendRevision changes only the +revision ledger: gate stays inapplicable, terminationExit stays none, and claimSatisfied +is allowed. gate_preserved_after_intake proves that even legitimate corrections cannot +update this projection. Without the repair, later claims consume stale authority. +This is an ordinary authorized source update under C5/S3/S5, not a request to infer +English authority or defend against a malicious owner. Regression evidence must cover +the source-update class, unsupported/unowned updates, and claims using current evidence +while retaining earlier revision/settlement facts. This narrow pre-edit reproduction +does not repair the historical baseline timing miss or claim pass-cap compliance. + +A-F2-ROSTER-SOURCE baseline (2026-10-03, before this evidence-source repair): +an outside-source Lean probe compiled against the unchanged model with the existing +Lake cache (stale-roster-baseline.lean, lake env lean, exit 0). From an approved-plan +fixture it proves every implementation/review guard, obtains an all-satisfied A1 +settlement, and appends an authorized positive-to-positive scope correction to A2. +Direct claim is refused, but resubmitting the genuine A1 roster to evaluateTermination +is allowed and restamps terminationAuthority as A2; claimSatisfied is then allowed +with the final budget unit consumed. The incoming interface carries no evaluated-source +association. Regression evidence must preserve that association from supplied evidence +through evaluation to claim: old A1 evidence must be refused while fresh A2 evidence +with identical verdicts is admitted. Relevant repeated/restored revisions and unrelated +notes must follow the same rule. Semantic truth of supplied evidence remains a premise. +This baseline does not undo the historical timing advisory. The session's immutable +pass_budget=3, remaining=0 and second explicitly recorded continuation exception remain; +no budget reset, refund, automatic extension or compliant-cap claim is made. + 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 @@ -318,7 +374,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 = "2896a31e2ddcbf25d48562f880ec60ccb9c43927950fe4a8737b451e9a35b436" +CANONICAL_NORMATIVE_DOCUMENT_SHA256 = "9b4e3ed87b774ee2b13041d7a07103cea4e58b445a5b7c5a8bae9c7ae202f0b8" JsonValue: TypeAlias = None | bool | int | float | str | list["JsonValue"] | dict[str, "JsonValue"] GapOwnerAssignment: TypeAlias = tuple[JsonValue, JsonValue] @@ -602,13 +658,13 @@ def resolve_termination_gate_applicability( capability_source_confirmed: bool, continuation_entry: str | None, ) -> str: - if not harness_complete or not capability_source_confirmed: - return "stop and escalate to the maintainer" - if continuation_entry == "present": + if continuation_entry == "present" and harness_complete and capability_source_confirmed: return "termination gate applies" if continuation_entry in {None, "absent"}: return "termination gate inapplicable" - return "stop and escalate to the maintainer" + if continuation_entry in {"ambiguous", "unconfirmed"} or not harness_complete or not capability_source_confirmed: + return "termination claim withheld; unresolved authority" + return "termination gate inapplicable" def blocking_force( @@ -634,6 +690,7 @@ def blocking_finding_force( trigger_path: str, recorded_occurrence: str | None, fields: frozenset[str] | None = None, + occurrence_pre_run: bool = True, ) -> str: required_fields = frozenset( {"trigger", "trigger_actor", "trigger_path", "mechanism_family", "recorded_occurrence"} @@ -644,7 +701,7 @@ def blocking_finding_force( raise ContractFailure("invalid trigger path") if basis_shown_false or not (names_goal_term and names_work_evidence): return "advisory" - if trigger_path != "ordinary-operation" and recorded_occurrence is None: + if trigger_path != "ordinary-operation" and (recorded_occurrence is None or not occurrence_pre_run): return "advisory" return "blocking" @@ -916,11 +973,11 @@ def test_sshx_goal_iteration_behavior_contract(self) -> None: ) self.assertIn("Do not generalize the convergence pass beyond that goal gap", text) self.assertIn( - "ask what still differs from `GoalArtifact`, apply the smallest change that addresses that blocking goal gap", + "Delegate the smallest changes for what still differs from `GoalArtifact`", text, ) self.assertIn( - "by delegating it to a worker using the stage's default carrier exactly as `## Implementation Worker` requires", + "using `## Implementation Worker` decomposition, allowance and evidence rules", text, ) self.assertIn("stay orchestration-only for the repair", text) @@ -943,7 +1000,9 @@ 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("stop and escalate to the maintainer", goal_section) + self.assertIn("must not ask a 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) self.assertEqual(text.count("`harness` is a prompt-level record containing exactly these three sub-items"), 1) self.assertEqual(text.count("`revisions` is an append-only list whose each item contains exactly these three sub-items"), 1) @@ -992,15 +1051,17 @@ def test_sshx_termination_trigger_and_claim_scope(self) -> None: "declare a host-provided goal-driven continuation mechanism only in `harness.provided_capabilities`", goal_section, ) - self.assertIn("must not discover or infer whether one exists", goal_section) + self.assertIn("must not discover or infer an external mechanism", goal_section) + self.assertIn("does not trigger a confirmation question", goal_section) for trigger_rule in [ - "triggered only by a positive, boundary-owner-confirmed entry", - "whether silent or explicitly negative, the gate is inapplicable", + "triggered only by an existing positive authoritative entry", + "When a complete `provided_capabilities` value contains no positive entry", "without asserting that the host mechanism is absent", - "purported continuation entry that is ambiguous or unconfirmed", + "Ambiguous or unconfirmed claim-specific authority constrains an affirmative claim", ]: self.assertIn(trigger_rule, goal_section) - self.assertIn("boundary-owner-confirmed `harness.provided_capabilities`", termination) + self.assertIn("existing positive authoritative `harness.provided_capabilities` entry", termination) + self.assertIn("never creates a startup confirmation question", termination) self.assertIn("permits only that `GoalArtifact`-scoped claim", termination) self.assertIn("does not certify any broader host goal condition", termination) for claim_surface in [ @@ -1042,9 +1103,9 @@ def test_sshx_termination_trigger_routing_is_total(self) -> None: "affirmative-presence": (True, True, "present", "termination gate applies"), "explicit-absence": (True, True, "absent", "termination gate inapplicable"), "silence": (True, True, None, "termination gate inapplicable"), - "ambiguous-entry": (True, True, "ambiguous", "stop and escalate to the maintainer"), - "unconfirmed-source": (True, False, "present", "stop and escalate to the maintainer"), - "incomplete-harness": (False, True, "present", "stop and escalate to the maintainer"), + "ambiguous-entry": (True, True, "ambiguous", "termination claim withheld; unresolved authority"), + "unconfirmed-source": (True, False, "present", "termination claim withheld; unresolved authority"), + "incomplete-harness": (False, True, "present", "termination claim withheld; unresolved authority"), } for name, (harness_complete, source_confirmed, entry, expected) in cases.items(): with self.subTest(case=name): @@ -1395,7 +1456,7 @@ def test_sshx_nonachievement_routes_report_honestly(self) -> None: delegation, ) self.assertIn( - "Stop when `pass_budget` owned below is exhausted and report remaining blockers honestly", + "At zero units, start no new pass and report remaining blockers honestly", fix_or_done, ) self.assertIn("reaching zero reports every unresolved blocker honestly", fix_or_done) @@ -1627,17 +1688,44 @@ def test_sshx_issue_1058_controls_are_declared_at_their_owners(self) -> None: review = section(text, "## Review Triplet", "## Review Truth Table") review_truth = section(text, "## Review Truth Table", "## Fix Or Done") fix_or_done = section(text, "## Fix Or Done", "## Termination Gate") - self.assertIn("who consumes outputs produced by the execution environment", goal) - self.assertIn("whether trusted operators' local state (configuration, indexes, and filesystem) is inside the review scope", goal) + self.assertIn("resolves these sub-items from the user's current input, repository rules", goal) + self.assertIn("records those sources and labels any minimal engineering assumptions explicitly", 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(f"`{field}`", envelope) - self.assertIn(f"`{field}`", review_truth) + 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("stop and escalate to the boundary owner", 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") + for basis in ("uniform invariant", "verified complete finite treatment", "already-authorized enforced boundary"): + self.assertIn(basis, reasoning) + self.assertIn("Unknown family or coverage routes bounded investigation under the intake scope", fix_or_done) self.assertIn("list each defense or validation element added since the previous pass", fix_or_done) + def test_sshx_intake_and_class_gate_use_existing_owner_paths(self) -> None: + text = read(SKILL) + 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.assertNotIn("IntakeScopeAnswers", guards) + self.assertNotIn("intakeScopeComplete", guards) + self.assertNotIn("repeatedFamilyRoute", guards) + for owner_path in [ + "def familyRoute", + "unsupported_class_never_dispatches", + "ClassCoverageBasis", + ]: + self.assertIn(owner_path, repair) + model = read(formal / "Sshx" / "Behavior" / "Model.lean") + self.assertIn("def guardPass", model) + self.assertNotIn("def repairDispatch", repair) + self.assertIn("member-by-member enumeration leaves the property unsupported", text) + self.assertIn("Do not pause for routine confirmation or ask the user to choose a method", text) + def test_sshx_planning_search_reuses_existing_work_and_plans_only_delta(self) -> None: text = read(SKILL) reasoning = section(text, "## Reasoning Discipline", "## Thinking Panel") @@ -1752,17 +1840,15 @@ def test_sshx_enumeration_escape_requires_verified_construction(self) -> None: fragment in reasoning for fragment in [ "That list is illustrative, not a closure, and enumeration is not itself an absorber", - "every finite listing of cases is escaped by a fixed-point-free self-application", - "an adversarial seat's charter is such a constructor", - "no extension of this or any register can complete it", - "the defense against an unlisted case is the two-conjunct test together with the declared recovery path, never another entry", + "A Lawvere-style diagonal escapes a register only under verified theorem hypotheses", + "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", "Extending an enumeration over an absorbed class is an ugly defect under the aesthetic verdict, not diligence", - "Without that construction hypothesis, a separately proven finite-domain completeness result remains admissible", ] ), "no finite listing of cases is escape-free" not in reasoning, "the longer the list grows the likelier" not in reasoning, - "when the same verified construction hypothesis applies, the register cannot be completed" in verification, + "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, finite_listing_closure_force( fixed_point_free_constructor_verified=True, finite_domain_completeness_proven=False, @@ -1813,7 +1899,7 @@ def test_sshx_blocking_gap_repair_order_is_main_path_first(self) -> None: self.assertEqual(text.count(anchor), 1) self.assertIn(anchor, fix_or_done) self.assertNotIn("`GoalArtifact` order", fix_or_done) - self.assertIn("Stop when `pass_budget` owned below is exhausted", fix_or_done) + self.assertIn("At zero units, start no new pass", fix_or_done) def test_sshx_depth_discipline_contract(self) -> None: text = read(SKILL) @@ -1945,15 +2031,13 @@ def test_sshx_blocking_authority_stage_references_and_downgrade_guards(self) -> self.assertIn(anchor, design) for anchor in [ "Every blocking finding must name both `BlockingAuthority` conjuncts under `## Reasoning Discipline`", - "the `GoalArtifact` term the work as built fails and the evidence in the work that shows it", "fails `ThreatEligibility` or `BlockingAuthority`", - "A `BlockingAuthority` downgrade is objective", - "it is recorded as `BlockingAuthority` requires and never assesses persuasiveness; disputed grounding stays blocking", + "Downgrade records and disputed grounding follow `BlockingAuthority`", "only for threat-model ineligibility or an advisory input", "never because a finding is inconvenient", "never sets aside a reachable defect", - "missing, ambiguous, or stale harness declaration", - "never a downgrade shield", + "Harness gaps and claim authority follow `## Goal Contract`", + "without startup confirmation", ]: self.assertIn(anchor, review) self.assertIn( @@ -2245,13 +2329,12 @@ def test_sshx_fixed_routing_units_and_reflection_actions(self) -> None: all( anchor in review_section for anchor in [ - "missing, ambiguous, or stale harness declaration", - "never a downgrade shield", - "pause routing", - "escalate to the maintainer", + "Harness gaps and claim authority follow `## Goal Contract`", + "claim authority follow `## Goal Contract`", + "without startup confirmation", ] ), - "missing unavailable-harness pause-and-escalate guard", + "missing autonomous intake authority guard", ) self.assertIn("`meta_judge` implement-exit gate", design_section) pre_fix_gate_start = fix_section.index("Before each fix or repeated review pass") @@ -2263,7 +2346,8 @@ def test_sshx_fixed_routing_units_and_reflection_actions(self) -> None: self.assertIn("Before each fix or repeated review pass", pre_fix_gate) self.assertIn("After any explicit correction", correction_gate) self.assertIn("`ThreatEligibility`", review_section) - for contract_section in [design_section, pre_fix_gate, correction_gate]: + self.assertIn("repeat this section's direction gate", correction_gate) + for contract_section in [design_section, pre_fix_gate]: for action in ["`continue`", "`revise`", "`stop`", "`escalate`"]: self.assertIn(action, contract_section) self.assertIn("responsible party", contract_section) @@ -3333,7 +3417,7 @@ def test_sshx_pass_budget_has_one_owner(self) -> None: ownership, "Protocol policy, not a mathematical consequence", precommit, - "a `meta-layer convergence`, a `focused round`, a repair flight together with its mandatory rerun review triplet, a repeated review pass without a repair, or a termination-gate evaluation including one that exits `reject fake termination consensus`", + "a `meta-layer convergence`, a `focused round`, a finite repair batch together with its mandatory rerun review triplet, a repeated review pass without a repair, or a termination-gate evaluation including one that exits `reject fake termination consensus`", "consumes exactly one unit when it is dispatched", "immutable for this run: no result, repair, or correction may add, replenish, reset, or replace units, and a unit is never refunded", "Carrier retries and fallbacks are bounded by each flight's `retry_budget` and the finite eligible-untried-carrier set and consume no unit",