Guide: Update language about logic functions and document #[open]

[ethanbb]

Following up on conversation in #1643. The first section of the "Logic functions" page was out of date, also mentioning #[predicate] which has been removed, plus it was a bit unclear about what is allowed where within a logic function. I rewrote that part with what I believe are the correct rules but please check. Also, I saw that #1622 would maybe change the situation re: loops? If so, that will need to be changed soon.

I added another paragraph documenting #[open] and saying a little about how it relates to how the logic function is used, e.g. as a lemma or as a predicate. I do think it might be useful to say more about lemmas somewhere and note how/when to use them and that actually any function can be considered a lemma if its pre/postconditions are useful for the prover but its body doesn't do anything useful for the program. I just realized this myself, maybe it is obvious if you have more experience working with automated provers though. For what it's worth, I found the Dafny tutorial on lemmas very helpful (actually I would have been totally lost trying to learn Creusot if I hadn't gone through the Dafny guides first, maybe it's worth recommending?)

[arnaudgolfouse]

Thanks a lot! There are things I want to reword, but I'll merge this and do my changes on top.

RE: lemmas: I think we should spend some time explaining this, yes... I think I'll add the Dafny tutorial in a footnote for now.