Declaring action signatures

Theorem files that reference actions in Let or Do must declare the expected Rust signature for each referenced action in a top-level Actions mapping. The theorem document is the source of truth for this contract; the macro checks it against the Rust export during compilation.

Actions:
  account.deposit:
    params:
      account: "&mut crate::account::Account"
      amount: u64
    returns: "Result<(), crate::account::DepositError>"

Each Actions key is the canonical action name used by Let and Do. Parameter order is the order written in params, and returns defaults to (). Parameter and return values are Rust type strings.

During theorem_file! expansion, theoremc mangles the canonical action name and emits a compile-time probe of this form:

const _: fn(&mut crate::account::Account, u64) -> Result<(), crate::account::DepositError> =
    crate::theorem_actions::account__deposit__h05158894bfb4;

If the crate::theorem_actions export is missing, renamed, or has a different signature, the theorem owner crate fails to compile.

A theorem file may hold several documents, and more than one of them may declare the same action. Repeated declarations are expected and need not be identical character for character, but they must describe the same Rust signature. The first declaration in document order is the reference; a later declaration that is not semantically equivalent is rejected. The diagnostic names the action, both declaring theorems, and both signatures:

error: referenced action `account.deposit` has conflicting Actions signatures:
theorem `FirstConflict` declares `fn(account: u64) -> bool`, but theorem
`SecondConflict` declares `fn(account: u32) -> bool`
 --> src/lib.rs:3:1

Equivalence requires the same parameter names in the same order as well as equivalent types, so a declaration that renames or reorders a parameter conflicts even when the parameter and return types are unchanged. Types are compared by their parsed tokens, so insignificant whitespace such as Vec<u8> versus Vec < u8> does not cause a conflict. Parenthesized types are not normalized: (u64) and u64 parse to different tokens and are reported as conflicting, so write the grouped and ungrouped forms consistently.

The macro also emits referenced-type probes for every distinct type named by Forall, Actions.params, and Actions.returns. These probes are ordinary Rust items outside the Kani-only module, so missing or moved type paths fail in normal cargo build:

Forall:
  account: crate::account::Account
Actions:
  account.deposit:
    params:
      command: crate::account::DepositCommand
    returns: crate::account::DepositOutcome

If crate::account::DepositCommand is renamed or moved, compilation fails while expanding theorem_file!. Referenced-type probes only check that Rust can resolve the declared type path. Typed action probes separately check that the mangled crate::theorem_actions::* function exists and has the declared signature.