Skip to content

Instantly share code, notes, and snippets.

View leonardoalt's full-sized avatar

Leo leonardoalt

591 followers · 0 following
View GitHub Profile
@leonardoalt
leonardoalt / erc777.sol
Created January 15, 2021 17:46
//SPDX-License-Identifier: GPL-v3
pragma solidity ^0.8.0;
pragma experimental SMTChecker;
interface IERC777Recipient {
function tokensReceived(
address from,
address to,
uint256 amount
) external;
@leonardoalt
leonardoalt / multisig.sol
Created January 15, 2021 17:43
//SPDX-License-Identifier: GPL-v3
pragma solidity ^0.8.0;
pragma experimental SMTChecker;
contract Multisig {
enum State { PENDING, APPROVED, EXECUTED }
struct Entry {
State state;
address payable to;
uint amount;
@leonardoalt
leonardoalt / loop.smt2
Created January 4, 2021 16:13
(set-logic HORN)
(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
(declare-fun |interface_C_40_0| (Int
@leonardoalt
leonardoalt / spacer_trace_rlimit_exceeded.txt
Created October 16, 2020 14:14
** expand-pob: query!0 level: 0 depth: 0 exprID: 1 pobID: none
true
** add-lemma: 0 exprID: 2 pobID: 1
query!0
false
* LEVEL 1
@leonardoalt
leonardoalt / spacer_trace_unsat.txt
Created October 16, 2020 14:13
** expand-pob: query!0 level: 0 depth: 0 exprID: 1 pobID: none
true
** add-lemma: 0 exprID: 2 pobID: 1
query!0
false
* LEVEL 1
@leonardoalt
leonardoalt / segfault2.smt2
Created September 29, 2020 18:26
(declare-datatypes ((bytes_tuple 0)) (((bytes_tuple (bytes_tuple_accessor_array (Array Int Int)) (bytes_tuple_accessor_length Int)))))
(declare-datatypes ((tx_type 0)) (((tx_type (block.coinbase Int) (block.difficulty Int) (block.gaslimit Int) (block.number Int) (block.timestamp Int) (blockhash (Array Int Int)) (msg.data bytes_tuple) (msg.sender Int) (msg.sig Int) (msg.value Int) (tx.gasprice Int) (tx.origin Int)))))
(declare-datatypes ((state_type 0)) (((state_type (balances (Array Int Int))))))
(declare-rel block_7_f_56_66_0 (Int Int tx_type state_type Bool Int Int Bool state_type Bool Int Int Bool Int))
(declare-rel implicit_constructor_C_66_0 (Int Int tx_type state_type))
(declare-rel interface_D_6_0 (Int state_type))
(declare-rel summary_constructor_D_6_0 (Int Int tx_type state_type))
(declare-rel summary_constructor_C_66_0 (Int Int tx_type state_type Bool Int Int))
(declare-rel nondet_interface_C_66_0 (state_type Bool Int Int state_type Bool Int Int))
(declare-rel summary_2_function_f__57_66_0 (Int Int
@leonardoalt
leonardoalt / segfault.smt2
Created September 17, 2020 17:04
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
(declare-datatypes ((|struct C.T| 0)) (((|struct C.T| (|struct C.T_accessor_y| Int) (|struct C.T_accessor_a| |uint[]_tuple|)))))
(declare-datatypes ((|struct C.T[]_tuple| 0)) (((|struct C.T[]_tuple| (|struct C.T[]_tuple_accessor_array| (Array Int |struct C.T|)) (|struct C.T[]_tuple_accessor_length| Int)))))
(declare-datatypes ((|struct C.S| 0)) (((|struct C.S| (|struct C.S_accessor_x| Int) (|struct C.S_accessor_t| |struct C.T|) (|struct C.S_accessor_a| |uint[]_tuple|) (|struct C.S_accessor_ts| |struct C.T[]_tuple|)))))
(declare-datatypes ((|struct C.S[]_tuple| 0)) (((|struct C.S[]_tuple| (|struct C.S[]_tuple_accessor_array| (Array Int |struct C.S|)) (|struct C.S[]_tuple_accessor_length| Int)))))
(declare-datatypes ((state_type 0)) (((state_type (balances (Array Int Int))))))
(declare-rel nondet_interface_C_154_0 (state_type state_type))
(declare-rel error_target_10
@leonardoalt
leonardoalt / segfault.smt2
Created September 17, 2020 16:41
(declare-datatypes ((struct C.T[]_tuple 0)) (((|struct C.T[]_tuple| (|struct C.T[]_tuple_accessor_array| (Array Int |struct C.T|)) (|struct C.T[]_tuple_accessor_length| Int)))))
(declare-datatypes ((uint[]_tuple 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
(declare-datatypes ((struct C.T 0)) (((|struct C.T| (|struct C.T_accessor_y| Int) (|struct C.T_accessor_a| |uint[]_tuple|)))))
(declare-datatypes ((struct C.S 0)) (((|struct C.S| (|struct C.S_accessor_x| Int) (|struct C.S_accessor_t| |struct C.T|) (|struct C.S_accessor_a| |uint[]_tuple|) (|struct C.S_accessor_ts| |struct C.T[]_tuple|)))))
(declare-datatypes ((struct C.S[]_tuple 0)) (((|struct C.S[]_tuple| (|struct C.S[]_tuple_accessor_array| (Array Int |struct C.S|)) (|struct C.S[]_tuple_accessor_length| Int)))))
(declare-datatypes ((state_type 0)) (((state_type (balances (Array Int Int))))))
(declare-rel nondet_interface_C_154_0 (state_type state_type))
(declare-rel error_target_10_0 ())
(de
@leonardoalt
leonardoalt / deposit_loop_mod_32.smt2
Created September 16, 2020 13:14
(declare-rel beforeLoop ())
(declare-rel loopCond (Int Int))
(declare-rel loopBody (Int Int))
(declare-rel afterLoop ())
(declare-rel endFunction ())
(declare-var size Int)
(declare-var height Int)
(rule beforeLoop)
@leonardoalt
leonardoalt / deposit.smt2
Created September 15, 2020 15:09
(declare-rel beforeLoop ())
(declare-rel loopCond (Int Int))
(declare-rel loopBody (Int Int))
(declare-rel afterLoop ())
(declare-rel endFunction ())
(declare-var size Int)
(declare-var height Int)
(rule beforeLoop)