PermuteValues.chain: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/permute_values.bend as PermuteValues
Lines 90-128 of bendtorch-core@0.1.0.0/src/tensor/permute_values.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values.bend&start_line=90&end_line=128

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
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/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/index_map.bend as IndexMap
import bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend as PermuteProof
import bendtorch-core@0.1.0.0/src/tensor/contracts/build_facts.bend as Facts
import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_storage_proof.bend as Owned
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/array.bend as ArrayCore
import bendtorch-core@0.1.0.0/src/storage/api.bend as Api
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

# The copy loop's write history, replayed on the owned storage that
# `created` makes, is the owned storage that holds the output spec.
def chain(+input: Shape.Shape, +axes: List<&2, U32>, +fill: F32, +ops: List<&2, StorageLaws.Op>, +d: Nat, +n: Nat, -f: {Storage.bounds(d, n) == True{} : Bool}, +fits: {Storage.bounds(d, n) == True{} : Bool},
  +limit: U32, +n_limit: {Nat.is_le(n, U32.to_nat(limit)) == True{} : Bool},
  +k: Nat, +room: {Nat.is_le(k, n) == True{} : Bool}) ->
  {StorageLaws.replay(IndexMap.writes(~Request, ~source_of, k, Request{input, axes}, input, fill, ops), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}) == Storage.Owned{d, n, PermuteProof.spec(input, axes, fill, ops, k, d, 0n), PermuteProof.spec_balanced(input, axes, fill, ops, k, d, 0n), f} : Storage.Storage}:
  match k:
    case 0n:
      Owned.owned_eq(d, n, Array.new(F32, d, 0.0), PermuteProof.spec(input, axes, fill, ops, 0n, d, 0n), PermuteProof.new_spec(input, axes, fill, ops, d, 0n), ArrayCore.new_balanced(F32, d, 0.0), f)(
        PermuteProof.spec_balanced(input, axes, fill, ops, 0n, d, 0n))
    case 1n+j:
      +index = U32.from_nat(j)
      +value = PermuteProof.word(input, axes, fill, ops, j)
      +below_n = Conversion.le_successor_lt(j, n, room)
      +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))
      +inside = Equal.trans(Bool, Nat.is_lt(U32.to_nat(index), n), Nat.is_lt(j, n), True{},
        Equal.cong(Nat, Bool, x => Nat.is_lt(x, n), U32.to_nat(index), j, exact), below_n)
      +offset = Equal.trans(Nat, Nat.add(Model.offset(d, Refinement.route(d, index)), 0n), U32.to_nat(index), j,
        Facts.output_position(d, n, index, fits, inside), exact)
      +written = Equal.trans(Array<F32>, Array.set(F32, PermuteProof.spec(input, axes, fill, ops, j, d, 0n), index, value), ArrayCore.write_path(F32, d, PermuteProof.spec(input, axes, fill, ops, j, d, 0n), Refinement.route(d, index), value),
        PermuteProof.spec(input, axes, fill, ops, 1n+j, d, 0n), Refinement.law_set_refines(F32, d, PermuteProof.spec(input, axes, fill, ops, j, d, 0n), index, value, PermuteProof.spec_balanced(input, axes, fill, ops, j, d, 0n)),
        PermuteProof.write_spec(input, axes, fill, ops, j, d, 0n, Refinement.route(d, index), offset))
      Equal.trans(Storage.Storage, StorageLaws.replay(IndexMap.writes(~Request, ~source_of, 1n+j, Request{input, axes}, input, fill, ops), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}),
        StorageLaws.step(StorageLaws.replay(IndexMap.writes(~Request, ~source_of, j, Request{input, axes}, input, fill, ops), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), StorageLaws.Write{index, value}),
        Storage.Owned{d, n, PermuteProof.spec(input, axes, fill, ops, 1n+j, d, 0n), PermuteProof.spec_balanced(input, axes, fill, ops, 1n+j, d, 0n), f},
        FromValues.replay_snoc(IndexMap.writes(~Request, ~source_of, j, Request{input, axes}, input, fill, ops), StorageLaws.Write{index, value}, Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}),
        %Equal.sym(Storage.Storage, StorageLaws.replay(IndexMap.writes(~Request, ~source_of, j, Request{input, axes}, input, fill, ops), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), Storage.Owned{d, n, PermuteProof.spec(input, axes, fill, ops, j, d, 0n), PermuteProof.spec_balanced(input, axes, fill, ops, j, d, 0n), f},
          chain(input, axes, fill, ops, d, n, f, fits, limit, n_limit, j, Conversion.le_predecessor(j, n, room))) :
          {StorageLaws.step(_, StorageLaws.Write{index, value}) == Storage.Owned{d, n, PermuteProof.spec(input, axes, fill, ops, 1n+j, d, 0n), PermuteProof.spec_balanced(input, axes, fill, ops, 1n+j, d, 0n), f} : Storage.Storage}
        %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>,
          Storage.set_checked(d, n, PermuteProof.spec(input, axes, fill, ops, j, d, 0n), index, value, Nat.is_lt(U32.to_nat(index), n), {==}, PermuteProof.spec_balanced(input, axes, fill, ops, j, d, 0n), f),
          (Storage.Owned{d, n, Array.set(F32, PermuteProof.spec(input, axes, fill, ops, j, d, 0n), index, value),
            Certificates.set_result(F32, d, PermuteProof.spec(input, axes, fill, ops, j, d, 0n), index, value, Array.set(F32, PermuteProof.spec(input, axes, fill, ops, j, d, 0n), index, value), {==}, PermuteProof.spec_balanced(input, axes, fill, ops, j, d, 0n)), f}, Done{Unit{}}),
          Api.set_checked_hit(d, n, PermuteProof.spec(input, axes, fill, ops, j, d, 0n), index, value, Nat.is_lt(U32.to_nat(index), n), {==}, PermuteProof.spec_balanced(input, axes, fill, ops, j, d, 0n), f,
            Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), n), True{}, inside), fits, inside)) :
          {StorageLaws.owner(Result<&2, &2, Storage.Error, Unit>, _) == Storage.Owned{d, n, PermuteProof.spec(input, axes, fill, ops, 1n+j, d, 0n), PermuteProof.spec_balanced(input, axes, fill, ops, 1n+j, d, 0n), f} : Storage.Storage}
        Owned.owned_eq(d, n, Array.set(F32, PermuteProof.spec(input, axes, fill, ops, j, d, 0n), index, value), PermuteProof.spec(input, axes, fill, ops, 1n+j, d, 0n), written,
          Certificates.set_result(F32, d, PermuteProof.spec(input, axes, fill, ops, j, d, 0n), index, value, Array.set(F32, PermuteProof.spec(input, axes, fill, ops, j, d, 0n), index, value), {==}, PermuteProof.spec_balanced(input, axes, fill, ops, j, d, 0n)), f)(
          PermuteProof.spec_balanced(input, axes, fill, ops, 1n+j, d, 0n)))

Uses (52):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.new
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.set
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=Op
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=owner
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=replay
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&name=set_checked_hit
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/array.bend&name=new_balanced
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/array.bend&name=write_path
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/certificates.bend&name=set_result
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=Error
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=Storage
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=bounds
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=set_checked
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=offset
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=law_set_refines
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=route
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/binary_storage_proof.bend&name=owned_eq
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/build_facts.bend&name=le_trans
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/build_facts.bend&name=output_position
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/from_values_contract.bend&name=replay_snoc
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/index_map.bend&name=writes
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=new_spec
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=spec
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=spec_balanced
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=word
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=write_spec
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values.bend&name=Request
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values.bend&name=source_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend&name=le_predecessor
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend&name=le_successor_lt
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend&name=lt_le
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend&name=natural_word_exact