Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

proofgen: generate new definitions needed for initialization support #65

Merged
merged 17 commits into from
Mar 7, 2025
Merged

proofgen: generate new definitions needed for initialization support #65

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
97a6eed
checkpoint
tchajed Mar 4, 2025
d58f6fe
Generate list of imported packages
tchajed Mar 5, 2025
aa4b8da
Generate PkgInfo definition
tchajed Mar 5, 2025
b43d2a8
Update gold
tchajed Mar 6, 2025
4f13685
Use PkgInfo in globals.package_init
tchajed Mar 6, 2025
89d2a1d
Rename pkg_defined
tchajed Mar 6, 2025
31e5cb6
Use new is_global_definitions
tchajed Mar 6, 2025
605ae05
Update gold
tchajed Mar 6, 2025
c565b63
Directly emit a `PkgInfo` instance, without an intermediate record
upamanyus Mar 6, 2025
e6cbc32
Update gold
upamanyus Mar 6, 2025
a4c18de
Generate `IsPkgDefined` instance directly without intermediate `is_de…
upamanyus Mar 7, 2025
942f78f
Remove `pkg_name'`
upamanyus Mar 7, 2025
963804b
Note a subtlety, which will probably become a problem again later
upamanyus Mar 7, 2025
62bff35
Update gold
upamanyus Mar 7, 2025
86e9881
`make fix`
upamanyus Mar 7, 2025
84a4b8b
Handle emitting qualified Gallina ident for local package
upamanyus Mar 7, 2025
148e5d4
Update gold
upamanyus Mar 7, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions go.work.sum
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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=
Expand Down
27 changes: 26 additions & 1 deletion proofgen/imports.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand All @@ -55,4 +55,29 @@ 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
}

func importPackageIdentifier(pkgPath string) string {
i := strings.LastIndex(pkgPath, ".")
if i < 0 {
return pkgPath
}
return pkgPath[i+1:]
}

func (tr *importsTranslator) translateImportList(w io.Writer, pkg *packages.Package) {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

At some point, it might be better to emit a list of imported packages in the trusted Goose translation, which would eliminate the need for this. The Go code's translation currently inlines calls to importA.initialize', importB.initialize' and so forth into the current package's initialize function, which prevents any abstraction in Coq about the import phase of initializing a package.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The list of imported packages is now in trusted code. Initialization uses globals.package_init which now takes most of its parameters through the PkgInfo class, but the translator still produces a function that calls all the dependencies - as with is_defined, abstracting this out is hard since we would need the PkgInfo of every dependent package and this isn't easy to abstract over.

fmt.Fprintf(w, "Definition imported_pkgs: list go_string := ")
if len(tr.importsList) == 0 {
fmt.Fprintf(w, "[].\n")
} else {
fmt.Fprintf(w, "[\n")
var lines []string
for _, imp := range tr.importsList {

lines = append(lines, fmt.Sprintf(" New.code.%s.%s.pkg_name'", imp, importPackageIdentifier(imp)))
}
fmt.Fprintf(w, strings.Join(lines, ";\n"))
fmt.Fprintf(w, "\n]%%go.\n")
}
}
15 changes: 10 additions & 5 deletions proofgen/names.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -100,6 +100,11 @@ Class GlobalAddrs :=
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 `is_pkg_defined`
fmt.Fprintf(w, `
Global Instance is_pkg_defined : PkgIsDefined %s.pkg_name' is_defined :=
ltac:(prove_pkg_is_defined).
`, pkg.Name)

// emit `own_allocated`
fmt.Fprint(w, "\nDefinition own_allocated `{!GlobalAddrs} : iProp Σ :=\n")
Expand Down Expand Up @@ -131,7 +136,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.pkg_name' \"%s\" _ (pkg_defined %s.pkg_name') :=\n", pkg.Name, funcName, pkg.Name)
fmt.Fprintf(w, " ltac:(apply wp_func_call'; reflexivity).\n")
}

Expand All @@ -147,8 +152,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.pkg_name' \"%s\" \"%s\" _ (pkg_defined %s.pkg_name') :=\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
Expand All @@ -164,8 +169,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.pkg_name' \"%s\" \"%s\" _ (pkg_defined %s.pkg_name') :=\n",
pkg.Name, typeName, methodName, pkg.Name)
fmt.Fprintf(w, " ltac:(apply wp_method_call'; reflexivity).\n")
}
}
Expand Down
4 changes: 3 additions & 1 deletion proofgen/proofgen.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,13 +24,15 @@ func Package(w io.Writer, pkg *packages.Package, usingFfi bool, ffi string, filt
fmt.Fprintf(w, "Require Export New.manualproof.%s.\n", coqPath)
}

translateImports(w, pkg, usingFfi, ffi, filter)
tr := 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, "Module %s.\n", pkg.Name)

tr.translateImportList(w, pkg)

translateTypes(w, pkg, usingFfi, ffi, filter)
translateNames(w, pkg, usingFfi, ffi, filter)
fmt.Fprintf(w, "End %s.\n", pkg.Name)
Expand Down