Hybrid.lean🔗

Tier 2 · definitions used by the computational proof 1 headline theorem depend on it 3 of 263 lines trusted trust banner B3, trusted in part source ↗

Read the definitions shown. Only the declarations that the headline statements use are shown, with the namespace, section, open and variable commands needed to read them. The collapsed runs are theorems, which Lean checks, and definitions that no headline statement uses.

Hybrid games for ACD19 Thm 5: shared state and non-encrypting oracles

Trusted in part. The theorems of Computational/Theorems/ use only isLookaheadHop from this file: read it. Everything else here is checked by Lean. See Computational/docs/TRUSTED_BASE.md.

Shared hybrid state (Slot, HState, HSt, Params, Kind, SpecialOps), state combinators (onH, getH, modifyH, sampleH), lazy chain generation (chainFrom, genStep, genN, genUpTo, reveal), decryption (kind, decIdx), corruption oracles (senderKey, corruptSenderH, corruptReceiverH), and hybrid parameters (hOut, hInit, DG, hp, isLookaheadHop) for the proof of ACD19 Thm 5 (including lookahead mode, DEV-FS14).

@[expose] public section

open OracleComp OracleSpec ENNReal

namespace CryptoGames.FSAEAD.Thm5

variable {CK MK AD M C : Type}

9 declarations not shown (lines 36–110): theorems, which Lean checks, or definitions that no headline statement uses

CryptoGames.FSAEAD.Thm5.chainFrom, CryptoGames.FSAEAD.Thm5.Slot.unknown, CryptoGames.FSAEAD.Thm5.Slot, CryptoGames.FSAEAD.Thm5.Slot.seed, CryptoGames.FSAEAD.Thm5.Slot.mat, CryptoGames.FSAEAD.Thm5.HState.b, CryptoGames.FSAEAD.Thm5.HState.ended, CryptoGames.FSAEAD.Thm5.HState.lf, CryptoGames.FSAEAD.Thm5.HState.corrKey, CryptoGames.FSAEAD.Thm5.HState.receiverIdx, CryptoGames.FSAEAD.Thm5.HState.lastSentIdx, CryptoGames.FSAEAD.Thm5.HState.skipped, CryptoGames.FSAEAD.Thm5.HState.win, CryptoGames.FSAEAD.Thm5.HState, CryptoGames.FSAEAD.Thm5.HState.keys, CryptoGames.FSAEAD.Thm5.HState.senderCorruptedAt, CryptoGames.FSAEAD.Thm5.HState.challengesInTransit, CryptoGames.FSAEAD.Thm5.HState.inTransit, CryptoGames.FSAEAD.Thm5.HState.isCompromised, CryptoGames.FSAEAD.Thm5.HState.removeFromTransit, CryptoGames.FSAEAD.Thm5.HSt, CryptoGames.FSAEAD.Thm5.SpecialOps.enc, CryptoGames.FSAEAD.Thm5.SpecialOps.dec, CryptoGames.FSAEAD.Thm5.SpecialOps, CryptoGames.FSAEAD.Thm5.Params, CryptoGames.FSAEAD.Thm5.Params.la, CryptoGames.FSAEAD.Thm5.Params.t, CryptoGames.FSAEAD.Thm5.Params.j, CryptoGames.FSAEAD.Thm5.Kind.ideal, CryptoGames.FSAEAD.Thm5.Kind.special, CryptoGames.FSAEAD.Thm5.Kind, CryptoGames.FSAEAD.Thm5.Kind.real

notation "St"L119 ↗#

local notation "St" => HSt CK MK AD M C

notation "HS"L120 ↗#

local notation "HS" => HState CK MK AD M C

14 declarations not shown (lines 122–230): theorems, which Lean checks, or definitions that no headline statement uses

CryptoGames.FSAEAD.Thm5.onH, CryptoGames.FSAEAD.Thm5.getH, CryptoGames.FSAEAD.Thm5.modifyH, CryptoGames.FSAEAD.Thm5.sampleH, CryptoGames.FSAEAD.Thm5.genStep, CryptoGames.FSAEAD.Thm5.genN, CryptoGames.FSAEAD.Thm5.genUpTo, CryptoGames.FSAEAD.Thm5.reveal, CryptoGames.FSAEAD.Thm5.kind, CryptoGames.FSAEAD.Thm5.decIdx, CryptoGames.FSAEAD.Thm5.newSkipped, CryptoGames.FSAEAD.Thm5.senderKey, CryptoGames.FSAEAD.Thm5.corruptSenderH, CryptoGames.FSAEAD.Thm5.corruptReceiverH

section Games

variable [SampleableType MK] [SampleableType CK] [SampleableType C]
  [DecidableEq AD] [DecidableEq M] [DecidableEq C]
  (ae : AEADScheme MK (ℕ × AD) M C) (G : ℕ → PRGScheme CK (CK × MK)) (maxSkip : ℕ)

4 declarations not shown (lines 242–255): theorems, which Lean checks, or definitions that no headline statement uses

CryptoGames.FSAEAD.Thm5.hOut, CryptoGames.FSAEAD.Thm5.hInit, CryptoGames.FSAEAD.Thm5.DG, CryptoGames.FSAEAD.Thm5.hp

def isLookaheadHopL257–259 ↗#

Hybrid step j of the sum: hop j / 2 of the main chain (j even) or of the lookahead chain (j odd).

def isLookaheadHop (j : ℕ) : Bool := j % 2 == 1

end Games

end CryptoGames.FSAEAD.Thm5