Updates due to example renaming

Author: dstebila

examples.md

@@ -27,7 +27,7 @@ Checking your first proof is as easy as:
 ```bash
 pip install proof_frog
 git clone https://github.com/ProofFrog/examples
-proof_frog prove examples/Proofs/PubEnc/KEMDEMCPA.proof
+proof_frog prove examples/Proofs/PubKeyEnc/HybridKEMDEM_INDCPA_MultiChal.proof
 ```
 
 See the [installation instructions]({% link manual/installation.md %}) for details.

index.md

@@ -73,7 +73,7 @@ E.Ciphertext Eavesdrop(E.Message mL, E.Message mR) {
 ```
 
 Real-proof pointer: every proof in the distribution relies on inlining.
-[`examples/Proofs/PRG/TriplingPRGSecure.proof`](https://github.com/ProofFrog/examples/blob/main/Proofs/PRG/TriplingPRGSecure.proof) is a clean illustration -- the
+[`examples/Proofs/PRG/TriplingPRG_PRGSecurity.proof`](https://github.com/ProofFrog/examples/blob/main/Proofs/PRG/TriplingPRG_PRGSecurity.proof) is a clean illustration -- the
 `TriplingPRG` scheme composes calls to an underlying `PRG`, and those calls are inlined
 before the PRG reduction hops.
 
@@ -114,7 +114,7 @@ return u;
 slice boundaries align with the component widths, saving a round-trip through
 concatenation and slicing.
 
-Real-proof pointer: [`examples/Proofs/SymEnc/SymEncPRFCPA$.proof`](https://github.com/ProofFrog/examples/blob/main/Proofs/SymEnc/SymEncPRFCPA%24.proof) -- the final
+Real-proof pointer: [`examples/Proofs/SymEnc/SymEncPRF_INDCPA$_MultiChal.proof`](https://github.com/ProofFrog/examples/blob/main/Proofs/SymEnc/SymEncPRF_INDCPA%24_MultiChal.proof) -- the final
 merge of two independent uniform samples into the CPA$ random game relies on XOR
 absorption after the PRF is replaced by a random function.
 
@@ -146,7 +146,7 @@ ModInt<q> u <- ModInt<q>;
 return u;
 ```
 
-Real-proof pointer: [`examples/Proofs/SymEnc/ModOTPSecure.proof`](https://github.com/ProofFrog/examples/blob/main/Proofs/SymEnc/ModOTPSecure.proof) uses the ModInt
+Real-proof pointer: [`examples/Proofs/SymEnc/ModOTP_INDOT.proof`](https://github.com/ProofFrog/examples/blob/main/Proofs/SymEnc/ModOTP_INDOT.proof) uses the ModInt
 one-time-pad argument directly.
 
 {: .note }
@@ -183,7 +183,7 @@ return (h ^ b) * (h ^ c);
 return G.generator ^ (a * b + a * c);
 ```
 
-Real-proof pointer: [`examples/Proofs/PubEnc/ElGamalCPA.proof`](https://github.com/ProofFrog/examples/blob/main/Proofs/PubEnc/ElGamalCPA.proof) uses the
+Real-proof pointer: [`examples/Proofs/PubKeyEnc/ElGamal_INDCPA_MultiChal.proof`](https://github.com/ProofFrog/examples/blob/main/Proofs/PubKeyEnc/ElGamal_INDCPA_MultiChal.proof) uses the
 group masking move (the DDH `Right` game replaces `pk ^ r` with a random group element `c`,
 and the uniform-absorbs rule fires to simplify `mL * c` to `c`, making the ciphertext
 independent of the message).
@@ -230,7 +230,7 @@ BitString<m> z_1 <- BitString<m>;
 return [z_0, z_1];
 ```
 
-Real-proof pointer: [`examples/Proofs/PRG/TriplingPRGSecure.proof`](https://github.com/ProofFrog/examples/blob/main/Proofs/PRG/TriplingPRGSecure.proof) uses sample split
+Real-proof pointer: [`examples/Proofs/PRG/TriplingPRG_PRGSecurity.proof`](https://github.com/ProofFrog/examples/blob/main/Proofs/PRG/TriplingPRG_PRGSecurity.proof) uses sample split
 to decompose a single PRG output into its two halves (each half is then used
 independently as a new seed or output value, and the split enables the per-component
 uniform reasoning).
@@ -272,7 +272,7 @@ BitString<n> r <-uniq[RF.domain] BitString<n>;
 BitString<m> z <- BitString<m>;
 ```
 
-Real-proof pointer: [`examples/Proofs/PubEnc/HashedElGamalCPAROM.proof`](https://github.com/ProofFrog/examples/blob/main/Proofs/PubEnc/HashedElGamalCPAROM.proof) -- the proof
+Real-proof pointer: [`examples/Proofs/PubKeyEnc/HashedElGamal_INDCPA_ROM_MultiChal.proof`](https://github.com/ProofFrog/examples/blob/main/Proofs/PubKeyEnc/HashedElGamal_INDCPA_ROM_MultiChal.proof) -- the proof
 uses `FreshInputRFToUniform` (after the DDH hop places a uniform group element `c` in
 the exclusion set) to collapse `H(c)` into a fresh uniform bitstring, which then masks
 the message via XOR.
@@ -370,7 +370,7 @@ return k + m;
 Real-proof pointer: dead code elimination is exercised in almost every proof. The
 elimination of the random-function field after `UniqueRFSimplification` replaces all
 its calls with uniform samples is a good representative case; see
-[`examples/Proofs/SymEnc/SymEncPRFCPA$.proof`](https://github.com/ProofFrog/examples/blob/main/Proofs/SymEnc/SymEncPRFCPA%24.proof).
+[`examples/Proofs/SymEnc/SymEncPRF_INDCPA$_MultiChal.proof`](https://github.com/ProofFrog/examples/blob/main/Proofs/SymEnc/SymEncPRF_INDCPA%24_MultiChal.proof).
 
 {: .note }
 **If a branch is not being eliminated:** The engine folds `if (true)` and `if (false)`
@@ -396,7 +396,7 @@ The `RemoveUnreachable` pass also uses Z3 to determine whether a statement after
 guarded return is reachable, allowing dead branches under non-trivially-false conditions
 to be removed.
 
-Real-proof pointer: [`examples/Proofs/SymEnc/EncryptThenMACCCA.proof`](https://github.com/ProofFrog/examples/blob/main/Proofs/SymEnc/EncryptThenMACCCA.proof) uses phased
+Real-proof pointer: [`examples/Proofs/SymEnc/EncryptThenMAC_INDCCA_MultiChal.proof`](https://github.com/ProofFrog/examples/blob/main/Proofs/SymEnc/EncryptThenMAC_INDCCA_MultiChal.proof) uses phased
 games with guard conditions that require Z3 to confirm equivalence after inlining.
 
 {: .note }
@@ -413,7 +413,7 @@ already in the simplified form.
 Some probabilistic facts cannot be derived purely from program structure: they require
 an external statistical argument (typically a birthday bound or a random oracle
 property). ProofFrog handles these via *helper games* -- ordinary `.game` files in
-`examples/Games/Misc/` that state a statistical equivalence as a security assumption.
+`examples/Games/Helpers/` that state a statistical equivalence as a security assumption.
 The user invokes a helper game as an assumption hop in the same way as any other
 assumption; the difference is that the helper game is not a hardness assumption but a
 statistical argument that the proof author vouches for.
@@ -422,7 +422,7 @@ Four helper games currently in the distribution are:
 
 ### UniqueSampling
 
-**File:** [`examples/Games/Misc/UniqueSampling.game`](https://github.com/ProofFrog/examples/blob/main/Games/Misc/UniqueSampling.game)
+**File:** [`examples/Games/Helpers/Probability/UniqueSampling.game`](https://github.com/ProofFrog/examples/blob/main/Games/Helpers/Probability/UniqueSampling.game)
 
 **What it states:** Sampling uniformly with replacement from a set `S` is
 indistinguishable from sampling without replacement (exclusion sampling, `<-uniq`).
@@ -447,12 +447,12 @@ UniqueSampling.NoReplacement compose R_Uniq against Adversary; // by UniqueSampl
 G_after against Adversary;                               // interchangeability
 ```
 
-Real-proof pointer: used in [`examples/Proofs/SymEnc/SymEncPRFCPA$.proof`](https://github.com/ProofFrog/examples/blob/main/Proofs/SymEnc/SymEncPRFCPA%24.proof),
-[`examples/Proofs/PubEnc/HashedElGamalCPAROM.proof`](https://github.com/ProofFrog/examples/blob/main/Proofs/PubEnc/HashedElGamalCPAROM.proof), [`examples/Proofs/Group/DDHMultiChalImpliesHashedDDHMultiChal.proof`](https://github.com/ProofFrog/examples/blob/main/Proofs/Group/DDHMultiChalImpliesHashedDDHMultiChal.proof).
+Real-proof pointer: used in [`examples/Proofs/SymEnc/SymEncPRF_INDCPA$_MultiChal.proof`](https://github.com/ProofFrog/examples/blob/main/Proofs/SymEnc/SymEncPRF_INDCPA%24_MultiChal.proof),
+[`examples/Proofs/PubKeyEnc/HashedElGamal_INDCPA_ROM_MultiChal.proof`](https://github.com/ProofFrog/examples/blob/main/Proofs/PubKeyEnc/HashedElGamal_INDCPA_ROM_MultiChal.proof), [`examples/Proofs/Group/DDHMultiChal_implies_HashedDDHMultiChal.proof`](https://github.com/ProofFrog/examples/blob/main/Proofs/Group/DDHMultiChal_implies_HashedDDHMultiChal.proof).
 
-### HashOnUniform
+### Regularity
 
-**File:** [`examples/Games/Misc/HashOnUniform.game`](https://github.com/ProofFrog/examples/blob/main/Games/Misc/HashOnUniform.game)
+**File:** [`examples/Games/Hash/Regularity.game`](https://github.com/ProofFrog/examples/blob/main/Games/Hash/Regularity.game)
 
 **What it states:** Applying a hash function `H : D -> BitString<n>` to a uniformly
 sampled input from `D` is indistinguishable from sampling `BitString<n>` uniformly.
@@ -465,11 +465,11 @@ block without sampling, so not a random oracle), and the proof requires treating
 output of `H` on a uniform input as uniformly random. This is the standard-model
 counterpart to what `FreshInputRFToUniform` does automatically in the ROM.
 
-Real-proof pointer: used in [`examples/Proofs/Group/DDHImpliesHashedDDH.proof`](https://github.com/ProofFrog/examples/blob/main/Proofs/Group/DDHImpliesHashedDDH.proof).
+Real-proof pointer: used in [`examples/Proofs/Group/DDH_implies_HashedDDH.proof`](https://github.com/ProofFrog/examples/blob/main/Proofs/Group/DDH_implies_HashedDDH.proof).
 
 ### ROMProgramming
 
-**File:** [`examples/Games/Misc/ROMProgramming.game`](https://github.com/ProofFrog/examples/blob/main/Games/Misc/ROMProgramming.game)
+**File:** [`examples/Games/Helpers/Probability/ROMProgramming.game`](https://github.com/ProofFrog/examples/blob/main/Games/Helpers/Probability/ROMProgramming.game)
 
 **What it states:** Programming a random function at a single target point with a fresh
 uniform value is statistically equivalent to evaluating it naturally. The `Natural` game
@@ -482,11 +482,11 @@ challenge point -- replacing `H(target)` with an independently sampled value so
 challenge ciphertext becomes statistically independent of the adversary's hash queries.
 This is a standard technique in ROM proofs.
 
-Real-proof pointer: used in [`examples/Proofs/Group/CDHImpliesHashedDDH.proof`](https://github.com/ProofFrog/examples/blob/main/Proofs/Group/CDHImpliesHashedDDH.proof).
+Real-proof pointer: used in [`examples/Proofs/Group/CDH_implies_HashedDDH.proof`](https://github.com/ProofFrog/examples/blob/main/Proofs/Group/CDH_implies_HashedDDH.proof).
 
 ### RandomTargetGuessing
 
-**File:** [`examples/Games/Misc/RandomTargetGuessing.game`](https://github.com/ProofFrog/examples/blob/main/Games/Misc/RandomTargetGuessing.game)
+**File:** [`examples/Games/Helpers/Probability/RandomTargetGuessing.game`](https://github.com/ProofFrog/examples/blob/main/Games/Helpers/Probability/RandomTargetGuessing.game)
 
 **What it states:** Comparing an adversary-supplied value against a hidden, uniformly
 sampled target is indistinguishable from always returning false. The `Real` game samples
@@ -498,7 +498,7 @@ game always returns `false`. Any adversary distinguishes the two with advantage
 uniform value, and the proof argues that such a guess succeeds only with negligible
 probability.
 
-Real-proof pointer: used in [`examples/Proofs/Group/DDHImpliesCDH.proof`](https://github.com/ProofFrog/examples/blob/main/Proofs/Group/DDHImpliesCDH.proof).
+Real-proof pointer: used in [`examples/Proofs/Group/DDH_implies_CDH.proof`](https://github.com/ProofFrog/examples/blob/main/Proofs/Group/DDH_implies_CDH.proof).
 
 {: .important }
 Using a helper game adds to the trust base -- see the [Soundness]({% link researchers/soundness.md %}) page in the For Researchers area.
@@ -565,7 +565,7 @@ fired asymmetrically).
 
 - *Add a helper assumption.* If the gap corresponds to a statistical fact (birthday
   bound, hash-on-uniform, ROM programming), introduce the appropriate helper game from
-  `examples/Games/Misc/` and use the four-step reduction pattern to cross the gap.
+  `examples/Games/Helpers/` and use the four-step reduction pattern to cross the gap.
 
 - *Restructure existing code.* If the canonical forms differ only in ordering --
   operand order in a concatenation, field declaration order, branch order in an

manual/canonicalization.md

@@ -177,7 +177,7 @@ python -m proof_frog prove -v examples/joy/Proofs/Ch2/OTPSecure.proof
 python -m proof_frog prove -vv examples/joy/Proofs/Ch2/OTPSecure.proof
 
 # Verify a PRG security proof, skipping lemma re-verification
-python -m proof_frog prove --skip-lemmas examples/Proofs/PRG/CounterPRGSecure.proof
+python -m proof_frog prove --skip-lemmas examples/Proofs/PRG/CounterPRG_PRGSecurity.proof
 ```
 
 ### Common Errors

manual/cli-reference.md

@@ -334,12 +334,12 @@ import 'relative/path/to/File.primitive';
 
 **Paths are file-relative**: the path is resolved relative to the directory containing the importing file, not relative to the directory where the CLI is invoked.
 
-**Example.** The proof `examples/Proofs/SymEnc/OTUCimpliesOTS.proof` imports:
+**Example.** The proof `examples/Proofs/SymEnc/INDOT$_implies_INDOT.proof` imports:
 
 ```prooffrog
 import '../../Primitives/SymEnc.primitive';
-import '../../Games/SymEnc/OneTimeSecrecy.game';
-import '../../Games/SymEnc/OneTimeUniformCiphertexts.game';
+import '../../Games/SymEnc/INDOT.game';
+import '../../Games/SymEnc/INDOT$.game';
 ```
 
 From `examples/Proofs/SymEnc/`, `../..` navigates up to `examples/`, and the paths then descend into `Primitives/` and `Games/SymEnc/`.

manual/language-reference/basics.md

@@ -29,8 +29,7 @@ There is no enforced naming convention for the two sides. Common choices from th
 |---|---|
 | `Left` / `Right` | General indistinguishability |
 | `Real` / `Random` | PRG, PRF security |
-| `Real` / `Fake` | Various simulation-based definitions |
-| `Real` / `Ideal` | Composable security |
+| `Real` / `Ideal` | Simulation-based security, correctness |
 
 Pick names that make sense for the property in question, and consider how the security property is stated in the relevant literature. Neither side is "preferred": your game hopping proof can go from left to right or right to left; all that matters is that in a proof's `games:` list, the sequence must start on one side and end on the other.
 
@@ -127,29 +126,29 @@ ProofFrog's convention, following Joy of Cryptography, allows all game oracles (
 The last line of every `.game` file is an `export as` statement that assigns a name to the security property:
 
 ```prooffrog
-export as OneTimeSecrecy;
+export as INDOT;
 ```
 
 This name is how the rest of the tool chain refers to the security property. In a proof file, after importing the game file, you write:
 
-- `OneTimeSecrecy(E).Left` — the left game instantiated with scheme `E`
-- `OneTimeSecrecy(E).Right` — the right game instantiated with `E`
-- `OneTimeSecrecy(E).Adversary` — the type of adversary for this property
+- `INDOT(E).Left` — the left game instantiated with scheme `E`
+- `INDOT(E).Right` — the right game instantiated with `E`
+- `INDOT(E).Adversary` — the type of adversary for this property
 
-The `export as` name is also what appears in the proof's `theorem:` and `assume:` sections. The name must be a valid identifier; by convention it matches the file name (e.g., `OneTimeSecrecy.game` exports `OneTimeSecrecy`).
+The `export as` name is also what appears in the proof's `theorem:` and `assume:` sections. The name must be a valid identifier; by convention it matches the file name (e.g., `INDOT.game` exports `INDOT`).
 
 ---
 
 ## Helper games as a special case
 
-Not every `.game` file has to define a *cryptographic security property*. Game files can be used to capture facts that ProofFrog's engine is not able to reason about, such as mathematical properties, statistical claims, or additional program equivalence properties. The [`Games/Misc/`](https://github.com/ProofFrog/examples/tree/main/Games/Misc) directory contains several *helper games*.
+Not every `.game` file has to define a *cryptographic security property*. Game files can be used to capture facts that ProofFrog's engine is not able to reason about, such as mathematical properties, statistical claims, or additional program equivalence properties. The [`Games/Helpers/`](https://github.com/ProofFrog/examples/tree/main/Games/Helpers) directory contains several *helper games*.
 
 Here are some helper games that capture mathematical facts:
 
-- **`UniqueSampling`** ([`UniqueSampling.game`](https://github.com/ProofFrog/examples/blob/main/Games/Misc/UniqueSampling.game)): sampling uniformly from a set `S` is indistinguishable from sampling from `S` with exclusion of a bookkeeping set (rejection sampling).
-- **`HashOnUniform`** ([`HashOnUniform.game`](https://github.com/ProofFrog/examples/blob/main/Games/Misc/HashOnUniform.game)): applying a hash to a uniformly random input yields a uniform output.
-- **`RandomTargetGuessing`** ([`RandomTargetGuessing.game`](https://github.com/ProofFrog/examples/blob/main/Games/Misc/RandomTargetGuessing.game)): guessing a random target is no easier than guessing any fixed value.
-- **`ROMProgramming`** ([`ROMProgramming.game`](https://github.com/ProofFrog/examples/blob/main/Games/Misc/ROMProgramming.game)): facts about programming random oracles.
+- **`UniqueSampling`** ([`UniqueSampling.game`](https://github.com/ProofFrog/examples/blob/main/Games/Helpers/Probability/UniqueSampling.game)): sampling uniformly from a set `S` is indistinguishable from sampling from `S` with exclusion of a bookkeeping set (rejection sampling).
+- **`Regularity`** ([`Regularity.game`](https://github.com/ProofFrog/examples/blob/main/Games/Hash/Regularity.game)): applying a hash to a uniformly random input yields a uniform output.
+- **`RandomTargetGuessing`** ([`RandomTargetGuessing.game`](https://github.com/ProofFrog/examples/blob/main/Games/Helpers/Probability/RandomTargetGuessing.game)): guessing a random target is no easier than guessing any fixed value.
+- **`ROMProgramming`** ([`ROMProgramming.game`](https://github.com/ProofFrog/examples/blob/main/Games/Helpers/Probability/ROMProgramming.game)): facts about programming random oracles.
 
 Helper games are structurally identical to security-property games — they are pairs of games with `export as` — but they appear in a proof's `assume:` block rather than the `theorem:` block. They can be assumed freely because they hold unconditionally or statistically, not by reduction to a computational hardness assumption. For the full catalog of available helper games and when to use each, see the [Canonicalization]({% link manual/canonicalization.md %}) page.
 
@@ -161,7 +160,7 @@ When a mathematical fact is encoded via a helper game and used to bridge a step
 
 ### One-time secrecy
 
-[`Games/SymEnc/OneTimeSecrecy.game`](https://github.com/ProofFrog/examples/blob/main/Games/SymEnc/OneTimeSecrecy.game)
+[`Games/SymEnc/INDOT.game`](https://github.com/ProofFrog/examples/blob/main/Games/SymEnc/INDOT.game)
 
 ```prooffrog
 import '../../Primitives/SymEnc.primitive';
@@ -182,14 +181,14 @@ Game Right(SymEnc E) {
     }
 }
 
-export as OneTimeSecrecy;
+export as INDOT;
 ```
 
 The adversary submits two equal-length messages and receives an encryption of either the left or the right one. A fresh key is sampled per query, so no key reuse is implied. One-time secrecy holds if the adversary cannot tell which message was encrypted.
 
 ### CPA security (stateful game)
 
-[`Games/SymEnc/CPA.game`](https://github.com/ProofFrog/examples/blob/main/Games/SymEnc/CPA.game)
+[`Games/SymEnc/INDCPA_MultiChal.game`](https://github.com/ProofFrog/examples/blob/main/Games/SymEnc/INDCPA_MultiChal.game)
 
 ```prooffrog
 import '../../Primitives/SymEnc.primitive';
@@ -214,14 +213,14 @@ Game Right(SymEnc E) {
     }
 }
 
-export as CPA;
+export as INDCPA_MultiChal;
 ```
 
 Like one-time secrecy, but the key is sampled once in `Initialize` and reused across all oracle calls. The state field `k` persists from one `Eavesdrop` call to the next, modelling the chosen-plaintext attack setting where the adversary may request many encryptions under the same key.
 
 ### A helper game
 
-[`Games/Misc/UniqueSampling.game`](https://github.com/ProofFrog/examples/blob/main/Games/Misc/UniqueSampling.game)
+[`Games/Helpers/Probability/UniqueSampling.game`](https://github.com/ProofFrog/examples/blob/main/Games/Helpers/Probability/UniqueSampling.game)
 
 ```prooffrog
 // Assumption: sampling uniformly from a set S is indistinguishable from