def step_left_certificate
bendtorch-core@0.1.0.0 · src/tensor/core_PROOF.bend:581
import bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend as CorePROOF
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
581def step_left_certificate(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +index: U32,
582 -original_left: Core.Dynamic, original_right: Core.Dynamic, original_output: Core.Tensor<Shape.output_shape(plan)>,
583 +left_index: U32, +right_index: U32,
584 -indices_exact: {Done{(left_index, right_index)} == Elementwise.input_indices(plan, index) : Result<&2, &1, Core.Error, U32 & U32>},
585 lift: @-result: Elementwise.Step<Shape.output_shape(plan)> ->
586 {result == Elementwise.step_left(operation, Shape.output_shape(plan), index, original_right, original_output, right_index,
587 Core.read_dynamic(original_left, left_index)) : Elementwise.Step<Shape.output_shape(plan)>} ->
588 {result == Elementwise.step(operation, plan, index, Elementwise.State{original_left, original_right, original_output}) : Elementwise.Step<Shape.output_shape(plan)>},
589 certificate: Core.DynamicRead<original_left, left_index>) ->
590 Elementwise.StepCertificate<operation, plan, index, Elementwise.State{original_left, original_right, original_output}>:
591 Core.DynamicRead{left, result, exact} = certificate
592 match result:
593 case Fail{error}:
594 Elementwise.StepCertificate{Elementwise.Stop{left, original_right, error},
595 lift(Elementwise.Stop{left, original_right, error}, Equal.cong(Core.Dynamic & Result<&2, &2, Core.Error, F32>, Elementwise.Step<Shape.output_shape(plan)>,
596 pair => Elementwise.step_left(operation, Shape.output_shape(plan), index, original_right, original_output, right_index, pair),
597 (left, Fail{error}), Core.read_dynamic(original_left, left_index), exact)), Unit{}}
598 case Done{+left_value}:
599 step_right_certificate(operation, plan, index, original_left, original_right,
600 left_index, right_index, left_value, indices_exact, Core.dynamic_read_certificate(original_right, right_index), original_output, left, exact,
601 result => equality => lift(result,
602 Equal.trans(Elementwise.Step<Shape.output_shape(plan)>, result,
603 Elementwise.step_left(operation, Shape.output_shape(plan), index, original_right, original_output, right_index, (left, Done{left_value})),
604 Elementwise.step_left(operation, Shape.output_shape(plan), index, original_right, original_output, right_index, Core.read_dynamic(original_left, left_index)), equality,
605 Equal.cong(Core.Dynamic & Result<&2, &2, Core.Error, F32>, Elementwise.Step<Shape.output_shape(plan)>,
606 pair => Elementwise.step_left(operation, Shape.output_shape(plan), index, original_right, original_output, right_index, pair),
607 (left, Done{left_value}), Core.read_dynamic(original_left, left_index), exact))))