Library mcertikos.mm.ALInitGen
This file provide the contextual refinement proof between MBoot layer and MALInit layer
Require
Export
ALInitGenDef
.
Require
Export
ALInitGenFresh
.
Require
Export
ALInitGenPassthrough
.