Proof fn signature

The general form of a proof function signature takes the form:

proof fn function_name generics?(args...) -> return_type_and_name?
    where_clause?
    requires_clause?
    ensures_clause?
    returns_clause?
    invariants_clause?

Function specification

The elements of the function specification are given by the signature clauses.

The precondition. The requires_clause is the precondition.

The postcondition. The ensures_clause and the returns_clause together form the postcondition.

The invariants. The invariants_clause specifies what invariants can be opened by the function. For proof functions, the default is open_invariants none. See this page for more details.

Function arguments

All arguments and return values need to have ghost or tracked mode. Arguments are ghost by default, and they can be declared tracked with the tracked keyword.

See here for more information.