Update gold

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

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.

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" :=

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

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