proofs/traversal_witness.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/traversal_witness.bend as Traversal_witness

Proof-only preservation of affine traversal owners. Reader values are handed back unchanged; output witnesses keep their original depth. Numerical loops call none of these functions: certificate equations use them under rewrites.

4 imports

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

Types

type Sample source · line 9 · raw

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

Sample

@-Reader:Type -> @-Element:Data -> @-reader:Reader -> @-result:Pair(Reader, Element) -> @-value:Element -> @equation:{result == (reader, value) : Pair(Reader, Element)} -> Sample<Reader, Element, reader, result>

type StateEvidence source · line 12 · raw

@-Reader:Type -> @-Element:Data -> @-Context:Data -> @-reader:Reader -> @-depth:Nat -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Reader, Array<Element>, Context> -> Data

StateEvidence

@-Reader:Type -> @-Element:Data -> @-Context:Data -> @-reader:Reader -> @-depth:Nat -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Reader, Array<Element>, Context> -> @-output:Array<Element> -> @position:U32 -> @context:Context -> @equation:{state == 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State{reader, output, position, context} : 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Reader, Array<Element>, Context>} -> @output_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(Element, depth, output) -> StateEvidence<Reader, Element, Context, reader, depth, state>

type ResultEvidence source · line 57 · raw

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

ResultEvidence

@-Reader:Type -> @-Element:Data -> @-reader:Reader -> @-depth:Nat -> @-result:Pair(Reader, Array<Element>) -> @-output:Array<Element> -> @equation:{result == (reader, output) : Pair(Reader, Array<Element>)} -> @output_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(Element, depth, output) -> ResultEvidence<Reader, Element, reader, depth, result>

type MapEvidence source · line 170 · raw

@-Element:Data -> @-Context:Data -> @-depth:Nat -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &1, Unit, Array<Element>, Context> -> Data

MapEvidence

@-Element:Data -> @-Context:Data -> @-depth:Nat -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &1, Unit, Array<Element>, Context> -> @-output:Array<Element> -> @position:U32 -> @context:Context -> @equation:{state == 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State{Unit{}, output, position, context} : 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &1, Unit, Array<Element>, Context>} -> @output_evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(Element, depth, output) -> MapEvidence<Element, Context, depth, state>

type FoldEvidence source · line 222 · raw

@-Reader:Type -> @-Accumulator:Data -> @-Context:Data -> @-reader:Reader -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &2, Reader, Accumulator, Context> -> Data

FoldEvidence

@-Reader:Type -> @-Accumulator:Data -> @-Context:Data -> @-reader:Reader -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &2, Reader, Accumulator, Context> -> @-accumulator:Accumulator -> @position:U32 -> @context:Context -> @equation:{state == 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State{reader, accumulator, position, context} : 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &2, Reader, Accumulator, Context>} -> FoldEvidence<Reader, Accumulator, Context, reader, state>

Templates

template store source · line 18 · raw

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

template step source · line 29 · raw

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

template run source · line 43 · raw

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

template finish source · line 61 · raw

@-Reader:Type -> @-Element:Data -> @-Context:Data -> @-reader:Reader -> @-depth:Nat -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &1, Reader, Array<Element>, Context> -> @evidence:StateEvidence<Reader, Element, Context, reader, depth, state> -> ResultEvidence<Reader, Element, reader, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.finish(Reader, Element, Context, state)>

template array_evidence source · line 70 · raw

@-Element:Data -> @-storage:Array<Element> -> Data

template array_sample source · line 73 · raw

@-Element:Data -> @-storage:Array<Element> -> @-result:Pair(Array<Element>, Element) -> @read:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Read<Element, storage, result> -> Sample<Array<Element>, Element, storage, result>

template offset_read source · line 78 · raw

@-Element:Data -> @-storage:Array<Element> -> @context:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.Offsets -> @index:U32 -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.ArrayWitness<Element, storage> -> Sample<Array<Element>, Element, storage, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.source_offset(Element, storage, context, index)>

template first source · line 84 · raw

@-Left:Type -> @-Right:Type -> @pair:Pair(Left, Right) -> Left

template second source · line 88 · raw

@-Left:Type -> @-Right:Type -> @pair:Pair(Left, Right) -> Right

template source_unchanged source · line 92 · raw

@-Reader:Type -> @-Element:Data -> @-reader:Reader -> @-depth:Nat -> @-result:Pair(Reader, Array<Element>) -> @evidence:ResultEvidence<Reader, Element, reader, depth, result> -> {first(Reader, Array<Element>, result) == reader : Reader}

template output_witness source · line 98 · raw

@-Reader:Type -> @-Element:Data -> @-reader:Reader -> @-depth:Nat -> @-result:Pair(Reader, Array<Element>) -> @evidence:ResultEvidence<Reader, Element, reader, depth, result> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(Element, depth, second(Reader, Array<Element>, result))

template update_sample source · line 105 · raw

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

template update_current source · line 120 · raw

@-Reader:Type -> @-Element:Data -> @-Value:Data -> @-Context:Data -> @-read:(@_:Reader -> @_:Context -> @_:U32 -> Pair(Reader, Value)) -> @-combine:(@_:Element -> @_:Value -> Element) -> @-destination:(@_:Context -> @_:U32 -> U32) -> @+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, Value, reader, read(reader, context, position)> -> StateEvidence<Reader, Element, Context, reader, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.update_current(Reader, Element, Value, Context, read, combine, destination, reader, position, context, result)>

template update_step source · line 136 · raw

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

template update source · line 154 · raw

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

template mapped_value source · line 176 · raw

@-Element:Data -> @-Context:Data -> @-map:(@_:Context -> @_:Element -> Element) -> @+depth:Nat -> @+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> -> MapEvidence<Element, Context, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.mapped_value(Element, Context, map, position, context, result)>

template map_step source · line 187 · raw

@-Element:Data -> @-Context:Data -> @-map:(@_:Context -> @_:Element -> Element) -> @+depth:Nat -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &1, Unit, Array<Element>, Context> -> @evidence:MapEvidence<Element, Context, depth, state> -> MapEvidence<Element, Context, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.map_step(Element, Context, map, state)>

template map_run source · line 197 · raw

@-Element:Data -> @-Context:Data -> @-map:(@_:Context -> @_:Element -> Element) -> @+depth:Nat -> @count:Nat -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &1, Unit, Array<Element>, Context> -> @evidence:MapEvidence<Element, Context, depth, state> -> MapEvidence<Element, Context, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_loop.run(0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &1, Unit, Array<Element>, Context>, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.map_step(Element, Context, map), count, state)>

template mapped_output source · line 206 · raw

@-Element:Data -> @-Context:Data -> @-depth:Nat -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&2, &1, Unit, Array<Element>, Context> -> @evidence:MapEvidence<Element, Context, depth, state> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(Element, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.mapped_output(Element, Context, state))

template map_in_place source · line 214 · raw

@-Element:Data -> @-Context:Data -> @-map:(@_:Context -> @_:Element -> Element) -> @+depth:Nat -> @count:Nat -> @position:U32 -> @context:Context -> @-output:Array<Element> -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(Element, depth, output) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.Witness(Element, depth, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.map_in_place(Element, Context, map, count, position, context, output))

template fold_value source · line 227 · raw

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

template fold_step source · line 239 · raw

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

template fold_run source · line 253 · raw

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

template fold_finished source · line 268 · raw

@-Reader:Type -> @-Accumulator:Data -> @-Context:Data -> @-reader:Reader -> @-state:0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.State<&1, &2, Reader, Accumulator, Context> -> @evidence:FoldEvidence<Reader, Accumulator, Context, reader, state> -> {first(Reader, Accumulator, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.finish_fold(Reader, Accumulator, Context, state)) == reader : Reader}

template fold source · line 277 · raw

@-Reader:Type -> @-Element:Data -> @-Accumulator:Data -> @-Context:Data -> @-ReaderEvidence:(@-reader:Reader -> Data) -> @-read:(@_:Reader -> @_:Context -> @_:U32 -> Pair(Reader, Element)) -> @-combine:(@_:Accumulator -> @_:Element -> Accumulator) -> @-read_preserves:(@-reader:Reader -> @context:Context -> @index:U32 -> @_:ReaderEvidence(reader) -> Sample<Reader, Element, reader, read(reader, context, index)>) -> @count:Nat -> @-reader:Reader -> @position:U32 -> @context:Context -> @-initial:Accumulator -> @reader_evidence:ReaderEvidence(reader) -> {first(Reader, Accumulator, 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.fold(Reader, Element, Accumulator, Context, read, combine, count, position, reader, initial, context)) == reader : Reader}