- [ ] Annotate safety invariants on `KnownLayout` - [ ] https://github.com/AeneasVerif/aeneas/issues/821 - [ ] https://github.com/AeneasVerif/aeneas/issues/912 - [ ] Annotate validity invariants on `DstLayout` - [ ] https://github.com/AeneasVerif/aeneas/issues/913 - [ ] https://github.com/google/zerocopy/issues/3030
KnownLayoutisSafeannotation) AeneasVerif/aeneas#912DstLayoutisValidannotation) AeneasVerif/aeneas#913