PrincetonUniversity
semax_external_funspec_sub
The lemma semax_external_funspec_sub in veric/semax.v is Admitted. There is a part at the end related to the aging of the ghost state. This should be fixed a.s.a.p., since it's part of the core soundness of VST.
Last time I talked to @lennartberinger about this axiom he said it should be true, but it's more of a sanity check than a rule of the logic, and could be removed from the SeparationLogic interface. It's not true as written because it needs a ghost-state update operator somewhere, but I haven't quite figured out where yet.
OK, now the lemma in question is "disabled" : one of its premises is (literally) False, so it's sound.