Skip to content

Export every ensures emission and otherwise: emissions, not just the first statement - #90

Merged
henrygarner merged 1 commit into
juxt:mainfrom
yenda:fix/ensures-emissions-export
Aug 26, 2026
Merged

Export every ensures emission and otherwise: emissions, not just the first statement#90
henrygarner merged 1 commit into
juxt:mainfrom
yenda:fix/ensures-emissions-export

Conversation

@yenda

@yenda yenda commented Aug 13, 2026

Copy link
Copy Markdown
Contributor

Fixes #88.

Bug

When building the set of names a module exports (and the local emitted-trigger set), the checker registered only the first statement of each rule's ensures: block — a compatibility remnant of the old TS regex, per the comment it carried. A trigger emitted as the second or later statement, even when the first statement is itself another emission, was invisible to importers:

  • every qualified reference to it drew a false allium.reference.unknownName warning (exit 1),
  • its cross-module consumers drew a false info-level allium.rule.unreachableTrigger,
  • local listeners of a mid-block emission drew the same false unreachable info.

Triggers emitted only through requires: ... otherwise: SomeError(...) were invisible the same way (they parse as an assignment item named otherwise, which no collector visited).

Repro (fails on main, passes on this branch — transcribed into cross_module_lifecycle.rs):

rule EmissionAfterEmission {
    when: Do2(x)

    ensures:
        FirstEmitted(value: x)
        SecondEmitted(value: x)   -- consumers of this one warned unknownName
}

Why reordering was never a workaround

A block emitting two triggers can export at most one under first-statement-only rules. And the single exportable slot is often pinned by data dependencies — an emission referencing a binding a let above it creates cannot move first.

Fix

collect_leading_ensures_call becomes collect_ensures_emission_calls: every block item whose top-level expression is a bare PascalCase call is an emission — first or not. Value-producing calls nested inside assignments, let bindings or arguments are still not collected, so the emission/black-box-call distinction is preserved. otherwise: values join the emitted set via a new arm in collect_emitted_trigger_from_item.

The parse layer needed no change: allium parse already contains every emission as a structured Call node — the loss happened only in the resolution layer.

Tests

  • 3 unit tests (local reachability: second-position, post-assignment, and otherwise: emissions; plus a guard that a trigger nothing emits stays unreachable)
  • 2 integration tests (cross-module: consumers of SecondEmitted / AfterAssignEmitted / otherwise-emitted triggers draw no diagnostics; a trigger the provider never mentions still warns)
  • Full workspace suite green: 651 tests, 0 failures. No existing test pinned the leading-only behaviour.

Real-world impact

On a ~180-spec production corpus, the v3.5.0 → v3.5.3 upgrade surfaced 4 false unknownName warnings of exactly this shape (a login spec consuming triggers its auth-OTP module emits mid-ensures), forcing per-site suppression comments. With this fix those suppressions become unnecessary.


Note: this PR and the config/deferred one both append tests to cross_module_lifecycle.rs and the analysis.rs test module — whichever merges second needs a trivial union rebase; happy to rebase promptly.

…first statement

The module export table (and the local emitted-trigger set) registered only
the leading call of each ensures block, a compatibility remnant of the old TS
regex. A trigger emitted as the second statement — even when the first
statement is itself another emission — was invisible to importers: every
qualified reference to it drew a false allium.reference.unknownName warning
and its consumers a false allium.rule.unreachableTrigger, although the
emission is right there in the provider's text. Triggers emitted only through
a `requires: ... otherwise:` clause were invisible the same way.

Reordering cannot work around it: a block emitting two triggers can export at
most one under first-statement-only rules, and the exportable slot is often
pinned by data dependencies (an emission referencing a binding a let above it
creates cannot move first).

collect_leading_ensures_call becomes collect_ensures_emission_calls: every
block item whose top-level expression is a bare PascalCase call is an
emission. Value-producing calls nested in assignments, lets or arguments are
still not collected. otherwise: emissions (parsed as an assignment item named
'otherwise') join the emitted set.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@henrygarner
henrygarner merged commit ee44727 into juxt:main Aug 26, 2026
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

check: only the first statement of an ensures: block is exported to importers — later emissions produce false unknownName on every consumer

2 participants