REVIEW 3 major objections 4 minor 1 cited by
Increasing the Expressiveness of a Gradual Verifier
T0 review · 3 major / 4 minor · reviewed 2026-08-06 · deepseek-v4-flash
Pith's one-line read This paper extends Gradual C0 with unfolding expressions for recursive heap data structures, preserving optimistic heap assumptions during evaluation to reduce run-time checks.
desk verdict Useful incremental design for adding unfolding expressions to Gradual C0, but the central safety claim needs a real soundness argument before it should land. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
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.
What would settle it
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.
Extended reading notes
Core claim
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.
Load-bearing premise
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.
Editorial extensions
If this is right
- 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.
Reading between the lines
- 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.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
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.
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 (3)
- [Appendix A / Fig. 1] 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 2 / Fig. 1 / Conclusion] 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 2 and Section 3] 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.
minor comments (4)
- [Section 2] "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.
- [Fig. 1] 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.
- [Fig. 1 / Section 2] 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.
- [References] Reference [9] lacks publication venue and year information; please complete the bibliographic entry.
Circularity Check
No circularity: the unfolding-expression design is an implementation proposal whose safety claim is asserted without a formal proof, but no step reduces to its own input or to a self-citation chain.
full rationale
The paper's central claim is that retaining optimistic heap chunks (h?) across an unfolding expression is safe and minimizes run-time checks. This is not a prediction fitted to data, nor is it equivalent by construction to its inputs. The modified eval rule in Figure 1 is an implemented design decision; its safety rests on an informal argument distinguishing precise predicate bodies, where the origin of optimistic chunks is known, from imprecise bodies, which are handled conservatively. The appendix explicitly notes the omission of Viper's join call, making the missing soundness argument an open correctness concern rather than a circular reduction. The cited prior work (Gradual C0, Viper, gradual verification) supplies background infrastructure and definitions, but is not used to define away the present result, and there is no self-citation chain that forces the design. The paper's equations do not reappear as outputs: the claimed run-time overhead reduction is an empirical design assertion awaiting benchmarks and a formal soundness proof. Therefore no circularity is present.
Assumptions & free parameters
assumptions (4)
- domain assumption Viper's symbolic execution logic and its eval rule for unfolding expressions are sound.
- domain assumption Gradual Viper's handling of imprecise formulas and optimistic heap chunks is sound and consistent with the new rule.
- ad hoc to paper The syntactic classification of a predicate body as precise or imprecise is sufficient to decide whether optimistic heap chunks may be retained.
- ad hoc to paper Omitting Viper's join call does not affect soundness for unfolding expressions with conditional predicate bodies.
Cite this review
Pith. "Pith review of Increasing the Expressiveness of a Gradual Verifier." pith.science (2026). https://pith.science/paper/OV24VICU
@misc{pith2026250713533,
author = {Pith},
title = {Pith review of: Increasing the Expressiveness of a Gradual Verifier},
year = {2026},
howpublished = {\url{https://pith.science/paper/OV24VICU}},
note = {Machine review of arXiv:2507.13533}
}
read the original abstract
Static verification provides strong correctness guarantees for code; however, fully specifying programs for static verification is a complex, burdensome process for users. Gradual verification was introduced to make this process easier by supporting the verification of partially specified programs. The only currently working gradual verifier, Gradual C0, successfully verifies heap manipulating programs, but lacks expressiveness in its specification language. This paper describes the design and implementation of an extension to Gradual C0 that supports unfolding expressions, which allow more intuitive specifications of recursive heap data structures.
Figures
Forward citations
Cited by 1 Pith paper
-
Gradually Verifying Unfolding Expressions & Pure Functions
Formal symbolic-execution and runtime semantics for unfolding expressions and pure functions in gradual verification, with a soundness proof extending Zimmerman et al.'s Gradual Viper formalization.
Reference graph
Works this paper leans on
-
[1]
Rob Arnold. 2010. C0, an imperative programming language for novice computer scientists . Master’s thesis. Department of Computer Science, Carnegie Mellon University
work page 2010
-
[2]
Johannes Bader, Jonathan Aldrich, and Éric Tanter. 2018. Gradual Program Verification. In International Conference on Verification, Model Checking, and Abstract Interpretation. Springer, 25–46. https://doi.org/10.1007/978-3-319-73721-8_2
-
[3]
Jenna DiVincenzo, Ian McCormack, Hemant Gouni, Jacob Gorenburg, Mona Zhang, Conrad Zimmerman, Joshua Sunshine, Éric Tanter, and Jonathan Aldrich. 2022. Gradual C0: Symbolic Execution for Efficient Gradual Verification. arXiv preprint arXiv:2210.02428 (2022)
work page Pith review arXiv 2022
-
[4]
Peter Müller, Malte H. Schwerhoff, and Alexander J. Summers. 2016. Viper: A Verification Infrastructure for Permission- Based Reasoning. In International Conference on Verification, Model Checking, and Abstract Interpretation . Springer, 41–62. https://doi.org/10.1007/978-3-662-49122-5_2
-
[5]
Matthew J. Parkinson and Gavin M. Bierman. 2005. Separation logic and abstraction. In ACM-SIGACT Symposium on Principles of Programming Languages . https://api.semanticscholar.org/CorpusID:6280787
work page 2005
-
[6]
Reducing urban traffic congestion due to localized routing decisions
J.C. Reynolds. 2002. Separation logic: a logic for shared mutable data structures. In Proceedings 17th Annual IEEE Symposium on Logic in Computer Science . 55–74. https://doi.org/10.1109/LICS.2002.1029817
work page Pith review arXiv 2002
-
[7]
Malte H. Schwerhoff. 2016. Advancing Automated, Permission-Based Program Verification Using Symbolic Execution . Ph. D. Dissertation. ETH Zürich. https://doi.org/10.3929/ethz-a-010835519
-
[8]
Jan Smans, Bart Jacobs, and Frank Piessens. 2009. Implicit dynamic frames: Combining dynamic frames and separation logic. In European Conference on Object-Oriented Programming . Springer, 148–172. https://doi.org/10.1145/2160910. 2160911
Show all 13 references
-
[9]
Alexander Summers and Sophia Drossopoulou. 2013. A Formal Semantics for Isorecursive and Equirecursive State Abstractions
2013
-
[10]
Jenna Wise, Johannes Bader, Cameron Wong, Jonathan Aldrich, Éric Tanter, and Joshua Sunshine. 2020. Gradual verification of recursive heap data structures. Proceedings of the ACM on Programming Languages 4, OOPSLA (2020), 1–28. https://doi.org/10.1145/3428296 Increasing the Ex...
2020 doi
-
[11]
its arity is |𝜎1.𝑞𝑣𝑠|
-
[12]
it can be applied to the argument vector 𝜎1.𝑞𝑣𝑠
-
[13]
its return sort matches 𝑏’s sort 𝑄(recunf(𝜎1.𝑞𝑣𝑠)) Fig. 1. Modified eval rule for unfolding expressions in Gradual Viper The eval rule for unfolding expressions in Viper [7] (defined in continuation-passing style) is modified (with highlighted parts) for Gradual Viper. Note,𝜎 ...
Reviewed August 6, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.