Verification of recursive functions in Coq. Stop problem. Fuel
The article assumes that the reader has experience with the interactive theorem proving tool, Coq.
The article is an adapted Russian version my articlewritten while working on formal verification of the Tezos cryptocurrency protocol.
In this article, we will look at a trick that is used to deal with recursive functions that fail the finality (totality) check in Coq. By “fuel” we mean a natural number that is introduced as an additional parameter to the function body to indicate the upper bound on the number of iterations that the function can perform. This transforms the function into a finalizable one that is easy to work with and welcome by the Coq compiler. In the literature, the term is found under the names: petrol, fuel, gas, etc.
Suppose we are faced with the task of verifying a function written in some programming language. We understand what this function does, we are already considering what lemmas we will formulate in order to prove that it behaves exactly as expected. We translate the function to Coq (manually, or using automatic translators, if there are any for the required language), and we see that the Coq termination check for our function (termination check) failed.
This means Coq cannot determine which argument will decrease at each iteration step. You can try to explicitly point Coq to an argument, which, we know for sure, will decrease at each step {struct уменьшаемый_аргумент}:
Fixpoint my_function
(a : A) (b : B) (legacy : bool) {struct a} : C :=
func_bodyBut if this does not help, and the function cannot be compiled, we are forced to put a flag on the function #[bypass_check(guard)].
Checkbox #[bypass_check(guard)] cannot but irritate the proof engineer. It means that Coq cannot prove the termination of a function. This means that we have no guarantee that the programmers did not make a mistake when writing this function. It is possible that the program will hang even if we prove some properties of this function and say that it has been verified.
The note: we are faced with the halting problem described by Alan Turing: there is no universal algorithm for determining whether a particular program terminates. The termination check in Coq is conservative. This means that Coq only accepts functions of a certain kind, for which it can definitely say that this function is completed. Other functions do not pass the termination test, even if such a function actually terminates. For Fixpoint functions, Coq requires that recursive calls only be made on parameters that are syntactically decremented at each iteration step.
From checkbox #[bypass_check(guard)]need to get rid of. The action plan is the following:
write a simulation of our function (its exact copy) that will differ from the original in that a new argument will be added to it, the so-called fuel fuel. This is a natural number that will decrease at each iteration step.
tell Kok that it is by this argument that the compiler should judge whether the function terminates: {struct fuel}
decrease fuel at each iteration step (by one, for example) in the function body
prove that for all possible input parameters, the result of the simulation function with fuel will be equal to the result of the original function
work with the simulation being terminated, not the original function.
To point 4:
Lemma func_eq_funcSym: forall n fuel:nat, func n = funcSym n fuel.And although the function func still under the flag #[bypass_check(guard)], it is possible to prove this lemma if we go by induction on fuel. Probably on fuel restrictions need to be imposed.
Let’s look at an example from practice:
Below is the start of the function parse_ty. The function is taken from the project “formal verification of the Tezos cryptocurrency protocol.
The function has an annotation {struct node_value}, which should tell the Coq compiler which of the arguments to check for “decreasing at each iteration step”. But this type Alpha_context.Script.node in the source code is designed in such a way that Coq cannot determine that at each step of the recursion we will work with a direct sub-term of the argument node_value (and in this case, it really isn’t always the case).
#[bypass_check(guard)]
Fixpoint parse_ty
(ctxt : Alpha_context.context) (stack_depth : int) (legacy : bool)
(allow_lazy_storage : bool) (allow_operation : bool) (allow_contract : bool)
(allow_ticket : bool) (ret_value : parse_ty_ret)
(node_value : Alpha_context.Script.node) {struct node_value}
: M? (ret * Alpha_context.context) :=
let parse_passable_ty_aux_with_ret {ret} := 'parse_passable_ty_aux_with_ret
ret in
let parse_any_ty_aux := 'parse_any_ty_aux in
let parse_big_map_value_ty_aux := 'parse_big_map_value_ty_aux in...So we want to get rid of #[bypass_check(guard)], make the function terminate. We create a simulation function parse_ty_symby adding a natural number fuel as an argument, and changing the recursive call check to {struct fuel}.
Fixpoint parse_ty_sym (fuel : nat)
(ctxt : Alpha_context.context) (stack_depth : int) (legacy : bool)
(allow_lazy_storage : bool) (allow_operation : bool) (allow_contract : bool)
(allow_ticket : bool) {ret_value : parse_ty_ret}
(node_value : Alpha_context.Script.node) {struct fuel}
: M? (ret * Alpha_context.context) :=
match fuel with
| Datatypes.O =>
Error_monad.error_value
(Build_extensible "Typechecking_too_many_recursive_calls" unit tt)
| Datatypes.S fuel => let parse_passable_ty_aux_with_ret {ret} := 'parse_passable_ty_aux_with_ret
ret in
let parse_any_ty_aux := 'parse_any_ty_aux in
let parse_big_map_value_ty_aux := 'parse_big_map_value_ty_aux in…In the body of the function, we first of all add a check to see if the fuel is equal to zero, and if it is, we exit the loop, if not, we continue to work. We decrease the fuel in the body of the function by one, and the termination check succeeds. Thus, we manage to get rid of #[bypass_check(guard)]now we can work with the simulation.
Conclusion
One of the problems of formal verification of recursive functions is the proof of termination. If the Coq compiler’s termination check fails, you can do one of three things to compile the function:
1. put a flag over the function #[bypass_check(guard)],but then the termination of this function will remain unproved. In addition, there may be problems with proofs of the properties of such functions.
2. directly tell the compiler which parameter in the function body is recursively reduced at each iteration step {struct param}.
Sometimes in practice, if the function is very large (for example, about 3 thousand lines of code), you can try to insert in turn into {struct ..} all the input parameters received by the function. This is a hack, but it doesn’t always work. Usually you have to analyze the source code of a function to find a parameter that is a test for termination for the function (it can also increase, and the termination condition will be the achievement of a specified threshold by the parameter).
if stack_depth >i 10000 then
Error_monad.error_valueIntroduce an additional parameter into the function, the fuel is a natural number, and in the body of the function:
a) if the parameter is equal to zero, interrupt the function;
b) decrease the parameter at each iteration step.
The method presented in the article for solving the problem of checking the termination of functions is rather laborious. But at the same time, this is probably the easiest way available.
