{"id":"71059ac8-d1c9-4e1d-8be7-6e736e46a464","arxiv_id":"2507.13533","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Gradual C0's specification language gains unfolding expressions through a modified symbolic-execution rule that retains optimistic heap chunks when predicate bodies are precise.","lead":"This paper extends the Gradual C0 verifier so that specifications of recursive heap data can use Viper's unfolding expressions, making them shorter and more intuitive. It is a design-and-implementation report for a niche tool, with no new theory and no benchmarks.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The central safety claim lacks a soundness argument for the modified unfolding rule: App. A omits Viper's join and preserves h? chunks with no invariant, so the claimed run-time-check reduction may hide a real unsoundness.","rationale":"The reader flagged the missing join, and I agree that is a live risk. The more load-bearing issue is the absence of any invariant for the h? preservation in Fig. 1: if the precise-body update retains chunks that are not justified after the heap reset, the central optimization is unsound, not merely unproven. The paper is honest in deferring soundness, but the central claim depends on that deferred proof. The proposed test is minimal and executable once the implementation is available. Since the claim is plausible and the paper is a design report, conditional acceptance remains appropriate; no verdict change is needed.","tokens_in":4798,"tokens_out":22343,"duration_ms":270070,"concrete_test":"Implement App. A's rule in Gradual C0 and run: predicate p(x) = q(x); predicate q(x) = acc(x.f); with a method requiring acc(p(x)), whose body first evaluates unfolding p(x) in (unfolding q(x) in x.f == x.f) and then executes unfold q(x);. If the verifier accepts the second unfold without emitting a runtime ownership check for q(x), the h?-preservation rule is unsound; if it rejects or inserts a check, the concern is resolved. Also compare verification of Listing 2 with and without the join: any branch whose runtime-check set differs indicates the omission is semantically observable.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 2's central claim is that retaining optimistic heap chunks across unfolding expressions is safe and reduces run-time checks. The only support is an informal example; the actual rule (Fig. 1) contains the decision. Two gaps make the claim unestablished. (1) The rule explicitly omits Viper's join call, but the paper gives no analysis of how branch divergence from conditional predicate bodies (e.g., Listing 2) is resolved; if the missing join merges or drops branches, soundness fails. (2) In the precise-body branch, h? is updated as sigma2.h? union sigma5.h? union pred(e'), retaining every optimistic chunk introduced while evaluating b. No invariant is stated showing that such chunks are still backed by sigma2's assumptions or by a runtime check after h is reset to sigma2.h. The paper merely asserts these predicates are 'soundly tracked'; the conclusion defers formal soundness. Without such an invariant, the claim that run-time overhead is minimized without sacrificing soundness is not established.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper describes an extension to the gradual verifier Gradual C0 (via its back-end Gradual Viper) that adds support for Viper-style unfolding expressions, allowing more intuitive specifications of recursive heap data structures such as sorted linked lists. The central design contribution is a modified evaluation rule for unfolding expressions that, after temporarily exposing a predicate body, resets the symbolic heap h but selectively retains the optimistic heap h? according to whether the predicate body is precise or imprecise. For precise bodies, h? is updated to the union of the pre-unfolding h?, the post-evaluation h?, and an instance of the unfolded predicate; for imprecise bodies, h? is reverted and only the predicate instance is added. The paper also adds branch-origin tracking for unfolding-induced branches. The authors argue that this design minimizes run-time checks while preserving soundness, but the conclusion defers a formal soundness proof.","tokens_in":4945,"tokens_out":2885,"duration_ms":33465,"significance":"If the design is sound, the extension meaningfully increases the expressiveness of Gradual C0's specification language and reduces the burden on users who need to reason about recursive heap structures, so the contribution is well-motivated for the gradual-verification community. The precise/imprecise distinction for retaining optimistic chunks is a sensible design idea, and origin tracking is a thoughtful adaptation of Gradual C0's existing branching machinery. However, the paper provides only an informal safety argument, explicitly defers soundness to future work, and reports no benchmarks or correctness tests for the claimed run-time-check reduction. The contribution is therefore best viewed as an implementation design with a plausible but unproven soundness argument, rather than a fully validated result.","major_comments":[{"comment":"The modified eval rule omits Viper's join call, and the appendix explicitly notes this omission, but the paper gives no analysis of how branch divergence after evaluating b with a conditional predicate body (as in Listing 2) is resolved in Gradual Viper's symbolic execution. If the missing join causes some branches to be dropped or merged unsoundly, then retaining h? chunks from those branches could make the verifier accept invalid programs. The paper should either define the missing merge semantics, provide a formal argument that Gradual Viper's architecture makes the join unnecessary, or give a concrete example showing how divergent branches from a conditional predicate body are tracked and checked.","section":"Appendix A / Fig. 1"},{"comment":"In the precise-body branch, h? is updated as sigma2.h? union sigma5.h? union pred(e'), retaining every optimistic chunk introduced while evaluating b, but no invariant is stated showing that these chunks remain backed by sigma2's assumptions or by run-time checks after h is reset to sigma2.h. The sentence \"Our extension ensures that predicates added to h? are soundly tracked\" is asserted rather than derived, and the conclusion defers formal soundness to future work. Without such an invariant, the paper's central claim that run-time overhead is minimized without sacrificing soundness is not established.","section":"Section 2 / Fig. 1 / Conclusion"},{"comment":"The paper claims that the design \"minimizes run-time overhead\" and achieves \"efficient gradual verification,\" but it reports no benchmarks, no comparison against the naive strategy of resetting both h and h?, and no test suite showing that the implementation verifies the example programs correctly and generates the expected dynamic checks. Since the efficiency claim is central to the paper's motivation, an experimental or at least an asymptotic comparison is needed to support it, unless the claim is explicitly scoped to a design-level qualitative argument.","section":"Section 2 and Section 3"}],"minor_comments":[{"comment":"\"Additonally\" should be \"Additionally\". The manuscript also relies on colored highlighting in the prose (e.g., \"highlighted in green\"), which may not survive printing; please describe the relevant constructs in words.","section":"Section 2"},{"comment":"The imprecise-body branch contains \"h ?\" with a space, which appears to be a formatting artifact for h?. The notation should be consistent throughout the figure and the text.","section":"Fig. 1"},{"comment":"The rule uses several unstated notions: the distinction between explicit and recursive (recunf) unfoldings, the meaning of scale, and the representation of predicate bodies. A brief explanation of these terms would make the rule accessible to readers not already familiar with Viper's internal formalization.","section":"Fig. 1 / Section 2"},{"comment":"Reference [9] lacks publication venue and year information; please complete the bibliographic entry.","section":"References"}],"recommendation":"major_revision","confidential_remarks":"The manuscript reads like a workshop or short-paper contribution: the idea is interesting, but the soundness gap around the missing join and the h? retention invariant is load-bearing and the empirical support is absent. I would encourage the authors to add a focused technical section that either proves the relevant preservation property for h? or provides a counterexample analysis of branch divergence, and to include at least a small case study with measured run-time checks. The self-referential limitation in the conclusion is appropriately honest and should be retained."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nShort version: this is a clear, focused design report for adding Viper's unfolding expressions to Gradual C0. It addresses a real limitation: specifying recursive heap structures without unfolding forces awkward auxiliary parameters. The design choices—retaining optimistic chunks only for precise predicate bodies, and origin tracking for branches—are sensible and explained with a good running example. The paper is honest about what it does and does not prove.\n\nWhat's genuinely new is the adaptation of the unfolding rule to the gradual setting, in particular the distinction between precise and imprecise predicate bodies for deciding whether h? chunks survive. That's a legitimate incremental contribution to a niche tool.\n\nThe soft spot is the central safety claim. The paper claims run-time overhead is minimized without sacrificing soundness, but the only support is an informal narrative. The appendix rule silently omits Viper's join call, and there's no analysis of what happens when a predicate body branches (like the conditional in Listing 2) and those branches rejoin after the unfolding. Without the join, branch divergence may be mishandled. Also, in the precise-body case, h? is updated to include all optimistic chunks introduced during evaluation of b, but no invariant ties those chunks back to the state after h is reset to sigma2.h. The paper's own conclusion defers formal soundness. These are not fatal objections to the design, but they are load-bearing gaps: the whole point is to preserve optimistic information safely, and safety is not demonstrated.\n\nThere are also no benchmarks or an implementation artifact, though the description suggests the code exists. For a tool paper, an artifact and at least a few measurements would help.\n\nThe citation pattern is fine: prior Gradual Viper work is the right background, and the paper builds on it without circularity.\n\nWho benefits: anyone working on gradual verification or extending Viper-based tools. It's a short read and worth serious referee time, but the referee should insist on a soundness argument (or proof) for the modified unfolding rule, a clarification of the join omission, and at least minimal evaluation. I'd accept it conditional on those. Bring it to reading group if you want a concrete example of design decisions in gradual verifiers.","headline":"Useful incremental design for adding unfolding expressions to Gradual C0, but the central safety claim needs a real soundness argument before it should land.","tokens_in":5420,"tokens_out":1616,"would_cite":true,"duration_ms":17298,"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":"This paper extends Gradual C0 with unfolding expressions for recursive heap data structures, preserving optimistic heap assumptions during evaluation to reduce run-time checks.","keywords":["gradual verification","symbolic execution","implicit dynamic frames","unfolding expressions","recursive predicates","optimistic heap","run-time checks","Viper"],"falsifier":"Run Gradual C0 on a method whose precondition unfolds a predicate whose body contains a conditional assertion with an imprecise branch, then execute the instrumented program with inputs that take each branch of that conditional; if the generated run-time checks do not cover the branch actually taken, or if two symbolic paths are merged without a check, the claimed soundness fails.","tokens_in":4539,"feed_emoji":"🔓","tokens_out":6729,"duration_ms":69952,"temperature":0.7,"pith_summary":"Gradually verified programs let users leave parts of the specification incomplete and still get sound checks, but the only working gradual verifier, Gradual C0, cannot express recursive heap data structures such as sorted lists without bending the specification around auxiliary parameters. This paper adds Viper's unfolding expressions to Gradual C0, so a predicate like sortedList can be opened temporarily inside a spec to talk about the data in the next node. The paper's central design choice is that after evaluating an unfolding expression, the verifier does not have to throw away the optimistically assumed heap permissions if the predicate body is precise; it can keep the useful ones and still be safe. That lets methods like frontInsert on a sorted list verify with fewer generated run-time checks than a naive full reset of the optimistic heap, while the same support is extended to branching origins when predicate bodies contain conditionals.","feed_headline":"Gradual C0 gains unfolding expressions for recursive heap specs","feed_subtitle":"Lets users specify sorted lists and other recursive structures without auxiliary parameters.","key_machinery":"The load-bearing object is the modified continuation-passing eval rule for the construct unfolding p(e) in b, which in Viper consumes the predicate instance, produces its body, evaluates b, and resets the symbolic heap h to its pre-consume version. The extension changes what happens to the separate optimistic heap h?: for a precise body it keeps the union of the pre-consume h? with the chunks assumed while evaluating b, for an imprecise body it reverts h?, and it always adds p(e) to h?. The rule also tracks a branch origin field, recording the unfolding expression when producing the predicate body introduces a branch and no origin was already in place. This machinery is what lets the verifier avoid a later run-time check for a permission that is still sitting in the optimistic heap.","core_discovery":"The core discovery is that optimistic heap information can outlive the temporary region of an unfolding expression without compromising soundness, provided the verifier distinguishes precise from imprecise predicate bodies. In the precise case, the produce step cannot have supplied the optimistically assumed chunks from inside the predicate, so those chunks must have come from the imprecision in the surrounding program and can be retained in the optimistic heap after the unfolding's symbolic heap is reset. In the imprecise case, the optimistic heap is reverted to its previous version to stay conservative, because the missing chunks could have originated in the predicate body itself. In both cases the unfolded predicate instance is added to the optimistic heap, since the consume step already framed it, and branch origins are set to the unfolding expression unless an enclosing method call or fold/unfold already defined them. The paper reports this as an implementation design in Gradual Viper, with the formal soundness proof left as future work.","pith_inferences":["A direct benchmark of frontInsert-style code against the naive full-reset strategy would quantify how many run-time checks the precise-body retention rule actually saves; the paper gives a running example but no measurement.","Because Gradual Viper omits the join call from Viper's original unfolding rule, a targeted soundness test should exercise a predicate whose body branches on an imprecise condition, to see whether both symbolic paths are still covered by appropriate run-time checks.","The precise/imprecise split is a binary heuristic; an alternative would be to tag each optimistic chunk with its origin and only retain chunks whose origin provably lies outside the predicate, which could recover more information in mixed cases.","If unfolding expressions reach pure functions, the same rule could also support user-defined inductive definitions inside predicates, further closing the expressiveness gap with fully static verifiers."],"forward_implications":["Users can specify sortedness of a linked list directly by unfolding sortedList(this.next), removing the need for the auxiliary prev parameter.","Recursive invariants that previously forced extra stored data, such as AVL balance conditions, can be expressed in the specification language instead.","Because unfolding expressions are side-effect free, supporting them in specifications prepares the way for their use inside pure functions, listed as a future extension.","The design reduces run-time checks in partially specified code by keeping newly assumed optimistic permissions after a precise unfolding, so later fold operations need no extra check.","The proposed 'options heap' construct suggests a path to choosing among several framing options for an imprecise formula, making framing more efficient as a follow-up."],"supporting_citations":[{"why":"Provides the Gradual C0 verifier and its optimistic heap h? machinery that the extension builds on.","marker":"[3]"},{"why":"Defines Viper and the unfolding expression construct whose eval rule is modified.","marker":"[4]"},{"why":"Details Viper's continuation-passing-style symbolic execution eval rule that the modified rule derives from.","marker":"[7]"},{"why":"Supplies implicit dynamic frames, including acc(...) permissions and recursive predicates, the underlying model for heap permissions.","marker":"[8]"},{"why":"Establishes the iso-recursive treatment of predicates, which is why explicit unfolding is needed to access predicate bodies.","marker":"[9]"},{"why":"Earlier work on gradual verification of recursive heap data structures frames the problem this extension addresses.","marker":"[10]"}],"fun_headline_variants":["Unfolding expressions enrich gradual verifier's recursive heap specs","Gradual C0 adds unfolding for intuitive recursive data specs","More expressive specs via unfolding in gradual verification","Unfolding expressions open recursive structures to gradual checking"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The design assumes that omitting the join call from Viper's original unfolding eval rule does not break soundness when a predicate body contains conditional assertions, since Gradual Viper has no join mechanism and the paper offers no analysis of how diverging branches are reconciled.","fun_headline_variants_meta":{"raw":{"variants":["Unfolding expressions enrich gradual verifier's recursive heap specs","Gradual C0 adds unfolding for intuitive recursive data specs","More expressive specs via unfolding in gradual verification","Unfolding expressions open recursive structures to gradual checking"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000237,"raw_usage":{"total_tokens":1434,"prompt_tokens":796,"completion_tokens":638,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":412,"completion_tokens_details":{"reasoning_tokens":574}},"tokens_in":412,"tokens_out":638,"duration_ms":7408,"temperature":1.0,"reasoning_tokens":574,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T16:21:57.526016+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run Gradual C0 on a method whose precondition unfolds a predicate whose body contains a conditional assertion with an imprecise branch, then execute the instrumented program with inputs that take each branch of that conditional; if the generated run-time checks do not cover the branch actually taken, or if two symbolic paths are merged without a check, the claimed soundness fails.","supporting_citations":[{"cited_title":"Gradual C0: Symbolic Execution for Gradual Verification","cited_arxiv_id":"2210.02428","evidence_quote":"Provides the Gradual C0 verifier and its optimistic heap h? machinery that the extension builds on."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies implicit dynamic frames, including acc(...) permissions and recursive predicates, the underlying model for heap permissions."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Establishes the iso-recursive treatment of predicates, which is why explicit unfolding is needed to access predicate bodies."}],"review_version":1}