def position_inv

bendtorch-core@0.1.0.0 · src/autograd/gradient_PROOF.bend:321

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

321def position_inv(+shape: Shape.Shape, -original: Core.Tensor<shape>, -contribution: Core.Dynamic, +cursor: Nat,
322  -before: Core.Tensor<shape>, read_owner: Core.Tensor<shape>, -written: Core.Tensor<shape>,
323  +index: U32, +accumulated: F32, +value: F32, -unit: Unit,
324  +other: U32, decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(index), U32.to_nat(other))>,
325  -inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool},
326  -exact: {U32.to_nat(index) == cursor : Nat},
327  -meaning: Core.CheckedUpdateMeaning(shape, read_owner, index, F32.add(accumulated, value), (written, Done{unit})),
328  -inv: Inv(shape, original, contribution, cursor, before),
329  -read: {Core.checked_observe(shape, before, index) == Some{accumulated} : Maybe<&2, F32>},
330  -kept: @+position: U32 -> {Core.checked_observe(shape, read_owner, position) == Core.checked_observe(shape, before, position) : Maybe<&2, F32>},
331  -word: {Core.checked_observe_dynamic(contribution, index) == Some{value} : Maybe<&2, F32>}) ->
332  Holds<{Core.checked_observe(shape, written, other) ==
333    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>}>:
334  match decision:
335    case Shape.BTrue{equal}:
336      written_true(shape, original, contribution, cursor, before, written, index, accumulated, value, other, equal, inside, exact, inv, read,
337        ReduceProof.update_written(shape, read_owner, written, index, F32.add(accumulated, value), unit, meaning), word)
338    case Shape.BFalse{equal}:
339      written_false(shape, original, contribution, cursor, before, read_owner, written, index, other, equal, inside, exact, inv,
340        kept(other),
341        ReduceProof.frame_equal(shape, written, read_owner, other,
342          ReduceProof.update_frame(shape, read_owner, written, index, F32.add(accumulated, value), unit, meaning)(other)(
343            {\{TransformProof.CheckedObservationModel: checked => checked} :
344              TransformProof.CheckedObservationModel<shape, read_owner, other> -> Core.ObservationChecked(Core.Packed{shape, read_owner}, other)}(
345              TransformProof.checked_observation_model(shape, read_owner, other, inside)))(
346            Equal.sym(Bool, False{}, Nat.is_eq(U32.to_nat(index), U32.to_nat(other)), equal))))