## Stream: Coq users

### Topic: Avoiding infinite loop

#### Julin S (May 15 2023 at 17:08):

Hi. I got a set of instructions to be used to run a VM function. Like this:

``````| i | instr        |
|---+--------------+
| 0 | Const true;  |
| 1 | Const false; |
| 2 | Goto 4;      |
| 3 | Const true;  |
| 4 | Goto 1       |
``````

Where `Goto k` signifies a jump to instruction at index `k`.

I wrote this up as:

``````Inductive instr :=
| Const: bool -> instr
| Goto: nat -> instr.

Definition prog := list instr.
``````

I wanted to get something like an epsilon-closure of an individual instruction. ie, the indices of non-Goto instructions that are reachable from a given instruction in a `prog`.

So I naïvely tried

``````Fixpoint eclosure_aux (p:prog) (i:nat) (visited:list nat): list nat :=
let inds := seq 0 (length p) in
let aug := list_prod inds p in
match List.nth i aug (0, Goto 0) with
| (i,x) =>
match x with
| Const _ => [i]
| Goto k =>
if List.existsb (fun a => Nat.eqb a k) visited then [i]
else i :: (eclosure_aux p k (i::visited))
end
end.
Definition eclosure (p:prog) (i:nat): list nat := eclosure_aux p i [].
(*
Cannot guess decreasing argument of fix.
*)
``````

I was hoping to get something like:

``````Example p1 := [
Const true;     (* 0 *)
Const false;    (* 1 *)
Goto 4;         (* 2 *)
Const true;     (* 3 *)
Goto 1          (* 4 *)
].

Compute eclosure p1 2 [].
(* [2; 4; 1] *)
``````

The function `eclosure_aux` can be made to terminate because of the `visited` argument which can be used to avoid infinite loops.

But how can we convince the type checker?

Is there a way?

#### Julin S (May 15 2023 at 17:12):

Complete example:

``````Require Import List.
Import ListNotations.

Inductive instr :=
| Const: bool -> instr
| Goto: nat -> instr.

Definition prog := list instr.

Example p1 := [
Const true;     (* 0 *)
Const false;    (* 1 *)
Goto 4;         (* 2 *)
Const true;     (* 3 *)
Goto 1          (* 4 *)
].

Fail Fixpoint eclosure_aux (p:prog) (i:nat) (visited:list nat): list nat :=
let inds := seq 0 (length p) in
let aug := list_prod inds p in
match List.nth i aug (0, Goto 0) with
| (i,x) =>
match x with
| Const _ => [i]
| Goto k =>
if List.existsb (fun a => Nat.eqb a k) visited then [i]
else i :: (eclosure_aux p k (i::visited))
end
end.
Fail Definition eclosure (p:prog) (i:nat): list nat := eclosure_aux p i [].
``````

#### Julin S (May 15 2023 at 17:22):

We can't just add a `fuel` parameter, right? Since we can't tell in advance how long a goto-goto-goto-... chain would be (or could such info be baked into the type?)

#### Gaëtan Gilbert (May 15 2023 at 17:44):

a chain is at most `length p` long so fuel should work AFAICT

Last updated: Jun 24 2024 at 12:02 UTC