The identity a checkpoint context binds: with replicated parameters the
placed learner's digest; with partitioned ones the digest of its
placement-independent identity.
1972def dpoContextDigest =
1973 (lambda unrestricted c : Nat .
1974 (lambda unrestricted u : Nat .
1975 (lambda unrestricted system : (family DataParallelSystem c u) .
1976 (lambda unrestricted p : Nat .
1977 (lambda unrestricted digest : Bytes .
1978 (nat-eliminate
1979 (lambda unrestricted current : Nat . Bytes)
1980 digest
1981 (lambda unrestricted previous : Nat .
1982 (lambda unrestricted ignored : Bytes .
1983 (sha256RawDigestOrEmpty (dataParallelLearnerIdentity c u system))))
1984 p))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.