Skip to main content

5. Collection Axiomatization for DeFi

1. Introduction: The Accounting Challenge​

In DeFi protocols, exactness is non-negotiable. A lending market must track hundreds of user positions in a Map, a decentralized exchange (DEX) must maintain an ordered Seq of price observations, and a DAO must manage a Set of voters. Any ambiguity in the formal model of these collections could lead to "Phantom Profits," "Ghost Liquidations," or "Infinite Minting" vulnerabilities.

However, modeling collections in an SMT solver (like Z3, which powers Viper) is notoriously difficult. Standard array axioms are often too slow, while fully abstract mathematical sets can't directly model heap-backed mutable structures. Sector9 solves this by providing a Rich Collection Axiomatization for ghost/spec collection models and by connecting runtime collection APIs to those models through library contracts. This research analyzes the implementation in src/viper/prelude.ml, src/viper/collection_helpers.ml, src/viper/collection_lowering.ml, and src/viper/lower_helpers_collections.ml.

2. Structural Layering: From Sector9 to SMT​

Sector9 does not treat collections as simple opaque blobs. It uses a three-layered approach:

  1. Sector9 Surface: Specs and ghost code use mathematical collections such as Map, Set, Seq, and Multiset; runtime libraries such as BMap, MBMap, and BSeq expose contracts that relate executable data structures to those models.
  2. Lowering Layer: collection_helpers.ml recognizes high-level collection operations, collection_lowering.ml dispatches primitive operations such as vmap_get and vseq_sorted, and lower_helpers_collections.ml builds the corresponding Viper expressions.
  3. Axiomatic Layer (prelude.ml): Defines the mathematical properties of these expressions in Viper domains.

3. Map Axiomatization: Domains and Range​

For DeFi, the map model is the most critical structure. Sector9 represents ghost/spec maps using Viper's Map[K, V] type and adds custom axioms to handle complex queries. Runtime maps are verified by relating their Spec.model view to this mathematical map.

The Range Axiom​

Viper's built-in map support doesn't natively include a range(m) function (the set of all values in the map). Sector9 injects this via a custom domain:

Printf.sprintf
  "function %s($m: %s): %s\n  axiom map_range_contains_%d {\n    forall $m: %s, $k: %s :: { $m[$k] } ($k in $m) ==> ($m[$k] in %s($m))\n  }"

This axiom is vital for DeFi protocols that need to prove properties over the "Total Value Locked" (TVL). By defining the range, the verifier can reason about summaries such as the sum or maximum value in a ghost ledger model.

Boxing and Injective Keys​

SMT solvers work best with simple types (Int, Bool). To support complex keys (like Records or Principals) in maps, Sector9 uses Boxing. It defines injective functions that map complex types to unique Ref or Int identifiers. The MapDomainBoxedAxioms ensure that even when a key is boxed, its presence in the map remains logically consistent.

4. Sequence Modeling: Sorting and Permutations​

DEXs often require sorted sequences (e.g., for order books). The collection lowering helpers provide a high-level vseq_sorted operation that lowers to a quantified Viper expression:

!!! exp_at (ForallE ([i_id, int_t; j_id, int_t], [s_i; s_j], body))

This encodes the obligation that for any two indices i < j, the value at i is less than or equal to the value at j.

Multi-set Permutations​

To prove that a sorting algorithm is correct, one must prove not just that the result is sorted, but that it is a permutation of the input (no elements were lost or fabricated). Sector9 handles this by mapping sequences to Multiset (Bags):

let bag_a = ctx.seq_multiset elem_t a in
let bag_b = ctx.seq_multiset elem_t b in
let bags_eq = !!! exp_at (EqCmpE (bag_a, bag_b)) in

The SeqMultisetAxioms in the prelude provide the mathematical link between sequence concatenation and multiset union, enabling powerful inductive proofs over data processing pipelines.

5. Array Snapshots: Solving the old() Problem​

A major innovation in Sector9 is the Array Snapshot Domain. In many verifiers, using old(arr[i]) in a postcondition is unstable because the solver might forget the relationship between the array elements and their previous state after a mutation.

Sector9 defines ArraySnapInt, ArraySnapBool, etc. These are Heap-Free mathematical views of an array's state at a specific point in time.

  • Snapshotting: A function snap_int(arr) creates an immutable snapshot.
  • Postconditions: The verifier proves that the snapshot matches the heap state at the time of creation.
  • Stability: Since the snapshot is a mathematical value, it remains stable even if the actual heap array is mutated later.

This is crucial for protocols that perform multi-step updates and need to refer back to the "Original Balance" or "Starting Price" throughout the function.

6. Prusti-Style "Place" Abstraction​

Sector9 adopts the "Place" and "Address" abstraction from Prusti (the Rust verifier).

domain Place {
  function $place_root(): Place
  function $place_index($base: Place, $i: Int): Place
  function $place_field($type_tag: Int, $field_tag: Int, $base: Place): Place
}

This allows the verifier to reason about Logical Identities of data locations. Instead of just saying "this pointer," Sector9 can say "the field balance inside the record at index i of the array users." This structural identity is what enables the high-precision framing discussed in Subject 2.

7. Evaluation & Comparison​

vs. Solidity's Mapping​

Solidity's mapping is an uninterpreted function in most symbolic execution tools. You can't iterate over it, and you can't reason about its size or range without manual instrumentation. Sector9's ghost/spec Map is a First-Class Mathematical Object with size, domain, and range, and runtime collection libraries can expose that model through contracts.

vs. Dafny's Collections​

Dafny has built-in sets, sequences, and maps.

  • Dafny: Excellent for general-purpose algorithms.
  • Sector9: Extends these with Actor-Awareness. Actor fields that store runtime collections or ghost collection models are integrated with the reads/modifies framing system, so contracts can state which ledger models a function reads or mutates and which facts remain stable across await boundaries.

vs. Move's Table/Map​

Move uses Table for large-scale storage.

  • Move: Table is opaque to the type system; you can only interact with individual keys.
  • Sector9: The ghost map model is transparent to the verifier. This allows for richer protocol-level invariants such as "the sum of modeled balances equals total supply."

8. Conclusion​

The collection axiomatization in Sector9 is a central piece of SMT engineering. By layering domains, axioms, and snapshots, it gives DeFi developers tools to prove complex accounting logic while keeping solver performance manageable. The introduction of Prusti-style places and range axioms specifically addresses the needs of financial protocols on the Internet Computer.

Strengths:

  1. Precision: Supports range, cardinality, sorting, and permutation proofs.
  2. Stability: Snapshot domains prevent solver "amnesia" over long functions.
  3. Integration: Collection models can participate in the actor's framing and permission model through reads/modifies contracts and runtime-library model functions.

Weaknesses:

  1. Quantifier Heat: Heavily nested quantified expressions (e.g., a map of maps) can still lead to solver timeouts if not carefully managed.
  2. Pre-baked Axioms: Developers cannot easily add their own axioms to the collections; they must rely on the provided prelude.