def read_slot

bendtorch-core@0.1.0.0 · src/tensor/gather_PROOF.bend:513

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
import bendtorch-core@0.1.0.0/src/tensor/gather.bend as Gather
import bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend as Laws

513def read_slot(+kind: Gather.Lookup, +count: Nat, +inner: Nat, +o: Nat, +k: Nat, +r: Nat, +di: Nat, -I: Array<U32>, +j: U32,
514  read: {Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(Gather.entry_of(kind, count, inner, o, k, r)))) == Some{j} : Maybe<&2, U32>}) ->
515  {Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(Laws.entry_at(kind, count, inner, o, k, r)))) == Some{j} : Maybe<&2, U32>}:
516  Equal.trans(Maybe<&2, U32>, Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(Laws.entry_at(kind, count, inner, o, k, r)))),
517    Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(Gather.entry_of(kind, count, inner, o, k, r)))), Some{j},
518    Equal.cong(Nat, Maybe<&2, U32>, e => Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(e))),
519      Laws.entry_at(kind, count, inner, o, k, r), Gather.entry_of(kind, count, inner, o, k, r),
520      Equal.sym(Nat, Gather.entry_of(kind, count, inner, o, k, r), Laws.entry_at(kind, count, inner, o, k, r), entry_same(kind, count, inner, o, k, r))),
521    read)