How to relate abstract and concrete execution

[hkim15]

hafnium-verification/coq-verification/src/Concrete/Model.v

Line 79 in a500450

Lemma execution_represents

This looks like the key lemma that links between abstract/concrete states. Before looking at the code, I was expecting it'd establish more explicit relation between transitions. This would estalish more explicit correspondence between the abstract and concrete layer. For instance,

AbstractShare <-> api_share_memory(..., HF_MEMORY_SHARE, ...)
AbstractLend <-> api_lend_memory(..., HF_MEMORY_LEND, ...)

Have you considered this approach?