Composing computations within a fixed workspace budget

The fun_prop rules in this module preserve the budget in ComputableInSpace. They compose existing arithmetic, list, option and conditional certificates. Composition uses a routine whose workspace is linear in its own encoded argument; the caller's certificate pays for that argument. No rule infers a bound on the states of an iteration.

Constants and the identity require the input encoding length to fit the requested budget. That side condition is explicit, including when the budget is not the input length.

theorem Turing.MultiTapeTM.ComputableInSpace.budget_id {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} (h : BigOLe (fun (a : α) => (enc a).length) S) : ComputableInSpace (fun (a : α) => a) enc enc S

Copy an encoded value when the caller's budget covers its input length.