def prefix_observation

bendtorch-core@0.1.0.0 · src/tensor/transform_PROOF.bend:2234

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/transforms.bend as Transforms
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as WordConversion
import bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend as Totality

2234def prefix_observation(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>,
2235  -original: Core.Tensor<input>, -retained: Core.Tensor<input>, -target: Core.Tensor<Layout.output(input, axes, plan)>, +index: U32,
2236  -prefix: Transforms.Prefix<input, axes, plan, original, retained, target, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan)))>,
2237  -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan)))) == True{} : Bool}) ->
2238  Totality.CopyObservation<input, axes, plan, original, target, index>:
2239  Totality.CopyObservation{
2240    {\{Transforms.Prefix: kept => words => checked => written =>
2241      Equal.trans(Maybe<&2, F32>, Core.observe(Layout.output(input, axes, plan), target, index), Core.checked_observe(Layout.output(input, axes, plan), target, index),
2242        Transforms.expected_output(input, axes, plan, original, index),
2243        {\{ObserveBridge: equal => Equal.sym(Maybe<&2, F32>, Core.checked_observe(Layout.output(input, axes, plan), target, index), Core.observe(Layout.output(input, axes, plan), target, index), equal)} :
2244          ObserveBridge<Layout.output(input, axes, plan), target, index> ->
2245            {Core.observe(Layout.output(input, axes, plan), target, index) == Core.checked_observe(Layout.output(input, axes, plan), target, index) : Maybe<&2, F32>}}(
2246              observe_bridge(Layout.output(input, axes, plan), target, index,
2247                %WordConversion.word_natural_exact(index) : Core.ObservationChecked(Core.Packed{Layout.output(input, axes, plan), target}, _)
2248                checked(U32.to_nat(index), inside))),
2249        %WordConversion.word_natural_exact(index) :
2250          {Core.checked_observe(Layout.output(input, axes, plan), target, _) == Transforms.expected_output(input, axes, plan, original, _) : Maybe<&2, F32>}
2251        written(U32.to_nat(index), inside))} :
2252          Transforms.Prefix<input, axes, plan, original, retained, target, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan)))> ->
2253            {Core.observe(Layout.output(input, axes, plan), target, index) == Transforms.expected_output(input, axes, plan, original, index) : Maybe<&2, F32>}}(prefix)}