proofs/kernel_gather_certificate.bend
stelliferous@0.0.2.0 · 57 lines · 6 definitions
1import Base
2import stelliferous@0.0.2.0/kernel_gather.bend as Gather
3import stelliferous@0.0.2.0/traversal_array.bend as Traversal
4import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness
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/traversal_witness.bend as TraversalWitness
8
9def channel(+depth: Nat,+channel: U32,+width: U32,+offset: U32,+positions: U32,+span: U32,-input: Array<F32>,-owners: Array<F32> & Array<F32>,
10 input_evidence: Witness.ArrayWitness<F32,input>,evidence: TraversalWitness.ResultEvidence<Array<F32>,F32,input,depth,owners>) ->
11 TraversalWitness.ResultEvidence<Array<F32>,F32,input,depth,Gather.gather_channel(channel,width,offset,positions,span,owners)>:
12 TraversalWitness.ResultEvidence{output,equation,balanced} = evidence
13 %Equal.sym(Array<F32> & Array<F32>,owners,(input,output),equation) :
14 TraversalWitness.ResultEvidence<Array<F32>,F32,input,depth,Gather.gather_channel(channel,width,offset,positions,span,_)>
15 +context = {Traversal.Offsets{(channel * span : U32),(channel * positions + offset : U32)} : Traversal.Offsets}
16 -state = {Traversal.State{input,output,0,context} : Traversal.State<&1,&1,Array<F32>,Array<F32>,Traversal.Offsets>}
17 TraversalWitness.finish(~Array<F32>,~F32,~Traversal.Offsets,input,depth,
18 Traversal.run(~Array<F32>,~F32,~Traversal.Offsets,~Traversal.source_offset(~F32),~Traversal.destination_offset,U32.to_nat(width),state),
19 TraversalWitness.run(~Array<F32>,~F32,~Traversal.Offsets,~TraversalWitness.array_evidence(~F32),~Traversal.source_offset(~F32),~Traversal.destination_offset,~TraversalWitness.offset_read(~F32),
20 depth,U32.to_nat(width),input,state,input_evidence,TraversalWitness.StateEvidence{output,0,context,{==},balanced}))
21
22def channels(+depth: Nat,count: Nat,+index: U32,+width: U32,+offset: U32,+positions: U32,+span: U32,-input: Array<F32>,-owners: Array<F32> & Array<F32>,
23 +input_evidence: Witness.ArrayWitness<F32,input>,evidence: TraversalWitness.ResultEvidence<Array<F32>,F32,input,depth,owners>) ->
24 TraversalWitness.ResultEvidence<Array<F32>,F32,input,depth,Gather.gather_channels(count,index,width,offset,positions,span,owners)>:
25 match count:
26 case 0n: evidence
27 case 1n+rest:
28 channels(depth,rest,(index + 1 : U32),width,offset,positions,span,input,Gather.gather_channel(index,width,offset,positions,span,owners),input_evidence,
29 channel(depth,index,width,offset,positions,span,input,owners,input_evidence,evidence))
30
31def finish(-depth: Nat,-input: Array<F32>,-owners: Array<F32> & Array<F32>,evidence: TraversalWitness.ResultEvidence<Array<F32>,F32,input,depth,owners>) ->
32 Witness.Witness(F32,depth,Gather.gathered_output(owners)):
33 TraversalWitness.ResultEvidence{output,equation,balanced} = evidence
34 %Equal.sym(Array<F32> & Array<F32>,owners,(input,output),equation) : Witness.Witness(F32,depth,Gather.gathered_output(_))
35 balanced
36
37def block(+depth: Nat,+count: U32,+offset: U32,+positions: U32,+span: U32,-input: Array<F32>,-output: Array<F32>,
38 input_evidence: Witness.ArrayWitness<F32,input>,balanced: Witness.Witness(F32,depth,output)) ->
39 Witness.Witness(F32,depth,Gather.gather_block(count,offset,positions,span,input,output)):
40 +width = Gather.gather_width(offset,positions,span)
41 finish(depth,input,Gather.gather_channels(U32.to_nat(count),0,width,offset,positions,span,(input,output)),
42 channels(depth,U32.to_nat(count),0,width,offset,positions,span,input,(input,output),input_evidence,TraversalWitness.ResultEvidence{output,{==},balanced}))
43
44def equation(+depth: Nat,count: U32,offset: U32,positions: U32,span: U32,-input: Array<F32>,-output: Array<F32>,
45 input_certificate: Certificate.Certificate<F32,input>,balanced: {output == Tree.pack(F32,Certificate.normalized(F32,depth,Tree.reflect(F32,output))) : Array<F32>}) ->
46 {Gather.gather_block(count,offset,positions,span,input,output) ==
47 Tree.pack(F32,Certificate.normalized(F32,depth,Tree.reflect(F32,Gather.gather_block(count,offset,positions,span,input,output)))) : Array<F32>}:
48 %Certificate.restored(F32,depth,Gather.gather_block(count,offset,positions,span,input,output),
49 block(depth,count,offset,positions,span,input,output,Certificate.witness(F32,input,input_certificate),Certificate.witness_at(F32,depth,output,balanced))) :
50 {_ == Tree.pack(F32,Certificate.normalized(F32,depth,Tree.reflect(F32,Gather.gather_block(count,offset,positions,span,input,output)))) : Array<F32>}
51 {==}
52
53def certificate(count: U32,offset: U32,positions: U32,span: U32,-input: Array<F32>,-output: Array<F32>,
54 input_certificate: Certificate.Certificate<F32,input>,output_certificate: Certificate.Certificate<F32,output>) ->
55 Certificate.Certificate<F32,Gather.gather_block(count,offset,positions,span,input,output)>:
56 Certificate.Certificate{+depth,balanced} = output_certificate
57 Certificate.Certificate{depth,equation(depth,count,offset,positions,span,input,output,input_certificate,balanced)}