Project goal for Contracts: primitive ownership assertions

[dawidl022]

I have kept the project goal brief, focusing on the concrete deliverables and high-level impact, as the details have already been discussed in depth in MCP #942.

I am missing the "Team asks" section, since it mentioned that I can leave it blank if I'm unsure.

@Nadrieril I would appreciate a review and guidance on further steps that need to be taken from my side.

Rendered

[Nadrieril]

This looks overall good to me! I think after that someone from the project goals team should be able to merge it, and I think we just wait for the goal to be approved along with everything else from the 2026 slate?

Goals team: I'm the lang champion for the contracts lang experiment, so it makes sense to me to champion this goal. But the goal doesn't have much team asks, so does it even need a champion? I'm also unsure what's up with the current goal slate, can we still add things to it?

[dawidl022]

Thanks for the review @Nadrieril! I have included the compiler and Miri teams. Since the Miri integration is a large chunk of this goal, I intend to contribute code to the Miri side of the goal too. Since it will likely be a non-trivial feature in Miri, I have marked the support level as "medium".

[Nadrieril]

LGTM! I think we wait for the project goal team now.

View changes since this review

[nxsaken]

This field (and the "Needs funding" paragraph below) is outdated; please add a ## Funding section according to the template.

View changes since the review

[nxsaken]

Who will champion from miri?

View changes since the review

[nxsaken]

For the full Miri runtime ownership support task, please add a ## Help wanted section referencing that task. See this goal for an example.

Suggested change

	#### Implementation
	| Task | Owner(s) | Notes |
	| ----------- | -------- | ----- |
	| Low-level ownership assertion intrinsics available for use in contracts. | @dawidl022 | |
	| Higher-level wrapper assertions for typical use cases, including alignment, arrays etc. | @dawidl022 | |
	| Prototype integration with Miri - runtime ownership checks should work with the prototype Miri runtime ownership tracker as [implemented by Johannes Hostert](https://github.com/JoJoDeveloping/miri/tree/fulminate).|@dawidl022 | |
	| Full Miri runtime ownership support | |
	#### Documentation
	| Task | Owner(s) | Notes |
	| ----------- | -------- | ----- |
	| Reference level documentation: explaining the semantics of the ownership primitives, along with basic examples. | @dawidl022 | |
	| A tutorial: selecting one of the challenges in https://model-checking.github.io/verify-rust-std/challenges.html and walking the developer through what it means to write the specifications, and testing them using the Miri runtime. | @dawidl022 | |
	| Task | Owner(s) | Notes |
	| ----------- | -------- | ----- |
	| Implement low-level ownership assertion intrinsics | @dawidl022 | |
	| Implement higher-level wrapper assertions | @dawidl022 | Should cover typical use cases, including alignment, arrays, etc. |
	| Implement a prototype integration with Miri | @dawidl022 | Runtime ownership checks should work with the prototype Miri runtime ownership tracker as [implemented by Johannes Hostert](https://github.com/JoJoDeveloping/miri/tree/fulminate). |
	| Implement full Miri runtime ownership support | | |
	| Write Reference-level documentation | @dawidl022 | Should explain the semantics of the ownership primitives, along with basic examples. |
	| Write a tutorial | @dawidl022 | Select one of the challenges in https://model-checking.github.io/verify-rust-std/challenges.html, and walk the developer through what it means to write specifications and test them using the Miri runtime. |

View changes since the review