{"id":"ab270db8-f7f0-47eb-a7e8-73049efa9a61","arxiv_id":"2506.13383","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"StacKAT adds a stack to NetKAT and has a decidable equivalence problem, with automata-based counterexample generation and a complete equational theory for the push-pop fragment.","lead":"This paper introduces StacKAT, a network verification language that adds an unbounded stack to NetKAT, letting programs push and pop packet header values as packets flow. The authors prove that equivalence of StacKAT programs is decidable, show how to extract counterexamples, and give a complete axiomatization for the stack-only fragment.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 3.12's 'check bisimilarity' is not justified: NFA bisimilarity is stronger than language equivalence, so the stated decision procedure may reject equivalent programs.","rationale":"I read the paper as claiming a decision procedure: Theorem 3.7 reduces semantic equivalence to equality of canonical languages, and Theorem 3.12 then gives the automata-theoretic check. The load-bearing step is therefore the final automaton comparison. The paper says 'check bisimilarity,' but never proves that the canonical NFAs are deterministic or that bisimilarity coincides with language equivalence on this class. Since bisimilarity of nondeterministic automata is a strictly finer invariant than language equivalence, the stated procedure is incomplete. This is a correctness gap in a main theorem, not a stylistic issue. However, it is readily addressable by checking NFA language equivalence (e.g., via product construction and emptiness, or subset construction), which is what Section 3.5's complexity discussion and Section 5.1's implementation actually describe. I therefore do not move the reader's CONDITIONAL verdict; I only sharpen the reason. The reader's named weakest assumption, Lemma 3.10, is less convincing as a fatal flaw: the poppush closure inserts pop(v)push(v) at every pop/push boundary for every v in the finite value set, so the generation of pop(a::r)push(b::r) from pop(a)push(b) goes through by induction on r, and V-fullness is already assumed in the alphabet. Thus the more dangerous unresolved point is Theorem 3.12's bisimilarity instruction. A concrete check on e=1 vs f=1+pop(1)push(1) will settle whether the canonical automata can be language-equivalent without being bisimilar; if so, the theorem must be amended.","tokens_in":34239,"tokens_out":24378,"duration_ms":254104,"concrete_test":"Implement the pipeline exactly as in Theorem 3.12 for the pair e = 1 and f = 1+pop(1)push(1): build the Antimirov NFAs, apply push-pop closure, filter, zip, and precompose with A*, then test whether the two resulting NFAs are bisimilar and whether they are language-equivalent. Both languages should be A* (i.e., all words pop(s)push(s)); if the automata are language-equivalent but not bisimilar, the stated 'check bisimilarity' is incomplete. If they happen to be bisimilar, repeat on the paper's own example e = push(3)*·pop(3)* and f = pop(3)*·push(3)* after the final A* precomposition; the two canonical automata are claimed to be language-equivalent, so they must also be bisimilar for Theorem 3.12 to hold.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central decidability claim rests on Theorem 3.7: JeK=JfK iff Lbar(e)=Lbar(f), so an equivalence decision can be obtained by comparing the canonical zipped languages. Theorem 3.12, however, says to 'check bisimilarity of these resulting automata.' The automata produced by Figure 6 are NFAs: initial states are all pairs (q,q), and the rules add epsilon transitions and simultaneous backward-pop/forward-push steps, so the machine is not determinized. For NFAs, bisimilarity is strictly stronger than language equivalence; two automata can accept the same language and still fail to be bisimilar. Hence the procedure as stated is incomplete: there will be semantically equivalent programs whose canonical automata are language-equivalent but not bisimilar, and the bisimilarity check would wrongly report inequivalence. The issue is not terminological: Section 3.5's PSPACE bound is justified by NFA language-equivalence, which is PSPACE-complete, whereas bisimilarity is polynomial; and Section 5.1 says the implementation checks language equivalence. Thus the main theorem's decision procedure needs either a determinization step or an explicit language-equivalence (or bisimulation-up-to-language-equivalence) check, and this must be stated and proved. Lemma 3.10, by contrast, appears repairable: the poppush closure does insert pop(r)push(r) for all residuals r, so the exact-stack semantics match once all values in V are available. The bisimilarity gap is the more direct threat to the advertised algorithm.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces StacKAT, an extension of NetKAT with push and pop stack operations over a finite value set, and studies the equivalence problem for StacKAT programs. The main claims are: (i) equivalence in the pure push-pop fragment is decidable by canonicalizing the trace language through push-pop cancellation, filtering to pop* push* traces, and pop-push closure, then comparing the resulting zipped trace languages (Theorems 3.7 and 3.12); (ii) equivalence for full StacKAT, including header tests and assignments, reduces to equivalence of header-parameterized trace languages (Theorem 4.2), giving an EXPSPACE decision procedure (Theorem 4.5); (iii) counterexamples can be extracted when programs are inequivalent; and (iv) a complete axiomatization for the push-pop fragment is provided using a new dagger operator on languages (Theorem 6.9). The paper includes a detailed appendix with proofs, an interactive implementation, and benchmarks.","tokens_in":34498,"tokens_out":11251,"duration_ms":115699,"significance":"If the results are correct, this is a substantial contribution: StacKAT is a natural infinite-state extension of NetKAT, and the paper shows that its equivalence problem remains decidable despite the presence of a stack, with a matching EXPSPACE algorithm and a completeness result for the push-pop fragment. The central technical idea, zipping trace languages so that the non-regular pop-push closure becomes a regular precomposition A* · zip(L), is elegant and useful. The paper also ships a working implementation and benchmarks, which strengthens confidence that the constructions are concretely realizable. The main caveats are that Theorem 3.12 states a bisimilarity check that is not justified for the nondeterministic automata built by the construction, and that the load-bearing Lemma 3.10 is only proved by a two-sentence sketch. Both issues appear repairable within the paper's scope.","major_comments":[{"comment":"The stated decision procedure says to 'check bisimilarity of these resulting automata,' but the constructed automata are NFAs in general. Figure 6 creates initial states (q,q), epsilon transitions, and simultaneous backward-pop/forward-push steps without determinization, and the precomposition with A* in Lemma 3.6 adds further nondeterminism. For NFAs, bisimilarity is strictly stronger than language equivalence, so a bisimilarity check can reject semantically equivalent programs and is not justified by Theorem 3.7, which is stated in terms of language equality. The complexity argument in Section 3.5 and the implementation description in Section 5.1 rely on language equivalence, not bisimilarity. Please replace the bisimilarity check with an explicit language-equivalence check on the canonicalized automata (or prove that the constructed automata are deterministic or complete in a sense that makes bisimilarity coincide with language equivalence), and update the counterexample-extraction wording in Section 5 accordingly.","section":"Section 3.4, Theorem 3.12"},{"comment":"Lemma 3.10 is load-bearing for Theorem 3.7: it identifies [Lbar] with [Lbar]' and is the only step that lets Lemma 3.11 be applied. The proof, however, is only a two-sentence sketch: the inclusion ⊆ is justified by saying that poppush(L) adds strings with pop(v)push(v) pairs that 'precisely match the possible additional values in the stack.' This is not a routine detail: the converse inclusion requires showing, for every residual context of stack values below the explicit stack content, that an inserted pop-push word makes the exact-stack semantics reach the same output. Please provide a full proof, for example by induction on the length of the residual stack, making explicit how the closure rules in Figure 4 supply the required words.","section":"Section 3.4, Lemma 3.10"},{"comment":"The decidability of full StacKAT is a headline result, but the proof of Lemma 4.3 is only summarized as proving two inclusions by induction, and Theorem 4.2 is described as 'entirely analogous' to Theorem 3.7. The header-annotated trace semantics introduces a genuine interaction: tests and assignments are compiled into automaton states, so the adaptation of Lemmas 3.9 and 3.10 to the annotated setting must be shown explicitly. Please give the full inductive proof of Lemma 4.3 and spell out how the canonicalization lemmas transfer to the pairs (α1, α2), rather than leaving the transfer to analogy.","section":"Section 4, Theorem 4.2 and Lemma 4.3"}],"minor_comments":[{"comment":"The finiteness argument for the trace automaton says the automaton steps only to expressions of the form e1·e2···ek where 'each ei is strictly smaller than ei+1,' but the ordering is not defined; please state the measure on expressions explicitly.","section":"Section 4.1"},{"comment":"The claim that (push(3)^n)*·(pop(3)^m)* is equivalent to (push(3)^gcd(n,m))* + (pop(3)^gcd(n,m))* is stated without proof; if kept, add a reference or a short derivation.","section":"Section 3.2"},{"comment":"The benchmark descriptions do not report the size of the value domain V, the number of header fields, or the hardware used; please include these details for reproducibility.","section":"Section 5.1"},{"comment":"There is a duplicated phrase in 'Below, we review below the most closely related work'; please fix the typo.","section":"Section 7"},{"comment":"The bar/overline notation for Lbar and a-bar is easy to lose in print, especially when it distinguishes push and pop letters; consider using a more robust notation such as subscripted or bracketed symbols.","section":"Throughout"}],"recommendation":"major_revision","confidential_remarks":"The paper is strong and the central decidability claim appears defensible, but the bisimilarity wording in Theorem 3.12 is formally incorrect for the NFAs actually constructed, and Lemma 3.10 needs a real proof, not a sketch. My impression is that the bisimilarity issue is a wording slip because Sections 3.5 and 5.1 use language equivalence, and the lemma is likely repairable; still, both points must be fixed before the paper can be accepted. I have no concerns about novelty or scope for PLDI."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"NetKAT gets a stack, and the paper shows equivalence is decidable anyway. That's the real story, and it's a substantial result. The zipping canonicalization—reading pop/push traces from the middle outward—is the key technical trick, and the reduction from full StacKAT to the push-pop fragment via per-header trace languages is clean. The PSPACE/EXPSPACE bounds and the completeness proof with the † operator are serious work. This is not a thin idea; it deserves a careful referee.\n\nBut there is a genuine bug in the stated algorithm. Theorem 3.12 tells you to 'check bisimilarity' of the resulting NFAs after zipping and pop-push closure. For NFAs, bisimilarity is strictly stronger than language equivalence. Two automata can accept the same language and not be bisimilar. The paper's own complexity argument (Section 3.5) and the implementation (Section 5.1) both use language equivalence, so the theorem statement appears to be a mistake—but as written, the decision procedure is incomplete. You cannot fix this by waving at 'bisimilarity'; you need either determinization (which would blow up the PSPACE bound) or an explicit language-equivalence check, or a proof that the canonical automata are deterministic or somehow bisimilarity coincides with language equivalence. No such proof is given. This is a load-bearing soft spot.\n\nThe other flagged point, Lemma 3.10, is underproved but looks repairable. The poppush closure is designed exactly to add the pop/push pairs that match arbitrary stack residues; the sketch is plausible, but in a paper where the main theorem depends on it, a two-sentence proof is thinner than it should be. I'd ask for a full proof in the appendix.\n\nThe axiom system with † is unusual and the completeness proof is intricate; I did not find an obvious hole there. The citation pattern is appropriate, with the VPL/DPDA/one-counter comparisons making the incomparability claim concrete. No code or data shipped, so the prototype claim is just a demo; not a problem for a theory paper.\n\nWho is this for? People working on NetKAT, network verification, and algebraic language theory. It will move the NetKAT line forward and should be published if the algorithmic gap is closed. I'd accept it for peer review, but with the expectation that Theorem 3.12 gets fixed and Lemma 3.10 gets a real proof.","headline":"StacKAT is a genuine theoretical advance for network verification, but the decision procedure as stated has a correctness gap (bisimilarity vs language equivalence) that needs fixing before the main decidability theorem is trustworthy.","tokens_in":35094,"tokens_out":3064,"would_cite":true,"duration_ms":27562,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q45","68Q60","68M12"],"pacs":[],"model":"deepseek-v4-flash","headline":"StacKAT adds a stack to NetKAT and still makes program equivalence decidable","keywords":["StacKAT","NetKAT","network verification","program equivalence","decision procedure","stack automata","Kleene algebra","pushdown languages"],"falsifier":"Search small value domains for two push-pop programs whose canonical trace automata accept the same language but whose input-output relations differ on some stack, e.g., by exhaustive enumeration of programs up to modest size; the paper's Theorem 3.7 predicts none exists. A more targeted check verifies Lemma 3.10 directly by computing $[\\bar L]$ and $[\\bar L]'$ for a collection of canonical languages and comparing them.","tokens_in":34001,"feed_emoji":"⚖️","tokens_out":4504,"duration_ms":38518,"temperature":0.7,"pith_summary":"StacKAT extends the network verification language NetKAT with push and pop operations on a packet stack, so programs can model parsing, source routing, telemetry, tunneling, and MPLS. The paper's central claim is that equivalence of such programs remains decidable even though the stack gives them infinitely many states. The proof works by reading each program as a regular expression over push and pop actions, then canonicalizing its trace language: cancel matching push-pop pairs, discard mismatched ones, and add pop-push pairs that are semantically invisible. Two programs are equivalent exactly when their canonicalized trace languages agree, and the canonical languages are regular enough to compare by finite automata. A complete axiomatization is given for the push-pop fragment.","feed_headline":"Stack-tossing network programs get a decidable equivalence check","feed_subtitle":"Push/pop on packet stacks stays verifiable: canonical trace automata decide equality and hand back counterexamples.","key_machinery":"The load-bearing object is the canonicalized trace language $\\bar L(e)$, produced in three steps: (1) pushpop closure adds shortcuts for matching $\\mathrm{push}(v)\\cdot\\mathrm{pop}(v)$; (2) filtering intersects with $\\mathrm{pop}^*\\mathrm{push}^*$, keeping only traces where all pops precede all pushes; (3) poppush closure inserts $\\mathrm{pop}(v)\\cdot\\mathrm{push}(v)$ pairs, implemented on automata by zipping the trace from the middle outward, representing a word $\\mathrm{pop}(1)\\mathrm{pop}(2)\\mathrm{push}(3)\\mathrm{push}(4)$ as $(\\mathrm{pop}(2),\\mathrm{push}(3))(\\mathrm{pop}(1),\\mathrm{push}(4))$, and prepending $((\\mathrm{pop}(v),\\mathrm{push}(v)))^*$. The zipped automaton makes the otherwise non-regular poppush closure regular, so language equivalence of the resulting automata is decidable and yields counterexamples.","core_discovery":"The paper establishes Theorem 3.7: for push-pop StacKAT programs $e,f$, semantic equivalence $\\llbracket e\\rrbracket=\\llbracket f\\rrbracket$ holds iff $\\bar L(e)=\\bar L(f)$, where $\\bar L=\\mathrm{poppush}(\\mathrm{filter}(\\mathrm{pushpop}(L)))$. It extends this to full StacKAT via trace languages $\\mathrm{traces}^{\\alpha_2}_{\\alpha_1}(e)$ for each input/output packet-header pair $(\\alpha_1,\\alpha_2)$, giving Theorem 4.2 and a decision procedure in EXPSPACE (Theorem 4.5), with PSPACE-completeness for the push-pop fragment (Theorems 3.13 and 3.14). For push-pop programs the paper also gives a complete equational axiomatization (Theorem 6.9): Kleene algebra plus $\\mathrm{push}(v)\\mathrm{pop}(v)=1$, $\\mathrm{push}(v)\\mathrm{pop}(w)=0$ for $v\\neq w$, the inequality $\\mathrm{pop}(v)\\mathrm{push}(v)\\le 1$, and a rule that transfers provability through a new operator $\\dagger$.","pith_inferences":["The zipping construction may generalize: any action language whose valid traces form $\\mathrm{pop}^*\\mathrm{push}^*$ can be decided by reading from the middle outward, which could apply to other stack-like models beyond network packets.","The paper's contrast with visibly pushdown languages suggests a broader lesson: removing the input tape while keeping an unrestricted stack is what buys decidability, so similar tape-less stack models elsewhere may also have decidable equivalence.","A symbolic implementation, e.g., BDD-style as the paper leaves to future work, would be the natural test of whether the EXPSPACE procedure scales to realistic header spaces; the paper's own benchmarks show header enumeration is the bottleneck."],"forward_implications":["Every StacKAT equivalence query, such as reachability, waypointing, correct compilation, and slice isolation, can be answered mechanically instead of by hand.","Inequivalent programs come with an explicit input-output packet pair witnessing the difference, computed from the symmetric difference of the canonical automata.","The push-pop fragment has a sound and complete axiomatization, so equivalence proofs can be carried out equationally as well as algorithmically.","Full StacKAT equivalence is EXPSPACE-complete, matching the hardness of regular expressions with squaring; with a fixed set of header variables the bound drops to PSPACE."],"supporting_citations":[{"why":"Supplies the NetKAT language and semantics that StacKAT extends.","marker":"[2]"},{"why":"Provides the Antimirov partial-derivative construction used to build NFAs from regular expressions.","marker":"[3]"},{"why":"Provides Brzozowski derivatives, the basis of the normal-form transformation and completeness proof.","marker":"[8]"},{"why":"Gives the coalgebraic NetKAT decision procedure that StacKAT builds on and generalizes.","marker":"[12]"},{"why":"Provides the completeness theorem for Kleene algebra used in the axiomatization.","marker":"[19]"},{"why":"Yields EXPSPACE-hardness for regular expressions with squaring, which is reduced to full StacKAT.","marker":"[23]"}],"fun_headline_variants":["StacKAT: infinite-state stack programs get decidable equality","Push-pop network verification now decidable via automata","StacKAT proves stack-program equivalence in EXPSPACE","Decidable equivalence for infinite-state network stacks","Stacked network logic: decidable equality, complete axioms"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The argument assumes that inserting pop-then-push pairs in the middle of canonical traces captures exactly the behavior of stacks with extra values underneath, so that no semantic difference is lost in the canonicalized language.","fun_headline_variants_meta":{"raw":{"variants":["StacKAT: infinite-state stack programs get decidable equality","Push-pop network verification now decidable via automata","StacKAT proves stack-program equivalence in EXPSPACE","Decidable equivalence for infinite-state network stacks","Stacked network logic: decidable equality, complete axioms"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000732,"raw_usage":{"total_tokens":3268,"prompt_tokens":932,"completion_tokens":2336,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":548,"completion_tokens_details":{"reasoning_tokens":2269}},"tokens_in":548,"tokens_out":2336,"duration_ms":16137,"temperature":1.0,"reasoning_tokens":2269,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T20:03:40.813978+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Search small value domains for two push-pop programs whose canonical trace automata accept the same language but whose input-output relations differ on some stack, e.g., by exhaustive enumeration of programs up to modest size; the paper's Theorem 3.7 predicts none exists. A more targeted check verifies Lemma 3.10 directly by computing $[\\bar L]$ and $[\\bar L]'$ for a collection of canonical languages and comparing them.","supporting_citations":[],"review_version":2}