Contracts: primitive ownership assertions

[nxsaken]

Metadata
Point of contact	@dawidl022
Team(s)	compiler, lang, miri
Goal document	2026/contracts-ownership-assertions

Summary

This project aims to implement the owned and alloc_block separation logic
assertions in the Rust compiler, as described in [MCP

Tasks and status

---

Note: we have updated the body to match the 2026 goal. Your original text is preserved below.

Details

Metadata
Point of contact	@dawidl022
Team(s)	compiler, lang, miri
Goal document	2026/contracts-ownership-assertions

Summary

This project aims to implement the owned and alloc_block separation logic assertions in the Rust compiler, as described in MCP #942, to enable the formal specification and verification of unsafe memory manipulation.

Tasks and status

[nxsaken]

This issue is intended for status updates only.

For general questions or comments, please contact the owner(s) directly.