proofs/loop_projection.bend

stelliferous@0.0.2.0 · 117 lines · 12 definitions

1# One induction for every state representation, output index and step count.
2import Base
3import stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend as Arithmetic
4import stelliferous@0.0.2.0/proofs/word_arithmetic.bend as WordArithmetic
5import stelliferous@0.0.2.0/traversal_loop.bend as Loop
6
7def 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.
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))
25
26# A read-only observation is preserved for every number of iterations.
27def 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
38def 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
54type Measured<-State: Data> is Data:
55  Measured{result: State,work: Nat}
56
57def add_work(-State: Data,work: Nat,tail: Measured<State>) -> Measured<State>:
58  Measured{result,remaining} = tail
59  Measured{result,Nat.add(work,remaining)}
60
61def measured_iteration(~State: Data,~step: State -> State,~cost: State -> Nat,count: Nat,+state: State) -> Measured<State>:
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.
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      {==}
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
86def 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)))
92def 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
101def 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.
113def 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))