feat(acpy): narrow proven rule field writes to field-level proposals

[zhoubot]

Frontend half of #129, on top of the merged backend (#141).

依赖与后继关系

本 PR 已被 #145 取代，请勿单独合并本 PR。

#145 完整吸收了本 PR 的 proven frontend field-write 切片，并进一步支持 module-local Table、普通/@ac.inline helper 的一致 provenance、同一 firing 对同一 Table 的不同字段 schema 多 proposal，以及 GFSim 逐条 footprint 原子批次。

#145 当前堆叠在 #144 上，而 #144 又依赖 #142；合并顺序为 #142 → #144 → #145。依赖合并后，#145 将 rebase 到最新 main。本 PR 保留用于历史评审和证据追踪，不应与 #145 分别合入。

Background

Two rules that update different fields of one Table Entry both lowered to ac.table.propose ... mode "replace" with the complete field set, so ac-lower-rules rejected them with "same-field overlap on owner @entries requires explicit priority on every writer endpoint", forcing one logical entry into several state banks.

#134 narrowed the frontend but only verified through ac-lower-rules: the narrowed firing write was mode "field", which the QueueGraph plan rejected, so it was reverted in #139. #141 then landed the backend: plan and CodeGen accept field-mode firing writes, and PYC commits them in gfsim's order (every FieldMerge against the committed image, then every Replace). This PR re-lands the frontend on top of it and verifies end to end.

What lands

ac.table + explicit with_fields (revives #134). proven_field_write_fields narrows a rule write to mode "field" with the canonical declaration-ordered field set only when the assigned value is provably the recorded read of that same target updated by with_fields(...) and the write index AST-equals the recorded read index. Any other producer keeps the complete replacement; recognition is syntactic and fail-closed.

Direct spelling entries[i].field = value. The field-assignment normalization binds the index once and rewrites the target into the with_fields form. For explicit ac.table owners the generated index binding is folded back into the recorded read, keeping the single-indexed-write grammar and the entry-locked result contract; a direct write without a recorded read feeding the rule result keeps the existing fail-closed behavior. For indexed persistent list[Struct] owners, ac-lower-variable-state now recognizes an ac.var.with chain rooted at the same-variable, same-index element read and emits mode "field" with the canonical field set (Decision 0261); input-rooted, other-index, and whole-value producers stay complete replacements.

Verifier tightening (from #134). The allocation-versus-field exemption in VerifyValueConstraints now requires both sides to be declarative field writers (ac.table.write in field mode, ac.table.masked_write), so a rule field proposal keeps arbitrating against a declarative allocation instead of inheriting the batch exemption (Decision 0156 order does not cover it).

Verification (deeper than #134 could go)

#134 verified only through ac-lower-rules because its checkout had a standalone ACIR build. This PR was verified with the integrated toolchain:

• python_frontend unittest: 393 OK (1 skipped)
• check-acir lit: 244/244 (100%) — including the 7 PYC/CodeGen lanes a standalone build misses (pycc/pyc-opt from this checkout's integrated toolchain)
• ctest: 18/18
• contracts unittest: 50 OK; check-contracts.py OK; check_decision_status.py ok (rows=261, deferred=0); IR coverage + PYC inventory ledgers regenerated
• e2e test_table_backend: 8/8, including the new test_rule_field_writers_merge_same_entry_in_native_cpp: two @ac.rule field writers commit disjoint fields of one Entry in native gfsim simulation, the unwritten field keeps its committed value, other entries untouched
• New lit fixture variable-element-field-write-lowering.mlir pins the list[Struct] narrowing boundary; the revived rule-field-write-merge.mlir now also pins freeze → plan → cxxgen → pycgen

Evidence: docs/gates/logs/20260915-issue129-frontend-field-writes/

Not in this slice (still #129)

• with ac.assert_disjoint(...) and cross-rule dynamic conflict obligations, with their gfsim/PYC/Verilog commit gating.
• Several field assignments to one target in a single rule (the frontend still allows one indexed state assignment per rule).
• The direct field spelling on ac.table without a recorded read feeding the rule result (fails closed with ACPY-RULE-008 today, matching the no-return table rule behavior on main).
• Full AC G0/G1/G2 closure and Verilator parity for this fixture; PYC emission parity is pinned structurally by the lit PYC checks.

refs #129

[zhoubot]

Review disposition: this slice is superseded by #145, as this PR body and #145 both state. I found no separate merge blocker in the historical diff, but it must not be merged independently; close it as superseded after #145 lands.

[zhoubot]

Closing as superseded by #145, per this PR description and the merged stack plan. Its frontend field-write slice is incorporated in #145 and must not be merged separately.