proofs/traversal_visit_witness.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/traversal_visit_witness.bend as Traversal_visit_witness

Shape and owner preservation for traversals with consumed cursor state.

5 imports

import Base
import ../traversal_array.bend as Traversal
import ../traversal_loop.bend as Loop
import ./storage_witness.bend as Witness
import ./traversal_witness.bend as TraversalWitness

Types

type Sample source · line 8 · raw

@-Reader:Type -> @-Element:Data -> @-Context:Data -> @-reader:Reader -> @-result:Pair(Reader, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.Visited<Context, Element>) -> Data

Sample

@-Reader:Type -> @-Element:Data -> @-Context:Data -> @-reader:Reader -> @-result:Pair(Reader, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.Visited<Context, Element>) -> @context:Context -> @-value:Element -> @equation:{result == (reader, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.Visited{context, value}) : Pair(Reader, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.Visited<Context, Element>)} -> Sample<Reader, Element, Context, reader, result>

Templates

template store source · line 11 · raw

@-Reader:Type -> @-Element:Data -> @-Context:Data -> @+depth:Nat -> @-reader:Reader -> @+position:U32 -> @-output:Array<Element> -> @-result:Pair(Reader, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.Visited<Context, Element>) -> @output_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(Element, depth, output) -> @sample:Sample<Reader, Element, Context, reader, result> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.StateEvidence<Reader, Element, Context, reader, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.visit_store(Reader, Element, Context, position, output, result)>

template step source · line 20 · raw

@-Reader:Type -> @-Element:Data -> @-Context:Data -> @-ReaderEvidence:(@-reader:Reader -> Data) -> @-read:(@_:Reader -> @_:Context -> Pair(Reader, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.Visited<Context, Element>)) -> @-read_preserves:(@-reader:Reader -> @context:Context -> @_:ReaderEvidence(reader) -> Sample<Reader, Element, Context, reader, read(reader, context)>) -> @+depth:Nat -> @-reader:Reader -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Reader, Array<Element>, Context> -> @reader_evidence:ReaderEvidence(reader) -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.StateEvidence<Reader, Element, Context, reader, depth, state> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.StateEvidence<Reader, Element, Context, reader, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.visit_step(Reader, Element, Context, read, state)>

template spread_store source · line 32 · raw

@-Element:Data -> @-Context:Data -> @+depth:Nat -> @-input:Array<Element> -> @+position:U32 -> @-output:Array<Element> -> @target:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.Target<Context> -> @-result:Pair(Array<Element>, Element) -> @output_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(Element, depth, output) -> @observed:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Read<Element, input, result> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.StateEvidence<Array<Element>, Element, Context, input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.spread_store(Element, Context, position, output, target, result)>

template spread_step source · line 41 · raw

@-Element:Data -> @-Context:Data -> @-target:(@_:Context -> 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.Target<Context>) -> @+depth:Nat -> @-input:Array<Element> -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Array<Element>, Array<Element>, Context> -> @input_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<Element, input> -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.StateEvidence<Array<Element>, Element, Context, input, depth, state> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.StateEvidence<Array<Element>, Element, Context, input, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.spread_step(Element, Context, target, state)>

template update_sample source · line 52 · raw

@-Reader:Type -> @-Element:Data -> @-Context:Data -> @-combine:(@_:Element -> @_:Element -> Element) -> @+depth:Nat -> @-reader:Reader -> @+position:U32 -> @-output:Array<Element> -> @-current:Element -> @-result:Pair(Reader, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.Visited<Context, Element>) -> @output_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(Element, depth, output) -> @sample:Sample<Reader, Element, Context, reader, result> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.StateEvidence<Reader, Element, Context, reader, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.visit_update_sample(Reader, Element, Context, combine, position, output, current, result)>

template update_current source · line 63 · raw

@-Reader:Type -> @-Element:Data -> @-Context:Data -> @-read:(@_:Reader -> @_:Context -> Pair(Reader, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.Visited<Context, Element>)) -> @-combine:(@_:Element -> @_:Element -> Element) -> @+depth:Nat -> @-reader:Reader -> @position:U32 -> @context:Context -> @-output:Array<Element> -> @-result:Pair(Array<Element>, Element) -> @output_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(Element, depth, output) -> @observed:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Read<Element, output, result> -> @sample:Sample<Reader, Element, Context, reader, read(reader, context)> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.StateEvidence<Reader, Element, Context, reader, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.visit_update_current(Reader, Element, Context, read, combine, position, context, reader, result)>

template update_step source · line 73 · raw

@-Reader:Type -> @-Element:Data -> @-Context:Data -> @-ReaderEvidence:(@-reader:Reader -> Data) -> @-read:(@_:Reader -> @_:Context -> Pair(Reader, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.Visited<Context, Element>)) -> @-combine:(@_:Element -> @_:Element -> Element) -> @-read_preserves:(@-reader:Reader -> @context:Context -> @_:ReaderEvidence(reader) -> Sample<Reader, Element, Context, reader, read(reader, context)>) -> @+depth:Nat -> @-reader:Reader -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Reader, Array<Element>, Context> -> @reader_evidence:ReaderEvidence(reader) -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.StateEvidence<Reader, Element, Context, reader, depth, state> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.StateEvidence<Reader, Element, Context, reader, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.visit_update_step(Reader, Element, Context, read, combine, state)>

template update source · line 86 · raw

@-Reader:Type -> @-Element:Data -> @-Context:Data -> @-ReaderEvidence:(@-reader:Reader -> Data) -> @-read:(@_:Reader -> @_:Context -> Pair(Reader, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.Visited<Context, Element>)) -> @-combine:(@_:Element -> @_:Element -> Element) -> @-read_preserves:(@-reader:Reader -> @context:Context -> @_:ReaderEvidence(reader) -> Sample<Reader, Element, Context, reader, read(reader, context)>) -> @+depth:Nat -> @count:Nat -> @-reader:Reader -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Reader, Array<Element>, Context> -> @+reader_evidence:ReaderEvidence(reader) -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.StateEvidence<Reader, Element, Context, reader, depth, state> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.StateEvidence<Reader, Element, Context, reader, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.visit_update(Reader, Element, Context, read, combine, count, state)>

template fold_value source · line 99 · raw

@-Reader:Type -> @-Element:Data -> @-Accumulator:Data -> @-Context:Data -> @-combine:(@_:Accumulator -> @_:Element -> Accumulator) -> @-reader:Reader -> @+position:U32 -> @-accumulator:Accumulator -> @-result:Pair(Reader, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.Visited<Context, Element>) -> @sample:Sample<Reader, Element, Context, reader, result> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.FoldEvidence<Reader, Accumulator, Context, reader, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.visit_fold_value(Reader, Element, Accumulator, Context, combine, position, accumulator, result)>

template fold_step source · line 108 · raw

@-Reader:Type -> @-Element:Data -> @-Accumulator:Data -> @-Context:Data -> @-ReaderEvidence:(@-reader:Reader -> Data) -> @-read:(@_:Reader -> @_:Context -> Pair(Reader, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.Visited<Context, Element>)) -> @-combine:(@_:Accumulator -> @_:Element -> Accumulator) -> @-read_preserves:(@-reader:Reader -> @context:Context -> @_:ReaderEvidence(reader) -> Sample<Reader, Element, Context, reader, read(reader, context)>) -> @-reader:Reader -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &2, Reader, Accumulator, Context> -> @reader_evidence:ReaderEvidence(reader) -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.FoldEvidence<Reader, Accumulator, Context, reader, state> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.FoldEvidence<Reader, Accumulator, Context, reader, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.visit_fold_step(Reader, Element, Accumulator, Context, read, combine, state)>

template fold_run source · line 120 · raw

@-Reader:Type -> @-Element:Data -> @-Accumulator:Data -> @-Context:Data -> @-ReaderEvidence:(@-reader:Reader -> Data) -> @-read:(@_:Reader -> @_:Context -> Pair(Reader, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.Visited<Context, Element>)) -> @-combine:(@_:Accumulator -> @_:Element -> Accumulator) -> @-read_preserves:(@-reader:Reader -> @context:Context -> @_:ReaderEvidence(reader) -> Sample<Reader, Element, Context, reader, read(reader, context)>) -> @count:Nat -> @-reader:Reader -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &2, Reader, Accumulator, Context> -> @+reader_evidence:ReaderEvidence(reader) -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.FoldEvidence<Reader, Accumulator, Context, reader, state> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.FoldEvidence<Reader, Accumulator, Context, reader, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.visit_fold(Reader, Element, Accumulator, Context, read, combine, count, state)>