Verity

https://verity.thomas.md
Admin
Verity is a formal verification framework that enables developers to write smart contracts with...
Tokens:47,364
Snippets:417
Trust Score:5.5
Update:7 months ago
Show doc for...
Tokens:
Raw
### Install Foundry Framework

Source: https://verity.thomas.md/getting-started

Commands to install Foundry, the framework used for compiling and testing Solidity contracts.

```bash
curl -L https://foundry.paradigm.xyz | bash
foundryup
forge --version
```

--------------------------------

### Install Solidity Compiler via solc-select

Source: https://verity.thomas.md/getting-started

Commands to install and configure a specific version of the Solidity compiler required for differential testing.

```bash
pip3 install solc-select
solc-select install 0.8.33
solc-select use 0.8.33
solc --version
```

--------------------------------

### Build Project and Verify Proofs

Source: https://verity.thomas.md/getting-started

Commands to clone the repository, build the project using Lake, and verify specific proof files.

```bash
git clone https://github.com/Th0rgal/verity.git
cd verity
lake build
lake build Verity.Proofs.SimpleStorage.Basic
```

--------------------------------

### Install Lean 4 Toolchain

Source: https://verity.thomas.md/getting-started

Commands to install the Lean toolchain manager (elan) and verify the installation.

```bash
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
source ~/.elan/env
lean --version
```

--------------------------------

### SimpleStorage Contract Implementation

Source: https://verity.thomas.md/examples

Implements a basic storage contract with get and set operations for a single Uint256 value. It utilizes `StorageSlot` for managing state and provides `store` and `retrieve` functions. Proofs focus on roundtrip functionality and state isolation.

```Lean
def storedData : StorageSlot Uint256 := ⟨0⟩

def store (value : Uint256) : Contract Unit := do
  setStorage storedData value

def retrieve : Contract Uint256 := do
  getStorage storedData
```

--------------------------------

### Minimal Failing Example Template in Lean

Source: https://verity.thomas.md/guides/debugging-proofs

A template for creating minimal failing examples when requesting help. It includes necessary imports, context definitions, the theorem to be proved, and placeholders for expected vs. actual outcomes, aiding in debugging and communication.

```lean
-- Minimal failing example for help requests
import Verity.Core

-- Context
def myDefinition : Type := ...

-- What I'm trying to prove
theorem my_theorem : myProperty := by
  unfold myDefinition
  simp
  -- ERROR: simp made no progress
  sorry

-- What I expected: ...
-- What I got: ...
```

--------------------------------

### Build and Verify Proofs

Source: https://verity.thomas.md/guides/first-contract

Command-line instructions for building the Lean project and auditing the codebase for incomplete proofs marked with 'sorry'.

```bash
lake build
grep -r "sorry" Contracts/TipJar/
```

--------------------------------

### Define Contract in Lean

Source: https://verity.thomas.md/getting-started

Example of defining a simple storage contract using the Verity EDSL in Lean.

```lean
-- A contract with a single uint256 storage slot
def store (value : Uint256) : Contract Unit := setStorage storedData value
def retrieve : Contract Uint256 := getStorage storedData
```

--------------------------------

### Example: Updating Oracle Prices (Lean)

Source: https://verity.thomas.md/edsl-api-reference

Shows an example of reading a price from a `Uint256`-keyed mapping and then updating it, applicable for scenarios like price feeds or item lookups.

```lean
let price <- getMappingUint oraclePrices tokenId
setMappingUint oraclePrices tokenId newPrice
```

--------------------------------

### Example: Updating Allowances (Lean)

Source: https://verity.thomas.md/edsl-api-reference

Provides an example of reading an allowance from a double-keyed mapping and then updating it, demonstrating how to manage delegated permissions.

```lean
let allow <- getMapping2 allowances owner spender
setMapping2 allowances owner spender (allow - amount)
```

--------------------------------

### Import Contract Components in Lean (Lean)

Source: https://verity.thomas.md/guides/first-contract

Demonstrates how to import necessary components of the TipJar contract into other Lean files. This includes importing specifications, invariants, the contract itself, and related proofs.

```lean
import Contracts.TipJar.Spec
import Contracts.TipJar.Invariants
import Contracts.TipJar.TipJar
import Contracts.TipJar.Proofs.Basic
import Contracts.TipJar.Proofs.Correctness
```

--------------------------------

### Run Test Suite

Source: https://verity.thomas.md/getting-started

Commands to execute the project's test suite, including property-based differential tests and unit tests.

```bash
# All tests
FOUNDRY_PROFILE=difftest forge test

# Unit tests only
forge test --no-match-path "test/Property*" --no-match-path "test/Differential*" --no-match-path "test/CallValue*" --no-match-path "test/CalldataSize*" --no-match-path "test/yul/*"
```

--------------------------------

### Balance Check and Update Statement Example

Source: https://verity.thomas.md/compiler

An example combining multiple features to perform a balance check using `Stmt.require` and then update the balance using `Stmt.setMapping`. The example also includes `Stmt.stop` to terminate execution.

```lean
Stmt.require (Expr.ge (Expr.mapping "balances" Expr.caller) (Expr.param "amount")) "Insufficient",
Stmt.setMapping "balances" Expr.caller
  (Expr.sub (Expr.mapping "balances" Expr.caller) (Expr.param "amount")),
Stmt.stop
```

--------------------------------

### Implement TipJar Contract Logic in EDSL

Source: https://verity.thomas.md/guides/first-contract

Implements the TipJar contract using the Verity EDSL, featuring mapping storage for balances, sender identification, and modular arithmetic. Includes an example usage block for testing contract execution.

```lean
import Contracts.Common

namespace Contracts.TipJar

open Verity hiding pure bind
open Verity.EVM.Uint256

-- Storage layout: tips mapping at slot 0
def tips : StorageSlot (Address → Uint256) := ⟨0⟩

-- Deposit a tip: add amount to sender's balance
def tip (amount : Uint256) : Contract Unit := do
  let sender ← msgSender
  let currentBalance ← getMapping tips sender
  setMapping tips sender (add currentBalance amount)

-- Look up balance for any address
def getBalance (addr : Address) : Contract Uint256 := do
  getMapping tips addr

-- Example: Alice tips 100, then we check her balance
def exampleUsage : Contract Uint256 := do
  tip 100
  getBalance "0xAlice"

#eval (exampleUsage.run { defaultState with
  sender := "0xAlice",
  thisAddress := "0xTipJar"
}).getValue?

end Contracts.TipJar
```

--------------------------------

### Example: Incrementing a Uint256 Storage Slot (Lean)

Source: https://verity.thomas.md/edsl-api-reference

Provides an example of reading a `Uint256` storage slot, incrementing its value, and writing it back. This demonstrates a common pattern for state updates.

```lean
let x <- getStorage counterSlot
setStorage counterSlot (x + 1)
```

--------------------------------

### Common Lean Proof Patterns

Source: https://verity.thomas.md/guides/first-contract

Standard tactics and structures for writing Lean proofs, including simplification, case analysis on conditions, and the use of intermediate lemmas.

```lean
theorem simple_property : ... := by
  simp [functionName, helperFunctions]

theorem conditional_property : ... := by
  unfold functionName
  split
  · simp [...]
  · simp [...]

theorem main_property : ... := by
  have h1 := helper_lemma_1
  have h2 := helper_lemma_2
  simp [h1, h2, ...]
```

--------------------------------

### Compilation Examples with Library Linking

Source: https://verity.thomas.md/guides/linking-libraries

Practical examples of compiling contracts with and without external Yul libraries. Demonstrates the use of the --link flag and verbose output options.

```bash
# Compile without libraries
lake exe verity-compiler

# Compile with one library
lake exe verity-compiler --link examples/external-libs/PoseidonT3.yul

# Compile with multiple libraries, verbose output
lake exe verity-compiler \
    --link examples/external-libs/PoseidonT3.yul \
    --link examples/external-libs/PoseidonT4.yul \
    --link examples/external-libs/Groth16.yul \
    -v -o output/
```

--------------------------------

### CryptoHash External Library Linking

Source: https://verity.thomas.md/examples

Shows how to define a placeholder hash function that is replaced by an external Yul library call at compile time. This pattern is used for integrating external cryptographic primitives.

```Lean
def hashTwo (a b : Uint256) : Contract Uint256 := do
  return add a b

def storeHashTwo (a b : Uint256) : Contract Unit := do
  let h ← hashTwo a b
  setStorage lastHash h
```

--------------------------------

### Example: Updating an Owner Address (Lean)

Source: https://verity.thomas.md/edsl-api-reference

Illustrates reading an `Address` from a storage slot and then writing a new `Address` to it, commonly used for updating ownership or other address references.

```lean
let owner <- getStorageAddr ownerSlot
setStorageAddr ownerSlot newOwner
```

--------------------------------

### Initialize Verity Contract Project

Source: https://verity.thomas.md/guides/first-contract

Commands to generate a new contract structure using the Verity scaffold generator or manual file creation. This establishes the necessary directory hierarchy for specifications, proofs, and tests.

```bash
python3 scripts/generate_contract.py TipJar \
  --fields "tips:mapping" \
  --functions "tip(uint256),getBalance(address)"
```

```bash
mkdir -p Contracts/TipJar/Proofs
touch Contracts/TipJar/Spec.lean
touch Contracts/TipJar/Invariants.lean
touch Contracts/TipJar/SpecProofs.lean
touch Contracts/TipJar/TipJar.lean
touch Contracts/TipJar/Proofs/Basic.lean
touch Contracts/TipJar/Proofs/Correctness.lean
touch test/PropertyTipJar.t.sol
```

--------------------------------

### Counter Contract Implementation

Source: https://verity.thomas.md/examples

Implements a counter contract with increment and decrement operations. It uses read-modify-write logic on a `Uint256` storage slot. Proofs cover arithmetic, composition, and behavior at zero.

```Lean
def count : StorageSlot Uint256 := ⟨0⟩

def increment : Contract Unit := do
  let current ← getStorage count
  setStorage count (add current 1)

def decrement : Contract Unit := do
  let current ← getStorage count
  setStorage count (sub current 1)
```

--------------------------------

### Reentrancy Vulnerability and Safety Modeling

Source: https://verity.thomas.md/examples

Demonstrates how to model reentrancy vulnerabilities and prove safety properties. It includes a theorem for an existential attack witness and a universal safety proof for a reentrancy-safe withdrawal function.

```Lean
theorem vulnerable_attack_exists :
  ∃ (s : ContractState),
    s.storageMap balances.slot "attacker" = (Verity.EVM.MAX_UINT256 : Uint256) ∧
    s.storage totalSupply.slot = (Verity.EVM.MAX_UINT256 : Uint256) ∧
    supplyInvariant s ["attacker"] ∧
    let s' := (withdraw (Verity.EVM.MAX_UINT256 : Uint256)).runState s;
    ¬ supplyInvariant s' ["attacker"]

theorem withdraw_maintains_supply (amount : Uint256) :
  ∀ (s : ContractState),
    supplyInvariant s [s.sender] →
    s.storageMap balances.slot s.sender ≥ amount →
    supplyInvariant ((withdraw amount).runState s) [s.sender]
```

--------------------------------

### Test EDSL Implementation

Source: https://verity.thomas.md/guides/first-contract

Commands and patterns for building and evaluating the contract implementation. Uses the Lake build system and default state initialization for testing.

```bash
lake build Contracts.TipJar
```

```lean
#eval (myContract.run { defaultState with sender := "0xAlice" }).getValue?
```

--------------------------------

### SimpleToken Contract Implementation

Source: https://verity.thomas.md/examples

Implements a basic token contract with owner-controlled minting and supply tracking. It uses storage slots for balances and total supply, ensuring safe arithmetic operations during minting and transfers.

```Lean
def owner : StorageSlot Address := ⟨0⟩
def balances : StorageSlot (Address → Uint256) := ⟨1⟩
def totalSupply : StorageSlot Uint256 := ⟨2⟩

def mint (to : Address) (amount : Uint256) : Contract Unit := do
  onlyOwner
  let currentBalance ← getMapping balances to
  let newBalance ← requireSomeUint (safeAdd currentBalance amount) "Balance overflow"
  let currentSupply ← getStorage totalSupply
  let newSupply ← requireSomeUint (safeAdd currentSupply amount) "Supply overflow"
  setMapping balances to newBalance
  setStorage totalSupply newSupply

def transfer (to : Address) (amount : Uint256) : Contract Unit := do
  let sender ← msgSender
  let senderBalance ← getMapping balances sender
  require (senderBalance >= amount) "Insufficient balance"
  if sender == to then
    pure ()
  else
    let recipientBalance ← getMapping balances to
    let newRecipientBalance ← requireSomeUint (safeAdd recipientBalance amount) "Recipient balance overflow"
    setMapping balances sender (sub senderBalance amount)
    setMapping balances to newRecipientBalance
```

--------------------------------

### Ledger Contract Implementation

Source: https://verity.thomas.md/examples

Implements a ledger contract using mapping storage for per-address balances. It supports deposit, withdraw, and transfer operations with balance checks and modular arithmetic. Proofs cover balance guards, sum equations, and cancellation properties.

```Lean
def balances : StorageSlot (Address → Uint256) := ⟨0⟩

def deposit (amount : Uint256) : Contract Unit := do
  let sender ← msgSender
  let currentBalance ← getMapping balances sender
  setMapping balances sender (add currentBalance amount)  -- modular arithmetic (EVM)

def transfer (to : Address) (amount : Uint256) : Contract Unit := do
  let sender ← msgSender
  let senderBalance ← getMapping balances sender
  require (senderBalance >= amount) "Insufficient balance"
  if sender == to then
    pure ()
  else
    let recipientBalance ← getMapping balances to
    let newRecipientBalance ← requireSomeUint (safeAdd recipientBalance amount) "Recipient balance overflow"
    setMapping balances sender (sub senderBalance amount)
    setMapping balances to newRecipientBalance
```

--------------------------------

### Verity Compiler Backend Profile Configuration

Source: https://verity.thomas.md/compiler

Provides examples of how to configure backend profiles for the `verity-compiler` to achieve deterministic output-shape normalization. Different profiles offer varying levels of sorting and optimization passes.

```bash
# Default semantic profile
lake exe verity-compiler --backend-profile semantic

# Sort dispatch `case` blocks by selector
lake exe verity-compiler --backend-profile solidity-parity-ordering

# Sort selector cases + enable deterministic patch pass
lake exe verity-compiler-patched --backend-profile solidity-parity
```

--------------------------------

### Verify TipJar Contract Correctness in Lean

Source: https://verity.thomas.md/guides/first-contract

Formal proofs for the TipJar contract ensuring that state transitions and balance queries match the formal specification. These proofs use the Verity proof automation library to validate storage invariants and function behavior.

```lean
theorem tip_meets_spec (s : ContractState) (amount : Uint256) :
    tip_spec amount s (((tip amount).run s).snd) := by
  simp [tip, tip_spec, tips, msgSender, getMapping, setMapping, bind,
        Specs.storageMapUnchangedExceptKeyAtSlot,
        Specs.storageMapUnchangedExceptKey, Specs.storageMapUnchangedExceptSlot,
        Specs.sameStorageAddrContext, Specs.sameStorage, Specs.sameStorageAddr,
        Specs.sameContext]
  constructor
  · simp [Contract.run]
  · constructor
    · constructor
      · intro other hne; simp [*]
      · intro other hne addr; simp [*]
    · simp
```

--------------------------------

### Build and Compile Lean Code (Bash)

Source: https://verity.thomas.md/guides/first-contract

Commands to build the Lean project, ensuring all code compiles and proofs are complete. It also checks the Yul compiler and Verity compiler executables.

```bash
# 1. All Lean code compiles (including proofs)
lake build

# 2. No incomplete proofs
grep -r "sorry" Contracts/TipJar/

# 3. Yul generates and compiles
lake build verity-compiler
lake exe verity-compiler
python3 scripts/check_yul.py
```

--------------------------------

### Verity Proof: SimpleStorage retrieve (spec-based proof)

Source: https://verity.thomas.md/guides/debugging-proofs

Demonstrates a basic spec-based proof for the 'retrieve' operation in SimpleStorage. It shows how to prove that the operation returns the stored value by comparing the result against the 'retrieve_spec' predicate. This example highlights the use of 'simp' for straightforward proofs.

```lean
def retrieve_spec (result : Uint256) (s : ContractState) : Prop :=
  result = s.storage storedData.slot

theorem retrieve_meets_spec (s : ContractState) :
  let result := ((retrieve).run s).fst
  retrieve_spec result s := by
  simp [retrieve, storedData, retrieve_spec]
```

--------------------------------

### Import Verity and Uint256 Modules in Lean (Lean)

Source: https://verity.thomas.md/guides/first-contract

Shows how to import and open namespaces for the Verity framework and its Uint256 module within Lean proofs. This is crucial for resolving 'Unknown identifier' errors.

```lean
import Contracts.TipJar.Spec
import Contracts.TipJar.TipJar

open Verity
open Verity.EVM.Uint256
```

--------------------------------

### Proof Debugging with unfold and simp (Lean)

Source: https://verity.thomas.md/guides/first-contract

Provides a strategy for debugging Lean proofs that fail to close with `simp`. The approach involves using `unfold` to expose definitions and then applying `simp` with specific lemmas.

```lean
theorem my_thm : ... := by
  unfold myFunction bind
  simp [getMapping, setMapping, msgSender, tips]
```

--------------------------------

### Compile to EVM Bytecode

Source: https://verity.thomas.md/getting-started

Command to run the Verity compiler to generate Yul artifacts from Lean definitions.

```bash
lake exe verity-compiler
cat artifacts/yul/SimpleStorage.yul
```

--------------------------------

### Define Verity Contract

Source: https://verity.thomas.md/guides/first-contract

Example of defining a smart contract using the verity_contract macro, specifying storage slots and function logic.

```lean
verity_contract TipJar where
  storage
    tips : Address -> Uint256 := slot 0

  function tip (amount : Uint256) : Unit := do
    let sender <- msgSender
    let current ← getMapping tips sender
    setMapping tips sender (add current amount)

  function getBalance (addr : Address) : Uint256 := do
    return (← getMapping tips addr)
```

--------------------------------

### Proving Storage Equality Using Function Extensionality in Lean

Source: https://verity.thomas.md/guides/debugging-proofs

Demonstrates the use of the `ext` tactic in Lean to prove the equality of two storage states. It involves iterating through each slot and proving equality for a target slot and unchanged status for other slots.

```lean
-- Goal: state1.storage = state2.storage
theorem storage_equal : state1.storage = state2.storage := by
  ext slot  -- For all slots
  by_cases h : slot = targetSlot
  · simp [h]  -- Show target slot is equal
  · simp [h]  -- Show other slots unchanged
```

--------------------------------

### Build and Execute Compiler

Source: https://verity.thomas.md/research

These bash commands demonstrate how to build the Verity compiler using 'lake build' and then execute it to generate contracts. The final command shows how to run tests using Foundry.

```bash
lake build verity-compiler    # Build compiler
lake exe verity-compiler      # Generate all contracts
FOUNDRY_PROFILE=difftest forge test
```

--------------------------------

### Optimize Tactic Ordering

Source: https://verity.thomas.md/guides/debugging-proofs

Demonstrates the preferred way to use 'simp' by passing definitions directly, and the fallback 'unfold' method for complex definitions.

```lean
theorem retrieve_meets_spec (s : ContractState) :
  let result := ((retrieve).run s).fst
  retrieve_spec result s := by
  simp [retrieve, storedData, retrieve_spec]

theorem good_order : getValue state = value := by
  unfold getValue
  simp [getStorage]
```

--------------------------------

### Compile Contract to Yul/EVM

Source: https://verity.thomas.md/getting-started

Utilizes the Lake build system to compile Verity contracts into Yul bytecode. Supports standard compilation and advanced scenarios involving external library linking.

```bash
lake build verity-compiler
lake exe verity-compiler          # Output in artifacts/yul/
```

```bash
lake exe verity-compiler --link examples/external-libs/PoseidonT3.yul -o artifacts/yul
```

--------------------------------

### Lean Goal Inspection and Proof Skipping

Source: https://verity.thomas.md/guides/debugging-proofs

Illustrates how to inspect the current state of a proof and temporarily skip steps. Useful for understanding the proof context and identifying what needs to be proven.

```lean
-- In a proof, inspect current state
theorem my_theorem : ... := by
  trace "{goal}"                -- Print current goal
  trace "Variable x: {x}"       -- Print specific variable
  sorry                         -- Skip temporarily to see what's needed
```

--------------------------------

### Lean Omega Tactic: Using Intermediate Lemmas

Source: https://verity.thomas.md/guides/debugging-proofs

Demonstrates how to assist the `omega` tactic by introducing intermediate lemmas that provide necessary context or break down complex constraints into simpler, linear ones.

```lean
-- Help omega with explicit steps
theorem with_helper : a + b < MAX := by
  have h1 : a < MAX / 2 := by assumption
  have h2 : b < MAX / 2 := by assumption
  omega  -- Now has enough context
```

--------------------------------

### Verify Compilation using Python Script

Source: https://verity.thomas.md/guides/first-contract

This snippet demonstrates how to verify the compilation process using a Python script. It executes the 'check_yul.py' script located in the 'scripts' directory. Ensure Python 3 is installed and accessible in your environment.

```bash
python3 scripts/check_yul.py
```

--------------------------------

### Contract Proof Unfolding Techniques in Lean

Source: https://verity.thomas.md/research

Demonstrates the primary proof strategies for the EDSL, including full unfolding of contract primitives and the use of private helper theorems to simplify state transitions.

```lean
simp only [operation, onlyOwner, isOwner, owner,
  msgSender, getStorageAddr, setStorage,
  Verity.bind, Bind.bind, Pure.pure,
  Contract.run, ContractResult.snd]
simp [h_owner]
```

```lean
private theorem increment_unfold (s : ContractState)
  (h_owner : s.sender = s.storageAddr 0) :
  (increment.run s) = ContractResult.success () { ... } := by
  simp only [increment, ...]; simp [h_owner]
```

--------------------------------

### Generate Contract Scaffold

Source: https://verity.thomas.md/getting-started

Uses the Python generation script to create the necessary Lean EDSL files, specification files, and Solidity test stubs for a new contract. The command requires the contract name, field definitions, and function signatures as inputs.

```bash
python3 scripts/generate_contract.py TipJar \
  --fields "tips:mapping" \
  --functions "tip(uint256),getBalance(address)"
```

--------------------------------

### Proving Sequential Storage Operations in Lean

Source: https://verity.thomas.md/guides/debugging-proofs

Illustrates how to prove the outcome of sequential storage operations in Lean. It involves chaining `_meets_spec` lemmas using `have` and `calc` or directly unfolding bind operations for low-level proofs.

```lean
-- Actual pattern from Counter/Basic.lean
theorem increment_twice_adds_two (s : ContractState) :
  let s' := ((increment).run s).snd
  let s'' := ((increment).run s').snd
  s''.storage 0 = EVM.Uint256.add (EVM.Uint256.add (s.storage 0) 1) 1 := by
  have h1 := increment_adds_one s                         -- First op
  have h2 := increment_adds_one (((increment).run s).snd) -- Second op
  calc ... = ... := h2
    _ = ... := by rw [h1]

-- For low-level multi-update proofs, unfold bind directly:
theorem two_updates (s : ContractState) :
  let s' := ((do setStorage slot1 val1; setStorage slot2 val2).run s).snd
  s'.storage slot2.slot = val2 := by
  simp [bind, Bind.bind, setStorage, Contract.run, ContractResult.snd]
```

--------------------------------

### Read and Write Mapping Entries Directly from Storage (Solidity/Yul)

Source: https://verity.thomas.md/guides/first-contract

Provides functions to directly read and write mapping entries from contract storage using Solidity and Yul. It leverages Foundry's vm.load and vm.store cheatcodes for direct storage manipulation, useful for test setup and assertions. The mapping slot formula `keccak256(abi.encode(key, baseSlot))` is central to these operations.

```Solidity
/// @notice Read a mapping(address => uint256) entry directly from storage
/// @dev TipJar uses slot 0 for the tips mapping.
///      Solidity/Yul mapping layout: keccak256(abi.encode(key, baseSlot))
function getBalanceFromStorage(address addr) internal view returns (uint256) {
    bytes32 slot = keccak256(abi.encode(addr, uint256(0)));
    return uint256(vm.load(tipjar, slot));
}

/// @notice Write a mapping entry directly (for test setup)
function setBalance(address addr, uint256 amount) internal {
    bytes32 slot = keccak256(abi.encode(addr, uint256(0)));
    vm.store(tipjar, slot, bytes32(amount));
}
```

--------------------------------

### Logging Intermediate Goal States in Lean

Source: https://verity.thomas.md/guides/debugging-proofs

Shows how to log intermediate goal states during proof execution using the `trace` command. This is valuable for debugging complex proofs by observing how the goal changes after each tactic application.

```lean
-- Log intermediate states
theorem complex_proof : ... := by
  trace "Initial goal: {goal}"
  unfold definition1
  trace "After unfold: {goal}"
  simp
  trace "After simp: {goal}"
  omega
```

--------------------------------

### Handle Option Types in Proofs

Source: https://verity.thomas.md/guides/debugging-proofs

Shows how to handle Option types by checking if a value exists, using 'cases' to safely extract values or handle contradictions.

```lean
theorem option_proof (opt : Option α) (h : opt.isSome) :
    opt.get! = value := by
  cases opt
  · contradiction
  · simp
```

--------------------------------

### Lean Omega Tactic: Converting Inequalities

Source: https://verity.thomas.md/guides/debugging-proofs

Explains how the `omega` tactic prefers less-than-or-equal-to (`≤`) over strictly less-than (`<`) and shows how to convert inequalities accordingly.

```lean
-- omega prefers ≤ over <
have h : a + b ≤ MAX := by omega
have h' : a + b < MAX + 1 := by omega
```

--------------------------------

### Lean Simp Tactic: Adding Simp Attributes and Lemmas

Source: https://verity.thomas.md/guides/debugging-proofs

Shows how to mark lemmas with the `simp` attribute for automatic application and how to explicitly provide lemmas to the `simp` tactic for simplification.

```lean
-- Mark lemma for automatic simplification
@[simp] theorem my_helper_lemma : a + 0 = a := ...

-- Now simp will use it automatically
theorem uses_helper : ... := by
  simp  -- Automatically applies my_helper_lemma

-- Be explicit about what to simplify
simp [myDefinition, myLemma1, myLemma2]
```

--------------------------------

### Context Accessor Example

Source: https://verity.thomas.md/edsl-api-reference

Demonstrates the usage of context accessors like `msgSender` and `msgValue` in a Lean code snippet. This example shows how to retrieve the sender's address and the message value within a contract.

```lean
let from <- msgSender
let value <- msgValue
```

--------------------------------

### If/Else Branching Statement Example

Source: https://verity.thomas.md/compiler

An example demonstrating conditional execution using `Stmt.ite` for if/else branching. It checks if the caller is the owner and, if true, sets the 'paused' storage variable to 1 and stops execution. Otherwise, it implicitly does nothing further in this snippet.

```lean
Stmt.ite (Expr.eq Expr.caller (Expr.storage "owner"))
  [Stmt.setStorage "paused" (Expr.literal 1), Stmt.stop]
```

--------------------------------

### Proof Term Inspection using #print in Lean

Source: https://verity.thomas.md/guides/debugging-proofs

Demonstrates how to inspect the proof term generated by Lean using the `#print` command. This is useful for understanding the structure of a proof and manually constructing or verifying proof terms.

```lean
-- See the proof term Lean generates
#print my_theorem  -- Shows proof term

-- Check if proof is what you expect
example : ... := proof_term  -- Manually write proof term
```

--------------------------------

### Lean Evaluation and Equivalence Checking

Source: https://verity.thomas.md/guides/debugging-proofs

Shows how to evaluate functions and check for definitional equality in Lean. Useful for testing function behavior and verifying simple equivalences.

```lean
-- Test functions
#eval myFunction arg1 arg2      -- Runs the function

-- Check equivalence
example : expr1 = expr2 := rfl  -- Definitional equality
```

--------------------------------

### Lean Omega Tactic: Handling Non-Linear Arithmetic

Source: https://verity.thomas.md/guides/debugging-proofs

Illustrates how to resolve issues with the `omega` tactic when dealing with non-linear arithmetic by splitting the problem into linear cases using `by_cases`.

```lean
-- ❌ DOESN'T WORK (non-linear)
theorem complex_bound : a * b ≤ MAX := by
  omega  -- Error: not linear arithmetic

-- ✅ WORKS (split cases)
theorem complex_bound : a * b ≤ MAX := by
  by_cases ha : a = 0
  · simp [ha]     -- a = 0 case is trivial
  · by_cases hb : b = 0
    · simp [hb]   -- b = 0 case is trivial
    · omega       -- Now linear constraints only
```

--------------------------------

### Function Selector Examples

Source: https://verity.thomas.md/compiler

This snippet provides examples of function selectors, which are the first four bytes of the Keccak-256 hash of a Solidity function's signature. These selectors are used to identify and dispatch function calls. The selectors shown are pre-computed and validated against `solc --hashes`.

```text
"store(uint256)" → 0x6057361d
"retrieve()" → 0x2e64cec1
```

--------------------------------

### Yul Linker: Code Injection Example

Source: https://verity.thomas.md/guides/linking-libraries

Demonstrates how the Verity linker injects external library functions into the compiled Yul contract's runtime code section. The example shows the `myHash` function from `MyHash.yul` being added with proper indentation within the `code {}` block of the `runtime` object.

```yul
object "MyContract" {
    code { /* deploy */ }
    object "runtime" {
        code {
            // ... generated contract code ...

            // Injected from MyHash.yul:
            function myHash(a, b) -> result {
                result := add(xor(a, b), 0x42)
            }
        }
    }
}
```

--------------------------------

### Proving Safe Addition Success in Lean

Source: https://verity.thomas.md/guides/debugging-proofs

Demonstrates a common pattern for proving that `safeAdd` returns `some c`. It requires establishing that the addition `a.val + b.val` does not exceed `MAX_UINT256` and then using `rfl` to complete the proof.

```lean
-- Goal: safeAdd a b = some c
theorem safeAdd_proof (h : a.val + b.val ≤ MAX_UINT256) :
    safeAdd a b = some ⟨a.val + b.val, by omega⟩ := by
  unfold safeAdd
  simp [willAddOverflow_eq_false h]
  -- Now prove the value is correct
  rfl
```

--------------------------------

### Bytecode Deployment Commands

Source: https://verity.thomas.md/compiler

These bash commands illustrate how to compile the generated Yul code into bytecode using 'solc' and then deploy that bytecode to an Ethereum network using 'forge'. The 'forge create' command requires specifying the contract name and the originating address and private key for the deployment transaction.

```bash
# Compile Yul to bytecode
solc --strict-assembly SimpleStorage.yul

# Deploy to Ethereum (local, testnet, or mainnet)
forge create SimpleStorage --from 0x... --private-key ...
```

--------------------------------

### Generate Yul Artifacts

Source: https://verity.thomas.md/guides/first-contract

Commands to compile the Verity project and generate Yul code for the defined contracts.

```bash
lake build verity-compiler
lake exe verity-compiler
ls artifacts/yul/TipJar.yul
```

--------------------------------

### Perform Structural Induction on Lists

Source: https://verity.thomas.md/guides/debugging-proofs

Demonstrates list induction by handling the empty list (nil) and the recursive cons case.

```lean
theorem by_list_induction (xs : List α) : Q xs := by
  induction xs with
  | nil =>
      simp [Q]
  | cons head tail ih =>
      simp [Q, ih]
```

--------------------------------

### Validate Contract and Tests

Source: https://verity.thomas.md/add-contract

Commands to verify the integrity of the Lean implementation, execute differential tests, and check property test coverage.

```bash
# 1. Lean code compiles
lake build

# 2. Differential tests pass
FOUNDRY_PROFILE=difftest forge test --match-contract Differential<Name>

# 3. Property tests pass
FOUNDRY_PROFILE=difftest forge test --match-contract Property<Name>

# 4. Regenerate property manifest and validate
python3 scripts/extract_property_manifest.py
python3 scripts/check_property_manifest.py
python3 scripts/check_property_manifest_sync.py
python3 scripts/check_property_coverage.py
```

--------------------------------

### Tactic Tracing for Simplification in Lean

Source: https://verity.thomas.md/guides/debugging-proofs

Enables detailed tracing of the `simp` tactic to observe all simplification steps during proof execution. This helps in understanding why `simp` might not be making progress or to debug complex simplification sequences.

```lean
-- Enable tactic tracing
set_option trace.Meta.Tactic.simp true

theorem my_theorem : ... := by
  simp  -- Will show all simplification steps
```

--------------------------------

### Debugging Type Mismatches in Lean

Source: https://verity.thomas.md/guides/debugging-proofs

Demonstrates how to debug and resolve type mismatches in Lean. It shows how to use `#check` to inspect types and how to apply explicit coercions using `ofNat` to resolve type errors.

```lean
-- Use #check to debug
#check myValue      -- Expected: Uint256, Got: Nat

-- Add explicit coercion
example : Uint256 := ofNat myNatValue  -- ✅
```

--------------------------------

### Example: Transferring Balances with Mappings (Lean)

Source: https://verity.thomas.md/edsl-api-reference

Demonstrates reading a balance from an address-keyed mapping and then updating it, simulating a token transfer operation.

```lean
let bal <- getMapping balances msgSenderAddr
setMapping balances msgSenderAddr (bal - amount)
```

--------------------------------

### Run Foundry Tests After Build (Bash)

Source: https://verity.thomas.md/guides/first-contract

Executes the Foundry tests for the TipJar contract after the build process to ensure integration and correctness.

```bash
FOUNDRY_PROFILE=difftest forge test --match-contract TipJar
```

--------------------------------

### Define Storage Slots in Lean

Source: https://verity.thomas.md/guides/solidity-to-verity

Defines storage slots for balances and total supply in a Lean smart contract. These slots are used to store contract state variables.

```lean
def balances : StorageSlot (Address → Uint256) := ⟨0⟩
def totalSupply : StorageSlot Uint256 := ⟨1⟩
```

--------------------------------

### Verify Authorization Logic in Lean

Source: https://verity.thomas.md/guides/debugging-proofs

Demonstrates how to prove that an operation succeeds when the sender is authorized. It uses the 'unfold' tactic to expose definitions and 'simp' to resolve the authorization check.

```lean
theorem authorized_succeeds (state : ContractState) (sender : Address)
    (h : state.storageAddr owner.slot = sender) :
    ((operation sender).run state).isSuccess = true := by
  unfold operation onlyOwner require
  simp [h]
  -- Prove rest of operation
```
Tokens:
Raw