The language reference does not say whether a provides argument references a surface binding or declares a fresh action input

[bombaywalla]

Summary

The arguments in a surface's provides entries can match the
surface's bindings or match nothing, and the reference's whole
statement about them is one table cell: "parameters are per-action
inputs from the party"
(language-reference.md L1785).
Its own examples pass both kinds side by side in one entry —
InterviewerDeclinesAssignment(viewer, assignment, reason?), where
viewer and assignment are the surface's facing and context
bindings and reason? matches no binding
(L1806-L1808).
The bundled patterns mix the kinds the same way throughout, for
example AddMemberToWorkspace(admin, workspace, new_user, role) with
two binding-matching and two unmatched names
(patterns.md L582).
The reference does not state what either kind means or how they are
told apart. It does
state a resolution rule for the neighboring construct: for trigger
emission arguments, "bound names are resolved first", and "Bare
identifiers that resolve to neither a binding nor an enum literal
are a checker warning"
(language-reference.md L946).
That rule treats an unresolvable bare name as a mistake, where the
tools treat the same shape in a provides entry as a declaration.

In the reference's silence, the tools have adopted an
interpretation. Where the distinction is load-bearing — the
cross-module witness crediting below — the lifecycle collectors
resolve by name matching:

• a positional argument that matches a context or facing binding
  is treated as a reference carrying that binding's type
  (analysis.rs L4704-L4790),
• an argument that matches nothing is treated as declaring a fresh,
  untyped action input, and
• a name: value form is treated as typing a fresh input:
  name: alias/Entity in the importing module
  (L4777-L4780),
  or name: Entity in the module that owns the entity
  (collect_command_param_types, L2644-L2693).
  Measured: an unqualified s: Ticket in the importer contributes
  no imported-entity lifecycle typing in this arrangement
  (console-unqualified.allium).

The parser itself carries no type reading: name: value parses
generically as a named call argument whose value is an arbitrary
expression
(parse_call_args, parser.rs L2321-L2341).
The collectors recognise the forms for status-bearing entities,
which is what lifecycle analysis needs. Whether the name: value
forms are type syntax for provides inputs generally, or an analysis
convention, is part of what is undocumented. No such form appears
in a provides entry anywhere in the reference or the bundled
patterns. The name: Type shapes that do occur elsewhere are
contract and black-box function parameter declarations.

The distinction is load-bearing across modules. Since
allium-tools#65 /
PR #69, for an
importer that owns its trigger, the provides argument is the typing
channel that credits its rule as a transition witness for the
imported entity. In the demonstration below, the first three
consoles differ only in one provides argument:

• Argument t, matching the context binding: the pair is completely
  clean. check 0, analyse 0.
• Argument s, matching nothing: the imported domain reports
  status.noExit, status.unreachableValue, and a deadlock
  finding. check 1, analyse 1.
• Argument s: tickets/Ticket: completely clean again. check 0,
  analyse 0.

The checker accepts all three arrangements, and under the tools'
fresh-input interpretation the middle one is handled consistently.
Between the first two, one identifier silently changes another
module's lifecycle analysis, and a reader has no documented rule to
predict or interpret any of the three outcomes. What (s) means —
a deliberate fresh input, or an unresolved reference — is a question
about the spec itself, and today its only answer is tool behavior.

#40 shows why this
matters beyond convenience. There, a trigger-parameter dispute was
settled by consulting the reference — the resolving comment turns on
"After checking against the language reference". For
provides-argument resolution there is no rule to consult.

The ask

An addition to the surface documentation that makes the intended
semantics explicit. Three questions it would settle:

• Does a positional argument that matches a context or facing
  binding denote that binding, or does it declare a separate
  party-supplied input that merely shares the name?
• Is an unmatched name intended to declare a fresh input, given that
  the emission-argument rule treats an unresolvable bare name as a
  checker warning?
• Are the name: Entity and name: alias/Entity forms type syntax
  for provides inputs generally, or a lifecycle-analysis
  convention — and if normative, for which types?

If the tools' current interpretation is the intended semantics,
documenting it is the whole fix, and
allium-tools#76's
workaround already leans on the qualified form. If it is not,
the reference is where the correction starts. Whether the tooling
should additionally mark a fresh input that matches no surface
binding (or a rename that flips a reference to fresh) is a checker
question for the tools repo, and it is left out of this ask.

Demonstration

The files below are complete. Save the domain and any console side
by side and run allium check ticket.allium <console>.allium (and
analyse likewise) with CLI 3.5.2.

ticket.allium (the domain)

-- allium: 3
-- ticket.allium
--
-- The domain.  Declares the transition the console witnesses.  The
-- console's provides argument is what carries the witness typing
-- across the module boundary.

entity Ticket {
    status: closed | archived

    transitions status {
        closed -> archived
        terminal: archived
    }
}

rule CreateTicket {
    when: CreateTicketRequested()
    ensures: Ticket.created(status: closed)
}

surface TicketIntake {
    provides:
        CreateTicketRequested()
}

console-bound.allium (arrangement 1)

-- allium: 3
-- console-bound.allium
--
-- Arrangement 1.  The provides argument `t` matches the context
-- binding and is treated as a reference to it: the trigger's
-- parameter carries the imported entity's type and the pair is
-- completely clean.

use "./ticket.allium" as tickets

surface ArchiveDesk {
    context t: tickets/Ticket

    provides:
        ArchiveTicketRequested(t)
            when t.status = closed
}

rule ArchiveClosedTicket {
    when: ArchiveTicketRequested(ticket)
    requires: ticket.status = closed
    ensures: ticket.status = archived
}

console-fresh.allium (arrangement 2)

-- allium: 3
-- console-fresh.allium
--
-- Arrangement 2.  One identifier differs from arrangement 1: the
-- argument is `s`, which matches no surface binding and is treated
-- as declaring a fresh untyped action input.  Nothing marks the
-- change.  The witness typing is gone and the domain reports
-- noExit, unreachableValue, and a deadlock finding.

use "./ticket.allium" as tickets

surface ArchiveDesk {
    context t: tickets/Ticket

    provides:
        ArchiveTicketRequested(s)
            when t.status = closed
}

rule ArchiveClosedTicket {
    when: ArchiveTicketRequested(ticket)
    requires: ticket.status = closed
    ensures: ticket.status = archived
}

console-typed.allium (arrangement 3)

-- allium: 3
-- console-typed.allium
--
-- Arrangement 3.  The same unmatched name `s` with an inline
-- qualified `name: value` form (`s: tickets/Ticket`).  The analyser
-- supports the form and the pair is completely clean, though the
-- reference does not document it.

use "./ticket.allium" as tickets

surface ArchiveDesk {
    context t: tickets/Ticket

    provides:
        ArchiveTicketRequested(s: tickets/Ticket)
            when t.status = closed
}

rule ArchiveClosedTicket {
    when: ArchiveTicketRequested(ticket)
    requires: ticket.status = closed
    ensures: ticket.status = archived
}

console-unqualified.allium (arrangement 4)

-- allium: 3
-- console-unqualified.allium
--
-- Arrangement 4.  The same form as arrangement 3 without the
-- qualifier (`s: Ticket`).  In an importing module it contributes
-- no imported-entity lifecycle typing: the reports are the same as
-- arrangement 2's.  The unqualified form is recognised in the
-- module that owns the entity.

use "./ticket.allium" as tickets

surface ArchiveDesk {
    context t: tickets/Ticket

    provides:
        ArchiveTicketRequested(s: Ticket)
            when t.status = closed
}

rule ArchiveClosedTicket {
    when: ArchiveTicketRequested(ticket)
    requires: ticket.status = closed
    ensures: ticket.status = archived
}

Measured results, all on CLI 3.5.2:

• Arrangement 1: completely clean. check 0, analyse 0.
• Arrangement 2: both commands report the two warnings on the
  domain, and analyse adds the deadlock finding. check 1,
  analyse 1.
• Arrangement 3: completely clean. check 0, analyse 0.
• Arrangement 4: the same reports as arrangement 2. check 1,
  analyse 1.

Related

• #40 ruled trigger
  parameter lists bare-names-only, so a subscriber cannot annotate
  its own binding. The provides entry is therefore the one typing
  source the tools currently support for an external-stimulus
  parameter, which raises the cost of leaving it undocumented.
• #38 is the precedent
  for docs-only additions to the bundled references (an accepted ask
  for a patterns.md example).
• allium-tools#65 /
  PR #69 made the
  provides argument the cross-module typing channel for an importer
  that owns its trigger.
• allium-tools#76's
  measured workaround is the name: alias/Entity form whose status
  this issue asks the reference to clarify.

Version: allium CLI 3.5.2 (language versions 1, 2, 3), Homebrew
arm64 macOS. Language reference and patterns cited at juxt/allium
899cb05e.