Logic Review

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 spec guarantees deferred calls execute on ALL function exit paths (return, panic, early return). [3] No conditional branch between Lock and defer registration.
Divergence: None — `defer mu.Unlock()` placed unconditionally after acquire guarantees release on every exit path; no lock leak possible.
Trigger: N/A (no bug to reproduce).
Remedy: N/A (code is correct as written).

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 any function mutate its input AND return the same object? 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, empty catch, missing set -e, bare except), it is L5 (control flow escape) — L7 requires multiple execution contexts. Error propagation failure within one sequential script/function is L5.

L9 check: if the bug's root cause is timezone/locale/encoding information lost at the data-type level (e.g., TIMESTAMP vs TIMESTAMPTZ, naive vs aware datetime, locale-dependent string sort), it is L9 — not L6 even if it looks like "callee behavior differs from expectation", not L2, not L8.

Step 4. Deep-trace selected paths (guide Step 4) — trace the normal path plus the highest-risk edge paths; resolve every name, state every type, cross callee boundaries, and stop each trace at either a confirmed divergence or a confirmed safe post-condition. Java/C++ DCL rule: for double-checked locking patterns, MUST trace both faces: (a) missing volatile / memory barrier (visibility hazard) AND (b) instance = new X(); instance.init(); as two non-atomic statements — lock-free readers can see non-null instance before init() completes (publish-before-init hazard). Report both; omitting either is an incomplete analysis.