PolyFun

Polynomial functors, interaction trees, and dependent interaction frameworks in Lean 4, generic substrate for protocol theory, PL semantics, and concurrent systems.

Status

PolyFun is a ready, buildable Lean 4 library. The repository builds without sorry or admit placeholders, and the public documentation reflects the current module layout and scope.

PolyFun originated as a wholesale extraction from Verified-zkEVM/VCVio.

Scope

PolyFun collects three layers of generic, domain-agnostic infrastructure that emerged from the cryptographic-protocols formalization in VCVio:

1. Polynomial functors and lenses. PFunctor cores (positions / directions), polynomial charts, lenses, equivalences, free monad FreeM, displayed FreeM, and the Cofree / M-type companion.
2. Interaction trees in the style of Xia, Zakowski, He, Hur, Malecha, Pierce, and Zdancewic (POPL 2020), modeled as the M-type of a one-step polynomial functor, with strong/weak bisimulation, simulation, handlers, and event signatures.
3. Generic interaction framework for sequential, two-party, multi-party, and concurrent interaction over a TypeTree polynomial substrate, with structural decoration, syntax/strategy/execution lenses, and an open-process layer for compositional reasoning.

Cryptographic content (probabilistic semantics, evaluation distributions, oracle simulation, security definitions) lives in Verified-zkEVM/VCVio and depends on this library.

Build

lake exe cache get
lake build

The repository pins Lean in lean-toolchain and pins Mathlib and cslib in lakefile.toml. Keep all three versions in sync.

Example

The following file defines a constant polynomial functor and checks one of its basic laws:

import PolyFun.PFunctor.Basic

open scoped PFunctor

#check PFunctor.C Nat

example : PFunctor.C PUnit = 1 := PFunctor.C_unit

Save it as Main.lean in the repository root and run:

lake env lean Main.lean

Documentation

• Generated API documentation: searchable documentation for public declarations.
• AGENTS.md, CLAUDE.md: one-screen guide for human and AI contributors. Symlinked.
• CONTRIBUTING.md: style, naming, attribution, and large- contribution policy.
• REFERENCES.md: the bibliography backing module docstrings.
• docs/wiki/: deeper agent-facing notes on the PFunctor substrate, interaction trees, the interaction framework, notation, and recurring gotchas.

License

Apache-2.0.