Bounded and unbounded iterators

This modules defines several Coq encodings of a general "while" loop. The loop is presented in functional style as the iteration of a step function of type A → B + A:

        let rec iterate step a =
          match step a with
          | inl b -> b
          | inr a' -> iterate step a'

This iteration cannot be defined directly in Coq using Fixpoint, because Coq is a logic of total functions, and therefore we must guarantee termination of the loop.

Terminating iteration

We first implement the case where termination is guaranteed because the current state a decreases at each iteration.

We now prove an invariance property iterate_prop, similar to the Hoare logic rule for "while" loops.

Bounded iteration

The presentation of iteration shown above is predicated on the existence of a well-founded ordering that decreases at each step of the iteration. In several parts of the CompCert development, it is very painful to define such a well-founded ordering and to prove decrease, even though we know our iterations always terminate. In the presentation below, we choose instead to bound the number of iterations by an arbitrary constant. iterate then becomes a function that can fail, of type A → option B. The None result denotes failure to reach a result in the number of iterations prescribed, or, in other terms, failure to find a solution to the dataflow problem. The compiler passes that exploit dataflow analysis (the Constprop, CSE and Allocation passes) will, in this case, either fail (Allocation) or turn off the optimization pass (Constprop and CSE). Since we know (informally) that our computations terminate, we can take a very large constant as the maximal number of iterations. Failure will therefore never happen in practice, but of course our proofs also cover the failure case and show that nothing bad happens in this hypothetical case either.

The simple definition of bounded iteration is:

Fixpoint iterate (niter: nat) (a: A) {struct niter} : option B :=
  match niter with
  | O => None
  | S niter' =>
      match step a with
      | inl b => b
      | inr a' => iterate niter' a'
      end
  end.

This function is structural recursive over the parameter niter (number of iterations), represented here as a Peano integer (type nat). However, we want to use very large values of niter. As Peano integers, these values would be much too large to fit in memory. Therefore, we must express iteration counts as a binary integer (type positive). However, Peano induction over type positive is not structural recursion, so we cannot define iterate as a Coq fixpoint and must use Noetherian recursion instead.

The iterate function is defined as iter up to num_iterations through the loop.

We now prove the invariance property iterate_prop.