• 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
Name
Last commit
Last update
..
interfaces Loading commit data...
utils Loading commit data...
L1CrossDomainMessenger.k.sol Loading commit data...
L1ERC721Bridge.k.sol Loading commit data...
L1StandardBridge.k.sol Loading commit data...
OptimismPortal.k.sol Loading commit data...