Problem
保守的な write-alias checker が「衝突を証明した」のではなく「反復間の index distinctness を証明できなかった」場合にも、次の断定的な semantics error を返す。
an action may not assign the same state location more than once
例えば forall c: Compartment { comp[d*NC + c] = ... } は、binder c の係数が 1 なので反復ごとの index は数学的には distinct だが、現実装の write_is_injective_for_binder は index が binder 単体のときだけ受理する。現在の message は実際の二重代入と解析限界を区別せず、利用者を誤った修正へ誘導する。
Evidence
- field report:
yumemi/referance/src/fsl/label_core.fsl の旧 cite / declassify / rehandshake 形
- current implementation:
rust/fsl-core/src/model.rs::write_is_injective_for_binder は m[c] のみを injective と判定
- existing diagnostic:
rust/fsl-core/src/model.rs::action が alias classification を捨てて同一 message を生成
- accepted workaround was found only after experiments: flattened Map の全域 binder と exact range guard を使い、write index 自体を binder にする
Desired diagnostic contract
確定した同一 location への重複 write と、alias / injectivity を証明できないため fail-closed したケースを区別する。後者は少なくとも次を返す。
- stable machine-readable diagnostic code/classification
- message:
cannot prove write-index distinctness across forall iterations 相当
- offending assignment の正確な
loc
hint: forall k: Cell { if k >= base and k < base + width { m[k] = ... } } のように、index を binder 自体にした受理形（具体的な型・名前に合わせる）
Acceptance criteria
Relationship
係数1 affine を実際に受理する #699 と、guard 排他を扱う #700 とは独立に先行できる。将来受理範囲が広がっても、解析不能な残余ケースには正確な fail-closed diagnostic が必要。
Problem
保守的な write-alias checker が「衝突を証明した」のではなく「反復間の index distinctness を証明できなかった」場合にも、次の断定的な semantics error を返す。
例えば
forall c: Compartment { comp[d*NC + c] = ... }は、bindercの係数が 1 なので反復ごとの index は数学的には distinct だが、現実装のwrite_is_injective_for_binderは index が binder 単体のときだけ受理する。現在の message は実際の二重代入と解析限界を区別せず、利用者を誤った修正へ誘導する。Evidence
yumemi/referance/src/fsl/label_core.fslの旧cite/declassify/rehandshake形rust/fsl-core/src/model.rs::write_is_injective_for_binderはm[c]のみを injective と判定rust/fsl-core/src/model.rs::actionが alias classification を捨てて同一 message を生成Desired diagnostic contract
確定した同一 location への重複 write と、alias / injectivity を証明できないため fail-closed したケースを区別する。後者は少なくとも次を返す。
cannot prove write-index distinctness across forall iterations相当lochint:forall k: Cell { if k >= base and k < base + width { m[k] = ... } }のように、index を binder 自体にした受理形（具体的な型・名前に合わせる）Acceptance criteria
m[0]を2回、forall c { m[0] = ... }) は従来どおり明確な duplicate-write errorm[base + c], non-affine index, collection binder) は distinctness-unproved classificationloc、actionablehintがあるcheckを通る positive control を持つcheck/verify, Worker, LSP diagnostic / quick-fix surface が分類と位置を共有するdocs/LANGUAGE.md,docs/LANGUAGE.ja.md,skills/fsl/reference.mdの double-assignment 説明が「確定 duplicate」と「保守的拒否」を区別するRelationship
係数1 affine を実際に受理する #699 と、guard 排他を扱う #700 とは独立に先行できる。将来受理範囲が広がっても、解析不能な残余ケースには正確な fail-closed diagnostic が必要。