Proof fn signature #

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

V@[proof_fn_item] ::= V@[proof_fn_proved] | V@[proof_fn_axiom]

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

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

V@[function_prover_mode]    ::= integer_ring | bit_vector | nonlinear_arith

V@[proof_return_type]       ::= V@[proof_return_type_named] | V@[proof_return_type_anon]
V@[proof_return_type_named] ::= ( tracked? R@[pattern] : R@[type] )
V@[proof_return_type_anon]  ::= R@[type]

Function specification #

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

The precondition. The V@[requires_clause] is the precondition.

The postcondition. The V@[ensures_clause] and the V@[returns_clause] together form the postcondition.

The invariants. The V@[invariants_clause] specifies which invariants can be opened by the function. For proof functions, the default is opens_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 V@[function_prover_mode] is provided, the proof is dispatched via the given solver (integer_ring, bit_vector, or nonlinear_arith).