Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix docstrings #108

Merged
merged 4 commits into from
Aug 6, 2024
Merged

Fix docstrings #108

merged 4 commits into from
Aug 6, 2024

Conversation

marsella
Copy link
Contributor

@marsella marsella commented Aug 5, 2024

Closes #105.

This fixes some docstring checks and proves to use the correct notation, instead of an outdated version, and updates some comments about provability to actually have a proving docstring. It also cleans up some parameterized imports in AES that didn't need to be parameterized.

- Fixes docstrings to use correct notation and parameterization
- Modifies AES spec to parameterize modules at import time instead of at
  use, to address an import sketchiness for running the docstrings
- Adds a citation.
Copy link
Contributor

@mccleeary-galois mccleeary-galois left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, :check-docstring seems to be working well @glguy on these. One thing of note is for extremely large :check-docstring processes there is no notion if it is just hanging or taking a long time to compute. I know that this is an issue for any property check that takes a significant amount of time but this is a bit extended by the fact that all of the checks need to complete before output is produced. No action needed on this comment at the moment just something to note.

Copy link
Member

@glguy glguy left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Everything looks right except:

  • GC28.cry has a couple of code fences using cryptol instead of repl that I think should be changed. I checked and those properties do pass unless that module is out of scope for things change.

These changes help demonstrate that it can be confusing to know which modules are functors and which are not and therefore which modules should be able to have their docstrings tested.

Primitive/Symmetric/Cipher/Authenticated/aes_gcm.bat Outdated Show resolved Hide resolved
@marsella marsella merged commit 40b6240 into master Aug 6, 2024
2 checks passed
@marsella marsella deleted the fix-docstrings branch August 6, 2024 14:47
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Fix docstrings for AES & friends
3 participants