def leaf_same

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

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
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/contracts/broadcast.bend as Broadcast
import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_build_proof.bend as Build
import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_storage_proof.bend as Owned

233# The build's leaf reads the replayed words the family cell names.
234def leaf_same(+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>, +dl: Nat, +dr: Nat, +position: Nat, inside: Bool) ->
235  {Build.leaf(operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill, U32.to_nat(Shape.count(left)), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill, U32.to_nat(Shape.count(right)), position, inside) == out_leaf(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, position, inside) : F32}:
236  match inside:
237    case False{}:
238      {==}
239    case True{}:
240      +li = Build.left_index(plan, position)
241      +ri = Build.right_index(plan, position)
242      +bli = U32.from_nat(Broadcast.left_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position))
243      +bri = U32.from_nat(Broadcast.right_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position))
244      Equal.trans(F32, Build.word(operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill, U32.to_nat(Shape.count(left)), Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill, U32.to_nat(Shape.count(right)), position),
245        Elementwise.scalar(operation, StorageLaws.expected(left_ops, U32.to_nat(Shape.count(left)), li, left_fill), StorageLaws.expected(right_ops, U32.to_nat(Shape.count(right)), ri, right_fill)),
246        cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, position),
247        scalar_cong(operation, Api.current(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), li, left_fill), StorageLaws.expected(left_ops, U32.to_nat(Shape.count(left)), li, left_fill),
248          Api.current(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), ri, right_fill), StorageLaws.expected(right_ops, U32.to_nat(Shape.count(right)), ri, right_fill),
249          Owned.norm_current(U32.to_nat(Shape.count(left)), left_ops, Nil{}, li, left_fill, Api.hit_of(U32.to_nat(Shape.count(left)), left_ops), {==}),
250          Owned.norm_current(U32.to_nat(Shape.count(right)), right_ops, Nil{}, ri, right_fill, Api.hit_of(U32.to_nat(Shape.count(right)), right_ops), {==})),
251        scalar_cong(operation, StorageLaws.expected(left_ops, U32.to_nat(Shape.count(left)), li, left_fill), StorageLaws.expected(left_ops, U32.to_nat(Shape.count(left)), bli, left_fill),
252          StorageLaws.expected(right_ops, U32.to_nat(Shape.count(right)), ri, right_fill), StorageLaws.expected(right_ops, U32.to_nat(Shape.count(right)), bri, right_fill),
253          Equal.cong(Nat, F32, w => StorageLaws.expected(left_ops, U32.to_nat(Shape.count(left)), U32.from_nat(w), left_fill),
254            Elementwise.left_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position), Broadcast.left_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position), Build.walk_left_same(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position)),
255          Equal.cong(Nat, F32, w => StorageLaws.expected(right_ops, U32.to_nat(Shape.count(right)), U32.from_nat(w), right_fill),
256            Elementwise.right_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position), Broadcast.right_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position), Build.walk_right_same(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position))))