Learn more about computerscience with this collection
How to analyze churn data and make data-driven decisions
The importance of customer feedback
How to improve customer experience
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.
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.
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 .
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.
In an ideal world, we would like to have a development cycle which efficiently integrates and interweaves concurrent verification and development efforts. This requires developing common specification styles and languages that can be shared by developers and verifiers. This internship provides a plausible approach: by extracting specs from F* and translating them directly to QCheck tests, we can ensure that the specs and definitions in both F* and OCaml — that is both in Proofs and Tests — are two correct reifications of the same concepts.
More like this
Explore the World’s
Take Your Ideas
Just press play and we take care of the words.
No Internet access? No problem. Within the mobile app, all your ideas are available, even when offline.
2 Million Stashers
Best app ever! You heard it right. This app has helped me get back on my quest to get things done while equipping myself with knowledge everyday.
Great interesting short snippets of informative articles. Highly recommended to anyone who loves information and lacks patience.
This app is LOADED with RELEVANT, HELPFUL, AND EDUCATIONAL material. It is creatively intellectual, yet minimal enough to not overstimulate and create a learning block. I am exceptionally impressed with this app!
Don’t look further if you love learning new things. A refreshing concept that provides quick ideas for busy thought leaders.
I have only been using it for a few days now, but I have found answers to questions I had never consciously formulated, or to problems I face everyday at work or at home. I wish I had found this earlier, highly recommended!
Brilliant. It feels fresh and encouraging. So many interesting pieces of information that are just enough to absorb and apply. So happy I found this.
Even five minutes a day will improve your thinking. I've come across new ideas and learnt to improve existing ways to become more motivated, confident and happier.
Great for quick bits of information and interesting ideas around whatever topics you are interested in. Visually, it looks great as well.
Read & Learn
Access to 200,000+ ideas
Access to the mobile app
Unlimited idea saving & library
Unlimited listening to ideas
Downloading & offline access
Supercharge your mind with one idea per day
Enter your email and spend 1 minute every day to learn something new.
I agree to receive email updates