For some reason if (config_set(CONFIG_HAVE_FPU)) doesn't work to hide things. Easily fixed by creating an empty fpuRelease, but I wouldn't expect that would be necessary. Any suggestions?

Edit: I fixed it by using ifdef.

@chrisguikema If you have time, could you review and test the x86 VCPU changes on your VmMs? Would be good to know whether there is a performance degradation too. I don't expect any, but if there is, it's probably a bug.

I'm not sure if the guest's requested CR0:TS is being preserved or not (because I clear TS when unconditionally enabling the FPU for the guest). Is the CR0 used by guests the same as the CR0 used by hosts, or does it have its own architectural copy? I guess it has it's own copy because of VMX_GUEST_CR0, but not sure what the interaction is with CR0.

Edit: Or was it @Furao who promised me this at the summit? I forgot.

Just a couple of last changes that we'd like to make to this for verification. Would it be ok to move prepareSetDomain out of setDomain and into decodeDomainInvocation? That matches up better with how the specifications have been written and allows us to separate out the proofs about FPU and domain state.

Separately, we need to label enableFpu with MODIFIES: phantom_machine_state, as it us where we currently have the machine interface for the proofs and we need to know that it only modifies state that is not in the model.

See corlewis@ef617bc for the versions of these changes that I've been working with.

Also, when you have a chance another rebase would be helpful, to get the most recent verification-visible changes.

With these we're able to complete the functional correctness proofs for AArch64 and expect the other architectures to be relatively straightforward (although keeping in mind that the verified x86 configuration does not have hypervisor support so we won't have to handle the complications there that you've been dealing with).

Just a couple of last changes that we'd like to make to this for verification. Would it be ok to move prepareSetDomain out of setDomain and into decodeDomainInvocation? That matches up better with how the specifications have been written and allows us to separate out the proofs about FPU and domain state.

Oh, I've just realised that if we do make this change then for consistency we should probably wrap them up in a new invokeDomain function and call that from decodeDomainInvocation, like we do with all of the other decode functions.

Okay, done. Let me know if this is fine.

Okay, done. Let me know if this is fine.

Sorry, I thought that the new invokeDomainSetSet function would be fine but it returning an exception causes a surprising amount of pain in the proofs. Do you have any objections to making it a void function, like in corlewis@c852075? With that I've been able to update all of the proofs. There is also a precedent for this pattern in the various invokeIRQHandler functions that can be seen at https://github.com/seL4/seL4/blob/master/src/object/interrupt.c#L86.

Sorry, I thought that the new invokeDomainSetSet function would be fine but it returning an exception causes a surprising amount of pain in the proofs. Do you have any objections to making it a void function, like in corlewis@c852075?

That's surprising, as that's how all other invoke functions are in that file. Actually, looking at all invoke functions, only the IRQ ones are void, all others return exception_t. I have no objection to changing it, but it might be worth looking into why this one is so hard compared to the others? Perhaps you can simplify the proofs a lot if you change the other invoke functions to void too.

That's surprising, as that's how all other invoke functions are in that file. Actually, looking at all invoke functions, only the IRQ ones are void, all others return exception_t. I have no objection to changing it, but it might be worth looking into why this one is so hard compared to the others? Perhaps you can simplify the proofs a lot if you change the other invoke functions to void too.

Honestly, in this case a fair bit of the pain is probably because I already had working proofs and I'm now trying to minimise the changes I'm making for invokeDomainSetSet. If we'd had this from the start I would have just copied the specifications and proofs of the other functions and it would presumably have been fine.

One thing when considering the other invoke functions is that some of them actually can be preempted and return an exception, so those ones can't be changed to void. Now that I've done this though I think that in the cases where they can't be preempted it actually is nicer to be void, but I don't think that it's enough of an improvement to be worth going through and updating them.

One thing when considering the other invoke functions is that some of them actually can be preempted and return an exception, so those ones can't be changed to void. Now that I've done this though I think that in the cases where they can't be preempted it actually is nicer to be void, but I don't think that it's enough of an improvement to be worth going through and updating them.

When there is a quiet period at some point, we should consider it, because it is one of the rare cases where the C type systems actually does help a little bit on the C side (when it returns void we know there is no preemption). Axel had a pull request up a while ago to change some of the existing invocations, but I never got around to doing the update. For the same reasons we don't want to do them now :-), but not because it's a bad idea as such.

Tests are looking good now, I'll rebase for the cmake restyling.

Alright, things are finally passing. The link check is failing on the RFC link that will only exist once merged, and the zcu106 is failure is unrelated.

Will go ahead with the merge!