Making extraction to Krml extensible; towards a separate repo for Steel?

Starting point: SteelC, a Steel model for C data types

Cf. https://github.com/FStarLang/FStar/pull/2349

Building on John Li’s 2021 internship at MSR, I now have a C model of Steel covering arbitrary nestings of structs, arrays and unions, with pointers to fields, and support for recursive data structures such as linked lists. This extracts to C with Karamel.

However, CI on this PR takes 55 minutes (as opposed to 25 minutes on master), mainly due to verifying the SteelC model. Thus, we are investigating whether to move SteelC (and maybe more) to a separate repository. If we were to do so, it wouldn’t be palatable to keep in F* FStar.Extraction.Krml the names of functions that have moved outside of F*. Thus, we need to make extraction to Krml extensible.

Making FStar.Extraction.Krml extensible

There are 3 functions piloting extraction to Karamel: translate_type, translate_expr, and translate_decl (to which one should add a new function, translate_type_without_decay, introduced by John Li to support extraction of known-length array types when inlined as struct/union fields)

In FStar.Extraction.Krml:

1. For each of those functions (say translate_type here), I created a reference of the corresponding function type (ref_translate_type), with an always failing function as initial value.

2. Then, I rename the old function (to translate_type’) and I redefine the function as evaluating the function contained in the corresponding reference.

3. Then, I introduce an initializer to append the old function (translate_type’) to the reference (ref_translate_type). This initializer is run once when fstar.exe starts.

4. Then, I introduce a function (register_pre_translate_type) for a client to prepend their custom function f on top of the current value f’ of the reference (ref_translate_type), so when the function (translate_type) is called when extracting some F* code to Krml, f is called first, and if it fails, then f’ is called.

Building and using an extraction extension

Based on that, I build a client for SteelC (in examples/steel/arraystructs/my_fstar) to register translation functions for SteelC types and operations. I define a module, ExtractSteelC, which friends FStar.Extraction.Krml and verifies and extracts to OCaml against the F* sources. In this module, I define custom translation functions for SteelC constructs and I define a let _ initializer to register them with the register_pre_* functions I created in FStar.Extraction.Krml.

Initially, from this module, I built a custom fstar.exe statically linked with the rest of F* (à la ocamlmktop.) But I was not happy with that solution.

So, based on suggestions by Guido and Nik, I now build a library, steel_c, which I can dynamically load as a plugin with fstar.exe --include examples/steel/arraystructs/my_fstar/lib/steel_c --load ExtractSteelC when extracting F* code using SteelC.

Next steps: towards a separate repository for Steel?

With this experiment, we have discussed the opportunity to move SteelC, or even Steel, to a separate repository, moving both the Steel tactic and the Steel and SteelC extraction rules to a library that can be both dynamically loaded as a plugin, or statically loaded into a new fstar.exe.

This gives rise to the possibility of building a binary distribution of Steel (and SteelC) for those users of F* who do not have OCaml and/or do not want to build F* from the sources (or via opam.) In practice, we could provide two binary distributions of F*, one without Steel, and one with Steel, for size reasons.

Moving Steel into a separate repository would also satisfy those users of F* who do not use Steel but need to build F* from its sources (or via opam) and complain about verification time for ulib when building F*. Moving Steel into a separate repository is consistent with the fact that Steel has long been labeled experimental anyway. With F* extraction to Krml extensible, changes to a separate Steel repository would no longer be marred by delays incurred by reviewing pull requests on the F* repository.

Then, we should open the discussion of how to distribute F* packages (as suggested by Lucas Franceschino.) One immediate possibility could be to leverage opam, with a fstar package without Steel, and a separate steel package depending on fstar and building Steel and SteelC as a dynamically loadable plugin.