arXiv subjects

Exequiel Rivas

Publications and source records attributed to Exequiel Rivas.

9 recordsLinked to original sources

arXiv2026

Misquoted No More: Securely Extracting F* Programs with IO

Shallow embeddings that use monads to represent effects are popular in proof-oriented languages because they are convenient for formal verification. Once shallowly embedded programs are verified, they are often extracted to mainstream languages like OCaml or C and linked into larger codebases. The extraction process is not fully verified because it often involves quotation -- turning the shallowly embedded program into a deeply embedded one -- and verifying quotation remains a major open challenge. Instead, some prior work obtains formal correctness guarantees using translation validation to certify individual extraction results. We build on this idea, but limit the use of translation validation to a first extraction step that we call relational quotation and that uses a metaprogram to construct a typing derivation for the given shallowly embedded program. This metaprogram is simple, since the typing derivation follows the structure of the original program. Once we validate that the typing derivation is valid for the original program, we pass it to a verified syntax-generation function that produces code guaranteed to be semantically related to the original program. We apply this general idea to build SEIO*, a framework for extracting shallowly embedded F* programs with IO and refinement types to a deeply embedded simply typed lambda-calculus while providing formal secure compilation guarantees. Using two cross-language logical relations, we devise a machine-checked proof in F* that SEIO* guarantees Robust Relational Hyperproperty Preservation (RrHP), a very strong secure compilation criterion that implies full abstraction as well as preservation of trace properties and hyperproperties against arbitrary linked adversarial code. This goes beyond the state of the art in verified and certifying extraction, which so far has focused on correctness rather than security.

cs.PL↗

arXiv2025

Formalizing a classification theorem for low-dimensional solvable Lie algebras in Lean

We present a formalization, in the theorem prover Lean, of the classification of solvable Lie algebras of dimension at most three over arbitrary fields. Lie algebras are algebraic objects which encode infinitesimal symmetries, and as such ubiquitous in geometry and physics. Our work involves explicit calculations on the level of the underlying vector spaces and provides a use case for the linear algebra and Lie theory routines in Lean's mathematical library mathlib. Along the way we formalize results about Lie algebras, define the semidirect product within this setting and add API for bases of vector spaces. In a wider context, this project aims to provide a complete mechanization of a classification theorem, covering both the statement and its full formal proof, and contribute to the development and broader adoption of such results in formalized mathematics.

cs.LO↗

arXiv2025

SecRef: Securely Sharing Mutable References Between Verified and Unverified Code in F

We introduce SecRef*, a secure compilation framework protecting stateful programs verified in F* against linked unverified code, with which the program dynamically shares ML-style mutable references. To ease program verification in this setting, we propose a way of tracking which references are shareable with the unverified code, and which ones are not shareable and whose contents are thus guaranteed to be unchanged after calling into unverified code. This universal property of non-shareable references is exposed in the interface on which the verified program can rely when calling into unverified code. The remaining refinement types and pre- and post-conditions that the verified code expects from the unverified code are converted into dynamic checks about the shared references by using higher-order contracts. We prove formally in F* that this strategy ensures sound and secure interoperability with unverified code. Since SecRef* is built on top of the Monotonic State effect of F*, these proofs rely on the first monadic representation for this effect, which is a contribution of our work that can be of independent interest. Finally, we use SecRef* to build a simple cooperative multi-threading scheduler that is verified and that securely interacts with unverified threads.

cs.PL↗

arXiv2023

Securing Verified IO Programs Against Unverified Code in F*

We introduce SCIO*, a formally secure compilation framework for statically verified partial programs performing input-output (IO). The source language is an F* subset in which a verified program interacts with its IO-performing context via a higher-order interface that includes refinement types as well as pre- and post-conditions about past IO events. The target language is a smaller F* subset in which the compiled program is linked with an adversarial context that has an interface without refinement types, pre-conditions, or concrete post-conditions. To bridge this interface gap and make compilation and linking secure we propose a formally verified combination of higher-order contracts and reference monitoring for recording and controlling IO operations. Compilation uses contracts to convert the logical assumptions the program makes about the context into dynamic checks on each context-program boundary crossing. These boundary checks can depend on information about past IO events stored in the state of the monitor. But these checks cannot stop the adversarial target context before it performs dangerous IO operations. Therefore linking in SCIO* additionally forces the context to perform all IO actions via a secure IO library, which uses reference monitoring to dynamically enforce an access control policy before each IO operation. We prove in F* that SCIO* soundly enforces a global trace property for the compiled verified program linked with the untrusted context. Moreover, we prove in F* that SCIO* satisfies by construction Robust Relational Hyperproperty Preservation, a very strong secure compilation criterion. Finally, we illustrate SCIO* at work on a simple web server example.

cs.PL↗

arXiv2019

Interaction laws of monads and comonads

We introduce and study functor-functor and monad-comonad interaction laws as mathematical objects to describe interaction of effectful computations with behaviors of effect-performing machines. Monad-comonad interaction laws are monoid objects of the monoidal category of functor-functor interaction laws. We show that, for suitable generalizations of the concepts of dual and Sweedler dual, the greatest functor resp. monad interacting with a given functor or comonad is its dual while the greatest comonad interacting with a given monad is its Sweedler dual. We relate monad-comonad interaction laws to stateful runners. We show that functor-functor interaction laws are Chu spaces over the category of endofunctors taken with the Day convolution monoidal structure. Hasegawa's glueing endows the category of these Chu spaces with a monoidal structure whose monoid objects are monad-comonad interaction laws.

cs.LO↗

arXiv2019

The Next 700 Relational Program Logics

We propose the first framework for defining relational program logics for arbitrary monadic effects. The framework is embedded within a relational dependent type theory and is highly expressive. At the semantic level, we provide an algebraic presentation of relational specifications as a class of relative monads, and link computations and specifications by introducing relational effect observations, which map pairs of monadic computations to relational specifications in a way that respects the algebraic structure. For an arbitrary relational effect observation, we generically define the core of a sound relational program logic, and explain how to complete it to a full-fledged logic for the monadic effect at hand. We show that this generic framework can be used to define relational program logics for effects as diverse as state, input-output, nondeterminism, and discrete probabilities. We, moreover, show that by instantiating our framework with state and unbounded iteration we can embed a variant of Benton's Relational Hoare Logic, and also sketch how to reconstruct Relational Hoare Type Theory. Finally, we identify and overcome conceptual challenges that prevented previous relational program logics from properly dealing with control effects, and are the first to provide a relational program logic for exceptions.

cs.PL↗

arXiv2019

Dijkstra Monads for All

This paper proposes a general semantic framework for verifying programs with arbitrary monadic side-effects using Dijkstra monads, which we define as monad-like structures indexed by a specification monad. We prove that any monad morphism between a computational monad and a specification monad gives rise to a Dijkstra monad, which provides great flexibility for obtaining Dijkstra monads tailored to the verification task at hand. We moreover show that a large variety of specification monads can be obtained by applying monad transformers to various base specification monads, including predicate transformers and Hoare-style pre- and postconditions. For defining correct monad transformers, we propose a language inspired by Moggi's monadic metalanguage that is parameterized by a dependent type theory. We also develop a notion of algebraic operations for Dijkstra monads, and start to investigate two ways of also accommodating effect handlers. We implement our framework in both Coq and F*, and illustrate that it supports a wide variety of verification styles for effects such as exceptions, nondeterminism, state, input-output, and general recursion.

cs.PL↗

arXiv2018

Relating Idioms, Arrows and Monads from Monoidal Adjunctions

We revisit once again the connection between three notions of computation: monads, arrows and idioms (also called applicative functors). We employ monoidal categories of finitary functors and profunctors on finite sets as models of these notions of computation, and develop the connections between them through adjunctions. As a result, we obtain a categorical version of Lindley, Yallop and Wadler's characterisation of monads and idioms as arrows satisfying an isomorphism.

cs.PL↗

arXiv2014

Notions of Computation as Monoids

There are different notions of computation, the most popular being monads, applicative functors, and arrows. In this article we show that these three notions can be seen as monoids in a monoidal category. We demonstrate that at this level of abstraction one can obtain useful results which can be instantiated to the different notions of computation. In particular, we show how free constructions and Cayley representations for monoids translate into useful constructions for monads, applicative functors, and arrows. Moreover, the uniform presentation of all three notions helps in the analysis of the relation between them.

cs.LO↗