Comment by addaon

Comment by addaon 6 days ago

I've wanted for years to take the research paper "Coq: The World's Best Macro Assembler" through several of its more and less obvious next steps, including re-implementing it on top of a formal specification of ARM (or RISC-V) machine code, and introducing a concept of virtual registers on top of a (light weight) register allocator. I really feel like there's a path here to a system in which low-level non-portable code can be written comfortably (if perhaps at a somewhat slower pace than C), with arbitrary correctness properties proven on it; but the learning curve to get there (through Coq, etc) has been a struggle. Every few years I set myself the goal of a proven-correct implementation of a min/max heap in assembly built on this approach, and every few years I give up.

ecesena 6 days ago

Not in Coq, but you might find this interesting from AWS: https://github.com/awslabs/s2n-bignum?tab=readme-ov-file#tes...

Reply View 3 replies

addaon 6 days ago

I've just taken a quick glance at this, and will explore further -- but at first, it seems like it's really a good application of ad-hoc proofs to assembly code; which is a subset of what I'm interested in, but for me the more interesting thing about the paper was the structured safety proofs for things like memory safety, no read-before-write, no overflow, etc., and thinking about how this can be expanded and generalized. While for something like a bignum library (or a heap) the actual conformance to the behavioral contract will be somewhat ad-hoc, having a lot of safety contracts also proved along the way "for free" (or at slightly reduced cost, anyway) is what really draws my attention. I can see spending 2x the time writing the code, and 10x the time proving things about it, in exchange for not having to spend the 100x (DAL B) or 1000x (DAL A) time testing it.

Reply View | 2 replies
- ecesena 5 days ago
  
  Yeah, I hear you. Many things are simplified in this crypto code, for example there’s no dynamic allocation. At the same time it’s incredibly difficult to get a realistic model of the hardware instructions because they all have side effects. And it gets incredibly more difficult if you try to prove real world, hand optimized code (vs academic proof of concept code).
  With all this said, I think this could be a good inspiration and look forward to seeing advancements!
  
  Reply View | 1 reply
  
  addaon 4 days ago
  
  > Many things are simplified in this crypto code, for example there’s no dynamic allocation.
  That's okay, I haven't worked on code bases with dynamic allocation professionally in years, and even my hobby projects usually avoid it.
  
  Reply View | 0 replies