# ExMaude AI Rule Conflict Detection

```elixir
Mix.install(
  [
    {:ex_maude, path: Path.join(__DIR__, ".."), env: :dev}
  ],
  config_path: :ex_maude,
  lockfile: :ex_maude,
  config: [
    ex_maude: [start_pool: true, use_pty: false]
  ]
)
```

## Introduction

`ExMaude.AI` is the companion to `ExMaude.IoT` for verifying AI-generated
automation rules over **Agents**, **Capabilities**, and **ToolInvocations**.

Where `ExMaude.IoT` models physical-IoT rules (Things, Properties, Actions),
`ExMaude.AI` adds:

* **Capability ontology** — typed, shape-versioned capability grants
* **Tool invocations** — structured tool calls with argument maps
* **Tenant scoping** — `{tenant_id, agent_name}` identifiers
* **Sovereignty** — jurisdiction-bound invocations
* **Authority levels** — required-vs-granted authority tracking
* **Approval gates** — explicit gates before high-impact actions
* **Budget intervals** — symbolic arithmetic over budget envelopes

Both modules target the same Maude verification core. They can ship in the
same application — the templates and APIs are independent.

## Rule Vocabulary

### Predicates (triggers)

```elixir
# 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"}

# Quantitative (interval-based, sound symbolic reasoning)
{:budget_within, "scope", {:interval, 0, 50_000}}

# Authority levels
{:authority_at_least, 2}
{:authority_required, 5}

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

# Latency budgets
{:latency_at_most, 2_000}

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

### Tool invocations

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

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

## Example 1: Sovereignty Violation

A US-routing search tool runs under a tenant that allows only EU/CH jurisdictions:

```elixir
rules = [
  %{
    id: "us-search",
    agent_id: {"acme", "research-agent"},
    trigger: {:always},
    invocations: [
      {:invoke_tool, "search", %{"q" => "x"}, "internet_access", :us}
    ]
  }
]

ExMaude.AI.detect_conflicts(rules, jurisdictions: [:eu, :ch])
```

Expect a `:sovereignty_violation` conflict — the tool routes through a
jurisdiction outside the tenant's allowed set.

## Example 2: Approval Gate Bypass

A high-impact dosing invocation must be preceded by an approval gate:

```elixir
# Without an approval gate — bypass is detected
without_approval = [
  %{
    id: "auto-dose",
    agent_id: {"acme", "ph-controller"},
    trigger: {:always},
    invocations: [
      {:invoke_tool, "dose", %{"ml" => 100}, "high_impact", :eu}
    ]
  }
]

ExMaude.AI.detect_conflicts(without_approval, jurisdictions: [:eu])
```

```elixir
# Add the gate — bypass clears
with_approval = [
  %{
    id: "approve-then-dose",
    agent_id: {"acme", "ph-controller"},
    trigger: {:always},
    invocations: [
      {:require_approval, "dosing_high_delta"},
      {:invoke_tool, "dose", %{"ml" => 100}, "high_impact", :eu}
    ]
  }
]

ExMaude.AI.detect_conflicts(with_approval, jurisdictions: [:eu])
```

## Example 3: Capability Shadowing

Two rules grant the same capability at equal priority within a tenant — the
verifier flags this as `:capability_shadowing` (ambiguous activation):

```elixir
rules = [
  %{
    id: "grant-search-a",
    agent_id: {"acme", "agent-a"},
    trigger: {:always},
    invocations: [],
    capability_grants: [{:cap, "web_search", "v1"}],
    priority: 1
  },
  %{
    id: "grant-search-b",
    agent_id: {"acme", "agent-b"},
    trigger: {:always},
    invocations: [],
    capability_grants: [{:cap, "web_search", "v1"}],
    priority: 1
  }
]

ExMaude.AI.detect_conflicts(rules)
```

## Example 4: Pack Tool Composition Mismatch

The same capability name with mismatched shape signatures — typically two
different versions of the same tool — is flagged as
`:pack_tool_composition_mismatch`:

```elixir
rules = [
  %{
    id: "grant-search-v1",
    agent_id: {"acme", "agent-a"},
    trigger: {:always},
    invocations: [],
    capability_grants: [{:cap, "web_search", "v1"}],
    priority: 1
  },
  %{
    id: "grant-search-v2",
    agent_id: {"acme", "agent-b"},
    trigger: {:always},
    invocations: [],
    capability_grants: [{:cap, "web_search", "v2"}],
    priority: 1
  }
]

ExMaude.AI.detect_conflicts(rules)
```

## Validation Without Maude

`validate_rule/1` and `validate_rules/1` catch shape errors before any Maude
round trip. Useful for fast feedback in editors or CI:

```elixir
ExMaude.AI.validate_rule(%{
  id: "ok",
  agent_id: {"acme", "ag1"},
  trigger: {:always},
  invocations: []
})
```

```elixir
ExMaude.AI.validate_rule(%{id: "broken"})
```

The validator also surfaces a contract for *unverifiable* predicates that the
equational fragment of Maude cannot decide:

```elixir
# Regex / string-search predicates are explicitly unverifiable
ExMaude.AI.Validator.validate_predicate({:contains, "subject", "needle"})
```

```elixir
ExMaude.AI.Validator.validate_predicate({:matches, "subject", ~r/x/})
```

Route these to a separate string-match safety net (sandbox, regex matcher,
LLM-as-judge) rather than trying to encode them into the Maude template.

## Conflict-Type Cheatsheet

```elixir
ExMaude.AI.ConflictParser
```

| Constructor | Atom | Detection |
|---|---|---|
| `toolCallConflict` | `:tool_call_conflict` | pairwise |
| `capabilityShadowing` | `:capability_shadowing` | pairwise |
| `packToolCompositionMismatch` | `:pack_tool_composition_mismatch` | pairwise |
| `authorityEscalation` | `:authority_escalation` | pairwise |
| `agentLoopCascade` | `:agent_loop_cascade` | pairwise |
| `sovereigntyViolation` | `:sovereignty_violation` | single-rule |
| `approvalGateBypass` | `:approval_gate_bypass` | single-rule |
| `budgetCascade` | `:budget_cascade` | search-based (deferred) |
| `costCeilingInfeasibility` | `:cost_ceiling_infeasibility` | search-based (deferred) |
| `providerRoutingInfeasibility` | `:provider_routing_infeasibility` | search-based (deferred) |

`detect_pair_conflicts/2` runs only the pairwise checks;
`detect_single_rule_conflicts/2` runs only the single-rule checks;
`detect_conflicts/2` runs both.

## Telemetry

`ExMaude.AI.detect_conflicts/2` emits the same telemetry envelope as
`ExMaude.IoT.detect_conflicts/2`, with `metadata.template == :ai_rules` so
handlers can route on template:

```elixir
:telemetry.attach(
  "ai-rules-logger",
  [:ex_maude, :ai, :detect_conflicts, :stop],
  fn _, %{duration: d, conflict_count: n}, %{result: r}, _ ->
    ms = System.convert_time_unit(d, :native, :millisecond)
    IO.puts("ai-rules: #{r}, #{n} conflicts in #{ms}ms")
  end,
  nil
)
```

```elixir
ExMaude.AI.detect_conflicts(
  [
    %{
      id: "demo",
      agent_id: {"acme", "ag1"},
      trigger: {:always},
      invocations: []
    }
  ],
  jurisdictions: [:eu]
)
```

```elixir
:telemetry.detach("ai-rules-logger")
```

## Next Steps

* [Quick Start](quickstart.livemd) - Basic Maude operations
* [Advanced Usage](advanced.livemd) - IoT conflict detection, custom modules, pooling
* [Term Rewriting](rewriting.livemd) - Rewriting and search deep dive