• Juan C's avatar
    Add Kontrol proofs for `L1StandardBridgeKontrol` and `L1ERC721BridgeKontrol` (#9183) · 640b4cb7
    Juan C authored
    * OptimismPortal.k.sol: directly feed `WithdrawalTransaction` argument
    
    * KontrolInterfaces: add interfaces for bridges
    
    * KontrolDeployment: add deployment for L1 bridges
    
    * run-kontrol.sh: add bridge proofs
    
    * Update summaries
    
    * Add `L1StandardBridge` proofs
    
    * Add `L1ERC721Bridge` proof
    
    * KontrolDeployment: remove typo import
    
    * `kontrol-tests`: add remaining files to `check-changed`
    
    * Fix spelling typo
    
    * Document current `vm.mockCall` workaround
    
    * Document symbolic bytes assumptions
    
    * Supress upper case legacy naming
    
    * Add summarization tests for `L1ERC721Bridge`
    
    * Add summarization tests for `L1StandardBridge`
    
    * run-kontrol.sh: set `workers` to `min(max_workers, #test_list)`
    
    * README.md: add bridge proofs
    
    * make `xDomainMessageSender` part of `IL1CrossDomainMessenger`
    
    * Missed instances of `ICrossDomainMessenger`
    
    * Document `vm.prank()` issue
    
    * Improve assumption documentation
    
    * run-kontrol.sh: improve style
    
    * `kontrol-tests`: add remaining files to `check-changed`
    
    * run-kontrol.sh: document `max_workers=7`
    640b4cb7
KontrolInterfaces.sol 2.14 KB