From f124f5abe7d44dcac21563d252c399700c9e559d Mon Sep 17 00:00:00 2001
From: Thomas Lively <tlively@google.com>
Date: Fri, 31 Oct 2025 07:23:24 -0700
Subject: [PATCH 1/4] Update exact function imports

Address feedback from #72, including by using (exact, deftype) pairs
instead of full heaptypes where possible in the interpreter. Update the
overview accordingly.

Also fix #74 by introducing a new externtype binary encoding for exact
function imports rather than using an s33 in the existing function
import variant.
---
 interpreter/binary/decode.ml             |  3 ++-
 interpreter/binary/encode.ml             |  3 ++-
 interpreter/host/env.ml                  |  4 ++--
 interpreter/runtime/instance.ml          |  2 +-
 interpreter/script/js.ml                 |  8 +++----
 interpreter/syntax/ast.ml                |  6 +++--
 interpreter/syntax/free.ml               |  2 +-
 interpreter/syntax/types.ml              | 12 ++++------
 interpreter/text/arrange.ml              |  8 +++----
 interpreter/text/parser.mly              | 25 +++++++++-----------
 interpreter/valid/match.ml               |  3 ++-
 interpreter/valid/valid.ml               | 28 +++++++++--------------
 proposals/custom-descriptors/Overview.md | 29 +++++++++++++++++++-----
 test/core/binary-leb128.wast             |  2 +-
 test/core/binary.wast                    | 25 ++------------------
 15 files changed, 75 insertions(+), 85 deletions(-)

diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml
index 2497ad717..b6c68b2f9 100644
--- a/interpreter/binary/decode.ml
+++ b/interpreter/binary/decode.ml
@@ -320,11 +320,12 @@ let tabletype s =
 
 let externtype s =
   match byte s with
-  | 0x00 -> ExternFuncT (heaptype s)
+  | 0x00 -> ExternFuncT (Inexact, typeuse idx s)
   | 0x01 -> ExternTableT (tabletype s)
   | 0x02 -> ExternMemoryT (memorytype s)
   | 0x03 -> ExternGlobalT (globaltype s)
   | 0x04 -> ExternTagT (tagtype s)
+  | 0x05 -> ExternFuncT (Exact, typeuse idx s)
   | _ -> error s (pos s - 1) "malformed import kind"
 
 
diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml
index 3d6651eb8..038ff7f4e 100644
--- a/interpreter/binary/encode.ml
+++ b/interpreter/binary/encode.ml
@@ -207,7 +207,8 @@ struct
     | TableT (at, lim, t) -> reftype t; limits at lim
 
   let externtype = function
-    | ExternFuncT ht -> byte 0x00; heaptype ht
+    | ExternFuncT (Inexact, ut) -> byte 0x00; typeuse u32 ut
+    | ExternFuncT (Exact, ut) -> byte 0x05; typeuse u32 ut
     | ExternTableT tt -> byte 0x01; tabletype tt
     | ExternMemoryT mt -> byte 0x02; memorytype mt
     | ExternGlobalT gt -> byte 0x03; globaltype gt
diff --git a/interpreter/host/env.ml b/interpreter/host/env.ml
index c095f8f21..376792ae2 100644
--- a/interpreter/host/env.ml
+++ b/interpreter/host/env.ml
@@ -42,8 +42,8 @@ let exit vs =
 
 let lookup name et =
   match Utf8.encode name, et with
-  | "abort", ExternFuncT (UseHT (_exact, ut)) ->
+  | "abort", ExternFuncT (_exact, ut) ->
     ExternFunc (Func.alloc_host (deftype_of_typeuse ut) abort)
-  | "exit", ExternFuncT (UseHT (_exact, ut)) ->
+  | "exit", ExternFuncT (_exact, ut) ->
     ExternFunc (Func.alloc_host (deftype_of_typeuse ut) exit)
   | _ -> raise Not_found
diff --git a/interpreter/runtime/instance.ml b/interpreter/runtime/instance.ml
index 446f3576b..01806aa3e 100644
--- a/interpreter/runtime/instance.ml
+++ b/interpreter/runtime/instance.ml
@@ -75,7 +75,7 @@ let externtype_of c = function
   | ExternGlobal glob -> ExternGlobalT (Global.type_of glob)
   | ExternMemory mem -> ExternMemoryT (Memory.type_of mem)
   | ExternTable tab -> ExternTableT (Table.type_of tab)
-  | ExternFunc func -> ExternFuncT (UseHT (Exact, Def (Func.type_of func)))
+  | ExternFunc func -> ExternFuncT (Exact, Def (Func.type_of func))
 
 let export inst name =
   try Some (List.assoc name inst.exports) with Not_found -> None
diff --git a/interpreter/script/js.ml b/interpreter/script/js.ml
index d395a6882..e98c137dc 100644
--- a/interpreter/script/js.ml
+++ b/interpreter/script/js.ml
@@ -424,7 +424,7 @@ let invoke dt vs at =
   let rts0 = Lib.List32.init subject_type_idx (fun i -> dummy, (dummy, i)) in
   let rts, i = statify_deftype rts0 dt in
   List.map (fun (_, (rt, _)) -> rt @@ at) (Lib.List32.drop subject_type_idx rts),
-  ExternFuncT (UseHT (Inexact, (Idx i))),
+  ExternFuncT (Inexact, (Idx i)),
   List.concat (List.map value vs) @ [Call (subject_idx @@ at) @@ at]
 
 let get t at =
@@ -606,9 +606,9 @@ let wrap item_name wrap_action wrap_assertion at =
   let imports =
     [ Import (Utf8.decode "module", item_name, idesc) @@ at;
       Import (Utf8.decode "spectest", Utf8.decode "hostref",
-        ExternFuncT (UseHT (Inexact, (Idx 1l)))) @@ at;
+        ExternFuncT (Inexact, (Idx 1l))) @@ at;
       Import (Utf8.decode "spectest", Utf8.decode "eq_ref",
-        ExternFuncT (UseHT (Inexact, (Idx 2l)))) @@ at;
+        ExternFuncT (Inexact, (Idx 2l))) @@ at;
     ]
   in
   let item =
@@ -775,7 +775,7 @@ let of_action env act =
     "call(" ^ of_inst_opt env x_opt ^ ", " ^ of_name name ^ ", " ^
       "[" ^ String.concat ", " (List.map of_value vs) ^ "])",
     (match lookup_export env x_opt name act.at with
-    | ExternFuncT (UseHT (_exact, (Def dt))) ->
+    | ExternFuncT (_exact, (Def dt)) ->
       let (_, out) as ft = functype_of_comptype (expand_deftype dt) in
       if is_js_functype ft then
         None
diff --git a/interpreter/syntax/ast.ml b/interpreter/syntax/ast.ml
index 0a654aa36..387a9f381 100644
--- a/interpreter/syntax/ast.ml
+++ b/interpreter/syntax/ast.ml
@@ -414,8 +414,10 @@ let exporttype_of (m : module_) (ex : export) : exporttype =
     | FuncX x ->
       let dts = funcs xts @ List.map (fun f ->
         let Func (y, _, _) = f.it in
-        UseHT (Exact, Def (Lib.List32.nth dts y.it))) m.it.funcs in
-      ExternFuncT (Lib.List32.nth dts x.it)
+        (Exact, Def (Lib.List32.nth dts y.it))) m.it.funcs
+      in
+      let (exact, dt) = Lib.List32.nth dts x.it in
+      ExternFuncT (exact, dt)
   in ExportT (name, subst_externtype (subst_of dts) xt)
 
 let moduletype_of (m : module_) : moduletype =
diff --git a/interpreter/syntax/free.ml b/interpreter/syntax/free.ml
index 812b12efc..8c4575492 100644
--- a/interpreter/syntax/free.ml
+++ b/interpreter/syntax/free.ml
@@ -129,7 +129,7 @@ let externtype = function
   | ExternGlobalT gt -> globaltype gt
   | ExternMemoryT mt -> memorytype mt
   | ExternTableT tt -> tabletype tt
-  | ExternFuncT ht -> heaptype ht
+  | ExternFuncT (_, ut) -> typeuse ut
 
 let blocktype = function
   | VarBlockType x -> types (idx x)
diff --git a/interpreter/syntax/types.ml b/interpreter/syntax/types.ml
index 71515192f..7e0e81e36 100644
--- a/interpreter/syntax/types.ml
+++ b/interpreter/syntax/types.ml
@@ -49,7 +49,7 @@ type externtype =
   | ExternGlobalT of globaltype
   | ExternMemoryT of memorytype
   | ExternTableT of tabletype
-  | ExternFuncT of heaptype
+  | ExternFuncT of exact * typeuse
 
 type exporttype = ExportT of name * externtype
 type importtype = ImportT of name * name * externtype
@@ -125,8 +125,6 @@ let unpacked_fieldtype (FieldT (_mut, t)) = unpacked_storagetype t
 let idx_of_typeuse = function Idx x -> x | _ -> assert false
 let deftype_of_typeuse = function Def dt -> dt | _ -> assert false
 
-let typeuse_of_heaptype = function UseHT (_, ut) -> ut | _ -> assert false
-
 let structtype_of_comptype = function StructT fts -> fts | _ -> assert false
 let arraytype_of_comptype = function ArrayT ft -> ft | _ -> assert false
 let functype_of_comptype = function FuncT rt2 -> rt2 | _ -> assert false
@@ -141,7 +139,7 @@ let tags = List.filter_map (function ExternTagT tt -> Some tt | _ -> None)
 let globals = List.filter_map (function ExternGlobalT gt -> Some gt | _ -> None)
 let memories = List.filter_map (function ExternMemoryT mt -> Some mt | _ -> None)
 let tables = List.filter_map (function ExternTableT tt -> Some tt | _ -> None)
-let funcs = List.filter_map (function ExternFuncT ft -> Some ft | _ -> None)
+let funcs = List.filter_map (function ExternFuncT (exact, ut) -> Some (exact, ut) | _ -> None)
 
 
 (* Substitution *)
@@ -237,7 +235,7 @@ let subst_externtype s = function
   | ExternGlobalT gt -> ExternGlobalT (subst_globaltype s gt)
   | ExternMemoryT mt -> ExternMemoryT (subst_memorytype s mt)
   | ExternTableT tt -> ExternTableT (subst_tabletype s tt)
-  | ExternFuncT ht -> ExternFuncT (subst_heaptype s ht)
+  | ExternFuncT (exact, ut) -> ExternFuncT (exact, subst_typeuse s ut)
 
 
 let subst_exporttype s = function
@@ -448,8 +446,8 @@ let string_of_externtype = function
   | ExternGlobalT gt -> "global " ^ string_of_globaltype gt
   | ExternMemoryT mt -> "memory " ^ string_of_memorytype mt
   | ExternTableT tt -> "table " ^ string_of_tabletype tt
-  | ExternFuncT ht -> "func " ^ string_of_heaptype ht
-
+  | ExternFuncT (Inexact, ut) -> "func " ^ string_of_typeuse ut
+  | ExternFuncT (Exact, ut) -> "func exact " ^ string_of_typeuse ut
 
 let string_of_exporttype = function
   | ExportT (name, xt) ->
diff --git a/interpreter/text/arrange.ml b/interpreter/text/arrange.ml
index 45c3348b7..d1a576653 100644
--- a/interpreter/text/arrange.ml
+++ b/interpreter/text/arrange.ml
@@ -85,9 +85,8 @@ let valtype t = string_of_valtype t
 let storagetype t = string_of_storagetype t
 
 let heaptypeuse = function
-  | UseHT (Inexact, ut) -> typeuse ut
-  | UseHT (Exact, ut) -> Node ("exact", [typeuse ut])
-  | _ -> assert false
+  | (Inexact, ut) -> typeuse ut
+  | (Exact, ut) -> Node ("exact", [typeuse ut])
 
 let final = function
   | NoFinal -> ""
@@ -713,7 +712,8 @@ let importtype fx tx mx tgx gx = function
   | ExternGlobalT gt -> incr gx; Node ("global $" ^ nat (!gx - 1), globaltype gt)
   | ExternMemoryT mt -> incr mx; Node ("memory $" ^ nat (!mx - 1), memorytype mt)
   | ExternTableT tt -> incr tx; Node ("table $" ^ nat (!tx - 1), tabletype tt)
-  | ExternFuncT ht -> incr fx; Node ("func $" ^ nat (!fx - 1), [heaptypeuse ht])
+  | ExternFuncT (exact, ut) ->
+    incr fx; Node ("func $" ^ nat (!fx - 1), [heaptypeuse (exact, ut)])
 
 let import fx tx mx ex gx im =
   let Import (module_name, item_name, xt) = im.it in
diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly
index 81fb70663..3ca59b750 100644
--- a/interpreter/text/parser.mly
+++ b/interpreter/text/parser.mly
@@ -492,9 +492,9 @@ limits :
 typeuse :
   | LPAR TYPE idx RPAR { fun c -> $3 c type_ }
 
-heaptypeuse :
-  | LPAR EXACT typeuse RPAR { fun c -> UseHT (Exact, Idx ($3 c).it) }
-  | typeuse { fun c -> UseHT (Inexact, Idx ($1 c).it) }
+exacttypeuse :
+  | LPAR EXACT typeuse RPAR { fun c -> (Exact, $3 c) }
+  | typeuse { fun c -> (Inexact, $1 c) }
 
 /* Immediates */
 
@@ -998,20 +998,17 @@ func_fields :
       let y = inline_functype c' (fst $1 c') loc in
       let Func (_, ls, es) = snd $1 c' in
       [Func (y, ls, es) @@ loc], [], [] }
-  | inline_import heaptypeuse func_fields_import  /* Sugar */
+  | inline_import exacttypeuse func_fields_import  /* Sugar */
     { fun c x loc ->
-      let exact, y = match ($2 c) with
-        | UseHT (exact, Idx y) -> exact, y
-        | _ -> assert false
-      in
-      let y = inline_functype_explicit c (y @@ loc) ($3 c) in
+      let exact, y = ($2 c) in
+      let y = inline_functype_explicit c y ($3 c) in
       [],
-      [Import (fst $1, snd $1, ExternFuncT (UseHT (exact, Idx y.it))) @@ loc ], [] }
+      [Import (fst $1, snd $1, ExternFuncT (exact, Idx y.it)) @@ loc ], [] }
   | inline_import func_fields_import  /* Sugar */
     { fun c x loc ->
       let y = inline_functype c ($2 c) loc in
       [],
-      [Import (fst $1, snd $1, ExternFuncT (UseHT (Inexact, Idx y.it))) @@ loc ], [] }
+      [Import (fst $1, snd $1, ExternFuncT (Inexact, Idx y.it)) @@ loc ], [] }
   | inline_export func_fields  /* Sugar */
     { fun c x loc ->
       let fns, ims, exs = $2 c x loc in fns, ims, $1 (FuncX x) c :: exs }
@@ -1253,9 +1250,9 @@ table_fields :
 /* Imports & Exports */
 
 externtype :
-  | LPAR FUNC bindidx_opt heaptypeuse RPAR
+  | LPAR FUNC bindidx_opt exacttypeuse RPAR
     { fun c -> ignore ($3 c anon_func bind_func);
-      fun () -> ExternFuncT ($4 c) }
+      fun () -> let exact, y = ($4 c) in ExternFuncT (exact, Idx y.it) }
   | LPAR TAG bindidx_opt typeuse RPAR
     { fun c -> ignore ($3 c anon_tag bind_tag);
       fun () -> ExternTagT (TagT (Idx ($4 c).it)) }
@@ -1276,7 +1273,7 @@ externtype :
       fun () ->
         let exact, ft = $4 c in
         let y = inline_functype c ft $loc($4) in
-        ExternFuncT (UseHT (exact, Idx y.it)) }
+        ExternFuncT (exact, Idx y.it) }
 
 import :
   | LPAR IMPORT name name externtype RPAR
diff --git a/interpreter/valid/match.ml b/interpreter/valid/match.ml
index 7b68937c1..70d198b90 100644
--- a/interpreter/valid/match.ml
+++ b/interpreter/valid/match.ml
@@ -197,5 +197,6 @@ let match_externtype c xt1 xt2 =
   | ExternGlobalT gt1, ExternGlobalT gt2 -> match_globaltype c gt1 gt2
   | ExternMemoryT mt1, ExternMemoryT mt2 -> match_memorytype c mt1 mt2
   | ExternTableT tt1, ExternTableT tt2 -> match_tabletype c tt1 tt2
-  | ExternFuncT ht1, ExternFuncT ht2 -> match_heaptype c ht1 ht2
+  | ExternFuncT (exact1, ut1), ExternFuncT (exact2, ut2) -> 
+    match_heaptype c (UseHT (exact1, ut1)) (UseHT (exact2, ut2))
   | _, _ -> false
diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml
index 7c4709e9b..f28ea9057 100644
--- a/interpreter/valid/valid.ml
+++ b/interpreter/valid/valid.ml
@@ -22,7 +22,7 @@ type context =
   globals : globaltype list;
   memories : memorytype list;
   tables : tabletype list;
-  funcs : heaptype list;
+  funcs : (exact * deftype) list;
   datas : unit list;
   elems : reftype list;
   locals : localtype list;
@@ -243,7 +243,6 @@ let check_rectype (c : context) (rt : rectype) at : context =
     (fun i st -> check_subtype_sub c' st (Int32.add x i) at) sts;
   c'
 
-
 let check_tagtype (c : context) (tt : tagtype) at =
   let TagT ut = tt in
   let (ts1, ts2) = func_type c (idx_of_typeuse ut @@ at) in
@@ -283,14 +282,8 @@ let check_externtype (c : context) (xt : externtype) at =
     check_memorytype c mt at
   | ExternTableT tt ->
     check_tabletype c tt at
-  | ExternFuncT (UseHT (_exact, ut)) ->
+  | ExternFuncT (_exact, ut) ->
     let _ft = func_type c (idx_of_typeuse ut @@ at) in ()
-  | ExternFuncT ht ->
-    error at
-      ("external function type should have defined type, but has " ^
-       string_of_heaptype ht)
-
-
 
 let diff_reftype (nul1, ht1) (nul2, ht2) =
   match nul2 with
@@ -639,7 +632,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_resulttype) : infer_ins
     c.results -->... [], []
 
   | Call x ->
-    let dt = deftype_of_typeuse (typeuse_of_heaptype (func c x)) in
+    let (_, dt) = func c x in
     let (ts1, ts2) = functype_of_comptype (expand_deftype dt) in
     ts1 --> ts2, []
 
@@ -656,7 +649,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_resulttype) : infer_ins
     (ts1 @ [NumT (numtype_of_addrtype at)]) --> ts2, []
 
   | ReturnCall x ->
-    let dt = deftype_of_typeuse (typeuse_of_heaptype (func c x)) in
+    let (_, dt) = func c x in
     let (ts1, ts2) = functype_of_comptype (expand_deftype dt) in
     require (match_resulttype c.types ts2 c.results) e.at
       ("type mismatch: current function requires result type " ^
@@ -832,9 +825,9 @@ let rec check_instr (c : context) (e : instr) (s : infer_resulttype) : infer_ins
     [] --> [RefT (Null, ht)], []
 
   | RefFunc x ->
-    let ht = func c x in
+    let (exact, dt) = func c x in
     refer_func c x;
-    [] --> [RefT (NoNull, ht)], []
+    [] --> [RefT (NoNull, UseHT (exact, Def dt))], []
 
   | RefIsNull ->
     let (_nul, ht) = peek_ref 0 s e.at in
@@ -1152,7 +1145,7 @@ let check_local (c : context) (loc : local) : localtype =
 let check_func (c : context) (f : func) : context =
   let Func (x, _ls, _es) = f.it in
   let _ft = func_type c x in
-  {c with funcs = c.funcs @ [UseHT (Exact, Def (type_ c x))]}
+  {c with funcs = c.funcs @ [(Exact, type_ c x)]}
 
 let check_func_body (c : context) (f : func) =
   let Func (x, ls, es) = f.it in
@@ -1248,7 +1241,7 @@ let check_type (c : context) (t : type_) : context =
 
 let check_start (c : context) (start : start) =
   let Start x = start.it in
-  let dt = deftype_of_typeuse (typeuse_of_heaptype (func c x)) in
+  let (_, dt) = func c x in
   let ft = functype_of_comptype (expand_deftype dt) in
   require (ft = ([], [])) start.at
     "start function must not have parameters or results"
@@ -1261,7 +1254,8 @@ let check_import (c : context) (im : import) : context =
   | ExternGlobalT gt -> {c with globals = c.globals @ [gt]}
   | ExternMemoryT mt -> {c with memories = c.memories @ [mt]}
   | ExternTableT tt -> {c with tables = c.tables @ [tt]}
-  | ExternFuncT ht -> {c with funcs = c.funcs @ [ht]}
+  | ExternFuncT (exact, ut) ->
+    {c with funcs = c.funcs @ [(exact, deftype_of_typeuse ut)]}
 
 module NameSet = Set.Make(struct type t = Ast.name let compare = compare end)
 
@@ -1273,7 +1267,7 @@ let check_export (c : context) (ex : export) : exporttype =
     | GlobalX x -> ExternGlobalT (global c x)
     | MemoryX x -> ExternMemoryT (memory c x)
     | TableX x -> ExternTableT (table c x)
-    | FuncX x -> ExternFuncT (func c x)
+    | FuncX x -> ExternFuncT (Inexact, Def (snd (func c x)))
   in ExportT (name, xt)
 
 let check_list f xs (c : context) : context =
diff --git a/proposals/custom-descriptors/Overview.md b/proposals/custom-descriptors/Overview.md
index 89687abf0..d57c16f44 100644
--- a/proposals/custom-descriptors/Overview.md
+++ b/proposals/custom-descriptors/Overview.md
@@ -387,10 +387,10 @@ Function imports already give a type for the imported function;
 we must now make it possible for that type to be exact.
 
 The external type of a function import is currently represented as a `typeuse`,
-but we can change that to `heaptype` to allow for exact types.
+so we can just make it a pair of `exact` and `typeuse`:
 
 ```
-externtype ::= ... | func heaptype
+externtype ::= ... | func exact? heaptype
 ```
 
 In the text format,
@@ -398,15 +398,15 @@ function import types are given by `typeuse` and its associated sugar.
 We don't want to allow exactness everywhere `typeuse`
 appears in the text format,
 so instead of extending the syntax of `typeuse`,
-we introduce a new production, `heaptypeuse`.
+we introduce a new production, `exacttypeuse`.
 
 ```
-heaptypeuse ::= '(' 'exact' ut:typeuse ')' => exact ut
-              | ut:typeuse                 => inexact ut
+exacttypeuse ::= '(' 'exact' ut:typeuse ')' => exact ut
+               | ut:typeuse                 => inexact ut
 ```
 
 Function imports, including all their sytax sugars,
-are updated to use `heaptypeuse` in place of `typeuse`.
+are updated to use `exacttypeuse` in place of `typeuse`.
 For example:
 
 ```wasm
@@ -941,6 +941,23 @@ heaptype :: ... | 0x62 x:u32 => exact x
 Note that the type index being encoded as a `u32` instead of an `s33`
 intentionally makes it impossible to encode an exact abstract heap type.
 
+### Exact Function Imports
+
+The `externtype` encoding is updated
+with a new variant for exact function imports:
+
+```
+externtype = 0x00 x:typeidx => func x
+             ...
+             0x05 x:typeidx => func exact x
+```
+
+Note that we do not add support for exactly exported functions.
+An export section using 0x05 is malfomed.
+
+> We may add support for exact function exports in the future if there is
+> some reason to do so.
+
 ### Instructions
 
 All existing instructions that take heap type immediates work without
diff --git a/test/core/binary-leb128.wast b/test/core/binary-leb128.wast
index b515893e1..27584c7f6 100644
--- a/test/core/binary-leb128.wast
+++ b/test/core/binary-leb128.wast
@@ -667,7 +667,7 @@
   "\00"                                ;; import kind
   "\80\80\80\80\10"                    ;; import signature index 0 with unused bits set
 )
-  "integer representation too long"
+  "integer too large"
 )
 (assert_malformed
   (module binary
diff --git a/test/core/binary.wast b/test/core/binary.wast
index e328be360..bdd3ef65d 100644
--- a/test/core/binary.wast
+++ b/test/core/binary.wast
@@ -491,7 +491,7 @@
       "\02\04\01"                           ;; import section with single entry
       "\00"                                 ;; string length 0
       "\00"                                 ;; string length 0
-      "\05"                                 ;; malformed import kind
+      "\06"                                 ;; malformed import kind
   )
   "malformed import kind"
 )
@@ -501,28 +501,7 @@
       "\02\05\01"                           ;; import section with single entry
       "\00"                                 ;; string length 0
       "\00"                                 ;; string length 0
-      "\05"                                 ;; malformed import kind
-      "\00"                                 ;; dummy byte
-  )
-  "malformed import kind"
-)
-(assert_malformed
-  (module binary
-      "\00asm" "\01\00\00\00"
-      "\02\04\01"                           ;; import section with single entry
-      "\00"                                 ;; string length 0
-      "\00"                                 ;; string length 0
-      "\05"                                 ;; malformed import kind
-  )
-  "malformed import kind"
-)
-(assert_malformed
-  (module binary
-      "\00asm" "\01\00\00\00"
-      "\02\05\01"                           ;; import section with single entry
-      "\00"                                 ;; string length 0
-      "\00"                                 ;; string length 0
-      "\05"                                 ;; malformed import kind
+      "\06"                                 ;; malformed import kind
       "\00"                                 ;; dummy byte
   )
   "malformed import kind"

From 5332008718a49da688d27540821b740d5e5b2314 Mon Sep 17 00:00:00 2001
From: Thomas Lively <tlively@google.com>
Date: Mon, 3 Nov 2025 14:28:56 -0800
Subject: [PATCH 2/4] formatting and typos

---
 interpreter/script/js.ml                 | 8 ++++----
 interpreter/text/arrange.ml              | 4 ++--
 interpreter/text/parser.mly              | 4 ++--
 proposals/custom-descriptors/Overview.md | 2 +-
 4 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/interpreter/script/js.ml b/interpreter/script/js.ml
index e98c137dc..18cfe79cf 100644
--- a/interpreter/script/js.ml
+++ b/interpreter/script/js.ml
@@ -424,7 +424,7 @@ let invoke dt vs at =
   let rts0 = Lib.List32.init subject_type_idx (fun i -> dummy, (dummy, i)) in
   let rts, i = statify_deftype rts0 dt in
   List.map (fun (_, (rt, _)) -> rt @@ at) (Lib.List32.drop subject_type_idx rts),
-  ExternFuncT (Inexact, (Idx i)),
+  ExternFuncT (Inexact, Idx i),
   List.concat (List.map value vs) @ [Call (subject_idx @@ at) @@ at]
 
 let get t at =
@@ -606,9 +606,9 @@ let wrap item_name wrap_action wrap_assertion at =
   let imports =
     [ Import (Utf8.decode "module", item_name, idesc) @@ at;
       Import (Utf8.decode "spectest", Utf8.decode "hostref",
-        ExternFuncT (Inexact, (Idx 1l))) @@ at;
+        ExternFuncT (Inexact, Idx 1l)) @@ at;
       Import (Utf8.decode "spectest", Utf8.decode "eq_ref",
-        ExternFuncT (Inexact, (Idx 2l))) @@ at;
+        ExternFuncT (Inexact, Idx 2l)) @@ at;
     ]
   in
   let item =
@@ -775,7 +775,7 @@ let of_action env act =
     "call(" ^ of_inst_opt env x_opt ^ ", " ^ of_name name ^ ", " ^
       "[" ^ String.concat ", " (List.map of_value vs) ^ "])",
     (match lookup_export env x_opt name act.at with
-    | ExternFuncT (_exact, (Def dt)) ->
+    | ExternFuncT (_exact, Def dt) ->
       let (_, out) as ft = functype_of_comptype (expand_deftype dt) in
       if is_js_functype ft then
         None
diff --git a/interpreter/text/arrange.ml b/interpreter/text/arrange.ml
index d1a576653..c374be470 100644
--- a/interpreter/text/arrange.ml
+++ b/interpreter/text/arrange.ml
@@ -84,7 +84,7 @@ let heaptype t = string_of_heaptype t
 let valtype t = string_of_valtype t
 let storagetype t = string_of_storagetype t
 
-let heaptypeuse = function
+let exacttypeuse = function
   | (Inexact, ut) -> typeuse ut
   | (Exact, ut) -> Node ("exact", [typeuse ut])
 
@@ -713,7 +713,7 @@ let importtype fx tx mx tgx gx = function
   | ExternMemoryT mt -> incr mx; Node ("memory $" ^ nat (!mx - 1), memorytype mt)
   | ExternTableT tt -> incr tx; Node ("table $" ^ nat (!tx - 1), tabletype tt)
   | ExternFuncT (exact, ut) ->
-    incr fx; Node ("func $" ^ nat (!fx - 1), [heaptypeuse (exact, ut)])
+    incr fx; Node ("func $" ^ nat (!fx - 1), [exacttypeuse (exact, ut)])
 
 let import fx tx mx ex gx im =
   let Import (module_name, item_name, xt) = im.it in
diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly
index 3ca59b750..422fa4aae 100644
--- a/interpreter/text/parser.mly
+++ b/interpreter/text/parser.mly
@@ -1000,7 +1000,7 @@ func_fields :
       [Func (y, ls, es) @@ loc], [], [] }
   | inline_import exacttypeuse func_fields_import  /* Sugar */
     { fun c x loc ->
-      let exact, y = ($2 c) in
+      let exact, y = $2 c in
       let y = inline_functype_explicit c y ($3 c) in
       [],
       [Import (fst $1, snd $1, ExternFuncT (exact, Idx y.it)) @@ loc ], [] }
@@ -1252,7 +1252,7 @@ table_fields :
 externtype :
   | LPAR FUNC bindidx_opt exacttypeuse RPAR
     { fun c -> ignore ($3 c anon_func bind_func);
-      fun () -> let exact, y = ($4 c) in ExternFuncT (exact, Idx y.it) }
+      fun () -> let exact, y = $4 c in ExternFuncT (exact, Idx y.it) }
   | LPAR TAG bindidx_opt typeuse RPAR
     { fun c -> ignore ($3 c anon_tag bind_tag);
       fun () -> ExternTagT (TagT (Idx ($4 c).it)) }
diff --git a/proposals/custom-descriptors/Overview.md b/proposals/custom-descriptors/Overview.md
index d57c16f44..6673b25c7 100644
--- a/proposals/custom-descriptors/Overview.md
+++ b/proposals/custom-descriptors/Overview.md
@@ -405,7 +405,7 @@ exacttypeuse ::= '(' 'exact' ut:typeuse ')' => exact ut
                | ut:typeuse                 => inexact ut
 ```
 
-Function imports, including all their sytax sugars,
+Function imports, including all their syntax sugars,
 are updated to use `exacttypeuse` in place of `typeuse`.
 For example:
 

From fb2cc7a78a693c287474c063d6652c6a43dc8f7b Mon Sep 17 00:00:00 2001
From: Thomas Lively <tlively@google.com>
Date: Mon, 3 Nov 2025 16:07:08 -0800
Subject: [PATCH 3/4] Use 0x20 to encode exact function imports

---
 interpreter/binary/decode.ml | 2 +-
 interpreter/binary/encode.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml
index b6c68b2f9..fc512f56a 100644
--- a/interpreter/binary/decode.ml
+++ b/interpreter/binary/decode.ml
@@ -325,7 +325,7 @@ let externtype s =
   | 0x02 -> ExternMemoryT (memorytype s)
   | 0x03 -> ExternGlobalT (globaltype s)
   | 0x04 -> ExternTagT (tagtype s)
-  | 0x05 -> ExternFuncT (Exact, typeuse idx s)
+  | 0x20 -> ExternFuncT (Exact, typeuse idx s)
   | _ -> error s (pos s - 1) "malformed import kind"
 
 
diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml
index 038ff7f4e..07792bcdf 100644
--- a/interpreter/binary/encode.ml
+++ b/interpreter/binary/encode.ml
@@ -208,7 +208,7 @@ struct
 
   let externtype = function
     | ExternFuncT (Inexact, ut) -> byte 0x00; typeuse u32 ut
-    | ExternFuncT (Exact, ut) -> byte 0x05; typeuse u32 ut
+    | ExternFuncT (Exact, ut) -> byte 0x20; typeuse u32 ut
     | ExternTableT tt -> byte 0x01; tabletype tt
     | ExternMemoryT mt -> byte 0x02; memorytype mt
     | ExternGlobalT gt -> byte 0x03; globaltype gt

From 0fb4e2df61bc3d54613b551d86354edf626bef00 Mon Sep 17 00:00:00 2001
From: Thomas Lively <tlively@google.com>
Date: Tue, 4 Nov 2025 13:04:43 -0800
Subject: [PATCH 4/4] update export type, overview, binary tests

---
 interpreter/valid/valid.ml                    |  2 +-
 proposals/custom-descriptors/Overview.md      | 13 +++--
 .../custom-descriptors/exact-func-import.wast | 51 +++++++++++++++++++
 3 files changed, 60 insertions(+), 6 deletions(-)

diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml
index 4b4cd55fd..f3bbf0a85 100644
--- a/interpreter/valid/valid.ml
+++ b/interpreter/valid/valid.ml
@@ -1267,7 +1267,7 @@ let check_export (c : context) (ex : export) : exporttype =
     | GlobalX x -> ExternGlobalT (global c x)
     | MemoryX x -> ExternMemoryT (memory c x)
     | TableX x -> ExternTableT (table c x)
-    | FuncX x -> ExternFuncT (Inexact, Def (snd (func c x)))
+    | FuncX x -> let exact, dt = func c x in ExternFuncT (exact, Def dt)
   in ExportT (name, xt)
 
 let check_list f xs (c : context) : context =
diff --git a/proposals/custom-descriptors/Overview.md b/proposals/custom-descriptors/Overview.md
index 6673b25c7..25bcacea4 100644
--- a/proposals/custom-descriptors/Overview.md
+++ b/proposals/custom-descriptors/Overview.md
@@ -949,14 +949,17 @@ with a new variant for exact function imports:
 ```
 externtype = 0x00 x:typeidx => func x
              ...
-             0x05 x:typeidx => func exact x
+             0x20 x:typeidx => func exact x
 ```
 
-Note that we do not add support for exactly exported functions.
-An export section using 0x05 is malfomed.
+> The intention is that bit 6 is reserved to indicate exactness of other kinds
+> of `externtype`s in the future.
 
-> We may add support for exact function exports in the future if there is
-> some reason to do so.
+Note that exports do not need to separately declare exactness.
+Exported functions are exact if and only if
+the internal type of the function is exact
+(i.e. the function is imported exactly or defined in the module).
+An export section using 0x20 is malfomed.
 
 ### Instructions
 
diff --git a/test/core/custom-descriptors/exact-func-import.wast b/test/core/custom-descriptors/exact-func-import.wast
index d5b4fcf5a..45b35a9eb 100644
--- a/test/core/custom-descriptors/exact-func-import.wast
+++ b/test/core/custom-descriptors/exact-func-import.wast
@@ -211,3 +211,54 @@
 (assert_trap (invoke "exact-cast") "cast failure")
 (assert_trap (invoke "exact-br-on-cast") "unreachable")
 (assert_trap (invoke "exact-br-on-cast-fail") "unreachable")
+
+
+;; Test the binary format
+
+;; Exact function imports use 0x20.
+(module definition binary
+  "\00asm" "\01\00\00\00"
+  "\01"  ;; Type section id
+  "\04"  ;; Type section length
+  "\01"  ;; Types vector length
+  "\60"  ;; Function
+  "\00"  ;; Number of params
+  "\00"  ;; Number of results
+  "\02"  ;; Import section id
+  "\05"  ;; Import section length
+  "\01"  ;; Import vector length
+  "\00"  ;; Module name length
+  "\00"  ;; Base name length
+  "\20"  ;; Exact function
+  "\00"  ;; Type index
+)
+
+;; 0x20 is malformed in exports.
+(assert_malformed
+  (module binary
+    "\00asm" "\01\00\00\00"
+    "\01"  ;; Type section id
+    "\04"  ;; Type section length
+    "\01"  ;; Types vector length
+    "\60"  ;; Function
+    "\00"  ;; Number of params
+    "\00"  ;; Number of results
+    "\03"  ;; Function section id
+    "\02"  ;; Function section length
+    "\01"  ;; Function vector length
+    "\00"  ;; Type index
+    "\07"  ;; Export section id
+    "\04"  ;; Export section length
+    "\01"  ;; Export vector length
+    "\00"  ;; Name length
+    "\20"  ;; Exact func (malformed)
+    "\00"  ;; Function index
+    "\0a"  ;; Code section
+    "\04"  ;; Code section length
+    "\01"  ;; Code vector length
+    "\02"  ;; Function length
+    "\00"  ;; Type index
+    "\0b"  ;; End
+  )
+  "malformed export kind"
+)