diff --git a/namegen/namegen.go b/namegen/namegen.go
new file mode 100644
index 0000000..15a1825
--- /dev/null
+++ b/namegen/namegen.go
@@ -0,0 +1,135 @@
+package namegen
+
+import (
+	"fmt"
+	"go/ast"
+	"go/token"
+	"go/types"
+	"io"
+	"strings"
+
+	"github.com/goose-lang/goose/glang"
+	"golang.org/x/tools/go/packages"
+)
+
+type Ctx struct {
+	varNames   []string
+	functions  []string
+	namedTypes []*types.Named
+
+	info *types.Info
+}
+
+func (ctx *Ctx) Decl(d ast.Decl) {
+	switch d := d.(type) {
+	case *ast.GenDecl:
+		switch d.Tok {
+		case token.VAR:
+			for _, spec := range d.Specs {
+				s := spec.(*ast.ValueSpec)
+				for _, name := range s.Names {
+					ctx.varNames = append(ctx.varNames, name.Name)
+				}
+			}
+		case token.TYPE:
+			for _, spec := range d.Specs {
+				spec := spec.(*ast.TypeSpec)
+				if t, ok := ctx.info.TypeOf(spec.Name).(*types.Named); ok {
+					if _, ok := t.Underlying().(*types.Interface); !ok {
+						ctx.namedTypes = append(ctx.namedTypes, t)
+					}
+				}
+			}
+		}
+	case *ast.FuncDecl:
+		if d.Recv == nil {
+			ctx.functions = append(ctx.functions, d.Name.Name)
+		} else {
+		}
+	case *ast.BadDecl:
+	default:
+	}
+}
+
+func Package(w io.Writer, pkg *packages.Package) {
+	fmt.Fprintf(w, "(* autogenerated by namegen; do not modify *)\n")
+
+	coqPath := strings.ReplaceAll(glang.ThisIsBadAndShouldBeDeprecatedGoPathToCoqPath(pkg.PkgPath), "/", ".")
+	fmt.Fprintf(w, "From New.code Require Import %s.\n", coqPath)
+	fmt.Fprintf(w, "From New.golang Require Import theory.\n\n")
+
+	ctx := &Ctx{info: pkg.TypesInfo}
+
+	for _, f := range pkg.Syntax {
+		for _, d := range f.Decls {
+			ctx.Decl(d)
+		}
+	}
+
+	fmt.Fprintf(w, "Module %s.\nSection defs.", pkg.Name)
+	// emit record for global addrs
+	fmt.Fprintf(w, `Class GlobalAddrs :=
+{
+`)
+	for _, varName := range ctx.varNames {
+		fmt.Fprintf(w, "  %s : loc;\n", varName)
+	}
+	fmt.Fprint(w, "}.\n\n")
+	fmt.Fprint(w, "Context `{!GlobalAddrs}.\n\n")
+
+	// emit `var_addrs` which converts GlobalAddrs into alist
+	fmt.Fprint(w, "Definition var_addrs `{!GlobalAddrs} : list (go_string * loc) := [")
+	sep := ""
+	for _, varName := range ctx.varNames {
+		fmt.Fprintf(w, "%s\n    (\"%s\"%%go, %s)", sep, varName, varName)
+		sep = ";"
+	}
+	fmt.Fprintln(w, "\n  ].")
+
+	// emit `is_defined`
+	fmt.Fprintf(w, `
+Definition is_defined := is_global_definitions %s.pkg_name' var_addrs %s.functions' %s.msets'.
+`, pkg.Name, pkg.Name, pkg.Name)
+
+	// emit instances for global.get
+	for _, varName := range ctx.varNames {
+		fmt.Fprintf(w, "\nGlobal Instance wp_globals_get_%s : \n", varName)
+		fmt.Fprintf(w, "  WpGlobalsGet %s.pkg_name' \"%s\" %s is_defined.\n", pkg.Name, varName, varName)
+		fmt.Fprintf(w, "Proof. apply wp_globals_get'. reflexivity. Qed.\n")
+	}
+
+	// emit instances for unfolding func_call
+	for _, funcName := range ctx.functions {
+		fmt.Fprintf(w, "\nGlobal Instance wp_func_call_%s : \n", funcName)
+		fmt.Fprintf(w, "  WpFuncCall %s.pkg_name' \"%s\" _ is_defined :=\n", pkg.Name, funcName)
+		fmt.Fprintf(w, "  ltac:(apply wp_func_call'; reflexivity).\n")
+	}
+
+	// emit instances for unfolding method_call
+	for _, namedType := range ctx.namedTypes {
+		typeName := namedType.Obj().Name()
+		goMset := types.NewMethodSet(namedType)
+		for i := range goMset.Len() {
+			methodName := goMset.At(i).Obj().Name()
+			fmt.Fprintf(w, "\nGlobal Instance wp_method_call_%s_%s : \n", typeName, methodName)
+			fmt.Fprintf(w, "  WpMethodCall %s.pkg_name' \"%s\" \"%s\" _ is_defined.\n",
+				pkg.Name, typeName, methodName)
+			// XXX: by using an ltac expression to generate the instance, we can
+			// leave an evar for the method val, avoiding the need to write out
+			// the promoted methods.
+			fmt.Fprintf(w, "  ltac:(apply wp_method_call'; reflexivity).\n")
+		}
+
+		typeName = namedType.Obj().Name() + "'ptr"
+		goMset = types.NewMethodSet(types.NewPointer(namedType))
+		for i := range goMset.Len() {
+			methodName := goMset.At(i).Obj().Name()
+			fmt.Fprintf(w, "\nGlobal Instance wp_method_call_%s_%s : \n", typeName, methodName)
+			fmt.Fprintf(w, "  WpMethodCall %s.pkg_name' \"%s\" \"%s\" _ is_defined.\n",
+				pkg.Name, typeName, methodName)
+			fmt.Fprintf(w, "  ltac:(apply wp_method_call'; reflexivity).\n")
+		}
+	}
+
+	fmt.Fprintf(w, "\nEnd defs.\nEnd %s.\n", pkg.Name)
+}