Automate wrappers around stubs

[N1ark]

Taking inspiration from how we handle intrinsics, I have created a new mechanism, to define wrappers for arbitrary stubs! All stubs in builtins are now defined through this mechanism.

How?

The entry point to all of this is the stubs.json file, in builtins/. This JSON is a dict, mapping category names (e.g. Optim, Fixme,Tokio`) to lists of patterns to match.

The stubs.py --stubs script (previously intrinsics.py) will then generate, for each category, a folder in builtins containing:

• intf.ml: a module defining the interface for all stubs. we try looking through Rust's stdlib to find the matching function, and if none is found a generic args:rust_val list -> rust_val ret signature is used.

• impl.ml: the hand-written implementation for the stubs, which must export a M functor to create a module matching the interface in intf.ml

• <category>.ml: hides both intf and impl, and instead exposes:

  • a fn type for each stub
  • a fn_pats list of patterns to match items
  • a eval_stub function that given a fn returns the right symbolic process

  this means we have basically the same thing as before but much more modular, and most of it is generated making adding new stubs hopefully easier

I've migrated all stubs to this system. Because AeneasVerif/charon#1088 got merged, I also managed to cleanly split out how we handle intrinsics, externs, and regular stubs: the resulting eval.ml file is incredibly small and simple which I'm very happy about, compared to before.

Extras

Additional fields that can be used for categories:

• dependencies (list of toml entries) if a category needs some dependency for its patterns (e.g. tokio)
• code (self-contained Rust code) useful for when Charon fails to find the item from its pattern
• features if a category needs some features enabled (e.g. f16, f128)

Additional fields that can be used for patterns:

• extra_args if a stub needs extra information (e.g. the signature of the function). valid values are sig for the function's signature, types for the function's type arguments, and fun_exec for the OCaml function to execute ULLBC functions
• include if a stub needs some other item to be resolved first (e.g. nested functions)
• alias if a stub is not found by Charon but may be re-exposed under a different name (this is risky to use, as it will expect the alias's signature for this pattern. use sparingly)

[giltho]

This looks so so cool! I'll do a proper review at some point

I'm going to be annoyingly pedantic here but you're writing json and then parsing text in the text fields to get additional structure and it's killing me 🙃
Instead of

"std::env::_var with sig"

Can we have

{
   "name": "std::env::_var with sig",
   "additional_args": [ "sig" ]
 }

(just a string should resolve to { "name": "the_string", "additional_args": [] })

And then, small cherry on top, because it's free to do with AI, can you add a stubs.schema.json so that we don't make mistakes writing it (it's checked automatically by vscode/zed). You'd also need to add a "$schema": "./stubs.schema.json" to stubs.json.
Schema is a bit over-engineered, but at least let's not re-parse strings 😭

[N1ark]

alrightttt you are right and i thought of it i just found the with sig thing cute .....

[giltho]

LGTM.
The only comment I want to make is that this lacks documentation.
We need explanation somewhere, possibly in CONTRIBUTING.md? But we need a tutorial on adding support for an intrinsic.

One slightly unclear thing to me is why is there two different procedure to generate stubs for external things and stubs for intrinsics?

[N1ark]

The only comment I want to make is that this lacks documentation. We need explanation somewhere, possibly in CONTRIBUTING.md? But we need a tutorial on adding support for an intrinsic.

Yeah sure I can add that in contributing, but like none of soteria rust is publicly documented so idk it feels weird?

One slightly unclear thing to me is why is there two different procedure to generate stubs for external things and stubs for intrinsics?

Because intrinsics are all in one place and you want to stub them all, so you dont need to do anything fancy you just parse them as-is. Same with externs, but which live in a separate world, and which dont have a signature defined, so you need to do it manually.

Stubs (e.g. the tokio or std stubs) are for function that exist and have a buddy but we choose to stub, so we want to allow for selecting exactly what we do; we can be a lot coarser with intrinsics.

i dont know if this answers the question or you meant something else :P

[giltho]

Yeah sure I can add that in contributing, but like none of soteria rust is publicly documented so idk it feels weird?

Agreed, though most of the code can be navigated through OCaml "go to reference", except this part because it's meta-programmed

[N1ark]

Yeah sure I can add that in contributing, but like none of soteria rust is publicly documented so idk it feels weird?

Agreed, though most of the code can be navigated through OCaml "go to reference", except this part because it's meta-programmed

then how about documented the builtins/eval.ml module with all the info for when the soteria rust doc is more refined