Hide `proof fn`s in doc

[rikosellic]

@Marsman1996 @hiroki-chen @SNoAnd Our doc currently renders all public functions. But many of the proof functions are undocumented and extremely hard for readers without a Verus background. Shall we hide at least some of them?

[Marsman1996]

Well, I guess OSTD developers may not be very interested in the proof code, so hiding it seems reasonable.

[hiroki-chen]

should we expose proof functions at all (except those for manipulating tracked variables)?

[rikosellic]

should we expose proof functions at all (except those for manipulating tracked variables)?

We should if it is a high-level lemma or an important invariant preservation lemma with detailed documentation. But most proof fns are not.

[hiroki-chen]

should we expose proof functions at all (except those for manipulating tracked variables)?

We should if it is a high-level lemma or an important invariant preservation lemma with detailed documentation. But most proof fns are not.

Okay, but due to the current unstable codebase this issue should be at low priority.

[rikosellic]

Considering that a verification blog will be released soon, we should do something. @Marsman1996 is KVerus able to give a list of non-critical proof fns? Then I can check it and decide whether we should hide the functions.

[Marsman1996]

is KVerus able to give a list of non-critical proof fns? Then I can check it and decide whether we should hide the functions.

I will give it a try

[Marsman1996]

@rikosellic KVerus (or GPT-5.5) gives me a 40 proof function version, and a 46 proof function version 👀

proof_fns_40_version.md

critical_proof_fns_by_dev_policy.md

[rikosellic]

Thanks, I will check this next week.