proofs/traversal_visit_witness.bend
stelliferous@0.0.2.0 · 131 lines · 12 definitions
1
2import Base
3import stelliferous@0.0.2.0/traversal_array.bend as Traversal
4import stelliferous@0.0.2.0/traversal_loop.bend as Loop
5import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness
6import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness
7
8type Sample<-Reader: Type,-Element: Data,-Context: Data,-reader: Reader,-result: Reader & Traversal.Visited<Context,Element>> is Data:
9 Sample{context: Context,-value: Element,equation: {result == (reader,Traversal.Visited{context,value}) : Reader & Traversal.Visited<Context,Element>}}
10
11def store(~Reader: Type,~Element: Data,~Context: Data,+depth: Nat,-reader: Reader,+position: U32,-output: Array<Element>,
12 -result: Reader & Traversal.Visited<Context,Element>,output_evidence: Witness.Witness(Element,depth,output),sample: Sample<Reader,Element,Context,reader,result>) ->
13 TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,Traversal.visit_store(~Reader,~Element,~Context,position,output,result)>:
14 match sample:
15 case Sample{context,value,equation}:
16 %Equal.sym(Reader & Traversal.Visited<Context,Element>,result,(reader,Traversal.Visited{context,value}),equation) :
17 TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,Traversal.visit_store(~Reader,~Element,~Context,position,output,_)>
18 TraversalWitness.StateEvidence{Array.set(Element,output,position,value),(position + 1 : U32),context,{==},Witness.write(Element,depth,output,position,value,output_evidence)}
19
20def step(~Reader: Type,~Element: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,
21 ~read: Reader -> Context -> Reader & Traversal.Visited<Context,Element>,
22 ~read_preserves: @-reader: Reader -> @context: Context -> ReaderEvidence(reader) -> Sample<Reader,Element,Context,reader,read(reader,context)>,
23 +depth: Nat,-reader: Reader,-state: Traversal.State<&1,&1,Reader,Array<Element>,Context>,reader_evidence: ReaderEvidence(reader),
24 evidence: TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,state>) ->
25 TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,Traversal.visit_step(~Reader,~Element,~Context,~read,state)>:
26 match evidence:
27 case TraversalWitness.StateEvidence{output,position,context,equation,output_evidence}:
28 %Equal.sym(Traversal.State<&1,&1,Reader,Array<Element>,Context>,state,Traversal.State{reader,output,position,context},equation) :
29 TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,Traversal.visit_step(~Reader,~Element,~Context,~read,_)>
30 store(~Reader,~Element,~Context,depth,reader,position,output,read(reader,context),output_evidence,read_preserves(reader,context,reader_evidence))
31
32def spread_store(~Element: Data,~Context: Data,+depth: Nat,-input: Array<Element>,+position: U32,-output: Array<Element>,target: Traversal.Target<Context>,
33 -result: Array<Element> & Element,output_evidence: Witness.Witness(Element,depth,output),observed: Witness.Read<Element,input,result>) ->
34 TraversalWitness.StateEvidence<Array<Element>,Element,Context,input,depth,Traversal.spread_store(~Element,~Context,position,output,target,result)>:
35 match target observed:
36 case Traversal.Target{context,+address} Witness.Read{value,equation}:
37 %Equal.sym(Array<Element> & Element,result,(input,value),equation) :
38 TraversalWitness.StateEvidence<Array<Element>,Element,Context,input,depth,Traversal.spread_store(~Element,~Context,position,output,Traversal.Target{context,address},_)>
39 TraversalWitness.StateEvidence{Array.set(Element,output,address,value),(position + 1 : U32),context,{==},Witness.write(Element,depth,output,address,value,output_evidence)}
40
41def spread_step(~Element: Data,~Context: Data,~target: Context -> Traversal.Target<Context>,
42 +depth: Nat,-input: Array<Element>,-state: Traversal.State<&1,&1,Array<Element>,Array<Element>,Context>,input_evidence: Witness.ArrayWitness<Element,input>,
43 evidence: TraversalWitness.StateEvidence<Array<Element>,Element,Context,input,depth,state>) ->
44 TraversalWitness.StateEvidence<Array<Element>,Element,Context,input,depth,Traversal.spread_step(~Element,~Context,~target,state)>:
45 match evidence:
46 case TraversalWitness.StateEvidence{output,+position,context,equation,output_evidence}:
47 %Equal.sym(Traversal.State<&1,&1,Array<Element>,Array<Element>,Context>,state,Traversal.State{input,output,position,context},equation) :
48 TraversalWitness.StateEvidence<Array<Element>,Element,Context,input,depth,Traversal.spread_step(~Element,~Context,~target,_)>
49 spread_store(~Element,~Context,depth,input,position,output,target(context),Array.get(Element,input,position),output_evidence,
50 Witness.observed(Element,input,position,input_evidence))
51
52def update_sample(~Reader: Type,~Element: Data,~Context: Data,~combine: Element -> Element -> Element,
53 +depth: Nat,-reader: Reader,+position: U32,-output: Array<Element>,-current: Element,-result: Reader & Traversal.Visited<Context,Element>,
54 output_evidence: Witness.Witness(Element,depth,output),sample: Sample<Reader,Element,Context,reader,result>) ->
55 TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,Traversal.visit_update_sample(~Reader,~Element,~Context,~combine,position,output,current,result)>:
56 match sample:
57 case Sample{context,value,equation}:
58 %Equal.sym(Reader & Traversal.Visited<Context,Element>,result,(reader,Traversal.Visited{context,value}),equation) :
59 TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,Traversal.visit_update_sample(~Reader,~Element,~Context,~combine,position,output,current,_)>
60 TraversalWitness.StateEvidence{Array.set(Element,output,position,combine(current,value)),(position + 1 : U32),context,{==},
61 Witness.write(Element,depth,output,position,combine(current,value),output_evidence)}
62
63def update_current(~Reader: Type,~Element: Data,~Context: Data,~read: Reader -> Context -> Reader & Traversal.Visited<Context,Element>,
64 ~combine: Element -> Element -> Element,+depth: Nat,-reader: Reader,position: U32,context: Context,-output: Array<Element>,-result: Array<Element> & Element,
65 output_evidence: Witness.Witness(Element,depth,output),observed: Witness.Read<Element,output,result>,sample: Sample<Reader,Element,Context,reader,read(reader,context)>) ->
66 TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,Traversal.visit_update_current(~Reader,~Element,~Context,~read,~combine,position,context,reader,result)>:
67 match observed:
68 case Witness.Read{value,equation}:
69 %Equal.sym(Array<Element> & Element,result,(output,value),equation) :
70 TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,Traversal.visit_update_current(~Reader,~Element,~Context,~read,~combine,position,context,reader,_)>
71 update_sample(~Reader,~Element,~Context,~combine,depth,reader,position,output,value,read(reader,context),output_evidence,sample)
72
73def update_step(~Reader: Type,~Element: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,
74 ~read: Reader -> Context -> Reader & Traversal.Visited<Context,Element>,~combine: Element -> Element -> Element,
75 ~read_preserves: @-reader: Reader -> @context: Context -> ReaderEvidence(reader) -> Sample<Reader,Element,Context,reader,read(reader,context)>,
76 +depth: Nat,-reader: Reader,-state: Traversal.State<&1,&1,Reader,Array<Element>,Context>,reader_evidence: ReaderEvidence(reader),
77 evidence: TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,state>) ->
78 TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,Traversal.visit_update_step(~Reader,~Element,~Context,~read,~combine,state)>:
79 match evidence:
80 case TraversalWitness.StateEvidence{output,+position,+context,equation,+output_evidence}:
81 %Equal.sym(Traversal.State<&1,&1,Reader,Array<Element>,Context>,state,Traversal.State{reader,output,position,context},equation) :
82 TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,Traversal.visit_update_step(~Reader,~Element,~Context,~read,~combine,_)>
83 update_current(~Reader,~Element,~Context,~read,~combine,depth,reader,position,context,output,Array.get(Element,output,position),output_evidence,
84 Witness.read(Element,depth,output,position,output_evidence),read_preserves(reader,context,reader_evidence))
85
86def update(~Reader: Type,~Element: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,
87 ~read: Reader -> Context -> Reader & Traversal.Visited<Context,Element>,~combine: Element -> Element -> Element,
88 ~read_preserves: @-reader: Reader -> @context: Context -> ReaderEvidence(reader) -> Sample<Reader,Element,Context,reader,read(reader,context)>,
89 +depth: Nat,count: Nat,-reader: Reader,-state: Traversal.State<&1,&1,Reader,Array<Element>,Context>,+reader_evidence: ReaderEvidence(reader),
90 evidence: TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,state>) ->
91 TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,Traversal.visit_update(~Reader,~Element,~Context,~read,~combine,count,state)>:
92 match count:
93 case 0n: evidence
94 case 1n+rest:
95 update(~Reader,~Element,~Context,~ReaderEvidence,~read,~combine,~read_preserves,depth,rest,reader,
96 Traversal.visit_update_step(~Reader,~Element,~Context,~read,~combine,state),reader_evidence,
97 update_step(~Reader,~Element,~Context,~ReaderEvidence,~read,~combine,~read_preserves,depth,reader,state,reader_evidence,evidence))
98
99def fold_value(~Reader: Type,~Element: Data,~Accumulator: Data,~Context: Data,~combine: Accumulator -> Element -> Accumulator,
100 -reader: Reader,+position: U32,-accumulator: Accumulator,-result: Reader & Traversal.Visited<Context,Element>,sample: Sample<Reader,Element,Context,reader,result>) ->
101 TraversalWitness.FoldEvidence<Reader,Accumulator,Context,reader,Traversal.visit_fold_value(~Reader,~Element,~Accumulator,~Context,~combine,position,accumulator,result)>:
102 match sample:
103 case Sample{context,value,equation}:
104 %Equal.sym(Reader & Traversal.Visited<Context,Element>,result,(reader,Traversal.Visited{context,value}),equation) :
105 TraversalWitness.FoldEvidence<Reader,Accumulator,Context,reader,Traversal.visit_fold_value(~Reader,~Element,~Accumulator,~Context,~combine,position,accumulator,_)>
106 TraversalWitness.FoldEvidence{combine(accumulator,value),(position + 1 : U32),context,{==}}
107
108def fold_step(~Reader: Type,~Element: Data,~Accumulator: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,
109 ~read: Reader -> Context -> Reader & Traversal.Visited<Context,Element>,~combine: Accumulator -> Element -> Accumulator,
110 ~read_preserves: @-reader: Reader -> @context: Context -> ReaderEvidence(reader) -> Sample<Reader,Element,Context,reader,read(reader,context)>,
111 -reader: Reader,-state: Traversal.State<&1,&2,Reader,Accumulator,Context>,reader_evidence: ReaderEvidence(reader),
112 evidence: TraversalWitness.FoldEvidence<Reader,Accumulator,Context,reader,state>) ->
113 TraversalWitness.FoldEvidence<Reader,Accumulator,Context,reader,Traversal.visit_fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine,state)>:
114 match evidence:
115 case TraversalWitness.FoldEvidence{accumulator,position,context,equation}:
116 %Equal.sym(Traversal.State<&1,&2,Reader,Accumulator,Context>,state,Traversal.State{reader,accumulator,position,context},equation) :
117 TraversalWitness.FoldEvidence<Reader,Accumulator,Context,reader,Traversal.visit_fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine,_)>
118 fold_value(~Reader,~Element,~Accumulator,~Context,~combine,reader,position,accumulator,read(reader,context),read_preserves(reader,context,reader_evidence))
119
120def fold_run(~Reader: Type,~Element: Data,~Accumulator: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,
121 ~read: Reader -> Context -> Reader & Traversal.Visited<Context,Element>,~combine: Accumulator -> Element -> Accumulator,
122 ~read_preserves: @-reader: Reader -> @context: Context -> ReaderEvidence(reader) -> Sample<Reader,Element,Context,reader,read(reader,context)>,
123 count: Nat,-reader: Reader,-state: Traversal.State<&1,&2,Reader,Accumulator,Context>,+reader_evidence: ReaderEvidence(reader),
124 evidence: TraversalWitness.FoldEvidence<Reader,Accumulator,Context,reader,state>) ->
125 TraversalWitness.FoldEvidence<Reader,Accumulator,Context,reader,Traversal.visit_fold(~Reader,~Element,~Accumulator,~Context,~read,~combine,count,state)>:
126 match count:
127 case 0n: evidence
128 case 1n+rest:
129 fold_run(~Reader,~Element,~Accumulator,~Context,~ReaderEvidence,~read,~combine,~read_preserves,rest,reader,
130 Traversal.visit_fold_step(~Reader,~Element,~Accumulator,~Context,~read,~combine,state),reader_evidence,
131 fold_step(~Reader,~Element,~Accumulator,~Context,~ReaderEvidence,~read,~combine,~read_preserves,reader,state,reader_evidence,evidence))