Dargent: A Silver Bullet for Verified Data Layout Refinement

on YouTube ↗23m

" summary

Dargent provides a declarative layout language integrated into Cogent that generates verified C getters and setters so algebraic types map to bit-precise memory formats without separate marshalling. The compiler emits C plus Isabelle proofs (via AutoCorres) that preserve Cogent’s functional semantics, proving two key properties: a get after set returns an equivalent value and setters don’t modify other fields. The system handles bitfields and custom-width integers, removes copying overhead, ships usable examples (a verified timer driver and power-control register updates), and currently requires statically sized, non-recursive types.

AI-written summary · about

" chapters (14)

1. 0:00Start
2. 0:30Developing High-Assurance Systems
3. 2:44Cogent's Certifying Compiler
4. 5:06Compilation with Dargent Specifications
5. 6:13Example: Power Control System
6. 7:10An Example of Dargent
7. 9:29Bit Fields
8. 10:30Assigning layouts
9. 11:04Cogent + Dargent Specifications
10. 12:06Auxiliary lemmas (CC HOL)
11. 13:06Compatibility with layouts
12. 13:23Compliance with the layout
13. 13:58Related Work
14. 15:04Conclusion