On 7/5/2022 8:47 AM, Paul N wrote:
The correctly emulated input to H(P,P) is an entirely different sequence
of configurations than the directly executed P(P). This is conclusively
proved by the provably correct execution trace of each.
Example 04: P(P) halts because H(P,P) correctly determines that its
input never halts
void P(u32 x)
{
if (H(x, x))
HERE: goto HERE;
return;
}
int main()
{
P((u32)P);
}
_P()
[000011f0](01) 55 push ebp
[000011f1](02) 8bec mov ebp,esp
[000011f3](03) 8b4508 mov eax,[ebp+08]
[000011f6](01) 50 push eax
[000011f7](03) 8b4d08 mov ecx,[ebp+08]
[000011fa](01) 51 push ecx
[000011fb](05) e820feffff call 00001020
[00001200](03) 83c408 add esp,+08
[00001203](02) 85c0 test eax,eax
[00001205](02) 7402 jz 00001209
[00001207](02) ebfe jmp 00001207
[00001209](01) 5d pop ebp
[0000120a](01) c3 ret
Size in bytes:(0027) [0000120a]
_main()
[00001210](01) 55 push ebp
[00001211](02) 8bec mov ebp,esp
[00001213](05) 68f0110000 push 000011f0
[00001218](05) e8d3ffffff call 000011f0
[0000121d](03) 83c404 add esp,+04
[00001220](02) 33c0 xor eax,eax
[00001222](01) 5d pop ebp
[00001223](01) c3 ret
Size in bytes:(0020) [00001223]
machine stack stack machine assembly
address address data code language
======== ======== ======== ========= =============
[00001210][00101fba][00000000] 55 push ebp
[00001211][00101fba][00000000] 8bec mov ebp,esp
[00001213][00101fb6][000011f0] 68f0110000 push 000011f0 // push P
[00001218][00101fb2][0000121d] e8d3ffffff call 000011f0 // call P
[000011f0][00101fae][00101fba] 55 push ebp // enter executed P
[000011f1][00101fae][00101fba] 8bec mov ebp,esp
[000011f3][00101fae][00101fba] 8b4508 mov eax,[ebp+08]
[000011f6][00101faa][000011f0] 50 push eax // push P
[000011f7][00101faa][000011f0] 8b4d08 mov ecx,[ebp+08]
[000011fa][00101fa6][000011f0] 51 push ecx // push P
[000011fb][00101fa2][00001200] e820feffff call 00001020 // call H
Begin Simulation Execution Trace Stored at:21206e
Address_of_H:1020
[000011f0][0021205a][0021205e] 55 push ebp // enter emulated P
[000011f1][0021205a][0021205e] 8bec mov ebp,esp
[000011f3][0021205a][0021205e] 8b4508 mov eax,[ebp+08]
[000011f6][00212056][000011f0] 50 push eax // push P
[000011f7][00212056][000011f0] 8b4d08 mov ecx,[ebp+08]
[000011fa][00212052][000011f0] 51 push ecx // push P
[000011fb][0021204e][00001200] e820feffff call 00001020 // call emulated H
Infinitely Recursive Simulation Detected Simulation Stopped
H knows its own machine address and on this basis it can easily
examine its stored execution_trace of P (see above) to determine:
(a) P is calling H with the same arguments that H was called with.
(b) No instructions in P could possibly escape this otherwise infinitely
recursive emulation.
(c) H aborts its emulation of P before its call to H is emulated.
From a purely software engineering perspective (anchored in the
semantics of the x86 language) it is proven that H(P,P) correctly
predicts that its correct and complete x86 emulation of its input would
never reach the "ret" instruction (final state) of this input.
[00001200][00101fae][00101fba] 83c408 add esp,+08 // return to
executed P
[00001203][00101fae][00101fba] 85c0 test eax,eax
[00001205][00101fae][00101fba] 7402 jz 00001209
[00001209][00101fb2][0000121d] 5d pop ebp
[0000120a][00101fb6][000011f0] c3 ret // return from
executed P
[0000121d][00101fba][00000000] 83c404 add esp,+04
[00001220][00101fba][00000000] 33c0 xor eax,eax
[00001222][00101fbe][00100000] 5d pop ebp
[00001223][00101fc2][00000000] c3 ret // ret from main
Number of Instructions Executed(878) / 67 = 13 pages