def source_pair

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

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

559def source_pair(+fuel: Nat, -shape: Shape.Shape, -original: Core.Tensor<shape>, +cursor: Nat, +accumulator: F32,
560  -rec: @tensor: Core.Tensor<shape> -> @+value: F32 -> Laws.SourceSum<fuel, shape, tensor, 1n+cursor, value,
561    Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value)>,
562  -exact_cursor: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
563  certificate: Core.Read<shape, original, U32.from_nat(cursor)>,
564  -source: Core.SourceRead<shape, original, U32.from_nat(cursor)>, -retention: Core.SourceReadKeeps<shape, original, U32.from_nat(cursor)>) ->
565  Laws.SourceSum<1n+fuel, shape, original, cursor, accumulator, Reduction.read_step(shape,
566    tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, Core.read_flat(shape, original, U32.from_nat(cursor)))>:
567  Core.Read{tensor, +result, +exact} = certificate
568  Laws.SourceSum{unit =>
569    claim : @certificate: Laws.SourceSum<1n+fuel, shape, original, cursor, accumulator, Reduction.read_step(shape,
570      tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, (tensor, result))> ->
571      Laws.LoopMeaning(1n+fuel, shape, original, cursor, accumulator, Reduction.read_step(shape,
572        tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, (tensor, result))) =
573      \{Laws.SourceSum: proof => proof(Unit{})}
574    prove : @certificates: Core.SourceRead<shape, original, U32.from_nat(cursor)> & Core.SourceReadKeeps<shape, original, U32.from_nat(cursor)> ->
575      Laws.LoopMeaning(1n+fuel, shape, original, cursor, accumulator, Reduction.read_step(shape,
576        tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, Core.read_flat(shape, original, U32.from_nat(cursor)))) =
577      \{Tuple: \{Core.SourceRead: meaning => \{Core.SourceReadKeeps: kept =>
578        %exact : Laws.LoopMeaning(1n+fuel, shape, original, cursor, accumulator, Reduction.read_step(shape,
579          tensor => value => Reduction.natural_sum_loop(fuel, shape, tensor, 1n+cursor, value), accumulator, _))
580        claim(source_read(fuel, shape, original, cursor, accumulator, tensor, result, rec, exact_cursor,
581          Equal.trans(Maybe<&2, F32>, Core.result_value(result), Core.read_value(shape, Core.read_flat(shape, original, U32.from_nat(cursor))),
582            Core.checked_observe(shape, original, U32.from_nat(cursor)),
583            Equal.cong(Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>, Maybe<&2, F32>, pair => Core.read_value(shape, pair),
584              (tensor, result), Core.read_flat(shape, original, U32.from_nat(cursor)), exact), meaning),
585          other => Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, tensor, other),
586            Core.retained_read_observe(shape, Core.read_flat(shape, original, U32.from_nat(cursor)), other), Core.checked_observe(shape, original, other),
587            Equal.cong(Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>, Maybe<&2, F32>, pair => Core.retained_read_observe(shape, pair, other),
588              (tensor, result), Core.read_flat(shape, original, U32.from_nat(cursor)), exact), kept(other))))}}}
589    prove((source, retention))}