chore: refactor to use arrayvec based datastructures

This should help to get better verification performance.

Sadly with
cargo kani --harness one_transaction --features verification
 --enable-unstable

I've got the following cbmc internal assertion failure:

_RNvMNtNtCsd3BvQT1zweK_17accord_playground8protocol7harnessNtB2_7Harness3run.0 iteration 6 file src/protocol/mod.rs line 159 column 33 function protocol::harness::Harness::run thread 0
--- begin invariant violation report ---
Invariant check failed
File: /tmp/tmp.uBRU9YPKKn/src/util/simplify_utils.cpp:345 function: bits2expr
Condition: el_size_opt.has_value() && *el_size_opt > 0
Reason: Check return value
Backtrace:
cbmc(+0xa16f7e) [0x560332c16f7e]
cbmc(+0xa17f0a) [0x560332c17f0a]
cbmc(+0x69abf) [0x560332269abf]
cbmc(+0xac1743) [0x560332cc1743]
cbmc(+0xabff5f) [0x560332cbff5f]
cbmc(+0xac0d4a) [0x560332cc0d4a]
cbmc(+0xa882bd) [0x560332c882bd]
cbmc(+0xa8702f) [0x560332c8702f]
cbmc(+0xabd0b2) [0x560332cbd0b2]
cbmc(+0xa85127) [0x560332c85127]
cbmc(+0xa85feb) [0x560332c85feb]
cbmc(+0xa8a69a) [0x560332c8a69a]
cbmc(+0xa8a7b9) [0x560332c8a7b9]
cbmc(+0x6375c9) [0x5603328375c9]
cbmc(+0x637636) [0x560332837636]
cbmc(+0x637636) [0x560332837636]
cbmc(+0x637636) [0x560332837636]
cbmc(+0x637636) [0x560332837636]
cbmc(+0x32dd1d) [0x56033252dd1d]
cbmc(+0x3e18ec) [0x5603325e18ec]
cbmc(+0x3e1dd5) [0x5603325e1dd5]
cbmc(+0x3e267a) [0x5603325e267a]
cbmc(+0x3921ea) [0x5603325921ea]
cbmc(+0x395c6e) [0x560332595c6e]
cbmc(+0x3980c2) [0x5603325980c2]
cbmc(+0x39627e) [0x56033259627e]
cbmc(+0x3292fc) [0x5603325292fc]
cbmc(+0x3c5ff3) [0x5603325c5ff3]
cbmc(+0x3c6463) [0x5603325c6463]
cbmc(+0x1ece0e) [0x5603323ece0e]
cbmc(+0x3c64b4) [0x5603325c64b4]
cbmc(+0x3c6755) [0x5603325c6755]
cbmc(+0x3c73dc) [0x5603325c73dc]
cbmc(+0x1c26d3) [0x5603323c26d3]
cbmc(+0x1c1c4b) [0x5603323c1c4b]
cbmc(+0x72c50) [0x560332272c50]
cbmc(+0x7089f) [0x56033227089f]
cbmc(+0x67a58) [0x560332267a58]
cbmc(+0x53c34) [0x560332253c34]
/lib64/libc.so.6(+0x27b8a) [0x7fd5a2049b8a]
/lib64/libc.so.6(__libc_start_main+0x8b) [0x7fd5a2049c4b]
cbmc(+0x696fa) [0x5603322696fa]

--- end invariant violation report ---

Cargo.toml

@@ -11,11 +11,11 @@ tracing = "0.1.40"
 # kani doesnt use dev-dependencies :(
 # https://github.com/model-checking/kani/issues/585
 # vector-map = { version = "1.0.1", optional = true }
-vector-map = { path = "vec-map-rs", optional = true }
+arrayvec = { version = "0.7.4", optional = true }
 
 [dev-dependencies]
 once_cell = "1.19.0"
 tracing-subscriber = "0.3.18"
 
 [features]
-verification = ["vector-map"]
+verification = ["arrayvec"]