1	# Flat certificates are updated once after a complete traversal. The witness
2	# traversal is evaluated only by the checker, beneath erased equality rewrites.
3	import Base
4	import ../traversal_array.bend as Traversal
5	import ./storage_tree_model.bend as Tree
6	import ./storage_certificate.bend as Certificate
7	import ./traversal_witness.bend as TraversalWitness
8	
9	type Certificates<-Reader: Type,-Element: Data,-ReaderCertificate: @-reader: Reader -> Data,
10	  -result: Reader & Array<Element>> is Data:
11	  Certificates{source: ReaderCertificate(TraversalWitness.first(~Reader,~Array<Element>,result)),
12	    output: Certificate.Certificate<Element,TraversalWitness.second(~Reader,~Array<Element>,result)>}
13	
14	def completed(~Reader: Type,~Element: Data,~Context: Data,~ReaderEvidence: @-reader: Reader -> Data,
15	  ~run: Nat -> Traversal.State<&1,&1,Reader,Array<Element>,Context> -> Traversal.State<&1,&1,Reader,Array<Element>,Context>,
16	  ~preserves: @+depth: Nat -> @count: Nat -> @-reader: Reader -> @-state: Traversal.State<&1,&1,Reader,Array<Element>,Context> ->
17	    @+reader_evidence: ReaderEvidence(reader) -> TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,state> ->
18	    TraversalWitness.StateEvidence<Reader,Element,Context,reader,depth,run(count,state)>,
19	  count: Nat,position: U32,context: Context,-reader: Reader,-output: Array<Element>,reader_evidence: ReaderEvidence(reader),+depth: Nat,
20	  equation: {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>}) ->
21	  TraversalWitness.ResultEvidence<Reader,Element,reader,depth,
22	    Traversal.finish(~Reader,~Element,~Context,run(count,Traversal.State{reader,output,position,context}))>:
23	  TraversalWitness.finish(~Reader,~Element,~Context,reader,depth,run(count,Traversal.State{reader,output,position,context}),
24	    preserves(depth,count,reader,Traversal.State{reader,output,position,context},reader_evidence,
25	      TraversalWitness.StateEvidence{output,position,context,{==},Certificate.witness_at(Element,depth,output,equation)}))
26	
27	def map_equation(~Element: Data,~Context: Data,~map: Context -> Element -> Element,count: Nat,position: U32,context: Context,
28	  -output: Array<Element>,+depth: Nat,
29	  equation: {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>}) ->
30	  {Traversal.map_in_place(~Element,~Context,~map,count,position,context,output) ==
31	    Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,Traversal.map_in_place(~Element,~Context,~map,count,position,context,output)))) : Array<Element>}:
32	  %Certificate.restored(Element,depth,Traversal.map_in_place(~Element,~Context,~map,count,position,context,output),
33	    TraversalWitness.map_in_place(~Element,~Context,~map,depth,count,position,context,output,Certificate.witness_at(Element,depth,output,equation))) :
34	    {_ == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,Traversal.map_in_place(~Element,~Context,~map,count,position,context,output)))) : Array<Element>}
35	  {==}
36	
37	def map_in_place(~Element: Data,~Context: Data,~map: Context -> Element -> Element,count: Nat,position: U32,context: Context,
38	  -output: Array<Element>,certificate: Certificate.Certificate<Element,output>) ->
39	  Certificate.Certificate<Element,Traversal.map_in_place(~Element,~Context,~map,count,position,context,output)>:
40	  Certificate.Certificate{+depth,equation} = certificate
41	  Certificate.Certificate{depth,map_equation(~Element,~Context,~map,count,position,context,output,depth,equation)}
42	
43	def fold(~Reader: Type,~Element: Data,~Accumulator: Data,~Context: Data,~ReaderCertificate: @-reader: Reader -> Data,
44	  ~ReaderEvidence: @-reader: Reader -> Data,~witness: @-reader: Reader -> ReaderCertificate(reader) -> ReaderEvidence(reader),
45	  ~read: Reader -> Context -> U32 -> Reader & Element,~combine: Accumulator -> Element -> Accumulator,
46	  ~read_preserves: @-reader: Reader -> @context: Context -> @index: U32 -> ReaderEvidence(reader) ->
47	    TraversalWitness.Sample<Reader,Element,reader,read(reader,context,index)>,
48	  count: Nat,position: U32,context: Context,-reader: Reader,-initial: Accumulator,+certificate: ReaderCertificate(reader)) ->
49	  ReaderCertificate(TraversalWitness.first(~Reader,~Accumulator,Traversal.fold(~Reader,~Element,~Accumulator,~Context,~read,~combine,count,position,reader,initial,context))):
50	  %Equal.sym(Reader,TraversalWitness.first(~Reader,~Accumulator,Traversal.fold(~Reader,~Element,~Accumulator,~Context,~read,~combine,count,position,reader,initial,context)),reader,
51	    TraversalWitness.fold(~Reader,~Element,~Accumulator,~Context,~ReaderEvidence,~read,~combine,~read_preserves,
52	      count,reader,position,context,initial,witness(reader,certificate))) : ReaderCertificate(_)
53	  certificate
54	
55	# Metadata preparation belongs inside the erased preservation proof. Passing a
56	# prepared cursor to a live certificate helper would retain or rebuild it.
57	def operation_source(~Reader: Type,~Element: Data,~Metadata: Data,~ReaderCertificate: @-reader: Reader -> Data,
58	  ~operation: Metadata -> Reader -> Array<Element> -> Reader & Array<Element>,
59	  ~preserves: @+depth: Nat -> @metadata: Metadata -> @-reader: Reader -> @-output: Array<Element> -> ReaderCertificate(reader) ->
60	    {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>} ->
61	    TraversalWitness.ResultEvidence<Reader,Element,reader,depth,operation(metadata,reader,output)>,
62	  metadata: Metadata,-reader: Reader,-output: Array<Element>,proof_certificate: ReaderCertificate(reader),reader_certificate: ReaderCertificate(reader),depth: Nat,
63	  equation: {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>}) ->
64	  ReaderCertificate(TraversalWitness.first(~Reader,~Array<Element>,operation(metadata,reader,output))):
65	  %Equal.sym(Reader,TraversalWitness.first(~Reader,~Array<Element>,operation(metadata,reader,output)),reader,
66	    TraversalWitness.source_unchanged(~Reader,~Element,reader,depth,operation(metadata,reader,output),
67	      preserves(depth,metadata,reader,output,proof_certificate,equation))) : ReaderCertificate(_)
68	  reader_certificate
69	
70	def operation_equation(~Reader: Type,~Element: Data,~Metadata: Data,~ReaderCertificate: @-reader: Reader -> Data,
71	  ~operation: Metadata -> Reader -> Array<Element> -> Reader & Array<Element>,
72	  ~preserves: @+depth: Nat -> @metadata: Metadata -> @-reader: Reader -> @-output: Array<Element> -> ReaderCertificate(reader) ->
73	    {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>} ->
74	    TraversalWitness.ResultEvidence<Reader,Element,reader,depth,operation(metadata,reader,output)>,
75	  metadata: Metadata,-reader: Reader,-output: Array<Element>,reader_certificate: ReaderCertificate(reader),+depth: Nat,
76	  equation: {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>}) ->
77	  {TraversalWitness.second(~Reader,~Array<Element>,operation(metadata,reader,output)) ==
78	    Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,TraversalWitness.second(~Reader,~Array<Element>,operation(metadata,reader,output))))) : Array<Element>}:
79	  %Certificate.restored(Element,depth,TraversalWitness.second(~Reader,~Array<Element>,operation(metadata,reader,output)),
80	    TraversalWitness.output_witness(~Reader,~Element,reader,depth,operation(metadata,reader,output),
81	      preserves(depth,metadata,reader,output,reader_certificate,equation))) :
82	    {_ == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,TraversalWitness.second(~Reader,~Array<Element>,operation(metadata,reader,output))))) : Array<Element>}
83	  {==}
84	
85	def operation(~Reader: Type,~Element: Data,~Metadata: Data,~ReaderCertificate: @-reader: Reader -> Data,
86	  ~operation: Metadata -> Reader -> Array<Element> -> Reader & Array<Element>,
87	  ~preserves: @+depth: Nat -> @metadata: Metadata -> @-reader: Reader -> @-output: Array<Element> -> ReaderCertificate(reader) ->
88	    {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>} ->
89	    TraversalWitness.ResultEvidence<Reader,Element,reader,depth,operation(metadata,reader,output)>,
90	  +metadata: Metadata,-reader: Reader,-output: Array<Element>,source_certificate: ReaderCertificate(reader),equation_certificate: ReaderCertificate(reader),
91	  reader_certificate: ReaderCertificate(reader),output_certificate: Certificate.Certificate<Element,output>) ->
92	  Certificates<Reader,Element,ReaderCertificate,operation(metadata,reader,output)>:
93	  Certificate.Certificate{+depth,+equation} = output_certificate
94	  Certificates{operation_source(~Reader,~Element,~Metadata,~ReaderCertificate,~operation,~preserves,metadata,reader,output,source_certificate,reader_certificate,depth,equation),
95	    Certificate.Certificate{depth,operation_equation(~Reader,~Element,~Metadata,~ReaderCertificate,~operation,~preserves,metadata,reader,output,equation_certificate,depth,equation)}}
96	
97	def fold_operation(~Reader: Type,~Accumulator: Data,~Metadata: Data,~ReaderCertificate: @-reader: Reader -> Data,
98	  ~operation: Metadata -> Reader -> Accumulator -> Reader & Accumulator,
99	  ~preserves: @metadata: Metadata -> @-reader: Reader -> @-initial: Accumulator -> ReaderCertificate(reader) ->
100	    {TraversalWitness.first(~Reader,~Accumulator,operation(metadata,reader,initial)) == reader : Reader},
101	  metadata: Metadata,-reader: Reader,-initial: Accumulator,proof_certificate: ReaderCertificate(reader),certificate: ReaderCertificate(reader)) ->
102	  ReaderCertificate(TraversalWitness.first(~Reader,~Accumulator,operation(metadata,reader,initial))):
103	  %Equal.sym(Reader,TraversalWitness.first(~Reader,~Accumulator,operation(metadata,reader,initial)),reader,
104	    preserves(metadata,reader,initial,proof_certificate)) : ReaderCertificate(_)
105	  certificate