Elton: Urn Resources for Reasoning about Adversarial Probabilistic Programs

2026-07-15T05:40:08Z

Probabilistic programs are important for many applications. For security applications in particular, one is interested in establishing properties that hold in the presence of arbitrary adversaries, i.e., unknown pieces of code. We present Elton, a higher-order separation logic for reasoning about higher-order probabilistic programs utilizing unknown adversarial code. Elton incorporates novel logical facilities for specifying invariants over distributional properties using delayed samplings at the language level, and a new kind of separation-logic predicate called urn resources at the logic level. We show that these extensions are sound and can be erased back to a standard call-by-value semantics. Combined with other features, e.g. invariants and ghost resources, Elton is expressive enough to prove error bounds on a wide range of security examples, some of which are beyond the scope of previous techniques. All proofs are mechanized with the Rocq proof assistant and the Iris separation logic framework.

A cubical formalisation of conditional independence, Bayesian conditioning, and Pearl's d-separation soundness

2026-07-15T04:05:03Z

The standard convex-algebra interchange axiom, common to probability-monad formalisations since Stone, is provably too weak to support full Bayesian conditioning. We make this precise in Cubical Agda: finite distributions as a higher inductive type, conditional independence as a cubical path between kernels, recursive Bayesian conditioning as a total function on a full-support fragment. Lifting conditioning to the full HIT exposes a structural mismatch -- the two halves of the rearranged 4-leaf mix carry distinct Bayesian weights related by Bayes' formula, not the single shared inner weight the standard axiom provides. We exhibit the minimal generalisation that resolves this and prove the standard form is the degenerate case where the two inner weights coincide. Around this observation we verify the algebraic context constructively, with zero postulates above an abstract ordered-field interface: bind commutativity, the four semi-graphoid axioms, intersection (reduced to contraction via structural $Σ$-witnesses, without positivity), Pearl's do-calculus Rules~1, 2, and~3 in kernel form, finite-type Bayesian conditioning, and the soundness of Pearl's d-separation theorem on arbitrary finite directed acyclic graphs (DAGs) -- in interventional form for multi-element $X$, $Y$, $Z$, and in Bayesian form for the elementary patterns. The probability monad is also verified as a Markov category; the abstract interface discharges at $\mathbb{Q}$.

Thermodynamic Limits of Proof

2026-07-14T22:01:07Z

Every irreversible recorded distinction has a positive thermodynamic work floor. Landauer's principle supplies the ideal bound $\varepsilon\ge k_B T\ln 2$ per irreversible bit, experimentally verified to $\pm 10\%$. Proof available to an agent is checkable information for that agent: some substrate must produce, retain, and expose evidence that excludes answer-changing alternatives. A finite detector array operating at temperature $T$ for finite time has finite signal-acquisition capacity. Combining finite causal access, positive retained-record cost, and exact lower bounds on required records gives the Physical Counting Impossibility Theorem: no fixed-budget substrate can provide universal exact proof once the retained-record lower bound exceeds the declared budget. The theorem requires exactly $B<\infty$ and $\varepsilon>0$. An answer reports a value; proof supplies checkable grounds for accepting it. A reversible device may compute an answer and erase its scratch history, but proof requires retained, inspectable records. A global answer register, oracle response, entanglement witness, finite survey catalog, or trusted device output supplies proof only through an interface that exposes the relevant grounds to the verifier. A proposed interface must identify the retained-record lower-bound family $R(n)$ it induces. Sound operational claims about efficient solvability inherit the same finite-budget obstruction when their acceptance would license universal exact proof. Substrate-free derivability has proof status only when a physical verification event makes it available to an agent.

Constraint Satisfaction Problems over Finitely Bounded Homogeneous Structures: a Dichotomy between FO and L-hard

2026-07-14T19:26:27Z

Feder-Vardi conjecture, which proposed that every finite-domain Constraint Satisfaction Problem (CSP) is either in P or it is NP-complete, has been solved independently by Bulatov and Zhuk almost ten years ago. Bodirsky-Pinsker conjecture which states a similar dichotomy for countably infinite first-order reducts of finitely bounded homogeneous structures is wide open. In this paper, we prove that CSPs over first-order expansions of finitely bounded homogeneous model-complete cores are either first-order definable (and hence in non-uniform AC$^0$) or L-hard under first-order reduction. It is arguably the most general complexity dichotomy when it comes to the scope of structures within Bodirsky-Pinsker conjecture. Our strategy is that we first give a new proof of Larose-Tesson theorem, which provides a similar dichotomy over finite structures, and then generalize that new proof to infinite structures.

Graph-Series Semantics and Abel Regularization for Recursive Hybrid Quantum Programs

2026-07-14T15:14:38Z

We introduce a graded graph-series semantics for recursive hybrid quantum programs interpreted in the quantum orchestra monad. Finite terminating executions are represented by directed paths whose edges carry normal completely positive subunital maps and whose terminal vertices carry classical results. Path concatenation defines a graded execution category, while continuation grafting models outcome-dependent sequential composition. We construct a semantic evaluation from admissible execution-graph series to quantum orchestras and prove that it is compatible with both channel composition and Kleisli composition. For finitary recursive programs, the truncation of the execution series at degree $n$ is shown to coincide with the $n$-th Kleene approximant of the associated Scott-continuous recursion functional. Consequently, evaluation of the complete graph series recovers the ordinary least-fixed-point denotation. Weighting a graph of degree $n$ by $q^n$, with $0

Double negation stable h-propositions in cubical sets

2026-07-14T15:06:15Z

We give a construction of classifiers for double negation stable h-propositions in a variety of cubical set models of homotopy type theory and cubical type theory. This is used to give some relative consistency results: classifiers for double negation stable propositions exist in cubical sets whenever they exist in the metatheory; the Dedekind real numbers can be added to homotopy type theory without changing the consistency strength; we construct a model of homotopy type theory with extended Church's thesis, which states that all partial functions with double negation stable domain are computable.

A Strategy Language for Controlled Proof Search

2026-07-14T11:38:30Z

This paper introduces the strategy language of Pgeon, a meta-prover with a clear separation between inference rules and proof search. We give the semantics of strategies as functions over proof states, and of the operators that are used to combine them, allowing for sequential composition, choice, repetition and interleaving of strategies. This language is designed to handle the challenge of fair proof search in semi-decidable logics, where simple depth-first exploration of the proof space is not guaranteed to achieve completeness. We showcase the expressiveness and effectiveness of the approach through case studies in first-order and modal logics.

Work-in-Progress: A Tactic for Pattern Matching in Autosubst

2026-07-14T11:38:14Z

Autosubst enables automatic equality-checking up to the sigma-calculus for assumption-free equalities, allowing users to avoid cumbersome reasoning about de Bruijn indices. While effective in many cases, this approach is inapplicable when matching against typing rules, reduction relations, or lemmas, requiring users to either phrase typing rules in a way that they work with Autosubst or even stating explicitly an alternative de Bruijn term. But even without beta-reduction, solutions of matching may not be unique. This paper presents a work-in-progress method for automatically pattern matching against assumptions, evaluated on standard case studies including the POPLMark and POPLMark Reloaded challenges.

Anti-Unification Completeness Analysis in PVS

2026-07-14T11:37:57Z

In syntactic anti-unification, one is concerned with finding the commonalities between terms, while (uniformly) abstracting their differences. The original goal of anti-unification development in the seventies was to automate inductive reasoning. Recent applications of anti-unification techniques include efficiently transforming sequential code into parallel code, detecting code clones, and preventing software failures. Previous work addressed the elements required to verify, in the Prototype Verification System (PVS), termination and soundness of a functional algorithm based on inference rules for syntactic anti-unification. This paper dissects all aspects required to formally establish the completeness of the rule-based algorithm, highlighting the significant differences in the formalizations of anti-unification and unification.

Proof Theory and Dependent Type Theory: Distinct Foundations for Designing Proof Assistants

2026-07-14T11:37:41Z

This paper examines the foundational distinctions between proof theory and dependent type theory (DTT) in the design of interactive theorem provers. While several implemented systems are designed using the dependently typed λ-calculus to represent proofs, no major proof assistant is designed using modern structural proof theory, even though, as I will argue here, the sequent calculus offers a compelling alternative framework. Six specific topics are proposed where the proof-theoretic perspective is arguably superior to the DTT perspective. These topics include the separation of logic from proof structure, the strategic use of non-determinism in proof reconstruction, and the avoidance of complex typing-discipline issues such as universe levels and proof irrelevance. The final topic -- the treatment of bindings -- is further developed to demonstrate how a natural, intensional approach is achieved through the mobility of binders. This methodology is illustrated via the Abella theorem prover, which leverages lambda-tree syntax and the nabla-quantifier to provide an elegant environment for reasoning about the meta-theory of languages and logics involving complex binding.

Barbed Similarity for the $π$-Calculus in Beluga: A Case Study in Coinductive Reasoning

2026-07-14T11:37:25Z

We formalize strong barbed similarity for the pi-calculus in the Beluga proof assistant, completing a line of work addressing the Concurrent Calculi Formalization Benchmark. By extending previous developments to include replication, we give a coinductive encoding of behavioral equivalence based on barbs and internal actions. Using Beluga's copattern-based coinduction, we obtain concise and compositional proofs, including compatibility properties and a context lemma characterizing barbed precongruence. The case study demonstrates the effectiveness of combining HOAS and coinductive reasoning for mechanizing concurrent calculi.

Building Extensible Program Logics through Effect Handlers

2026-07-14T11:21:43Z

One strategy for reasoning about programs that have certain kinds of effects is to use program logics that provide specialized rules for reasoning about these effects. However, developing program logics requires skills that are distinct from those needed for using program logics, making the development of new logics challenging and less accessible. Moreover, when developing new logics, it can be difficult to reuse components from prior logics or combine support for different effects. In this paper, we propose an approach for operationally building extensible program logics based on effect handlers. Our starting point is an expressive program logic for reasoning about programs written in a pure, sequential language with support for effect handlers. Within this language, we implement handlers that model concurrency, distributed execution, and crash-recovery behavior. Then, by proving properties about these handlers, we extend the program logic and derive expressive rules for reasoning about these effects. In some cases, this approach leads to stronger reasoning rules than those found in prior program logics targeting these features. In addition, we develop a relational logic for proving contextual refinements between programs using effects. As with unary reasoning, handlers enable this relational logic to be developed in an extensible way.

Quantum Weakest Preconditions Revisited: Pre-expectations for Expected Runtime Analysis

2026-07-14T09:06:02Z

Quantum weakest preconditions are a fundamental tool for program verification of quantum programs. Many variations have been reported in the literature. We revisit quantum weakest preconditions from the perspective of expected runtime analysis of quantum programs and introduce a novel pre-expectation framework that enables to reason about the preconditions of quantum programs without the need of an upper bound. This is particularly interesting for quantum programs involving reward statements. The overall goal is to analyze runtime behavior even in the case of programs with potentially infinite expected runtime. This paper presents several ways to do so, e.g., a program transformation such that the expected runtime of a quantum program can be expressed using the weakest pre-expectation calculus with rewards.

A Unified Framework for Reaction Systems Based on Interval Structures

2026-07-14T05:46:22Z

Reaction systems have evolved into a rich family of computational models differing in their treatment of multiplicities, resource management, concurrency, and state evolution. We introduce a unified semantic framework based on interval structures and interval-based transformation systems. The framework decomposes operational semantics into independent resource, production, update, and execution strategies, providing a common basis for describing, comparing, and constructing reaction-system variants. We show that classical reaction systems, restricted reaction systems, multiset reaction systems, reaction systems with concentration, and resource-preserving multiset reaction systems are all recovered as instantiations of the framework. Quantitative reaction systems are accommodated through an additional preprocessing stage. We further demonstrate that the framework naturally extends beyond reaction systems to other computational models, including Petri nets. The proposed framework provides a common semantic foundation for existing models and a flexible basis for developing and analysing new computational formalisms.

Foundational Constraint Solving for Expressive Refinement Typing

2026-07-14T00:15:23Z

SMT-based program verifiers are hamstrung by two problems: expressiveness, because predictable verification restricts to the boundaries of SMT decidability, and trust, because the solver is a large, unverified artifact whose soundness bugs may quietly compromise every tool built on it. We present FLEX, a foundational Constrained Horn Clause (CHC) solver implemented in LEAN, that reduces the trusted base to the kernel alone, and allows using LEAN's entire proof ecosystem to verify low-level systems code, via three contributions. First, FLEX encodes CHCs as plain LEAN propositions where the Horn variables are existentially bound predicates, and shows how to implement CHC solvers as tactics (meta-programs) that compute kernel checkable proofs of the CHC propositions. Second, we show how to implement two verified CHC generators in LEAN: a Floyd-Hoare style generator for an imperative language, and a refinement-type-based generator for a functional calculus, which can be composed with the solving tactics to yield the first end-to-end foundational CHC-based verifiers. Finally, we show how FLEX allows us to leapfrog the expressiveness limitations of SMT by unleashing LEAN's entire ecosystem of proof machinery to prove arbitrary functional correctness properties of various low-level Rust libraries using the FLUX refinement type checker, and demonstrate the viability of FLEX as a trustworthy CHC backend, by showing it automatically discharges 95.7% of the CHCs from FLUX's benchmark suite.