From 68b9649b3b8af0acae64e572844a5be725315f6d Mon Sep 17 00:00:00 2001
From: Hideaki Takahashi <koukyosyumei@hotmail.com>
Date: Fri, 16 Aug 2024 08:26:43 -0400
Subject: [PATCH] Precompiled ECDSA (#14)

* implement a ecrecover contract

* add test cases for ecrecover

* support precompiled ecrecover

* fix simplify

* fix memcopy

* decrease clone

* improve logging

* fix the process of addrs

* update
---
 Cargo.toml                 |   4 +-
 src/main.rs                |   6 +-
 src/modules/cli.rs         |   6 +-
 src/modules/evm.rs         | 225 +++++++++++++++++++------------------
 src/modules/expr.rs        |  43 ++++---
 src/modules/precompiled.rs | 195 ++++++++++----------------------
 src/modules/smt.rs         |  25 +++--
 src/modules/symexec.rs     |   2 +-
 src/modules/traversals.rs  |  13 +--
 src/modules/types.rs       |  12 +-
 tests/evm_test.rs          |   4 +-
 tests/precompiled_test.rs  |  56 +++++++++
 12 files changed, 294 insertions(+), 297 deletions(-)
 create mode 100644 tests/precompiled_test.rs

diff --git a/Cargo.toml b/Cargo.toml
index bea541d..c4d3580 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -24,4 +24,6 @@ byteorder = "1.5.0"
 env_logger = "0.11.5"
 log = "0.4.22"
 regex = "1.10.5"
-getopts = "0.2"
\ No newline at end of file
+getopts = "0.2"
+secp256k1={ version = "0.29.0", features = ["recovery", "rand-std"] }
+sha3="0.10.8"
\ No newline at end of file
diff --git a/src/main.rs b/src/main.rs
index 5350208..895ba97 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -16,7 +16,7 @@ use rhoevm::modules::expr::is_function_sig_check_prop;
 use rhoevm::modules::format::{hex_byte_string, strip_0x};
 use rhoevm::modules::smt::parse_z3_output;
 use rhoevm::modules::transactions::init_tx;
-use rhoevm::modules::types::{ContractCode, Env, Expr, Prop, RuntimeCodeStruct, VM, W256};
+use rhoevm::modules::types::{ContractCode, Env, Expr, Prop, RuntimeCodeStruct, EXPR_MEMPTY, VM, W256};
 
 #[derive(Debug)]
 struct Args {
@@ -118,7 +118,7 @@ fn dummy_symvm_from_command(cmd: &SymbolicCommand, calldata: (Expr, Vec<Box<Prop
     (_, _, Some(code)) => {
       let bs = hex_byte_string("bytes", &strip_0x(code));
       let mc = if cmd.create {
-        ContractCode::InitCode(Box::new(bs), Box::new(Expr::Mempty))
+        ContractCode::InitCode(Box::new(bs), Box::new(EXPR_MEMPTY))
       } else {
         ContractCode::RuntimeCode(RuntimeCodeStruct::ConcreteRuntimeCode(Box::new(bs)))
       };
@@ -357,6 +357,7 @@ async fn main() {
         vm.state.pc += 1;
       }
 
+      debug!("Start SMT Solving...");
       let mut tasks_check_envs = vec![];
       for (pc, constraints, env) in potential_envs {
         let constraints_clone = constraints.clone(); // Clone constraints to move into the task
@@ -442,7 +443,6 @@ async fn main() {
           //debug!("UNRECHABLE REVERT @ PC=0x{:x}", pc);
           //}
       }
-
       info!("Execution of '{}' completed.\n", function_signature);
     }
     reachable_envs = next_reachable_envs;
diff --git a/src/modules/cli.rs b/src/modules/cli.rs
index fdaac02..3c004ba 100644
--- a/src/modules/cli.rs
+++ b/src/modules/cli.rs
@@ -11,7 +11,7 @@ use crate::modules::format::{hex_byte_string, strip_0x};
 use crate::modules::symexec::mk_calldata;
 use crate::modules::transactions::init_tx;
 use crate::modules::types::{
-  Addr, BaseState, Contract, ContractCode, Expr, Gas, Prop, RuntimeCodeStruct, VMOpts, VM, W256,
+  Addr, BaseState, Contract, ContractCode, Expr, Gas, Prop, RuntimeCodeStruct, VMOpts, EXPR_MEMPTY, VM, W256,
 };
 
 type URL = String;
@@ -110,7 +110,7 @@ pub async fn symvm_from_command(cmd: &SymbolicCommand, calldata: (Expr, Vec<Box<
           Some(code) => {
             let bs = hex_byte_string("bytes", &strip_0x(code));
             let mc = if cmd.create {
-              ContractCode::InitCode(Box::new(bs), Box::new(Expr::Mempty))
+              ContractCode::InitCode(Box::new(bs), Box::new(EXPR_MEMPTY))
             } else {
               ContractCode::RuntimeCode(RuntimeCodeStruct::ConcreteRuntimeCode(Box::new(bs)))
             };
@@ -127,7 +127,7 @@ pub async fn symvm_from_command(cmd: &SymbolicCommand, calldata: (Expr, Vec<Box<
     (_, _, Some(code)) => {
       let bs = hex_byte_string("bytes", &strip_0x(code));
       let mc = if cmd.create {
-        ContractCode::InitCode(Box::new(bs), Box::new(Expr::Mempty))
+        ContractCode::InitCode(Box::new(bs), Box::new(EXPR_MEMPTY))
       } else {
         ContractCode::RuntimeCode(RuntimeCodeStruct::ConcreteRuntimeCode(Box::new(bs)))
       };
diff --git a/src/modules/evm.rs b/src/modules/evm.rs
index 6bb8704..c910e6b 100644
--- a/src/modules/evm.rs
+++ b/src/modules/evm.rs
@@ -1,5 +1,6 @@
 use log::{error, warn};
 use ripemd::Ripemd160;
+use secp256k1::Secp256k1;
 use sha2::{Digest, Sha256};
 use std::collections::{HashMap, HashSet, VecDeque};
 use std::fs;
@@ -19,13 +20,14 @@ use crate::modules::expr::{
 use crate::modules::feeschedule::FeeSchedule;
 use crate::modules::format::format_prop;
 use crate::modules::op::{get_op, op_size, op_string, Op};
+use crate::modules::precompiled::precompiled_ecrecover;
 use crate::modules::smt::{assert_props, format_smt2};
 use crate::modules::types::{
   from_list, keccak, keccak_prime, maybe_lit_addr, maybe_lit_byte, maybe_lit_word, pad_left_prime, pad_right,
   word256_bytes, Addr, BaseState, Block, BranchDir, BranchReachability, ByteString, Cache, CodeLocation, Contract,
   ContractCode, Env, EvmError, Expr, ExprSet, ForkState, Frame, FrameContext, FrameState, Gas, Memory, MutableMemory,
   PartialExec, Prop, RuntimeCodeStruct, RuntimeConfig, SubState, Trace, TraceData, TxState, VMOpts, VMResult,
-  W256W256Map, VM, W256, W64,
+  W256W256Map, EXPR_MEMPTY, VM, W256, W64,
 };
 
 fn initial_gas() -> u64 {
@@ -50,11 +52,11 @@ pub fn blank_state() -> FrameState {
     stack: Vec::new(),
     memory: Memory::ConcreteMemory(Vec::new()),
     memory_size: 0,
-    calldata: Box::new(Expr::Mempty),
+    calldata: Box::new(EXPR_MEMPTY),
     callvalue: Box::new(Expr::Lit(W256(0, 0))),
     caller: Box::new(Expr::LitAddr(W256(0, 0))),
     gas: Gas::Concerete(initial_gas()),
-    returndata: Box::new(Expr::Mempty),
+    returndata: Box::new(EXPR_MEMPTY),
     static_flag: false,
     prev_model: None,
   }
@@ -63,7 +65,7 @@ pub fn blank_state() -> FrameState {
 /// Retrieves the bytecode of a contract as an expression.
 ///
 /// This function examines the contract's code and returns the corresponding expression:
-/// - If the contract code is initialization code, an empty expression (`Expr::Mempty`) is returned.
+/// - If the contract code is initialization code, an empty expression (`EXPR_MEMPTY`) is returned.
 /// - If the contract code is runtime code, a concrete buffer containing the code is returned.
 ///
 /// # Arguments
@@ -75,7 +77,7 @@ pub fn blank_state() -> FrameState {
 /// An `Option<Expr>` containing the bytecode expression, or `None` if the contract code is unsupported.
 pub fn bytecode(contract: &Contract) -> Option<Expr> {
   match &contract.code {
-    ContractCode::InitCode(_, _) => Some(Expr::Mempty),
+    ContractCode::InitCode(_, _) => Some(EXPR_MEMPTY),
     ContractCode::RuntimeCode(RuntimeCodeStruct::ConcreteRuntimeCode(buf)) => Some(Expr::ConcreteBuf(buf.to_vec())),
     _ => None,
   }
@@ -169,7 +171,7 @@ pub fn make_vm(opts: VMOpts) -> VM {
       callvalue: Box::new(opts.value),
       caller: Box::new(opts.caller),
       gas: opts.gas,
-      returndata: Box::new(Expr::Mempty),
+      returndata: Box::new(EXPR_MEMPTY),
       static_flag: false,
       prev_model: None,
     },
@@ -420,7 +422,7 @@ impl VM {
       }
       true
     } else if self.state.pc >= opslen(&self.state.code) {
-      finish_frame(self, FrameResult::FrameReturned(Expr::Mempty));
+      finish_frame(self, FrameResult::FrameReturned(EXPR_MEMPTY));
       false
     } else {
       let op = match &self.state.code {
@@ -482,7 +484,7 @@ impl VM {
           limit_stack(1, self.state.stack.len(), || {
             burn(self, fees.g_verylow, || {});
             next(self, op);
-            push_sym(self, Box::new(xs.clone()));
+            push_sym(self, Box::new(xs));
           });
           true
         }
@@ -491,7 +493,7 @@ impl VM {
             limit_stack(1, self.state.stack.len(), || {
               burn(self, fees.g_verylow, || {});
               next(self, op);
-              push_sym(self, y.clone());
+              push_sym(self, y);
             });
           } else {
             underrun();
@@ -536,7 +538,7 @@ impl VM {
           true
         }
         Op::Stop => {
-          finish_frame(self, FrameResult::FrameReturned(Expr::Mempty));
+          finish_frame(self, FrameResult::FrameReturned(EXPR_MEMPTY));
           false
         }
         Op::Add => stack_op2(self, fees.g_verylow, "add"),
@@ -595,13 +597,13 @@ impl VM {
           limit_stack(1, self.state.stack.len(), || {
             burn(self, fees.g_base, || {});
             next(self, op);
-            push_addr(self, *self_contract.clone());
+            push_addr(self, *self_contract);
           });
           true
         }
         Op::Balance => {
           if let Some((x, xs)) = self.state.stack.clone().split_last() {
-            let mut a: Expr = Expr::Mempty;
+            let mut a: Expr = EXPR_MEMPTY;
             force_addr(self, x, "BALANCE", |a_| a = a_);
             access_and_burn(&a, || {
               let mut c = empty_contract();
@@ -757,7 +759,7 @@ impl VM {
           - size: byte size of the code.
           */
           if let Some((x, xs)) = self.state.stack.clone().split_last() {
-            let mut a: Expr = Expr::Mempty;
+            let mut a: Expr = EXPR_MEMPTY;
             force_addr(self, x, "EXTCODESIZE", |a_| a = a_);
             access_and_burn(&a, || {
               let mut c = empty_contract();
@@ -1011,7 +1013,7 @@ impl VM {
             let x = self.state.stack.pop().unwrap();
             let new = self.state.stack.pop().unwrap();
             // Access current storage
-            let mut current: Expr = Expr::Mempty;
+            let mut current: Expr = EXPR_MEMPTY;
             access_storage(self, *self_contract.clone(), *x.clone(), |current_| current = current_);
             let original = match conc_keccak_simp_expr(Box::new(Expr::SLoad(
               x.clone(),
@@ -1107,10 +1109,8 @@ impl VM {
               burn(self, fees.g_high, || {});
               let mut x_int = None;
               force_concrete(self, x, "JUMPI: symbolic jumpdest", |x_| x_int = x_.to_int());
-
               let mut condition = BranchReachability::NONE;
               let else_vm_ = branch(self, y.clone(), |condition_| Ok(condition = condition_), max_num_iterations);
-
               if condition == BranchReachability::ONLYTHEN || condition == BranchReachability::BOTH {
                 match x_int {
                   None => {
@@ -1251,31 +1251,31 @@ impl VM {
             if gt0 == BranchReachability::ONLYTHEN || gt0 == BranchReachability::BOTH {
               not_static(self, || {});
 
-              let mut x_to_a = Expr::Mempty;
+              let mut x_to_a = EXPR_MEMPTY;
               force_addr(self, x_to, "unable to determine a call target", |x_to_a_| x_to_a = x_to_a_);
               match Some(x_gas) {
                 None => vm_error("IllegalOverflow"),
                 _ => {
-                  let mut callee: Expr = Expr::Mempty;
+                  let mut callee: Expr = EXPR_MEMPTY;
                   general_call(
                     self,
                     op,
-                    this_contract.clone(),
+                    &this_contract,
                     Gas::Concerete(0),
-                    x_to_a.clone(),
-                    x_to_a.clone(),
-                    *x_value.clone(),
-                    *x_in_offset.clone(),
-                    *x_in_size.clone(),
-                    *x_out_offset.clone(),
-                    *x_out_size.clone(),
+                    &x_to_a,
+                    &x_to_a,
+                    &x_value,
+                    &x_in_offset,
+                    &x_in_size,
+                    &x_out_offset,
+                    &x_out_size,
                     xs.to_vec(),
                     |callee_| callee = callee_,
                     max_num_iterations,
                   );
                   let from_ = self.config.override_caller.clone();
                   let scaller =
-                    if let Some(_) = from_ { Box::new(from_.clone().unwrap()) } else { Box::new(Expr::Mempty) };
+                    if let Some(_) = from_ { Box::new(from_.clone().unwrap()) } else { Box::new(EXPR_MEMPTY) };
                   self.state.callvalue = x_value.clone();
                   self.state.caller = scaller.clone();
                   self.state.contract = Box::new(callee.clone());
@@ -1307,15 +1307,15 @@ impl VM {
             general_call(
               self,
               op,
-              this_contract.clone(),
+              &this_contract,
               Gas::Concerete(0),
-              *x_to.clone(),
-              *self_contract.clone(),
-              *x_value.clone(),
-              *x_in_offset.clone(),
-              *x_in_size.clone(),
-              *x_out_offset.clone(),
-              *x_out_size.clone(),
+              &x_to,
+              &self_contract,
+              &x_value,
+              &x_in_offset,
+              &x_in_size,
+              &x_out_offset,
+              &x_out_size,
               xs.to_vec(),
               |_| {},
               max_num_iterations,
@@ -1404,15 +1404,15 @@ impl VM {
                     general_call(
                       self,
                       op,
-                      this_contract.clone(),
+                      &this_contract,
                       Gas::Concerete(0),
-                      *x_to.clone(),
-                      *self_contract.clone(),
-                      Expr::Lit(W256(0, 0)),
-                      *x_in_offset.clone(),
-                      *x_in_size.clone(),
-                      *x_out_offset.clone(),
-                      *x_out_size.clone(),
+                      &x_to,
+                      &self_contract,
+                      &Expr::Lit(W256(0, 0)),
+                      &x_in_offset,
+                      &x_in_size,
+                      &x_out_offset,
+                      &x_out_size,
                       vec![],
                       |_| {},
                       max_num_iterations,
@@ -1478,19 +1478,19 @@ impl VM {
                   // gasTryFrom(x_gas)
                   None => vm_error("IllegalOverflow"),
                   _ => {
-                    let mut callee = Expr::Mempty;
+                    let mut callee = EXPR_MEMPTY;
                     general_call(
                       self,
                       op,
-                      this_contract.clone(),
+                      &this_contract.clone(),
                       Gas::Concerete(0),
-                      x_to_prime.clone(),
-                      x_to_prime.clone(),
-                      Expr::Lit(W256(0, 0)),
-                      *x_in_offset.clone(),
-                      *x_in_size.clone(),
-                      *x_out_offset.clone(),
-                      *x_out_size.clone(),
+                      &x_to_prime.clone(),
+                      &x_to_prime.clone(),
+                      &Expr::Lit(W256(0, 0)),
+                      &x_in_offset.clone(),
+                      &x_in_size.clone(),
+                      &x_out_offset.clone(),
+                      &x_out_size.clone(),
                       xs.to_vec(),
                       |callee_| callee = callee_,
                       max_num_iterations,
@@ -1520,7 +1520,7 @@ impl VM {
         Op::Selfdestruct => {
           not_static(self, || {});
           if let [.., x_to] = &self.state.stack.clone()[..] {
-            let mut x_to_a = Expr::Mempty;
+            let mut x_to_a = EXPR_MEMPTY;
             force_addr(self, x_to, "SELFDESTRUCT", |x_to_a_| x_to_a = x_to_a_);
             if let Expr::WAddr(_) = x_to_a {
               let acc = access_account_for_gas(self, x_to_a.clone());
@@ -1552,7 +1552,7 @@ impl VM {
                 // });
               } else {
                 let mut else_vm = else_vm_.unwrap();
-                finish_frame(&mut else_vm, FrameResult::FrameReturned(Expr::Mempty));
+                finish_frame(&mut else_vm, FrameResult::FrameReturned(EXPR_MEMPTY));
               }
             } else {
               let pc = 0; // use(state.pc)
@@ -1579,7 +1579,7 @@ impl VM {
         }
         Op::Extcodecopy => {
           if let [xs @ .., code_size, code_offset, mem_offset, ext_account] = &self.state.stack.clone()[..] {
-            let mut ext_account_a = Expr::Mempty;
+            let mut ext_account_a = EXPR_MEMPTY;
             force_addr(self, ext_account, "EXTCODECOPY", |ext_account_a_| ext_account_a = ext_account_a_);
             burn_extcodecopy(self, ext_account_a.clone(), *code_size.clone(), self.block.schedule.clone(), || {});
             access_memory_range(self, &mem_offset, &code_size, || {});
@@ -1660,7 +1660,7 @@ impl VM {
         }
         Op::Extcodehash => {
           if let Some((x, xs)) = self.state.stack.clone().split_last() {
-            let mut addr = Expr::Mempty;
+            let mut addr = EXPR_MEMPTY;
             force_addr(self, x, "EXTCODEHASH", |addr_| addr = addr_);
             access_and_burn(&addr, || {
               next(self, op);
@@ -1844,7 +1844,21 @@ fn execute_precompile(
   match pre_compile_addr {
     W256(0x1, 0) => {
       force_concrete_buf(vm, &input, "ECRECOVER", |input| input_prime = input);
-      todo!()
+      let secp = Secp256k1::new();
+      let mut output = [0u8; 32];
+      let is_success = precompiled_ecrecover(&secp, &input_prime, &mut output);
+      if is_success.is_ok() {
+        vm.state.stack = xs;
+        vm.state.stack.push(Box::new(Expr::Lit(W256(1, 0))));
+        vm.state.returndata = Box::new(Expr::ConcreteBuf(output.to_vec()));
+        copy_bytes_to_memory(&Expr::ConcreteBuf(output.to_vec()), out_size, &Expr::Lit(W256(0, 0)), out_offset, vm);
+        next(vm, 0x00)
+      } else {
+        vm.state.stack = xs;
+        vm.state.stack.push(Box::new(Expr::Lit(W256(1, 0))));
+        vm.state.returndata = Box::new(EXPR_MEMPTY);
+        next(vm, 0x00)
+      }
     }
     W256(0x2, 0) => {
       force_concrete_buf(vm, &input, "SHA2-256", |input| input_prime = input);
@@ -1933,7 +1947,6 @@ fn fetch_account<F: FnOnce(&Contract)>(vm: &mut VM, addr: &Expr, f: F) {
         }
       },
       Expr::GVar(_) => panic!("unexpected GVar"),
-      Expr::Mempty => {}
       _ => panic!("unexpected expr in `fetch_account`: addr={}", addr),
     },
   }
@@ -2057,7 +2070,7 @@ fn finish_frame(vm: &mut VM, result: FrameResult) -> bool {
             FrameResult::FrameErrored(_) => {
               vm.env.contracts = callreversion.clone();
               vm.tx.substate = substate.clone();
-              vm.state.returndata = Box::new(Expr::Mempty);
+              vm.state.returndata = Box::new(EXPR_MEMPTY);
               push(vm, W256(0, 0));
             }
           }
@@ -2082,7 +2095,7 @@ fn finish_frame(vm: &mut VM, result: FrameResult) -> bool {
             FrameResult::FrameReturned(output) => {
               let mut on_contract_code = |contract_code| {
                 replace_code(vm, createe.clone(), contract_code);
-                vm.state.returndata = Box::new(Expr::Mempty);
+                vm.state.returndata = Box::new(EXPR_MEMPTY);
                 // reclaimRemainingGasAllowance oldVm
                 push_addr(vm, *createe.clone());
               };
@@ -2115,7 +2128,7 @@ fn finish_frame(vm: &mut VM, result: FrameResult) -> bool {
             FrameResult::FrameErrored(_) => {
               vm.env.contracts = reversion_prime;
               vm.tx.substate = substate.clone();
-              vm.state.returndata = Box::new(Expr::Mempty);
+              vm.state.returndata = Box::new(EXPR_MEMPTY);
               push(vm, W256(0, 0));
             }
           }
@@ -2305,7 +2318,7 @@ fn read_memory(vm: &mut VM, offset_: &Expr, size_: &Expr) -> Expr {
   match &vm.state.memory {
     Memory::ConcreteMemory(mem) => match (simplify(Box::new(offset_.clone())), simplify(Box::new(size_.clone()))) {
       (Expr::Lit(offset_val), Expr::Lit(size_val)) => {
-        if size_val.clone() > MAX_BYTES
+        if size_val > MAX_BYTES
           || offset_val.clone() + size_val.clone() > MAX_BYTES
           || offset_val >= W256(mem.len() as u128, 0)
         {
@@ -2313,16 +2326,13 @@ fn read_memory(vm: &mut VM, offset_: &Expr, size_: &Expr) -> Expr {
         } else {
           let mem_size: usize = mem.len();
           let (from_mem_size, past_end) = if offset_val.clone() + size_val.clone() > W256(mem_size as u128, 0) {
-            (
-              W256(mem_size as u128, 0) - offset_val.clone(),
-              offset_val.clone() + size_val.clone() - W256(mem_size as u128, 0),
-            )
+            (W256(mem_size as u128, 0) - offset_val.clone(), offset_val.clone() + size_val - W256(mem_size as u128, 0))
           } else {
             (size_val, W256(0, 0))
           };
 
           let mut data_from_mem: Vec<u8> =
-            mem.clone()[(offset_val.0 as usize)..(offset_val.0 as usize) + (from_mem_size.0 as usize)].to_vec();
+            mem[(offset_val.0 as usize)..(offset_val.0 as usize) + (from_mem_size.0 as usize)].to_vec();
           let pad = vec![0; past_end.0 as usize];
           data_from_mem.extend(pad);
           Expr::ConcreteBuf(data_from_mem)
@@ -2335,7 +2345,7 @@ fn read_memory(vm: &mut VM, offset_: &Expr, size_: &Expr) -> Expr {
           &(Expr::Lit(W256(0, 0))),
           &(simplify(Box::new(size_.clone()))),
           &(buf),
-          &(Expr::Mempty),
+          &(EXPR_MEMPTY),
         )
       }
     },
@@ -2344,7 +2354,7 @@ fn read_memory(vm: &mut VM, offset_: &Expr, size_: &Expr) -> Expr {
       &(Expr::Lit(W256(0, 0))),
       &(simplify(Box::new(size_.clone()))),
       &(simplify(Box::new(mem.clone()))),
-      &(Expr::Mempty),
+      &(EXPR_MEMPTY),
     ),
   }
 }
@@ -2380,7 +2390,7 @@ fn stack_op2(vm: &mut VM, gas: u64, op: &str) -> bool {
       "shl" => Box::new(Expr::SHL(a.clone(), b.clone())),
       "shr" => Box::new(Expr::SHR(a.clone(), b.clone())),
       "sar" => Box::new(Expr::SAR(a.clone(), b.clone())),
-      _ => Box::new(Expr::Mempty),
+      _ => Box::new(EXPR_MEMPTY),
     };
     vm.state.stack = xs.to_vec();
     vm.state.stack.push(res);
@@ -2398,7 +2408,7 @@ fn stack_op3(vm: &mut VM, gas: u64, op: &str) -> bool {
     let res = match op {
       "addmod" => Box::new(Expr::AddMod(a.clone(), b.clone(), c.clone())),
       "mulmod" => Box::new(Expr::MulMod(a.clone(), b.clone(), c.clone())),
-      _ => Box::new(Expr::Mempty),
+      _ => Box::new(EXPR_MEMPTY),
     };
     vm.state.stack = xs.to_vec();
     vm.state.stack.push(res);
@@ -2416,8 +2426,8 @@ fn stack_op1(vm: &mut VM, gas: u64, op: &str) -> bool {
     let res = match op {
       "iszero" => Box::new(Expr::IsZero(a.clone())),
       "not" => Box::new(Expr::Not(a.clone())),
-      "calldataload" => read_word(&a, &vm.state.calldata.clone()), // Box::new(Expr::Mempty),
-      _ => Box::new(Expr::Mempty),
+      "calldataload" => read_word(&a, &vm.state.calldata.clone()), // Box::new(EXPR_MEMPTY),
+      _ => Box::new(EXPR_MEMPTY),
     };
     vm.state.stack = xs.to_vec();
     vm.state.stack.push(res);
@@ -2586,10 +2596,10 @@ where
   if c.external {
     if let Some(addr_) = maybe_lit_addr(addr.clone()) {
       if force_concrete(vm, &slot_conc.clone(), "cannot read symbolic slots via RPC", |_| {}) {
-        match vm.cache.fetched.clone().get(&addr_) {
+        match vm.cache.fetched.get(&addr_) {
           Some(fetched) => match read_storage(Box::new(slot), Box::new(fetched.storage.clone())) {
             Some(val) => continue_fn(val),
-            None => mk_query(vm, addr, maybe_lit_word(slot_conc.clone()).unwrap().0 as u64, continue_fn),
+            None => mk_query(vm, addr, maybe_lit_word(slot_conc).unwrap().0 as u64, continue_fn),
           },
           None => internal_error("contract marked external not found in cache"),
         }
@@ -2649,15 +2659,15 @@ fn is_precompile_addr(_addr: &Expr) -> bool {
 fn general_call(
   vm: &mut VM,
   op: u8,
-  this: Contract,
+  this: &Contract,
   gas_given: Gas,
-  x_to: Expr,
-  x_context: Expr,
-  x_value: Expr,
-  x_in_offset: Expr,
-  x_in_size: Expr,
-  x_out_offset: Expr,
-  x_out_size: Expr,
+  x_to: &Expr,
+  x_context: &Expr,
+  x_value: &Expr,
+  x_in_offset: &Expr,
+  x_in_size: &Expr,
+  x_out_offset: &Expr,
+  x_out_size: &Expr,
   xs: Vec<Box<Expr>>,
   continue_fn: impl FnOnce(Expr),
   max_num_iterations: u32,
@@ -2665,7 +2675,7 @@ fn general_call(
   if is_precompile_addr(&x_to) {
     force_concrete_addr2(
       vm,
-      (x_to, x_context),
+      (x_to.clone(), x_context.clone()),
       "Cannot call precompile with symbolic addresses".to_string(),
       |(_x_to, _x_context)| {
         /*
@@ -2685,7 +2695,7 @@ fn general_call(
         */
       },
     );
-  } else if x_to == cheat_code() {
+  } else if *x_to == cheat_code() {
     vm.state.stack = xs;
     todo!()
     // cheat(vm, x_in_offset, x_in_size, x_out_offset, x_out_size);
@@ -2707,9 +2717,9 @@ fn general_call(
       |x_gas_| x_gas = x_gas_,
       max_num_iterations,
     );
-    let mut target_code = ContractCode::UnKnownCode(Box::new(Expr::Mempty));
-    let mut taregt_codehash = Expr::Mempty;
-    fetch_account(vm, &x_to.clone(), |target| {
+    let mut target_code = ContractCode::UnKnownCode(Box::new(EXPR_MEMPTY));
+    let mut taregt_codehash = EXPR_MEMPTY;
+    fetch_account(vm, &x_to, |target| {
       target_code = target.code.clone();
       taregt_codehash = target.codehash.clone();
     });
@@ -2733,8 +2743,8 @@ fn general_call(
         let new_context = FrameContext::CallContext {
           target: x_to.clone(),
           context: x_context.clone(),
-          offset: x_out_offset,
-          size: x_out_size,
+          offset: x_out_offset.clone(),
+          size: x_out_size.clone(),
           codehash: taregt_codehash,
           callreversion: vm.env.contracts.clone(),
           substate: vm.tx.substate.clone(),
@@ -2750,7 +2760,7 @@ fn general_call(
         // update the state
         let new_memory = Memory::ConcreteMemory(vec![]);
         let cleared_init_code = match target_code {
-          ContractCode::InitCode(_, _) => ContractCode::InitCode(Box::new(vec![]), Box::new(Expr::Mempty)),
+          ContractCode::InitCode(_, _) => ContractCode::InitCode(Box::new(vec![]), Box::new(EXPR_MEMPTY)),
           a => a.clone(),
         };
         vm.state = FrameState {
@@ -2762,7 +2772,7 @@ fn general_call(
           stack: vec![],
           memory: new_memory,
           memory_size: 0,
-          returndata: Box::new(Expr::Mempty),
+          returndata: Box::new(EXPR_MEMPTY),
           calldata: Box::new(calldata.clone()),
           contract: vm.state.contract.clone(),
           callvalue: vm.state.callvalue.clone(),
@@ -2770,7 +2780,7 @@ fn general_call(
           static_flag: vm.state.static_flag.clone(),
           prev_model: None,
         };
-        continue_fn(x_to);
+        continue_fn(x_to.clone());
       }
     }
   }
@@ -2797,18 +2807,18 @@ fn create(
   if x_size_val > vm.block.max_code_size.clone() * W256(2, 0) {
     vm.state.stack = xs;
     vm.state.stack.push(Box::new(Expr::Lit(W256(0, 0))));
-    vm.state.returndata = Box::new(Expr::Mempty);
+    vm.state.returndata = Box::new(EXPR_MEMPTY);
     // vm_error(EvmError::MaxInitCodeSizeExceeded(vm0.block.max_code_size * 2, x_size));
   } else if this.nonce == Some(u64::max_value()) {
     vm.state.stack = xs;
     vm.state.stack.push(Box::new(Expr::Lit(W256(0, 0))));
-    vm.state.returndata = Box::new(Expr::Mempty);
+    vm.state.returndata = Box::new(EXPR_MEMPTY);
     vm.traces.push(with_trace_location(vm, TraceData::ErrorTrace(EvmError::NonceOverflow)));
     next(vm, op);
   } else if vm.frames.len() >= 1024 {
     vm.state.stack = xs;
     vm.state.stack.push(Box::new(Expr::Lit(W256(0, 0))));
-    vm.state.returndata = Box::new(Expr::Mempty);
+    vm.state.returndata = Box::new(EXPR_MEMPTY);
     vm.traces.push(with_trace_location(vm, TraceData::ErrorTrace(EvmError::CallDepthLimitReached)));
     next(vm, op);
   } else if collision(vm.env.contracts.get(&new_addr).cloned()) {
@@ -2816,7 +2826,7 @@ fn create(
     burn(vm, x_gas_val, || {});
     vm.state.stack = xs;
     vm.state.stack.push(Box::new(Expr::Lit(W256(0, 0))));
-    vm.state.returndata = Box::new(Expr::Mempty);
+    vm.state.returndata = Box::new(EXPR_MEMPTY);
     let n = vm.env.contracts.entry(self_addr.clone()).or_insert(empty_contract()).nonce;
     let new_nonce = if let Some(n_) = n { Some(n_ + 1) } else { None };
     vm.env.contracts.entry(self_addr).or_insert(empty_contract()).nonce = new_nonce;
@@ -2833,14 +2843,14 @@ fn create(
       // not enough balance
       vm.state.stack = xs.clone();
       vm.state.stack.push(Box::new(Expr::Lit(W256(0, 0))));
-      vm.state.returndata = Box::new(Expr::Mempty);
+      vm.state.returndata = Box::new(EXPR_MEMPTY);
       vm.traces.push(with_trace_location(
         vm,
         TraceData::ErrorTrace(EvmError::BalanceTooLow(Box::new(x_value.clone()), Box::new(this.balance.clone()))),
       ));
       next(vm, op);
-      touch_account(vm, &self_addr.clone());
-      touch_account(vm, &new_addr.clone());
+      touch_account(vm, &self_addr);
+      touch_account(vm, &new_addr);
     }
     if condition == BranchReachability::ONLYELSE || condition == BranchReachability::BOTH {
       {
@@ -3192,6 +3202,10 @@ pub async fn solve_constraints(pc: usize, pathconds: Vec<Box<Prop>>) -> (bool, O
       let stdout = String::from_utf8(output.stdout).unwrap();
       (stdout[..3] == *"sat", Some(stdout))
     } else {
+      let stdout = String::from_utf8(output.stdout).unwrap();
+      if stdout.len() >= 6 && stdout[..6] == *"(error" {
+        error!("ERROR OF SMT FILE @ {}", file_path.to_str().unwrap());
+      }
       (false, None)
     }
   })
@@ -3238,14 +3252,12 @@ where
   let cond_simp_conc = conc_keccak_simp_expr(Box::new(cond_simp));
   let then_branch_cond = Prop::PNeg(Box::new(Prop::PEq(cond_simp_conc.clone(), Expr::Lit(W256(0, 0)))));
   let else_branch_cond = Prop::PEq(cond_simp_conc.clone(), Expr::Lit(W256(0, 0)));
-
   let mut new_vm = vm.clone();
 
   // vm.constraints_raw_expr.push(cond.clone());
   vm.constraints.push(Box::new(then_branch_cond));
   // new_vm.constraints_raw_expr.push(Box::new(Expr::Not(cond)));
   new_vm.constraints.push(Box::new(else_branch_cond));
-
   let branchreachability = if itr_cnt < max_num_iterations as i64 {
     if let Expr::Lit(W256(1, 0)) = cond_simp_conc {
       BranchReachability::ONLYTHEN
@@ -3270,7 +3282,6 @@ where
     (itr_cnt, new_vm.state.stack.clone(), BranchDir::ELSE);
 
   let _ = continue_fn(branchreachability);
-
   Some(new_vm)
 }
 
@@ -3382,7 +3393,7 @@ fn cheat_code() -> Expr {
 /// * `Option<ContractCode>` - The parsed initialization code, or `None` if parsing fails.
 fn parse_init_code(buf: &Expr) -> Option<ContractCode> {
   match buf {
-    Expr::ConcreteBuf(b) => Some(ContractCode::InitCode(Box::new(b.to_vec()), Box::new(Expr::Mempty))),
+    Expr::ConcreteBuf(b) => Some(ContractCode::InitCode(Box::new(b.to_vec()), Box::new(EXPR_MEMPTY))),
     _ => {
       let conc = concrete_prefix(buf);
       if conc.is_empty() {
@@ -3441,7 +3452,7 @@ fn call_checks<F>(
       if vm.frames.len() >= 1024 {
         vm.state.stack = xs.to_vec();
         vm.state.stack.push(Box::new(Expr::Lit(W256(0, 0))));
-        vm.state.returndata = Box::new(Expr::Mempty);
+        vm.state.returndata = Box::new(EXPR_MEMPTY);
         vm.traces.push(with_trace_location(vm, TraceData::ErrorTrace(EvmError::CallDepthLimitReached)));
         next(vm, op);
       } else {
@@ -3460,7 +3471,7 @@ fn call_checks<F>(
       if is_greater == BranchReachability::ONLYELSE || is_greater == BranchReachability::BOTH {
         vm.state.stack = xs.to_vec();
         vm.state.stack.push(Box::new(Expr::Lit(W256(0, 0))));
-        vm.state.returndata = Box::new(Expr::Mempty);
+        vm.state.returndata = Box::new(EXPR_MEMPTY);
         vm.traces.push(with_trace_location(
           vm,
           TraceData::ErrorTrace(EvmError::BalanceTooLow(Box::new(x_value), Box::new(this.balance.clone()))),
@@ -3472,7 +3483,7 @@ fn call_checks<F>(
         if else_vm.frames.len() >= 1024 {
           else_vm.state.stack = xs.to_vec();
           else_vm.state.stack.push(Box::new(Expr::Lit(W256(0, 0))));
-          else_vm.state.returndata = Box::new(Expr::Mempty);
+          else_vm.state.returndata = Box::new(EXPR_MEMPTY);
           else_vm.traces.push(with_trace_location(&else_vm, TraceData::ErrorTrace(EvmError::CallDepthLimitReached)));
           next(&mut else_vm, op);
         } else {
diff --git a/src/modules/expr.rs b/src/modules/expr.rs
index bbb3baf..6bb98be 100644
--- a/src/modules/expr.rs
+++ b/src/modules/expr.rs
@@ -7,7 +7,8 @@ use crate::modules::cse::BufEnv;
 use crate::modules::rlp::{rlp_addr_full, rlp_list, rlp_word_256};
 use crate::modules::traversals::{fold_expr, map_expr, map_prop, map_prop_prime};
 use crate::modules::types::{
-  keccak, keccak_prime, maybe_lit_byte, pad_right, until_fixpoint, word256_bytes, Addr, Expr, GVar, Prop, W256, W64,
+  keccak, keccak_prime, maybe_lit_byte, pad_right, until_fixpoint, word256_bytes, Addr, Expr, GVar, Prop, EXPR_MEMPTY,
+  W256, W64,
 };
 
 use super::types::{ByteString, Word8};
@@ -701,15 +702,23 @@ pub fn read_word_from_bytes(idx: &Expr, buf: &Expr) -> Box<Expr> {
   }
 }
 
+fn is_addr_litaddr(e: &Expr) -> bool {
+  if let Expr::LitAddr(_) = e {
+    return true;
+  } else {
+    return false;
+  }
+}
+
 pub fn write_word(offset: &Expr, value: &Expr, buf: &Expr) -> Expr {
   let buf_clone = buf.clone();
   match (offset.clone(), value.clone(), buf.clone()) {
     (Expr::Lit(offset), Expr::WAddr(addr), Expr::ConcreteBuf(_))
-      if offset.clone() < MAX_BYTES && offset.clone() + W256(32, 0) < MAX_BYTES =>
+      if offset.clone() < MAX_BYTES && offset.clone() + W256(32, 0) < MAX_BYTES && is_addr_litaddr(&addr) =>
     {
       let val = match *addr.clone() {
         Expr::LitAddr(v) => v,
-        _ => panic!("unsupported"),
+        _ => panic!("unsupported expr: {}", addr),
       };
       write_word(&(Expr::Lit(offset.clone())), &(Expr::Lit(val)), &buf_clone)
     }
@@ -871,7 +880,11 @@ pub fn copy_slice(src_offset: &Expr, dst_offset: &Expr, size: &Expr, src: &Expr,
         let sl: Vec<Expr> = ((src_offset.0)..(src_offset.0) + (size.0))
           .map(|i| read_byte(Box::new(Expr::Lit(W256(i as u128, 0))), Box::new(src.clone())))
           .collect();
-        let tl = &dst_buf[dst_offset.0 as usize + size.0 as usize..];
+        let tl = if (dst_offset.0 as usize + size.0 as usize) < dst_buf.len() {
+          &dst_buf[dst_offset.0 as usize + size.0 as usize..]
+        } else {
+          &vec![]
+        };
 
         if sl.iter().all(|arg0: &Expr| is_lit_byte(Box::new(arg0.clone()))) {
           let packed_sl: Vec<u8> = sl.into_iter().filter_map(maybe_lit_byte).collect();
@@ -1012,15 +1025,11 @@ fn conc_keccak_one_pass(expr: Box<Expr>) -> Expr {
 
 // Main simplify function
 pub fn simplify(expr: Box<Expr>) -> Expr {
-  if *expr != Expr::Mempty {
-    let simplified = map_expr(|arg0: &Expr| go_expr(arg0), *expr.clone());
-    if simplified == *expr {
-      simplified
-    } else {
-      simplify(Box::new(map_expr(|arg0: &Expr| go_expr(arg0), structure_array_slots(Box::new(*expr.clone())))))
-    }
+  let simplified = map_expr(|arg0: &Expr| go_expr(arg0), *expr.clone());
+  if simplified == *expr {
+    simplified
   } else {
-    Expr::Mempty
+    simplify(Box::new(map_expr(|arg0: &Expr| go_expr(arg0), structure_array_slots(Box::new(*expr.clone())))))
   }
 }
 
@@ -1167,6 +1176,13 @@ fn go_expr(expr: &Expr) -> Expr {
         Expr::SymAddr(_) => Expr::Lit(W256(0, 0)),
         _ => iszero(a),
       },
+      Expr::IsZero(b) => match *b.clone() {
+        Expr::IsZero(c) => iszero(c),
+        Expr::LT(x, y) => lt(x, y),
+        Expr::Eq(x, y) => eq(x, y),
+        _ => iszero(a),
+      },
+      Expr::Xor(x, y) => eq(x, y),
       _ => iszero(a),
     },
     // Expr::IsZero(a) => iszero(a),
@@ -1865,7 +1881,7 @@ pub fn drop(n: W256, buf: &Expr) -> Expr {
 }
 
 pub fn slice(offset: Box<Expr>, size: Box<Expr>, src: Box<Expr>) -> Expr {
-  copy_slice(&offset, &(Expr::Lit(W256(0, 0))), &size, &src, &(Expr::Mempty))
+  copy_slice(&offset, &(Expr::Lit(W256(0, 0))), &size, &src, &(EXPR_MEMPTY))
 }
 
 pub fn buf_length(buf: &Expr) -> Expr {
@@ -1898,7 +1914,6 @@ pub fn buf_length_env(env: &HashMap<usize, Expr>, use_env: bool, buf: Expr) -> E
           emax(Box::new(l), Box::new(Expr::BufLength(Box::new(Expr::GVar(GVar::BufVar(a))))))
         }
       }
-      Expr::Mempty => l,
       _ => panic!("unsupported expression: {}", buf),
     }
   }
diff --git a/src/modules/precompiled.rs b/src/modules/precompiled.rs
index f9c5133..5297e4f 100644
--- a/src/modules/precompiled.rs
+++ b/src/modules/precompiled.rs
@@ -1,148 +1,73 @@
-use std::os::raw::{c_char, c_int, c_void};
-use std::ptr::NonNull;
-use std::sync::Once;
+use secp256k1::{ecdsa::RecoverableSignature, ecdsa::RecoveryId, Message, Secp256k1};
+use sha3::{Digest, Sha3_256};
 
-extern "C" {
-  /// Initializes the Ethjet context in the C library.
-  ///
-  /// # Safety
-  /// This function interacts directly with the underlying C library and should be
-  /// used with caution. Ensure that the context is properly freed after use.
-  pub fn ethjet_init() -> *mut c_void;
+pub fn precompiled_ecrecover(
+  ctx: &Secp256k1<secp256k1::All>,
+  in_data: &[u8],
+  out: &mut [u8],
+) -> Result<(), &'static str> {
+  /*
+  Inputs
+        Byte range	     | Name	 |                  Description
+    ----------------------------------------------------------------------------------
+    [0; 31] (32 bytes)	 | hash	 | Keccack-256 hash of the transaction
+    [32; 63] (32 bytes)	 |  v	   | Recovery identifier, expected to be either 27 or 28
+    [64; 95] (32 bytes)	 |  r	   | x-value, expected to be in the range ]0; secp256k1n[
+    [96; 127] (32 bytes) |	s	   | Expected to be in the range ]0; secp256k1n[
 
-  /// Frees the Ethjet context in the C library.
-  ///
-  /// # Safety
-  /// This function must only be called with a valid, non-null pointer returned by
-  /// `ethjet_init`.
-  pub fn ethjet_free(context: *mut c_void);
+  Output
+        Byte range	     |     Name	     |                    Description
+    ----------------------------------------------------------------------------------------------
+    [0; 31] (32 bytes)	 | publicAddress | The recovered 20-byte address right aligned to 32 bytes
+  */
 
-  /// Executes an operation using the Ethjet context in the C library.
-  ///
-  /// # Arguments
-  ///
-  /// * `context` - A pointer to the initialized Ethjet context.
-  /// * `operation` - The operation to be performed (contract number).
-  /// * `input` - A pointer to the input data buffer.
-  /// * `input_len` - The length of the input data buffer.
-  /// * `output` - A pointer to the output data buffer.
-  /// * `output_len` - The desired length of the output data buffer.
-  ///
-  /// # Returns
-  ///
-  /// Returns `1` if the operation was successful, otherwise returns a non-1 value.
-  ///
-  /// # Safety
-  /// This function interacts directly with the underlying C library, so ensure that
-  /// all pointers passed to it are valid.
-  pub fn ethjet(
-    context: *mut c_void,
-    operation: c_int,
-    input: *const c_char,
-    input_len: c_int,
-    output: *mut c_char,
-    output_len: c_int,
-  ) -> c_int;
-}
-
-/// A wrapper around the Ethjet context provided by the C library.
-///
-/// This struct manages the lifetime of the context, ensuring that it is properly
-/// initialized and freed.
-pub struct EthjetContext(NonNull<c_void>);
+  // Check input size
+  if in_data.len() != 128 {
+    return Err("Invalid input size");
+  }
 
-impl EthjetContext {
-  /// Creates a new `EthjetContext` by initializing the context via the C library.
-  ///
-  /// # Returns
-  ///
-  /// Returns `Some(EthjetContext)` if the context was successfully initialized,
-  /// otherwise returns `None`.
-  pub fn new() -> Option<Self> {
-    let context_ptr = unsafe { ethjet_init() };
-    NonNull::new(context_ptr).map(EthjetContext)
+  // Check output size
+  if out.len() != 32 {
+    return Err("Invalid output size");
   }
 
-  /// Executes a precompiled contract using the Ethjet context.
-  ///
-  /// # Arguments
-  ///
-  /// * `contract` - The number of the precompiled contract to execute.
-  /// * `input` - A byte slice containing the input data.
-  /// * `output_size` - The desired size of the output buffer.
-  ///
-  /// # Returns
-  ///
-  /// Returns `Some(Vec<u8>)` containing the output data if the operation was successful,
-  /// otherwise returns `None`.
-  pub fn execute(&self, contract: i32, input: &[u8], output_size: usize) -> Option<Vec<u8>> {
-    let mut output = vec![0u8; output_size];
-    let status = unsafe {
-      ethjet(
-        self.0.as_ptr(),
-        contract,
-        input.as_ptr() as *const c_char,
-        input.len() as c_int,
-        output.as_mut_ptr() as *mut c_char,
-        output_size as c_int,
-      )
-    };
+  // Extract recovery ID from V (last byte of in_data)
+  let recid = match RecoveryId::from_i32((in_data[63] - 27) as i32) {
+    Ok(id) => id,
+    Err(_) => return Err("Invalid recid"),
+  };
 
-    match status {
-      1 => Some(output),
-      _ => None,
-    }
+  // Check higher bytes of V are zero
+  if in_data[32..63].iter().all(|&x| x != 0) {
+    return Err("Invalid higher bytes of V");
   }
-}
 
-impl Drop for EthjetContext {
-  /// Frees the Ethjet context when the `EthjetContext` struct is dropped.
-  ///
-  /// This ensures that the C library's resources are properly released when the Rust
-  /// wrapper goes out of scope.
-  fn drop(&mut self) {
-    unsafe {
-      ethjet_free(self.0.as_ptr());
-    }
-  }
-}
+  // Prepare the signature and message
+  let sig = match RecoverableSignature::from_compact(&in_data[64..128], recid) {
+    Ok(s) => s,
+    Err(_) => return Err("Failed to parse signature"),
+  };
+  let message = match Message::from_digest_slice(&in_data[0..32]) {
+    Ok(m) => m,
+    Err(_) => return Err("Failed to parse message"),
+  };
 
-static INIT: Once = Once::new();
-static mut GLOBAL_CONTEXT: Option<EthjetContext> = None;
+  // Recover the public key
+  let pubkey = match ctx.recover_ecdsa(&message, &sig) {
+    Ok(pk) => pk,
+    Err(_) => return Err("Failed to recover public key"),
+  };
 
-/// Retrieves the global `EthjetContext`, initializing it if necessary.
-///
-/// # Returns
-///
-/// Returns a reference to the global `EthjetContext`. If initialization fails,
-/// the program will panic.
-///
-/// # Safety
-///
-/// This function should only be called from a single thread during the initialization phase,
-/// as it uses unsafe code to manage the global context.
-pub fn get_global_context() -> &'static EthjetContext {
-  unsafe {
-    INIT.call_once(|| {
-      GLOBAL_CONTEXT = EthjetContext::new();
-    });
-    GLOBAL_CONTEXT.as_ref().expect("Failed to initialize EthjetContext")
-  }
-}
+  // Serialize the public key to uncompressed form
+  let pubkey_uncompressed = pubkey.serialize_uncompressed();
+
+  // Hash the public key with SHA3-256
+  let mut hasher = Sha3_256::new();
+  hasher.update(&pubkey_uncompressed[1..65]); // skip the first byte
+  let hash = hasher.finalize();
+
+  // Copy the first 32 bytes of the hash to the output
+  out.copy_from_slice(&hash[0..32]);
 
-/// Executes a precompiled contract using the global `EthjetContext`.
-///
-/// # Arguments
-///
-/// * `contract` - The number of the precompiled contract to execute.
-/// * `input` - A byte slice containing the input data.
-/// * `output_size` - The desired size of the output buffer.
-///
-/// # Returns
-///
-/// Returns `Some(Vec<u8>)` containing the output data if the operation was successful,
-/// otherwise returns `None`.
-pub fn execute(contract: i32, input: &[u8], output_size: usize) -> Option<Vec<u8>> {
-  let context = get_global_context();
-  context.execute(contract, input, output_size)
+  Ok(())
 }
diff --git a/src/modules/smt.rs b/src/modules/smt.rs
index 5efade0..5140e0b 100644
--- a/src/modules/smt.rs
+++ b/src/modules/smt.rs
@@ -12,7 +12,7 @@ use crate::modules::expr::{
 use crate::modules::format::format_prop;
 use crate::modules::keccak::{keccak_assumptions, keccak_compute};
 use crate::modules::traversals::{fold_prop, TraversableTerm};
-use crate::modules::types::{AddableVec, Addr, Expr, GVar, Prop, W256W256Map, W256};
+use crate::modules::types::{AddableVec, Addr, Expr, GVar, Prop, W256W256Map, EXPR_MEMPTY, W256};
 
 // Type aliases for convenience
 type Text = String;
@@ -292,15 +292,15 @@ pub fn get_var(cex: &SMTCex, name: &str) -> W256 {
 
 fn encode_store(n: usize, expr: &Expr) -> SMT2 {
   let expr_to_smt = expr_to_smt(expr.clone());
-  let txt = format!("(define-fun store{} () Storage {})", n, expr_to_smt);
+  let txt = format!("(define-fun store{:012} () Storage {})", n, expr_to_smt);
   SMT2(vec![txt], RefinementEqs(vec![], vec![]), CexVars::new(), vec![])
 }
 
 fn encode_buf(n: usize, expr: &Expr, bufs: &BufEnv) -> SMT2 {
   let buf_smt = expr_to_smt(expr.clone());
-  let def_buf = format!("(define-fun buf{} () Buf {})", n, buf_smt);
+  let def_buf = format!("(define-fun buf{:012} () Buf {})", n, buf_smt);
   let len_smt = expr_to_smt(buf_length_env(bufs, true, expr.clone()));
-  let def_len = format!("(define-fun buf{}_length () (_ BitVec 256) {})", n, len_smt);
+  let def_len = format!("(define-fun buf{:012}_length () (_ BitVec 256) {})", n, len_smt);
   SMT2(vec![def_buf, def_len], RefinementEqs(vec![], vec![]), CexVars::new(), vec![])
 }
 
@@ -833,7 +833,6 @@ fn create_read_assumptions(ps_elim: &Vec<Box<Prop>>, bufs: &BufEnv, stores: &Sto
 
 pub fn assert_props(config: &Config, ps_pre_conc: Vec<Box<Prop>>) -> Option<SMT2> {
   let simplified_ps = decompose(simplify_props(ps_pre_conc.clone()), config);
-
   if (&simplified_ps).into_iter().any(|p| **p == Prop::PBool(false)) {
     return None;
   }
@@ -878,7 +877,7 @@ pub fn assert_props(config: &Config, ps_pre_conc: Vec<Box<Prop>>) -> Option<SMT2
     .flat_map(|term: Prop| referenced_abstract_stores(&term))
     .collect();
   let abstract_stores: Vec<Builder> = abstract_stores_set.into_iter().collect();
-  let addresses =
+  let addresses: HashSet<String> =
     to_declare_ps.into_iter().map(|t| *t.clone()).flat_map(|term: Prop| referenced_waddrs(&term)).collect();
 
   /*allVars = fmap referencedVars toDeclarePsElim <> fmap referencedVars bufVals <> fmap referencedVars storeVals <> [abstrVars abst] */
@@ -909,7 +908,7 @@ pub fn assert_props(config: &Config, ps_pre_conc: Vec<Box<Prop>>) -> Option<SMT2
     + (smt2_line("; intermediate buffers & stores".to_owned()))
     + (declare_abstract_stores(&abstract_stores))
     + (smt2_line("".to_owned()))
-    + (declare_addrs(addresses))
+    + (declare_addrs(addresses.into_iter().collect()))
     + (smt2_line("".to_owned()))
     + (declare_bufs(&to_declare_ps_elim, bufs, stores))
     + (smt2_line("".to_owned()))
@@ -969,8 +968,8 @@ fn expr_to_smt(expr: Expr) -> String {
   match expr.clone() {
     Expr::Lit(w) => format!("(_ bv{} 256)", w.to_decimal()),
     Expr::Var(s) => s,
-    Expr::GVar(GVar::BufVar(n)) => format!("buf{}", n),
-    Expr::GVar(GVar::StoreVar(n)) => format!("store{}", n),
+    Expr::GVar(GVar::BufVar(n)) => format!("buf{:012}", n),
+    Expr::GVar(GVar::StoreVar(n)) => format!("store{:012}", n),
     Expr::JoinBytes(v) => concat_bytes(&v),
     Expr::Add(a, b) => op2("bvadd", unbox(a), unbox(b)),
     Expr::Sub(a, b) => op2("bvsub", unbox(a), unbox(b)),
@@ -1103,7 +1102,7 @@ fn expr_to_smt(expr: Expr) -> String {
     },
     Expr::ReadByte(idx, src) => op2("select", *src, *idx),
     Expr::ConcreteBuf(bs) if bs.len() == 0 => "((as const Buf) #b00000000)".to_string(),
-    Expr::ConcreteBuf(bs) => write_bytes(&bs, Expr::Mempty),
+    Expr::ConcreteBuf(bs) => write_bytes(&bs, EXPR_MEMPTY),
     Expr::AbstractBuf(s) => s,
     Expr::ReadWord(idx, prev) => op2("readWord", *idx, *prev),
 
@@ -1232,7 +1231,9 @@ fn internal(size: Expr, src_offset: Expr, dst_offset: Expr, dst: Builder) -> Bui
 
 // Unrolls an exponentiation into a series of multiplications
 fn expand_exp(base: Expr, expnt: W256) -> Builder {
-  if expnt == W256(1, 0) {
+  if expnt == W256(0, 0) {
+    expr_to_smt(Expr::Lit(W256(1, 0)))
+  } else if expnt == W256(1, 0) {
     expr_to_smt(base)
   } else {
     let b = expr_to_smt(base.clone());
@@ -1243,7 +1244,7 @@ fn expand_exp(base: Expr, expnt: W256) -> Builder {
 
 // Concatenates a list of bytes into a larger bitvector
 fn write_bytes(bytes: &[u8], buf: Expr) -> Builder {
-  let skip_zeros = buf == Expr::Mempty;
+  let skip_zeros = buf == EXPR_MEMPTY;
   let mut idx = 0;
   let mut inner = expr_to_smt(buf);
   for &byte in bytes {
diff --git a/src/modules/symexec.rs b/src/modules/symexec.rs
index 1e44809..dbc5509 100644
--- a/src/modules/symexec.rs
+++ b/src/modules/symexec.rs
@@ -68,7 +68,7 @@ pub fn sym_abi_arg(name: &str, abi_type: AbiType) -> CalldataFragment {
       let v = Expr::Var(name.into());
       CalldataFragment::St(vec![Box::new(to_bool(&v))], v)
     }
-    AbiType::AbiAddressType => CalldataFragment::St(vec![], Expr::SymAddr(name.into())),
+    AbiType::AbiAddressType => CalldataFragment::St(vec![], Expr::WAddr(Box::new(Expr::SymAddr(name.into())))),
     AbiType::AbiBytesType(n) => {
       if n > 0 && n <= 32 {
         let v = Expr::Var(name.into());
diff --git a/src/modules/traversals.rs b/src/modules/traversals.rs
index 1cc0d1b..216aba4 100644
--- a/src/modules/traversals.rs
+++ b/src/modules/traversals.rs
@@ -355,11 +355,7 @@ pub fn fold_expr<B>(f: &mut dyn FnMut(&Expr) -> B, acc: B, expr: &Expr) -> B
 where
   B: Add<B, Output = B> + Default + Clone,
 {
-  if *expr == Expr::Mempty {
-    acc.clone()
-  } else {
-    acc.clone() + go_expr(f, acc.clone(), expr.clone())
-  }
+  acc.clone() + go_expr(f, acc.clone(), expr.clone())
 }
 
 /// A trait for types that can map a function over their `Expr` components.
@@ -777,7 +773,6 @@ impl ExprMappable for Expr {
         let a = a.map_expr_m(f);
         f(&Expr::BufLength(Box::new(a)))
       }
-      Expr::Mempty => Expr::Mempty,
       _ => panic!("unuexpected expr {}", self),
     }
   }
@@ -798,11 +793,7 @@ pub fn map_expr<F>(mut f: F, expr: Expr) -> Expr
 where
   F: FnMut(&Expr) -> Expr,
 {
-  if expr == Expr::Mempty {
-    expr
-  } else {
-    expr.map_expr_m(&mut f)
-  }
+  expr.map_expr_m(&mut f)
 }
 
 /// Recursively applies a given function `f` to each `Expr` within a `Prop`.
diff --git a/src/modules/types.rs b/src/modules/types.rs
index 617f8fa..e6a0532 100644
--- a/src/modules/types.rs
+++ b/src/modules/types.rs
@@ -402,7 +402,6 @@ impl fmt::Display for GVar {
 
 #[derive(Debug, Clone)]
 pub enum Expr {
-  Mempty,
   // Identifiers
   Lit(W256),
   Var(String),
@@ -515,7 +514,6 @@ pub enum Expr {
 impl fmt::Display for Expr {
   fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
     match self {
-      Expr::Mempty => write!(f, "Mempty"),
       Expr::Lit(val) => write!(f, "Lit(0x{})", val.to_hex()),
       Expr::Var(name) => write!(f, "Var({})", name),
       Expr::GVar(gvar) => write!(f, "GVar({})", gvar),
@@ -601,6 +599,8 @@ impl fmt::Display for Expr {
   }
 }
 
+pub const EXPR_MEMPTY: Expr = Expr::ConcreteBuf(vec![]);
+
 impl Eq for Expr {}
 
 impl PartialEq for Expr {
@@ -608,7 +608,6 @@ impl PartialEq for Expr {
     use Expr::*;
 
     match (self, other) {
-      (Mempty, Mempty) => true,
       (Lit(val1), Lit(val2)) => val1 == val2,
       (Var(name1), Var(name2)) => name1 == name2,
       (GVar(gvar1), GVar(gvar2)) => gvar1 == gvar2,
@@ -710,9 +709,6 @@ impl Hash for Expr {
     use Expr::*;
 
     match self {
-      Mempty => {
-        "Mempty".hash(state);
-      }
       Lit(val) => {
         "Lit".hash(state);
         val.hash(state);
@@ -1167,7 +1163,7 @@ pub fn update_balance(c: Contract, new_balance: Expr) -> Contract {
 impl Contract {
   pub fn bytecode(&self) -> Option<Expr> {
     match &self.code {
-      ContractCode::InitCode(_, _) => Some(Expr::Mempty), // Equivalent to Just mempty
+      ContractCode::InitCode(_, _) => Some(EXPR_MEMPTY), // Equivalent to Just mempty
       ContractCode::RuntimeCode(RuntimeCodeStruct::ConcreteRuntimeCode(bs)) => Some(Expr::ConcreteBuf(*bs.clone())),
       ContractCode::RuntimeCode(RuntimeCodeStruct::SymbolicRuntimeCode(ops)) => Some(from_list(ops.to_vec())),
       ContractCode::UnKnownCode(_) => None,
@@ -1587,7 +1583,7 @@ where
 // Implement the Default trait for AddableVec
 impl Default for Expr {
   fn default() -> Expr {
-    Expr::Mempty // Return an empty vector
+    EXPR_MEMPTY // Return an empty vector
   }
 }
 
diff --git a/tests/evm_test.rs b/tests/evm_test.rs
index 5c88dff..6571da5 100644
--- a/tests/evm_test.rs
+++ b/tests/evm_test.rs
@@ -6,7 +6,7 @@ use rhoevm::modules::format::{hex_byte_string, strip_0x};
 
 //use rhoevm::modules::solvers::{with_solvers, Solver};
 use rhoevm::modules::transactions::init_tx;
-use rhoevm::modules::types::{ContractCode, Expr, Memory, Prop, RuntimeCodeStruct, VM, W256};
+use rhoevm::modules::types::{ContractCode, Expr, Memory, Prop, RuntimeCodeStruct, EXPR_MEMPTY, VM, W256};
 
 const MAX_NUM_ITERATIONS: u32 = 1;
 
@@ -22,7 +22,7 @@ fn dummy_symvm_from_command(cmd: &SymbolicCommand, calldata: (Expr, Vec<Box<Prop
     (_, _, Some(code)) => {
       let bs = hex_byte_string("bytes", &strip_0x(code));
       let mc = if cmd.create {
-        ContractCode::InitCode(Box::new(bs), Box::new(Expr::Mempty))
+        ContractCode::InitCode(Box::new(bs), Box::new(EXPR_MEMPTY))
       } else {
         ContractCode::RuntimeCode(RuntimeCodeStruct::ConcreteRuntimeCode(Box::new(bs)))
       };
diff --git a/tests/precompiled_test.rs b/tests/precompiled_test.rs
new file mode 100644
index 0000000..9aafd58
--- /dev/null
+++ b/tests/precompiled_test.rs
@@ -0,0 +1,56 @@
+use secp256k1::rand::rngs::OsRng;
+use secp256k1::{Message, PublicKey, Secp256k1, SecretKey};
+use sha3::{Digest, Sha3_256};
+
+use rhoevm::modules::precompiled::precompiled_ecrecover;
+
+#[test]
+fn test_ecrecover_success() {
+  let secp = Secp256k1::new();
+  let mut rng = OsRng;
+
+  // Generate a random secret key and corresponding public key
+  let sk = SecretKey::new(&mut rng);
+  let pk = PublicKey::from_secret_key(&secp, &sk);
+
+  // Create a message and its corresponding recoverable signature
+  let message = Message::from_digest_slice(&[0xab; 32]).unwrap();
+  let (recid, sig) = secp.sign_ecdsa_recoverable(&message, &sk).serialize_compact();
+
+  // Prepare the input (message, V, R, S concatenated)
+  let mut input = [0u8; 128];
+  input[0..32].copy_from_slice(&message[..]);
+  input[63] = (recid.to_i32() + 27) as u8;
+  input[64..128].copy_from_slice(&sig);
+
+  // Prepare the output buffer
+  let mut output = [0u8; 32];
+
+  // Call the function
+  let result = precompiled_ecrecover(&secp, &input, &mut output);
+
+  // Assert the function succeeded
+  assert!(result.is_ok());
+
+  // Compute the expected output (SHA3-256 of the public key)
+  let mut hasher = Sha3_256::new();
+  hasher.update(&pk.serialize_uncompressed()[1..65]);
+  let expected_hash = hasher.finalize();
+
+  // The output should match the first 32 bytes of the expected hash
+  assert_eq!(&output, &expected_hash[..32]);
+}
+
+#[test]
+fn test_ecrecover_invalid_recid() {
+  let secp = Secp256k1::new();
+  let mut input = [0u8; 128];
+  let mut output = [0u8; 32];
+
+  // Set an invalid recid value
+  input[63] = 31; // recid would be 4, which is invalid
+
+  let result = precompiled_ecrecover(&secp, &input, &mut output);
+  assert!(result.is_err());
+  assert_eq!(result.err().unwrap(), "Invalid recid");
+}