From 4f77473d01bc9a6430d69ea8cabd23d1925ffc78 Mon Sep 17 00:00:00 2001 From: "macstudio-3[bot]" <315372789+macstudio-3[bot]@users.noreply.github.com> Date: Fri, 6 Nov 2026 06:16:56 +0800 Subject: [PATCH 1/2] fix(sshx): qualify extra-work uncertainty dispositions --- README.md | 2 +- README.zh-CN.md | 2 +- skills/sshx/SKILL.md | 2 +- skills/sshx/formal/README.md | 9 ++ .../formal/Sshx/Reasoning/Discipline.lean | 111 ++++++++++++++++-- skills/sshx/tests/test_sshx_contract.py | 27 ++++- 6 files changed, 142 insertions(+), 11 deletions(-) diff --git a/README.md b/README.md index d3ae5d8c..7f349170 100644 --- a/README.md +++ b/README.md @@ -57,7 +57,7 @@ The [review triplet](./skills/sshx/SKILL.md#review-triplet) applies the [review A [termination gate](./skills/sshx/SKILL.md#termination-gate) applies inside the final stage only when the host has positively declared a goal-driven continuation mechanism in the [goal contract](./skills/sshx/SKILL.md#goal-contract), and an affirmative satisfaction claim is being considered. It is not an eighth stage and grants no control over the host mechanism. -Only confirmed defects against the current goal or an existing contract enter automatic repairs. Findings retain `evidence_status` and `user_goal_basis`; uncertain changes to product or permission semantics go to their owner for clarification. A user correction cancels dependent stale plan, review and repair authority while preserving history and active-job protection. See [goal corrections](./skills/sshx/SKILL.md#goal-contract) and [admission](./skills/sshx/SKILL.md#reasoning-discipline). +Only confirmed defects against the current goal or an existing contract enter automatic repairs. Unverified objections alone authorize no repair or blocking goal-gap/abstention; bounded checks investigate unknowns only when the decision depends on them. Findings retain `evidence_status` and `user_goal_basis`; uncertain changes to product or permission semantics go to their owner for clarification. A user correction cancels dependent stale plan, review and repair authority while preserving history and active-job protection. See [goal corrections](./skills/sshx/SKILL.md#goal-contract) and [admission](./skills/sshx/SKILL.md#reasoning-discipline). ## Risks and Limits diff --git a/README.zh-CN.md b/README.zh-CN.md index 56de1e59..1cb789c5 100644 --- a/README.zh-CN.md +++ b/README.zh-CN.md @@ -57,7 +57,7 @@ 只有 host 在[目标合同](./skills/sshx/SKILL.md#goal-contract)中明确声明了目标驱动的继续执行机制，且 caller 正准备肯定目标已满足时，最后阶段内部才适用[终止闸门](./skills/sshx/SKILL.md#termination-gate)。它不是第八阶段，也不授予控制 host 机制的权限。 -只有违反当前目标或既有合同的已确认缺陷进入自动修复。发现项保留 `evidence_status` 与 `user_goal_basis`；涉及产品或权限语义的不确定改动向 owner 澄清。用户纠正立即撤销依赖旧方案的 plan、review 与 repair 权限，同时保留历史及 active job 保护。详见[目标纠正](./skills/sshx/SKILL.md#goal-contract)与[准入](./skills/sshx/SKILL.md#reasoning-discipline)。 +只有违反当前目标或既有合同的已确认缺陷进入自动修复。未验证的异议本身不授权修复或阻断性的 goal gap/abstain；只有决策依赖的未知项才值得进行有界核实。发现项保留 `evidence_status` 与 `user_goal_basis`；涉及产品或权限语义的不确定改动向 owner 澄清。用户纠正立即撤销依赖旧方案的 plan、review 与 repair 权限，同时保留历史及 active job 保护。详见[目标纠正](./skills/sshx/SKILL.md#goal-contract)与[准入](./skills/sshx/SKILL.md#reasoning-discipline)。 ## 风险与限制 diff --git a/skills/sshx/SKILL.md b/skills/sshx/SKILL.md index e7468932..83a0b4db 100644 --- a/skills/sshx/SKILL.md +++ b/skills/sshx/SKILL.md @@ -194,7 +194,7 @@ Planning evidence must be gathered before a thinking seat settles a candidate pl Aesthetic/adversarial: give a symmetric 美不美 (is it beautiful?) verdict for each candidate approach materially weighed: the chosen, revised, or repair approach and each rejected alternative whose rejection changed the conclusion — beautiful, mixed, or ugly, earned from evidence, not a presumed indictment; a micro-variation that changed no decision needs no separate verdict. Name any specific locatable ugly defect, or state `no material defect found` when none exists; where a defect exists, state why the approach is ugly as a specific locatable defect and what the beautiful form would be. Ugly defects include leaked abstraction, duplicated source of truth, special-case, bad coupling, asymmetry, lying name, hidden intent, or unverifiable premise. The beautiful form is the smaller, symmetric, single-responsibility, single-source-of-truth, intent-revealing form that satisfies `GoalArtifact` — smaller, not maximally complete; gold-plating past `GoalArtifact` is itself an ugly defect, not beauty. Beauty judges the coherence and integrity of the form that remains; whether any element is unnecessary is `parsimony`'s question, and whether the whole intervention is worth its cost is the `worth` seat's — beauty must not become a second parsimony or worth vote. -seek truth from facts: verify every factual premise against actual evidence before relying on it. Evidence examples include source artifact or line, current file contents, command result, test assertion, visible input, implementation-worker conclusion, or declared `GoalArtifact` constraint. Any assumed-not-verified premise must be explicitly marked `ASSUMED-UNVERIFIED` in `SshxResultEnvelope.conclusion` and either verified before routing, treated as a `GoalArtifact` goal gap, or used as an abstain trigger. A perspective must never silently rely on an assumed premise. +seek truth from facts: verify every factual premise against actual evidence before relying on it (source artifact or line, command result, test assertion). Mark decision-relevant unknowns `ASSUMED-UNVERIFIED` in `SshxResultEnvelope.conclusion`: verified before routing or bounded checks; a `GoalArtifact` goal gap or abstain trigger needs a separate admitted `BlockingAuthority` basis; abstain only if no bounded check is available. Irrelevant premises warrant no investigation; unsupported premises warrant no repair. A perspective must never silently rely on an assumed premise. A mathematical conclusion binds a mechanism only when that mechanism's recorded state instantiates every hypothesis the conclusion needs. A name applied by analogy carries no blocking, convergence, or completion force. A missing or disputed instantiation is `ASSUMED-UNVERIFIED`; a false instantiation makes the conclusion inapplicable. diff --git a/skills/sshx/formal/README.md b/skills/sshx/formal/README.md index 49708ecd..8992c2b9 100644 --- a/skills/sshx/formal/README.md +++ b/skills/sshx/formal/README.md @@ -184,6 +184,15 @@ and termination-seat settlement all consume that judgment. Downgrade records retain the original words and trigger decision. `force` alone remains a partial conjunct judgment, never a complete blocking decision. +`MarkedPremise.explicit` also qualifies uncertainty dispositions: an irrelevant +premise needs no disposition; bounded verification requires decision relevance +and an available bounded check. Goal-gap and abstention dispositions require a +separate `completeAdmission` basis; abstention additionally requires that no bounded +check is available. The theorems reject unsupported goal gaps and abstentions, +exclude irrelevant investigation, and preserve independently admitted missing +requirements. These are source/model correspondence checks, not live evidence of +an operational repair bypass or proof that a confirmed label is truthful. + `failed_trigger_rejected_by_every_consumer` checks the twenty existing decisions for every supplied input with a failed trigger, independently of prose labels; `admitted_basis_retained_by_every_consumer` retains every admitted basis that diff --git a/skills/sshx/formal/Sshx/Reasoning/Discipline.lean b/skills/sshx/formal/Sshx/Reasoning/Discipline.lean index 0afd1567..821be4ac 100644 --- a/skills/sshx/formal/Sshx/Reasoning/Discipline.lean +++ b/skills/sshx/formal/Sshx/Reasoning/Discipline.lean @@ -152,7 +152,7 @@ theorem beauty_ignores_cost_and_necessity (f : Form) (cost necessity : Nat) : /-! ## Seek truth from facts -/ --- SKILL[def]: "Evidence examples include source artifact or line, current file contents, command result, test assertion, visible input, implementation-worker conclusion, or declared `GoalArtifact` constraint." +-- SKILL[def]: "source artifact or line, command result, test assertion" inductive Evidence | sourceArtifactOrLine (ref : String) | currentFileContents (path : String) @@ -163,7 +163,7 @@ inductive Evidence | declaredGoalConstraint (item : String) deriving DecidableEq, Repr --- SKILL[def]: "seek truth from facts: verify every factual premise against actual evidence before relying on it." +-- SKILL[def]: "seek truth from facts: verify every factual premise against actual evidence before relying on it (source artifact or line, command result, test assertion)." structure Premise where claim : String evidence : Option Evidence @@ -181,21 +181,118 @@ def Premise.status (p : Premise) : PremiseStatus := | some e => .verified e | none => .assumedUnverified --- SKILL[def]: "Any assumed-not-verified premise must be explicitly marked `ASSUMED-UNVERIFIED` in `SshxResultEnvelope.conclusion` and either verified before routing, treated as a `GoalArtifact` goal gap, or used as an abstain trigger." +-- SKILL[def]: "Mark decision-relevant unknowns `ASSUMED-UNVERIFIED` in `SshxResultEnvelope.conclusion`: verified before routing or bounded checks; a `GoalArtifact` goal gap or abstain trigger needs a separate admitted `BlockingAuthority` basis; abstain only if no bounded check is available." inductive UnverifiedDisposition | verifiedBeforeRouting (e : Evidence) + | boundedVerification (question : String) | treatedAsGoalGap | abstainTrigger deriving DecidableEq, Repr -/-- A marked premise carries its disposition; a verified premise needs none. -/ +/-- A confirmed `BlockingAuthority` basis is required before an unverified premise +can block as a goal gap or abstention. Bounded investigation and abstention require that the +verdict actually depends on the premise; a non-empty question names the bounded check. -/ structure MarkedPremise where premise : Premise disposition : Option UnverifiedDisposition + blockingBasis : Option DecisionBasis + boundedCheckAvailable : Bool deriving DecidableEq, Repr +def MarkedPremise.dispositionAdmitted (m : MarkedPremise) : Bool := + match m.disposition with + | none => false + | some (.verifiedBeforeRouting _) => true + | some (.boundedVerification question) => + m.premise.verdictDependsOnIt && question != "" && m.boundedCheckAvailable + | some .treatedAsGoalGap => + m.premise.verdictDependsOnIt && m.blockingBasis.any completeAdmission + | some .abstainTrigger => + m.premise.verdictDependsOnIt && !m.boundedCheckAvailable && + m.blockingBasis.any completeAdmission + def MarkedPremise.explicit (m : MarkedPremise) : Prop := - m.premise.status = .assumedUnverified → m.disposition.isSome = true + m.premise.status = .assumedUnverified → + match m.disposition with + | none => m.premise.verdictDependsOnIt = false + | some _ => m.dispositionAdmitted = true + +-- SKILL[thm]: "Irrelevant premises warrant no investigation; unsupported premises warrant no repair." +theorem decision_irrelevant_unverified_needs_no_disposition (m : MarkedPremise) + (h : m.premise.verdictDependsOnIt = false) (hnone : m.disposition = none) : + m.explicit := by + intro _ + simp [hnone, h] + +theorem decision_irrelevant_cannot_investigate (m : MarkedPremise) (question : String) + (h : m.premise.verdictDependsOnIt = false) + (hd : m.disposition = some (.boundedVerification question)) : + m.dispositionAdmitted = false := by + simp [MarkedPremise.dispositionAdmitted, hd, h] + +theorem unverified_goal_gap_requires_admitted_basis (m : MarkedPremise) + (hstatus : m.premise.status = .assumedUnverified) + (hdisposition : m.disposition = some .treatedAsGoalGap) + (hexplicit : m.explicit) : + m.premise.verdictDependsOnIt = true ∧ + ∃ b, m.blockingBasis = some b ∧ completeAdmission b = true := by + have ha : m.dispositionAdmitted = true := by + simpa only [hdisposition] using hexplicit hstatus + have hb : m.premise.verdictDependsOnIt = true ∧ + m.blockingBasis.any completeAdmission = true := by + simpa only [MarkedPremise.dispositionAdmitted, hdisposition, Bool.and_eq_true] using ha + exact ⟨hb.1, (Option.any_eq_true _ _).mp hb.2⟩ + +def unsupportedGoalGap : MarkedPremise := + { premise := { claim := "unconfirmed premise", evidence := none, verdictDependsOnIt := true } + disposition := some .treatedAsGoalGap + blockingBasis := none + boundedCheckAvailable := false } + +theorem unsupported_goal_gap_is_not_explicit : ¬ unsupportedGoalGap.explicit := by + intro h + have hadmitted := h (by simp [unsupportedGoalGap, Premise.status]) + simp [unsupportedGoalGap, MarkedPremise.dispositionAdmitted] at hadmitted + +def boundedUnknown : MarkedPremise := + { premise := { claim := "unknown premise", evidence := none, verdictDependsOnIt := true } + disposition := some (.boundedVerification "check the decision-relevant workflow input") + blockingBasis := none + boundedCheckAvailable := true } + +theorem bounded_unknown_is_explicit : boundedUnknown.explicit := by + intro _ + simp [boundedUnknown, MarkedPremise.dispositionAdmitted] + +def unresolvableUnknown : MarkedPremise := + { premise := { claim := "unresolvable premise", evidence := none, verdictDependsOnIt := true } + disposition := some .abstainTrigger + blockingBasis := none + boundedCheckAvailable := false } + +theorem unsupported_abstention_is_not_explicit : ¬ unresolvableUnknown.explicit := by + intro h + have hadmitted := h (by simp [unresolvableUnknown, Premise.status]) + simp [unresolvableUnknown, MarkedPremise.dispositionAdmitted] at hadmitted + +theorem admitted_unresolvable_unknown_is_explicit (p : Premise) (b : DecisionBasis) + (hrelevant : p.verdictDependsOnIt = true) (hadmitted : completeAdmission b = true) : + (MarkedPremise.mk p (some .abstainTrigger) (some b) false).explicit := by + intro _ + simp [MarkedPremise.dispositionAdmitted, hrelevant, hadmitted] + +theorem available_check_prevents_abstention (m : MarkedPremise) + (h : m.boundedCheckAvailable = true) (hd : m.disposition = some .abstainTrigger) : + m.dispositionAdmitted = false := by + simp [MarkedPremise.dispositionAdmitted, hd, h] + +/-- An independently evidenced missing requirement retains the same admission, even +when another premise is unknown. No majority or observed-occurrence condition is added. -/ +theorem admitted_goal_gap_is_explicit (p : Premise) (b : DecisionBasis) + (hrelevant : p.verdictDependsOnIt = true) (hadmitted : completeAdmission b = true) : + (MarkedPremise.mk p (some .treatedAsGoalGap) (some b) false).explicit := by + intro _ + simp [MarkedPremise.dispositionAdmitted, hrelevant, hadmitted] -- SKILL[thm]: "A perspective must never silently rely on an assumed premise." /-- A premise the verdict depends on, assumed and carrying no disposition, is silent reliance @@ -206,9 +303,9 @@ def silentReliance (m : MarkedPremise) : Prop := theorem explicit_excludes_silent_reliance (m : MarkedPremise) (h : m.explicit) : ¬ silentReliance m := by - rintro ⟨-, hstatus, hnone⟩ + rintro ⟨hdepends, hstatus, hnone⟩ have := h hstatus - simp [hnone] at this + simp [hnone, hdepends] at this /-! ## Mathematical applicability -/ diff --git a/skills/sshx/tests/test_sshx_contract.py b/skills/sshx/tests/test_sshx_contract.py index 39239fdc..56915df1 100644 --- a/skills/sshx/tests/test_sshx_contract.py +++ b/skills/sshx/tests/test_sshx_contract.py @@ -381,6 +381,23 @@ The earlier #1071-#1074 baseline and caller-reported carrier evidence retain their original scope and timing; they are not observations by this assignment. +Extra-work-admission no-skill baseline (2026-11-05, before this assignment's +source/model edits): the published `seek truth from facts` sentence permits every +`ASSUMED-UNVERIFIED` premise to be treated as a `GoalArtifact` goal gap or an +abstain trigger without saying that either disposition must be decision-relevant or +pass `BlockingAuthority`. The unchanged formal projection `MarkedPremise.explicit` +accepts a premise with no evidence, `verdictDependsOnIt=true`, and either +`some .treatedAsGoalGap` or `some .abstainTrigger` because it checks only that a +disposition is present. This is a local contract/model ambiguity: the existing +`force`, `completeAdmission`, and operational consumers already require confirmed +evidence, a sourced goal basis, both named conjuncts, and trigger grounding, so no +live repair bypass is claimed. A source-level witness was established from the +HEAD source and rechecked independently during recovery; this pre-edit baseline +makes no compiled-model claim. Later compiled regressions are forward model evidence, +not a live observation of a repair bypass. The forward check must qualify the +dispositions while preserving confirmed actual defects and bounded checks for +decision-relevant unknowns. + ARCH-001 / TEST-1073-01 frozen repair baseline (2026-11-04): before this batch, the delegating caller supplied two independent compiled counterexamples against the dirty candidate. A confirmed, goal-sourced input with a failed trigger was @@ -697,7 +714,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 = "f590f8a8529b03053cbcd63a2d9478ede828a1261af3d9976ddc57fd93a2f6f2" +CANONICAL_NORMATIVE_DOCUMENT_SHA256 = "ca846cc828331f2d74e9563667a4022031f80b8f9d84fc87d41c2702087c8c9e" JsonValue: TypeAlias = None | bool | int | float | str | list["JsonValue"] | dict[str, "JsonValue"] GapOwnerAssignment: TypeAlias = tuple[JsonValue, JsonValue] @@ -4269,6 +4286,14 @@ def test_sshx_baseline_evidence_is_source_owned(self) -> None: ).stdout.strip() self.assertEqual(tracked, "") + def test_extra_work_admission_baseline_is_source_owned(self) -> None: + baseline = __doc__ or "" + marker = "Extra-work-admission no-skill baseline (2026-11-05, before this assignment's" + self.assertIn(marker, baseline) + self.assertIn("`MarkedPremise.explicit`", baseline) + self.assertIn("no compiled-model claim", baseline) + self.assertIn("no\nlive repair bypass is claimed", baseline) + def test_sshx_has_no_scientific_source_coupling(self) -> None: text = read(SKILL) self.assertEqual(set(formal_identifiers(text)), SSHX_CONTRACT_FORMAL_IDENTIFIERS) From e1ac5cd848f862ecc5078409014fe76e90e03ab5 Mon Sep 17 00:00:00 2001 From: "macstudio-3[bot]" <315372789+macstudio-3[bot]@users.noreply.github.com> Date: Fri, 6 Nov 2026 06:16:57 +0800 Subject: [PATCH 2/2] chore: upgrade version to 1.0.0-beta.56 --- .claude-plugin/marketplace.json | 2 +- .claude-plugin/plugin.json | 2 +- .codex-plugin/plugin.json | 2 +- .cursor-plugin/plugin.json | 2 +- gemini-extension.json | 2 +- package.json | 2 +- 6 files changed, 6 insertions(+), 6 deletions(-) diff --git a/.claude-plugin/marketplace.json b/.claude-plugin/marketplace.json index 505ed7d6..42981371 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.55", + "version": "1.0.0-beta.56", "source": "./", "author": { "name": "auric", diff --git a/.claude-plugin/plugin.json b/.claude-plugin/plugin.json index 04137f63..f0268e6f 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.55", + "version": "1.0.0-beta.56", "author": { "name": "auric", "email": "loning.ma@aelf.io" diff --git a/.codex-plugin/plugin.json b/.codex-plugin/plugin.json index e874cd73..050947f2 100644 --- a/.codex-plugin/plugin.json +++ b/.codex-plugin/plugin.json @@ -1,6 +1,6 @@ { "name": "consensus-rnd", - "version": "1.0.0-beta.55", + "version": "1.0.0-beta.56", "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 f35053f0..9f91e777 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.55", + "version": "1.0.0-beta.56", "author": { "name": "auric", "email": "loning.ma@aelf.io" diff --git a/gemini-extension.json b/gemini-extension.json index afb41d44..512b67f2 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.55", + "version": "1.0.0-beta.56", "contextFileName": "GEMINI.md" } diff --git a/package.json b/package.json index c0e26943..b6e9070b 100644 --- a/package.json +++ b/package.json @@ -1,6 +1,6 @@ { "name": "consensus-rnd", - "version": "1.0.0-beta.55", + "version": "1.0.0-beta.56", "description": "worker-delegated inline consensus skills：隔离多视角、固定真值表，无自有 daemon、GitHub 或 git 编排", "license": "MIT", "author": "auric ",