def contract
bendtorch-core@0.1.0.0 · src/tensor/contracts/pointwise_proof.bend:470
import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise_proof.bend as PointwiseProof
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/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed
import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise.bend as Pointwise
import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise_records.bend as Records
470def contract(~O: Data, ~f: O -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~ib: P -> Nat -> Nat,
471 +operation: O, +plan: P, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
472 +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +shape: Shape.Shape,
473 +left_inside: {Pointwise.inside(~P, ~ia, plan, Shape.logical_numel(Shape.dimensions(shape)), Shape.logical_numel(Shape.dimensions(left))) == True{} : Bool},
474 +right_inside: {Pointwise.inside(~P, ~ib, plan, Shape.logical_numel(Shape.dimensions(shape)), Shape.logical_numel(Shape.dimensions(right))) == True{} : Bool},
475 -left_fits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_ops)) == Shape.logical_numel(Shape.dimensions(left)) : Nat},
476 -right_fits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_ops)) == Shape.logical_numel(Shape.dimensions(right)) : Nat}) ->
477 Records.PointwiseContract<shape, left, right,
478 index => Pointwise.cell(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, index),
479 other => Replayed.value(left, left_fill, left_ops, other), other => Replayed.value(right, right_fill, right_ops, other),
480 Pointwise.run(~O, ~f, ~P, ~ia, ~ib, operation, plan, shape,
481 Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), left_fits}},
482 Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), right_fits}})>:
483 +total = Shape.logical_numel(Shape.dimensions(shape))
484 Records.PointwiseContract{
485 run_lift(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, shape, left_inside, right_inside,
486 result => {Pointwise.succeeded(result) == True{} : Bool},
487 left_after => right_after => output_after => {==})(left_fits, right_fits),
488 run_lift(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, shape, left_inside, right_inside,
489 result => {Pointwise.output_dimensions(result) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>},
490 left_after => right_after => output_after => {==})(left_fits, right_fits),
491 index => inside =>
492 +inside = inside
493 run_lift(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, shape, left_inside, right_inside,
494 result => {Pointwise.output_point(result, index) ==
495 Some{Pointwise.cell(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(index))} : Maybe<&2, F32>},
496 left_after => right_after => output_after =>
497 +history = Pointwise.writes(~O, ~f, ~P, ~ia, ~ib, total, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops)
498 Equal.trans(Maybe<&2, F32>,
499 Core.dynamic_read_value(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Replayed.storage(shape, 0.0, history), output_after}}, index)),
500 Some{Replayed.value(shape, 0.0, history, index)},
501 Some{Pointwise.cell(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(index))},
502 replayed_point(shape, 0.0, history, output_after, index, inside),
503 Equal.cong(F32, Maybe<&2, F32>, word => Some{word}, Replayed.value(shape, 0.0, history, index),
504 Pointwise.cell(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(index)),
505 writes_value(~O, ~f, ~P, ~ia, ~ib, total, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, shape, index,
506 inside, Conversion.le_reflexive(total)))))(left_fits, right_fits),
507 other => inside =>
508 run_lift(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, shape, left_inside, right_inside,
509 result => {Pointwise.left_point(result, other) == Some{Replayed.value(left, left_fill, left_ops, other)} : Maybe<&2, F32>},
510 left_after => right_after => output_after =>
511 input_point(~P, ~ia, plan, total, left, left_fill, left_ops, left_after, other, inside))(left_fits, right_fits),
512 other => inside =>
513 run_lift(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, shape, left_inside, right_inside,
514 result => {Pointwise.right_point(result, other) == Some{Replayed.value(right, right_fill, right_ops, other)} : Maybe<&2, F32>},
515 left_after => right_after => output_after =>
516 input_point(~P, ~ib, plan, total, right, right_fill, right_ops, right_after, other, inside))(left_fits, right_fits)}