proofs/loop_projection.bend
stelliferous@0.0.3.0 · 125 lines · 0 definitions
1# One induction for every state representation, output index and step count.
2import Base
3import stelliferous@0.0.3.0/proofs/natural_addition.bend as Addition
4import stelliferous@0.0.3.0/proofs/bounded_u32_arithmetic.bend as Arithmetic
5import stelliferous@0.0.3.0/proofs/word_arithmetic.bend as WordArithmetic
6import stelliferous@0.0.3.0/proofs/nat_order.bend as Order
7import stelliferous@0.0.3.0/proofs/nat_division_order.bend as DivisionOrder
8import stelliferous@0.0.3.0/traversal_loop.bend as Loop
9
10def iterate(~State: Data,~step: State -> State,count: Nat,state: State) -> State:
11 Loop.run(~State,~step,count,state)
12
13def 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.
20def 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.
34def 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.
50def 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.
65def 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
76def 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
92def 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.
100def 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.
107def 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.
119def 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))