diff --git a/crates/allium-parser/src/analysis.rs b/crates/allium-parser/src/analysis.rs index e97979a..6bb9d2d 100644 --- a/crates/allium-parser/src/analysis.rs +++ b/crates/allium-parser/src/analysis.rs @@ -67,6 +67,11 @@ pub struct ReverseContributions { /// witnesses by guarding on `from` and assigning `to` on a binding typed to /// that entity by the imported module's surface `provides:` (#64). pub witnessed_transitions: HashMap>, + /// Field names of imported entities that an importer references via a + /// qualified access (`alias/Entity.field`). Such a field is used even though + /// its only reference lives in another module, so the imported module must + /// not report it as unused. + pub referenced_fields: HashSet, } impl ReverseContributions { @@ -75,6 +80,7 @@ impl ReverseContributions { self.provided_triggers.is_empty() && self.assigned_statuses.is_empty() && self.witnessed_transitions.is_empty() + && self.referenced_fields.is_empty() } /// Fold another importer's contributions into this aggregate. @@ -86,6 +92,7 @@ impl ReverseContributions { for (entity, edges) in other.witnessed_transitions { self.witnessed_transitions.entry(entity).or_default().extend(edges); } + self.referenced_fields.extend(other.referenced_fields); } } @@ -145,9 +152,8 @@ fn run_checks(mut ctx: Ctx<'_>, source: &str) -> Vec { ctx.check_duplicate_let_bindings(); ctx.check_config_undefined_references(); ctx.check_list_literal_homogeneity(); - ctx.check_qualified_default_aliases(); + ctx.check_undefined_import_aliases(); ctx.check_default_field_schemas(); - ctx.check_qualified_provides(); let mut diagnostics = apply_suppressions(ctx.diagnostics, source); // Deterministic ordering: the analysis passes iterate `HashMap`s, whose @@ -180,7 +186,7 @@ pub fn analyse_with_external_refs( external_refs: &HashSet, ) -> crate::diagnostic::AnalyseResult { let diagnostics = analyze_with_external_refs(module, source, external_refs); - let findings = find_process_issues(module, None, None); + let findings = find_process_issues(module, None, None, None); crate::diagnostic::AnalyseResult { diagnostics, findings, @@ -200,6 +206,7 @@ pub fn analyse_with_cross_module( ambiguous_imports: &AmbiguousImports, reverse: &ReverseContributions, imported_referenced_triggers: &HashMap>, + imported_entity_statuses: &HashMap>, ) -> crate::diagnostic::AnalyseResult { let diagnostics = analyze_with_cross_module( module, @@ -212,7 +219,12 @@ pub fn analyse_with_cross_module( reverse, imported_referenced_triggers, ); - let findings = find_process_issues(module, Some(imported_triggers), Some(reverse)); + let findings = find_process_issues( + module, + Some(imported_triggers), + Some(reverse), + Some(imported_entity_statuses), + ); crate::diagnostic::AnalyseResult { diagnostics, findings, @@ -300,13 +312,15 @@ fn find_process_issues( module: &Module, imported_triggers: Option<&HashMap>>, reverse: Option<&ReverseContributions>, + imported_statuses: Option<&HashMap>>, ) -> Vec { let empty = HashSet::new(); + let no_statuses = HashMap::new(); let mut ctx = Ctx::new(module, &empty, None, imported_triggers, None); ctx.reverse_contributions = reverse; let info = EntityInfo::from_module(module); ctx.collect_process_findings(&info); - ctx.collect_conflict_findings(&info); + ctx.collect_conflict_findings(&info, imported_statuses.unwrap_or(&no_statuses)); ctx.collect_invariant_findings(&info); let mut findings = std::mem::take(&mut ctx.findings); // Deterministic ordering (#71): findings carry no source span, so order by @@ -1641,8 +1655,27 @@ impl Ctx<'_> { } } - fn collect_conflict_findings(&mut self, info: &EntityInfo<'_>) { - let status_by_entity = info.status_by_entity(); + fn collect_conflict_findings( + &mut self, + info: &EntityInfo<'_>, + imported_statuses: &HashMap>, + ) { + // Conflict attribution resolves a rule's entity from the status values it + // reads and writes, so an importer rule acting on an imported entity needs + // that entity's status vocabulary in scope. Merge the imported statuses in + // for *this* pass only — the lifecycle checks stay local, so imported + // entities are not re-analysed in the importer. A local declaration wins on + // a name clash. + let local = info.status_by_entity(); + let mut status_by_entity: HashMap<&str, HashSet<&str>> = HashMap::new(); + for (k, v) in &local { + status_by_entity.insert(*k, v.iter().copied().collect()); + } + for (ent, statuses) in imported_statuses { + status_by_entity + .entry(ent.as_str()) + .or_insert_with(|| statuses.iter().map(String::as_str).collect()); + } if status_by_entity.is_empty() { return; @@ -1664,39 +1697,37 @@ impl Ctx<'_> { }; // Conflict detection resolves entities by name matching against // status_by_entity, not through binding types from when clauses. - let binding_types = collect_rule_binding_types(rule, &HashMap::new()); + let binding_types = collect_rule_binding_types(rule, &HashMap::<&str, ()>::new()); let mut trigger_kind = ConflictTriggerKind::Unknown; let mut requires_statuses: HashMap> = HashMap::new(); let mut ensures_statuses: HashMap = HashMap::new(); - for item in &rule.items { - let BlockItemKind::Clause { keyword, value } = &item.kind else { - continue; - }; - match keyword.as_str() { - "when" => { - trigger_kind = classify_trigger(value); - } - "requires" => { - collect_requires_statuses_for_conflict( - value, - &binding_types, - &status_by_entity, - &mut requires_statuses, - ); - } - "ensures" => { - collect_ensures_statuses_for_conflict( - value, - &binding_types, - &status_by_entity, - &mut ensures_statuses, - ); - } - _ => {} + // Descend into `if`/`else` and `for` bodies so a conditional effect + // nested in a branch still counts toward conflict detection; a + // top-level-only walk let a branch-nested `ensures` hide a conflict. + for_each_rule_clause(&rule.items, &mut |keyword, value| match keyword { + "when" => { + trigger_kind = classify_trigger(value); + } + "requires" => { + collect_requires_statuses_for_conflict( + value, + &binding_types, + &status_by_entity, + &mut requires_statuses, + ); } - } + "ensures" => { + collect_ensures_statuses_for_conflict( + value, + &binding_types, + &status_by_entity, + &mut ensures_statuses, + ); + } + _ => {} + }); conflict_rules.push(ConflictRule { name: rule_name, @@ -1800,46 +1831,43 @@ impl Ctx<'_> { let mut field_sets = HashSet::new(); let mut requires = Vec::new(); - for item in &rule.items { - let BlockItemKind::Clause { keyword, value } = &item.kind else { - continue; - }; - match keyword.as_str() { - "ensures" => { - collect_rule_effects( - value, - &binding_types, - &status_by_entity, - &field_types, - &mut status_sets, - &mut field_sets, - ); - } - "requires" => { - collect_requires_conditions( - value, - &binding_types, - &binding_map, - &mut |binding, field, val| { - let entity = resolve_binding_entity( - binding, - None, - &binding_types, - &binding_map_for_types, - ); - if let Some(e) = entity { - requires.push(( - e.to_string(), - field.to_string(), - val.to_string(), - )); - } - }, - ); - } - _ => {} + // Descend into `if`/`else` and `for` bodies so branch-nested effects + // and guards count toward the rule's effect set. + for_each_rule_clause(&rule.items, &mut |keyword, value| match keyword { + "ensures" => { + collect_rule_effects( + value, + &binding_types, + &status_by_entity, + &field_types, + &mut status_sets, + &mut field_sets, + ); } - } + "requires" => { + collect_requires_conditions( + value, + &binding_types, + &binding_map, + &mut |binding, field, val| { + let entity = resolve_binding_entity( + binding, + None, + &binding_types, + &binding_map_for_types, + ); + if let Some(e) = entity { + requires.push(( + e.to_string(), + field.to_string(), + val.to_string(), + )); + } + }, + ); + } + _ => {} + }); rule_effects.push(RuleEffect { name: rule_name, @@ -2589,9 +2617,9 @@ fn collect_created_field_assignments<'a>( } } -fn collect_rule_binding_types<'a>( +fn collect_rule_binding_types<'a, V>( rule: &'a BlockDecl, - status_by_entity: &HashMap<&str, (Vec<&Ident>, HashSet<&str>)>, + status_by_entity: &HashMap<&str, V>, ) -> HashMap<&'a str, &'a str> { let mut types = HashMap::new(); for item in &rule.items { @@ -2606,9 +2634,9 @@ fn collect_rule_binding_types<'a>( types } -fn collect_binding_types_from_expr<'a>( +fn collect_binding_types_from_expr<'a, V>( expr: &'a Expr, - status_by_entity: &HashMap<&str, (Vec<&Ident>, HashSet<&str>)>, + status_by_entity: &HashMap<&str, V>, out: &mut HashMap<&'a str, &'a str>, ) { match expr { @@ -2652,7 +2680,7 @@ fn collect_command_param_types<'a, V>( let params: Vec> = args .iter() .map(|arg| match arg { - CallArg::Named(named) => match &named.value { + CallArg::Named(named) => match unwrap_type_refinement(&named.value) { Expr::Ident(val) if status_by_entity.contains_key(val.name.as_str()) => { @@ -3275,15 +3303,19 @@ impl Ctx<'_> { } } - // Check rule type references (when clauses, ensures entity references) - for rule in self.blocks(BlockKind::Rule) { - for item in &rule.items { - let BlockItemKind::Clause { keyword, value } = &item.kind else { - continue; - }; + // Check rule type references (when clauses, ensures entity references). + // Descend into `if`/`else` and `for` bodies so a type reference nested in + // a branch is checked, not just top-level clauses. + let rules: Vec<_> = self.blocks(BlockKind::Rule).collect(); + for rule in rules { + let mut refs = Vec::new(); + for_each_rule_clause(&rule.items, &mut |keyword, value| { if keyword == "when" || keyword == "ensures" || keyword == "requires" { - self.check_type_refs_in_rule_expr(value, &known); + refs.push(value); } + }); + for value in refs { + self.check_type_refs_in_rule_expr(value, &known); } } } @@ -3686,7 +3718,12 @@ fn extract_trigger_refs(expr: &Expr) -> Vec> { impl Ctx<'_> { fn check_unused_fields(&mut self) { - let accessed = self.collect_all_accessed_field_names(); + let mut accessed = self.collect_all_accessed_field_names(); + // A field referenced only by an importer (`alias/Entity.field`) is used, + // even though the reference lives in another module. + if let Some(rev) = self.reverse_contributions { + accessed.extend(rev.referenced_fields.iter().map(String::as_str)); + } for d in &self.module.declarations { let block = match d { @@ -3895,6 +3932,139 @@ fn collect_idents_from_expr<'a>(expr: &'a Expr, out: &mut HashSet<&'a str>) { } } +/// Collect field names an expression references through a qualified access +/// `alias/Entity.field`. Alias-aware, unlike `collect_accessed_fields_from_expr`, +/// so a reference through a different alias contributes nothing (contributions +/// must stay alias-scoped for cross-module aggregation to be sound). Recurses +/// through the same expression shapes as the module-local collector. +fn collect_qualified_field_refs<'a>(expr: &'a Expr, alias: &str, out: &mut HashSet<&'a str>) { + match expr { + Expr::MemberAccess { object, field, .. } | Expr::OptionalAccess { object, field, .. } => { + if let Expr::QualifiedName(q) = object.as_ref() { + if q.qualifier.as_deref() == Some(alias) { + out.insert(&field.name); + } + } + collect_qualified_field_refs(object, alias, out); + } + Expr::Call { function, args, .. } => { + collect_qualified_field_refs(function, alias, out); + for a in args { + match a { + CallArg::Positional(e) => collect_qualified_field_refs(e, alias, out), + CallArg::Named(n) => collect_qualified_field_refs(&n.value, alias, out), + } + } + } + Expr::BinaryOp { left, right, .. } + | Expr::Comparison { left, right, .. } + | Expr::LogicalOp { left, right, .. } + | Expr::Pipe { left, right, .. } + | Expr::NullCoalesce { left, right, .. } + | Expr::In { element: left, collection: right, .. } + | Expr::NotIn { element: left, collection: right, .. } => { + collect_qualified_field_refs(left, alias, out); + collect_qualified_field_refs(right, alias, out); + } + Expr::Not { operand, .. } + | Expr::Exists { operand, .. } + | Expr::NotExists { operand, .. } + | Expr::TypeOptional { inner: operand, .. } => { + collect_qualified_field_refs(operand, alias, out); + } + Expr::Where { source, condition, .. } + | Expr::With { source, predicate: condition, .. } => { + collect_qualified_field_refs(source, alias, out); + collect_qualified_field_refs(condition, alias, out); + } + Expr::WhenGuard { action, condition, .. } => { + collect_qualified_field_refs(action, alias, out); + collect_qualified_field_refs(condition, alias, out); + } + Expr::Binding { value, .. } | Expr::LetExpr { value, .. } | Expr::Lambda { body: value, .. } => { + collect_qualified_field_refs(value, alias, out); + } + Expr::TransitionsTo { subject, new_state, .. } + | Expr::Becomes { subject, new_state, .. } => { + collect_qualified_field_refs(subject, alias, out); + collect_qualified_field_refs(new_state, alias, out); + } + Expr::Conditional { branches, else_body, .. } => { + for b in branches { + collect_qualified_field_refs(&b.condition, alias, out); + collect_qualified_field_refs(&b.body, alias, out); + } + if let Some(body) = else_body { + collect_qualified_field_refs(body, alias, out); + } + } + Expr::For { collection, filter, body, .. } => { + collect_qualified_field_refs(collection, alias, out); + if let Some(f) = filter { + collect_qualified_field_refs(f, alias, out); + } + collect_qualified_field_refs(body, alias, out); + } + Expr::SetLiteral { elements, .. } | Expr::ListLiteral { elements, .. } => { + for e in elements { + collect_qualified_field_refs(e, alias, out); + } + } + Expr::ObjectLiteral { fields, .. } => { + for f in fields { + collect_qualified_field_refs(&f.value, alias, out); + } + } + Expr::Block { items, .. } => { + for item in items { + collect_qualified_field_refs(item, alias, out); + } + } + _ => {} + } +} + +fn collect_qualified_field_refs_from_item<'a>( + kind: &'a BlockItemKind, + alias: &str, + out: &mut HashSet<&'a str>, +) { + match kind { + BlockItemKind::Clause { value, .. } + | BlockItemKind::Assignment { value, .. } + | BlockItemKind::ParamAssignment { value, .. } + | BlockItemKind::Let { value, .. } + | BlockItemKind::PathAssignment { value, .. } + | BlockItemKind::InvariantBlock { body: value, .. } + | BlockItemKind::FieldWithWhen { value, .. } => { + collect_qualified_field_refs(value, alias, out); + } + BlockItemKind::ForBlock { collection, filter, items, .. } => { + collect_qualified_field_refs(collection, alias, out); + if let Some(f) = filter { + collect_qualified_field_refs(f, alias, out); + } + for item in items { + collect_qualified_field_refs_from_item(&item.kind, alias, out); + } + } + BlockItemKind::IfBlock { branches, else_items } => { + for b in branches { + collect_qualified_field_refs(&b.condition, alias, out); + for item in &b.items { + collect_qualified_field_refs_from_item(&item.kind, alias, out); + } + } + if let Some(items) = else_items { + for item in items { + collect_qualified_field_refs_from_item(&item.kind, alias, out); + } + } + } + _ => {} + } +} + fn collect_accessed_fields_from_item<'a>(kind: &'a BlockItemKind, out: &mut HashSet<&'a str>) { match kind { BlockItemKind::Clause { value, .. } @@ -4350,6 +4520,15 @@ fn collect_uppercase_idents_from_expr<'a>(expr: &'a Expr, out: &mut Vec Vec<(String, String)> { + collect_qref_nodes(module) + .into_iter() + .map(|r| (r.qualifier.to_string(), r.name.to_string())) + .collect() +} + +/// Every qualified reference in a module, with spans. Backs both the +/// cross-module reference map and the undefined-import-alias check. +fn collect_qref_nodes(module: &Module) -> Vec> { let mut refs = Vec::new(); for d in &module.declarations { match d { @@ -4530,13 +4709,15 @@ pub fn collect_trigger_outputs(module: &Module) -> HashSet { names.into_iter().map(str::to_string).collect() } -/// Collect every trigger name a module references: those it provides or emits -/// (`collect_trigger_outputs`) plus those its rules listen for in `when:` -/// clauses. Used by multi-file checking to validate a qualified `provides:` -/// entry against the aliased module — a trigger the module never mentions is a -/// resolution error at the entry (#72). +/// Collect every name a module *offers* to importers: declared type names +/// (`collect_declared_names`), plus every trigger name it references — provided, +/// emitted (`collect_trigger_outputs`), or listened for in `when:` clauses. +/// Used by multi-file checking to validate a qualified reference `alias/Name` +/// against the aliased module — a name it never mentions is a resolution error +/// at the reference (#72, and the name-existence audit). pub fn collect_referenced_trigger_names(module: &Module) -> HashSet { let mut names = collect_trigger_outputs(module); + names.extend(collect_declared_names(module)); for d in &module.declarations { let Decl::Block(b) = d else { continue }; if b.kind != BlockKind::Rule { @@ -4570,12 +4751,14 @@ pub fn collect_reverse_contributions<'a>( let imported_info = EntityInfo::from_module(imported); let status_by_entity = imported_info.status_by_entity(); - // Command → positional parameter entity types. Two sources contribute a + // Command → positional parameter entity types. Three sources contribute a // parameter typed to a status-bearing imported entity: // - the imported module's surface `provides:` (`Trigger(b: Entity)`), - // typing a binding the importer subscribes to across the boundary; and + // typing a binding the importer subscribes to across the boundary; // - the importer's OWN surface `provides:`, where a parameter is typed to - // a qualified imported entity inline or via a `context` binding (#65). + // a qualified imported entity inline or via a `context` binding (#65); and + // - the imported module's rule emissions (`ensures: Event(p: b)`), where + // the emitting rule's own trigger types `b` (#77). let mut command_param_types: HashMap<&str, Vec>> = HashMap::new(); for b in module_blocks(imported, BlockKind::Surface) { for item in &b.items { @@ -4589,6 +4772,7 @@ pub fn collect_reverse_contributions<'a>( collect_importer_command_param_types( importer, alias, &status_by_entity, &mut command_param_types, ); + collect_emitted_event_param_types(imported, &status_by_entity, &mut command_param_types); // 1. Provided triggers: `provides: alias/Trigger(...)` in importer surfaces. for b in module_blocks(importer, BlockKind::Surface) { @@ -4602,21 +4786,51 @@ pub fn collect_reverse_contributions<'a>( } // 2 & 3. Qualified creation and witnessed transitions from importer rules. + // Descend into `if`/`else` and `for` bodies so a creation nested in a branch + // is seen, not just top-level ensures (the #58 traversal fix). for rule in module_blocks(importer, BlockKind::Rule) { - for item in &rule.items { - if let BlockItemKind::Clause { keyword, value } = &item.kind { - if keyword == "ensures" { - collect_qualified_created( - value, alias, &status_by_entity, &mut out.assigned_statuses, - ); - } + for_each_rule_clause(&rule.items, &mut |keyword, value| { + if keyword == "ensures" { + collect_qualified_created(value, alias, &status_by_entity, &mut out.assigned_statuses); } - } + }); collect_witnessed_transition( rule, alias, &command_param_types, &status_by_entity, &mut out, ); } + // Fields the importer references through this alias (`alias/Entity.field`), + // restricted to real imported-entity fields. Credited so the imported module + // does not report a field as unused when its only reference lives across the + // boundary. + let mut imported_field_names: HashSet<&str> = HashSet::new(); + for entity in module_blocks(imported, BlockKind::Entity) + .chain(module_blocks(imported, BlockKind::ExternalEntity)) + { + for item in &entity.items { + if let BlockItemKind::Assignment { name, .. } + | BlockItemKind::FieldWithWhen { name, .. } = &item.kind + { + imported_field_names.insert(&name.name); + } + } + } + if !imported_field_names.is_empty() { + let mut qualified_refs: HashSet<&str> = HashSet::new(); + for block in &importer.declarations { + if let Decl::Block(b) = block { + for item in &b.items { + collect_qualified_field_refs_from_item(&item.kind, alias, &mut qualified_refs); + } + } + } + for f in qualified_refs { + if imported_field_names.contains(f) { + out.referenced_fields.insert(f.to_string()); + } + } + } + out } @@ -4663,38 +4877,6 @@ fn collect_qualified_provides(expr: &Expr, alias: &str, out: &mut HashSet( - expr: &'a Expr, - out: &mut Vec<(&'a str, &'a str, Span)>, -) { - match expr { - Expr::Call { function, .. } => { - if let Expr::QualifiedName(q) = function.as_ref() { - if let Some(qualifier) = q.qualifier.as_deref() { - out.push((qualifier, q.name.as_str(), q.span)); - } - } - } - Expr::Block { items, .. } => { - for item in items { - collect_qualified_provides_refs(item, out); - } - } - Expr::WhenGuard { action, .. } => collect_qualified_provides_refs(action, out), - Expr::Conditional { branches, else_body, .. } => { - for b in branches { - collect_qualified_provides_refs(&b.body, out); - } - if let Some(body) = else_body { - collect_qualified_provides_refs(body, out); - } - } - Expr::For { body, .. } => collect_qualified_provides_refs(body, out), - _ => {} - } -} /// Augment `out` with the importer's own surface `provides:` parameter types, /// where a parameter is typed to a status-bearing imported entity — inline @@ -4729,8 +4911,109 @@ fn collect_importer_command_param_types<'a>( } } +/// Add rule-emitted events as a binding-type source (#77). For an imported rule +/// `ensures: Event(param: b)`, the event's parameter takes the type the emitting +/// rule's own trigger gives `b`, mapped positionally so a positional subscriber +/// binding resolves. This lets a consumer subscribing to a rule-emitted event +/// across a module boundary type its binding. +fn collect_emitted_event_param_types<'a>( + imported: &'a Module, + status_by_entity: &HashMap<&'a str, HashSet<&'a str>>, + out: &mut HashMap<&'a str, Vec>>, +) { + // The emitting rule's binding may be typed by the imported module's own + // surface `provides:` parameters, not only by a transition trigger — so type + // it the same way the local pass does, from those parameters (else the + // emission carries no type across the split). + let mut surface_params: HashMap<&str, Vec>> = HashMap::new(); + for surface in module_blocks(imported, BlockKind::Surface) { + for item in &surface.items { + if let BlockItemKind::Clause { keyword, value } = &item.kind { + if keyword == "provides" { + collect_command_param_types(value, status_by_entity, &mut surface_params); + } + } + } + } + for rule in module_blocks(imported, BlockKind::Rule) { + let mut binding_types = collect_rule_binding_types(rule, status_by_entity); + augment_binding_types_from_commands(rule, &surface_params, &mut binding_types); + if binding_types.is_empty() { + continue; + } + for_each_rule_clause(&rule.items, &mut |keyword, value| { + if keyword == "ensures" { + collect_emission_param_types(value, &binding_types, out); + } + }); + } +} + +/// From an `ensures:` value, record each leading `Event(args)` emission's +/// positional parameter types, resolved from the emitting rule's binding types. +fn collect_emission_param_types<'a>( + expr: &'a Expr, + binding_types: &HashMap<&'a str, &'a str>, + out: &mut HashMap<&'a str, Vec>>, +) { + match expr { + Expr::Call { function, args, .. } => { + if let Expr::Ident(event) = function.as_ref() { + let params: Vec> = args + .iter() + .map(|arg| { + let val = match arg { + CallArg::Named(n) => &n.value, + CallArg::Positional(e) => e, + }; + match val { + Expr::Ident(v) => binding_types.get(v.name.as_str()).copied(), + _ => None, + } + }) + .collect(); + if params.iter().any(Option::is_some) { + out.entry(&event.name).or_insert(params); + } + } + } + Expr::Block { items, .. } => { + for item in items { + collect_emission_param_types(item, binding_types, out); + } + } + Expr::Conditional { branches, else_body, .. } => { + for b in branches { + collect_emission_param_types(&b.body, binding_types, out); + } + if let Some(body) = else_body { + collect_emission_param_types(body, binding_types, out); + } + } + _ => {} + } +} + /// Record a surface `context`/`facing` binding typed to a qualified imported /// entity: `name: alias/Entity` maps `name` to the imported entity. +/// Peel transparent type-refinement wrappers so a resolver sees the underlying +/// type expression. A binding's declared type may be refined with `where` +/// (`Expr::Where`) or `with` (`Expr::With`), or marked optional (`Expr::TypeOptional`); +/// none of these change which entity the binding refers to. Any resolver that +/// matches `QualifiedName`/`Ident` to type a binding must unwrap first, or a +/// refined type silently fails to resolve (the #76 family). One helper so the +/// unwrap can't be applied at one site and forgotten at its siblings. +fn unwrap_type_refinement(expr: &Expr) -> &Expr { + let mut cur = expr; + loop { + cur = match cur { + Expr::Where { source, .. } | Expr::With { source, .. } => source, + Expr::TypeOptional { inner, .. } => inner, + other => return other, + }; + } +} + fn qualified_context_binding<'a>( expr: &'a Expr, alias: &str, @@ -4739,7 +5022,10 @@ fn qualified_context_binding<'a>( ) { match expr { Expr::Binding { name, value, .. } => { - if let Expr::QualifiedName(q) = value.as_ref() { + // `context b: alias/E where …` (and `with …`, and `alias/E?`) must + // type `b` exactly as the bare `context b: alias/E` does (#76 family). + let type_expr = unwrap_type_refinement(value.as_ref()); + if let Expr::QualifiedName(q) = type_expr { if q.qualifier.as_deref() == Some(alias) { if let Some((entity, _)) = status_by_entity.get_key_value(q.name.as_str()) { out.insert(&name.name, entity); @@ -4774,7 +5060,7 @@ fn collect_provides_param_types<'a>( CallArg::Positional(Expr::Ident(id)) => { context_types.get(id.name.as_str()).copied() } - CallArg::Named(n) => match &n.value { + CallArg::Named(n) => match unwrap_type_refinement(&n.value) { Expr::QualifiedName(q) if q.qualifier.as_deref() == Some(alias) => { status_by_entity.get_key_value(q.name.as_str()).map(|(k, _)| *k) } @@ -4924,6 +5210,12 @@ fn collect_witnessed_transition( { binding_entity.insert(name.name.as_str(), entity); trigger_source.insert(name.name.as_str(), source); + } else if let Some(entity) = + qualified_temporal_trigger_entity(inner, alias, status_by_entity) + { + // Temporal/relational trigger: type the binding, but let the + // `requires` clause supply the `from` (no implicit source). + binding_entity.insert(name.name.as_str(), entity); } } _ => {} @@ -4940,19 +5232,19 @@ fn collect_witnessed_transition( for (binding, source) in &trigger_source { froms.entry(binding).or_default().insert(source); } - for item in &rule.items { - let BlockItemKind::Clause { keyword, value } = &item.kind else { - continue; - }; - let target = match keyword.as_str() { + // Descend into `if`/`else` and `for` bodies so a guard or assignment nested + // in a branch is seen, not just top-level clauses (the #58 traversal fix, + // applied here in the reverse channel). + for_each_rule_clause(&rule.items, &mut |keyword, value| { + let target = match keyword { "requires" => &mut froms, "ensures" => &mut tos, - _ => continue, + _ => return, }; collect_binding_status_eq(value, &mut |binding, status| { target.entry(binding).or_default().insert(status); }); - } + }); for (binding, entity) in &binding_entity { let Some(valid) = status_by_entity.get(*entity) else { @@ -5018,6 +5310,41 @@ fn qualified_transition_trigger<'a>( Some((*entity, source)) } +/// Resolve the imported entity that a temporal or relational trigger observes, +/// e.g. `m: alias/E.expires_at <= now`. Unlike `becomes`/`transitions_to`, such a +/// trigger carries no implicit `from` state, so the binding is typed but no source +/// status is contributed; the rule's `requires` clause supplies the `from`. Without +/// this, a temporal-triggered transition over an imported entity is never credited +/// back across the split, so the imported entity looks stuck (false `deadlock`, +/// `noExit`, `unreachableValue`). +fn qualified_temporal_trigger_entity<'a>( + expr: &'a Expr, + alias: &str, + status_by_entity: &HashMap<&'a str, HashSet<&'a str>>, +) -> Option<&'a str> { + fn member_entity<'a>( + e: &'a Expr, + alias: &str, + status_by_entity: &HashMap<&'a str, HashSet<&'a str>>, + ) -> Option<&'a str> { + let Expr::MemberAccess { object, .. } = e else { + return None; + }; + let Expr::QualifiedName(q) = object.as_ref() else { + return None; + }; + if q.qualifier.as_deref() != Some(alias) { + return None; + } + status_by_entity.get_key_value(q.name.as_str()).map(|(k, _)| *k) + } + match expr { + Expr::Comparison { left, right, .. } => member_entity(left, alias, status_by_entity) + .or_else(|| member_entity(right, alias, status_by_entity)), + _ => None, + } +} + /// From a local `when: b: Entity.status becomes state` (or `transitions_to`) /// trigger, return the binding, the entity, and the state the entity is in when /// the rule fires — the start state of the transition the rule then performs @@ -5089,7 +5416,32 @@ pub fn collect_entity_field_schemas(module: &Module) -> HashMap) { +/// Entity name → its declared status values. The cross-module counterpart of +/// [`collect_entity_field_schemas`]: it gives an importer's conflict pass the +/// status vocabulary of the entities it imports, so two importer rules acting on +/// an imported entity can be attributed to it and compared for conflict. +pub fn collect_entity_status_schemas(module: &Module) -> HashMap> { + EntityInfo::from_module(module) + .status_by_entity() + .into_iter() + .map(|(name, statuses)| { + ( + name.to_string(), + statuses.into_iter().map(|s| s.to_string()).collect(), + ) + }) + .collect() +} + +/// A qualified reference `qualifier/name` (or the `alias.Type` dot form) with +/// the span to anchor a diagnostic at. +struct QRef<'a> { + qualifier: &'a str, + name: &'a str, + span: Span, +} + +fn collect_qrefs_from_item<'a>(kind: &'a BlockItemKind, out: &mut Vec>) { match kind { BlockItemKind::Clause { value, .. } | BlockItemKind::Assignment { value, .. } @@ -5132,8 +5484,8 @@ fn collect_qrefs_from_item(kind: &BlockItemKind, out: &mut Vec<(String, String)> } BlockItemKind::ContractsClause { entries } => { for e in entries { - if let Some(ref qualifier) = e.qualifier { - out.push((qualifier.clone(), e.name.name.clone())); + if let Some(qualifier) = &e.qualifier { + out.push(QRef { qualifier, name: &e.name.name, span: e.name.span }); } } } @@ -5143,11 +5495,11 @@ fn collect_qrefs_from_item(kind: &BlockItemKind, out: &mut Vec<(String, String)> } } -fn collect_qrefs_from_expr(expr: &Expr, out: &mut Vec<(String, String)>) { +fn collect_qrefs_from_expr<'a>(expr: &'a Expr, out: &mut Vec>) { match expr { Expr::QualifiedName(q) => { - if let Some(ref qualifier) = q.qualifier { - out.push((qualifier.clone(), q.name.clone())); + if let Some(qualifier) = &q.qualifier { + out.push(QRef { qualifier, name: &q.name, span: q.span }); } } Expr::MemberAccess { object, field, .. } @@ -5155,7 +5507,7 @@ fn collect_qrefs_from_expr(expr: &Expr, out: &mut Vec<(String, String)>) { // Detect alias.TypeName pattern (e.g. core.EntityMap in exposes) if let Expr::Ident(id) = object.as_ref() { if starts_uppercase(&field.name) { - out.push((id.name.clone(), field.name.clone())); + out.push(QRef { qualifier: &id.name, name: &field.name, span: id.span.merge(field.span) }); } } collect_qrefs_from_expr(object, out); @@ -5498,14 +5850,16 @@ impl Ctx<'_> { } impl Ctx<'_> { - /// A qualified type name in a `default` (`default alias/Type x = ...`) must - /// reference a module brought into scope by `use "..." as alias`. Keeps - /// parity with the TypeScript `findDefaultTypeReferenceIssues` alias check. - /// Validate qualified `provides: alias/Trigger` entries at the entry (#72). - /// An `alias` that matches no `use` import is an error; a trigger name the - /// aliased module never references is a warning, but only when that module - /// is in the check set (a target outside it is unknowable by design). - fn check_qualified_provides(&mut self) { + + /// A qualified reference `alias/Name` at any site — a `when:` trigger or + /// entity subject, a `provides:` entry, a surface `context`, an inline + /// parameter type, a field type, a `.created(...)` call, a `default`, a + /// contract clause — must name a module brought into scope by `use "..." as + /// alias`. A qualifier matching no declared alias is a locally-knowable typo + /// and is diagnosed at the reference, single-file and multi-file alike + /// (#78 and the wider sites audit). One pass over every qualified reference + /// rather than a separate check per site. + fn check_undefined_import_aliases(&mut self) { let aliases: HashSet<&str> = self .module .declarations @@ -5516,76 +5870,56 @@ impl Ctx<'_> { }) .collect(); - let mut entries: Vec<(&str, &str, Span)> = Vec::new(); - for surface in self.blocks(BlockKind::Surface) { - for item in &surface.items { - if let BlockItemKind::Clause { keyword, value } = &item.kind { - if keyword == "provides" { - collect_qualified_provides_refs(value, &mut entries); - } + let mut refs = collect_qref_nodes(self.module); + // A `default alias/Type` reference's qualifier sits on the declaration, + // not inside its value expression, so add it explicitly. + for d in &self.module.declarations { + if let Decl::Default(def) = d { + if let (Some(a), Some(t)) = (&def.type_alias, &def.type_name) { + refs.push(QRef { + qualifier: &a.name, + name: &t.name, + span: a.span.merge(t.span), + }); } } } - for (qualifier, name, span) in entries { - if !aliases.contains(qualifier) { + for r in refs { + if !aliases.contains(r.qualifier) { self.push( Diagnostic::error( - span, + r.span, format!( - "Provides entry '{qualifier}/{name}' uses unknown import alias '{qualifier}'." + "Reference '{}/{}' uses unknown import alias '{}'.", + r.qualifier, r.name, r.qualifier ), ) - .with_code("allium.provides.undefinedImportedAlias"), + .with_code("allium.reference.undefinedImportedAlias"), ); - } else if let Some(triggers) = self + } else if let Some(offered) = self .imported_referenced_triggers - .and_then(|m| m.get(qualifier)) + .and_then(|m| m.get(r.qualifier)) { - if !triggers.contains(name) { + // The alias resolves into the check set: the name must be one the + // aliased module offers (a declared type or a referenced trigger). + // A target outside the check set is unknowable and left alone. + if !offered.contains(r.name) { self.push( Diagnostic::warning( - span, + r.span, format!( - "Provides entry '{qualifier}/{name}' names trigger '{name}', which imported module '{qualifier}' does not use." + "Reference '{}/{}' names '{}', which imported module '{}' does not define.", + r.qualifier, r.name, r.name, r.qualifier ), ) - .with_code("allium.provides.unknownTrigger"), + .with_code("allium.reference.unknownName"), ); } } } } - fn check_qualified_default_aliases(&mut self) { - let mut aliases: HashSet<&str> = HashSet::new(); - for d in &self.module.declarations { - if let Decl::Use(u) = d { - if let Some(alias) = &u.alias { - aliases.insert(alias.name.as_str()); - } - } - } - for d in &self.module.declarations { - let Decl::Default(def) = d else { continue }; - let (Some(alias), Some(type_name)) = (&def.type_alias, &def.type_name) else { - continue; - }; - if !aliases.contains(alias.name.as_str()) { - self.push( - Diagnostic::error( - alias.span.merge(type_name.span), - format!( - "Type reference '{}/{}' uses unknown import alias '{}'.", - alias.name, type_name.name, alias.name - ), - ) - .with_code("allium.default.undefinedImportedAlias"), - ); - } - } - } - /// Validates `default Type x = { ... }` object literals against the /// declared schema of `Type` (and, recursively, of nested value/entity /// types). Catches drift — an object-literal field that the entity no @@ -5967,52 +6301,13 @@ impl Ctx<'_> { collect_bound_names(value, &mut bound); } - // Collect let bindings - for item in &rule.items { - if let BlockItemKind::Let { name, .. } = &item.kind { - bound.insert(&name.name); - } - } - - // Check requires/ensures for unbound references - for item in &rule.items { - let BlockItemKind::Clause { keyword, value } = &item.kind else { - continue; - }; - if keyword != "requires" && keyword != "ensures" { - continue; - } - check_unbound_roots(value, &bound, rule_name, &mut self.diagnostics); - } - - // Check for-block and if-block items - for item in &rule.items { - match &item.kind { - BlockItemKind::ForBlock { - binding, - items, - .. - } => { - let mut inner_bound = bound.clone(); - match binding { - ForBinding::Single(id) => { inner_bound.insert(&id.name); } - ForBinding::Destructured(ids, _) => { - for id in ids { - inner_bound.insert(&id.name); - } - } - } - for sub_item in items { - if let BlockItemKind::Clause { keyword, value } = &sub_item.kind { - if keyword == "ensures" || keyword == "requires" { - check_unbound_roots(value, &inner_bound, rule_name, &mut self.diagnostics); - } - } - } - } - _ => {} - } - } + // Check requires/ensures for unbound references, descending into + // `if`/`else` and `for` bodies. Let-bindings are collected per block + // level (so a branch-local let scopes only within that branch and a + // sibling branch can't see it), and each `for` body adds its loop + // binding. Previously only top-level and one level of `for` were + // checked, so a branch-nested unbound reference went unflagged. + check_unbound_in_items(&rule.items, &bound, rule_name, &mut self.diagnostics); // Rules with bare entity bindings (e.g. `when: state: ClerkEventState`) // have an invalid trigger form. The binding name is syntactically present @@ -6024,7 +6319,14 @@ impl Ctx<'_> { if !matches!(trigger_value.as_ref(), Expr::Ident(id) if starts_uppercase(&id.name)) { continue; } - // Find the first requires/ensures clause that references this binding + // Find the first requires/ensures clause that references this binding. + // NOTE: this only scans top-level clauses, so if the binding is + // referenced *only* inside an `if`/`for` branch the secondary + // `undefinedBinding` anchor is not emitted. This is benign today + // because the malformed trigger still raises `invalidTrigger` + // regardless, so the rule is never silently accepted. Making it + // branch-aware needs a span-carrying traversal (the diagnostic + // anchors on `check_item.span`, which `for_each_rule_clause` drops). let mut found = false; for check_item in &rule.items { let BlockItemKind::Clause { keyword: kw, value: v } = &check_item.kind else { continue }; @@ -6050,6 +6352,57 @@ impl Ctx<'_> { } } +/// Check `requires`/`ensures` clauses for references to unbound names, recursing +/// through `if`/`else` and `for` bodies. Each block level first collects its own +/// `let` names (so references resolve regardless of order and a branch-local let +/// is invisible to sibling branches and the parent), and each `for` body adds its +/// loop binding to the in-scope set. +fn check_unbound_in_items<'a>( + items: &'a [BlockItem], + parent_bound: &HashSet<&'a str>, + rule_name: &str, + diagnostics: &mut Vec, +) { + let mut bound: HashSet<&'a str> = parent_bound.clone(); + for item in items { + if let BlockItemKind::Let { name, .. } = &item.kind { + bound.insert(&name.name); + } + } + for item in items { + match &item.kind { + BlockItemKind::Clause { keyword, value } => { + if keyword == "requires" || keyword == "ensures" { + check_unbound_roots(value, &bound, rule_name, diagnostics); + } + } + BlockItemKind::IfBlock { branches, else_items } => { + for b in branches { + check_unbound_in_items(&b.items, &bound, rule_name, diagnostics); + } + if let Some(else_items) = else_items { + check_unbound_in_items(else_items, &bound, rule_name, diagnostics); + } + } + BlockItemKind::ForBlock { binding, items: for_items, .. } => { + let mut inner = bound.clone(); + match binding { + ForBinding::Single(id) => { + inner.insert(&id.name); + } + ForBinding::Destructured(ids, _) => { + for id in ids { + inner.insert(&id.name); + } + } + } + check_unbound_in_items(for_items, &inner, rule_name, diagnostics); + } + _ => {} + } + } +} + fn collect_bound_names<'a>(expr: &'a Expr, out: &mut HashSet<&'a str>) { match expr { Expr::Binding { name, .. } => { @@ -6991,6 +7344,26 @@ mod tests { assert!(has_finding(&r, "conflict")); } + #[test] + fn conflict_detected_when_effect_nested_in_branch() { + // The conflicting `ensures` sits inside an `if`/`else`, so a + // top-level-only walk of the rule body would miss it. The conflict must + // still be found (branch-nesting invariance for conflict detection). + let r = analyse_src( + "entity Membership {\n status: active | expired | extended\n \ + expires_at: Timestamp\n \ + transitions status {\n active -> expired\n active -> extended\n \ + terminal: expired, extended\n }\n}\n\n\ + rule AutoExpire {\n when: m: Membership.expires_at <= now\n \ + requires: m.status = active\n ensures: m.status = expired\n}\n\n\ + rule ManualExtend {\n when: AdminExtends(admin, membership, flag)\n \ + requires: membership.status = active\n \ + if flag:\n ensures: membership.status = extended\n \ + else:\n ensures: membership.status = extended\n}\n", + ); + assert!(has_finding(&r, "conflict")); + } + #[test] fn no_conflict_actor_choice() { let r = analyse_src( @@ -8030,14 +8403,14 @@ surface AccountManagement { let ds = analyze_src( "use \"./p.allium\" as gp\n\ndefault gp/Policy my_policy = { id: \"x\" }", ); - assert!(!has_code(&ds, "allium.default.undefinedImportedAlias")); + assert!(!has_code(&ds, "allium.reference.undefinedImportedAlias")); } #[test] fn qualified_default_unknown_alias_flagged() { - // `zz` is not imported — must be flagged, matching the TS analyzer. + // `zz` is not imported — must be flagged by the unified reference check. let ds = analyze_src("default zz/Policy my_policy = { id: \"x\" }"); - assert!(has_code(&ds, "allium.default.undefinedImportedAlias")); + assert!(has_code(&ds, "allium.reference.undefinedImportedAlias")); } // -- Default field-schema validation (drift) + rule 14c -- @@ -8218,6 +8591,21 @@ surface AccountManagement { assert!(rc.is_empty()); } + #[test] + fn reverse_contributions_credit_qualified_field_reference() { + let imported = + module_of("entity Ticket {\n status: open | closed\n due_at: Timestamp\n}\n"); + let importer = module_of( + "use \"./t.allium\" as tickets\nrule Sweep {\n when: t: tickets/Ticket.due_at <= now\n requires: t.status = open\n ensures: t.status = closed\n}\n", + ); + // `due_at` is referenced only across the boundary, so it must be credited + // for the matching alias and left alone for a different one. + let rc = collect_reverse_contributions(&importer, "tickets", &imported); + assert!(rc.referenced_fields.contains("due_at")); + let other = collect_reverse_contributions(&importer, "other", &imported); + assert!(!other.referenced_fields.contains("due_at")); + } + #[test] fn reverse_contributions_filter_undeclared_status() { let imported = module_of("entity Ticket {\n status: open | closed\n}\n"); diff --git a/crates/allium-parser/src/lib.rs b/crates/allium-parser/src/lib.rs index 7b7cdca..bc35d53 100644 --- a/crates/allium-parser/src/lib.rs +++ b/crates/allium-parser/src/lib.rs @@ -8,7 +8,8 @@ pub mod span; pub use analysis::{ analyze, analyze_with_cross_module, analyze_with_external_refs, analyse, analyse_with_cross_module, analyse_with_external_refs, collect_all_referenced_idents, - collect_declared_names, collect_entity_field_schemas, collect_qualified_references, + collect_declared_names, collect_entity_field_schemas, collect_entity_status_schemas, + collect_qualified_references, collect_referenced_trigger_names, collect_reverse_contributions, collect_trigger_outputs, AmbiguousImports, ReverseContributions, }; diff --git a/crates/allium/src/main.rs b/crates/allium/src/main.rs index 4e55f20..07a9dbc 100644 --- a/crates/allium/src/main.rs +++ b/crates/allium/src/main.rs @@ -210,6 +210,10 @@ struct CrossModuleContext { /// creations, provides and witnessed transitions). Keyed by the imported /// (target) module, aggregated across all its importers in the check set. reverse_contributions: HashMap, + /// Per-file: imported entity name → its declared status values, flattened + /// across every `use` alias whose target is in the check set. Lets the + /// importer's conflict pass attribute a rule to an imported entity. + imported_entity_statuses: HashMap>>, } /// Shared loop for commands that process multiple .allium files. @@ -220,7 +224,7 @@ struct CrossModuleContext { fn run_multi_file( command: &str, args: &[String], - analyse_file: impl Fn(&Path, &str, &allium_parser::ParseResult, &SourceMap, &HashSet, &HashSet, &HashMap>, &HashMap>>, &AmbiguousImports, &ReverseContributions, &HashMap>) -> FileResult, + analyse_file: impl Fn(&Path, &str, &allium_parser::ParseResult, &SourceMap, &HashSet, &HashSet, &HashMap>, &HashMap>>, &AmbiguousImports, &ReverseContributions, &HashMap>, &HashMap>) -> FileResult, ) -> ExitCode { let files = resolve_files(args); if files.is_empty() { @@ -265,7 +269,8 @@ fn run_multi_file( let ambiguous = ctx.ambiguous_imports.get(&key).unwrap_or(&no_ambiguity); let reverse = ctx.reverse_contributions.get(&key).unwrap_or(&no_reverse); let referenced = ctx.imported_referenced_triggers.get(&key).cloned().unwrap_or_default(); - let file_result = analyse_file(&pf.path, &pf.source, &pf.result, &source_map, &refs, &use_paths, &imports, &imported_fields, ambiguous, reverse, &referenced); + let imported_statuses = ctx.imported_entity_statuses.get(&key).cloned().unwrap_or_default(); + let file_result = analyse_file(&pf.path, &pf.source, &pf.result, &source_map, &refs, &use_paths, &imports, &imported_fields, ambiguous, reverse, &referenced, &imported_statuses); if file_result.has_issues { any_issues = true; @@ -329,6 +334,18 @@ fn build_cross_module_context(parsed: &[ParsedFile]) -> CrossModuleContext { }) .collect(); + // Each file's entity → status-values schema, so an importer's conflict pass + // can attribute a rule to an imported entity by the statuses it references. + let entity_status_outputs: HashMap>> = parsed + .iter() + .map(|pf| { + ( + canonical_key(&pf.path), + allium_parser::collect_entity_status_schemas(&pf.result.module), + ) + }) + .collect(); + // Pre-compute every trigger name each file references (provides, emits or // listens for), so an importing file can validate a qualified `provides:` // entry against the aliased module (#72). @@ -359,6 +376,8 @@ fn build_cross_module_context(parsed: &[ParsedFile]) -> CrossModuleContext { PathBuf, HashMap>>, > = HashMap::new(); + let mut imported_entity_statuses: HashMap>> = + HashMap::new(); let mut ambiguous_imports: HashMap = HashMap::new(); for pf in parsed { @@ -472,6 +491,22 @@ fn build_cross_module_context(parsed: &[ParsedFile]) -> CrossModuleContext { } imported_entity_fields.insert(file_key.clone(), imported_fields_for_file); + // 3c. Imported entity status vocabularies, flattened across aliases to + // entity name → status values, so the importer's conflict pass can + // attribute a rule to an imported entity by the statuses it uses. + let mut imported_statuses_for_file: HashMap> = HashMap::new(); + for target_key in alias_targets.values() { + if let Some(statuses) = entity_status_outputs.get(target_key) { + for (entity, values) in statuses { + imported_statuses_for_file + .entry(entity.clone()) + .or_default() + .extend(values.iter().cloned()); + } + } + } + imported_entity_statuses.insert(file_key.clone(), imported_statuses_for_file); + // 4. Ambiguous imports — names declared, and triggers provided or // emitted, by more than one distinct imported file. Keyed by // distinct target so that two aliases for the same file are not @@ -529,6 +564,7 @@ fn build_cross_module_context(parsed: &[ParsedFile]) -> CrossModuleContext { imported_referenced_triggers, ambiguous_imports, reverse_contributions, + imported_entity_statuses, } } @@ -542,7 +578,9 @@ fn canonical_key(path: &Path) -> PathBuf { } fn cmd_check(args: &[String]) -> ExitCode { - run_multi_file("check", args, |path, source, result, source_map, external_refs, resolved_use_paths, imported_triggers, imported_entity_fields, ambiguous_imports, reverse, referenced_triggers| { + run_multi_file("check", args, |path, source, result, source_map, external_refs, resolved_use_paths, imported_triggers, imported_entity_fields, ambiguous_imports, reverse, referenced_triggers, _imported_entity_statuses| { + // `check` emits diagnostics only, not findings, so it needs no imported + // status vocabulary (conflicts are findings, surfaced by `analyse`). let analysis = allium_parser::analyze_with_cross_module(&result.module, source, external_refs, resolved_use_paths, imported_triggers, imported_entity_fields, ambiguous_imports, reverse, referenced_triggers); let diagnostics: Vec = result .diagnostics @@ -558,8 +596,8 @@ fn cmd_check(args: &[String]) -> ExitCode { } fn cmd_analyse(args: &[String]) -> ExitCode { - run_multi_file("analyse", args, |path, source, result, source_map, external_refs, resolved_use_paths, imported_triggers, imported_entity_fields, ambiguous_imports, reverse, referenced_triggers| { - let analyse_result = allium_parser::analyse_with_cross_module(&result.module, source, external_refs, resolved_use_paths, imported_triggers, imported_entity_fields, ambiguous_imports, reverse, referenced_triggers); + run_multi_file("analyse", args, |path, source, result, source_map, external_refs, resolved_use_paths, imported_triggers, imported_entity_fields, ambiguous_imports, reverse, referenced_triggers, imported_entity_statuses| { + let analyse_result = allium_parser::analyse_with_cross_module(&result.module, source, external_refs, resolved_use_paths, imported_triggers, imported_entity_fields, ambiguous_imports, reverse, referenced_triggers, imported_entity_statuses); let diagnostics: Vec = result .diagnostics .iter() diff --git a/crates/allium/tests/cli_smoke.rs b/crates/allium/tests/cli_smoke.rs new file mode 100644 index 0000000..833fec2 --- /dev/null +++ b/crates/allium/tests/cli_smoke.rs @@ -0,0 +1,87 @@ +//! End-to-end smoke tests for the `check`/`analyse`/`parse` commands: run the +//! real binary on a written-out spec and assert the exit-code and output-shape +//! contract. These guard the CLI surface itself (JSON envelope, exit codes), +//! which the in-process analyser tests never exercise. + +use std::fs; +use std::process::Command; + +fn allium() -> Command { + Command::new(env!("CARGO_BIN_EXE_allium")) +} + +/// A throwaway spec file under the OS temp dir, removed on drop. +struct SpecFile { + path: std::path::PathBuf, +} +impl SpecFile { + fn new(tag: &str, content: &str) -> Self { + let path = std::env::temp_dir().join(format!( + "allium-smoke-{tag}-{}.allium", + std::process::id() + )); + fs::write(&path, content).unwrap(); + Self { path } + } + fn arg(&self) -> String { + self.path.to_string_lossy().into_owned() + } +} +impl Drop for SpecFile { + fn drop(&mut self) { + let _ = fs::remove_file(&self.path); + } +} + +const VALID: &str = "-- allium: 3\n\n\ + entity Job {\n status: pending | done\n transitions status { pending -> done terminal: done }\n}\n\n\ + rule CreateJob {\n when: JobRequested()\n ensures: Job.created(status: pending)\n}\n\n\ + rule Finish {\n when: j: Job.status becomes pending\n ensures: j.status = done\n}\n\n\ + surface JobIntake {\n provides:\n JobRequested()\n}\n"; + +// References an undeclared entity `Ghost`, which is an error-severity diagnostic. +const BROKEN: &str = "-- allium: 3\n\n\ + rule R {\n when: Go()\n ensures: Ghost.created(status: pending)\n}\n"; + +#[test] +fn check_valid_spec_exits_zero_with_empty_reports() { + let spec = SpecFile::new("valid", VALID); + let out = allium().arg("check").arg(spec.arg()).output().expect("spawn allium"); + assert!(out.status.success(), "expected exit 0, got {:?}", out.status); + let stdout = String::from_utf8_lossy(&out.stdout); + assert!(stdout.contains("\"command\": \"check\""), "missing command envelope: {stdout}"); + assert!(stdout.contains("\"diagnostics\": []"), "expected no diagnostics: {stdout}"); + assert!(stdout.contains("\"findings\": []"), "expected no findings: {stdout}"); +} + +#[test] +fn check_spec_with_error_exits_one_and_names_the_offender() { + let spec = SpecFile::new("broken", BROKEN); + let out = allium().arg("check").arg(spec.arg()).output().expect("spawn allium"); + assert_eq!(out.status.code(), Some(1), "an error-severity diagnostic should exit 1"); + let stdout = String::from_utf8_lossy(&out.stdout); + assert!(stdout.contains("allium.rule.undefinedTypeReference"), "expected the type-ref error: {stdout}"); + assert!(stdout.contains("\"severity\": \"error\""), "expected an error severity: {stdout}"); + assert!(stdout.contains("Ghost"), "diagnostic should name the offending reference: {stdout}"); +} + +#[test] +fn analyse_valid_spec_emits_the_json_envelope() { + let spec = SpecFile::new("analyse", VALID); + let out = allium().arg("analyse").arg(spec.arg()).output().expect("spawn allium"); + assert!(out.status.success(), "expected exit 0, got {:?}", out.status); + let stdout = String::from_utf8_lossy(&out.stdout); + for key in ["\"command\"", "\"diagnostics\"", "\"findings\""] { + assert!(stdout.contains(key), "analyse output missing {key}: {stdout}"); + } + // Output must be a single well-formed JSON document. + serde_json::from_str::(stdout.trim()) + .expect("analyse stdout should be valid JSON"); +} + +#[test] +fn parse_valid_spec_exits_zero() { + let spec = SpecFile::new("parse", VALID); + let out = allium().arg("parse").arg(spec.arg()).output().expect("spawn allium"); + assert!(out.status.success(), "expected exit 0 on a well-formed spec, got {:?}", out.status); +} diff --git a/crates/allium/tests/cross_module_lifecycle.rs b/crates/allium/tests/cross_module_lifecycle.rs index f6fb350..a503f4a 100644 --- a/crates/allium/tests/cross_module_lifecycle.rs +++ b/crates/allium/tests/cross_module_lifecycle.rs @@ -970,15 +970,15 @@ fn prop_malformed_provides_entry_is_anchored() { let ok_diags = run_case("ok", &ok); assert!( - !ok_diags.iter().any(|d| d.code == "allium.provides.undefinedImportedAlias" - || d.code == "allium.provides.unknownTrigger"), + !ok_diags.iter().any(|d| d.code == "allium.reference.undefinedImportedAlias" + || d.code == "allium.reference.unknownName"), "seed {seed}: well-formed provides drew a resolution diagnostic.\n{:?}", ok_diags.iter().map(|d| (&d.code, &d.message)).collect::>() ); let alias_diags = run_case("badalias", &bad_alias); assert!( - alias_diags.iter().any(|d| d.code == "allium.provides.undefinedImportedAlias" + alias_diags.iter().any(|d| d.code == "allium.reference.undefinedImportedAlias" && d.message.contains("nosuch")), "seed {seed}: a bad provides alias must be anchored.\n{:?}", alias_diags.iter().map(|d| (&d.code, &d.message)).collect::>() @@ -986,7 +986,7 @@ fn prop_malformed_provides_entry_is_anchored() { let trigger_diags = run_case("badtrigger", &bad_trigger); assert!( - trigger_diags.iter().any(|d| d.code == "allium.provides.unknownTrigger" + trigger_diags.iter().any(|d| d.code == "allium.reference.unknownName" && d.message.contains(&absent)), "seed {seed}: a bad provides trigger must be anchored.\n{:?}", trigger_diags.iter().map(|d| (&d.code, &d.message)).collect::>() diff --git a/crates/allium/tests/properties.rs b/crates/allium/tests/properties.rs index 1d128e9..0ad4746 100644 --- a/crates/allium/tests/properties.rs +++ b/crates/allium/tests/properties.rs @@ -208,6 +208,218 @@ fn prop_redundant_trigger_guard_is_invariant() { } } +// --------------------------------------------------------------------------- +// Branch-nesting invariance for undefined-binding detection. +// +// A reference to an unbound name must be flagged the same whether it sits at the +// top level of a rule or inside an `if`/`else` body. The undefined-binding pass +// used to walk only the top level (plus one level of `for`), so a branch-nested +// reference went silently unflagged. +// --------------------------------------------------------------------------- + +fn undefined_binding_codes(src: &str) -> Vec<&'static str> { + let mut v: Vec<&'static str> = diagnostics_of(src) + .iter() + .filter_map(|d| d.code) + .filter(|c| *c == "allium.rule.undefinedBinding") + .collect(); + v.sort_unstable(); + v +} + +// --------------------------------------------------------------------------- +// Branch-nesting invariance (generative). Wrapping a rule's `requires`/`ensures` +// in an identical `if flag: ... else: ...` is semantically a no-op, so the set of +// reports must be unchanged — across every analysis pass. A pass that still walks +// only the top level of a rule body breaks this. A fault (an undefined binding, an +// undeclared type) is injected on some seeds so the property also asserts a +// diagnostic is raised whether its clause is flat or nested. +// +// Wrapping duplicates the clause, so a per-clause diagnostic fires twice in the +// wrapped form; the invariant is therefore set-equality of report *kinds* (a +// branch gap makes a report vanish, which this still catches) rather than a +// multiset. +// --------------------------------------------------------------------------- + +/// Wrap a clause block in `depth` levels of identical `if flag: … else: …`. Both +/// branches are the same, so it is a semantic no-op at any depth. A pass that +/// descends only one level of nesting would miss a clause wrapped deeper. +fn wrap_ifelse(inner: &str, depth: u32) -> String { + if depth == 0 { + return inner.to_string(); + } + let deeper = wrap_ifelse(inner, depth - 1); + format!("if flag:\n{deeper}\nelse:\n{deeper}\n") +} + +fn gen_branch_case(rng: &mut Rng, depth: u32) -> String { + let name = format!("Ent{}", rng.below(1000)); + let s0 = format!("s{}start", rng.below(100)); + let s1 = format!("s{}end", rng.below(100)); + let (req, ens) = match rng.below(3) { + 1 => ( + format!("requires: ghost.status = {s0}"), + format!("ensures: t.status = {s1}"), + ), + 2 => ( + format!("requires: t.status = {s0}"), + format!("ensures: Ghost{name}.created(status: {s0})"), + ), + _ => ( + format!("requires: t.status = {s0}"), + format!("ensures: t.status = {s1}"), + ), + }; + let body = wrap_ifelse(&format!("{req}\n{ens}"), depth); + format!( + "-- allium: 3\n\ + entity {name} {{\n status: {s0} | {s1}\n transitions status {{ {s0} -> {s1} terminal: {s1} }}\n}}\n\ + rule Create{name} {{\n when: Create{name}Requested()\n ensures: {name}.created(status: {s0})\n}}\n\ + rule Advance{name} {{\n when: Advance{name}(t, flag)\n{body}\n}}\n\ + surface {name}Desk {{\n provides:\n Create{name}Requested()\n Advance{name}(t: {name}, flag)\n}}\n", + ) +} + +fn report_kinds(src: &str) -> Vec { + let mut v = report_set(src); + v.dedup(); + v +} + +#[test] +fn branch_wrapping_is_report_invariant() { + for seed in 0..400u64 { + // Compare the flat form against 1..=3 levels of identical if/else nesting; + // the depth cycles with the seed so every depth is exercised. + let depth = 1 + (seed % 3) as u32; + let flat = gen_branch_case(&mut Rng::new(seed), 0); + let nested = gen_branch_case(&mut Rng::new(seed), depth); + let a = report_kinds(&flat); + let b = report_kinds(&nested); + assert_eq!( + a, b, + "seed {seed}: wrapping requires/ensures in {depth} level(s) of identical if/else changed the reports.\n\ + FLAT:\n{flat}\n-> {a:?}\n\nNESTED:\n{nested}\n-> {b:?}" + ); + } +} + +// --------------------------------------------------------------------------- +// Declaration-order invariance. Reordering a spec's top-level declarations must +// not change the reports: the analysis is a function of the spec, not its text +// order. This targets order-dependent bugs — HashMap iteration order, or a +// first-writer-wins aggregation across entities — that the split-invariance +// properties never disturb. Some entities are generated without an advancing +// rule so they produce lifecycle findings, making the invariant non-trivial. +// --------------------------------------------------------------------------- + +fn gen_blocks(rng: &mut Rng) -> Vec { + let n = 3 + rng.below(4); // 3..=6 entities + let mut blocks = Vec::new(); + for i in 0..n { + let name = format!("Ent{i}"); + let s0 = format!("s{i}a"); + let s1 = format!("s{i}b"); + blocks.push(format!( + "entity {name} {{\n status: {s0} | {s1}\n transitions status {{ {s0} -> {s1} terminal: {s1} }}\n}}\n" + )); + blocks.push(format!( + "rule Create{name} {{\n when: {name}Req()\n ensures: {name}.created(status: {s0})\n}}\n" + )); + // Omit the advancing rule on some entities, so they draw lifecycle + // findings and the report set is non-empty. + if rng.below(2) == 0 { + blocks.push(format!( + "rule Advance{name} {{\n when: b: {name}.status becomes {s0}\n ensures: b.status = {s1}\n}}\n" + )); + } + blocks.push(format!( + "surface {name}Desk {{\n provides:\n {name}Req()\n}}\n" + )); + } + blocks +} + +fn shuffle(rng: &mut Rng, v: &mut [String]) { + for i in (1..v.len()).rev() { + let j = rng.below(i + 1); + v.swap(i, j); + } +} + +#[test] +fn declaration_order_is_report_invariant() { + for seed in 0..250u64 { + let mut rng = Rng::new(seed); + let blocks = gen_blocks(&mut rng); + let base = format!("-- allium: 3\n\n{}", blocks.join("\n")); + let mut shuffled = blocks.clone(); + shuffle(&mut rng, &mut shuffled); + let variant = format!("-- allium: 3\n\n{}", shuffled.join("\n")); + let a = report_set(&base); + let b = report_set(&variant); + assert_eq!( + a, b, + "seed {seed}: reordering top-level declarations changed the reports.\n\ + BASE -> {a:?}\nSHUFFLED -> {b:?}\n\n{variant}" + ); + } +} + +#[test] +fn undefined_binding_flagged_inside_if_branch() { + let base = "-- allium: 3\n\nentity Job {\n status: pending | done\n transitions status { pending -> done terminal: done }\n}\n\nsurface S {\n provides:\n Go(flag)\n}\n"; + let top = format!( + "{base}\nrule R {{\n when: Go(flag)\n requires: ghost.status = pending\n ensures: Job.created(status: pending)\n}}\n" + ); + let branched = format!( + "{base}\nrule R {{\n when: Go(flag)\n if flag:\n requires: ghost.status = pending\n ensures: Job.created(status: pending)\n else:\n ensures: Job.created(status: pending)\n}}\n" + ); + let t = undefined_binding_codes(&top); + let b = undefined_binding_codes(&branched); + assert!(!t.is_empty(), "control: a top-level undefined binding should be flagged, got {t:?}"); + assert_eq!( + t, b, + "an undefined binding nested in an if-branch was not flagged like the top-level form" + ); +} + +#[test] +fn branch_local_let_is_not_a_false_positive() { + // A `let` declared inside a branch scopes that branch, so referencing it + // there must not trip undefinedBinding. + let src = "-- allium: 3\n\nentity Job {\n status: pending | done\n transitions status { pending -> done terminal: done }\n}\n\nsurface S {\n provides:\n Go(flag)\n}\n\nrule R {\n when: Go(flag)\n if flag:\n let j = Job\n ensures: j.status = done\n else:\n ensures: Job.created(status: pending)\n}\n"; + assert!( + undefined_binding_codes(src).is_empty(), + "a branch-local let was wrongly flagged as undefined: {:?}", + undefined_binding_codes(src) + ); +} + +#[test] +fn undeclared_type_flagged_inside_if_branch() { + // A type reference to an undeclared entity must be flagged the same whether + // it sits at the top level of a rule or inside an `if`/`else` body. The + // type-reference pass used to walk only top-level clauses. + let base = "-- allium: 3\n\nentity Job {\n status: pending | done\n transitions status { pending -> done terminal: done }\n}\n\nsurface S {\n provides:\n Go(flag)\n}\n"; + let top = format!( + "{base}\nrule R {{\n when: Go(flag)\n ensures: Ghost.created(status: pending)\n}}\n" + ); + let branched = format!( + "{base}\nrule R {{\n when: Go(flag)\n if flag:\n ensures: Ghost.created(status: pending)\n else:\n ensures: Job.created(status: pending)\n}}\n" + ); + let has_undeclared = |src: &str| { + diagnostics_of(src) + .iter() + .any(|d| d.message.contains("Type reference 'Ghost' is not declared")) + }; + assert!(has_undeclared(&top), "control: a top-level undeclared type should be flagged"); + assert!( + has_undeclared(&branched), + "an undeclared type nested in an if-branch was not flagged like the top-level form" + ); +} + #[test] fn becomes_triggered_transition_has_no_false_noexit() { // #70 subject, single file: the exit from `closed` is witnessed by the diff --git a/crates/allium/tests/witness_matrix.rs b/crates/allium/tests/witness_matrix.rs new file mode 100644 index 0000000..fc60e05 --- /dev/null +++ b/crates/allium/tests/witness_matrix.rs @@ -0,0 +1,1065 @@ +//! Witness matrix: a systematic sweep over how a cross-module transition +//! witness can be expressed, so a false lifecycle report on a *valid* witness +//! surfaces regardless of which binding-type source or module layout is used. +//! +//! Every scenario is a complete, valid lifecycle: entity `Job` is created in +//! `pending`, a rule witnesses `pending -> done`, and `done` is terminal. The +//! only thing that varies is *how the witnessing rule's binding is typed to the +//! entity* (the binding-type source) and whether the spec is one file or split +//! across a `use` edge. All of them should be completely clean. +//! +//! Two properties per scenario: +//! 1. the single-file form (a valid witness) reports nothing; +//! 2. the split form reports exactly what the single-file form does +//! (the merged-single-file oracle from #66/#74). +//! +//! Discovery mode: this collects every anomaly and reports them together, so a +//! sweep shows the whole failing set at once rather than the first cell. + +use std::fs; +use std::path::Path; +use std::process::Command; +use std::sync::atomic::{AtomicU64, Ordering}; + +fn allium() -> Command { + Command::new(env!("CARGO_BIN_EXE_allium")) +} + +// Unique per TempDir, so tests running in parallel never share a path. Keying on +// the process id alone let concurrent tests clobber each other's `single`/`pair` +// directories, which showed up as flaky split-invariance failures in the full run. +static TEMPDIR_SEQ: AtomicU64 = AtomicU64::new(0); + +struct TempDir { + path: std::path::PathBuf, +} +impl TempDir { + fn new(name: &str) -> Self { + let seq = TEMPDIR_SEQ.fetch_add(1, Ordering::Relaxed); + let path = std::env::temp_dir() + .join(format!("allium-wm-{name}-{}-{seq}", std::process::id())); + let _ = fs::remove_dir_all(&path); + fs::create_dir_all(&path).unwrap(); + Self { path } + } + fn write(&self, name: &str, content: &str) { + fs::write(self.path.join(name), content).unwrap(); + } + fn file(&self, name: &str) -> String { + self.path.join(name).to_string_lossy().into_owned() + } + fn path(&self) -> &Path { + &self.path + } +} +impl Drop for TempDir { + fn drop(&mut self) { + let _ = fs::remove_dir_all(&self.path); + } +} + +fn split_json_docs(s: &str) -> Vec { + let mut docs = Vec::new(); + let (mut depth, mut start, mut in_str, mut esc) = (0i32, None, false, false); + for (i, ch) in s.char_indices() { + if in_str { + if esc { + esc = false; + } else if ch == '\\' { + esc = true; + } else if ch == '"' { + in_str = false; + } + continue; + } + match ch { + '"' => in_str = true, + '{' => { + if depth == 0 { + start = Some(i); + } + depth += 1; + } + '}' => { + depth -= 1; + if depth == 0 { + if let Some(s0) = start { + docs.push(s[s0..=i].to_string()); + } + start = None; + } + } + _ => {} + } + } + docs +} + +/// A canonical report set, independent of which file a report lands in: the +/// diagnostic codes and finding types (with the entity/status they name, via +/// the message, which is filename- and line-free). +fn report_set(stdout: &str) -> Vec { + let mut rows = Vec::new(); + for doc in split_json_docs(stdout) { + let Ok(v) = serde_json::from_str::(&doc) else { + continue; + }; + if let Some(arr) = v["diagnostics"].as_array() { + for d in arr { + if let (Some(c), Some(m)) = (d["code"].as_str(), d["message"].as_str()) { + rows.push(format!("D {c} :: {m}")); + } + } + } + if let Some(arr) = v["findings"].as_array() { + for f in arr { + rows.push(format!( + "F {} :: {}", + f["type"].as_str().unwrap_or(""), + f["summary"].as_str().unwrap_or("") + )); + } + } + } + rows.sort(); + rows +} + +fn run(cmd: &str, args: &[&str]) -> String { + let out = allium().arg(cmd).args(args).output().expect("spawn allium"); + String::from_utf8_lossy(&out.stdout).into_owned() +} + +fn reports_of_file(content: &str) -> Vec { + let dir = TempDir::new("single"); + dir.write("spec.allium", content); + let mut all = report_set(&run("check", &[&dir.file("spec.allium")])); + all.extend(report_set(&run("analyse", &[&dir.file("spec.allium")]))); + all.sort(); + all.dedup(); + all +} + +fn reports_of_pair(domain: &str, consumer: &str) -> Vec { + let dir = TempDir::new("pair"); + dir.write("domain.allium", domain); + dir.write("consumer.allium", consumer); + let mut all = report_set(&run("check", &[dir.path().to_str().unwrap()])); + all.extend(report_set(&run("analyse", &[dir.path().to_str().unwrap()]))); + all.sort(); + all.dedup(); + all +} + +// --------------------------------------------------------------------------- +// Scenario generation: one valid witness of Job: pending -> done, expressed +// through each binding-type source, as a single file and as a domain+consumer +// split. +// --------------------------------------------------------------------------- + +/// The domain always present: entity, creation rule, and a surface providing +/// the creation trigger (so the creation trigger is never unreachable). +const DOMAIN_BASE: &str = "entity Job {\n status: pending | done\n transitions status { pending -> done terminal: done }\n}\n\nrule CreateJob {\n when: JobRequested()\n ensures: Job.created(status: pending)\n}\n\nsurface JobIntake {\n provides:\n JobRequested()\n}\n"; + +struct Scenario { + name: &'static str, + single: String, + domain: String, + consumer: String, +} + +fn scenarios() -> Vec { + // (domain-side extra, consumer body qualified via `dom/`, consumer body local) + // Each consumer body witnesses pending -> done. + let cases: Vec<(&'static str, &str, &str, &str)> = vec![ + ( + "sub_requires", + "surface JobDesk {\n provides:\n Ready(x: Job)\n when x.status = pending\n}\n", + "rule Witness {\n when: dom/Ready(b)\n requires: b.status = pending\n ensures: b.status = done\n}\n", + "rule Witness {\n when: Ready(b)\n requires: b.status = pending\n ensures: b.status = done\n}\n", + ), + ( + "becomes", + "", + "rule Witness {\n when: b: dom/Job.status becomes pending\n ensures: b.status = done\n}\n", + "rule Witness {\n when: b: Job.status becomes pending\n ensures: b.status = done\n}\n", + ), + ( + "transitions_to", + "", + "rule Witness {\n when: b: dom/Job.status transitions_to pending\n ensures: b.status = done\n}\n", + "rule Witness {\n when: b: Job.status transitions_to pending\n ensures: b.status = done\n}\n", + ), + ( + "importer_context", + "", + "surface WDesk {\n context b: dom/Job\n provides:\n Ready(b)\n when b.status = pending\n}\n\nrule Witness {\n when: Ready(z)\n requires: z.status = pending\n ensures: z.status = done\n}\n", + "surface WDesk {\n context b: Job\n provides:\n Ready(b)\n when b.status = pending\n}\n\nrule Witness {\n when: Ready(z)\n requires: z.status = pending\n ensures: z.status = done\n}\n", + ), + ( + "importer_context_where_eq", + "", + "surface WDesk {\n context b: dom/Job where status = pending\n provides:\n Ready(b)\n when b.status = pending\n}\n\nrule Witness {\n when: Ready(z)\n requires: z.status = pending\n ensures: z.status = done\n}\n", + "surface WDesk {\n context b: Job where status = pending\n provides:\n Ready(b)\n when b.status = pending\n}\n\nrule Witness {\n when: Ready(z)\n requires: z.status = pending\n ensures: z.status = done\n}\n", + ), + ( + "importer_context_where_in", + "", + "surface WDesk {\n context b: dom/Job where status in {pending, done}\n provides:\n Ready(b)\n when b.status = pending\n}\n\nrule Witness {\n when: Ready(z)\n requires: z.status = pending\n ensures: z.status = done\n}\n", + "surface WDesk {\n context b: Job where status in {pending, done}\n provides:\n Ready(b)\n when b.status = pending\n}\n\nrule Witness {\n when: Ready(z)\n requires: z.status = pending\n ensures: z.status = done\n}\n", + ), + ( + "importer_facing", + "", + "surface WDesk {\n facing b: dom/Job\n provides:\n Ready(b)\n when b.status = pending\n}\n\nrule Witness {\n when: Ready(z)\n requires: z.status = pending\n ensures: z.status = done\n}\n", + "surface WDesk {\n facing b: Job\n provides:\n Ready(b)\n when b.status = pending\n}\n\nrule Witness {\n when: Ready(z)\n requires: z.status = pending\n ensures: z.status = done\n}\n", + ), + ( + "importer_inline", + "", + "surface WDesk {\n provides:\n Ready(b: dom/Job)\n when b.status = pending\n}\n\nrule Witness {\n when: Ready(z)\n requires: z.status = pending\n ensures: z.status = done\n}\n", + "surface WDesk {\n provides:\n Ready(b: Job)\n when b.status = pending\n}\n\nrule Witness {\n when: Ready(z)\n requires: z.status = pending\n ensures: z.status = done\n}\n", + ), + ( + "importer_inline_where", + "", + "surface WDesk {\n provides:\n Ready(b: dom/Job where status = pending)\n when b.status = pending\n}\n\nrule Witness {\n when: Ready(z)\n requires: z.status = pending\n ensures: z.status = done\n}\n", + "surface WDesk {\n provides:\n Ready(b: Job where status = pending)\n when b.status = pending\n}\n\nrule Witness {\n when: Ready(z)\n requires: z.status = pending\n ensures: z.status = done\n}\n", + ), + ( + "importer_inline_with", + "", + "surface WDesk {\n provides:\n Ready(b: dom/Job with status = pending)\n when b.status = pending\n}\n\nrule Witness {\n when: Ready(z)\n requires: z.status = pending\n ensures: z.status = done\n}\n", + "surface WDesk {\n provides:\n Ready(b: Job with status = pending)\n when b.status = pending\n}\n\nrule Witness {\n when: Ready(z)\n requires: z.status = pending\n ensures: z.status = done\n}\n", + ), + ( + "importer_context_with", + "", + "surface WDesk {\n context b: dom/Job with status = pending\n provides:\n Ready(b)\n when b.status = pending\n}\n\nrule Witness {\n when: Ready(z)\n requires: z.status = pending\n ensures: z.status = done\n}\n", + "surface WDesk {\n context b: Job with status = pending\n provides:\n Ready(b)\n when b.status = pending\n}\n\nrule Witness {\n when: Ready(z)\n requires: z.status = pending\n ensures: z.status = done\n}\n", + ), + ( + "importer_facing_with", + "", + "surface WDesk {\n facing b: dom/Job with status = pending\n provides:\n Ready(b)\n when b.status = pending\n}\n\nrule Witness {\n when: Ready(z)\n requires: z.status = pending\n ensures: z.status = done\n}\n", + "surface WDesk {\n facing b: Job with status = pending\n provides:\n Ready(b)\n when b.status = pending\n}\n\nrule Witness {\n when: Ready(z)\n requires: z.status = pending\n ensures: z.status = done\n}\n", + ), + ( + "rule_emission", + "rule Announce {\n when: j: Job.status becomes pending\n ensures: Ready(job: j)\n}\n", + "rule Witness {\n when: dom/Ready(b)\n requires: b.status = pending\n ensures: b.status = done\n}\n", + "rule Witness {\n when: Ready(b)\n requires: b.status = pending\n ensures: b.status = done\n}\n", + ), + ( + "rule_emission_transitions_to", + "rule Announce {\n when: j: Job.status transitions_to pending\n ensures: Ready(job: j)\n}\n", + "rule Witness {\n when: dom/Ready(b)\n requires: b.status = pending\n ensures: b.status = done\n}\n", + "rule Witness {\n when: Ready(b)\n requires: b.status = pending\n ensures: b.status = done\n}\n", + ), + ( + "emission_command_typed", + "surface Kicker {\n provides:\n Kick(j: Job)\n}\n\nrule Announce {\n when: Kick(j)\n ensures: Ready(job: j)\n}\n", + "rule Witness {\n when: dom/Ready(b)\n requires: b.status = pending\n ensures: b.status = done\n}\n", + "rule Witness {\n when: Ready(b)\n requires: b.status = pending\n ensures: b.status = done\n}\n", + ), + ( + "emission_in_branch", + "surface Kicker {\n provides:\n Kick(j: Job, flag)\n}\n\nrule Announce {\n when: Kick(j, flag)\n if flag:\n ensures: Ready(job: j)\n else:\n ensures: Ready(job: j)\n}\n", + "rule Witness {\n when: dom/Ready(b)\n requires: b.status = pending\n ensures: b.status = done\n}\n", + "rule Witness {\n when: Ready(b)\n requires: b.status = pending\n ensures: b.status = done\n}\n", + ), + ( + "branch_target", + "surface JobDesk {\n provides:\n Ready(x: Job, flag)\n when x.status = pending\n}\n", + "rule Witness {\n when: dom/Ready(b, ok)\n requires: b.status = pending\n if ok:\n ensures: b.status = done\n else:\n ensures: b.status = done\n}\n", + "rule Witness {\n when: Ready(b, ok)\n requires: b.status = pending\n if ok:\n ensures: b.status = done\n else:\n ensures: b.status = done\n}\n", + ), + ]; + + let mut out: Vec = cases + .into_iter() + .map(|(name, domain_extra, consumer_qual, consumer_local)| { + let single = format!("-- allium: 3\n\n{DOMAIN_BASE}\n{domain_extra}\n{consumer_local}"); + let domain = format!("-- allium: 3\n\n{DOMAIN_BASE}\n{domain_extra}"); + let consumer = + format!("-- allium: 3\n\nuse \"./domain.allium\" as dom\n\n{consumer_qual}"); + Scenario { name, single, domain, consumer } + }) + .collect(); + + // Multi-hop lifecycle (pending -> active -> done) witnessed across a module, + // one becomes-triggered rule per hop. Needs its own 3-state entity, so it + // does not use DOMAIN_BASE. + let mh_entity = "entity Job {\n status: pending | active | done\n transitions status { pending -> active active -> done terminal: done }\n}\n\nrule CreateJob {\n when: JobRequested()\n ensures: Job.created(status: pending)\n}\n\nsurface JobIntake {\n provides:\n JobRequested()\n}\n"; + out.push(Scenario { + name: "multi_hop", + single: format!( + "-- allium: 3\n\n{mh_entity}\nrule W1 {{\n when: a: Job.status becomes pending\n ensures: a.status = active\n}}\n\nrule W2 {{\n when: c: Job.status becomes active\n ensures: c.status = done\n}}\n" + ), + domain: format!("-- allium: 3\n\n{mh_entity}"), + consumer: "-- allium: 3\n\nuse \"./domain.allium\" as dom\n\nrule W1 {\n when: a: dom/Job.status becomes pending\n ensures: a.status = active\n}\n\nrule W2 {\n when: c: dom/Job.status becomes active\n ensures: c.status = done\n}\n".to_string(), + }); + + // Importer creates the imported entity inside an if/else branch. The domain + // does not create it, so the importer's creation is the only assignment of + // `pending`. + let ci_domain = "entity Job {\n status: pending | done\n transitions status { pending -> done terminal: done }\n}\n\nrule Advance {\n when: t: Job.status becomes pending\n ensures: t.status = done\n}\n"; + out.push(Scenario { + name: "created_in_branch", + single: format!( + "-- allium: 3\n\n{ci_domain}\nrule Make {{\n when: Go(flag)\n if flag:\n ensures: Job.created(status: pending)\n else:\n ensures: Job.created(status: pending)\n}}\n\nsurface Intake {{\n provides:\n Go(flag)\n}}\n" + ), + domain: format!("-- allium: 3\n\n{ci_domain}"), + consumer: "-- allium: 3\n\nuse \"./domain.allium\" as dom\n\nrule Make {\n when: Go(flag)\n if flag:\n ensures: dom/Job.created(status: pending)\n else:\n ensures: dom/Job.created(status: pending)\n}\n\nsurface Intake {\n provides:\n Go(flag)\n}\n".to_string(), + }); + + // Temporal trigger (`m: E.due_at <= now`) as the witnessing form. It needs a + // Timestamp field, so it doesn't fit DOMAIN_BASE. The imported entity's + // transition is witnessed by a time-based, not event-based, trigger. + let tt_domain = "entity Job {\n status: pending | done\n due_at: Timestamp\n transitions status { pending -> done terminal: done }\n}\n\nrule CreateJob {\n when: JobRequested()\n ensures: Job.created(status: pending)\n}\n\nsurface JobIntake {\n provides:\n JobRequested()\n}\n"; + out.push(Scenario { + name: "temporal_trigger", + single: format!( + "-- allium: 3\n\n{tt_domain}\nrule Witness {{\n when: m: Job.due_at <= now\n requires: m.status = pending\n ensures: m.status = done\n}}\n" + ), + domain: format!("-- allium: 3\n\n{tt_domain}"), + consumer: "-- allium: 3\n\nuse \"./domain.allium\" as dom\n\nrule Witness {\n when: m: dom/Job.due_at <= now\n requires: m.status = pending\n ensures: m.status = done\n}\n".to_string(), + }); + + out +} + +#[test] +fn witness_matrix_sweep() { + let mut anomalies: Vec = Vec::new(); + + for sc in scenarios() { + let single = reports_of_file(&sc.single); + let split = reports_of_pair(&sc.domain, &sc.consumer); + + if !single.is_empty() { + anomalies.push(format!( + "[{}] SINGLE-FILE not clean (valid witness should report nothing):\n {}\n--- spec ---\n{}", + sc.name, + single.join("\n "), + sc.single + )); + } + if split != single { + anomalies.push(format!( + "[{}] SPLIT != SINGLE (split-invariance violation):\n single: {:?}\n split: {:?}", + sc.name, single, split + )); + } + } + + if !anomalies.is_empty() { + panic!( + "\n==== WITNESS MATRIX: {} anomalies ====\n\n{}\n", + anomalies.len(), + anomalies.join("\n\n") + ); + } +} + +// --------------------------------------------------------------------------- +// Alias-anchoring sweep: at every site a qualified reference `alias/Name` can +// appear, a qualifier that matches no `use` alias is a locally-knowable typo +// and should be diagnosed at the reference. This is the "sites audit" as a +// test: #72 covers `provides:`, #78 asks for `when:`; the rest are unaudited. +// +// Each snippet declares `dom` and then misspells one qualifier as `nosuch`. +// A site is caught if some diagnostic names `nosuch`. +// --------------------------------------------------------------------------- + +fn diagnostics_mentioning(content: &str, needle: &str) -> Vec { + let dir = TempDir::new("alias"); + dir.write("spec.allium", content); + let out = run("check", &[&dir.file("spec.allium")]); + let mut hits = Vec::new(); + for doc in split_json_docs(&out) { + let Ok(v) = serde_json::from_str::(&doc) else { + continue; + }; + if let Some(arr) = v["diagnostics"].as_array() { + for d in arr { + let msg = d["message"].as_str().unwrap_or(""); + if msg.contains(needle) { + hits.push(format!("{} :: {msg}", d["code"].as_str().unwrap_or(""))); + } + } + } + } + hits +} + +#[test] +fn alias_anchoring_sweep() { + let head = "-- allium: 3\n\nuse \"./domain.allium\" as dom\n\n"; + // (site name, snippet after the `use dom` header, with one `nosuch/` typo) + let sites: Vec<(&str, String)> = vec![ + ("when_subscription", format!("{head}rule R {{\n when: nosuch/Ready(x)\n ensures: Done()\n}}\n")), + ("when_transition_trigger", format!("{head}rule R {{\n when: t: nosuch/Job.status becomes pending\n ensures: t.status = done\n}}\n")), + ("provides", format!("{head}surface S {{\n provides:\n nosuch/Ready()\n}}\n")), + ("surface_context", format!("{head}surface S {{\n context b: nosuch/Job\n provides:\n Ready(b)\n}}\n")), + ("inline_provides_param", format!("{head}surface S {{\n provides:\n Ready(b: nosuch/Job)\n}}\n")), + ("field_type", format!("{head}entity Wrapper {{\n j: nosuch/Job\n}}\n")), + ("ensures_created", format!("{head}rule R {{\n when: Go()\n ensures: nosuch/Job.created(status: pending)\n}}\n")), + ("default_type", format!("{head}default nosuch/Config c = {{ enabled: true }}\n")), + ("requires_entity", format!("{head}rule R {{\n when: Go()\n requires: nosuch/Job.status = pending\n ensures: Done()\n}}\n")), + ("ensures_status", format!("{head}rule R {{\n when: Go()\n ensures: nosuch/Job.status = done\n}}\n")), + ("invariant_ref", format!("{head}invariant I {{\n nosuch/Job.status = done\n}}\n")), + ("contract_fulfils", format!("{head}surface S {{\n facing u: User\n contracts:\n fulfils nosuch/MyContract\n}}\n")), + ("field_type_in_value", format!("{head}value Wrapper {{\n j: nosuch/Job\n}}\n")), + ]; + + let mut uncaught: Vec = Vec::new(); + for (site, snippet) in sites { + let hits = diagnostics_mentioning(&snippet, "nosuch"); + if hits.is_empty() { + uncaught.push(format!("[{site}] NO diagnostic names the undeclared alias 'nosuch'\n--- spec ---\n{snippet}")); + } + } + + if !uncaught.is_empty() { + panic!( + "\n==== ALIAS ANCHORING: {} sites do not diagnose an undeclared qualifier ====\n\n{}\n", + uncaught.len(), + uncaught.join("\n\n") + ); + } +} + +// --------------------------------------------------------------------------- +// Name-existence sweep: with a valid alias, a qualified reference to a name the +// aliased module does not declare (`dom/Ghost`) should be diagnosed. #72 does +// this for provides triggers and #47 for default fields; every other qualified +// entity/type reference site is the audit's next layer. Needs the domain in the +// check set, so it runs as pairs. +// --------------------------------------------------------------------------- + +const NE_DOMAIN: &str = "-- allium: 3\n\nentity Job {\n status: pending | done\n transitions status { pending -> done terminal: done }\n}\n\nrule CreateJob {\n when: JobRequested()\n ensures: Job.created(status: pending)\n}\n\nsurface JobIntake {\n provides:\n JobRequested()\n}\n"; + +fn pair_diagnostics_mentioning(consumer: &str, needle: &str) -> Vec { + let dir = TempDir::new("nameexist"); + dir.write("domain.allium", NE_DOMAIN); + dir.write("consumer.allium", consumer); + let out = run("check", &[dir.path().to_str().unwrap()]); + let mut hits = Vec::new(); + for doc in split_json_docs(&out) { + let Ok(v) = serde_json::from_str::(&doc) else { + continue; + }; + if let Some(arr) = v["diagnostics"].as_array() { + for d in arr { + let msg = d["message"].as_str().unwrap_or(""); + if msg.contains(needle) { + hits.push(format!("{} :: {msg}", d["code"].as_str().unwrap_or(""))); + } + } + } + } + hits +} + +#[test] +fn name_existence_sweep() { + // `dom` is valid; `Ghost` is not an entity/type the domain declares. + let head = "-- allium: 3\n\nuse \"./domain.allium\" as dom\n\n"; + let sites: Vec<(&str, String)> = vec![ + ("surface_context", format!("{head}surface S {{\n context t: dom/Ghost\n provides:\n Ev(t)\n}}\n")), + ("field_type", format!("{head}entity W {{\n j: dom/Ghost\n}}\n")), + ("ensures_created", format!("{head}rule R {{\n when: Go()\n ensures: dom/Ghost.created(status: pending)\n}}\n")), + ("transition_subject", format!("{head}rule R {{\n when: t: dom/Ghost.status becomes pending\n ensures: t.status = done\n}}\n")), + ("inline_provides_param", format!("{head}surface S {{\n provides:\n Ev(b: dom/Ghost)\n}}\n")), + ]; + + let mut uncaught: Vec = Vec::new(); + for (site, snippet) in sites { + if pair_diagnostics_mentioning(&snippet, "Ghost").is_empty() { + uncaught.push(format!("[{site}] NO diagnostic names the nonexistent 'dom/Ghost'\n--- consumer ---\n{snippet}")); + } + } + + if !uncaught.is_empty() { + panic!( + "\n==== NAME EXISTENCE: {} sites do not diagnose a nonexistent qualified name ====\n\n{}\n", + uncaught.len(), + uncaught.join("\n\n") + ); + } +} + +// --------------------------------------------------------------------------- +// Generative split-invariance. The hand-written scenarios above enumerate the +// binding-type sources at fixed names; this generates random entity/state names +// and picks a witnessing form each seed, so the property (a valid witness is +// clean single-file, and the split reports exactly the same) is exercised over a +// far wider surface than the fixed cells. A false lifecycle report that only +// shows up for some name or form combination surfaces here. +// --------------------------------------------------------------------------- + +struct Rng(u64); +impl Rng { + fn new(seed: u64) -> Self { + Rng(seed.wrapping_mul(0x9E37_79B9_7F4A_7C15).wrapping_add(1)) + } + fn next(&mut self) -> u64 { + self.0 = self.0.wrapping_add(0x9E37_79B9_7F4A_7C15); + let mut z = self.0; + z = (z ^ (z >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9); + z = (z ^ (z >> 27)).wrapping_mul(0x94D0_49BB_1331_11EB); + z ^ (z >> 31) + } + fn below(&mut self, n: u64) -> u64 { + self.next() % n + } +} + +struct SplitCase { + single: String, + domain: String, + consumer: String, + form: &'static str, +} + +fn gen_split_case(seed: u64) -> SplitCase { + let mut rng = Rng::new(seed); + let e = format!("Ent{}", rng.below(1000)); + let s0 = format!("s{}a", rng.below(100)); + let s1 = format!("s{}b", rng.below(100)); + let form = rng.below(6); + let temporal = form == 5; + let field = if temporal { " due_at: Timestamp\n" } else { "" }; + let entity = format!( + "entity {e} {{\n status: {s0} | {s1}\n{field} transitions status {{ {s0} -> {s1} terminal: {s1} }}\n}}\n" + ); + let create = format!("rule Create{e} {{\n when: {e}Req()\n ensures: {e}.created(status: {s0})\n}}\n"); + let intake = format!("surface {e}Intake {{\n provides:\n {e}Req()\n}}\n"); + let domain_body = format!("{entity}\n{create}\n{intake}"); + + // A type refinement is a no-op on which entity a binding refers to, so the + // context/facing/inline forms carry a random one to also exercise refinement + // unwrapping (the #76 family) generatively. + let refine = match rng.below(3) { + 1 => format!(" where status = {s0}"), + 2 => format!(" with status = {s0}"), + _ => String::new(), + }; + let witness = |q: &str| -> String { + match form { + 0 => format!("rule W {{\n when: b: {q}{e}.status becomes {s0}\n ensures: b.status = {s1}\n}}\n"), + 1 => format!("rule W {{\n when: b: {q}{e}.status transitions_to {s0}\n ensures: b.status = {s1}\n}}\n"), + 2 => format!("surface WDesk {{\n context b: {q}{e}{refine}\n provides:\n Ready(b)\n when b.status = {s0}\n}}\n\nrule W {{\n when: Ready(z)\n requires: z.status = {s0}\n ensures: z.status = {s1}\n}}\n"), + 3 => format!("surface WDesk {{\n facing b: {q}{e}{refine}\n provides:\n Ready(b)\n when b.status = {s0}\n}}\n\nrule W {{\n when: Ready(z)\n requires: z.status = {s0}\n ensures: z.status = {s1}\n}}\n"), + 4 => format!("surface WDesk {{\n provides:\n Ready(b: {q}{e}{refine})\n when b.status = {s0}\n}}\n\nrule W {{\n when: Ready(z)\n requires: z.status = {s0}\n ensures: z.status = {s1}\n}}\n"), + _ => format!("rule W {{\n when: m: {q}{e}.due_at <= now\n requires: m.status = {s0}\n ensures: m.status = {s1}\n}}\n"), + } + }; + let form_name = ["becomes", "transitions_to", "context", "facing", "inline", "temporal"][form as usize]; + + SplitCase { + single: format!("-- allium: 3\n\n{domain_body}\n{}", witness("")), + domain: format!("-- allium: 3\n\n{domain_body}"), + consumer: format!("-- allium: 3\n\nuse \"./domain.allium\" as dom\n\n{}", witness("dom/")), + form: form_name, + } +} + +#[test] +fn generative_split_invariance() { + let mut anomalies: Vec = Vec::new(); + for seed in 0..90u64 { + let c = gen_split_case(seed); + let single = reports_of_file(&c.single); + let split = reports_of_pair(&c.domain, &c.consumer); + if !single.is_empty() { + anomalies.push(format!( + "[seed {seed} form={}] generated single-file witness is not clean: {single:?}\n{}", + c.form, c.single + )); + } else if single != split { + anomalies.push(format!( + "[seed {seed} form={}] SPLIT != SINGLE\n single: {single:?}\n split: {split:?}\n--- consumer ---\n{}", + c.form, c.consumer + )); + } + } + assert!( + anomalies.is_empty(), + "\n==== GENERATIVE SPLIT-INVARIANCE: {} anomalies ====\n\n{}\n", + anomalies.len(), + anomalies.join("\n\n") + ); +} + +// --------------------------------------------------------------------------- +// Multi-entity split-invariance. Several entities, each created in the domain and +// advanced by a witnessing rule in the consumer, exercise the reverse channel +// aggregating contributions for more than one entity at once. A per-entity key +// mix-up (crediting entity A's transition to entity B, say) shows up as a +// spurious lifecycle report on the split that the single file does not have. +// --------------------------------------------------------------------------- + +fn gen_multi_split_case(seed: u64) -> (String, String, String) { + let mut rng = Rng::new(seed); + let n = 2 + rng.below(3); // 2..=4 entities + let mut domain_body = String::new(); + let mut single_witness = String::new(); + let mut consumer_witness = String::new(); + for i in 0..n { + let e = format!("Ent{i}x{}", rng.below(100)); + let s0 = format!("s{}a", rng.below(100)); + let s1 = format!("s{}b", rng.below(100)); + let trig = if rng.below(2) == 0 { "becomes" } else { "transitions_to" }; + domain_body.push_str(&format!( + "entity {e} {{\n status: {s0} | {s1}\n transitions status {{ {s0} -> {s1} terminal: {s1} }}\n}}\n\nrule Create{e} {{\n when: {e}Req()\n ensures: {e}.created(status: {s0})\n}}\n\nsurface {e}Intake {{\n provides:\n {e}Req()\n}}\n\n" + )); + single_witness.push_str(&format!( + "rule W{i} {{\n when: b: {e}.status {trig} {s0}\n ensures: b.status = {s1}\n}}\n\n" + )); + consumer_witness.push_str(&format!( + "rule W{i} {{\n when: b: dom/{e}.status {trig} {s0}\n ensures: b.status = {s1}\n}}\n\n" + )); + } + let single = format!("-- allium: 3\n\n{domain_body}{single_witness}"); + let domain = format!("-- allium: 3\n\n{domain_body}"); + let consumer = format!("-- allium: 3\n\nuse \"./domain.allium\" as dom\n\n{consumer_witness}"); + (single, domain, consumer) +} + +#[test] +fn generative_multi_entity_split_invariance() { + let mut anomalies: Vec = Vec::new(); + for seed in 0..70u64 { + let (single_src, domain, consumer) = gen_multi_split_case(seed); + let single = reports_of_file(&single_src); + let split = reports_of_pair(&domain, &consumer); + if !single.is_empty() { + anomalies.push(format!("[seed {seed}] multi-entity single-file not clean: {single:?}\n{single_src}")); + } else if single != split { + anomalies.push(format!( + "[seed {seed}] SPLIT != SINGLE\n single: {single:?}\n split: {split:?}\n--- consumer ---\n{consumer}" + )); + } + } + assert!( + anomalies.is_empty(), + "\n==== MULTI-ENTITY SPLIT-INVARIANCE: {} anomalies ====\n\n{}\n", + anomalies.len(), + anomalies.join("\n\n") + ); +} + +fn reports_of_set(files: &[(String, String)]) -> Vec { + let dir = TempDir::new("set"); + for (name, content) in files { + dir.write(name, content); + } + let mut all = report_set(&run("check", &[dir.path().to_str().unwrap()])); + all.extend(report_set(&run("analyse", &[dir.path().to_str().unwrap()]))); + all.sort(); + all.dedup(); + all +} + +// --------------------------------------------------------------------------- +// Multi-importer merge. A multi-hop lifecycle is witnessed one transition at a +// time, and the transitions are spread across several consumer modules. Only by +// merging every importer's contributions does the domain see a complete +// lifecycle, so a merge that drops one importer's witness leaves a state with no +// exit — a split report the single-file form never has. +// --------------------------------------------------------------------------- + +fn gen_distributed_lifecycle(seed: u64) -> (String, Vec<(String, String)>) { + let mut rng = Rng::new(seed); + let n = (3 + rng.below(3)) as usize; // 3..=5 states + let k = (2 + rng.below(2)) as usize; // 2..=3 consumers + let e = format!("Job{}", rng.below(100)); + let states: Vec = (0..n).map(|i| format!("s{i}v{}", rng.below(100))).collect(); + let mut trans = String::new(); + for i in 0..n - 1 { + trans.push_str(&format!("{} -> {} ", states[i], states[i + 1])); + } + let entity = format!( + "entity {e} {{\n status: {}\n transitions status {{ {trans}terminal: {} }}\n}}\n", + states.join(" | "), + states[n - 1] + ); + let create = format!( + "rule Create{e} {{\n when: {e}Req()\n ensures: {e}.created(status: {})\n}}\n", + states[0] + ); + let intake = format!("surface {e}Intake {{\n provides:\n {e}Req()\n}}\n"); + let domain_body = format!("{entity}\n{create}\n{intake}"); + + let mut single_witness = String::new(); + let mut consumer_bodies: Vec = vec![String::new(); k]; + for i in 0..n - 1 { + let (from, to) = (&states[i], &states[i + 1]); + single_witness.push_str(&format!( + "rule W{i} {{\n when: b: {e}.status becomes {from}\n ensures: b.status = {to}\n}}\n\n" + )); + consumer_bodies[i % k].push_str(&format!( + "rule W{i} {{\n when: b: dom/{e}.status becomes {from}\n ensures: b.status = {to}\n}}\n\n" + )); + } + let single = format!("-- allium: 3\n\n{domain_body}\n{single_witness}"); + let mut files = vec![("domain.allium".to_string(), format!("-- allium: 3\n\n{domain_body}"))]; + for (c, body) in consumer_bodies.iter().enumerate() { + if !body.is_empty() { + files.push((format!("c{c}.allium"), format!("-- allium: 3\n\nuse \"./domain.allium\" as dom\n\n{body}"))); + } + } + (single, files) +} + +#[test] +fn generative_multi_importer_merge() { + let mut anomalies: Vec = Vec::new(); + for seed in 0..60u64 { + let (single_src, files) = gen_distributed_lifecycle(seed); + let single = reports_of_file(&single_src); + let split = reports_of_set(&files); + if !single.is_empty() { + anomalies.push(format!("[seed {seed}] multi-hop single not clean: {single:?}\n{single_src}")); + } else if single != split { + anomalies.push(format!( + "[seed {seed}] MERGE != SINGLE\n single: {single:?}\n split: {split:?}\n--- files ---\n{}", + files.iter().map(|(n, c)| format!("== {n} ==\n{c}")).collect::>().join("\n") + )); + } + } + assert!( + anomalies.is_empty(), + "\n==== MULTI-IMPORTER MERGE: {} anomalies ====\n\n{}\n", + anomalies.len(), + anomalies.join("\n\n") + ); +} + +// --------------------------------------------------------------------------- +// Combined fuzzer. Every valid dimension at once: a multi-hop lifecycle whose +// transitions each pick a trigger form (becomes / transitions_to / temporal), +// are optionally wrapped in an identical if/else, and are spread across one or +// two consumer modules. The property is unchanged (a valid witness is clean, and +// the split equals the single file); the point is to hit interactions the +// single-dimension generators miss. +// --------------------------------------------------------------------------- + +fn gen_combined(seed: u64) -> (String, Vec<(String, String)>) { + let mut rng = Rng::new(seed); + let n = (3 + rng.below(3)) as usize; // 3..=5 states + let k = (1 + rng.below(2)) as usize; // 1..=2 consumers + let e = format!("Job{}", rng.below(100)); + let states: Vec = (0..n).map(|i| format!("s{i}v{}", rng.below(100))).collect(); + + // Decide per-transition form and wrapping up front. + let forms: Vec = (0..n - 1).map(|_| rng.below(3)).collect(); + let wraps: Vec = (0..n - 1).map(|_| rng.below(2) == 0).collect(); + let temporal_used = forms.contains(&2); + + let mut trans = String::new(); + for i in 0..n - 1 { + trans.push_str(&format!("{} -> {} ", states[i], states[i + 1])); + } + let field = if temporal_used { " due_at: Timestamp\n" } else { "" }; + let entity = format!( + "entity {e} {{\n status: {}\n{field} transitions status {{ {trans}terminal: {} }}\n}}\n", + states.join(" | "), + states[n - 1] + ); + let domain_body = format!( + "{entity}\nrule Create{e} {{\n when: {e}Req()\n ensures: {e}.created(status: {})\n}}\n\nsurface {e}Intake {{\n provides:\n {e}Req()\n}}\n", + states[0] + ); + + let witness = |i: usize, q: &str| -> String { + let (from, to) = (&states[i], &states[i + 1]); + let (trigger, clauses) = match forms[i] { + 0 => (format!("b: {q}{e}.status becomes {from}"), format!("ensures: b.status = {to}")), + 1 => (format!("b: {q}{e}.status transitions_to {from}"), format!("ensures: b.status = {to}")), + _ => ( + format!("m: {q}{e}.due_at <= now"), + format!("requires: m.status = {from}\nensures: m.status = {to}"), + ), + }; + let body = if wraps[i] { + format!("if true:\n{clauses}\nelse:\n{clauses}") + } else { + clauses + }; + format!("rule W{i} {{\n when: {trigger}\n{body}\n}}\n\n") + }; + + let mut single_witness = String::new(); + let mut consumer_bodies: Vec = vec![String::new(); k]; + for i in 0..n - 1 { + single_witness.push_str(&witness(i, "")); + consumer_bodies[i % k].push_str(&witness(i, "dom/")); + } + let single = format!("-- allium: 3\n\n{domain_body}\n{single_witness}"); + let mut files = vec![("domain.allium".to_string(), format!("-- allium: 3\n\n{domain_body}"))]; + for (c, body) in consumer_bodies.iter().enumerate() { + if !body.is_empty() { + files.push((format!("c{c}.allium"), format!("-- allium: 3\n\nuse \"./domain.allium\" as dom\n\n{body}"))); + } + } + (single, files) +} + +#[test] +fn generative_combined_fuzzer() { + let mut anomalies: Vec = Vec::new(); + for seed in 0..150u64 { + let (single_src, files) = gen_combined(seed); + let single = reports_of_file(&single_src); + let split = reports_of_set(&files); + if !single.is_empty() { + anomalies.push(format!("[seed {seed}] combined single not clean: {single:?}\n{single_src}")); + } else if single != split { + anomalies.push(format!( + "[seed {seed}] SPLIT != SINGLE\n single: {single:?}\n split: {split:?}\n--- files ---\n{}", + files.iter().map(|(n, c)| format!("== {n} ==\n{c}")).collect::>().join("\n") + )); + } + } + assert!( + anomalies.is_empty(), + "\n==== COMBINED FUZZER: {} anomalies (of 150 seeds) ====\n\n{}\n", + anomalies.len(), + // Cap the dump so a broad failure stays readable. + anomalies.iter().take(6).cloned().collect::>().join("\n\n") + ); +} + +// --------------------------------------------------------------------------- +// True-positive cross-module detection. Everything above checks that a *valid* +// witness stays clean; this checks the opposite failure mode — that a genuine +// fault is not silently dropped across a split. A multi-hop lifecycle has some of +// its witnessing rules omitted at random (leaving stuck / unreachable states) and +// the surviving witnesses spread across consumer modules. The single-file form is +// the oracle: it reports the real faults. The split must report exactly the same +// set. A split that reports *fewer* faults is over-crediting (hiding a real +// deadlock); one that reports *more* is the false-positive class fixed earlier. +// Only witnesses are omitted (never conflicting effects added), so every finding +// here is a lifecycle fault, which is genuinely cross-module-detectable. +// --------------------------------------------------------------------------- + +fn gen_faulty_lifecycle(seed: u64) -> (String, Vec<(String, String)>) { + let mut rng = Rng::new(seed); + let n = (3 + rng.below(3)) as usize; // 3..=5 states + let k = (1 + rng.below(2)) as usize; // 1..=2 consumers + let e = format!("Job{}", rng.below(100)); + let states: Vec = (0..n).map(|i| format!("s{i}v{}", rng.below(100))).collect(); + // Which transitions are actually witnessed. Omitting one strands its source + // state (and everything past it). + let present: Vec = (0..n - 1).map(|_| rng.below(5) != 0).collect(); // ~80% present + + let mut trans = String::new(); + for i in 0..n - 1 { + trans.push_str(&format!("{} -> {} ", states[i], states[i + 1])); + } + let entity = format!( + "entity {e} {{\n status: {}\n transitions status {{ {trans}terminal: {} }}\n}}\n", + states.join(" | "), + states[n - 1] + ); + let domain_body = format!( + "{entity}\nrule Create{e} {{\n when: {e}Req()\n ensures: {e}.created(status: {})\n}}\n\nsurface {e}Intake {{\n provides:\n {e}Req()\n}}\n", + states[0] + ); + + let mut single_witness = String::new(); + let mut consumer_bodies: Vec = vec![String::new(); k]; + for i in 0..n - 1 { + if !present[i] { + continue; + } + let (from, to) = (&states[i], &states[i + 1]); + single_witness.push_str(&format!( + "rule W{i} {{\n when: b: {e}.status becomes {from}\n ensures: b.status = {to}\n}}\n\n" + )); + consumer_bodies[i % k].push_str(&format!( + "rule W{i} {{\n when: b: dom/{e}.status becomes {from}\n ensures: b.status = {to}\n}}\n\n" + )); + } + let single = format!("-- allium: 3\n\n{domain_body}\n{single_witness}"); + let mut files = vec![("domain.allium".to_string(), format!("-- allium: 3\n\n{domain_body}"))]; + for (c, body) in consumer_bodies.iter().enumerate() { + if !body.is_empty() { + files.push((format!("c{c}.allium"), format!("-- allium: 3\n\nuse \"./domain.allium\" as dom\n\n{body}"))); + } + } + (single, files) +} + +#[test] +fn generative_faults_survive_the_split() { + let mut anomalies: Vec = Vec::new(); + for seed in 0..200u64 { + let (single_src, files) = gen_faulty_lifecycle(seed); + let single = reports_of_file(&single_src); + let split = reports_of_set(&files); + if single != split { + let missing: Vec<_> = single.iter().filter(|r| !split.contains(r)).cloned().collect(); + let extra: Vec<_> = split.iter().filter(|r| !single.contains(r)).cloned().collect(); + anomalies.push(format!( + "[seed {seed}] SPLIT != SINGLE\n dropped by split (false negative): {missing:?}\n extra in split (false positive): {extra:?}\n--- files ---\n{}", + files.iter().map(|(n, c)| format!("== {n} ==\n{c}")).collect::>().join("\n") + )); + } + } + assert!( + anomalies.is_empty(), + "\n==== FAULT SURVIVAL: {} anomalies (of 200 seeds) ====\n\n{}\n", + anomalies.len(), + anomalies.iter().take(6).cloned().collect::>().join("\n\n") + ); +} + +// --------------------------------------------------------------------------- +// Transition-graph chaos. Witnesses assign a *random valid* target status (often +// an edge not in the declared graph), so the single file reports a tangle of +// undeclaredTransition / noExit / unreachable / deadlock findings. The split must +// report exactly that tangle — the analysis is a function of the spec, not the +// module layout, for faulty specs as much as clean ones. Targets are always +// declared status values (never undefined), so the faults are transition-graph +// faults, not undefined-reference noise, and no conflicting effects are added so +// the known cross-module conflict gap is not in play. +// --------------------------------------------------------------------------- + +fn gen_graph_chaos(seed: u64) -> (String, Vec<(String, String)>) { + let mut rng = Rng::new(seed); + let n = (3 + rng.below(3)) as usize; // 3..=5 states + let k = (1 + rng.below(2)) as usize; // 1..=2 consumers + let e = format!("Job{}", rng.below(100)); + let states: Vec = (0..n).map(|i| format!("s{i}v{}", rng.below(100))).collect(); + + let mut trans = String::new(); + for i in 0..n - 1 { + trans.push_str(&format!("{} -> {} ", states[i], states[i + 1])); + } + let entity = format!( + "entity {e} {{\n status: {}\n transitions status {{ {trans}terminal: {} }}\n}}\n", + states.join(" | "), + states[n - 1] + ); + let domain_body = format!( + "{entity}\nrule Create{e} {{\n when: {e}Req()\n ensures: {e}.created(status: {})\n}}\n\nsurface {e}Intake {{\n provides:\n {e}Req()\n}}\n", + states[0] + ); + + // For each source state, maybe witness a transition to a random (declared) + // target — frequently a non-adjacent, undeclared edge. + let mut single_witness = String::new(); + let mut consumer_bodies: Vec = vec![String::new(); k]; + let mut w = 0; + for i in 0..n { + if rng.below(4) == 0 { + continue; // no witness from this state + } + let from = &states[i]; + let to = &states[rng.below(n as u64) as usize]; + if from == to { + continue; // skip trivial self-assignment + } + single_witness.push_str(&format!( + "rule W{w} {{\n when: b: {e}.status becomes {from}\n ensures: b.status = {to}\n}}\n\n" + )); + consumer_bodies[w % k].push_str(&format!( + "rule W{w} {{\n when: b: dom/{e}.status becomes {from}\n ensures: b.status = {to}\n}}\n\n" + )); + w += 1; + } + let single = format!("-- allium: 3\n\n{domain_body}\n{single_witness}"); + let mut files = vec![("domain.allium".to_string(), format!("-- allium: 3\n\n{domain_body}"))]; + for (c, body) in consumer_bodies.iter().enumerate() { + if !body.is_empty() { + files.push((format!("c{c}.allium"), format!("-- allium: 3\n\nuse \"./domain.allium\" as dom\n\n{body}"))); + } + } + (single, files) +} + +#[test] +fn generative_graph_chaos_survives_the_split() { + let mut anomalies: Vec = Vec::new(); + for seed in 0..250u64 { + let (single_src, files) = gen_graph_chaos(seed); + let single = reports_of_file(&single_src); + let split = reports_of_set(&files); + if single != split { + let missing: Vec<_> = single.iter().filter(|r| !split.contains(r)).cloned().collect(); + let extra: Vec<_> = split.iter().filter(|r| !single.contains(r)).cloned().collect(); + anomalies.push(format!( + "[seed {seed}] SPLIT != SINGLE\n dropped by split (false negative): {missing:?}\n extra in split (false positive): {extra:?}\n--- single ---\n{single_src}\n--- files ---\n{}", + files.iter().map(|(n, c)| format!("== {n} ==\n{c}")).collect::>().join("\n") + )); + } + } + assert!( + anomalies.is_empty(), + "\n==== GRAPH CHAOS: {} anomalies (of 250 seeds) ====\n\n{}\n", + anomalies.len(), + anomalies.iter().take(4).cloned().collect::>().join("\n\n") + ); +} + +// --------------------------------------------------------------------------- +// Known gap: cross-module conflict detection. The single-file oracle detects that +// two rules can both fire in `pending` and set conflicting statuses; the split +// does not, because the importer's conflict pass builds `EntityInfo` from the +// local module only and never learns the imported entity's status vocabulary, so +// it cannot attribute either rule to `Job`. This is a false negative (a missed +// finding), not a false positive. Ignored until the conflict pass takes imported +// entity statuses; the fault-survival properties above prove every *other* fault +// class already survives the split, so this is the one remaining detection gap. +// --------------------------------------------------------------------------- + +const CONFLICT_SINGLE: &str = "-- allium: 3\n\nentity Job {\n status: pending | expired | extended\n deadline: Timestamp\n transitions status { pending -> expired pending -> extended terminal: expired, extended }\n}\n\nrule Create {\n when: JobReq()\n ensures: Job.created(status: pending)\n}\n\nrule AutoExpire {\n when: t: Job.deadline <= now\n requires: t.status = pending\n ensures: t.status = expired\n}\n\nrule ManualExtend {\n when: Extend(j)\n requires: j.status = pending\n ensures: j.status = extended\n}\n\nsurface Desk {\n provides:\n JobReq()\n Extend(j: Job)\n}\n"; + +const CONFLICT_DOMAIN: &str = "-- allium: 3\n\nentity Job {\n status: pending | expired | extended\n deadline: Timestamp\n transitions status { pending -> expired pending -> extended terminal: expired, extended }\n}\n\nrule Create {\n when: JobReq()\n ensures: Job.created(status: pending)\n}\n\nsurface JobIntake {\n provides:\n JobReq()\n}\n"; + +const CONFLICT_CONSUMER: &str = "-- allium: 3\n\nuse \"./domain.allium\" as dom\n\nrule AutoExpire {\n when: t: dom/Job.deadline <= now\n requires: t.status = pending\n ensures: t.status = expired\n}\n\nrule ManualExtend {\n when: Extend(j)\n requires: j.status = pending\n ensures: j.status = extended\n}\n\nsurface Ops {\n provides:\n Extend(j: dom/Job)\n}\n"; + +#[test] +fn cross_module_conflict_is_detected_single_file() { + // The oracle: single-file, the conflict is detected. This half is not ignored, + // so the oracle itself stays honest. + let single = reports_of_file(CONFLICT_SINGLE); + assert!( + single.iter().any(|r| r.starts_with("F conflict")), + "single-file oracle must detect the conflict, got {single:?}" + ); +} + +#[test] +fn cross_module_conflict_survives_the_split() { + let single = reports_of_file(CONFLICT_SINGLE); + let split = reports_of_pair(CONFLICT_DOMAIN, CONFLICT_CONSUMER); + assert_eq!(single, split, "the split should report the same conflict as the single file"); +} + +// Guard the other direction of cross-module conflict detection: two importer +// rules that act on the same imported entity but fire on different external +// triggers are an actor's choice, not a race, so no conflict must be invented. +const ACTOR_DOMAIN: &str = "-- allium: 3\n\nentity LeaveRequest {\n status: pending | approved | denied\n transitions status { pending -> approved pending -> denied terminal: approved, denied }\n}\n\nrule Create {\n when: LeaveReq()\n ensures: LeaveRequest.created(status: pending)\n}\n\nsurface Intake {\n provides:\n LeaveReq()\n}\n"; + +const ACTOR_CONSUMER: &str = "-- allium: 3\n\nuse \"./domain.allium\" as dom\n\nrule Approve {\n when: ManagerApproves(m, r)\n requires: r.status = pending\n ensures: r.status = approved\n}\n\nrule Deny {\n when: ManagerDenies(m, r)\n requires: r.status = pending\n ensures: r.status = denied\n}\n\nsurface Ops {\n provides:\n ManagerApproves(m, r: dom/LeaveRequest)\n ManagerDenies(m, r: dom/LeaveRequest)\n}\n"; + +#[test] +fn cross_module_actor_choice_is_not_a_conflict() { + let split = reports_of_pair(ACTOR_DOMAIN, ACTOR_CONSUMER); + assert!( + !split.iter().any(|r| r.starts_with("F conflict")), + "actor-choice across a module must not be reported as a conflict: {split:?}" + ); + // The single file agrees (no conflict), so this is genuinely split-invariant. + let single = reports_of_file(&format!( + "{}\n{}", + ACTOR_DOMAIN, + ACTOR_CONSUMER.replace("-- allium: 3\n\nuse \"./domain.allium\" as dom\n\n", "").replace("dom/", "") + )); + assert_eq!(single, split, "actor-choice split should match the single file"); +} diff --git a/docs/project/specs/allium-analyse-tool-behaviour.allium b/docs/project/specs/allium-analyse-tool-behaviour.allium index 63dffe0..bb9676e 100644 --- a/docs/project/specs/allium-analyse-tool-behaviour.allium +++ b/docs/project/specs/allium-analyse-tool-behaviour.allium @@ -240,6 +240,25 @@ rule ConflictDetected { ) } +-- Reverse cross-module aggregation: a conflict between two importer rules acting +-- on an imported entity is detected the same as when the entity is local. The +-- importer's conflict pass is given the imported entity's status vocabulary, so +-- it can attribute both rules to the entity by the statuses they read and write. +-- An actor's choice (rules on different call triggers) is still not a conflict. + +rule ConflictDetectedOnImportedEntity { + when: RulePairAnalysed(rule_a, rule_b, entity, state) + requires: entity is imported by the analysed file via a use alias + requires: RulesShareOverlappingRequiresState(rule_a, rule_b, entity, state) = true + requires: RulesSetConflictingEnsuresValues(rule_a, rule_b, entity) = true + requires: NotBothCallTriggered(rule_a, rule_b) = true + + ensures: AnalyseFinding.created( + type: conflict, + summary: "Rules can both fire in the same state, setting conflicting values" + ) +} + -- Invariant risk finding rule InvariantRiskDetected { diff --git a/docs/project/specs/allium-check-tool-behaviour.allium b/docs/project/specs/allium-check-tool-behaviour.allium index b98013b..a3ef301 100644 --- a/docs/project/specs/allium-check-tool-behaviour.allium +++ b/docs/project/specs/allium-check-tool-behaviour.allium @@ -385,34 +385,43 @@ rule QualifiedProvidesCreditsImportedTriggerReachability { ensures: FindingNotObserved(code: "allium.rule.unreachableTrigger", trigger: trigger) } --- A qualified provides entry's spelling is load-bearing (it gates crediting), --- so both halves of the reference are resolution-checked at the entry, rather --- than surfacing only as a misleading downstream unreachableTrigger on the --- imported module (#72). +-- A qualified reference alias/Name at any site — a when trigger or entity +-- subject, a provides entry, a surface context, an inline parameter type, a +-- field type, a .created call, a default, a contract clause — must name a +-- module a use declaration binds. An undeclared alias is a locally-knowable +-- typo, diagnosed once at the reference by a single pass over every qualified +-- reference, single-file and multi-file alike (#72, #78 and the sites audit). -rule UnknownProvidesAliasIsDiagnosedAtEntry { +rule UndeclaredImportAliasIsDiagnosedAtEveryReferenceSite { when: CheckCommandInvokedWithInputs(inputs) - requires: a surface provides a trigger qualified by an alias that no use declaration binds + requires: a qualified reference alias/Name appears at any site + requires: no use declaration in the module binds alias - ensures: FindingObserved(code: "allium.provides.undefinedImportedAlias", severity: error) - ensures: FindingMessage anchored at the provides entry names the unknown alias + ensures: FindingObserved(code: "allium.reference.undefinedImportedAlias", severity: error) + ensures: FindingMessage anchored at the reference names the unknown alias } -rule UnknownProvidesTriggerIsDiagnosedAtEntry { +-- Beyond the alias, the name itself must resolve: with a valid alias whose +-- target is in the check set, a qualified reference alias/Name where the aliased +-- module offers no such name (a declared type or a referenced trigger) is +-- diagnosed at the reference. Same unified pass, every site (#72 and the +-- name-existence audit). A target outside the check set is unknowable. + +rule UnknownImportedNameIsDiagnosedAtEveryReferenceSite { when: CheckCommandInvokedWithInputs(inputs) requires: inputs resolve to multiple files - requires: a surface provides alias/Trigger where alias's target is in the check set - requires: the aliased module never references trigger + requires: a qualified reference alias/Name where a use declaration binds alias to a file in the check set + requires: the aliased module offers no declared type or referenced trigger named Name - ensures: FindingObserved(code: "allium.provides.unknownTrigger", severity: warning) - ensures: FindingMessage anchored at the provides entry names the unknown trigger + ensures: FindingObserved(code: "allium.reference.unknownName", severity: warning) + ensures: FindingMessage anchored at the reference names the unknown name } -rule ProvidesTriggerOutsideCheckSetNotFlagged { +rule QualifiedNameOutsideCheckSetNotFlagged { when: CheckCommandInvokedWithInputs(inputs) - requires: a surface provides alias/Trigger where alias's target is outside the check set + requires: a qualified reference alias/Name where alias's target is outside the check set - ensures: FindingNotObserved(code: "allium.provides.unknownTrigger", trigger: trigger) + ensures: FindingNotObserved(code: "allium.reference.unknownName", name: Name) } rule WitnessedTransitionCreditsImportedLifecycle {