Stream: Coq users

Topic: Avoiding infinite loop


view this post on Zulip 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?

view this post on Zulip 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 [].

view this post on Zulip 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?)

view this post on Zulip 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