proofs/traversal_certificate.bend
stelliferous@0.0.3.0 · 93 lines · 0 definitions
1# Flat certificates are updated once after a complete traversal. The witness
2# traversal is evaluated only by the checker, beneath erased equality rewrites.
3import Base
4import stelliferous@0.0.3.0/traversal_array.bend as Traversal
5import stelliferous@0.0.3.0/proofs/storage_tree_model.bend as Tree
6import stelliferous@0.0.3.0/proofs/storage_certificate.bend as Certificate
7import stelliferous@0.0.3.0/proofs/traversal_witness.bend as TraversalWitness
8
9type 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
14def 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
27def 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
37def 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# Metadata preparation belongs inside the erased preservation proof. Passing a
44# prepared cursor to a live certificate helper would retain or rebuild it.
45def operation_source(~Reader: Type,~Element: Data,~Metadata: Data,~ReaderCertificate: @-reader: Reader -> Data,
46 ~operation: Metadata -> Reader -> Array<Element> -> Reader & Array<Element>,
47 ~preserves: @+depth: Nat -> @metadata: Metadata -> @-reader: Reader -> @-output: Array<Element> -> ReaderCertificate(reader) ->
48 {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>} ->
49 TraversalWitness.ResultEvidence<Reader,Element,reader,depth,operation(metadata,reader,output)>,
50 metadata: Metadata,-reader: Reader,-output: Array<Element>,proof_certificate: ReaderCertificate(reader),reader_certificate: ReaderCertificate(reader),depth: Nat,
51 equation: {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>}) ->
52 ReaderCertificate(TraversalWitness.first(~Reader,~Array<Element>,operation(metadata,reader,output))):
53 %Equal.sym(Reader,TraversalWitness.first(~Reader,~Array<Element>,operation(metadata,reader,output)),reader,
54 TraversalWitness.source_unchanged(~Reader,~Element,reader,depth,operation(metadata,reader,output),
55 preserves(depth,metadata,reader,output,proof_certificate,equation))) : ReaderCertificate(_)
56 reader_certificate
57
58def operation_equation(~Reader: Type,~Element: Data,~Metadata: Data,~ReaderCertificate: @-reader: Reader -> Data,
59 ~operation: Metadata -> Reader -> Array<Element> -> Reader & Array<Element>,
60 ~preserves: @+depth: Nat -> @metadata: Metadata -> @-reader: Reader -> @-output: Array<Element> -> ReaderCertificate(reader) ->
61 {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>} ->
62 TraversalWitness.ResultEvidence<Reader,Element,reader,depth,operation(metadata,reader,output)>,
63 metadata: Metadata,-reader: Reader,-output: Array<Element>,reader_certificate: ReaderCertificate(reader),+depth: Nat,
64 equation: {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>}) ->
65 {TraversalWitness.second(~Reader,~Array<Element>,operation(metadata,reader,output)) ==
66 Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,TraversalWitness.second(~Reader,~Array<Element>,operation(metadata,reader,output))))) : Array<Element>}:
67 %Certificate.restored(Element,depth,TraversalWitness.second(~Reader,~Array<Element>,operation(metadata,reader,output)),
68 TraversalWitness.output_witness(~Reader,~Element,reader,depth,operation(metadata,reader,output),
69 preserves(depth,metadata,reader,output,reader_certificate,equation))) :
70 {_ == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,TraversalWitness.second(~Reader,~Array<Element>,operation(metadata,reader,output))))) : Array<Element>}
71 {==}
72
73def operation(~Reader: Type,~Element: Data,~Metadata: Data,~ReaderCertificate: @-reader: Reader -> Data,
74 ~operation: Metadata -> Reader -> Array<Element> -> Reader & Array<Element>,
75 ~preserves: @+depth: Nat -> @metadata: Metadata -> @-reader: Reader -> @-output: Array<Element> -> ReaderCertificate(reader) ->
76 {output == Tree.pack(Element,Certificate.normalized(Element,depth,Tree.reflect(Element,output))) : Array<Element>} ->
77 TraversalWitness.ResultEvidence<Reader,Element,reader,depth,operation(metadata,reader,output)>,
78 +metadata: Metadata,-reader: Reader,-output: Array<Element>,source_certificate: ReaderCertificate(reader),equation_certificate: ReaderCertificate(reader),
79 reader_certificate: ReaderCertificate(reader),output_certificate: Certificate.Certificate<Element,output>) ->
80 Certificates<Reader,Element,ReaderCertificate,operation(metadata,reader,output)>:
81 Certificate.Certificate{+depth,+equation} = output_certificate
82 Certificates{operation_source(~Reader,~Element,~Metadata,~ReaderCertificate,~operation,~preserves,metadata,reader,output,source_certificate,reader_certificate,depth,equation),
83 Certificate.Certificate{depth,operation_equation(~Reader,~Element,~Metadata,~ReaderCertificate,~operation,~preserves,metadata,reader,output,equation_certificate,depth,equation)}}
84
85def fold_operation(~Reader: Type,~Accumulator: Data,~Metadata: Data,~ReaderCertificate: @-reader: Reader -> Data,
86 ~operation: Metadata -> Reader -> Accumulator -> Reader & Accumulator,
87 ~preserves: @metadata: Metadata -> @-reader: Reader -> @-initial: Accumulator -> ReaderCertificate(reader) ->
88 {TraversalWitness.first(~Reader,~Accumulator,operation(metadata,reader,initial)) == reader : Reader},
89 metadata: Metadata,-reader: Reader,-initial: Accumulator,proof_certificate: ReaderCertificate(reader),certificate: ReaderCertificate(reader)) ->
90 ReaderCertificate(TraversalWitness.first(~Reader,~Accumulator,operation(metadata,reader,initial))):
91 %Equal.sym(Reader,TraversalWitness.first(~Reader,~Accumulator,operation(metadata,reader,initial)),reader,
92 preserves(metadata,reader,initial,proof_certificate)) : ReaderCertificate(_)
93 certificate