fix: mark exported stubs of `partial` definitions as unsafe

This PR fixes a soundness bug in the module system.
A `partial` definition lost its `partial` marking when it crossed a module boundary,
so downstream modules could use it from safe declarations.
Again, this issue can only be exploited using metaprogramming.

When a module exports a definition whose body stays private,
`addDeclCore` publishes an axiom stub in its place.
The stub's `isUnsafe` flag was computed as `defn.safety == .unsafe`,
which is false for `DefinitionSafety.partial`, so a `partial` definition
was summarized as an ordinary safe axiom.
The fix computes it as `defn.safety != .safe` instead.
4 files changed