VDD: App2 Invariants and Frames

This tutorial walks through the app2 suite in test/viper/app2 and focuses on the invariants and proof structure that make the system modular. The flow is VDD: define the contracts first, then refine each operation to satisfy them. Read this alongside actor invariants, modifies clauses, reads clauses, and quantifiers.

Snippets below are excerpts and are not standalone modules. Use the full files under test/viper/app2 for executable context. The excerpts use the current BSeq proof-sequence API from mo:core/pure/BSeq.

1) Layered invariants and bridge lemmas

The core invariant structure lives in test/viper/app2/Invariants_sat.mo. The key idea is to show a small always-on actor_invariant, then a stronger operational_invariant used by trading paths. Two lemmas split and rebuild the invariant set so you can refine transitions in small steps.

Invariants_sat.mo (excerpt)

module Invariants {
  public inline pure func valid_config(cfg : RebalanceConfig) : Bool {
    cfg.max_out_multiplier_e8s >= 100_000_000
    and cfg.swap_fee_e8s < 100_000_000
    and cfg.deposit_fee_e8s < 100_000_000
    and cfg.withdraw_fee_e8s < 100_000_000
    and cfg.pl_tolerance_e8s < 100_000_000
  };

  public pure func reserves_wf(rs : Reserves) : Bool {
    ReservesOps.no_duplicate_principals(rs)
    and ReservesOps.prices_positive(rs)
    and ReservesOps.weights_positive(rs)
  };

  public pure func reserves_wf_or_empty(rs : Reserves) : Bool {
    ReservesOps.no_duplicate_principals(rs)
    and ReservesOps.prices_positive(rs)
    and (if (BSeq.len(rs) == 0) true else ReservesOps.weights_positive(rs))
  };

  public pure func cache_ok(state : State) : Bool {
    Accounting.total_value_base_ok(state.reserves, state.total_base)
    and (
      switch (state.last_rebalance_cost) {
        case null { true };
        case (?c) { c >= 0 };
      }
    )
  };

  public inline pure func solvent(state : State) : Bool {
    state.total_base >= state.rebate_pot + state.eToken_circulation
  };

  public ghost func actor_invariant(state : State) : Bool {
    valid_config(state.rebalanceConfig)
    and ReservesOps.nonneg_reserves(state.reserves)
    and reserves_wf_or_empty(state.reserves)
    and cache_ok(state)
  };

  public ghost func operational_invariant(state : State) : Bool {
    actor_invariant(state)
    and BSeq.len(state.reserves) > 0
    and solvent(state)
  };

  public lemma operational_invariant_parts(state : State) : ()
    requires operational_invariant(state);
    ensures actor_invariant(state);
    ensures valid_config(state.rebalanceConfig);
    ensures ReservesOps.nonneg_reserves(state.reserves);
    ensures ReservesOps.no_duplicate_principals(state.reserves);
    ensures ReservesOps.prices_positive(state.reserves);
    ensures ReservesOps.weights_positive(state.reserves);
    ensures cache_ok(state);
    ensures solvent(state);
  {
  };

  public lemma state_ok_from_parts(state : State) : ()
    requires valid_config(state.rebalanceConfig);
    requires ReservesOps.nonneg_reserves(state.reserves);
    requires ReservesOps.no_duplicate_principals(state.reserves);
    requires ReservesOps.prices_positive(state.reserves);
    requires ReservesOps.weights_positive(state.reserves);
    requires Accounting.total_value_base_ok(state.reserves, state.total_base);
    requires state.last_rebalance_cost == null;
    requires state.total_base >= state.rebate_pot + state.eToken_circulation;
    ensures actor_invariant(state);
    ensures solvent(state);
    ensures cache_ok(state);
  {
  };
}

Why this matters:

• actor_invariant is the baseline for persisted state and is written as a ghost predicate.
• operational_invariant adds extra constraints needed by quotes and transitions.
• operational_invariant_parts lets you unpack the strong invariant for local reasoning.
• state_ok_from_parts lets you rebuild the invariant once you construct a new state.

2) Quantified solvency under updates

Price updates are specified with quantified obligations so callers do not need to inline update logic. These predicates say that any update matching a frame predicate preserves solvency.

Invariants_sat.mo (excerpt)

module Invariants {
  public pure func solvent_for_reserves(rs : Reserves, rebate_pot : Nat, eToken_circulation : Nat) : Bool {
    let reserves = rs;
    let rebate = rebate_pot;
    let circulation = eToken_circulation;
    forallWith<Nat>(
      pure func (total : Nat) : Bool =
        Accounting.total_value_base_ok(reserves, total) ==> total >= rebate + circulation,
      [pure func (total : Nat) : Bool = Accounting.total_value_base_ok(reserves, total)]
    )
  };

  public ghost func price_update_solvent(state : State, ledger_id : Principal, price_e8s : Nat) : Bool {
    let reserves = state.reserves;
    let rebate = state.rebate_pot;
    let circulation = state.eToken_circulation;
    forallWith<Reserves>(
      pure func (updated : Reserves) : Bool =
        if (ReservesOps.update_price_reserves_frame(reserves, ledger_id, price_e8s, updated)) {
          solvent_for_reserves(updated, rebate, circulation)
        } else { true },
      [pure func (updated : Reserves) : Bool =
        ReservesOps.update_price_reserves_frame(reserves, ledger_id, price_e8s, updated)]
    )
  };

  public ghost func price_updates_solvent(state : State, ps : BSeq.BSeq<Types.PriceUpdate>) : Bool {
    let reserves = state.reserves;
    let rebate = state.rebate_pot;
    let circulation = state.eToken_circulation;
    let updates = ps;
    forallWith<Reserves>(
      pure func (updated : Reserves) : Bool =
        if (ReservesOps.apply_price_updates_frame(reserves, updates, updated)) {
          solvent_for_reserves(updated, rebate, circulation)
        } else { true },
      [pure func (updated : Reserves) : Bool =
        ReservesOps.apply_price_updates_frame(reserves, updates, updated)]
    )
  };
}

How it works:

• solvent_for_reserves talks about any cached total that matches total_value_base_ok.
• price_update_solvent and price_updates_solvent quantify over every update that satisfies the frame.
• This keeps solvency proofs at the contract level, not inside update loops.

3) Frame predicates for state updates

Reserve updates are described with frame predicates in test/viper/app2/ReservesOps_sat.mo. A frame predicate states exactly which fields may change and which must stay untouched.

ReservesOps_sat.mo (excerpt)

module ReservesOps {
  public pure func no_duplicate_principals(reserves : Reserves) : Bool {
    let reserves_seq = BSeq.Spec.model(reserves);
    forall<Int>(pure func (i : Int) : Bool =
      forall<Int>(pure func (j : Int) : Bool =
        if (0 <= i and i < Seq.len(reserves_seq) and 0 <= j and j < Seq.len(reserves_seq) and i != j) {
          Seq.get(reserves_seq, i).id != Seq.get(reserves_seq, j).id
        } else { true }))
  };

  public ghost func with_delta_frame(
    reserves : Reserves,
    ledger_id : Principal,
    delta : Int,
    updated : Reserves
  ) : Bool {
    let reserves_seq = BSeq.Spec.model(reserves);
    let updated_seq = BSeq.Spec.model(updated);
    Seq.len(updated_seq) == Seq.len(reserves_seq)
    and forall<Int>(pure func (i : Int) : Bool =
      if (0 <= i and i < Seq.len(reserves_seq)) {
        let prev = Seq.get(reserves_seq, i);
        let next = Seq.get(updated_seq, i);
        if (prev.id == ledger_id) {
          next.id == prev.id
          and next.target_weight == prev.target_weight
          and next.max_weight_bps_opt == prev.max_weight_bps_opt
          and next.price_e8s == prev.price_e8s
          and (next.total_reserve : Int) == (prev.total_reserve : Int) + delta
        } else {
          next == prev
        }
      } else { true })
  };

  public lemma with_delta_frame_preserves_wf(
    reserves : Reserves,
    ledger_id : Principal,
    delta : Int,
    updated : Reserves
  ) : ()
    requires no_duplicate_principals(reserves);
    requires with_delta_frame(reserves, ledger_id, delta, updated);
    ensures no_duplicate_principals(updated);
    ensures prices_positive(reserves) ==> prices_positive(updated);
    ensures weights_positive(reserves) ==> weights_positive(updated);
  {
  };

  public pure func update_price_reserves_frame_seq(
    reserves_seq : Seq<ReserveItemFull>,
    ledger_id : Principal,
    price_e8s : Nat,
    updated_seq : Seq<ReserveItemFull>
  ) : Bool {
    Seq.len(updated_seq) == Seq.len(reserves_seq)
    and forall<Int>(pure func (i : Int) : Bool =
      if (0 <= i and i < Seq.len(reserves_seq)) {
        let prev = Seq.get(reserves_seq, i);
        let next = Seq.get(updated_seq, i);
        prev.id == next.id
        and prev.total_reserve == next.total_reserve
        and prev.target_weight == next.target_weight
        and prev.max_weight_bps_opt == next.max_weight_bps_opt
        and (if (prev.id == ledger_id) { next.price_e8s == price_e8s } else { next.price_e8s == prev.price_e8s })
      } else { true })
  };

  public pure func update_price_reserves_frame(
    reserves : Reserves,
    ledger_id : Principal,
    price_e8s : Nat,
    updated : Reserves
  ) : Bool {
    update_price_reserves_frame_seq(
      BSeq.Spec.model(reserves),
      ledger_id,
      price_e8s,
      BSeq.Spec.model(updated)
    )
  };
}

Key points:

• with_delta_frame describes a single-ledger reserve change without touching other fields.
• with_delta_frame_preserves_wf reuses that frame to preserve uniqueness and positivity.
• update_price_reserves_frame isolates price changes so callers can rely on the frame.

4) Batch updates and loop invariants

Batch price updates are specified with an existential witness of intermediate steps. The implementation refines that spec by constructing the steps sequence in a loop, using invariants to keep the witness consistent.

ReservesOps_sat.mo (excerpt)

module ReservesOps {
  public ghost func apply_price_updates_frame(
    reserves : Reserves,
    ps : BSeq.BSeq<PriceUpdate>,
    updated : Reserves
  ) : Bool {
    let reserves_seq = BSeq.Spec.model(reserves);
    let updated_seq = BSeq.Spec.model(updated);
    let ps_seq = BSeq.Spec.model(ps);
    exists<Seq<Seq<ReserveItemFull>>>(pure func (steps : Seq<Seq<ReserveItemFull>>) : Bool =
      Seq.len(steps) == Seq.len(ps_seq) + 1
      and Seq.get(steps, 0) == reserves_seq
      and Seq.get(steps, Seq.len(ps_seq)) == updated_seq
      and forall<Int>(pure func (j : Int) : Bool =
        if (0 <= j and j < Seq.len(ps_seq)) {
          let upd = Seq.get(ps_seq, j);
          update_price_reserves_frame_seq(Seq.get(steps, j), upd.id, upd.price_e8s, Seq.get(steps, j + 1))
        } else { true }))
  };

  public func apply_price_updates(reserves : Reserves, ps : BSeq.BSeq<PriceUpdate>) : Reserves
    requires prices_positive(reserves);
    requires no_duplicate_principals(reserves);
    requires forall<Int>(pure func (i : Int) : Bool =
      if (0 <= i and i < BSeq.len(ps)) { BSeq.get(ps, i).price_e8s > 0 } else { true });
    ensures BSeq.len(result) == BSeq.len(reserves);
    ensures prices_positive(result);
    ensures no_duplicate_principals(result);
    ensures weights_positive(reserves) ==> weights_positive(result);
    ensures nonneg_reserves(reserves) ==> nonneg_reserves(result);
    ensures apply_price_updates_frame(reserves, ps, result);
  {
    var updated = reserves;
    ghost var reserves_seq : Seq<ReserveItemFull> = BSeq.Spec.model(reserves);
    ghost var ps_seq : Seq<PriceUpdate> = BSeq.Spec.model(ps);
    ghost {
      BSeq.model_len(ps);
      assert Seq.len(ps_seq) == BSeq.len(ps);
    };
    ghost var steps : Seq<Seq<ReserveItemFull>> = Seq.singleton<Seq<ReserveItemFull>>(reserves_seq);
    var j : Int = 0;
    while (j < BSeq.len(ps)) {
      loop:invariant j >= 0;
      loop:invariant j <= BSeq.len(ps);
      loop:invariant reserves_seq == BSeq.Spec.model(reserves);
      loop:invariant ps_seq == BSeq.Spec.model(ps);
      loop:invariant Seq.len(ps_seq) == BSeq.len(ps);
      loop:invariant BSeq.len(updated) == BSeq.len(reserves);
      loop:invariant prices_positive(updated);
      loop:invariant no_duplicate_principals(updated);
      loop:invariant weights_positive(reserves) ==> weights_positive(updated);
      loop:invariant nonneg_reserves(reserves) ==> nonneg_reserves(updated);
      loop:invariant Seq.len(steps) == j + 1;
      loop:invariant Seq.get(steps, 0) == reserves_seq;
      loop:invariant Seq.get(steps, j) == BSeq.Spec.model(updated);
      loop:invariant forall<Int>(pure func (k : Int) : Bool =
        if (0 <= k and k < j) {
          let upd = Seq.get(ps_seq, k);
          update_price_reserves_frame_seq(Seq.get(steps, k), upd.id, upd.price_e8s, Seq.get(steps, k + 1))
        } else { true });
      let pair = BSeq.get(ps, j);
      let prev = updated;
      updated := update_price_reserves(prev, pair.id, pair.price_e8s);
      ghost {
        let next_seq = BSeq.Spec.model(updated);
        assert update_price_reserves_frame(prev, pair.id, pair.price_e8s, updated);
        update_price_reserves_frame_seq_of_frame(prev, pair.id, pair.price_e8s, updated);
        assert update_price_reserves_frame_seq(BSeq.Spec.model(prev), pair.id, pair.price_e8s, next_seq);
        steps := Seq.concat(steps, Seq.singleton<Seq<ReserveItemFull>>(next_seq));
      };
      j += 1;
    };
    ghost {
      assert Seq.len(steps) == BSeq.len(ps) + 1;
      assert Seq.get(steps, 0) == reserves_seq;
      assert Seq.get(steps, Seq.len(ps_seq)) == BSeq.Spec.model(updated);
      assert forall<Int>(pure func (k : Int) : Bool =
        if (0 <= k and k < Seq.len(ps_seq)) {
          let upd = Seq.get(ps_seq, k);
          update_price_reserves_frame_seq(Seq.get(steps, k), upd.id, upd.price_e8s, Seq.get(steps, k + 1))
        } else { true });
    };
    assert apply_price_updates_frame(reserves, ps, updated);
    updated
  };
}

What to notice:

• apply_price_updates_frame uses exists to describe a chain of updates.
• The loop maintains a ghost steps sequence that witnesses the chain.
• The final assert apply_price_updates_frame(...) closes the refinement.

5) Transition contracts that reuse the invariants

Transitions in test/viper/app2/Transitions_sat.mo rely on the invariant layer and reassemble it after building a new state. The function below shows how VDD refinement uses state_ok_from_parts to restore the contract.

Transitions_sat.mo (excerpt)

module Transitions {
  public func process_deposit(state : State, req : QuoteDepositInput) : ResultStateQuoteDeposit
    requires Invariants.operational_invariant(state);
    requires Invariants.reserves_wf(state.reserves);
    requires ReservesOps.has_reserve(state.reserves, req.from_ledger);
    requires req.amount_in > 0;
    ensures switch (result) {
      case (#ok((next, _quote))) {
        Invariants.actor_invariant(next)
        and Invariants.solvent(next)
      };
      case (#err(_)) { true };
    };
    ensures switch (result) {
      case (#ok((next, _quote))) { next.rebalanceConfig == state.rebalanceConfig and next.last_rebalance_cost == null };
      case (#err(_)) { true };
    };
  {
    Invariants.operational_invariant_parts(state);
    switch (Quotes.quote_deposit(state, req)) {
      case (#err(e)) { return #err(e) };
      case (#ok(quote)) {
        var new_rebate_pot = state.rebate_pot;
        // ... apply rebate and toll adjustments ...

        switch (ReservesOps.with_delta(state.reserves, req.from_ledger, (req.amount_in : Int))) {
          case null { return #err("reserve update failed") };
          case (?updated_reserves) {
            let total_base_after = Accounting.total_value_base(updated_reserves);
            let next_shares = state.eToken_circulation + quote.amount_out;
            if (total_base_after < new_rebate_pot + next_shares) {
              return #err("solvency violated");
            };
            let newState : State = {
              reserves = updated_reserves;
              rebalanceConfig = state.rebalanceConfig;
              eToken_circulation = next_shares;
              rebate_pot = new_rebate_pot;
              last_rebalance_cost = null;
              total_base = total_base_after;
            };
            Invariants.state_ok_from_parts(newState);
            return #ok((newState, quote));
          };
        };
      };
    }
  };
}

What to take away:

• The preconditions demand operational_invariant before any transition.
• The body constructs a new state with explicit solvency and cache checks.
• state_ok_from_parts reestablishes the full actor invariant after refinement.