module-system

Module Boundaries and the PolyFun Façade

This guide records the intended long-term boundary between PolyFun and VCVio under Lean's module system. It is the decision record for visibility, import all, and the OracleComp/PFunctor.FreeM relationship.

The normative language behavior is described by Lean's Source Files and Modules reference. In particular:

• a plain import exposes the dependency's public scope only in the importing module's private scope;
• a public import also re-exports that public scope;
• import all exposes the imported module's private scope;
• a public definition is opaque to importers unless its body is deliberately exposed; and
• the type of a public declaration may mention only public names.

Architectural decision

VCVio is a thin, opinionated façade over PolyFun, rather than either a second generic free-monad library or a sealed wrapper that hides PolyFun completely.

PolyFun owns domain-independent structure:

• polynomial functors, lenses, handlers, and PFunctor.FreeM;
• reusable handler transformations such as target lifting, before/after instrumentation, and writer tracing;
• interaction trees, observations, fairness predicates, processes, and UC structural laws; and
• public equations needed to reason about those abstractions without opening private definitions.

VCVio owns cryptographic specialization:

• OracleSpec, OracleQuery, OracleComp, QueryImpl, and established oracle notation;
• PMF/SPMF and support semantics, probability lemmas, uniform-oracle policy, query accounting, and program logic;
• cryptographic games, reductions, and examples; and
• compatibility names that keep existing oracle-facing developments stable.

Generic code should accept PFunctor, PFunctor.Handler, or PFunctor.FreeM directly. Oracle- and cryptography-facing code should use the VCVio names. OracleComp spec remains definitionally the free monad on spec.toPFunctor, and QueryImpl compatibility operations are thin aliases of the generic handler operations.