def continue_success

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

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/elementwise_totality.bend as Totality
import bendtorch-core@0.1.0.0/src/autograd/gradient.bend as Gradient
import bendtorch-core@0.1.0.0/src/autograd/gradient_LAWS.bend as Laws

654def continue_success(+remaining: Nat, +shape: Shape.Shape, +cursor: Nat, result: Gradient.Step<shape>,
655  -continued: {step_continued(shape, result) == True{} : Bool},
656  -fits: {Totality.dimensions(step_owner(shape, result)) == Shape.dimensions(shape) : List<&2, U32>},
657  -rec: @state: Gradient.State<shape> -> @-fits: {Totality.dimensions(state_contribution(shape, state)) == Shape.dimensions(shape) : List<&2, U32>} ->
658    Holds<{Laws.accumulated(Gradient.loop(remaining, shape, 1n+cursor, state)) == True{} : Bool}>) ->
659  Holds<{Laws.accumulated(Gradient.continue_step(shape, state => Gradient.loop(remaining, shape, 1n+cursor, state), result)) == True{} : Bool}>:
660  match result:
661    case Gradient.Stop{owner, total, error}:
662      Holds{Empty.absurd({False{} == True{} : Bool}, Arith.clash(continued))}
663    case Gradient.Continue{state}:
664      Holds{{\{Holds: proof => proof} : Holds<{Laws.accumulated(Gradient.loop(remaining, shape, 1n+cursor, state)) == True{} : Bool}> ->
665        {Laws.accumulated(Gradient.loop(remaining, shape, 1n+cursor, state)) == True{} : Bool}}(rec(state, fits))}