{"id":"a1e8de77-e905-4874-b652-4fe1c9f35749","arxiv_id":"2509.06872","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Rocq-checked soundness and completeness of meta-configuration tracking, plus a verified end-to-end linearizability proof for a concurrent register.","lead":"This paper reports a machine-checked formalization of the soundness and completeness of meta-configuration tracking, a forward reasoning technique for proving linearizability of concurrent data structures. If correct, it lets users of the technique build end-to-end verified proofs of linearizability without trusting an unmechanized metatheory.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 1's Rocq statement omits the WF_aug hypothesis, making it false as written; the proof relies on well-formedness.","rationale":"The central claim rests on Theorem 1. The displayed formal statement is inconsistent with the informal 'every augmented run admitted by that implementation' and with the proof, which uses well-formedness to derive `tracker(c) = evolve ...`. Since arbitrary runs with empty trackers are allowed by the inductive definition, the statement as written is false. This is a concrete internal error, not a disagreement about the standard definition. It may be fixable by adding the `WF_aug r` hypothesis, but until the artifact is available and the statement corrected, the paper's main theorem cannot be taken as established. The reader's concern about the unmechanized Lynch equivalence is also valid, but the missing hypothesis is more immediate. I therefore leave the verdict as CONDITIONAL (UNCHANGED) with an additional explicit condition on the artifact.","tokens_in":14906,"tokens_out":15418,"duration_ms":170179,"concrete_test":"Inspect the Rocq artifact for the exact `adequacy` statement. If it is `∀r, WF_aug r → ∃σ f, ...`, confirm the paper text is a typo; if it is genuinely `∀r, ∃σ f, ...`, refute it by constructing `Initial c` with `tracker = ∅` and showing the right side fails. Also check whether Lemma 2 is stated with `WF_aug r`.","verdict_should_be":"UNCHANGED","load_bearing_attack":"In §4, the formal statement of Theorem 1 is `Theorem adequacy : linearizable impl ↔ ∀r, ∃σ f, (final r).(tracker) σ f`. But `run` (§3.1) is an inductive type whose `Initial` and `Step` constructors accept arbitrary configurations `c`. Ill-formed runs therefore exist, e.g. `Initial c` where `c` has an empty `tracker`; for such `r`, `(final r).(tracker) σ f` is false, making the right-hand side false for every implementation. The proof of Lemma 2 explicitly assumes `r` is well-formed (`WF_aug r`) to justify `tracker(c) = evolve π l M(r)`; without this hypothesis the induction fails. Thus the displayed theorem is either a typo (missing `WF_aug r`) or, if mechanized exactly as written, refutable. This is the most load-bearing issue because it concerns the precise statement of the central adequacy claim, before considering the cited Lynch equivalence.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper claims to mechanize in Rocq the metatheory of meta-configuration tracking, a forward-reasoning technique for proving linearizability introduced by Jayanti et al. It formalizes a small concurrent language, an implementation semantics, a Lynch-style behavior-based definition of linearizability, augmented runs with tracker state, and states an Adequacy theorem (Theorem 1) connecting linearizability to the inhabitedness of trackers. It also reports a case study: an end-to-end proof of linearizability for a read/write register implemented with read and CAS. The paper contains informal proof sketches, Rocq snippets, and claims that all proofs are mechanized in about 3250 lines of Rocq, but it provides no artifact, repository link, or commit hash.","tokens_in":15107,"tokens_out":5734,"duration_ms":67773,"significance":"If fully machine-checked, this would be a valuable contribution: it would be the first mechanized proof of soundness and completeness for the meta-configuration tracking technique, and the first end-to-end linearizability proof built on that metatheory. The formalization is careful in many places—the run semantics, the distinction between implementation runs and atomic runs, and the inductive definition of well-formedness are all concrete, and the paper explicitly names the key adequacy theorem and its two directions. The register case study is well chosen because it illustrates future-dependent linearizability. However, the absence of a machine-checked artifact and the incomplete informal proofs prevent the reader from verifying the central claim as presented.","major_comments":[{"comment":"The displayed Rocq statement `Theorem adequacy : linearizable impl ↔ ∀r, ∃σ f, (final r).(tracker) σ f` is false as written. Because the type `run` (§3.1) admits `Initial c` for arbitrary configurations `c`, choose `r = Initial c` where `c`'s tracker is empty; then `(final r).(tracker) σ f` is false for all σ and f, making the right-hand side false even for a linearizable implementation. The informal proof of Lemma 2 also says \"Because we assume that r is well-formed,\" but the lemma statement says \"arbitrary augmented run r.\" The theorem must be quantified over well-formed augmented runs, e.g. `∀r, WF_aug r → ...`, and the formal statement must match the proof. This is a load-bearing issue for the central adequacy claim.","section":"§4, Theorem 1"},{"comment":"The paper's central claim is that all proofs are \"fully mechanized in Rocq,\" but no development is provided: there is no repository URL, commit hash, buildable artifact, or even a listing of the main proof files. Section 6 states that the mechanization amounts to about 3250 lines of Rocq, but gives the reader no way to inspect, reproduce, or check that claim. In a mechanized-metatheory paper, the artifact is essential evidence. Please provide a public artifact and a clear mapping from the paper's theorem and lemma names to the corresponding Rocq definitions and proofs.","section":"§6, Mechanization"},{"comment":"The completeness direction of Adequacy is load-bearing: Theorem 1's reverse direction depends on Lemma 3, which asserts that every linearization's final atomic configuration appears in the tracker. However, the paper says only \"For brevity, we omit an informal proof of completeness here.\" No artifact is available to supply the missing details. As a result, the completeness half of the central theorem is unsupported in the manuscript. Please include an informal proof or a detailed proof sketch, and ensure the artifact contains the complete machine-checked proof of Lemma 3.","section":"§4, Lemma 3"},{"comment":"The formal predicate `linearizable` is defined as: every well-formed implementation run has behavior syntactically equal to the behavior of some well-formed atomic run. This is not the original Herlihy-Wing definition; the paper cites Lynch's Theorems 13.4 and 13.5 for the equivalence, but that equivalence is not mechanized. Since the abstract emphasizes \"verified end-to-end proofs of linearizability\" and \"reducing the trusted computing base,\" this unmechanized equivalence remains in the trusted base. Please either mechanize the equivalence, or explicitly state that the end-to-end result is for the behavior-based (Lynch) notion of linearizability.","section":"§3.4, Linearizability"}],"minor_comments":[{"comment":"In defining the base object type, the text says \"Define OP RWCELL to be {Read, CAS}\", but this should be `OP_RCASCELL`, the operation set for the compare-and-swap cell.","section":"§5, object definitions"},{"comment":"The Step-Invoke rule has a stray trailing comma in its conclusion: `⟨σ,[Pendingop arg/π]f,⟩`. It should be `⟨σ,[Pendingop arg/π]f⟩`.","section":"Figure 5"},{"comment":"Minor typos: \"extenstionally\" should be \"extensionally\" in §6, and \"asychronous\" should be \"asynchronous\" in §7.","section":"§6 and §7"},{"comment":"The paper uses CVIT 2016 template placeholders (conference name, DOI `10.4230/LIPIcs.CVIT.2016.23`, page numbering). These should be updated to the actual venue and DOI before publication.","section":"Template and front matter"},{"comment":"The informal soundness proof omits the Intermediate and Response cases after saying they are similar and \"included in the mechanization.\" Without the artifact, these cases are not inspectable; even an informal treatment of the Response case would help the reader.","section":"§4, Lemma 2 proof"}],"recommendation":"major_revision","confidential_remarks":"The absence of any artifact is the largest concern: a mechanized metatheory paper that does not ship the machine-checked proof cannot be accepted as evidence of the central claim. I would ask the editor to require a public artifact with a reproducible build before any acceptance, and to verify that the formal statement of Theorem 1 includes the well-formedness hypothesis. The remaining issues (missing completeness proof, unmechanized Lynch equivalence) are also load-bearing but are fixable in revision."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper's real contribution is the first Rocq mechanization of the meta-theory behind Jayanti et al.'s meta-configuration tracking: soundness and completeness of the adequacy theorem, plus a register case study that is genuinely end-to-end and future-dependent. That is useful and, if the artifact checks out, worth a serious referee. But as submitted, the central theorem is misstated and there is no artifact, so I can't endorse the current version.\n\nWhat's good: the formalization is coherent, the definitions (runs, well-formedness, behavior, linearizability, trackers) are laid out carefully, and the soundness/completeness proof outline follows a sensible induction. The register example is a good stress test because its linearization really is future-dependent, so it demonstrates the technique rather than just retreading a trivially linearizable example. Credit where due: this is the first mechanization of this particular metatheory and would shrink the TCB for this line of verification.\n\nThe soft spots are real. First, the Rocq statement of Theorem 1 in Section 4 is `linearizable impl <-> forall r, exists sigma f, (final r).(tracker) sigma f`. The `run` inductive type allows arbitrary ill-formed runs, e.g. `Initial c` with an empty tracker. Such a run makes the right side false regardless of the implementation, so as written the theorem is refutable. The proof of Lemma 2 explicitly uses `WF_aug r`; without that hypothesis the induction doesn't go through. The stress-test note about this is not a nitpick. I assume this is a typo in the write-up and not in the actual Rocq development, but it is load-bearing and must be fixed with an explicit `WF_aug r` (or by defining `final`/`tracker` only for well-formed runs).\n\nSecond, no artifact, build script, or commit hash is shipped. For a paper whose entire claim is \"fully mechanized,\" the absence of the development is a blocker for verification. Third, the completeness proof is omitted from the text. Fine if the artifact covers it, but it makes the paper hard to referee. Fourth, the equivalence between the formalized behavior-based linearizability and Herlihy-Wing is cited via Lynch Theorems 13.4/13.5, not mechanized. I think that's acceptable—it is a standard result—but the paper should state clearly that the end-to-end guarantee is relative to a provably equivalent formulation, not the exact H-W definition.\n\nBottom line: the underlying work is sound in intent, the method is worthwhile, and a corrected version with artifact deserves a serious referee. Don't desk-reject; send it out, but require the artifact and the fixed theorem statement before accepting.","headline":"A genuinely useful mechanization of Jayanti et al.'s meta-configuration tracking metatheory, but the submitted text misstates the central adequacy theorem (missing a well-formedness hypothesis) and ships no Rocq artifact, so it needs correction and artifact release before I'd trust the end-to-end claim.","tokens_in":15596,"tokens_out":3698,"would_cite":false,"duration_ms":39777,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Mechanized proof in Rocq certifies forward-reasoning linearizability end to end.","keywords":["linearizability","meta-configuration tracking","forward reasoning","mechanical verification","Rocq","concurrent data structures","future-dependent linearization","concurrent register"],"falsifier":"Inspect the Rocq proof term of Theorem adequacy: if its only assumptions are the paper's definitions, functional extensionality, and standard finite-map facts, the claimed mechanization is real; any hidden axiom or unverified use of Lynch's Theorems 13.4/13.5 would expose a trust gap. Separately, a concrete counterexample—an implementation whose tracker is inhabited in every admitted augmented run yet whose behavior differs from every atomic run—would directly refute soundness.","tokens_in":14809,"feed_emoji":"✅","tokens_out":6686,"duration_ms":66493,"temperature":0.7,"pith_summary":"Linearizability is the gold standard for concurrent data structure correctness, but machine-checked proofs of it are hard to obtain end to end. This paper formalizes meta-configuration tracking, the first sound and complete forward-reasoning technique for proving linearizability, and mechanizes its metatheory in the Rocq proof assistant. The central result, Theorem 1 (Adequacy), states that an implementation is linearizable if and only if the tracker of the final configuration of every augmented run it admits is inhabited. Both directions of this biconditional are machine-checked, and a concurrent register with a future-dependent linearization structure receives a fully verified end-to-end linearizability proof. If the paper is right, future linearizability proofs using this technique no longer need to trust an unmechanized soundness and completeness argument.","feed_headline":"Machine-checked theorem makes linearizability proofs end-to-end","feed_subtitle":"Meta-configuration tracking's adequacy is now verified in Rocq, closing the trust gap in forward-reasoning proofs.","key_machinery":"The central mechanism is meta-configuration tracking, with a 'tracker' as ghost state attached to each concrete configuration. The tracker holds the set of all atomic configurations that could be the final state of some linearization of the run so far. The evolve function updates this set on each executed line: invocations mark a process pending, responses discard atomic configurations whose linearized value does not match the returned value, and intermediate lines leave the set unchanged; a linearize_pending relation then closes the set under arbitrary sequences of pending operations taking effect. The multistep transition relation δ* is the load-bearing bridge that lets the proof maintain","core_discovery":"The paper's central claim is an adequacy biconditional: an implementation is linearizable exactly when, in every run augmented with ghost 'tracker' state, the final tracker contains at least one atomic configuration consistent with the run. Soundness says an inhabited tracker forces the existence of a linearization; completeness says every linearizable implementation keeps its tracker inhabited. The authors formalize runs, atomic runs, behavior equality, and the tracker's evolution function in Rocq, and they prove the biconditional as the theorem 'linearizable impl ↔ ∀r, ∃σ f, (final r).(tracker) σ f'. As an end-to-end demonstration, they build a machine-checked linearizability proof for a r","pith_inferences":["A natural next step is to mechanize the cited equivalence between the formalized atomic-run definition and Herlihy-Wing histories, which would close the remaining trust gap in the end-to-end guarantee.","The same tracker framework should generalize to other refinement-based correctness conditions, such as sequential consistency or set-linearizability, by changing the atomic dynamics and the evolve rules.","Because the tracker is a set rather than a single simulation, automated invariant discovery could target the tracker directly, offering a machine-checkable route to verifying more complex concurrent structures.","A stress test would be to replay the earlier TLAPS-verified examples, such as the Herlihy-Wing queue or union-find, inside this Rocq framework without trusting an unmechanized metatheory."],"forward_implications":["New linearizability proofs using meta-configuration tracking can now be checked end to end in a proof assistant, with soundness and completeness already mechanized.","The proof burden for a concrete data structure reduces to showing that the tracker in every admitted augmented run remains inhabited, rather than constructing an explicit linearization from scratch.","Future-dependent algorithms, whose linearization points cannot be decided online, remain provable in a forward reasoning style because the tracker keeps all possible linearizations alive.","The register case study supplies a verified implementation of a double-width write using only read and CAS on a single-width cell, connecting the metatheory to a practical hardware gap."],"supporting_citations":[{"why":"Introduced meta-configuration tracking and proved its soundness and completeness informally; the present paper mechanizes that metatheory.","marker":"[16]"},{"why":"Defines linearizability itself, the correctness property the whole argument targets.","marker":"[15]"},{"why":"Supplies the atomic-run formulation of linearizability and the theorems (13.4 and 13.5) that tie it to Herlihy-Wing's definition; the formalization builds on this formulation.","marker":"[25]"}],"fun_headline_variants":["Mechanized soundness and completeness for linearizability in Rocq","Verified forward reasoning: linearizability proofs end-to-end","Machine-checked metatheory closes the linearizability trust gap","Forward reasoning linearizability now proven in Rocq","End-to-end linearizability proofs via verified forward reasoning"],"cache_read_input_tokens":2688,"weakest_assumption_plain":"The formalized notion of linearizability is the atomic-run definition taken from Lynch, and the paper relies on a cited, not machine-checked, equivalence to Herlihy-Wing's history-based definition; if that equivalence is unfaithful, the end-to-end verified guarantee attaches to a different correctness condition.","fun_headline_variants_meta":{"raw":{"variants":["Mechanized soundness and completeness for linearizability in Rocq","Verified forward reasoning: linearizability proofs end-to-end","Machine-checked metatheory closes the linearizability trust gap","Forward reasoning linearizability now proven in Rocq","End-to-end linearizability proofs via verified forward reasoning"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000381,"raw_usage":{"total_tokens":1853,"prompt_tokens":735,"completion_tokens":1118,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":479,"completion_tokens_details":{"reasoning_tokens":1038}},"tokens_in":479,"tokens_out":1118,"duration_ms":9506,"temperature":1.0,"reasoning_tokens":1038,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-04T22:57:40.074346+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Inspect the Rocq proof term of Theorem adequacy: if its only assumptions are the paper's definitions, functional extensionality, and standard finite-map facts, the claimed mechanization is real; any hidden axiom or unverified use of Lynch's Theorems 13.4/13.5 would expose a trust gap. Separately, a concrete counterexample—an implementation whose tracker is inhabited in every admitted augmented run yet whose behavior differs from every atomic run—would directly refute soundness.","supporting_citations":[],"review_version":1}