refactor(OracleComp): make OracleComp/OracleQuery reducible over PolyFun

[dtumad]

Motivation

OracleComp and OracleQuery are definitionally the free monad PFunctor.FreeM spec.toPFunctor and the polynomial functor PFunctor.Obj spec.toPFunctor, but as semireducible wrappers with their own Monad/LawfulMonad/MonadLift/Functor instances they presented a second, defeq-but-syntactically-distinct representation of the same objects. Rewriting, normalization, and matching against the machinery that already exists in PolyFun had to cross that seam: rw/simp lemmas stated on FreeM would not fire on OracleComp goals, instances resolved along two different paths, and generic PolyFun constructions needed bespoke VCVio shims.

This PR makes OracleComp, OracleQuery, and OracleSpec.toPFunctor @[reducible] and deletes the duplicate instances, so PolyFun's instances and lemmas apply directly and there is a single canonical representation — a step toward treating VCVio as a thin probability layer on top of PolyFun's theory of interactions. The rest of the diff repairs everything that the transparency change surfaced. All CI libraries (ToMathlib, VCVio, FFI, LatticeCrypto, HashSig, Examples, VCVioWidgets) build clean, and VCVioTest/Smoke.lean passes.

Changes

VCVio/OracleComp/OracleComp.lean, VCVio/OracleComp/OracleQuery.lean — the core change: @[reducible] on both types; the bespoke Monad/LawfulMonad/MonadLift (OracleComp) and Functor/LawfulFunctor (OracleQuery) instances are removed in favor of the PFunctor.FreeM/PFunctor.Obj instances they were forwarding to.

VCVio/OracleComp/Traversal.lean — allPathsSatisfy/somePathSatisfies were defined by tactic-mode recursion through the bespoke OracleComp.construct eliminator, and their @[simp] lemmas used dot notation on (query q : OracleComp spec _) >>= oa. Once the types were reducible, the bind's inferred type has head PFunctor.FreeM, so generalized field resolution looked for PFunctor.FreeM.allPathsSatisfy and the statements no longer elaborated (taking four downstream proofs with them). The predicates are now stated directly over PolyFun's path-prefix machinery: a single ∀/∃ over PFunctor.FreeM.Cursor, filtered by two new generic helpers, PFunctor.TraceList.WithinOn (every recorded answer lies in the allowed fibers) and PFunctor.FreeM.Cursor.Sat (a leaf-residual cursor demands the output predicate, a node-residual cursor the query predicate). Cursors rather than complete Paths because the recursion demands queryPred at every node reachable by possible answers even when the subtree below has no possible completion (empty ranges). The public API — names, signatures, simp attributes — is unchanged, and the supportWhen bridges and bind_iff lemmas keep their original proofs. The two helpers are natural candidates for upstreaming into PolyFun.

VCVio/OracleComp/OracleSpec.lean — two adjustments:

• toPFunctor is now @[reducible], matching Domain/Range/ofPFunctor/QueryLog which already were. This is required for simp/rw matching across the QueryLog spec ↔ PFunctor.TraceList spec.toPFunctor identification in ReplayFork, and (see below) a file-local reducibility attribute for it is no longer viable once OracleComp is reducible.
• toPFunctor_add loses its @[simp]. toPFunctor occurs inside the instance-carrying type of an OracleComp, so rewriting (spec + spec').toPFunctor under a simulateQ/liftM strands goals in a form the simulateQ_query family can no longer match. This single re-key is what let LoggingOracle, MacFromPRF, and FiatShamir/Sigma/Fork keep their original proofs with zero diff.

VCVio/CryptoFoundations/ReplayFork.lean — the file-wide attribute [local reducible] OracleSpec.toPFunctor PFunctor.Idx is narrowed to PFunctor.Idx only (a Mathlib definition we cannot re-attribute globally). With OracleComp reducible, instance-resolution queries for MonadLiftT (OracleComp spec) SetM normalize through toPFunctor, so a local transparency change makes query-time keys diverge from the declaration-time discrimination-tree keys and support/evalDist silently stop elaborating. The toPFunctor half of the attribute is subsumed by the global @[reducible]. Two now-redundant simp arguments (mem_support_freeM_pure_iff) are dropped.

VCVio/OracleComp/SimSemantics/WriterT/PreservesInv.lean, VCVio/OracleComp/SimSemantics/StateT/PreservesInv.lean, VCVio/StateSeparating/CellRef.lean — the invariant-preservation proofs simplified queries via OracleSpec.query_def + simulateQ_query + OracleQuery.input_apply/cont_apply. Under the reducible regime the query_def expansion changes normal form first and the projection lemmas no longer fire, leaving cont ⟨t, id⟩ <$> impl (input ⟨t, id⟩) stuck. Each proof now routes through simulateQ_spec_query, the canonical entry point that avoids the projection artifact entirely.

VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Compatibility.lean — two simpa [monad_norm] using h closings become plain exact h. The helper lemmas' statements and the goal now differ only by ∘/eta wrappers (definitionally equal), and monad_norm over-normalization produced display-identical terms differing at implicit instance positions, which the final simpa match rejected. Direct exact is both simpler and robust.

Examples/PRGfromPRF.lean — show → change at one site: the goal reaching it changed shape under the new simp normal forms, so the show-only-for-readability style linter fires.

VCVio/ProgramLogic/Tactics/Common/{Core,Registry,WpStepRegistry}.lean — fixes the vcstep/vcgen engine, which failed on even wp⟦pure x⟧/wp⟦oa >>= f⟧ goals ("no matching rule applied", plus cascading whnf timeouts) while manual rw [wp_pure]/rw [wp_bind] worked. Root cause: @[vcspec]/@[wpStep] patterns are built via Sym.mkPatternFromDeclWithKey, whose Sym.preprocessType step unfolds reducible definitions — so with OracleComp reducible, stored patterns key the monad argument of Bind.bind and friends in FreeM form. Sym.DiscrTree.getMatch is purely structural and was queried with the raw goal computation, whose keys stayed in OracleComp form; the keys diverged at the monad argument and every registry lookup silently returned no candidates (a rule's own LHS failed to match its own stored pattern). The fix is a shared symMatchKey helper (= Sym.preprocessType on the query term) applied in all five registry query functions, restoring the registration/query symmetry the Sym framework assumes. This bug was latent: it only bites when a definition occurring in rule statements is reducible.

docs/agents/gotchas.md, docs/agents/program-logic.md — document the new invariants: prefix-form statements for lemmas about monadic results, the toPFunctor_add re-key rationale, the prohibition on attribute [local reducible] for definitions occurring in instance keys, and the Sym registry pattern/query alignment invariant.

Verification

• lake build ToMathlib VCVio FFI LatticeCrypto HashSig Examples VCVioWidgets — clean (no errors, no new warnings).
• lake env lean VCVioTest/Smoke.lean — passes.
• No sorrys introduced; pre-existing sorry census unchanged.

🤖 Generated with Claude Code

[github-actions]

🤖 PR Summary

Architectural Thrust

This PR makes OracleComp, OracleQuery, and OracleSpec.toPFunctor @[reducible], unifying them definitionally with their underlying PFunctor.FreeM/PFunctor.Obj representations. The bespoke Monad/LawfulMonad/MonadLift/Functor/LawfulFunctor instances that forwarded to PolyFun's are deleted, so PolyFun's instances and lemmas apply directly. The diff then repairs every site that the increased transparency broke — about a dozen files across the entire VCVio stack.

Mathematical Formalization

No new theorems or definitions are added. The core change is structural.

Core Change: Reducibility

• VCVio/OracleComp/OracleComp.lean: OracleComp is now @[reducible]; its Monad, LawfulMonad, MonadLift instances (which forwarded to the PFunctor.FreeM instances) are deleted.
• VCVio/OracleComp/OracleQuery.lean: OracleQuery is now @[reducible]; its Functor/LawfulFunctor instances (which forwarded to the PFunctor.Obj instances) are deleted.
• VCVio/OracleComp/OracleSpec.lean: toPFunctor is now @[reducible] (and defined via PFunctor.mk). toPFunctor_add loses @[simp] — a deliberate choice because rewriting (spec + spec').toPFunctor under simulateQ/liftM prevents the simulateQ_query family from matching.

Ripple Fixes

Traversal

• VCVio/OracleComp/Traversal.lean: allPathsSatisfy/somePathSatisfies were defined by tactic recursion on the bespoke OracleComp.construct eliminator. Once OracleComp is reducible, the inferred type of >>= has head PFunctor.FreeM, so dot notation on monadic results no longer elaborates. The predicates are now stated directly over PFunctor.FreeM.Cursor, using two new generic helpers PFunctor.TraceList.WithinOn and PFunctor.FreeM.Cursor.Sat. Public API names, signatures, and @[simp] attributes are unchanged.

ReplayFork

• VCVio/CryptoFoundations/ReplayFork.lean: A file-wide attribute [local reducible] OracleSpec.toPFunctor PFunctor.Idx is narrowed to PFunctor.Idx only (since a local transparency change makes instance-resolution query keys diverge from discrimination-tree keys). Two now-redundant simp arguments (mem_support_freeM_pure_iff) are dropped.

Invariant Preservation Proofs

• VCVio/OracleComp/SimSemantics/WriterT/PreservesInv.lean, VCVio/OracleComp/SimSemantics/StateT/PreservesInv.lean, VCVio/StateSeparating/CellRef.lean: The invariant-preservation proofs simplified queries via OracleSpec.query_def + simulateQ_query + OracleQuery.input_apply/cont_apply. Under the reducible regime the projection lemmas no longer fire; each proof now routes through simulateQ_spec_query, the canonical entry point that avoids the projection artifact.

Cosmetic / Minor

• VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Compatibility.lean: Two simpa [monad_norm] become exact (the monad_norm over-normalization produced display-identical terms differing at implicit instance positions).
• Examples/PRGfromPRF.lean: show → change (stylistic; avoids a linter complaint about the new simp normal form).

Infrastructure / CI

Tactic Engine Fix (Key Alignment)

• VCVio/ProgramLogic/Tactics/Common/Core.lean: Adds a symMatchKey function that normalizes reducible oracle wrappers in goal-side computations, and the import Lean.Meta.Sym.Pattern.
• VCVio/ProgramLogic/Tactics/Common/Registry.lean: Three lookup functions (getRegisteredUnaryVCSpecEntries, getRegisteredUnaryVCSpecEntriesNoWhnf, getRegisteredRelationalVCSpecEntries) now apply symMatchKey before querying the discrimination tree.
• VCVio/ProgramLogic/Tactics/Common/WpStepRegistry.lean: getRegisteredWpStepEntries and getRegisteredWpStepEntriesNoWhnf now apply symMatchKey before registry lookup.
• Root cause: @[vcspec]/@[wpStep] patterns are built via Sym.mkPatternFromDeclWithKey, which unfolds reducible definitions; stored patterns thus key the monad argument of Bind.bind in FreeM form. The registry query was purely structural but used the raw goal computation (keys in OracleComp form), so keys diverged at every lookup and no candidates were found — even a rule's own LHS failed to match its own stored pattern. This bug was latent, only surfacing when a definition in rule statements became reducible.

Dependency Update

• lakefile.lean: Pinned PolyFun dependency updated to commit 1f7f477c9701f7606841bb1638dcffb9b2359d62.

Documentation

• docs/agents/gotchas.md: Documents the new invariants: prefix-form statements for lemmas about monadic results, the toPFunctor_add re-key rationale, the prohibition on attribute [local reducible] for definitions occurring in instance keys, and lists OracleQuery/OracleSpec.toPFunctor as newly reducible types.
• docs/agents/program-logic.md: Documents the Sym registry pattern/query alignment invariant and the symMatchKey workaround.

Proof Completion (sorries removed)

No sorry or admit are introduced or removed. Pre-existing sorry census is unchanged.

---

Statistics

Metric	Count
📝 Files Changed	17
✅ Lines Added	177
❌ Lines Removed	89

---

Lean Declarations

✏️ Added: 1 declaration(s)

VCVio/ProgramLogic/Tactics/Common/Core.lean (1)

• def symMatchKey (e : Expr) : MetaM Expr

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

• def ofFreeM {α : Type w} (oa : PFunctor.FreeM spec.toPFunctor α) : OracleComp spec α in VCVio/OracleComp/OracleComp.lean moved from L37 to L38
• def toFreeM {α : Type w} (oa : OracleComp spec α) : PFunctor.FreeM spec.toPFunctor α in VCVio/OracleComp/OracleComp.lean moved from L43 to L42
• theorem toFreeM_ofFreeM {α : Type w} (oa : PFunctor.FreeM spec.toPFunctor α) : in VCVio/OracleComp/OracleComp.lean moved from L50 to L47
• def toPFunctor (spec : OracleSpec ι) : PFunctor in VCVio/OracleComp/OracleSpec.lean moved from L32 to L33
• lemma toPFunctor_add {ι : Type u} {ι' : Type u'} in VCVio/OracleComp/OracleSpec.lean moved from L100 to L104

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

The pull request is largely compliant with the project's contribution guidelines. The main issue is missing declaration docstrings on several new lemmas in Traversal.lean.

---

📄 **Per-File Summaries**

• Examples/PRGfromPRF.lean: In Examples/PRGfromPRF.lean, a show tactic was replaced with change in the proof of the private lemma simulateQ_prfReal_oracleOutputs, at the point where the goal is prfRealQueryImpl prf k (Sum.inr s) >>= _ = _. This is a purely stylistic or tactic-level refactor; no definition, theorem statement, or proof logic was altered.
• VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Compatibility.lean: In the proof of statefulPostKeygenFreshAdvantage_eq_cmaRealRunProb_signedFreshAdv, two cases (cache_some and cache_none) were simplified by replacing simpa [monad_norm] with exact. This removes an unnecessary monad_norm rewrite, making the proof more direct.
• VCVio/CryptoFoundations/ReplayFork.lean: Removed the OracleSpec.toPFunctor entry from the attribute [local reducible] directive, keeping only PFunctor.Idx reducible locally. In contextFork_success, two simp calls that previously included mem_support_freeM_pure_iff as an argument now omit it, changing how the goal is simplified in those branches. No sorry or admit appear in the diff.
• VCVio/OracleComp/OracleComp.lean: The diff makes OracleComp itself @[reducible] (it was previously not marked reducible, while ofFreeM and toFreeM already were). It also removes three instance declarations: the Monad, LawfulMonad, and MonadLift instances for OracleComp spec that were previously defined by casting to the underlying PFunctor.FreeM instances. Finally, several theorem and definition signatures are reformatted for brevity (line breaks removed), but their statements are unchanged.
• VCVio/OracleComp/OracleQuery.lean: The OracleQuery definition is now marked @[reducible] to improve definitional unfolding and type inference. The explicit Functor and LawfulFunctor instances for OracleQuery spec have been removed, since their definitions are no longer needed given the @[reducible] attribute and the fact that OracleQuery is defined as PFunctor.Obj spec.toPFunctor, which already provides those instances via the inherited structure from PFunctor.Obj. No sorry or admit are present.
• VCVio/OracleComp/OracleSpec.lean: The diff makes two changes to VCVio/OracleComp/OracleSpec.lean. First, toPFunctor is marked @[reducible] and defined via PFunctor.mk (rather than a structure literal), increasing the API's transparency for typeclass resolution. Second, the @[simp] attribute is removed from toPFunctor_add with a comment explaining that rewriting toPFunctor inside the instance-carrying type of OracleComp under simulateQ/liftM blocks the simulateQ_query family from matching, so the lemma is deliberately not a simp lemma to avoid breaking those tactics.
• VCVio/OracleComp/SimSemantics/StateT/PreservesInv.lean: In the proof of simulateQ_run_preservesInv, the simpa tactic was updated to use the lemma simulateQ_spec_query instead of the combination OracleSpec.query_def, simulateQ_query. This change simplifies the proof by consolidating the previously used lemmas into a single lemma.
• VCVio/OracleComp/SimSemantics/WriterT/PreservesInv.lean: The proof of simulateQ_run_writerPreservesInv was updated to replace a group of simplification lemmas (OracleSpec.query_def, ofPFunctor_toPFunctor, simulateQ_query, OracleQuery.input_apply, OracleQuery.cont_apply, id_map) with the single lemma simulateQ_spec_query. This refactors the simp call in the query_bind case, likely to align with a consolidation of query-related reasoning in the project.
• VCVio/OracleComp/Traversal.lean: This PR refactors VCVio/OracleComp/Traversal.lean to redefine allPathsSatisfy and somePathSatisfies using PFunctor.FreeM.Cursor from the PolyFun library, replacing prior inductive definitions. It adds the import PolyFun.PFunctor.Free.Cursor and updates the file’s module docstring to explain the new cursor-based phrasing: a cursor represents a typed path prefix into the free-monad tree, so quantifying over cursors whose recorded directions stay within possibleOutputs captures every demanded query node (via non-terminal cursors) and every reachable final output (via terminal cursors). The lemmas allPathsSatisfy_pure, somePathSatisfies_pure, allPathsSatisfy_query_bind, and somePathSatisfies_query_bind are rewritten to use a propext-based proof pattern involving cursor operations (PFunctor.FreeM.Cursor.root, .down, .trace_down) and TraceList.directionsWithin_cons. The auxiliary definitions allOutputsSatisfyWhen and someOutputSatisfiesWhen are changed from method invocations (oa.allPathsSatisfy) to function applications (allPathsSatisfy ... oa). The lemma allOutputsSatisfyWhen_iff_supportWhen and someOutputSatisfiesWhen_iff_supportWhen are updated accordingly, and both allPathsSatisfy_bind_iff and somePathSatisfies_bind_iff are refactored from a single-line induction with simp to an explicit pattern match using pure x and query_bind q oa ih cases, calling pure_bind and monad_norm directly.
• VCVio/ProgramLogic/Tactics/Common/Core.lean: This diff adds a new symMatchKey function to Core.lean that normalizes reducible oracle wrappers (OracleComp, OracleQuery, OracleSpec.toPFunctor) in goal-side computations. It also adds the import import Lean.Meta.Sym.Pattern. The purpose is to ensure that goal expressions have keys matching those produced by Sym.mkPatternFromDeclWithKey, which is needed for proper Sym.DiscrTree.getMatch lookup. A comment explains that Sym.preprocessType must not be used here because it could cause panics with matchers and loose de Bruijn variables.
• VCVio/ProgramLogic/Tactics/Common/Registry.lean: In Registry.lean, three lookup functions for VC spec entries were modified to apply symMatchKey to the key expression before querying the discrimination tree: getRegisteredUnaryVCSpecEntries now calls symMatchKey after whnfReducible, getRegisteredUnaryVCSpecEntriesNoWhnf replaced its instantiateMVars call with symMatchKey, and getRegisteredRelationalVCSpecEntries now wraps symMatchKey around the reduction of oa. This ensures that the key used for tree lookup is normalized by symMatchKey, which likely expands or canonicalizes symbolic names (e.g., unfold sym projections) so that the discrimination tree matches entries registered under the underlying constant rather than the symbolic wrapper. No sorry or admit were introduced.
• VCVio/ProgramLogic/Tactics/Common/WpStepRegistry.lean: In getRegisteredWpStepEntries, a call to symMatchKey was added after whnf; in getRegisteredWpStepEntriesNoWhnf, the existing instantiateMVars call was replaced with symMatchKey. Both functions now canonicalize the expression via symMatchKey before registry lookup, ensuring consistent normalization for symbolic matching and likely fixing cases where instantiateMVars alone was insufficient.
• VCVio/StateSeparating/CellRef.lean: In theorem simulateQ_run_cellPreserved, the simpa call was simplified by removing the reference to OracleSpec.query_def, leaving only simulateQ_spec_query. This eliminates an unnecessary lemma dependency, streamlining the proof.
• docs/agents/gotchas.md: Extended the existing gotcha about @[reducib le] thin wrappers by listing OracleQuery and OracleSpec.toPFunctor as newly included types, and by stating that the Monad/Functor instances come directly from PFunctor.FreeM/PFunctor.Obj. Added two detailed failure modes: (1) dot notation on monadic results fails because the inferred type is PFunctor.FreeM, not OracleComp — the workaround is to use prefix form; (2) attribute [local reducible] on a definition that instance keys mention silently breaks instance resolution (e.g. MonadLiftT (OracleComp spec) SetM vanishes). Finally, documented that OracleSpec.toPFunctor_add is deliberately not @[simp], explaining that rewriting (spec + spec').toPFunctor under simulateQ/liftM prevents the simulateQ_query family from matching.
• docs/agents/program-logic.md: Added a new subsection documenting the key alignment invariant for Sym.DiscrTree.getMatch in the program logic tactic framework. The invariant states that goal-side query terms must undergo the same normalization as patterns receive at registration time, because DiscrTree matching is purely structural. All registry query functions now route extracted computations through symMatchKey (located in Tactics/Common/Core.lean), which applies Sym.preprocessType (unfold-reducible + beta/zeta/eta). This alignment is critical because OracleComp is a reducible alias of PFunctor.FreeM: stored patterns carry unfolded FreeM-form keys at the monad argument of Bind.bind and analogous constructors, so an unnormalized query key diverges there and causes every lookup to silently return no candidates, the symptom being that vcstep reports "no matching rule applied" on plain pure/>>= goals while manual rw [wp_pure]/rw [wp_bind] works.
• lakefile.lean: Updated the pinned commit for the PolyFun dependency in the lakefile.lean from old commit 97a262ce2ba7513448b76635e1f6a07f61f40de5 to new commit 1f7f477c9701f7606841bb1638dcffb9b2359d62. This ensures the project builds against a specific later version of the PolyFun library, which may include bug fixes, new lemmas, or API changes that affect the rest of the VCVio codebase.
• 1 file(s) filtered as noise (lockfiles, generated, or trivial): lake-manifest.json

---

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

[github-actions]

Build Timing Report

• Commit: 50726f0
• Message: Merge 874ef00 into a5f474f
• Ref: dtumad/reducible-oraclecomp
• 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	745.71	+34.16	ok
Warm rebuild	4.41	4.38	-0.03	ok
Smoke test	2.96	2.58	-0.38	ok

Incremental Rebuild Signal

• Warm rebuild saved 741.33s vs clean (170.25x 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
65.00	57.00	+8.00	LatticeCrypto/MLKEM/Concrete/NTT.lean
38.00	34.00	+4.00	VCVio/ProgramLogic/Relational/Loom/Probabilistic.lean
38.00	35.00	+3.00	VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Chain.lean
35.00	30.00	+5.00	VCVio/ProgramLogic/Relational/SimulateQ.lean
30.00	27.00	+3.00	VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Compatibility.lean
28.00	23.00	+5.00	VCVio/OracleComp/Coercions/Add.lean
25.00	30.00	-5.00	LatticeCrypto/MLKEM/Concrete/Encoding.lean
22.00	20.00	+2.00	VCVio/CryptoFoundations/SecExp.lean
22.00	20.00	+2.00	VCVio/CryptoFoundations/FiatShamir/Sigma/Fork.lean
21.00	20.00	+1.00	VCVio/CryptoFoundations/Fischlin/KnowledgeSoundness.lean
21.00	17.00	+4.00	VCVio/ProgramLogic/Tactics/Unary/Internals.lean
21.00	19.00	+2.00	VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Hops.lean
21.00	19.00	+2.00	Examples/SimpleTwoServerPIR.lean
19.00	19.00	+0.00	VCVio/EvalDist/Defs/Basic.lean
19.00	18.00	+1.00	VCVio/OracleComp/QueryTracking/Birthday.lean
18.00	18.00	+0.00	VCVio/ProgramLogic/Tactics/Relational/Internals.lean
16.00	14.00	+2.00	VCVio/EvalDist/Monad/Basic.lean
16.00	17.00	-1.00	VCVio/CryptoFoundations/Fischlin/Completeness.lean
16.00	12.00	+4.00	Examples/PRGfromPRF.lean

[github-actions]

🤖 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 Examples/PRGfromPRF.lean
• Agent B failed for VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Compatibility.lean
• Agent B failed for VCVio/CryptoFoundations/ReplayFork.lean
• Agent B failed for VCVio/OracleComp/OracleComp.lean
• Agent B failed for VCVio/OracleComp/OracleQuery.lean
• Agent B failed for VCVio/OracleComp/OracleSpec.lean
• Agent B failed for VCVio/OracleComp/SimSemantics/StateT/PreservesInv.lean
• Agent B failed for VCVio/OracleComp/SimSemantics/WriterT/PreservesInv.lean
• Agent B failed for VCVio/OracleComp/Traversal.lean
• Agent B failed for VCVio/ProgramLogic/Tactics/Common/Core.lean
• Agent B failed for VCVio/ProgramLogic/Tactics/Common/Registry.lean
• Agent B failed for VCVio/ProgramLogic/Tactics/Common/WpStepRegistry.lean
• Agent B failed for VCVio/StateSeparating/CellRef.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 `Examples/PRGfromPRF.lean`**

An error occurred while analyzing Examples/PRGfromPRF.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/CryptoFoundations/FiatShamir/Sigma/Stateful/Compatibility.lean`**

An error occurred while analyzing VCVio/CryptoFoundations/FiatShamir/Sigma/Stateful/Compatibility.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/CryptoFoundations/ReplayFork.lean`**

An error occurred while analyzing VCVio/CryptoFoundations/ReplayFork.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/OracleComp/OracleComp.lean`**

An error occurred while analyzing VCVio/OracleComp/OracleComp.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/OracleComp/OracleQuery.lean`**

An error occurred while analyzing VCVio/OracleComp/OracleQuery.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/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/OracleComp/SimSemantics/StateT/PreservesInv.lean`**

An error occurred while analyzing VCVio/OracleComp/SimSemantics/StateT/PreservesInv.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/OracleComp/SimSemantics/WriterT/PreservesInv.lean`**

An error occurred while analyzing VCVio/OracleComp/SimSemantics/WriterT/PreservesInv.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/OracleComp/Traversal.lean`**

An error occurred while analyzing VCVio/OracleComp/Traversal.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 `VCVio/ProgramLogic/Tactics/Common/Registry.lean`**

An error occurred while analyzing VCVio/ProgramLogic/Tactics/Common/Registry.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/WpStepRegistry.lean`**

An error occurred while analyzing VCVio/ProgramLogic/Tactics/Common/WpStepRegistry.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/StateSeparating/CellRef.lean`**

An error occurred while analyzing VCVio/StateSeparating/CellRef.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.'}]}}

[dtumad]

@quangvdao would be good to know if you see this as the right fix for mvcgen breakage