Library mcertikos.ipc.IPCIntroGen


This file provide the contextual refinement proof between PKContextNew layer and PThreadIntro layer
Require Export IPCIntroGenDef.
Require Export IPCIntroGenFresh.
Require Export IPCIntroGenPassthrough.