feat(classes): add cryptographic primitives#6
Conversation
…TComputable) Add foundational infrastructure for cryptographic formalization: - BitEncodable: specification-level typeclass for encoding types as bit strings, with instances for Unit, List Bool, Option, and Prod. - unpair: left inverse of pair, with roundtrip proof. - PPTComputable: predicate asserting a randomized function (List Bool → PMF (List Bool)) is computable by a PPT NTM, bridging NTM output distributions to Mathlib's PMF via ENNReal. - Make pair_nil_eq and pair_cons_eq public @[simp] lemmas.
| | none => [false] | ||
| | some x => true :: x | ||
| decode | ||
| | [] => none |
| @@ -17,14 +17,38 @@ search-problem classes. | |||
| def pair (x y : List Bool) : List Bool := | |||
There was a problem hiding this comment.
I'm not sure I follow why you need pair/unpair, rather than defining BitEncodable on products of bitstrings
|
|
||
| ## Main definitions | ||
|
|
||
| - `PPTComputable` — a randomized function is PPT-computable if there exists a PPT NTM |
There was a problem hiding this comment.
The way we define PTMs here is as NTMs with certain properties. That said, maybe we should change the PTM definition to be a PTM which gets spawned with a worktape with a bunch of random bits on it.
There was a problem hiding this comment.
Yeah, I think defining a PTM as an NTM is non-standard; defining it as a TM with an extra random tape is better.
| open Complexity | ||
|
|
||
| /-- A randomized function `f : List Bool → PMF (List Bool)` is **PPT-computable** | ||
| if there exists a PPT NTM whose output distribution matches `f` on all inputs. |
| and outputs `y`. The time bound `T` must be polynomial: `T =O (· ^ d)` | ||
| for some degree `d`. -/ | ||
| def PPTComputable (f : List Bool → PMF (List Bool)) : Prop := | ||
| ∃ (k : ℕ) (tm : NTM k) (T : ℕ → ℕ) (d : ℕ), |
There was a problem hiding this comment.
I am unsure how you define NTM k with time bound T. Do you require that it consume a random tape of length exactly T?
There was a problem hiding this comment.
There was a problem hiding this comment.
If you re-define PTMs then I guess this will also change,
2 participants
Summary
BitEncodable: Specification-level typeclass for encoding types as bit strings (List Bool). Instances forUnit,List Bool,Option (List Bool), andProd. Used to state that a TM's bit-string I/O corresponds to a Lean function on abstract types — carries no computational obligation.unpair: Left inverse ofpairwith roundtrip proofunpair (pair x y) = (x, y). Returns([], [])for strings not in the image ofpair.PPTComputable: Predicate asserting a randomized functionList Bool → PMF (List Bool)is computable by a PPT NTM, bridging NTM output distributions (outputCount) to Mathlib'sPMFviaENNReal.pair_nil_eqandpair_cons_eqpublic@[simp]lemmas (needed byunpair_pair).Motivation
These are foundational building blocks for formalizing computational cryptography (KL Chapter 3). The cryptolib project will use
BitEncodableandPPTComputableto define encryption schemes where algorithms are Lean functions with PPT realizability asserted via existential TM witnesses.Test plan
lake buildpasses with no new errors or warnings