Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises

Explore a groundbreaking approach to implementing cryptographic arithmetic in this 18-minute IEEE conference talk. Discover how to create short, high-level code with machine-checked proofs of functional correctness, and learn how simple partial evaluation can transform it into the fastest-known C code. Examine the development of an elliptic-curve library that achieves competitive performance across 80 prime fields and multiple CPU architectures. Gain insights into the first verified high-performance implementation of P-256, the most widely used elliptic curve. Follow the journey of how these implementations were integrated into BoringSSL, replacing existing specialized code for major deployments in Chrome, Android, and CloudFlare. Delve into topics such as compile-time representation, call-by-value evaluation, specialized versions, known weights, and the technical deliverables that made this innovation possible.

Introduction
The Problem
The Solution
Performance
Architecture
Compile Time Representation
Example Code
CallbyValue Evaluation
Specialized Version
Known Weights
Gathering the Weights
Steps
Coefficients
Assigning fixed integers
What took time
Technical deliverable
Conclusion