[Tooling] Create VS Code extension for DumbContracts development

[Th0rgal]

Summary

Build VS Code extension with DumbContracts-specific features to dramatically improve developer experience and reduce learning curve.

Motivation

Current Developer Experience:

• Generic Lean 4 extension exists
• No DumbContracts-specific features
• No contract scaffolding
• No proof hints or autocomplete
• No integrated coverage tracking

Pain Points:

• Manual contract scaffolding
• No IDE support for proof patterns
• Context switching to run tests
• Manual coverage checking

Proposed Features

Feature 1: Contract Scaffolding

Command: "DumbContracts: New Contract"

Generated Structure:

-- DumbContracts/Examples/MyContract/Spec.lean
-- DumbContracts/Examples/MyContract/Contract.lean
-- DumbContracts/Examples/MyContract/Proofs.lean
-- test/PropertyMyContract.t.sol

Template includes:

• Placeholder spec definitions
• EDSL implementation skeleton
• Common proof patterns
• Property test template

Feature 2: Proof Assistant

Auto-suggest tactics based on goal type:

-- Goal: a + b ≤ MAX_UINT256
-- Suggestion: omega | linarith | have h : ... := safeAdd_some_iff_le

Autocomplete for Automation.lean:

• Type safe → suggests safeAdd, safeSub
• Type storage → suggests storage lemmas
• Inline documentation for each lemma

Feature 3: Inline Property Coverage

Visual indicators in editor:

theorem transfer_correct : ... := by  -- ✅ Tested (Property...t.sol:42)
  ...

theorem new_property : ... := by      -- ⚠️ No test found
  ...

Jump to test: Click indicator → jump to Solidity test

Feature 4: Build Integration

Command Palette:

• "DumbContracts: Build All"
• "DumbContracts: Run Tests"
• "DumbContracts: Check Coverage"

Inline errors:

• Show lake build errors in editor
• Highlight failing theorems
• Quick-fix suggestions

Feature 5: Proof Explorer (Sidebar)

Tree view:

📁 SimpleStorage
  ├── ✅ getValue_correct
  ├── ✅ setValue_correct
  ├── ⚠️ authorization_check (no test)
  └── 📊 Coverage: 95% (19/20)

📁 Ledger
  ├── ✅ deposit_increases_balance
  ├── 🚧 deposit_sum_equation (sorry)
  └── 📊 Coverage: 88% (28/32)

Click theorem → jump to proof

Feature 6: Proof Snippets

Shortcuts for common patterns:

prop-getter →

theorem getter_correct : ... := by
  unfold getValue
  simp [getStorage]

prop-setter →

theorem setter_correct : ... := by
  unfold setValue
  simp [setStorage]

Technical Implementation

Technology Stack

• Language: TypeScript
• Base: Lean 4 LSP (existing extension)
• Protocol: Language Server Protocol
• UI: VS Code Extension API

Architecture

DumbContracts Extension
├── LSP Client (communicate with Lean)
├── Contract Scaffolder
├── Proof Assistant (tactic suggestions)
├── Coverage Tracker (parse manifest)
├── Build Runner (execute lake)
└── Proof Explorer (tree view)

Integration Points

1. Lean 4 LSP: Get goal state, type information
2. Property Manifest: Read property_manifest.json
3. Lake: Execute lake build, parse output
4. Forge: Run tests, parse results

Benefits

✅ Dramatically improves DX (developer experience)
✅ Reduces learning curve
✅ Fewer context switches
✅ Inline feedback loop
✅ Industry-standard practice
✅ Attracts VS Code users (majority of developers)

Implementation Plan

Phase 1: Core Features (3 weeks)

• Contract scaffolding
• Build integration
• Basic proof explorer

Phase 2: AI Assistant (2 weeks)

• Tactic suggestions
• Autocomplete for automation
• Inline documentation

Phase 3: Coverage Integration (1 week)

• Parse property manifest
• Inline coverage indicators
• Jump to test

Phase 4: Polish (1 week)

• Snippets library
• Settings/configuration
• Documentation
• Marketplace publish

Files Created

dumbcontracts-vscode-extension/
├── package.json
├── src/
│   ├── extension.ts (entry point)
│   ├── scaffolder.ts
│   ├── proofAssistant.ts
│   ├── coverageTracker.ts
│   ├── buildRunner.ts
│   └── proofExplorer.ts
├── syntaxes/
│   └── dumbcontracts.tmLanguage.json
└── README.md

Dependencies

• VS Code Extension API
• Lean 4 LSP (extend existing extension)
• TypeScript toolchain

Estimated Effort

2-3 months for initial release

Success Criteria

• Scaffolding generates working contract template
• Proof suggestions reduce time by 30%
• Coverage tracking shows real-time status
• Build integration shows errors inline
• 90%+ user satisfaction
• Published to VS Code Marketplace

Related Issues

• Complements [Documentation] Create 'Adding Your First Contract' tutorial #66 (First Contract tutorial)
• Uses [Automation] Auto-generate property manifest from Lean files #72 (automated property extraction)
• Improves workflow for [Example Contract] Implement ERC20 standard token with full verification #69, [Example Contract] Implement ERC721 NFT contract with advanced state modeling #73 (ERC20, ERC721)

Future Enhancements

• Proof search (find similar proofs)
• AI-powered proof completion
• Interactive proof tree visualization
• Git integration for proof versioning

[Th0rgal]

Review Findings

1. Wrong References

• References DumbContracts/ paths throughout
• Depends on [Automation] Auto-generate property manifest from Lean files #72 (property extraction) which is already closed — this dependency is resolved

2. Significant Scope Concern

A VS Code extension is a major project (2-3 months estimated). Given that the core verification work (#65 Ledger sum proofs, #67 UInt256 integration) is still incomplete, and no realistic example contracts (ERC20, ERC721) exist yet, investing in tooling at this stage may be premature.

The existing Lean 4 VS Code extension already provides LSP features, proof state visualization, and error reporting. The incremental value of a DumbContracts/Verity-specific extension may not justify the effort until the framework has more users.

3. Consider Lower-Cost Alternatives

Instead of a full extension, consider:

• VS Code snippets file (.vscode/verity.code-snippets) for common patterns
• A Lean 4 library of tactics (already proposed in [Infrastructure] Proof automation library expansion and optimization #79)
• Better documentation of existing Lean 4 VS Code workflows

[Th0rgal]

This references the old DumbContracts naming. The standard Lean 4 VS Code extension provides language server support for Verity. A custom extension for a project at this scale is premature — the effort is better invested in the verification pipeline itself.