114 lines
2.9 KiB
Bash
114 lines
2.9 KiB
Bash
|
#!/usr/bin/env bash
|
||
|
|
# Verify Bridge Contracts with Certora Prover
|
||
|
|
# Runs formal verification for all bridge contracts
|
||
|
|
|
||
|
|
set -euo pipefail
|
||
|
|
|
||
|
|
SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
|
||
|
|
PROJECT_ROOT="$(cd "$SCRIPT_DIR/../../.." && pwd)"
|
||
|
|
|
||
|
|
CERTORA_DIR="$PROJECT_ROOT/verification/certora"
|
||
|
|
SPECS_DIR="$CERTORA_DIR/specs"
|
||
|
|
REPORTS_DIR="$PROJECT_ROOT/verification/reports"
|
||
|
|
CONTRACTS_DIR="$PROJECT_ROOT/contracts/bridge/trustless"
|
||
|
|
|
||
|
|
echo "Certora Formal Verification - Trustless Bridge"
|
||
|
|
echo "==============================================="
|
||
|
|
echo ""
|
||
|
|
|
||
|
|
# Check if Certora is installed
|
||
|
|
if ! command -v certoraRun &> /dev/null; then
|
||
|
|
echo "Error: Certora Prover not found"
|
||
|
|
echo ""
|
||
|
|
echo "To install Certora Prover:"
|
||
|
|
echo "1. Contact Certora for a license: https://www.certora.com/"
|
||
|
|
echo "2. Follow installation instructions from Certora"
|
||
|
|
echo "3. Ensure certoraRun is in your PATH"
|
||
|
|
exit 1
|
||
|
|
fi
|
||
|
|
|
||
|
|
# Check if specs exist
|
||
|
|
if [ ! -d "$SPECS_DIR" ]; then
|
||
|
|
echo "Error: Specifications directory not found: $SPECS_DIR"
|
||
|
|
exit 1
|
||
|
|
fi
|
||
|
|
|
||
|
|
# Create reports directory
|
||
|
|
mkdir -p "$REPORTS_DIR"
|
||
|
|
|
||
|
|
echo "Verification Configuration:"
|
||
|
|
echo " Contracts: $CONTRACTS_DIR"
|
||
|
|
echo " Specs: $SPECS_DIR"
|
||
|
|
echo " Reports: $REPORTS_DIR"
|
||
|
|
echo ""
|
||
|
|
|
||
|
|
# Verify each contract
|
||
|
|
CONTRACTS=(
|
||
|
|
"BondManager"
|
||
|
|
"ChallengeManager"
|
||
|
|
"InboxETH"
|
||
|
|
"LiquidityPoolETH"
|
||
|
|
"Lockbox138"
|
||
|
|
)
|
||
|
|
|
||
|
|
PASSED=0
|
||
|
|
FAILED=0
|
||
|
|
|
||
|
|
for contract in "${CONTRACTS[@]}"; do
|
||
|
|
contract_file="$CONTRACTS_DIR/${contract}.sol"
|
||
|
|
spec_file="$SPECS_DIR/${contract}.spec"
|
||
|
|
|
||
|
|
if [ ! -f "$contract_file" ]; then
|
||
|
|
echo "⚠️ Skipping $contract: contract file not found"
|
||
|
|
continue
|
||
|
|
fi
|
||
|
|
|
||
|
|
if [ ! -f "$spec_file" ]; then
|
||
|
|
echo "⚠️ Skipping $contract: specification file not found"
|
||
|
|
continue
|
||
|
|
fi
|
||
|
|
|
||
|
|
echo "Verifying $contract..."
|
||
|
|
echo " Contract: $contract_file"
|
||
|
|
echo " Spec: $spec_file"
|
||
|
|
|
||
|
|
# Run Certora verification
|
||
|
|
if certoraRun "$contract_file" \
|
||
|
|
--verify "$contract:$spec_file" \
|
||
|
|
--solc solc-0.8.19 \
|
||
|
|
--optimistic_loop \
|
||
|
|
--loop_iter 3 \
|
||
|
|
--smt_timeout 600 \
|
||
|
|
--msg "$contract verification" \
|
||
|
|
--output_dir "$REPORTS_DIR" \
|
||
|
|
2>&1 | tee "$REPORTS_DIR/${contract}_verification.log"; then
|
||
|
|
echo "✅ $contract: Verification passed"
|
||
|
|
PASSED=$((PASSED + 1))
|
||
|
|
else
|
||
|
|
echo "❌ $contract: Verification failed"
|
||
|
|
FAILED=$((FAILED + 1))
|
||
|
|
fi
|
||
|
|
|
||
|
|
echo ""
|
||
|
|
done
|
||
|
|
|
||
|
|
echo "=========================================="
|
||
|
|
echo "Verification Summary"
|
||
|
|
echo "=========================================="
|
||
|
|
echo " ✅ Passed: $PASSED"
|
||
|
|
echo " ❌ Failed: $FAILED"
|
||
|
|
echo " 📊 Total: $((PASSED + FAILED))"
|
||
|
|
echo ""
|
||
|
|
echo "Reports saved to: $REPORTS_DIR"
|
||
|
|
|
||
|
|
if [ $FAILED -eq 0 ]; then
|
||
|
|
echo ""
|
||
|
|
echo "✅ All verifications passed!"
|
||
|
|
exit 0
|
||
|
|
else
|
||
|
|
echo ""
|
||
|
|
echo "❌ Some verifications failed. Review reports for details."
|
||
|
|
exit 1
|
||
|
|
fi
|
||
|
|
|