Specify functions that must extract?

[mtzguido]

This is more of a question really. A snippet like

open FStar.Seq

module U32 = FStar.UInt32

[@@Comment "test"]
let f (x:U32.t) (s : seq int) : U32.t = x

will be dropped (albeit raising a warning) since seq does not have a definition (it should probably erasable.. but that's a whole thing F* responsibility). I was wondering if we could

• Support a keywork/attribute to specify that something must extract, and failhard if it doesn't. I see a note in F's examples/kv_parsing/README.md that this could be useful, wondering if you see any gotchas with adding this logic to F/krml.
• If the function has a "C" attribute, like above, I think it's a reasonable assumption that this was meant to actually extract, and hence trigger the logic above. I'm not convinced it's a good idea, just putting it out there (it can be an F*-only patch, and we could set it with an extension, so it's not a big deal either).

[msprotz]

The idea was that if something failed to extract, you'd get a warning 2 in krml (which if I recall correctly is set as an error, by default). This is how I notice this kind of issues. This is of course assuming that f is suitably called, say, by one of your tests.

The latter sounds like a good sanity check to have, and I would add it in F*. But also, I'm wondering what tripped you -- can you say more about what prompted this issue? Thanks!

[mtzguido]

Right, in my case this is not externally called at the F* level, only by a C driver. This is part of the API of the library we're building, say. The warning raised here is 5, the description seems slightly wrong in the help (5: type definition contains an application of an undefined type abbreviation, but this is not a type definition).

Maybe we can add a attribute like CExtract? Or CAPI? Don't have any great ideas for the name itself :-)

Here's the out.krml contents and output of krml, for posterity.

$ ./bin/fstar.exe --read_krml_file out.krml  | tail -n12
FStar_Seq:
X:
  (DFunction None [(Comment "test")] 0 (TInt UInt32) (["X"], "f")
  [{ name = "x"; typ = (TInt UInt32); mut = false; meta = [] };
    {
      name = "s";
      typ =
        (TApp (["FStar", "Seq", "Base"], "seq")
          [(TQualified (["Prims"], "int"))]);
      mut = false;
      meta = []
      }] (EBound 1))

$ krml out.krml -skip-compilation
✔ [Monomorphization] ⏱️ 5ms
✔ [Inlining] ⏱️ 2ms
✔ [Pattern matches compilation] ⏱️ 2ms
✔ [Structs + Simplify 2] ⏱️ 4ms
✔ [Drop] ⏱️ <1ms
Warning 15: X.f is not Low*; it uses mathematical integers and runtime checks may fail; rewrite your code to use machine integers, or if you must, use -add-include '"krml/internal/compat.h"'; if this declaration is for specification purposes only, consider marking it noextract or using -bundle <name-of-the-module> to only keep reachable definitions.
Warning 1: X_f: Not generating code for X/X_f because of the error below:
Warning 5: X_f: hit a type application of FStar.Seq.Base.seq, which is not defined; dropping
✔ [AstToCStar] ⏱️ <1ms
✔ [CStarToC] ⏱️ <1ms
⚙ KaRaMeL auto-detecting tools. Here's what we found:
readlink is: readlink
KaRaMeL called via: krml
KaRaMeL home is: /home/guido/r/karamel
⚙ KaRaMeL will drive F*. Here's what we found:
read FSTAR_HOME via the environment
fstar is on branch master
fstar is: /home/guido/r/fstar/master/bin/fstar.exe /home/guido/r/karamel/runtime/WasmSupport.fst /home/guido/r/fstar/master/ulib/FStar.UInt128.fst --trace_error --expose_interfaces --include /home/guido/r/karamel/krmllib --include /home/guido/r/karamel/include
✔ [PrettyPrinting] ⏱️ 5ms
KaRaMeL: wrote out .c files for
KaRaMeL: wrote out .h files for

[msprotz]

Yeah in that case an attribute (not forwarded to krml) is your best bet. How about assert_lowstar?