def chain

bendtorch-core@0.1.0.0 · src/autograd/reduce_replayed_proof.bend:378

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/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
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

378# The family history, replayed on the owned storage that `created` makes,
379# is the owned storage that holds the output spec.
380def chain(+plan: Shape.BroadcastPlan, +map: PlanMap(plan), +shape: Shape.Shape, +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},
381  +limit: U32, +n_limit: {Nat.is_le(n, U32.to_nat(limit)) == True{} : Bool},
382  +k: Nat, +room: {Nat.is_le(k, n) == True{} : Bool}) ->
383  {StorageLaws.replay(writes(plan, map, shape, fill, 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(plan, map, shape, fill, ops, k, d, 0n), out_balanced(plan, map, shape, fill, ops, k, d, 0n), f} : Storage.Storage}:
384  match k:
385    case 0n:
386      Owned.owned_eq(d, n, Array.new(F32, d, 0.0), out_spec(plan, map, shape, fill, ops, 0n, d, 0n), new_spec(plan, map, shape, fill, ops, d, 0n), ArrayCore.new_balanced(F32, d, 0.0), f)(
387        out_balanced(plan, map, shape, fill, ops, 0n, d, 0n))
388    case 1n+j:
389      +index = U32.from_nat(j)
390      +value = cell_word(plan, map, shape, fill, ops, j)
391      +below_n = Conversion.le_successor_lt(j, n, room)
392      +exact = Conversion.natural_word_exact(j, limit, le_trans(j, n, U32.to_nat(limit), Conversion.lt_le(j, n, below_n), n_limit))
393      +inside = Equal.trans(Bool, Nat.is_lt(U32.to_nat(index), n), Nat.is_lt(j, n), True{},
394        Equal.cong(Nat, Bool, x => Nat.is_lt(x, n), U32.to_nat(index), j, exact), below_n)
395      +offset = Equal.trans(Nat, Nat.add(Model.offset(d, Refinement.route(d, index)), 0n), U32.to_nat(index), j,
396        output_position(d, n, index, fits, inside), exact)
397      +written = Equal.trans(Array<F32>, Array.set(F32, out_spec(plan, map, shape, fill, ops, j, d, 0n), index, value), ArrayCore.write_path(F32, d, out_spec(plan, map, shape, fill, ops, j, d, 0n), Refinement.route(d, index), value),
398        out_spec(plan, map, shape, fill, ops, 1n+j, d, 0n), Refinement.law_set_refines(F32, d, out_spec(plan, map, shape, fill, ops, j, d, 0n), index, value, out_balanced(plan, map, shape, fill, ops, j, d, 0n)),
399        write_spec(plan, map, shape, fill, ops, j, d, 0n, Refinement.route(d, index), offset))
400      Equal.trans(Storage.Storage, StorageLaws.replay(writes(plan, map, shape, fill, ops, 1n+j), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}),
401        StorageLaws.step(StorageLaws.replay(writes(plan, map, shape, fill, ops, j), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), StorageLaws.Write{index, value}),
402        Storage.Owned{d, n, out_spec(plan, map, shape, fill, ops, 1n+j, d, 0n), out_balanced(plan, map, shape, fill, ops, 1n+j, d, 0n), f},
403        FromValues.replay_snoc(writes(plan, map, shape, fill, ops, j), StorageLaws.Write{index, value}, Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}),
404        %Equal.sym(Storage.Storage, StorageLaws.replay(writes(plan, map, shape, fill, 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(plan, map, shape, fill, ops, j, d, 0n), out_balanced(plan, map, shape, fill, ops, j, d, 0n), f},
405          chain(plan, map, shape, fill, ops, d, n, f, fits, limit, n_limit, j, Conversion.le_predecessor(j, n, room))) :
406          {StorageLaws.step(_, StorageLaws.Write{index, value}) == Storage.Owned{d, n, out_spec(plan, map, shape, fill, ops, 1n+j, d, 0n), out_balanced(plan, map, shape, fill, ops, 1n+j, d, 0n), f} : Storage.Storage}
407        %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>,
408          Storage.set_checked(d, n, out_spec(plan, map, shape, fill, ops, j, d, 0n), index, value, Nat.is_lt(U32.to_nat(index), n), {==}, out_balanced(plan, map, shape, fill, ops, j, d, 0n), f),
409          (Storage.Owned{d, n, Array.set(F32, out_spec(plan, map, shape, fill, ops, j, d, 0n), index, value),
410            Certificates.set_result(F32, d, out_spec(plan, map, shape, fill, ops, j, d, 0n), index, value, Array.set(F32, out_spec(plan, map, shape, fill, ops, j, d, 0n), index, value), {==}, out_balanced(plan, map, shape, fill, ops, j, d, 0n)), f}, Done{Unit{}}),
411          Api.set_checked_hit(d, n, out_spec(plan, map, shape, fill, ops, j, d, 0n), index, value, Nat.is_lt(U32.to_nat(index), n), {==}, out_balanced(plan, map, shape, fill, ops, j, d, 0n), f,
412            Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), n), True{}, inside), fits, inside)) :
413          {StorageLaws.owner(Result<&2, &2, Storage.Error, Unit>, _) == Storage.Owned{d, n, out_spec(plan, map, shape, fill, ops, 1n+j, d, 0n), out_balanced(plan, map, shape, fill, ops, 1n+j, d, 0n), f} : Storage.Storage}
414        Owned.owned_eq(d, n, Array.set(F32, out_spec(plan, map, shape, fill, ops, j, d, 0n), index, value), out_spec(plan, map, shape, fill, ops, 1n+j, d, 0n), written,
415          Certificates.set_result(F32, d, out_spec(plan, map, shape, fill, ops, j, d, 0n), index, value, Array.set(F32, out_spec(plan, map, shape, fill, ops, j, d, 0n), index, value), {==}, out_balanced(plan, map, shape, fill, ops, j, d, 0n)), f)(
416          out_balanced(plan, map, shape, fill, ops, 1n+j, d, 0n)))