making vale extensible

[divinusdracodominus]

the use of an extern or language personality notation to declare or implement a function as the syscall equivalent to linux mmap for the purposes of making edge platforms supportable, potentially also having such denotation for mprotect. This will help minimize the work we need to do, as well as allow vale to compete with languages like rust and python in places such as embedded without the need to maintain a bloated environment, this approach encourages modularity and if done using externs fits within vales notion of platform independence. This approach can also be used in for example JVM to support creation of an array as the memory buffer used by vale, but this is optional. knowing the potential issues with this (such as safety) this function will be implemented by the vale team for major platforms including JVM, CLR, linux, mac, windows, redox, WASM, and JS. fundamentally this is no different from using externs or builtins which is already the case in Midas, and thus I don't understand the issue with safety concerning this issue. since we are implementing for major platforms safety is maintained will still allowing extensibility, and in accordance with the argument deploy in discord, supposing that a platform becomes mainstream, or grows in popularity as a build target, then the vale team will ensure the safety of the extern or syscall used to allocate memory by HGM, resilient, and arena. (and any other regions supported as part of Midas), contrary to the purposed approach of forking Midas, this approach allows rapid reimplementation, and encourages safety through the use of existing tested Midas code, rather then forcing the reimplementation of a region that could cause potentially extensive compromise to the safety and performance that people should come to expect from vale.

[Verdagon]

Just to be super clear: are you proposing we make it so the user can provide a C implementation for our regions' (HGM, arena, type-pool, etc) calls to mmap?

This would allow the user to provide an untrustworthy chunk of memory (which could be deleted or modified by someone other than the compiler), so it would degrade Vale's safety guarantees. Vale's strength is in knowing that, no matter whose code you depend on, your Vale code will never trigger memory unsafety. If someone publishes a library that defines an extern mmap, and someone accidentally indirectly depends on it, their memory safety could be at risk.

Is there a way to do this without risking people publishing packages that could trigger memory unsafety in Vale code that depends on them?

[divinusdracodominus]

yeah they would only be able to do it for target triples for which the extern doesn't already exist, but also the OS could always do this, or the user could relink against an alternative version of libc with an invalid malloc, so you can never really be sure it isn't happening

[Verdagon]

I sure hope there's no way for a fountain module to re-link against a different version of libc with an invalid malloc. Is there a way we can avoid that?

Even on platforms we don't yet support, I'm nervous about someone accidentally depending on a module that breaks memory safety for their vale code.

[khaledh]

I'm interested in this discussion from the point of view of developing for a freestanding environment, e.g. hobby kernels/OSs, embedded, etc. I currently have a hobby kernel implementation in Nim, where I just need to provide several C lib functions, namely malloc/free (and friends), memcpy/set/cmp, and strlen/strstr. I was wondering what it would take to support this in Vale.