ExMaude Usage Rules

Guidelines for AI agents and developers working with ExMaude - Elixir bindings for the Maude formal verification system.

Every backend enforces the same :max_response_bytes ceiling (16 MiB by default). A response that crosses it returns %ExMaude.Error{type: :response_too_large} and retires the worker; retry only after reducing the Maude command's output or deliberately raising the limit.

Overview

ExMaude provides a high-level Elixir API for interacting with Maude, a formal specification language based on rewriting logic. It manages independent Maude processes through a pluggable Port, C-Node, or NIF backend and a Poolboy worker pool.

Core Concepts

Maude Operations

• reduce - Apply equations to simplify a term to normal form (deterministic)
• rewrite - Apply rules and equations (may be non-deterministic)
• search - Explore state space to find states matching a pattern
• load_file - Load a Maude module file into all workers
• ensure_file_loaded - Idempotently load a file on concurrent runtime paths

Module Types in Maude

• fmod ... endfm - Functional modules with equations only
• mod ... endm - System modules with rules and equations

API Usage

Reducing Terms

# GOOD: Use reduce for deterministic computation
{:ok, "6"} = ExMaude.reduce("NAT", "1 + 2 + 3")

# GOOD: Handle errors
case ExMaude.reduce("NAT", term) do
  {:ok, result} -> process(result)
  {:error, %ExMaude.Error{type: :parse_error}} -> handle_parse_error()
  {:error, %ExMaude.Error{type: :timeout}} -> retry_or_fail()
end

# BAD: Ignoring errors
{:ok, result} = ExMaude.reduce("NAT", user_input)  # Will crash on error

Rewriting Terms

# GOOD: Set max_rewrites to prevent infinite loops
{:ok, result} = ExMaude.rewrite("MY-MOD", "initial", max_rewrites: 100)

# BAD: Unlimited rewrites on potentially non-terminating rules
{:ok, result} = ExMaude.rewrite("MY-MOD", "initial")

Searching State Space

# GOOD: Set reasonable bounds
{:ok, solutions} = ExMaude.search("MY-MOD", "init", "goal",
  max_depth: 10,
  max_solutions: 5,
  timeout: 30_000
)

# GOOD: Use appropriate search arrows
# =>1  exactly one step
# =>+  one or more steps  
# =>*  zero or more steps (default)
# =>!  to normal form only

# Defaults: at most one solution, depth 100, and the configured command timeout
{:ok, solutions} = ExMaude.search("MY-MOD", "init", "goal")

Loading Modules

# GOOD: Check file exists or handle error
case ExMaude.load_file(path) do
  :ok -> :loaded
  {:error, %ExMaude.Error{type: :file_not_found}} -> create_or_fail()
end

# GOOD: Avoid duplicate broadcasts when concurrent requests need the same file
:ok = ExMaude.ensure_file_loaded(path, pool: :verification_pool)

# GOOD: Load from string for dynamic modules
ExMaude.load_module("""
fmod MY-MOD is
  sort Foo .
  op bar : -> Foo .
endfm
""")

# GOOD: Use bundled IoT module
:ok = ExMaude.load_file(ExMaude.iot_rules_path())

File loads retain their original paths so relative imports resolve correctly. Keep these files available for replacement workers. String modules use private cache files that are removed when the owning pool exits. Failed preloads prevent a worker from starting; correct the file before restarting the pool.

IoT Conflict Detection

ExMaude includes an equational conflict model for IoT automation rules.

Using the High-Level API

# GOOD: Use ExMaude.IoT module for conflict detection
rules = [
  %{
    id: "motion-light",
    thing_id: "light-1",
    trigger: {:prop_eq, "motion", true},
    actions: [{:set_prop, "light-1", "state", "on"}],
    priority: 1
  },
  %{
    id: "night-mode",
    thing_id: "light-1",
    trigger: {:prop_gt, "time", 2300},
    actions: [{:set_prop, "light-1", "state", "off"}],
    priority: 1
  }
]

{:ok, conflicts} = ExMaude.IoT.detect_conflicts(rules)

# GOOD: Validate rules before detection
:ok = ExMaude.IoT.validate_rule(rule)
{:error, errors} = ExMaude.IoT.validate_rule(%{})

Conflict Types

• state_conflict - Same device, incompatible state changes
• env_conflict - Opposing environmental effects
• state_cascade - Rule output triggers another rule
• state_env_cascade - Combined state-environment cascading

Rule Structure

# Rule map structure
%{
  id: String.t(),           # Required: unique identifier
  thing_id: String.t(),     # Required: target device
  trigger: trigger(),       # Required: condition
  actions: [action()],      # Required: list of actions
  priority: integer()       # Optional: defaults to 1
}

# Trigger types
{:prop_eq, property, value}
{:prop_gt, property, number}
{:prop_lt, property, number}
{:env_eq, property, value}
{:always}
{:and, trigger, trigger}
{:or, trigger, trigger}
{:not, trigger}

# Action types
{:set_prop, thing_id, property, value}
{:set_env, property, value}
{:invoke, thing_id, action_name}

Structured Types

ExMaude.Term

# Parse Maude output into structured term
{:ok, term} = ExMaude.Term.parse("result Nat: 42")
term.value  #=> "42"
term.sort   #=> "Nat"

# Convert to Elixir types
{:ok, 42} = ExMaude.Term.to_integer(term)
{:ok, true} = ExMaude.Term.to_boolean(bool_term)

ExMaude.Error

# Errors are structured with type and message
%ExMaude.Error{
  type: :parse_error | :module_not_found | :timeout | :maude_crash | ...,
  message: String.t(),
  details: map() | nil
}

# Check if error is recoverable
ExMaude.Error.recoverable?(error)  #=> true for :timeout, :maude_crash

Configuration

# config/config.exs
config :ex_maude,
  maude_path: "/usr/local/bin/maude",  # Path to Maude binary
  pool_size: 4,                        # Worker processes
  pool_max_overflow: 2,                # Extra workers under load
  timeout: 5_000,                      # Default command timeout (ms)
  preload_modules: [],                 # Modules to load on every pool at startup
  telemetry_include_commands: false    # Secure default: command text is omitted

Pool Management

# GOOD: the host owns placement, lifecycle, and configuration
children = [
  ExMaude.Pool.child_spec(name: :verification_pool, pool_size: 4)
]

# GOOD: Let the pool manage workers automatically
{:ok, result} = ExMaude.reduce("NAT", "1 + 2")

# GOOD: Use transaction for multiple operations on same worker
ExMaude.Pool.transaction(fn worker ->
  ExMaude.Server.load_file(worker, path)
  ExMaude.Server.execute(worker, "reduce in MY-MOD : term .")
end, pool: :verification_pool)

# GOOD: Broadcast to all workers for module loading
{:ok, results} = ExMaude.Pool.broadcast(fn worker ->
  ExMaude.Server.load_file(worker, path)
end)

# GOOD: high-level loading supports named pools; use the idempotent form on
# concurrent runtime paths
:ok = ExMaude.ensure_file_loaded(path, pool: :verification_pool)

Backend Selection

ExMaude provides three backends with different deployment requirements:

config :ex_maude, backend: :port    # default — text I/O, full process isolation
config :ex_maude, backend: :cnode   # C bridge over Erlang distribution
config :ex_maude, backend: :nif     # Rustler NIF managing subprocess pipes

Precompiled NIF binaries are attached to GitHub releases and verified by checksums shipped in the Hex package for macOS aarch64/x86_64, Linux gnu/musl × aarch64/x86_64, and Windows gnu/msvc. On platforms outside that list, force a local build:

EX_MAUDE_BUILD=1 mix deps.compile ex_maude

Verify availability at runtime:

ExMaude.Backend.available_backends()
#=> [:port, :cnode, :nif]

Error Handling Patterns

# GOOD: Pattern match on error types
case ExMaude.reduce("MOD", term) do
  {:ok, result} -> 
    {:ok, result}
  {:error, %ExMaude.Error{type: :timeout}} -> 
    {:error, :retry_later}
  {:error, %ExMaude.Error{type: :parse_error, message: msg}} -> 
    {:error, {:invalid_term, msg}}
  {:error, %ExMaude.Error{type: :module_not_found}} -> 
    {:error, :load_module_first}
  {:error, error} -> 
    {:error, error}
end

# GOOD: Use recoverable? for retry logic
if ExMaude.Error.recoverable?(error) do
  retry(operation)
else
  fail(error)
end

Testing

# Integration tests require Maude
# Tag with @moduletag :integration or @tag :integration

defmodule MyTest do
  use ExMaude.MaudeCase
  
  @moduletag :integration
  
  test "reduces term", %{maude_available: true} do
    {:ok, "6"} = ExMaude.reduce("NAT", "1 + 2 + 3")
  end
end

# Run integration tests
# mix test --include integration

Common Mistakes

Don't construct Maude syntax manually when APIs exist

# BAD: Manual Maude command construction
ExMaude.execute("reduce in CONFLICT-DETECTOR : detectConflicts(...) .")

# GOOD: Use the IoT API
ExMaude.IoT.detect_conflicts(rules)

Don't ignore timeouts

# BAD: Default timeout may be too short for complex operations
ExMaude.search("MOD", "init", "goal")

# GOOD: Set appropriate timeout
ExMaude.search("MOD", "init", "goal", timeout: 60_000)

Don't forget to load modules

# BAD: Using module before loading
ExMaude.reduce("MY-CUSTOM-MOD", term)  # Will fail

# GOOD: Load first; use ensure_file_loaded when multiple callers may race
:ok = ExMaude.ensure_file_loaded("my-custom-mod.maude")
{:ok, result} = ExMaude.reduce("MY-CUSTOM-MOD", term)

AI Rules (v0.2.0+)

ExMaude.AI is the parallel API to ExMaude.IoT for AI-generated rules over Agents, Capabilities, ToolInvocations, and richer predicates. It targets the bundled priv/maude/ai-rules.maude template.

Supported predicate shapes

# Property-style (carry-over from iot-rules)
{:prop_eq, "key", value}
{:prop_gt, "key", value}
{:prop_lt, "key", value}
{:prop_gte, "key", value}
{:prop_lte, "key", value}

# Capability ontology
{:capability_required, "name"}
{:capability_granted, "name"}

# Interval-valued predicate encoding (no budget conflict detector yet)
{:budget_within, "scope", {:interval, lo, hi}}

# Authority levels
{:authority_at_least, n}
{:authority_required, n}

# Sovereignty
{:jurisdiction_allowed, :eu}
{:jurisdiction_forbidden, :us}

# Latency
{:latency_at_most, ms}

# Logical operators
{:always}
{:and, p1, p2}
{:or, p1, p2}
{:not, p}

Tool invocations

# Direct tool invocation
{:invoke_tool, "tool_name", %{"arg" => value}, "capability_required", :eu}

# Approval gate — must precede high_impact invocations
{:require_approval, "approval_class"}

Conflict types detected

Example

rules = [
  %{
    id: "approve-then-dose",
    agent_id: {"acme", "ph-controller"},
    trigger: {:prop_lt, "ph", {:int, 6}},
    invocations: [
      {:require_approval, "dosing_high_delta"},
      {:invoke_tool, "dose", %{"ml" => 50}, "high_impact", :eu}
    ],
    capability_grants: [{:cap, "ph_dosing", "v1"}],
    authority_required: 2,
    priority: 1
  }
]

{:ok, conflicts} = ExMaude.AI.detect_conflicts(rules, jurisdictions: [:eu, :ch])

When to choose AI rules over IoT rules

Use ExMaude.IoT when modelling Things, Properties, and Actions in a single deployment (one building, one factory, one farm). Use ExMaude.AI when modelling Agents with capability ontologies, tool-invocation argument structure, tenant scoping, sovereignty, authority levels, or approval gates. Both can ship in the same application — the templates and APIs are independent.

Unsupported predicates

:contains and :matches are decidable operations, but this Maude template does not implement them. The validator returns an unsupported-predicate error; evaluate them in the component that defines the intended string/regex semantics.

Links

• ExMaude HexDocs
• Maude System
• Maude Manual
• AutoIoT Paper - IoT conflict detection research