{"id":"15e9997a-0a0e-4b4d-8031-129f2005b8ee","arxiv_id":"2501.13002","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Standard acceptance-set, must-set and coinductive characterisations of the must-preorder remain sound and complete for asynchronous output-buffered agents with feedback, after equipping servers with forwarding.","lead":"Programs that communicate asynchronously can still be compared with the classic 'must' server refinement test, provided servers are upgraded so they can accept any incoming message and immediately store it back in the shared mailbox. This paper proves that result for a general class of labelled transition systems and backs it with a large Coq development.","discovery_kind":"unification","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 1 as stated for all Fdb LTSs is unsupported: the mechanized theorem requires client-generator hypotheses gen_spec_conv/gen_spec_acc (Appendix D, Table 1) that are not proved to hold for arbitrary Fdb LTSs.","rationale":"The reader's weakest_assumption identifies exactly the gap I consider most load-bearing: completeness relies on client generators tc and ta whose existence is not guaranteed for arbitrary Fdb LTSs. The prose statement of Theorem 1 quantifies over all Fdb LTSs, while the Coq theorem carries explicit gen_spec_conv and gen_spec_acc hypotheses, and Appendix D admits that existence depends on the LTS. This makes the central characterization conditional on an expressiveness property that is neither stated in the main theorems nor proved generically. The paper does provide real support: a substantial Coq development, a concrete ACCS instantiation, and a counterexample to prior work. These justify a conditional verdict rather than rejection. The secondary concern about bar induction being derived from a classical axiom affects the 'fully constructive' claim but not the classical validity of the characterization, so I do not treat it as the primary load-bearing issue. The recommended verdict remains CONDITIONAL, matching the reader.","tokens_in":67736,"tokens_out":7446,"duration_ms":84660,"concrete_test":"In the Coq artifact, search for instances of gen_spec_conv and gen_spec_acc outside the ACCS instantiation. If the only instances are for ACCS—or if attempting to build an instance for an arbitrary LtsObaFB typeclass fails—then the unqualified Theorem 1 is not mechanized. As a sharper check, try to instantiate Theorem equivalence_bhv_acc_ctx with a finite non-ACCS Fdb LTS (e.g., a two-state LTS with a τ-loop and one input action) and attempt to discharge gen_spec_conv/gen_spec_acc using only the Fdb axioms. Failure to discharge, or absence of any such instance, confirms that the prose theorem overclaims.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's central result, Theorem 1, is stated as p ⊑must q iff FW(p) ≼_AS FW(q) for all LTSs LA, LB ∈ Fdb. The Coq statement (Appendix J.6, Theorem equivalence_bhv_acc_ctx) is proved only inside a section whose hypotheses include Context gen_spec_conv gen_conv and gen_spec_acc gen_acc, i.e. the existence of test-generating functions tc and ta satisfying Table 1. Appendix D explicitly says 'whether such tc and ta can actually exist depends on the LTS at hand' and gives definitions only for ACCS (Appendix H.2). Thus the completeness direction—the only direction using these tests—is established only for Fdb LTSs that can express convergence tests and acceptance-set tests. The prose theorem quantifying over all Fdb LTSs is therefore stronger than anything mechanized or proved. If a particular asynchronous calculus cannot express these client generators, the stated equivalence may fail there. This is a load-bearing gap because the paper's headline 'calculus-independent' characterization depends on the tests being available in every Fdb instance, and no generic construction from the Fdb axioms is provided.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies De Nicola and Hennessy's must-preorder for asynchronous systems modelled as Selinger output-buffered agents with feedback (the class Fdb). Its central claim is that the standard characterisations of the must-preorder carry over unchanged to asynchrony provided each server is enhanced with a forwarding construction FW: Theorem 1 states that for all LTSs LA, LB in Fdb and all servers p, q, p is must-below q if and only if FW(p) is below FW(q) in the acceptance-set preorder; Theorem 3 gives the analogous must-set characterisation, and Theorem 2 gives a coinductive characterisation on image-finite LTSs. The development is mechanised in Coq, uses a conversion between extensional and intensional liveness predicates via bar induction, introduces an auxiliary predicate mustaux on sets of servers, and demonstrates the coinductive preorder on a code-hoisting example. The paper also contains a counterexample to a previously published completeness result for asynchronous CCS.","tokens_in":67952,"tokens_out":6988,"duration_ms":80550,"significance":"If the main theorem is correct with a suitable statement, this is a significant contribution: it provides the first calculus-independent account of the must-preorder for asynchrony, shows that the standard acceptance-set, must-set, and coinductive preorders need no modification once forwarding is added, and supplies a substantial machine-checked Coq development with an archived artifact. The methodological choices are also valuable: the LTS-of-sets construction, the explicit use of bar induction for liveness reasoning, and the disclosure of the underlying axioms are all strong points. The proof of the code-hoisting example gives evidence that the coinductive characterisation is practically usable. However, the printed Theorem 1 is stronger than the mechanised theorem, and this mismatch affects the paper's headline claim of a characterisation for every Fdb LTS.","major_comments":[{"comment":"Theorem 1 is stated as an equivalence for every LA, LB ∈ Fdb, but the Coq statement equivalence_bhv_acc_ctx shown in Appendix J.6 is proved inside a section whose hypotheses include FiniteLts A L, FiniteLts B L, gen_spec_conv gen_conv, and gen_spec_acc gen_acc. Appendix D explicitly says that the existence of the client-generating functions tc and ta satisfying Table 1 depends on the LTS at hand, and concrete definitions are given only for ACCS in Appendix H.2. No construction of these generators from the Fdb axioms is supplied. Consequently, the completeness direction (Proposition 4 / Lemma 20) is established only for Fdb instances that are finite in the sense of the Coq typeclass and that can express convergence tests and acceptance-set tests. Since Theorem 1 is the linchpin from which Theorem 3, Corollary 4, and the normal-form characterisation are derived, the missing hypotheses propagate. The theorem statements, the abstract's 'calculus-independent' claim, and the contribution list need to be amended to include these hypotheses, or a proof that every Fdb LTS admits such generators must be provided.","section":"§3.1, Theorem 1; Appendix D, Table 1; Appendix J.6"},{"comment":"The proof of Lemma 20 uses the set E = ⋃ Afw(p, s) and then applies Lemma 19 with the set X = E \\ O, where O is a ready set of q. Lemma 19 is stated only for a finite set O, and the test generator ta defined in Appendix H.2 forms a finite product Π{μ.1 | μ ∈ L}, so it is only well defined for finite L. The Fdb axioms guarantee that each individual set O(p') is finite, but they do not guarantee that the union over all stable states reachable after a trace is finite. The Coq statement's FiniteLts hypothesis would provide such finiteness, but the printed theorem omits it. This is a load-bearing gap in the completeness proof as written, and it reinforces the need to state Theorem 1 with the mechanised hypotheses.","section":"Appendix D, Lemma 20; Appendix H.2"},{"comment":"Theorem 2 is stated for image-finite LTSs, but its proof relies on Theorem 1, which is stated without any image-finiteness or FiniteLts hypothesis. The reader is left with inconsistent assumptions between the two central theorems. The paper should either make Theorem 1's hypotheses explicit and then state Theorem 2 as a consequence under the same hypotheses, or explain why Theorem 2 can be derived without the finiteness assumptions that the mechanised completeness proof requires.","section":"§3.3, Theorem 2; §3.1, Theorem 1"},{"comment":"The paper advertises a 'constructive account' of the must-preorder, but the equivalence between the extensional and intensional predicates (Corollary 2) depends on Proposition 1, decidable bar induction over an STS, which is postulated as an axiom and proved in Coq using the ClassicalEpsilon axiom. The authors disclose this in §3.2 and argue admissibility, but the abstract and contribution list state the development is constructive without this qualification. The claim should be restated as constructive relative to bar induction / ClassicalEpsilon, or the proof of bar induction in the base type theory should be supplied. This is not a fatal flaw, but it is part of the paper's central novelty claim.","section":"§3.2, Proposition 1; Appendix B.1; Abstract"}],"minor_comments":[{"comment":"The proof contains the placeholder identifier 'pattaboy' in several equations; this should be replaced with a proper variable name.","section":"Appendix E, proof of Lemma 37"},{"comment":"The notation line 'p − →[α] q' is defined with 'lts_step p (ActExt µ) q', where the binder µ is not the same as α; the displayed notation and the definition should use a consistent action variable.","section":"Appendix J.2, Coq snippet"},{"comment":"The sentence 'whether such tc and ta can actually exist' is important but easy to miss; it should be highlighted in the main text near Theorem 1, since it determines the actual scope of the characterisation.","section":"Appendix D, first paragraph"},{"comment":"The phrase 'since it is not provable directly in the type theory of Coq' could be misread as saying bar induction is inconsistent with Coq; consider rephrasing to 'not derivable in the current set-theoretic/type-theoretic formalisation'.","section":"§3.2, paragraph on admissibility"}],"recommendation":"major_revision","confidential_remarks":"The main issue is a scope mismatch between the printed theorems and the mechanised statements. This is fixable by restating the theorems with the FiniteLts, gen_spec_conv, and gen_spec_acc hypotheses, or by proving those generators exist for all Fdb LTSs. The paper's contribution remains strong for ACCS and similar calculi even under the restricted statement, so I would not recommend rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The headline result is real: the standard acceptance-set, must-set, and coinductive preorders do characterise the must-preorder after forwarding, for Selinger output-buffered agents with feedback. The Coq development backs the central technical work, and the counterexample to the Castellani–Hennessy completeness result looks correct. This is the first calculus-independent treatment and the first mechanisation of this theory, and that is worth taking seriously.\n\nThe forwarding construction is the right idea, and the paper is honest about its lineage: the lifting FW works on any LTS, and the standard preorders are used unchanged. The bar-induction material is a genuine addition, not a ornament, and the code-hoisting example shows the coinductive preorder is usable in practice.\n\nThe soft spots are real but local. The main one is the mismatch the stress-test identifies: Theorem 1 as printed quantifies over all Fdb LTSs, but the Coq theorem in Appendix J.6 is proved only under the hypotheses gen_spec_conv and gen_spec_acc. Appendix D says explicitly that whether such client generators exist depends on the LTS at hand. So the completeness direction is not established for arbitrary Fdb LTSs, and the prose theorem is stronger than anything proved. This is load-bearing, because the paper's \"calculus-independent\" claim rests on those tests being available in every instance, and no generic construction from the Fdb axioms is supplied. The fix is straightforward in principle: state the theorem with its full hypotheses, or prove the generators exist for every Fdb LTS if that is true. As printed, a reader who wants to instantiate the theorem for a new calculus has to do extra work that the paper does not advertise.\n\nThe constructive claim is also slightly overstated. Bar induction is proved using ClassicalEpsilon in Coq, and the paper argues admissibility via Rahli et al. That is a reasonable position, but \"fully constructive\" in the abstract hides the axiom dependence. This is disclosed later, so it is not dishonest, but it should be in the abstract or introduction.\n\nNone of this undermines the soundness direction or the overall architecture. The acceptance-set, must-set, and coinductive preorders are defined independently of the contextual preorder, the equivalences are mechanised, and the self-citations are background, not load-bearing. The paper deserves a serious referee and a revision, not a desk rejection. I would bring it to a reading group and would cite it, with a caveat about the theorem statement.","headline":"A substantial, mostly machine-checked result with an important mismatch between the prose theorems and the Coq statement: the completeness direction needs client-generator hypotheses that are not guaranteed for all Fdb LTSs.","tokens_in":68484,"tokens_out":1742,"would_cite":true,"duration_ms":23381,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q85","03B35"],"pacs":[],"model":"deepseek-v4-flash","headline":"The standard characterisations of the must-preorder survive asynchrony once servers act as forwarders.","keywords":["must-preorder","asynchronous communication","acceptance sets","must-sets","coinductive preorder","forwarders","bar induction","Coq mechanisation"],"falsifier":"Take a finite Fdb LTS whose only client state is stable, non-successful, and has no outgoing transitions, while two servers differ in their reachable output sets. Then $p \\sqsubseteq_{\\mathrm{must}} q$ holds vacuously (no client can make $p$ succeed), yet $FW(p) \\preceq_{AS} FW(q)$ fails if the servers' stable output sets are incomparable; such a pair would show the unqualified Theorem 1 fails without the $tc$ and $ta$ hypotheses.","tokens_in":67524,"feed_emoji":"📬","tokens_out":9988,"duration_ms":101850,"temperature":0.7,"pith_summary":"This paper establishes that the classic behavioural characterisations of De Nicola and Hennessy's must-preorder --- acceptance sets, must-sets, and the coinductive preorder --- are sound and complete for asynchronous communication, provided each server is first lifted to a \"forwarding\" version that can read any message as long as it stores it back into the shared mailbox. Since the must-preorder quantifies over all possible clients, it is not a workable proof method on its own; the characterisations turn it into a comparison of observable behaviour on a single labelled transition system. The result is calculus-independent: it is proved for Selinger's output-buffered agents with feedback, the general LTS class covering asynchronous CCS and the asynchronous pi-calculus, and it is fully mechanised in Coq. The development is constructive, using Brouwer's bar induction to relate the extensional definition of \"must\" to an inductive one. As corollaries, the must-preorder coincides with failure-divergence refinement, and a normal form that ignores non-causal action orderings also characterises it.","feed_headline":"Forwarding makes asynchronous refinement match classical tests","feed_subtitle":"Adding a forwarder lift lets acceptance sets prove the contextual must-preorder, all verified in Coq.","key_machinery":"The load-bearing construction is the forwarder lift $FW$, which maps any output-buffered agent with feedback $L = \\langle A, L, \\to\\rangle$ to an LTS whose states are pairs $p \\vartriangleright M$ of a process and a finite multiset of messages in a shared mailbox. Four rules govern it: the process may move alone; an input may synchronise with a matching message in the mailbox; the whole state may input any message into the mailbox; and it may output any message from the mailbox. This makes every state input-enabled, with each input looping back through a complementary output --- exactly the behaviour of a forwarder that receives a message and stores it back. The lift preserves the must predicate (Lemma 3), places the LTS in the class Fwd where acceptance sets can be simplified to sets of outputs, and leaves the standard alternative preorders unchanged, so the complexity of asynchrony is absorbed by the LTS rather than by the definitions.","core_discovery":"The paper's central claim is Theorem 1: for every LTS $L_A, L_B$ in the class Fdb and every servers $p, q$, $p \\sqsubseteq_{\\mathrm{must}} q$ holds exactly when $FW(p)$ is below $FW(q)$ in the standard acceptance-set preorder $\\preceq_{AS}$, where $FW$ is the forwarder lift pairing each process with a multiset mailbox. The same comparison also characterises the preorder through must-sets (Theorem 3) and through a single-action coinductive preorder $\\preceq_{\\mathrm{co}}$ (Theorem 2), which gives a practical proof method and is used to certify a code-hoisting transformation. The paper shows, contrary to earlier calculus-specific work, that the alternative preorders themselves need no adjustment: only the LTS is enhanced, so the same definitions work for synchronous and asynchronous semantics. Along the way it proves that the intensional (inductive) and extensional versions of termination and \"must\" coincide using decidable bar induction, and it reports the first fully mechanised, fully nondeterministic theory of the must-preorder in Coq.","pith_inferences":["The forwarder construction is a general recipe for transferring synchronous testing theories to asynchronous ones: any calculus with an Fdb LTS inherits the standard characterisations, and the same lift may apply to may-preorder, fair testing, or compliance.","Adopting these theorems in a new calculus leaves one concrete task unautomated: constructing the convergence and acceptance client generators; the paper supplies them for ACCS, and their absence would void the characterisation.","The normal-form result suggests a testable extension to ordered media: replacing the order-insensitive normal form with queue-respecting traces should yield the analogous characterisation for FIFO or per-channel mailboxes, with the forwarder axioms adjusted accordingly.","A finite counterexample of the kind described under falsifier would settle whether the main-text Theorem 1 overstates the mechanised theorem; if it exists, the effective statement is the hypothesised one."],"forward_implications":["For any calculus whose LTS is in Fdb and can express the two client generators, proving a refinement reduces to comparing acceptance sets on the forwarder-lifted LTS, with no calculus-specific machinery.","The coinductive preorder gives a single-action proof method; the paper uses it to certify the code-hoisting refinement $\\tau.(\\bar a \\parallel b) + \\tau.(\\bar a \\parallel c) \\sqsubseteq_{\\mathrm{must}} \\bar a \\parallel (\\tau.b + \\tau.c)$.","The must-preorder coincides with failure-divergence refinement: $p \\sqsubseteq_{\\mathrm{must}} q$ iff $FW(p) \\preceq_{\\mathrm{cnv}} FW(q)$ and $FW(p) \\le_{\\mathrm{fail}} FW(q)$ (Corollary 3).","Normalising traces into multisets of consecutive inputs and outputs yields a preorder on normal forms that again characterises the must-preorder (Corollary 4), so irrelevant action orderings can be dropped in proofs.","Because all statements are mechanised in Coq, the characterisations are reusable as a library for machine-checked liveness-preserving transformations in message-passing languages."],"supporting_citations":[{"why":"Defines the must-preorder and the must-set testing theory that the paper characterises.","marker":"[43]"},{"why":"Introduces acceptance sets and the behavioural preorder whose asynchronous validity is the paper's main theorem.","marker":"[55]"},{"why":"Supplies the first-order axioms for asynchrony that define the class Fdb of output-buffered agents with feedback.","marker":"[90]"},{"why":"Pioneered the forwarding or saturated-server idea that the FW construction adapts.","marker":"[64]"},{"why":"Gives the prior asynchronous testing characterisation that Appendix I shows incomplete; the paper's forwarding method repairs the gap.","marker":"[38]"},{"why":"Extends the earlier approach to a typed asynchronous pi-calculus via a context LTS, the baseline the LTS-level results supersede.","marker":"[57]"},{"why":"Supplies the coinductive preorder and the termination/divergence treatment underlying the convergence predicate.","marker":"[2]"},{"why":"Revisited the must-preorder and provided the coinductive characterisation that the paper lifts to asynchrony.","marker":"[72]"},{"why":"Supplies the extensional/intensional predicate terminology and the bar-induction viewpoint used to make the development constructive.","marker":"[28]"},{"why":"Shows bar induction is compatible with constructive type theory, supporting the paper's claim that the Coq mechanisation is constructive.","marker":"[81]"}],"fun_headline_variants":["Forwarders make async must-preorder match classical tests","Coq-verified: forwarder lift standardizes async refinement","Just add forwarders: async must-preorder gets standard tests","Standard preorders work for async with forwarder lift","Coq proof: forwarders let classical characterizations hold async"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The completeness direction assumes that the asynchronous LTS at hand can express the two client generators $tc$ and $ta$ with the properties listed in Table 1 --- one that tests convergence along traces, one that tests acceptance sets --- because the main text states Theorem 1 for every Fdb LTS, while the mechanised statement carries these as explicit hypotheses and Appendix D notes their existence depends on the LTS at hand.","fun_headline_variants_meta":{"raw":{"variants":["Forwarders make async must-preorder match classical tests","Coq-verified: forwarder lift standardizes async refinement","Just add forwarders: async must-preorder gets standard tests","Standard preorders work for async with forwarder lift","Coq proof: forwarders let classical characterizations hold async"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001044,"raw_usage":{"total_tokens":4429,"prompt_tokens":1024,"completion_tokens":3405,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":640,"completion_tokens_details":{"reasoning_tokens":3323}},"tokens_in":640,"tokens_out":3405,"duration_ms":24534,"temperature":1.0,"reasoning_tokens":3323,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T16:32:43.043568+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a finite Fdb LTS whose only client state is stable, non-successful, and has no outgoing transitions, while two servers differ in their reachable output sets. Then $p \\sqsubseteq_{\\mathrm{must}} q$ holds vacuously (no client can make $p$ succeed), yet $FW(p) \\preceq_{AS} FW(q)$ fails if the servers' stable output sets are incomparable; such a pair would show the unqualified Theorem 1 fails without the $tc$ and $ta$ hypotheses.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Extends the earlier approach to a typed asynchronous pi-calculus via a context LTS, the baseline the LTS-level results supersede."}],"review_version":1}