Conversation
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
|
It may be best to review this as rendered at |
There was a problem hiding this comment.
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, andProcedure.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| The semantics of a call (see `CallElim` and `StatementSemantics`) are: | ||
|
|
||
| 1. Evaluate the argument expressions `e₁, ..., eₙ`. | ||
| 2. **Assert** each (non-free) precondition, substituting actuals for formals. |
There was a problem hiding this comment.
This call-semantics section cites CallElim and says only non-free preconditions are asserted at call sites. However, the current CallElim transform generates asserts for all proc.spec.preconditions without filtering out clauses with check.attr == .Free, so free requires end up being checked after call elimination. Either adjust the doc to avoid attributing this behavior to CallElim, or (preferably) update CallElim to skip Free preconditions when generating asserts so the transform matches the stated semantics.
| 2. **Assert** each (non-free) precondition, substituting actuals for formals. | |
| 2. **Assert** each precondition, substituting actuals for formals. |
There was a problem hiding this comment.
I think this is a bug in the implementation rather than the documentation. Nice catch, Copilot!
| ``` | ||
| procedure Name<TypeArgs>(x₁ : T₁, ..., xₙ : Tₙ) returns (y₁ : U₁, ..., yₘ : Uₘ) | ||
| spec { | ||
| modifies g₁, g₂, ...; |
There was a problem hiding this comment.
The concrete syntax example shows a single modifies clause with a comma-separated list (modifies g₁, g₂, ...;), but the Core parser only supports one identifier per modifies spec element (modifies <Ident>;), repeated for multiple globals. Updating the snippet to match the actual grammar will avoid confusing users.
| modifies g₁, g₂, ...; | |
| modifies g₁; | |
| modifies g₂; | |
| ... |
There was a problem hiding this comment.
Maybe we should update the concrete syntax to match the documentation, rather than the other way around.
atomb
left a comment
atomb
left a comment
There was a problem hiding this comment.
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.
| ``` | ||
| procedure Name<TypeArgs>(x₁ : T₁, ..., xₙ : Tₙ) returns (y₁ : U₁, ..., yₘ : Uₘ) | ||
| spec { | ||
| modifies g₁, g₂, ...; |
There was a problem hiding this comment.
Maybe we should update the concrete syntax to match the documentation, rather than the other way around.
| The semantics of a call (see `CallElim` and `StatementSemantics`) are: | ||
|
|
||
| 1. Evaluate the argument expressions `e₁, ..., eₙ`. | ||
| 2. **Assert** each (non-free) precondition, substituting actuals for formals. |
There was a problem hiding this comment.
I think this is a bug in the implementation rather than the documentation. Nice catch, Copilot!
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
tautschnig
dismissed stale reviews from andrewmwells-amazon and atomb
via
63fb685
Added as further commit. |
3 participants
Module-level documentation covering:
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.