diff --git a/testdata/examples/append_log/append_log.gold.v b/testdata/examples/append_log/append_log.gold.v
index 45893c39..62c4f0af 100644
--- a/testdata/examples/append_log/append_log.gold.v
+++ b/testdata/examples/append_log/append_log.gold.v
@@ -18,6 +18,17 @@ Definition Log : go_type := structT [
   "diskSz" :: uint64T
 ].
 
+Definition Log__mset : list (string * val) := [
+  ("mkHdr", Log__mkHdr)
+  ("writeHdr", Log__writeHdr)
+  ("get", Log__get)
+  ("Get", Log__Get)
+  ("append", Log__append)
+  ("Append", Log__Append)
+  ("reset", Log__reset)
+  ("Reset", Log__Reset)
+].
+
 Definition Log__mkHdr : val :=
   rec: "Log__mkHdr" "log" <> :=
     exception_do (let: "log" := ref_ty ptrT "log" in
diff --git a/testdata/examples/comments/comments.gold.v b/testdata/examples/comments/comments.gold.v
index 4afb2a48..7a2633b9 100644
--- a/testdata/examples/comments/comments.gold.v
+++ b/testdata/examples/comments/comments.gold.v
@@ -21,4 +21,7 @@ Definition Foo : go_type := structT [
   "a" :: boolT
 ].
 
+Definition Foo__mset : list (string * val) := [
+].
+
 End code.
diff --git a/testdata/examples/logging2/logging2.gold.v b/testdata/examples/logging2/logging2.gold.v
index a8c9d5df..099681b0 100644
--- a/testdata/examples/logging2/logging2.gold.v
+++ b/testdata/examples/logging2/logging2.gold.v
@@ -26,6 +26,21 @@ Definition Log : go_type := structT [
   "logTxnNxt" :: ptrT
 ].
 
+Definition Log__mset : list (string * val) := [
+  ("writeHdr", Log__writeHdr)
+  ("readHdr", Log__readHdr)
+  ("readBlocks", Log__readBlocks)
+  ("Read", Log__Read)
+  ("memWrite", Log__memWrite)
+  ("memAppend", Log__memAppend)
+  ("readLogTxnNxt", Log__readLogTxnNxt)
+  ("diskAppendWait", Log__diskAppendWait)
+  ("Append", Log__Append)
+  ("writeBlocks", Log__writeBlocks)
+  ("diskAppend", Log__diskAppend)
+  ("Logger", Log__Logger)
+].
+
 Definition Log__writeHdr : val :=
   rec: "Log__writeHdr" "log" "len" :=
     exception_do (let: "log" := ref_ty Log "log" in
@@ -252,6 +267,12 @@ Definition Txn : go_type := structT [
   "blks" :: mapT uint64T (sliceT byteT)
 ].
 
+Definition Txn__mset : list (string * val) := [
+  ("Write", Txn__Write)
+  ("Read", Txn__Read)
+  ("Commit", Txn__Commit)
+].
+
 (* XXX wait if cannot reserve space in log *)
 Definition Begin : val :=
   rec: "Begin" "log" :=
diff --git a/testdata/examples/semantics/semantics.gold.v b/testdata/examples/semantics/semantics.gold.v
index a6660dc5..b88ced2d 100644
--- a/testdata/examples/semantics/semantics.gold.v
+++ b/testdata/examples/semantics/semantics.gold.v
@@ -11,6 +11,9 @@ From New Require Import disk_prelude.
 Definition unit : go_type := structT [
 ].
 
+Definition unit__mset : list (string * val) := [
+].
+
 Definition findKey : val :=
   rec: "findKey" "m" :=
     exception_do (let: "m" := ref_ty (mapT uint64T unit) "m" in
@@ -324,6 +327,10 @@ Definition Enc : go_type := structT [
   "p" :: sliceT byteT
 ].
 
+Definition Enc__mset : list (string * val) := [
+  ("consume", Enc__consume)
+].
+
 Definition Enc__consume : val :=
   rec: "Enc__consume" "e" "n" :=
     exception_do (let: "e" := ref_ty ptrT "e" in
@@ -342,6 +349,10 @@ Definition Dec : go_type := structT [
   "p" :: sliceT byteT
 ].
 
+Definition Dec__mset : list (string * val) := [
+  ("consume", Dec__consume)
+].
+
 Definition Dec__consume : val :=
   rec: "Dec__consume" "d" "n" :=
     exception_do (let: "d" := ref_ty ptrT "d" in
@@ -488,6 +499,10 @@ Definition Editor : go_type := structT [
   "next_val" :: uint64T
 ].
 
+Definition Editor__mset : list (string * val) := [
+  ("AdvanceReturn", Editor__AdvanceReturn)
+].
+
 (* advances the array editor, and returns the value it wrote, storing
    "next" in next_val *)
 Definition Editor__AdvanceReturn : val :=
@@ -521,6 +536,9 @@ Definition Pair : go_type := structT [
   "y" :: uint64T
 ].
 
+Definition Pair__mset : list (string * val) := [
+].
+
 (* tests *)
 Definition failing_testFunctionOrdering : val :=
   rec: "failing_testFunctionOrdering" <> :=
@@ -638,6 +656,9 @@ Definition testU32Len : val :=
 
 Definition Uint32 : go_type := uint32T.
 
+Definition Uint32__mset : list (string * val) := [
+].
+
 (* https://github.com/tchajed/goose/issues/14 *)
 Definition failing_testU32NewtypeLen : val :=
   rec: "failing_testU32NewtypeLen" <> :=
@@ -651,6 +672,9 @@ Definition failing_testU32NewtypeLen : val :=
 
 Definition geometryInterface : go_type := interfaceT.
 
+Definition geometryInterface__mset : list (string * val) := [
+].
+
 Definition measureArea : val :=
   rec: "measureArea" "t" :=
     exception_do (let: "t" := ref_ty geometryInterface "t" in
@@ -675,6 +699,11 @@ Definition SquareStruct : go_type := structT [
   "Side" :: uint64T
 ].
 
+Definition SquareStruct__mset : list (string * val) := [
+  ("Square", SquareStruct__Square)
+  ("Volume", SquareStruct__Volume)
+].
+
 Definition SquareStruct__Square : val :=
   rec: "SquareStruct__Square" "t" <> :=
     exception_do (let: "t" := ref_ty SquareStruct "t" in
@@ -813,6 +842,10 @@ Definition LoopStruct : go_type := structT [
   "loopNext" :: ptrT
 ].
 
+Definition LoopStruct__mset : list (string * val) := [
+  ("forLoopWait", LoopStruct__forLoopWait)
+].
+
 Definition LoopStruct__forLoopWait : val :=
   rec: "LoopStruct__forLoopWait" "ls" "i" :=
     exception_do (let: "ls" := ref_ty LoopStruct "ls" in
@@ -1498,6 +1531,9 @@ Definition BoolTest : go_type := structT [
   "fc" :: uint64T
 ].
 
+Definition BoolTest__mset : list (string * val) := [
+].
+
 Definition CheckTrue : val :=
   rec: "CheckTrue" "b" :=
     exception_do (let: "b" := ref_ty ptrT "b" in
@@ -1592,6 +1628,10 @@ Definition ArrayEditor : go_type := structT [
   "next_val" :: uint64T
 ].
 
+Definition ArrayEditor__mset : list (string * val) := [
+  ("Advance", ArrayEditor__Advance)
+].
+
 Definition ArrayEditor__Advance : val :=
   rec: "ArrayEditor__Advance" "ae" "arr" "next" :=
     exception_do (let: "ae" := ref_ty ptrT "ae" in
@@ -1783,10 +1823,18 @@ Definition Bar : go_type := structT [
   "b" :: uint64T
 ].
 
+Definition Bar__mset : list (string * val) := [
+  ("mutate", Bar__mutate)
+].
+
 Definition Foo : go_type := structT [
   "bar" :: Bar
 ].
 
+Definition Foo__mset : list (string * val) := [
+  ("mutateBar", Foo__mutateBar)
+].
+
 Definition Bar__mutate : val :=
   rec: "Bar__mutate" "bar" <> :=
     exception_do (let: "bar" := ref_ty ptrT "bar" in
@@ -1823,12 +1871,23 @@ Definition TwoInts : go_type := structT [
   "y" :: uint64T
 ].
 
+Definition TwoInts__mset : list (string * val) := [
+].
+
 Definition S : go_type := structT [
   "a" :: uint64T;
   "b" :: TwoInts;
   "c" :: boolT
 ].
 
+Definition S__mset : list (string * val) := [
+  ("readA", S__readA)
+  ("readB", S__readB)
+  ("readBVal", S__readBVal)
+  ("updateBValX", S__updateBValX)
+  ("negateC", S__negateC)
+].
+
 Definition NewS : val :=
   rec: "NewS" <> :=
     exception_do (return: (ref_ty S (struct.make S [{
@@ -1992,6 +2051,9 @@ Definition StructWrap : go_type := structT [
   "i" :: uint64T
 ].
 
+Definition StructWrap__mset : list (string * val) := [
+].
+
 Definition testStoreInStructVar : val :=
   rec: "testStoreInStructVar" <> :=
     exception_do (let: "p" := ref_ty StructWrap (struct.make StructWrap [{
@@ -2040,6 +2102,9 @@ Definition StructWithFunc : go_type := structT [
   "fn" :: funcT
 ].
 
+Definition StructWithFunc__mset : list (string * val) := [
+].
+
 Definition testStructFieldFunc : val :=
   rec: "testStructFieldFunc" <> :=
     exception_do (let: "a" := ref_ty ptrT (zero_val ptrT) in
@@ -2095,6 +2160,17 @@ Definition Log : go_type := structT [
   "length" :: ptrT
 ].
 
+Definition Log__mset : list (string * val) := [
+  ("lock", Log__lock)
+  ("unlock", Log__unlock)
+  ("BeginTxn", Log__BeginTxn)
+  ("Read", Log__Read)
+  ("Size", Log__Size)
+  ("Write", Log__Write)
+  ("Commit", Log__Commit)
+  ("Apply", Log__Apply)
+].
+
 Definition intToBlock : val :=
   rec: "intToBlock" "a" :=
     exception_do (let: "a" := ref_ty uint64T "a" in
diff --git a/testdata/examples/simpledb/simpledb.gold.v b/testdata/examples/simpledb/simpledb.gold.v
index 911dda4c..d44f3738 100644
--- a/testdata/examples/simpledb/simpledb.gold.v
+++ b/testdata/examples/simpledb/simpledb.gold.v
@@ -26,6 +26,9 @@ Definition Table : go_type := structT [
   "File" :: fileT
 ].
 
+Definition Table__mset : list (string * val) := [
+].
+
 (* CreateTable creates a new, empty table. *)
 Definition CreateTable : val :=
   rec: "CreateTable" "p" :=
@@ -53,6 +56,9 @@ Definition Entry : go_type := structT [
   "Value" :: sliceT byteT
 ].
 
+Definition Entry__mset : list (string * val) := [
+].
+
 (* DecodeUInt64 is a Decoder(uint64)
 
    All decoders have the shape func(p []byte) (T, uint64)
@@ -127,6 +133,9 @@ Definition lazyFileBuf : go_type := structT [
   "next" :: sliceT byteT
 ].
 
+Definition lazyFileBuf__mset : list (string * val) := [
+].
+
 (* readTableIndex parses a complete table on disk into a key->offset index *)
 Definition readTableIndex : val :=
   rec: "readTableIndex" "f" "index" :=
@@ -260,6 +269,9 @@ Definition bufFile : go_type := structT [
   "buf" :: ptrT
 ].
 
+Definition bufFile__mset : list (string * val) := [
+].
+
 Definition newBuf : val :=
   rec: "newBuf" "f" :=
     exception_do (let: "f" := ref_ty fileT "f" in
@@ -316,6 +328,9 @@ Definition tableWriter : go_type := structT [
   "offset" :: ptrT
 ].
 
+Definition tableWriter__mset : list (string * val) := [
+].
+
 Definition newTableWriter : val :=
   rec: "newTableWriter" "p" :=
     exception_do (let: "p" := ref_ty stringT "p" in
@@ -427,6 +442,9 @@ Definition Database : go_type := structT [
   "compactionL" :: ptrT
 ].
 
+Definition Database__mset : list (string * val) := [
+].
+
 Definition makeValueBuffer : val :=
   rec: "makeValueBuffer" <> :=
     exception_do (let: "buf" := ref_ty (mapT uint64T (sliceT byteT)) (zero_val (mapT uint64T (sliceT byteT))) in
diff --git a/testdata/examples/unittest/unittest.gold.v b/testdata/examples/unittest/unittest.gold.v
index 37da6867..16f78272 100644
--- a/testdata/examples/unittest/unittest.gold.v
+++ b/testdata/examples/unittest/unittest.gold.v
@@ -15,6 +15,9 @@ From New Require Import disk_prelude.
 Definition importantStruct : go_type := structT [
 ].
 
+Definition importantStruct__mset : list (string * val) := [
+].
+
 (* doSubtleThings does a number of subtle things:
 
    (actually, it does nothing) *)
@@ -163,6 +166,9 @@ Definition elseIf : val :=
 
 Definition stringWrapper : go_type := stringT.
 
+Definition stringWrapper__mset : list (string * val) := [
+].
+
 Definition typedLiteral : val :=
   rec: "typedLiteral" <> :=
     exception_do (return: (#3);;;
@@ -374,6 +380,9 @@ Definition diskWrapper : go_type := structT [
   "d" :: disk.Disk
 ].
 
+Definition diskWrapper__mset : list (string * val) := [
+].
+
 Definition diskArgument : val :=
   rec: "diskArgument" "d" :=
     exception_do (let: "d" := ref_ty disk.Disk "d" in
@@ -400,6 +409,12 @@ Definition Enc : go_type := structT [
   "p" :: sliceT byteT
 ].
 
+Definition Enc__mset : list (string * val) := [
+  ("consume", Enc__consume)
+  ("UInt64", Enc__UInt64)
+  ("UInt32", Enc__UInt32)
+].
+
 Definition Enc__consume : val :=
   rec: "Enc__consume" "e" "n" :=
     exception_do (let: "e" := ref_ty ptrT "e" in
@@ -432,6 +447,12 @@ Definition Dec : go_type := structT [
   "p" :: sliceT byteT
 ].
 
+Definition Dec__mset : list (string * val) := [
+  ("consume", Dec__consume)
+  ("UInt64", Dec__UInt64)
+  ("UInt32", Dec__UInt32)
+].
+
 Definition Dec__consume : val :=
   rec: "Dec__consume" "d" "n" :=
     exception_do (let: "d" := ref_ty ptrT "d" in
@@ -470,10 +491,17 @@ Definition TakesFunctionType : val :=
 
 Definition Fooer : go_type := interfaceT.
 
+Definition Fooer__mset : list (string * val) := [
+].
+
 Definition concreteFooer : go_type := structT [
   "a" :: uint64T
 ].
 
+Definition concreteFooer__mset : list (string * val) := [
+  ("Foo", concreteFooer__Foo)
+].
+
 Definition concreteFooer__Foo : val :=
   rec: "concreteFooer__Foo" "f" <> :=
     exception_do (let: "f" := ref_ty ptrT "f" in
@@ -517,8 +545,14 @@ Definition useInts : val :=
 
 Definition my_u32 : go_type := uint32T.
 
+Definition my_u32__mset : list (string * val) := [
+].
+
 Definition also_u32 : go_type := my_u32.
 
+Definition also_u32__mset : list (string * val) := [
+].
+
 Definition ConstWithAbbrevType : expr := #(U32 3).
 
 (* literals.go *)
@@ -529,6 +563,9 @@ Definition allTheLiterals : go_type := structT [
   "b" :: boolT
 ].
 
+Definition allTheLiterals__mset : list (string * val) := [
+].
+
 Definition normalLiterals : val :=
   rec: "normalLiterals" <> :=
     exception_do (return: (struct.make allTheLiterals [{
@@ -594,6 +631,9 @@ Definition hasCondVar : go_type := structT [
   "cond" :: ptrT
 ].
 
+Definition hasCondVar__mset : list (string * val) := [
+].
+
 (* log_debugging.go *)
 
 Definition ToBeDebugged : val :=
@@ -856,8 +896,14 @@ Definition MapSize : val :=
 
 Definition IntWrapper : go_type := uint64T.
 
+Definition IntWrapper__mset : list (string * val) := [
+].
+
 Definition MapWrapper : go_type := mapT uint64T boolT.
 
+Definition MapWrapper__mset : list (string * val) := [
+].
+
 Definition MapTypeAliases : val :=
   rec: "MapTypeAliases" "m1" "m2" :=
     exception_do (let: "m2" := ref_ty MapWrapper "m2" in
@@ -1013,6 +1059,10 @@ Definition wrapExternalStruct : go_type := structT [
   "d" :: marshal.Dec
 ].
 
+Definition wrapExternalStruct__mset : list (string * val) := [
+  ("moveUint64", wrapExternalStruct__moveUint64)
+].
+
 Definition wrapExternalStruct__moveUint64 : val :=
   rec: "wrapExternalStruct__moveUint64" "w" <> :=
     exception_do (let: "w" := ref_ty wrapExternalStruct "w" in
@@ -1041,6 +1091,9 @@ Definition typing : go_type := structT [
   "proph" :: ProphIdT
 ].
 
+Definition typing__mset : list (string * val) := [
+].
+
 (* reassign.go *)
 
 Definition composite : go_type := structT [
@@ -1048,6 +1101,9 @@ Definition composite : go_type := structT [
   "b" :: uint64T
 ].
 
+Definition composite__mset : list (string * val) := [
+].
+
 Definition ReassignVars : val :=
   rec: "ReassignVars" <> :=
     exception_do (let: "x" := ref_ty uint64T (zero_val uint64T) in
@@ -1075,6 +1131,9 @@ Definition Block : go_type := structT [
   "Value" :: uint64T
 ].
 
+Definition Block__mset : list (string * val) := [
+].
+
 Definition Disk1 : expr := #0.
 
 Definition Disk2 : expr := #0.
@@ -1179,6 +1238,9 @@ Definition ReplicatedDiskRecover : val :=
 
 Definition SliceAlias : go_type := sliceT boolT.
 
+Definition SliceAlias__mset : list (string * val) := [
+].
+
 Definition sliceOps : val :=
   rec: "sliceOps" <> :=
     exception_do (let: "x" := ref_ty (sliceT uint64T) (zero_val (sliceT uint64T)) in
@@ -1211,10 +1273,17 @@ Definition thing : go_type := structT [
   "x" :: uint64T
 ].
 
+Definition thing__mset : list (string * val) := [
+].
+
 Definition sliceOfThings : go_type := structT [
   "things" :: sliceT thing
 ].
 
+Definition sliceOfThings__mset : list (string * val) := [
+  ("getThingRef", sliceOfThings__getThingRef)
+].
+
 Definition sliceOfThings__getThingRef : val :=
   rec: "sliceOfThings__getThingRef" "ts" "i" :=
     exception_do (let: "ts" := ref_ty sliceOfThings "ts" in
@@ -1315,6 +1384,11 @@ Definition Point : go_type := structT [
   "y" :: uint64T
 ].
 
+Definition Point__mset : list (string * val) := [
+  ("Add", Point__Add)
+  ("GetField", Point__GetField)
+].
+
 Definition Point__Add : val :=
   rec: "Point__Add" "c" "z" :=
     exception_do (let: "c" := ref_ty Point "c" in
@@ -1366,12 +1440,24 @@ Definition TwoInts : go_type := structT [
   "y" :: uint64T
 ].
 
+Definition TwoInts__mset : list (string * val) := [
+].
+
 Definition S : go_type := structT [
   "a" :: uint64T;
   "b" :: TwoInts;
   "c" :: boolT
 ].
 
+Definition S__mset : list (string * val) := [
+  ("readA", S__readA)
+  ("readB", S__readB)
+  ("readBVal", S__readBVal)
+  ("writeB", S__writeB)
+  ("negateC", S__negateC)
+  ("refC", S__refC)
+].
+
 Definition NewS : val :=
   rec: "NewS" <> :=
     exception_do (return: (ref_ty S (struct.make S [{
@@ -1469,10 +1555,16 @@ Definition sleep : val :=
 Definition A : go_type := structT [
 ].
 
+Definition A__mset : list (string * val) := [
+].
+
 Definition B : go_type := structT [
   "a" :: sliceT A
 ].
 
+Definition B__mset : list (string * val) := [
+].
+
 (* trailing_call.go *)
 
 Definition mkInt : val :=
@@ -1491,10 +1583,19 @@ Definition my_u64 : go_type := uint64T.
 
 Definition Timestamp : go_type := uint64T.
 
+Definition Timestamp__mset : list (string * val) := [
+].
+
 Definition UseTypeAbbrev : go_type := uint64T.
 
+Definition UseTypeAbbrev__mset : list (string * val) := [
+].
+
 Definition UseNamedType : go_type := Timestamp.
 
+Definition UseNamedType__mset : list (string * val) := [
+].
+
 Definition convertToAlias : val :=
   rec: "convertToAlias" <> :=
     exception_do (let: "x" := ref_ty uint64T (zero_val uint64T) in
diff --git a/testdata/examples/wal/wal.gold.v b/testdata/examples/wal/wal.gold.v
index 74221bd3..1153ca11 100644
--- a/testdata/examples/wal/wal.gold.v
+++ b/testdata/examples/wal/wal.gold.v
@@ -18,6 +18,17 @@ Definition Log : go_type := structT [
   "length" :: ptrT
 ].
 
+Definition Log__mset : list (string * val) := [
+  ("lock", Log__lock)
+  ("unlock", Log__unlock)
+  ("BeginTxn", Log__BeginTxn)
+  ("Read", Log__Read)
+  ("Size", Log__Size)
+  ("Write", Log__Write)
+  ("Commit", Log__Commit)
+  ("Apply", Log__Apply)
+].
+
 Definition intToBlock : val :=
   rec: "intToBlock" "a" :=
     exception_do (let: "a" := ref_ty uint64T "a" in