Add documentation to Core.Procedure

[tautschnig]

Module-level documentation covering:

• Concrete syntax of procedure declarations
• Parameter modes (input vs output) and their semantics
• Specification: modifies, requires, ensures
• Free specifications (free requires, free ensures)
• Labels on specification clauses
• The old(expr) expression and its semantics (distribution, idempotence, global-only)
• Call semantics (assert preconditions → havoc → assume postconditions)
• Body verification
• Type parameters (polymorphism)
• A concrete example from the repository

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[tautschnig]

It may be best to review this as rendered at docs/verso/_out/api/Strata/Languages/Core/Procedure.html.

[Copilot]

Pull request overview

This PR adds comprehensive module-level documentation to Core.Procedure, describing Strata Core procedures as the main verification unit and documenting their syntax, specification constructs (modifies/requires/ensures), free clauses, labels, old(expr), call semantics, and polymorphic type parameters.

Changes:

• Added a large module doc comment explaining procedure syntax and verification semantics.
• Added/expanded docstrings on Procedure.Header, Procedure.CheckAttr, Procedure.Check, Procedure.Spec, and Procedure.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[atomb]

It'd be good to address the Copilot suggestions, but otherwise I think this is good.

One question I have, and this might be for a future PR, is how much of this text should be in the Core language definition document.

[tautschnig]

One question I have, and this might be for a future PR, is how much of this text should be in the Core language definition document.

Added as further commit.

[atomb]

Now that the Core.Procedure module is imported into the Verso docs, there are a few errors building it:

• Core.Procedure.CheckAttr.Free doesn't have a docstring
• Core.Procedure.CheckAttr.Default doesn't have a docstring
• Factory is ambiguous

[tautschnig]

Now that the Core.Procedure module is imported into the Verso docs, there are a few errors building it:

* `Core.Procedure.CheckAttr.Free` doesn't have a docstring

* `Core.Procedure.CheckAttr.Default` doesn't have a docstring

* `Factory` is ambiguous

Fixed in f8c433f.