Pith. sign in

REVIEW 3 major objections 5 minor 22 references

Unfolding Iterators: Specification and Verification of Higher-Order Iterators, in OCaml

T0 review · 3 major / 5 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Higher-order iterators in OCaml can be specified with permitted/complete predicates and verified automatically by translation into first-order cursor programs.

desk verdict Useful, honest tool paper on verifying higher-order OCaml iterators, but its central guarantee is undercut by an unproven translation equivalence, so the VCs only certify the generated code. read the letter →

arxiv 2506.20310 v1 pith:KARLDYFE submitted 2025-06-25 cs.PL cs.LO

Ion Chirica , Mário Pereira This is my paper · ORCID
classification cs.PLcs.LO
keywords deductiveverificationhigher-orderiteratorsGospelCameleercursortranslationpermitted/completepredicatesOCamlSMTsolving
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper aims to make formal verification of higher-order iteration in OCaml practical by giving a generic specification and a translation-based proof method. The method captures any iteration through two logical predicates, permitted and complete, plus a user-supplied invariant, and then translates the higher-order iterator into a first-order cursor while-loop. Verification conditions for the translated code are discharged automatically by SMT solvers, so the user never reasons about generated WhyML. If correct, this makes the verification of iteration-heavy OCaml code, including graph algorithms from OCamlGraph, quasi-automatic.

What carries the argument

The cursor: an abstract first-order object holding the sequence of elements visited so far plus two predicates, permitted (the visited sequence is a valid prefix of the iteration) and complete (the iteration is finished). The paper embeds these predicates inside the cursor type as a type invariant and builds two translation schemas around it: one turns a higher-order function declaration into a cursor create function, and the other turns each higher-order call into a while-loop using has_next and next. These schemas are the load-bearing mechanism because they convert a higher-order problem into the first-order form that Why3 and SMT solvers can attack automatically.

What would settle it

Take a fold over a mutable collection in which the consumer, upon visiting an element, also deletes that element from the collection; the translated cursor program iterates over a snapshot and proves its specification, while the original fold's errors or results differ. Any single case where the translated program's verification conditions all discharge but the original OCaml code violates the same postcondition settles that the translation is not meaning-preserving.

Watch

Extended reading notes

Core claim

The paper's central claim is that higher-order iterators such as fold, iter, filter, and map can be unfolded into first-order cursor programs without loss of meaning, and that this unfolding enables modular, mostly automatic deductive verification. A fold declaration annotated in Gospel is translated into a cursor creator whose type carries permitted and complete predicates; each call site is translated into a while-loop over has_next and next, with the variant and invariant taken from the user's specification. iter, filter, and map are treated as degenerate cases of fold, and nested iterations are handled by threading the outer iteration's invariant into the inner one. The approach is validated on lists, binary trees, and OCamlGraph graph operations, with all generated verification conditions automatically dispatched.

Load-bearing premise

The load-bearing premise is that translating a higher-order iterator into a first-order cursor while-loop preserves the behavior of the original OCaml program; the authors state this equivalence is supported only by an informal argument, not a formal proof.

Editorial extensions

If this is right

  • Users of OCaml libraries can verify clients of higher-order iterators by writing only the iteration invariant; the tool derives the loop, its variant, and its proof obligations.
  • Supporting fold alone covers iter, filter, and map, so the same specification machinery generalizes across the standard iteration patterns.
  • Nested higher-order iterations verify like nested loops: each inner iteration must preserve the invariants of all enclosing iterations.
  • The OCamlGraph case study indicates the method scales to real library code, with all 275 generated verification conditions for the graph modules discharged automatically.
  • Re-verifying the check_path algorithm with the new method needs about half the verification conditions of the previous manual approach.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Inference: the only unproven link in the chain is the meaning-preservation of the translation schemas; a formal relational proof between original iterator and cursor loop would make the methodology's automated proofs sound guarantees about the original source.
  • Inference: the permitted/complete encoding is expressed in first-order logic and does not depend on OCaml-specific features, so the same specification style could be ported to other languages whose verification backends target SMT solvers.
  • Inference: the reported costs suggest specification effort, not proof interaction, is the main bottleneck, so future work on inferring or synthesizing permitted/complete predicates and invariants would be the most direct scaling path.
  • Inference: the schemas assume the iteration's only effects are those of the consumer function; iterations where the consumer mutates the collection being traversed sit outside the current coverage and would need an extended cursor model.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper proposes a specification and automatic-verification methodology for higher-order iterators in OCaml. It extends the Gospel specification language with iterator-specific keywords (folds, iters, etc.) and extends the Cameleer verification tool to translate higher-order iterator declarations and calls into first-order cursor-based WhyML programs, relying on the permitted/complete predicates and a user-supplied iteration invariant. The approach is evaluated on list, graph (OCamlGraph), and tree case studies; all generated verification conditions are reported as automatically discharged by Alt-Ergo. The central claim is that this yields quasi-automatic deductive verification of clients of higher-order iterators.

Significance. If the translation from higher-order iterator calls to cursor loops were proved sound, the work would be a valuable step: it would allow Cameleer users to verify realistic OCaml code that uses higher-order iteration without manually desugaring iterators, and the OCamlGraph case study demonstrates that the methodology scales to nontrivial imperative code. Strengths include the availability of an online artifact, the use of existing real-world library code, and the honest, explicit statement in Section 10 that translation correctness is currently based on an informal argument. The main weakness is that the central guarantee—that proving the generated cursor program proves the original OCaml program—is not formally established, and the displayed specifications in the graph case study contain ambiguities.

major comments (3)
  1. [§10, 'Relational equivalence'; §6.1–6.2] The correctness of the translation schemas is the load-bearing premise of the paper, yet Section 10 explicitly defers it to future work: "The correctness of our translation schemas is based on an informal argument that a higher-order iterator can be converted in a cursor that plays the iteration part." The VCs in Table 1 are discharged against the generated WhyML cursor programs, so without a soundness argument for the §6 schemas, those proofs do not formally establish properties of the original OCaml higher-order calls. I request either a formal statement and proof (or at least a rigorous proof sketch) of a simulation or relational-equivalence theorem between each schema and the original iterator, or a substantial weakening of the paper's claims to say that the method verifies the generated cursor programs.
  2. [§8.2, with §6.2] The specifications for fold_vertex and fold_succ constrain only membership and distinctness (and cardinality for the complete predicate), not the iteration order. The generated loop in §6.2 fixes an evaluation order: call next, then apply the consumer to the accumulator and the new element. The actual OCamlGraph iterator may enumerate vertices or successors in any order, and for side-effecting consumers, which the paper explicitly supports in §7, observable behavior depends on this order. No argument is given that the real iterator is simulated by any cursor satisfying these predicates, so the discharged VCs do not establish that the original OCamlGraph call has the specified behavior.
  3. [§8.3, with §8.2] The displayed invariants are ill-typed as written: `visited` is declared a `vt seq`, while `g2.dom` is a `vt fset`, yet the formulas `acc.dom = visited g2.dom` and `acc'.suc src = visited' (g2.suc src)` use set union between the two types, with no coercion or conversion described. Additionally, the Gospel header for fold_succ in §8.2 binds the result as `r = fold_succ func acc pair`, but the accompanying OCaml signature has four arguments and no parameter named `pair`. Since the graph case study is the main validation, these ambiguities must be resolved, either by correcting the display or by stating the exact Gospel declarations used in the artifact.
minor comments (5)
  1. [Title and §1] The text uses "high-order" in several places (e.g., the title, abstract, and introduction), where the intended term is "higher-order."
  2. [§6.2] The schema's first generated line reads `let acc = ref x 0 in`, which appears to be a typo for `ref x0` (or `ref x_0`); additionally, the schematic example `fold (fun a e -> ...) col x 0` has an argument order inconsistent with the fold signature shown earlier in §5.
  3. [§6.3] The formula `invariant { I B ( l ' i=0 (!ai)? (v i)) }` is under-specified: the meaning of `B`, the optional annotation `(!ai)?`, and the indexing convention `(v i)` are not defined, making the nested-iteration rule hard to reproduce.
  4. [§8.3] In the postcondition `gr.dom = g1.dom g2.dom`, the union symbol appears to be missing between `g1.dom` and `g2.dom`.
  5. [§9] The phrase "permitted{complete methodology" contains a stray brace from the source formatting; it should read "permitted/complete methodology."

Circularity Check

0 steps flagged · score 1.0 of 10

No circular derivation: the verified VCs target generated cursor programs, and the only gap—the unproved translation equivalence—is an explicitly acknowledged soundness limitation, not an input-output reduction.

full rationale

The paper's central claim is that higher-order iterator clients can be specified via permitted/complete predicates and verified by translating calls into first-order cursor loops. The verification conditions are generated for the translated WhyML code and discharged by SMT solvers; this is not circular because the predicates, invariants, collections, and convergence terms are user-supplied logical content, and the VCs assert properties of the cursor computation relative to those predicates. For example, the postcondition of sum_fold is the mathematical sum over the whole sequence, which is not identical to the loop invariant; it follows only through the complete predicate. The permitted/complete framework and cursor type are inherited from prior work, including Filliâtre and Pereira 2016, whose second author is also an author of this paper, but the citation is not the sole support for the new results: the paper applies the framework to independent case studies and reports SMT-discharged VCs. Cameleer and Gospel are also author-related tools, but their outputs are externally checkable and are not being used as an unverified premise. The one genuine caveat is that the correctness of the §6 translation schemas is not formally proved: Section 6 describes the schemas informally, and Section 10 explicitly says 'The correctness of our translation schemas is based on an informal argument that a higher-order iterator can be converted in a cursor that plays the iteration part,' listing relational equivalence as future work. This is a soundness/completeness gap in the methodology, not circularity: the paper does not claim to have proved the equivalence, and the gap is between the original OCaml iterator and the generated cursor, not a reduction of the conclusions to the assumptions by construction. No step in the derivation equates its output with its input by definition, so no circular step is exhibited.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The paper introduces no numerical fitted parameters; the main assumptions are the correctness of the permitted/complete predicate method inherited from prior work, the soundness of the translation schemas (acknowledged as informal in Section 10), and standard set-theoretic facts. No new physical or logical entities are postulated beyond the cursor type with embedded predicates, which is a program-level abstraction.

assumptions (4)
  • domain assumption The permitted predicate is a valid invariant of the cursor type: at any point before a function call, the visited sequence is permitted.
    Embedded as a type invariant in the WhyML cursor declaration (Section 4). This is assumed, not proven, for arbitrary instantiations.
  • ad hoc to paper The translation schemes from higher-order iterators to first-order cursor loops preserve program semantics.
    The authors state in Section 10 that correctness of the translation schemas is based on an informal argument; no formal proof is provided.
  • standard math The predicate 'complete' for fold_succ, based only on cardinality equality, correctly implies set equality.
    Used in Section 8.2; relies on the standard set-theoretic result that a subset with the same cardinality as its superset is equal, for finite sets.
  • domain assumption The permitted/complete predicates from Filliâtre and Pereira (2016) are correct for first-order iteration.
    The work builds directly on [15], which is cited and assumed as the foundation; this is a legitimate reuse of prior published work.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Unfolding Iterators: Specification and Verification of Higher-Order Iterators, in OCaml." pith.science (2026). https://pith.science/paper/KARLDYFE

@misc{pith2026250620310,
  author       = {Pith},
  title        = {Pith review of: Unfolding Iterators: Specification and Verification of Higher-Order Iterators, in OCaml},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/KARLDYFE}},
  note         = {Machine review of arXiv:2506.20310}
}
read the original abstract

Albeit being a central notion of every programming language, formally and modularly reasoning about iteration proves itself to be a non-trivial feat, specially in the context of higher-order iteration. In this paper, we present a generic approach to the specification and deductive verification of higher-order iterators, written in the OCaml language. Our methodology follows two key principles: first, the usage of the Gospel specification language to describe the general behaviour of any iteration schema; second, the usage of the Cameleer framework to deductively verify that every iteration client is correct with respect to its logical specification. To validate our approach we develop a set of verified case studies, ranging from classic list iterators to graph algorithms implemented in the widely used OCamlGraph library.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

22 extracted references · 16 canonical work pages

  1. [1]

    Astrauskas, V., Müller, P., Poli, F., Summers, A.J.: Leveraging Rust types for Modular Specification and Verification. Proc. ACM Program. Lang.3(OOPSLA), 147:1–147:30 (2019). https://doi.org/10.1145/3360573

    doi:10.1145/3360573 2019

  2. [2]

    SIGPLAN Not.39(1), 14–25 (Jan 2004).https://doi.org/10

    Benton, N.: Simple Relational correctness proofs for Static Analyses and Program Transformations. SIGPLAN Not.39(1), 14–25 (Jan 2004).https://doi.org/10. 1145/982962.964003

    work page arXiv 2004

  3. [3]

    Bílý, A., Hansen, J., Müller, P., Summers, A.J.: Compositional Reasoning for Side- effectful Iterators and Iterator Adapters (2022), https://arxiv.org/abs/2210. 09857

    work page 2022

  4. [4]

    Castanho, D., Pereira, M.: Auto-active Verification of Graph Algorithms, Written in OCaml (2022),https://arxiv.org/abs/2207.09854

    work page Pith review arXiv 2022

  5. [5]

    SIGPLAN Not

    Charguéraud, A.: Characteristic formulae for the verification of imperative programs. SIGPLAN Not. 46(9), 418–430 (sep 2011).https://doi.org/10.1145/2034574. 2034828

    work page doi:10.1145/2034574 2011

  6. [6]

    In: Formal Methods - The Next 30 Years - Third World Congress

    Charguéraud, A., Filliâtre, J., Lourenço, C., Pereira, M.: GOSPEL — Providing OCaml with a Formal Specification Language. In: Formal Methods - The Next 30 Years - Third World Congress. Lecture Notes in Computer Science, vol. 11800, pp. 484–501. Springer (2019),10.1007/978-3-030-30942-8_29

    work page doi:10.1007/978-3-030-30942-8_29 2019

  7. [7]

    https://ionchirica.github.io/ ifm2025 (2025), Companion artifact

    Chirica, I., Pereira, M.: Unfolding Iterators. https://ionchirica.github.io/ ifm2025 (2025), Companion artifact

    work page 2025

  8. [8]

    In: Morazán, M.T

    Conchon, S., Filliâtre, J., Signoles, J.: Designing a Generic Graph Library Using ML Functors. In: Morazán, M.T. (ed.) Proceedings of the Eighth Symposium on Trends in Functional Programming, TFP 2007, New York City, New York, USA. Trends in Functional Programming, vol. 8, pp. 124–140. Intellect (2007)

    work page 2007

Show all 22 references
  1. [9]

    In: Sankaranarayanan, S., Sharygina, N

    Denis, X., Jourdan, J.H.: Specifying and Verifying Higher-order Rust Iterators. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 13994, pp. 93–110. ETAPS, Springer,...

    doi

  2. [10]

    In: Riesco, A., Zhang, M

    Denis, X., Jourdan, J., Marché, C.: Creusot: A Foundry for the Deductive Ver- ification of Rust Programs. In: Riesco, A., Zhang, M. (eds.) Formal Methods and Software Engineering - 23rd International Conference on Formal Engineer- ing Methods, ICFEM 2022, Madrid, Spain, Octobe...

    2022 doi

  3. [11]

    Prentice Hall PTR, USA, 1st edn

    Dijkstra, E.W.: A Discipline of Programming. Prentice Hall PTR, USA, 1st edn. (1997)

    1997

  4. [12]

    International Journal on Soft- ware Tools for Technology Transfer (STTT)13(5), 397–403 (Aug 2011),10.1007/ s10009-011-0211-0

    Filliâtre, J.C.: Deductive Software Verification. International Journal on Soft- ware Tools for Technology Transfer (STTT)13(5), 397–403 (Aug 2011),10.1007/ s10009-011-0211-0

    2011

  5. [13]

    In: Proceedings of the 22nd European Conference on Programming Languages and Systems

    Filliâtre, J.C., Paskevich, A.: Why3: where programs meet provers. In: Proceedings of the 22nd European Conference on Programming Languages and Systems. p. 125–128. ESOP’13, Springer-Verlag, Berlin, Heidelberg (2013).https://doi.org/ 10.1007/978-3-642-37036-6_8

    2013 doi

  6. [14]

    In: ISoLA 2021 - 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation

    Filliâtre, J.C., Paskevich, A.: Abstraction and Genericity in Why3. In: ISoLA 2021 - 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation. vol. 12476. Rhodes, Greece (Oct 2021).https://doi. org/10.1007/978-3-030-61362-4_7 18 I. ...

    2021 doi

  7. [15]

    In: Rayadurgam, S., Tkachuk, O

    Filliâtre, J.C., Pereira, M.: A Modular Way to Reason About Iteration. In: Rayadurgam, S., Tkachuk, O. (eds.) NASA Formal Methods. pp. 322–336. Springer International Publishing, Cham (2016)

    2016

  8. [16]

    Hoare, C.A.R.: An Axiomatic Basis for Computer Programming. Commun. ACM 12(10), 576–580 (oct 1969).https://doi.org/10.1145/363235.363259

    1969

  9. [17]

    Journal of Functional Programming28(e20) (2018)

    Jung, R., Krebbers, R., Jourdan, J.H., Bizjak, A., Birkedal, L., Dreyer, D.: Iris From the Ground Up: A Modular Foundation For Higher-order Concurrent Separation Logic. Journal of Functional Programming28(e20) (2018). https://doi.org/10. 1017/S0956796818000151

    2018

  10. [18]

    Springer (2003),http://www.springer

    Monin, J.: Understanding Formal Methods. Springer (2003),http://www.springer. com/computer/swe/book/978-1-85233-247-1

    2003

  11. [19]

    104–125 (01 2017).https://doi.org/10.3233/ 978-1-61499-810-5-104

    Müller, P., Schwerhoff, M., Summers, A.: Viper: A verification infrastructure for permission-based reasoning, pp. 104–125 (01 2017).https://doi.org/10.3233/ 978-1-61499-810-5-104

    2017

  12. [20]

    In: Silva, A., Leino, K.R.M

    Pereira, M., Ravara, A.: Cameleer: A Deductive Verification Tool for OCaml. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II. Lecture Notes in Computer Science, vol....

    2021

  13. [21]

    In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs

    Pottier, F.: Verifying a hash table and its iterators in higher-order separation logic. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs. p. 3–16. CPP 2017, Association for Computing Machinery, New York, NY, USA (2017). https://doi.org/10.1145...

    2017

  14. [22]

    In: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science

    Reynolds, J.: Separation Logic: A Logic for Shared Mutable Data Structures. In: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science. pp. 55–74 (2002). https://doi.org/10.1109/LICS.2002.1029817

    2002 arXiv

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.