document links block#464
Conversation
naftali-g
force-pushed
the
naftali/new_links_block
branch
from
f47ea03 to
b8746a3
Compare
johspaeth
left a comment
johspaeth
left a comment
There was a problem hiding this comment.
We should make it more explicit in options.md that linking via spec is the preferred way.
Other than that, only minor nits. Thanks a lot.
docs/cvl/linking.md
Outdated
| =========== | ||
|
|
||
| The `links` block allows you to declare contract linking directly in your CVL | ||
| specification, replacing the {ref}`--link` and {ref}`--struct_link` CLI flags. |
There was a problem hiding this comment.
I would talk about the conf file attributes rather, I doubt people use the CLI flags for linking.
docs/cvl/linking.md
Outdated
|
|
||
| The simplest form of linking maps a storage variable that holds an address to a | ||
| contract instance in the scene. This is equivalent to using the {ref}`--link` | ||
| CLI flag. |
There was a problem hiding this comment.
... / conf file attribute
| This allows the Prover to explore both the case where both elements point to | ||
| the same contract and the case where they point to different contracts. |
There was a problem hiding this comment.
Do we want to state here that this is similar to a dispatch list? Should we recommend one over the other?
There was a problem hiding this comment.
I think that might just be more confusing...
There was a problem hiding this comment.
You might be right, let's keep it simple.
docs/prover/cli/options.md
Outdated
| ```{note} | ||
| You can also declare linking inline in your spec using a {ref}`links block <linking>`, | ||
| which provides type checking, precise struct paths, and support for arrays, | ||
| mappings, and wildcards. The `links` block and `--link` flag cannot be used | ||
| together for the same contract. | ||
| ``` |
There was a problem hiding this comment.
Please state that linking in spec is the recommended approach - and move it to the top of the entry so that user directly see it.
|
@naftali-g Just a reminder not to merge this PR until we release the main version. |
srunquist-certora
changed the base branch from
master
to
release/version_8.11.0
Co-authored-by: Shane <shane@certora.com>
4 participants
Naming convention:
Before requesting review:
spelling_wordlist.txtREADME.mdfor information about style and markdown syntaxJira ticket: TODO
Link to generated documentation: https://certora-certora-prover-documentation--464.com.readthedocs.build/en/464/docs/cvl/linking.html