proofgen: generate new definitions needed for initialization support #65
Conversation
proofgen/imports.go
Outdated
| return pkgPath[i+1:] | ||
| } | ||
|
|
||
| func (tr *importsTranslator) translateImportList(w io.Writer, pkg *packages.Package) { |
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
(e.g. etcd's `raft` package has a type `raft` that conflicts with the package name)
This PR adds new typeclasses `PkgIsInitialized pkg_name` and `PkgIsDefined pkg_nam` that associate a package with its "initialization" and "definenedness" predicate, respectively. The latter is already automatically generated, while the former is defined in manual proofs but in the absence of global variables or initialization functions consists of `is_defined` for that package and is_initialized for all imported packages. The instances of these typeclasses essentially register a predicate to a package name, accessed via `is_pkg_init` and `is_pkg_defined`. This PR also adds a new `PkgInfo` typeclass, which is used to get the information that constructs `is_defined` and the list of imports. This PR depends on goose-lang/goose#65 to create new instances and definitions. These typeclasses permit some useful automation of initialization predicates, most of which is included here: - The tactic `basic_pkg_init` defines an initialization predicate. - `wp_apply` automatically proves any pkg_init preconditions it finds from any found in the persistent context. - A new `wp_start` tactic automatically introduces the initialization predicate and names only the remaining hypotheses according to the user pattern. --------- Co-authored-by: Upamanyu Sharma <[email protected]>
This PR adds generation of
PkgIsDefinedinstances and a new definitionimported_pkgs, a list of packages whose initialization a package depends on. I also shifted all the WpFuncCall and related instances to be based onpkg_definedto be systematic.