┌─────────────────────────────────────────────────────────────────────────────┐
│                    FORMAL VERIFICATION APPROACHES                          │
├─────────────────────────────────────────────────────────────────────────────┤
│                                                                             │
│  1. THEOREM PROVING                                                         │
│  ┌──────────────────────────────────────────────────────────────────────┐   │
│  │ • Uses mathematical logic to prove properties                       │   │
│  │ • Requires manual guidance (proof assistants)                       │   │
│  │ • Examples: Coq, Isabelle/HOL, Lean                               │   │
│  │ • Pros: Very powerful, can prove complex properties               │   │
│  │ • Cons: Requires expert knowledge, time-consuming                 │   │
│  └──────────────────────────────────────────────────────────────────────┘   │
│                                                                             │
│  2. MODEL CHECKING                                                         │
│  ┌──────────────────────────────────────────────────────────────────────┐   │
│  │ • Exhaustively checks all states of a finite-state model           │   │
│  │ • Automated, no manual guidance                                      │   │
│  │ • Examples: SPIN, NuSMV                                              │   │
│  │ • Pros: Automated, finds bugs                                        │   │
│  │ • Cons: State explosion problem                                     │   │
│  └──────────────────────────────────────────────────────────────────────┘   │
│                                                                             │
│  3. SYMBOLIC EXECUTION                                                     │
│  ┌──────────────────────────────────────────────────────────────────────┐   │
│  │ • Explores all possible execution paths with symbolic values       │   │
│  │ • Examples: Mythril, Manticore                                      │   │
│  │ • Pros: Finds bugs, works on existing code                          │   │
│  │ • Cons: Path explosion                                               │   │
│  └──────────────────────────────────────────────────────────────────────┘   │
│                                                                             │
│  4. PROPERTY-BASED TESTING                                                  │
│  ┌──────────────────────────────────────────────────────────────────────┐   │
│  │ • Tests properties with random inputs                                │   │
│  │ • Examples: QuickCheck, Echidna, Foundry fuzzing                   │   │
│  │ • Pros: Practical, discovers bugs                                   │   │
│  │ • Cons: Not exhaustive                                               │   │
│  └──────────────────────────────────────────────────────────────────────┘   │
│                                                                             │
└─────────────────────────────────────────────────────────────────────────────┘

┌─────────────────────────────────────────────────────────────────────────────┐
│                    SECURE DEVELOPMENT LIFECYCLE                             │
├─────────────────────────────────────────────────────────────────────────────┤
│                                                                             │
│  1. REQUIREMENTS                                                           │
│  ┌──────────────────────────────────────────────────────────────────────┐   │
│  │ • Define security requirements                                      │   │
│  │ • Identify threat model                                              │   │
│  │ • Specify invariants                                                 │   │
│  └──────────────────────────────────────────────────────────────────────┘   │
│                                    │                                        │
│                                    v                                        │
│  2. DESIGN                                                                 │
│  ┌──────────────────────────────────────────────────────────────────────┐   │
│  │ • Security by design                                                 │   │
│  │ • Minimise attack surface                                           │   │
│  │ • Define access controls                                             │   │
│  └──────────────────────────────────────────────────────────────────────┘   │
│                                    │                                        │
│                                    v                                        │
│  3. IMPLEMENTATION                                                         │
│  ┌──────────────────────────────────────────────────────────────────────┐   │
│  │ • Follow secure coding practices                                    │   │
│  │ • Use established libraries                                         │   │
│  │ • Regular code review                                               │   │
│  └──────────────────────────────────────────────────────────────────────┘   │
│                                    │                                        │
│                                    v                                        │
│  4. TESTING                                                                │
│  ┌──────────────────────────────────────────────────────────────────────┐   │
│  │ • Unit tests                                                         │   │
│  │ • Integration tests                                                  │   │
│  │ • Fuzzing                                                           │   │
│  │ • Formal verification                                                │   │
│  └──────────────────────────────────────────────────────────────────────┘   │
│                                    │                                        │
│                                    v                                        │
│  5. DEPLOYMENT & MONITORING                                               │
│  ┌──────────────────────────────────────────────────────────────────────┐   │
│  │ • Deploy with monitoring                                            │   │
│  │ • Incident response ready                                           │   │
│  │ • Continuous security monitoring                                   │   │
│  └──────────────────────────────────────────────────────────────────────┘   │
│                                                                             │
└─────────────────────────────────────────────────────────────────────────────┘

# ===================================================================
# MODULE 9, LESSON 3: FORMAL VERIFICATION AND SECURE DEVELOPMENT
# ===================================================================

import hashlib
import random
from typing import Dict, List, Callable, Tuple
import warnings
warnings.filterwarnings('ignore')

print("="*70)
print("FORMAL VERIFICATION AND SECURE DEVELOPMENT")
print("="*70)

# ----------------------------------------------------------------
# PART A: PROPERTY-BASED TESTING SIMULATION
# ----------------------------------------------------------------

print("\n" + "-"*60)
print("PART A: Property-Based Testing Simulation")
print("-"*60)

class PropertyTester:
    """
    Simulated property-based testing for smart contracts.
    """
    def __init__(self):
        self.properties = []
        self.results = []
    
    def add_property(self, name: str, test_func: Callable, description: str):
        """Add a property to test."""
        self.properties.append({
            'name': name,
            'test': test_func,
            'description': description
        })
    
    def run_tests(self, test_cases: int = 100) -> Dict:
        """Run property tests with random inputs."""
        results = {}
        for prop in self.properties:
            passed = 0
            failures = []
            for i in range(test_cases):
                try:
                    if prop['test']():
                        passed += 1
                    else:
                        failures.append(i)
                except Exception as e:
                    failures.append({'index': i, 'error': str(e)})
            
            results[prop['name']] = {
                'passed': passed,
                'total': test_cases,
                'success_rate': passed / test_cases,
                'failures': len(failures),
                'description': prop['description']
            }
        
        return results

# Define test properties
def balance_invariant():
    """Simulate balance non-negativity invariant."""
    balance = random.randint(-10, 100)
    return balance >= 0

def transfer_invariant():
    """Simulate transfer preserving total supply."""
    sender_balance = random.randint(0, 100)
    recipient_balance = random.randint(0, 100)
    amount = random.randint(0, min(50, sender_balance))
    
    new_sender = sender_balance - amount
    new_recipient = recipient_balance + amount
    
    # Check total balance is preserved
    old_total = sender_balance + recipient_balance
    new_total = new_sender + new_recipient
    
    return old_total == new_total

def access_control_test():
    """Simulate access control check."""
    roles = ['admin', 'user', 'guest']
    role = random.choice(roles)
    function = random.choice(['admin_only', 'user_only', 'public'])
    
    if function == 'admin_only':
        return role == 'admin'
    elif function == 'user_only':
        return role in ['admin', 'user']
    else:
        return True

# Run property tests
tester = PropertyTester()
tester.add_property('Balance Non-negative', balance_invariant, 'Balances are never negative')
tester.add_property('Total Supply Preserved', transfer_invariant, 'Total supply is constant')
tester.add_property('Access Control Correct', access_control_test, 'Access control enforces roles')

print("Property-Based Testing Simulation:")
results = tester.run_tests(100)

for prop, result in results.items():
    status = "✅" if result['success_rate'] == 1.0 else "⚠️" if result['success_rate'] > 0.8 else "❌"
    print(f"\n{status} {prop}: {result['success_rate']:.0%} passed")
    print(f"  {result['description']}")
    if result['failures'] > 0:
        print(f"  Failures: {result['failures']}/{result['total']}")

# ----------------------------------------------------------------
# PART B: INVARIANT CHECKING SIMULATION
# -----------------------------------------------------------------

print("\n" + "-"*60)
print("PART B: Invariant Checking Simulation")
print("-"*60)

class InvariantChecker:
    """
    Simulated invariant checking for a contract.
    """
    def __init__(self):
        self.state = {}
        self.invariants = []
        self.violations = []
    
    def set_state(self, key: str, value):
        self.state[key] = value
    
    def add_invariant(self, name: str, check_func: Callable):
        self.invariants.append({
            'name': name,
            'check': check_func
        })
    
    def check_invariants(self) -> List[Dict]:
        """Check all invariants on the current state."""
        violations = []
        for invariant in self.invariants:
            is_valid = invariant['check'](self.state)
            if not is_valid:
                violations.append({
                    'invariant': invariant['name'],
                    'state': self.state.copy()
                })
        self.violations.extend(violations)
        return violations

# Define invariants
def total_supply_invariant(state):
    """Total supply should never exceed max supply."""
    total = state.get('total_supply', 0)
    max_supply = state.get('max_supply', 1000000)
    return total <= max_supply

def balance_non_negative(state):
    """All balances should be non-negative."""
    for key, value in state.items():
        if key.startswith('balance_') and value < 0:
            return False
    return True

# Simulate invariant checking
checker = InvariantChecker()

# Add invariants
checker.add_invariant('Total Supply ≤ Max Supply', total_supply_invariant)
checker.add_invariant('Balances ≥ 0', balance_non_negative)

print("Invariant Checking Simulation:")

# Test with valid state
print("\nValid State:")
checker.set_state('total_supply', 500000)
checker.set_state('max_supply', 1000000)
checker.set_state('balance_alice', 100)
checker.set_state('balance_bob', 200)
violations = checker.check_invariants()
print(f"  Violations: {len(violations)}")

# Test with invalid state
print("\nInvalid State:")
checker.set_state('total_supply', 2000000)  # Exceeds max
checker.set_state('balance_alice', -50)     # Negative balance
violations = checker.check_invariants()
print(f"  Violations: {len(violations)}")
for v in violations:
    print(f"  ❌ {v['invariant']} violated")
    print(f"     State: {v['state']}")

# ----------------------------------------------------------------
# PART C: SECURITY DEVELOPMENT CHECKLIST
# -----------------------------------------------------------------

print("\n" + "-"*60)
print("PART C: Secure Development Checklist")
print("-"*60)

security_checklist = {
    "Design Phase": [
        "Threat model documented",
        "Security requirements defined",
        "Attack surface minimised",
        "Upgradeability strategy defined",
        "Emergency response plan prepared"
    ],
    "Implementation Phase": [
        "Use latest Solidity version",
        "Use audited libraries (OpenZeppelin)",
        "Follow Checks-Effects-Interactions pattern",
        "Proper access control implemented",
        "Events emitted for all state changes"
    ],
    "Testing Phase": [
        "Unit tests written and passing",
        "Integration tests performed",
        "Fuzzing conducted",
        "Formal verification considered",
        "Gas usage optimised"
    ],
    "Audit Phase": [
        "Internal security review conducted",
        "External audit commissioned",
        "Findings addressed",
        "Bug bounty program considered"
    ],
    "Deployment Phase": [
        "Testnet deployment successful",
        "Mainnet deployment planned",
        "Monitoring and alerting configured",
        "Incident response ready"
    ]
}

for phase, items in security_checklist.items():
    print(f"\n{phase.upper()}:")
    for item in items:
        print(f"  □ {item}")

# ----------------------------------------------------------------
# PART D: SUMMARY AND RECOMMENDATIONS
# -----------------------------------------------------------------

print("\n" + "="*70)
print("PART D: Summary and Recommendations")
print("="*70)

print("""
Formal Verification and Secure Development – Key Takeaways:

1. Formal verification uses mathematical proofs to ensure correctness.
2. Approaches: theorem proving, model checking, symbolic execution, property-based testing.
3. Properties: invariants, pre/post-conditions, safety/liveness properties.
4. Tools: Certora, Scribble, Echidna, Mythril, Slither, Foundry.
5. Secure development lifecycle: requirements → design → implementation → testing → deployment.
6. Threat modeling: identify assets, threats, vulnerabilities, risks, and mitigations.

Recommendations:
  - Use formal verification for high-value contracts.
  - Implement property-based testing and fuzzing.
  - Follow secure coding practices.
  - Conduct multiple audits.
  - Monitor contracts in production.
  - Have an incident response plan.
  - Continuously improve security processes.
""")