def contribution_inv
bendtorch-core@0.1.0.0 · src/autograd/gradient_PROOF.bend:394
import bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend as GradientPROOF
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_totality.bend as Totality
import bendtorch-core@0.1.0.0/src/autograd/gradient.bend as Gradient
394def contribution_inv(+shape: Shape.Shape, -original: Core.Tensor<shape>, -contribution: Core.Dynamic, +cursor: Nat, +index: U32,
395 total: Core.Tensor<shape>, -current: Core.Dynamic, pair: Core.Dynamic & Result<&2, &2, Core.Error, F32>,
396 -exact: {U32.to_nat(index) == cursor : Nat},
397 -source: {Core.dynamic_read_value(pair) == Core.checked_observe_dynamic(current, index) : Maybe<&2, F32>},
398 -same: Totality.SameSource(contribution, current),
399 -inv: Inv(shape, original, contribution, cursor, total)) ->
400 Holds<StepInv(shape, original, contribution, cursor, Gradient.step_contribution(shape, index, total, pair))>:
401 (owner, result) = pair
402 match result:
403 case Fail{error}:
404 Holds{Unit{}}
405 case Done{+value}:
406 total_inv(shape, original, contribution, cursor, total, index, value, owner, Core.read_flat(shape, total, index), exact,
407 {\{Core.SourceRead: meaning => meaning} : Core.SourceRead<shape, total, index> ->
408 {Core.read_value(shape, Core.read_flat(shape, total, index)) == Core.checked_observe(shape, total, index) : Maybe<&2, F32>}}(
409 Core.source_read_model(shape, total, index)),
410 {\{Core.SourceReadKeeps: kept => kept} : Core.SourceReadKeeps<shape, total, index> ->
411 @+position: U32 -> {Core.retained_read_observe(shape, Core.read_flat(shape, total, index), position) == Core.checked_observe(shape, total, position) : Maybe<&2, F32>}}(
412 Core.source_read_keeps(shape, total, index)),
413 inv,
414 Equal.trans(Maybe<&2, F32>, Core.checked_observe_dynamic(contribution, index), Core.checked_observe_dynamic(current, index), Some{value},
415 Equal.sym(Maybe<&2, F32>, Core.checked_observe_dynamic(current, index), Core.checked_observe_dynamic(contribution, index),
416 {\{Holds: proof => proof} : Holds<{Core.checked_observe_dynamic(current, index) == Core.checked_observe_dynamic(contribution, index) : Maybe<&2, F32>}> ->
417 {Core.checked_observe_dynamic(current, index) == Core.checked_observe_dynamic(contribution, index) : Maybe<&2, F32>}}(
418 same_checked(contribution, current, same, index))),
419 Equal.sym(Maybe<&2, F32>, Some{value}, Core.checked_observe_dynamic(current, index), source)))