Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .claude-plugin/marketplace.json
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@
{
"name": "consensus-rnd",
"description": "worker-delegated inline consensus:隔离多视角、固定真值表,无 daemon、GitHub 或 git 编排",
"version": "1.0.0-beta.48",
"version": "1.0.0-beta.49",
"source": "./",
"author": {
"name": "auric",
Expand Down
2 changes: 1 addition & 1 deletion .claude-plugin/plugin.json
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
{
"name": "consensus-rnd",
"description": "worker-delegated inline consensus skills:隔离多视角、固定真值表,无 daemon、GitHub 或 git 编排",
"version": "1.0.0-beta.48",
"version": "1.0.0-beta.49",
"author": {
"name": "auric",
"email": "loning.ma@aelf.io"
Expand Down
2 changes: 1 addition & 1 deletion .codex-plugin/plugin.json
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
{
"name": "consensus-rnd",
"version": "1.0.0-beta.48",
"version": "1.0.0-beta.49",
"description": "worker-delegated inline consensus skills:隔离多视角、固定真值表,无 daemon、GitHub 或 git 编排",
"author": {
"name": "auric",
Expand Down
2 changes: 1 addition & 1 deletion .cursor-plugin/plugin.json
Original file line number Diff line number Diff line change
Expand Up @@ -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.48",
"version": "1.0.0-beta.49",
"author": {
"name": "auric",
"email": "loning.ma@aelf.io"
Expand Down
2 changes: 1 addition & 1 deletion gemini-extension.json
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
{
"name": "consensus-rnd",
"description": "worker-delegated inline consensus skills:隔离多视角、固定真值表,无 daemon、GitHub 或 git 编排",
"version": "1.0.0-beta.48",
"version": "1.0.0-beta.49",
"contextFileName": "GEMINI.md"
}
2 changes: 1 addition & 1 deletion package.json
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
{
"name": "consensus-rnd",
"version": "1.0.0-beta.48",
"version": "1.0.0-beta.49",
"description": "worker-delegated inline consensus skills:隔离多视角、固定真值表,无 daemon、GitHub 或 git 编排",
"license": "MIT",
"author": "auric <loning.ma@aelf.io>",
Expand Down
13 changes: 5 additions & 8 deletions skills/sshx/SKILL.md
Original file line number Diff line number Diff line change
Expand Up @@ -284,16 +284,13 @@ Material comparison coordinates form a product preorder: one candidate dominates

## Implementation Worker

Implement only the concrete plan approved by the thinking gate. Keep the implementation boundary narrow and state any deviation before making it.
Thinking-gate approval binds outcomes, scope and requirements before implementation. Send goal, verifiable acceptance, authorized scope/prohibitions and grounded context/evidence. Workers inspect the target and choose mechanics; compliant alternatives alone are not deviations. No caller recipes (steps, code/pseudocode, structures or algorithms), even as consensus, acceptance or prohibitions. Preserve user/host technical requirements with their sources. Report goal, authority or constraint changes before acting via existing correction, direction and class gates.

`sshx` does not grant permission to commit, push, merge, close issues, edit labels, publish releases, or mutate external lifecycle state.
Implementation must be delegated to a worker using the stage's default carrier under `WorkerDelegationContract`. No lifecycle authority is granted. Exchange the brief for `conclusion` (changed files, checks) and opaque `log_ref`.

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.
Predeclare finite assignments and allowance in the approved plan's conclusion. Accumulate completed/remaining obligations and test evidence; terminal completion permits handoff only. Pending work/checks stay in implementation within the allowance; exhaustion/failure reports unresolved work. Local allowance is separate from `pass_budget` and carrier retry/fallback bounds.

Initial review needs worker evidence for all approved work/checks and no active/unrecovered failed flight. Testing continues; routing never replaces independent review.

## Review Triplet

Expand Down Expand Up @@ -333,7 +330,7 @@ Every blocking finding must name both `BlockingAuthority` conjuncts under `## Re

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`, 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.
For `fix`, freeze admitted repairs as a finite batch under `## Implementation Worker` handoff, allowance and evidence rules; include findings and failure evidence. Delegate the smallest changes for what still differs from `GoalArtifact`; open a `SshxWorkerFlightRecord` per assignment and stay orchestration-only for the repair. Complete the batch before its one mandatory rerun review triplet; a chunk boundary never starts formal review. When a pass carries more than one blocking goal gap, repair them in goal-primacy rank, so the main path is repaired first. At zero units, 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`, 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.

Expand Down
10 changes: 10 additions & 0 deletions skills/sshx/formal/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -110,6 +110,16 @@ not claimed as consequences of the abstract model.

## What the model cannot verify

The implementation/repair handoff in `Clauses/Contract.lean` projects the approved
outcome, brief completeness, sourced requirements and worker ownership. Relabelling
a caller recipe cannot make it binding; a compliant internal alternative alone does
not activate the existing change gates. Both initial and repair examples use the same
projection. Requirement provenance, compliance and brief completeness are interpreted
premises, not classifications proved by Lean. The fixture
`tests/fixtures/implementation_dispatch.md` (relative to the skill directory) exercises
actual brief generation and routing; generated behavior evidence stays outside source.
These definitions do not extend the runtime or replace the independent review gate.

The trace ties each clause to a Lean object, and the Lean kernel checks the object. Whether
the object *means* what the English says is a human correspondence judgment, kept reviewable
by placing each quote next to its object. A clause traced as `prose` carries no norm in the
Expand Down
2 changes: 1 addition & 1 deletion skills/sshx/formal/Sshx/Behavior/Invariant.lean
Original file line number Diff line number Diff line change
Expand Up @@ -337,7 +337,7 @@ theorem review_dispatch_needs_whole_candidate (s : ProtocolState) (role : Role)
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."
-- SKILL[inv]: "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 =
Expand Down
12 changes: 6 additions & 6 deletions skills/sshx/formal/Sshx/Behavior/Model.lean
Original file line number Diff line number Diff line change
Expand Up @@ -165,7 +165,7 @@ structure ImplementationPlan where
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."
-- SKILL[def]: "Predeclare finite assignments and allowance in the approved plan's conclusion."
def ImplementationPlan.valid (p : ImplementationPlan) : Prop :=
p.obligations ≠ [] ∧ 0 < p.flightAllowance

Expand Down Expand Up @@ -289,7 +289,7 @@ def ProtocolState.batchSettled (s : ProtocolState) : Bool :=
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."
-- SKILL[guard]: "Initial review needs worker evidence for all approved work/checks and no active/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 :=
Expand All @@ -304,7 +304,7 @@ 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."
-- SKILL[guard]: "Pending work/checks stay in implementation within the allowance; exhaustion/failure reports unresolved work."
def guardImplementationFlight (s : ProtocolState) : Prop :=
(s.stage = .implementation ∨ s.stage = .fixOrDone) ∧
s.reviewStarted = false ∧ s.reviewReady = false ∧ s.batchSettled = true ∧
Expand Down Expand Up @@ -413,7 +413,7 @@ 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."
-- SKILL[guard]: "Worker conclusions accumulate completed and remaining obligations and test evidence; terminal flight completion permits handoff only."
-- SKILL[guard]: "Accumulate completed/remaining obligations and test evidence; terminal 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 ∧
Expand All @@ -423,7 +423,7 @@ def guardBeginImplementation (s : ProtocolState) (plan : ImplementationPlan) : P
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."
-- SKILL[guard]: "For `fix`, freeze admitted repairs as a finite batch under `## Implementation Worker` handoff, allowance and evidence rules;"
def guardPass (s : ProtocolState) (t : Transition) (e : Reasoning.FamilyEvidence)
(plan : Option ImplementationPlan) : Prop :=
s.stage = .fixOrDone ∧ Reasoning.familyPassAllowed e t = true ∧
Expand All @@ -450,7 +450,7 @@ def guardClaimSatisfied (s : ProtocolState) : Prop :=
(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."
-- SKILL[guard]: "No lifecycle authority is granted."
def guardNoLifecycle : Prop := False

-- SKILL[guard]: "Such a URL is permitted only when the referenced content is already anonymously readable on the remote, which the caller confirms before the first submission; the caller must never push, publish, change repository visibility, or otherwise mutate remote state to make content linkable."
Expand Down
Loading
Loading