proofs/parameter_gradient_certificate.bend
stelliferous@0.0.3.0 · 47 lines · 0 definitions
1# The read-only traversal of the kernel preserves its native source.
2# Certificates are transported once at this boundary; every model traversal
3# is erased.
4import Base
5import stelliferous@0.0.3.0/kernel_parameter_gradient.bend as Kernel
6import stelliferous@0.0.3.0/traversal_grouped.bend as Grouped
7import stelliferous@0.0.3.0/storage_buffer.bend as Storage
8import stelliferous@0.0.3.0/proofs/storage_certificate.bend as Certificate
9import stelliferous@0.0.3.0/proofs/parameter_gradient_source_witness.bend as SourceWitness
10import stelliferous@0.0.3.0/proofs/traversal_witness.bend as Witness
11
12def source(~Reader: Type,result: Reader & Storage.Buffer<F32>) -> Reader:
13 (reader,values) = result
14 reader
15
16def stored_source(~Reader: Type,~read: Reader -> Kernel.Context -> Nat -> Reader & F32,rest: Nat,+index: Nat,+position: U32,+work: Kernel.Work,+ranges: List<&2,Grouped.Range>,
17 -reader: Reader,-result: Storage.Buffer<F32>,-pair: Reader & F32,sample: Witness.Sample<Reader,F32,reader,pair>,
18 tail: @-value: F32 -> {source(~Reader,Kernel.written(~Reader,~read,rest,1n+index,(position + 1 : U32),work,ranges,reader,Storage.write(~F32,position,value,result))) == reader : Reader}) ->
19 {source(~Reader,Kernel.stored(~Reader,position,result,pair,
20 reader => result => Kernel.written(~Reader,~read,rest,1n+index,(position + 1 : U32),work,ranges,reader,result))) == reader : Reader}:
21 Witness.Sample{value,equation} = sample
22 %Equal.sym(Reader & F32,pair,(reader,value),equation) :
23 {source(~Reader,Kernel.stored(~Reader,position,result,_,
24 reader => result => Kernel.written(~Reader,~read,rest,1n+index,(position + 1 : U32),work,ranges,reader,result))) == reader : Reader}
25 tail(value)
26
27def written_source(~Reader: Type,~Evidence: @-reader: Reader -> Data,~read: Reader -> Kernel.Context -> Nat -> Reader & F32,
28 ~preserves: @-reader: Reader -> @context: Kernel.Context -> @position: Nat -> Evidence(reader) -> Witness.Sample<Reader,F32,reader,read(reader,context,position)>,
29 remaining: Nat,+index: Nat,+position: U32,+work: Kernel.Work,+ranges: List<&2,Grouped.Range>,-reader: Reader,-result: Storage.Buffer<F32>,+evidence: Evidence(reader)) ->
30 {source(~Reader,Kernel.written(~Reader,~read,remaining,index,position,work,ranges,reader,result)) == reader : Reader}:
31 match remaining:
32 case 0n: {==}
33 case 1n+ +rest:
34 stored_source(~Reader,~read,rest,index,position,work,ranges,reader,result,Kernel.element(~Reader,~read,work,index,ranges,reader),
35 SourceWitness.element(~Reader,~Evidence,~read,~preserves,work,index,ranges,reader,evidence),
36 value => written_source(~Reader,~Evidence,~read,~preserves,rest,1n+index,(position + 1 : U32),work,ranges,reader,Storage.write(~F32,position,value,result),evidence))
37
38def bias_owner(+work: Kernel.Work,-d: Array<F32>,-result: Storage.Buffer<F32>,certificate: Certificate.Certificate<F32,d>) ->
39 {source(~Array<F32>,Kernel.bias(work,d,result)) == d : Array<F32>}:
40 Kernel.Work{n,c,o,h,w,k,s,p,rows,columns,g} = work
41 written_source(~Array<F32>,~SourceWitness.bias_evidence,~Kernel.bias_at,~SourceWitness.bias_cell,o,0n,0,work,Grouped.ranges(rows,columns,g),d,result,
42 Certificate.witness(F32,d,certificate))
43
44def bias(+work: Kernel.Work,-d: Array<F32>,-result: Storage.Buffer<F32>,+certificate: Certificate.Certificate<F32,d>) ->
45 Certificate.Certificate<F32,source(~Array<F32>,Kernel.bias(work,d,result))>:
46 %Equal.sym(Array<F32>,source(~Array<F32>,Kernel.bias(work,d,result)),d,bias_owner(work,d,result,certificate)) : Certificate.Certificate<F32,_>
47 certificate