Function plan_budgeted 

pub fn plan_budgeted(
    prog: &CompiledProgram,
    mode: ReverseMode,
    budget: usize,
) -> Vec<JournalDecision>

plan with an explicit pebble CHECKPOINT budget (corner 2). Under Adiabatic, budget recomputable chain intermediates are KEPT on the tape (journaled once — landauer = 0, since a recomputable scratch is first-def so its displaced value is Nothing) instead of upgraded to Recompute. A reverse step that reads a node above a checkpoint then re-walks only down to the nearest checkpoint, not to the chain root — the Bennett space-for-time trade. budget = 0 is the recompute-everything corner (O(1) tape, chain·reads time); higher budgets bound the re-walk length.