type Certified

bendtorch-core@0.1.0.0 · src/tensor/parallel.bend:86

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model

86# A run of the one-thread tree next to its proof of balance: `result` is
87# the term the code computes, and its first component is balanced at
88# `depth`. The proofs only follow the code, so they cost nothing at runtime.
89type Certified<-S: Type, -depth: Nat, -expected: Array<F32> & S> is Type:
90  Certified{result: Array<F32> & S, same: {result == expected : Array<F32> & S},
91    balanced: Model.Balanced(F32, depth, Pair.fst(Array<F32>, S, result))}