### Install Foundry Framework

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/getting-started.mdx

Installs the Foundry toolchain for Solidity testing and compilation, which is required for property-based differential tests.

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

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

### Install Dependencies and Start Dev Server (npm/bun)

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/README.md

Commands to install project dependencies using either npm or bun, and to start the development server. This is a common setup step for Next.js projects.

```bash
# Install dependencies
npm install
# or
bun install

# Start dev server
npm run dev
# or
bun dev
```

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

### Build Verity Project

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/getting-started.mdx

Clones the repository and uses the Lake build system to download dependencies and compile the project.

```bash
git clone https://github.com/Th0rgal/verity.git
cd verity
lake build
```

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

### Install Lean 4 Toolchain

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/getting-started.mdx

Installs the elan toolchain manager and verifies the Lean 4 installation to ensure compatibility with the project's pinned toolchain.

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

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

### Install Solidity Compiler via solc-select

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/getting-started.mdx

Installs and configures the specific version of the Solidity compiler required for differential testing in the Verity project.

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

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

### Minimal Lean proof example template

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/guides/debugging-proofs.mdx

A template for creating minimal failing examples when requesting help with Lean proofs.

```lean
import Verity.Core

def myDefinition : Type := ...

theorem my_theorem : myProperty := by
  unfold myDefinition
  simp
  sorry
```

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

### Build and Start Production Server (npm)

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/README.md

Commands to build the project for production and start the production server using npm. This is typically done after development is complete.

```bash
npm run build
npm start
```

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

### Example Lean Proof Snippet

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/index.mdx

Demonstrates a simplified example of a proof in Lean, showing how to define a theorem and use tactics like `unfold` and `simp` to prove it. This illustrates the core proof mechanism used in the project.

```lean
-- Claim: After storing 42, retrieving gives 42
theorem store_retrieve : store 42 >> retrieve = pure 42 := by
  unfold store retrieve  -- Expand definitions
  simp                   -- Simplify with built-in rules
  -- Proof complete

```

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

### Verify and Compile Contracts

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/getting-started.mdx

Commands to verify specific Lean proofs and execute the Verity compiler to generate Yul artifacts.

```bash
lake build Verity.Proofs.SimpleStorage.Basic
lake exe verity-compiler
cat artifacts/yul/SimpleStorage.yul
```

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

### Run Test Suite

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/getting-started.mdx

Executes the test suite using Foundry, including options for running property tests with FFI or filtering tests to exclude specific categories.

```bash
FOUNDRY_PROFILE=difftest forge test
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/*"
```

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

### Simp Lemmas for Storage and Require (Lean)

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/core.mdx

Examples of `@[simp]` lemmas used in proofs. These lemmas provide simplified forms for `getStorage` and `require` operations, proving their success or revert outcomes directly. The full-result forms are preferred for proofs.

```lean
-- Full-result form (preferred for new proofs):
@[simp] theorem getStorage_run (s : StorageSlot Uint256) (state : ContractState) :
  (getStorage s).run state = ContractResult.success (state.storage s.slot) state := rfl

@[simp] theorem require_true (msg : String) (s : ContractState) :
  (require true msg).run s = ContractResult.success () s := rfl

@[simp] theorem require_false (msg : String) (s : ContractState) :
  (require false msg).run s = ContractResult.revert msg s := rfl
```

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

### Storage Slot Inference and Constructor Parameters

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/compiler.mdx

Examples showing how the compiler automatically infers storage slots based on field order and handles constructor parameters via deployment bytecode arguments.

```lean
fields := [
  { name := "owner", ty := FieldType.address },     -- slot 0
  { name := "balances", ty := FieldType.mappingTyped (.simple .address) },  -- slot 1
  { name := "totalSupply", ty := FieldType.uint256 } -- slot 2
]

constructor := some {
  params := [{ name := "initialOwner", ty := ParamType.address }]
  body := [
    Stmt.setStorage "owner" (Expr.constructorArg 0)
  ]
}
```

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

### Implement SimpleToken with Minting and Transfers

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/examples.mdx

Demonstrates a token contract using Owned and Ledger patterns. It includes minting and transfer logic with supply tracking and overflow protection.

```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
```

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

### Integrate External Libraries via Linking

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/examples.mdx

Shows how to use placeholder functions in the EDSL that are replaced by external Yul helper functions (like Poseidon) during the compilation linking phase.

```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
```

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

### Implement TipJar Contract Logic in EDSL

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/guides/first-contract.mdx

Implements the TipJar contract using the Verity EDSL, featuring a mapping-based balance ledger. Includes functions for depositing tips, querying balances, and an example usage block for testing.

```lean
def tips : StorageSlot (Address → Uint256) := ⟨0⟩

def tip (amount : Uint256) : Contract Unit := do
  let sender ← msgSender
  let currentBalance ← getMapping tips sender
  setMapping tips sender (add currentBalance amount)

def getBalance (addr : Address) : Contract Uint256 := do
  getMapping tips addr

def exampleUsage : Contract Uint256 := do
  tip 100
  getBalance "0xAlice"
```

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

### Define SimpleStorage Contract in Lean

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/getting-started.mdx

Example of a Lean contract definition using the Verity EDSL to manage storage state.

```lean
def store (value : Uint256) : Contract Unit := setStorage storedData value
def retrieve : Contract Uint256 := getStorage storedData
```

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

### Runtime Contract Helper Documentation

Source: https://github.com/lfglabs-dev/verity/blob/main/docs/GENERIC_LAYER2_PLAN.md

Lemmas and theorems documenting the helper-free runtime constructor and the conservative extension proofs for the current theorem stack.

```Lean
Dispatch.runtimeContractOfFunctions(internalFunctions = [])
interpretIRWithInternalsZeroConservativeExtensionGoal_closed
compile_preserves_semantics_with_helper_proofs_and_helper_ir_supported
```

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

### Sequential Storage Operations

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/guides/debugging-proofs.mdx

Demonstrates how to chain lemmas for sequential storage updates or unfold bind operations directly for low-level proofs.

```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
  have h2 := increment_adds_one (((increment).run s).snd)
  calc ... = ... := h2
    _ = ... := by rw [h1]
```

```lean
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]
```

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

### Compile Contracts to Yul/EVM using Lake

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/getting-started.mdx

This command compiles Verity contracts to Yul/EVM format using the 'lake' build tool. The output is typically found in the 'artifacts/yul/' directory. For contracts requiring external libraries, specify the library path using the '--link' option.

```bash
lake build verity-compiler
```

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

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

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

### Adding Intermediate Lemmas for Omega Tactic in Lean

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/guides/debugging-proofs.mdx

Demonstrates how to introduce intermediate lemmas using `have` to provide `omega` with sufficient context to solve a goal. This is useful when the direct constraints are not immediately obvious to `omega`.

```lean
```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
```
```

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

### Generate First Contract with Python Script

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/getting-started.mdx

This script generates scaffold files for a new contract. It takes the contract name, field definitions, and function signatures as arguments. The output includes Lean files for EDSL implementation, formal specifications, invariants, proofs, and Solidity property tests.

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

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

### Translate ERC20 Transfer Logic

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/guides/solidity-to-verity.mdx

A comprehensive example showing the translation of an ERC20 transfer function from Solidity to the Verity EDSL, including state updates, requirement checks, and event emission.

```solidity
function transfer(address to, uint256 amount) external returns (bool) {
    require(balances[msg.sender] >= amount, "insufficient");
    balances[msg.sender] -= amount;
    balances[to] += amount;
    emit Transfer(msg.sender, to, amount);
    return true;
}
```

```lean
def transfer (to : Address) (amount : Uint256) : Contract Bool := do
  let sender <- msgSender
  let b <- getStorage balances
  require (b sender >= amount) "insufficient"
  let newSenderBal := b sender - amount
  let newToBal := b to + amount
  setStorage balances (fun k => if k == sender then newSenderBal else if k == to then newToBal else b k)
  emit [sender.toNat, to.toNat, amount.toNat]
  pure true
```

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

### Induction and Case Analysis

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/guides/debugging-proofs.mdx

Standard patterns for structural induction on natural numbers and lists, as well as boolean case splitting.

```lean
theorem by_nat_induction : ∀ n : Nat, P n := by
  intro n
  induction n with
  | zero => constructor; simp
  | succ k ih => constructor; simp [ih]

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

theorem by_bool_cases (b : Bool) : R b := by
  cases b
  · simp [R]
  · simp [R]
```

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

### SimpleStorage Contract in Lean

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/examples.mdx

Implements a basic storage mechanism with get and set operations for a single Uint256 value. It uses a StorageSlot to manage the data. Proofs cover 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
```

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

### Tactic Ordering

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/guides/debugging-proofs.mdx

Best practices for using simp and unfold tactics to ensure efficient proof simplification.

```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]
```

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

### Commit Type Examples

Source: https://github.com/lfglabs-dev/verity/blob/main/CONTRIBUTING.md

Examples of commit message types and formats used in the Verity project, including `feat`, `fix`, `proof`, `docs`, `refactor`, `test`, and `chore`.

```git
type: description

[optional body]

Co-Authored-By: Claude <noreply@anthropic.com>
```

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

### Full Unfolding Proof Technique in Lean

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/research.mdx

Demonstrates the primary proof technique of full unfolding, which leverages the shallow EDSL structure to simplify contract operations into core primitives.

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

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

### Fetch Prebuilt Compiler Artifacts

Source: https://github.com/lfglabs-dev/verity/blob/main/README.md

Downloads prebuilt compiler artifacts from CI to avoid local native code compilation, followed by running Foundry tests.

```bash
scripts/fetch_prebuilt_compiler_artifacts.sh main
FOUNDRY_PROFILE=difftest DIFFTEST_YUL_DIR=compiler/yul forge test
```

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

### Splitting Cases for Omega Tactic in Lean

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/guides/debugging-proofs.mdx

Illustrates how to use `by_cases` to split a goal into cases when the `omega` tactic fails due to non-linear arithmetic. This makes the constraints linear and solvable by `omega`.

```lean
```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
```
```

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

### Yul Code Optimization: Manual vs. Automatic

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/compiler.mdx

Illustrates code optimization in Yul, specifically the inlining of expressions. The 'Before' example shows manual optimization, while the 'After' example demonstrates automatic inlining, which reduces bytecode size and gas costs.

```yul
// Before (manual): Unnecessary variable
let current := sload(0)
sstore(0, add(current, 1))

// After (automatic): Inlined expression
sstore(0, add(sload(0), 1))
```

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

### Perform storage operations

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/edsl-api-reference.mdx

Examples of reading and writing to various storage slots, including simple values, addresses, and single or double mappings.

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

-- Address storage
let owner <- getStorageAddr ownerSlot
setStorageAddr ownerSlot newOwner

-- Mappings
let bal <- getMapping balances msgSenderAddr
setMapping balances msgSenderAddr (bal - amount)

let price <- getMappingUint oraclePrices tokenId
setMappingUint oraclePrices tokenId newPrice

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

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

### Adding Simp Attribute and Specific Lemmas in Lean

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/guides/debugging-proofs.mdx

Shows how to mark a lemma with the `simp` attribute for automatic simplification and how to explicitly provide lemmas to the `simp` tactic. This helps `simp` make progress on goals.

```lean
```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
```
```

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

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

### Advanced Lean debugging and tracing techniques

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/guides/debugging-proofs.mdx

Collection of commands and tactics for inspecting proof terms, tracing tactic execution, and logging intermediate goal states.

```lean
#print my_theorem

set_option trace.Meta.Tactic.simp true

theorem complex_proof : ... := by
  trace "Initial goal: {goal}"
  unfold definition1
  trace "After unfold: {goal}"
  simp
  trace "After simp: {goal}"
  omega
```

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

### Combine Verity Statements for Logic Implementation

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/compiler.mdx

Examples of using the Stmt and Expr constructors to implement common contract patterns like balance checks and conditional branching.

```lean
-- Balance check with require
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
```

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

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

### Option Handling

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/guides/debugging-proofs.mdx

Pattern for handling Option types by proving contradictions for none cases and simplifying some cases.

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

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

### Build and Verify Proofs

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/guides/first-contract.mdx

Shell commands to compile the proof environment and audit for incomplete proofs marked with 'sorry'.

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

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

### Manual IR Contract Definition (Owned Contract)

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/compiler.mdx

An example of a manually constructed Intermediate Representation (IR) for the 'Owned' contract. This approach is brittle and error-prone compared to declarative specs.

```lean
private def ownedContract : IRContract :=
  let deployBody := [
    stmtLet "argsOffset" (call "sub" [call "codesize" [], lit 32]),
    stmtExpr (call "codecopy" [lit 0, ident "argsOffset", lit 32]),
    stmtLet "initialOwner" (call "and" [call "mload" [lit 0], hex addressMask]),
    sstoreSlot 0 (ident "initialOwner")
  ]
  let transferBody := onlyOwnerCheck 0 ++ [
    stmtLet "newOwner" (calldataAddress 4),
    sstoreSlot 0 (ident "newOwner"),
    stop
  ]
  let getOwnerBody := returnUint (sloadSlot 0)
  { name := "Owned"
    deploy := deployBody
    functions := [
      fn "transferOwnership" 0xf2fde38b [addrParam "newOwner"] IRType.unit transferBody,
      fn "getOwner" 0x893d20e8 [] IRType.address getOwnerBody
    ]
    usesMapping := false }
```

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

### Counter Contract in Lean

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/examples.mdx

Provides increment and decrement functionality for a Uint256 counter stored in a StorageSlot. It demonstrates read-modify-write operations. Proofs cover arithmetic, composition, and decrement-at-zero behavior.

```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)
```

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

### Verify Safe Arithmetic Boundary Conditions

Source: https://github.com/lfglabs-dev/verity/blob/main/Compiler/Proofs/README.md

A Lean 4 theorem pattern for verifying that operations involving safe arithmetic succeed under specific conditions. It uses helper lemmas to prove the safety of the operation before checking success.

```lean
theorem safe_op_succeeds (state : ContractState) (sender : Address)
    (h : condition) :
    let result := operation.run { state with sender := sender }
    result.isSuccess = true := by
  unfold operation Contract.run
  have h_safe : (safeOp a b).isSome := by
    rw [safeOp_some_iff_condition]; exact h
  simp [h_safe]
```

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

### Yul Library Formatting Rules

Source: https://github.com/lfglabs-dev/verity/blob/main/examples/external-libs/README.md

Illustrates the correct structure for Yul library files, emphasizing the use of plain function definitions instead of object wrappers.

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

### Manual IR Translation (Before)

Source: https://github.com/lfglabs-dev/verity/blob/main/docs-site/content/research.mdx

This snippet illustrates the previous approach of manually translating contract logic into Intermediate Representation (IR) using Lean. It highlights the verbose and repetitive nature of this method, involving detailed Yul construction for deployment logic.

```lean
private def ownedContract : IRContract :=
  let deployBody := [
    stmtLet "argsOffset" (call "sub" [call "codesize" [], lit 32]),
    stmtExpr (call "codecopy" [lit 0, ident "argsOffset", lit 32]),
    stmtLet "initialOwner" (call "and" [call "mload" [lit 0], hex addressMask]),
    sstoreSlot 0 (ident "initialOwner")
  ]
  // ... more manual Yul construction
```

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

### Define Lean Placeholder for Proving

Source: https://github.com/lfglabs-dev/verity/blob/main/examples/external-libs/README.md

Shows how to create a Lean EDSL placeholder for a cryptographic function to facilitate formal verification before linking the actual Yul implementation.