import Runtime.Proofs.VM.InstrSpec.Preservation
import Runtime.Proofs.VM.InstrSpec.ConfigEquivSendRecv
import Runtime.Proofs.VM.InstrSpec.ConfigEquivSelectBranch
import Runtime.Proofs.VM.InstrSpec.ConfigEquivOpenCloseTransfer
import Runtime.Proofs.VM.InstrSpec.ConfigEquivAcquire
import Runtime.Proofs.VM.InstrSpec.ErasureExactness
