Zulip Chat Archive

Stream: general

Topic: FFI - representing C structs in Lean

Greg Shuflin (Dec 18 2025 at 02:10):

I'm currently hacking on this SDL3 bindings library (https://github.com/ValorZard/lean-sdl3) that @Oliver Dressler and @Srayan Jana have contributed to, trying to understand how it works and expand its functionality. At the moment, I'm trying to get the SDL3 webcam bindings working.

I'm specifically trying to figure out how to best represent C SDL structures as types in Lean. I can see that the existing bindings are doing something like:

private opaque SDLWindow.nonemptyType : NonemptyType
def SDLWindow : Type := SDLWindow.nonemptyType.type
instance SDLWindow.instNonempty : Nonempty SDLWindow := SDLWindow.nonemptyType.property

to create a Lean equivalent of a SDL_Window structure. But I'm not sure how to create a Lean structure that has fields equivalent to a C structure, and I don't see any examples of this in these existing bindings. I specifically want to be able to represent a SDL_CameraSpec in Lean as a Lean structure and get access to the various C integer fields on it.

Mac Malone (Dec 18 2025 at 02:39):

If you want the C structure to also appear in the formalization, below is a brief example of how that could be done. In the example, SDL types are represented by Lean external objects with the assumption that the proper external classes are registered in the C code (e.g., g_pixelformat_external_class).

In general, I should probably explain the example a bit more, but I do not have the time at the present.

Example Code

Greg Shuflin (Dec 18 2025 at 10:51):

Mac Malone said:

If you want the C structure to also appear in the formalization, below is a brief example of how that could be done. In the example, SDL types are represented by Lean external objects with the assumption that the proper external classes are registered in the C code (e.g., g_pixelformat_external_class).

In general, I should probably explain the example a bit more, but I do not have the time at the present.

Example Code


yeah I think I need a bit more explanation to make sense of this, either that or this block of code as such doesn't work and I need to modify it some.

Greg Shuflin (Dec 24 2025 at 01:21):

In particular, I'm not sure what you were getting at with 

structure CameraSpec where
  private ofModel ::
    private toModel : CameraSpec.Model

I think this is just not syntactically correct? @Mac Malone

Mac Malone (Dec 24 2025 at 01:44):

The code should elaborate without errors. Viewing it on live.lean-lang.org shows no errors.

To elaborate a bit on the example:

  • PixelFormat and Colorspace are like SDLWindow. They are essentially opaque types with the added property that they are know to be Nonempty. This property allows them to be safely used in the return types of opaque defintions.
  • CameraSpec.Model is Lean formalization (model) of the SDL_CameraSpec data structure. It is not meant to actually be used in compiled code, but rather enable Lean proofs about the CameraSpec type.
  • CameraSpec wraps the CameraSpec.Model into a FFI type amendable to compiled code. Like PixelFormat or Colorspace, this is the type one is meant to use in FFI definitions and should be represented at compile time through an actual SDL_CameraSpec wrapped in a Lean object via lean_alloc_external(). The constructor ofModel and the field toModel are marked private because they are not meant to be used in compiled code. They simply exist to further enable formalization of CameraSpec's definitions.
  • CameraSpec.format and CameraSpec.width are example FFI definitions that have both a Lean formalization leveraging toModel and FFI implementation using the C data structure. This enables both proofs about and compiled uses of these fields.

It was not (and is not) entirely clear to me if a Lean formalization of the C data structure was what you were looking for when you asked for "a Lean structure that has fields equivalent to a C structure". An alternative version of the example with an opaque CameraSpec would look like the following:

Opaque CameraSpec

Greg Shuflin (Dec 24 2025 at 02:37):

@Mac Malone ah, I was confused by the :: syntax for the constructor, I see where that is documented now.

To step back a bit, I'm generally interested in using Lean for software development, and in particular right now I'm trying to translate a C program that uses the SDL3 library into Lean, adding FFI bindings as I find I need them. In my C code, I call https://wiki.libsdl.org/SDL3/SDL_GetCameraFormat which fills in a SDL_CameraSpec pointer argument; I'm trying to translate this to a lean function SDL.getCameraFormat : @& SDLCamera -> SDLIO CameraSpec, mimicking the C function signature. This means that I need to define the CameraSpec type in Lean, and since this is the lean equivalent of a semantically-meaningful C structure, it would be nice if I could access fields of the lean structure CameraSpec that are equivalent to the fields on the C SDL_CameraSpec struct.

It looks like the approach you're suggesting is to manually define a CType.Modelstructure that I manually define the (lean) fields of to exactly correspond to the C struct's fields, and then define CType itself as a structure that has exactly one field to contain a CType.Model. Then, for every field access I care about, I need to write a C function with the signature lean_obj_res <funcname>(b_lean_obj), which is bound to a Lean function with the name of the field and the signature @& CType -> <field_type>. The C function casts b_lean_obj_arg as the C type (here, SDL_CameraSpec*), extracts the field, and packages it as a lean_obj_res.

This is what is going on in your example:

@[extern "sdl_camera_spec_format"]
def format (spec : @& CameraSpec) : PixelFormat :=
  spec.toModel.format
/-

extern "C" LEAN_EXPORT lean_obj_res sdl_camera_spec_format(b_lean_obj_arg spec) {
  SDL_PixelFormat format = static_cast<SDL_CameraSpec*>(lean_get_external_data(spec))->format;
  return lean_alloc_external(g_pixelformat_external_class, format);
}

-/

What I'm still confused about is:
1) how does it make sense to define the body of format in Lean, if that function is decorated with @[extern <c_function>], which I thought would provide the definition of the Lean function purely in C.
2) As a matter of style, should people writing Lean bindings to C libraries prefer to map every C type that someone would want to interact with in Lean to an opaque Lean type, or use this CType.Model approach where the CType.Model fields are defined in Lean to be analogous to the C struct's fields (but still using C code to actually do the field access)?

Even though I'm still trying to get my head around this FFI code, I can tell that this is quite boilerplate-y to write. In the Rust ecosystem there are libraries like bindgen to automate some of this, and I wonder if anyone has been working on a Lean equivalent.

Mac Malone (Dec 24 2025 at 02:48):

Greg Shuflin said:

What I'm still confused about is:
1) how does it make sense to define the body of format in Lean, if that function is decorated with @[extern <c_function>], which I thought would provide the definition of the Lean function purely in C.
2) As a matter of style, should people writing Lean bindings to C libraries prefer to map every C type that someone would want to interact with in Lean to an opaque Lean type, or use this CType.Model approach where the CType.Model fields are defined in Lean to be analogous to the C struct's fields (but still using C code to actually do the field access)?

An opaque definition in Lean has essentially no formally defined behavior. As a result, very little can be proved about it. Providing a Lean model for a definition alleviates this and allows neaningful reasoning about the code in Lean. However, this is contigent on parity between the Lean model and the FFI implementation. If the definitions don't match, then the proofs are meaningless. For example:

Model/FFI Mismatch Example

Mac Malone (Dec 24 2025 at 02:50):

Greg Shuflin said:

Even though I'm still trying to get my head around this FFI code, I can tell that this is quite boilerplate-y to write. In the Rust ecosystem there are libraries like bindgen to automate some of this, and I wonder if anyone has been working on a Lean equivalent.

Yes, the code is unfortunately very boilerplate. There are some user libraries that attempt to ease this burden in various ways, but I don't think any really mature solution exists in the ecosystem yet.

Greg Shuflin (Dec 24 2025 at 03:53):

Mac Malone said:

An opaque definition in Lean has essentially no formally defined behavior. As a result, very little can be proved about it. Providing a Lean model for a definition alleviates this and allows neaningful reasoning about the code in Lean. However, this is contigent on parity between the Lean model and the FFI implementation. If the definitions don't match, then the proofs are meaningless. For example:

Model/FFI Mismatch Example


Ok so I guess the implication of this example is that it's possible to put the @[extern] attribute on any definition, and even if that definition has some lean code in it that the lean elaborator will use, at runtime the C code will be executed and the lean code will be completely ignored. So it's up to the programmer to make sure that the semantics of any C code in an extern function match any lean code in it (and also that extern directives are a place where Lean's correctness guarantees might fail)

This would be a handy thing to mention explicitly in https://lean-lang.org/doc/reference/latest/Run-Time-Code/Foreign-Function-Interface/#Lean___Parser___Attr___extern

Greg Shuflin (Dec 24 2025 at 06:25):

huh I just discovered I had this document open in a tab: https://gist.github.com/ydewit/7ab62be1bd0fea5bd53b48d23914dd6b from @Yuri , which perhaps also sheds some light on these questions

Srayan Jana (Dec 24 2025 at 09:11):

Oh hello @Greg Shuflin I’m glad to see my library has been useful in some way haha

Greg Shuflin (Dec 24 2025 at 09:12):

Srayan Jana said:

Oh hello Greg Shuflin I’m glad to see my library has been useful in some way haha

yeah it's definitely a good start towards making lean4 capable of doing graphical programming, which is a thing I personally (quixotically?) care about :slight_smile: plus a good onramp towards learning how lean4 ffi works

Srayan Jana (Dec 24 2025 at 09:12):

I wonder if a way to do bindgen for C in Lean would be to end up writing a full formal definition of the C99 spec in Lean

Srayan Jana (Dec 24 2025 at 09:13):

Also the main reason I stopped working in Lean FFI stuff is I found the experience on windows to be particularly painful with MSYS2 clang and whatnot

Greg Shuflin (Dec 24 2025 at 09:13):

it hasn't been too bad in linux

Greg Shuflin (Dec 24 2025 at 09:13):

actually, I have a question right this second

Srayan Jana (Dec 24 2025 at 09:14):

Yeah you need to be careful when redistrubbng games with this, since not all the libraries will be linked properly

Greg Shuflin (Dec 24 2025 at 09:15):

Srayan Jana said:

Yeah you need to be careful when redistrubbng games with this, since not all the libraries will be linked properly

I installed lean via nix and that caused some linking issues, although I'm currently working around them

Greg Shuflin (Dec 24 2025 at 09:15):

anyway, here's my fork: https://code.everydayimshuflin.com/greg/lean-sdl3

Srayan Jana (Dec 24 2025 at 09:15):

https://github.com/BRonen/sqlite-lean

Srayan Jana (Dec 24 2025 at 09:16):

This readme has the most up to date research I have on lean and C ffi stuff

Srayan Jana (Dec 24 2025 at 09:16):

Also you are going to want to join the SDL discord

Greg Shuflin (Dec 24 2025 at 09:16):

and in particular I'm owrking on adding SDL_CreateTexture. you only had SDL_CreateTextureFromSurface. the commit is https://code.everydayimshuflin.com/greg/lean-sdl3/commit/d1479f9db45b72c7188e4e2322871e12f0f5cbbc

Srayan Jana (Dec 24 2025 at 09:16):

https://discord.gg/sdl-enthusiasts-405784877305298944

Greg Shuflin (Dec 24 2025 at 09:16):

yeah I"m a beginner to sdl too

Srayan Jana (Dec 24 2025 at 09:17):

Something I really wanted to do before losing motivation was adding SDL GPU supporg

Srayan Jana (Dec 24 2025 at 09:18):

https://github.com/TheSpydog/SDL_gpu_examples
I wanted to port all of these to Lean at some poknf

Greg Shuflin (Dec 24 2025 at 09:20):

anyway, I basically need to be able to get the SDL_PixelFormat out of the https://wiki.libsdl.org/SDL3/SDL_Surface struct, which I think you represented as an opaque type

Srayan Jana (Dec 24 2025 at 09:21):

Yeah to be honest I was mostly copying and pasting a lot of stuff since I didn’t fully understand how the C FFI works, it’s mostly undocumented

Srayan Jana (Dec 24 2025 at 09:22):

I DMed @Mac Malone a lot to ask for questions

Greg Shuflin (Dec 24 2025 at 09:24):

certainly it would be good if important details about the FFI could make it into public documentation, rather than having to ask a specific person

Srayan Jana (Dec 24 2025 at 09:24):

Yeah that’s why I tried to write down everything I know on GitHub and in Zulip

Srayan Jana (Dec 24 2025 at 09:25):

There was also this GitHub repository that was super helpfil

Greg Shuflin (Dec 24 2025 at 09:25):

do you ahve notes somewhere I can search for?

Srayan Jana (Dec 24 2025 at 09:25):

https://github.com/DSLstandard/Lean4-FFI-Programming-Tutorial-GLFW

Greg Shuflin (Dec 24 2025 at 09:26):

heh he says that https://gist.github.com/ydewit/7ab62be1bd0fea5bd53b48d23914dd6b supercedes his own, which I already found

Srayan Jana (Dec 24 2025 at 09:26):

https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Making.20SDL3.20bindings.20for.20Lean.204/with/541774356

Srayan Jana (Dec 24 2025 at 09:27):

https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/SQLite.20bindings.20for.20Lean/

Srayan Jana (Dec 24 2025 at 09:27):

These two threads should contain most of my notes, but I’m pretty sure if you search my username up you can find more

Srayan Jana (Dec 24 2025 at 09:29):

Unfortunately it seems that C FFI for lean is a pretty low priority for the Lean Team, there are a couple of issues I made on GitHub about it that are on the back butnwr

Greg Shuflin (Dec 24 2025 at 09:29):

understandable, it's not really the core use case

Srayan Jana (Dec 24 2025 at 09:29):

The really big one is that the clang that Lean ships with is really weird, it strips out most of the standard library

Srayan Jana (Dec 24 2025 at 09:29):

So you can’t actually compile most C code with it, like sqlite

Srayan Jana (Dec 24 2025 at 09:30):

You have to download an external clang to compile and then link it

Greg Shuflin (Dec 24 2025 at 09:31):

honestly I'm more interested in getting rust FFI working reliably. I think at some point I might want to see if I can use the rust bindings to sdl as the thing that gets linked into lean, and put C code at an even further remove

Srayan Jana (Dec 24 2025 at 09:32):

That does not sound fun lol, good luck

Yuri (Dec 27 2025 at 20:37):

Greg Shuflin said:

huh I just discovered I had this document open in a tab: https://gist.github.com/ydewit/7ab62be1bd0fea5bd53b48d23914dd6b from Yuri , which perhaps also sheds some light on these questions

@Greg Shuflin, FYI, this document needs some revision due to a few FFI changes in Lean.

Greg Shuflin (Dec 28 2025 at 00:06):

@Yuri do you know what changes offhand? also, it would probably be good if as much of this FFI information could live in the official lean FFI documentation

Yuri (Dec 29 2025 at 00:44):

Greg Shuflin said:

Yuri do you know what changes offhand? also, it would probably be good if as much of this FFI information could live in the official lean FFI documentation

I’m on vacation and without my notebook, so I am of no help at this moment. I do know that we now have more primitive types and a couple (?) of small changes to some structure representation.

It seems to me that we need a core subset of C data types plus some types to provide a type safe representation for pointers, etc with some support for them directly in the code generator.

In addition, a bindgen (roughly following what rust does) tool to auto generate Lean and C bindins based on existing C headers. With the blessed C subset we could reduce more of the C boilerplate and write them (and reuse them) in Lean.

I do have an initial impl for this bindgen tool that at this point uses clang API to parse headers (that is where I learned most of what I know so far). Once I’m back, I will try to clean it up and share it here, if useful.

Yuri (Dec 29 2025 at 00:56):

But that says nothing about a transparent C representation for structs. Maybe this subset of C could allow us to write this getter/setters for structures in Lean (and automate that)?

Greg Shuflin (Dec 29 2025 at 00:58):

Yuri said:

Greg Shuflin said:

Yuri do you know what changes offhand? also, it would probably be good if as much of this FFI information could live in the official lean FFI documentation

I’m on vacation and without my notebook, so I am of no help at this moment. I do know that we now have more primitive types and a couple (?) of small changes to some structure representation.

It seems to me that we need a core subset of C data types plus some types to provide a type safe representation for pointers, etc with some support for them directly in the code generator.

Something that I've been wondering about based on the SDL3 code is, what's the best way to work with a C void* arbitrary handle to something in Lean? I found myself bascially declaring an arbitrary opaque type that represents one particular use of a void* in SDL3 C code (e.g. a pixel buffer) - so effectively adding a bit more type safety to the C bindings based on my human knowledge of how some C struct member would probably be used.

Another thing that's come to mind is C enums - the existing bindings were simply exposing (some) SDL3 C enums as UInt32 and implementing lean functions that expect a UInt32 argument. This works well enough, but it should be possible to translate a C enum into a Lean inductive type and map back the Lean representation to a C integer where it's being used in the underlying C functions.

In addition, a bindgen (roughly following what rust does) tool to auto generate Lean and C bindins based on existing C headers. With the blessed C subset we could reduce more of the C boilerplate and write them (and reuse them) in Lean.

I do have an initial impl for this bindgen tool that at this point uses clang API to parse headers (that is where I learned most of what I know so far). Once I’m back, I will try to clean it up and share it here, if useful.

I would be very interested in seeing this code when you have a chance to make it publishable.

Srayan Jana (Dec 29 2025 at 23:42):

@Greg Shuflin you might be interested in this one issue i raised on github: https://github.com/leanprover/lean4/issues/10561

Greg Shuflin (Jan 14 2026 at 04:04):

@Yuri have you had a chance to clean up the bindgen tool proof-of-concept you were talking about?

Last updated: Feb 28 2026 at 14:05 UTC