diff --git a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md index d3cdcbf42e..f43cd71134 100644 --- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md +++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md @@ -1146,6 +1146,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 — Two measurements that contradicted themselves, corrected Normative for what F5's `verified` count means and for closed-set collision 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 d59746f570..c700f55261 100644 --- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md +++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md @@ -922,6 +922,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 — 两处自相矛盾的度量已修正 对 F5 的 `verified` 含义与闭集碰撞身份是规范性的。没有放松任何预算、下限或锚点； 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