proofs/traversal_certificate.bend

stelliferous@0.0.2.0 · 105 lines · 9 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.2.0/traversal_array.bend as Traversal
5import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
6import stelliferous@0.0.2.0/proofs/storage_certificate.bend as Certificate
7import stelliferous@0.0.2.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
43def 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.
57def 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
70def 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
85def 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
97def 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