Improve formatting and print expected result from trace on generated …

…tests
informalsystems · May 27, 2024 · 27fad74 · 27fad74
1 parent 77db3a0
commit 27fad74
Show file tree

Hide file tree

Showing 13 changed files with 519 additions and 130 deletions.
diff --git a/src/boilerplate.rs b/src/boilerplate.rs
@@ -161,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"

diff --git a/src/test_generation/boilerplate.rs b/src/test_generation/boilerplate.rs
@@ -4,7 +4,7 @@ pub fn test_header(crate_name: &str) -> String {
 #[cfg(test)]
 pub mod tests {{
     use {crate_name}::contract;
-    use {crate_name}::msg::{{ExecuteMsg, InstantiateMsg, QueryMsg}};
+    use {crate_name}::msg::{{ExecuteMsg, InstantiateMsg}};
 
 {TEST_AUX}
 "
@@ -124,6 +124,7 @@ const TEST_AUX: &str = "
             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() {
 ";
@@ -194,10 +195,24 @@ pub const STRUCTS_MODULE_IMPORTS: &str = "use num_bigint::BigInt;
 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<BigInt>),
+    }
 
     #[derive(Clone, Debug, Deserialize)]
     pub struct Response {
         pub messages: Vec<Message>,
+        pub attributes: Vec<Attribute>,
     }
 
     #[derive(Clone, Debug, Deserialize)]

diff --git 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/tests/snapshots/integration_tests__ctf01.snap b/tests/snapshots/integration_tests__ctf01.snap
@@ -34,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
@@ -48,7 +56,11 @@ 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
@@ -63,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()
   }
 
@@ -79,11 +91,9 @@ 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 } }
@@ -200,10 +210,24 @@ pub mod state_structs {
 
     #[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<BigInt>),
+    }
 
     #[derive(Clone, Debug, Deserialize)]
     pub struct Response {
         pub messages: Vec<Message>,
+        pub attributes: Vec<Attribute>,
     }
 
     #[derive(Clone, Debug, Deserialize)]
@@ -222,7 +246,7 @@ pub mod state_structs {
 #[cfg(test)]
 pub mod tests {
     use oaksecurity_cosmwasm_ctf_01::contract;
-    use oaksecurity_cosmwasm_ctf_01::msg::{ExecuteMsg, InstantiateMsg, QueryMsg};
+    use oaksecurity_cosmwasm_ctf_01::msg::{ExecuteMsg, InstantiateMsg};
 
 
     use crate::state_structs::*;
@@ -337,6 +361,7 @@ pub mod tests {
             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() {
 

diff --git a/tests/snapshots/integration_tests__ctf02.snap b/tests/snapshots/integration_tests__ctf02.snap
@@ -36,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
@@ -52,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
@@ -61,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
@@ -70,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
@@ -87,7 +107,7 @@ module oaksecurity_cosmwasm_ctf_02 {
   }
 
   pure val init_contract_state = {
-        voting_power: Map()
+    voting_power: Map()
   }
 
   action execute_step = all {
@@ -100,11 +120,9 @@ 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 } }
@@ -225,10 +243,24 @@ pub mod state_structs {
 
     #[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<BigInt>),
+    }
 
     #[derive(Clone, Debug, Deserialize)]
     pub struct Response {
         pub messages: Vec<Message>,
+        pub attributes: Vec<Attribute>,
     }
 
     #[derive(Clone, Debug, Deserialize)]
@@ -247,7 +279,7 @@ pub mod state_structs {
 #[cfg(test)]
 pub mod tests {
     use oaksecurity_cosmwasm_ctf_02::contract;
-    use oaksecurity_cosmwasm_ctf_02::msg::{ExecuteMsg, InstantiateMsg, QueryMsg};
+    use oaksecurity_cosmwasm_ctf_02::msg::{ExecuteMsg, InstantiateMsg};
 
 
     use crate::state_structs::*;
@@ -362,6 +394,7 @@ pub mod tests {
             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() {