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?

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 [].
```

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?)

a chain is at most `length p`

long so fuel should work AFAICT

Last updated: Jun 24 2024 at 12:02 UTC