Safe Rust guarantees memory safety through strict compile-time constraints: ownership can be transferred, borrowing can temporarily guarantee either shared read-only or exclusive write access, and ownership and borrowing are scoped by lifetime. Automatically synthesizing correct and safe Rust code is challenging, as the generated code must not only satisfy ownership, borrowing, and lifetime constraints, but also meet type and interface requirements at compile time. This work proposes a synthesis method based on our newly defined Pushdown Colored Petri Net (PCPN) that models these compilation constraints directly from public API signatures to synthesize valid call sequences. Token colors encode dynamic resource states together with a scope level indicating the lifetime region in which a borrow is valid. The pushdown stack tracks the entering or leaving of lifetime parameter via pushing and popping tokens. A transition is enabled only when type matching and interface obligations both hold and the required resource states are available. Based on the bisimulation theory, we prove that the enabling and firing rules of PCPN are consistent with the compile-time check of these three constraints. We develop an automatic synthesis tool based on PCPN and the experimental results show that the synthesized codes are all correct.

翻译：安全Rust通过严格的编译时约束保证内存安全性：所有权可被转移，借用可临时保证只读共享或独占写访问，且所有权和借用由生命周期限定范围。自动合成正确且安全的Rust代码极具挑战性，因为生成的代码不仅必须满足所有权、借用和生命周期约束，还必须在编译时满足类型及接口要求。本文提出一种基于新定义的下推着色Petri网（PCPN）的合成方法，该方法直接从公共API签名对这些编译约束进行建模，以合成有效调用序列。令牌颜色编码动态资源状态，同时包含指示借用有效生命周期区域的层级范围。下推栈通过推入和弹出令牌来跟踪生命周期参数的进入或退出。仅当类型匹配与接口义务均满足且所需资源状态可用时，变迁才可被启用。基于互模拟理论，我们证明PCPN的启用与触发规则与这三类约束的编译时检查一致。我们开发了基于PCPN的自动合成工具，实验结果表明合成代码均正确无误。