GradientPROOF.position_inv: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend as GradientPROOF Lines 321-346 of bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&start_line=321&end_line=346 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/transform_PROOF.bend as TransformProof import bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend as ReduceProof def position_inv(+shape: Shape.Shape, -original: Core.Tensor, -contribution: Core.Dynamic, +cursor: Nat, -before: Core.Tensor, read_owner: Core.Tensor, -written: Core.Tensor, +index: U32, +accumulated: F32, +value: F32, -unit: Unit, +other: U32, decision: Shape.BoolCase, -inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}, -exact: {U32.to_nat(index) == cursor : Nat}, -meaning: Core.CheckedUpdateMeaning(shape, read_owner, index, F32.add(accumulated, value), (written, Done{unit})), -inv: Inv(shape, original, contribution, cursor, before), -read: {Core.checked_observe(shape, before, index) == Some{accumulated} : Maybe<&2, F32>}, -kept: @+position: U32 -> {Core.checked_observe(shape, read_owner, position) == Core.checked_observe(shape, before, position) : Maybe<&2, F32>}, -word: {Core.checked_observe_dynamic(contribution, index) == Some{value} : Maybe<&2, F32>}) -> Holds<{Core.checked_observe(shape, written, other) == partial(Nat.is_lt(U32.to_nat(other), 1n+cursor), Core.checked_observe(shape, original, other), Core.checked_observe_dynamic(contribution, other)) : Maybe<&2, F32>}>: match decision: case Shape.BTrue{equal}: written_true(shape, original, contribution, cursor, before, written, index, accumulated, value, other, equal, inside, exact, inv, read, ReduceProof.update_written(shape, read_owner, written, index, F32.add(accumulated, value), unit, meaning), word) case Shape.BFalse{equal}: written_false(shape, original, contribution, cursor, before, read_owner, written, index, other, equal, inside, exact, inv, kept(other), ReduceProof.frame_equal(shape, written, read_owner, other, ReduceProof.update_frame(shape, read_owner, written, index, F32.add(accumulated, value), unit, meaning)(other)( {\{TransformProof.CheckedObservationModel: checked => checked} : TransformProof.CheckedObservationModel -> Core.ObservationChecked(Core.Packed{shape, read_owner}, other)}( TransformProof.checked_observation_model(shape, read_owner, other, inside)))( Equal.sym(Bool, False{}, Nat.is_eq(U32.to_nat(index), U32.to_nat(other)), equal)))) Uses (33): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat 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=Nat.is_lt 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/autograd/gradient_PROOF.bend&name=Holds https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&name=Inv https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&name=partial https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&name=written_false https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&name=written_true https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend&name=frame_equal https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend&name=update_frame https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend&name=update_written https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BoolCase https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=dimensions https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=logical_numel https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=CheckedUpdateMeaning 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=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=checked_observe https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=checked_observe_dynamic https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=CheckedObservationModel https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=checked_observation_model