Three questions to Nomadic Labs interns — Antonio Locascio - Deepstash

1. model a piece of OCaml code in F*, specifying and proving interesting properties that it should satisfy.

2. extract a certified OCaml implementation from the model, with which to replace the original implementation.

3. extract the specification itself from the model, as Property Based Tests for the OCaml code.

We consider this last step very important, as it helps to close the verification gap , i.e. the semantic difference between the verified model and the actual OCaml code.

2 STASHED

Concretely, I’ve first applied this workflow to the implementation of Sapling , a protocol used in Tezos for enabling privacy-preserving transactions. The main verification effort for this initial case study was focused on its storage, which consists of a special type of Merkle tree. After finishing with it, I’ve moved on to the ZK -Rollup project , which proposes a Layer 2 scalability solution with minimal impact on the main chain. Before starting its verification, I’ve been working on a prototype OCaml implementation that is helpful for tinkering with its design.

2 STASHED

As Antonio’s mentors, our role is to provide guidance based on our combined experience working on the development of the Tezos Economic Protocol, on mechanized software development and verification, and in the toolchain itself. We plant seeds, in the form of suggesting relevant academic literature or related projects; we brainstorm ideas together; we provide feedback on his contributions; and answer his questions. Occasionally, we also warn him of known pitfalls, and of Here be dragons .

2 STASHED

Making verification techniques scale up to a large industrial, cutting edge, project is a Herculean task. In our case, one of the great hurdles is tightening the verification gap between a mechanization in F*, and the real-world Tezos implementation in OCaml. In a large and complex codebase like ours, there is inevitably a semantic distance between the abstract models we build for the verification of critical components of the Tezos Economic Protocol, such as Sapling or ZK -rollups, and the nitty-gritty of their implementation.

2 STASHED

Deepstash helps you become inspired, wiser and productive, through bite-sized ideas from the best articles, books and videos out there.

GET THE APP: