Skip to main content

8. Modular Verification & Monomorphization

1. Introduction: The Generics Challenge​

Polymorphism (Generics) is a powerful tool for code reuse, but it is hard for formal verification. When a developer writes a generic List<T>, the verifier must prove that the list's invariants hold for any possible type T.

There are two main ways to verify generics:

  1. Modular Verification: Prove the generic code once using abstract type parameters. This is mathematically elegant but often fails when the proof depends on specific properties of T (e.g., that it is an integer or that it has a compare method).
  2. Monomorphization: Generate a separate copy of the code for every concrete type instantiation (e.g., List<Int>, List<Principal>) and verify each one independently. This is easier for the SMT solver but can lead to "Code Explosion."

Sector9 adopts a Global Monomorphization strategy, ensuring that every protocol-relevant type instance is verified with full precision. This research explores the implementation in src/viper/prep.ml and src/viper/lower_types.ml.

2. The Monomorphization Pipeline (prep.ml)​

Sector9 performs monomorphization early in the verification pipeline, before Sector9 source is lowered to MVIR.

mono_goal Extraction​

The system first identifies "Monomorphization Goals." A goal is a unique combination of a module/function and its concrete type arguments.

type mono_goal = { mg_mod : string option; mg_id : string; mg_typs : T.typ list; }

The mono_calls_visitor traverses the AST and records every call site where a generic function is invoked with concrete types. It also looks inside Type Contracts (Subject 11) to find nested monomorphization requirements.

Fixpoint Instantiation​

Monomorphization is iterative. Instantiating Map<K, V> might reveal that the internal implementation calls a generic Tree<T> function. prep.ml implements a fixpoint loop (mono_iterate) that continues instantiating templates until no new goals are discovered.

let rec mono_iterate ts dfs goals =
  (* ... *)
  let df = tmpl.dft_mk g.mg_typs in              (* instantiate the template *)
  let (gs', df') = mono_calls_dec_field df in    (* find new polymorphic calls *)
  mono_iterate ts (add g df' dfs) (gs' @ gs)

3. Contract Specialization​

A standout feature of Sector9 is that it monomorphizes the specification.

When a generic function func sort<T>(arr : [T]) is instantiated as sort<Nat>, the verifier doesn't just substitute the types in the code. It also substitutes them in the requires and ensures clauses.

Leveraging Instance-Specific Facts​

This is crucial for DeFi. A generic sum<T>(arr : [T]) might be impossible to prove sound because T could be a type that overflows or has no addition. But once monomorphized to sum<Nat>, the verifier can use built-in axioms about natural numbers (Subject 5) to prove that the sum is always non-negative and correctly preserved.

4. Name Mangling and Identity​

To prevent collisions in the generated Viper code, Sector9 uses a deterministic name-mangling scheme based on type fingerprints:

let string_of_mono_goal (g : mono_goal) : string =
  (* ... Int -> Int, Nat -> Nat, complex types -> Hash *)
  String.concat "$" (g.mg_id :: List.map mono_typ_key g.mg_typs)

This ensures that List<Int> and List<Nat> become two distinct entities in the SMT solver (List$Int and List$Nat), allowing each specialization to be reasoned about separately.

5. Selective Abstraction in lower_types.ml​

While the code is monomorphized, the type system in lower_types.ml still performs Erasure for the SMT solver's benefit.

Type Erasure to Solver Shapes​

Viper doesn't need to know the full complexity of Sector9's type system. lower_types.ml maps source types to solver-friendly shapes such as Int, Bool, Ref, arrays, and generated domains/wrappers where the proof needs more structure.

This "Monomorphize then Erase" strategy combines the precision of specialization with the solver performance of simple primitive types. For opaque/token handles, source-level capability summaries preserve the ownership and carrier/container facts that would otherwise be lost at this erasure boundary; MVIR passes consume those summaries instead of rediscovering handle policy from lowered type names.

6. Modular Boundary: The sr9 Verified Call​

Sector9's monomorphization is local to the compilation and verification unit. You cannot verify a remote canister body by monomorphizing it into the caller.

Instead, cross-canister calls rely on shared interfaces and the token system where shareable asset identities cross a wire boundary. sr9 shared wrappers convert between runtime wire values and verified local representations, while CHASH labels identify code-bound token shapes. Local-only opaque handles do not cross shared boundaries, but they can still be routed inside a verification unit through capability-summarized module APIs and supported carriers. This provides a "Coarse-Grained Modularity" that prevents monomorphization from leaking across the entire distributed system.

7. Evaluation & Comparison​

vs. Move Prover​

The Move Prover also uses global monomorphization.

  • Move: Highly effective because Move code is naturally small and modular.
  • Sector9: Faces a harder challenge because it is a more expressive, high-level language. Sector9's preparation and lowering passes are more complex because they must handle features like nested generic modules and polymorphic records that Move doesn't support.

vs. Dafny's Abstract Types​

Dafny uses modular verification with type parameters.

  • Dafny: Can verify a generic List<T> once. However, developers often have to write complex "Trait" or "Interface" specifications to tell the verifier what T is allowed to do.
  • Sector9: Avoids the need for complex trait specs. By monomorphizing, the verifier always knows exactly what T is, making it much more "Push-Button" for the user.

vs. Rust's Monomorphization​

Rust's compiler uses monomorphization for performance. Sector9 uses it for Verifiability.

  • Rust: Can lead to slow compile times but fast runtime.
  • Sector9: Leads to more solver obligations but higher proof precision.

8. Conclusion​

Sector9's approach to generics is pragmatic and precision-focused. By choosing Global Monomorphization over Abstract Modular Verification, it reduces the abstraction gap that appears when proofs depend on concrete type properties. For DeFi protocols, this means each supported asset-type instantiation can be verified against its specialized obligations, without requiring the developer to write complex abstract mathematical proofs up front.

Strengths:

  1. Precision: Allows proofs to use concrete properties of the instantiated types.
  2. Simplicity: No need for complex "Type Classes" or "Traits" in the specification language.
  3. Stability: Specialized code is often easier for SMT solvers to reason about than abstract code.

Weaknesses:

  1. Verification Time: Verifying 10 instances of a module takes 10 times longer than verifying it once.
  2. Code Explosion: For extremely generic libraries, the number of specializations can become large.