proofgen: generate new definitions needed for initialization support (#65)

This PR adds generation of PkgInfo, PkgIsDefined, and PkgIsInitialized instances. It also shifts all the WpFuncCall and related instances to be based on is_pkg_defined to be systematic.

At the same time, we change `pkg_name'` to be the name of the package itself. There is some subtlety here: if a package has an identifier of the same name (e.g., package `raft` has a type `raft`, or package `main` has a function `main`), then it must be referenced with a package qualifier.

---------

Co-authored-by: Upamanyu Sharma <[email protected]>

Author: tchajed

glang/coq.go

@@ -899,6 +899,32 @@ func (d ConstDecl) DefName() (bool, string) {
 	return true, d.Name
 }
 
+type InstanceDecl struct {
+	Type Expr
+	// If not global, instance will be export
+	Global bool
+	Body   Expr
+	// Can be empty (instance gets an automatic name in Coq)
+	Name string
+}
+
+func (d InstanceDecl) CoqDecl() string {
+	var pp buffer
+	qualifier := "#[export]"
+	if d.Global {
+		qualifier = "#[global]"
+	}
+	pp.Add("%s Instance %s : %s :=",
+		qualifier, d.Name, d.Type.Coq(false))
+	pp.Indent(2)
+	pp.Add("%s.", d.Body.Coq(false))
+	return pp.Build()
+}
+
+func (d InstanceDecl) DefName() (bool, string) {
+	return true, d.Name
+}
+
 type AxiomDecl struct {
 	DeclName string
 	Type     Expr
@@ -989,6 +1015,32 @@ func (decls ImportDecls) PrintImports() string {
 	return strings.Join(ss, "\n")
 }
 
+type RecordField struct {
+	Name  string
+	Value Expr
+}
+
+// RecordLiteral represents a Gallina record literal
+type RecordLiteral struct {
+	Fields []RecordField
+}
+
+func (r RecordField) Coq(needs_paren bool) string {
+	return fmt.Sprintf("%s := %s", r.Name, r.Value.Coq(needs_paren))
+}
+
+func (r RecordLiteral) Coq(needs_paren bool) string {
+	var pp buffer
+	pp.AddLine("{|")
+	pp.Indent(2)
+	for _, field := range r.Fields {
+		pp.Add("%s;", field.Coq(false))
+	}
+	pp.Indent(-2)
+	pp.AddLine("|}")
+	return addParens(needs_paren, pp.Build())
+}
+
 // File represents a complete Coq file (a sequence of declarations).
 type File struct {
 	ImportHeader string

go.work.sum

@@ -21,6 +21,7 @@ golang.org/x/mod v0.21.0/go.mod h1:6SkKJ3Xj0I0BrPOZoBy3bdMptDDU9oJrpohJ3eWZ1fY=
 golang.org/x/net v0.27.0 h1:5K3Njcw06/l2y9vpGCSdcxWOYHOUk3dVNGDXN+FvAys=
 golang.org/x/net v0.27.0/go.mod h1:dDi0PyhWNoiUOrAS8uXv/vnScO4wnHQO4mj9fn/RytE=
 golang.org/x/net v0.30.0/go.mod h1:2wGyMJ5iFasEhkwi13ChkO/t1ECNC4X4eBKkVFyYFlU=
+golang.org/x/net v0.34.0 h1:Mb7Mrk043xzHgnRM88suvJFwzVrRfHEHJEl5/71CKw0=
 golang.org/x/net v0.34.0/go.mod h1:di0qlW3YNM5oh6GqDGQr92MyTozJPmybPK4Ev/Gm31k=
 golang.org/x/sys v0.26.0/go.mod h1:/VUhepiaJMQUp4+oa/7Zr1D23ma6VTLIYjOOTFZPUcA=
 golang.org/x/telemetry v0.0.0-20240521205824-bda55230c457 h1:zf5N6UOrA487eEFacMePxjXAJctxKmyjKUsjA11Uzuk=

goose.go

@@ -32,6 +32,16 @@ type Ctx struct {
 	namesToTranslate map[string]bool
 	info             *types.Info
 	pkgPath          string
+
+	// XXX: Initially tried using `pkg.Name` as the Gallina identifier holding
+	// the full package path, but that doesn't work in a `package main` with a `func main`.
+	// In that case, as soon as `func main` is defined inside `Module main.`,
+	// reference to simply `main` (which should be the go_string holding the
+	// package path) end up referring to the function. So, this uses `filename +
+	// "." + pkg.Name` to refer to the Gallina definition that holds a package's
+	// full path as a go_string (e.g. in `globals_test`, instead of `func_call #main ...`,
+	// this results in `func_call #globals_test.main ...`).
+	pkgIdent string
 	errorReporter
 
 	// XXX: this is so we can determine the expected return type when handling a
@@ -87,9 +97,12 @@ func getFfi(pkg *packages.Package) string {
 
 // NewPkgCtx initializes a context based on a properly loaded package
 func NewPkgCtx(pkg *packages.Package, filter declfilter.DeclFilter) Ctx {
+	ss := strings.Split(pkg.PkgPath, "/")
+	pkgIdent := ss[len(ss)-1]
 	return Ctx{
 		info:          pkg.TypesInfo,
 		pkgPath:       pkg.PkgPath,
+		pkgIdent:      pkgIdent + "." + pkg.Name,
 		errorReporter: newErrorReporter(pkg.Fset),
 		dep:           newDepTracker(),
 		importNames:   make(map[string]struct{}),
@@ -646,26 +659,28 @@ func (ctx *Ctx) qualifiedName(obj types.Object) string {
 }
 
 func (ctx *Ctx) getPkgAndName(obj types.Object) (pkg string, name string) {
+	if obj.Pkg() == nil {
+		ctx.unsupported(obj, "expected object to have package")
+	}
 	name = obj.Name()
-	pkg = "pkg_name'"
-	if obj.Pkg() == nil || ctx.pkgPath == obj.Pkg().Path() {
-		return
+	if obj.Pkg().Path() == ctx.pkgPath {
+		pkg = ctx.pkgIdent
+	} else {
+		pkg = obj.Pkg().Name()
 	}
-	pkg = obj.Pkg().Name() + "." + pkg
 	return
 }
 
 func (ctx *Ctx) selectorExprAddr(e *ast.SelectorExpr) glang.Expr {
 	selection := ctx.info.Selections[e]
 	if selection == nil {
-		pkg, ok := getIdent(e.X)
+		pkgName, ok := getIdent(e.X)
 		if !ok {
 			ctx.unsupported(e, "expected package selector with idtent, got %T", e.X)
 		}
 		if _, ok := ctx.info.ObjectOf(e.Sel).(*types.Var); ok {
-			ctx.dep.addDep("pkg_name'")
 			return glang.NewCallExpr(glang.GallinaIdent("globals.get"),
-				glang.StringVal{Value: glang.GallinaIdent(pkg + ".pkg_name'")},
+				glang.StringVal{Value: glang.GallinaIdent(pkgName)},
 				glang.StringVal{Value: glang.StringLiteral{Value: e.Sel.Name}},
 			)
 		} else {
@@ -858,7 +873,7 @@ func (ctx *Ctx) selectorExpr(e *ast.SelectorExpr) glang.Expr {
 				ctx.info.TypeOf(e),
 				glang.NewCallExpr(
 					glang.GallinaIdent("func_call"),
-					glang.StringVal{Value: glang.GallinaIdent(f.Pkg().Name() + ".pkg_name'")},
+					glang.StringVal{Value: glang.GallinaIdent(f.Pkg().Name())},
 					glang.StringVal{Value: glang.StringLiteral{Value: e.Sel.Name}},
 				),
 			)
@@ -1307,12 +1322,13 @@ func (ctx *Ctx) unaryExpr(e *ast.UnaryExpr, isSpecial bool) glang.Expr {
 }
 
 func (ctx *Ctx) function(s *ast.Ident) glang.Expr {
-	ctx.dep.addDep("pkg_name'")
-
 	typeArgs := ctx.info.Instances[s].TypeArgs
 	if typeArgs.Len() == 0 {
+		if ctx.info.ObjectOf(s).Pkg().Path() != ctx.pkgPath {
+			ctx.nope(s, "expected function ident to refer to local function")
+		}
 		return glang.NewCallExpr(glang.GallinaIdent("func_call"),
-			glang.StringVal{Value: glang.GallinaIdent("pkg_name'")},
+			glang.StringVal{Value: glang.GallinaIdent(ctx.pkgIdent)},
 			glang.StringVal{Value: glang.StringLiteral{Value: s.Name}},
 		)
 	}
@@ -1904,9 +1920,14 @@ func (ctx *Ctx) exprAddr(e ast.Expr) glang.Expr {
 		obj := ctx.info.ObjectOf(e)
 		if _, ok := obj.(*types.Var); ok {
 			if obj.Pkg().Scope() == obj.Parent() {
-				ctx.dep.addDep("pkg_name'")
+				pkgIdent := ""
+				if obj.Pkg().Path() == ctx.pkgPath {
+					pkgIdent = ctx.pkgIdent
+				} else {
+					pkgIdent = obj.Pkg().Name()
+				}
 				return glang.NewCallExpr(glang.GallinaIdent("globals.get"),
-					glang.StringVal{Value: glang.GallinaIdent("pkg_name'")},
+					glang.StringVal{Value: glang.GallinaIdent(pkgIdent)},
 					glang.StringVal{Value: glang.StringLiteral{Value: e.Name}},
 				)
 			} else {
@@ -2827,12 +2848,6 @@ func (ctx *Ctx) decl(d ast.Decl) []glang.Decl {
 
 func (ctx *Ctx) initFunctions() []glang.Decl {
 	var decls = []glang.Decl{}
-	nameDecl := glang.ConstDecl{
-		Name: "pkg_name'",
-		Val:  glang.GallinaString(ctx.pkgPath),
-		Type: glang.GallinaIdent("go_string"),
-	}
-	decls = append(decls, nameDecl)
 
 	ctx.dep.setCurrentName("initialize'")
 	initFunc := glang.FuncDecl{Name: "initialize'"}
@@ -2882,6 +2897,33 @@ func (ctx *Ctx) initFunctions() []glang.Decl {
 	}
 	decls = append(decls, msetsDecl)
 
+	var imports glang.ListExpr
+	for _, impName := range ctx.importNamesOrdered {
+		imports = append(imports, glang.GallinaIdent(fmt.Sprintf("%s", impName)))
+	}
+	infoRecord := glang.RecordLiteral{
+		Fields: []glang.RecordField{
+			{Name: "pkg_vars",
+				Value: glang.GallinaIdent("vars'")},
+			{Name: "pkg_functions",
+				Value: glang.GallinaIdent("functions'")},
+			{Name: "pkg_msets",
+				Value: glang.GallinaIdent("msets'")},
+			{Name: "pkg_imported_pkgs",
+				Value: imports},
+		},
+	}
+
+	infoInstanceDecl := glang.InstanceDecl{
+		Type: glang.NewCallExpr(glang.GallinaIdent("PkgInfo"),
+			glang.GallinaIdent(ctx.pkgIdent),
+		),
+		Global: true,
+		Body:   infoRecord,
+		Name:   "info'", // no name required
+	}
+	decls = append(decls, infoInstanceDecl)
+
 	var e glang.Expr
 
 	// add all init() function bodies
@@ -2919,7 +2961,7 @@ InitLoop:
 				e = glang.NewDoSeq(
 					glang.StoreStmt{
 						Dst: glang.NewCallExpr(glang.GallinaIdent("globals.get"),
-							glang.StringVal{Value: glang.GallinaIdent("pkg_name'")},
+							glang.StringVal{Value: glang.GallinaIdent(ctx.pkgIdent)},
 							glang.StringVal{Value: glang.StringLiteral{Value: init.Lhs[i-1].Name()}},
 						),
 						X:  glang.IdentExpr(fmt.Sprintf("$r%d", i-1)),
@@ -2988,10 +3030,7 @@ InitLoop:
 
 	e = glang.NewCallExpr(glang.GallinaIdent("exception_do"), e)
 	e = glang.NewCallExpr(glang.GallinaIdent("globals.package_init"),
-		glang.GallinaIdent("pkg_name'"),
-		glang.GallinaIdent("vars'"),
-		glang.GallinaIdent("functions'"),
-		glang.GallinaIdent("msets'"),
+		glang.GallinaIdent(ctx.pkgIdent),
 		glang.FuncLit{Args: nil, Body: e},
 	)
 

interface.go

@@ -240,6 +240,7 @@ func translatePackage(pkg *packages.Package, configContents []byte) (glang.File,
 
 func (ctx *Ctx) ffiHeaderFooter(pkg *packages.Package) (header string, footer string) {
 	ffi := getFfi(pkg)
+	header += fmt.Sprintf("Definition %s : go_string := \"%s\".\n\n", pkg.Name, pkg.PkgPath)
 	if ffi == "none" {
 		header += fmt.Sprintf("Module %s.\n", pkg.Name)
 		header += "Section code.\n" +

proofgen/imports.go

@@ -42,7 +42,7 @@ func (tr *importsTranslator) Decl(d ast.Decl) {
 	}
 }
 
-func translateImports(w io.Writer, pkg *packages.Package, usingFfi bool, ffi string, filter declfilter.DeclFilter) {
+func translateImports(w io.Writer, pkg *packages.Package, usingFfi bool, ffi string, filter declfilter.DeclFilter) *importsTranslator {
 	tr := &importsTranslator{
 		importsSet: make(map[string]struct{}),
 		filter:     filter,
@@ -55,4 +55,5 @@ func translateImports(w io.Writer, pkg *packages.Package, usingFfi bool, ffi str
 	for _, imp := range tr.importsList {
 		fmt.Fprintf(w, "Require Export New.generatedproof.%s.\n", imp)
 	}
+	return tr
 }

proofgen/names.go

@@ -96,10 +96,13 @@ Class GlobalAddrs :=
 	}
 	fmt.Fprintln(w, "\n  ].")
 
-	// emit `is_defined`
+	// emit `PkgIsDefined instance`
 	fmt.Fprintf(w, `
-Definition is_defined := is_global_definitions %s.pkg_name' var_addrs %s.functions' %s.msets'.
-`, pkg.Name, pkg.Name, pkg.Name)
+Global Instance is_pkg_defined_instance : IsPkgDefined %s :=
+{|
+  is_pkg_defined := is_global_definitions %s var_addrs;
+|}.
+`, pkg.Name, pkg.Name)
 
 	// emit `own_allocated`
 	fmt.Fprint(w, "\nDefinition own_allocated `{!GlobalAddrs} : iProp Σ :=\n")
@@ -121,7 +124,7 @@ Definition is_defined := is_global_definitions %s.pkg_name' var_addrs %s.functio
 	// emit instances for global.get
 	for _, varName := range tr.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, "  WpGlobalsGet %s \"%s\" %s (is_pkg_defined %s).\n", pkg.Name, varName, varName, pkg.Name)
 		fmt.Fprintf(w, "Proof. apply wp_globals_get'. reflexivity. Qed.\n")
 	}
 
@@ -131,7 +134,7 @@ Definition is_defined := is_global_definitions %s.pkg_name' var_addrs %s.functio
 			continue
 		}
 		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, "  WpFuncCall %s \"%s\" _ (is_pkg_defined %s) :=\n", pkg.Name, funcName, pkg.Name)
 		fmt.Fprintf(w, "  ltac:(apply wp_func_call'; reflexivity).\n")
 	}
 
@@ -147,8 +150,8 @@ Definition is_defined := is_global_definitions %s.pkg_name' var_addrs %s.functio
 			}
 
 			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, "  WpMethodCall %s \"%s\" \"%s\" _ (is_pkg_defined %s) :=\n",
+				pkg.Name, typeName, methodName, pkg.Name)
 			fmt.Fprintf(w, "  ltac:(apply wp_method_call'; reflexivity).\n")
 			// 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
@@ -164,8 +167,8 @@ Definition is_defined := is_global_definitions %s.pkg_name' var_addrs %s.functio
 			}
 
 			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, "  WpMethodCall %s \"%s\" \"%s\" _ (is_pkg_defined %s) :=\n",
+				pkg.Name, typeName, methodName, pkg.Name)
 			fmt.Fprintf(w, "  ltac:(apply wp_method_call'; reflexivity).\n")
 		}
 	}

proofgen/proofgen.go

@@ -11,7 +11,7 @@ import (
 )
 
 func Package(w io.Writer, pkg *packages.Package, usingFfi bool, ffi string, filter declfilter.DeclFilter) {
-	fmt.Fprintf(w, "(* autogenerated by goose proofgen (types); do not modify *)\n")
+	fmt.Fprintf(w, "(* autogenerated by goose proofgen; do not modify *)\n")
 
 	if usingFfi {
 		fmt.Fprintf(w, "Require Export New.proof.%s_prelude.\n", ffi)
@@ -26,8 +26,8 @@ func Package(w io.Writer, pkg *packages.Package, usingFfi bool, ffi string, filt
 
 	translateImports(w, pkg, usingFfi, ffi, filter)
 
-	fmt.Fprintf(w, "Require Export New.code.%s.\n", coqPath)
 	fmt.Fprintf(w, "Require Export New.golang.theory.\n\n")
+	fmt.Fprintf(w, "Require Export New.code.%s.\n", coqPath)
 
 	fmt.Fprintf(w, "Module %s.\n", pkg.Name)
 

proofgen/types.go

@@ -241,7 +241,7 @@ Context `+"`"+`{!ffi_model, !ffi_semantics _ _, !ffi_interp _, !heapGS Σ}.
 		fmt.Fprintf(w, "%s\n      \"%s\" ::= #%s", sep, getFieldName(i), toCoqName(getFieldName(i)))
 		sep = ";"
 	}
-	fmt.Fprint(w, "\n    ]))%%V\n    #(")
+	fmt.Fprintf(w, "%s", "\n    ]))"+`%struct`+"\n    #(")
 	fmt.Fprintf(w, "%s.mk", name)
 	for i := 0; i < s.NumFields(); i++ {
 		fmt.Fprintf(w, " %s", toCoqName(getFieldName(i)))
@@ -341,7 +341,7 @@ func translateTypes(w io.Writer, pkg *packages.Package, usingFfi bool, ffi strin
 		for _, depName := range tr.deps[n] {
 			printDefAndDeps(depName)
 		}
-		fmt.Fprintf(w, tr.defs[n])
+		fmt.Fprint(w, tr.defs[n])
 		printed[n] = true
 	}
 	for _, d := range tr.defNames {