def output_word

bendtorch-core@0.1.0.0 · src/tensor/permute_build_proof.bend:396

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/observation.bend as Values
import bendtorch-core@0.1.0.0/src/tensor/permute_build.bend as Build
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/refinement.bend as Refinement
import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
import bendtorch-core@0.1.0.0/src/tensor/contracts/build_facts.bend as Facts

396# What the parallel build holds at output index `other`.
397def output_word(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +d: Nat, +n: Nat,
398  +valid: {Storage.bounds(d, n) == True{} : Bool}, +exact: {n == Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))) : Nat},
399  +ds: Nat, -c: Array<F32>, -bc: Model.Balanced(F32, ds, c), +other: Nat, +earlier: {Nat.is_lt(other, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan)))) == True{} : Bool}) ->
400  Fact<{Lifecycle.checked_observe_array(d, n, Build.build(d, Build.Request{input, axes}, n, c), U32.from_nat(other)) ==
401    Some{Refinement.second(F32, Array.get(F32, c, U32.from_nat(Values.permute_source_index(input, axes, other))))} : Maybe<&2, F32>}>:
402  +index = U32.from_nat(other)
403  +inside = length_below(Layout.output(input, axes, plan), n, exact, other, earlier)
404  +at = Equal.trans(Nat, Nat.add(Model.offset(d, Refinement.route(d, index)), 0n), U32.to_nat(index), other,
405    Facts.output_position(d, n, index, valid, inside), word_below(Layout.output(input, axes, plan), other, earlier))
406  +below : {Nat.is_lt(other, n) == True{} : Bool} = %Equal.sym(Nat, n, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))), exact) : {Nat.is_lt(other, _) == True{} : Bool}
407    earlier
408  -built = Build.build(d, Build.Request{input, axes}, n, c)
409  -recipe = Build.recipe(Build.Request{input, axes})
410  Fact{Equal.trans(Maybe<&2, F32>, Lifecycle.checked_observe_array(d, n, built, index), Model.observe(F32, d, built, Refinement.route(d, index)),
411    Some{Refinement.second(F32, Array.get(F32, c, U32.from_nat(Values.permute_source_index(input, axes, other))))},
412    owned_observe(d, n, built, index, valid, inside),
413    Equal.trans(Maybe<&2, F32>, Model.observe(F32, d, built, Refinement.route(d, index)),
414      Some{Pair.fst(F32, Array<F32> & Array<F32>, Build.cell(recipe, Nat.add(Model.offset(d, Refinement.route(d, index)), 0n), (c, Array.new(F32, 0n, 0.0)),
415        Nat.is_lt(Nat.add(Model.offset(d, Refinement.route(d, index)), 0n), n)))},
416      Some{Refinement.second(F32, Array.get(F32, c, U32.from_nat(Values.permute_source_index(input, axes, other))))},
417      {\{Fact: q => q} : Fact<{Model.observe(F32, d, built, Refinement.route(d, index)) ==
418        Some{Pair.fst(F32, Array<F32> & Array<F32>, Build.cell(recipe, Nat.add(Model.offset(d, Refinement.route(d, index)), 0n), (c, Array.new(F32, 0n, 0.0)),
419          Nat.is_lt(Nat.add(Model.offset(d, Refinement.route(d, index)), 0n), n)))} : Maybe<&2, F32>}> ->
420        {Model.observe(F32, d, built, Refinement.route(d, index)) ==
421          Some{Pair.fst(F32, Array<F32> & Array<F32>, Build.cell(recipe, Nat.add(Model.offset(d, Refinement.route(d, index)), 0n), (c, Array.new(F32, 0n, 0.0)),
422            Nat.is_lt(Nat.add(Model.offset(d, Refinement.route(d, index)), 0n), n)))} : Maybe<&2, F32>}}(
423        build_cell(d, input, axes, n, ds, c, Refinement.route(d, index), bc)),
424      %Equal.sym(Nat, Nat.add(Model.offset(d, Refinement.route(d, index)), 0n), other, at) : {Some{Pair.fst(F32, Array<F32> & Array<F32>, Build.cell(recipe, _, (c, Array.new(F32, 0n, 0.0)), Nat.is_lt(_, n)))} == Some{Refinement.second(F32, Array.get(F32, c, U32.from_nat(Values.permute_source_index(input, axes, other))))} : Maybe<&2, F32>}
425      %Equal.sym(Bool, Nat.is_lt(other, n), True{}, below) :
426        {Some{Pair.fst(F32, Array<F32> & Array<F32>, Build.cell(recipe, other, (c, Array.new(F32, 0n, 0.0)), _))} == Some{Refinement.second(F32, Array.get(F32, c, U32.from_nat(Values.permute_source_index(input, axes, other))))} : Maybe<&2, F32>}
427      Equal.cong(F32, Maybe<&2, F32>, word => Some{word}, Pair.fst(F32, Array<F32> & Array<F32>, Build.cell(recipe, other, (c, Array.new(F32, 0n, 0.0)), True{})),
428        Refinement.second(F32, Array.get(F32, c, U32.from_nat(Values.permute_source_index(input, axes, other)))),
429        {\{Fact: q => q} : Fact<{Pair.fst(F32, Array<F32> & Array<F32>, Build.cell(recipe, other, (c, Array.new(F32, 0n, 0.0)), True{})) == Refinement.second(F32, Array.get(F32, c, U32.from_nat(Values.permute_source_index(input, axes, other)))) : F32}> ->
430          {Pair.fst(F32, Array<F32> & Array<F32>, Build.cell(recipe, other, (c, Array.new(F32, 0n, 0.0)), True{})) == Refinement.second(F32, Array.get(F32, c, U32.from_nat(Values.permute_source_index(input, axes, other)))) : F32}}(
431          cell_word(input, axes, c, other)))))}