Abstract Signature-Only Declarations

Bodyless verifier placeholders are written with abstract. Use bodyless trusted only for permanent assumptions that belong in the trusted base.

Overview

A signature-only declaration has contracts but no body. The normal verification-driven-development form is abstract:

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

Historically, some VDD placeholders were written as trusted bodyless functions. That is outdated for normal proof scaffolding. Use abstract when the declaration is an interface or placeholder that should be refined later. Use trusted only when you are intentionally adding an unchecked trusted boundary.

For function-focused syntax and restrictions, see Abstract Functions.

The verifier treats an abstract declaration as a specification stub: callers must prove the requires clauses, and after the call the verifier may use the ensures clauses. No implementation is checked because no implementation exists yet. That makes abstract declarations useful but still assumption-bearing until refined.

This enables:

• Proof-oriented VDD: write proof-helper specifications first, then add implementations later
• Modular proof scaffolding: verify ghost callers and lemmas against abstract interfaces
• Mathematical specs: define proof-only functions used in contracts, lemmas, and ghost blocks

Syntax

Mark the declaration abstract and omit the body:

public ghost abstract func name(params) : ReturnType
  requires true;
  ensures postcondition;

The final contract semicolon ends the declaration. There are no braces and no implementation.

abstract works with pure functions, ghost functions, and lemmas:

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

public abstract lemma fact(x : Nat) : ()
  requires true;
  ensures x >= 0;

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

public ghost func name(params) : ReturnType
  requires true;
  ensures postcondition;
{
  body
};

Bodyless declarations must be explicit. A declaration without a body must be marked either abstract or trusted; a plain bodyless function is rejected. abstract trusted is also rejected because the two markers mean different things. Abstract declarations also cannot be inline or use entry_requires.

Basic Example

signature-basic.sr9

// Abstract signature-only declarations: proof-only functions with contracts but no body
module {
  // Abstract ghost function with contract only - no runtime implementation
  public ghost abstract func abs(x : Int) : Nat
    requires true;
    ensures result >= 0;
    ensures x >= 0 ==> result == x;
    ensures x < 0 ==> result == -x;

  // Another abstract signature-only proof helper
  public ghost abstract func max(a : Nat, b : Nat) : Nat
    requires true;
    ensures result >= a;
    ensures result >= b;
    ensures result == a or result == b;

  // Proof-only code can use signature-only declarations.
  public ghost func demo(x : Int) : Nat
    ensures result >= 0;
  {
    abs(x)
  };
}

In this example:

• abs and max are abstract proof helpers with contracts but no bodies
• demo is proof-only and uses abs
• The verifier assumes abs returns a non-negative value based on its ensures clause
• No implementation of abs is checked
• No trusted marker is needed for this placeholder workflow

Verification-Driven Development

Abstract declarations 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
  };
}

This pattern lets you:

1. Define proof helpers as abstract stubs with contracts
2. Implement and verify ghost callers or lemmas using those stubs
3. Refine each stub by removing abstract and adding a body

Each stage verifies independently in the proof-only lane. Runtime callers still need implemented helpers, not bodyless declarations. If a bodyless declaration appears in deployable code, refine it before compile/run or make the trusted runtime boundary explicit with a body.

Abstract Lemmas

Lemmas can also be abstract. This states a proof obligation for later without providing the proof now:

signature-lemma.sr9

// Abstract signature-only lemma: states a fact before providing proof
module {
  public ghost abstract func square(x : Nat) : Nat
    requires true;
    ensures result == x * x;

  // Abstract signature-only lemma - contract assumed until refined
  public abstract lemma squareNonNeg(x : Nat) : ()
    requires true;
    ensures square(x) >= 0;

  // Another lemma stating a mathematical identity
  public abstract lemma squareMonotonic(a : Nat, b : Nat) : ()
    requires a <= b;
    ensures square(a) <= square(b);

  // Use the lemmas in verification
  public lemma demo(n : Nat) : ()
    ensures square(n) >= 0;
  {
    squareNonNeg(n);
  };
}

Abstract lemmas are useful when:

• The property is part of a proof plan, but the proof will be filled in later
• You want to unblock callers while developing supporting facts
• The fact belongs to an interface between proof modules

They should not be used to hide a fact that you never intend to prove. If the fact is a permanent external assumption, make that explicit as trusted code instead.

Preconditions Are Still Checked

Abstract does not mean "trust every call." Callers must still establish 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
  };
}

The verifier rejects bad because it cannot prove n <= 1000000. The abstract function's precondition creates a proof obligation at every call site.

What Gets Verified vs Assumed

Aspect	Abstract signature-only	Trusted signature-only	Implemented non-trusted function
Body	None	None	Present
Call-site preconditions	Verified	Verified	Verified
Postconditions at calls	Assumed from contract until refined	Assumed from contract	Used after body verification
Body checked	No body to check	No body to check	Yes
Runtime implementation	None	None	Present
Code-review meaning	Placeholder or interface to refine	Explicit trusted assumption	Checked implementation

The verification boundary:

1. Callers must satisfy preconditions - every call site is checked.
2. Postconditions are assumed while abstract - after a call, the verifier treats ensures as facts.
3. No body is checked - there is no body to verify yet.
4. Refinement changes the boundary - once you add a body and remove abstract, the verifier checks the implementation against the same contract.

Abstract vs Trusted

abstract and trusted serve different purposes:

Form	Has body	Typical use
abstract signature-only	No	VDD placeholders, proof interfaces, abstract lemmas
trusted signature-only	No	Permanent explicit assumptions or external axioms
trusted with body	Yes	Runtime or proof code whose implementation is intentionally unchecked

Use abstract when:

• You want a proof-only specification with no implementation yet
• You are doing verification-driven development for lemmas or ghost helpers
• You expect to refine the declaration by adding a verified body later

Use trusted when:

• You have an implementation but intentionally do not want to verify it
• You are modeling a permanent external fact or axiom
• You want the declaration to be part of the trusted base

The compiler rejects abstract trusted declarations. Pick one meaning.

Combining with Proof Helpers

Most user-facing signature-only helpers should now be ghost abstract:

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

Ghost signature-only functions can appear in contracts and lemmas:

public func example(n : Nat) : Nat
  ensures result >= helper(n);
{
  // ...
}

The postcondition of example can mention the abstract helper, and the body can call it in ghost/proof-only code. The call is legal only where the verifier can prove the helper's preconditions.

Runtime Restriction

Abstract functions cannot be compiled or executed. They are verification-only placeholders. If you try to compile or run code that still contains an abstract declaration in the runtime projection, you get an error like:

abstract functions are verification-only; refine them with a body before compiling or running

This prevents deploying code with missing implementations. For runtime code, refine the declaration by removing abstract and adding a body. If the runtime implementation itself must remain unchecked, write a trusted function with a body.

Abstract declaration-only functions also cannot use entry_requires, because entry guards are executable runtime checks and require a concrete public/exported runtime body.

When to Use Signature-Only

Appropriate uses:

• Verification-driven development for proof helpers - specify interfaces before implementing
• Modular proof scaffolding - verify lemmas and ghost code against abstract interfaces
• Proof-only specification functions - mathematical helpers for contracts
• Abstract lemmas - state proof goals before filling in the proof

Avoid when:

• You have a straightforward implementation - just write the body
• The function will be called at runtime - use an implemented function, possibly marked trusted
• The contract is speculative - abstract contracts are still assumptions while the body is missing
• The declaration needs entry_requires - entry guards require a concrete public/exported body

Soundness Implications

abstract makes the VDD intent explicit and avoids labeling temporary placeholders as trusted code. It does not prove the placeholder's contract. While a declaration remains abstract, its postconditions are assumptions at call sites. If the contract is wrong, the verifier may prove false properties until the declaration is refined.

Keep abstract declarations minimal:

• Replace stubs with implementations when possible
• Keep contracts small and reviewable
• Document why the declaration is still abstract if it lasts beyond the current proof task
• Prefer implemented lemmas once the supporting proof is available

See The Trusted Base for more on verification soundness.

Summary

• Use abstract, not trusted, for normal bodyless VDD placeholders
• trusted is still available for explicit unchecked implementations or permanent assumptions
• The verifier checks preconditions at call sites and assumes abstract postconditions while the body is missing
• Abstract declarations cannot have bodies, cannot be inline, cannot use entry_requires, and cannot be combined with trusted
• Plain bodyless functions are rejected; the declaration must be either abstract, trusted, or implemented
• Compile/run require refinement: remove abstract and add a body before runtime use

Related Topics

• Trusted modifier for unchecked implementations
• CLI check for fast syntax and type validation while stubs are still abstract
• Contract placement for refining a signature into an implemented function
• Verified subset limitations for proof-only declarations and runtime projection boundaries