def copy_checked_mapping

bendtorch-core@0.1.0.0 · src/tensor/transform_PROOF.bend:162

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/transforms.bend as Transforms
import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws

162def copy_checked_mapping(-input: Shape.Shape, -axes: List<&2, U32>, +plan: Layout.Plan<input, axes>,
163  +depth: Nat, +length: Nat, array: Array<F32>, +index: U32, source: Core.Tensor<input>, +value: F32,
164  balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool},
165  -exact: {length == Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))) : Nat}, allowed: Bool,
166  -decision: {allowed == Nat.is_lt(U32.to_nat(index), length) : Bool},
167  -same: {Storage.set_checked(depth, length, array, index, value, allowed, decision, balanced, valid) ==
168    Storage.set(Storage.Owned{depth, length, array, balanced, valid}, index, value) : Storage.Storage & Result<&2, &2, Storage.Error, Unit>},
169  accepted: {allowed == True{} : Bool}) ->
170  {Transforms.copy_observe(input, axes, plan,
171    Transforms.copy_written(input, axes, plan, source => target => (source, Done{target}), source,
172      Core.write_result(Layout.output(input, axes, plan), Storage.Owned{depth, length, array, balanced, valid}, exact, index, value,
173        Storage.set_checked(depth, length, array, index, value, allowed, decision, balanced, valid), same)), index) == Some{value} : Maybe<&2, F32>}:
174  match allowed:
175    case False{}:
176      Empty.absurd({Transforms.copy_observe(input, axes, plan,
177        Transforms.copy_written(input, axes, plan, source => target => (source, Done{target}), source,
178          Core.write_result(Layout.output(input, axes, plan), Storage.Owned{depth, length, array, balanced, valid}, exact, index, value,
179            Storage.set_checked(depth, length, array, index, value, False{}, decision, balanced, valid), same)), index) == Some{value} : Maybe<&2, F32>},
180        Lifecycle.false_true(Equal.sym(Bool, False{}, True{}, accepted)))
181    case True{}:
182      StorageLaws.primitive_write_read(F32, depth, array, index, value, balanced)