proofs/tensor_indexed_certificate.bend
stelliferous@0.0.2.0 · 117 lines · 12 definitions
1import Base
2import stelliferous@0.0.2.0/tensor_indexed.bend as Indexed
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_tree_model.bend as Tree
6import stelliferous@0.0.2.0/proofs/storage_certificate.bend as Certificate
7import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness
8import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness
9import stelliferous@0.0.2.0/proofs/traversal_certificate.bend as TraversalCertificate
10
11def sample(~Element: Data,~Context: Data,~index: Context -> U32 -> U32,~operation: U32 -> Element -> Element,
12 -input: Array<Element>,+context: Context,+position: U32,-result: Array<Element> & Element,
13 evidence: TraversalWitness.Sample<Array<Element>,Element,input,result>) ->
14 TraversalWitness.Sample<Array<Element>,Element,input,Indexed.value(~Element,~Context,~index,~operation,context,position,result)>:
15 match evidence:
16 case TraversalWitness.Sample{value,equation}:
17 %Equal.sym(Array<Element> & Element,result,(input,value),equation) :
18 TraversalWitness.Sample<Array<Element>,Element,input,Indexed.value(~Element,~Context,~index,~operation,context,position,_)>
19 TraversalWitness.Sample{operation(index(context,position),value),{==}}
20
21def read(~Element: Data,~Context: Data,~index: Context -> U32 -> U32,~operation: U32 -> Element -> Element,
22 -input: Array<Element>,context: Context,position: U32,evidence: Witness.ArrayWitness<Element,input>) ->
23 TraversalWitness.Sample<Array<Element>,Element,input,Indexed.read(~Element,~Context,~index,~operation,input,context,position)>:
24 +position = position
25 sample(~Element,~Context,~index,~operation,input,context,position,Array.get(Element,input,position),
26 TraversalWitness.array_sample(~Element,input,Array.get(Element,input,position),Witness.observed(Element,input,position,evidence)))
27
28def preserves(~Element: Data,~Context: Data,~index: Context -> U32 -> U32,~operation: U32 -> Element -> Element,
29 +depth: Nat,call: Indexed.Call<Context>,-input: Array<Element>,-output: Array<Element>,input_certificate: Certificate.Certificate<Element,input>,
30 equation: {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>}) ->
31 TraversalWitness.ResultEvidence<Array<Element>,Element,input,depth,Indexed.run(~Element,~Context,~index,~operation,call,input,output)>:
32 Indexed.Call{count,context} = call
33 TraversalCertificate.completed(~Array<Element>,~Element,~Context,~TraversalWitness.array_evidence(~Element),
34 ~Traversal.run(~Array<Element>,~Element,~Context,~Indexed.read(~Element,~Context,~index,~operation),~Indexed.destination(~Context)),
35 ~TraversalWitness.run(~Array<Element>,~Element,~Context,~TraversalWitness.array_evidence(~Element),~Indexed.read(~Element,~Context,~index,~operation),
36 ~Indexed.destination(~Context),~read(~Element,~Context,~index,~operation)),
37 count,0,context,input,output,Certificate.witness(Element,input,input_certificate),depth,equation)
38
39def certificates(~Element: Data,~Context: Data,~index: Context -> U32 -> U32,~operation: U32 -> Element -> Element,
40 +call: Indexed.Call<Context>,-input: Array<Element>,-output: Array<Element>,input_certificate: Certificate.Certificate<Element,input>,
41 output_certificate: Certificate.Certificate<Element,output>) ->
42 TraversalCertificate.Certificates<Array<Element>,Element,Certificate.family(~Element),Indexed.run(~Element,~Context,~index,~operation,call,input,output)>:
43 Certificate.Certificate{+depth,+equation} = input_certificate
44 TraversalCertificate.operation(~Array<Element>,~Element,~Indexed.Call<Context>,~Certificate.family(~Element),
45 ~Indexed.run(~Element,~Context,~index,~operation),~preserves(~Element,~Context,~index,~operation),
46 call,input,output,Certificate.Certificate{depth,equation},Certificate.Certificate{depth,equation},Certificate.Certificate{depth,equation},output_certificate)
47
48def next_block(~Element: Data,~Context: Data,+depth: Nat,block: U32,size: U32,context: Context,-input: Array<Element>,-state: Traversal.State<&1,&1,Array<Element>,Array<Element>,Indexed.Block>,
49 evidence: TraversalWitness.StateEvidence<Array<Element>,Element,Indexed.Block,input,depth,state>) ->
50 TraversalWitness.StateEvidence<Array<Element>,Element,Indexed.Blocks<Context>,input,depth,Indexed.next_block(~Element,~Context,block,size,context,state)>:
51 match evidence:
52 case TraversalWitness.StateEvidence{output,position,inner,equation,output_evidence}:
53 %Equal.sym(Traversal.State<&1,&1,Array<Element>,Array<Element>,Indexed.Block>,state,Traversal.State{input,output,position,inner},equation) :
54 TraversalWitness.StateEvidence<Array<Element>,Element,Indexed.Blocks<Context>,input,depth,Indexed.next_block(~Element,~Context,block,size,context,_)>
55 TraversalWitness.StateEvidence{output,position,Indexed.Blocks{(block + 1 : U32),size,context},{==},output_evidence}
56
57def block_step(~Element: Data,~Context: Data,~base: Context -> U32 -> U32,~operation: U32 -> Element -> Element,+depth: Nat,-input: Array<Element>,-state: Traversal.State<&1,&1,Array<Element>,Array<Element>,Indexed.Blocks<Context>>,
58 +input_evidence: Witness.ArrayWitness<Element,input>,evidence: TraversalWitness.StateEvidence<Array<Element>,Element,Indexed.Blocks<Context>,input,depth,state>) ->
59 TraversalWitness.StateEvidence<Array<Element>,Element,Indexed.Blocks<Context>,input,depth,Indexed.block_step(~Element,~Context,~base,~operation,state)>:
60 match evidence:
61 case TraversalWitness.StateEvidence{output,+position,Indexed.Blocks{+block,+size,+context},equation,output_evidence}:
62 %Equal.sym(Traversal.State<&1,&1,Array<Element>,Array<Element>,Indexed.Blocks<Context>>,state,Traversal.State{input,output,position,Indexed.Blocks{block,size,context}},equation) :
63 TraversalWitness.StateEvidence<Array<Element>,Element,Indexed.Blocks<Context>,input,depth,Indexed.block_step(~Element,~Context,~base,~operation,_)>
64 next_block(~Element,~Context,depth,block,size,context,input,
65 Traversal.run(~Array<Element>,~Element,~Indexed.Block,~Indexed.read(~Element,~Indexed.Block,~Indexed.block_index,~operation),~Indexed.destination(~Indexed.Block),U32.to_nat(size),
66 Traversal.State{input,output,position,Indexed.Block{base(context,block),position}}),
67 TraversalWitness.run(~Array<Element>,~Element,~Indexed.Block,~TraversalWitness.array_evidence(~Element),~Indexed.read(~Element,~Indexed.Block,~Indexed.block_index,~operation),
68 ~Indexed.destination(~Indexed.Block),~read(~Element,~Indexed.Block,~Indexed.block_index,~operation),depth,U32.to_nat(size),input,
69 Traversal.State{input,output,position,Indexed.Block{base(context,block),position}},input_evidence,
70 TraversalWitness.StateEvidence{output,position,Indexed.Block{base(context,block),position},{==},output_evidence}))
71
72def block_loop(~Element: Data,~Context: Data,~base: Context -> U32 -> U32,~operation: U32 -> Element -> Element,+depth: Nat,count: Nat,-input: Array<Element>,-state: Traversal.State<&1,&1,Array<Element>,Array<Element>,Indexed.Blocks<Context>>,
73 +input_evidence: Witness.ArrayWitness<Element,input>,evidence: TraversalWitness.StateEvidence<Array<Element>,Element,Indexed.Blocks<Context>,input,depth,state>) ->
74 TraversalWitness.StateEvidence<Array<Element>,Element,Indexed.Blocks<Context>,input,depth,
75 Loop.run(~Traversal.State<&1,&1,Array<Element>,Array<Element>,Indexed.Blocks<Context>>,~Indexed.block_step(~Element,~Context,~base,~operation),count,state)>:
76 match count:
77 case 0n: evidence
78 case 1n+rest:
79 block_loop(~Element,~Context,~base,~operation,depth,rest,input,Indexed.block_step(~Element,~Context,~base,~operation,state),input_evidence,
80 block_step(~Element,~Context,~base,~operation,depth,input,state,input_evidence,evidence))
81
82type Tiling<-Context: Data> is Data:
83 Tiling{total: U32,context: Context}
84
85def tiled_operation(~Element: Data,~Context: Data,~index: Context -> U32 -> U32,~base: Context -> U32 -> U32,~blocks: Context -> U32,~size: Context -> U32,~operation: U32 -> Element -> Element,
86 tiling: Tiling<Context>,input: Array<Element>,output: Array<Element>) -> Array<Element> & Array<Element>:
87 Tiling{total,context} = tiling
88 Indexed.run_tiled(~Element,~Context,~index,~base,~blocks,~size,~operation,total,context,input,output)
89
90def whole_preserves(~Element: Data,~Context: Data,~index: Context -> U32 -> U32,~base: Context -> U32 -> U32,~operation: U32 -> Element -> Element,
91 +depth: Nat,whole: Bool,blocks: U32,size: U32,total: U32,context: Context,-input: Array<Element>,-output: Array<Element>,input_certificate: Certificate.Certificate<Element,input>,
92 equation: {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>}) ->
93 TraversalWitness.ResultEvidence<Array<Element>,Element,input,depth,Indexed.run_whole(~Element,~Context,~index,~base,~operation,whole,blocks,size,total,context,input,output)>:
94 match whole:
95 case True{}:
96 TraversalCertificate.completed(~Array<Element>,~Element,~Indexed.Blocks<Context>,~TraversalWitness.array_evidence(~Element),
97 ~Loop.run(~Traversal.State<&1,&1,Array<Element>,Array<Element>,Indexed.Blocks<Context>>,~Indexed.block_step(~Element,~Context,~base,~operation)),~block_loop(~Element,~Context,~base,~operation),
98 U32.to_nat(blocks),0,Indexed.Blocks{0,size,context},input,output,Certificate.witness(Element,input,input_certificate),depth,equation)
99 case False{}:
100 preserves(~Element,~Context,~index,~operation,depth,Indexed.Call{U32.to_nat(total),context},input,output,input_certificate,equation)
101
102def tiled_preserves(~Element: Data,~Context: Data,~index: Context -> U32 -> U32,~base: Context -> U32 -> U32,~blocks: Context -> U32,~size: Context -> U32,~operation: U32 -> Element -> Element,
103 +depth: Nat,tiling: Tiling<Context>,-input: Array<Element>,-output: Array<Element>,input_certificate: Certificate.Certificate<Element,input>,
104 equation: {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>}) ->
105 TraversalWitness.ResultEvidence<Array<Element>,Element,input,depth,tiled_operation(~Element,~Context,~index,~base,~blocks,~size,~operation,tiling,input,output)>:
106 Tiling{+total,+context} = tiling
107 whole_preserves(~Element,~Context,~index,~base,~operation,depth,U32.is_le(total,Indexed.block_limit()) && Nat.is_eq(Nat.mul(U32.to_nat(blocks(context)),U32.to_nat(size(context))),U32.to_nat(total)),
108 blocks(context),size(context),total,context,input,output,input_certificate,equation)
109
110def tiled_certificates(~Element: Data,~Context: Data,~index: Context -> U32 -> U32,~base: Context -> U32 -> U32,~blocks: Context -> U32,~size: Context -> U32,~operation: U32 -> Element -> Element,
111 +total: U32,+context: Context,-input: Array<Element>,-output: Array<Element>,input_certificate: Certificate.Certificate<Element,input>,
112 output_certificate: Certificate.Certificate<Element,output>) ->
113 TraversalCertificate.Certificates<Array<Element>,Element,Certificate.family(~Element),Indexed.run_tiled(~Element,~Context,~index,~base,~blocks,~size,~operation,total,context,input,output)>:
114 Certificate.Certificate{+depth,+equation} = input_certificate
115 TraversalCertificate.operation(~Array<Element>,~Element,~Tiling<Context>,~Certificate.family(~Element),
116 ~tiled_operation(~Element,~Context,~index,~base,~blocks,~size,~operation),~tiled_preserves(~Element,~Context,~index,~base,~blocks,~size,~operation),
117 Tiling{total,context},input,output,Certificate.Certificate{depth,equation},Certificate.Certificate{depth,equation},Certificate.Certificate{depth,equation},output_certificate)