Trusted Base Awareness

When extending Sector9, understanding what the verifier trusts without proof is essential for maintaining soundness.

Why This Matters for Contributors

Every verification system has a trusted base - axioms and primitives assumed correct without proof. When you add features to Sector9, you must understand:

1. What existing axioms your feature depends on
2. Whether your feature introduces new trusted components
3. How to minimize soundness risks

A bug in the trusted base can make the entire verification system unsound, proving false properties about user code.

The Trusted Base Architecture

The trusted base has three layers, each with different stability guarantees:

┌─────────────────────────────────────────────────┐
│  Layer 3: User Assumption Boundaries            │
│  (trusted functions, abstract proof interfaces) │
├─────────────────────────────────────────────────┤
│  Layer 2: Primitive Collection Operations       │
│  (Seq, Set, Map, Multiset from prelude)         │
├─────────────────────────────────────────────────┤
│  Layer 1: Viper Prelude Axioms                  │
│  (arrays, snapshots, options, arithmetic)       │
└─────────────────────────────────────────────────┘

Layer 1: Prelude Axioms

The core axioms are generated in src/viper/prelude.ml. Key axiom categories:

Category	Purpose	Example Axiom
Array Injectivity	Unique heap locations	$loc_inv1($loc(a, i)) == a
Snapshot Domains	old() expression support	$snap_cons_int / $snap_uncons_int
Option Types	Exhaustiveness guarantees	isNone(o) || isSome(o)
Place/Address	Ownership tracking	$place_index, $addr_ref axioms
Tuples	Projection correctness	tup$N$i(Tup$N(...)) axioms

When adding a new type encoding, you may need corresponding axioms. Follow these principles:

• Axioms must be mathematically sound
• Use triggers to control SMT instantiation
• Test with pathological inputs (empty arrays, boundary values)

Layer 2: Collection Operations

Collection operations in src/prelude/prelude.mo and src/prelude/prim.mo are marked pure trusted:

module Seq = {
  public pure trusted func empty<T>() : Seq<T> {
    (prim "vseq_empty" : () -> Seq<T>)()
  };
  public pure trusted func len<T>(s : Seq<T>) : Int {
    (prim "vseq_len" : Seq<T> -> Int) s
  };
  // ...
};

These map to Viper's built-in SMT-LIB theories through the collection preprocessing path. The primitive-name table lives in src/viper/collection_helpers.ml and is used from src/viper/prep.ml:

let collection_prim_name (collection : string) (func : string) : string option =
  match collection with
  | "Seq" ->
      (match func with
       | "empty" -> Some "vseq_empty"
       | "len" -> Some "vseq_len"
       | "get" -> Some "vseq_get"
       (* ... *)
       | _ -> None)
  (* ... *)

If adding new primitive collection operations:

1. Define the Motoko signature in prelude.mo as pure trusted
2. Map to a primitive name in collection_helpers.ml
3. Handle the primitive in the collection lowering path, usually collection_lowering.ml or lower_stmt.ml
4. Ensure semantics match Viper's built-in theory exactly

Layer 3: User Assumption Boundaries

User assumptions come in two distinct forms:

• trusted functions have bodies or declaration-only signatures whose contracts are assumed rather than proved. They must declare at least one requires and one ensures.
• abstract functions are bodyless verifier placeholders for proof interfaces or verification-driven development. Their contracts are assumed by callers until the declaration is refined with a verified body, but they are not permanent trusted-base decisions.

Signature-only declarations that are neither trusted nor abstract are rejected. entry_requires is also rejected on declaration-only functions because there is no exported runtime body to guard.

Trusted and bodyless declarations are handled in lowering by emitting their contracts for call sites without verifying a body:

(* src/viper/lower.ml, simplified *)
let trusted = attrs.Fun_attrs.trusted || attrs.Fun_attrs.decl_only in
(* contracts are emitted; trusted bodies and bodyless declarations are not verified here *)

This layer is user-controlled, but the mechanism is part of Sector9's trusted base. Prefer verified lemmas, ordinary contracted helpers, and refined abstract declarations when the implementation can be checked.

Adding Features Safely

Checklist for New Features

When extending Sector9, verify:

• Does your feature depend on existing axioms?
• Do you introduce new axioms or trusted components?
• Have you added _sat, _unsat, and _reject tests for boundary cases?
• Are axiom triggers properly scoped?
• Does your feature interact with old() or permissions?

When New Axioms Are Needed

New axioms may be required when:

1. Introducing a new type encoding - Needs injectivity and projection axioms
2. Adding heap structure - Needs distinctness axioms
3. Supporting new spec operations - Needs semantic axioms

Example: Adding a new tuple arity requires projection and injectivity axioms (see prelude_tuple_encoding in prelude.ml).

Testing Axiom Soundness

Axioms cannot be proven within the system, but you can test them:

1. Consistency tests - Ensure axioms don't derive false
2. Semantic tests - Verify operations behave as expected
3. Boundary tests - Check empty collections, zero indices, maximum values
4. Interaction tests - Test axiom combinations

Create tests in test/viper/ with both _sat and _unsat variants:

// axiom_seq_len_sat.mo - Should verify
ghost {
  let s = Seq.singleton(42);
  assert Seq.len(s) == 1;  // Tests singleton/len axiom
}

// axiom_seq_len_wrong_unsat.mo - Should fail
ghost {
  let s = Seq.empty<Nat>();
  assert Seq.len(s) == 1;  // Wrong: empty has length 0
}

Key Source Files

Understanding these files is essential for trusted base work:

File	Purpose
src/viper/prelude.ml	Viper prelude axiom generation
src/prelude/prelude.mo	Sector9 prelude with spec collections
src/prelude/prim.mo	Primitive prelude declarations used by builtin lowering
src/viper/collection_helpers.ml	Collection primitive name mapping
src/viper/prep.ml	AST preprocessing and collection primitive preparation
src/viper/lower_exp.ml	Expression lowering including quantifiers
src/viper/builder.ml	Uninterpreted function emission
src/mo_def/fun_attrs.ml	Function attribute storage (trusted, pure, etc.)
src/viper/spec_meta.ml	Spec metadata collection

Axiom Generation Flow

When Sector9 generates Viper code, axioms are assembled in stages:

1. Core prelude (prelude_core)
   └─ Written once to $XDG_CACHE_HOME/sector9/prelude.vpr
   └─ Contains: Array, Place, Address, Snapshot domains

2. Per-file prelude (prelude_per_file)
   └─ Generated based on accumulated requirements
   └─ Contains: Tuple$N domains, Map range axioms, typed fields

3. Program body
   └─ Methods, predicates, functions with contracts

The reqs structure in src/viper/common.ml tracks what axioms are needed:

type reqs = {
  tuple_arities : Int_set.t ref;           (* Tuple$2, Tuple$3, etc. *)
  map_types : (typ * typ) list ref;        (* Map<K,V> types used *)
  mutable_record_snapshots : ... ref;      (* Snapshot domains needed *)
  (* ... *)
}

Common Pitfalls

Missing Triggers

Axioms without proper triggers can cause SMT timeout or unsoundness:

// Bad: No trigger, matches everything
axiom bad_axiom {
  forall x: Int :: x >= 0 ==> f(x) >= 0
}

// Good: Trigger limits instantiation
axiom good_axiom {
  forall x: Int :: {f(x)} x >= 0 ==> f(x) >= 0
}

Overly Strong Axioms

Axioms that are too strong can prove false properties:

// Dangerous: Claims all arrays have same size
axiom wrong_size {
  forall a: Array, b: Array :: $size(a) == $size(b)
}

Missing Domain Constraints

Quantifiers over Nat types need non-negativity constraints:

(* src/viper/lower_exp.ml *)
let domain_constraint_for_binder at (binder, motoko_typ) =
  if is_nat_like_type motoko_typ then
    Some (!!! at (GeCmpE (binder, intLitE at 0)))
  else None

Reviewing Trusted Base Changes

When reviewing PRs that modify the trusted base:

1. Justify the change - Why is a new axiom necessary?
2. Check mathematical soundness - Is the axiom correct?
3. Review triggers - Are they properly scoped?
4. Examine interactions - Does the axiom compose with existing ones?
5. Verify test coverage - Are boundary cases tested?

Minimizing Trusted Base Growth

The smaller the trusted base, the higher verification confidence. Strategies:

• Derive instead of axiomatize - If a property can be proven from existing axioms, prove it
• Use lemmas over unchecked assumptions - Lemmas with bodies are verified; trusted declarations are permanent assumptions, while abstract signature-only declarations should be refined when possible
• Test extensively - Testing catches specification errors before they become soundness bugs
• Document trust decisions - Explain why each trusted component exists

Summary

• The trusted base has three layers: prelude axioms, collection operations, and user assumption boundaries
• New features may require new axioms; design them carefully for soundness
• Test axioms with _sat and _unsat variants covering boundary cases
• Key files: prelude.ml, prelude.mo, collection_helpers.ml, prep.ml, lower_exp.ml
• Minimize trusted base growth by preferring verification over trust
• Review trusted base changes with extra scrutiny