Static desk checking confirms that Halts(H_Hat, H_Hat) == 0 is correct

[olcott]

For partial halt deciders defined according to the following design it
can be confirmed by desk checking that Halts(H_Hat, H_Hat) would never
halt unless Halts stops simulating it.


Every partial halt decider H that that bases its halting decision
on simulating its input P until criteria (1)(2)(3) are met by the
execution trace of P correctly decides not halting on input P.

If the execution trace of function P() [i.e. the input to H] shows:
(1) Partial halt decider H is called twice in sequence from the same
machine address of P.
(2) with the same machine address parameters to H
(3) with no conditional branch or indexed jump instructions in P
then H correctly decides not halting on P.

void H_Hat(u32 P)
{
u32 Input_Halts = Halts(P, P);
if (Input_Halts)
HERE: goto HERE;
}

int main()
{
u32 Input_Would_Halt = Halts((u32)H_Hat, (u32)H_Hat);
Output("Input_Would_Halt = ", Input_Would_Halt);
}

_H_Hat()
[00000b1f](01) 55 push ebp
[00000b20](02) 8bec mov ebp,esp
[00000b22](01) 51 push ecx
[00000b23](03) 8b4508 mov eax,[ebp+08]
[00000b26](01) 50 push eax
[00000b27](03) 8b4d08 mov ecx,[ebp+08]
[00000b2a](01) 51 push ecx
[00000b2b](05) e82ffeffff call 0000095f
[00000b30](03) 83c408 add esp,+08
[00000b33](03) 8945fc mov [ebp-04],eax
[00000b36](04) 837dfc00 cmp dword [ebp-04],+00
[00000b3a](02) 7402 jz 00000b3e
[00000b3c](02) ebfe jmp 00000b3c
[00000b3e](02) 8be5 mov esp,ebp
[00000b40](01) 5d pop ebp
[00000b41](01) c3 ret
Size in bytes:(0035) [00000b41]

_main()
[00000b4f](01) 55 push ebp
[00000b50](02) 8bec mov ebp,esp
[00000b52](01) 51 push ecx
[00000b53](05) 681f0b0000 push 00000b1f
[00000b58](05) 681f0b0000 push 00000b1f
[00000b5d](05) e8fdfdffff call 0000095f
[00000b62](03) 83c408 add esp,+08
[00000b65](03) 8945fc mov [ebp-04],eax
[00000b68](03) 8b45fc mov eax,[ebp-04]
[00000b6b](01) 50 push eax
[00000b6c](05) 682b030000 push 0000032b
[00000b71](05) e8e9f7ffff call 0000035f
[00000b76](03) 83c408 add esp,+08
[00000b79](02) 33c0 xor eax,eax
[00000b7b](02) 8be5 mov esp,ebp
[00000b7d](01) 5d pop ebp
[00000b7e](01) c3 ret
Size in bytes:(0048) [00000b7e]

Columns
(1) Machine address of instruction
(2) Machine address of top of stack
(3) Value of top of stack after instruction executed
(4) Number of bytes of machine code
(5) Machine language bytes
(6) Assembly language text




01.[00000b4f][00101542][00000000](01) 55 push ebp
02.[00000b50][00101542][00000000](02) 8bec mov ebp,esp
03.[00000b52][0010153e][00000000](01) 51 push ecx
04.[00000b53][0010153a][00000b1f](05) 681f0b0000 push 00000b1f
05.[00000b58][00101536][00000b1f](05) 681f0b0000 push 00000b1f
06.[00000b5d][00101532][00000b62](05) e8fdfdffff call 0000095f

Begin Local Halt Decider Simulation at Machine Address:b1f
07.[00000b1f][002115e2][002115e6](01) 55 push ebp
08.[00000b20][002115e2][002115e6](02) 8bec mov ebp,esp
09.[00000b22][002115de][002015b2](01) 51 push ecx
10.[00000b23][002115de][002015b2](03) 8b4508 mov eax,[ebp+08]
11.[00000b26][002115da][00000b1f](01) 50 push eax
12.[00000b27][002115da][00000b1f](03) 8b4d08 mov ecx,[ebp+08]
13.[00000b2a][002115d6][00000b1f](01) 51 push ecx
14.[00000b2b][002115d2][00000b30](05) e82ffeffff call 0000095f

15.[00000b1f][0025c00a][0025c00e](01) 55 push ebp
16.[00000b20][0025c00a][0025c00e](02) 8bec mov ebp,esp
17.[00000b22][0025c006][0024bfda](01) 51 push ecx
18.[00000b23][0025c006][0024bfda](03) 8b4508 mov eax,[ebp+08]
19.[00000b26][0025c002][00000b1f](01) 50 push eax
20.[00000b27][0025c002][00000b1f](03) 8b4d08 mov ecx,[ebp+08]
21.[00000b2a][0025bffe][00000b1f](01) 51 push ecx
22.[00000b2b][0025bffa][00000b30](05) e82ffeffff call 0000095f
Local Halt Decider: Infinite Recursion Detected Simulation Stopped

(1) Halts is called twice in sequence from the same machine address of
H_Hat.
14.[00000b2b][002115d2][00000b30](05) e82ffeffff call 0000095f
22.[00000b2b][0025bffa][00000b30](05) e82ffeffff call 0000095f

(2) With the same machine address of H_Hat parameters to H
(Pair of push instructions preceding the call to Halts are its input)
11.[00000b26][002115da][00000b1f](01) 50 push eax
13.[00000b2a][002115d6][00000b1f](01) 51 push ecx

19.[00000b26][0025c002][00000b1f](01) 50 push eax
21.[00000b2a][0025bffe][00000b1f](01) 51 push ecx

(3) with no conditional branch or indexed jump instructions in H_Hat
None of the machine instructions from line 07 to line 22 are this type.

23.[00000b62][0010153e][00000000](03) 83c408 add esp,+08
24.[00000b65][0010153e][00000000](03) 8945fc mov
[ebp-04],eax
25.[00000b68][0010153e][00000000](03) 8b45fc mov
eax,[ebp-04]
26.[00000b6b][0010153a][00000000](01) 50 push eax
27.[00000b6c][00101536][0000032b](05) 682b030000 push 0000032b
28.[00000b71][00101532][00000b76](05) e8e9f7ffff call 0000035f
Input_Would_Halt = 0
29.[00000b76][0010153e][00000000](03) 83c408 add esp,+08
30.[00000b79][0010153e][00000000](02) 33c0 xor eax,eax
31.[00000b7b][00101542][00000000](02) 8be5 mov esp,ebp
32.[00000b7d][00101546][00100000](01) 5d pop ebp
33.[00000b7e][0010154a][00000080](01) c3 ret
Number_of_User_Instructions(33)
Number of Instructions Executed(26560)

Halting problem undecidability and infinitely nested simulation
http://www.liarparadox.org/Halting_problem_undecidability_and_infinitely_nested_simulation.pdf

--
Copyright 2021 Pete Olcott

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