Incremental computing promises large speed-ups after small input edits. Yet, most incrementality approaches merely skip unchanged work and recompute the remaining sub-computations, even when the inputs change only slightly. Differential execution avoids this by propagating data changes (i.e., deltas), and prior work has shown how to develop a provably correct differential big-step semantics. Unfortunately, that semantics must still replay the original computation at every step, squandering much of the potential gain of incrementalization. While the semantics clearly needs caching to avoid recomputations, a sound and efficient caching discipline is challenging. First, each execution step must be uniquely identified; second, the identifier must remain stable even when the preceding control flow changes. To this end, we develop lexical tracing , which identifies execution steps through their path in the derivation tree of the big-step semantics. We then extend differential execution with lexical tracing and caching to deliver, for the first time, a formally verified, asymptotically efficient account of differential execution for imperative languages. In particular, we developed a novel mechanized theory of cache stability for lexical traces and their semantic rules, which was essential in proving the differential caching semantics correct and complete in Rocq.

Differential operators map input changes to output changes and form the building blocks of efficient incremental computations. For example, differential operators for relational algebra are used to perform live view maintenance in database systems. However, few differential operators are known and it is unclear how to develop and verify new efficient operators. In particular, we found that differential operators often need to use internal state to selectively cache relevant information, which is not supported by prior work. To this end, we designed a specification for stateful differential operators that allows custom state, yet places sufficient constraints to ensure correctness. We model our specification in Rocq and show that the specification not only guides the design of novel differential operators, but also can capture some of the most sophisticated existing differential operators: database join and Datalog aggregation. We show how to describe complex incremental computations in OCaml by composing stateful differential operators, which we have extracted from Rocq.

Dilithium is a signature scheme that is currently being standardized to the Module-Lattice-Based Digital Signature Standard by NIST. It is believed to be secure even against attacks from large-scale quantum computers based on lattice problems. The implementation efficiency is important for promoting the migration of current cryptography algorithms to post-quantum cryptography algorithms. In this article, we optimize the implementation of Dilithium with several new approaches proposed. Firstly, we improve the efficiency of parallel NTT implementations. The overhead of shuffling operations is reduced in our implementations, and fewer loading instructions are invoked for the precomputations. Then, we optimize the sampling and bit-packing of polynomial coefficients in Dilithium. We can handle double the number of coefficients within one register using a new approach for the sampling of secret key polynomials. The approaches proposed in this article are applicable to implementations under AVX2 and AVX-512 instruction sets. Take Dilithium2 as an illustration, our AVX2 implementation demonstrates improvements of 22.7%, 16.9%, and 13.5% for KeyGen, Sign, and Verify compared with the previous implementation.

Abstract The need to verify symbolic computation arises in diverse application areas. In this paper, based on earlier work on verifying computation of definite integrals in , we present a tool for performing a variety of symbolic computations interactively, taking a middle ground in terms of easy of use and rigor between computer algebra systems and interactive theorem provers. The tool supports user-level definitions and dependency among computations, allowing construction and reuse of custom theories. Side conditions are checked on a best-effort basis. The tool is applied to highly non-trivial computations from the textbook Inside Interesting Integrals.

Abstract Symbolic computation is involved in many areas of mathematics, as well as in analysis of physical systems in science and engineering. Computer algebra systems present an easy-to-use interface for performing these calculations, but do not provide strong guarantees of correctness. In contrast, interactive theorem proving provides much stronger guarantees of correctness, but requires more time and expertise. In this paper, we propose a general framework for combining these two methods, and demonstrate it using computation of definite integrals. It allows the user to carry out step-by-step computations in a familiar user interface, while also verifying the computation by translating it to proofs in higher-order logic. The system consists of an intermediate language for recording computations, proof automation for simplification and inequality checking, and heuristic integration methods. A prototype is implemented in Python based on HolPy, and tested on a large collection of examples at the undergraduate level.