ソケットをIO Handleでラップする

SCGIでリクエストを受け付けたいという文脈。
ファイル記述子から直接IO Handleを生成する方法がなさそう（？）だった。
leanprover/lean4:v4.27.0-rc1時点においては、ファイルポインタをlean_alloc_externalで包めば動いた。

/**
 * @&UInt32 -> IO Handle
 * sys/socket::accept - accept a new connection on a socket
 */
/*@
requires socket >= 0;
ensures \result != \null;
*/
LEAN_EXPORT lean_obj_res c_accept_socket (uint32_t socket) {
  int conn = accept(socket, NULL, NULL);
  if (conn < 0) {
    return lean_io_result_mk_error(
      lean_mk_io_user_error(lean_mk_string("accept failed"))
    );
  }

  FILE* fp = fdopen(conn, "r+");
  if (fp == NULL) {
    close(conn);
    return lean_io_result_mk_error(
      lean_mk_io_user_error(lean_mk_string(strerror(errno)))
    );
  }

  return lean_io_result_mk_ok(lean_alloc_external(NULL, fp));
}

/**
 * Handle -> IO Unit
 */
LEAN_EXPORT lean_obj_res c_close_socket (lean_obj_arg handle) {
  void* fp = lean_get_external_data(handle);
  fclose((FILE *)(fp));
  return lean_io_result_mk_ok(lean_box(0));
}

参考文献

https://github.com/leanprover/lean4/blob/6e711bf067a0d9dc6623996b4bd3757ac6c46886/src/runtime/io.cpp#L385
https://github.com/leanprover/lean4/blob/6e711bf067a0d9dc6623996b4bd3757ac6c46886/src/include/lean/lean.h#L1241