def iteration_result_and_work

stelliferous@0.0.2.0 · proofs/loop_projection.bend:67

import Base

67# Concrete adapters must establish cost_per_step; it is not a heap-cost claim.
68def iteration_result_and_work(
69  ~State: Data,~step: State -> State,~cost: State -> Nat,
70  ~width: Nat,
71  ~cost_per_step: @+state: State -> {cost(state) == width : Nat},
72  +count: Nat,+state: State
73) -> {measured_iteration(~State,~step,~cost,count,state) == Measured{iterate(~State,~step,count,state),Nat.mul(count,width)} : Measured<State>}:
74  match count:
75    case 0n: {==}
76    case 1n+ +rest:
77      %cost_per_step(state) : {add_work(State,cost(state),measured_iteration(~State,~step,~cost,rest,step(state))) == add_work(State,_,
78          Measured{iterate(~State,~step,rest,step(state)),Nat.mul(rest,width)}) : Measured<State>}
79      %iteration_result_and_work(~State,~step,~cost,~width,~cost_per_step,rest,step(state)) : {add_work(State,cost(state),
80          measured_iteration(~State,~step,~cost,rest,step(state))) == add_work(State,cost(state),_) : Measured<State>}
81      {==}