multisig.sol

//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;
		uint id;
		uint approved;
	}

	Entry[] txs;
	mapping (address =>  bool) owners;
	mapping (address => mapping (uint => bool)) approved;
	uint immutable required;
	
	constructor(address[] memory _owners, uint _required) {
		require(_owners.length >= _required);
		required = _required;
		for (uint i = 0; i < _owners.length; ++i)
			owners[_owners[i]] = true;
	}

	function add(address payable _to, uint _amount) public {
		require(owners[msg.sender]);
		uint id = txs.length;
		txs.push(Entry(State.PENDING, _to, _amount, id, 1));
		approved[msg.sender][id] = true;
	}

	function approve(uint _id) public {
		require(_id < txs.length);
		require(txs[_id].state != State.EXECUTED);
		require(owners[msg.sender]);
		require(!approved[msg.sender][_id]);
		uint approvedOwners = txs[_id].approved + 1;
		if (approvedOwners >= required)
			txs[_id].state = State.APPROVED;
		txs[_id].approved = approvedOwners;
	}

	function execute(uint _id) public {
		require(_id < txs.length);
		require(txs[_id].state == State.APPROVED);
		assert(txs[_id].approved >= required);
		_execute(_id);
		txs[_id].state = State.EXECUTED;
	}

	function _execute(uint) internal {}
}