Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verifica...
summary
Implements a userland F metaprogram that performs whole-call-graph code specialization for Low and compiles to readable C, producing an extra compiler stage and a specialization tactic that emits monomorphic copies rather than function-pointer or massive inlining hacks. Verifies and generates HACL codebases (over 100,000 verified F lines → ~880,000 C lines) and ships specialized streaming-hash implementations into CPython 3.12, yielding a 0.51 F*-to-C code ratio and replacing several buggy reference implementations successfully.
AI-written summary · about
chapters (9)
- 0:00Verified Python cryptography
- 1:05Verified Python 3.12 hashing
- 3:58Python hash algorithm challenges
- 8:51Code specialization for C
- 15:16Rewriting pattern for specialization
- 19:26Hackle Star applications
- 21:33Python hash streaming API
- 24:44Python integration gains
- 25:48Q&A
related talks
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
29müberSpark: Enforcing Verifiable Object Abstractions for Automated...
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
15mAutomatic and Efficient Variability-Aware Lifting of Functional Programs
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
01h 02mLanguage Design meets Verifying Compilers
01h 16mPolymorphism, Cohesion, and Coupling in C++
17mCode-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into(…)