📦 deps(thirdparty): update snapshots
This commit is contained in:
ci[bot]
@@ -0,0 +1,100 @@
|
||||
---
|
||||
name: logic-review
|
||||
description: 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",...
|
||||
risk: unknown
|
||||
source: https://github.com/hyhmrright/logic-lens/tree/main/skills/logic-review
|
||||
source_repo: hyhmrright/logic-lens
|
||||
source_type: community
|
||||
date_added: 2026-07-01
|
||||
license: MIT
|
||||
license_source: https://github.com/hyhmrright/logic-lens/blob/main/LICENSE
|
||||
---
|
||||
|
||||
# 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.
|
||||
|
||||
**Step 5. Identify divergences** (guide Step 5) — classify each by L1–L9; assign severity; apply the reachability gate (Class A reports directly; Class B requires a probe — enforcement found → drop candidate, not found → assigned severity, partial → cap at Warning with `manual verification recommended`). Apply the correctness parity principle for no-bug scenarios. **No-bug output discipline:** when zero divergences remain, still emit the full template skeleton — Mode line, Scope, `**Logic Score:** 100/100`, `## Findings` followed by a finding block that uses `Divergence: None — [why the premise holds]` (中文 `偏差：无——[原因]`) with all five field labels present. This makes the reasoning auditable and satisfies the format contract. If analysis actively disproves a suspected bug, explain the defense in the `Trace:` field (e.g., "Go `defer mu.Unlock()` guarantees release on all exit paths including early return"). Do not collapse the verdict into free-form prose or omit the structured fields; downstream grading requires the five-field format even for no-bug conclusions.
|
||||
|
||||
**Step 5.5. Adversarial Red Team** (guide Step 5.5) — for each candidate finding, attempt to disprove it by answering three rebuttal questions (premise rebuttal, path rebuttal, consequence rebuttal). Withdraw findings with confirmed defenses; downgrade findings with partial defenses to Suggestion. **Design-intent gate:** before reporting an L3 Boundary Blindspot, ask "Does the code explicitly return an error / rejection at this boundary rather than attempting to continue past it?" If yes (e.g., `errors.New("cache full")` at `maxSize`, `429 Too Many Requests`, buffer-full rejection), withdraw — these are correct boundary enforcement, not blindspots. L3 applies only when code *attempts* to operate past the boundary and silently fails (wrong result, crash, infinite loop). Note: a `panic` at a boundary is a crash, not a designed error return, and remains a potential L3.
|
||||
|
||||
**Step 6. Apply Iron Law — Five-Field Discipline** (guide Step 6) — confirm all findings have Premises → Trace → Divergence complete; then write Trigger (concrete reproducing input, required for Critical/Warning) and Remedy (paste-ready per `common.md` §10). **Each finding MUST use these literal field labels** — English `Premises:` / `Trace:` / `Divergence:` / `Trigger:` / `Remedy:`, or Chinese `前提：` / `追踪：` / `偏差：` / `触发：` / `修复：`. Do not paraphrase. Headers like `Execution Path`, `Issue Found`, `Core Defect`, `执行路径`, `发现的逻辑隐患`, `核心缺陷` are unacceptable substitutes — they fail downstream grading and break the report contract that other Logic-Lens skills consume. **Multi-finding discipline:** When there are multiple findings, each finding block inside `## Findings` must include all five literal field labels — `Premises:` / `Trace:` / `Divergence:` / `Trigger:` / `Remedy:` (or their Chinese equivalents) — with content specific to that finding. Any shared background context may appear as a preamble section, but it does NOT substitute for the per-finding fields. A finding that omits `Divergence:` (or any other required field) breaks the contract even if `Premises:` or `Trace:` appear elsewhere in the report.
|
||||
|
||||
**Step 6.5. Remedy Dry-Run** (guide Step 6.5) — mentally re-trace the Trigger input through the fixed code to confirm: divergence eliminated, no regression introduced, happy path preserved.
|
||||
|
||||
**Step 7. Score and output** (guide Step 7) — compute Logic Score per `common.md` §6 and emit it as the literal line `**Logic Score:** XX/100` (中文 `**逻辑评分：** XX/100`) directly under `**Scope:**` — this exact token (not "Score: XX", not "Quality: XX") is required for both grader recognition and cross-skill consumption. Then render the rest of the Report Template with localized headers.
|
||||
|
||||
**Step 8. Execution Verification Gate** (guide Step 8, optional) — when a runtime is available, generate a minimal reproducer script for each Critical/Warning finding, execute it to confirm the bug exists, apply the Remedy and re-execute to confirm the fix works. Withdraw false positives; mark verified findings as `✅ Execution-verified`.
|
||||
|
||||
**Mode line in report:** `Logic Review` (Chinese: `逻辑审查`).
|
||||
|
||||
## Limitations
|
||||
|
||||
- Use this skill only when the task clearly matches its upstream source and local project context.
|
||||
- Verify commands, generated code, dependencies, credentials, and external service behavior before applying changes.
|
||||
- Do not treat examples as a substitute for environment-specific tests, security review, or user approval for destructive or costly actions.
|
||||
@@ -0,0 +1,296 @@
|
||||
# Logic Review — Step-by-Step Guide
|
||||
|
||||
## Step 1: Establish Claimed Behavior
|
||||
|
||||
Read any comments, docstrings, test names, or commit message. Write one sentence:
|
||||
"This code is supposed to [verb] [what], given [inputs], producing [output/side effect]."
|
||||
|
||||
This sentence is the reference point: anything the trace contradicts is a candidate finding. If no documentation exists, infer intent from the function signature, caller usage, tests, and names. Do not emit a documentation-gap finding unless the missing contract directly prevents a logic conclusion.
|
||||
|
||||
Select the review entry point before tracing:
|
||||
- Single function input: trace that function and any local callees reached from it.
|
||||
- Single file input: identify public/exported functions, functions changed recently, and functions touching external state. If the file exceeds `common.md` §9 limits, choose at most 3 high-risk functions and state the uncovered functions in Scope.
|
||||
- Pasted snippet without line numbers: anchor trace steps to function names and expressions; do not invent line numbers.
|
||||
|
||||
## Step 2: Build Premises
|
||||
|
||||
Run through every applicable item in **`../_shared/semiformal-checklist.md`** — Name Resolution, Type Contracts, State Preconditions, Control Flow Assumptions. Read its "What is NOT a Premise" section before writing.
|
||||
|
||||
Write premises **before** starting the trace.
|
||||
|
||||
**Good premise example:** "`users` is a `list[User]` passed by reference; `users.remove(x)` mutates the list in place; the `for user in users` iterator does not re-index after a mutation, so removing element at position `i` causes element at original position `i+1` to be skipped."
|
||||
|
||||
For logic-review, premises must cover both sides of each important boundary:
|
||||
- **Caller contract:** What values can enter this function from real call sites? If call sites are unavailable, mark this premise as partial.
|
||||
- **Callee contract:** What can each local callee return, raise, mutate, or skip? Trace into local callees when the finding depends on their behavior.
|
||||
- **State lifetime:** Which state survives across calls, iterations, awaits, callbacks, or retries?
|
||||
- **Observable consequence:** What output, mutation, exception, persisted value, or externally visible side effect would make the bug real?
|
||||
|
||||
## Step 3: Build the Risk Path Ledger
|
||||
|
||||
Before writing any finding, enumerate candidate paths. This prevents the review from anchoring on the happy path.
|
||||
|
||||
Create a short internal ledger with one row per path:
|
||||
|
||||
```
|
||||
[risk code] [entry point] [input/state condition] [branch/callee/resource involved] [why this path is reachable or not] [Class A | Class B]
|
||||
```
|
||||
|
||||
Tag each **retained** candidate with a **Reachability Class** (discarded candidates need no tag):
|
||||
- **Class A (Self-evident):** triggering condition is visible in local code — e.g., dereference after explicit nil check, index beyond bounds, unchecked type assertion, resource with no release on a visible exit path.
|
||||
- **Class B (Invariant-dependent):** triggering condition requires an implicit external assumption to be false — e.g., "all groups always contain at least one alias" or "callers never pass nil here." Requires a reachability probe in Step 5 before reporting.
|
||||
|
||||
Example ledger rows:
|
||||
```
|
||||
L3 parseCSV empty input len(rows)==0 guard absent always reachable from callers Class A
|
||||
L5 filterPkgVulns all groups ignored len(newGroups)==0 guard depends on "vuln always in ≥1 group" invariant Class B
|
||||
```
|
||||
|
||||
Minimum ledger coverage:
|
||||
- **Normal path:** the common valid input path.
|
||||
- **Boundary paths (L3):** empty/null/zero, single item, first/last item, max/min, divide/slice/index boundaries.
|
||||
- **Type/name paths (L1/L2):** shadowed identifiers, dynamic dispatch, coercions, nullable values, deserialized input.
|
||||
- **Callee paths (L6):** local callees returning null/None/undefined, raising, mutating arguments, or returning a different shape.
|
||||
- **Control/resource paths (L5/L8):** every early return, throw/raise, catch/except, break/continue after acquisition or required post-condition. **L5 exhaustive enumeration:** when a required side-effect (audit log, metric, notification, state update) must run on every exit, verify EVERY exit path independently — `return`, explicit `raise`/`throw`, implicit raises from callees, `break`, `continue`. Name each skipped path separately in the finding; a finding that identifies only the first skipped path is incomplete. Example: "Two paths skip `audit_log.record`: (1) `return _unauthorized()` at line 3, (2) `raise BadRequest` at line 5." Note: if the skipped operation is a resource release or rollback, reclassify as L8 and apply the same exhaustive path logic there.
|
||||
- **State/concurrency paths (L4/L7):** mutation during iteration, shared mutable defaults, aliases, closures, await/callback/task boundaries. For L4 also check: does the function mutate its argument AND return it (aliased-return dual contract)? For L7: does the hazard require two concurrent execution contexts — if yes it is L7, not L4 (e.g. lock-order inversion between goroutines is L7 even though it involves mutation).
|
||||
- **L4 aliased-return trap (high priority):** When a function BOTH mutates its input in-place AND returns the same object, this is an L4 finding — not a style issue. The caller may write `result = func(original)` and assume `original` is unchanged. Trace: (a) confirm mutation is in-place (e.g., `list.sort()`, `del arr[i]`, `arr[i], arr[j] = arr[j], arr[i]`); (b) confirm the function returns the SAME object (not a copy); (c) construct a Trigger showing `original` is unexpectedly modified. This is L4, not L3 or L7.
|
||||
- **L7 async interleaving (critical for asyncio/coroutines):** When shared mutable state is accessed across `await`/`yield` boundaries, the bug is L7 even if no threads are involved — asyncio coroutines interleave on a single thread via the event loop. Key indicator: a check-then-act pattern with an `await` between the check and the act. Do NOT classify asyncio interleaving as L4.
|
||||
- **L7 memory model hazards (Java/C++/Go):** For double-checked locking, volatile/atomic, happens-before: always check BOTH (a) the visibility hazard (missing volatile/atomic) AND (b) the initialization-before-publish ordering (is the object fully constructed before other threads can see it?). Two-step trace: step 1 = reordering/visibility, step 2 = consequence of observing partially-constructed object.
|
||||
- **Time/locale paths (L9):** naive/aware datetime, DST, locale-sensitive parse/sort/format, implicit encoding.
|
||||
|
||||
Discard a candidate only after stating why it is unreachable or irrelevant. Deep-trace the normal path and the highest-risk reachable candidates first.
|
||||
|
||||
## Step 4: Deep-Trace Selected Execution Paths
|
||||
|
||||
Trace the most common execution path step by step:
|
||||
|
||||
```
|
||||
1. [line N] [expression evaluated] → [result]
|
||||
2. `name` resolves to [full qualified definition] at [file:line]
|
||||
3. Arguments passed: arg1 = [value/type], arg2 = [value/type]
|
||||
4. Inside [callee] at [line]: [key operation] → [result]
|
||||
5. Returns [value/type] to caller at [line]
|
||||
6. [line N+k] Result used as [role]
|
||||
```
|
||||
|
||||
**Minimum thresholds** (per `../_shared/semiformal-guide.md`): ≥ 3 substantive steps and ≥ 2 location anchors. Below either threshold, downgrade the finding to Suggestion with `manual verification recommended`.
|
||||
|
||||
**Good trace example:**
|
||||
```
|
||||
1. [service.py:6] `result = charge(order)` — `charge` resolves to `payments.gateway.charge` (imported at line 1).
|
||||
2. [gateway.py:3] Inside `charge`: condition `order.amount == 0` evaluates to True for this input.
|
||||
3. [gateway.py:4] Returns `None` (early return; no dict constructed).
|
||||
4. [service.py:7] `result['transaction_id']` evaluates `None['transaction_id']` → raises `TypeError`.
|
||||
```
|
||||
|
||||
Then trace each selected risk path separately:
|
||||
|
||||
- Start with concrete input/state values, not abstract phrases like "bad input".
|
||||
- Follow value origin → branch decision → callee behavior → state mutation/output.
|
||||
- For loops, trace zero iterations, one iteration, and the iteration where the invariant changes.
|
||||
- For async/concurrent code, name the exact boundary where another execution context can observe or mutate state.
|
||||
- For **L4 aliased-return mutation**: trace what happens when the caller holds a reference to the input BEFORE the call, calls the function, then uses the original reference. Show that the original was mutated. Example trace:
|
||||
```
|
||||
1. caller: original = [3, 1, 2]
|
||||
2. caller: result = quicksort(original)
|
||||
3. inside quicksort: arr is the SAME object as original (passed by reference)
|
||||
4. quicksort mutates arr in-place via swaps
|
||||
5. quicksort returns arr — same object
|
||||
6. caller: original is now [1, 2, 3] — mutated without caller's knowledge
|
||||
7. caller: result is original — they are the same object (result is original == True)
|
||||
```
|
||||
- For **L7 memory model**: trace two threads/goroutines/coroutines with numbered interleaving steps:
|
||||
```
|
||||
T1-step1: thread A checks instance == null → true
|
||||
T1-step2: thread A enters synchronized, creates object
|
||||
T1-step3: JIT reorders: reference published BEFORE constructor completes
|
||||
T2-step1: thread B checks instance == null → false (sees non-null)
|
||||
T2-step2: thread B returns instance — but object.data is still null
|
||||
```
|
||||
- Stop at a confirmed safe post-condition if the candidate is not a bug; do not turn safe paths into Suggestions.
|
||||
|
||||
## Step 5: Identify Divergences
|
||||
|
||||
For each point where a premise is violated, write a finding using the five-field format (Premises → Trace → Divergence → Trigger → Remedy) with the L-code that best describes the cause.
|
||||
|
||||
**Severity:**
|
||||
- 🔴 Critical: causes exception, data corruption, incorrect output, or security-relevant behavior in a reachable path.
|
||||
- 🟡 Warning: reachable but only under uncommon inputs or a specific sequence of prior operations.
|
||||
- 🟢 Suggestion: requires unusual/currently-impossible conditions, consequence is minor, or one premise is partial.
|
||||
|
||||
For Class A candidates: if the trace does not conclusively confirm consequence (reachability is already self-evident for Class A), downgrade to Suggestion with `manual verification recommended` or omit it. A plausible code smell without a concrete execution path is not a logic-review finding.
|
||||
|
||||
**Reachability gate — apply before writing any finding:**
|
||||
|
||||
- **Class A:** report at the assigned severity (local code is sufficient evidence).
|
||||
- **Class B:** run a reachability probe first:
|
||||
1. Search for invariant enforcement — constructor, validator, schema definition, or call sites visible in current scope.
|
||||
2. Enforcement found and airtight (no code path bypasses it) → **drop the candidate; do not write a finding.** Optionally record in the report Summary: "Invariant enforced at [location] — no current bug; revisit if callers or schema change."
|
||||
3. No enforcement found → report at the assigned severity.
|
||||
4. Enforcement partial or outside current scope → report at the assigned severity, capped at 🟡 Warning, with `manual verification recommended`.
|
||||
|
||||
Record the probe result in the finding's Trace (not Premises) so the reader can verify the class assignment without violating the Premises checklist.
|
||||
|
||||
Deduplicate by root cause: if one bad callee contract creates several caller symptoms, report one L6 finding at the callee/caller contract boundary and list representative call sites in the Trace or Remedy.
|
||||
|
||||
**No-bug discipline:** When the user's question is framed as "does X cause bug Y?" and the trace conclusively shows Y does NOT apply (e.g., `defer` in Go runs on all exit paths so there is no lock leak), write a finding concluding **NO logic error** for Y with Premises → Trace → Divergence showing why. Do not fabricate unrelated findings to appear thorough — that undermines precision and triggers false positives. However, if the Risk Path Ledger from Step 3 surfaced a separate, concrete, reachable bug with a complete trace, report it as an independent finding; a no-bug verdict on Y does not suppress genuine findings on other risks. If the ledger produced no other findings, stop.
|
||||
|
||||
**Correctness parity principle:** Correctly concluding "no bug" is equally valuable as correctly finding a bug. A Logic Score 100 report with "no confirmed logic errors" is a professional, high-value output — not a failure. Do not lower evidence standards to produce findings. If every path in the Risk Path Ledger terminates at a confirmed safe post-condition, output Score 100 immediately. Record each path's safe-termination reason (≥1 sentence) but do NOT wrap safe paths as Suggestion findings.
|
||||
|
||||
## Step 5.5: Adversarial Red Team
|
||||
|
||||
For each candidate finding that survived Step 5, attempt to **disprove it** from the defender's perspective before writing the Remedy. This step reduces false positives by forcing an adversarial check.
|
||||
|
||||
**Three Rebuttal Questions** (answer each explicitly — do not skip):
|
||||
|
||||
1. **Premise rebuttal:** Does any of my premises rest on an unverified assumption? Could callers guarantee the premise through schema validation, type checking, wrapper functions, middleware, or a constructor that enforces the invariant? Search the current scope for evidence.
|
||||
|
||||
2. **Path rebuttal:** Is the trigger path truly reachable in production? Could an upstream guard, configuration flag, middleware filter, type system constraint, or framework convention prevent the input from ever reaching this code path?
|
||||
|
||||
3. **Consequence rebuttal:** Even if the divergence exists, is the consequence truly harmful? Could a downstream defense (catch/except, fallback value, retry logic, idempotency guard) neutralize the impact?
|
||||
|
||||
**Ruling:**
|
||||
- Any question finds **conclusive evidence** (a defense locatable in code) → **withdraw the finding**. Record in Summary: "Candidate [L-code] at [location] withdrawn — defense confirmed at [defense location]."
|
||||
- Any question finds **partial evidence** (indirect defense, uncertain coverage) → **downgrade to Suggestion** with `manual verification recommended`.
|
||||
- All three questions find **no rebuttal evidence** → **retain at original severity**.
|
||||
|
||||
**Async/concurrency protection clause:** For L7 findings involving async interleaving (asyncio, goroutines, coroutines) or memory model hazards (volatile, happens-before), apply stricter rebuttal thresholds — only withdraw if the defense is an **explicit synchronization primitive** (lock, semaphore, atomic, channel, volatile). Do NOT treat the GIL, event loop single-threading, or "unlikely timing" as a defense. The GIL does not prevent asyncio interleaving; single-threaded event loops DO interleave at await points.
|
||||
|
||||
**Recording:** Append the rebuttal conclusion to the Trace field:
|
||||
- `Rebuttal check: PASSED — no defense mechanism found in scope.`
|
||||
- `Rebuttal check: DOWNGRADED — partial defense found at [location].`
|
||||
- `Rebuttal check: WITHDRAWN — confirmed defense at [location].`
|
||||
|
||||
(Chinese: `反驳检查：已通过——范围内未发现防御机制。` / `反驳检查：已降级——在 [位置] 发现部分防御。` / `反驳检查：已撤回——在 [位置] 确认防御。`)
|
||||
|
||||
## Step 6: Apply Iron Law (Five-Field Discipline)
|
||||
|
||||
Premises, Trace, and Divergence must all be complete before writing a **Trigger** or **Remedy**.
|
||||
|
||||
Every finding follows five fields in order: **Premises → Trace → Divergence → Trigger → Remedy**.
|
||||
|
||||
### Trigger field (required for Critical and Warning; optional for Suggestion)
|
||||
|
||||
Provide a **concrete input or state** that triggers the bug. The trigger must be specific enough that a developer can paste it into a REPL or test to reproduce.
|
||||
|
||||
**Good trigger example:**
|
||||
```
|
||||
Trigger: remove_inactive([User(active=False), User(active=False), User(active=True)])
|
||||
Expected: returns [User(active=True)] (1 element)
|
||||
Actual: returns [User(active=False), User(active=True)] (2 elements — second inactive user skipped)
|
||||
```
|
||||
|
||||
**Bad trigger (unacceptable):**
|
||||
```
|
||||
Trigger: "when passing a list with inactive users" ← too vague, cannot reproduce
|
||||
```
|
||||
|
||||
**When a concrete trigger is difficult to construct:**
|
||||
- Bug depends on external state (DB, network): describe the minimal triggering condition + mark `manual verification recommended`.
|
||||
- Bug involves concurrency/timing: describe the specific thread/coroutine interleaving sequence with numbered steps.
|
||||
- Completely unable to construct a trigger: **automatically downgrade to Suggestion**.
|
||||
|
||||
### Remedy field
|
||||
|
||||
**Good remedy example:** "On line 42, replace `format(self.data.year, '04d')` with `builtins.format(self.data.year, '04d')` to avoid dispatching to the module-level `format()` that expects a datetime object."
|
||||
|
||||
## Step 6.5: Remedy Dry-Run Verification
|
||||
|
||||
After writing the Remedy, mentally re-execute the Trigger input against the **fixed** code to confirm correctness. This prevents remedies that are ineffective or introduce regressions.
|
||||
|
||||
**Procedure (3-step minimum):**
|
||||
|
||||
1. **Mentally apply** the Remedy to the original code.
|
||||
2. **Re-trace** the Trigger input through the fixed code (≥3 steps).
|
||||
3. **Confirm** all three conditions:
|
||||
- (a) The original Divergence no longer occurs.
|
||||
- (b) No new Divergence is introduced by the fix (check boundary conditions of the fix itself).
|
||||
- (c) The happy-path behavior is preserved (the fix does not change correct behavior).
|
||||
|
||||
**Outcomes:**
|
||||
- (a) fails → Remedy is ineffective. Rewrite before emitting.
|
||||
- (b) fails → Remedy introduces a regression. Record the new risk, narrow the fix scope, and rewrite.
|
||||
- (c) fails → Remedy is over-scoped. Reduce the fix to the minimal change.
|
||||
|
||||
**Recording:** Append to the Remedy field:
|
||||
```
|
||||
Dry-run: ✅ Trigger input re-traced through fix — divergence eliminated, no regression, happy path preserved.
|
||||
```
|
||||
(Chinese: `预演：✅ 触发输入已在修复代码中重新追踪——偏差已消除，无回归，正常路径行为保持不变。`)
|
||||
|
||||
If dry-run reveals a problem, record the issue and the corrected remedy:
|
||||
```
|
||||
Dry-run: ⚠️ Initial remedy [description] failed check (b) — [new issue]. Revised remedy applied.
|
||||
```
|
||||
|
||||
## Step 7: Compute Score and Output
|
||||
|
||||
1. Start at 100. Deduct per confirmed finding (Critical −15, Warning −7, Suggestion −2).
|
||||
2. Fill in the Report Template from `report-template.md`.
|
||||
3. Summary: most critical finding, recommended next action, whether the logic is safe to ship.
|
||||
|
||||
## Step 8: Execution Verification Gate (Optional — when runtime is available)
|
||||
|
||||
When the environment supports code execution (CLI with shell access, sandbox, or REPL), apply this step to each **Critical** and **Warning** finding. Skip this step entirely if no runtime is available — mark findings as `unverified — no runtime available` and proceed.
|
||||
|
||||
**Prerequisite check:** Detect whether the target language runtime is available (e.g., `python3 --version`, `node --version`, `go version`). If unavailable, skip to output.
|
||||
|
||||
### 8a. Generate Minimal Reproducer Script
|
||||
|
||||
For each finding, generate a self-contained script based on the Trigger field:
|
||||
- Include the reviewed function (or a minimal standalone version).
|
||||
- Include the concrete trigger input from the Trigger field.
|
||||
- Include an assertion: expected behavior vs. actual behavior.
|
||||
- The script must **FAIL** (assertion error or exception) when the bug is present.
|
||||
|
||||
**Safety constraints:**
|
||||
- The script must contain only pure computation — NO network requests, file writes, database operations, or other side effects.
|
||||
- If the function depends on external state, create in-memory mocks/stubs.
|
||||
- Execution timeout: 10 seconds maximum.
|
||||
|
||||
### 8b. Run Original Code (Confirm Bug Exists)
|
||||
|
||||
Execute the reproducer script against the original code.
|
||||
- **Script FAILS (assertion error or expected exception):** Bug confirmed. Proceed to 8c.
|
||||
- **Script PASSES:** Finding is a **false positive**. Withdraw it, remove from report, and adjust Logic Score.
|
||||
- **Script errors unexpectedly (syntax error, import failure):** Script needs fixing. Retry once with corrected script. If still broken, mark `unverified — reproducer generation failed`.
|
||||
|
||||
### 8c. Apply Remedy and Re-run (Confirm Fix Works)
|
||||
|
||||
Apply the Remedy to the code in the reproducer script, then re-execute.
|
||||
- **Script PASSES:** Fix verified. Mark finding as `✅ Execution-verified`.
|
||||
- **Script still FAILS:** Remedy is ineffective. Revise and retry (up to 3 attempts). After 3 failures, mark `unverified — remedy needs manual review`.
|
||||
- **Script throws NEW exception:** Remedy introduces regression. Revert, mark `⚠️ Remedy caused regression — manual fix recommended`.
|
||||
|
||||
### 8d. Update Report
|
||||
|
||||
Add verification status to each finding:
|
||||
|
||||
```
|
||||
Verification: ✅ Execution-verified — reproducer FAIL → applied fix → PASS
|
||||
Verification: ⚠️ Unverified — [reason]
|
||||
Verification: ❌ False positive withdrawn — reproducer PASS on original code
|
||||
```
|
||||
|
||||
(Chinese: `验证：✅ 已执行验证——复现脚本 FAIL → 应用修复 → PASS` / `验证：⚠️ 未验证——[原因]` / `验证：❌ 假阳性已撤回——复现脚本在原始代码上 PASS`)
|
||||
|
||||
**Example reproducer (Python, L4 mutation-during-iteration):**
|
||||
|
||||
```python
|
||||
# 最小可复现脚本 — L4: 迭代中修改列表
|
||||
class User:
|
||||
def __init__(self, active):
|
||||
self.is_active = active
|
||||
|
||||
def remove_inactive(users):
|
||||
for user in users:
|
||||
if not user.is_active:
|
||||
users.remove(user)
|
||||
return users
|
||||
|
||||
# 触发输入：两个连续的失效用户
|
||||
users = [User(False), User(False), User(True)]
|
||||
result = remove_inactive(users)
|
||||
assert len(result) == 1, f"Expected 1 active user, got {len(result)}"
|
||||
# 预期：AssertionError（bug 存在）
|
||||
```
|
||||
Reference in New Issue
Block a user