Monads in FFI

Stream: lean4

[Leni Aniva]

How can I tell the native function signature of a function that has generic/type arguments? e.g.

@[export generic_function]
def execCore {α} (context: Lean.Core.Context) (state: Lean.Core.State) (coreM: Lean.CoreM α):
    IO (α × Lean.Core.State) :=
  coreM.toIO context state

In the FFI documentation, it says that a type like the α above is either erased or represented as a dummy. How can I determine which case happened for this symbol?

[Leni Aniva]

An even simplier example:

abbrev M := ExceptT String IO

@[export exec_monad]
def exec_monad {α} (m: M α): IO α := do
  let a ← m
  IO.println "exec_monad"
  let b ← m
  match b with
  | .ok v => return v
  | .error e => throw <| IO.userError <| e
@[export example_monad]
def example_monad: M Nat := do
  IO.println "example_monad"
  return 5

@[export another_example_monad]
def another_example_monad (s: String): M Nat := do
  IO.println s
  return s.length

and calling it with

lean_obj_res exec_monad(lean_obj_arg m, lean_obj_arg world);
lean_obj_res example_monad;

{
  ...
  lean_obj_res result = exec_monad(example_monad, lean_io_mk_world());
}

leads to segmentation fault

[Tomas Skrivan]

If you put your file in ffi.lean and call lean ffi.lean -c ffi.c the output C file will contain

LEAN_EXPORT lean_object* exec_monad(lean_object*, lean_object*, lean_object*);
...
LEAN_EXPORT lean_object* exec_monad(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
...
}

You can see that exec_monad has three instead of two arguments and they correspond to {α}, (m: M α) and IO.RealWorld. I think you should call your function as exec_monad(nullptr, example_monad, lean_io_mk_world()). Type arguments are still present in the function signature but are ignored(as far I'm aware) so you can just pass nullptr.

[Leni Aniva]

Tomas Skrivan said:

If you put your file in ffi.lean and call lean ffi.lean -c ffi.c the output C file will contain

LEAN_EXPORT lean_object* exec_monad(lean_object*, lean_object*, lean_object*);
...
LEAN_EXPORT lean_object* exec_monad(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
...
}

You can see that exec_monad has three instead of two arguments and they correspond to {α}, (m: M α) and IO.RealWorld. I think you should call your function as exec_monad(nullptr, example_monad, lean_io_mk_world()). Type arguments are still present in the function signature but are ignored(as far I'm aware) so you can just pass nullptr.

If I write it as

lean_obj_res result = exec_monad(NULL, example_monad(lean_io_mk_world()), lean_io_mk_world());

it segfaults in lean_apply_1

#0  0x00007fffea23d378 in ?? ()
#1  0x00007ffff79084a6 in lean_apply_1 () from /nix/store/092a3afjqb2kg62iqy7wzs8mi6g10bv9-lean-stage1/lib/lean/libleanshared.so
#2  0x00007ffff7fbe444 in exec_monad () from /nix/store/62bnbaf22qykwa5vxnjj4zvyhhl72kir-libCallee-dynlib/libCallee.so

I suspect this has something to do with the extra argument generated on example_monad

[Leni Aniva]

my hypothesis is that the execCore function is not needed at all, and if there is a function of type Lean.CoreM _, its signature will be

lean_obj_res some_moand(..., lean_obj_arg context, lean_obj_arg state, lean_obj_arg world);

[Leni Aniva]

However, if I have

@[export init_search]
unsafe def initSearch: IO Unit := do
  Lean.enableInitializersExecution
  Lean.initSearchPath (← Lean.findSysroot)

@[export create_core_context]
def createCoreContext: IO Lean.Core.Context := do
  return {
    currNamespace := Lean.Name.str .anonymous "Test"
    openDecls := [],     -- No 'open' directives needed
    fileName := "<Filename>",
    fileMap := { source := "", positions := #[0], lines := #[1] },
    options := Lean.Options.empty,
  }

@[export create_core_state]
def createCoreState: IO Lean.Core.State := do
  let env ← Lean.importModules
    (imports := #["Init".toName])
    (opts := {})
    (trustLevel := 1)
  return { env := env }
@[export exec_core]
def execCore {α} (context: Lean.Core.Context) (state: Lean.Core.State) (coreM: Lean.CoreM α):
    IO (α × Lean.Core.State) :=
  coreM.toIO context state


@[export core_catalog]
def core_catalog: Lean.CoreM Unit := do
  let env ← Lean.MonadEnv.getEnv
  let names := env.constants.fold (init := "") (λ acc name _ => acc ++ name.toString)
  IO.println names

and I call the functions

lean_obj_res unbox_io(lean_obj_arg obj) {
  b_lean_obj_res ok = lean_inc(lean_io_result_get_value(obj));
  lean_dec(obj);
  return ok;
}
...
    lean_obj_res res = unbox_io(init_search(lean_io_mk_world()));
    lean_dec(res);
    lean_obj_res context = unbox_io(create_core_context(lean_io_mk_world());
    lean_obj_res state = unbox_io(create_core_state(lean_io_mk_world());
    lean_obj_res res = core_catalog(context, state, lean_io_mk_world());
    lean_dec(res);

[Leni Aniva]

this again results in a segfault in the fold function inside core_catalog:

Program received signal SIGSEGV, Segmentation fault.
0x00007ffff7fbd8b1 in l_Lean_SMap_fold___at_core__catalog___spec__1___rarg () from /nix/store/ngnmajqx2pnshf8dx8rvqv65xx5ry4wd-libCallee-dynlib/libCallee.so
(gdb) bt
#0  0x00007ffff7fbd8b1 in l_Lean_SMap_fold___at_core__catalog___spec__1___rarg () from /nix/store/ngnmajqx2pnshf8dx8rvqv65xx5ry4wd-libCallee-dynlib/libCallee.so
#1  0x00007ffff7fbdcb4 in core_catalog () from /nix/store/ngnmajqx2pnshf8dx8rvqv65xx5ry4wd-libCallee-dynlib/libCallee.so

[Sebastian Ullrich]

You really should avoid using complex types like elaboration monads in FFI because it is way too easy to get wrong. There's a reason Lean itself avoids it.

[Leni Aniva]

Sebastian Ullrich said:

You really should avoid using complex types like elaboration monads in FFI because it is way too easy to get wrong. There's a reason Lean itself avoids it.

is it ok to just use CoreM? I want to invoke tactics via the FFI

[Leni Aniva]

I found that the solution is to turn the state argument into a reference via lean_st_mk_ref.