Fitting the pieces together: a machine-checked model of safe composition