def loop_success

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

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/tensor/transform_PROOF.bend as TransformProof
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
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

699def loop_success(fuel: Nat, +shape: Shape.Shape, +cursor: Nat, state: Gradient.State<shape>,
700  -fits: {Totality.dimensions(state_contribution(shape, state)) == Shape.dimensions(shape) : List<&2, U32>},
701  -within: {Nat.is_le(Nat.add(fuel, cursor), Shape.elements(shape)) == True{} : Bool}) ->
702  Holds<{Laws.accumulated(Gradient.loop(fuel, shape, cursor, state)) == True{} : Bool}>:
703  match fuel:
704    case 0n:
705      Gradient.State{owner, total} = state
706      Holds{{==}}
707    case 1n+remaining:
708      decided_success(remaining, shape, cursor, U32.from_nat(cursor), state,
709        Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)),
710        TransformProof.cursor_word_exact(shape, cursor,
711          Conversion.lt_le(cursor, Shape.elements(shape),
712            Arith.lt_le_trans(cursor, 1n+Nat.add(remaining, cursor), Shape.elements(shape),
713              Arith.lt_succ(cursor, Nat.add(remaining, cursor), TransformProof.add_cursor_le(remaining, cursor)), within))),
714        fits,
715        Arith.lt_le_trans(cursor, 1n+Nat.add(remaining, cursor), Shape.elements(shape),
716          Arith.lt_succ(cursor, Nat.add(remaining, cursor), TransformProof.add_cursor_le(remaining, cursor)), within),
717        state => fits => loop_success(remaining, shape, 1n+cursor, state, fits,
718          %Equal.sym(Nat, Nat.add(remaining, 1n+cursor), 1n+Nat.add(remaining, cursor), Arith.add_succ(remaining, cursor)) :
719            {Nat.is_le(_, Shape.elements(shape)) == True{} : Bool}
720          within))