/machines/1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---/rocq/dev_block.v · raw
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
Require Import ssim.
From BusyCoq Require Import Individual62.
Require Import List NArith.
Import ListNotations.

Definition ustep (st : N * cfg * bool) : N * cfg * bool :=
  let '(k, c, stop) := st in
  if stop then st else
  match sstep c with Some (c', _) => (N.succ k, c', false) | None => (k, c, true) end.
Definition until_stuck (fuel : positive) (c : cfg) := Pos.iter ustep (0%N, c, false) fuel.
Definition v (i : nat) (c : N) : lf := LF c (List.repeat 0%N i ++ [4%N]).
(* t = v0, s = v1, a = v2, lp = v3 *)
Definition U0c := Lc D ([(S0, LF 3 []); (S0, v 0 4); (S1, v 1 4); (S0, v 2 1); (S0, v 3 2)], TV 0) ([], TV 1).
Time Eval vm_compute in until_stuck 1000 U0c.
Definition U1c := Lc D ([(S0, LF 3 []); (S0, v 0 4); (S1, v 1 4); (S0, v 2 2); (S1, v 3 1)], TV 0) ([], TV 1).
Time Eval vm_compute in until_stuck 1000 U1c.
(* tight digit gap variants *)
Definition U0c' := Lc D ([(S0, LF 3 []); (S0, v 0 4); (S1, v 1 4); (S0, LF 1 []); (S0, v 3 2)], TV 0) ([], TV 1).
Time Eval vm_compute in until_stuck 1000 U0c'.