{"id":"a847dfcc-389e-4f40-b1d4-eb1e03b3504a","arxiv_id":"2607.15383","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"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.","lead":"This paper writes down formal rules for two specification features — unfolding expressions and pure functions — used by the Viper family of program verifiers, and extends a hand-written soundness proof to cover them. The proof is thorough and clearly structured but is not machine-checked, and its two hardest parts (recursive constructs, and the mutual dependence between expression and formula lemmas) are handled by design choices and an asserted induction.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Missing well-founded measure for mutual induction between evaluation and consume/produce lemmas threatens soundness proof.","rationale":"The reader identified the missing well-founded measure as the weakest assumption, and my independent review agrees. I examined other potential concerns—the recursion-cut correspondence in Definition 36, the implicit rules' fresh values, and the asserted conservativity to Silicon—but these are either handled in the paper's own text or do not create an internal contradiction. The mutual induction between Lemmas 26 and 43 is the single most load-bearing issue because if the induction principle is not well-founded, the central soundness claim is unproven. The paper explicitly flags this in Section 4 and asserts a realization without giving the measure. This warrants the CONDITIONAL verdict: the authors must supply the missing measure. Since the reader already reached CONDITIONAL, my assessment does not change the verdict.","tokens_in":94157,"tokens_out":5763,"duration_ms":62745,"concrete_test":"Independently define a size measure |·| on Expr ∪ Formula (e.g., counting syntax nodes after one-level predicate-body expansion at unfolding/function boundaries) and check that in every mutual call between Lemma 26 and Lemma 43 the measure strictly decreases. Specifically, for Lemma 26 Case 13 (SEvalUnfoldingPrecise), compare |unfolding p(e) in e0| against the size of the premise σ2 ⊢ p(e) ▷ σ3 and the produce premise σ3[...] ⊢ predicate(p) ◁ σ4, where predicate(p) is the body. If no such decreasing measure can be defined, the claimed 'mutual induction' is not well-founded. A mechanized proof in Rocq/Coq would settle this definitively.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The soundness proof's central induction is not demonstrated. Appendix D proves Lemma 26 (Soundness of evaluation) by induction on the evaluation derivation, but in Cases 13/17 (SEvalUnfoldingPrecise and SEvalFunctionExplicit) it invokes Lemma 43 (Soundness of consume). Lemma 43 is proved by induction on the consume derivation, and its cases (e.g., SConsumePredicate, SConsumeAcc) invoke Lemma 26 to evaluate argument expressions. This mutual dependency is acknowledged in Section 4: the paper notes that expression lemmas and formula lemmas now depend on each other and asserts this 'can be proved by induction on the size of the term' and is 'concretely realize[d] via mutual induction over the previous decoupled theorems.' However, neither the size measure nor the mutual induction principle is supplied. This is not a cosmetic gap: the symbolic footprint (Appendix C.3) and exact footprint (Definition 5 / Appendix B.4) substitute predicate bodies, so substituted terms can be larger than the original instances; the evaluation rules for unfolding and pure functions thread produce/consume between mutually recursive constructs. Without an explicit well-founded order on Expr ∪ Formula, the induction in Lemmas 26 and 43 may be circular. The recursion-cut correspondence (Definition 36) is a secondary concern, but it is not fatal: it only defines valuations for existing runtime evaluations, so it does not introduce circularity by itself.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper formalizes symbolic-execution semantics for unfolding expressions and pure functions in Viper-style implicit-dynamic-frames verifiers, extends these semantics to the gradual verifier Gradual C0/Gradual Viper with imprecise specifications and run-time checks, and claims a soundness proof for the resulting system. The static and gradual inference rules (Figures 4, 6, 8, 11), the dynamic evaluation/framing rules (Figures 12–13), and the state-correspondence machinery are presented in detail, with a large appendix containing the lemmas and theorems that are supposed to establish progress and preservation. The central claim is that, if these rules are correct, a program that passes static verification will only fail at run time when a generated run-time check fails.","tokens_in":94447,"tokens_out":7428,"duration_ms":85044,"significance":"The target constructs are widely used in Viper-based verifiers (Gobra, Nagini, SnaKt), and the paper addresses a real gap: prior formalizations of Viper and Gradual C0 do not cover unfolding expressions or pure functions. If the soundness result is established, it would also transfer to static symbolic-execution backends by conservative extension, which would be a useful contribution to the verification community. The paper gives a careful, example-driven account of several delicate design choices (visited sets for recursion cutoff, heap snapshots via symbolic footprints, optimistic heaps and run-time checks, correspondence between symbolic and dynamic states), and it is honest about its limitations. However, the proof of soundness is hand-written, explicitly not mechanized, and contains an unresolved mutual-induction step that is load-bearing for the main theorem. The paper is therefore best regarded as a substantial formalization effort and proof sketch that needs completion before the soundness claim can be accepted.","major_comments":[{"comment":"The soundness proof has a genuine circularity that is acknowledged but not resolved. Lemma 26 (Soundness of evaluation) is proved by induction on the evaluation derivation, but its Cases 13 and 17 invoke Lemma 43 (Soundness of consume); Lemma 43 is derived from Lemma 41, whose proof cases (SConsumeValue, SConsumePredicate, SConsumeAcc) invoke Lemma 26 to evaluate argument expressions. Section 4 asserts that this can be handled by induction on the size of the term and by mutual induction, but no concrete size measure is supplied. This is not cosmetic: the footprint definitions in Appendix B.4 and C.3 substitute predicate and function bodies, which need not be syntactic subterms and can be larger than the original instance, and the evaluation rules for unfolding and pure functions consume formulae that are not subexpressions of the original expression. Please provide an explicit well-found","section":"Section 4 / Appendix D, Lemma 26 vs. Lemma 41"},{"comment":"The text says that lemmas stated without proof 'have the same proof as Zimmerman et al.' This is not enough in the new dependency graph. The prior proof had a one-directional dependency of consume lemmas on the evaluation lemma; the new Lemma 26 has cases that call consume lemmas, so Lemma 41 now depends on Lemma 26 for the very cases that were previously independent. Key lemmas such as 42 and 43 are not proved in this manuscript, and their previous proofs cannot be assumed to carry over unchanged. Since the central claim is soundness, the authors should either prove the adapted lemmas in the new setting or provide a machine-checked proof artifact that makes the dependency graph explicit and verifiable.","section":"Appendix D, first paragraph (inherited lemmas)"},{"comment":"The grammar permits pure-function applications inside expressions, hence inside function postconditions (func_post), but the axiomatize function is defined only for literals, variables, field accesses, binary/logical operators, and unfolding expressions. There is no case for a pure-function call, including nested calls. Consequently, SEvalFunctionExplicit and SEvalFunctionImplicit are under-defined for a function whose postcondition contains another pure-function application. This is a load-bearing incompleteness in the formal semantics, not a presentation issue. Either extend axiomatize with a recursive case for pure-function calls and prove a matching soundness property, or explicitly restrict the grammar/well-formedness conditions to exclude such postconditions.","section":"Appendix C.6, axiomatize definition; Appendix A grammar"}],"minor_comments":[{"comment":"The last sentence says 'where V′ is the corresponding valuation extending V′'; this should presumably be 'extending V'. Please correct the typo.","section":"Theorem 2 statement"},{"comment":"References [32] and [33] appear to be the same paper by the same authors with the same title and year, cited with different publication details. This is confusing; please consolidate into a single reference or explicitly explain why two entries are needed.","section":"References [32] and [33]"},{"comment":"The notation T𝑒U⟨𝐻,𝜌⟩ ;⟨ℓ, 𝑓⟩ in the exact-footprint clauses is unclear; it appears to mean union with the singleton {⟨ℓ,𝑓⟩}. Please define the intended operation explicitly.","section":"Appendix B.4, footprint notation"},{"comment":"The static rules in Figures 8 and 11 branch on whether a predicate or function body is 'precise'/'imprecise'. Definition 3 defines 'completely precise' for formulas, but it would help to state explicitly how this is decided statically for a predicate body, especially when predicate bodies refer to other predicates, and to confirm that 'imprecise' means 'not completely precise'.","section":"Definition 3 / Figures 8 and 11"}],"recommendation":"major_revision","confidential_remarks":"This is a same-group extension of Zimmerman et al.'s formalization of Gradual C0. The missing well-founded measure for the mutual induction in the soundness proof is a genuine technical gap, and the unproved inherited lemmas should not be assumed to transfer unchanged once the dependency graph changes. I see no reason to suspect bad faith or a fundamental flaw beyond this gap; the paper is careful and informative. I would be willing to accept after the authors supply the missing induction order and either prove or mechanize the adapted lemmas."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Here's my take on arXiv:2607.15383. The paper does something genuinely useful: it gives the first formal semantics for unfolding expressions and pure functions in the Viper/Silicon symbolic-execution family, and extends a gradual verification soundness proof to cover them. That gap is real—prior formalizations of Viper skip these constructs, and they are used in verified codebases like VerifiedSCION and the verified Go standard library. The rule design in Figures 4, 6, 8, and 11–13 looks consistent with the implementations it describes, and the paper is honest about what it did and did not do.\n\nThe soft spot is exactly where the stress-test note lands. The soundness proof has a genuine mutual dependency: the evaluation lemma calls the consume lemma, and the consume lemma calls back into evaluation. The paper says this is handled by \"induction on the size of the term\" and mutual induction, but never gives the size measure. With footprints that substitute predicate bodies, the substituted term can be larger than the original instance, so it is not obvious the induction is well-founded. That is a load-bearing gap in a proof whose whole point is soundness. It may be fixable, but it is not a cosmetic omission.\n\nTwo lesser issues. First, the recursion-cut rules replace recursive evaluation with an uninterpreted fresh value, and Definition 36 simply asserts that this value corresponds to the full runtime result; later path-condition constraints on that value are not addressed. Second, the transfer of the result to the static Silicon backend is asserted via conservativity of the gradual extension, but no conservativity lemma is derived for the new rules. And the proof is hand-written, not mechanized—the authors say so themselves.\n\nNone of this convinces me the paper is wrong. The semantics look plausible, the examples check out, and the related work is handled fairly. But the central claim is a soundness proof, and the proof as written has a hole in its induction structure. That is a conditional accept: the authors need to supply the missing well-founded measure and spell out the recursion-cut correspondence.\n\nThe audience is PL and verification researchers working on Viper, gradual verification, or symbolic-execution soundness. It deserves a serious referee—send it to peer review. I would want the missing measure and a clearer correspondence argument before signing off, but this is the right paper at the right time.","headline":"Useful formalization of a real gap, but the soundness proof relies on a mutual induction whose well-foundedness is never demonstrated.","tokens_in":95064,"tokens_out":2170,"would_cite":true,"duration_ms":26365,"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":"Gradual verification of unfolding expressions and pure functions is sound: accepted programs always pass the generated runtime checks.","keywords":["gradual verification","symbolic execution","unfolding expressions","pure functions","implicit dynamic frames","soundness proof","runtime checks","Viper"],"falsifier":"Run a verified program that uses a recursive pure function with an imprecise precondition and an inner expression that reads a field optimistically assumed during a recursive call—for instance, the paper's sum example with 'requires ?' and body 'node != null ? node.val + sum(node.next) : 0'—and execute the client. If the generated run-time checks omit a needed field or any check fails on a program the verifier accepted, the soundness theorem is false. A second check: mechanically verify the mutual induction over Expr ∪ Formula and see whether a decreasing measure can actually be constructed.","tokens_in":93903,"feed_emoji":"✅","tokens_out":6438,"duration_ms":61647,"temperature":0.7,"pith_summary":"Unfolding expressions and pure functions are the workhorse constructs that make ownership-based specifications modular—unfolding temporarily opens a predicate to reach the fields it owns, and pure functions let specifications call recursive heap-dependent functions—yet neither had a formal semantics or soundness proof for symbolic-execution verifiers. This paper supplies both for a static verifier and extends them to a gradual verifier, where imprecise specifications create optimistic assumptions that are backed by runtime checks. The central result is a soundness theorem for the new rules: whenever the verifier accepts a program, the run-time checks it generates will all succeed during execution, so there is no false acceptance. Because the gradual verifier is a conservative extension of the static one, the result transfers to the static symbolic-execution backend underlying several Viper-based tools. If correct, this closes a foundational gap for modular verification and makes gradual verification a viable route for real codebases that already rely on these constructs.","feed_headline":"Gradual verifier's unfolding and pure-function rules proven sound","feed_subtitle":"Any program the verifier accepts passes its own generated runtime checks, covering Viper's symbolic-execution backend too.","key_machinery":"The symbolic state σ = ⟨ι, H, H, γ, g, V⟩—imprecision flag, precise heap, optimistic heap, store, path condition, and a visited set of already-unfolded predicates/functions—along with the evaluation rules SEvalUnfolding* and SEvalFunction* that consume a predicate/precondition, produce its body, evaluate the inner expression under the temporary permissions, then restore the state. The visited-set recursion cutoff replaces recursive evaluations with fresh uninterpreted values, and the symbolic footprint J·Kσ computes the heap snapshot needed to evaluate pure-function bodies and postconditions. Soundness is carried by corresponding valuations that map symbolic values to the concrete values of","core_discovery":"The paper's claim, on its own terms, is that the symbolic-evaluation rules for unfolding expressions and pure-function applications—Figures 4, 6, 8, 11 through 13—together with the extended dynamic semantics and correspondence, are sound. Concretely, Theorems 1–3 establish progress and preservation: a valid dynamic state can always take a step when the matching run-time checks are satisfied, and every step preserves validity. The proof introduces the machinery that makes this hold: a visited set cuts unbounded recursion by replacing recursive unfolding/function evaluation with an uninterpreted fresh value (while still checking the predicate/precondition exists), a symbolic footprint snapshot","pith_inferences":["The mutual recursion between expression and formula semantics in the soundness proof suggests that any future construct mixing the two—quantified permissions, fractional permissions—will need the same coupled induction; the paper's structure provides a template.","The proof's asserted-but-unstated size measure for the mutual induction invites mechanization; formalizing this proof in a proof assistant would either produce the missing measure or expose a gap.","A concrete testable prediction: in recursive-pure-function-heavy verified code, the recursion-cut incompleteness should rarely surface; measuring how often manual unfolding is needed could quantify the practical cost.","The visited set could be replaced by a multiset to allow a configurable recursion cutoff depth, which the paper notes; this suggests an easy experimental knob for balancing completeness and termination."],"forward_implications":["Accepted programs can no longer fail their own checks: the generated run-time checks are guaranteed to hold on every execution of a verified program.","Static symbolic-execution verifiers built on the same backend inherit the soundness result, since gradual verification reduces to static verification on fully-specified programs.","Developers can use unfolding expressions and recursive pure functions in specifications without worrying about unsoundness from recursion cutoffs—the cutoff is incomplete but never unsound.","Imprecise specifications with '?' can now cover heap-dependent expressions, with the verifier generating runtime checks for optimistically assumed fields and predicate instances.","The semantics pin down when optimistic assumptions survive an unfolding: retained for imprecise initial states, discarded for imprecise predicate bodies—a distinction that future verifier implementations can rely on."],"fun_headline_variants":["Soundness proven: gradual verifier's unfolding and pure-function rules","Unfolding & pure functions: soundness proof for gradual verification","Progress and preservation prove gradual verifier sound for unfolding & pure functions","Gradual verifier's pure functions and unfolding expressions: soundness theorem"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The proof stands on a well-founded mutual induction over expressions and formulas—a size measure that the paper asserts but never defines—and on the recursion-cut rules' fresh uninterpreted values faithfully representing the full runtime result of the skipped evaluation.","fun_headline_variants_meta":{"raw":{"variants":["Soundness proven: gradual verifier's unfolding and pure-function rules","Unfolding & pure functions: soundness proof for gradual verification","Progress and preservation prove gradual verifier sound for unfolding & pure functions","Gradual verifier's pure functions and unfolding expressions: soundness theorem"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000697,"raw_usage":{"total_tokens":2967,"prompt_tokens":706,"completion_tokens":2261,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":450,"completion_tokens_details":{"reasoning_tokens":2185}},"tokens_in":450,"tokens_out":2261,"duration_ms":17280,"temperature":1.0,"reasoning_tokens":2185,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-01T23:31:50.337065+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run a verified program that uses a recursive pure function with an imprecise precondition and an inner expression that reads a field optimistically assumed during a recursive call—for instance, the paper's sum example with 'requires ?' and body 'node != null ? node.val + sum(node.next) : 0'—and execute the client. If the generated run-time checks omit a needed field or any check fails on a program the verifier accepted, the soundness theorem is false. A second check: mechanically verify the mutual induction over Expr ∪ Formula and see whether a decreasing measure can actually be constructed.","supporting_citations":[],"review_version":1}