docs: add examples and documentation in the guide about HOCAP style logatom

[bsdinis]

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[ahuoguo]

I think Travis might have mentioned this at the retreat, but maybe making this a module-level rustdoc for vstd::logatom makes more sense, and leaving a link to the rustdoc in the logical atomicity chapter. I think my process of going through this guide requires me to jump to the vstd::logatom code frequently.

[tjhance]

We should definitely have verusdoc style docs for logatom in vstd, but we also desperately need more "guide" material on the subject of concurrency verification, which should include an overview of logical atomicity approaches, among other topics. So I think this material, as written, is appropriate for the guide. It's probably fine as-is; we can organize it more later once we have more material.

[parno]

Thanks for working on this! I realize it's still work in progress, but I was curious to take a look.

[parno]

Ideally, the Guide examples should be readable in the guide, without having to refer to the Verus files elsewhere in the repo. Can you use some anchor tags to include relevant snippets from the file here instead?

[slerpyyy]

If the example is too large, we could also hide it behind an HTML <detail> element so it doesn't interrupt the flow of the explanation too much. The mdbook does seem to support this, but it would be the first time we do this in the guide.

[bsdinis]

I think the point here is to guide through the HOCAP parts of the example, and the reference to the guide is just for reference (pardon my tautology).

If we do want to insist on having the full thing, the way to go is the <detail>, but at the end of the example