FFI call C from within Lean

Stream: lean4

[Tage Johansson]

When reading the FFI chapter of the Lean 4 manual, I get the impression that it is (at the moment) only possible to call Lean functions from C and not call external C-functions from Lean. Is that correct or is there some way to make use of external libraries from a Lean program?

[Arthur Paulino]

I think that's backwards. We use the C FFI to call C implementations from Lean

[Tage Johansson]

I think that's backwards. We use the C FFI to call C implementations from Lean

Do you have some example of that? A link to a source file on github would be fine.

[Arthur Paulino]

Yes, you can find some examples here: https://github.com/yatima-inc/YatimaStdLib.lean

This is the setup to make it work: https://github.com/yatima-inc/YatimaStdLib.lean/blob/main/lakefile.lean

This is the C code that has some fast implementations: https://github.com/yatima-inc/YatimaStdLib.lean/blob/main/YatimaStdLib/FFI/ffi.c

And this is how you can refer to them in Lean: https://github.com/yatima-inc/YatimaStdLib.lean/blob/main/YatimaStdLib/FFI/UIntByteArray.lean (with the extern tag)

[Arthur Paulino]

I defined them as opaque but that's not needed. You may also have regular definitions if you want to prove properties about them. When compiled, it will use your C code instead. But the responsibility for maintaining semantics is on you

[Arthur Paulino]

Example: ByteArray.copySlice

/--
  Copy the slice at `[srcOff, srcOff + len)` in `src` to `[destOff, destOff + len)` in `dest`, growing `dest` if necessary.
  If `exact` is `false`, the capacity will be doubled when grown. -/
@[extern "lean_byte_array_copy_slice"]
def copySlice (src : @& ByteArray) (srcOff : Nat) (dest : ByteArray) (destOff len : Nat) (exact : Bool := true) : ByteArray :=
  ⟨dest.data.extract 0 destOff ++ src.data.extract srcOff (srcOff + len) ++ dest.data.extract (destOff + len) dest.data.size⟩