and then you need to log in a VIP user or a debug user without auth but cant produce a proof so now it wont compile at all. not a problem i you own the code but in client/server a third party could be the client or server so will have to be very careful about placing proof obligations on code you dont own.