# symevm

symbolic EVM implin Haskell for smart contract analysis/ equivalence checking and verification that tracks path constraints through JUMPI branches, maintains symbolic state (stack, memory, storage) and has constraint analysis of contract behavior

## Usage

```haskell
import SymbolicExpression
import SymbolicState
import Executor
import qualified Data.ByteString as BS

let bytecode = BS.pack [0x33, 0x61, 0x12, 0x34, 0x14, 0x60, 0x0b, 0x57, ...]
let paths = explore bytecode (initState BS.empty) 1000

mapM_ analyzeConstraints paths
```

**Single path execution**:
```haskell
run :: ByteString -> ExecState -> Int -> [ExecState]
```

**Path exploration**:
```haskell
explore :: ByteString -> ExecState -> Int -> [ExecState]
```
## Build

```bash
cabal build
cabal run symevm
```

## Example

```haskell
let code = BS.pack [
  0x60, 0x00, 
  0x35,        
  0x60, 0x64,  
  0x11,       
  0x60, 0x0a,  
  0x57,       
  0xfd,        
  0x5b,        
  0x00       
  ]

let paths = explore code (initState BS.empty) 50
```

Yields 2 paths:

 Path 1: `calldataload(0) > 100` → PC=10, halted
 Path 2: `calldataload(0) <= 100` → reverted