def step_write_certificate
bendtorch-core@0.1.0.0 · src/tensor/core_PROOF.bend:501
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
501def step_write_certificate(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +index: U32,
502 -original_left: Core.Dynamic, -original_right: Core.Dynamic, -original_output: Core.Tensor<Shape.output_shape(plan)>,
503 +left_index: U32, +right_index: U32, +left_value: F32, +right_value: F32,
504 -indices_exact: {Done{(left_index, right_index)} == Elementwise.input_indices(plan, index) : Result<&2, &1, Core.Error, U32 & U32>},
505 certificate: Core.Write<Shape.output_shape(plan), original_output, index, Elementwise.scalar(operation, left_value, right_value)>,
506 left: Core.Dynamic, right: Core.Dynamic,
507 -left_exact: {(left, Done{left_value}) == Core.read_dynamic(original_left, left_index) : Core.Dynamic & Result<&2, &2, Core.Error, F32>},
508 -right_exact: {(right, Done{right_value}) == Core.read_dynamic(original_right, right_index) : Core.Dynamic & Result<&2, &2, Core.Error, F32>},
509 lift: @-result: Elementwise.Step<Shape.output_shape(plan)> ->
510 {result == Elementwise.step_write(Shape.output_shape(plan), left, right,
511 Core.write_flat(Shape.output_shape(plan), original_output, index, Elementwise.scalar(operation, left_value, right_value))) : Elementwise.Step<Shape.output_shape(plan)>} ->
512 {result == Elementwise.step(operation, plan, index, Elementwise.State{original_left, original_right, original_output}) : Elementwise.Step<Shape.output_shape(plan)>}) ->
513 Elementwise.StepCertificate<operation, plan, index, Elementwise.State{original_left, original_right, original_output}>:
514 Core.Write{output, result, exact} = certificate
515 match result:
516 case Fail{error}:
517 Elementwise.StepCertificate{Elementwise.Stop{left, right, error},
518 lift(Elementwise.Stop{left, right, error},
519 Equal.cong(Core.Tensor<Shape.output_shape(plan)> & Result<&2, &2, Core.Error, Unit>, Elementwise.Step<Shape.output_shape(plan)>,
520 pair => Elementwise.step_write(Shape.output_shape(plan), left, right, pair),
521 (output, Fail{error}), Core.write_flat(Shape.output_shape(plan), original_output, index, Elementwise.scalar(operation, left_value, right_value)), exact)), Unit{}}
522 case Done{unit}:
523 Elementwise.StepCertificate{Elementwise.Continue{Elementwise.State{left, right, output}},
524 lift(Elementwise.Continue{Elementwise.State{left, right, output}},
525 Equal.cong(Core.Tensor<Shape.output_shape(plan)> & Result<&2, &2, Core.Error, Unit>, Elementwise.Step<Shape.output_shape(plan)>,
526 pair => Elementwise.step_write(Shape.output_shape(plan), left, right, pair),
527 (output, Done{unit}), Core.write_flat(Shape.output_shape(plan), original_output, index, Elementwise.scalar(operation, left_value, right_value)), exact)),
528 ({\{RetainedSourceModel: kept => kept} : RetainedSourceModel<original_left, left> -> Elementwise.SameSource(original_left, left)}(retained_source_model(original_left, left, left_index, left_value, left_exact, Core.dynamic_source_read_keeps(original_left, left_index))),
529 ({\{RetainedSourceModel: kept => kept} : RetainedSourceModel<original_right, right> -> Elementwise.SameSource(original_right, right)}(retained_source_model(original_right, right, right_index, right_value, right_exact, Core.dynamic_source_read_keeps(original_right, right_index))),
530 {\{KnownUpdate: meaning =>
531 (update_route(Shape.output_shape(plan), original_output, output, index, Elementwise.scalar(operation, left_value, right_value), unit, meaning),
532 (Equal.trans(Maybe<&2, F32>, Core.observe(Shape.output_shape(plan), output, index), Some{Elementwise.scalar(operation, left_value, right_value)},
533 Elementwise.expected(operation, plan, original_left, original_right, index),
534 update_value(Shape.output_shape(plan), original_output, output, index, Elementwise.scalar(operation, left_value, right_value), unit, meaning),
535 {\{ExpectedValue: equal => equal} : ExpectedValue<operation, plan, index, original_left, original_right, left_value, right_value> ->
536 {Some{Elementwise.scalar(operation, left_value, right_value)} == Elementwise.expected(operation, plan, original_left, original_right, index) : Maybe<&2, F32>}}(expected_value(operation, plan, index, original_left, original_right, left_index, right_index, left_value, right_value, indices_exact,
537 read_value_model(original_left, left, left_index, left_value, left_exact, Core.dynamic_source_read_model(original_left, left_index)),
538 read_value_model(original_right, right, right_index, right_value, right_exact, Core.dynamic_source_read_model(original_right, right_index))))),
539 update_frame(Shape.output_shape(plan), original_output, output, index, Elementwise.scalar(operation, left_value, right_value), unit, meaning)))
540 } : KnownUpdate<Shape.output_shape(plan), original_output, output, index, Elementwise.scalar(operation, left_value, right_value), unit> ->
541 (Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), output}, index) &
542 ({Core.observe(Shape.output_shape(plan), output, index) == Elementwise.expected(operation, plan, original_left, original_right, index) : Maybe<&2, F32>} &
543 (@+other: U32 -> @checked: Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), original_output}, other) ->
544 @different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool} ->
545 Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), output}, other) &
546 {Core.observe(Shape.output_shape(plan), output, other) == Core.observe(Shape.output_shape(plan), original_output, other) : Maybe<&2, F32>})))}(known_update(Shape.output_shape(plan), original_output, output, index, Elementwise.scalar(operation, left_value, right_value), unit, exact,
547 update_model(Shape.output_shape(plan), original_output, index, Elementwise.scalar(operation, left_value, right_value))))))}