Summary

This is a tracking issue for the RFC mir_linker which will enable users to use non-generic + non-inlined methods of the standard library.

During development, this feature will be gated by the unstable option --mir-linker.

Major Steps

Suggestion of major steps:

• Get feedback on the RFC PR.
• Implement compiler options --reachability=[legacy | none | harnesses]
• Create a mechanism to generate and ship Kani sysroot.
• Introduce unstable user option --mir-linker.
• Implement compiler option --reachability=pub_fns.
• Stabilization PR.

• Broken down issues will be tracked by https://github.com/model-checking/kani/milestone/12

Open Questions

• Should we build or download the sysroot during kani setup?