No more, no less: A formal model for serverless computing