ReductionPROOF.run_value: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend as ReductionPROOF Lines 318-354 of bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend&start_line=318&end_line=354 import Base import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core import bendtorch-core@0.1.0.0/src/tensor/reduction.bend as Reduction import bendtorch-core@0.1.0.0/src/tensor/reduction_LAWS.bend as Laws import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage import bendtorch-core@0.1.0.0/src/storage/model.bend as Model import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement # A run of fuel + 1 words from slot `cursor` adds the words the tensor holds # there, in index order. def run_value(-shape: Shape.Shape, +depth: Nat, +length: Nat, -original: Array, -balanced: Model.Balanced(F32, depth, original), -valid: {Storage.bounds(depth, length) == True{} : Bool}, -exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, fuel: Nat, +cursor: Nat, +accumulator: F32, -array: Array, pair: Array & F32, -read: {pair == Array.get(F32, array, U32.from_nat(cursor)) : Array & F32}, -same: {array == original : Array}, values: List<&2, F32>, logical: Laws.LogicalValues(1n+fuel, shape, Core.TTensor{Storage.Owned{depth, length, original, balanced, valid}, exact}, cursor, values)) -> Fact<{Pair.fst(F32, Array, Reduction.array_run(fuel, cursor, accumulator, pair)) == Reduction.sequential_sum(values, accumulator) : F32}>: match fuel pair values: case 0n Tuple{kept, word} +value <> Nil{}: Laws.LogicalStep{index_exact, observed, remaining} = logical Fact{Equal.cong(F32, F32, w => F32.add(accumulator, w), word, value, {\{Fact: p => p} : Fact<({Refinement.second(F32, (kept, word)) == value : F32})> -> {word == value : F32}}( read_word(shape, depth, length, original, balanced, valid, exact, array, U32.from_nat(cursor), (kept, word), read, same, value, observed)))} case 0n Tuple{kept, word} value <> later <> others: Laws.LogicalStep{index_exact, observed, remaining} = logical Fact{Empty.absurd({Pair.fst(F32, Array, Reduction.array_run(0n, cursor, accumulator, (kept, word))) == Reduction.sequential_sum(value <> later <> others, accumulator) : F32}, remaining)} case 1n+next Tuple{kept, word} +value <> rest: Laws.LogicalStep{index_exact, observed, remaining} = logical -word_same = {\{Fact: p => p} : Fact<({Refinement.second(F32, (kept, word)) == value : F32})> -> {word == value : F32}}( read_word(shape, depth, length, original, balanced, valid, exact, array, U32.from_nat(cursor), (kept, word), read, same, value, observed)) Fact{ %word_same : {Pair.fst(F32, Array, Reduction.array_run(next, 1n+cursor, F32.add(accumulator, word), Array.get(F32, kept, U32.from_nat(1n+cursor)))) == Reduction.sequential_sum(rest, F32.add(accumulator, _)) : F32} {\{Fact: p => p} : Fact<({Pair.fst(F32, Array, Reduction.array_run(next, 1n+cursor, F32.add(accumulator, word), Array.get(F32, kept, U32.from_nat(1n+cursor)))) == Reduction.sequential_sum(rest, F32.add(accumulator, word)) : F32})> -> {Pair.fst(F32, Array, Reduction.array_run(next, 1n+cursor, F32.add(accumulator, word), Array.get(F32, kept, U32.from_nat(1n+cursor)))) == Reduction.sequential_sum(rest, F32.add(accumulator, word)) : F32}}( run_value(shape, depth, length, original, balanced, valid, exact, next, 1n+cursor, F32.add(accumulator, word), kept, Array.get(F32, kept, U32.from_nat(1n+cursor)), {==}, {\{Reduction.Fact: p => p} : Reduction.Fact<({Reduction.array_from((kept, word)) == original : Array})> -> {kept == original : Array}}( Reduction.read_keeps(depth, original, balanced, array, U32.from_nat(cursor), (kept, word), read, same)), rest, remaining))} case fuel pair Nil{}: Empty.absurd(Fact<{Pair.fst(F32, Array, Reduction.array_run(fuel, cursor, accumulator, pair)) == Reduction.sequential_sum(Nil{}, accumulator) : F32}>, logical) Uses (30): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.fst https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=dimensions https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=logical_numel https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=Storage https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=bounds https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=Balanced https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=second https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Tensor https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction.bend&name=Fact https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction.bend&name=array_from https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction.bend&name=array_run https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction.bend&name=read_keeps https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction.bend&name=sequential_sum https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_LAWS.bend&name=LogicalStep https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_LAWS.bend&name=LogicalValues https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend&name=Fact https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend&name=read_word