Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866911624677294080 |
|---|---|
| author | Li, Kwing Hei Aguirre, Alejandro Tassarotti, Joseph Birkedal, Lars |
| author_facet | Li, Kwing Hei Aguirre, Alejandro Tassarotti, Joseph Birkedal, Lars |
| contents | We present Foxtrot, the first higher-order separation logic for proving contextual refinement of higher-order concurrent probabilistic programs with higher-order local state. From a high level, Foxtrot inherits various concurrency reasoning principles from standard concurrent separation logic, e.g. invariants and ghost resources, and supports advanced probabilistic reasoning principles for reasoning about complex probability distributions induced by concurrent threads, e.g. tape presampling and induction by error amplification. The integration of these strong reasoning principles is highly non-trivial due to the combination of probability and concurrency in the language and the complexity of the Foxtrot model; the soundness of the logic relies on a version of the axiom of choice within the Iris logic, which is not used in earlier work on Iris-based logics. We demonstrate the expressiveness of Foxtrot on a wide range of examples, including the adversarial von Neumann coin and the $\mathsf{randombytes\_uniform}$ function of the Sodium cryptography software library.
All results have been mechanized in the Rocq proof assistant and the Iris separation logic framework. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_10135 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version) Li, Kwing Hei Aguirre, Alejandro Tassarotti, Joseph Birkedal, Lars Logic in Computer Science Programming Languages We present Foxtrot, the first higher-order separation logic for proving contextual refinement of higher-order concurrent probabilistic programs with higher-order local state. From a high level, Foxtrot inherits various concurrency reasoning principles from standard concurrent separation logic, e.g. invariants and ghost resources, and supports advanced probabilistic reasoning principles for reasoning about complex probability distributions induced by concurrent threads, e.g. tape presampling and induction by error amplification. The integration of these strong reasoning principles is highly non-trivial due to the combination of probability and concurrency in the language and the complexity of the Foxtrot model; the soundness of the logic relies on a version of the axiom of choice within the Iris logic, which is not used in earlier work on Iris-based logics. We demonstrate the expressiveness of Foxtrot on a wide range of examples, including the adversarial von Neumann coin and the $\mathsf{randombytes\_uniform}$ function of the Sodium cryptography software library. All results have been mechanized in the Rocq proof assistant and the Iris separation logic framework. |
| title | Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version) |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2511.10135 |