Use PFunctor.mk directly for OracleSpec by quangvdao · Pull Request #493 · Verified-zkEVM/VCVio

quangvdao · 2026-07-17T10:48:37Z

Summary

define OracleSpec.toPFunctor directly with PFunctor.mk
remove the obsolete PFunctor.ofFamily case from the structural registry-key normalizer
pin PolyFun to merged cleanup PR PolyFun #73, commit 1f7f477c9701f7606841bb1638dcffb9b2359d62

Rationale

PFunctor.ofFamily was only a reducible wrapper around the structure constructor and has now been removed upstream. Using PFunctor.mk preserves the existing definitional round trips while removing one reducible declaration from the normalization path.

Stack and conflict audit

This PR targets the current head of #490 (dtumad/reducible-oraclecomp). The newer draft #492 is also stacked on #490, but touches none of this PR's four files, so the branches can proceed independently.

Validation

exact Mathlib revision and origin verified against lake-manifest.json
exact merged PolyFun revision and origin verified against lake-manifest.json
focused build: 2,778 jobs passed
LAKE_ARTIFACT_CACHE=false lake build Examples: 2,966 jobs passed
git diff --check
no remaining ofFamily references in VCVio, VCVioTest, or Examples

github-actions · 2026-07-17T10:49:19Z

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Use PFunctor.mk directly for OracleSpec

The PR updates OracleSpec.toPFunctor to use PFunctor.mk directly, removing dependency on the now-removed upstream PFunctor.ofFamily. Correspondingly, the symMatchKey tactic is adjusted to not unfold ofFamily. PolyFun dependency is pinned to a compatible commit. No new sorry/admit are introduced.

Statistics

Metric	Count
📝 Files Changed	4
✅ Lines Added	7
❌ Lines Removed	7

Lean Declarations

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

def toPFunctor (spec : OracleSpec ι) : PFunctor in VCVio/OracleComp/OracleSpec.lean moved from L33 to L33

sorry Tracking

No sorrys were added, removed, or affected.

📋 **Additional Analysis**

The diff updates the PolyFun dependency, adjusts OracleSpec.toPFunctor and symMatchKey to follow upstream API changes, and removes a stale reference to PFunctor.ofFamily. No style, documentation, or process violations were found.

📄 **Per-File Summaries**

VCVio/OracleComp/OracleSpec.lean: In OracleSpec.lean, the definition of toPFunctor was refactored: instead of calling PFunctor.ofFamily spec, it now directly constructs a PFunctor via PFunctor.mk ι spec. This changes the internal representation but preserves the semantics; no other definitions, theorems, or sorry/admit are affected.
VCVio/ProgramLogic/Tactics/Common/Core.lean: The symMatchKey tactic helper in Core.lean was modified to no longer unfold PFunctor.ofFamily when computing the key for Sym's discrimination-tree matching. The docstring comment above the function was updated accordingly, removing the mention of PFunctor.ofFamily both from the list of unfolded wrappers and from the note about not using Sym.preprocessType. This change ensures that the key computation matches only the structural patterns produced by Sym.mkPatternFromDeclWithKey for OracleComp, OracleQuery, and OracleSpec.toPFunctor, aligning the implementation with the original intent described in the docstring.
lakefile.lean: The only change is that the pinned commit hash for the PolyFun dependency was updated from a65a9ab83ad42034229d379940bbeed2f44831df to 1f7f477c9701f7606841bb1638dcffb9b2359d62. This matters because it changes the precise version of that external library used by the project.
1 file(s) filtered as noise (lockfiles, generated, or trivial): lake-manifest.json

Last updated: 2026-07-17 10:49 UTC.

github-actions · 2026-07-17T11:00:08Z

🤖 AI Review

Overall Summary:
An error occurred while synthesizing the summary: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

Errors during review:

Agent B failed for VCVio/OracleComp/OracleSpec.lean
Agent B failed for VCVio/ProgramLogic/Tactics/Common/Core.lean
Agent B failed for lakefile.lean

🔗 **Cross-File Analysis**

Cross-file analysis failed: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

📄 **Review for `VCVio/OracleComp/OracleSpec.lean`**

An error occurred while analyzing VCVio/OracleComp/OracleSpec.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

📄 **Review for `VCVio/ProgramLogic/Tactics/Common/Core.lean`**

An error occurred while analyzing VCVio/ProgramLogic/Tactics/Common/Core.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

📄 **Review for `lakefile.lean`**

An error occurred while analyzing lakefile.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

github-actions · 2026-07-17T11:09:45Z

Build Timing Report

Commit: beaa51b
Message: Merge 81251ae into 5d75264
Ref: agent/remove-pfunctor-offamily
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	Wall (s)	Status
Clean build	712.37	ok
Warm rebuild	4.40	ok
Smoke test	3.03	ok

Incremental Rebuild Signal

Warm rebuild saved 707.97s vs clean (161.90x 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 388 repo targets parsed from the current clean build log.

Wall (s)	Path
63.00	`LatticeCrypto/MLKEM/Concrete/NTT.lean`
62.00	`LatticeCrypto/MLDSA/Concrete/NTT.lean`
37.00	`VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Chain.lean`
34.00	`VCVio/ProgramLogic/Relational/Loom/Probabilistic.lean`
30.00	`VCVio/ProgramLogic/Relational/SimulateQ.lean`
27.00	`VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Compatibility.lean`
26.00	`VCVio/OracleComp/Coercions/Add.lean`
25.00	`LatticeCrypto/MLKEM/Concrete/Encoding.lean`
22.00	`VCVio/ProgramLogic/Tactics/Unary/Internals.lean`
21.00	`VCVio/CryptoFoundations/Fischlin/KnowledgeSoundness.lean`
21.00	`VCVio/CryptoFoundations/FiatShamir/Sigma/Fork.lean`
20.00	`VCVio/ProgramLogic/Tactics/Relational/Internals.lean`
20.00	`Examples/SimpleTwoServerPIR.lean`
19.00	`VCVio/CryptoFoundations/SecExp.lean`
19.00	`VCVio/OracleComp/QueryTracking/Birthday.lean`
19.00	`VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Hops.lean`
17.00	`Examples/ElGamal/Hash.lean`
16.00	`VCVio/EvalDist/Defs/Basic.lean`
15.00	`VCVio/CryptoFoundations/Fischlin/Completeness.lean`
15.00	`Examples/CommitmentScheme/Hiding/LoggingBounds/QuerySalt.lean`

…PolyFun (#490) * refactor(OracleComp): make OracleComp and OracleQuery reducible over PolyFun Make `OracleComp`, `OracleQuery`, and `OracleSpec.toPFunctor` reducible aliases of their `PolyFun` counterparts and delete the bespoke `Monad`/`LawfulMonad`/`MonadLift`/`Functor` instances, so PolyFun's own instances and lemmas apply directly to oracle computations. Repair the resulting breakage: restate `Traversal` over `PFunctor.FreeM.Cursor`, re-key `toPFunctor_add` off the simp set, narrow ReplayFork's local transparency to `PFunctor.Idx`, route invariant-preservation proofs via `simulateQ_spec_query`, and align the `@[vcspec]`/`@[wpStep]` registry lookups with `Sym` pattern preprocessing via `symMatchKey`. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Consume generic PolyFun traversal predicates (#491) * refactor(OracleComp): consume generic PolyFun traversal predicates * chore: pin merged PolyFun traversal API * refactor(OracleSpec): use PFunctor.mk directly (#493) * refactor: align VCVio with merged PolyFun APIs * chore: update PolyFun and split sampler ornaments * refactor: consume PolyFun handler normalization --------- Co-authored-by: Claude Fable 5 <noreply@anthropic.com> Co-authored-by: Quang Dao <qvd@andrew.cmu.edu>

refactor(OracleSpec): use PFunctor.mk directly

81251ae

quangvdao marked this pull request as ready for review July 17, 2026 10:52

quangvdao merged commit 874ef00 into dtumad/reducible-oraclecomp Jul 17, 2026
7 checks passed

quangvdao deleted the agent/remove-pfunctor-offamily branch July 19, 2026 20:30

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Use PFunctor.mk directly for OracleSpec#493

Use PFunctor.mk directly for OracleSpec#493
quangvdao merged 1 commit into
dtumad/reducible-oraclecompfrom
agent/remove-pfunctor-offamily

quangvdao commented Jul 17, 2026

Uh oh!

github-actions Bot commented Jul 17, 2026

Uh oh!

Uh oh!

github-actions Bot commented Jul 17, 2026

Uh oh!

github-actions Bot commented Jul 17, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

quangvdao commented Jul 17, 2026

Summary

Rationale

Stack and conflict audit

Validation

Uh oh!

github-actions Bot commented Jul 17, 2026

🤖 PR Summary

Uh oh!

Uh oh!

github-actions Bot commented Jul 17, 2026

🤖 AI Review

Uh oh!

github-actions Bot commented Jul 17, 2026

Build Timing Report

Incremental Rebuild Signal

Slowest Current Clean-Build Files

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant