From ca3085f82358327ecb432151e553e4324f7def53 Mon Sep 17 00:00:00 2001 From: Denis Efremov Date: Sun, 14 Jun 2026 20:35:00 +0400 Subject: [PATCH 1/4] feat(wd): port Rodin's well-definedness calculus Add the calculus eventb-checker borrows from Rodin to decide whether a formula is well-defined, as a self-contained rossi-build module: - computer: the L-operator deriving a formula's WD lemma - builder: FormulaBuilder smart constructors keeping the lemma in normal form - improve: the WDImprover simplifier dropping trivial/subsumed conjuncts - normal: binder flattening and capture-aware binder renaming - render: a Formula#toString renderer, byte-identical to Rodin The module is the calculus only and is not yet wired to any checker; its inline unit tests exercise each layer directly. --- crates/rossi-build/src/lib.rs | 1 + crates/rossi-build/src/wd/builder.rs | 258 +++++++++ crates/rossi-build/src/wd/computer.rs | 454 +++++++++++++++ crates/rossi-build/src/wd/improve.rs | 424 ++++++++++++++ crates/rossi-build/src/wd/mod.rs | 19 + crates/rossi-build/src/wd/normal.rs | 800 ++++++++++++++++++++++++++ crates/rossi-build/src/wd/render.rs | 694 ++++++++++++++++++++++ 7 files changed, 2650 insertions(+) create mode 100644 crates/rossi-build/src/wd/builder.rs create mode 100644 crates/rossi-build/src/wd/computer.rs create mode 100644 crates/rossi-build/src/wd/improve.rs create mode 100644 crates/rossi-build/src/wd/mod.rs create mode 100644 crates/rossi-build/src/wd/normal.rs create mode 100644 crates/rossi-build/src/wd/render.rs diff --git a/crates/rossi-build/src/lib.rs b/crates/rossi-build/src/lib.rs index 8740585..69c20c7 100644 --- a/crates/rossi-build/src/lib.rs +++ b/crates/rossi-build/src/lib.rs @@ -38,6 +38,7 @@ pub mod sc_model; pub mod sc_view; pub mod type_env; pub mod types; +pub mod wd; pub mod wellformed; pub mod xml_out; diff --git a/crates/rossi-build/src/wd/builder.rs b/crates/rossi-build/src/wd/builder.rs new file mode 100644 index 0000000..e0a5614 --- /dev/null +++ b/crates/rossi-build/src/wd/builder.rs @@ -0,0 +1,258 @@ +//! Smart constructors for WD lemmas — port of rodin-ast's +//! `org.eventb.internal.core.ast.wd.FormulaBuilder`. +//! +//! `Predicate::True` plays the role of Rodin's `BTRUE` literal: it is the +//! neutral element the constructors simplify away, and a final result of +//! `Predicate::True` means "no WD condition". +//! +//! The conjunction constructors build left-associated binary chains; +//! Rodin builds n-ary `LAND` nodes and `flatten()`s at the end, which is +//! indistinguishable after rendering and improver decomposition (both +//! flatten same-operator chains). + +use rossi::ast::expression::{BinaryOp, UnaryOp}; +use rossi::ast::predicate::{ComparisonOp, LogicalOp, Quantifier}; +use rossi::{Expression, Predicate, TypedIdentifier}; + +use crate::normalize::type_to_expression; +use crate::types::Type; + +/// `left ∧ right`, with `⊤` as the neutral element. +pub fn land2(left: Predicate, right: Predicate) -> Predicate { + if left == Predicate::True { + return right; + } + if right == Predicate::True { + return left; + } + Predicate::logical(LogicalOp::And, left, right) +} + +/// n-ary conjunction: filters `⊤` conjuncts, then chains the rest. +pub fn land(children: Vec) -> Predicate { + let mut iter = children.into_iter().filter(|c| *c != Predicate::True); + let Some(first) = iter.next() else { + return Predicate::True; + }; + iter.fold(first, |acc, c| Predicate::logical(LogicalOp::And, acc, c)) +} + +/// `left ⇒ right` with Rodin's simplifications: +/// - `⊤ ⇒ r` and `l ⇒ ⊤` collapse to `r` / `⊤`; +/// - nested implications merge their antecedents: +/// `l ⇒ (a ⇒ b)` becomes `l ∧ a ⇒ b`; +/// - `l ⇒ l` collapses to `⊤`. +pub fn limp(left: Predicate, right: Predicate) -> Predicate { + if left == Predicate::True || right == Predicate::True { + return right; + } + if let Predicate::Logical { + op: LogicalOp::Implies, + left: inner_left, + right: inner_right, + } = right + { + return limp(land2(left, *inner_left), *inner_right); + } + if left == right { + return Predicate::True; + } + Predicate::logical(LogicalOp::Implies, left, right) +} + +/// `left ∨ right`; `⊤` absorbs the disjunction. +pub fn lor2(left: Predicate, right: Predicate) -> Predicate { + if left == Predicate::True { + return left; + } + if right == Predicate::True { + return right; + } + Predicate::logical(LogicalOp::Or, left, right) +} + +/// `∀decls·pred`, skipped entirely when the body is `⊤`. +pub fn forall(decls: Vec, pred: Predicate) -> Predicate { + if pred == Predicate::True { + return pred; + } + Predicate::quantified(Quantifier::ForAll, decls, pred) +} + +/// `∃decls·pred`, skipped entirely when the body is `⊤`. +pub fn exists(decls: Vec, pred: Predicate) -> Predicate { + if pred == Predicate::True { + return pred; + } + Predicate::quantified(Quantifier::Exists, decls, pred) +} + +/// `expr ≠ 0` (divisor of `÷`). +pub fn not_zero(expr: Expression) -> Predicate { + Predicate::comparison(ComparisonOp::NotEqual, expr, Expression::Integer(0)) +} + +/// `0 ≤ expr`. +pub fn non_negative(expr: Expression) -> Predicate { + Predicate::comparison(ComparisonOp::LessEqual, Expression::Integer(0), expr) +} + +/// `0 < expr` (divisor of `mod`). +pub fn positive(expr: Expression) -> Predicate { + Predicate::comparison(ComparisonOp::LessThan, Expression::Integer(0), expr) +} + +/// `finite(expr)` (operand of `card`). +pub fn finite(expr: Expression) -> Predicate { + Predicate::BuiltinApplication { + predicate: rossi::ast::predicate::BuiltinPredicate::Finite, + arguments: vec![expr], + } +} + +/// `expr ≠ ∅`. Rodin types the empty set; the type never shows in +/// `toString` output, so the bare `∅` is byte-identical. +pub fn not_empty(expr: Expression) -> Predicate { + Predicate::comparison(ComparisonOp::NotEqual, expr, Expression::EmptySet) +} + +/// `arg ∈ dom(fun)`. +pub fn in_domain(fun: Expression, arg: Expression) -> Predicate { + let dom = Expression::Unary { + op: UnaryOp::Domain, + operand: Box::new(fun), + }; + Predicate::comparison(ComparisonOp::In, arg, dom) +} + +/// `fun ∈ src ⇸ trg`, where `src`/`trg` come from `fun`'s relational +/// type. Returns `None` when the type is not a relation (ill-typed +/// input the SC nevertheless kept). +pub fn partial(fun: Expression, fun_type: &Type) -> Option { + let Type::PowerSet(pair) = fun_type else { + return None; + }; + let Type::Product(src, trg) = pair.as_ref() else { + return None; + }; + let pfun = Expression::binary( + BinaryOp::PartialFunction, + type_to_expression(src), + type_to_expression(trg), + ); + Some(Predicate::comparison(ComparisonOp::In, fun, pfun)) +} + +/// Boundedness condition for `min` (`lower = true`) / `max`: +/// `∃b·∀x·x∈set ⇒ b ≤ x` (resp. `b ≥ x`). +/// +/// Rodin builds this with fresh De Bruijn identifiers it *names* `b` and +/// `x` only at `toString`, renaming on collision. The `$`-prefixed +/// placeholders reproduce that: `$` cannot occur in an Event-B +/// identifier, so the synthesized binders can never capture names free +/// in `set`; [`super::normal::resolve_binders`] later picks the display +/// names (`b`/`x`, suffixed when taken). +pub fn bounded(set: Expression, lower: bool) -> Predicate { + let op = if lower { + ComparisonOp::LessEqual + } else { + ComparisonOp::GreaterEqual + }; + let rel = Predicate::comparison( + op, + Expression::identifier("$b"), + Expression::identifier("$x"), + ); + let x_in_set = Predicate::comparison(ComparisonOp::In, Expression::identifier("$x"), set); + // Rodin assembles this implication directly, bypassing the `limp` + // simplifications. + let body = Predicate::logical(LogicalOp::Implies, x_in_set, rel); + Predicate::quantified( + Quantifier::Exists, + vec![TypedIdentifier::untyped("$b".into())], + Predicate::quantified( + Quantifier::ForAll, + vec![TypedIdentifier::untyped("$x".into())], + body, + ), + ) +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::wd::render::render_predicate; + use rossi::parse_predicate_str; + + fn p(src: &str) -> Predicate { + parse_predicate_str(src).unwrap() + } + + #[test] + fn land_is_true_neutral() { + assert_eq!(land2(Predicate::True, p("x∈S")), p("x∈S")); + assert_eq!(land2(p("x∈S"), Predicate::True), p("x∈S")); + assert_eq!(land(vec![]), Predicate::True); + assert_eq!( + land(vec![Predicate::True, p("x∈S"), Predicate::True]), + p("x∈S") + ); + } + + #[test] + fn limp_merges_nested_antecedents() { + // l ⇒ (a ⇒ b) ⇝ l ∧ a ⇒ b + let merged = limp(p("l∈S"), limp(p("a∈S"), p("b∈S"))); + assert_eq!(render_predicate(&merged), "l∈S∧a∈S⇒b∈S"); + } + + #[test] + fn limp_collapses_identity_and_true() { + assert_eq!(limp(p("x∈S"), p("x∈S")), Predicate::True); + assert_eq!(limp(p("x∈S"), Predicate::True), Predicate::True); + assert_eq!(limp(Predicate::True, p("x∈S")), p("x∈S")); + } + + #[test] + fn lor_absorbs_true() { + assert_eq!(lor2(Predicate::True, p("x∈S")), Predicate::True); + assert_eq!(lor2(p("x∈S"), Predicate::True), Predicate::True); + } + + #[test] + fn forall_skips_true_body() { + assert_eq!( + forall(vec![TypedIdentifier::untyped("x".into())], Predicate::True), + Predicate::True + ); + } + + #[test] + fn bounded_renders_like_rodin() { + use crate::wd::normal::resolve_binders; + let set = rossi::parse_expression_str("s").unwrap(); + assert_eq!( + render_predicate(&resolve_binders(&bounded(set.clone(), true))), + "∃b·∀x·x∈s⇒b≤x" + ); + assert_eq!( + render_predicate(&resolve_binders(&bounded(set, false))), + "∃b·∀x·x∈s⇒b≥x" + ); + } + + #[test] + fn partial_renders_function_space_from_type() { + let f = rossi::parse_expression_str("f").unwrap(); + let ty = Type::pow(Type::Product( + Box::new(Type::GivenSet("S".into())), + Box::new(Type::pow(Type::Integer)), + )); + let pred = partial(f, &ty).unwrap(); + assert_eq!(render_predicate(&pred), "f∈S ⇸ ℙ(ℤ)"); + assert_eq!( + partial(rossi::parse_expression_str("g").unwrap(), &Type::Integer), + None + ); + } +} diff --git a/crates/rossi-build/src/wd/computer.rs b/crates/rossi-build/src/wd/computer.rs new file mode 100644 index 0000000..c0fe021 --- /dev/null +++ b/crates/rossi-build/src/wd/computer.rs @@ -0,0 +1,454 @@ +//! The WD L-operator — port of rodin-ast's +//! `org.eventb.internal.core.ast.wd.WDComputer`. +//! +//! Computes the well-definedness lemma of a predicate, expression, or +//! assignment over the raw (source-form) AST. Runs on the *unenriched* +//! formula because the lemma embeds verbatim fragments of the original — +//! Rodin's `toString` preserves the source's comprehension forms, so +//! rendering the SC-lowered AST would diverge from the oracle. +//! +//! Types are needed in exactly one rule (`f(x)` ⇒ `f ∈ src ⇸ trg`): the +//! computer carries a scoped [`TypeEnv`] seeded with the component +//! environment and extended at each binder using the same inference the +//! enrichment pass uses. When a function's type cannot be resolved, the +//! whole formula is flagged ([`WdComputer::failed`]) and the caller skips +//! its finding rather than emit a partial lemma. + +use rossi::ast::expression::{BinaryOp, BuiltinFunction}; +use rossi::ast::predicate::LogicalOp; +use rossi::{Action, Expression, Predicate, TypedIdentifier}; + +use crate::infer::{collect_binder_types, parse_type_from_expression, type_of_expression}; +use crate::type_env::TypeEnv; +use crate::wd::builder as fb; + +/// One WD computation over a single formula. +pub struct WdComputer { + env: TypeEnv, + /// Set when a sub-lemma could not be built (untypeable function in a + /// function application). The formula's finding must be skipped. + pub failed: Option, +} + +impl WdComputer { + pub fn new(env: TypeEnv) -> Self { + Self { env, failed: None } + } + + /// Clear the per-formula state so one computer can serve every formula + /// sharing a base environment. `scoped` always pops the binder scope it + /// pushes, so the env is already back at its base after a computation — + /// only [`Self::failed`] needs resetting. + pub fn reset(&mut self) { + self.failed = None; + } + + // ----------------------------------------------------------------- + // Predicates + // ----------------------------------------------------------------- + + pub fn wd_predicate(&mut self, p: &Predicate) -> Predicate { + match p { + Predicate::True | Predicate::False => Predicate::True, + Predicate::Comparison { left, right, .. } => { + fb::land2(self.wd_expression(left), self.wd_expression(right)) + } + Predicate::Not(inner) => self.wd_predicate(inner), + Predicate::Logical { + op: op @ (LogicalOp::And | LogicalOp::Or), + .. + } => { + let mut children: Vec<&Predicate> = Vec::new(); + flatten_chain(p, *op, &mut children); + if *op == LogicalOp::And { + self.land_wd(&children) + } else { + self.lor_wd(&children) + } + } + Predicate::Logical { + op: LogicalOp::Implies, + left, + right, + } => { + let wd_left = self.wd_predicate(left); + let wd_right = self.wd_predicate(right); + fb::land2(wd_left, fb::limp((**left).clone(), wd_right)) + } + Predicate::Logical { + op: LogicalOp::Equivalent, + left, + right, + } => fb::land2(self.wd_predicate(left), self.wd_predicate(right)), + Predicate::Quantified { + identifiers, + predicate, + .. + } => { + // Both ∀ and ∃ produce a universally quantified lemma. + let body = self.scoped(identifiers, Some(predicate), |s| s.wd_predicate(predicate)); + fb::forall(untyped(identifiers), body) + } + Predicate::Application { arguments, .. } + | Predicate::BuiltinApplication { arguments, .. } => self.wd_expressions(arguments), + } + } + + /// `landWD` — right-to-left fold over the flattened conjunction: + /// each conjunct's WD is asserted under the hypothesis of the + /// conjuncts before it. + fn land_wd(&mut self, children: &[&Predicate]) -> Predicate { + let mut result = Predicate::True; + for child in children.iter().rev() { + let wd = self.wd_predicate(child); + result = fb::land2(wd, fb::limp((*child).clone(), result)); + } + result + } + + /// `lorWD` — dual of [`Self::land_wd`] with disjunction. + fn lor_wd(&mut self, children: &[&Predicate]) -> Predicate { + let mut result = Predicate::True; + for child in children.iter().rev() { + let wd = self.wd_predicate(child); + result = fb::land2(wd, fb::lor2((*child).clone(), result)); + } + result + } + + // ----------------------------------------------------------------- + // Expressions + // ----------------------------------------------------------------- + + pub fn wd_expression(&mut self, e: &Expression) -> Predicate { + match e { + Expression::Integer(_) + | Expression::Identifier(_) + | Expression::True + | Expression::False + | Expression::EmptySet + | Expression::Naturals + | Expression::Naturals1 + | Expression::Integers + | Expression::BoolType + | Expression::StringLiteral(_) => Predicate::True, + + Expression::SetEnumeration(items) => self.wd_expressions(items), + + Expression::Binary { op, left, right } => { + let wd_l = self.wd_expression(left); + let wd_r = self.wd_expression(right); + let extra = match op { + BinaryOp::Divide => fb::not_zero((**right).clone()), + BinaryOp::Modulo => fb::land2( + fb::non_negative((**left).clone()), + fb::positive((**right).clone()), + ), + BinaryOp::Exponent => fb::land2( + fb::non_negative((**left).clone()), + fb::non_negative((**right).clone()), + ), + _ => Predicate::True, + }; + fb::land(vec![wd_l, wd_r, extra]) + } + + Expression::Unary { operand, .. } => self.wd_expression(operand), + + Expression::BuiltinApplication { + function, + arguments, + } => { + let wd_children = self.wd_expressions(arguments); + let extra = match (function, arguments.as_slice()) { + (BuiltinFunction::Card, [arg]) => fb::finite(arg.clone()), + (BuiltinFunction::Min, [arg]) => { + fb::land2(fb::not_empty(arg.clone()), fb::bounded(arg.clone(), true)) + } + (BuiltinFunction::Max, [arg]) => { + fb::land2(fb::not_empty(arg.clone()), fb::bounded(arg.clone(), false)) + } + (BuiltinFunction::Inter, [arg]) => fb::not_empty(arg.clone()), + _ => Predicate::True, + }; + fb::land2(wd_children, extra) + } + + Expression::FunctionApplication { + function, + arguments, + } => { + let mut parts = vec![self.wd_expression(function)]; + parts.push(self.wd_expressions(arguments)); + if !self.is_builtin_total(function) { + // A multi-argument application `f(a, b)` denotes + // application to the maplet tuple `a ↦ b`. + let Some(arg) = (!arguments.is_empty()) + .then(|| crate::ast_util::left_assoc_maplet(arguments)) + else { + self.fail("function application without argument"); + return Predicate::True; + }; + let domain = fb::in_domain((**function).clone(), arg); + match type_of_expression(&self.env, function) + .and_then(|ty| fb::partial((**function).clone(), &ty)) + { + Some(partial) => parts.push(fb::land2(domain, partial)), + None => { + self.fail("cannot type function in application"); + return Predicate::True; + } + } + } + fb::land(parts) + } + + Expression::RelationalImage { relation, set } => { + fb::land2(self.wd_expression(relation), self.wd_expression(set)) + } + + Expression::SetComprehension { + identifiers, + predicate, + expression, + } => { + self.comprehension_wd(identifiers.clone(), predicate, expression.as_deref(), false) + } + + Expression::SetBuilder { + member_expression, + predicate, + } => { + // Rodin's implicit comprehension `{E ∣ P}` binds every + // identifier occurring in E. + let mut names: Vec<&str> = Vec::new(); + crate::infer::collect_free_identifiers(member_expression, &mut names); + let mut decls: Vec = Vec::new(); + for n in names { + if decls.iter().all(|d| d.name != n) { + decls.push(TypedIdentifier::untyped(n.to_string())); + } + } + self.comprehension_wd(decls, predicate, Some(member_expression), false) + } + + Expression::QuantifiedUnion { + identifiers, + predicate, + expression, + } => self.comprehension_wd(identifiers.clone(), predicate, Some(expression), false), + + Expression::QuantifiedInter { + identifiers, + predicate, + expression, + } => self.comprehension_wd(identifiers.clone(), predicate, Some(expression), true), + + Expression::Lambda { + pattern, + predicate, + expression, + } => { + let decls: Vec = pattern + .identifiers() + .into_iter() + .map(|n| TypedIdentifier::untyped(n.to_string())) + .collect(); + self.comprehension_wd(decls, predicate, Some(expression), false) + } + + Expression::Bool(p) => self.wd_predicate(p), + + Expression::IfThenElse { + condition, + then_expr, + else_expr, + } => { + // ProB extension, absent from Rodin models. + let c = self.wd_predicate(condition); + let t = self.wd_expression(then_expr); + let f = self.wd_expression(else_expr); + fb::land(vec![c, t, f]) + } + } + } + + /// Shared rule for CSET / λ / ⋃ / ⋂: + /// `∀decls·wd(P) ∧ (P ⇒ wd(E))`, plus `∃decls·P` for ⋂. + fn comprehension_wd( + &mut self, + decls: Vec, + predicate: &Predicate, + expression: Option<&Expression>, + require_nonempty: bool, + ) -> Predicate { + let body = self.scoped(&decls, Some(predicate), |s| { + let wd_p = s.wd_predicate(predicate); + let wd_e = expression.map_or(Predicate::True, |e| s.wd_expression(e)); + fb::land2(wd_p, fb::limp(predicate.clone(), wd_e)) + }); + let children_wd = fb::forall(untyped(&decls), body); + let local_wd = if require_nonempty { + fb::exists(untyped(&decls), predicate.clone()) + } else { + Predicate::True + }; + fb::land2(children_wd, local_wd) + } + + // ----------------------------------------------------------------- + // Assignments + // ----------------------------------------------------------------- + + pub fn wd_action(&mut self, a: &Action) -> Predicate { + match a { + Action::Skip => Predicate::True, + Action::Assignment { expressions, .. } => self.wd_expressions(expressions), + Action::BecomesIn { set, .. } => self.wd_expression(set), + Action::BecomesSuchThat { + variables, + predicate, + } => { + // ∀x'·wd(P) — the primed identifiers are bound, typed + // like their unprimed counterparts. + let decls: Vec = variables + .iter() + .map(|v| TypedIdentifier::untyped(format!("{v}'"))) + .collect(); + self.env.push_scope(); + for v in variables { + if let Some(ty) = self.env.get(v).cloned() { + self.env.insert(format!("{v}'"), ty); + } + } + let body = self.wd_predicate(predicate); + self.env.pop_scope(); + fb::forall(decls, body) + } + Action::FunctionOverride { + arguments, + expression, + .. + } => { + // `f(x) ≔ E` is sugar for `f ≔ f {x ↦ E}`: the WD is + // that of the desugared right-hand side — children only, + // no domain condition. + let wd_args = self.wd_expressions(arguments); + fb::land2(wd_args, self.wd_expression(expression)) + } + } + } + + // ----------------------------------------------------------------- + // Helpers + // ----------------------------------------------------------------- + + fn wd_expressions(&mut self, items: &[Expression]) -> Predicate { + let parts: Vec = items.iter().map(|e| self.wd_expression(e)).collect(); + fb::land(parts) + } + + /// Rodin skips the domain condition for the built-in total functions + /// (`KPRED`, `KSUCC`, and the generic `id`/`prj1`/`prj2`). These are + /// reserved identifiers, so they always denote the built-in — the same + /// shared membership set ([`rossi::builtins::is_reserved_relational_atom`]) + /// that [`crate::infer`]'s `reserved_atom` consults to type them ahead of + /// the environment, keeping the two passes in agreement by construction. + fn is_builtin_total(&self, function: &Expression) -> bool { + match function { + Expression::Identifier(name) => rossi::builtins::is_reserved_relational_atom(name), + _ => false, + } + } + + /// Push a scope typing `decls` (explicit `x⦂T` annotation first, + /// otherwise inferred from the typing shapes of `typing_pred` — the + /// same source the enrichment pass uses), run `body`, pop. + fn scoped( + &mut self, + decls: &[TypedIdentifier], + typing_pred: Option<&Predicate>, + body: F, + ) -> Predicate + where + F: FnOnce(&mut Self) -> Predicate, + { + self.env.push_scope(); + let names: Vec<&str> = decls.iter().map(|d| d.name.as_str()).collect(); + let mut inferred = std::collections::BTreeMap::new(); + if let Some(pred) = typing_pred { + collect_binder_types(&self.env, pred, &names, &mut inferred); + } + for decl in decls { + let ty = decl + .type_expr + .as_deref() + .and_then(parse_type_from_expression) + .or_else(|| inferred.get(&decl.name).cloned()); + match ty { + // Type known: shadow the outer binding with it. + Some(ty) => self.env.insert(decl.name.clone(), ty), + // Type unknown: still shadow the outer binding, but mask it + // to "undeclared" so a use of this binder is untypeable and + // the formula fails-and-skips, rather than silently leaking + // the outer declaration's type into the lemma. + None => self.env.remove(&decl.name), + } + } + let result = body(self); + self.env.pop_scope(); + result + } + + fn fail(&mut self, reason: &str) { + if self.failed.is_none() { + self.failed = Some(reason.to_string()); + } + } +} + +/// Flatten a same-operator ∧/∨ chain into its n-ary children, the way +/// Rodin's parser builds `AssociativePredicate` nodes. WD computation +/// must see the whole chain at once: pairwise processing yields +/// structurally different (wrong) lemmas. +fn flatten_chain<'a>(p: &'a Predicate, op: LogicalOp, out: &mut Vec<&'a Predicate>) { + match p { + Predicate::Logical { + op: child_op, + left, + right, + } if *child_op == op => { + flatten_chain(left, op, out); + flatten_chain(right, op, out); + } + _ => out.push(p), + } +} + +fn untyped(decls: &[TypedIdentifier]) -> Vec { + decls + .iter() + .map(|d| TypedIdentifier::untyped(d.name.clone())) + .collect() +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::types::Type; + use rossi::parse_predicate_str; + + #[test] + fn shadowing_binder_with_uninferable_type_skips_formula() { + // Outer f : BOOL ↔ BOOL; the inner ∃f shadows it but its own type + // can't be inferred from the body, so `f(1)` is untypeable and the + // whole formula is flagged for skipping — it must not borrow the + // outer declaration's type into the lemma. + let mut env = TypeEnv::new(); + env.insert("f", Type::relation(Type::Boolean, Type::Boolean)); + let p = parse_predicate_str("∃f·f(1) = 2").unwrap(); + let mut c = WdComputer::new(env); + let _ = c.wd_predicate(&p); + assert!(c.failed.is_some()); + } +} diff --git a/crates/rossi-build/src/wd/improve.rs b/crates/rossi-build/src/wd/improve.rs new file mode 100644 index 0000000..0c14716 --- /dev/null +++ b/crates/rossi-build/src/wd/improve.rs @@ -0,0 +1,424 @@ +//! WD lemma simplification — port of rodin-ast's +//! `org.eventb.internal.core.ast.wd.WDImprover` and its `Node`/`Lemma` +//! classes. +//! +//! The computed lemma is decomposed into a tree of conjunctions, +//! implications, universal quantifiers, and opaque leaf predicates. Each +//! leaf is normalized so that predicates under different quantifier +//! prefixes become comparable (Rodin shifts De Bruijn indices as if all +//! quantifiers were hoisted to the root; we rename bound identifiers to +//! positional markers, which is the same equivalence). The tree is then +//! simplified by marking subsumed nodes: +//! +//! - a leaf equal to one of the antecedents in force is dropped; +//! - duplicated antecedents are dropped; +//! - a lemma (antecedent set ⊢ consequent) subsumed by an already-known +//! lemma — same consequent, smaller antecedent set — is dropped, and +//! conversely evicts weaker known lemmas. +//! +//! Rebuilding the tree afterwards (subsumed nodes become `⊤`, which the +//! smart constructors absorb) yields Rodin's simplified WD predicate. + +use std::collections::BTreeSet; + +use rossi::ast::predicate::{LogicalOp, Quantifier}; +use rossi::{Predicate, TypedIdentifier}; + +use crate::wd::builder as fb; +use crate::wd::normal::{BinderRewriter, NamePolicy}; +use crate::wd::render::render_predicate; + +/// Simplify a computed WD lemma. `Predicate::True` means the whole +/// condition was discharged structurally. +pub fn improve(lemma: Predicate) -> Predicate { + let mut tree = Tree { nodes: Vec::new() }; + let root = tree.build(lemma); + tree.normalize(root, &mut Vec::new(), &mut 0); + let mut known: Vec = Vec::new(); + tree.simplify(root, &mut known, &BTreeSet::new()); + tree.original(root) +} + +type NodeId = usize; + +struct Tree { + nodes: Vec, +} + +struct Node { + kind: Kind, + subsumed: bool, +} + +enum Kind { + /// Flattened conjunction. + Land(Vec), + Limp(NodeId, NodeId), + Forall(Vec, NodeId), + /// Anything else — including `∨`, `⇔`, `∃` and relational predicates + /// — is an opaque leaf, exactly like Rodin's `NodePred`. + Leaf { + original: Predicate, + /// Set by [`Tree::normalize`]; the comparison key. + normalized: Option, + /// The marker-renamed predicate, for composing normalized keys + /// of enclosing implication nodes. + normalized_pred: Option, + }, +} + +/// An implication in comparable form: a set of antecedent keys and a +/// consequent key. Subsumption: A subsumes B iff same consequent and +/// A's antecedents ⊆ B's antecedents. +#[derive(Clone)] +struct Lemma { + antecedents: BTreeSet, + consequent: String, + origin: NodeId, +} + +impl Lemma { + fn subsumes(&self, other: &Lemma) -> bool { + self.consequent == other.consequent && self.antecedents.is_subset(&other.antecedents) + } +} + +impl Tree { + fn add(&mut self, kind: Kind) -> NodeId { + self.nodes.push(Node { + kind, + subsumed: false, + }); + self.nodes.len() - 1 + } + + /// Decompose the lemma: ∧-chains (any nesting) become n-ary `Land` + /// nodes — mirroring Rodin's `flatten()` before improvement — `⇒` + /// becomes `Limp`, `∀` becomes `Forall`, the rest are leaves. + fn build(&mut self, p: Predicate) -> NodeId { + match p { + Predicate::Logical { + op: LogicalOp::And, .. + } => { + let mut conjuncts = Vec::new(); + collect_conjuncts(p, &mut conjuncts); + let children: Vec = conjuncts.into_iter().map(|c| self.build(c)).collect(); + self.add(Kind::Land(children)) + } + Predicate::Logical { + op: LogicalOp::Implies, + left, + right, + } => { + let l = self.build(*left); + let r = self.build(*right); + self.add(Kind::Limp(l, r)) + } + Predicate::Quantified { + quantifier: Quantifier::ForAll, + identifiers, + predicate, + } => { + let child = self.build(*predicate); + self.add(Kind::Forall(identifiers, child)) + } + other => self.add(Kind::Leaf { + original: other, + normalized: None, + normalized_pred: None, + }), + } + } + + /// Assign root-first slots to the tree-level quantifier bindings and + /// normalize every leaf against them. Equivalent to Rodin's + /// `boundIdentifiersEqualizer`: a binder's identity becomes its + /// position in the (virtually hoisted) quantifier prefix. + fn normalize(&mut self, id: NodeId, scope: &mut Vec<(String, String)>, next_slot: &mut usize) { + match &self.nodes[id].kind { + Kind::Land(children) => { + for child in children.clone() { + self.normalize(child, scope, &mut next_slot.clone()); + } + } + Kind::Limp(l, r) => { + let (l, r) = (*l, *r); + self.normalize(l, scope, &mut next_slot.clone()); + self.normalize(r, scope, &mut next_slot.clone()); + } + Kind::Forall(decls, child) => { + let child = *child; + let names: Vec = decls.iter().map(|d| d.name.clone()).collect(); + let depth = scope.len(); + let mut slot = *next_slot; + for name in names { + scope.push((name, format!("${slot}"))); + slot += 1; + } + self.normalize(child, scope, &mut slot); + scope.truncate(depth); + } + Kind::Leaf { .. } => { + let mut renamer = + BinderRewriter::with_scope(scope.clone(), MarkerPolicy { counter: 0 }); + let Kind::Leaf { + original, + normalized, + normalized_pred, + } = &mut self.nodes[id].kind + else { + unreachable!() + }; + let renamed = renamer.pred(original); + *normalized = Some(render_predicate(&renamed)); + *normalized_pred = Some(renamed); + } + } + } + + /// The node as a normalized predicate (`asPredicate(fb, false)`): + /// subsumed nodes are `⊤`, quantifiers are transparent. + fn normalized_pred(&self, id: NodeId) -> Predicate { + let node = &self.nodes[id]; + if node.subsumed { + return Predicate::True; + } + match &node.kind { + Kind::Land(children) => { + fb::land(children.iter().map(|c| self.normalized_pred(*c)).collect()) + } + Kind::Limp(l, r) => fb::limp(self.normalized_pred(*l), self.normalized_pred(*r)), + Kind::Forall(_, child) => self.normalized_pred(*child), + Kind::Leaf { + normalized_pred, .. + } => normalized_pred.clone().expect("normalize() ran"), + } + } + + fn normalized_key(&self, id: NodeId) -> String { + match &self.nodes[id].kind { + Kind::Leaf { normalized, .. } if !self.nodes[id].subsumed => { + normalized.clone().expect("normalize() ran") + } + _ => render_predicate(&self.normalized_pred(id)), + } + } + + /// Collect this subtree's antecedent keys into `set`. A predicate + /// already present marks the node subsumed (duplicate antecedents + /// collapse), exactly like `Node.addPredicateToSet`. + fn collect_antecedents(&mut self, id: NodeId, set: &mut BTreeSet) { + match &self.nodes[id].kind { + Kind::Land(children) => { + for child in children.clone() { + self.collect_antecedents(child, set); + } + } + Kind::Forall(_, child) => { + let child = *child; + self.collect_antecedents(child, set); + } + Kind::Limp(..) | Kind::Leaf { .. } => self.add_predicate_to_set(id, set), + } + } + + fn add_predicate_to_set(&mut self, id: NodeId, set: &mut BTreeSet) { + if self.nodes[id].subsumed { + return; + } + let key = self.normalized_key(id); + if !set.insert(key) { + self.nodes[id].subsumed = true; + } + } + + fn simplify(&mut self, id: NodeId, known: &mut Vec, antecedents: &BTreeSet) { + if self.nodes[id].subsumed { + return; + } + match &self.nodes[id].kind { + Kind::Land(children) => { + for child in children.clone() { + self.simplify(child, known, antecedents); + } + } + Kind::Forall(_, child) => { + let child = *child; + self.simplify(child, known, antecedents); + } + Kind::Limp(l, r) => { + let (l, r) = (*l, *r); + // The left side is simplified against a private copy of + // the known lemmas (its discoveries don't leak out) and + // no antecedents. This must be a full deep clone, not a + // truncate-to-len / restore: `add_lemma` doesn't only + // append — it also *evicts* (`known.remove(i)`) every + // parent lemma the left side subsumes, so trimming back to + // the prior length would silently resurrect those evicted + // lemmas. Cloning is the cheapest trivially-correct + // isolation; `known` is small (a few lemmas per branch). + let mut left_known: Vec = known.clone(); + self.simplify(l, &mut left_known, &BTreeSet::new()); + // The right side gains the left side as hypotheses. + let mut right_antes = antecedents.clone(); + self.collect_antecedents(l, &mut right_antes); + self.simplify(r, known, &right_antes); + } + Kind::Leaf { .. } => { + let key = self.normalized_key(id); + if antecedents.contains(&key) { + self.nodes[id].subsumed = true; + return; + } + let lemma = Lemma { + antecedents: antecedents.clone(), + consequent: key, + origin: id, + }; + self.add_lemma(known, lemma); + } + } + } + + /// `Lemma.addToSet`: an existing lemma that subsumes the new one + /// kills it; otherwise the new one evicts every lemma it subsumes. + /// Never marks both sides. The eviction (`known.remove`) is why + /// `simplify`'s `Limp` branch isolates the left side with a deep + /// `known.clone()` rather than a truncate/restore. + fn add_lemma(&mut self, known: &mut Vec, lemma: Lemma) { + let mut i = 0; + while i < known.len() { + if known[i].subsumes(&lemma) { + self.nodes[lemma.origin].subsumed = true; + return; + } + if lemma.subsumes(&known[i]) { + let evicted = known.remove(i); + self.nodes[evicted.origin].subsumed = true; + continue; + } + i += 1; + } + known.push(lemma); + } + + /// Rebuild the simplified predicate from the original (source-form) + /// leaves; subsumed nodes become `⊤` and evaporate in the smart + /// constructors. + fn original(&self, id: NodeId) -> Predicate { + let node = &self.nodes[id]; + if node.subsumed { + return Predicate::True; + } + match &node.kind { + Kind::Land(children) => fb::land(children.iter().map(|c| self.original(*c)).collect()), + Kind::Limp(l, r) => fb::limp(self.original(*l), self.original(*r)), + Kind::Forall(decls, child) => fb::forall(decls.clone(), self.original(*child)), + Kind::Leaf { original, .. } => original.clone(), + } + } +} + +fn collect_conjuncts(p: Predicate, out: &mut Vec) { + match p { + Predicate::Logical { + op: LogicalOp::And, + left, + right, + } => { + collect_conjuncts(*left, out); + collect_conjuncts(*right, out); + } + other => out.push(other), + } +} + +// --------------------------------------------------------------------- +// Leaf normalization: bound-identifier renaming +// --------------------------------------------------------------------- + +/// Renames every bound identifier to a globally unique positional marker +/// (`$iN` in declaration preorder) so predicates under different +/// quantifier prefixes become comparable — a name-based equivalent of +/// comparing shifted De Bruijn terms (alpha-equivalence). Tree-level +/// binders enter the rewriter already mapped to their root-first slot +/// (`$0`, `$1`, …); `$` cannot occur in an Event-B identifier, so markers +/// never collide with free names. Drives the shared [`BinderRewriter`]. +struct MarkerPolicy { + counter: usize, +} + +impl NamePolicy for MarkerPolicy { + const NEEDS_NODE_FREE: bool = false; + fn choose(&mut self, _original: &str, _taken: &dyn Fn(&str) -> bool) -> String { + let marker = format!("$i{}", self.counter); + self.counter += 1; + marker + } +} + +#[cfg(test)] +mod tests { + use super::*; + use rossi::parse_predicate_str; + + fn imp(src: &str) -> String { + render_predicate(&improve(parse_predicate_str(src).unwrap())) + } + + #[test] + fn duplicate_conjuncts_collapse() { + // Identical consequents under the same antecedents: the second + // lemma is subsumed by the first. + assert_eq!(imp("x∈dom(f)∧f∈S ⇸ T∧x∈dom(f)"), "x∈dom(f)∧f∈S ⇸ T"); + } + + #[test] + fn consequent_equal_to_antecedent_collapses() { + assert_eq!(imp("x∈dom(f)⇒x∈dom(f)∧f∈S ⇸ T"), "x∈dom(f)⇒f∈S ⇸ T"); + } + + #[test] + fn weaker_lemma_is_subsumed_by_hypothesis_free_one() { + // f∈S⇸T holds unconditionally, so the conditional copy under + // x∈dom(f) is subsumed; the implication then collapses entirely. + assert_eq!(imp("f∈S ⇸ T∧(x∈dom(f)⇒f∈S ⇸ T)"), "f∈S ⇸ T"); + } + + #[test] + fn stronger_lemma_evicts_weaker_one() { + // The unconditional lemma arrives second and evicts the + // conditional occurrence. + assert_eq!(imp("(x∈dom(f)⇒f∈S ⇸ T)∧f∈S ⇸ T"), "f∈S ⇸ T"); + } + + #[test] + fn quantifier_prefixes_are_equalized() { + // The same leaf at different binding depths: ∀x·P⇒(∀y·P∧Q) + // where P doesn't mention y — Rodin's canonical example. The + // inner copy of x∈dom(f) is subsumed by the antecedent. + assert_eq!( + imp("∀x·x∈dom(f)⇒(∀y·x∈dom(f)∧y∈dom(f))"), + "∀x·x∈dom(f)⇒(∀y·y∈dom(f))" + ); + } + + #[test] + fn alpha_equivalent_leaves_match_across_branches() { + // Two sibling quantifiers binding different names: the leaves + // normalize to the same slot and the second lemma is subsumed. + assert_eq!(imp("(∀x·x∈S)∧(∀y·y∈S)"), "∀x·x∈S"); + } + + #[test] + fn fully_subsumed_tree_collapses_to_true() { + assert_eq!( + improve(parse_predicate_str("x∈S⇒x∈S∧x∈S").unwrap()), + { + // limp() already kills the first copy; the improver kills + // the rest. + Predicate::True + } + ); + } +} diff --git a/crates/rossi-build/src/wd/mod.rs b/crates/rossi-build/src/wd/mod.rs new file mode 100644 index 0000000..bad27d4 --- /dev/null +++ b/crates/rossi-build/src/wd/mod.rs @@ -0,0 +1,19 @@ +//! Rodin's well-definedness calculus. +//! +//! A faithful port of the machinery eventb-checker borrows from Rodin to +//! decide whether a formula is well-defined: the L-operator that derives a +//! formula's WD lemma ([`computer`]), the `FormulaBuilder` smart +//! constructors that keep the lemma in Rodin's normal form ([`builder`]), +//! the `WDImprover` simplifier that drops trivial and subsumed conjuncts +//! ([`mod@improve`]), binder flattening and capture-aware renaming +//! ([`normal`]), and the `Formula#toString` renderer that prints a lemma +//! byte-identically to Rodin ([`render`]). +//! +//! This module is the calculus only; turning its lemmas into diagnostics +//! over a checked project is layered on top. + +pub mod builder; +pub mod computer; +pub mod improve; +pub mod normal; +pub mod render; diff --git a/crates/rossi-build/src/wd/normal.rs b/crates/rossi-build/src/wd/normal.rs new file mode 100644 index 0000000..505c1ab --- /dev/null +++ b/crates/rossi-build/src/wd/normal.rs @@ -0,0 +1,800 @@ +//! AST normalizations Rodin applies around WD improvement. +//! +//! [`flatten`] ports the quantifier part of Rodin's `Formula.flatten()`: +//! directly-nested same-quantifier prefixes merge (`∀x·∀y·P` → `∀x,y·P`) +//! and declarations with no free occurrence in the body are dropped — +//! after improvement subsumes every use of a bound identifier, Rodin's +//! output loses the binder (`∀x·P` → `P` when `x` is unused). +//! +//! [`resolve_binders`] ports `QuantifiedUtil.resolveIdents`, the renaming +//! Rodin's `toString` applies to bound-identifier declarations: a +//! declaration whose name is already taken — by an enclosing binder or by +//! a free identifier of the quantified node — gets the first fresh +//! `name0`, `name1`, … (`∃b·∀x0·x0∈{y − x,…}⇒b≥x0` when `x` is bound +//! outside). Synthesized binders (the `$`-prefixed placeholders from +//! [`super::builder::bounded`]) resolve to their preferred name through +//! the same rule; `$` cannot occur in an Event-B identifier, so +//! placeholders never capture user names. + +use std::collections::BTreeSet; + +use rossi::ast::expression::IdentPattern; +use rossi::{Expression, Predicate, TypedIdentifier}; + +// --------------------------------------------------------------------- +// Free-name collection (name-based, shadow-aware) +// --------------------------------------------------------------------- +// +// This walk *descends into* every binder (quantifiers, lambdas, +// comprehensions, QUnion/QInter) with a shadowing stack, and covers +// predicates as well as expressions, so `free_names` answers "is this +// bound name actually referenced anywhere in the body?" — exactly what +// `flatten` and `resolve_binders` need to drop unused declarations and +// rename on capture. +// +// It is deliberately NOT the same analysis as +// `infer::collect_free_identifiers`, which *stops at* binders and is +// expression-only (it discovers the implicit binders of a SetBuilder). +// The two compute different things on purpose and must stay separate; +// the only point they meet is the `SetBuilder` arm below, which calls +// `collect_free_identifiers` to learn which names that node binds. + +pub(crate) fn predicate_free_names( + p: &Predicate, + bound: &mut Vec, + out: &mut BTreeSet, +) { + match p { + Predicate::True | Predicate::False => {} + Predicate::Comparison { left, right, .. } => { + expression_free_names(left, bound, out); + expression_free_names(right, bound, out); + } + Predicate::Not(inner) => predicate_free_names(inner, bound, out), + Predicate::Logical { left, right, .. } => { + predicate_free_names(left, bound, out); + predicate_free_names(right, bound, out); + } + Predicate::Quantified { + identifiers, + predicate, + .. + } => { + let depth = bound.len(); + bound.extend(identifiers.iter().map(|i| i.name.clone())); + predicate_free_names(predicate, bound, out); + bound.truncate(depth); + } + Predicate::Application { arguments, .. } + | Predicate::BuiltinApplication { arguments, .. } => { + for arg in arguments { + expression_free_names(arg, bound, out); + } + } + } +} + +pub(crate) fn expression_free_names( + e: &Expression, + bound: &mut Vec, + out: &mut BTreeSet, +) { + match e { + Expression::Identifier(name) => { + if !bound.iter().any(|b| b == name) { + out.insert(name.clone()); + } + } + Expression::Integer(_) + | Expression::True + | Expression::False + | Expression::EmptySet + | Expression::Naturals + | Expression::Naturals1 + | Expression::Integers + | Expression::BoolType + | Expression::StringLiteral(_) => {} + Expression::SetEnumeration(items) => { + for item in items { + expression_free_names(item, bound, out); + } + } + Expression::SetComprehension { + identifiers, + predicate, + expression, + } => { + let depth = bound.len(); + bound.extend(identifiers.iter().map(|i| i.name.clone())); + predicate_free_names(predicate, bound, out); + if let Some(body) = expression { + expression_free_names(body, bound, out); + } + bound.truncate(depth); + } + Expression::SetBuilder { + member_expression, + predicate, + } => { + // The implicit form binds every identifier of the member + // expression (mirrors the WD computer). + let mut names: Vec<&str> = Vec::new(); + crate::infer::collect_free_identifiers(member_expression, &mut names); + let depth = bound.len(); + bound.extend(names.iter().map(|n| (*n).to_string())); + predicate_free_names(predicate, bound, out); + bound.truncate(depth); + } + Expression::RelationalImage { relation, set } => { + expression_free_names(relation, bound, out); + expression_free_names(set, bound, out); + } + Expression::QuantifiedUnion { + identifiers, + predicate, + expression, + } + | Expression::QuantifiedInter { + identifiers, + predicate, + expression, + } => { + let depth = bound.len(); + bound.extend(identifiers.iter().map(|i| i.name.clone())); + predicate_free_names(predicate, bound, out); + expression_free_names(expression, bound, out); + bound.truncate(depth); + } + Expression::Lambda { + pattern, + predicate, + expression, + } => { + let depth = bound.len(); + bound.extend(pattern.identifiers().into_iter().map(str::to_string)); + predicate_free_names(predicate, bound, out); + expression_free_names(expression, bound, out); + bound.truncate(depth); + } + Expression::Binary { left, right, .. } => { + expression_free_names(left, bound, out); + expression_free_names(right, bound, out); + } + Expression::Unary { operand, .. } => expression_free_names(operand, bound, out), + Expression::FunctionApplication { + function, + arguments, + } => { + expression_free_names(function, bound, out); + for arg in arguments { + expression_free_names(arg, bound, out); + } + } + Expression::BuiltinApplication { arguments, .. } => { + for arg in arguments { + expression_free_names(arg, bound, out); + } + } + Expression::Bool(p) => predicate_free_names(p, bound, out), + Expression::IfThenElse { + condition, + then_expr, + else_expr, + } => { + predicate_free_names(condition, bound, out); + expression_free_names(then_expr, bound, out); + expression_free_names(else_expr, bound, out); + } + } +} + +fn free_names(p: &Predicate) -> BTreeSet { + let mut out = BTreeSet::new(); + predicate_free_names(p, &mut Vec::new(), &mut out); + out +} + +// --------------------------------------------------------------------- +// flatten — quantifier merging and unused-declaration removal +// --------------------------------------------------------------------- + +/// Port of the quantifier simplifications of Rodin's `Formula.flatten()`. +/// (The associative-chain merging part is moot on rossi's binary AST — +/// rendering and improvement both flatten chains structurally.) +pub fn flatten(p: Predicate) -> Predicate { + match p { + Predicate::True | Predicate::False => p, + Predicate::Comparison { op, left, right } => Predicate::Comparison { + op, + left: flatten_expr(left), + right: flatten_expr(right), + }, + Predicate::Not(inner) => Predicate::Not(Box::new(flatten(*inner))), + Predicate::Logical { op, left, right } => Predicate::Logical { + op, + left: Box::new(flatten(*left)), + right: Box::new(flatten(*right)), + }, + Predicate::Quantified { + quantifier, + mut identifiers, + predicate, + } => { + let mut body = flatten(*predicate); + // Merge directly-nested same-quantifier prefixes. + while let Predicate::Quantified { + quantifier: inner_q, + identifiers: inner_ids, + predicate: inner_body, + } = body + { + if inner_q == quantifier { + identifiers.extend(inner_ids); + body = *inner_body; + } else { + body = Predicate::Quantified { + quantifier: inner_q, + identifiers: inner_ids, + predicate: inner_body, + }; + break; + } + } + // Drop declarations with no bound occurrence in the body. + // Merging same-quantifier prefixes can leave two binders with + // the same name (`∀x·∀x·P` → decls `[x, x]`); a free `x` in the + // body binds to the *innermost* (last) one only, so an earlier + // shadowed duplicate is dead even though the name is free — + // De Bruijn flatten drops it. Name-set membership alone keeps + // both, diverging from Rodin (`∀x,x0·…`). + let free = free_names(&body); + let names: Vec<&str> = identifiers.iter().map(|d| d.name.as_str()).collect(); + let keep: Vec = (0..identifiers.len()) + .map(|i| free.contains(names[i]) && !names[i + 1..].contains(&names[i])) + .collect(); + let mut keep = keep.into_iter(); + identifiers.retain(|_| keep.next().unwrap_or(false)); + if identifiers.is_empty() { + body + } else { + Predicate::Quantified { + quantifier, + identifiers, + predicate: Box::new(body), + } + } + } + Predicate::Application { + function, + arguments, + } => Predicate::Application { + function, + arguments: arguments.into_iter().map(flatten_expr).collect(), + }, + Predicate::BuiltinApplication { + predicate, + arguments, + } => Predicate::BuiltinApplication { + predicate, + arguments: arguments.into_iter().map(flatten_expr).collect(), + }, + } +} + +fn flatten_expr(e: Expression) -> Expression { + match e { + Expression::Integer(_) + | Expression::Identifier(_) + | Expression::True + | Expression::False + | Expression::EmptySet + | Expression::Naturals + | Expression::Naturals1 + | Expression::Integers + | Expression::BoolType + | Expression::StringLiteral(_) => e, + Expression::SetEnumeration(items) => { + Expression::SetEnumeration(items.into_iter().map(flatten_expr).collect()) + } + Expression::SetComprehension { + identifiers, + predicate, + expression, + } => Expression::SetComprehension { + identifiers, + predicate: Box::new(flatten(*predicate)), + expression: expression.map(|b| Box::new(flatten_expr(*b))), + }, + Expression::SetBuilder { + member_expression, + predicate, + } => Expression::SetBuilder { + member_expression: Box::new(flatten_expr(*member_expression)), + predicate: Box::new(flatten(*predicate)), + }, + Expression::RelationalImage { relation, set } => Expression::RelationalImage { + relation: Box::new(flatten_expr(*relation)), + set: Box::new(flatten_expr(*set)), + }, + Expression::QuantifiedUnion { + identifiers, + predicate, + expression, + } => Expression::QuantifiedUnion { + identifiers, + predicate: Box::new(flatten(*predicate)), + expression: Box::new(flatten_expr(*expression)), + }, + Expression::QuantifiedInter { + identifiers, + predicate, + expression, + } => Expression::QuantifiedInter { + identifiers, + predicate: Box::new(flatten(*predicate)), + expression: Box::new(flatten_expr(*expression)), + }, + Expression::Lambda { + pattern, + predicate, + expression, + } => Expression::Lambda { + pattern, + predicate: Box::new(flatten(*predicate)), + expression: Box::new(flatten_expr(*expression)), + }, + Expression::Binary { op, left, right } => Expression::Binary { + op, + left: Box::new(flatten_expr(*left)), + right: Box::new(flatten_expr(*right)), + }, + Expression::Unary { op, operand } => Expression::Unary { + op, + operand: Box::new(flatten_expr(*operand)), + }, + Expression::FunctionApplication { + function, + arguments, + } => Expression::FunctionApplication { + function: Box::new(flatten_expr(*function)), + arguments: arguments.into_iter().map(flatten_expr).collect(), + }, + Expression::BuiltinApplication { + function, + arguments, + } => Expression::BuiltinApplication { + function, + arguments: arguments.into_iter().map(flatten_expr).collect(), + }, + Expression::Bool(p) => Expression::Bool(Box::new(flatten(*p))), + Expression::IfThenElse { + condition, + then_expr, + else_expr, + } => Expression::IfThenElse { + condition: Box::new(flatten(*condition)), + then_expr: Box::new(flatten_expr(*then_expr)), + else_expr: Box::new(flatten_expr(*else_expr)), + }, + } +} + +// --------------------------------------------------------------------- +// BinderRewriter — capture-avoiding bound-identifier renaming +// --------------------------------------------------------------------- + +/// Policy for choosing a bound identifier's replacement during a +/// [`BinderRewriter`] walk — the only thing that differs between Rodin's +/// `toString` collision resolution and the improver's positional-marker +/// renaming, which are otherwise the same traversal. +pub(crate) trait NamePolicy { + /// Whether the walk must compute a binder node's free names before + /// choosing replacements (collision resolution needs them; globally + /// unique markers never clash, so they don't). + const NEEDS_NODE_FREE: bool; + /// Choose the replacement for `original`. `taken` reports whether a + /// candidate already clashes with a free name of the node or an + /// earlier sibling declaration. + fn choose(&mut self, original: &str, taken: &dyn Fn(&str) -> bool) -> String; +} + +/// Rodin `toString` collision resolution: keep each binder's preferred +/// name (a `$name` placeholder resolves to `name`), suffixing `name0`, +/// `name1`, … only on a real clash with the node's free names. +pub(crate) struct DisplayPolicy; + +impl NamePolicy for DisplayPolicy { + const NEEDS_NODE_FREE: bool = true; + fn choose(&mut self, original: &str, taken: &dyn Fn(&str) -> bool) -> String { + let preferred = original.strip_prefix('$').unwrap_or(original); + let mut chosen = preferred.to_string(); + let mut i = 0usize; + while taken(&chosen) { + chosen = format!("{preferred}{i}"); + i += 1; + } + chosen + } +} + +/// Rename bound-identifier declarations the way Rodin's `toString` +/// resolves them: against the names *free in the quantified node* — +/// mere shadowing without capture keeps the name (`∃b·∀x·x∈{x·P ∣ x}…` +/// prints two `x` binders). Placeholders (`$name`) resolve to `name` +/// through the same collision rule. +pub fn resolve_binders(p: &Predicate) -> Predicate { + BinderRewriter::new(DisplayPolicy).pred(p) +} + +/// A capture-avoiding rewrite of bound identifiers, parameterized by a +/// [`NamePolicy`]. The single binder-scoped traversal shared by +/// [`resolve_binders`] and the improver's leaf normalization, so a scoping +/// fix can't land in one copy and silently miss the other. +pub(crate) struct BinderRewriter

{ + /// original name → replacement name, innermost binder last. + scope: Vec<(String, String)>, + policy: P, +} + +impl BinderRewriter

{ + pub(crate) fn new(policy: P) -> Self { + Self { + scope: Vec::new(), + policy, + } + } + + /// Seed the rewriter with an enclosing scope: the improver maps the + /// tree-level binders to their positional slots before walking a leaf. + pub(crate) fn with_scope(scope: Vec<(String, String)>, policy: P) -> Self { + Self { scope, policy } + } + + fn display<'a>(&'a self, name: &'a str) -> &'a str { + self.scope + .iter() + .rev() + .find(|(n, _)| n == name) + .map_or(name, |(_, d)| d.as_str()) + } + + /// Push replacements for one binder node's declarations, deferring the + /// per-name choice to the policy. A referenced enclosing binder shows + /// up in `node_free` through the scope mapping; an unreferenced one + /// causes no collision — matching Rodin's `resolveIdents`, which only + /// consults the names used in the subtree. Returns the scope checkpoint + /// to truncate to afterwards. + fn bind( + &mut self, + decls: &[String], + node_free: &BTreeSet, + ) -> (usize, Vec) { + let checkpoint = self.scope.len(); + let mut displays: Vec = Vec::with_capacity(decls.len()); + for name in decls { + let chosen = { + let taken = |cand: &str| { + node_free.contains(cand) || displays.iter().any(|d| d.name == cand) + }; + self.policy.choose(name, &taken) + }; + self.scope.push((name.clone(), chosen.clone())); + displays.push(TypedIdentifier::untyped(chosen)); + } + (checkpoint, displays) + } + + fn unbind(&mut self, checkpoint: usize) { + self.scope.truncate(checkpoint); + } + + /// Free names of a binder node, mapped through the current scope to + /// their replacement form. Empty when the policy renames to globally + /// unique markers that can never collide. + fn node_free( + &self, + bound: &[String], + preds: &[&Predicate], + exprs: &[&Expression], + ) -> BTreeSet { + if !P::NEEDS_NODE_FREE { + return BTreeSet::new(); + } + let mut raw = BTreeSet::new(); + let mut bound_vec: Vec = bound.to_vec(); + for p in preds { + predicate_free_names(p, &mut bound_vec, &mut raw); + } + for e in exprs { + expression_free_names(e, &mut bound_vec, &mut raw); + } + raw.iter().map(|n| self.display(n).to_string()).collect() + } + + pub(crate) fn pred(&mut self, p: &Predicate) -> Predicate { + match p { + Predicate::True | Predicate::False => p.clone(), + Predicate::Comparison { op, left, right } => Predicate::Comparison { + op: *op, + left: self.expr(left), + right: self.expr(right), + }, + Predicate::Not(inner) => Predicate::Not(Box::new(self.pred(inner))), + Predicate::Logical { op, left, right } => Predicate::Logical { + op: *op, + left: Box::new(self.pred(left)), + right: Box::new(self.pred(right)), + }, + Predicate::Quantified { + quantifier, + identifiers, + predicate, + } => { + let names: Vec = identifiers.iter().map(|i| i.name.clone()).collect(); + let free = self.node_free(&names, &[predicate], &[]); + let (checkpoint, displays) = self.bind(&names, &free); + let body = self.pred(predicate); + self.unbind(checkpoint); + Predicate::Quantified { + quantifier: *quantifier, + identifiers: displays, + predicate: Box::new(body), + } + } + Predicate::Application { + function, + arguments, + } => Predicate::Application { + function: function.clone(), + arguments: arguments.iter().map(|a| self.expr(a)).collect(), + }, + Predicate::BuiltinApplication { + predicate, + arguments, + } => Predicate::BuiltinApplication { + predicate: *predicate, + arguments: arguments.iter().map(|a| self.expr(a)).collect(), + }, + } + } + + fn expr(&mut self, e: &Expression) -> Expression { + match e { + Expression::Identifier(name) => Expression::Identifier(self.display(name).to_string()), + Expression::Integer(_) + | Expression::True + | Expression::False + | Expression::EmptySet + | Expression::Naturals + | Expression::Naturals1 + | Expression::Integers + | Expression::BoolType + | Expression::StringLiteral(_) => e.clone(), + Expression::SetEnumeration(items) => { + Expression::SetEnumeration(items.iter().map(|i| self.expr(i)).collect()) + } + Expression::SetComprehension { + identifiers, + predicate, + expression, + } => { + let names: Vec = identifiers.iter().map(|i| i.name.clone()).collect(); + let mut parts: Vec<&Expression> = Vec::new(); + if let Some(body) = expression { + parts.push(body); + } + let free = self.node_free(&names, &[predicate], &parts); + let (checkpoint, displays) = self.bind(&names, &free); + let p = self.pred(predicate); + let body = expression.as_ref().map(|b| Box::new(self.expr(b))); + self.unbind(checkpoint); + Expression::SetComprehension { + identifiers: displays, + predicate: Box::new(p), + expression: body, + } + } + Expression::SetBuilder { + member_expression, + predicate, + } => { + let mut raw: Vec<&str> = Vec::new(); + crate::infer::collect_free_identifiers(member_expression, &mut raw); + let mut names: Vec = Vec::new(); + for n in raw { + if names.iter().all(|m| m != n) { + names.push(n.to_string()); + } + } + let free = self.node_free(&names, &[predicate], &[member_expression]); + let (checkpoint, _) = self.bind(&names, &free); + let member = self.expr(member_expression); + let p = self.pred(predicate); + self.unbind(checkpoint); + Expression::SetBuilder { + member_expression: Box::new(member), + predicate: Box::new(p), + } + } + Expression::RelationalImage { relation, set } => Expression::RelationalImage { + relation: Box::new(self.expr(relation)), + set: Box::new(self.expr(set)), + }, + Expression::QuantifiedUnion { + identifiers, + predicate, + expression, + } => { + let (ids, p, b) = self.quantified_expr(identifiers, predicate, expression); + Expression::QuantifiedUnion { + identifiers: ids, + predicate: p, + expression: b, + } + } + Expression::QuantifiedInter { + identifiers, + predicate, + expression, + } => { + let (ids, p, b) = self.quantified_expr(identifiers, predicate, expression); + Expression::QuantifiedInter { + identifiers: ids, + predicate: p, + expression: b, + } + } + Expression::Lambda { + pattern, + predicate, + expression, + } => { + let names: Vec = pattern + .identifiers() + .into_iter() + .map(str::to_string) + .collect(); + let free = self.node_free(&names, &[predicate], &[expression]); + let (checkpoint, _) = self.bind(&names, &free); + let renamed = self.pattern(pattern); + let p = self.pred(predicate); + let body = self.expr(expression); + self.unbind(checkpoint); + Expression::Lambda { + pattern: renamed, + predicate: Box::new(p), + expression: Box::new(body), + } + } + Expression::Binary { op, left, right } => Expression::Binary { + op: *op, + left: Box::new(self.expr(left)), + right: Box::new(self.expr(right)), + }, + Expression::Unary { op, operand } => Expression::Unary { + op: *op, + operand: Box::new(self.expr(operand)), + }, + Expression::FunctionApplication { + function, + arguments, + } => Expression::FunctionApplication { + function: Box::new(self.expr(function)), + arguments: arguments.iter().map(|a| self.expr(a)).collect(), + }, + Expression::BuiltinApplication { + function, + arguments, + } => Expression::BuiltinApplication { + function: *function, + arguments: arguments.iter().map(|a| self.expr(a)).collect(), + }, + Expression::Bool(p) => Expression::Bool(Box::new(self.pred(p))), + Expression::IfThenElse { + condition, + then_expr, + else_expr, + } => Expression::IfThenElse { + condition: Box::new(self.pred(condition)), + then_expr: Box::new(self.expr(then_expr)), + else_expr: Box::new(self.expr(else_expr)), + }, + } + } + + fn quantified_expr( + &mut self, + identifiers: &[TypedIdentifier], + predicate: &Predicate, + expression: &Expression, + ) -> (Vec, Box, Box) { + let names: Vec = identifiers.iter().map(|i| i.name.clone()).collect(); + let free = self.node_free(&names, &[predicate], &[expression]); + let (checkpoint, displays) = self.bind(&names, &free); + let p = self.pred(predicate); + let body = self.expr(expression); + self.unbind(checkpoint); + (displays, Box::new(p), Box::new(body)) + } + + fn pattern(&mut self, pattern: &IdentPattern) -> IdentPattern { + match pattern { + IdentPattern::Identifier(t) => IdentPattern::Identifier(TypedIdentifier::untyped( + self.display(&t.name).to_string(), + )), + IdentPattern::Maplet(l, r) => { + IdentPattern::Maplet(Box::new(self.pattern(l)), Box::new(self.pattern(r))) + } + } + } +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::wd::render::render_predicate; + use rossi::parse_predicate_str; + + #[test] + fn flatten_drops_unused_decls() { + let p = parse_predicate_str("∀x,y·x∈S").unwrap(); + assert_eq!(render_predicate(&flatten(p)), "∀x·x∈S"); + let q = parse_predicate_str("∀x·a∈S").unwrap(); + assert_eq!(render_predicate(&flatten(q)), "a∈S"); + } + + #[test] + fn flatten_merges_nested_same_quantifier() { + let p = parse_predicate_str("∀x·∀y·x ↦ y∈S").unwrap(); + assert_eq!(render_predicate(&flatten(p)), "∀x,y·x ↦ y∈S"); + // Different quantifiers stay nested. + let q = parse_predicate_str("∀x·∃y·x ↦ y∈S").unwrap(); + assert_eq!(render_predicate(&flatten(q)), "∀x·∃y·x ↦ y∈S"); + } + + #[test] + fn flatten_drops_shadowed_duplicate_binder() { + // ∀x·∀x·x∈S merges to decls [x, x]; the body's x binds to the + // inner one, so the outer shadowed x is dead and dropped — Rodin's + // De Bruijn flatten yields `∀x·x∈S`, not a renamed `∀x,x0·…`. + let p = parse_predicate_str("∀x·∀x·x∈S").unwrap(); + assert_eq!(render_predicate(&flatten(p)), "∀x·x∈S"); + let q = parse_predicate_str("∀x·∀x·∀x·x∈S").unwrap(); + assert_eq!(render_predicate(&flatten(q)), "∀x·x∈S"); + } + + #[test] + fn placeholders_resolve_to_preferred_names() { + let set = rossi::parse_expression_str("s").unwrap(); + let p = crate::wd::builder::bounded(set, false); + assert_eq!(render_predicate(&resolve_binders(&p)), "∃b·∀x·x∈s⇒b≥x"); + } + + #[test] + fn colliding_placeholder_gets_suffixed() { + // bounded() inside ∀x — the synthesized x collides and becomes x0, + // while occurrences of the outer x are untouched. + let set = rossi::parse_expression_str("{y − x,x − y}").unwrap(); + let inner = crate::wd::builder::bounded(set, false); + let outer = Predicate::quantified( + rossi::ast::predicate::Quantifier::ForAll, + vec![ + TypedIdentifier::untyped("x".into()), + TypedIdentifier::untyped("y".into()), + ], + inner, + ); + assert_eq!( + render_predicate(&resolve_binders(&outer)), + "∀x,y·∃b·∀x0·x0∈{y − x,x − y}⇒b≥x0" + ); + } + + #[test] + fn shadowing_without_capture_keeps_the_name() { + // The inner binder never references the outer x, so Rodin keeps + // both named x. + let p = parse_predicate_str("∀x·x∈S∧(∀x·x∈T)").unwrap(); + assert_eq!(render_predicate(&resolve_binders(&p)), "∀x·x∈S∧(∀x·x∈T)"); + } +} diff --git a/crates/rossi-build/src/wd/render.rs b/crates/rossi-build/src/wd/render.rs new file mode 100644 index 0000000..c9ec29a --- /dev/null +++ b/crates/rossi-build/src/wd/render.rs @@ -0,0 +1,694 @@ +//! Rodin-`toString` renderer for WD lemmas. +//! +//! Renders a predicate the way Rodin's `Formula.toString()` does, because +//! the WD message contract is byte-identical output to eventb-checker +//! (which prints Rodin `Predicate#toString()` verbatim). This differs from +//! the Camille canonical form in `crate::normalize` on several axes, so it +//! gets its own renderer rather than retrofitting `rossi::pretty`: +//! +//! - Rodin-*associative* expression operators (`∪ ∩ + ∗ ∘ ; `) print +//! tight, all other infix expression operators (including `↦`, `−`, +//! `∖`, `×`, the arrows) get one space each side: `Union ⇸ ℙ(Union × Names)`. +//! - Relational and logical predicate operators are always tight: +//! `∀e·e∈dom(f)⇒f∈S ⇸ T`. +//! - Bound-identifier declarations never show types (`∀x·…`, not `∀x⦂ℤ·…`). +//! - The comprehension bar is spaced: `{y·y∈s ∣ y}`. +//! +//! Parenthesization starts from the shared `rossi::op_info` table and is +//! patched against eventb-checker oracle findings. + +use rossi::ast::expression::{BinaryOp, IdentPattern, UnaryOp}; +use rossi::ast::predicate::LogicalOp; +use rossi::operators::{self, binary_op_id, comparison_op_id, logical_op_id, quantifier_id}; +use rossi::{Expression, Predicate, TypedIdentifier, op_info}; + +/// Render a predicate as Rodin's `Predicate#toString()` would. +#[must_use] +pub fn render_predicate(p: &Predicate) -> String { + let mut s = String::new(); + pred(&mut s, p); + s +} + +/// Render an expression as Rodin's `Expression#toString()` would. +#[must_use] +pub fn render_expression(e: &Expression) -> String { + let mut s = String::new(); + expr(&mut s, e); + s +} + +fn spell(id: operators::OperatorId) -> &'static str { + operators::spell(id, true) +} + +// --------------------------------------------------------------------- +// Predicates +// --------------------------------------------------------------------- + +fn pred(out: &mut String, p: &Predicate) { + match p { + Predicate::True => out.push('⊤'), + Predicate::False => out.push('⊥'), + Predicate::Comparison { op, left, right } => { + expr_comparison_operand(out, left); + out.push_str(spell(comparison_op_id(*op))); + expr_comparison_operand(out, right); + } + Predicate::Not(inner) => { + out.push('¬'); + pred_not_operand(out, inner); + } + Predicate::Logical { op, .. } => { + let mut children: Vec<&Predicate> = Vec::new(); + flatten_logical(p, *op, &mut children); + let sym = spell(logical_op_id(*op)); + for (i, child) in children.iter().enumerate() { + if i > 0 { + out.push_str(sym); + } + pred_logical_operand(out, child, *op); + } + } + Predicate::Quantified { + quantifier, + identifiers, + predicate, + } => { + out.push_str(spell(quantifier_id(*quantifier))); + decls(out, identifiers); + out.push('·'); + pred(out, predicate); // quantifier body extends to the right + } + Predicate::Application { + function, + arguments, + } => { + out.push_str(function); + out.push('('); + args(out, arguments); + out.push(')'); + } + Predicate::BuiltinApplication { + predicate, + arguments, + } => { + out.push_str(predicate.name()); + out.push('('); + args(out, arguments); + out.push(')'); + } + } +} + +/// Collect the children of a same-operator ∧/∨ chain (any nesting shape), +/// mirroring Rodin's n-ary associative predicates after `flatten()`. +/// `⇒` and `⇔` are binary in Rodin, so they only ever yield two children. +fn flatten_logical<'a>(p: &'a Predicate, op: LogicalOp, out: &mut Vec<&'a Predicate>) { + match p { + Predicate::Logical { + op: child_op, + left, + right, + } if *child_op == op && matches!(op, LogicalOp::And | LogicalOp::Or) => { + flatten_logical(left, op, out); + flatten_logical(right, op, out); + } + Predicate::Logical { + op: child_op, + left, + right, + } if *child_op == op => { + // ⇒ / ⇔ — binary, left then right. + out.push(left); + out.push(right); + } + _ => out.push(p), + } +} + +fn pred_logical_operand(out: &mut String, child: &Predicate, parent_op: LogicalOp) { + let needs_parens = match child { + // Quantifiers sit below the connectives in Rodin's grammar: they + // are parenthesized as operands, even as the right child of `⇒` + // (`…⇒(∀p,n·…)` in the oracle output). + Predicate::Quantified { .. } => true, + Predicate::Logical { op: child_op, .. } => { + let child_prec = op_info::logical_precedence(*child_op); + let parent_prec = op_info::logical_precedence(parent_op); + // Same-op ∧/∨ chains were flattened away; what remains needs + // parens when not strictly tighter than the parent. + child_prec <= parent_prec + } + _ => false, + }; + if needs_parens { + out.push('('); + pred(out, child); + out.push(')'); + } else { + pred(out, child); + } +} + +fn pred_not_operand(out: &mut String, child: &Predicate) { + match child { + Predicate::Logical { .. } | Predicate::Quantified { .. } => { + out.push('('); + pred(out, child); + out.push(')'); + } + _ => pred(out, child), + } +} + +// --------------------------------------------------------------------- +// Expressions +// --------------------------------------------------------------------- + +/// True for operators Rodin models as `AssociativeExpression` — these +/// print tight (`a∪b`, `a+b`). Every other infix expression operator is +/// a Rodin `BinaryExpression` and gets one space each side (`a − b`, +/// `S × T`, `f g`… exception: `` is associative, see list). +fn is_rodin_associative(op: BinaryOp) -> bool { + matches!( + op, + BinaryOp::Add + | BinaryOp::Multiply + | BinaryOp::Union + | BinaryOp::Intersection + | BinaryOp::Composition + | BinaryOp::Semicolon + | BinaryOp::Overwrite + ) +} + +fn expr(out: &mut String, e: &Expression) { + match e { + Expression::Integer(n) => out.push_str(&n.to_string()), + Expression::Identifier(name) => out.push_str(name), + Expression::True => out.push_str("TRUE"), + Expression::False => out.push_str("FALSE"), + Expression::EmptySet => out.push('∅'), + Expression::Naturals => out.push('ℕ'), + Expression::Naturals1 => out.push_str("ℕ1"), + Expression::Integers => out.push('ℤ'), + Expression::BoolType => out.push_str("BOOL"), + Expression::StringLiteral(s) => { + out.push('"'); + out.push_str(s); + out.push('"'); + } + Expression::SetEnumeration(items) => { + out.push('{'); + args(out, items); + out.push('}'); + } + Expression::SetComprehension { + identifiers, + predicate, + expression, + } => { + out.push('{'); + match expression { + Some(body) => { + decls(out, identifiers); + out.push('·'); + pred(out, predicate); + out.push_str(" ∣ "); + expr(out, body); + } + None => { + decls(out, identifiers); + out.push_str(" ∣ "); + pred(out, predicate); + } + } + out.push('}'); + } + Expression::SetBuilder { + member_expression, + predicate, + } => { + out.push('{'); + expr(out, member_expression); + out.push_str(" ∣ "); + pred(out, predicate); + out.push('}'); + } + Expression::RelationalImage { relation, set } => { + expr_tight_operand(out, relation); + out.push('['); + expr(out, set); + out.push(']'); + } + Expression::QuantifiedUnion { + identifiers, + predicate, + expression, + } => quantified_expr(out, "⋃", identifiers, predicate, expression), + Expression::QuantifiedInter { + identifiers, + predicate, + expression, + } => quantified_expr(out, "⋂", identifiers, predicate, expression), + Expression::Lambda { + pattern, + predicate, + expression, + } => { + out.push('λ'); + ident_pattern(out, pattern); + out.push('·'); + pred(out, predicate); + out.push_str(" ∣ "); + expr(out, expression); + } + Expression::Binary { + op: BinaryOp::OfType, + left, + .. + } => { + // Rodin folds the `⦂T` type ascription into the atomic's type + // at type-check, so `Predicate#toString()` prints only the + // ascribed expression (`finite(∅⦂ℙ(S))` → `finite(∅)`). + // Verified against eventb-checker. + expr(out, left); + } + Expression::Binary { op, left, right } => { + expr_binary_operand(out, left, *op, false); + if is_rodin_associative(*op) { + out.push_str(spell(binary_op_id(*op))); + } else { + out.push(' '); + out.push_str(spell(binary_op_id(*op))); + out.push(' '); + } + expr_binary_operand(out, right, *op, true); + } + Expression::Unary { op, operand } => match op { + UnaryOp::Minus => { + out.push('−'); + expr_minus_operand(out, operand); + } + UnaryOp::PowerSet => call(out, "ℙ", operand), + UnaryOp::PowerSet1 => call(out, "ℙ1", operand), + UnaryOp::Domain => call(out, "dom", operand), + UnaryOp::Range => call(out, "ran", operand), + UnaryOp::Inverse => { + expr_tight_operand(out, operand); + out.push('∼'); + } + }, + Expression::FunctionApplication { + function, + arguments, + } => { + expr_tight_operand(out, function); + out.push('('); + args(out, arguments); + out.push(')'); + } + Expression::BuiltinApplication { + function, + arguments, + } => { + out.push_str(function.name()); + out.push('('); + args(out, arguments); + out.push(')'); + } + Expression::Bool(p) => { + out.push_str("bool("); + pred(out, p); + out.push(')'); + } + Expression::IfThenElse { + condition, + then_expr, + else_expr, + } => { + // ProB extension — never produced by Rodin, rendered for + // completeness only. + out.push_str("IF "); + pred(out, condition); + out.push_str(" THEN "); + expr(out, then_expr); + out.push_str(" ELSE "); + expr(out, else_expr); + out.push_str(" END"); + } + } +} + +fn quantified_expr( + out: &mut String, + sym: &str, + identifiers: &[TypedIdentifier], + predicate: &Predicate, + expression: &Expression, +) { + out.push_str(sym); + decls(out, identifiers); + out.push('·'); + pred(out, predicate); + out.push_str(" ∣ "); + expr(out, expression); +} + +fn call(out: &mut String, name: &str, operand: &Expression) { + out.push_str(name); + out.push('('); + expr(out, operand); + out.push(')'); +} + +/// Operand of a binary expression operator: parenthesized per the shared +/// precedence/compatibility table. +fn expr_binary_operand(out: &mut String, child: &Expression, parent_op: BinaryOp, is_right: bool) { + let needs_parens = match strip_oftype(child) { + Expression::Lambda { .. } + | Expression::QuantifiedUnion { .. } + | Expression::QuantifiedInter { .. } => true, + Expression::Unary { + op: UnaryOp::Minus, .. + } => { + // Unary minus binds at additive precedence, left-associatively + // (`(−c)∗d`, but `−a+b` / `−a − b` bare). Verified against + // eventb-checker. + let parent_prec = op_info::binary_precedence(parent_op); + let child_prec = op_info::unary_minus_precedence(); + child_prec < parent_prec || (child_prec == parent_prec && is_right) + } + Expression::Binary { op: child_op, .. } => { + let child_prec = op_info::binary_precedence(*child_op); + let parent_prec = op_info::binary_precedence(parent_op); + if child_prec < parent_prec { + true + } else if child_prec > parent_prec { + false + } else if *child_op == BinaryOp::CartesianProduct + && parent_op == BinaryOp::CartesianProduct + { + // Rodin prints left-nested × chains bare: + // `interaction_modes × ℤ × ℙ(AIRPLANES × ℤ)`. + is_right + } else if !op_info::binary_ops_compatible(*child_op, parent_op) + || op_info::is_non_associative(parent_op) + { + true + } else { + // Left-associative: right child needs parens. + is_right + } + } + _ => false, + }; + if needs_parens { + out.push('('); + expr(out, child); + out.push(')'); + } else { + expr(out, child); + } +} + +/// See through a source-level `⦂` type ascription: Rodin folds the type +/// into the atomic's type at type-check, so `e⦂T` renders and +/// parenthesizes exactly as `e`. Idempotent on every other expression. +fn strip_oftype(e: &Expression) -> &Expression { + let mut cur = e; + while let Expression::Binary { + op: BinaryOp::OfType, + left, + .. + } = cur + { + cur = left; + } + cur +} + +/// Operand of unary `−`. Rodin binds unary minus at additive precedence, +/// so a tighter operand (`∗`/`÷`/`mod`/`^`) prints bare (`−a∗b`) while a +/// same-or-looser binary, or a nested `−`, needs parens (`−(a+b)`, +/// `−(−a)`). Verified against eventb-checker. +fn expr_minus_operand(out: &mut String, child: &Expression) { + let needs_parens = match strip_oftype(child) { + Expression::Binary { op, .. } => { + op_info::binary_precedence(*op) <= op_info::unary_minus_precedence() + } + Expression::Unary { + op: UnaryOp::Minus, .. + } + | Expression::Lambda { .. } + | Expression::QuantifiedUnion { .. } + | Expression::QuantifiedInter { .. } => true, + _ => false, + }; + if needs_parens { + out.push('('); + expr(out, child); + out.push(')'); + } else { + expr(out, child); + } +} + +/// Operand in a tight position: function position of an application, +/// relation of `r[S]`, postfix `∼`. Only atom-like expressions go bare. +fn expr_tight_operand(out: &mut String, child: &Expression) { + let bare = matches!( + strip_oftype(child), + Expression::Integer(_) + | Expression::Identifier(_) + | Expression::True + | Expression::False + | Expression::EmptySet + | Expression::Naturals + | Expression::Naturals1 + | Expression::Integers + | Expression::BoolType + | Expression::SetEnumeration(_) + | Expression::SetComprehension { .. } + | Expression::SetBuilder { .. } + | Expression::RelationalImage { .. } + | Expression::FunctionApplication { .. } + | Expression::BuiltinApplication { .. } + | Expression::Bool(_) + | Expression::Unary { + op: UnaryOp::PowerSet + | UnaryOp::PowerSet1 + | UnaryOp::Domain + | UnaryOp::Range + | UnaryOp::Inverse, + .. + } + ); + if bare { + expr(out, child); + } else { + out.push('('); + expr(out, child); + out.push(')'); + } +} + +/// Operand of a relational predicate (`∈`, `=`, …): expressions of any +/// binary precedence go bare (`x ↦ y+1∈dom(f)`); quantified expression +/// forms are parenthesized. Sees through a `⦂` ascription when deciding +/// (like the other operand handlers), so `(λ…⦂T)∈R` keeps its parens. +fn expr_comparison_operand(out: &mut String, child: &Expression) { + match strip_oftype(child) { + Expression::Lambda { .. } + | Expression::QuantifiedUnion { .. } + | Expression::QuantifiedInter { .. } => { + out.push('('); + expr(out, child); + out.push(')'); + } + _ => expr(out, child), + } +} + +// --------------------------------------------------------------------- +// Shared bits +// --------------------------------------------------------------------- + +fn args(out: &mut String, items: &[Expression]) { + for (i, item) in items.iter().enumerate() { + if i > 0 { + out.push(','); + } + expr(out, item); + } +} + +/// Bound-identifier declarations: names only, comma-tight — Rodin's +/// `toString` never prints declaration types. +fn decls(out: &mut String, identifiers: &[TypedIdentifier]) { + for (i, ident) in identifiers.iter().enumerate() { + if i > 0 { + out.push(','); + } + out.push_str(&ident.name); + } +} + +fn ident_pattern(out: &mut String, pattern: &IdentPattern) { + match pattern { + IdentPattern::Identifier(t) => out.push_str(&t.name), + IdentPattern::Maplet(l, r) => { + ident_pattern(out, l); + out.push_str(" ↦ "); + ident_pattern(out, r); + } + } +} + +#[cfg(test)] +mod tests { + use super::*; + use rossi::{parse_expression_str, parse_predicate_str}; + + fn rp(src: &str) -> String { + render_predicate(&parse_predicate_str(src).unwrap()) + } + + #[test] + fn oftype_ascribed_lambda_operand_keeps_parens() { + // `expr_comparison_operand` must see through `⦂` like the other + // operand handlers: an OfType-ascribed lambda compared with `∈` + // keeps the parentheses a bare lambda gets, else the relation is + // swallowed into the lambda body (`λx·x>0 ∣ x∈R`). The `⦂` folds + // away in rendering, so both forms are identical. + assert_eq!(rp("(λx·x>0∣x)⦂ℙ(ℤ×ℤ)∈R"), "(λx·x>0 ∣ x)∈R"); + assert_eq!(rp("(λx·x>0∣x)∈R"), "(λx·x>0 ∣ x)∈R"); + } + + #[test] + fn relational_and_logical_are_tight() { + assert_eq!(rp("x ∈ S ∧ y = 3 ⇒ z ≠ 0"), "x∈S∧y=3⇒z≠0"); + } + + #[test] + fn binary_expression_ops_are_spaced() { + assert_eq!(rp("f ∈ S ∖ T ⇸ U × V"), "f∈S ∖ T ⇸ U × V"); + assert_eq!(rp("a − 1 ∈ 1 ‥ b"), "a − 1∈1 ‥ b"); + } + + #[test] + fn associative_expression_ops_are_tight() { + assert_eq!(rp("a + b ∗ c ∈ S ∪ T"), "a+b∗c∈S∪T"); + } + + #[test] + fn maplet_is_spaced_inside_tight_relation() { + assert_eq!(rp("x ↦ y ∈ dom(f)"), "x ↦ y∈dom(f)"); + } + + #[test] + fn implication_in_conjunction_is_parenthesized() { + let p = Predicate::logical( + LogicalOp::And, + parse_predicate_str("a ∈ S ⇒ b ∈ S").unwrap(), + parse_predicate_str("c ∈ S").unwrap(), + ); + assert_eq!(render_predicate(&p), "(a∈S⇒b∈S)∧c∈S"); + } + + #[test] + fn conjunction_under_implication_is_bare() { + assert_eq!(rp("a ∈ S ∧ b ∈ S ⇒ c ∈ S"), "a∈S∧b∈S⇒c∈S"); + } + + #[test] + fn quantifier_is_parenthesized_as_operand() { + let p = Predicate::logical( + LogicalOp::Implies, + parse_predicate_str("s ≠ ∅").unwrap(), + parse_predicate_str("∀x · x ∈ s").unwrap(), + ); + assert_eq!(render_predicate(&p), "s≠∅⇒(∀x·x∈s)"); + let q = Predicate::logical( + LogicalOp::And, + parse_predicate_str("s ≠ ∅").unwrap(), + parse_predicate_str("∃b · ∀x · x ∈ s ⇒ b ≥ x").unwrap(), + ); + assert_eq!(render_predicate(&q), "s≠∅∧(∃b·∀x·x∈s⇒b≥x)"); + } + + #[test] + fn quantifier_body_extends_right_without_parens() { + assert_eq!(rp("∀e · e ∈ dom(f) ⇒ f ∈ S ⇸ T"), "∀e·e∈dom(f)⇒f∈S ⇸ T"); + } + + #[test] + fn set_extension_commas_are_tight() { + assert_eq!(rp("{TRUE ↦ a, FALSE ↦ b} ≠ ∅"), "{TRUE ↦ a,FALSE ↦ b}≠∅"); + } + + #[test] + fn comprehension_bar_is_spaced() { + let e = parse_expression_str("{y · y ∈ s ∣ y}").unwrap(); + assert_eq!(render_expression(&e), "{y·y∈s ∣ y}"); + } + + #[test] + fn inverse_is_tight_postfix() { + assert_eq!(rp("r∼[{c}] ⊆ S"), "r∼[{c}]⊆S"); + } + + #[test] + fn type_expression_needs_no_parens() { + // partial(f) for f : ℤ×ℤ ⇸ ℤ — × binds tighter than ⇸. + assert_eq!(rp("g ∈ ℤ × ℤ ⇸ ℤ"), "g∈ℤ × ℤ ⇸ ℤ"); + } + + fn re(src: &str) -> String { + render_expression(&parse_expression_str(src).unwrap()) + } + + #[test] + fn unary_minus_parenthesized_under_tighter_operator() { + // Unary minus binds at additive precedence; multiplicative, + // division and exponent are tighter, so the minus needs parens + // on either side. Golden strings from eventb-checker. + assert_eq!(re("(−a) ∗ b"), "(−a)∗b"); + assert_eq!(re("b ∗ (−a)"), "b∗(−a)"); + assert_eq!(re("(−a) ÷ b"), "(−a) ÷ b"); + assert_eq!(re("(−a) ^ b"), "(−a) ^ b"); + assert_eq!(re("(−a) mod b"), "(−a) mod b"); + assert_eq!(re("(−a) ∗ (−b)"), "(−a)∗(−b)"); + } + + #[test] + fn unary_minus_bare_at_additive_level() { + // Same precedence as +/−, left-associative: the left operand is + // bare, the right operand is parenthesized. Golden strings from + // eventb-checker. + assert_eq!(re("(−a) + b"), "−a+b"); + assert_eq!(re("(−a) − b"), "−a − b"); + assert_eq!(re("b + (−a)"), "b+(−a)"); + assert_eq!(re("b − (−a)"), "b − (−a)"); + } + + #[test] + fn unary_minus_operand_follows_its_own_precedence() { + // The operand of `−` is bare when it binds tighter (`−a∗b`) and + // parenthesized otherwise (`−(a+b)`, `−(−a)`). Golden strings + // from eventb-checker. + assert_eq!(re("−(a ∗ b)"), "−a∗b"); + assert_eq!(re("−(a + b)"), "−(a+b)"); + assert_eq!(re("−(−a)"), "−(−a)"); + assert_eq!(re("−(a)"), "−a"); + } + + #[test] + fn oftype_ascription_is_folded_away() { + // Rodin folds `⦂T` into the atomic's type; toString omits it. + assert_eq!(re("∅ ⦂ ℙ(S)"), "∅"); + assert_eq!(rp("∅ ⦂ ℙ(S) = ∅ ⦂ ℙ(S)"), "∅=∅"); + assert_eq!(rp("(∅ ⦂ ℙ(S)) ∪ s = s"), "∅∪s=s"); + } +} From 9d79dda604b0766778145a2562885728f5e75545 Mon Sep 17 00:00:00 2001 From: Denis Efremov Date: Sun, 14 Jun 2026 20:36:12 +0400 Subject: [PATCH 2/4] feat(wd): emit EB010 well-definedness findings from the typed model Drive the calculus over a checked project: for every formula the static check kept, compute its WD lemma, simplify it, and report the survivors as INFO diagnostics carrying RuleId::WellDefinedness (EB010), the message rendered byte-identically to eventb-checker. Raw component ASTs supply the formulas (the lemma embeds verbatim source fragments); the typed model supplies the environments and decides which clauses the check kept, paired by source position rather than label. Registers EB010 in the rule catalogue. --- crates/rossi-build/src/rules.rs | 15 +- crates/rossi-build/src/wd/mod.rs | 251 +++++++++++++++++++++++++++++-- 2 files changed, 252 insertions(+), 14 deletions(-) diff --git a/crates/rossi-build/src/rules.rs b/crates/rossi-build/src/rules.rs index a9a849e..157091d 100644 --- a/crates/rossi-build/src/rules.rs +++ b/crates/rossi-build/src/rules.rs @@ -9,9 +9,8 @@ use crate::Severity; /// Validation rule identifiers exposed in `Diagnostic.rule_id`. /// -/// Codes follow the eventb-checker scheme (`"EB001"`..`"EB019"`); unused -/// numbers correspond to rules not yet implemented in rossi (e.g. EB010 well- -/// definedness, EB015–17 proof status). +/// Codes follow the eventb-checker scheme (`"EB001"`..`"EB019"`), with the +/// full catalogue implemented. #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] pub enum RuleId { /// EB001 — XML parse error (corrupt Rodin archive, malformed `.buc`/`.bum`). @@ -32,6 +31,8 @@ pub enum RuleId { CircularRefines, /// EB009 — Cross-reference target not found (unknown SEES / EXTENDS / REFINES name). CrossReferenceNotFound, + /// EB010 — Non-trivial well-definedness condition (informational). + WellDefinedness, /// EB011 — Declared variable never referenced. DeadVariable, /// EB012 — Variable referenced but never assigned by any event. @@ -63,6 +64,7 @@ impl RuleId { RuleId::CircularExtends => "EB007", RuleId::CircularRefines => "EB008", RuleId::CrossReferenceNotFound => "EB009", + RuleId::WellDefinedness => "EB010", RuleId::DeadVariable => "EB011", RuleId::UnmodifiedVariable => "EB012", RuleId::DeadConstant => "EB013", @@ -86,6 +88,7 @@ impl RuleId { RuleId::CircularExtends => "Circular EXTENDS", RuleId::CircularRefines => "Circular REFINES", RuleId::CrossReferenceNotFound => "Cross-reference not found", + RuleId::WellDefinedness => "Well-definedness condition", RuleId::DeadVariable => "Dead variable", RuleId::UnmodifiedVariable => "Unmodified variable", RuleId::DeadConstant => "Dead constant", @@ -123,6 +126,9 @@ impl RuleId { RuleId::CrossReferenceNotFound => { "A SEES, EXTENDS, or REFINES clause names a component that does not exist." } + RuleId::WellDefinedness => { + "A formula carries a non-trivial well-definedness condition that must be proven." + } RuleId::DeadVariable => { "A machine variable is declared but never referenced in any invariant, guard, or action." } @@ -168,6 +174,7 @@ impl RuleId { | RuleId::IncompleteInitialisation | RuleId::DuplicateComponent | RuleId::ShadowedName => Severity::Warning, + RuleId::WellDefinedness => Severity::Info, } } @@ -185,6 +192,7 @@ impl RuleId { RuleId::CircularExtends, RuleId::CircularRefines, RuleId::CrossReferenceNotFound, + RuleId::WellDefinedness, RuleId::DeadVariable, RuleId::UnmodifiedVariable, RuleId::DeadConstant, @@ -224,6 +232,7 @@ mod tests { assert_eq!(RuleId::CircularExtends.code(), "EB007"); assert_eq!(RuleId::CircularRefines.code(), "EB008"); assert_eq!(RuleId::CrossReferenceNotFound.code(), "EB009"); + assert_eq!(RuleId::WellDefinedness.code(), "EB010"); assert_eq!(RuleId::DeadVariable.code(), "EB011"); assert_eq!(RuleId::UnmodifiedVariable.code(), "EB012"); assert_eq!(RuleId::DeadConstant.code(), "EB013"); diff --git a/crates/rossi-build/src/wd/mod.rs b/crates/rossi-build/src/wd/mod.rs index bad27d4..7d50377 100644 --- a/crates/rossi-build/src/wd/mod.rs +++ b/crates/rossi-build/src/wd/mod.rs @@ -1,19 +1,248 @@ -//! Rodin's well-definedness calculus. +//! Well-definedness conditions (EB010). //! -//! A faithful port of the machinery eventb-checker borrows from Rodin to -//! decide whether a formula is well-defined: the L-operator that derives a -//! formula's WD lemma ([`computer`]), the `FormulaBuilder` smart -//! constructors that keep the lemma in Rodin's normal form ([`builder`]), -//! the `WDImprover` simplifier that drops trivial and subsumed conjuncts -//! ([`mod@improve`]), binder flattening and capture-aware renaming -//! ([`normal`]), and the `Formula#toString` renderer that prints a lemma -//! byte-identically to Rodin ([`render`]). +//! Mirrors eventb-checker's `WellDefinednessChecker`: for every formula +//! the static check accepted, compute its WD lemma (Rodin's L-operator, +//! [`computer`]), simplify it (Rodin's `WDImprover`, [`mod@improve`]), and +//! report the survivors as INFO diagnostics with the message +//! `Well-definedness condition: ` — byte-identical to +//! eventb-checker, which prints Rodin's `Predicate#toString()` +//! ([`render`]). //! -//! This module is the calculus only; turning its lemmas into diagnostics -//! over a checked project is layered on top. +//! Formulas come from the *raw* component ASTs (the lemma embeds +//! verbatim fragments of the source, including its comprehension forms); +//! the [`ScModel`] supplies the type environments and decides which +//! formulas the static check kept. Coverage matches eventb-checker: +//! context axioms and theorems; machine invariants, theorems, and +//! variant; event guards, actions, and witnesses (including +//! INITIALISATION). pub mod builder; pub mod computer; pub mod improve; pub mod normal; pub mod render; + +use std::collections::HashSet; + +use rossi::{Action, Component, Expression, Predicate}; + +use crate::project::Project; +use crate::sc::{CheckedContext, CheckedMachine, ScModel}; +use crate::{Diagnostic, RuleId, Severity}; + +use computer::WdComputer; +use improve::improve; +use normal::{flatten, resolve_binders}; +use render::render_predicate; + +/// Compute WD findings for every successfully-checked component of the +/// project, in declaration order. +pub fn run(project: &Project, model: &ScModel) -> Vec { + let mut out = Vec::new(); + // The [`ScModel`] is keyed by component name, so a project with two + // components of the same name (a duplicate already flagged EB019) has + // a single model entry for both. Check each name once to avoid pairing + // a raw component against another's environment and emitting duplicate + // EB010 rows. + let mut seen: HashSet<&str> = HashSet::new(); + for pc in &project.components { + match &pc.component { + Component::Context(ctx) => { + if seen.insert(&ctx.name) + && let Some(cc) = model.contexts.get(&ctx.name) + { + check_context(ctx, cc, &mut out); + } + } + Component::Machine(m) => { + if seen.insert(&m.name) + && let Some(cm) = model.machines.get(&m.name) + { + check_machine(m, cm, &mut out); + } + } + } + } + out +} + +/// Yields the raw clauses the SC kept, paired by source *position* rather +/// than label: two clauses can share an (effective) label, so label-set +/// membership would WD-check a clause the SC actually dropped. `idx` reads +/// each kept decl's `source_index`; `raw` is the verbatim source list. +/// Centralized so all seven call sites share one pairing implementation. +fn kept_clauses<'a, D, R: 'a>( + decls: &[D], + idx: impl Fn(&D) -> usize, + raw: impl Iterator + 'a, +) -> impl Iterator + 'a { + let kept: HashSet = decls.iter().map(idx).collect(); + raw.enumerate() + .filter_map(move |(i, item)| kept.contains(&i).then_some(item)) +} + +fn check_context( + ctx: &rossi::ast::context::Context, + cc: &CheckedContext, + out: &mut Vec, +) { + // One computer per environment: the env is restored after each formula + // (every binder scope is popped), so reuse avoids re-cloning it. + let mut computer = WdComputer::new(cc.env().clone()); + for ax in kept_clauses(&cc.record.axioms, |a| a.source_index, ctx.axioms.iter()) { + let label = effective(&ax.label, "axm"); + check( + &mut computer, + Formula::Pred(&ax.predicate), + format!("{}.{}", ctx.name, label), + out, + ); + } +} + +fn check_machine(m: &rossi::Machine, cm: &CheckedMachine, out: &mut Vec) { + // Invariants and the variant share the machine environment; one computer + // serves both (it self-restores after each formula). + let mut mc = WdComputer::new(cm.env().clone()); + for inv in kept_clauses( + &cm.record.invariants, + |i| i.source_index, + m.invariants.iter(), + ) { + let label = effective(&inv.label, "inv"); + check( + &mut mc, + Formula::Pred(&inv.predicate), + format!("{}.{}", m.name, label), + out, + ); + } + + if let (Some(variant), Some(decl)) = (&m.variant, &cm.record.variant) { + check( + &mut mc, + Formula::Expr(variant), + format!("{}.{}", m.name, decl.label), + out, + ); + } + + if let (Some(init), Some(decl)) = (&m.initialisation, cm.events_by_label.get("INITIALISATION")) + { + // `event_env` builds an owned env per event — move it into the + // computer (no clone) and reuse it for the INIT actions + witnesses. + let mut ec = WdComputer::new(cm.event_env(decl)); + for act in kept_clauses(&decl.actions, |a| a.source_index, init.actions.iter()) { + let label = effective(&act.label, "act"); + check( + &mut ec, + Formula::Act(&act.action), + format!("{}.INITIALISATION/{}", m.name, label), + out, + ); + } + // Witnesses are paired in the SC's build order (`witnesses` then + // `with`); see [`super::sc::machine_record::WitnessDecl::source_index`]. + for wit in kept_clauses( + &decl.witnesses, + |w| w.source_index, + init.witnesses.iter().chain(&init.with), + ) { + let label = effective(&wit.label, "wit"); + check( + &mut ec, + Formula::Pred(&wit.predicate), + format!("{}.INITIALISATION/{}", m.name, label), + out, + ); + } + } + + for event in &m.events { + let Some(decl) = cm.events_by_label.get(&event.name) else { + continue; + }; + let mut ec = WdComputer::new(cm.event_env(decl)); + + for guard in kept_clauses(&decl.guards, |g| g.source_index, event.guards.iter()) { + let label = effective(&guard.label, "grd"); + check( + &mut ec, + Formula::Pred(&guard.predicate), + format!("{}.{}/{}", m.name, event.name, label), + out, + ); + } + + for act in kept_clauses(&decl.actions, |a| a.source_index, event.actions.iter()) { + let label = effective(&act.label, "act"); + check( + &mut ec, + Formula::Act(&act.action), + format!("{}.{}/{}", m.name, event.name, label), + out, + ); + } + + // Witnesses paired in `witnesses`-then-`with` order (see INIT). + for wit in kept_clauses( + &decl.witnesses, + |w| w.source_index, + event.witnesses.iter().chain(&event.with), + ) { + let label = effective(&wit.label, "wit"); + check( + &mut ec, + Formula::Pred(&wit.predicate), + format!("{}.{}/{}", m.name, event.name, label), + out, + ); + } + } +} + +enum Formula<'a> { + Pred(&'a Predicate), + Expr(&'a Expression), + Act(&'a Action), +} + +/// The eventb-checker recipe: compute, drop trivially-true lemmas, +/// improve, drop again, report. A formula whose lemma cannot be fully +/// built (untypeable function application) is skipped rather than +/// reported partially. +fn check( + computer: &mut WdComputer, + formula: Formula<'_>, + origin: String, + out: &mut Vec, +) { + computer.reset(); + let lemma = match formula { + Formula::Pred(p) => computer.wd_predicate(p), + Formula::Expr(e) => computer.wd_expression(e), + Formula::Act(a) => computer.wd_action(a), + }; + if computer.failed.is_some() || lemma == Predicate::True { + return; + } + // Rodin: getWDLemma() flattens, improve() flattens again at the end, + // and toString resolves bound-name collisions. + let improved = flatten(improve(flatten(lemma))); + if improved == Predicate::True { + return; + } + out.push(Diagnostic { + severity: Severity::Info, + origin, + message: format!( + "Well-definedness condition: {}", + render_predicate(&resolve_binders(&improved)) + ), + rule_id: Some(RuleId::WellDefinedness), + }); +} + +fn effective<'a>(label: &'a Option, default: &'static str) -> &'a str { + label.as_deref().unwrap_or(default) +} From 2bf34034fd320a9b0b1e05bd12eb3828b61796f7 Mon Sep 17 00:00:00 2001 From: Denis Efremov Date: Sun, 14 Jun 2026 20:37:05 +0400 Subject: [PATCH 3/4] test(wd): pin well-definedness output to the eventb-checker oracle Add the wd_oracle_diff gate: build each corpus model, run the WD pipeline, and assert the rendered findings are byte-identical to eventb-checker's EB010 output. The gate is #[ignore] and skips unless EVENTB_CORPUS_DIR and the oracle CLI are available. Factor the corpus plumbing it shares with the other oracle gates (eventb_checker_bin, oracle_available, collect_zips) into tests/common. --- crates/rossi-build/tests/common/mod.rs | 29 +++ crates/rossi-build/tests/wd_oracle_diff.rs | 219 +++++++++++++++++++++ 2 files changed, 248 insertions(+) create mode 100644 crates/rossi-build/tests/wd_oracle_diff.rs diff --git a/crates/rossi-build/tests/common/mod.rs b/crates/rossi-build/tests/common/mod.rs index 6d1f739..61e9c28 100644 --- a/crates/rossi-build/tests/common/mod.rs +++ b/crates/rossi-build/tests/common/mod.rs @@ -256,6 +256,35 @@ pub fn locate_corpus() -> Option { env_path("EVENTB_CORPUS_DIR").filter(|p| p.is_dir()) } +/// The `eventb-checker` oracle command: `EVENTB_CHECKER` if set, else the +/// `eventb-checker` CLI resolved from `PATH`. Shared by the oracle-diff gates. +pub fn eventb_checker_bin() -> String { + std::env::var("EVENTB_CHECKER").unwrap_or_else(|_| "eventb-checker".to_string()) +} + +/// Whether the oracle CLI is runnable (` --version` succeeds). +pub fn oracle_available(bin: &str) -> bool { + std::process::Command::new(bin) + .arg("--version") + .output() + .map(|o| o.status.success()) + .unwrap_or(false) +} + +/// The `.zip` corpus models in `dir`, sorted for deterministic iteration. +pub fn collect_zips(dir: &Path) -> Vec { + let mut zips: Vec = std::fs::read_dir(dir) + .map(|rd| { + rd.filter_map(Result::ok) + .map(|e| e.path()) + .filter(|p| p.extension().is_some_and(|x| x == "zip")) + .collect() + }) + .unwrap_or_default(); + zips.sort(); + zips +} + /// One row of a corpus report: the `model` and its `expected`/`actual` /// outcomes, the resulting `verdict`, and any `notes`. Shared by every corpus /// harness; see [`write_report`] for the columnar layout. diff --git a/crates/rossi-build/tests/wd_oracle_diff.rs b/crates/rossi-build/tests/wd_oracle_diff.rs new file mode 100644 index 0000000..9ecbd5c --- /dev/null +++ b/crates/rossi-build/tests/wd_oracle_diff.rs @@ -0,0 +1,219 @@ +//! Well-definedness oracle diff — compares `rossi_build::wd` against +//! eventb-checker's EB010 findings over a corpus of real Rodin archives. +//! +//! This is a GATE on message text: every finding both sides report for +//! the same `(component, element)` must be byte-identical (eventb-checker +//! prints Rodin's `Predicate#toString()`, so this pins the whole +//! compute → improve → render pipeline to Rodin's output). +//! +//! Coverage differences are allowed only for models the corpus flags with +//! `wd_coverage_gap` in its `model_flags.tsv` — places where the two tools +//! legitimately check different formula sets (each row's notes give the +//! reason: a component rossi's parser rejects, a decomposition stub rossi +//! does not check, an event/guard/witness one side's type check drops, a +//! variant labelled differently, …). Keeping the model list in the corpus +//! rather than this source avoids leaking corpus contents into the tree. +//! Message mismatches still fail even for flagged models — only one-sided +//! rows are tolerated. +//! +//! Ignored by default (needs the `eventb-checker` CLI and a models +//! corpus). Run: +//! +//! cargo test -p rossi-build --test wd_oracle_diff -- --ignored --nocapture +//! +//! The corpus directory is taken from `EVENTB_CORPUS_DIR` (the test skips +//! when unset). The oracle runs from `PATH`; set `EVENTB_CHECKER` to +//! override. + +mod common; + +use std::collections::BTreeMap; +use std::path::Path; +use std::process::Command; + +use common::{collect_zips, eventb_checker_bin, load_flags, locate_corpus, oracle_available}; +use rossi_build::rules::RuleId; +use rossi_build::{Project, build_with_model, wd}; + +#[test] +#[ignore = "needs the eventb-checker CLI and a models corpus; run with --ignored"] +fn wd_oracle_diff() { + let oracle = eventb_checker_bin(); + if !oracle_available(&oracle) { + eprintln!( + "SKIP wd_oracle_diff: `{oracle}` not runnable. Install the eventb-checker CLI \ + or set EVENTB_CHECKER to its path." + ); + return; + } + let Some(dir) = locate_corpus() else { + eprintln!("SKIP wd_oracle_diff: EVENTB_CORPUS_DIR is not set"); + return; + }; + let zips = collect_zips(&dir); + if zips.is_empty() { + eprintln!("SKIP wd_oracle_diff: no .zip models in {}", dir.display()); + return; + } + // Coverage-gap models are declared in the corpus, not here — see the + // module docs. + let gap_flags = load_flags(&dir.join("model_flags.tsv")).unwrap_or_default(); + eprintln!("oracle: {oracle}"); + eprintln!("corpus: {} zip(s) in {}", zips.len(), dir.display()); + + let (mut matched, mut failures) = (0usize, Vec::new()); + for zip in &zips { + let name = zip.file_name().and_then(|s| s.to_str()).unwrap_or("?"); + let model = zip.file_stem().and_then(|s| s.to_str()).unwrap_or(""); + let coverage_gap_ok = gap_flags + .get(model) + .is_some_and(|f| f.contains("wd_coverage_gap")); + match diff_one(&oracle, zip, coverage_gap_ok) { + Ok(n) => { + matched += n; + eprintln!(" OK {name} ({n} finding(s))"); + } + Err(e) => { + eprintln!(" FAIL {name}: {e}"); + failures.push(format!("{name}: {e}")); + } + } + } + eprintln!("total byte-identical findings: {matched}"); + + assert!( + failures.is_empty(), + "{} model(s) diverged from the oracle:\n{}", + failures.len(), + failures.join("\n") + ); +} + +/// Returns the number of byte-identical findings on success. `coverage_gap_ok` +/// comes from the corpus `wd_coverage_gap` flag and tolerates one-sided rows. +fn diff_one(oracle: &str, zip: &Path, coverage_gap_ok: bool) -> Result { + let theirs = rodin_wd(oracle, zip)?; + // A rossi-side loader failure is a real divergence, not "0 findings" — + // only swallow it for models we already know rossi can't parse. + let mine = match rossi_wd(zip) { + Ok(m) => m, + Err(_) if coverage_gap_ok => BTreeMap::new(), + Err(e) => return Err(e), + }; + + let mut matched = 0usize; + let mut problems = Vec::new(); + let keys: Vec<&(String, String)> = mine.keys().chain(theirs.keys()).collect(); + let mut seen = std::collections::HashSet::new(); + for key in keys { + if !seen.insert(key) { + continue; + } + match (mine.get(key), theirs.get(key)) { + (Some(a), Some(b)) if a == b => matched += 1, + (Some(a), Some(b)) => problems.push(format!( + "MISMATCH {}/{}: rossi `{a}` vs oracle `{b}`", + key.0, key.1 + )), + (Some(_), None) if coverage_gap_ok => {} + (None, Some(_)) if coverage_gap_ok => {} + (Some(_), None) => problems.push(format!("ROSSI_ONLY {}/{}", key.0, key.1)), + (None, Some(_)) => problems.push(format!("ROSSI_MISSING {}/{}", key.0, key.1)), + (None, None) => unreachable!("key came from one of the maps"), + } + } + if problems.is_empty() { + Ok(matched) + } else { + problems.truncate(5); + Err(problems.join("; ")) + } +} + +/// rossi's EB010 findings keyed by (component, element). Errors when the +/// model can't be loaded (the caller decides whether that's a known gap) +/// or when two findings collide on one key — a collision would otherwise +/// let a masked divergence slip through as a MATCH. +fn rossi_wd(zip: &Path) -> Result, String> { + let project = Project::from_zip_file(zip).map_err(|e| format!("rossi load: {e}"))?; + let (_result, model) = build_with_model(&project); + let mut out = BTreeMap::new(); + for d in wd::run(&project, &model) { + if d.rule_id != Some(RuleId::WellDefinedness) { + continue; + } + let (component, element) = d.origin.split_once('.').map_or_else( + || (d.origin.clone(), String::new()), + |(c, e)| (c.to_string(), e.to_string()), + ); + let message = d + .message + .strip_prefix("Well-definedness condition: ") + .unwrap_or(&d.message) + .to_string(); + if let Some(prev) = out.insert((component.clone(), element.clone()), message) { + return Err(format!( + "rossi findings collide on {component}/{element}: `{prev}`" + )); + } + } + Ok(out) +} + +/// eventb-checker's EB010 findings keyed by (component, element). +fn rodin_wd(oracle: &str, zip: &Path) -> Result, String> { + let output = Command::new(oracle) + .args(["check", "--show-info", "--format", "json"]) + .arg(zip) + .output() + .map_err(|e| format!("spawn {oracle}: {e}"))?; + if output.stdout.is_empty() { + return Err(format!( + "no oracle output (status {}): {}", + output.status, + String::from_utf8_lossy(&output.stderr).trim() + )); + } + let json: serde_json::Value = + serde_json::from_slice(&output.stdout).map_err(|e| format!("oracle json: {e}"))?; + let rows = json + .get("errors") + .and_then(|v| v.as_array()) + .ok_or("oracle json has no errors array")?; + + let mut out = BTreeMap::new(); + for row in rows { + if row.get("ruleId").and_then(|v| v.as_str()) != Some("EB010") { + continue; + } + let file = row.get("file").and_then(|v| v.as_str()).unwrap_or(""); + let component = Path::new(file) + .file_stem() + .and_then(|s| s.to_str()) + .unwrap_or("") + .to_string(); + let mut element = row + .get("element") + .and_then(|v| v.as_str()) + .unwrap_or("") + .to_string(); + if element.is_empty() { + // The variant carries no label attribute in Rodin XML; + // rossi labels it "vrn". + element = "vrn".to_string(); + } + let message = row + .get("message") + .and_then(|v| v.as_str()) + .unwrap_or("") + .strip_prefix("Well-definedness condition: ") + .unwrap_or("") + .to_string(); + if let Some(prev) = out.insert((component.clone(), element.clone()), message) { + return Err(format!( + "oracle findings collide on {component}/{element}: `{prev}`" + )); + } + } + Ok(out) +} From 8935b70ab7c13afaf1e86138e8509047320ffa0d Mon Sep 17 00:00:00 2001 From: Denis Efremov Date: Sun, 14 Jun 2026 20:37:30 +0400 Subject: [PATCH 4/4] feat(validate): surface EB010 well-definedness via --show-info Wire the WD pipeline into `rossi validate`: build the typed model once, run wd:: over it, and fold the EB010 findings into the results. They are INFO-severity and, like eventb-checker, dropped from every output format unless the new --show-info flag is set; the WD pass is skipped entirely when its rows would be discarded. Text output gains an INFO glyph. --- crates/rossi-cli/src/commands/validate.rs | 29 ++++++++- crates/rossi-cli/tests/cli_test.rs | 78 +++++++++++++++++++++++ 2 files changed, 104 insertions(+), 3 deletions(-) diff --git a/crates/rossi-cli/src/commands/validate.rs b/crates/rossi-cli/src/commands/validate.rs index b9b5e0c..22aa2d0 100644 --- a/crates/rossi-cli/src/commands/validate.rs +++ b/crates/rossi-cli/src/commands/validate.rs @@ -40,6 +40,11 @@ pub struct ValidateArgs { #[arg(long)] no_lints: bool, + /// Include INFO-severity findings in the output (hidden by default, + /// like eventb-checker's --show-info). + #[arg(long)] + show_info: bool, + /// Reported file name for `-` (stdin) input (default: ``). #[arg(long, value_name = "PATH")] stdin_filename: Option, @@ -117,7 +122,12 @@ pub fn run(cli: ValidateArgs) -> ExitCode { let aggregating_format = matches!(cli.format, OutputFormat::Json | OutputFormat::Sarif); for file in &cli.files { - let file_results = validate_file(file, &cli); + let mut file_results = validate_file(file, &cli); + // Drop INFO rows before any formatting or counting so summaries + // match what is displayed (eventb-checker's `withoutInfo()`). + if !cli.show_info { + file_results.retain(|r| r.severity != Some(Severity::Info)); + } for result in file_results { if !result.success { @@ -339,10 +349,19 @@ fn fold_semantic( cli: &ValidateArgs, out: &mut Vec, ) { - let build = rossi_build::build(project); + let (build, model) = rossi_build::build_with_model(project); for diag in build.diagnostics { out.push(fold_diagnostic(file, diag)); } + // EB010 well-definedness conditions are INFO-only, and INFO rows are + // dropped from every output format unless `--show-info` is set (see + // the post-collection filter). Running the WD pipeline otherwise is + // pure waste — skip it when the rows would be discarded. + if cli.show_info { + for diag in rossi_build::wd::run(project, &model) { + out.push(fold_diagnostic(file, diag)); + } + } if !cli.no_lints { for diag in rossi_build::lint::run(project) { out.push(fold_diagnostic(file, diag)); @@ -500,7 +519,11 @@ fn print_text_result(result: &ValidationResult, quiet: bool) { } let is_error = result.severity == Some(Severity::Error); - let glyph = if is_error { "✗" } else { "!" }; + let glyph = match result.severity { + Some(Severity::Error) => "✗", + Some(Severity::Info) => "i", + _ => "!", + }; let prefix = result .rule_id .map(|r| format!("[{}] ", r.code())) diff --git a/crates/rossi-cli/tests/cli_test.rs b/crates/rossi-cli/tests/cli_test.rs index 02f11b3..e9c81d4 100644 --- a/crates/rossi-cli/tests/cli_test.rs +++ b/crates/rossi-cli/tests/cli_test.rs @@ -1113,6 +1113,84 @@ fn validate_zip_bad_formula_reports_eb005() { ); } +#[test] +fn validate_zip_reports_wd_condition_with_show_info() { + // EB010 findings are INFO-severity: hidden by default, shown with + // --show-info, never affecting the exit code. The message is the + // Rodin-rendered WD lemma (byte-compatible with eventb-checker). + let tmp = tempdir_unique("rossi-cli-validate-wd"); + let zip_path = tmp.join("wd.zip"); + write_zip( + &zip_path, + &[( + "C0.buc", + r#" + + + + + + + +"# + .as_bytes(), + )], + ); + + // Default: INFO rows filtered out, exit 0. + let output = Command::new("cargo") + .args([ + "run", + "-p", + "rossi-cli", + "--", + "validate", + "--format", + "json", + zip_path.to_str().unwrap(), + ]) + .output() + .expect("Failed to execute command"); + assert!(output.status.success()); + let stdout = String::from_utf8_lossy(&output.stdout); + assert!( + !stdout.contains("EB010"), + "INFO findings must be hidden without --show-info: {stdout}" + ); + + // --show-info: the WD condition appears, exit code stays 0. + let output = Command::new("cargo") + .args([ + "run", + "-p", + "rossi-cli", + "--", + "validate", + "--show-info", + "--format", + "json", + zip_path.to_str().unwrap(), + ]) + .output() + .expect("Failed to execute command"); + assert!( + output.status.success(), + "INFO findings should not flip the exit code; stderr={}", + String::from_utf8_lossy(&output.stderr) + ); + let stdout = String::from_utf8_lossy(&output.stdout); + for needle in [ + "\"rule_id\": \"EB010\"", + "\"severity\": \"info\"", + "Well-definedness condition: x∈dom(f)∧f∈S ⇸ ℤ", + "\"origin\": \"C0.axm3\"", + ] { + assert!(stdout.contains(needle), "expected {needle} in: {stdout}"); + } + + std::fs::remove_dir_all(&tmp).ok(); +} + fn assert_validate_zip_json_contains_rule( tmp_prefix: &str, zip_name: &str,