diff --git a/changelog.d/698-write-distinctness-diagnostic.fixed.md b/changelog.d/698-write-distinctness-diagnostic.fixed.md new file mode 100644 index 00000000..136947ad --- /dev/null +++ b/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` 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. diff --git a/docs/DESIGN-v1.md b/docs/DESIGN-v1.md index 2d13e39d..b9b401c3 100644 --- a/docs/DESIGN-v1.md +++ b/docs/DESIGN-v1.md @@ -182,8 +182,12 @@ state { bounded. - `Map` is rejected by `fslc check`. Declare a bounded domain key, for example `type K = 0..`, and use `Map`. 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` case does. ### 3.8 Int / Bool diff --git a/docs/LANGUAGE.ja.md b/docs/LANGUAGE.ja.md index fd36588f..8b305157 100644 --- a/docs/LANGUAGE.ja.md +++ b/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` の値については、フィールドの書き込みはフィールド単位で追跡され ます。1 つの action の中で同じ要素の異なる 2 つのフィールドを更新すること、例えば `m[k].f1 = 1` に続く `m[k].f2 = 2` は許されます。同じパスで同じフィールドを繰り返す diff --git a/docs/LANGUAGE.md b/docs/LANGUAGE.md index 5635bf0f..43787c3f 100644 --- a/docs/LANGUAGE.md +++ b/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` 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 diff --git a/docs/intro/language.en.html b/docs/intro/language.en.html index 76f949a2..483cc169 100644 --- a/docs/intro/language.en.html +++ b/docs/intro/language.en.html @@ -761,6 +761,17 @@

Language Reference

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 diff --git a/docs/intro/language.ja.html b/docs/intro/language.ja.html index 7577df81..7cd70445 100644 --- a/docs/intro/language.ja.html +++ b/docs/intro/language.ja.html @@ -737,6 +737,18 @@

    言語リファレンス

    代入するのは意味論エラーです。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 は許されます。同じパスで同じフィールドを繰り返す diff --git a/rust/fsl-core/src/lib.rs b/rust/fsl-core/src/lib.rs index 6a6924ac..83afa0d9 100644 --- a/rust/fsl-core/src/lib.rs +++ b/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, diff --git a/rust/fsl-core/src/model.rs b/rust/fsl-core/src/model.rs index 2b9dcade..7550ce63 100644 --- a/rust/fsl-core/src/model.rs +++ b/rust/fsl-core/src/model.rs @@ -11,10 +11,21 @@ use fsl_syntax::{ use crate::{ INIT_TARGET, KernelSpec, LoweringStep, OriginChain, OriginId, OriginRegistry, OriginSite, - ProjectionDef, SPEC_TARGET, TERMINAL_TARGET, TraceabilityRegistry, action_target, + ProjectionDef, SPEC_TARGET, TERMINAL_TARGET, TraceabilityRegistry, action_target, expr_text, property_target, state_target, type_target, }; +/// Stable semantic diagnostic code for a conservative write-alias rejection where +/// index distinctness across `forall` iterations could not be proved (issue #698). +pub const WRITE_DISTINCTNESS_UNPROVED_CODE: &str = "FSL-SEMANTIC-WRITE-DISTINCTNESS-UNPROVED"; + +/// A machine-applicable source edit carried by a typed model diagnostic. +#[derive(Clone, Debug, Eq, PartialEq)] +pub struct DiagnosticEdit { + pub span: Span, + pub replacement: String, +} + #[derive(Clone, Debug, Eq, Ord, PartialEq, PartialOrd)] pub enum Value { Int(i64), @@ -462,6 +473,12 @@ pub struct ModelError { /// Whether this is a name-resolution failure. See /// [`crate::CoreError::name_resolution`] (issue 565). pub name_resolution: bool, + /// Stable machine-readable classification when the frontend knows it. + pub diagnostic_code: Option<&'static str>, + /// Actionable repair guidance for delivery surfaces that render hints. + pub hint: Option>, + /// A machine-applicable edit for LSP quick-fix surfaces. + pub quick_fix: Option>, } impl ModelError { @@ -486,6 +503,24 @@ impl ModelError { } self } + + #[must_use] + fn with_diagnostic_code(mut self, code: &'static str) -> Self { + self.diagnostic_code = Some(code); + self + } + + #[must_use] + fn with_hint(mut self, hint: impl Into) -> Self { + self.hint = Some(Box::new(hint.into())); + self + } + + #[must_use] + fn with_quick_fix(mut self, edit: DiagnosticEdit) -> Self { + self.quick_fix = Some(Box::new(edit)); + self + } } fn with_type_diagnostic_origin(mut error: ModelError, span: Span) -> ModelError { @@ -594,6 +629,9 @@ impl ModelBuilder { origin: Some(Box::new(source_origin("annotation", error.span, None))), span: Some(error.span), name_resolution: false, + diagnostic_code: None, + hint: None, + quick_fix: None, })?; let state_names = self .spec @@ -1232,13 +1270,23 @@ impl ModelBuilder { } let mut index_constants = self.consts.clone(); index_constants.extend(self.enum_members.clone()); - if let Some((_, duplicate_span)) = duplicate_statement_write(&statements, &index_constants) - { - return Err(model_error( - "an action may not assign the same state location more than once", - ) - .with_origin(self.origins.diagnostic_origin(&action_target(name))) - .at(duplicate_span)); + if let Some(conflict) = duplicate_statement_write(&statements, &index_constants) { + return Err(match conflict { + WriteAliasConflict::Duplicate((_, duplicate_span)) => { + model_error("an action may not assign the same state location more than once") + .with_origin(self.origins.diagnostic_origin(&action_target(name))) + .at(duplicate_span) + } + WriteAliasConflict::DistinctnessUnproved(conflict) => self + .write_distinctness_unproved_error( + name, + &conflict.target, + &conflict.value, + conflict.span, + &conflict.binder, + conflict.forall_span, + ), + }); } Ok(ActionDef { name: name.to_owned(), @@ -1443,6 +1491,139 @@ impl ModelBuilder { _ => Err(model_error("constant expression must be an integer")), } } + + fn write_distinctness_unproved_error( + &self, + action_name: &str, + target: &LValue, + value: &Expr, + span: Span, + binder: &Binder, + forall_span: Span, + ) -> ModelError { + let mut error = + model_error("cannot prove write-index distinctness across forall iterations") + .with_diagnostic_code(WRITE_DISTINCTNESS_UNPROVED_CODE) + .with_origin(self.origins.diagnostic_origin(&action_target(action_name))) + .at(span); + if let Some((hint, replacement)) = + self.try_distinctness_hint(target, value, binder, forall_span) + { + error = error.with_hint(hint).with_quick_fix(DiagnosticEdit { + span: forall_span, + replacement, + }); + } + error + } + + fn try_distinctness_hint( + &self, + target: &LValue, + value: &Expr, + binder: &Binder, + forall_span: Span, + ) -> Option<(String, String)> { + let LValue::Index(map_name, index) = target else { + return None; + }; + let binder_name = match binder { + Binder::Typed { name, .. } | Binder::Range { name, .. } => name, + Binder::Collection { .. } => return None, + }; + if expr_contains_var(value, binder_name) { + return None; + } + let key_type = self.map_key_type_name(map_name)?; + let offset = affine_binder_offset(index, binder_name)?; + // The binder's real bounds, not its width: `Off = 2..5` indexed as + // `BASE + c` covers `BASE+2..=BASE+5`, and a width-only rewrite writes + // `BASE..BASE+4`. `binder_domain_bounds` also refuses a filtered binder, + // whose subset this rewrite cannot reproduce. + let (lo, hi) = self.binder_domain_bounds(binder)?; + // The replacement introduces `k`. If the RHS or the offset already + // refers to a `k` from an enclosing scope, the new binder captures it + // and the rewrite changes meaning. Refuse instead of renaming: the + // classification, code and location still reach the reader. + if expr_contains_var(value, "k") || expr_contains_var(&offset, "k") || map_name == "k" { + return None; + } + // `hi + 1` is the exclusive upper bound; refuse rather than wrap if the + // domain reaches i64::MAX. + let exclusive_hi = hi.checked_add(1)?; + // The offset is spliced into `k >= ` and `k < + n`. + // `expr_text` does not parenthesize a conditional or a binary operand, + // so anything that is not already atomic must be wrapped or the emitted + // comparison reassociates. + let offset_text = match &offset { + Expr::Var(_) | Expr::Num(_) | Expr::Field(..) => expr_text(&offset), + other => format!("({})", expr_text(other)), + }; + let rhs = expr_text(value); + // The written set is `offset + lo ..= offset + hi`, so the exclusive + // upper bound is `offset + hi + 1`. Emitting `offset + width` instead + // silently shifts the whole interval whenever `lo != 0`. + let low_text = if lo == 0 { + offset_text.clone() + } else { + format!("{offset_text} + {lo}") + }; + let high_text = format!("{offset_text} + {exclusive_hi}"); + let replacement = format!( + "forall k: {key_type} {{ if k >= {low_text} and k < {high_text} {{ {map_name}[k] = {rhs} }} }}" + ); + let _ = forall_span; + let hint = replacement.clone(); + Some((hint, replacement)) + } + + fn map_key_type_name(&self, map_name: &str) -> Option { + self.spec.items.iter().find_map(|item| match item { + SpecItem::State(fields) => fields.iter().find_map(|field| { + if field.name != map_name { + return None; + } + match &field.ty { + TypeExpr::Map(key, _) => type_expr_display_name(key), + _ => None, + } + }), + _ => None, + }) + } + + /// The binder's inclusive `(lo, hi)`, or `None` when it is not a bounded + /// integer domain. #698's quick-fix needs the lower bound, not just the + /// width: `Off = 2..5` indexed as `BASE + c` covers `BASE+2..=BASE+5`, and + /// a width-only rewrite writes `BASE..BASE+4` -- a different set. + fn binder_domain_bounds(&self, binder: &Binder) -> Option<(i64, i64)> { + match binder { + Binder::Typed { + type_name, + where_expr, + .. + } => { + // A filtered binder ranges over a subset this rewrite cannot + // reproduce, so refuse rather than widen it. + if where_expr.is_some() { + return None; + } + match self.types.get(&type_name.name) { + Some(TypeDef::Domain { lo, hi, .. }) => Some((*lo, *hi)), + _ => None, + } + } + Binder::Range { + lo, hi, where_expr, .. + } => { + if where_expr.is_some() { + return None; + } + Some((self.const_int(lo).ok()?, self.const_int(hi).ok()?)) + } + Binder::Collection { .. } => None, + } + } } fn resolve_type( @@ -1488,6 +1669,21 @@ fn const_int(expr: &Expr, consts: &BTreeMap) -> Result), +} + /// Find a state location an action writes twice, with the span of the write /// that repeats it. /// @@ -1496,11 +1692,11 @@ type StateWrite = (LValue, Span); fn duplicate_statement_write( statements: &[Statement], constants: &BTreeMap, -) -> Option { +) -> Option { fn writes( statements: &[Statement], constants: &BTreeMap, - ) -> Result, Box> { + ) -> Result, Box> { let mut seen: Vec<(LValue, Span)> = Vec::new(); for statement in statements { let candidates = match statement { @@ -1515,14 +1711,39 @@ fn duplicate_statement_write( branch } Statement::ForAll { - binder, statements, .. + binder, + statements, + span: forall_span, + .. } => { let repeated = writes(statements, constants)?; - if let Some(write) = repeated + if let Some((target, write_span)) = repeated .iter() .find(|(target, _)| !write_is_injective_for_binder(target, binder)) { - return Err(Box::new(write.clone())); + let (_, index, _) = lvalue_path(target); + if index.is_some_and(|idx| static_index_identity(idx, constants).is_some()) + { + return Err(Box::new(WriteAliasConflict::Duplicate(( + target.clone(), + *write_span, + )))); + } + let Some((value, _)) = assignment_for_target(statements, target) else { + return Err(Box::new(WriteAliasConflict::Duplicate(( + target.clone(), + *write_span, + )))); + }; + return Err(Box::new(WriteAliasConflict::DistinctnessUnproved( + Box::new(DistinctnessUnprovedWrite { + target: target.clone(), + value, + span: *write_span, + binder: binder.clone(), + forall_span: *forall_span, + }), + ))); } repeated } @@ -1531,7 +1752,7 @@ fn duplicate_statement_write( seen.iter() .any(|(previous, _)| lvalues_may_alias(previous, target, constants)) }) { - return Err(Box::new(write.clone())); + return Err(Box::new(WriteAliasConflict::Duplicate(write.clone()))); } seen.extend(candidates); } @@ -1540,6 +1761,74 @@ fn duplicate_statement_write( writes(statements, constants).err().map(|write| *write) } +fn assignment_for_target(statements: &[Statement], target: &LValue) -> Option<(Expr, Span)> { + statements.iter().find_map(|statement| match statement { + Statement::Assign { + target: candidate, + value, + span, + } if candidate == target => Some((value.clone(), *span)), + _ => None, + }) +} + +/// The key type as it may appear after `forall k:`. +/// +/// Deliberately named types only. An inline `Map<0..7, _>` key would render as +/// `forall k: 0..7`, but the grammar only accepts a qualified name after `:` +/// (`fsl-syntax`'s `parser.rs`, the `qualified_name()` call in the binder rule); +/// the range form is spelled `forall k in 0..7`. Emitting the former produces a +/// hint that does not parse, which is a worse outcome than no hint: #698's +/// contract is that the repair it names actually checks. +fn type_expr_display_name(ty: &TypeExpr) -> Option { + match ty { + TypeExpr::Name(name) => Some(name.clone()), + _ => None, + } +} + +fn affine_binder_offset(index: &Expr, binder_name: &str) -> Option { + match index { + Expr::Binary { op, left, right } if op == "+" => { + if matches!(&**right, Expr::Var(name) if name == binder_name) + && !expr_contains_var(left, binder_name) + { + return Some(left.as_ref().clone()); + } + if matches!(&**left, Expr::Var(name) if name == binder_name) + && !expr_contains_var(right, binder_name) + { + return Some(right.as_ref().clone()); + } + } + _ => {} + } + None +} + +fn expr_contains_var(expr: &Expr, name: &str) -> bool { + // Built on `expr_children`/`binder_exprs` rather than a second hand-written + // match: the hand-written one silently missed `Expr::Method`'s `args` and a + // quantifier's own range/filter, and #698's quick-fix guard reads this. A + // walk that drifts from the AST here does not merely miss a case, it emits + // an edit that moves an RHS out of the scope that bound it. Any new `Expr` + // variant is covered the moment `expr_children` covers it. + if let Expr::Var(candidate) = expr + && candidate == name + { + return true; + } + // A binder's own range and filter are evaluated in the outer scope, and its + // body may shadow `name`. Fail closed on the whole construct rather than + // modelling that: refusing a hint is safe, offering a captured one is not. + if matches!(expr, Expr::Quantified { .. } | Expr::Aggregate { .. }) { + return true; + } + expr_children(expr) + .into_iter() + .any(|child| expr_contains_var(child, name)) +} + fn write_is_injective_for_binder(target: &LValue, binder: &Binder) -> bool { let name = match binder { Binder::Typed { name, .. } | Binder::Range { name, .. } => name, @@ -2080,6 +2369,9 @@ fn model_error(message: impl Into) -> ModelError { origin: None, span: None, name_resolution: false, + diagnostic_code: None, + hint: None, + quick_fix: None, } } diff --git a/rust/fsl-core/src/reserved.rs b/rust/fsl-core/src/reserved.rs index e5520c6e..5f7f02e0 100644 --- a/rust/fsl-core/src/reserved.rs +++ b/rust/fsl-core/src/reserved.rs @@ -63,6 +63,9 @@ fn reject(name: &str, position: &str, span: Option) -> ModelError { // classification did not exist yet (issue 565), and recorded the move // as pending. name_resolution: true, + diagnostic_code: None, + hint: None, + quick_fix: None, } } diff --git a/rust/fsl-core/tests/duplicate_writes.rs b/rust/fsl-core/tests/duplicate_writes.rs index 89fca5c0..657bc65e 100644 --- a/rust/fsl-core/tests/duplicate_writes.rs +++ b/rust/fsl-core/tests/duplicate_writes.rs @@ -93,6 +93,27 @@ fn rejects_a_constant_index_repeated_by_forall() { .expect_err("constant write repeats across forall iterations"); assert!(error.message.contains("same state location")); + assert!(error.diagnostic_code.is_none()); +} + +#[test] +fn classifies_affine_forall_index_as_distinctness_unproved() { + let error = build( + "spec Affine { type Cell = 0..7 type Off = 0..3 const BASE = 2 \ + state { m: Map } init { forall i: Cell { m[i] = false } } \ + action shift() { forall c: Off { m[BASE + c] = true } } }", + ) + .expect_err("affine index must stay rejected with distinctness classification"); + + assert_eq!( + error.message, + "cannot prove write-index distinctness across forall iterations" + ); + assert_eq!( + error.diagnostic_code, + Some(fsl_core::WRITE_DISTINCTNESS_UNPROVED_CODE) + ); + assert!(error.hint.is_some()); } #[test] diff --git a/rust/fsl-lsp/src/server.rs b/rust/fsl-lsp/src/server.rs index 184f1c42..bf38b6ae 100644 --- a/rust/fsl-lsp/src/server.rs +++ b/rust/fsl-lsp/src/server.rs @@ -761,29 +761,74 @@ const fn token_type(role: SymbolRole) -> u32 { fn code_actions(state: &ServerState, uri: &Url) -> Option> { let source = source_for_uri(state, uri)?; - let rewrites = fsl_syntax::canonical_rewrites(&source).ok()?; - Some( - rewrites - .into_iter() - .map(|rewrite| { - let edits = rewrite - .edits - .into_iter() - .map(|edit| TextEdit::new(span_range(&source, edit.span), edit.replacement)) - .collect::>(); + let path = uri.to_file_path().ok(); + let base = path + .as_deref() + .and_then(Path::parent) + .unwrap_or_else(|| Path::new(".")); + let resolver = StoreResolver { + state, + base: base.to_path_buf(), + }; + let source_file = path + .as_deref() + .and_then(Path::to_str) + .unwrap_or(uri.as_str()); + let (diagnostics, _) = + fslc_rust::source_diagnostic::diagnostics_with_model(&source, source_file, &resolver); + let semantic_fixes = diagnostics + .into_iter() + .filter_map(|diagnostic| { + diagnostic.quick_fix.map(|edit| { CodeActionOrCommand::CodeAction(CodeAction { - title: format!("Use canonical FSL: {}", rewrite.canonical_replacement), + title: "Apply write-index distinctness repair".to_owned(), kind: Some(CodeActionKind::QUICKFIX), diagnostics: None, - edit: Some(WorkspaceEdit::new(HashMap::from([(uri.clone(), edits)]))), + edit: Some(WorkspaceEdit::new(HashMap::from([( + uri.clone(), + vec![TextEdit::new( + span_range(&source, edit.span), + edit.replacement, + )], + )]))), command: None, is_preferred: Some(true), disabled: None, data: None, }) }) - .collect(), - ) + }) + .collect::>(); + let rewrites = fsl_syntax::canonical_rewrites(&source).ok()?; + let canonical_fixes = rewrites + .into_iter() + .map(|rewrite| { + let edits = rewrite + .edits + .into_iter() + .map(|edit| TextEdit::new(span_range(&source, edit.span), edit.replacement)) + .collect::>(); + CodeActionOrCommand::CodeAction(CodeAction { + title: format!("Use canonical FSL: {}", rewrite.canonical_replacement), + kind: Some(CodeActionKind::QUICKFIX), + diagnostics: None, + edit: Some(WorkspaceEdit::new(HashMap::from([(uri.clone(), edits)]))), + command: None, + is_preferred: Some(true), + disabled: None, + data: None, + }) + }) + .collect::>(); + let actions = semantic_fixes + .into_iter() + .chain(canonical_fixes) + .collect::>(); + if actions.is_empty() { + None + } else { + Some(actions) + } } fn workspace_roots(params: &InitializeParams) -> Vec { diff --git a/rust/fsl-wasm/src/lib.rs b/rust/fsl-wasm/src/lib.rs index 7d0c9810..266fa9cd 100644 --- a/rust/fsl-wasm/src/lib.rs +++ b/rust/fsl-wasm/src/lib.rs @@ -124,6 +124,8 @@ fn verifier_error(solver_version: &str, failure: &impl std::fmt::Display) -> Val &failure.to_string(), None, false, + None, + None, ) } @@ -152,12 +154,14 @@ fn build(request: &Request, solver_version: &str) -> Result<(KernelModel, Vec (Val &diagnostic.message, diagnostic.located.then(|| diagnostic.span.python_loc()), diagnostic.kind == "name", + Some(diagnostic.code.as_str()).filter(|code| { + *code != "FSL-SEMANTIC" && *code != "FSL-TYPE" && *code != "FSL-NAME" + }), + diagnostic.hint.as_deref(), ), 2, ); @@ -16688,8 +16692,9 @@ fn load_kernel_model_from_source( Ok(kernel) => kernel, Err(error) => return Err(kernel_load_error(source, &error)), }; - let model = fsl_core::build_model(kernel.clone()) - .map_err(|error| SpecLoadError::Semantic(SemanticDiagnostic::from_model_error(&error)))?; + let model = fsl_core::build_model(kernel.clone()).map_err(|error| { + SpecLoadError::Semantic(Box::new(SemanticDiagnostic::from_model_error(&error))) + })?; Ok((kernel, model)) } @@ -16962,14 +16967,15 @@ fn load_model_scoped_from_source( // A rejected `--instances`/`--values` bound is a CLI argument // defect, not a construct in the spec, so it owns no location. Err(error) if error.message.starts_with("--instances/--values") => { - return Err(SpecLoadError::Semantic(SemanticDiagnostic::unlocated( - error.message, + return Err(SpecLoadError::Semantic(Box::new( + SemanticDiagnostic::unlocated(error.message), ))); } Err(error) => return Err(kernel_load_error(source, &error)), }; - fsl_core::build_model(kernel) - .map_err(|error| SpecLoadError::Semantic(SemanticDiagnostic::from_model_error(&error))) + fsl_core::build_model(kernel).map_err(|error| { + SpecLoadError::Semantic(Box::new(SemanticDiagnostic::from_model_error(&error))) + }) } fn envelope() -> Map { @@ -17031,7 +17037,14 @@ fn normalized_exit_status(output: &Value, reported_status: i32) -> i32 { } fn semantic_error_output(message: &str) -> Value { - fslc_rust::verification_output::render_semantic_error(envelope(), message, None, false) + fslc_rust::verification_output::render_semantic_error( + envelope(), + message, + None, + false, + None, + None, + ) } /// Render a core frontend/lowering diagnostic without discarding its typed @@ -17043,6 +17056,8 @@ fn core_error_output(error: &fsl_core::CoreError) -> Value { &diagnostic.message, diagnostic.loc, diagnostic.name_resolution, + diagnostic.diagnostic_code, + diagnostic.hint.as_deref(), ) } @@ -17073,6 +17088,8 @@ fn model_error_output(error: &fsl_core::ModelError) -> Value { &error.to_string(), fslc_rust::verification_output::model_error_loc(error), error.name_resolution, + error.diagnostic_code, + error.hint.as_deref().map(String::as_str), ) } diff --git a/rust/fslc/src/source_diagnostic.rs b/rust/fslc/src/source_diagnostic.rs index fbd9f30d..2ffee2ba 100644 --- a/rust/fslc/src/source_diagnostic.rs +++ b/rust/fslc/src/source_diagnostic.rs @@ -14,6 +14,8 @@ pub struct SourceDiagnostic { /// document as a last resort, but the CLI's `loc` must stay absent rather /// than claim a position the diagnostic does not have (issue 555). pub located: bool, + pub hint: Option, + pub quick_fix: Option, } /// Run the authoritative syntax and typed-model gates and return editor diagnostics. @@ -48,6 +50,8 @@ pub fn diagnostics_with_model( message: error.to_string(), span: error.span, located: true, + hint: None, + quick_fix: None, }], None, ), @@ -63,6 +67,8 @@ pub fn diagnostics_with_model( message: error.to_string(), span: error.span, located: true, + hint: None, + quick_fix: None, }], None, ); @@ -102,6 +108,8 @@ fn core_diagnostic(source: &str, error: &fsl_core::CoreError) -> SourceDiagnosti // `line`/`column` also carry legacy placeholders such as `(1, 1)`. // Only an authored origin proves that the public location is real. located: diagnostic.loc.is_some(), + hint: None, + quick_fix: None, } } @@ -120,14 +128,19 @@ fn model_diagnostic(source: &str, error: &fsl_core::ModelError) -> SourceDiagnos .or_else(|| diagnostic_span_from_message(source, &message)); SourceDiagnostic { kind, - code: match kind { - "type" => "FSL-TYPE".to_owned(), - "name" => "FSL-NAME".to_owned(), - _ => "FSL-SEMANTIC".to_owned(), - }, + code: error.diagnostic_code.map_or_else( + || match kind { + "type" => "FSL-TYPE".to_owned(), + "name" => "FSL-NAME".to_owned(), + _ => "FSL-SEMANTIC".to_owned(), + }, + str::to_owned, + ), message, span: located.unwrap_or_else(|| point_span(source, 1, 1)), located: located.is_some(), + hint: error.hint.as_deref().cloned(), + quick_fix: error.quick_fix.as_deref().cloned(), } } @@ -166,6 +179,8 @@ fn migration_diagnostics(source: &str) -> Vec { message: message.to_owned(), span: rewrite.span, located: true, + hint: None, + quick_fix: None, } }) .collect() diff --git a/rust/fslc/src/spec_load.rs b/rust/fslc/src/spec_load.rs index 46e1c2bc..2e13bc99 100644 --- a/rust/fslc/src/spec_load.rs +++ b/rust/fslc/src/spec_load.rs @@ -38,7 +38,11 @@ use serde_json::{Map, Value, json}; pub enum SpecLoadError { Io(String), Parse(Box), - Semantic(SemanticDiagnostic), + // Boxed for the same reason as `Parse` above: #698 added a diagnostic + // code, hint and quick-fix edit to the typed-model error this carries, + // which pushed the inline variant past clippy's `result_large_err` + // threshold for every `Result<_, SpecLoadError>` in the crate. + Semantic(Box), } /// A typed-model spec-load failure with the location the model recorded for the @@ -50,6 +54,9 @@ pub struct SemanticDiagnostic { /// Whether the failure was resolving a name, which `docs/DESIGN-v1.md` /// §7.2 classifies `kind:"name"` (issue 565). pub name_resolution: bool, + pub diagnostic_code: Option<&'static str>, + pub hint: Option, + pub quick_fix: Option, } impl SemanticDiagnostic { @@ -61,6 +68,9 @@ impl SemanticDiagnostic { message: message.into(), loc: None, name_resolution: false, + diagnostic_code: None, + hint: None, + quick_fix: None, } } @@ -73,6 +83,9 @@ impl SemanticDiagnostic { message: message.into(), loc: crate::verification_output::origin_loc(origin), name_resolution: false, + diagnostic_code: None, + hint: None, + quick_fix: None, } } @@ -96,6 +109,9 @@ impl SemanticDiagnostic { }, loc: crate::verification_output::origin_loc(error.origin.as_deref()), name_resolution: error.name_resolution, + diagnostic_code: None, + hint: None, + quick_fix: None, } } @@ -108,6 +124,9 @@ impl SemanticDiagnostic { message: error.to_string(), loc: crate::verification_output::model_error_loc(error), name_resolution: error.name_resolution, + diagnostic_code: error.diagnostic_code, + hint: error.hint.as_deref().cloned(), + quick_fix: error.quick_fix.as_deref().cloned(), } } } @@ -117,7 +136,7 @@ impl SpecLoadError { /// rejected CLI selection, a whole-document shape mismatch, or a diagnostic /// whose span belongs to a different file than the one being reported on. pub fn unlocated_semantic(message: impl Into) -> Self { - Self::Semantic(SemanticDiagnostic::unlocated(message)) + Self::Semantic(Box::new(SemanticDiagnostic::unlocated(message))) } } @@ -155,9 +174,11 @@ pub fn kernel_load_error(source: &str, error: &fsl_core::CoreError) -> SpecLoadE // keeps no location; the original diagnostic keeps whatever origin the // frontend recorded. if error.message == "top-level document has not reached the kernel lowering gate" { - return SpecLoadError::Semantic(SemanticDiagnostic::unlocated("spec has no state block")); + return SpecLoadError::Semantic(Box::new(SemanticDiagnostic::unlocated( + "spec has no state block", + ))); } - SpecLoadError::Semantic(SemanticDiagnostic::from_core_error(error)) + SpecLoadError::Semantic(Box::new(SemanticDiagnostic::from_core_error(error))) } /// Render a classified spec-load failure into the public error envelope. @@ -178,6 +199,8 @@ pub fn render_spec_load_error(mut output: Map, error: &SpecLoadEr &diagnostic.message, diagnostic.loc.clone(), diagnostic.name_resolution, + diagnostic.diagnostic_code, + diagnostic.hint.as_deref(), ), } } diff --git a/rust/fslc/src/verification_output.rs b/rust/fslc/src/verification_output.rs index 16b92b19..f7dfb06d 100644 --- a/rust/fslc/src/verification_output.rs +++ b/rust/fslc/src/verification_output.rs @@ -158,6 +158,8 @@ pub fn render_semantic_error( message: &str, loc: Option, name_resolution: bool, + diagnostic_code: Option<&str>, + hint: Option<&str>, ) -> Value { let kind = diagnostic_kind(message, name_resolution); output.insert("result".to_owned(), json!("error")); @@ -166,7 +168,12 @@ pub fn render_semantic_error( if let Some(loc) = loc { output.insert("loc".to_owned(), loc); } - if message.starts_with("struct field '") && message.ends_with(" has non-scalar type") { + if let Some(code) = diagnostic_code { + output.insert("diagnostic_code".to_owned(), json!(code)); + } + if let Some(hint) = hint { + output.insert("hint".to_owned(), json!(hint)); + } else if message.starts_with("struct field '") && message.ends_with(" has non-scalar type") { output.insert( "hint".to_owned(), json!("struct fields must be a scalar (domain type, enum, Bool, Int) or nested Option around a scalar; use a separate Map for Set, Map, Seq, relation, or struct fields"), @@ -200,6 +207,8 @@ pub fn render_runtime_error( &error.message, error.span.map(fsl_syntax::Span::python_loc), false, + None, + None, ) } @@ -2244,6 +2253,8 @@ mod tests { "state variable 'x' has unsupported state type", Some(json!({"line": 3, "column": 3})), false, + None, + None, ); assert_eq!(output["result"], "error"); assert_eq!(output["kind"], "type"); @@ -2261,6 +2272,8 @@ mod tests { "struct field 'Record.nested' has non-scalar type", Some(json!({"line": 3, "column": 3})), false, + None, + None, ); assert_eq!(output["result"], "error"); assert_eq!(output["kind"], "type"); diff --git a/rust/fslc/tests/fixtures/issue_698_affine_index.fsl b/rust/fslc/tests/fixtures/issue_698_affine_index.fsl new file mode 100644 index 00000000..8c127aba --- /dev/null +++ b/rust/fslc/tests/fixtures/issue_698_affine_index.fsl @@ -0,0 +1,10 @@ +spec AffineIndex { + type Cell = 0..7 + type Off = 0..3 + const BASE = 2 + state { m: Map } + init { forall i: Cell { m[i] = false } } + action shift() { + forall c: Off { m[BASE + c] = true } + } +} diff --git a/rust/fslc/tests/fixtures/issue_698_affine_index_fixed.fsl b/rust/fslc/tests/fixtures/issue_698_affine_index_fixed.fsl new file mode 100644 index 00000000..edaca3d0 --- /dev/null +++ b/rust/fslc/tests/fixtures/issue_698_affine_index_fixed.fsl @@ -0,0 +1,10 @@ +spec AffineIndexFixed { + type Cell = 0..7 + type Off = 0..3 + const BASE = 2 + state { m: Map } + init { forall i: Cell { m[i] = false } } + action shift() { + forall k: Cell { if k >= BASE and k < BASE + 4 { m[k] = true } } + } +} diff --git a/rust/fslc/tests/fixtures/issue_698_conditional_offset.fsl b/rust/fslc/tests/fixtures/issue_698_conditional_offset.fsl new file mode 100644 index 00000000..f861d694 --- /dev/null +++ b/rust/fslc/tests/fixtures/issue_698_conditional_offset.fsl @@ -0,0 +1,9 @@ +spec CondOffset { + type Cell = 0..9 + type Off = 0..2 + state { flag: Bool, m: Map } + init { flag = false forall i: Cell { m[i] = false } } + action shift() { + forall c: Off { m[(if flag then 1 else 2) + c] = true } + } +} diff --git a/rust/fslc/tests/fixtures/issue_698_forall_constant.fsl b/rust/fslc/tests/fixtures/issue_698_forall_constant.fsl new file mode 100644 index 00000000..71789b6c --- /dev/null +++ b/rust/fslc/tests/fixtures/issue_698_forall_constant.fsl @@ -0,0 +1,8 @@ +spec ForallConstant { + type Idx = 0..3 + state { m: Map } + init { forall i: Idx { m[i] = false } } + action dup() { + forall c: Idx { m[0] = true } + } +} diff --git a/rust/fslc/tests/fixtures/issue_698_genuine_literal.fsl b/rust/fslc/tests/fixtures/issue_698_genuine_literal.fsl new file mode 100644 index 00000000..39e08db0 --- /dev/null +++ b/rust/fslc/tests/fixtures/issue_698_genuine_literal.fsl @@ -0,0 +1,9 @@ +spec GenuineLiteral { + type Idx = 0..3 + state { m: Map } + init { forall i: Idx { m[i] = false } } + action twice() { + m[0] = true + m[0] = false + } +} diff --git a/rust/fslc/tests/fixtures/issue_698_map_named_k.fsl b/rust/fslc/tests/fixtures/issue_698_map_named_k.fsl new file mode 100644 index 00000000..86d4250d --- /dev/null +++ b/rust/fslc/tests/fixtures/issue_698_map_named_k.fsl @@ -0,0 +1,10 @@ +spec MapNamedK { + type Cell = 0..7 + type Off = 0..3 + const BASE = 2 + state { k: Map } + init { forall i: Cell { k[i] = false } } + action shift() { + forall c: Off { k[BASE + c] = true } + } +} diff --git a/rust/fslc/tests/fixtures/issue_698_nonzero_lower_bound.fsl b/rust/fslc/tests/fixtures/issue_698_nonzero_lower_bound.fsl new file mode 100644 index 00000000..84077b27 --- /dev/null +++ b/rust/fslc/tests/fixtures/issue_698_nonzero_lower_bound.fsl @@ -0,0 +1,10 @@ +spec NonZeroLo { + type Cell = 0..9 + type Off = 2..5 + const BASE = 1 + state { m: Map } + init { forall i: Cell { m[i] = false } } + action shift() { + forall c: Off { m[BASE + c] = true } + } +} diff --git a/rust/fslc/tests/issue_698_distinctness_diagnostic.rs b/rust/fslc/tests/issue_698_distinctness_diagnostic.rs new file mode 100644 index 00000000..494e5ebb --- /dev/null +++ b/rust/fslc/tests/issue_698_distinctness_diagnostic.rs @@ -0,0 +1,306 @@ +// SPDX-License-Identifier: Apache-2.0 +// Copyright 2026 Ryoichi Izumita + +use std::path::Path; +use std::process::Command; + +use fsl_core::WRITE_DISTINCTNESS_UNPROVED_CODE; +use serde_json::{Value, json}; + +const FIXTURE_DIR: &str = concat!(env!("CARGO_MANIFEST_DIR"), "/tests/fixtures"); +const REPO_ROOT: &str = concat!(env!("CARGO_MANIFEST_DIR"), "/../.."); + +fn run_cli(args: &[&str]) -> (Value, i32) { + let output = Command::new(env!("CARGO_BIN_EXE_fslc")) + .args(args) + .output() + .expect("run fslc"); + let status = output.status.code().unwrap_or(-1); + let value: Value = serde_json::from_slice(&output.stdout).unwrap_or_else(|error| { + panic!( + "stdout must be JSON: status={status} stderr={} error={error}", + String::from_utf8_lossy(&output.stderr) + ) + }); + (value, status) +} + +fn shared_diagnostic(source: &str, path: &str) -> fslc_rust::source_diagnostic::SourceDiagnostic { + let resolver = fsl_core::FsResolver::new(Path::new(".")); + fslc_rust::source_diagnostic::diagnostics(source, path, &resolver) + .into_iter() + .find(|diagnostic| diagnostic.kind != "migration") + .expect("expected a semantic diagnostic") +} + +#[test] +fn genuine_literal_duplicate_keeps_legacy_duplicate_contract() { + let fixture = format!("{FIXTURE_DIR}/issue_698_genuine_literal.fsl"); + let source = std::fs::read_to_string(&fixture).expect("read fixture"); + for command in ["check", "verify"] { + let args = if command == "check" { + vec!["check", &fixture] + } else { + vec!["verify", &fixture, "--no-cache"] + }; + let (value, status) = run_cli(&args); + assert_eq!(status, 2, "{command}: {value}"); + assert_eq!(value["result"], "error", "{command}"); + assert_eq!(value["kind"], "semantics", "{command}"); + assert_eq!( + value["message"], "an action may not assign the same state location more than once", + "{command}" + ); + assert!(value.get("diagnostic_code").is_none(), "{command}: {value}"); + assert!(value.get("hint").is_none(), "{command}: {value}"); + assert_eq!(value["loc"], json!({"line": 7, "column": 5}), "{command}"); + } + let shared = shared_diagnostic(&source, &fixture); + assert_eq!(shared.code, "FSL-SEMANTIC"); + assert_eq!( + shared.message, + "an action may not assign the same state location more than once" + ); + assert_eq!(shared.span.start.line, 7); + assert_eq!(shared.span.start.column, 5); + assert!(shared.hint.is_none()); + assert!(shared.quick_fix.is_none()); +} + +#[test] +fn forall_constant_duplicate_keeps_legacy_duplicate_contract() { + let fixture = format!("{FIXTURE_DIR}/issue_698_forall_constant.fsl"); + let source = std::fs::read_to_string(&fixture).expect("read fixture"); + let (value, status) = run_cli(&["check", &fixture]); + assert_eq!(status, 2, "{value}"); + assert_eq!( + value["message"], + "an action may not assign the same state location more than once" + ); + assert!(value.get("diagnostic_code").is_none(), "{value}"); + assert_eq!(value["loc"], json!({"line": 6, "column": 21})); + let shared = shared_diagnostic(&source, &fixture); + assert_eq!(shared.code, "FSL-SEMANTIC"); + assert_eq!(shared.span.start.line, 6); + assert_eq!(shared.span.start.column, 21); +} + +#[test] +fn affine_index_reports_distinctness_unproved_contract() { + let fixture = format!("{FIXTURE_DIR}/issue_698_affine_index.fsl"); + let source = std::fs::read_to_string(&fixture).expect("read fixture"); + let expected_hint = "forall k: Cell { if k >= BASE and k < BASE + 4 { m[k] = true } }"; + for command in ["check", "verify"] { + let args = if command == "check" { + vec!["check", &fixture] + } else { + vec!["verify", &fixture, "--no-cache"] + }; + let (value, status) = run_cli(&args); + assert_eq!(status, 2, "{command}: {value}"); + assert_eq!(value["result"], "error", "{command}"); + assert_eq!(value["kind"], "semantics", "{command}"); + assert_eq!( + value["message"], "cannot prove write-index distinctness across forall iterations", + "{command}" + ); + assert_eq!( + value["diagnostic_code"], WRITE_DISTINCTNESS_UNPROVED_CODE, + "{command}" + ); + assert_eq!(value["hint"], expected_hint, "{command}"); + assert_eq!(value["loc"], json!({"line": 8, "column": 21}), "{command}"); + } + let shared = shared_diagnostic(&source, &fixture); + assert_eq!(shared.code, WRITE_DISTINCTNESS_UNPROVED_CODE); + assert_eq!(shared.span.start.line, 8); + assert_eq!(shared.span.start.column, 21); + assert_eq!(shared.hint.as_deref(), Some(expected_hint)); + assert_eq!( + shared + .quick_fix + .as_ref() + .map(|edit| edit.replacement.as_str()), + Some(expected_hint) + ); +} + +#[test] +fn hint_positive_control_checks_cleanly() { + let fixed = format!("{FIXTURE_DIR}/issue_698_affine_index_fixed.fsl"); + let (value, status) = run_cli(&["check", &fixed]); + assert_eq!(status, 0, "{value}"); + assert_eq!(value["result"], "ok"); +} + +fn build_model_from_source(source: &str) -> Result { + let kernel = + fsl_core::parse_kernel_source(source, &fsl_core::FsResolver::new(".")).expect("parse"); + fsl_core::build_model(kernel) +} + +#[test] +fn non_affine_index_stays_rejected_without_actionable_hint() { + let source = r"spec NonAffine { + type Cell = 0..7 + type Off = 0..3 + state { m: Map } + init { forall i: Cell { m[i] = false } } + action shift() { + forall c: Off { m[c + c] = true } + } +}"; + let error = build_model_from_source(source).expect_err("non-affine index must stay rejected"); + assert_eq!( + error.message, + "cannot prove write-index distinctness across forall iterations" + ); + assert_eq!( + error.diagnostic_code, + Some(WRITE_DISTINCTNESS_UNPROVED_CODE) + ); + assert!(error.hint.is_none()); + assert!(error.quick_fix.is_none()); +} + +#[test] +fn rhs_binder_use_blocks_machine_hint() { + let source = r"spec RhsBinder { + type Cell = 0..7 + type Off = 0..3 + const BASE = 2 + state { m: Map } + init { forall i: Cell { m[i] = false } } + action shift() { + forall c: Off { m[BASE + c] = c } + } +}"; + let error = build_model_from_source(source) + .expect_err("binder-dependent RHS must not get a machine hint"); + assert_eq!( + error.diagnostic_code, + Some(WRITE_DISTINCTNESS_UNPROVED_CODE) + ); + assert!(error.hint.is_none()); + assert!(error.quick_fix.is_none()); +} + +#[test] +fn docs_distinguish_proven_duplicate_from_conservative_rejection() { + let english = + std::fs::read_to_string(format!("{REPO_ROOT}/docs/LANGUAGE.md")).expect("read LANGUAGE.md"); + let japanese = std::fs::read_to_string(format!("{REPO_ROOT}/docs/LANGUAGE.ja.md")) + .expect("read LANGUAGE.ja.md"); + let syntax = std::fs::read_to_string(format!("{REPO_ROOT}/skills/fsl/references/syntax.md")) + .expect("read skills/fsl/references/syntax.md"); + for doc in [&english, &japanese, &syntax] { + assert!(doc.contains("FSL-SEMANTIC-WRITE-DISTINCTNESS-UNPROVED")); + assert!(doc.contains("cannot prove write-index distinctness across forall iterations")); + assert!( + doc.contains("same state location more than once") + || doc.contains("legacy duplicate-write") + ); + } +} + +/// REJECTING CONTROL for the independent review's counterexample: a binder +/// whose domain does not start at zero. Emitting `offset .. offset + width` +/// silently shifts the whole interval -- `Off = 2..5` written as `BASE + c` +/// covers `BASE+2 ..= BASE+5`, not `BASE ..= BASE+3`. The hint must name the +/// set the original statement writes, or it is a wrong repair dressed as an +/// actionable one. +#[test] +fn nonzero_lower_bound_hint_names_the_written_interval() { + let path = format!("{FIXTURE_DIR}/issue_698_nonzero_lower_bound.fsl"); + let (output, status) = run_cli(&["check", &path]); + assert_eq!(status, 2, "{output:#}"); + assert_eq!( + output["diagnostic_code"], "FSL-SEMANTIC-WRITE-DISTINCTNESS-UNPROVED", + "{output:#}" + ); + let hint = output["hint"].as_str().expect("hint"); + // Off = 2..5 with BASE + c writes BASE+2 ..= BASE+5, so the exclusive upper + // bound is BASE + 6. + assert!( + hint.contains("k >= BASE + 2"), + "lower bound must carry the binder's own lower bound: {hint}" + ); + assert!( + hint.contains("k < BASE + 6"), + "exclusive upper bound must be offset + hi + 1: {hint}" + ); +} + +/// REJECTING CONTROL: the replacement introduces `k`, so an RHS that already +/// refers to a `k` from an enclosing scope would be captured by it. The +/// classification and code must still arrive; only the machine-applicable +/// repair is withheld. +#[test] +fn an_rhs_that_names_k_withholds_the_hint() { + let source = r" +spec CapturesK { + type Cell = 0..7 + type Off = 0..3 + const BASE = 2 + state { m: Map } + init { forall i: Cell { m[i] = 0 } } + action shift(k: Cell) { + forall c: Off { m[BASE + c] = k } + } +} +"; + let error = build_model_from_source(source).expect_err("distinctness is unproved here"); + assert_eq!( + error.diagnostic_code, + Some("FSL-SEMANTIC-WRITE-DISTINCTNESS-UNPROVED"), + "{error:?}" + ); + assert!( + error.hint.is_none(), + "a hint that rebinds a name the RHS already uses must be withheld: {error:?}" + ); +} + +/// REJECTING CONTROL for the independent review's second counterexample: the +/// state map itself is named `k`. The replacement binder shadows it, so the +/// rewritten `k[k] = ...` resolves its root to the scalar binder and fails to +/// check. A repair that does not check is worse than no repair, so the hint is +/// withheld while the classification, code and location still arrive. +#[test] +fn a_state_map_named_k_withholds_the_hint() { + let path = format!("{FIXTURE_DIR}/issue_698_map_named_k.fsl"); + let (output, status) = run_cli(&["check", &path]); + assert_eq!(status, 2, "{output:#}"); + assert_eq!( + output["diagnostic_code"], "FSL-SEMANTIC-WRITE-DISTINCTNESS-UNPROVED", + "{output:#}" + ); + assert!( + output.get("hint").is_none() || output["hint"].is_null(), + "a rewrite whose binder shadows the written map must not be offered: {output:#}" + ); +} + +/// REJECTING CONTROL for the independent review's counterexample: the affine +/// offset is a conditional. `expr_text` does not parenthesize one, so splicing +/// it raw into `k >= ` and `k < + n` reassociates the +/// comparison. The emitted hint must keep the offset bracketed. +#[test] +fn a_conditional_offset_is_parenthesised_in_the_hint() { + let path = format!("{FIXTURE_DIR}/issue_698_conditional_offset.fsl"); + let (output, status) = run_cli(&["check", &path]); + assert_eq!(status, 2, "{output:#}"); + assert_eq!( + output["diagnostic_code"], "FSL-SEMANTIC-WRITE-DISTINCTNESS-UNPROVED", + "{output:#}" + ); + let hint = output["hint"].as_str().expect("hint"); + assert!( + hint.contains("k >= (if flag then 1 else 2)"), + "the offset must be bracketed where it is compared: {hint}" + ); + assert!( + hint.contains("k < (if flag then 1 else 2) + 3"), + "the offset must be bracketed where it is added to: {hint}" + ); +} diff --git a/rust/fslc/tests/lsp_diagnostic_contract.rs b/rust/fslc/tests/lsp_diagnostic_contract.rs index 97a46050..80021f8d 100644 --- a/rust/fslc/tests/lsp_diagnostic_contract.rs +++ b/rust/fslc/tests/lsp_diagnostic_contract.rs @@ -78,6 +78,39 @@ fn cli_and_lsp_source_diagnostics_share_identity_without_changing_cli_envelopes( std::fs::remove_dir_all(directory).expect("remove diagnostic fixture directory"); } +#[test] +fn distinctness_unproved_diagnostic_shares_cli_and_lsp_identity() { + let fixture = format!( + "{}/tests/fixtures/issue_698_affine_index.fsl", + env!("CARGO_MANIFEST_DIR") + ); + let source = std::fs::read_to_string(&fixture).expect("read fixture"); + let output = Command::new(env!("CARGO_BIN_EXE_fslc")) + .args(["check", &fixture]) + .output() + .expect("run native check"); + assert_eq!(output.status.code(), Some(2)); + let cli: Value = serde_json::from_slice(&output.stdout).expect("parse CLI envelope"); + let shared = fslc_rust::source_diagnostic::diagnostics( + &source, + &fixture, + &fsl_core::FsResolver::new(Path::new(".")), + ) + .into_iter() + .find(|diagnostic| diagnostic.kind != "migration") + .expect("shared source diagnostic"); + assert_eq!(cli["kind"], shared.kind); + assert_eq!(cli["message"], shared.message); + assert_eq!( + cli["diagnostic_code"], + fsl_core::WRITE_DISTINCTNESS_UNPROVED_CODE + ); + assert_eq!(shared.code, fsl_core::WRITE_DISTINCTNESS_UNPROVED_CODE); + assert_eq!(cli["loc"], shared.span.python_loc()); + assert_eq!(cli["hint"].as_str(), shared.hint.as_deref()); + assert!(shared.quick_fix.is_some()); +} + #[test] fn nested_option_payload_diagnostics_have_cli_lsp_identity() { const STATE_HINT: &str = "state types allow scalars, nested Option around a scalar, structs with those fields, Map, Set, Seq, and bounded-scalar relations; Option cannot wrap a collection or struct"; diff --git a/skills/fsl/SKILL.md b/skills/fsl/SKILL.md index 68d124de..6039c57d 100644 --- a/skills/fsl/SKILL.md +++ b/skills/fsl/SKILL.md @@ -272,7 +272,11 @@ domain truth. See [layers](references/layers.md), "Authoring specs as readable d - **Do not hand-write "non-negative"-style invariants** → `type Qty = 0..N` checks them automatically. - A **double assignment on the same execution path is an error**. Assigning to the - same variable after an if as inside a branch is also an error. + same variable after an if as inside a branch is also an error. **Proven duplicate + writes** keep the legacy duplicate-write message; **conservative rejections** for + unproved `forall` index distinctness report + `FSL-SEMANTIC-WRITE-DISTINCTNESS-UNPROVED` with `loc` and a safe `hint` when one + exists (acceptance is not widened). - Updates to Set/Seq are **re-assignments**: `s = s.add(x)`, `q = q.pop()`. - Seq `pop/head/at` and the divisor of `/` `%` **must always be guarded** (requires or if). Forgetting is detected as partial_op. diff --git a/skills/fsl/references/syntax.md b/skills/fsl/references/syntax.md index 9ef9102f..45a4c6d5 100644 --- a/skills/fsl/references/syntax.md +++ b/skills/fsl/references/syntax.md @@ -828,6 +828,13 @@ could read (#570). No other word is reserved — `count`, `sum`, `stage`, `in`, variable/field on the same path. then/else are separate paths (assigning in both is allowed). Assigning to the same variable **after an if** as inside a branch is also an error. + **Proven duplicate writes** (for example `m[0]` twice or `forall c { m[0] = ... }`) + keep the legacy duplicate-write message. **Conservative rejections** for unproved + `forall` index distinctness (for example `forall c { m[BASE + c] = ... }`) report + `cannot prove write-index distinctness across forall iterations` with + `FSL-SEMANTIC-WRITE-DISTINCTNESS-UNPROVED`, `loc`, and a safe `hint` when one + exists. Acceptance is not widened: the checked Kernel model still rejects before + any verifier backend runs. For `Map` values, the path includes the field: `m[k].f1 = ...` and `m[k].f2 = ...` in one action are allowed independent field writes (`check` and `verify --depth 1` succeed in the repro). Repeating the same