{"id":"6ad566b2-de5b-4218-8a38-aede58061c83","arxiv_id":"2504.17444","paper_version":2,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":8.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"Relational Hoare triples expressing forall-exists refinement between nondeterministic programs are encoded as standard unary Hoare triples using an execution predicate, with a machine-checked proof of validity equivalence.","lead":"This paper shows how to translate the nondeterministic relational Hoare logic, which is used to prove that one program refines another, into ordinary unary Hoare logic. This means refinement proofs could be done without extending or re-verifying the base logic, potentially simplifying verification tools.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The encoding theorem is proved only for the redefined configuration-refinement semantics; the original multi-step ∀∃ relational triple validity is not encoded, so the title's claim is stronger than what is established.","rationale":"The strongest claim is the exact if-and-only-if of Theorem 4. The weakest point is not an internal error in the proof—the proof is clean and the Rocq formalization is independent support—but the fact that the theorem's left-hand side uses Definition 9, a strictly weaker validity than the multi-step Definition 1 used in the ∀∃ relational Hoare logic literature. The paper announces in Sec. 1 that it redefines validity, and Sec. 8 gives a concrete triple that is valid under the new definition but invalid under the old one. I checked that the encoded standard triple for that example is ∀-valid, so the equivalence genuinely fails for the original semantics. This does not refute the paper's internal claims; it scopes them. Because the title and abstract say 'the ∀∃ relational Hoare logic' without the qualification, this is a load-bearing concern for the advertised contribution. The reader's conditional verdict captures exactly this gap, so no change is needed. If the artifact's Rocq development were inspected and the theorem is stated with ↩→, the conditional would remain; if the authors could show that for the fragment actually used (triples ending in [skip]) the two semantics coincide, the practical impact would be smaller, but the logic-level claim would still need qualification.","tokens_in":50015,"tokens_out":10448,"duration_ms":104572,"concrete_test":"Replace Definition 9's ↩→ by Definition 1's →* in the statement of Theorem 4 and rerun the proof attempt; the ⇐ direction breaks at the point where X is instantiated to the terminal-state set, since this yields only configuration refinement, not multi-step reachability. Then verify the paper's own Sec. 8 witness: for ⟨x=y∧[skip]⟩ x:=x+1 ⟨x=y∧[y:=y−1]⟩, the left-hand side is false under →* while the encoded standard triple {LPM_X} x:=x+1 {LQM_X} is ∀-valid; if this holds, the theorem depends essentially on the relaxed semantics.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is Theorem 4, whose proof goes through Definition 9 (relational validity via configuration refinement) and Theorem 11 (decomposition of ↩→ by wlp). This is not the same judgment as Definition 1, where the high-level configuration must be reachable by multi-step transitions →*. The paper's own Sec. 8 example shows the difference: ⟨x=y∧[skip]⟩ x:=x+1 ⟨x=y∧[y:=y−1]⟩ is valid under ↩→ but not under →*, because skip cannot reduce to y:=y−1. Under the encoding, however, the corresponding standard triple is ∀-valid, since LQM_X can be satisfied by the continuation y:=y−1. Hence Theorem 4 would be false if Definition 1 were used. Because the right-hand side is independent of the relational semantics, the semantic weakening is load-bearing: the paper establishes an exact correspondence with a relaxed logic, not with the original ∀∃ relational Hoare logic advertised in the title and abstract. The practical refinement fragment with [skip] postconditions is unaffected by Prop. 10, but the logic's intermediate judgments—needed for rules such as Rel-Seq and High-Focus—are not equivalent, so the encoding does not preserve the original proof-theoretic content. The authors are transparent about the modification, but the central claim should be scoped accordingly.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes an encoding theory that reduces a programs-as-resources relational Hoare logic for nondeterministic programs to standard (unary) Hoare logic. It redefines relational triple validity using a configuration-refinement relation based on denotational semantics rather than multi-step transitions, then defines an assertion encoding L·M_X via weakest preconditions. Theorem 4 states that a relational triple is valid under this relaxed semantics iff, for every high-level postcondition X, the encoded standard Hoare triple is ∀-valid. The paper also gives a syntactic encoding using an execution predicate Exec_X, presents proof rules for this predicate, shows how relational proof rules become standard proof rules, and reports machine-checked Rocq formalization plus case studies including mergesort, BST, DFS, and KMP.","tokens_in":50225,"tokens_out":10871,"duration_ms":118230,"significance":"Within its redefined semantics, the encoding is elegant and theoretically useful: it avoids ghost-state and invariant machinery, and it allows standard Hoare logic proof infrastructure to be reused for refinement proofs. The paper's strengths include a semantic proof of the central equivalence, a machine-checked Rocq formalization with a Zenodo artifact, and substantial case studies. The authors are also transparent in Section 8 that configuration refinement is a weakening of multi-step validity and that some previously invalid triples become valid. The main limitation is that Theorem 4 does not encode the original Definition 1 semantics; because the encoded standard triple does not depend on the relational semantics, the equivalence is exact only for the relaxed logic. For final refinement judgments with [skip] postconditions, Proposition 10 recovers the original meaning, but intermediate judgments in relational proofs are broader, so the advertised scope of the title and abstract should be adjusted.","major_comments":[{"comment":"Theorem 4 is proved for the relaxed validity based on configuration refinement ↩→, not for the original multi-step validity of Definition 1. The example in Section 8, ⟨x = y ∧ [skip]⟩ x := x+1 ⟨x = y ∧ [y := y−1]⟩, is valid under Definition 9 but invalid under Definition 1, and since the encoded standard triple is ∀-valid independently of which relational semantics is fixed, the theorem would be false for Definition 1. This gap is load-bearing for the paper's central claim: the title and abstract present the result as an encoding of the ∀∃ relational Hoare logic, and intermediate rules such as Rel-Seq and High-Focus can derive triples that are valid only under the relaxed semantics. Proposition 10 rescues only the fragment whose postcondition is [skip]. I request that the paper be explicitly rescoped—in the title, abstract, and introduction—to the configuration-refinement-based validity, with a precise statement that the original multi-step semantics is encoded only for the [skip]-postcondition refinement fragment.","section":"§3 (Definition 9), §4 (Theorem 4), §8"},{"comment":"The theorem's right-hand side universally quantifies over an arbitrary subset X of high-level states, and the assertion encoding L·M_X and Exec_X are parameterized by this second-order object. The paper argues in Section 8 that X is a mere placeholder and compares it to logical variables in VST specifications, but VST-style logical variables range over data values, not over sets of states. The text should state more precisely that using the encoding in a concrete standard Hoare logic requires either a schematic meta-level variable X or an assertion language extended with a family of predicates indexed by X; otherwise the reduction is a meta-theorem rather than a syntactic judgment in the underlying object logic. This is a clarification of the practical scope of the reduction rather than a challenge to the semantic argument.","section":"§4.2 (Theorem 4), §5.2 (Definition 17)"}],"minor_comments":[{"comment":"In the sentence 'That is for any σH3 such that (σH2,σH3)∈JcH2Knrm, we have (σH1,σH3)∈JcH2Knrm', the second occurrence of JcH2Knrm should be JcH1Knrm; the same typo appears in the appendix proof.","section":"§4.2 and Appendix B (Theorem 4 proof, ⇐ direction)"},{"comment":"The numbering 'Definition 17' is used twice: once for the syntactic encoding in Section 5.2 and once for the semantic interpretation of the execution predicate in Appendix C.2. Please renumber so that cross-references are unambiguous.","section":"§5.2 vs. Appendix C.2"},{"comment":"The high-level mergeH code is misparenthesized and hard to parse; the two branches of the choice construct are not clearly delimited. Please rewrite the pseudocode with explicit begin/end or indentation for each branch.","section":"§7.1 (Figure 10)"},{"comment":"The proof of the disjunction case begins with 'we have ∃𝑎.∃σH cH...' even though no existential variable 𝑎 is involved in that case; remove the stray ∃𝑎 or correct the formula to match the disjunction case.","section":"§5.1 (Theorem 16(d), proof)"},{"comment":"The side condition of Exec-Nondet is written as 'P_H[v/x] ⇒ e1≤v≤e2' without explicit quantification over v. State whether this is meant universally over all v or for the value chosen by the nondeterministic assignment, since this affects how the rule is applied.","section":"§6.1 (Figure 9, Exec-Nondet)"},{"comment":"The phrase 'without requiring modifications to the logic framework' is stronger than what is demonstrated: the paper introduces the Exec_X predicate and its update rules into the assertion language and proof system. Suggest wording such as 'without changing the core standard Hoare rules or re-verifying their soundness.'","section":"Abstract and §1"}],"recommendation":"major_revision","confidential_remarks":"The core semantic argument is correct and machine-checked, and the artifact is a genuine strength. The main risk is scope overclaim: the title and abstract promise an encoding of the original ∀∃ relational Hoare logic, while Theorem 4 holds for the relaxed configuration-refinement semantics. If the authors rescope the claims clearly and address the intermediate-judgment issue, I would be willing to support acceptance."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick read: the core reduction is real and the Rocq formalization is a plus, but the paper encodes a redefined, configuration-refinement-based validity of relational triples, not the original multi-step semantics advertised in the title. The reader’s conditional verdict is fair.\n\nWhat is new: a uniform encoding of program-as-resource ∀∃ relational triples into standard Hoare triples using a single predicate Exec, parameterized by a high-level postcondition X, with no ghost states or changes to the host logic. The proof of Theorem 4 is a straightforward semantic argument; the encoded assertion translations and the derivation of Low-Focus, High-Focus, Rel-Wh, and vertical composition as standard rules are all worked out. The case studies (mergesort, BST, DFS, KMP) and the machine-checked artifact are real evidence. The comparison with Roever–Engelhardt correctly identifies why uniformity of the pre/post encoding matters.\n\nWhere it is soft: the equivalence is proved only for the relaxed semantics given by configuration refinement (Definition 7/9). Section 8 is transparent about this, and the example ⟨x=y∧[skip]⟩ x:=x+1 ⟨x=y∧[y:=y−1]⟩ shows the two semantics diverge. The stress-test note is right that Theorem 4 would fail if Definition 1 were kept unchanged. This matters because the encoding is used to justify proof rules; intermediate relational judgments in the relaxed logic can be strictly more permissive, so the paper is not encoding the original ∀∃ relational logic. The practical refinement fragment ending with [skip] is unaffected, and the authors disclose the change, but the title and abstract should say 'a relaxed variant' rather than 'the ∀∃ relational Hoare logic.' A minor issue: the Zenodo artifact is referenced without a commit hash, so the formalization cannot be independently audited from the text.\n\nBottom line: sound on its stated terms, and a useful theoretical contribution even if narrower than advertised. It deserves serious peer review; the revision should focus on scoping the claims and being explicit about what the relaxed semantics buys and costs.","headline":"A clean, machine-checked encoding of a relaxed ∀∃ relational Hoare logic into standard Hoare logic; the title overstates the semantics, but the contribution is real and worth reviewing.","tokens_in":50774,"tokens_out":3003,"would_cite":true,"duration_ms":32529,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q60","03B70"],"pacs":[],"model":"deepseek-v4-flash","headline":"A single assertion encoding reduces ∀∃ relational Hoare logic to standard Hoare logic, proved under a relaxed refinement semantics.","keywords":["relational Hoare logic","program refinement","nondeterminism","assertion encoding","weakest precondition","configuration refinement","program-as-resource assertions","execution predicate"],"falsifier":"Run the paper's own counterexample: under the original multi-step semantics, the triple $\\langle x = y \\land [\\mathbf{skip}]\\rangle\\, x := x+1\\,\\langle x = y \\land [y := y-1]\\rangle$ is invalid because there is no small-step path from the initial configuration to the final configuration, while the configuration-refinement definition declares it valid and Theorem 4 proves the encoded standard triple.","tokens_in":49761,"feed_emoji":"🧩","tokens_out":8060,"duration_ms":77295,"temperature":0.7,"pith_summary":"The paper claims that the $\\forall\\exists$ relational Hoare logic used to prove refinement of nondeterministic programs can be embedded faithfully in ordinary standard Hoare logic, with no ghost states or invariant machinery. The key move is to redefine relational-triple validity using configuration refinement, a denotational inclusion of possible outcomes, instead of multi-step small-step transitions, and then to encode each program-as-resource assertion as a unary assertion over low-level states that existentially abstracts the high-level state and remaining high-level program. The main theorem states that a relational triple is valid exactly when every encoded standard triple, universally parameterized by a high-level postcondition $X$, is $\\forall$-valid. A syntactic form of the encoding uses a pure execution predicate $\\mathrm{Exec}_X(P^H,c^H)$ that the low-level proof can carry along with ordinary Hoare rules, so relational proof rules become derivable standard rules. If the encoding is right, existing standard-Hoare verification infrastructure can prove refinement without building or re-verifying a second program logic.","feed_headline":"Program refinement becomes standard Hoare logic","feed_subtitle":"Ordinary unary Hoare triples can now prove forall-exists refinement of nondeterministic programs, with no ghost-state machinery.","key_machinery":"The load-bearing object is configuration refinement: $(\\sigma_1,c_1)\\hookrightarrow(\\sigma_2,c_2)$ holds exactly when every terminal state reachable from $(\\sigma_2,c_2)$ by denotational semantics is reachable from $(\\sigma_1,c_1)$. Its decomposition theorem is what makes the encoding work: $(\\sigma_1,c_1)\\hookrightarrow(\\sigma_2,c_2)$ is equivalent to $\\forall X\\subseteq\\Sigma^H.\\ \\sigma_1\\models\\mathrm{wlp}(c_1,X)\\Rightarrow \\sigma_2\\models\\mathrm{wlp}(c_2,X)$. Because a refinement step becomes a universal implication over weakest preconditions, the existential 'choose a matching high-level execution' can be absorbed into the assertion encoding $\\llbracket\\cdot\\rrbracket_X$. The syntactic encoding introduces the pure execution predicate $\\mathrm{Exec}_X(P^H,c^H)$, read as 'there is a high-level state satisfying $P^H$ from which every $c^H$ outcome satisfies $X$'; proof rules update this predicate to emulate high-level evaluation steps.","core_discovery":"The central discovery is Theorem 4: for any low-level statement $c^L$ and program-as-resource assertions $\\mathcal{P},\\mathcal{Q}$, the relational triple $\\langle\\mathcal{P}\\rangle\\,c^L\\,\\langle\\mathcal{Q}\\rangle$ is valid if and only if, for every high-level state set $X$, the standard triple $\\{\\llbracket\\mathcal{P}\\rrbracket_X\\}\\,c^L\\,\\{\\llbracket\\mathcal{Q}\\rrbracket_X\\}$ is $\\forall$-valid. The encoding is $\\sigma^L \\models \\llbracket\\mathcal{P}\\rrbracket_X$ iff there exist $\\sigma^H,c^H$ with $(\\sigma^L,\\sigma^H,c^H)\\models\\mathcal{P}$ and $\\sigma^H\\models\\mathrm{wlp}(c^H,X)$. This turns the existential choice inside a relational proof into an existential quantifier inside an assertion, which standard Hoare logic can handle. The equivalence is proved under Definition 9, where the high-level update relation is configuration refinement rather than multi-step transition; the authors explicitly note that this relaxed validity makes some previously invalid triples valid, while preserving the intended refinement reading when the postcondition program is $\\mathbf{skip}$.","pith_inferences":["The relaxed validity trades exact trace alignment for denotational behaviour: refinement conclusions are about possible final results, not about matching every small step; full refinement still requires the postcondition program to be $\\mathbf{skip}$, but intermediate continuations in assertions are interpreted coarser than before.","A testable extension is to specialize the universal placeholder $X$ to the weakest precondition of a concrete high-level postcondition, yielding a proof rule for known input-output refinement that may recover exact small-step validity when the high-level language is deterministic.","The encoding suggests that adding an execution predicate to an existing unary verifier is a modular route to refinement checking; one could compare proof effort and automation against ghost-state-based refinement logics on the heap-manipulating case studies."],"forward_implications":["Any verification infrastructure for standard Hoare logic can prove refinement triples by adding the execution predicate, without re-proving soundness of a second logic.","Relational proof rules for sequencing, loops, nondeterministic choice, and the two vertical-composition rules become derivable standard rules, so relational proof steps correspond one-for-one to standard proof steps.","The placeholder $X$ is inert in practice: proofs operate on $\\mathrm{Exec}_X(P^H,c^H)$ by update rules, so users never need to construct $X$ explicitly.","The encoding extends to function calls, error behaviour, and separation-logic frame reasoning while preserving the same equivalence."],"supporting_citations":[{"why":"Introduces relational Hoare logic, the general framework that the encoding reduces to standard Hoare logic.","marker":"[8]"},{"why":"Supplies the program-as-resource assertion form over triples $(\\sigma^L,\\sigma^H,c^H)$ that the encoding targets.","marker":"[43]"},{"why":"Provides the weakest-precondition notion used in the decomposition theorem and in the definition of $\\mathrm{Exec}_X$.","marker":"[15]"},{"why":"Gives the decomposed assertion form with pure, low-level, high-level, and program components that the syntactic encoding is built on.","marker":"[19]"},{"why":"Establishes self-composition for $\\forall\\forall$ properties, the baseline that this $\\forall\\exists$ encoding extends beyond.","marker":"[7]"}],"fun_headline_variants":["Relational Hoare logic falls back to standard Hoare logic","Standard Hoare logic proves all-exists refinement","No ghost states needed for relational proofs","forall-exists refinement encoded in unary triples","Relational correctness from ordinary Hoare logic"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The central equivalence assumes the relaxed definition of relational validity via configuration refinement; under the original multi-step-transition semantics, the theorem as stated is not expected to hold.","fun_headline_variants_meta":{"raw":{"variants":["Relational Hoare logic falls back to standard Hoare logic","Standard Hoare logic proves all-exists refinement","No ghost states needed for relational proofs","forall-exists refinement encoded in unary triples","Relational correctness from ordinary Hoare logic"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000562,"raw_usage":{"total_tokens":2725,"prompt_tokens":1061,"completion_tokens":1664,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":677,"completion_tokens_details":{"reasoning_tokens":1592}},"tokens_in":677,"tokens_out":1664,"duration_ms":10433,"temperature":1.0,"reasoning_tokens":1592,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-16T10:39:12.257623+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the paper's own counterexample: under the original multi-step semantics, the triple $\\langle x = y \\land [\\mathbf{skip}]\\rangle\\, x := x+1\\,\\langle x = y \\land [y := y-1]\\rangle$ is invalid because there is no small-step path from the initial configuration to the final configuration, while the configuration-refinement definition declares it valid and Theorem 4 proves the encoded standard triple.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the weakest-precondition notion used in the decomposition theorem and in the definition of $\\mathrm{Exec}_X$."},{"cited_title":"ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity","cited_arxiv_id":"2006.13635","evidence_quote":"Gives the decomposed assertion form with pure, low-level, high-level, and program components that the syntactic encoding is built on."}],"review_version":1}