diff --git a/ROADMAP.md b/ROADMAP.md
index 5276234..86d6258 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -430,7 +430,7 @@ publish warnings and no cleanup diagnostic. Both CoreCLR and Native AOT print
| P1-03 | ✅ Complete | Lower AST to HIR and implement the declared safe-core modules, namespaces, visibility, imports, name resolution, and Cargo package entry point. | P1-02 | `dotnet run --project tools/RustSharp.Conformance -c Release --no-restore -- --profile safe-core-name-resolution`
`dotnet run --project tests/RustSharp.Tests/RustSharp.Tests.csproj -c Release --no-restore`
`rsc check tests/workspaces/basic/Cargo.toml --profile safe-core-primitives-v1` | The acceptance manifest and executable harness pass 25/25 and 190/190. HIR preserves const-function qualifiers and deterministic declaration/reference bindings. Grouped/glob/self/anonymous imports, restricted visibility, source documentation, bounded file modules, original-file diagnostics and PDB mappings are integrated. `Cargo.toml` is accepted by `check`, `build`/`compile`, `run` and `publish`; package metadata, deterministic local `path` dependencies, source discovery, cycle/limit checks and explicit registry-dependency diagnostics are implemented. Leading `::`, unevaluated attributes, registry packages, Cargo features/lockfiles and macro expansion remain explicit profile boundaries for later milestones. |
| P1-04 | ✅ Complete | Implement primitive, tuple, array, slice, reference, function, ADT, and never types with inference/coercion rules. | P1-03 | `dotnet run --project tests/RustSharp.Tests/RustSharp.Tests.csproj -c Release --no-restore`
`dotnet run --project tools/RustSharp.Conformance -c Release --no-build --no-restore -- --profile safe-core-types-v1 --oracle rustc-1.98` | The monomorphic check-only contract includes primitive numeric types, aggregates, references, function pointers, nongeneric ADTs, aliases, patterns/match, closures, bounded const evaluation, inference and directional coercions. All 265/265 regressions and 96/96 version 2 differential cases across sixteen required categories pass, with zero failures/skips and no cleanup diagnostic. File/Cargo checking is integrated; executable commands reject with RSC0009 before output. Generic/trait, MIR, ownership and executable-lowering gates remain separate. |
| P1-05 | 🚧 In progress | Implement generic substitution, monomorphization, impl coherence, and the versioned trait-solver subset. | P0-14, P1-04 | `dotnet run --project tests/RustSharp.Tests -c Release --no-build --no-restore` | The first PR adds bounded structural substitution, trait obligations/coherence and deterministic closed-instance planning; see the [generic foundation contract](docs/generic-profile.md). Generic source/HIR integration, body specialization and AOT-reachable emission remain required for the full gate. |
-| P1-06 | ⏳ Planned | Define typed MIR, CFG validation, desugaring, and source mapping. | P1-04 | `dotnet test RustSharp.slnx -c Release --filter Mir` | MIR snapshots are deterministic; invalid edges/types are rejected; diagnostics map back to `.rs` spans. |
+| P1-06 | 🚧 In progress | Define typed MIR, CFG validation, desugaring, and source mapping. | P1-04 | `dotnet run --project tests/RustSharp.Tests -c Release --no-build --no-restore` | The first PR adds immutable typed MIR, bounded CFG/type validation, deterministic snapshots and scalar HIR lowering with source spans; see the [typed MIR contract](docs/typed-mir-profile.md). Aggregate/pattern/closure lowering, ownership integration and backend consumption remain subsequent batches. |
| P1-07 | ⏳ Planned | Implement move paths, borrow checking, non-lexical lifetimes, reborrowing, and escape analysis for the profile. | P0-13, P1-06 | `dotnet run --project tools/RustSharp.Conformance -- --profile safe-core-borrow` | All declared borrow compile-pass/fail cases match rustc outcome and no rejected construct is silently accepted under CLR rules. |
| P1-08 | ⏳ Planned | Implement scope cleanup, deterministic `Drop`, unwind/abort profile behavior, and panic boundaries. | P1-06, P1-07 | `dotnet test RustSharp.slnx -c Release --filter DropAndPanic` | Normal/early-return/branch/panic paths run destructors once in specified order on CoreCLR and AOT. |
| P1-09 | 🚧 In progress | Emit safe-core programs through CLR LIR with Rust# cross-package metadata. | P0-07, P1-05, P1-08 | `rsc build tests/programs/safe-core/Cargo.toml` (future full gate; current primitive commands above) | Primitive multi-function IL/PDB emission is integrated. Generic/ownership lowering, cross-package metadata and separate consumer compilation remain open. |
diff --git a/ROADMAP_zh.md b/ROADMAP_zh.md
index 75dbdae..00c417e 100644
--- a/ROADMAP_zh.md
+++ b/ROADMAP_zh.md
@@ -355,7 +355,7 @@ AOT 探测器。这些工作流修改需要新的 CI 运行。此配置的 Linux
| P1-03 | ✅ 已完成 | 将 AST 降低为 HIR，并实现声明的安全核心模块、命名空间、可见性、导入、名称解析和 Cargo 包入口。 | P1-02 | `dotnet run --project tools/RustSharp.Conformance -c Release --no-restore -- --profile safe-core-name-resolution`
`dotnet run --project tests/RustSharp.Tests/RustSharp.Tests.csproj -c Release --no-restore`
`rsc check tests/workspaces/basic/Cargo.toml --profile safe-core-primitives-v1` | 名称解析清单和可执行测试分别通过 25/25、190/190。HIR 保留 const 函数限定符，并确定性绑定声明和引用。分组/glob/self/匿名导入、受限可见性、源码文档、有界文件模块、原文件诊断和 PDB 映射已接入。`Cargo.toml` 已接入 `check`、`build`/`compile`、`run` 和 `publish`；已实现包元数据、确定性的本地 `path` 依赖、源码发现、循环/限制检查及对注册表依赖的明确诊断。前导 `::`、未求值属性、注册表包、Cargo feature/锁文件和宏展开仍作为后续里程碑的明确配置档边界。 |
| P1-04 | ✅ 已完成 | 实现原始类型、元组、数组、切片、引用、函数、ADT 和 never 类型，以及推断/强制转换规则。 | P1-03 | `dotnet run --project tests/RustSharp.Tests/RustSharp.Tests.csproj -c Release --no-restore`
`dotnet run --project tools/RustSharp.Conformance -c Release --no-build --no-restore -- --profile safe-core-types-v1 --oracle rustc-1.98` | 单态的仅检查类型契约覆盖基础数值类型、聚合、引用、函数指针、非泛型 ADT、别名、模式/match、闭包、有界 const 求值、推断和有方向的强制转换。265/265 项回归及十六个必需类别中的 96/96 项第 2 版差分用例全部通过，失败和跳过均为零，无清理诊断。已接入文件/Cargo 检查；可执行命令在输出前以 RSC0009 拒绝。泛型/trait、MIR、所有权及可执行降低仍属于独立门槛。 |
| P1-05 | 🚧 进行中 | 实现泛型替换、单态化、impl 一致性和版本化 trait 求解器子集。 | P0-14, P1-04 | `dotnet run --project tests/RustSharp.Tests -c Release --no-build --no-restore` | 首个 PR 增加有界结构替换、trait 约束/一致性和确定性的封闭实例规划；见[泛型基础契约](docs/generic-profile.md)。完整门槛仍要求泛型源码/HIR 接入、主体特化以及 AOT 可达的代码生成。 |
-| P1-06 | ⏳ 计划中 | 定义类型化 MIR、CFG 验证、脱糖和源码映射。 | P1-04 | `dotnet test RustSharp.slnx -c Release --filter Mir` | MIR 快照具有确定性；无效边/类型被拒绝；诊断映射回 `.rs` 范围。 |
+| P1-06 | 🚧 进行中 | 定义类型化 MIR、CFG 验证、脱糖和源码映射。 | P1-04 | `dotnet run --project tests/RustSharp.Tests -c Release --no-build --no-restore` | 首个 PR 增加不可变类型化 MIR、有界 CFG/类型验证、确定性快照以及带源码范围的标量 HIR 降低；见[类型化 MIR 契约](docs/typed-mir-profile.md)。聚合/模式/闭包降低、所有权接入和后端消费保留为后续批次。 |
| P1-07 | ⏳ 计划中 | 为该配置档实现移动路径、借用检查、非词法生命周期、再借用和逃逸分析。 | P0-13, P1-06 | `dotnet run --project tools/RustSharp.Conformance -- --profile safe-core-borrow` | 所有已声明的借用编译通过/失败用例都与 rustc 结果匹配，且不会在 CLR 规则下静默接受被拒绝的构造。 |
| P1-08 | ⏳ 计划中 | 实现作用域清理、确定性 `Drop`、展开/中止配置档行为和 panic 边界。 | P1-06, P1-07 | `dotnet test RustSharp.slnx -c Release --filter DropAndPanic` | 正常/提前返回/分支/panic 路径在 CoreCLR 和 AOT 上按指定顺序恰好运行一次析构函数。 |
| P1-09 | 🚧 进行中 | 通过 CLR LIR 发出带有 Rust# 跨包元数据的安全核心程序。 | P0-07, P1-05, P1-08 | `rsc build tests/programs/safe-core/Cargo.toml`（未来完整门槛；当前基础类型命令见上文） | 基础类型多函数 IL/PDB 发射已接入。泛型/所有权降低、跨包元数据和独立消费者编译仍未完成。 |
diff --git a/docs/typed-mir-profile.md b/docs/typed-mir-profile.md
new file mode 100644
index 0000000..a93cb7e
--- /dev/null
+++ b/docs/typed-mir-profile.md
@@ -0,0 +1,116 @@
+# Typed MIR: first P1-06 pull request
+
+Status: 🚧 In progress. The opt-in `safe-core-mir-v1` API establishes the scalar
+HIR-to-MIR boundary. P1-06 remains open for aggregate, reference, closure, match,
+const, move, and drop lowering and for later ownership and backend integration.
+
+This profile consumes successful `SafeCoreTypeAnalysisProgram` evidence from
+P1-04. It does not change the existing primitive executable profile, the CLI,
+or the IL emitter, and it does not make type-only programs executable.
+
+## Supported source subset
+
+Functions have unit, bool, char, integer, or floating-point parameters and return
+values. A function may also return never (`!`). Scalar aliases, modules, and
+resolved imports keep their existing HIR meaning. Calls resolve directly to a
+function item in the same HIR document, including forward and recursive calls.
+Function IDs follow declaration order; the function name is the type checker's
+canonical item identity, including the `#value` namespace discriminator.
+
+Bodies support initialized identifier/wildcard bindings, shadowing, scalar local
+assignment and compound assignment, unary numeric/boolean operators, binary
+arithmetic/bitwise/comparison operators, scalar casts, blocks, return, `if` and
+`else`, `loop`, `while`, unlabeled `break` and `continue`, loop values,
+and short-circuit `&&`/`||`. Every local read is captured before evaluation of
+subsequent operands, so `x + { x = 2; x }` and multi-argument calls preserve source
+evaluation order. Compound assignment evaluates its right operand before reading
+the destination scalar place.
+
+Aggregates, references, function-pointer values/indirect calls, closures,
+`match`, destructuring, `let-else`, const items, and inline const blocks produce
+`RSM2002` at the unsupported construct. Unreachable source tails after an
+unconditional transfer are omitted after P1-04 has checked their types; they are
+not represented as executable MIR or independently checked against this subset.
+No unsupported construct is translated into a dummy value.
+
+Loop/control-flow labels remain outside the upstream P1-04 HIR gate and receive
+`RSN1007` before MIR lowering. Internal loop contexts retain label information,
+but this first source profile makes no labeled-control-flow support claim.
+
+## Representation and invariants
+
+`SafeCoreMirProgram` owns functions. A function owns typed locals and basic
+blocks. Function, local, and block IDs are their stable collection indices.
+Parameters precede other locals; user names and mutability are preserved and
+temporary names are deterministic `tmpN` values. Constants store invariant
+decimal integers, round-trip float text, bool words, decimal Unicode scalars for
+char, or `()` for unit. Signed minimum literals, including grouped operands, are
+represented as one negative constant instead of an out-of-range positive value.
+
+Statements assign an explicit typed rvalue to a local slot. Every block has
+exactly one terminator: return, goto, boolean branch, direct call, or unreachable.
+Calls have explicit result destinations and continuations. A diverging call has
+no result and an unreachable continuation. Branch and loop results are assigned
+on their incoming paths to a shared temporary. Short-circuit operators branch
+before entering the right operand's block. Empty unreachable join blocks have
+an explicit unreachable terminator.
+
+Each element carries `SafeCoreMirSource`: original source path, span, HIR node
+ID, and HIR document extent (`Hir.Root.Span.End`). The extent can exclude trailing
+trivia; it is not claimed to be the original text buffer length. Introduced
+temporaries and control-flow blocks refer to the HIR expression that caused
+their creation.
+
+`SafeCoreMirValidation.Validate` checks IDs, targets, source bounds, operand and
+rvalue types, supported operations, function/call signatures, and return types.
+It checks unreachable blocks too and reports reachable block IDs separately.
+Its structural validation does not prove ownership, definite initialization,
+termination, panic behavior, or executable backend correctness. Those properties
+must not be inferred from a successful result.
+
+## Opt-in API
+
+```csharp
+SafeCoreTypeAnalysisResult types = SafeCoreTypeAnalysis.Check(hir,
+ cancellationToken: cancellationToken);
+if (!types.IsSuccessful)
+ return;
+
+SafeCoreMirLoweringResult lowered = SafeCoreMirLowering.Lower(types.Program!,
+ new SafeCoreMirLoweringOptions { Timeout = TimeSpan.FromSeconds(10) },
+ cancellationToken);
+if (lowered.IsSuccessful)
+{
+ // Every published program includes successful structural validation evidence.
+ string text = SafeCoreMirFormatting.Format(lowered.Program!);
+}
+```
+
+`Lower` returns no partial program when lowering or validation fails. Stable
+lowering diagnostics distinguish incomplete input evidence (`RSM2001`),
+unsupported syntax (`RSM2002`), and exceeded bounds (`RSM2003`). Validation errors
+retain their `RSM000x`/`RSM100x` codes and are also available in `Validation`.
+Caller cancellation throws `OperationCanceledException`; invalid option values
+throw `ArgumentOutOfRangeException`.
+
+The default lowering budget is ten seconds and one million operations, shared
+with final validation. Independent size caps cover functions, per-function
+blocks and locals, and nesting. MIR collection construction, validation, and
+formatting also impose bounded size/time limits and accept cancellation. A
+small configured limit rejects deterministically instead of publishing an
+incomplete graph.
+
+## Verification
+
+`SafeCoreMirLoweringTests` parses real sources through HIR and P1-04 type analysis.
+It checks deterministic typed snapshots, constants and HIR provenance, exact
+unsupported spans, and work/depth/size/time/cancellation failures. A small,
+independent test interpreter runs scalar control-flow graphs with a maximum of
+4,096 total steps, 32 call levels, a five-second deadline, and cancellation. It
+checks evaluation order, shadowing, direct calls, nested loops, branch joins,
+early returns, and short-circuit behavior.
+
+`SafeCoreMirValidationTests` exercises constructed malformed MIR independently
+of source lowering. Both test classes run with the repository test harness.
+This first pull request provides no runtime or rustc differential conformance
+claim for the new MIR representation.
diff --git a/src/RustSharp.Semantics/SafeCoreMirFormatting.cs b/src/RustSharp.Semantics/SafeCoreMirFormatting.cs
new file mode 100644
index 0000000..dce6338
--- /dev/null
+++ b/src/RustSharp.Semantics/SafeCoreMirFormatting.cs
@@ -0,0 +1,155 @@
+using System.Diagnostics;
+using System.Globalization;
+using System.Text;
+
+namespace RustSharp.Semantics;
+
+public sealed record SafeCoreMirFormattingOptions
+{
+ public TimeSpan Timeout { get; init; } = TimeSpan.FromSeconds(10);
+ public CancellationToken CancellationToken { get; init; }
+ public int MaximumOperations { get; init; } = 1_000_000;
+ public int MaximumCharacters { get; init; } = 4_000_000;
+}
+
+/// Versioned deterministic text with explicit IDs, types and original source evidence.
+/// Inputs must first pass ; formatting does not
+/// repeat structural validation or certify validity of manually constructed programs.
+public static class SafeCoreMirFormatting
+{
+ public static string Format(SafeCoreMirProgram program, SafeCoreMirFormattingOptions? options = null)
+ {
+ ArgumentNullException.ThrowIfNull(program);
+ options ??= new();
+ ArgumentOutOfRangeException.ThrowIfLessThanOrEqual(options.Timeout, TimeSpan.Zero);
+ ArgumentOutOfRangeException.ThrowIfNegativeOrZero(options.MaximumOperations);
+ ArgumentOutOfRangeException.ThrowIfNegativeOrZero(options.MaximumCharacters);
+ return new Formatter(options).Format(program);
+ }
+
+ private sealed class Formatter(SafeCoreMirFormattingOptions options)
+ {
+ private readonly StringBuilder _text = new();
+ private readonly Stopwatch _clock = Stopwatch.StartNew();
+ private int _operations;
+
+ public string Format(SafeCoreMirProgram program)
+ {
+ Add("safe-core-mir-v1\n");
+ for (int index = 0; index < program.Functions.Count; index++)
+ {
+ Step();
+ SafeCoreMirFunction function = program.Functions[index];
+ Add(FormattableString.Invariant($"fn @{function.Id} {Escape(function.Name)} -> {function.ReturnType} entry bb{function.EntryBlockId} "));
+ Source(function.Source);
+ Add(" {\n");
+ for (int localIndex = 0; localIndex < function.Locals.Count; localIndex++)
+ {
+ Step();
+ SafeCoreMirLocal local = function.Locals[localIndex];
+ Add(FormattableString.Invariant($" let %{local.Id} {local.Kind.ToString().ToLowerInvariant()}{(local.IsMutable ? " mut" : "")} {Escape(local.Name)}: {local.Type} "));
+ Source(local.Source);
+ Add("\n");
+ }
+ for (int blockIndex = 0; blockIndex < function.Blocks.Count; blockIndex++)
+ {
+ Step();
+ SafeCoreMirBlock block = function.Blocks[blockIndex];
+ Add(FormattableString.Invariant($" bb{block.Id} "));
+ Source(block.Source);
+ Add(":\n");
+ for (int statementIndex = 0; statementIndex < block.Statements.Count; statementIndex++)
+ {
+ Step();
+ SafeCoreMirStatement statement = block.Statements[statementIndex];
+ SafeCoreMirRvalue value = statement.Value;
+ Add(FormattableString.Invariant($" %{statement.DestinationLocalId} = {value.Kind.ToString().ToLowerInvariant()}"));
+ if (value.Operator is not null) Add($" {Escape(value.Operator)}");
+ Add("(");
+ Operands(value.Operands);
+ Add($"): {value.Type} ");
+ Source(statement.Source);
+ Add("\n");
+ }
+ Terminator(block.Terminator);
+ }
+ Add("}\n");
+ }
+ return _text.ToString();
+ }
+
+ private void Terminator(SafeCoreMirTerminator terminator)
+ {
+ Step();
+ Add($" {terminator.Kind.ToString().ToLowerInvariant()}");
+ if (terminator.Operand is not null)
+ {
+ Add(" ");
+ Operand(terminator.Operand);
+ }
+ if (terminator.Kind == SafeCoreMirTerminatorKind.Call)
+ {
+ Add("(");
+ Operands(terminator.Arguments);
+ Add(")");
+ if (terminator.DestinationLocalId is int destination) Add(FormattableString.Invariant($" -> %{destination}"));
+ }
+ if (terminator.TargetBlockId >= 0) Add(FormattableString.Invariant($" bb{terminator.TargetBlockId}"));
+ if (terminator.FalseTargetBlockId >= 0) Add(FormattableString.Invariant($" else bb{terminator.FalseTargetBlockId}"));
+ Add(" ");
+ Source(terminator.Source);
+ Add("\n");
+ }
+
+ private void Operands(IReadOnlyList operands)
+ {
+ for (int index = 0; index < operands.Count; index++)
+ {
+ Step();
+ if (index != 0) Add(", ");
+ Operand(operands[index]);
+ }
+ }
+
+ private void Operand(SafeCoreMirOperand operand)
+ {
+ Step();
+ Add(operand.Kind switch
+ {
+ SafeCoreMirOperandKind.Local => "%" + operand.Id.ToString(CultureInfo.InvariantCulture),
+ SafeCoreMirOperandKind.Function => "@" + operand.Id.ToString(CultureInfo.InvariantCulture),
+ _ => "const " + Escape(operand.Value ?? ""),
+ });
+ Add($":{operand.Type}");
+ }
+
+ private void Source(SafeCoreMirSource source) => Add(FormattableString.Invariant(
+ $"[{Escape(source.SourcePath)}:{source.Span.Start}+{source.Span.Length}/{source.SourceLength} hir#{source.HirNodeId}]"));
+
+ private string Escape(string value)
+ {
+ Step();
+ if (value.Length > 262_144) throw new SafeCoreMirLimitException("MIR formatting input text limit reached.");
+ return value.Replace("\\", "\\\\", StringComparison.Ordinal).Replace("\r", "\\r", StringComparison.Ordinal)
+ .Replace("\n", "\\n", StringComparison.Ordinal).Replace("\t", "\\t", StringComparison.Ordinal)
+ .Replace("[", "\\[", StringComparison.Ordinal).Replace("]", "\\]", StringComparison.Ordinal);
+ }
+
+ private void Add(string value)
+ {
+ Step();
+ if ((long)_text.Length + value.Length > Math.Clamp(options.MaximumCharacters, 1, 4_000_000))
+ throw new SafeCoreMirLimitException("MIR formatting character limit reached.");
+ _text.Append(value);
+ }
+
+ private void Step()
+ {
+ options.CancellationToken.ThrowIfCancellationRequested();
+ if (++_operations > Math.Clamp(options.MaximumOperations, 1, 1_000_000)
+ || _clock.Elapsed >= (options.Timeout > TimeSpan.Zero && options.Timeout <= TimeSpan.FromMinutes(1)
+ ? options.Timeout : TimeSpan.FromSeconds(10)))
+ throw new SafeCoreMirLimitException("MIR formatting work or time limit reached.");
+ }
+ }
+}
diff --git a/src/RustSharp.Semantics/SafeCoreMirLowering.cs b/src/RustSharp.Semantics/SafeCoreMirLowering.cs
new file mode 100644
index 0000000..ab80a28
--- /dev/null
+++ b/src/RustSharp.Semantics/SafeCoreMirLowering.cs
@@ -0,0 +1,618 @@
+using System.Diagnostics;
+using System.Diagnostics.CodeAnalysis;
+using System.Globalization;
+using System.Numerics;
+using System.Text;
+using RustSharp.Syntax;
+using K = RustSharp.Semantics.SafeCoreSemanticTypeKind;
+using N = RustSharp.Semantics.SafeCoreHirNodeKind;
+
+namespace RustSharp.Semantics;
+
+/// Independent bounds for the opt-in scalar MIR lowering pass.
+public sealed record SafeCoreMirLoweringOptions
+{
+ public TimeSpan Timeout { get; init; } = TimeSpan.FromSeconds(10);
+ public int MaximumOperations { get; init; } = 1_000_000;
+ public int MaximumNestingDepth { get; init; } = 128;
+ public int MaximumFunctions { get; init; } = 1_024;
+ public int MaximumBlocksPerFunction { get; init; } = 16_384;
+ public int MaximumLocalsPerFunction { get; init; } = 65_536;
+}
+
+/// No partial program is published when lowering or validation fails.
+public sealed record SafeCoreMirLoweringResult(
+ SafeCoreMirProgram? Program,
+ IReadOnlyList Diagnostics,
+ SafeCoreMirValidationResult? Validation,
+ bool IsTruncated)
+{
+ public bool IsSuccessful => Program is not null && Diagnostics.Count == 0 &&
+ !IsTruncated && Validation is { IsSuccessful: true };
+}
+
+///
+/// Lowers resolved P1-04 evidence to the experimental scalar MIR profile.
+/// This API does not change the existing compiler driver or IL emission path.
+///
+public static class SafeCoreMirLowering
+{
+ public const string Profile = "safe-core-mir-v1";
+ public const string InvalidEvidence = "RSM2001";
+ public const string UnsupportedSyntax = "RSM2002";
+ public const string LimitReached = "RSM2003";
+
+ public static SafeCoreMirLoweringResult Lower(SafeCoreTypeAnalysisProgram program,
+ SafeCoreMirLoweringOptions? options = null, CancellationToken cancellationToken = default)
+ {
+ ArgumentNullException.ThrowIfNull(program);
+ ArgumentNullException.ThrowIfNull(program.Hir);
+ ArgumentNullException.ThrowIfNull(program.Types);
+ ArgumentNullException.ThrowIfNull(program.Coercions);
+ cancellationToken.ThrowIfCancellationRequested();
+ options ??= new();
+ if (options.Timeout <= TimeSpan.Zero || options.Timeout > TimeSpan.FromMinutes(1) ||
+ options.MaximumOperations is < 1 or > 4_000_000 ||
+ options.MaximumNestingDepth is < 1 or > 128 ||
+ options.MaximumFunctions is < 1 or > 4_096 ||
+ options.MaximumBlocksPerFunction is < 1 or > 65_536 ||
+ options.MaximumLocalsPerFunction is < 1 or > 262_144)
+ throw new ArgumentOutOfRangeException(nameof(options));
+ if (!program.Hir.IsSuccessful)
+ return new(null, [new Diagnostic(InvalidEvidence, "MIR requires successful, resolved HIR type evidence.",
+ program.Hir.Root?.Span ?? new TextSpan(0, 0)) { SourcePath = program.Hir.SourcePath }], null, false);
+ try
+ {
+ var lowerer = new Lowerer(program, options, cancellationToken);
+ SafeCoreMirProgram mir = lowerer.Run();
+ SafeCoreMirValidationResult validation = SafeCoreMirValidation.Validate(mir,
+ new() { CancellationToken = cancellationToken, Timeout = lowerer.Remaining,
+ MaximumOperations = lowerer.RemainingOperations });
+ return validation.IsSuccessful
+ ? new(mir, [], validation, false)
+ : new(null, validation.Diagnostics.Select(d => new Diagnostic(d.Code, d.Message,
+ d.Source?.Span ?? program.Hir.Root!.Span) { SourcePath = d.Source?.SourcePath ?? program.Hir.SourcePath }).ToArray(),
+ validation, validation.IsTruncated);
+ }
+ catch (LoweringException exception)
+ {
+ return new(null, [exception.Diagnostic with { SourcePath = program.Hir.SourcePath }], null,
+ exception.Diagnostic.Code == LimitReached);
+ }
+ catch (SafeCoreMirLimitException)
+ {
+ return new(null, [new Diagnostic(LimitReached, "MIR construction exceeded its bounded collection limits.",
+ program.Hir.Root!.Span) { SourcePath = program.Hir.SourcePath }], null, true);
+ }
+ }
+
+ private sealed class LoweringException(Diagnostic diagnostic) : Exception(diagnostic.Message)
+ {
+ public Diagnostic Diagnostic { get; } = diagnostic;
+ }
+
+ private sealed class Lowerer(SafeCoreTypeAnalysisProgram input, SafeCoreMirLoweringOptions options,
+ CancellationToken cancellation)
+ {
+ private readonly Stopwatch _clock = Stopwatch.StartNew();
+ private readonly List _functionNodes = [];
+ private readonly Dictionary _functions = new(StringComparer.Ordinal);
+ private readonly List _locals = [];
+ private readonly Dictionary _bindings = [];
+ private readonly List _blocks = [];
+ private readonly List _loops = [];
+ private BlockBuilder? _current;
+ private int _operations;
+
+ private sealed class BlockBuilder(int id, SafeCoreMirSource source)
+ {
+ public int Id { get; } = id;
+ public SafeCoreMirSource Source { get; } = source;
+ public List Statements { get; } = [];
+ public SafeCoreMirTerminator? Terminator { get; set; }
+ }
+
+ private sealed class LoopContext(string? label, int header, int exit, int? result)
+ {
+ public string? Label { get; } = label;
+ public int Header { get; } = header;
+ public int Exit { get; } = exit;
+ public int? Result { get; } = result;
+ public bool HasBreak { get; set; }
+ }
+
+ public TimeSpan Remaining
+ {
+ get
+ {
+ Step(input.Hir.Root!, 0);
+ TimeSpan remaining = options.Timeout - _clock.Elapsed;
+ if (remaining <= TimeSpan.Zero) Limit(input.Hir.Root!);
+ return remaining;
+ }
+ }
+
+ public int RemainingOperations
+ {
+ get
+ {
+ if (_operations >= options.MaximumOperations) Limit(input.Hir.Root!);
+ return options.MaximumOperations - _operations;
+ }
+ }
+
+ public SafeCoreMirProgram Run()
+ {
+ Collect(input.Hir.Root!, 0);
+ var functions = new List(_functionNodes.Count);
+ for (int index = 0; index < _functionNodes.Count; index++)
+ {
+ Step(_functionNodes[index], 0);
+ functions.Add(Function(_functionNodes[index], index));
+ }
+ return new(functions, cancellation);
+ }
+
+ private void Collect(SafeCoreHirNode node, int depth)
+ {
+ Step(node, depth);
+ if (node.Kind is N.CompilationUnit or N.Module)
+ {
+ for (int index = 0; index < node.ChildIds.Count; index++) Collect(Child(node, index), depth + 1);
+ return;
+ }
+ if (node.Kind is N.Attribute or N.Import or N.ImportGroup or N.TypeAlias) return;
+ if (node.Kind != N.Function) Unsupported(node);
+ if (_functionNodes.Count >= options.MaximumFunctions) Limit(node);
+ SafeCoreType signature = Type(node);
+ if (signature.Kind != K.Function || node.DeclaredSymbol is null) Invalid(node);
+ Scalar(signature.ReturnType, node, allowNever: true);
+ for (int index = 0; index < signature.ParameterTypes.Count; index++)
+ {
+ Step(node, depth);
+ Scalar(signature.ParameterTypes[index], node);
+ }
+ if (!_functions.TryAdd(SymbolKey(node.DeclaredSymbol!), _functionNodes.Count)) Invalid(node);
+ _functionNodes.Add(node);
+ }
+
+ private SafeCoreMirFunction Function(SafeCoreHirNode node, int id)
+ {
+ _locals.Clear(); _bindings.Clear(); _blocks.Clear(); _loops.Clear();
+ SafeCoreType signature = Type(node);
+ int parameterIndex = 0;
+ for (int index = 0; index < node.ChildIds.Count; index++)
+ {
+ SafeCoreHirNode child = Child(node, index);
+ Step(child, 0);
+ if (child.Kind != N.Parameter) continue;
+ SafeCoreHirNode pattern = UnwrapPattern(Child(child, 0));
+ if (pattern.Kind is not (N.IdentifierPattern or N.WildcardPattern) ||
+ pattern.Modifiers.HasFlag(SafeCoreHirNodeModifiers.ByReference)) Unsupported(pattern);
+ int local = Local(pattern.Name ?? $"arg{parameterIndex.ToString(CultureInfo.InvariantCulture)}",
+ signature.ParameterTypes[parameterIndex++], SafeCoreMirLocalKind.Parameter,
+ pattern.Modifiers.HasFlag(SafeCoreHirNodeModifiers.Mutable), pattern);
+ if (pattern.DeclaredSymbol is not null) _bindings.Add(pattern.DeclaredSymbol, local);
+ }
+ if (parameterIndex != signature.ParameterTypes.Count) Invalid(node);
+ _current = Block(node);
+ SafeCoreMirOperand? body = Expr(Child(node, node.ChildIds.Count - 1), 0);
+ if (_current is not null)
+ End(SafeCoreMirTerminator.Return(signature.ReturnType.Kind == K.Unit ? null : body, Source(node)));
+ var blocks = new List(_blocks.Count);
+ for (int index = 0; index < _blocks.Count; index++)
+ {
+ Step(node, 0);
+ BlockBuilder block = _blocks[index];
+ blocks.Add(new(block.Id, block.Statements,
+ block.Terminator ?? SafeCoreMirTerminator.Unreachable(block.Source), block.Source, cancellation));
+ }
+ return new(id, signature.Name!, signature.ReturnType, _locals.ToArray(), blocks, 0, Source(node), cancellation);
+ }
+
+ private SafeCoreMirOperand? Expr(SafeCoreHirNode node, int depth)
+ {
+ Step(node, depth);
+ if (_current is null) return null;
+ SafeCoreMirOperand? value = ExprCore(node, depth);
+ if (value is not null && _current is not null && input.Coercions.TryGetValue(node.Id, out SafeCoreType? target) &&
+ !value.Type.Equals(target))
+ {
+ Scalar(target, node);
+ value = Emit(SafeCoreMirRvalue.Coerce(value, target, Source(node)), target, node);
+ }
+ return value;
+ }
+
+ private SafeCoreMirOperand? ExprCore(SafeCoreHirNode node, int depth)
+ {
+ switch (node.Kind)
+ {
+ case N.Attribute: return Unit(node);
+ case N.Block:
+ SafeCoreMirOperand? result = Unit(node);
+ for (int index = 0; index < node.ChildIds.Count && _current is not null; index++)
+ result = Expr(Child(node, index), depth + 1);
+ return result;
+ case N.BlockExpression: return Expr(Child(node, 0), depth + 1);
+ case N.TupleExpression when node.ChildIds.Count == 0: return Unit(node);
+ case N.TupleExpression when node.ChildIds.Count == 1 &&
+ !node.Modifiers.HasFlag(SafeCoreHirNodeModifiers.HasTrailingComma):
+ return Expr(Child(node, 0), depth + 1);
+ case N.ExpressionStatement:
+ _ = Expr(Child(node, 0), depth + 1);
+ return _current is null ? null : Unit(node);
+ case N.LetStatement: return Let(node, depth);
+ case N.LiteralExpression: return Literal(node, Type(node));
+ case N.NameExpression:
+ int binding = -1;
+ if (node.ReferencedSymbol is null || !_bindings.TryGetValue(node.ReferencedSymbol, out binding)) Unsupported(node);
+ SafeCoreMirLocal local = _locals[binding];
+ // Snapshot the read before a later operand can mutate the user local.
+ return Emit(SafeCoreMirRvalue.Use(SafeCoreMirOperand.Local(binding, local.Type, Source(node)), Source(node)), local.Type, node);
+ case N.UnaryExpression:
+ if (node.Value is not ("!" or "-")) Unsupported(node);
+ SafeCoreHirNode inner = UnwrapExpression(Child(node, 0), depth + 1);
+ if (node.Value == "-" && inner.Kind == N.LiteralExpression && Type(node).IsInteger)
+ return Literal(inner, Type(node), negate: true, origin: node);
+ SafeCoreMirOperand? operand = Expr(Child(node, 0), depth + 1);
+ return operand is null ? null : Emit(SafeCoreMirRvalue.Unary(node.Value!, operand, Type(node), Source(node)), Type(node), node);
+ case N.BinaryExpression: return Binary(node, depth);
+ case N.CastExpression:
+ SafeCoreMirOperand? cast = Expr(Child(node, 0), depth + 1);
+ Scalar(Type(node), node);
+ return cast is null ? null : Emit(SafeCoreMirRvalue.Cast(cast, Type(node), Source(node)), Type(node), node);
+ case N.CallExpression: return Call(node, depth);
+ case N.IfExpression: return If(node, depth);
+ case N.LoopExpression:
+ case N.WhileExpression: return Loop(node, depth);
+ case N.BreakExpression:
+ case N.ContinueExpression: return LoopControl(node, depth);
+ case N.ReturnExpression:
+ case N.ReturnStatement:
+ SafeCoreMirOperand? returned = node.ChildIds.Count == 0 ? null : Expr(Child(node, 0), depth + 1);
+ if (_current is not null) End(SafeCoreMirTerminator.Return(returned?.Type.Kind == K.Unit ? null : returned, Source(node)));
+ return null;
+ default: Unsupported(node); return null;
+ }
+ }
+
+ private SafeCoreMirOperand? Let(SafeCoreHirNode node, int depth)
+ {
+ if (node.Modifiers.HasFlag(SafeCoreHirNodeModifiers.HasElse)) Unsupported(node);
+ SafeCoreHirNode pattern = UnwrapPattern(Child(node, 0));
+ if (pattern.Kind is not (N.IdentifierPattern or N.WildcardPattern) ||
+ pattern.Modifiers.HasFlag(SafeCoreHirNodeModifiers.ByReference)) Unsupported(pattern);
+ SafeCoreMirOperand? value = Expr(Child(node, node.ChildIds.Count - 1), depth + 1);
+ if (_current is null || value is null) return null;
+ if (pattern.Kind == N.WildcardPattern) return Unit(node);
+ if (pattern.DeclaredSymbol is null) Invalid(pattern);
+ int local = Local(pattern.Name!, Type(pattern), SafeCoreMirLocalKind.User,
+ pattern.Modifiers.HasFlag(SafeCoreHirNodeModifiers.Mutable), pattern);
+ _bindings.Add(pattern.DeclaredSymbol!, local);
+ Assign(local, value, node);
+ return Unit(node);
+ }
+
+ private SafeCoreMirOperand? Binary(SafeCoreHirNode node, int depth)
+ {
+ string op = node.Value!;
+ if (op is "&&" or "||") return ShortCircuit(node, depth);
+ if (op is "=" or "+=" or "-=" or "*=" or "/=" or "%=" or "&=" or "|=" or "^=" or "<<=" or ">>=")
+ {
+ SafeCoreHirNode place = UnwrapExpression(Child(node, 0), depth + 1);
+ int destination = -1;
+ if (place.Kind != N.NameExpression || place.ReferencedSymbol is null ||
+ !_bindings.TryGetValue(place.ReferencedSymbol, out destination)) Unsupported(place);
+ SafeCoreMirOperand? right = Expr(Child(node, 1), depth + 1);
+ if (right is null || _current is null) return null;
+ if (op != "=")
+ right = Emit(SafeCoreMirRvalue.Binary(op[..^1],
+ SafeCoreMirOperand.Local(destination, _locals[destination].Type, Source(place)),
+ right, _locals[destination].Type, Source(node)), _locals[destination].Type, node);
+ Assign(destination, right, node);
+ return Unit(node);
+ }
+ SafeCoreMirOperand? leftValue = Expr(Child(node, 0), depth + 1);
+ SafeCoreMirOperand? rightValue = Expr(Child(node, 1), depth + 1);
+ if (leftValue is null || rightValue is null || _current is null) return null;
+ return Emit(SafeCoreMirRvalue.Binary(op, leftValue, rightValue, Type(node), Source(node)), Type(node), node);
+ }
+
+ private SafeCoreMirOperand? Call(SafeCoreHirNode node, int depth)
+ {
+ SafeCoreHirNode calleeNode = UnwrapExpression(Child(node, 0), depth + 1);
+ int function = -1;
+ if (calleeNode.Kind != N.NameExpression || calleeNode.ReferencedSymbol is null ||
+ !_functions.TryGetValue(SymbolKey(calleeNode.ReferencedSymbol), out function)) Unsupported(calleeNode);
+ SafeCoreType signature = Type(_functionNodes[function]);
+ var arguments = new List();
+ for (int index = 1; index < node.ChildIds.Count && _current is not null; index++)
+ {
+ SafeCoreMirOperand? argument = Expr(Child(node, index), depth + 1);
+ if (argument is not null) arguments.Add(argument);
+ }
+ if (_current is null) return null;
+ int? destination = signature.ReturnType.Kind is K.Unit or K.Never ? null : Temp(signature.ReturnType, node);
+ BlockBuilder continuation = Block(node);
+ End(SafeCoreMirTerminator.Call(SafeCoreMirOperand.Function(function, signature, Source(calleeNode)),
+ arguments, destination, continuation.Id, Source(node), cancellation));
+ _current = continuation;
+ if (signature.ReturnType.Kind == K.Never)
+ {
+ End(SafeCoreMirTerminator.Unreachable(Source(node)));
+ return null;
+ }
+ return destination is int local ? SafeCoreMirOperand.Local(local, signature.ReturnType, Source(node)) : Unit(node);
+ }
+
+ private SafeCoreMirOperand? If(SafeCoreHirNode node, int depth)
+ {
+ SafeCoreMirOperand? condition = Expr(Child(node, 0), depth + 1);
+ if (condition is null || _current is null) return null;
+ SafeCoreType type = EffectiveType(node);
+ int? destination = type.Kind is K.Unit or K.Never ? null : Temp(type, node);
+ BlockBuilder thenBlock = Block(Child(node, 1));
+ BlockBuilder elseBlock = Block(node.ChildIds.Count == 3 ? Child(node, 2) : node);
+ BlockBuilder join = Block(node);
+ End(SafeCoreMirTerminator.Branch(condition, thenBlock.Id, elseBlock.Id, Source(node)));
+ _current = thenBlock;
+ SafeCoreMirOperand? then = Expr(Child(node, 1), depth + 1);
+ bool thenReturns = Join(destination, then, join, node);
+ _current = elseBlock;
+ SafeCoreMirOperand? other = node.ChildIds.Count == 3 ? Expr(Child(node, 2), depth + 1) : Unit(node);
+ bool elseReturns = Join(destination, other, join, node);
+ _current = thenReturns || elseReturns ? join : null;
+ return _current is null ? null : destination is int local ? SafeCoreMirOperand.Local(local, type, Source(node)) : Unit(node);
+ }
+
+ private SafeCoreMirOperand? ShortCircuit(SafeCoreHirNode node, int depth)
+ {
+ SafeCoreMirOperand? left = Expr(Child(node, 0), depth + 1);
+ if (left is null || _current is null) return null;
+ int result = Temp(SafeCoreType.Primitive(K.Bool), node);
+ BlockBuilder rhs = Block(Child(node, 1)), shortcut = Block(node), join = Block(node);
+ bool and = node.Value == "&&";
+ End(SafeCoreMirTerminator.Branch(left, and ? rhs.Id : shortcut.Id, and ? shortcut.Id : rhs.Id, Source(node)));
+ _current = shortcut;
+ Assign(result, SafeCoreMirOperand.Constant(SafeCoreType.Primitive(K.Bool), and ? "false" : "true", Source(node)), node);
+ End(SafeCoreMirTerminator.Goto(join.Id, Source(node)));
+ _current = rhs;
+ _ = Join(result, Expr(Child(node, 1), depth + 1), join, node);
+ _current = join;
+ return SafeCoreMirOperand.Local(result, SafeCoreType.Primitive(K.Bool), Source(node));
+ }
+
+ private SafeCoreMirOperand? Loop(SafeCoreHirNode node, int depth)
+ {
+ bool isWhile = node.Kind == N.WhileExpression;
+ SafeCoreType type = EffectiveType(node);
+ int? result = type.Kind is K.Unit or K.Never ? null : Temp(type, node);
+ BlockBuilder header = Block(node), body = Block(node), exit = Block(node);
+ End(SafeCoreMirTerminator.Goto(header.Id, Source(node)));
+ var context = new LoopContext(node.Name, header.Id, exit.Id, result);
+ _loops.Add(context);
+ _current = header;
+ if (isWhile)
+ {
+ SafeCoreMirOperand? condition = Expr(Child(node, 0), depth + 1);
+ if (_current is not null && condition is not null)
+ End(SafeCoreMirTerminator.Branch(condition, body.Id, exit.Id, Source(node)));
+ else
+ {
+ _loops.RemoveAt(_loops.Count - 1);
+ _current = context.HasBreak ? exit : null;
+ return _current is null ? null : Unit(node);
+ }
+ }
+ else End(SafeCoreMirTerminator.Goto(body.Id, Source(node)));
+ _current = body;
+ _ = Expr(Child(node, isWhile ? 1 : 0), depth + 1);
+ if (_current is not null) End(SafeCoreMirTerminator.Goto(header.Id, Source(node)));
+ _loops.RemoveAt(_loops.Count - 1);
+ _current = isWhile || context.HasBreak ? exit : null;
+ return _current is null ? null : result is int local ? SafeCoreMirOperand.Local(local, type, Source(node)) : Unit(node);
+ }
+
+ private SafeCoreMirOperand? LoopControl(SafeCoreHirNode node, int depth)
+ {
+ LoopContext? context = null;
+ for (int index = _loops.Count - 1; index >= 0; index--)
+ {
+ Step(node, depth);
+ if (node.Name is null || node.Name == _loops[index].Label) { context = _loops[index]; break; }
+ }
+ if (context is null) Invalid(node);
+ if (node.Kind == N.ContinueExpression)
+ {
+ End(SafeCoreMirTerminator.Goto(context!.Header, Source(node)));
+ return null;
+ }
+ SafeCoreMirOperand? value = node.ChildIds.Count == 0 ? Unit(node) : Expr(Child(node, 0), depth + 1);
+ if (_current is null || value is null) return null;
+ if (context!.Result is int result) Assign(result, value, node);
+ context.HasBreak = true;
+ End(SafeCoreMirTerminator.Goto(context.Exit, Source(node)));
+ return null;
+ }
+
+ private bool Join(int? destination, SafeCoreMirOperand? value, BlockBuilder join, SafeCoreHirNode node)
+ {
+ if (_current is null) return false;
+ if (destination is int local)
+ {
+ if (value is null) Invalid(node);
+ Assign(local, value!, node);
+ }
+ End(SafeCoreMirTerminator.Goto(join.Id, Source(node)));
+ return true;
+ }
+
+ private SafeCoreMirOperand Literal(SafeCoreHirNode node, SafeCoreType type, bool negate = false,
+ SafeCoreHirNode? origin = null)
+ {
+ Scalar(type, node);
+ string text = node.Value ?? string.Empty;
+ if (text.Length is 0 or > 4_096) Unsupported(node);
+ string value;
+ if (type.Kind == K.Bool) value = text;
+ else if (type.Kind == K.Char || text.StartsWith("b'", StringComparison.Ordinal))
+ {
+ string character = text[(type.Kind == K.Char ? 1 : 2)..^1];
+ int scalar = character.StartsWith("\\u{", StringComparison.Ordinal)
+ ? int.Parse(character[3..^1].Replace("_", string.Empty, StringComparison.Ordinal), NumberStyles.HexNumber, CultureInfo.InvariantCulture)
+ : character.StartsWith("\\x", StringComparison.Ordinal)
+ ? int.Parse(character[2..], NumberStyles.HexNumber, CultureInfo.InvariantCulture)
+ : character switch
+ {
+ "\\n" => '\n', "\\r" => '\r', "\\t" => '\t', "\\0" => 0,
+ "\\\\" => '\\', "\\'" => '\'', "\\\"" => '"',
+ _ => Rune.GetRuneAt(character, 0).Value,
+ };
+ value = scalar.ToString(CultureInfo.InvariantCulture);
+ }
+ else
+ {
+ string suffix = type.ToString();
+ text = text.Replace("_", string.Empty, StringComparison.Ordinal);
+ if (text.EndsWith(suffix, StringComparison.Ordinal)) text = text[..^suffix.Length];
+ if (type.IsFloat)
+ {
+ double number = double.Parse(text, NumberStyles.Float, CultureInfo.InvariantCulture);
+ value = type.Kind == K.F32 ? ((float)number).ToString("R", CultureInfo.InvariantCulture)
+ : number.ToString("R", CultureInfo.InvariantCulture);
+ }
+ else
+ {
+ int radix = text.StartsWith("0x", StringComparison.Ordinal) ? 16 :
+ text.StartsWith("0o", StringComparison.Ordinal) ? 8 : text.StartsWith("0b", StringComparison.Ordinal) ? 2 : 10;
+ int start = radix == 10 ? 0 : 2;
+ BigInteger number = BigInteger.Zero;
+ for (int index = start; index < text.Length; index++)
+ {
+ Step(node, 0);
+ char c = char.ToLowerInvariant(text[index]);
+ int digit = c is >= 'a' and <= 'f' ? c - 'a' + 10 : c - '0';
+ if (digit < 0 || digit >= radix) Invalid(node);
+ number = number * radix + digit;
+ }
+ value = (negate ? -number : number).ToString(CultureInfo.InvariantCulture);
+ }
+ }
+ return SafeCoreMirOperand.Constant(type, value, Source(origin ?? node));
+ }
+
+ private SafeCoreHirNode UnwrapExpression(SafeCoreHirNode node, int depth)
+ {
+ for (int index = 0; index <= options.MaximumNestingDepth; index++)
+ {
+ Step(node, depth + index);
+ if (node.Kind != N.TupleExpression || node.ChildIds.Count != 1 ||
+ node.Modifiers.HasFlag(SafeCoreHirNodeModifiers.HasTrailingComma)) return node;
+ node = Child(node, 0);
+ }
+ Limit(node); return null!;
+ }
+
+ private SafeCoreHirNode UnwrapPattern(SafeCoreHirNode node)
+ {
+ for (int depth = 0; depth <= options.MaximumNestingDepth; depth++)
+ {
+ Step(node, depth);
+ if (node.Kind != N.TuplePattern || node.ChildIds.Count != 1 ||
+ node.Modifiers.HasFlag(SafeCoreHirNodeModifiers.HasTrailingComma)) return node;
+ node = Child(node, 0);
+ }
+ Limit(node); return null!;
+ }
+
+ private SafeCoreMirOperand Emit(SafeCoreMirRvalue value, SafeCoreType type, SafeCoreHirNode node)
+ {
+ int local = Temp(type, node);
+ _current!.Statements.Add(new(local, value, Source(node)));
+ return SafeCoreMirOperand.Local(local, type, Source(node));
+ }
+
+ private void Assign(int local, SafeCoreMirOperand value, SafeCoreHirNode node) =>
+ _current!.Statements.Add(new(local, SafeCoreMirRvalue.Use(value, Source(node)), Source(node)));
+
+ private int Temp(SafeCoreType type, SafeCoreHirNode node) => Local(
+ $"tmp{_locals.Count.ToString(CultureInfo.InvariantCulture)}", type, SafeCoreMirLocalKind.Temporary, false, node);
+
+ private int Local(string name, SafeCoreType type, SafeCoreMirLocalKind kind, bool mutable, SafeCoreHirNode node)
+ {
+ Step(node, 0);
+ Scalar(type, node);
+ if (_locals.Count >= options.MaximumLocalsPerFunction) Limit(node);
+ int id = _locals.Count;
+ _locals.Add(new(id, name, type, kind, mutable, Source(node)));
+ return id;
+ }
+
+ private BlockBuilder Block(SafeCoreHirNode node)
+ {
+ Step(node, 0);
+ if (_blocks.Count >= options.MaximumBlocksPerFunction) Limit(node);
+ var block = new BlockBuilder(_blocks.Count, Source(node));
+ _blocks.Add(block);
+ return block;
+ }
+
+ private void End(SafeCoreMirTerminator terminator)
+ {
+ _current!.Terminator = terminator;
+ _current = null;
+ }
+
+ private SafeCoreType EffectiveType(SafeCoreHirNode node) =>
+ input.Coercions.TryGetValue(node.Id, out SafeCoreType? target) ? target : Type(node);
+
+ private SafeCoreType Type(SafeCoreHirNode node)
+ {
+ if (!input.Types.TryGetValue(node.Id, out SafeCoreType? type) || type is null) Invalid(node);
+ return type!;
+ }
+
+ private static void Scalar(SafeCoreType type, SafeCoreHirNode node, bool allowNever = false)
+ {
+ if (!(type.IsInteger || type.IsFloat || type.Kind is K.Unit or K.Bool or K.Char || allowNever && type.Kind == K.Never))
+ Unsupported(node);
+ }
+
+ private SafeCoreHirNode Child(SafeCoreHirNode node, int index)
+ {
+ if ((uint)index >= (uint)node.ChildIds.Count) Invalid(node);
+ int id = node.ChildIds[index];
+ if ((uint)id >= (uint)input.Hir.Nodes.Count) Invalid(node);
+ return input.Hir.GetNode(id);
+ }
+
+ private SafeCoreMirSource Source(SafeCoreHirNode node) =>
+ new(input.Hir.SourcePath, node.Span, node.Id, input.Hir.Root!.Span.End);
+
+ private SafeCoreMirOperand Unit(SafeCoreHirNode node) =>
+ SafeCoreMirOperand.Constant(SafeCoreType.Primitive(K.Unit), "()", Source(node));
+
+ private static string SymbolKey(SafeCoreSymbol symbol) =>
+ symbol.ResolvedImportTargetQualifiedName ?? symbol.QualifiedName;
+
+ private void Step(SafeCoreHirNode node, int depth)
+ {
+ cancellation.ThrowIfCancellationRequested();
+ if (++_operations > options.MaximumOperations || depth > options.MaximumNestingDepth || _clock.Elapsed >= options.Timeout)
+ Limit(node);
+ }
+
+ [DoesNotReturn]
+ private static void Invalid(SafeCoreHirNode node) => throw new LoweringException(new(InvalidEvidence,
+ "MIR lowering requires complete and consistent resolved type evidence.", node.Span));
+
+ [DoesNotReturn]
+ private static void Unsupported(SafeCoreHirNode node) => throw new LoweringException(new(UnsupportedSyntax,
+ "This construct is outside the scalar MIR profile; aggregate, reference, closure, pattern and const lowering are not yet available.", node.Span));
+
+ [DoesNotReturn]
+ private static void Limit(SafeCoreHirNode node) => throw new LoweringException(new(LimitReached,
+ "MIR lowering exceeded its configured work, size, depth or time limit.", node.Span));
+ }
+}
diff --git a/src/RustSharp.Semantics/SafeCoreMirModels.cs b/src/RustSharp.Semantics/SafeCoreMirModels.cs
new file mode 100644
index 0000000..0453dd3
--- /dev/null
+++ b/src/RustSharp.Semantics/SafeCoreMirModels.cs
@@ -0,0 +1,177 @@
+using System.Diagnostics;
+using RustSharp.Syntax;
+
+namespace RustSharp.Semantics;
+
+/// Original source evidence for a MIR element. IDs and offsets are nonnegative.
+public sealed record SafeCoreMirSource(string SourcePath, TextSpan Span, int HirNodeId, int SourceLength);
+
+public enum SafeCoreMirLocalKind { Parameter, User, Temporary }
+public enum SafeCoreMirOperandKind { Local, Constant, Function }
+public enum SafeCoreMirRvalueKind { Use, Unary, Binary, Coerce, Cast, Tuple }
+public enum SafeCoreMirTerminatorKind { Return, Goto, Branch, Call, Unreachable }
+
+/// A local slot. ID is its index in the owning function. Parameters precede other slots.
+public sealed record SafeCoreMirLocal(int Id, string Name, SafeCoreType Type,
+ SafeCoreMirLocalKind Kind, bool IsMutable, SafeCoreMirSource Source);
+
+/// One immutable leaf operand. Constants use invariant decimal text, bool words,
+/// decimal Unicode scalar values for char, or () for unit; they are not Rust source tokens.
+public sealed record SafeCoreMirOperand(SafeCoreMirOperandKind Kind, SafeCoreType Type,
+ int Id, string? Value, SafeCoreMirSource Source)
+{
+ public static SafeCoreMirOperand Local(int localId, SafeCoreType type, SafeCoreMirSource source) =>
+ new(SafeCoreMirOperandKind.Local, type, localId, null, source);
+ public static SafeCoreMirOperand Constant(SafeCoreType type, string value, SafeCoreMirSource source) =>
+ new(SafeCoreMirOperandKind.Constant, type, -1, value, source);
+ public static SafeCoreMirOperand Function(int functionId, SafeCoreType type, SafeCoreMirSource source) =>
+ new(SafeCoreMirOperandKind.Function, type, functionId, null, source);
+}
+
+/// An explicit typed computation. Collections are copied with bounded indexed access.
+public sealed class SafeCoreMirRvalue
+{
+ public SafeCoreMirRvalue(SafeCoreMirRvalueKind kind, SafeCoreType type,
+ IReadOnlyList operands, string? @operator, SafeCoreMirSource source,
+ CancellationToken cancellationToken = default)
+ {
+ Kind = kind;
+ Type = type;
+ Operands = SafeCoreMirCollections.Freeze(operands, cancellationToken);
+ Operator = @operator;
+ Source = source;
+ }
+
+ public SafeCoreMirRvalueKind Kind { get; }
+ public SafeCoreType Type { get; }
+ public IReadOnlyList Operands { get; }
+ public string? Operator { get; }
+ public SafeCoreMirSource Source { get; }
+ public static SafeCoreMirRvalue Use(SafeCoreMirOperand operand, SafeCoreMirSource source) =>
+ new(SafeCoreMirRvalueKind.Use, operand.Type, [operand], null, source);
+ public static SafeCoreMirRvalue Unary(string op, SafeCoreMirOperand operand, SafeCoreType resultType, SafeCoreMirSource source) =>
+ new(SafeCoreMirRvalueKind.Unary, resultType, [operand], op, source);
+ public static SafeCoreMirRvalue Binary(string op, SafeCoreMirOperand left, SafeCoreMirOperand right,
+ SafeCoreType resultType, SafeCoreMirSource source) =>
+ new(SafeCoreMirRvalueKind.Binary, resultType, [left, right], op, source);
+ public static SafeCoreMirRvalue Coerce(SafeCoreMirOperand operand, SafeCoreType resultType, SafeCoreMirSource source) =>
+ new(SafeCoreMirRvalueKind.Coerce, resultType, [operand], null, source);
+ public static SafeCoreMirRvalue Cast(SafeCoreMirOperand operand, SafeCoreType resultType, SafeCoreMirSource source) =>
+ new(SafeCoreMirRvalueKind.Cast, resultType, [operand], null, source);
+ public static SafeCoreMirRvalue Tuple(IReadOnlyList operands, SafeCoreType resultType,
+ SafeCoreMirSource source, CancellationToken cancellationToken = default) =>
+ new(SafeCoreMirRvalueKind.Tuple, resultType, operands, null, source, cancellationToken);
+}
+
+/// Assign a value to a local slot. Source binding mutability is checked by HIR;
+/// MIR locals are storage slots and may be written on separate CFG paths.
+public sealed record SafeCoreMirStatement(int DestinationLocalId, SafeCoreMirRvalue Value, SafeCoreMirSource Source);
+
+/// Exactly one explicit control-flow terminator ends every basic block.
+/// Unused target IDs use -1; a diverging call uses continuation -1 and no destination.
+public sealed class SafeCoreMirTerminator
+{
+ public SafeCoreMirTerminator(SafeCoreMirTerminatorKind kind, SafeCoreMirOperand? operand,
+ IReadOnlyList arguments, int? destinationLocalId, int targetBlockId,
+ int falseTargetBlockId, SafeCoreMirSource source, CancellationToken cancellationToken = default)
+ {
+ Kind = kind;
+ Operand = operand;
+ Arguments = SafeCoreMirCollections.Freeze(arguments, cancellationToken);
+ DestinationLocalId = destinationLocalId;
+ TargetBlockId = targetBlockId;
+ FalseTargetBlockId = falseTargetBlockId;
+ Source = source;
+ }
+
+ public SafeCoreMirTerminatorKind Kind { get; }
+ public SafeCoreMirOperand? Operand { get; }
+ public IReadOnlyList Arguments { get; }
+ public int? DestinationLocalId { get; }
+ public int TargetBlockId { get; }
+ public int FalseTargetBlockId { get; }
+ public SafeCoreMirSource Source { get; }
+ public static SafeCoreMirTerminator Return(SafeCoreMirOperand? value, SafeCoreMirSource source) =>
+ new(SafeCoreMirTerminatorKind.Return, value, [], null, -1, -1, source);
+ public static SafeCoreMirTerminator Goto(int target, SafeCoreMirSource source) =>
+ new(SafeCoreMirTerminatorKind.Goto, null, [], null, target, -1, source);
+ public static SafeCoreMirTerminator Branch(SafeCoreMirOperand condition, int trueTarget, int falseTarget, SafeCoreMirSource source) =>
+ new(SafeCoreMirTerminatorKind.Branch, condition, [], null, trueTarget, falseTarget, source);
+ public static SafeCoreMirTerminator Call(SafeCoreMirOperand callee, IReadOnlyList arguments,
+ int? destinationLocalId, int continuationBlockId, SafeCoreMirSource source, CancellationToken cancellationToken = default) =>
+ new(SafeCoreMirTerminatorKind.Call, callee, arguments, destinationLocalId, continuationBlockId, -1, source, cancellationToken);
+ public static SafeCoreMirTerminator Unreachable(SafeCoreMirSource source) =>
+ new(SafeCoreMirTerminatorKind.Unreachable, null, [], null, -1, -1, source);
+}
+
+public sealed class SafeCoreMirBlock
+{
+ public SafeCoreMirBlock(int id, IReadOnlyList statements,
+ SafeCoreMirTerminator terminator, SafeCoreMirSource source, CancellationToken cancellationToken = default)
+ {
+ Id = id;
+ Statements = SafeCoreMirCollections.Freeze(statements, cancellationToken);
+ Terminator = terminator;
+ Source = source;
+ }
+ public int Id { get; }
+ public IReadOnlyList Statements { get; }
+ public SafeCoreMirTerminator Terminator { get; }
+ public SafeCoreMirSource Source { get; }
+}
+
+public sealed class SafeCoreMirFunction
+{
+ public SafeCoreMirFunction(int id, string name, SafeCoreType returnType,
+ IReadOnlyList locals, IReadOnlyList blocks, int entryBlockId,
+ SafeCoreMirSource source, CancellationToken cancellationToken = default)
+ {
+ Id = id;
+ Name = name;
+ ReturnType = returnType;
+ Locals = SafeCoreMirCollections.Freeze(locals, cancellationToken);
+ Blocks = SafeCoreMirCollections.Freeze(blocks, cancellationToken);
+ EntryBlockId = entryBlockId;
+ Source = source;
+ }
+ public int Id { get; }
+ public string Name { get; }
+ public SafeCoreType ReturnType { get; }
+ public IReadOnlyList Locals { get; }
+ public IReadOnlyList Blocks { get; }
+ public int EntryBlockId { get; }
+ public SafeCoreMirSource Source { get; }
+}
+
+/// Backend-independent typed MIR. IDs index immutable owning collections.
+public sealed class SafeCoreMirProgram
+{
+ public SafeCoreMirProgram(IReadOnlyList functions, CancellationToken cancellationToken = default) =>
+ Functions = SafeCoreMirCollections.Freeze(functions, cancellationToken);
+ public IReadOnlyList Functions { get; }
+}
+
+public sealed class SafeCoreMirLimitException(string message) : Exception(message);
+
+internal static class SafeCoreMirCollections
+{
+ public static IReadOnlyList Freeze(IReadOnlyList items, CancellationToken cancellationToken = default)
+ {
+ ArgumentNullException.ThrowIfNull(items);
+ cancellationToken.ThrowIfCancellationRequested();
+ var clock = Stopwatch.StartNew();
+ int count = items.Count;
+ if (count is < 0 or > 100_000) throw new SafeCoreMirLimitException("MIR collection limit reached.");
+ var copy = new T[count];
+ for (int index = 0; index < count; index++)
+ {
+ cancellationToken.ThrowIfCancellationRequested();
+ if (clock.Elapsed > TimeSpan.FromSeconds(10)) throw new SafeCoreMirLimitException("MIR construction timeout reached.");
+ copy[index] = items[index];
+ ArgumentNullException.ThrowIfNull(copy[index]);
+ }
+ cancellationToken.ThrowIfCancellationRequested();
+ if (clock.Elapsed > TimeSpan.FromSeconds(10)) throw new SafeCoreMirLimitException("MIR construction timeout reached.");
+ return Array.AsReadOnly(copy);
+ }
+}
diff --git a/src/RustSharp.Semantics/SafeCoreMirValidation.cs b/src/RustSharp.Semantics/SafeCoreMirValidation.cs
new file mode 100644
index 0000000..117f36b
--- /dev/null
+++ b/src/RustSharp.Semantics/SafeCoreMirValidation.cs
@@ -0,0 +1,500 @@
+using System.Collections.ObjectModel;
+using System.Diagnostics;
+using System.Globalization;
+using System.Numerics;
+
+namespace RustSharp.Semantics;
+
+public sealed record SafeCoreMirValidationOptions
+{
+ public TimeSpan Timeout { get; init; } = TimeSpan.FromSeconds(10);
+ public CancellationToken CancellationToken { get; init; }
+ public int MaximumOperations { get; init; } = 1_000_000;
+ public int MaximumFunctions { get; init; } = 4_096;
+ public int MaximumLocals { get; init; } = 100_000;
+ public int MaximumBlocks { get; init; } = 100_000;
+ public int MaximumStatements { get; init; } = 100_000;
+ public int MaximumDiagnostics { get; init; } = 128;
+ public int MaximumTypeDepth { get; init; } = 128;
+}
+
+public static class SafeCoreMirDiagnosticCodes
+{
+ public const string InvalidInput = "RSM0001";
+ public const string LimitReached = "RSM0002";
+ public const string InvalidControlFlow = "RSM1001";
+ public const string TypeMismatch = "RSM1002";
+ public const string InvalidSource = "RSM1003";
+ public const string InvalidOperand = "RSM1004";
+ public const string UnsupportedNode = "RSM1005";
+}
+
+public sealed record SafeCoreMirDiagnostic(string Code, string Message, SafeCoreMirSource? Source,
+ int FunctionId = -1, int BlockId = -1);
+
+public sealed class SafeCoreMirValidationResult
+{
+ internal SafeCoreMirValidationResult(List diagnostics,
+ Dictionary> reachableBlocks, bool isTruncated)
+ {
+ Diagnostics = diagnostics.AsReadOnly();
+ ReachableBlocks = new ReadOnlyDictionary>(reachableBlocks);
+ IsTruncated = isTruncated;
+ }
+ public IReadOnlyList Diagnostics { get; }
+ public IReadOnlyDictionary> ReachableBlocks { get; }
+ public bool IsTruncated { get; }
+ public bool IsSuccessful => !IsTruncated && Diagnostics.Count == 0;
+}
+
+/// Checks structural, source and type invariants, including unreachable blocks.
+/// CFG cycles are legal. This is not ownership or definite-initialization analysis.
+public static class SafeCoreMirValidation
+{
+ public static SafeCoreMirValidationResult Validate(SafeCoreMirProgram program,
+ SafeCoreMirValidationOptions? options = null)
+ {
+ ArgumentNullException.ThrowIfNull(program);
+ options ??= new();
+ ArgumentOutOfRangeException.ThrowIfLessThanOrEqual(options.Timeout, TimeSpan.Zero);
+ ArgumentOutOfRangeException.ThrowIfNegativeOrZero(options.MaximumOperations);
+ ArgumentOutOfRangeException.ThrowIfNegativeOrZero(options.MaximumFunctions);
+ ArgumentOutOfRangeException.ThrowIfNegativeOrZero(options.MaximumLocals);
+ ArgumentOutOfRangeException.ThrowIfNegativeOrZero(options.MaximumBlocks);
+ ArgumentOutOfRangeException.ThrowIfNegativeOrZero(options.MaximumStatements);
+ ArgumentOutOfRangeException.ThrowIfNegativeOrZero(options.MaximumDiagnostics);
+ ArgumentOutOfRangeException.ThrowIfNegativeOrZero(options.MaximumTypeDepth);
+ return new Validator(program, options).Run();
+ }
+
+ private sealed class Validator(SafeCoreMirProgram program, SafeCoreMirValidationOptions options)
+ {
+ private readonly Stopwatch _clock = Stopwatch.StartNew();
+ private readonly List _diagnostics = [];
+ private readonly Dictionary> _reachable = [];
+ private SafeCoreMirFunction? _function;
+ private SafeCoreMirBlock? _block;
+ private int _operations;
+ private int _locals;
+ private int _blocks;
+ private int _statements;
+
+ public SafeCoreMirValidationResult Run()
+ {
+ try
+ {
+ Step();
+ Limit(program.Functions.Count, options.MaximumFunctions, 4_096);
+ var names = new HashSet(StringComparer.Ordinal);
+ for (int index = 0; index < program.Functions.Count; index++)
+ {
+ Step();
+ _function = program.Functions[index];
+ _block = null;
+ Source(_function.Source);
+ if (_function.Id != index || string.IsNullOrEmpty(_function.Name)
+ || _function.Name.Length > 4_096 || !names.Add(_function.Name))
+ Error(SafeCoreMirDiagnosticCodes.InvalidInput, "Function IDs must index the arena and names must be unique and bounded.", _function.Source);
+ if (Type(_function.ReturnType)) Function();
+ }
+ return new(_diagnostics, _reachable, false);
+ }
+ catch (SafeCoreMirLimitException exception)
+ {
+ _diagnostics.Add(new(SafeCoreMirDiagnosticCodes.LimitReached, exception.Message,
+ _block?.Source ?? _function?.Source, _function?.Id ?? -1, _block?.Id ?? -1));
+ return new(_diagnostics, _reachable, true);
+ }
+ }
+
+ private void Step()
+ {
+ options.CancellationToken.ThrowIfCancellationRequested();
+ if (++_operations > Math.Clamp(options.MaximumOperations, 1, 1_000_000)
+ || _clock.Elapsed >= (options.Timeout > TimeSpan.Zero && options.Timeout <= TimeSpan.FromMinutes(1)
+ ? options.Timeout : TimeSpan.FromSeconds(10)))
+ throw new SafeCoreMirLimitException("MIR validation work or time limit reached.");
+ }
+
+ private static void Limit(int count, int requested, int ceiling)
+ {
+ if (count > Math.Clamp(requested, 1, ceiling)) throw new SafeCoreMirLimitException("MIR validation size limit reached.");
+ }
+
+ private void Error(string code, string message, SafeCoreMirSource? source)
+ {
+ Step();
+ if (_diagnostics.Count >= Math.Clamp(options.MaximumDiagnostics, 1, 1_024))
+ throw new SafeCoreMirLimitException("MIR diagnostic limit reached.");
+ _diagnostics.Add(new(code, message, source, _function?.Id ?? -1, _block?.Id ?? -1));
+ }
+
+ private void Source(SafeCoreMirSource? source)
+ {
+ Step();
+ if (source is null || string.IsNullOrWhiteSpace(source.SourcePath) || source.SourcePath.Length > 4_096
+ || source.HirNodeId < 0 || source.SourceLength < 0 || source.Span.Start < 0 || source.Span.Length < 0
+ || (long)source.Span.Start + source.Span.Length > source.SourceLength)
+ Error(SafeCoreMirDiagnosticCodes.InvalidSource, "MIR source evidence requires a path, HIR ID and a span within its source.", source);
+ }
+
+ private bool Type(SafeCoreType? type, int depth = 0)
+ {
+ Step();
+ if (depth >= Math.Clamp(options.MaximumTypeDepth, 1, 128)) throw new SafeCoreMirLimitException("MIR type nesting limit reached.");
+ if (type is null || type.Kind is SafeCoreSemanticTypeKind.Inference or SafeCoreSemanticTypeKind.Error)
+ {
+ Error(SafeCoreMirDiagnosticCodes.TypeMismatch, "MIR requires a fully resolved non-error type.", _block?.Source ?? _function?.Source);
+ return false;
+ }
+ bool valid = true;
+ for (int index = 0; index < type.Elements.Count; index++) valid &= Type(type.Elements[index], depth + 1);
+ return valid;
+ }
+
+ private void Function()
+ {
+ SafeCoreMirFunction function = _function!;
+ _locals += function.Locals.Count;
+ _blocks += function.Blocks.Count;
+ Limit(_locals, options.MaximumLocals, 100_000);
+ Limit(_blocks, options.MaximumBlocks, 100_000);
+ bool pastParameters = false;
+ for (int index = 0; index < function.Locals.Count; index++)
+ {
+ Step();
+ SafeCoreMirLocal local = function.Locals[index];
+ Source(local.Source);
+ Type(local.Type);
+ if (local.Id != index || string.IsNullOrEmpty(local.Name) || local.Name.Length > 4_096
+ || !Enum.IsDefined(local.Kind))
+ Error(SafeCoreMirDiagnosticCodes.InvalidInput, "Local IDs must index the arena and local metadata must be valid.", local.Source);
+ if (local.Type?.Kind == SafeCoreSemanticTypeKind.Never)
+ Error(SafeCoreMirDiagnosticCodes.TypeMismatch, "The never type cannot occupy a local slot.", local.Source);
+ if (local.Kind == SafeCoreMirLocalKind.Parameter && pastParameters)
+ Error(SafeCoreMirDiagnosticCodes.InvalidInput, "Parameter slots must precede other locals.", local.Source);
+ pastParameters |= local.Kind != SafeCoreMirLocalKind.Parameter;
+ }
+ Target(function.EntryBlockId, function.Source);
+ for (int index = 0; index < function.Blocks.Count; index++)
+ {
+ Step();
+ _block = function.Blocks[index];
+ Source(_block.Source);
+ if (_block.Id != index) Error(SafeCoreMirDiagnosticCodes.InvalidControlFlow, "Block IDs must index the function's block arena.", _block.Source);
+ _statements += _block.Statements.Count;
+ Limit(_statements, options.MaximumStatements, 100_000);
+ for (int statementIndex = 0; statementIndex < _block.Statements.Count; statementIndex++)
+ {
+ Step();
+ SafeCoreMirStatement statement = _block.Statements[statementIndex];
+ Source(statement.Source);
+ SafeCoreType? destination = LocalType(statement.DestinationLocalId, statement.Source);
+ if (statement.Value is null)
+ Error(SafeCoreMirDiagnosticCodes.InvalidInput, "An assignment requires a value.", statement.Source);
+ else
+ {
+ Rvalue(statement.Value);
+ Equal(destination, statement.Value.Type, statement.Source, "Assignment type differs from its destination.");
+ }
+ }
+ Terminator(_block.Terminator);
+ }
+ Reachability();
+ }
+
+ private SafeCoreType? LocalType(int id, SafeCoreMirSource? source)
+ {
+ Step();
+ if (id < 0 || id >= _function!.Locals.Count)
+ {
+ Error(SafeCoreMirDiagnosticCodes.InvalidOperand, "Local ID is outside the function's local arena.", source);
+ return null;
+ }
+ return _function.Locals[id].Type;
+ }
+
+ private void Equal(SafeCoreType? expected, SafeCoreType? actual, SafeCoreMirSource? source, string message)
+ {
+ Step();
+ if (expected is not null && actual is not null && expected != actual)
+ Error(SafeCoreMirDiagnosticCodes.TypeMismatch, message, source);
+ }
+
+ private bool Operand(SafeCoreMirOperand operand)
+ {
+ Step();
+ Source(operand.Source);
+ if (!Type(operand.Type)) return false;
+ switch (operand.Kind)
+ {
+ case SafeCoreMirOperandKind.Local:
+ Equal(LocalType(operand.Id, operand.Source), operand.Type, operand.Source, "Local operand type differs from its slot.");
+ if (operand.Value is not null) Error(SafeCoreMirDiagnosticCodes.InvalidOperand, "A local operand cannot carry a constant payload.", operand.Source);
+ break;
+ case SafeCoreMirOperandKind.Function:
+ if (operand.Id < 0 || operand.Id >= program.Functions.Count)
+ Error(SafeCoreMirDiagnosticCodes.InvalidOperand, "Function operand ID is outside the function arena.", operand.Source);
+ else
+ {
+ SafeCoreMirFunction target = program.Functions[operand.Id];
+ int parameterCount = 0;
+ for (int index = 0; index < target.Locals.Count; index++)
+ {
+ Step();
+ if (target.Locals[index].Kind != SafeCoreMirLocalKind.Parameter) break;
+ parameterCount++;
+ }
+ if (operand.Type.Kind != SafeCoreSemanticTypeKind.Function || operand.Type.Name != target.Name
+ || operand.Type.ParameterTypes.Count != parameterCount || operand.Type.ReturnType != target.ReturnType)
+ Error(SafeCoreMirDiagnosticCodes.TypeMismatch, "Function operand does not match its declaration's nominal signature.", operand.Source);
+ else
+ for (int index = 0; index < parameterCount; index++)
+ Equal(target.Locals[index].Type, operand.Type.ParameterTypes[index], operand.Source, "Function parameter signature mismatch.");
+ }
+ if (operand.Value is not null) Error(SafeCoreMirDiagnosticCodes.InvalidOperand, "A function operand cannot carry a constant payload.", operand.Source);
+ break;
+ case SafeCoreMirOperandKind.Constant:
+ if (operand.Id != -1 || !Constant(operand.Type, operand.Value))
+ Error(SafeCoreMirDiagnosticCodes.InvalidOperand, "Constant payload is invalid or out of range for its type.", operand.Source);
+ break;
+ default:
+ Error(SafeCoreMirDiagnosticCodes.InvalidOperand, "Unknown operand kind.", operand.Source);
+ break;
+ }
+ return true;
+ }
+
+ private static bool Constant(SafeCoreType type, string? text)
+ {
+ if (text is null || text.Length > 4_096) return false;
+ if (type.Kind == SafeCoreSemanticTypeKind.Unit) return text == "()";
+ if (type.Kind == SafeCoreSemanticTypeKind.Bool) return text is "true" or "false";
+ if (type.IsFloat)
+ return double.TryParse(text, NumberStyles.Float, CultureInfo.InvariantCulture, out double value)
+ && double.IsFinite(value) && (type.Kind != SafeCoreSemanticTypeKind.F32 || float.IsFinite((float)value));
+ if ((!type.IsInteger && type.Kind != SafeCoreSemanticTypeKind.Char)
+ || !BigInteger.TryParse(text, NumberStyles.AllowLeadingSign, CultureInfo.InvariantCulture, out BigInteger number)) return false;
+ if (type.Kind == SafeCoreSemanticTypeKind.Char) return number >= 0 && number <= 0x10ffff && (number < 0xd800 || number > 0xdfff);
+ int bits = type.Kind switch
+ {
+ SafeCoreSemanticTypeKind.I8 or SafeCoreSemanticTypeKind.U8 => 8,
+ SafeCoreSemanticTypeKind.I16 or SafeCoreSemanticTypeKind.U16 => 16,
+ SafeCoreSemanticTypeKind.I32 or SafeCoreSemanticTypeKind.U32 => 32,
+ SafeCoreSemanticTypeKind.I128 or SafeCoreSemanticTypeKind.U128 => 128,
+ _ => 64,
+ };
+ bool signed = type.Kind is >= SafeCoreSemanticTypeKind.I8 and <= SafeCoreSemanticTypeKind.Isize;
+ BigInteger magnitude = BigInteger.One << (signed ? bits - 1 : bits);
+ return number >= (signed ? -magnitude : BigInteger.Zero) && number < magnitude;
+ }
+
+ private void Rvalue(SafeCoreMirRvalue value)
+ {
+ Step();
+ Source(value.Source);
+ if (!Type(value.Type)) return;
+ bool validOperands = true;
+ for (int index = 0; index < value.Operands.Count; index++) validOperands &= Operand(value.Operands[index]);
+ if (!validOperands) return;
+ int expectedCount = value.Kind switch
+ {
+ SafeCoreMirRvalueKind.Use or SafeCoreMirRvalueKind.Unary or SafeCoreMirRvalueKind.Coerce or SafeCoreMirRvalueKind.Cast => 1,
+ SafeCoreMirRvalueKind.Binary => 2,
+ SafeCoreMirRvalueKind.Tuple => value.Type.Kind == SafeCoreSemanticTypeKind.Unit ? 0 : value.Type.Elements.Count,
+ _ => -1,
+ };
+ if (expectedCount < 0 || value.Operands.Count != expectedCount)
+ {
+ Error(SafeCoreMirDiagnosticCodes.InvalidOperand, "Rvalue operand count or kind is invalid.", value.Source);
+ return;
+ }
+ if (value.Kind is not (SafeCoreMirRvalueKind.Unary or SafeCoreMirRvalueKind.Binary) && value.Operator is not null)
+ Error(SafeCoreMirDiagnosticCodes.InvalidOperand, "Only unary and binary computations carry an operator.", value.Source);
+ SafeCoreType? first = value.Operands.Count > 0 ? value.Operands[0].Type : null;
+ bool valid = value.Kind switch
+ {
+ SafeCoreMirRvalueKind.Use => first == value.Type,
+ SafeCoreMirRvalueKind.Unary => Unary(value.Operator, first!, value.Type),
+ SafeCoreMirRvalueKind.Binary => Binary(value.Operator, first!, value.Operands[1].Type, value.Type),
+ SafeCoreMirRvalueKind.Coerce => Coercion(first!, value.Type),
+ SafeCoreMirRvalueKind.Cast => Cast(first!, value.Type),
+ SafeCoreMirRvalueKind.Tuple => Tuple(value),
+ _ => false,
+ };
+ if (!valid) Error(SafeCoreMirDiagnosticCodes.TypeMismatch, "Rvalue operator and operand/result types are incompatible.", value.Source);
+ }
+
+ private static bool Unary(string? op, SafeCoreType operand, SafeCoreType result) => result == operand && op switch
+ {
+ "-" => operand.IsFloat || operand.Kind is >= SafeCoreSemanticTypeKind.I8 and <= SafeCoreSemanticTypeKind.Isize,
+ "!" => operand.IsInteger || operand.Kind == SafeCoreSemanticTypeKind.Bool,
+ _ => false,
+ };
+
+ private static bool Binary(string? op, SafeCoreType left, SafeCoreType right, SafeCoreType result) => op switch
+ {
+ "+" or "-" or "*" or "/" or "%" => left == right && result == left && (left.IsInteger || left.IsFloat),
+ "&" or "|" or "^" => left == right && result == left && (left.IsInteger || left.Kind == SafeCoreSemanticTypeKind.Bool),
+ "<<" or ">>" => left.IsInteger && right.IsInteger && result == left,
+ "==" or "!=" or "<" or "<=" or ">" or ">=" => left == right && result.Kind == SafeCoreSemanticTypeKind.Bool
+ && (left.IsInteger || left.IsFloat || left.Kind is SafeCoreSemanticTypeKind.Bool or SafeCoreSemanticTypeKind.Char),
+ _ => false,
+ };
+
+ private bool Coercion(SafeCoreType from, SafeCoreType to)
+ {
+ Step();
+ var inference = new SafeCoreTypeInference(new()
+ {
+ MaximumOperations = Math.Max(1, Math.Clamp(options.MaximumOperations, 1, 1_000_000) - _operations),
+ MaximumNestingDepth = Math.Clamp(options.MaximumTypeDepth, 1, 128),
+ Timeout = options.Timeout > TimeSpan.Zero ? options.Timeout : TimeSpan.FromSeconds(10),
+ CancellationToken = options.CancellationToken,
+ });
+ try { return inference.Coerce(from, to); }
+ catch (SafeCoreTypeInferenceLimitException) { throw new SafeCoreMirLimitException("MIR coercion work limit reached."); }
+ }
+
+ private static bool Cast(SafeCoreType from, SafeCoreType to) =>
+ (from.IsInteger || from.IsFloat || from.Kind is SafeCoreSemanticTypeKind.Bool or SafeCoreSemanticTypeKind.Char)
+ && (to.IsInteger || to.IsFloat && (from.IsInteger || from.IsFloat)
+ || to.Kind == SafeCoreSemanticTypeKind.Char && from.Kind == SafeCoreSemanticTypeKind.U8);
+
+ private bool Tuple(SafeCoreMirRvalue value)
+ {
+ if (value.Type.Kind == SafeCoreSemanticTypeKind.Unit) return value.Operands.Count == 0;
+ if (value.Type.Kind != SafeCoreSemanticTypeKind.Tuple) return false;
+ for (int index = 0; index < value.Operands.Count; index++)
+ {
+ Step();
+ if (value.Operands[index].Type != value.Type.Elements[index]) return false;
+ }
+ return true;
+ }
+
+ private bool Target(int id, SafeCoreMirSource source)
+ {
+ Step();
+ if (id >= 0 && id < _function!.Blocks.Count) return true;
+ Error(SafeCoreMirDiagnosticCodes.InvalidControlFlow, "Branch target is outside the function's block arena.", source);
+ return false;
+ }
+
+ private void Terminator(SafeCoreMirTerminator? terminator)
+ {
+ Step();
+ if (terminator is null)
+ {
+ Error(SafeCoreMirDiagnosticCodes.InvalidControlFlow, "Every block requires an explicit terminator.", _block!.Source);
+ return;
+ }
+ Source(terminator.Source);
+ if (terminator.Operand is not null) Operand(terminator.Operand);
+ for (int index = 0; index < terminator.Arguments.Count; index++) Operand(terminator.Arguments[index]);
+ if (terminator.Kind != SafeCoreMirTerminatorKind.Call && (terminator.Arguments.Count != 0 || terminator.DestinationLocalId is not null))
+ Error(SafeCoreMirDiagnosticCodes.InvalidControlFlow, "Only call terminators may carry arguments or a destination.", terminator.Source);
+ if (terminator.Kind != SafeCoreMirTerminatorKind.Branch && terminator.FalseTargetBlockId != -1)
+ Error(SafeCoreMirDiagnosticCodes.InvalidControlFlow, "Only branch terminators may carry a false target.", terminator.Source);
+ switch (terminator.Kind)
+ {
+ case SafeCoreMirTerminatorKind.Return:
+ if (terminator.TargetBlockId != -1) Error(SafeCoreMirDiagnosticCodes.InvalidControlFlow, "Return cannot have a successor.", terminator.Source);
+ if (_function!.ReturnType.Kind == SafeCoreSemanticTypeKind.Never)
+ Error(SafeCoreMirDiagnosticCodes.TypeMismatch, "A diverging function cannot return.", terminator.Source);
+ else if (terminator.Operand is null)
+ {
+ if (_function.ReturnType.Kind != SafeCoreSemanticTypeKind.Unit)
+ Error(SafeCoreMirDiagnosticCodes.TypeMismatch, "A non-unit return requires a value.", terminator.Source);
+ }
+ else Equal(_function.ReturnType, terminator.Operand.Type, terminator.Source, "Return type differs from the function result.");
+ break;
+ case SafeCoreMirTerminatorKind.Goto:
+ if (terminator.Operand is not null) Error(SafeCoreMirDiagnosticCodes.InvalidControlFlow, "Goto cannot carry an operand.", terminator.Source);
+ Target(terminator.TargetBlockId, terminator.Source);
+ break;
+ case SafeCoreMirTerminatorKind.Branch:
+ if (terminator.Operand?.Type?.Kind != SafeCoreSemanticTypeKind.Bool)
+ Error(SafeCoreMirDiagnosticCodes.TypeMismatch, "A branch condition must be bool.", terminator.Source);
+ Target(terminator.TargetBlockId, terminator.Source);
+ Target(terminator.FalseTargetBlockId, terminator.Source);
+ break;
+ case SafeCoreMirTerminatorKind.Call:
+ Call(terminator);
+ break;
+ case SafeCoreMirTerminatorKind.Unreachable:
+ if (terminator.Operand is not null || terminator.TargetBlockId != -1)
+ Error(SafeCoreMirDiagnosticCodes.InvalidControlFlow, "Unreachable cannot carry operands or successors.", terminator.Source);
+ break;
+ default:
+ Error(SafeCoreMirDiagnosticCodes.InvalidControlFlow, "Unknown terminator kind.", terminator.Source);
+ break;
+ }
+ }
+
+ private void Call(SafeCoreMirTerminator terminator)
+ {
+ SafeCoreType? callee = terminator.Operand?.Type;
+ if (callee?.Kind != SafeCoreSemanticTypeKind.Function)
+ {
+ Error(SafeCoreMirDiagnosticCodes.TypeMismatch, "A call requires a typed function operand.", terminator.Source);
+ return;
+ }
+ if (callee.ParameterTypes.Count != terminator.Arguments.Count)
+ Error(SafeCoreMirDiagnosticCodes.TypeMismatch, "Call argument count differs from the function signature.", terminator.Source);
+ else
+ for (int index = 0; index < terminator.Arguments.Count; index++)
+ Equal(callee.ParameterTypes[index], terminator.Arguments[index].Type, terminator.Arguments[index].Source,
+ "Call argument type differs from the function parameter; coercions must be explicit.");
+ if (terminator.DestinationLocalId is int destination)
+ {
+ Equal(LocalType(destination, terminator.Source), callee.ReturnType, terminator.Source, "Call destination type differs from the function result.");
+ if (callee.ReturnType.Kind == SafeCoreSemanticTypeKind.Never)
+ Error(SafeCoreMirDiagnosticCodes.TypeMismatch, "A diverging call cannot initialize a destination.", terminator.Source);
+ }
+ else if (callee.ReturnType.Kind is not (SafeCoreSemanticTypeKind.Unit or SafeCoreSemanticTypeKind.Never))
+ Error(SafeCoreMirDiagnosticCodes.TypeMismatch, "A value-returning call requires a destination, including discarded results.", terminator.Source);
+ if (callee.ReturnType.Kind == SafeCoreSemanticTypeKind.Never)
+ {
+ if (terminator.TargetBlockId != -1 && Target(terminator.TargetBlockId, terminator.Source)
+ && _function!.Blocks[terminator.TargetBlockId].Terminator?.Kind != SafeCoreMirTerminatorKind.Unreachable)
+ Error(SafeCoreMirDiagnosticCodes.InvalidControlFlow, "A diverging call cannot continue to executable control flow.", terminator.Source);
+ }
+ else Target(terminator.TargetBlockId, terminator.Source);
+ }
+
+ private void Reachability()
+ {
+ SafeCoreMirFunction function = _function!;
+ var visited = new bool[function.Blocks.Count];
+ var pending = new Queue();
+ if (function.EntryBlockId >= 0 && function.EntryBlockId < visited.Length) pending.Enqueue(function.EntryBlockId);
+ for (int iterations = 0; pending.Count > 0 && iterations <= function.Blocks.Count * 2; iterations++)
+ {
+ Step();
+ int id = pending.Dequeue();
+ if (visited[id]) continue;
+ visited[id] = true;
+ SafeCoreMirTerminator? terminator = function.Blocks[id].Terminator;
+ if (terminator?.Kind is SafeCoreMirTerminatorKind.Goto or SafeCoreMirTerminatorKind.Branch
+ || terminator?.Kind == SafeCoreMirTerminatorKind.Call && terminator.Operand?.Type?.Kind == SafeCoreSemanticTypeKind.Function
+ && terminator.Operand.Type.ReturnType.Kind != SafeCoreSemanticTypeKind.Never)
+ {
+ Enqueue(terminator.TargetBlockId);
+ if (terminator.Kind == SafeCoreMirTerminatorKind.Branch) Enqueue(terminator.FalseTargetBlockId);
+ }
+ }
+ var reachable = new List();
+ for (int index = 0; index < visited.Length; index++)
+ {
+ Step();
+ if (visited[index]) reachable.Add(index);
+ }
+ _reachable[function.Id] = reachable.AsReadOnly();
+ void Enqueue(int id)
+ {
+ if (id >= 0 && id < visited.Length && !visited[id]) pending.Enqueue(id);
+ }
+ }
+ }
+}
diff --git a/tests/RustSharp.Tests/Program.cs b/tests/RustSharp.Tests/Program.cs
index f23906e..81bc1da 100644
--- a/tests/RustSharp.Tests/Program.cs
+++ b/tests/RustSharp.Tests/Program.cs
@@ -15,6 +15,7 @@ public static async Task Main(string[] args)
[.. SyntaxTests.All, .. LexerTests.All, .. LexerClosureTests.All, .. LexingManifestTests.All, .. SafeCoreSyntaxTests.All, .. SafeCoreTypeHirTests.All, .. SafeCoreTypeInferenceTests.All, .. SafeCoreTypeProfileTests.All, .. SafeCoreTypeAnalysisTests.All, .. SafeCoreTypeConformanceTests.All, .. SyntaxGrammarTests.All, .. SyntaxModuleExpansionTests.All, .. SyntaxItemExpansionTests.All, .. SyntaxExpressionExpansionTests.All, .. SyntaxProfileBoundaryTests.All, .. SemanticAstBoundaryTests.All, .. SyntaxManifestTests.All, .. NameResolutionManifestTests.All, .. SafeCoreNameResolutionTests.All, .. SafeCoreModuleResolutionTests.All, .. SafeCoreHirTests.All, .. SafeCoreCompilationTests.All, .. SafeCoreWorkspaceTests.All, .. CargoWorkspaceTests.All, .. SafeCoreModuleCompilationTests.All, .. WorkspaceSourceMapTests.All, .. EmissionTests.All, .. NativeAotTests.All, .. BoundedProcessTests.All, .. ClrLirTests.All, .. VerticalProofTests.All, .. OwnershipTests.All];
tests = [.. tests, .. SafeCoreAdvancedTypeHirTests.All, .. SafeCorePatternClosureTests.All, .. SafeCoreConstantTests.All];
tests = [.. tests, .. GenericFoundationTests.All];
+ tests = [.. tests, .. SafeCoreMirValidationTests.All, .. SafeCoreMirLoweringTests.All];
if (tests.Count > MaximumTestCount)
{
Console.Error.WriteLine($"Test count {tests.Count} exceeds the safety limit {MaximumTestCount}.");
diff --git a/tests/RustSharp.Tests/SafeCoreMirLoweringTests.cs b/tests/RustSharp.Tests/SafeCoreMirLoweringTests.cs
new file mode 100644
index 0000000..55303fe
--- /dev/null
+++ b/tests/RustSharp.Tests/SafeCoreMirLoweringTests.cs
@@ -0,0 +1,268 @@
+using System.Diagnostics;
+using System.Globalization;
+using RustSharp.Semantics;
+using RustSharp.Syntax;
+
+namespace RustSharp.Tests;
+
+internal static class SafeCoreMirLoweringTests
+{
+ public static IReadOnlyList All { get; } =
+ [
+ new("MIR lowering produces deterministic typed three-address snapshots", SnapshotAsync),
+ new("MIR lowering preserves scalar literal spelling and original HIR evidence", LiteralsAsync),
+ new("MIR lowering preserves branches loops break continue and direct calls", ControlFlowAsync),
+ new("MIR lowering snapshots reads before later side effects", EvaluationOrderAsync),
+ new("MIR lowering short circuits and drops unreachable tails", DivergenceAsync),
+ new("MIR lowering rejects unsupported constructs at their original spans", UnsupportedAsync),
+ new("MIR lowering bounds work size nesting time and cancellation", LimitsAsync),
+ ];
+
+ private static Task SnapshotAsync()
+ {
+ using var cancellation = new CancellationTokenSource(TimeSpan.FromSeconds(20));
+ SafeCoreTypeAnalysisProgram typed = Check("fn f() -> i32 { 1 + 2 }", cancellation.Token);
+ SafeCoreMirProgram first = Lower(typed, cancellation.Token);
+ SafeCoreMirProgram second = Lower(typed, cancellation.Token);
+ AssertEx.Equal(SafeCoreMirFormatting.Format(first), SafeCoreMirFormatting.Format(second));
+ SafeCoreMirFunction function = first.Functions.Single();
+ AssertEx.Equal("crate::f#value", function.Name);
+ AssertEx.Equal(1, function.Blocks.Count);
+ AssertEx.Equal(1, function.Locals.Count);
+ AssertEx.Equal("tmp0", function.Locals[0].Name);
+ AssertEx.Equal("i32", function.Locals[0].Type.ToString());
+ SafeCoreMirStatement statement = function.Blocks[0].Statements.Single();
+ AssertEx.Equal(SafeCoreMirRvalueKind.Binary, statement.Value.Kind);
+ AssertEx.Equal("+", statement.Value.Operator!);
+ AssertEx.Equal("1,2", string.Join(',', statement.Value.Operands.Select(o => o.Value)));
+ AssertEx.Equal(SafeCoreMirTerminatorKind.Return, function.Blocks[0].Terminator.Kind);
+ AssertEx.Equal(statement.DestinationLocalId, function.Blocks[0].Terminator.Operand!.Id);
+ return Task.CompletedTask;
+ }
+
+ private static Task LiteralsAsync()
+ {
+ using var cancellation = new CancellationTokenSource(TimeSpan.FromSeconds(20));
+ const string source = "fn a() -> i8 { -((128i8)) } fn b() -> i128 { -170141183460469231731687303715884105728i128 } " +
+ "fn c() -> u16 { 0xff_u16 } fn d() -> u16 { 0o17u16 } fn e() -> u16 { 0b1010u16 } " +
+ "fn f() -> f32 { 0.1f32 } fn g() -> char { '\\u{1_f980}' } fn h() -> u8 { b'\\xFF' }";
+ SafeCoreTypeAnalysisProgram typed = Check(source, cancellation.Token);
+ SafeCoreMirProgram mir = Lower(typed, cancellation.Token);
+ AssertEx.Equal("-128,-170141183460469231731687303715884105728,255,15,10,0.1,129408,255",
+ string.Join(',', mir.Functions.Select(f => f.Blocks[0].Terminator.Operand!.Value)));
+ var clock = Stopwatch.StartNew();
+ AssertEx.True(mir.Functions.Count <= 10, "The source-evidence audit is capped at ten functions.");
+ foreach (SafeCoreMirFunction function in mir.Functions)
+ {
+ cancellation.Token.ThrowIfCancellationRequested();
+ AssertEx.True(clock.Elapsed < TimeSpan.FromSeconds(10), "Source audit timed out.");
+ SafeCoreMirSource original = function.Blocks[0].Terminator.Operand!.Source;
+ AssertEx.Equal("mir-lowering.rs", original.SourcePath);
+ AssertEx.Equal(typed.Hir.GetNode(original.HirNodeId).Span, original.Span);
+ AssertEx.True(original.Span.End <= original.SourceLength && original.SourceLength <= source.Length,
+ "MIR source provenance must stay inside the HIR document extent.");
+ }
+ return Task.CompletedTask;
+ }
+
+ private static Task ControlFlowAsync()
+ {
+ Run("fn add(a: i32, b: i32) -> i32 { a + b } fn f() -> i32 { let mut x = 0; " +
+ "while x < 5 { x += 1; if x == 2 { continue; } if x == 4 { break; } } add(x, 3) }", 7L);
+ Run("fn f() -> i32 { let mut x = 0; loop { x += 1; if x == 3 { break x + 4; } } }", 7L);
+ Run("fn f() -> i32 { loop { let inner = loop { break 9; }; break inner; } }", 9L);
+ Run("fn f() -> i32 { while { return 6; true } {} 7 }", 6L);
+ Run("fn f() -> i32 { let x = if true { return 3; } else { 4 }; x }", 3L);
+ Run("mod m { pub fn add(x: i32) -> i32 { x + 2 } } use m::add as plus; fn f() -> i32 { plus(5) }", 7L);
+ return Task.CompletedTask;
+ }
+
+ private static Task EvaluationOrderAsync()
+ {
+ Run("fn f() -> i32 { let mut x = 1; x + { x = 2; x } }", 3L);
+ Run("fn pair(a: i32, b: i32) -> i32 { a * 10 + b } fn f() -> i32 { let mut x = 1; pair(x, { x = 2; x }) }", 12L);
+ Run("fn f() -> i32 { let mut x = 1; x += { x = 2; 3 }; x }", 5L);
+ Run("fn f() -> i32 { let mut x = 1; { let x = 9; x; } x }", 1L);
+ return Task.CompletedTask;
+ }
+
+ private static Task DivergenceAsync()
+ {
+ Run("fn f() -> i32 { let mut x = 0; false && { x = 1; true }; true || { x = 2; false }; x }", 0L);
+ Run("fn f() -> i32 { let mut x = 0; true && { x = 1; true }; false || { x = 2; false }; x }", 2L);
+ Run("fn f() -> i32 { false && { return 9; }; 1 }", 1L);
+ Run("fn f() -> i32 { loop { let x = { break 5; }; x; } }", 5L);
+ using var cancellation = new CancellationTokenSource(TimeSpan.FromSeconds(20));
+ SafeCoreMirProgram mir = Lower(Check("fn unused() -> i32 { 2 } fn f() -> i32 { return 1; unused() }", cancellation.Token), cancellation.Token);
+ SafeCoreMirFunction f = mir.Functions.Single(f => f.Name == "crate::f#value");
+ AssertEx.Equal(1, f.Blocks.Count);
+ AssertEx.Equal(0, f.Blocks[0].Statements.Count);
+ AssertEx.Equal("1", f.Blocks[0].Terminator.Operand!.Value!);
+ SafeCoreMirProgram never = Lower(Check("fn halt() -> ! { loop {} } fn f(flag: bool) -> i32 { if flag { halt() } else { 4 } }", cancellation.Token), cancellation.Token);
+ AssertEx.True(never.Functions[1].Blocks.Any(b => b.Terminator.Kind == SafeCoreMirTerminatorKind.Call), "A never-returning call must remain an explicit call terminator.");
+ AssertEx.True(never.Functions[1].Blocks.Any(b => b.Terminator.Kind == SafeCoreMirTerminatorKind.Unreachable), "The never continuation must terminate explicitly.");
+ return Task.CompletedTask;
+ }
+
+ private static Task UnsupportedAsync()
+ {
+ (string Source, string Span)[] cases =
+ [
+ ("fn f() { let x = [1, 2]; }", "[1, 2]"),
+ ("fn f() { let x = || 1; }", "|| 1"),
+ ("fn f() -> i32 { match true { true => 1, false => 2 } }", "match true { true => 1, false => 2 }"),
+ ("fn f() { let x = &1; }", "&1"),
+ ("fn f() { let x = (1, 2); }", "(1, 2)"),
+ ("const X: i32 = 1; fn f() -> i32 { X }", "const X: i32 = 1;"),
+ ("fn id() {} fn f() { let p = id; p(); }", "id"),
+ ];
+ using var cancellation = new CancellationTokenSource(TimeSpan.FromSeconds(20));
+ for (int index = 0; index < cases.Length; index++)
+ {
+ cancellation.Token.ThrowIfCancellationRequested();
+ var item = cases[index];
+ SafeCoreMirLoweringResult result = SafeCoreMirLowering.Lower(Check(item.Source, cancellation.Token), cancellationToken: cancellation.Token);
+ AssertEx.False(result.IsSuccessful, item.Source);
+ AssertEx.True(result.Program is null, "Rejected lowering must never expose a partial program.");
+ Diagnostic diagnostic = result.Diagnostics.Single();
+ AssertEx.Equal(SafeCoreMirLowering.UnsupportedSyntax, diagnostic.Code);
+ AssertEx.Equal("mir-lowering.rs", diagnostic.SourcePath!);
+ AssertEx.Equal(item.Span, item.Source.Substring(diagnostic.Span.Start, diagnostic.Span.Length));
+ }
+ return Task.CompletedTask;
+ }
+
+ private static Task LimitsAsync()
+ {
+ using var cancellation = new CancellationTokenSource(TimeSpan.FromSeconds(20));
+ SafeCoreTypeAnalysisProgram typed = Check("fn f(flag: bool) -> i32 { if flag { 1 + 2 } else { 3 } }", cancellation.Token);
+ SafeCoreMirLoweringOptions[] limits =
+ [
+ new() { MaximumOperations = 1 }, new() { MaximumNestingDepth = 1 },
+ new() { MaximumBlocksPerFunction = 1 }, new() { MaximumLocalsPerFunction = 1 },
+ new() { Timeout = TimeSpan.FromTicks(1) },
+ ];
+ for (int index = 0; index < limits.Length; index++)
+ {
+ SafeCoreMirLoweringResult result = SafeCoreMirLowering.Lower(typed, limits[index], cancellation.Token);
+ AssertEx.True(result.IsTruncated && result.Program is null, "Each configured bound must reject without a partial program.");
+ AssertEx.Equal(SafeCoreMirLowering.LimitReached, result.Diagnostics.Single().Code);
+ }
+ var missing = typed with { Types = new Dictionary() };
+ AssertEx.Equal(SafeCoreMirLowering.InvalidEvidence,
+ SafeCoreMirLowering.Lower(missing, cancellationToken: cancellation.Token).Diagnostics.Single().Code);
+ using var cancelled = new CancellationTokenSource();
+ cancelled.Cancel();
+ AssertEx.Throws(() => SafeCoreMirLowering.Lower(typed, cancellationToken: cancelled.Token));
+ AssertEx.Throws(() => SafeCoreMirLowering.Lower(typed, new() { Timeout = TimeSpan.Zero }));
+ return Task.CompletedTask;
+ }
+
+ private static SafeCoreTypeAnalysisProgram Check(string source, CancellationToken cancellation)
+ {
+ SafeCoreSyntaxResult syntax = SafeCoreSyntax.Parse(source, "mir-lowering.rs", new() { Timeout = TimeSpan.FromSeconds(5) }, cancellation);
+ AssertEx.True(syntax.IsSuccessful, $"Syntax: {source}\n{Format(syntax.Diagnostics)}");
+ SafeCoreHirResult hir = SafeCoreHirLowering.Lower(syntax, new()
+ {
+ Timeout = TimeSpan.FromSeconds(5), CancellationToken = cancellation,
+ NameResolution = new() { EnableTypeSystemExtensions = true, Timeout = TimeSpan.FromSeconds(5) },
+ });
+ AssertEx.True(hir.IsSuccessful, $"HIR: {source}\n{Format(hir.Diagnostics)}");
+ SafeCoreTypeAnalysisResult typed = SafeCoreTypeAnalysis.Check(hir, new() { Timeout = TimeSpan.FromSeconds(5) }, cancellation);
+ AssertEx.True(typed.IsSuccessful, $"{source}\n{Format(typed.Diagnostics)}");
+ return typed.Program!;
+ }
+
+ private static SafeCoreMirProgram Lower(SafeCoreTypeAnalysisProgram typed, CancellationToken cancellation)
+ {
+ SafeCoreMirLoweringResult result = SafeCoreMirLowering.Lower(typed, new() { Timeout = TimeSpan.FromSeconds(5) }, cancellation);
+ AssertEx.True(result.IsSuccessful, Format(result.Diagnostics));
+ AssertEx.True(result.Validation is { IsSuccessful: true }, "Every successful lowering must contain explicit validator evidence.");
+ return result.Program!;
+ }
+
+ private static string Format(IReadOnlyList diagnostics) => string.Join("; ", diagnostics.Select(d => $"{d.Code}: {d.Message}"));
+
+ private static void Run(string source, long expected)
+ {
+ using var cancellation = new CancellationTokenSource(TimeSpan.FromSeconds(20));
+ SafeCoreMirProgram mir = Lower(Check(source, cancellation.Token), cancellation.Token);
+ var interpreter = new ScalarInterpreter(mir, cancellation.Token);
+ AssertEx.Equal(expected, (long)interpreter.Invoke(mir.Functions.Single(f => f.Name == "crate::f#value").Id, [], 0)!, source);
+ }
+
+ // Test-only executable semantics checks evaluation and branch behavior independently
+ // of how many temporary slots or empty join blocks the lowerer chooses to emit.
+ private sealed class ScalarInterpreter(SafeCoreMirProgram program, CancellationToken cancellation)
+ {
+ private readonly Stopwatch _clock = Stopwatch.StartNew();
+ private int _steps;
+
+ public object? Invoke(int functionId, object?[] arguments, int depth)
+ {
+ AssertEx.True(depth <= 32, "MIR test call nesting exceeded 32.");
+ SafeCoreMirFunction function = program.Functions[functionId];
+ var locals = new object?[function.Locals.Count];
+ for (int index = 0; index < arguments.Length; index++) { Step(); locals[index] = arguments[index]; }
+ int blockId = function.EntryBlockId;
+ for (int iteration = 0; iteration < 4_096; iteration++)
+ {
+ Step();
+ SafeCoreMirBlock block = function.Blocks[blockId];
+ foreach (SafeCoreMirStatement statement in block.Statements)
+ {
+ Step();
+ IReadOnlyList operands = statement.Value.Operands;
+ object? first = Read(operands[0], locals);
+ object? value = statement.Value.Kind switch
+ {
+ SafeCoreMirRvalueKind.Use or SafeCoreMirRvalueKind.Coerce => first,
+ SafeCoreMirRvalueKind.Binary => Binary(statement.Value.Operator!, first!, Read(operands[1], locals)!),
+ SafeCoreMirRvalueKind.Unary => statement.Value.Operator == "!" ? !(bool)first! : -(long)first!,
+ _ => throw new InvalidOperationException("Unexpected rvalue in bounded scalar test interpreter."),
+ };
+ locals[statement.DestinationLocalId] = value;
+ }
+ SafeCoreMirTerminator terminator = block.Terminator;
+ switch (terminator.Kind)
+ {
+ case SafeCoreMirTerminatorKind.Return: return terminator.Operand is null ? null : Read(terminator.Operand, locals);
+ case SafeCoreMirTerminatorKind.Goto: blockId = terminator.TargetBlockId; break;
+ case SafeCoreMirTerminatorKind.Branch:
+ blockId = (bool)Read(terminator.Operand!, locals)! ? terminator.TargetBlockId : terminator.FalseTargetBlockId; break;
+ case SafeCoreMirTerminatorKind.Call:
+ object? result = Invoke(terminator.Operand!.Id, terminator.Arguments.Select(a => Read(a, locals)).ToArray(), depth + 1);
+ if (terminator.DestinationLocalId is int local) locals[local] = result;
+ blockId = terminator.TargetBlockId; break;
+ default: throw new InvalidOperationException("Test unexpectedly reached unreachable MIR.");
+ }
+ }
+ throw new InvalidOperationException("MIR test exceeded 4096 CFG steps.");
+ }
+
+ private static object? Read(SafeCoreMirOperand operand, object?[] locals) => operand.Kind == SafeCoreMirOperandKind.Local
+ ? locals[operand.Id] ?? throw new InvalidOperationException("Test read an uninitialized MIR slot.")
+ : operand.Type.Kind switch
+ {
+ SafeCoreSemanticTypeKind.Unit => null,
+ SafeCoreSemanticTypeKind.Bool => bool.Parse(operand.Value!),
+ _ => long.Parse(operand.Value!, CultureInfo.InvariantCulture),
+ };
+
+ private static object Binary(string op, object left, object right) => op switch
+ {
+ "+" => (long)left + (long)right, "-" => (long)left - (long)right,
+ "*" => (long)left * (long)right, "/" => (long)left / (long)right,
+ "==" => left.Equals(right), "!=" => !left.Equals(right),
+ "<" => (long)left < (long)right, ">" => (long)left > (long)right,
+ "<=" => (long)left <= (long)right, ">=" => (long)left >= (long)right,
+ _ => throw new InvalidOperationException("Unexpected binary operator in MIR test."),
+ };
+
+ private void Step()
+ {
+ cancellation.ThrowIfCancellationRequested();
+ AssertEx.True(++_steps <= 4_096 && _clock.Elapsed < TimeSpan.FromSeconds(5), "Bounded MIR interpreter exceeded its work or time budget.");
+ }
+ }
+}
diff --git a/tests/RustSharp.Tests/SafeCoreMirValidationTests.cs b/tests/RustSharp.Tests/SafeCoreMirValidationTests.cs
new file mode 100644
index 0000000..0a8cae7
--- /dev/null
+++ b/tests/RustSharp.Tests/SafeCoreMirValidationTests.cs
@@ -0,0 +1,242 @@
+using System.Collections;
+using System.Globalization;
+using RustSharp.Semantics;
+using RustSharp.Syntax;
+
+namespace RustSharp.Tests;
+
+internal static class SafeCoreMirValidationTests
+{
+ public static IReadOnlyList All { get; } =
+ [
+ new("typed MIR preserves frozen collection ownership", FrozenInputsAsync),
+ new("typed MIR accepts cyclic CFG and reports deterministic reachability", CyclicFlowAsync),
+ new("typed MIR rejects negative and duplicate arena IDs", InvalidIdsAsync),
+ new("typed MIR validates dead blocks and explicit terminator shapes", DeadBlocksAsync),
+ new("typed MIR validates source evidence without integer overflow", SourceEvidenceAsync),
+ new("typed MIR enforces assignments branches and return types", ValueTypesAsync),
+ new("typed MIR checks scalar constant ranges and Unicode scalars", ConstantsAsync),
+ new("typed MIR checks nominal call signatures arguments and results", CallsAsync),
+ new("typed MIR keeps diverging calls terminal", DivergingCallsAsync),
+ new("typed MIR validates explicit coercions casts and tuple construction", ComputationsAsync),
+ new("typed MIR validation obeys cancellation work size diagnostic depth and time budgets", ValidationBudgetsAsync),
+ new("typed MIR formatter is invariant deterministic and bounded", FormattingAsync),
+ ];
+
+ private static readonly SafeCoreType Integer = SafeCoreType.Primitive(SafeCoreSemanticTypeKind.I32);
+ private static readonly SafeCoreType Boolean = SafeCoreType.Primitive(SafeCoreSemanticTypeKind.Bool);
+ private static readonly SafeCoreType Unit = SafeCoreType.Primitive(SafeCoreSemanticTypeKind.Unit);
+ private static readonly SafeCoreType Never = SafeCoreType.Primitive(SafeCoreSemanticTypeKind.Never);
+ private static readonly SafeCoreMirSource Source = new("sample.rs", new TextSpan(0, 12), 0, 12);
+
+ private static SafeCoreMirOperand Number(string value = "1") => SafeCoreMirOperand.Constant(Integer, value, Source);
+ private static SafeCoreMirBlock ReturnBlock(int id = 0) => new(id, [], SafeCoreMirTerminator.Return(Number(), Source), Source);
+ private static SafeCoreMirFunction Function(IReadOnlyList blocks,
+ IReadOnlyList? locals = null, SafeCoreType? result = null, int entry = 0) =>
+ new(0, "crate::main", result ?? Integer, locals ?? [], blocks, entry, Source);
+ private static SafeCoreMirProgram Program(params SafeCoreMirBlock[] blocks) => new([Function(blocks)]);
+ private static void Invalid(SafeCoreMirProgram program, string code)
+ {
+ SafeCoreMirValidationResult validation = SafeCoreMirValidation.Validate(program);
+ AssertEx.False(validation.IsSuccessful, "Malformed MIR must not pass validation.");
+ AssertEx.True(validation.Diagnostics.Any(diagnostic => diagnostic.Code == code), $"Expected MIR diagnostic {code}.");
+ }
+
+ private static Task FrozenInputsAsync()
+ {
+ SafeCoreMirBlock[] blocks = [ReturnBlock()];
+ var function = Function(blocks);
+ blocks[0] = new(7, [], SafeCoreMirTerminator.Goto(7, Source), Source);
+ SafeCoreMirFunction[] functions = [function];
+ var program = new SafeCoreMirProgram(functions);
+ functions[0] = Function(blocks);
+ AssertEx.True(SafeCoreMirValidation.Validate(program).IsSuccessful, "Caller mutations cannot change a MIR snapshot.");
+ var indexed = new IndexOnlyList(function);
+ AssertEx.Equal(1, new SafeCoreMirProgram(indexed).Functions.Count);
+ AssertEx.Throws(() => _ = new SafeCoreMirProgram(new OversizedList()));
+ using var cancelled = new CancellationTokenSource();
+ cancelled.Cancel();
+ AssertEx.Throws(() => _ = new SafeCoreMirProgram(indexed, cancelled.Token));
+ return Task.CompletedTask;
+ }
+
+ private static Task CyclicFlowAsync()
+ {
+ SafeCoreMirProgram program = Program(
+ new(0, [], SafeCoreMirTerminator.Branch(SafeCoreMirOperand.Constant(Boolean, "true", Source), 1, 2, Source), Source),
+ new(1, [], SafeCoreMirTerminator.Goto(0, Source), Source), ReturnBlock(2), ReturnBlock(3));
+ SafeCoreMirValidationResult result = SafeCoreMirValidation.Validate(program);
+ AssertEx.True(result.IsSuccessful, "CFG back edges are valid.");
+ AssertEx.Equal("0,1,2", string.Join(',', result.ReachableBlocks[0]));
+ return Task.CompletedTask;
+ }
+
+ private static Task InvalidIdsAsync()
+ {
+ Invalid(Program(new SafeCoreMirBlock(0, [], SafeCoreMirTerminator.Goto(-2, Source), Source)), SafeCoreMirDiagnosticCodes.InvalidControlFlow);
+ Invalid(Program(ReturnBlock(1)), SafeCoreMirDiagnosticCodes.InvalidControlFlow);
+ Invalid(new([Function([ReturnBlock()], entry: -1)]), SafeCoreMirDiagnosticCodes.InvalidControlFlow);
+ Invalid(Program(new SafeCoreMirBlock(0, [], SafeCoreMirTerminator.Return(SafeCoreMirOperand.Local(-1, Integer, Source), Source), Source)),
+ SafeCoreMirDiagnosticCodes.InvalidOperand);
+ Invalid(new([Function([ReturnBlock()], [new(-1, "x", Integer, SafeCoreMirLocalKind.Parameter, false, Source)])]),
+ SafeCoreMirDiagnosticCodes.InvalidInput);
+ SafeCoreMirFunction duplicate = Function([ReturnBlock()]);
+ Invalid(new([duplicate, duplicate]), SafeCoreMirDiagnosticCodes.InvalidInput);
+ return Task.CompletedTask;
+ }
+
+ private static Task DeadBlocksAsync()
+ {
+ Invalid(Program(ReturnBlock(), new(1, [], SafeCoreMirTerminator.Goto(99, Source), Source)),
+ SafeCoreMirDiagnosticCodes.InvalidControlFlow);
+ Invalid(Program(new SafeCoreMirBlock(0, [], null!, Source)), SafeCoreMirDiagnosticCodes.InvalidControlFlow);
+ Invalid(Program(new SafeCoreMirBlock(0, [], new(SafeCoreMirTerminatorKind.Return, Number(), [], null, 0, -1, Source), Source)),
+ SafeCoreMirDiagnosticCodes.InvalidControlFlow);
+ return Task.CompletedTask;
+ }
+
+ private static Task SourceEvidenceAsync()
+ {
+ var overflow = new SafeCoreMirSource("bad.rs", new(int.MaxValue, int.MaxValue), 0, int.MaxValue);
+ Invalid(Program(new SafeCoreMirBlock(0, [], SafeCoreMirTerminator.Return(Number(), overflow), Source)), SafeCoreMirDiagnosticCodes.InvalidSource);
+ var negative = Source with { HirNodeId = -1 };
+ Invalid(Program(new SafeCoreMirBlock(0, [], SafeCoreMirTerminator.Return(Number(), negative), Source)), SafeCoreMirDiagnosticCodes.InvalidSource);
+ Invalid(Program(new SafeCoreMirBlock(0, [], SafeCoreMirTerminator.Return(Number(), Source with { SourcePath = "" }), Source)),
+ SafeCoreMirDiagnosticCodes.InvalidSource);
+ return Task.CompletedTask;
+ }
+
+ private static Task ValueTypesAsync()
+ {
+ Invalid(Program(new SafeCoreMirBlock(0, [], SafeCoreMirTerminator.Branch(Number(), 0, 0, Source), Source)), SafeCoreMirDiagnosticCodes.TypeMismatch);
+ Invalid(Program(new SafeCoreMirBlock(0, [], SafeCoreMirTerminator.Return(null, Source), Source)), SafeCoreMirDiagnosticCodes.TypeMismatch);
+ Invalid(new([Function([new(0, [], SafeCoreMirTerminator.Return(null, Source), Source)], result: Never)]), SafeCoreMirDiagnosticCodes.TypeMismatch);
+ SafeCoreMirStatement statement = new(0, SafeCoreMirRvalue.Use(Number(), Source), Source);
+ Invalid(new([Function([new(0, [statement], SafeCoreMirTerminator.Return(Number(), Source), Source)],
+ [new(0, "x", Boolean, SafeCoreMirLocalKind.User, false, Source)])]), SafeCoreMirDiagnosticCodes.TypeMismatch);
+ SafeCoreType unresolved = new SafeCoreTypeInference().Fresh();
+ Invalid(new([Function([ReturnBlock()], [new(0, "x", unresolved, SafeCoreMirLocalKind.Parameter, false, Source)])]), SafeCoreMirDiagnosticCodes.TypeMismatch);
+ SafeCoreMirOperand invalidOperand = new(SafeCoreMirOperandKind.Constant, null!, -1, "1", Source);
+ Invalid(Computation(SafeCoreMirRvalue.Unary("-", invalidOperand, Integer, Source)), SafeCoreMirDiagnosticCodes.TypeMismatch);
+ Invalid(Program(new SafeCoreMirBlock(0, [], SafeCoreMirTerminator.Branch(invalidOperand, 0, 0, Source), Source)), SafeCoreMirDiagnosticCodes.TypeMismatch);
+ Invalid(new([new(0, "crate::invalid", null!, [], [ReturnBlock()], 0, Source)]), SafeCoreMirDiagnosticCodes.TypeMismatch);
+ return Task.CompletedTask;
+ }
+
+ private static Task ConstantsAsync()
+ {
+ Invalid(Program(new SafeCoreMirBlock(0, [], SafeCoreMirTerminator.Return(Number("2147483648"), Source), Source)), SafeCoreMirDiagnosticCodes.InvalidOperand);
+ Invalid(Program(new SafeCoreMirBlock(0, [], SafeCoreMirTerminator.Return(Number("1i32"), Source), Source)), SafeCoreMirDiagnosticCodes.InvalidOperand);
+ SafeCoreType character = SafeCoreType.Primitive(SafeCoreSemanticTypeKind.Char);
+ var surrogate = SafeCoreMirOperand.Constant(character, "55296", Source);
+ Invalid(new([Function([new(0, [], SafeCoreMirTerminator.Return(surrogate, Source), Source)], result: character)]), SafeCoreMirDiagnosticCodes.InvalidOperand);
+ AssertEx.True(SafeCoreMirValidation.Validate(Program(new SafeCoreMirBlock(0, [], SafeCoreMirTerminator.Return(Number("-2147483648"), Source), Source))).IsSuccessful,
+ "Signed minimum constant must be representable.");
+ return Task.CompletedTask;
+ }
+
+ private static Task CallsAsync()
+ {
+ SafeCoreMirFunction callee = new(1, "crate::callee", Integer,
+ [new(0, "arg", Integer, SafeCoreMirLocalKind.Parameter, false, Source)],
+ [new(0, [], SafeCoreMirTerminator.Return(SafeCoreMirOperand.Local(0, Integer, Source), Source), Source)], 0, Source);
+ SafeCoreMirOperand target = SafeCoreMirOperand.Function(1, SafeCoreType.Function([Integer], Integer, "crate::callee"), Source);
+ SafeCoreMirLocal[] locals = [new(0, "result", Integer, SafeCoreMirLocalKind.Temporary, false, Source)];
+ SafeCoreMirFunction caller = Function([
+ new(0, [], SafeCoreMirTerminator.Call(target, [Number()], 0, 1, Source), Source),
+ new(1, [], SafeCoreMirTerminator.Return(SafeCoreMirOperand.Local(0, Integer, Source), Source), Source)], locals);
+ AssertEx.True(SafeCoreMirValidation.Validate(new([caller, callee])).IsSuccessful, "Typed calls should pass.");
+ Invalid(new([Function([new(0, [], SafeCoreMirTerminator.Call(target, [], 0, 0, Source), Source)], locals), callee]), SafeCoreMirDiagnosticCodes.TypeMismatch);
+ Invalid(new([Function([new(0, [], SafeCoreMirTerminator.Call(target, [Number()], null, 0, Source), Source)], locals), callee]), SafeCoreMirDiagnosticCodes.TypeMismatch);
+ SafeCoreMirOperand wrongNominal = target with { Type = SafeCoreType.Function([Integer], Integer, "crate::other") };
+ Invalid(new([Function([new(0, [], SafeCoreMirTerminator.Call(wrongNominal, [Number()], 0, 0, Source), Source)], locals), callee]), SafeCoreMirDiagnosticCodes.TypeMismatch);
+ SafeCoreMirOperand negative = target with { Id = -1 };
+ Invalid(new([Function([new(0, [], SafeCoreMirTerminator.Call(negative, [Number()], 0, 0, Source), Source)], locals), callee]), SafeCoreMirDiagnosticCodes.InvalidOperand);
+ return Task.CompletedTask;
+ }
+
+ private static Task DivergingCallsAsync()
+ {
+ SafeCoreMirFunction diverge = new(1, "crate::diverge", Never, [], [new(0, [], SafeCoreMirTerminator.Goto(0, Source), Source)], 0, Source);
+ SafeCoreMirOperand target = SafeCoreMirOperand.Function(1, SafeCoreType.Function([], Never, "crate::diverge"), Source);
+ SafeCoreMirFunction caller = Function([new(0, [], SafeCoreMirTerminator.Call(target, [], null, -1, Source), Source)]);
+ AssertEx.True(SafeCoreMirValidation.Validate(new([caller, diverge])).IsSuccessful, "A diverging callee requires no return path.");
+ Invalid(new([Function([new(0, [], SafeCoreMirTerminator.Call(target, [], null, 1, Source), Source), ReturnBlock(1)]), diverge]),
+ SafeCoreMirDiagnosticCodes.InvalidControlFlow);
+ return Task.CompletedTask;
+ }
+
+ private static Task ComputationsAsync()
+ {
+ SafeCoreType wider = SafeCoreType.Primitive(SafeCoreSemanticTypeKind.I64);
+ SafeCoreMirRvalue invalid = SafeCoreMirRvalue.Coerce(Number(), wider, Source);
+ Invalid(Computation(invalid), SafeCoreMirDiagnosticCodes.TypeMismatch);
+ AssertEx.True(SafeCoreMirValidation.Validate(Computation(SafeCoreMirRvalue.Cast(Number(), wider, Source))).IsSuccessful,
+ "Explicit numeric casts are distinct from implicit coercions.");
+ SafeCoreType tuple = SafeCoreType.Tuple([Integer, Boolean]);
+ AssertEx.True(SafeCoreMirValidation.Validate(Computation(SafeCoreMirRvalue.Tuple(
+ [Number(), SafeCoreMirOperand.Constant(Boolean, "false", Source)], tuple, Source))).IsSuccessful, "Tuple members retain their types.");
+ Invalid(Computation(SafeCoreMirRvalue.Binary("&&", SafeCoreMirOperand.Constant(Boolean, "true", Source),
+ SafeCoreMirOperand.Constant(Boolean, "false", Source), Boolean, Source)), SafeCoreMirDiagnosticCodes.TypeMismatch);
+ return Task.CompletedTask;
+ }
+
+ private static SafeCoreMirProgram Computation(SafeCoreMirRvalue value) => new([Function([
+ new(0, [new(0, value, Source)], SafeCoreMirTerminator.Return(SafeCoreMirOperand.Local(0, value.Type, Source), Source), Source)],
+ [new(0, "result", value.Type, SafeCoreMirLocalKind.Temporary, false, Source)], value.Type)]);
+
+ private static Task ValidationBudgetsAsync()
+ {
+ SafeCoreMirProgram program = Program(ReturnBlock());
+ using var cancellation = new CancellationTokenSource();
+ cancellation.Cancel();
+ AssertEx.Throws(() => SafeCoreMirValidation.Validate(program, new() { CancellationToken = cancellation.Token }));
+ AssertEx.True(SafeCoreMirValidation.Validate(program, new() { MaximumOperations = 1 }).IsTruncated, "Operation limits are explicit.");
+ AssertEx.True(SafeCoreMirValidation.Validate(program, new() { Timeout = TimeSpan.FromTicks(1) }).IsTruncated, "Wall time must be checked.");
+ AssertEx.True(SafeCoreMirValidation.Validate(Program(ReturnBlock(), ReturnBlock(1)), new() { MaximumBlocks = 1 }).IsTruncated, "Block limits are enforced.");
+ SafeCoreMirProgram malformed = Program(new SafeCoreMirBlock(1, [], SafeCoreMirTerminator.Goto(-1, Source), Source));
+ AssertEx.True(SafeCoreMirValidation.Validate(malformed, new() { MaximumDiagnostics = 1 }).IsTruncated, "Diagnostic overflow cannot report successful validation.");
+ SafeCoreType nested = SafeCoreType.Tuple([SafeCoreType.Tuple([Integer])]);
+ SafeCoreMirProgram deep = new([Function([ReturnBlock()], [new(0, "arg", nested, SafeCoreMirLocalKind.Parameter, false, Source)])]);
+ AssertEx.True(SafeCoreMirValidation.Validate(deep, new() { MaximumTypeDepth = 1 }).IsTruncated, "Nested types consume depth budget.");
+ AssertEx.Throws(() => SafeCoreMirValidation.Validate(program, new() { MaximumOperations = 0 }));
+ return Task.CompletedTask;
+ }
+
+ private static Task FormattingAsync()
+ {
+ SafeCoreMirProgram program = Program(ReturnBlock());
+ const string expected = "safe-core-mir-v1\nfn @0 crate::main -> i32 entry bb0 [sample.rs:0+12/12 hir#0] {\n bb0 [sample.rs:0+12/12 hir#0]:\n return const 1:i32 [sample.rs:0+12/12 hir#0]\n}\n";
+ CultureInfo previous = CultureInfo.CurrentCulture;
+ try
+ {
+ CultureInfo.CurrentCulture = CultureInfo.GetCultureInfo("ar-EG");
+ AssertEx.Equal(expected, SafeCoreMirFormatting.Format(program));
+ }
+ finally { CultureInfo.CurrentCulture = previous; }
+ AssertEx.Equal(expected, SafeCoreMirFormatting.Format(program));
+ AssertEx.Throws(() => SafeCoreMirFormatting.Format(program, new() { MaximumCharacters = 1 }));
+ AssertEx.Throws(() => SafeCoreMirFormatting.Format(program, new() { MaximumOperations = 1 }));
+ AssertEx.Throws(() => SafeCoreMirFormatting.Format(program, new() { Timeout = TimeSpan.FromTicks(1) }));
+ using var cancellation = new CancellationTokenSource();
+ cancellation.Cancel();
+ AssertEx.Throws(() => SafeCoreMirFormatting.Format(program, new() { CancellationToken = cancellation.Token }));
+ return Task.CompletedTask;
+ }
+
+ private sealed class IndexOnlyList(T item) : IReadOnlyList
+ {
+ public int Count => 1;
+ public T this[int index] => index == 0 ? item : throw new ArgumentOutOfRangeException(nameof(index));
+ public IEnumerator GetEnumerator() => throw new InvalidOperationException("Unbounded enumeration is forbidden.");
+ IEnumerator IEnumerable.GetEnumerator() => GetEnumerator();
+ }
+
+ private sealed class OversizedList : IReadOnlyList
+ {
+ public int Count => 100_001;
+ public T this[int index] => throw new InvalidOperationException("Oversized collections must be rejected before access.");
+ public IEnumerator GetEnumerator() => throw new InvalidOperationException("Unbounded enumeration is forbidden.");
+ IEnumerator IEnumerable.GetEnumerator() => GetEnumerator();
+ }
+}