pith. sign in

arxiv: 2604.02399 · v1 · submitted 2026-04-02 · 💻 cs.SE · cs.AI· cs.FL· cs.PL

A Synthesis Method of Safe Rust Code Based on Pushdown Colored Petri Nets

Kaiwen Zhang , Guanjun Liu This is my paper

Pith reviewed 2026-05-13 21:15 UTC · model grok-4.3

classification 💻 cs.SE cs.AIcs.FLcs.PL
keywords safe Rust synthesisPushdown Colored Petri Netsownership borrowing lifetimesbisimulationcode generationmemory safetyPetri netscompile-time constraints
0
0 comments X

The pith

Pushdown colored Petri nets model Rust ownership, borrowing, and lifetime rules to synthesize safe code from API signatures.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops a synthesis technique that automatically produces call sequences in safe Rust by encoding the language's strict compile-time constraints into a new kind of Petri net. Token colors track resource states and lifetime scopes while a pushdown stack records when lifetime parameters enter or leave scope. Transitions fire only when type matching, interface obligations, and available resource states all align. A bisimulation proof establishes that these net rules are equivalent to the checks performed by the Rust compiler for ownership transfer, shared or exclusive borrowing, and lifetime validity. The authors implement the method as a tool and report that every synthesized program compiles without violation of the safety rules.

Core claim

The central claim is that Pushdown Colored Petri Nets (PCPN) can synthesize valid Rust call sequences by modeling ownership transfer, borrowing access modes, and lifetime scoping directly from public API signatures, with colored tokens representing dynamic resource states together with scope levels and a pushdown stack managing lifetime parameter entry and exit, such that the enabling and firing rules are proven via bisimulation to be consistent with the Rust compiler's static checks for these three constraints.

What carries the argument

Pushdown Colored Petri Net (PCPN), in which token colors encode resource states and lifetime scope levels while the pushdown stack tracks entry and exit of lifetime parameters so that a transition is enabled only when type matching, interface obligations, and required resource states all hold.

Load-bearing premise

The public API signatures supply all information needed to model the full set of ownership, borrowing, and lifetime constraints and the bisimulation proof covers every relevant case of the Rust borrow checker.

What would settle it

An API for which the PCPN produces a call sequence that the Rust compiler rejects, or refuses to produce a known valid safe sequence, would show the model or proof is incomplete.

Figures

Figures reproduced from arXiv: 2604.02399 by Guanjun Liu, Kaiwen Zhang.

Figure 1
Figure 1. Figure 1: illustrates ownership transfer, where s is invalidated after moving to t, and the borrowing exclusivity rule, which allows the mutable borrow m only after the shared borrow r is explicitly dropped. It also shows explicit termination of borrows. 1 let s = R(1); 2 let t = s; // Ownership moved from s to t 3 // let u = s; // Illegal: s is now moved 4 let mut x = 0; 5 let r = &x; // Shared borrow starts 6 // l… view at source ↗
read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper claims to introduce Pushdown Colored Petri Nets (PCPN) to model Rust's ownership, borrowing, and lifetime constraints directly from public API signatures for synthesizing safe Rust code. Token colors encode resource states and scope levels, a pushdown stack tracks lifetime parameters, transitions are enabled only when type matching and resource states hold, and a bisimulation proof establishes consistency between PCPN enabling/firing rules and the borrow checker's compile-time checks for the three constraints. An automatic synthesis tool is developed, with experiments showing all generated codes are correct.

Significance. If the bisimulation proof holds without gaps, the work provides a formal, model-driven approach to safe Rust code synthesis that directly encodes compile-time constraints, which could support automated generation of memory-safe programs from API interfaces. The use of standard bisimulation theory and the experimental validation of synthesized code are strengths that add credibility to the central claim.

major comments (2)
  1. [Bisimulation proof section] The bisimulation proof (described in the section following the PCPN definition) claims that enabling and firing rules are consistent with compile-time checks for ownership, borrowing, and lifetimes, but the model description does not detail handling of non-lexical lifetimes or reborrowing; this is load-bearing for the consistency claim since the pushdown stack for lifetime parameters may not capture conditional access patterns.
  2. [§3.1] §3.1 (PCPN model definition): the assumption that public API signatures alone suffice to model all constraints is used to justify the transition enabling rules, but no explicit argument or counterexample analysis shows coverage of Rust-specific features like reborrowing, which risks the proof not applying to realistic call sequences.
minor comments (2)
  1. The abstract states that experiments show synthesized codes are correct but provides no details on the experimental setup, number of test cases, or how correctness was verified (e.g., via rustc compilation).
  2. [Notation] Notation for token colors (resource state + scope level) and pushdown operations could be clarified with a small example table to improve readability of the enabling conditions.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful and constructive review. The comments correctly identify areas where additional detail on lifetime handling would strengthen the presentation. We address each point below and will revise the manuscript to incorporate clarifications and expanded arguments.

read point-by-point responses

  1. Referee: [Bisimulation proof section] The bisimulation proof (described in the section following the PCPN definition) claims that enabling and firing rules are consistent with compile-time checks for ownership, borrowing, and lifetimes, but the model description does not detail handling of non-lexical lifetimes or reborrowing; this is load-bearing for the consistency claim since the pushdown stack for lifetime parameters may not capture conditional access patterns.

    Authors: The core PCPN model encodes lifetimes via the pushdown stack for entering and exiting lexical regions together with scope levels stored in token colors. This directly supports the standard borrow-checker rules for ownership transfer and borrowing. Non-lexical lifetimes are handled implicitly because a borrow token can be invalidated early when its resource state changes or when a conflicting transition fires, without requiring an explicit pop of the stack. Reborrowing is modeled by enabling a new transition that consumes the parent borrow token and produces a child borrow token carrying a nested lifetime; the bisimulation relation is preserved because both the original and reborrowed states remain consistent with the checker’s access rules. We will add an explicit subsection to the bisimulation proof that enumerates these cases and shows the relation still holds for conditional access patterns. revision: partial

  2. Referee: [§3.1] §3.1 (PCPN model definition): the assumption that public API signatures alone suffice to model all constraints is used to justify the transition enabling rules, but no explicit argument or counterexample analysis shows coverage of Rust-specific features like reborrowing, which risks the proof not applying to realistic call sequences.

    Authors: Public API signatures supply the type, mutability, and lifetime information that the borrow checker uses; the PCPN transition enabling rules replicate exactly those checks by matching colors and stack contents against the signature. Reborrowing is covered because a transition for a reborrow is enabled only when the parent mutable borrow’s color indicates an active exclusive state and the new lifetime is compatible with the stack top. We will insert into §3.1 a short paragraph that states this coverage argument and supplies a concrete counterexample (a reborrow from a mutable reference) demonstrating that the enabling condition correctly accepts or rejects the sequence. This addition will make the applicability to realistic call sequences explicit. revision: yes

Circularity Check

0 steps flagged

No significant circularity; PCPN model and bisimulation proof are independently defined

full rationale

The paper defines the PCPN model directly from public API signatures, with token colors and pushdown stack encoding states and lifetimes. It then invokes standard bisimulation theory to prove that enabling/firing rules match Rust's compile-time checks for ownership, borrowing, and lifetimes. No equations reduce a claimed prediction to a fitted input by construction, no self-citations form the load-bearing justification, and the bisimulation relation is presented as an external verification step rather than a tautology. The derivation chain remains self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central claim rests on the newly invented PCPN and the application of bisimulation theory, with no free parameters mentioned.

axioms (1)
  • standard math Bisimulation theory applies to the PCPN model to prove consistency with Rust compiler checks
    Invoked to prove that PCPN rules match compile-time checks.
invented entities (1)
  • Pushdown Colored Petri Net (PCPN) no independent evidence
    purpose: To model ownership, borrowing, and lifetime constraints in Rust
    Newly defined in this work to capture dynamic resource states and scope levels.

pith-pipeline@v0.9.0 · 5501 in / 1233 out tokens · 67430 ms · 2026-05-13T21:15:21.990329+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

29 extracted references · 29 canonical work pages

  1. [1]

    In: Proceedings of the thirty-sixth annual ACM symposium on Theory of computing

    Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Proceedings of the thirty-sixth annual ACM symposium on Theory of computing. pp. 202–211 (2004)

    work page 2004

  2. [2]

    Proceedings of the ACM on Programming Lan- guages3(OOPSLA), 1–30 (2019)

    Astrauskas, V., Müller, P., Poli, F., Summers, A.J.: Leveraging rust types for mod- ular specification and verification. Proceedings of the ACM on Programming Lan- guages3(OOPSLA), 1–30 (2019)

    work page 2019

  3. [3]

    In: International Conference on Concurrency The- ory

    Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: International Conference on Concurrency The- ory. pp. 135–150. Springer (1997)

    work page 1997

  4. [4]

    In: 2010 2nd International Symposium on Information Engineering and Electronic Com- merce

    Cai, L., Zhang, J., Liu, Z.: Generating test cases using colored petri net. In: 2010 2nd International Symposium on Information Engineering and Electronic Com- merce. pp. 1–5 (2010)

    work page 2010

  5. [5]

    In: European Conference on Object-Oriented Programming

    DeLine, R., Fähndrich, M.: Typestates for objects. In: European Conference on Object-Oriented Programming. pp. 465–490. Springer (2004)

    work page 2004

  6. [6]

    IEEE Trans- actions on Systems, Man, and Cybernetics54(7), 3908–3919 (Jan 2024)

    Dou, H., Zhou, M., Wang, S., Albeshri, A.: An Efficient Liveness Analy- sis Method for Petri Nets via Maximally Good-Step Graphs. IEEE Trans- actions on Systems, Man, and Cybernetics54(7), 3908–3919 (Jan 2024). https://doi.org/10.1109/TSMC.2024.3372941

    work page doi:10.1109/tsmc.2024.3372941 2024

  7. [7]

    In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

    Feng, Y., Martins, R., Wang, Y., Dillig, I., Reps, T.W.: Component-based synthesis for complex apis. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. pp. 599–612 (2017)

    work page 2017

  8. [8]

    Formal aspects of computing13(3), 341–363 (2002)

    Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable bind- ing. Formal aspects of computing13(3), 341–363 (2002)

    work page 2002

  9. [9]

    Theoretical computer science50(1), 1–101 (1987)

    Girard, J.Y.: Linear logic. Theoretical computer science50(1), 1–101 (1987)

    work page 1987

  10. [10]

    Proceed- ings of the ACM on Programming Languages6(ICFP), 711–741 (2022)

    Ho, S., Protzenko, J.: Aeneas: Rust verification by functional translation. Proceed- ings of the ACM on Programming Languages6(ICFP), 711–741 (2022)

    work page 2022

  11. [11]

    In: Petri nets: central models and their properties, pp

    Jensen, K.: Coloured petri nets. In: Petri nets: central models and their properties, pp. 248–299. Springer (1987)

    work page 1987

  12. [12]

    International Journal on Software Tools for Technology Transfer9(3), 213–254 (2007)

    Jensen, K., Kristensen, L.M., Wells, L.: Coloured petri nets and cpn tools for modelling and validation of concurrent systems. International Journal on Software Tools for Technology Transfer9(3), 213–254 (2007)

    work page 2007

  13. [13]

    In: Proceedings of the 36th International Conference on Software Engineering

    Jung, C., Lee, S., Raman, E., Pande, S.: Automated memory leak detection for production use. In: Proceedings of the 36th International Conference on Software Engineering. p. 825–836. ICSE 2014, Association for Computing Machinery, New York, NY, USA (2014), https://doi.org/10.1145/2568225.2568311

    work page doi:10.1145/2568225.2568311 2014

  14. [14]

    Proceedings of the ACM on Programming Languages4(POPL), 1–32 (2019)

    Jung, R., Dang, H.H., Kang, J., Dreyer, D.: Stacked borrows: an aliasing model for rust. Proceedings of the ACM on Programming Languages4(POPL), 1–32 (2019)

    work page 2019

  15. [15]

    Proceedings of the ACM on Programming Languages2(POPL), 1–34 (2017)

    Jung, R., Jourdan, J.H., Krebbers, R., Dreyer, D.: Rustbelt: Securing the founda- tions of the rust programming language. Proceedings of the ACM on Programming Languages2(POPL), 1–34 (2017)

    work page 2017

  16. [16]

    In: Proceedings of the fourteenth annual ACM symposium on Theory of computing

    Kosaraju, S.R.: Decidability of reachability in vector addition systems (preliminary version). In: Proceedings of the fourteenth annual ACM symposium on Theory of computing. pp. 267–281 (1982)

    work page 1982

  17. [17]

    Springer Nature (2022) 22 Kaiwen Zhang et al

    Liu, G.: Petri Nets: Theoretical Models and Analysis Methods for Concurrent Systems. Springer Nature (2022) 22 Kaiwen Zhang et al

    work page 2022

  18. [18]

    In: Proceedings of the 2014 ACM SIGAda annual conference on High integrity language technology

    Matsakis, N.D., Klock, F.S.: The rust language. In: Proceedings of the 2014 ACM SIGAda annual conference on High integrity language technology. pp. 103–104 (2014)

    work page 2014

  19. [19]

    Cambridge University Press (2013)

    Pitts, A.M.: Nominal sets: Names and symmetry in computer science. Cambridge University Press (2013)

    work page 2013

  20. [20]

    Theoretical Computer Science6(2), 223–231 (1978)

    Rackoff, C.: The covering and boundedness problems for vector addition systems. Theoretical Computer Science6(2), 223–231 (1978)

    work page 1978

  21. [21]

    In: Proceedings of the 22nd ACM SIGPLAN-SIGACT sympo- sium on Principles of programming languages

    Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: Proceedings of the 22nd ACM SIGPLAN-SIGACT sympo- sium on Principles of programming languages. pp. 49–61 (1995)

    work page 1995

  22. [22]

    IEEE Transactions on Systems, Man, and Cybernetics - Part A: Systems and Humans40(2), 337–351 (2010)

    Robidoux, R., Xu, H., Xing, L., Zhou, M.: Automated modeling of dynamic re- liability block diagrams using colored petri nets. IEEE Transactions on Systems, Man, and Cybernetics - Part A: Systems and Humans40(2), 337–351 (2010)

    work page 2010

  23. [23]

    In: Proceedings of the 12th international conference on Architectural support for programming languages and operating systems

    Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., Saraswat, V.: Combinatorial sketching for finite programs. In: Proceedings of the 12th international conference on Architectural support for programming languages and operating systems. pp. 404–415 (2006)

    work page 2006

  24. [24]

    ACM SIGPLAN Notices46(1), 447– 458 (2011)

    Tov, J.A., Pucella, R.: Practical affine types. ACM SIGPLAN Notices46(1), 447– 458 (2011)

    work page 2011

  25. [25]

    In: Proceedings of the 44th International Conference on Software Engineering: Software Engineering in Practice

    VanHattum, A., Schwartz-Narbonne, D., Chong, N., Sampson, A.: Verifying dy- namic trait objects in rust. In: Proceedings of the 44th International Conference on Software Engineering: Software Engineering in Practice. pp. 321–330 (2022)

    work page 2022

  26. [26]

    Proceedings of the ACM on Programming Languages9(PLDI), 1019–1042 (2025)

    Villani, N., Hostert, J., Dreyer, D., Jung, R.: Tree borrows. Proceedings of the ACM on Programming Languages9(PLDI), 1019–1042 (2025)

    work page 2025

  27. [27]

    Wadler, P.: Linear types can change the world! In: Programming concepts and methods. vol. 3, p. 5. North-Holland, Amsterdam (1990)

    work page 1990

  28. [28]

    CoRR abs/1903.00982 (2019)

    Weiss, A., Gierczak, O., Patterson, D., Ahmed, A.: Oxide: The essence of rust. arXiv preprint arXiv:1903.00982 (2019)

    work page arXiv 1903

  29. [29]

    IEEE Transactions on Industrial Electronics41(6), 567–583 (1994)

    Zurawski, R., Zhou, M.: Petri nets and industrial applications: A tutorial. IEEE Transactions on Industrial Electronics41(6), 567–583 (1994)

    work page 1994