skill-lean-implementation-hard

# Lean Implementation Hard Skill Thin wrapper that delegates Lean 4 hard-mode proof implementation to `lean-implementation-hard-agent` subagent with per-phase dispatch context. **IMPORTANT**: This skill implements the skill-internal postflight pattern. After the subagent returns, this skill handles all postflight operations (status update, artifact linking, sorry_inventory propagation, git commit) before returning. Hard mode activates H2 (anti-analysis with formal proof line bar) and H9 (sorry inventory tracking with orchestrator handoff JSON at every dispatch). Cost is approximately 3-5x standard lean4 implementation. ## Trigger Conditions This skill activates when: - Task type is "lean4" or "lean" (either accepted) - `/implement N --hard` is invoked for a lean4 task - Dispatched from `skill-orchestrate`'s hard-mode per-phase dispatch (H1) branch — the formerly-separate standalone hard-mode engine that used to own this dispatch is deleted and merged into `skill-orchestrate` itself - Routed by `command-route-skill.sh` via `routing_hard.implement.lean4` --- ## Execution Flow ### Stage 1: Input Validation Validate required inputs: - `task_number` - Must be provided and exist in state.json - Task status must allow implementation (planned, implementing, partial) - Task type must be lean4/lean ```bash # Lookup task task_data=$(jq -r --argjson num "$task_number" \ '.active_projects[] | select(.project_number == $num)' \ specs/state.json) # Validate exists if [ -z "$task_data" ]; then return error "Task $task_number not found" fi # Extract fields task_type=$(echo "$task_data" | jq -r '.task_type // "general"') status=$(echo "$task_data" | jq -r '.status') project_name=$(echo "$task_data" | jq -r '.project_name') # Validate task_type (accept both "lean" and "lean4") if [ "$task_type" != "lean" ] && [ "$task_type" != "lean4" ]; then return error "Task $task_number is not a Lean task (got: $task_type)" fi # Check terminal states if [ "$status" = "completed" ] || [ "$status" = "abandoned" ] || [ "$status" = "expanded" ]; then return error "Task $task_number is in terminal state: $status" fi ``` --- ### Stage 1.5: Hard-Mode Cost Note Before proceeding, emit the cost note for session tracking: ``` [hard-mode] skill-lean-implementation-hard activated (session flag: hard) Cost multiplier: ~3-5x standard lean4 implementation Behavioral contracts: H2 (formal proof line bar), H9 (sorry inventory tracking) Per-phase dispatch: each agent invocation handles exactly one plan phase ``` --- ### Stage 2: Preflight Status Update Update task status to "implementing" BEFORE invoking subagent. ```bash bash .claude/scripts/update-task-status.sh preflight "$task_number" implement "$session_id" ``` ```bash # WARN-only: reports lean-lsp MCP registration drift without blocking dispatch. if [ -x .claude/scripts/lean-mcp-preflight-check.sh ]; then bash .claude/scripts/lean-mcp-preflight-check.sh || true fi ``` --- ### Stage 3: Plan Resolution and Phase Identification Find the latest plan file and identify the next incomplete phase for per-phase dispatch: ```bash # Find latest plan padded_num=$(printf "%03d" "$task_number") # Absolute anchor handed to the dispatched agent. SKILL_REPO_ROOT is exported by skill-base.sh # when sourced; $(pwd) is a last-resort fallback for direct invocation. task_dir_abs="${SKILL_REPO_ROOT:-$(pwd)}/specs/${padded_num}_${project_name}" handoff_path_abs="${task_dir_abs}/.orchestrator-handoff.json" plan_file=$(ls "specs/${padded_num}_${project_name}/plans/"*.md 2>/dev/null | sort -V | tail -1) if [ -z "$plan_file" ]; then return error "No plan file found for task $task_number" fi # Read plan to find next incomplete phase. Sourced from the shared anchor # (scripts/lib/phase-heading-patterns.sh) rather than re-derived inline -- this also gains # decimal sub-phase support (e.g. "Phase 3.1"), which the prior digits-only pattern never had. # # Leaf-worker posture (the same posture core's own standalone hard-mode implementer skill once # had in its Stage 3b, before it was merged into skill-orchestrate and deleted): this check runs # strictly before any Agent tool dispatch, so no handoff write is owed here, and adopts this # file's own `return error` convention rather than a raw `exit`. . .claude/scripts/lib/phase-heading-patterns.sh phase_number="" phase_scan_inconclusive=false # --- resume-scan-conformance-gate:begin --- # Whole-file conformance check BEFORE the filtered scan below. PHASE_HEADING_ERE admits # conforming headings only, so a non-conforming heading is not merely unmatched by that grep -- # it is INVISIBLE to it, and the scan would silently select the next conforming OPEN heading # instead, dispatching out of order on top of unfinished work. has_nonconforming_phase_headings # is the required boolean predicate; the `nonconforming_phase_headings | grep -q .` pipe form is # forbidden (unsafe under pipefail). if has_nonconforming_phase_headings "$plan_file"; then warn_nonconforming "$plan_file" "lean-implementation-hard-next-phase" || true phase_scan_inconclusive=true else # Extract phase number via the library's extract_phase_number rather than the prior PCRE-based # lookbehind extraction -- the PCRE grep flag is not available on every platform and was a # second, unnecessary divergence from every other consumer of this grammar. next_phase_heading=$(grep -E "${PHASE_HEADING_ERE} .*${PHASE_STATUS_OPEN_ERE}" "$plan_file" | head -1) if [ -n "$next_phase_heading" ]; then phase_number=$(extract_phase_number "$next_phase_heading") || phase_number="" if [ -z "$phase_number" ]; then # Defense-in-depth only, and unreachable by construction: the grep above already # guarantees this line matches PHASE_HEADING_ERE. Funnelled into the same sentinel so # there is exactly one inconclusive path, never a second silent one. phase_scan_inconclusive=true fi fi fi # --- resume-scan-conformance-gate:end --- if [ "$phase_scan_inconclusive" = "true" ]; then return error "Non-conforming phase heading(s) found during resume-scan -- the filtered scan cannot see them, so the resume point is UNKNOWN. Refusing to guess. See the named, line-numbered warning above." fi # Read handoff for per-phase dispatch context (territory, continuation_context) handoff_file=$(ls "${handoff_path_abs}" 2>/dev/null | head -1) territory=null continuation_context=null if [ -f "$handoff_file" ] && jq empty "$handoff_file" 2>/dev/null; then territory=$(jq -c '.territory // null' "$handoff_file") continuation_context=$(jq -c '.continuation_context // null' "$handoff_file") # Import sorry_inventory from previous handoff for propagation prev_sorry_inventory=$(jq -c '.sorry_inventory // []' "$handoff_file") fi ``` --- ### Stage 4: Prepare Delegation Context Prepare delegation context for the subagent with per-phase dispatch parameters: ```json { "session_id": "sess_{timestamp}_{random}", "delegation_depth": 1, "delegation_path": ["orchestrator", "implement", "skill-lean-implementation-hard"], "timeout": 7200, "effort_flag": "hard", "compare_flag": {true|false}, "task_context": { "task_number": N, "task_name": "{project_name}", "description": "{description}", "task_type": "lean4" }, "plan_path": "specs/{N}_{SLUG}/plans/MM_{short-slug}.md", "phase_number": {N_or_null}, "territory": {territory_or_null}, "continuation_context": {continuation_context_or_null}, "metadata_file_path": "specs/{N}_{SLUG}/.return-meta.json", "task_dir": "{ABSOLUTE path to the task directory}", "handoff_path": "{ABSOLUTE path the agent MUST write its handoff to}", "dispatch_seq": "{dispatch_seq from this skill's own delegation context, forwarded unchanged; omit if absent}" } ``` **Forward `dispatch_seq` unchanged.** If this skill's own delegation context carries a `dispatch_seq` field, forward it into the sub-agent's delegation context above verbatim — the same pass-through treatment already given to `territory` and `handoff_path`. Never invent, increment, or recompute a value at this layer; only the orchestrator mints one. If absent, omit the field. See `context/patterns/dispatch-report-not-termination.md`. **Forward `compare_flag` unchanged, and never let it replace `effort_flag`.** `compare_flag` is forwarded from this skill's own delegation context unchanged and defaults to `false` when absent, composing with `"effort_flag": "hard"` above rather than competing with it — both fields are present together whenever `--compare --hard` was passed. It gates the subagent's advisory Comparator step (see Stage 5 below). --- ### Stage 5: Invoke Subagent **CRITICAL**: You MUST use the **Agent** tool to spawn the subagent. **Required Tool Invocation**: ``` Tool: Agent (NOT Skill, NOT Plan) Parameters: - subagent_type: "lean-implementation-hard-agent" - model: "opus" - prompt: [Include task_context, delegation_context, plan_path, phase_number, territory, continuation_context, metadata_file_path, handoff_path] - description: "Execute hard-mode Lean implementation for task {N} phase {P}" ``` **DO NOT** use `Skill(lean-implementation-hard-agent)` - this will FAIL. The subagent will: - Apply H2 anti-analysis contract (formal proof line bar within 30% of tool calls) - Apply H9 wrap-up discipline (sorry_inventory in every dispatch end) - Implement ONLY the specified phase (per-phase focus) - Use lean_goal before and after each tactic application - Use lean_multi_attempt before applying edits - Run final verification (sorry check, axiom check, lake build — detached, via the build guard, see `context/project/lean4/operations/long-builds.md`) - Write the orchestrator handoff (with sorry_inventory) to the ABSOLUTE path given as `handoff_path` in the delegation context — never a bare `.orchestrator-handoff.json` filename - Create implementation summary - Run the advisory Comparator gate against the snapshot Challenge and the implemented Solution when `compare_flag` is `true` (no-op, no cost, when absent or `false`) - Write metadata to `specs/{N}_{SLUG}/.return-meta.json` - Return a brief text summary (NOT JSON) --- ### Stage 5b: Self-Execution Fallback **CRITICAL**: If you performed the work above WITHOUT using the Agent tool, you MUST write a `.return-meta.json` file now before proceeding to postflight. If you DID use the Agent tool, skip this stage. --- ## Postflight (ALWAYS EXECUTE) ### Stage 6: Parse Subagent Return Read the metadata file: ```bash metadata_file="specs/${padded_num}_${project_name}/.return-meta.json" if [ -f "$metadata_file" ] && jq empty "$metadata_file" 2>/dev/null; then status=$(jq -r '.status' "$metadata_file") artifact_path=$(jq -r '.artifacts[0].path // ""' "$metadata_file") phases_completed=$(jq -r '.metadata.phases_completed // 0' "$metadata_file") phases_total=$(jq -r '.metadata.phases_total // 0' "$metadata_file") # Read verification results (agent is responsible for verification) verification_passed=$(jq -r '.verification.verification_passed // false' "$metadata_file") sorry_count=$(jq -r '.verification.sorry_count // 0' "$metadata_file") # Read sorry_inventory from agent output sorry_inventory=$(jq -c '.sorry_inventory // []' "$metadata_file") else echo "Error: Invalid or missing metadata file" status="failed" verification_passed="false" sorry_inventory="[]" fi ``` --- ### Stage 6a: Plan Compliance Check (Read from Metadata) **This stage only runs if status from metadata is "implemented".** Read the agent-reported compliance result from metadata: ```bash if [ "$status" = "implemented" ]; then compliance_check=$(jq -r '.metadata.compliance_check // "skipped"' "$metadata_file" 2>/dev/null) case "$compliance_check" in "failed") echo "Stage 6a: Plan compliance check FAILED (agent reported)" status="partial" ;; "passed") echo "Stage 6a: Plan compliance check PASSED" ;; "skipped"|*) echo "Stage 6a: INFO — compliance_check absent or skipped; proceeding" ;; esac fi ``` --- ### Stage 6b: Sorry Inventory Propagation After agent returns, propagate sorry_inventory to `.orchestrator-handoff.json`: ```bash handoff_file="${handoff_path_abs}" if [ -f "$handoff_file" ] && jq empty "$handoff_file" 2>/dev/null; then # Merge with previous sorry_inventory (prev + new — resolved) # The agent writes the authoritative sorry_inventory to the handoff JSON echo "Stage 6b: sorry_inventory propagated via agent handoff JSON" echo " Current sorry count: $(echo "$sorry_inventory" | jq 'length')" else echo "Stage 6b: WARNING — no .orchestrator-handoff.json found" echo " Agent should have written this file. Check agent output." fi ``` ---