Simple proof of {Linz, Siper, Kozen} counter-example decidability

[olcott]

The simplest way to understand that a halt decider could correctly
decide the {Linz, Siper, Kozen} counter-examples (shown here as H_Hat)
is to see what happens when we define a halt decider that simply
simulates its input and returns True only after its input terminates (if
ever).

#define HALT __asm hlt

void H_Hat(u32 P)
{
u32 Input_Halted = Simulate(P, P);
if (Input_Halts)
HERE: goto HERE;
else
HALT
}

int main()
{
u32 Input_Halted = Simulate((u32)H_Hat, (u32)H_Hat);
Output("Input_Halted =", Input_Halted);
HALT;
}

_H_Hat()
[000007ca](01) 55 push ebp
[000007cb](02) 8bec mov ebp,esp
[000007cd](01) 51 push ecx
[000007ce](03) 8b4508 mov eax,[ebp+08]
[000007d1](01) 50 push eax
[000007d2](03) 8b4d08 mov ecx,[ebp+08]
[000007d5](01) 51 push ecx
[000007d6](05) e80ffeffff call 000005ea
[000007db](03) 83c408 add esp,+08
[000007de](03) 8945fc mov [ebp-04],eax
[000007e1](04) 837dfc00 cmp dword [ebp-04],+00
[000007e5](02) 7404 jz 000007eb
[000007e7](02) ebfe jmp 000007e7
[000007e9](02) eb01 jmp 000007ec
[000007eb](01) f4 hlt
[000007ec](02) 8be5 mov esp,ebp
[000007ee](01) 5d pop ebp
[000007ef](01) c3 ret

_main()
[000007fa](01) 55 push ebp
[000007fb](02) 8bec mov ebp,esp
[000007fd](01) 51 push ecx
[000007fe](05) 68ca070000 push 000007ca
[00000803](05) 68ca070000 push 000007ca
[00000808](05) e8ddfdffff call 000005ea
[0000080d](03) 83c408 add esp,+08
[00000810](03) 8945fc mov [ebp-04],eax
[00000813](03) 8b45fc mov eax,[ebp-04]
[00000816](01) 50 push eax
[00000817](05) 68d7020000 push 000002d7
[0000081c](05) e8e9faffff call 0000030a
[00000821](03) 83c408 add esp,+08
[00000824](01) f4 hlt
[00000825](02) 8be5 mov esp,ebp
[00000827](01) 5d pop ebp
[00000828](01) c3 ret

Output_Debug_Trace() Trace_List.size(30)
---[000007fa](01) 55 push ebp
---[000007fb](02) 8bec mov ebp,esp
---[000007fd](01) 51 push ecx
---[000007fe](05) 68ca070000 push 000007ca
---[00000803](05) 68ca070000 push 000007ca
---[00000808](05) e8ddfdffff call 000005ea --CALL [000005ea]
---[000007ca](01) 55 push ebp
---[000007cb](02) 8bec mov ebp,esp
---[000007cd](01) 51 push ecx
---[000007ce](03) 8b4508 mov eax,[ebp+08]
---[000007d1](01) 50 push eax
---[000007d2](03) 8b4d08 mov ecx,[ebp+08]
---[000007d5](01) 51 push ecx
---[000007d6](05) e80ffeffff call 000005ea --CALL [000005ea]
---[000007ca](01) 55 push ebp
---[000007cb](02) 8bec mov ebp,esp
---[000007cd](01) 51 push ecx
---[000007ce](03) 8b4508 mov eax,[ebp+08]
---[000007d1](01) 50 push eax
---[000007d2](03) 8b4d08 mov ecx,[ebp+08]
---[000007d5](01) 51 push ecx
---[000007d6](05) e80ffeffff call 000005ea --CALL [000005ea]
... the last 8 lines infinitely repeat.

Every time that the same function is called from the same machine
address a second time (within an execution trace) without any control
flow instructions in-between is a case of infinite recursion. This is
shown at execution trace lines 14-22 above.

(1) The C code does map to its machine code.
(2) The machine code does map to its execution trace (when Halts() is a
simulator).
(3) The execution trace does map to infinite recursion.

The semantics specified by the syntax of the formal x86 language proves
(2) and (3).



--
Copyright 2020 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein