Lean Vulkan

Stream: general

[György Kurucz]

I just wanted to show off a project I have been working on, creating bindings for Vulkan to Lean: https://github.com/kuruczgy/lean-vulkan

Right now the project is mostly an exercise in pushing what can be done with the current lean FFI. The bindings are automatically generated from the Vulkan XML specification. (See the README for more details.)

It is an aim of the project to make the API easier to work with than the C API. Simplifications are made wherever possible, for example by using namespaces and automatically filling some values. For example this:

const char *extensions[] = {"VK_EXT_debug_utils"};
const char *validationLayers[] = {"VK_LAYER_KHRONOS_validation"};
VkInstanceCreateInfo instanceCreateInfo = {
  .sType = VK_STRUCTURE_TYPE_INSTANCE_CREATE_INFO,
  .enabledExtensionCount = 1,
  .ppEnabledExtensionNames = extensions,
  .enabledLayerCount = 1,
  .ppEnabledLayerNames = validationLayers,
};
VkInstance inst;
VkResult res = vkCreateInstance(&instanceCreateInfo, NULL, &inst);

turns into this in lean:

let (res, inst) ← Vk.createInstance {
  enabledExtensionNames := #["VK_EXT_debug_utils"]
  enabledLayerNames := #["VK_LAYER_KHRONOS_validation"],
}

Currently the project is capable of rendering a single triangle:
The "hello world" triangle

Rendering more complex stuff should be doable, but needs a little more work. (E.g. figuring out what would be the best way to construct vertex buffers in lean.)

[Geoffrey Irving]

Are you planning to compile lean code to shaders? It would be super cool if we could use this for semi-verified high-performance compute kernels as well.

[György Kurucz]

In theory it should be possible, compile Lean to LLVM then LLVM to SPIR-V. The hard part would be working out how to reference uniforms, samplers, and other special stuff like shader built-in variables.

[Geoffrey Irving]

Even if it only did Array a -> Array b map for simple structure types a, b, it could be very useful.

[Henrik Böving]

Geoffrey Irving said:

Even if it only did Array a -> Array b map for simple structure types a, b, it could be very useful.

Arrays in Lean contain boxed types so they can't really be used with SIMD operations (well I guess unless you have some funky pointer ops), the only unboxed array types that Lean has right now are ByteArrays and FloatArrays

[Joachim Breitner]

I would already be happy about a EDSL for shaders in Lean, using the type system to ensure that everything lines up. Would maybe be fun to port https://kaleidogen.nomeata.de/ (which dynamically generates shader code in the browser) from Haskell to Lean.

[Wojciech Nawrocki]

Henrik Böving said:

Geoffrey Irving said:

Even if it only did Array a -> Array b map for simple structure types a, b, it could be very useful.

Arrays in Lean contain boxed types so they can't really be used with SIMD operations (well I guess unless you have some funky pointer ops), the only unboxed array types that Lean has right now are ByteArrays and FloatArrays

Could we have @[implemented_by name platform] and box-less intrinsics?

[Henrik Böving]

Not really no, the value would still be treated as an Array a by the rest of the Lean world so if any other function apart from your special implemented_by ones try to access stuff you end up in trouble. That said it would be very cool if we could support unboxed integer and float values in Array in general.

[Wojciech Nawrocki]

The assumption would be on a given platform, you can only run @[implemented_by name platform], otherwise an unknown symbol error occurs (or the Lean code is run). Then with a runtime that also makes the right assumptions, there would be no rest of the Lean world that could break, I think.