R3: whole SYSTEM-call Ξ correspondence

[Th0rgal]

Summary

• compose a complete SYSTEM-call Ξ prefix through RETURN / REVERT into an observational result
• relate the pinned predeploy account to the abstract model with a minimal main-based Represents relation
• keep the existing A-ABSTRACT-TX gap explicit as the named EndpointAgrees premise
• carry exactly the existing P-SUBMIT-1, P-DRAIN-1, and P-CONTROL-1 parents; add no assurance IDs and leave kill-lines unchanged
• update EVMYulLean to the required d164b61b995f4f553e975db9cfe3640d0aeefafa pin

Verification

• lake build EvmYul.FFI.ffi:dynlib
• lake build Eip8282.Audit.SystemXiCorrespondence
• make prove
• python3 scripts/audit_metadata.py

All pass locally.

Honest open dependency

whole_system_call_xi_correspondence requires EndpointAgrees as an explicit theorem argument. This is the existing OPEN A-ABSTRACT-TX; the PR does not claim to close it.