Skip to main content

2. Algebraic Framing & Effect Inference

1. Introduction: The Frame Problem in Smart Contracts​

In formal verification, the Frame Problem is the challenge of expressing what doesn't change when an action is performed. For a smart contract with hundreds of state variables, a function that updates only one balance must be proved not to have accidentally wiped the entire ledger or corrupted unrelated configuration fields.

Without an efficient framing mechanism, the SMT solver is forced to consider every possible state mutation, leading to "state explosion" and solver timeouts. Sector9 addresses this using Algebraic Framing and Effect Inference, a system that combines developer-written "footprints" with automated static analysis. This research explores the implementation in src/viper/mvir_effects.ml, src/viper/mvir_modifies.ml, and src/viper/mvir_reads.ml.

2. Footprint Declarations: reads and modifies​

Sector9 introduces explicit footprint annotations to the Sector9 language. These allow developers to declare the "reachable surface" of a function:

  • reads field1, field2: Declares that the function may read these fields but will not mutate them.
  • modifies field3: Declares that the function may both read and write this field.

These annotations serve as the specification-level anchor for framing. They are captured during the lowering phase from the Sector9 AST to MVIR and registered in specialized registries (mvir_reads.ml and mvir_modifies.ml).

Implementation of Footprint Registries​

The registries are essentially hash tables keyed by sanitized method names. They support "fallback names" to handle specialized methods (e.g., generated code for different type instances) by stripping specialization hashes, ensuring that verification properties are shared across monomorphized versions of the same logic.

3. The Effect Inference Engine (mvir_effects.ml)​

While developer annotations provide the intended footprint, the verifier must ensure the actual implementation respects these bounds. mvir_effects.ml implements a sophisticated effect inference engine that operates on MVIR (Sector9 Verification IR).

The Effect Summary Structure​

The system uses a structured effect_summary to track three categories of effects:

  1. reads: A set of AbstractLoc (heap locations) that are accessed for reading.
  2. writes: A set of heap locations that are mutated.
  3. unknown: A boolean flag indicating if the function has side effects that cannot be statically resolved (e.g., calling an unverified external library).

Fixpoint Analysis over the Call Graph​

Effect inference is not a single pass but an iterative fixpoint analysis.

  1. Initial Seeding: Every method is initialized with its local effects (direct field reads/writes in its body).
  2. Propagation: The engine iterates over the call graph. If function A calls function B, A's summary is updated to include the union of its own effects and B's summary.
  3. Monomorphization & Specialization: Crucially, the engine "specializes" summaries at call sites. If a method is called with a specific receiver (e.g., this.sub_module), the generic $Self references in the callee's summary are substituted with the actual heap path in the caller.
let rec iterate () : unit =
  (* ... *)
  let new_sum = union_summary !s (specialize_summary ~sigs ~callee ~call_args:args callee_summary)
  (* Repeat until no summaries change *)

4. Solving the Frame Problem in Viper​

Once the effect summaries are computed, they are used to generate the final Viper code. The "Algebraic" nature of the framing comes from how these summaries are translated into Viper's Implicit Dynamic Frames logic.

Inhale/Exhale and Permissions​

Viper uses Linear Permissions (acc(field)) to manage heap access. Sector9's framing logic uses the inferred summaries to:

  • Grant Permissions: Before a function executes, it "inhales" the permissions for every field in its modifies and reads footprint.
  • Enforce Restrictions: If the code attempts to write to a field not in its modifies set, the verifier fails because it lacks the necessary write permission.
  • Generate Frame Posts: For any field in the reads set (but not modifies), the translator automatically generates a postcondition: ensures field == old(field). This gives the solver an explicit obligation that the field remained constant throughout the function.

The "Havoc" at Await Boundaries​

As discussed in Subject 1, await points are suspension boundaries. The effect inference engine plays a vital role here by determining the await interference set.

When an actor suspends, the system identifies all public methods of that actor. It unions their writes summaries, adds actor-rooted locations that are deep mutable or otherwise nonstable, and filters the result to shared locations. At the await point, everything in this havoc set is invalidated. This lets the local function keep facts about fields that no interleaving public method can write, while rejecting stale facts about fields that may be touched.

5. Built-in Collection Semantics​

One important feature of Sector9's effect system is how it handles the "Total vs. Partial" nature of collections (Maps, Sets, Seqs).

The engine contains hardcoded knowledge of core collection modules and their trusted wrappers.

  • Calls to ghost/spec operations such as Map.get or Seq.len, and pure collection operations such as BMap.get, are inferred as pure/read-only.
  • Calls to mutable wrappers such as MBMap.put or array mutation helpers are inferred as writes to the relevant abstract location, or as unknown writes when the location cannot be resolved precisely.

This prevents the verifier from treating every collection as an opaque blob. By understanding the semantics of ghost maps, pure BMap values, and mutable MBMap wrappers, Sector9 can preserve useful frame facts while still requiring explicit footprints for runtime state updates.

6. Soundness and Completeness Checks​

The system includes "fail-closed" checks to prevent developer error:

  • check_modifies: If the inference engine finds a write to a field that isn't in the function's modifies clause, it throws an Unsupported error with a helpful message: modifies clause missing fields: balance; add modifies balance.
  • check_reads: Similar to writes, it ensures all reads are declared.

This forces an explicit-footprint workflow. Verified functions must document their read/write surface, which creates the audit trail needed for security-critical review.

7. Evaluation & Comparison​

vs. Solidity's Memory Model​

Solidity has no concept of framing. A function can overwrite any storage slot using assembly or via delegatecalls. This is why "Storage Collision" and "Unintended State Overwrites" are common vulnerabilities. Sector9's algebraic framing makes undeclared state reads and writes fail verification instead of being silently assumed.

vs. Dafny's reads/modifies​

Sector9's system is heavily inspired by Dafny. Dafny also uses reads and modifies clauses.

  • Dafny: Often requires complex "Dynamic Frames" (using sets of objects) which can be hard for beginners.
  • Sector9: Tailors this to the Actor Model. Since state is isolated within the canister, the "universe" of possibly modified fields is finite and bounded by the actor's declaration. This makes Sector9's framing significantly more predictable and stable for the SMT solver than Dafny's general-purpose heap model.

vs. Move Prover​

The Move Prover uses a similar "Footprint Analysis" to determine which global resources a function might touch.

  • Move: Relies on the type system (acquires Resource) to drive framing.
  • Sector9: Uses a combination of the type system and explicit field-level annotations. Sector9's model is more granular, allowing framing at the level of individual record fields, whereas Move usually frames at the level of the entire Resource type.

8. Conclusion​

The Algebraic Framing and Effect Inference system is the "efficiency engine" of Sector9. By translating high-level footprint declarations into precise permissions and equality postconditions, it gives the SMT solver focused obligations instead of the whole actor heap. For DeFi protocols, this lets accounting proofs explicitly state which protocol state they depend on and which state must remain framed.

Strengths:

  1. Granularity: Field-level framing prevents unrelated state corruption.
  2. Automation: Fixpoint inference reduces the annotation burden on developers by propagating effects through the call graph.
  3. Solver Stability: Explicit frame postconditions (field == old(field)) are much easier for SMT solvers to handle than complex heap reachability proofs.

Weaknesses:

  1. Annotation Burden: While propagated, the initial reads/modifies clauses on public methods are still required and can be tedious for large actors.
  2. Higher-Order Complexity: Framing through function pointers or objects remains a "narrow supported surface" because effect inference is significantly harder when the callee is not statically known. (This is addressed in Subject 11).