def total_inv

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

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/core_PROOF.bend as CoreProof
import bendtorch-core@0.1.0.0/src/autograd/gradient.bend as Gradient

371def total_inv(+shape: Shape.Shape, -original: Core.Tensor<shape>, -contribution: Core.Dynamic, +cursor: Nat,
372  -before: Core.Tensor<shape>, +index: U32, +value: F32, owner: Core.Dynamic,
373  pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>,
374  -exact: {U32.to_nat(index) == cursor : Nat},
375  -source: {Core.read_value(shape, pair) == Core.checked_observe(shape, before, index) : Maybe<&2, F32>},
376  -keeps: @+position: U32 -> {Core.retained_read_observe(shape, pair, position) == Core.checked_observe(shape, before, position) : Maybe<&2, F32>},
377  -inv: Inv(shape, original, contribution, cursor, before),
378  -word: {Core.checked_observe_dynamic(contribution, index) == Some{value} : Maybe<&2, F32>}) ->
379  Holds<StepInv(shape, original, contribution, cursor, Gradient.step_total(shape, index, owner, value, pair))>:
380  (read_owner, result) = pair
381  match result:
382    case Fail{error}:
383      Holds{Unit{}}
384    case Done{+accumulated}:
385      write_inv(shape, original, contribution, cursor, before, read_owner, index, accumulated, value, owner,
386        Core.write_flat(shape, read_owner, index, F32.add(accumulated, value)), exact,
387        {\{Core.CheckedUpdateModel: meaning => meaning} :
388          Core.CheckedUpdateModel<shape, read_owner, index, F32.add(accumulated, value)> ->
389          Core.CheckedUpdateMeaning(shape, read_owner, index, F32.add(accumulated, value),
390            Core.write_flat(shape, read_owner, index, F32.add(accumulated, value)))}(
391          CoreProof.checked_update_model(shape, read_owner, index, F32.add(accumulated, value))),
392        inv, Equal.sym(Maybe<&2, F32>, Some{accumulated}, Core.checked_observe(shape, before, index), source), keeps, word)