KaRaMeL extraction: type alias not normalized in alloc, causes subtype mismatch

[elefthei]

Summary

When extracting Pulse code to C via --codegen krml, F* emits a type alias (e.g., ASpec_mybyte) for the array element type in alloc but emits the concrete base type (uint8_t) for the initializer literal. KaRaMeL sees these as mismatched types and drops the function with Warning 4.

Minimal reproducer

ASpec.fst — defines a type alias:

module ASpec
type mybyte = FStar.UInt8.t

ABuf.fsti — interface using the alias:

module ABuf
open Pulse.Lib.Pervasives
open Pulse.Lib.Vec
open FStar.SizeT
module SZ = FStar.SizeT

noeq type my_buf = { data: Pulse.Lib.Box.box (vec ASpec.mybyte); len: SZ.t }

val create (n: SZ.t{SZ.v n > 0})
  : stt my_buf emp (fun _ -> emp)

ABuf.fst — implementation:

module ABuf
#lang-pulse
open Pulse.Lib.Pervasives
open Pulse.Lib.Vec
open FStar.SizeT
module SZ = FStar.SizeT
module B = Pulse.Lib.Box
open Pulse.Lib.Box { box, (:=), (!) }

fn create (n: SZ.t{SZ.v n > 0})
  requires emp
  returns s : my_buf
  ensures emp
{
  let v : vec ASpec.mybyte = alloc #ASpec.mybyte 0uy n;
  let b = B.alloc #(vec ASpec.mybyte) v;
  admit();
  { data = b; len = n }
}

Wrap.fst — wrapper (no .fsti) to make function public in krml:

module Wrap
#lang-pulse
open Pulse.Lib.Pervasives
open FStar.SizeT
module SZ = FStar.SizeT

fn wrap_create (n: SZ.t{SZ.v n > 0})
  requires emp
  returns s : ABuf.my_buf
  ensures emp
{ ABuf.create n }

Steps to reproduce

PULSE_ROOT=~/pulse

# Extract all modules to krml
for mod in ASpec ABuf Wrap; do
  fstar.exe ${mod}.fst \
    --include $PULSE_ROOT/out/lib/pulse \
    --include $PULSE_ROOT/out/lib/pulse/lib \
    --cache_checked_modules --cache_dir _cache --odir _output \
    --already_cached 'Prims,FStar,Pulse.Nolib,Pulse.Lib,Pulse.Class,PulseCore' \
    --warn_error -321 --ext optimize_let_vc \
    --codegen krml --extract_module $mod
done

# Bundle WITHOUT ASpec.krml → ABuf.create is DROPPED
krml -skip-compilation -skip-makefiles -skip-linking \
  -bundle 'Wrap=Wrap,ABuf' -tmpdir _c_bug \
  _output/Wrap.krml _output/ABuf.krml

Observed behavior

Cannot re-check ABuf.create as valid Low* and will not extract it.

Warning 4: in the definition of v, in top-level declaration ABuf.create, in file Wrap:
Malformed input:
subtype mismatch:
  uint8_t (a.k.a. uint8_t) vs:
  ASpec_mybyte (a.k.a. ASpec_mybyte)

ABuf.create is silently dropped from the C output.

Root cause

In the krml AST for ABuf.create, the alloc call has:

• Buffer element type: ASpec_mybyte (unresolved alias)
• Initializer literal: 0uint8_t (concrete type)

KaRaMeL's monomorphization sees ASpec_mybyte ≠ uint8_t and rejects the function.

Workaround

Include the type-defining module's krml in the bundle:

krml -bundle 'Wrap=Wrap,ABuf,ASpec' _output/*.krml  # works

Expected behavior

F*'s --codegen krml should normalize type aliases to their base types in the krml output, so that alloc #ASpec.mybyte 0uy n produces consistent types for both the buffer element type and the initializer. This would eliminate the dependency on having the type-alias-defining module's krml present.

Versions

• F* 2025.12.15~dev
• KaRaMeL d6607b99
• Pulse: current main