def looked_value

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

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/parallel_proofs.bend as Generic

278# ... and gives the input word at the entry it read.
279def looked_value(+plan: Gather.Plan, +at: Nat, +da: Nat, -A: Array<F32>, pair: Array<U32> & U32, +j: U32,
280  -seen: {Refinement.second(U32, pair) == j : U32}, -valid: Model.Balanced(F32, da, A)) ->
281  Generic.Fact<{Some{Pair.fst(F32, Array<F32> & Array<U32>, Gather.looked(plan, at, A, pair))} ==
282    Model.observe(F32, da, A, Refinement.route(da, U32.from_nat(Gather.source(plan, at, U32.to_nat(j))))) : Maybe<&2, F32>}>:
283  (index, +found) = pair
284  Generic.Fact{
285    %seen : {Some{Pair.fst(F32, Array<F32> & Array<U32>, Gather.take(index, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(found))))))} ==
286      Model.observe(F32, da, A, Refinement.route(da, U32.from_nat(Gather.source(plan, at, U32.to_nat(_))))) : Maybe<&2, F32>}
287    Equal.trans(Maybe<&2, F32>, Some{Pair.fst(F32, Array<F32> & Array<U32>, Gather.take(index, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(found))))))},
288      Some{Refinement.second(F32, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(found)))))},
289      Model.observe(F32, da, A, Refinement.route(da, U32.from_nat(Gather.source(plan, at, U32.to_nat(found))))),
290      Equal.cong(F32, Maybe<&2, F32>, x => Some{x},
291        Pair.fst(F32, Array<F32> & Array<U32>, Gather.take(index, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(found)))))),
292        Refinement.second(F32, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(found))))),
293        take_fst(index, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(found)))))),
294      Refinement.law_get_refines(F32, da, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(found))), valid))}