1 # One induction for every state representation, output index and step count. 2 import Base 3 import ./natural_addition.bend as Addition 4 import ./bounded_u32_arithmetic.bend as Arithmetic 5 import ./word_arithmetic.bend as WordArithmetic 6 import ./nat_order.bend as Order 7 import ./nat_division_order.bend as DivisionOrder 8 import ../traversal_loop.bend as Loop 9 10 def iterate(~State: Data,~step: State -> State,count: Nat,state: State) -> State: 11 Loop.run(~State,~step,count,state) 12 13 def iteration_split(~State: Type,~step: State -> State,first: Nat,+second: Nat,-state: State) -> 14 {Loop.run(~State,~step,Nat.add(first,second),state) == Loop.run(~State,~step,second,Loop.run(~State,~step,first,state)) : State}: 15 match first: 16 case 0n: {==} 17 case 1n+rest: iteration_split(~State,~step,rest,second,step(state)) 18 19 # count runs of a step that is eight steps are 8 * count steps. 20 def eights(~State: Type,~step: State -> State,~eight: State -> State, 21 ~grouped: @-state: State -> {eight(state) == Loop.run(~State,~step,8n,state) : State},count: Nat,-state: State) -> 22 {Loop.run(~State,~eight,count,state) == Loop.run(~State,~step,Nat.mul(count,8n),state) : State}: 23 match count: 24 case 0n: {==} 25 case 1n+ +rest: 26 %Equal.sym(State,eight(state),Loop.run(~State,~step,8n,state),grouped(state)) : 27 {Loop.run(~State,~eight,rest,_) == Loop.run(~State,~step,Nat.mul(1n+rest,8n),state) : State} 28 %Equal.sym(State,Loop.run(~State,~step,Nat.add(8n,Nat.mul(rest,8n)),state),Loop.run(~State,~step,Nat.mul(rest,8n),Loop.run(~State,~step,8n,state)), 29 iteration_split(~State,~step,8n,Nat.mul(rest,8n),state)) : 30 {Loop.run(~State,~eight,rest,Loop.run(~State,~step,8n,state)) == _ : State} 31 eights(~State,~step,~eight,~grouped,rest,Loop.run(~State,~step,8n,state)) 32 33 # The first count % 8 steps one by one, then the rest eight at a time. 34 def head_then_eights(~State: Type,~step: State -> State,~eight: State -> State, 35 ~grouped: @-state: State -> {eight(state) == Loop.run(~State,~step,8n,state) : State},+count: Nat,-state: State) -> 36 {Loop.run(~State,~eight,Nat.div(count,8n),Loop.run(~State,~step,Nat.mod(count,8n),state)) == Loop.run(~State,~step,count,state) : State}: 37 +rounds = Nat.mul(Nat.div(count,8n),8n) 38 +head = Nat.mod(count,8n) 39 %Equal.sym(Nat,count,Nat.add(rounds,head),DivisionOrder.quotient_exact(count,8n,{==})) : 40 {Loop.run(~State,~eight,Nat.div(count,8n),Loop.run(~State,~step,head,state)) == Loop.run(~State,~step,_,state) : State} 41 %Order.commutative(head,rounds) : 42 {Loop.run(~State,~eight,Nat.div(count,8n),Loop.run(~State,~step,head,state)) == Loop.run(~State,~step,_,state) : State} 43 %Equal.sym(State,Loop.run(~State,~step,Nat.add(head,rounds),state),Loop.run(~State,~step,rounds,Loop.run(~State,~step,head,state)), 44 iteration_split(~State,~step,head,rounds,state)) : 45 {Loop.run(~State,~eight,Nat.div(count,8n),Loop.run(~State,~step,head,state)) == _ : State} 46 eights(~State,~step,~eight,~grouped,Nat.div(count,8n),Loop.run(~State,~step,head,state)) 47 48 # A single commuting step lifts to every count. RuntimeState may own arrays; 49 # only the model is duplicated in the proof. No runtime array is cloned. 50 def iteration_refines_model( 51 ~RuntimeState: Type,~ModelState: Data, 52 ~runtime_step: RuntimeState -> RuntimeState,~model_step: ModelState -> ModelState, 53 ~represent: ModelState -> RuntimeState, 54 ~step_matches: @+state: ModelState -> {runtime_step(represent(state)) == represent(model_step(state)) : RuntimeState}, 55 +count: Nat,+state: ModelState 56 ) -> {Loop.run(~RuntimeState,~runtime_step,count,represent(state)) == represent(Loop.run(~ModelState,~model_step,count,state)) : RuntimeState}: 57 match count: 58 case 0n: {==} 59 case 1n+ +rest: 60 %Equal.sym(RuntimeState,runtime_step(represent(state)),represent(model_step(state)),step_matches(state)) : 61 {Loop.run(~RuntimeState,~runtime_step,rest,_) == represent(Loop.run(~ModelState,~model_step,rest,model_step(state))) : RuntimeState} 62 iteration_refines_model(~RuntimeState,~ModelState,~runtime_step,~model_step,~represent,~step_matches,rest,model_step(state)) 63 64 # A read-only observation is preserved for every number of iterations. 65 def preserves_observation( 66 ~State: Data,~Observation: Data,~step: State -> State,~observe: State -> Observation, 67 ~preserved: @+state: State -> {observe(step(state)) == observe(state) : Observation}, 68 +count: Nat,+state: State 69 ) -> {observe(iterate(~State,~step,count,state)) == observe(state) : Observation}: 70 match count: 71 case 0n: {==} 72 case 1n+ +rest: 73 %preserved(state) : {observe(iterate(~State,~step,rest,step(state))) == _ : Observation} 74 preserves_observation(~State,~Observation,~step,~observe,~preserved,rest,step(state)) 75 76 def iteration_matches_denotation( 77 ~Observation: Data,~State: Data, 78 ~Index: Data, 79 ~step: State -> State, 80 ~project: Index -> State -> Observation, 81 ~denote: Index -> Nat -> State -> Observation, 82 ~at_zero: @+index: Index -> @+state: State -> {project(index,state) == denote(index,0n,state) : Observation}, 83 ~after_step: @+index: Index -> @+count: Nat -> @+state: State -> {denote(index,count,step(state)) == denote(index,1n+count,state) : Observation}, 84 +count: Nat,+index: Index,+state: State 85 ) -> {project(index,iterate(~State,~step,count,state)) == denote(index,count,state) : Observation}: 86 match count: 87 case 0n: at_zero(index,state) 88 case 1n+ +rest: 89 %after_step(index,rest,state) : {project(index,iterate(~State,~step,rest,step(state))) == _ : Observation} 90 iteration_matches_denotation(~Observation,~State,~Index,~step,~project,~denote,~at_zero,~after_step,rest,index,step(state)) 91 92 def indexed_successor(+position: U32,+offset: Nat) -> 93 {(position + U32.from_nat(1n+offset) : U32) == ((position + 1 : U32) + U32.from_nat(offset) : U32) : U32}: 94 %WordArithmetic.native_add(1n,offset) : 95 {(position + _ : U32) == ((position + 1 : U32) + U32.from_nat(offset) : U32) : U32} 96 Equal.sym(U32,((position + 1 : U32) + U32.from_nat(offset) : U32),(position + (1 + U32.from_nat(offset) : U32) : U32), 97 Arithmetic.add_associative(position,1,U32.from_nat(offset))) 98 99 # The final step is applied once, to the state the loop ends in. 100 def run_then_finishes(~State: Type,~Result: Type,~step: State -> State,~finish: State -> Result,count: Nat,-state: State) -> 101 {Loop.run_then(~State,~Result,~step,~finish,count,state) == finish(Loop.run(~State,~step,count,state)) : Result}: 102 match count: 103 case 0n: {==} 104 case 1n+rest: run_then_finishes(~State,~Result,~step,~finish,rest,step(state)) 105 106 # Natural counters use the same symbolic induction as machine counters. 107 def natural_counter_progress(~State: Data,~step: State -> State,~position: State -> Nat, 108 ~advances: @+state: State -> {position(step(state)) == 1n+position(state) : Nat}, 109 +count: Nat,+state: State) -> 110 {position(iterate(~State,~step,count,state)) == Nat.add(count,position(state)) : Nat}: 111 match count: 112 case 0n: {==} 113 case 1n+ +rest: 114 %Addition.successor_right(rest,position(state)) : {position(iterate(~State,~step,rest,step(state))) == _ : Nat} 115 %advances(state) : {position(iterate(~State,~step,rest,step(state))) == Nat.add(rest,_) : Nat} 116 natural_counter_progress(~State,~step,~position,~advances,rest,step(state)) 117 118 # Structural properties of an owned model also follow the shared loop. 119 def preserves_invariant(~State: Data,~Context: Data,~Property: Context -> State -> Data,~step: State -> State, 120 ~preserved: @+context: Context -> @+state: State -> Property(context,state) -> Property(context,step(state)), 121 count: Nat,+context: Context,+state: State,evidence: Property(context,state)) -> Property(context,Loop.run(~State,~step,count,state)): 122 match count: 123 case 0n: evidence 124 case 1n+rest: 125 preserves_invariant(~State,~Context,~Property,~step,~preserved,rest,context,step(state),preserved(context,state,evidence))