Translation Validation for the P4 compiler

[fruffy]

Gauntlet (cough) has show that it is possible to use translation validation at scale and effectively for P4 programs. This is because the P4 language itself is restricted enough that you can easily convert it to pure SMT expressions and then use these expressions for equality checks in a solver like Z3.

The problem with Gauntlet is that it is an external tool, and not well integrated with the current P4 compiler. Particularly because Gauntlet uses its own type inference and state tracking it is difficult to maintain with developments to the P4 language.

Ideally, we should have a translation validation library as part of P4C, which we can call into to convert a particular P4 construct (e.g., IR:Expression, IR::P4Control, IR::P4Parser) into SMT logic and then use this representation for various validation tasks.

Use case 1: You could use this representation to check whether a particular language construction is "semantically equivalent" before and after a compiler transformation. This is similar to Credible Compilation, which validates that a particular compile step is semantically correct.

Use case 2: Another use case is superoptimization. We can use this SMT representation to transform basic blocks into "better", and semantically equivalent structures.

[jnfoster]

Cool ideas! Would any of the p4testgen infrastructure be useful for this?

[fruffy]

Cool ideas! Would any of the p4testgen infrastructure be useful for this?

I think so, but it requires work. One problem is that the P4Testgen is build as a monolith, it is designed to consume a P4 program as a whole. Ideally, we want to check single basic blocks.

The symbolic executor interface requires ProgramInfo, which in turn requires compiler information.

Carrying this information along could be onerous.

[Sarthak-Developer-Coder]

It looks like you're referring to Translation Validation for the P4 compiler, possibly an issue or a feature request (likely from the P4 GitHub repositories).

What is Translation Validation?

Translation validation is a technique used in compilers to verify that the translation (compilation) of a source program to a lower-level representation (e.g., P4 to target-specific backend) is correct. Instead of proving the compiler correct, we validate that a given compilation result preserves the intended behavior of the source program.

Why is this Important for P4?

• P4 is used to define packet-processing behavior, so correctness is critical to avoid unintended network issues.
• Different targets (BMv2, Tofino, FPGA, etc.) have different compilation paths, and ensuring correctness across them is essential.
• Helps debug and prevent compiler bugs that might lead to incorrect forwarding behavior.

Possible Approaches for Translation Validation in P4

1. Symbolic Execution & Equivalence Checking

   • Compare the P4 source and the compiled intermediate representation (IR) to check if they are semantically equivalent.
   • Could use SMT solvers like Z3 or Coq for verification.

2. Reference Execution (Test-Based Approach)

   • Run the same test packets on both the original P4 program (BMv2) and the compiled target (Tofino, etc.).
   • Compare outputs to validate correctness.

3. Intermediate Representation (IR) Comparison

   • Check the P4_16 representation before and after passes (P4IR, P4Info, etc.) for consistency.
   • Ensure optimizations do not change packet-processing semantics.

4. Trace-based Validation

   • Capture packet traces before and after compilation and compare them.
   • Requires defining correctness invariants (e.g., headers should be modified as expected).

Challenges

• Target-Specific Behavior: Some backends introduce optimizations that may alter execution order.
• Scalability: Formal verification can be computationally expensive.
• Debugging Complex Pipelines: Large P4 programs can have deeply nested control logic.

Next Steps

• Are you looking to implement this in a specific P4 compiler (e.g., p4c)?
• Would you like help in designing a test framework for translation validation?

Let me know how I can assist! 🚀

[qobilidop]

I'm interested in integrating Gauntlet into P4MLIR for its translation validation as well. I just came across this PLDI'25 paper that seems very relevant: First-Class Verification Dialects for MLIR. Some inspirations from this paper:

1. At a high-level, I feel this MLIR based approach is quite extensible. We can build on top of it and add the P4 domain specific part, e.g. adding a P4MLIR box alongside MLIR-CORE and CIRCT in Fig. 1.
2. The SMT dialect is already upstreamed to MLIR. The semantics of P4MLIR dialects can be specified as lowerings to this SMT dialect.
3. Direct lowering from P4MLIR dialects to the SMT dialect might be challenging. However, as proposed in this paper, there could be a middle layer to separate the concern (see the High-Level Semantics box of Fig. 2). I think for P4, there could probably be a Gauntlet IR dialect designed at this abstraction level. This whole idea is also similar to Alive2 IR in Alive2.

Some figures copied from the paper for the convenience of discussion:

[Sarthak-Developer-Coder]

Hii @qobilidop can we connect
my linkedin id https://www.linkedin.com/in/sarthak-nag-b91861291?lipi=urn%3Ali%3Apage%3Ad_flagship3_profile_view_base_contact_details%3BN2XPHeZESOaWoxXq6FINbQ%3D%3D

[Sarthak-Developer-Coder]

---

Hi  @qobilidop

Thanks a ton for sharing the First‑Class Verification Dialects for MLIR paper—this is exactly the missing puzzle‑piece for integrating Gauntlet into our P4MLIR translation‑validation flow. A few quick reactions and a proposal for next steps:

---

1  |  Positioning P4MLIR inside the new “First‑Class Semantics” stack

• Fig. 1 maps cleanly to a future “P4MLIR” pillar, sitting alongside mlir‑core and CIRCT.

• That lets us reuse the same semantics/TV/BMC toolchain instead of inventing a P4‑specific one.

2  |  Lower‑to‑SMT strategy

• Great call‑out on the upstream SMT dialect—it gives us a solver‑agnostic target.

• Direct lowering from every P4 construct → smt_* ops is indeed steep. I agree with the paper’s layered approach and …

3  |  Introducing a Gauntlet‑IR dialect as the “High‑Level Semantics” layer (Fig. 2)

• Mirrors Alive2‑IR’s role for LLVM.

• Encodes P4 semantics (match‑action, parser state, deparser ordering, etc.) in a form that’s:

  1. Easier for Gauntlet to reason about, and

  2. Still MLIR‑native, so we keep passes/composability.

• From there we can explore multiple, semantics‑preserving lowering paths to smt_bv, smt_array, etc., just like the paper suggests.

4  |  Translation‑Validation Pipeline Sketch (adapted from Fig. 7)

P4 source  ──► P4MLIR (frontend)
              │
              ├─►   Gauntlet‑IR   ──►   SMT‑dialect   ──►  Z3/CVC5
              │        ▲                         │
   optimized  │        │                         │
   P4MLIR  ───┘   semantics‑optimization   (Gauntlet TV)

TV = translation validation, BMC = bounded model checking

---

5  |  Concrete next steps

When	Task	Owner
Week 0–1	Draft the GauntletIR dialect definition (ops/types for headers, tables, actions).	Me
Week 1–2	Spike a trivial lowering “GauntletIR → smt_core” for a tiny P4 program.	Me + <Solver‑Guru>
Week 2	Sync w/ MLIR devs to upstream any reusable pieces.	Us
Month 1	Prototype first translation‑validation pass (P4MLIR → GauntletIR on two versions, prove equivalence).	Team

---

6  |  Open questions for you

1. Do you foresee any P4 corner‑cases that must bypass GauntletIR and drop straight to SMT?

2. Would it help to expose P4 control‑plane constraints (e.g. table updates) as first‑class SMT axioms?

3. Timing: can we pencil in a 30‑min design review next week?

Really excited—this paper gives us a principled roadmap instead of a bespoke one‑off. Let me know what you think, and happy to iterate.

Best,
Sarthak Nag

---

[qobilidop]

Hi @Sarthak-Developer-Coder,

Thanks for your interest in this project. A few quick comments:

1. Your responses seem to be mainly AI-generated. For a healthy open source community, we don't want to be overwhelmed by AI-generated responses. So for our further communications, please provide your own thoughts.
2. As to the project itself, it's still at a phase of high-level discussion. I don't think any concrete approach is committed yet, including my proposal. So it's too early to talk about execution and timeline. I would expect @fruffy (as the author of Gauntlet and main maintainer of P4C) to lead and make the major technical decisions.
3. I don't think either @fruffy or I have time to mentor someone to work on this. So if you are really excited about this project, I'd encourage you to build some prototype on your side, e.g. in a repo you own. And when you have more concrete questions, feel free to ping us for discussion.
4. To emphasize again, please don't simply use AI for any further discussions. We might just ignore them if we feel that's what you are doing.

Best,
Bili

[Sarthak-Developer-Coder]

Hi @qobilidop,

Thank you so much for the candid feedback — I truly respect your honesty.

I completely understand the concern around AI-generated content. From now on, everything I write will reflect my own voice, understanding, and genuine curiosity. I’m committed to growing in open source the right way, by learning, building, and contributing authentically.

Regarding the Gauntlet project, I appreciate the clarification about its current stage. I’ll start working on a small prototype on my own repo and experiment with lowering GauntletIR to something minimal, just to get my hands dirty and gain deeper insights. I’ll make sure to only reach out when I have concrete technical progress or thoughtful questions that can actually contribute to the conversation.

On a separate note — I’m really passionate about compilers, systems, and developer tooling, and I’m currently exploring internship opportunities. If you happen to think I could be a good fit for an internship at Google, I would be incredibly grateful for a referral. I’m a Computer Science student from India, and I’d love a chance to learn from teams working on cutting-edge infrastructure like this.
Here’s my GitHub: https://github.com/Sarthak-Developer-Coder
Email: sarthakthesde@gmail.com

Thanks again for your time, guidance, and for maintaining the spirit of high-quality collaboration. I’ll be back with something meaningful.

Best regards,
Sarthak Nag

[fruffy]

@Sarthak-Developer-Coder This is not the right forum to ask for internships.

@qobilidop

I'm interested in integrating Gauntlet into P4MLIR for its translation validation as well. I just came across this PLDI'25 paper that seems very relevant: First-Class Verification Dialects for MLIR. Some inspirations from this paper:

If the dialect allows us to convert a particular block of code into SMT in a self-contained way, that would be great.

I have done conversion from P4C-IR to SMT/Z3 several times now. The challenge is usually crafting the interpreter and walking through the IR in such a way that you avoid state-space explosion. In this case, if we check peep-hole optimizations similar to Alive2 that could work out well. We probably can be much more aggressive, too.