[Infrastructure] Gas cost modeling and optimization analysis

[Th0rgal]

Summary

Add gas cost tracking and optimization analysis to enable production deployment readiness and cost-efficient contract verification.

Motivation

Current State:

• No gas modeling in verification
• Unknown gas costs for verified contracts
• No optimization guidance
• Can't prove gas bounds

Production Need:

• Gas costs affect deployment viability
• Users care about transaction costs
• Optimization opportunities unknown
• Competitive disadvantage vs hand-written Solidity

Proposed Implementation

Phase 1: Gas Cost Model (from EVMYulLean)

Reuse EVMYulLean's gas model:

-- File: DumbContracts/EVM/GasCosts.lean

import EVMYulLean.EVM.GasCosts

def gasCost : YulStmt → Nat
  | .assign _ _ => 3              -- PUSH, DUP, SWAP
  | .storageLoad _ _ => 100       -- SLOAD (warm)
  | .storageStore _ _ => 100      -- SSTORE (warm, no change)
  | .if_ cond body => 
      gasCost cond + 10 + gasCost body  -- JUMPI
  | .for_ init cond post body =>
      gasCost init + n * (gasCost cond + gasCost body + gasCost post)

Phase 2: Gas Tracking in Compiler

Add gas annotations:

-- File: Compiler/GasAnnotation.lean

structure GasAnnotatedStmt where
  stmt : YulStmt
  estimatedGas : Nat
  worstCaseGas : Nat

def annotateGas : YulStmt → GasAnnotatedStmt := ...

theorem gas_bounded (stmt : YulStmt) :
    actualGas stmt ≤ worstCaseGas (annotateGas stmt)

Phase 3: Optimization Analysis

Identify optimization opportunities:

-- File: Compiler/Optimization/Analysis.lean

inductive Optimization where
  | StoragePackaging : List (Nat × Uint256) → Optimization  -- Pack into fewer slots
  | MemoryReuse : List Identifier → Optimization            -- Reuse memory slots
  | ConstantFolding : YulExpr → Optimization                 -- Fold at compile time
  | DeadCodeElimination : YulStmt → Optimization             -- Remove unused code

def findOptimizations : YulProgram → List Optimization := ...

Prove optimizations preserve semantics:

theorem optimization_preserves_semantics (opt : Optimization) :
    let optimized := applyOptimization opt program
    ∀ state, exec state program = exec state optimized

Phase 4: Gas Profiling in Tests

Add gas measurement:

// test/Gas*.t.sol

function test_transfer_gas() public {
    uint256 gasBefore = gasleft();
    ledger.transfer(recipient, amount);
    uint256 gasUsed = gasBefore - gasleft();
    
    // Assert gas bounds
    assertLt(gasUsed, EXPECTED_GAS_BOUND);
}

Generate gas report:

# scripts/gas_report.py

def generate_gas_report():
    """Generate gas usage report for all functions"""
    for contract in contracts:
        for function in contract.functions:
            print(f"{function}: {avg_gas} ± {std_dev}")

Gas Cost Categories

Storage Operations (Most Expensive)

Operation	Cold Cost	Warm Cost	Note
SLOAD	2,100	100	First access vs subsequent
SSTORE (zero→non-zero)	20,000	-	Most expensive
SSTORE (non-zero→non-zero)	5,000	-	Modify existing
SSTORE (non-zero→zero)	-15,000	-	Gas refund

Memory Operations

Operation	Cost	Note
MLOAD	3	Load from memory
MSTORE	3	Store to memory
Memory expansion	3 + quadratic	Increases with size

Computation

Operation	Cost	Note
ADD, SUB, MUL	3-5	Basic arithmetic
DIV, MOD	5	Division
SHA3 (KECCAK)	30 + 6/word	Hash function
ECRECOVER	3,000	Signature verification

Optimization Strategies

Strategy 1: Storage Packing

Problem: Each storage slot costs ~2,100 gas (cold)

Solution: Pack multiple values in one slot

-- Before: 3 slots (6,300 gas cold)
slot0: totalSupply (256 bits)
slot1: paused (8 bits)  -- Waste!
slot2: owner (160 bits) -- Waste!

-- After: 1 slot (2,100 gas cold)
slot0: [totalSupply (96 bits) | paused (8 bits) | owner (160 bits)]
-- Savings: 4,200 gas

Strategy 2: Memory Reuse

Problem: Memory expansion is quadratic

Solution: Reuse memory slots

-- Reuse temporary memory locations
let temp1 := mload(0x00)
-- ... use temp1 ...
let temp2 := mload(0x00)  -- Reuse same slot

Strategy 3: Constant Folding

Problem: Runtime computation costs gas

Solution: Compute at compile time

-- Before: Runtime computation
let x := add(mul(5, 3), 7)  -- 3 + 5 = 8 gas

-- After: Compile-time fold
let x := 22  -- 3 gas
-- Savings: 5 gas per occurrence

Strategy 4: Short-Circuit Evaluation

Problem: Expensive checks execute even when unnecessary

Solution: Order checks by cost (cheap first)

-- Before:
require(expensiveCheck() && cheapCheck())  -- Both execute

-- After:
require(cheapCheck() && expensiveCheck())  -- Short-circuit if cheap fails

Benefits

✅ Production deployment readiness
✅ Cost-competitive with hand-written Solidity
✅ Optimization opportunities identified
✅ Proven gas bounds (safety property)
✅ User confidence (predictable costs)

Implementation Plan

Phase 1: Gas Model (1 week)

• Import EVMYulLean gas costs
• Implement gas tracking

Phase 2: Compiler Integration (2 weeks)

• Annotate generated Yul
• Prove gas bounds

Phase 3: Optimization (2 weeks)

• Implement optimizations
• Prove semantic preservation

Phase 4: Testing & Reporting (1 week)

• Gas profiling tests
• Generate reports
• Documentation

Files Affected

Create:

• DumbContracts/EVM/GasCosts.lean
• Compiler/GasAnnotation.lean
• Compiler/Optimization/Analysis.lean
• scripts/gas_report.py
• test/Gas*.t.sol

Update:

• Compiler/YulGeneration.lean (add gas annotations)

Dependencies

• [Integration] Integrate EVMYulLean UInt256 arithmetic library #67: EVMYulLean integration (for gas model)
• [Infrastructure] Formal Yul-to-Bytecode verification (eliminate solc trust) #76: Bytecode verification (for accurate gas)

Estimated Effort

6 weeks

Success Criteria

• Gas costs tracked for all operations
• Gas bounds proven
• Optimizations preserve semantics
• Gas reports generated
• Competitive with hand-written Solidity

Related Issues

• Part of EVMYulLean integration ([Integration] Integrate EVMYulLean UInt256 arithmetic library #67)
• Enables production deployments
• Complements [Documentation] Document trust assumptions and verification boundaries #68 (trust assumptions)

Future Work

• Auto-optimization (apply proven optimizations)
• Gas budgeting (fail compilation if too expensive)
• Gas attack resistance (prove DoS bounds)

[Th0rgal]

Review Findings

1. Wrong File Paths

All DumbContracts/ → Verity/:

• DumbContracts/EVM/GasCosts.lean → Verity/EVM/GasCosts.lean

2. Depends on EVMYulLean (Not Available)

Phase 1 proposes reusing "EVMYulLean's gas model." EVMYulLean is not a dependency of this project. This creates a cascading dependency: #67 and #71 must be completed first (both also blocked on EVMYulLean integration).

3. Low Priority — Correctly Placed in Phase 4

Gas modeling is a nice-to-have for production readiness but doesn't affect verification correctness. The 6-week estimate and Phase 4 placement seem appropriate.

[Th0rgal]

Duplicate of #174 (No gas modeling). Both track the same gap. Closing this in favor of #174 which has more detail.