Performance Portability Explained: Insights from accelerating ICON microphysics

2026-11-10T15:24:22Z

Scientific computing is under increasing pressure to adapt to HPC hardware that is shaped by AI workloads. In these modern ecosystems, extracting reasonable performance without investing major engineering effort is a central issue for domain scientists. Correctness constraints and intricate reference implementations represent further impediments to development. Instead of using a double-precision implementation as a reference, considering the underlying scientific problem directly opens more opportunities for performance improvements when updating and rewriting applications. We take seven different portability frameworks---covering pragma-based, DSL, and data-centric approaches---and evaluate them on a microphysics kernel of the ICON climate model. Our performance benchmarks show that each different HPC system benefits from a different combination of optimizations, so we develop the measure of framework expressivity to gauge how easily each framework can customize portable implementations in this way.

CFGKAT: A Complete Calculus for Non-Local Control Flow

2026-11-10T15:22:03Z

CFGKAT is an extension of guarded Kleene Algebra with Tests (GKAT) that adds non-local control flow (e.g., break, goto) while maintaining an efficient decision procedure. An axiomatization of equivalence for CFGKAT presents unique barriers created by the presence of non-local control flow and contextual semantics of goto which compromises compositional reasoning. In this paper, we overcome these barriers and present a sound and complete axiomatization of program equivalence in CFGKAT. We verify the loop case of the Erosa-Hendren goto elimination algorithm, a difficult syntactic metatheorem which requires reasoning about fixpoints, control-flow contexts, and mutable state. We mechanize the metatheory and case study in Rocq.

Secure Information Flow in Quantum Programs

2026-11-10T14:34:39Z

Information-flow security aims to prevent the leakage of confidential information through program execution. This problem becomes fundamentally subtler for quantum programs, because their states may involve superposition and entanglement, and their executions may involve intricate interactions between classical and quantum variables. This paper develops semantic foundations and verification methods for secure information flow in quantum programs. We formulate two notions of information-flow security. The first is a noninterference-based definition that naturally generalizes its classical counterpart. The second is a simulation-based definition that explicitly models an attacker, providing a clear operational interpretation of security. We prove that these two notions are equivalent. To verify the information-flow security of quantum programs, we develop a proof framework based on quantum Hoare logic. A key challenge is that the standard self-composition technique, which expresses information-flow security in Hoare logic by composing a program with a renamed copy of itself, fails in the quantum setting due to an obstruction analogous to the no-cloning theorem. To overcome this challenge, we introduce self-conjugation, a novel technique that leverages the deferred measurement principle and properties of unitary operations. We demonstrate our framework on examples drawn from the quantum one-time pad, quantum error correction, and anonymous entanglement generation.

RECURSUM: Automated Code Generation for Recurrence Relations Exceeds Expert Optimization via LayeredCodegen

2026-11-10T13:28:53Z

Automated code generation can systematically exceed expert hand-optimization for recurrence relations--computational primitives ubiquitous in orthogonal polynomials, special functions, numerical integration, and molecular integral evaluation. We present RECURSUM, a Python DSL generating optimized C++ for arbitrary recurrence relations via three backends--template metaprogramming, a novel LayeredCodegen backend, and runtime loop-based evaluation--specifying recurrences in 10--30 lines of Python that generate 650+ lines of production C++. LayeredCodegen achieves 9.8$\times$ speedup over expert hand-written code and 1.9$\times$ over template metaprogramming for McMurchie-Davidson Hermite coefficients, through zero-copy output parameters, guaranteed inlining, and exact-sized stack buffers. A DAG-topological generalization of this architecture--built to express the four-center electron-repulsion integral that LayeredCodegen's tower model cannot--beats libint2, a mature, two-decade-refined production library, on 12 of 14 Cartesian integral classes, with $\sim$2$\times$ faster contracted Coulomb/exchange (J/K) matrix construction (alkanes and 3-D DNA fragments alike) and 1.1--2.7$\times$ faster one-electron integrals, completing the full Hartree-Fock integral set from one DAG framework. We validate 24 recurrence types spanning pure mathematics, numerical analysis, and quantum chemistry; production benchmarks confirm these speedups propagate to complete algorithms, matching expert baselines within 3.3\%. By eliminating the dual expertise barrier of domain knowledge and C++ metaprogramming, RECURSUM establishes systematic code generation--not hand-tuning--as the performance ceiling for recurrence algorithms.

For Generalised Algebraic Theories, Two Sorts Are Enough

2026-11-10T10:06:05Z

Generalised algebraic theories (GATs) allow multiple sorts indexed over each other. Categories have two sorts, objects and morphisms, and the latter are double-indexed over the former. Martin-Löf type theory has four sorts: contexts, substitutions, types and terms. For example, types are indexed over contexts, and terms are indexed over both contexts and types. In this paper we show that any GAT can be reduced to a GAT involving only two sorts: a first one without dependencies, and another one indexed over the former. We show that a model of the reduced GAT is equivalently given by a pair consisting of a model of the original GAT, which we call the core model, and a "cartesian" morphism from the family of sets induced by this core model. In a type-theoretic metatheory, the initial model of a GAT is called a quotient inductive-inductive type (QIIT). The above characterisation justifies soundness of the reduction, in the sense that the QIIT of the original GAT can be simulated from the QIIT of the reduced GAT, by taking its core model. A particular case of our reduction is the well-known method of reducing mutual inductive types to a single indexed family. Other instances of this reduction can be found in the literature to simulate sophisticated QIITs in Cubical Agda. Indeed, the reduced GAT is simpler than the original GAT in the following aspects: it does not have sort equalities; it does not have interleaved sorts and operations; if the original GAT did not have interleaved sorts and operations, then the reduced GAT won't have operations interleaved between different sorts. Our approach is semantic in that it does not rely on a syntactic description of GATs, but instead, on Uemura's bi-initial characterisation of the category of (finite) GATs in the 2-category of finitely complete categories with a chosen exponentiable morphism.

Retargetable Compilation for Tensor Kernels via a Unified Layout Abstraction

2026-11-10T08:42:17Z

Modern hardware accelerators achieve high performance through specialized instructions coupled with tightly managed memory hierarchies. These instructions impose strict layout requirements on their operands: where tensor fragments reside, how they are organized, and how parallel units access them. Such instruction-visible layout is critical to kernel performance, as it determines whether instructions execute correctly and how much data movement they incur. However, existing compilers either scatter layout requirements across handwritten programs and local scheduling rules, or provide layout representations and conversions specific to a single class of targets. Both approaches expose the same abstraction gap: the absence of a unified model for instruction layout requirements across backends. This paper presents Arknife, a retargetable compiler that treats instruction-visible layout as first-class instruction semantics. Its central idea is a constraint-based layout algebra: tensor layouts map logical axes to hardware axes spanning parallel levels and memory spaces. Instruction operands declare layout requirements, and target-provided repairs resolve conflicts. Layouts are then solved globally across the program. ISA-specific layout facts are supplied by target-side instruction descriptions rather than hardcoded in the compiler. Retargeting reuses the layout algebra and solver while defining the new target's instructions and their operand requirements. We evaluate Arknife across x86 CPU, Hexagon NPU, and NVIDIA A100 GPU. Arknife matches cuBLAS on A100, and on x86 and Hexagon outperforms vendor-optimized libraries by $2.17\times$ and $3.78\times$ and the retargetable compiler MISAAL by $5.08\times$ and $4.53\times$, respectively.

Gödel's Incompleteness Theorems in Grounded Arithmetic

2026-11-10T07:43:34Z

Reflective Grounded Arithmetic (RGA) is a paracomplete arithmetic in which every term is a program and truth is grounded evaluation. RGA discharges a hypothesis only when it proves the hypothesis decided. This paper shows, in a machine-checked Isabelle/HOL development, how Gödel's incompleteness theorems hold for RGA and for systems built on it. RGA's implication is material and RGA has the disjunction property, so the implications the textbook proof of the second theorem uses fail while its entailments and rules hold: Gödel's proof survives as entailments. RGA does not prove its consistency sentence Con, and RGA derives its own second theorem as the entailment $\mathit{Con}\vdash\neg\mathit{Pr}(\ulcorner\mathit{Con}\urcorner)$ and as one sentence quantified over proofs. The second theorem is then proved once, for every Gödel extension of RGA: an entailment relation on RGA's language, closed under RGA's rules, with a checker that meets three structural conditions, NEC, D3 and EXPL as proof transformers, D1 as closed acceptance, and consistency. D2 is not among the conditions. RGA with its checker is one instance. Inductive Grounded Arithmetic (IGA), RGA with ground induction, is another, its checker adding one rule detector, and IGA does not derive its consistency sentence for it. Adoption, a reflection rule whose premise is a derived warrant that the checker accepts computed proofs of every instance of a universal, gives consistent extensions RGA$^+$ and IGA$^+$. RGA$^+$ derives RGA's consistency sentence and IGA$^+$ derives RGA's and IGA's, so each strictly extends its base, and IGA$^+$ both. The second theorem holds at every adopted notation claim, and adopting Turing's code for that claim's checker derives its consistency sentence, so no claim certifies itself. Whether IGA alone derives RGA's consistency sentence is open, and the paper names what two routes to an answer need.

Curriculum proof repair with learned counterexamples

2026-11-10T06:14:20Z

Language models (LMs) have substantially lowered the barrier to applying formal verification for building reliable and secure software. Existing approaches commonly follow the verifier-in-the-loop paradigm, but the verifier often provides only coarse, binary pass/fail feedback, which offers little actionable signal on how the proof should be repaired. Recent work shows that counterexamples provide more actionable feedback by grounding proof failures in concrete program states, but generating useful ones at inference time requires costly iterative refinement. We present TopoVerus, an LM-based framework for Verus proof repair that internalizes counterexample-guided diagnosis as a model capability, producing useful counterexamples in a single pass. Our key insight is to train counterexample generation not as a standalone validation task, but as a data-driven diagnostic objective: a counterexample is useful when conditioning on it helps the model produce a safe, verifier-passing proof. Given a failed Verus proof and verifier error, TopoVerus generates a structured source-level counterexample, repair rationale, and repaired proof in one trajectory, optimized with reinforcement learning from Verus feedback and a proof-code safety gate. To guide the order of invariant repairs, TopoVerus introduces a curriculum with a topological graph reward based on invariant dependencies derived from inductiveness tests, which encourages counterexample generation to follow the same topological order. Across seven Verus benchmarks with 471 problems, TopoVerus achieves 61.6%/72.2% weighted-average Safe-Pass@1/Safe-Pass@3, outperforming the strongest baseline, Claude Sonnet 4.5, by 5.7/6.3 points. We also show that TopoVerus's learned counterexamples can directly augment the reasoning of existing LM-based proof repair approaches, improving their success rate by 64.3% compared to chain-of-thought diagnostics.

Context Types: Bunched Modalities for Unifying Safety and Reachability

2026-11-10T02:31:13Z

Most type systems are designed to verify safety properties: the judgement $e : τ$ holds if $e$ may evaluate to any value contained in the denotation of $τ$, but nothing more. More recent type systems have considered the complementary class of reachability properties: in these systems, the typing judgment holds if $e$ must be able to evaluate to every value denoted by $τ$, and possibly more. This paper introduces a refinement type system for higher-order functional programs where types can capture both safety and reachability properties. Simultaneously supporting both is challenging because each imposes different constraints on how variable bindings in a typing context are interpreted. We address this challenge by treating typing contexts as a kind of resource that mediates which capabilities are available when typing a program. We formalize this notion by developing a resource algebra of contextual capabilities and a bunched modal context logic over this algebra. We then interpret our type system in this logic, establishing soundness with respect to a denotational semantics that unifies safety and reachability guarantees within a single typing judgement.

Fibered Separation Logic: Weakest Preconditions, Universal Constructions, and Local Independence

2026-11-10T01:23:23Z

This paper introduces a categorical framework for models of higher-order separation logic including the weakest precondition modality. Weakest preconditions are interpreted by strong monads on a category fibered over a model of Moggi's computational lambda calculus. The fibered categories in question are termed bunched fibrations and shown to be equivalent to BI hyperdoctrines. Well-known heuristic techniques for obtaining weakest preconditions are shown to be expressible in categorical terms and are proved sound. The ``baking in the frame rule'' trick is shown to satisfy a universal property. Constructions are given for extending a program logic with cost credits. Our largest case study is parametrized by a category having local independent product (LIP) structure, a notion due to Simpson that axiomatizes name generation, randomness, and local state. From an LIP category, we construct an allocation monad, a bunched fibration, and a monad lifting. We instantiate our construction to obtain a novel probabilistic separation logic for measure-theoretic probability that both simplifies and clarifies prior work.

Discovering formally verified quantum programs with AI

2026-11-09T18:55:19Z

The timeline by which quantum computers can solve breakthrough problems in science depends on improved quantum algorithms as much as on better hardware. Such algorithmic advances are typically achieved through many years of expert human collaboration. In mathematics and computer science, large language models have accelerated progress through automated discovery loops. However, quantum algorithms can only be evaluated by classical computers on restricted or small instances. Here we demonstrate automated discovery of quantum programs beyond these regimes including order-of-magnitude improvements on scientific applications. To achieve this, we build a quantum program library in the Lean theorem prover in which Gemini 4 agents synthesize novel programs against formal problem specifications and verify their correctness and cost. Agent teams collaborate, sharing results and knowledge through wikis and discussing ideas at organized conferences. Our results improve on prior baselines for parallel search (up to 2.55x), quantum arithmetic (290x), and simulations relevant to fusion, photochemistry and drug-metabolism by 11x, 8x and 2.5x respectively. Combining human and artificial intelligence at scale, under the rigor of mathematical proof, lets researchers design algorithms that today's classical and quantum computers cannot test, shortening the path to practical quantum computation.

Validating direct solvers for Newton's gravitational N-body problem, and the systematic comparison between IEEE floating point and Posits

2026-11-09T18:26:30Z

We present a systematic comparison between arbitrary precise arithmetic and integration, IEEE-754 compliant floating point arithmetic (fp16, bfp16, fp32, double precision fp64, and quadruple precision fp128), and two implementations of Posits (type III unum) for solving Newton's chaotic N-body problem. Each implementation is benchmarked with arbitrary precise calculations to objectively evaluate their performance in precision as well as speed. We rely on hardware and compiler implementations for fp64, and software implementations for arbitrary-precision arithmetic and Posits. Half precision arithmetic (fp16, bfp16, and Posits$<16,1>$) are insufficiently precise for solving Newton's equations of motion. Single precision (fp32, and Posits$<32,2>$) could be used for statistical ensemble calculations, but lead to relatively large errors in any individual strong encounter. All 64-bit implementations fp64 as well as Posits (Posits$<64,3>$) experience difficulty in our tests. One of the implementations of Posits (Universal) gives precision comparable to fp64 but is slow (by at least an orders of magnitude compared to fp64 after correcting for the more efficient hardware support for the latter). The other (CPPPosits) has a speed comparable to fp64 but has systematically larger errors (by about an order of magnitude compared to fp64 with excesses exceeding two orders of magnitude). As a consequence, this implementation leads to a systematic drift in the result space and has difficulty resolving close encounters. Posits and fp64 have difficulty when integrating a dynamical system in a moving reference frame; testing Galileo invariancy. In their current implementation, Posits do not seem to be the ideal alternative for fp64 when integrating chaotic or stiff ordinary differential equations, such as Newton's equations of motion.

The Left Ripple of Byte-Pair Encoding: Certified Lookbehind for Every Dictionary

2026-11-09T17:48:27Z

Berglund and van der Merwe formalized byte-pair encoding and bounded how far an appended string can change a tokenization, leaving the converse open: how far can a string prepended on the left change it, which dictionaries make that ripple infinite, and can it be computed efficiently when finite? We answer all three for every dictionary. The origin radius, how far a prepend can change covering spans, is decided with radius certificates by a product of two runs of the automaton that guesses the final tokens, in time polynomial in the dictionary written out, and it is infinite exactly when one periodic word has two canonical tilings with no common boundary. Under their ordering condition it is infinite exactly when some rule (t, t) finds its two copies adjacent at its own stage, and such a rule makes any dictionary infinite. A finite radius makes every window of a width read off the radii have a cut, and the radius is finite exactly when such cuts are dense. The token machine completes for every dictionary, and the tokenization is subsequential, extending what Berglund, Martens and van der Merwe proved for proper ones under one pass per rule. A streaming tokenizer emits after every symbol exactly the tokens that no continuation changes, in polynomial time, answering a question of Dalirrooyfard and Ye. Boundedness of the label measure, the edit distance of the token sequences, is decided for every dictionary in polynomial time as well, and under the ordering condition the largest distance one edit causes over dictionaries of m rules lies asymptotically between m^2/10 and m^2/2. GPT-2's merge table carries 244 effective self-pairs, so its origin radius is infinite from the forty-second merge on, and that of cl100k, o200k and Llama 3 from their first. Every measured number is its program's output, and what is not executed is named.

A Hoare Logic for Continuous-Time Stochastic Processes

2026-11-09T17:38:04Z

Programming language researchers have developed a wide array of tools to reason about probabilistic programs, but it remains unclear how to apply these proof techniques to continuous-time stochastic processes. To bridge this gap, we propose a verification method for properties of continuous-time stochastic processes by reasoning about them as standard programs. To demonstrate our approach, we define a continuous semantics for a probabilistic imperative language $\mathrm{pWhile}^{\mathrm{dt}}$ by taking the Kuratowski limit of the standard semantics, which collects limit points of the standard program semantics as the time-step approaches zero. Then, we present a Hoare-style logic that uses loop invariants and decreasing functions to verify properties of continuous programs. To establish soundness, we identify a broad class of assertions that are preserved from the standard semantics to the continuous semantics. To demonstrate our approach, we verify properties of ten continuous-time stochastic processes modeled in $\mathrm{pWhile}^{\mathrm{dt}}$, including variants of Brownian motion and a stochastic hybrid system.

Ceci n'est pas une pipe: A semantics of justified reliance for AI systems

2026-11-09T16:07:23Z

An AI agent may keep a successful check in context after an edit has invalidated its evidence. We give a semantics for specifying when a system may rely on a message and act on it. Reliability checks an asserted claim against accepted domain knowledge, sources, and messages in the selected context. Justified reliance additionally checks current evidence, authority, and the proposed world change. Relational component semantics and event traces represent nondeterministic outputs, iteration, and external changes. We characterise when merging claims preserves derivable conclusion classes, then construct the coarsest permitted quotient whose rules preserve the exact statuses of designated concrete claims. Construction is polynomial for unary rules; deciding even one permitted merge is coNP-complete for acyclic binary rules. This applies completeness and strong-preservation methods to the execution of quotiented rules. We also relate transition safeguards to runtime enforcement. Relative to a supplied set of possible worlds, a sound guard accepts an observation only when every matching world passes the checks. Exact acceptance requires observations that distinguish opposite-decision worlds; choosing sufficient services is NP-complete on explicit finite tables. A complete finite passport-renewal instance, Lean theorem encodings, Z3 instance checks, and an OCaml harness exercise the semantics. Domain knowledge, interpretation, source licenses, and policy remain application inputs.