Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2611.06924

Replay Is a Family of Assertions: Fork-Safety in Event-Sourced Agent Runtimes

Yohei Nakajima
View original source ↗Read source document ↗Export metadata ↓

Abstract

Event-sourced agent runtimes commonly claim deterministic replay, cheap forking, and lineage. These are families of assertions, not one guarantee. A fixed-log fold may be deterministic while reactive settlement remains schedule-sensitive; a recorded oracle result can enable zero-call replay while the original interaction still changed cost or world state; and a prefix copy cannot undo an action in a discarded suffix. We present an executable F# contract that separates facts from effect requests, makes scheduling explicit, and assesses a cut relative to projection, strict execution replay, external continuation, or a declared counterfactual-world observation. Preserved counterexamples show that general settlement is neither terminating nor confluent and that disjoint declared writes do not prevent read/trigger interference. Against 5,540 public runtime logs, all 317,296 projection cuts satisfy the stated observation, while 36,251 cuts split a model request and do not license continuation; another 120,969 are Conditional because a committed oracle result must be served from the record without re-execution. In 121 observed forks, 16,625 retained-prefix events have zero structural mismatches, but none crosses an external-effect boundary. A separate public offline conformance fork crosses a committed, recorded oracle boundary. Its generator observes that the inherited result is served without a second fixture-oracle call; its verifier checks receipt/log consistency and a fork-bound HMAC assertion under a public conformance key. The result reframes cheap forking as a property-indexed semantic contract with explicit evidence and environment preconditions.

Explore related subjects

cs.PLcs.SE

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Yohei Nakajima. 2026-08-29. Replay Is a Family of Assertions: Fork-Safety in Event-Sourced Agent Runtimes. https://arxiv.org/abs/2611.06924

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Silent Degradation during Auto-Vectorization of bf16/fp16 on RISC-V Under LLVM

Low-precision numeric types such as 8-bit integers, bfloat16, and half-precision floating point (fp16) are often used in AI inference workloads to reduce memory bandwidth, and RISC-V's openly specified Vector extension (RVV) is a natural target for compiling such workloads with auto-vectorization. This paper examines whether LLVM's RISC-V auto-vectorizer handles these narrow types equally well, using a multiply-accumulate loop written for fp32, int8, bf16, and fp16. Under a common baseline target (-march=rv64gcv), int8 and fp32 vectorize cleanly, while bf16 and fp16 degrade to increasingly scalar-heavy fallback code, with fp16 falling back to per-element software conversion calls, unless additional target-feature extensions (zvfbfmin/zvfbfwma, zvfhmin) are enabled. Under QEMU user-mode emulation, the baseline bf16 and fp16 kernels execute $17.0\times$ and $75.9\times$ as many dynamic instructions as their extension-enabled counterparts. Compiler diagnostics do report this degradation, but do not distinguish, in their wording, between a limitation that a compiler flag resolves entirely and one reflecting an inherent conversion cost, leaving no direct signal toward the fix. These results are supported by assembly-level instruction analysis, by direct inspection of LLVM's optimization remarks, and by dynamic instruction counts collected under emulation.

cs.PL↗
arXiv2026

Verified Implementation of the Next-gen Borrow Checking Algorithm for Rust via Abstract Interpretation

Borrow checking is a central mechanism for Rust to ensure temporal memory safety. Its correctness is based on the intuition that the Aliasing XOR Mutability discipline guarantees that programs without borrow errors inherently could not access invalid references (i.e., pointers). However, existing work on formalizing borrow checking treats it either as a component of type systems or as symbolic execution describing resource transfer. None provides a direct explanation of the correctness of borrow checking algorithms such as Non-Lexical Lifetimes (NLL) or Polonius in the official Rust compiler that function more like static pointer analysis. We take a first step toward solving this problem by formalizing Polonius, the next-generation borrow- checking algorithm for the Rust compiler, on a core subset of Rust. We prove its correctness by showing that any program accepted by Polonius does not access invalid references at runtime. The key observation is that, when borrow checking is performed lazily, Polonius could be treated as a forward abstract interpretation on abstract domains recording pointer aliasing (borrowing) relations. By providing a concrete semantics that formally describes the Aliasing XOR Mutability discipline, we prove the soundness of this abstract interpretation, from which we derive memory safety of checked programs. This formulation of Polonius is implemented and formally verified in the abstract interpretation framework of CompCert. The correctness proofs are generated by an agentic AI under human guidance using paper proofs as proof outline. To the best of our knowledge, this is the first comprehensive formalization and verification of a borrow checking algorithm as manifested in the Rust compiler.

cs.PL↗