Simple High-Level Code For Cryptographic Arithmetic With Proofs, Without Compromises
We introduce an unusual approach for implementing cryptographic arithmetic in short high-level code with machinechecked proofs of functional correctness. We further demonstrate that simple partial evaluation is sufficient to transform such initial code into highly competitive C code, breaking the de...
| Main Authors: | , , , , |
|---|---|
| Other Authors: | , |
| Format: | Article |
| Language: | English |
| Published: |
Association for Computing Machinery (ACM),
2021-07-14T15:11:01Z.
|
| Subjects: | |
| Online Access: | Get fulltext |