fix(diagnostics): separate unproved write distinctness from a genuine duplicate (#698)

changelog.d/698-write-distinctness-diagnostic.fixed.md

@@ -0,0 +1,10 @@
+Distinguish proven duplicate writes from conservative `forall` index-distinctness
+rejections in native `check`/`verify`, the browser Worker, and LSP diagnostics.
+Unproved injectivity now reports `FSL-SEMANTIC-WRITE-DISTINCTNESS-UNPROVED` with
+`loc` and a safe repair `hint` when one exists; acceptance is unchanged.
+
+Known limit: an affine write inside an `if` within the `forall` is still reported with the previous duplicate-write message, because `assignment_for_target` only scans top-level assignments. That shape is unchanged from before this fix, not a regression.
+
+The quick-fix is withheld rather than guessed: the RHS scan is built on the shared `expr_children`/`binder_exprs` walk instead of a second hand-written match, a binder whose domain does not start at zero contributes its own lower bound, a filtered binder is refused outright, and an RHS that already names `k` blocks the rewrite. The classification, code and location still arrive in every one of those cases.
+
+The hint is emitted only for a shape it can render correctly: a named key type (an inline `Map<lo..hi, _>` key would render as `forall k: lo..hi`, which the grammar does not accept after `:`), and an offset that is bracketed unless it is already a single token.

docs/DESIGN-v1.md

@@ -182,8 +182,12 @@ state {
   bounded.
 - `Map<Int, ·>` is rejected by `fslc check`. Declare a bounded domain key, for
   example `type K = 0..<max>`, and use `Map<K, ·>`. The guidance is part of
-  the located `message`: the semantic-error envelope has no general `hint`
-  field.
+  the located `message`. The semantic-error envelope carries no general
+  `hint`; a `hint` appears only alongside a `diagnostic_code` that names the
+  classification it repairs, and only when the repair is provably safe for
+  that spec (issue #698 added the first one,
+  `FSL-SEMANTIC-WRITE-DISTINCTNESS-UNPROVED`). Guidance that is not tied to a
+  coded classification stays in `message`, as this `Map<Int, ·>` case does.
 
 ### 3.8 Int / Bool
 

docs/LANGUAGE.ja.md

@@ -685,6 +685,18 @@ until  Name { P until Q }    // unless safety plus a leadsTo P ~> Q progress obl
   代入するのは意味論エラーです。if の then/else は別々のパスなので、両方で代入して
   かまいません。if の**後**に同じ変数へ代入するのもエラーです(分岐の内側の書き込み
   が失われるのを防ぐため)。
+- **保守的な write-alias 拒否**: `forall` 本体が反復間で相異性を証明できない
+  インデックス付き location へ書き込む場合、ネイティブの `check`/`verify` と
+  ブラウザ Worker は検証器バックエンドより前に spec を拒否します。これは
+  **確定した重複 write**(例: `m[0]` を 2 回、`forall c { m[0] = ... }`)とは別で、
+  後者は従来の
+  `an action may not assign the same state location more than once` メッセージを
+  維持します。injectivity 未証明は
+  `cannot prove write-index distinctness across forall iterations` と
+  `diagnostic_code: FSL-SEMANTIC-WRITE-DISTINCTNESS-UNPROVED`、問題の代入 `loc`、
+  安全な修復が存在する場合は
+  `forall k: Cell { if k >= BASE and k < BASE + 4 { m[k] = ... } }` のような
+  `hint` で報告されます。
 - `Map<K, Struct>` の値については、フィールドの書き込みはフィールド単位で追跡され
   ます。1 つの action の中で同じ要素の異なる 2 つのフィールドを更新すること、例えば
   `m[k].f1 = 1` に続く `m[k].f2 = 2` は許されます。同じパスで同じフィールドを繰り返す

docs/LANGUAGE.md

@@ -710,6 +710,17 @@ variable.
   of an if are separate paths, so you may assign in both. Assigning to the same
   variable **after** an if is also an error (to prevent the writes inside the
   branches from being lost).
+- **Conservative write-alias rejection**: when a `forall` body writes an indexed
+  location whose indices are not provably distinct across iterations, native
+  `check`/`verify` and the browser Worker reject the spec before any verifier
+  backend runs. This is distinct from a **proven duplicate write** (for example
+  `m[0]` twice, or `forall c { m[0] = ... }`), which keeps the legacy
+  `an action may not assign the same state location more than once` message.
+  Unproved injectivity is reported as
+  `cannot prove write-index distinctness across forall iterations` with
+  `diagnostic_code: FSL-SEMANTIC-WRITE-DISTINCTNESS-UNPROVED`, the offending
+  assignment `loc`, and—when a safe repair exists—a `hint` such as
+  `forall k: Cell { if k >= BASE and k < BASE + 4 { m[k] = ... } }`.
 - For `Map<K, Struct>` values, field writes are tracked per field. Updating two
   different fields of the same element in one action, such as `m[k].f1 = 1`
   followed by `m[k].f2 = 2`, is allowed. Repeating the same field on the same

docs/intro/language.en.html

@@ -761,6 +761,17 @@ <h1 class="reveal" style="margin-top:14px">Language Reference</h1>
   of an if are separate paths, so you may assign in both. Assigning to the same
   variable <strong>after</strong> an if is also an error (to prevent the writes inside the
   branches from being lost).</li>
+<li><strong>Conservative write-alias rejection</strong>: when a <code>forall</code> body writes an indexed
+  location whose indices are not provably distinct across iterations, native
+  <code>check</code>/<code>verify</code> and the browser Worker reject the spec before any verifier
+  backend runs. This is distinct from a <strong>proven duplicate write</strong> (for example
+  <code>m[0]</code> twice, or <code>forall c { m[0] = ... }</code>), which keeps the legacy
+  <code>an action may not assign the same state location more than once</code> message.
+  Unproved injectivity is reported as
+  <code>cannot prove write-index distinctness across forall iterations</code> with
+  <code>diagnostic_code: FSL-SEMANTIC-WRITE-DISTINCTNESS-UNPROVED</code>, the offending
+  assignment <code>loc</code>, and—when a safe repair exists—a <code>hint</code> such as
+  <code>forall k: Cell { if k &gt;= BASE and k &lt; BASE + 4 { m[k] = ... } }</code>.</li>
 <li>For <code>Map&lt;K, Struct&gt;</code> values, field writes are tracked per field. Updating two
   different fields of the same element in one action, such as <code>m[k].f1 = 1</code>
   followed by <code>m[k].f2 = 2</code>, is allowed. Repeating the same field on the same

docs/intro/language.ja.html

@@ -737,6 +737,18 @@ <h1 class="reveal" style="margin-top:14px">言語リファレンス</h1>
   代入するのは意味論エラーです。if の then/else は別々のパスなので、両方で代入して
   かまいません。if の<strong>後</strong>に同じ変数へ代入するのもエラーです(分岐の内側の書き込み
   が失われるのを防ぐため)。</li>
+<li><strong>保守的な write-alias 拒否</strong>: <code>forall</code> 本体が反復間で相異性を証明できない
+  インデックス付き location へ書き込む場合、ネイティブの <code>check</code>/<code>verify</code> と
+  ブラウザ Worker は検証器バックエンドより前に spec を拒否します。これは
+  <strong>確定した重複 write</strong>(例: <code>m[0]</code> を 2 回、<code>forall c { m[0] = ... }</code>)とは別で、
+  後者は従来の
+  <code>an action may not assign the same state location more than once</code> メッセージを
+  維持します。injectivity 未証明は
+  <code>cannot prove write-index distinctness across forall iterations</code> と
+  <code>diagnostic_code: FSL-SEMANTIC-WRITE-DISTINCTNESS-UNPROVED</code>、問題の代入 <code>loc</code>、
+  安全な修復が存在する場合は
+  <code>forall k: Cell { if k &gt;= BASE and k &lt; BASE + 4 { m[k] = ... } }</code> のような
+  <code>hint</code> で報告されます。</li>
 <li><code>Map&lt;K, Struct&gt;</code> の値については、フィールドの書き込みはフィールド単位で追跡され
   ます。1 つの action の中で同じ要素の異なる 2 つのフィールドを更新すること、例えば
   <code>m[k].f1 = 1</code> に続く <code>m[k].f2 = 2</code> は許されます。同じパスで同じフィールドを繰り返す

rust/fsl-core/src/lib.rs

@@ -61,8 +61,9 @@ pub use domain::{DomainDefault, domain_kernel_source, domain_type_default};
 pub use domain_lowering::{domain_effect_owns_event, event_flag, state_name};
 pub use expr_text::{binder_text, expr_text, source_binder_text, source_expr_text};
 pub use model::{
-    ActionDef, ActionGuard, KernelModel, LeadsToDef, ModelError, ParamDef, PropertyDef, TypeDef,
-    TypeRef, Value as FslValue, build_model, static_leadsto_bindings,
+    ActionDef, ActionGuard, DiagnosticEdit, KernelModel, LeadsToDef, ModelError, ParamDef,
+    PropertyDef, TypeDef, TypeRef, Value as FslValue, WRITE_DISTINCTNESS_UNPROVED_CODE,
+    build_model, static_leadsto_bindings,
 };
 pub use origin::{
     INIT_TARGET, LoweringStep, OriginChain, OriginId, OriginRegistry, OriginSite, SPEC_TARGET,