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.
4	import Base
5	import ../kernel_parameter_gradient.bend as Kernel
6	import ../traversal_grouped.bend as Grouped
7	import ../storage_buffer.bend as Storage
8	import ./storage_certificate.bend as Certificate
9	import ./parameter_gradient_source_witness.bend as SourceWitness
10	import ./traversal_witness.bend as Witness
11	
12	def source(~Reader: Type,result: Reader & Storage.Buffer<F32>) -> Reader:
13	  (reader,values) = result
14	  reader
15	
16	def 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	
27	def 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	
38	def 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	
44	def 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