def loop_inv

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

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
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

479def loop_inv(fuel: Nat, +shape: Shape.Shape, -original: Core.Tensor<shape>, -contribution: Core.Dynamic, +cursor: Nat, state: Gradient.State<shape>,
480  -inv: Inv(shape, original, contribution, cursor, state_total(shape, state)),
481  -same: Totality.SameSource(contribution, state_contribution(shape, state))) ->
482  Holds<LoopInv(shape, original, contribution, Nat.add(fuel, cursor), Gradient.loop(fuel, shape, cursor, state))>:
483  match fuel:
484    case 0n:
485      Gradient.State{owner, total} = state
486      Holds{({==}, inv)}
487    case 1n+remaining:
488      Holds{
489        %Arith.add_succ(remaining, cursor) : LoopInv(shape, original, contribution, _, Gradient.loop(1n+remaining, shape, cursor, state))
490        {\{Holds: proof => proof} :
491          Holds<LoopInv(shape, original, contribution, Nat.add(remaining, 1n+cursor), Gradient.loop(1n+remaining, shape, cursor, state))> ->
492          LoopInv(shape, original, contribution, Nat.add(remaining, 1n+cursor), Gradient.loop(1n+remaining, shape, cursor, state))}(
493          decided_inv(remaining, shape, original, contribution, cursor, U32.from_nat(cursor), state,
494            Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)), inv, same,
495            state => inv => same => loop_inv(remaining, shape, original, contribution, 1n+cursor, state, inv, same)))}