logic-review – skill Lập trình cho agent AI

Supporting material availability

This catalog copy contains the inline guidance below, but does not include the following supporting paths. They are external prerequisites, not bundled files:

• <support-root>/scripts/grade-iteration.py

Obtain the required material from the [declared upstream source](https://github.com/hyhmrright/logic-lens), or from a user-provided installation of that source. Resolve each path relative to that installation, inspect its contents, and verify any applicable license and execution prerequisites. Do not run a command or claim a referenced procedure was followed until its required file exists. Do not fabricate the missing scripts or treat an unrelated file with the same name as equivalent. Independent steps fully documented here can proceed within the user’s authorized scope; report any dependent step as unavailable.

Logic-Lens — Logic Review

When to Use

Use this skill when you need find logic bugs in a single file or function via semi-formal execution tracing (Premises → Trace → Divergence → Trigger → Remedy). Trigger when a user shares code and suspects something is wrong without naming a concrete failure — phrases like "review this", "does this look right",...

Output Skeleton Contract

The downstream grader (scripts/grade-iteration.py) and other Logic-Lens skills consume this report by substring-matching literal tokens defined in ../_shared/common.md §1 (header map), §2 (mandatory field labels + Logic Score), and ../_shared/report-template.md (skeleton). Paraphrasing those tokens — even with a synonym that reads fine to a human — breaks the contract regardless of analysis quality.

Three failure modes observed in benchmark that deserve specific callout beyond the general rule:

• Synonym substitution for field labels whose substituted form omits the required substring — replacing Premises / 前提 with 前置条件构建 / 前置条件 (eval-201), or Divergence / 偏差 with 根因 / 核心缺陷 / 结论 (eval-252). Each substitution reads fine to a human and may even appear as a section heading or table column, but the substituted word does NOT contain the required substring, so grader and cross-skill consumers see the document as missing the field entirely. Use the literal token from common.md §1; you can still add a descriptive subtitle alongside it.
• Demoting a confirmed L-code finding to ### 附加观察（非 Finding） / ### Additional observation — if Premises→Trace→Divergence holds, the finding belongs inside ## Findings with the five literal fields, even at Suggestion severity. This was a recurring cause of eval-279 (quicksort L4) failing on Sonnet runs.
• Omitting Divergence: / 偏差： field entirely — the single most frequent failure mode. Many outputs correctly analyze the bug but write the divergence as prose, in a table cell, or under headings like 根因, 故障点, 核心问题, 缺陷. The Divergence: field is the specific label for "the point where actual behavior diverges from the premise." It is NOT optional and has no acceptable synonym. For no-bug findings use Divergence: None — [why the premise holds] (中文 偏差：无——[原因]).

Correctly formatted finding — use as template:

### 🔴 Critical
**[L4] — Mutation during iteration skips elements**
Premises: `users` is `list[User]` passed by reference; `list.remove()` shifts subsequent elements left; the `for` iterator advances by index.
Trace: [1] index=0, user is inactive → `remove()` shifts list. [2] Iterator advances to index 1, which now holds the element originally at index 2 — the original index-1 element is skipped. Rebuttal check: PASSED — no defense found.
Divergence: `remove_inactive([inactive₁, inactive₂, active])` returns `[inactive₂, active]` (2 elements) instead of `[active]` (1 element) — the second inactive user is never visited.
Trigger: `remove_inactive([User(False), User(False), User(True)])` → expected 1, actual 2.
Remedy: Replace loop body with `return [u for u in users if u.is_active]`. Dry-run: ✅ divergence eliminated.

Each finding block MUST contain all five literal labels (Premises: / Trace: / Divergence: / Trigger: / Remedy: or 前提： / 追踪： / 偏差： / 触发： / 修复：) as line-starting prefixes. Section headers (### Premises, ## Execution Trace) do NOT satisfy this requirement — the labels must appear inside the finding block.

No-bug case: emit ## Findings with a finding block that uses all five field labels, with Divergence: None — [why the premise holds]. This format is REQUIRED — it satisfies both grading and auditing. Example:

### ✅ No Bug
**[No Bug] — defer guarantees unlock on all exit paths**
Premises: `mu.Lock()` acquired at line 12; `defer mu.Unlock()` placed at line 13 (before any conditional branch or early return).
Trace: [1] `defer` registered immediately after `Lock()`. [2] Go deferred calls run on ordinary returns and panic unwinding; os.Exit, process termination and non-terminating paths do not execute defers. [3] No conditional branch between Lock and defer registration.
Divergence: None — `defer mu.Unlock()` placed unconditionally after acquire releases the lock on the traced returns/panic paths; process exit and non-termination remain outside that claim.
Trigger: N/A (no bug to reproduce).
Remedy: N/A (code is correct as written).

The ../_shared/*.md files referenced below are not bundled either. Their grader/template compatibility cannot be claimed here; use the inline five-field format for an independent review and report that limitation. Never execute the code under review by importing it merely to trace it.

Setup

Use lazy loading per ../_shared/common.md §13:

1. Read ../_shared/common.md only for language, Iron Law, Logic Score, scope management, Remedy discipline, config fields, and loading budget.

2. Read only the relevant step in logic-review-guide.md as you reach it.

3. Load ../_shared/logic-risks.md, ../_shared/semiformal-guide.md, ../_shared/semiformal-checklist.md, and ../_shared/report-template.md on demand when the current step needs them.

Process

Step 0. Language + scope routing. Detect the user's language per common.md §1; every label and header below must be in that language. Confirm scope is one file or one function — if the user points at a directory, switch to logic-health; if they describe a confirmed failure, switch to logic-locate; if two versions, logic-diff.

Step 1. Establish claimed behavior + review entry points (guide Step 1) — write one sentence describing what the code is supposed to do, then select the concrete entry function(s) that will be traced. If a file exceeds common.md §9 limits, state the selected subset and why.

Step 2. Build premises (guide Step 2) — per the Premises Construction Checklist in semiformal-checklist.md; include caller/callee contracts when the reviewed function depends on another local function.

Step 3. Build the risk path ledger (guide Step 3) — enumerate candidate bug paths across L1–L9 before writing findings. Tag each retained path as Class A (self-evident) or Class B (invariant-dependent). Do not stop after the happy path. Read logic-risks.md Quick Disambiguation Table before assigning any L-code — common misclassifications are catalogued there. L4 priority check: does mutation plus returning the same object violate an established caller/API contract? Intentional in-place APIs are valid. L7 priority check: is shared state accessed across await/yield/thread boundaries without explicit synchronization? L4 vs L7 disambiguation: any state access involving more than one execution context (thread / goroutine / await / yield) is L7, never L4 — including single-threaded asyncio where coroutines interleave at await. L4 is for single-context aliasing only (mutable defaults, in-place mutation footgun, mutation-during-iteration). L4 requires an actual mutation of shared/aliased state as the root cause — variable scoping issues (const/let visibility, constructor scope) are L1, and query-pattern inefficiencies (N+1) are L3.

L1 vs L6 disambiguation: if the root cause is a name/identifier resolving to a different definition than the developer expected (import shadowing, module constant lookup, prototype chain, constructor-scoped const/let not visible to methods), it is L1 even when the symptom is a missing-method error or wrong return value — L6 applies only when the name resolves correctly but the callee's behavior differs from what the caller assumed.

L2 vs L6 disambiguation: if the root cause is an implicit type coercion at the operator level (+/-/*/== triggering string↔number conversion, or as/cast bypassing runtime type checks), it is L2 — L6 requires calling a specific callee whose behavior differs from the caller's assumption. Operators are not callees.

L5 vs L7 disambiguation: if an error code, exit status, or exception is suppressed by a single-context construct (|| true, emp

… (nội dung đầy đủ có trong gói tải về)