diff --git a/docs/CALL-CONTRACT.md b/docs/CALL-CONTRACT.md
new file mode 100644
index 0000000..2e49449
--- /dev/null
+++ b/docs/CALL-CONTRACT.md
@@ -0,0 +1,170 @@
+# PureSharp `[PureMethod]` Call Contract
+
+**How `[PureMethod]` behaves across call boundaries, and how far v1.0 analyses.**
+
+This document specifies the call contract enforced by `RT0002`. For the purity model
+itself see [`PURITY-SEMANTICS.md`](PURITY-SEMANTICS.md); for the diagnostic contract see
+[`DIAGNOSTICS.md`](DIAGNOSTICS.md).
+
+Every behaviour below was **observed** by running the analyzer and is locked by
+`CallContractTests`.
+
+## Design goal
+
+v1.0 deliberately does **not** attempt unrestricted whole-program analysis. The goal is a
+contract that is **decidable, reproducible, and fast** inside a Roslyn analyzer:
+
+- decidable from the current compilation alone,
+- independent of build order and of which assemblies happen to have source available,
+- linear in the size of the analysed code.
+
+Whole-program purity inference would fail all three.
+
+## The contract
+
+> `[PureMethod]` is a **declared contract on a symbol**, not an inferred property of an
+> implementation.
+
+From a `[PureMethod]` method you may call:
+
+1. a method whose **statically resolved symbol** carries `[PureMethod]`, or
+2. a method on a **known-pure type**.
+
+Everything else is `RT0002`. PureSharp never opens the callee's body to decide whether it
+happens to be pure — an unmarked method is treated as impure, always.
+
+This is a **fail-closed** rule: it can over-report, never under-report, for the calls it
+covers.
+
+## Resolution rules
+
+The contract is checked against the symbol the compiler resolves the call to. This has
+consequences worth stating explicitly, because they are easy to get wrong.
+
+| Call shape | Where `[PureMethod]` must be | Behaviour |
+|---|---|---|
+| Interface method | On the **interface declaration** | Attribute on the implementing class does **not** satisfy a call made through the interface — the call resolves to the interface member |
+| `virtual` method called through the base type | On the **base declaration** | Attribute on the `override` alone does **not** satisfy it |
+| `override` called through the derived type | On the resolved (derived) symbol | Normal resolution applies |
+| Overloads | On the **specific overload** selected | Each overload is judged independently |
+| Extension method | On the extension method itself | Resolves to the static method |
+| Static method | On the method | Normal resolution applies |
+| Recursion, mutual recursion | On **every** participant | One unmarked participant produces `RT0002` at that call site |
+| Generic method | On the generic definition | Type arguments do not affect the decision |
+
+### Consequence: virtual dispatch is not sound
+
+Marking a base `virtual` method `[PureMethod]` permits every call made through the base
+type, but an override may be impure. PureSharp does not verify that overrides honour the
+base contract.
+
+```csharp
+public class Base { [PureMethod] public virtual int M() => 1; }
+public class Derived : Base { public override int M() { Console.WriteLine(); return 2; } }
+```
+
+A call to `Base.M()` from a pure method is accepted, and `Derived.M()` is not checked
+against the base's contract. **Marking a virtual or interface member `[PureMethod]` is an
+assertion the author is responsible for upholding in every override.**
+
+Verifying that overrides preserve the contract is a candidate for a future diagnostic
+(see Open decisions).
+
+## Interprocedural scope
+
+**In scope for v1.0:** exactly one level — the call site, judged against the resolved
+callee's declared attribute.
+
+**Not in scope for v1.0:**
+
+- Reading the callee's body to infer purity
+- Propagating purity transitively through unmarked methods
+- Verifying that overrides honour a base `[PureMethod]` contract
+- Whole-program or cross-compilation analysis
+- Purity of delegate targets (see `PURITY-SEMANTICS.md`)
+
+The analysis performs **no cross-method traversal**. Each call site is decided from the
+resolved symbol's attributes and containing type name alone, which is what keeps the cost
+linear.
+
+### Not covered by the call contract
+
+Two call-like constructs are not analysed as invocations at all:
+
+| Construct | Status |
+|---|---|
+| User-defined property getter | **Not checked.** Property references are inspected only for I/O types, so a getter running arbitrary code is invisible. |
+| Constructor (`new T()`) | **Not checked.** Object creation is not an invocation operation here, so a constructor body doing anything at all is invisible. |
+
+Both are false negatives, locked by `FALSE_NEGATIVE_*` tests in `CallContractTests`.
+
+## External dependencies
+
+**Decision: external assemblies are handled by the same fail-closed rule, with no special
+casing.**
+
+A method from an assembly PureSharp does not control cannot carry `[PureMethod]`, so:
+
+- if its containing type is on the **known-pure list**, the call is allowed;
+- otherwise the call is `RT0002`.
+
+```csharp
+[PureMethod] public object Run() => Math.Abs(-1); // allowed
+[PureMethod] public object Run() => new StringBuilder().ToString(); // RT0002
+```
+
+The alternatives were rejected:
+
+| Alternative | Why rejected |
+|---|---|
+| Read external metadata/IL to infer purity | Not decidable in an analyzer; depends on whether reference assemblies or full IL are available; not reproducible across build environments |
+| Trust external methods by default | Fails open — silently permits arbitrary I/O |
+| Honour a `[Pure]`-style attribute from other libraries | `System.Diagnostics.Contracts.PureAttribute` has weaker, inconsistently applied semantics; adopting it would import an unverified guarantee |
+
+The consequence is accepted: the known-pure list is an **allowlist**, and any pure BCL
+type absent from it over-reports. Growing that list is a non-breaking change (it narrows
+detection), so gaps can be fixed in minor releases.
+
+## Performance
+
+Measured on the analyzer as shipped, on synthetic compilations of `[PureMethod]` methods
+each containing a pure call, an arithmetic call, and a local assignment.
+
+| Methods analysed | Analyzer time | Per method |
+|---|---|---|
+| 100 | 186 ms | 1.86 ms |
+| 500 | 349 ms | 0.70 ms |
+| 2 000 | 844 ms | 0.42 ms |
+
+Observations:
+
+- Cost grows **linearly** with the number of analysed operations. Per-method cost falls as
+ fixed startup cost is amortised; the 100-method figure is dominated by JIT warm-up.
+- Analyzer time is of the same order as the baseline compilation of the same source
+ (roughly 0.8–1.1×), which is the expected range for an operation-walking analyzer.
+- There is no super-linear behaviour, because no call graph is built and no callee body is
+ visited. This is the practical payoff of the one-level contract.
+
+**Method.** Build a `CSharpCompilation` from generated source, wrap it with
+`WithAnalyzers`, and time `GetAnalyzerDiagnosticsAsync()`. `CallContractTests`
+contains a reproducible guard at 2 000 methods; its bound is deliberately generous
+(60 s) so it detects catastrophic regressions without becoming flaky on shared CI.
+
+Absolute numbers are machine-dependent and are recorded for **shape**, not as a
+threshold to enforce.
+
+## Open decisions
+
+Each would be a breaking change under `DIAGNOSTICS.md` (widening detection → major
+release) and needs a product decision.
+
+1. **Override contract verification** — report when an `override` of a `[PureMethod]`
+ member is not itself pure. Would close the virtual-dispatch soundness gap.
+2. **Attribute inheritance** — should an `override` inherit the base's `[PureMethod]`, so
+ marking only the override is unnecessary and calls through the derived type behave
+ consistently?
+3. **Property getters** — treat a user-defined getter as an invocation for contract
+ purposes.
+4. **Constructors** — bring object creation under the call contract.
+5. **Local functions** — let a local function inherit the enclosing method's contract, so
+ its invocation stops producing `RT0002` (see `PURITY-SEMANTICS.md`, gap 7).
diff --git a/docs/DIAGNOSTICS.md b/docs/DIAGNOSTICS.md
index 9c5fabd..6a035f0 100644
--- a/docs/DIAGNOSTICS.md
+++ b/docs/DIAGNOSTICS.md
@@ -20,6 +20,8 @@ with `[PureMethod]`**.
The purity model these diagnostics approximate — and, importantly, the cases v1.0 does
**not** detect — is specified in [`PURITY-SEMANTICS.md`](PURITY-SEMANTICS.md).
+How `RT0002` treats calls across method, interface, and assembly boundaries is specified
+in [`CALL-CONTRACT.md`](CALL-CONTRACT.md).
| Field | Value |
|---|---|
diff --git a/docs/PURITY-SEMANTICS.md b/docs/PURITY-SEMANTICS.md
index c30ed77..d7ef5f3 100644
--- a/docs/PURITY-SEMANTICS.md
+++ b/docs/PURITY-SEMANTICS.md
@@ -150,7 +150,7 @@ analysed in v1.0.
An unmarked method is reported (`RT0002`) without inspecting its body, so PureSharp never
concludes that an unmarked method *is* pure. The reach of the `[PureMethod]` contract
-across call boundaries is specified separately — see Issue #10.
+across call boundaries is specified in [`CALL-CONTRACT.md`](CALL-CONTRACT.md).
### 7. Local functions
diff --git a/src/PureSharp.Analyzers.Tests/CallContractTests.cs b/src/PureSharp.Analyzers.Tests/CallContractTests.cs
new file mode 100644
index 0000000..1b190f1
--- /dev/null
+++ b/src/PureSharp.Analyzers.Tests/CallContractTests.cs
@@ -0,0 +1,240 @@
+using System;
+using System.Collections.Immutable;
+using System.Diagnostics;
+using System.Linq;
+using System.Text;
+using System.Threading.Tasks;
+using Microsoft.CodeAnalysis;
+using Microsoft.CodeAnalysis.CSharp;
+using Microsoft.CodeAnalysis.Diagnostics;
+using Xunit;
+
+namespace PureSharp.Analyzers.Tests;
+
+///
+/// [PureMethod] 呼び出し契約の仕様テスト。
+///
+/// docs/CALL-CONTRACT.md が定義する「契約は静的に解決されたシンボルに対して
+/// 判定される」という原則と、interprocedural analysis の対象範囲を固定する。
+///
+public class CallContractTests
+{
+ private const string Attr = @"
+namespace PureSharp.Core
+{
+ [System.AttributeUsage(System.AttributeTargets.Method, Inherited = false, AllowMultiple = false)]
+ public sealed class PureMethodAttribute : System.Attribute { }
+}
+";
+
+ private static string Source(string body, string members = "", string outer = "") => @"
+using PureSharp.Core;
+using System;
+using System.Collections.Generic;
+using System.Linq;
+" + outer + @"
+public class Probe
+{
+" + members + @"
+ [PureMethod]
+ public object Run()
+ {
+" + body + @"
+ }
+}
+" + Attr;
+
+ private static async Task AssertIdsAsync(string source, params string[] expected)
+ {
+ var diagnostics = await AnalyzerProbe.RunAsync(new ReferentialTransparencyAnalyzer(), source);
+ var actual = diagnostics.Select(d => d.Id).OrderBy(x => x, StringComparer.Ordinal).ToArray();
+ Assert.Equal(expected, actual);
+ }
+
+ // =========================================================
+ // 原則: 契約は「静的に解決されたシンボル」に対して判定される
+ // =========================================================
+
+ [Fact]
+ public async Task Interface_AttributeOnDeclaration_NoDiagnostic()
+ => await AssertIdsAsync(Source(
+ "return t.M();",
+ "private IThing t;",
+ "public interface IThing { [PureMethod] int M(); }"));
+
+ [Fact]
+ public async Task Interface_AttributeOnImplementationOnly_ReportsRT0002()
+ // 呼び出しは interface メンバに解決されるため、実装側の [PureMethod] は
+ // 契約を満たさない。属性は宣言側に付ける必要がある。
+ => await AssertIdsAsync(Source(
+ "return t.M();",
+ "private IThing t;",
+ "public interface IThing { int M(); } public class Impl : IThing { [PureMethod] public int M() => 1; }"),
+ "RT0002");
+
+ [Fact]
+ public async Task Virtual_AttributeOnBase_NoDiagnostic()
+ => await AssertIdsAsync(Source(
+ "return b.M();",
+ "private Base b;",
+ "public class Base { [PureMethod] public virtual int M() => 1; } public class Derived : Base { public override int M() => 2; }"));
+
+ [Fact]
+ public async Task Virtual_AttributeOnOverrideOnly_ReportsRT0002()
+ // base 型経由の呼び出しは base のシンボルに解決されるため、override 側の
+ // [PureMethod] は効かない。
+ => await AssertIdsAsync(Source(
+ "return b.M();",
+ "private Base b;",
+ "public class Base { public virtual int M() => 1; } public class Derived : Base { [PureMethod] public override int M() => 2; }"),
+ "RT0002");
+
+ [Fact]
+ public async Task Virtual_Unmarked_ReportsRT0002()
+ => await AssertIdsAsync(Source(
+ "return b.M();",
+ "private Base b;",
+ "public class Base { public virtual int M() => 1; }"),
+ "RT0002");
+
+ // =========================================================
+ // Overload 解決
+ // =========================================================
+
+ [Fact]
+ public async Task Overload_ResolvedToMarkedOverload_NoDiagnostic()
+ => await AssertIdsAsync(Source(
+ "return H(1);",
+ "[PureMethod] private int H(int x) => x; private int H(string s) => 0;"));
+
+ [Fact]
+ public async Task Overload_ResolvedToUnmarkedOverload_ReportsRT0002()
+ => await AssertIdsAsync(Source(
+ "return H(\"a\");",
+ "[PureMethod] private int H(int x) => x; private int H(string s) => 0;"),
+ "RT0002");
+
+ // =========================================================
+ // Extension method
+ // =========================================================
+
+ [Fact]
+ public async Task ExtensionMethod_Marked_NoDiagnostic()
+ => await AssertIdsAsync(Source(
+ "return this.Ext();",
+ "",
+ "public static class Ex { [PureMethod] public static int Ext(this Probe p) => 1; }"));
+
+ [Fact]
+ public async Task ExtensionMethod_Unmarked_ReportsRT0002()
+ => await AssertIdsAsync(Source(
+ "return this.Ext();",
+ "",
+ "public static class Ex { public static int Ext(this Probe p) => 1; }"),
+ "RT0002");
+
+ // =========================================================
+ // 再帰 / 相互再帰
+ // =========================================================
+
+ [Fact]
+ public async Task MutualRecursion_BothMarked_NoDiagnostic()
+ => await AssertIdsAsync(Source(
+ "return A(1);",
+ "[PureMethod] private int A(int n) => n <= 0 ? 0 : B(n - 1); " +
+ "[PureMethod] private int B(int n) => n <= 0 ? 0 : A(n - 1);"));
+
+ [Fact]
+ public async Task MutualRecursion_OneUnmarked_ReportsRT0002()
+ => await AssertIdsAsync(Source(
+ "return A(1);",
+ "[PureMethod] private int A(int n) => n <= 0 ? 0 : B(n - 1); " +
+ "private int B(int n) => n <= 0 ? 0 : A(n - 1);"),
+ "RT0002");
+
+ [Fact]
+ public async Task StaticMarkedMethod_NoDiagnostic()
+ => await AssertIdsAsync(Source("return S();", "[PureMethod] private static int S() => 1;"));
+
+ // =========================================================
+ // External dependency
+ // =========================================================
+
+ [Fact]
+ public async Task ExternalAssembly_UnmarkedType_ReportsRT0002()
+ // 外部アセンブリの型は [PureMethod] を付けられないため、既知純粋型
+ // リストに含まれない限り常に RT0002 になる (fail-closed)。
+ => await AssertIdsAsync(
+ Source("return new System.Text.StringBuilder().ToString();"),
+ "RT0002");
+
+ [Fact]
+ public async Task ExternalAssembly_KnownPureType_NoDiagnostic()
+ => await AssertIdsAsync(Source("return Math.Abs(-1);"));
+
+ // =========================================================
+ // 対象範囲外 (FALSE NEGATIVE)
+ // =========================================================
+
+ [Fact]
+ public async Task FALSE_NEGATIVE_UserPropertyGetter_NotDetected()
+ // プロパティ参照は I/O 型かどうかしか見ていないため、任意のコードを
+ // 実行しうるユーザー定義 getter は呼び出し契約の対象外。
+ => await AssertIdsAsync(Source("return Q;", "private int Q => 1;"));
+
+ [Fact]
+ public async Task FALSE_NEGATIVE_Constructor_NotDetected()
+ // オブジェクト生成は invocation として解析されないため、コンストラクタ本体は
+ // 呼び出し契約の対象外。
+ => await AssertIdsAsync(Source(
+ "return new Other();", "", "public class Other { public Other() { } }"));
+
+ // =========================================================
+ // Performance guard
+ // =========================================================
+
+ [Fact]
+ public async Task Analyzer_ScalesLinearly_AndCompletesWithinGenerousBound()
+ {
+ // docs/CALL-CONTRACT.md の測定を再現可能にするための guard。
+ // 厳密な閾値は環境差でフレークになるため、破滅的な性能退行のみを検出する
+ // 十分に緩い上限を用いる。
+ var source = GenerateMethods(2000);
+
+ var references = AppDomain.CurrentDomain.GetAssemblies()
+ .Where(a => !a.IsDynamic && !string.IsNullOrEmpty(a.Location))
+ .Select(a => (MetadataReference)MetadataReference.CreateFromFile(a.Location))
+ .ToImmutableArray();
+
+ var compilation = CSharpCompilation.Create(
+ "PerfGuard",
+ new[] { CSharpSyntaxTree.ParseText(source) },
+ references,
+ new CSharpCompilationOptions(OutputKind.DynamicallyLinkedLibrary));
+
+ var withAnalyzers = compilation.WithAnalyzers(
+ ImmutableArray.Create(new ReferentialTransparencyAnalyzer()));
+
+ var stopwatch = Stopwatch.StartNew();
+ var diagnostics = await withAnalyzers.GetAnalyzerDiagnosticsAsync();
+ stopwatch.Stop();
+
+ Assert.Empty(diagnostics);
+ Assert.True(stopwatch.Elapsed < TimeSpan.FromSeconds(60),
+ $"Analyzing 2000 pure methods took {stopwatch.Elapsed}, which indicates a severe regression.");
+ }
+
+ private static string GenerateMethods(int count)
+ {
+ var sb = new StringBuilder();
+ sb.AppendLine("using PureSharp.Core;");
+ sb.AppendLine("using System;");
+ sb.AppendLine("public class Big {");
+ sb.AppendLine(" [PureMethod] private int Helper(int x) => x + 1;");
+ for (var i = 0; i < count; i++)
+ sb.AppendLine($" [PureMethod] public int M{i}(int a) {{ var v = Helper(a); v = v + Math.Abs(a); return v + {i}; }}");
+ sb.AppendLine("}");
+ sb.AppendLine(Attr);
+ return sb.ToString();
+ }
+}