Skip to main content

The Trusted Base

Understanding what Sector9 trusts without proof: prelude axioms, primitive collections, core-library boundaries, and user-defined trusted code.

Overview​

Formal verification can only prove your code correct relative to assumptions. The trusted base is the set of components Sector9 assumes correct without proof. If anything in the trusted base is wrong, the verifier can prove false properties about your code.

The trusted base includes:

  • Viper prelude axioms: Logical foundations for arrays, snapshots, options, and arithmetic
  • Primitive collections: Seq, Set, Map, and Multiset operations from the prelude
  • Core library trusted wrappers: runtime and ghost helpers in core/src whose contracts are the proof boundary
  • User-defined trusted code: Functions marked trusted, including trusted declarations without bodies

Understanding the trusted base helps you assess verification confidence and minimize soundness risks.

The Three Layers​

Layer 1: Viper Prelude Axioms​

The verifier lowers Sector9 code to Viper, which relies on axiomatized domains. These axioms encode fundamental type behavior:

Array Encoding

axiom $all_diff_array {
  forall $a: Array, $i: Int ::
    $loc_inv1($loc($a, $i)) == $a &&
    $loc_inv2($loc($a, $i)) == $i
}

This axiom states that array locations are injective - different (array, index) pairs map to different heap locations.

Snapshot Domains

Snapshot axioms enable old() expressions to refer to pre-state values:

axiom snap_int_cons_uncons {
  forall $data: Seq[Int] :: {$snap_cons_int($data)}
    $snap_uncons_int($snap_cons_int($data)) == $data
}

Option Type Axioms

Exhaustiveness and discrimination for option types:

axiom option_exhaustive { forall $o: Option[T] :: isNone($o) || isSome($o) }
axiom option_exclusive  { forall $o: Option[T] :: !(isNone($o) && isSome($o)) }

Mathematical Operations

Power, absolute value, min, and max:

axiom pow_zero { forall $x: Int :: $pow($x, 0) == 1 }
axiom abs_nonneg_id { forall $n: Int :: $n >= 0 ==> $abs($n) == $n }

These axioms are intended to encode standard mathematical facts, but they are trusted - Sector9 does not prove them internally.

Layer 2: Primitive Collections​

The prelude provides specification collections as pure trusted functions:

Sequence Operations

  • Seq.empty<T>(), Seq.singleton<T>(e), Seq.len<T>(s)
  • Seq.get<T>(s, i), Seq.concat<T>(s, t), Seq.update<T>(s, i, v)
  • Seq.take<T>(s, n), Seq.drop<T>(s, n), Seq.slice<T>(s, i, j)
  • Seq.contains<T>(e, s), Seq.sorted(s), Seq.permutes<T>(a, b)

Set Operations

  • Set.empty<T>(), Set.singleton<T>(e), Set.card<T>(s)
  • Set.contains<T>(e, s), Set.union<T>(s, t), Set.minus<T>(s, t)
  • Set.intersect<T>(s, t), Set.subset<T>(s, t)

Map Operations

  • Map.empty<K,V>(), Map.get<K,V>(m, k), Map.update<K,V>(m, k, v)
  • Map.getOr<K,V>(m, k, d), Map.contains<K,V>(k, m)
  • Map.domain<K,V>(m), Map.range<K,V>(m), Map.card<K,V>(m)
  • Map.remove<K,V>(m, key), Map.putOption<K,V>(m, key, value)
  • Map.delete<K,V>(m, key), Map.take<K,V>(m, key)

Multiset Operations

  • Multiset.empty<T>(), Multiset.singleton<T>(e), Multiset.card<T>(m)
  • Multiset.contains<T>(e, m), Multiset.count<T>(m, e)
  • Multiset.union<T>(m, n), Multiset.intersect<T>(m, n), Multiset.minus<T>(m, n)

Quantifiers

  • forall<T>(f: T -> Bool), exists<T>(f: T -> Bool)
  • forallWith<T>(pred, triggers) for trigger control

These operations map to Viper's built-in collection theories and trusted ghost wrappers in core/src/ghost. Their semantics are standard, but they are not proven within user code. See the collection pages for practical patterns and immutability restrictions.

Layer 3: Core Library Runtime Boundaries​

The core library also contains trusted runtime-facing helpers for text, blob, numeric conversions, timers, cycles, iterators, mutable data structures, and platform APIs. These functions are part of the trusted base because their executable behavior comes from the runtime or library implementation while their contracts become verifier facts.

For example, numeric division wrappers, iterator constructors, and mutable map model functions are trusted where Sector9 needs a compact proof summary rather than inlining the full implementation. When a proof relies on one of these summaries, it relies on the corresponding core-library contract.

Layer 4: User-Defined Trusted Code​

Any code you mark as trusted becomes part of the trusted base:

Trusted Functions

Functions with the trusted modifier have bodies that are not verified:

public trusted func factorial(n : Nat) : Nat
  requires n <= 12;
  ensures result >= 1;
{
  // Body NOT verified - contract is assumed
  if (n == 0) { 1 } else { n * factorial(n - 1) }
}

The body is still parsed and type-checked, but its proof obligations are skipped. If the function is an impure actor helper, it must declare reads or modifies so callers know the state boundary.

Trusted Signature-Only Declarations

Trusted functions declared without bodies are assumed to satisfy their contracts:

public pure trusted func abs(x : Int) : Int
  requires true;
  ensures result >= 0;
  ensures x >= 0 ==> result == x;
  ensures x < 0 ==> result == -x;

Trusted functions with bodies and trusted bodyless declarations both add to your trusted base. Use this only for permanent external assumptions or code you intentionally do not verify. See The trusted Modifier and Signature-Only Declarations for details.

Abstract Signature-Only Declarations

Normal VDD stubs should be abstract, not trusted:

public ghost abstract func abs(x : Int) : Nat
  requires true;
  ensures result >= 0;

Abstract declarations are not marked as trusted code, but their postconditions are still assumptions while the declaration has no body. Track them as open proof obligations and refine them with implementations when possible. See Abstract Functions.

What Sector9 Verifies vs Assumes​

ComponentVerifiedAssumed
User function bodies (non-trusted)Yes-
Preconditions at all call sitesYes-
Type correctnessYes-
Trusted function bodies-Yes
Trusted function postconditions-Yes
Trusted signature-only postconditions-Yes
Abstract signature-only postconditions-Yes, until refined
Core library trusted wrappers-Yes
Prelude axiom correctness-Yes
Collection operation semantics-Yes

Key principle: Preconditions are always verified, even for trusted code. Only postconditions and body correctness are assumed.

Soundness Consequences​

If any trusted component has incorrect specifications, the verifier can prove false properties.

Wrong Axiom Example

If the array injectivity axiom were wrong, permitting aliased array locations, permission reasoning would become unsound. Two variables could refer to the same memory, violating isolation guarantees.

Wrong Collection Semantics

If Seq.len returned a negative value for some input, proofs relying on Seq.len(s) >= 0 would be unsound.

Wrong Trusted Contract

If a trusted function has an incorrect postcondition:

public trusted func buggyDouble(x : Nat) : Nat
  ensures result == x * 2
{
  x + 1  // BUG: does not match contract
}

Any caller that relies on result == x * 2 will have verified proofs that are actually false.

Minimizing the Trusted Base​

Smaller trusted bases mean higher verification confidence.

Guidelines​

Prefer verification over trust

If a function is simple enough to verify, verify it. Use trusted only when verification is impractical.

Replace stubs incrementally

Use abstract signature-only declarations for verification-driven development, then replace them with verified implementations when possible. Keep trusted signature-only declarations for permanent assumptions only.

Test trusted code thoroughly

Testing cannot prove correctness, but it catches obvious specification errors. Every trusted function should have comprehensive tests.

Document trust decisions

For each trusted function, document:

  • Why it is trusted (too complex, external dependency, mathematical fact)
  • How it was validated (testing, external proof, manual review)
  • When it might be replaced with verified code

Review trusted contracts carefully

During code review, flag all trusted declarations and long-lived abstract declarations. Question whether postconditions are exactly right - not too strong, not too weak.

What You Can Remove​

Some patterns reduce the trusted base:

Verify simple helpers

// Instead of trusted:
public trusted func max(a : Nat, b : Nat) : Nat
  ensures result == a or result == b
  ensures result >= a and result >= b
{ if (a >= b) { a } else { b } }

// Verify directly:
public pure func max(a : Nat, b : Nat) : Nat
  ensures result == a or result == b
  ensures result >= a and result >= b
{ if (a >= b) { a } else { b } }

Use lemmas for mathematical facts

Lemmas with bodies are verified, not trusted. If you can prove a property, use a lemma body instead of a trusted signature-only declaration.

Tracking the Trusted Base​

For projects with verification requirements, track your trusted base explicitly:

  1. List trusted functions: Maintain a list of all trusted functions, including trusted signature-only stubs
  2. Categorize by risk: Which trusted code is most critical to soundness?
  3. Plan verification work: Which stubs can be replaced with implementations?
  4. Review regularly: As the codebase evolves, trusted code may become verifiable

Track long-lived abstract declarations separately as unresolved proof obligations. They are not trusted-code markers, but they still provide assumed postconditions until refined.

The Prelude is Curated​

The Viper prelude axioms are curated and regression-tested. They encode standard mathematical and logical properties:

  • Array injectivity and bounds
  • Option exhaustiveness and discrimination
  • Integer arithmetic identities
  • Collection operation semantics

These axioms have been reviewed and tested, but they remain part of the trusted base. Future work may include mechanically verified proofs of prelude axioms.

Summary​

  • The trusted base includes prelude axioms, primitive collections, core-library trusted wrappers, and user-defined trusted code
  • Preconditions are always verified; postconditions and bodies of trusted code are assumed
  • Core-library trusted wrappers and ghost collection primitives are part of the proof boundary
  • Wrong specifications in the trusted base can lead to false proofs
  • Minimize the trusted base by verifying when possible and documenting trust decisions
  • Track trusted code explicitly for projects with verification requirements