{"id":"05183fbe-0c3c-47ee-b0a9-d59a14c655c7","arxiv_id":"2411.13220","paper_version":2,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"CF-GKAT is an extension of Guarded Kleene Algebra with Tests that soundly and completely checks trace equivalence of programs with non-local control flow and a restricted 'indicator' variable, in nearly linear time.","lead":"This paper extends an algebra for program equivalence (GKAT) so it can handle goto, break, return, and a restricted kind of variable assignment. The result is an efficient checker that can validate decompiler and goto-elimination transformations, tested on C code from GNU Coreutils.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Definition 3.11's lowering rule only resolves jmp(ℓ,i) with the current indicator, yet Example 3.6 emits jmp(ℓ,1) from indicator 2, leaving δ↓ ill-typed; the central algorithm as printed is not well-defined.","rationale":"The reader's weakest assumption (isolation of the indicator variable) is a real applicability limitation, but it is explicitly stated and scoped in the paper; it does not threaten the soundness and completeness theorem for the class of accepted inputs. The more immediate correctness risk is Definition 3.11: the lowering operation is the bridge from CF-GKAT automata to GKAT automata, and the printed rule is inconsistent with the paper's own Example 3.6, which produces a jump continuation whose target indicator differs from the current indicator. As written, the resulting δ↓ is not a well-typed GKAT transition function, so the algorithm announced by the central claim is not actually defined. This is a concrete, checkable defect in the presentation rather than a disagreement with the underlying approach; the Coq formalization likely uses the repaired version. The unproved fresh-indicator-value lemma is a smaller gap: it is plausible and easily supplied by induction. Overall, conditional acceptance remains appropriate, pending a corrected Definition 3.11 and confirmation from the artifact.","tokens_in":29026,"tokens_out":18944,"duration_ms":215753,"concrete_test":"Open the Coq artifact (DOI 10.5281/zenodo.13938565) and inspect the lower function corresponding to Definition 3.11. Check whether it matches jmp(l,j) for an arbitrary target indicator j and resolves it with λ↓(l,j,a); if so, the printed rule is a typo and the central theorem stands. Independently, instantiate Example 3.6 with I={1,2} and lower the state (ŝ,2): under the printed rule, δ↓((ŝ,2),{t}) is not in the GKAT codomain, so any executable implementation of the printed algorithm should be ill-typed or reject the transition.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Definition 3.11, as printed, does not define a GKAT transition function. Its first clause resolves a jump only when δ(s,i,α)=jmp(ℓ,i), i.e., when the continuation's target indicator equals the current indicator of the state. But Example 3.6's automaton explicitly returns jmp(ℓ,1) from input (2,{t}): the else branch x:=1; gotoℓ is compressed into a single jmp continuation with a new indicator value. So a jump with j≠i arises in the paper's own example. In that case δ′ keeps the jmp, and the 'otherwise' branch of δ↓ returns δ(s,i,α), a CF-GKAT dynamics, rather than an element of ⊥+⊤+Σ×(S×I). Thus A↓i is not well-formed. Even setting that aside, the second step of Definition 3.11 writes δ(s,i,α) where it must be δ′(s,i,α). Theorem 3.13 and the soundness/completeness corollary depend on this lowering, so the central algorithm as written is not established. If the intended rule is jmp(ℓ,j) resolved by λ↓(ℓ,j,α), the construction is repairable and the Coq development likely already does this, but the paper text needs correction.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces CF-GKAT, an extension of Guarded Kleene Algebra with Tests (GKAT) that adds indicator variables and non-local control flow (goto, break, return). It defines a continuation semantics for CF-GKAT expressions, presents CF-GKAT automata, and shows how to lower these automata to GKAT automata so that trace equivalence can be decided by the existing nearly-linear-time GKAT algorithm. The authors report a Coq formalization of the main theorems and demonstrate the approach on a decompilation case study (Ghidra) and a goto-elimination transformation (Calipso) applied to a function from GNU Coreutils.","tokens_in":29315,"tokens_out":11844,"duration_ms":118284,"significance":"If the printed constructions are corrected, this is a solid and useful contribution: it enlarges the class of programs that can be checked for trace equivalence in nearly linear time, while keeping the decision procedure sound and complete. The explicit reduction to GKAT equivalence is elegant, the machine-checked Coq development is a major strength, and the case study on real control-flow transformations gives evidence of practical applicability. The main caveat is that the paper text currently contains definitional errors in two load-bearing places, so the central algorithm as printed is not yet established.","major_comments":[{"comment":"The second rule of the sequencing operation copies every trace of G whose continuation lies in {brk_i, acc_i, jmp(ℓ,i)}. Including acc_i is inconsistent with the stated purpose of the rule (preserving non-local control flow) and with the neutrality of labels: with this rule, assert true; assert false would contain the trace α·acc_i, and while true do assert true would spuriously contain α·acc_i via Definition 2.13. The set should be {brk_i, ret, jmp(ℓ,i)} (with the indicator values handled as in the examples), since accepting traces must be composed with H, not copied.","section":"Definition 2.9"},{"comment":"The lowering is not well-defined as printed. The first clause of δ′ resolves a jump only when δ(s,i,α)=jmp(ℓ,i), but Example 3.6 has δ(ŝ,2,{t})=jmp(ℓ,1), so a jump with j≠i arises in the paper's own example. In that case δ′ keeps the jump, and the final 'otherwise' clause of δ↓ returns δ(s,i,α) — also a typo for δ′(s,i,α) — which is a CF-GKAT continuation rather than an element of ⊥+⊤+Σ×(S×I). The intended rule should resolve δ(s,i,α)=jmp(ℓ,j) by λ↓(ℓ,j,α), and δ↓ should use δ′ in its final clause. Since Theorem 3.13 and the equivalence algorithm depend on this construction, the printed definition must be corrected.","section":"Definition 3.11"},{"comment":"The restriction of the indicator set to the values occurring in e and f plus one fresh value relies on the claim that if neither i nor i′ appears in e, then ⟦e⟧ℓ_i = ⟦e⟧ℓ_i′ for all labels ℓ. This lemma is stated as 'not hard to show' but is load-bearing for the completeness of the algorithm. Please state it as a lemma and provide a proof or an explicit reference to the corresponding Coq statement.","section":"Section 3.5"}],"minor_comments":[{"comment":"Definition 2.2 writes pairs in ⟦−⟧ as (i,α), but Example 2.3 lists ({t1,t2},2), ({t1},2), (∅,2), reversing the order. Please make the notation consistent.","section":"Definition 2.2 and Example 2.3"},{"comment":"The final equivalence chain and the sentence 'Therefore e and f are trace equivalent if and only if equivGKAT(e,f) returns true' should refer to equivCFGKAT, not equivGKAT.","section":"Section 3.5"},{"comment":"In the paragraph on trace equivalence, 'the assignment of x is different at the end of the so' should read 'at the end of the program'.","section":"Section 5.2"},{"comment":"The remark about converting do-while loops says the conversion is admissible when the loop body does not contain break or a label; please clarify whether this condition is checked by the tool or assumed by the front-end.","section":"Section 4.1"}],"recommendation":"major_revision","confidential_remarks":"The Definition 2.9 and Definition 3.11 issues are of different natures: the former appears to be a typo that nevertheless changes the semantics if read literally, while the latter is an inconsistency between the printed lowering rule and the paper's own example. Both are likely fixed in the Coq development, but the text must be corrected before the paper can be accepted. The case study is honest about its manual adjustments, and the complexity claims are plausible once the printed definitions are repaired."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick take: this is a real step forward. CF-GKAT adds indicator variables and non-local control flow to GKAT, and gives a decision procedure by lowering to GKAT automata, with the whole thing formalized in Coq. The resolution of Kozen's open question is genuine, and the Thompson-style construction and lowering are the right tools. The paper is worth a serious referee.\n\nWhat's good: the continuation semantics is clean, the automaton model is natural, and the proof sketches match what I'd expect from a Coq development. The empirical section is honest about its limitations, even if the abstract oversells 'several transformations' when the body reports two transformations on one function.\n\nNow the soft spots. The stress-test note is right: Definition 3.11 as printed is not well-typed. The first clause only resolves a jump jmp(ℓ,i) when the target indicator equals the current state's indicator. But Example 3.6 explicitly produces jmp(ℓ,1) from state (ŝ,2), so the lowering leaves a continuation in the GKAT transition function, which is not an element of ⊥+⊤+Σ×(S×I). The otherwise branch also refers to δ instead of δ′. These look like typos in the write-up, not errors in the Coq formalization, but they make the central algorithm as printed undefined. A reader cannot implement the algorithm from the text as it stands.\n\nThe second issue is the fresh indicator value lemma: the text asserts that if neither i nor i′ appears in e then the behaviors coincide, and calls it 'not hard to show' — a proof sketch or a pointer to the Coq file would be better. Also, the experiments required manual adjustments (propagating assignments, simplifying Boolean expressions, changing types), which the paper acknowledges. The indicator-isolation assumption is restrictive but clearly stated. These are addressable and don't undermine the main contribution.\n\nThe intended audience is the PL/verification community, especially anyone building decompiler or refactoring validators. Bottom line: the theory is sound, the Coq artifact is the real evidence, and the paper deserves peer review and likely acceptance after a revision that fixes Definition 3.11 and tones down the abstract. I'd send it to referees.","headline":"Solid, Coq-verified theory; the printed lowering definition has a typo that makes it ill-typed, but the underlying result looks right and deserves a referee.","tokens_in":29830,"tokens_out":5197,"would_cite":true,"duration_ms":47625,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q60","68Q45","03B70"],"pacs":[],"model":"deepseek-v4-flash","headline":"CF-GKAT decides trace equivalence of programs with goto, break, and return soundly and completely in nearly-linear time.","keywords":["control-flow equivalence","guarded Kleene algebra with tests","indicator variables","non-local control flow","trace equivalence","goto elimination","decompiler validation","continuation semantics"],"falsifier":"Compute, by the explicit definitions in the paper, the trace language of the goto-based program and of the break-based loop from the introduction over one test and a two-valued indicator set: this is a finite enumeration of guarded words, and any guarded word present in one language but not the other would refute the claim that CF-GKAT equates the two. A sharper boundary test targets completeness: the algorithm assumes that starting indicator values absent from both programs all behave alike, so any expression whose traces depend on which absent value it starts from would produce a false equivalence verdict.","tokens_in":28826,"feed_emoji":"✅","tokens_out":18874,"duration_ms":173899,"temperature":0.7,"pith_summary":"CF-GKAT extends guarded Kleene algebra with tests (GKAT) — an algebraic framework that equates programs whenever the same test outcomes always lead to the same sequence of uninterpreted actions — with two capabilities GKAT lacked: indicator variables, a single value programs can set and test, and non-local control flow (goto, break, return). The paper aims to make automatic trace-equivalence checking usable for real control-flow transformations, such as goto-elimination, decompiler loop structuring, and rewrites into single Böhm-Jacopini loops, where the interesting question is whether two very differently written programs always take the same action path. Its central claim is that trace equivalence of CF-GKAT programs is decidable soundly and completely by reducing it to GKAT automaton bisimulation, with cost roughly $|I|^2 \\times (|e|+|f|)$ — nearly linear in program size when the test alphabet is fixed. To back the claim, the paper's checker validates the output of a goto-elimination tool and of the Ghidra decompiler on a function from GNU Coreutils. A sympathetic reader should care because this offers a fast, automatic way to certify that control-flow-manipulating tools preserve observable behavior.","feed_headline":"Checking goto-heavy code now runs in near-linear time","feed_subtitle":"CF-GKAT proves decompiler and goto-removal output matches the original program.","key_machinery":"The argument is carried by two intermediate objects. The first is the continuation, a tag attached to each guarded word that records how control proceeds after that trace ends: $\\mathrm{acc}_i$ (normal termination with indicator value $i$), $\\mathrm{brk}_i$ (break out of the enclosing loop), $\\mathrm{ret}$ (return from the whole program), or $\\mathrm{jmp}(\\ell,i)$ (continue at label $\\ell$). Tagging traces this way lets the otherwise non-compositional constructs goto, break, and return get an inductive semantics, with jump resolution deferred until the whole program is known. The second is the CF-GKAT automaton: a transition function of type $I \\times \\mathrm{At} \\to \\bot + C + \\Sigma{\\times}S{\\times}I$ together with a jump map assigning a transition to every label. Expressions compile to these automata by a Thompson-style construction whose iterated start dynamics handles the subtle case where a loop body changes the indicator value without executing any action. Lowering to GKAT automata is the reduction that does the work: indicator values become part of the state, jumps are resolved by iterating the jump map (cycles become rejection), break continuations become rejection, and return becomes acceptance — after which the existing GKAT bisimulation check decides the question.","core_discovery":"The paper's central claim is that the procedure equivCFGKAT decides trace equivalence exactly: for CF-GKAT programs $e$ and $f$ it returns true precisely when the two programs have the same guarded-language semantics — for every initial truth assignment to the primitive tests and every starting indicator value, they execute the same sequence of uninterpreted actions in the same order. The procedure converts each program into a CF-GKAT automaton by a Thompson-style construction that preserves an intermediate continuation semantics, lowers each automaton to a GKAT automaton by embedding indicator values into the state space and resolving jump continuations through the label map, and runs the existing GKAT bisimulation check for every starting indicator value (including one fresh value not appearing in either program). Soundness and completeness follow from two theorems — the Thompson construction preserves the continuation semantics, and lowering commutes with semantic jump resolution — both backed by a machine-checked formalization; the equivalence checks cost on the order of $|I|^2 \\times (|e|+|f|)$ and automaton construction about $|L|\\times|I| + |I|\\times(|e|+|f|)$, so the method inherits GKAT's near-linear complexity.","pith_inferences":["The framework's natural sweet spot is compiler-generated control flow, where a 'mode' or 'state' variable is written only by dispatcher assignments and read only by dispatcher tests; a testable extension is to measure how many functions in a large C corpus admit such an isolated variable without rewriting.","The construction extends in a straightforward way to several indicator variables, since the semantics is indexed by the indicator set; the cost would multiply by the product of the value sets, which would cover structuring passes that introduce more than one state variable.","A consequence the paper leaves implicit is that an infinite loop that only cycles through indicator values is identified with outright rejection, since the jump-resolution fixed point returns $\\bot$ on cycles; users who care about termination-sensitive transformations should notice this identification.","The practical bottleneck is the front-end: choosing which C variable is the indicator and normalizing decompiler artifacts (value masking, temporary-assignment propagation) were done by hand in the case study, and automating those steps is what would determine how broadly the method applies."],"forward_implications":["Decompiler and refactoring tooling gains an automatic oracle for control-flow-preserving rewrites: the paper's checker validates both a goto-elimination pass and Ghidra's control-flow structuring of a compiled GNU Coreutils function, each in under a second.","The decidable class extends from while-programs to programs with goto, break, return, and assignments of hardcoded values to an isolated variable — covering pseudo-assembly input, decompiled code, and single-loop normal forms from the Böhm-Jacopini construction.","Trace-equivalence checking keeps GKAT's efficiency: with the test alphabet fixed, the algorithm is nearly linear in the sizes of the two programs and linear in the number of labels, with cost quadratic only in the number of indicator values.","The automaton construction answers an open question in the Kleene-algebra literature about whether non-local control flow can be handled directly, by compiling expressions to automata rather than first encoding gotos away.","Because the final indicator value is invisible in the trace semantics, CF-GKAT equates programs that differ only in their final indicator value, and the resulting equivalence is not a congruence: programs must be compared as wholes, not in arbitrary contexts."],"supporting_citations":[{"why":"Supplies the GKAT automata, the near-linear bisimulation decision procedure, and the Thompson-style construction that CF-GKAT generalizes and lowers into.","marker":"[41]"},{"why":"Defines guarded languages and their sequencing (the coalesced product) that the CF-GKAT continuation semantics extends.","marker":"[27]"},{"why":"Poses the open question of treating non-local control flow directly rather than via KAT encodings, which the CF-GKAT automaton construction answers.","marker":"[23]"},{"why":"The goto-elimination procedure whose output the checker validates in the experimental section.","marker":"[16]"},{"why":"The Böhm-Jacopini single-loop construction that CF-GKAT must equate with goto- and break-based programs.","marker":"[7]"},{"why":"The classic regular-expression-to-automaton construction that the expression-to-CF-GKAT-automaton translation generalizes.","marker":"[45]"},{"why":"The artifact containing the machine-checked proofs of the lowering and Thompson-correctness theorems that ground soundness and completeness.","marker":"[51]"}],"fun_headline_variants":["Near-linear equivalence checking for programs with goto","Exact trace equivalence for non-local control flow","Validating control-flow transformations in near-linear time","CF-GKAT: proving decompiler and goto-elimination correctness","Machine-checked verification of goto elimination and decompilation"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"Everything rests on the premise that the indicator variable never appears in any primitive test or action, so it is purely a control-flow value — if the program's key variable is read or written by other operations, CF-GKAT's semantics no longer describes the program and the checker's verdict is meaningless for it.","fun_headline_variants_meta":{"raw":{"variants":["Near-linear equivalence checking for programs with goto","Exact trace equivalence for non-local control flow","Validating control-flow transformations in near-linear time","CF-GKAT: proving decompiler and goto-elimination correctness","Machine-checked verification of goto elimination and decompilation"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00054,"raw_usage":{"total_tokens":2623,"prompt_tokens":1015,"completion_tokens":1608,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":631,"completion_tokens_details":{"reasoning_tokens":1546}},"tokens_in":631,"tokens_out":1608,"duration_ms":14477,"temperature":1.0,"reasoning_tokens":1546,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T16:41:13.887294+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Compute, by the explicit definitions in the paper, the trace language of the goto-based program and of the break-based loop from the introduction over one test and a two-valued indicator set: this is a finite enumeration of guarded words, and any guarded word present in one language but not the other would refute the claim that CF-GKAT equates the two. A sharper boundary test targets completeness: the algorithm assumes that starting indicator values absent from both programs all behave alike, so any expression whose traces depend on which absent value it starts from would produce a false equivalence verdict.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Poses the open question of treating non-local control flow directly rather than via KAT encodings, which the CF-GKAT automaton construction answers."},{"cited_title":"Narvaéz, and Nico Naus","cited_arxiv_id":null,"evidence_quote":"The artifact containing the machine-checked proofs of the lowering and Thompson-correctness theorems that ground soundness and completeness."}],"review_version":1}