CorePROOF.step_write_certificate: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend as CorePROOF Lines 501-547 of bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&start_line=501&end_line=547 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 def step_write_certificate(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +index: U32, -original_left: Core.Dynamic, -original_right: Core.Dynamic, -original_output: Core.Tensor, +left_index: U32, +right_index: U32, +left_value: F32, +right_value: F32, -indices_exact: {Done{(left_index, right_index)} == Elementwise.input_indices(plan, index) : Result<&2, &1, Core.Error, U32 & U32>}, certificate: Core.Write, left: Core.Dynamic, right: Core.Dynamic, -left_exact: {(left, Done{left_value}) == Core.read_dynamic(original_left, left_index) : Core.Dynamic & Result<&2, &2, Core.Error, F32>}, -right_exact: {(right, Done{right_value}) == Core.read_dynamic(original_right, right_index) : Core.Dynamic & Result<&2, &2, Core.Error, F32>}, lift: @-result: Elementwise.Step -> {result == Elementwise.step_write(Shape.output_shape(plan), left, right, Core.write_flat(Shape.output_shape(plan), original_output, index, Elementwise.scalar(operation, left_value, right_value))) : Elementwise.Step} -> {result == Elementwise.step(operation, plan, index, Elementwise.State{original_left, original_right, original_output}) : Elementwise.Step}) -> Elementwise.StepCertificate: Core.Write{output, result, exact} = certificate match result: case Fail{error}: Elementwise.StepCertificate{Elementwise.Stop{left, right, error}, lift(Elementwise.Stop{left, right, error}, Equal.cong(Core.Tensor & Result<&2, &2, Core.Error, Unit>, Elementwise.Step, pair => Elementwise.step_write(Shape.output_shape(plan), left, right, pair), (output, Fail{error}), Core.write_flat(Shape.output_shape(plan), original_output, index, Elementwise.scalar(operation, left_value, right_value)), exact)), Unit{}} case Done{unit}: Elementwise.StepCertificate{Elementwise.Continue{Elementwise.State{left, right, output}}, lift(Elementwise.Continue{Elementwise.State{left, right, output}}, Equal.cong(Core.Tensor & Result<&2, &2, Core.Error, Unit>, Elementwise.Step, pair => Elementwise.step_write(Shape.output_shape(plan), left, right, pair), (output, Done{unit}), Core.write_flat(Shape.output_shape(plan), original_output, index, Elementwise.scalar(operation, left_value, right_value)), exact)), ({\{RetainedSourceModel: kept => kept} : RetainedSourceModel -> 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))), ({\{RetainedSourceModel: kept => kept} : RetainedSourceModel -> 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))), {\{KnownUpdate: meaning => (update_route(Shape.output_shape(plan), original_output, output, index, Elementwise.scalar(operation, left_value, right_value), unit, meaning), (Equal.trans(Maybe<&2, F32>, Core.observe(Shape.output_shape(plan), output, index), Some{Elementwise.scalar(operation, left_value, right_value)}, Elementwise.expected(operation, plan, original_left, original_right, index), update_value(Shape.output_shape(plan), original_output, output, index, Elementwise.scalar(operation, left_value, right_value), unit, meaning), {\{ExpectedValue: equal => equal} : ExpectedValue -> {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, read_value_model(original_left, left, left_index, left_value, left_exact, Core.dynamic_source_read_model(original_left, left_index)), read_value_model(original_right, right, right_index, right_value, right_exact, Core.dynamic_source_read_model(original_right, right_index))))), update_frame(Shape.output_shape(plan), original_output, output, index, Elementwise.scalar(operation, left_value, right_value), unit, meaning))) } : KnownUpdate -> (Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), output}, index) & ({Core.observe(Shape.output_shape(plan), output, index) == Elementwise.expected(operation, plan, original_left, original_right, index) : Maybe<&2, F32>} & (@+other: U32 -> @checked: Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), original_output}, other) -> @different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool} -> Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), output}, other) & {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, update_model(Shape.output_shape(plan), original_output, index, Elementwise.scalar(operation, left_value, right_value))))))} Uses (45): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BroadcastPlan https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=output_shape https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Dynamic https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Error https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=ObservationChecked https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Tensor https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Write https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=dynamic_source_read_keeps https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=dynamic_source_read_model https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=observe https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=read_dynamic https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=write_flat https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=ExpectedValue https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=KnownUpdate https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=RetainedSourceModel https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=expected_value https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=known_update https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=read_value_model https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=retained_source_model https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=update_frame https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=update_model https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=update_route https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=update_value https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=Operation https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=SameSource https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=State https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=Step https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=StepCertificate https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=expected https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=input_indices https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=scalar https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=step https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=step_write