From a022005911a3b34d64ce637c16f007abacba337c Mon Sep 17 00:00:00 2001 From: song <22676124+songoow@users.noreply.github.com> Date: Thu, 17 Sep 2026 11:01:02 -0400 Subject: [PATCH 1/3] feat(semantics): bind three bounded producer forms and share the blocker taxonomy The B2 residue in #4447 was recorded as 34 sites; measured on this tree it is 41, spread across every scanned vocabulary rather than effective_action alone. This deepens the bounded producer scan by three recognized forms, each with a negative twin, and leaves every site it cannot bind unresolved with its reason. Same-module call results: a call to an undecorated, non-generator, plainly defined top-level def of the same module resolves to the union of that function's own returns. Arguments are never bound to parameters, so a returned parameter stays unknown and the answer does not depend on the call site. Ordered rebinding: a local written more than once resolves to the union of the writes that textually precede the read, and only when every store of that name is a plain name = expression. Key-precise container writes: a container mutated only through direct literal-key subscript writes keeps its untouched keys; a written key carries the union of its initializer and every write. A ** spread of statically known dict literals is flattened so an optional spread no longer hides a sibling key. The TypeScript parser gains the two sound forms the Python scanner already had and reports the same blocker vocabulary, so one residue taxonomy covers both runtimes instead of a single typescript_dynamic catch-all. An owner-member result now carries its reason too. Unresolved sites 41 -> 40; unresolved rows carrying at least one known value 2 -> 7. Registry values, budgets and the producer site list are unchanged. The producer scan is net faster (9.20s -> 7.17s over the 319 files it reaches) because it now reuses the memoised parse and module-function table. Refs #4447 (B2) Co-Authored-By: Claude Opus 5 (1M context) Signed-off-by: song <22676124+songoow@users.noreply.github.com> --- .../semantic-vocabulary-convergence-v0.md | 104 ++++- ...emantic-vocabulary-convergence-v0.zh-CN.md | 78 +++- loopx/semantics/production.py | 4 +- loopx/semantics/python_production.py | 426 ++++++++++++++---- scripts/semantic_production_scan.mjs | 37 +- .../test_semantic_producer_binding.py | 300 ++++++++++++ .../test_semantic_python_production.py | 7 + 7 files changed, 852 insertions(+), 104 deletions(-) create mode 100644 tests/architecture/test_semantic_producer_binding.py diff --git a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md index 581a73af80..4d025fb4ac 100644 --- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md +++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md @@ -391,9 +391,25 @@ dictionaries, call keywords, owner-member results and declared scalar returns are parsed with AST. Imported enum aliases resolve only to the registered owner, including one unrenamed re-export hop through a tracked module (a second hop, a renamed re-export or a rebinding stays unknown); shadowed -names, reassignments and unresolved calls remain unknown. Conditional -results exclude the condition's literals. TypeScript object writes, assignments -and declared returns use the repository's TypeScript parser rather than regex. +names and unbindable calls remain unknown. Conditional +results exclude the condition's literals. Three further local forms are bound, +each only under a stated condition: a call to an undecorated, non-generator, +plainly-defined top-level `def` **of the same module** resolves to the union of +that function's own returns, with arguments never bound to parameters, so a +returned parameter stays unknown and the result is independent of the call site; +a local written more than once resolves to the union of the writes that +textually precede the read, and only when every store of that name is a plain +`name = expression`; and a container mutated only through direct literal-key +subscript writes keeps its untouched keys, with a written key carrying the union +of its initializer and every write. Anything outside those conditions — a +decorator, `async def`, a generator, recursion, an imported or attribute call, a +loop, `with`, `except`, walrus, augmented, unpacking, `global` or `del` +rebinding, an alias, a method call, a computed or deeper store, an escape into a +call, or an unknown `**` spread — leaves the site unknown rather than admitting +a value. TypeScript object writes, assignments +and declared returns use the repository's TypeScript parser rather than regex, +and report the same blocker vocabulary as the Python scanner, so one residue +taxonomy covers both runtimes. Neither parser executes inspected source. These are syntactic result witnesses, not a proof of reachability or whole-program data flow. @@ -791,6 +807,7 @@ on the next full-tree scan; genuine shared-contract changes still need review. | Historical committed snapshots could become stale across merges | Replay the scanner over the first parent and the merge of the last twenty `upstream/main` merge commits | 8 of 20 merges change at least one carrier | Historical cost motivating Q9; current checks compute the combined tree without a committed snapshot | | The formal model cannot silently lose a proof obligation | Remove an invariant, role, relation, candidate decision, or proof-boundary category from `formal_model` | The drift smoke fails on the exact formal-model shape | The model is a finite contract and proof ledger; it does not prove the listed properties by itself | | An obligation cannot claim a domain nobody counts | `uv run --extra test python -m pytest tests/architecture/test_semantic_vocabulary_drift.py -k domain` | Dropping `domain`, inflating `verified` or `registered`, inventing a selector, claiming an unanchored selector or an out-of-stage evidence bound, and an advisory invariant claiming verified members each fail closed | The sizes are derived from the registry, so the check grounds the declared domain in registry data; it does not prove the obligation over that domain | +| Bounded binding forms cannot be loosened into false evidence | `uv run --extra test python -m pytest tests/architecture/test_semantic_producer_binding.py` | pass; every recognized form has a negative twin — a decorated, `async`, generator, rebound, imported or recursive callee, an unordered store, an aliased or escaped container, and an unknown `**` spread each keep the site unresolved | Fixture repository; a site the scan cannot bind stays unresolved with its recorded reason, never dead | | F1/F2 quantify over exactly what the producer check walks | Same test module: compare `check_producers`' predicate with the declared F1/F2 domain | The vocabularies with `producers` are exactly the `kernel` tier, 6 of 26; the other 20 are all `cross_runtime` | The scan reach bounds the claim further and is reported, not pinned | Known limits, stated so the check is not over-trusted: @@ -1071,6 +1088,86 @@ introduce a competing target state. ## Appendix A: Execution ledger (non-normative) +### 2026-09-17 — B2: three bounded binding forms, and the residue that stays unresolved + +- **Trigger:** [#4447](https://github.com/huangruiteng/loopx/issues/4447) recorded + the B2 residue as "34 total minus the 15 unprovable by design". Re-measured on + `9003577f9` the total is **41**, and the breakdown is across every scanned + vocabulary rather than `effective_action` alone: `annotation_only=5, + argument_name_only=10, attribute_read=2, call_result=11, other=1, + typescript_dynamic=8, unstable_local=4`. The issue's number was stale; this + entry records the measured split. +- **Delivered:** three bounded local forms in `python_production`, each with + positive and negative fixtures in + `tests/architecture/test_semantic_producer_binding.py`. + 1. **Same-module call results.** A call to an undecorated, non-generator, + plainly-defined top-level `def` of the same module resolves to the union of + that function's own returns. Arguments are never bound to parameters, so a + returned parameter stays unknown and the answer does not depend on the call + site; it is memoised per module scan. A decorator, `async def`, a generator, + a second top-level binding of the name, an imported or attribute call, a + local rebinding and recursion all keep the `call_result` blocker. + 2. **Ordered rebinding of a local.** A local written more than once resolves to + the union of the writes that textually precede the read, and only when every + store of that name is a plain `name = expression`. Loop, `with`, `except`, + walrus, augmented, unpacking, `global` and `del` rebindings are not ordered + by this scan and erase the local. + 3. **Key-precise container writes.** A local container mutated only through + direct literal-key subscript writes keeps its untouched keys, and a written + key carries the union of its initializer and every write. An alias, a method + call, a computed or deeper store, a `del`, or passing the container to any + call still discards the container, as before. A `**` spread of statically + known dict literals is flattened, so an optional spread no longer hides a + sibling key; an unknown spread still makes every key dynamic. + + The TypeScript parser gains the two sound forms the Python scanner already had + (`||` and `??` arms, a transparent `String(x)`, and `undefined` read as no + value) and, more importantly, reports the **same blocker vocabulary**: the + single `typescript_dynamic` catch-all is replaced by `attribute_read`, + `call_result`, `unstable_local` and `dynamic_key`, with `typescript_dynamic` + kept only as the fallback for a form it cannot classify. An owner-member + result (`enum_result`) now carries its reason too; an unlabelled unknown was + invisible in the report breakdown. +- **Result:** unresolved sites **41 → 40**, split + `annotation_only=5, argument_name_only=10, attribute_read=7, call_result=14, + other=1, unstable_local=3`. All eight TypeScript sites are reclassified (five + `attribute_read`, three `call_result`); none was resolvable, so that part is a + taxonomy, not a shrink. The one site that closes is + `driver.py::build_loopx_turn_plan:500`, which needed all three forms and the + spread flattening at once. Evidence improves further than the count shows: + unresolved rows carrying at least one known value go **2 → 7**. Registry + values, budgets and the producer site list are unchanged, and no site becomes + newly visible or unregistered. +- **Deliberately not bound, with the reason recorded:** + - `annotation_only` (5) — all five are bare `effective_action: str` field + declarations carrying **no value node at all**. Unprovable by design; + the issue's classification is confirmed. + - `argument_name_only` (10) — confirmed unprovable by design, with one + sharpening: these are unprovable as a *production role*, not unresolvable as + an expression. Four of the ten now carry a fully resolved value set and are + still correctly unresolved, because the callee (`_execution_obligation` and + its peers) reads the field rather than emitting it. The honest way to shrink + this bucket is a registry `call_producers` declaration naming a reviewed + output builder — a data edit a reviewer sees — never a scanner change. + Counting any field-named keyword as production would make the obligation + tautological, which Section 5 forbids. + - `attribute_read` (7), `call_result` (14), `unstable_local` (3) and `other` + (1) — every remaining site bottoms out in one of four things outside this + scan's bound: a read off a caller-supplied mapping or object + (`decision.get("effective_action")`, `run_decision.effective_action`), a call + into another module, a returned parameter, or a method chain. Binding any of + them needs cross-module or object-field resolution, a separate bounded form + with its own blast radius; it is not attempted here. **A site this scan + cannot bind stays `unresolved` with its recorded reason — it is never + treated as dead.** +- **Cost:** the producer scan runs on every pull request touching `loopx/`. Over + the 319 Python files it reaches and the 5 producer vocabularies, best of three + runs on one tree: **9.20 s → 7.17 s**. The deepened scan is net faster because + it now reuses the memoised parse and the module-function table across + vocabularies instead of re-parsing once per scan. +- **Effect on normative design:** Section 5's bounded producer model names the + three forms and the shared blocker taxonomy; no invariant or milestone changes. + ### 2026-09-17 — Invariant statements bounded to their verified domains Normative; requires kernel-maintainer approval. No check changes its pass/fail @@ -1280,6 +1377,7 @@ result on the current tree; what changes is what the invariants claim. | 2026-09-16 | Q9: compute the full inventory on demand; retire the committed census | Implementation for [maintainer feedback](https://github.com/huangruiteng/loopx/pull/4360#issuecomment-5692062394); PR review pending | Committed snapshot with post-merge regeneration; diff-only scan rejected | 1, I6, 3, 5, 9, 10, 12 | | 2026-09-16 | B2: bind one unrenamed re-export hop in the Python producer scanner | Implementation, Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B2; PR review pending | Require every consumer to import the owner module (fragile; failed silently in M2); unbounded multi-hop resolution rejected | 5, Appendix A | | 2026-09-16 | B1 rename invariance: add the name-keyed divergence advisory; state the limit it does not close | Implementation, Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B1; PR review pending | Keying the budget on value sets (rejected: `CONFIDENCE_LEVELS` and `EDGE_CASE_COMPLEXITIES` share `high/low/medium` with different meanings); a committed name ledger (rejected at M0: Q9 retired the committed census). The advisory lists surviving forks by name; it was first described as catching a one-sided rename, which measurement disproved, so both mirrors state the limit as it behaves | 9 | +| 2026-09-17 | B2: bind same-module call results, ordered local rebinding and key-precise container writes; reclassify the TypeScript residue rather than shrink it | Implementation, Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B2; PR review pending | Bind cross-module calls and object fields (rejected: a separate bounded form with its own blast radius, not this slice); count a field-named keyword as production (rejected: it makes the obligation tautological, Section 5); leave `typescript_dynamic` as one catch-all (rejected: eight sites shared one reason, so the residue was not actionable); bind the callee's parameters to the call-site arguments (rejected: the answer would depend on the caller and could not be memoised, and a wrong binding would invent evidence) | 5, 9, Appendix A | | 2026-09-17 | Bound F1/F2 to the kernel tier and the scan reach, restate F4 as scope enumeration completeness, and give every obligation a derived `domain` | Implementation, Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447); **kernel-maintainer approval required, not yet given** | Leave the unconditional statements and record the gap in prose only (rejected: the statement was stronger than `validate_production`'s own docstring); restate F4 as per-context value-set disjointness (rejected: refuted by the repo's own data, since `scope_declarations` exists to permit legitimate same-name reuse); widen the scan so the unconditional claim becomes true (rejected: a separate change with its own risk) | 5, 9, Appendix B, Appendix C | ## Appendix C: Evidence registry 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 abb3c455ec..96da6d4981 100644 --- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md +++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md @@ -307,9 +307,20 @@ M0.5 之后新增或删除值时；`cross_module` 只在晋升后（Q8）。持 Python 通过 AST 解析字段赋值（含下标、属性及带注解赋值）、字典、调用关键字、 owner 成员结果及声明函数的标量返回。导入枚举的别名只解析到已登记 owner，含经由一个被跟踪模块的一跳未改名再导出（第二跳、改名再导出或重新绑定保持 unknown）； -被遮蔽的名字、重复赋值及未解析调用仍为 unknown。条件表达式只检查结果分支， -排除条件中的字面量。TypeScript 的对象写入、赋值及声明返回使用仓库的 TypeScript -解析器。两个解析器都不执行被检查源码。这些是句法结果证据，不是可达性或全程序 +被遮蔽的名字与无法绑定的调用仍为 unknown。条件表达式只检查结果分支， +排除条件中的字面量。另有三条局部形式被绑定，且各自只在明确条件下成立：对 +**同模块内**一个未被装饰、非生成器、以普通 `def` 定义的顶层函数的调用，解析为 +该函数自身全部 return 的并集，实参从不绑定到形参，因此返回形参仍为 unknown， +结果与调用点无关；被写入多次的局部变量解析为文本上位于该读取之前的那些写入的 +并集，且仅当该名字的每一次 store 都是普通的 `name = expression` 时成立；只经由 +直接字面量键下标写入被改动的容器保留其未被触碰的键，被写入的键携带其初始化值 +与每一次写入的并集。凡落在上述条件之外的——装饰器、`async def`、生成器、递归、 +导入调用或属性调用，循环、`with`、`except`、海象、增量赋值、解包、`global` 或 +`del` 造成的重绑定，别名、方法调用、计算键或更深层的 store、逃逸进调用，以及 +未知的 `**` 展开——都让该位点保持 unknown，而不是采信一个取值。 +TypeScript 的对象写入、赋值及声明返回使用仓库的 TypeScript +解析器，并报告与 Python 扫描器相同的阻塞原因词汇，因此同一套残量分类覆盖两个 +运行时。两个解析器都不执行被检查源码。这些是句法结果证据，不是可达性或全程序 数据流证明。 `uv run python examples/semantic-vocabulary-drift-smoke.py --report` 列出未解析的生产 @@ -647,6 +658,7 @@ owner 符号集合的组：`EffectiveAction` 与 `EFFECTIVE_ACTIONS` 是同一 | 历史上的已提交清单会因上游合并而过期 | 对 `upstream/main` 最近二十个合并提交，在第一父提交与合并结果之间重放扫描器 | 20 次合并中 8 次至少改变一个载体 | Q9 的历史动机；当前检查直接计算合并后的全树，不再依赖提交快照 | | 形式模型不能静默丢失证明义务 | 从 `formal_model` 删除不变量、角色、候选决策、关系或证明边界分类 | 漂移 smoke 针对形式模型结构失败 | 该模型是有限契约和证明账本，本身不等于这些性质已经被证明 | | 义务不能声称一个无人清点的值域 | `uv run --extra test python -m pytest tests/architecture/test_semantic_vocabulary_drift.py -k domain` | 删掉 `domain`、调大 `verified` 或 `registered`、自造 selector、使用未钉住的 selector 或跨阶段的证据边界、以及 advisory 不变量声称已验证成员，逐项失败关闭 | 规模从注册表推导，因此该检查把声明值域接地到注册表数据；它不证明该义务在那个值域上成立 | +| 有界绑定形式不能被放宽成假证据 | `uv run --extra test python -m pytest tests/architecture/test_semantic_producer_binding.py` | 通过；每条被识别的形式都有反例孪生——被装饰的、`async`、生成器、被重绑定的、导入的或递归的被调方，无序 store，被别名或逃逸的容器，以及未知 `**` 展开，都让该位点保持未解析 | 夹具仓库；本扫描无法绑定的位点保持未解析并带上被记录的原因，绝不当作 dead | | F1/F2 恰好量化 producer 检查真正走到的集合 | 同一测试模块：将 `check_producers` 的谓词与 F1/F2 声明的值域对比 | 声明了 `producers` 的词表恰好是 `kernel` 层，26 中的 6；其余 20 个全部是 `cross_runtime` | 扫描范围进一步约束该声明，它被上报而不被钉住 | 已知边界，写明是为了不让这个检查被过度信任： @@ -871,6 +883,65 @@ PR review 保留这些层级。普通改动记录检查范围和理由，无共 ## 附录 A：执行账本（非规范） +### 2026-09-17 — B2：三条有界绑定形式，以及仍然保持未解析的残量 + +- **起因：**[#4447](https://github.com/huangruiteng/loopx/issues/4447) 把 B2 残量 + 记为“34 个减去 15 个设计上不可证的”。在 `9003577f9` 上重新测量，总数是 **41**， + 且分布覆盖全部被扫描词表，而不只是 `effective_action`：`annotation_only=5, + argument_name_only=10, attribute_read=2, call_result=11, other=1, + typescript_dynamic=8, unstable_local=4`。issue 里的数字已经过期；本条记录实测分布。 +- **交付：**在 `python_production` 中新增三条有界局部形式，每条都在 + `tests/architecture/test_semantic_producer_binding.py` 里配有正例与反例。 + 1. **同模块调用结果。**对同模块内一个未被装饰、非生成器、以普通 `def` 定义的 + 顶层函数的调用，解析为该函数自身全部 return 的并集。实参从不绑定到形参， + 因此返回形参仍然未知，且结果与调用点无关，可按模块扫描记忆化。装饰器、 + `async def`、生成器、该名字的第二个顶层绑定、导入调用与属性调用、局部重绑定 + 以及递归，都继续保留 `call_result` 阻塞原因。 + 2. **局部变量的有序重绑定。**被写入多次的局部变量，解析为文本上位于该读取之前 + 的那些写入的并集，且仅当该名字的每一次 store 都是普通的 + `name = expression` 时才成立。循环、`with`、`except`、海象、增量赋值、解包、 + `global` 与 `del` 造成的重绑定不被本扫描定序，会直接抹掉该局部变量。 + 3. **按键精确的容器写入。**只经由直接字面量键下标写入被改动的局部容器，保留其 + 未被触碰的键；被写入的键则携带其初始化值与每一次写入的并集。别名、方法调用、 + 计算键或更深层的 store、`del`，以及把容器作为任何调用的实参传出，仍然像以前 + 一样丢弃整个容器。对静态可知的 dict 字面量的 `**` 展开会被摊平，因此可选展开 + 不再遮蔽同级键；未知展开仍使所有键变为动态。 + + TypeScript 解析器补上了 Python 扫描器早已具备的两条可靠形式（`||` 与 `??` 的 + 分支、透明的 `String(x)`，以及把 `undefined` 读作无值），更重要的是开始报告 + **同一套阻塞原因词汇**：单一的 `typescript_dynamic` 兜底被 + `attribute_read`、`call_result`、`unstable_local` 与 `dynamic_key` 取代， + `typescript_dynamic` 只保留为无法进一步归类时的兜底。owner 成员结果 + （`enum_result`）现在也携带原因；未打标签的未知在报告分布里是不可见的。 +- **结果：**未解析位点 **41 → 40**，分布为 `annotation_only=5, + argument_name_only=10, attribute_read=7, call_result=14, other=1, + unstable_local=3`。八个 TypeScript 位点全部被重新归类（五个 `attribute_read`、 + 三个 `call_result`）；它们没有一个是可解析的，因此这部分是分类学修正，不是缩减。 + 唯一被关闭的位点是 `driver.py::build_loopx_turn_plan:500`，它同时需要三条形式加上 + 展开摊平。证据的改善超过数字所显示的：携带至少一个已知值的未解析行从 **2 → 7**。 + 注册表取值、预算与 producer 位点清单均未变化，也没有任何位点变为新可见或未注册。 +- **有意不绑定，并记录原因：** + - `annotation_only`（5）——五个全部是裸的 `effective_action: str` 字段声明， + **根本没有值节点**。设计上不可证；issue 的归类得到确认。 + - `argument_name_only`（10）——确认设计上不可证，但需要一点锐化：它们不可证的是 + *生产角色*，而不是表达式不可解析。十个里现在有四个已经携带完整解析出的取值集合， + 并且仍然被正确地判为未解析，因为被调方（`_execution_obligation` 及其同类）是在 + 读取该字段而不是产出它。缩减这一类的诚实做法是在注册表 `call_producers` 中声明 + 一个经过评审的输出构造器——一次评审者看得见的数据编辑——而绝不是改扫描器。把任何 + 与字段同名的关键字算作生产，会使该义务变成同义反复，这是第 5 节所禁止的。 + - `attribute_read`（7）、`call_result`（14）、`unstable_local`（3）与 `other` + （1）——剩下的每个位点最终都落在本扫描边界之外的四件事之一：读取调用方提供的 + 映射或对象（`decision.get("effective_action")`、`run_decision.effective_action`）、 + 跨模块调用、返回形参，或方法链。绑定其中任何一种都需要跨模块或对象字段解析， + 那是另一条有自己影响面的有界形式，本切片不做。**本扫描无法绑定的位点，保持 + `unresolved` 并带上它被记录的原因——绝不当作 dead。** +- **成本：**producer 扫描在每个触及 `loopx/` 的 PR 上都会运行。在它覆盖的 319 个 + Python 文件与 5 个 producer 词表上，同一棵树三次取最优：**9.20 s → 7.17 s**。 + 加深后的扫描净变快，因为它现在跨词表复用记忆化的语法树与模块函数表，而不再每次 + 扫描重新解析。 +- **对规范设计的影响：**第 5 节的有界 producer 模型写明这三条形式与共享的阻塞原因 + 分类；不变量与里程碑均无变化。 + ### 2026-09-17 — 不变量表述收敛到各自已验证的值域 规范性变更；需要内核维护者批准。当前源码树上没有任何检查的通过/失败结果改变， @@ -1043,6 +1114,7 @@ PR review 保留这些层级。普通改动记录检查范围和理由，无共 | 2026-09-16 | Q9：全树按需计算；移除已提交结构清单 | 根据[维护者反馈](https://github.com/huangruiteng/loopx/pull/4360#issuecomment-5692062394)实现，PR 评审待完成 | 取代合并后补再生成；拒绝只扫描 diff | 1、I6、3、5、9、10、12 | | 2026-09-16 | B2：Python producer 扫描器绑定一跳未改名再导出 | 实现，Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B2；PR 评审待完成 | 要求每个消费者都从 owner 模块导入（脆弱；M2 中已静默失效）；拒绝无界多跳解析 | 5、附录 A | | 2026-09-16 | B1 改名不变性：新增按名字归组的分歧报告；写明它未闭合的边界 | 实现，Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B1；PR 评审待完成 | 把预算改按值集归组（否决：`CONFIDENCE_LEVELS` 与 `EDGE_CASE_COMPLEXITIES` 共享 `high/low/medium` 而含义不同）；提交名字账本（M0 否决：Q9 已退役提交式清单）。该报告列出仍然存在的分叉；初稿称它能抓住单侧改名，实测证否，故两份镜像按真实行为写明边界 | 9 | +| 2026-09-17 | B2：绑定同模块调用结果、局部变量有序重绑定与按键精确的容器写入；对 TypeScript 残量做重新归类而非缩减 | 实现，Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B2；PR 评审待完成 | 绑定跨模块调用与对象字段（拒绝：那是另一条有自己影响面的有界形式，不属于本切片）；把与字段同名的关键字算作生产（拒绝：会使该义务变成同义反复，见第 5 节）；保留 `typescript_dynamic` 作为单一兜底（拒绝：八个位点共用一个原因，残量无法被行动）；把被调方形参绑定到调用点实参（拒绝：结果会依赖调用方而无法记忆化，且一次错误绑定会凭空造出证据） | 5、9、附录 A | | 2026-09-17 | 将 F1/F2 限定在 kernel 层与扫描范围，把 F4 重述为作用域枚举完备性，并给每条义务加上可推导的 `domain` | 实现，Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447)；**需要内核维护者批准，尚未获得** | 保留无条件表述、只在正文记一笔缺口（否决：该表述比 `validate_production` 自己的 docstring 还强）；把 F4 重述为各上下文值集互斥（否决：会被仓库自身数据推翻，`scope_declarations` 恰恰就是为了允许合理的同名复用）；扒宽扫描让无条件声明成立（否决：那是自带风险的另一个变更） | 5、9、附录 B、附录 C | ## 附录 C：证据登记 diff --git a/loopx/semantics/production.py b/loopx/semantics/production.py index 0b12cbaa61..97eedc2c7a 100644 --- a/loopx/semantics/production.py +++ b/loopx/semantics/production.py @@ -126,8 +126,10 @@ def _typescript_scan( and isinstance(error.get('line'), int) and error['line'] > 0): raise ValueError(f"{error['path']}:{error['line']}: invalid TypeScript source; repair syntax before semantic scanning") raise ValueError('TypeScript production parser failed; run npm ci --ignore-scripts and check the Node runtime') + # The parser names the same blocker vocabulary as the Python scanner; + # ``typescript_dynamic`` stays the fallback for a form it cannot classify. rows.extend(Production(r['site'], r['line'], r['form'], frozenset(r['values']), r['unresolved'], - 'typescript_dynamic' if r['unresolved'] else None) + (r.get('blocker') or 'typescript_dynamic') if r['unresolved'] else None) for r in json.loads(completed.stdout)) return rows diff --git a/loopx/semantics/python_production.py b/loopx/semantics/python_production.py index 3bcf1be656..689efd2db5 100644 --- a/loopx/semantics/python_production.py +++ b/loopx/semantics/python_production.py @@ -9,6 +9,7 @@ import ast from collections import Counter from dataclasses import dataclass +from types import SimpleNamespace from typing import Mapping, TypeVar from .inventory import SourceFile @@ -25,13 +26,15 @@ class Production: """Why the unknown portion stayed unknown; ``None`` when fully resolved. ``argument_name_only`` a field-named keyword argument, which never proves an - output role. ``unstable_local`` a parameter, reassignment or shadowed name. - ``call_result`` the value comes back from a call. ``dynamic_key`` a computed - or non-literal subscript. ``serialized_value`` a string where an enum object - was required. ``annotation_only`` a bare annotation that declares the field - without a value. ``attribute_read`` an attribute of an unresolved object. - ``typescript_dynamic`` the TypeScript scanner could not resolve the write. - ``other`` anything else; it keeps the site visible. + output role. ``unstable_local`` a parameter, an unordered rebinding or a + shadowed name. ``call_result`` the value comes back from a call this scan + cannot bind. ``dynamic_key`` a computed or non-literal subscript. + ``serialized_value`` a string where an enum object was required. + ``annotation_only`` a bare annotation that declares the field without a + value. ``attribute_read`` an attribute of an unresolved object. + ``typescript_dynamic`` a TypeScript form the parser cannot classify further; + every other label is shared by both runtimes, so one residue taxonomy + covers them. ``other`` anything else; it keeps the site visible. """ @@ -227,6 +230,73 @@ def _qualified_bindings(source: SourceFile, tree: ast.Module, owners: Mapping[st return bindings +def _is_generator(node: ast.FunctionDef) -> bool: + return any(isinstance(child, (ast.Yield, ast.YieldFrom)) for child in ast.walk(node)) + + +# Keyed by tree identity, which is stable because ``_TREES`` retains every tree +# it parses; the table is derived from the module body alone, so it is the same +# for every vocabulary scanned over that file. +_MODULE_FUNCTIONS: dict[int, dict[str, ast.FunctionDef]] = {} + + +def _module_functions(tree: ast.Module) -> dict[str, ast.FunctionDef]: + """Top-level plain ``def``s a same-module call may be bound to. + + A decorator can replace the returned object, ``async def`` hands back a + coroutine rather than the value, and a generator yields instead of + returning, so none of those is a recognized producer. Any second top-level + binding of the name -- a redefinition, class, import, assignment or + ``del`` -- leaves the name unproven and the call keeps ``call_result``. + """ + known = _MODULE_FUNCTIONS.get(id(tree)) + if known is not None: + return known + bound: Counter[str] = Counter() + defined: dict[str, ast.FunctionDef] = {} + for node in tree.body: + if isinstance(node, (ast.FunctionDef, ast.AsyncFunctionDef, ast.ClassDef)): + bound[node.name] += 1 + if isinstance(node, ast.FunctionDef): + defined[node.name] = node + continue + for child in ast.walk(node): + if isinstance(child, ast.Name) and isinstance(child.ctx, (ast.Store, ast.Del)): + bound[child.id] += 1 + elif isinstance(child, (ast.Import, ast.ImportFrom)): + for alias in child.names: + bound[alias.asname or alias.name.split('.')[0]] += 1 + elif isinstance(child, (ast.FunctionDef, ast.AsyncFunctionDef, ast.ClassDef)): + bound[child.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[id(tree)] = functions + return functions + + +def _index_value(node: ast.AST) -> str | int | None: + if isinstance(node, ast.Constant) and type(node.value) in (str, int): + return node.value + if (isinstance(node, ast.UnaryOp) and isinstance(node.op, ast.USub) + and isinstance(node.operand, ast.Constant) and type(node.operand.value) is int): + return -node.operand.value + return None + + +def _union(values: list[ast.AST]) -> ast.AST: + """Fold several definitions of one local into a finite selection node. + + The scan reports syntactic result possibilities, so a name written more than + once carries the union of the writes that precede the read. The synthetic + test is never inspected; only the arms are resolved. + """ + node = values[0] + for other in values[1:]: + test = ast.copy_location(ast.Constant(value=True), other) + node = ast.copy_location(ast.IfExp(test=test, body=node, orelse=other), other) + return node + + def scan_python_production( source: SourceFile, *, @@ -244,15 +314,36 @@ def scan_python_production( ``modules`` additionally lets one unrenamed re-export hop through a tracked module bind the owner. Longer chains and renamed re-exports stay unknown. Local aliases and complete branch selections resolve only at output sites. - General reassignment and parameter shadowing become unknown. Explicit call - metadata names only reviewed builder arguments; arbitrary calls are consumers. - Nested function returns belong to that function, not a registered enclosure. + Explicit call metadata names only reviewed builder arguments; arbitrary calls + are consumers. Nested function returns belong to that function, not a + registered enclosure. + + Three bounded local forms are recognized beyond a single straight-line + binding. A local written more than once resolves to the union of the writes + that textually precede the read, provided every store of that name is a + plain ``name = expression`` (loop, ``with``, ``except``, walrus, augmented, + unpacking, ``global`` and ``del`` rebindings are not ordered by this scan and + stay unknown). A local container mutated only through direct literal-key + subscript writes keeps its untouched keys, and a written key carries the + union of its initializer and every write; an alias, a method call, a deeper + or computed store, or passing the container to any call still discards it. + A call to an undecorated, non-generator, plainly-defined top-level function + of the same module resolves to the union of that function's own returns. + Arguments are never bound to parameters, so a returned parameter stays + unknown and the result is independent of the call site; recursion, imported + and attribute calls keep the ``call_result`` blocker. """ - tree = ast.parse(source.text, filename=source.path) + # The scan never mutates the tree, so one parse per file serves every + # vocabulary; synthetic selection nodes are built fresh, never spliced in. + tree = _parsed(source) bindings = _qualified_bindings(source, tree, enums, modules) call_arguments = call_arguments or {} calls = _qualified_bindings(source, tree, call_arguments, modules) return_paths = return_paths or {} + module_functions = _module_functions(tree) + call_memo: dict[tuple[str, str], tuple[frozenset[str], tuple[str, ...]]] = {} + environments: dict[tuple[int, str], SimpleNamespace] = {} + resolving: set[str] = set() result: list[Production] = [] @@ -264,7 +355,13 @@ def matches(node: ast.AST) -> bool: return (isinstance(node, ast.Subscript) and isinstance(node.slice, ast.Constant) and node.slice.value == field) - def scan_scope(body: list[ast.stmt], scope: str, parameters: set[str]) -> None: + def environment(body: list[ast.stmt], scope: str, parameters: set[str], + call_shadows: frozenset[str] = frozenset(), + own: frozenset[str] = frozenset()) -> SimpleNamespace: + """Build one scope's bounded local view and its resolvers, once.""" + cached = environments.get((id(body), scope)) + if cached is not None: + return cached nodes: list[ast.AST] = [] nested: list[ast.FunctionDef | ast.AsyncFunctionDef | ast.ClassDef] = [] @@ -293,50 +390,56 @@ def collect(node: ast.AST) -> None: exception_targets = {n.name for n in nodes if isinstance(n, ast.ExceptHandler) and n.name} deleted = {n.id for n in nodes if isinstance(n, ast.Name) and isinstance(n.ctx, ast.Del)} shadows = set(assigned) | parameters | nested_names | imported | exception_targets | deleted + # A same-module call binds to a top-level ``def``, so that definition is + # not itself a shadow; only a rebinding inside this scope or an + # enclosing one takes the name away from the module function. + # ``parameters`` also carries every enclosing owner shadow, including the + # module's own top-level definitions, so only this scope's real bindings + # may take a name away from the module function it would otherwise name. + rebinds = set(assigned) | set(own) | imported | exception_targets | deleted + if scope != '': + rebinds |= nested_names + calls_shadowed = frozenset(call_shadows) | rebinds local_bindings = {k: v for k, v in bindings.items() if k not in shadows} local_calls = {k: v for k, v in calls.items() if k not in shadows} - single_values = {} - for node in nodes: - if isinstance(node, ast.Assign) and len(node.targets) == 1 and isinstance(node.targets[0], ast.Name): - target = node.targets[0].id - if assigned[target] == 1 and target not in parameters: - single_values[target] = node.value - elif isinstance(node, ast.AnnAssign) and isinstance(node.target, ast.Name): - target = node.target.id - if assigned[target] == 1 and target not in parameters and node.value is not None: - single_values[target] = node.value - - def conditional_values(node: ast.If) -> dict[str, tuple[ast.AST, int]]: - # A complete if/elif/else defining a local in each arm is one finite - # selection. Partial branches, loops and general reassignments stay - # unknown; no assignment is itself an enum production site. - def arm(statements: list[ast.stmt]) -> dict[str, tuple[ast.AST, int]]: - if len(statements) == 1 and isinstance(statements[0], ast.If): - return conditional_values(statements[0]) - definitions = {} - for statement in statements: - if (isinstance(statement, ast.Assign) and len(statement.targets) == 1 - and isinstance(statement.targets[0], ast.Name)): - name = statement.targets[0].id - definitions[name] = (statement.value, definitions.get(name, (None, 0))[1] + 1) - return {name: item for name, item in definitions.items() if item[1] == 1} - left, right = arm(node.body), arm(node.orelse) - return {name: (ast.copy_location(ast.IfExp(test=node.test, body=left[name][0], - orelse=right[name][0]), node), left[name][1] + right[name][1]) - for name in left.keys() & right.keys()} + plain: dict[str, list[ast.AST]] = {} + for node in nodes: + target = value = None + if (isinstance(node, ast.Assign) and len(node.targets) == 1 + and isinstance(node.targets[0], ast.Name)): + target, value = node.targets[0].id, node.value + elif (isinstance(node, ast.AnnAssign) and isinstance(node.target, ast.Name) + and node.value is not None): + target, value = node.target.id, node.value + if target is not None: + plain.setdefault(target, []).append(value) + declared = {name for node in nodes if isinstance(node, (ast.Global, ast.Nonlocal)) + for name in node.names} + # Every store of the name must be one of those plain writes, so a value + # this scan cannot order never masquerades as a finite selection. + definitions = {name: values for name, values in plain.items() + if assigned[name] == len(values) and name not in parameters + and name not in declared and name not in deleted} + + # Resolve only local containers that have not been mutated through an + # unrecognized path or escaped. A direct literal-key subscript write is + # recorded against that key; anything else invalidates every alias, + # rather than turning a stale initializer into false scalar evidence. + written: dict[str, dict[str | int, list[ast.AST]]] = {} + recorded: set[int] = set() for node in nodes: - if isinstance(node, ast.If): - for name, (value, count) in conditional_values(node).items(): - if assigned[name] == count and name not in parameters: - single_values[name] = value - - # Resolve only local containers that have not been mutated or escaped. - # A subscript write through an alias invalidates every alias, rather - # than turning a stale initializer into false scalar output evidence. - containers = {name for name, value in single_values.items() - if isinstance(value, (ast.List, ast.Dict, ast.Set))} - aliases = [(name, value.id) for name, value in single_values.items() if isinstance(value, ast.Name)] + if isinstance(node, ast.Assign) and len(node.targets) == 1: + store = node.targets[0] + if (isinstance(store, ast.Subscript) and isinstance(store.value, ast.Name) + and not isinstance(store.slice, ast.Slice) + and (key := _index_value(store.slice)) is not None): + recorded.add(id(store)) + written.setdefault(store.value.id, {}).setdefault(key, []).append(node.value) + containers = {name for name, values in definitions.items() + if any(isinstance(value, (ast.List, ast.Dict, ast.Set)) for value in values)} + aliases = [(name, value.id) for name, values in definitions.items() + for value in values if isinstance(value, ast.Name)] unsafe: set[str] = set() def root_name(node: ast.AST) -> str | None: @@ -346,6 +449,8 @@ def root_name(node: ast.AST) -> str | None: for node in nodes: if isinstance(node, (ast.Attribute, ast.Subscript)) and isinstance(node.ctx, (ast.Store, ast.Del)): + if id(node) in recorded: + continue if name := root_name(node): unsafe.add(name) elif isinstance(node, ast.Call): @@ -354,6 +459,9 @@ def root_name(node: ast.AST) -> str | None: for argument in [*node.args, *(kw.value for kw in node.keywords)]: if isinstance(argument, ast.Name): unsafe.add(argument.id) + # A second name for the same container would let a write land outside + # this key map, so an aliased container keeps no key-precise evidence. + unsafe.update(name for name in written if name in {n for pair in aliases for n in pair}) for group in (containers, unsafe): changed = True while changed: @@ -363,46 +471,94 @@ def root_name(node: ast.AST) -> str | None: group.update((left, right)) changed = len(group) != before for name in containers & unsafe: - single_values.pop(name, None) + definitions.pop(name, None) + for name in unsafe: + written.pop(name, None) + + blockers: list[str] = [] + + def blocked(label: str) -> bool: + blockers.append(label) + return True def bound(node: ast.AST | None, seen: frozenset[str]) -> tuple[ast.AST | None, frozenset[str]]: - while isinstance(node, ast.Name) and node.id in single_values and node.id not in seen: - definition = single_values[node.id] - if (definition.lineno, definition.col_offset) >= (node.lineno, node.col_offset): + while isinstance(node, ast.Name) and node.id in definitions and node.id not in seen: + values = [value for value in definitions[node.id] + if (value.lineno, value.col_offset) < (node.lineno, node.col_offset)] + if not values: break seen = seen | {node.id} - node = definition + node = values[0] if len(values) == 1 else _union(values) return node, seen - def index_value(node: ast.AST) -> str | int | None: - if isinstance(node, ast.Constant) and type(node.value) in (str, int): - return node.value - if (isinstance(node, ast.UnaryOp) and isinstance(node.op, ast.USub) - and isinstance(node.operand, ast.Constant) and type(node.operand.value) is int): - return -node.operand.value - return None - - def lookup(container: ast.AST | None, key: str | int | None) -> tuple[list[ast.AST], bool]: + def flatten(container: ast.Dict, seen: frozenset[str], + depth: int = 0) -> tuple[list[tuple[str | int, ast.AST]], bool] | None: + """Expand ``**`` spreads of statically known dict literals, in write order. + + A spread whose operand is not a finite selection of dict literals + with literal keys could overwrite any key, so the whole lookup falls + back to the unknown-key answer instead of trusting a literal entry. + """ + if depth > 4: + return None + pairs: list[tuple[str | int, ast.AST]] = [] + spread = False + for key, value in zip(container.keys, container.values, strict=True): + if key is not None: + index = _index_value(key) + if index is None: + return None + pairs.append((index, value)) + continue + spread = True + arms = [value] + while arms: + arm, visited = bound(arms.pop(), seen) + if isinstance(arm, ast.IfExp): + arms.extend((arm.body, arm.orelse)) + continue + if not isinstance(arm, ast.Dict): + return None + inner = flatten(arm, visited, depth + 1) + if inner is None: + return None + pairs.extend(inner[0]) + return pairs, spread + + def lookup(container: ast.AST | None, key: str | int | None, + seen: frozenset[str] = frozenset(), absent_ok: bool = False) -> tuple[list[ast.AST], bool]: + # ``absent_ok`` says a recorded write already supplies this key, so an + # initializer that does not carry it is not an unknown boundary. if isinstance(container, (ast.Tuple, ast.List)): if type(key) is int: - return ([container.elts[key]], False) if -len(container.elts) <= key < len(container.elts) else ([], blocked('dynamic_key')) + if -len(container.elts) <= key < len(container.elts): + return [container.elts[key]], False + return [], (False if absent_ok else blocked('dynamic_key')) if key is not None: return [], blocked('dynamic_key') return list(container.elts), blocked('dynamic_key') if isinstance(container, ast.Dict): - keys = [index_value(k) if k is not None else None for k in container.keys] - if key is not None and all(k is not None for k in keys): - # Python dict construction keeps the last duplicate key. - found = [v for k, v in zip(keys, container.values, strict=True) if k == key] - return ([found[-1]], False) if found else ([], blocked('dynamic_key')) - return list(container.values), blocked('dynamic_key') + expanded = flatten(container, seen) + if expanded is None: + return list(container.values), blocked('dynamic_key') + pairs, spread = expanded + if key is None: + return [value for _, value in pairs], blocked('dynamic_key') + found = [value for index, value in pairs if index == key] + if not found: + return [], (False if absent_ok else blocked('dynamic_key')) + # Python dict construction keeps the last duplicate key; an + # optional spread makes each contributor a live possibility. + return (found if spread else [found[-1]]), False return [], blocked('unstable_local' if isinstance(container, ast.Name) else 'other') - blockers: list[str] = [] - - def blocked(label: str) -> bool: - blockers.append(label) - return True + def element(root: str | None, container: ast.AST | None, key: str | int | None, + seen: frozenset[str] = frozenset()) -> tuple[list[ast.AST], bool]: + updates = written.get(root or '') + extra = [] if not updates else (updates.get(key, []) if key is not None + else [v for values in updates.values() for v in values]) + choices, unknown = lookup(container, key, seen, absent_ok=bool(extra)) + return [*choices, *extra], unknown def resolve(node: ast.AST | None, seen: frozenset[str] = frozenset(), *, enum_only: bool = False) -> tuple[set[str], bool]: node, seen = bound(node, seen) @@ -414,8 +570,9 @@ def resolve(node: ast.AST | None, seen: frozenset[str] = frozenset(), *, enum_on if isinstance(node.slice, ast.Slice) or (isinstance(node.slice, ast.Constant) and type(node.slice.value) not in (str, int)): return set(), blocked('dynamic_key') + root = node.value.id if isinstance(node.value, ast.Name) else None container, visited = bound(node.value, seen) - choices, unknown = lookup(container, index_value(node.slice)) + choices, unknown = element(root, container, _index_value(node.slice), visited) known: set[str] = set() for value in choices: part, unresolved = resolve(value, visited, enum_only=enum_only) @@ -442,13 +599,25 @@ def resolve(node: ast.AST | None, seen: frozenset[str] = frozenset(), *, enum_on return enum_object_value(node.value, seen) return set(), blocked('attribute_read') if isinstance(node, ast.Call): - return set(), blocked('call_result') + hit = same_module_call(node, 'enum' if enum_only else 'value') + return hit if hit is not None else (set(), blocked('call_result')) if isinstance(node, ast.Name): return set(), blocked('unstable_local') if node is None: return set(), blocked('other') return set(), blocked('other') + def same_module_call(node: ast.Call, mode: str) -> tuple[set[str], bool] | None: + if not isinstance(node.func, ast.Name) or node.func.id in calls_shadowed: + return None + hit = call_values(node.func.id, mode) + if hit is None: + return None + values, reasons = hit + for reason in reasons: + blocked(reason) + return set(values), bool(reasons) + def enum_object_value(node: ast.AST, seen: frozenset[str]) -> tuple[set[str], bool]: node, seen = bound(node, seen) if isinstance(node, ast.IfExp): @@ -456,6 +625,13 @@ def enum_object_value(node: ast.AST, seen: frozenset[str]) -> tuple[set[str], bo return set().union(*(v for v, _ in parts)), any(u for _, u in parts) if isinstance(node, ast.Attribute) and isinstance(node.value, ast.Name) and node.value.id in local_bindings: return resolve(node, seen, enum_only=True) + if isinstance(node, ast.Call): + # Only a same-module function that returns owner members as enum + # objects has another ``.value``; a function handing back + # ``Action.RUN.value`` already returns the serialized string. + hit = same_module_call(node, 'object') + if hit is not None and hit[0]: + return hit # A serialized string (including Action.RUN.value) is not an enum # object with another .value attribute. return set(), blocked('serialized_value') @@ -463,15 +639,76 @@ def enum_object_value(node: ast.AST, seen: frozenset[str]) -> tuple[set[str], bo def returned(node: ast.AST | None, path: tuple[str | int, ...], seen: frozenset[str] = frozenset()) -> tuple[set[str], bool]: if not path: return resolve(node, seen) + root = node.id if isinstance(node, ast.Name) else None node, seen = bound(node, seen) - choices, unknown = lookup(node, path[0]) + choices, unknown = element(root, node, path[0], seen) parts = [returned(value, path[1:], seen) for value in choices] return set().union(*(v for v, _ in parts)), unknown or any(u for _, u in parts) + built = SimpleNamespace(nodes=nodes, nested=nested, shadows=shadows, blockers=blockers, + calls_shadowed=calls_shadowed, local_calls=local_calls, + resolve=resolve, returned=returned, enum_object=enum_object_value) + environments[(id(body), scope)] = built + return built + + def call_values(name: str, mode: str) -> tuple[frozenset[str], tuple[str, ...]] | None: + """Union of one same-module function's own returns, or ``None``. + + ``mode`` asks what the caller needs of each return: its written value, + only owner members (``enum``), or the member behind an enum object + (``object``). The last is not the same question as the first: a function + returning ``Action.RUN.value`` hands back a string that has no further + ``.value``, so it answers ``object`` with nothing. + + Call arguments are never bound to parameters, so a returned parameter + stays unknown and the answer does not depend on the call site; it is + memoised per module scan. A call reached from inside its own callee + chain keeps the ``call_result`` blocker instead of unrolling recursion. + A bare ``return`` or a fall-through yields ``None``, which is not a + vocabulary value: it contributes nothing and blocks nothing. + """ + target = module_functions.get(name) + if target is None or name in resolving: + return None + key = (name, mode) + if key not in call_memo: + resolving.add(name) + try: + args = target.args + params = {a.arg for a in (*args.posonlyargs, *args.args, *args.kwonlyargs)} + params.update(a.arg for a in (args.vararg, args.kwarg) if a) + env = environment(target.body, name, params | module_env.shadows, + module_env.calls_shadowed, frozenset(params)) + values: set[str] = set() + unknown = False + start = len(env.blockers) + for node in env.nodes: + if isinstance(node, ast.Return) and node.value is not None: + part, missing = (env.enum_object(node.value, frozenset()) if mode == 'object' + else env.resolve(node.value, enum_only=mode == 'enum')) + values |= part + unknown |= missing + first = env.blockers[start] if len(env.blockers) > start else 'call_result' + del env.blockers[start:] + call_memo[key] = (frozenset(values), (first,) if unknown else ()) + finally: + resolving.discard(name) + return call_memo[key] + + def scan_scope(body: list[ast.stmt], scope: str, parameters: set[str], + call_shadows: frozenset[str] = frozenset(), own: frozenset[str] = frozenset(), + env: SimpleNamespace | None = None) -> None: + env = env if env is not None else environment(body, scope, parameters, call_shadows, own) + blockers = env.blockers + def record(node: ast.AST | None, form: str, location: ast.AST) -> None: - blockers.clear() - values, unknown = (returned(node, return_paths.get(scope, ())) if form == 'return' else resolve(node)) - blocker = blockers[0] if blockers else None + # Reasons are read back by position: one scope's environment is + # shared with same-module call resolution, which may nest inside. + start = len(blockers) + values, unknown = (env.returned(node, return_paths.get(scope, ())) + if form == 'return' else env.resolve(node)) + blocker = blockers[start] if len(blockers) > start else None + del blockers[start:] if node is None and form == 'assignment': # A bare annotation declares the field; there is no value to resolve. blocker = 'annotation_only' @@ -481,7 +718,7 @@ def record(node: ast.AST | None, form: str, location: ast.AST) -> None: result.append(Production(f'{source.path}::{scope}', location.lineno, form, frozenset(values), unknown, blocker if unknown else None)) - for node in nodes: + for node in env.nodes: if isinstance(node, ast.Assign): if field and any(matches(t) for t in node.targets): record(node.value, 'assignment', node) @@ -492,7 +729,7 @@ def record(node: ast.AST | None, form: str, location: ast.AST) -> None: if isinstance(key, ast.Constant) and key.value == field: record(value, 'dict', node) elif isinstance(node, ast.Call): - output_arguments = local_calls.get(node.func.id, {}) if isinstance(node.func, ast.Name) else {} + output_arguments = env.local_calls.get(node.func.id, {}) if isinstance(node.func, ast.Name) else {} for kw in node.keywords: if kw.arg in output_arguments: record(kw.value, 'call_argument', node) @@ -505,10 +742,16 @@ def record(node: ast.AST | None, form: str, location: ast.AST) -> None: if scope in return_functions: record(node.value, 'return', node) else: - values, unknown = resolve(node.value, enum_only=True) + start = len(blockers) + values, unknown = env.resolve(node.value, enum_only=True) + # An owner-member result keeps its reason too; an unlabelled + # unknown would be invisible in the report breakdown. + reason = blockers[start] if len(blockers) > start else None + del blockers[start:] if values: - result.append(Production(f'{source.path}::{scope}', node.lineno, 'enum_result', frozenset(values), unknown)) - for child in nested: + result.append(Production(f'{source.path}::{scope}', node.lineno, 'enum_result', + frozenset(values), unknown, reason if unknown else None)) + for child in env.nested: name = child.name if scope == '' else f'{scope}.{child.name}' params: set[str] = set() if not isinstance(child, ast.ClassDef): @@ -516,7 +759,8 @@ def record(node: ast.AST | None, form: str, location: ast.AST) -> None: params = {a.arg for a in (*args.posonlyargs, *args.args, *args.kwonlyargs)} params.update(a.arg for a in (args.vararg, args.kwarg) if a) # A nested closure might shadow an owner in any enclosing scope. - scan_scope(child.body, name, params | shadows) + scan_scope(child.body, name, params | env.shadows, env.calls_shadowed, frozenset(params)) - scan_scope(tree.body, '', set()) + module_env = environment(tree.body, '', set()) + scan_scope(tree.body, '', set(), frozenset(), frozenset(), module_env) return sorted(set(result), key=lambda row: (row.site, row.line, row.form, sorted(row.values))) diff --git a/scripts/semantic_production_scan.mjs b/scripts/semantic_production_scan.mjs index d1a6b0efec..95d437414f 100644 --- a/scripts/semantic_production_scan.mjs +++ b/scripts/semantic_production_scan.mjs @@ -16,19 +16,44 @@ for (const source of request.sources) { const field = request.field; const returns = new Set((request.return_functions ?? []).filter(x => x.startsWith(`${source.path}::`))); const unwrap = node => { - while (node && (ts.isParenthesizedExpression(node) || ts.isAsExpression(node) || ts.isSatisfiesExpression(node))) node = node.expression; + while (node && (ts.isParenthesizedExpression(node) || ts.isAsExpression(node) || + ts.isSatisfiesExpression(node) || ts.isNonNullExpression(node))) node = node.expression; return node; }; + // Say why a write stayed unknown using the same labels as the Python scanner, + // so one residue taxonomy covers both runtimes instead of a single catch-all. + const blockerFor = node => { + if (!node) return 'other'; + if (ts.isPropertyAccessExpression(node) || ts.isElementAccessExpression(node)) return 'attribute_read'; + if (ts.isCallExpression(node) || ts.isNewExpression(node) || ts.isAwaitExpression(node)) return 'call_result'; + if (ts.isIdentifier(node)) return 'unstable_local'; + if (ts.isObjectLiteralExpression(node) || ts.isArrayLiteralExpression(node) || + ts.isTemplateExpression(node)) return 'dynamic_key'; + return 'typescript_dynamic'; + }; + const merge = parts => ({ + values: [...new Set(parts.flatMap(part => part.values))].sort(), + unresolved: parts.some(part => part.unresolved), + blocker: parts.find(part => part.unresolved)?.blocker, + }); const values = expression => { const node = unwrap(expression); - if (!node) return {values: [], unresolved: true}; + if (!node) return {values: [], unresolved: true, blocker: 'other'}; if (ts.isStringLiteral(node) || ts.isNoSubstitutionTemplateLiteral(node)) return {values: node.text ? [node.text] : [], unresolved: false}; if (node.kind === ts.SyntaxKind.NullKeyword) return {values: [], unresolved: false}; - if (ts.isConditionalExpression(node)) { - const left = values(node.whenTrue), right = values(node.whenFalse); - return {values: [...new Set([...left.values, ...right.values])].sort(), unresolved: left.unresolved || right.unresolved}; + // ``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.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. + if (ts.isBinaryExpression(node) && [ts.SyntaxKind.BarBarToken, + ts.SyntaxKind.QuestionQuestionToken].includes(node.operatorToken.kind)) { + return merge([values(node.left), values(node.right)]); } - return {values: [], unresolved: true}; + if (ts.isCallExpression(node) && ts.isIdentifier(node.expression) && + node.expression.text === 'String' && node.arguments.length === 1) return values(node.arguments[0]); + return {values: [], unresolved: true, blocker: blockerFor(node)}; }; const staticName = expression => { const node = unwrap(expression); diff --git a/tests/architecture/test_semantic_producer_binding.py b/tests/architecture/test_semantic_producer_binding.py new file mode 100644 index 0000000000..4aa2f8fcde --- /dev/null +++ b/tests/architecture/test_semantic_producer_binding.py @@ -0,0 +1,300 @@ +"""Counterexamples for the bounded binding forms the producer scan recognizes. + +Each form here narrows an ``unresolved`` blocker, so every one needs a negative +twin: a site the scan must keep unresolved rather than call dead. Shrinking the +residue by loosening the rule is the failure this file is meant to catch. +""" +from __future__ import annotations + +import ast +import time + +import pytest + +from loopx.semantics.inventory import SourceFile +from loopx.semantics.python_production import scan_python_production + +OWNER = 'loopx/quota/owner.py::Action' +ENUMS = {OWNER: {'RUN': 'run', 'WAIT': 'wait'}} +CONSUMER = 'loopx/quota/client.py' + + +def scan(text, *, returns=(), paths=None, calls=None, field='action', enums=ENUMS): + return scan_python_production(SourceFile(CONSUMER, '.py', text), field=field, enums=enums, + return_functions=frozenset(returns), return_paths=paths, + call_arguments=calls) + + +def known(rows): + return set().union(*(row.values for row in rows if row.form != 'keyword_unproved')) + + +def blockers(rows): + return {row.blocker for row in rows if row.unresolved} + + +def at(rows, scope): + """Only the consumer's own rows; a helper's own returns are its evidence.""" + return [row for row in rows if row.site == f'{CONSUMER}::{scope}'] + + +# --- same-module call results ------------------------------------------------- + + +def test_same_module_call_resolves_to_the_callee_own_returns(): + rows = scan('def pick(flag):\n return "run" if flag else "wait"\n' + 'def emit():\n return {"action": pick(True)}\n') + assert known(rows) == {'run', 'wait'} + assert not any(row.unresolved for row in rows) + + +def test_same_module_call_keeps_the_callee_unknown_portion(): + """A bound call reports the callee's own reason, not a blanket call_result.""" + rows = scan('def pick(flag):\n return "run" if flag else dynamic()\n' + 'def emit():\n return {"action": pick(True)}\n') + assert known(rows) == {'run'} + assert blockers(rows) == {'call_result'} + + +def test_call_arguments_are_never_bound_to_callee_parameters(): + """A returned parameter stays unknown however literal the argument is.""" + rows = scan('def pick(choice):\n return choice\n' + 'def emit():\n return {"action": pick("run")}\n') + assert known(rows) == set() + assert blockers(rows) == {'unstable_local'} + + +def test_enum_object_returned_by_a_same_module_call_supplies_value(): + rows = scan('from .owner import Action\ndef pick():\n return Action.RUN\n' + 'def emit():\n choice = pick()\n return {"action": choice.value}\n') + assert known(rows) == {'run'} + assert not any(row.unresolved for row in rows) + + +def test_serialized_result_is_not_an_enum_object_with_a_value_attribute(): + rows = at(scan('from .owner import Action\ndef pick():\n return Action.RUN.value\n' + 'def emit():\n choice = pick()\n return {"action": choice.value}\n'), 'emit') + assert known(rows) == set() + assert blockers(rows) == {'serialized_value'} + + +@pytest.mark.parametrize('definition, reason', [ + # A decorator can replace the returned object entirely. + ('@wrap\ndef pick():\n return "run"\n', 'call_result'), + # await of a coroutine is a different expression; a bare call is not the value. + ('async def pick():\n return "run"\n', 'call_result'), + # A generator yields; the call returns the iterator, not a member. + ('def pick():\n yield "run"\n', 'call_result'), + # A second top-level binding takes the name away from the definition. + ('def pick():\n return "run"\npick = other\n', 'call_result'), + ('def pick():\n return "run"\nfrom .elsewhere import pick\n', 'call_result'), +]) +def test_unbindable_definitions_keep_the_site_unresolved(definition, reason): + rows = scan(definition + 'def emit():\n return {"action": pick()}\n') + assert known(rows) == set() + assert blockers(rows) == {reason} + + +def test_imported_and_attribute_calls_are_not_same_module_definitions(): + rows = scan('from .elsewhere import pick\nimport helper\n' + 'def emit():\n return {"action": pick(), "other": helper.pick()}\n') + assert known(rows) == set() + assert blockers(rows) == {'call_result'} + + +def test_locally_rebound_name_does_not_borrow_the_module_definition(): + rows = scan('def pick():\n return "run"\n' + 'def emit(pick):\n return {"action": pick()}\n') + assert known(rows) == set() + assert blockers(rows) == {'call_result'} + + +def test_recursive_call_chain_terminates_and_stays_unresolved(): + rows = scan('def left():\n return right()\ndef right():\n return left()\n' + 'def emit():\n return {"action": left()}\n') + assert known(rows) == set() + assert blockers(rows) == {'call_result'} + + +def test_a_callee_that_only_raises_produces_no_value_and_no_blocker(): + rows = scan('def pick():\n raise ValueError("no route")\n' + 'def emit():\n return {"action": pick()}\n') + assert known(rows) == set() + assert not any(row.unresolved for row in rows) + + +# --- ordered rebinding of a local -------------------------------------------- + + +def test_rebound_local_unions_the_writes_that_precede_the_read(): + rows = scan('from .owner import Action\ndef emit(flag):\n choice = Action.RUN.value\n' + ' if flag:\n choice = Action.WAIT.value\n return {"action": choice}\n') + assert known(rows) == {'run', 'wait'} + assert not any(row.unresolved for row in rows) + + +def test_a_write_after_the_read_is_not_a_definition_for_that_read(): + rows = scan('from .owner import Action\ndef emit(flag):\n choice = Action.RUN.value\n' + ' packet = {"action": choice}\n choice = Action.WAIT.value\n return packet\n') + assert known(rows) == {'run'} + assert not any(row.unresolved for row in rows) + + +def test_a_rebound_local_keeps_its_unknown_arm_visible(): + rows = scan('from .owner import Action\ndef emit(flag):\n choice = Action.RUN.value\n' + ' if flag:\n choice = dynamic()\n return {"action": choice}\n') + assert known(rows) == {'run'} + assert blockers(rows) == {'call_result'} + + +@pytest.mark.parametrize('rebind', [ + 'for choice in options: pass', + 'with opened() as choice: pass', + 'choice += suffix', + 'choice, extra = pair()', + 'del choice', + 'print(choice := dynamic())', +]) +def test_stores_this_scan_cannot_order_leave_the_local_unknown(rebind): + """Only a plain ``name = expression`` is an ordered write; nothing else is.""" + rows = scan('from .owner import Action\ndef emit():\n choice = Action.RUN.value\n ' + + rebind + '\n return {"action": choice}\n') + assert known(rows) == set() + assert blockers(rows) == {'unstable_local'} + + +def test_a_global_declaration_takes_the_name_out_of_this_scope(): + rows = scan('from .owner import Action\ndef emit():\n global choice\n' + ' choice = Action.RUN.value\n return {"action": choice}\n') + assert known(rows) == set() + assert blockers(rows) == {'unstable_local'} + + +# --- key-precise container writes -------------------------------------------- + + +def test_untouched_keys_survive_a_literal_key_write(): + rows = scan('from .owner import Action\ndef emit(flag):\n' + ' packet = {"action": Action.RUN.value, "note": ""}\n' + ' if flag:\n packet["note"] = "changed"\n return packet\n', + returns=['emit'], paths={'emit': ('action',)}) + assert known(rows) == {'run'} + assert not any(row.unresolved for row in rows) + + +def test_a_written_key_carries_every_contributing_write(): + rows = scan('from .owner import Action\ndef emit(flag):\n' + ' packet = {"action": Action.RUN.value}\n' + ' if flag:\n packet["action"] = Action.WAIT.value\n return packet\n', + returns=['emit'], paths={'emit': ('action',)}) + assert known(rows) == {'run', 'wait'} + assert not any(row.unresolved for row in rows) + + +def test_a_key_supplied_only_by_a_write_is_not_an_unknown_boundary(): + rows = scan('from .owner import Action\ndef emit():\n packet = {}\n' + ' packet["action"] = Action.RUN.value\n return packet\n', + returns=['emit'], paths={'emit': ('action',)}) + assert known(rows) == {'run'} + assert not any(row.unresolved for row in rows) + + +def test_an_unresolved_write_to_the_read_key_stays_unresolved(): + rows = scan('from .owner import Action\ndef emit(flag):\n' + ' packet = {"action": Action.RUN.value}\n' + ' if flag:\n packet["action"] = dynamic()\n return packet\n', + returns=['emit'], paths={'emit': ('action',)}) + assert known(rows) == {'run'} + assert blockers(rows) == {'call_result'} + + +@pytest.mark.parametrize('mutation', [ + # A second name could carry a write this key map never sees. + 'alias = packet\n alias["action"] = dynamic()', + # A computed key could land on any key at all. + 'packet[key()] = dynamic()', + # A deeper store is not a write to a key of this container. + 'packet["action"]["kind"] = dynamic()', + # A method or an escape can rewrite the whole container. + 'packet.update(other)', + 'consume(packet)', + 'del packet["action"]', +]) +def test_writes_outside_the_recognized_form_discard_the_container(mutation): + rows = [row for row in scan('from .owner import Action\ndef emit():\n' + ' packet = {"action": Action.RUN.value}\n ' + mutation + '\n return packet\n', + returns=['emit'], paths={'emit': ('action',)}) if row.form == 'return'] + assert known(rows) == set() + assert rows and all(row.unresolved for row in rows) + + +# --- dict literal spreads ----------------------------------------------------- + + +def test_a_spread_of_known_literals_does_not_hide_a_sibling_key(): + rows = scan('from .owner import Action\ndef emit(flag):\n' + ' packet = {"action": Action.RUN.value, **({"note": "x"} if flag else {})}\n' + ' return packet\n', returns=['emit'], paths={'emit': ('action',)}) + assert known(rows) == {'run'} + assert not any(row.unresolved for row in rows) + + +def test_a_spread_that_may_carry_the_key_keeps_both_possibilities(): + rows = scan('from .owner import Action\ndef emit(flag):\n' + ' packet = {"action": Action.RUN.value, **({"action": Action.WAIT.value} if flag else {})}\n' + ' return packet\n', returns=['emit'], paths={'emit': ('action',)}) + assert known(rows) == {'run', 'wait'} + assert not any(row.unresolved for row in rows) + + +@pytest.mark.parametrize('spread', ['**overrides', '**dict(overrides)', '**{key(): "x"}']) +def test_an_unknown_spread_could_overwrite_any_key(spread): + rows = scan('from .owner import Action\ndef emit(overrides):\n' + ' packet = {"action": Action.RUN.value, ' + spread + '}\n return packet\n', + returns=['emit'], paths={'emit': ('action',)}) + assert blockers(rows) == {'dynamic_key'} + + +# --- the residue stays honest ------------------------------------------------- + + +def test_an_unbound_site_is_unresolved_and_never_silently_dropped(): + """No recognized producer means unresolved; it never means dead.""" + rows = scan('def emit(payload):\n return {"action": payload.get("action")}\n') + assert len(rows) == 1 + assert rows[0].unresolved and rows[0].blocker == 'call_result' + assert rows[0].values == frozenset() + + +def test_every_recognized_form_still_labels_what_it_could_not_bind(): + rows = scan('from .owner import Action\ndef pick(flag):\n return Action.RUN.value if flag else late()\n' + 'def emit(flag):\n packet = {"action": pick(flag)}\n' + ' packet["note"] = dynamic()\n return packet\n', + returns=['emit'], paths={'emit': ('action',)}) + assert known(at(rows, 'emit')) == {'run'} + assert all(row.blocker for row in rows if row.unresolved) + + +def test_deep_call_chains_stay_bounded(): + """The memo and the recursion guard keep a long chain linear, not explosive.""" + depth = 60 + text = 'def step0():\n return "run"\n' + text += ''.join(f'def step{i}():\n return step{i - 1}() or step{i - 1}()\n' + for i in range(1, depth)) + text += f'def emit():\n return {{"action": step{depth - 1}()}}\n' + started = time.perf_counter() + rows = scan(text) + assert known(rows) == {'run'} + assert time.perf_counter() - started < 5.0 + + +def test_synthetic_selection_nodes_never_enter_the_shared_tree(): + """Rebinding folds a union for the read only; the parsed tree is untouched.""" + text = ('from .owner import Action\ndef emit(flag):\n choice = Action.RUN.value\n' + ' if flag:\n choice = Action.WAIT.value\n return {"action": choice}\n') + source = SourceFile(CONSUMER, '.py', text) + first = scan_python_production(source, field='action', enums=ENUMS) + before = ast.dump(ast.parse(text)) + second = scan_python_production(source, field='action', enums=ENUMS) + assert first == second + assert ast.dump(ast.parse(text)) == before diff --git a/tests/architecture/test_semantic_python_production.py b/tests/architecture/test_semantic_python_production.py index faf6299705..59e41a7d0d 100644 --- a/tests/architecture/test_semantic_python_production.py +++ b/tests/architecture/test_semantic_python_production.py @@ -58,7 +58,14 @@ def test_single_local_variable_and_reassignment_boundary(): rows = scan('def emit(flag):\n code = "run" if flag else "wait"\n return code\n', returns=['emit']) assert known(rows) == {'run', 'wait'} assert not any(r.unresolved for r in rows) + # An ordered rebinding is a finite selection, so the literal arm is real + # evidence; the unknown arm still keeps the row unresolved. + # tests/architecture/test_semantic_producer_binding.py covers the form. rows = scan('def emit(flag):\n code = "run"\n if flag:\n code = dynamic()\n return code\n', returns=['emit']) + assert known(rows) == {'run'} + assert rows[0].unresolved + # A store this scan cannot order erases the local altogether. + rows = scan('def emit(codes):\n code = "run"\n for code in codes:\n pass\n return code\n', returns=['emit']) assert known(rows) == set() assert rows[0].unresolved From bf7a7cc4112c00a41b5b238086e6d788c8682fc2 Mon Sep 17 00:00:00 2001 From: song <22676124+songoow@users.noreply.github.com> Date: Thu, 17 Sep 2026 21:40:26 -0400 Subject: [PATCH 2/3] fix(semantics): keep a local unknown when a back edge can carry a later write The multi-write form resolved a local to the writes that textually precede the read. Textual position is execution order only where no back edge crosses it, and the filter did not look for one. A local written at the bottom of a loop body and read at the top resolved to the value written before the loop, and the site reported `unresolved=False` with no blocker. That is the one failure mode that turns an unknown into wrong evidence instead of into a smaller residue. F1 asks whether a producer writes only registered values; a producer that emits an unregistered value on every iteration after the first passed it, because the scan had reported a closed value set that was not closed. Four shapes reproduce it: a `for` back edge, a `while` back edge, a write carried by an outer loop, and a `finally` that rebinds. A negative subscript store had the same shape. `table[-1]` names the same slot as some non-negative index whose number depends on the container's length, so recording it under the key `-1` left a read of `table[0]` looking at an initializer the write had already replaced; a one-element list reported the overwritten value and called the site resolved. Both now stay unresolved. The name is not a finite selection when a write shares an enclosing loop with the read, and a negative store sends the container down the existing invalidation path, so the answer is `unstable_local` rather than a value the code does not produce. Measured on the tree: unresolved sites stay at 40 and the blocker split is unchanged at `annotation_only=5, argument_name_only=10, attribute_read=7, call_result=14, other=1, unstable_local=3`. No site was resolving through the unsound path, so the generality bought nothing that this takes away. Two positive tests hold the ordering the form was built for: a straight-line rebinding still resolves, and a single write inside a loop is still its only value. Refs #4447 B2. Co-Authored-By: Claude Opus 5 (1M context) Signed-off-by: song <22676124+songoow@users.noreply.github.com> --- .../semantic-vocabulary-convergence-v0.md | 47 +++++--- ...emantic-vocabulary-convergence-v0.zh-CN.md | 34 ++++-- loopx/semantics/python_production.py | 45 ++++++-- .../test_semantic_producer_binding.py | 109 ++++++++++++++++++ 4 files changed, 203 insertions(+), 32 deletions(-) diff --git a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md index 4d025fb4ac..a6cfa83393 100644 --- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md +++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md @@ -399,14 +399,15 @@ that function's own returns, with arguments never bound to parameters, so a returned parameter stays unknown and the result is independent of the call site; a local written more than once resolves to the union of the writes that textually precede the read, and only when every store of that name is a plain -`name = expression`; and a container mutated only through direct literal-key -subscript writes keeps its untouched keys, with a written key carrying the union -of its initializer and every write. Anything outside those conditions — a -decorator, `async def`, a generator, recursion, an imported or attribute call, a -loop, `with`, `except`, walrus, augmented, unpacking, `global` or `del` -rebinding, an alias, a method call, a computed or deeper store, an escape into a -call, or an unknown `**` spread — leaves the site unknown rather than admitting -a value. TypeScript object writes, assignments +`name = expression` **and** no write shares an enclosing loop with the read; +and a container mutated only through direct literal-key subscript writes keeps +its untouched keys, with a written key carrying the union of its initializer and +every write. Anything outside those conditions — a decorator, `async def`, a +generator, recursion, an imported or attribute call, a back edge that carries a +later write to the read, a `with`, `except`, walrus, augmented, unpacking, +`global` or `del` rebinding, an alias, a method call, a computed, negative or +deeper store, an escape into a call, or an unknown `**` spread — leaves the site +unknown rather than admitting a value. TypeScript object writes, assignments and declared returns use the repository's TypeScript parser rather than regex, and report the same blocker vocabulary as the Python scanner, so one residue taxonomy covers both runtimes. @@ -1109,14 +1110,29 @@ introduce a competing target state. local rebinding and recursion all keep the `call_result` blocker. 2. **Ordered rebinding of a local.** A local written more than once resolves to the union of the writes that textually precede the read, and only when every - store of that name is a plain `name = expression`. Loop, `with`, `except`, - walrus, augmented, unpacking, `global` and `del` rebindings are not ordered - by this scan and erase the local. + store of that name is a plain `name = expression` and no write shares an + enclosing loop with the read. `with`, `except`, walrus, augmented, + unpacking, `global` and `del` rebindings are not ordered by this scan and + erase the local. + + Textual position is execution order only where no back edge crosses it. A + write later in a loop body reaches the read at the top of the next + iteration, so the preceding-writes filter dropped a live value and reported + a closed value set that was not closed: a producer emitting an unregistered + value on every iteration after the first read as fully resolved, which is + the one failure mode that turns an unknown into wrong evidence rather than + into a smaller residue. Four shapes are pinned as regressions — a `for` + back edge, a `while` back edge, a write carried by an outer loop, and a + `finally` that rebinds — beside two positives that keep the ordering this + form was built for. 3. **Key-precise container writes.** A local container mutated only through direct literal-key subscript writes keeps its untouched keys, and a written key carries the union of its initializer and every write. An alias, a method - call, a computed or deeper store, a `del`, or passing the container to any - call still discards the container, as before. A `**` spread of statically + call, a computed or deeper store, a `del`, a negative index, or passing the + container to any call still discards the container. A negative index names + the same slot as a non-negative one whose number depends on the container's + length, so recording it against the key `-1` left a read of `table[0]` + looking at an initializer the write had already replaced. A `**` spread of statically known dict literals is flattened, so an optional spread no longer hides a sibling key; an unknown spread still makes every key dynamic. @@ -1130,7 +1146,10 @@ introduce a competing target state. invisible in the report breakdown. - **Result:** unresolved sites **41 → 40**, split `annotation_only=5, argument_name_only=10, attribute_read=7, call_result=14, - other=1, unstable_local=3`. All eight TypeScript sites are reclassified (five + other=1, unstable_local=3`. The back-edge and negative-index rules were added + after that measurement and left every number in it unchanged, so no site on + the tree was resolving through the unsound path: the generality had bought + nothing that the soundness fix takes away. All eight TypeScript sites are reclassified (five `attribute_read`, three `call_result`); none was resolvable, so that part is a taxonomy, not a shrink. The one site that closes is `driver.py::build_loopx_turn_plan:500`, which needed all three forms and the 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 96da6d4981..47d5cc16d4 100644 --- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md +++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md @@ -312,12 +312,13 @@ owner 成员结果及声明函数的标量返回。导入枚举的别名只解 **同模块内**一个未被装饰、非生成器、以普通 `def` 定义的顶层函数的调用，解析为 该函数自身全部 return 的并集，实参从不绑定到形参，因此返回形参仍为 unknown， 结果与调用点无关；被写入多次的局部变量解析为文本上位于该读取之前的那些写入的 -并集，且仅当该名字的每一次 store 都是普通的 `name = expression` 时成立；只经由 -直接字面量键下标写入被改动的容器保留其未被触碰的键，被写入的键携带其初始化值 -与每一次写入的并集。凡落在上述条件之外的——装饰器、`async def`、生成器、递归、 -导入调用或属性调用，循环、`with`、`except`、海象、增量赋值、解包、`global` 或 -`del` 造成的重绑定，别名、方法调用、计算键或更深层的 store、逃逸进调用，以及 -未知的 `**` 展开——都让该位点保持 unknown，而不是采信一个取值。 +并集，且仅当该名字的每一次 store 都是普通的 `name = expression`、**并且**没有 +任何写入与该读取处在同一个循环内时成立；只经由直接字面量键下标写入被改动的容器 +保留其未被触碰的键，被写入的键携带其初始化值与每一次写入的并集。凡落在上述条件 +之外的——装饰器、`async def`、生成器、递归、导入调用或属性调用，把靠后的写入带回 +读取处的回边，`with`、`except`、海象、增量赋值、解包、`global` 或 `del` 造成的 +重绑定，别名、方法调用、计算键、负索引或更深层的 store、逃逸进调用，以及未知的 +`**` 展开——都让该位点保持 unknown，而不是采信一个取值。 TypeScript 的对象写入、赋值及声明返回使用仓库的 TypeScript 解析器，并报告与 Python 扫描器相同的阻塞原因词汇，因此同一套残量分类覆盖两个 运行时。两个解析器都不执行被检查源码。这些是句法结果证据，不是可达性或全程序 @@ -899,12 +900,22 @@ PR review 保留这些层级。普通改动记录检查范围和理由，无共 以及递归，都继续保留 `call_result` 阻塞原因。 2. **局部变量的有序重绑定。**被写入多次的局部变量，解析为文本上位于该读取之前 的那些写入的并集，且仅当该名字的每一次 store 都是普通的 - `name = expression` 时才成立。循环、`with`、`except`、海象、增量赋值、解包、 - `global` 与 `del` 造成的重绑定不被本扫描定序，会直接抹掉该局部变量。 + `name = expression`、并且没有任何写入与该读取处在同一个循环内时才成立。 + `with`、`except`、海象、增量赋值、解包、`global` 与 `del` 造成的重绑定不被 + 本扫描定序，会直接抹掉该局部变量。 + + 只有在没有回边横跨的位置上，文本先后才等于执行先后。循环体里靠后的一次写入 + 会在下一轮迭代抵达位于顶部的读取，于是「取文本在前的写入」这条过滤会丢掉一个 + 活的取值，并报出一个并不封闭的取值集合：一个从第二轮迭代起就发出未注册取值的 + 生产者会被读作「完全解析」。这是唯一一种把未知变成错误证据、而不是变成更小残量 + 的失效方式。四种形态已被钉为回归——`for` 回边、`while` 回边、由外层循环携带的 + 写入、以及在 `finally` 中重绑定——旁边另有两条正例，守住这条形式本来要支持的定序。 3. **按键精确的容器写入。**只经由直接字面量键下标写入被改动的局部容器，保留其 未被触碰的键；被写入的键则携带其初始化值与每一次写入的并集。别名、方法调用、 - 计算键或更深层的 store、`del`，以及把容器作为任何调用的实参传出，仍然像以前 - 一样丢弃整个容器。对静态可知的 dict 字面量的 `**` 展开会被摊平，因此可选展开 + 计算键、负索引或更深层的 store、`del`，以及把容器作为任何调用的实参传出，仍然 + 丢弃整个容器。负索引指向的槽位，其序号取决于容器长度，与某个非负索引是同一个 + 槽；把它按键 `-1` 记录下来，会让对 `table[0]` 的读取仍然看到那次写入早已替换掉 + 的初始化值。对静态可知的 dict 字面量的 `**` 展开会被摊平，因此可选展开 不再遮蔽同级键；未知展开仍使所有键变为动态。 TypeScript 解析器补上了 Python 扫描器早已具备的两条可靠形式（`||` 与 `??` 的 @@ -920,6 +931,9 @@ PR review 保留这些层级。普通改动记录检查范围和理由，无共 唯一被关闭的位点是 `driver.py::build_loopx_turn_plan:500`，它同时需要三条形式加上 展开摊平。证据的改善超过数字所显示的：携带至少一个已知值的未解析行从 **2 → 7**。 注册表取值、预算与 producer 位点清单均未变化，也没有任何位点变为新可见或未注册。 + 回边规则与负索引规则是在这次测量之后补上的，补上后这组数字一个都没有变化：树上 + 没有任何一个位点是靠那条不可靠的路径解析出来的——那份「通用性」并没有换来任何 + 被这次可靠性修复夺走的东西。 - **有意不绑定，并记录原因：** - `annotation_only`（5）——五个全部是裸的 `effective_action: str` 字段声明， **根本没有值节点**。设计上不可证；issue 的归类得到确认。 diff --git a/loopx/semantics/python_production.py b/loopx/semantics/python_production.py index 689efd2db5..c1843a3960 100644 --- a/loopx/semantics/python_production.py +++ b/loopx/semantics/python_production.py @@ -323,10 +323,15 @@ def scan_python_production( that textually precede the read, provided every store of that name is a plain ``name = expression`` (loop, ``with``, ``except``, walrus, augmented, unpacking, ``global`` and ``del`` rebindings are not ordered by this scan and - stay unknown). A local container mutated only through direct literal-key - subscript writes keeps its untouched keys, and a written key carries the - union of its initializer and every write; an alias, a method call, a deeper - or computed store, or passing the container to any call still discards it. + stay unknown) **and** no write shares an enclosing loop with the read. + Textual position is execution order only where no back edge crosses it: a + write later in a loop body reaches the read at the top of the next + iteration, so such a name is not a finite selection and stays unknown. A + local container mutated only through direct literal-key subscript writes + keeps its untouched keys, and a written key carries the union of its + initializer and every write; an alias, a method call, a deeper or computed + store, a negative index (which names a slot whose number depends on the + container's length), or passing the container to any call still discards it. A call to an undecorated, non-generator, plainly-defined top-level function of the same module resolves to the union of that function's own returns. Arguments are never bound to parameters, so a returned parameter stays @@ -364,16 +369,23 @@ def environment(body: list[ast.stmt], scope: str, parameters: set[str], return cached nodes: list[ast.AST] = [] nested: list[ast.FunctionDef | ast.AsyncFunctionDef | ast.ClassDef] = [] + # Which loops enclose each node. A write inside a loop reaches a read in + # the same loop through the back edge, so their textual order says + # nothing about which value the read sees. + enclosing_loops: dict[int, frozenset[int]] = {} - def collect(node: ast.AST) -> None: + def collect(node: ast.AST, loops: frozenset[int] = frozenset()) -> None: if isinstance(node, (ast.FunctionDef, ast.AsyncFunctionDef, ast.ClassDef)): nested.append(node) return if isinstance(node, ast.Lambda): return nodes.append(node) + enclosing_loops[id(node)] = loops + if isinstance(node, (ast.For, ast.AsyncFor, ast.While)): + loops = loops | {id(node)} for child in ast.iter_child_nodes(node): - collect(child) + collect(child, loops) for statement in body: collect(statement) assigned = Counter(n.id for n in nodes if isinstance(n, ast.Name) and isinstance(n.ctx, ast.Store)) @@ -431,9 +443,14 @@ def collect(node: ast.AST) -> None: for node in nodes: if isinstance(node, ast.Assign) and len(node.targets) == 1: store = node.targets[0] + # A negative index names the same slot as a non-negative one + # whose number depends on the container's length, so it cannot + # be recorded against a key. Leaving it unrecorded sends the + # container down the existing invalidation path below. if (isinstance(store, ast.Subscript) and isinstance(store.value, ast.Name) and not isinstance(store.slice, ast.Slice) - and (key := _index_value(store.slice)) is not None): + and (key := _index_value(store.slice)) is not None + and not (type(key) is int and key < 0)): recorded.add(id(store)) written.setdefault(store.value.id, {}).setdefault(key, []).append(node.value) containers = {name for name, values in definitions.items() @@ -483,7 +500,19 @@ def blocked(label: str) -> bool: def bound(node: ast.AST | None, seen: frozenset[str]) -> tuple[ast.AST | None, frozenset[str]]: while isinstance(node, ast.Name) and node.id in definitions and node.id not in seen: - values = [value for value in definitions[node.id] + writes = definitions[node.id] + # Textual position is execution order only where no back edge + # crosses it. When a second write shares a loop with the read, + # the next iteration sees that write and the preceding-writes + # filter would drop a live value, so the name is not a finite + # selection and stays unknown. + if len(writes) > 1 and any( + enclosing_loops.get(id(value), frozenset()) + & enclosing_loops.get(id(node), frozenset()) + for value in writes + ): + break + values = [value for value in writes if (value.lineno, value.col_offset) < (node.lineno, node.col_offset)] if not values: break diff --git a/tests/architecture/test_semantic_producer_binding.py b/tests/architecture/test_semantic_producer_binding.py index 4aa2f8fcde..6d4b97ee72 100644 --- a/tests/architecture/test_semantic_producer_binding.py +++ b/tests/architecture/test_semantic_producer_binding.py @@ -298,3 +298,112 @@ def test_synthetic_selection_nodes_never_enter_the_shared_tree(): second = scan_python_production(source, field='action', enums=ENUMS) assert first == second assert ast.dump(ast.parse(text)) == before + + +# A write that textually follows a read still reaches it when a loop carries +# control back. The preceding-writes filter reads file position as execution +# order, so without these the scan reports the value that happens to appear +# first and marks the site fully resolved -- the one failure mode that turns an +# unknown into wrong evidence. F1 would then pass over a producer that emits an +# unregistered value on every iteration after the first. +@pytest.mark.parametrize('text', [ + # for-loop back edge: iteration 2 emits 'leaked' + 'def build(rows):\n' + ' chosen = "run"\n' + ' for row in rows:\n' + ' emit({"action": chosen})\n' + ' chosen = "leaked"\n', + # while-loop back edge + 'def build(rows):\n' + ' chosen = "run"\n' + ' while rows:\n' + ' emit({"action": chosen})\n' + ' chosen = "leaked"\n' + ' rows = rows[1:]\n', + # the carrying write sits in the outer loop, the read in the inner one + 'def build(rows):\n' + ' chosen = "run"\n' + ' for row in rows:\n' + ' for inner in row:\n' + ' emit({"action": chosen})\n' + ' chosen = "leaked"\n', + # finally runs after the read and feeds the next iteration + 'def build(rows):\n' + ' chosen = "run"\n' + ' for row in rows:\n' + ' try:\n' + ' emit({"action": chosen})\n' + ' finally:\n' + ' chosen = "leaked"\n', +]) +def test_a_loop_back_edge_leaves_the_local_unordered(text): + rows = [row for row in scan(text) if row.form == 'dict'] + assert rows, 'the dict write must still be observed' + assert all(row.unresolved for row in rows), ( + 'a write the back edge carries past the read makes the writes unorderable; ' + 'reporting only the textually earlier value states a closed value set that is not closed' + ) + assert blockers(rows) == {'unstable_local'} + assert 'leaked' not in known(rows) + + +def test_a_straight_line_rebinding_still_resolves(): + """The back-edge rule must not retract the ordering it was built for. + + Without a loop the preceding-writes filter is execution order, so a local + written twice before the read is still a finite selection. + """ + rows = [row for row in scan( + 'def build(flag):\n' + ' chosen = "run"\n' + ' if flag:\n' + ' chosen = "wait"\n' + ' return {"action": chosen}\n', + ) if row.form == 'dict'] + assert known(rows) == {'run', 'wait'} and not any(row.unresolved for row in rows) + + +def test_a_single_write_inside_a_loop_is_still_its_only_value(): + """One plain store is the only value a read can see, back edge or not.""" + rows = [row for row in scan( + 'def build(rows):\n' + ' for row in rows:\n' + ' chosen = "run"\n' + ' emit({"action": chosen})\n', + ) if row.form == 'dict'] + assert known(rows) == {'run'} and not any(row.unresolved for row in rows) + + +def test_a_negative_index_store_discards_the_container(): + """``table[-1]`` names a slot whose number depends on the length. + + Recording it against the key ``-1`` leaves a read of ``table[0]`` looking at + the untouched initializer, so a one-element list reports the value the write + replaced and calls the site resolved. + """ + rows = [row for row in scan( + 'def build():\n' + ' table = ["run"]\n' + ' table[-1] = "leaked"\n' + ' return {"action": table[0]}\n', + ) if row.form == 'dict'] + assert rows and all(row.unresolved for row in rows) + assert 'run' not in known(rows), 'the initializer was overwritten by the negative store' + + +def test_a_non_negative_index_store_still_carries_its_key(): + """The negative-index rule must not discard the key map it was built on. + + A written key carries the union of its initializer and the write, which is + this scan's documented answer: it reports syntactic possibilities, not the + one value a flow-sensitive reading would pick. What matters here is that the + site stays resolved and the write is visible, both of which the discard path + would have taken away. + """ + rows = [row for row in scan( + 'def build():\n' + ' table = ["run"]\n' + ' table[0] = "wait"\n' + ' return {"action": table[0]}\n', + ) if row.form == 'dict'] + assert known(rows) == {'run', 'wait'} and not any(row.unresolved for row in rows) From 3e1be977e103b0e696327d01a72d1712f78e7e6a Mon Sep 17 00:00:00 2001 From: song <22676124+songoow@users.noreply.github.com> Date: Thu, 17 Sep 2026 22:05:13 -0400 Subject: [PATCH 3/3] refactor(semantics): keep the producer blocker taxonomy, drop the local interpreter B2 of #4447 asks for bounded producer identification and says dynamic, aliased, external and unprovable paths must stay explicitly unresolved. The first cut of this slice went the other way: it grew python_production into a local abstract interpreter -- ordered local rebinding, container-mutation tracking with alias invalidation, ** spread flattening, same-module call resolution -- plus String()/undefined special cases in the TypeScript scanner. It bought one site, 41 unresolved to 40. Review reproduced five confidently wrong "fully resolved" verdicts from it: a loop whose second iteration emits a value the scan never sees; a write through container[-1] missed by a read of container[0]; a dict mutated after construction then spread with **, read back from its stale initializer; a helper rebound through global, still attributed to the module-level def; and a TypeScript parameter shadowing String, still treated as the builtin conversion. For a gate that decides whether code is safe, a confident wrong answer is worse than an admitted unknown, so every one of those inferences is removed and both scanners keep exactly the bounded syntactic reach they had on main. What is kept is the part that was actually worth having: every unresolved site now carries a specific, actionable reason from one taxonomy shared by both runtimes. The TypeScript scanner's single typescript_dynamic catch-all becomes attribute_read / call_result / unstable_local / dynamic_key, with typescript_dynamic left only as the fallback for a write the parser cannot classify; a ??/|| fallback reports the reason of the operand that could not be read. enum_result rows carry their reason too. A label narrows nothing: no value set and no unresolved flag changes, and that is asserted. Unresolved sites go back to 41 with a site list identical to main's. The one site the interpreter closed, driver.py::build_loopx_turn_plan:500, needed container-mutation tracking to read a payload dict through subscript writes it could not order, so it was never proven. No budget, ratchet or anchor moved. The five reproductions stay as tests, now asserting the conservative outcome: each construct stays unresolved with its blocker. Both RFC mirrors are narrowed to the delivered scope, record the rejected attempt, and add evidence row E25. Refs #4447 Co-Authored-By: Claude Opus 5 (1M context) Signed-off-by: song <22676124+songoow@users.noreply.github.com> --- .../semantic-vocabulary-convergence-v0.md | 195 ++++---- ...emantic-vocabulary-convergence-v0.zh-CN.md | 147 +++--- loopx/semantics/python_production.py | 431 ++++-------------- scripts/semantic_production_scan.mjs | 35 +- .../test_semantic_producer_binding.py | 346 +++++--------- .../test_semantic_python_production.py | 7 - 6 files changed, 403 insertions(+), 758 deletions(-) diff --git a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md index 36a5313c0d..335ae83955 100644 --- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md +++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md @@ -409,28 +409,25 @@ dictionaries, call keywords, owner-member results and declared scalar returns are parsed with AST. Imported enum aliases resolve only to the registered owner, including one unrenamed re-export hop through a tracked module (a second hop, a renamed re-export or a rebinding stays unknown); shadowed -names and unbindable calls remain unknown. Conditional -results exclude the condition's literals. Three further local forms are bound, -each only under a stated condition: a call to an undecorated, non-generator, -plainly-defined top-level `def` **of the same module** resolves to the union of -that function's own returns, with arguments never bound to parameters, so a -returned parameter stays unknown and the result is independent of the call site; -a local written more than once resolves to the union of the writes that -textually precede the read, and only when every store of that name is a plain -`name = expression`; and a container mutated only through direct literal-key -subscript writes keeps its untouched keys, with a written key carrying the union -of its initializer and every write. Anything outside those conditions — a -decorator, `async def`, a generator, recursion, an imported or attribute call, a -loop, `with`, `except`, walrus, augmented, unpacking, `global` or `del` -rebinding, an alias, a method call, a computed or deeper store, an escape into a -call, or an unknown `**` spread — leaves the site unknown rather than admitting -a value. TypeScript object writes, assignments -and declared returns use the repository's TypeScript parser rather than regex, -and report the same blocker vocabulary as the Python scanner, so one residue -taxonomy covers both runtimes. +names, reassignments and unresolved calls remain unknown. Conditional +results exclude the condition's literals. TypeScript object writes, assignments +and declared returns use the repository's TypeScript parser rather than regex. Neither parser executes inspected source. These are syntactic result witnesses, not a proof of reachability or whole-program data flow. +Neither scanner interprets the module it reads. There is no local environment, +no loop or call-graph fixpoint, and no model of container mutation: the bound is +the syntax in front of the reader, not the program's behaviour. What the scan +adds instead is a **reason** on every unresolved site, drawn from one taxonomy +shared by both runtimes — `argument_name_only`, `unstable_local`, `call_result`, +`dynamic_key`, `serialized_value`, `annotation_only`, `attribute_read`, `other`, +with `typescript_dynamic` kept only as the TypeScript fallback for a write the +parser cannot classify further. A reason narrows nothing; it tells a reviewer +which residue is a registry edit away and which needs a different analysis. When +the scan cannot enumerate the complete set of possible outputs, the site stays +unresolved with its reason. It is never reported as fully resolved, and never +treated as dead. + `uv run python examples/semantic-vocabulary-drift-smoke.py --report` lists unresolved production locations. Unresolved parts cannot supply missing value evidence; known conditional branches remain structural witnesses, not reachability proofs. @@ -848,7 +845,7 @@ on the next full-tree scan; genuine shared-contract changes still need review. | Historical committed snapshots could become stale across merges | Replay the scanner over the first parent and the merge of the last twenty `upstream/main` merge commits | 8 of 20 merges change at least one carrier | Historical cost motivating Q9; current checks compute the combined tree without a committed snapshot | | The formal model cannot silently lose a proof obligation | Remove an invariant, role, relation, candidate decision, or proof-boundary category from `formal_model` | The drift smoke fails on the exact formal-model shape | The model is a finite contract and proof ledger; it does not prove the listed properties by itself | | An obligation cannot claim a domain nobody counts | `uv run --extra test python -m pytest tests/architecture/test_semantic_vocabulary_drift.py -k domain` | Dropping `domain`, inflating `verified` or `registered`, inventing a selector, claiming an unanchored selector or an out-of-stage evidence bound, and an advisory invariant claiming verified members each fail closed | The sizes are derived from the registry, so the check grounds the declared domain in registry data; it does not prove the obligation over that domain | -| Bounded binding forms cannot be loosened into false evidence | `uv run --extra test python -m pytest tests/architecture/test_semantic_producer_binding.py` | pass; every recognized form has a negative twin — a decorated, `async`, generator, rebound, imported or recursive callee, an unordered store, an aliased or escaped container, and an unknown `**` spread each keep the site unresolved | Fixture repository; a site the scan cannot bind stays unresolved with its recorded reason, never dead | +| An unprovable write cannot be reported as a confident value | `uv run --extra test python -m pytest tests/architecture/test_semantic_producer_binding.py` | pass; the five constructs an earlier local-interpretation attempt reported as fully resolved — a loop-carried write, a negative-index write, a mutated dict re-read through a `**` spread, a helper rebound through `global`, and a TypeScript parameter shadowing `String` — each stay unresolved with their own reason | Fixture repository; a reason names the obstacle without narrowing it, so a site the scan cannot bind stays unresolved, never dead | | F1/F2 quantify over exactly what the producer check walks | Same test module: compare `check_producers`' predicate with the declared F1/F2 domain | The vocabularies with `producers` are exactly the `kernel` tier, 6 of 26; the other 20 are all `cross_runtime` | The scan reach bounds the claim further and is reported, not pinned | Known limits, stated so the check is not over-trusted: @@ -1140,85 +1137,88 @@ introduce a competing target state. ## Appendix A: Execution ledger (non-normative) -### 2026-09-17 — B2: three bounded binding forms, and the residue that stays unresolved - -- **Trigger:** [#4447](https://github.com/huangruiteng/loopx/issues/4447) recorded - the B2 residue as "34 total minus the 15 unprovable by design". Re-measured on - `9003577f9` the total is **41**, and the breakdown is across every scanned - vocabulary rather than `effective_action` alone: `annotation_only=5, - argument_name_only=10, attribute_read=2, call_result=11, other=1, - typescript_dynamic=8, unstable_local=4`. The issue's number was stale; this - entry records the measured split. -- **Delivered:** three bounded local forms in `python_production`, each with - positive and negative fixtures in - `tests/architecture/test_semantic_producer_binding.py`. - 1. **Same-module call results.** A call to an undecorated, non-generator, - plainly-defined top-level `def` of the same module resolves to the union of - that function's own returns. Arguments are never bound to parameters, so a - returned parameter stays unknown and the answer does not depend on the call - site; it is memoised per module scan. A decorator, `async def`, a generator, - a second top-level binding of the name, an imported or attribute call, a - local rebinding and recursion all keep the `call_result` blocker. - 2. **Ordered rebinding of a local.** A local written more than once resolves to - the union of the writes that textually precede the read, and only when every - store of that name is a plain `name = expression`. Loop, `with`, `except`, - walrus, augmented, unpacking, `global` and `del` rebindings are not ordered - by this scan and erase the local. - 3. **Key-precise container writes.** A local container mutated only through - direct literal-key subscript writes keeps its untouched keys, and a written - key carries the union of its initializer and every write. An alias, a method - call, a computed or deeper store, a `del`, or passing the container to any - call still discards the container, as before. A `**` spread of statically - known dict literals is flattened, so an optional spread no longer hides a - sibling key; an unknown spread still makes every key dynamic. - - The TypeScript parser gains the two sound forms the Python scanner already had - (`||` and `??` arms, a transparent `String(x)`, and `undefined` read as no - value) and, more importantly, reports the **same blocker vocabulary**: the - single `typescript_dynamic` catch-all is replaced by `attribute_read`, - `call_result`, `unstable_local` and `dynamic_key`, with `typescript_dynamic` - kept only as the fallback for a form it cannot classify. An owner-member - result (`enum_result`) now carries its reason too; an unlabelled unknown was - invisible in the report breakdown. -- **Result:** unresolved sites **41 → 40**, split +### 2026-09-17 — B2: a bounded blocker taxonomy; the residue stays unresolved + +- **Trigger:** [#4447](https://github.com/huangruiteng/loopx/issues/4447) asks B2 + for *bounded* producer identification, with dynamic, aliased, external and + unprovable paths staying **explicitly unresolved**. The issue's residue figure + ("34 total minus the 15 unprovable by design") was stale. Re-measured on + `d8e7af141` the total is **41**, across every scanned vocabulary rather than + `effective_action` alone, split `annotation_only=5, argument_name_only=10, + attribute_read=2, call_result=11, other=1, typescript_dynamic=8, + unstable_local=4`. +- **Rejected first, recorded because the failure is the lesson.** The first + attempt at this slice grew `python_production` into a local abstract + interpreter: ordered rebinding of a local, container-mutation tracking with + alias invalidation, `**` spread flattening, and same-module call resolution, + plus `String()`/`undefined` special cases in the TypeScript scanner. It closed + **one** site, and review reproduced five confidently wrong "fully resolved" + verdicts: a loop whose second iteration emits a value the scan never sees; a + write through `container[-1]` missed by a read of `container[0]`; a dict + mutated after construction and then spread with `**`, read back from its stale + initializer; a helper rebound through `global` still attributed to the + module-level `def`; and a TypeScript parameter shadowing `String` still treated + as the builtin conversion. For a gate that decides whether code is safe, a + wrong confident answer is strictly worse than an admitted unknown, so all of it + was removed. The five reproductions are kept as tests in + `tests/architecture/test_semantic_producer_binding.py`, now asserting the + conservative outcome: each stays unresolved, with its reason. +- **Delivered: the reason, not the value.** Both scanners keep exactly the + bounded syntactic reach they had, and every unresolved site now carries a + specific, actionable blocker from **one taxonomy shared by both runtimes**. + The TypeScript scanner's single `typescript_dynamic` catch-all is replaced by + `attribute_read`, `call_result`, `unstable_local` and `dynamic_key`, with + `typescript_dynamic` kept only as the fallback for a write the parser cannot + classify further; a `??`/`||` fallback reports the reason of the operand that + could not be read, since the fallback is not itself the obstacle. An + owner-member result (`enum_result`) carries its reason too; an unlabelled + unknown was invisible in the report breakdown. A label narrows nothing: it + changes no value set and no `unresolved` flag, and it is checked as such. +- **Result:** unresolved sites **41 → 41**, and the site list is byte-identical + to the baseline's. The split moves only between labels: `annotation_only=5, argument_name_only=10, attribute_read=7, call_result=14, - other=1, unstable_local=3`. All eight TypeScript sites are reclassified (five - `attribute_read`, three `call_result`); none was resolvable, so that part is a - taxonomy, not a shrink. The one site that closes is - `driver.py::build_loopx_turn_plan:500`, which needed all three forms and the - spread flattening at once. Evidence improves further than the count shows: - unresolved rows carrying at least one known value go **2 → 7**. Registry - values, budgets and the producer site list are unchanged, and no site becomes - newly visible or unregistered. -- **Deliberately not bound, with the reason recorded:** + other=1, unstable_local=4`, and `typescript_dynamic` empties. All eight + TypeScript sites are reclassified; none was + resolvable, so this is a taxonomy, not a shrink. That is the intended outcome — + where the scan cannot prove the complete set of possible outputs, the honest + answer is `unresolved`, never a confident default. Registry values, budgets, + anchors and the producer site list are unchanged, and no site becomes newly + visible or unregistered. +- **Deliberately not narrowed, with the reason recorded:** - `annotation_only` (5) — all five are bare `effective_action: str` field - declarations carrying **no value node at all**. Unprovable by design; - the issue's classification is confirmed. - - `argument_name_only` (10) — confirmed unprovable by design, with one - sharpening: these are unprovable as a *production role*, not unresolvable as - an expression. Four of the ten now carry a fully resolved value set and are - still correctly unresolved, because the callee (`_execution_obligation` and - its peers) reads the field rather than emitting it. The honest way to shrink - this bucket is a registry `call_producers` declaration naming a reviewed - output builder — a data edit a reviewer sees — never a scanner change. - Counting any field-named keyword as production would make the obligation - tautological, which Section 5 forbids. - - `attribute_read` (7), `call_result` (14), `unstable_local` (3) and `other` + declarations carrying **no value node at all**. Unprovable by design; the + issue's classification is confirmed. + - `argument_name_only` (10) — unprovable as a *production role*, which is not + the same as unresolvable as an expression. One of the ten already carries a + fully resolved value set and is still correctly unresolved, because the + callee reads the field rather than emitting it. Counting any field-named + keyword as production would make the obligation tautological, which Section 5 + forbids. The honest way to narrow this bucket is a registry `call_producers` + declaration naming a reviewed output builder — a data edit a reviewer sees — + never a cleverer scanner. + - `attribute_read` (7), `call_result` (14), `unstable_local` (4) and `other` (1) — every remaining site bottoms out in one of four things outside this - scan's bound: a read off a caller-supplied mapping or object - (`decision.get("effective_action")`, `run_decision.effective_action`), a call - into another module, a returned parameter, or a method chain. Binding any of - them needs cross-module or object-field resolution, a separate bounded form - with its own blast radius; it is not attempted here. **A site this scan - cannot bind stays `unresolved` with its recorded reason — it is never - treated as dead.** -- **Cost:** the producer scan runs on every pull request touching `loopx/`. Over - the 319 Python files it reaches and the 5 producer vocabularies, best of three - runs on one tree: **9.20 s → 7.17 s**. The deepened scan is net faster because - it now reuses the memoised parse and the module-function table across - vocabularies instead of re-parsing once per scan. -- **Effect on normative design:** Section 5's bounded producer model names the - three forms and the shared blocker taxonomy; no invariant or milestone changes. + scan's bound: a read off a caller-supplied mapping or object, a call into + another module, a returned parameter, or a method chain. Binding any of them + needs cross-module or object-field resolution — a separate bounded form with + its own blast radius, and, as the rejected attempt showed, one whose + soundness has to be argued before its convenience. It is not attempted here. + **A site this scan cannot bind stays `unresolved` with its recorded reason — + it is never treated as dead.** +- **Cost:** the producer scan runs on every pull request touching `loopx/`. + Best of three on one tree, over the six vocabularies that declare `producers`: + baseline **28.6 s**, this branch **26.4 s**, the rejected interpreter **25.6 s**. + The spread inside a single variant is 26-31 s on the measuring host, so none of + these differences is outside run-to-run noise: the reduction neither costs nor + saves measurable time, because a label is computed on a path that had already + failed to resolve. The interpreter's apparent speedup came from a parse memo it + shipped alongside, not from the inference; reusing `_parsed` in + `scan_python_production` is a sound one-line change on its own and is left to a + separate PR rather than folded into a reduction. +- **Effect on normative design:** Section 5's bounded producer model gains the + shared blocker taxonomy and the statement that neither scanner interprets the + module it reads; no invariant or milestone changes. + ### 2026-09-17 — Formula, role and enforcement claims separated; formal signature mutated Normative for the enforcement-lane wording; the checks are unchanged except for @@ -1467,8 +1467,8 @@ result on the current tree; what changes is what the invariants claim. | 2026-09-16 | Q9: compute the full inventory on demand; retire the committed census | Implementation for [maintainer feedback](https://github.com/huangruiteng/loopx/pull/4360#issuecomment-5692062394); PR review pending | Committed snapshot with post-merge regeneration; diff-only scan rejected | 1, I6, 3, 5, 9, 10, 12 | | 2026-09-16 | B2: bind one unrenamed re-export hop in the Python producer scanner | Implementation, Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B2; PR review pending | Require every consumer to import the owner module (fragile; failed silently in M2); unbounded multi-hop resolution rejected | 5, Appendix A | | 2026-09-16 | B1 rename invariance: add the name-keyed divergence advisory; state the limit it does not close | Implementation, Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B1; PR review pending | Keying the budget on value sets (rejected: `CONFIDENCE_LEVELS` and `EDGE_CASE_COMPLEXITIES` share `high/low/medium` with different meanings); a committed name ledger (rejected at M0: Q9 retired the committed census). The advisory lists surviving forks by name; it was first described as catching a one-sided rename, which measurement disproved, so both mirrors state the limit as it behaves | 9 | -| 2026-09-17 | B2: bind same-module call results, ordered local rebinding and key-precise container writes; reclassify the TypeScript residue rather than shrink it | Implementation, Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B2; PR review pending | Bind cross-module calls and object fields (rejected: a separate bounded form with its own blast radius, not this slice); count a field-named keyword as production (rejected: it makes the obligation tautological, Section 5); leave `typescript_dynamic` as one catch-all (rejected: eight sites shared one reason, so the residue was not actionable); bind the callee's parameters to the call-site arguments (rejected: the answer would depend on the caller and could not be memoised, and a wrong binding would invent evidence) | 5, 9, Appendix A | | 2026-09-17 | B0: state schema validation, implementation stage, evidence status and blocking behaviour separately for I2/I11-I14 and the enforcement lanes; require each formal invariant id exactly once | Implementation, Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B0; PR review pending | Rename the `blocking_next` lane to match its behaviour (rejected: the lane name is the milestone that owns the check, and renaming it would lose that and collapse the two readings the other way); add a `blocks_today` boolean to `formal_model` (rejected: it would be one more declared field a reader could mistake for a measurement, and the fact is a property of the smoke's `main()`, which no registry edit can change); leave the lane gloss and note the gap in the ledger only (rejected: the gloss is the sentence a reviewer quotes) | 2, 5, 11, Appendix A, Appendix B | +| 2026-09-17 | B2: give every unresolved producer site a specific blocker reason from one taxonomy shared by both runtimes; leave the bounded syntactic reach unchanged | Implementation, Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B2; PR review pending | Bind same-module call results, ordered local rebinding, key-precise container writes and `**` spreads (implemented, then **rejected on review**: it closed one site and produced five confidently wrong "fully resolved" verdicts — a loop-carried write, a negative-index write, a spread of a mutated dict, a `global` rebinding, and a shadowed `String`; a wrong confident answer is worse for this gate than an admitted unknown); count a field-named keyword as production (rejected: it makes the obligation tautological, Section 5); leave `typescript_dynamic` as one catch-all (rejected: eight sites shared one reason, so the residue was not actionable); loosen a budget or anchor to bank the one closed site (rejected: the site was never proven) | 5, 9, Appendix A, Appendix C | | 2026-09-17 | Bound F1/F2 to the kernel tier and the scan reach, restate F4 as scope enumeration completeness, and give every obligation a derived `domain` | Implementation, Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447); **kernel-maintainer approval required, not yet given** | Leave the unconditional statements and record the gap in prose only (rejected: the statement was stronger than `validate_production`'s own docstring); restate F4 as per-context value-set disjointness (rejected: refuted by the repo's own data, since `scope_declarations` exists to permit legitimate same-name reuse); widen the scan so the unconditional claim becomes true (rejected: a separate change with its own risk) | 5, 9, Appendix B, Appendix C | ## Appendix C: Evidence registry @@ -1497,6 +1497,7 @@ result on the current tree; what changes is what the invariants claim. | E21 | F1/F2 were unconditional but verified over one tier | `3ca868193` | `check_producers`' skip predicate, and the producer scan roots, read from the tree | 6 of 26 vocabularies declare `producers`, exactly the `tier: kernel` ones; the 20 skipped are all `cross_runtime`; the scan reaches 432 of 1203 tracked `loopx/**/*.{py,ts}` files (35.9%), the uncovered bulk being capabilities 285, other control-plane 192, extensions 83 | Counts from the registry and the tracked tree; the reach denominator moves with any new module, so it is reported, not pinned | | E22 | Fifteen reported unresolved sites can never become evidence | `3ca868193` | smoke report `unresolved_producer_blockers` | 41 unresolved sites, of which `argument_name_only` 10 and `annotation_only` 5 are a field-named keyword argument and a bare declaration; the other 26 are dynamic or interprocedural | Label-keyed; the two labels are code-owned in the scanner, so the floor moves only by a code edit | | E23 | F4 as written could not be violated | `3ca868193` | read `check_scope_declarations` against the F4 statement | Scope is declared and never inferred, so `conflict := collision ∧ scope_overlap` is a definition; what is enforced is that a declaration names every defining module exactly once, over 1 declaration and 4 contexts | Judgement from reading the check; value-set disjointness across contexts is deliberately *not* the property, because `SOURCE_SURFACES` legitimately reuses one name in four contexts (E19) | +| E25 | Local interpretation bought one site and five wrong answers | `d8e7af141` + `a02200591` | replay the producer scan with and without the rejected local interpreter, and run the five reproductions in `tests/architecture/test_semantic_producer_binding.py` against both | The interpreter moved the residue 41 → 40, closing only `driver.py::build_loopx_turn_plan:500`, which needed container-mutation tracking to read a `payload` dict through subscript writes it could not order. On the same build it reported five constructs as **fully resolved** whose true value set it never saw: a loop-carried write (`{"run"}` while iteration two emits `drop`), `codes[-1] = "drop"` read back as `codes[0] == "run"`, a mutated dict re-read through `**` from its stale initializer, a `global`-rebound helper still read off the module `def`, and `String("run")` under a parameter named `String`. Removed, the residue returns to 41 with a byte-identical site list | Fixture constructs plus one real site; they show the inference is unsound, not how often it misfires in this tree. The five now stand as regression tests asserting the unresolved outcome, so the failure mode cannot return unnoticed | | E13 | The conflict budget mostly measured local naming | `1dc6ad8d8` | `MODULE_LOCAL_CONVENTION` applied to `conflicting_values` and `same_runtime_forks` names | 16 of 18 conflicts and 7 of 25 forks are module-local conventions; the semantic subsets are 2 and 18 | Classification is a name pattern, documented in the scanner and pinned by a fixture test | ## Appendix D: Rejected or superseded alternatives 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 bcb00691a2..23ed3eda2c 100644 --- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md +++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md @@ -316,22 +316,20 @@ M0.5 之后新增或删除值时；`cross_module` 只在晋升后（Q8）。持 Python 通过 AST 解析字段赋值（含下标、属性及带注解赋值）、字典、调用关键字、 owner 成员结果及声明函数的标量返回。导入枚举的别名只解析到已登记 owner，含经由一个被跟踪模块的一跳未改名再导出（第二跳、改名再导出或重新绑定保持 unknown）； -被遮蔽的名字与无法绑定的调用仍为 unknown。条件表达式只检查结果分支， -排除条件中的字面量。另有三条局部形式被绑定，且各自只在明确条件下成立：对 -**同模块内**一个未被装饰、非生成器、以普通 `def` 定义的顶层函数的调用，解析为 -该函数自身全部 return 的并集，实参从不绑定到形参，因此返回形参仍为 unknown， -结果与调用点无关；被写入多次的局部变量解析为文本上位于该读取之前的那些写入的 -并集，且仅当该名字的每一次 store 都是普通的 `name = expression` 时成立；只经由 -直接字面量键下标写入被改动的容器保留其未被触碰的键，被写入的键携带其初始化值 -与每一次写入的并集。凡落在上述条件之外的——装饰器、`async def`、生成器、递归、 -导入调用或属性调用，循环、`with`、`except`、海象、增量赋值、解包、`global` 或 -`del` 造成的重绑定，别名、方法调用、计算键或更深层的 store、逃逸进调用，以及 -未知的 `**` 展开——都让该位点保持 unknown，而不是采信一个取值。 -TypeScript 的对象写入、赋值及声明返回使用仓库的 TypeScript -解析器，并报告与 Python 扫描器相同的阻塞原因词汇，因此同一套残量分类覆盖两个 -运行时。两个解析器都不执行被检查源码。这些是句法结果证据，不是可达性或全程序 +被遮蔽的名字、重复赋值及未解析调用仍为 unknown。条件表达式只检查结果分支， +排除条件中的字面量。TypeScript 的对象写入、赋值及声明返回使用仓库的 TypeScript +解析器。两个解析器都不执行被检查源码。这些是句法结果证据，不是可达性或全程序 数据流证明。 +两个扫描器都不解释它们读到的模块：没有局部环境，没有循环或调用图不动点，也没有 +任何容器改动模型；边界就是读者眼前的语法，而不是程序的行为。扫描新增的是给每一个 +未解析位点附上**原因**，取自两个运行时共用的同一套分类——`argument_name_only`、 +`unstable_local`、`call_result`、`dynamic_key`、`serialized_value`、 +`annotation_only`、`attribute_read`、`other`，而 `typescript_dynamic` 只保留为 +TypeScript 侧对解析器无法进一步归类的写入的兜底。原因不缩小任何东西；它告诉评审者 +哪些残量只差一次注册表编辑，哪些需要另一种分析。当扫描无法枚举出可能输出的完整集合 +时，该位点就带着原因保持未解析。它绝不会被报成完全解析，也绝不会被当作 dead。 + `uv run python examples/semantic-vocabulary-drift-smoke.py --report` 列出未解析的生产 位置。unknown 不能补足缺失值的生产证据。生产者守卫对六个 kernel 条目使用不同证据：`effective_action`、`turn_route`、 `loop_disposition` 和 `agent_scope_frontier_action` 使用源码见证； @@ -686,7 +684,7 @@ owner 符号集合的组：`EffectiveAction` 与 `EFFECTIVE_ACTIONS` 是同一 | 历史上的已提交清单会因上游合并而过期 | 对 `upstream/main` 最近二十个合并提交，在第一父提交与合并结果之间重放扫描器 | 20 次合并中 8 次至少改变一个载体 | Q9 的历史动机；当前检查直接计算合并后的全树，不再依赖提交快照 | | 形式模型不能静默丢失证明义务 | 从 `formal_model` 删除不变量、角色、候选决策、关系或证明边界分类 | 漂移 smoke 针对形式模型结构失败 | 该模型是有限契约和证明账本，本身不等于这些性质已经被证明 | | 义务不能声称一个无人清点的值域 | `uv run --extra test python -m pytest tests/architecture/test_semantic_vocabulary_drift.py -k domain` | 删掉 `domain`、调大 `verified` 或 `registered`、自造 selector、使用未钉住的 selector 或跨阶段的证据边界、以及 advisory 不变量声称已验证成员，逐项失败关闭 | 规模从注册表推导，因此该检查把声明值域接地到注册表数据；它不证明该义务在那个值域上成立 | -| 有界绑定形式不能被放宽成假证据 | `uv run --extra test python -m pytest tests/architecture/test_semantic_producer_binding.py` | 通过；每条被识别的形式都有反例孪生——被装饰的、`async`、生成器、被重绑定的、导入的或递归的被调方，无序 store，被别名或逃逸的容器，以及未知 `**` 展开，都让该位点保持未解析 | 夹具仓库；本扫描无法绑定的位点保持未解析并带上被记录的原因，绝不当作 dead | +| 无法证明的写入不能被报成一个自信的取值 | `uv run --extra test python -m pytest tests/architecture/test_semantic_producer_binding.py` | 通过；五个曾被上一版局部解释报成“完全解析”的构造——循环携带的写入、负下标写入、被改动后再 `**` 展开的字典、经 `global` 重绑定的辅助函数，以及遮蔽 `String` 的 TypeScript 形参——逐一保持未解析并带上各自的原因 | 夹具仓库；原因只命名障碍，不缩小它：本扫描无法绑定的位点保持未解析，绝不当作 dead | | F1/F2 恰好量化 producer 检查真正走到的集合 | 同一测试模块：将 `check_producers` 的谓词与 F1/F2 声明的值域对比 | 声明了 `producers` 的词表恰好是 `kernel` 层，26 中的 6；其余 20 个全部是 `cross_runtime` | 扫描范围进一步约束该声明，它被上报而不被钉住 | 已知边界，写明是为了不让这个检查被过度信任： @@ -918,64 +916,64 @@ PR review 保留这些层级。普通改动记录检查范围和理由，无共 ## 附录 A：执行账本（非规范） -### 2026-09-17 — B2：三条有界绑定形式，以及仍然保持未解析的残量 - -- **起因：**[#4447](https://github.com/huangruiteng/loopx/issues/4447) 把 B2 残量 - 记为“34 个减去 15 个设计上不可证的”。在 `9003577f9` 上重新测量，总数是 **41**， - 且分布覆盖全部被扫描词表，而不只是 `effective_action`：`annotation_only=5, - argument_name_only=10, attribute_read=2, call_result=11, other=1, - typescript_dynamic=8, unstable_local=4`。issue 里的数字已经过期；本条记录实测分布。 -- **交付：**在 `python_production` 中新增三条有界局部形式，每条都在 - `tests/architecture/test_semantic_producer_binding.py` 里配有正例与反例。 - 1. **同模块调用结果。**对同模块内一个未被装饰、非生成器、以普通 `def` 定义的 - 顶层函数的调用，解析为该函数自身全部 return 的并集。实参从不绑定到形参， - 因此返回形参仍然未知，且结果与调用点无关，可按模块扫描记忆化。装饰器、 - `async def`、生成器、该名字的第二个顶层绑定、导入调用与属性调用、局部重绑定 - 以及递归，都继续保留 `call_result` 阻塞原因。 - 2. **局部变量的有序重绑定。**被写入多次的局部变量，解析为文本上位于该读取之前 - 的那些写入的并集，且仅当该名字的每一次 store 都是普通的 - `name = expression` 时才成立。循环、`with`、`except`、海象、增量赋值、解包、 - `global` 与 `del` 造成的重绑定不被本扫描定序，会直接抹掉该局部变量。 - 3. **按键精确的容器写入。**只经由直接字面量键下标写入被改动的局部容器，保留其 - 未被触碰的键；被写入的键则携带其初始化值与每一次写入的并集。别名、方法调用、 - 计算键或更深层的 store、`del`，以及把容器作为任何调用的实参传出，仍然像以前 - 一样丢弃整个容器。对静态可知的 dict 字面量的 `**` 展开会被摊平，因此可选展开 - 不再遮蔽同级键；未知展开仍使所有键变为动态。 - - TypeScript 解析器补上了 Python 扫描器早已具备的两条可靠形式（`||` 与 `??` 的 - 分支、透明的 `String(x)`，以及把 `undefined` 读作无值），更重要的是开始报告 - **同一套阻塞原因词汇**：单一的 `typescript_dynamic` 兜底被 - `attribute_read`、`call_result`、`unstable_local` 与 `dynamic_key` 取代， - `typescript_dynamic` 只保留为无法进一步归类时的兜底。owner 成员结果 - （`enum_result`）现在也携带原因；未打标签的未知在报告分布里是不可见的。 -- **结果：**未解析位点 **41 → 40**，分布为 `annotation_only=5, - argument_name_only=10, attribute_read=7, call_result=14, other=1, - unstable_local=3`。八个 TypeScript 位点全部被重新归类（五个 `attribute_read`、 - 三个 `call_result`）；它们没有一个是可解析的，因此这部分是分类学修正，不是缩减。 - 唯一被关闭的位点是 `driver.py::build_loopx_turn_plan:500`，它同时需要三条形式加上 - 展开摊平。证据的改善超过数字所显示的：携带至少一个已知值的未解析行从 **2 → 7**。 - 注册表取值、预算与 producer 位点清单均未变化，也没有任何位点变为新可见或未注册。 -- **有意不绑定，并记录原因：** - - `annotation_only`（5）——五个全部是裸的 `effective_action: str` 字段声明， - **根本没有值节点**。设计上不可证；issue 的归类得到确认。 - - `argument_name_only`（10）——确认设计上不可证，但需要一点锐化：它们不可证的是 - *生产角色*，而不是表达式不可解析。十个里现在有四个已经携带完整解析出的取值集合， - 并且仍然被正确地判为未解析，因为被调方（`_execution_obligation` 及其同类）是在 - 读取该字段而不是产出它。缩减这一类的诚实做法是在注册表 `call_producers` 中声明 - 一个经过评审的输出构造器——一次评审者看得见的数据编辑——而绝不是改扫描器。把任何 - 与字段同名的关键字算作生产，会使该义务变成同义反复，这是第 5 节所禁止的。 - - `attribute_read`（7）、`call_result`（14）、`unstable_local`（3）与 `other` - （1）——剩下的每个位点最终都落在本扫描边界之外的四件事之一：读取调用方提供的 - 映射或对象（`decision.get("effective_action")`、`run_decision.effective_action`）、 - 跨模块调用、返回形参，或方法链。绑定其中任何一种都需要跨模块或对象字段解析， - 那是另一条有自己影响面的有界形式，本切片不做。**本扫描无法绑定的位点，保持 - `unresolved` 并带上它被记录的原因——绝不当作 dead。** -- **成本：**producer 扫描在每个触及 `loopx/` 的 PR 上都会运行。在它覆盖的 319 个 - Python 文件与 5 个 producer 词表上，同一棵树三次取最优：**9.20 s → 7.17 s**。 - 加深后的扫描净变快，因为它现在跨词表复用记忆化的语法树与模块函数表，而不再每次 - 扫描重新解析。 -- **对规范设计的影响：**第 5 节的有界 producer 模型写明这三条形式与共享的阻塞原因 - 分类；不变量与里程碑均无变化。 +### 2026-09-17 — B2：有界的阻塞原因分类；残量继续保持未解析 + +- **起因：**[#4447](https://github.com/huangruiteng/loopx/issues/4447) 要求 B2 做 + *有界的* producer 识别，并明确要求动态、别名、外部与不可证的路径**保持显式未解析**。 + issue 里的残量数字（“34 个减去 15 个设计上不可证的”）已经过期。在 `d8e7af141` + 上重新测量，总数是 **41**，且分布覆盖全部被扫描词表，而不只是 `effective_action`： + `annotation_only=5, argument_name_only=10, attribute_read=2, call_result=11, + other=1, typescript_dynamic=8, unstable_local=4`。 +- **先被否决的做法，记录在案是因为这次失败本身就是结论。**本切片的第一版把 + `python_production` 长成了一个局部抽象解释器：局部变量的有序重绑定、带别名失效的 + 容器改动跟踪、`**` 展开的展平、同模块调用结果解析，外加 TypeScript 扫描器里的 + `String()`/`undefined` 特例。它只闭合了**一个**位点，而评审复现出五个自信但错误的 + “完全解析”判定：第二次迭代才产出、扫描根本看不到的循环写入；被 `container[0]` 读取 + 却遗漏的 `container[-1]` 写入；被改动之后再用 `**` 展开、却从陈旧初始化值读回的字典； + 经 `global` 重绑定却仍被算到模块级 `def` 头上的辅助函数；以及遮蔽了 `String`、却仍被 + 当成内建转换的 TypeScript 形参。对一个要判定代码是否安全的门禁来说，一个自信的错误 + 答案严格劣于一个承认的未知，因此这些推断被整体移除。五个复现作为测试保留在 + `tests/architecture/test_semantic_producer_binding.py`，现在断言的是保守结果： + 每一个都保持未解析，并带上各自的原因。 +- **交付的是原因，不是取值。**两个扫描器的有界句法范围与此前完全一致，而每一个未解析 + 位点现在都带上一个具体、可行动的阻塞原因，取自**两个运行时共用的同一套分类**。 + TypeScript 侧单一的 `typescript_dynamic` 兜底被 `attribute_read`、`call_result`、 + `unstable_local` 与 `dynamic_key` 取代，`typescript_dynamic` 只保留为解析器无法进一步 + 归类时的兜底；`??`/`||` 的兜底表达式上报的是那个读不到的操作数的原因，因为兜底本身 + 并不是障碍。owner 成员结果（`enum_result`）也带上自己的原因；未标注的未知在报告分布里 + 是不可见的。原因不缩小任何东西：它不改变任何值集合，也不改变任何 `unresolved` 标志， + 并且这一点本身被测试钉住。 +- **结果：**未解析位点 **41 → 41**，且位点清单与基线逐字相同。变化只发生在标签之间： + `annotation_only=5, argument_name_only=10, attribute_read=7, call_result=14, + other=1, unstable_local=4`，`typescript_dynamic` 归零。八个 TypeScript 位点全部 + 被重新归类；其中没有一个是可解析的，所以这是一次分类，而不是一次缩减。这正是预期结果——当扫描无法证明可能输出的完整集合 + 时，诚实的答案是 `unresolved`，而不是一个自信的默认值。注册表取值、预算、锚点与 + producer 位点清单均无变化，也没有任何位点变成新可见或未登记。 +- **刻意不去缩小的部分，并记录理由：** + - `annotation_only`（5）——五个全部是裸的 `effective_action: str` 字段声明，**根本没有 + 取值节点**。设计上不可证；issue 的分类得到确认。 + - `argument_name_only`（10）——不可证的是*生产角色*，这与“表达式无法解析”不是一回事。 + 十个里已经有一个带着完全解析的值集合，而它仍然正确地保持未解析，因为被调方是在 + *读*这个字段而不是产出它。把任何与字段同名的关键字都算作生产，会使该义务变成同义 + 反复，这是第 5 节所禁止的。缩小这个桶的诚实办法是在注册表里用 `call_producers` + 声明一个经过评审的输出构建器——一次评审者看得见的数据修改——而不是一个更聪明的扫描器。 + - `attribute_read`（7）、`call_result`（14）、`unstable_local`（4）与 `other`（1） + ——其余每一个位点最终都落到本扫描边界之外的四件事之一：从调用方传入的映射或对象上 + 读取、跨模块调用、返回形参、方法链。绑定其中任何一种都需要跨模块或对象字段解析——那是 + 另一条有自己影响面的有界形式，而且正如被否决的那一版所显示的，它的可靠性必须先于它 + 的便利被论证。本次不做尝试。**本扫描无法绑定的位点带着被记录的原因保持 + `unresolved`——它绝不会被当作 dead。** +- **成本：**producer 扫描会在每一个触及 `loopx/` 的 PR 上运行。 + 同一棵树上、对声明了 `producers` 的六个词表、三次取最好：基线 **28.6 s**， + 本分支 **26.4 s**，被否决的解释器版 **25.6 s**。在测量主机上，单个变体自身的 + 波动区间就是 26-31 s，因此这些差异没有一个超出运行间噪声：这次缩减既不增加也不 + 节省可测量的时间，因为原因标签是在一条本来就没能解析的路径上计算出来的。解释器版 + 看起来更快，来自它一并带入的解析结果记忆化，而不是来自那些推断；在 + `scan_python_production` 里复用 `_parsed` 本身是一处可靠的单行改动，留给另一个 PR， + 不并入这次缩减。 +- **对规范设计的影响：**第 5 节的有界 producer 模型加入共享的阻塞原因分类，以及“两个 + 扫描器都不解释它们读到的模块”这一表述；不变量与里程碑均无变化。 + ### 2026-09-17 — 分离公式、角色与强制性声明；对形式签名做突变 强制层级的表述是规范性变更；除新增一条规则外，检查本身不变。#4447 Track B 的 B0 切片。 @@ -1177,8 +1175,8 @@ PR review 保留这些层级。普通改动记录检查范围和理由，无共 | 2026-09-16 | Q9：全树按需计算；移除已提交结构清单 | 根据[维护者反馈](https://github.com/huangruiteng/loopx/pull/4360#issuecomment-5692062394)实现，PR 评审待完成 | 取代合并后补再生成；拒绝只扫描 diff | 1、I6、3、5、9、10、12 | | 2026-09-16 | B2：Python producer 扫描器绑定一跳未改名再导出 | 实现，Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B2；PR 评审待完成 | 要求每个消费者都从 owner 模块导入（脆弱；M2 中已静默失效）；拒绝无界多跳解析 | 5、附录 A | | 2026-09-16 | B1 改名不变性：新增按名字归组的分歧报告；写明它未闭合的边界 | 实现，Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B1；PR 评审待完成 | 把预算改按值集归组（否决：`CONFIDENCE_LEVELS` 与 `EDGE_CASE_COMPLEXITIES` 共享 `high/low/medium` 而含义不同）；提交名字账本（M0 否决：Q9 已退役提交式清单）。该报告列出仍然存在的分叉；初稿称它能抓住单侧改名，实测证否，故两份镜像按真实行为写明边界 | 9 | -| 2026-09-17 | B2：绑定同模块调用结果、局部变量有序重绑定与按键精确的容器写入；对 TypeScript 残量做重新归类而非缩减 | 实现，Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B2；PR 评审待完成 | 绑定跨模块调用与对象字段（拒绝：那是另一条有自己影响面的有界形式，不属于本切片）；把与字段同名的关键字算作生产（拒绝：会使该义务变成同义反复，见第 5 节）；保留 `typescript_dynamic` 作为单一兜底（拒绝：八个位点共用一个原因，残量无法被行动）；把被调方形参绑定到调用点实参（拒绝：结果会依赖调用方而无法记忆化，且一次错误绑定会凭空造出证据） | 5、9、附录 A | | 2026-09-17 | B0：为 I2/I11-I14 与各强制层级分别陈述 schema 校验、实施阶段、证据状态与阻断行为；要求每个形式不变量 ID 恰好出现一次 | 实现，Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B0；PR 评审待完成 | 把 `blocking_next` 层级改名以匹配其行为（否决：层级名字表示拥有该检查的里程碑，改名会丢掉这层含义，并从另一个方向把两种读法重新合并）；在 `formal_model` 中加一个 `blocks_today` 布尔字段（否决：那只会多出一个可被读者误当作度量的声明字段，而该事实是 smoke `main()` 的性质，任何注册表修改都改不了它）；保留原注解、只在账本里记一笔缺口（否决：评审者引用的正是那句注解） | 2、5、11、附录 A、附录 B | +| 2026-09-17 | B2：给每一个未解析的 producer 位点附上取自两个运行时共用分类的具体阻塞原因；有界句法范围保持不变 | 实现，Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B2；PR 评审待完成 | 绑定同模块调用结果、局部变量有序重绑定、按键精确的容器写入与 `**` 展开（已实现，随后在**评审中被否决**：它只闭合一个位点，却产出五个自信而错误的“完全解析”判定——循环携带的写入、负下标写入、被改动后再展开的字典、`global` 重绑定，以及被遮蔽的 `String`；对这个门禁而言，一个自信的错误答案劣于一个承认的未知）；把与字段同名的关键字算作生产（拒绝：会使该义务变成同义反复，见第 5 节）；保留 `typescript_dynamic` 作为单一兜底（拒绝：八个位点共用一个原因，残量无法被行动）；放宽预算或锚点以把那一个闭合位点收入账（拒绝：该位点从未被证明） | 5、9、附录 A、附录 C | | 2026-09-17 | 将 F1/F2 限定在 kernel 层与扫描范围，把 F4 重述为作用域枚举完备性，并给每条义务加上可推导的 `domain` | 实现，Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447)；**需要内核维护者批准，尚未获得** | 保留无条件表述、只在正文记一笔缺口（否决：该表述比 `validate_production` 自己的 docstring 还强）；把 F4 重述为各上下文值集互斥（否决：会被仓库自身数据推翻，`scope_declarations` 恰恰就是为了允许合理的同名复用）；扒宽扫描让无条件声明成立（否决：那是自带风险的另一个变更） | 5、9、附录 B、附录 C | ## 附录 C：证据登记 @@ -1207,6 +1205,7 @@ PR review 保留这些层级。普通改动记录检查范围和理由，无共 | E21 | F1/F2 写成无条件，但只在一个层上被验证 | `3ca868193` | 从源码树读 `check_producers` 的跳过谓词与 producer 扫描根目录 | 26 个词表中 6 个声明了 `producers`，恰好是 `tier: kernel` 那几个；被跳过的 20 个全部是 `cross_runtime`；扫描触及 1203 个已跟踪 `loopx/**/*.{py,ts}` 中的 432 个（35.9%），未覆盖部分主要是 capabilities 285、其余控制面 192、extensions 83 | 计数来自注册表与已跟踪源码树；分母会随任何新模块移动，所以只上报、不钉住 | | E22 | 15 个被上报的未解析位点永远不可能成为证据 | `3ca868193` | smoke 报告的 `unresolved_producer_blockers` | 41 个未解析位点，其中 `argument_name_only` 10 个、`annotation_only` 5 个分别是以字段名命名的关键字参数和裸声明；其余 26 个是动态或跨过程的 | 按标签归组；这两个标签在扫描器里由代码持有，因此这个下界只能靠改代码移动 | | E23 | F4 写法本身不可能被违反 | `3ca868193` | 对照 F4 表述阅读 `check_scope_declarations` | 作用域是声明的、从不推断，所以 `conflict := collision ∧ scope_overlap` 是一条定义；真正被强制的是一份声明必须恰好枚举每个定义模块，范围是 1 份声明、4 个上下文 | 阅读检查后的判断；各上下文值集互斥故意*不*作为该性质，因为 `SOURCE_SURFACES` 正是合理地在四个上下文复用同一个名字（E19） | +| E25 | 局部解释换来一个位点和五个错误答案 | `d8e7af141` + `a02200591` | 在有/无被否决的局部解释器两种情况下重放 producer 扫描，并对两者运行 `tests/architecture/test_semantic_producer_binding.py` 里的五个复现 | 解释器把残量从 41 推到 40，唯一闭合的是 `driver.py::build_loopx_turn_plan:500`，它需要容器改动跟踪才能读出一个经由它无法定序的下标写入被改动的 `payload` 字典。在同一次构建上，它把五个自己从未看全取值集合的构造报成**完全解析**：循环携带的写入（报 `{"run"}`，而第二次迭代产出 `drop`）、被当作 `codes[0] == "run"` 读回的 `codes[-1] = "drop"`、被改动后再经 `**` 从陈旧初始化值读回的字典、经 `global` 重绑定却仍从模块级 `def` 读出的辅助函数，以及在名为 `String` 的形参下的 `String("run")`。移除之后残量回到 41，位点清单逐字相同 | 夹具构造加一个真实位点；它们证明这条推断不可靠，而不是它在本树上误报多频繁。五个复现现在作为回归测试断言未解析结果，因此该失效模式无法再无声回归 | | E13 | 冲突预算主要在度量局部命名 | `1dc6ad8d8` | 对 `conflicting_values` 与 `same_runtime_forks` 名字应用 `MODULE_LOCAL_CONVENTION` | 18 个冲突中 16 个、25 个分叉中 7 个是模块局部约定；语义子集分别为 2 与 18 | 分类是名字模式，已在扫描器中说明并由夹具测试钉住 | ## 附录 D：被否决或取代的方案 diff --git a/loopx/semantics/python_production.py b/loopx/semantics/python_production.py index 689efd2db5..0b417170f5 100644 --- a/loopx/semantics/python_production.py +++ b/loopx/semantics/python_production.py @@ -9,7 +9,6 @@ import ast from collections import Counter from dataclasses import dataclass -from types import SimpleNamespace from typing import Mapping, TypeVar from .inventory import SourceFile @@ -26,15 +25,21 @@ class Production: """Why the unknown portion stayed unknown; ``None`` when fully resolved. ``argument_name_only`` a field-named keyword argument, which never proves an - output role. ``unstable_local`` a parameter, an unordered rebinding or a - shadowed name. ``call_result`` the value comes back from a call this scan - cannot bind. ``dynamic_key`` a computed or non-literal subscript. - ``serialized_value`` a string where an enum object was required. - ``annotation_only`` a bare annotation that declares the field without a - value. ``attribute_read`` an attribute of an unresolved object. - ``typescript_dynamic`` a TypeScript form the parser cannot classify further; - every other label is shared by both runtimes, so one residue taxonomy - covers them. ``other`` anything else; it keeps the site visible. + output role. ``unstable_local`` a parameter, reassignment or shadowed name. + ``call_result`` the value comes back from a call. ``dynamic_key`` a computed + or non-literal subscript. ``serialized_value`` a string where an enum object + was required. ``annotation_only`` a bare annotation that declares the field + without a value. ``attribute_read`` an attribute of an unresolved object. + ``other`` anything else; it keeps the site visible. + + Every label above is shared by both runtimes, so one residue taxonomy covers + the Python and the TypeScript scanner. ``typescript_dynamic`` is the + TypeScript-only fallback for a write the parser cannot classify further. + + A label is a reason, never a value: naming the obstacle does not narrow it. + When the scan cannot enumerate the complete set of possible outputs the site + stays unresolved with its reason; it is never reported as fully resolved and + never treated as dead. """ @@ -230,73 +235,6 @@ def _qualified_bindings(source: SourceFile, tree: ast.Module, owners: Mapping[st return bindings -def _is_generator(node: ast.FunctionDef) -> bool: - return any(isinstance(child, (ast.Yield, ast.YieldFrom)) for child in ast.walk(node)) - - -# Keyed by tree identity, which is stable because ``_TREES`` retains every tree -# it parses; the table is derived from the module body alone, so it is the same -# for every vocabulary scanned over that file. -_MODULE_FUNCTIONS: dict[int, dict[str, ast.FunctionDef]] = {} - - -def _module_functions(tree: ast.Module) -> dict[str, ast.FunctionDef]: - """Top-level plain ``def``s a same-module call may be bound to. - - A decorator can replace the returned object, ``async def`` hands back a - coroutine rather than the value, and a generator yields instead of - returning, so none of those is a recognized producer. Any second top-level - binding of the name -- a redefinition, class, import, assignment or - ``del`` -- leaves the name unproven and the call keeps ``call_result``. - """ - known = _MODULE_FUNCTIONS.get(id(tree)) - if known is not None: - return known - bound: Counter[str] = Counter() - defined: dict[str, ast.FunctionDef] = {} - for node in tree.body: - if isinstance(node, (ast.FunctionDef, ast.AsyncFunctionDef, ast.ClassDef)): - bound[node.name] += 1 - if isinstance(node, ast.FunctionDef): - defined[node.name] = node - continue - for child in ast.walk(node): - if isinstance(child, ast.Name) and isinstance(child.ctx, (ast.Store, ast.Del)): - bound[child.id] += 1 - elif isinstance(child, (ast.Import, ast.ImportFrom)): - for alias in child.names: - bound[alias.asname or alias.name.split('.')[0]] += 1 - elif isinstance(child, (ast.FunctionDef, ast.AsyncFunctionDef, ast.ClassDef)): - bound[child.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[id(tree)] = functions - return functions - - -def _index_value(node: ast.AST) -> str | int | None: - if isinstance(node, ast.Constant) and type(node.value) in (str, int): - return node.value - if (isinstance(node, ast.UnaryOp) and isinstance(node.op, ast.USub) - and isinstance(node.operand, ast.Constant) and type(node.operand.value) is int): - return -node.operand.value - return None - - -def _union(values: list[ast.AST]) -> ast.AST: - """Fold several definitions of one local into a finite selection node. - - The scan reports syntactic result possibilities, so a name written more than - once carries the union of the writes that precede the read. The synthetic - test is never inspected; only the arms are resolved. - """ - node = values[0] - for other in values[1:]: - test = ast.copy_location(ast.Constant(value=True), other) - node = ast.copy_location(ast.IfExp(test=test, body=node, orelse=other), other) - return node - - def scan_python_production( source: SourceFile, *, @@ -314,36 +252,15 @@ def scan_python_production( ``modules`` additionally lets one unrenamed re-export hop through a tracked module bind the owner. Longer chains and renamed re-exports stay unknown. Local aliases and complete branch selections resolve only at output sites. - Explicit call metadata names only reviewed builder arguments; arbitrary calls - are consumers. Nested function returns belong to that function, not a - registered enclosure. - - Three bounded local forms are recognized beyond a single straight-line - binding. A local written more than once resolves to the union of the writes - that textually precede the read, provided every store of that name is a - plain ``name = expression`` (loop, ``with``, ``except``, walrus, augmented, - unpacking, ``global`` and ``del`` rebindings are not ordered by this scan and - stay unknown). A local container mutated only through direct literal-key - subscript writes keeps its untouched keys, and a written key carries the - union of its initializer and every write; an alias, a method call, a deeper - or computed store, or passing the container to any call still discards it. - A call to an undecorated, non-generator, plainly-defined top-level function - of the same module resolves to the union of that function's own returns. - Arguments are never bound to parameters, so a returned parameter stays - unknown and the result is independent of the call site; recursion, imported - and attribute calls keep the ``call_result`` blocker. + General reassignment and parameter shadowing become unknown. Explicit call + metadata names only reviewed builder arguments; arbitrary calls are consumers. + Nested function returns belong to that function, not a registered enclosure. """ - # The scan never mutates the tree, so one parse per file serves every - # vocabulary; synthetic selection nodes are built fresh, never spliced in. - tree = _parsed(source) + tree = ast.parse(source.text, filename=source.path) bindings = _qualified_bindings(source, tree, enums, modules) call_arguments = call_arguments or {} calls = _qualified_bindings(source, tree, call_arguments, modules) return_paths = return_paths or {} - module_functions = _module_functions(tree) - call_memo: dict[tuple[str, str], tuple[frozenset[str], tuple[str, ...]]] = {} - environments: dict[tuple[int, str], SimpleNamespace] = {} - resolving: set[str] = set() result: list[Production] = [] @@ -355,13 +272,7 @@ def matches(node: ast.AST) -> bool: return (isinstance(node, ast.Subscript) and isinstance(node.slice, ast.Constant) and node.slice.value == field) - def environment(body: list[ast.stmt], scope: str, parameters: set[str], - call_shadows: frozenset[str] = frozenset(), - own: frozenset[str] = frozenset()) -> SimpleNamespace: - """Build one scope's bounded local view and its resolvers, once.""" - cached = environments.get((id(body), scope)) - if cached is not None: - return cached + def scan_scope(body: list[ast.stmt], scope: str, parameters: set[str]) -> None: nodes: list[ast.AST] = [] nested: list[ast.FunctionDef | ast.AsyncFunctionDef | ast.ClassDef] = [] @@ -390,56 +301,50 @@ def collect(node: ast.AST) -> None: exception_targets = {n.name for n in nodes if isinstance(n, ast.ExceptHandler) and n.name} deleted = {n.id for n in nodes if isinstance(n, ast.Name) and isinstance(n.ctx, ast.Del)} shadows = set(assigned) | parameters | nested_names | imported | exception_targets | deleted - # A same-module call binds to a top-level ``def``, so that definition is - # not itself a shadow; only a rebinding inside this scope or an - # enclosing one takes the name away from the module function. - # ``parameters`` also carries every enclosing owner shadow, including the - # module's own top-level definitions, so only this scope's real bindings - # may take a name away from the module function it would otherwise name. - rebinds = set(assigned) | set(own) | imported | exception_targets | deleted - if scope != '': - rebinds |= nested_names - calls_shadowed = frozenset(call_shadows) | rebinds local_bindings = {k: v for k, v in bindings.items() if k not in shadows} local_calls = {k: v for k, v in calls.items() if k not in shadows} - - plain: dict[str, list[ast.AST]] = {} + single_values = {} for node in nodes: - target = value = None - if (isinstance(node, ast.Assign) and len(node.targets) == 1 - and isinstance(node.targets[0], ast.Name)): - target, value = node.targets[0].id, node.value - elif (isinstance(node, ast.AnnAssign) and isinstance(node.target, ast.Name) - and node.value is not None): - target, value = node.target.id, node.value - if target is not None: - plain.setdefault(target, []).append(value) - declared = {name for node in nodes if isinstance(node, (ast.Global, ast.Nonlocal)) - for name in node.names} - # Every store of the name must be one of those plain writes, so a value - # this scan cannot order never masquerades as a finite selection. - definitions = {name: values for name, values in plain.items() - if assigned[name] == len(values) and name not in parameters - and name not in declared and name not in deleted} - - # Resolve only local containers that have not been mutated through an - # unrecognized path or escaped. A direct literal-key subscript write is - # recorded against that key; anything else invalidates every alias, - # rather than turning a stale initializer into false scalar evidence. - written: dict[str, dict[str | int, list[ast.AST]]] = {} - recorded: set[int] = set() + if isinstance(node, ast.Assign) and len(node.targets) == 1 and isinstance(node.targets[0], ast.Name): + target = node.targets[0].id + if assigned[target] == 1 and target not in parameters: + single_values[target] = node.value + elif isinstance(node, ast.AnnAssign) and isinstance(node.target, ast.Name): + target = node.target.id + if assigned[target] == 1 and target not in parameters and node.value is not None: + single_values[target] = node.value + + def conditional_values(node: ast.If) -> dict[str, tuple[ast.AST, int]]: + # A complete if/elif/else defining a local in each arm is one finite + # selection. Partial branches, loops and general reassignments stay + # unknown; no assignment is itself an enum production site. + def arm(statements: list[ast.stmt]) -> dict[str, tuple[ast.AST, int]]: + if len(statements) == 1 and isinstance(statements[0], ast.If): + return conditional_values(statements[0]) + definitions = {} + for statement in statements: + if (isinstance(statement, ast.Assign) and len(statement.targets) == 1 + and isinstance(statement.targets[0], ast.Name)): + name = statement.targets[0].id + definitions[name] = (statement.value, definitions.get(name, (None, 0))[1] + 1) + return {name: item for name, item in definitions.items() if item[1] == 1} + left, right = arm(node.body), arm(node.orelse) + return {name: (ast.copy_location(ast.IfExp(test=node.test, body=left[name][0], + orelse=right[name][0]), node), left[name][1] + right[name][1]) + for name in left.keys() & right.keys()} + for node in nodes: - if isinstance(node, ast.Assign) and len(node.targets) == 1: - store = node.targets[0] - if (isinstance(store, ast.Subscript) and isinstance(store.value, ast.Name) - and not isinstance(store.slice, ast.Slice) - and (key := _index_value(store.slice)) is not None): - recorded.add(id(store)) - written.setdefault(store.value.id, {}).setdefault(key, []).append(node.value) - containers = {name for name, values in definitions.items() - if any(isinstance(value, (ast.List, ast.Dict, ast.Set)) for value in values)} - aliases = [(name, value.id) for name, values in definitions.items() - for value in values if isinstance(value, ast.Name)] + if isinstance(node, ast.If): + for name, (value, count) in conditional_values(node).items(): + if assigned[name] == count and name not in parameters: + single_values[name] = value + + # Resolve only local containers that have not been mutated or escaped. + # A subscript write through an alias invalidates every alias, rather + # than turning a stale initializer into false scalar output evidence. + containers = {name for name, value in single_values.items() + if isinstance(value, (ast.List, ast.Dict, ast.Set))} + aliases = [(name, value.id) for name, value in single_values.items() if isinstance(value, ast.Name)] unsafe: set[str] = set() def root_name(node: ast.AST) -> str | None: @@ -449,8 +354,6 @@ def root_name(node: ast.AST) -> str | None: for node in nodes: if isinstance(node, (ast.Attribute, ast.Subscript)) and isinstance(node.ctx, (ast.Store, ast.Del)): - if id(node) in recorded: - continue if name := root_name(node): unsafe.add(name) elif isinstance(node, ast.Call): @@ -459,9 +362,6 @@ def root_name(node: ast.AST) -> str | None: for argument in [*node.args, *(kw.value for kw in node.keywords)]: if isinstance(argument, ast.Name): unsafe.add(argument.id) - # A second name for the same container would let a write land outside - # this key map, so an aliased container keeps no key-precise evidence. - unsafe.update(name for name in written if name in {n for pair in aliases for n in pair}) for group in (containers, unsafe): changed = True while changed: @@ -471,94 +371,46 @@ def root_name(node: ast.AST) -> str | None: group.update((left, right)) changed = len(group) != before for name in containers & unsafe: - definitions.pop(name, None) - for name in unsafe: - written.pop(name, None) - - blockers: list[str] = [] - - def blocked(label: str) -> bool: - blockers.append(label) - return True + single_values.pop(name, None) def bound(node: ast.AST | None, seen: frozenset[str]) -> tuple[ast.AST | None, frozenset[str]]: - while isinstance(node, ast.Name) and node.id in definitions and node.id not in seen: - values = [value for value in definitions[node.id] - if (value.lineno, value.col_offset) < (node.lineno, node.col_offset)] - if not values: + while isinstance(node, ast.Name) and node.id in single_values and node.id not in seen: + definition = single_values[node.id] + if (definition.lineno, definition.col_offset) >= (node.lineno, node.col_offset): break seen = seen | {node.id} - node = values[0] if len(values) == 1 else _union(values) + node = definition return node, seen - def flatten(container: ast.Dict, seen: frozenset[str], - depth: int = 0) -> tuple[list[tuple[str | int, ast.AST]], bool] | None: - """Expand ``**`` spreads of statically known dict literals, in write order. - - A spread whose operand is not a finite selection of dict literals - with literal keys could overwrite any key, so the whole lookup falls - back to the unknown-key answer instead of trusting a literal entry. - """ - if depth > 4: - return None - pairs: list[tuple[str | int, ast.AST]] = [] - spread = False - for key, value in zip(container.keys, container.values, strict=True): - if key is not None: - index = _index_value(key) - if index is None: - return None - pairs.append((index, value)) - continue - spread = True - arms = [value] - while arms: - arm, visited = bound(arms.pop(), seen) - if isinstance(arm, ast.IfExp): - arms.extend((arm.body, arm.orelse)) - continue - if not isinstance(arm, ast.Dict): - return None - inner = flatten(arm, visited, depth + 1) - if inner is None: - return None - pairs.extend(inner[0]) - return pairs, spread - - def lookup(container: ast.AST | None, key: str | int | None, - seen: frozenset[str] = frozenset(), absent_ok: bool = False) -> tuple[list[ast.AST], bool]: - # ``absent_ok`` says a recorded write already supplies this key, so an - # initializer that does not carry it is not an unknown boundary. + def index_value(node: ast.AST) -> str | int | None: + if isinstance(node, ast.Constant) and type(node.value) in (str, int): + return node.value + if (isinstance(node, ast.UnaryOp) and isinstance(node.op, ast.USub) + and isinstance(node.operand, ast.Constant) and type(node.operand.value) is int): + return -node.operand.value + return None + + def lookup(container: ast.AST | None, key: str | int | None) -> tuple[list[ast.AST], bool]: if isinstance(container, (ast.Tuple, ast.List)): if type(key) is int: - if -len(container.elts) <= key < len(container.elts): - return [container.elts[key]], False - return [], (False if absent_ok else blocked('dynamic_key')) + return ([container.elts[key]], False) if -len(container.elts) <= key < len(container.elts) else ([], blocked('dynamic_key')) if key is not None: return [], blocked('dynamic_key') return list(container.elts), blocked('dynamic_key') if isinstance(container, ast.Dict): - expanded = flatten(container, seen) - if expanded is None: - return list(container.values), blocked('dynamic_key') - pairs, spread = expanded - if key is None: - return [value for _, value in pairs], blocked('dynamic_key') - found = [value for index, value in pairs if index == key] - if not found: - return [], (False if absent_ok else blocked('dynamic_key')) - # Python dict construction keeps the last duplicate key; an - # optional spread makes each contributor a live possibility. - return (found if spread else [found[-1]]), False + keys = [index_value(k) if k is not None else None for k in container.keys] + if key is not None and all(k is not None for k in keys): + # Python dict construction keeps the last duplicate key. + found = [v for k, v in zip(keys, container.values, strict=True) if k == key] + return ([found[-1]], False) if found else ([], blocked('dynamic_key')) + return list(container.values), blocked('dynamic_key') return [], blocked('unstable_local' if isinstance(container, ast.Name) else 'other') - def element(root: str | None, container: ast.AST | None, key: str | int | None, - seen: frozenset[str] = frozenset()) -> tuple[list[ast.AST], bool]: - updates = written.get(root or '') - extra = [] if not updates else (updates.get(key, []) if key is not None - else [v for values in updates.values() for v in values]) - choices, unknown = lookup(container, key, seen, absent_ok=bool(extra)) - return [*choices, *extra], unknown + blockers: list[str] = [] + + def blocked(label: str) -> bool: + blockers.append(label) + return True def resolve(node: ast.AST | None, seen: frozenset[str] = frozenset(), *, enum_only: bool = False) -> tuple[set[str], bool]: node, seen = bound(node, seen) @@ -570,9 +422,8 @@ def resolve(node: ast.AST | None, seen: frozenset[str] = frozenset(), *, enum_on if isinstance(node.slice, ast.Slice) or (isinstance(node.slice, ast.Constant) and type(node.slice.value) not in (str, int)): return set(), blocked('dynamic_key') - root = node.value.id if isinstance(node.value, ast.Name) else None container, visited = bound(node.value, seen) - choices, unknown = element(root, container, _index_value(node.slice), visited) + choices, unknown = lookup(container, index_value(node.slice)) known: set[str] = set() for value in choices: part, unresolved = resolve(value, visited, enum_only=enum_only) @@ -599,25 +450,13 @@ def resolve(node: ast.AST | None, seen: frozenset[str] = frozenset(), *, enum_on return enum_object_value(node.value, seen) return set(), blocked('attribute_read') if isinstance(node, ast.Call): - hit = same_module_call(node, 'enum' if enum_only else 'value') - return hit if hit is not None else (set(), blocked('call_result')) + return set(), blocked('call_result') if isinstance(node, ast.Name): return set(), blocked('unstable_local') if node is None: return set(), blocked('other') return set(), blocked('other') - def same_module_call(node: ast.Call, mode: str) -> tuple[set[str], bool] | None: - if not isinstance(node.func, ast.Name) or node.func.id in calls_shadowed: - return None - hit = call_values(node.func.id, mode) - if hit is None: - return None - values, reasons = hit - for reason in reasons: - blocked(reason) - return set(values), bool(reasons) - def enum_object_value(node: ast.AST, seen: frozenset[str]) -> tuple[set[str], bool]: node, seen = bound(node, seen) if isinstance(node, ast.IfExp): @@ -625,13 +464,6 @@ def enum_object_value(node: ast.AST, seen: frozenset[str]) -> tuple[set[str], bo return set().union(*(v for v, _ in parts)), any(u for _, u in parts) if isinstance(node, ast.Attribute) and isinstance(node.value, ast.Name) and node.value.id in local_bindings: return resolve(node, seen, enum_only=True) - if isinstance(node, ast.Call): - # Only a same-module function that returns owner members as enum - # objects has another ``.value``; a function handing back - # ``Action.RUN.value`` already returns the serialized string. - hit = same_module_call(node, 'object') - if hit is not None and hit[0]: - return hit # A serialized string (including Action.RUN.value) is not an enum # object with another .value attribute. return set(), blocked('serialized_value') @@ -639,76 +471,15 @@ def enum_object_value(node: ast.AST, seen: frozenset[str]) -> tuple[set[str], bo def returned(node: ast.AST | None, path: tuple[str | int, ...], seen: frozenset[str] = frozenset()) -> tuple[set[str], bool]: if not path: return resolve(node, seen) - root = node.id if isinstance(node, ast.Name) else None node, seen = bound(node, seen) - choices, unknown = element(root, node, path[0], seen) + choices, unknown = lookup(node, path[0]) parts = [returned(value, path[1:], seen) for value in choices] return set().union(*(v for v, _ in parts)), unknown or any(u for _, u in parts) - built = SimpleNamespace(nodes=nodes, nested=nested, shadows=shadows, blockers=blockers, - calls_shadowed=calls_shadowed, local_calls=local_calls, - resolve=resolve, returned=returned, enum_object=enum_object_value) - environments[(id(body), scope)] = built - return built - - def call_values(name: str, mode: str) -> tuple[frozenset[str], tuple[str, ...]] | None: - """Union of one same-module function's own returns, or ``None``. - - ``mode`` asks what the caller needs of each return: its written value, - only owner members (``enum``), or the member behind an enum object - (``object``). The last is not the same question as the first: a function - returning ``Action.RUN.value`` hands back a string that has no further - ``.value``, so it answers ``object`` with nothing. - - Call arguments are never bound to parameters, so a returned parameter - stays unknown and the answer does not depend on the call site; it is - memoised per module scan. A call reached from inside its own callee - chain keeps the ``call_result`` blocker instead of unrolling recursion. - A bare ``return`` or a fall-through yields ``None``, which is not a - vocabulary value: it contributes nothing and blocks nothing. - """ - target = module_functions.get(name) - if target is None or name in resolving: - return None - key = (name, mode) - if key not in call_memo: - resolving.add(name) - try: - args = target.args - params = {a.arg for a in (*args.posonlyargs, *args.args, *args.kwonlyargs)} - params.update(a.arg for a in (args.vararg, args.kwarg) if a) - env = environment(target.body, name, params | module_env.shadows, - module_env.calls_shadowed, frozenset(params)) - values: set[str] = set() - unknown = False - start = len(env.blockers) - for node in env.nodes: - if isinstance(node, ast.Return) and node.value is not None: - part, missing = (env.enum_object(node.value, frozenset()) if mode == 'object' - else env.resolve(node.value, enum_only=mode == 'enum')) - values |= part - unknown |= missing - first = env.blockers[start] if len(env.blockers) > start else 'call_result' - del env.blockers[start:] - call_memo[key] = (frozenset(values), (first,) if unknown else ()) - finally: - resolving.discard(name) - return call_memo[key] - - def scan_scope(body: list[ast.stmt], scope: str, parameters: set[str], - call_shadows: frozenset[str] = frozenset(), own: frozenset[str] = frozenset(), - env: SimpleNamespace | None = None) -> None: - env = env if env is not None else environment(body, scope, parameters, call_shadows, own) - blockers = env.blockers - def record(node: ast.AST | None, form: str, location: ast.AST) -> None: - # Reasons are read back by position: one scope's environment is - # shared with same-module call resolution, which may nest inside. - start = len(blockers) - values, unknown = (env.returned(node, return_paths.get(scope, ())) - if form == 'return' else env.resolve(node)) - blocker = blockers[start] if len(blockers) > start else None - del blockers[start:] + blockers.clear() + values, unknown = (returned(node, return_paths.get(scope, ())) if form == 'return' else resolve(node)) + blocker = blockers[0] if blockers else None if node is None and form == 'assignment': # A bare annotation declares the field; there is no value to resolve. blocker = 'annotation_only' @@ -718,7 +489,7 @@ def record(node: ast.AST | None, form: str, location: ast.AST) -> None: result.append(Production(f'{source.path}::{scope}', location.lineno, form, frozenset(values), unknown, blocker if unknown else None)) - for node in env.nodes: + for node in nodes: if isinstance(node, ast.Assign): if field and any(matches(t) for t in node.targets): record(node.value, 'assignment', node) @@ -729,7 +500,7 @@ def record(node: ast.AST | None, form: str, location: ast.AST) -> None: if isinstance(key, ast.Constant) and key.value == field: record(value, 'dict', node) elif isinstance(node, ast.Call): - output_arguments = env.local_calls.get(node.func.id, {}) if isinstance(node.func, ast.Name) else {} + output_arguments = local_calls.get(node.func.id, {}) if isinstance(node.func, ast.Name) else {} for kw in node.keywords: if kw.arg in output_arguments: record(kw.value, 'call_argument', node) @@ -742,16 +513,15 @@ def record(node: ast.AST | None, form: str, location: ast.AST) -> None: if scope in return_functions: record(node.value, 'return', node) else: - start = len(blockers) - values, unknown = env.resolve(node.value, enum_only=True) + blockers.clear() + values, unknown = resolve(node.value, enum_only=True) # An owner-member result keeps its reason too; an unlabelled # unknown would be invisible in the report breakdown. - reason = blockers[start] if len(blockers) > start else None - del blockers[start:] + reason = blockers[0] if blockers else None if values: result.append(Production(f'{source.path}::{scope}', node.lineno, 'enum_result', frozenset(values), unknown, reason if unknown else None)) - for child in env.nested: + for child in nested: name = child.name if scope == '' else f'{scope}.{child.name}' params: set[str] = set() if not isinstance(child, ast.ClassDef): @@ -759,8 +529,7 @@ def record(node: ast.AST | None, form: str, location: ast.AST) -> None: params = {a.arg for a in (*args.posonlyargs, *args.args, *args.kwonlyargs)} params.update(a.arg for a in (args.vararg, args.kwarg) if a) # A nested closure might shadow an owner in any enclosing scope. - scan_scope(child.body, name, params | env.shadows, env.calls_shadowed, frozenset(params)) + scan_scope(child.body, name, params | shadows) - module_env = environment(tree.body, '', set()) - scan_scope(tree.body, '', set(), frozenset(), frozenset(), module_env) + scan_scope(tree.body, '', set()) return sorted(set(result), key=lambda row: (row.site, row.line, row.form, sorted(row.values))) diff --git a/scripts/semantic_production_scan.mjs b/scripts/semantic_production_scan.mjs index 95d437414f..4ff9ec38cd 100644 --- a/scripts/semantic_production_scan.mjs +++ b/scripts/semantic_production_scan.mjs @@ -16,14 +16,22 @@ for (const source of request.sources) { const field = request.field; const returns = new Set((request.return_functions ?? []).filter(x => x.startsWith(`${source.path}::`))); const unwrap = node => { - while (node && (ts.isParenthesizedExpression(node) || ts.isAsExpression(node) || - ts.isSatisfiesExpression(node) || ts.isNonNullExpression(node))) node = node.expression; + while (node && (ts.isParenthesizedExpression(node) || ts.isAsExpression(node) || ts.isSatisfiesExpression(node))) node = node.expression; return node; }; - // Say why a write stayed unknown using the same labels as the Python scanner, + // Name why a write stayed unknown using the same labels as the Python scanner, // so one residue taxonomy covers both runtimes instead of a single catch-all. + // This only labels the residue; it never narrows it. Nothing here resolves a + // value, so a site the parser cannot enumerate stays unresolved as before. const blockerFor = node => { if (!node) return 'other'; + // A ``??``/``||`` fallback is not itself the obstacle; the operand that + // could not be read is. Reporting that reason renames the residue only -- + // the site stays unresolved with no value either way. + if (ts.isBinaryExpression(node) && [ts.SyntaxKind.BarBarToken, + ts.SyntaxKind.QuestionQuestionToken].includes(node.operatorToken.kind)) { + return blockerFor(unwrap(node.left)); + } if (ts.isPropertyAccessExpression(node) || ts.isElementAccessExpression(node)) return 'attribute_read'; if (ts.isCallExpression(node) || ts.isNewExpression(node) || ts.isAwaitExpression(node)) return 'call_result'; if (ts.isIdentifier(node)) return 'unstable_local'; @@ -31,28 +39,17 @@ for (const source of request.sources) { ts.isTemplateExpression(node)) return 'dynamic_key'; return 'typescript_dynamic'; }; - const merge = parts => ({ - values: [...new Set(parts.flatMap(part => part.values))].sort(), - unresolved: parts.some(part => part.unresolved), - blocker: parts.find(part => part.unresolved)?.blocker, - }); const values = expression => { const node = unwrap(expression); if (!node) return {values: [], unresolved: true, blocker: 'other'}; if (ts.isStringLiteral(node) || ts.isNoSubstitutionTemplateLiteral(node)) return {values: node.text ? [node.text] : [], unresolved: false}; 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.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. - if (ts.isBinaryExpression(node) && [ts.SyntaxKind.BarBarToken, - ts.SyntaxKind.QuestionQuestionToken].includes(node.operatorToken.kind)) { - return merge([values(node.left), values(node.right)]); + if (ts.isConditionalExpression(node)) { + const left = values(node.whenTrue), right = values(node.whenFalse); + return {values: [...new Set([...left.values, ...right.values])].sort(), + unresolved: left.unresolved || right.unresolved, + blocker: (left.unresolved ? left : right).blocker}; } - if (ts.isCallExpression(node) && ts.isIdentifier(node.expression) && - node.expression.text === 'String' && node.arguments.length === 1) return values(node.arguments[0]); return {values: [], unresolved: true, blocker: blockerFor(node)}; }; const staticName = expression => { diff --git a/tests/architecture/test_semantic_producer_binding.py b/tests/architecture/test_semantic_producer_binding.py index 4aa2f8fcde..e75a7ad0c6 100644 --- a/tests/architecture/test_semantic_producer_binding.py +++ b/tests/architecture/test_semantic_producer_binding.py @@ -1,22 +1,32 @@ -"""Counterexamples for the bounded binding forms the producer scan recognizes. - -Each form here narrows an ``unresolved`` blocker, so every one needs a negative -twin: a site the scan must keep unresolved rather than call dead. Shrinking the -residue by loosening the rule is the failure this file is meant to catch. +"""The producer scan's residue stays unresolved; it never becomes a guess. + +Track B item B2 of #4447 asks for *bounded* producer identification: dynamic, +aliased, external and unprovable paths must stay explicitly unresolved. A +confident wrong answer is the worst failure this gate can produce, because a +reviewer reads "fully resolved" as "these are all the values this site can +emit". Every construct below was reported as fully resolved by a local +abstract-interpretation attempt that this slice removed; each must now come +back unresolved, carrying the blocker label that says why. + +The blocker labels themselves are what B2 keeps: a reason a reviewer can act on +in place of one opaque bucket. A label narrows nothing -- it only names the +obstacle -- so these tests assert the reason *and* that the site stayed unknown. """ from __future__ import annotations -import ast -import time +from pathlib import Path import pytest from loopx.semantics.inventory import SourceFile +from loopx.semantics.production import collect_production from loopx.semantics.python_production import scan_python_production +ROOT = Path(__file__).resolve().parents[2] OWNER = 'loopx/quota/owner.py::Action' ENUMS = {OWNER: {'RUN': 'run', 'WAIT': 'wait'}} CONSUMER = 'loopx/quota/client.py' +TS_CONSUMER = 'loopx/control_plane/quota/probe.ts' def scan(text, *, returns=(), paths=None, calls=None, field='action', enums=ENUMS): @@ -33,268 +43,144 @@ def blockers(rows): return {row.blocker for row in rows if row.unresolved} -def at(rows, scope): - """Only the consumer's own rows; a helper's own returns are its evidence.""" - return [row for row in rows if row.site == f'{CONSUMER}::{scope}'] - - -# --- same-module call results ------------------------------------------------- - +def only(rows, form): + return [row for row in rows if row.form == form] -def test_same_module_call_resolves_to_the_callee_own_returns(): - rows = scan('def pick(flag):\n return "run" if flag else "wait"\n' - 'def emit():\n return {"action": pick(True)}\n') - assert known(rows) == {'run', 'wait'} - assert not any(row.unresolved for row in rows) +def ts_vocabulary(): + return {'values': ['run', 'wait'], 'producers': ['loopx/control_plane/quota/probe.py::emit'], + 'owners': {'python': None}, 'literal_scan': {'field': 'action'}} -def test_same_module_call_keeps_the_callee_unknown_portion(): - """A bound call reports the callee's own reason, not a blanket call_result.""" - rows = scan('def pick(flag):\n return "run" if flag else dynamic()\n' - 'def emit():\n return {"action": pick(True)}\n') - assert known(rows) == {'run'} - assert blockers(rows) == {'call_result'} +def ts_scan(text): + return collect_production(ROOT, ts_vocabulary(), [SourceFile(TS_CONSUMER, '.ts', text)]) -def test_call_arguments_are_never_bound_to_callee_parameters(): - """A returned parameter stays unknown however literal the argument is.""" - rows = scan('def pick(choice):\n return choice\n' - 'def emit():\n return {"action": pick("run")}\n') - assert known(rows) == set() - assert blockers(rows) == {'unstable_local'} +# --- five reproductions of confidently wrong answers -------------------------- +# +# Each case below has a value the scan cannot see. Reporting the values it *can* +# see as the complete set would be the false verdict; the honest answer is that +# the complete set is unknown. -def test_enum_object_returned_by_a_same_module_call_supplies_value(): - rows = scan('from .owner import Action\ndef pick():\n return Action.RUN\n' - 'def emit():\n choice = pick()\n return {"action": choice.value}\n') - assert known(rows) == {'run'} - assert not any(row.unresolved for row in rows) +def test_a_loop_carried_write_is_not_the_first_iteration_alone(): + """The second iteration emits ``drop``; only the first write precedes the read. -def test_serialized_result_is_not_an_enum_object_with_a_value_attribute(): - rows = at(scan('from .owner import Action\ndef pick():\n return Action.RUN.value\n' - 'def emit():\n choice = pick()\n return {"action": choice.value}\n'), 'emit') - assert known(rows) == set() - assert blockers(rows) == {'serialized_value'} - - -@pytest.mark.parametrize('definition, reason', [ - # A decorator can replace the returned object entirely. - ('@wrap\ndef pick():\n return "run"\n', 'call_result'), - # await of a coroutine is a different expression; a bare call is not the value. - ('async def pick():\n return "run"\n', 'call_result'), - # A generator yields; the call returns the iterator, not a member. - ('def pick():\n yield "run"\n', 'call_result'), - # A second top-level binding takes the name away from the definition. - ('def pick():\n return "run"\npick = other\n', 'call_result'), - ('def pick():\n return "run"\nfrom .elsewhere import pick\n', 'call_result'), -]) -def test_unbindable_definitions_keep_the_site_unresolved(definition, reason): - rows = scan(definition + 'def emit():\n return {"action": pick()}\n') + Ordering a local's writes by source position is sound only in straight-line + code. 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. + """ + rows = only(scan('def emit(rows):\n choice = "run"\n for row in rows:\n' + ' packet = {"action": choice}\n choice = "drop"\n return packet\n'), 'dict') + assert rows and all(row.unresolved for row in rows) + assert blockers(rows) == {'unstable_local'} assert known(rows) == set() - assert blockers(rows) == {reason} -def test_imported_and_attribute_calls_are_not_same_module_definitions(): - rows = scan('from .elsewhere import pick\nimport helper\n' - 'def emit():\n return {"action": pick(), "other": helper.pick()}\n') - assert known(rows) == set() - assert blockers(rows) == {'call_result'} +def test_a_negative_index_write_is_not_a_write_to_a_different_key(): + """``codes[-1]`` and ``codes[0]`` are the same element of a one-item list.""" + rows = only(scan('def emit():\n codes = ["run"]\n codes[-1] = "drop"\n' + ' return {"action": codes[0]}\n'), 'dict') + assert rows and all(row.unresolved for row in rows) + assert blockers(rows) == {'unstable_local'} + assert 'run' not in known(rows) -def test_locally_rebound_name_does_not_borrow_the_module_definition(): - rows = scan('def pick():\n return "run"\n' - 'def emit(pick):\n return {"action": pick()}\n') +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() - assert blockers(rows) == {'call_result'} -def test_recursive_call_chain_terminates_and_stays_unresolved(): - rows = scan('def left():\n return right()\ndef right():\n return left()\n' - 'def emit():\n return {"action": left()}\n') - 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'} - - -def test_a_callee_that_only_raises_produces_no_value_and_no_blocker(): - rows = scan('def pick():\n raise ValueError("no route")\n' - 'def emit():\n return {"action": pick()}\n') assert known(rows) == set() - assert not any(row.unresolved for row in rows) - -# --- ordered rebinding of a local -------------------------------------------- - -def test_rebound_local_unions_the_writes_that_precede_the_read(): - rows = scan('from .owner import Action\ndef emit(flag):\n choice = Action.RUN.value\n' - ' if flag:\n choice = Action.WAIT.value\n return {"action": choice}\n') - assert known(rows) == {'run', 'wait'} - assert not any(row.unresolved for row in rows) - - -def test_a_write_after_the_read_is_not_a_definition_for_that_read(): - rows = scan('from .owner import Action\ndef emit(flag):\n choice = Action.RUN.value\n' - ' packet = {"action": choice}\n choice = Action.WAIT.value\n return packet\n') - assert known(rows) == {'run'} - assert not any(row.unresolved for row in rows) - - -def test_a_rebound_local_keeps_its_unknown_arm_visible(): - rows = scan('from .owner import Action\ndef emit(flag):\n choice = Action.RUN.value\n' - ' if flag:\n choice = dynamic()\n return {"action": choice}\n') - assert known(rows) == {'run'} +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('rebind', [ - 'for choice in options: pass', - 'with opened() as choice: pass', - 'choice += suffix', - 'choice, extra = pair()', - 'del choice', - 'print(choice := dynamic())', -]) -def test_stores_this_scan_cannot_order_leave_the_local_unknown(rebind): - """Only a plain ``name = expression`` is an ordered write; nothing else is.""" - rows = scan('from .owner import Action\ndef emit():\n choice = Action.RUN.value\n ' - + rebind + '\n return {"action": choice}\n') - assert known(rows) == set() - assert blockers(rows) == {'unstable_local'} - - -def test_a_global_declaration_takes_the_name_out_of_this_scope(): - rows = scan('from .owner import Action\ndef emit():\n global choice\n' - ' choice = Action.RUN.value\n return {"action": choice}\n') - assert known(rows) == set() - assert blockers(rows) == {'unstable_local'} - - -# --- key-precise container writes -------------------------------------------- - - -def test_untouched_keys_survive_a_literal_key_write(): - rows = scan('from .owner import Action\ndef emit(flag):\n' - ' packet = {"action": Action.RUN.value, "note": ""}\n' - ' if flag:\n packet["note"] = "changed"\n return packet\n', - returns=['emit'], paths={'emit': ('action',)}) - assert known(rows) == {'run'} - assert not any(row.unresolved for row in rows) - - -def test_a_written_key_carries_every_contributing_write(): - rows = scan('from .owner import Action\ndef emit(flag):\n' - ' packet = {"action": Action.RUN.value}\n' - ' if flag:\n packet["action"] = Action.WAIT.value\n return packet\n', - returns=['emit'], paths={'emit': ('action',)}) - assert known(rows) == {'run', 'wait'} - assert not any(row.unresolved for row in rows) - - -def test_a_key_supplied_only_by_a_write_is_not_an_unknown_boundary(): - rows = scan('from .owner import Action\ndef emit():\n packet = {}\n' - ' packet["action"] = Action.RUN.value\n return packet\n', - returns=['emit'], paths={'emit': ('action',)}) - assert known(rows) == {'run'} - assert not any(row.unresolved for row in rows) - - -def test_an_unresolved_write_to_the_read_key_stays_unresolved(): - rows = scan('from .owner import Action\ndef emit(flag):\n' - ' packet = {"action": Action.RUN.value}\n' - ' if flag:\n packet["action"] = dynamic()\n return packet\n', - returns=['emit'], paths={'emit': ('action',)}) - assert known(rows) == {'run'} - assert blockers(rows) == {'call_result'} +# --- the residue is labelled, and a label is not a narrowing ------------------- -@pytest.mark.parametrize('mutation', [ - # A second name could carry a write this key map never sees. - 'alias = packet\n alias["action"] = dynamic()', - # A computed key could land on any key at all. - 'packet[key()] = dynamic()', - # A deeper store is not a write to a key of this container. - 'packet["action"]["kind"] = dynamic()', - # A method or an escape can rewrite the whole container. - 'packet.update(other)', - 'consume(packet)', - 'del packet["action"]', +@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_writes_outside_the_recognized_form_discard_the_container(mutation): - rows = [row for row in scan('from .owner import Action\ndef emit():\n' - ' packet = {"action": Action.RUN.value}\n ' + mutation + '\n return packet\n', - returns=['emit'], paths={'emit': ('action',)}) if row.form == 'return'] - assert known(rows) == set() - assert rows and all(row.unresolved for row in rows) +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} -# --- dict literal spreads ----------------------------------------------------- +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_a_spread_of_known_literals_does_not_hide_a_sibling_key(): - rows = scan('from .owner import Action\ndef emit(flag):\n' - ' packet = {"action": Action.RUN.value, **({"note": "x"} if flag else {})}\n' - ' return packet\n', returns=['emit'], paths={'emit': ('action',)}) - assert known(rows) == {'run'} - assert not any(row.unresolved for row in rows) +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_spread_that_may_carry_the_key_keeps_both_possibilities(): - rows = scan('from .owner import Action\ndef emit(flag):\n' - ' packet = {"action": Action.RUN.value, **({"action": Action.WAIT.value} if flag else {})}\n' - ' return packet\n', returns=['emit'], paths={'emit': ('action',)}) - assert known(rows) == {'run', 'wait'} - assert not any(row.unresolved for row in rows) +def test_an_unbound_site_is_unresolved_and_never_silently_dropped(): + """No recognized producer means unresolved; it never means dead.""" + rows = scan('def emit(payload):\n return {"action": payload.get("action")}\n') + assert len(rows) == 1 + assert rows[0].unresolved and rows[0].blocker == 'call_result' + assert rows[0].values == frozenset() -@pytest.mark.parametrize('spread', ['**overrides', '**dict(overrides)', '**{key(): "x"}']) -def test_an_unknown_spread_could_overwrite_any_key(spread): - rows = scan('from .owner import Action\ndef emit(overrides):\n' - ' packet = {"action": Action.RUN.value, ' + spread + '}\n return packet\n', - returns=['emit'], paths={'emit': ('action',)}) - assert blockers(rows) == {'dynamic_key'} +# --- argument_name_only: resolved values, and still correctly unresolved ------- -# --- the residue stays honest ------------------------------------------------- +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. -def test_an_unbound_site_is_unresolved_and_never_silently_dropped(): - """No recognized producer means unresolved; it never means dead.""" - rows = scan('def emit(payload):\n return {"action": payload.get("action")}\n') + 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].unresolved and rows[0].blocker == 'call_result' - assert rows[0].values == frozenset() + 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_every_recognized_form_still_labels_what_it_could_not_bind(): - rows = scan('from .owner import Action\ndef pick(flag):\n return Action.RUN.value if flag else late()\n' - 'def emit(flag):\n packet = {"action": pick(flag)}\n' - ' packet["note"] = dynamic()\n return packet\n', - returns=['emit'], paths={'emit': ('action',)}) - assert known(at(rows, 'emit')) == {'run'} - assert all(row.blocker for row in rows if row.unresolved) - - -def test_deep_call_chains_stay_bounded(): - """The memo and the recursion guard keep a long chain linear, not explosive.""" - depth = 60 - text = 'def step0():\n return "run"\n' - text += ''.join(f'def step{i}():\n return step{i - 1}() or step{i - 1}()\n' - for i in range(1, depth)) - text += f'def emit():\n return {{"action": step{depth - 1}()}}\n' - started = time.perf_counter() - rows = scan(text) - assert known(rows) == {'run'} - assert time.perf_counter() - started < 5.0 - - -def test_synthetic_selection_nodes_never_enter_the_shared_tree(): - """Rebinding folds a union for the read only; the parsed tree is untouched.""" - text = ('from .owner import Action\ndef emit(flag):\n choice = Action.RUN.value\n' - ' if flag:\n choice = Action.WAIT.value\n return {"action": choice}\n') - source = SourceFile(CONSUMER, '.py', text) - first = scan_python_production(source, field='action', enums=ENUMS) - before = ast.dump(ast.parse(text)) - second = scan_python_production(source, field='action', enums=ENUMS) - assert first == second - assert ast.dump(ast.parse(text)) == before +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 diff --git a/tests/architecture/test_semantic_python_production.py b/tests/architecture/test_semantic_python_production.py index 59e41a7d0d..faf6299705 100644 --- a/tests/architecture/test_semantic_python_production.py +++ b/tests/architecture/test_semantic_python_production.py @@ -58,14 +58,7 @@ def test_single_local_variable_and_reassignment_boundary(): rows = scan('def emit(flag):\n code = "run" if flag else "wait"\n return code\n', returns=['emit']) assert known(rows) == {'run', 'wait'} assert not any(r.unresolved for r in rows) - # An ordered rebinding is a finite selection, so the literal arm is real - # evidence; the unknown arm still keeps the row unresolved. - # tests/architecture/test_semantic_producer_binding.py covers the form. rows = scan('def emit(flag):\n code = "run"\n if flag:\n code = dynamic()\n return code\n', returns=['emit']) - assert known(rows) == {'run'} - assert rows[0].unresolved - # A store this scan cannot order erases the local altogether. - rows = scan('def emit(codes):\n code = "run"\n for code in codes:\n pass\n return code\n', returns=['emit']) assert known(rows) == set() assert rows[0].unresolved