CFGKAT: A Complete Calculus for Non-Local Control Flow

CFGKAT is an extension of guarded Kleene Algebra with Tests (GKAT) that adds non-local control flow (e.g., break, goto) while maintaining an efficient decision procedure. An axiomatization of equivalence for CFGKAT presents unique barriers created by the presence of non-local control flow and contextual semantics of goto which compromises compositional reasoning. In this paper, we overcome these barriers and present a sound and complete axiomatization of program equivalence in CFGKAT. We verify the loop case of the Erosa-Hendren goto elimination algorithm, a difficult syntactic metatheorem which requires reasoning about fixpoints, control-flow contexts, and mutable state. We mechanize the metatheory and case study in Rocq.