def zero_prefix

bendtorch-core@0.1.0.0 · src/tensor/matmul_PROOF.bend:614

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/matmul_LAWS.bend as Laws

614def zero_prefix(+left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor<left>, -b: Core.Tensor<right>, +output: Shape.Shape,
615  -ra: Core.Tensor<left>, -rb: Core.Tensor<right>, -out: Core.Tensor<output>, +end: Nat,
616  prefix: Laws.ProductPrefix<0, left, right, a, b, output, ra, rb, out, end>) -> Laws.ZeroPrefix<left, right, output, out, end>:
617  Laws.ProductPrefix{left_kept, right_kept, cells} = prefix
618  Laws.ZeroPrefix{position => earlier =>
619    claim : @certificate: ZeroCell<output, out, position> -> {Core.checked_observe(output, out, U32.from_nat(position)) == Some{0.0} : Maybe<&2, F32>} =
620      \{ZeroCell: observed => observed}
621    claim(zero_cell(left, right, a, b, output, out, position, cells(position, earlier)))}