leonardoalt

//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

//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

contract A {
	uint x;
	function f() internal virtual {
		v();
		assert(x == 0); // should fail
		assert(x == 2); // should hold
	}
	function v() internal virtual {
		x = 0;
	}

leonardoalt

(set-logic HORN)

(declare-fun loopInvStart (Int Int Int Int) Bool)
(declare-fun loopHeader (Int Int Int Int) Bool)
(declare-fun loopBody (Int Int Int Int) Bool)
(declare-fun loopInvBlock1 (Int Int Int Int) Bool)
(declare-fun summaryLoopInv (Int Int Int Int) Bool)

(assert
(forall ( (nInit Int) (xInit Int) (nCur Int) (xCur Int) )

leonardoalt

I contributed to the ZKOPRU Trusted Setup Multi-Party Ceremony.
The following are my contribution signatures:
Circuit: zk_transaction_1_2 
          Contributor # 153
          Hash: 9013e7f4 d68711db 32b0d504 9960dd8d
 19d938cf a516fb3c a6b95fac 3a83054f
 fe52c389 5f301522 111e542f 6f32354e
 da9db310 1ec95c55 10c79c09 15f177f0

leonardoalt

(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-fun |interface_0_C_13_0| (In

leonardoalt

(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 ((|uint_array_tuple| 0)) (((|uint_array_tuple| (|uint_array_tuple_access

leonardoalt

;;------------- State definition ---------
(declare-datatypes () ((State (mkState (error Bool) (running Bool) (stack (Array Int Int)) (len Int) ))))

;;------------- Opcode declarations ------------

(declare-rel evmPush (State Int State))
(declare-rel evmAdd (State State))
(declare-rel evmStop (State State))

;;------------- Helper vars --------------

leonardoalt

(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 ((|t_function_abiencodepacked_pure()returns(t_bytes_memory_ptr)_t_bytes3

leonardoalt

// SPDX-License-Identifier: LGPL-3.0-only
// This file is LGPL3 Licensed
pragma solidity ^0.8.0;

/**
 * @title Elliptic curve operations on twist points for alt_bn128
 * @author Mustafa Al-Bassam ([email protected])
 * @dev Homepage: https://github.com/musalbas/solidity-BN256G2
 */