Refactor rules to generate constraints
 Rename rate -> size consistently.
 Use u^k as a size variable generator.
 Make the main interpretation function take a list of bindings directly.
 Add an interpretation for the top level function form.