/machines/1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---/rocq/dev_count.v · raw
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
Require Import ssim.
From BusyCoq Require Import Individual62.
Require Import List NArith.
Import ListNotations.

(* TM-step cost of one sstep (concrete forms only) *)
Definition cost (c : cfg) : N :=
  match c with
  | Rc q l ((b, n) :: rs, t) =>
      if is_zero n then 0 else match cR_idx q b with Some _ => if all4 (lv n) then lc n else 1 | None => 1 end
  | Lc q ((b, n) :: ls, t) r =>
      if is_zero n then 0 else match cL_idx q b with Some _ => if all4 (lv n) then lc n else 1 | None => 1 end
  | _ => 1
  end%N.

(* run until the TM step count reaches T exactly; return ssim step count *)
Definition gostep (T : N) (st : N * N * cfg * bool) : N * N * cfg * bool :=
  let '(k, t, c, stop) := st in
  if stop then st else
  if N.eqb t T then (k, t, c, true) else
  let w := cost c in
  if N.ltb T (t + w) then (k, t, c, true) else
  match sstep c with Some (c', _) => (N.succ k, (t + w)%N, c', false) | None => (k, t, c, true) end.

Definition go (fuel : positive) (T : N) (c : cfg) := Pos.iter (gostep T) (0%N, 0%N, c, false) fuel.

Definition c00 := Rc A ([], T0) ([], T0).

Definition res28 := go 1000000000 2629088227408 c00.
Time Eval native_compute in (let '(k, t, c, s) := res28 in (k, t, s, c)).