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.

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.