Converting structures from lean4 to C

Stream: lean4

[z battleman]

Hi! I'm very new to development with the ffi and I'm sturggling a bit to get footing. From what I can tell, many projects leave their types abstract and define their functions as constants that have no Lean representation and interface with c. Ideally, I would like to write a library that has a Lean representation which allows one to do proofs.

I tried to do this basing essentially all of the code on this repository, with the idea to try and get a Vector in Lean of Fin m -> Float which has a backend in C given as a struct. As of right now, my Lean code looks like

structure mathVec (m : Nat) where
  data : Fin m -> Float

instance : Inhabited (mathVec m) where
  default : mathVec m := ⟨λ i => 0⟩

namespace mathVec

unsafe def externMk {m : Nat} : (Fin m -> Float) -> mathVec m
  := panic! "Can't actually do this"
attribute [implementedBy externMk] mathVec.mk

unsafe def externData : mathVec m -> (Fin m -> Float)
  := panic! "Can't actually do this"
attribute [implementedBy externData] mathVec.data

@[extern "mathVec_new"]
def new (x : Float) (m : Nat) : mathVec m
  := ⟨λ i => x⟩

@[extern "mathVec_get_val"]
def get {m : @&Nat} (v : @&mathVec m) (i : @&Fin m)
  := v.data i

and the underlying c is essentially the exact same as the repository from before with the allocations and whatnot changed accordingly. Here is a pastebin of it

This unsurprisingly doesn't immediately work out of the box becausee you never tell Lean how to take something of Fin m -> Float and turn it into the desired struct. However, after looking at a couple of projects on github, I haven't been able to figure out how to do this.

Thank you so much for any advice!

(As a bit of an additional question, even with abstract types, it seems like somehow the inputs to the Lean functions are automatically transformed into the C struct. I think it makes a bit more sense how this might work as the names are the same, and more importantly, they are of the same type in the same order, but I would be curious to know how this worked in more detail)

[Tomas Skrivan]

Generating C code with lean -c is very useful to figure out how to use lean objects. Create a function that takes a function f : Fin m -> Float and an index i : Fin m and returns f i:

@[export eval_fun]
def eval_fun {n : Nat} (f : Fin n → Float) (i : Fin n) : Float := f i

Run lean -c eval_fun.c eval_fun.lean and the generate .c file contains:

LEAN_EXPORT lean_object* eval_fun(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
lean_dec(x_1);
x_4 = lean_apply_1(x_2, x_3);
return x_4;
}

This shows that to evaluate an object of type Fin m -> Float, you should use lean_apply_1. Therefore the main loop to load the data on C level will look like this:

for(size_t i=0;i<m;i++){
  lean_inc(x_2);
  v->data[i] = lean_unbox_float(lean_apply_1(x_2, lean_usize_to_nat(i)));
}

[Tomas Skrivan]

How did I figure out lean_usize_to_nat? I just created another function

@[export mk_index]
def mk_index (n : Nat) (i : USize) (h : i.toNat < n) : Fin n := ⟨i.toNat, h⟩

Which generates this C code:

LEAN_EXPORT lean_object* mk_index(lean_object* x_1, size_t x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
lean_dec(x_1);
x_4 = lean_usize_to_nat(x_2);
return x_4;
}

You can see that Fin m and Nat have the same representation on C level.

[Tomas Skrivan]

By inspecting some code It looks like that lean_unbox_float does not consume its argument. Therefore the code should look like:

for(size_t i=0;i<m;i++){
  lean_inc(x_2);
  lean_object * val = lean_apply_1(x_2, lean_usize_to_nat(i));
  v->data[i] = lean_unbox_float(val);
  lean_dec(val);
}

I'm still unsure if I have the reference counting correct here, so someone more knowledgeable should comment on that.

[Henrik Böving]

Generating C code for written Lean code to check out what to do is pretty clever, I'll definitely keep that in mind!

[Tomas Skrivan]

Also you have incorrect declaration of the mathVec_get_val function.

You have

lean_obj_res mathVec_get_val(b_lean_obj_arg _v, uint32_t i)

But lean code:

structure mathVec (m : Nat) where
  data : Fin m -> Float

@[export mathVec_get_val]
def get {m : @&Nat} (v : @&mathVec m) (i : @&Fin m)
  := v.data i

generates

LEAN_EXPORT lean_object* mathVec_get_val(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
lean_dec(x_1);
x_4 = lean_apply_1(x_2, x_3);
return x_4;
}

Where x_1 is the {m : Nat}, x_2 is the (v : mathVec m) and x_3 is the (i : Fin m). As you can see, those declarations are very different, but they have to match!

Few notes:

- Every function accepting mathVec m will also accepts m as argument. It is usually implicit, i.e. with {}, but on C level it is always explicit. Therefore your C struct mathVec does not need to hold the array size.
- Already mentioned before, Fin m is the same as Nat on C level. It is not size_t or uint32_t. For those you need to use USize orUInt32

example:

@[export mathVec_get_val]
def get {m : @&Nat} (v : @&mathVec m) (i : UInt32)
  := v.data ⟨i.toNat,sorry⟩

generates

LEAN_EXPORT lean_object* mathVec_get_val(lean_object* x_1, lean_object* x_2, uint32_t x_3)

[Tomas Skrivan]

In my project, I really try to minimize the amount of hand written C code involving lean_object. To interface with lean, I mostly try to create lean functions accepting or returning Float, USize or UInt and tag them with export attribute to fix their corresponding C name. You really want to avoid messing with lean_ctor_... functions. To use them correctly you would need to know the exact memory layout.

Example of defining a three dimensional vector and accessing its components.

[Tomas Skrivan]

Ahh there are more things incorrect.

The mathVec_new returns data with lean_io_result_mk_ok(mathVec_boxer(v)) however this would mean the lean function new returns IO (mathVec m) but it returns only mathVec m.

[Tomas Skrivan]

Unfortunately, I do not have the time to make your code work right now. I strongly recommend to mess around with lean code , generate C code with lean -c and inspect it.

[Tomas Skrivan]

Also recommend having look at lean.h file. The link takes to C implementation of Array.get!

[z battleman]

oh wow this is so incredibly useful!! I will spend some time trying to understand this and update my code accordingly, and I'll report back!

[z battleman]

This makes so much sense! This thread should be immortalized for how helpful it was to understand what's actually going on here. I've got a bunch of small examples working now! The one thing that I'm a bit unclear about is how to go to and from c. The direction from Lean to C is not that hard, as you mention you can just iterate over the lean object and put that into the C struct. However, for the other direction, I'm not sure what to do. The example from before simply has box and unbox functions, but going from an arbitrary c struct, I'm not sure how to go about this. I wrote a simple function to turn a Lean Float array into a Vector (in the hopes that it would be easily copyable, but... not so much

LEAN_EXPORT lean_object* l_mathVec_fromList___elambda__1___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4;
x_3 = l_instInhabitedFloat;
x_4 = lean_array_get(x_3, x_1, x_2);
return x_4;
}
}
LEAN_EXPORT lean_object* l_mathVec_fromList___elambda__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_mathVec_fromList___elambda__1___rarg___boxed), 2, 0);
return x_2;
}
}
LEAN_EXPORT lean_object* mathVec_from_list(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
lean_dec(x_1);
x_3 = lean_alloc_closure((void*)(l_mathVec_fromList___elambda__1___rarg___boxed), 2, 1);
lean_closure_set(x_3, 0, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_mathVec_fromList___elambda__1___rarg___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_mathVec_fromList___elambda__1___rarg(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
LEAN_EXPORT lean_object* l_mathVec_fromList___elambda__1___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_mathVec_fromList___elambda__1(x_1);
lean_dec(x_1);
return x_2;
}

Can someone help me make sense of this and/or give me some tips on how to write a much simpler version to do what I want? It would be nice to have this so I could have functions that return Vectors. Thank you again so so much!

[z battleman]

At the suggestion of @James Gallicchio I'm going to put in a layer of abstraction between the Vector Fin m -> Float and c. This layer will represent the vectors as Float Arrays rather than functions which should hopefully make converting to C easier. That being said, just boxing it up doesn't seem to be working. How can I tell lean how to interpret a c struct and convert it into a Lean structure? Fortunately, the lean sturcture and the c struct look very similar - both contain a Float/Double array and an length as a Nat/uint32_t

I'm currently trying

lean_object* cVec_new(double val, lean_object* len_) {
    uint32_t len = lean_unbox_uint32(len_);
    printf("hereee");
    printf("len: %d", len);
    fflush(stdout);

    if (len == 0) {
        return make_error("invalid length");
    }

    cVec* v = cVec_alloc(sizeof(double)*len);
    if (!v) {
        return make_error("ERROR_INSUF_MEM");
    }
    for (size_t i = 0; i < len; i++) {
        v->data[i] = val;
    }
    printf("hereee2");
    fflush(stdout);
    lean_object* out = cVec_boxer(v);
    printf("reting");
    fflush(stdout);
    return out;
}

My guess is the proper way is to make a ctor with the array and the int, but that would require figuring out how to turn an array into a lean object. I'll keep looking!

Thanks!!

[Tomas Skrivan]

I didn't read your code yet but I would recommend to have a look at this example how to wrap C++ object into lean_external_object. https://github.com/leanprover/lean4/tree/66fcfcce3716774dacbd35e1ea0f5c75356df311/tests/compiler/foreign

[Yuri de Wit]

Henrik Böving said:

Generating C code for written Lean code to check out what to do is pretty clever, I'll definitely keep that in mind!

Indeed!

I also noticed that when using Lake, all the generated .c files are dumped into ./build/ir/..., making it quite easy to inspect.

[z battleman]

Progress has been made! I have the new array working! However, now I am having some issues with retrieving elements from it. The c code that lean generates for this function looks like:

LEAN_EXPORT lean_object* cVec_get_val(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_3 = lean_ctor_get(x_1, 0);
lean_inc(x_3);
lean_dec(x_1);
x_4 = l_instInhabitedFloat;
x_5 = lean_array_get(x_4, x_3, x_2);
lean_dec(x_2);
lean_dec(x_3);
return x_5;
}

and my c code I wrote by hand looks like

lean_object* cVec_get_val(lean_object* v_, lean_object* i_) {
    printf("here3");
    fflush(stdout);
    lean_object* lean_arr = lean_ctor_get(v_, 0);
    printf("length?: %u\n", lean_unbox_uint32(lean_ctor_get(v_, 1)));
    printf("index?: %u\n", lean_unbox_uint32(i_));
    lean_inc(lean_arr);
    lean_dec(v_);
    lean_object* out = lean_array_get(l_instInhabitedFloat, lean_arr, i_);
    lean_dec(i_);
    lean_dec(lean_arr);
    return out;
}

which as far as I can tell are the same. I really have no idea on this one, but I'll keep trying stuff until it hopefully works (or I realize I made a typo somewhere haha)

Edit: Curiously, if I copy the generated code exactly and replace my get function with it, it still doesn't work. And even stranger, the get function is returning correctly. So something is happening between when it retrives the lean object from the array and returns it, and when it prints it. (I verified this by unbox the lean object just before returning from the get function, and it works properly)

I found the problem! But I have no idea whatsoever how to fix it. My code cVec_get_val returns a lean_object*, but for whatever reason, in the Main.c file, it's trying to access it as if it were a double

static double _init_l_main___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; double x_3;
x_1 = l_main___closed__2;
x_2 = lean_unsigned_to_nat(2u);
x_3 = cVec_get_val(x_1, x_2);
return x_3;
}

Edit 2: Apparently if I just make my get function return a double it works! But then the question is why are there inconsistencies between the function signatures when the functions are and are not exported?