# Certora Prover Report

**Generated:** 2025-08-24 11:02:26
**Job URL:** https://prover.certora.com/output/60724/03ed357c1fec4934a150b162b6061122
**Job ID:** 03ed357c1fec4934a150b162b6061122

## Summary

- **Total Assert Nodes:** 33
- **Violated:** 0 ❌
- **Verified:** 33 ✅

✅ **All assertions verified successfully**

## Detailed Results

### 1. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowDst.cancel((bytes32,bytes32,uint256,uint256,uint256,uint256,uint256,uint256,bytes))`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_34.json`
- 🔍 Debug trace: `dap_calltrace_34-certora-dap.json`

---

### 2. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowDst.publicWithdraw(bytes32,(bytes32,bytes32,uint256,uint256,uint256,uint256,uint256,uint256,bytes))`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_37.json`
- 🔍 Debug trace: `dap_calltrace_37-certora-dap.json`

---

### 3. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowDst.withdraw(bytes32,(bytes32,bytes32,uint256,uint256,uint256,uint256,uint256,uint256,bytes))`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_36.json`
- 🔍 Debug trace: `dap_calltrace_36-certora-dap.json`

---

### 4. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowDst.FACTORY()`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_2.json`
- 🔍 Debug trace: `dap_calltrace_2-certora-dap.json`

---

### 5. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowDst.RESCUE_DELAY()`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_9.json`
- 🔍 Debug trace: `dap_calltrace_9-certora-dap.json`

---

### 6. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowDst.PROXY_BYTECODE_HASH()`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_10.json`
- 🔍 Debug trace: `dap_calltrace_10-certora-dap.json`

---

### 7. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowDst.rescueFunds(address,uint256,(bytes32,bytes32,uint256,uint256,uint256,uint256,uint256,uint256,bytes))`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_29.json`
- 🔍 Debug trace: `dap_calltrace_29-certora-dap.json`

---

### 8. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowFactory.addressOfEscrowDst((bytes32,bytes32,uint256,uint256,uint256,uint256,uint256,uint256,bytes))`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_23.json`
- 🔍 Debug trace: `dap_calltrace_23-certora-dap.json`

---

### 9. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowFactory.addressOfEscrowSrc((bytes32,bytes32,uint256,uint256,uint256,uint256,uint256,uint256,bytes))`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_22.json`
- 🔍 Debug trace: `dap_calltrace_22-certora-dap.json`

---

### 10. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowFactory.getMakingAmount((uint256,uint256,uint256,uint256,uint256,uint256,uint256,uint256),bytes,bytes32,address,uint256,uint256,bytes)`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_24.json`
- 🔍 Debug trace: `dap_calltrace_24-certora-dap.json`

---

### 11. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowFactory.getTakingAmount((uint256,uint256,uint256,uint256,uint256,uint256,uint256,uint256),bytes,bytes32,address,uint256,uint256,bytes)`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_25.json`
- 🔍 Debug trace: `dap_calltrace_25-certora-dap.json`

---

### 12. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowFactory.createDstEscrow((bytes32,bytes32,uint256,uint256,uint256,uint256,uint256,uint256,bytes),uint256)`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_31.json`
- 🔍 Debug trace: `dap_calltrace_31-certora-dap.json`

---

### 13. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowFactory.ESCROW_SRC_IMPLEMENTATION()`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_1.json`
- 🔍 Debug trace: `dap_calltrace_1-certora-dap.json`

---

### 14. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowFactory.<receiveOrFallback>()`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_12.json`
- 🔍 Debug trace: `dap_calltrace_12-certora-dap.json`

---

### 15. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowFactory.ESCROW_DST_IMPLEMENTATION()`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_7.json`
- 🔍 Debug trace: `dap_calltrace_7-certora-dap.json`

---

### 16. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowFactory.owner()`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_8.json`
- 🔍 Debug trace: `dap_calltrace_8-certora-dap.json`

---

### 17. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowFactory.renounceOwnership()`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_16.json`
- 🔍 Debug trace: `dap_calltrace_16-certora-dap.json`

---

### 18. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowFactory.lastValidated(bytes32)`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_4.json`
- 🔍 Debug trace: `dap_calltrace_4-certora-dap.json`

---

### 19. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowFactory.transferOwnership(address)`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_17.json`
- 🔍 Debug trace: `dap_calltrace_17-certora-dap.json`

---

### 20. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowFactory.postInteraction((uint256,uint256,uint256,uint256,uint256,uint256,uint256,uint256),bytes,bytes32,address,uint256,uint256,uint256,bytes)`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_35.json`
- 🔍 Debug trace: `dap_calltrace_35-certora-dap.json`

---

### 21. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowFactory.takerInteraction((uint256,uint256,uint256,uint256,uint256,uint256,uint256,uint256),bytes,bytes32,address,uint256,uint256,uint256,bytes)`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_19.json`
- 🔍 Debug trace: `dap_calltrace_19-certora-dap.json`

---

### 22. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowFactory.rescueFunds(address,uint256)`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_20.json`
- 🔍 Debug trace: `dap_calltrace_20-certora-dap.json`

---

### 23. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowSrc.withdrawTo(bytes32,address,(bytes32,bytes32,uint256,uint256,uint256,uint256,uint256,uint256,bytes))`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_32.json`
- 🔍 Debug trace: `dap_calltrace_32-certora-dap.json`

---

### 24. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowSrc.publicCancel((bytes32,bytes32,uint256,uint256,uint256,uint256,uint256,uint256,bytes))`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_27.json`
- 🔍 Debug trace: `dap_calltrace_27-certora-dap.json`

---

### 25. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowSrc.cancel((bytes32,bytes32,uint256,uint256,uint256,uint256,uint256,uint256,bytes))`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_28.json`
- 🔍 Debug trace: `dap_calltrace_28-certora-dap.json`

---

### 26. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowSrc.publicWithdraw(bytes32,(bytes32,bytes32,uint256,uint256,uint256,uint256,uint256,uint256,bytes))`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_33.json`
- 🔍 Debug trace: `dap_calltrace_33-certora-dap.json`

---

### 27. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowSrc.withdraw(bytes32,(bytes32,bytes32,uint256,uint256,uint256,uint256,uint256,uint256,bytes))`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_30.json`
- 🔍 Debug trace: `dap_calltrace_30-certora-dap.json`

---

### 28. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowSrc.FACTORY()`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_6.json`
- 🔍 Debug trace: `dap_calltrace_6-certora-dap.json`

---

### 29. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowSrc.RESCUE_DELAY()`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_13.json`
- 🔍 Debug trace: `dap_calltrace_13-certora-dap.json`

---

### 30. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowSrc.PROXY_BYTECODE_HASH()`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_15.json`
- 🔍 Debug trace: `dap_calltrace_15-certora-dap.json`

---

### 31. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `EscrowSrc.rescueFunds(address,uint256,(bytes32,bytes32,uint256,uint256,uint256,uint256,uint256,uint256,bytes))`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_26.json`
- 🔍 Debug trace: `dap_calltrace_26-certora-dap.json`

---

### 32. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `MerkleStorageInvalidator.lastValidated(bytes32)`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_14.json`
- 🔍 Debug trace: `dap_calltrace_14-certora-dap.json`

---

### 33. ✅ sanity

- **Status:** **VERIFIED**
- **Method:** `MerkleStorageInvalidator.takerInteraction((uint256,uint256,uint256,uint256,uint256,uint256,uint256,uint256),bytes,bytes32,address,uint256,uint256,uint256,bytes)`
- **Assert Message:** Reaching end of method's code
- **Location:** `certora_generic_checker/sanity.spec:Unknown line`

**Available Traces:**
- 📄 Raw trace: `rule_output_18.json`
- 🔍 Debug trace: `dap_calltrace_18-certora-dap.json`

---
