def invariant_advance

bendtorch-core@0.1.0.0 · src/tensor/core_PROOF.bend:893

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.bend as Elementwise

893def invariant_advance(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, -original_left: Core.Dynamic, -original_right: Core.Dynamic,
894  +cursor: Nat, +index: U32, -converted: {U32.to_nat(index) == cursor : Nat},
895  before: Elementwise.State<Shape.output_shape(plan)>, after: Elementwise.State<Shape.output_shape(plan)>,
896  -invariant: Elementwise.StateInvariant(operation, plan, original_left, original_right, cursor, before),
897  -meaning: Elementwise.StepMeaning(operation, plan, index, before, Elementwise.Continue{after})) ->
898  Elementwise.InvariantModel<operation, plan, original_left, original_right, 1n+cursor, after>:
899  Elementwise.State{left, right, output} = before
900  Elementwise.State{after_left, after_right, after_output} = after
901  Elementwise.InvariantModel{(other => Equal.trans(Maybe<&2, F32>, Core.checked_observe_dynamic(after_left, other), Core.checked_observe_dynamic(left, other), Core.checked_observe_dynamic(original_left, other),
902      step_same_left(operation, plan, index, left, right, output, after_left, after_right, after_output, meaning)(other),
903      invariant_left(operation, plan, original_left, original_right, cursor, left, right, output, invariant)(other)),
904    (other => Equal.trans(Maybe<&2, F32>, Core.checked_observe_dynamic(after_right, other), Core.checked_observe_dynamic(right, other), Core.checked_observe_dynamic(original_right, other),
905      step_same_right(operation, plan, index, left, right, output, after_left, after_right, after_output, meaning)(other),
906      invariant_right(operation, plan, original_left, original_right, cursor, left, right, output, invariant)(other)),
907      {\{PrefixModel: prefix => prefix} : PrefixModel<operation, plan, original_left, original_right, 1n+cursor, after_output> ->
908        Elementwise.PrefixInvariant(operation, plan, original_left, original_right, 1n+cursor, Core.Packed{Shape.output_shape(plan), after_output})}(prefix_extend(operation, plan, original_left, original_right, cursor, index, output, after_output, converted,
909          invariant_prefix(operation, plan, original_left, original_right, cursor, left, right, output, invariant),
910          step_checked(operation, plan, index, left, right, output, after_left, after_right, after_output, meaning),
911          Equal.trans(Maybe<&2, F32>, Core.observe(Shape.output_shape(plan), after_output, index), Elementwise.expected(operation, plan, left, right, index),
912            Elementwise.expected(operation, plan, original_left, original_right, index),
913            step_observed(operation, plan, index, left, right, output, after_left, after_right, after_output, meaning),
914            {\{ExpectedSame: equal => equal} : ExpectedSame<operation, plan, index, original_left, original_right, left, right> ->
915              {Elementwise.expected(operation, plan, left, right, index) == Elementwise.expected(operation, plan, original_left, original_right, index) : Maybe<&2, F32>}}(expected_same(operation, plan, index, original_left, original_right, left, right,
916                invariant_left(operation, plan, original_left, original_right, cursor, left, right, output, invariant),
917                invariant_right(operation, plan, original_left, original_right, cursor, left, right, output, invariant)))),
918          step_frame(operation, plan, index, left, right, output, after_left, after_right, after_output, meaning)))))}