def chain

bendtorch-core@0.1.0.0 · src/tensor/contracts/binary_proofs.bend:156

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
import bendtorch-core@0.1.0.0/src/storage/array.bend as ArrayCore
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
import bendtorch-core@0.1.0.0/src/storage/certificates.bend as Certificates
import bendtorch-core@0.1.0.0/src/storage/api.bend as Api
import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
import bendtorch-core@0.1.0.0/src/tensor/from_values_contract.bend as FromValues
import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise.bend as Pointwise
import bendtorch-core@0.1.0.0/src/tensor/contracts/broadcast.bend as Broadcast
import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_storage_proof.bend as Owned
import bendtorch-core@0.1.0.0/src/tensor/contracts/build_facts.bend as Facts

156# The family history, replayed on the owned storage that `created` makes,
157# is the owned storage that holds the output spec.
158def chain(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +d: Nat, +n: Nat, -f: {Storage.bounds(d, n) == True{} : Bool}, +fits: {Storage.bounds(d, n) == True{} : Bool},
159  +limit: U32, +n_limit: {Nat.is_le(n, U32.to_nat(limit)) == True{} : Bool},
160  +k: Nat, +room: {Nat.is_le(k, n) == True{} : Bool}) ->
161  {StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, k, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}) == Storage.Owned{d, n, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, d, 0n), out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, d, 0n), f} : Storage.Storage}:
162  match k:
163    case 0n:
164      Owned.owned_eq(d, n, Array.new(F32, d, 0.0), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 0n, d, 0n), new_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, d, 0n), ArrayCore.new_balanced(F32, d, 0.0), f)(
165        out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 0n, d, 0n))
166    case 1n+j:
167      +index = U32.from_nat(j)
168      +value = cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j)
169      +below_n = Conversion.le_successor_lt(j, n, room)
170      +exact = Conversion.natural_word_exact(j, limit, Facts.le_trans(j, n, U32.to_nat(limit), Conversion.lt_le(j, n, below_n), n_limit))
171      +inside = Equal.trans(Bool, Nat.is_lt(U32.to_nat(index), n), Nat.is_lt(j, n), True{},
172        Equal.cong(Nat, Bool, x => Nat.is_lt(x, n), U32.to_nat(index), j, exact), below_n)
173      +offset = Equal.trans(Nat, Nat.add(Model.offset(d, Refinement.route(d, index)), 0n), U32.to_nat(index), j,
174        Facts.output_position(d, n, index, fits, inside), exact)
175      +written = Equal.trans(Array<F32>, Array.set(F32, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value), ArrayCore.write_path(F32, d, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), Refinement.route(d, index), value),
176        out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), Refinement.law_set_refines(F32, d, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value, out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n)),
177        write_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n, Refinement.route(d, index), offset))
178      Equal.trans(Storage.Storage, StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, 1n+j, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}),
179        StorageLaws.step(StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, j, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), StorageLaws.Write{index, value}),
180        Storage.Owned{d, n, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), f},
181        FromValues.replay_snoc(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, j, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), StorageLaws.Write{index, value}, Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}),
182        %Equal.sym(Storage.Storage, StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, j, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), Storage.Owned{d, n, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), f},
183          chain(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, d, n, f, fits, limit, n_limit, j, Conversion.le_predecessor(j, n, room))) :
184          {StorageLaws.step(_, StorageLaws.Write{index, value}) == Storage.Owned{d, n, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), f} : Storage.Storage}
185        %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>,
186          Storage.set_checked(d, n, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value, Nat.is_lt(U32.to_nat(index), n), {==}, out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), f),
187          (Storage.Owned{d, n, Array.set(F32, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value),
188            Certificates.set_result(F32, d, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value, Array.set(F32, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value), {==}, out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n)), f}, Done{Unit{}}),
189          Api.set_checked_hit(d, n, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value, Nat.is_lt(U32.to_nat(index), n), {==}, out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), f,
190            Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), n), True{}, inside), fits, inside)) :
191          {StorageLaws.owner(Result<&2, &2, Storage.Error, Unit>, _) == Storage.Owned{d, n, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), f} : Storage.Storage}
192        Owned.owned_eq(d, n, Array.set(F32, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), written,
193          Certificates.set_result(F32, d, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value, Array.set(F32, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value), {==}, out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n)), f)(
194          out_balanced(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n)))