diff --git a/src/boilerplate.rs b/src/boilerplate.rs index dae6a0c..9e39a9a 100644 --- a/src/boilerplate.rs +++ b/src/boilerplate.rs @@ -87,7 +87,7 @@ pub fn initializers(ctx: &Context) -> String { " pure val init_bank_state = ADDRESSES.mapBy(_ => DENOMS.mapBy(_ => MAX_AMOUNT)) - val env_val = {{ block: {{ time: time }} }} + val env_val = {{ block: {{ time: time, height: 1 }} }} // TODO: Add a height var if you need it action init = {{ // TODO: Change next line according to fund expectations @@ -100,7 +100,7 @@ pub fn initializers(ctx: &Context) -> String { val info = {{ sender: sender, funds: funds }} pure val message: InstantiateMsg = {} - pure val r = instantiate(init_contract_state, {{ block: {{ time: 0 }} }}, info, message) + pure val r = instantiate(init_contract_state, {{ block: {{ time: 0, height: 1 }} }}, info, message) all {{ contract_state' = r._2, @@ -126,9 +126,14 @@ pub fn init_value_for_type(ctx: &Context, ty: String) -> String { return "[]".to_string(); } - if ctx.structs.contains_key(&ty) { + if ty.starts_with("Option") { + return "None".to_string(); + } + + let typ = ty.split('[').next().unwrap(); + if ctx.structs.contains_key(typ) { // Type is a struct, initialize fields recursively - let fields = ctx.structs.get(&ty).unwrap(); + let fields = ctx.structs.get(typ).unwrap(); let struct_value = fields .iter() .map(|field| { @@ -139,17 +144,17 @@ pub fn init_value_for_type(ctx: &Context, ty: String) -> String { ) }) .collect_vec() - .join(","); + .join(", "); return format!("{{ {} }}", struct_value); } - match ty.as_str() { + match typ { "str" => "\"\"".to_string(), "int" => "0".to_string(), "Addr" => "\"s1\"".to_string(), _ => { eprintln!("No init value for type: {ty}"); - "".to_string() + "\"\"".to_string() } } } @@ -195,7 +200,7 @@ pub fn post_items(ctx: &Context) -> String { {contract_state} }} - pure val init_contract_state = {{ + pure val init_contract_state: ContractState = {{ {initializer} }} diff --git a/src/lib.rs b/src/lib.rs index 8345b58..fd09d43 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -155,10 +155,13 @@ fn translate_items(tcx: TyCtxt, crate_name: &str, items: Vec<&rustc_hir::Item>) ("denom".to_string(), "str".to_string()), ("amount".to_string(), "int".to_string()), ], + enums: HashMap::new(), + type_aliases: HashMap::new(), // scoped record_fields: vec![], struct_fields: vec![], pat_fields: vec![], + generics: vec![], current_item_name: "".to_string(), }; diff --git a/src/nondet.rs b/src/nondet.rs index 60b111c..c2aea90 100644 --- a/src/nondet.rs +++ b/src/nondet.rs @@ -69,7 +69,7 @@ fn missing_nondet_value( kind: &str, ) -> String { eprintln!("No nondet value for {}: {:?}", kind, item.translate(ctx)); - "".to_string() + "\"\"".to_string() } fn nondet_value_for_list(ty: &rustc_hir::Ty<'_>, ctx: &mut Context, ident: &str) -> NondetInfo { @@ -187,6 +187,19 @@ impl NondetValue for rustc_hir::PathSegment<'_> { return fields.nondet_info(ctx, ident); } + // If the type refers to an enum, get the first variant and generate a nondet value for it + if ctx.enums.contains_key(&translated_type) { + let variants = ctx.enums[&translated_type].clone(); + let variant = variants[0].clone(); + return self.nondet_info(ctx, variant.as_str()); + } + + // If the type refers to a type alias, generate a nondet value for the type alias + if ctx.type_aliases.contains_key(&translated_type) { + let alias = ctx.type_aliases[&translated_type].clone(); + return self.nondet_info(ctx, alias.as_str()); + } + // If the type refers to a primitive type, generate a nondet value for the primitive type let value = match translated_type.as_str() { "str" | "Addr" => "Set(\"s1\", \"s2\", \"s3\")".to_string(), diff --git a/src/quint-lib-files/cw_types.qnt b/src/quint-lib-files/cw_types.qnt index 38614a1..45f1f43 100644 --- a/src/quint-lib-files/cw_types.qnt +++ b/src/quint-lib-files/cw_types.qnt @@ -65,7 +65,7 @@ module cw_types { gas_limit: None, } - pure def SubMsg_reply_on_sucess(msg: CosmosMsg, id: int): SubMsg = { + pure def SubMsg_reply_on_success(msg: CosmosMsg, id: int): SubMsg = { __reply_on(msg, id, ReplyOn_Success) } @@ -133,7 +133,8 @@ module cw_types { querier: TODO, } - type Env = { block: { time: int /*, height: int */ } } // TODO + type BlockInfo = { time: int, height: int } + type Env = { block: BlockInfo } type Coin = { denom: str, @@ -149,4 +150,16 @@ module cw_types { | FromStr(str) | FromInt(int) | FromListInt(List[int]) + + // These shouldn't be actually used, but they are here for completion + type MultiIndex[ik, t, pk] = () + type IndexedMap[k, t i] = () + + type StdError = str + type StdResult[a] = Result[a, StdError] + + // There's no dynamic dispatch in Quint, so the best we can do is to have a + // special string argument to identify a behavior and then have the + // implementation depend on it + type TraitObject = str } diff --git a/src/quint-lib-files/cw_utils.qnt b/src/quint-lib-files/cw_utils.qnt index e662dbe..8e7d7a5 100644 --- a/src/quint-lib-files/cw_utils.qnt +++ b/src/quint-lib-files/cw_utils.qnt @@ -4,6 +4,19 @@ module cw_utils { import cw_types.* from "./cw_types" + type Expiration = + // AtHeight will expire when `env.block.height` >= height + | Expiration_AtHeight(int) + // AtTime will expire when `env.block.time` >= time + | Expiration_AtTime(int) + // Never will never expire. Used to express the empty variant + | Expiration_Never + + type Duration = + | Duration_Height(int) + // Time in seconds + | Duration_Time(int) + def one_coin(info: MessageInfo): Result[Coin, ContractError] = { if (info.funds.indices().size() == 0) { Err("No funds") diff --git a/src/state_extraction.rs b/src/state_extraction.rs index 4949c83..58925d6 100644 --- a/src/state_extraction.rs +++ b/src/state_extraction.rs @@ -1,7 +1,9 @@ use itertools::Itertools; +use regex::Regex; use rustc_span::{symbol::Ident, Symbol}; use crate::{translate::Translatable, types::Context}; +extern crate regex; // State extraction is the only place where we need to deal with // rustc_middle::ty::Ty. This is the type given by typeck, which is the only way @@ -11,19 +13,30 @@ use crate::{translate::Translatable, types::Context}; impl Translatable for rustc_middle::ty::Ty<'_> { fn translate(&self, ctx: &mut Context) -> String { // FIXME: This should be quite unstable, but I couldn't figure out how to navigate `ty` here + let var_name = &format!("{:#?}", self); - let name = var_name - .split("::") - .last() - .unwrap() + let name_core = var_name + .clone() .split(' ') .last() .unwrap() .split(')') .next() - .unwrap(); + .unwrap() + .to_string(); + + // The name_core can look like namespace::namespace::type + // The following regex replacement has the goal of transforming it into type + let re = Regex::new(r"(\w+::)*(\w+)(<(\w+::)*(\w+)>)?").unwrap(); + let name = re.replace(name_core.as_str(), |caps: ®ex::Captures| { + if let Some(m) = caps.get(5) { + format!("{}[{}]", &caps[2], m.as_str()) + } else { + caps[2].to_string() + } + }); - Ident::with_dummy_span(Symbol::intern(name)).translate(ctx) + Ident::with_dummy_span(Symbol::intern(name.to_string().as_str())).translate(ctx) } } impl Translatable for rustc_middle::ty::GenericArg<'_> { diff --git a/src/translate.rs b/src/translate.rs index 9dd4d5f..0a90399 100644 --- a/src/translate.rs +++ b/src/translate.rs @@ -1,4 +1,4 @@ -use std::{collections::HashMap, fmt::Debug}; +use std::fmt::Debug; use itertools::Itertools; use rustc_span::symbol::Ident; @@ -18,6 +18,7 @@ pub fn translate_list(items: &[T], ctx: &mut Context, sep: &str items .iter() .map(|x| x.translate(ctx)) + .filter(|x| !x.is_empty()) .collect_vec() .join(sep) } @@ -28,31 +29,33 @@ pub fn missing_translation(item: T, descr: &str) -> Str } impl Translatable for Ident { - fn translate(&self, _ctx: &mut Context) -> String { - // FIXME: this should be a map - let translated_segments: &HashMap<&str, &str> = &HashMap::from([ - ("Vec", "List"), - ("String", "str"), - ("Uint128", "int"), - ("Uint64", "int"), - ("Uint32", "int"), - ("u128", "int"), - ("u64", "int"), - ("u32", "int"), - ("i128", "int"), - ("i64", "int"), - ("i32", "int"), - ("Decimal", "int"), - ("Timestamp", "int"), - ("DepsMut", "ContractStateMut"), // Not an actual translation, but a placeholder - ("Deps", "ContractState"), - ("Ok", "Ok"), - ("deps", "state"), - ("_deps", "state"), - ]); - - let s = self.as_str(); - translated_segments.get(s).unwrap_or(&s).to_string() + fn translate(&self, ctx: &mut Context) -> String { + const QUINT_KEYWORDS: [&str; 31] = [ + "Set", "List", "Rec", "Tup", "not", "and", "or", "iff", "implies", "all", "any", "if", + "else", "module", "import", "from", "export", "as", "const", "var", "def", "val", + "pure", "nondet", "action", "temporal", "assume", "type", "Bool", "Int", "Nat", + ]; + let name_with_underscore = format!("{}_", self); + let lowercase_name = self.as_str().to_lowercase(); + + let translated_str = match self.as_str() { + "Vec" => "List", + "String" => "str", + "Uint128" | "Uint64" | "Uint32" | "u128" | "u64" | "u32" | "i128" | "i64" | "i32" => { + "int" + } + "Decimal" => "int", + "Timestamp" => "int", + "Deps" => "ContractState", + "DepsMut" => "ContractStateMut", // Not an actual translation, but a placeholder + "deps" => "state", + "_deps" => "state", + s if QUINT_KEYWORDS.contains(&s) => name_with_underscore.as_str(), + s if ctx.generics.contains(&s.to_string()) => lowercase_name.as_str(), + s => s, + }; + + translated_str.to_string() } } @@ -82,6 +85,8 @@ impl Translatable for rustc_hir::QPath<'_> { rustc_hir::QPath::TypeRelative(ty, segment) => { format!("{}_{}", ty.translate(ctx), segment.translate(ctx)) } + // Question mark operator, remove them for now + rustc_hir::QPath::LangItem(rustc_hir::LangItem::TryTraitBranch, _) => "".to_string(), _ => missing_translation(*self, "qualified-path"), } } @@ -109,7 +114,19 @@ impl Translatable for rustc_hir::Ty<'_> { ); t } - _ => missing_translation(*self, "type"), + rustc_hir::TyKind::TraitObject(_refs, _, _) => { + // Getting trait identifier (not very useful in Quint): + // refs[0].trait_ref.path.segments[0].ident.translate(ctx) + + // There's no dynamic dispatch in Quint, so the best we can do + // is to have a special string argument to identify a behavior + // and then have the implementation depend on it + "TraitObject".to_string() + } + _ => { + eprintln!("No translation for type: {:#?}", *self); + "MissingType".to_string() + } } } } @@ -125,7 +142,7 @@ impl Translatable for rustc_hir::Param<'_> { impl Translatable for rustc_hir::Pat<'_> { fn translate(&self, ctx: &mut Context) -> String { match self.kind { - rustc_hir::PatKind::Binding(_a, _id, name, _n) => name.as_str().to_string(), + rustc_hir::PatKind::Binding(_a, _id, name, _n) => name.translate(ctx), rustc_hir::PatKind::Path(qpath) => qpath.translate(ctx), rustc_hir::PatKind::Struct(qpath, pat_fields, _) => { // TODO: raise error if pat != field (I think this is matching for {field_ident: field_pat}) @@ -133,7 +150,7 @@ impl Translatable for rustc_hir::Pat<'_> { let fields = pat_fields .iter() - .map(|field| field.ident.to_string()) + .map(|field| field.ident.translate(ctx)) .collect_vec(); ctx.pat_fields.extend(fields.clone()); @@ -236,10 +253,10 @@ impl Translatable for rustc_hir::Expr<'_> { rustc_hir::ExprKind::Tup(exprs) => format!("({})", translate_list(exprs, ctx, ", ")), rustc_hir::ExprKind::Struct(_, expr_fields, base) => { let translated_base = base - .map(|e| format!("... {}", e.translate(ctx))) + .map(|e| format!("... {},", e.translate(ctx))) .unwrap_or("".to_string()); let record_fields = translate_list(expr_fields, ctx, ", "); - format!("{{ {} }}", [translated_base, record_fields].join(", ")) + format!("{{ {} }}", [translated_base, record_fields].join("")) } rustc_hir::ExprKind::Block(block, _label) => match block.expr { Some(expr) => expr.translate(ctx), @@ -331,7 +348,7 @@ impl Translatable for rustc_hir::VariantData<'_> { let translated_fields = fields .iter() .map(|field| { - let field_ident = field.ident.to_string(); + let field_ident = field.ident.translate(ctx); Field { name: field_ident.clone(), ty: field.ty.translate(ctx), @@ -390,6 +407,13 @@ impl Translatable for rustc_hir::EnumDef<'_> { if self.variants.is_empty() { return "{}".to_string(); } + ctx.enums.insert( + ctx.current_item_name.to_string(), + self.variants + .iter() + .map(|x| x.ident.to_string()) + .collect_vec(), + ); translate_list(self.variants, ctx, "\n") } @@ -460,6 +484,11 @@ impl Translatable for Function<'_> { return "".to_string(); } + if output.starts_with("IndexedMap") || output.starts_with("MultiIndex") { + // These won't be useful in the Quint model, ignore them + return "".to_string(); + } + if has_mutability { ctx.ops_with_mutability.push(ctx.current_item_name.clone()); @@ -470,6 +499,34 @@ impl Translatable for Function<'_> { } } +impl Translatable for rustc_hir::GenericParam<'_> { + fn translate(&self, ctx: &mut Context) -> String { + match self.name { + rustc_hir::ParamName::Plain(ident) => { + let name = ident.translate(ctx); + if name.starts_with('\'') { + // Lifetime, ignore it + return "".to_string(); + } + ctx.generics.push(name.clone()); + name.to_lowercase() + } + _ => "".to_string(), + } + } +} + +impl Translatable for rustc_hir::Generics<'_> { + fn translate(&self, ctx: &mut Context) -> String { + let type_args = translate_list(self.params, ctx, ", "); + if type_args.is_empty() { + "".to_string() + } else { + format!("[{type_args}]") + } + } +} + impl Translatable for rustc_hir::Item<'_> { fn translate(&self, ctx: &mut Context) -> String { let name = self.ident.as_str(); @@ -573,21 +630,31 @@ impl Translatable for rustc_hir::Item<'_> { }}" ) } - rustc_hir::ItemKind::Struct(variant_data, _generics) => { + rustc_hir::ItemKind::Struct(variant_data, generics) => { + let type_args = generics.translate(ctx); let translated_fields = variant_data.translate(ctx); let fields = ctx.struct_fields.clone(); ctx.struct_fields.clear(); + ctx.generics.clear(); ctx.structs.insert(name.to_string(), fields); - format!(" type {name} = {translated_fields}") + format!(" type {name}{type_args} = {translated_fields}") } - rustc_hir::ItemKind::Enum(enum_def, _generics) => { - format!(" type {name} =\n{}", enum_def.translate(ctx)) + rustc_hir::ItemKind::Enum(enum_def, generics) => { + let type_args = generics.translate(ctx); + let enum_variants = enum_def.translate(ctx); + ctx.generics.clear(); + format!(" type {name}{type_args} =\n{enum_variants}",) } - rustc_hir::ItemKind::TyAlias(ty, _generics) => { - format!(" type {name} = {}", ty.translate(ctx)) + rustc_hir::ItemKind::TyAlias(ty, generics) => { + let type_args = generics.translate(ctx); + let translated_type = ty.translate(ctx); + ctx.type_aliases + .insert(name.to_string(), translated_type.clone()); + ctx.generics.clear(); + format!(" type {name}{type_args} = {translated_type}") } // FIXME: We should translate this (at least Use) into imports. // This is only necessary for crates that import things from other crates diff --git a/src/types.rs b/src/types.rs index ad1637f..d189157 100644 --- a/src/types.rs +++ b/src/types.rs @@ -38,12 +38,15 @@ pub struct Context<'tcx, 'c> { pub tcx: TyCtxt<'tcx>, pub contract_state: Vec<(String, String)>, pub nondet_picks: Vec<(String, String)>, + pub enums: HashMap>, + pub type_aliases: HashMap, // scoped // FIXME: This should be a stack to account for nested scopes. // No need to worry about nested scopes for stub generation. pub record_fields: Vec, pub struct_fields: Vec, pub pat_fields: Vec, + pub generics: Vec, pub current_item_name: String, } diff --git a/tests/integration_tests.rs b/tests/integration_tests.rs index e6a8297..c3624ab 100644 --- a/tests/integration_tests.rs +++ b/tests/integration_tests.rs @@ -36,6 +36,8 @@ fn run(dir: &str, f: impl FnOnce(&mut Command)) -> Result { f(&mut cmd); let _ = fs::remove_dir_all(ws.join("target")); + let _ = fs::remove_dir_all(ws.join("quint")); + let _ = fs::remove_dir_all(ws.join("tests")); let output = cmd.output().context("Process failed")?; ensure!( diff --git a/tests/snapshots/integration_tests__ctf01.snap b/tests/snapshots/integration_tests__ctf01.snap index 1baa8cb..a8b6634 100644 --- a/tests/snapshots/integration_tests__ctf01.snap +++ b/tests/snapshots/integration_tests__ctf01.snap @@ -78,7 +78,7 @@ module oaksecurity_cosmwasm_ctf_01 { lockups: int -> Lockup } - pure val init_contract_state = { + pure val init_contract_state: ContractState = { last_id: 0, lockups: Map() } @@ -96,7 +96,7 @@ module oaksecurity_cosmwasm_ctf_01 { pure val init_bank_state = ADDRESSES.mapBy(_ => DENOMS.mapBy(_ => MAX_AMOUNT)) - val env_val = { block: { time: time } } + val env_val = { block: { time: time, height: 1 } } // TODO: Add a height var if you need it action init = { // TODO: Change next line according to fund expectations @@ -109,7 +109,7 @@ module oaksecurity_cosmwasm_ctf_01 { val info = { sender: sender, funds: funds } pure val message: InstantiateMsg = { count: 0 } - pure val r = instantiate(init_contract_state, { block: { time: 0 } }, info, message) + pure val r = instantiate(init_contract_state, { block: { time: 0, height: 1 } }, info, message) all { contract_state' = r._2, diff --git a/tests/snapshots/integration_tests__ctf02.snap b/tests/snapshots/integration_tests__ctf02.snap index 88f4efe..eebedd7 100644 --- a/tests/snapshots/integration_tests__ctf02.snap +++ b/tests/snapshots/integration_tests__ctf02.snap @@ -106,7 +106,7 @@ module oaksecurity_cosmwasm_ctf_02 { voting_power: Addr -> UserInfo } - pure val init_contract_state = { + pure val init_contract_state: ContractState = { voting_power: Map() } @@ -125,7 +125,7 @@ module oaksecurity_cosmwasm_ctf_02 { pure val init_bank_state = ADDRESSES.mapBy(_ => DENOMS.mapBy(_ => MAX_AMOUNT)) - val env_val = { block: { time: time } } + val env_val = { block: { time: time, height: 1 } } // TODO: Add a height var if you need it action init = { // TODO: Change next line according to fund expectations @@ -138,7 +138,7 @@ module oaksecurity_cosmwasm_ctf_02 { val info = { sender: sender, funds: funds } pure val message: InstantiateMsg = { } - pure val r = instantiate(init_contract_state, { block: { time: 0 } }, info, message) + pure val r = instantiate(init_contract_state, { block: { time: 0, height: 1 } }, info, message) all { contract_state' = r._2, diff --git a/tests/snapshots/integration_tests__ctf03.snap b/tests/snapshots/integration_tests__ctf03.snap index 696818a..6283b3d 100644 --- a/tests/snapshots/integration_tests__ctf03.snap +++ b/tests/snapshots/integration_tests__ctf03.snap @@ -112,9 +112,9 @@ module flash_loan { flash_loan: FlashLoanState } - pure val init_contract_state = { - config: , - flash_loan: + pure val init_contract_state: ContractState = { + config: "", + flash_loan: "" } action execute_step = all { @@ -133,7 +133,7 @@ module flash_loan { pure val init_bank_state = ADDRESSES.mapBy(_ => DENOMS.mapBy(_ => MAX_AMOUNT)) - val env_val = { block: { time: time } } + val env_val = { block: { time: time, height: 1 } } // TODO: Add a height var if you need it action init = { // TODO: Change next line according to fund expectations @@ -145,8 +145,8 @@ module flash_loan { 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) + pure val message: InstantiateMsg = "" + pure val r = instantiate(init_contract_state, { block: { time: 0, height: 1 } }, info, message) all { contract_state' = r._2, @@ -254,8 +254,8 @@ module mock_arb { config: Config } - pure val init_contract_state = { - config: + pure val init_contract_state: ContractState = { + config: "" } action execute_step = all { @@ -270,7 +270,7 @@ module mock_arb { pure val init_bank_state = ADDRESSES.mapBy(_ => DENOMS.mapBy(_ => MAX_AMOUNT)) - val env_val = { block: { time: time } } + val env_val = { block: { time: time, height: 1 } } // TODO: Add a height var if you need it action init = { // TODO: Change next line according to fund expectations @@ -282,8 +282,8 @@ module mock_arb { 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) + pure val message: InstantiateMsg = "" + pure val r = instantiate(init_contract_state, { block: { time: 0, height: 1 } }, info, message) all { contract_state' = r._2, @@ -389,8 +389,8 @@ module proxy { config: Config } - pure val init_contract_state = { - config: + pure val init_contract_state: ContractState = { + config: "" } action execute_step = all { @@ -405,7 +405,7 @@ module proxy { pure val init_bank_state = ADDRESSES.mapBy(_ => DENOMS.mapBy(_ => MAX_AMOUNT)) - val env_val = { block: { time: time } } + val env_val = { block: { time: time, height: 1 } } // TODO: Add a height var if you need it action init = { // TODO: Change next line according to fund expectations @@ -417,8 +417,8 @@ module proxy { 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) + pure val message: InstantiateMsg = "" + pure val r = instantiate(init_contract_state, { block: { time: 0, height: 1 } }, info, message) all { contract_state' = r._2, diff --git a/tests/snapshots/integration_tests__ctf04.snap b/tests/snapshots/integration_tests__ctf04.snap index 438f2cb..b4d3bff 100644 --- a/tests/snapshots/integration_tests__ctf04.snap +++ b/tests/snapshots/integration_tests__ctf04.snap @@ -77,7 +77,7 @@ module oaksecurity_cosmwasm_ctf_04 { balances: Addr -> Balance } - pure val init_contract_state = { + pure val init_contract_state: ContractState = { config: { total_supply: 0 }, balances: Map() } @@ -95,7 +95,7 @@ module oaksecurity_cosmwasm_ctf_04 { pure val init_bank_state = ADDRESSES.mapBy(_ => DENOMS.mapBy(_ => MAX_AMOUNT)) - val env_val = { block: { time: time } } + val env_val = { block: { time: time, height: 1 } } // TODO: Add a height var if you need it action init = { // TODO: Change next line according to fund expectations @@ -108,7 +108,7 @@ module oaksecurity_cosmwasm_ctf_04 { val info = { sender: sender, funds: funds } pure val message: InstantiateMsg = { offset: 0 } - pure val r = instantiate(init_contract_state, { block: { time: 0 } }, info, message) + pure val r = instantiate(init_contract_state, { block: { time: 0, height: 1 } }, info, message) all { contract_state' = r._2, diff --git a/tests/snapshots/integration_tests__ctf05.snap b/tests/snapshots/integration_tests__ctf05.snap index c6247ee..8d3510c 100644 --- a/tests/snapshots/integration_tests__ctf05.snap +++ b/tests/snapshots/integration_tests__ctf05.snap @@ -86,7 +86,7 @@ module oaksecurity_cosmwasm_ctf_05 { action owner_action_action = { // TODO: Change next line according to fund expectations pure val max_funds = MAX_AMOUNT - nondet message_msg: CosmosMsg = .oneOf() + nondet message_msg: CosmosMsg = "".oneOf() pure val message: ExecuteMsg = ExecuteMsg_OwnerAction({ msg: message_msg }) execute_message(message, max_funds) } @@ -129,7 +129,7 @@ module oaksecurity_cosmwasm_ctf_05 { pure val message: ExecuteMsg = ExecuteMsg_DropOwnershipProposal execute_message(message, max_funds) } - pure def assert_owner(store: , sender: Addr): Result[(), ContractError] = Ok(()) + pure def assert_owner(store: TraitObject, sender: Addr): Result[(), ContractError] = Ok(()) pure val DENOM = "uawesome" type ContractState = { @@ -137,8 +137,8 @@ module oaksecurity_cosmwasm_ctf_05 { balances: Addr -> int } - pure val init_contract_state = { - state: { current_owner: "s1",proposed_owner: }, + pure val init_contract_state: ContractState = { + state: { current_owner: "s1", proposed_owner: None }, balances: Map() } @@ -159,7 +159,7 @@ module oaksecurity_cosmwasm_ctf_05 { pure val init_bank_state = ADDRESSES.mapBy(_ => DENOMS.mapBy(_ => MAX_AMOUNT)) - val env_val = { block: { time: time } } + val env_val = { block: { time: time, height: 1 } } // TODO: Add a height var if you need it action init = { // TODO: Change next line according to fund expectations @@ -172,7 +172,7 @@ module oaksecurity_cosmwasm_ctf_05 { val info = { sender: sender, funds: funds } pure val message: InstantiateMsg = { owner: "" } - pure val r = instantiate(init_contract_state, { block: { time: 0 } }, info, message) + pure val r = instantiate(init_contract_state, { block: { time: 0, height: 1 } }, info, message) all { contract_state' = r._2, diff --git a/tests/snapshots/integration_tests__ctf06.snap b/tests/snapshots/integration_tests__ctf06.snap index 5cef446..c44ca19 100644 --- a/tests/snapshots/integration_tests__ctf06.snap +++ b/tests/snapshots/integration_tests__ctf06.snap @@ -35,7 +35,7 @@ module oaksecurity_cosmwasm_ctf_06 { type ExecuteMsg = | ExecuteMsg_Propose | ExecuteMsg_ResolveProposal - | ExecuteMsg_OwnerAction({ action: CosmosMsg }) + | ExecuteMsg_OwnerAction({ action_: CosmosMsg }) | ExecuteMsg_Receive(Cw20ReceiveMsg) type Cw20HookMsg = | Cw20HookMsg_CastVote @@ -47,7 +47,7 @@ module oaksecurity_cosmwasm_ctf_06 { 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_OwnerAction(__r) => owner_action(state, info, __r.action_) | ExecuteMsg_Receive(msg) => receive_cw20(state, env, info, msg) } @@ -98,8 +98,8 @@ module oaksecurity_cosmwasm_ctf_06 { action owner_action_action = { // TODO: Change next line according to fund expectations pure val max_funds = MAX_AMOUNT - nondet message_action: CosmosMsg = .oneOf() - pure val message: ExecuteMsg = ExecuteMsg_OwnerAction({ action: message_action }) + nondet message_action_: CosmosMsg = "".oneOf() + pure val message: ExecuteMsg = ExecuteMsg_OwnerAction({ action_: message_action_ }) execute_message(message, max_funds) } pure val DENOM = "uawesome" @@ -109,9 +109,9 @@ module oaksecurity_cosmwasm_ctf_06 { proposal: Proposal } - pure val init_contract_state = { - config: { voting_window: 0,voting_token: "s1",owner: "s1" }, - proposal: { proposer: "s1",timestamp: 0 } + pure val init_contract_state: ContractState = { + config: { voting_window: 0, voting_token: "s1", owner: "s1" }, + proposal: { proposer: "s1", timestamp: 0 } } action execute_step = all { @@ -129,7 +129,7 @@ module oaksecurity_cosmwasm_ctf_06 { pure val init_bank_state = ADDRESSES.mapBy(_ => DENOMS.mapBy(_ => MAX_AMOUNT)) - val env_val = { block: { time: time } } + val env_val = { block: { time: time, height: 1 } } // TODO: Add a height var if you need it action init = { // TODO: Change next line according to fund expectations @@ -141,8 +141,8 @@ module oaksecurity_cosmwasm_ctf_06 { 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) + pure val message: InstantiateMsg = { token: "", owner: "", window: 0 } + pure val r = instantiate(init_contract_state, { block: { time: 0, height: 1 } }, info, message) all { contract_state' = r._2, @@ -245,7 +245,7 @@ pub mod state_structs { pub amount: Option, #[serde(with = "As::>")] - pub message_action: Option + pub message_action_: Option } #[derive(Clone, Debug, Deserialize)] @@ -444,8 +444,8 @@ pub mod tests { 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 }; + 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); diff --git a/tests/snapshots/integration_tests__ctf07.snap b/tests/snapshots/integration_tests__ctf07.snap index f4b9bb4..6a97f8b 100644 --- a/tests/snapshots/integration_tests__ctf07.snap +++ b/tests/snapshots/integration_tests__ctf07.snap @@ -95,7 +95,7 @@ module oaksecurity_cosmwasm_ctf_07 { action owner_action_action = { // TODO: Change next line according to fund expectations pure val max_funds = MAX_AMOUNT - nondet message_msg: CosmosMsg = .oneOf() + nondet message_msg: CosmosMsg = "".oneOf() pure val message: ExecuteMsg = ExecuteMsg_OwnerAction({ msg: message_msg }) execute_message(message, max_funds) } @@ -108,7 +108,7 @@ module oaksecurity_cosmwasm_ctf_07 { balances: Addr -> int } - pure val init_contract_state = { + pure val init_contract_state: ContractState = { top_depositor: "s1", owner: "s1", threshold: 0, @@ -130,7 +130,7 @@ module oaksecurity_cosmwasm_ctf_07 { pure val init_bank_state = ADDRESSES.mapBy(_ => DENOMS.mapBy(_ => MAX_AMOUNT)) - val env_val = { block: { time: time } } + val env_val = { block: { time: time, height: 1 } } // TODO: Add a height var if you need it action init = { // TODO: Change next line according to fund expectations @@ -142,8 +142,8 @@ module oaksecurity_cosmwasm_ctf_07 { 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) + pure val message: InstantiateMsg = { owner: "", threshold: 0 } + pure val r = instantiate(init_contract_state, { block: { time: 0, height: 1 } }, info, message) all { contract_state' = r._2, diff --git a/tests/snapshots/integration_tests__ctf08.snap b/tests/snapshots/integration_tests__ctf08.snap index f7c6b89..cfd6cba 100644 --- a/tests/snapshots/integration_tests__ctf08.snap +++ b/tests/snapshots/integration_tests__ctf08.snap @@ -153,11 +153,11 @@ module oaksecurity_cosmwasm_ctf_08 { operations: Operations } - pure val init_contract_state = { + pure val init_contract_state: ContractState = { config: { nft_contract: "s1" }, sales: Map(), trades: Map(), - operations: { n_trades: 0,n_sales: 0 } + operations: { n_trades: 0, n_sales: 0 } } action execute_step = all { @@ -176,7 +176,7 @@ module oaksecurity_cosmwasm_ctf_08 { pure val init_bank_state = ADDRESSES.mapBy(_ => DENOMS.mapBy(_ => MAX_AMOUNT)) - val env_val = { block: { time: time } } + val env_val = { block: { time: time, height: 1 } } // TODO: Add a height var if you need it action init = { // TODO: Change next line according to fund expectations @@ -189,7 +189,7 @@ module oaksecurity_cosmwasm_ctf_08 { val info = { sender: sender, funds: funds } pure val message: InstantiateMsg = { nft_address: "" } - pure val r = instantiate(init_contract_state, { block: { time: 0 } }, info, message) + pure val r = instantiate(init_contract_state, { block: { time: 0, height: 1 } }, info, message) all { contract_state' = r._2, diff --git a/tests/snapshots/integration_tests__ctf09.snap b/tests/snapshots/integration_tests__ctf09.snap index f591a40..0605f66 100644 --- a/tests/snapshots/integration_tests__ctf09.snap +++ b/tests/snapshots/integration_tests__ctf09.snap @@ -108,8 +108,8 @@ module oaksecurity_cosmwasm_ctf_09 { users: Addr -> UserRewardInfo } - pure val init_contract_state = { - state: { owner: "s1",total_staked: 0,global_index: 0 }, + pure val init_contract_state: ContractState = { + state: { owner: "s1", total_staked: 0, global_index: 0 }, users: Map() } @@ -128,7 +128,7 @@ module oaksecurity_cosmwasm_ctf_09 { pure val init_bank_state = ADDRESSES.mapBy(_ => DENOMS.mapBy(_ => MAX_AMOUNT)) - val env_val = { block: { time: time } } + val env_val = { block: { time: time, height: 1 } } // TODO: Add a height var if you need it action init = { // TODO: Change next line according to fund expectations @@ -141,7 +141,7 @@ module oaksecurity_cosmwasm_ctf_09 { val info = { sender: sender, funds: funds } pure val message: InstantiateMsg = { } - pure val r = instantiate(init_contract_state, { block: { time: 0 } }, info, message) + pure val r = instantiate(init_contract_state, { block: { time: 0, height: 1 } }, info, message) all { contract_state' = r._2, diff --git a/tests/snapshots/integration_tests__ctf10.snap b/tests/snapshots/integration_tests__ctf10.snap index 2c4d97c..225ad2f 100644 --- a/tests/snapshots/integration_tests__ctf10.snap +++ b/tests/snapshots/integration_tests__ctf10.snap @@ -67,8 +67,8 @@ module oaksecurity_cosmwasm_ctf_10 { whitelist: Whitelist } - pure val init_contract_state = { - config: { nft_contract: "s1",mint_per_user: 0,total_tokens: 0 }, + pure val init_contract_state: ContractState = { + config: { nft_contract: "s1", mint_per_user: 0, total_tokens: 0 }, whitelist: { users: [] } } @@ -83,7 +83,7 @@ module oaksecurity_cosmwasm_ctf_10 { pure val init_bank_state = ADDRESSES.mapBy(_ => DENOMS.mapBy(_ => MAX_AMOUNT)) - val env_val = { block: { time: time } } + val env_val = { block: { time: time, height: 1 } } // TODO: Add a height var if you need it action init = { // TODO: Change next line according to fund expectations @@ -95,8 +95,8 @@ module oaksecurity_cosmwasm_ctf_10 { 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) + pure val message: InstantiateMsg = { cw721_code_id: 0, mint_per_user: 0, whitelisted_users: [] } + pure val r = instantiate(init_contract_state, { block: { time: 0, height: 1 } }, info, message) all { contract_state' = r._2,