A Verified Pipeline from a Specification Language to Optimized, Safe Rust
summary
A verified pipeline converts hacspec executable specs to optimized, safe Rust by adding a Coq backend for hacspec, synthesizing low-level code with Fiat Cryptography, embedding and proving code in bedrock2 using separation logic for memory safety and functional correctness, then printing to Rust. Applied to BLS12-381 curves, the end-to-end artifacts are about 5.5k LOC and currently run ~80% slower than unverified Rust equivalents; proofs succeed, printing verification remains future work.
AI-written summary · about
chapters (5)
- 0:00Start
- 6:12Overview
- 7:00Case Study. The BLS12 381 Curves
- 11:08Verified Printing to Rust
- 13:02Metrics and Conclusion
related talks
19mA Hybrid Approach to Semi-automated Rust Verification
17mRefinedRust: A Type System for High-Assurance Verification of Rust Programs
15mAeneas: Rust Verification by Functional Translation
09mFormally Secure Hardware with Rust
06mLayered Configuration and Safe Hot Reload in Rust
21mA Tour of Empirical Verification in Rust
21mMaking Concurrent Hardware Verification Sequential
26mBuilding Private And Secure Applications Easily Using The Sunscreen FHE Compiler&Rust