{"id":"c2147235-8e21-4e57-b42b-882fe49901f9","arxiv_id":"2509.04777","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"A sound filter-adequacy transformation proves that verifying a forall-forall property of a transformed bicom implies the original forall-exists property.","lead":"This paper introduces a transformation that converts a forall-exists relational verification task into a forall-forall task on an instrumented product program, so existing verifiers can be reused. The approach could make it practical to verify nondeterministic refinement and possibilistic noninterference properties.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Lemma 5.3's while-case proof uses the wlp of the loop body as invariant; the claimed R⇒I step does not follow from the loop equation, leaving a gap that only the missing Rocq artifact can resolve.","rationale":"The paper's central claim is Theorem 5.4, reducing ∀∃ verification to ∀∀ verification of chk(B). The theorem is supported by a long appendix proof and a claimed Rocq mechanization, but no artifact is released. Reading the appendix in good faith, the most load-bearing soft spot is in Lemma 5.3, which Theorem 5.4's embed case depends on. In the while case, the invariant I is defined as wlpR of the loop body with postcondition S, whereas the assumption only entails R⇒wlpR of the whole loop, namely the gfp from Lemma 4.9. These are not the same; the printed proof's R⇒I and 'fixpoint property' steps are unjustified as written. If the invariant is corrected to the gfp, the rest of the proof is plausible and the theorem may well be sound; a typo of this kind is consistent with the claimed mechanization. This reinforces, rather than replaces, the reader's CONDITIONAL verdict. The reader's identified weakest assumption—manual projection equivalence in the prototype—is a separate, genuine methodology limitation; our concern is a proof-level gap in the presented argument. Given no artifact, the right posture is to keep the conditional acceptance but require the Rocq development to resolve the printed gap.","tokens_in":41543,"tokens_out":11058,"duration_ms":103438,"concrete_test":"Reconstruct the Rocq development and check Lemma 5.3's statement and proof, particularly the while case. If unavailable, formalize Lemma 5.3 in Rocq using the paper's definitions; a correct formalization should use Q := wlpR(while e vnt e_v do (x:=e_v; uchk(d); assert(0≤e_v<x)), S) (the gfp) as the invariant and verify R⇒Q and Q⇒F(Q). A quick sanity check: instantiate the printed identity with c = while true do skip, S arbitrary; the printed R⇒I fails, the gfp version succeeds.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Appendix A, proof of Lemma 5.3, while case: the invariant is defined as I := wlpR(x:=e_v; uchk(d); assert(0≤e_v<x), S), i.e., wlp of one loop body. But the assumption |=⟨skip|uchk(while...)⟩:R¥{S gives R⇒wlpR(while...,S), which by the loop equation (Lemma 4.9) is R⇒gfp(F), not R⇒wlpR(body,S). These differ: for while true do skip with any postcondition S, gfp(F)=true while wlp(body,S)=S. The subsequent use of 'the fixpoint property' applies to the gfp, not to this I. If I is meant to be the gfp wlp of the whole loop, the proof is recoverable, but as printed it is a genuine gap. This matters because the embed case of Theorem 5.4 appeals to Lemma 5.3, so the central soundness claim is not fully established by the written proof; the claimed Rocq mechanization is not released for checking.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a method to verify ∀∃ (forall-exists) relational properties of nondeterministic imperative programs by reducing them to ∀∀ (forall-forall) properties of a transformed product program, called a bicom. It introduces ERHL, a program logic for ∀∃ judgments extended with assertion failures; defines bicoms with a big-step semantics, weakest preconditions, and framing conditions; and defines a filter-adequacy transformation chk that adds assertions to a bicom so that successful ∀∀ verification of chk(B) implies the desired ∀∃ property for the projections of B. The main result is Theorem 5.4. A prototype based on Why3 is described and used to verify several examples, and the paper claims full mechanization in Rocq.","tokens_in":41749,"tokens_out":8187,"duration_ms":67354,"significance":"If the main theorem is correct, this is a significant contribution: it offers a way to leverage mature auto-active verification tools for ∀∃ properties, which are notoriously harder than ∀∀ properties. The paper is well structured, provides detailed semantic definitions, and includes an extended appendix with proofs. The authors also give explicit credit to the sources of their proof rules and discuss related work thoroughly. The claimed Rocq mechanization, if made available, would strengthen confidence considerably, but in the absence of a public artifact the correctness of the central theorem rests on the written proofs, which contain a serious gap (see Major Comment 1).","major_comments":[{"comment":"The invariant is defined as I := wlpR(x:=e_v; uchk(d); assert(0≤e_v<x), S), the wlp of a single loop body. However, the assumption |= ⟨skip|uchk(while e vnt e_v do d)⟩ : R ¥{S gives, via wlp/correctness, R⇒wlpR(uchk(while...), S), which by the loop equation is R⇒gfp(F) for the function F of Lemma 4.9. The step 'so by definition of wlpR and wlp/correctness lemma we have |= R⇒I' is therefore not a logical consequence, since gfp(F) does not imply wlpR(body, S) in general. For example, take c = while false do skip with e_v = 0 and S = true; then wlpR(uchk(c), S) = true while wlpR(body, S) = false, so the claimed implication fails. The proof appears repairable by defining I as wlpR(uchk(while...), S) (the greatest fixpoint), which makes R⇒I immediate and still allows the derivation of the eSkipDo premise from the post-fixpoint property, but as printed the proof is invalid. Since the embed case of Theorem 5.4 appeals to Lemma 5.3, this gap directly affects the central soundness claim.","section":"Appendix A, proof of Lemma 5.3, while case"},{"comment":"The paper states that 'The theorem has also been fully mechanized in Rocq' and that missing details can be found in the Rocq development, but no artifact, repository, or link is provided. Given the subtlety of the proofs—exemplified by the gap in Lemma 5.3—an independent check of the mechanization is essential to validate the central claim. Without the artifact, the claimed machine-checked proof cannot be confirmed, and the written proof alone is insufficient.","section":"Section 1 and Appendix A"}],"minor_comments":[{"comment":"The abstract contains a spelling error: 'specificaton' should be 'specification'; the authors may also want to proofread the phrase 'the the existentially quantified asserts' in Section 6.","section":"Abstract"},{"comment":"The label 'adeqacy' is misspelled; it should be 'adequacy'.","section":"Lemma 4.7"},{"comment":"The derivation of eSkipIf refers to 'rIf' but no rule with that name appears in the paper; the intended rule is likely eIf4 or eRewrite. Please clarify the reference.","section":"Section 3, footnote 3"},{"comment":"The statement that checking conditions ↼−B≃c and −⇀B≃c′ 'was done manually for our examples' is a significant limitation of the methodology; it deserves more prominence, since a mistake in this step would make the verified ∀∀ property irrelevant to the original programs.","section":"Section 6"},{"comment":"The notation −⇀ ⇀ for the bi-right projection is difficult to parse in the calculation; consider introducing a more mnemonic name or a brief explanation of its use in that proof.","section":"Appendix A, Theorem 5.4, loop case"}],"recommendation":"major_revision","confidential_remarks":"The paper builds heavily on the authors' own prior work [52], and the novelty rests mainly on the filter-adequacy transformation and the accompanying soundness theorem. The missing Rocq artifact is a serious concern for a paper that claims full mechanization; I recommend requiring an artifact in the revision. The gap in Lemma 5.3 is likely repairable, but it must be fixed and the proof carefully rechecked before the paper can be accepted."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThe paper is worth your time if you work on relational verification. The central idea—transform a bicom so that a forall-exists judgment is implied by a forall-forall judgment, then verify with ordinary tools—is new as far as I know, and the chk transformation plus the bicom semantics with failure are real contributions. The detailed proof of Theorem 5.4 is a serious attempt to make the reduction foundational. The prototype and examples give reason to think the approach scales to small but nontrivial nondeterministic programs.\n\nWhere it is soft: the stress-test concern is real. In the appendix proof of Lemma 5.3, while-case, the invariant is defined as wlpR(x:=e_v; uchk(d); assert(...), S), i.e., the wlp of a single loop body. But the assumption of the lemma gives R⇒wlpR(while...,S), which is R⇒gfp(F), not R⇒wlpR(body,S). The proof then says I⇒F(I) \"by the fixpoint property\"; that property applies to the greatest fixpoint, not to this I. For a loop like while true do skip, I can be S while gfp is true, so the step does not follow. If the authors intended I to be the gfp wlp of the whole loop, the rest of the calculation can likely be repaired; as printed, the central soundness chain from Lemma 5.3 to Theorem 5.4 has a gap. The claimed Rocq mechanization would settle this, but no artifact is released, so I can't check.\n\nOther soft spots are minor. The projection equivalence in Section 6 is checked manually; that's a usability caveat, not a flaw in the theorem. Self-citation to the authors' ERHL+ preprint is appropriate—they adapted those rules and say so.\n\nOverall: the reduction is important, the semantic setup is coherent, and the gap looks fixable rather than fatal. I'd send this to a serious referee, with the explicit instruction to verify Lemma 5.3 and ideally to ask for the Rocq development. I'd probably cite it for the chk idea once the proof issue is resolved.","headline":"A genuinely useful reduction of forall-exists to forall-forall, with a real but likely repairable gap in the printed proof of the key lemma.","tokens_in":42267,"tokens_out":4014,"would_cite":true,"duration_ms":37396,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68N30","03B70","68Q60"],"pacs":[],"model":"deepseek-v4-flash","headline":"By instrumenting a paired product program with filtering assertions, this paper proves that a forall-forall verification success implies the original forall-exists relational specification.","keywords":["relational verification","forall-exists properties","product programs","bicoms","filter-adequacy transformation","nondeterminism","auto-active verification","program logic"],"falsifier":"Search for a well-formed bicom $B$ and relations $R,S$ such that $B$ is framed by $\\mathit{vs}$, $\\mathit{vs}$ frames $R$ and $S$, and $\\models \\mathit{chk}(B,\\mathit{vs}) : R\\ \\yen\\ S$ holds while $\\models \\mathit{left}(B)|\\mathit{right}(B) : R\\ \\exists{\\approx\\!\\!>}\\ S$ fails; the theorem says no such instance exists, so a small brute-force enumeration over finite-state commands would settle the claim. A more operational check: use the prototype on a pair where the bicom's projection is not equivalent to the intended program, e.g., $\\langle x:=0|\\mathit{skip}\\rangle;\\mathit{havf}_y(y=0)$ for $\\mathit{hav}\\,x\\,|\\,\\mathit{hav}\\,y$ with postcondition $x=0$; if the tool reports success, it is not enforcing the representation condition.","tokens_in":41367,"feed_emoji":"✅","tokens_out":9553,"duration_ms":84115,"temperature":0.7,"pith_summary":"This paper tries to establish a route from hard relational program properties to easy ones: any $\\forall\\exists$ correctness judgment between two nondeterministic programs can be verified by building a paired product program, instrumenting it with filtering assertions, and then proving an ordinary $\\forall\\forall$ property of the instrumented product. The central soundness theorem says that if the transformed product satisfies its specification, the original pair of programs really does satisfy the $\\forall\\exists$ judgment. This matters because $\\forall\\forall$ verification is well supported by existing logics and tools, while $\\forall\\exists$ verification---needed for nondeterminism, refinement, and generalized noninterference---has few practical tools. The paper backs the claim with a program logic, a fully mechanized proof, and a working prototype that verifies the paper's examples through an existing SMT-based verifier.","feed_headline":"Forall-exists checks become forall-forall checks","feed_subtitle":"Prove nondeterministic refinement and noninterference using ordinary assertion-based tools, not new logics.","key_machinery":"The load-bearing object is the bicom, a syntactic product program that runs a pair of commands side by side with explicit alignment constructs: the embed $\\langle c|c'\\rangle$, bi-if, bi-while with data-dependent alignment conditions, and the havoc-filter $\\mathit{havf}_x\\,Q$, which nondeterministically picks a right-side value for $x$ and then assumes the relation $Q$. The filter-adequacy transformation $\\mathit{chk}$ instruments each loop with snapshot variables and asserts that the declared variant decreases on right-only iterations, and guards every havoc-filter with an existential assertion ensuring that a witness value exists. These inserted assertions are what turn $\\forall\\exists$ adequacy into a $\\forall\\forall$ verification condition; the semantic framing condition $\\mathit{bFrame}(B,\\mathit{vs})$ keeps the instrumentation from interfering with the underlying executions.","core_discovery":"The paper's central claim is Theorem 5.4: from a well-formed bicom $B$ framed by a variable list $\\mathit{vs}$, if the instrumented bicom $\\mathit{chk}(B,\\mathit{vs})$ is correct for pre-relation $R$ and post-relation $S$ in the $\\forall\\forall$ sense, then the left and right projections of $B$ satisfy the $\\forall\\exists$ judgment $R\\ \\exists{\\approx\\!\\!>}\\ S$. In other words, the filter-adequacy transformation turns the existence of a matching right-side execution into a checkable universal property of a product program, provided the original programs are semantically equivalent to the projections of $B$ and the framing conditions hold. The proof works by deriving, from the weakest-precondition equations of the instrumented bicom, exactly the premises of the paper's program-logic rules for the projections.","pith_inferences":["The same filter-adequacy idea could plausibly extend to forall-exists properties with multiple existential witnesses, since existing k-safety product encodings could be instrumented in the same way.","Because the transformation is purely syntactic and linear-time, one could automate the search over candidate bicoms: generate alignments, apply chk, and let an SMT solver decide the forall-forall check, turning the methodology into a fully automatic procedure for decidable fragments.","The paper's reliance on user-supplied framing lists and manual projection checks suggests that the next practical step is to infer frames automatically and discharge projection equivalence with a syntax-directed checker; if those checks are automated, the method becomes a drop-in front-end for existing auto-active verifiers.","The treatment of right-side may-termination via filtering could also serve as a lightweight termination argument in settings where must-termination is too strong, such as probabilistic program refinement with almost-sure termination."],"forward_implications":["A successful forall-forall verification of the transformed bicom is sufficient evidence for the forall-exists specification of the actual programs, so users can work with ordinary assertions and standard verifiers.","Right-side divergence, the main obstacle in forall-exists reasoning, is handled by filtering right-side executions to those that decrease the declared variant, making may-termination a by-product of the forall-forall check.","Data-dependent loop alignments, not just lockstep or fixed n,m alignments, are supported, which covers stuttering loops and conditional alignments such as the paper's running example.","The soundness theorem is independent of how the forall-forall property is discharged, so the same transformation can be used with any verification technique, including testing.","The theory is proved for a small core language, but the structure of the proof is designed to adapt to richer programming languages and assertion languages."],"supporting_citations":[{"why":"Supplies the ERHL+ logic that the paper adapts into its program logic for forall-exists judgments.","marker":"[52]"},{"why":"Supplies the filtering-with-assumptions idea and the embed notation for pairs of executions.","marker":"[2]"},{"why":"Provides complementary product-program and alignment-search work that motivates the bicom design.","marker":"[24]"},{"why":"Supplies Kleene algebra with tests, the basis for the kat equivalence used in projections and rewriting.","marker":"[43]"},{"why":"Provides the bicom-like alignment product and the failure-semantics considerations that shape bicom semantics.","marker":"[6]"},{"why":"Supplies the prototype base that translates bicoms into verification conditions for SMT solvers.","marker":"[50]"}],"fun_headline_variants":["Filter-adequacy: ∀∃ verification via ∀∀ checks","Turn existential proof goals into universal ones","Prove nondeterministic specs with standard ∀∀ tools","From ∃ to ∀: a filter transform for relational proofs","Use ordinary assertion verifiers for ∀∃ properties"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The method only works if the user's product program actually represents the two programs being verified: the bicom's left and right projections must be equivalent to the two unary programs, and the supplied framing list must cover every variable the programs and specifications depend on; the paper's prototype checks these conditions manually rather than automatically.","fun_headline_variants_meta":{"raw":{"variants":["Filter-adequacy: ∀∃ verification via ∀∀ checks","Turn existential proof goals into universal ones","Prove nondeterministic specs with standard ∀∀ tools","From ∃ to ∀: a filter transform for relational proofs","Use ordinary assertion verifiers for ∀∃ properties"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000322,"raw_usage":{"total_tokens":1851,"prompt_tokens":1027,"completion_tokens":824,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":643,"completion_tokens_details":{"reasoning_tokens":745}},"tokens_in":643,"tokens_out":824,"duration_ms":7786,"temperature":1.0,"reasoning_tokens":745,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T16:27:19.919268+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Search for a well-formed bicom $B$ and relations $R,S$ such that $B$ is framed by $\\mathit{vs}$, $\\mathit{vs}$ frames $R$ and $S$, and $\\models \\mathit{chk}(B,\\mathit{vs}) : R\\ \\yen\\ S$ holds while $\\models \\mathit{left}(B)|\\mathit{right}(B) : R\\ \\exists{\\approx\\!\\!>}\\ S$ fails; the theorem says no such instance exists, so a small brute-force enumeration over finite-state commands would settle the claim. A more operational check: use the prototype on a pair where the bicom's projection is not equivalent to the intended program, e.g., $\\langle x:=0|\\mathit{skip}\\rangle;\\mathit{havf}_y(y=0)$ for $\\mathit{hav}\\,x\\,|\\,\\mathit{hav}\\,y$ with postcondition $x=0$; if the tool reports success, it is not enforcing the representation condition.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the ERHL+ logic that the paper adapts into its program logic for forall-exists judgments."},{"cited_title":"Naumann, and Minh Ngo","cited_arxiv_id":null,"evidence_quote":"Supplies the filtering-with-assumptions idea and the embed notation for pairs of executions."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides complementary product-program and alignment-search work that motivates the bicom design."},{"cited_title":"Naumann, and Mohammad Nikouei","cited_arxiv_id":null,"evidence_quote":"Provides the bicom-like alignment product and the failure-semantics considerations that shape bicom semantics."},{"cited_title":"Nagasamudram, A","cited_arxiv_id":null,"evidence_quote":"Supplies the prototype base that translates bicoms into verification conditions for SMT solvers."}],"review_version":2}