def mapped_value

bendtorch-core@0.1.0.0 · src/autograd/broadcast_PROOF.bend:104

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/elementwise.bend as Elementwise
import bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend as ElementwiseProof
import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformProof
import bendtorch-core@0.1.0.0/src/tensor/projection_LAWS.bend as Projection
import bendtorch-core@0.1.0.0/src/autograd/broadcast_LAWS.bend as Laws

104def mapped_value(+plan: Shape.BroadcastPlan, +index: U32, -input: Core.Dynamic, +target: Shape.Shape, -zeros: Core.Tensor<target>,
105  -right_dims: {Shape.dimensions(Shape.right_shape(plan)) == Shape.dimensions(target) : List<&2, U32>},
106  -indices: ElementwiseProof.IndicesDone<plan, Elementwise.input_indices(plan, index)>) ->
107  Holds<{Elementwise.expected(Elementwise.KeepLeft{}, plan, input, Core.Packed{target, zeros}, index) ==
108    Laws.source_value(input, Projection.offset_spec(plan, U32.to_nat(index))) : Maybe<&2, F32>}>:
109  Holds{{\{ElementwiseProof.IndicesDone: li => ri => exact => lb => rb =>
110    {\{TransformProof.PresentObservation: value => equal =>
111      {\{Holds: proof => proof} : Holds<{Elementwise.expected(Elementwise.KeepLeft{}, plan, input, Core.Packed{target, zeros}, index) ==
112    Laws.source_value(input, Projection.offset_spec(plan, U32.to_nat(index))) : Maybe<&2, F32>}> -> {Elementwise.expected(Elementwise.KeepLeft{}, plan, input, Core.Packed{target, zeros}, index) ==
113    Laws.source_value(input, Projection.offset_spec(plan, U32.to_nat(index))) : Maybe<&2, F32>}}(
114        keep_left_source(plan, index, input, Core.Packed{target, zeros}, li, ri, value, exact,
115          Equal.sym(Maybe<&2, F32>, Core.checked_observe(target, zeros, ri), Some{value}, equal)))} :
116      TransformProof.PresentObservation<target, zeros, ri> -> {Elementwise.expected(Elementwise.KeepLeft{}, plan, input, Core.Packed{target, zeros}, index) ==
117    Laws.source_value(input, Projection.offset_spec(plan, U32.to_nat(index))) : Maybe<&2, F32>}}(
118      TransformProof.present_observation(target, zeros, ri,
119        %right_dims : {Nat.is_lt(U32.to_nat(ri), Shape.logical_numel(_)) == True{} : Bool}
120        rb))} :
121    ElementwiseProof.IndicesDone<plan, Elementwise.input_indices(plan, index)> -> {Elementwise.expected(Elementwise.KeepLeft{}, plan, input, Core.Packed{target, zeros}, index) ==
122    Laws.source_value(input, Projection.offset_spec(plan, U32.to_nat(index))) : Maybe<&2, F32>}}(indices)}