1 # One induction for every state representation, output index and step count. 2 import Base 3 import ./bounded_u32_arithmetic.bend as Arithmetic 4 import ./word_arithmetic.bend as WordArithmetic 5 import ../traversal_loop.bend as Loop 6 7 def iterate(~State: Data,~step: State -> State,count: Nat,state: State) -> State: 8 Loop.run(~State,~step,count,state) 9 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. 12 def 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)) 25 26 # A read-only observation is preserved for every number of iterations. 27 def preserves_observation( 28 ~State: Data,~Observation: Data,~step: State -> State,~observe: State -> Observation, 29 ~preserved: @+state: State -> {observe(step(state)) == observe(state) : Observation}, 30 +count: Nat,+state: State 31 ) -> {observe(iterate(~State,~step,count,state)) == observe(state) : Observation}: 32 match count: 33 case 0n: {==} 34 case 1n+ +rest: 35 %preserved(state) : {observe(iterate(~State,~step,rest,step(state))) == _ : Observation} 36 preserves_observation(~State,~Observation,~step,~observe,~preserved,rest,step(state)) 37 38 def iteration_matches_denotation( 39 ~Observation: Data,~State: Data, 40 ~Index: Data, 41 ~step: State -> State, 42 ~project: Index -> State -> Observation, 43 ~denote: Index -> Nat -> State -> Observation, 44 ~at_zero: @+index: Index -> @+state: State -> {project(index,state) == denote(index,0n,state) : Observation}, 45 ~after_step: @+index: Index -> @+count: Nat -> @+state: State -> {denote(index,count,step(state)) == denote(index,1n+count,state) : Observation}, 46 +count: Nat,+index: Index,+state: State 47 ) -> {project(index,iterate(~State,~step,count,state)) == denote(index,count,state) : Observation}: 48 match count: 49 case 0n: at_zero(index,state) 50 case 1n+ +rest: 51 %after_step(index,rest,state) : {project(index,iterate(~State,~step,rest,step(state))) == _ : Observation} 52 iteration_matches_denotation(~Observation,~State,~Index,~step,~project,~denote,~at_zero,~after_step,rest,index,step(state)) 53 54 type Measured<-State: Data> is Data: 55 Measured{result: State,work: Nat} 56 57 def add_work(-State: Data,work: Nat,tail: Measured) -> Measured: 58 Measured{result,remaining} = tail 59 Measured{result,Nat.add(work,remaining)} 60 61 def measured_iteration(~State: Data,~step: State -> State,~cost: State -> Nat,count: Nat,+state: State) -> Measured: 62 match count: 63 case 0n: Measured{state,0n} 64 case 1n+rest: 65 add_work(State,cost(state),measured_iteration(~State,~step,~cost,rest,step(state))) 66 67 # Concrete adapters must establish cost_per_step; it is not a heap-cost claim. 68 def 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}: 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} 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} 81 {==} 82 83 # Machine counters share the same modular progress theorem for any step size. 84 # Non-wrapping coordinate bounds are separate obligations of the caller. 85 86 def indexed_successor(+position: U32,+offset: Nat) -> 87 {(position + U32.from_nat(1n+offset) : U32) == ((position + 1 : U32) + U32.from_nat(offset) : U32) : U32}: 88 %WordArithmetic.native_add(1n,offset) : 89 {(position + _ : U32) == ((position + 1 : U32) + U32.from_nat(offset) : U32) : U32} 90 Equal.sym(U32,((position + 1 : U32) + U32.from_nat(offset) : U32),(position + (1 + U32.from_nat(offset) : U32) : U32), 91 Arithmetic.add_associative(position,1,U32.from_nat(offset))) 92 def add_counted_stride(+position: U32,+stride: Nat,+count: Nat) -> 93 {((position + U32.from_nat(stride) : U32) + U32.from_nat(Nat.mul(count,stride)) : U32) == 94 (position + U32.from_nat(Nat.mul(1n+count,stride)) : U32) : U32}: 95 Equal.trans(U32,((position + U32.from_nat(stride) : U32) + U32.from_nat(Nat.mul(count,stride)) : U32), 96 (position + (U32.from_nat(stride) + U32.from_nat(Nat.mul(count,stride)) : U32) : U32), 97 (position + U32.from_nat(Nat.mul(1n+count,stride)) : U32),Arithmetic.add_associative(position,U32.from_nat(stride),U32.from_nat(Nat.mul(count,stride))), 98 Equal.cong(U32,U32,value => (position + value : U32),(U32.from_nat(stride) + U32.from_nat(Nat.mul(count,stride)) : U32), 99 U32.from_nat(Nat.mul(1n+count,stride)),WordArithmetic.native_add(stride,Nat.mul(count,stride)))) 100 101 def counter_progress(~State: Data,~step: State -> State,~position: State -> U32,~stride: Nat, 102 ~advances: @+state: State -> {position(step(state)) == (position(state) + U32.from_nat(stride) : U32) : U32}, 103 +count: Nat,+state: State) -> 104 {position(iterate(~State,~step,count,state)) == (position(state) + U32.from_nat(Nat.mul(count,stride)) : U32) : U32}: 105 match count: 106 case 0n: Equal.sym(U32,(position(state) + 0 : U32),position(state),Arithmetic.add_zero(position(state))) 107 case 1n+ +rest: 108 %add_counted_stride(position(state),stride,rest) : {position(iterate(~State,~step,rest,step(state))) == _ : U32} 109 %advances(state) : {position(iterate(~State,~step,rest,step(state))) == (_ + U32.from_nat(Nat.mul(rest,stride)) : U32) : U32} 110 counter_progress(~State,~step,~position,~stride,~advances,rest,step(state)) 111 112 # The final step is applied once, to the state the loop ends in. 113 def run_then_finishes(~State: Type,~Result: Type,~step: State -> State,~finish: State -> Result,count: Nat,-state: State) -> 114 {Loop.run_then(~State,~Result,~step,~finish,count,state) == finish(Loop.run(~State,~step,count,state)) : Result}: 115 match count: 116 case 0n: {==} 117 case 1n+rest: run_then_finishes(~State,~Result,~step,~finish,rest,step(state))