From 1f477eb0fea642d53219745afb6606d1b3600e8e Mon Sep 17 00:00:00 2001 From: song <22676124+songoow@users.noreply.github.com> Date: Fri, 18 Sep 2026 01:02:07 -0400 Subject: [PATCH] fix(semantics): close three producer-scan answers that were confidently 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) Signed-off-by: song <22676124+songoow@users.noreply.github.com> --- .../semantic-vocabulary-convergence-v0.md | 39 ++++ ...emantic-vocabulary-convergence-v0.zh-CN.md | 30 +++ loopx/semantics/python_production.py | 42 ++++- scripts/semantic_production_scan.mjs | 30 ++- .../test_semantic_producer_binding.py | 174 ++++++++++++++++++ 5 files changed, 311 insertions(+), 4 deletions(-) diff --git a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md index d543ea5012..5288bca007 100644 --- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md +++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md @@ -1142,6 +1142,45 @@ introduce a competing target state. ## Appendix A: Execution ledger (non-normative) +### 2026-09-18 — Three producer-scan answers that were confidently wrong + +Normative for what the producer scan may report as complete. No budget, floor or +anchor moved: `unresolved_producer_sites` is 40 before and after, because no +site in the tree exercises these shapes today. The fixes remove a way for a +future edit to pass the gate, not a current violation. + +- **Why the direction matters.** F1 proves `Produced_scan(v) ⊆ S(v)`, so the + dangerous error is a value the scan does not see: an unregistered value then + passes. Over-reporting can only raise a false alarm. Each case below was a + *missing* value reported inside a complete-looking set. +- **A `global` rebinding was invisible.** `_module_functions` walks `tree.body` + and skips into no function, so `global pick; pick = other` inside another + function never counted as a second binding of `pick`, and a same-module call + still resolved to the original `def`'s returns for a name the module swaps at + runtime. A name some scope declares `global` and then stores is now + disqualified, and the call keeps `call_result`. +- **A `**` spread replayed a stale initializer.** `bound` follows plain + `name = expression` writes, so a dict mutated afterwards through a subscript + still resolved to its initializer. `{**overrides}` therefore reported the + key's original value as the produced one. The per-key union that `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 had no scope model.** Any identifier spelled `String` + was read as the builtin conversion and any `undefined` as the literal, so + `function emit(String)` — a caller-supplied function that can return anything + — produced a confident value. Shadowing is now detected per file, which is + coarser than per scope and deliberately so: file granularity can only withhold + a builtin reading, never invent one. +- **One counterexample was relaxed, not removed.** 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. +- **What this does not establish.** The scan still models no cross-module data + flow, and 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 stay measured rather than assumed. + ### 2026-09-17 — B2: three bounded binding forms, and the residue that stays unresolved - **Trigger:** [#4447](https://github.com/huangruiteng/loopx/issues/4447) recorded diff --git a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md index 6f1e9f21f6..da57acdde6 100644 --- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md +++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md @@ -920,6 +920,36 @@ PR review 保留这些层级。普通改动记录检查范围和理由，无共 ## 附录 A：执行账本（非规范） +### 2026-09-18 — 生产者扫描三处自信而错误的答案 + +对"扫描可以把什么报成完整"是规范性的。没有移动任何预算、下限或锚点： +`unresolved_producer_sites` 修前修后都是 40，因为当前树里没有站点触发这些形状。 +修的是"未来某次改动能蒙过门禁"的路径，不是现存的违规。 + +- **为什么方向重要。** F1 要证明 `Produced_scan(v) ⊆ S(v)`，所以危险的错误是 + 扫描**没看见**的值——那样一个未注册值就会通过。多报只会产生误报。下面每一条 + 都是一个**被漏掉**的值，却装在一个看起来完整的集合里。 +- **`global` 重绑定完全不可见。** `_module_functions` 只遍历 `tree.body`，从不 + 进入任何函数体，所以另一个函数里的 `global pick; pick = other` 从未被算作 + `pick` 的第二次绑定，同模块调用仍然解析到原始 `def` 的返回值——而这个名字在 + 运行时会被模块换掉。现在任何被某个作用域声明为 `global` 且在该作用域赋值的 + 名字都被取消资格，调用保留 `call_result`。 +- **`**` 展开重播了陈旧的初始值。** `bound` 只跟随朴素的 `name = expression` + 写入，所以一个随后被下标改写的字典仍解析到它的初始值，于是 `{**overrides}` + 把该键的原值报成了产出值。`lookup` 的逐键并集在展开路径上不可达——展开一次 + 贡献所有键——因此被改写过的容器的展开现在走未知键答案。 +- **TypeScript 扫描器没有作用域模型。** 任何拼作 `String` 的标识符都被读成内建 + 转换、任何 `undefined` 都被读成字面量，于是 `function emit(String)`（一个由 + 调用方提供、可以返回任何东西的函数）产出了一个自信的值。现在按**文件**粒度 + 检测遮蔽，比按作用域更粗，而且是刻意的：文件粒度只可能**扣留**一次内建读法， + 永远不可能**凭空造出**一个。 +- **有一条反例是被放松，而不是被删除。** 字面非负下标写入**确实**被建模，读回 + 解析为初始值与该写入的并集。在那里强求 `unresolved` 等于把一个更弱的扫描钉死， + 所以断言改成陈述真正要紧的性质：报告的集合可以多报，但绝不能漏掉被写入的值。 +- **它没有确立什么。** 扫描仍然不建模任何跨模块数据流；文件粒度的遮蔽检测会对 + "在无关函数里遮蔽了 `String`"的文件也扣留内建读法。两者都是保守方向的失效， + 且都是实测记录而非假设。 + ### 2026-09-17 — B2：三条有界绑定形式，以及仍然保持未解析的残量 - **起因：**[#4447](https://github.com/huangruiteng/loopx/issues/4447) 把 B2 残量 diff --git a/loopx/semantics/python_production.py b/loopx/semantics/python_production.py index 6a3d0a0af5..a9e87aa44b 100644 --- a/loopx/semantics/python_production.py +++ b/loopx/semantics/python_production.py @@ -260,6 +260,24 @@ def _is_generator(node: ast.FunctionDef) -> bool: _MODULE_FUNCTIONS: dict[tuple[str, int], dict[str, ast.FunctionDef]] = {} +def _enclosing_scope(tree: ast.Module, target: ast.Global) -> ast.AST: + """The function body that owns this ``global`` statement, else the module.""" + for node in ast.walk(tree): + if isinstance(node, (ast.FunctionDef, ast.AsyncFunctionDef, ast.Lambda, ast.ClassDef)): + for child in ast.walk(node): + if child is target: + return node + return tree + + +def _stores_name(scope: ast.AST, name: str) -> bool: + """True when ``scope`` assigns, augments or deletes ``name``.""" + for child in ast.walk(scope): + if isinstance(child, ast.Name) and child.id == name and isinstance(child.ctx, (ast.Store, ast.Del)): + return True + return False + + def _module_functions(source: SourceFile, tree: ast.Module) -> dict[str, ast.FunctionDef]: """Top-level plain ``def``s a same-module call may be bound to. @@ -289,6 +307,18 @@ def _module_functions(source: SourceFile, tree: ast.Module) -> dict[str, ast.Fun bound[alias.asname or alias.name.split('.')[0]] += 1 elif isinstance(child, (ast.FunctionDef, ast.AsyncFunctionDef, ast.ClassDef)): bound[child.name] += 1 + # A ``global`` rebinding lives inside a function body, which the loop above + # never enters, so the module-level name it replaces looked untouched. Any + # name some scope declares ``global`` and then stores is no longer reliably + # the ``def`` above; binding a call to that ``def`` would report the original + # body's returns for a function the module can swap at runtime. + for node in ast.walk(tree): + if not isinstance(node, ast.Global): + continue + scope = _enclosing_scope(tree, node) + for name in node.names: + if name in defined and _stores_name(scope, name): + bound[name] += 1 functions = {name: node for name, node in defined.items() if bound[name] == 1 and not node.decorator_list and not _is_generator(node)} _MODULE_FUNCTIONS[key] = functions @@ -563,7 +593,17 @@ def flatten(container: ast.Dict, seen: frozenset[str], spread = True arms = [value] while arms: - arm, visited = bound(arms.pop(), seen) + candidate = arms.pop() + # ``bound`` follows plain ``name = expression`` writes only, + # so a container mutated afterwards through a subscript still + # resolves to its initializer. Spreading it would replay the + # stale literal and report a key's original value as the one + # produced. The per-key union that ``lookup`` applies is not + # reachable here, because a spread contributes every key at + # once, so the honest answer is the unknown-key fallback. + if isinstance(candidate, ast.Name) and candidate.id in written: + return None + arm, visited = bound(candidate, seen) if isinstance(arm, ast.IfExp): arms.extend((arm.body, arm.orelse)) continue diff --git a/scripts/semantic_production_scan.mjs b/scripts/semantic_production_scan.mjs index b82c8f1775..a7e28b78fd 100644 --- a/scripts/semantic_production_scan.mjs +++ b/scripts/semantic_production_scan.mjs @@ -35,6 +35,28 @@ for (const source of request.sources) { ts.isTemplateExpression(node)) return 'other'; return 'typescript_dynamic'; }; + // The scanner has no scope model, so it cannot tell the builtin `String` + // from a parameter that shadows it, nor the `undefined` literal from a + // local of that name. A caller-supplied `String` can return anything, so + // trusting the builtin reading would report a produced value the code never + // produces. Shadowing is therefore detected per file -- coarser than per + // scope, which can only withhold a builtin reading, never invent one. + const shadowedGlobals = new Set(); + { + const noteName = name => { + if (!name) return; + if (ts.isIdentifier(name)) shadowedGlobals.add(name.text); + else if (ts.isObjectBindingPattern(name) || ts.isArrayBindingPattern(name)) + for (const element of name.elements) if (ts.isBindingElement(element)) noteName(element.name); + }; + const collect = node => { + if (ts.isParameter(node) || ts.isVariableDeclaration(node) || ts.isBindingElement(node)) noteName(node.name); + else if (ts.isFunctionDeclaration(node) || ts.isClassDeclaration(node)) noteName(node.name); + else if (ts.isImportSpecifier(node) || ts.isImportClause(node) || ts.isNamespaceImport(node)) noteName(node.name); + ts.forEachChild(node, collect); + }; + collect(tree); + } const merge = parts => ({ values: [...new Set(parts.flatMap(part => part.values))].sort(), unresolved: parts.some(part => part.unresolved), @@ -47,7 +69,7 @@ for (const source of request.sources) { if (node.kind === ts.SyntaxKind.NullKeyword) return {values: [], unresolved: false}; // ``undefined`` carries no value and is not an unknown, matching the way // the Python scanner treats an explicit ``None``. - if (ts.isIdentifier(node) && node.text === 'undefined') return {values: [], unresolved: false}; + if (ts.isIdentifier(node) && node.text === 'undefined' && !shadowedGlobals.has('undefined')) return {values: [], unresolved: false}; if (ts.isConditionalExpression(node)) return merge([values(node.whenTrue), values(node.whenFalse)]); // ``a || b`` and ``a ?? b`` are a finite selection, exactly like the // Python scanner's BoolOp arms; ``String(x)`` is a transparent wrapper. @@ -56,7 +78,8 @@ for (const source of request.sources) { return merge([values(node.left), values(node.right)]); } if (ts.isCallExpression(node) && ts.isIdentifier(node.expression) && - node.expression.text === 'String' && node.arguments.length === 1) return values(node.arguments[0]); + node.expression.text === 'String' && node.arguments.length === 1 && + !shadowedGlobals.has('String')) return values(node.arguments[0]); return {values: [], unresolved: true, blocker: blockerFor(node)}; }; const staticName = expression => { @@ -76,7 +99,8 @@ for (const source of request.sources) { if (!node) return false; if (target(node)) return true; if (ts.isCallExpression(node) && ts.isIdentifier(node.expression) && - node.expression.text === 'String' && node.arguments.length === 1) return reads(node.arguments[0]); + node.expression.text === 'String' && node.arguments.length === 1 && + !shadowedGlobals.has('String')) return reads(node.arguments[0]); return ts.isBinaryExpression(node) && [ts.SyntaxKind.BarBarToken, ts.SyntaxKind.QuestionQuestionToken].includes(node.operatorToken.kind) && reads(node.left) && (staticName(node.right) === "" || unwrap(node.right).kind === ts.SyntaxKind.NullKeyword); diff --git a/tests/architecture/test_semantic_producer_binding.py b/tests/architecture/test_semantic_producer_binding.py index 1529bea8ef..08e2edb0bf 100644 --- a/tests/architecture/test_semantic_producer_binding.py +++ b/tests/architecture/test_semantic_producer_binding.py @@ -11,7 +11,10 @@ import pytest +from pathlib import Path + from loopx.semantics.inventory import SourceFile +from loopx.semantics.production import collect_production from loopx.semantics.python_production import scan_python_production OWNER = 'loopx/quota/owner.py::Action' @@ -38,6 +41,24 @@ def at(rows, scope): return [row for row in rows if row.site == f'{CONSUMER}::{scope}'] +ROOT = Path(__file__).resolve().parents[2] +TS_CONSUMER = 'loopx/control_plane/quota/probe.ts' + + +def only(rows, form): + return [row for row in rows if row.form == form] + + +def ts_vocabulary(): + return {'values': ['run', 'wait'], 'producers': ['loopx/control_plane/quota/probe.py::emit'], + 'owners': {'python': None}, 'literal_scan': {'field': 'action'}} + + +def ts_scan(text): + return collect_production(ROOT, ts_vocabulary(), [SourceFile(TS_CONSUMER, '.ts', text)]) + + + # --- same-module call results ------------------------------------------------- @@ -452,3 +473,156 @@ def test_a_function_that_yields_itself_is_still_not_bound(): ' return {"action": choose()}\n', ), 'emit') assert blockers(rows) == {'call_result'} + + +# --- counterexamples: shapes whose complete output the scan cannot see -------- +# +# Each case has a value the scan cannot see. Reporting the values it *can* see as +# the complete set is the dangerous direction: F1 proves production is a subset +# of what is registered, so a value the scan misses is an unregistered value +# that passes the gate. Over-reporting only raises a false alarm. These pin the +# unknown open so a later "improvement" cannot quietly close it. + +@pytest.mark.parametrize('text', [ + # a `for` back edge: iteration two emits 'drop' + 'def emit(rows):\n chosen = "run"\n for row in rows:\n' + ' build({"action": chosen})\n chosen = "drop"\n', + # a `while` back edge + 'def emit(rows):\n chosen = "run"\n while rows:\n' + ' build({"action": chosen})\n chosen = "drop"\n rows = rows[1:]\n', + # the carrying write sits in the outer loop, the read in the inner one + 'def emit(rows):\n chosen = "run"\n for row in rows:\n for inner in row:\n' + ' build({"action": chosen})\n chosen = "drop"\n', + # `finally` runs after the read and feeds the next iteration + 'def emit(rows):\n chosen = "run"\n for row in rows:\n try:\n' + ' build({"action": chosen})\n finally:\n chosen = "drop"\n', +]) +def test_a_loop_carried_write_is_not_the_first_iteration_alone(text): + """The second iteration emits ``drop``; only the first write precedes the read. + + Ordering a local's writes by source position is execution order only where + no back edge crosses it. Inside a loop the textually *later* write reaches + the read on the next iteration, so "the writes above this line" is not the + set of possible values, and reporting it states a closed value set that is + not closed. F1 asks whether a producer writes only registered values; a + producer emitting an unregistered value on every iteration after the first + would pass it. + """ + rows = only(scan(text), 'dict') + assert rows, 'the dict write must still be observed' + assert all(row.unresolved for row in rows) + assert blockers(rows) == {'unstable_local'} + assert known(rows) == set() + + +@pytest.mark.parametrize('store', [ + # `codes[-1]` and `codes[0]` are the same element of a one-item list, and a + # negative index names a slot whose number depends on the container length, + # so the scan cannot order this write and keeps the read unknown. + 'codes[-1] = "drop"', + # A literal non-negative store *is* modelled: the key carries the union of + # its initializer and every write, so the read resolves to {run, drop}. + 'codes[0] = "drop"', +]) +def test_a_subscript_write_is_never_read_as_the_untouched_container(store): + """After the write the element is `drop`, and the scan must not miss it. + + What matters is soundness, not strictness. F1 proves production is a subset + of what is registered, so the failure that lets an unregistered value + through is *missing* `drop`; still offering `run` is an over-approximation + that can only raise a false alarm. Both answers below are therefore + acceptable, and demanding `unresolved` for the modelled case would pin a + weaker scan in place rather than a safer one. + """ + rows = only(scan('def emit():\n codes = ["run"]\n ' + store + '\n' + ' return {"action": codes[0]}\n'), 'dict') + assert rows + assert all(row.unresolved for row in rows) or 'drop' in known(rows), ( + f'{store}: reported {known(rows)} as complete, which omits the written value' + ) + + +def test_a_dict_mutated_after_construction_is_not_read_from_its_initializer(): + """A ``**`` spread of a mutated local must not replay the stale literal.""" + rows = only(scan('def emit():\n overrides = {"action": "run"}\n' + ' overrides["action"] = "drop"\n return {**overrides}\n', + returns=['emit'], paths={'emit': ('action',)}), 'return') + assert rows and all(row.unresolved for row in rows) + assert blockers(rows) == {'dynamic_key'} + assert known(rows) == set() + + +def test_a_helper_rebound_through_global_is_not_the_module_level_function(): + """``install()`` replaces ``pick``; the call site cannot be read off the ``def``.""" + rows = only(scan('def pick():\n return "run"\n' + 'def install():\n global pick\n pick = other\n' + 'def emit():\n return {"action": pick()}\n'), 'dict') + assert rows and all(row.unresolved for row in rows) + assert blockers(rows) == {'call_result'} + assert known(rows) == set() + + +def test_a_typescript_parameter_shadowing_string_is_not_the_builtin_conversion(): + """``String`` here is a caller-supplied function that can return anything.""" + rows = ts_scan('function emit(String) {\n return {action: String("run")};\n}\n') + assert rows and all(row.unresolved for row in rows) + assert blockers(rows) == {'call_result'} + assert set().union(*(row.values for row in rows)) == set() + + +@pytest.mark.parametrize('text, reason', [ + # An attribute of an object this scan never resolved. + ('function emit(decision) {\n return {action: decision.effective_action};\n}\n', 'attribute_read'), + # A fallback is not the obstacle; the operand that could not be read is. + ('function emit(decision) {\n return {action: decision.effective_action ?? ""};\n}\n', 'attribute_read'), + # A value handed back by a call. + ('function emit(input) {\n return {action: project(input)};\n}\n', 'call_result'), + ('function emit(input) {\n return {action: await project(input)};\n}\n', 'call_result'), + # A bare local name. + ('function emit(choice) {\n return {action: choice};\n}\n', 'unstable_local'), +]) +def test_typescript_unresolved_writes_name_their_own_reason(text, reason): + """B2 keeps the taxonomy: one opaque bucket told a reviewer nothing.""" + rows = ts_scan(text) + assert rows and all(row.unresolved and not row.values for row in rows) + assert blockers(rows) == {reason} + + +def test_typescript_dynamic_remains_only_as_the_unclassifiable_fallback(): + rows = ts_scan('function emit(a, b) {\n return {action: a + b};\n}\n') + assert blockers(rows) == {'typescript_dynamic'} + + +def test_python_and_typescript_report_the_same_labels_for_the_same_shape(): + shape = 'attribute_read' + python = scan('def emit(decision):\n return {"action": decision.effective_action}\n') + typescript = ts_scan('function emit(decision) {\n return {action: decision.effective_action};\n}\n') + assert blockers(python) == blockers(typescript) == {shape} + + +def test_a_field_named_keyword_stays_unproved_even_when_its_value_is_known(): + """A resolved expression is not a resolved *role*, and the gate wants the role. + + The scan can read this argument perfectly well -- it is an owner member. The + site stays unresolved because the callee is not a reviewed output builder: + a helper that takes a field-named keyword is at least as likely to read the + field as to emit it. Counting any field-named keyword as production would + make the obligation tautological, which Section 5 of the RFC forbids. + + Narrowing this bucket therefore needs a registry ``call_producers`` entry + naming the builder -- a data edit a reviewer sees and approves -- and not a + cleverer scanner. That is why these sites keep a fully resolved value set + alongside ``unresolved``; the pair is the evidence for the registry edit. + """ + rows = scan('from .owner import Action\ndef emit():\n return record(action=Action.RUN.value)\n') + assert len(rows) == 1 + assert rows[0].form == 'keyword_unproved' + assert rows[0].unresolved and rows[0].blocker == 'argument_name_only' + assert rows[0].values == frozenset({'run'}) + + +def test_a_declared_output_builder_is_what_turns_that_value_into_production(): + rows = scan('from .owner import Action\ndef emit():\n return record(action=Action.RUN.value)\n', + calls={f'{CONSUMER}::record': {'action': 0}}) + assert [row.form for row in rows] == ['call_argument'] + assert known(rows) == {'run'} and not rows[0].unresolved