def chain

bendtorch-core@0.1.0.0 · src/tensor/contracts/matmul_parallel_proof.bend:361

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
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/LAWS.bend as StorageLaws
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
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/contracts/binary_storage_proof.bend as Owned
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/certificates.bend as Certificates

361# The family history, replayed on the owned storage that `created` makes,
362# is the owned storage that holds the output spec.
363def chain(+span: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +d: Nat, +n: Nat, -f: {Storage.bounds(d, n) == True{} : Bool}, +fits: {Storage.bounds(d, n) == True{} : Bool},
364  +limit: U32, +n_limit: {Nat.is_le(n, U32.to_nat(limit)) == True{} : Bool},
365  +k: Nat, +room: {Nat.is_le(k, n) == True{} : Bool}) ->
366  {StorageLaws.replay(writes(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}) == Storage.Owned{d, n, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k, d, 0n), out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, k, d, 0n), f} : Storage.Storage}:
367  match k:
368    case 0n:
369      Owned.owned_eq(d, n, Array.new(F32, d, 0.0), out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 0n, d, 0n), new_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, d, 0n), ArrayCore.new_balanced(F32, d, 0.0), f)(
370        out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 0n, d, 0n))
371    case 1n+j:
372      +index = U32.from_nat(j)
373      +value = cell_word(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j)
374      +below_n = Conversion.le_successor_lt(j, n, room)
375      +exact = Conversion.natural_word_exact(j, limit, le_trans(j, n, U32.to_nat(limit), Conversion.lt_le(j, n, below_n), n_limit))
376      +inside = Equal.trans(Bool, Nat.is_lt(U32.to_nat(index), n), Nat.is_lt(j, n), True{},
377        Equal.cong(Nat, Bool, x => Nat.is_lt(x, n), U32.to_nat(index), j, exact), below_n)
378      +offset = Equal.trans(Nat, Nat.add(Model.offset(d, Refinement.route(d, index)), 0n), U32.to_nat(index), j,
379        output_position(d, n, index, fits, inside), exact)
380      +written = Equal.trans(Array<F32>, Array.set(F32, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value), ArrayCore.write_path(F32, d, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), Refinement.route(d, index), value),
381        out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), Refinement.law_set_refines(F32, d, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value, out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n)),
382        write_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n, Refinement.route(d, index), offset))
383      Equal.trans(Storage.Storage, StorageLaws.replay(writes(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}),
384        StorageLaws.step(StorageLaws.replay(writes(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), StorageLaws.Write{index, value}),
385        Storage.Owned{d, n, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), f},
386        FromValues.replay_snoc(writes(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j), StorageLaws.Write{index, value}, Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}),
387        %Equal.sym(Storage.Storage, StorageLaws.replay(writes(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), Storage.Owned{d, n, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), f},
388          chain(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, d, n, f, fits, limit, n_limit, j, Conversion.le_predecessor(j, n, room))) :
389          {StorageLaws.step(_, StorageLaws.Write{index, value}) == Storage.Owned{d, n, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), f} : Storage.Storage}
390        %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>,
391          Storage.set_checked(d, n, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value, Nat.is_lt(U32.to_nat(index), n), {==}, out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), f),
392          (Storage.Owned{d, n, Array.set(F32, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value),
393            Certificates.set_result(F32, d, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value, Array.set(F32, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value), {==}, out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n)), f}, Done{Unit{}}),
394          Api.set_checked_hit(d, n, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value, Nat.is_lt(U32.to_nat(index), n), {==}, out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), f,
395            Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), n), True{}, inside), fits, inside)) :
396          {StorageLaws.owner(Result<&2, &2, Storage.Error, Unit>, _) == Storage.Owned{d, n, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), f} : Storage.Storage}
397        Owned.owned_eq(d, n, Array.set(F32, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value), out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n), written,
398          Certificates.set_result(F32, d, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value, Array.set(F32, out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n), index, value), {==}, out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, j, d, 0n)), f)(
399          out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, 1n+j, d, 0n)))