Pith. sign in

REVIEW 3 major objections 6 minor 27 references

Octopus: Practical Equivalence Checking of P4 Packet Parsers

T0 review · 3 major / 6 minor · reviewed 2026-08-04 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read A new checker named Octopus verifies that two P4 packet parsers accept exactly the same packets, producing a machine-checkable certificate or a counterexample bit-stream, and does so in minutes on a laptop.

desk verdict A genuinely useful tool with strong benchmarks, but the uninitialized-store semantics make negative equivalence verdicts unsound, so the main claim needs a caveat or a fix. read the letter →

arxiv 2608.01982 v1 pith:SCUVYM24 submitted 2026-08-03 cs.LO cs.PL

Jort van Leenen , Tobias Kappé This is my paper
classification cs.LOcs.PL
keywords P4packetparsersequivalencecheckingsymbolicbisimulationtemplate-guardedformulasstrongestpostconditionscertificatesSMTsolver
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper presents Octopus, a tool that decides whether two P4 packet parsers are behaviorally equivalent—whether they accept exactly the same input bit-streams and parse them into the same headers. It represents each parser as a finite automaton over configurations, then tries to build a symbolic bisimulation between two automata using template-guarded formulas. The central claim is that this approach makes parser equivalence checking practical: on every benchmark where a previous checker terminated, Octopus finished orders of magnitude faster and with far less memory, and it handled one benchmark that the earlier tool could not complete at all. If the claim holds, developers can run equivalence checks on refactored or optimized parsers in minutes on ordinary hardware, rather than reserving a server for a day.

What carries the argument

Template-guarded formulas (TGFs) are the load-bearing object: each TGF pairs a template—one state and buffer length per parser—with a first-order formula over both parsers' buffers and stores. The algorithm maintains a worklist of TGFs, repeatedly computing symbolic successors by reading bit chunks and applying strongest postconditions for extract and assignment operations, along with transition guards that include negations of earlier case conditions. SMT implication checks decide whether a successor is already covered; a mismatch in acceptance status triggers counterexample extraction. This compresses the astronomically large set of concrete configuration pairs into a few thousand formulas

What would settle it

Run the certificate validator on a set of known equivalent parsers and inspect the certificate with an independent checker; any certificate that passes validation but is rejected by an independent semantic check would refute soundness. More directly, construct two parsers that are identical except for reading an uninitialized header field before it is written, brute-force all bit-streams up to the parser's maximum depth, and check whether Octopus reports a counterexample despite identical accepted-language behavior; the paper's synthetic experiments suggest it sometimes does.

Watch

Extended reading notes

Core claim

The discovery is that a forward, symbolic bisimulation search can decide P4 parser equivalence without ever enumerating the enormous concrete state space. Octopus starts from the symbolic pair of initial configurations and repeatedly advances both parsers until one executes an operation, extending buffers with fresh bits and applying strongest-postcondition rules to update a first-order formula relating the two stores and buffers. Each symbolic step yields a template-guarded formula; if an SMT implication check shows a formula adds no new information, it is dropped, and if a template ever pairs an accepting state with a non-accepting state, the SMT model yields a concrete bit-stream countere

Load-bearing premise

Everything rests on Algorithm 1 and its strongest-postcondition rules being a faithful and terminating account of P4 parser semantics, and the paper supplies no proof of that; the synthetic benchmarks show uninitialized store values can already make the tool report a difference between parsers that are semantically equivalent.

Editorial extensions

If this is right

  • Developers can verify that a refactored or optimized P4 parser still accepts exactly the same packets, and can do so locally during development rather than on special hardware.
  • When parsers differ, the output includes a concrete bit-stream both parsers process and the paths each takes, so the failure can be reproduced and debugged mechanically.
  • Equivalence certificates can be re-checked independently by rerunning the validation routine, so a user need not trust the construction pass blindly.
  • The supported subset covers parsers where every state consumes at least one bit, with no lookahead and no header stacks; fixed-size header stacks can be encoded, while unbounded stacks would make equivalence undecidable.
  • The tool can also establish equivalence modulo later rejection, letting users compare parsers that differ only on packets discarded by later processing stages.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The main scalability gain comes from not constructing a machine-checked proof object at every run; this suggests a general strategy for practical verification—generate a lightweight certificate first, and only pay for formal proof when the certificate is disputed.
  • Because the paper reports that equivalent parsers can be judged inequivalent when store values are uninitialized, a natural extension is a mode that treats uninitialized reads as nondeterministic but abstracts over them, or that rewrites parsers to initialize headers first, yielding fewer false alarms.
  • The symbolic-bisimulation recipe is not P4-specific; the same TGF machinery could be applied to other stateful bit-stream decoders or binary-format parsers, as long as they can be modeled as finite automata with extract-like operations.
  • The observed runtime dominated by SMT calls suggests solver-side optimizations—such as incremental solving or embedded proof certificates—could reduce the validation phase, which currently roughly doubles the total time.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 6 minor

Summary. The paper presents Octopus, a Python tool for equivalence checking of P4 packet parsers. Octopus translates P4 programs (via P4C's IR) into deterministic automata over configurations consisting of parser state, store, and bit buffer, then attempts to construct a symbolic bisimulation using template-guarded formulas (TGFs) and SMT solving. Building on Leapfrog, it uses strongest-postcondition rules and a 'leaps' optimization to avoid bit-by-bit exploration. The evaluation reports orders-of-magnitude improvements over Leapfrog in runtime and memory on the Leapfrog benchmark suite, successfully handles a previously infeasible benchmark, scales on synthetic Whippersnapper parsers, and processes 435 comparisons of public P4 parsers on a laptop. The tool outputs either a bisimulation certificate or a counterexample bit-stream; the paper explicitly notes that synthetic self-comparisons may yield negative results due to uninitialized store values.

Significance. If the core algorithmic claims are correct, Octopus is a significant practical step: it makes parser equivalence checking feasible on consumer hardware, is open source, and ships a Docker artifact that reproduces the reported results. The use of an external benchmark suite (Leapfrog, Whippersnapper, public P4 programs) and the comparison with a previous tool are strengths. The main weakness is that the negative direction of the equivalence check is not a decision procedure under the paper's own automaton semantics, and no formal correctness theorem is supplied for the symbolic algorithm. These issues directly affect the central claim that Octopus can 'verify equivalence' and provide trustworthy counterexamples, so they need to be addressed before the paper can be accepted.

major comments (3)
  1. [Section 4, Algorithm 1; Section 5 ('Synthetic benchmarks')] The algorithm initializes the worklist with the TGF ⟨start,start,0,0,⊤⟩, leaving the left and right stores completely independent. For a parser whose transition logic reads a field that may not have been extracted, the same bit-stream can be accepted under one initial store and rejected under another. Octopus can therefore return a counterexample for a parser compared with itself. The paper acknowledges this in Section 5, but the consequence is not merely a limitation: under the automaton semantics of Section 3, accepted packets are those accepted by some initial store, so a disagreeing pair of stores does not witness language inequivalence. Negative verdicts are thus unsound with respect to the stated language-equivalence notion, and the public-code experiment's conclusion that 'the remaining parsers are pairwise inequivalent' relies on such verdicts. The fix should make the intended eq
  2. [Section 4, 'Bisimulation checking'] There is no formal statement, let alone proof, that Algorithm 1 is sound, complete, or terminating. The termination argument ('each iteration either grows the number of configurations ... or keeps this quantity constant while shrinking W') is not a proof: syntactically distinct TGFs are infinite even though configurations are finite, and the coverage check on Line 5 is an SMT entailment, not a well-founded measure. The paper also gives no theorem that returning K yields a bisimulation or that a returned counterexample witnesses inequivalence under a precisely defined parser-equivalence relation. Given that the central contribution is an equivalence checker, the authors should add precise theorem statements and proof sketches (or a reference to a full version containing them).
  3. [Section 4, Fig. 2 and ST≶] The strongest-postcondition rules in Fig. 2 cover only extraction and assignment; the transition-block semantics ST≶ is described only informally ('symbolically determine the next state', 'conjoin ... the negation of the conditions of all earlier cases'). Since Algorithm 1's successor generation and the certificate coverage check depend on this semantics, the described algorithm is not fully specified. A formal definition of ST≶, including how case conditions and their negations are encoded into TGFs, is necessary for the algorithm to be implemented and verified.
minor comments (6)
  1. [Section 3] The definition of configuration requires |w| < |op(q)|, but no op(q) is defined for the accept and reject states. Clarify how these states fit into the automaton, since δ maps transitions out of them to reject.
  2. [Section 4, Algorithm 1, Line 5] The notation W{φγ' | γ' ∈ K ∪ W, τγ' = τγ} is not defined; it presumably denotes a disjunction, but the formula construction should be spelled out.
  3. [Section 5, Table 1] It is unclear whether the Leapfrog runtimes and memory numbers were reproduced by the authors or taken from [8]. The text says the benchmarks were reproduced, but the data-availability statement excludes Leapfrog measurements; please state the source explicitly for each column.
  4. [Section 5, Fig. 3] Several axis labels are corrupted ('Memo y', 'T otal time', '#Val.'), and the figure does not report the equivalence outcomes of the synthetic self-comparisons. Since the paper admits false negatives in this class, the verdicts should be shown.
  5. [Section 5, 'Public code'] The claim that the remaining parsers are pairwise inequivalent 'because they support different sets of protocols' is presented as if it followed from the tool's negative results. Given the soundness issue in the negative direction, this conclusion needs manual evidence or a corrected algorithm.
  6. [Section 4, 'Certificate validation'] The certificate validator is not independent: it is described as using the same Algorithm 1 code paths. If the goal of certificates is to 'engender trust', the paper should either provide an independent validator or clearly state that validation reuses the construction algorithm and therefore does not provide independent assurance.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: Octopus is an independent reimplementation evaluated against external benchmarks; self-citations point to machine-checked prior work.

full rationale

The central claim—that Octopus can practically check P4 parser equivalence—is supported by an implementation (Algorithm 1) whose correctness would stand or fall on the soundness of the symbolic bisimulation construction, not on any fitted parameter or prediction. The paper's new contribution is an engineering reimplementation in Python of the Leapfrog approach, and it is evaluated against Leapfrog's own benchmark suite, Whippersnapper synthetic parsers, and 435 comparisons of public P4 programs. These are external benchmarks, not quantities derived from the tool's own outputs. The only self-citation that carries weight is the 'leaps' optimization: the paper says 'For a correctness proof of the leaps optimization, please consult [9, Lemma 5.6]' (Section 4), where [9] is a coauthored full version. However, Leapfrog [8] is implemented in the Rocq proof assistant and its proofs are machine-checked, so under the review rules this is independent evidence and does not raise the circularity score. The paper's admitted limitation in Section 5—that Octopus 'may decide negatively when different packets can be accepted depending on the (uninitialized) values in the store'—is a soundness/correctness concern for the negative direction of the equivalence check, not a circular argument, because it concerns the algorithm's behavior on self-comparisons rather than a derivation that assumes its own conclusion. No fitted input is renamed as a prediction, no uniqueness theorem is imported from the authors, and no known result is merely relabeled. Overall, the derivation chain is not circular: the tool's verdicts are checkable against the P4 semantics and external test cases, and the cited prior work provides independent, machine-verified backing for the optimizations borrowed from Leapfrog.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

Octopus is an engineering tool. It introduces no free parameters or invented entities. Its correctness rests on the stated P4-to-automata model, the unproved SP calculus, the cited leaps correctness lemma, and the trustworthiness of external tools (P4C, Z3, PySMT).

assumptions (5)
  • domain assumption P4 parsers in scope can be faithfully modeled as deterministic finite automata over configurations.
    Depends on restrictions: each state consumes at least one bit, no lookahead, no header stacks; unbounded stacks would make equivalence undecidable (Section 3).
  • domain assumption Acceptance is existential over initial store: a bit-stream is accepted if some start configuration with uninitialized store accepts.
    This semantic choice is from the P4 spec on uninitialized fields; it underlies the initial TGF with the ⊤ formula (Section 4).
  • ad hoc to paper The strongest-postcondition rules in Fig. 2 correctly capture the effect of extract and assignment operations.
    The rules are stated without proof; correctness is assumed for the symbolic bisimulation.
  • domain assumption The leaps optimization is correct per Lemma 5.6 of the cited full Leapfrog version [9].
    Cited to a reference co-authored by one of the present authors; not proved in this paper.
  • domain assumption Z3, PySMT, and P4C are trusted to be correct.
    The tool's verdicts rely on these external components; the paper acknowledges this in its trusted-base discussion (Section 5).

how reviews work

0 comments
Cite this review

Pith. "Pith review of Octopus: Practical Equivalence Checking of P4 Packet Parsers." pith.science (2026). https://pith.science/paper/SCUVYM24

@misc{pith2026260801982,
  author       = {Pith},
  title        = {Pith review of: Octopus: Practical Equivalence Checking of P4 Packet Parsers},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/SCUVYM24}},
  note         = {Machine review of arXiv:2608.01982}
}
read the original abstract

P4 is a domain-specific language for programming protocol-independent packet processors, where packet parsers describe how incoming bit-streams are structured into headers and fields. Building on work by Doenges et al. (2022), we present Octopus, a tool that translates P4 packet parsers into automata and then attempts to (symbolically) check their equivalence. Octopus produces evidence, either in the form of a bisimulation demonstrating equivalence, or a counterexample bit-stream witnessing a behavioral difference between the two parsers. In contrast with earlier work, our tool can check equivalence between non-trivial parsers within minutes, on consumer hardware. We report on the tool's implementation and evaluate its usability in networking contexts.

Figures

Figures reproduced from arXiv: 2608.01982 by the authors.

Figure 1
Figure 1. An illustration of the structured information contained in a UDP packet. The left-most four blocks represent the fields comprising the packet’s header. The right￾most block represents the packet’s payload. Leapfrog [8] is an equivalence checker for P4 packet parsers, implemented in the Rocq proof assistant [26]. It accepts a deeply embedded representation of a subset of P4 parsers, which it attempts to prove equival… view at source ↗
Figure 2
Figure 2. The strongest postcondition (SP≶) of an operation block, with the symbol ≶ ∈ {<, >} depending on which parser the operation block belongs to. depending on where the transition block belongs. If no transition is executed, the symbolic transition leaves the state unchanged under the trivial constraint. On the whole, the algorithm must terminate, simply because each iteration of the loop either grows the number of conf… view at source ↗
Figure 3
Figure 3. The total wall-clock time (left vertical axis, in seconds) and peak resident mem￾ory (right vertical axis, in MiB) required by Octopus running on synthetic benchmarks generated through Whippersnapper. Each generated parser is compared against itself, where the expected outcome is equivalence — although Octopus may decide negatively when different packets can be accepted depending on the (uninitialized) values in the… view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

27 extracted references · 1 canonical work pages

  1. [9]

    https://doi.org/10.48550/arXiv.2205

    Doenges, R., Kappé, T., Sarracino, J., Foster, N., Morrisett, G.: Leapfrog: certi- fied equivalence for protocol parsers (2022). https://doi.org/10.48550/arXiv.2205. 08762, full version including proofs

    doi:10.48550/arxiv.2205 2022

  2. [1]

    In: TACAS

    Barbosa, H., Barrett, C., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mo- hamed, A., Mohamed, M., Niemetz, A., Nötzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A Versatile and Industrial- Strength SMT Solver. In: TACAS. pp. 415–442 (2022). https://doi.org/10.1007/ 978-3-030-99524-9_24

    2022

  3. [2]

    In: HotSDN

    Berde, P., Gerola, M., Hart, J., Higuchi, Y., Kobayashi, M., Koide, T., Lantz, B., O’Connor, B., Radoslavov, P., Snow, W., Parulkar, G.M.: ONOS: towards an open, distributed SDN OS. In: HotSDN. pp. 1–6 (2014). https://doi.org/10.1145/ 2620728.2620744

    arXiv 2014

  4. [3]

    Bosshart,P.,Daly,D.,Gibb,G.,Izzard,M.,McKeown,N.,Rexford,J.,Schlesinger, C., Talayco, D., Vahdat, A., Varghese, G., Walker, D.: P4: programming protocol- independent packet processors. Comput. Commun. Rev.44(3), 87–95 (2014). https://doi.org/10.1145/2656877.2656890

    arXiv 2014

  5. [4]

    Czajka, L., Kaliszyk, C.: Hammer for Coq: Automation for dependent type theory. J. Autom. Reason.61(1-4), 423–453 (2018). https://doi.org/10.1007/ S10817-018-9458-4

    2018

  6. [5]

    In: SOSR

    Dang, H.T., Wang, H., Jepsen, T., Brebner, G., Kim, C., Rexford, J., Soulé, R., Weatherspoon, H.: Whippersnapper: A P4 Language Benchmark Suite. In: SOSR. pp. 95–101 (2017). https://doi.org/10.1145/3050220.3050231

    arXiv 2017

  7. [6]

    In: TACAS

    De Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: TACAS. pp. 337–340 (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    doi:10.1007/978-3-540-78800-3_24 2008

  8. [7]

    In: POPL

    Doenges, R., Arashloo, M.T., Bautista, S., Chang, A., Ni, N., Parkinson, S., Pe- terson, R., Solko-Breslin, A., Xu, A., Foster, N.: Petr4: formal foundations for P4 data planes. In: POPL. pp. 1–32 (2021). https://doi.org/10.1145/3434322

    doi:10.1145/3434322 2021

Show all 27 references
  1. [8]

    In: PLDI

    Doenges, R., Kappé, T., Sarracino, J., Foster, N., Morrisett, G.: Leapfrog: certified equivalence for protocol parsers. In: PLDI. pp. 950–965 (2022). https://doi.org/10. 1145/3519939.3523715

    2022

  2. [10]

    Ekici, B., Mebsout, A., Tinelli, C., Keller, C., Katz, G., Reynolds, A., Barrett, C.W.: SMTCoq: A plug-in for integrating SMT solvers into Coq. In: CAV. pp. 126–133 (2017). https://doi.org/10.1007/978-3-319-63390-9_7

    2017 doi

  3. [11]

    In: SMT workshop (2015)

    Gario, M., Micheli, A.: PySMT: a solver-agnostic library for fast prototyping of SMT-based algorithms. In: SMT workshop (2015)

    2015

  4. [12]

    In: NEAT@SIGCOMM

    He, M., Blenk, A., Kellerer, W., Schmid, S.: Toward consistent state management of adaptive programmable networks based on P4. In: NEAT@SIGCOMM. pp. 29– 35 (2019). https://doi.org/10.1145/3341558.3342202

    2019

  5. [13]

    https://doi.org/10.48550/arXiv.1804.01468

    Kheradmand, A., Rosu, G.: P4K: A Formal Semantics of P4 and Applications (2018). https://doi.org/10.48550/arXiv.1804.01468

    2018 doi arXiv

  6. [14]

    Pearson Education Limited, Harlow, United Kingdom, 8th edn

    Kurose, J.F., Ross, K.W.: Computer Networking: A Top-Down Approach. Pearson Education Limited, Harlow, United Kingdom, 8th edn. (2022)

    2022

  7. [15]

    Thesis Bach- elor Informatica, LIACS, Leiden University (2025), https://theses.liacs.nl/3410

    van Leenen, J.: Practical Equivalence Checking of P4 Packet Parsers. Thesis Bach- elor Informatica, LIACS, Leiden University (2025), https://theses.liacs.nl/3410

    2025

  8. [16]

    In: SIGCOMM

    Liu, J., Hallahan, W., Schlesinger, C., Sharif, M., Lee, J., Soulé, R., Wang, H., Caşcaval,C.,McKeown,N.,Foster,N.:p4v:practicalverificationforprogrammable data planes. In: SIGCOMM. pp. 490–503 (2018). https://doi.org/10.1145/3230543. 3230582 14 J. van Leenen & T. Kappé

    2018 doi

  9. [17]

    In: CoNEXT

    Neves, M., Freire, L., Schaeffer-Filho, A., Barcellos, M.: Verification of P4 programs in feasible time using assertions. In: CoNEXT. pp. 73–85 (2018). https://doi.org/ 10.1145/3281411.3281421

    2018

  10. [18]

    In: SOSR

    Nötzli, A., Khan, J., Fingerhut, A., Barrett, C., Athanas, P.: p4pktgen: Automated Test Case Generation for P4 Programs. In: SOSR. pp. 1–7 (2018). https://doi.org/ 10.1145/3185467.3185497

    2018

  11. [19]

    In: USENIX Security

    Ramananandro, T., Delignat-Lavaud, A., Fournet, C., Swamy, N., Chajed, T., Kobeissi, N., Protzenko, J.: Everparse: Verified secure zero-copy parsers for au- thenticated message formats. In: USENIX Security. pp. 1465–1482 (2019). https: //doi.org/10.5555/3361338.3361440

    2019

  12. [20]

    Rosu, G., Serbanuta, T.: An overview of the K semantic framework. J. Log. Alge- braic Methods Program.79(6), 397–434 (2010). https://doi.org/10.1016/J.JLAP. 2010.03.012

    2010 doi

  13. [21]

    Cambridge University Press (2011)

    Sangiorgi, D.: Introduction to bisimulation and coinduction. Cambridge University Press (2011). https://doi.org/10.1017/CBO9780511777110

    2011 doi

  14. [22]

    IEEE Syst

    Sassaman, L., Patterson, M.L., Bratus, S., Locasto, M.E.: Security applications of formal language theory. IEEE Syst. J.7(3), 489–500 (2013). https://doi.org/10. 1109/JSYST.2012.2222000

    2013

  15. [23]

    In: SIGCOMM

    Stoenescu, R., Dumitrescu, D., Popovici, M., Negreanu, L., Raiciu, C.: Debugging P4 programs with vera. In: SIGCOMM. pp. 518–532 (2018). https://doi.org/10. 1145/3230543.3230548

    2018

  16. [24]

    The P4 Language Consortium: P416 Language Specification - version 1.2.5 (2024), https://p4.org/wp-content/uploads/2024/10/P4-16-spec-v1.2.5.html

    2024

  17. [25]

    The P4 Language Consortium: P4C — the P416 reference compiler (2026), https: //github.com/p4lang/p4c

    2026

  18. [26]

    The Rocq development team: The Rocq Prover (2026), https://rocq-prover.org/

    2026

  19. [27]

    In: SIGCOMM

    Tian, B., Gao, J., Liu, M., Zhai, E., Chen, Y., Zhou, Y., Dai, L., Yan, F., Ma, M., Tang, M., Lu, J., Wei, X., Liu, H.H., Zhang, M., Tian, C., Yu, M.: Aquila: a prac- tically usable verification system for production-scale programmable data planes. In: SIGCOMM. pp. 17–32 (2021...

    2021

Pith tools

Reviewed August 4, 2026 · model on record in the stance chip above.