Language Reference
FrogLang has four file types — primitives, schemes, games, and proofs — and a shared syntactic and semantic layer beneath them. This section is organized to match that structure.
- Basics covers the syntactic layer that every file type uses: types, expressions and operators, sampling, statements, and imports.
- Execution Model covers the operational layer — what it means for an adversary to interact with a game, how state persists, what interchangeability means formally, and how composition works.
- The four file-type pages below cover what is specific to each kind of file.
The tutorials and worked examples are a good starting place if you are new to ProofFrog.
| Reference Page | Topic |
|---|---|
| Basics | Types, operators, sampling forms, statements, imports |
| Execution Model | Adversary model, game lifecycle, state, non-determinism, composition, interchangeability |
| Primitives | The .primitive file type: Primitive block, parameters, set fields, method signatures, deterministic/injective modifiers |
| Schemes | The .scheme file type: extends, parameter forms, requires, field assignments, method bodies, the this keyword, matching-modifier rule |
| Games | The .game file type: two-game requirement, Initialize and state, oracle methods, export as, helper games |
| Proofs | The .proof file type: let:, assume:, lemma:, theorem:, games: blocks, reductions, the reduction parameter rule, the four-step reduction pattern |