Formally verified
AI-generated
software

// Universal PROP-EE-003: execute blocked whenever confirmations < threshold.
property "execute blocked while confirmations < threshold"
    (threshold: u64, confirmed: u64, txId: U256) for MultisigWallet {
    assume threshold >= 1
    assume confirmed < threshold
    assume txId > 0

    // Any state with:
    //   m_threshold == threshold
    //   confirmation_count(txId) == confirmed
    //   pending (!executed) transaction txId
    call execute(txId)

    expect revert 203
}

m_transactions: HashMap<U256, Transaction> {
    in submit(to, value, data) => {
        let id = m_txCount + 1;
        let tx = Transaction { to: to, value: value, data: data, executed: false };
        m_transactions.insert(id, tx)
    }
    in execute(txId) => {
        let tx = m_transactions[txId];
        let done = tx { executed: true };
        m_transactions.update(txId, done)   // only if execute's where passed
    }
}

m_confirmations: HashMap<U256, bool> {
    in submit(_, _, _) => {
        let id = m_txCount + 1;
        m_confirmations.insert(confirmation_key(id, msg::sender), true)
    }
    in confirm(txId) => {
        m_confirmations.insert(confirmation_key(txId, msg::sender), true)
    }
    in revoke(txId) => {
        m_confirmations.remove(confirmation_key(txId, msg::sender))
    }
}

private theorem _probe_exec_fails :
    (MultisigWallet.Routes.execute _w {} Cambrian.MsgCtx.default 1).isOk = false := by
  native_decide

theorem prop_ee_003_below_threshold_execute_blocked :
  ∀ (trace : List Action),
  -- seeded: m_threshold = 3, exactly two confirmation keys, pending tx 1
  traceValid w inst ctx trace = true →
  (match runTrace w inst ctx trace with
   | .error _ => True
   | .ok w =>
     (!((Cambrian.AddressMap.lookup
          (Cambrian.Generated.World.multisigWallet w inst).m_transactions 1 |>.get!)).executed)) := by
  exact _ee003_core