FFI to Rust/C++

Stream: lean4

[Tage Johansson]

I tried to build the Rust FFI template in this repo. It basicly compiles the Rust functions to a static c++ library and then uses functions from that in the lean code. But for some strange reason lake build fails on my machine. I get the following strange error:

Compiling shim.cpp
Creating libffi.a
Linking libffi.so
Building FFI
error: > LEAN_PATH=./build/lib LD_LIBRARY_PATH=/home/tage/.elan/toolchains/leanprover--lean4---nightly-2022-12-08/lib:./build/lib:./build/src /home/tage/.elan/toolchains/leanprover--lean4---nightly-2022-12-08/bin/lean ./lean/./FFI.lean -R ./lean/. -o ./build/lib/FFI.olean -i ./build/lib/FFI.ilean -c ./build/ir/FFI.c --load-dynlib=libffi.so
error: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library, ./build/src/libffi.so: undefined symbol: _ZNSt8ios_base4InitD1Ev
error: external command `/home/tage/.elan/toolchains/leanprover--lean4---nightly-2022-12-08/bin/lean` exited with code 134

I think the point here is the undefined symbol _ZNSt8ios_base4InitD1Ev. After some googling it seems that it has something to do with the linking of libc++.so.

So does anyone have any experience of linking c++ libraries and what might cause the error?

[Arthur Paulino]

Yeah, this is something we've been trying to do for a while. So far, the setup is flaky and doesn't work on all machines. There is a nix branch that seems to work though (I haven't tested it yet). This is highly experimental at this point, as you can see

[Henrik Böving]

Is there a reason you are going over C++ instead of just using the C FFI that we already have in Lean? In theory we could auto generate all of the Lean <-> C FFI <-> Rust glue code automatically just from the types that are in Lean without dealing with C++ at all.

[Henrik Böving]

Basically like https://github.com/rust-lang/rust-bindgen but for Lean instead (of course the tool would be written in Lean instead of Rust in order to access the Environment.

[Arthur Paulino]

Do you mean parsing Rust code in Lean?

[Henrik Böving]

No. When you compile lean code and you tag a declaration with @[export] you can know the symbol name in advance, furthermore you can also deduce the C type of the function in advance based on our FFI. Since you can do this you can also automatically decude a Rust representation of any Lean type automatically (based on #[repr(C)], however many lean types will end up being lean_object*. For that you can define type aliases + wrapper functions to allocate and pattern match on stuff). So in theory I believe it should be possible to automatically generate a .rs file using a Lean program that reads some other Lean file and exposes all of the functions tagged with export in that Lean file to Rust + at least working representation of all Lean types defined in that file in Rust. I don't think that representation and the way you interact with it will necessarily end up being safe but it should in general be possible.

[Henrik Böving]

So basically writing a bindgen that generates a Rust C FFI layer for some arbitrary Lean file automatically should be perfectly possible.

[Arthur Paulino]

Sorry, I still don't understand it. Suppose we have some huge Rust lib whose behavior we want to access from Lean. How would an automatically generated .rs file help us bridge the gap between Lean and Rust?

[Arthur Paulino]

We want to use access Rust programs from Lean, not the other way around

[Henrik Böving]

Arthur Paulino said:

We want to use access Rust programs from Lean, not the other way around

But surely you are passing Lean objects into those rust programs so you will still need the information about Lean exposed in Rust no? Exposing the Rust types to Lean is also possible via C FFI if you want to.

[Henrik Böving]

What I am confused about is, why are you taking the indirection over the C++ FFI with cxx when both Rust and Lean support C FII.

[Arthur Paulino]

In my mind, it's the flow of data. Lean can use code that's written in C. So does Rust. But we are trying to use code that's written in Rust from Lean

[Arthur Paulino]

The Lean objects that we want to pass are extremely simple, like unboxed unsigned integers and such. Writing the bindings is the easy part - we do it by hand.

[Reid Barton]

But then why is C++ (rather than C) involved?

[Arthur Paulino]

Because that's what https://cxx.rs/ provides

[Reid Barton]

... is there https://c.rs/ ?

[Reid Barton]

Unlucky.

[Reid Barton]

Avoiding C++ should make everything easier.

[Reid Barton]

The C ABI is in general the normal way to do FFI; I imagine it must be supported natively by Rust

[Henrik Böving]

It is, CXX does still use the C ABI under the hood it just hides stuff behind a C++ facade.

[Arthur Paulino]

@Tage Johansson Okay it works now (thanks everyone!!)
The misconception I had was that I didn't think we could call Rust code from C. I thought it was like Lean, which allows us to call C code from it.

Here's the PR with the changes: https://github.com/yatima-inc/FFI.lean/pull/1
You might as well just fetch the c branch

[Anders Christiansen Sørby]

@Arthur Paulino I tried that approach, but I still get the undefined symbol error above. The --load-dynlib doesn't include all the rust library dependencies. Also how this is added to the lean runtime command is rather undocumented. I also need some way of providing the libraries in topological order which is not the default case. How can I add more runtime dynlibs to the lean command invocation by lake?

[Notification Bot]

Anders Christiansen Sørby has marked this topic as unresolved.

[Anders Christiansen Sørby]

I'm trying to link lean with an advanced rust application and using lean as the main entrypoint and executable.

[Anders Christiansen Sørby]

@Mac Is it possible to disable the load dynlib feature in Lake? I don't think I will need this in the interpreter

[Arthur Paulino]

@Anders Christiansen Sørby the repo had to undergo yet another change in order to work when used as a dependency. This is the template: https://github.com/yatima-inc/RustFFI.lean

[Anders Christiansen Sørby]

I based it on that repo, but it is a rust lib with no dependencies so not very representative. With dependencies you need to have all the dynlib dependencies topologically sorted or disable the --load-dynlib

[Anders Christiansen Sørby]

I guess I could do something similar to copy out all those libraries too

[Mac Malone]

Anders Christiansen Sørby said:

Mac Is it possible to disable the load dynlib feature in Lake? I don't think I will need this in the interpreter

Just turn off precompileModules? Oh, I guess you mean turning off loading external shared libraries during interpretation. Sadly, no that is not currently an option. It would be pretty easier to add though.

[Mac Malone]

One important design decision question, though, would be what should happen if a dependent package wants its dependencies dynlibs loaded but the dependency itself does not.

[Sebastian Ullrich]

@Anders Christiansen Sørby
Why does the external shared library not properly declare its dependencies? At least on Unix, loading a correctly linked dynlib should automatically load its dependencies.

[Sebastian Ullrich]

I suppose a simple workaround for avoiding the --load-dynlib though would be not to tell Lake about the library but add it manually to the linker flags

[Anders Christiansen Sørby]

@Mac Yeah, that could be a nice feature.

[Anders Christiansen Sørby]

@Sebastian Ullrich So that would mean using just target instead of externLib?
The library declares some of it's dependencies which is shown by ldd, but not all apparently(?). I don't know why. It is built with rust and cargo to a static lib. Copied over to the build dir. How this interpreter dynamic loading is enabled is mysterious and it would be nice to have an option.
Would love for some more work on the FFI. Maybe someone will make a full rust FFI ABI interface?

[Anders Christiansen Sørby]

@Sebastian Ullrich I've tried handcrafting the link args, but I run into other problems:
Using roughly /home/anderscs/.elan/toolchains/leanprover--lean4---nightly-2023-02-06/bin/leanc -o ./build/bin/remodel ./build/ir/Main.o ./build/ir/Remodel.o -Lbuild/lib/ -Lrust/target/release/deps -lc -lc++ -lc++abi -lffi -lremodel_rust_ffi

Which leads to some undefined references

/nix/store/pnajkjw1fz03z1x27ski1qbx9n3hd4df-binutils-2.39/bin/ld: build/lib//libremodel_rust_ffi.so: undefined reference to `std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >::_M_replace(unsigned long, unsigned long, char const*, unsigned long)'
/nix/store/pnajkjw1fz03z1x27ski1qbx9n3hd4df-binutils-2.39/bin/ld: build/lib//libremodel_rust_ffi.so: undefined reference to `std::__future_base::_Result_base::_Result_base()'
/nix/store/pnajkjw1fz03z1x27ski1qbx9n3hd4df-binutils-2.39/bin/ld: build/lib//libremodel_rust_ffi.so: undefined reference to `std::__throw_bad_cast()'
/nix/store/pnajkjw1fz03z1x27ski1qbx9n3hd4df-binutils-2.39/bin/ld: build/lib//libremodel_rust_ffi.so: undefined reference to `std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >::~basic_string()'
/nix/store/pnajkjw1fz03z1x27ski1qbx9n3hd4df-binutils-2.39/bin/ld: build/lib//libremodel_rust_ffi.so: undefined reference to `std::thread::detach()'
/nix/store/pnajkjw1fz03z1x27ski1qbx9n3hd4df-binutils-2.39/bin/ld: build/lib//libremodel_rust_ffi.so: undefined reference to `std::thread::join()'

Why are these rust symbols not linked? I suppose these are from the rust std lib and intended to be loaded at runtime?

[Anders Christiansen Sørby]

Ok, the answer is that I didn't link with stdc++and Idk why that is needed in a rust binary.

[Reid Barton]

Reading between the lines, it seems like your Rust library has Rust dependencies, and maybe some parts of those are implemented in C++?

[Anders Christiansen Sørby]

Ok, it works now. leanc -o ./build/bin/remodel ./build/ir/Main.o ./build/ir/Remodel.o -Lbuild/lib/ -lssl -lstdc++ -lffi -lremodel_rust_ffi
I think I can remove the -lstdc++ too if I don't include the cxx rust dependency.

[Anders Christiansen Sørby]

Rust shouldn't need stdc++ normally

[Anders Christiansen Sørby]

@Mac Follow up question: How do I add the targets to extraDepTargets without causing unknown identifier '_package.name'

[Anders Christiansen Sørby]

Oh, it was just adding strings not symbols

[Anders Christiansen Sørby]

What would be best practice for working with strings in a Rust to Lean and Lean to Rust context? Is it passing strings to lean_mk_string_from_bytes(str, str_len) based on the string in Rust? Just using lean_mk_string(str) on a null terminated C string borrowed from rust seems to cause segmentation fault.

[Anders Christiansen Sørby]

This causes a segmentation fault. Do I perhaps need to run lean_inc(ns)? @Sebastian Ullrich ?

extern void rust_test(const char* name) {
  //char* namec = malloc();
  lean_obj_res ns = lean_mk_string(name);
  char* name_l = lean_string_cstr(ns);
}

[Sebastian Ullrich]

I don't see how that could fail if the string is indeed null-terminated. But really there's no reason not to use lean_mk_string_from_bytes if you want to avoid the extra conversion

[Anders Christiansen Sørby]

Both of them cause segmentation fault apparently. Does lean_mk_string_from_bytes copy the string? Need to do more debugging next week.

[Sebastian Ullrich]

It does

[Anders Christiansen Sørby]

It causes a segmentation fault and idk why.
Given this rust code calling from inside a tokio runtime:

let name = CString::new(name).expect("CString::new failed");
 unsafe {
        let name_raw = name.into_raw();
        let result = rust_test(name_raw, name_len);
        // Take back ownership and drop
        drop(CString::from_raw(name_raw));
}

This causes a Segmentation fault in 0x000000000447258b in lean::utf8_strlen(char const*, unsigned long) ()

extern char* rust_test(const char* name, size_t name_len) {
  lean_obj_res ns = lean_mk_string_from_bytes(name, name_len);
//...

I've also tried to use the rust as_bytes approach

let name = name.as_bytes();
 unsafe {
        let result = rust_test(name.as_ptr().cast(), name.len());

}

But this also leads to segmentation fault. Can this be due to the pointer being freed before it is passed to C? I'm pretty stuck

[Anders Christiansen Sørby]

@Sebastian Ullrich Do you have some hints?

[Sebastian Ullrich]

There is some way to find out the address of a segfault in gdb, you could check what the correlation to the pointer address in Rust is. Otherwise I can't say anything on these snippets.

[Anders Christiansen Sørby]

gdb reports the segfault in lean::utf8_strlen(char const*, unsigned long), but it seems to happen even when I set the size to 0 and the pointer should never be accessed.

[Anders Christiansen Sørby]

I guess my next step would be to break the error down into even smaller pieces.

[Chase Norman]

@Arthur Paulino When compiling on Mac, I obtain this result:

info: Compiling ffi.c
info: Creating libffi.a
info: Linking libffi.dylib
info: Building Main
info: Linking ffi
dyld[67114]: Library not loaded: @rpath/libc++.1.dylib
  Referenced from: <4C4C44C3-5555-3144-A162-517666152A8B> /Users/chasenorman/Research/RustFFI.lean/build/bin/ffi
  Reason: tried: './build/lib/libc++.1.dylib' (no such file)

libc++.1.dylib is a Mac-specific library that is not anywhere in the filesystem, so it's no wonder it can't find it. I am not sure what is convincing ffi.c that it needs it. Do you have any ideas on what I should do?

[Chase Norman]

Here's a maniacal manual fix:
install_name_tool -change @rpath/libc++.1.dylib /usr/lib/libc++.1.dylib build/bin/ffi

[Arthur Paulino]

Ugh, it's been a while since I've touched this. Unfortunately I can't debug it on a Mac

[Chase Norman]

Honestly, it could be lake's fault. I don't see this library mentioned anywhere explicitly

[Arthur Paulino]

In case someone else can and wants to help, here's the repo I think Chase is talking about: https://github.com/argumentcomputer/RustFFI.lean

Note: the last commit is 2 years old. Things are surely very different nowadays.

[Chase Norman]

Is there anything special you have to do to get FFI working in VSCode? I still get "could not find native implementation of external declaration" even though the compiled binary works

[Arthur Paulino]

How do you make that error message pop up?

[Chase Norman]

@Arthur Paulino
I open the project in VSCode and add #eval addFromRust 1 2

[Arthur Paulino]

Yeah the kernel can't do it because it's not implemented in Lean. The binary works because it's linked in the compilation process

[Chase Norman]

So in general, this is a dead end?

[Arthur Paulino]

AFAIK you won't be able to #eval things implemented in C.

[Chase Norman]

Can tactics use code that is compiled outside of the trusted kernel? I didn't necessarily need to use #eval

[Chase Norman]

Thanks so much for the really quick response, I'd probably flounder for a lot longer otherwise

[Arthur Paulino]

Oh, I'm pretty sure tactics can use implementations accessed via FFI. You just need to figure out a serialization format so the implementations can communicate

[Henrik Böving]

Arthur Paulino said:

AFAIK you won't be able to #eval things implemented in C.

That's wrong, you just wont be able to #reduce, #eval is in no relation to the kernel.

Chase Norman said:

Can tactics use code that is compiled outside of the trusted kernel? I didn't necessarily need to use #eval

yes

[Arthur Paulino]

Ah, right. There's #eval and #reduce. I had forgotten about those two and thought #eval was #reduce. Thanks for the reminder

[Chase Norman]

Serialization was my original solution, I was looking for something a little bit more long-term. Do you have advice for how I might go about directly calling Rust code?

[Henrik Böving]

I've never done FFI with Rust in Lean but it seems pretty clear to me that you should be able to just let rust expose functions that conform to the C ABI and call them like you would any other C FFI function with lean_objects as parameters.

[Chase Norman]

@Henrik Böving This github repo goes to C first before Rust, so nothing out of the ordinary. Do you have a hypothesis for why the linking that works with lake exe ffi does not work with #eval in the Main.lean?

[Chase Norman]

Lakefile for reference:

import Lake
open System Lake DSL

package RustFFI

@[default_target]
lean_exe ffi where
  root := `Main

def ffiC := "ffi.c"
def ffiO := "ffi.o"

target importTarget (pkg : Package) : FilePath := do
  let oFile := pkg.oleanDir / ffiO
  let srcJob ← inputFile ffiC
  buildFileAfterDep oFile srcJob fun srcFile => do
    let flags := #["-I", (← getLeanIncludeDir).toString]
    compileO ffiC oFile srcFile flags

extern_lib libffi (pkg : Package) := do
  let name := nameToStaticLib "ffi"
  let job ← fetch <| pkg.target ``importTarget
  buildStaticLib (pkg.libDir / name) #[job]

extern_lib some_rust_lib (pkg : Package) := do
  proc { cmd := "cargo", args := #["build", "--release"], cwd := pkg.dir }
  let name := nameToStaticLib "some_rust_lib"
  let srcPath := pkg.dir / "target" / "release" / name
  IO.FS.createDirAll pkg.libDir
  let tgtPath := pkg.libDir / name
  IO.FS.writeBinFile tgtPath (← IO.FS.readBinFile srcPath)
  return (pure tgtPath)

[Arthur Paulino]

For a long-term solution I would personally avoid relying on the data format that Lean 4 chooses (like lean_obects as Henrik mentioned) to encode data because that might change.

Instead, I would write my data to arrays of bytes following my own protocol on the Lean side, then deserialize it in Rust (following my own protocol again).

[Chase Norman]

Using JSON right now. The files are getting pretty large. I just was concerned that the extra translation and piping was adding latency. Not to mention there are weird OS-specific things like special characters cannot be sent over stdin on Windows. And pipes get broken and terminated Lean processes don't terminate the external code

[Chase Norman]

But perhaps FFI is only worse as far as OS compatibility and stability goes.

[Arthur Paulino]

Can you exploit specific patterns on your data to shrink it? It's often the case with specific problem domains.

Gluing FFI code often becomes the most fragile point in the pipeline. I would spend extra time on the data format used

[Chase Norman]

I can definitely switch to custom serialization, but we are sending the entire goal state and all definitions/types recursively needed to express it. So basically we are serializing a decent percentage of the entire working memory of the Lean process.

[Chase Norman]

But if we can directly call, then we can do all sorts of cool things. We can envison systems where information is sent as it is required, intermediate feedback can be sent back from the rust, visualizations can show in the infoview, etc.

[Chase Norman]

So I was hoping FFI would be a qualitative change, not just a quantitative one.

[Arthur Paulino]

Are you sending the same partial data over and over or are you updating a state with diffs?

[Chase Norman]

Right now 1 tactic call is 1 terminal command is 1 json file. Are you suggesting that I have some kind of server set up, where I have a way to check if there is one currently running and if so send information to that server?

[Chase Norman]

But also ensuring that there are not multiple users at the same time

[Arthur Paulino]

There are multiple ways to tackle this. You need to find your bottlenecks and redundancies. But the general idea is correct: manage a state in Rust so you don't need to send the same data over and over. Have the Rust state be updated with patches. You can even use a proper database like DuckDB or Polars for this. This is my suggestion

[Arthur Paulino]

These ideas may or may not apply, depending on the data flow of your application. Either way, looking at a more efficient data format instead of using generic JSON seems to be worth it.

Also, you mentioned "file" a few times. I hope you're not writing things to your filesystem just to communicate with Rust. That would have a great potential to become a bottleneck

[Chase Norman]

While it happens to be the same data in practice, there is nothing stopping variables from changing definitions, changing names, being considered opaque, etc. How the problem is encoded is somewhat at the discretion of the serializer. I think it would take just as long to ensure that definitions and their hashes are all present on the Rust side as it would to send them over. And yes, it's done over stdio.

[Chase Norman]

https://github.com/abdoo8080/lean-cvc5/tree/main

cvc5 seems to have the same kind of situation, and they have FFI working

[Leni Aniva]

I use the FFI between Lean and Rust regularly. I wrote a tutorial here: https://leni.sh/post/240304-rust-call-lean/