diff --git a/README.md b/README.md index db99882..b69454a 100644 --- a/README.md +++ b/README.md @@ -26,3 +26,14 @@ rustup target add wasm32-unknown-unknown ``` bash cargo clean && cargo cosmwasm-to-quint ``` + +4. In order to run the generated tests, you'll need to add some dependencies: +```bash +cargo add cw-multi-test@0.16.2 --dev +cargo add itf@0.2.4 --dev +cargo add anyhow@1.0.83 --dev +cargo add num-bigint@0.4.4 --dev +cargo add num-traits@0.2.17 --dev +``` + +5. TODO: Add instructions on how to produce traces for the test diff --git a/src/boilerplate.rs b/src/boilerplate.rs index 32a436e..dae6a0c 100644 --- a/src/boilerplate.rs +++ b/src/boilerplate.rs @@ -3,42 +3,30 @@ use itertools::Itertools; use crate::types::Context; pub const IMPORTS: &str = " - import basicSpells.* from \"../lib/basicSpells\" - import cw_types.* from \"../lib/cw_types\" - import messaging.* from \"../lib/messaging\" - import bank from \"../lib/bank\" + import basicSpells.* from \"./lib/basicSpells\" + import cw_types.* from \"./lib/cw_types\" + import cw_utils.* from \"./lib/cw_utils\" + import messaging.* from \"./lib/messaging\" + import bank from \"./lib/bank\" "; pub const VARS: &str = " var contract_state: ContractState - var return: Result + var result: Result var bank: bank::Bank var time: int "; pub const CONTRACT_ADDRESS: &str = " - pure val CONTRACT_ADDRESS = \"\" + pure val CONTRACT_ADDRESS = \"contract0\" "; pub const VALUES: &str = " - pure val ADDRESSES = Set(\"s1\", \"s2\", \"s3\", CONTRACT_ADDRESS) + pure val ADDRESSES = Set(\"sender1\", \"sender2\", \"sender3\", CONTRACT_ADDRESS) pure val DENOMS = Set(\"d1\", \"uawesome\") pure val MAX_AMOUNT = 200 "; -pub const INITIALIZERS: &str = " - pure val init_bank_state = ADDRESSES.mapBy(_ => DENOMS.mapBy(_ => MAX_AMOUNT)) - - val env_val = { block: { time: time } } - - action init = all { - contract_state' = init_contract_state, - bank' = init_bank_state, - return' = Err(\"No previous request\"), - time' = 0, - } -"; - pub const ACTIONS: &str = " action execute_message(message, max_funds) = { nondet sender = ADDRESSES.oneOf() @@ -50,9 +38,12 @@ pub const ACTIONS: &str = " val r = execute(contract_state, env_val, info, message) all { bank.get(sender).get(denom) >= amount, - bank' = bank.setBy(sender, balances => balances.setBy(denom, balance => balance - amount)) - .setBy(CONTRACT_ADDRESS, balances => balances.setBy(denom, balance => balance + amount)), - return' = r._1, + match r._1 { + | Ok(_) => bank' = bank.setBy(sender, balances => balances.setBy(denom, balance => balance - amount)) + .setBy(CONTRACT_ADDRESS, balances => balances.setBy(denom, balance => balance + amount)) + | Err(_) => bank' = bank + }, + result' = r._1, contract_state' = r._2, } } @@ -60,16 +51,16 @@ pub const ACTIONS: &str = " action advance_time = time' = time + 1 action step = { - val message_getting = get_message(return) - val new_return = message_getting._1 + val message_getting = get_message(result) + val new_result = message_getting._1 val opt_message = message_getting._2 match opt_message { | Some(submsg) => { - val current_state = { bank: bank, return: new_return, contract_state: contract_state } + val current_state = { bank: bank, result: new_result, contract_state: contract_state } val new_state = process_message(current_state, env_val, CONTRACT_ADDRESS, submsg, reply) all { bank' = new_state.bank, - return' = new_state.return, + result' = new_state.result, contract_state' = new_state.contract_state, advance_time, } @@ -90,10 +81,43 @@ pub fn pre_items(crate_name: &str) -> String { ) } +pub fn initializers(ctx: &Context) -> String { + let instatiate_msg = ctx.message_type_for_action.get("instantiate").unwrap(); + format!( + " + pure val init_bank_state = ADDRESSES.mapBy(_ => DENOMS.mapBy(_ => MAX_AMOUNT)) + + val env_val = {{ block: {{ time: time }} }} + + action init = {{ + // TODO: Change next line according to fund expectations + pure val max_funds = 0 + + nondet sender = Set(\"admin\").oneOf() + nondet denom = DENOMS.oneOf() + nondet amount = 0.to(max_funds).oneOf() + val funds = [{{ denom: denom, amount: amount }}] + val info = {{ sender: sender, funds: funds }} + + pure val message: InstantiateMsg = {} + pure val r = instantiate(init_contract_state, {{ block: {{ time: 0 }} }}, info, message) + + all {{ + contract_state' = r._2, + bank' = init_bank_state, + result' = r._1, + time' = 0, + }} + }} +", + init_value_for_type(ctx, instatiate_msg.clone()) + ) +} + // TODO: This doesn't belong here, but I'm not sure where to put it /// Generates a default value for a given type, used to initialize values of all /// contract state fields -fn init_value_for_type(ctx: &Context, ty: String) -> String { +pub fn init_value_for_type(ctx: &Context, ty: String) -> String { if ty.contains("->") { return "Map()".to_string(); } @@ -137,29 +161,21 @@ pub fn post_items(ctx: &Context) -> String { .iter() .map(|x| format!("{}: {}", x.0, x.1)) .collect_vec() - .join(",\n "); + .join(",\n "); // After all items were visited, we can produce the complete contract state initializer let initializer = ctx .contract_state .iter() - .map(|field| { - format!( - " {}: {}", - field.0, - init_value_for_type(ctx, field.1.clone()) - ) - }) + .map(|field| format!("{}: {}", field.0, init_value_for_type(ctx, field.1.clone()))) .collect_vec() - .join(",\n"); + .join(",\n "); let special_actions = ["execute", "instantiate", "reply"]; let reply = if !ctx.ops_with_mutability.contains(&"reply".to_string()) { // Generate default reply to be given for the message handler " - pure def reply(state: ContractState, _env: Env, _reply: Reply): (Result, ContractState) = (Ok(Response_new), state) - " } else { "\n" @@ -190,8 +206,9 @@ pub fn post_items(ctx: &Context) -> String { advance_time, }} {reply} -{INITIALIZERS} +{} {ACTIONS} -}}" +}}", + initializers(ctx) ) } diff --git a/src/lib.rs b/src/lib.rs index bc347ca..8345b58 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -5,6 +5,7 @@ pub mod boilerplate; pub mod nondet; pub mod state_extraction; +pub mod test_generation; pub mod translate; pub mod types; @@ -30,6 +31,7 @@ use translate::Translatable; use crate::types::{Constructor, Context}; use crate::boilerplate::{post_items, pre_items}; +use crate::test_generation::generate_tests; // This struct is the plugin provided to the rustc_plugin framework, // and it must be exported for use by the CLI/driver binaries. @@ -125,13 +127,14 @@ fn translate_all_items(tcx: TyCtxt) { items_by_crate.into_iter().for_each(|(crate_id, items)| { let crate_name = tcx.crate_name(crate_id); - traslate_items(tcx, crate_name.as_str(), items.collect_vec()) + translate_items(tcx, crate_name.as_str(), items.collect_vec()) }); } -fn traslate_items(tcx: TyCtxt, crate_name: &str, items: Vec<&rustc_hir::Item>) { +fn translate_items(tcx: TyCtxt, crate_name: &str, items: Vec<&rustc_hir::Item>) { let mut ctx = Context { tcx, + crate_name, message_type_for_action: HashMap::from([( "instantiate".to_string(), "InstantiateMsg".to_string(), @@ -147,6 +150,11 @@ fn traslate_items(tcx: TyCtxt, crate_name: &str, items: Vec<&rustc_hir::Item>) { structs: HashMap::new(), ops_with_mutability: vec![], contract_state: vec![], + nondet_picks: vec![ + ("sender".to_string(), "Addr".to_string()), + ("denom".to_string(), "str".to_string()), + ("amount".to_string(), "int".to_string()), + ], // scoped record_fields: vec![], struct_fields: vec![], @@ -170,12 +178,46 @@ fn traslate_items(tcx: TyCtxt, crate_name: &str, items: Vec<&rustc_hir::Item>) { return; } - println!("{}", pre_items(crate_name)); - println!("{}", translated_items); - println!("{}", post_items(&ctx)); + let module = format!( + "{}\n{}\n{}\n", + pre_items(crate_name), + translated_items, + post_items(&ctx) + ); + let tests = generate_tests(ctx.clone()); + + // write module to file + std::fs::write(format!("quint/{}_stubs.qnt", crate_name), module) + .expect("Unable to write file"); + + // write tests to file + std::fs::write(format!("tests/mbt_{}.rs", crate_name), tests).expect("Unable to write file"); } // This is the main entry point for the plugin. It prints the generated quint code to STDOUT. fn cosmwasm_to_quint(tcx: TyCtxt, _args: &CosmwasmToQuintPluginArgs) { + // create directories for the output files (if they don't already exist) + std::fs::create_dir_all("quint/lib").expect("Unable to create directory"); + std::fs::create_dir_all("tests").expect("Unable to create directory"); + + // Read quint lib files. `include_str!` makes it so they are read at + // compilation time, and therefore get embeded in the cosmwasm-to-quint executable + let bank = include_str!("./quint-lib-files/bank.qnt"); + let basic_spells = include_str!("./quint-lib-files/basicSpells.qnt"); + let bounded_uint = include_str!("./quint-lib-files/BoundedUInt.qnt"); + let cw_types = include_str!("./quint-lib-files/cw_types.qnt"); + let cw_utils = include_str!("./quint-lib-files/cw_utils.qnt"); + let messaging = include_str!("./quint-lib-files/messaging.qnt"); + + // Write the lib files in runtime + std::fs::write("quint/lib/bank.qnt", bank).expect("Unable to write file"); + std::fs::write("quint/lib/basicSpells.qnt", basic_spells).expect("Unable to write file"); + std::fs::write("quint/lib/BoundedUInt.qnt", bounded_uint).expect("Unable to write file"); + std::fs::write("quint/lib/cw_types.qnt", cw_types).expect("Unable to write file"); + std::fs::write("quint/lib/cw_utils.qnt", cw_utils).expect("Unable to write file"); + std::fs::write("quint/lib/messaging.qnt", messaging).expect("Unable to write file"); + translate_all_items(tcx); + + println!("Sucessfully generated files. Quint files are inside quint/ and test files are inside tests/.") } diff --git a/src/nondet.rs b/src/nondet.rs index 635414d..60b111c 100644 --- a/src/nondet.rs +++ b/src/nondet.rs @@ -17,15 +17,16 @@ pub trait NondetValue: Translatable { fn nondet_definition(&self, ctx: &mut Context, ident: &str) -> String { let info = self.nondet_info(ctx, ident); let ty = self.translate(ctx); - nondet_info_to_def(info, &ty, ident) + nondet_info_to_def(ctx, info, &ty, ident) } } /// Converts a NondetInfo to a definition for a nondeterministic value with the /// given identifier, ready to be printed. -fn nondet_info_to_def(info: NondetInfo, ty: &str, ident: &str) -> String { +fn nondet_info_to_def(ctx: &mut Context, info: NondetInfo, ty: &str, ident: &str) -> String { let (auxiliary_defs, value) = info; if auxiliary_defs.is_empty() { + ctx.nondet_picks.push((ident.to_string(), ty.to_string())); format!("nondet {}: {} = {}.oneOf()", ident, ty, value) } else { format!( @@ -82,25 +83,9 @@ fn nondet_value_for_list(ty: &rustc_hir::Ty<'_>, ctx: &mut Context, ident: &str) return (element_defs, format!("[{element_value}]")); } - let defs = vec![ - format!( - "val possibilities = {}.map(i => Some(i)).union(Set(None))", - element_value - ), - "nondet v1 = possibilities.oneOf()".to_string(), - "nondet v2 = possibilities.oneOf()".to_string(), - "nondet v3 = possibilities.oneOf()".to_string(), - ]; - - let value = " - [v1, v2, v3].foldl([], (acc, v) => match v { - | Some(i) => acc.append(i) - | None => acc - }) -" - .to_string(); + let value = format!("{element_value}.allListsUpTo(2)"); - (defs, value) + (vec![], value) } fn nondet_value_for_option(ty: &rustc_hir::Ty<'_>, ctx: &mut Context, ident: &str) -> NondetInfo { @@ -122,13 +107,14 @@ fn nondet_value_for_option(ty: &rustc_hir::Ty<'_>, ctx: &mut Context, ident: &st } impl NondetValue for Vec { - fn nondet_info(&self, _ctx: &mut Context, ident: &str) -> NondetInfo { + fn nondet_info(&self, ctx: &mut Context, ident: &str) -> NondetInfo { // Each field needs its own named nondet value, in the form of // `nondet ident_field_name: field_type = something.oneOf()` let defs = self .iter() .map(|field| { nondet_info_to_def( + ctx, field.nondet_info.clone(), &field.ty, format!("{}_{}", ident, field.name).as_str(), diff --git a/src/quint-lib-files/basicSpells.qnt b/src/quint-lib-files/basicSpells.qnt index 02f8c54..f7588e4 100644 --- a/src/quint-lib-files/basicSpells.qnt +++ b/src/quint-lib-files/basicSpells.qnt @@ -171,4 +171,15 @@ module basicSpells { pure def listFilter(l: List[a], f: (a) => bool): List[a] = l.foldl([], (acc, e) => if (f(e)) acc.append(e) else acc) + + pure def listMap(l: List[a], f: (a) => b): List[b] = + l.foldl([], (acc, e) => acc.append(f(e))) + + //// Returns a set of the elements in the list. + //// + //// - @param l a list + //// - @returns a set of the elements in l + pure def toSet(l: List[a]): Set[a] = { + l.foldl(Set(), (s, e) => s.union(Set(e))) + } } diff --git a/src/quint-lib-files/cw_utils.qnt b/src/quint-lib-files/cw_utils.qnt index 65597a6..e662dbe 100644 --- a/src/quint-lib-files/cw_utils.qnt +++ b/src/quint-lib-files/cw_utils.qnt @@ -10,7 +10,7 @@ module cw_utils { } else if (info.funds.indices().size() == 1) { val coin = info.funds[0] if (coin.amount == 0) { - Err("No funds") + Err("Zero funds") } else { Ok(coin) } @@ -24,7 +24,7 @@ module cw_utils { | Err(err) => Err(err) | Ok(coin) => { if (coin.denom != denom) { - Err("Missing Denom") + Err("Wrong Denom") } else { Ok(coin.amount) } diff --git a/src/quint-lib-files/messaging.qnt b/src/quint-lib-files/messaging.qnt index 32ea905..b0ef7dc 100644 --- a/src/quint-lib-files/messaging.qnt +++ b/src/quint-lib-files/messaging.qnt @@ -5,18 +5,18 @@ module messaging { import bank from "./bank" import basicSpells.* from "./basicSpells" - pure def get_message(return_val: Result[Response, ContractError]): (Result[Response, ContractError], Option[SubMsg]) = { - match return_val { + pure def get_message(result_val: Result[Response, ContractError]): (Result[Response, ContractError], Option[SubMsg]) = { + match result_val { | Ok(response) => if (response.messages.indices().size() > 0) { val submsg = response.messages.head() - val new_return = Ok({ ...response, messages: response.messages.listFilter(m => m != submsg) }) - (new_return, Some(submsg)) + val new_result = Ok({ ...response, messages: response.messages.listFilter(m => m != submsg) }) + (new_result, Some(submsg)) } else { - (return_val, None) + (result_val, None) } - | _ => (return_val, None) + | _ => (result_val, None) } } @@ -29,16 +29,16 @@ module messaging { | Ok(new_bank) => if (should_reply_on_success(submsg.reply_on)) { val reply_result = reply(state.contract_state, env, { id: submsg.id, result: Ok({ events: [/* TODO */], data: None }) }) - { bank: new_bank, return: reply_result._1, contract_state: reply_result._2 } + { bank: new_bank, result: reply_result._1, contract_state: reply_result._2 } } else { { ...state, bank: new_bank } } | Err(err) => if (should_reply_on_error(submsg.reply_on)) { val reply_result = reply(state.contract_state, env, { id: submsg.id, result: Err(err) }) - { ...state, return: reply_result._1, contract_state: reply_result._2 } + { ...state, result: reply_result._1, contract_state: reply_result._2 } } else { - state + { ...state, result: Err(err) } } } } diff --git a/src/test_generation/actions.rs b/src/test_generation/actions.rs new file mode 100644 index 0000000..0cb37ac --- /dev/null +++ b/src/test_generation/actions.rs @@ -0,0 +1,135 @@ +use crate::boilerplate::init_value_for_type; +use crate::test_generation::boilerplate::*; +use crate::types::{fallback_constructor, Context}; +use itertools::Itertools; + +/// Generates one match arm per action on the model: +/// "foo_action" => // run foo and compare result +/// "bar_action" => // run bar and compare result +pub fn arms_for_actions(ctx: Context) -> String { + ctx.message_type_for_action + .iter() + // Sort items by name so that the generated code is deterministic + .sorted_by(|a, b| a.0.cmp(b.0)) + .map(|(action, ty)| { + if action == "instantiate" { + let msg = generate_instantiate_msg(ctx.clone()); + return arm_for_init(msg); + } + + let msg = generate_message(ctx.clone(), ty.clone()); + arm_for_action(action, msg) + }) + .join("\n") +} + +fn arm_for_action(action_name: &str, msg: String) -> String { + format!( + " + \"{action_name}_action\" => {{ + {EXTRACT_SENDER_AND_FUNDS} + {msg} + {PRINT_MESSAGE_FIELDS} + {EXECUTE_CONTRACT} + {COMPARE_RESULT} + }} +" + ) +} + +fn arm_for_init(msg: String) -> String { + format!( + " + \"q::init\" => {{ + println!(\"Initializing contract.\"); + + {EXTRACT_SENDER_AND_FUNDS} + {msg} + {PRINT_MESSAGE_FIELDS} + {INITIALIZE_CONTRACT} + {MINT_TOKENS} + }} +" + ) +} + +fn generate_instantiate_msg(ctx: Context) -> String { + let msg_struct = ctx + .structs + .get("InstantiateMsg") + .cloned() + .unwrap_or_default(); + + let msg_fields = msg_struct + .iter() + .map(|f| { + let body = init_value_for_type(&ctx, f.ty.clone()); + + format!("{}: {}", f.name, body) + }) + .collect_vec(); + + format!("let msg = InstantiateMsg {{ {} }};", msg_fields.join(", ")) +} + +fn generate_message(ctx: Context, ty: String) -> String { + let constructor = ctx + .constructors + .get(ty.as_str()) + .cloned() + .unwrap_or_else(|| fallback_constructor(ty.as_ref())); + + let nondet_picks = constructor + .fields + .iter() + .map(|f| { + let body = type_conversion( + format!("nondet_picks.message_{}.clone().unwrap()", f.name), + f.ty.clone(), + ); + + format!("let message_{} = {};", f.name, body) + }) + .collect_vec(); + + let fields = constructor + .fields + .iter() + .map(|f| format!("{}: message_{}", f.name, f.name)) + .collect_vec() + .join(", "); + + let message_type = constructor.name.replace('_', "::"); + + let msg_def = format!("let msg = {message_type} {{ {fields} }};"); + + [nondet_picks, vec![msg_def]] + .concat() + .join("\n ") +} + +fn type_conversion(value: String, ty: String) -> String { + if ty.starts_with("List") { + // FIXME: we should have an intermediate representation for types so we + // don't have to convert to and from strings like this. + return format!( + "{}.iter().map(|x| {}).collect()", + value, + type_conversion( + "x".to_string(), + ty.trim_start_matches("List[") + .trim_end_matches(']') + .to_string() + ) + ); + } + + // TODO: convert other types + + match ty.as_str() { + "str" => value, + "int" => format!("{}.to_u64().unwrap().into()", value), + "Addr" => format!("Addr::unchecked_from({})", value), + _ => value, + } +} diff --git a/src/test_generation/boilerplate.rs b/src/test_generation/boilerplate.rs new file mode 100644 index 0000000..28c3a77 --- /dev/null +++ b/src/test_generation/boilerplate.rs @@ -0,0 +1,228 @@ +pub fn test_header(crate_name: &str) -> String { + format!( + " +#[cfg(test)] +pub mod tests {{ + use {crate_name}::contract; + use {crate_name}::msg::{{ExecuteMsg, InstantiateMsg}}; + +{TEST_AUX} +" + ) +} + +const TEST_AUX: &str = " + use crate::state_structs::*; + use cosmwasm_std::{coin, Addr, Uint128}; + use cw_multi_test::{App, AppResponse, ContractWrapper, Executor}; + use itf::trace_from_str; + use num_bigint::BigInt; + use num_traits::{ToPrimitive, Zero}; + + pub const DENOM: &str = \"uawesome\"; + pub const TICK: u64 = 1; + + pub fn mint_tokens(mut app: App, recipient: String, denom: String, amount: Uint128) -> App { + app.sudo(cw_multi_test::SudoMsg::Bank( + cw_multi_test::BankSudo::Mint { + to_address: recipient.to_owned(), + amount: vec![coin(amount.u128(), denom)], + }, + )) + .unwrap(); + app + } + + fn compare_state(test_state: &TestState, app: &App, state: &State) { + // compare contract balances + let balance = app + .wrap() + .query_balance(&test_state.contract_addr, DENOM) + .unwrap() + .amount; + let trace_balance = state + .bank + .get(&test_state.contract_addr.to_string()) + .and_then(|x| x.get(DENOM)) + .and_then(|x| x.to_u128()) + .unwrap_or(0); + println!( + \"Contract balance ({:?}) for {DENOM}: {:?} vs {:?}\", + test_state.contract_addr, + balance, + Uint128::new(trace_balance) + ); + assert_eq!(balance, Uint128::new(trace_balance)); + + // TODO: Query the contract and compare the state as you wish + } + + fn compare_result( + trace_result: Result, + app_result: Result, + ) { + if trace_result.is_ok() { + assert!( + app_result.is_ok(), + \"Action unexpectedly failed, error: {:?}\", + app_result.err() + ); + println!(\"Action successful as expected\"); + } else { + assert!( + app_result.is_err(), + \"Expected action to fail with error: {:?}\", + trace_result.err() + ); + println!(\"Action failed as expected\"); + } + } + + fn funds_from_trace(amount: Option, denom: Option) -> Vec { + if amount.is_none() || denom.is_none() || amount == Some(Zero::zero()) { + return vec![]; + } + + vec![coin( + amount.as_ref().unwrap().to_u128().unwrap(), + denom.unwrap(), + )] + } + + // Testing is stateful. + struct TestState { + // we will only know the contract address once we have processed an `instantiate` step + pub contract_addr: Addr, + } + + #[test] + fn model_test() { + let mut app = App::default(); + let code = ContractWrapper::new(contract::execute, contract::instantiate, contract::query); + let code_id = app.store_code(Box::new(code)); + + // create test state + let mut test_state = TestState { + contract_addr: Addr::unchecked(\"contract0\"), + }; + + // load trace data + let data = include_str!(\"../quint/test.itf.json\"); + let trace: itf::Trace = trace_from_str(data).unwrap(); + + for s in trace.states { + let last_result = s.value.result.clone(); + if last_result.is_ok() && !last_result.unwrap().messages.is_empty() { + println!(\"Processing messages, skipping\"); + continue; + } + + let action_taken = &s.value.action_taken; + let nondet_picks = &s.value.nondet_picks; + let amount = nondet_picks.amount.clone(); + let denom = nondet_picks.denom.clone(); + let sender = nondet_picks.sender.clone(); + + println!(\"Step number: {:?}\", s.meta.index); + println!(\"Result from trace: {:?}\", s.value.result.clone()); + + match action_taken.as_str() { +"; + +pub const TEST_FOOTER: &str = " + _ => panic!(\"Invalid action taken\"), + } + compare_state(&test_state, &app, &(s.value.clone())); + println!( + \"clock is advancing for {} seconds\", + TICK + ); + app.update_block(|block| { + block.time = block.time.plus_seconds(TICK); + }); + println!(\"-----------------------------------\"); + } + } +} +"; + +pub const PRINT_MESSAGE_FIELDS: &str = "println!(\"Message: {:?}\", msg); + println!(\"Sender: {:?}\", sender); + println!(\"Funds: {:?}\", funds); +"; + +pub const EXECUTE_CONTRACT: &str = "let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); +"; + +pub const COMPARE_RESULT: &str = "compare_result(s.value.result.clone(), res)"; + +pub const EXTRACT_SENDER_AND_FUNDS: &str = "let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); +"; + +pub const INITIALIZE_CONTRACT: &str = "test_state.contract_addr = app.instantiate_contract( + code_id, + sender, + &msg, + &funds, + \"test\", + None, + ).unwrap(); +"; + +pub const MINT_TOKENS: &str = "for (addr, coins) in s.value.bank.clone().iter() { + for (denom, amount) in coins.iter() { + app = mint_tokens( + app, + addr.clone(), + denom.to_string(), + Uint128::new(amount.to_u128().unwrap()), + ); + } + } +"; + +pub const STRUCTS_MODULE_IMPORTS: &str = "use num_bigint::BigInt; + use serde::Deserialize; + use std::collections::HashMap; + use itf::de::{self, As};"; + +pub const DEFAULT_STRUCTS: &str = " + #[derive(Clone, Debug, Deserialize)] + pub struct Message {} + #[derive(Clone, Debug, Deserialize)] + pub struct Attribute { + pub key: String, + pub value: QuintSerializedValue, + } + + #[derive(Clone, Debug, Deserialize)] + #[serde(tag = \"tag\", content = \"value\")] + pub enum QuintSerializedValue { + FromInt(BigInt), + FromStr(String), + FromListInt(Vec), + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Response { + pub messages: Vec, + pub attributes: Vec, + } + + #[derive(Clone, Debug, Deserialize)] + pub struct State { + pub contract_state: ContractState, + pub bank: HashMap>, + #[serde(with = \"As::>\")] + pub result: Result, + pub action_taken: String, + pub nondet_picks: NondetPicks, + pub time: BigInt, + } +"; diff --git a/src/test_generation/mod.rs b/src/test_generation/mod.rs new file mode 100644 index 0000000..811b6e1 --- /dev/null +++ b/src/test_generation/mod.rs @@ -0,0 +1,15 @@ +use crate::types::Context; + +mod actions; +mod boilerplate; +mod structs; + +pub fn generate_tests(ctx: Context) -> String { + format!( + "{}{}{}{}", + structs::translate_structs(ctx.clone()), + boilerplate::test_header(ctx.crate_name), + actions::arms_for_actions(ctx), + boilerplate::TEST_FOOTER + ) +} diff --git a/src/test_generation/structs.rs b/src/test_generation/structs.rs new file mode 100644 index 0000000..93444d0 --- /dev/null +++ b/src/test_generation/structs.rs @@ -0,0 +1,102 @@ +use crate::test_generation::boilerplate::*; +use crate::types::Context; +use itertools::Itertools; + +/// Defines a module with all necesary structs for the contract state and messages. +pub fn translate_structs(ctx: Context) -> String { + let contract_structs = ctx + .structs + .iter() + // Sort items by name so that the generated code is deterministic + .sorted_by(|a, b| a.0.cmp(b.0)) + .map(|(name, fields)| { + let field_tuples = fields + .iter() + .map(|f| (f.name.clone(), f.ty.clone())) + .collect_vec(); + + format_struct(name.to_string(), field_tuples, false) + }) + .collect_vec() + .join("\n"); + + let contract_state_struct = format_struct( + "ContractState".to_string(), + ctx.contract_state.clone(), + false, + ); + + let nondet_picks_struct = + format_struct("NondetPicks".to_string(), ctx.nondet_picks.clone(), true); + + format!( + " +pub mod state_structs {{ + {STRUCTS_MODULE_IMPORTS} + {contract_structs} + {contract_state_struct} + {nondet_picks_struct} + {DEFAULT_STRUCTS} +}} + " + ) +} + +fn format_struct(name: String, fields: Vec<(String, String)>, optional: bool) -> String { + let fields = fields + .iter() + .map(|(name, ty)| { + let typ = translate_type(ty.clone()); + if optional { + format!( + " + #[serde(with = \"As::>\")] + pub {name}: Option<{typ}>" + ) + } else { + format!("pub {name}: {typ}") + } + }) + .join(",\n "); + + format!( + " + #[derive(Clone, Debug, Deserialize)] + pub struct {name} {{ + {fields} + }}" + ) +} + +fn translate_type(ty: String) -> String { + // FIXME: we should have an intermediate representation for types so we + // don't have to convert to and from strings like this. + if ty.contains("->") { + let it = ty.split("->").collect_vec(); + let key = it[0]; + let value = it[1..].join("->"); + return format!( + "HashMap<{}, {}>", + translate_type(key.trim().to_string()), + translate_type(value.trim().to_string()) + ); + } + + if ty.starts_with("List") { + return format!( + "Vec<{}>", + translate_type( + ty.trim_start_matches("List[") + .trim_end_matches(']') + .to_string() + ) + ); + } + + match ty.as_str() { + "str" => "String".to_string(), + "int" => "BigInt".to_string(), + "Addr" => "String".to_string(), + _ => ty, + } +} diff --git a/src/translate.rs b/src/translate.rs index 19012e2..9dd4d5f 100644 --- a/src/translate.rs +++ b/src/translate.rs @@ -534,18 +534,20 @@ impl Translatable for rustc_hir::Item<'_> { if name == "instantiate" || name == "reply" { // instantiate explanation: // - // FIXME: We need to do something about instantiate - // Instantiate is a stateful function (taking state as an - // argument and returning it) But currently we don't call it - // in the state machine (from `step`). We probably need to - // update the boilerplate stuff to call it. + // Instantiate is a special def that will be called on init // // reply explanation: // // Reply is a special def that will be called when // processing a message with a compatible reply_on field. We // don't want to generate a nondet action for it. - return format!(" pure def {name}{sig} = ({body_value}, state)"); + return format!( + " pure def {name}{sig} = {{ + // TODO: Update body + ({body_value}, state) + }} +" + ); } let ctor: Constructor = ctx @@ -557,7 +559,11 @@ impl Translatable for rustc_hir::Item<'_> { let nondet_value = ctor.nondet_definition(ctx, "message"); format!( - " pure def {name}{sig} = ({body_value}, state) + " + pure def {name}{sig} = {{ + // TODO: Update body + ({body_value}, state) + }} action {name}_action = {{ // TODO: Change next line according to fund expectations diff --git a/src/types.rs b/src/types.rs index 8536500..ad1637f 100644 --- a/src/types.rs +++ b/src/types.rs @@ -28,14 +28,16 @@ pub struct Function<'f> { } #[derive(Clone)] -pub struct Context<'tcx> { +pub struct Context<'tcx, 'c> { // global + pub crate_name: &'c str, pub message_type_for_action: HashMap, pub constructors: HashMap, pub structs: HashMap>, pub ops_with_mutability: Vec, pub tcx: TyCtxt<'tcx>, pub contract_state: Vec<(String, String)>, + pub nondet_picks: Vec<(String, String)>, // scoped // FIXME: This should be a stack to account for nested scopes. // No need to worry about nested scopes for stub generation. diff --git a/tests/integration_tests.rs b/tests/integration_tests.rs index a7d3579..e6a8297 100644 --- a/tests/integration_tests.rs +++ b/tests/integration_tests.rs @@ -1,4 +1,4 @@ -use std::{env, fs, path::Path, process::Command, sync::Once}; +use std::{env, fs, io, path::Path, process::Command, sync::Once}; use anyhow::{ensure, Context, Result}; @@ -44,7 +44,47 @@ fn run(dir: &str, f: impl FnOnce(&mut Command)) -> Result { String::from_utf8(output.stderr)? ); - Ok(String::from_utf8(output.stdout)?) + let mut quint_entries = fs::read_dir(ws.join("quint"))? + .map(|res| res.map(|e| e.path())) + .collect::, io::Error>>()?; + quint_entries.sort(); + + let quint_files = quint_entries + .iter() + .map(|path| { + if path.is_dir() { + return "".to_string(); + } + format!( + "{}:\n{}", + path.clone().file_name().unwrap().to_string_lossy(), + fs::read_to_string(path).expect("Should have been able to read the file"), + ) + }) + .collect::>() + .join("\n\n"); + + let mut mbt_entries = fs::read_dir(ws.join("tests"))? + .map(|res| res.map(|e| e.path())) + .collect::, io::Error>>()?; + mbt_entries.sort(); + + let mbt_files = mbt_entries + .iter() + .map(|path| { + if path.is_dir() { + return "".to_string(); + } + format!( + "{}:\n{}", + path.clone().file_name().unwrap().to_string_lossy(), + fs::read_to_string(path).expect("Should have been able to read the file"), + ) + }) + .collect::>() + .join("\n\n"); + + Ok(format!("quint:\n{}\n\nmbt:\n{}", quint_files, mbt_files)) } #[test] diff --git a/tests/snapshots/integration_tests__ctf01.snap b/tests/snapshots/integration_tests__ctf01.snap index 2e4d5b8..1baa8cb 100644 --- a/tests/snapshots/integration_tests__ctf01.snap +++ b/tests/snapshots/integration_tests__ctf01.snap @@ -2,24 +2,29 @@ source: tests/integration_tests.rs expression: output --- +quint: + + +oaksecurity_cosmwasm_ctf_01_stubs.qnt: module oaksecurity_cosmwasm_ctf_01 { - import basicSpells.* from "../lib/basicSpells" - import cw_types.* from "../lib/cw_types" - import messaging.* from "../lib/messaging" - import bank from "../lib/bank" + import basicSpells.* from "./lib/basicSpells" + import cw_types.* from "./lib/cw_types" + import cw_utils.* from "./lib/cw_utils" + import messaging.* from "./lib/messaging" + import bank from "./lib/bank" var contract_state: ContractState - var return: Result + var result: Result var bank: bank::Bank var time: int - pure val CONTRACT_ADDRESS = "" + pure val CONTRACT_ADDRESS = "contract0" - pure val ADDRESSES = Set("s1", "s2", "s3", CONTRACT_ADDRESS) + pure val ADDRESSES = Set("sender1", "sender2", "sender3", CONTRACT_ADDRESS) pure val DENOMS = Set("d1", "uawesome") pure val MAX_AMOUNT = 200 @@ -29,12 +34,20 @@ module oaksecurity_cosmwasm_ctf_01 { type ExecuteMsg = | ExecuteMsg_Deposit | ExecuteMsg_Withdraw({ ids: List[int] }) - pure def instantiate(state: ContractState, _env: Env, _info: MessageInfo, _msg: InstantiateMsg): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + pure def instantiate(state: ContractState, _env: Env, _info: MessageInfo, _msg: InstantiateMsg): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } + pure def execute(state: ContractState, env: Env, info: MessageInfo, msg: ExecuteMsg): (Result[Response, ContractError], ContractState) = match msg { | ExecuteMsg_Deposit(__r) => deposit(state, env, info) | ExecuteMsg_Withdraw(__r) => withdraw(state, env, info, __r.ids) } - pure def deposit(state: ContractState, env: Env, info: MessageInfo): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def deposit(state: ContractState, env: Env, info: MessageInfo): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action deposit_action = { // TODO: Change next line according to fund expectations @@ -43,21 +56,16 @@ module oaksecurity_cosmwasm_ctf_01 { pure val message: ExecuteMsg = ExecuteMsg_Deposit execute_message(message, max_funds) } - pure def withdraw(state: ContractState, env: Env, info: MessageInfo, ids: List[int]): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def withdraw(state: ContractState, env: Env, info: MessageInfo, ids: List[int]): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action withdraw_action = { // TODO: Change next line according to fund expectations pure val max_funds = MAX_AMOUNT - val possibilities = 0.to(MAX_AMOUNT).map(i => Some(i)).union(Set(None)) - nondet v1 = possibilities.oneOf() - nondet v2 = possibilities.oneOf() - nondet v3 = possibilities.oneOf() - pure val message_ids: List[int] = - [v1, v2, v3].foldl([], (acc, v) => match v { - | Some(i) => acc.append(i) - | None => acc - }) - + nondet message_ids: List[int] = 0.to(MAX_AMOUNT).allListsUpTo(2).oneOf() pure val message: ExecuteMsg = ExecuteMsg_Withdraw({ ids: message_ids }) execute_message(message, max_funds) } @@ -67,11 +75,11 @@ module oaksecurity_cosmwasm_ctf_01 { type ContractState = { last_id: int, - lockups: int -> Lockup + lockups: int -> Lockup } pure val init_contract_state = { - last_id: 0, + last_id: 0, lockups: Map() } @@ -83,20 +91,32 @@ module oaksecurity_cosmwasm_ctf_01 { advance_time, } - pure def reply(state: ContractState, _env: Env, _reply: Reply): (Result, ContractState) = (Ok(Response_new), state) - pure val init_bank_state = ADDRESSES.mapBy(_ => DENOMS.mapBy(_ => MAX_AMOUNT)) val env_val = { block: { time: time } } - action init = all { - contract_state' = init_contract_state, - bank' = init_bank_state, - return' = Err("No previous request"), - time' = 0, + action init = { + // TODO: Change next line according to fund expectations + pure val max_funds = 0 + + nondet sender = Set("admin").oneOf() + nondet denom = DENOMS.oneOf() + nondet amount = 0.to(max_funds).oneOf() + val funds = [{ denom: denom, amount: amount }] + val info = { sender: sender, funds: funds } + + pure val message: InstantiateMsg = { count: 0 } + pure val r = instantiate(init_contract_state, { block: { time: 0 } }, info, message) + + all { + contract_state' = r._2, + bank' = init_bank_state, + result' = r._1, + time' = 0, + } } @@ -110,9 +130,12 @@ module oaksecurity_cosmwasm_ctf_01 { val r = execute(contract_state, env_val, info, message) all { bank.get(sender).get(denom) >= amount, - bank' = bank.setBy(sender, balances => balances.setBy(denom, balance => balance - amount)) - .setBy(CONTRACT_ADDRESS, balances => balances.setBy(denom, balance => balance + amount)), - return' = r._1, + match r._1 { + | Ok(_) => bank' = bank.setBy(sender, balances => balances.setBy(denom, balance => balance - amount)) + .setBy(CONTRACT_ADDRESS, balances => balances.setBy(denom, balance => balance + amount)) + | Err(_) => bank' = bank + }, + result' = r._1, contract_state' = r._2, } } @@ -120,16 +143,16 @@ module oaksecurity_cosmwasm_ctf_01 { action advance_time = time' = time + 1 action step = { - val message_getting = get_message(return) - val new_return = message_getting._1 + val message_getting = get_message(result) + val new_result = message_getting._1 val opt_message = message_getting._2 match opt_message { | Some(submsg) => { - val current_state = { bank: bank, return: new_return, contract_state: contract_state } + val current_state = { bank: bank, result: new_result, contract_state: contract_state } val new_state = process_message(current_state, env_val, CONTRACT_ADDRESS, submsg, reply) all { bank' = new_state.bank, - return' = new_state.return, + result' = new_state.result, contract_state' = new_state.contract_state, advance_time, } @@ -139,3 +162,295 @@ module oaksecurity_cosmwasm_ctf_01 { } } + + +mbt: +mbt_oaksecurity_cosmwasm_ctf_01.rs: + +pub mod state_structs { + use num_bigint::BigInt; + use serde::Deserialize; + use std::collections::HashMap; + use itf::de::{self, As}; + + #[derive(Clone, Debug, Deserialize)] + pub struct InstantiateMsg { + pub count: BigInt + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Lockup { + pub id: BigInt, + pub owner: String, + pub amount: BigInt, + pub release_timestamp: BigInt + } + + #[derive(Clone, Debug, Deserialize)] + pub struct ContractState { + pub last_id: BigInt, + pub lockups: HashMap + } + + #[derive(Clone, Debug, Deserialize)] + pub struct NondetPicks { + + #[serde(with = "As::>")] + pub sender: Option, + + #[serde(with = "As::>")] + pub denom: Option, + + #[serde(with = "As::>")] + pub amount: Option, + + #[serde(with = "As::>")] + pub message_ids: Option> + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Message {} + #[derive(Clone, Debug, Deserialize)] + pub struct Attribute { + pub key: String, + pub value: QuintSerializedValue, + } + + #[derive(Clone, Debug, Deserialize)] + #[serde(tag = "tag", content = "value")] + pub enum QuintSerializedValue { + FromInt(BigInt), + FromStr(String), + FromListInt(Vec), + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Response { + pub messages: Vec, + pub attributes: Vec, + } + + #[derive(Clone, Debug, Deserialize)] + pub struct State { + pub contract_state: ContractState, + pub bank: HashMap>, + #[serde(with = "As::>")] + pub result: Result, + pub action_taken: String, + pub nondet_picks: NondetPicks, + pub time: BigInt, + } + +} + +#[cfg(test)] +pub mod tests { + use oaksecurity_cosmwasm_ctf_01::contract; + use oaksecurity_cosmwasm_ctf_01::msg::{ExecuteMsg, InstantiateMsg}; + + + use crate::state_structs::*; + use cosmwasm_std::{coin, Addr, Uint128}; + use cw_multi_test::{App, AppResponse, ContractWrapper, Executor}; + use itf::trace_from_str; + use num_bigint::BigInt; + use num_traits::{ToPrimitive, Zero}; + + pub const DENOM: &str = "uawesome"; + pub const TICK: u64 = 1; + + pub fn mint_tokens(mut app: App, recipient: String, denom: String, amount: Uint128) -> App { + app.sudo(cw_multi_test::SudoMsg::Bank( + cw_multi_test::BankSudo::Mint { + to_address: recipient.to_owned(), + amount: vec![coin(amount.u128(), denom)], + }, + )) + .unwrap(); + app + } + + fn compare_state(test_state: &TestState, app: &App, state: &State) { + // compare contract balances + let balance = app + .wrap() + .query_balance(&test_state.contract_addr, DENOM) + .unwrap() + .amount; + let trace_balance = state + .bank + .get(&test_state.contract_addr.to_string()) + .and_then(|x| x.get(DENOM)) + .and_then(|x| x.to_u128()) + .unwrap_or(0); + println!( + "Contract balance ({:?}) for {DENOM}: {:?} vs {:?}", + test_state.contract_addr, + balance, + Uint128::new(trace_balance) + ); + assert_eq!(balance, Uint128::new(trace_balance)); + + // TODO: Query the contract and compare the state as you wish + } + + fn compare_result( + trace_result: Result, + app_result: Result, + ) { + if trace_result.is_ok() { + assert!( + app_result.is_ok(), + "Action unexpectedly failed, error: {:?}", + app_result.err() + ); + println!("Action successful as expected"); + } else { + assert!( + app_result.is_err(), + "Expected action to fail with error: {:?}", + trace_result.err() + ); + println!("Action failed as expected"); + } + } + + fn funds_from_trace(amount: Option, denom: Option) -> Vec { + if amount.is_none() || denom.is_none() || amount == Some(Zero::zero()) { + return vec![]; + } + + vec![coin( + amount.as_ref().unwrap().to_u128().unwrap(), + denom.unwrap(), + )] + } + + // Testing is stateful. + struct TestState { + // we will only know the contract address once we have processed an `instantiate` step + pub contract_addr: Addr, + } + + #[test] + fn model_test() { + let mut app = App::default(); + let code = ContractWrapper::new(contract::execute, contract::instantiate, contract::query); + let code_id = app.store_code(Box::new(code)); + + // create test state + let mut test_state = TestState { + contract_addr: Addr::unchecked("contract0"), + }; + + // load trace data + let data = include_str!("../quint/test.itf.json"); + let trace: itf::Trace = trace_from_str(data).unwrap(); + + for s in trace.states { + let last_result = s.value.result.clone(); + if last_result.is_ok() && !last_result.unwrap().messages.is_empty() { + println!("Processing messages, skipping"); + continue; + } + + let action_taken = &s.value.action_taken; + let nondet_picks = &s.value.nondet_picks; + let amount = nondet_picks.amount.clone(); + let denom = nondet_picks.denom.clone(); + let sender = nondet_picks.sender.clone(); + + println!("Step number: {:?}", s.meta.index); + println!("Result from trace: {:?}", s.value.result.clone()); + + match action_taken.as_str() { + + + "deposit_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = ExecuteMsg::Deposit { }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "q::init" => { + println!("Initializing contract."); + + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = InstantiateMsg { count: 0 }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + test_state.contract_addr = app.instantiate_contract( + code_id, + sender, + &msg, + &funds, + "test", + None, + ).unwrap(); + + for (addr, coins) in s.value.bank.clone().iter() { + for (denom, amount) in coins.iter() { + app = mint_tokens( + app, + addr.clone(), + denom.to_string(), + Uint128::new(amount.to_u128().unwrap()), + ); + } + } + + } + + + "withdraw_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let message_ids = nondet_picks.message_ids.clone().unwrap().iter().map(|x| x.to_u64().unwrap().into()).collect(); + let msg = ExecuteMsg::Withdraw { ids: message_ids }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + _ => panic!("Invalid action taken"), + } + compare_state(&test_state, &app, &(s.value.clone())); + println!( + "clock is advancing for {} seconds", + TICK + ); + app.update_block(|block| { + block.time = block.time.plus_seconds(TICK); + }); + println!("-----------------------------------"); + } + } +} diff --git a/tests/snapshots/integration_tests__ctf02.snap b/tests/snapshots/integration_tests__ctf02.snap index 12af37e..88f4efe 100644 --- a/tests/snapshots/integration_tests__ctf02.snap +++ b/tests/snapshots/integration_tests__ctf02.snap @@ -2,24 +2,29 @@ source: tests/integration_tests.rs expression: output --- +quint: + + +oaksecurity_cosmwasm_ctf_02_stubs.qnt: module oaksecurity_cosmwasm_ctf_02 { - import basicSpells.* from "../lib/basicSpells" - import cw_types.* from "../lib/cw_types" - import messaging.* from "../lib/messaging" - import bank from "../lib/bank" + import basicSpells.* from "./lib/basicSpells" + import cw_types.* from "./lib/cw_types" + import cw_utils.* from "./lib/cw_utils" + import messaging.* from "./lib/messaging" + import bank from "./lib/bank" var contract_state: ContractState - var return: Result + var result: Result var bank: bank::Bank var time: int - pure val CONTRACT_ADDRESS = "" + pure val CONTRACT_ADDRESS = "contract0" - pure val ADDRESSES = Set("s1", "s2", "s3", CONTRACT_ADDRESS) + pure val ADDRESSES = Set("sender1", "sender2", "sender3", CONTRACT_ADDRESS) pure val DENOMS = Set("d1", "uawesome") pure val MAX_AMOUNT = 200 @@ -31,14 +36,22 @@ module oaksecurity_cosmwasm_ctf_02 { | ExecuteMsg_Withdraw({ amount: int }) | ExecuteMsg_Stake({ lock_amount: int }) | ExecuteMsg_Unstake({ unlock_amount: int }) - pure def instantiate(state: ContractState, _env: Env, _info: MessageInfo, _msg: InstantiateMsg): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + pure def instantiate(state: ContractState, _env: Env, _info: MessageInfo, _msg: InstantiateMsg): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } + pure def execute(state: ContractState, env: Env, info: MessageInfo, msg: ExecuteMsg): (Result[Response, ContractError], ContractState) = match msg { | ExecuteMsg_Deposit(__r) => deposit(state, info) | ExecuteMsg_Withdraw(__r) => withdraw(state, info, __r.amount) | ExecuteMsg_Stake(__r) => stake(state, env, info, __r.lock_amount) | ExecuteMsg_Unstake(__r) => unstake(state, env, info, __r.unlock_amount) } - pure def deposit(state: ContractState, info: MessageInfo): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def deposit(state: ContractState, info: MessageInfo): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action deposit_action = { // TODO: Change next line according to fund expectations @@ -47,7 +60,11 @@ module oaksecurity_cosmwasm_ctf_02 { pure val message: ExecuteMsg = ExecuteMsg_Deposit execute_message(message, max_funds) } - pure def withdraw(state: ContractState, info: MessageInfo, amount: int): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def withdraw(state: ContractState, info: MessageInfo, amount: int): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action withdraw_action = { // TODO: Change next line according to fund expectations @@ -56,7 +73,11 @@ module oaksecurity_cosmwasm_ctf_02 { pure val message: ExecuteMsg = ExecuteMsg_Withdraw({ amount: message_amount }) execute_message(message, max_funds) } - pure def stake(state: ContractState, env: Env, info: MessageInfo, lock_amount: int): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def stake(state: ContractState, env: Env, info: MessageInfo, lock_amount: int): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action stake_action = { // TODO: Change next line according to fund expectations @@ -65,7 +86,11 @@ module oaksecurity_cosmwasm_ctf_02 { pure val message: ExecuteMsg = ExecuteMsg_Stake({ lock_amount: message_lock_amount }) execute_message(message, max_funds) } - pure def unstake(state: ContractState, env: Env, info: MessageInfo, unlock_amount: int): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def unstake(state: ContractState, env: Env, info: MessageInfo, unlock_amount: int): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action unstake_action = { // TODO: Change next line according to fund expectations @@ -82,7 +107,7 @@ module oaksecurity_cosmwasm_ctf_02 { } pure val init_contract_state = { - voting_power: Map() + voting_power: Map() } action execute_step = all { @@ -95,20 +120,32 @@ module oaksecurity_cosmwasm_ctf_02 { advance_time, } - pure def reply(state: ContractState, _env: Env, _reply: Reply): (Result, ContractState) = (Ok(Response_new), state) - pure val init_bank_state = ADDRESSES.mapBy(_ => DENOMS.mapBy(_ => MAX_AMOUNT)) val env_val = { block: { time: time } } - action init = all { - contract_state' = init_contract_state, - bank' = init_bank_state, - return' = Err("No previous request"), - time' = 0, + action init = { + // TODO: Change next line according to fund expectations + pure val max_funds = 0 + + nondet sender = Set("admin").oneOf() + nondet denom = DENOMS.oneOf() + nondet amount = 0.to(max_funds).oneOf() + val funds = [{ denom: denom, amount: amount }] + val info = { sender: sender, funds: funds } + + pure val message: InstantiateMsg = { } + pure val r = instantiate(init_contract_state, { block: { time: 0 } }, info, message) + + all { + contract_state' = r._2, + bank' = init_bank_state, + result' = r._1, + time' = 0, + } } @@ -122,9 +159,12 @@ module oaksecurity_cosmwasm_ctf_02 { val r = execute(contract_state, env_val, info, message) all { bank.get(sender).get(denom) >= amount, - bank' = bank.setBy(sender, balances => balances.setBy(denom, balance => balance - amount)) - .setBy(CONTRACT_ADDRESS, balances => balances.setBy(denom, balance => balance + amount)), - return' = r._1, + match r._1 { + | Ok(_) => bank' = bank.setBy(sender, balances => balances.setBy(denom, balance => balance - amount)) + .setBy(CONTRACT_ADDRESS, balances => balances.setBy(denom, balance => balance + amount)) + | Err(_) => bank' = bank + }, + result' = r._1, contract_state' = r._2, } } @@ -132,16 +172,16 @@ module oaksecurity_cosmwasm_ctf_02 { action advance_time = time' = time + 1 action step = { - val message_getting = get_message(return) - val new_return = message_getting._1 + val message_getting = get_message(result) + val new_result = message_getting._1 val opt_message = message_getting._2 match opt_message { | Some(submsg) => { - val current_state = { bank: bank, return: new_return, contract_state: contract_state } + val current_state = { bank: bank, result: new_result, contract_state: contract_state } val new_state = process_message(current_state, env_val, CONTRACT_ADDRESS, submsg, reply) all { bank' = new_state.bank, - return' = new_state.return, + result' = new_state.result, contract_state' = new_state.contract_state, advance_time, } @@ -151,3 +191,341 @@ module oaksecurity_cosmwasm_ctf_02 { } } + + +mbt: +mbt_oaksecurity_cosmwasm_ctf_02.rs: + +pub mod state_structs { + use num_bigint::BigInt; + use serde::Deserialize; + use std::collections::HashMap; + use itf::de::{self, As}; + + #[derive(Clone, Debug, Deserialize)] + pub struct InstantiateMsg { + + } + + #[derive(Clone, Debug, Deserialize)] + pub struct UserInfo { + pub total_tokens: BigInt, + pub voting_power: BigInt, + pub released_time: BigInt + } + + #[derive(Clone, Debug, Deserialize)] + pub struct ContractState { + pub voting_power: HashMap + } + + #[derive(Clone, Debug, Deserialize)] + pub struct NondetPicks { + + #[serde(with = "As::>")] + pub sender: Option, + + #[serde(with = "As::>")] + pub denom: Option, + + #[serde(with = "As::>")] + pub amount: Option, + + #[serde(with = "As::>")] + pub message_amount: Option, + + #[serde(with = "As::>")] + pub message_lock_amount: Option, + + #[serde(with = "As::>")] + pub message_unlock_amount: Option + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Message {} + #[derive(Clone, Debug, Deserialize)] + pub struct Attribute { + pub key: String, + pub value: QuintSerializedValue, + } + + #[derive(Clone, Debug, Deserialize)] + #[serde(tag = "tag", content = "value")] + pub enum QuintSerializedValue { + FromInt(BigInt), + FromStr(String), + FromListInt(Vec), + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Response { + pub messages: Vec, + pub attributes: Vec, + } + + #[derive(Clone, Debug, Deserialize)] + pub struct State { + pub contract_state: ContractState, + pub bank: HashMap>, + #[serde(with = "As::>")] + pub result: Result, + pub action_taken: String, + pub nondet_picks: NondetPicks, + pub time: BigInt, + } + +} + +#[cfg(test)] +pub mod tests { + use oaksecurity_cosmwasm_ctf_02::contract; + use oaksecurity_cosmwasm_ctf_02::msg::{ExecuteMsg, InstantiateMsg}; + + + use crate::state_structs::*; + use cosmwasm_std::{coin, Addr, Uint128}; + use cw_multi_test::{App, AppResponse, ContractWrapper, Executor}; + use itf::trace_from_str; + use num_bigint::BigInt; + use num_traits::{ToPrimitive, Zero}; + + pub const DENOM: &str = "uawesome"; + pub const TICK: u64 = 1; + + pub fn mint_tokens(mut app: App, recipient: String, denom: String, amount: Uint128) -> App { + app.sudo(cw_multi_test::SudoMsg::Bank( + cw_multi_test::BankSudo::Mint { + to_address: recipient.to_owned(), + amount: vec![coin(amount.u128(), denom)], + }, + )) + .unwrap(); + app + } + + fn compare_state(test_state: &TestState, app: &App, state: &State) { + // compare contract balances + let balance = app + .wrap() + .query_balance(&test_state.contract_addr, DENOM) + .unwrap() + .amount; + let trace_balance = state + .bank + .get(&test_state.contract_addr.to_string()) + .and_then(|x| x.get(DENOM)) + .and_then(|x| x.to_u128()) + .unwrap_or(0); + println!( + "Contract balance ({:?}) for {DENOM}: {:?} vs {:?}", + test_state.contract_addr, + balance, + Uint128::new(trace_balance) + ); + assert_eq!(balance, Uint128::new(trace_balance)); + + // TODO: Query the contract and compare the state as you wish + } + + fn compare_result( + trace_result: Result, + app_result: Result, + ) { + if trace_result.is_ok() { + assert!( + app_result.is_ok(), + "Action unexpectedly failed, error: {:?}", + app_result.err() + ); + println!("Action successful as expected"); + } else { + assert!( + app_result.is_err(), + "Expected action to fail with error: {:?}", + trace_result.err() + ); + println!("Action failed as expected"); + } + } + + fn funds_from_trace(amount: Option, denom: Option) -> Vec { + if amount.is_none() || denom.is_none() || amount == Some(Zero::zero()) { + return vec![]; + } + + vec![coin( + amount.as_ref().unwrap().to_u128().unwrap(), + denom.unwrap(), + )] + } + + // Testing is stateful. + struct TestState { + // we will only know the contract address once we have processed an `instantiate` step + pub contract_addr: Addr, + } + + #[test] + fn model_test() { + let mut app = App::default(); + let code = ContractWrapper::new(contract::execute, contract::instantiate, contract::query); + let code_id = app.store_code(Box::new(code)); + + // create test state + let mut test_state = TestState { + contract_addr: Addr::unchecked("contract0"), + }; + + // load trace data + let data = include_str!("../quint/test.itf.json"); + let trace: itf::Trace = trace_from_str(data).unwrap(); + + for s in trace.states { + let last_result = s.value.result.clone(); + if last_result.is_ok() && !last_result.unwrap().messages.is_empty() { + println!("Processing messages, skipping"); + continue; + } + + let action_taken = &s.value.action_taken; + let nondet_picks = &s.value.nondet_picks; + let amount = nondet_picks.amount.clone(); + let denom = nondet_picks.denom.clone(); + let sender = nondet_picks.sender.clone(); + + println!("Step number: {:?}", s.meta.index); + println!("Result from trace: {:?}", s.value.result.clone()); + + match action_taken.as_str() { + + + "deposit_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = ExecuteMsg::Deposit { }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "q::init" => { + println!("Initializing contract."); + + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = InstantiateMsg { }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + test_state.contract_addr = app.instantiate_contract( + code_id, + sender, + &msg, + &funds, + "test", + None, + ).unwrap(); + + for (addr, coins) in s.value.bank.clone().iter() { + for (denom, amount) in coins.iter() { + app = mint_tokens( + app, + addr.clone(), + denom.to_string(), + Uint128::new(amount.to_u128().unwrap()), + ); + } + } + + } + + + "stake_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let message_lock_amount = nondet_picks.message_lock_amount.clone().unwrap().to_u64().unwrap().into(); + let msg = ExecuteMsg::Stake { lock_amount: message_lock_amount }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "unstake_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let message_unlock_amount = nondet_picks.message_unlock_amount.clone().unwrap().to_u64().unwrap().into(); + let msg = ExecuteMsg::Unstake { unlock_amount: message_unlock_amount }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "withdraw_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let message_amount = nondet_picks.message_amount.clone().unwrap().to_u64().unwrap().into(); + let msg = ExecuteMsg::Withdraw { amount: message_amount }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + _ => panic!("Invalid action taken"), + } + compare_state(&test_state, &app, &(s.value.clone())); + println!( + "clock is advancing for {} seconds", + TICK + ); + app.update_block(|block| { + block.time = block.time.plus_seconds(TICK); + }); + println!("-----------------------------------"); + } + } +} diff --git a/tests/snapshots/integration_tests__ctf03.snap b/tests/snapshots/integration_tests__ctf03.snap index a76fdb1..696818a 100644 --- a/tests/snapshots/integration_tests__ctf03.snap +++ b/tests/snapshots/integration_tests__ctf03.snap @@ -2,29 +2,36 @@ source: tests/integration_tests.rs expression: output --- +quint: +flash_loan_stubs.qnt: module flash_loan { - import basicSpells.* from "../lib/basicSpells" - import cw_types.* from "../lib/cw_types" - import messaging.* from "../lib/messaging" - import bank from "../lib/bank" + import basicSpells.* from "./lib/basicSpells" + import cw_types.* from "./lib/cw_types" + import cw_utils.* from "./lib/cw_utils" + import messaging.* from "./lib/messaging" + import bank from "./lib/bank" var contract_state: ContractState - var return: Result + var result: Result var bank: bank::Bank var time: int - pure val CONTRACT_ADDRESS = "" + pure val CONTRACT_ADDRESS = "contract0" - pure val ADDRESSES = Set("s1", "s2", "s3", CONTRACT_ADDRESS) + pure val ADDRESSES = Set("sender1", "sender2", "sender3", CONTRACT_ADDRESS) pure val DENOMS = Set("d1", "uawesome") pure val MAX_AMOUNT = 200 - pure def instantiate(state: ContractState, _env: Env, info: MessageInfo, _msg: InstantiateMsg): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + pure def instantiate(state: ContractState, _env: Env, info: MessageInfo, _msg: InstantiateMsg): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } + pure def execute(state: ContractState, env: Env, info: MessageInfo, msg: ExecuteMsg): (Result[Response, ContractError], ContractState) = match msg { | ExecuteMsg_FlashLoan(__r) => flash_loan(state, env, info) | ExecuteMsg_SettleLoan(__r) => settle_loan(state, env, info) @@ -32,7 +39,11 @@ module flash_loan { | ExecuteMsg_WithdrawFunds(__r) => withdraw_funds(state, env, info, __r.recipient) | ExecuteMsg_TransferOwner(__r) => transfer_owner(state, info, __r.new_owner) } - pure def flash_loan(state: ContractState, env: Env, info: MessageInfo): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def flash_loan(state: ContractState, env: Env, info: MessageInfo): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action flash_loan_action = { // TODO: Change next line according to fund expectations @@ -41,7 +52,11 @@ module flash_loan { pure val message: UnknownType = ConstructorForflash_loan execute_message(message, max_funds) } - pure def settle_loan(state: ContractState, env: Env, info: MessageInfo): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def settle_loan(state: ContractState, env: Env, info: MessageInfo): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action settle_loan_action = { // TODO: Change next line according to fund expectations @@ -50,7 +65,11 @@ module flash_loan { pure val message: UnknownType = ConstructorForsettle_loan execute_message(message, max_funds) } - pure def set_proxy_addr(state: ContractState, info: MessageInfo, proxy_addr: str): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def set_proxy_addr(state: ContractState, info: MessageInfo, proxy_addr: str): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action set_proxy_addr_action = { // TODO: Change next line according to fund expectations @@ -59,7 +78,11 @@ module flash_loan { pure val message: UnknownType = ConstructorForset_proxy_addr execute_message(message, max_funds) } - pure def withdraw_funds(state: ContractState, env: Env, info: MessageInfo, recipient: Addr): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def withdraw_funds(state: ContractState, env: Env, info: MessageInfo, recipient: Addr): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action withdraw_funds_action = { // TODO: Change next line according to fund expectations @@ -68,7 +91,11 @@ module flash_loan { pure val message: UnknownType = ConstructorForwithdraw_funds execute_message(message, max_funds) } - pure def transfer_owner(state: ContractState, info: MessageInfo, new_owner: Addr): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def transfer_owner(state: ContractState, info: MessageInfo, new_owner: Addr): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action transfer_owner_action = { // TODO: Change next line according to fund expectations @@ -82,11 +109,11 @@ module flash_loan { type ContractState = { config: Config, - flash_loan: FlashLoanState + flash_loan: FlashLoanState } pure val init_contract_state = { - config: , + config: , flash_loan: } @@ -101,20 +128,32 @@ module flash_loan { advance_time, } - pure def reply(state: ContractState, _env: Env, _reply: Reply): (Result, ContractState) = (Ok(Response_new), state) - pure val init_bank_state = ADDRESSES.mapBy(_ => DENOMS.mapBy(_ => MAX_AMOUNT)) val env_val = { block: { time: time } } - action init = all { - contract_state' = init_contract_state, - bank' = init_bank_state, - return' = Err("No previous request"), - time' = 0, + action init = { + // TODO: Change next line according to fund expectations + pure val max_funds = 0 + + nondet sender = Set("admin").oneOf() + nondet denom = DENOMS.oneOf() + nondet amount = 0.to(max_funds).oneOf() + val funds = [{ denom: denom, amount: amount }] + val info = { sender: sender, funds: funds } + + pure val message: InstantiateMsg = + pure val r = instantiate(init_contract_state, { block: { time: 0 } }, info, message) + + all { + contract_state' = r._2, + bank' = init_bank_state, + result' = r._1, + time' = 0, + } } @@ -128,9 +167,12 @@ module flash_loan { val r = execute(contract_state, env_val, info, message) all { bank.get(sender).get(denom) >= amount, - bank' = bank.setBy(sender, balances => balances.setBy(denom, balance => balance - amount)) - .setBy(CONTRACT_ADDRESS, balances => balances.setBy(denom, balance => balance + amount)), - return' = r._1, + match r._1 { + | Ok(_) => bank' = bank.setBy(sender, balances => balances.setBy(denom, balance => balance - amount)) + .setBy(CONTRACT_ADDRESS, balances => balances.setBy(denom, balance => balance + amount)) + | Err(_) => bank' = bank + }, + result' = r._1, contract_state' = r._2, } } @@ -138,16 +180,16 @@ module flash_loan { action advance_time = time' = time + 1 action step = { - val message_getting = get_message(return) - val new_return = message_getting._1 + val message_getting = get_message(result) + val new_result = message_getting._1 val opt_message = message_getting._2 match opt_message { | Some(submsg) => { - val current_state = { bank: bank, return: new_return, contract_state: contract_state } + val current_state = { bank: bank, result: new_result, contract_state: contract_state } val new_state = process_message(current_state, env_val, CONTRACT_ADDRESS, submsg, reply) all { bank' = new_state.bank, - return' = new_state.return, + result' = new_state.result, contract_state' = new_state.contract_state, advance_time, } @@ -157,33 +199,47 @@ module flash_loan { } } + + + + +mock_arb_stubs.qnt: module mock_arb { - import basicSpells.* from "../lib/basicSpells" - import cw_types.* from "../lib/cw_types" - import messaging.* from "../lib/messaging" - import bank from "../lib/bank" + import basicSpells.* from "./lib/basicSpells" + import cw_types.* from "./lib/cw_types" + import cw_utils.* from "./lib/cw_utils" + import messaging.* from "./lib/messaging" + import bank from "./lib/bank" var contract_state: ContractState - var return: Result + var result: Result var bank: bank::Bank var time: int - pure val CONTRACT_ADDRESS = "" + pure val CONTRACT_ADDRESS = "contract0" - pure val ADDRESSES = Set("s1", "s2", "s3", CONTRACT_ADDRESS) + pure val ADDRESSES = Set("sender1", "sender2", "sender3", CONTRACT_ADDRESS) pure val DENOMS = Set("d1", "uawesome") pure val MAX_AMOUNT = 200 - pure def instantiate(state: ContractState, _env: Env, _info: MessageInfo, _msg: InstantiateMsg): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + pure def instantiate(state: ContractState, _env: Env, _info: MessageInfo, _msg: InstantiateMsg): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } + pure def execute(state: ContractState, env: Env, info: MessageInfo, msg: ExecuteMsg): (Result[Response, ContractError], ContractState) = match msg { | ExecuteMsg_Arbitrage(__r) => arbitrage(state, env, info, __r.recipient) } - pure def arbitrage(state: ContractState, env: Env, info: MessageInfo, recipient: Addr): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def arbitrage(state: ContractState, env: Env, info: MessageInfo, recipient: Addr): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action arbitrage_action = { // TODO: Change next line according to fund expectations @@ -199,7 +255,7 @@ module mock_arb { } pure val init_contract_state = { - config: + config: } action execute_step = all { @@ -209,20 +265,32 @@ module mock_arb { advance_time, } - pure def reply(state: ContractState, _env: Env, _reply: Reply): (Result, ContractState) = (Ok(Response_new), state) - pure val init_bank_state = ADDRESSES.mapBy(_ => DENOMS.mapBy(_ => MAX_AMOUNT)) val env_val = { block: { time: time } } - action init = all { - contract_state' = init_contract_state, - bank' = init_bank_state, - return' = Err("No previous request"), - time' = 0, + action init = { + // TODO: Change next line according to fund expectations + pure val max_funds = 0 + + nondet sender = Set("admin").oneOf() + nondet denom = DENOMS.oneOf() + nondet amount = 0.to(max_funds).oneOf() + val funds = [{ denom: denom, amount: amount }] + val info = { sender: sender, funds: funds } + + pure val message: InstantiateMsg = + pure val r = instantiate(init_contract_state, { block: { time: 0 } }, info, message) + + all { + contract_state' = r._2, + bank' = init_bank_state, + result' = r._1, + time' = 0, + } } @@ -236,9 +304,12 @@ module mock_arb { val r = execute(contract_state, env_val, info, message) all { bank.get(sender).get(denom) >= amount, - bank' = bank.setBy(sender, balances => balances.setBy(denom, balance => balance - amount)) - .setBy(CONTRACT_ADDRESS, balances => balances.setBy(denom, balance => balance + amount)), - return' = r._1, + match r._1 { + | Ok(_) => bank' = bank.setBy(sender, balances => balances.setBy(denom, balance => balance - amount)) + .setBy(CONTRACT_ADDRESS, balances => balances.setBy(denom, balance => balance + amount)) + | Err(_) => bank' = bank + }, + result' = r._1, contract_state' = r._2, } } @@ -246,16 +317,16 @@ module mock_arb { action advance_time = time' = time + 1 action step = { - val message_getting = get_message(return) - val new_return = message_getting._1 + val message_getting = get_message(result) + val new_result = message_getting._1 val opt_message = message_getting._2 match opt_message { | Some(submsg) => { - val current_state = { bank: bank, return: new_return, contract_state: contract_state } + val current_state = { bank: bank, result: new_result, contract_state: contract_state } val new_state = process_message(current_state, env_val, CONTRACT_ADDRESS, submsg, reply) all { bank' = new_state.bank, - return' = new_state.return, + result' = new_state.result, contract_state' = new_state.contract_state, advance_time, } @@ -265,33 +336,45 @@ module mock_arb { } } + + +proxy_stubs.qnt: module proxy { - import basicSpells.* from "../lib/basicSpells" - import cw_types.* from "../lib/cw_types" - import messaging.* from "../lib/messaging" - import bank from "../lib/bank" + import basicSpells.* from "./lib/basicSpells" + import cw_types.* from "./lib/cw_types" + import cw_utils.* from "./lib/cw_utils" + import messaging.* from "./lib/messaging" + import bank from "./lib/bank" var contract_state: ContractState - var return: Result + var result: Result var bank: bank::Bank var time: int - pure val CONTRACT_ADDRESS = "" + pure val CONTRACT_ADDRESS = "contract0" - pure val ADDRESSES = Set("s1", "s2", "s3", CONTRACT_ADDRESS) + pure val ADDRESSES = Set("sender1", "sender2", "sender3", CONTRACT_ADDRESS) pure val DENOMS = Set("d1", "uawesome") pure val MAX_AMOUNT = 200 - pure def instantiate(state: ContractState, _env: Env, _info: MessageInfo, msg: InstantiateMsg): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + pure def instantiate(state: ContractState, _env: Env, _info: MessageInfo, msg: InstantiateMsg): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } + pure def execute(state: ContractState, env: Env, info: MessageInfo, msg: ExecuteMsg): (Result[Response, ContractError], ContractState) = match msg { | ExecuteMsg_RequestFlashLoan(__r) => request_flash_loan(state, env, info, __r.recipient, __r.msg) } - pure def request_flash_loan(state: ContractState, env: Env, _info: MessageInfo, recipient: Addr, msg: Binary): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def request_flash_loan(state: ContractState, env: Env, _info: MessageInfo, recipient: Addr, msg: Binary): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action request_flash_loan_action = { // TODO: Change next line according to fund expectations @@ -307,7 +390,7 @@ module proxy { } pure val init_contract_state = { - config: + config: } action execute_step = all { @@ -317,20 +400,32 @@ module proxy { advance_time, } - pure def reply(state: ContractState, _env: Env, _reply: Reply): (Result, ContractState) = (Ok(Response_new), state) - pure val init_bank_state = ADDRESSES.mapBy(_ => DENOMS.mapBy(_ => MAX_AMOUNT)) val env_val = { block: { time: time } } - action init = all { - contract_state' = init_contract_state, - bank' = init_bank_state, - return' = Err("No previous request"), - time' = 0, + action init = { + // TODO: Change next line according to fund expectations + pure val max_funds = 0 + + nondet sender = Set("admin").oneOf() + nondet denom = DENOMS.oneOf() + nondet amount = 0.to(max_funds).oneOf() + val funds = [{ denom: denom, amount: amount }] + val info = { sender: sender, funds: funds } + + pure val message: InstantiateMsg = + pure val r = instantiate(init_contract_state, { block: { time: 0 } }, info, message) + + all { + contract_state' = r._2, + bank' = init_bank_state, + result' = r._1, + time' = 0, + } } @@ -344,9 +439,12 @@ module proxy { val r = execute(contract_state, env_val, info, message) all { bank.get(sender).get(denom) >= amount, - bank' = bank.setBy(sender, balances => balances.setBy(denom, balance => balance - amount)) - .setBy(CONTRACT_ADDRESS, balances => balances.setBy(denom, balance => balance + amount)), - return' = r._1, + match r._1 { + | Ok(_) => bank' = bank.setBy(sender, balances => balances.setBy(denom, balance => balance - amount)) + .setBy(CONTRACT_ADDRESS, balances => balances.setBy(denom, balance => balance + amount)) + | Err(_) => bank' = bank + }, + result' = r._1, contract_state' = r._2, } } @@ -354,16 +452,16 @@ module proxy { action advance_time = time' = time + 1 action step = { - val message_getting = get_message(return) - val new_return = message_getting._1 + val message_getting = get_message(result) + val new_result = message_getting._1 val opt_message = message_getting._2 match opt_message { | Some(submsg) => { - val current_state = { bank: bank, return: new_return, contract_state: contract_state } + val current_state = { bank: bank, result: new_result, contract_state: contract_state } val new_state = process_message(current_state, env_val, CONTRACT_ADDRESS, submsg, reply) all { bank' = new_state.bank, - return' = new_state.return, + result' = new_state.result, contract_state' = new_state.contract_state, advance_time, } @@ -373,3 +471,847 @@ module proxy { } } + + +mbt: +mbt_flash_loan.rs: + +pub mod state_structs { + use num_bigint::BigInt; + use serde::Deserialize; + use std::collections::HashMap; + use itf::de::{self, As}; + + + #[derive(Clone, Debug, Deserialize)] + pub struct ContractState { + pub config: Config, + pub flash_loan: FlashLoanState + } + + #[derive(Clone, Debug, Deserialize)] + pub struct NondetPicks { + + #[serde(with = "As::>")] + pub sender: Option, + + #[serde(with = "As::>")] + pub denom: Option, + + #[serde(with = "As::>")] + pub amount: Option + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Message {} + #[derive(Clone, Debug, Deserialize)] + pub struct Attribute { + pub key: String, + pub value: QuintSerializedValue, + } + + #[derive(Clone, Debug, Deserialize)] + #[serde(tag = "tag", content = "value")] + pub enum QuintSerializedValue { + FromInt(BigInt), + FromStr(String), + FromListInt(Vec), + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Response { + pub messages: Vec, + pub attributes: Vec, + } + + #[derive(Clone, Debug, Deserialize)] + pub struct State { + pub contract_state: ContractState, + pub bank: HashMap>, + #[serde(with = "As::>")] + pub result: Result, + pub action_taken: String, + pub nondet_picks: NondetPicks, + pub time: BigInt, + } + +} + +#[cfg(test)] +pub mod tests { + use flash_loan::contract; + use flash_loan::msg::{ExecuteMsg, InstantiateMsg}; + + + use crate::state_structs::*; + use cosmwasm_std::{coin, Addr, Uint128}; + use cw_multi_test::{App, AppResponse, ContractWrapper, Executor}; + use itf::trace_from_str; + use num_bigint::BigInt; + use num_traits::{ToPrimitive, Zero}; + + pub const DENOM: &str = "uawesome"; + pub const TICK: u64 = 1; + + pub fn mint_tokens(mut app: App, recipient: String, denom: String, amount: Uint128) -> App { + app.sudo(cw_multi_test::SudoMsg::Bank( + cw_multi_test::BankSudo::Mint { + to_address: recipient.to_owned(), + amount: vec![coin(amount.u128(), denom)], + }, + )) + .unwrap(); + app + } + + fn compare_state(test_state: &TestState, app: &App, state: &State) { + // compare contract balances + let balance = app + .wrap() + .query_balance(&test_state.contract_addr, DENOM) + .unwrap() + .amount; + let trace_balance = state + .bank + .get(&test_state.contract_addr.to_string()) + .and_then(|x| x.get(DENOM)) + .and_then(|x| x.to_u128()) + .unwrap_or(0); + println!( + "Contract balance ({:?}) for {DENOM}: {:?} vs {:?}", + test_state.contract_addr, + balance, + Uint128::new(trace_balance) + ); + assert_eq!(balance, Uint128::new(trace_balance)); + + // TODO: Query the contract and compare the state as you wish + } + + fn compare_result( + trace_result: Result, + app_result: Result, + ) { + if trace_result.is_ok() { + assert!( + app_result.is_ok(), + "Action unexpectedly failed, error: {:?}", + app_result.err() + ); + println!("Action successful as expected"); + } else { + assert!( + app_result.is_err(), + "Expected action to fail with error: {:?}", + trace_result.err() + ); + println!("Action failed as expected"); + } + } + + fn funds_from_trace(amount: Option, denom: Option) -> Vec { + if amount.is_none() || denom.is_none() || amount == Some(Zero::zero()) { + return vec![]; + } + + vec![coin( + amount.as_ref().unwrap().to_u128().unwrap(), + denom.unwrap(), + )] + } + + // Testing is stateful. + struct TestState { + // we will only know the contract address once we have processed an `instantiate` step + pub contract_addr: Addr, + } + + #[test] + fn model_test() { + let mut app = App::default(); + let code = ContractWrapper::new(contract::execute, contract::instantiate, contract::query); + let code_id = app.store_code(Box::new(code)); + + // create test state + let mut test_state = TestState { + contract_addr: Addr::unchecked("contract0"), + }; + + // load trace data + let data = include_str!("../quint/test.itf.json"); + let trace: itf::Trace = trace_from_str(data).unwrap(); + + for s in trace.states { + let last_result = s.value.result.clone(); + if last_result.is_ok() && !last_result.unwrap().messages.is_empty() { + println!("Processing messages, skipping"); + continue; + } + + let action_taken = &s.value.action_taken; + let nondet_picks = &s.value.nondet_picks; + let amount = nondet_picks.amount.clone(); + let denom = nondet_picks.denom.clone(); + let sender = nondet_picks.sender.clone(); + + println!("Step number: {:?}", s.meta.index); + println!("Result from trace: {:?}", s.value.result.clone()); + + match action_taken.as_str() { + + + "flash_loan_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = ConstructorForExecuteMsg::FlashLoan { }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "q::init" => { + println!("Initializing contract."); + + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = InstantiateMsg { }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + test_state.contract_addr = app.instantiate_contract( + code_id, + sender, + &msg, + &funds, + "test", + None, + ).unwrap(); + + for (addr, coins) in s.value.bank.clone().iter() { + for (denom, amount) in coins.iter() { + app = mint_tokens( + app, + addr.clone(), + denom.to_string(), + Uint128::new(amount.to_u128().unwrap()), + ); + } + } + + } + + + "set_proxy_addr_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = ConstructorForExecuteMsg::SetProxyAddr { }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "settle_loan_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = ConstructorForExecuteMsg::SettleLoan { }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "transfer_owner_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = ConstructorForExecuteMsg::TransferOwner { }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "withdraw_funds_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = ConstructorForExecuteMsg::WithdrawFunds { }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + _ => panic!("Invalid action taken"), + } + compare_state(&test_state, &app, &(s.value.clone())); + println!( + "clock is advancing for {} seconds", + TICK + ); + app.update_block(|block| { + block.time = block.time.plus_seconds(TICK); + }); + println!("-----------------------------------"); + } + } +} + + +mbt_mock_arb.rs: + +pub mod state_structs { + use num_bigint::BigInt; + use serde::Deserialize; + use std::collections::HashMap; + use itf::de::{self, As}; + + + #[derive(Clone, Debug, Deserialize)] + pub struct ContractState { + pub config: Config + } + + #[derive(Clone, Debug, Deserialize)] + pub struct NondetPicks { + + #[serde(with = "As::>")] + pub sender: Option, + + #[serde(with = "As::>")] + pub denom: Option, + + #[serde(with = "As::>")] + pub amount: Option + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Message {} + #[derive(Clone, Debug, Deserialize)] + pub struct Attribute { + pub key: String, + pub value: QuintSerializedValue, + } + + #[derive(Clone, Debug, Deserialize)] + #[serde(tag = "tag", content = "value")] + pub enum QuintSerializedValue { + FromInt(BigInt), + FromStr(String), + FromListInt(Vec), + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Response { + pub messages: Vec, + pub attributes: Vec, + } + + #[derive(Clone, Debug, Deserialize)] + pub struct State { + pub contract_state: ContractState, + pub bank: HashMap>, + #[serde(with = "As::>")] + pub result: Result, + pub action_taken: String, + pub nondet_picks: NondetPicks, + pub time: BigInt, + } + +} + +#[cfg(test)] +pub mod tests { + use mock_arb::contract; + use mock_arb::msg::{ExecuteMsg, InstantiateMsg}; + + + use crate::state_structs::*; + use cosmwasm_std::{coin, Addr, Uint128}; + use cw_multi_test::{App, AppResponse, ContractWrapper, Executor}; + use itf::trace_from_str; + use num_bigint::BigInt; + use num_traits::{ToPrimitive, Zero}; + + pub const DENOM: &str = "uawesome"; + pub const TICK: u64 = 1; + + pub fn mint_tokens(mut app: App, recipient: String, denom: String, amount: Uint128) -> App { + app.sudo(cw_multi_test::SudoMsg::Bank( + cw_multi_test::BankSudo::Mint { + to_address: recipient.to_owned(), + amount: vec![coin(amount.u128(), denom)], + }, + )) + .unwrap(); + app + } + + fn compare_state(test_state: &TestState, app: &App, state: &State) { + // compare contract balances + let balance = app + .wrap() + .query_balance(&test_state.contract_addr, DENOM) + .unwrap() + .amount; + let trace_balance = state + .bank + .get(&test_state.contract_addr.to_string()) + .and_then(|x| x.get(DENOM)) + .and_then(|x| x.to_u128()) + .unwrap_or(0); + println!( + "Contract balance ({:?}) for {DENOM}: {:?} vs {:?}", + test_state.contract_addr, + balance, + Uint128::new(trace_balance) + ); + assert_eq!(balance, Uint128::new(trace_balance)); + + // TODO: Query the contract and compare the state as you wish + } + + fn compare_result( + trace_result: Result, + app_result: Result, + ) { + if trace_result.is_ok() { + assert!( + app_result.is_ok(), + "Action unexpectedly failed, error: {:?}", + app_result.err() + ); + println!("Action successful as expected"); + } else { + assert!( + app_result.is_err(), + "Expected action to fail with error: {:?}", + trace_result.err() + ); + println!("Action failed as expected"); + } + } + + fn funds_from_trace(amount: Option, denom: Option) -> Vec { + if amount.is_none() || denom.is_none() || amount == Some(Zero::zero()) { + return vec![]; + } + + vec![coin( + amount.as_ref().unwrap().to_u128().unwrap(), + denom.unwrap(), + )] + } + + // Testing is stateful. + struct TestState { + // we will only know the contract address once we have processed an `instantiate` step + pub contract_addr: Addr, + } + + #[test] + fn model_test() { + let mut app = App::default(); + let code = ContractWrapper::new(contract::execute, contract::instantiate, contract::query); + let code_id = app.store_code(Box::new(code)); + + // create test state + let mut test_state = TestState { + contract_addr: Addr::unchecked("contract0"), + }; + + // load trace data + let data = include_str!("../quint/test.itf.json"); + let trace: itf::Trace = trace_from_str(data).unwrap(); + + for s in trace.states { + let last_result = s.value.result.clone(); + if last_result.is_ok() && !last_result.unwrap().messages.is_empty() { + println!("Processing messages, skipping"); + continue; + } + + let action_taken = &s.value.action_taken; + let nondet_picks = &s.value.nondet_picks; + let amount = nondet_picks.amount.clone(); + let denom = nondet_picks.denom.clone(); + let sender = nondet_picks.sender.clone(); + + println!("Step number: {:?}", s.meta.index); + println!("Result from trace: {:?}", s.value.result.clone()); + + match action_taken.as_str() { + + + "arbitrage_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = ConstructorForExecuteMsg::Arbitrage { }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "q::init" => { + println!("Initializing contract."); + + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = InstantiateMsg { }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + test_state.contract_addr = app.instantiate_contract( + code_id, + sender, + &msg, + &funds, + "test", + None, + ).unwrap(); + + for (addr, coins) in s.value.bank.clone().iter() { + for (denom, amount) in coins.iter() { + app = mint_tokens( + app, + addr.clone(), + denom.to_string(), + Uint128::new(amount.to_u128().unwrap()), + ); + } + } + + } + + _ => panic!("Invalid action taken"), + } + compare_state(&test_state, &app, &(s.value.clone())); + println!( + "clock is advancing for {} seconds", + TICK + ); + app.update_block(|block| { + block.time = block.time.plus_seconds(TICK); + }); + println!("-----------------------------------"); + } + } +} + + +mbt_proxy.rs: + +pub mod state_structs { + use num_bigint::BigInt; + use serde::Deserialize; + use std::collections::HashMap; + use itf::de::{self, As}; + + + #[derive(Clone, Debug, Deserialize)] + pub struct ContractState { + pub config: Config + } + + #[derive(Clone, Debug, Deserialize)] + pub struct NondetPicks { + + #[serde(with = "As::>")] + pub sender: Option, + + #[serde(with = "As::>")] + pub denom: Option, + + #[serde(with = "As::>")] + pub amount: Option + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Message {} + #[derive(Clone, Debug, Deserialize)] + pub struct Attribute { + pub key: String, + pub value: QuintSerializedValue, + } + + #[derive(Clone, Debug, Deserialize)] + #[serde(tag = "tag", content = "value")] + pub enum QuintSerializedValue { + FromInt(BigInt), + FromStr(String), + FromListInt(Vec), + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Response { + pub messages: Vec, + pub attributes: Vec, + } + + #[derive(Clone, Debug, Deserialize)] + pub struct State { + pub contract_state: ContractState, + pub bank: HashMap>, + #[serde(with = "As::>")] + pub result: Result, + pub action_taken: String, + pub nondet_picks: NondetPicks, + pub time: BigInt, + } + +} + +#[cfg(test)] +pub mod tests { + use proxy::contract; + use proxy::msg::{ExecuteMsg, InstantiateMsg}; + + + use crate::state_structs::*; + use cosmwasm_std::{coin, Addr, Uint128}; + use cw_multi_test::{App, AppResponse, ContractWrapper, Executor}; + use itf::trace_from_str; + use num_bigint::BigInt; + use num_traits::{ToPrimitive, Zero}; + + pub const DENOM: &str = "uawesome"; + pub const TICK: u64 = 1; + + pub fn mint_tokens(mut app: App, recipient: String, denom: String, amount: Uint128) -> App { + app.sudo(cw_multi_test::SudoMsg::Bank( + cw_multi_test::BankSudo::Mint { + to_address: recipient.to_owned(), + amount: vec![coin(amount.u128(), denom)], + }, + )) + .unwrap(); + app + } + + fn compare_state(test_state: &TestState, app: &App, state: &State) { + // compare contract balances + let balance = app + .wrap() + .query_balance(&test_state.contract_addr, DENOM) + .unwrap() + .amount; + let trace_balance = state + .bank + .get(&test_state.contract_addr.to_string()) + .and_then(|x| x.get(DENOM)) + .and_then(|x| x.to_u128()) + .unwrap_or(0); + println!( + "Contract balance ({:?}) for {DENOM}: {:?} vs {:?}", + test_state.contract_addr, + balance, + Uint128::new(trace_balance) + ); + assert_eq!(balance, Uint128::new(trace_balance)); + + // TODO: Query the contract and compare the state as you wish + } + + fn compare_result( + trace_result: Result, + app_result: Result, + ) { + if trace_result.is_ok() { + assert!( + app_result.is_ok(), + "Action unexpectedly failed, error: {:?}", + app_result.err() + ); + println!("Action successful as expected"); + } else { + assert!( + app_result.is_err(), + "Expected action to fail with error: {:?}", + trace_result.err() + ); + println!("Action failed as expected"); + } + } + + fn funds_from_trace(amount: Option, denom: Option) -> Vec { + if amount.is_none() || denom.is_none() || amount == Some(Zero::zero()) { + return vec![]; + } + + vec![coin( + amount.as_ref().unwrap().to_u128().unwrap(), + denom.unwrap(), + )] + } + + // Testing is stateful. + struct TestState { + // we will only know the contract address once we have processed an `instantiate` step + pub contract_addr: Addr, + } + + #[test] + fn model_test() { + let mut app = App::default(); + let code = ContractWrapper::new(contract::execute, contract::instantiate, contract::query); + let code_id = app.store_code(Box::new(code)); + + // create test state + let mut test_state = TestState { + contract_addr: Addr::unchecked("contract0"), + }; + + // load trace data + let data = include_str!("../quint/test.itf.json"); + let trace: itf::Trace = trace_from_str(data).unwrap(); + + for s in trace.states { + let last_result = s.value.result.clone(); + if last_result.is_ok() && !last_result.unwrap().messages.is_empty() { + println!("Processing messages, skipping"); + continue; + } + + let action_taken = &s.value.action_taken; + let nondet_picks = &s.value.nondet_picks; + let amount = nondet_picks.amount.clone(); + let denom = nondet_picks.denom.clone(); + let sender = nondet_picks.sender.clone(); + + println!("Step number: {:?}", s.meta.index); + println!("Result from trace: {:?}", s.value.result.clone()); + + match action_taken.as_str() { + + + "q::init" => { + println!("Initializing contract."); + + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = InstantiateMsg { }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + test_state.contract_addr = app.instantiate_contract( + code_id, + sender, + &msg, + &funds, + "test", + None, + ).unwrap(); + + for (addr, coins) in s.value.bank.clone().iter() { + for (denom, amount) in coins.iter() { + app = mint_tokens( + app, + addr.clone(), + denom.to_string(), + Uint128::new(amount.to_u128().unwrap()), + ); + } + } + + } + + + "request_flash_loan_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = ConstructorForExecuteMsg::RequestFlashLoan { }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + _ => panic!("Invalid action taken"), + } + compare_state(&test_state, &app, &(s.value.clone())); + println!( + "clock is advancing for {} seconds", + TICK + ); + app.update_block(|block| { + block.time = block.time.plus_seconds(TICK); + }); + println!("-----------------------------------"); + } + } +} diff --git a/tests/snapshots/integration_tests__ctf04.snap b/tests/snapshots/integration_tests__ctf04.snap index c267c88..438f2cb 100644 --- a/tests/snapshots/integration_tests__ctf04.snap +++ b/tests/snapshots/integration_tests__ctf04.snap @@ -2,24 +2,29 @@ source: tests/integration_tests.rs expression: output --- +quint: + + +oaksecurity_cosmwasm_ctf_04_stubs.qnt: module oaksecurity_cosmwasm_ctf_04 { - import basicSpells.* from "../lib/basicSpells" - import cw_types.* from "../lib/cw_types" - import messaging.* from "../lib/messaging" - import bank from "../lib/bank" + import basicSpells.* from "./lib/basicSpells" + import cw_types.* from "./lib/cw_types" + import cw_utils.* from "./lib/cw_utils" + import messaging.* from "./lib/messaging" + import bank from "./lib/bank" var contract_state: ContractState - var return: Result + var result: Result var bank: bank::Bank var time: int - pure val CONTRACT_ADDRESS = "" + pure val CONTRACT_ADDRESS = "contract0" - pure val ADDRESSES = Set("s1", "s2", "s3", CONTRACT_ADDRESS) + pure val ADDRESSES = Set("sender1", "sender2", "sender3", CONTRACT_ADDRESS) pure val DENOMS = Set("d1", "uawesome") pure val MAX_AMOUNT = 200 @@ -30,12 +35,20 @@ module oaksecurity_cosmwasm_ctf_04 { type ExecuteMsg = | ExecuteMsg_Mint | ExecuteMsg_Burn({ shares: int }) - pure def instantiate(state: ContractState, _env: Env, _info: MessageInfo, _msg: InstantiateMsg): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + pure def instantiate(state: ContractState, _env: Env, _info: MessageInfo, _msg: InstantiateMsg): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } + pure def execute(state: ContractState, env: Env, info: MessageInfo, msg: ExecuteMsg): (Result[Response, ContractError], ContractState) = match msg { | ExecuteMsg_Mint(__r) => mint(state, env, info) | ExecuteMsg_Burn(__r) => burn(state, env, info, __r.shares) } - pure def mint(state: ContractState, env: Env, info: MessageInfo): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def mint(state: ContractState, env: Env, info: MessageInfo): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action mint_action = { // TODO: Change next line according to fund expectations @@ -44,7 +57,11 @@ module oaksecurity_cosmwasm_ctf_04 { pure val message: ExecuteMsg = ExecuteMsg_Mint execute_message(message, max_funds) } - pure def burn(state: ContractState, env: Env, info: MessageInfo, shares: int): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def burn(state: ContractState, env: Env, info: MessageInfo, shares: int): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action burn_action = { // TODO: Change next line according to fund expectations @@ -57,11 +74,11 @@ module oaksecurity_cosmwasm_ctf_04 { type ContractState = { config: Config, - balances: Addr -> Balance + balances: Addr -> Balance } pure val init_contract_state = { - config: { total_supply: 0 }, + config: { total_supply: 0 }, balances: Map() } @@ -73,20 +90,32 @@ module oaksecurity_cosmwasm_ctf_04 { advance_time, } - pure def reply(state: ContractState, _env: Env, _reply: Reply): (Result, ContractState) = (Ok(Response_new), state) - pure val init_bank_state = ADDRESSES.mapBy(_ => DENOMS.mapBy(_ => MAX_AMOUNT)) val env_val = { block: { time: time } } - action init = all { - contract_state' = init_contract_state, - bank' = init_bank_state, - return' = Err("No previous request"), - time' = 0, + action init = { + // TODO: Change next line according to fund expectations + pure val max_funds = 0 + + nondet sender = Set("admin").oneOf() + nondet denom = DENOMS.oneOf() + nondet amount = 0.to(max_funds).oneOf() + val funds = [{ denom: denom, amount: amount }] + val info = { sender: sender, funds: funds } + + pure val message: InstantiateMsg = { offset: 0 } + pure val r = instantiate(init_contract_state, { block: { time: 0 } }, info, message) + + all { + contract_state' = r._2, + bank' = init_bank_state, + result' = r._1, + time' = 0, + } } @@ -100,9 +129,12 @@ module oaksecurity_cosmwasm_ctf_04 { val r = execute(contract_state, env_val, info, message) all { bank.get(sender).get(denom) >= amount, - bank' = bank.setBy(sender, balances => balances.setBy(denom, balance => balance - amount)) - .setBy(CONTRACT_ADDRESS, balances => balances.setBy(denom, balance => balance + amount)), - return' = r._1, + match r._1 { + | Ok(_) => bank' = bank.setBy(sender, balances => balances.setBy(denom, balance => balance - amount)) + .setBy(CONTRACT_ADDRESS, balances => balances.setBy(denom, balance => balance + amount)) + | Err(_) => bank' = bank + }, + result' = r._1, contract_state' = r._2, } } @@ -110,16 +142,16 @@ module oaksecurity_cosmwasm_ctf_04 { action advance_time = time' = time + 1 action step = { - val message_getting = get_message(return) - val new_return = message_getting._1 + val message_getting = get_message(result) + val new_result = message_getting._1 val opt_message = message_getting._2 match opt_message { | Some(submsg) => { - val current_state = { bank: bank, return: new_return, contract_state: contract_state } + val current_state = { bank: bank, result: new_result, contract_state: contract_state } val new_state = process_message(current_state, env_val, CONTRACT_ADDRESS, submsg, reply) all { bank' = new_state.bank, - return' = new_state.return, + result' = new_state.result, contract_state' = new_state.contract_state, advance_time, } @@ -129,3 +161,297 @@ module oaksecurity_cosmwasm_ctf_04 { } } + + +mbt: +mbt_oaksecurity_cosmwasm_ctf_04.rs: + +pub mod state_structs { + use num_bigint::BigInt; + use serde::Deserialize; + use std::collections::HashMap; + use itf::de::{self, As}; + + #[derive(Clone, Debug, Deserialize)] + pub struct Balance { + pub amount: BigInt + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Config { + pub total_supply: BigInt + } + + #[derive(Clone, Debug, Deserialize)] + pub struct InstantiateMsg { + pub offset: BigInt + } + + #[derive(Clone, Debug, Deserialize)] + pub struct ContractState { + pub config: Config, + pub balances: HashMap + } + + #[derive(Clone, Debug, Deserialize)] + pub struct NondetPicks { + + #[serde(with = "As::>")] + pub sender: Option, + + #[serde(with = "As::>")] + pub denom: Option, + + #[serde(with = "As::>")] + pub amount: Option, + + #[serde(with = "As::>")] + pub message_shares: Option + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Message {} + #[derive(Clone, Debug, Deserialize)] + pub struct Attribute { + pub key: String, + pub value: QuintSerializedValue, + } + + #[derive(Clone, Debug, Deserialize)] + #[serde(tag = "tag", content = "value")] + pub enum QuintSerializedValue { + FromInt(BigInt), + FromStr(String), + FromListInt(Vec), + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Response { + pub messages: Vec, + pub attributes: Vec, + } + + #[derive(Clone, Debug, Deserialize)] + pub struct State { + pub contract_state: ContractState, + pub bank: HashMap>, + #[serde(with = "As::>")] + pub result: Result, + pub action_taken: String, + pub nondet_picks: NondetPicks, + pub time: BigInt, + } + +} + +#[cfg(test)] +pub mod tests { + use oaksecurity_cosmwasm_ctf_04::contract; + use oaksecurity_cosmwasm_ctf_04::msg::{ExecuteMsg, InstantiateMsg}; + + + use crate::state_structs::*; + use cosmwasm_std::{coin, Addr, Uint128}; + use cw_multi_test::{App, AppResponse, ContractWrapper, Executor}; + use itf::trace_from_str; + use num_bigint::BigInt; + use num_traits::{ToPrimitive, Zero}; + + pub const DENOM: &str = "uawesome"; + pub const TICK: u64 = 1; + + pub fn mint_tokens(mut app: App, recipient: String, denom: String, amount: Uint128) -> App { + app.sudo(cw_multi_test::SudoMsg::Bank( + cw_multi_test::BankSudo::Mint { + to_address: recipient.to_owned(), + amount: vec![coin(amount.u128(), denom)], + }, + )) + .unwrap(); + app + } + + fn compare_state(test_state: &TestState, app: &App, state: &State) { + // compare contract balances + let balance = app + .wrap() + .query_balance(&test_state.contract_addr, DENOM) + .unwrap() + .amount; + let trace_balance = state + .bank + .get(&test_state.contract_addr.to_string()) + .and_then(|x| x.get(DENOM)) + .and_then(|x| x.to_u128()) + .unwrap_or(0); + println!( + "Contract balance ({:?}) for {DENOM}: {:?} vs {:?}", + test_state.contract_addr, + balance, + Uint128::new(trace_balance) + ); + assert_eq!(balance, Uint128::new(trace_balance)); + + // TODO: Query the contract and compare the state as you wish + } + + fn compare_result( + trace_result: Result, + app_result: Result, + ) { + if trace_result.is_ok() { + assert!( + app_result.is_ok(), + "Action unexpectedly failed, error: {:?}", + app_result.err() + ); + println!("Action successful as expected"); + } else { + assert!( + app_result.is_err(), + "Expected action to fail with error: {:?}", + trace_result.err() + ); + println!("Action failed as expected"); + } + } + + fn funds_from_trace(amount: Option, denom: Option) -> Vec { + if amount.is_none() || denom.is_none() || amount == Some(Zero::zero()) { + return vec![]; + } + + vec![coin( + amount.as_ref().unwrap().to_u128().unwrap(), + denom.unwrap(), + )] + } + + // Testing is stateful. + struct TestState { + // we will only know the contract address once we have processed an `instantiate` step + pub contract_addr: Addr, + } + + #[test] + fn model_test() { + let mut app = App::default(); + let code = ContractWrapper::new(contract::execute, contract::instantiate, contract::query); + let code_id = app.store_code(Box::new(code)); + + // create test state + let mut test_state = TestState { + contract_addr: Addr::unchecked("contract0"), + }; + + // load trace data + let data = include_str!("../quint/test.itf.json"); + let trace: itf::Trace = trace_from_str(data).unwrap(); + + for s in trace.states { + let last_result = s.value.result.clone(); + if last_result.is_ok() && !last_result.unwrap().messages.is_empty() { + println!("Processing messages, skipping"); + continue; + } + + let action_taken = &s.value.action_taken; + let nondet_picks = &s.value.nondet_picks; + let amount = nondet_picks.amount.clone(); + let denom = nondet_picks.denom.clone(); + let sender = nondet_picks.sender.clone(); + + println!("Step number: {:?}", s.meta.index); + println!("Result from trace: {:?}", s.value.result.clone()); + + match action_taken.as_str() { + + + "burn_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let message_shares = nondet_picks.message_shares.clone().unwrap().to_u64().unwrap().into(); + let msg = ExecuteMsg::Burn { shares: message_shares }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "q::init" => { + println!("Initializing contract."); + + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = InstantiateMsg { offset: 0 }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + test_state.contract_addr = app.instantiate_contract( + code_id, + sender, + &msg, + &funds, + "test", + None, + ).unwrap(); + + for (addr, coins) in s.value.bank.clone().iter() { + for (denom, amount) in coins.iter() { + app = mint_tokens( + app, + addr.clone(), + denom.to_string(), + Uint128::new(amount.to_u128().unwrap()), + ); + } + } + + } + + + "mint_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = ExecuteMsg::Mint { }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + _ => panic!("Invalid action taken"), + } + compare_state(&test_state, &app, &(s.value.clone())); + println!( + "clock is advancing for {} seconds", + TICK + ); + app.update_block(|block| { + block.time = block.time.plus_seconds(TICK); + }); + println!("-----------------------------------"); + } + } +} diff --git a/tests/snapshots/integration_tests__ctf05.snap b/tests/snapshots/integration_tests__ctf05.snap index c8b271d..c6247ee 100644 --- a/tests/snapshots/integration_tests__ctf05.snap +++ b/tests/snapshots/integration_tests__ctf05.snap @@ -2,24 +2,29 @@ source: tests/integration_tests.rs expression: output --- +quint: + + +oaksecurity_cosmwasm_ctf_05_stubs.qnt: module oaksecurity_cosmwasm_ctf_05 { - import basicSpells.* from "../lib/basicSpells" - import cw_types.* from "../lib/cw_types" - import messaging.* from "../lib/messaging" - import bank from "../lib/bank" + import basicSpells.* from "./lib/basicSpells" + import cw_types.* from "./lib/cw_types" + import cw_utils.* from "./lib/cw_utils" + import messaging.* from "./lib/messaging" + import bank from "./lib/bank" var contract_state: ContractState - var return: Result + var result: Result var bank: bank::Bank var time: int - pure val CONTRACT_ADDRESS = "" + pure val CONTRACT_ADDRESS = "contract0" - pure val ADDRESSES = Set("s1", "s2", "s3", CONTRACT_ADDRESS) + pure val ADDRESSES = Set("sender1", "sender2", "sender3", CONTRACT_ADDRESS) pure val DENOMS = Set("d1", "uawesome") pure val MAX_AMOUNT = 200 @@ -33,7 +38,11 @@ module oaksecurity_cosmwasm_ctf_05 { | ExecuteMsg_ProposeNewOwner({ new_owner: str }) | ExecuteMsg_AcceptOwnership | ExecuteMsg_DropOwnershipProposal - pure def instantiate(state: ContractState, _env: Env, _info: MessageInfo, msg: InstantiateMsg): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + pure def instantiate(state: ContractState, _env: Env, _info: MessageInfo, msg: InstantiateMsg): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } + pure def execute(state: ContractState, _env: Env, info: MessageInfo, msg: ExecuteMsg): (Result[Response, ContractError], ContractState) = match msg { | ExecuteMsg_Deposit(__r) => deposit(state, info) | ExecuteMsg_Withdraw(__r) => withdraw(state, info, __r.amount) @@ -42,7 +51,11 @@ module oaksecurity_cosmwasm_ctf_05 { | ExecuteMsg_AcceptOwnership(__r) => accept_owner(state, info) | ExecuteMsg_DropOwnershipProposal(__r) => drop_owner(state, info) } - pure def deposit(state: ContractState, info: MessageInfo): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def deposit(state: ContractState, info: MessageInfo): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action deposit_action = { // TODO: Change next line according to fund expectations @@ -51,7 +64,11 @@ module oaksecurity_cosmwasm_ctf_05 { pure val message: ExecuteMsg = ExecuteMsg_Deposit execute_message(message, max_funds) } - pure def withdraw(state: ContractState, info: MessageInfo, amount: int): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def withdraw(state: ContractState, info: MessageInfo, amount: int): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action withdraw_action = { // TODO: Change next line according to fund expectations @@ -60,7 +77,11 @@ module oaksecurity_cosmwasm_ctf_05 { pure val message: ExecuteMsg = ExecuteMsg_Withdraw({ amount: message_amount }) execute_message(message, max_funds) } - pure def owner_action(state: ContractState, info: MessageInfo, msg: CosmosMsg): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def owner_action(state: ContractState, info: MessageInfo, msg: CosmosMsg): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action owner_action_action = { // TODO: Change next line according to fund expectations @@ -69,7 +90,11 @@ module oaksecurity_cosmwasm_ctf_05 { pure val message: ExecuteMsg = ExecuteMsg_OwnerAction({ msg: message_msg }) execute_message(message, max_funds) } - pure def propose_owner(state: ContractState, info: MessageInfo, new_owner: str): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def propose_owner(state: ContractState, info: MessageInfo, new_owner: str): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action propose_owner_action = { // TODO: Change next line according to fund expectations @@ -78,7 +103,11 @@ module oaksecurity_cosmwasm_ctf_05 { pure val message: ExecuteMsg = ExecuteMsg_ProposeNewOwner({ new_owner: message_new_owner }) execute_message(message, max_funds) } - pure def accept_owner(state: ContractState, info: MessageInfo): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def accept_owner(state: ContractState, info: MessageInfo): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action accept_owner_action = { // TODO: Change next line according to fund expectations @@ -87,7 +116,11 @@ module oaksecurity_cosmwasm_ctf_05 { pure val message: ExecuteMsg = ExecuteMsg_AcceptOwnership execute_message(message, max_funds) } - pure def drop_owner(state: ContractState, info: MessageInfo): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def drop_owner(state: ContractState, info: MessageInfo): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action drop_owner_action = { // TODO: Change next line according to fund expectations @@ -101,11 +134,11 @@ module oaksecurity_cosmwasm_ctf_05 { type ContractState = { state: State, - balances: Addr -> int + balances: Addr -> int } pure val init_contract_state = { - state: { current_owner: "s1",proposed_owner: }, + state: { current_owner: "s1",proposed_owner: }, balances: Map() } @@ -121,20 +154,32 @@ module oaksecurity_cosmwasm_ctf_05 { advance_time, } - pure def reply(state: ContractState, _env: Env, _reply: Reply): (Result, ContractState) = (Ok(Response_new), state) - pure val init_bank_state = ADDRESSES.mapBy(_ => DENOMS.mapBy(_ => MAX_AMOUNT)) val env_val = { block: { time: time } } - action init = all { - contract_state' = init_contract_state, - bank' = init_bank_state, - return' = Err("No previous request"), - time' = 0, + action init = { + // TODO: Change next line according to fund expectations + pure val max_funds = 0 + + nondet sender = Set("admin").oneOf() + nondet denom = DENOMS.oneOf() + nondet amount = 0.to(max_funds).oneOf() + val funds = [{ denom: denom, amount: amount }] + val info = { sender: sender, funds: funds } + + pure val message: InstantiateMsg = { owner: "" } + pure val r = instantiate(init_contract_state, { block: { time: 0 } }, info, message) + + all { + contract_state' = r._2, + bank' = init_bank_state, + result' = r._1, + time' = 0, + } } @@ -148,9 +193,12 @@ module oaksecurity_cosmwasm_ctf_05 { val r = execute(contract_state, env_val, info, message) all { bank.get(sender).get(denom) >= amount, - bank' = bank.setBy(sender, balances => balances.setBy(denom, balance => balance - amount)) - .setBy(CONTRACT_ADDRESS, balances => balances.setBy(denom, balance => balance + amount)), - return' = r._1, + match r._1 { + | Ok(_) => bank' = bank.setBy(sender, balances => balances.setBy(denom, balance => balance - amount)) + .setBy(CONTRACT_ADDRESS, balances => balances.setBy(denom, balance => balance + amount)) + | Err(_) => bank' = bank + }, + result' = r._1, contract_state' = r._2, } } @@ -158,16 +206,16 @@ module oaksecurity_cosmwasm_ctf_05 { action advance_time = time' = time + 1 action step = { - val message_getting = get_message(return) - val new_return = message_getting._1 + val message_getting = get_message(result) + val new_result = message_getting._1 val opt_message = message_getting._2 match opt_message { | Some(submsg) => { - val current_state = { bank: bank, return: new_return, contract_state: contract_state } + val current_state = { bank: bank, result: new_result, contract_state: contract_state } val new_state = process_message(current_state, env_val, CONTRACT_ADDRESS, submsg, reply) all { bank' = new_state.bank, - return' = new_state.return, + result' = new_state.result, contract_state' = new_state.contract_state, advance_time, } @@ -177,3 +225,384 @@ module oaksecurity_cosmwasm_ctf_05 { } } + + +mbt: +mbt_oaksecurity_cosmwasm_ctf_05.rs: + +pub mod state_structs { + use num_bigint::BigInt; + use serde::Deserialize; + use std::collections::HashMap; + use itf::de::{self, As}; + + #[derive(Clone, Debug, Deserialize)] + pub struct InstantiateMsg { + pub owner: String + } + + #[derive(Clone, Debug, Deserialize)] + pub struct State { + pub current_owner: String, + pub proposed_owner: Option[Addr] + } + + #[derive(Clone, Debug, Deserialize)] + pub struct ContractState { + pub state: State, + pub balances: HashMap + } + + #[derive(Clone, Debug, Deserialize)] + pub struct NondetPicks { + + #[serde(with = "As::>")] + pub sender: Option, + + #[serde(with = "As::>")] + pub denom: Option, + + #[serde(with = "As::>")] + pub amount: Option, + + #[serde(with = "As::>")] + pub proposed_owner_element: Option, + + #[serde(with = "As::>")] + pub message_amount: Option, + + #[serde(with = "As::>")] + pub message_msg: Option, + + #[serde(with = "As::>")] + pub message_new_owner: Option + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Message {} + #[derive(Clone, Debug, Deserialize)] + pub struct Attribute { + pub key: String, + pub value: QuintSerializedValue, + } + + #[derive(Clone, Debug, Deserialize)] + #[serde(tag = "tag", content = "value")] + pub enum QuintSerializedValue { + FromInt(BigInt), + FromStr(String), + FromListInt(Vec), + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Response { + pub messages: Vec, + pub attributes: Vec, + } + + #[derive(Clone, Debug, Deserialize)] + pub struct State { + pub contract_state: ContractState, + pub bank: HashMap>, + #[serde(with = "As::>")] + pub result: Result, + pub action_taken: String, + pub nondet_picks: NondetPicks, + pub time: BigInt, + } + +} + +#[cfg(test)] +pub mod tests { + use oaksecurity_cosmwasm_ctf_05::contract; + use oaksecurity_cosmwasm_ctf_05::msg::{ExecuteMsg, InstantiateMsg}; + + + use crate::state_structs::*; + use cosmwasm_std::{coin, Addr, Uint128}; + use cw_multi_test::{App, AppResponse, ContractWrapper, Executor}; + use itf::trace_from_str; + use num_bigint::BigInt; + use num_traits::{ToPrimitive, Zero}; + + pub const DENOM: &str = "uawesome"; + pub const TICK: u64 = 1; + + pub fn mint_tokens(mut app: App, recipient: String, denom: String, amount: Uint128) -> App { + app.sudo(cw_multi_test::SudoMsg::Bank( + cw_multi_test::BankSudo::Mint { + to_address: recipient.to_owned(), + amount: vec![coin(amount.u128(), denom)], + }, + )) + .unwrap(); + app + } + + fn compare_state(test_state: &TestState, app: &App, state: &State) { + // compare contract balances + let balance = app + .wrap() + .query_balance(&test_state.contract_addr, DENOM) + .unwrap() + .amount; + let trace_balance = state + .bank + .get(&test_state.contract_addr.to_string()) + .and_then(|x| x.get(DENOM)) + .and_then(|x| x.to_u128()) + .unwrap_or(0); + println!( + "Contract balance ({:?}) for {DENOM}: {:?} vs {:?}", + test_state.contract_addr, + balance, + Uint128::new(trace_balance) + ); + assert_eq!(balance, Uint128::new(trace_balance)); + + // TODO: Query the contract and compare the state as you wish + } + + fn compare_result( + trace_result: Result, + app_result: Result, + ) { + if trace_result.is_ok() { + assert!( + app_result.is_ok(), + "Action unexpectedly failed, error: {:?}", + app_result.err() + ); + println!("Action successful as expected"); + } else { + assert!( + app_result.is_err(), + "Expected action to fail with error: {:?}", + trace_result.err() + ); + println!("Action failed as expected"); + } + } + + fn funds_from_trace(amount: Option, denom: Option) -> Vec { + if amount.is_none() || denom.is_none() || amount == Some(Zero::zero()) { + return vec![]; + } + + vec![coin( + amount.as_ref().unwrap().to_u128().unwrap(), + denom.unwrap(), + )] + } + + // Testing is stateful. + struct TestState { + // we will only know the contract address once we have processed an `instantiate` step + pub contract_addr: Addr, + } + + #[test] + fn model_test() { + let mut app = App::default(); + let code = ContractWrapper::new(contract::execute, contract::instantiate, contract::query); + let code_id = app.store_code(Box::new(code)); + + // create test state + let mut test_state = TestState { + contract_addr: Addr::unchecked("contract0"), + }; + + // load trace data + let data = include_str!("../quint/test.itf.json"); + let trace: itf::Trace = trace_from_str(data).unwrap(); + + for s in trace.states { + let last_result = s.value.result.clone(); + if last_result.is_ok() && !last_result.unwrap().messages.is_empty() { + println!("Processing messages, skipping"); + continue; + } + + let action_taken = &s.value.action_taken; + let nondet_picks = &s.value.nondet_picks; + let amount = nondet_picks.amount.clone(); + let denom = nondet_picks.denom.clone(); + let sender = nondet_picks.sender.clone(); + + println!("Step number: {:?}", s.meta.index); + println!("Result from trace: {:?}", s.value.result.clone()); + + match action_taken.as_str() { + + + "accept_owner_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = ExecuteMsg::AcceptOwnership { }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "deposit_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = ExecuteMsg::Deposit { }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "drop_owner_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = ExecuteMsg::DropOwnershipProposal { }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "q::init" => { + println!("Initializing contract."); + + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = InstantiateMsg { owner: "" }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + test_state.contract_addr = app.instantiate_contract( + code_id, + sender, + &msg, + &funds, + "test", + None, + ).unwrap(); + + for (addr, coins) in s.value.bank.clone().iter() { + for (denom, amount) in coins.iter() { + app = mint_tokens( + app, + addr.clone(), + denom.to_string(), + Uint128::new(amount.to_u128().unwrap()), + ); + } + } + + } + + + "owner_action_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let message_msg = nondet_picks.message_msg.clone().unwrap(); + let msg = ExecuteMsg::OwnerAction { msg: message_msg }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "propose_owner_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let message_new_owner = nondet_picks.message_new_owner.clone().unwrap(); + let msg = ExecuteMsg::ProposeNewOwner { new_owner: message_new_owner }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "withdraw_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let message_amount = nondet_picks.message_amount.clone().unwrap().to_u64().unwrap().into(); + let msg = ExecuteMsg::Withdraw { amount: message_amount }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + _ => panic!("Invalid action taken"), + } + compare_state(&test_state, &app, &(s.value.clone())); + println!( + "clock is advancing for {} seconds", + TICK + ); + app.update_block(|block| { + block.time = block.time.plus_seconds(TICK); + }); + println!("-----------------------------------"); + } + } +} diff --git a/tests/snapshots/integration_tests__ctf06.snap b/tests/snapshots/integration_tests__ctf06.snap index 7518a5a..5cef446 100644 --- a/tests/snapshots/integration_tests__ctf06.snap +++ b/tests/snapshots/integration_tests__ctf06.snap @@ -2,24 +2,29 @@ source: tests/integration_tests.rs expression: output --- +quint: + + +oaksecurity_cosmwasm_ctf_06_stubs.qnt: module oaksecurity_cosmwasm_ctf_06 { - import basicSpells.* from "../lib/basicSpells" - import cw_types.* from "../lib/cw_types" - import messaging.* from "../lib/messaging" - import bank from "../lib/bank" + import basicSpells.* from "./lib/basicSpells" + import cw_types.* from "./lib/cw_types" + import cw_utils.* from "./lib/cw_utils" + import messaging.* from "./lib/messaging" + import bank from "./lib/bank" var contract_state: ContractState - var return: Result + var result: Result var bank: bank::Bank var time: int - pure val CONTRACT_ADDRESS = "" + pure val CONTRACT_ADDRESS = "contract0" - pure val ADDRESSES = Set("s1", "s2", "s3", CONTRACT_ADDRESS) + pure val ADDRESSES = Set("sender1", "sender2", "sender3", CONTRACT_ADDRESS) pure val DENOMS = Set("d1", "uawesome") pure val MAX_AMOUNT = 200 @@ -34,14 +39,22 @@ module oaksecurity_cosmwasm_ctf_06 { | ExecuteMsg_Receive(Cw20ReceiveMsg) type Cw20HookMsg = | Cw20HookMsg_CastVote - pure def instantiate(state: ContractState, _env: Env, _info: MessageInfo, msg: InstantiateMsg): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + pure def instantiate(state: ContractState, _env: Env, _info: MessageInfo, msg: InstantiateMsg): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } + pure def execute(state: ContractState, env: Env, info: MessageInfo, msg: ExecuteMsg): (Result[Response, ContractError], ContractState) = match msg { | ExecuteMsg_Propose(__r) => propose(state, env, info) | ExecuteMsg_ResolveProposal(__r) => resolve_proposal(state, env, info) | ExecuteMsg_OwnerAction(__r) => owner_action(state, info, __r.action) | ExecuteMsg_Receive(msg) => receive_cw20(state, env, info, msg) } - pure def receive_cw20(state: ContractState, env: Env, info: MessageInfo, cw20_msg: Cw20ReceiveMsg): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def receive_cw20(state: ContractState, env: Env, info: MessageInfo, cw20_msg: Cw20ReceiveMsg): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action receive_cw20_action = { // TODO: Change next line according to fund expectations @@ -50,7 +63,11 @@ module oaksecurity_cosmwasm_ctf_06 { pure val message: ExecuteMsg = ExecuteMsg_Receive execute_message(message, max_funds) } - pure def propose(state: ContractState, env: Env, info: MessageInfo): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def propose(state: ContractState, env: Env, info: MessageInfo): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action propose_action = { // TODO: Change next line according to fund expectations @@ -59,7 +76,11 @@ module oaksecurity_cosmwasm_ctf_06 { pure val message: ExecuteMsg = ExecuteMsg_Propose execute_message(message, max_funds) } - pure def resolve_proposal(state: ContractState, env: Env, _info: MessageInfo): (Result[Response, ContractError], ContractState) = (Ok(response), state) + + pure def resolve_proposal(state: ContractState, env: Env, _info: MessageInfo): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(response), state) + } action resolve_proposal_action = { // TODO: Change next line according to fund expectations @@ -68,7 +89,11 @@ module oaksecurity_cosmwasm_ctf_06 { pure val message: ExecuteMsg = ExecuteMsg_ResolveProposal execute_message(message, max_funds) } - pure def owner_action(state: ContractState, info: MessageInfo, msg: CosmosMsg): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def owner_action(state: ContractState, info: MessageInfo, msg: CosmosMsg): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action owner_action_action = { // TODO: Change next line according to fund expectations @@ -81,11 +106,11 @@ module oaksecurity_cosmwasm_ctf_06 { type ContractState = { config: Config, - proposal: Proposal + proposal: Proposal } pure val init_contract_state = { - config: { voting_window: 0,voting_token: "s1",owner: "s1" }, + config: { voting_window: 0,voting_token: "s1",owner: "s1" }, proposal: { proposer: "s1",timestamp: 0 } } @@ -99,20 +124,32 @@ module oaksecurity_cosmwasm_ctf_06 { advance_time, } - pure def reply(state: ContractState, _env: Env, _reply: Reply): (Result, ContractState) = (Ok(Response_new), state) - pure val init_bank_state = ADDRESSES.mapBy(_ => DENOMS.mapBy(_ => MAX_AMOUNT)) val env_val = { block: { time: time } } - action init = all { - contract_state' = init_contract_state, - bank' = init_bank_state, - return' = Err("No previous request"), - time' = 0, + action init = { + // TODO: Change next line according to fund expectations + pure val max_funds = 0 + + nondet sender = Set("admin").oneOf() + nondet denom = DENOMS.oneOf() + nondet amount = 0.to(max_funds).oneOf() + val funds = [{ denom: denom, amount: amount }] + val info = { sender: sender, funds: funds } + + pure val message: InstantiateMsg = { token: "",owner: "",window: 0 } + pure val r = instantiate(init_contract_state, { block: { time: 0 } }, info, message) + + all { + contract_state' = r._2, + bank' = init_bank_state, + result' = r._1, + time' = 0, + } } @@ -126,9 +163,12 @@ module oaksecurity_cosmwasm_ctf_06 { val r = execute(contract_state, env_val, info, message) all { bank.get(sender).get(denom) >= amount, - bank' = bank.setBy(sender, balances => balances.setBy(denom, balance => balance - amount)) - .setBy(CONTRACT_ADDRESS, balances => balances.setBy(denom, balance => balance + amount)), - return' = r._1, + match r._1 { + | Ok(_) => bank' = bank.setBy(sender, balances => balances.setBy(denom, balance => balance - amount)) + .setBy(CONTRACT_ADDRESS, balances => balances.setBy(denom, balance => balance + amount)) + | Err(_) => bank' = bank + }, + result' = r._1, contract_state' = r._2, } } @@ -136,16 +176,16 @@ module oaksecurity_cosmwasm_ctf_06 { action advance_time = time' = time + 1 action step = { - val message_getting = get_message(return) - val new_return = message_getting._1 + val message_getting = get_message(result) + val new_result = message_getting._1 val opt_message = message_getting._2 match opt_message { | Some(submsg) => { - val current_state = { bank: bank, return: new_return, contract_state: contract_state } + val current_state = { bank: bank, result: new_result, contract_state: contract_state } val new_state = process_message(current_state, env_val, CONTRACT_ADDRESS, submsg, reply) all { bank' = new_state.bank, - return' = new_state.return, + result' = new_state.result, contract_state' = new_state.contract_state, advance_time, } @@ -155,3 +195,342 @@ module oaksecurity_cosmwasm_ctf_06 { } } + + +mbt: +mbt_oaksecurity_cosmwasm_ctf_06.rs: + +pub mod state_structs { + use num_bigint::BigInt; + use serde::Deserialize; + use std::collections::HashMap; + use itf::de::{self, As}; + + #[derive(Clone, Debug, Deserialize)] + pub struct Config { + pub voting_window: BigInt, + pub voting_token: String, + pub owner: String + } + + #[derive(Clone, Debug, Deserialize)] + pub struct InstantiateMsg { + pub token: String, + pub owner: String, + pub window: BigInt + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Proposal { + pub proposer: String, + pub timestamp: BigInt + } + + #[derive(Clone, Debug, Deserialize)] + pub struct ContractState { + pub config: Config, + pub proposal: Proposal + } + + #[derive(Clone, Debug, Deserialize)] + pub struct NondetPicks { + + #[serde(with = "As::>")] + pub sender: Option, + + #[serde(with = "As::>")] + pub denom: Option, + + #[serde(with = "As::>")] + pub amount: Option, + + #[serde(with = "As::>")] + pub message_action: Option + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Message {} + #[derive(Clone, Debug, Deserialize)] + pub struct Attribute { + pub key: String, + pub value: QuintSerializedValue, + } + + #[derive(Clone, Debug, Deserialize)] + #[serde(tag = "tag", content = "value")] + pub enum QuintSerializedValue { + FromInt(BigInt), + FromStr(String), + FromListInt(Vec), + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Response { + pub messages: Vec, + pub attributes: Vec, + } + + #[derive(Clone, Debug, Deserialize)] + pub struct State { + pub contract_state: ContractState, + pub bank: HashMap>, + #[serde(with = "As::>")] + pub result: Result, + pub action_taken: String, + pub nondet_picks: NondetPicks, + pub time: BigInt, + } + +} + +#[cfg(test)] +pub mod tests { + use oaksecurity_cosmwasm_ctf_06::contract; + use oaksecurity_cosmwasm_ctf_06::msg::{ExecuteMsg, InstantiateMsg}; + + + use crate::state_structs::*; + use cosmwasm_std::{coin, Addr, Uint128}; + use cw_multi_test::{App, AppResponse, ContractWrapper, Executor}; + use itf::trace_from_str; + use num_bigint::BigInt; + use num_traits::{ToPrimitive, Zero}; + + pub const DENOM: &str = "uawesome"; + pub const TICK: u64 = 1; + + pub fn mint_tokens(mut app: App, recipient: String, denom: String, amount: Uint128) -> App { + app.sudo(cw_multi_test::SudoMsg::Bank( + cw_multi_test::BankSudo::Mint { + to_address: recipient.to_owned(), + amount: vec![coin(amount.u128(), denom)], + }, + )) + .unwrap(); + app + } + + fn compare_state(test_state: &TestState, app: &App, state: &State) { + // compare contract balances + let balance = app + .wrap() + .query_balance(&test_state.contract_addr, DENOM) + .unwrap() + .amount; + let trace_balance = state + .bank + .get(&test_state.contract_addr.to_string()) + .and_then(|x| x.get(DENOM)) + .and_then(|x| x.to_u128()) + .unwrap_or(0); + println!( + "Contract balance ({:?}) for {DENOM}: {:?} vs {:?}", + test_state.contract_addr, + balance, + Uint128::new(trace_balance) + ); + assert_eq!(balance, Uint128::new(trace_balance)); + + // TODO: Query the contract and compare the state as you wish + } + + fn compare_result( + trace_result: Result, + app_result: Result, + ) { + if trace_result.is_ok() { + assert!( + app_result.is_ok(), + "Action unexpectedly failed, error: {:?}", + app_result.err() + ); + println!("Action successful as expected"); + } else { + assert!( + app_result.is_err(), + "Expected action to fail with error: {:?}", + trace_result.err() + ); + println!("Action failed as expected"); + } + } + + fn funds_from_trace(amount: Option, denom: Option) -> Vec { + if amount.is_none() || denom.is_none() || amount == Some(Zero::zero()) { + return vec![]; + } + + vec![coin( + amount.as_ref().unwrap().to_u128().unwrap(), + denom.unwrap(), + )] + } + + // Testing is stateful. + struct TestState { + // we will only know the contract address once we have processed an `instantiate` step + pub contract_addr: Addr, + } + + #[test] + fn model_test() { + let mut app = App::default(); + let code = ContractWrapper::new(contract::execute, contract::instantiate, contract::query); + let code_id = app.store_code(Box::new(code)); + + // create test state + let mut test_state = TestState { + contract_addr: Addr::unchecked("contract0"), + }; + + // load trace data + let data = include_str!("../quint/test.itf.json"); + let trace: itf::Trace = trace_from_str(data).unwrap(); + + for s in trace.states { + let last_result = s.value.result.clone(); + if last_result.is_ok() && !last_result.unwrap().messages.is_empty() { + println!("Processing messages, skipping"); + continue; + } + + let action_taken = &s.value.action_taken; + let nondet_picks = &s.value.nondet_picks; + let amount = nondet_picks.amount.clone(); + let denom = nondet_picks.denom.clone(); + let sender = nondet_picks.sender.clone(); + + println!("Step number: {:?}", s.meta.index); + println!("Result from trace: {:?}", s.value.result.clone()); + + match action_taken.as_str() { + + + "q::init" => { + println!("Initializing contract."); + + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = InstantiateMsg { token: "", owner: "", window: 0 }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + test_state.contract_addr = app.instantiate_contract( + code_id, + sender, + &msg, + &funds, + "test", + None, + ).unwrap(); + + for (addr, coins) in s.value.bank.clone().iter() { + for (denom, amount) in coins.iter() { + app = mint_tokens( + app, + addr.clone(), + denom.to_string(), + Uint128::new(amount.to_u128().unwrap()), + ); + } + } + + } + + + "owner_action_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let message_action = nondet_picks.message_action.clone().unwrap(); + let msg = ExecuteMsg::OwnerAction { action: message_action }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "propose_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = ExecuteMsg::Propose { }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "receive_cw20_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = ExecuteMsg::Receive { }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "resolve_proposal_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = ExecuteMsg::ResolveProposal { }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + _ => panic!("Invalid action taken"), + } + compare_state(&test_state, &app, &(s.value.clone())); + println!( + "clock is advancing for {} seconds", + TICK + ); + app.update_block(|block| { + block.time = block.time.plus_seconds(TICK); + }); + println!("-----------------------------------"); + } + } +} diff --git a/tests/snapshots/integration_tests__ctf07.snap b/tests/snapshots/integration_tests__ctf07.snap index c0e34c2..f4b9bb4 100644 --- a/tests/snapshots/integration_tests__ctf07.snap +++ b/tests/snapshots/integration_tests__ctf07.snap @@ -2,24 +2,29 @@ source: tests/integration_tests.rs expression: output --- +quint: + + +oaksecurity_cosmwasm_ctf_07_stubs.qnt: module oaksecurity_cosmwasm_ctf_07 { - import basicSpells.* from "../lib/basicSpells" - import cw_types.* from "../lib/cw_types" - import messaging.* from "../lib/messaging" - import bank from "../lib/bank" + import basicSpells.* from "./lib/basicSpells" + import cw_types.* from "./lib/cw_types" + import cw_utils.* from "./lib/cw_utils" + import messaging.* from "./lib/messaging" + import bank from "./lib/bank" var contract_state: ContractState - var return: Result + var result: Result var bank: bank::Bank var time: int - pure val CONTRACT_ADDRESS = "" + pure val CONTRACT_ADDRESS = "contract0" - pure val ADDRESSES = Set("s1", "s2", "s3", CONTRACT_ADDRESS) + pure val ADDRESSES = Set("sender1", "sender2", "sender3", CONTRACT_ADDRESS) pure val DENOMS = Set("d1", "uawesome") pure val MAX_AMOUNT = 200 @@ -31,14 +36,22 @@ module oaksecurity_cosmwasm_ctf_07 { | ExecuteMsg_Withdraw({ amount: int }) | ExecuteMsg_OwnerAction({ msg: CosmosMsg }) | ExecuteMsg_UpdateConfig({ new_threshold: int }) - pure def instantiate(state: ContractState, _env: Env, _info: MessageInfo, msg: InstantiateMsg): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + pure def instantiate(state: ContractState, _env: Env, _info: MessageInfo, msg: InstantiateMsg): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } + pure def execute(state: ContractState, _env: Env, info: MessageInfo, msg: ExecuteMsg): (Result[Response, ContractError], ContractState) = match msg { | ExecuteMsg_Deposit(__r) => deposit(state, info) | ExecuteMsg_Withdraw(__r) => withdraw(state, info, __r.amount) | ExecuteMsg_OwnerAction(__r) => owner_action(state, info, __r.msg) | ExecuteMsg_UpdateConfig(__r) => update_config(state, info, __r.new_threshold) } - pure def deposit(state: ContractState, info: MessageInfo): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def deposit(state: ContractState, info: MessageInfo): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action deposit_action = { // TODO: Change next line according to fund expectations @@ -47,7 +60,11 @@ module oaksecurity_cosmwasm_ctf_07 { pure val message: ExecuteMsg = ExecuteMsg_Deposit execute_message(message, max_funds) } - pure def withdraw(state: ContractState, info: MessageInfo, amount: int): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def withdraw(state: ContractState, info: MessageInfo, amount: int): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action withdraw_action = { // TODO: Change next line according to fund expectations @@ -56,7 +73,11 @@ module oaksecurity_cosmwasm_ctf_07 { pure val message: ExecuteMsg = ExecuteMsg_Withdraw({ amount: message_amount }) execute_message(message, max_funds) } - pure def update_config(state: ContractState, info: MessageInfo, new_threshold: int): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def update_config(state: ContractState, info: MessageInfo, new_threshold: int): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action update_config_action = { // TODO: Change next line according to fund expectations @@ -65,7 +86,11 @@ module oaksecurity_cosmwasm_ctf_07 { pure val message: ExecuteMsg = ExecuteMsg_UpdateConfig({ new_threshold: message_new_threshold }) execute_message(message, max_funds) } - pure def owner_action(state: ContractState, info: MessageInfo, msg: CosmosMsg): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def owner_action(state: ContractState, info: MessageInfo, msg: CosmosMsg): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action owner_action_action = { // TODO: Change next line according to fund expectations @@ -78,13 +103,13 @@ module oaksecurity_cosmwasm_ctf_07 { type ContractState = { top_depositor: Addr, - owner: Addr, - threshold: int, - balances: Addr -> int + owner: Addr, + threshold: int, + balances: Addr -> int } pure val init_contract_state = { - top_depositor: "s1", + top_depositor: "s1", owner: "s1", threshold: 0, balances: Map() @@ -100,20 +125,32 @@ module oaksecurity_cosmwasm_ctf_07 { advance_time, } - pure def reply(state: ContractState, _env: Env, _reply: Reply): (Result, ContractState) = (Ok(Response_new), state) - pure val init_bank_state = ADDRESSES.mapBy(_ => DENOMS.mapBy(_ => MAX_AMOUNT)) val env_val = { block: { time: time } } - action init = all { - contract_state' = init_contract_state, - bank' = init_bank_state, - return' = Err("No previous request"), - time' = 0, + action init = { + // TODO: Change next line according to fund expectations + pure val max_funds = 0 + + nondet sender = Set("admin").oneOf() + nondet denom = DENOMS.oneOf() + nondet amount = 0.to(max_funds).oneOf() + val funds = [{ denom: denom, amount: amount }] + val info = { sender: sender, funds: funds } + + pure val message: InstantiateMsg = { owner: "",threshold: 0 } + pure val r = instantiate(init_contract_state, { block: { time: 0 } }, info, message) + + all { + contract_state' = r._2, + bank' = init_bank_state, + result' = r._1, + time' = 0, + } } @@ -127,9 +164,12 @@ module oaksecurity_cosmwasm_ctf_07 { val r = execute(contract_state, env_val, info, message) all { bank.get(sender).get(denom) >= amount, - bank' = bank.setBy(sender, balances => balances.setBy(denom, balance => balance - amount)) - .setBy(CONTRACT_ADDRESS, balances => balances.setBy(denom, balance => balance + amount)), - return' = r._1, + match r._1 { + | Ok(_) => bank' = bank.setBy(sender, balances => balances.setBy(denom, balance => balance - amount)) + .setBy(CONTRACT_ADDRESS, balances => balances.setBy(denom, balance => balance + amount)) + | Err(_) => bank' = bank + }, + result' = r._1, contract_state' = r._2, } } @@ -137,16 +177,16 @@ module oaksecurity_cosmwasm_ctf_07 { action advance_time = time' = time + 1 action step = { - val message_getting = get_message(return) - val new_return = message_getting._1 + val message_getting = get_message(result) + val new_result = message_getting._1 val opt_message = message_getting._2 match opt_message { | Some(submsg) => { - val current_state = { bank: bank, return: new_return, contract_state: contract_state } + val current_state = { bank: bank, result: new_result, contract_state: contract_state } val new_state = process_message(current_state, env_val, CONTRACT_ADDRESS, submsg, reply) all { bank' = new_state.bank, - return' = new_state.return, + result' = new_state.result, contract_state' = new_state.contract_state, advance_time, } @@ -156,3 +196,344 @@ module oaksecurity_cosmwasm_ctf_07 { } } + + +mbt: +mbt_oaksecurity_cosmwasm_ctf_07.rs: + +pub mod state_structs { + use num_bigint::BigInt; + use serde::Deserialize; + use std::collections::HashMap; + use itf::de::{self, As}; + + #[derive(Clone, Debug, Deserialize)] + pub struct ConfigQueryResponse { + pub owner: String, + pub threshold: BigInt + } + + #[derive(Clone, Debug, Deserialize)] + pub struct InstantiateMsg { + pub owner: String, + pub threshold: BigInt + } + + #[derive(Clone, Debug, Deserialize)] + pub struct ContractState { + pub top_depositor: String, + pub owner: String, + pub threshold: BigInt, + pub balances: HashMap + } + + #[derive(Clone, Debug, Deserialize)] + pub struct NondetPicks { + + #[serde(with = "As::>")] + pub sender: Option, + + #[serde(with = "As::>")] + pub denom: Option, + + #[serde(with = "As::>")] + pub amount: Option, + + #[serde(with = "As::>")] + pub message_amount: Option, + + #[serde(with = "As::>")] + pub message_new_threshold: Option, + + #[serde(with = "As::>")] + pub message_msg: Option + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Message {} + #[derive(Clone, Debug, Deserialize)] + pub struct Attribute { + pub key: String, + pub value: QuintSerializedValue, + } + + #[derive(Clone, Debug, Deserialize)] + #[serde(tag = "tag", content = "value")] + pub enum QuintSerializedValue { + FromInt(BigInt), + FromStr(String), + FromListInt(Vec), + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Response { + pub messages: Vec, + pub attributes: Vec, + } + + #[derive(Clone, Debug, Deserialize)] + pub struct State { + pub contract_state: ContractState, + pub bank: HashMap>, + #[serde(with = "As::>")] + pub result: Result, + pub action_taken: String, + pub nondet_picks: NondetPicks, + pub time: BigInt, + } + +} + +#[cfg(test)] +pub mod tests { + use oaksecurity_cosmwasm_ctf_07::contract; + use oaksecurity_cosmwasm_ctf_07::msg::{ExecuteMsg, InstantiateMsg}; + + + use crate::state_structs::*; + use cosmwasm_std::{coin, Addr, Uint128}; + use cw_multi_test::{App, AppResponse, ContractWrapper, Executor}; + use itf::trace_from_str; + use num_bigint::BigInt; + use num_traits::{ToPrimitive, Zero}; + + pub const DENOM: &str = "uawesome"; + pub const TICK: u64 = 1; + + pub fn mint_tokens(mut app: App, recipient: String, denom: String, amount: Uint128) -> App { + app.sudo(cw_multi_test::SudoMsg::Bank( + cw_multi_test::BankSudo::Mint { + to_address: recipient.to_owned(), + amount: vec![coin(amount.u128(), denom)], + }, + )) + .unwrap(); + app + } + + fn compare_state(test_state: &TestState, app: &App, state: &State) { + // compare contract balances + let balance = app + .wrap() + .query_balance(&test_state.contract_addr, DENOM) + .unwrap() + .amount; + let trace_balance = state + .bank + .get(&test_state.contract_addr.to_string()) + .and_then(|x| x.get(DENOM)) + .and_then(|x| x.to_u128()) + .unwrap_or(0); + println!( + "Contract balance ({:?}) for {DENOM}: {:?} vs {:?}", + test_state.contract_addr, + balance, + Uint128::new(trace_balance) + ); + assert_eq!(balance, Uint128::new(trace_balance)); + + // TODO: Query the contract and compare the state as you wish + } + + fn compare_result( + trace_result: Result, + app_result: Result, + ) { + if trace_result.is_ok() { + assert!( + app_result.is_ok(), + "Action unexpectedly failed, error: {:?}", + app_result.err() + ); + println!("Action successful as expected"); + } else { + assert!( + app_result.is_err(), + "Expected action to fail with error: {:?}", + trace_result.err() + ); + println!("Action failed as expected"); + } + } + + fn funds_from_trace(amount: Option, denom: Option) -> Vec { + if amount.is_none() || denom.is_none() || amount == Some(Zero::zero()) { + return vec![]; + } + + vec![coin( + amount.as_ref().unwrap().to_u128().unwrap(), + denom.unwrap(), + )] + } + + // Testing is stateful. + struct TestState { + // we will only know the contract address once we have processed an `instantiate` step + pub contract_addr: Addr, + } + + #[test] + fn model_test() { + let mut app = App::default(); + let code = ContractWrapper::new(contract::execute, contract::instantiate, contract::query); + let code_id = app.store_code(Box::new(code)); + + // create test state + let mut test_state = TestState { + contract_addr: Addr::unchecked("contract0"), + }; + + // load trace data + let data = include_str!("../quint/test.itf.json"); + let trace: itf::Trace = trace_from_str(data).unwrap(); + + for s in trace.states { + let last_result = s.value.result.clone(); + if last_result.is_ok() && !last_result.unwrap().messages.is_empty() { + println!("Processing messages, skipping"); + continue; + } + + let action_taken = &s.value.action_taken; + let nondet_picks = &s.value.nondet_picks; + let amount = nondet_picks.amount.clone(); + let denom = nondet_picks.denom.clone(); + let sender = nondet_picks.sender.clone(); + + println!("Step number: {:?}", s.meta.index); + println!("Result from trace: {:?}", s.value.result.clone()); + + match action_taken.as_str() { + + + "deposit_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = ExecuteMsg::Deposit { }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "q::init" => { + println!("Initializing contract."); + + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = InstantiateMsg { owner: "", threshold: 0 }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + test_state.contract_addr = app.instantiate_contract( + code_id, + sender, + &msg, + &funds, + "test", + None, + ).unwrap(); + + for (addr, coins) in s.value.bank.clone().iter() { + for (denom, amount) in coins.iter() { + app = mint_tokens( + app, + addr.clone(), + denom.to_string(), + Uint128::new(amount.to_u128().unwrap()), + ); + } + } + + } + + + "owner_action_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let message_msg = nondet_picks.message_msg.clone().unwrap(); + let msg = ExecuteMsg::OwnerAction { msg: message_msg }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "update_config_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let message_new_threshold = nondet_picks.message_new_threshold.clone().unwrap().to_u64().unwrap().into(); + let msg = ExecuteMsg::UpdateConfig { new_threshold: message_new_threshold }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "withdraw_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let message_amount = nondet_picks.message_amount.clone().unwrap().to_u64().unwrap().into(); + let msg = ExecuteMsg::Withdraw { amount: message_amount }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + _ => panic!("Invalid action taken"), + } + compare_state(&test_state, &app, &(s.value.clone())); + println!( + "clock is advancing for {} seconds", + TICK + ); + app.update_block(|block| { + block.time = block.time.plus_seconds(TICK); + }); + println!("-----------------------------------"); + } + } +} diff --git a/tests/snapshots/integration_tests__ctf08.snap b/tests/snapshots/integration_tests__ctf08.snap index bec0354..f7c6b89 100644 --- a/tests/snapshots/integration_tests__ctf08.snap +++ b/tests/snapshots/integration_tests__ctf08.snap @@ -2,24 +2,29 @@ source: tests/integration_tests.rs expression: output --- +quint: + + +oaksecurity_cosmwasm_ctf_08_stubs.qnt: module oaksecurity_cosmwasm_ctf_08 { - import basicSpells.* from "../lib/basicSpells" - import cw_types.* from "../lib/cw_types" - import messaging.* from "../lib/messaging" - import bank from "../lib/bank" + import basicSpells.* from "./lib/basicSpells" + import cw_types.* from "./lib/cw_types" + import cw_utils.* from "./lib/cw_utils" + import messaging.* from "./lib/messaging" + import bank from "./lib/bank" var contract_state: ContractState - var return: Result + var result: Result var bank: bank::Bank var time: int - pure val CONTRACT_ADDRESS = "" + pure val CONTRACT_ADDRESS = "contract0" - pure val ADDRESSES = Set("s1", "s2", "s3", CONTRACT_ADDRESS) + pure val ADDRESSES = Set("sender1", "sender2", "sender3", CONTRACT_ADDRESS) pure val DENOMS = Set("d1", "uawesome") pure val MAX_AMOUNT = 200 @@ -37,7 +42,11 @@ module oaksecurity_cosmwasm_ctf_08 { | ExecuteMsg_NewTrade({ target: str, offered: str }) | ExecuteMsg_AcceptTrade({ id: str, trader: str }) | ExecuteMsg_CancelTrade({ id: str }) - pure def instantiate(state: ContractState, _env: Env, _info: MessageInfo, msg: InstantiateMsg): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + pure def instantiate(state: ContractState, _env: Env, _info: MessageInfo, msg: InstantiateMsg): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } + pure def execute(state: ContractState, env: Env, info: MessageInfo, msg: ExecuteMsg): (Result[Response, ContractError], ContractState) = match msg { | ExecuteMsg_BuyNFT(__r) => exec_buy(state, env, info, __r.id) | ExecuteMsg_NewSale(__r) => exec_new_sale(state, env, info, __r.id, __r.price, __r.tradable) @@ -46,7 +55,11 @@ module oaksecurity_cosmwasm_ctf_08 { | ExecuteMsg_AcceptTrade(__r) => exec_accept_trade(state, info, __r.id, __r.trader) | ExecuteMsg_CancelTrade(__r) => exec_cancel_trade(state, info, __r.id) } - pure def exec_new_sale(state: ContractState, env: Env, info: MessageInfo, id: str, price: int, tradable: bool): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def exec_new_sale(state: ContractState, env: Env, info: MessageInfo, id: str, price: int, tradable: bool): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action exec_new_sale_action = { // TODO: Change next line according to fund expectations @@ -57,7 +70,11 @@ module oaksecurity_cosmwasm_ctf_08 { pure val message: ExecuteMsg = ExecuteMsg_NewSale({ id: message_id, price: message_price, tradable: message_tradable }) execute_message(message, max_funds) } - pure def exec_buy(state: ContractState, _env: Env, info: MessageInfo, id: str): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def exec_buy(state: ContractState, _env: Env, info: MessageInfo, id: str): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action exec_buy_action = { // TODO: Change next line according to fund expectations @@ -66,7 +83,11 @@ module oaksecurity_cosmwasm_ctf_08 { pure val message: ExecuteMsg = ExecuteMsg_BuyNFT({ id: message_id }) execute_message(message, max_funds) } - pure def exec_cancel_sale(state: ContractState, info: MessageInfo, id: str): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def exec_cancel_sale(state: ContractState, info: MessageInfo, id: str): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action exec_cancel_sale_action = { // TODO: Change next line according to fund expectations @@ -75,7 +96,11 @@ module oaksecurity_cosmwasm_ctf_08 { pure val message: ExecuteMsg = ExecuteMsg_CancelSale({ id: message_id }) execute_message(message, max_funds) } - pure def exec_new_trade(state: ContractState, env: Env, info: MessageInfo, asked_id: str, offered_id: str): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def exec_new_trade(state: ContractState, env: Env, info: MessageInfo, asked_id: str, offered_id: str): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action exec_new_trade_action = { // TODO: Change next line according to fund expectations @@ -85,7 +110,11 @@ module oaksecurity_cosmwasm_ctf_08 { pure val message: ExecuteMsg = ExecuteMsg_NewTrade({ target: message_target, offered: message_offered }) execute_message(message, max_funds) } - pure def exec_accept_trade(state: ContractState, info: MessageInfo, asked_id: str, trader: str): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def exec_accept_trade(state: ContractState, info: MessageInfo, asked_id: str, trader: str): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action exec_accept_trade_action = { // TODO: Change next line according to fund expectations @@ -95,7 +124,11 @@ module oaksecurity_cosmwasm_ctf_08 { pure val message: ExecuteMsg = ExecuteMsg_AcceptTrade({ id: message_id, trader: message_trader }) execute_message(message, max_funds) } - pure def exec_cancel_trade(state: ContractState, info: MessageInfo, asked_id: str): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def exec_cancel_trade(state: ContractState, info: MessageInfo, asked_id: str): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action exec_cancel_trade_action = { // TODO: Change next line according to fund expectations @@ -104,20 +137,24 @@ module oaksecurity_cosmwasm_ctf_08 { pure val message: ExecuteMsg = ExecuteMsg_CancelTrade({ id: message_id }) execute_message(message, max_funds) } - pure def reply(state: ContractState, _env: Env, reply: Reply): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + pure def reply(state: ContractState, _env: Env, reply: Reply): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } + pure val DENOM = "uawesome" pure val TRADE_REPLY = 1 pure val SALE_REPLY = 2 type ContractState = { config: Config, - sales: str -> Sale, - trades: str -> Trade, - operations: Operations + sales: str -> Sale, + trades: str -> Trade, + operations: Operations } pure val init_contract_state = { - config: { nft_contract: "s1" }, + config: { nft_contract: "s1" }, sales: Map(), trades: Map(), operations: { n_trades: 0,n_sales: 0 } @@ -141,11 +178,25 @@ module oaksecurity_cosmwasm_ctf_08 { val env_val = { block: { time: time } } - action init = all { - contract_state' = init_contract_state, - bank' = init_bank_state, - return' = Err("No previous request"), - time' = 0, + action init = { + // TODO: Change next line according to fund expectations + pure val max_funds = 0 + + nondet sender = Set("admin").oneOf() + nondet denom = DENOMS.oneOf() + nondet amount = 0.to(max_funds).oneOf() + val funds = [{ denom: denom, amount: amount }] + val info = { sender: sender, funds: funds } + + pure val message: InstantiateMsg = { nft_address: "" } + pure val r = instantiate(init_contract_state, { block: { time: 0 } }, info, message) + + all { + contract_state' = r._2, + bank' = init_bank_state, + result' = r._1, + time' = 0, + } } @@ -159,9 +210,12 @@ module oaksecurity_cosmwasm_ctf_08 { val r = execute(contract_state, env_val, info, message) all { bank.get(sender).get(denom) >= amount, - bank' = bank.setBy(sender, balances => balances.setBy(denom, balance => balance - amount)) - .setBy(CONTRACT_ADDRESS, balances => balances.setBy(denom, balance => balance + amount)), - return' = r._1, + match r._1 { + | Ok(_) => bank' = bank.setBy(sender, balances => balances.setBy(denom, balance => balance - amount)) + .setBy(CONTRACT_ADDRESS, balances => balances.setBy(denom, balance => balance + amount)) + | Err(_) => bank' = bank + }, + result' = r._1, contract_state' = r._2, } } @@ -169,16 +223,16 @@ module oaksecurity_cosmwasm_ctf_08 { action advance_time = time' = time + 1 action step = { - val message_getting = get_message(return) - val new_return = message_getting._1 + val message_getting = get_message(result) + val new_result = message_getting._1 val opt_message = message_getting._2 match opt_message { | Some(submsg) => { - val current_state = { bank: bank, return: new_return, contract_state: contract_state } + val current_state = { bank: bank, result: new_result, contract_state: contract_state } val new_state = process_message(current_state, env_val, CONTRACT_ADDRESS, submsg, reply) all { bank' = new_state.bank, - return' = new_state.return, + result' = new_state.result, contract_state' = new_state.contract_state, advance_time, } @@ -188,3 +242,436 @@ module oaksecurity_cosmwasm_ctf_08 { } } + + +mbt: +mbt_oaksecurity_cosmwasm_ctf_08.rs: + +pub mod state_structs { + use num_bigint::BigInt; + use serde::Deserialize; + use std::collections::HashMap; + use itf::de::{self, As}; + + #[derive(Clone, Debug, Deserialize)] + pub struct Config { + pub nft_contract: String + } + + #[derive(Clone, Debug, Deserialize)] + pub struct GetCountResponse { + pub count: BigInt + } + + #[derive(Clone, Debug, Deserialize)] + pub struct InstantiateMsg { + pub nft_address: String + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Operations { + pub n_trades: BigInt, + pub n_sales: BigInt + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Sale { + pub nft_id: String, + pub price: BigInt, + pub owner: String, + pub tradable: bool + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Trade { + pub asked_id: String, + pub to_trade_id: String, + pub trader: String + } + + #[derive(Clone, Debug, Deserialize)] + pub struct ContractState { + pub config: Config, + pub sales: HashMap, + pub trades: HashMap, + pub operations: Operations + } + + #[derive(Clone, Debug, Deserialize)] + pub struct NondetPicks { + + #[serde(with = "As::>")] + pub sender: Option, + + #[serde(with = "As::>")] + pub denom: Option, + + #[serde(with = "As::>")] + pub amount: Option, + + #[serde(with = "As::>")] + pub message_id: Option, + + #[serde(with = "As::>")] + pub message_price: Option, + + #[serde(with = "As::>")] + pub message_tradable: Option, + + #[serde(with = "As::>")] + pub message_id: Option, + + #[serde(with = "As::>")] + pub message_id: Option, + + #[serde(with = "As::>")] + pub message_target: Option, + + #[serde(with = "As::>")] + pub message_offered: Option, + + #[serde(with = "As::>")] + pub message_id: Option, + + #[serde(with = "As::>")] + pub message_trader: Option, + + #[serde(with = "As::>")] + pub message_id: Option + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Message {} + #[derive(Clone, Debug, Deserialize)] + pub struct Attribute { + pub key: String, + pub value: QuintSerializedValue, + } + + #[derive(Clone, Debug, Deserialize)] + #[serde(tag = "tag", content = "value")] + pub enum QuintSerializedValue { + FromInt(BigInt), + FromStr(String), + FromListInt(Vec), + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Response { + pub messages: Vec, + pub attributes: Vec, + } + + #[derive(Clone, Debug, Deserialize)] + pub struct State { + pub contract_state: ContractState, + pub bank: HashMap>, + #[serde(with = "As::>")] + pub result: Result, + pub action_taken: String, + pub nondet_picks: NondetPicks, + pub time: BigInt, + } + +} + +#[cfg(test)] +pub mod tests { + use oaksecurity_cosmwasm_ctf_08::contract; + use oaksecurity_cosmwasm_ctf_08::msg::{ExecuteMsg, InstantiateMsg}; + + + use crate::state_structs::*; + use cosmwasm_std::{coin, Addr, Uint128}; + use cw_multi_test::{App, AppResponse, ContractWrapper, Executor}; + use itf::trace_from_str; + use num_bigint::BigInt; + use num_traits::{ToPrimitive, Zero}; + + pub const DENOM: &str = "uawesome"; + pub const TICK: u64 = 1; + + pub fn mint_tokens(mut app: App, recipient: String, denom: String, amount: Uint128) -> App { + app.sudo(cw_multi_test::SudoMsg::Bank( + cw_multi_test::BankSudo::Mint { + to_address: recipient.to_owned(), + amount: vec![coin(amount.u128(), denom)], + }, + )) + .unwrap(); + app + } + + fn compare_state(test_state: &TestState, app: &App, state: &State) { + // compare contract balances + let balance = app + .wrap() + .query_balance(&test_state.contract_addr, DENOM) + .unwrap() + .amount; + let trace_balance = state + .bank + .get(&test_state.contract_addr.to_string()) + .and_then(|x| x.get(DENOM)) + .and_then(|x| x.to_u128()) + .unwrap_or(0); + println!( + "Contract balance ({:?}) for {DENOM}: {:?} vs {:?}", + test_state.contract_addr, + balance, + Uint128::new(trace_balance) + ); + assert_eq!(balance, Uint128::new(trace_balance)); + + // TODO: Query the contract and compare the state as you wish + } + + fn compare_result( + trace_result: Result, + app_result: Result, + ) { + if trace_result.is_ok() { + assert!( + app_result.is_ok(), + "Action unexpectedly failed, error: {:?}", + app_result.err() + ); + println!("Action successful as expected"); + } else { + assert!( + app_result.is_err(), + "Expected action to fail with error: {:?}", + trace_result.err() + ); + println!("Action failed as expected"); + } + } + + fn funds_from_trace(amount: Option, denom: Option) -> Vec { + if amount.is_none() || denom.is_none() || amount == Some(Zero::zero()) { + return vec![]; + } + + vec![coin( + amount.as_ref().unwrap().to_u128().unwrap(), + denom.unwrap(), + )] + } + + // Testing is stateful. + struct TestState { + // we will only know the contract address once we have processed an `instantiate` step + pub contract_addr: Addr, + } + + #[test] + fn model_test() { + let mut app = App::default(); + let code = ContractWrapper::new(contract::execute, contract::instantiate, contract::query); + let code_id = app.store_code(Box::new(code)); + + // create test state + let mut test_state = TestState { + contract_addr: Addr::unchecked("contract0"), + }; + + // load trace data + let data = include_str!("../quint/test.itf.json"); + let trace: itf::Trace = trace_from_str(data).unwrap(); + + for s in trace.states { + let last_result = s.value.result.clone(); + if last_result.is_ok() && !last_result.unwrap().messages.is_empty() { + println!("Processing messages, skipping"); + continue; + } + + let action_taken = &s.value.action_taken; + let nondet_picks = &s.value.nondet_picks; + let amount = nondet_picks.amount.clone(); + let denom = nondet_picks.denom.clone(); + let sender = nondet_picks.sender.clone(); + + println!("Step number: {:?}", s.meta.index); + println!("Result from trace: {:?}", s.value.result.clone()); + + match action_taken.as_str() { + + + "exec_accept_trade_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let message_id = nondet_picks.message_id.clone().unwrap(); + let message_trader = nondet_picks.message_trader.clone().unwrap(); + let msg = ExecuteMsg::AcceptTrade { id: message_id, trader: message_trader }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "exec_buy_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let message_id = nondet_picks.message_id.clone().unwrap(); + let msg = ExecuteMsg::BuyNFT { id: message_id }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "exec_cancel_sale_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let message_id = nondet_picks.message_id.clone().unwrap(); + let msg = ExecuteMsg::CancelSale { id: message_id }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "exec_cancel_trade_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let message_id = nondet_picks.message_id.clone().unwrap(); + let msg = ExecuteMsg::CancelTrade { id: message_id }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "exec_new_sale_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let message_id = nondet_picks.message_id.clone().unwrap(); + let message_price = nondet_picks.message_price.clone().unwrap().to_u64().unwrap().into(); + let message_tradable = nondet_picks.message_tradable.clone().unwrap(); + let msg = ExecuteMsg::NewSale { id: message_id, price: message_price, tradable: message_tradable }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "exec_new_trade_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let message_target = nondet_picks.message_target.clone().unwrap(); + let message_offered = nondet_picks.message_offered.clone().unwrap(); + let msg = ExecuteMsg::NewTrade { target: message_target, offered: message_offered }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "q::init" => { + println!("Initializing contract."); + + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = InstantiateMsg { nft_address: "" }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + test_state.contract_addr = app.instantiate_contract( + code_id, + sender, + &msg, + &funds, + "test", + None, + ).unwrap(); + + for (addr, coins) in s.value.bank.clone().iter() { + for (denom, amount) in coins.iter() { + app = mint_tokens( + app, + addr.clone(), + denom.to_string(), + Uint128::new(amount.to_u128().unwrap()), + ); + } + } + + } + + _ => panic!("Invalid action taken"), + } + compare_state(&test_state, &app, &(s.value.clone())); + println!( + "clock is advancing for {} seconds", + TICK + ); + app.update_block(|block| { + block.time = block.time.plus_seconds(TICK); + }); + println!("-----------------------------------"); + } + } +} diff --git a/tests/snapshots/integration_tests__ctf09.snap b/tests/snapshots/integration_tests__ctf09.snap index 11c3aa6..f591a40 100644 --- a/tests/snapshots/integration_tests__ctf09.snap +++ b/tests/snapshots/integration_tests__ctf09.snap @@ -2,24 +2,29 @@ source: tests/integration_tests.rs expression: output --- +quint: + + +oaksecurity_cosmwasm_ctf_09_stubs.qnt: module oaksecurity_cosmwasm_ctf_09 { - import basicSpells.* from "../lib/basicSpells" - import cw_types.* from "../lib/cw_types" - import messaging.* from "../lib/messaging" - import bank from "../lib/bank" + import basicSpells.* from "./lib/basicSpells" + import cw_types.* from "./lib/cw_types" + import cw_utils.* from "./lib/cw_utils" + import messaging.* from "./lib/messaging" + import bank from "./lib/bank" var contract_state: ContractState - var return: Result + var result: Result var bank: bank::Bank var time: int - pure val CONTRACT_ADDRESS = "" + pure val CONTRACT_ADDRESS = "contract0" - pure val ADDRESSES = Set("s1", "s2", "s3", CONTRACT_ADDRESS) + pure val ADDRESSES = Set("sender1", "sender2", "sender3", CONTRACT_ADDRESS) pure val DENOMS = Set("d1", "uawesome") pure val MAX_AMOUNT = 200 @@ -32,14 +37,22 @@ module oaksecurity_cosmwasm_ctf_09 { | ExecuteMsg_Deposit | ExecuteMsg_Withdraw({ amount: int }) | ExecuteMsg_ClaimRewards - pure def instantiate(state: ContractState, _env: Env, info: MessageInfo, _msg: InstantiateMsg): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + pure def instantiate(state: ContractState, _env: Env, info: MessageInfo, _msg: InstantiateMsg): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } + pure def execute(state: ContractState, env: Env, info: MessageInfo, msg: ExecuteMsg): (Result[Response, ContractError], ContractState) = match msg { | ExecuteMsg_IncreaseReward(__r) => increase_reward(state, env, info) | ExecuteMsg_Deposit(__r) => deposit(state, info) | ExecuteMsg_Withdraw(__r) => withdraw(state, info, __r.amount) | ExecuteMsg_ClaimRewards(__r) => claim_rewards(state, info) } - pure def increase_reward(state: ContractState, _env: Env, info: MessageInfo): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def increase_reward(state: ContractState, _env: Env, info: MessageInfo): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action increase_reward_action = { // TODO: Change next line according to fund expectations @@ -48,7 +61,11 @@ module oaksecurity_cosmwasm_ctf_09 { pure val message: ExecuteMsg = ExecuteMsg_IncreaseReward execute_message(message, max_funds) } - pure def deposit(state: ContractState, info: MessageInfo): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def deposit(state: ContractState, info: MessageInfo): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action deposit_action = { // TODO: Change next line according to fund expectations @@ -57,7 +74,11 @@ module oaksecurity_cosmwasm_ctf_09 { pure val message: ExecuteMsg = ExecuteMsg_Deposit execute_message(message, max_funds) } - pure def withdraw(state: ContractState, info: MessageInfo, amount: int): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def withdraw(state: ContractState, info: MessageInfo, amount: int): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action withdraw_action = { // TODO: Change next line according to fund expectations @@ -66,7 +87,11 @@ module oaksecurity_cosmwasm_ctf_09 { pure val message: ExecuteMsg = ExecuteMsg_Withdraw({ amount: message_amount }) execute_message(message, max_funds) } - pure def claim_rewards(state: ContractState, info: MessageInfo): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def claim_rewards(state: ContractState, info: MessageInfo): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action claim_rewards_action = { // TODO: Change next line according to fund expectations @@ -80,11 +105,11 @@ module oaksecurity_cosmwasm_ctf_09 { type ContractState = { state: State, - users: Addr -> UserRewardInfo + users: Addr -> UserRewardInfo } pure val init_contract_state = { - state: { owner: "s1",total_staked: 0,global_index: 0 }, + state: { owner: "s1",total_staked: 0,global_index: 0 }, users: Map() } @@ -98,20 +123,32 @@ module oaksecurity_cosmwasm_ctf_09 { advance_time, } - pure def reply(state: ContractState, _env: Env, _reply: Reply): (Result, ContractState) = (Ok(Response_new), state) - pure val init_bank_state = ADDRESSES.mapBy(_ => DENOMS.mapBy(_ => MAX_AMOUNT)) val env_val = { block: { time: time } } - action init = all { - contract_state' = init_contract_state, - bank' = init_bank_state, - return' = Err("No previous request"), - time' = 0, + action init = { + // TODO: Change next line according to fund expectations + pure val max_funds = 0 + + nondet sender = Set("admin").oneOf() + nondet denom = DENOMS.oneOf() + nondet amount = 0.to(max_funds).oneOf() + val funds = [{ denom: denom, amount: amount }] + val info = { sender: sender, funds: funds } + + pure val message: InstantiateMsg = { } + pure val r = instantiate(init_contract_state, { block: { time: 0 } }, info, message) + + all { + contract_state' = r._2, + bank' = init_bank_state, + result' = r._1, + time' = 0, + } } @@ -125,9 +162,12 @@ module oaksecurity_cosmwasm_ctf_09 { val r = execute(contract_state, env_val, info, message) all { bank.get(sender).get(denom) >= amount, - bank' = bank.setBy(sender, balances => balances.setBy(denom, balance => balance - amount)) - .setBy(CONTRACT_ADDRESS, balances => balances.setBy(denom, balance => balance + amount)), - return' = r._1, + match r._1 { + | Ok(_) => bank' = bank.setBy(sender, balances => balances.setBy(denom, balance => balance - amount)) + .setBy(CONTRACT_ADDRESS, balances => balances.setBy(denom, balance => balance + amount)) + | Err(_) => bank' = bank + }, + result' = r._1, contract_state' = r._2, } } @@ -135,16 +175,16 @@ module oaksecurity_cosmwasm_ctf_09 { action advance_time = time' = time + 1 action step = { - val message_getting = get_message(return) - val new_return = message_getting._1 + val message_getting = get_message(result) + val new_result = message_getting._1 val opt_message = message_getting._2 match opt_message { | Some(submsg) => { - val current_state = { bank: bank, return: new_return, contract_state: contract_state } + val current_state = { bank: bank, result: new_result, contract_state: contract_state } val new_state = process_message(current_state, env_val, CONTRACT_ADDRESS, submsg, reply) all { bank' = new_state.bank, - return' = new_state.return, + result' = new_state.result, contract_state' = new_state.contract_state, advance_time, } @@ -154,3 +194,341 @@ module oaksecurity_cosmwasm_ctf_09 { } } + + +mbt: +mbt_oaksecurity_cosmwasm_ctf_09.rs: + +pub mod state_structs { + use num_bigint::BigInt; + use serde::Deserialize; + use std::collections::HashMap; + use itf::de::{self, As}; + + #[derive(Clone, Debug, Deserialize)] + pub struct InstantiateMsg { + + } + + #[derive(Clone, Debug, Deserialize)] + pub struct State { + pub owner: String, + pub total_staked: BigInt, + pub global_index: BigInt + } + + #[derive(Clone, Debug, Deserialize)] + pub struct UserRewardInfo { + pub staked_amount: BigInt, + pub user_index: BigInt, + pub pending_rewards: BigInt + } + + #[derive(Clone, Debug, Deserialize)] + pub struct ContractState { + pub state: State, + pub users: HashMap + } + + #[derive(Clone, Debug, Deserialize)] + pub struct NondetPicks { + + #[serde(with = "As::>")] + pub sender: Option, + + #[serde(with = "As::>")] + pub denom: Option, + + #[serde(with = "As::>")] + pub amount: Option, + + #[serde(with = "As::>")] + pub message_amount: Option + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Message {} + #[derive(Clone, Debug, Deserialize)] + pub struct Attribute { + pub key: String, + pub value: QuintSerializedValue, + } + + #[derive(Clone, Debug, Deserialize)] + #[serde(tag = "tag", content = "value")] + pub enum QuintSerializedValue { + FromInt(BigInt), + FromStr(String), + FromListInt(Vec), + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Response { + pub messages: Vec, + pub attributes: Vec, + } + + #[derive(Clone, Debug, Deserialize)] + pub struct State { + pub contract_state: ContractState, + pub bank: HashMap>, + #[serde(with = "As::>")] + pub result: Result, + pub action_taken: String, + pub nondet_picks: NondetPicks, + pub time: BigInt, + } + +} + +#[cfg(test)] +pub mod tests { + use oaksecurity_cosmwasm_ctf_09::contract; + use oaksecurity_cosmwasm_ctf_09::msg::{ExecuteMsg, InstantiateMsg}; + + + use crate::state_structs::*; + use cosmwasm_std::{coin, Addr, Uint128}; + use cw_multi_test::{App, AppResponse, ContractWrapper, Executor}; + use itf::trace_from_str; + use num_bigint::BigInt; + use num_traits::{ToPrimitive, Zero}; + + pub const DENOM: &str = "uawesome"; + pub const TICK: u64 = 1; + + pub fn mint_tokens(mut app: App, recipient: String, denom: String, amount: Uint128) -> App { + app.sudo(cw_multi_test::SudoMsg::Bank( + cw_multi_test::BankSudo::Mint { + to_address: recipient.to_owned(), + amount: vec![coin(amount.u128(), denom)], + }, + )) + .unwrap(); + app + } + + fn compare_state(test_state: &TestState, app: &App, state: &State) { + // compare contract balances + let balance = app + .wrap() + .query_balance(&test_state.contract_addr, DENOM) + .unwrap() + .amount; + let trace_balance = state + .bank + .get(&test_state.contract_addr.to_string()) + .and_then(|x| x.get(DENOM)) + .and_then(|x| x.to_u128()) + .unwrap_or(0); + println!( + "Contract balance ({:?}) for {DENOM}: {:?} vs {:?}", + test_state.contract_addr, + balance, + Uint128::new(trace_balance) + ); + assert_eq!(balance, Uint128::new(trace_balance)); + + // TODO: Query the contract and compare the state as you wish + } + + fn compare_result( + trace_result: Result, + app_result: Result, + ) { + if trace_result.is_ok() { + assert!( + app_result.is_ok(), + "Action unexpectedly failed, error: {:?}", + app_result.err() + ); + println!("Action successful as expected"); + } else { + assert!( + app_result.is_err(), + "Expected action to fail with error: {:?}", + trace_result.err() + ); + println!("Action failed as expected"); + } + } + + fn funds_from_trace(amount: Option, denom: Option) -> Vec { + if amount.is_none() || denom.is_none() || amount == Some(Zero::zero()) { + return vec![]; + } + + vec![coin( + amount.as_ref().unwrap().to_u128().unwrap(), + denom.unwrap(), + )] + } + + // Testing is stateful. + struct TestState { + // we will only know the contract address once we have processed an `instantiate` step + pub contract_addr: Addr, + } + + #[test] + fn model_test() { + let mut app = App::default(); + let code = ContractWrapper::new(contract::execute, contract::instantiate, contract::query); + let code_id = app.store_code(Box::new(code)); + + // create test state + let mut test_state = TestState { + contract_addr: Addr::unchecked("contract0"), + }; + + // load trace data + let data = include_str!("../quint/test.itf.json"); + let trace: itf::Trace = trace_from_str(data).unwrap(); + + for s in trace.states { + let last_result = s.value.result.clone(); + if last_result.is_ok() && !last_result.unwrap().messages.is_empty() { + println!("Processing messages, skipping"); + continue; + } + + let action_taken = &s.value.action_taken; + let nondet_picks = &s.value.nondet_picks; + let amount = nondet_picks.amount.clone(); + let denom = nondet_picks.denom.clone(); + let sender = nondet_picks.sender.clone(); + + println!("Step number: {:?}", s.meta.index); + println!("Result from trace: {:?}", s.value.result.clone()); + + match action_taken.as_str() { + + + "claim_rewards_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = ExecuteMsg::ClaimRewards { }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "deposit_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = ExecuteMsg::Deposit { }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "increase_reward_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = ExecuteMsg::IncreaseReward { }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + + "q::init" => { + println!("Initializing contract."); + + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = InstantiateMsg { }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + test_state.contract_addr = app.instantiate_contract( + code_id, + sender, + &msg, + &funds, + "test", + None, + ).unwrap(); + + for (addr, coins) in s.value.bank.clone().iter() { + for (denom, amount) in coins.iter() { + app = mint_tokens( + app, + addr.clone(), + denom.to_string(), + Uint128::new(amount.to_u128().unwrap()), + ); + } + } + + } + + + "withdraw_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let message_amount = nondet_picks.message_amount.clone().unwrap().to_u64().unwrap().into(); + let msg = ExecuteMsg::Withdraw { amount: message_amount }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + _ => panic!("Invalid action taken"), + } + compare_state(&test_state, &app, &(s.value.clone())); + println!( + "clock is advancing for {} seconds", + TICK + ); + app.update_block(|block| { + block.time = block.time.plus_seconds(TICK); + }); + println!("-----------------------------------"); + } + } +} diff --git a/tests/snapshots/integration_tests__ctf10.snap b/tests/snapshots/integration_tests__ctf10.snap index 1090f62..2c4d97c 100644 --- a/tests/snapshots/integration_tests__ctf10.snap +++ b/tests/snapshots/integration_tests__ctf10.snap @@ -2,24 +2,29 @@ source: tests/integration_tests.rs expression: output --- +quint: + + +oaksecurity_cosmwasm_ctf_10_stubs.qnt: module oaksecurity_cosmwasm_ctf_10 { - import basicSpells.* from "../lib/basicSpells" - import cw_types.* from "../lib/cw_types" - import messaging.* from "../lib/messaging" - import bank from "../lib/bank" + import basicSpells.* from "./lib/basicSpells" + import cw_types.* from "./lib/cw_types" + import cw_utils.* from "./lib/cw_utils" + import messaging.* from "./lib/messaging" + import bank from "./lib/bank" var contract_state: ContractState - var return: Result + var result: Result var bank: bank::Bank var time: int - pure val CONTRACT_ADDRESS = "" + pure val CONTRACT_ADDRESS = "contract0" - pure val ADDRESSES = Set("s1", "s2", "s3", CONTRACT_ADDRESS) + pure val ADDRESSES = Set("sender1", "sender2", "sender3", CONTRACT_ADDRESS) pure val DENOMS = Set("d1", "uawesome") pure val MAX_AMOUNT = 200 @@ -29,11 +34,19 @@ module oaksecurity_cosmwasm_ctf_10 { type Whitelist = { users: List[str] } type ExecuteMsg = | ExecuteMsg_Mint - pure def instantiate(state: ContractState, env: Env, _info: MessageInfo, msg: InstantiateMsg): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + pure def instantiate(state: ContractState, env: Env, _info: MessageInfo, msg: InstantiateMsg): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } + pure def execute(state: ContractState, env: Env, info: MessageInfo, msg: ExecuteMsg): (Result[Response, ContractError], ContractState) = match msg { | ExecuteMsg_Mint(__r) => mint(state, env, info) } - pure def mint(state: ContractState, _env: Env, info: MessageInfo): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + + pure def mint(state: ContractState, _env: Env, info: MessageInfo): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } action mint_action = { // TODO: Change next line according to fund expectations @@ -42,16 +55,20 @@ module oaksecurity_cosmwasm_ctf_10 { pure val message: ExecuteMsg = ExecuteMsg_Mint execute_message(message, max_funds) } - pure def reply(state: ContractState, _env: Env, reply: Reply): (Result[Response, ContractError], ContractState) = (Ok(Response_new), state) + pure def reply(state: ContractState, _env: Env, reply: Reply): (Result[Response, ContractError], ContractState) = { + // TODO: Update body + (Ok(Response_new), state) + } + pure val DENOM = "uawesome" type ContractState = { config: Config, - whitelist: Whitelist + whitelist: Whitelist } pure val init_contract_state = { - config: { nft_contract: "s1",mint_per_user: 0,total_tokens: 0 }, + config: { nft_contract: "s1",mint_per_user: 0,total_tokens: 0 }, whitelist: { users: [] } } @@ -68,11 +85,25 @@ module oaksecurity_cosmwasm_ctf_10 { val env_val = { block: { time: time } } - action init = all { - contract_state' = init_contract_state, - bank' = init_bank_state, - return' = Err("No previous request"), - time' = 0, + action init = { + // TODO: Change next line according to fund expectations + pure val max_funds = 0 + + nondet sender = Set("admin").oneOf() + nondet denom = DENOMS.oneOf() + nondet amount = 0.to(max_funds).oneOf() + val funds = [{ denom: denom, amount: amount }] + val info = { sender: sender, funds: funds } + + pure val message: InstantiateMsg = { cw721_code_id: 0,mint_per_user: 0,whitelisted_users: [] } + pure val r = instantiate(init_contract_state, { block: { time: 0 } }, info, message) + + all { + contract_state' = r._2, + bank' = init_bank_state, + result' = r._1, + time' = 0, + } } @@ -86,9 +117,12 @@ module oaksecurity_cosmwasm_ctf_10 { val r = execute(contract_state, env_val, info, message) all { bank.get(sender).get(denom) >= amount, - bank' = bank.setBy(sender, balances => balances.setBy(denom, balance => balance - amount)) - .setBy(CONTRACT_ADDRESS, balances => balances.setBy(denom, balance => balance + amount)), - return' = r._1, + match r._1 { + | Ok(_) => bank' = bank.setBy(sender, balances => balances.setBy(denom, balance => balance - amount)) + .setBy(CONTRACT_ADDRESS, balances => balances.setBy(denom, balance => balance + amount)) + | Err(_) => bank' = bank + }, + result' = r._1, contract_state' = r._2, } } @@ -96,16 +130,16 @@ module oaksecurity_cosmwasm_ctf_10 { action advance_time = time' = time + 1 action step = { - val message_getting = get_message(return) - val new_return = message_getting._1 + val message_getting = get_message(result) + val new_result = message_getting._1 val opt_message = message_getting._2 match opt_message { | Some(submsg) => { - val current_state = { bank: bank, return: new_return, contract_state: contract_state } + val current_state = { bank: bank, result: new_result, contract_state: contract_state } val new_state = process_message(current_state, env_val, CONTRACT_ADDRESS, submsg, reply) all { bank' = new_state.bank, - return' = new_state.return, + result' = new_state.result, contract_state' = new_state.contract_state, advance_time, } @@ -115,3 +149,277 @@ module oaksecurity_cosmwasm_ctf_10 { } } + + +mbt: +mbt_oaksecurity_cosmwasm_ctf_10.rs: + +pub mod state_structs { + use num_bigint::BigInt; + use serde::Deserialize; + use std::collections::HashMap; + use itf::de::{self, As}; + + #[derive(Clone, Debug, Deserialize)] + pub struct Config { + pub nft_contract: String, + pub mint_per_user: BigInt, + pub total_tokens: BigInt + } + + #[derive(Clone, Debug, Deserialize)] + pub struct InstantiateMsg { + pub cw721_code_id: BigInt, + pub mint_per_user: BigInt, + pub whitelisted_users: Vec + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Whitelist { + pub users: Vec + } + + #[derive(Clone, Debug, Deserialize)] + pub struct ContractState { + pub config: Config, + pub whitelist: Whitelist + } + + #[derive(Clone, Debug, Deserialize)] + pub struct NondetPicks { + + #[serde(with = "As::>")] + pub sender: Option, + + #[serde(with = "As::>")] + pub denom: Option, + + #[serde(with = "As::>")] + pub amount: Option + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Message {} + #[derive(Clone, Debug, Deserialize)] + pub struct Attribute { + pub key: String, + pub value: QuintSerializedValue, + } + + #[derive(Clone, Debug, Deserialize)] + #[serde(tag = "tag", content = "value")] + pub enum QuintSerializedValue { + FromInt(BigInt), + FromStr(String), + FromListInt(Vec), + } + + #[derive(Clone, Debug, Deserialize)] + pub struct Response { + pub messages: Vec, + pub attributes: Vec, + } + + #[derive(Clone, Debug, Deserialize)] + pub struct State { + pub contract_state: ContractState, + pub bank: HashMap>, + #[serde(with = "As::>")] + pub result: Result, + pub action_taken: String, + pub nondet_picks: NondetPicks, + pub time: BigInt, + } + +} + +#[cfg(test)] +pub mod tests { + use oaksecurity_cosmwasm_ctf_10::contract; + use oaksecurity_cosmwasm_ctf_10::msg::{ExecuteMsg, InstantiateMsg}; + + + use crate::state_structs::*; + use cosmwasm_std::{coin, Addr, Uint128}; + use cw_multi_test::{App, AppResponse, ContractWrapper, Executor}; + use itf::trace_from_str; + use num_bigint::BigInt; + use num_traits::{ToPrimitive, Zero}; + + pub const DENOM: &str = "uawesome"; + pub const TICK: u64 = 1; + + pub fn mint_tokens(mut app: App, recipient: String, denom: String, amount: Uint128) -> App { + app.sudo(cw_multi_test::SudoMsg::Bank( + cw_multi_test::BankSudo::Mint { + to_address: recipient.to_owned(), + amount: vec![coin(amount.u128(), denom)], + }, + )) + .unwrap(); + app + } + + fn compare_state(test_state: &TestState, app: &App, state: &State) { + // compare contract balances + let balance = app + .wrap() + .query_balance(&test_state.contract_addr, DENOM) + .unwrap() + .amount; + let trace_balance = state + .bank + .get(&test_state.contract_addr.to_string()) + .and_then(|x| x.get(DENOM)) + .and_then(|x| x.to_u128()) + .unwrap_or(0); + println!( + "Contract balance ({:?}) for {DENOM}: {:?} vs {:?}", + test_state.contract_addr, + balance, + Uint128::new(trace_balance) + ); + assert_eq!(balance, Uint128::new(trace_balance)); + + // TODO: Query the contract and compare the state as you wish + } + + fn compare_result( + trace_result: Result, + app_result: Result, + ) { + if trace_result.is_ok() { + assert!( + app_result.is_ok(), + "Action unexpectedly failed, error: {:?}", + app_result.err() + ); + println!("Action successful as expected"); + } else { + assert!( + app_result.is_err(), + "Expected action to fail with error: {:?}", + trace_result.err() + ); + println!("Action failed as expected"); + } + } + + fn funds_from_trace(amount: Option, denom: Option) -> Vec { + if amount.is_none() || denom.is_none() || amount == Some(Zero::zero()) { + return vec![]; + } + + vec![coin( + amount.as_ref().unwrap().to_u128().unwrap(), + denom.unwrap(), + )] + } + + // Testing is stateful. + struct TestState { + // we will only know the contract address once we have processed an `instantiate` step + pub contract_addr: Addr, + } + + #[test] + fn model_test() { + let mut app = App::default(); + let code = ContractWrapper::new(contract::execute, contract::instantiate, contract::query); + let code_id = app.store_code(Box::new(code)); + + // create test state + let mut test_state = TestState { + contract_addr: Addr::unchecked("contract0"), + }; + + // load trace data + let data = include_str!("../quint/test.itf.json"); + let trace: itf::Trace = trace_from_str(data).unwrap(); + + for s in trace.states { + let last_result = s.value.result.clone(); + if last_result.is_ok() && !last_result.unwrap().messages.is_empty() { + println!("Processing messages, skipping"); + continue; + } + + let action_taken = &s.value.action_taken; + let nondet_picks = &s.value.nondet_picks; + let amount = nondet_picks.amount.clone(); + let denom = nondet_picks.denom.clone(); + let sender = nondet_picks.sender.clone(); + + println!("Step number: {:?}", s.meta.index); + println!("Result from trace: {:?}", s.value.result.clone()); + + match action_taken.as_str() { + + + "q::init" => { + println!("Initializing contract."); + + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = InstantiateMsg { cw721_code_id: 0, mint_per_user: 0, whitelisted_users: [] }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + test_state.contract_addr = app.instantiate_contract( + code_id, + sender, + &msg, + &funds, + "test", + None, + ).unwrap(); + + for (addr, coins) in s.value.bank.clone().iter() { + for (denom, amount) in coins.iter() { + app = mint_tokens( + app, + addr.clone(), + denom.to_string(), + Uint128::new(amount.to_u128().unwrap()), + ); + } + } + + } + + + "mint_action" => { + let sender = Addr::unchecked(sender.unwrap()); + let funds = funds_from_trace(amount, denom); + + let msg = ExecuteMsg::Mint { }; + println!("Message: {:?}", msg); + println!("Sender: {:?}", sender); + println!("Funds: {:?}", funds); + + let res = app.execute_contract( + sender, + test_state.contract_addr.clone(), + &msg, + &funds, + ); + + compare_result(s.value.result.clone(), res) + } + + _ => panic!("Invalid action taken"), + } + compare_state(&test_state, &app, &(s.value.clone())); + println!( + "clock is advancing for {} seconds", + TICK + ); + app.update_block(|block| { + block.time = block.time.plus_seconds(TICK); + }); + println!("-----------------------------------"); + } + } +}