not as broken tun bindings for lean

bindings.cpp

#include <lean/lean.h>

#include <cstring>
#include <fcntl.h>
#include <linux/if.h>
#include <linux/if_tun.h>
#include <string>
#include <sys/ioctl.h>
#include <unistd.h>

#include <iostream>

using u8 = uint8_t;
using i64 = int64_t;

struct Tundev {
  std::string name;
  int fd;

  Tundev(const char *name) {
    int fd = open("/dev/net/tun", O_RDWR);
    if (fd < 0) {
      std::cerr << "A FATAL ERROR HAS OCCURED: opening /dev/net/tun failed\n";
      throw std::runtime_error("opening /dev/net/tun failed");
    }

    ifreq ifr;
    memset(&ifr, 0, sizeof(ifr));

    ifr.ifr_flags = IFF_TUN | IFF_NO_PI;
    if (name)
      strncpy(ifr.ifr_name, name, IFNAMSIZ);

    int err = ioctl(fd, TUNSETIFF, (void *)&ifr);
    if (err < 0) {
      std::cerr << "A FATAL ERROR HAS OCCURED: ioctl failed\n";
      throw std::runtime_error("ioctl failed");
    }

    this->name = ifr.ifr_name;
    this->fd = fd;
  }

  Tundev() : Tundev(nullptr) {}

  ~Tundev() { close(fd); }

  auto recv(u8 *data, size_t capacity) -> size_t {
    return read(fd, data, capacity);
  }

  auto send(const u8 *data, size_t size) -> void { write(fd, data, size); }
};

static void Tundev_finalize(void *tundev) {
  delete static_cast<Tundev *>(tundev);
}

static void Tundev_foreach(void *, b_lean_obj_arg) {
  // do nothing
}

static lean_external_class *g_Tundev_class = nullptr;

static lean_object *Tundev_to_lean(Tundev *tundev) {
  if (!g_Tundev_class) {
    g_Tundev_class =
        lean_register_external_class(Tundev_finalize, Tundev_foreach);
  }
  return lean_alloc_external(g_Tundev_class, tundev);
}

static Tundev *to_Tundev(lean_object *obj) {
  return static_cast<Tundev *>(lean_get_external_data(obj));
}

extern "C" LEAN_EXPORT lean_obj_res mk_Tundev(lean_obj_arg name,
                                              lean_obj_arg /* w */) {
  try {
    Tundev *dev;
    if (lean_obj_tag(name) == 0) {
      dev = new Tundev();
    } else {
      dev = new Tundev(lean_string_cstr(lean_ctor_get(name, 0)));
    }
    return lean_io_result_mk_ok(Tundev_to_lean(dev));
  } catch (std::runtime_error e) {
    return lean_io_result_mk_error(
        lean_mk_io_user_error(lean_mk_string(e.what())));
  }
}

extern "C" LEAN_EXPORT lean_obj_res Tundev_name(b_lean_obj_arg tundev) {
  return lean_mk_string(to_Tundev(tundev)->name.data());
}

extern "C" LEAN_EXPORT lean_obj_res Tundev_recv(b_lean_obj_arg obj,
                                                lean_obj_arg) {
  constexpr int CAPACITY = 1500;
  auto buffer = lean_mk_empty_byte_array(lean_int_to_int(CAPACITY));
  auto sz = to_Tundev(obj)->recv(lean_sarray_cptr(buffer), CAPACITY);
  lean_sarray_set_size(buffer, sz);
  return lean_io_result_mk_ok(buffer);
}

extern "C" LEAN_EXPORT lean_obj_res Tundev_recv_into(b_lean_obj_arg obj,
                                                     lean_obj_arg buffer_,
                                                     lean_obj_arg) {
  if (!lean_is_exclusive(buffer_))
    buffer_ = lean_copy_byte_array(buffer_);

  auto buffer = lean_to_sarray(buffer_);
  auto cap = buffer->m_capacity;

  auto sz = to_Tundev(obj)->recv(buffer->m_data, cap);
  lean_sarray_set_size(buffer_, sz);

  return lean_io_result_mk_ok(buffer_);
}

extern "C" LEAN_EXPORT lean_obj_res Tundev_send(b_lean_obj_arg obj,
                                                b_lean_obj_arg buf,
                                                lean_obj_arg) {
  to_Tundev(obj)->send(lean_sarray_cptr(buf), lean_sarray_size(buf));
  return lean_io_result_mk_ok(lean_box(0));
}

extern "C" LEAN_EXPORT lean_obj_res Tundev_refcnt(b_lean_obj_arg obj,
                                                  lean_obj_arg) {
  return lean_io_result_mk_ok(lean_int_to_int(obj->m_rc));
}

build.sh

#!/usr/bin/env bash

CFLAGS=(
  # -O3
  -Wl,-lstdc++
  -ggdb
)

g++ bindings.cpp -c -I/home/magnus/.elan/toolchains/stable/include -fPIC -fvisibility=hidden "${CFLAGS[@]}" -std=c++20
lean main.lean -c main.c
# leanc main.c -c "${CFLAGS[@]}"
# leanc main.o bindings.o -lstdc++ -Wl,-lstdc++
leanc main.c bindings.o "${CFLAGS[@]}"

main.lean

opaque TundevPointed : NonemptyType
def Tundev : Type := TundevPointed.type
instance : Nonempty Tundev := TundevPointed.property

@[extern "mk_Tundev"] opaque Tundev.mk (name : @& Option String := none) : IO Tundev
@[extern "Tundev_name"] opaque Tundev.name : @& Tundev -> String

@[extern "Tundev_recv"] opaque Tundev.recv : @& Tundev -> IO ByteArray
@[extern "Tundev_recv_into"] opaque Tundev.recvInto : @& Tundev -> ByteArray -> IO ByteArray
@[extern "Tundev_send"] opaque Tundev.send : @& Tundev -> @& ByteArray -> IO Unit

@[extern "Tundev_refcnt"] opaque Tundev.refcnt : @& Tundev -> IO Int

partial def forever [Monad m] (action : m Unit) : m Unit := do
  action
  forever action

partial def foreverA [Monad m] (initial : a) (action : a -> m a) : m Unit := do
  let x <- action initial
  foreverA x action

-- partial def foreverA [Monad m] (initial : a) (action : a -> m a) : m Unit := do
--   let actionM : StateT a m Unit := fun x => ((), .) <$> action x
--   _ <- StateT.run (s := initial) (forever actionM)

def main : IO Unit := do
  let dev <- Tundev.mk
  IO.println s!"Interface name: {dev.name}"

  let buf := ByteArray.mk (Array.mkArray 1500 0)

  foreverA buf $ fun buf => do
    let buf <- dev.recvInto (dbgTraceIfShared "a" buf)
    IO.println s!"Received: {buf}"
    dev.send buf -- Note: this is a stupid thing to do and achieves nothing
    pure buf