fix: invariant func type params (#309)

* fix: invariant func type params

* cleanup

* fixed useless code

* cleanup

* feat: simplify

* feat: removed clone

* feat: cleanup

Author: andrii-a8c

crates/move-stackless-bytecode/src/mono_analysis.rs

@@ -374,6 +374,8 @@ impl Analyzer<'_> {
             }
         }
 
+        self.analyze_type_invariant_functions();
+
         // Next do todo-list for regular functions, while self.inst_opt contains the
         // specific instantiation.
         while let Some((fun, variant, inst)) = self.todo_funs.pop() {
@@ -608,6 +610,25 @@ impl Analyzer<'_> {
         }
     }
 
+    fn analyze_type_invariant_functions(&mut self) {
+        let items_to_process: Vec<_> = self
+            .info
+            .structs
+            .iter()
+            .filter_map(|(struct_qid, type_instantiations)| {
+                self.targets
+                    .get_inv_by_datatype(struct_qid)
+                    .map(|inv_fun_qid| (*inv_fun_qid, type_instantiations.clone()))
+            })
+            .collect();
+
+        for (inv_fun_qid, type_instantiations) in items_to_process {
+            for type_inst in type_instantiations.iter() {
+                self.push_todo_fun(inv_fun_qid, type_inst.clone());
+            }
+        }
+    }
+
     // Expression and Spec Fun Analysis
     // --------------------------------
 

crates/sui-prover/tests/inputs/inv/inv_type_detection.move

@@ -0,0 +1,116 @@
+module 0x42::inv_types_detection;
+
+use sui::balance::{Self, Balance};
+use sui::sui::SUI;
+use sui::table::{Self, Table};
+
+public struct StakingPool has key, store {
+    id: UID,
+    activation_epoch: Option<u64>,
+    deactivation_epoch: Option<u64>,
+    sui_balance: u64,
+    rewards_pool: Balance<SUI>,
+    pool_token_balance: u64,
+    exchange_rates: Table<u64, PoolTokenExchangeRate>,
+    pending_stake: u64,
+    pending_total_sui_withdraw: u64,
+    pending_pool_token_withdraw: u64,
+}
+
+public struct PoolTokenExchangeRate has store, copy, drop {
+    sui_amount: u64,
+    pool_token_amount: u64,
+}
+
+public struct StakedSui has key, store {
+    id: UID,
+    pool_id: ID,
+    stake_activation_epoch: u64,
+}
+
+public(package) fun new(ctx: &mut TxContext): StakingPool {
+    let exchange_rates = table::new(ctx);
+    StakingPool {
+        id: object::new(ctx),
+        activation_epoch: option::none(),
+        deactivation_epoch: option::none(),
+        sui_balance: 0,
+        rewards_pool: balance::zero(),
+        pool_token_balance: 0,
+        exchange_rates,
+        pending_stake: 0,
+        pending_total_sui_withdraw: 0,
+        pending_pool_token_withdraw: 0,
+    }
+}
+
+public fun is_preactive(pool: &StakingPool): bool{
+    pool.activation_epoch.is_none()
+}
+
+public fun is_equal_staking_metadata(self: &StakedSui, other: &StakedSui): bool {
+    (self.pool_id == other.pool_id) &&
+    (self.stake_activation_epoch == other.stake_activation_epoch)
+}
+
+public fun pool_token_exchange_rate_at_epoch(pool: &StakingPool, epoch: u64): PoolTokenExchangeRate {
+    if (is_preactive_at_epoch(pool, epoch)) {
+        return initial_exchange_rate()
+    };
+    let clamped_epoch = pool.deactivation_epoch.get_with_default(epoch);
+    let mut epoch = clamped_epoch.min(epoch);
+    let activation_epoch = *pool.activation_epoch.borrow();
+    while (epoch >= activation_epoch) {
+        if (pool.exchange_rates.contains(epoch)) {
+            return pool.exchange_rates[epoch]
+        };
+        epoch = epoch - 1;
+    };
+    initial_exchange_rate()
+}
+
+fun is_preactive_at_epoch(pool: &StakingPool, epoch: u64): bool{
+    is_preactive(pool) || (*pool.activation_epoch.borrow() > epoch)
+}
+
+fun initial_exchange_rate(): PoolTokenExchangeRate {
+    PoolTokenExchangeRate { sui_amount: 0, pool_token_amount: 0 }
+}
+
+#[spec_only]
+use prover::prover::requires;
+
+#[spec(prove, no_opaque)]
+public fun is_equal_staking_metadata_spec(self: &StakedSui, other: &StakedSui): bool {
+    is_equal_staking_metadata(self, other)
+}
+
+#[spec_only]
+public fun activation_epoch_is_positive(pool: &StakingPool): bool {
+    pool.activation_epoch.is_some() &&
+    *pool.activation_epoch.borrow() > 0
+}
+
+#[spec()]
+public fun pool_token_exchange_rate_at_epoch_spec(
+    pool: &StakingPool,
+    epoch: u64,
+): PoolTokenExchangeRate {
+    requires(! pool.is_preactive());
+    requires(activation_epoch_is_positive(pool));
+    pool_token_exchange_rate_at_epoch(pool, epoch)
+}
+
+
+#[spec_only(inv_target=std::option::Option)]
+fun Option_inv<T>(self: &Option<T>): bool {
+    if (self.is_some()) {
+        let o = prover::prover::val(self.borrow());
+        let x = std::option::some(o);
+        let b = self == x;
+        prover::prover::drop(x);
+        b
+    } else {
+        true
+    }
+}

crates/sui-prover/tests/snapshots/inv/inv_type_detection.move.snap

@@ -0,0 +1,6 @@
+---
+source: crates/sui-prover/tests/integration.rs
+assertion_line: 270
+expression: output
+---
+Verification successful