Proof fn signature

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

proof_fn_item ::= proof_fn_proved | proof_fn_axiom

proof_fn_proved ::=
    visibility? broadcast? proof fn function_name generics?(args...) ( by(function_prover_mode) )? ( -> proof_return_type )?
        where_clause?
        requires_clause?
        ensures_clause?
        returns_clause?
        invariants_clause?
        decreases_clause?
    { proof_stmt* }

proof_fn_axiom ::=
    visibility? broadcast? axiom fn function_name generics?(args...) ( -> proof_return_type )?
        where_clause?
        requires_clause?
        ensures_clause?
        returns_clause?
        invariants_clause?
        decreases_clause?
        ;

function_prover_mode    ::= integer_ring | bit_vector | nonlinear_arith

proof_return_type       ::= proof_return_type_named | proof_return_type_anon
proof_return_type_named ::= ( tracked? pattern : type )
proof_return_type_anon  ::= type

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 which 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.

Function prover mode

If the function_prover_mode is provided, the proof is dispatched via the given solver (integer_ring, bit_vector, or nonlinear_arith).