fix(semantics): close three producer-scan answers that were confidently wrong - #4687
Conversation
…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
left a comment
There was a problem hiding this comment.
动机
F1 证明的是 Produced_scan(v) ⊆ S(v),所以危险的错误方向只有一个:扫描器看不见的值——它会把一个未注册的值当成"已核查通过"。这个 PR 关掉的正是三处"扫描器答得很有信心、但证据不支持"的形状:
- 模块级
def pick被函数体里的global pick; pick = other重新绑定后,调用点仍被绑定到那个def; - 构造后被下标改写过的 dict,经
{**overrides}展开时仍按初始字面量给出取值; - 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.mjs:shadowedGlobals集合与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(方向保守,但会多报):
- 展开守卫不比较位置:
written按名字收集、不筛位置,所以"展开之后才发生的下标写入"也会让该处变成未知(flatten其他分支的bound()是会比较lineno/col_offset的)。新增测试只覆盖了"先写后展开",建议要么复用位置比较,要么补一条"写在后"的用例把这个行为显式定下来。 _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).
Supersedes the reduction approach in #4664. That PR's implementation reached
mainthrough #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
mainbefore 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
mainreportedglobal pick; pick = otherelsewhere, thenpick(){run}confident{**overrides}{run}confidentdropfunction emit(String) { …String("run")… }{run}confidentglobalwas invisible._module_functionswalkstree.bodyand enters no function body, so aglobalrebinding — which lives inside one — never counted as a second binding of the name, and a same-module call still resolved to the originaldeffor a name the module swaps at runtime.**replayed a stale initializer.boundfollows plainname = expressionwrites only, so a dict mutated afterwards through a subscript still resolved to its initializer. The per-key unionlookupapplies 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
Stringread as the builtin conversion, anyundefinedas 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
unresolvedthere 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 ofmain.No budget moves
unresolved_producer_sitesis 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
pytest tests/architecture/test_semantic_producer_binding.pysemantic-vocabulary-drift-smoke.pydocs-governance-smoke.pycanary premerge --from-git-diffWhat 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
Stringin an unrelated function. Both are conservative failures, and both are recorded in the RFC rather than assumed away.Refs #4447
🤖 Generated with Claude Code