Design the VCVio × PolyFun integration

[quangvdao]

Summary

• add the VCVio × PolyFun integration design suite
• describe the behavior-backed UC model, pattern-runs-on-matter experiment engine, displayed program logic, scheduling/ownership disciplines, and dynamic-participant roadmap
• extend the design outward to separation logic, protocol-scale verification, and quantum strategy carriers
• audit every named VCVio and PolyFun anchor in a verification ledger
• cut the suite over to PolyFun main at f887c096 after Crypto Ladder Problems #66, chore: adjust basic poly-time def #71–Bump to 4.20.0. #72, feat: Bump v4.22.0 rc2, update PFunctor #76–bump Lean/mathlib to v4.22.0 #83, pr summary workflow #88, and chore: fix all linter warnings #91–feat(StateT): prove StateT_run'_simulateQ_eq_self #99 merged

PolyFun naming model

The generic Aberlé-derived layer is structural rather than intrinsically a verification claim:

• Display is a Type-valued polynomial family
• a displayed responder coalgebra preserves one-step witness data
• toDisplayedBehavior coinduces a state-and-witness presentation into a state-free displayed behavior
• PresentationHom maps responder presentations while commuting with their complete displayed step

Accordingly, the design notes now use Displayed*, responder presentations, and PresentationHom. “Verified” is reserved for factual audit statements or applications where the chosen display really encodes a specification and correctness evidence.

Current-state audit

• VCVio main: a5f474fd
• PolyFun main: f887c096
• bump to 4.23 #89 is recorded as the superseded, unmerged parallel prototype
• the merged pattern-runs-on-matter, issue-32, TypeTree-chain, display, parallel, wiring, and consolidation trains are treated as available dependencies rather than open-PR prerequisites
• legacy IOMachine references are replaced by the merged DynComputation API

Validation

• python3 scripts/check-agent-docs.py
• python3 scripts/extract-doc-fragments.py --check
• git diff --check
• stale-name/status scan for the retired Verified* API and pre-merge assumptions

This PR changes documentation only; no Lean source or dependency revision changes.

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Design the VCVio × PolyFun integration

The PR adds a comprehensive design suite for the VCVio × PolyFun integration — 13 documents under docs/design/ that together define the architecture, formalization targets, and roadmap for unifying game-based, simulation-based, and program-logic proofs over the PolyFun interaction substrate. The suite is documentation only; no Lean source or dependency revisions are included.

---

Statistics

Metric	Count
📝 Files Changed	15
✅ Lines Added	2588
❌ Lines Removed	0

---

Lean Declarations

• No declarations were added, removed, or affected.

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

No findings.

---

📄 **Per-File Summaries**

• docs/design/00-end-state.md: Added a new design document docs/design/00-end-state.md (120 lines) that serves as the north-star coverage contract for the VCVio project. It defines the long-term ambition of unifying game-based proofs, state-separating proofs, simulation-based/UC security, and program logics into a single connected stack over the PolyFun interaction substrate. The document specifies five falsifiable formalization targets (e.g., Ξ : Free(P) ⊗ Cofree(Q) → Free(P ⊗ Q), mate equality, bicomodule structure, functorial UC composition, displayed program logics), gives the architecture split with the PolyFun deliverables and VCVio consumers listed per layer (programs via FreeM/OracleComp, implementations via DynSystem/Cofree mate, experiments via runAgainst, packages via StateSeparating classes, scheduling via ProcessScheduler/EnvScheduler, party topology via MachineId/Sid/Pid), and enumerates concrete checkable criteria (rent tests for UC composition, SSP reduction lemma, displayed instrumentation, relational joint displays, named scheduling disciplines, dynamic session creation, and strengthened existing examples). It also codifies non-goals (no rebuild of Paper 1 layers, no synthetic/internal-language UC, no computational-cost foundations, no fixed-ε transitivity, no Canetti ITM fidelity) and states scoping decisions including the promotion of quantum access (staged design 12) and protocol-scale proofs with compromise events (track 11).
• docs/design/01-substrate-inventory.md: Added docs/design/01-substrate-inventory.md, a systematic inventory of the VCVio and PolyFun codebases as of 2026-07-22. The document catalogs VCVio's layered architecture (oracle core, handlers/state-separating, program logic, UC layer with its tier gap), lists PolyFun's merged features (pattern-runs-on-matter, Aberlé display series, Issue-32 chain, etc.), identifies six specific disconnection points (e.g., the tier gap between UC composition theorems and concrete models, the unnamed identification of QueryImpl.Stateful with Responder), and records dependency constraints (toolchain version, pinning via lake manifest, pre-split tickets).
• docs/design/02-behavior-model.md: This document introduces a new 'behavior model' for the OpenTheory framework, designed as an alternative to the existing process model. It defines BehaviorObj as the cofree mate of a process (an element of the final coalgebra of a step polynomial) and a behaviorTheory that interprets OpenTheory's operations (par, wire, plug) directly on these behaviors. The key innovation is that coherence laws satisfied only up to OpenProcessActivationEquiv in the process model become strict Eq in the behavior model via finality, unlocking OpenTheory's composition theorems (Emulates.par_compose, wire_compose, plug_compose) for use with runnable content. The document details a preferred quotient-free construction using M.corec and a fallback strategy, outlines gates (G-2a for IsMonoidal, G-2b for IsTraced, G-2c for HasPlugWireFactor) to measure progress, and notes the integration plan, including a Semantics.ofBehavior layer for probabilistic VCVio contexts.
• docs/design/03-pattern-adversary-ssp.md: This document introduces a new design direction for the VCVio cryptographic verification project: the Libkind–Spivak module action Ξ : Free(P) ⊗ Cofree(Q) → Free(P ⊗ Q) (already merged in PolyFun as chore: adjust basic poly-time def #71/Bump to 4.20.0. #72) is positioned as the canonical semantics for running an adversary against an implementation. It establishes a detailed dictionary mapping VCVio's cryptographic primitives (e.g., adversary OracleComp E α, package QueryImpl.Stateful, composition linkWith, SSP reduction lemma) to PolyFun's pattern/matter notions (e.g., pattern FreeM p α, responder, module action, simulation-invariance theorems). The central design proposes a new VCVio definition runExp as the single point through which experiments are run, with a normative theorem runExp_eq_runThrough identifying it with the Ξ instance, enabling deletion of bespoke associativity and simulation-invariance proofs. The document further outlines plans to use forking/rewinding as pattern surgery via the cursor/occurrence-fork algebra, restate forking lemmas through runExp, and provides a concrete integration plan, deletion targets, rent tests (R-3.1 through R-3.3), and a kill criterion if the identification with Ξ proves infeasible, with explicit risks noted regarding stateful handlers and the evalDist bridge.
• docs/design/04-displayed-program-logic.md: Added a new design document, docs/design/04-displayed-program-logic.md, which argues that Aberlé's 'display' construction (merged as series Bump to 4.21.0-rc3; please read description. #74–chore: 4.28 update #98) constitutes a second, intrinsic program logic for the VCVio project, complementary to the existing extrinsic Loom logic. The document details the current state of instrumentation and relational reasoning in VCVio and sketches a two-phase integration plan: first, re-deriving instrumented wrappers (e.g., QueryTracking, QueryLog) as decorations/displays with transport by one theorem, and second, re-founding relational reasoning via a RelDisplayed judgment over a lockstep parallel composite into a CouplingPost bridge theorem. It also outlines rent tests (e.g., R-4.1: counting as a decoration, R-4.3: qualitative soundness bridge) and kill criteria, and documents risks including potential elaboration bloat for proof-relevant evidence.
• docs/design/05-scheduling-and-ownership.md: This pull request adds a new design document docs/design/05-scheduling-and-ownership.md that outlines Direction 4 of the project. It introduces two key concepts: (1) SchedulingDiscipline as a named, first-class hypothesis for UC statements, replacing the current ambient scheduler convention with three initial instances (lockstep, sequential-activation, env-driven) and requiring discipline-indexed theorems; and (2) OwnershipFrame, a separation-algebra structure on state lenses that generalizes the existing separated vwb lens discipline, enabling a race-free wiring theorem that licenses contraction where Wiring.evalParallel currently refuses it. The document also presents an integration plan across the PolyFun and VCVio repos, including discipline-indexed security statements, a shared-RO model using unowned framed components, and a dummy-adversary derivation for sequential-activation over the behavior model.
• docs/design/06-unbounded-participants.md: This document introduces a design for handling unbounded, dynamically-created protocol participants using indexed polynomial functors (IPFunctor I), where the index set (Topology) represents the directory of live machines with roles and corruption status. It defines spawning as cartesian reindexing along topology inclusions, and corruption as a structure map that swaps a party's interface, unifying across CorruptionModel/Leakage.lean files. The core claim is that the UC composition theorem reduces to the functoriality of behavior assignment, extended by naturality squares for topology changes (spawn/corruption events). A pilot (!F_com) formalizes a multi-session commitment functionality to validate this approach, with explicit rent tests and kill criteria.
• docs/design/07-references.md: Added a new documentation file docs/design/07-references.md that defines the suite's working bibliography, organized into three sections: (A) in-hand sources (e.g., Spivak–Niu, Aberlé, Canetti UC papers, CryptoVerif, Unruh, etc.) with their consuming directions, (B) papers to acquire, including a status update that nine ePrint items (Owl, OwlC, IPDL, Zhandry, BDF+11, Ambainis–Hamburg–Unruh, EasyUC, Canetti–Cohen–Lindell, iUC) are now acquired and indexed, and a correction to a previous revision that misattributed a third author and cited a wrong ePrint number for iUC, and (C) code baselines (SSProve, CryptHOL, EasyUC artifact, squiggle/aberle Agda artifact) for honest comparison. The file also notes a suggested first action for an implementation agent to download the nine items.
• docs/design/08-roadmap.md: Added a new roadmap document (docs/design/08-roadmap.md) that organizes the project’s development into three phases (Phase 0: unblocking, Phase 1: normative directions, Phase 2: displayed logic/disciplines, Phase 2b: outward tracks, Phase 3: paper-3 pilot) and defines eight parallel tracks (A–D, S, P, Q) with explicit gates, kill criteria, cross-references to standing risks, and a success snapshot listing the eight required artifacts. The file also includes parallelization guidance for agent sessions, a risk table, and dependencies such as G-2a, G-2b, G-2c, and specific entry conditions for each track. This documentation establishes the project’s overall plan and coordination constraints for reviewers.
• docs/design/08a-phase1-pr-plan.md: Added a new document docs/design/08a-phase1-pr-plan.md that serves as an operational companion to document 08, detailing a phased PR plan for Exact Slices. It defines Phase 0 slices (P0-1, P0-2, P0-3) and Phase 1 Track A (A1–A5) and Track B (B1–B5) slices, each specifying the repository, base branch, files, key declarations (e.g., OpenProcess.stepPoly, BehaviorObj, Semantics.ofBehavior, runExp), and acceptance gates. Additionally, it includes Phase 2 early-startable slices (C1, D1) and standing PR discipline regarding links to direction docs, kill criteria, and ledger updates.
• docs/design/09-verification-ledger.md: This PR adds a new file, docs/design/09-verification-ledger.md, which serves as a comprehensive, audited catalog of every load-bearing declaration and file named across design docs 00–08. It records the verified locations, merge status (M = merged on main, OFF = on a branch only, SK = design sketch not yet implemented), and a detailed correction history. The ledger covers the VCVio and PolyFun repositories, including anchors for core structures like OracleComp, Stateful, DynSystem, UCSecure, and Emulates, as well as recently merged trains (e.g., FreeP.runOn, Display, ParallelChoice, Wiring). It also adds a new section for Docs 10–12 anchors (e.g., OracleSpec, SecExp, FujisakiOkamoto, GPVHashAndSign, SeededOracle) and records external checkout facts (e.g., iris-lean, Clutch, Approxis, iris-bluebell, IPDL, Owl). The file's correction history documents multiple rounds of auditing and fact-correction (e.g., moving anchors from open-PR to merged state, updating iris-lean capabilities, correcting author names and paper references), concluding with the statement that this review added the escape-hatch nuance for _of_observes_plug_comm, moved TwoPhaseGame to OFF status, fixed the runExp sketch, and annotated IOMachine removal.
• docs/design/10-separation-logic.md: Added a new design document, docs/design/10-separation-logic.md, which establishes three precise identifications between separation logic structures and PolyFun/VCVio structures: resource algebras as ownership frames, BI conjunction as joint displays over ⊗, and step-indexing as finite projections of the cofree comonoid. It outlines two integration tracks: S1 using iris-lean as an engine for the structural/concurrent layer (including a frame camera, behavior COFE, and a contingent abstract WP over OracleComp), and S2 integrating Bluebell-style probabilistic BI over VCVio's evalDist and CouplingPost carrier (including program semantics for Bluebell, joint conditioning lemmas, and a ghost-coupling layer with spec resources and seed tapes). The document also provides a current state audit of iris-lean, iris-bluebell, and VCVio, a list of integration levers, rent tests (e.g., R-10.1 through R-10.6), and a risk analysis.
• docs/design/11-protocol-track.md: Added a new design document, docs/design/11-protocol-track.md, which outlines the Protocol Track for the VCVio project. It describes how CryptoVerif’s game-hop discipline, IPDL’s equational proof style, and Owl’s information-flow type system will be adapted into VCVio’s substrate, and defines a concrete hop engine (game_hop), a corruption/compromise epoch combinator, and a multi-stage pilot ladder (P-1 through P-4) culminating in a signed-DH key exchange proof and a TLS 1.3 skeleton. The document also establishes integration steps, unified assumption registry format, rent tests (R-11.1–R-11.4), and explicit risks.
• docs/design/12-quantum.md: This new design document proposes a boundary–carrier split for VCVio to handle quantum adversaries while keeping existing classical schemes and game definitions unchanged. It introduces a StrategyModel typeclass with two intended instances: Classical (using the current OracleComp/FreeM tree model) and Quantum (using quantum combs over dilated Hilbert spaces). The document details which classical proof techniques survive the QROM and which break (e.g., rewinding, lazy sampling, identical-until-bad), and outlines a three-stage roadmap: Q1 (axiom-graded transfer certificates for quantum-sound hop steps), Q2 (interface-packaged QROM lemmas like O2H with query-count/depth parameters), and Q3 (concrete quantum adversary semantics via combs, discharging the axioms). Key deliverables include rent tests for zero breakage of existing parametric games, a litmus test with ML-KEM sharing one game definition for classical and quantum security, and auditing of the GPVHashAndSign chain through a historyFree certificate. The document also identifies kill criteria and explicitly names risks including the axiom-grade middle years and the lack of prior mechanized solutions at this scale.
• docs/design/README.md: Added a new normative architecture document (docs/design/README.md) for the VCVio × PolyFun integration, based on an audit of both libraries and the PolyFun reading-note suite. It defines the design in one paragraph (structural upstairs in PolyFun, distributional downstairs in VCVio), lists 12 linked design documents with their stability statuses (ranging from normative to research), records 9 resolved design decisions (D1–D9, covering behaviors, SSP/UC unification, program logics, scheduling, probability separation, rent tests, adversary-neutral boundaries, cryptographic assumptions as registry objects, and separation-logic entry via bridges), and states 5 ground rules carried forward (dependency direction, lawfulness tiers, security-definition naming conventions, extension over shadowing, and honest tracking of abstraction costs). This document orients contributors and reviewers by giving the complete structural plan and design rationale before any implementation diff is opened.

---

Last updated: 2026-07-22 10:53 UTC.

[github-actions]

🤖 AI Review

No Lean files were changed in this PR.

[github-actions]

Build Timing Report

• Commit: 482a928
• Message: Merge 3a9bfa2 into a5f474f
• Ref: design/polyfun-integration
• Comparison baseline: a5f474f from the latest successful main run.
• Measured on ubuntu-latest with /usr/bin/time -p.
• Commands: clean build rm -rf .lake/build && lake build ToMathlib VCVio FFI LatticeCrypto HashSig Examples VCVioWidgets; warm rebuild lake build ToMathlib VCVio FFI LatticeCrypto HashSig Examples VCVioWidgets; smoke test lake env lean VCVioTest/Smoke.lean.

Measurement	Baseline (s)	Current (s)	Delta (s)	Status
Clean build	711.55	763.75	+52.20	ok
Warm rebuild	4.41	4.78	+0.37	ok
Smoke test	2.96	2.90	-0.06	ok

Incremental Rebuild Signal

• Warm rebuild saved 758.97s vs clean (159.78x 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 current targets, with comparison against the selected baseline when available.

Current (s)	Baseline (s)	Delta (s)	Path
73.00	60.00	+13.00	LatticeCrypto/MLDSA/Concrete/NTT.lean
71.00	57.00	+14.00	LatticeCrypto/MLKEM/Concrete/NTT.lean
41.00	34.00	+7.00	VCVio/ProgramLogic/Relational/Loom/Probabilistic.lean
35.00	30.00	+5.00	VCVio/ProgramLogic/Relational/SimulateQ.lean
33.00	35.00	-2.00	VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Chain.lean
30.00	27.00	+3.00	VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Compatibility.lean
29.00	30.00	-1.00	LatticeCrypto/MLKEM/Concrete/Encoding.lean
25.00	23.00	+2.00	VCVio/OracleComp/Coercions/Add.lean
24.00	20.00	+4.00	VCVio/CryptoFoundations/Fischlin/KnowledgeSoundness.lean
22.00	20.00	+2.00	VCVio/CryptoFoundations/SecExp.lean
22.00	18.00	+4.00	VCVio/OracleComp/QueryTracking/Birthday.lean
22.00	20.00	+2.00	VCVio/CryptoFoundations/FiatShamir/Sigma/Fork.lean
21.00	17.00	+4.00	VCVio/CryptoFoundations/Fischlin/Completeness.lean
20.00	19.00	+1.00	VCVio/EvalDist/Defs/Basic.lean
20.00	17.00	+3.00	VCVio/ProgramLogic/Tactics/Unary/Internals.lean
20.00	19.00	+1.00	VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Hops.lean
18.00	19.00	-1.00	Examples/SimpleTwoServerPIR.lean
17.00	18.00	-1.00	VCVio/ProgramLogic/Tactics/Relational/Internals.lean
16.00	14.00	+2.00	VCVio/EvalDist/Monad/Basic.lean
16.00	13.00	+3.00	Examples/CommitmentScheme/Hiding/CountBounds.lean

[dtumad]

I agree with the long-term direction, especially the attempt to make the PolyFun connection explanatory rather than just an implementation refactor. After comparing the proposal with the current VCVio/PolyFun code and with adjacent formal-crypto work, I think the suite has a strong central thesis available, but I would sharpen “structural upstairs, distributional downstairs” to:

Cryptography is an abstraction over typed interaction. PolyFun supplies a general structural theory of interfaces, programs, machines, behaviors, and composition; VCVio supplies cryptographic interpretations and restrictions—probability, computational cost, adversarial games, reductions, and security observations. The main result is not that these layers are identical, but that their connections are explicit and machine-checked.

I would present this as two separate contributions joined by one thesis:

1. PolyFun: a reusable Lean theory of polynomial interfaces, free programs/patterns, coinductive systems/behaviors, handlers, interaction laws, displays, and composition.
2. VCVio: a cryptographic verification framework abstracted over that interaction theory, with probability and computational restrictions entering through interpretations/observations, and with forking, Fiat–Shamir, program logic, packages, machines, and compositional security as substantial applications.

This lets a future full-framework paper treat the combination as one strong object without making PolyFun merely an internal implementation detail of VCVio.

Where I think the novelty does and does not lie

The phrase “probability only afterward” is not independently novel:

• ILC gives deterministic/confluent process semantics over explicit random-bit streams and defines the distribution afterward.
• SSProve writes package procedures in a free monad that records probabilistic operations without initially evaluating them, then supplies semantics later.
• CryptHOL already gives coinductive interactive strategies, although probability is intrinsic through spmf at each step rather than one ordinary effect among others.
• EasyUC is less similar: it inherits EasyCrypt's probabilistic-program/module semantics rather than using a free/cofree polynomial interaction account.

Taken together, these comparisons mean that late interpretation alone should not carry the novelty claim. The proposal becomes more distinctive when the polynomial free/cofree structure, handler semantics, and crypto-specific consequences are all connected by theorems.

The plausible distinctive contribution is the combination:

• OracleSpec is an arbitrary typed polynomial interface and OracleComp is definitionally its free monad;
• randomness is not privileged in program syntax—it is one possible typed effect;
• finite syntax supports generic occurrence/cursor surgery before any interpretation;
• machines and pure extensional behaviors are treated coinductively;
• arbitrary effectful packages remain handlers/Kleisli–Mealy systems;
• UC boundary behavior and probabilistic observation are related to those exact structures by adequacy theorems;
• generic forking, package composition, and UC composition become consequences of this common interaction boundary.

The relevant mathematical context includes Katsumata–Rivas–Uustalu on monad/comonad interaction laws, generic coalgebraic trace semantics, Niu–Spivak on polynomial dynamics, Libkind–Spivak's pattern-runs-on-matter action, and Aberlé's polynomial account of compositional program verification. The opportunity is to make these structures pay rent in computational cryptography, not just to import their vocabulary.

Forking is the best evidence we currently have for this thesis. Its pleasant form is a diagnostic that the abstraction boundary is right: replay/forking is surgery on a finite free pattern, while probability is only needed when interpreting the resulting experiment. I would keep forking central in the eventual paper, but describe it as the flagship consequence of the architecture rather than evidence that every implementation is literally cofree matter.

A semantic distinction the proposal currently needs

I think there are three different notions of equivalence in play:

Level	What it observes	Intended use
activation equivalence	only silent versus externally activated steps	coarse scheduler coherence
exact/reified behavior equality	the complete typed event/query tree	machines and equality under every handler
boundary-contextual behavior	boundary traffic/results after hiding or normalizing internal scheduling	UC composition and cryptographic observation

These cannot currently be collapsed.

In particular, OpenProcessActivationEquiv deliberately forgets packet/action identity and stepSampler. I checked the consequence directly in Lean: two OpenProcess ProbComp values can have the same process states, structural steps, and activation LTS (hence be activation-equivalent), while one step sampler returns true and the other returns false; their one-step evalDists are unequal. Thus the proposed A1/B3 chain

activation equivalence → behavior equality → evalDist equality

cannot hold for a single behavior that both forgets samplers and determines execution.

“Equal under every handler” repairs this for exact oracle-machine behavior: behavior equality gives equality of every finite/fuelled run after every lawful interpretation, while the free identity interpretation explains why this remains an exact rather than scheduler-quotiented observation. But it is too strong for UC boundary behavior. An arbitrary handler may distinguish the number, ordering, or bracketing of internal scheduler effects that UC intends to hide. The middle notion should instead quantify over admissible boundary handlers/contexts after internal scheduler behavior has been hidden or normalized.

I would therefore revise Direction 02 around:

1. an exact/reified behavior with an all-handler adequacy theorem;
2. a boundary behavior preserving traffic and observations but abstracting internal scheduling;
3. an explicitly defined class of admissible boundary interpretations;
4. evalDist as one such interpretation;
5. computational UC as the further restriction to admissible PPT environments and approximate observations.

OpenProcessActivationEquiv remains useful as a coarse scheduler diagnostic, but should not be the quotient theorem for semantic behavior. Finality can make an already-chosen observational boundary canonical; it cannot decide which effects are observable.

A second distinction: simulateQ versus Ξ

I also would not make literal identification of simulateQ with Ξ normative.

runThrough/Ξ constructs a pure synchronized free tree from a free pattern and cofree matter. simulateQ folds free syntax into an arbitrary effectful monad. PolyFun's runWithHandler first performs the structural synchronization and then applies a handler; it does not turn every stateful effectful handler into cofree matter.

This matters for ProbResponder: its transition is a joint SPMF (answer × nextState). A lazy random oracle must store exactly the answer it sampled. There is no canonical answer-then-state deterministic factorization. It can be made pure/cofree only after explicitly reifying its randomness (for example as random-tape or sampling events), and that reification is a choice.

I suggest two honest bridge families:

1. Deterministic/reified compatibility: for pure matter or an explicitly reified responder, the Ξ run agrees with handler execution after interpreting its events.
2. Effectful composition: arbitrary stateful packages compose through FreeM.liftM naturality/fusion and Handler.Stateful reindexing/composition laws.

This still permits gradual adoption. ProbResponder and existing stateful packages remain first-class; a component moves to a reified/cofree presentation when the new representation is more useful and an adequacy theorem protects the cutover. Migration should be evidence for the thesis, not an assumed global endpoint.

The full vision I would aim for

The strongest coherent end state looks like a four-corner architecture:

finite free syntax ─────────────── effectful handler execution
  induction, cursor/fork             StateT / OracleComp / SPMF
          │                                      │
          │ unroll / adequacy                     │ observation
          ▼                                      ▼
coinductive machines ─────────── exact and boundary behaviors
  scheduling, complexity          finality, composition, UC

The research contribution is the collection of commuting diagrams between these corners. A result should move between representations through a named theorem rather than an implicit identification.

I would keep all of the outward tracks ambitious and allow them to run in parallel. Separation logic, protocol-scale reasoning, dynamic participants, and quantum-aware games can all be strong evidence for a comprehensive paper. But they should consume the central interfaces rather than determine them prematurely. The central success tests should remain concrete:

• generic forking is structural and probability-independent;
• at least one probabilistic responder has a reified presentation with adequacy;
• repeated bespoke simulateQ/evalDist inductions disappear behind generic fold naturality;
• a real package/hybrid proof loses glue;
• a runnable UC example uses composition through boundary behavior;
• existing crypto developments can migrate incrementally without semantic rewrites.

With those corrections, I think this proposal points to a genuinely strong and reasonably distinctive thesis: not merely “probability is interpreted late,” but a machine-checked account of cryptography as a computational observation of general typed interaction, with structural rewinding and compositional security derived at the appropriate layers.

[dtumad]

Here is the concrete roadmap delta I would make after the conceptual review above and an audit against the current default branches. I think the broad program should remain ambitious and parallel; the changes below are mainly about moving two semantic decisions in front of implementation and updating work that has already landed.

0. Refresh the baseline before assigning slices

This design head predates several changes that materially alter Phase 0/1:

• VCVio #490: OracleComp/OracleQuery are reducible over PolyFun.
• VCVio #492: the replay and seeded forking developments share a generic PolyFun cursor/fork core.
• VCVio #498: OracleStrategy, DynComputation-backed OracleMachine, Implements, and simulations are on main.
• VCVio #499: ProbResponder, wired runs, and the IND-CPA responder presentation are on main; the old WireK direction has effectively become generic eval wiring/runAgainst.
• PolyFun #101: effectful stateful handler execution is merged.
• PolyFun #103: generic handler normalization is merged.

Consequences:

• G-0b should mark Implements/IsSimulation re-derived and merged, and WireK superseded by the new wiring account. RunLimit/TwoPhaseGame can be triaged separately.
• G-0c should agree with doc 07's “acquired and indexed” state rather than remain pending.
• B1 is substantially complete already through PolyFun feat(Traversal): prove neverFailsWhen_simulate #101/Prove sorries in PFunctor equivalences, OptionT EvalDist, and bind failure lemmas #103.
• The ledger should add refactor(OracleComp): make OracleComp/OracleQuery reducible over PolyFun #490/refactor(CryptoFoundations): share a generic PolyFun core across the forking lemmas #492/feat(coinductive): oracle strategies and DynComputation-backed oracle machines #498/feat(coinductive): probabilistic responders, wired runs, and the IND-CPA responder presentation #499 and PolyFun feat(Traversal): prove neverFailsWhen_simulate #101/Prove sorries in PFunctor equivalences, OptionT EvalDist, and bind failure lemmas #103 before new slices cite old anchors.

1. Insert an A0 gate: choose the observation boundary

Before defining BehaviorObj, add an explicit design/experiment slice:

A0 — exact, internal, and boundary observations

Specify:

• which events are protocol/boundary events;
• which events are internal scheduler effects;
• what must be retained about packets/actions;
• whether scheduler effects are hidden, normalized, or interpreted by a law-constrained handler;
• the class of admissible boundary handlers/contexts;
• the exact relationship among activation equivalence, exact behavior equality, boundary behavior, and evalDist.

Required negative test: retain a small Lean example of two activation-equivalent processes with different stepSamplers and unequal one-step evalDists. This prevents the coarse relation from silently becoming a semantic quotient again.

Required positive target:

exact behavior equality
    → equal finite/fuelled runs under every lawful handler

boundary behavior equality
    → equal closed observations under every admissible boundary interpretation
    → equal evalDist for the probabilistic instance

This should also decide whether SchedulingDiscipline or a normalization/hiding construction is needed before strict monoidal laws. At present D1 is nominally needed only by A3, but the observation problem can make it an A1/A2 prerequisite.

2. Split the current A1 rather than proving behavior_congr_activationEquiv

The present A1 gate

OpenProcessActivationEquiv W₁ W₂ → behavior W₁ = behavior W₂

is false for any behavior that retains enough sampler information to determine evalDist, and if behavior discards that information then B3's behavior_eq → evalDist_eq is false.

Replace it with:

• A1a exact/reified behavior: cofree/final behavior retaining the typed event structure, plus finite-projection and “all handlers” adequacy results.
• A1b boundary behavior: the A0-selected hiding/normalization or effect-respecting weak behavior, with a theorem from an appropriately rich bisimulation—not OpenProcessActivationEquiv.
• A1c process-to-boundary adequacy: execution of a process and its boundary behavior agree for every admissible interpretation.

Keep activation-equivalence lemmas as useful coarse facts and scheduler diagnostics. Do not require R-2.1 to erase them from the entire proof closure; require instead that the final UC theorem cross them only through the one explicit A0/A1 bridge, or use the stronger boundary relation directly.

Then A2–A5 can retain the existing ambition:

• direct behavior-level par/wire/plug;
• finality-based strict laws;
• IsTraced/HasPlugWireFactor;
• a runnable probabilistic UC composition pilot.

But the finality argument is valid only after A0 has chosen what the final object observes. Finality does not itself justify forgetting scheduler effects.

3. Reframe B2: do not force simulateQ = Ξ

QueryImpl.Stateful is definitionally PolyFun's stateful handler, and its current run/VCVio runState bridge already gives the natural experiment seam. A new runExp alias is useful only if it has a distinct stable theorem vocabulary; it should not become a second synonymous execution API by default.

More importantly:

• FreeP.runThrough/runTree is pure structural synchronization with cofree matter;
• FreeP.runWithHandler applies an arbitrary monadic handler after that synchronization;
• simulateQ/FreeM.liftM directly interprets free syntax through an arbitrary handler;
• an arbitrary QueryImpl.Stateful I E σ is effectful package data, not literal cofree matter.

Replace runExp_eq_runThrough with two slices:

B2a — deterministic/reified Ξ compatibility

For PFunctor.Responder/ProbResponder.ofDet, and later for an explicitly reified probabilistic responder, prove that the structural Ξ run followed by event interpretation agrees with the established handler run.

B2b — effectful handler composition

Derive package/link laws from the actual universal-fold structure: FreeM.liftM_comp, Handler.Stateful.reindex_comp/run_reindex, fusion, and related normalization laws. Use runOn_assoc only where there is genuinely cofree matter on both sides.

The current ProbResponder API already exposes the right distinction:

• deterministic responders embed canonically using ofDet;
• ProbResponder.toQueryImpl is definitionally a StateT State SPMF handler;
• ofStateQueryImpl maps established StateT σ ProbComp packages into responders through evalDist;
• the reverse “make arbitrary SPMF transitions pure/cofree” direction is not canonical because the joint answer/state draw must be reified.

This gives a gradual migration policy: keep existing effectful packages first-class, add reified presentations where they improve proofs or usability, and require adequacy for every cutover. Do not make global reification a roadmap gate.

4. Add the missing high-rent generic theorem

The #499 bridge

run_simulateQ_toQueryImpl_ofStateQueryImpl

is currently a bespoke induction. Its own documentation identifies the missing generic result: naturality of the universal fold along a monad morphism, together with StateT lifting. This should be promoted ahead of B3:

φ ∘ simulateQ impl = simulateQ (φ ∘ impl)

in the appropriately bundled/typed form.

This is a stronger rent test than adding runExp: it should delete repeated custom OracleComp inductions from responder, simulation, and evalDist bridges. I would make “one generic theorem deletes at least two bespoke inductions” an explicit acceptance gate.

5. Preserve the broad parallel program, but distinguish spine from consumers

I would not narrow Tracks C/D/S/P/Q or hold completed results for a later paper. The strongest eventual paper should include every mature result that supports the thesis. I would only label dependencies more carefully:

• Spine: typed interaction, free syntax, machines/responders, exact/boundary behavior, handlers/observations, generic forking.
• Core consumers/evidence: UC composition, SSP/hybrids, displayed/program logic, scheduling/ownership, asymptotic complexity.
• Parallel research consumers: separation logic, protocol-scale reasoning, unbounded participants, quantum interfaces.

The parallel tracks should be allowed to start early and can feed requirements back through explicit counterexamples. They should not require premature identification of cofree matter with arbitrary effectful packages, or activation equivalence with semantic equality.

I would also replace “paper-3 pilot” language with a single comprehensive-paper evidence plan. The earlier forking/Fiat–Shamir ePrint was not an archival publication; the next paper should present the full framework, with PolyFun and VCVio as two separate contributions and “cryptography as an abstraction over interaction” as the central thesis.

Suggested revised near-term order

1. Baseline refresh: update the inventory/ledger and retire completed/superseded Phase 0 items.
2. Generic fold naturality: land the monad-morphism/StateT theorem and delete bespoke bridge inductions.
3. A0 observation experiment: formalize the counterexample; define the exact/boundary/admissible-handler obligations.
4. B2a deterministic pilot: ofDet/reified responder agrees with the Ξ presentation.
5. B2b effectful pilot: derive one real link/composition law via handler fusion and delete a bespoke twin.
6. A1 exact behavior pilot: obtain the all-handler theorem for machine/reified behavior.
7. A1 boundary pilot: choose hiding/normalization and prove one nontrivial scheduler coherence plus probabilistic adequacy.
8. UC/SSP pilots: only then commit to the full behaviorTheory ladder and broad consumer migrations.

Tracks C/D/S/P/Q can run alongside this where their inputs are already stable. In particular, scheduling counterexamples and disciplines are useful inputs to A0 rather than something that must wait for Phase 2.

The proposal's rent-test discipline is excellent and should remain. The main adjustment is to put the semantic distinctions themselves behind falsifiable gates. If the natural boundary-behavior construction exists, it becomes one of the strongest results in the project; if it does not, the exact behavior, handler, and probabilistic layers remain honest and useful without claiming a false unification.