For release 1.0.0, we need to update SOUNDNESS.md Specifically: 1. Update the link to the s2n-bignum SOUNDNESS document. It moved from the "doc" subdirectory to the root of the s2n-bigum repo. 2. Update the text to cover the final set of x86_64 functions that have HOL-Light proofs at the v1.0.0 release point.
Activity
mkannwischer commentedon Jun 25, 2026
Already implemented by #1112.
[-]Create SOUNDNESS.md[/-][+]Update SOUNDNESS.md for release v1.0.0[/+]mkannwischer commentedon Jul 17, 2026
I think this was addressed by #1188.
@rod-chapman, @hanno-becker are you happy with the current state of the soundness documwnt?
mkannwischer commentedon Jul 26, 2026
@rod-chapman, @jakemas, do you want to make additional changes to the SOUNDNESS.md, or is this done already?
rod-chapman commentedon Jul 27, 2026
Please update the link to the s2n-bignum SOUNDNESS document. It moved from the "docs" subdirectory into the root dir of the s2n-bignum repo.