Unused argument elimination discards required field

[landonf]

The following fails with an assert in krml (see below)

module CB = LowStar.ConstBuffer

module U8 = FStar.UInt8
module U32 = FStar.UInt32

inline_for_extraction
type buftype =
  | CONST

inline_for_extraction
let buffer_t (ty:buftype) (a:Type0) =
  match ty with
  | CONST -> CB.const_buffer a

inline_for_extraction
let length (#t:buftype) (#a:Type0) (b:buffer_t t a): GTot nat =
  match t with
  | CONST -> CB.length (b <: buffer_t CONST a)

inline_for_extraction
noeq type slice_t (t:buftype) (a:Type0) = {
  len: U32.t;
  bytes: (b:buffer_t t a { length b == U32.v len });
}

let example (s:slice_t CONST U8.t) = s.bytes

Fails with:

> fstar --odir . --codegen Kremlin BufferSlice.fst && krml out.krml
...
✔ [Monomorphization] ⏱️ 31ms
✔ [Inlining] ⏱️ 3ms
Fatal error: exception File "src/DataTypes.ml", line 508, characters 11-17: Assertion failed

The assert is in remove_unit_fields:

  method private default_value = function
    | TUnit -> EUnit
    | TAny -> EAny
    | _ -> assert false

Not a Contribution.

[msprotz]

Hi Landon,

Unfortunately I don't think you can achieve this as-is. Let me try to explain a little bit. After processing all of the inline_for_extraction's (let's ignore refinements which are irrelevant and get erased anyhow), you're getting this:

type slice t a = {
  len: u32;
  bytes: (match t with CONST -> const_buffer a);
}

let example (s: slice CONST u8) = s.bytes

This normalization is roughly the first step that happens in the extraction pipeline. The next step is erasing types that would prevent the program from type-checking with, roughly, ML-like polymorphism (this is a Letouzey-style extraction). This means in particular that the bytes field, having an indexed type (a match), gets erased to unit, because match ... is not a valid type, neither in Low* (or in ML for that matter). When a meaningful type like this gets erased to unit, the program falls outside of the Low* subset and all bets are off. (Granted, it could be better surfaced to the user than having me write an explanation on GitHub.)

Then, KreMLin thinks that this field is a unit and eliminates it, causing problems further down the pipeline.

I don't know much about your use-case, so it's hard to speculate, but let me try to offer a few suggestions.

General solution

There is a workaround that I established recently and documented here: https://github.com/project-everest/hacl-star/blob/master/code/streaming/Hacl.Streaming.Functor.fst#L29 -- well, sort of documented. (I had the same problem as you just a few months ago.)

Let me explain: you can introduce a spurious type parameter whose sole purpose is to superficially make your data type definition look like it's parameterized over a type. Here's your example, fixed, along with a demo of how to write buftype-polymorphic functions.

module Test

module CB = LowStar.ConstBuffer

module U8 = FStar.UInt8
module U32 = FStar.UInt32

inline_for_extraction
type buftype =
  | CONST

inline_for_extraction
let buffer_t (ty:buftype) (a:Type0) =
  match ty with
  | CONST -> CB.const_buffer a

inline_for_extraction
let length (#t:buftype) (#a:Type0) (b:buffer_t t a): GTot nat =
  match t with
  | CONST -> CB.length (b <: buffer_t CONST a)

// This extracts in ML as:
// type 'b slice_t = { len: U32.t; bytes: 'b }
// which then triggers whole-program monomorphization over type parameter 'b.
inline_for_extraction
noeq type slice_t (t:Ghost.erased buftype) (a:Type0) (b: Type0 { b == buffer_t t a }) = {
  len: U32.t;
  bytes: (buf:b { length (buf <: buffer_t t a) == U32.v len });
}

// An abbreviation for convenience.
inline_for_extraction noextract
let slice_t' (t: Ghost.erased buftype) (a: Type0) =
  slice_t t a (buffer_t t a)

// No particular precautions are required to use slice_t' provided the t is a
// constant value that can trigger reduction (you get a monomorphic function).
let example (s:slice_t' CONST U8.t) = s.bytes

// If you want to write a slice-polymorphic function, you need to enforce
// ML-style prenex polymorphism via a type parameter that appears *first*.
let length' (#t: Ghost.erased buftype) (#a:Type0) (#b: Type0 { b == buffer_t t a }) (s: slice_t t a b) =
  s.len

module B = LowStar.Buffer

let test (): FStar.HyperStack.ST.St UInt32.t =
  let b = B.malloc FStar.HyperStack.root 0uy 1ul in
  let b = CB.of_buffer b in
  let s: slice_t' CONST UInt8.t = { bytes = b; len = 1ul } in
  length' s

Note that you will get a monomorphization of the type slice_t for each flavor of buffer you use in your program.

// Specialized definition of slice, for b == CB.const_buffer UInt8.t, obtained via KreMLin whole-program monomorphization
typedef struct Test_slice_t__const_uint8_t__s
{
  uint32_t len;
  const uint8_t *bytes;
}
Test_slice_t__const_uint8_t_;

// Specialized definition of example, obtained via F* reduction since the arguments to the type are constant
const uint8_t *Test_example(Test_slice_t__const_uint8_t_ s);

// No polymorphism in C, so the polymorphic function length is not compiled, but for each use-site, a monomorphic instance is generated, in this case, from the use of `length'` in test (). Also note how the judicious use of `erased` in the F* code makes sure the signature of Test_length' is clean and doesn't mention any buftype parameter. (It would without the erased, which would be a shame.)
uint32_t Test_length_(uint32_t s);

Ad-hoc solution

You can probably replace the record type with a pair to achieve the same effect.

---

If this helps, don't hesitate to continue the discussion on zulip (https://fstar.zulipchat.com/#narrow/stream/184683-questions-and.20help) so that others can benefit from it, or feel free to submit a PR to the Low* tutorial to include this trick in the tips & tricks section.

Cheers,

Jonathan