how does "proofs for performance and profit" work?

Stream: lean4

[Daniel Fabian]

I'm really excited for lean 4 and I've been following the various lectures. Today I re-visited an older one from about 9 months ago. There's a slide that says you can use proofs to make more efficient machine code.

The examples given were:

• avoiding array bounds checks if you have a proof that your index is in bounds
• avoiding execution of a continuation function k, if you know that x = y -> k () = true and you know that x and y are pointer equal

Now, I obviously see how you can write more efficient code by hand if you know these properties hold, but in the slide it said, that the compiler generates better code. How does that work?

[Sebastian Ullrich]

The short answer is that the compiler does not know about proofs (only how to detect and eliminate them), but some primitives do:

• https://github.com/leanprover/lean4/blob/e228ca38b812af098046b63f049d3c0e5f6c8e0c/src/Init/Data/Array/Basic.lean#L36-L41
• https://github.com/leanprover/lean4/blob/e228ca38b812af098046b63f049d3c0e5f6c8e0c/src/Init/Util.lean#L43-L44 (see also https://icfp20.sigplan.org/details/icfp-2020-papers/13/Sealing-Pointer-Based-Optimizations-Behind-Pure-Functions)

In both cases we use optimized but unsafe code (once in C++, once in unsafe Lean) that (we assume) becomes safe by the presence of the proof

[Daniel Fabian]

Ah I see, you use the implementedBy or extern for an efficient manual implementation and use the pure reference implementation for type checking purposes only.