Skip to content

fix(semantics): close three producer-scan answers that were confidently wrong - #4687

Merged
huangruiteng merged 2 commits into
loopx-project:mainfrom
songoow:codex/b2-counterexamples-and-soundness
Sep 18, 2026
Merged

huangruiteng merged 2 commits into
loopx-project:mainfrom
songoow:codex/b2-counterexamples-and-soundness

Conversation

@songoow

@songoow songoow commented Sep 18, 2026

Copy link
Copy Markdown
Contributor

Supersedes the reduction approach in #4664. That PR's implementation reached main through #4682, so its branch would now revert merged work; what survived review was its counterexample suite, which is carried here and is what found these three holes.

Why the direction matters

F1 proves Produced_scan(v) ⊆ S(v). The dangerous error is therefore a value the scan cannot see — an unregistered value then passes the gate. Over-reporting can only raise a false alarm. Each case below was a missing value delivered inside a complete-looking set.

I ran the suite against main before writing anything: 16 of 20 passed, 4 failed. Three of the four are genuine under-approximations, fixed here. The fourth is the test being stricter than soundness requires, relaxed rather than removed.

The three holes

Shape main reported Truth
global pick; pick = other elsewhere, then pick() {run} confident unknown
dict mutated by subscript, then {**overrides} {run} confident drop
function emit(String) { …String("run")… } {run} confident unknown

global was invisible. _module_functions walks tree.body and enters no function body, so a global rebinding — which lives inside one — never counted as a second binding of the name, and a same-module call still resolved to the original def for a name the module swaps at runtime.

** replayed a stale initializer. bound follows plain name = expression writes only, so a dict mutated afterwards through a subscript still resolved to its initializer. The per-key union lookup applies is unreachable through a spread, which contributes every key at once, so a spread of a mutated container now takes the unknown-key answer.

The TypeScript scanner has no scope model. Any identifier spelled String read as the builtin conversion, any undefined as the literal. Shadowing is now detected per file — coarser than per scope, and deliberately: file granularity can only withhold a builtin reading, never invent one. The genuine builtin still resolves (verified).

The relaxed test

A literal non-negative subscript write is modelled, and the read resolves to the union of the initializer and the write. Demanding unresolved there pinned a weaker scan in place, so the assertion now states the property that matters: the reported set may over-approximate but must never omit the written value. The test's old comment claimed "this scan does not model container mutation at all", which was true of the reduction, not of main.

No budget moves

unresolved_producer_sites is 40 before and after. No site in the tree exercises these shapes today, so this removes a way for a future edit to pass the gate rather than a current violation — and it needs no budget, floor or anchor change.

Verification

Gate Result
pytest tests/architecture/ 526 passed
test_semantic_producer_binding.py 72 passed (was 62 on main)
semantic-vocabulary-drift-smoke.py ok — unresolved 40, blockers unchanged
docs-governance-smoke.py ok
canary premerge --from-git-diff ok — direct / catalog / risk / boundary all 0 failures

What this does not establish

No cross-module data flow is modelled. File-granular shadow detection will withhold the builtin reading from a file that shadows String in an unrelated function. Both are conservative failures, and both are recorded in the RFC rather than assumed away.

Refs #4447

🤖 Generated with Claude Code

…ly wrong

F1 proves production is a subset of what is registered, so the dangerous error
is a value the scan cannot see: an unregistered value then passes the gate.
Over-reporting can only raise a false alarm. Each case here was a *missing*
value delivered inside a complete-looking set.

- `_module_functions` walks `tree.body` and enters no function, so a
  `global pick; pick = other` elsewhere in the module never counted as a second
  binding and a same-module call still resolved to the original `def`. A name
  some scope declares `global` and then stores is now disqualified.
- `bound` follows plain `name = expression` writes, so a dict mutated afterwards
  through a subscript still resolved to its initializer and `{**overrides}`
  reported the key's original value. A spread contributes every key at once, so
  the per-key union is unreachable there; a spread of a mutated container now
  takes the unknown-key answer.
- The TypeScript scanner has no scope model, so any identifier spelled `String`
  read as the builtin conversion and `function emit(String)` produced a
  confident value. Shadowing is detected per file, which is coarser than per
  scope and deliberately so: it can only withhold a builtin reading, never
  invent one.

`unresolved_producer_sites` is 40 before and after: no site in the tree
exercises these shapes today, so no budget, floor or anchor moves. The ten
counterexample tests carry over from the B2 review, six of which already passed
and now stay pinned. The subscript-write case is relaxed rather than removed: a
literal non-negative store is modelled, and demanding `unresolved` there pinned
a weaker scan in place, so it now asserts that the reported set may
over-approximate but must never omit the written value.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: song <22676124+songoow@users.noreply.github.com>
Appendix A append cluster in both mirrors; both sides kept, ours first, nothing
removed from main's version. None of the seventeen commits main added since this
branch started touch the producer scanner, so the three soundness fixes apply
unchanged; the counterexamples are re-run on the merged tree.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Signed-off-by: song <22676124+songoow@users.noreply.github.com>

@huangruiteng huangruiteng left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

动机

F1 证明的是 Produced_scan(v) ⊆ S(v),所以危险的错误方向只有一个:扫描器看不见的值——它会把一个未注册的值当成"已核查通过"。这个 PR 关掉的正是三处"扫描器答得很有信心、但证据不支持"的形状:

  1. 模块级 def pick 被函数体里的 global pick; pick = other 重新绑定后,调用点仍被绑定到那个 def
  2. 构造后被下标改写过的 dict,经 {**overrides} 展开时仍按初始字面量给出取值;
  3. TypeScript 里被参数遮蔽的 String / undefined,仍被当成内建转换/空值。

作者同时说明:它取代 #4664 的缩减路线(该分支的实现已通过 #4682 进入 main,继续合并会回退已落地的内容),带来的是那条路真正留下的反例套件——也就是发现这三个洞的东西。

改动思路

  • Python 绑定_module_functions 原本只看模块级语句,于是函数体里的 global 重绑定对它是隐形的。新增 _enclosing_scope + _stores_name,把"某个作用域声明 global 并真的写入该名字"也算作一次绑定占用,使该名字不再被绑定到 def
  • Python 展开flatten** 展开只跟随 name = expression 形式的写入,所以"构造后经下标改写"的容器会重放过期字面量。新增守卫:展开操作数是出现在 written 里的名字时,整个取值退回"未知键"答案——这正是该函数 docstring 早已写明的规则。
  • TypeScript 遮蔽:扫描器没有作用域模型。新增按文件收集被绑定的名字集合(参数、变量声明、解构绑定、函数/类声明、import),一旦文件里出现 String/undefined不再把它们读成内建。这一方向只能收回一个读数,永远不会凭空造出一个值。

具体改动

关键代码讲解

  • loopx/semantics/python_production.py_enclosing_scope / _stores_name 两个小助手 + bound[name] += 1 守卫;flatten 内新增 if isinstance(candidate, ast.Name) and candidate.id in written: return None
  • scripts/semantic_production_scan.mjsshadowedGlobals 集合与 values() / reads() 里的两个 !shadowedGlobals.has(...) 判断。
  • tests/architecture/test_semantic_producer_binding.py:+174 行,覆盖循环回边(for/while/内外层/finally 四种写法)、两种下标写入(含 codes[-1]codes[0]可接受答案界定)、构造后改写的 dict 展开、global 重绑定、TS 参数遮蔽 String,以及五类 unresolved 各自的原因标签与跨运行时标签一致性。

我特别认可其中两处测试写法

  • test_a_subscript_write_is_never_read_as_the_untouched_container 用的是健全性判据("未解析"或"取值包含写入后的值"都算通过),而不是把更弱的扫描钉死;
  • test_a_field_named_keyword_stays_unproved_even_when_its_value_is_known 明确写出"值可解 ≠ 角色可证",并指出要收窄这个桶只能靠 registry 里 call_producers 这类审阅者看得见的数据改动,而不是更聪明的扫描器。

我实跑的证据(exact head e4dcb009

pytest tests/architecture/test_semantic_producer_binding.py \
       tests/architecture/test_semantic_production.py \
       tests/architecture/test_semantic_python_production.py -q     → 181 passed in 20.24s
python examples/semantic-vocabulary-drift-smoke.py                  → ok
  token 预算未动:work_lane_contract.py=29/29、goal_boundary.py=30/30、
                 external_evidence_observation.py=8/8
  unresolved_producer_sites=40(与 main 相同)
  标签分布:annotation_only=5,argument_name_only=10,attribute_read=7,
            call_result=14,other=1,unstable_local=3

三处改动方向都是减少扫描器声称知道的东西,所以"未改动的树开始挂预算"这条风险在本轮不成立——smoke 的预算与残量数字都没变,这也正是我想先确认的。

对主干的风险

一条 P2(非阻塞,但需要你在合并动作上配合)

[P2] #4664 还在队列里、且被我标为 merge-ready,但它的分支现在已经与 main 冲突、合并会回退已落地内容。 我在本地做了 merge 分析:

git merge-tree --write-tree --name-only origin/main origin/pr-4664
  → CONFLICT (content): docs/.../semantic-vocabulary-convergence-v0.md
  → CONFLICT (content): docs/.../semantic-vocabulary-convergence-v0.zh-CN.md
  → CONFLICT (content): loopx/semantics/python_production.py
git diff origin/main..origin/pr-4664 -- loopx/semantics/python_production.py
  → 该分支删除了 main 当前的 blocker taxonomy docstring

也就是说本 PR 作者的说法与本地证据一致:#4664 应作为"已被取代"关闭,而不是合并。我没法自己关它(那属于合并/仓库动作),所以把这条记在这里。

两条 P3(方向保守,但会多报):

  1. 展开守卫不比较位置written 按名字收集、不筛位置,所以"展开之后才发生的下标写入"也会让该处变成未知(flatten 其他分支的 bound() 是会比较 lineno/col_offset 的)。新增测试只覆盖了"先写后展开",建议要么复用位置比较,要么补一条"写在后"的用例把这个行为显式定下来。
  2. _enclosing_scope 取的是最外层作用域ast.walk 先命中外层函数,_stores_name 又会走遍其子树,于是"内层函数声明 global、外层函数写入"也会被当成不可绑定。方向仍保守,但报出的原因可能指向一个实际不存在的障碍。

两者都只影响残量读数的保守度,不影响健全性,因此不阻塞。

我的整体评价

这是"把信心收回到证据以内"的改动,方向和判据都对:F1 的下界性质决定了唯一致命错误是"漏",所以三处都改成"未解析 + 具名原因",而且测试用的是健全性判据而不是把更弱的实现钉死。反例套件(循环回边、两种下标、构造后改写、global 重绑定、TS 遮蔽)明显比生产改动更大——对这个门禁来说这是健康的比例:证据比代码更贵

我实跑确认预算与残量没变、181 条聚焦测试通过;合并顺序上唯一要你配合的是把 #4664 关成 superseded,不要与它一起合并。

English verdict: APPROVE - head e4dcb00 closes three shapes in which the producer scan answered confidently while its evidence could not support the answer (a module-level def rebound through a global store stayed bound, a dict mutated after construction was still read from its literal through a ** spread, and a TypeScript parameter shadowing String/undefined was still read as the builtin), and every change moves a site from "resolved" to "unresolved with a named reason", which for an F1 lower-bound gate is the only safe direction; I verified it by running the focused suites (181 passed in 20.24s) and the drift smoke (ok, unchanged token budgets and the same 40 unresolved producer sites), and by reading the new counterexample tests, which pin the unknown rather than a weaker scan's output (the subscript test accepts either "unresolved" or "includes the written value", and the field-named-keyword test states that narrowing that bucket needs a registry data edit a reviewer can see); three non-blocking notes remain - the spread guard is order-insensitive so a dict written after the spread also loses a correct answer (P3), _enclosing_scope returns the outermost scope so a nested global also suppresses the outer function's stores (P3), and, more importantly for merge order, PR #4664 is still open and listed as merge-ready while git merge-tree shows its branch conflicting with main in python_production.py and both RFC mirrors and reverting main's current docstring, so it should be closed as superseded rather than merged (P2).

@huangruiteng
huangruiteng merged commit ac604a2 into loopx-project:main Sep 18, 2026
22 of 23 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants