Skip to main content

Abstract Functions (abstract func)

Abstract functions are contract-only declarations for verification-driven development. They have requires and ensures clauses, but no body yet, so their postconditions are assumptions until the declaration is refined.

Use abstract when you want to specify a proof helper or interface first, verify callers against that interface, and fill in the implementation later. For the broader signature-only workflow, see Signature-Only Declarations. Use trusted instead when the unchecked boundary is permanent.

Basic Syntax​

An abstract function has a signature and contracts, then stops after the final contract semicolon:

public pure abstract func specValue(x : Int) : Int
  requires true;
  ensures result == x + 1;

There are no braces and no implementation.

For proof-only helpers, prefer ghost abstract func:

public ghost abstract func distance(a : Int, b : Int) : Nat
  requires true;
  ensures result >= 0;

abstract ghost func is also accepted:

public abstract ghost func chooseGreater(x : Int) : Int
  requires true;
  ensures result > x;

Example​

abstract-func-basic.sr9
// Abstract functions are contract-only verifier placeholders.
module {
  public pure abstract func oneMore(x : Int) : Int
    requires true;
    ensures result == x + 1;

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

  public abstract ghost func chooseGreater(x : Int) : Int
    requires true;
    ensures result > x;

  public lemma abstractPostconditionsAreAvailable(x : Int) : ()
    requires true;
    ensures oneMore(x) == x + 1;
    ensures chooseAtLeast(x) >= x;
    ensures chooseGreater(x) > x;
  {};
}

The lemma can use the postconditions of all three abstract functions. No body is checked because no body exists yet.

Verification Semantics​

Abstract functions are not magic trusted calls. The verifier still checks every call against the function's preconditions:

signature-precondition-fail_unsat.sr9
// Abstract signature-only proof helpers still require preconditions at call sites
module {
  // Abstract signature-only proof helper with precondition
  public ghost abstract func safeSqrt(x : Nat) : Nat
    requires x <= 1000000;
    ensures result * result <= x;

  // This lemma violates the precondition in proof code - verification fails
  public lemma bad(n : Nat) : () {
    let _witness = safeSqrt(n);  // Error: cannot prove n <= 1000000
  };
}

After a valid call, the verifier may use the abstract function's postconditions. While the declaration remains abstract, those postconditions are assumptions. If the contract is wrong, callers can verify against a false interface until you refine the declaration.

Verification-Driven Development​

Abstract functions support a specify-first workflow:

signature-vdd.sr9
// Verification-Driven Development for proof-only helpers:
// start with specs, add implementations later.
module {
  // Stage 1: Abstract ghost helper stubs with contracts only
  public ghost abstract func lineTotal(qty : Nat, unit : Nat) : Nat
    requires true;
    ensures result == qty * unit;

  public ghost abstract func discount(subtotal : Nat, rate : Nat) : Nat
    requires rate <= 100;
    ensures result <= subtotal;

  public ghost abstract func shipping(weight : Nat) : Nat
    requires true;
    ensures result == weight * 2;

  // Stage 2: Implement a proof-only helper using stubs
  public ghost func invoice(qty : Nat, unit : Nat, rate : Nat, weight : Nat) : Nat
    requires rate <= 100;
    ensures result == lineTotal(qty, unit) + shipping(weight);
  {
    let sub = lineTotal(qty, unit);
    let ship = shipping(weight);
    sub + ship
  };
}

The workflow is:

  1. Write abstract function contracts.
  2. Verify proof-only callers against those contracts.
  3. Replace each abstract declaration with an implemented function when the body is ready.

When you refine an abstract function, remove abstract and add the body:

public ghost func distance(a : Int, b : Int) : Nat
  requires true;
  ensures result >= 0;
{
  if (a >= b) { a - b } else { b - a }
};

Abstract vs Trusted​

abstract and trusted mean different things:

FormBodyMeaning
abstract funcNoVDD placeholder or proof interface to refine later
trusted funcOptionalExplicit unchecked trusted boundary
Implemented non-trusted functionYesBody is verified against its contract

Use abstract for temporary proof interfaces and specification scaffolding. Use trusted only when you intentionally want an unchecked implementation or permanent external assumption.

The compiler rejects abstract trusted because it mixes those two meanings.

Allowed Forms​

FormTypical Use
pure abstract funcSpecification function usable from contracts
ghost abstract funcProof-only helper returning a value
abstract ghost funcSame as ghost abstract func
abstract lemmaBodyless proof obligation

Most abstract helpers should be ghost abstract func unless they must be usable as pure specification functions from non-ghost contracts. Use abstract lemma when the placeholder is a proof step rather than a value-returning helper.

Restrictions​

Abstract functions:

  • Must not have a body.
  • Must not be trusted.
  • Must not be inline.
  • Must not use entry_requires.
  • Must be refined before compile/run if they appear in deployable code.
  • Still create call-site proof obligations from every requires clause.

entry_requires is executable runtime-entry checking. An abstract function has no runtime body, so use logical requires clauses instead.

Runtime Restriction​

Abstract declarations are verification-only placeholders. They are useful while proving and refactoring, but they are not deployable implementations.

Before compiling or running runtime code, replace abstract declarations with implemented functions. If the implementation itself must remain unchecked, write a trusted function with a body and document why it belongs in the trusted base.

Abstract declarations are allowed in verification-oriented modules and ghost proof surfaces. They are not a way to ship missing runtime behavior.

Summary​

  • abstract func declares a contract-only placeholder with no body.
  • Callers still have to prove requires.
  • Callers may use ensures after a valid call.
  • Abstract postconditions are assumptions until the declaration is refined.
  • Use ghost abstract func for proof-only helpers.
  • Use abstract lemma for bodyless proof obligations.
  • Use trusted, not abstract, only for intentional trusted boundaries.