pith. machine review for the scientific record. sign in

arxiv: 2605.13526 · v1 · submitted 2026-05-13 · 💻 cs.LO

Recognition: unknown

Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic

Markus de Medeiros , Puming Liu , Kwing Hei Li , Alejandro Aguirre , Lars Birkedal , Joseph Tassarotti
Authors on Pith no claims yet

Pith reviewed 2026-05-14 18:24 UTC · model grok-4.3

classification 💻 cs.LO
keywords separation logicexact samplingcomputable realscontinuous distributionsprogram verificationprobabilistic programshigher-order logic
0
0 comments X

The pith

A higher-order separation logic proves exact samplers for continuous distributions correct.

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

The paper introduces Continuous-Eris, a higher-order separation logic for establishing that programs correctly implement exact sampling from computable continuous distributions. These programs combine probabilistic choice, higher-order functions, and mutable state to lazily generate real samples digit by digit, avoiding floating-point approximations. The authors apply the logic to verify samplers for the uniform, Gaussian, and Laplace distributions plus a supporting library for exact real arithmetic. All proofs are machine-checked in the Rocq proof assistant. This provides formal guarantees for sampling methods used in settings where approximation errors matter.

Core claim

Continuous-Eris is a higher-order separation logic that allows verification of the correctness of exact sampling algorithms for computable distributions. The logic is used to establish that verified samplers for the uniform, Gaussian, and Laplace distributions generate samples according to their target distributions, along with a verified library for exact real arithmetic operations on those samples, all formalized in Rocq.

What carries the argument

Continuous-Eris, a higher-order separation logic whose rules reason about probabilistic choice, higher-order functions, and mutable state over a model of computable reals.

If this is right

  • The verified uniform, Gaussian, and Laplace samplers are correct by construction.
  • The exact real arithmetic library correctly supports operations on lazily generated samples.
  • The same logic can be applied to other computable continuous distributions.
  • Machine-checked proofs eliminate hidden approximation errors in the sampling code.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The verified samplers could be composed into larger differential privacy mechanisms while preserving formal guarantees against approximation-based attacks.
  • The approach may extend to verifying exact sampling in other probabilistic programming languages that support lazy real generation.
  • Developers could use the verified library as a trusted building block when implementing new exact samplers.

Load-bearing premise

The separation logic rules faithfully reflect the underlying language semantics for probabilistic choice, higher-order functions, and mutable state, and the computable reals model correctly captures lazy digit generation.

What would settle it

Execution of one of the Rocq-verified samplers producing a sequence of samples whose empirical distribution deviates from the claimed target distribution, or discovery of an inconsistency in the formalization of the separation logic rules.

Figures

Figures reproduced from arXiv: 2605.13526 by Alejandro Aguirre, Joseph Tassarotti, Kwing Hei Li, Lars Birkedal, Markus de Medeiros, Puming Liu.

Figure 2
Figure 2. Figure 2: The maximum of two uniform [0, 1] samples. 2 Key Ideas To illustrate the key concepts of Continuous-Eris, we will verify the MaxU2 program in [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 10
Figure 10. Figure 10: The Negative Exponential sampler (E). L ε µ ≜ let (z, u) := E 0 in let sgn := rand 1 in Radd µ (Rscal ε (RofBZU (sgn, z, u))) [PITH_FULL_IMAGE:figures/full_fig_p021_10.png] view at source ↗
read the original abstract

Most implementations of sampling algorithms for continuous distributions use floating-point numbers, which introduce round-off errors and approximations. These errors can be difficult to analyze, and can cause security issues when used in algorithms for differential privacy. An alternative is to use exact sampling algorithms based on computable reals, which can lazily generate the digits of a continuous sample to arbitrary precision. However, these algorithms are intricate, and implementing and using them involves a combination of semantically challenging language features, such as probabilistic choice, higher-order functions, and dynamically-allocated mutable state. In this paper we present Continuous-Eris, a higher-order separation logic for verifying the correctness of exact sampling algorithms for computable distributions. To demonstrate Continuous-Eris, we verify the correctness of computable samplers for the uniform, Gaussian, and Laplace distributions, as well as a library for exact real arithmetic for working with generated samples. All of the results in this paper have been verified in the Rocq proof assistant.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper introduces Continuous-Eris, a higher-order separation logic for verifying exact sampling algorithms for computable continuous distributions. It demonstrates the logic by mechanically verifying in Rocq the correctness of samplers for the uniform, Gaussian, and Laplace distributions together with a supporting library for exact real arithmetic based on lazy digit generation.

Significance. If the result holds, the work supplies a sound, machine-checked foundation for reasoning about probabilistic programs that combine continuous sampling, higher-order functions, and mutable state. The Rocq-verified examples eliminate approximation gaps that arise in floating-point implementations and directly support applications such as differential privacy that require exact distributions.

minor comments (2)
  1. The abstract and introduction would benefit from a brief sentence clarifying how the lazy-digit model of computable reals interacts with the probabilistic choice rules in Continuous-Eris.
  2. Notation for the higher-order separation logic connectives (e.g., the precise form of the probabilistic choice rule) could be summarized in a small table for readers who are not already familiar with the Eris family of logics.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive review, accurate summary of the contributions, and recommendation to accept the paper. We are pleased that the significance of Continuous-Eris as a verified foundation for exact sampling of continuous distributions is recognized.

Circularity Check

0 steps flagged

No significant circularity; formal verification is self-contained

full rationale

The paper defines Continuous-Eris as a higher-order separation logic and mechanically verifies its soundness plus the correctness of uniform/Gaussian/Laplace samplers and an exact-real library inside the Rocq proof assistant. All load-bearing steps are established by direct proof rules and semantic models (lazy-digit computable reals) rather than by fitting parameters, renaming prior results, or reducing claims to self-citations. The Rocq development supplies an independent, machine-checked foundation with no unverified semantic gaps or self-referential definitions.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central claim rests on standard mathematical foundations for separation logic and computable reals; the main contribution is the new logic definition and its application, with no free parameters or ad-hoc fitted quantities.

axioms (1)
  • standard math Standard axioms of higher-order separation logic and the theory of computable real numbers
    The logic is built on established mathematical foundations for reals and separation logic as background.
invented entities (1)
  • Continuous-Eris logic no independent evidence
    purpose: To specify and verify exact sampling programs for continuous distributions
    Newly defined logic whose rules are introduced in the paper and checked in Rocq.

pith-pipeline@v0.9.0 · 5481 in / 1287 out tokens · 47898 ms · 2026-05-14T18:24:00.056657+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

16 extracted references · 16 canonical work pages

  1. [1]

    Ackerman, Cameron E

    1 Nathanael L. Ackerman, Cameron E. Freer, and Daniel M. Roy. On the computability of conditional probability.J. ACM, 66(3):23:1–23:40, 2019.doi:10.1145/3321699. 2 Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Odder- shede Gregersen, Joseph Tassarotti, and Lars Birkedal. Error credits: Resourceful reasoning about error...

    work page doi:10.1145/3321699 2019

  2. [2]

    5 Kevin Batz, Joost-Pieter Katoen, Francesca Randone, and Tobias Winkler

    doi:10.4230/LIPIcs.ICALP.2016.107. 5 Kevin Batz, Joost-Pieter Katoen, Francesca Randone, and Tobias Winkler. Foundations for deductive verification of continuous probabilistic programs: From lebesgue to riemann and back.Proc. ACM Program. Lang., 9(OOPSLA1):421–448, 2025.doi:10.1145/3720429. 6 Andrej Bauer and Iztok Kavkler. Implementing real numbers with ...

    work page doi:10.4230/lipics.icalp.2016.107 2016

  3. [3]

    8Patrick Billingsley.Probability and Measure

    doi:10.1145/3519939.3523721. 8Patrick Billingsley.Probability and Measure. Wiley, 3rd edition,

    work page doi:10.1145/3519939.3523721

  4. [4]

    A domain-theoretic approach to brownian motion and general continuous stochastic processes

    9 Paul Bilokon and Abbas Edalat. A domain-theoretic approach to brownian motion and general continuous stochastic processes. In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ...

    work page 2014

  5. [5]

    10 Hans-Juergen Boehm

    doi:10.1145/2603088.2603102. 10 Hans-Juergen Boehm. Towards an API for the real numbers. In Alastair F. Donaldson and Emina Torlak, editors,Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020, pages 562–576. ACM, 2020.doi:10.1145/3385412.3386037. 11 Sylvie ...

    work page doi:10.1145/2603088.2603102 2020

  6. [6]

    12 Johannes Borgström, Ugo Dal Lago, Andrew D

    doi:10.1007/ S11786-014-0181-1. 12 Johannes Borgström, Ugo Dal Lago, Andrew D. Gordon, and Marcin Szymczak. A lambda- calculus foundation for universal probabilistic programming. In Jacques Garrigue, Gabriele Keller, and Eijiro Sumii, editors,Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, Se...

    work page doi:10.1145/2951913.2951942 2016

  7. [7]

    Verifying exact samplers for continuous distributions with a discrete program logic

    doi:10.1145/3571239. 15 Markus de Medeiros, Puming Liu, Kwing Hei Li, Alejandro Aguirre, Lars Birkedal, and Joseph Tassarotti. Artifact for "Verifying exact samplers for continuous distributions with a discrete program logic", May 2026.doi:10.5281/zenodo.20114733. 16 Markus de Medeiros, Muhammad Naveed, Tancrède Lepoint, Temesghen Kahsai, Tristan Ravitch,...

    work page doi:10.1145/3571239 2026

  8. [8]

    26 Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G

    Springer Berlin Heidelberg. 26 Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, and Lars Birkedal. Asynchronous probabilistic couplings in higher-order separation logic.Proc. ACM Program. Lang., 8(POPL):753–784, 2024.doi:10.1145/3632868. 27 Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede G...

    work page doi:10.1145/3632868 2024

  9. [9]

    33 Daniel Huang and Greg Morrisett

    URL: https://www.sciencedirect.com/science/article/pii/S0890540109000170, doi:10.1016/j.ic.2008.12.009. 33 Daniel Huang and Greg Morrisett. An application of computable distributions to the semantics of probabilistic programming languages. In Peter Thiemann, editor,Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held...

    work page doi:10.1016/j.ic.2008.12.009 2008

  10. [10]

    10175691

    35 Mathieu Huot, Alexander K. Lew, Vikash K. Mansinghka, and Sam Staton.ωpap spaces: Rea- soning denotationally about higher-order, recursive probabilistic and differentiable programs. In 38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023, Boston, MA, USA, June 26-29, 2023, pages 1–14. IEEE, 2023.doi:10.1109/LICS56636.2023.10175739. 36...

    work page doi:10.1109/lics56636.2023.10175739 2023

  11. [11]

    42 Valérie Ménissier-Morain

    Association for Computing Machinery.doi:10.1145/3779031.3779109. 42 Valérie Ménissier-Morain. Arbitrary precision real arithmetic: design and algorithms. Research Report lip6.2003.003, LIP6, May

    work page doi:10.1145/3779031.3779109 2003

  12. [12]

    URL:https://hal

    Springer. URL:https://hal. science/hal-02183311,doi:10.1007/978-3-030-17184-1\_1. 44 Ilya Mironov. On significance of the least significant bits for differential privacy. InProceedings of the 2012 ACM conference on Computer and communications security, pages 650–661,

    work page doi:10.1007/978-3-030-17184-1 2012

  13. [13]

    TheiRRAM:ExactarithmeticinC++

    45 NorbertTh.Müller. TheiRRAM:ExactarithmeticinC++. InJensBlanck, VascoBrattka, and Peter Hertling, editors,Computability and Complexity in Analysis, 4th International Workshop, CCA 2000, Swansea, UK, September 17-19, 2000, Selected Papers, volume 2064 ofLecture Notes in Computer Science, pages 222–252. Springer, 2000.doi:10.1007/3-540-45335-0\_14. 46 Pet...

    work page doi:10.1007/3-540-45335-0 2000

  14. [14]

    48 Tetsuya Sato

    doi:10.1109/LICS.1997.614952. 48 Tetsuya Sato. Approximate relational hoare logic for continuous random samplings. In Lars Birkedal, editor,The Thirty-second Conference on the Mathematical Foundations of Programming Semantics, MFPS 2016, Carnegie Mellon University, Pittsburgh, PA, USA, May 23-26, 2016, volume 325 ofElectronic Notes in Theoretical Computer...

    work page doi:10.1109/lics.1997.614952 1997

  15. [15]

    Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, bayesian inference, and optimization.Proc

    49 Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Justin Hsu. Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, bayesian inference, and optimization.Proc. ACM Program. Lang., 3(POPL):38:1– 38:30, 2019.doi:10.1145/3290351. 50 Alex K. Simpson. Lazy functional algorithms ...

    work page doi:10.1145/3290351 2019

  16. [16]

    Exact real computer arithmetic with continued fractions.IEEE Trans

    53 Jean Vuillemin. Exact real computer arithmetic with continued fractions.IEEE Trans. Computers, 39(8):1087–1105, 1990.doi:10.1109/12.57047. 54 Mitchell Wand, Ryan Culpepper, Theophilos Giannakopoulos, and Andrew Cobb. Contextual equivalence for a probabilistic language with continuous random variables and recursion.Proc. ACM Program. Lang., 2(ICFP):87:1...

    work page doi:10.1109/12.57047 1990