proofs/traversal_certificate.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/traversal_certificate.bend as Traversal_certificate

Flat certificates are updated once after a complete traversal. The witness traversal is evaluated only by the checker, beneath erased equality rewrites.

5 imports

import Base
import ../traversal_array.bend as Traversal
import ./storage_tree_model.bend as Tree
import ./storage_certificate.bend as Certificate
import ./traversal_witness.bend as TraversalWitness

Types

type Certificates source · line 9 · raw

@-Reader:Type -> @-Element:Data -> @-ReaderCertificate:(@-reader:Reader -> Data) -> @-result:Pair(Reader, Array<Element>) -> Data

Certificates

@-Reader:Type -> @-Element:Data -> @-ReaderCertificate:(@-reader:Reader -> Data) -> @-result:Pair(Reader, Array<Element>) -> @source:ReaderCertificate(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.first(Reader, Array<Element>, result)) -> @output:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.second(Reader, Array<Element>, result)> -> Certificates<Reader, Element, ReaderCertificate, result>

Templates

template completed source · line 14 · raw

@-Reader:Type -> @-Element:Data -> @-Context:Data -> @-ReaderEvidence:(@-reader:Reader -> Data) -> @-run:(@_:Nat -> @_:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Reader, Array<Element>, Context> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Reader, Array<Element>, Context>) -> @-preserves:(@+depth:Nat -> @count:Nat -> @-reader:Reader -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Reader, Array<Element>, Context> -> @+reader_evidence:ReaderEvidence(reader) -> @_:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.StateEvidence<Reader, Element, Context, reader, depth, state> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.StateEvidence<Reader, Element, Context, reader, depth, run(count, state)>) -> @count:Nat -> @position:U32 -> @context:Context -> @-reader:Reader -> @-output:Array<Element> -> @reader_evidence:ReaderEvidence(reader) -> @+depth:Nat -> @equation:{output == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.normalized(Element, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(Element, output))) : Array<Element>} -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.ResultEvidence<Reader, Element, reader, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.finish(Reader, Element, Context, run(count, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State{reader, output, position, context}))>

template map_equation source · line 27 · raw

@-Element:Data -> @-Context:Data -> @-map:(@_:Context -> @_:Element -> Element) -> @count:Nat -> @position:U32 -> @context:Context -> @-output:Array<Element> -> @+depth:Nat -> @equation:{output == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.normalized(Element, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(Element, output))) : Array<Element>} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.map_in_place(Element, Context, map, count, position, context, output) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.normalized(Element, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.map_in_place(Element, Context, map, count, position, context, output)))) : Array<Element>}

template map_in_place source · line 37 · raw

@-Element:Data -> @-Context:Data -> @-map:(@_:Context -> @_:Element -> Element) -> @count:Nat -> @position:U32 -> @context:Context -> @-output:Array<Element> -> @certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<Element, output> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.map_in_place(Element, Context, map, count, position, context, output)>

template fold source · line 43 · raw

@-Reader:Type -> @-Element:Data -> @-Accumulator:Data -> @-Context:Data -> @-ReaderCertificate:(@-reader:Reader -> Data) -> @-ReaderEvidence:(@-reader:Reader -> Data) -> @-witness:(@-reader:Reader -> @_:ReaderCertificate(reader) -> ReaderEvidence(reader)) -> @-read:(@_:Reader -> @_:Context -> @_:U32 -> Pair(Reader, Element)) -> @-combine:(@_:Accumulator -> @_:Element -> Accumulator) -> @-read_preserves:(@-reader:Reader -> @context:Context -> @index:U32 -> @_:ReaderEvidence(reader) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<Reader, Element, reader, read(reader, context, index)>) -> @count:Nat -> @position:U32 -> @context:Context -> @-reader:Reader -> @-initial:Accumulator -> @+certificate:ReaderCertificate(reader) -> ReaderCertificate(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.first(Reader, Accumulator, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.fold(Reader, Element, Accumulator, Context, read, combine, count, position, reader, initial, context)))

template operation_source source · line 57 · raw

@-Reader:Type -> @-Element:Data -> @-Metadata:Data -> @-ReaderCertificate:(@-reader:Reader -> Data) -> @-operation:(@_:Metadata -> @_:Reader -> @_:Array<Element> -> Pair(Reader, Array<Element>)) -> @-preserves:(@+depth:Nat -> @metadata:Metadata -> @-reader:Reader -> @-output:Array<Element> -> @_:ReaderCertificate(reader) -> @_:{output == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.normalized(Element, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(Element, output))) : Array<Element>} -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.ResultEvidence<Reader, Element, reader, depth, operation(metadata, reader, output)>) -> @metadata:Metadata -> @-reader:Reader -> @-output:Array<Element> -> @proof_certificate:ReaderCertificate(reader) -> @reader_certificate:ReaderCertificate(reader) -> @depth:Nat -> @equation:{output == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.normalized(Element, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(Element, output))) : Array<Element>} -> ReaderCertificate(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.first(Reader, Array<Element>, operation(metadata, reader, output)))

Metadata preparation belongs inside the erased preservation proof. Passing a prepared cursor to a live certificate helper would retain or rebuild it.

template operation_equation source · line 70 · raw

@-Reader:Type -> @-Element:Data -> @-Metadata:Data -> @-ReaderCertificate:(@-reader:Reader -> Data) -> @-operation:(@_:Metadata -> @_:Reader -> @_:Array<Element> -> Pair(Reader, Array<Element>)) -> @-preserves:(@+depth:Nat -> @metadata:Metadata -> @-reader:Reader -> @-output:Array<Element> -> @_:ReaderCertificate(reader) -> @_:{output == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.normalized(Element, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(Element, output))) : Array<Element>} -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.ResultEvidence<Reader, Element, reader, depth, operation(metadata, reader, output)>) -> @metadata:Metadata -> @-reader:Reader -> @-output:Array<Element> -> @reader_certificate:ReaderCertificate(reader) -> @+depth:Nat -> @equation:{output == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.normalized(Element, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(Element, output))) : Array<Element>} -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.second(Reader, Array<Element>, operation(metadata, reader, output)) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.normalized(Element, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.second(Reader, Array<Element>, operation(metadata, reader, output))))) : Array<Element>}

template operation source · line 85 · raw

@-Reader:Type -> @-Element:Data -> @-Metadata:Data -> @-ReaderCertificate:(@-reader:Reader -> Data) -> @-operation:(@_:Metadata -> @_:Reader -> @_:Array<Element> -> Pair(Reader, Array<Element>)) -> @-preserves:(@+depth:Nat -> @metadata:Metadata -> @-reader:Reader -> @-output:Array<Element> -> @_:ReaderCertificate(reader) -> @_:{output == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.normalized(Element, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.reflect(Element, output))) : Array<Element>} -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.ResultEvidence<Reader, Element, reader, depth, operation(metadata, reader, output)>) -> @+metadata:Metadata -> @-reader:Reader -> @-output:Array<Element> -> @source_certificate:ReaderCertificate(reader) -> @equation_certificate:ReaderCertificate(reader) -> @reader_certificate:ReaderCertificate(reader) -> @output_certificate:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.Certificate<Element, output> -> Certificates<Reader, Element, ReaderCertificate, operation(metadata, reader, output)>

template fold_operation source · line 97 · raw

@-Reader:Type -> @-Accumulator:Data -> @-Metadata:Data -> @-ReaderCertificate:(@-reader:Reader -> Data) -> @-operation:(@_:Metadata -> @_:Reader -> @_:Accumulator -> Pair(Reader, Accumulator)) -> @-preserves:(@metadata:Metadata -> @-reader:Reader -> @-initial:Accumulator -> @_:ReaderCertificate(reader) -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.first(Reader, Accumulator, operation(metadata, reader, initial)) == reader : Reader}) -> @metadata:Metadata -> @-reader:Reader -> @-initial:Accumulator -> @proof_certificate:ReaderCertificate(reader) -> @certificate:ReaderCertificate(reader) -> ReaderCertificate(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.first(Reader, Accumulator, operation(metadata, reader, initial)))