Leo leonardoalt
leonardoalt
/ mutex_sat.smt2
Created
August 12, 2021 11:54
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (set-logic HORN) | |
| (declare-fun |interface_0_I_4_0| (Int ) Bool) | |
| (declare-fun |nondet_interface_1_I_4_0| (Int Int ) Bool) | |
| (declare-fun |summary_constructor_2_I_4_0| (Int Int ) Bool) | |
| (assert | |
| (forall ( (error_0 Int) (this_0 Int)) | |
| (=> (= error_0 0) (nondet_interface_1_I_4_0 error_0 this_0)))) | |
leonardoalt
/ simple_unsat.smt2
Created
August 12, 2021 11:53
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (set-logic HORN) | |
| (declare-fun |interface_0_C_13_0| (Int ) Bool) | |
| (declare-fun |nondet_interface_1_C_13_0| (Int Int ) Bool) | |
| (declare-fun |summary_constructor_2_C_13_0| (Int Int ) Bool) | |
| (assert | |
| (forall ( (error_0 Int) (this_0 Int)) | |
| (=> (= error_0 0) (nondet_interface_1_C_13_0 error_0 this_0)))) | |
leonardoalt
/ simple_sat.smt2
Created
August 12, 2021 11:53
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (set-logic HORN) | |
| (declare-fun |interface_0_C_13_0| (Int ) Bool) | |
| (declare-fun |nondet_interface_1_C_13_0| (Int Int ) Bool) | |
| (declare-fun |summary_constructor_2_C_13_0| (Int Int ) Bool) | |
| (assert | |
| (forall ( (error_0 Int) (this_0 Int)) | |
| (=> (= error_0 0) (nondet_interface_1_C_13_0 error_0 this_0)))) | |
leonardoalt
/ soundness_sat.smt2
Created
July 19, 2021 12:37
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (set-logic HORN) | |
| (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.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-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| 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 ((|abi_type| 0)) (((|abi_type|)))) | |
| (declare-datatypes ((|mapping(address |
leonardoalt
/ soundness_unsat.smt2
Created
July 19, 2021 12:37
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (set-logic HORN) | |
| (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.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-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| 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 ((|abi_type| 0)) (((|abi_type|)))) | |
| (declare-datatypes ((|mapping(address |
leonardoalt
/ soundness.smt2
Created
July 19, 2021 11:49
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (set-logic HORN) | |
| (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.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-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| 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 ((|abi_type| 0)) (((|abi_type|)))) | |
| (declare-datatypes ((|mapping(address |
leonardoalt
/ verifier.sol
Created
July 15, 2021 19:34
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| // SPDX-License-Identifier: LGPL-3.0-only | |
| // This file is LGPL3 Licensed | |
| //pragma solidity ^0.8.0; | |
| pragma abicoder v1; | |
| library UnsafeMath { | |
| function add(uint a, uint b) internal pure returns (uint c) { | |
| unchecked { c = a + b; } | |
| } |
leonardoalt
/ asm_080
Created
July 15, 2021 19:02
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| .code | |
| PUSH 80 contract Verifier {\n using... | |
| PUSH 40 contract Verifier {\n using... | |
| MSTORE contract Verifier {\n using... | |
| CALLVALUE contract Verifier {\n using... | |
| DUP1 contract Verifier {\n using... | |
| ISZERO contract Verifier {\n using... | |
| PUSH [tag] 1 contract Verifier {\n using... | |
| JUMPI contract Verifier {\n using... | |
| PUSH 0 contract Verifier {\n using... |
leonardoalt
/ asm_076
Created
July 15, 2021 19:02
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| .code | |
| PUSH 80 contract Verifier {\n using... | |
| PUSH 40 contract Verifier {\n using... | |
| MSTORE contract Verifier {\n using... | |
| CALLVALUE contract Verifier {\n using... | |
| DUP1 contract Verifier {\n using... | |
| ISZERO contract Verifier {\n using... | |
| PUSH [tag] 1 contract Verifier {\n using... | |
| JUMPI contract Verifier {\n using... | |
| PUSH 0 contract Verifier {\n using... |
leonardoalt
/ out1.smt2
Created
July 8, 2021 09:20
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (set-logic HORN) | |
| (declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) | |
| (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.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-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| 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 ((|abi_type| 0)) (((|abi_type|)))) | |
| (declare-datatypes ((|struct MultiSig |