proofs/parameter_gradient_source_witness.bend

stelliferous@0.0.3.0 · 41 lines · 0 definitions

1# The bias reader instantiates the shared grouped source witness: each
2# reduced output leaves the reader as it was.
3import Base
4import stelliferous@0.0.3.0/kernel_parameter_gradient.bend as Kernel
5import stelliferous@0.0.3.0/traversal_grouped.bend as Grouped
6import stelliferous@0.0.3.0/proofs/storage_witness.bend as ArrayWitness
7import stelliferous@0.0.3.0/proofs/traversal_witness.bend as Witness
8import stelliferous@0.0.3.0/proofs/grouped_source_witness.bend as GroupWitness
9
10def bias_evidence(-reader: Array<F32>) -> Data:
11  ArrayWitness.ArrayWitness<F32,reader>
12
13def bias_cell(-reader: Array<F32>,context: Kernel.Context,position: Nat,source: bias_evidence(reader)) ->
14  Witness.Sample<Array<F32>,F32,reader,Kernel.bias_at(reader,context,position)>:
15  Witness.array_sample(~F32,reader,Kernel.bias_at(reader,context,position),ArrayWitness.observed(F32,reader,Kernel.bias_address(context,position),source))
16
17def image_tail(~Reader: Type,~read: Reader -> Kernel.Context -> Nat -> Reader & F32,-reader: Reader,-result: Reader & F32,
18  +rest: Nat,+image: Nat,+element: Nat,+work: Kernel.Work,+ranges: List<&2,Grouped.Range>,
19  head: Witness.Sample<Reader,F32,reader,result>,tail: Witness.Sample<Reader,List<&2,F32>,reader,Kernel.image_values(~Reader,~read,rest,image,element,work,ranges,reader)>) ->
20  Witness.Sample<Reader,List<&2,F32>,reader,Kernel.image_tail(~Reader,result,reader => Kernel.image_values(~Reader,~read,rest,image,element,work,ranges,reader))>:
21  Witness.Sample{value,equation} = head
22  %Equal.sym(Reader & F32,result,(reader,value),equation) : Witness.Sample<Reader,List<&2,F32>,reader,Kernel.image_tail(~Reader,_,reader => Kernel.image_values(~Reader,~read,rest,image,element,work,ranges,reader))>
23  GroupWitness.prepended(~Reader,reader,value,Kernel.image_values(~Reader,~read,rest,image,element,work,ranges,reader),tail)
24
25def images(~Reader: Type,~Evidence: @-reader: Reader -> Data,~read: Reader -> Kernel.Context -> Nat -> Reader & F32,
26  ~preserves: @-reader: Reader -> @context: Kernel.Context -> @position: Nat -> Evidence(reader) -> Witness.Sample<Reader,F32,reader,read(reader,context,position)>,
27  remaining: Nat,+image: Nat,+element: Nat,+work: Kernel.Work,+ranges: List<&2,Grouped.Range>,-reader: Reader,+source: Evidence(reader)) ->
28  Witness.Sample<Reader,List<&2,F32>,reader,Kernel.image_values(~Reader,~read,remaining,image,element,work,ranges,reader)>:
29  match remaining:
30    case 0n: Witness.Sample{[],{==}}
31    case 1n+ +rest:
32      image_tail(~Reader,~read,reader,Grouped.run(~Reader,~Kernel.Context,~read,ranges,reader,Kernel.Context{work,image,element}),rest,1n+image,element,work,ranges,
33        GroupWitness.run(~Reader,~Kernel.Context,~Evidence,~read,~preserves,ranges,reader,Kernel.Context{work,image,element},source),
34        images(~Reader,~Evidence,~read,~preserves,rest,1n+image,element,work,ranges,reader,source))
35
36def element(~Reader: Type,~Evidence: @-reader: Reader -> Data,~read: Reader -> Kernel.Context -> Nat -> Reader & F32,
37  ~preserves: @-reader: Reader -> @context: Kernel.Context -> @position: Nat -> Evidence(reader) -> Witness.Sample<Reader,F32,reader,read(reader,context,position)>,
38  +work: Kernel.Work,+index: Nat,+ranges: List<&2,Grouped.Range>,-reader: Reader,source: Evidence(reader)) ->
39  Witness.Sample<Reader,F32,reader,Kernel.element(~Reader,~read,work,index,ranges,reader)>:
40  Kernel.Work{+count,c,o,h,w,k,s,p,rows,columns,g} = work
41  GroupWitness.reduced(~Reader,reader,Kernel.image_values(~Reader,~read,count,0n,index,work,ranges,reader),images(~Reader,~Evidence,~read,~preserves,count,0n,index,work,ranges,reader,source))