Merged
Conversation
Create stub landing pages for the new nav hierarchy (manual/, manual/language-reference/, manual/worked-examples/, researchers/) so later tasks have parents to attach to. Bump nav_order on existing top-level pages (examples, design, getting-started, guide) so the new sections take their correct slots while the old pages remain reachable until decommission. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Migrated install instructions from getting-started.md, expanded with platform-specific prerequisites (macOS/Windows/Linux), shell-specific venv activation (bash/zsh, fish, PowerShell), and command-not-found troubleshooting. Co-Authored-By: Claude Sonnet (subagent) <noreply@anthropic.com>
- Correct proof_frog version output example to match real format - Add PowerShell execution-policy warning for fresh Windows installs - Include python3-pip in Fedora install command - Add git submodule update --init to source install Co-Authored-By: Claude Sonnet (subagent) <noreply@anthropic.com>
10-minute first-run experience using the web editor against examples/joy: run OTPSecure.proof green, break a single game-sequence line to see the real diagnostic, fix it, three-sentence conceptual summary. No FrogLang is written by the reader. Co-Authored-By: Claude Sonnet (subagent) <noreply@anthropic.com>
Reference for the six public commands (version, parse, check, prove, describe, web) with synopsis, behavior, options, examples, and common errors per command. Authoritative help output captured from the current proof_frog source. Engine-introspection commands are deliberately excluded; they will live in the researcher-facing engine-internals page. Co-Authored-By: Claude Sonnet (subagent) <noreply@anthropic.com>
Shared syntactic layer of FrogLang: lexical, types, expressions and operators, sampling, statements, and imports. Draws from SEMANTICS.md Sections 2-4 with operator-precedence and algebraic-property tables, migrated prose from guide.md, and gotchas from CLAUDE.md (XOR on bitstrings, non-determinism default, sampled vs. declared Function<D, R>). Co-Authored-By: Claude Sonnet (subagent) <noreply@anthropic.com>
- Distinguish status badge color from body text in the broken-proof example - Add parenthetical explaining the engine's "Succeeded, but is incomplete" wording Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Operational semantics layer between basics.md and the four file-type pages: adversary model, game execution lifecycle, state semantics, the non-determinism default and the deterministic/injective annotations, sampling and randomness including the random-oracle Function<D,R> distinction, composition mechanics for game+scheme and game+reduction, and the formal definition of interchangeability. Drawn primarily from SEMANTICS.md sections 6, 7, and 8.3. Co-Authored-By: Claude Sonnet (subagent) <noreply@anthropic.com>
Reference for the .primitive file type: block syntax, parameter forms, set field declarations, method signatures, deterministic/injective modifiers and matching- modifier rule, with examples drawn from current examples/Primitives/. Cross- references basics.md for types and execution-model.md (in progress) for oracle semantics. Co-Authored-By: Claude Sonnet (subagent) <noreply@anthropic.com>
Long-form four-file walkthrough mirroring Joy of Cryptography Sec 2.5: define SymEnc primitive, OneTimeSecrecy game, OTP scheme, and OTPSecure proof. Each step shows the file growing incrementally with new language constructs explained at the line that introduces them; CLI alternatives in callouts; empty assume: block called out as the information-theoretic case. Closing pointer to worked examples, language reference, and transformations for what's next. Co-Authored-By: Claude Sonnet (subagent) <noreply@anthropic.com>
basics.md: - Remove fabricated % (remainder) operator (not in FrogLang grammar) cli-reference.md: - parse: clarify default output is pretty-printed source, not an AST tree - check: document success output (`<file> is well-formed.`) and exit code - check: replace fictitious const/random modifiers with the real deterministic/injective modifiers - web: clarify port 5173 is the starting candidate, not guaranteed; actual port is printed at startup Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…rror with verified output - tutorial-1: replace "(coming soon)" placeholder with live link to tutorial-2 - tutorial-2: replace the implementer's reconstructed mismatch-signature error with the actual format produced by the engine (captured by running check on a deliberately-broken copy of OneTimeSecrecy.game) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
User-facing documentation for proof_frog web: launching, layout (file tree, editor, output, toolbar), editing features (syntax highlighting, Insert wizards enumerated from wizardConfig, file actions), validation buttons with CLI equivalents, hop inspection via Describe and Inlined Game, and the limitations of the web editor relative to the CLI's engine-introspection commands. Co-Authored-By: Claude Sonnet (subagent) <noreply@anthropic.com>
tutorial-2: - Add screenshot placeholders to Step 1, 2, 3 "Check it" sections (consistency with tutorial-1's pattern) execution-model: - Note that the compose syntax is a games:-block game step, not a free-standing expression - Tighten Initialize return-type wording: only Phase 2+ initializers may return values - Add the M[k] <- Type; map-entry sampling form to the Sampling section basics: - Replace stale "(coming soon)" reference to Execution Model with a live link now that the page exists primitives: - Add the Group parameter form to Parameter Forms (used by DH-style primitives) - Replace plain-text reference to Execution Model with a live link Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Reference for the .scheme file type: extends syntax, parameter forms (including primitives as parameters for generic constructions), requires preconditions, set/integer field assignments, method bodies, the this keyword and its proof-verification rewriting, the matching-modifiers rule between scheme and primitive, with worked examples (OTP, TriplingPRG, EncryptThenMAC, KEMDEM) drawn from current examples/Schemes/. Co-Authored-By: Claude Sonnet (subagent) <noreply@anthropic.com>
Reference for the .game file type: two-game requirement and naming conventions, Game block syntax with Initialize and state fields, oracle methods, export as, phases (drawn from SEMANTICS.md 5.5; previously undocumented in guide.md, real example from CCA.game), helper games as a special case, with worked examples drawn from current examples/Games/ including OneTimeSecrecy, CPA, and UniqueSampling. Co-Authored-By: Claude Sonnet (subagent) <noreply@anthropic.com>
Reference for the .proof file type: helpers section above proof:, the let:, assume:, lemma:, theorem:, and games: blocks, game step syntax (direct vs. composed-with-reduction), reductions in detail with the challenger keyword, the reduction parameter rule, and the standard four-step reduction pattern boxed from CLAUDE.md. Examples drawn from current examples/Proofs/ including OTPSecure, OTUCimpliesOTS, and TriplingPRGSecure. Co-Authored-By: Claude Sonnet (subagent) <noreply@anthropic.com>
VSCode extension installation (from VSIX, with build-from-source instructions) and feature list (syntax highlighting, diagnostics, go-to-definition, hover, outline, folding, F2 rename, completion and signature help, code lens for proof hops, proof hops tree view) — each enumerated from the corresponding file in proof_frog/lsp/. Future Emacs and JetBrains slots noted with eglot/ lsp-mode and LSP4IJ pointers. Adding-a-new-editor paragraph for LSP-aware editors. Co-Authored-By: Claude Sonnet (subagent) <noreply@anthropic.com>
- Trim from ~1276 to ~700 words: fold syntax highlighting into Layout's editor pane bullet, flatten the wizard list to a single sentence (the file-type filtering note replaces the misleading "Always-available wizards" heading), collapse file actions and limitations sections, condense launching prose - Replace the implementation-specific "up to port 5272" upper bound with the user-facing "scans upward for the next available port" wording (consistent with cli-reference.md) - Tone down the Inlined Game description: drop the unverified "split-pane diff against the adjacent step" claim; describe what the modal actually does Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Six sections distinguishing capability limits from trust limits (which live on researchers/soundness): things FrogLang does not model (SEMANTICS.md sec 10), capabilities deliberately lacking, capabilities the engine aspires to but is weak at (verified ENGINE_LIMITATION_DETECTORS from diagnostics.py plus higher-level soft spots), what kinds of proofs do work well, and how to report a limitation. Co-Authored-By: Claude Sonnet (subagent) <noreply@anthropic.com>
Symptom-keyed reference covering install problems, parse errors, type errors, proof errors, web editor problems, and "my proof should work but doesn't" diagnostics. Each entry follows a Symptom/Likely cause/Fix/See also template with verbatim error wording captured from proof_frog/diagnostics.py, semantic_analysis.py, proof_engine.py, and frog_parser.py. Co-Authored-By: Claude Sonnet (subagent) <noreply@anthropic.com>
Replace four plain-text references with live {% link %} tags, per the
combined schemes/games/proofs review:
- schemes.md: "Basics page" link in the Scheme block section
- proofs.md: "games file-type reference" link in the helpers section
- proofs.md: "Basics language reference page" link in the let: section
- proofs.md: "CLI reference page" link in the --skip-lemmas callout
(the one explicitly flagged by the implementer as uncertain-path)
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
First reduction proof in the manual, walkthrough of examples/joy/Proofs/Ch2/ChainedEncryptionSecure.proof: the scheme, the proof structure (two reductions R1 and R2, each applying the four-step pattern), the four-step reduction pattern walked through verbatim on one hop, and R1 in detail with the reduction parameter rule explained. Introduction of reductions in narrative form for a student who has just finished Tutorial Part 2. Co-Authored-By: Claude Sonnet (subagent) <noreply@anthropic.com>
User-facing model of the canonicalization pipeline: overview of what prove does, topic-organized subsections covering what the engine simplifies automatically (inlining, bitstring/ModInt/group algebra, sample merge/split, random functions, deterministic/injective annotations, code simplification, SMT-assisted branch comparison), catalog of load-bearing helper games currently in examples/Games/Misc/ (UniqueSampling, HashOnUniform, ROMProgramming, RandomTargetGuessing), the four-step reduction pattern pointer, what the engine does not do, and a diagnosing-a-failing-hop recipe. Drawn from extras/docs/transforms/ per-transform docs and SEMANTICS.md. Co-Authored-By: Claude Sonnet (subagent) <noreply@anthropic.com>
Motivation, the three tasks of a game-hopping proof (ProofFrog focuses on task 1), design choices (AST-level, canonicalization, user-supplies-reductions, C/Java-like syntax), positioning relative to EasyCrypt/CryptoVerif and other computer-aided cryptography tools, and what ProofFrog is and isn't with the lineage and acknowledgements. Drawn from design.md and the eprint (eprint_source/conference_101719.tex sections 1 and 2). Co-Authored-By: Claude Sonnet (subagent) <noreply@anthropic.com>
- §4 four-step pattern: replace 3-bullet rendition with a 4-entry numbered list matching the actual games:-block structure (G_before, Side1 compose R, Side2 compose R, G_after) - §6 "Diagnosing a failing hop": add #prove anchor to the cli-reference link - §2 ModInt subsection: remove inaccurate examples/Proofs/PRF/ pointer (the only PRF proof uses a BitString-based PRF, not modular arithmetic) - §2 deterministic subsection: replace the inaccurate "PRF proofs rely on DeduplicateDeterministicCalls" claim with a correct generic description Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Honest negative soundness story: ProofFrog has no formal soundness proof. Seven sections: the summary (treat as proof-finding aid, not certifier), the formal claim stated in terms of interchangeability, the full trust base (parser, type checker, transformation pipeline, Z3, SymPy, Python runtime), what is not claimed, mitigations a careful user can apply (small hops, prove -v inspection, cross-check with pen-and-paper, reporting suspicious validations), a calibrated comparison to EasyCrypt and CryptoVerif, and known soundness issues (no dedicated label on the issue tracker yet). Co-Authored-By: Claude Sonnet (subagent) <noreply@anthropic.com>
Multi-primitive worked example based on the modernized asymmetric-ladder files at examples/asymmetric-ladder/kemdem/. Walks through Hyb-is-CPA.proof's three- reduction proof (R1 KEM-CPA real->ideal, R2 SymEnc OTS left->right, R3 KEM-CPA ideal->real) as a pedagogical graduation from the single-primitive Chained Encryption example: multi-primitive composition, reductions to the same assumption in opposite directions, and generic-construction parameter handling. Co-Authored-By: Claude Sonnet (subagent) <noreply@anthropic.com>
- worked-examples/index: intro + links to chained-encryption and kemdem-cpa - language-reference/index: intro + cheat-sheet table linking all six language-reference pages Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Restructured from the hacs-2026/vibe/ event handout as a researcher-facing page: explicit framing as a research-and-experimentation tool (not a student workflow), setup of the MCP server and Claude Code configuration, what works well, what does not (hallucinated helpers, silent drift, premature success claims), soundness considerations (vibe-coding does not lower the trust load), and pointers to the original HACS 2026 demo artifacts which stay on disk. Co-Authored-By: Claude Sonnet (subagent) <noreply@anthropic.com>
… links
After all the new pages exist on the branch, sweep through and replace every
"(coming soon)" / "(not yet available)" / "(not yet published)" placeholder
with the actual {% link %} tag now that the target pages have landed:
- manual/installation: Tutorial Part 1 link
- manual/cli-reference: Engine Internals link (intro-commands paragraph)
- manual/tutorial-2-otp-ots: Chained Encryption + Transformations links
- manual/editor-plugins: Engine Internals link (3 occurrences)
- manual/limitations: Soundness link, Transformations link
- manual/transformations: Soundness link (helper-game callout)
- manual/web-editor: Engine Internals link
- manual/worked-examples/chained-encryption: Transformations + KEMDEM-CPA links
- researchers/vibe-coding: Engine Internals link
Also fix a broken {% link %} tag in manual/limitations.md that was split across
two lines (Jekyll tolerated it but the line break was fragile).
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Rewrites manual/worked-examples/kemdem-cpa.md so it is based on examples/Proofs/PubEnc/KEMDEMCPA.proof (and its associated primitive, scheme, and game files) instead of the asymmetric-ladder variant. - Scheme and instance renamed from Hyb/H to KEMDEM/KD throughout. - Five reductions instead of three: the in-repo OneTimeSecrecy game uses E.KeyGen() rather than uniform sampling, so the proof now includes two KeyUniformity hops (one forward, one back) bracketing the OTS hop. - Six conceptual games (Game_0..Game_5) described narratively; no explicit intermediate Game definitions, matching the proof file. - Primitive and game definitions updated: NonNullableSymEnc (total Dec), KEM.Encaps returning [SharedSecret, Ciphertext], CPAKEM with Real/Random sides and Initialize returning pk, OneTimeSecrecy with Eavesdrop oracle, new KeyUniformity game, PubKeyEnc primitive, and CPA game with Challenge oracle. - All file paths and Try-it commands updated to the examples/ directory layout (Primitives/, Games/, Schemes/PubEnc/, Proofs/PubEnc/). - Section 1 now explains why the key-uniformity assumption is needed instead of the "sidestepping" framing. - Closing Proof Ladders note preserved, with a brief mention that that version uses the alternative OTS formulation to collapse the five reductions down to three. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Reflect the examples repo rename where single-instance assumptions (formerly OneTimeDDH, OneTimeCDH, OneTimeHashedDDH) now get the simpler names (DDH, CDH, HashedDDH) and multi-challenge variants get the MultiChal suffix (DDHMultiChal, HashedDDHMultiChal). Updates all proof and game links in examples.md, canonicalization.md, and language-reference/games.md. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Update installation guide and tutorial to recommend `proof_frog download-examples` as the primary way to obtain examples, replacing `git clone`. Add download-examples to the CLI reference with full documentation of --ref and --force options. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-authored-by: Claude Opus 4.6 (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.
No description provided.