Skip to main content

Verified Subtyping and Contracts

Verification mode applies additional type rules to keep ownership, heap identity, effects, and function contracts sound. These rules sit on top of Sector9's structural type system.

The goal is not to make subtyping smaller for its own sake. It is to prevent a coercion from hiding the facts that the verifier needs: who owns a mutable value, which fields a callable may touch, and which pre/postconditions remain available to callers.

Structural Subtyping Limits​

In verified code, structural subtyping is allowed only for spec-immutable record/module types:

  • No var fields
  • No arrays or mutable records
  • No functions, actors, or nested module values
  • No async or async* values

If a structural coercion violates this rule, the verifier rejects it with M0338. Aliases do not bypass this check because the verifier sees the expanded type.

// Rejected in verification (module contains functions)
module M1 { public func inc(n : Nat) : Nat { n + 1 } };
module M2 = M1;  // M0338

Mutable Identity Coercions​

Any structural coercion that would hide heap or mutable identity is rejected in verification (error M0339). This includes arrays, mutable record fields, actors, mixins, and memory objects:

// Rejected in verification (array identity cannot be hidden by coercion)
let xs : [var Nat] = [var 1, 2];
let ys : [Nat] = xs;  // M0339

The same principle applies to module-owned handles such as opaque and token values. Outside the defining module, their payload is sealed; subtyping cannot be used to peel away the owner boundary or confuse one module's handle with another module's handle.

Contract Preservation in Subtyping​

Function types can carry contracts. In verification:

  • Contract subtyping uses logical implication (requires contravariant, ensures covariant)
  • Contracts are preserved when the expected type has contracts
  • A contract-bearing function can be used where the expected type has no contracts, but callers through that weaker type cannot rely on the dropped facts
type Weak = (x : Nat) -> Nat contract {
  requires x > 0;
  ensures result >= x;
};

type Strong = (x : Nat) -> Nat contract {
  requires x > 0;
  ensures result > x;
};

let f : Strong = ...;
let g : Weak = f;  // OK: Strong implies Weak

If the implication does not hold, the coercion is rejected.

This is why callback APIs should usually publish the contract they require. If you accept an uncontracted function type, the verifier cannot assume the callback preserves a balance, respects a permission check, or stays within a useful footprint. Use function type contracts for callbacks that participate in protocol reasoning.

Practical Guidance​

  • Keep public structural views spec-immutable when you expect verified coercions.
  • Use function type contracts instead of passing impure callbacks through uncontracted function types.
  • Snapshot heap data into ghost/spec collections before using broad structural views in specifications.
  • Keep mutable implementation details behind owner modules and expose pure observers or contracted methods.
  • Treat a failed coercion as a signal that the target type is hiding proof-relevant identity, not just as a type-system inconvenience.