-2) Soundness: Enzyme currently does assume that the user passes shadow arguments (`dx`, `dy`, ...) of appropriate size. That's a current research project of Manuel, so we hope to check at least basic DST (vectors, enums) till end of November. If we remember the backprop function from above, there is no way for the type system to guarantee that `dweights` is at least as large as the `weights` vector. Adding length checks for vectors and making sure that in case of enums primal and shadow are of the same variant should get us a large step towards soundness. Once implemented, we can still evaluate how many more checks we can insert automatically and where we want to fall back to unsafe. We also consider to allow the user to (unsafely) implement a safety check for his own types which we would then insert. Concretely, here we would add the following check at the top of backprop (above the code generated by enzyme) `assert!(dweights.len() >= weights.len())`
0 commit comments