check_kill: compiling temp copy (timeout 1800s, -native-compiler yes) ... check_kill /home/dennis/projects/bb6-hunt/machines/1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---/1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---.v tm 1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE--- | mode halt | theorem `halt` | sha256 30ba969372712e44 ------------------------------------------------------------------------------ [PASS] args arguments: TM string format and mode 6x2 machine, framework module Individual62, mode halt [PASS] input input file: readable UTF-8 .v outside vendor/, lexically complete 23312 bytes, 838 lines, 470 sentences [PASS] framework (a) busycoq HEAD == tools/busycoq.pin, no tracked changes under verify/ HEAD 0940bb9cf434ba68f0c025dabfde45a219999973 == pin; no tracked changes under verify/ [PASS] framework_build (a) every framework .vo the file needs is built and newer than its .v, with its native code 19 needed framework .vo files present and fresh, with native code no older than the .vo [PASS] forbidden (d) forbidden tokens anywhere in the file (comments and strings included) none of 30 forbidden patterns occur (ground rule 1's words: anywhere; command words: outside comments and strings; comments never split a token) [PASS] structure (d) Require allowlist, no top-level Variable/Context, no shadowing, balanced modules 11 Require name(s) allowed; no top-level Variable/Context; no shadowing; Module/Section balanced line 25: From BusyCoq Require Individual62 -> framework Individual62.v line 26: Require Lia -> Coq stdlib line 27: Require ZArith -> Coq stdlib line 28: Require NArith -> Coq stdlib line 29: Require String -> Coq stdlib line 30: Require List -> Coq stdlib line 31: From BusyCoq Require BinaryCounter_v2 -> framework BinaryCounter_v2.v line 32: From BusyCoq Require NatMod -> framework NatMod.v line 33: From BusyCoq Require SimplTape -> framework SimplTape.v line 34: From BusyCoq Require Longitudinal -> framework Longitudinal.v line 35: From BusyCoq Require Eqb -> framework Eqb.v [PASS] tm_text (b) TM_from_str literal of the top-level `Definition tm` == byte for byte line 39: TM_from_str "1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---" == (41 bytes) [PASS] theorem_text (c) exactly one top-level `halt : halts tm c0` (text) line 797: halt : halts tm c0 [PASS] coq Coq toolchain coqc 8.20.1 (/home/dennis/.opam/bb6/bin/coqc) [PASS] names absolute names of the framework's halts / c0 / TM_from_str (probe) halts, c0, TM_from_str resolved inside Individual62 halts = BusyCoq.Individual62.Individual62.Enumerate.Permute.Flip.Compute.TM.halts c0 = BusyCoq.Individual62.Individual62.Enumerate.Permute.Flip.Compute.TM.c0 TM_from_str = BusyCoq.Individual62.TM_from_str [PASS] compile (f) temp copy + appended checks compile within 1800s, flags from verify/_CoqProject compiled in 25.6s with all appended checks command: /home/dennis/.opam/bb6/bin/coqc -q -Q /home/dennis/projects/bb6-hunt/vendor/busycoq/verify BusyCoq -Q /home/dennis/projects/bb6-hunt/vendor/busycoq/verify/BigInt BigInt -Q /tmp/check_kill.j3kwaq77/kill BB6Kill -native-compiler yes Candidate.v wall time: 25.6s warning: -native-compiler yes: native code is in the trusted base unless coqchk finishes (policy A) warning: Warning: /home/dennis/projects/bb6-hunt/vendor/busycoq/verify/BigInt was warning: Warning: The native-compiler option is deprecated. To compile native files warning: Warning: Notation "_ || _" was already used in scope bool_scope. warning: Warning: Notation "_ && _" was already used in scope bool_scope. [PASS] tm_rocq (b) Rocq: tm = TM_from_str "" by eq_refl (in-file + isolated checker) BB6Kill.Candidate.tm = BusyCoq.Individual62.TM_from_str "1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---" by eq_refl (in-file and isolated) in-file tm_conv: ok isolated tm_conv: ok [PASS] theorem_rocq (c) Rocq: halt : halts tm c0 with absolute names (in-file + isolated checker) halt : halts (TM_from_str "1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---") c0 with absolute names (in-file and isolated) in-file halt : halts tm c0: ok in-file halt : halts (TM_from_str lit) c0: ok isolated halt : halts tm c0: ok isolated halt : halts (TM_from_str lit) c0: ok [PASS] isolation (g) isolated checker: stock proof plugins only; kernel checks on, definitional UIP off only stock proof plugins loaded; guard/positivity/universe checking on, definitional UIP off isolated checker plugins and typing flags: ok ML modules: ltac_plugin.cmxs, number_string_notation_plugin.cmxs, tauto_plugin.cmxs, cc_plugin.cmxs, firstorder_plugin.cmxs, ring_plugin.cmxs, zify_plugin.cmxs, micromega_core_plugin.cmxs, micromega_plugin.cmxs, btauto_plugin.cmxs [PASS] assumptions (e) Print Assumptions halt within tools/assumptions_baseline.txt 1 assumption(s), all in the baseline isolated Print Assumptions (1): Axioms|FunctionalExtensionality.functional_extensionality_dep : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x), (forall x : A, f x = g x) -> f = g baseline entries (1): Axioms|FunctionalExtensionality.functional_extensionality_dep : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x), (forall x : A, f x = g x) -> f = g [PASS] coqchk (h) coqchk -norec re-checks the compiled candidate (VM/native steps included) coqchk -norec BB6Kill.Candidate ok (43.3s); its context summary lists nothing of the file's own [PASS] integrity input file and framework unchanged during the run input sha256 and framework HEAD/cleanliness identical before and after ------------------------------------------------------------------------------ RESULT: PASS -- this is a kill JSON: {"tool":"check_kill","tool_version":4,"result":"PASS","exit":0,"file":"/home/dennis/projects/bb6-hunt/machines/1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---/1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---.v","sha256":"30ba969372712e441c93cb004872c9f78e9361ea47fb3e8e96c66957fc076786","tm":"1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---","mode":"halt","theorem":"halt","framework_head":"0940bb9cf434ba68f0c025dabfde45a219999973","coqc":"/home/dennis/.opam/bb6/bin/coqc","coqc_version":"8.20.1","compile_seconds":25.61,"native_compiler":"yes","coqchk":"pass","coqchk_timeout":600,"coqchk_seconds":43.32,"ml_modules":["ltac_plugin.cmxs","number_string_notation_plugin.cmxs","tauto_plugin.cmxs","cc_plugin.cmxs","firstorder_plugin.cmxs","ring_plugin.cmxs","zify_plugin.cmxs","micromega_core_plugin.cmxs","micromega_plugin.cmxs","btauto_plugin.cmxs"],"fqns":{"halts":"BusyCoq.Individual62.Individual62.Enumerate.Permute.Flip.Compute.TM.halts","c0":"BusyCoq.Individual62.Individual62.Enumerate.Permute.Flip.Compute.TM.c0","TM_from_str":"BusyCoq.Individual62.TM_from_str"},"assumptions":["Axioms|FunctionalExtensionality.functional_extensionality_dep : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x), (forall x : A, f x = g x) -> f = g"],"checked_at":"2026-10-13T11:35:43Z","checks":[{"id":"args","status":"PASS","summary":"6x2 machine, framework module Individual62, mode halt","details":[],"warnings":[]},{"id":"input","status":"PASS","summary":"23312 bytes, 838 lines, 470 sentences","details":[],"warnings":[]},{"id":"framework","status":"PASS","summary":"HEAD 0940bb9cf434ba68f0c025dabfde45a219999973 == pin; no tracked changes under verify/","details":[],"warnings":[]},{"id":"framework_build","status":"PASS","summary":"19 needed framework .vo files present and fresh, with native code no older than the .vo","details":[],"warnings":[]},{"id":"forbidden","status":"PASS","summary":"none of 30 forbidden patterns occur (ground rule 1's words: anywhere; command words: outside comments and strings; comments never split a token)","details":[],"warnings":[]},{"id":"structure","status":"PASS","summary":"11 Require name(s) allowed; no top-level Variable/Context; no shadowing; Module/Section balanced","details":["line 25: From BusyCoq Require Individual62 -> framework Individual62.v","line 26: Require Lia -> Coq stdlib","line 27: Require ZArith -> Coq stdlib","line 28: Require NArith -> Coq stdlib","line 29: Require String -> Coq stdlib","line 30: Require List -> Coq stdlib","line 31: From BusyCoq Require BinaryCounter_v2 -> framework BinaryCounter_v2.v","line 32: From BusyCoq Require NatMod -> framework NatMod.v","line 33: From BusyCoq Require SimplTape -> framework SimplTape.v","line 34: From BusyCoq Require Longitudinal -> framework Longitudinal.v","line 35: From BusyCoq Require Eqb -> framework Eqb.v"],"warnings":[]},{"id":"tm_text","status":"PASS","summary":"line 39: TM_from_str \"1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---\" == (41 bytes)","details":[],"warnings":[]},{"id":"theorem_text","status":"PASS","summary":"line 797: halt : halts tm c0","details":[],"warnings":[]},{"id":"coq","status":"PASS","summary":"coqc 8.20.1 (/home/dennis/.opam/bb6/bin/coqc)","details":[],"warnings":[]},{"id":"names","status":"PASS","summary":"halts, c0, TM_from_str resolved inside Individual62","details":["halts = BusyCoq.Individual62.Individual62.Enumerate.Permute.Flip.Compute.TM.halts","c0 = BusyCoq.Individual62.Individual62.Enumerate.Permute.Flip.Compute.TM.c0","TM_from_str = BusyCoq.Individual62.TM_from_str"],"warnings":[]},{"id":"compile","status":"PASS","summary":"compiled in 25.6s with all appended checks","details":["command: /home/dennis/.opam/bb6/bin/coqc -q -Q /home/dennis/projects/bb6-hunt/vendor/busycoq/verify BusyCoq -Q /home/dennis/projects/bb6-hunt/vendor/busycoq/verify/BigInt BigInt -Q /tmp/check_kill.j3kwaq77/kill BB6Kill -native-compiler yes Candidate.v","wall time: 25.6s"],"warnings":["-native-compiler yes: native code is in the trusted base unless coqchk finishes (policy A)","Warning: /home/dennis/projects/bb6-hunt/vendor/busycoq/verify/BigInt was","Warning: The native-compiler option is deprecated. To compile native files","Warning: Notation \"_ || _\" was already used in scope bool_scope.","Warning: Notation \"_ && _\" was already used in scope bool_scope."]},{"id":"tm_rocq","status":"PASS","summary":"BB6Kill.Candidate.tm = BusyCoq.Individual62.TM_from_str \"1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---\" by eq_refl (in-file and isolated)","details":["in-file tm_conv: ok","isolated tm_conv: ok"],"warnings":[]},{"id":"theorem_rocq","status":"PASS","summary":"halt : halts (TM_from_str \"1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---\") c0 with absolute names (in-file and isolated)","details":["in-file halt : halts tm c0: ok","in-file halt : halts (TM_from_str lit) c0: ok","isolated halt : halts tm c0: ok","isolated halt : halts (TM_from_str lit) c0: ok"],"warnings":[]},{"id":"isolation","status":"PASS","summary":"only stock proof plugins loaded; guard/positivity/universe checking on, definitional UIP off","details":["isolated checker plugins and typing flags: ok","ML modules: ltac_plugin.cmxs, number_string_notation_plugin.cmxs, tauto_plugin.cmxs, cc_plugin.cmxs, firstorder_plugin.cmxs, ring_plugin.cmxs, zify_plugin.cmxs, micromega_core_plugin.cmxs, micromega_plugin.cmxs, btauto_plugin.cmxs"],"warnings":[]},{"id":"assumptions","status":"PASS","summary":"1 assumption(s), all in the baseline","details":["isolated Print Assumptions (1): Axioms|FunctionalExtensionality.functional_extensionality_dep : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x), (forall x : A, f x = g x) -> f = g","baseline entries (1): Axioms|FunctionalExtensionality.functional_extensionality_dep : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x), (forall x : A, f x = g x) -> f = g"],"warnings":[]},{"id":"coqchk","status":"PASS","summary":"coqchk -norec BB6Kill.Candidate ok (43.3s); its context summary lists nothing of the file's own","details":[],"warnings":[]},{"id":"integrity","status":"PASS","summary":"input sha256 and framework HEAD/cleanliness identical before and after","details":[],"warnings":[]}]}