diff --git a/crates/app/sdk/extensions/token/src/lib.rs b/crates/app/sdk/extensions/token/src/lib.rs index 1d3bda6..0b092ae 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..7bade5a 100644 --- a/crates/app/stf/Cargo.toml +++ b/crates/app/stf/Cargo.toml @@ -17,6 +17,8 @@ linkme = {version = "0.3", default-features = false, optional = true} [dev-dependencies] proptest = "1.4" +serde = { version = "1", features = ["derive"] } +serde_json = "1" [lints] workspace = true diff --git a/crates/app/stf/tests/quint_call_depth_conformance.rs b/crates/app/stf/tests/quint_call_depth_conformance.rs new file mode 100644 index 0000000..1baf370 --- /dev/null +++ b/crates/app/stf/tests/quint_call_depth_conformance.rs @@ -0,0 +1,315 @@ +//! Conformance tests: replay Quint ITF traces for stf_call_depth.qnt. +//! +//! The Quint spec models nested do_exec calls with a call_stack. This +//! conformance test uses a RecursiveAccount that calls itself N times, +//! verifying that the real STF matches the spec's depth enforcement. +//! +//! Run: +//! `quint test --main=stf_call_depth specs/stf_call_depth.qnt --out-itf "specs/traces/out_{test}_{seq}.itf.json"` +//! `cargo test -p evolve_stf --test quint_call_depth_conformance` + +use borsh::{BorshDeserialize, BorshSerialize}; +use evolve_core::{ + AccountCode, AccountId, BlockContext, Environment, EnvironmentQuery, FungibleAsset, + InvokableMessage, InvokeRequest, InvokeResponse, Message, SdkResult, +}; +use evolve_stf::gas::StorageGasConfig; +use evolve_stf::Stf; +use evolve_stf_traits::{Block as BlockTrait, PostTxExecution, Transaction, TxValidator}; +use serde::Deserialize; +use std::path::Path; + +mod quint_common; +use quint_common::{ + account_code_key, find_single_trace_file, read_itf_trace, CodeStore, InMemoryStorage, + ItfBigInt, NoopBegin, NoopEnd, +}; + +#[derive(Deserialize)] +struct ItfTrace { + states: Vec, +} + +#[derive(Deserialize)] +struct ItfState { + #[allow(dead_code)] + call_stack: Vec, + last_result: ItfResult, +} + +#[derive(Deserialize)] +struct ItfResult { + ok: bool, + #[allow(dead_code)] + err_code: ItfBigInt, +} + +#[derive(Clone, Debug, BorshSerialize, BorshDeserialize)] +struct RecurseMsg { + remaining: u16, +} + +impl InvokableMessage for RecurseMsg { + const FUNCTION_IDENTIFIER: u64 = 1; + const FUNCTION_IDENTIFIER_NAME: &'static str = "recurse"; +} + +#[derive(Clone, Debug)] +struct TestTx { + sender: AccountId, + recipient: AccountId, + request: InvokeRequest, + gas_limit: u64, + funds: Vec, +} + +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 + } + fn gas_limit(&self) -> u64 { + 1_000_000 + } +} + +#[derive(Default)] +struct NoopValidator; +impl TxValidator for NoopValidator { + fn validate_tx(&self, _tx: &TestTx, _env: &mut dyn Environment) -> SdkResult<()> { + Ok(()) + } +} + +#[derive(Default)] +struct NoopPostTx; +impl PostTxExecution for NoopPostTx { + fn after_tx_executed( + _tx: &TestTx, + _gas_consumed: u64, + _tx_result: &SdkResult, + _env: &mut dyn Environment, + ) -> SdkResult<()> { + Ok(()) + } +} + +#[derive(Default)] +struct RecursiveAccount; + +impl AccountCode for RecursiveAccount { + fn identifier(&self) -> String { + "recursive".to_string() + } + fn schema(&self) -> evolve_core::schema::AccountSchema { + evolve_core::schema::AccountSchema::new("RecursiveAccount", "recursive") + } + fn init( + &self, + _env: &mut dyn Environment, + _request: &InvokeRequest, + ) -> SdkResult { + InvokeResponse::new(&()) + } + fn execute( + &self, + env: &mut dyn Environment, + request: &InvokeRequest, + ) -> SdkResult { + let msg: RecurseMsg = request.get()?; + if msg.remaining == 0 { + return InvokeResponse::new(&()); + } + let next = RecurseMsg { + remaining: msg.remaining - 1, + }; + env.do_exec(env.whoami(), &InvokeRequest::new(&next)?, vec![])?; + InvokeResponse::new(&()) + } + fn query( + &self, + _env: &mut dyn EnvironmentQuery, + _request: &InvokeRequest, + ) -> SdkResult { + InvokeResponse::new(&()) + } +} + +const RECURSIVE_ACCOUNT: u128 = 100; +const TEST_SENDER: u128 = 200; + +/// Maps Quint test names to the recursive depth the Rust test should exercise. +/// +/// The Quint spec models individual do_exec/return_from_call steps. The Rust +/// conformance test uses a single recursive account that calls itself N times. +struct ConformanceCase { + test_name: &'static str, + requested_depth: u16, + expect_ok: bool, +} + +fn known_test_cases() -> Vec { + vec![ + // singleCallTest: one do_exec, stack=[1], OK + ConformanceCase { + test_name: "singleCallTest", + requested_depth: 1, + expect_ok: true, + }, + // nestedCallsTest: 3 nested calls, stack=[1,2,3], OK + ConformanceCase { + test_name: "nestedCallsTest", + requested_depth: 3, + expect_ok: true, + }, + // returnUnwindsStackTest: 2 calls + 1 return, OK (depth 2 succeeds) + ConformanceCase { + test_name: "returnUnwindsStackTest", + requested_depth: 2, + expect_ok: true, + }, + // fullUnwindTest: 2 calls + 2 returns, OK (depth 2 succeeds) + ConformanceCase { + test_name: "fullUnwindTest", + requested_depth: 2, + expect_ok: true, + }, + // recursiveCallsTest: 3 recursive self-calls, OK + ConformanceCase { + test_name: "recursiveCallsTest", + requested_depth: 3, + expect_ok: true, + }, + ] +} + +#[test] +fn quint_itf_call_depth_conformance() { + let traces_dir = Path::new(env!("CARGO_MANIFEST_DIR")).join("../../../specs/traces"); + if !traces_dir.exists() { + panic!( + "ITF traces not found at {}. Run: quint test --main=stf_call_depth \ + specs/stf_call_depth.qnt \ + --out-itf \"specs/traces/out_{{test}}_{{seq}}.itf.json\"", + traces_dir.display() + ); + } + + let test_cases = known_test_cases(); + for case in &test_cases { + let trace_file = find_single_trace_file(&traces_dir, case.test_name); + let trace: ItfTrace = read_itf_trace(&trace_file); + let spec_state = trace + .states + .last() + .expect("trace must have at least one state"); + let spec_result = &spec_state.last_result; + + assert_eq!( + spec_result.ok, case.expect_ok, + "{}: expected ok={} but trace says ok={}", + case.test_name, case.expect_ok, spec_result.ok + ); + + let gas_config = StorageGasConfig { + storage_get_charge: 1, + storage_set_charge: 1, + storage_remove_charge: 1, + }; + let stf = Stf::new( + NoopBegin::::default(), + NoopEnd, + NoopValidator, + NoopPostTx, + gas_config, + ); + + let mut storage = InMemoryStorage::default(); + let mut codes = CodeStore::new(); + codes.add_code(RecursiveAccount); + + let recursive_account = AccountId::new(RECURSIVE_ACCOUNT); + let code_id = "recursive".to_string(); + storage.data.insert( + account_code_key(recursive_account), + Message::new(&code_id).unwrap().into_bytes().unwrap(), + ); + + let msg = RecurseMsg { + remaining: case.requested_depth, + }; + let tx = TestTx { + sender: AccountId::new(TEST_SENDER), + recipient: recursive_account, + request: InvokeRequest::new(&msg).unwrap(), + gas_limit: 1_000_000, + funds: vec![], + }; + let block = TestBlock { + height: 1, + time: 0, + txs: vec![tx], + }; + + let (real_result, _) = stf.apply_block(&storage, &codes, &block); + assert_eq!( + real_result.tx_results.len(), + 1, + "{}: expected one tx result", + case.test_name + ); + + let real_ok = real_result.tx_results[0].response.is_ok(); + assert_eq!( + real_ok, case.expect_ok, + "{}: ok mismatch (real={real_ok}, expected={})", + case.test_name, case.expect_ok + ); + + if !case.expect_ok { + let real_err = real_result.tx_results[0] + .response + .as_ref() + .unwrap_err() + .id; + assert_eq!( + real_err, + evolve_stf::errors::ERR_CALL_DEPTH_EXCEEDED.id, + "{}: expected call depth error", + case.test_name + ); + } + + eprintln!("PASS: {}", case.test_name); + } +} diff --git a/crates/app/stf/tests/quint_common.rs b/crates/app/stf/tests/quint_common.rs new file mode 100644 index 0000000..545ba72 --- /dev/null +++ b/crates/app/stf/tests/quint_common.rs @@ -0,0 +1,135 @@ +#![allow(dead_code)] + +use evolve_core::runtime_api::ACCOUNT_IDENTIFIER_PREFIX; +use evolve_core::{AccountCode, AccountId, ErrorCode, ReadonlyKV}; +use evolve_stf_traits::{AccountsCodeStorage, BeginBlocker, EndBlocker, StateChange, WritableKV}; +use hashbrown::HashMap; +use serde::de::DeserializeOwned; +use serde::Deserialize; +use std::fs; +use std::path::Path; + +#[derive(Deserialize, Clone, Debug)] +pub struct ItfBigInt { + #[serde(rename = "#bigint")] + value: String, +} + +impl ItfBigInt { + pub fn as_i64(&self) -> i64 { + self.value.parse().unwrap() + } + pub fn as_u64(&self) -> u64 { + self.value.parse().unwrap() + } +} + +#[derive(Deserialize)] +pub struct ItfMap { + #[serde(rename = "#map")] + pub entries: Vec<(K, V)>, +} + +pub fn find_single_trace_file(traces_dir: &Path, test_name: &str) -> std::path::PathBuf { + let trace_files: Vec<_> = fs::read_dir(traces_dir) + .unwrap() + .filter_map(|e| e.ok()) + .filter(|e| { + let name = e.file_name().to_string_lossy().to_string(); + name.starts_with(&format!("out_{}_", test_name)) && name.ends_with(".itf.json") + }) + .collect(); + + assert_eq!( + trace_files.len(), + 1, + "{}: expected exactly 1 trace file, found {}", + test_name, + trace_files.len() + ); + trace_files[0].path() +} + +pub fn read_itf_trace(trace_path: &Path) -> T { + let trace_json = fs::read_to_string(trace_path).unwrap(); + serde_json::from_str(&trace_json).unwrap() +} + +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 evolve_core::Environment) {} +} + +#[derive(Default)] +pub struct NoopEnd; + +impl EndBlocker for NoopEnd { + fn end_block(&self, _env: &mut dyn evolve_core::Environment) {} +} + +pub struct CodeStore { + codes: HashMap>, +} + +impl CodeStore { + pub fn new() -> Self { + Self { + codes: HashMap::new(), + } + } + 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(()) + } +} + +pub fn account_code_key(account: AccountId) -> Vec { + let mut out = vec![ACCOUNT_IDENTIFIER_PREFIX]; + out.extend_from_slice(&account.as_bytes()); + out +} diff --git a/crates/app/stf/tests/quint_conformance.rs b/crates/app/stf/tests/quint_conformance.rs new file mode 100644 index 0000000..eed4a24 --- /dev/null +++ b/crates/app/stf/tests/quint_conformance.rs @@ -0,0 +1,791 @@ +//! Conformance tests: replay Quint ITF traces against the real STF. +//! +//! This test reads ITF (Informal Trace Format) JSON files generated by +//! `quint test specs/stf_core.qnt --out-itf ...` and replays each trace against +//! the actual STF implementation, asserting that the real execution matches +//! the spec's expected outcomes. +//! +//! Run: `cargo test -p evolve_stf --test quint_conformance` +//! Regenerate traces: `quint test --main=stf specs/stf_core.qnt --out-itf "specs/traces/out_{test}_{seq}.itf.json"` + +use borsh::{BorshDeserialize, BorshSerialize}; +use evolve_core::storage_api::{StorageSetRequest, STORAGE_ACCOUNT_ID}; +use evolve_core::{ + AccountCode, AccountId, BlockContext, Environment, EnvironmentQuery, ErrorCode, FungibleAsset, + InvokableMessage, InvokeRequest, InvokeResponse, Message, SdkResult, +}; +use evolve_stf::gas::StorageGasConfig; +use evolve_stf::Stf; +use evolve_stf_traits::{ + Block as BlockTrait, PostTxExecution, SenderBootstrap, Transaction, TxValidator, WritableKV, +}; +use hashbrown::HashMap; +use serde::Deserialize; +use std::path::Path; + +mod quint_common; +use quint_common::{ + account_code_key, find_single_trace_file, read_itf_trace, CodeStore, InMemoryStorage, + ItfBigInt, ItfMap, NoopBegin, NoopEnd, +}; + +// --------------------------------------------------------------------------- +// ITF deserialization types +// --------------------------------------------------------------------------- + +#[derive(Deserialize)] +struct ItfTrace { + states: Vec, +} + +#[derive(Deserialize)] +struct ItfState { + block_height: ItfBigInt, + last_result: ItfBlockResult, + #[allow(dead_code)] + last_block_tx_count: ItfBigInt, + storage: ItfMap, Vec>>, +} + +#[derive(Deserialize)] +struct ItfBlockResult { + gas_used: ItfBigInt, + tx_results: Vec, + txs_skipped: ItfBigInt, +} + +#[derive(Deserialize)] +struct ItfTxResult { + gas_used: ItfBigInt, + result: ItfResult, +} + +#[derive(Deserialize)] +struct ItfResult { + ok: bool, + err_code: ItfBigInt, +} + +// --------------------------------------------------------------------------- +// STF test infrastructure (mirrors model_tests in lib.rs) +// --------------------------------------------------------------------------- + +#[derive(Clone, Debug, BorshSerialize, BorshDeserialize)] +struct TestMsg { + key: Vec, + value: Vec, + fail_after_write: bool, +} + +impl InvokableMessage for TestMsg { + const FUNCTION_IDENTIFIER: u64 = 1; + const FUNCTION_IDENTIFIER_NAME: &'static str = "test_msg"; +} + +#[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(100)); + } + // Simulate production signature verification: query the sender's + // account code. If the sender is not registered this fails, mirroring + // the real validator that cannot verify signatures without account code. + let probe = TestMsg { + key: vec![], + value: vec![], + fail_after_write: false, + }; + env.do_query(tx.sender(), &InvokeRequest::new(&probe).unwrap()) + .map_err(|_| ErrorCode::new(100))?; + Ok(()) + } +} + +#[derive(Default)] +struct NoopPostTx; +impl PostTxExecution for NoopPostTx { + fn after_tx_executed( + _tx: &TestTx, + _gas_consumed: u64, + _tx_result: &SdkResult, + _env: &mut dyn Environment, + ) -> SdkResult<()> { + 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(300)); + } + 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(200)); + } + InvokeResponse::new(&()) + } + fn query( + &self, + _env: &mut dyn EnvironmentQuery, + _request: &InvokeRequest, + ) -> SdkResult { + InvokeResponse::new(&()) + } +} + +// --------------------------------------------------------------------------- +// Test case definitions (must match the Quint spec's run declarations) +// --------------------------------------------------------------------------- + +const SPEC_ERR_OUT_OF_GAS: i64 = 0x01; +const SPEC_ERR_VALIDATION: i64 = 100; +const SPEC_ERR_EXECUTION: i64 = 200; +const SPEC_ERR_BOOTSTRAP: i64 = 300; + +const TEST_ACCOUNT: u128 = 100; +const TEST_SENDER: u128 = 200; + +struct TxCase { + sender: u128, + recipient: u128, + key: Vec, + value: Vec, + gas_limit: u64, + fail_validate: bool, + fail_execute: bool, + needs_bootstrap: bool, + fail_bootstrap: bool, +} + +fn make_tx(tc: TxCase) -> TestTx { + let msg = TestMsg { + key: tc.key, + value: tc.value, + fail_after_write: tc.fail_execute, + }; + TestTx { + sender: AccountId::new(tc.sender), + recipient: AccountId::new(tc.recipient), + request: InvokeRequest::new(&msg).unwrap(), + gas_limit: tc.gas_limit, + funds: vec![], + fail_validate: tc.fail_validate, + needs_bootstrap: tc.needs_bootstrap, + fail_bootstrap: tc.fail_bootstrap, + } +} + +struct ConformanceCase { + test_name: &'static str, + blocks: Vec, +} + +fn known_test_cases() -> Vec { + vec![ + ConformanceCase { + test_name: "emptyBlockTest", + blocks: vec![TestBlock { + height: 1, + time: 0, + txs: vec![], + gas_limit: 1_000_000, + }], + }, + // sender=TEST_ACCOUNT (registered) for all non-bootstrap tests + ConformanceCase { + test_name: "successfulTxTest", + blocks: vec![TestBlock { + height: 1, + time: 0, + gas_limit: 1_000_000, + txs: vec![make_tx(TxCase { + sender: TEST_ACCOUNT, + recipient: TEST_ACCOUNT, + key: vec![1], + value: vec![11], + gas_limit: 10000, + fail_validate: false, + fail_execute: false, + needs_bootstrap: false, + fail_bootstrap: false, + })], + }], + }, + ConformanceCase { + test_name: "validationFailureTest", + blocks: vec![TestBlock { + height: 1, + time: 0, + gas_limit: 1_000_000, + txs: vec![make_tx(TxCase { + sender: TEST_ACCOUNT, + recipient: TEST_ACCOUNT, + key: vec![1], + value: vec![11], + gas_limit: 10000, + fail_validate: true, + fail_execute: false, + needs_bootstrap: false, + fail_bootstrap: false, + })], + }], + }, + ConformanceCase { + test_name: "executionFailureRollbackTest", + blocks: vec![TestBlock { + height: 1, + time: 0, + gas_limit: 1_000_000, + txs: vec![make_tx(TxCase { + sender: TEST_ACCOUNT, + recipient: TEST_ACCOUNT, + key: vec![1], + value: vec![11], + gas_limit: 10000, + fail_validate: false, + fail_execute: true, + needs_bootstrap: false, + fail_bootstrap: false, + })], + }], + }, + ConformanceCase { + test_name: "outOfGasTest", + blocks: vec![TestBlock { + height: 1, + time: 0, + gas_limit: 1_000_000, + txs: vec![make_tx(TxCase { + sender: TEST_ACCOUNT, + recipient: TEST_ACCOUNT, + key: vec![1], + value: vec![11], + gas_limit: 1, + fail_validate: false, + fail_execute: false, + needs_bootstrap: false, + fail_bootstrap: false, + })], + }], + }, + ConformanceCase { + test_name: "blockGasLimitTest", + blocks: vec![TestBlock { + height: 1, + time: 0, + gas_limit: 30, + txs: vec![ + make_tx(TxCase { + sender: TEST_ACCOUNT, + recipient: TEST_ACCOUNT, + key: vec![1], + value: vec![11], + gas_limit: 25, + fail_validate: false, + fail_execute: false, + needs_bootstrap: false, + fail_bootstrap: false, + }), + make_tx(TxCase { + sender: TEST_ACCOUNT, + recipient: TEST_ACCOUNT, + key: vec![2], + value: vec![12], + gas_limit: 25, + fail_validate: false, + fail_execute: false, + needs_bootstrap: false, + fail_bootstrap: false, + }), + ], + }], + }, + ConformanceCase { + test_name: "mixedOutcomesTest", + blocks: vec![TestBlock { + height: 1, + time: 0, + gas_limit: 1_000_000, + txs: vec![ + make_tx(TxCase { + sender: TEST_ACCOUNT, + recipient: TEST_ACCOUNT, + key: vec![0], + value: vec![10], + gas_limit: 10000, + fail_validate: false, + fail_execute: false, + needs_bootstrap: false, + fail_bootstrap: false, + }), + make_tx(TxCase { + sender: TEST_ACCOUNT, + recipient: TEST_ACCOUNT, + key: vec![1], + value: vec![11], + gas_limit: 10000, + fail_validate: true, + fail_execute: false, + needs_bootstrap: false, + fail_bootstrap: false, + }), + make_tx(TxCase { + sender: TEST_ACCOUNT, + recipient: TEST_ACCOUNT, + key: vec![2], + value: vec![12], + gas_limit: 10000, + fail_validate: false, + fail_execute: true, + needs_bootstrap: false, + fail_bootstrap: false, + }), + make_tx(TxCase { + sender: TEST_ACCOUNT, + recipient: TEST_ACCOUNT, + key: vec![3], + value: vec![13], + gas_limit: 1, + fail_validate: false, + fail_execute: false, + needs_bootstrap: false, + fail_bootstrap: false, + }), + ], + }], + }, + ConformanceCase { + test_name: "bootstrapTest", + blocks: vec![TestBlock { + height: 1, + time: 0, + gas_limit: 1_000_000, + txs: vec![make_tx(TxCase { + sender: TEST_SENDER, + recipient: TEST_ACCOUNT, + key: vec![1], + value: vec![11], + gas_limit: 10000, + fail_validate: false, + fail_execute: false, + needs_bootstrap: true, + fail_bootstrap: false, + })], + }], + }, + ConformanceCase { + test_name: "bootstrapFailureTest", + blocks: vec![TestBlock { + height: 1, + time: 0, + gas_limit: 1_000_000, + txs: vec![make_tx(TxCase { + sender: TEST_SENDER, + recipient: TEST_ACCOUNT, + key: vec![1], + value: vec![11], + gas_limit: 10000, + fail_validate: false, + fail_execute: false, + needs_bootstrap: true, + fail_bootstrap: true, + })], + }], + }, + // unregisteredSenderTest: sender=200 (not registered), no bootstrap + // Validator queries sender account for sig verification -> fails + ConformanceCase { + test_name: "unregisteredSenderTest", + blocks: vec![TestBlock { + height: 1, + time: 0, + gas_limit: 1_000_000, + txs: vec![make_tx(TxCase { + sender: TEST_SENDER, + recipient: TEST_ACCOUNT, + key: vec![1], + value: vec![11], + gas_limit: 10000, + fail_validate: false, + fail_execute: false, + needs_bootstrap: false, + fail_bootstrap: false, + })], + }], + }, + ConformanceCase { + test_name: "multiBlockTest", + blocks: vec![ + TestBlock { + height: 1, + time: 0, + gas_limit: 1_000_000, + txs: vec![make_tx(TxCase { + sender: TEST_ACCOUNT, + recipient: TEST_ACCOUNT, + key: vec![1], + value: vec![11], + gas_limit: 10000, + fail_validate: false, + fail_execute: false, + needs_bootstrap: false, + fail_bootstrap: false, + })], + }, + TestBlock { + height: 2, + time: 10, + gas_limit: 1_000_000, + txs: vec![make_tx(TxCase { + sender: TEST_ACCOUNT, + recipient: TEST_ACCOUNT, + key: vec![2], + value: vec![12], + gas_limit: 10000, + fail_validate: false, + fail_execute: false, + needs_bootstrap: false, + fail_bootstrap: false, + })], + }, + ], + }, + ConformanceCase { + test_name: "overwriteTest", + blocks: vec![TestBlock { + height: 1, + time: 0, + gas_limit: 1_000_000, + txs: vec![ + make_tx(TxCase { + sender: TEST_ACCOUNT, + recipient: TEST_ACCOUNT, + key: vec![1], + value: vec![20], + gas_limit: 10000, + fail_validate: false, + fail_execute: false, + needs_bootstrap: false, + fail_bootstrap: false, + }), + make_tx(TxCase { + sender: TEST_ACCOUNT, + recipient: TEST_ACCOUNT, + key: vec![1], + value: vec![21], + gas_limit: 10000, + fail_validate: false, + fail_execute: false, + needs_bootstrap: false, + fail_bootstrap: false, + }), + ], + }], + }, + ] +} + +// --------------------------------------------------------------------------- +// Conformance test +// --------------------------------------------------------------------------- + +#[test] +fn quint_itf_conformance() { + let traces_dir = Path::new(env!("CARGO_MANIFEST_DIR")).join("../../../specs/traces"); + + if !traces_dir.exists() { + panic!( + "ITF traces not found at {}. \ + Run: quint test --main=stf specs/stf_core.qnt \ + --out-itf \"specs/traces/out_{{test}}_{{seq}}.itf.json\"", + traces_dir.display() + ); + } + + let test_cases = known_test_cases(); + let mut matched = 0; + + for case in &test_cases { + let trace_file = find_single_trace_file(&traces_dir, case.test_name); + let trace: ItfTrace = read_itf_trace(&trace_file); + + let expected_block_height = + case.blocks.last().expect("case must have blocks").height as i64; + let spec_state = trace + .states + .iter() + .find(|s| s.block_height.as_i64() == expected_block_height) + .unwrap_or_else(|| { + panic!( + "{}: no trace state with block_height={expected_block_height}", + case.test_name + ) + }); + + let spec_result = &spec_state.last_result; + + let gas_config = StorageGasConfig { + storage_get_charge: 1, + storage_set_charge: 1, + storage_remove_charge: 1, + }; + let stf = Stf::new( + NoopBegin::::default(), + NoopEnd, + Validator, + NoopPostTx, + gas_config, + ); + + let mut storage = InMemoryStorage::default(); + let mut codes = CodeStore::new(); + codes.add_code(TestAccount); + + let test_account = AccountId::new(TEST_ACCOUNT); + let code_id = "test_account".to_string(); + storage.data.insert( + account_code_key(test_account), + Message::new(&code_id).unwrap().into_bytes().unwrap(), + ); + + let mut real_result = None; + for block in &case.blocks { + let (result, exec_state) = stf.apply_block(&storage, &codes, block); + storage + .apply_changes(exec_state.into_changes().unwrap()) + .unwrap(); + real_result = Some(result); + } + let real_result = real_result.expect("case must run at least one block"); + + // --- Assert conformance --- + + // 1. tx_results count + assert_eq!( + real_result.tx_results.len(), + spec_result.tx_results.len(), + "{}: tx_results count mismatch", + case.test_name + ); + + // 2. Per-tx outcomes + for (i, (real_tx, spec_tx)) in real_result + .tx_results + .iter() + .zip(spec_result.tx_results.iter()) + .enumerate() + { + let spec_ok = spec_tx.result.ok; + let real_ok = real_tx.response.is_ok(); + assert_eq!( + real_ok, spec_ok, + "{} tx[{i}]: ok mismatch (real={real_ok}, spec={spec_ok})", + case.test_name + ); + + if !spec_ok { + let spec_err = spec_tx.result.err_code.as_i64(); + let real_err = real_tx.response.as_ref().unwrap_err().id; + match spec_err { + SPEC_ERR_OUT_OF_GAS => assert_eq!( + real_err, + evolve_stf::ERR_OUT_OF_GAS.id, + "{} tx[{i}]: expected OOG", + case.test_name + ), + SPEC_ERR_VALIDATION => assert_eq!( + real_err, 100, + "{} tx[{i}]: expected validation error", + case.test_name + ), + SPEC_ERR_EXECUTION => assert_eq!( + real_err, 200, + "{} tx[{i}]: expected execution error", + case.test_name + ), + SPEC_ERR_BOOTSTRAP => assert_eq!( + real_err, 300, + "{} tx[{i}]: expected bootstrap error", + case.test_name + ), + _ => panic!( + "{} tx[{i}]: unknown spec error code {spec_err}", + case.test_name + ), + } + } + + // 3. Gas + assert_eq!( + real_tx.gas_used, + spec_tx.gas_used.as_u64(), + "{} tx[{i}]: gas_used mismatch", + case.test_name + ); + } + + // 4. Block-level gas + assert_eq!( + real_result.gas_used, + spec_result.gas_used.as_u64(), + "{}: block gas_used mismatch", + case.test_name + ); + + // 5. Skipped count + assert_eq!( + real_result.txs_skipped, + spec_result.txs_skipped.as_u64() as usize, + "{}: txs_skipped mismatch", + case.test_name + ); + + // 6. Storage + let modeled_accounts = + [AccountId::new(TEST_ACCOUNT), AccountId::new(TEST_SENDER)]; + for account_id in modeled_accounts { + let mut expected = HashMap::, Vec>::new(); + for (account_id_itf, account_store_itf) in &spec_state.storage.entries { + if AccountId::new(account_id_itf.as_u64() as u128) != account_id { + continue; + } + for (key_itf, value_itf) in &account_store_itf.entries { + let key: Vec = key_itf.iter().map(|b| b.as_u64() as u8).collect(); + let value: Vec = + value_itf.iter().map(|b| b.as_u64() as u8).collect(); + expected.insert(key, value); + } + } + + let mut actual = HashMap::, Vec>::new(); + let account_prefix = account_id.as_bytes(); + for (raw_key, raw_value) in &storage.data { + if raw_key.len() < account_prefix.len() { + continue; + } + if raw_key[..account_prefix.len()] == account_prefix { + actual.insert( + raw_key[account_prefix.len()..].to_vec(), + raw_value.clone(), + ); + } + } + assert_eq!( + actual, expected, + "{}: storage mismatch for account {:?}", + case.test_name, account_id + ); + } + + matched += 1; + eprintln!("PASS: {}", case.test_name); + } + + assert!( + matched == test_cases.len(), + "Matched {matched}/{} traces", + test_cases.len() + ); + eprintln!("{matched}/{} conformance tests passed", test_cases.len()); +} diff --git a/crates/app/stf/tests/quint_post_tx_conformance.rs b/crates/app/stf/tests/quint_post_tx_conformance.rs new file mode 100644 index 0000000..c64a4cc --- /dev/null +++ b/crates/app/stf/tests/quint_post_tx_conformance.rs @@ -0,0 +1,404 @@ +//! Conformance tests: replay Quint ITF traces for stf_post_tx.qnt. +//! +//! Run: +//! `quint test specs/stf_post_tx.qnt --out-itf "specs/traces/out_{test}_{seq}.itf.json"` +//! `cargo test -p evolve_stf --test quint_post_tx_conformance` + +use borsh::{BorshDeserialize, BorshSerialize}; +use evolve_core::storage_api::{StorageSetRequest, STORAGE_ACCOUNT_ID}; +use evolve_core::{ + AccountCode, AccountId, BlockContext, Environment, EnvironmentQuery, ErrorCode, FungibleAsset, + InvokableMessage, InvokeRequest, InvokeResponse, Message, SdkResult, +}; +use evolve_stf::gas::StorageGasConfig; +use evolve_stf::Stf; +use evolve_stf_traits::{ + Block as BlockTrait, PostTxExecution, Transaction, TxValidator, WritableKV, +}; +use hashbrown::HashMap; +use serde::Deserialize; +use std::path::Path; + +mod quint_common; +use quint_common::{ + account_code_key, find_single_trace_file, read_itf_trace, CodeStore, InMemoryStorage, + ItfBigInt, ItfMap, NoopBegin, NoopEnd, +}; + +#[derive(Deserialize)] +struct ItfTrace { + states: Vec, +} + +#[derive(Deserialize)] +struct ItfState { + last_result: ItfBlockResult, + storage: ItfMap, Vec>>, +} + +#[derive(Deserialize)] +struct ItfBlockResult { + gas_used: ItfBigInt, + tx_results: Vec, +} + +#[derive(Deserialize)] +struct ItfTxResult { + gas_used: ItfBigInt, + result: ItfResult, +} + +#[derive(Deserialize)] +struct ItfResult { + ok: bool, + err_code: ItfBigInt, +} + +#[derive(Clone, Debug, BorshSerialize, BorshDeserialize)] +struct TestMsg { + key: Vec, + value: Vec, + fail_after_write: bool, +} + +impl InvokableMessage for TestMsg { + const FUNCTION_IDENTIFIER: u64 = 1; + const FUNCTION_IDENTIFIER_NAME: &'static str = "test_exec"; +} + +#[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 NoopValidator; +impl TxValidator for NoopValidator { + fn validate_tx(&self, _tx: &TestTx, _env: &mut dyn Environment) -> SdkResult<()> { + Ok(()) + } +} + +#[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(999)); + } + 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(200)); + } + InvokeResponse::new(&()) + } + fn query( + &self, + _env: &mut dyn EnvironmentQuery, + _request: &InvokeRequest, + ) -> SdkResult { + InvokeResponse::new(&()) + } +} + +const SPEC_ERR_OUT_OF_GAS: i64 = 0x01; +const SPEC_ERR_EXECUTION: i64 = 200; +const SPEC_ERR_POST_TX: i64 = 999; +const TEST_ACCOUNT: u128 = 100; +const TEST_SENDER: u128 = 200; + +struct ConformanceCase { + test_name: &'static str, + block: TestBlock, +} + +fn make_tx(fail_execute: bool, reject_post_tx: bool) -> TestTx { + make_tx_with(vec![1], vec![11], 10000, fail_execute, reject_post_tx) +} + +fn make_tx_with( + key: Vec, + value: Vec, + gas_limit: u64, + fail_execute: bool, + reject_post_tx: bool, +) -> TestTx { + let msg = TestMsg { + key, + value, + fail_after_write: fail_execute, + }; + TestTx { + sender: AccountId::new(TEST_SENDER), + recipient: AccountId::new(TEST_ACCOUNT), + request: InvokeRequest::new(&msg).unwrap(), + gas_limit, + funds: vec![], + reject_post_tx, + } +} + +fn known_test_cases() -> Vec { + vec![ + ConformanceCase { + test_name: "postTxRejectsButKeepsStateTest", + block: TestBlock { + height: 1, + time: 0, + txs: vec![make_tx(false, true)], + }, + }, + ConformanceCase { + test_name: "postTxDoesNotMaskExecFailureTest", + block: TestBlock { + height: 1, + time: 0, + txs: vec![make_tx(true, true)], + }, + }, + ConformanceCase { + test_name: "happyPathTest", + block: TestBlock { + height: 1, + time: 0, + txs: vec![make_tx(false, false)], + }, + }, + ConformanceCase { + test_name: "mixedPostTxTest", + block: TestBlock { + height: 1, + time: 0, + txs: vec![ + make_tx(false, true), + make_tx_with(vec![2], vec![12], 10000, false, false), + ], + }, + }, + ConformanceCase { + test_name: "outOfGasIgnoresPostTxTest", + block: TestBlock { + height: 1, + time: 0, + txs: vec![make_tx_with(vec![1], vec![11], 1, false, true)], + }, + }, + ] +} + +#[test] +fn quint_itf_post_tx_conformance() { + let traces_dir = Path::new(env!("CARGO_MANIFEST_DIR")).join("../../../specs/traces"); + if !traces_dir.exists() { + panic!( + "ITF traces not found at {}. Run: quint test specs/stf_post_tx.qnt --out-itf \"specs/traces/out_{{test}}_{{seq}}.itf.json\"", + traces_dir.display() + ); + } + + let test_cases = known_test_cases(); + for case in &test_cases { + let trace_file = find_single_trace_file(&traces_dir, case.test_name); + let trace: ItfTrace = read_itf_trace(&trace_file); + let spec_state = trace + .states + .last() + .expect("trace must have at least one state"); + let spec_result = &spec_state.last_result; + + let gas_config = StorageGasConfig { + storage_get_charge: 1, + storage_set_charge: 1, + storage_remove_charge: 1, + }; + let stf = Stf::new( + NoopBegin::::default(), + NoopEnd, + NoopValidator, + RejectingPostTx, + gas_config, + ); + + let mut storage = InMemoryStorage::default(); + let mut codes = CodeStore::new(); + codes.add_code(TestAccount); + + let test_account = AccountId::new(TEST_ACCOUNT); + let code_id = "test_account".to_string(); + storage.data.insert( + account_code_key(test_account), + Message::new(&code_id).unwrap().into_bytes().unwrap(), + ); + + let (real_result, exec_state) = stf.apply_block(&storage, &codes, &case.block); + storage + .apply_changes(exec_state.into_changes().unwrap()) + .unwrap(); + + assert_eq!( + real_result.tx_results.len(), + spec_result.tx_results.len(), + "{}: tx_results count mismatch", + case.test_name + ); + + for (i, (real_tx, spec_tx)) in real_result + .tx_results + .iter() + .zip(spec_result.tx_results.iter()) + .enumerate() + { + let spec_ok = spec_tx.result.ok; + let real_ok = real_tx.response.is_ok(); + assert_eq!(real_ok, spec_ok, "{} tx[{i}]: ok mismatch", case.test_name); + + if !spec_ok { + let spec_err = spec_tx.result.err_code.as_i64(); + let real_err = real_tx.response.as_ref().unwrap_err().id; + match spec_err { + SPEC_ERR_OUT_OF_GAS => assert_eq!( + real_err, + evolve_stf::ERR_OUT_OF_GAS.id, + "{} tx[{i}]: expected OOG", + case.test_name + ), + SPEC_ERR_EXECUTION => assert_eq!( + real_err, 200, + "{} tx[{i}]: expected execution error", + case.test_name + ), + SPEC_ERR_POST_TX => assert_eq!( + real_err, 999, + "{} tx[{i}]: expected post-tx error", + case.test_name + ), + _ => panic!( + "{} tx[{i}]: unknown spec error code {spec_err}", + case.test_name + ), + } + } + + assert_eq!( + real_tx.gas_used, + spec_tx.gas_used.as_u64(), + "{} tx[{i}]: gas_used mismatch", + case.test_name + ); + } + + assert_eq!( + real_result.gas_used, + spec_result.gas_used.as_u64(), + "{}: block gas mismatch", + case.test_name + ); + + let account_id = AccountId::new(TEST_ACCOUNT); + let mut expected = HashMap::, Vec>::new(); + for (account_id_itf, account_store_itf) in &spec_state.storage.entries { + if AccountId::new(account_id_itf.as_u64() as u128) != account_id { + continue; + } + for (key_itf, value_itf) in &account_store_itf.entries { + let key: Vec = key_itf.iter().map(|b| b.as_u64() as u8).collect(); + let value: Vec = value_itf.iter().map(|b| b.as_u64() as u8).collect(); + expected.insert(key, value); + } + } + + let mut actual = HashMap::, Vec>::new(); + let account_prefix = account_id.as_bytes(); + for (raw_key, raw_value) in &storage.data { + if raw_key.len() < account_prefix.len() { + continue; + } + if raw_key[..account_prefix.len()] == account_prefix { + actual.insert(raw_key[account_prefix.len()..].to_vec(), raw_value.clone()); + } + } + assert_eq!( + actual, expected, + "{}: storage mismatch for account {:?}", + case.test_name, account_id + ); + } +} diff --git a/justfile b/justfile index 5419bfd..af77979 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: @@ -208,6 +214,40 @@ sim-debug trace: sim-report trace: cargo run -p evolve-sim -- report --trace {{trace}} +# ============================================================================ +# SPEC CONFORMANCE +# ============================================================================ + +# Run core STF Quint tests/traces and Rust conformance checks +[group('spec')] +spec-test-core: + quint test specs/stf_core.qnt + rm -f specs/traces/*.itf.json + quint test specs/stf_core.qnt --out-itf "specs/traces/out_{test}_{seq}.itf.json" + cargo test -p evolve_stf --test quint_conformance + +# Run extended STF model specs (currently Quint-only) +[group('spec')] +spec-test-extended: + quint test specs/stf_post_tx.qnt + quint test specs/stf_post_tx.qnt --out-itf "specs/traces/out_{test}_{seq}.itf.json" + cargo test -p evolve_stf --test quint_post_tx_conformance + quint test specs/stf_call_depth.qnt + quint test specs/stf_call_depth.qnt --out-itf "specs/traces/out_{test}_{seq}.itf.json" + cargo test -p evolve_stf --test quint_call_depth_conformance + +# Run full STF spec suite (core + extended) +[group('spec')] +spec-test: + just spec-test-core + just spec-test-extended + +# Regenerate ITF traces from core Quint spec (run after editing specs/stf_core.qnt) +[group('spec')] +spec-traces: + rm -f specs/traces/*.itf.json + quint test specs/stf_core.qnt --out-itf "specs/traces/out_{test}_{seq}.itf.json" + # ============================================================================ # 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..c0f3c9c --- /dev/null +++ b/specs/stf_core.qnt @@ -0,0 +1,714 @@ +// 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, 25, 100, 10000) + val MC_BLOCK_GAS_LIMITS: Set[int] = Set(30, 1000, 1000000) + + // + // === Pure helpers === + // + + /// AccountId is u128 in the Rust implementation = 16 bytes. + /// The real storage key is `account_id_bytes ++ user_key`. + val ACCOUNT_ID_BYTE_SIZE: int = 16 + 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 (16 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_result = + if (tx.needs_bootstrap and not(registered.contains(tx.sender))) + if (tx.fail_bootstrap) + // Bootstrap failed + { ok: false, accounts: registered, gas: bootstrap_gas_cost(config) } + else + // Bootstrap succeeds: register sender + { ok: true, accounts: registered.union(Set(tx.sender)), gas: bootstrap_gas_cost(config) } + else + // No bootstrap needed or already registered + { ok: true, accounts: registered, gas: 0 } + + if (not(bootstrap_result.ok)) + // Bootstrap failed -> return error, no state changes + { + result: { result: Err(ERR_BOOTSTRAP), gas_used: bootstrap_result.gas }, + store: account_store, + accounts: registered, + } + else + val current_accounts = bootstrap_result.accounts + 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: account_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: account_store, + accounts: current_accounts, + } + else if (tx.fail_execute) + // Execution error after write -> rollback + { + result: { result: Err(ERR_EXECUTION), gas_used: total_gas }, + store: account_store, + accounts: current_accounts, + } + else + // Phase 3: Write succeeds -> apply to storage + 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) + { + 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(), + } + + /// 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), + } + } + + // + // === 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*(16+1+1+1+1) = 20 per tx. + /// tx1.gas_limit=25, tx2.gas_limit=25. Block gas_limit=30. + /// Pre-check: cumulative(0) + tx1.gas_limit(25) = 25 <= 30 -> execute tx1 (uses 20 gas). + /// Pre-check: cumulative(20) + tx2.gas_limit(25) = 45 > 30 -> skip tx2. + run blockGasLimitTest = { + val tx1: Tx = { + sender: 100, recipient: 100, gas_limit: 25, + 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: 25, + 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: 30 })) + .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), + // Sender should NOT be registered + assert(not(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..37e255e --- /dev/null +++ b/specs/stf_post_tx.qnt @@ -0,0 +1,350 @@ +// 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 = 16 + + 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, + } + + 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), + } + } + + // + // === 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] + + // + // === 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(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), + // State change persists despite post-tx error + assert(storage.get(100).get(K1) == V1), + assert(gas_accounting), + stutter, + }) + } + + /// 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(all { + assert(last_result.tx_results.length() == 1), + assert(last_result.tx_results[0].result.ok == false), + // Execution error, NOT post-tx error + assert(last_result.tx_results[0].result.err_code == ERR_EXECUTION), + // No state changes (execution was rolled back) + assert(storage.get(100) == Map()), + assert(gas_accounting), + stutter, + }) + } + + /// 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(all { + assert(last_result.tx_results[0].result.ok == true), + assert(storage.get(100).get(K1) == V1), + assert(gas_accounting), + stutter, + }) + } + + /// 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(all { + assert(last_result.tx_results.length() == 2), + // First tx: post-tx rejected, but state persists + assert(last_result.tx_results[0].result.err_code == ERR_POST_TX), + assert(storage.get(100).get(K1) == V1), + // Second tx: fully succeeds + assert(last_result.tx_results[1].result.ok == true), + assert(storage.get(100).get(K2) == V2), + assert(gas_accounting), + stutter, + }) + } + + /// 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(all { + assert(last_result.tx_results[0].result.err_code == ERR_OUT_OF_GAS), + assert(storage.get(100) == Map()), + assert(gas_accounting), + stutter, + }) + } +} diff --git a/specs/traces/out_blockGasLimitTest_5.itf.json b/specs/traces/out_blockGasLimitTest_5.itf.json new file mode 100644 index 0000000..2873af0 --- /dev/null +++ b/specs/traces/out_blockGasLimitTest_5.itf.json @@ -0,0 +1 @@ +{"#meta":{"format":"ITF","format-description":"https://apalache-mc.org/docs/adr/015adr-trace.html","source":"specs/stf_core.qnt","status":"passed","description":"Created by Quint on Wed Feb 25 2026 16:32:37 GMT+0100 (Central European Standard Time)","timestamp":1772033557717},"vars":["storage","accounts","block_height","last_result","last_block_tx_count"],"states":[{"#meta":{"index":0},"accounts":{"#set":[]},"block_height":{"#bigint":"0"},"last_block_tx_count":{"#bigint":"0"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[]}},{"#meta":{"index":1},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"0"},"last_block_tx_count":{"#bigint":"0"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}},{"#meta":{"index":2},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"1"},"last_block_tx_count":{"#bigint":"2"},"last_result":{"gas_used":{"#bigint":"20"},"tx_results":[{"gas_used":{"#bigint":"20"},"result":{"err_code":{"#bigint":"0"},"ok":true}}],"txs_skipped":{"#bigint":"1"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[[[{"#bigint":"1"}],[{"#bigint":"11"}]]]}]]}},{"#meta":{"index":3},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"1"},"last_block_tx_count":{"#bigint":"2"},"last_result":{"gas_used":{"#bigint":"20"},"tx_results":[{"gas_used":{"#bigint":"20"},"result":{"err_code":{"#bigint":"0"},"ok":true}}],"txs_skipped":{"#bigint":"1"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[[[{"#bigint":"1"}],[{"#bigint":"11"}]]]}]]}}]} \ No newline at end of file diff --git a/specs/traces/out_bootstrapFailureTest_8.itf.json b/specs/traces/out_bootstrapFailureTest_8.itf.json new file mode 100644 index 0000000..cdcb19c --- /dev/null +++ b/specs/traces/out_bootstrapFailureTest_8.itf.json @@ -0,0 +1 @@ +{"#meta":{"format":"ITF","format-description":"https://apalache-mc.org/docs/adr/015adr-trace.html","source":"specs/stf_core.qnt","status":"passed","description":"Created by Quint on Wed Feb 25 2026 16:32:37 GMT+0100 (Central European Standard Time)","timestamp":1772033557728},"vars":["storage","accounts","block_height","last_result","last_block_tx_count"],"states":[{"#meta":{"index":0},"accounts":{"#set":[]},"block_height":{"#bigint":"0"},"last_block_tx_count":{"#bigint":"0"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[]}},{"#meta":{"index":1},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"0"},"last_block_tx_count":{"#bigint":"0"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}},{"#meta":{"index":2},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"1"},"last_block_tx_count":{"#bigint":"1"},"last_result":{"gas_used":{"#bigint":"35"},"tx_results":[{"gas_used":{"#bigint":"35"},"result":{"err_code":{"#bigint":"300"},"ok":false}}],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}},{"#meta":{"index":3},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"1"},"last_block_tx_count":{"#bigint":"1"},"last_result":{"gas_used":{"#bigint":"35"},"tx_results":[{"gas_used":{"#bigint":"35"},"result":{"err_code":{"#bigint":"300"},"ok":false}}],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}}]} \ No newline at end of file diff --git a/specs/traces/out_bootstrapTest_7.itf.json b/specs/traces/out_bootstrapTest_7.itf.json new file mode 100644 index 0000000..7de9fe3 --- /dev/null +++ b/specs/traces/out_bootstrapTest_7.itf.json @@ -0,0 +1 @@ +{"#meta":{"format":"ITF","format-description":"https://apalache-mc.org/docs/adr/015adr-trace.html","source":"specs/stf_core.qnt","status":"passed","description":"Created by Quint on Wed Feb 25 2026 16:32:37 GMT+0100 (Central European Standard Time)","timestamp":1772033557727},"vars":["storage","accounts","block_height","last_result","last_block_tx_count"],"states":[{"#meta":{"index":0},"accounts":{"#set":[]},"block_height":{"#bigint":"0"},"last_block_tx_count":{"#bigint":"0"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[]}},{"#meta":{"index":1},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"0"},"last_block_tx_count":{"#bigint":"0"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}},{"#meta":{"index":2},"accounts":{"#set":[{"#bigint":"100"},{"#bigint":"200"}]},"block_height":{"#bigint":"1"},"last_block_tx_count":{"#bigint":"1"},"last_result":{"gas_used":{"#bigint":"55"},"tx_results":[{"gas_used":{"#bigint":"55"},"result":{"err_code":{"#bigint":"0"},"ok":true}}],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[[[{"#bigint":"1"}],[{"#bigint":"11"}]]]}]]}},{"#meta":{"index":3},"accounts":{"#set":[{"#bigint":"100"},{"#bigint":"200"}]},"block_height":{"#bigint":"1"},"last_block_tx_count":{"#bigint":"1"},"last_result":{"gas_used":{"#bigint":"55"},"tx_results":[{"gas_used":{"#bigint":"55"},"result":{"err_code":{"#bigint":"0"},"ok":true}}],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[[[{"#bigint":"1"}],[{"#bigint":"11"}]]]}]]}}]} \ No newline at end of file diff --git a/specs/traces/out_cannotReturnFromEmptyTest_4.itf.json b/specs/traces/out_cannotReturnFromEmptyTest_4.itf.json new file mode 100644 index 0000000..226104b --- /dev/null +++ b/specs/traces/out_cannotReturnFromEmptyTest_4.itf.json @@ -0,0 +1 @@ +{"#meta":{"format":"ITF","format-description":"https://apalache-mc.org/docs/adr/015adr-trace.html","source":"specs/stf_call_depth.qnt","status":"passed","description":"Created by Quint on Wed Feb 25 2026 16:32:42 GMT+0100 (Central European Standard Time)","timestamp":1772033562682},"vars":["call_stack","last_result"],"states":[{"#meta":{"index":0},"call_stack":[],"last_result":{"err_code":{"#bigint":"0"},"ok":true}},{"#meta":{"index":1}}]} \ No newline at end of file diff --git a/specs/traces/out_emptyBlockTest_0.itf.json b/specs/traces/out_emptyBlockTest_0.itf.json new file mode 100644 index 0000000..a3a98e5 --- /dev/null +++ b/specs/traces/out_emptyBlockTest_0.itf.json @@ -0,0 +1 @@ +{"#meta":{"format":"ITF","format-description":"https://apalache-mc.org/docs/adr/015adr-trace.html","source":"specs/stf_core.qnt","status":"passed","description":"Created by Quint on Wed Feb 25 2026 16:32:37 GMT+0100 (Central European Standard Time)","timestamp":1772033557711},"vars":["storage","accounts","block_height","last_result","last_block_tx_count"],"states":[{"#meta":{"index":0},"accounts":{"#set":[]},"block_height":{"#bigint":"0"},"last_block_tx_count":{"#bigint":"0"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[]}},{"#meta":{"index":1},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"0"},"last_block_tx_count":{"#bigint":"0"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}},{"#meta":{"index":2},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"1"},"last_block_tx_count":{"#bigint":"0"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}},{"#meta":{"index":3},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"1"},"last_block_tx_count":{"#bigint":"0"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}}]} \ No newline at end of file diff --git a/specs/traces/out_executionFailureRollbackTest_3.itf.json b/specs/traces/out_executionFailureRollbackTest_3.itf.json new file mode 100644 index 0000000..bac590b --- /dev/null +++ b/specs/traces/out_executionFailureRollbackTest_3.itf.json @@ -0,0 +1 @@ +{"#meta":{"format":"ITF","format-description":"https://apalache-mc.org/docs/adr/015adr-trace.html","source":"specs/stf_core.qnt","status":"passed","description":"Created by Quint on Wed Feb 25 2026 16:32:37 GMT+0100 (Central European Standard Time)","timestamp":1772033557715},"vars":["storage","accounts","block_height","last_result","last_block_tx_count"],"states":[{"#meta":{"index":0},"accounts":{"#set":[]},"block_height":{"#bigint":"0"},"last_block_tx_count":{"#bigint":"0"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[]}},{"#meta":{"index":1},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"0"},"last_block_tx_count":{"#bigint":"0"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}},{"#meta":{"index":2},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"1"},"last_block_tx_count":{"#bigint":"1"},"last_result":{"gas_used":{"#bigint":"20"},"tx_results":[{"gas_used":{"#bigint":"20"},"result":{"err_code":{"#bigint":"200"},"ok":false}}],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}},{"#meta":{"index":3},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"1"},"last_block_tx_count":{"#bigint":"1"},"last_result":{"gas_used":{"#bigint":"20"},"tx_results":[{"gas_used":{"#bigint":"20"},"result":{"err_code":{"#bigint":"200"},"ok":false}}],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}}]} \ No newline at end of file diff --git a/specs/traces/out_fullUnwindTest_3.itf.json b/specs/traces/out_fullUnwindTest_3.itf.json new file mode 100644 index 0000000..d0755e7 --- /dev/null +++ b/specs/traces/out_fullUnwindTest_3.itf.json @@ -0,0 +1 @@ +{"#meta":{"format":"ITF","format-description":"https://apalache-mc.org/docs/adr/015adr-trace.html","source":"specs/stf_call_depth.qnt","status":"passed","description":"Created by Quint on Wed Feb 25 2026 16:32:42 GMT+0100 (Central European Standard Time)","timestamp":1772033562681},"vars":["call_stack","last_result"],"states":[{"#meta":{"index":0},"call_stack":[],"last_result":{"err_code":{"#bigint":"0"},"ok":true}},{"#meta":{"index":1},"call_stack":[{"#bigint":"1"}],"last_result":{"err_code":{"#bigint":"0"},"ok":true}},{"#meta":{"index":2},"call_stack":[{"#bigint":"1"},{"#bigint":"2"}],"last_result":{"err_code":{"#bigint":"0"},"ok":true}},{"#meta":{"index":3},"call_stack":[{"#bigint":"1"}],"last_result":{"err_code":{"#bigint":"0"},"ok":true}},{"#meta":{"index":4},"call_stack":[],"last_result":{"err_code":{"#bigint":"0"},"ok":true}},{"#meta":{"index":5},"call_stack":[],"last_result":{"err_code":{"#bigint":"0"},"ok":true}}]} \ No newline at end of file diff --git a/specs/traces/out_happyPathTest_2.itf.json b/specs/traces/out_happyPathTest_2.itf.json new file mode 100644 index 0000000..59be5f9 --- /dev/null +++ b/specs/traces/out_happyPathTest_2.itf.json @@ -0,0 +1 @@ +{"#meta":{"format":"ITF","format-description":"https://apalache-mc.org/docs/adr/015adr-trace.html","source":"specs/stf_post_tx.qnt","status":"passed","description":"Created by Quint on Wed Feb 25 2026 16:32:43 GMT+0100 (Central European Standard Time)","timestamp":1772033563574},"vars":["storage","accounts","last_result"],"states":[{"#meta":{"index":0},"accounts":{"#set":[]},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[]},"storage":{"#map":[]}},{"#meta":{"index":1},"accounts":{"#set":[{"#bigint":"100"}]},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[]},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}},{"#meta":{"index":2},"accounts":{"#set":[{"#bigint":"100"}]},"last_result":{"gas_used":{"#bigint":"20"},"tx_results":[{"gas_used":{"#bigint":"20"},"result":{"err_code":{"#bigint":"0"},"ok":true}}]},"storage":{"#map":[[{"#bigint":"100"},{"#map":[[[{"#bigint":"1"}],[{"#bigint":"11"}]]]}]]}},{"#meta":{"index":3},"accounts":{"#set":[{"#bigint":"100"}]},"last_result":{"gas_used":{"#bigint":"20"},"tx_results":[{"gas_used":{"#bigint":"20"},"result":{"err_code":{"#bigint":"0"},"ok":true}}]},"storage":{"#map":[[{"#bigint":"100"},{"#map":[[[{"#bigint":"1"}],[{"#bigint":"11"}]]]}]]}}]} \ No newline at end of file diff --git a/specs/traces/out_mixedOutcomesTest_6.itf.json b/specs/traces/out_mixedOutcomesTest_6.itf.json new file mode 100644 index 0000000..08a7267 --- /dev/null +++ b/specs/traces/out_mixedOutcomesTest_6.itf.json @@ -0,0 +1 @@ +{"#meta":{"format":"ITF","format-description":"https://apalache-mc.org/docs/adr/015adr-trace.html","source":"specs/stf_core.qnt","status":"passed","description":"Created by Quint on Wed Feb 25 2026 16:32:37 GMT+0100 (Central European Standard Time)","timestamp":1772033557719},"vars":["storage","accounts","block_height","last_result","last_block_tx_count"],"states":[{"#meta":{"index":0},"accounts":{"#set":[]},"block_height":{"#bigint":"0"},"last_block_tx_count":{"#bigint":"0"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[]}},{"#meta":{"index":1},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"0"},"last_block_tx_count":{"#bigint":"0"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}},{"#meta":{"index":2},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"1"},"last_block_tx_count":{"#bigint":"4"},"last_result":{"gas_used":{"#bigint":"40"},"tx_results":[{"gas_used":{"#bigint":"20"},"result":{"err_code":{"#bigint":"0"},"ok":true}},{"gas_used":{"#bigint":"0"},"result":{"err_code":{"#bigint":"100"},"ok":false}},{"gas_used":{"#bigint":"20"},"result":{"err_code":{"#bigint":"200"},"ok":false}},{"gas_used":{"#bigint":"0"},"result":{"err_code":{"#bigint":"1"},"ok":false}}],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[[[{"#bigint":"0"}],[{"#bigint":"10"}]]]}]]}},{"#meta":{"index":3},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"1"},"last_block_tx_count":{"#bigint":"4"},"last_result":{"gas_used":{"#bigint":"40"},"tx_results":[{"gas_used":{"#bigint":"20"},"result":{"err_code":{"#bigint":"0"},"ok":true}},{"gas_used":{"#bigint":"0"},"result":{"err_code":{"#bigint":"100"},"ok":false}},{"gas_used":{"#bigint":"20"},"result":{"err_code":{"#bigint":"200"},"ok":false}},{"gas_used":{"#bigint":"0"},"result":{"err_code":{"#bigint":"1"},"ok":false}}],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[[[{"#bigint":"0"}],[{"#bigint":"10"}]]]}]]}}]} \ No newline at end of file diff --git a/specs/traces/out_mixedPostTxTest_3.itf.json b/specs/traces/out_mixedPostTxTest_3.itf.json new file mode 100644 index 0000000..d368482 --- /dev/null +++ b/specs/traces/out_mixedPostTxTest_3.itf.json @@ -0,0 +1 @@ +{"#meta":{"format":"ITF","format-description":"https://apalache-mc.org/docs/adr/015adr-trace.html","source":"specs/stf_post_tx.qnt","status":"passed","description":"Created by Quint on Wed Feb 25 2026 16:32:43 GMT+0100 (Central European Standard Time)","timestamp":1772033563582},"vars":["storage","accounts","last_result"],"states":[{"#meta":{"index":0},"accounts":{"#set":[]},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[]},"storage":{"#map":[]}},{"#meta":{"index":1},"accounts":{"#set":[{"#bigint":"100"}]},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[]},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}},{"#meta":{"index":2},"accounts":{"#set":[{"#bigint":"100"}]},"last_result":{"gas_used":{"#bigint":"40"},"tx_results":[{"gas_used":{"#bigint":"20"},"result":{"err_code":{"#bigint":"999"},"ok":false}},{"gas_used":{"#bigint":"20"},"result":{"err_code":{"#bigint":"0"},"ok":true}}]},"storage":{"#map":[[{"#bigint":"100"},{"#map":[[[{"#bigint":"1"}],[{"#bigint":"11"}]],[[{"#bigint":"2"}],[{"#bigint":"12"}]]]}]]}},{"#meta":{"index":3},"accounts":{"#set":[{"#bigint":"100"}]},"last_result":{"gas_used":{"#bigint":"40"},"tx_results":[{"gas_used":{"#bigint":"20"},"result":{"err_code":{"#bigint":"999"},"ok":false}},{"gas_used":{"#bigint":"20"},"result":{"err_code":{"#bigint":"0"},"ok":true}}]},"storage":{"#map":[[{"#bigint":"100"},{"#map":[[[{"#bigint":"1"}],[{"#bigint":"11"}]],[[{"#bigint":"2"}],[{"#bigint":"12"}]]]}]]}}]} \ No newline at end of file diff --git a/specs/traces/out_multiBlockTest_10.itf.json b/specs/traces/out_multiBlockTest_10.itf.json new file mode 100644 index 0000000..69724d0 --- /dev/null +++ b/specs/traces/out_multiBlockTest_10.itf.json @@ -0,0 +1 @@ +{"#meta":{"format":"ITF","format-description":"https://apalache-mc.org/docs/adr/015adr-trace.html","source":"specs/stf_core.qnt","status":"passed","description":"Created by Quint on Wed Feb 25 2026 16:32:37 GMT+0100 (Central European Standard Time)","timestamp":1772033557729},"vars":["storage","accounts","block_height","last_result","last_block_tx_count"],"states":[{"#meta":{"index":0},"accounts":{"#set":[]},"block_height":{"#bigint":"0"},"last_block_tx_count":{"#bigint":"0"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[]}},{"#meta":{"index":1},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"0"},"last_block_tx_count":{"#bigint":"0"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}},{"#meta":{"index":2},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"1"},"last_block_tx_count":{"#bigint":"1"},"last_result":{"gas_used":{"#bigint":"20"},"tx_results":[{"gas_used":{"#bigint":"20"},"result":{"err_code":{"#bigint":"0"},"ok":true}}],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[[[{"#bigint":"1"}],[{"#bigint":"11"}]]]}]]}},{"#meta":{"index":3},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"2"},"last_block_tx_count":{"#bigint":"1"},"last_result":{"gas_used":{"#bigint":"20"},"tx_results":[{"gas_used":{"#bigint":"20"},"result":{"err_code":{"#bigint":"0"},"ok":true}}],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[[[{"#bigint":"1"}],[{"#bigint":"11"}]],[[{"#bigint":"2"}],[{"#bigint":"12"}]]]}]]}},{"#meta":{"index":4},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"2"},"last_block_tx_count":{"#bigint":"1"},"last_result":{"gas_used":{"#bigint":"20"},"tx_results":[{"gas_used":{"#bigint":"20"},"result":{"err_code":{"#bigint":"0"},"ok":true}}],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[[[{"#bigint":"1"}],[{"#bigint":"11"}]],[[{"#bigint":"2"}],[{"#bigint":"12"}]]]}]]}}]} \ No newline at end of file diff --git a/specs/traces/out_nestedCallsTest_1.itf.json b/specs/traces/out_nestedCallsTest_1.itf.json new file mode 100644 index 0000000..2a20845 --- /dev/null +++ b/specs/traces/out_nestedCallsTest_1.itf.json @@ -0,0 +1 @@ +{"#meta":{"format":"ITF","format-description":"https://apalache-mc.org/docs/adr/015adr-trace.html","source":"specs/stf_call_depth.qnt","status":"passed","description":"Created by Quint on Wed Feb 25 2026 16:32:42 GMT+0100 (Central European Standard Time)","timestamp":1772033562680},"vars":["call_stack","last_result"],"states":[{"#meta":{"index":0},"call_stack":[],"last_result":{"err_code":{"#bigint":"0"},"ok":true}},{"#meta":{"index":1},"call_stack":[{"#bigint":"1"}],"last_result":{"err_code":{"#bigint":"0"},"ok":true}},{"#meta":{"index":2},"call_stack":[{"#bigint":"1"},{"#bigint":"2"}],"last_result":{"err_code":{"#bigint":"0"},"ok":true}},{"#meta":{"index":3},"call_stack":[{"#bigint":"1"},{"#bigint":"2"},{"#bigint":"3"}],"last_result":{"err_code":{"#bigint":"0"},"ok":true}},{"#meta":{"index":4},"call_stack":[{"#bigint":"1"},{"#bigint":"2"},{"#bigint":"3"}],"last_result":{"err_code":{"#bigint":"0"},"ok":true}}]} \ No newline at end of file diff --git a/specs/traces/out_outOfGasIgnoresPostTxTest_4.itf.json b/specs/traces/out_outOfGasIgnoresPostTxTest_4.itf.json new file mode 100644 index 0000000..b9c41f2 --- /dev/null +++ b/specs/traces/out_outOfGasIgnoresPostTxTest_4.itf.json @@ -0,0 +1 @@ +{"#meta":{"format":"ITF","format-description":"https://apalache-mc.org/docs/adr/015adr-trace.html","source":"specs/stf_post_tx.qnt","status":"passed","description":"Created by Quint on Wed Feb 25 2026 16:32:43 GMT+0100 (Central European Standard Time)","timestamp":1772033563583},"vars":["storage","accounts","last_result"],"states":[{"#meta":{"index":0},"accounts":{"#set":[]},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[]},"storage":{"#map":[]}},{"#meta":{"index":1},"accounts":{"#set":[{"#bigint":"100"}]},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[]},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}},{"#meta":{"index":2},"accounts":{"#set":[{"#bigint":"100"}]},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[{"gas_used":{"#bigint":"0"},"result":{"err_code":{"#bigint":"1"},"ok":false}}]},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}},{"#meta":{"index":3},"accounts":{"#set":[{"#bigint":"100"}]},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[{"gas_used":{"#bigint":"0"},"result":{"err_code":{"#bigint":"1"},"ok":false}}]},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}}]} \ No newline at end of file diff --git a/specs/traces/out_outOfGasTest_4.itf.json b/specs/traces/out_outOfGasTest_4.itf.json new file mode 100644 index 0000000..9a1a57f --- /dev/null +++ b/specs/traces/out_outOfGasTest_4.itf.json @@ -0,0 +1 @@ +{"#meta":{"format":"ITF","format-description":"https://apalache-mc.org/docs/adr/015adr-trace.html","source":"specs/stf_core.qnt","status":"passed","description":"Created by Quint on Wed Feb 25 2026 16:32:37 GMT+0100 (Central European Standard Time)","timestamp":1772033557716},"vars":["storage","accounts","block_height","last_result","last_block_tx_count"],"states":[{"#meta":{"index":0},"accounts":{"#set":[]},"block_height":{"#bigint":"0"},"last_block_tx_count":{"#bigint":"0"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[]}},{"#meta":{"index":1},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"0"},"last_block_tx_count":{"#bigint":"0"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}},{"#meta":{"index":2},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"1"},"last_block_tx_count":{"#bigint":"1"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[{"gas_used":{"#bigint":"0"},"result":{"err_code":{"#bigint":"1"},"ok":false}}],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}},{"#meta":{"index":3},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"1"},"last_block_tx_count":{"#bigint":"1"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[{"gas_used":{"#bigint":"0"},"result":{"err_code":{"#bigint":"1"},"ok":false}}],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}}]} \ No newline at end of file diff --git a/specs/traces/out_overwriteTest_11.itf.json b/specs/traces/out_overwriteTest_11.itf.json new file mode 100644 index 0000000..2495fb3 --- /dev/null +++ b/specs/traces/out_overwriteTest_11.itf.json @@ -0,0 +1 @@ +{"#meta":{"format":"ITF","format-description":"https://apalache-mc.org/docs/adr/015adr-trace.html","source":"specs/stf_core.qnt","status":"passed","description":"Created by Quint on Wed Feb 25 2026 16:32:37 GMT+0100 (Central European Standard Time)","timestamp":1772033557730},"vars":["storage","accounts","block_height","last_result","last_block_tx_count"],"states":[{"#meta":{"index":0},"accounts":{"#set":[]},"block_height":{"#bigint":"0"},"last_block_tx_count":{"#bigint":"0"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[]}},{"#meta":{"index":1},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"0"},"last_block_tx_count":{"#bigint":"0"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}},{"#meta":{"index":2},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"1"},"last_block_tx_count":{"#bigint":"2"},"last_result":{"gas_used":{"#bigint":"40"},"tx_results":[{"gas_used":{"#bigint":"20"},"result":{"err_code":{"#bigint":"0"},"ok":true}},{"gas_used":{"#bigint":"20"},"result":{"err_code":{"#bigint":"0"},"ok":true}}],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[[[{"#bigint":"1"}],[{"#bigint":"21"}]]]}]]}},{"#meta":{"index":3},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"1"},"last_block_tx_count":{"#bigint":"2"},"last_result":{"gas_used":{"#bigint":"40"},"tx_results":[{"gas_used":{"#bigint":"20"},"result":{"err_code":{"#bigint":"0"},"ok":true}},{"gas_used":{"#bigint":"20"},"result":{"err_code":{"#bigint":"0"},"ok":true}}],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[[[{"#bigint":"1"}],[{"#bigint":"21"}]]]}]]}}]} \ No newline at end of file diff --git a/specs/traces/out_postTxDoesNotMaskExecFailureTest_1.itf.json b/specs/traces/out_postTxDoesNotMaskExecFailureTest_1.itf.json new file mode 100644 index 0000000..8d3f342 --- /dev/null +++ b/specs/traces/out_postTxDoesNotMaskExecFailureTest_1.itf.json @@ -0,0 +1 @@ +{"#meta":{"format":"ITF","format-description":"https://apalache-mc.org/docs/adr/015adr-trace.html","source":"specs/stf_post_tx.qnt","status":"passed","description":"Created by Quint on Wed Feb 25 2026 16:32:43 GMT+0100 (Central European Standard Time)","timestamp":1772033563573},"vars":["storage","accounts","last_result"],"states":[{"#meta":{"index":0},"accounts":{"#set":[]},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[]},"storage":{"#map":[]}},{"#meta":{"index":1},"accounts":{"#set":[{"#bigint":"100"}]},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[]},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}},{"#meta":{"index":2},"accounts":{"#set":[{"#bigint":"100"}]},"last_result":{"gas_used":{"#bigint":"20"},"tx_results":[{"gas_used":{"#bigint":"20"},"result":{"err_code":{"#bigint":"200"},"ok":false}}]},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}},{"#meta":{"index":3},"accounts":{"#set":[{"#bigint":"100"}]},"last_result":{"gas_used":{"#bigint":"20"},"tx_results":[{"gas_used":{"#bigint":"20"},"result":{"err_code":{"#bigint":"200"},"ok":false}}]},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}}]} \ No newline at end of file diff --git a/specs/traces/out_postTxRejectsButKeepsStateTest_0.itf.json b/specs/traces/out_postTxRejectsButKeepsStateTest_0.itf.json new file mode 100644 index 0000000..cc5a5b1 --- /dev/null +++ b/specs/traces/out_postTxRejectsButKeepsStateTest_0.itf.json @@ -0,0 +1 @@ +{"#meta":{"format":"ITF","format-description":"https://apalache-mc.org/docs/adr/015adr-trace.html","source":"specs/stf_post_tx.qnt","status":"passed","description":"Created by Quint on Wed Feb 25 2026 16:32:43 GMT+0100 (Central European Standard Time)","timestamp":1772033563572},"vars":["storage","accounts","last_result"],"states":[{"#meta":{"index":0},"accounts":{"#set":[]},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[]},"storage":{"#map":[]}},{"#meta":{"index":1},"accounts":{"#set":[{"#bigint":"100"}]},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[]},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}},{"#meta":{"index":2},"accounts":{"#set":[{"#bigint":"100"}]},"last_result":{"gas_used":{"#bigint":"20"},"tx_results":[{"gas_used":{"#bigint":"20"},"result":{"err_code":{"#bigint":"999"},"ok":false}}]},"storage":{"#map":[[{"#bigint":"100"},{"#map":[[[{"#bigint":"1"}],[{"#bigint":"11"}]]]}]]}},{"#meta":{"index":3},"accounts":{"#set":[{"#bigint":"100"}]},"last_result":{"gas_used":{"#bigint":"20"},"tx_results":[{"gas_used":{"#bigint":"20"},"result":{"err_code":{"#bigint":"999"},"ok":false}}]},"storage":{"#map":[[{"#bigint":"100"},{"#map":[[[{"#bigint":"1"}],[{"#bigint":"11"}]]]}]]}}]} \ No newline at end of file diff --git a/specs/traces/out_recursiveCallsTest_5.itf.json b/specs/traces/out_recursiveCallsTest_5.itf.json new file mode 100644 index 0000000..e4d6e04 --- /dev/null +++ b/specs/traces/out_recursiveCallsTest_5.itf.json @@ -0,0 +1 @@ +{"#meta":{"format":"ITF","format-description":"https://apalache-mc.org/docs/adr/015adr-trace.html","source":"specs/stf_call_depth.qnt","status":"passed","description":"Created by Quint on Wed Feb 25 2026 16:32:42 GMT+0100 (Central European Standard Time)","timestamp":1772033562682},"vars":["call_stack","last_result"],"states":[{"#meta":{"index":0},"call_stack":[],"last_result":{"err_code":{"#bigint":"0"},"ok":true}},{"#meta":{"index":1},"call_stack":[{"#bigint":"1"}],"last_result":{"err_code":{"#bigint":"0"},"ok":true}},{"#meta":{"index":2},"call_stack":[{"#bigint":"1"},{"#bigint":"1"}],"last_result":{"err_code":{"#bigint":"0"},"ok":true}},{"#meta":{"index":3},"call_stack":[{"#bigint":"1"},{"#bigint":"1"},{"#bigint":"1"}],"last_result":{"err_code":{"#bigint":"0"},"ok":true}},{"#meta":{"index":4},"call_stack":[{"#bigint":"1"},{"#bigint":"1"},{"#bigint":"1"}],"last_result":{"err_code":{"#bigint":"0"},"ok":true}}]} \ No newline at end of file diff --git a/specs/traces/out_returnUnwindsStackTest_2.itf.json b/specs/traces/out_returnUnwindsStackTest_2.itf.json new file mode 100644 index 0000000..7ab15ea --- /dev/null +++ b/specs/traces/out_returnUnwindsStackTest_2.itf.json @@ -0,0 +1 @@ +{"#meta":{"format":"ITF","format-description":"https://apalache-mc.org/docs/adr/015adr-trace.html","source":"specs/stf_call_depth.qnt","status":"passed","description":"Created by Quint on Wed Feb 25 2026 16:32:42 GMT+0100 (Central European Standard Time)","timestamp":1772033562680},"vars":["call_stack","last_result"],"states":[{"#meta":{"index":0},"call_stack":[],"last_result":{"err_code":{"#bigint":"0"},"ok":true}},{"#meta":{"index":1},"call_stack":[{"#bigint":"1"}],"last_result":{"err_code":{"#bigint":"0"},"ok":true}},{"#meta":{"index":2},"call_stack":[{"#bigint":"1"},{"#bigint":"2"}],"last_result":{"err_code":{"#bigint":"0"},"ok":true}},{"#meta":{"index":3},"call_stack":[{"#bigint":"1"}],"last_result":{"err_code":{"#bigint":"0"},"ok":true}},{"#meta":{"index":4},"call_stack":[{"#bigint":"1"}],"last_result":{"err_code":{"#bigint":"0"},"ok":true}}]} \ No newline at end of file diff --git a/specs/traces/out_singleCallTest_0.itf.json b/specs/traces/out_singleCallTest_0.itf.json new file mode 100644 index 0000000..b0c7e85 --- /dev/null +++ b/specs/traces/out_singleCallTest_0.itf.json @@ -0,0 +1 @@ +{"#meta":{"format":"ITF","format-description":"https://apalache-mc.org/docs/adr/015adr-trace.html","source":"specs/stf_call_depth.qnt","status":"passed","description":"Created by Quint on Wed Feb 25 2026 16:32:42 GMT+0100 (Central European Standard Time)","timestamp":1772033562678},"vars":["call_stack","last_result"],"states":[{"#meta":{"index":0},"call_stack":[],"last_result":{"err_code":{"#bigint":"0"},"ok":true}},{"#meta":{"index":1},"call_stack":[{"#bigint":"1"}],"last_result":{"err_code":{"#bigint":"0"},"ok":true}},{"#meta":{"index":2},"call_stack":[{"#bigint":"1"}],"last_result":{"err_code":{"#bigint":"0"},"ok":true}}]} \ No newline at end of file diff --git a/specs/traces/out_successfulTxTest_1.itf.json b/specs/traces/out_successfulTxTest_1.itf.json new file mode 100644 index 0000000..d4bc6e3 --- /dev/null +++ b/specs/traces/out_successfulTxTest_1.itf.json @@ -0,0 +1 @@ +{"#meta":{"format":"ITF","format-description":"https://apalache-mc.org/docs/adr/015adr-trace.html","source":"specs/stf_core.qnt","status":"passed","description":"Created by Quint on Wed Feb 25 2026 16:32:37 GMT+0100 (Central European Standard Time)","timestamp":1772033557713},"vars":["storage","accounts","block_height","last_result","last_block_tx_count"],"states":[{"#meta":{"index":0},"accounts":{"#set":[]},"block_height":{"#bigint":"0"},"last_block_tx_count":{"#bigint":"0"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[]}},{"#meta":{"index":1},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"0"},"last_block_tx_count":{"#bigint":"0"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}},{"#meta":{"index":2},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"1"},"last_block_tx_count":{"#bigint":"1"},"last_result":{"gas_used":{"#bigint":"20"},"tx_results":[{"gas_used":{"#bigint":"20"},"result":{"err_code":{"#bigint":"0"},"ok":true}}],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[[[{"#bigint":"1"}],[{"#bigint":"11"}]]]}]]}},{"#meta":{"index":3},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"1"},"last_block_tx_count":{"#bigint":"1"},"last_result":{"gas_used":{"#bigint":"20"},"tx_results":[{"gas_used":{"#bigint":"20"},"result":{"err_code":{"#bigint":"0"},"ok":true}}],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[[[{"#bigint":"1"}],[{"#bigint":"11"}]]]}]]}}]} \ No newline at end of file diff --git a/specs/traces/out_unregisteredSenderTest_9.itf.json b/specs/traces/out_unregisteredSenderTest_9.itf.json new file mode 100644 index 0000000..c08a5d6 --- /dev/null +++ b/specs/traces/out_unregisteredSenderTest_9.itf.json @@ -0,0 +1 @@ +{"#meta":{"format":"ITF","format-description":"https://apalache-mc.org/docs/adr/015adr-trace.html","source":"specs/stf_core.qnt","status":"passed","description":"Created by Quint on Wed Feb 25 2026 16:32:37 GMT+0100 (Central European Standard Time)","timestamp":1772033557728},"vars":["storage","accounts","block_height","last_result","last_block_tx_count"],"states":[{"#meta":{"index":0},"accounts":{"#set":[]},"block_height":{"#bigint":"0"},"last_block_tx_count":{"#bigint":"0"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[]}},{"#meta":{"index":1},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"0"},"last_block_tx_count":{"#bigint":"0"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}},{"#meta":{"index":2},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"1"},"last_block_tx_count":{"#bigint":"1"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[{"gas_used":{"#bigint":"0"},"result":{"err_code":{"#bigint":"100"},"ok":false}}],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}},{"#meta":{"index":3},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"1"},"last_block_tx_count":{"#bigint":"1"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[{"gas_used":{"#bigint":"0"},"result":{"err_code":{"#bigint":"100"},"ok":false}}],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}}]} \ No newline at end of file diff --git a/specs/traces/out_validationFailureTest_2.itf.json b/specs/traces/out_validationFailureTest_2.itf.json new file mode 100644 index 0000000..ba3ac70 --- /dev/null +++ b/specs/traces/out_validationFailureTest_2.itf.json @@ -0,0 +1 @@ +{"#meta":{"format":"ITF","format-description":"https://apalache-mc.org/docs/adr/015adr-trace.html","source":"specs/stf_core.qnt","status":"passed","description":"Created by Quint on Wed Feb 25 2026 16:32:37 GMT+0100 (Central European Standard Time)","timestamp":1772033557714},"vars":["storage","accounts","block_height","last_result","last_block_tx_count"],"states":[{"#meta":{"index":0},"accounts":{"#set":[]},"block_height":{"#bigint":"0"},"last_block_tx_count":{"#bigint":"0"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[]}},{"#meta":{"index":1},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"0"},"last_block_tx_count":{"#bigint":"0"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}},{"#meta":{"index":2},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"1"},"last_block_tx_count":{"#bigint":"1"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[{"gas_used":{"#bigint":"0"},"result":{"err_code":{"#bigint":"100"},"ok":false}}],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}},{"#meta":{"index":3},"accounts":{"#set":[{"#bigint":"100"}]},"block_height":{"#bigint":"1"},"last_block_tx_count":{"#bigint":"1"},"last_result":{"gas_used":{"#bigint":"0"},"tx_results":[{"gas_used":{"#bigint":"0"},"result":{"err_code":{"#bigint":"100"},"ok":false}}],"txs_skipped":{"#bigint":"0"}},"storage":{"#map":[[{"#bigint":"100"},{"#map":[]}]]}}]} \ No newline at end of file