Generate `:exhaust` for simple properties. #1848

ChrisEPhifer · 2025-04-28T10:57:33Z

Closes #1842.

This works by adding Text of the form:

```
:exhaust p
```

To the list of docstrings extracted from a module's Decls, when p is a Bit-typed declaration that has the property Pragma.

I wasn't set up to run every test in the regression suite (particularly those requiring CVC4/CVC5/Bitwuzla/Yices); I've marked this as a draft for now, and will use CI to determine which (if any) additional golden/.stdout files I need to update.

ChrisEPhifer · 2025-04-28T11:20:59Z

OK, CI seems happy, so I think this is ready for review / to be merged.

RyanGlScott · 2025-04-28T11:22:46Z

I think I'm missing something: what is the :ensure command mentioned in the PR title? Did you mean to say ":exhaust", or is :ensure something different entirely?

ChrisEPhifer · 2025-04-28T11:23:52Z

I think I'm missing something: what is the :ensure command mentioned in the PR title? Did you mean to say ":exhaust", or is :ensure something different entirely?

... Oops. You're right, sorry. Let's not think too hard about what time it is on the west coast...

RyanGlScott

This looks reasonable at a quick glance. I think it would be worth mentioning the fact that Cryptol implicitly :exhausts Bool-typed properties somewhere in the Documentation Comments section of the Cryptol user manual, however.

RyanGlScott · 2025-04-28T11:27:06Z

tests/docstrings/T05.icry.stdout

+    :exhaust p
+      Using exhaustive testing.
+      Testing... Passed 1 tests.
+      Q.E.D.


This example already has an explicit :exhaust pragma in the docstrings:

cryptol/tests/docstrings/T05.md

Lines 13 to 15 in 86ee4b6

```

:exhaust p

```

As such, this runs :exhaust p twice (you can see the output of the other :exhaust p invocation above). Is it possible to detect examples like this to avoid redundantly running :exhaust again?

Good idea. I can poke around at the code consuming the gathered-up docstrings / see about de-duplicating what's extracted there, rather than trying to detect this based on the docstring text itself.

How about we change the rule to be "if a piece of code has no code blocks and it is of type Bit, then add an implicit :exhaust" otherwise leave it alone. So this is a kind of default action for things of type Bit but if the user adds a code block, then they can say explicitly say what they want to do, so we don't add an implicit one as well.

Oh sure! If that's an acceptable adjustment to what we originally wanted, it's definitely an easy way to avoid duplicates without any kind of janky cleanup after gathering up / extracting all the code blocks.

I'll adjust what I had queued up re: changes to the reference manual and implement this check instead.

~~Actually -- We don't know about the structure of the docstring code blocks until the extraction is done, so we'll have to move some of this into the REPL.Command module.~~

I was hoping to just replace <> with <|> where I'm adding the new doctring test, but this is too aggressive, as it'll skip adding the :exhaust if there are any docstring comments, even if there are no other code fences,

Pay no mind, I'm silly :)

RyanGlScott · 2025-04-28T11:28:18Z

tests/docstrings/T10.icry.stdout

@@ -22,12 +22,32 @@ Checking module T10
  Docstrings on T10::where_at__30_11::N
  Docstrings on T10::F1::N
  Docstrings on T10::M::q
+    :exhaust q


Relatedly, I wonder if this output should say something like ":exhaust q (implicit)" or some such to indicate that this is running due to the implicit behavior of how :check-docstrings works, rather than an explicit directive in the docstrings themselves.

yav

Looks good to me, but let's do the fix where we only add the :exhaust if there's no user-defined code blocks.

We should also update the docs, and the CHANGES files before merging.

If the given declaration is of Bit (Boolean) type and a property, return a docstring code fence that uses :exhaust to validate the property. Note that we return a Maybe value in order to easily integrate with the existing declaration docstring handling.

Straightforward use of the Semigroup a => Semigroup (Maybe a) instance to combine user-provided docstrings with our :exhaust tests (when we encounter a property declaration of Bit/Boolean type, as described in the previous commit).

These show the new :exhaust tests being added as expected. I'm not currently set up to run CVC4/5, Yices, or Bitwuzla - so I am unsure if those tests need their golden/reference files updated.

This helps distinguish automatically-generated :exhaust checks from those that were explicitly written by users. Fortunately, the docstring/doctest extraction mechanism preserves the full text -- so this was as simple as adding a valid line comment.

This function is useful to determine when to add implicit :exhaust commands to property docstrings, but was too high in the Cryptol.* module dependency hierarchy.

This adds the additional condition that the declaration's docstring contain no runnable code blocks (i.e. code blocks that are unlabeled or labeled with repl). This change 'fixes' docstring test T05, in particular by avoiding the duplicate exhaustive testing the previous behavior caused.

ChrisEPhifer · 2025-04-29T07:10:21Z

Looks good to me, but let's do the fix where we only add the :exhaust if there's no user-defined code blocks.

We should also update the docs, and the CHANGES files before merging.

e26fcf7 and ea49660

RyanGlScott

LGTM, aside from some minor quibbles.

RyanGlScott · 2025-04-29T11:59:18Z

src/Cryptol/TypeCheck/AST.hs

+-- | Extract the code blocks from the body of a docstring.
+--
+-- A single code block starts with at least 3 backticks followed by an
+-- optional language specifier of "cryptol". This allowed other kinds


Haddock trick to prevent "cryptol" from being highlighted as a module identifier:

Suggested change

-- optional language specifier of "cryptol". This allowed other kinds

-- optional language specifier of \"cryptol\". This allowed other kinds

RyanGlScott · 2025-04-29T11:59:31Z

src/Cryptol/TypeCheck/AST.hs

+-- | Extract the code blocks from the body of a docstring.
+--
+-- A single code block starts with at least 3 backticks followed by an
+-- optional language specifier of "cryptol". This allowed other kinds


Suggested change

-- optional language specifier of "cryptol". This allowed other kinds

-- optional language specifier of "cryptol". This allows other kinds

RyanGlScott · 2025-04-29T12:02:42Z

CHANGES.md

+* `Bit` properties (e.g. `property p = True`) will be checked with `:exhaust`,
+  unless their docstrings contain code blocks understood by `:check-docstrings`.
+  ([#1842](https://github.com/GaloisInc/cryptol/issues/1842))


When I first read this sentence, I was under the false impression that all Bit properties would be checked with :exhaust. I think this should mention "when running :check-docstrings" upfront, as that is an important caveat. Something like:

Suggested change

* `Bit` properties (e.g. `property p = True`) will be checked with `:exhaust`,

unless their docstrings contain code blocks understood by `:check-docstrings`.

([#1842](https://github.com/GaloisInc/cryptol/issues/1842))

* When running the `:check-docstrings` command, `Bit` properties (e.g. `property p = True`) will be checked with `:exhaust`,

unless their docstrings contain code blocks understood by `:check-docstrings`.

([#1842](https://github.com/GaloisInc/cryptol/issues/1842))

yav

I don't think Crypto.TypeCheck.AST is a good home for extractBlocks, let's find a better place.

yav · 2025-04-29T15:55:27Z

src/Cryptol/REPL/Command.hs

@@ -1993,61 +1993,6 @@ moduleInfoCmd isFile name
       rPutStrLn "}"
       pure emptyCommandResult



Why did extractCodeBlocks get moved to Cryptol.TypeCheck.AST? I don't think that's a good place for it, as we already have too much stuff in that module. As far as I can see, it's only called from Command, so keeping it there is probably OK. If it does need to be moved for some reason, let's see what's a better place for it.

This PR updates the code to also call extractCodeBlocks from Cryptol.TypeCheck.AST (from gatherModuleDocstrings).

Oh I see, that was already there. I think we should make a new module called Docstrings (or something) in the same directory, and move both of these functions there. In general, the plan is that AST should contain the AST and any little convenience function for working with it, but things that provide additional functionality should be in their own modules.

OK, no problem -- I didn't love it either, I was just trying to make minimally-invasive changes that made sense in the existing module hierarchy, but I'm happy to add this new module.

The new module is Cryptol.TypeCheck.Docstrings.

ChrisEPhifer

Alright, I've moved the docstring functions to a new module Cryptol.TypeCheck.Docstrings, and addressed the the small Haddock typos / lacking clarity Ryan caught in CHANGES.md.

ChrisEPhifer · 2025-04-29T19:51:28Z

src/Cryptol/REPL/Command.hs

@@ -1993,61 +1993,6 @@ moduleInfoCmd isFile name
       rPutStrLn "}"
       pure emptyCommandResult



ChrisEPhifer · 2025-04-29T19:51:53Z

CHANGES.md

+* `Bit` properties (e.g. `property p = True`) will be checked with `:exhaust`,
+  unless their docstrings contain code blocks understood by `:check-docstrings`.
+  ([#1842](https://github.com/GaloisInc/cryptol/issues/1842))


ChrisEPhifer · 2025-04-29T19:52:13Z

src/Cryptol/TypeCheck/AST.hs

+-- | Extract the code blocks from the body of a docstring.
+--
+-- A single code block starts with at least 3 backticks followed by an
+-- optional language specifier of "cryptol". This allowed other kinds


ChrisEPhifer · 2025-04-29T19:52:38Z

src/Cryptol/TypeCheck/AST.hs

+-- | Extract the code blocks from the body of a docstring.
+--
+-- A single code block starts with at least 3 backticks followed by an
+-- optional language specifier of "cryptol". This allowed other kinds


yav

Looks good, thanks!

ChrisEPhifer added feature docstrings labels Apr 28, 2025

ChrisEPhifer added this to the ASAP milestone Apr 28, 2025

ChrisEPhifer requested a review from yav April 28, 2025 10:57

ChrisEPhifer self-assigned this Apr 28, 2025

ChrisEPhifer linked an issue Apr 28, 2025 that may be closed by this pull request

Improve project checking to auto validate easy properties #1842

Closed

ChrisEPhifer temporarily deployed to github-pages April 28, 2025 10:57 — with GitHub Actions Inactive

ChrisEPhifer changed the title ~~Draft: Generate :ensure for simple properties.~~ Generate :ensure for simple properties. Apr 28, 2025

ChrisEPhifer changed the title ~~Generate :ensure for simple properties.~~ Generate :exhaust for simple properties. Apr 28, 2025

RyanGlScott reviewed Apr 28, 2025

View reviewed changes

yav approved these changes Apr 28, 2025

View reviewed changes

ChrisEPhifer temporarily deployed to github-pages April 29, 2025 06:53 — with GitHub Actions Inactive

chrisephifer-g added 7 commits April 28, 2025 23:59

Update some .stdout files.

9c25ddd

These show the new :exhaust tests being added as expected. I'm not currently set up to run CVC4/5, Yices, or Bitwuzla - so I am unsure if those tests need their golden/reference files updated.

docs/RefMan/BasicSyntax: Add a short note about implicit :exhaust.

e26fcf7

Move extractCodeBlocks REPL.Command -> TypeCheck.AST.

8456380

This function is useful to determine when to add implicit :exhaust commands to property docstrings, but was too high in the Cryptol.* module dependency hierarchy.

ChrisEPhifer force-pushed the 1842-improve-project-checking branch from a535b85 to 6af7930 Compare April 29, 2025 06:59

ChrisEPhifer temporarily deployed to github-pages April 29, 2025 06:59 — with GitHub Actions Inactive

CHANGES: Document new implicit :exhaust checks on Bit properties.

ea49660

ChrisEPhifer temporarily deployed to github-pages April 29, 2025 07:06 — with GitHub Actions Inactive

RyanGlScott approved these changes Apr 29, 2025

View reviewed changes

yav requested changes Apr 29, 2025

View reviewed changes

TypeCheck.AST: Prevent highlighting "cryptol" as module identifier.

d041d04

chrisephifer-g added 2 commits April 29, 2025 11:46

TypeCheck.AST: Typo allowed -> allows.

faf00ff

CHANGES: Clarify when Bit properties will be implicitly :exhaust-ed.

aee7bfb

ChrisEPhifer temporarily deployed to github-pages April 29, 2025 18:52 — with GitHub Actions Inactive

Move gatherModuleDocstrings and extractCodeBlocks to new module.

dd8f8da

The new module is Cryptol.TypeCheck.Docstrings.

ChrisEPhifer temporarily deployed to github-pages April 29, 2025 19:50 — with GitHub Actions Inactive

ChrisEPhifer commented Apr 29, 2025

View reviewed changes

ChrisEPhifer requested a review from yav April 29, 2025 20:34

yav approved these changes Apr 29, 2025

View reviewed changes

yav merged commit 6653adb into master Apr 29, 2025
50 checks passed

yav deleted the 1842-improve-project-checking branch April 29, 2025 22:07

	-- optional language specifier of "cryptol". This allowed other kinds
	-- optional language specifier of \"cryptol\". This allowed other kinds

		@@ -1993,61 +1993,6 @@ moduleInfoCmd isFile name
		rPutStrLn "}"
		pure emptyCommandResult

Generate :exhaust for simple properties. #1848

Generate :exhaust for simple properties. #1848

Uh oh!

Conversation

ChrisEPhifer commented Apr 28, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ChrisEPhifer commented Apr 28, 2025

Uh oh!

RyanGlScott commented Apr 28, 2025

Uh oh!

ChrisEPhifer commented Apr 28, 2025

Uh oh!

RyanGlScott left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

yav Apr 28, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ChrisEPhifer Apr 28, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

yav left a comment

Choose a reason for hiding this comment

Uh oh!

ChrisEPhifer commented Apr 29, 2025

Uh oh!

RyanGlScott left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

yav left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ChrisEPhifer left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Generate `:exhaust` for simple properties. #1848

Generate `:exhaust` for simple properties. #1848

ChrisEPhifer commented Apr 28, 2025 •

edited

Loading

yav Apr 28, 2025 •

edited

Loading

ChrisEPhifer Apr 28, 2025 •

edited

Loading