proofs/kernel_tile_witness.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/kernel_tile_witness.bend as Kernel_tile_witness

4 imports

import Base
import ../kernel_block.bend as Block
import ../kernel_tile.bend as Tile
import ./traversal_witness.bend as TraversalWitness

Templates

template pair source · line 8 · raw

@-State:Type -> @-Context:Data -> @-Element:Data -> @-read:(@_:State -> @_:Context -> @_:Nat -> Pair(State, Element)) -> @-stride:Nat -> @-state:State -> @-context:Context -> @+index:Nat -> @first:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<State, Element, state, read(state, context, index)> -> @second:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<State, Element, state, read(state, context, Nat.add(index, stride))> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<State, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_block.Twin<Element>, state, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_block.read_pair(State, Context, Element, read, stride, state, context, index)>

Pair composition consumes already established observations. Context and values may be erased, so a cached head need not become a live proof field.

template finish source · line 21 · raw

@-State:Type -> @-state:State -> @-result:Pair(State, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_block.Twin<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_block.Twin<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_block.Twin<F32>>>) -> @evidence:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<State, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_block.Twin<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_block.Twin<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_block.Twin<F32>>>, state, result> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<State, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, state, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.finish_pairs(State, result)>

template with_head source · line 29 · raw

@-State:Type -> @-Context:Data -> @-Evidence:(@-state:State -> Data) -> @-read:(@_:State -> @_:Context -> @_:Nat -> Pair(State, F32)) -> @-read_preserves:(@-state:State -> @context:Context -> @index:Nat -> @_:Evidence(state) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<State, F32, state, read(state, context, index)>) -> @-state:State -> @+context:Context -> @-head:F32 -> @+index:Nat -> @evidence:Evidence(state) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<State, F32, state, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.read_with_head(State, Context, read, state, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.HeadContext{head, context}, index)>

template pair_head source · line 38 · raw

@-State:Type -> @-Context:Data -> @-Evidence:(@-state:State -> Data) -> @-read:(@_:State -> @_:Context -> @_:Nat -> Pair(State, F32)) -> @-read_preserves:(@-state:State -> @context:Context -> @index:Nat -> @_:Evidence(state) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<State, F32, state, read(state, context, index)>) -> @-state:State -> @+context:Context -> @-head:F32 -> @+index:Nat -> @+evidence:Evidence(state) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<State, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_block.Twin<F32>, state, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_block.read_pair(State, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.HeadContext<Context>, F32, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.read_with_head(State, Context, read), 1n, state, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.HeadContext{head, context}, index)>

template four_head source · line 48 · raw

@-State:Type -> @-Context:Data -> @-Evidence:(@-state:State -> Data) -> @-read:(@_:State -> @_:Context -> @_:Nat -> Pair(State, F32)) -> @-read_preserves:(@-state:State -> @context:Context -> @index:Nat -> @_:Evidence(state) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<State, F32, state, read(state, context, index)>) -> @-state:State -> @+context:Context -> @-head:F32 -> @+index:Nat -> @+evidence:Evidence(state) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<State, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_block.Twin<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_block.Twin<F32>>, state, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_block.read_pair(State, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.HeadContext<Context>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_block.Twin<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_block.read_pair(State, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.HeadContext<Context>, F32, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.read_with_head(State, Context, read), 1n), 2n, state, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.HeadContext{head, context}, index)>

template eight_head source · line 60 · raw

@-State:Type -> @-Context:Data -> @-Evidence:(@-state:State -> Data) -> @-read:(@_:State -> @_:Context -> @_:Nat -> Pair(State, F32)) -> @-read_preserves:(@-state:State -> @context:Context -> @index:Nat -> @_:Evidence(state) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<State, F32, state, read(state, context, index)>) -> @-state:State -> @+context:Context -> @-head:F32 -> @+evidence:Evidence(state) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<State, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_block.Twin<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_block.Twin<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_block.Twin<F32>>>, state, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_block.read_pair(State, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.HeadContext<Context>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_block.Twin<0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_block.Twin<F32>>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_block.read_pair(State, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.HeadContext<Context>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_block.Twin<F32>, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_block.read_pair(State, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.HeadContext<Context>, F32, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.read_with_head(State, Context, read), 1n), 2n), 4n, state, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.HeadContext{head, context}, 0n)>

template tail source · line 74 · raw

@-State:Type -> @-Context:Data -> @-Evidence:(@-state:State -> Data) -> @-read:(@_:State -> @_:Context -> @_:Nat -> Pair(State, F32)) -> @-read_preserves:(@-state:State -> @context:Context -> @index:Nat -> @_:Evidence(state) -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<State, F32, state, read(state, context, index)>) -> @-state:State -> @+context:Context -> @-first:Pair(State, F32) -> @evidence:Evidence(state) -> @sample:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<State, F32, state, first> -> 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.Sample<State, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.Tile8, state, 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.read_tail(State, Context, read, first, context)>