From e3bfaed87b9c9f48b0df74b68d4b753548907331 Mon Sep 17 00:00:00 2001 From: Wayne Nilsen Date: Mon, 22 Mar 2021 11:18:42 -0400 Subject: [PATCH 1/3] CLI Configuration (#264) * also patch ETH_KEY_ID situation * update integration tests to use CLI configuration --- gateway-crypto/src/dev.rs | 12 ++- gateway-crypto/src/std.rs | 6 ++ integration/util/scenario/validator.js | 8 +- node/src/cli.rs | 22 ++++ node/src/command.rs | 11 +- pallets/cash/src/events.rs | 1 - pallets/cash/src/internal/notices.rs | 10 -- pallets/cash/src/internal/validate_trx.rs | 8 -- pallets/cash/src/tests/mod.rs | 1 - pallets/oracle/src/tests/mod.rs | 1 - pallets/runtime-interfaces/src/lib.rs | 118 ++++++++++++++++------ 11 files changed, 138 insertions(+), 60 deletions(-) diff --git a/gateway-crypto/src/dev.rs b/gateway-crypto/src/dev.rs index c80799728..d1738079e 100644 --- a/gateway-crypto/src/dev.rs +++ b/gateway-crypto/src/dev.rs @@ -25,6 +25,8 @@ fn get_eth_private_key_from_environment_variable() -> Result Result InMemoryKeyring { let mut keyring = InMemoryKeyring::new(); - let eth_key_id: KeyId = ETH_KEY_ID_ENV_VAR_DEV_DEFAULT.into(); + let eth_key_id: KeyId = if let Ok(eth_key_id_from_env) = std::env::var(ETH_KEY_ID_ENV_VAR) { + if eth_key_id_from_env.len() > 0 { + KeyId::from(eth_key_id_from_env) + } else { + ETH_KEY_ID_ENV_VAR_DEV_DEFAULT.into() + } + } else { + ETH_KEY_ID_ENV_VAR_DEV_DEFAULT.into() + }; let pair = match get_eth_private_key_from_environment_variable() { Ok(pair) => pair, diff --git a/gateway-crypto/src/std.rs b/gateway-crypto/src/std.rs index 176d2ebdc..3f78b09b3 100644 --- a/gateway-crypto/src/std.rs +++ b/gateway-crypto/src/std.rs @@ -31,6 +31,12 @@ impl From<&str> for KeyId { } } +impl From for KeyId { + fn from(source: String) -> Self { + KeyId { data: source } + } +} + impl Into for KeyId { fn into(self) -> String { self.data diff --git a/integration/util/scenario/validator.js b/integration/util/scenario/validator.js index 33ce62edb..8a028014f 100644 --- a/integration/util/scenario/validator.js +++ b/integration/util/scenario/validator.js @@ -132,11 +132,7 @@ class Validator { let env = { ...this.spawnOpts, - ETH_RPC_URL: this.ctx.eth.web3Url, ETH_KEY: this.ethPrivateKey, - ETH_KEY_ID: "my_eth_key_id", - MINER: `Eth:${this.ethAccount}`, - OPF_URL: this.ctx.__opfUrl() }; let versioning = []; @@ -166,6 +162,10 @@ class Validator { '--no-mdns', '--node-key', this.nodeKey, + '--eth-rpc-url', this.ctx.eth.web3Url, + '--eth-key-id', "my_eth_key_id", + '--miner', `Eth:${this.ethAccount}`, + '--opf-url', this.ctx.__opfUrl(), '-lruntime=debug', '--reserved-only', ...versioning, diff --git a/node/src/cli.rs b/node/src/cli.rs index 63da9cc59..bc748b735 100644 --- a/node/src/cli.rs +++ b/node/src/cli.rs @@ -1,6 +1,25 @@ use sc_cli::RunCmd; use structopt::StructOpt; +#[derive(Debug, StructOpt)] +pub struct GatewayCmd { + /// Set the ETH Key ID for AWS KMS integration + #[structopt(long = "eth-key-id")] + pub eth_key_id: Option, + + /// Set the ETH RPC Url for interfacing with ethereum + #[structopt(long = "eth-rpc-url")] + pub eth_rpc_url: Option, + + /// Set the miner address (only useful for validator) + #[structopt(long = "miner")] + pub miner: Option, + + /// Open price feed URL + #[structopt(long = "opf-url")] + pub opf_url: Option, +} + #[derive(Debug, StructOpt)] pub struct Cli { #[structopt(subcommand)] @@ -8,6 +27,9 @@ pub struct Cli { #[structopt(flatten)] pub run: RunCmd, + + #[structopt(flatten)] + pub gateway: GatewayCmd, } #[derive(Debug, StructOpt)] diff --git a/node/src/command.rs b/node/src/command.rs index c059b6993..7d27d803c 100644 --- a/node/src/command.rs +++ b/node/src/command.rs @@ -31,11 +31,6 @@ impl SubstrateCli for Cli { } fn load_spec(&self, id: &str) -> Result, String> { - if id == "dev" { - // check for our required environment variables and set them to the defaults if necessary - runtime_interfaces::set_validator_config_dev_defaults(); - } - Ok(match id { "dev" => Box::new(chain_spec::development_config()), "" | "local" | "testnet" => Box::new(chain_spec::local_testnet_config()), @@ -138,6 +133,12 @@ pub fn run() -> sc_cli::Result<()> { } None => { let runner = cli.create_runner(&cli.run)?; + runtime_interfaces::initialize_validator_config( + cli.gateway.eth_key_id.clone(), + cli.gateway.eth_rpc_url.clone(), + cli.gateway.miner.clone(), + cli.gateway.opf_url.clone(), + ); Ok(runner.run_node_until_exit(|config| async move { match config.role { Role::Light => service::new_light(config), diff --git a/pallets/cash/src/events.rs b/pallets/cash/src/events.rs index dced8d87a..1028cb0b4 100644 --- a/pallets/cash/src/events.rs +++ b/pallets/cash/src/events.rs @@ -138,7 +138,6 @@ pub mod tests { "0xbbde1662bC3ED16aA8C618c9833c801F3543B587".into(); let config = runtime_interfaces::new_config(given_eth_starport_address.clone()); runtime_interfaces::config_interface::set(config); - runtime_interfaces::set_validator_config_dev_defaults(); let given_eth_rpc_url = runtime_interfaces::validator_config_interface::get_eth_rpc_url().unwrap(); diff --git a/pallets/cash/src/internal/notices.rs b/pallets/cash/src/internal/notices.rs index be9f67ef1..5faa5667b 100644 --- a/pallets/cash/src/internal/notices.rs +++ b/pallets/cash/src/internal/notices.rs @@ -470,7 +470,6 @@ mod tests { #[test] fn test_process_notice_state_missing_notice() { new_test_ext().execute_with(|| { - runtime_interfaces::set_validator_config_dev_defaults(); let chain_id = ChainId::Eth; let notice_id = NoticeId(5, 6); let notice = Notice::ExtractionNotice(ExtractionNotice::Eth { @@ -492,7 +491,6 @@ mod tests { #[test] fn test_process_notice_state_non_pending() { new_test_ext().execute_with(|| { - runtime_interfaces::set_validator_config_dev_defaults(); let chain_id = ChainId::Eth; let notice_id = NoticeId(5, 6); let notice_state = NoticeState::Executed {}; @@ -507,7 +505,6 @@ mod tests { #[test] fn test_process_notice_state_already_signed() { new_test_ext().execute_with(|| { - runtime_interfaces::set_validator_config_dev_defaults(); let chain_id = ChainId::Eth; let notice_id = NoticeId(5, 6); let signer = ::signer_address().unwrap(); @@ -525,7 +522,6 @@ mod tests { #[test] fn test_process_notice_state_valid() { new_test_ext().execute_with(|| { - runtime_interfaces::set_validator_config_dev_defaults(); let chain_id = ChainId::Eth; let notice_id = NoticeId(5, 6); let notice = Notice::ExtractionNotice(ExtractionNotice::Eth { @@ -550,7 +546,6 @@ mod tests { #[test] fn test_process_notices() { new_test_ext().execute_with(|| { - runtime_interfaces::set_validator_config_dev_defaults(); let chain_id = ChainId::Eth; let notice_id_1 = NoticeId(5, 6); let notice_1 = Notice::ExtractionNotice(ExtractionNotice::Eth { @@ -616,7 +611,6 @@ mod tests { #[test] fn test_publish_signature_pending_valid() { new_test_ext().execute_with(|| { - runtime_interfaces::set_validator_config_dev_defaults(); let chain_id = ChainId::Eth; let notice_id = NoticeId(5, 6); let notice = Notice::ExtractionNotice(ExtractionNotice::Eth { @@ -685,7 +679,6 @@ mod tests { #[test] fn test_publish_signature_pending_already_signed() { new_test_ext().execute_with(|| { - runtime_interfaces::set_validator_config_dev_defaults(); let chain_id = ChainId::Eth; let notice_id = NoticeId(5, 6); let notice = Notice::ExtractionNotice(ExtractionNotice::Eth { @@ -714,7 +707,6 @@ mod tests { #[test] fn test_publish_signature_signature_mismatch() { new_test_ext().execute_with(|| { - runtime_interfaces::set_validator_config_dev_defaults(); let chain_id = ChainId::Eth; let notice_id = NoticeId(5, 6); let notice = Notice::ExtractionNotice(ExtractionNotice::Eth { @@ -746,7 +738,6 @@ mod tests { #[test] fn test_publish_signature_pending_unknown_validator() { new_test_ext().execute_with(|| { - runtime_interfaces::set_validator_config_dev_defaults(); let chain_id = ChainId::Eth; let notice_id = NoticeId(5, 6); let notice = Notice::ExtractionNotice(ExtractionNotice::Eth { @@ -773,7 +764,6 @@ mod tests { #[test] fn test_publish_signature_pending_invalid_signature() { new_test_ext().execute_with(|| { - runtime_interfaces::set_validator_config_dev_defaults(); let chain_id = ChainId::Eth; let notice_id = NoticeId(5, 6); let notice = Notice::ExtractionNotice(ExtractionNotice::Eth { diff --git a/pallets/cash/src/internal/validate_trx.rs b/pallets/cash/src/internal/validate_trx.rs index 06f43f1e4..3897ee69a 100644 --- a/pallets/cash/src/internal/validate_trx.rs +++ b/pallets/cash/src/internal/validate_trx.rs @@ -249,8 +249,6 @@ mod tests { #[test] fn test_receive_event_not_a_validator() { new_test_ext().execute_with(|| { - runtime_interfaces::set_validator_config_dev_defaults(); - let event_id: ChainLogId = ChainLogId::Eth(1, 1); let event: ChainLogEvent = ChainLogEvent::Eth(EthereumLogEvent { block_hash: [0u8; 32], @@ -283,7 +281,6 @@ mod tests { #[test] fn test_receive_event_is_validator() { new_test_ext().execute_with(|| { - runtime_interfaces::set_validator_config_dev_defaults(); let substrate_id = AccountId32::new([0u8; 32]); let eth_address = ::signer_address().unwrap(); Validators::insert( @@ -332,7 +329,6 @@ mod tests { #[test] fn test_exec_trx_request_nonce_zero() { new_test_ext().execute_with(|| { - runtime_interfaces::set_validator_config_dev_defaults(); let request: Vec = String::from("Hello").as_bytes().into(); let nonce = 0; let full_request: Vec = format!("\x19Ethereum Signed Message:\n70:Hello") @@ -366,7 +362,6 @@ mod tests { #[test] fn test_exec_trx_request_nonce_nonzero() { new_test_ext().execute_with(|| { - runtime_interfaces::set_validator_config_dev_defaults(); let request: Vec = String::from("Hello").as_bytes().into(); let nonce = 5; let full_request: Vec = format!("\x19Ethereum Signed Message:\n75:Hello") @@ -400,7 +395,6 @@ mod tests { #[test] fn test_publish_signature_invalid_signature() { new_test_ext().execute_with(|| { - runtime_interfaces::set_validator_config_dev_defaults(); let chain_id = ChainId::Eth; let notice_id = NoticeId(5, 6); let notice = Notice::ExtractionNotice(ExtractionNotice::Eth { @@ -438,7 +432,6 @@ mod tests { #[test] fn test_publish_signature_invalid_validator() { new_test_ext().execute_with(|| { - runtime_interfaces::set_validator_config_dev_defaults(); let chain_id = ChainId::Eth; let notice_id = NoticeId(5, 6); let notice = Notice::ExtractionNotice(ExtractionNotice::Eth { @@ -473,7 +466,6 @@ mod tests { #[test] fn test_publish_signature_valid() { new_test_ext().execute_with(|| { - runtime_interfaces::set_validator_config_dev_defaults(); let chain_id = ChainId::Eth; let notice_id = NoticeId(5, 6); let notice = Notice::ExtractionNotice(ExtractionNotice::Eth { diff --git a/pallets/cash/src/tests/mod.rs b/pallets/cash/src/tests/mod.rs index 48adeb014..8c810e261 100644 --- a/pallets/cash/src/tests/mod.rs +++ b/pallets/cash/src/tests/mod.rs @@ -72,7 +72,6 @@ macro_rules! qty { } pub fn initialize_storage() { - runtime_interfaces::set_validator_config_dev_defaults(); CashModule::initialize_assets(vec![ AssetInfo { liquidity_factor: FromStr::from_str("7890").unwrap(), diff --git a/pallets/oracle/src/tests/mod.rs b/pallets/oracle/src/tests/mod.rs index 65f3c9316..f2eeb9b9a 100644 --- a/pallets/oracle/src/tests/mod.rs +++ b/pallets/oracle/src/tests/mod.rs @@ -11,7 +11,6 @@ pub use mock::*; pub const ETH_TICKER: Ticker = Ticker::new("ETH"); pub fn initialize_storage() { - runtime_interfaces::set_validator_config_dev_defaults(); OracleModule::initialize_reporters( vec![ "0x85615b076615317c80f14cbad6501eec031cd51c", diff --git a/pallets/runtime-interfaces/src/lib.rs b/pallets/runtime-interfaces/src/lib.rs index e2904c91f..2f540564f 100644 --- a/pallets/runtime-interfaces/src/lib.rs +++ b/pallets/runtime-interfaces/src/lib.rs @@ -11,6 +11,14 @@ pub struct Config { eth_starport_address: Vec, } +#[derive(Clone)] +pub struct ValidatorConfig { + eth_key_id: String, + eth_rpc_url: String, + miner: String, + opf_url: String, +} + /// XXX Possible sanity checks for config fields here impl Config { pub fn update(&mut self, new: Config) { @@ -32,9 +40,29 @@ type PriceFeedData = (Vec<(Vec, Vec)>, u64); lazy_static! { static ref CONFIG: Mutex = Mutex::new(new_config("".into())); + static ref VALIDATOR_CONFIG: Mutex> = Mutex::new(None); static ref PRICE_FEED_DATA: Mutex> = Mutex::new(None); } +pub fn initialize_validator_config( + eth_key_id: Option, + eth_rpc_url: Option, + miner: Option, + opf_url: Option, +) { + match VALIDATOR_CONFIG.lock() { + Ok(mut data_ref) => { + *data_ref = Some(ValidatorConfig { + eth_key_id: eth_key_id.unwrap_or(ETH_KEY_ID_DEFAULT.to_owned()), + eth_rpc_url: eth_rpc_url.unwrap_or(ETH_RPC_URL_DEFAULT.to_owned()), + miner: miner.unwrap_or(MINER_DEFAULT.to_owned()), + opf_url: opf_url.unwrap_or(OPF_URL_DEFAULT.to_owned()), + }); + } + _ => (), // XXX todo: log? + }; +} + /// The configuration interface for offchain workers. This is designed to manage configuration /// that is specific to gateway AND distributed in the chain spec file. Ultimately /// the things that are being configured here should not be changed by any honest validators. @@ -58,12 +86,14 @@ pub trait ConfigInterface { } const ETH_KEY_ID_ENV_VAR: &str = "ETH_KEY_ID"; -const ETH_KEY_ID_ENV_VAR_DEV_DEFAULT: &str = gateway_crypto::ETH_KEY_ID_ENV_VAR_DEV_DEFAULT; const ETH_RPC_URL_ENV_VAR: &str = "ETH_RPC_URL"; const MINER_ENV_VAR: &str = "MINER"; -const ETH_RPC_URL_ENV_VAR_DEV_DEFAULT: &str = "https://goerli-eth.compound.finance"; const OPF_URL_ENV_VAR: &str = "OPF_URL"; -const OPF_URL_ENV_VAR_DEFAULT: &str = "https://prices.compound.finance/coinbase"; + +const ETH_KEY_ID_DEFAULT: &str = gateway_crypto::ETH_KEY_ID_ENV_VAR_DEV_DEFAULT; +const MINER_DEFAULT: &str = "Eth:0x0000000000000000000000000000000000000000"; +const ETH_RPC_URL_DEFAULT: &str = "https://ropsten-eth.compound.finance"; +const OPF_URL_DEFAULT: &str = "https://prices.compound.finance/coinbase"; /// The ValidatorConfigInterface is designed to be modified as needed by the validators. This means /// that each validator should be modifying the values here. For example, the ETH_KEY_ID is set @@ -82,22 +112,74 @@ pub trait ValidatorConfigInterface { /// Downstream this is used to feed the keyring for signing and obtaining the corresponding /// public key. fn get_eth_key_id() -> Option> { - std::env::var(ETH_KEY_ID_ENV_VAR).ok().map(Into::into) + // check env override + if let Ok(eth_key_id_from_env) = std::env::var(ETH_KEY_ID_ENV_VAR) { + if eth_key_id_from_env.len() > 0 { + return Some(eth_key_id_from_env.into()); + } + } + // check config + if let Ok(config) = VALIDATOR_CONFIG.lock() { + if let Some(inner) = config.as_ref() { + return Some(inner.eth_key_id.clone().into()); + } + } + // not set + return Some(ETH_KEY_ID_DEFAULT.into()); } /// Get the Ethereum node RPC URL fn get_eth_rpc_url() -> Option> { - std::env::var(ETH_RPC_URL_ENV_VAR).ok().map(Into::into) + // check env override + if let Ok(eth_rpc_url) = std::env::var(ETH_RPC_URL_ENV_VAR) { + if eth_rpc_url.len() > 0 { + return Some(eth_rpc_url.into()); + } + } + // check config + if let Ok(config) = VALIDATOR_CONFIG.lock() { + if let Some(inner) = config.as_ref() { + return Some(inner.eth_rpc_url.clone().into()); + } + } + // not set + return Some(ETH_RPC_URL_DEFAULT.into()); } /// Get the open price feed URLs fn get_opf_url() -> Option> { - std::env::var(OPF_URL_ENV_VAR).ok().map(Into::into) + // check env override + if let Ok(opf_url) = std::env::var(OPF_URL_ENV_VAR) { + if opf_url.len() > 0 { + return Some(opf_url.into()); + } + } + // check config + if let Ok(config) = VALIDATOR_CONFIG.lock() { + if let Some(inner) = config.as_ref() { + return Some(inner.opf_url.clone().into()); + } + } + // not set + return Some(OPF_URL_DEFAULT.into()); } /// Get the Miner address fn get_miner_address() -> Option> { - std::env::var(MINER_ENV_VAR).ok().map(Into::into) + // check env override + if let Ok(miner) = std::env::var(MINER_ENV_VAR) { + if miner.len() > 0 { + return Some(miner.into()); + } + } + // check config + if let Ok(config) = VALIDATOR_CONFIG.lock() { + if let Some(inner) = config.as_ref() { + return Some(inner.miner.clone().into()); + } + } + // not set + return Some(MINER_DEFAULT.into()); } } @@ -141,28 +223,6 @@ pub trait KeyringInterface { } } -/// Set an environment variable to a value if it is not already set to an existing value. -fn set_validator_config_dev_default(key: &str, value: &str) { - let existing = std::env::var(key); - if existing.is_ok() { - return; - } - - std::env::set_var(key, value); -} - -/// For the local dev environment we want some sane defaults for these configuration values -/// without always having to set up the developer's machine, with, say, a `.env` file -/// or a run shell script. We would like to just stick with `cargo run -- ...`. To that end -/// when the `--dev` flag is passed, these defaults are used but only when an existing environment -/// variable is not already set. -pub fn set_validator_config_dev_defaults() { - set_validator_config_dev_default(ETH_KEY_ID_ENV_VAR, ETH_KEY_ID_ENV_VAR_DEV_DEFAULT); - set_validator_config_dev_default(ETH_RPC_URL_ENV_VAR, ETH_RPC_URL_ENV_VAR_DEV_DEFAULT); - set_validator_config_dev_default(OPF_URL_ENV_VAR, OPF_URL_ENV_VAR_DEFAULT); - set_validator_config_dev_default(MINER_ENV_VAR, ""); -} - #[sp_runtime_interface::runtime_interface] pub trait PriceFeedInterface { fn get_price_data() -> Option { From 43fe0566b180fd5203aefc91bced2dd3d3d4203c Mon Sep 17 00:00:00 2001 From: Jared Flatow Date: Mon, 22 Mar 2021 13:47:02 -0700 Subject: [PATCH 2/3] Some tiny cleanups (#260) --- README.md | 3 +- ethereum-client/src/events.rs | 54 ------------------- ops/tf/main.tf | 6 +-- .../cash/src/internal/change_validators.rs | 2 +- pallets/cash/src/lib.rs | 6 ++- 5 files changed, 10 insertions(+), 61 deletions(-) diff --git a/README.md b/README.md index cb0b46751..42c548c01 100644 --- a/README.md +++ b/README.md @@ -219,4 +219,5 @@ by appending your own. A few useful ones are as follow. ./scripts/docker_run.sh ./target/release/gateway purge-chain --dev # Check whether the code is compilable -./scripts/docker_run.sh cargo +nightly check \ No newline at end of file +./scripts/docker_run.sh cargo +nightly check +``` diff --git a/ethereum-client/src/events.rs b/ethereum-client/src/events.rs index 973076c94..3a0738572 100644 --- a/ethereum-client/src/events.rs +++ b/ethereum-client/src/events.rs @@ -36,33 +36,6 @@ pub enum EthereumEvent { } lazy_static! { - static ref LOCK_OLD_EVENT: ethabi::Event = ethabi::Event { - name: String::from("Lock"), - inputs: vec![ - ethabi::EventParam { - name: String::from("asset"), - kind: ethabi::param_type::ParamType::Address, - indexed: true - }, - ethabi::EventParam { - name: String::from("sender"), - kind: ethabi::param_type::ParamType::Address, - indexed: true - }, - ethabi::EventParam { - name: String::from("recipient"), - kind: ethabi::param_type::ParamType::Address, - indexed: true - }, - ethabi::EventParam { - name: String::from("amount"), - kind: ethabi::param_type::ParamType::Uint(256), - indexed: false - } - ], - anonymous: false - }; - static ref LOCK_OLD_EVENT_TOPIC: ethabi::Hash = LOCK_OLD_EVENT.signature(); static ref LOCK_EVENT: ethabi::Event = ethabi::Event { name: String::from("Lock"), inputs: vec![ @@ -95,33 +68,6 @@ lazy_static! { anonymous: false }; static ref LOCK_EVENT_TOPIC: ethabi::Hash = LOCK_EVENT.signature(); - static ref LOCK_CASH_OLD_EVENT: ethabi::Event = ethabi::Event { - name: String::from("LockCash"), - inputs: vec![ - ethabi::EventParam { - name: String::from("sender"), - kind: ethabi::param_type::ParamType::Address, - indexed: true - }, - ethabi::EventParam { - name: String::from("recipient"), - kind: ethabi::param_type::ParamType::Address, - indexed: true - }, - ethabi::EventParam { - name: String::from("amount"), - kind: ethabi::param_type::ParamType::Uint(256), - indexed: false - }, - ethabi::EventParam { - name: String::from("principal"), - kind: ethabi::param_type::ParamType::Uint(128), - indexed: false - }, - ], - anonymous: false - }; - static ref LOCK_CASH_OLD_EVENT_TOPIC: ethabi::Hash = LOCK_CASH_OLD_EVENT.signature(); static ref LOCK_CASH_EVENT: ethabi::Event = ethabi::Event { name: String::from("LockCash"), inputs: vec![ diff --git a/ops/tf/main.tf b/ops/tf/main.tf index 3459e630f..52b9d2a9d 100644 --- a/ops/tf/main.tf +++ b/ops/tf/main.tf @@ -137,7 +137,7 @@ resource "aws_security_group" "full_node_sg" { protocol = "-1" cidr_blocks = ["0.0.0.0/0"] } - + egress { from_port = 0 to_port = 0 @@ -162,7 +162,7 @@ resource "aws_security_group" "authority_node_sg" { protocol = "-1" cidr_blocks = ["0.0.0.0/0"] } - + egress { from_port = 0 to_port = 0 @@ -193,7 +193,7 @@ resource "aws_security_group" "bastion_node_sg" { protocol = "-1" ipv6_cidr_blocks = ["::/0"] } - + egress { from_port = 0 to_port = 0 diff --git a/pallets/cash/src/internal/change_validators.rs b/pallets/cash/src/internal/change_validators.rs index 9e661c804..45cdc3e6a 100644 --- a/pallets/cash/src/internal/change_validators.rs +++ b/pallets/cash/src/internal/change_validators.rs @@ -10,7 +10,7 @@ pub fn change_validators(validators: Vec) -> Result<() for validator in validators.iter() { require!( - ::SessionInterface::is_valid_keys(validator.substrate_id.clone()), + ::SessionInterface::has_next_keys(validator.substrate_id.clone()), Reason::ChangeValidatorsError ); } diff --git a/pallets/cash/src/lib.rs b/pallets/cash/src/lib.rs index 427903289..51d87df95 100644 --- a/pallets/cash/src/lib.rs +++ b/pallets/cash/src/lib.rs @@ -92,6 +92,8 @@ pub trait Config: /// Placate substrate's `HandleLifetime` trait. type AccountStore: StoredMap; + + /// Associated type which allows us to interact with substrate Sessions. type SessionInterface: self::SessionInterface; } @@ -300,7 +302,7 @@ fn check_failure(res: Result<(), Reason>) -> Result<(), Reason> { } pub trait SessionInterface: frame_system::Config { - fn is_valid_keys(x: AccountId) -> bool; + fn has_next_keys(x: AccountId) -> bool; fn rotate_session(); } @@ -308,7 +310,7 @@ impl SessionInterface for T where T: pallet_session::Config, { - fn is_valid_keys(x: SubstrateId) -> bool { + fn has_next_keys(x: SubstrateId) -> bool { match >::next_keys(x as T::ValidatorId) { Some(_keys) => true, None => false, From 715f76aee71b99fde6b4d67aaaabbb07a0103395 Mon Sep 17 00:00:00 2001 From: Thomas b e e f y b o i Bernardi Date: Tue, 9 Mar 2021 10:41:27 -0800 Subject: [PATCH 3/3] Certora modifications + rules --- certora/contracts/CashToken.sol | 289 ++++++ certora/contracts/CashTokenHarness.sol | 27 + certora/contracts/ICash.sol | 37 + certora/contracts/Starport.sol | 470 +++++++++ certora/contracts/StarportHarness.sol | 152 +++ certora/contracts/StarportHarnessOrdering.sol | 52 + certora/readme.txt | 10 + certora/runCashToken.sh | 5 + certora/runCashTokenHarness.sh | 5 + certora/runPrivileged.sh | 5 + certora/runSanity.sh | 6 + certora/runSanityAssume.sh | 6 + certora/runStarportHarness.sh | 9 + certora/runStarportHarnessOrdering.sh | 9 + certora/spec/CashToken.spec | 653 +++++++++++++ certora/spec/CashTokenHarness.spec | 804 ++++++++++++++++ certora/spec/Privileged.spec | 22 + certora/spec/Starport.spec | 284 ++++++ certora/spec/StarportOrdering.spec | 266 ++++++ certora/spec/erc20.spec | 895 ++++++++++++++++++ certora/spec/harnesses/ERC20.sol | 57 ++ certora/spec/harnesses/ExcessiveERC20.sol | 59 ++ certora/spec/harnesses/NonStandardERC20.sol | 56 ++ certora/spec/sanity.spec | 6 + certora/spec/sanitySound.spec | 9 + 25 files changed, 4193 insertions(+) create mode 100644 certora/contracts/CashToken.sol create mode 100644 certora/contracts/CashTokenHarness.sol create mode 100644 certora/contracts/ICash.sol create mode 100644 certora/contracts/Starport.sol create mode 100644 certora/contracts/StarportHarness.sol create mode 100644 certora/contracts/StarportHarnessOrdering.sol create mode 100644 certora/readme.txt create mode 100755 certora/runCashToken.sh create mode 100755 certora/runCashTokenHarness.sh create mode 100755 certora/runPrivileged.sh create mode 100755 certora/runSanity.sh create mode 100755 certora/runSanityAssume.sh create mode 100755 certora/runStarportHarness.sh create mode 100755 certora/runStarportHarnessOrdering.sh create mode 100644 certora/spec/CashToken.spec create mode 100644 certora/spec/CashTokenHarness.spec create mode 100644 certora/spec/Privileged.spec create mode 100644 certora/spec/Starport.spec create mode 100644 certora/spec/StarportOrdering.spec create mode 100644 certora/spec/erc20.spec create mode 100644 certora/spec/harnesses/ERC20.sol create mode 100644 certora/spec/harnesses/ExcessiveERC20.sol create mode 100644 certora/spec/harnesses/NonStandardERC20.sol create mode 100644 certora/spec/sanity.spec create mode 100644 certora/spec/sanitySound.spec diff --git a/certora/contracts/CashToken.sol b/certora/contracts/CashToken.sol new file mode 100644 index 000000000..03d370c3d --- /dev/null +++ b/certora/contracts/CashToken.sol @@ -0,0 +1,289 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity ^0.8.1; + +import "./ICash.sol"; + +/** + * @title Compound Cash Token + * @author Compound Finance + * @notice The Compound Cash Token for Ethereum + */ +contract CashToken is ICash { + // @notice Structure to save gas while storing yield and index + struct CashYieldAndIndex { + uint128 yield; + uint128 index; + } + + /// @notice The number of seconds in the year, used for Cash index calculations + uint public constant SECONDS_PER_YEAR = 31536000; + + /// @notice The denomination of Cash index + uint public constant indexBaseUnit = 1e18; + + /// @notice The denomination of `exponent` result + uint public constant expBaseUnit = 1e18; + + /// @notice The denomination of Cash APY BPS + uint public constant bpsBaseUnit = 1e4; + + /// @notice The admin of contract, address of `Starport` contract + address immutable public admin; + + /// @notice The timestamp when current Cash yield and index are activated + uint public cashYieldStart; + + /// @notice The Cash yield and index values + CashYieldAndIndex public cashYieldAndIndex; + + /// @notice The timestamp when next Cash yield and index should be activated + uint public nextCashYieldStart; + + /// @notice The next Cash yield and index values + CashYieldAndIndex public nextCashYieldAndIndex; + + /// @notice See {IERC20-allowance} + mapping (address => mapping (address => uint)) public allowances; + + /// @notice The total amount of minted Cash principal + uint public totalCashPrincipal; + + /// @notice The amount of cash principal per account + mapping (address => uint128) public cashPrincipal; + + /** + * @notice Construct a Cash Token + * @dev You must call `initialize()` after construction + * @param admin_ The address of admin + */ + constructor(address admin_) { + admin = admin_; + } + + /** + * @notice Initialize Cash token contract + * @param initialYield The initial value for Cash token APY in BPS (e.g. 100=1%) + * @param initialYieldStart The timestamp when Cash index and yield were activated on Compound Chain + */ + function initialize(uint128 initialYield, uint initialYieldStart) external { + require(cashYieldAndIndex.index == 0, "Cash Token already initialized"); + + // Note: we don't check that this is in the past, but calls will revert until it is. + cashYieldStart = initialYieldStart; + cashYieldAndIndex = CashYieldAndIndex({yield: initialYield, index: 1e18}); + } + + /** + * Section: Ethereum Asset Interface + */ + + /** + * @notice Mint Cash tokens for the given account + * @dev Invoked by Starport contract + * @dev principal is `u128` to be compliant with Compound Chain + * @param account The owner of minted Cash tokens + * @param principal The principal amount of minted Cash tokens + * @return The minted amount of Cash tokens = principal * index + */ + function mint(address account, uint128 principal) external override returns (uint) { + require(msg.sender == admin, "Must be admin"); + uint amount = principal * getCashIndex() / indexBaseUnit; + cashPrincipal[account] += principal; + totalCashPrincipal = totalCashPrincipal + principal; + emit Transfer(address(0), account, amount); + return amount; + } + + /** + * @notice Burn Cash tokens for the given account + * @dev Invoked by Starport contract + * @dev principal is `u128` to be compliant with Compound Chain + * @param account The owner of burned Cash tokens + * @param amount The amount of burned Cash tokens + * @return The amount of burned principal = amount / index + */ + function burn(address account, uint amount) external override returns (uint128) { + require(msg.sender == admin, "Must be admin"); + uint128 principal = amountToPrincipal(amount); + cashPrincipal[account] -= principal; + totalCashPrincipal = totalCashPrincipal - principal; + emit Transfer(account, address(0), amount); + return principal; + } + + /** + * @notice Update yield and index to be in sync with Compound chain + * @dev It is expected to be called at least once per day + * @dev Cash index denomination is 1e18 + * @param nextYield The new value of Cash APY measured in BPS + * @param nextIndex The new value of Cash index + * @param nextYieldStart The timestamp when new values for cash and index are activated + */ + function setFutureYield(uint128 nextYield, uint128 nextIndex, uint nextYieldStart) external override { + require(msg.sender == admin, "Must be admin"); + uint nextStart = nextCashYieldStart; + + // Updating cash yield and index to the 'old' next values + if (nextStart != 0 && block.timestamp > nextStart) { + cashYieldStart = nextStart; + cashYieldAndIndex = nextCashYieldAndIndex; + } + nextCashYieldStart = nextYieldStart; + nextCashYieldAndIndex = CashYieldAndIndex({yield: nextYield, index: nextIndex}); + } + + /** + * @notice Get current cash index + * @dev Since function is `view` and cannot modify storage, + the check for next index and yield values was added + * @return The current cash index, 18 decimals + */ + function getCashIndex() public view virtual override returns (uint128) { + uint nextStart = nextCashYieldStart; + if (nextStart != 0 && block.timestamp > nextStart) { + return calculateIndex(nextCashYieldAndIndex.yield, nextCashYieldAndIndex.index, nextStart); + } else { + return calculateIndex(cashYieldAndIndex.yield, cashYieldAndIndex.index, cashYieldStart); + } + } + + /** + * Section: ERC20 Interface + */ + + /** + * @notice Returns the amount of tokens in existence. + */ + function totalSupply() external view override returns (uint) { + return totalCashPrincipal * getCashIndex() / indexBaseUnit; + } + + /** + * @notice Returns the amount of tokens owned by `account`. + */ + function balanceOf(address account) view external override returns (uint) { + return cashPrincipal[account] * getCashIndex() / indexBaseUnit; + } + + /** + * @notice Moves `amount` tokens from the caller's account to `recipient`. + * @return a boolean value indicating whether the operation succeeded. + * Emits a {Transfer} event. + */ + function transfer(address recipient, uint amount) external override returns (bool) { + require(msg.sender != recipient, "Invalid recipient"); + uint128 principal = amountToPrincipal(amount); + cashPrincipal[recipient] += principal; + cashPrincipal[msg.sender] -= principal; + emit Transfer(msg.sender, recipient, amount); + return true; + } + + /** + * @notice Returns the remaining number of tokens that `spender` will be + * allowed to spend on behalf of `owner` through {transferFrom}. This is + * zero by default. + * + * This value changes when {approve} or {transferFrom} are called. + */ + function allowance(address owner, address spender) external view override returns (uint256) { + return allowances[owner][spender]; + } + + /** + * @dev Sets `amount` as the allowance of `spender` over the caller's tokens. + * + * Returns a boolean value indicating whether the operation succeeded. + * IMPORTANT: Beware that changing an allowance with this method brings the risk + * that someone may use both the old and the new allowance by unfortunate + * transaction ordering. One possible solution to mitigate this race + * condition is to first reduce the spender's allowance to 0 and set the + * desired value afterwards: + * https://github.com/ethereum/EIPs/issues/20#issuecomment-263524729 + * + * Emits an {Approval} event. + */ + // XXX double check that issue won't occur in transferFrom + function approve(address spender, uint amount) external override returns (bool) { + allowances[msg.sender][spender] = amount; + emit Approval(msg.sender, spender, amount); + return true; + } + + /** + * @notice Moves `amount` tokens from `sender` to `recipient` using the + * allowance mechanism. `amount` is then deducted from the caller's + * allowance. + * @return a boolean value indicating whether the operation succeeded. + * Emits a {Transfer} event. + */ + function transferFrom(address sender, address recipient, uint256 amount) external override returns (bool) { + require(sender != recipient, "Invalid recipient"); + address spender = msg.sender; + uint128 principal = amountToPrincipal(amount); + allowances[sender][spender] -= amount; + cashPrincipal[recipient] += principal; + cashPrincipal[sender] -= principal; + emit Transfer(sender, recipient, amount); + return true; + } + + /** + * @notice Returns the name of the token. + */ + function name() external pure returns (string memory) { + return "SECRET, change"; + } + + /** + * @notice Returns the symbol of the token, usually a shorter version of the + * name. + */ + function symbol() external pure returns (string memory) { + return "SECRET"; + } + + /** + * @notice Returns the number of decimals + */ + function decimals() external pure returns (uint8) { + return 6; + } + + /** + * Section: Function Helpers + */ + + // Helper function to conver amount to principal using current Cash index + function amountToPrincipal(uint amount) virtual public returns (uint128) { + uint256 principal = amount * indexBaseUnit / getCashIndex(); + require(principal < type(uint128).max, "amountToPrincipal::overflow"); + return uint128(principal); + } + + // Helper function to calculate current Cash index + // Note: Formula for continuos compounding interest -> A = Pe^rt, + // current_index = base_index * e^(yield * time_ellapsed) + // yield is in BPS, so 300 = 3% = 0.03 + // XXX TODO: check if it's really safe if time_elapsed > 1 day and yield is high + function calculateIndex(uint128 yield, uint128 index, uint start) virtual public view returns (uint128) { + require(index > 0, "Cash Token uninitialized"); + uint newIndex = index * exponent(yield, block.timestamp - start) / expBaseUnit; + require(newIndex < type(uint128).max, "calculateIndex::overflow"); + return uint128(newIndex); + } + + // Helper function to calculate e^rt part from countinous compounding interest formula + // Note: We use the third degree approximation of Taylor Series + // 1 + x/1! + x^2/2! + x^3/3! + // XXX TODO: check if it's really safe if time_elapsed > 1 day and yield is high + // XXX TODO add ranges for which it works + function exponent(uint128 yield, uint time) public pure returns (uint) { + uint scale = expBaseUnit / bpsBaseUnit; + uint epower = yield * time * scale / SECONDS_PER_YEAR; + uint first = epower * expBaseUnit ** 2; + uint second = epower * epower * expBaseUnit / 2; + uint third = epower * epower * epower / 6; + return (expBaseUnit ** 3 + first + second + third) / expBaseUnit ** 2; + } +} \ No newline at end of file diff --git a/certora/contracts/CashTokenHarness.sol b/certora/contracts/CashTokenHarness.sol new file mode 100644 index 000000000..059ceffdc --- /dev/null +++ b/certora/contracts/CashTokenHarness.sol @@ -0,0 +1,27 @@ +pragma solidity ^0.8.1; +pragma abicoder v2; + +import './CashToken.sol'; + + +contract CashTokenHarness is CashToken { + // yield -> index -> start -> timestamp -> uint128 + mapping(uint128 => mapping(uint128 => mapping(uint256 => mapping(uint256 => uint128)))) uninterpIndexCalc; + // amount -> calculatedIndex -> uint128 + mapping(uint256 => mapping(uint128 => uint128)) uninterpPrincipalCalc; + + constructor(address admin_) CashToken(admin_) {} + + function calculateIndex(uint128 yield, uint128 index, uint start) override public view returns (uint128) { + // uint128 newIndex = super.calculateIndex(yield, index, start); + // require(newIndex == uninterpIndexCalc[yield][index][start][block.timestamp]); + // return newIndex; + return uninterpIndexCalc[yield][index][start][block.timestamp]; + } + + function amountToPrincipal(uint amount) override public returns (uint128) { + uint128 principal = super.amountToPrincipal(amount); + uninterpPrincipalCalc[amount][getCashIndex()] = principal; + return principal; + } +} \ No newline at end of file diff --git a/certora/contracts/ICash.sol b/certora/contracts/ICash.sol new file mode 100644 index 000000000..ddb82dec5 --- /dev/null +++ b/certora/contracts/ICash.sol @@ -0,0 +1,37 @@ +// SPDX-License-Identifier: GPL-3.0 + +pragma solidity ^0.8.1; + +/** + * @title Generic Erc-20 Interface + */ +interface IERC20 { + function totalSupply() external view returns (uint256); + function balanceOf(address account) external view returns (uint256); + function transfer(address recipient, uint256 amount) external returns (bool); + function allowance(address owner, address spender) external view returns (uint256); + function approve(address spender, uint amount) external returns (bool); + function transferFrom(address sender, address recipient, uint256 amount) external returns (bool); + + event Transfer(address indexed from, address indexed to, uint256 value); + event Approval(address indexed owner, address indexed spender, uint256 value); +} + +/** + * @title Generic Cash Token Interface + */ +interface ICash is IERC20 { + function mint(address account, uint128 principal) external returns (uint); + function burn(address account, uint amount) external returns (uint128); + function setFutureYield(uint128 nextYield, uint128 nextIndex, uint nextYieldStartAt) external; + function getCashIndex() external view returns (uint128); +} + +/** + * @title Non-Standard Erc-20 Interface for tokens which do not return from `transfer` or `transferFrom` + */ +interface INonStandardERC20 { + function transfer(address recipient, uint256 amount) external; + function transferFrom(address sender, address recipient, uint256 amount) external; + function balanceOf(address account) external view returns (uint256); +} \ No newline at end of file diff --git a/certora/contracts/Starport.sol b/certora/contracts/Starport.sol new file mode 100644 index 000000000..b126cd406 --- /dev/null +++ b/certora/contracts/Starport.sol @@ -0,0 +1,470 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity ^0.8.1; +pragma abicoder v2; + +import "./ICash.sol"; + +/** + * @title Compound Chain Starport + * @author Compound Finance + * @notice Contract to link Ethereum to Compound Chain + */ +contract Starport { + ICash immutable public cash; + + address immutable public admin; + address constant public ETH_ADDRESS = address(0xEeeeeEeeeEeEeeEeEeEeeEEEeeeeEeeeeeeeEEeE); + bytes4 constant MAGIC_HEADER = "ETH:"; + address[] public authorities; + mapping(address => uint) public supplyCaps; + + uint public eraId; // TODO: could bitpack here and use uint32 + mapping(bytes32 => bool) public isNoticeInvoked; + + event NoticeInvoked(uint32 indexed eraId, uint32 indexed eraIndex, bytes32 indexed noticeHash, bytes result); + event NoticeReplay(bytes32 indexed noticeHash); + + event Lock(address indexed asset, address indexed sender, address indexed recipient, uint amount); + event LockCash(address indexed sender, address indexed recipient, uint amount, uint128 principal); + event ExecTrxRequest(address indexed account, string trxRequest); + event Unlock(address indexed account, uint amount, address asset); + event UnlockCash(address indexed account, uint amount, uint128 principal); + event ChangeAuthorities(address[] newAuthorities); + event SetFutureYield(uint128 nextCashYield, uint128 nextCashYieldIndex, uint nextCashYieldStart); + event ExecuteProposal(string title, bytes[] extrinsics); + event NewSupplyCap(address indexed asset, uint supplyCap); + + constructor(ICash cash_, address admin_) { + cash = cash_; + admin = admin_; + } + + /** + * Section: Ethereum Asset Interface + */ + + /** + * @notice Transfer an asset to Compound Chain via locking it in the Starport + * @dev Use `lockEth` to lock Ether. Note: locking CASH will burn the CASH from Ethereum. + * @param amount The amount (in the asset's native wei) to lock + * @param asset The asset to lock in the Starport + */ + function lock(uint amount, address asset) external { + lockTo(amount, asset, msg.sender); + } + + /** + * @notice Transfer an asset to Compound Chain via locking it in the Starport + * @dev Use `lockEth` to lock Ether. Note: locking CASH will burn the CASH from Ethereum. + * @param amount The amount (in the asset's native wei) to lock + * @param asset The asset to lock in the Starport + * @param recipient The recipient of the asset in Compound Chain + */ + function lockTo(uint amount, address asset, address recipient) public { + require(asset != ETH_ADDRESS, "Please use lockEth"); + + if (asset == address(cash)) { + lockCashInternal(amount, recipient); + } else { + lockAssetInternal(amount, asset, recipient); + } + } + + /* + * @notice Transfer Eth to Compound Chain via locking it in the Starport + * @dev Use `lock` to lock CASH or collateral assets. + */ + function lockEth() public payable { + lockEthTo(msg.sender); + } + + /* + * @notice Transfer Eth to Compound Chain via locking it in the Starport + * @param recipient The recipient of the Eth on Compound Chain + * @dev Use `lock` to lock CASH or collateral assets. + */ + function lockEthTo(address recipient) public payable { + require(address(this).balance <= supplyCaps[ETH_ADDRESS], "Supply Cap Exceeded"); + emit Lock(ETH_ADDRESS, msg.sender, recipient, msg.value); + } + + /* + * @notice Emits an event s.t. a given trx request will execute as if called by `msg.sender` + * @dev Externally-owned accounts may call `execTrxRequest` with a signed message to avoid Ethereum fees. + * @param trxRequest An ASCII-encoded transaction request + */ + function execTrxRequest(string calldata trxRequest) public payable { + emit ExecTrxRequest(msg.sender, trxRequest); + } + + /** + * @notice Internal function for locking CASH (as opposed to collateral assets) + * @dev Locking CASH will burn the CASH (as it's being transfer to Compound Chain) + * @param amount The amount of CASH to lock and burn. + */ + function lockCashInternal(uint amount, address recipient) internal { + uint128 principal = cash.burn(msg.sender, amount); + emit LockCash(msg.sender, recipient, amount, principal); + } + + // Internal function for locking non-ETH collateral assets + function lockAssetInternal(uint amount, address asset, address recipient) internal { + uint amountTransferred = transferAssetIn(msg.sender, amount, asset); + require(IERC20(asset).balanceOf(address(this)) <= supplyCaps[asset], "Supply Cap Exceeded"); + emit Lock(asset, msg.sender, recipient, amountTransferred); + } + + // Transfer in an asset, returning the balance actually accrued (i.e. less token fees) + // Note: do not use for Ether or CASH + function transferAssetIn(address from, uint amount, address asset) internal returns (uint) { + uint balanceBefore = IERC20(asset).balanceOf(address(this)); + INonStandardERC20(asset).transferFrom(from, address(this), amount); + + bool success; + assembly { + switch returndatasize() + case 0 { // This is a non-standard ERC-20 + success := not(0) // set success to true + } + case 32 { // This is a compliant ERC-20 + returndatacopy(0, 0, 32) + success := mload(0) // Set `success = returndata` of external call + } + default { // This is an excessively non-compliant ERC-20, revert. + revert(0, 0) + } + } + require(success, "transferAssetIn failed"); + + uint balanceAfter = IERC20(asset).balanceOf(address(this)); + return balanceAfter - balanceBefore; + } + + // Transfer out an asset + // Note: we do not check fees here, since we do not account for them on transfer out + function transferAssetOut(address to, uint amount, address asset) internal { + INonStandardERC20(asset).transfer(to, amount); + + bool success; + assembly { + switch returndatasize() + case 0 { // This is a non-standard ERC-20 + success := not(0) // set success to true + } + case 32 { // This is a complaint ERC-20 + returndatacopy(0, 0, 32) + success := mload(0) // Set `success = returndata` of external call + } + default { // This is an excessively non-compliant ERC-20, revert. + revert(0, 0) + } + } + require(success, "transferAssetOut failed"); + } + + /** + * @notice Executes governance proposal on Compound Chain + * @dev This must be called from the admin, which should be the Compound Timelock + * @param extrinsics SCALE-encoded extrinsics that can execute on Compound Chain + */ + function executeProposal(string calldata title, bytes[] calldata extrinsics) external { + require(msg.sender == admin, "Call must originate from admin"); + + emit ExecuteProposal(title, extrinsics); + } + + /* + * @notice Transfer Eth to Compound Chain via locking it in the Starport + * @dev This is a shortcut for `lockEth`. See `lockEth` for more details. + */ + receive() external payable { + lockEth(); + } + + /** + * Section: L2 Message Ports + **/ + + /** + * @notice Invoke a signed notice from the Starport, which will execute a function such as unlock. + * @dev Notices are generated by certain actions from Compound Chain and signed by validators. + * @param notice The notice generated by Compound Chain, encoded for Ethereum. + * @param signatures Signatures from a quorum of validator nodes from Compound Chain. + * @return The result of the invokation of the action of the notice. + */ + function invoke(bytes calldata notice, bytes[] calldata signatures) external returns (bytes memory) { + bytes32 noticeHash = hashNotice(notice); + checkNoticeSignerAuthorized(noticeHash, authorities, signatures); + + return invokeNoticeInternal(notice, noticeHash); + } + + /** + * @notice Invoke a notice by passing a chain of notices the head of which has already been accepted + * @dev As an alternative to `invoke`, for instance, after authorities have been rotated. + * @param notice The notice generated by Compound Chain, encoded for Ethereum. + * @param notices A chain of notices, the tail of which must have already been accepted + * @return The result of the invokation of the action of the notice. + */ + function invokeChain(bytes calldata notice, bytes[] calldata notices) external returns (bytes memory) { + bytes32 noticeHash = hashNotice(notice); + checkNoticeChainAuthorized(noticeHash, notices); + + return invokeNoticeInternal(notice, noticeHash); + } + + // Invoke without authorization checks used by external functions + function invokeNoticeInternal(bytes calldata notice, bytes32 noticeHash) virtual internal returns (bytes memory) { + if (isNoticeInvoked[noticeHash]) { + emit NoticeReplay(noticeHash); + return ""; + } + + isNoticeInvoked[noticeHash] = true; + + require(notice.length >= 100, "Must have full header"); // 4 + 3 * 32 + require(notice[0] == MAGIC_HEADER[0], "Invalid header[0]"); + require(notice[1] == MAGIC_HEADER[1], "Invalid header[1]"); + require(notice[2] == MAGIC_HEADER[2], "Invalid header[2]"); + require(notice[3] == MAGIC_HEADER[3], "Invalid header[3]"); + + (uint noticeEraId, uint noticeEraIndex, bytes32 noticeParent) = + abi.decode(notice[4:100], (uint, uint, bytes32)); + + noticeParent; // unused + + bool startNextEra = noticeEraId == eraId + 1 && noticeEraIndex == 0; + + require( + noticeEraId <= eraId || startNextEra, + "Notice must use existing era or start next era" + ); + + if (startNextEra) { + eraId++; + } + + bytes memory calldata_ = bytes(notice[100:]); + (bool success, bytes memory callResult) = address(this).call(calldata_); + if (!success) { + require(false, _getRevertMsg(callResult)); + } + + emit NoticeInvoked(uint32(noticeEraId), uint32(noticeEraIndex), noticeHash, callResult); + + return callResult; + } + + /** + * @notice Unlock the given asset from the Starport + * @dev This must be called from `invoke` via passing in a signed notice from Compound Chain. + * @dev Note: for Cash token, we would expect to use `unlockCash` which mints the CASH. + * @param asset The Asset to unlock + * @param amount The amount of the asset to unlock in its native token units + * @param account The account to transfer the asset to + */ + function unlock(address asset, uint amount, address payable account) external { + require(msg.sender == address(this), "Call must originate locally"); + + emit Unlock(account, amount, asset); + + if (asset == ETH_ADDRESS) { + account.transfer(amount); + } else { + transferAssetOut(account, amount, asset); + } + } + + /** + * @notice Unlock CASH from the Starport by minting + * @dev This must be called from `invoke` via passing in a signed notice from Compound Chain. + * @param account The account to transfer the asset to + * @param principal The principal of CASH to unlock + */ + function unlockCash(address account, uint128 principal) external { + require(msg.sender == address(this), "Call must originate locally"); + + uint256 amount = cash.mint(account, principal); + emit UnlockCash(account, amount, principal); + } + + /** + * @notice Rotates authorities which can be used to sign notices for the Staport + * @dev This must be called from `invoke` via passing in a signed notice from Compound Chain or by the admin. + * @param newAuthorities The new authorities which may sign notices for execution by the Starport + */ + function changeAuthorities(address[] calldata newAuthorities) external { + require(msg.sender == address(this) || msg.sender == admin, "Call must be by notice or admin"); + require(newAuthorities.length > 0, "New authority set can not be empty"); + + emit ChangeAuthorities(newAuthorities); + + authorities = newAuthorities; + } + + /** + * @notice Sets the supply cap for a given asset. + * @dev This must be called from `invoke` via passing in a signed notice from Compound Chain or by the admin. + * @dev Note: supply caps start at zero. This must be called to allow an asset to be locked in the Starport. + * @param asset The asset to set the supply cap for. This may be Ether Token but may not be CASH. + * @param supplyCap The cap to put on the asset, in its native token units. + */ + function setSupplyCap(address asset, uint supplyCap) external { + require(msg.sender == address(this) || msg.sender == admin, "Call must be by notice or admin"); + require(asset != address(cash), "Cash does not accept supply cap"); + + emit NewSupplyCap(asset, supplyCap); + + supplyCaps[asset] = supplyCap; + } + + /** + * @notice Sets the yield of the CASH token for some future time. + * @dev This must be called from `invoke` via passing in a signed notice from Compound Chain or by the admin. + * @param nextCashYield The yield to set + * @param nextCashYieldIndex The pre-calculated index at change-over for error correction + * @param nextCashYieldStart When the yield change-over should occur + */ + function setFutureYield(uint128 nextCashYield, uint128 nextCashYieldIndex, uint nextCashYieldStart) external { + require(msg.sender == address(this) || msg.sender == admin, "Call must be by notice or admin"); + + emit SetFutureYield(nextCashYield, nextCashYieldIndex, nextCashYieldStart); + cash.setFutureYield(nextCashYield, nextCashYieldIndex, nextCashYieldStart); + } + + /** + * Section: View Helpers + */ + + /** + * @notice Returns the current authority nodes + * @return The current authority node addresses + */ + function getAuthorities() public view returns (address[] memory) { + return authorities; + } + + /** + * @notice Checks that the given notice is authorized + * @dev Notices are authorized by having a quorum of signatures from the `authorities` set + * @dev Notices can be separately validated by a notice chain + * @dev Reverts if notice is not authorized + * @param noticeHash Hash of the given notice + * @param authorities_ A set of authorities to check the notice against + * @param signatures The signatures to verify + */ + function checkNoticeSignerAuthorized( + bytes32 noticeHash, + address[] memory authorities_, + bytes[] calldata signatures + ) internal view { + address[] memory sigs = new address[](signatures.length); + for (uint i = 0; i < signatures.length; i++) { + address signer = recover(noticeHash, signatures[i]); + require(contains(sigs, signer) == false, "Duplicated authority signer"); + require(contains(authorities_, signer) == true, "Unauthorized authority signer"); + sigs[i] = signer; + } + + require(sigs.length >= getQuorum(authorities_.length), "Below quorum threshold"); + } + + /** + * @notice Checks that the given target notice is valid by chaining + * @dev Notices each contain a hash of the parent, and thus any previous notice can be + * @dev included by showing a chain of notices connecting to an already accepted notice. + * @param targetHash Hash of the target notice to verify + * @param notices A list of notices where the tail notice must already be accepted in the chain + */ + function checkNoticeChainAuthorized( + bytes32 targetHash, + bytes[] calldata notices + ) internal view { + bytes32 currHash = targetHash; + + for (uint i = 0; i < notices.length; i++) { + require(getParentHash(notices[i]) == currHash, "Notice hash mismatch"); + currHash = hashNotice(notices[i]); + } + + require(isNoticeInvoked[currHash] == true, "Tail notice must have been accepted"); + } + + /** + * Section: Pure Function Helpers + */ + + // Helper function to hash a notice + function hashNotice(bytes calldata data) virtual internal pure returns (bytes32) { + return keccak256((abi.encodePacked(data))); + } + + // Helper function to check if a given list contains an element + function contains(address[] memory arr, address elem) internal pure returns (bool) { + for (uint i = 0; i < arr.length; i++) { + if (arr[i] == elem) { + return true; + } + } + return false; + } + + // Helper function to get parent hash from a notice + // Note: we don't check much about the notices, but since we're verifying + // by notice hashes, we should be secure. + // TODO: Consider if we should use the full decoding check from above? + function getParentHash(bytes calldata notice) pure internal returns (bytes32) { + require(notice.length >= 100, "Must have full header"); // 4 + 3 * 32 + (bytes32 noticeParent) = + abi.decode(notice[68:100], (bytes32)); + + return noticeParent; + } + + // Quorum is >1/3 authorities approving (XXX TODO: 1/3??) + function getQuorum(uint authorityCount) internal pure returns (uint) { + return (authorityCount / 3) + 1; + } + + // Adapted from https://github.com/OpenZeppelin/openzeppelin-contracts/blob/master/contracts/cryptography/ECDSA.sol + function recover(bytes32 digest, bytes memory signature) virtual internal view returns (address) { + // Check the signature length + if (signature.length != 65) { + revert("ECDSA: invalid signature length"); + } + + // Divide the signature in r, s and v variables + bytes32 r; + bytes32 s; + uint8 v; + + // ecrecover takes the signature parameters, and the only way to get them + // currently is to use assembly. + // solhint-disable-next-line no-inline-assembly + assembly { + r := mload(add(signature, 0x20)) + s := mload(add(signature, 0x40)) + v := byte(0, mload(add(signature, 0x60))) + } + + // XXX Does this mean EIP-155 signatures are considered invalid? + require(v == 27 || v == 28, "ECDSA: invalid signature 'v' value"); + + // If the signature is valid (and not malleable), return the signer address + address signer = ecrecover(digest, v, r, s); + require(signer != address(0), "ECDSA: invalid signature"); + + return signer; + } + + function _getRevertMsg(bytes memory _returnData) internal pure returns (string memory) { + // If the _res length is less than 68, then the transaction failed silently (without a revert message) + if (_returnData.length < 68) return 'Call failed'; + + assembly { + // Slice the sighash. + _returnData := add(_returnData, 0x04) + } + return abi.decode(_returnData, (string)); // All that remains is the revert string + } +} \ No newline at end of file diff --git a/certora/contracts/StarportHarness.sol b/certora/contracts/StarportHarness.sol new file mode 100644 index 000000000..8113bcaf5 --- /dev/null +++ b/certora/contracts/StarportHarness.sol @@ -0,0 +1,152 @@ +pragma solidity ^0.8.1; +pragma abicoder v2; + +import './Starport.sol'; + + +contract StarportHarness is Starport { + constructor(ICash cash_, address admin_) Starport(cash_, admin_) {} + + address[] havocdAuthorities; + bytes[] havocdSignatures; + bytes[] havocdNotices; + bytes havocdNotice; + bool public isAssert; + + // for harness version of recover + mapping(bytes32 => mapping(bytes => address)) recoverer; + + function noticeAlreadyInvoked() public returns (bool) { + // force model of hash not to just havoc + bytes32 noticeHash = this.hashNoticeExt(havocdNotice); + return isNoticeInvoked[noticeHash]; + } + + function nowAssert() public { + isAssert = true; + } + + function invokeNotice(bytes calldata theNotice, bytes[] calldata signatures) public returns (bool) { + if (isAssert) { + bytes32 noticeHash = this.hashNoticeExt(theNotice); + return isNoticeInvoked[noticeHash]; + } else { + this.invoke(theNotice, signatures); + return true; + } + } + + function invokeNoticeChain(bytes calldata theNotice, bytes[] calldata notices) public returns (bool) { + if (isAssert) { + bytes32 noticeHash = hashNotice(theNotice); + return isNoticeInvoked[noticeHash]; + } else { + this.invokeChain(theNotice, notices); + return true; + } + } + + function partialOrderingCall(bytes calldata notice) public returns (uint256,uint256,bytes32) { + if (isAssert) { + bytes32 noticeHash = hashNotice(notice); + uint256 returnSize = invokeNoticeInternal(notice, noticeHash).length; + return (returnSize,0,0); + } else { + return myNoticeInfo(notice); + } + } + + function myNoticeInfo(bytes calldata notice) public returns (uint256,uint256,bytes32) { + // copy-pasat from invokeNoticeInternal + (uint noticeEraId, uint noticeEraIndex, bytes32 noticeParent) = + abi.decode(notice[4:100], (uint, uint, bytes32)); + bytes32 noticeHash = hashNotice(notice); + return (noticeEraId, noticeEraIndex, noticeHash); + } + + function noticeReturnsEmptyString() public returns (bool) { + return this.invokeNoticeInternalExt(havocdNotice, this.hashNoticeExt(havocdNotice)).length == 0; + } + + function invokeNoticeInternalExt(bytes calldata notice, bytes32 noticeHash) public returns (bytes memory) { + return invokeNoticeInternal(notice, noticeHash); + } + + function balanceInERC20Asset(address asset) public view returns (uint256) { + return IERC20(asset).balanceOf(address(this)); + } + + function signaturesAuthorizedPrecondition(uint256 nSignatures, uint256 nAuthorities, bytes32 noticeHash) public { + require(havocdSignatures.length == nSignatures); + require(havocdAuthorities.length == nAuthorities); + for (uint i = 0; i < nSignatures; i++) { + for (uint j = 0; j < nSignatures; j++) { + if (i != j) { + require(recover(noticeHash, havocdSignatures[i]) != recover(noticeHash, havocdSignatures[j])); + } + } + require(contains(havocdAuthorities, recover(noticeHash, havocdSignatures[i]))); + } + } + + function checkSignatures(uint256 nSignatures, uint256 nAuthorities, bytes32 noticeHash) public { + address[] memory authorities = new address[](nAuthorities); + bytes[] memory signatures = new bytes[](nSignatures); + for (uint i = 0; i < nSignatures; i++) { + signatures[i] = havocdSignatures[i]; + } + for (uint i = 0; i < nAuthorities; i++) { + authorities[i] = havocdAuthorities[i]; + } + this.checkSignaturesAuthorized(noticeHash, authorities, signatures); + } + + function checkSignaturesAuthorized(bytes32 noticeHash, address[] memory authorities, bytes[] calldata signatures) public { + checkNoticeSignerAuthorized(noticeHash, authorities, signatures); + } + + function hashChainTargetNotParentPrecond(bytes32 targetHash) public { + bytes memory firstNotice = havocdNotices[0]; + require(this.getParentHashExt(firstNotice) != targetHash); + } + + function hashChainBrokenLinkPrecond(uint256 brokenLink) public { + require(brokenLink + 1 < havocdNotices.length); + bytes memory firstNotice = havocdNotices[brokenLink + 1]; + bytes memory shouldBeParentNotice = havocdNotices[brokenLink]; + bytes32 shouldBeParentHash = this.hashNoticeExt(shouldBeParentNotice); + bytes32 parentHashOfFirstNotice = this.getParentHashExt(firstNotice); + require(shouldBeParentHash != parentHashOfFirstNotice); + } + + function getParentHashExt(bytes calldata theNotice) public returns (bytes32) { + return getParentHash(theNotice); + } + + function hashNoticeExt(bytes calldata theNotice) public returns (bytes32) { + return hashNotice(theNotice); + } + + function hashNotice(bytes calldata data) override internal pure returns (bytes32) { + return keccak256(data[4:68]); + } + + function checkNoticeChain(bytes32 targetHash) public { + bytes[] memory notices = new bytes[](havocdNotices.length); + for (uint i = 0; i < havocdNotices.length; i++) { + notices[i] = havocdNotices[i]; + } + this.checkNoticeChainAuthorizedExt(targetHash, notices); + } + + function checkNoticeChainAuthorizedExt( + bytes32 targetHash, + bytes[] calldata notices + ) public { + checkNoticeChainAuthorized(targetHash, notices); + } + + function recover(bytes32 digest, bytes memory signature) override internal view returns (address) { + return recoverer[digest][signature]; + } +} \ No newline at end of file diff --git a/certora/contracts/StarportHarnessOrdering.sol b/certora/contracts/StarportHarnessOrdering.sol new file mode 100644 index 000000000..86b8208d7 --- /dev/null +++ b/certora/contracts/StarportHarnessOrdering.sol @@ -0,0 +1,52 @@ +pragma solidity ^0.8.1; +pragma abicoder v2; + +import './StarportHarness.sol'; + + +contract StarportHarnessOrdering is StarportHarness { + constructor(ICash cash_, address admin_) StarportHarness(cash_, admin_) {} + + function invokeNoticeInternal(bytes calldata notice, bytes32 noticeHash) override internal returns (bytes memory) { + if (isNoticeInvoked[noticeHash]) { + emit NoticeReplay(noticeHash); + return ""; + } + + isNoticeInvoked[noticeHash] = true; + + require(notice.length >= 100, "Must have full header"); // 4 + 3 * 32 + require(notice[0] == MAGIC_HEADER[0], "Invalid header[0]"); + require(notice[1] == MAGIC_HEADER[1], "Invalid header[1]"); + require(notice[2] == MAGIC_HEADER[2], "Invalid header[2]"); + require(notice[3] == MAGIC_HEADER[3], "Invalid header[3]"); + + (uint noticeEraId, uint noticeEraIndex, bytes32 noticeParent) = + abi.decode(notice[4:100], (uint, uint, bytes32)); + + noticeParent; // unused + + bool startNextEra = noticeEraId == eraId + 1 && noticeEraIndex == 0; + + require( + noticeEraId <= eraId || startNextEra, + "Notice must use existing era or start next era" + ); + + if (startNextEra) { + eraId++; + } + + // bytes memory calldata_ = bytes(notice[100:]); + // (bool success, bytes memory callResult) = address(this).call(calldata_); + // if (!success) { + // require(false, _getRevertMsg(callResult)); + // } + + // emit NoticeInvoked(uint32(noticeEraId), uint32(noticeEraIndex), noticeHash, callResult); + + // return callResult; + + return "success"; + } +} \ No newline at end of file diff --git a/certora/readme.txt b/certora/readme.txt new file mode 100644 index 000000000..5d0e8600c --- /dev/null +++ b/certora/readme.txt @@ -0,0 +1,10 @@ + + - Run Scripts + CashToken: + - runCashToken.sh: specs without any summarizing + - runCashHarness.sh: spects summarizing index as 1e18 and axiomatizing + amountToPrincipal as monotonic + Starport: + - runStarportHarness.sh: specs, no summaries but harnessing needed + - runStarportHarnessOrdering.sh: partial ordering spec, override invokeNoticeInternal to not + perform the function call since this havocs all storage \ No newline at end of file diff --git a/certora/runCashToken.sh b/certora/runCashToken.sh new file mode 100755 index 000000000..c3daedb2f --- /dev/null +++ b/certora/runCashToken.sh @@ -0,0 +1,5 @@ +certoraRun.py contracts/CashToken.sol \ + --verify CashToken:spec/CashToken.spec \ + --solc solc8.1 --settings -t=300,-assumeUnwindCond,-b=3 \ + --cache "CashToken" \ + --cloud --msg "CashToken: ERC20 etc." \ No newline at end of file diff --git a/certora/runCashTokenHarness.sh b/certora/runCashTokenHarness.sh new file mode 100755 index 000000000..4229683c6 --- /dev/null +++ b/certora/runCashTokenHarness.sh @@ -0,0 +1,5 @@ +certoraRun.py contracts/CashTokenHarness.sol \ + --verify CashTokenHarness:spec/CashTokenHarness.spec \ + --solc solc8.1 --settings -t=300,-ignoreViewFunctions,-assumeUnwindCond,-b=3 \ + --cache "CashTokenHarness" \ + --cloud --msg "CashToken with Harness: ERC20 etc." \ No newline at end of file diff --git a/certora/runPrivileged.sh b/certora/runPrivileged.sh new file mode 100755 index 000000000..bb2a88f02 --- /dev/null +++ b/certora/runPrivileged.sh @@ -0,0 +1,5 @@ +contract=${1} +certoraRun.py contracts/${contract}.sol \ + --verify ${contract}:spec/Privileged.spec \ + --solc solc8.1 --settings -t=300,-ignoreViewFunctions,-assumeUnwindCond,-b=3 \ + --cloud --msg "${contract} Privileged" diff --git a/certora/runSanity.sh b/certora/runSanity.sh new file mode 100755 index 000000000..73f54f18b --- /dev/null +++ b/certora/runSanity.sh @@ -0,0 +1,6 @@ +contract=${1} +certoraRun.py contracts/${contract}.sol \ + --verify ${contract}:spec/sanity.spec \ + --solc solc8.1 \ + --settings -t=300 \ + --cloud --msg "${contract} Sanity" diff --git a/certora/runSanityAssume.sh b/certora/runSanityAssume.sh new file mode 100755 index 000000000..895c4d143 --- /dev/null +++ b/certora/runSanityAssume.sh @@ -0,0 +1,6 @@ +contract=${1} +certoraRun.py contracts/${contract}.sol \ + --verify ${contract}:spec/sanity.spec \ + --solc solc8.1 \ + --settings -t=300,-assumeUnwindCond \ + --cloud --msg "${contract} Sanity with assume unwind" diff --git a/certora/runStarportHarness.sh b/certora/runStarportHarness.sh new file mode 100755 index 000000000..341a41a77 --- /dev/null +++ b/certora/runStarportHarness.sh @@ -0,0 +1,9 @@ +certoraRun.py contracts/StarportHarness.sol \ + spec/harnesses/ERC20.sol \ + spec/harnesses/NonStandardERC20.sol \ + spec/harnesses/ExcessiveERC20.sol \ + contracts/CashToken.sol \ + --verify StarportHarness:spec/Starport.spec \ + --solc solc8.1 --settings -t=300,-assumeUnwindCond,-b=3 \ + --cache "the-starport-cache" \ + --cloud --msg "Starport with Harness" \ No newline at end of file diff --git a/certora/runStarportHarnessOrdering.sh b/certora/runStarportHarnessOrdering.sh new file mode 100755 index 000000000..525528a3c --- /dev/null +++ b/certora/runStarportHarnessOrdering.sh @@ -0,0 +1,9 @@ +certoraRun.py contracts/StarportHarnessOrdering.sol \ + spec/harnesses/ERC20.sol \ + spec/harnesses/NonStandardERC20.sol \ + spec/harnesses/ExcessiveERC20.sol \ + contracts/CashToken.sol \ + --verify StarportHarnessOrdering:spec/StarportOrdering.spec \ + --solc solc8.1 --settings -t=300,-assumeUnwindCond,-b=3 \ + --cache "starport-ordering" \ + --cloud --msg "Starport with Harness: Notice Partial Ordering" \ No newline at end of file diff --git a/certora/spec/CashToken.spec b/certora/spec/CashToken.spec new file mode 100644 index 000000000..eabfa8452 --- /dev/null +++ b/certora/spec/CashToken.spec @@ -0,0 +1,653 @@ +methods { + totalCashPrincipal() returns (uint256) envfree; + amountToPrincipal(uint256) returns (uint128); + admin() returns (address) envfree; + indexBaseUnit() returns (uint256) envfree; + transfer(address,uint256); + cashYieldAndIndex() returns (uint128,uint128) envfree; + nextCashYieldAndIndex() returns (uint128,uint128) envfree; + balanceOf(address) returns (uint256); + cashPrincipal(address) returns (uint128) envfree; +} + +definition MAX_UINT256() returns uint256 = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff; +definition MAX_UINT128() returns uint256 = 0xffffffffffffffffffffffffffffffff; +definition MAX_ADDRESS() returns uint256 = 0xffffffffffffffffffffffffffffffffffffffff; +// MAX_UINT128 / 1e18 +definition MAX_AMOUNT() returns uint256 = 340282366920938487808; +// 1e18 +definition INDEX_BASE_UNIT() returns uint256 = 1000000000000000000; + +/** x and y are almost equal; y may be _smaller or larger_ than x up to an amount of epsilon */ +definition bounded_error_eq(uint x, uint y, uint epsilon) returns bool = x <= y + epsilon && x + epsilon >= y; +/** x and y are almost equal; y may be _smaller_ than x up to an amount of epsilon */ +definition only_slightly_larger_than(uint x, uint y, uint epsilon) returns bool = y <= x && x <= y + epsilon; +/** x and y are almost equal; y may be _larger_ than x up to an amount of epsilon */ +definition only_slightly_smaller_than(uint x, uint y, uint epsilon) returns bool = x <= y && y <= x + epsilon; + +/** + * A ghost function that shadows the storage variable totalCashPrincipal + */ +ghost principal() returns uint256; + +/** + * We use a hook to define principal as the sum of all entries inside cashPrincipal + */ +hook Sstore cashPrincipal[KEY address _] uint128 balance (uint128 old_balance) STORAGE { + require old_balance <= principal(); + require balance <= MAX_UINT128(); + require old_balance <= MAX_UINT128(); + havoc principal assuming principal@new() == principal@old() + (balance - old_balance); + require principal() <= MAX_UINT256(); +} + +/** + * Using the ghost principal (defined to be the sum of entries inside cashPrincipal) + * we prove the invariant that totalCashPrincipal == principal and so it is also an + * invariant that totalCashPrincipal the sum of entries inside cashPrincipal + */ +rule integrityOfTotalCashPrincipal(method f) { + env e; + calldataarg args; + require totalCashPrincipal() == principal(); + f(e, args); + assert totalCashPrincipal() == principal(); +} + +/** + * @title Monotonicity of Amount to Principal + * @status timing out: this is just too hard for SMT + */ +rule monotonicityOfAmountToPrincipal(uint256 amount1, uint256 amount2) { + env e; + uint128 principal1 = amountToPrincipal(e, amount1); + uint128 principal2 = amountToPrincipal(e, amount2); + + assert amount1 >= amount2 => principal1 >= principal2; +} + +/** + * We have learned at least that the return value of mint doesn't necessarily + * reflect the amount minted if the principal to mint is less than INDEX_BASE_UNIT + * + * @status timeout + * @notice passing in harness + */ +rule inverseOfMintAndBurn(address a, uint256 p) { + env e1; + env e2; + calldataarg args; + + uint128 indexBase = indexBaseUnit(); + uint128 cashIndex = getCashIndex(e1, args); + + uint256 startBalance = balanceOf(e1, a); + uint128 startPrincipal = cashPrincipal(a); + uint256 amountMinted = mint(e1, a, p); + uint256 principalMinted = amountToPrincipal(e1, amountMinted); + // DANGER DANGER: HIGH VOLTAGE! + // pretty big assumption here + require principalMinted == p; + uint256 intermediateBalance = balanceOf(e2, a); + uint256 intermediatePrincipal = cashPrincipal(a); + uint128 principalBurned = burn(e2, a, amountMinted); + uint256 endBalance = balanceOf(e2, a); + uint128 endPrincipal = cashPrincipal(a); + + assert intermediatePrincipal >= startPrincipal; + assert startPrincipal == endPrincipal; + assert startBalance == endBalance; + assert principalBurned == p; +// assert false; +} + +/** + * Checks that if the sender is not starport, that none of + * cashYieldAndIndex and nextCashYieldAndIndex are characterizeModifyIndex + * + * @notice seems like there's no reason not to put an admin check on initialize + * @status passing except initialize + */ +rule onlyStarportModifyYieldAndIndex(method f) { + address starport = admin(); + + env e; + calldataarg args; + require e.msg.sender != starport; + + uint128 startYield; + uint128 startIndex; + uint128 startNextYield; + uint128 startNextIndex; + startYield, startIndex = cashYieldAndIndex(); + startNextYield, startNextIndex = nextCashYieldAndIndex(); + + f(e, args); + + uint128 endYield; + uint128 endIndex; + uint128 endNextYield; + uint128 endNextIndex; + endYield, endIndex = cashYieldAndIndex(); + endNextYield, endNextIndex = nextCashYieldAndIndex(); + + assert startYield == endYield && + startIndex == endIndex && + startNextYield == endNextYield && + startNextIndex == endNextIndex; +} + +/** + * @ERC20 + * - looking at the code, I would expect this rule to fail + * is this expected behavior? + * - diff, REMOVE: require from != 0 + * @status failing + */ +cannotApproveNonZeroWhenCurrentlyNonZero(env e, address spender, uint256 value) +description "Approve succeeded even though current allowance is non-zero and value is non-zero" +{ + address from = e.msg.sender; + require value != 0; + uint256 currentAllowance = allowance(e,from,spender); + require currentAllowance != 0; + + bool result = approve@withrevert(e, spender, value); + bool reverted = lastReverted; // loading transferReverted + + assert reverted || !result, "Approve succeeded even though value is non-zero and current allowance is non-zero"; +} + +/** + * @ERC20 + * @status passing + */ +approveStandardPrecondition(env e, address spender, uint256 value) +description "Approve failed even though current allowance is 0" +{ + // require e.msg.value == 0; // not necessary because enforced by call to allowance. + + address from = e.msg.sender; + require from != 0; // checked in zeroCannotApprove + require spender != 0; // checked in cannotApproveToZeroSpender + bool precondition = sinvoke allowance(e,from,spender) == 0; + + require precondition; + + bool result = invoke approve(e, spender, value); + bool reverted = lastReverted; // loading transferReverted + + assert !reverted && result, "approve failed even though meets precondition"; +} + +/** + * @ERC20 + * - diff remove require to != 0 + * @notice try with principal instead of balance + * @notice timeout with harness + */ +transferCheckPreconds(env e, address to, uint256 value) +{ + require to != 0; + require value != 0; + + address from = e.msg.sender; + bool precondition = balanceOf(e, from) >= value; + + bool result = transfer@withrevert(e, to, value); + bool transferReverted = lastReverted; // loading transferReverted + + // The transfer function must meet the precondition, or to revert. + assert !precondition => (transferReverted || !result), "If transfer() precondition does not hold, must either revert or return 0"; +} + +/** + * @ERC20 + * @status violated here but timeout in harness + */ +transferCheckEffects(env e, address to, uint256 value) +{ + require to != 0; + require value != 0; + + address from = e.msg.sender; + uint256 origBalanceOfFrom = balanceOf(e, from); + uint256 origBalanceOfTo = balanceOf(e, to); + bool result = transfer(e, to, value); + + // Start checking the effects + env e2; + require e2.block.timestamp >= e.block.timestamp && e2.block.number >= e.block.number; // Checking new balance in new, later environment + uint256 newBalanceOfTo = sinvoke balanceOf(e, to); // loading new balance of recipient + uint256 newBalanceOfFrom = sinvoke balanceOf(e, from); + + // Compute the expected new balance. + uint expectedNewBalanceOfTo; + uint expectedNewBalanceOfFrom; + if (from != to && result) { + require expectedNewBalanceOfTo == origBalanceOfTo + value; + require expectedNewBalanceOfFrom == origBalanceOfFrom - value; + } else { + require expectedNewBalanceOfTo == origBalanceOfTo; + require expectedNewBalanceOfFrom == origBalanceOfFrom; + } + + // Effects: new balance of recipient is as expected, and it should also be not less than the original balance + assert newBalanceOfTo == expectedNewBalanceOfTo && newBalanceOfTo >= origBalanceOfTo, "invalid new balance of to"; + assert newBalanceOfFrom == expectedNewBalanceOfFrom && newBalanceOfFrom <= origBalanceOfFrom, "invalid new balance of from"; +} + +/** + * @notice we don't care right? + */ +transferForIllegalRecipient +description "Checked implementation permits sending to the 0 address via the transfer function." +good_description "Checked implementation does not permit sending funds to the 0 address via the transfer function." +{ + env e; + + uint256 origBalanceOf0 = sinvoke balanceOf(e, 0); + + uint256 value; + require value > 0; // zero tokens sent to 0 are less 'interesting' since there is no real effect + + invoke transfer(e, 0, value); + + uint256 newBalanceOf0 = sinvoke balanceOf(e, 0); + + assert newBalanceOf0 == origBalanceOf0, "Transfer to 0 changed the balance of 0 --> it is allowed"; +} + +/** + * @ERC20 + * @status timeout + * @notice passing in harness + */ +transferImpactOthers(env e, address to, uint256 value, address other) +description "Unexpected effect of transfer (sender=${e.msg.sender} to=$to value=${value}): +should not change the balance of $other from $origBalanceOfOther to $newBalanceOfOther." +good_description "An invocation of transfer can potentially only affect the balances of sender and recipient." +{ + require e.msg.sender != other && other != to; + + uint256 origBalanceOfOther = sinvoke balanceOf(e,other); + + invoke transfer(e,to,value); + + env e2; + require e2.block.number >= e.block.number; + + uint256 newBalanceOfOther = sinvoke balanceOf(e2, other); + assert newBalanceOfOther == origBalanceOfOther; +} + +/** + * @ERC20 + * @status passing + */ +unexpectedAllowanceChange(method f, address tokenOwner, address spender) +description "Function $f, which is not transferFrom or approve, +should not change allowance of token admin $tokenOwner to spender $spender +from $origSpenderAllowance to $newSpenderAllowance." +{ + env e; + uint256 origSpenderAllowance = sinvoke allowance(e, tokenOwner, spender); + + calldataarg arg; + require f.selector != transferFrom(address,address,uint256).selector && f.selector != approve(address,uint256).selector; + env ef; + invoke f(ef, arg); + + env e2; + require e2.block.number >= e.block.number; + + uint256 newSpenderAllowance = sinvoke allowance(e2, tokenOwner, spender); + assert newSpenderAllowance == origSpenderAllowance; +} + +/** + * @ERC20 + * @status last run failed + */ +unexpectedTotalSupplyChange(method f, address targetAddress) +description "Function $f should not change total supply from $origTotalSupply to $newTotalSupply." +{ + env e; + uint256 origTotalSupply = sinvoke totalSupply(e); + + calldataarg arg; + + require f.selector != burn(address,uint256).selector && f.selector != mint(address,uint128).selector; + env ef; + invoke f(ef, arg); + + env e2; + require e2.block.number > e.block.number; + + uint256 newTotalSupply = sinvoke totalSupply(e2); + + /* some implementations subtracts balance of address(0) and this will have to be accounted for. + This particular test assumes that totalSupply is only updated from mint, burn. + */ + assert newTotalSupply == origTotalSupply; +} + +/** + * @ERC20 + * @status timeout + * @notice passing in harness + */ +unexpectedApproveImpact(env e, address spender, uint256 value, address x, address y, address z) +description "approve by ${e.msg.sender} to spender $spender with value $value should update allowance of sender to spender, and nothing else. +Consider checking balance of x=$x or allowance from y=$y to z=$z." +{ + // Load everything that should not change + uint256 origBalanceOfX = sinvoke balanceOf(e, x); + uint256 origAllowanceYZ = sinvoke allowance(e, y, z); + uint256 origTotalSupply = sinvoke totalSupply(e); + + bool retVal = invoke approve(e,spender, value); + bool approveInvocationReverted = lastReverted; + + env e2; + require e2.block.number >= e.block.number; + + // load new allowance that should be updated + uint256 newAllowanceOfSpender = sinvoke allowance(e2,e.msg.sender,spender); + + // load new values that should stay the same + uint256 newBalanceOfX = sinvoke balanceOf(e2, x); + uint256 newAllowanceYZ = sinvoke allowance(e2, y, z); + uint256 newTotalSupply = sinvoke totalSupply(e2); + + bool correctEffectOnSpender = approveInvocationReverted || !retVal || newAllowanceOfSpender == value; + bool sameTotalSupply = newTotalSupply == origTotalSupply; + bool sameBalanceOfX = newBalanceOfX == origBalanceOfX; + bool sameAllowanceYZ = y == e.msg.sender && z == spender || newAllowanceYZ == origAllowanceYZ; + assert correctEffectOnSpender && sameTotalSupply && sameBalanceOfX && sameAllowanceYZ; +} + +/** + * @ERC20 + * @status passing + */ +approveMustBeAuthorized(env e, method f, address _admin, address spender) +description "Unallowed approval (increase of allowances) for $a" +{ + calldataarg arg; + + env e0; + uint256 origAllowance = sinvoke allowance(e0, _admin, spender); + + invoke f(e, arg); + + uint256 newAllowance = sinvoke allowance(e0, _admin, spender); + + assert (newAllowance > origAllowance) => e.msg.sender == _admin; +} + +// Basic mint test +/** + * @ERC20 + * @status failing (as expected) + */ +noUnlimitedMintingByOwner +description "The admin may at some stage fail to mint before reaching MAX_UINT -> contract contains conditions to limit minting." +{ + uint256 MAXINT = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF; + env e; + uint256 origTotalSupply = sinvoke totalSupply(e); + + address _admin = sinvoke admin(); + + uint256 amount; + require amount > 0; + + require origTotalSupply + amount <= MAXINT; // it is still possible to increase total supply + + address receiver; + + env e2; + require e2.msg.sender == _admin && e2.block.number >= e.block.number; + + invoke mint(e2, receiver, amount); + bool mintReverted = lastReverted; + + uint256 newTotalSupply = sinvoke totalSupply(e2); + + assert newTotalSupply > origTotalSupply; +} + +/** + * @ERC20 + * @status timeout + * @notice failing (as expected) in harness + */ +noUnlimitedMintingByOwner2 +description "The admin may at some stage fail to mint before reaching MAX_UINT -> contract contains conditions to limit minting." +{ + uint256 MAXINT = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF; + env e; + uint256 origTotalSupply = sinvoke totalSupply(e); + + address _admin = sinvoke admin(); + + uint256 amount; + require amount > 0; + + require origTotalSupply + amount <= MAXINT; // it is still possible to increase total supply + + address receiver; + require sinvoke balanceOf(e,receiver) + amount <= MAXINT; + + env e2; + require e2.msg.sender == _admin && e2.block.number >= e.block.number; + + invoke mint(e2, receiver, amount); + bool mintReverted = lastReverted; + + uint256 newTotalSupply = sinvoke totalSupply(e2); + + assert newTotalSupply > origTotalSupply; +} + +/*********************** + * Characterizations * + ***********************/ + +/** + * @ERC20 + * @status failing + */ +transferWithIllegalValue +description "Checked implementation permits a transfer of zero tokens." +good_description "Checked implementation does not permit a transfer of zero tokens." +{ + env e; + address to; + require to != 0; + + require e.msg.value == 0; + bool res = invoke transfer(e, to, 0); + + assert lastReverted || !res; +} + +/** + * @ERC20 + * @status failing (as expected): transfer may revert + */ +transferMayThrow +description "Checked implementation for transfer may revert." +good_description "Checked implementation for transfer never reverts." +{ + env e; + require e.msg.value == 0; // transfer is non payable, so this is the only precondition. + + // calldataarg arg; + // invoke transfer(e, arg); + address a; + uint256 v; + invoke transfer(e, a, v); + + assert !lastReverted; +} + +/** + * @ERC20 + * @status passing: transfer will never return false + */ +transferMayReturnFalse +description "Checked implementation for transfer may return false (0) and not due to a revert." +good_description "Checked implementation for transfer always returns `true` when not reverting." +{ + env e; + calldataarg arg; + + bool ret = sinvoke transfer(e, arg); + + assert ret; +} + +/** + * @ERC20 + * @status passing: transferFrom will never return false + */ +transferFromMayReturnFalse +description "Checked implementation for transferFrom may return false (0) and not due to a revert." +good_description "Checked implementation for transferFrom always returns `true` when not reverting." +{ + env e; + calldataarg arg; + + bool ret = sinvoke transferFrom(e, arg); + + assert ret; +} + +/** + * @ERC20 + * @status failing: balanceOf may revert + * @notice also failing in harness, looks like an uninterp division problem + */ +balanceOfShouldNotRevert +description "balanceOf function may revert" +{ + env e; + calldataarg arg; + + require e.msg.value == 0; + invoke balanceOf(e, arg); + + assert !lastReverted; +} + +/** + * @ERC20 + * @status passing + */ +allowanceShouldNotRevert +description "allowance function may revert" +{ + env e; + address owner; + address spender; + + require e.msg.value == 0; + invoke allowance(e, owner, spender); + + assert !lastReverted; +} + +/** + * Provides a "characterization" of which methods modify the yield + * field of cashYieldAndIndex + */ +rule characterizeModifyYield(method f) { + address starport = admin(); + + env e; + calldataarg args; + require e.msg.sender == starport; + + uint128 startYield; + startYield, _ = cashYieldAndIndex(); + f(e, args); + uint128 endYield; + endYield, _ = cashYieldAndIndex(); + assert startYield == endYield; +} + +/** + * Provides a "characterization" of which methods modify the index + * field of cashYieldAndIndex + */ +rule characterizeModifyIndex(method f) { + address starport = admin(); + env e; + calldataarg args; + require e.msg.sender == starport; + + uint128 startIndex; + _, startIndex = cashYieldAndIndex(); + + f(e, args); + + uint128 endIndex; + _, endIndex = cashYieldAndIndex(); + assert startIndex == endIndex; +} + +/** + * Provides a "characterization" of which methods modify the yield + * field of nextCashYieldAndIndex + */ +rule characterizeModifyNextYield(method f) { + address starport = admin(); + env e; + calldataarg args; + require e.msg.sender == starport; + + uint128 startNextYield; + startNextYield, _ = nextCashYieldAndIndex(); + + f(e, args); + + uint128 endNextYield; + endNextYield, _ = nextCashYieldAndIndex(); + + assert startNextYield == endNextYield; +} + +/** + * Provides a "characterization" of which methods modify the index + * field of nextCashYieldAndIndex + */ +rule characterizeModifyNextIndex(method f) { + address starport = admin(); + env e; + calldataarg args; + require e.msg.sender == starport; + + uint128 startNextIndex; + _, startNextIndex = nextCashYieldAndIndex(); + + f(e, args); + + uint128 endNextIndex; + _, endNextIndex = nextCashYieldAndIndex(); + + assert startNextIndex == endNextIndex; +} + +/** + * An attempt to characterize reasonable preconditions to amountToPrincipal() to help + * figure out transferStandardPrecondition + */ +rule amountToPrincipalCharacterizeRevert(uint256 amount) { + env e; + require e.msg.value == 0; + require amount * indexBaseUnit@norevert() < MAX_UINT128(); + amountToPrincipal@withrevert(e, amount); + assert !lastReverted; +} \ No newline at end of file diff --git a/certora/spec/CashTokenHarness.spec b/certora/spec/CashTokenHarness.spec new file mode 100644 index 000000000..eb4d7c03e --- /dev/null +++ b/certora/spec/CashTokenHarness.spec @@ -0,0 +1,804 @@ +methods { + totalCashPrincipal() returns (uint256) envfree; + amountToPrincipal(uint256) returns (uint128); + admin() returns (address) envfree; + indexBaseUnit() returns (uint256) envfree; + transfer(address,uint256); + cashYieldAndIndex() returns (uint128,uint128) envfree; + nextCashYieldAndIndex() returns (uint128,uint128) envfree; + balanceOf(address) returns (uint256); + cashPrincipal(address) returns (uint128) envfree; + burn(address,uint256) returns (uint128); + mint(address,uint128) returns (uint256); +} + +definition MAX_UINT256() returns uint256 = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff; +definition MAX_UINT128() returns uint256 = 0xffffffffffffffffffffffffffffffff; +definition MAX_ADDRESS() returns uint256 = 0xffffffffffffffffffffffffffffffffffffffff; +// MAX_UINT128 / 1e18 +definition MAX_AMOUNT() returns uint256 = 340282366920938487808; +// 1e18 +definition INDEX_BASE_UNIT() returns uint256 = 1000000000000000000; + +/** x and y are almost equal; y may be _smaller or larger_ than x up to an amount of epsilon */ +definition bounded_error_eq(uint x, uint y, uint epsilon) returns bool = x <= y + epsilon && x + epsilon >= y; +/** x and y are almost equal; y may be _smaller_ than x up to an amount of epsilon */ +definition only_slightly_larger_than(uint x, uint y, uint epsilon) returns bool = y <= x && x <= y + epsilon; +/** x and y are almost equal; y may be _larger_ than x up to an amount of epsilon */ +definition only_slightly_smaller_than(uint x, uint y, uint epsilon) returns bool = x <= y && y <= x + epsilon; + +/** + * A ghost function that shadows the storage variable totalCashPrincipal + */ +ghost principal() returns uint256; +ghost ghostCalculateIndex(uint128, uint128, uint256, uint256) returns uint128 { + axiom forall uint128 yield. forall uint128 index. forall uint256 start. forall uint256 timestamp. ghostCalculateIndex(yield, index, start, timestamp) == 1000000000000000000; +} + +ghost ghostCalculatePrincipal(uint256, uint128) returns uint128 { + axiom forall uint256 amount1. forall uint256 amount2. forall uint128 index. + amount1 >= amount2 => ghostCalculatePrincipal(amount1, index) >= ghostCalculatePrincipal(amount2, index); + axiom forall uint256 amount. forall uint128 index. ghostCalculatePrincipal(amount, index) <= 0xffffffffffffffffffffffffffffffff; +} + +/** + * We use a hook to define principal as the sum of all entries inside cashPrincipal + */ +hook Sstore cashPrincipal[KEY address _] uint128 balance (uint128 old_balance) STORAGE { + require old_balance <= principal(); + require balance <= MAX_UINT128(); + require old_balance <= MAX_UINT128(); + havoc principal assuming principal@new() == principal@old() + (balance - old_balance); + require principal() <= MAX_UINT256(); +} + +hook Sload uint128 calculatedIndex uninterpIndexCalc[KEY uint128 yield][KEY uint128 index][KEY uint256 start][KEY uint256 timestamp] STORAGE { + require ghostCalculateIndex(yield, index, start, timestamp) == calculatedIndex; +} + +hook Sload uint128 calculatedPrincipal uninterpPrincipalCalc[KEY uint256 amount][KEY uint128 index] STORAGE { + require ghostCalculatePrincipal(amount, index) == calculatedPrincipal; +} + +hook Sstore uninterpPrincipalCalc[KEY uint256 amount][KEY uint128 index] uint128 calculatedPrincipal STORAGE { + havoc ghostCalculatePrincipal assuming (forall uint256 a. forall uint128 i. (a != amount || i != index) => + ghostCalculatePrincipal@new(a, i) == ghostCalculatePrincipal@old(a, i)) && + ghostCalculatePrincipal@new(amount, index) == calculatedPrincipal; +} + +/** + * Using the ghost principal (defined to be the sum of entries inside cashPrincipal) + * we prove the invariant that totalCashPrincipal == principal and so it is also an + * invariant that totalCashPrincipal the sum of entries inside cashPrincipal + */ +rule integrityOfTotalCashPrincipal(method f) { + env e; + calldataarg args; + require totalCashPrincipal() == principal(); + f(e, args); + assert totalCashPrincipal() == principal(); +} + +// sanity check for axioms +rule monotonicityOfAmountToPrincipal(uint256 amount1, uint256 amount2, uint256 ghostPrincipal1, uint256 ghostPrincipal2) { + env e; + uint128 principal1 = amountToPrincipal(e, amount1); + uint128 principal2 = amountToPrincipal(e, amount2); + + assert amount1 >= amount2 => principal1 >= principal2; +} + +rule cantTransferMoreThanPrincipal(address account, uint256 amount) { + env e; + uint128 principal = amountToPrincipal(e, amount); + uint128 accountPrincipal = cashPrincipal(e.msg.sender); + require principal > accountPrincipal; + bool result = transfer@withrevert(e, account, amount); + assert lastReverted || !result; +} + +/** + * We have learned at least that the return value of mint doesn't necessarily + * reflect the amount minted if the principal to mint is less than INDEX_BASE_UNIT + * + * @status passing + */ +rule inverseOfMintAndBurn(address a, uint256 p) { + env e1; + env e2; + calldataarg args; + + uint128 indexBase = indexBaseUnit(); + uint128 cashIndex = getCashIndex(e1, args); + + uint256 startBalance = balanceOf(e1, a); + uint128 startPrincipal = cashPrincipal(a); + uint256 amountMinted = mint(e1, a, p); + uint256 principalMinted = amountToPrincipal(e1, amountMinted); + // DANGER DANGER: HIGH VOLTAGE! + // pretty big assumption here + require principalMinted == p; + uint256 intermediateBalance = balanceOf(e2, a); + uint256 intermediatePrincipal = cashPrincipal(a); + uint128 principalBurned = burn(e2, a, amountMinted); + uint256 endBalance = balanceOf(e2, a); + uint128 endPrincipal = cashPrincipal(a); + + assert intermediatePrincipal >= startPrincipal; + assert startPrincipal == endPrincipal; + assert startBalance == endBalance; + assert principalBurned == p; +// assert false; +} + +/** + * An attempt to characterize reasonable preconditions to amountToPrincipal() to help + * figure out transferStandardPrecondition + * @status passing + */ +rule amountToPrincipalCharacterizeRevert(uint256 amount) { + env e; + require e.msg.value == 0; + require amount * indexBaseUnit@norevert() < MAX_UINT128(); + amountToPrincipal@withrevert(e, amount); + assert !lastReverted; +} + +/** + * @ERC20 + * - diff change balanceOf(e, to) + value <= MAX_UINT256() + * becomes (balanceOf(e, to) + value) * indexBaseUnit + (indexBaseUnit - 1) < MAX_UINT128() + * 1. type is uint128 + * 2. underlying principal is uint128 + division truncation with indexBaseUnit conversion + * - diff add require from != to + * - diff remove require to != 0 + * - Will time out if calculateIndex is not summarized + * preconditions checked - no pause + * @status passing + */ +transferStandardPrecondition(env e, address to, uint128 value) +description "Transfer failed even though to != 0, value > 0, balances match" +{ + require value > 0; + address from = e.msg.sender; + require from != to; + + uint256 fromBalance = balanceOf(e, from); + uint256 toBalance = balanceOf(e, to); + uint256 indexBase = indexBaseUnit(); + uint256 truncationDiscrepancy = indexBase - 1; + + bool precondition = fromBalance > value && (toBalance + value) * indexBase + truncationDiscrepancy < MAX_UINT128(); + require precondition; + + bool result = transfer@withrevert(e, to, value); + bool transferReverted = lastReverted; + + assert !transferReverted && result; +} + +/** + * @ERC20 + * - diff change value <= MAX_UINT256() becomes value < MAX_UINT128() + * 1. type is uint128 + * 2. amountToPrincipal() requires strict inequality + * - diff add require from != to + * - diff remove require to != 0 + * - diff remove require from != 0 + * - Will time out if calculateIndex is not summarized + * @status passing (check?) + */ +transferFromStandardPrecondition(env e, address from, address to, uint256 value) +description "TransferFrom failed even though to != 0, value > 0, balances match, allowance suffices" +{ + require value > 0; + require from != to; + require e.msg.value == 0; // is this an okay precondition? + + address spender = e.msg.sender; + require spender != 0; // checked in cannotTransferFromWithSpenderZero + uint256 fromBalance = balanceOf(e, from); + uint256 toBalance = balanceOf(e, to); + uint256 indexBase = indexBaseUnit(); + uint256 truncationDiscrepancy = indexBase - 1; + bool precondition = balanceOf(e, from) >= value && (toBalance + value) * indexBase + truncationDiscrepancy < MAX_UINT128() && allowance(e,from,spender) >= value && from != to; + + require precondition; + + bool result = transferFrom@withrevert(e, from, to, value); + bool transferReverted = lastReverted; + + assert !transferReverted && result; +} + +/** + * @ERC20 + * - diff remove require to != 0 + * @status timeout + */ +transferCheckPreconds(env e, address to, uint256 value) +{ + require value != 0; + + address from = e.msg.sender; + bool precondition = balanceOf(e, from) >= value; + + bool result = transfer@withrevert(e, to, value); + bool transferReverted = lastReverted; // loading transferReverted + + // The transfer function must meet the precondition, or to revert. + assert !precondition => (transferReverted || !result), "If transfer() precondition does not hold, must either revert or return 0"; +} + +/** + * @ERC20 + * @status timeout + * @notice try with principal instead of balance + */ +transferCheckEffects(env e, address to, uint256 value) +{ + require to != 0; + require value != 0; + + address from = e.msg.sender; + uint256 origBalanceOfFrom = balanceOf(e, from); + uint256 origBalanceOfTo = balanceOf(e, to); + bool result = transfer(e, to, value); + + // Start checking the effects + env e2; + require e2.block.timestamp >= e.block.timestamp && e2.block.number >= e.block.number; // Checking new balance in new, later environment + uint256 newBalanceOfTo = sinvoke balanceOf(e, to); // loading new balance of recipient + uint256 newBalanceOfFrom = sinvoke balanceOf(e, from); + + // Compute the expected new balance. + uint expectedNewBalanceOfTo; + uint expectedNewBalanceOfFrom; + if (from != to && result) { + require expectedNewBalanceOfTo == origBalanceOfTo + value; + require expectedNewBalanceOfFrom == origBalanceOfFrom - value; + } else { + require expectedNewBalanceOfTo == origBalanceOfTo; + require expectedNewBalanceOfFrom == origBalanceOfFrom; + } + + // Effects: new balance of recipient is as expected, and it should also be not less than the original balance + assert newBalanceOfTo == expectedNewBalanceOfTo && newBalanceOfTo >= origBalanceOfTo, "invalid new balance of to"; + assert newBalanceOfFrom == expectedNewBalanceOfFrom && newBalanceOfFrom <= origBalanceOfFrom, "invalid new balance of from"; +} + +/* +// Transfer related tests +transferIncorrectUpdateOfBalanceForLegalRecipient(env e, address to, uint256 value) +-- split to other rules + +*/ + +/** + * @ERC20 + * @status passing + */ +transferImpactOthers(env e, address to, uint256 value, address other) +description "Unexpected effect of transfer (sender=${e.msg.sender} to=$to value=${value}): +should not change the balance of $other from $origBalanceOfOther to $newBalanceOfOther." +good_description "An invocation of transfer can potentially only affect the balances of sender and recipient." +{ + require e.msg.sender != other && other != to; + + uint256 origBalanceOfOther = sinvoke balanceOf(e,other); + + invoke transfer(e,to,value); + + env e2; + require e2.block.number >= e.block.number; + + uint256 newBalanceOfOther = sinvoke balanceOf(e2, other); + assert newBalanceOfOther == origBalanceOfOther; +} + +/** + * @ERC20 + * @status timeout + */ +transferUnexpectedBalanceChange(env e, address to, uint256 value) +description "A transfer (sender=${e.msg.sender} to=$to value=${value}) changed balances in an unexpected way. +Original balance of sender $balanceOfFrom updated to $updatedBalanceOfFrom. +Original balance of to $balanceOfTo updated to $updatedBalanceOfTo." +good_description "An invocation of transfer may only increase recipient's balance only and decrease sender's balance." +{ + uint256 balanceOfFrom = sinvoke balanceOf(e, e.msg.sender); + uint256 balanceOfTo = sinvoke balanceOf(e, to); + + invoke transfer(e,to,value); + + uint256 updatedBalanceOfTo = sinvoke balanceOf(e,to); + uint256 updatedBalanceOfFrom = sinvoke balanceOf(e,e.msg.sender); + + assert updatedBalanceOfTo >= balanceOfTo && updatedBalanceOfFrom <= balanceOfFrom; +} + +/** + * @ERC20 + * @status timeout + */ +transferCappedDebit(env e, address to, uint256 value) +description "A transfer debits more than authorized: debit=$debit, while authorized=$value" +good_description "A transfer cannot debit the sender by more than the passed value." +{ + env e0; + require e0.block.number == e.block.number; + uint256 balanceOfFrom = sinvoke balanceOf(e0, e.msg.sender); + + invoke transfer(e,to,value); + + uint256 updatedBalanceOfFrom = sinvoke balanceOf(e0,e.msg.sender); + + uint256 debit = balanceOfFrom-updatedBalanceOfFrom; + assert debit <= value; +} + + +// Higher-order tests +/** + * @ERC20 + * @status passing + */ +unexpectedBalanceChangeExtendedAPI(method f, address targetAddress) +description "Function $f, which is not transferFrom, transfer, mint or burn, +should not change balanceOf of targetAddress=$targetAddress +from $origBalanceOfTarget to $newBalanceOfTarget." +{ + env e; + uint256 origBalanceOfTarget = sinvoke balanceOf(e, targetAddress); + + calldataarg arg; + require f.selector != transferFrom(address,address,uint256).selector && f.selector != transfer(address,uint256).selector && f.selector != burn(address,uint256).selector && f.selector != mint(address,uint128).selector; + env ef; + invoke f(ef, arg); + + env e2; + require e2.block.number >= e.block.number; + + uint256 newBalanceOfTarget = sinvoke balanceOf(e2, targetAddress); + + assert newBalanceOfTarget == origBalanceOfTarget; +} + +/** + * @ERC20 + * @status passing: most + * violated: burn, mint + * timeout: transfer + */ +senderCanOnlyReduceHerOwnBalance( method f, address sender, address other) +description "Sender $sender calling method $f (not transferFrom) should only reduce her own balance and not other's. +But other's $other balance updated from $origBalanceOfOther to $newBalanceOfOther." +{ + env e; + require other != sender; + uint256 origBalanceOfOther = sinvoke balanceOf(e, other); + + calldataarg arg; + env ef; + require ef.msg.sender == sender; + require f.selector != transferFrom(address,address,uint256).selector; + invoke f(ef, arg); + + env e2; + require e2.block.number >= e.block.number; + + uint256 newBalanceOfOther = sinvoke balanceOf(e2, other); + + assert newBalanceOfOther >= origBalanceOfOther; +} + +/** + * @ERC20 modified + * @status passing: most + * timeout: burn + */ +senderCanOnlyReduceHerOwnPrincipal( method f, address sender, address other) +description "Sender $sender calling method $f (not transferFrom) should only reduce her own balance and not other's. +But other's $other balance updated from $origBalanceOfOther to $newBalanceOfOther." +{ + env e; + require other != sender; + uint256 origBalanceOfOther = sinvoke cashPrincipal(other); + + calldataarg arg; + env ef; + require ef.msg.sender == sender; + require f.selector != transferFrom(address,address,uint256).selector; + invoke f(ef, arg); + + env e2; + require e2.block.number >= e.block.number; + + uint256 newBalanceOfOther = sinvoke cashPrincipal(other); + + assert newBalanceOfOther >= origBalanceOfOther; +} + +/** + * @ERC20 + * @status passing: most + * violated: burn, transfer, transferFrom + * timeout: mint + */ +senderCanOnlyReduceHerOwnBalanceUnlessAllowanceAllowsIt( method f, address sender, address other) +description "Sender $sender calling method $f (not transferFrom) should only reduce her own balance and not other's. +But other's $other balance updated from $origBalanceOfOther to $newBalanceOfOther." +{ + env e; + require other != sender; + uint256 origBalanceOfOther = sinvoke balanceOf(e, other); + + uint256 origAllowance = sinvoke allowance(e, other, sender); + + calldataarg arg; + env ef; + require ef.msg.sender == sender; + invoke f(ef, arg); + + env e2; + require e2.block.number >= e.block.number; + + uint256 newBalanceOfOther = sinvoke balanceOf(e2, other); + + assert newBalanceOfOther >= origBalanceOfOther || origAllowance >= origBalanceOfOther-newBalanceOfOther; +} + +/** + * @ERC20 modified + * @status passing: most + * timeout: burn + */ +senderCanOnlyReduceHerOwnPrincipalUnlessAllowanceAllowsIt( method f, address sender, address other) +description "Sender $sender calling method $f (not transferFrom) should only reduce her own balance and not other's. +But other's $other balance updated from $origBalanceOfOther to $newBalanceOfOther." +{ + env e; + require other != sender; + uint256 origBalanceOfOther = sinvoke cashPrincipal(other); + + uint256 origAllowance = amountToPrincipal(e, allowance(e, other, sender)); + + calldataarg arg; + env ef; + require ef.msg.sender == sender; + invoke f(ef, arg); + + env e2; + require e2.block.number >= e.block.number; + + uint256 newBalanceOfOther = sinvoke cashPrincipal(other); + + assert newBalanceOfOther >= origBalanceOfOther || origAllowance >= origBalanceOfOther-newBalanceOfOther; +} + +/** + * @ERC20 + * @status passing + */ +unexpectedTotalSupplyChange(method f, address targetAddress) +description "Function $f should not change total supply from $origTotalSupply to $newTotalSupply." +{ + env e; + uint256 origTotalSupply = sinvoke totalSupply(e); + + calldataarg arg; + + require f.selector != burn(address,uint256).selector && f.selector != mint(address,uint128).selector; + env ef; + invoke f(ef, arg); + + env e2; + require e2.block.number > e.block.number; + + uint256 newTotalSupply = sinvoke totalSupply(e2); + + /* some implementations subtracts balance of address(0) and this will have to be accounted for. + This particular test assumes that totalSupply is only updated from mint, burn. + */ + assert newTotalSupply == origTotalSupply; +} + +// Characterizing totalSupply +/** + * @ERC20 + * @status not tested + * @notice we don't care right? + */ +totalSupplyDoesNotIncludeBalanceOfZeroCheckWithTransferToZero(uint256 expectedChange) +description "function totalSupply does not include the balance of the zero address: +When transferring $expectedChange tokens to the zero address, totalSupply was deducted that amount" +/* + If the contract does not allow sending to zero address, there must be some other functionality (like burn) that can be used to check for that behavior. + */ +{ + env e; + + uint256 origTotalSupply = sinvoke totalSupply(e); + + // now, transfer to zero a positive number of tokens, require it to succeed. + require expectedChange > 0; + + sinvoke transfer(e, 0, expectedChange); + + env e2; + uint256 newTotalSupply = sinvoke totalSupply(e2); + + assert newTotalSupply != origTotalSupply - expectedChange; +} + +// TransferFrom related tests + +/** + * @ERC20 + * @status timeout + */ +transferFromWrongBalanceOrAllowanceChanges_0(env e, address from, address to, uint256 value) +description "transferFrom (from = $from, to = $to, by ${e.msg.sender}, value = $value) did not update participants balances and allowances as expected." +{ + address caller = e.msg.sender; + uint256 origBalanceOfFrom = sinvoke balanceOf(e, from); + uint256 origBalanceOfTo = sinvoke balanceOf(e, to); + uint256 origAllowance = sinvoke allowance(e, from, caller); + + bool precondition = origBalanceOfFrom >= value && origAllowance >= value; + + bool result = invoke transferFrom(e, from, to, value); + bool transferFromReverted = lastReverted; + // The transferFrom function must meet the precondition, or to revert. + assert precondition || (transferFromReverted || !result); +} + +/** + * @ERC20 + * @status timeout + */ +transferFromWrongBalanceOrAllowanceChanges(env e, address from, address to, uint256 value) +description "transferFrom (from = $from, to = $to, by ${e.msg.sender}, value = $value) did not update participants balances and allowances as expected." +{ + address caller = e.msg.sender; + uint256 origBalanceOfFrom = sinvoke balanceOf(e, from); + uint256 origBalanceOfTo = sinvoke balanceOf(e, to); + uint256 origAllowance = sinvoke allowance(e, from, caller); + + bool precondition = origBalanceOfFrom >= value && origAllowance >= value; + + bool result = invoke transferFrom(e, from, to, value); + bool transferFromReverted = lastReverted; + // The transferFrom function must meet the precondition, or to revert. + //assert precondition || (transferFromReverted || !result); + + env e2; + require e2.block.number >= e.block.number; + uint256 newBalanceOfFrom = sinvoke balanceOf(e2, from); + uint256 newBalanceOfTo = sinvoke balanceOf(e2, to); + uint256 newAllowance = sinvoke allowance(e2,from, caller); + + bool expectedNewBalanceOfFrom = (((transferFromReverted || !result) || from == to) && newBalanceOfFrom == origBalanceOfFrom) + || (!((transferFromReverted || !result) || from == to) && newBalanceOfFrom == origBalanceOfFrom - value); + bool expectedNewBalanceOfTo = (((transferFromReverted || !result) || from == to) && newBalanceOfTo == origBalanceOfTo) + || (!((transferFromReverted || !result) || from == to) && newBalanceOfTo == origBalanceOfTo + value); + bool expectedNewAllowance = ((transferFromReverted || !result) && newAllowance == origAllowance) + || (!(transferFromReverted || !result) && newAllowance == (origAllowance - value)); + + + bool newFromBalanceChanged = (sinvoke balanceOf(e2, from) == origBalanceOfFrom - value); + bool newToBalanceChanged = (sinvoke balanceOf(e2, to) == origBalanceOfTo + value); + bool newAllowanceChanged = (sinvoke allowance(e2, from, caller) == origAllowance - value); + + assert expectedNewBalanceOfFrom && expectedNewBalanceOfTo && expectedNewAllowance; +} + +/** + * @notice we don't care right? + */ +transferFromWithIllegalRecipient +description "transferFrom permits sending to zero address." +{ + env e; + address from; + uint256 value; + + uint256 origBalanceOfFrom = sinvoke balanceOf(e, from); + uint256 origAllowance = sinvoke allowance(e, from, e.msg.sender); + + require origBalanceOfFrom >= value && origAllowance >= value; + + invoke transferFrom(e, from, 0, value); + + assert lastReverted; +} + +/** + * @ERC20 + * @status passing + */ +unexpectedTransferFromImpact(env e, address from, address to, uint256 value, address x, address y, address z) +description "transferFrom sender=${e.msg.sender}, from=$from, to=$to, value=$value - should not impact other allowances (e.g. from y=$y to z=$z), balances (e.g. for x=$x), or total supply" +{ + uint256 origBalanceX = sinvoke balanceOf(e,x); + uint256 origAllowanceYZ = sinvoke allowance(e, y, z); + uint256 origTotalSupply = sinvoke totalSupply(e); + + invoke transferFrom(e, from, to, value); + + env e2; + require e2.block.number >= e.block.number; + + uint256 newBalanceX = sinvoke balanceOf(e2, x); + uint256 newAllowanceYZ = sinvoke allowance(e2, y, z); + uint256 newTotalSupply = sinvoke totalSupply(e2); + + bool sameBalanceOfX = x == from || x == to || origBalanceX == newBalanceX; + bool sameAllowanceYZ = (y == from && z == e.msg.sender) || newAllowanceYZ == origAllowanceYZ; + bool sameTotalSupply = origTotalSupply == newTotalSupply; + + assert sameBalanceOfX && sameAllowanceYZ && sameTotalSupply; +} + +/** + * @ERC20 + * @status timeout + */ +transferFromCappedDebit(env e, address from, address to, uint256 value) +description "A transfer debits more than authorized: debit=$debit, while authorized=$value" +{ + env e0; + require e0.block.number == e.block.number; + uint256 balanceOfFrom = sinvoke balanceOf(e0, e.msg.sender); + + invoke transferFrom(e,from,to,value); + + uint256 updatedBalanceOfFrom = sinvoke balanceOf(e0,e.msg.sender); + + mathint debit = balanceOfFrom-updatedBalanceOfFrom; + assert debit <= value; +} + + +// Approve related tests + +/** + * @ERC20 + * @status passing + */ +unexpectedApproveImpact(env e, address spender, uint256 value, address x, address y, address z) +description "approve by ${e.msg.sender} to spender $spender with value $value should update allowance of sender to spender, and nothing else. +Consider checking balance of x=$x or allowance from y=$y to z=$z." +{ + // Load everything that should not change + uint256 origBalanceOfX = sinvoke balanceOf(e, x); + uint256 origAllowanceYZ = sinvoke allowance(e, y, z); + uint256 origTotalSupply = sinvoke totalSupply(e); + + bool retVal = invoke approve(e,spender, value); + bool approveInvocationReverted = lastReverted; + + env e2; + require e2.block.number >= e.block.number; + + // load new allowance that should be updated + uint256 newAllowanceOfSpender = sinvoke allowance(e2,e.msg.sender,spender); + + // load new values that should stay the same + uint256 newBalanceOfX = sinvoke balanceOf(e2, x); + uint256 newAllowanceYZ = sinvoke allowance(e2, y, z); + uint256 newTotalSupply = sinvoke totalSupply(e2); + + bool correctEffectOnSpender = approveInvocationReverted || !retVal || newAllowanceOfSpender == value; + bool sameTotalSupply = newTotalSupply == origTotalSupply; + bool sameBalanceOfX = newBalanceOfX == origBalanceOfX; + bool sameAllowanceYZ = y == e.msg.sender && z == spender || newAllowanceYZ == origAllowanceYZ; + assert correctEffectOnSpender && sameTotalSupply && sameBalanceOfX && sameAllowanceYZ; +} + +// Getters + +// Basic mint test +/** + * @ERC20 + * @status failing (as expected) + */ +noUnlimitedMintingByOwner2 +description "The admin may at some stage fail to mint before reaching MAX_UINT -> contract contains conditions to limit minting." +{ + uint256 MAXINT = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF; + env e; + uint256 origTotalSupply = sinvoke totalSupply(e); + + address _admin = sinvoke admin(); + + uint256 amount; + require amount > 0; + + require origTotalSupply + amount <= MAXINT; // it is still possible to increase total supply + + address receiver; + require sinvoke balanceOf(e,receiver) + amount <= MAXINT; + + env e2; + require e2.msg.sender == _admin && e2.block.number >= e.block.number; + + invoke mint(e2, receiver, amount); + bool mintReverted = lastReverted; + + uint256 newTotalSupply = sinvoke totalSupply(e2); + + assert newTotalSupply > origTotalSupply; +} + +/** + * @ERC20 + * @status failing + * @notice looks like this stems from an over(under?)flow check using division, + * and that division is modeled incorrectly + */ +balanceOfShouldNotRevert +description "balanceOf function may revert" +{ + env e; + address account; + require account <= MAX_ADDRESS(); + + require e.msg.value == 0; + invoke balanceOf(e, account); + + assert !lastReverted; +} + +// Check for privileged operations +privilegedOperation(method f, address privileged) +description "$f can be called by more than one user without reverting" +{ + env e1; + calldataarg arg; + require (e1.msg.sender == privileged); + invoke f(e1, arg); // privileged succeeds executing candidate privileged operation. + bool firstSucceeded = !lastReverted; + + env e2; + calldataarg arg2; + require (e2.msg.sender != privileged); + invoke f(e2, arg2); // unprivileged + bool secondSucceeded = !lastReverted; + + assert !(firstSucceeded && secondSucceeded), "$f can be called by both ${e1.msg.sender} and ${e2.msg.sender}, so it is not privileged"; +} + +smartPrivilegedOperation(method f, address privileged) +description "$f can be called by more than one user without reverting" +{ + env e1; + calldataarg arg; + require (e1.msg.sender == privileged); + storage initialStorage = lastStorage; + invoke f(e1, arg); // privileged succeeds executing candidate privileged operation. + bool firstSucceeded = !lastReverted; + + env e2; + calldataarg arg2; + require (e2.msg.sender != privileged); + invoke f(e2, arg2) at initialStorage; // unprivileged + bool secondSucceeded = !lastReverted; + + assert !(firstSucceeded && secondSucceeded), "$f can be called by both ${e1.msg.sender} and ${e2.msg.sender}, so it is not privileged"; +} + +simplePrivilegedOperation(method f) +description "Function $f is not privileged" +{ + env e; + address o = sinvoke admin(); + + env e2; + require e2.msg.sender != o; + + calldataarg arg; + invoke f(e2,arg); + + assert lastReverted, "$f did not revert even though not called by the admin"; +} \ No newline at end of file diff --git a/certora/spec/Privileged.spec b/certora/spec/Privileged.spec new file mode 100644 index 000000000..6a2a29fe2 --- /dev/null +++ b/certora/spec/Privileged.spec @@ -0,0 +1,22 @@ +definition knownAsNonPrivileged(method f) returns bool = false; + +rule privilegedOperation(method f, address privileged) +description "$f can be called by more than one user without reverting" +{ + env e1; + calldataarg arg; + require !knownAsNonPrivileged(f); + require e1.msg.sender == privileged; + + storage initialStorage = lastStorage; + invoke f(e1, arg); // privileged succeeds executing candidate privileged operation. + bool firstSucceeded = !lastReverted; + + env e2; + calldataarg arg2; + require e2.msg.sender != privileged; + invoke f(e2, arg2) at initialStorage; // unprivileged + bool secondSucceeded = !lastReverted; + + assert !(firstSucceeded && secondSucceeded), "${f.selector} can be called by both ${e1.msg.sender} and ${e2.msg.sender}, so it is not privileged"; +} diff --git a/certora/spec/Starport.spec b/certora/spec/Starport.spec new file mode 100644 index 000000000..67a185618 --- /dev/null +++ b/certora/spec/Starport.spec @@ -0,0 +1,284 @@ +using StarportHarness as starport +using ERC20 as token +using NonStandardERC20 as nonStandardToken +using ExcessiveERC20 as excessiveToken +using CashToken as cashToken + +methods { + starport.eraId() returns (uint256) envfree + starport.admin() returns (address) envfree + starport.cash() returns (address) envfree + starport.supplyCaps(address) returns (uint256) envfree + starport.authorities(uint256) returns (address) envfree + starport.isNoticeInvoked(bytes32) returns (bool) envfree + starport.noticeAlreadyInvoked() returns (bool) envfree + starport.noticeReturnsEmptyString() returns (bool) envfree + starport.signaturesAuthorizedPrecondition(uint256,uint256,bytes32) envfree + starport.checkSignatures(uint256,uint256,bytes32) envfree + starport.hashChainTargetNotParentPrecond(bytes32) envfree + starport.checkNoticeChain(bytes32) envfree + starport.hashChainBrokenLinkPrecond(uint256) envfree + starport.lockTo(uint,address,address) + starport.balanceInERC20Asset(address) envfree + starport.isAssert() returns (bool) envfree + starport.nowAssert() envfree + + cashToken.totalCashPrincipal() returns (uint256) envfree + + transfer(address,uint256) => DISPATCHER(true) + transferFrom(address,address,uint256) => DISPATCHER(true) + balanceOf(address) => DISPATCHER(true) +} + +definition MAX_UINT256() returns uint256 = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff; + +/** + * @title Invoke is Idempotent + * @description Invoking a notice once or twice will result in the same change in state + * @status timeout! (-b 2 and -b 1) + * @notice This is too hard a rule it seems, but alreadyInvoked /\ invokeSetsInvoked /\ + * invokeChainSetsInvoked gives us a similar guarantee + */ +rule invokeChainIdempotent { + env e; + calldataarg args; + uint256 n; + uint256 authority; + address asset; + bytes32 noticeHash; + + storage init_storage = lastStorage; + require !starport.isAssert(); + invoke starport.invokeNoticeChain(e, args); + address authority1 = authorities(authority); + uint256 supplyCap1 = supplyCaps(asset); + sinvoke starport.nowAssert(); + bool invoked1 = starport.invokeNoticeChain(e, args); + uint256 era1 = starport.eraId(); + + bool isAssert = sinvoke starport.isAssert() at init_storage; + invoke starport.invokeNoticeChain(e, args); + invoke starport.invokeNoticeChain(e, args); + address authority2 = starport.authorities(authority); + uint256 supplyCap2 = starport.supplyCaps(asset); + sinvoke starport.nowAssert(); + bool invoked2 = starport.invokeNoticeChain(e, args); + uint256 era2 = starport.eraId(); + + assert era1 == era2; + assert authority1 == authority2; + assert supplyCap1 == supplyCap2; + assert invoked1 == invoked2; +} + +/** + * @status timeout! (-b 2 and -b 1) + */ +rule invokeSetsInvoked { + env e; + calldataarg args; + require starport.isAssert() == false; + sinvoke starport.invokeNotice(e, args); + sinvoke starport.nowAssert(); + assert starport.invokeNotice(e, args); +} + +/** + * @status passing + */ +rule invokeChainSetsInvoked { + env e; + calldataarg args; + require starport.isAssert() == false; + sinvoke starport.invokeNoticeChain(e, args); + sinvoke starport.nowAssert(); + assert starport.invokeNoticeChain(e, args); +} + +/** + * @title Already Invoked Notice Doesn't Change state + * @description If a notice is already invoked, invokeNoticeInternal does not change + * starport state + * @notice I'm not 100% sure cashToken.totalCashPrincipal() is getting the total + * principal of starport.cash()?? @Shelly + * @notice DON'T RUN WITH --CACHE + * @status violated with assert totalCashPrincipal1 == totalCashPrincipal2 + * passing with totalCashPrincipal1 == totalCashPrincipal2 (no cache) + * timeout with asserts about balances + */ +rule alreadyInvoked { + uint256 n; + uint256 authority; + address asset; + bytes32 noticeHash; + require cashToken == starport.cash(); + + address authority1 = authorities(authority); + uint256 supplyCap1 = supplyCaps(asset); + bool invoked1 = isNoticeInvoked(noticeHash); + uint256 era1 = starport.eraId(); + uint256 totalCashPrincipal1 = cashToken.totalCashPrincipal(); +// uint256 cashBalance1 = starport.balanceInERC20Asset(cashToken); +// uint256 tokenBalance1 = starport.balanceInERC20Asset(token); +// uint256 nonStandardTokenBalance1 = starport.balanceInERC20Asset(nonStandardToken); +// uint256 excessiveTokenBalance1 = starport.balanceInERC20Asset(excessiveToken); + + require starport.noticeAlreadyInvoked(); + bool returnsEmptyString = starport.noticeReturnsEmptyString(); + + address authority2 = starport.authorities(authority); + uint256 supplyCap2 = starport.supplyCaps(asset); + bool invoked2 = starport.isNoticeInvoked(noticeHash); + uint256 era2 = starport.eraId(); + uint256 totalCashPrincipal2 = cashToken.totalCashPrincipal(); +// uint256 cashBalance2 = starport.balanceInERC20Asset(cashToken); +// uint256 tokenBalance2 = starport.balanceInERC20Asset(token); +// uint256 nonStandardTokenBalance2 = starport.balanceInERC20Asset(nonStandardToken); +// uint256 excessiveTokenBalance2 = starport.balanceInERC20Asset(excessiveToken); + + assert returnsEmptyString; + assert era1 == era2; + assert authority1 == authority2; + assert supplyCap1 == supplyCap2; + assert invoked1 == invoked2; + assert totalCashPrincipal1 == totalCashPrincipal2; +// assert cashBalance1 == cashBalance2; +// assert tokenBalance1 == tokenBalance2; +// assert nonStandardTokenBalance1 == nonStandardTokenBalance2; +// assert excessiveTokenBalance1 == excessiveTokenBalance2; +} + +/** + * @title Supply Cap Limits Starport Balance in Asset + * @description checks that lockTo reverts if it would cause the balance of starport + * to go above its supply cap + * @notice this rule and indeed assets rely on proper ERC20 behavior (what if transfering allows overflow?) + * @status ? + */ +rule supplyCapLimit(uint amount, address recipient) { + env e; + require token != cash(); + require e.msg.sender != starport; + uint256 startBalance = starport.balanceInERC20Asset(token); + require startBalance + amount > starport.supplyCaps(token); + invoke starport.lockTo(e, amount, token, recipient); + assert lastReverted; +} + +/** + * @title Supply Cap Limits Starport Balance in Asset + * @description checks that lockTo reverts if it would cause the balance of starport + * to go above its supply cap for non-standard ERC20 token + * @notice this rule and indeed assets rely on proper ERC20 behavior (what if transfering allows overflow?) + * @status ? + */ +rule supplyCapLimitNonStandard(uint amount, address recipient) { + env e; + require nonStandardToken != cash(); + require e.msg.sender != starport; + uint256 startBalance = starport.balanceInERC20Asset(nonStandardToken); + require startBalance + amount > starport.supplyCaps(nonStandardToken); + invoke starport.lockTo(e, amount, nonStandardToken, recipient); + assert lastReverted; +} + +/** + * @title Supply Cap Limits Starport Balance in Asset + * @description checks that lockTo reverts if it would cause the balance of starport + * to go above its supply cap for non-standard ERC20 token + * @notice this rule and indeed assets rely on proper ERC20 behavior (what if transfering allows overflow?) + * @status ? + */ +rule supplyCapLimitExcessiveNonStandard(uint amount, address recipient) { + env e; + require excessiveToken != cash(); + require e.msg.sender != starport; + require startBalance + amount > starport.supplyCaps(excessiveToken); + uint256 startBalance = starport.balanceInERC20Asset(excessiveToken); + invoke starport.lockTo(e, amount, excessiveToken, recipient); + assert lastReverted; +} + +/** + * @title Invoke Requires Quorum of Signatures + * @status ? + */ +rule checkSignatures(uint256 nSignatures, uint256 nAuthorities, bytes32 noticeHash) { + require nSignatures > 0; + require nAuthorities >= nSignatures; + // I don't trust multiplication + require nAuthorities < (nSignatures - 1) + (nSignatures - 1) + (nSignatures - 1); + sinvoke starport.signaturesAuthorizedPrecondition(nSignatures, nAuthorities, noticeHash); + invoke starport.checkSignatures(nSignatures, nAuthorities, noticeHash); + assert !lastReverted; +} + +/** + * @title Invoke Requires Quorum of Signatures + * @status ? + */ +rule checkSignaturesNotEnoughSignatures(uint256 nSignatures, uint256 nAuthorities, bytes32 noticeHash) { + require nSignatures > 0; + require nAuthorities > nSignatures + nSignatures + nSignatures; + sinvoke starport.signaturesAuthorizedPrecondition(nSignatures, nAuthorities, noticeHash); + invoke starport.checkSignatures(nSignatures, nAuthorities, noticeHash); + assert lastReverted; +} + +/** + * @title Invoke Requires Valid Notice Chain + * @status ? + */ +rule checkNoticeChainTargetNotHead(bytes32 targetHash) { + sinvoke starport.hashChainTargetNotParentPrecond(targetHash); + invoke starport.checkNoticeChain(targetHash); + assert lastReverted; +} + +/** + * @title Invoke Requires Valid Notice Chain + * @status ? + */ +rule checkNoticeChainBrokenLink(uint256 randomLink, bytes32 targetHash) { + sinvoke starport.hashChainBrokenLinkPrecond(randomLink); + invoke starport.checkNoticeChain(targetHash); + assert lastReverted; +} + +/** + * Check that supplyCaps is changed only if msg.sender is starport + * @status passing + */ +rule onlyStarportChangeSupplyCap(method f) { + address token; + uint256 tokenSupplyCap = starport.supplyCaps(token); + require e.msg.sender != currentContract && e.msg.sender != starport.admin(); + env e; + calldataarg args; + f(e, args); + assert tokenSupplyCap == starport.supplyCaps(token); +} + +/** + * Provides a "characterization" of which methods are restricted + * to being called by starport + */ +rule characterizeStarportOnlyMethods(method f) { + env e; + calldataarg args; + require e.msg.sender != currentContract; + f@withrevert(e, args); + assert lastReverted; +} + +/** + * Provides a "characterization" of which methods are restricted + * to being called by starport or admin + */ +rule characterizeStarportOrAdminOnlyMethods(method f) { + env e; + calldataarg args; + require e.msg.sender != currentContract && e.msg.sender != admin(); + f@withrevert(e, args); + assert lastReverted; +} \ No newline at end of file diff --git a/certora/spec/StarportOrdering.spec b/certora/spec/StarportOrdering.spec new file mode 100644 index 000000000..8c5493abd --- /dev/null +++ b/certora/spec/StarportOrdering.spec @@ -0,0 +1,266 @@ +using StarportHarnessOrdering as starport +using ERC20 as token +using NonStandardERC20 as nonStandardToken +using ExcessiveERC20 as excessiveToken +using CashToken as cashToken + +methods { + starport.eraId() returns (uint256) envfree + starport.admin() returns (address) envfree + starport.cash() returns (address) envfree + starport.supplyCaps(address) returns (uint256) envfree + starport.authorities(uint256) returns (address) envfree + starport.isNoticeInvoked(bytes32) returns (bool) envfree + starport.noticeAlreadyInvoked() returns (bool) envfree + starport.noticeReturnsEmptyString() returns (bool) envfree + starport.signaturesAuthorizedPrecondition(uint256,uint256,bytes32) envfree + starport.checkSignatures(uint256,uint256,bytes32) envfree + starport.hashChainTargetNotParentPrecond(bytes32) envfree + starport.checkNoticeChain(bytes32) envfree + starport.hashChainBrokenLinkPrecond(uint256) envfree + starport.lockTo(uint,address,address) + starport.balanceInERC20Asset(address) envfree + starport.isAssert() returns (bool) envfree + starport.nowAssert() envfree + + cashToken.totalCashPrincipal() returns (uint256) envfree + + transfer(address,uint256) => DISPATCHER(true) + transferFrom(address,address,uint256) => DISPATCHER(true) + balanceOf(address) => DISPATCHER(true) +} + +definition MAX_UINT256() returns uint256 = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff; + +/** + * forall m, n : N. m > n => (m, 0) > (n, 0) + * forall m, n : N. n > 0 => (m, 0) < (m, n) + * + * forall i, j : N. i <= j && isCurrentEra(j) => wasAccepted((i, 0)) + * + * forall i, j : EraAndIndex. i <= j && willAcceptNoticeAt(j) => alreadyAcceptedNoticeAt(i) + * - proof outline + * + * + * willAcceptNoticeAt(noticeEraId, noticeEraIndex) = noticeEraId <= eraId || noticeEraId == eraId + 1 && noticeEraIndex == 0 + * alreadyAcceptedNoticeAt(noticeEraId, noticeEraIndex) = + * + * (helper) + * invariant: forall era. era <= currentEra => isNoticeInvoked[(era, 0)] + * invairant: there is only ever one notice with a given (eraId, eraIndex) + */ +rule eraLemma { + env e; + calldataarg args; + calldataarg args1; + calldataarg args2; + + uint256 era; + uint256 eraIndex; + bytes32 noticeHash; + uint256 era1; + uint256 eraIndex1; + bytes32 noticeHash1; + + require !starport.isAssert(); + era, eraIndex, noticeHash = starport.myNoticeInfo(e, args); + // get notice info + era1, eraIndex1, noticeHash1 = starport.partialOrderingCall(e, args1); + + // notice unique by era,index: must be guaranteed by compound chain + require era == era1 && eraIndex == eraIndex1 <=> noticeHash == noticeHash1; + + require eraIndex == 0; + require era <= starport.eraId() => starport.isNoticeInvoked(noticeHash); + + sinvoke starport.nowAssert(); + // invoke notice + invoke starport.partialOrderingCall(e, args1); + + assert era <= starport.eraId() => starport.isNoticeInvoked(noticeHash); +} + +definition noticeLt(uint256 era1, uint256 index1, uint256 era2, uint256 index2) returns bool = (era1 <= era2 && index1 == 0 && index2 > 0) || (era1 < era2 && index1 == 0 && index2 == 0); +definition noticeLeq(uint256 era1, uint256 index1, uint256 era2, uint256 index2) returns bool = noticeLt(era1, index1, era2, index2) || era1 == era2 && index1 == index2; +/** + * forall i, j : EraAndIndex. i <= j && willAcceptNoticeAt(j) => alreadyAcceptedNoticeAt(i) + * + * @notice "address(this).call(calldata_)" must be removed from invokeNoticeInternal in order + * for this rule to pass. This is because we overapproximate "a call to any function" + * by havocing the entirety of storage (including eraId and isNoticeInvoked). We + * currently have no other way to handle unresolved calls. To mitigate this we have + * added a rule that checks that only invoke and invokeChain modify eraId and + * isNoticeInvoked (and presumably, a notice won't call invoke or invokeChain) + */ +rule noticePartialOrdering { + env e; + calldataarg args_i; + calldataarg args_j; + calldataarg args_call; + uint256 era_i; + uint256 era_j; + uint256 era_call; + uint256 eraIndex_i; + uint256 eraIndex_j; + uint256 eraIndex_call; + bytes32 noticeHash_i; + bytes32 noticeHash_j; + bytes32 noticeHash_call; + + require !starport.isAssert(); + + era_i, eraIndex_i, noticeHash_i = starport.partialOrderingCall(e, args_i); + era_j, eraIndex_j, noticeHash_j = starport.partialOrderingCall(e, args_j); + era_call, eraIndex_call, noticeHash_call = starport.partialOrderingCall(e, args_call); + + // notice unique by era,index: must be guaranteed by compound chain + require (era_i == era_call && eraIndex_i == eraIndex_call) <=> noticeHash_i == noticeHash_call; + require (era_i == era_j && eraIndex_i == eraIndex_j) <=> noticeHash_i == noticeHash_j; + require (era_j == era_call && eraIndex_j == eraIndex_call) <=> noticeHash_j == noticeHash_call; + + // eraLemma + uint256 era_pre = starport.eraId(); + require eraIndex_i == 0 => (era_i <= era_pre => starport.isNoticeInvoked(noticeHash_i)); + + sinvoke starport.nowAssert(); + + // invoke notice + invoke starport.partialOrderingCall(e, args_call); + + // eraLemma + uint256 era_post = starport.eraId(); + assert eraIndex_i == 0 => (era_i <= era_post => starport.isNoticeInvoked(noticeHash_i)); + + uint256 returnLength_post; + returnLength_post, _, _ = starport.partialOrderingCall@withrevert(e, args_j); + bool willAcceptNoticeAt_j = returnLength_post != 0 && !lastReverted; + assert (noticeLeq(era_i, eraIndex_i, era_j, eraIndex_j) && willAcceptNoticeAt_j) => starport.isNoticeInvoked(noticeHash_i); +} + +/** + * @title Only Invoking a Notice Modifies Era or Acceptance + * @status passing (failing on expected methods only) + */ +rule onlyInvokeChangesEraOrNoticeAccepted(method f) { + bytes32 noticeHash_1; + bytes32 noticeHash_2; + uint256 eraId = starport.eraId(); + require !starport.isNoticeInvoked(noticeHash_1); + require starport.isNoticeInvoked(noticeHash_2); + + env e; + calldataarg args; + f(e, args); + + assert starport.eraId() == eraId; + assert !starport.isNoticeInvoked(noticeHash_1); + assert starport.isNoticeInvoked(noticeHash_2); +} + +/* +A hand proof for the rule "noticePartialOrdering" + +assume i_i = 0 => e_i <= e => wasAccepted[(e_i, i_i)] +invoke invokeNotice((e_call, i_call)); +accepted_j := invokeNotice((e_j, i_j)); +assert accepted_j && (e_i, i_i) <= (e_j, i_j) => wasAccepted[(e_i, i_i)]; + + +H_1: i_i = 0 => e_i <= e => wasAccepted[(e_i, i_i)] +wasAccepted': N x N +e': N +wasAccepted'': N x N +e'': N +H_2: accepted_j = (e_j <= e' || (e_j == e' + 1 && i_j == 0) (from invokeNotice((e_j, i_j))) +H_3: wasAccepted'' = wasAccepted' U {(e_j, i_j)} +H_4: accepted_j && (e_i, i_i) <= (e_j, i_J) +H_9: i_i == 0 || (e_i == e_j && i_i == i_j) by H_4 and definition of <= +--------------------------------------------------------------------------------------------------- +wasAccepted''[(e_i, i_i)] + +case on invokeNotice((e_call, i_call)): + 1,2: no change or accepted without new era + H_6: wasAccepted' = wasAccepted || wasAccepted' z wasAccepted U {(e_call, i_call)} + H_7: e' = e + H_13: wasAccepted'' = wasAccepted U {(e_j, i_j)} by H_4 and H_6 || wasAccepted U {(e_call, i_call)} U {(e_j, i_j)} + ------------------------------------------------------------------------------------------- + case on H_9 (disjunction) + 1: + H_8: i_i == 0 (left disjunct) + --------------------------------------------------------------------------------------- + case on H_4, H_2 (disjunction) + 1: + H_10: e_j <= e' + H_11: e_i <= e_j H_8, H_4 and definition of <= + H_12: e_i <= e H_11, H_10, H_7 + ----------------------------------------------------------------------------------- + wasAccepted''[(e_i, i_i)] H_13, H_1, H_8, H_12 + 2: + H_14: (e_j == e' + 1 && i_j == 0) + ----------------------------------------------------------------------------------- + case on H_4, 2nd conjunct (disjunction of <=): + 1: + H_15: (e_i, i_i) == (e_j, i_j) + ------------------------------------------------------------------------------- + wasAccepted''[(e_i, i_i)] H_15, H_13 + 2: + H_16: (e_i, i_i) < (e_j, i_j) + H_17: e_i < e_j H_16, H_14 (i_j == 0) and definition of < + H_18: e_i <= e' H_14, H_17 + H_19: e_i <= e H_18, H_7 + ------------------------------------------------------------------------------- + wasAccepted''[(e_i, i_i)] H_13, H_1, H_8, H_19 + 2: + H_20: (e_i, i_i) == (e_j, i_j) + --------------------------------------------------------------------------------------- + wasAccepted''[(e_i, i_i)] H_13, H_20 + 3: accepted with new era + H_21: e_call == e + 1 && i_call == 0 + H_22: e' = e + 1 + H_23: wasAccepted' = wasAccepted U {(e_call, i_call)} + H_27: wasAccepted'' = wasAccepted U {(e_call, i_call)} U {(e_j, i_j)} + ------------------------------------------------------------------------------------------- + case on H_9 (disjunction) + 1: + H_24: i_i == 0 (left disjunct) + --------------------------------------------------------------------------------------- + case on H_4, H_2 (disjunction) + 1: + H_25: e_j <= e' + H_26: e_i <= e_j H_24, H_4 and definition of <= + H_28: e_i <= e H_26, H_25, H_22 + ----------------------------------------------------------------------------------- + wasAccepted''[(e_i, i_i)] H_27, H_1, H_24, H_28 + 2: + H_29: (e_j == e' + 1 && i_j == 0) + ----------------------------------------------------------------------------------- + case on H_4, 2nd conjunct (disjunction of <=): + 1: + H_30: (e_i, i_i) == (e_j, i_j) + ------------------------------------------------------------------------------- + wasAccepted''[(e_i, i_i)] H_30, H_27 + 2: + H_31: (e_i, i_i) < (e_j, i_j) + H_32: e_i < e_j H_31, H_29 (i_j == 0) and definition of < + H_33: e_i <= e' H_32, H_29 + H_34: e_i <= e + 1 H_33, H_22 + ------------------------------------------------------------------------------- + case on H_34: + 1: + H_35: e_i == e + 1 + H_36: e_i != e_j H_32 + H_37 (e_i, i_i) != (e_j, i_j) H_36 + H_39 (e_call, i_call) = (e_i, i_i) H_24, H_35, H_21 + --------------------------------------------------------------------------- + wasAccepted''[(e_i, i_i)] H_39, H_27 + 2: + H_40: e_i < e + 1 + H_41: e_i <= e H_40 + --------------------------------------------------------------------------- + wasAccepted''[(e_i, i_i)] H_27, H_1, H_24, H_41 + + 2: + H_42: e_i == e_j && i_i == i_j + --------------------------------------------------------------------------------------- + wasAccepted''[(e_i, i_i)] H_27, H_42 +*/ \ No newline at end of file diff --git a/certora/spec/erc20.spec b/certora/spec/erc20.spec new file mode 100644 index 000000000..f7ed74794 --- /dev/null +++ b/certora/spec/erc20.spec @@ -0,0 +1,895 @@ +// Specification for core ERC20 tokens +methods { + balanceOf(address) returns uint256 + transfer(address,uint256) returns bool + transferFrom(address, address, uint256) returns bool + approve(address, uint256) returns bool + allowance(address, address) returns uint256 + totalSupply() returns uint256 + // Extended API - not implemented + mint(address,uint256) returns bool + burn(uint256) + owner() returns address + paused() returns bool +} + +// Preconditions checked - no pause +transferStandardPrecondition(env e, address to, uint256 value) +description "Transfer failed even though to != 0, value > 0, balances match" +{ + uint256 MAXINT = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF; + require to != 0; + require value > 0; + + address from = e.msg.sender; + bool precondition = sinvoke balanceOf(e, from) >= value && sinvoke balanceOf(e,to) + value <= MAXINT; + + require precondition; + + bool result = invoke transfer(e, to, value); + bool transferReverted = lastReverted; + + assert !transferReverted && result; +} + +cannotTransferFromZero(env e, address to, uint256 value) +description "TransferFrom succeeded with from=0" +{ + address from = 0; + + bool result = invoke transferFrom(e, from, to, value); + bool transferReverted = lastReverted; + + assert transferReverted || !result, "Succeeded to transferFrom with from=0"; +} + + +cannotTransferFromWithSpenderZero(env e, address from, address to, uint256 value) +description "TransferFrom succeeded with spender=0" +{ + address spender = e.msg.sender; + require spender == 0; + + bool result = invoke transferFrom(e, from, to, value); + bool transferReverted = lastReverted; + + assert transferReverted || !result, "Succeeded to transferFrom with spender=0"; +} + +transferFromStandardPrecondition(env e, address from, address to, uint256 value) +description "TransferFrom failed even though to != 0, value > 0, balances match, allowance suffices" +{ + uint256 MAXINT = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF; + require to != 0; + require value > 0; + require from != 0; // checked in cannotTransferFromZero + // require e.msg.value == 0; // not necessary because enforced by call to balanceOf. + + address spender = e.msg.sender; + require spender != 0; // checked in cannotTransferFromWithSpenderZero + bool precondition = sinvoke balanceOf(e, from) >= value && sinvoke balanceOf(e,to) + value <= MAXINT && sinvoke allowance(e,from,spender) >= value; + + require precondition; + + bool result = invoke transferFrom(e, from, to, value); + bool transferReverted = lastReverted; + + assert !transferReverted && result; +} + +zeroCannotApprove(env e, address spender, uint256 value) +description "Approve succeeded for sender=0" +{ + require e.msg.sender == 0; + address from = e.msg.sender; + + bool result = invoke approve(e, spender, value); + bool reverted = lastReverted; + + assert reverted || !result, "Approve succeeded for sender=0"; +} + +cannotApproveNonZeroWhenCurrentlyNonZero(env e, address spender, uint256 value) +description "Approve succeeded even though current allowance is non-zero and value is non-zero" +{ + address from = e.msg.sender; + require from != 0; // checked in canZeroApprove + require value != 0; + uint256 currentAllowance = sinvoke allowance(e,from,spender); + require currentAllowance != 0; + + bool result = invoke approve(e, spender, value); + bool reverted = lastReverted; // loading transferReverted + + assert reverted || !result, "Approve succeeded even though value is non-zero and current allowance is non-zero"; +} + +cannotApproveToZeroSpender(env e, address spender, uint256 value) +description "Approve succeeded even though approved to spender=0" +{ + require spender == 0; + + bool result = invoke approve(e, spender, value); + bool reverted = lastReverted; + + assert reverted || !result, "Approve succeeded for spender=0"; +} + +approveStandardPrecondition(env e, address spender, uint256 value) +description "Approve failed even though current allowance is 0" +{ + // require e.msg.value == 0; // not necessary because enforced by call to allowance. + + address from = e.msg.sender; + require from != 0; // checked in zeroCannotApprove + require spender != 0; // checked in cannotApproveToZeroSpender + bool precondition = sinvoke allowance(e,from,spender) == 0; + + require precondition; + + bool result = invoke approve(e, spender, value); + bool reverted = lastReverted; // loading transferReverted + + assert !reverted && result, "approve failed even though meets precondition"; +} + + + +// Preconditions checked - with pause +transferStandardPreconditionWithPause(env e, address to, uint256 value) +description "Transfer failed even though to != 0, value > 0, balances match" +{ + uint256 MAXINT = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF; + require to != 0; + require value > 0; + + // require e.msg.value == 0; // not necessary because enforced by call to balanceOf. + + address from = e.msg.sender; + bool precondition = sinvoke balanceOf(e, from) >= value && sinvoke balanceOf(e,to) + value <= MAXINT && !(sinvoke paused(e)); + + require precondition; + + bool result = invoke transfer(e, to, value); + bool transferReverted = lastReverted; // loading transferReverted + + assert !transferReverted && result; +} + +transferFromStandardPreconditionWithPause(env e, address from, address to, uint256 value) +description "TransferFrom failed even though to != 0, value > 0, balances match, allowance suffices" +{ + uint256 MAXINT = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF; + require to != 0; + require value > 0; + + // require e.msg.value == 0; // not necessary because enforced by call to balanceOf. + + address spender = e.msg.sender; + bool precondition = sinvoke balanceOf(e, from) >= value && sinvoke balanceOf(e,to) + value <= MAXINT && sinvoke allowance(e,from,spender) >= value && !(sinvoke paused(e)); + + require precondition; + + bool result = invoke transferFrom(e, from, to, value); + bool transferReverted = lastReverted; // loading transferReverted + + assert !transferReverted && result; +} + + +approveStandardPreconditionWithPause(env e, address spender, uint256 value) +description "Approve failed even though current allowance is 0" +{ + // require e.msg.value == 0; // not necessary because enforced by call to allowance. + + address from = e.msg.sender; + bool precondition = sinvoke allowance(e,from,spender) == 0 && !(sinvoke paused(e)); + + require precondition; + + bool result = invoke approve(e, spender, value); + bool reverted = lastReverted; // loading transferReverted + + assert !reverted && result; +} + +/* +isApproveLike(env e, method f, address approvedAddress, uint256 amount, address randomAddress) +good_description "method f is potentially approve-like: updates allowance from sender, but not balances" +{ + env eGetters; + uint256 originalBalanceOfRandomAddress = sinvoke balanceOf(eGetters, randomAddress); + + sinvoke f(e, approvedAddress, amount); + + uint256 newBalanceOfRandomAddress = sinvoke balanceOf(eGetters, randomAddress); + +} +*/ + +transferCheckPreconds(env e, address to, uint256 value) +{ + require to != 0; + require value != 0; + + address from = e.msg.sender; + bool precondition = sinvoke balanceOf(e, from) >= value; + + bool result = invoke transfer(e, to, value); + bool transferReverted = lastReverted; // loading transferReverted + + // The transfer function must meet the precondition, or to revert. + assert !precondition => (transferReverted || !result), "If transfer() precondition does not hold, must either revert or return 0"; +} + +transferCheckEffects(env e, address to, uint256 value) +{ + require to != 0; + require value != 0; + + address from = e.msg.sender; + uint256 origBalanceOfFrom = sinvoke balanceOf(e, from); + uint256 origBalanceOfTo = sinvoke balanceOf(e, to); + bool result = sinvoke transfer(e, to, value); + + // Start checking the effects + env e2; + require e2.block.timestamp >= e.block.timestamp && e2.block.number >= e.block.number; // Checking new balance in new, later environment + uint256 newBalanceOfTo = sinvoke balanceOf(e2, to); // loading new balance of recipient + uint256 newBalanceOfFrom = sinvoke balanceOf(e2,from); + + // Compute the expected new balance. + uint expectedNewBalanceOfTo; + uint expectedNewBalanceOfFrom; + if (from != to && result) { + require expectedNewBalanceOfTo == origBalanceOfTo + value; + require expectedNewBalanceOfFrom == origBalanceOfFrom - value; + } else { + require expectedNewBalanceOfTo == origBalanceOfTo; + require expectedNewBalanceOfFrom == origBalanceOfFrom; + } + + // Effects: new balance of recipient is as expected, and it should also be not less than the original balance + assert newBalanceOfTo == expectedNewBalanceOfTo && newBalanceOfTo >= origBalanceOfTo, "invalid new balance of to"; + assert newBalanceOfFrom == expectedNewBalanceOfFrom && newBalanceOfFrom <= origBalanceOfFrom, "invalid new balance of from"; +} + +/* +// Transfer related tests +transferIncorrectUpdateOfBalanceForLegalRecipient(env e, address to, uint256 value) +-- split to other rules + +*/ + +transferForIllegalRecipient +description "Checked implementation permits sending to the 0 address via the transfer function." +good_description "Checked implementation does not permit sending funds to the 0 address via the transfer function." +{ + env e; + + uint256 origBalanceOf0 = sinvoke balanceOf(e, 0); + + uint256 value; + require value > 0; // zero tokens sent to 0 are less 'interesting' since there is no real effect + + invoke transfer(e, 0, value); + + uint256 newBalanceOf0 = sinvoke balanceOf(e, 0); + + assert newBalanceOf0 == origBalanceOf0, "Transfer to 0 changed the balance of 0 --> it is allowed"; +} + +transferWithIllegalValue +description "Checked implementation permits a transfer of zero tokens." +good_description "Checked implementation does not permit a transfer of zero tokens." +{ + env e; + address to; + require to != 0; + + require e.msg.value == 0; + bool res = invoke transfer(e, to, 0); + + assert lastReverted || !res; +} + +transferMayThrow +description "Checked implementation for transfer may revert." +good_description "Checked implementation for transfer never reverts." +{ + env e; + require e.msg.value == 0; // transfer is non payable, so this is the only precondition. + + // calldataarg arg; + // invoke transfer(e, arg); + address a; + uint256 v; + invoke transfer(e, a, v); + + assert !lastReverted; +} + +transferMayReturnFalse +description "Checked implementation for transfer may return false (0) and not due to a revert." +good_description "Checked implementation for transfer always returns `true` when not reverting." +{ + env e; + calldataarg arg; + + bool ret = sinvoke transfer(e, arg); + + assert ret; +} + +transferFromMayReturnFalse +description "Checked implementation for transferFrom may return false (0) and not due to a revert." +good_description "Checked implementation for transferFrom always returns `true` when not reverting." +{ + env e; + calldataarg arg; + + bool ret = sinvoke transferFrom(e, arg); + + assert ret; +} + + +transferImpactOthers(env e, address to, uint256 value, address other) +description "Unexpected effect of transfer (sender=${e.msg.sender} to=$to value=${value}): +should not change the balance of $other from $origBalanceOfOther to $newBalanceOfOther." +good_description "An invocation of transfer can potentially only affect the balances of sender and recipient." +{ + require e.msg.sender != other && other != to; + + uint256 origBalanceOfOther = sinvoke balanceOf(e,other); + + invoke transfer(e,to,value); + + env e2; + require e2.block.number >= e.block.number; + + uint256 newBalanceOfOther = sinvoke balanceOf(e2, other); + assert newBalanceOfOther == origBalanceOfOther; +} + +transferUnexpectedBalanceChange(env e, address to, uint256 value) +description "A transfer (sender=${e.msg.sender} to=$to value=${value}) changed balances in an unexpected way. +Original balance of sender $balanceOfFrom updated to $updatedBalanceOfFrom. +Original balance of to $balanceOfTo updated to $updatedBalanceOfTo." +good_description "An invocation of transfer may only increase recipient's balance only and decrease sender's balance." +{ + uint256 balanceOfFrom = sinvoke balanceOf(e, e.msg.sender); + uint256 balanceOfTo = sinvoke balanceOf(e, to); + + invoke transfer(e,to,value); + + uint256 updatedBalanceOfTo = sinvoke balanceOf(e,to); + uint256 updatedBalanceOfFrom = sinvoke balanceOf(e,e.msg.sender); + + assert updatedBalanceOfTo >= balanceOfTo && updatedBalanceOfFrom <= balanceOfFrom; +} + +transferCappedDebit(env e, address to, uint256 value) +description "A transfer debits more than authorized: debit=$debit, while authorized=$value" +good_description "A transfer cannot debit the sender by more than the passed value." +{ + env e0; + require e0.block.number == e.block.number; + uint256 balanceOfFrom = sinvoke balanceOf(e0, e.msg.sender); + + invoke transfer(e,to,value); + + uint256 updatedBalanceOfFrom = sinvoke balanceOf(e0,e.msg.sender); + + uint256 debit = balanceOfFrom-updatedBalanceOfFrom; + assert debit <= value; +} + + +// Higher-order tests +unexpectedAllowanceChange(method f, address tokenOwner, address spender) +description "Function $f, which is not transferFrom or approve, +should not change allowance of token owner $tokenOwner to spender $spender +from $origSpenderAllowance to $newSpenderAllowance." +{ + env e; + uint256 origSpenderAllowance = sinvoke allowance(e, tokenOwner, spender); + + calldataarg arg; + require f.selector != transferFrom(address,address,uint256).selector && f.selector != approve(address,uint256).selector; + env ef; + invoke f(ef, arg); + + env e2; + require e2.block.number >= e.block.number; + + uint256 newSpenderAllowance = sinvoke allowance(e2, tokenOwner, spender); + assert newSpenderAllowance == origSpenderAllowance; +} + +unexpectedBalanceChange(method f, address targetAddress) +description "Function $f, which is not transferFrom or transfer, +should not change balanceOf of targetAddress=$targetAddress +from $origBalanceOfTarget to $newBalanceOfTarget." +{ + env e; + uint256 origBalanceOfTarget = sinvoke balanceOf(e, targetAddress); + + calldataarg arg; + require f.selector != transferFrom(address,address,uint256).selector && f.selector != transfer(address,uint256).selector; + env ef; + invoke f(ef, arg); + + env e2; + require e2.block.number >= e.block.number; + + uint256 newBalanceOfTarget = sinvoke balanceOf(e2, targetAddress); + + assert newBalanceOfTarget == origBalanceOfTarget; +} + +unexpectedBalanceChangeExtendedAPI(method f, address targetAddress) +description "Function $f, which is not transferFrom, transfer, mint or burn, +should not change balanceOf of targetAddress=$targetAddress +from $origBalanceOfTarget to $newBalanceOfTarget." +{ + env e; + uint256 origBalanceOfTarget = sinvoke balanceOf(e, targetAddress); + + calldataarg arg; + require f.selector != transferFrom(address,address,uint256).selector && f.selector != transfer(address,uint256).selector && f.selector != burn(uint256).selector && f.selector != mint(address,uint256).selector; + env ef; + invoke f(ef, arg); + + env e2; + require e2.block.number >= e.block.number; + + uint256 newBalanceOfTarget = sinvoke balanceOf(e2, targetAddress); + + assert newBalanceOfTarget == origBalanceOfTarget; +} + +senderCanOnlyReduceHerOwnBalance( method f, address sender, address other) +description "Sender $sender calling method $f (not transferFrom) should only reduce her own balance and not other's. +But other's $other balance updated from $origBalanceOfOther to $newBalanceOfOther." +{ + env e; + require other != sender; + uint256 origBalanceOfOther = sinvoke balanceOf(e, other); + + calldataarg arg; + env ef; + require ef.msg.sender == sender; + require f.selector != transferFrom(address,address,uint256).selector; + invoke f(ef, arg); + + env e2; + require e2.block.number >= e.block.number; + + uint256 newBalanceOfOther = sinvoke balanceOf(e2, other); + + assert newBalanceOfOther >= origBalanceOfOther; +} + +senderCanOnlyReduceHerOwnBalanceUnlessAllowanceAllowsIt( method f, address sender, address other) +description "Sender $sender calling method $f (not transferFrom) should only reduce her own balance and not other's. +But other's $other balance updated from $origBalanceOfOther to $newBalanceOfOther." +{ + env e; + require other != sender; + uint256 origBalanceOfOther = sinvoke balanceOf(e, other); + + uint256 origAllowance = sinvoke allowance(e, other, sender); + + calldataarg arg; + env ef; + require ef.msg.sender == sender; + invoke f(ef, arg); + + env e2; + require e2.block.number >= e.block.number; + + uint256 newBalanceOfOther = sinvoke balanceOf(e2, other); + + assert newBalanceOfOther >= origBalanceOfOther || origAllowance >= origBalanceOfOther-newBalanceOfOther; +} + + +unexpectedTotalSupplyChange(method f, address targetAddress) +description "Function $f should not change total supply from $origTotalSupply to $newTotalSupply." +{ + env e; + uint256 origTotalSupply = sinvoke totalSupply(e); + + calldataarg arg; + + //require f != mint && f != burn; + env ef; + invoke f(ef, arg); + + env e2; + require e2.block.number > e.block.number; + + uint256 newTotalSupply = sinvoke totalSupply(e2); + + /* some implementations subtracts balance of address(0) and this will have to be accounted for. + This particular test assumes that totalSupply is only updated from mint, burn. + */ + assert newTotalSupply == origTotalSupply; +} + +unexpectedTotalSupplyIncrease(method f, address targetAddress) +{ + env e; + uint256 origTotalSupply = sinvoke totalSupply(e); + + calldataarg arg; + + //require f != mint && f != burn; + env ef; + invoke f(ef, arg); + + env e2; + require e2.block.number >= e.block.number; + + uint256 newTotalSupply = sinvoke totalSupply(e2); + + /* some implementations subtracts balance of address(0) and this will have to be accounted for. + This particular test assumes that totalSupply is only updated from mint, burn. + */ + assert newTotalSupply <= origTotalSupply; +} + +// Characterizing totalSupply +totalSupplyDoesNotIncludeBalanceOfZeroCheckWithTransferToZero(uint256 expectedChange) +description "function totalSupply does not include the balance of the zero address: +When transferring $expectedChange tokens to the zero address, totalSupply was deducted that amount" +/* + If the contract does not allow sending to zero address, there must be some other functionality (like burn) that can be used to check for that behavior. + */ +{ + env e; + + uint256 origTotalSupply = sinvoke totalSupply(e); + + // now, transfer to zero a positive number of tokens, require it to succeed. + require expectedChange > 0; + + sinvoke transfer(e, 0, expectedChange); + + env e2; + uint256 newTotalSupply = sinvoke totalSupply(e2); + + assert newTotalSupply != origTotalSupply - expectedChange; +} + +// TransferFrom related tests +transferFromWrongBalanceOrAllowanceChanges_0(env e, address from, address to, uint256 value) +description "transferFrom (from = $from, to = $to, by ${e.msg.sender}, value = $value) did not update participants balances and allowances as expected." +{ + address caller = e.msg.sender; + uint256 origBalanceOfFrom = sinvoke balanceOf(e, from); + uint256 origBalanceOfTo = sinvoke balanceOf(e, to); + uint256 origAllowance = sinvoke allowance(e, from, caller); + + bool precondition = origBalanceOfFrom >= value && origAllowance >= value; + + bool result = invoke transferFrom(e, from, to, value); + bool transferFromReverted = lastReverted; + // The transferFrom function must meet the precondition, or to revert. + assert precondition || (transferFromReverted || !result); +} + +transferFromWrongBalanceOrAllowanceChanges(env e, address from, address to, uint256 value) +description "transferFrom (from = $from, to = $to, by ${e.msg.sender}, value = $value) did not update participants balances and allowances as expected." +{ + address caller = e.msg.sender; + uint256 origBalanceOfFrom = sinvoke balanceOf(e, from); + uint256 origBalanceOfTo = sinvoke balanceOf(e, to); + uint256 origAllowance = sinvoke allowance(e, from, caller); + + bool precondition = origBalanceOfFrom >= value && origAllowance >= value; + + bool result = invoke transferFrom(e, from, to, value); + bool transferFromReverted = lastReverted; + // The transferFrom function must meet the precondition, or to revert. + //assert precondition || (transferFromReverted || !result); + + env e2; + require e2.block.number >= e.block.number; + uint256 newBalanceOfFrom = sinvoke balanceOf(e2, from); + uint256 newBalanceOfTo = sinvoke balanceOf(e2, to); + uint256 newAllowance = sinvoke allowance(e2,from, caller); + + bool expectedNewBalanceOfFrom = (((transferFromReverted || !result) || from == to) && newBalanceOfFrom == origBalanceOfFrom) + || (!((transferFromReverted || !result) || from == to) && newBalanceOfFrom == origBalanceOfFrom - value); + bool expectedNewBalanceOfTo = (((transferFromReverted || !result) || from == to) && newBalanceOfTo == origBalanceOfTo) + || (!((transferFromReverted || !result) || from == to) && newBalanceOfTo == origBalanceOfTo + value); + bool expectedNewAllowance = ((transferFromReverted || !result) && newAllowance == origAllowance) + || (!(transferFromReverted || !result) && newAllowance == (origAllowance - value)); + + + bool newFromBalanceChanged = (sinvoke balanceOf(e2, from) == origBalanceOfFrom - value); + bool newToBalanceChanged = (sinvoke balanceOf(e2, to) == origBalanceOfTo + value); + bool newAllowanceChanged = (sinvoke allowance(e2, from, caller) == origAllowance - value); + + assert expectedNewBalanceOfFrom && expectedNewBalanceOfTo && expectedNewAllowance; +} + +transferFromWithIllegalRecipient +description "transferFrom permits sending to zero address." +{ + env e; + address from; + uint256 value; + + uint256 origBalanceOfFrom = sinvoke balanceOf(e, from); + uint256 origAllowance = sinvoke allowance(e, from, e.msg.sender); + + require origBalanceOfFrom >= value && origAllowance >= value; + + invoke transferFrom(e, from, 0, value); + + assert lastReverted; +} + +unexpectedTransferFromImpact(env e, address from, address to, uint256 value, address x, address y, address z) +description "transferFrom sender=${e.msg.sender}, from=$from, to=$to, value=$value - should not impact other allowances (e.g. from y=$y to z=$z), balances (e.g. for x=$x), or total supply" +{ + uint256 origBalanceX = sinvoke balanceOf(e,x); + uint256 origAllowanceYZ = sinvoke allowance(e, y, z); + uint256 origTotalSupply = sinvoke totalSupply(e); + + invoke transferFrom(e, from, to, value); + + env e2; + require e2.block.number >= e.block.number; + + uint256 newBalanceX = sinvoke balanceOf(e2, x); + uint256 newAllowanceYZ = sinvoke allowance(e2, y, z); + uint256 newTotalSupply = sinvoke totalSupply(e2); + + bool sameBalanceOfX = x == from || x == to || origBalanceX == newBalanceX; + bool sameAllowanceYZ = (y == from && z == e.msg.sender) || newAllowanceYZ == origAllowanceYZ; + bool sameTotalSupply = origTotalSupply == newTotalSupply; + + assert sameBalanceOfX && sameAllowanceYZ && sameTotalSupply; +} + +transferFromCappedDebit(env e, address from, address to, uint256 value) +description "A transfer debits more than authorized: debit=$debit, while authorized=$value" +{ + env e0; + require e0.block.number == e.block.number; + uint256 balanceOfFrom = sinvoke balanceOf(e0, e.msg.sender); + + invoke transferFrom(e,from,to,value); + + uint256 updatedBalanceOfFrom = sinvoke balanceOf(e0,e.msg.sender); + + mathint debit = balanceOfFrom-updatedBalanceOfFrom; + assert debit <= value; +} + + +// Approve related tests +unexpectedApproveImpact(env e, address spender, uint256 value, address x, address y, address z) +description "approve by ${e.msg.sender} to spender $spender with value $value should update allowance of sender to spender, and nothing else. +Consider checking balance of x=$x or allowance from y=$y to z=$z." +{ + // Load everything that should not change + uint256 origBalanceOfX = sinvoke balanceOf(e, x); + uint256 origAllowanceYZ = sinvoke allowance(e, y, z); + uint256 origTotalSupply = sinvoke totalSupply(e); + + bool retVal = invoke approve(e,spender, value); + bool approveInvocationReverted = lastReverted; + + env e2; + require e2.block.number >= e.block.number; + + // load new allowance that should be updated + uint256 newAllowanceOfSpender = sinvoke allowance(e2,e.msg.sender,spender); + + // load new values that should stay the same + uint256 newBalanceOfX = sinvoke balanceOf(e2, x); + uint256 newAllowanceYZ = sinvoke allowance(e2, y, z); + uint256 newTotalSupply = sinvoke totalSupply(e2); + + bool correctEffectOnSpender = approveInvocationReverted || !retVal || newAllowanceOfSpender == value; + bool sameTotalSupply = newTotalSupply == origTotalSupply; + bool sameBalanceOfX = newBalanceOfX == origBalanceOfX; + bool sameAllowanceYZ = y == e.msg.sender && z == spender || newAllowanceYZ == origAllowanceYZ; + assert correctEffectOnSpender && sameTotalSupply && sameBalanceOfX && sameAllowanceYZ; +} + +approveMustBeAuthorized(env e, method f, address _owner, address spender) +description "Unallowed approval (increase of allowances) for $a" +{ + calldataarg arg; + + env e0; + uint256 origAllowance = sinvoke allowance(e0, _owner, spender); + + invoke f(e, arg); + + uint256 newAllowance = sinvoke allowance(e0, _owner, spender); + + assert (newAllowance > origAllowance) => e.msg.sender == _owner; +} + +// Getters +balanceOfShouldNotRevert +description "balanceOf function may revert" +{ + env e; + calldataarg arg; + + require e.msg.value == 0; + invoke balanceOf(e, arg); + + assert !lastReverted; +} + +allowanceShouldNotRevert +description "allowance function may revert" +{ + env e; + calldataarg arg; + + require e.msg.value == 0; + invoke allowance(e, arg); + + assert !lastReverted; +} + +// Basic mint test +noUnlimitedMintingByOwner +description "The owner may at some stage fail to mint before reaching MAX_UINT -> contract contains conditions to limit minting." +{ + uint256 MAXINT = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF; + env e; + uint256 origTotalSupply = sinvoke totalSupply(e); + + address _owner = sinvoke owner(e); + + uint256 amount; + require amount > 0; + + require origTotalSupply + amount <= MAXINT; // it is still possible to increase total supply + + address receiver; + + env e2; + require e2.msg.sender == _owner && e2.block.number >= e.block.number; + + invoke mint(e2, receiver, amount); + bool mintReverted = lastReverted; + + uint256 newTotalSupply = sinvoke totalSupply(e2); + + assert newTotalSupply > origTotalSupply; +} + +noUnlimitedMintingByOwner2 +description "The owner may at some stage fail to mint before reaching MAX_UINT -> contract contains conditions to limit minting." +{ + uint256 MAXINT = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF; + env e; + uint256 origTotalSupply = sinvoke totalSupply(e); + + address _owner = sinvoke owner(e); + + uint256 amount; + require amount > 0; + + require origTotalSupply + amount <= MAXINT; // it is still possible to increase total supply + + address receiver; + require sinvoke balanceOf(e,receiver) + amount <= MAXINT; + + env e2; + require e2.msg.sender == _owner && e2.block.number >= e.block.number; + + invoke mint(e2, receiver, amount); + bool mintReverted = lastReverted; + + uint256 newTotalSupply = sinvoke totalSupply(e2); + + assert newTotalSupply > origTotalSupply; +} + +// Check for privileged operations +privilegedOperation(method f, address privileged) +description "$f can be called by more than one user without reverting" +{ + env e1; + calldataarg arg; + require (e1.msg.sender == privileged); + invoke f(e1, arg); // privileged succeeds executing candidate privileged operation. + bool firstSucceeded = !lastReverted; + + env e2; + calldataarg arg2; + require (e2.msg.sender != privileged); + invoke f(e2, arg2); // unprivileged + bool secondSucceeded = !lastReverted; + + assert !(firstSucceeded && secondSucceeded), "$f can be called by both ${e1.msg.sender} and ${e2.msg.sender}, so it is not privileged"; +} + +smartPrivilegedOperation(method f, address privileged) +description "$f can be called by more than one user without reverting" +{ + env e1; + calldataarg arg; + require (e1.msg.sender == privileged); + storage initialStorage = lastStorage; + invoke f(e1, arg); // privileged succeeds executing candidate privileged operation. + bool firstSucceeded = !lastReverted; + + env e2; + calldataarg arg2; + require (e2.msg.sender != privileged); + invoke f(e2, arg2) at initialStorage; // unprivileged + bool secondSucceeded = !lastReverted; + + assert !(firstSucceeded && secondSucceeded), "$f can be called by both ${e1.msg.sender} and ${e2.msg.sender}, so it is not privileged"; +} + +simplePrivilegedOperation(method f) +description "Function $f is not privileged" +{ + env e; + address o = sinvoke owner(e); + + env e2; + require e2.msg.sender != o; + + calldataarg arg; + invoke f(e2,arg); + + assert lastReverted, "$f did not revert even though not called by the owner"; +} + +// Standard methods implemented test +implementsStandard(env e) +description "If compiles, then checked implementation implements all standard ERC20 functions" +{ + address x; + address y; + uint256 a; + + invoke balanceOf(e,x); + invoke transfer(e,x,a); + invoke transferFrom(e,x,y,a); + invoke approve(e,x,a); + invoke allowance(e,x,y); + invoke totalSupply(e); + + assert true; +} + +hasMint(env e, address argForMint1, uint256 argForMint2) +description "The call to mint({$argForMint1,${argForMint2}) is possible" +{ + invoke mint(e,argForMint1,argForMint2); + + assert true; +} + +hasBurn(uint256 argForBurn) +description "The call to burn($argForBurn) is possible" +{ + env e; + invoke burn(e,argForBurn); + + assert true; +} + +hasOwner(env e) +description "There is an explicit owner by name in the contract" +{ + invoke owner(e); + assert true; +} diff --git a/certora/spec/harnesses/ERC20.sol b/certora/spec/harnesses/ERC20.sol new file mode 100644 index 000000000..bea10af46 --- /dev/null +++ b/certora/spec/harnesses/ERC20.sol @@ -0,0 +1,57 @@ +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.1; +import '../../contracts/ICash.sol'; +// with mint +contract ERC20 is IERC20 { + uint256 t; + mapping (address => uint256) b; + mapping (address => mapping (address => uint256)) a; + + string public name; + string public symbol; + uint public decimals; + + function myAddress() public returns (address) { + return address(this); + } + + function add(uint a, uint b) internal pure returns (uint256) { + uint c = a +b; + require (c >= a); + return c; + } + function sub(uint a, uint b) internal pure returns (uint256) { + require (a>=b); + return a-b; + } + + function totalSupply() override external view returns (uint256) { + return t; + } + function balanceOf(address account) override external view returns (uint256) { + return b[account]; + } + function transfer(address recipient, uint256 amount) override external returns (bool) { + b[msg.sender] = sub(b[msg.sender], amount); + b[recipient] = add(b[recipient], amount); + return true; + } + function allowance(address owner, address spender) override external view returns (uint256) { + return a[owner][spender]; + } + function approve(address spender, uint256 amount) override external returns (bool) { + a[msg.sender][spender] = amount; + return true; + } + + function transferFrom( + address sender, + address recipient, + uint256 amount + ) override external returns (bool) { + b[sender] = sub(b[sender], amount); + b[recipient] = add(b[recipient], amount); + a[sender][msg.sender] = sub(a[sender][msg.sender], amount); + return true; + } +} \ No newline at end of file diff --git a/certora/spec/harnesses/ExcessiveERC20.sol b/certora/spec/harnesses/ExcessiveERC20.sol new file mode 100644 index 000000000..dd5e47295 --- /dev/null +++ b/certora/spec/harnesses/ExcessiveERC20.sol @@ -0,0 +1,59 @@ +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.1; + +import '../../contracts/ICash.sol'; +// with mint +contract ExcessiveERC20 { + uint256 t; + mapping (address => uint256) b; + mapping (address => mapping (address => uint256)) a; + + string public name; + string public symbol; + uint public decimals; + + function myAddress() public returns (address) { + return address(this); + } + + function add(uint a, uint b) internal pure returns (uint256) { + uint c = a +b; + require (c >= a); + return c; + } + function sub(uint a, uint b) internal pure returns (uint256) { + require (a>=b); + return a-b; + } + + function totalSupply() external view returns (uint256) { + return t; + } + function balanceOf(address account) external view returns (uint256) { + return b[account]; + } + function transfer(address recipient, uint256 amount) external returns (address, uint256, bool) { + b[msg.sender] = sub(b[msg.sender], amount); + b[recipient] = add(b[recipient], amount); + return (recipient, amount, true); + } + + function allowance(address owner, address spender) external view returns (uint256) { + return a[owner][spender]; + } + function approve(address spender, uint256 amount) external returns (bool) { + a[msg.sender][spender] = amount; + return true; + } + + function transferFrom( + address sender, + address recipient, + uint256 amount + ) external returns (address, uint256, bool) { + b[sender] = sub(b[sender], amount); + b[recipient] = add(b[recipient], amount); + a[sender][msg.sender] = sub(a[sender][msg.sender], amount); + return (recipient, amount, true); + } +} \ No newline at end of file diff --git a/certora/spec/harnesses/NonStandardERC20.sol b/certora/spec/harnesses/NonStandardERC20.sol new file mode 100644 index 000000000..61fed727b --- /dev/null +++ b/certora/spec/harnesses/NonStandardERC20.sol @@ -0,0 +1,56 @@ +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.1; + +import '../../contracts/ICash.sol'; +// with mint +contract NonStandardERC20 is INonStandardERC20 { + uint256 t; + mapping (address => uint256) b; + mapping (address => mapping (address => uint256)) a; + + string public name; + string public symbol; + uint public decimals; + + function myAddress() public returns (address) { + return address(this); + } + + function add(uint a, uint b) internal pure returns (uint256) { + uint c = a +b; + require (c >= a); + return c; + } + function sub(uint a, uint b) internal pure returns (uint256) { + require (a>=b); + return a-b; + } + + function totalSupply() external view returns (uint256) { + return t; + } + function balanceOf(address account) override external view returns (uint256) { + return b[account]; + } + function transfer(address recipient, uint256 amount) override external { + b[msg.sender] = sub(b[msg.sender], amount); + b[recipient] = add(b[recipient], amount); + } + function allowance(address owner, address spender) external view returns (uint256) { + return a[owner][spender]; + } + function approve(address spender, uint256 amount) external returns (bool) { + a[msg.sender][spender] = amount; + return true; + } + + function transferFrom( + address sender, + address recipient, + uint256 amount + ) override external { + b[sender] = sub(b[sender], amount); + b[recipient] = add(b[recipient], amount); + a[sender][msg.sender] = sub(a[sender][msg.sender], amount); + } +} \ No newline at end of file diff --git a/certora/spec/sanity.spec b/certora/spec/sanity.spec new file mode 100644 index 000000000..204c7d43b --- /dev/null +++ b/certora/spec/sanity.spec @@ -0,0 +1,6 @@ +rule sanity(method f) { + env e; + calldataarg arg; + sinvoke f(e, arg); + assert false; +} \ No newline at end of file diff --git a/certora/spec/sanitySound.spec b/certora/spec/sanitySound.spec new file mode 100644 index 000000000..581a44641 --- /dev/null +++ b/certora/spec/sanitySound.spec @@ -0,0 +1,9 @@ +methods { + 0xee872558 /*executeOperation(address,uint256,uint256,bytes memory)*/ => HAVOC_ALL; +} +rule sanity(method f) { + env e; + calldataarg arg; + sinvoke f(e, arg); + assert false; +} \ No newline at end of file