def run_value

bendtorch-core@0.1.0.0 · src/tensor/reduction_PROOF.bend:318

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

318# A run of fuel + 1 words from slot `cursor` adds the words the tensor holds
319# there, in index order.
320def run_value(-shape: Shape.Shape, +depth: Nat, +length: Nat, -original: Array<F32>, -balanced: Model.Balanced(F32, depth, original),
321  -valid: {Storage.bounds(depth, length) == True{} : Bool},
322  -exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, fuel: Nat, +cursor: Nat, +accumulator: F32,
323  -array: Array<F32>, pair: Array<F32> & F32, -read: {pair == Array.get(F32, array, U32.from_nat(cursor)) : Array<F32> & F32},
324  -same: {array == original : Array<F32>}, values: List<&2, F32>,
325  logical: Laws.LogicalValues(1n+fuel, shape, Core.TTensor{Storage.Owned{depth, length, original, balanced, valid}, exact}, cursor, values)) ->
326  Fact<{Pair.fst(F32, Array<F32>, Reduction.array_run(fuel, cursor, accumulator, pair)) == Reduction.sequential_sum(values, accumulator) : F32}>:
327  match fuel pair values:
328    case 0n Tuple{kept, word} +value <> Nil{}:
329      Laws.LogicalStep{index_exact, observed, remaining} = logical
330      Fact{Equal.cong(F32, F32, w => F32.add(accumulator, w), word, value,
331        {\{Fact: p => p} : Fact<({Refinement.second(F32, (kept, word)) == value : F32})> -> {word == value : F32}}(
332          read_word(shape, depth, length, original, balanced, valid, exact, array, U32.from_nat(cursor), (kept, word), read, same, value, observed)))}
333    case 0n Tuple{kept, word} value <> later <> others:
334      Laws.LogicalStep{index_exact, observed, remaining} = logical
335      Fact{Empty.absurd({Pair.fst(F32, Array<F32>, Reduction.array_run(0n, cursor, accumulator, (kept, word))) ==
336        Reduction.sequential_sum(value <> later <> others, accumulator) : F32}, remaining)}
337    case 1n+next Tuple{kept, word} +value <> rest:
338      Laws.LogicalStep{index_exact, observed, remaining} = logical
339      -word_same = {\{Fact: p => p} : Fact<({Refinement.second(F32, (kept, word)) == value : F32})> -> {word == value : F32}}(
340        read_word(shape, depth, length, original, balanced, valid, exact, array, U32.from_nat(cursor), (kept, word), read, same, value, observed))
341      Fact{
342        %word_same : {Pair.fst(F32, Array<F32>, Reduction.array_run(next, 1n+cursor, F32.add(accumulator, word),
343          Array.get(F32, kept, U32.from_nat(1n+cursor)))) == Reduction.sequential_sum(rest, F32.add(accumulator, _)) : F32}
344        {\{Fact: p => p} : Fact<({Pair.fst(F32, Array<F32>, Reduction.array_run(next, 1n+cursor, F32.add(accumulator, word),
345          Array.get(F32, kept, U32.from_nat(1n+cursor)))) == Reduction.sequential_sum(rest, F32.add(accumulator, word)) : F32})> ->
346          {Pair.fst(F32, Array<F32>, Reduction.array_run(next, 1n+cursor, F32.add(accumulator, word),
347            Array.get(F32, kept, U32.from_nat(1n+cursor)))) == Reduction.sequential_sum(rest, F32.add(accumulator, word)) : F32}}(
348          run_value(shape, depth, length, original, balanced, valid, exact, next, 1n+cursor, F32.add(accumulator, word), kept,
349            Array.get(F32, kept, U32.from_nat(1n+cursor)), {==},
350            {\{Reduction.Fact: p => p} : Reduction.Fact<({Reduction.array_from((kept, word)) == original : Array<F32>})> -> {kept == original : Array<F32>}}(
351              Reduction.read_keeps(depth, original, balanced, array, U32.from_nat(cursor), (kept, word), read, same)),
352            rest, remaining))}
353    case fuel pair Nil{}:
354      Empty.absurd(Fact<{Pair.fst(F32, Array<F32>, Reduction.array_run(fuel, cursor, accumulator, pair)) == Reduction.sequential_sum(Nil{}, accumulator) : F32}>, logical)