Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 15 additions & 1 deletion ROADMAP.md
Original file line number Diff line number Diff line change
Expand Up @@ -429,7 +429,7 @@ publish warnings and no cleanup diagnostic. Both CoreCLR and Native AOT print
| P1-02 | ✅ Complete | Parse modules, items, statements, expressions, patterns, types, generics, and attributes in the safe-core profile. | P1-01 | `dotnet run --project tools/RustSharp.Conformance -c Release --no-restore -- --profile safe-core-syntax`<br>`pwsh -NoProfile -File eng/Test-SyntaxEvidence.ps1` | Manifest v3 passes 49/49 cases, 34/34 exact AST snapshots and 18/18 required categories. Rejections match diagnostic codes and source text; cancellation/deadlines, recovery and invalid evidence are tested in the 141/141 regression harness. The declared syntax profile is complete; unsupported semantic/HIR extensions explicitly report RSN1007. See the syntax contract and local evidence above. |
| 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`<br>`dotnet run --project tests/RustSharp.Tests/RustSharp.Tests.csproj -c Release --no-restore`<br>`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`<br>`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 | ⏳ Planned | Implement generic substitution, monomorphization, impl coherence, and the versioned trait-solver subset. | P0-14, P1-04 | `dotnet test RustSharp.slnx -c Release --filter GenericsAndTraits` | Generic functions/types emit closed AOT-reachable bodies; overlap, ambiguity, and missing bounds fail predictably. |
| 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-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. |
Expand All @@ -440,6 +440,20 @@ P1 exits when the versioned safe-core profile passes on CoreCLR and Windows/
Linux x64 Native AOT, and when borrow/Drop behavior has no unresolved semantic
difference inside that profile.

### PR execution order after P1-04

The next two implementation tracks may run in parallel: P1-05 depends on
P0-14/P1-04, and P1-06 depends on P1-04. Review and merge the generic foundation
PR first, followed by the typed-MIR foundation PR. Each PR states its exact
implemented subset, regression evidence and remaining milestone criteria.

Continue P1-05 with source/HIR generic binding and body specialization, and
P1-06 with aggregate, pattern and closure lowering. P1-07 starts when its typed
MIR prerequisites are usable; P1-08 follows the move/borrow gate. P1-09 combines
generic specialization and ownership-aware lowering before P1-10 closes the
full differential denominator. Completing a foundation PR does not mark its
entire milestone complete.

## P2: Deliver the core library and usable toolchain

| ID | Status | Work item | Hard dependency | Acceptance command | Observable result |
Expand Down
13 changes: 12 additions & 1 deletion ROADMAP_zh.md
Original file line number Diff line number Diff line change
Expand Up @@ -354,7 +354,7 @@ AOT 探测器。这些工作流修改需要新的 CI 运行。此配置的 Linux
| P1-02 | ✅ 已完成 | 解析安全核心配置档中的模块、项、语句、表达式、模式、类型、泛型和属性。 | P1-01 | `dotnet run --project tools/RustSharp.Conformance -c Release --no-restore -- --profile safe-core-syntax`<br>`pwsh -NoProfile -File eng/Test-SyntaxEvidence.ps1` | 第 3 版清单通过 49/49 个用例、34/34 份精确 AST 快照及 18/18 个必需类别。拒绝用例匹配诊断代码和源码文本;141/141 项回归工具覆盖取消/超时、错误恢复及非法证据。声明的语法配置已完成;尚不支持的语义/HIR 扩展显式返回 RSN1007。详见语法契约及上方本地证据。 |
| P1-03 | ✅ 已完成 | 将 AST 降低为 HIR,并实现声明的安全核心模块、命名空间、可见性、导入、名称解析和 Cargo 包入口。 | P1-02 | `dotnet run --project tools/RustSharp.Conformance -c Release --no-restore -- --profile safe-core-name-resolution`<br>`dotnet run --project tests/RustSharp.Tests/RustSharp.Tests.csproj -c Release --no-restore`<br>`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`<br>`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 test RustSharp.slnx -c Release --filter GenericsAndTraits` | 泛型函数/类型发出封闭且 AOT 可达的主体;重叠、歧义和缺失约束会以可预测方式失败。 |
| 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-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 上按指定顺序恰好运行一次析构函数。 |
Expand All @@ -364,6 +364,17 @@ AOT 探测器。这些工作流修改需要新的 CI 运行。此配置的 Linux
当版本化安全核心配置档在 CoreCLR 以及 Windows/Linux x64 Native AOT 上通过,且该
配置档内的借用/Drop 行为不存在未解决的语义差异时,P1 才能退出。

### P1-04 之后的 PR 执行顺序

接下来的两条实现线可以并行:P1-05 依赖 P0-14/P1-04,P1-06 依赖 P1-04。
评审和合并时先处理泛型基础 PR,再处理类型化 MIR 基础 PR。每个 PR 都列明
准确的已实现子集、回归证据及里程碑剩余验收条件。

随后 P1-05 继续接入源码/HIR 泛型绑定和主体特化,P1-06 继续实现聚合、模式和
闭包降低。P1-07 在类型化 MIR 前置条件可用后开始,P1-08 在移动/借用门槛之后
推进。P1-09 汇合泛型特化和所有权感知降低,之后由 P1-10 闭合完整差分分母。
基础 PR 完成不等于整个里程碑完成。

## P2:交付核心库和可用工具链

| ID | 状态 | 工作项 | 硬依赖 | 验收命令 | 可观察结果 |
Expand Down
127 changes: 127 additions & 0 deletions docs/generic-profile.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,127 @@
# Generic and trait foundation contracts

P1-05 is 🚧 In progress. This first PR adds reusable semantic foundations on the
existing `RustType` model. The P0 `TraitSolver`, its public signatures and default
behavior, and the `safe-core-types-v1` check-only profile remain unchanged.

The two version identifiers below describe library contracts. They are **not CLI
profile names**. This PR neither accepts generic Rust source through the compiler
pipeline nor emits generic executable bodies.

## Structural substitution and matching

`GenericSubstitution.Apply` recursively replaces type parameters inside nominal
type arguments. Substitution is simultaneous: `{T -> U, U -> i32}` applied to
`Pair<T, U>` produces `Pair<U, i32>`. A missing replacement leaves its parameter
open. Input dictionaries are copied with ordinal name comparison, regardless of
the caller's dictionary comparer. Replacement types and the resulting composed
type must satisfy the operation's nesting and identity-size limits.

`GenericSubstitution.Match` matches a template against a **closed** actual type.
Every occurrence of the same parameter must match the same structural type:
`Pair<T, T>` matches `Pair<i32, i32>` and rejects `Pair<i32, bool>`. The returned
binding map is immutable and ordinal. A failed match returns no partial bindings.

The type vocabulary is the P0 model: unit, bool, i32, str, parameters and nominal
types with type arguments. The richer P1-04 semantic type model is not implicitly
converted or erased. Lifetime and const parameters are outside this contract.

## `bounded-traits-v1`

`GenericTraitSolver` consumes immutable `GenericTraitImplementation` records.
Each record declares an implementation identity, trait identity, target template,
type parameters, and zero or more positive `GenericTraitObligation` bounds.
Identities supplied by the integration layer must be fully resolved and unique;
this layer does not perform source name resolution or crate ownership checks.

The solver validates its complete implementation set before solving a closed
goal. Every parameter must be declared and occur in its implementation target;
every bound may reference only those parameters. Duplicate implementation IDs and
malformed/default collections report `InvalidInput`.

Coherence uses structural unification of implementation heads. Variables are
shared within one head and renamed apart between implementations. An occurs
check rules out overlap that would require an infinite type. An exact head and a
matching generic head overlap; no most-specific winner is silently selected.
Overlapping heads fail with `OverlappingImplementations` even if their bounds
currently lack evidence. This conservative rule does not implement specialization,
negative reasoning, Rust's orphan rules, associated types, supertraits, auto
traits, higher-ranked bounds or trait objects.

A unique matching implementation substitutes and recursively proves its bounds.
Repeated successful goals are memoized within one operation. Missing evidence
reports `MissingImplementation`; a repeated active goal reports
`CyclicObligation`. Cycles are not accepted as coinductive proofs. Implementations
and selected evidence are ordered by ordinal identity, independent of insertion
order. Failures expose no partial successful evidence.

## `generic-plan-v1`

`GenericMonomorphization.Plan` consumes immutable function definitions, call
templates and explicit root instances. A definition contains its declared type
parameters, parameter/return type templates, call edges and trait bounds. All
definitions and call references are validated, including unreachable definitions.
Only instances reachable from the explicit roots appear in the output.

The planner substitutes each reachable function's signature and calls, rejects
open roots, undeclared parameters, wrong generic arity and missing definitions,
and proves each instantiated function's bounds with `bounded-traits-v1`. The
substitution, coherence checks, obligation proofs and reachability traversal share
one resource budget.

An instance is identified by its resolved function identity and structural type
arguments, using length-delimited canonical keys rather than display strings.
Repeated roots, diamond-shaped calls, and recursive calls to the same closed
instance deduplicate. Calls and instances have deterministic canonical-key order;
the order is stable, not a promise of source order or human alphabetical order.
Type-growing recursion must terminate within the instance, depth, work and time
budgets or report `LimitExceeded` with an empty plan. A failed plan never exposes
a partial graph as an AOT-ready result.

The output contains closed signatures and call edges. It is a reachability plan,
not a typed generic body or generated IL, and does not itself prove executable
AOT compatibility or Rust ownership semantics.

## Resource and failure contract

`GenericAnalysisLimits` applies to one public operation:

| Limit | Default | Allowed range |
| --- | --- | --- |
| Recursive depth | 64 | 1–128 |
| Work units | 100,000 | 1–1,000,000 |
| Collection, cache or instance items | 4,096 | 1–4,096 |
| Wall-clock timeout | 2 seconds | Greater than zero, at most 1 minute |

Existing nominal types allow at most 16 arguments; generic declarations likewise
allow at most 16 type parameters. Individual names are limited to 1,024
characters and canonical type identities to 65,536 characters. Recursive and
iterative work checks the shared wall-clock deadline and cancellation token.
No background tasks, processes, timers or temporary files are created.

Invalid limit configuration and null top-level arguments throw standard argument
exceptions. Invalid model data returns `InvalidInput`. Cancellation throws
`OperationCanceledException`. Exhaustion returns `LimitExceeded`; it never becomes
an assumed proof or a successful partial plan. Public results include a status,
an optional diagnostic and an `IsSuccess` property.

## Validation and remaining P1-05 work

`GenericFoundationTests` exercises nested/simultaneous substitution, ordinal
identities, repeated-parameter consistency, composed depth limits, nested and
missing bounds, conservative overlap, alpha-renaming and occurs checks, recursive
obligation cycles, type-growing obligations, deterministic reachability,
same-instance recursion, display-key collisions, bound validation, malformed
inputs, cancellation and resource limits. The tests run in the existing executable
regression harness:

```powershell
dotnet run --project tests/RustSharp.Tests/RustSharp.Tests.csproj -c Release --no-restore
```

The next P1-05 PRs must connect generic declarations and body checking to typed
HIR, resolve trait/impl identities and crate ownership, define source diagnostics
and a fixed differential corpus, and produce closed executable bodies through
the later CLR LIR/AOT integration. The full P1-05 acceptance criterion remains
open until generic functions/types emit closed AOT-reachable bodies and overlap,
ambiguity and missing bounds fail predictably through that compiler pipeline.
Loading
Loading