Website updates for 0.6.0 release#6
Merged
Merged
Conversation
Add the 0.6.0 news item and refresh the CFRG hybrid KEM case study for the report, bounds companion, and per-proof `bound:` clauses the release adds. This is a partial update: the rest of the 0.6.0 website work is specified in extras/docs/plans/todo/2026-07-22-website-update-0.6.0.md in the engine repo. Notably, limitations.md, canonicalization.md, and researchers/soundness.md still state that ProofFrog does not track quantitative advantage bounds, which 0.6.0 makes false. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Partial website update for the forthcoming 0.6.0 release.
Changes
index.md— news item for 0.6.0: concrete advantage bounds, LaTeX export, tuple-destructuring bindings, the Emacs mode, and the soundness-fix wave with the re-run advisory.examples.md— CFRG hybrid KEM case study refreshed: the report of findings and bounds companion, the 57 proofs now each declaring abound:clause, and the sixgames/ROM/helper games with declaredadvantage <= ...;clauses backed by hand-written EasyCrypt proofs of those bounds.Verified with
bundle exec jekyll build.Needs checking before merge
The news item is dated Jul. 22, 2026 and links
releases/tag/v0.6.0. Both were inferred fromRELEASE.md— at the time of writing,pyproject.tomlon the engine'smainstill read0.5.1.dev0and nov0.6.0tag existed. Confirm both once the release is cut.Not included
This is deliberately a subset. The remaining 0.6.0 website work is specified in
extras/docs/plans/todo/2026-07-22-website-update-0.6.0.mdin the engine repo — 11 items covering a new Advantage Bounds page (full draft embedded in the plan), a LaTeX Export page,export-latexand--skip-boundin the CLI reference, thebound:andadvantage <=language-reference sections, tuple-destructuring bindings, the Emacs section, and the engine-internals additions.Worth flagging:
manual/limitations.md,manual/canonicalization.md, andresearchers/soundness.mdeach currently state that ProofFrog does not track quantitative advantage bounds — the headline feature of this release. Those passages are live and now false; they are the top-priority items in the plan.🤖 Generated with Claude Code