feat: define VCVio’s public boundary over PolyFun

[dtumad]

Stack

• base: Migrate to Lean modules and update dependencies to v4.32.2 #510
• PolyFun dependency: feat: expose the public PFunctor module surface PolyFun#114 (134eca434dc21d692737f5daa2b05aa189ca2dfa)

This PR is intentionally stacked on the module-system migration so its diff is limited to the long-term PolyFun/VCVio boundary work.

Summary

• add generic PFunctor probability semantics in VCVio.EvalDist.PFunctor, with OracleComp delegating through the existing VCVio façade
• move query-handler instrumentation to PolyFun and retain thin QueryImpl aliases for VCVio consumers
• replace downstream reliance on PolyFun implementation imports with public laws, including interaction and UC clients
• document the intended boundary: expose foundational PFunctor concepts where they are useful, while keeping probability and cryptographic policy in VCVio
• add a compile-time façade canary and CI check that rejects import all PolyFun...
• pin the paired PolyFun draft commit so the stack is reproducible

Design direction

This takes a hybrid approach rather than making VCVio uniformly thinner or uniformly more opaque:

• generic free-monad operations and handler instrumentation belong in PolyFun
• VCVio should expose those concepts when they improve interoperability
• VCVio continues to own OracleSpec, OracleComp, probability-spec policy, notation, and compatibility aliases used by cryptographic developments
• downstream code should depend on public laws, not the reducibility of PolyFun internals

Validation

• lake build (3,007 jobs)
• lake build ToMathlib VCVio LatticeCrypto Extern HashSig Examples VCVioWidgets (9,214 jobs)
• scripts/check-polyfun-boundary.sh
• lake env lean VCVioTest/PFunctorFacade.lean
• lake env lean VCVioTest/Smoke.lean
• lake env lean LatticeCryptoTest/Falcon/Main.lean
• git diff --check

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Define VCVio’s public boundary over PolyFun

Failed to generate AI summary. Please check the per-file summaries and statistics below.

---

Statistics

Metric	Count
📝 Files Changed	35
✅ Lines Added	696
❌ Lines Removed	248

---

Lean Declarations

✏️ Removed: 12 declaration(s)

VCVio/Interaction/UC/StdDoBridge.lean (7)

• abbrev trivCtx : Interaction.TypeTree.Node.Context.{0, 0}
• def incrementProcess : ProcessOver ℕ trivCtx
• def trivSampler :
• private example (p₀ s₀ n : ℕ) :
• private theorem incrementProcess_step_triple (p₀ p : ℕ) :
• theorem samplePath_done (samp : Sampler m .done) :
• theorem samplePath_node {X : Type}

VCVio/OracleComp/EvalDist.lean (5)

• instance instLawfulMonadLiftTSetM : LawfulMonadLiftT (OracleComp spec) SetM where
• instance instMonadLiftTSetM : MonadLiftT (OracleComp spec) SetM where
• noncomputable instance instLawfulMonadLiftTPMF [IsProbabilitySpec spec] :
• noncomputable instance instMonadLiftTPMF [IsProbabilitySpec spec] :
• private lemma support_eq_SPMF_support (oa : OracleComp spec α) :

✏️ Added: 32 declaration(s)

VCVio/EvalDist/PFunctor.lean (10)

• instance instLawfulMonadLiftTSetM : LawfulMonadLiftT (FreeM P) SetM where
• instance instMonadLiftTSetM : MonadLiftT (FreeM P) SetM where
• noncomputable def IsUniformSpec.ofFintypeInhabited (P : PFunctor.{uA, u})
• noncomputable instance instLawfulMonadLiftTPMF [P.IsProbabilitySpec] :
• noncomputable instance instMonadLiftTPMF [P.IsProbabilitySpec] :
• theorem evalDist_eq_liftM [P.IsProbabilitySpec] (program : FreeM P α) :
• theorem evalDist_lift [P.IsProbabilitySpec] (operation : P.A) :
• theorem evalDist_lift_eq_uniform [h : P.IsUniformSpec] (operation : P.A) :
• theorem support_eq_liftM (program : FreeM P α) :
• theorem support_lift (operation : P.A) :

VCVio/Interaction/UC/StdDoBridge.lean (1)

• private example (p₀ s₀ n : ℕ) : True

VCVio/OracleComp/EvalDist.lean (4)

• abbrev IsProbabilitySpec (spec : OracleSpec ι)
• abbrev toPMF [IsProbabilitySpec spec] (t : spec.Domain) : PMF (spec.Range t)
• noncomputable def IsUniformSpec.toPFunctor [h : IsUniformSpec spec] :
• private lemma support_eq_evalDist_support :

VCVio/OracleComp/QueryTracking/CountingOracle.lean (2)

• lemma OracleSpec.countingOracle_apply [DecidableEq ι] (t : spec.Domain) :
• lemma costOracle_apply {ω : Type u} [Monoid ω] (costFn : spec.Domain → ω)

VCVio/OracleComp/QueryTracking/LoggingOracle.lean (1)

• theorem writerTMapBase_apply

VCVioTest/PFunctorFacade.lean (14)

• @[reducible] def boolOracleSpec : OracleSpec (Fin 1)
• @[reducible] def triPFunctor : PFunctor
• def directSample : PFunctor.FreeM triPFunctor (Fin 3)
• def zeroHandler : PFunctor.Handler Option triPFunctor
• example (program : OracleComp boolOracleSpec Bool) :
• example (program : OracleComp boolOracleSpec Bool) :
• example : EvalDistCompatible (PFunctor.FreeM triPFunctor)
• example : support directSample = Set.univ
• example : zeroHandler.postInsert (fun _ _ => some ()) () = some 0
• example : zeroHandler.preInsert (fun _ => some ()) () = some 0
• example : 𝒟[directSample] =
• example
• noncomputable example : PFunctor.IsProbabilitySpec boolOracleSpec.toPFunctor
• noncomputable example : PFunctor.IsUniformSpec boolOracleSpec.toPFunctor

✏️ Affected: 25 declaration(s) (line number changed)

• private def floatExpmP63 (x ccs : Float) : UInt64 in LatticeCrypto/Falcon/Concrete/FloatLike.lean moved from L95 to L95
• private def floatFloorInt64 (x : Float) : Int64 in LatticeCrypto/Falcon/Concrete/FloatLike.lean moved from L102 to L102
• private def floatOfInt32 (i : Int32) : Float in LatticeCrypto/Falcon/Concrete/FloatLike.lean moved from L90 to L90
• private def floatOfInt64 (i : Int64) : Float in LatticeCrypto/Falcon/Concrete/FloatLike.lean moved from L86 to L86
• private def floatRint (x : Float) : Int64 in LatticeCrypto/Falcon/Concrete/FloatLike.lean moved from L107 to L107
• private def floatScaled (i : Int64) (sc : Int32) : Float in LatticeCrypto/Falcon/Concrete/FloatLike.lean moved from L92 to L92
• private def checkFPR (st : IO.Ref TestState) (name : String) in LatticeCryptoTest/Falcon/Main.lean moved from L58 to L58
• private def flush : IO Unit in LatticeCryptoTest/Falcon/Main.lean moved from L63 to L63
• private def prngNextSalt (s : PRNGState) : Bytes 40 × PRNGState in LatticeCryptoTest/Falcon/Main.lean moved from L72 to L72
• private def testFalcon1024 : Params where in LatticeCryptoTest/Falcon/Main.lean moved from L42 to L42
• private def testFalcon512 : Params where in LatticeCryptoTest/Falcon/Main.lean moved from L35 to L35
• private def u64ToHex (v : UInt64) : String in LatticeCryptoTest/Falcon/Main.lean moved from L49 to L49
• instance instEvalDistCompatible : EvalDistCompatible (OracleComp spec) in VCVio/OracleComp/EvalDist.lean moved from L295 to L273
• abbrev withTrace (so : QueryImpl spec m) in VCVio/OracleComp/QueryTracking/Tracing.lean moved from L158 to L163
• abbrev withTraceAppend (so : QueryImpl spec m) in VCVio/OracleComp/QueryTracking/Tracing.lean moved from L315 to L330
• abbrev withTraceAppendBefore (so : QueryImpl spec m) (traceFn : spec.Domain → ω) : in VCVio/OracleComp/QueryTracking/Tracing.lean moved from L245 to L255
• abbrev withTraceBefore (so : QueryImpl spec m) (traceFn : spec.Domain → ω) : in VCVio/OracleComp/QueryTracking/Tracing.lean moved from L83 to L83
• lemma simulateQ_add_liftM_query_left (t : spec₁'.Domain) : in VCVio/OracleComp/SimSemantics/Append.lean moved from L62 to L64
• lemma simulateQ_add_liftM_query_right (t : spec₂'.Domain) : in VCVio/OracleComp/SimSemantics/Append.lean moved from L69 to L73
• @[simp] lemma ofLift_eq_id' : ofLift spec (OracleComp spec) = QueryImpl.id' spec in VCVio/OracleComp/SimSemantics/QueryImpl/Basic.lean moved from L144 to L150
• abbrev liftTarget (n : Type u → Type*) [MonadLiftT m n] in VCVio/OracleComp/SimSemantics/QueryImpl/Basic.lean moved from L83 to L83
• abbrev postInsert (so : QueryImpl spec m) {α} in VCVio/OracleComp/SimSemantics/QueryImpl/Constructions.lean moved from L260 to L256
• abbrev preInsert (so : QueryImpl spec m) (nx : spec.Domain → n α) : in VCVio/OracleComp/SimSemantics/QueryImpl/Constructions.lean moved from L93 to L90
• private abbrev VCSpecBackwardRuleCacheKey in VCVio/ProgramLogic/Tactics/Common/Backward.lean moved from L42 to L42
• private def valImage (c : Prob → Prop) : Set ℝ≥0∞ in VCVio/ProgramLogic/Unary/Loom/Probabilistic.lean moved from L113 to L113

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

The diff is largely compliant with the VCVio contributing guidelines. Below are observations organized by the categories emphasized in the instructions.

---

📄 **Per-File Summaries**

• LatticeCrypto/Falcon/Concrete/FloatLike.lean: The six helper functions floatOfInt64, floatOfInt32, floatScaled, floatExpmP63, floatFloorInt64, and floatRint were changed from def to private def, making them inaccessible outside this module. The instance : FloatLike Float was additionally annotated with @[no_expose], preventing it from being exported by the containing namespace. These changes restrict the public API of the file to only the FloatLike instance and its associated #check-style usage, while keeping the internal conversion and rounding helpers hidden.

• LatticeCryptoTest/Falcon/Main.lean: Made six definitions private to restrict their visibility to the current file: testFalcon512, testFalcon1024, u64ToHex, checkFPR, flush, and prngNextSalt. No other changes were made to the bodies or signatures of these definitions.

• VCVio/CryptoFoundations/KeyEncapMech.lean: Refactors the proof of IND_CPA_Game_eq_IND_CCA_Game_toIND_CCA by replacing a multi-step simp/change block with a cleaner simp call using the new lemma HasQuery.toQueryImpl_eq_id' and a simpa invocation of the new lemma QueryImpl.simulateQ_add_liftM_query_left. The earlier proof relied on an inlined simulateQ_query rewrite; the revised version factors that reasoning out into reusable lemmas, making the proof more modular and maintainable.

• VCVio/EvalDist/PFunctor.lean: Adds a new file VCVio/EvalDist/PFunctor.lean that equips an arbitrary polynomial functor (PFunctor) with per-operation probability semantics: defines the class IsProbabilitySpec (via a Handler PMF P) and its uniform subclass IsUniformSpec (requiring finite, inhabited response types and uniform distributions). Provides constructors (IsUniformSpec.ofFintypeInhabited), MonadLiftT instances to lift FreeM P into PMF and SetM, and theorems (evalDist_eq_liftM, support_eq_liftM, evalDist_lift, evalDist_lift_eq_uniform, support_lift) relating evaluation/support to those lifts. Finally, an instEvalDistCompatible instance (priority 100) proves agreement between syntactic and distribution support for any IsUniformSpec.

• VCVio/Interaction/UC/AsyncSecurity.lean: The weakFairOn_of_strongFairOn proof was refactored from a direct fun-based term to a tactic block using obtain. The import changed from private to public import for PolyFun.Interaction.Concurrent.Fairness. The eventuallyAlways_iff lemma and infinitelyOften_iff lemma (Concurrent.ProcessOver.Run) are now invoked via obtain/exact with mpr/mp in the tactic proof. The body is semantically equivalent but uses tactic mode with explicit projection of the eventuallyAlways premise hEA.

• VCVio/Interaction/UC/StdDoBridge.lean: The diff removes a former import all PolyFun.Interaction.Basic.Sampler and adds public import PolyFun.Interaction.Basic.Sampler lower in the import block. The TypeTree namespace block containing the samplePath_done and samplePath_node simplification theorems is deleted. Inside Interaction.Concurrent.ProcessOver.Example, the standalone definitions trivCtx, incrementProcess, trivSampler, the incrementProcess_step_triple theorem, and the separate private example that used them are replaced by a single private example that constructs these objects locally and then uses runSteps_triple_preserves_invariant. The former incrementProcess_step_triple theorem is replaced by a local stepTriple lemma that additionally rewrites with StepOver.sample_eq before applying Std.Do.Triple.pure.

• VCVio/OracleComp/EvalDist.lean: This diff refactors EvalDist.lean to factor IsProbabilitySpec and IsUniformSpec through a functorial PFunctor layer, replacing direct OracleComp instances with PFunctor-based counterparts. The IsProbabilitySpec class and toPMF field are replaced by abbrev/abbrev definitions that delegate to PFunctor.IsProbabilitySpec, and IsUniformSpec.toPMF gains a corresponding toPFunctor conversion. The direct MonadLiftT instances for PMF and SetM are removed; instead, EvalDistCompatible is derived via PFunctor.FreeM.instEvalDistCompatible. The private lemma support_eq_SPMF_support is replaced by support_eq_evalDist_support, and mem_support_evalDist_iff is updated accordingly. The proofs in evalDist_liftM and evalDist_query are adjusted to use the new IsUniformSpec.toPFunctor conversion.

• VCVio/OracleComp/QueryTracking/CostModel.lean: IsPerIndexQueryBound.toWorstCaseCostBound_unit_sum retains its existing statement. In its proof, the application of the lemma HasQuery.queryBoundedAboveBy_withUnitCost_query is now wrapped with a by simpa block that explicitly unfolds instrumentedRun, CostModel.unit, and HasQuery.Program.withUnitCost, making the type equality visible to the simplifier.

• VCVio/OracleComp/QueryTracking/CountingOracle.lean: This change refactors the withCost_apply and withCounting_apply lemmas from rfl to explicit proofs using withTraceBefore_apply and withCost_apply respectively. It also adds two new @[simp] lemmas: costOracle_apply and OracleSpec.countingOracle_apply, which give the pointwise rewriting of costOracle and spec.countingOracle in terms of tell, liftM, and spec.query. Additionally, the lemma countingOracle_eq_costOracle remains unchanged.

• VCVio/OracleComp/QueryTracking/LoggingOracle.lean: The diff adds three new theorem/lemma definitions and changes the existing lemma definitions from using := rfl to using a by block with an exact that references the new theorems. Specifically, it adds:

• writerTMapBase_apply: a new theorem that expresses the run of outer.writerTMapBase inner t in terms of simulateQ outer ((inner t).run).

• Updates withLogging_apply, appendInputLog_apply to use := by rw [withLogging_eq_withTraceAppend] and := by exact preInsert_apply ... respectively, replacing the previous rfl proofs.

This appears to be a refactor that introduces dedicated lemmas for the run equation of writerTMapBase and connects the existing withLogging_apply and appendInputLog_apply lemmas to underlying withTraceAppend_apply and preInsert_apply helper lemmas.

• VCVio/OracleComp/QueryTracking/QueryCost.lean: The proofs of queryBoundedAboveBy_withUnitCost_query and queryBoundedBelowBy_withUnitCost_query were refactored from a direct term application of AddWriterT.queryBoundedAboveBy_bind / AddWriterT.queryBoundedBelowBy_bind to a by block using simpa [HasQuery.Program.withUnitCost] with the same AddWriterT lemmas. This change makes the proof rely on rewriting HasQuery.Program.withUnitCost before applying the boundedness lemmas, simplifying the proof structure.
• VCVio/OracleComp/QueryTracking/Tracing.lean: The four tracing combinators withTraceBefore, withTrace, withTraceAppendBefore, and withTraceAppend are changed from def to abbrev and their bodies now delegate to the corresponding PFunctor.Handler.withTraceBefore, withTrace, withTraceAppendBefore, and withTraceAppend functions rather than directly calling preInsert or postInsert. The application lemmas (withTraceBefore_apply, etc.) and the projection lemmas (fst_map_run_withTraceBefore, etc.) are updated to use new equalities (PFunctor.Handler.withTraceBefore_eq_preInsert, etc.) to rewrite the abbreviation into the original preInsert/postInsert form before applying existing reasoning; in fst_map_run_withTraceAppendBefore, the simp call is also augmented with seqRight_eq_bind. No sorry or admit are introduced.
• VCVio/OracleComp/SimSemantics/Append.lean: The diff makes two previously private lemmas simulateQ_add_liftM_query_left and simulateQ_add_liftM_query_right public by removing the private modifier, and adds a docstring to each explaining that simulating a query-level lift from the left summand routes it to the left implementation and from the right summand routes it to the right implementation. Exposing these lemmas allows other files in the project to use them directly when reasoning about simulateQ on a sum of QueryImpls. No new theorems, definitions, sorry, or admit are introduced.
• VCVio/OracleComp/SimSemantics/QueryImpl/Basic.lean: This diff replaces rfl proofs with explicit by blocks in five lemmas in VCVio/OracleComp/SimSemantics/QueryImpl/Basic.lean, and changes liftTarget from a def to an abbrev that delegates to PFunctor.Handler.liftTarget. The lemma proofs now use simp and rw tactics instead of direct reflexivity, and the liftTarget abbreviation receives an updated doc comment. These changes make the definitions and proofs uniform with the underlying PFunctor.Handler API.
• VCVio/OracleComp/SimSemantics/QueryImpl/Constructions.lean: preInsert and postInsert are redefined as abbrev aliases for PFunctor.Handler.preInsert and PFunctor.Handler.postInsert respectively, replacing their previous direct definitions and updating doc comments. The proofs of simulateQ_preInsert_query and postInsert_apply are updated to use these new aliases and the underlying PFunctor.Handler lemmas, ensuring continued correctness.
• VCVio/ProgramLogic/Tactics/Common/Backward.lean: Makes VCSpecBackwardRuleCacheKey and vcSpecBackwardRuleCache private, restricting their visibility to the Backward module. This clarifies that these declarations are internal implementation details and prevents external access to the cache.
• VCVio/ProgramLogic/Unary/HandlerSpecs.lean: In VCVio/ProgramLogic/Unary/HandlerSpecs.lean, the proofs of loggingOracle_triple and loggingOracle_triple_prefix are refactored: instead of unfolding QueryImpl.withLogging, QueryImpl.withTraceAppend, QueryImpl.postInsert, and QueryImpl.ofLift directly, they now unfold loggingOracle, then rw [QueryImpl.withLogging_apply], and unfold QueryImpl.ofLift. In countingOracle_triple, a call to rw [OracleSpec.countingOracle_apply] is added to the hrun block. In costOracle_triple, a call to rw [costOracle_apply] is added to the analogous hrun block. These changes replace inlined unfolding with rewrites using dedicated lemmas, making the proofs more robust to changes in the underlying definitions.
• VCVio/ProgramLogic/Unary/Loom/Probabilistic.lean: Summary unavailable — AI generation failed.
• VCVioTest/PFunctorFacade.lean: The new file VCVioTest/PFunctorFacade.lean adds a suite of example tests exercising the polynomial functor API and the OracleSpec compatibility façade. It defines a three-way oracle triPFunctor (a PFunctor with one operation returning Fin 3) and a one-step program directSample, then verifies that its evaluation distribution equals the uniform distribution via PFunctor.FreeM.evalDist_lift_eq_uniform and that its support is full. A deterministic handler zeroHandler is introduced along with proofs of its preInsert/postInsert behavior. Separately, a Boolean oracle boolOracleSpec is defined, given uniform and probability spec instances, and two key equivalences are proved: 𝒟[program] = program.liftM PFunctor.IsProbabilitySpec.toPMF and 𝒟[program] = simulateQ OracleSpec.IsProbabilitySpec.toPMF program. All declarations are complete (sorry-free).
• scripts/check-polyfun-boundary.sh: Added scripts/check-polyfun-boundary.sh, a shell script that enforces the public module boundary between VCVio and PolyFun. It scans a fixed set of library directories (e.g., VCVio, ToMathlib, LatticeCrypto, HashSig, Extern, etc.) for any import all PolyFun.… statement, which would leak PolyFun's private declarations and turn a module migration into an unintended API expansion. If a violation is found, the script prints the offending lines to stderr and exits with code 1; otherwise it exits 0.
• 15 file(s) filtered as noise (lockfiles, generated, or trivial): .github/workflows/build.yml, AGENTS.md, CONTRIBUTING.md, Examples/CommitmentScheme/Hiding/LoggingBounds/QuerySalt.lean, Examples/OneTimePad/UC.lean, Examples/PRFTagReader/MultipleToHybrid/Setup.lean, Examples/SealedSender/AspectObservation.lean, VCVio.lean, VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Bridge.lean, VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Chain.lean, VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Compatibility.lean, VCVioTest.lean, …(+3 more)

---

Last updated: 2026-08-08 18:04 UTC.

[github-actions]

Build Timing Report

• Commit: f002f1b
• Message: Merge b17d690 into 9337b8e
• Ref: refactor/polyfun-module-boundary
• Measured on ubuntu-latest with /usr/bin/time -p.
• Commands: clean build rm -rf .lake/build && lake build ToMathlib VCVio LatticeCrypto Extern HashSig Examples VCVioWidgets; warm rebuild lake build ToMathlib VCVio LatticeCrypto Extern HashSig Examples VCVioWidgets; smoke test lake env lean VCVioTest/Smoke.lean.

Measurement	Wall (s)	Status
Clean build	753.91	ok
Warm rebuild	4.65	ok
Smoke test	2.68	ok

Incremental Rebuild Signal

• Warm rebuild saved 749.26s vs clean (162.13x faster).

This compares a clean project build against an incremental rebuild in the same CI job; it is a lightweight variability signal, not a full cross-run benchmark.

Slowest Current Clean-Build Files

Showing 20 slowest of 399 repo targets parsed from the current clean build log.

Wall (s)	Path
78.00	LatticeCrypto/MLKEM/Concrete/NTT.lean
75.00	LatticeCrypto/MLDSA/Concrete/NTT.lean
42.00	VCVio/ProgramLogic/Relational/Loom/Probabilistic.lean
37.00	VCVio/ProgramLogic/Relational/SimulateQ.lean
37.00	VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Chain.lean
28.00	VCVio/OracleComp/Coercions/Add.lean
25.00	VCVio/ProgramLogic/Tactics/Relational/Internals.lean
25.00	VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Compatibility.lean
22.00	VCVio/CryptoFoundations/SecExp.lean
22.00	VCVio/CryptoFoundations/Fischlin/KnowledgeSoundness.lean
20.00	VCVio/OracleComp/QueryTracking/Birthday.lean
20.00	VCVio/ProgramLogic/Tactics/Unary/Internals.lean
19.00	VCVio/EvalDist/Defs/Basic.lean
19.00	VCVio/CryptoFoundations/ReplayFork.lean
19.00	Examples/SimpleTwoServerPIR.lean
18.00	VCVio/CryptoFoundations/Fischlin/Completeness.lean
18.00	VCVio/CryptoFoundations/FiatShamir/Sigma/Fork.lean
18.00	LatticeCrypto/MLKEM/Concrete/Encoding.lean
17.00	VCVio/EvalDist/Monad/Basic.lean
16.00	VCVio/OracleComp/QueryTracking/QueryBound.lean