Release Notes — v0.4.1

This release focuses on proof engine improvements, adding new canonicalization transforms and fixing correctness bugs in the inliner and type resolver. The main driver is a complete IND-CCA proof of the CK hybrid KEM combiner from the StarHunters paper, which required extending the engine to handle tuple reasoning, cross-scope dead branch elimination, and deterministic call hoisting.

New canonicalization transforms

• HoistDeterministicCallToInitialize (#206): Hoists a repeated deterministic call out of oracle methods into Initialize, caching the result in a new field. Enables proofs where the reduction caches a challenger response while the scheme re-expands it at each oracle site.
• ExtractRepeatedTupleAccess (#204): Extracts repeated variable[constant] tuple accesses into named locals, normalizing explicit tuple destructuring against inline access.
• IfSplitBranchAssignment (#204): Moves subsequent code into if/else branches when all branches assign the same variable.
• ElseUnwrap (#204): Unwraps else blocks when the if-branch unconditionally returns.

Engine improvements

• Z3 tuple support (#204): Z3 can now reason about tuple equality, opaque types, and array access.
• Nested dead branch elimination (#204): RemoveUnreachableTransformer now propagates path constraints into nested blocks, eliminating branches that require cross-scope reasoning.
• Extended IfConditionAliasSubstitution to accept parameter[constant] patterns (#204).
• Extended ChallengeExclusionRFToUniform to resolve local aliases through intermediate cast variables (#204).
• Extended DeadNullGuardElimination to handle provably non-nullable expressions (not just variables) (#204).

Bug fixes

• Fix inliner early-return handling (#204): The inliner leaked bare ReturnStatement nodes from callees with early returns into the caller's block. Now correctly normalizes early returns via else-branch folding.
• Fix _resolve_type_alias for tuple-of-types (#203): Tuple arguments substituted for game parameters caused false type mismatches on FieldAccess nodes; fixed by adding a Tuple case that normalizes to ProductType.

Tooling

• Dev builds annotated with git SHA (#205): proof_frog version now appends the short commit SHA to dev builds (e.g. 0.4.1.dev0+d3de90e).

New examples

• CK hybrid KEM combiner (#204): Complete IND-CCA proof for the CK hybrid KEM combiner from the StarHunters paper, verifying all 17 game hops.

Release Notes — v0.4.0

This is a major release with significant language additions, many engine soundness fixes and new transforms, a redesigned web interface, and new tooling features.

Language

• Added built-in Function<D, R> type replacing RandomFunctions, with random oracle model (ROM) support (#177).
• Added built-in Group type and group algebra engine transforms (#176).
• Added deterministic and injective method annotations for primitives and schemes, with typechecker enforcement of consistency (#179).
• Added support for type equality constraints between abstract and concrete types (#165).
• Added multi-line block comment syntax (/* ... */).
• Removed Phase support from the grammar and engine.

Proof Engine

• Parallelized proof hop verification for faster proof checking.
• Added lemma support for modular proof composition via lemma: sections (#166).
• Added diagnostic engine for proof failure explanations, including diff classification, near-miss matching, and engine limitation detection (#162).
• Added multi-level verbosity to the prove command and web UI (#163).
• Fixed over 30 soundness bugs across numerous transforms, including CrossMethodFieldAlias, HoistFieldPureAlias, RedundantFieldCopy, InlineSingleUseField, CounterGuardedFieldToLocal, SimplifyReturn, ApplyAssumptions, and others.

New and Extended Transforms

• DeduplicateDeterministicCalls and CrossMethodFieldAlias for deterministic method optimization (#164).
• NormalizeCommutativeChains for canonical ordering of + and * operators.
• BooleanIdentity for AND/OR constant folding (#173).
• DistinctConstRFToUniform with length-carrying BinaryNum refactor (#187).
• UniformBijectionElimination replacing the unsound TrivialEncodingElimination.
• ChallengeExclusionRFToUniform extended for slice-based guards.
• FreshInputRFToUniform extended for tuple and concatenation arguments.
• Replaced bubble sort with canonical topological sort in StabilizeIndependentStatements.
• Replaced str()-based sort keys with structural AST sort keys (#190).

CLI

• Added version command.
• Added download-examples command for fetching example files (#193).
• Added --skip-lemmas flag for bypassing lemma verification.
• Improved error messages for parse and check commands, including typo suggestions for field access errors (#161).

Web Interface

• Redesigned toolbar with Insert dropdown and engine introspection actions (Describe, Inlined Game).
• Added wizard system with server-side scaffolding for intermediate games, reductions, and reduction hops.
• Added help menu with links to manual pages.

MCP Server

• Updated language reference to cover full FrogLang syntax.

Release Notes — v0.3.1

This version primarily focuses on improvements to the web interface.

Web Interface

• Added "New File" button and dialog for creating new files directly in the web UI (#108).
• Highlight error lines in the web editor and improved missing-semicolon diagnostics (#107).
• Fixed inline Hop Inspector breaking the Game Hops panel and incorrectly showing the Run Proof button (#106).
• Highlight differing lines between canonical forms in the hop inspection view (#105).
• Added live Markdown preview to the web UI editor (#104).
• Show warning modal for proofs containing induction steps (#103).

CLI

• Added --json flag to CLI commands for structured output (#101).

Release Notes — v0.3.0

Web Interface (new)

• Added a browser-based web interface (proof_frog web <directory>) powered by Flask and CodeMirror 5.
• File explorer sidebar with expand/collapse all buttons for navigating .primitive, .scheme, .game, and .proof files.
• FrogLang syntax highlighting, light and dark (Dracula) themes.
• Parse, type-check, and run proofs directly from the browser.
• Game hop explorer: view per-hop validity results, inspect inlined and canonicalized forms of each game step in a resizable split-view panel.
• Initial setup wizard for new users.
• Security hardening: CSRF resistance, Content Security Policy headers, dotfile blocking, import path sandboxing, capped iteration limits, and XSS protections.

MCP Server (new)

• Added a Model Context Protocol (MCP) server (proof_frog/mcp_server.py) for AI-assisted proof authoring.
• Tools include parse_file, check_file, prove_file, get_step_detail, get_inlined_game, and more.
• Documented in CLAUDE_MCP.md with a full usage guide.

CLI

• Migrated CLI argument parsing from sys.argv to click.
• Improved parse and semantic error messages with source location and context.
• Better file-not-found error messages.

Proof Engine

• InlineSingleUseVariableTransformer: inlines single-use variable assignments during canonicalization.
• SimplifyReturnTransformer and ExpandTupleTransformer improvements.
• Fixed redundant copy bug in RedundantCopyTransformer.
• Fixed naming collision in VariableStandardizingTransformer.
• Eliminated read-after-read dependency in analysis.
• All hops are now checked even when an earlier hop fails, with per-hop result tracking.

Import Resolution

• Import paths in FrogLang files are now resolved relative to the importing file's directory (previously relative to the working directory).
• All example files migrated to use file-relative import paths.

Testing

• Converted shell-based test scripts (testAST.sh, testProofs.sh) to pytest.
• Parallelized test execution via pytest-xdist (-n auto by default).
• Added new test suites: test_inline_single_use_variable.py, test_variable_standardizing.py, test_redundant_copies.py, test_path_security.py, test_describe.py, test_ast.py.

Documentation

• Added docs/guide.md: a comprehensive guide for writing primitives, games, schemes, and proofs in FrogLang.
• Expanded README.md with documentation and FrogLang examples.
• Added CLAUDE.md project instructions and CLAUDE_MCP.md MCP tool usage guide.
• Added Makefile with lint and format targets.

Other

• Added click and flask to project dependencies.
• Added ProofFrog favicon and logo assets.