def source_read

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

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

535def source_read(+fuel: Nat, -shape: Shape.Shape, -original: Core.Tensor<shape>, +cursor: Nat, +accumulator: F32,
536  tensor: Core.Tensor<shape>, result: Result<&2, &2, Core.Error, F32>,
537  -rec: @tensor: Core.Tensor<shape> -> @+value: F32 -> Laws.SourceSum<fuel, shape, tensor, 1n+cursor, value,
538    Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value)>,
539  -exact: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
540  -meaning: {Core.result_value(result) == Core.checked_observe(shape, original, U32.from_nat(cursor)) : Maybe<&2, F32>},
541  -kept: @+other: U32 -> {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}) ->
542  Laws.SourceSum<1n+fuel, shape, original, cursor, accumulator, Reduction.read_step(shape,
543    tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, (tensor, result))>:
544  match result:
545    case Fail{error}:
546      Laws.SourceSum{unit => Unit{}}
547    case Done{+value}:
548      Laws.SourceSum{unit =>
549        claim : @certificate: Laws.SourceSum<fuel, shape, tensor, 1n+cursor, F32.add(accumulator, value),
550          Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, F32.add(accumulator, value))> ->
551          Laws.LoopMeaning(fuel, shape, tensor, 1n+cursor, F32.add(accumulator, value),
552            Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, F32.add(accumulator, value))) =
553          \{Laws.SourceSum: proof => proof(Unit{})}
554        source_extend(fuel, shape, original, tensor, cursor, accumulator, value,
555          Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, F32.add(accumulator, value)),
556          claim(rec(tensor, F32.add(accumulator, value))), exact,
557          Equal.sym(Maybe<&2, F32>, Some{value}, Core.checked_observe(shape, original, U32.from_nat(cursor)), meaning), kept)}