Extraction.Krml: properly detect mem type, it does not have an argument

[mtzguido]

(ccing @msprotz since we were really surprised this would fail, but perhaps most krml invocations are done including an extracted ulib, wondering if it's worthwhile to add a test for this somewhere --- commit message below)

Previous to this patch, extracting this snippet to kmrl:

module B = LowStar.Buffer
module HST = FStar.HyperStack.ST
module U32 = FStar.UInt32

let test2 (a : B.buffer U32.t) :
  HST.ST unit
    (requires fun h -> B.live h a /\ B.freeable a /\ B.length a > 0)
    (ensures fun _ _ _ -> True)
=
  B.upd a 0ul 42ul

Would result in:

$ fstar.exe Inline.fst --codegen krml --krmloutput x.krml && fstar.exe --read_krml_file x.krml
[...]
Inline:
  DFunction (None, [], 0, TInt UInt32, (["Inline"], "test"), [{name = "a"; typ = TBuf TInt UInt32; mut = false; meta = []}], ELet ({name = "x"; typ = TInt UInt32; mut = false; meta = [CInline]}, EBufRead (EBound 0, EConstant (UInt32, "0")), ESequence [EBufFree EBound 1, EBound 0]))
  DFunction (None, [], 0, TUnit, (["Inline"], "test2"), [{name = "a"; typ = TBuf TInt UInt32; mut = false; meta = []}], ELet ({name = "h"; typ = TQualified (["FStar", "Monotonic", "HyperStack"], "mem"); mut = false; meta = []}, EUnit, EBufWrite (EBound 1, EConstant (UInt32, "0"), EConstant (UInt32, "42"))))

Note the binding for h at type FStar.Monotonic.HyperStack.mem, defined as EUnit. This comes from the definition of upd as wrapper:

val upd'
  (#a:Type0) (#rrel #rel:srel a)
  (b:mbuffer a rrel rel)
  (i:U32.t)
  (v:a)
  :HST.Stack unit (requires (fun h -> live h b /\ U32.v i < length b /\
				   rel (as_seq h b) (Seq.upd (as_seq h b) (U32.v i) v)))
		  (ensures  (fun h _ h' -> h' == g_upd b (U32.v i) v h))

inline_for_extraction
let upd
  (#a:Type0) (#rrel #rel:srel a)
  (b:mbuffer a rrel rel)
  (i:U32.t)
  (v:a)
  : HST.Stack unit (requires (fun h -> live h b /\ U32.v i < length b /\
				    rel (as_seq h b) (Seq.upd (as_seq h b) (U32.v i) v)))
		   (ensures (fun h _ h' -> (not (g_is_null b)) /\
					modifies (loc_buffer b) h h' /\
					live h' b /\
					as_seq h' b == Seq.upd (as_seq h b) (U32.v i) v))
  = let h = HST.get () in
    upd' b i v;
    g_upd_seq_as_seq b (Seq.upd (as_seq h b) (U32.v i) v) h

Now, if we try to actually extract C code, it works fine, but apparently only since karamel knows the definition of the mem, since it is in the krml file, and erases it. Tightening the --extract makes it fail with a type mismatch, and the function is skipped.

$ rm -f *.checked *.c *.h *.ml && fstar.exe Inline.fst --codegen krml --extract '-*,Inline' && krml Inline.krml -skip-compilation
Extracted module Inline
Attempting to translate module Inline
Verified module: Inline
All verification conditions discharged successfully
make: Entering directory '/home/guido/r/gpu/main/karamel'
dune build
ln -sf _build/default/src/Karamel.exe krml
make: Leaving directory '/home/guido/r/gpu/main/karamel'
Cannot re-check Inline.test2 as valid Low* and will not extract it.  If
Inline.test2 is not meant to be extracted, consider marking it as Ghost,
noextract, or using a bundle. If it is meant to be extracted, use -dast
for further debugging.

Warning 4: in the definition of h, in top-level declaration
Inline.test2, in file Inline: Malformed input:
subtype mismatch:
  () (a.k.a. ()) vs:
  FStar_Monotonic_HyperStack_mem (a.k.a. FStar_Monotonic_HyperStack_mem)
--------------------------------------------------------------------------------

⚠ [Monomorphization] ⏱️ 2ms
✔ [Inlining] ⏱️ 2ms
✔ [Pattern matches compilation] ⏱️ 2ms
✔ [Structs + Simplify 2] ⏱️ 3ms
✔ [Drop] ⏱️ <1ms
✔ [AstToCStar] ⏱️ <1ms
✔ [CStarToC] ⏱️ <1ms
⚙ KaRaMeL auto-detecting tools. Here's what we found:
readlink is: readlink
KaRaMeL called via: ./karamel/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] ⏱️ 4ms
KaRaMeL: wrote out .c files for
KaRaMeL: wrote out .h files for

$ ls *.c
ls: cannot access '*.c': No such file or directory

[msprotz]

Yeah so krml is whole-program and expects definitions for the entire universe -- I don't think I ever tried to make it more modular. If this is a goal, you and I can start discussing how to make this happen, but I don't think this has been tried before :-)