Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
25 commits
Select commit Hold shift + click to select a range
da6a0a9
Add witness-matrix and alias-anchoring sweeps (discovery harness)
henrygarner Aug 5, 2026
2fc615b
Unwrap a where clause when typing a qualified surface context (#76)
henrygarner Aug 5, 2026
4e5d6a8
Type a cross-module witness from a rule-emitted event (#77)
henrygarner Aug 5, 2026
36e08ef
Diagnose an undeclared import alias at every qualified-reference site…
henrygarner Aug 5, 2026
d0c55be
Widen sweeps; fix reverse channel skipping if/else ensures in a witness
henrygarner Aug 5, 2026
72ffc6f
Diagnose a nonexistent qualified name at every reference site (name-e…
henrygarner Aug 5, 2026
15de287
Type an emitter's binding from surface params in the reverse channel
henrygarner Aug 5, 2026
789ed12
Descend into branches for qualified creation in the reverse channel
henrygarner Aug 5, 2026
a66ff92
Descend into branches for qualified emission typing and undefined bin…
henrygarner Aug 5, 2026
7f82305
Guard branch-nesting invariance for undefined-binding detection
henrygarner Aug 5, 2026
4082a89
Descend into branches when checking rule type references
henrygarner Aug 5, 2026
1130d0d
Descend into branches for conflict and determinism effect analysis
henrygarner Aug 5, 2026
878f91e
Note the benign top-level-only scan in the bare-entity binding anchor
henrygarner Aug 5, 2026
81b8236
Unwrap where/with/optional type refinements in every binding-type res…
henrygarner Aug 5, 2026
d011826
Credit temporal-triggered transitions and their field refs across mod…
henrygarner Aug 5, 2026
8bf4efa
Add generative branch/split-invariance properties and CLI smoke tests…
henrygarner Aug 5, 2026
5d0c865
Add deep-nesting branch invariance and generative multi-importer merg…
henrygarner Aug 5, 2026
8bd0ba3
Add combined metamorphic fuzzer over hop-count, trigger form, branch …
henrygarner Aug 5, 2026
6cbb0b3
Use contains in fuzzer to satisfy clippy
henrygarner Aug 5, 2026
704c0a2
Add declaration-order invariance property
henrygarner Aug 5, 2026
3692608
Add true-positive property: lifecycle faults survive the module split
henrygarner Aug 5, 2026
bc39c1e
Add transition-graph chaos oracle: faulty specs survive the split ide…
henrygarner Aug 5, 2026
9d90d13
Document cross-module conflict-detection gap with an oracle and ignor…
henrygarner Aug 5, 2026
f3edea9
Detect conflicts on imported entities: thread imported status vocabul…
henrygarner Aug 5, 2026
f5d3341
Document cross-module conflict detection in the analyse behaviour spec
henrygarner Aug 5, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
898 changes: 643 additions & 255 deletions crates/allium-parser/src/analysis.rs

Large diffs are not rendered by default.

3 changes: 2 additions & 1 deletion crates/allium-parser/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
};
Expand Down
48 changes: 43 additions & 5 deletions crates/allium/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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<PathBuf, ReverseContributions>,
/// 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<PathBuf, HashMap<String, HashSet<String>>>,
}

/// Shared loop for commands that process multiple .allium files.
Expand All @@ -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<String>, &HashSet<String>, &HashMap<String, HashSet<String>>, &HashMap<String, HashMap<String, HashSet<String>>>, &AmbiguousImports, &ReverseContributions, &HashMap<String, HashSet<String>>) -> FileResult,
analyse_file: impl Fn(&Path, &str, &allium_parser::ParseResult, &SourceMap, &HashSet<String>, &HashSet<String>, &HashMap<String, HashSet<String>>, &HashMap<String, HashMap<String, HashSet<String>>>, &AmbiguousImports, &ReverseContributions, &HashMap<String, HashSet<String>>, &HashMap<String, HashSet<String>>) -> FileResult,
) -> ExitCode {
let files = resolve_files(args);
if files.is_empty() {
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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<PathBuf, HashMap<String, HashSet<String>>> = 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).
Expand Down Expand Up @@ -359,6 +376,8 @@ fn build_cross_module_context(parsed: &[ParsedFile]) -> CrossModuleContext {
PathBuf,
HashMap<String, HashMap<String, HashSet<String>>>,
> = HashMap::new();
let mut imported_entity_statuses: HashMap<PathBuf, HashMap<String, HashSet<String>>> =
HashMap::new();
let mut ambiguous_imports: HashMap<PathBuf, AmbiguousImports> = HashMap::new();

for pf in parsed {
Expand Down Expand Up @@ -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<String, HashSet<String>> = 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
Expand Down Expand Up @@ -529,6 +564,7 @@ fn build_cross_module_context(parsed: &[ParsedFile]) -> CrossModuleContext {
imported_referenced_triggers,
ambiguous_imports,
reverse_contributions,
imported_entity_statuses,
}
}

Expand All @@ -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<serde_json::Value> = result
.diagnostics
Expand All @@ -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<serde_json::Value> = result
.diagnostics
.iter()
Expand Down
87 changes: 87 additions & 0 deletions crates/allium/tests/cli_smoke.rs
Original file line number Diff line number Diff line change
@@ -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::<serde_json::Value>(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);
}
8 changes: 4 additions & 4 deletions crates/allium/tests/cross_module_lifecycle.rs
Original file line number Diff line number Diff line change
Expand Up @@ -970,23 +970,23 @@ 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::<Vec<_>>()
);

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::<Vec<_>>()
);

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::<Vec<_>>()
Expand Down
Loading