feat: add game-hop proof widgets for examples

[quangvdao]

Summary

• add an opt-in VCVioWidgets Lean library for infoview proof visualizations
• implement a typed game-hop diagram model, deterministic renderer, and source-location clickback widget
• wire up initial OneTimePad and ElGamal diagrams so the example proofs display readable game-hop views

Test plan

• lake build
• Open Examples/OneTimePad.lean in the infoview and verify the widget layout and clickback targets
• Open Examples/ElGamal.lean in the infoview and verify the widget layout and clickback targets

Made with Cursor

[github-actions]

🤖 Gemini PR Summary

Infrastructure

• Adds the VCVioWidgets library as an opt-in component in lakefile.lean to support experimental proof visualizations.
• Implements a registry and lookup mechanism in Lookup.lean to map Lean modules to context-sensitive visual diagrams.
• Provides a top-level entry point in VCVioWidgets.lean aggregating UI components and example diagrams.

Interactive UI and Widgets

• Implements a "Game Hop" visualization stack with a typed node/edge model (Model.lean) and a deterministic HTML renderer using ProofWidgets.
• Adds GameHopPanel, an Infoview widget that uses RPC methods to fetch and display diagrams based on the user's cursor position.
• Introduces "clickback" functionality via RevealLocation and source-code anchoring (Anchor.lean), enabling navigation from diagram elements to their formal definitions in the editor.

Proof Visualization

• Formalizes visual structures for the ElGamal IND-CPA hybrid argument and the One-Time Pad perfect secrecy proof.
• Integrates these diagrams into the Examples/ directory to provide graphical roadmaps of the underlying relational equivalences and game transitions.
• Note: No new theorems were added, and no existing proofs were modified. No sorry or admit placeholders were introduced in this PR.

---

Statistics

Metric	Count
📝 Files Changed	13
✅ Lines Added	976
❌ Lines Removed	0

---

Lean Declarations

✏️ **Added:** 19 declaration(s)

• def resolve? (anchor : AnchorRef) : MetaM (Option ResolvedAnchor) in VCVioWidgets/GameHop/Anchor.lean
• def rpc (props : PanelWidgetProps) : RequestM (RequestTask Html) in VCVioWidgets/GameHop/Panel.lean
• def defn (declName : Name) : AnchorRef in VCVioWidgets/GameHop/Model.lean
• def chipLabel : AnchorKind → String in VCVioWidgets/GameHop/Anchor.lean
• def thm (declName : Name) : AnchorRef in VCVioWidgets/GameHop/Model.lean
• def findEdge? (diagram : GameDiagram) (source target : NodeId) : Option GameEdge in VCVioWidgets/GameHop/Model.lean
• def RevealLocation : ProofWidgets.Component RevealLocationProps where in VCVioWidgets/Component/RevealLocation.lean
• def matchesModule (binding : DiagramBinding) (modName : Name) : Bool in VCVioWidgets/GameHop/Lookup.lean
• def result (declName : Name) : AnchorRef in VCVioWidgets/GameHop/Model.lean
• def targetRange (anchor : AnchorRef) (resolved : ResolvedAnchor) : Lsp.Range in VCVioWidgets/GameHop/Anchor.lean
• abbrev NodeId in VCVioWidgets/GameHop/Model.lean
• def diagramForModule? (modName : Name) : Option GameDiagram in VCVioWidgets/GameHop/Lookup.lean
• def GameDiagram.renderHtml (diagram : GameDiagram) : MetaM Html in VCVioWidgets/GameHop/Render.lean
• def GameHopPanel : Component PanelWidgetProps in VCVioWidgets/GameHop/Panel.lean
• def cipherGivenMsgEquivDiagram : VCVioWidgets.GameHop.GameDiagram in VCVioWidgets/GameHop/Examples/OneTimePad.lean
• def reduction (declName : Name) : AnchorRef in VCVioWidgets/GameHop/Model.lean
• def withSelection (anchor : AnchorRef) : AnchorRef in VCVioWidgets/GameHop/Model.lean
• def findNode? (diagram : GameDiagram) (nodeId : NodeId) : Option GameNode in VCVioWidgets/GameHop/Model.lean
• def hybridSequenceDiagram : VCVioWidgets.GameHop.GameDiagram in VCVioWidgets/GameHop/Examples/ElGamal.lean

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📄 **Per-File Summaries**

• Examples/ElGamal.lean: This change integrates the GameHopPanel widget into the ElGamal example by importing the necessary module and enabling the panel. This provides interactive UI support for visualizing and managing the cryptographic game-hopping proof steps within the file.
• Examples/OneTimePad.lean: The changes enable the GameHopPanel visualization widget for interactive proof development in OneTimePad.lean by adding the corresponding import and configuration command. No new theorems or proofs are modified, and no sorry or admit placeholders are introduced.
• VCVio/CryptoFoundations/SymmEncAlg.lean: This change integrates the GameHopPanel widget into the symmetric encryption module to ensure the interactive UI remains visible when navigating its core definitions. It does not introduce any new theorems or definitions, nor does it contain any sorry or admit placeholders.
• VCVioWidgets.lean: This new file serves as a top-level module for the VCVioWidgets library, aggregating imports for the GameHop framework, its UI components, and cryptographic examples like ElGamal and OneTimePad. It does not introduce any new theorems, definitions, or sorry placeholders directly.
• VCVioWidgets/GameHop/Anchor.lean: This file introduces the ResolvedAnchor structure and definitions to facilitate mapping Lean declarations to their source locations and metadata for the GameHop widget. It provides logic to resolve declaration names into specific LSP ranges and URIs using the Lean environment, with no sorry placeholders.
• VCVioWidgets/GameHop/Examples/ElGamal.lean: Introduces the hybridSequenceDiagram definition to provide a structured visualization of the ElGamal IND-CPA security proof. The diagram maps the hybrid argument's progression from the initial experiment to the final DDH-based bound by referencing existing theorems and definitions in the library.
• VCVioWidgets/GameHop/Examples/OneTimePad.lean: This file introduces the cipherGivenMsgEquivDiagram definition, which provides a structured visual representation (game hop diagram) for a One-Time Pad perfect secrecy proof. It maps the relational equivalence between different message experiments to their corresponding formal Lean definitions and theorems without introducing new proofs or sorry placeholders.
• VCVioWidgets/GameHop/Lookup.lean: This new file introduces the DiagramBinding structure and a lookup mechanism to map Lean module names to specific GameDiagram visualizations. It establishes a static registry for the One-Time Pad and ElGamal examples to ensure the correct game-hop diagrams are displayed while browsing related files. No theorems, proofs, or sorry placeholders are included.
• VCVioWidgets/GameHop/Model.lean: This file defines the core data structures and types for modeling game-hopping proof diagrams, including definitions for nodes, edges, and layout configurations. It introduces several inductive types and structures to support UI widgets and code anchoring, but does not contain any theorems, proofs, or sorry placeholders.
• VCVioWidgets/GameHop/Panel.lean: This file introduces the GameHopPanel widget, which provides a visual interface for rendering and displaying game-hop diagrams within the Lean environment. It defines a server-side RPC method to retrieve the appropriate diagram for the current module and document position, falling back to an informative message if no diagram is registered.
• lakefile.lean: This change adds the VCVioWidgets library target to the project configuration to support optional proof widget experiments and visualizations.
• VCVioWidgets/Component/RevealLocation.lean: This new file defines the RevealLocation widget and its corresponding properties structure, providing a clickable UI component that navigates the editor to a specified URI and range. It consists of definitions and a JavaScript implementation for the interactive component, with no theorems, proofs, or sorry placeholders included.
• VCVioWidgets/GameHop/Render.lean: This file introduces definitions to render GameDiagram structures as interactive HTML widgets, providing a visual representation of game-hopping proofs with stylized nodes and edges. It leverages the ProofWidgets library and a RevealLocation component to link diagram elements back to their Lean source code, including support for interactive code snippets. No theorems, proofs, or sorry placeholders are included in these changes.

---

Last updated: 2026-03-11 15:51 UTC.

[github-actions]

🤖 Initial AI review without external context

🤖 AI Review

Reviewed Revision

• Commit: 500952477d66759a944d5942ae82978c6f5c5f59
• Commit message:

fix: restore game-hop widget navigation and readability

Make persistent game-hop panels navigate from full cards and snippets so clickthrough works reliably in the infoview. Reflow theorem snippets for narrow widget cards so linked statements stay readable.

Made-with: Cursor

Overall Summary:

1. TL;DR

The foundational models, cryptography examples, and UI widget infrastructures in this PR are structurally sound and well-formalized. However, a couple of files contain hallucinated file-header syntax that will cause immediate parsing errors and break the build, requiring a quick cleanup before this can be merged.

2. Checklist Coverage

No explicit specification checklist was provided for this PR.

3. Key Lean 4 / Mathlib Issues

• Invalid Syntax at File Headers (2 files)
  Files affected: VCVioWidgets/Component/RevealLocation.lean and VCVioWidgets/GameHop/Model.lean
  Both files start with invalid syntax—such as module, public import Lean, public meta import, and public section. Lean 4 does not support the module command, nor does it allow visibility modifiers (like public) on import statements or sections. These appear to be syntax hallucinations from other programming languages and will immediately break the build.
  Action: Remove these modifiers. Begin the files with standard standard import statements followed by the relevant namespace declarations (e.g., import Lean followed by namespace VCVioWidgets).

Minor Nitpicks & Polish:

• Idiomatic Pattern Matching: In VCVioWidgets/GameHop/Anchor.lean, you can use dot notation for the AnchorMode constructors in targetRange (e.g., | .declaration => ... and | .selection => ...) to be more concise and idiomatic.
• Documentation: In VCVioWidgets/GameHop/Model.lean, consider adding docstrings (/-- ... -/) to the core widget structures (GameDiagram, GameNode, GameEdge) and their fields to clarify how elements like AnchorRef hook into the LSP for future contributors.

4. Overall Verdict

Changes Requested

---

📄 **Review for `Examples/ElGamal.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `Examples/OneTimePad.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `VCVio/CryptoFoundations/SymmEncAlg.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `VCVioWidgets.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `VCVioWidgets/Component/RevealLocation.lean`**

Verdict: Changes Requested

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:

• Invalid Syntax at File Header: The file begins with module, public meta import, and public meta section. These are not valid Lean 4 keywords or modifiers. In Lean 4, macros and syntax extensions cannot be applied before imports have been resolved, meaning module and public meta will immediately cause parsing errors.
  The top of the file should simply be standard imports followed by the namespace:

  import ProofWidgets.Component.Basic
  
  namespace VCVioWidgets

Nitpicks:
None

📄 **Review for `VCVioWidgets/GameHop/Anchor.lean`**

Verdict: Needs Minor Revisions

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:

• In targetRange, you can use dot notation for the AnchorMode constructors to be more concise and idiomatic in Lean 4:

  def targetRange (anchor : AnchorRef) (resolved : ResolvedAnchor) : Lsp.Range :=
    match anchor.mode with
    | .declaration => resolved.declarationRange
    | .selection => resolved.selectionRange

📄 **Review for `VCVioWidgets/GameHop/Examples/ElGamal.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `VCVioWidgets/GameHop/Examples/OneTimePad.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

(The file correctly instantiates the GameDiagram structure. The referenced names and anchors match the ones defined in Examples/OneTimePad.lean and the structure fields correctly map to the expected GameHop widget fields without any typeclass or best-practice violations.)

📄 **Review for `VCVioWidgets/GameHop/Lookup.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `VCVioWidgets/GameHop/Model.lean`**

Verdict: Changes Requested

Critical Misformalizations:
None. The data model accurately represents the intended structure for the game hop diagrams and correctly leverages Lean 4's inductive types and structures.

Lean 4 / Mathlib Issues:

• Invalid Syntax at File Start: The file begins with module, public import Lean, and public section. Lean 4 does not have a module command, nor does it support visibility modifiers like public on import statements or sections. This will cause immediate parse errors and break the build. These appear to be syntax hallucinations from other programming languages (like Swift or C++). You should replace them with standard Lean 4 syntax:

  import Lean
  
  namespace VCVioWidgets
  namespace GameHop

Nitpicks:

• Documentation: Consider adding docstrings (/-- ... -/) to the core structures (GameDiagram, GameNode, GameEdge) and their fields. Since this file defines the primary data model for the game hop UI widgets, documenting the expected contents (e.g., how AnchorRef is expected to hook into the LSP) will make the widget infrastructure much easier for future contributors to maintain.

📄 **Review for `VCVioWidgets/GameHop/Panel.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `VCVioWidgets/GameHop/Render.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

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

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

[github-actions]

Automated AI review refreshed.

Trigger: PR synchronize event
Updated review comment: #154 (comment)
Workflow run: https://github.com/Verified-zkEVM/VCV-io/actions/runs/22934623059
Head SHA: 0e53a6681a6402708944840df0ae6be1321a28f9

[quangvdao]

Addressed the actionable Gemini nits in 888927f:

• replaced the manual dotted helpers with Lean Name literals in the example diagram specs
• switched the find? predicates in GameDiagram to direct boolean equality
• simplified RevealLocationProps to derive RpcEncodable directly

I also re-ran lake build VCVioWidgets Examples.OneTimePad Examples.ElGamal, which passed.

The remaining Gemini "changes requested" items are false positives for this repo/toolchain:

• the module / public import / public meta section headers are part of the repo's Lean module-system setup and build successfully here
• the Widget.savePanelWidgetInfo + (return json% { ... $(← rpcEncode ...) }) pattern is the same pattern used upstream in ProofWidgets.Component.HtmlDisplay
• findModuleOf? and documentUriFromModule? are available in the current Lean/mathlib stack used by this project

[github-actions]

Automated AI review refreshed.

Trigger: PR synchronize event
Updated review comment: #154 (comment)
Workflow run: https://github.com/Verified-zkEVM/VCV-io/actions/runs/22939616192
Head SHA: 888927f857180fd0f81dfa37fdcaaaac721facc6