def iteration_refines_model

stelliferous@0.0.2.0 · proofs/loop_projection.bend:10

import Base
import stelliferous@0.0.2.0/traversal_loop.bend as Loop

10# A single commuting step lifts to every count. RuntimeState may own arrays;
11# only the model is duplicated in the proof. No runtime array is cloned.
12def iteration_refines_model(
13  ~RuntimeState: Type,~ModelState: Data,
14  ~runtime_step: RuntimeState -> RuntimeState,~model_step: ModelState -> ModelState,
15  ~represent: ModelState -> RuntimeState,
16  ~step_matches: @+state: ModelState -> {runtime_step(represent(state)) == represent(model_step(state)) : RuntimeState},
17  +count: Nat,+state: ModelState
18) -> {Loop.run(~RuntimeState,~runtime_step,count,represent(state)) == represent(Loop.run(~ModelState,~model_step,count,state)) : RuntimeState}:
19  match count:
20    case 0n: {==}
21    case 1n+ +rest:
22      %Equal.sym(RuntimeState,runtime_step(represent(state)),represent(model_step(state)),step_matches(state)) :
23        {Loop.run(~RuntimeState,~runtime_step,rest,_) == represent(Loop.run(~ModelState,~model_step,rest,model_step(state))) : RuntimeState}
24      iteration_refines_model(~RuntimeState,~ModelState,~runtime_step,~model_step,~represent,~step_matches,rest,model_step(state))