As you may already know from the article Simulations - dependently-typed version,
in the `Proto_alpha`

folder we keep code, generated by the `coq-of-ocaml`

.
Many of the fixpoints here are preceded by the annotation `#[bypass_check(guard)]`

,
which means that guard checking is locally disabled. And this means that
we can not consider these functions to be total. In such cases, proof engineers
usually feel irritation, because "total" is one of their favorite words.
We know that total functions never crush and they always return a well-typed
result within a finite time.

##### note

Thanks to Alan Turing we know that the halting problem - the difficulty of determining whether a specific program terminates or not - is undecidable. Coq can't determine if a function is total in general, according to the original definition of totality. Instead, it analyzes a function's syntax and makes a conservative approximation.

Our current goal is that the doubles defined in the folder
`Simulations`

, whose equivalence with their prototypes from `Proto_alpha`

should
be proved, would be total (have enabled Coqs guard checking on fixpoint).
We already mentioned the `Guard Checking`

question here.

Coq is analyzing the function's syntax to consider it to be total. One way to convince Coq that a function is total is to show that there is a decreasing argument that converges to the base case.

Let's consider the function `parse_ty_aux`

from `Proto_alpha`

and its clone
`dep_parse_ty_aux`

from the `Simulations`

folder. `parse_ty_aux`

is having
`{struct node_value}`

annotation. The point of the `{struct ident}`

annotation is
to tell the Coq, which argument decreases along the recursive calls.
`node_value : Alpha_context.Script.node`

is designed in such a way that it is
not trivial to show that the function converges. Coq can not detect that each
and every recursion call is done on the direct subterm of a given `node_value`

argument (and it is indeed actually not the case).

`#[bypass_check(guard)]`

Fixpoint parse_ty_aux {ret : Set}

(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

let? ctxt := Alpha_context.Gas.consume ctxt Typecheck_costs.parse_type_cycle

in

if stack_depth >i 10000 then

Error_monad.error_value

(Build_extensible "Typechecking_too_many_recursive_calls" unit tt)

else ...

For `dep_parse_ty_aux`

we change the `recursive call argument`

annotation,
we make it {struct fuel}

`Fixpoint dep_parse_ty_aux `

(ctxt : Alpha_context.context) (fuel : nat) (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_fam ret_value * Alpha_context.context) :=

let parse_passable_ty_aux_with_ret := 'parse_passable_ty_aux_with_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

let? ctxt := Alpha_context.Gas.consume ctxt Typecheck_costs.parse_type_cycle

in

match fuel with

| Datatypes.O =>

Error_monad.error_value

(Build_extensible "Typechecking_too_many_recursive_calls" unit tt)

| Datatypes.S fuel => ...

We see that in `parse_ty_aux`

we have an argument `stack_depth`

, we can think of
it as being a `fuel`

that allows us to continue the processing. We do something
similar for `dep_parse_ty`

. First of all we define it without
the `#[bypass_check(guard)]`

. We add new argument `fuel : nat`

, we chose `nat`

because it is easy to work with natural numbers in Coq. We need to prefix
the constructors `O`

and `S`

with `Datatypes`

to avoid undesirable collisions
and intersections. On each recursive step we consume one drop of fuel and
continue execution, and when we've got no more fuel we abandon execution.

`match fuel with | Datatypes.O =>`

In the next step, we prove equality of our functions. Notice how we define
`stack_depth`

parameter for `parse_ty_aux`

using fuel.

`Fixpoint parse_ty_aux_dep_parse_ty_aux_eq`

(ctxt : Alpha_context.context) (fuel : nat) (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) : (fuel <= nat_number_10001)%nat ->

match (@dep_parse_ty_aux

ctxt fuel legacy

allow_lazy_storage allow_operation allow_contract

allow_ticket ret_value node_value,

parse_ty_aux

ctxt (number_10001 - Z.of_nat fuel) legacy

allow_lazy_storage

allow_operation allow_contract allow_ticket

ret_value node_value ) with

| (Pervasives.Ok (res, c), Pervasives.Ok (res',c')) =>

ret_fam_to_ex_ty_entrypoints res = res' /\ c = c'

| (Pervasives.Error e, Pervasives.Error e') => e = e'

| _ => False

end.

Proof. ...

So summarizing the above: **fuel** or sometimes in articles or books, we can meet
the term **gas** is a useful life hack for proof engineers, which helps to convince
Coq that function terminates, and makes proofs lighter and shorter.