diff --git a/crates/app/sdk/extensions/token/src/lib.rs b/crates/app/sdk/extensions/token/src/lib.rs index 7cdaf0e..da655f8 100644 --- a/crates/app/sdk/extensions/token/src/lib.rs +++ b/crates/app/sdk/extensions/token/src/lib.rs @@ -177,7 +177,6 @@ mod tests { use crate::account::Token; // The generated account struct use crate::account::{ERR_NOT_ENOUGH_BALANCE, ERR_UNDERFLOW}; - use evolve_testing::MockEnv; /// Helper to initialize a `Token` with some default data. diff --git a/crates/app/stf/Cargo.toml b/crates/app/stf/Cargo.toml index e30800f..fc756db 100644 --- a/crates/app/stf/Cargo.toml +++ b/crates/app/stf/Cargo.toml @@ -16,7 +16,10 @@ ahash = { version = "0.8.11", optional = true } linkme = {version = "0.3", default-features = false, optional = true} [dev-dependencies] +anyhow = "1" proptest = "1.4" +quint-connect = "0.1.1" +serde = { version = "1", features = ["derive"] } [lints] workspace = true diff --git a/crates/app/stf/tests/quint_common.rs b/crates/app/stf/tests/quint_common.rs new file mode 100644 index 0000000..993bd77 --- /dev/null +++ b/crates/app/stf/tests/quint_common.rs @@ -0,0 +1,191 @@ +#![allow(dead_code)] + +use borsh::{BorshDeserialize, BorshSerialize}; +use evolve_core::runtime_api::ACCOUNT_IDENTIFIER_PREFIX; +use evolve_core::{ + AccountCode, AccountId, Environment, ErrorCode, InvokableMessage, InvokeResponse, ReadonlyKV, + SdkResult, +}; +use evolve_stf::gas::StorageGasConfig; +use evolve_stf_traits::{ + AccountsCodeStorage, BeginBlocker, EndBlocker, PostTxExecution, StateChange, TxValidator, + WritableKV, +}; +use hashbrown::HashMap; + +// --------------------------------------------------------------------------- +// Shared test message (used by core and post-tx conformance tests) +// --------------------------------------------------------------------------- + +#[derive(Clone, Debug, BorshSerialize, BorshDeserialize)] +pub struct TestMsg { + pub key: Vec, + pub value: Vec, + pub fail_after_write: bool, +} + +impl InvokableMessage for TestMsg { + const FUNCTION_IDENTIFIER: u64 = 1; + const FUNCTION_IDENTIFIER_NAME: &'static str = "test_msg"; +} + +// --------------------------------------------------------------------------- +// Noop STF components +// --------------------------------------------------------------------------- + +pub struct NoopBegin(std::marker::PhantomData); + +impl Default for NoopBegin { + fn default() -> Self { + Self(std::marker::PhantomData) + } +} + +impl BeginBlocker for NoopBegin { + fn begin_block(&self, _block: &B, _env: &mut dyn Environment) {} +} + +#[derive(Default)] +pub struct NoopEnd; + +impl EndBlocker for NoopEnd { + fn end_block(&self, _env: &mut dyn Environment) {} +} + +pub struct NoopValidator(std::marker::PhantomData); + +impl Default for NoopValidator { + fn default() -> Self { + Self(std::marker::PhantomData) + } +} + +impl TxValidator for NoopValidator { + fn validate_tx(&self, _tx: &T, _env: &mut dyn Environment) -> SdkResult<()> { + Ok(()) + } +} + +pub struct NoopPostTx(std::marker::PhantomData); + +impl Default for NoopPostTx { + fn default() -> Self { + Self(std::marker::PhantomData) + } +} + +impl PostTxExecution for NoopPostTx { + fn after_tx_executed( + _tx: &T, + _gas_consumed: u64, + _tx_result: &SdkResult, + _env: &mut dyn Environment, + ) -> SdkResult<()> { + Ok(()) + } +} + +// --------------------------------------------------------------------------- +// In-memory storage and code store +// --------------------------------------------------------------------------- + +pub struct CodeStore { + codes: HashMap>, +} + +impl Default for CodeStore { + fn default() -> Self { + Self { + codes: HashMap::new(), + } + } +} + +impl CodeStore { + pub fn new() -> Self { + Self::default() + } + pub fn add_code(&mut self, code: impl AccountCode + 'static) { + self.codes.insert(code.identifier(), Box::new(code)); + } +} + +impl AccountsCodeStorage for CodeStore { + fn with_code(&self, identifier: &str, f: F) -> Result + where + F: FnOnce(Option<&dyn AccountCode>) -> R, + { + Ok(f(self.codes.get(identifier).map(|c| c.as_ref()))) + } + fn list_identifiers(&self) -> Vec { + self.codes.keys().cloned().collect() + } +} + +#[derive(Default)] +pub struct InMemoryStorage { + pub data: HashMap, Vec>, +} + +impl ReadonlyKV for InMemoryStorage { + fn get(&self, key: &[u8]) -> Result>, ErrorCode> { + Ok(self.data.get(key).cloned()) + } +} + +impl WritableKV for InMemoryStorage { + fn apply_changes(&mut self, changes: Vec) -> Result<(), ErrorCode> { + for change in changes { + match change { + StateChange::Set { key, value } => { + self.data.insert(key, value); + } + StateChange::Remove { key } => { + self.data.remove(&key); + } + } + } + Ok(()) + } +} + +// --------------------------------------------------------------------------- +// Helpers +// --------------------------------------------------------------------------- + +pub fn account_code_key(account: AccountId) -> Vec { + let mut out = vec![ACCOUNT_IDENTIFIER_PREFIX]; + out.extend_from_slice(&account.as_bytes()); + out +} + +pub fn default_gas_config() -> StorageGasConfig { + StorageGasConfig { + storage_get_charge: 1, + storage_set_charge: 1, + storage_remove_charge: 1, + } +} + +pub fn register_account(storage: &mut InMemoryStorage, account: AccountId, code_id: &str) { + use evolve_core::Message; + let id = code_id.to_string(); + storage.data.insert( + account_code_key(account), + Message::new(&id).unwrap().into_bytes().unwrap(), + ); +} + +pub fn extract_account_storage( + storage: &InMemoryStorage, + account: AccountId, +) -> HashMap, Vec> { + let prefix = account.as_bytes(); + let mut result = HashMap::new(); + for (key, value) in &storage.data { + if key.len() >= prefix.len() && key[..prefix.len()] == prefix { + result.insert(key[prefix.len()..].to_vec(), value.clone()); + } + } + result +} diff --git a/crates/app/stf/tests/quint_core_connect.rs b/crates/app/stf/tests/quint_core_connect.rs new file mode 100644 index 0000000..e886c17 --- /dev/null +++ b/crates/app/stf/tests/quint_core_connect.rs @@ -0,0 +1,438 @@ +//! `quint_connect` pilot for `specs/stf_core.qnt`. +//! +//! This uses `quint run --mbt` rather than `quint test`: with Quint 0.30.0, the +//! plain `test` traces do not include `mbt::actionTaken`/`mbt::nondetPicks`, +//! which `quint_connect` needs in order to replay steps. + +use anyhow::anyhow; +use borsh::{BorshDeserialize, BorshSerialize}; +use evolve_core::runtime_api::ACCOUNT_IDENTIFIER_PREFIX; +use evolve_core::storage_api::{StorageSetRequest, STORAGE_ACCOUNT_ID}; +use evolve_core::{ + AccountCode, AccountId, BlockContext, Environment, EnvironmentQuery, ErrorCode, FungibleAsset, + InvokeRequest, InvokeResponse, Message, SdkResult, +}; +use evolve_stf::Stf; +use evolve_stf_traits::{ + Block as BlockTrait, SenderBootstrap, Transaction, TxValidator, WritableKV, +}; +use quint_connect::*; +use serde::Deserialize; +use std::collections::{BTreeMap, BTreeSet}; + +mod quint_common; +use quint_common::{ + default_gas_config, extract_account_storage, register_account, CodeStore, InMemoryStorage, + NoopBegin, NoopEnd, NoopPostTx, TestMsg, +}; + +const SPEC_ERR_VALIDATION: u16 = 100; +const SPEC_ERR_EXECUTION: u16 = 200; +const SPEC_ERR_BOOTSTRAP: u16 = 300; +const WRITE_KEY: &[u8] = &[1]; +const WRITE_VALUE: &[u8] = &[11]; + +#[derive(Clone, Debug, Deserialize, Eq, PartialEq)] +struct SpecState { + storage: BTreeMap, Vec>>, + accounts: BTreeSet, + block_height: u64, + last_result: SpecBlockResult, + last_block_tx_count: u64, +} + +#[derive(Clone, Debug, Default, Deserialize, Eq, PartialEq)] +struct SpecBlockResult { + tx_results: Vec, + gas_used: u64, + txs_skipped: u64, +} + +#[derive(Clone, Debug, Deserialize, Eq, PartialEq)] +struct SpecTxResult { + result: SpecResult, + gas_used: u64, +} + +#[derive(Clone, Debug, Deserialize, Eq, PartialEq)] +struct SpecResult { + ok: bool, + err_code: u64, +} + +impl State for SpecState { + fn from_driver(driver: &CoreDriver) -> Result { + let accounts = driver.accounts(); + let storage = accounts + .iter() + .copied() + .map(|account| { + ( + account, + extract_account_storage(&driver.storage, AccountId::from_u64(account)) + .into_iter() + .map(|(key, value)| { + ( + key.into_iter().map(u64::from).collect(), + value.into_iter().map(u64::from).collect(), + ) + }) + .collect(), + ) + }) + .collect(); + + Ok(Self { + storage, + accounts, + block_height: driver.block_height, + last_result: driver.last_result.clone(), + last_block_tx_count: driver.last_block_tx_count, + }) + } +} + +#[derive(Clone, Debug)] +struct TestTx { + sender: AccountId, + recipient: AccountId, + request: InvokeRequest, + gas_limit: u64, + funds: Vec, + fail_validate: bool, + needs_bootstrap: bool, + fail_bootstrap: bool, +} + +impl Transaction for TestTx { + fn sender(&self) -> AccountId { + self.sender + } + fn recipient(&self) -> AccountId { + self.recipient + } + fn request(&self) -> &InvokeRequest { + &self.request + } + fn gas_limit(&self) -> u64 { + self.gas_limit + } + fn funds(&self) -> &[FungibleAsset] { + &self.funds + } + fn compute_identifier(&self) -> [u8; 32] { + [0u8; 32] + } + fn sender_bootstrap(&self) -> Option { + if !self.needs_bootstrap { + return None; + } + let init = BootstrapInit { + fail: self.fail_bootstrap, + }; + let init_message = + Message::new(&init).expect("bootstrap init serialization must succeed in tests"); + Some(SenderBootstrap { + account_code_id: "test_account", + init_message, + }) + } +} + +#[derive(Clone)] +struct TestBlock { + height: u64, + time: u64, + txs: Vec, + gas_limit: u64, +} + +impl BlockTrait for TestBlock { + fn context(&self) -> BlockContext { + BlockContext::new(self.height, self.time) + } + fn txs(&self) -> &[TestTx] { + &self.txs + } + fn gas_limit(&self) -> u64 { + self.gas_limit + } +} + +#[derive(Default)] +struct Validator; + +impl TxValidator for Validator { + fn validate_tx(&self, tx: &TestTx, env: &mut dyn Environment) -> SdkResult<()> { + if tx.fail_validate { + return Err(ErrorCode::new(SPEC_ERR_VALIDATION)); + } + let probe = TestMsg { + key: vec![], + value: vec![], + fail_after_write: false, + }; + env.do_query(tx.sender(), &InvokeRequest::new(&probe).unwrap()) + .map_err(|_| ErrorCode::new(SPEC_ERR_VALIDATION))?; + Ok(()) + } +} + +#[derive(Default)] +struct TestAccount; + +#[derive(Clone, Debug, BorshSerialize, BorshDeserialize)] +struct BootstrapInit { + fail: bool, +} + +impl AccountCode for TestAccount { + fn identifier(&self) -> String { + "test_account".to_string() + } + fn schema(&self) -> evolve_core::schema::AccountSchema { + evolve_core::schema::AccountSchema::new("TestAccount", "test_account") + } + fn init( + &self, + _env: &mut dyn Environment, + request: &InvokeRequest, + ) -> SdkResult { + let init: BootstrapInit = request.get()?; + if init.fail { + return Err(ErrorCode::new(SPEC_ERR_BOOTSTRAP)); + } + InvokeResponse::new(&()) + } + fn execute( + &self, + env: &mut dyn Environment, + request: &InvokeRequest, + ) -> SdkResult { + let msg: TestMsg = request.get()?; + let set = StorageSetRequest { + key: msg.key.clone(), + value: Message::from_bytes(msg.value.clone()), + }; + env.do_exec(STORAGE_ACCOUNT_ID, &InvokeRequest::new(&set)?, vec![])?; + if msg.fail_after_write { + return Err(ErrorCode::new(SPEC_ERR_EXECUTION)); + } + InvokeResponse::new(&()) + } + fn query( + &self, + _env: &mut dyn EnvironmentQuery, + _request: &InvokeRequest, + ) -> SdkResult { + InvokeResponse::new(&()) + } +} + +#[derive(Default)] +struct CoreDriver { + storage: InMemoryStorage, + block_height: u64, + last_result: SpecBlockResult, + last_block_tx_count: u64, +} + +impl Driver for CoreDriver { + type State = SpecState; + + fn step(&mut self, step: &Step) -> Result { + switch!(step { + init => { self.reset()?; }, + register_account(id: u64) => { self.register(id)?; }, + apply_registered_block( + sender: u64, + recipient: u64, + gas_limit: u64, + block_gas: u64, + fail_v: bool, + fail_e: bool, + needs_b: bool, + fail_b: bool + ) => { + self.apply_registered_block( + sender, recipient, gas_limit, block_gas, fail_v, fail_e, needs_b, fail_b + )?; + } + }) + } +} + +impl CoreDriver { + fn reset(&mut self) -> Result { + self.storage = InMemoryStorage::default(); + self.block_height = 0; + self.last_result = SpecBlockResult::default(); + self.last_block_tx_count = 0; + Ok(()) + } + + fn register(&mut self, account_id: u64) -> Result { + register_account( + &mut self.storage, + AccountId::from_u64(account_id), + "test_account", + ); + Ok(()) + } + + #[allow(clippy::too_many_arguments)] + fn apply_registered_block( + &mut self, + sender: u64, + recipient: u64, + gas_limit: u64, + block_gas: u64, + fail_v: bool, + fail_e: bool, + needs_b: bool, + fail_b: bool, + ) -> Result { + let msg = TestMsg { + key: WRITE_KEY.to_vec(), + value: WRITE_VALUE.to_vec(), + fail_after_write: fail_e, + }; + let tx = TestTx { + sender: AccountId::from_u64(sender), + recipient: AccountId::from_u64(recipient), + request: InvokeRequest::new(&msg) + .map_err(|err| anyhow!("failed to serialize test request: {err:?}"))?, + gas_limit, + funds: vec![], + fail_validate: fail_v, + needs_bootstrap: needs_b, + fail_bootstrap: fail_b, + }; + let block = TestBlock { + height: self.block_height + 1, + time: 0, + txs: vec![tx], + gas_limit: block_gas, + }; + + let stf = build_stf(); + let codes = build_codes(); + let (result, exec_state) = stf.apply_block(&self.storage, &codes, &block); + let changes = exec_state + .into_changes() + .map_err(|err| anyhow!("failed to extract execution changes: {err:?}"))?; + self.storage + .apply_changes(changes) + .map_err(|err| anyhow!("failed to apply execution changes: {err:?}"))?; + self.block_height = block.height; + self.last_result = SpecBlockResult::from_real(&result); + self.last_block_tx_count = block.txs.len() as u64; + + Ok(()) + } + + fn accounts(&self) -> BTreeSet { + self.storage + .data + .iter() + .filter(|(key, value)| { + key.first() == Some(&ACCOUNT_IDENTIFIER_PREFIX) + && Message::from_bytes((*value).clone()) + .get::() + .ok() + .as_deref() + == Some("test_account") + }) + .filter_map(|(key, _)| { + let bytes = key.get(1..33)?; + let account_bytes: [u8; 32] = bytes.try_into().ok()?; + Some(account_id_to_u64(AccountId::from_bytes(account_bytes))) + }) + .collect() + } +} + +fn build_codes() -> CodeStore { + let mut codes = CodeStore::new(); + codes.add_code(TestAccount); + codes +} + +fn build_stf( +) -> Stf, Validator, NoopEnd, NoopPostTx> { + Stf::new( + NoopBegin::::default(), + NoopEnd, + Validator, + NoopPostTx::::default(), + default_gas_config(), + ) +} + +fn account_id_to_u64(account: AccountId) -> u64 { + let bytes = account.as_bytes(); + u64::from_be_bytes( + bytes[24..32] + .try_into() + .expect("account id must be 32 bytes"), + ) +} + +impl SpecBlockResult { + fn from_real(result: &evolve_stf::results::BlockResult) -> Self { + Self { + tx_results: result + .tx_results + .iter() + .map(SpecTxResult::from_real) + .collect(), + gas_used: result.gas_used, + txs_skipped: result.txs_skipped as u64, + } + } +} + +impl SpecTxResult { + fn from_real(result: &evolve_stf::results::TxResult) -> Self { + Self { + result: SpecResult::from_real(&result.response), + gas_used: result.gas_used, + } + } +} + +impl SpecResult { + fn from_real(result: &SdkResult) -> Self { + match result { + Ok(_) => Self { + ok: true, + err_code: 0, + }, + Err(err) => Self { + ok: false, + err_code: normalize_error_code(err.id), + }, + } + } +} + +fn normalize_error_code(err_id: u16) -> u64 { + if err_id == evolve_stf::ERR_OUT_OF_GAS.id { + 0x01 + } else { + err_id as u64 + } +} + +#[quint_run( + spec = "../../../specs/stf_core.qnt", + main = "stf", + init = "init", + step = "qc_step", + max_samples = 8, + max_steps = 10, + seed = "0x42" +)] +fn quint_core_qc_run() -> impl Driver { + CoreDriver::default() +} diff --git a/crates/app/stf/tests/quint_post_tx_connect.rs b/crates/app/stf/tests/quint_post_tx_connect.rs new file mode 100644 index 0000000..26251f6 --- /dev/null +++ b/crates/app/stf/tests/quint_post_tx_connect.rs @@ -0,0 +1,376 @@ +//! `quint_connect` pilot for `specs/stf_post_tx.qnt`. +//! +//! This uses `quint run --mbt` rather than `quint test`: with Quint 0.30.0, the +//! plain `test` traces do not include `mbt::actionTaken`/`mbt::nondetPicks`, +//! which `quint_connect` needs in order to replay steps. + +use anyhow::anyhow; +use evolve_core::runtime_api::ACCOUNT_IDENTIFIER_PREFIX; +use evolve_core::storage_api::{StorageSetRequest, STORAGE_ACCOUNT_ID}; +use evolve_core::{ + AccountCode, AccountId, BlockContext, Environment, EnvironmentQuery, ErrorCode, FungibleAsset, + InvokeRequest, InvokeResponse, Message, SdkResult, +}; +use evolve_stf::Stf; +use evolve_stf_traits::{Block as BlockTrait, PostTxExecution, Transaction, WritableKV}; +use quint_connect::*; +use serde::Deserialize; +use std::collections::{BTreeMap, BTreeSet}; + +mod quint_common; +use quint_common::{ + default_gas_config, extract_account_storage, register_account, CodeStore, InMemoryStorage, + NoopBegin, NoopEnd, NoopValidator, TestMsg, +}; + +const SPEC_ERR_EXECUTION: u16 = 200; +const SPEC_ERR_POST_TX: u16 = 999; +const TEST_SENDER: u64 = 200; +const WRITE_KEY: &[u8] = &[1]; +const WRITE_VALUE: &[u8] = &[11]; + +#[derive(Clone, Debug, Deserialize, Eq, PartialEq)] +struct SpecState { + storage: BTreeMap, Vec>>, + accounts: BTreeSet, + last_result: SpecBlockResult, +} + +#[derive(Clone, Debug, Default, Deserialize, Eq, PartialEq)] +struct SpecBlockResult { + tx_results: Vec, + gas_used: u64, +} + +#[derive(Clone, Debug, Deserialize, Eq, PartialEq)] +struct SpecTxResult { + result: SpecResult, + gas_used: u64, +} + +#[derive(Clone, Debug, Deserialize, Eq, PartialEq)] +struct SpecResult { + ok: bool, + err_code: u64, +} + +impl State for SpecState { + fn from_driver(driver: &PostTxDriver) -> Result { + let accounts = driver.accounts(); + let storage = accounts + .iter() + .copied() + .map(|account| { + ( + account, + extract_account_storage(&driver.storage, AccountId::from_u64(account)) + .into_iter() + .map(|(key, value)| { + ( + key.into_iter().map(u64::from).collect(), + value.into_iter().map(u64::from).collect(), + ) + }) + .collect(), + ) + }) + .collect(); + + Ok(Self { + storage, + accounts, + last_result: driver.last_result.clone(), + }) + } +} + +#[derive(Clone, Debug)] +struct TestTx { + sender: AccountId, + recipient: AccountId, + request: InvokeRequest, + gas_limit: u64, + funds: Vec, + reject_post_tx: bool, +} + +impl Transaction for TestTx { + fn sender(&self) -> AccountId { + self.sender + } + fn recipient(&self) -> AccountId { + self.recipient + } + fn request(&self) -> &InvokeRequest { + &self.request + } + fn gas_limit(&self) -> u64 { + self.gas_limit + } + fn funds(&self) -> &[FungibleAsset] { + &self.funds + } + fn compute_identifier(&self) -> [u8; 32] { + [0u8; 32] + } +} + +#[derive(Clone)] +struct TestBlock { + height: u64, + time: u64, + txs: Vec, +} + +impl BlockTrait for TestBlock { + fn context(&self) -> BlockContext { + BlockContext::new(self.height, self.time) + } + fn txs(&self) -> &[TestTx] { + &self.txs + } +} + +#[derive(Default)] +struct RejectingPostTx; + +impl PostTxExecution for RejectingPostTx { + fn after_tx_executed( + tx: &TestTx, + _gas_consumed: u64, + tx_result: &SdkResult, + _env: &mut dyn Environment, + ) -> SdkResult<()> { + if tx.reject_post_tx && tx_result.is_ok() { + return Err(ErrorCode::new(SPEC_ERR_POST_TX)); + } + Ok(()) + } +} + +#[derive(Default)] +struct TestAccount; + +impl AccountCode for TestAccount { + fn identifier(&self) -> String { + "test_account".to_string() + } + fn schema(&self) -> evolve_core::schema::AccountSchema { + evolve_core::schema::AccountSchema::new("TestAccount", "test_account") + } + fn init( + &self, + _env: &mut dyn Environment, + _request: &InvokeRequest, + ) -> SdkResult { + InvokeResponse::new(&()) + } + fn execute( + &self, + env: &mut dyn Environment, + request: &InvokeRequest, + ) -> SdkResult { + let msg: TestMsg = request.get()?; + let set = StorageSetRequest { + key: msg.key.clone(), + value: Message::from_bytes(msg.value.clone()), + }; + env.do_exec(STORAGE_ACCOUNT_ID, &InvokeRequest::new(&set)?, vec![])?; + if msg.fail_after_write { + return Err(ErrorCode::new(SPEC_ERR_EXECUTION)); + } + InvokeResponse::new(&()) + } + fn query( + &self, + _env: &mut dyn EnvironmentQuery, + _request: &InvokeRequest, + ) -> SdkResult { + InvokeResponse::new(&()) + } +} + +#[derive(Default)] +struct PostTxDriver { + storage: InMemoryStorage, + last_result: SpecBlockResult, +} + +impl Driver for PostTxDriver { + type State = SpecState; + + fn step(&mut self, step: &Step) -> Result { + switch!(step { + init => { self.reset()?; }, + register_account(recipient: u64) => { self.register_account(recipient)?; }, + apply_registered_tx( + recipient: u64, + gas_limit: u64, + fail_e: bool, + reject_pt: bool + ) => { self.apply_registered_tx(recipient, gas_limit, fail_e, reject_pt)?; } + }) + } +} + +impl PostTxDriver { + fn reset(&mut self) -> Result { + self.storage = InMemoryStorage::default(); + self.last_result = SpecBlockResult::default(); + Ok(()) + } + + fn register_account(&mut self, recipient: u64) -> Result { + register_account( + &mut self.storage, + AccountId::from_u64(recipient), + "test_account", + ); + Ok(()) + } + + fn apply_registered_tx( + &mut self, + recipient: u64, + gas_limit: u64, + fail_e: bool, + reject_pt: bool, + ) -> Result { + let msg = TestMsg { + key: WRITE_KEY.to_vec(), + value: WRITE_VALUE.to_vec(), + fail_after_write: fail_e, + }; + let tx = TestTx { + sender: AccountId::from_u64(TEST_SENDER), + recipient: AccountId::from_u64(recipient), + request: InvokeRequest::new(&msg) + .map_err(|err| anyhow!("failed to serialize test request: {err:?}"))?, + gas_limit, + funds: vec![], + reject_post_tx: reject_pt, + }; + let block = TestBlock { + height: 1, + time: 0, + txs: vec![tx], + }; + + let stf = build_stf(); + let codes = build_codes(); + let (result, exec_state) = stf.apply_block(&self.storage, &codes, &block); + let changes = exec_state + .into_changes() + .map_err(|err| anyhow!("failed to extract execution changes: {err:?}"))?; + self.storage + .apply_changes(changes) + .map_err(|err| anyhow!("failed to apply execution changes: {err:?}"))?; + self.last_result = SpecBlockResult::from_real(&result); + + Ok(()) + } + + fn accounts(&self) -> BTreeSet { + self.storage + .data + .iter() + .filter(|(key, value)| { + key.first() == Some(&ACCOUNT_IDENTIFIER_PREFIX) + && Message::from_bytes((*value).clone()) + .get::() + .ok() + .as_deref() + == Some("test_account") + }) + .filter_map(|(key, _)| { + let bytes = key.get(1..33)?; + let account_bytes: [u8; 32] = bytes.try_into().ok()?; + Some(account_id_to_u64(AccountId::from_bytes(account_bytes))) + }) + .collect() + } +} + +fn build_codes() -> CodeStore { + let mut codes = CodeStore::new(); + codes.add_code(TestAccount); + codes +} + +fn build_stf( +) -> Stf, NoopValidator, NoopEnd, RejectingPostTx> { + Stf::new( + NoopBegin::::default(), + NoopEnd, + NoopValidator::::default(), + RejectingPostTx, + default_gas_config(), + ) +} + +fn account_id_to_u64(account: AccountId) -> u64 { + let bytes = account.as_bytes(); + u64::from_be_bytes( + bytes[24..32] + .try_into() + .expect("account id must be 32 bytes"), + ) +} + +impl SpecBlockResult { + fn from_real(result: &evolve_stf::results::BlockResult) -> Self { + Self { + tx_results: result + .tx_results + .iter() + .map(SpecTxResult::from_real) + .collect(), + gas_used: result.gas_used, + } + } +} + +impl SpecTxResult { + fn from_real(result: &evolve_stf::results::TxResult) -> Self { + Self { + result: SpecResult::from_real(&result.response), + gas_used: result.gas_used, + } + } +} + +impl SpecResult { + fn from_real(result: &SdkResult) -> Self { + match result { + Ok(_) => Self { + ok: true, + err_code: 0, + }, + Err(err) => Self { + ok: false, + err_code: normalize_error_code(err.id), + }, + } + } +} + +fn normalize_error_code(err_id: u16) -> u64 { + if err_id == evolve_stf::ERR_OUT_OF_GAS.id { + 0x01 + } else { + err_id as u64 + } +} + +#[quint_run( + spec = "../../../specs/stf_post_tx.qnt", + main = "stf_post_tx", + init = "init", + step = "qc_step", + max_samples = 8, + max_steps = 8, + seed = "0x42" +)] +fn quint_post_tx_qc_run() -> impl Driver { + PostTxDriver::default() +} diff --git a/justfile b/justfile index 3852d5f..75eaa53 100644 --- a/justfile +++ b/justfile @@ -49,6 +49,12 @@ check: # QUALITY # ============================================================================ +# Generate token module Rust code from Quint spec +[group('build')] +gen-token: + cargo run -p evolve_specgen -- specs/token.qnt crates/app/sdk/extensions/token/src/generated/token_from_spec.rs + cargo fmt --all + # Format all code [group('quality')] fmt: @@ -213,6 +219,28 @@ sim-debug trace: sim-report trace: cargo run -p evolve-sim -- report --trace {{trace}} +# ============================================================================ +# SPEC CONFORMANCE +# ============================================================================ + +# Run core STF Quint spec tests and live `quint_connect` conformance +[group('spec')] +spec-test-core: + quint test specs/stf_core.qnt + cargo test -p evolve_stf --test quint_core_connect + +# Run extended STF model specs backed by live `quint_connect` +[group('spec')] +spec-test-extended: + quint test specs/stf_post_tx.qnt + cargo test -p evolve_stf --test quint_post_tx_connect + +# Run full STF spec suite (core + extended) +[group('spec')] +spec-test: + just spec-test-core + just spec-test-extended + # ============================================================================ # BENCHMARKS # ============================================================================ diff --git a/specs/stf_call_depth.qnt b/specs/stf_call_depth.qnt new file mode 100644 index 0000000..90bfc3f --- /dev/null +++ b/specs/stf_call_depth.qnt @@ -0,0 +1,193 @@ +// Evolve SDK - STF Call Depth Specification +// +// Models nested do_exec calls with call depth accumulation. +// In the runtime, each do_exec/branch_exec increments call_depth +// via saturating_add. Calls are rejected when depth >= MAX_CALL_DEPTH. +// +// This spec models: +// - Call stack growth through nested execution +// - Depth enforcement at MAX_CALL_DEPTH (64) +// - Stack unwinding on return +// - Invariant: depth never exceeds the limit + +module stf_call_depth { + type AccountId = int + type Result = { ok: bool, err_code: int } + + val OK: Result = { ok: true, err_code: 0 } + pure def Err(code: int): Result = { ok: false, err_code: code } + + val ERR_CALL_DEPTH: int = 0x14 + val MAX_CALL_DEPTH: int = 64 + + /// The set of account IDs for nondeterministic exploration. + val ACCOUNTS: Set[AccountId] = Set(1, 2, 3) + + // + // === State === + // + + /// Call stack: tracks the chain of nested calls. + /// Length of this list is the current call depth. + var call_stack: List[AccountId] + + /// Result of the last attempted operation. + var last_result: Result + + // + // === Actions === + // + + action init = all { + call_stack' = List(), + last_result' = OK, + } + + /// Nested call. In the runtime this is do_exec -> branch_exec + /// which increments call_depth. Succeeds only if depth < MAX. + action do_exec(target: AccountId): bool = all { + // Guard: depth check happens BEFORE checkpoint is taken + call_stack.length() < MAX_CALL_DEPTH, + // Update: push target onto call stack (depth increments) + call_stack' = call_stack.append(target), + last_result' = OK, + } + + /// Call rejected because depth limit is reached. + action do_exec_rejected(target: AccountId): bool = all { + // Guard: at or above the limit + call_stack.length() >= MAX_CALL_DEPTH, + // No state change: rejected before any checkpoint + call_stack' = call_stack, + last_result' = Err(ERR_CALL_DEPTH), + } + + /// Return from a call (pop the stack). + action return_from_call: bool = all { + // Guard: must have an active call + call_stack.length() > 0, + // Update: pop the last call + call_stack' = call_stack.slice(0, call_stack.length() - 1), + last_result' = OK, + } + + /// Stutter step: no state change. + action stutter: bool = all { + call_stack' = call_stack, + last_result' = last_result, + } + + // + // === Nondeterministic step for model checking === + // + + action step = { + nondet target = ACCOUNTS.oneOf() + any { + do_exec(target), + do_exec_rejected(target), + return_from_call, + } + } + + // + // === Invariants === + // + + /// INV-1: Call stack depth never exceeds MAX_CALL_DEPTH. + val depthBounded: bool = call_stack.length() <= MAX_CALL_DEPTH + + /// INV-2: A rejected call always produces ERR_CALL_DEPTH. + val rejectionCorrect: bool = + not(last_result.ok) implies last_result.err_code == ERR_CALL_DEPTH + + /// INV-3: Call depth is non-negative (structural with List). + val depthNonNegative: bool = call_stack.length() >= 0 + + // + // === False-invariant witnesses (should be violated) === + // + + /// Should be violated: proves calls can happen. + val witnessNoCalls: bool = call_stack.length() == 0 + + /// Should be violated: proves nested calls are reachable. + val witnessAlwaysShallow: bool = call_stack.length() < 3 + + /// Should be violated: proves call rejection is reachable. + val witnessNoRejections: bool = last_result.ok + + // + // === Tests === + // + + /// Test: single call succeeds and increments depth. + run singleCallTest = + init + .then(do_exec(1)) + .then(all { + assert(call_stack.length() == 1), + assert(last_result.ok == true), + assert(depthBounded), + stutter, + }) + + /// Test: nested calls accumulate depth correctly. + run nestedCallsTest = + init + .then(do_exec(1)) + .then(do_exec(2)) + .then(do_exec(3)) + .then(all { + assert(call_stack.length() == 3), + assert(call_stack[0] == 1), + assert(call_stack[1] == 2), + assert(call_stack[2] == 3), + assert(depthBounded), + stutter, + }) + + /// Test: return_from_call decrements depth. + run returnUnwindsStackTest = + init + .then(do_exec(1)) + .then(do_exec(2)) + .then(return_from_call) + .then(all { + assert(call_stack.length() == 1), + assert(call_stack[0] == 1), + stutter, + }) + + /// Test: full unwind returns to empty stack. + run fullUnwindTest = + init + .then(do_exec(1)) + .then(do_exec(2)) + .then(return_from_call) + .then(return_from_call) + .then(all { + assert(call_stack.length() == 0), + stutter, + }) + + /// Test: cannot return from empty stack. + run cannotReturnFromEmptyTest = + init + .then(return_from_call) + .fail() + + /// Test: recursive calls (same account) track depth. + run recursiveCallsTest = + init + .then(do_exec(1)) + .then(do_exec(1)) + .then(do_exec(1)) + .then(all { + assert(call_stack.length() == 3), + assert(call_stack[0] == 1), + assert(call_stack[1] == 1), + assert(call_stack[2] == 1), + stutter, + }) +} diff --git a/specs/stf_core.qnt b/specs/stf_core.qnt new file mode 100644 index 0000000..58c8702 --- /dev/null +++ b/specs/stf_core.qnt @@ -0,0 +1,779 @@ +// Evolve SDK - State Transition Function (STF) Specification +// +// This Quint spec models the core STF logic: +// - Block lifecycle: begin_block -> process txs -> end_block +// - Transaction lifecycle: bootstrap -> validate -> execute -> post_tx +// - Gas metering with per-tx limits and block gas limits +// - Storage overlay with checkpoint/restore for atomicity +// - Determinism: same block on same state => same result +// +// The model abstracts away concrete account code and message formats, +// focusing on the STF orchestration and invariants. + +module stf { + + // + // === Types === + // + + type AccountId = int + type Key = List[int] + type Value = List[int] + + /// Result of an operation: either Ok or an error code. + type Result = { ok: bool, err_code: int } + + val OK: Result = { ok: true, err_code: 0 } + pure def Err(code: int): Result = { ok: false, err_code: code } + + // Error codes (matching Rust implementation) + val ERR_OUT_OF_GAS: int = 0x01 + val ERR_CALL_DEPTH: int = 0x02 + val ERR_VALIDATION: int = 100 + val ERR_EXECUTION: int = 200 + val ERR_POST_TX: int = 999 + val ERR_BOOTSTRAP: int = 300 + + /// Storage gas configuration: cost per byte for get/set/remove. + type GasConfig = { + get_charge: int, + set_charge: int, + remove_charge: int, + } + + /// A transaction to be executed. + type Tx = { + sender: AccountId, + recipient: AccountId, + gas_limit: int, + // Abstract payload: key/value the tx wants to write + write_key: Key, + write_value: Value, + // Control flags for modeling different outcomes + fail_validate: bool, + fail_execute: bool, + needs_bootstrap: bool, + fail_bootstrap: bool, + } + + /// A block containing transactions and context. + type Block = { + height: int, + time: int, + txs: List[Tx], + gas_limit: int, + } + + /// Result of a single transaction execution. + type TxResult = { + result: Result, + gas_used: int, + } + + /// Result of block execution. + type BlockResult = { + tx_results: List[TxResult], + gas_used: int, + txs_skipped: int, + } + + // + // === State === + // + + /// The persistent key-value store. Maps (account_id, key) -> value. + var storage: AccountId -> (Key -> Value) + + /// Set of registered account IDs (have account code assigned). + var accounts: Set[AccountId] + + /// Current block height (monotonically increasing). + var block_height: int + + /// The last block result produced. + var last_result: BlockResult + + /// Ghost: number of txs submitted in the last applied block. + var last_block_tx_count: int + + /// Gas configuration (fixed at construction). + val gas_config: GasConfig = { get_charge: 1, set_charge: 1, remove_charge: 1 } + + // + // === Constants for model checking === + // + + val MC_ACCOUNTS: Set[AccountId] = Set(100, 101, 200, 201) + val MC_GAS_LIMITS: Set[int] = Set(1, 40, 100, 10000) + val MC_BLOCK_GAS_LIMITS: Set[int] = Set(30, 70, 1000, 1000000) + + // + // === Pure helpers === + // + + /// AccountId is canonical 32-byte storage in the Rust implementation. + /// The real storage key is `account_id_bytes ++ user_key`. + val ACCOUNT_ID_BYTE_SIZE: int = 32 + val ACCOUNT_CODE_PREFIX_SIZE: int = 1 + val BORSH_LEN_PREFIX_SIZE: int = 4 + val TEST_ACCOUNT_CODE_ID_LEN: int = 12 // "test_account" + + /// Compute gas cost for a storage write operation. + /// Real formula: set_charge * (full_key_len + 1 + value_len + 1) + /// where full_key_len = ACCOUNT_ID_BYTE_SIZE + user_key.length() + pure def write_gas_cost(config: GasConfig, key: Key, value: Value): int = + config.set_charge * (ACCOUNT_ID_BYTE_SIZE + key.length() + 1 + value.length() + 1) + + /// Gas cost for sender bootstrap account-code registration. + /// Real runtime charges storage set gas for: + /// key = ACCOUNT_IDENTIFIER_PREFIX (1 byte) ++ account_id (32 bytes) + /// value = Borsh-encoded code id string ("test_account" => 4-byte len + 12 bytes) + pure def bootstrap_gas_cost(config: GasConfig): int = + config.set_charge * ( + ACCOUNT_CODE_PREFIX_SIZE + ACCOUNT_ID_BYTE_SIZE + 1 + + BORSH_LEN_PREFIX_SIZE + TEST_ACCOUNT_CODE_ID_LEN + 1 + ) + + /// Determine whether a transaction's write would exceed its gas limit. + pure def would_exceed_gas(config: GasConfig, tx: Tx): bool = + write_gas_cost(config, tx.write_key, tx.write_value) > tx.gas_limit + + /// Process a single transaction against the current state. + /// Returns (tx_result, updated_account_storage, updated_accounts). + /// + /// Models the full tx lifecycle: + /// 1. Optional sender bootstrap (account registration) + /// 2. Sender existence check + /// 3. Validation + /// 4. Recipient existence check + /// 5. Execution (write to storage) + /// 6. Rollback on any failure + pure def process_tx( + config: GasConfig, + tx: Tx, + account_store: AccountId -> (Key -> Value), + registered: Set[AccountId], + ): { result: TxResult, store: AccountId -> (Key -> Value), accounts: Set[AccountId] } = + // Phase 0: Bootstrap sender if needed + val bootstrap_gas = bootstrap_gas_cost(config) + val bootstrap_result = + if (tx.needs_bootstrap and not(registered.contains(tx.sender))) + if (bootstrap_gas > tx.gas_limit) + // Bootstrap consumes storage gas first; if that exceeds the tx budget, + // the runtime returns out-of-gas before running account init. + { ok: false, err_code: ERR_OUT_OF_GAS, store: account_store, accounts: registered, gas: 0 } + else if (tx.fail_bootstrap) + // The runtime persists account registration before init runs, so an + // init failure still leaves the sender registered with empty storage. + { + ok: false, + err_code: ERR_BOOTSTRAP, + store: account_store.put(tx.sender, Map()), + accounts: registered.union(Set(tx.sender)), + gas: bootstrap_gas, + } + else + // Bootstrap succeeds: register sender and expose an empty user-store. + { ok: true, err_code: 0, store: account_store.put(tx.sender, Map()), accounts: registered.union(Set(tx.sender)), gas: bootstrap_gas } + else + // No bootstrap needed or already registered + { ok: true, err_code: 0, store: account_store, accounts: registered, gas: 0 } + + if (not(bootstrap_result.ok)) + // Bootstrap failed -> return the runtime-visible post-bootstrap state. + { + result: { result: Err(bootstrap_result.err_code), gas_used: bootstrap_result.gas }, + store: bootstrap_result.store, + accounts: bootstrap_result.accounts, + } + else + val current_accounts = bootstrap_result.accounts + val current_store = bootstrap_result.store + val gas_after_bootstrap = bootstrap_result.gas + + // Phase 1: Validation + // In the real runtime the pluggable TxValidator verifies signatures by + // calling into the sender's account code. If the sender is not + // registered (no account code), validation fails. + if (tx.fail_validate or not(current_accounts.contains(tx.sender))) + { + result: { result: Err(ERR_VALIDATION), gas_used: gas_after_bootstrap }, + store: current_store, + accounts: current_accounts, + } + else + // Phase 2: Execution - compute gas for the write + val gas_needed = write_gas_cost(config, tx.write_key, tx.write_value) + val total_gas = gas_after_bootstrap + gas_needed + + if (total_gas > tx.gas_limit) + // Out of gas: the real GasCounter does NOT increment gas_used on + // a failed consume_gas call. So gas_used stays at its pre-call value. + { + result: { result: Err(ERR_OUT_OF_GAS), gas_used: gas_after_bootstrap }, + store: current_store, + accounts: current_accounts, + } + else if (tx.fail_execute) + // Execution error after write -> rollback + { + result: { result: Err(ERR_EXECUTION), gas_used: total_gas }, + store: current_store, + accounts: current_accounts, + } + else + // Phase 3: Write succeeds -> apply to storage + val recipient_store = + if (current_store.keys().contains(tx.recipient)) + current_store.get(tx.recipient) + else + Map() + val updated_recipient = recipient_store.put(tx.write_key, tx.write_value) + val updated_store = current_store.put(tx.recipient, updated_recipient) + { + result: { result: OK, gas_used: total_gas }, + store: updated_store, + accounts: current_accounts, + } + + /// Process all transactions in a block sequentially, enforcing block gas limit. + pure def process_block( + config: GasConfig, + block: Block, + account_store: AccountId -> (Key -> Value), + registered: Set[AccountId], + ): { result: BlockResult, store: AccountId -> (Key -> Value), accounts: Set[AccountId] } = + val init_state = { + tx_results: List(), + cumulative_gas: 0, + txs_skipped: 0, + store: account_store, + accounts: registered, + stopped: false, + } + val final_state = block.txs.foldl(init_state, (acc, tx) => + if (acc.stopped) + // Already hit block gas limit, skip remaining + acc.with("txs_skipped", acc.txs_skipped + 1) + else + // Check if this tx would exceed block gas limit (pre-execution check) + if (acc.cumulative_gas + tx.gas_limit > block.gas_limit) + acc.with("txs_skipped", acc.txs_skipped + 1) + else + val tx_out = process_tx(config, tx, acc.store, acc.accounts) + val new_cumulative = acc.cumulative_gas + tx_out.result.gas_used + val should_stop = new_cumulative >= block.gas_limit + { + tx_results: acc.tx_results.append(tx_out.result), + cumulative_gas: new_cumulative, + txs_skipped: acc.txs_skipped, + store: tx_out.store, + accounts: tx_out.accounts, + stopped: should_stop, + } + ) + { + result: { + tx_results: final_state.tx_results, + gas_used: final_state.cumulative_gas, + txs_skipped: final_state.txs_skipped, + }, + store: final_state.store, + accounts: final_state.accounts, + } + + // + // === Actions (state transitions) === + // + + action init = all { + storage' = Map(), + accounts' = Set(), + block_height' = 0, + last_result' = { tx_results: List(), gas_used: 0, txs_skipped: 0 }, + last_block_tx_count' = 0, + } + + /// Apply a block to the current state. + action apply_block(block: Block): bool = + val out = process_block(gas_config, block, storage, accounts) + all { + // Block height must be monotonically increasing. + block.height > block_height, + block.gas_limit > 0, + storage' = out.store, + accounts' = out.accounts, + block_height' = block.height, + last_result' = out.result, + last_block_tx_count' = block.txs.length(), + } + + /// Driver-friendly block wrapper for `quint_connect`. + /// The STF can only execute against accounts with registered code, so this + /// wrapper aligns the model with the real runtime by requiring a registered recipient. + action apply_registered_block( + sender: AccountId, + recipient: AccountId, + gas_limit: int, + block_gas: int, + fail_v: bool, + fail_e: bool, + needs_b: bool, + fail_b: bool, + ): bool = + val tx: Tx = { + sender: sender, + recipient: recipient, + gas_limit: gas_limit, + write_key: K1, + write_value: V1, + fail_validate: fail_v, + fail_execute: fail_e, + needs_bootstrap: needs_b, + fail_bootstrap: fail_b, + } + all { + accounts.contains(recipient), + apply_block({ + height: block_height + 1, + time: 0, + txs: [tx], + gas_limit: block_gas, + }), + } + + /// Register an account (e.g., during genesis). + action register_account(id: AccountId): bool = all { + not(accounts.contains(id)), + storage' = storage.put(id, Map()), + accounts' = accounts.union(Set(id)), + block_height' = block_height, + last_result' = last_result, + last_block_tx_count' = last_block_tx_count, + } + + // + // === Invariants === + // + + /// INV-1: Block height is non-negative. + /// Monotonicity is enforced structurally by the guard block.height > block_height + /// in apply_block. This invariant checks the weaker non-negativity property. + val height_non_negative: bool = block_height >= 0 + + /// INV-2: Total gas reported equals sum of individual tx gas. + val gas_accounting: bool = + val sum = last_result.tx_results.foldl(0, (acc, tr) => acc + tr.gas_used) + last_result.gas_used == sum + + /// INV-3: Number of results + skipped = number of txs submitted. + val result_completeness: bool = + last_result.tx_results.length() + last_result.txs_skipped == last_block_tx_count + + /// INV-4: Failed transactions do not modify storage. + /// (Encoded structurally: process_tx returns the original store on failure.) + + /// INV-5: Only registered accounts appear as storage keys. + val storage_accounts_registered: bool = + storage.keys().forall(id => accounts.contains(id)) + + /// INV-6: Gas used is always non-negative. + val gas_non_negative: bool = + last_result.tx_results.foldl(true, (acc, tr) => acc and tr.gas_used >= 0) + + // + // === False-invariant witnesses (should be violated) === + // + + /// Should be violated: proves blocks with txs are processed. + val witnessNoTxsProcessed: bool = last_result.tx_results.length() == 0 + + /// Should be violated: proves successful txs can write to storage. + val witnessStorageNeverWritten: bool = + storage.keys().forall(id => storage.get(id) == Map()) + + /// Should be violated: proves block gas limit causes skips. + val witnessNoSkippedTxs: bool = last_result.txs_skipped == 0 + + /// Should be violated: proves bootstrap can register new accounts. + val witnessNoBootstrap: bool = accounts.size() <= 1 + + // + // === Temporal Properties === + // + + /// PROP-1: Determinism - same block on same state produces identical results. + /// This is ensured structurally: all functions are pure, no randomness, + /// no non-deterministic collection iteration (BTreeMap in Rust, ordered Map in Quint). + + /// PROP-2: If a transaction has fail_validate=true, it always returns ERR_VALIDATION. + /// PROP-3: If a transaction runs out of gas, it always returns ERR_OUT_OF_GAS. + /// PROP-4: Successful transactions always produce storage changes. + /// These are verified by the process_tx function structure. + + // + // === Nondeterministic step for model checking === + // + + action step = { + nondet id = MC_ACCOUNTS.oneOf() + nondet sender = MC_ACCOUNTS.oneOf() + nondet recipient = MC_ACCOUNTS.oneOf() + nondet gas_limit = MC_GAS_LIMITS.oneOf() + nondet block_gas = MC_BLOCK_GAS_LIMITS.oneOf() + nondet fail_v = Set(true, false).oneOf() + nondet fail_e = Set(true, false).oneOf() + nondet needs_b = Set(true, false).oneOf() + nondet fail_b = Set(true, false).oneOf() + val tx: Tx = { + sender: sender, recipient: recipient, gas_limit: gas_limit, + write_key: K1, write_value: V1, + fail_validate: fail_v, fail_execute: fail_e, + needs_bootstrap: needs_b, fail_bootstrap: fail_b, + } + any { + apply_block({ + height: block_height + 1, time: 0, + txs: [tx], gas_limit: block_gas, + }), + register_account(id), + } + } + + /// Alternate MBT step for `quint_connect`: keeps the same exploration + /// parameters, but only dispatches to runtime-valid block applications. + action qc_step = { + nondet id = MC_ACCOUNTS.oneOf() + nondet sender = MC_ACCOUNTS.oneOf() + nondet recipient = MC_ACCOUNTS.oneOf() + nondet gas_limit = MC_GAS_LIMITS.oneOf() + nondet block_gas = MC_BLOCK_GAS_LIMITS.oneOf() + nondet fail_v = Set(true, false).oneOf() + nondet fail_e = Set(true, false).oneOf() + nondet needs_b = Set(true, false).oneOf() + nondet fail_b = Set(true, false).oneOf() + any { + apply_registered_block(sender, recipient, gas_limit, block_gas, fail_v, fail_e, needs_b, fail_b), + register_account(id), + } + } + + // + // === Test helpers === + // + + // Byte-list keys/values for test readability + val K0: Key = [0] + val K1: Key = [1] + val K2: Key = [2] + val K3: Key = [3] + val V0: Value = [10] + val V1: Value = [11] + val V2: Value = [12] + val V3: Value = [13] + val V_OLD: Value = [20] + val V_NEW: Value = [21] + + /// Stutter step: keep all state unchanged (required to end a run). + action stutter: bool = all { + storage' = storage, + accounts' = accounts, + block_height' = block_height, + last_result' = last_result, + last_block_tx_count' = last_block_tx_count, + } + + // + // === Tests === + // + + /// Test: empty block produces no results and no state changes. + run emptyBlockTest = { + init + .then(register_account(100)) + .then(apply_block({ height: 1, time: 0, txs: List(), gas_limit: 1000000 })) + .then(all { + assert(last_result.tx_results.length() == 0), + assert(last_result.gas_used == 0), + assert(last_result.txs_skipped == 0), + assert(result_completeness), + stutter, + }) + } + + /// Test: successful transaction writes to storage. + run successfulTxTest = { + val tx1: Tx = { + sender: 100, recipient: 100, gas_limit: 10000, + write_key: K1, write_value: V1, + fail_validate: false, fail_execute: false, + needs_bootstrap: false, fail_bootstrap: false, + } + init + .then(register_account(100)) + .then(apply_block({ height: 1, time: 0, txs: [tx1], gas_limit: 1000000 })) + .then(all { + assert(last_result.tx_results.length() == 1), + assert(last_result.tx_results[0].result.ok == true), + assert(storage.get(100).get(K1) == V1), + assert(result_completeness), + stutter, + }) + } + + /// Test: validation failure does not modify storage. + run validationFailureTest = { + val tx1: Tx = { + sender: 100, recipient: 100, gas_limit: 10000, + write_key: K1, write_value: V1, + fail_validate: true, fail_execute: false, + needs_bootstrap: false, fail_bootstrap: false, + } + init + .then(register_account(100)) + .then(apply_block({ height: 1, time: 0, txs: [tx1], gas_limit: 1000000 })) + .then(all { + assert(last_result.tx_results[0].result.ok == false), + assert(last_result.tx_results[0].result.err_code == ERR_VALIDATION), + assert(storage.get(100) == Map()), + assert(result_completeness), + stutter, + }) + } + + /// Test: execution failure rolls back storage write. + run executionFailureRollbackTest = { + val tx1: Tx = { + sender: 100, recipient: 100, gas_limit: 10000, + write_key: K1, write_value: V1, + fail_validate: false, fail_execute: true, + needs_bootstrap: false, fail_bootstrap: false, + } + init + .then(register_account(100)) + .then(apply_block({ height: 1, time: 0, txs: [tx1], gas_limit: 1000000 })) + .then(all { + assert(last_result.tx_results[0].result.ok == false), + assert(last_result.tx_results[0].result.err_code == ERR_EXECUTION), + assert(storage.get(100) == Map()), + assert(result_completeness), + stutter, + }) + } + + /// Test: out-of-gas transaction fails and does not write. + run outOfGasTest = { + val tx1: Tx = { + sender: 100, recipient: 100, gas_limit: 1, + write_key: K1, write_value: V1, + fail_validate: false, fail_execute: false, + needs_bootstrap: false, fail_bootstrap: false, + } + init + .then(register_account(100)) + .then(apply_block({ height: 1, time: 0, txs: [tx1], gas_limit: 1000000 })) + .then(all { + assert(last_result.tx_results[0].result.ok == false), + assert(last_result.tx_results[0].result.err_code == ERR_OUT_OF_GAS), + assert(storage.get(100) == Map()), + assert(result_completeness), + stutter, + }) + } + + /// Test: block gas limit causes transactions to be skipped. + /// With Key=[1], Value=[11]: gas_cost = 1*(32+1+1+1+1) = 36 per tx. + /// tx1.gas_limit=40, tx2.gas_limit=40. Block gas_limit=70. + /// Pre-check: cumulative(0) + tx1.gas_limit(40) = 40 <= 70 -> execute tx1 (uses 36 gas). + /// Pre-check: cumulative(36) + tx2.gas_limit(40) = 76 > 70 -> skip tx2. + run blockGasLimitTest = { + val tx1: Tx = { + sender: 100, recipient: 100, gas_limit: 40, + write_key: K1, write_value: V1, + fail_validate: false, fail_execute: false, + needs_bootstrap: false, fail_bootstrap: false, + } + val tx2: Tx = { + sender: 100, recipient: 100, gas_limit: 40, + write_key: K2, write_value: V2, + fail_validate: false, fail_execute: false, + needs_bootstrap: false, fail_bootstrap: false, + } + init + .then(register_account(100)) + .then(apply_block({ height: 1, time: 0, txs: [tx1, tx2], gas_limit: 70 })) + .then(all { + assert(last_result.tx_results.length() == 1), + assert(last_result.txs_skipped == 1), + assert(last_result.tx_results[0].result.ok == true), + assert(result_completeness), + stutter, + }) + } + + /// Test: mixed block with success, validation failure, execution failure, OOG. + run mixedOutcomesTest = { + val tx_ok: Tx = { + sender: 100, recipient: 100, gas_limit: 10000, + write_key: K0, write_value: V0, + fail_validate: false, fail_execute: false, + needs_bootstrap: false, fail_bootstrap: false, + } + val tx_validate_fail: Tx = { + sender: 100, recipient: 100, gas_limit: 10000, + write_key: K1, write_value: V1, + fail_validate: true, fail_execute: false, + needs_bootstrap: false, fail_bootstrap: false, + } + val tx_exec_fail: Tx = { + sender: 100, recipient: 100, gas_limit: 10000, + write_key: K2, write_value: V2, + fail_validate: false, fail_execute: true, + needs_bootstrap: false, fail_bootstrap: false, + } + val tx_oog: Tx = { + sender: 100, recipient: 100, gas_limit: 1, + write_key: K3, write_value: V3, + fail_validate: false, fail_execute: false, + needs_bootstrap: false, fail_bootstrap: false, + } + init + .then(register_account(100)) + .then(apply_block({ + height: 1, time: 0, + txs: [tx_ok, tx_validate_fail, tx_exec_fail, tx_oog], + gas_limit: 1000000, + })) + .then(all { + assert(last_result.tx_results.length() == 4), + // tx_ok succeeds + assert(last_result.tx_results[0].result.ok == true), + // tx_validate_fail fails validation + assert(last_result.tx_results[1].result.err_code == ERR_VALIDATION), + // tx_exec_fail fails execution + assert(last_result.tx_results[2].result.err_code == ERR_EXECUTION), + // tx_oog fails with out of gas + assert(last_result.tx_results[3].result.err_code == ERR_OUT_OF_GAS), + // Only the first tx's write should be in storage + assert(storage.get(100).get(K0) == V0), + assert(not(storage.get(100).keys().contains(K1))), + assert(not(storage.get(100).keys().contains(K2))), + assert(not(storage.get(100).keys().contains(K3))), + assert(result_completeness), + stutter, + }) + } + + /// Test: sender bootstrap registers account before execution. + run bootstrapTest = { + val tx1: Tx = { + sender: 200, recipient: 100, gas_limit: 10000, + write_key: K1, write_value: V1, + fail_validate: false, fail_execute: false, + needs_bootstrap: true, fail_bootstrap: false, + } + init + .then(register_account(100)) + .then(apply_block({ height: 1, time: 0, txs: [tx1], gas_limit: 1000000 })) + .then(all { + assert(last_result.tx_results[0].result.ok == true), + // Sender should now be registered + assert(accounts.contains(200)), + assert(result_completeness), + stutter, + }) + } + + /// Test: failed bootstrap prevents execution. + run bootstrapFailureTest = { + val tx1: Tx = { + sender: 200, recipient: 100, gas_limit: 10000, + write_key: K1, write_value: V1, + fail_validate: false, fail_execute: false, + needs_bootstrap: true, fail_bootstrap: true, + } + init + .then(register_account(100)) + .then(apply_block({ height: 1, time: 0, txs: [tx1], gas_limit: 1000000 })) + .then(all { + assert(last_result.tx_results[0].result.ok == false), + assert(last_result.tx_results[0].result.err_code == ERR_BOOTSTRAP), + // Registration persists even though init failed. + assert(accounts.contains(200)), + assert(result_completeness), + stutter, + }) + } + + /// Test: unregistered sender (no bootstrap) fails validation. + /// In production, the validator queries the sender's account code for + /// signature verification. Without account code the query fails. + run unregisteredSenderTest = { + val tx1: Tx = { + sender: 200, recipient: 100, gas_limit: 10000, + write_key: K1, write_value: V1, + fail_validate: false, fail_execute: false, + needs_bootstrap: false, fail_bootstrap: false, + } + init + .then(register_account(100)) + .then(apply_block({ height: 1, time: 0, txs: [tx1], gas_limit: 1000000 })) + .then(all { + assert(last_result.tx_results[0].result.ok == false), + assert(last_result.tx_results[0].result.err_code == ERR_VALIDATION), + assert(storage.get(100) == Map()), + assert(result_completeness), + stutter, + }) + } + + /// Test: sequential blocks accumulate state correctly. + run multiBlockTest = { + val tx1: Tx = { + sender: 100, recipient: 100, gas_limit: 10000, + write_key: K1, write_value: V1, + fail_validate: false, fail_execute: false, + needs_bootstrap: false, fail_bootstrap: false, + } + val tx2: Tx = { + sender: 100, recipient: 100, gas_limit: 10000, + write_key: K2, write_value: V2, + fail_validate: false, fail_execute: false, + needs_bootstrap: false, fail_bootstrap: false, + } + init + .then(register_account(100)) + .then(apply_block({ height: 1, time: 0, txs: [tx1], gas_limit: 1000000 })) + .then(apply_block({ height: 2, time: 10, txs: [tx2], gas_limit: 1000000 })) + .then(all { + // Both writes should be present + assert(storage.get(100).get(K1) == V1), + assert(storage.get(100).get(K2) == V2), + assert(block_height == 2), + stutter, + }) + } + + /// Test: overwriting a key updates the value. + run overwriteTest = { + val tx1: Tx = { + sender: 100, recipient: 100, gas_limit: 10000, + write_key: K1, write_value: V_OLD, + fail_validate: false, fail_execute: false, + needs_bootstrap: false, fail_bootstrap: false, + } + val tx2: Tx = { + sender: 100, recipient: 100, gas_limit: 10000, + write_key: K1, write_value: V_NEW, + fail_validate: false, fail_execute: false, + needs_bootstrap: false, fail_bootstrap: false, + } + init + .then(register_account(100)) + .then(apply_block({ height: 1, time: 0, txs: [tx1, tx2], gas_limit: 1000000 })) + .then(all { + assert(storage.get(100).get(K1) == V_NEW), + stutter, + }) + } +} diff --git a/specs/stf_post_tx.qnt b/specs/stf_post_tx.qnt new file mode 100644 index 0000000..d943f49 --- /dev/null +++ b/specs/stf_post_tx.qnt @@ -0,0 +1,392 @@ +// Evolve SDK - STF Post-Tx Hook Specification +// +// Focus: post-tx handler semantics. +// In the runtime, the post-tx handler runs AFTER the execution checkpoint +// is dropped. A post-tx error overrides the tx response, but state changes +// from execution remain committed. +// +// This spec verifies: +// - Post-tx rejection keeps execution state changes +// - Post-tx rejection does not mask execution failures +// - Gas accounting remains correct across post-tx outcomes + +module stf_post_tx { + type AccountId = int + type Key = List[int] + type Value = List[int] + + type Result = { ok: bool, err_code: int } + val OK: Result = { ok: true, err_code: 0 } + pure def Err(code: int): Result = { ok: false, err_code: code } + + val ERR_OUT_OF_GAS: int = 0x01 + val ERR_EXECUTION: int = 200 + val ERR_POST_TX: int = 999 + + type GasConfig = { + set_charge: int, + } + + type Tx = { + recipient: AccountId, + gas_limit: int, + write_key: Key, + write_value: Value, + fail_execute: bool, + reject_post_tx: bool, + } + + type TxResult = { + result: Result, + gas_used: int, + } + + type BlockResult = { + tx_results: List[TxResult], + gas_used: int, + } + + // + // === State === + // + + var storage: AccountId -> (Key -> Value) + var accounts: Set[AccountId] + var last_result: BlockResult + + /// Constants for model checking. + val MC_ACCOUNTS: Set[AccountId] = Set(100, 101) + + val gas_config: GasConfig = { set_charge: 1 } + val ACCOUNT_ID_BYTE_SIZE: int = 32 + + pure def write_gas_cost(config: GasConfig, key: Key, value: Value): int = + config.set_charge * (ACCOUNT_ID_BYTE_SIZE + key.length() + 1 + value.length() + 1) + + pure def process_tx( + config: GasConfig, + tx: Tx, + account_store: AccountId -> (Key -> Value), + ): { result: TxResult, store: AccountId -> (Key -> Value) } = + val gas_needed = write_gas_cost(config, tx.write_key, tx.write_value) + if (gas_needed > tx.gas_limit) + { + result: { result: Err(ERR_OUT_OF_GAS), gas_used: 0 }, + store: account_store, + } + else if (tx.fail_execute) + // Runtime do_exec rolls back storage on execution error. + // Post-tx does not run after execution failure. + { + result: { result: Err(ERR_EXECUTION), gas_used: gas_needed }, + store: account_store, + } + else + // Execution succeeds and writes state. + val recipient_store = + if (account_store.keys().contains(tx.recipient)) + account_store.get(tx.recipient) + else + Map() + val updated_recipient = recipient_store.put(tx.write_key, tx.write_value) + val updated_store = account_store.put(tx.recipient, updated_recipient) + // Post-tx handler runs AFTER checkpoint is dropped. + // It can override the response but NOT roll back state. + { + result: { + result: if (tx.reject_post_tx) Err(ERR_POST_TX) else OK, + gas_used: gas_needed, + }, + store: updated_store, + } + + pure def process_block( + config: GasConfig, + txs: List[Tx], + account_store: AccountId -> (Key -> Value), + ): { result: BlockResult, store: AccountId -> (Key -> Value) } = + val init_state = { + tx_results: List(), + cumulative_gas: 0, + store: account_store, + } + val final_state = txs.foldl(init_state, (acc, tx) => + val tx_out = process_tx(config, tx, acc.store) + { + tx_results: acc.tx_results.append(tx_out.result), + cumulative_gas: acc.cumulative_gas + tx_out.result.gas_used, + store: tx_out.store, + } + ) + { + result: { tx_results: final_state.tx_results, gas_used: final_state.cumulative_gas }, + store: final_state.store, + } + + // + // === Actions === + // + + action init = all { + storage' = Map(), + accounts' = Set(), + last_result' = { tx_results: List(), gas_used: 0 }, + } + + action register_account(id: AccountId): bool = all { + not(accounts.contains(id)), + storage' = storage.put(id, Map()), + accounts' = accounts.union(Set(id)), + last_result' = last_result, + } + + action apply_txs(txs: List[Tx]): bool = + val out = process_block(gas_config, txs, storage) + all { + storage' = out.store, + accounts' = accounts, + last_result' = out.result, + } + + /// Driver-friendly wrapper for MBT: only execute txs against registered accounts. + action apply_registered_tx( + recipient: AccountId, + gas_limit: int, + fail_e: bool, + reject_pt: bool, + ): bool = + val tx: Tx = { + recipient: recipient, + gas_limit: gas_limit, + write_key: K1, + write_value: V1, + fail_execute: fail_e, + reject_post_tx: reject_pt, + } + all { + accounts.contains(recipient), + apply_txs([tx]), + } + + action stutter: bool = all { + storage' = storage, + accounts' = accounts, + last_result' = last_result, + } + + // + // === Nondeterministic step for model checking === + // + + action step = { + nondet recipient = MC_ACCOUNTS.oneOf() + nondet gas_limit = Set(1, 100, 10000).oneOf() + nondet fail_e = Set(true, false).oneOf() + nondet reject_pt = Set(true, false).oneOf() + val tx: Tx = { + recipient: recipient, + gas_limit: gas_limit, + write_key: K1, + write_value: V1, + fail_execute: fail_e, + reject_post_tx: reject_pt, + } + any { + apply_txs([tx]), + register_account(recipient), + } + } + + /// Alternate MBT step for `quint_connect`: aligns with STF requirement that + /// execution targets a registered account code. + action qc_step = { + nondet recipient = MC_ACCOUNTS.oneOf() + nondet gas_limit = Set(1, 100, 10000).oneOf() + nondet fail_e = Set(true, false).oneOf() + nondet reject_pt = Set(true, false).oneOf() + any { + apply_registered_tx(recipient, gas_limit, fail_e, reject_pt), + register_account(recipient), + } + } + + // + // === Invariants === + // + + /// INV-1: Gas accounting -- total equals sum of individual tx gas. + val gas_accounting: bool = + last_result.tx_results.foldl(0, (acc, tr) => acc + tr.gas_used) == last_result.gas_used + + /// INV-2: Gas is non-negative. + val gas_non_negative: bool = + last_result.tx_results.foldl(true, (acc, tr) => acc and tr.gas_used >= 0) + + /// INV-3: Only registered accounts have storage entries. + val storage_accounts_registered: bool = + storage.keys().forall(id => accounts.contains(id)) + + // + // === False-invariant witnesses (should be violated) === + // + + /// Should be violated: proves post-tx rejection path is reachable. + val witnessNoPostTxReject: bool = + last_result.tx_results.foldl(true, (acc, tr) => + acc and (tr.result.ok or tr.result.err_code != ERR_POST_TX)) + + /// Should be violated: proves execution happens. + val witnessNoExecution: bool = last_result.tx_results.length() == 0 + + /// Should be violated: proves successful txs write storage. + val witnessStorageEmpty: bool = + storage.keys().forall(id => storage.get(id) == Map()) + + // + // === Test helpers === + // + + val K1: Key = [1] + val V1: Value = [11] + val K2: Key = [2] + val V2: Value = [12] + + // + // === Named test expectation actions === + // + + action expect_post_tx_rejects_but_keeps_state: bool = all { + assert(last_result.tx_results.length() == 1), + assert(last_result.tx_results[0].result.ok == false), + assert(last_result.tx_results[0].result.err_code == ERR_POST_TX), + assert(storage.get(100).get(K1) == V1), + assert(gas_accounting), + stutter, + } + + action expect_post_tx_does_not_mask_exec_failure: bool = all { + assert(last_result.tx_results.length() == 1), + assert(last_result.tx_results[0].result.ok == false), + assert(last_result.tx_results[0].result.err_code == ERR_EXECUTION), + assert(storage.get(100) == Map()), + assert(gas_accounting), + stutter, + } + + action expect_happy_path: bool = all { + assert(last_result.tx_results[0].result.ok == true), + assert(storage.get(100).get(K1) == V1), + assert(gas_accounting), + stutter, + } + + action expect_mixed_post_tx: bool = all { + assert(last_result.tx_results.length() == 2), + assert(last_result.tx_results[0].result.err_code == ERR_POST_TX), + assert(storage.get(100).get(K1) == V1), + assert(last_result.tx_results[1].result.ok == true), + assert(storage.get(100).get(K2) == V2), + assert(gas_accounting), + stutter, + } + + action expect_out_of_gas_ignores_post_tx: bool = all { + assert(last_result.tx_results[0].result.err_code == ERR_OUT_OF_GAS), + assert(storage.get(100) == Map()), + assert(gas_accounting), + stutter, + } + + // + // === Tests === + // + + /// Core property: post-tx rejection keeps execution state changes. + /// This is the critical semantic: the handler runs after checkpoint drop. + run postTxRejectsButKeepsStateTest = { + val tx: Tx = { + recipient: 100, + gas_limit: 10000, + write_key: K1, + write_value: V1, + fail_execute: false, + reject_post_tx: true, + } + init + .then(register_account(100)) + .then(apply_txs([tx])) + .then(expect_post_tx_rejects_but_keeps_state) + } + + /// Post-tx does not mask execution failure (exec error takes precedence). + run postTxDoesNotMaskExecFailureTest = { + val tx: Tx = { + recipient: 100, + gas_limit: 10000, + write_key: K1, + write_value: V1, + fail_execute: true, + reject_post_tx: true, + } + init + .then(register_account(100)) + .then(apply_txs([tx])) + .then(expect_post_tx_does_not_mask_exec_failure) + } + + /// Happy path: no post-tx rejection, execution succeeds. + run happyPathTest = { + val tx: Tx = { + recipient: 100, + gas_limit: 10000, + write_key: K1, + write_value: V1, + fail_execute: false, + reject_post_tx: false, + } + init + .then(register_account(100)) + .then(apply_txs([tx])) + .then(expect_happy_path) + } + + /// Mixed block: one tx with post-tx rejection, one without. + run mixedPostTxTest = { + val tx_reject: Tx = { + recipient: 100, + gas_limit: 10000, + write_key: K1, + write_value: V1, + fail_execute: false, + reject_post_tx: true, + } + val tx_ok: Tx = { + recipient: 100, + gas_limit: 10000, + write_key: K2, + write_value: V2, + fail_execute: false, + reject_post_tx: false, + } + init + .then(register_account(100)) + .then(apply_txs([tx_reject, tx_ok])) + .then(expect_mixed_post_tx) + } + + /// Out-of-gas: post-tx flag is irrelevant since execution never completes. + run outOfGasIgnoresPostTxTest = { + val tx: Tx = { + recipient: 100, + gas_limit: 1, + write_key: K1, + write_value: V1, + fail_execute: false, + reject_post_tx: true, + } + init + .then(register_account(100)) + .then(apply_txs([tx])) + .then(expect_out_of_gas_ignores_post_tx) + } +}