François Garillot

François Garillot

Research engineer and coffee fan.

Sitemap

A list of all the posts and pages found on the site. For you robots out there is an XML version available for digesting as well.

Pages

Posts

Drilling down on Rust Performance Bottlenecks with tokio-tracing and texray

10 minute read

Published:

When a Rust program feels sluggish, adding instrumentation can shine a light on where the time is going. In this post, we’ll walk through a guided journey of using Tokio’s tracing framework and the tracing-texray tool to drill into performance issues. We assume you’re familiar with the basics of tokio-tracing (if not, see the Tokio tracing introduction for spans and events fundamentals). Our journey will start with a simple sequential task, then ramp up to parallel execution and illustrate how to maintain insight at each step.

Byzantine-Consistent Broadcast- A Promising Yet Challenging Frontier in Digital Asset Transfers

7 minute read

Published:

Digital asset transfer systems are at a crossroads. An idea that first captured attention between 2020 and 2022—Byzantine Consistent Broadcast (BCB)—is now experiencing a revival with projects like Pod and Delta. In this post, we to show that while BCB can unlock incredible performance through parallel state execution, it also introduces important challenges, especially around expressivity and the scalability of reads. The goal is to explain why this approach is both exciting and demanding.

PSA: maven central and sonatype are slow

less than 1 minute read

Published:

Most of the public maven repositories for downloading java artifacts (notably maven-central, and sonatype) are slow. Besides, build tools do not have a perfect track record of resolving dependencies from these repositories in an efficient manner.

May 2016 time series storage roundup

1 minute read

Published:

A recent slew of blogs and articles have been shedding new insight on time series storage. I thought I’d list some of the zeitgeist.

A quick update on Spark Streaming work

3 minute read

Published:

Since I was asked a few times here at Scala Days, I thought I’d write an update on how some of our work on making Spark Streaming more resilient is going. Naturally, all of this is open-source, otherwise I wouldn’t be writing this.

Look, Ma, no queues!

4 minute read

Published:

A very classic, if a bit overrated exercise, is to print a tree in width-first order. Also called level-order, it means you print your binary tree row-by-row, with the nodes of depth d, leftmost first, before the nodes of depth d+1.

Every freshman CS question in ±80 lines of Scala

14 minute read

Published:

This post is about writing a single program that returns the stream representing any recursive sequence of order $k$, which $i$th term a[i] = f(a[i-1], a[i-2], ... a[i-k]), for all $k$, in Scala. It explains things very slowly: If the meaning of the previous sentence is already 100% clear to you, you can easily skip the next 2 paragraphs.

Certifying RSA correct for breakfast

7 minute read

Published:

Reasoning on the correctness of the RSA cryptosystem is much easier with a little bit of algebra: this is a perfect example of a case where the ``practical’’ applications of proof assistants can be helped with libraries dealing with abstract algebra, including SSReflect. The proof we are going to build in the present post is based on a stock SSReflect version 1.3pl1, and is available on github. It can be compared with the RSA contribution to Coq, made on the basis of the standard library (note this is not a code golf, but rather a tentative to demonstrate that a big mathematical library helps).

How do you make a recursive merge sort more efficient in Python?

5 minute read

Published:

This is re-worked from an excerpt of an answer of mine (1) to an SO question that made me discover some interesting things about Python : turns out it’s not easy to make recursion faster by doing tail call elimination, even by hand. (2)

  1. Initially fraught with errors, and therefore duly ill-scored. ↩

  2. This has also benefited a lot of a discussion with Carey Underwood below and in a reddit thread on this post. Many thanks ! ↩

Ligtweight profiling for your Coq hacks

3 minute read

Published:

Let’s suppose we want to hack a few functions in the Coq compiler. The classic situation is that we have the base implementation of our function as it stands, and an optimized version for which we want to check it really improves things.

portfolio

publications

talks

Taming the Many EddSAs

Published:

In this talk we will discuss the security of concrete instantiations of EdDSA by identifying exploitable inconsistencies between standardization recommendations and Ed25519 implementations. We will mainly focus on current ambiguity regarding signature verification equations, binding and malleability guarantees, and incompatibilities between randomized batch and single verification. Based on our work that appeared at SSR 2020, we will give a formulation of the Ed25519 signature scheme that achieves the highest level of security, explaining how each step of the algorithm links with the formal security properties.

Lambda the Ultimate Recursive Knowledge

Published:

We introduce Lurk, a groundbreaking LISP-based programming language for zk-SNARKs. Unlike conventional approaches that involve compiling computations into flat circuits, Lurk allows programs to be provided as data to the universal Lurk interpreter circuit. This innovative design empowers Lurk with Turing-completeness, without sacrificing the size of the resulting proof artifacts.

Nova ZK Proof Verification in the EVM

Published:

We introduce the challenges of writing a verifier for the Nova ZKP system on Ethereum, and the methods used to overcome those challenges.

Lurk: Lambda, the Ultimate Recursive Knowledge

Published:

We introduce Lurk, a new LISP-based programming language for zk-SNARKs. Traditional approaches to programming over zero-knowledge proofs require compiling the desired computation into a flat circuit, imposing serious constraints on the size and complexity of computations that can be achieved in practice. Lurk programs are instead provided as data to the universal Lurk interpreter circuit, allowing the resulting language to be Turing-complete without compromising the size of the resulting proof artifacts. Our work describes the design and theory behind Lurk, along with detailing how its implementation of content addressing can be used to sidestep many of the usual concerns of programming zero-knowledge proofs.

Front-Running the Aggregate: Proofcoin as a New Paradigm for Security and Flexibility

Published:

Proofcoin, a next-generation decentralized Layer 2 solution with an Ethereum backstop, redefines how proof aggregation can enhance security without compromising user flexibility. In this talk, we’ll explore how Proofcoin employs aggregation, not for programmability, but as a foundation for security. Rather than relying on aggregated proofs as a programming model, Proofcoin provides users with proof certificates that they can work with directly, effectively front-running the aggregate.

teaching