diff --git a/ArkLib/Data/Fin/Basic.lean b/ArkLib/Data/Fin/Basic.lean index 98e7ed893..566e68b13 100644 --- a/ArkLib/Data/Fin/Basic.lean +++ b/ArkLib/Data/Fin/Basic.lean @@ -243,8 +243,44 @@ theorem append_right_injective (a : Fin m → α) : Function.Injective (@Fin.app simp only [append_right] at this exact this +section Subtype + +variable {m n : ℕ} {α : Sort*} {p : Fin m → Prop} {q : Fin n → Prop} + +/-- Append two vectors defined on subtypes of `Fin m` and `Fin n` respectively. -/ +def appendSubtype (u : { i : Fin m // p i} → α) (v : { i : Fin n // q i} → α) : + { i : Fin (m + n) // Fin.append p q i } → α := fun x => + if hi : x.1.1 < m then u ⟨⟨x.1.1, by omega⟩, by simpa [append, addCases, hi] using x.2⟩ + else v ⟨⟨x.1.1 - m, by omega⟩, by simpa [append, addCases, hi] using x.2⟩ + +variable {u : { i : Fin m // p i} → α} {v : { i : Fin n // q i} → α} + +@[simp] +theorem appendSubtype_left (i : { i : Fin m // p i }) : + appendSubtype u v ⟨castAdd n i.1, by simpa [append, addCases] using i.2⟩ = u i := by + simp [appendSubtype] + +@[simp] +theorem appendSubtype_right (i : { i : Fin n // q i }) : + appendSubtype u v ⟨natAdd m i.1, by simpa [append, addCases] using i.2⟩ = v i := by + simp [appendSubtype] + +theorem appendSubtype_left_injective : Function.Injective (@appendSubtype m n α p q · v) := by + intro x y h + ext i + simpa using funext_iff.mp h ⟨i.1.castAdd n, by simpa [append, addCases] using i.2⟩ + +theorem appendSubtype_right_injective : Function.Injective (@appendSubtype m n α p q u ·) := by + intro x y h + ext i + simpa using funext_iff.mp h ⟨i.1.natAdd m, by simpa [append, addCases] using i.2⟩ + +end Subtype + end Append +section AddCases + /-- Version of `Fin.addCases` that splits the motive into two dependent vectors `α` and `β`, and the return type is `Fin.append α β`. -/ def addCases' {m n : ℕ} {α : Fin m → Sort u} {β : Fin n → Sort u} (left : (i : Fin m) → α i) @@ -272,6 +308,59 @@ theorem addCases'_right {m n : ℕ} {α : Fin m → Sort u} {β : Fin n → Sort -- refine addCasesFn_iff.mpr (fun i => ?_) -- simp [addCases'] +section Subtype + +variable {m n : ℕ} {α : Fin m → Sort u} {β : Fin n → Sort u} {p : Fin m → Prop} {q : Fin n → Prop} + (f : Sort u → Sort v) + +/-- Append two heterogeneous vectors defined on subtypes of `Fin m` and `Fin n` respectively, where + the return type is further transformed by a function `f` on types. -/ +def addCasesSubtypeFun (left : (i : { j : Fin m // p j }) → f (α i)) + (right : (j : { i : Fin n // q i }) → f (β j)) : + (i : { j : Fin (m + n) // append p q j }) → f (append α β i) := + fun x => if hi : x.1.1 < m then + (by simpa [append, addCases, hi] using + left ⟨⟨x.1.1, by omega⟩, by simpa [append, addCases, hi] using x.2⟩) + else + (by simpa [append, addCases, hi] using + right ⟨⟨x.1.1 - m, by omega⟩, by simpa [append, addCases, hi] using x.2⟩) + +/-- Append two heterogeneous vectors defined on subtypes of `Fin m` and `Fin n` respectively. -/ +def addCasesSubtype (left : (i : { j : Fin m // p j }) → α i) + (right : (j : { i : Fin n // q i }) → β j) : + (i : { j : Fin (m + n) // append p q j }) → append α β i := + addCasesSubtypeFun id left right + +variable {f : Sort u → Sort v} {left : (i : { j : Fin m // p j }) → f (α i)} + {right : (j : { i : Fin n // q i }) → f (β j)} + +@[simp] +theorem addCasesSubtypeFun_left (i : { j : Fin m // p j }) : + addCasesSubtypeFun f left right ⟨castAdd n i.1, by simpa [append, addCases] using i.2⟩ = + (by simpa [append, addCases] using left i) := by + simp [addCasesSubtypeFun] + +@[simp] +theorem addCasesSubtypeFun_right (j : { i : Fin n // q i }) : + addCasesSubtypeFun f left right ⟨natAdd m j.1, by simpa [append, addCases] using j.2⟩ = + (by simpa [append, addCases] using right j) := by + simp [addCasesSubtypeFun] + congr 1 + · simp + · simp + · rw! (castMode := .all) [Nat.add_sub_self_left]; simp + +theorem addCasesSubtypeFun_eq_appendSubtype {α : Sort u} + {left : (i : { j : Fin m // p j }) → f α} {right : (j : { i : Fin n // q i }) → f α} + {i : { j : Fin (m + n) // append p q j }} : + addCasesSubtypeFun (α := fun _ => α) (β := fun _ => α) f left right i = + (by simpa [append, addCases] using appendSubtype left right i) := by + by_cases h : i.1.1 < m <;> simp [addCasesSubtypeFun, appendSubtype, h] + +end Subtype + +end AddCases + variable {n : ℕ} {α : Fin n → Sort u} theorem take_addCases'_left {n' : ℕ} {β : Fin n' → Sort u} (m : ℕ) (h : m ≤ n) diff --git a/ArkLib/OracleReduction/Basic.lean b/ArkLib/OracleReduction/Basic.lean index c19855123..28888fb9c 100644 --- a/ArkLib/OracleReduction/Basic.lean +++ b/ArkLib/OracleReduction/Basic.lean @@ -83,17 +83,19 @@ structure Indexer {ι : Type} (oSpec : OracleSpec ι) {n : ℕ} (pSpec : Protoco encode : Index → OracleComp oSpec Encoding [OracleInterface : OracleInterface Encoding] -/-- The type signature for the prover's state at each round. +/-- The type signature for the prover's state at each step. For a protocol with `n` messages exchanged, there will be `(n + 1)` prover states, with the first state before the first message and the last state after the last message. -/ @[ext] structure ProverState (n : ℕ) where + /-- The prover's state at each step (before first message and after last message) -/ PrvState : Fin (n + 1) → Type /-- Initialization of prover's state via inputting the statement and witness. -/ @[ext] structure ProverIn (StmtIn WitIn PrvState : Type) where + /-- Initialize the prover's state via taking in the input statement and witness -/ input : StmtIn × WitIn → PrvState -- initState : PrvState -- if honest prover, then expect that PrvState 0 = WitIn @@ -109,16 +111,17 @@ other functions are pure. We may revisit this decision in the future. @[ext] structure ProverRound {ι : Type} (oSpec : OracleSpec ι) {n : ℕ} (pSpec : ProtocolSpec n) extends ProverState n where - /-- Send a message and update the prover's state -/ + /-- Send a message (when the round is a message round) and update the prover's state -/ sendMessage (i : MessageIdx pSpec) : PrvState i.1.castSucc → OracleComp oSpec (pSpec.Message i × PrvState i.1.succ) - /-- Receive a challenge and update the prover's state -/ + /-- Receive a challenge (when the round is a challenge round) and update the prover's state -/ receiveChallenge (i : ChallengeIdx pSpec) : PrvState i.1.castSucc → (pSpec.Challenge i) → PrvState i.1.succ /-- The output of the prover, which is a function from the prover's state to the output witness -/ @[ext] structure ProverOut (StmtOut WitOut PrvState : Type) where + /-- Output the output statement and witness from the (final) prover's state -/ output : PrvState → StmtOut × WitOut /-- A prover for an interactive protocol with `n` messages consists of a sequence of internal states @@ -147,8 +150,16 @@ structure Prover {ι : Type} (oSpec : OracleSpec ι) @[ext] structure Verifier {ι : Type} (oSpec : OracleSpec ι) (StmtIn StmtOut : Type) {n : ℕ} (pSpec : ProtocolSpec n) where + /-- Verify the output statement, in terms of the input statement and the transcript, and having + access to the shared oracle. -/ verify : StmtIn → FullTranscript pSpec → OracleComp oSpec StmtOut +namespace Verifier + +alias reduce := verify + +end Verifier + /-- An **(oracle) prover** in an interactive **oracle** reduction is a prover in the non-oracle reduction whose input statement also consists of the underlying messages for the oracle statements -/ @@ -159,83 +170,126 @@ def OracleProver {ι : Type} (oSpec : OracleSpec ι) {n : ℕ} (pSpec : ProtocolSpec n) := Prover oSpec (StmtIn × (∀ i, OStmtIn i)) WitIn (StmtOut × (∀ i, OStmtOut i)) WitOut pSpec -/-- An **(oracle) verifier** of an interactive **oracle** reduction consists of: - - - an oracle computation `verify` that outputs the next statement. It may make queries to each of - the prover's messages and each of the oracles present in the statement (according to a specified - interface defined by `OracleInterface` instances). +namespace OracleVerifier - - output oracle statements `OStmtOut : ιₛₒ → Type`, meant to be a **subset** of the input oracle - statements and the prover's oracle messages. Formally, this is specified by an embedding `ιₛₒ ↪ - ιₛᵢ ⊕ pSpec.MessageIdx` and a proof that `OStmtOut` is compatible with `OStmtIn` and - `pSpec.Messages` via this embedding. +variable {ι : Type} (oSpec : OracleSpec ι) + (StmtIn : Type) {ιₛᵢ : Type} (OStmtIn : ιₛᵢ → Type) [Oₛᵢ : ∀ i, OracleInterface (OStmtIn i)] + (StmtOut : Type) {ιₛₒ : Type} (OStmtOut : ιₛₒ → Type) [Oₛₒ : ∀ i, OracleInterface (OStmtOut i)] + {n : ℕ} (pSpec : ProtocolSpec n) [Oₘ : ∀ i, OracleInterface (pSpec.Message i)] -Intuitively, the oracle verifier cannot do anything more in returning the output oracle statements, -other than specifying a subset of the ones it has received (and dropping the rest). -/ -@[ext] -structure OracleVerifier {ι : Type} (oSpec : OracleSpec ι) - (StmtIn : Type) {ιₛᵢ : Type} (OStmtIn : ιₛᵢ → Type) - (StmtOut : Type) {ιₛₒ : Type} (OStmtOut : ιₛₒ → Type) - {n : ℕ} (pSpec : ProtocolSpec n) - [Oₛᵢ : ∀ i, OracleInterface (OStmtIn i)] - [Oₘ : ∀ i, OracleInterface (pSpec.Message i)] - where - -- This will be needed after the switch to `simOStmt` - -- [Oₛₒ : ∀ i, OracleInterface (OStmtOut i)] - - /-- The core verification logic. Takes the input statement `stmtIn` and all verifier challenges - `challenges` (which are determined outside this function, typically by sampling for - public-coin protocols). Returns the output statement `StmtOut` within an `OracleComp` that has - access to external oracles `oSpec`, input statement oracles `OStmtIn`, and prover message - oracles `pSpec.Message`. -/ +/-- The computation of the output statement from the input statement and the challenges, given + access to the shared oracle, the input oracle statements, and the prover's messages. -/ +@[ext] structure Verify where + /-- Verify the output statement, in terms of the input statement, the challenges, and having + access to the shared oracle, the input oracle statements, and the prover's messages. -/ verify : StmtIn → pSpec.Challenges → OracleComp (oSpec ++ₒ ([OStmtIn]ₒ ++ₒ [pSpec.Message]ₒ)) StmtOut - -- TODO: this seems like the right way for compositionality - -- Makes it potentially more difficult for compilation with commitment schemes - -- Can recover the old version (with `embed` and `hEq`) via a constructor `QueryImpl.ofEmbed` +alias Verify.reduce := Verify.verify - -- simOStmt : QueryImpl [OStmtOut]ₒ (OracleComp ([OStmtIn]ₒ ++ₒ [pSpec.Message]ₒ)) +/-- The simulation of the (oracles corresponding to the) output oracle statements, in terms of the + shared oracle, the input oracle statements, and the prover's messages (as oracles). May depend + on the challenges. +-/ +@[ext] structure Simulate where + /-- Simulate the output oracle statements, in terms of the shared oracle, the input oracle + statements, and the prover's messages (as oracles), and depends on the challenges. + + NOTE: we do not make this depend on the input statement (yet). This is because if we do, then for + sequential composition, we need to wrap `QueryImpl` inside an `OracleComp` (i.e. to derive the + second simulation, we need the second statement, which is only available inside the monad). + Unfortunately, `QueryImpl` currently raises universe levels (i.e. it contains `OracleComp`), so we + cannot do this. May revisit this in the future. -/ + simulate : pSpec.Challenges → + QueryImpl [OStmtOut]ₒ (OracleComp (oSpec ++ₒ ([OStmtIn]ₒ ++ₒ [pSpec.Message]ₒ))) + +/-- An oracle verifier that only supports simulation, without an associated reification. + +This is sufficient for all downstream definitions, but at the expense of more verbosity due to not +taking advantage of the reification. + +Since all known IORs have reifiable oracle verifiers, we have that as the default. + +NOTE: given just the oracle simulation, there may not be an obvious target for reification. This is +because, say, the oracle interface doesn't allow for reconstructing the underlying data (e.g. if +it's a vector and we can only query a subset of it) -/ +@[ext] structure SimulateOnly extends + Verify oSpec StmtIn OStmtIn StmtOut pSpec, + Simulate oSpec OStmtIn OStmtOut pSpec + +/-- The computation of the (actual) output oracle statements from the input statement, input oracle + statements, the transcript, and with access to the shared oracle. -/ +@[ext] structure Reify where + /-- Reify the output oracle statements, in terms of the input statement, input oracle statements, + the transcript, and with access to the shared oracle. -/ + reify : StmtIn × (∀ i, OStmtIn i) → pSpec.FullTranscript → OracleComp oSpec (∀ i, OStmtOut i) + +/-- A reification is lawful if the computation of the output oracle statements is compatible with + the simulation of the (oracles corresponding to the) output oracle statements. -/ +@[ext] class LawfulReify (S : Simulate oSpec OStmtIn OStmtOut pSpec) + (R : Reify oSpec StmtIn OStmtIn OStmtOut pSpec) where + /-- The reification and simulation are compatible, in the sense that the following two processes + are equal: + 1. First derive the output oracle statements via reification, then use that to answer queries to + the oracles. + 2. Answer queries to the oracles by first lifting it (via simulation) to a computation querying + the shared oracle, the input oracle statement, and the prover's messages, then use the + provided data for the latter two to reduce it to just an oracle computation. -/ + reify_simulate : ∀ stmtIn oStmtIn transcript i q, + (do return (Oₛₒ i).oracle ((← R.reify ⟨stmtIn, oStmtIn⟩ transcript) i) q) = + simulateQ (OracleInterface.simOracle2 oSpec oStmtIn transcript.messages) + (simulateQ (S.simulate transcript.challenges) + (query (spec := [OStmtOut]ₒ) i q)) + +end OracleVerifier - /-- An embedding that specifies how each output oracle statement (indexed by `ιₛₒ`) is derived. - It maps an index `i : ιₛₒ` to either an index `j : ιₛᵢ` (meaning `OStmtOut i` comes from - `OStmtIn j`) or an index `k : pSpec.MessageIdx` (meaning `OStmtOut i` comes from the - prover's message `pSpec.Message k`). This enforces that output oracles are a subset of - input oracles or received prover messages. -/ - embed : ιₛₒ ↪ ιₛᵢ ⊕ pSpec.MessageIdx +/-- An **(oracle) verifier** of an interactive **oracle** reduction, which consists of the following + components: - /-- A proof term ensuring that the type of each `OStmtOut i` matches the type of the - corresponding source oracle statement (`OStmtIn j` or `pSpec.Message k`) as determined - by the `embed` mapping. -/ - hEq : ∀ i, OStmtOut i = match embed i with - | Sum.inl j => OStmtIn j - | Sum.inr j => pSpec.Message j +1. `verify`: the main verification logic, derives the output statement from the input statement, the + challenges, and with access to the shared oracle, the oracle statements, and the prover's + messages --- Cannot find synthesization order... --- instance {ιₛᵢ ιₘ ιₛₒ : Type} {OStmtIn : ιₛᵢ → Type} [Oₛᵢ : ∀ i, OracleInterface (OStmtIn i)] --- {Message : ιₘ → Type} [Oₘ : ∀ i, OracleInterface (Message i)] --- (OStmtOut : ιₛₒ → Type) (embed : ιₛₒ ↪ ιₛᵢ ⊕ ιₘ) : --- ∀ i, OStmtOut i := fun i => by sorry +2. `simulate`: a specification of how to answer queries to the output oracle statements, again + allowed to make (adaptive) queries to both the input oracle statements and the prover's messages + +3. `reify`: a function that derives the output oracle statements from the input statement + (non-oracle & oracle), the entire transcript, and with access to the shared oracle (essentially + same interface as the prover) + +4. `reify_simulate`: a compatibility condition that ensures that the reification and simulation are + compatible (see `OracleVerifier.LawfulReify` for the precise theorem statement). +-/ +@[ext] structure OracleVerifier {ι : Type} (oSpec : OracleSpec ι) + (StmtIn : Type) {ιₛᵢ : Type} (OStmtIn : ιₛᵢ → Type) [Oₛᵢ : ∀ i, OracleInterface (OStmtIn i)] + (StmtOut : Type) {ιₛₒ : Type} (OStmtOut : ιₛₒ → Type) [Oₛₒ : ∀ i, OracleInterface (OStmtOut i)] + {n : ℕ} (pSpec : ProtocolSpec n) [Oₘ : ∀ i, OracleInterface (pSpec.Message i)] + extends + OracleVerifier.SimulateOnly oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec, + OracleVerifier.Reify oSpec StmtIn OStmtIn OStmtOut pSpec, + OracleVerifier.LawfulReify oSpec StmtIn OStmtIn OStmtOut pSpec toSimulate toReify namespace OracleVerifier variable {ι : Type} {oSpec : OracleSpec ι} - {StmtIn : Type} {ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} - {StmtOut : Type} {ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} - {n : ℕ} {pSpec : ProtocolSpec n} - [Oₛᵢ : ∀ i, OracleInterface (OStmtIn i)] - [Oₘ : ∀ i, OracleInterface (pSpec.Message i)] - (verifier : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec) - -/-- An oracle verifier can be seen as a (non-oracle) verifier by providing the oracle interface - using its knowledge of the oracle statements and the transcript messages in the clear -/ + {StmtIn : Type} {ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} [Oₛᵢ : ∀ i, OracleInterface (OStmtIn i)] + {StmtOut : Type} {ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} [Oₛₒ : ∀ i, OracleInterface (OStmtOut i)] + {n : ℕ} {pSpec : ProtocolSpec n} [Oₘ : ∀ i, OracleInterface (pSpec.Message i)] + (V : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec) + +/-- Convert an oracle verifier to a non-oracle verifier (for the associated reduction where all + messages are sent in the clear). + + This is done by using the underlying data for the input oracle statement & the prover's messages + to derive both the output statement (via `verify`) and the output oracle statements (via `reify`). +-/ def toVerifier : Verifier oSpec (StmtIn × ∀ i, OStmtIn i) (StmtOut × (∀ i, OStmtOut i)) pSpec where verify := fun ⟨stmt, oStmt⟩ transcript => do + -- First compute the output statement using `verify` / `reduce` let stmtOut ← simulateQ (OracleInterface.simOracle2 oSpec oStmt transcript.messages) - (verifier.verify stmt transcript.challenges) - letI oStmtOut := fun i => match h : verifier.embed i with - | Sum.inl j => by simpa only [verifier.hEq, h] using (oStmt j) - | Sum.inr j => by simpa only [verifier.hEq, h] using (transcript j) + (V.verify stmt transcript.challenges) + -- Then compute the output oracle statements using the reification + let oStmtOut ← V.reify ⟨stmt, oStmt⟩ transcript return (stmtOut, oStmtOut) /-- The number of queries made to the oracle statements and the prover's messages, for a given input @@ -249,6 +303,45 @@ def numQueries (stmt : StmtIn) (challenges : ∀ i, pSpec.Challenge i) (verifier : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec) : OracleComp (oSpec ++ₒ ([OStmtIn]ₒ ++ₒ [pSpec.Message]ₒ)) ℕ := sorry +/-- Construct an oracle verifier whose output oracle statements are a subset of the input oracle + statements and the prover's messages (without any fancy simulation semantics). + + This is the case for most IORs under consideration. -/ +def ofEmbed + (verify : StmtIn → pSpec.Challenges → + OracleComp (oSpec ++ₒ ([OStmtIn]ₒ ++ₒ [pSpec.Message]ₒ)) StmtOut) + (embed : ιₛₒ ↪ ιₛᵢ ⊕ pSpec.MessageIdx) + (hData : ∀ i, OStmtOut i = match embed i with + | Sum.inl j => OStmtIn j + | Sum.inr j => pSpec.Message j) + (hInterface : ∀ i, Oₛₒ i = match h : embed i with + | Sum.inl j => by simpa [hData, h] using Oₛᵢ j + | Sum.inr j => by simpa [hData, h] using Oₘ j) : + OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec where + verify := verify + simulate := fun _ => { + impl | query i q => match h : embed i with + | Sum.inl j => sorry + -- liftM <| query (spec := [OStmtIn]ₒ) j + -- (by + -- have h1 := hData i + -- have h2 := hInterface i + -- rw! [h] at h2 + -- simp [h] at h1 h2 + -- -- rw [← cast_symm] at h2 + -- simp [OracleInterface.toOracleSpec, OracleSpec.domain] at q ⊢ + -- let q' := h2 ▸ q + -- sorry + -- ) + | Sum.inr j => sorry + } + reify := fun ⟨stmt, oStmt⟩ transcript => do + let oStmtOut := fun i => match h : embed i with + | Sum.inl j => by simpa [hData, h] using oStmt j + | Sum.inr j => by simpa [hData, h] using transcript.messages j + return oStmtOut + reify_simulate := sorry + /-- A **non-adaptive** oracle verifier is an oracle verifier that makes a **fixed** list of queries to the input oracle statements and the prover's messages. These queries can depend on the input statement and the challenges, but later queries are not dependent on the responses of previous @@ -263,16 +356,18 @@ def numQueries (stmt : StmtIn) (challenges : ∀ i, pSpec.Challenge i) the output statement, but not on the list of queries made to the oracle statements or the prover's messages. - Finally, we also allow for choosing a subset of the input oracle statements + the prover's - messages to retain for the output oracle statements. + We keep the same simulate and reification components, only changing the `verify` component to + only make non-adaptive queries to the oracle statements and the prover's messages. -/ structure NonAdaptive {ι : Type} (oSpec : OracleSpec ι) - (StmtIn : Type) {ιₛᵢ : Type} (OStmtIn : ιₛᵢ → Type) - (StmtOut : Type) {ιₛₒ : Type} (OStmtOut : ιₛₒ → Type) - {n : ℕ} (pSpec : ProtocolSpec n) - [Oₛᵢ : ∀ i, OracleInterface (OStmtIn i)] - [Oₘ : ∀ i, OracleInterface (pSpec.Message i)] - where + (StmtIn : Type) {ιₛᵢ : Type} (OStmtIn : ιₛᵢ → Type) [Oₛᵢ : ∀ i, OracleInterface (OStmtIn i)] + (StmtOut : Type) {ιₛₒ : Type} (OStmtOut : ιₛₒ → Type) [Oₛₒ : ∀ i, OracleInterface (OStmtOut i)] + {n : ℕ} (pSpec : ProtocolSpec n) [Oₘ : ∀ i, OracleInterface (pSpec.Message i)] + extends + OracleVerifier.Simulate oSpec OStmtIn OStmtOut pSpec, + OracleVerifier.Reify oSpec StmtIn OStmtIn OStmtOut pSpec, + OracleVerifier.LawfulReify oSpec StmtIn OStmtIn OStmtOut pSpec toSimulate toReify + where /-- Makes a list of queries to each of the oracle statements, given the input statement and the challenges -/ @@ -287,12 +382,6 @@ structure NonAdaptive {ι : Type} (oSpec : OracleSpec ι) List ((i : ιₛᵢ) × ((Oₛᵢ i).Query × (Oₛᵢ i).Response)) → List ((i : pSpec.MessageIdx) × ((Oₘ i).Query × (Oₘ i).Response)) → OracleComp oSpec StmtOut - embed : ιₛₒ ↪ ιₛᵢ ⊕ pSpec.MessageIdx - - hEq : ∀ i, OStmtOut i = match embed i with - | Sum.inl j => OStmtIn j - | Sum.inr j => pSpec.Message j - namespace NonAdaptive /-- Converts a non-adaptive oracle verifier into the general oracle verifier interface. @@ -300,25 +389,25 @@ namespace NonAdaptive This essentially performs the queries via `List.mapM`, then runs `verify` on the query-response pairs. -/ def toOracleVerifier - (naVerifier : OracleVerifier.NonAdaptive oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec) : + (nonAdaptiveV : OracleVerifier.NonAdaptive oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec) : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec where verify := fun stmt challenges => do let queryResponsesOStmt : List ((i : ιₛᵢ) × ((Oₛᵢ i).Query × (Oₛᵢ i).Response)) ← - (naVerifier.queryOStmt stmt challenges).mapM + (nonAdaptiveV.queryOStmt stmt challenges).mapM (fun q => do let resp ← liftM <| query (spec := [OStmtIn]ₒ) q.1 q.2 return ⟨q.1, (q.2, by simpa only using resp)⟩) let queryResponsesOMsg : List ((i : pSpec.MessageIdx) × ((Oₘ i).Query × (Oₘ i).Response)) ← - (naVerifier.queryMsg stmt challenges).mapM + (nonAdaptiveV.queryMsg stmt challenges).mapM (fun q => do let resp ← liftM <| query (spec := [pSpec.Message]ₒ) q.1 q.2 return ⟨q.1, ⟨q.2, by simpa only using resp⟩⟩) - let stmtOut ← liftM <| naVerifier.verify stmt challenges queryResponsesOStmt queryResponsesOMsg + let stmtOut ← liftM <| + nonAdaptiveV.verify stmt challenges queryResponsesOStmt queryResponsesOMsg return stmtOut - - embed := naVerifier.embed - - hEq := naVerifier.hEq + simulate := nonAdaptiveV.simulate + reify := nonAdaptiveV.reify + reify_simulate := nonAdaptiveV.reify_simulate /-- The number of queries made to the `i`-th oracle statement, for a given input statement and challenges. -/ @@ -356,10 +445,11 @@ structure Reduction {ι : Type} (oSpec : OracleSpec ι) oracles defined by `oSpec`, consists of a prover and an **oracle** verifier. -/ @[ext] structure OracleReduction {ι : Type} (oSpec : OracleSpec ι) - (StmtIn : Type) {ιₛᵢ : Type} (OStmtIn : ιₛᵢ → Type) (WitIn : Type) - (StmtOut : Type) {ιₛₒ : Type} (OStmtOut : ιₛₒ → Type) (WitOut : Type) - {n : ℕ} (pSpec : ProtocolSpec n) - [Oₛᵢ : ∀ i, OracleInterface (OStmtIn i)] [Oₘ : ∀ i, OracleInterface (pSpec.Message i)] + (StmtIn : Type) {ιₛᵢ : Type} (OStmtIn : ιₛᵢ → Type) [Oₛᵢ : ∀ i, OracleInterface (OStmtIn i)] + (WitIn : Type) + (StmtOut : Type) {ιₛₒ : Type} (OStmtOut : ιₛₒ → Type) [Oₛₒ : ∀ i, OracleInterface (OStmtOut i)] + (WitOut : Type) + {n : ℕ} (pSpec : ProtocolSpec n) [Oₘ : ∀ i, OracleInterface (pSpec.Message i)] where prover : OracleProver oSpec StmtIn OStmtIn WitIn StmtOut OStmtOut WitOut pSpec verifier : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec @@ -367,21 +457,26 @@ structure OracleReduction {ι : Type} (oSpec : OracleSpec ι) /-- An interactive oracle reduction can be seen as an interactive reduction, via coercing the oracle verifier to a (normal) verifier -/ def OracleReduction.toReduction {ι : Type} {oSpec : OracleSpec ι} - {StmtIn : Type} {ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} {WitIn : Type} - {StmtOut : Type} {ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} {WitOut : Type} - {n : ℕ} {pSpec : ProtocolSpec n} - [Oₛᵢ : ∀ i, OracleInterface (OStmtIn i)] [Oₘ : ∀ i, OracleInterface (pSpec.Message i)] + {StmtIn : Type} {ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} [Oₛᵢ : ∀ i, OracleInterface (OStmtIn i)] + {WitIn : Type} + {StmtOut : Type} {ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} [Oₛₒ : ∀ i, OracleInterface (OStmtOut i)] + {WitOut : Type} + {n : ℕ} {pSpec : ProtocolSpec n} [Oₘ : ∀ i, OracleInterface (pSpec.Message i)] (oracleReduction : OracleReduction oSpec StmtIn OStmtIn WitIn StmtOut OStmtOut WitOut pSpec) : Reduction oSpec (StmtIn × (∀ i, OStmtIn i)) WitIn (StmtOut × (∀ i, OStmtOut i)) WitOut pSpec := ⟨oracleReduction.prover, oracleReduction.verifier.toVerifier⟩ +/-- Since `TrivialOracleStatement` is `Empty`-indexed, it has an (indexed family of) + `OracleInterface` instance via empty elimination. -/ +instance : ∀ i, OracleInterface (TrivialOracleStatement i) := isEmptyElim + /-- An **interactive proof (IP)** is an interactive reduction where the output statement is a boolean, the output witness is trivial (a `Unit`), and the relation checks whether the output statement is true. -/ @[reducible] def Proof {ι : Type} (oSpec : OracleSpec ι) (Statement Witness : Type) {n : ℕ} (pSpec : ProtocolSpec n) := - Reduction oSpec Statement Witness Bool Unit pSpec + Reduction oSpec Statement Witness TrivialStatement TrivialWitness pSpec /-- An **interactive oracle proof (IOP)** is an interactive oracle reduction where the output statement is a boolean, while both the output oracle statement & the output witness are @@ -390,11 +485,11 @@ def OracleReduction.toReduction {ι : Type} {oSpec : OracleSpec ι} As a consequence, the output relation in an IOP is effectively a function `Bool → Prop`, which we can again assume to be the trivial one (sending `true` to `True`). -/ @[reducible] def OracleProof {ι : Type} (oSpec : OracleSpec ι) - (Statement : Type) {ιₛᵢ : Type} (OStatement : ιₛᵢ → Type) (Witness : Type) - {n : ℕ} (pSpec : ProtocolSpec n) - [Oₛᵢ : ∀ i, OracleInterface (OStatement i)] - [Oₘ : ∀ i, OracleInterface (pSpec.Message i)] := - OracleReduction oSpec Statement OStatement Witness Bool (fun _ : Empty => Unit) Unit pSpec + (Statement : Type) {ιₛ : Type} (OStatement : ιₛ → Type) + [Oₛ : ∀ i, OracleInterface (OStatement i)] (Witness : Type) + {n : ℕ} (pSpec : ProtocolSpec n) [Oₘ : ∀ i, OracleInterface (pSpec.Message i)] := + OracleReduction oSpec Statement OStatement Witness + TrivialStatement TrivialOracleStatement TrivialWitness pSpec /-- A **non-interactive prover** is a prover that only sends a single message to the verifier. -/ @[reducible] def NonInteractiveProver (Message : Type) {ι : Type} (oSpec : OracleSpec ι) @@ -445,12 +540,16 @@ protected def OracleProver.id : Prover.id /-- The trivial / identity verifier in an oracle reduction, which receives no messages from the - prover, and returns its input statement as output. -/ + prover, and returns its input statement (both non-oracle and oracle) as output. -/ protected def OracleVerifier.id : OracleVerifier oSpec Statement OStatement Statement OStatement ![] where verify := fun stmt _ => pure stmt - embed := Function.Embedding.inl - hEq := fun _ => rfl + simulate := fun _ => { + impl | query i q => (query (Sum.inr (Sum.inl i)) q + (spec := oSpec ++ₒ ([OStatement]ₒ ++ₒ [ProtocolSpec.Message ![]]ₒ))) + } + reify := fun combinedStmt _ => pure combinedStmt.2 + reify_simulate := fun _ _ _ _ _ => rfl /-- The trivial / identity oracle reduction, which consists of the trivial oracle prover and verifier. -/ diff --git a/ArkLib/OracleReduction/Composition/Sequential/Append.lean b/ArkLib/OracleReduction/Composition/Sequential/Append.lean index 844eaa6e6..bcb43cb54 100644 --- a/ArkLib/OracleReduction/Composition/Sequential/Append.lean +++ b/ArkLib/OracleReduction/Composition/Sequential/Append.lean @@ -22,8 +22,15 @@ import ArkLib.OracleReduction.Security.RoundByRound of the reductions being composed (with extra conditions on the extractor). -/ +universe u v + section find_home +@[simp] +theorem eqRec_eqRec_eq_self {α β : Sort u} {h : α = β} {h' : β = α} {a : α} : + h ▸ h' ▸ a = a := by + cases h; cases h'; rfl + variable {ι ι' : Type} {spec : OracleSpec ι} {spec' : OracleSpec ι'} {α β : Type} (oa : OracleComp spec α) @@ -46,25 +53,44 @@ section Instances /-- If two protocols have sampleable challenges, then their concatenation also has sampleable challenges. -/ -instance [h₁ : ∀ i, Sampleable (pSpec₁.Challenge i)] [h₂ : ∀ i, Sampleable (pSpec₂.Challenge i)] : - ∀ i, Sampleable ((pSpec₁ ++ₚ pSpec₂).Challenge i) := fun ⟨⟨i, isLt⟩, h⟩ => by - dsimp [ProtocolSpec.append, Fin.append, Fin.addCases, Fin.castLT, Fin.subNat, Fin.cast] at h ⊢ - by_cases h' : i < m <;> simp [h'] at h ⊢ - · exact h₁ ⟨⟨i, by omega⟩, h⟩ - · exact h₂ ⟨⟨i - m, by omega⟩, h⟩ +instance instSampleableChallengeAppend + [h₁ : ∀ i, Sampleable (pSpec₁.Challenge i)] + [h₂ : ∀ i, Sampleable (pSpec₂.Challenge i)] : + ∀ i, Sampleable ((pSpec₁ ++ₚ pSpec₂).Challenge i) := + -- unfold ChallengeIdx Challenge at h₁ h₂ + -- unfold ProtocolSpec.append at i ⊢ + -- unfold ChallengeIdx at i + -- exact Fin.addCasesSubtypeFun + -- (α := fun i => (pSpec₁ i).2) (β := fun i => (pSpec₂ i).2) + -- (p := fun i => (pSpec₁ i).1 = .V_to_P) (q := fun i => (pSpec₂ i).1 = .V_to_P) + -- (f := Sampleable) + -- h₁ h₂ i + fun ⟨⟨i, isLt⟩, h⟩ => by + dsimp [ProtocolSpec.append, Fin.append, Fin.addCases, Fin.castLT, Fin.subNat, Fin.cast] at h ⊢ + by_cases h' : i < m <;> simp [h'] at h ⊢ + · exact h₁ ⟨⟨i, by omega⟩, h⟩ + · exact h₂ ⟨⟨i - m, by omega⟩, h⟩ /-- If two protocols' messages have oracle representations, then their concatenation's messages also have oracle representations. -/ -instance [O₁ : ∀ i, OracleInterface (pSpec₁.Message i)] +instance instOracleInterfaceMessageAppend + [O₁ : ∀ i, OracleInterface (pSpec₁.Message i)] [O₂ : ∀ i, OracleInterface (pSpec₂.Message i)] : - ∀ i, OracleInterface ((pSpec₁ ++ₚ pSpec₂).Message i) := fun ⟨⟨i, isLt⟩, h⟩ => by + ∀ i, OracleInterface ((pSpec₁ ++ₚ pSpec₂).Message i) := + fun ⟨⟨i, isLt⟩, h⟩ => by dsimp [ProtocolSpec.append, ProtocolSpec.getDir, Fin.append, Fin.addCases, Fin.castLT, Fin.subNat, Fin.cast] at h ⊢ by_cases h' : i < m <;> simp [h'] at h ⊢ · exact O₁ ⟨⟨i, by omega⟩, h⟩ · exact O₂ ⟨⟨i - m, by omega⟩, h⟩ -open OracleComp OracleSpec SubSpec +-- #print instOracleInterfaceMessageAppend + +open OracleComp OracleSpec SubSpec OracleInterface + +namespace ProtocolSpec + +namespace Challenge variable [∀ i, Sampleable (pSpec₁.Challenge i)] [∀ i, Sampleable (pSpec₂.Challenge i)] @@ -72,11 +98,11 @@ instance instSubSpecOfProtocolSpecAppendChallenge : SubSpec ([pSpec₁.Challenge]ₒ ++ₒ [pSpec₂.Challenge]ₒ) ([(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ) where monadLift | query i t => match i with | Sum.inl j => by - simpa [OracleSpec.append, OracleSpec.range, OracleInterface.toOracleSpec, ChallengeIdx.inl, + simpa [OracleSpec.append, OracleSpec.range, toOracleSpec, ChallengeIdx.inl, instChallengeOracleInterface] using query (spec := [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ) j.inl () | Sum.inr j => by - simpa [OracleSpec.append, OracleSpec.range, OracleInterface.toOracleSpec, ChallengeIdx.inr, + simpa [OracleSpec.append, OracleSpec.range, toOracleSpec, ChallengeIdx.inr, instChallengeOracleInterface] using query (spec := [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ) j.inr () -- evalDist_toFun' := fun i q => by @@ -112,6 +138,54 @@ instance : SubSpec [pSpec₁.Challenge]ₒ ([(pSpec₁ ++ₚ pSpec₂).Challenge instance : SubSpec [pSpec₂.Challenge]ₒ ([(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ) where monadLift | query i t => instSubSpecOfProtocolSpecAppendChallenge.monadLift (query (Sum.inr i) t) +end Challenge + +namespace Message + +private lemma eqRec_aux {α β : Sort u} {f : Sort u → Sort v} + {h : β = α} {h' : f α = f β} {a : f α} : h ▸ h' ▸ a = a := by + cases h; cases h'; rfl + +variable [O₁ : ∀ i, OracleInterface (pSpec₁.Message i)] + [O₂ : ∀ i, OracleInterface (pSpec₂.Message i)] + +instance instSubSpecOfProtocolSpecAppendMessage : + SubSpec ([pSpec₁.Message]ₒ ++ₒ [pSpec₂.Message]ₒ) ([(pSpec₁ ++ₚ pSpec₂).Message]ₒ) where + monadLift | query i t => match i with + | Sum.inl j => by + haveI hDoamin : [(pSpec₁ ++ₚ pSpec₂).Message]ₒ.domain j.inl = [pSpec₁.Message]ₒ.domain j := by + simp [OracleSpec.domain, MessageIdx.inl, ProtocolSpec.append, + instOracleInterfaceMessageAppend, toOracleSpec] + rw! (castMode := .all) [Fin.append_left] + congr + have : ⟨j.1, j.2⟩ = j := rfl + rw! (castMode := .all) [this] + simp [cast] + generalize_proofs h h1 h2 h3 h4 h5 + -- rw! (castMode := .all) [h5] + -- exact eqRec_aux (f := fun α => OracleInterface (Prod.snd α)) (a := O₁ j) + -- rw! (castMode := .all) [eqRec_eqRec_eq_self (a := O₁ j)] + sorry + -- rw! (castMode := .all) [h5] + letI result := query (spec := [(pSpec₁ ++ₚ pSpec₂).Message]ₒ) j.inl (cast hDoamin.symm t) + haveI hRange : [(pSpec₁ ++ₚ pSpec₂).Message]ₒ.range j.inl = Response (pSpec₁ ↑j).2 := by + simp [OracleSpec.range, toOracleSpec, ProtocolSpec.Message, MessageIdx.inl, + ProtocolSpec.append, instOracleInterfaceMessageAppend] + rw! (castMode := .all) [Fin.append_left] + congr + sorry + exact cast (congrArg _ hRange) result + | Sum.inr j => by sorry + -- simpa [OracleSpec.append, OracleSpec.range, toOracleSpec, MessageIdx.inl, + -- instOracleInterfaceMessageAppend] using + -- query (spec := [(pSpec₁ ++ₚ pSpec₂).Message]ₒ) j.inr sorry + +#print instSubSpecOfProtocolSpecAppendMessage + +end Message + +end ProtocolSpec + end Instances /-- @@ -231,37 +305,58 @@ def OracleVerifier.append (V₁ : OracleVerifier oSpec Stmt₁ OStmt₁ Stmt₂ OracleVerifier oSpec Stmt₁ OStmt₁ Stmt₃ OStmt₃ (pSpec₁ ++ₚ pSpec₂) where verify := fun stmt challenges => by -- First, invoke the first oracle verifier, handling queries as necessary - have := V₁.verify stmt (fun chal => sorry) + have := V₁.verify stmt + (fun i => by simpa [ProtocolSpec.append, ChallengeIdx.inl] using challenges i.inl) simp at this -- Then, invoke the second oracle verifier, handling queries as necessary -- Return the final output statement sorry + simulate := fun challenges => by + let sim₁ := V₁.simulate challenges.fst + let sim₂ := V₂.simulate challenges.snd + refine QueryImpl.compose ?_ sim₂ + refine SimOracle.append idOracle ?_ + (m₂ := OracleComp (oSpec ++ₒ ([OStmt₁]ₒ ++ₒ [(pSpec₁ ++ₚ pSpec₂).Message]ₒ))) + refine SimOracle.append sim₁ ?_ + -- return ⟨stmt₃, sim₂.snd⟩ + + reify := fun ⟨stmt₁, oStmt₁⟩ transcript => do + let ⟨stmt₂, oStmt₂⟩ ← V₁.run stmt₁ oStmt₁ transcript.fst + let ⟨stmt₃, oStmt₃⟩ ← V₂.run stmt₂ oStmt₂ transcript.snd + return oStmt₃ + + reify_simulate := sorry + + + + -- TODO: these stuff can go in the composition of `ofEmbed` definitions + -- Need to provide an embedding `ιₛ₃ ↪ ιₛ₁ ⊕ (pSpec₁ ++ₚ pSpec₂).MessageIdx` - embed := - -- `ιₛ₃ ↪ ιₛ₂ ⊕ pSpec₂.MessageIdx` - .trans V₂.embed <| - -- `ιₛ₂ ⊕ pSpec₂.MessageIdx ↪ (ιₛ₁ ⊕ pSpec₁.MessageIdx) ⊕ pSpec₂.MessageIdx` - .trans (.sumMap V₁.embed (.refl _)) <| - -- re-associate the sum `_ ↪ ιₛ₁ ⊕ (pSpec₁.MessageIdx ⊕ pSpec₂.MessageIdx)` - .trans (Equiv.sumAssoc _ _ _).toEmbedding <| + -- embed := + -- -- `ιₛ₃ ↪ ιₛ₂ ⊕ pSpec₂.MessageIdx` + -- .trans V₂.embed <| + -- -- `ιₛ₂ ⊕ pSpec₂.MessageIdx ↪ (ιₛ₁ ⊕ pSpec₁.MessageIdx) ⊕ pSpec₂.MessageIdx` + -- .trans (.sumMap V₁.embed (.refl _)) <| + -- -- re-associate the sum `_ ↪ ιₛ₁ ⊕ (pSpec₁.MessageIdx ⊕ pSpec₂.MessageIdx)` + -- .trans (Equiv.sumAssoc _ _ _).toEmbedding <| -- use the equivalence `pSpec₁.MessageIdx ⊕ pSpec₂.MessageIdx ≃ (pSpec₁ ++ₚ pSpec₂).MessageIdx` - .sumMap (.refl _) MessageIdx.sumEquiv.toEmbedding - - hEq := fun i => by - rcases h : V₂.embed i with j | j - · rcases h' : V₁.embed j with k | k - · have h1 := V₁.hEq j - have h2 := V₂.hEq i - simp [h, h'] at h1 h2 ⊢ - exact h2.trans h1 - · have h1 := V₁.hEq j - have h2 := V₂.hEq i - simp [h, h', MessageIdx.inl] at h1 h2 ⊢ - exact h2.trans h1 - · have := V₂.hEq i - simp [h] at this ⊢ - simp [this, MessageIdx.inr] + -- .sumMap (.refl _) MessageIdx.sumEquiv.toEmbedding + + -- hEq := fun i => by + -- rcases h : V₂.embed i with j | j + -- · rcases h' : V₁.embed j with k | k + -- · have h1 := V₁.hEq j + -- have h2 := V₂.hEq i + -- simp [h, h'] at h1 h2 ⊢ + -- exact h2.trans h1 + -- · have h1 := V₁.hEq j + -- have h2 := V₂.hEq i + -- simp [h, h', MessageIdx.inl] at h1 h2 ⊢ + -- exact h2.trans h1 + -- · have := V₂.hEq i + -- simp [h] at this ⊢ + -- simp [this, MessageIdx.inr] /-- Sequential composition of oracle reductions is just the sequential composition of the oracle provers and oracle verifiers. -/ @@ -303,13 +398,24 @@ def Extractor.Straightline.append (E₁ : Extractor.Straightline oSpec Stmt₁ W /-- The round-by-round extractor for the sequential composition of two (oracle) reductions -The nice thing is we just extend the first extractor to the concatenated protocol. The intuition is -that RBR extraction happens on the very first message, so further messages don't matter. -/ -def Extractor.RoundByRound.append (E₁ : Extractor.RoundByRound oSpec Stmt₁ Wit₁ pSpec₁) : - Extractor.RoundByRound oSpec Stmt₁ Wit₁ (pSpec₁ ++ₚ pSpec₂) := - -- (TODO: describe `Transcript.fst` and `Transcript.snd`) - fun roundIdx stmt₁ transcript proveQueryLog => - E₁ ⟨min roundIdx m, by omega⟩ stmt₁ transcript.fst proveQueryLog +The nice thing is we just extend the first extractor to the concatenated protocol. The intuition +is that RBR extraction happens on the very first message, so further messages don't matter. -/ +def Extractor.RoundByRound.append + {WitMid₁ : Fin (m + 1) → Type} {WitMid₂ : Fin (n + 1) → Type} + (E₁ : Extractor.RoundByRound oSpec Stmt₁ Wit₁ Wit₂ pSpec₁ WitMid₁) + (E₂ : Extractor.RoundByRound oSpec Stmt₂ Wit₂ Wit₃ pSpec₂ WitMid₂) : + Extractor.RoundByRound oSpec Stmt₁ Wit₁ Wit₃ (pSpec₁ ++ₚ pSpec₂) + (Fin.append (m := m) (Fin.init WitMid₁) WitMid₂ ∘ Fin.cast (by omega)) where + extractIn := sorry + extractMid := sorry + extractOut := sorry + -- fun roundIdx stmt₁ transcript proveQueryLog => do + -- let wit₂ ← E₂ stmt₂ wit₃ transcript.snd proveQueryLog verifyQueryLog + -- let wit₁ ← E₁ stmt₁ wit₂ transcript.fst proveQueryLog verifyQueryLog + -- return wit₁ + -- -- (TODO: describe `Transcript.fst` and `Transcript.snd`) + -- fun roundIdx stmt₁ transcript proveQueryLog => + -- E₁ ⟨min roundIdx m, by omega⟩ stmt₁ transcript.fst proveQueryLog variable {lang₁ : Set Stmt₁} {lang₂ : Set Stmt₂} {lang₃ : Set Stmt₃} diff --git a/ArkLib/OracleReduction/Composition/Sequential/ProtocolSpec.lean b/ArkLib/OracleReduction/Composition/Sequential/ProtocolSpec.lean index 998eb7aec..8ba6d86b4 100644 --- a/ArkLib/OracleReduction/Composition/Sequential/ProtocolSpec.lean +++ b/ArkLib/OracleReduction/Composition/Sequential/ProtocolSpec.lean @@ -49,6 +49,16 @@ theorem append_cast_right {n m : ℕ} (pSpec : ProtocolSpec n) (pSpec' : Protoco dcast h (pSpec ++ₚ pSpec') = pSpec ++ₚ (dcast (Nat.add_left_cancel h) pSpec') := by simp [append, dcast, ProtocolSpec.cast, Fin.append_cast_right] +@[simp] +theorem append_left {n m : ℕ} {pSpec : ProtocolSpec n} {pSpec' : ProtocolSpec m} (i : Fin n) : + (pSpec ++ₚ pSpec') (Fin.castAdd m i) = pSpec i := by + simp [append, Fin.append_left] + +@[simp] +theorem append_right {n m : ℕ} {pSpec : ProtocolSpec n} {pSpec' : ProtocolSpec m} (i : Fin m) : + (pSpec ++ₚ pSpec') (Fin.natAdd n i) = pSpec' i := by + simp [append, Fin.append_right] + theorem append_left_injective {pSpec : ProtocolSpec n} : Function.Injective (@ProtocolSpec.append m n · pSpec) := Fin.append_left_injective pSpec @@ -78,7 +88,6 @@ variable {pSpec₁ : ProtocolSpec m} {pSpec₂ : ProtocolSpec n} @[simp] theorem take_append_left : (pSpec₁ ++ₚ pSpec₂).take m (Nat.le_add_right m n) = pSpec₁ := by - simp only [take, append] ext i : 1 have : Fin.castLE (by omega) i = Fin.castAdd n i := rfl simp [Fin.take_apply, Fin.append_left, this] @@ -86,7 +95,6 @@ theorem take_append_left : @[simp] theorem rtake_append_right : (pSpec₁ ++ₚ pSpec₂).rtake n (Nat.le_add_left n m) = pSpec₂ := by - simp only [rtake, append] ext i : 1 simp [Fin.rtake_apply, Fin.append_right] @@ -141,7 +149,7 @@ def snoc {pSpec : ProtocolSpec n} {NextMessage : Type} @[simp] theorem take_append_left (T : FullTranscript pSpec₁) (T' : FullTranscript pSpec₂) : (T ++ₜ T').take m (Nat.le_add_right m n) = - T.cast rfl (by simp [ProtocolSpec.append]) := by + T.cast rfl (by simp) := by ext i simp [take, append, ProtocolSpec.append, Fin.castLE, Fin.addCases', Fin.addCases, FullTranscript.cast, Transcript.cast] @@ -149,7 +157,7 @@ theorem take_append_left (T : FullTranscript pSpec₁) (T' : FullTranscript pSpe @[simp] theorem rtake_append_right (T : FullTranscript pSpec₁) (T' : FullTranscript pSpec₂) : (T ++ₜ T').rtake n (Nat.le_add_left n m) = - T'.cast rfl (by simp [ProtocolSpec.append]) := by + T'.cast rfl (by simp) := by ext i simp only [ProtocolSpec.append, getType, Fin.rtake_apply, Fin.natAdd, Fin.cast_mk, rtake, append, Fin.addCases', Fin.addCases, add_tsub_cancel_right, add_lt_iff_neg_left, not_lt_zero', @@ -161,13 +169,11 @@ theorem rtake_append_right (T : FullTranscript pSpec₁) (T' : FullTranscript pS /-- The first half of a transcript for a concatenated protocol -/ def fst (T : FullTranscript (pSpec₁ ++ₚ pSpec₂)) : FullTranscript pSpec₁ := - fun i => by - simpa [ProtocolSpec.append, Fin.append_left] using T (Fin.castAdd n i) + fun i => by simpa using T (Fin.castAdd n i) /-- The second half of a transcript for a concatenated protocol -/ def snd (T : FullTranscript (pSpec₁ ++ₚ pSpec₂)) : FullTranscript pSpec₂ := - fun i => by - simpa [ProtocolSpec.append, Fin.append_right] using T (Fin.natAdd m i) + fun i => by simpa using T (Fin.natAdd m i) @[simp] theorem append_fst (T₁ : FullTranscript pSpec₁) (T₂ : FullTranscript pSpec₂) : @@ -183,53 +189,141 @@ theorem append_snd (T₁ : FullTranscript pSpec₁) (T₂ : FullTranscript pSpec end FullTranscript -def MessageIdx.inl (i : MessageIdx pSpec₁) : MessageIdx (pSpec₁ ++ₚ pSpec₂) := - ⟨Fin.castAdd n i.1, by simpa only [Fin.append_left] using i.2⟩ +namespace MessageIdx -def MessageIdx.inr (i : MessageIdx pSpec₂) : MessageIdx (pSpec₁ ++ₚ pSpec₂) := - ⟨Fin.natAdd m i.1, by simpa only [Fin.append_right] using i.2⟩ +def inl (i : MessageIdx pSpec₁) : MessageIdx (pSpec₁ ++ₚ pSpec₂) := + ⟨Fin.castAdd n i.1, by simpa using i.2⟩ + +def inr (i : MessageIdx pSpec₂) : MessageIdx (pSpec₁ ++ₚ pSpec₂) := + ⟨Fin.natAdd m i.1, by simpa using i.2⟩ @[simps!] -def MessageIdx.sumEquiv : - MessageIdx pSpec₁ ⊕ MessageIdx pSpec₂ ≃ MessageIdx (pSpec₁ ++ₚ pSpec₂) where - toFun := Sum.elim (MessageIdx.inl) (MessageIdx.inr) - invFun := fun ⟨i, h⟩ => by +def sumEquiv : + MessageIdx (pSpec₁ ++ₚ pSpec₂) ≃ MessageIdx pSpec₁ ⊕ MessageIdx pSpec₂ where + toFun := fun ⟨i, h⟩ => by by_cases hi : i < m - · simp [ProtocolSpec.append, Fin.append, Fin.addCases, hi] at h + · simp only [append, Fin.append, Fin.addCases, hi] at h exact Sum.inl ⟨⟨i, hi⟩, h⟩ - · simp [ProtocolSpec.append, Fin.append, Fin.addCases, hi] at h + · simp only [append, Fin.append, Fin.addCases, hi, eq_rec_constant] at h exact Sum.inr ⟨⟨i - m, by omega⟩, h⟩ - left_inv := fun i => by - rcases i with ⟨⟨i, isLt⟩, h⟩ | ⟨⟨i, isLt⟩, h⟩ <;> - simp [MessageIdx.inl, MessageIdx.inr, isLt] - right_inv := fun ⟨i, h⟩ => by + invFun := Sum.elim inl inr + left_inv := fun ⟨i, h⟩ => by by_cases hi : i < m <;> - simp [MessageIdx.inl, MessageIdx.inr, hi] + simp [inl, inr, hi] congr; omega + right_inv := fun i => by + rcases i with ⟨⟨i, isLt⟩, h⟩ | ⟨⟨i, isLt⟩, h⟩ <;> + simp [inl, inr, isLt] + +end MessageIdx -def ChallengeIdx.inl (i : ChallengeIdx pSpec₁) : ChallengeIdx (pSpec₁ ++ₚ pSpec₂) := +namespace Messages + +/-- The first half of the messages for a concatenated protocol -/ +def fst (m : (pSpec₁ ++ₚ pSpec₂).Messages) : pSpec₁.Messages := + fun i => by simpa [MessageIdx.inl] using m (MessageIdx.inl i) + +/-- The second half of the messages for a concatenated protocol -/ +def snd (m : (pSpec₁ ++ₚ pSpec₂).Messages) : pSpec₂.Messages := + fun i => by simpa [MessageIdx.inr] using m (MessageIdx.inr i) + +/-- The equivalence between the messages for a concatenated protocol and the tuple of messages for + the two protocols -/ +def prodEquiv : + (pSpec₁ ++ₚ pSpec₂).Messages ≃ pSpec₁.Messages × pSpec₂.Messages where + toFun := fun m => ⟨m.fst, m.snd⟩ + invFun := fun ⟨m₁, m₂⟩ => fun ⟨i, h⟩ => by + by_cases hi : i < m + · haveI : i = Fin.castAdd n ⟨i.val, hi⟩ := rfl + rw! [this] at h ⊢ + simp only [ProtocolSpec.Message, ProtocolSpec.append_left] at h ⊢ + exact m₁ ⟨⟨i.val, hi⟩, h⟩ + · haveI : i = Fin.natAdd m ⟨i.val - m, by omega⟩ := by ext; simp; omega + rw! [this] at h ⊢ + simp only [ProtocolSpec.Message, ProtocolSpec.append_right] at h ⊢ + exact m₂ ⟨⟨i.val - m, by omega⟩, h⟩ + left_inv := fun msgs => by + funext ⟨i, h⟩ + by_cases hi : i.val < m + · simp [hi, fst, MessageIdx.inl] + · simp only [hi, ↓reduceDIte, snd, Message, MessageIdx.inr, Fin.natAdd_mk] + rw! [Nat.add_sub_of_le (Nat.le_of_not_lt hi)] + simp + right_inv := fun ⟨m₁, m₂⟩ => by + simp only [MessageIdx, Message, Prod.mk.injEq] + constructor + · funext i; simp [fst, MessageIdx.inl] + · funext i; simp only [snd, MessageIdx.inr]; rw! [Nat.add_sub_self_left]; simp + +end Messages + +namespace ChallengeIdx + +def inl (i : ChallengeIdx pSpec₁) : ChallengeIdx (pSpec₁ ++ₚ pSpec₂) := ⟨Fin.castAdd n i.1, by simpa only [Fin.append_left] using i.2⟩ -def ChallengeIdx.inr (i : ChallengeIdx pSpec₂) : ChallengeIdx (pSpec₁ ++ₚ pSpec₂) := +def inr (i : ChallengeIdx pSpec₂) : ChallengeIdx (pSpec₁ ++ₚ pSpec₂) := ⟨Fin.natAdd m i.1, by simpa only [Fin.append_right] using i.2⟩ @[simps!] -def ChallengeIdx.sumEquiv : - ChallengeIdx pSpec₁ ⊕ ChallengeIdx pSpec₂ ≃ ChallengeIdx (pSpec₁ ++ₚ pSpec₂) where - toFun := Sum.elim (ChallengeIdx.inl) (ChallengeIdx.inr) - invFun := fun ⟨i, h⟩ => by +def sumEquiv : + ChallengeIdx (pSpec₁ ++ₚ pSpec₂) ≃ ChallengeIdx pSpec₁ ⊕ ChallengeIdx pSpec₂ where + toFun := fun ⟨i, h⟩ => by by_cases hi : i < m · simp [ProtocolSpec.append, Fin.append, Fin.addCases, hi] at h exact Sum.inl ⟨⟨i, hi⟩, h⟩ · simp [ProtocolSpec.append, Fin.append, Fin.addCases, hi] at h exact Sum.inr ⟨⟨i - m, by omega⟩, h⟩ - left_inv := fun i => by - rcases i with ⟨⟨i, isLt⟩, h⟩ | ⟨⟨i, isLt⟩, h⟩ <;> - simp [ChallengeIdx.inl, ChallengeIdx.inr, isLt] - right_inv := fun ⟨i, h⟩ => by + invFun := Sum.elim inl inr + left_inv := fun ⟨i, h⟩ => by by_cases hi : i < m <;> - simp [ChallengeIdx.inl, ChallengeIdx.inr, hi] + simp [inl, inr, hi] congr; omega + right_inv := fun i => by + rcases i with ⟨⟨i, isLt⟩, h⟩ | ⟨⟨i, isLt⟩, h⟩ <;> + simp [inl, inr, isLt] + +end ChallengeIdx + +namespace Challenges + +/-- The first half of the challenges for a concatenated protocol -/ +def fst (c : (pSpec₁ ++ₚ pSpec₂).Challenges) : pSpec₁.Challenges := + fun i => by simpa [ChallengeIdx.inl] using c (ChallengeIdx.inl i) + +/-- The second half of the challenges for a concatenated protocol -/ +def snd (c : (pSpec₁ ++ₚ pSpec₂).Challenges) : pSpec₂.Challenges := + fun i => by simpa [ChallengeIdx.inr] using c (ChallengeIdx.inr i) + +/-- The equivalence between the challenges for a concatenated protocol and the tuple of challenges + for the two protocols -/ +def prodEquiv : + (pSpec₁ ++ₚ pSpec₂).Challenges ≃ pSpec₁.Challenges × pSpec₂.Challenges where + toFun := fun c => ⟨c.fst, c.snd⟩ + invFun := fun ⟨c₁, c₂⟩ => fun ⟨i, h⟩ => by + by_cases hi : i < m + · haveI : i = Fin.castAdd n ⟨i.val, hi⟩ := rfl + rw! [this] at h ⊢ + simp only [ProtocolSpec.Challenge, ProtocolSpec.append_left] at h ⊢ + exact c₁ ⟨⟨i.val, hi⟩, h⟩ + · haveI : i = Fin.natAdd m ⟨i.val - m, by omega⟩ := by ext; simp; omega + rw! [this] at h ⊢ + simp only [ProtocolSpec.Challenge, ProtocolSpec.append_right] at h ⊢ + exact c₂ ⟨⟨i.val - m, by omega⟩, h⟩ + left_inv := fun challs => by + funext ⟨i, h⟩ + by_cases hi : i.val < m + · simp [hi, fst, ChallengeIdx.inl] + · simp only [hi, ↓reduceDIte, snd, Challenge, ChallengeIdx.inr, Fin.natAdd_mk] + rw! [Nat.add_sub_of_le (Nat.le_of_not_lt hi)] + simp + right_inv := fun ⟨c₁, c₂⟩ => by + simp only [ChallengeIdx, Challenge, Prod.mk.injEq] + constructor + · funext i; simp [fst, ChallengeIdx.inl] + · funext i; simp only [snd, ChallengeIdx.inr]; rw! [Nat.add_sub_self_left]; simp + +end Challenges /-- Sequential composition of a family of `ProtocolSpec`s, indexed by `i : Fin m`. diff --git a/ArkLib/OracleReduction/Execution.lean b/ArkLib/OracleReduction/Execution.lean index 85bbaf734..962e702ea 100644 --- a/ArkLib/OracleReduction/Execution.lean +++ b/ArkLib/OracleReduction/Execution.lean @@ -42,10 +42,11 @@ end loggingOracle section Execution variable {ι : Type} {oSpec : OracleSpec ι} - {StmtIn : Type} {ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} {WitIn : Type} - {StmtOut : Type} {ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} {WitOut : Type} - {n : ℕ} {pSpec : ProtocolSpec n} - [Oₛᵢ : ∀ i, OracleInterface (OStmtIn i)] + {StmtIn : Type} {ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} [Oₛᵢ : ∀ i, OracleInterface (OStmtIn i)] + {WitIn : Type} + {StmtOut : Type} {ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} [Oₛₒ : ∀ i, OracleInterface (OStmtOut i)] + {WitOut : Type} + {n : ℕ} {pSpec : ProtocolSpec n} [Oₘ : ∀ i, OracleInterface (pSpec.Message i)] /-- Prover's function for processing the next round, given the current result of the previous round. @@ -124,28 +125,43 @@ def Verifier.run (stmt : StmtIn) (transcript : FullTranscript pSpec) (verifier : Verifier oSpec StmtIn StmtOut pSpec) : OracleComp oSpec StmtOut := verifier.verify stmt transcript -/-- Run the oracle verifier in the interactive protocol. Returns the verifier's output and the log - of queries made by the verifier. +/-- Running the oracle verifier without reification. Since we do not know the input oracle + statements nor the prover's messages, we return an oracle computation (with those as oracles) of + type `StmtOut` together with a simulation strategy for `OStmtOut` in terms of the rest. + + Essentially, we call `verify` and `simulate` on the input statement & the challenges. +-/ +@[inline, specialize] +def OracleVerifier.SimulateOnly.run + (stmt : StmtIn) (challenges : pSpec.Challenges) + (verifier : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec) : + OracleComp (oSpec ++ₒ ([OStmtIn]ₒ ++ₒ [pSpec.Message]ₒ)) StmtOut × + QueryImpl [OStmtOut]ₒ (OracleComp (oSpec ++ₒ ([OStmtIn]ₒ ++ₒ [pSpec.Message]ₒ))) := + ⟨verifier.verify stmt challenges, verifier.simulate challenges⟩ + +/-- Run the oracle verifier (with reification) in an (interactive) oracle reduction. + +We take in all available information (input statement, input oracle statements, and the full +transcript), and use `verify` and `reify` to compute the output statement (non-oracle & oracle). -/ @[inline, specialize] -def OracleVerifier.run [Oₘ : ∀ i, OracleInterface (pSpec.Message i)] +def OracleVerifier.run (stmt : StmtIn) (oStmtIn : ∀ i, OStmtIn i) (transcript : FullTranscript pSpec) (verifier : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec) : - OracleComp oSpec StmtOut := do + OracleComp oSpec (StmtOut × (∀ i, OStmtOut i)) := do let f := OracleInterface.simOracle2 oSpec oStmtIn transcript.messages let stmtOut ← simulateQ f (verifier.verify stmt transcript.challenges) - return stmtOut + let oStmtOut ← verifier.reify ⟨stmt, oStmtIn⟩ transcript + return ⟨stmtOut, oStmtOut⟩ -/-- Running an oracle verifier then discarding the query list is equivalent to -running a non-oracle verifier -/ +/-- Running an oracle verifier (with reification) is definitionally equal to first converting it to + a non-oracle verifier, and then running it. -/ @[simp] -theorem OracleVerifier.run_eq_run_verifier [Oₘ : ∀ i, OracleInterface (pSpec.Message i)] +theorem OracleVerifier.run_eq_run_verifier {stmt : StmtIn} {oStmt : ∀ i, OStmtIn i} {transcript : FullTranscript pSpec} {verifier : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec} : verifier.run stmt oStmt transcript = - Prod.fst <$> verifier.toVerifier.run ⟨stmt, oStmt⟩ transcript := by - simp only [run, bind_pure, Verifier.run, toVerifier, eq_mpr_eq_cast, - bind_pure_comp, Functor.map_map, id_map'] + verifier.toVerifier.run ⟨stmt, oStmt⟩ transcript := rfl /-- An execution of an interactive reduction on a given initial statement and witness. Consists of first running the prover, and then the verifier. Returns the output statement and witness, and the @@ -190,34 +206,62 @@ theorem Reduction.runWithLog_eq_run simp [run, runWithLog, Verifier.run, Prover.runWithLog, Prover.runWithLogToRound] sorry -/-- Run an interactive oracle reduction. Returns the full transcript, the output statement and - witness, the log of all prover's oracle queries, and the log of all verifier's oracle queries to - the prover's messages and to the shared oracle. +/-- Run an interactive oracle reduction (where the oracle verifier has reification). + +Returns the full transcript, the output statement and witness, the log of all prover's oracle +queries, and the log of all verifier's oracle queries to the prover's messages and to the shared +oracle. -/ @[inline, specialize] -def OracleReduction.run [∀ i, OracleInterface (pSpec.Message i)] +def OracleReduction.run (stmt : StmtIn) (oStmt : ∀ i, OStmtIn i) (wit : WitIn) (reduction : OracleReduction oSpec StmtIn OStmtIn WitIn StmtOut OStmtOut WitOut pSpec) : OracleComp (oSpec ++ₒ [pSpec.Challenge]ₒ) - (((StmtOut × ∀ i, OStmtOut i) × WitOut) × StmtOut × FullTranscript pSpec × - QueryLog (oSpec ++ₒ [pSpec.Challenge]ₒ) × QueryLog oSpec) := do - let ⟨⟨ctxOut, transcript⟩, proveQueryLog⟩ ← - (simulateQ loggingOracle (reduction.prover.run ⟨stmt, oStmt⟩ wit)).run + (((StmtOut × ∀ i, OStmtOut i) × WitOut) × (StmtOut × ∀ i, OStmtOut i) + × FullTranscript pSpec) := do + let ⟨ctxOut, transcript⟩ ← reduction.prover.run ⟨stmt, oStmt⟩ wit + let stmtOut ← liftM <| reduction.verifier.run stmt oStmt transcript + return (ctxOut, stmtOut, transcript) + +/-- Run an interactive oracle reduction (where the oracle verifier has reification), with logging + the oracle queries of the prover and the verifier. + +Returns the full transcript, the output statement and witness, the log of all prover's oracle +queries, and the log of all verifier's oracle queries to the prover's messages and to the shared +oracle. +-/ +@[inline, specialize] +def OracleReduction.runWithLog + (stmt : StmtIn) (oStmt : ∀ i, OStmtIn i) (wit : WitIn) + (reduction : OracleReduction oSpec StmtIn OStmtIn WitIn StmtOut OStmtOut WitOut pSpec) : + OracleComp (oSpec ++ₒ [pSpec.Challenge]ₒ) + (((StmtOut × ∀ i, OStmtOut i) × WitOut) × (StmtOut × ∀ i, OStmtOut i) + × FullTranscript pSpec × QueryLog (oSpec ++ₒ [pSpec.Challenge]ₒ) × QueryLog oSpec) := do + let ⟨ctxOut, transcript, proveQueryLog⟩ ← reduction.prover.runWithLog ⟨stmt, oStmt⟩ wit let ⟨stmtOut, verifyQueryLog⟩ ← liftM (simulateQ loggingOracle (reduction.verifier.run stmt oStmt transcript)).run return (ctxOut, stmtOut, transcript, proveQueryLog, verifyQueryLog) --- /-- Running an oracle verifier then discarding the query list is equivalent to --- running a non-oracle verifier -/ --- @[simp] --- theorem OracleReduction.run_eq_run_reduction [DecidableEq ι] --- [∀ i, VCVCompatible (pSpec.Challenge i)] --- [∀ i, OracleInterface (pSpec.Message i)] {stmt : StmtIn} {wit : WitIn} --- {oracleReduction : OracleReduction pSpec oSpec StmtIn WitIn StmtOut WitOut OStmt} : --- Prod.snd <$> oracleReduction.run stmt wit = oracleReduction.toReduction.run stmt wit := by --- simp [OracleReduction.run, Reduction.run, OracleReduction.toReduction, OracleVerifier.run, --- Verifier.run, OracleVerifier.toVerifier, liftComp] +/-- Running an oracle reduction (with reification for verifier) is definitionally equal to first + converting it to a non-oracle reduction, and then running it. -/ +@[simp] +theorem OracleReduction.run_eq_run_reduction + {stmt : StmtIn} {oStmt : ∀ i, OStmtIn i} {wit : WitIn} + {oracleReduction : OracleReduction oSpec StmtIn OStmtIn WitIn StmtOut OStmtOut WitOut pSpec} : + oracleReduction.run stmt oStmt wit = + oracleReduction.toReduction.run ⟨stmt, oStmt⟩ wit := rfl + + +/-- Running an oracle reduction (with reification for verifier) with logging is definitionally equal + to first converting it to a non-oracle reduction, and then running it with logging. -/ +@[simp] +theorem OracleReduction.runWithLog_eq_runWithLog_reduction + {stmt : StmtIn} {oStmt : ∀ i, OStmtIn i} {wit : WitIn} + {oracleReduction : OracleReduction oSpec StmtIn OStmtIn WitIn StmtOut OStmtOut WitOut pSpec} : + oracleReduction.runWithLog stmt oStmt wit = + oracleReduction.toReduction.runWithLog ⟨stmt, oStmt⟩ wit := rfl +omit Oₘ in @[simp] theorem Prover.runToRound_zero_of_prover_first (stmt : StmtIn) (wit : WitIn) (prover : Prover oSpec StmtIn WitIn StmtOut WitOut pSpec) : diff --git a/ArkLib/OracleReduction/LiftContext/Lens.lean b/ArkLib/OracleReduction/LiftContext/Lens.lean index f84334c34..7601993a3 100644 --- a/ArkLib/OracleReduction/LiftContext/Lens.lean +++ b/ArkLib/OracleReduction/LiftContext/Lens.lean @@ -8,7 +8,7 @@ import ArkLib.OracleReduction.Security.Basic import ToMathlib.PFunctor.Basic /-! - ## Lens between Input and Output Contexts of (Oracle) Reductions + ## Lens between Input and Output Contexts of (Non-Oracle) Reductions This file defines the different lenses required for the transformation / lifting of context for an (oracle) reduction, and the properties required for the transformation / lift to be complete / @@ -18,9 +18,11 @@ import ToMathlib.PFunctor.Basic We also define simpler examples of lenses, when we don't need the full generality. For instance, lenses where we have (only) an equivalence between the statements / witnesses, or lenses where the witnesses are trivial. + + See `OracleLens.lean` for the definition of lenses for oracle reductions. -/ -open OracleSpec OracleComp +open OracleSpec OracleComp OracleInterface /-- A lens for transporting input and output statements for the verifier of a (non-oracle) reduction. @@ -56,74 +58,6 @@ def lift : OuterStmtIn → InnerStmtOut → OuterStmtOut := end Statement.Lens -/-- A lens for transporting input and output statements (both oracle and non-oracle) for the - oracle verifier of an oracle reduction. - - TODO: figure out the right way to define this -/ -@[inline, reducible] -def OracleStatement.Lens (OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type) - {Outer_ιₛᵢ : Type} (OuterOStmtIn : Outer_ιₛᵢ → Type) [∀ i, OracleInterface (OuterOStmtIn i)] - {Outer_ιₛₒ : Type} (OuterOStmtOut : Outer_ιₛₒ → Type) [∀ i, OracleInterface (OuterOStmtOut i)] - {Inner_ιₛᵢ : Type} (InnerOStmtIn : Inner_ιₛᵢ → Type) [∀ i, OracleInterface (InnerOStmtIn i)] - {Inner_ιₛₒ : Type} (InnerOStmtOut : Inner_ιₛₒ → Type) [∀ i, OracleInterface (InnerOStmtOut i)] - := - Statement.Lens (OuterStmtIn × ∀ i, OuterOStmtIn i) (OuterStmtOut × ∀ i, OuterOStmtOut i) - (InnerStmtIn × ∀ i, InnerOStmtIn i) (InnerStmtOut × ∀ i, InnerOStmtOut i) - -- TODO: fill in the extra conditions - /- Basically, as we model the output oracle statement as a subset of the input oracle statement + - the prover's messages, we need to make sure that this subset relation is satisfied in the - statement lens mapping. - - We also need to provide a `QueryImpl` instance for simulating the outer oracle verifier using - the inner oracle verifier. - -/ - - -- simOStmt : QueryImpl [InnerOStmtIn]ₒ - -- (ReaderT OuterStmtIn (OracleComp [OuterOStmtIn]ₒ)) - - -- simOStmt_neverFails : ∀ i, ∀ t, ∀ outerStmtIn, - -- ((simOStmt.impl (query i t)).run outerStmtIn).neverFails - -- To get back an output oracle statement in the outer context, we may simulate it using the input - -- (non-oracle) statement of the outer context, the output (non-oracle) statement of the inner - -- context, along with oracle access to the inner output oracle statements - - -- liftOStmt : QueryImpl [OuterOStmtOut]ₒ - -- (ReaderT (OuterStmtIn × InnerStmtOut) (OracleComp ([OuterOStmtIn]ₒ ++ₒ [InnerOStmtOut]ₒ))) - -- liftOStmt_neverFails : ∀ i, ∀ t, ∀ outerStmtIn, ∀ innerStmtOut, - -- ((liftOStmt.impl (query i t)).run (outerStmtIn, innerStmtOut)).neverFails - -namespace OracleStatement.Lens - -variable {OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type} - {Outer_ιₛᵢ : Type} {OuterOStmtIn : Outer_ιₛᵢ → Type} [∀ i, OracleInterface (OuterOStmtIn i)] - {Outer_ιₛₒ : Type} {OuterOStmtOut : Outer_ιₛₒ → Type} [∀ i, OracleInterface (OuterOStmtOut i)] - {Inner_ιₛᵢ : Type} {InnerOStmtIn : Inner_ιₛᵢ → Type} [∀ i, OracleInterface (InnerOStmtIn i)] - {Inner_ιₛₒ : Type} {InnerOStmtOut : Inner_ιₛₒ → Type} [∀ i, OracleInterface (InnerOStmtOut i)] - (lens : OracleStatement.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut - OuterOStmtIn OuterOStmtOut InnerOStmtIn InnerOStmtOut) -/-- Transport input statements from the outer context to the inner context - -TODO: refactor etc. -/ -@[inline, reducible] -def proj : OuterStmtIn × (∀ i, OuterOStmtIn i) → InnerStmtIn × (∀ i, InnerOStmtIn i) := - lens.toFunA - -/-- Transport output statements from the inner context to the outer context, - additionally relying on the input statements of the outer context. - - TODO: refactor etc. -/ -@[inline, reducible] -def lift : OuterStmtIn × (∀ i, OuterOStmtIn i) → InnerStmtOut × (∀ i, InnerOStmtOut i) → - OuterStmtOut × (∀ i, OuterOStmtOut i) := - lens.toFunB - --- def toVerifierLens : Statement.Lens --- (OuterStmtIn × ∀ i, OuterOStmtIn i) (OuterStmtOut × ∀ i, OuterOStmtOut i) --- (InnerStmtIn × ∀ i, InnerOStmtIn i) (InnerStmtOut × ∀ i, InnerOStmtOut i) --- := oStmtLens - -end OracleStatement.Lens - /-- Lenses for transporting the input & output witnesses from an inner protocol to an outer protocol. @@ -186,53 +120,6 @@ def lift : OuterStmtIn × OuterWitIn → InnerStmtOut × InnerWitOut → OuterSt end Context.Lens -/-- A structure collecting a lens for the prover, and a lens for the oracle verifier, for - transporting between the contexts of an outer oracle reduction and an inner oracle reduction. -/ -structure OracleContext.Lens (OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type) - {Outer_ιₛᵢ : Type} (OuterOStmtIn : Outer_ιₛᵢ → Type) [∀ i, OracleInterface (OuterOStmtIn i)] - {Outer_ιₛₒ : Type} (OuterOStmtOut : Outer_ιₛₒ → Type) [∀ i, OracleInterface (OuterOStmtOut i)] - {Inner_ιₛᵢ : Type} (InnerOStmtIn : Inner_ιₛᵢ → Type) [∀ i, OracleInterface (InnerOStmtIn i)] - {Inner_ιₛₒ : Type} (InnerOStmtOut : Inner_ιₛₒ → Type) [∀ i, OracleInterface (InnerOStmtOut i)] - (OuterWitIn OuterWitOut InnerWitIn InnerWitOut : Type) where - stmt : OracleStatement.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut - OuterOStmtIn OuterOStmtOut InnerOStmtIn InnerOStmtOut - wit : Witness.Lens (OuterStmtIn × ∀ i, OuterOStmtIn i) (InnerStmtOut × ∀ i, InnerOStmtOut i) - OuterWitIn OuterWitOut InnerWitIn InnerWitOut - -namespace OracleContext.Lens - -variable {OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type} - {Outer_ιₛᵢ : Type} {OuterOStmtIn : Outer_ιₛᵢ → Type} [∀ i, OracleInterface (OuterOStmtIn i)] - {Outer_ιₛₒ : Type} {OuterOStmtOut : Outer_ιₛₒ → Type} [∀ i, OracleInterface (OuterOStmtOut i)] - {Inner_ιₛᵢ : Type} {InnerOStmtIn : Inner_ιₛᵢ → Type} [∀ i, OracleInterface (InnerOStmtIn i)] - {Inner_ιₛₒ : Type} {InnerOStmtOut : Inner_ιₛₒ → Type} [∀ i, OracleInterface (InnerOStmtOut i)] - {OuterWitIn OuterWitOut InnerWitIn InnerWitOut : Type} - (lens : OracleContext.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut - OuterOStmtIn OuterOStmtOut InnerOStmtIn InnerOStmtOut - OuterWitIn OuterWitOut InnerWitIn InnerWitOut) -/-- Projection of the context. -/ -@[inline, reducible] -def proj : (OuterStmtIn × (∀ i, OuterOStmtIn i)) × OuterWitIn → - (InnerStmtIn × (∀ i, InnerOStmtIn i)) × InnerWitIn := - fun ctxIn => ⟨lens.stmt.proj ctxIn.1, lens.wit.proj ctxIn⟩ - -/-- Lifting of the context. -/ -@[inline, reducible] -def lift : (OuterStmtIn × (∀ i, OuterOStmtIn i)) × OuterWitIn → - (InnerStmtOut × (∀ i, InnerOStmtOut i)) × InnerWitOut → - (OuterStmtOut × (∀ i, OuterOStmtOut i)) × OuterWitOut := - fun ctxIn ctxOut => ⟨lens.stmt.lift ctxIn.1 ctxOut.1, lens.wit.lift ctxIn ctxOut⟩ - -/-- Convert the oracle context lens to a context lens. -/ -@[inline, reducible] -def toContext : - Context.Lens (OuterStmtIn × (∀ i, OuterOStmtIn i)) (OuterStmtOut × (∀ i, OuterOStmtOut i)) - (InnerStmtIn × (∀ i, InnerOStmtIn i)) (InnerStmtOut × (∀ i, InnerOStmtOut i)) - OuterWitIn OuterWitOut InnerWitIn InnerWitOut := - ⟨lens.stmt, lens.wit⟩ - -end OracleContext.Lens - /-- Lens for lifting the witness extraction procedure from the inner reduction to the outer reduction. @@ -289,15 +176,6 @@ def proj (lens : Extractor.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOu OuterStmtIn × OuterWitOut → InnerStmtIn × InnerWitOut := fun ⟨stmtIn, witOut⟩ => ⟨lens.stmt.proj stmtIn, lens.wit.proj (stmtIn, witOut)⟩ --- /-- Transport the inner input witness to the outer input witness, also relying on the tuple --- (outer-- input statement, outer output witness) -/ --- @[inline, reducible] --- def lift (lens : Extractor.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut --- OuterWitIn OuterWitOut InnerWitIn InnerWitOut) : --- OuterStmtIn × OuterWitOut → InnerWitIn → OuterWitIn := --- fun ⟨stmtIn, witOut⟩ innerWitIn => --- lens.wit.lift (stmtIn, witOut) innerWitIn - end Extractor.Lens /-- Conditions for the lens / transformation to preserve completeness @@ -325,26 +203,6 @@ class Context.Lens.IsComplete {OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut (lens.stmt.lift outerStmtIn innerStmtOut, lens.wit.lift (outerStmtIn, outerWitIn) (innerStmtOut, innerWitOut)) ∈ outerRelOut -/-- The completeness condition for the oracle context lens is just the one for the underlying - context lens -/ -@[reducible, simp] -def OracleContext.Lens.IsComplete {OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type} - {Outer_ιₛᵢ : Type} {OuterOStmtIn : Outer_ιₛᵢ → Type} [∀ i, OracleInterface (OuterOStmtIn i)] - {Outer_ιₛₒ : Type} {OuterOStmtOut : Outer_ιₛₒ → Type} [∀ i, OracleInterface (OuterOStmtOut i)] - {Inner_ιₛᵢ : Type} {InnerOStmtIn : Inner_ιₛᵢ → Type} [∀ i, OracleInterface (InnerOStmtIn i)] - {Inner_ιₛₒ : Type} {InnerOStmtOut : Inner_ιₛₒ → Type} [∀ i, OracleInterface (InnerOStmtOut i)] - {OuterWitIn OuterWitOut InnerWitIn InnerWitOut : Type} - (outerRelIn : Set ((OuterStmtIn × (∀ i, OuterOStmtIn i)) × OuterWitIn)) - (innerRelIn : Set ((InnerStmtIn × (∀ i, InnerOStmtIn i)) × InnerWitIn)) - (outerRelOut : Set ((OuterStmtOut × (∀ i, OuterOStmtOut i)) × OuterWitOut)) - (innerRelOut : Set ((InnerStmtOut × (∀ i, InnerOStmtOut i)) × InnerWitOut)) - (compat : (OuterStmtIn × (∀ i, OuterOStmtIn i)) × OuterWitIn → - (InnerStmtOut × (∀ i, InnerOStmtOut i)) × InnerWitOut → Prop) - (lens : OracleContext.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut - OuterOStmtIn OuterOStmtOut InnerOStmtIn InnerOStmtOut - OuterWitIn OuterWitOut InnerWitIn InnerWitOut) := - Context.Lens.IsComplete outerRelIn innerRelIn outerRelOut innerRelOut compat lens.toContext - /-- Conditions for the lens / transformation to preserve soundness -/ class Statement.Lens.IsSound {OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type} (outerLangIn : Set OuterStmtIn) (outerLangOut : Set OuterStmtOut) @@ -360,24 +218,6 @@ class Statement.Lens.IsSound {OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut innerStmtOut ∉ innerLangOut → lens.lift outerStmtIn innerStmtOut ∉ outerLangOut -/-- The soundness condition for the oracle statement lens is just the one for the underlying - statement lens -/ -@[reducible, simp] -def OracleStatement.Lens.IsSound {OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type} - {Outer_ιₛᵢ : Type} {OuterOStmtIn : Outer_ιₛᵢ → Type} [∀ i, OracleInterface (OuterOStmtIn i)] - {Outer_ιₛₒ : Type} {OuterOStmtOut : Outer_ιₛₒ → Type} [∀ i, OracleInterface (OuterOStmtOut i)] - {Inner_ιₛᵢ : Type} {InnerOStmtIn : Inner_ιₛᵢ → Type} [∀ i, OracleInterface (InnerOStmtIn i)] - {Inner_ιₛₒ : Type} {InnerOStmtOut : Inner_ιₛₒ → Type} [∀ i, OracleInterface (InnerOStmtOut i)] - (outerLangIn : Set (OuterStmtIn × (∀ i, OuterOStmtIn i))) - (outerLangOut : Set (OuterStmtOut × (∀ i, OuterOStmtOut i))) - (innerLangIn : Set (InnerStmtIn × (∀ i, InnerOStmtIn i))) - (innerLangOut : Set (InnerStmtOut × (∀ i, InnerOStmtOut i))) - (compatStmt : - OuterStmtIn × (∀ i, OuterOStmtIn i) → InnerStmtOut × (∀ i, InnerOStmtOut i) → Prop) - (lens : OracleStatement.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut - OuterOStmtIn OuterOStmtOut InnerOStmtIn InnerOStmtOut) := - Statement.Lens.IsSound outerLangIn outerLangOut innerLangIn innerLangOut compatStmt lens - /-- Conditions for the extractor lens to preserve knowledge soundness -/ class Extractor.Lens.IsKnowledgeSound {OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type} @@ -446,31 +286,7 @@ end Extractor.Lens.IsKnowledgeSound section SpecialCases --- Plan (do not delete) - --- 1. When the lens is over the input context only (keeping the output the same) --- 1.1. Over the input statement only --- 1.1.1. When the map is an equivalence --- 1.2. Over the input witness only --- 1.2.1. When the map is an equivalence - --- TODO for oracle statements as we haven't figured it out - --- 2. When the lens is over the output context only (keeping the input the same) --- 2.1. Over the output statement only --- 2.1.1. When the map is an equivalence --- 2.2. Over the output witness only --- 2.2.1. When the map is an equivalence - --- When does this lead to secure protocols? Since one of input / output is trivial, this essentially --- reduces to the security of the zero-round reduction (that is either the on the input or the --- output context) - variable {OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type} - {Outer_ιₛᵢ : Type} {OuterOStmtIn : Outer_ιₛᵢ → Type} [∀ i, OracleInterface (OuterOStmtIn i)] - {Outer_ιₛₒ : Type} {OuterOStmtOut : Outer_ιₛₒ → Type} [∀ i, OracleInterface (OuterOStmtOut i)] - {Inner_ιₛᵢ : Type} {InnerOStmtIn : Inner_ιₛᵢ → Type} [∀ i, OracleInterface (InnerOStmtIn i)] - {Inner_ιₛₒ : Type} {InnerOStmtOut : Inner_ιₛₒ → Type} [∀ i, OracleInterface (InnerOStmtOut i)] {OuterWitIn OuterWitOut InnerWitIn InnerWitOut : Type} namespace Statement.Lens @@ -499,41 +315,6 @@ def ofOutputOnly (liftStmt : OuterStmtIn → InnerStmtOut → OuterStmtOut) : end Statement.Lens -namespace OracleStatement.Lens - --- TODO: replace with new definitions when we figure out the right definition for oracle statements --- lens - -/-- The identity lens for the statement, which acts as identity on the input and output. -/ -@[inline, reducible] -protected def id : - OracleStatement.Lens OuterStmtIn OuterStmtOut OuterStmtIn OuterStmtOut - OuterOStmtIn OuterOStmtOut OuterOStmtIn OuterOStmtOut := - PFunctor.Lens.id _ - -alias trivial := OracleStatement.Lens.id - -/-- Lens for the statement which keeps the output the same, and hence only requires a - projection on the input. -/ -@[inline] -def ofInputOnly - (projStmt : OuterStmtIn × (∀ i, OuterOStmtIn i) → InnerStmtIn × (∀ i, InnerOStmtIn i)) : - OracleStatement.Lens OuterStmtIn OuterStmtOut InnerStmtIn OuterStmtOut - OuterOStmtIn OuterOStmtOut InnerOStmtIn OuterOStmtOut := - ⟨projStmt, fun _ => id⟩ - -/-- Lens for the statement which keeps the input the same, and hence only requires a - lift on the output. -/ -@[inline] -def ofOutputOnly - (liftStmt : OuterStmtIn × (∀ i, OuterOStmtIn i) → InnerStmtOut × (∀ i, InnerOStmtOut i) → - OuterStmtOut × (∀ i, OuterOStmtOut i)) : - OracleStatement.Lens OuterStmtIn OuterStmtOut OuterStmtIn InnerStmtOut - OuterOStmtIn OuterOStmtOut OuterOStmtIn InnerOStmtOut := - ⟨id, liftStmt⟩ - -end OracleStatement.Lens - namespace Witness.Lens /-- The identity lens for the witness, which acts as projection from the context (statement + @@ -627,47 +408,6 @@ def ofOutputOnly end Context.Lens -namespace OracleContext.Lens - -/-- The identity lens for the context, which combines the identity statement and witness lenses. -/ -@[inline, reducible] -protected def id : - OracleContext.Lens OuterStmtIn OuterStmtOut OuterStmtIn OuterStmtOut - OuterOStmtIn OuterOStmtOut OuterOStmtIn OuterOStmtOut - OuterWitIn OuterWitOut OuterWitIn OuterWitOut where - stmt := OracleStatement.Lens.id - wit := Witness.Lens.id - -alias trivial := OracleContext.Lens.id - -/-- Lens for the oracle context which keeps the output contexts the same, and only requires - projections on the statement & witness for the input. -/ -@[inline] -def ofInputOnly - (stmtProj : OuterStmtIn × (∀ i, OuterOStmtIn i) → InnerStmtIn × (∀ i, InnerOStmtIn i)) - (witProj : (OuterStmtIn × (∀ i, OuterOStmtIn i)) × OuterWitIn → InnerWitIn) : - OracleContext.Lens OuterStmtIn OuterStmtOut InnerStmtIn OuterStmtOut - OuterOStmtIn OuterOStmtOut InnerOStmtIn OuterOStmtOut - OuterWitIn OuterWitOut InnerWitIn OuterWitOut where - stmt := OracleStatement.Lens.ofInputOnly stmtProj - wit := Witness.Lens.ofInputOnly witProj - -/-- Lens for the oracle context which keeps the input contexts the same, and only requires lifts on - the statement & witness for the output. -/ -@[inline] -def ofOutputOnly - (stmtLift : OuterStmtIn × (∀ i, OuterOStmtIn i) → InnerStmtOut × (∀ i, InnerOStmtOut i) → - OuterStmtOut × (∀ i, OuterOStmtOut i)) - (witLift : (OuterStmtIn × (∀ i, OuterOStmtIn i)) × OuterWitIn → - (InnerStmtOut × (∀ i, InnerOStmtOut i)) × InnerWitOut → OuterWitOut) : - OracleContext.Lens OuterStmtIn OuterStmtOut OuterStmtIn InnerStmtOut - OuterOStmtIn OuterOStmtOut OuterOStmtIn InnerOStmtOut - OuterWitIn OuterWitOut OuterWitIn InnerWitOut where - stmt := OracleStatement.Lens.ofOutputOnly stmtLift - wit := Witness.Lens.ofOutputOnly witLift - -end OracleContext.Lens - namespace Extractor.Lens /-- The identity lens for the extractor on the witness, given a statement lens. -/ diff --git a/ArkLib/OracleReduction/LiftContext/OracleLens.lean b/ArkLib/OracleReduction/LiftContext/OracleLens.lean new file mode 100644 index 000000000..2c5cffd3c --- /dev/null +++ b/ArkLib/OracleReduction/LiftContext/OracleLens.lean @@ -0,0 +1,348 @@ +/- +Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Quang Dao +-/ + +import ArkLib.OracleReduction.LiftContext.Lens +import ArkLib.ToVCVio.Oracle + +/-! + # Lenses for Oracle Reductions + + This file defines the `OracleStatement.Lens` and `OracleContext.Lens` that are necessary to lift + the context of oracle reductions. + + Defining lenses in this setting is more complicated than in the non-oracle setting, because we + need to provide two separate components, mappings on the underlying data and oracle simulations on + the oracle interfaces. We also need those two components to be compatible with each other. +-/ + +open OracleSpec OracleComp OracleInterface + +namespace OracleStatement + +variable (OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type) + {Outer_ιₛᵢ : Type} (OuterOStmtIn : Outer_ιₛᵢ → Type) + [Outer_Oₛᵢ : ∀ i, OracleInterface (OuterOStmtIn i)] + {Outer_ιₛₒ : Type} (OuterOStmtOut : Outer_ιₛₒ → Type) + [Outer_Oₛₒ : ∀ i, OracleInterface (OuterOStmtOut i)] + {Inner_ιₛᵢ : Type} (InnerOStmtIn : Inner_ιₛᵢ → Type) + [Inner_Oₛᵢ : ∀ i, OracleInterface (InnerOStmtIn i)] + {Inner_ιₛₒ : Type} (InnerOStmtOut : Inner_ιₛₒ → Type) + [Inner_Oₛₒ : ∀ i, OracleInterface (InnerOStmtOut i)] + +namespace Lens + +/-- A lens for transporting input and output statements (both oracle and non-oracle) for the + prover of an oracle reduction. This operates on the underlying data. -/ +@[inline, reducible] +def Prover := + Statement.Lens (OuterStmtIn × ∀ i, OuterOStmtIn i) (OuterStmtOut × ∀ i, OuterOStmtOut i) + (InnerStmtIn × ∀ i, InnerOStmtIn i) (InnerStmtOut × ∀ i, InnerOStmtOut i) + +namespace Prover + +variable {OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut} + {Outer_ιₛᵢ : Type} {OuterOStmtIn : Outer_ιₛᵢ → Type} + {Outer_ιₛₒ : Type} {OuterOStmtOut : Outer_ιₛₒ → Type} + {Inner_ιₛᵢ : Type} {InnerOStmtIn : Inner_ιₛᵢ → Type} + {Inner_ιₛₒ : Type} {InnerOStmtOut : Inner_ιₛₒ → Type} + (lensP : Prover OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut + OuterOStmtIn OuterOStmtOut InnerOStmtIn InnerOStmtOut) + +/-- Projection for the main statement part for the prover's lens. -/ +@[inline, reducible] +def projStmt : OuterStmtIn × (∀ i, OuterOStmtIn i) → InnerStmtIn := + Prod.fst ∘ lensP.proj + +/-- Projection for the oracle statement part for the prover's lens. -/ +@[inline, reducible] +def projOStmt : OuterStmtIn × (∀ i, OuterOStmtIn i) → ∀ i, InnerOStmtIn i := + Prod.snd ∘ lensP.proj + +/-- Lifting for the main statement part for the prover's lens. -/ +@[inline, reducible] +def liftStmt : OuterStmtIn × (∀ i, OuterOStmtIn i) → InnerStmtOut × (∀ i, InnerOStmtOut i) → + OuterStmtOut := + fun a b => (lensP.lift a b).1 + +/-- Lifting for the oracle statement part for the prover's lens. -/ +@[inline, reducible] +def liftOStmt : OuterStmtIn × (∀ i, OuterOStmtIn i) → InnerStmtOut × (∀ i, InnerOStmtOut i) → + ∀ i, OuterOStmtOut i := + fun a b => (lensP.lift a b).2 + +end Prover + +/-- The lens for transporting the oracle statements for the oracle verifier. + +Unlike the one for the prover, this only has the simulation for the oracles corresponding to the +oracle statements, and not actual functions returning the underlying data. + +We will define a compatibility condition between the two (map on data and oracle simulation). -/ +structure Verifier where + /-- Projection of the outer statement to the inner statement, with oracle access to the input + oracle statement. -/ + projStmt : OuterStmtIn → OracleComp [OuterOStmtIn]ₒ InnerStmtIn + + /-- Projection of the outer oracle statement to the inner oracle statement, which takes in the + outer input (non-oracle) statement and returns a simulation of the inner oracle statement in + terms of the outer oracle statement. + + NOTE: we would like `OuterStmtIn → `this. Cannot have this for now since + `OracleVerifier.simulate` is also not as general as we want. -/ + projOStmt : QueryImpl [InnerOStmtIn]ₒ (OracleComp [OuterOStmtIn]ₒ) + + /-- Lifting of the outer statement to the inner statement, with oracle access to the input + oracle statement. -/ + liftStmt : OuterStmtIn → InnerStmtOut → + OracleComp ([OuterOStmtIn]ₒ ++ₒ [InnerOStmtOut]ₒ) OuterStmtOut + + /-- Lifting of the inner output oracle statement to outer one. Expressed as an oracle simulation + of `OuterOStmtOut` in terms of `OuterOStmtIn` and `InnerOStmtOut`. + + NOTE: ideally, we would also have `OuterStmtIn → InnerStmtOut → ` this. Need to drop this for now + since `OracleVerifier.simulate` definition is also not as general as we want. -/ + liftOStmt : QueryImpl [OuterOStmtOut]ₒ (OracleComp ([OuterOStmtIn]ₒ ++ₒ [InnerOStmtOut]ₒ)) + +/-- The oracle statement lenses for the prover and verifier are **compatible** if the verifier's +oracle-based "simulation" of the statement transformation matches the prover's data-level +"reification" when the oracles are instantiated with the prover's data. + +This is broken down into four conditions: + +- `projStmt_compatible`: The verifier's simulated projection of the main statement, when run with + the actual outer oracle data, must produce the same inner statement as the prover's direct + data-level projection. + +- `projOStmt_compatible`: Querying the verifier's *simulated* inner oracle statement must yield the + same response as querying the *actual* inner oracle data produced by the prover's lens. + +- `liftStmt_compatible`: The verifier's simulated lift of the main statement, when run with the + actual outer input and inner output oracle data, must produce the same outer output statement as + the prover's direct data-level lift. + +- `liftOStmt_compatible`: Querying the verifier's *simulated* outer output oracle statement must + yield the same response as querying the *actual* outer output oracle data produced by the prover's + lens. -/ +class IsCompatible + {OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type} + {Outer_ιₛᵢ : Type} {OuterOStmtIn : Outer_ιₛᵢ → Type} + [Outer_Oₛᵢ : ∀ i, OracleInterface (OuterOStmtIn i)] + {Outer_ιₛₒ : Type} {OuterOStmtOut : Outer_ιₛₒ → Type} + [Outer_Oₛₒ : ∀ i, OracleInterface (OuterOStmtOut i)] + {Inner_ιₛᵢ : Type} {InnerOStmtIn : Inner_ιₛᵢ → Type} + [Inner_Oₛᵢ : ∀ i, OracleInterface (InnerOStmtIn i)] + {Inner_ιₛₒ : Type} {InnerOStmtOut : Inner_ιₛₒ → Type} + [Inner_Oₛₒ : ∀ i, OracleInterface (InnerOStmtOut i)] + (lensP : Prover OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut + OuterOStmtIn OuterOStmtOut InnerOStmtIn InnerOStmtOut) + (lensV : Verifier OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut + OuterOStmtIn OuterOStmtOut InnerOStmtIn InnerOStmtOut) where + + projStmt : ∀ outerStmtIn outerOStmtIn, + runWithOracle (fun i => oracle (outerOStmtIn i)) (lensV.projStmt outerStmtIn) + = some (lensP.projStmt ⟨outerStmtIn, outerOStmtIn⟩) + + projOStmt : ∀ outerStmtIn outerOStmtIn i t, + runWithOracle (fun i => oracle (outerOStmtIn i)) + (simulateQ (lensV.projOStmt) (query (spec := [InnerOStmtIn]ₒ) i t)) + = some ((Inner_Oₛᵢ i).oracle ((lensP.projOStmt ⟨outerStmtIn, outerOStmtIn⟩) i) t) + + liftStmt : ∀ outerStmtIn outerOStmtIn innerStmtOut innerOStmtOut, + runWithOracle + (fun i => match i with + | .inl j => oracle (outerOStmtIn j) + | .inr j => oracle (innerOStmtOut j)) + (lensV.liftStmt outerStmtIn innerStmtOut) + = some (lensP.liftStmt ⟨outerStmtIn, outerOStmtIn⟩ ⟨innerStmtOut, innerOStmtOut⟩) + + liftOStmt : ∀ outerStmtIn outerOStmtIn innerStmtOut innerOStmtOut i t, + runWithOracle (fun i => match i with + | .inl j => oracle (outerOStmtIn j) + | .inr j => oracle (innerOStmtOut j)) + (simulateQ (lensV.liftOStmt) (query (spec := [OuterOStmtOut]ₒ) i t)) + = some + ((Outer_Oₛₒ i).oracle + ((lensP.liftOStmt ⟨outerStmtIn, outerOStmtIn⟩ ⟨innerStmtOut, innerOStmtOut⟩) i) t) + +end Lens + +structure Lens where + prover : Lens.Prover OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut + OuterOStmtIn OuterOStmtOut InnerOStmtIn InnerOStmtOut + verifier : Lens.Verifier OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut + OuterOStmtIn OuterOStmtOut InnerOStmtIn InnerOStmtOut + [is_compatible : Lens.IsCompatible prover verifier] + +attribute [instance] Lens.is_compatible + +namespace Lens + +variable {OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type} + {Outer_ιₛᵢ : Type} {OuterOStmtIn : Outer_ιₛᵢ → Type} + [Outer_Oₛᵢ : ∀ i, OracleInterface (OuterOStmtIn i)] + {Outer_ιₛₒ : Type} {OuterOStmtOut : Outer_ιₛₒ → Type} + [Outer_Oₛₒ : ∀ i, OracleInterface (OuterOStmtOut i)] + {Inner_ιₛᵢ : Type} {InnerOStmtIn : Inner_ιₛᵢ → Type} + [Inner_Oₛᵢ : ∀ i, OracleInterface (InnerOStmtIn i)] + {Inner_ιₛₒ : Type} {InnerOStmtOut : Inner_ιₛₒ → Type} + [Inner_Oₛₒ : ∀ i, OracleInterface (InnerOStmtOut i)] + (lens : Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut + OuterOStmtIn OuterOStmtOut InnerOStmtIn InnerOStmtOut) + +/-- Convert the oracle statement lens to a statement lens. -/ +@[inline, reducible] +def toStatement : Statement.Lens + (OuterStmtIn × (∀ i, OuterOStmtIn i)) (OuterStmtOut × (∀ i, OuterOStmtOut i)) + (InnerStmtIn × (∀ i, InnerOStmtIn i)) (InnerStmtOut × (∀ i, InnerOStmtOut i)) := + lens.prover + +end Lens + +end OracleStatement + +/-- A structure collecting a lens for the prover, and a lens for the oracle verifier, for + transporting between the contexts of an outer oracle reduction and an inner oracle reduction. -/ +structure OracleContext.Lens (OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type) + {Outer_ιₛᵢ : Type} (OuterOStmtIn : Outer_ιₛᵢ → Type) + [Outer_Oₛᵢ : ∀ i, OracleInterface (OuterOStmtIn i)] + {Outer_ιₛₒ : Type} (OuterOStmtOut : Outer_ιₛₒ → Type) + [Outer_Oₛₒ : ∀ i, OracleInterface (OuterOStmtOut i)] + {Inner_ιₛᵢ : Type} (InnerOStmtIn : Inner_ιₛᵢ → Type) + [Inner_Oₛᵢ : ∀ i, OracleInterface (InnerOStmtIn i)] + {Inner_ιₛₒ : Type} (InnerOStmtOut : Inner_ιₛₒ → Type) + [Inner_Oₛₒ : ∀ i, OracleInterface (InnerOStmtOut i)] + (OuterWitIn OuterWitOut InnerWitIn InnerWitOut : Type) where + stmt : OracleStatement.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut + OuterOStmtIn OuterOStmtOut InnerOStmtIn InnerOStmtOut + wit : Witness.Lens (OuterStmtIn × ∀ i, OuterOStmtIn i) (InnerStmtOut × ∀ i, InnerOStmtOut i) + OuterWitIn OuterWitOut InnerWitIn InnerWitOut + +namespace OracleContext.Lens + +variable {OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type} + {Outer_ιₛᵢ : Type} {OuterOStmtIn : Outer_ιₛᵢ → Type} [∀ i, OracleInterface (OuterOStmtIn i)] + {Outer_ιₛₒ : Type} {OuterOStmtOut : Outer_ιₛₒ → Type} [∀ i, OracleInterface (OuterOStmtOut i)] + {Inner_ιₛᵢ : Type} {InnerOStmtIn : Inner_ιₛᵢ → Type} [∀ i, OracleInterface (InnerOStmtIn i)] + {Inner_ιₛₒ : Type} {InnerOStmtOut : Inner_ιₛₒ → Type} [∀ i, OracleInterface (InnerOStmtOut i)] + {OuterWitIn OuterWitOut InnerWitIn InnerWitOut : Type} + (lens : OracleContext.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut + OuterOStmtIn OuterOStmtOut InnerOStmtIn InnerOStmtOut + OuterWitIn OuterWitOut InnerWitIn InnerWitOut) + +/-- Projection of the context. -/ +@[inline, reducible] +def proj : (OuterStmtIn × (∀ i, OuterOStmtIn i)) × OuterWitIn → + (InnerStmtIn × (∀ i, InnerOStmtIn i)) × InnerWitIn := + fun ctxIn => ⟨lens.stmt.prover.proj ctxIn.1, lens.wit.proj ctxIn⟩ + +/-- Lifting of the context. -/ +@[inline, reducible] +def lift : (OuterStmtIn × (∀ i, OuterOStmtIn i)) × OuterWitIn → + (InnerStmtOut × (∀ i, InnerOStmtOut i)) × InnerWitOut → + (OuterStmtOut × (∀ i, OuterOStmtOut i)) × OuterWitOut := + fun ctxIn ctxOut => ⟨lens.stmt.prover.lift ctxIn.1 ctxOut.1, lens.wit.lift ctxIn ctxOut⟩ + +/-- Convert the oracle context lens to a context lens. -/ +@[inline, reducible] +def toContext : + Context.Lens (OuterStmtIn × (∀ i, OuterOStmtIn i)) (OuterStmtOut × (∀ i, OuterOStmtOut i)) + (InnerStmtIn × (∀ i, InnerOStmtIn i)) (InnerStmtOut × (∀ i, InnerOStmtOut i)) + OuterWitIn OuterWitOut InnerWitIn InnerWitOut := + ⟨lens.stmt.prover, lens.wit⟩ + +end OracleContext.Lens + +/-- The completeness condition for the oracle context lens is just the one for the underlying + context lens -/ +@[reducible, simp] +def OracleContext.Lens.IsComplete {OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type} + {Outer_ιₛᵢ : Type} {OuterOStmtIn : Outer_ιₛᵢ → Type} [∀ i, OracleInterface (OuterOStmtIn i)] + {Outer_ιₛₒ : Type} {OuterOStmtOut : Outer_ιₛₒ → Type} [∀ i, OracleInterface (OuterOStmtOut i)] + {Inner_ιₛᵢ : Type} {InnerOStmtIn : Inner_ιₛᵢ → Type} [∀ i, OracleInterface (InnerOStmtIn i)] + {Inner_ιₛₒ : Type} {InnerOStmtOut : Inner_ιₛₒ → Type} [∀ i, OracleInterface (InnerOStmtOut i)] + {OuterWitIn OuterWitOut InnerWitIn InnerWitOut : Type} + (outerRelIn : Set ((OuterStmtIn × (∀ i, OuterOStmtIn i)) × OuterWitIn)) + (innerRelIn : Set ((InnerStmtIn × (∀ i, InnerOStmtIn i)) × InnerWitIn)) + (outerRelOut : Set ((OuterStmtOut × (∀ i, OuterOStmtOut i)) × OuterWitOut)) + (innerRelOut : Set ((InnerStmtOut × (∀ i, InnerOStmtOut i)) × InnerWitOut)) + (compat : (OuterStmtIn × (∀ i, OuterOStmtIn i)) × OuterWitIn → + (InnerStmtOut × (∀ i, InnerOStmtOut i)) × InnerWitOut → Prop) + (lens : OracleContext.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut + OuterOStmtIn OuterOStmtOut InnerOStmtIn InnerOStmtOut + OuterWitIn OuterWitOut InnerWitIn InnerWitOut) := + Context.Lens.IsComplete outerRelIn innerRelIn outerRelOut innerRelOut compat lens.toContext + +/-- The soundness condition for the oracle statement lens is just the one for the underlying + statement lens -/ +@[reducible, simp] +def OracleStatement.Lens.IsSound {OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type} + {Outer_ιₛᵢ : Type} {OuterOStmtIn : Outer_ιₛᵢ → Type} [∀ i, OracleInterface (OuterOStmtIn i)] + {Outer_ιₛₒ : Type} {OuterOStmtOut : Outer_ιₛₒ → Type} [∀ i, OracleInterface (OuterOStmtOut i)] + {Inner_ιₛᵢ : Type} {InnerOStmtIn : Inner_ιₛᵢ → Type} [∀ i, OracleInterface (InnerOStmtIn i)] + {Inner_ιₛₒ : Type} {InnerOStmtOut : Inner_ιₛₒ → Type} [∀ i, OracleInterface (InnerOStmtOut i)] + (outerLangIn : Set (OuterStmtIn × (∀ i, OuterOStmtIn i))) + (outerLangOut : Set (OuterStmtOut × (∀ i, OuterOStmtOut i))) + (innerLangIn : Set (InnerStmtIn × (∀ i, InnerOStmtIn i))) + (innerLangOut : Set (InnerStmtOut × (∀ i, InnerOStmtOut i))) + (compatStmt : + OuterStmtIn × (∀ i, OuterOStmtIn i) → InnerStmtOut × (∀ i, InnerOStmtOut i) → Prop) + (lens : OracleStatement.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut + OuterOStmtIn OuterOStmtOut InnerOStmtIn InnerOStmtOut) := + Statement.Lens.IsSound outerLangIn outerLangOut innerLangIn innerLangOut compatStmt lens.prover + +/- + +Commit-and-open / generalized BCS transformation: + +Let's simplify the situation here: +- Let's say there is a single oracle message of type `M` from the prover to the verifier, with + oracle interface specified by an instance `O`. +- The reduction is from `R₁ : S → W → Prop` to `R₂ : S × M → W → Prop` (no oracle statements, output + witness is the same, output statement only appends `M` to the input statement) +- We have a functional commitment scheme `FC = (Commit, Open)` for the oracle message. Let's also + assume that this is determnistic and does not use any oracle. + +The transformation produces a new oracle reduction and works as follows: + +A. First phase, commit: + +1. The prover, instead of sending `M`, computes `cm = Commit M` and sends `cm : CM` in the clear to + the verifier. +2. The verifier, instead of receiving oracle access to `M`, receives full access to the commitment + `cm : CM` instead. +3. Syntactically, this means we must change the definition of the statements and witnesses: + - We now go from `R₁ : S → W → Prop` to + + `R₂' : S × CM × (List (M.Query × M.Response)) → W × M → Prop` + +To be more precise, the verifier changes from `S → OracleComp [M]ₒ (S × M)` to + +`S → CM → Option (S × CM × (List (M.Query × M.Response)))`. + +Note that `OracleComp` has a failure option. We should basically think of this as the verifier being +able to run many checks before returning the data. + +What is the resulting relation? `R₂' := R₂ ∧ cm = Commit m`? + +What about all the queries? Query logs (dependent on `m : M`)! Or alternatively, assume a +non-adaptive verifier, which makes the same queries throughout. + +So the right resulting relation is: `R₂' := R₂ ∧ cm = Commit m ∧ ∀ i, respᵢ = oracle m queryᵢ`. + +B. Second phase, open: + +`FC.Open` should be an interactive argument for the relation +`cm = Commit m ∧ ∀ i, respᵢ = oracle m queryᵢ`. + +Guarantees: + +A. First transformation should preserve completeness & knowledge soundness. + +-> require straightline extraction right after the commitment + +(unlike rewinding extraction, which requires knowledge of the opening proofs as well?) + +-/ diff --git a/ArkLib/OracleReduction/LiftContext/OracleReduction.lean b/ArkLib/OracleReduction/LiftContext/OracleReduction.lean index 689a2ac98..855e47b80 100644 --- a/ArkLib/OracleReduction/LiftContext/OracleReduction.lean +++ b/ArkLib/OracleReduction/LiftContext/OracleReduction.lean @@ -5,6 +5,7 @@ Authors: Quang Dao -/ import ArkLib.OracleReduction.LiftContext.Reduction +import ArkLib.OracleReduction.LiftContext.OracleLens /-! ## Lifting Oracle Reductions to Larger Contexts @@ -50,12 +51,41 @@ def OracleVerifier.liftContext OuterOStmtIn OuterOStmtOut InnerOStmtIn InnerOStmtOut) (V : OracleVerifier oSpec InnerStmtIn InnerOStmtIn InnerStmtOut InnerOStmtOut pSpec) : OracleVerifier oSpec OuterStmtIn OuterOStmtIn OuterStmtOut OuterOStmtOut pSpec where - verify := fun outerStmtIn transcript => sorry - embed := by - have := V.embed - + verify := fun outerStmtIn challenges => do + let innerStmtIn ← lens.verifier.projStmt outerStmtIn + let simOStmtIn := lens.verifier.projOStmt + let liftedSim : QueryImpl ([InnerOStmtIn]ₒ ++ₒ [pSpec.Message]ₒ) + (OracleComp ([OuterOStmtIn]ₒ ++ₒ [pSpec.Message]ₒ)) := + simOStmtIn ++ₛₒ idOracle + let lifted2Sim : QueryImpl (oSpec ++ₒ ([InnerOStmtIn]ₒ ++ₒ [pSpec.Message]ₒ)) + (OracleComp (oSpec ++ₒ ([OuterOStmtIn]ₒ ++ₒ [pSpec.Message]ₒ))) := + idOracle ++ₛₒ liftedSim + let innerStmtOut ← simulateQ lifted2Sim (V.verify innerStmtIn challenges) + let simOStmtOut := lens.verifier.liftOStmt + + let outerStmtOut ← simulateQ sorry (lens.verifier.liftStmt outerStmtIn innerStmtOut) + return outerStmtOut + + simulate := fun challenges => by + letI simOStmtOut := lens.verifier.liftOStmt + letI simInner := V.simulate challenges + letI simOStmtIn := lens.verifier.projOStmt + refine QueryImpl.compose ?_ simOStmtOut + refine SimOracle.append idOracle ?_ + (m₂ := OracleComp (oSpec ++ₒ ([OuterOStmtIn]ₒ ++ₒ [pSpec.Message]ₒ))) + refine QueryImpl.compose ?_ simInner + refine SimOracle.append idOracle ?_ + (m₂ := OracleComp (oSpec ++ₒ ([OuterOStmtIn]ₒ ++ₒ [pSpec.Message]ₒ))) + exact SimOracle.append simOStmtIn idOracle + + reify := fun combinedOuterStmtIn transcript => do + let combinedInnerStmtIn := lens.prover.proj combinedOuterStmtIn + let combinedInnerStmtOut ← V.toVerifier.verify combinedInnerStmtIn transcript + return lens.prover.liftOStmt combinedOuterStmtIn combinedInnerStmtOut + + reify_simulate := by + simp [OracleVerifier.toVerifier] sorry - hEq := sorry /-- The lifting of an inner oracle reduction to an outer oracle reduction, requiring an associated oracle context lens -/ @@ -70,6 +100,24 @@ def OracleReduction.liftContext prover := R.prover.liftContext lens verifier := R.verifier.liftContext lens.stmt +@[reducible] +def OracleVerifier.compatStatement + (lens : OracleStatement.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut + OuterOStmtIn OuterOStmtOut InnerOStmtIn InnerOStmtOut) + (V : OracleVerifier oSpec InnerStmtIn InnerOStmtIn InnerStmtOut InnerOStmtOut pSpec) : + (OuterStmtIn × (∀ i, OuterOStmtIn i)) → (InnerStmtOut × (∀ i, InnerOStmtOut i)) → Prop := + V.toVerifier.compatStatement lens.toStatement + +def OracleReduction.compatContext + (lens : OracleContext.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut + OuterOStmtIn OuterOStmtOut InnerOStmtIn InnerOStmtOut + OuterWitIn OuterWitOut InnerWitIn InnerWitOut) + (R : OracleReduction oSpec InnerStmtIn InnerOStmtIn InnerWitIn + InnerStmtOut InnerOStmtOut InnerWitOut pSpec) : + (OuterStmtIn × (∀ i, OuterOStmtIn i)) × OuterWitIn → + (InnerStmtOut × (∀ i, InnerOStmtOut i)) × InnerWitOut → Prop := + R.toReduction.compatContext lens.toContext + section Execution /-- The lifting of the verifier commutes with the conversion from the oracle verifier to the @@ -78,7 +126,7 @@ theorem OracleVerifier.liftContext_toVerifier_comm {lens : OracleStatement.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterOStmtIn OuterOStmtOut InnerOStmtIn InnerOStmtOut} {V : OracleVerifier oSpec InnerStmtIn InnerOStmtIn InnerStmtOut InnerOStmtOut pSpec} : - (V.liftContext lens).toVerifier = V.toVerifier.liftContext lens := by + (V.liftContext lens).toVerifier = V.toVerifier.liftContext lens.toStatement := by sorry /-- The lifting of the reduction commutes with the conversion from the oracle reduction to the @@ -144,29 +192,30 @@ theorem liftContext_soundness OuterOStmtIn OuterOStmtOut InnerOStmtIn InnerOStmtOut} (V : OracleVerifier oSpec InnerStmtIn InnerOStmtIn InnerStmtOut InnerOStmtOut pSpec) [lensSound : lens.IsSound outerLangIn outerLangOut innerLangIn innerLangOut - (V.toVerifier.compatStatement lens)] + (V.compatStatement lens)] (h : V.soundness innerLangIn innerLangOut soundnessError) : (V.liftContext lens).soundness outerLangIn outerLangOut soundnessError := by unfold OracleVerifier.soundness at h ⊢ rw [liftContext_toVerifier_comm] - exact V.toVerifier.liftContext_soundness h (lens := lens) + exact V.toVerifier.liftContext_soundness h (lens := lens.toStatement) theorem liftContext_knowledgeSoundness [Inhabited InnerWitIn] {knowledgeError : ℝ≥0} - {stmtLens : OracleStatement.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut + {oStmtLens : OracleStatement.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterOStmtIn OuterOStmtOut InnerOStmtIn InnerOStmtOut} {witLens : Witness.InvLens (OuterStmtIn × ∀ i, OuterOStmtIn i) OuterWitIn OuterWitOut InnerWitIn InnerWitOut} (V : OracleVerifier oSpec InnerStmtIn InnerOStmtIn InnerStmtOut InnerOStmtOut pSpec) [lensKS : Extractor.Lens.IsKnowledgeSound outerRelIn innerRelIn outerRelOut innerRelOut - (V.toVerifier.compatStatement stmtLens) (fun _ _ => True) ⟨stmtLens, witLens⟩] + (V.compatStatement oStmtLens) (fun _ _ => True) ⟨oStmtLens.toStatement, witLens⟩] (h : V.knowledgeSoundness innerRelIn innerRelOut knowledgeError) : - (V.liftContext stmtLens).knowledgeSoundness outerRelIn outerRelOut + (V.liftContext oStmtLens).knowledgeSoundness outerRelIn outerRelOut knowledgeError := by unfold OracleVerifier.knowledgeSoundness at h ⊢ rw [liftContext_toVerifier_comm] - exact V.toVerifier.liftContext_knowledgeSoundness h (stmtLens := stmtLens) (witLens := witLens) + exact V.toVerifier.liftContext_knowledgeSoundness h + (stmtLens := oStmtLens.toStatement) (witLens := witLens) theorem liftContext_rbr_soundness {rbrSoundnessError : pSpec.ChallengeIdx → ℝ≥0} @@ -175,30 +224,30 @@ theorem liftContext_rbr_soundness (V : OracleVerifier oSpec InnerStmtIn InnerOStmtIn InnerStmtOut InnerOStmtOut pSpec) [lensSound : lens.IsSound outerLangIn outerLangOut innerLangIn innerLangOut - (V.toVerifier.compatStatement lens)] + (V.compatStatement lens)] (h : V.rbrSoundness innerLangIn innerLangOut rbrSoundnessError) : (V.liftContext lens).rbrSoundness outerLangIn outerLangOut rbrSoundnessError := by unfold OracleVerifier.rbrSoundness at h ⊢ rw [liftContext_toVerifier_comm] - exact V.toVerifier.liftContext_rbr_soundness h (lens := lens) + exact V.toVerifier.liftContext_rbr_soundness h (lens := lens.toStatement) theorem liftContext_rbr_knowledgeSoundness [Inhabited InnerWitIn] {rbrKnowledgeError : pSpec.ChallengeIdx → ℝ≥0} - {stmtLens : OracleStatement.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut + {oStmtLens : OracleStatement.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterOStmtIn OuterOStmtOut InnerOStmtIn InnerOStmtOut} {witLens : Witness.InvLens (OuterStmtIn × ∀ i, OuterOStmtIn i) OuterWitIn OuterWitOut InnerWitIn InnerWitOut} (V : OracleVerifier oSpec InnerStmtIn InnerOStmtIn InnerStmtOut InnerOStmtOut pSpec) [lensKS : Extractor.Lens.IsKnowledgeSound outerRelIn innerRelIn outerRelOut innerRelOut - (V.toVerifier.compatStatement stmtLens) (fun _ _ => True) ⟨stmtLens, witLens⟩] + (V.compatStatement oStmtLens) (fun _ _ => True) ⟨oStmtLens.toStatement, witLens⟩] (h : V.rbrKnowledgeSoundness innerRelIn innerRelOut rbrKnowledgeError) : - (V.liftContext stmtLens).rbrKnowledgeSoundness outerRelIn outerRelOut + (V.liftContext oStmtLens).rbrKnowledgeSoundness outerRelIn outerRelOut rbrKnowledgeError := by unfold OracleVerifier.rbrKnowledgeSoundness at h ⊢ rw [liftContext_toVerifier_comm] exact V.toVerifier.liftContext_rbr_knowledgeSoundness h - (stmtLens := stmtLens) (witLens := witLens) + (stmtLens := oStmtLens.toStatement) (witLens := witLens) end OracleVerifier diff --git a/ArkLib/OracleReduction/LiftContext/Reduction.lean b/ArkLib/OracleReduction/LiftContext/Reduction.lean index 4d77301de..302d423dd 100644 --- a/ArkLib/OracleReduction/LiftContext/Reduction.lean +++ b/ArkLib/OracleReduction/LiftContext/Reduction.lean @@ -114,10 +114,11 @@ open Verifier in /-- The outer round-by-round extractor after lifting invokes the inner extractor on the projected input, and lifts the output -/ def Extractor.RoundByRound.liftContext + {WitMid : Fin (n + 1) → Type} (lens : Extractor.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut) - (E : Extractor.RoundByRound oSpec InnerStmtIn InnerWitIn pSpec) : - Extractor.RoundByRound oSpec OuterStmtIn OuterWitIn pSpec := + (E : Extractor.RoundByRound oSpec InnerStmtIn InnerWitIn InnerWitOut pSpec WitMid) : + Extractor.RoundByRound oSpec OuterStmtIn OuterWitIn OuterWitOut pSpec WitMid := sorry -- fun roundIdx outerStmtIn fullTranscript proveQueryLog => -- rbrLensInv.liftWit (E roundIdx (lens.projStmt outerStmtIn) fullTranscript proveQueryLog) @@ -179,8 +180,9 @@ def Verifier.StateFunction.liftContext [oSpec.FiniteRange] where toFun := fun m outerStmtIn transcript => stF m (lens.proj outerStmtIn) transcript - toFun_empty := fun stmt hStmt => - stF.toFun_empty (lens.proj stmt) (lensSound.proj_sound stmt hStmt) + toFun_empty := sorry + -- fun stmt hStmt => + -- stF.toFun_empty (lens.proj stmt) (lensSound.proj_sound stmt hStmt) toFun_next := fun m hDir outerStmtIn transcript hStmt msg => stF.toFun_next m hDir (lens.proj outerStmtIn) transcript hStmt msg toFun_full := fun outerStmtIn transcript hStmt => by diff --git a/ArkLib/OracleReduction/Prelude.lean b/ArkLib/OracleReduction/Prelude.lean index d9d70d290..aa67cfbff 100644 --- a/ArkLib/OracleReduction/Prelude.lean +++ b/ArkLib/OracleReduction/Prelude.lean @@ -74,6 +74,18 @@ def directionEquivFin2 : Direction ≃ Fin 2 where /-- This allows us to write `0` for `.V_to_P` and `1` for `.P_to_V`. -/ instance : Coe (Fin 2) Direction := ⟨directionEquivFin2.invFun⟩ +/-- The trivial statement, which is a `Unit` type. -/ +@[reducible] +def TrivialStatement := Unit + +/-- The trivial oracle statement, which is an `Empty`-indexed `Unit` family of types. -/ +@[reducible] +def TrivialOracleStatement := fun _ : Empty => Unit + +/-- The trivial witness, which is a `Unit` type. -/ +@[reducible] +def TrivialWitness := Unit + section Relation /-- The associated language `Set α` for a relation `Set (α × β)`. -/ @@ -91,22 +103,23 @@ theorem Set.not_mem_language_iff {α β} (rel : Set (α × β)) (stmt : α) : stmt ∉ rel.language ↔ ∀ wit, (stmt, wit) ∉ rel := by simp [language] -/-- The trivial relation on Boolean statement and unit witness, which outputs the Boolean (i.e. - accepts or rejects). -/ -def acceptRejectRel : Set (Bool × Unit) := - { (true, ()) } +/-- The trivial relation on the trivial statement and unit witness, which outputs the trivial + statement (i.e. `()`), which is the same as accepting. -/ +def acceptRejectRel : Set (TrivialStatement × TrivialWitness) := + { ((()), ()) } -/-- The trivial relation on Boolean statement, no oracle statements, and unit witness. -/ -def acceptRejectOracleRel : Set ((Bool × (∀ _ : Empty, Unit)) × Unit) := - { ((true, isEmptyElim), ()) } +/-- The trivial relation on the trivial statement, oracle statements, and witness. -/ +def acceptRejectOracleRel : + Set ((TrivialStatement × (∀ i, TrivialOracleStatement i)) × TrivialWitness) := + { (((), isEmptyElim), ()) } @[simp] -theorem acceptRejectRel_language : acceptRejectRel.language = { true } := by +theorem acceptRejectRel_language : acceptRejectRel.language = { () } := by unfold Set.language acceptRejectRel; simp @[simp] theorem acceptRejectOracleRel_language : - acceptRejectOracleRel.language = { (true, isEmptyElim) } := by + acceptRejectOracleRel.language = { ((), isEmptyElim) } := by unfold Set.language acceptRejectOracleRel; simp end Relation diff --git a/ArkLib/OracleReduction/Security/Basic.lean b/ArkLib/OracleReduction/Security/Basic.lean index c608e2f2c..96d1ae988 100644 --- a/ArkLib/OracleReduction/Security/Basic.lean +++ b/ArkLib/OracleReduction/Security/Basic.lean @@ -284,14 +284,31 @@ open Reduction section OracleProtocol variable - {StmtIn : Type} {ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} {WitIn : Type} - {StmtOut : Type} {ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} {WitOut : Type} - {n : ℕ} {pSpec : ProtocolSpec n} - [Oₛᵢ : ∀ i, OracleInterface (OStmtIn i)] - [∀ i, OracleInterface (pSpec.Message i)] [∀ i, VCVCompatible (pSpec.Challenge i)] + {StmtIn : Type} {ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} [Oₛᵢ : ∀ i, OracleInterface (OStmtIn i)] + {WitIn : Type} + {StmtOut : Type} {ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} [Oₛₒ : ∀ i, OracleInterface (OStmtOut i)] + {WitOut : Type} + {n : ℕ} {pSpec : ProtocolSpec n} [Oₘ : ∀ i, OracleInterface (pSpec.Message i)] + [∀ i, VCVCompatible (pSpec.Challenge i)] namespace OracleReduction +-- TODO: define more general definitions of completeness & soundness for oracle verifiers that are +-- not necessarily reifiable (so just containing `verify` and `simulate`). + +-- What needs to be changed: +-- +-- 1. For completeness, we need compatibility between the prover's output oracle statements and the +-- oracle verifier's simulation of the output oracle statements. +-- +-- 2. For (knowledge) soundness, we need to change relations to be of the form +-- `Stmt{In/Out} (→ Wit{In/Out}) → OracleComp (oSpec ++ₒ [OStmt{In/Out}]ₒ) Prop`, +-- +-- so that it can be checked by the data provided by the oracle verifier (this is especially true +-- for output relation). Namely, we may first lift to +-- `OracleComp (oSpec ++ₒ ([OStmtIn]ₒ ++ₒ [pSpec.Message]ₒ)) Prop`, and then check the relation +-- using the provided values of `OStmtIn` and `pSpec.Message`. + /-- Completeness of an oracle reduction is the same as for non-oracle reductions. -/ def completeness (relIn : Set ((StmtIn × ∀ i, OStmtIn i) × WitIn)) @@ -357,13 +374,13 @@ def perfectCompleteness (relation : Set (Statement × Witness)) @[reducible, simp] def soundness (langIn : Set Statement) - (verifier : Verifier oSpec Statement Bool pSpec) + (verifier : Verifier oSpec Statement TrivialStatement pSpec) (soundnessError : ℝ≥0) : Prop := verifier.soundness langIn acceptRejectRel.language soundnessError @[reducible, simp] -def knowledgeSoundness (relation : Set (Statement × Bool)) - (verifier : Verifier oSpec Statement Bool pSpec) +def knowledgeSoundness (relation : Set (Statement × TrivialStatement)) + (verifier : Verifier oSpec Statement TrivialStatement pSpec) (knowledgeError : ℝ≥0) : Prop := verifier.knowledgeSoundness relation acceptRejectRel knowledgeError @@ -393,7 +410,8 @@ def perfectCompleteness @[reducible, simp] def soundness (langIn : Set (Statement × ∀ i, OStatement i)) - (verifier : OracleVerifier oSpec Statement OStatement Bool (fun _ : Empty => Unit) pSpec) + (verifier : OracleVerifier oSpec Statement OStatement TrivialStatement + TrivialOracleStatement pSpec) (soundnessError : ℝ≥0) : Prop := verifier.toVerifier.soundness langIn acceptRejectOracleRel.language soundnessError @@ -401,7 +419,8 @@ def soundness @[reducible, simp] def knowledgeSoundness (relation : Set ((Statement × ∀ i, OStatement i) × Witness)) - (verifier : OracleVerifier oSpec Statement OStatement Bool (fun _ : Empty => Unit) pSpec) + (verifier : OracleVerifier oSpec Statement OStatement TrivialStatement + TrivialOracleStatement pSpec) (knowledgeError : ℝ≥0) : Prop := verifier.toVerifier.knowledgeSoundness relation acceptRejectOracleRel knowledgeError diff --git a/ArkLib/OracleReduction/Security/RoundByRound.lean b/ArkLib/OracleReduction/Security/RoundByRound.lean index 74e70bc7d..f1a0138e9 100644 --- a/ArkLib/OracleReduction/Security/RoundByRound.lean +++ b/ArkLib/OracleReduction/Security/RoundByRound.lean @@ -23,16 +23,26 @@ variable [oSpec.FiniteRange] [∀ i, VCVCompatible (pSpec.Challenge i)] namespace Extractor -/-- A round-by-round extractor with index `m` is given the input statement, a partial transcript - of length `m`, the prover's query log, and returns a witness to the statement. - - Note that the RBR extractor does not need to take in the output statement or witness. -/ -def RoundByRound (oSpec : OracleSpec ι) (StmtIn WitIn : Type) {n : ℕ} (pSpec : ProtocolSpec n) := +/-- A **one-shot** round-by-round extractor is a function that: +- Takes in index `m : Fin (n + 1)` +- Takes in the input statement `stmtIn : StmtIn` +- Takes in a partial transcript up to round `m` +- Takes in the prover's query log (TODO: refine this, verifier's query log as well?) + +and returns an input witness `witIn : WitIn`. + +This is the old definition of round-by-round extractor, which is less general than the new +definition (i.e. the input witness is extracted immediately, "in one shot", unlike the general +definition where the input witness is derived via intermediate witnesses). -/ +def RoundByRoundOneShot + (oSpec : OracleSpec ι) (StmtIn WitIn : Type) {n : ℕ} (pSpec : ProtocolSpec n) := (m : Fin (n + 1)) → StmtIn → Transcript m pSpec → QueryLog oSpec → WitIn -/-- A round-by-round extractor is **monotone** if its success probability on a given query log - is the same as the success probability on any extension of that query log. -/ -class RoundByRound.IsMonotone (E : RoundByRound oSpec StmtIn WitIn pSpec) +/-- A one-shot round-by-round extractor is **monotone** if its success probability on a given query + log is the same as the success probability on any extension of that query log. + + TODO: refine this -/ +class RoundByRoundOneShot.IsMonotone (E : RoundByRoundOneShot oSpec StmtIn WitIn pSpec) (relIn : Set (StmtIn × WitIn)) where is_monotone : ∀ roundIdx stmtIn transcript, ∀ proveQueryLog₁ proveQueryLog₂ : oSpec.QueryLog, @@ -43,6 +53,46 @@ class RoundByRound.IsMonotone (E : RoundByRound oSpec StmtIn WitIn pSpec) (stmtIn, E roundIdx stmtIn transcript proveQueryLog₁) ∈ relIn → (stmtIn, E roundIdx stmtIn transcript proveQueryLog₂) ∈ relIn +/-- A **round-by-round extractor** is a tuple of algorithms that iteratively extracts the input + witness from the output witness, through a series of intermediate witnesses + (indexed by `m : Fin (n + 1)`). Formally, it is a tuple of algorithms: + + - `extractIn : StmtIn → WitMid 0 → WitIn` + - `extractMid : (m : Fin n) → StmtIn → Transcript m.succ pSpec` + `→ WitMid m.succ → WitMid m.castSucc` + - `extractOut : StmtIn → FullTranscript pSpec → WitOut → WitMid (.last n)` + + The extractor processes rounds in decreasing order: `n → n-1 → ... → 1 → 0`, using + intermediate witness types `WitMid m` for each round `m`. +-/ +structure RoundByRound + (oSpec : OracleSpec ι) (StmtIn WitIn WitOut : Type) {n : ℕ} (pSpec : ProtocolSpec n) + (WitMid : Fin (n + 1) → Type) where + /-- Extract the input witness from the intermediate witness at round 0 -/ + extractIn : StmtIn → (WitMid 0 ≃ WitIn) + /-- Extract intermediate witness for round `m` from intermediate witness for round `m+1`, + using the transcript up to round `m+1` -/ + extractMid : (m : Fin n) → StmtIn → Transcript m.succ pSpec → WitMid m.succ → WitMid m.castSucc + /-- Construct the intermediate witness for the final round from the output witness -/ + extractOut : StmtIn → FullTranscript pSpec → WitOut → WitMid (.last n) + +namespace RoundByRoundOneShot + +/-- A one-shot round-by-round extractor can be converted to the general round-by-round extractor + format, where all intermediate witness types are equal to the input witness type. + + (something is wrong here...) + + Note that the converse is _not_ true: it's not possible in general to convert a general + round-by-round extractor to a one-shot one. -/ +def toRoundByRound (E : RoundByRoundOneShot oSpec StmtIn WitIn pSpec) : + RoundByRound oSpec StmtIn WitIn WitOut pSpec (fun _ => WitIn) where + extractIn := fun _ => Equiv.refl _ + extractMid := fun m stmtIn tr _ => E m.succ stmtIn tr default + extractOut := fun stmtIn tr _ => E (.last n) stmtIn tr default + +end RoundByRoundOneShot + end Extractor namespace Verifier @@ -58,9 +108,9 @@ structure StateFunction (verifier : Verifier oSpec StmtIn StmtOut pSpec) where toFun : (m : Fin (n + 1)) → StmtIn → Transcript m pSpec → Prop - /-- For all input statement not in the language, the state function is false for the empty - transcript -/ - toFun_empty : ∀ stmt ∉ langIn, ¬ toFun 0 stmt default + /-- For all input statement not in the language, the state function is false for that statement + and the empty transcript -/ + toFun_empty : ∀ stmt, stmt ∈ langIn ↔ toFun 0 stmt default /-- If the state function is false for a partial transcript, and the next message is from the prover to the verifier, then the state function is also false for the new partial transcript regardless of the message -/ @@ -79,55 +129,109 @@ structure KnowledgeStateFunction (relIn : Set (StmtIn × WitIn)) (relOut : Set (StmtOut × WitOut)) (verifier : Verifier oSpec StmtIn StmtOut pSpec) (WitMid : Fin (n + 1) → Type) + (extractor : Extractor.RoundByRound oSpec StmtIn WitIn WitOut pSpec WitMid) where /-- The knowledge state function: takes in round index, input statement, transcript up to that round, and intermediate witness of that round, and returns True/False. -/ toFun : (m : Fin (n + 1)) → StmtIn → Transcript m pSpec → WitMid m → Prop - /-- For all input statement such that for all input witness, the statement and witness is not - in the input relation, the state function is false for the empty transcript and any witness. -/ - toFun_empty : ∀ stmtIn, stmtIn ∉ relIn.language → - ∀ witMid, ¬ toFun 0 stmtIn default witMid - /-- If the state function is false for a partial transcript, and the next message is from the - prover to the verifier, then the state function is also false for the new partial transcript - regardless of the message and the next intermediate witness. -/ + /-- If the state function is true for the empty transcript and some initial intermediate witness, + then the input statement and extracted witness are in the input relation -/ + toFun_empty : ∀ stmtIn witMid, + ⟨stmtIn, extractor.extractIn stmtIn witMid⟩ ∈ relIn ↔ + toFun 0 stmtIn default witMid + /-- If the state function is true for a partial transcript extended with a prover message, then + the state function is also true for the original partial transcript with the extracted + intermediate witness -/ toFun_next : ∀ m, pSpec.getDir m = .P_to_V → - ∀ stmtIn tr, (∀ witMid, ¬ toFun m.castSucc stmtIn tr witMid) → - ∀ msg, (∀ witMid', ¬ toFun m.succ stmtIn (tr.concat msg) witMid') - toFun_full : ∀ stmtIn tr, (∀ witMid, ¬ toFun (.last n) stmtIn tr witMid) → - [fun stmtOut => stmtOut ∈ relOut.language | verifier.run stmtIn tr ] = 0 - -/-- A knowledge state function gives rise to a state function -/ + ∀ stmtIn tr msg witMid, toFun m.succ stmtIn (tr.concat msg) witMid → + toFun m.castSucc stmtIn tr (extractor.extractMid m stmtIn (tr.concat msg) witMid) + /-- If the verifier can output a statement `stmtOut` that is in the output relation with some + output witness `witOut`, then the state function is true for the full transcript and the + extracted last middle witness. -/ + toFun_full : ∀ stmtIn tr witOut, + [fun stmtOut => (stmtOut, witOut) ∈ relOut | verifier.run stmtIn tr ] > 0 → + toFun (.last n) stmtIn tr (extractor.extractOut stmtIn tr witOut) + +/-- A knowledge state function gives rise to a state function via quantifying over the witness -/ def KnowledgeStateFunction.toStateFunction {relIn : Set (StmtIn × WitIn)} {relOut : Set (StmtOut × WitOut)} {verifier : Verifier oSpec StmtIn StmtOut pSpec} {WitMid : Fin (n + 1) → Type} - (kSF : KnowledgeStateFunction relIn relOut verifier WitMid) : + {extractor : Extractor.RoundByRound oSpec StmtIn WitIn WitOut pSpec WitMid} + (kSF : KnowledgeStateFunction relIn relOut verifier WitMid extractor) : verifier.StateFunction relIn.language relOut.language where toFun := fun m stmtIn tr => ∃ witMid, kSF.toFun m stmtIn tr witMid - toFun_empty := fun stmtIn hStmtIn => by - simp; exact kSF.toFun_empty stmtIn (by simpa [Set.language] using hStmtIn) + toFun_empty := by + intro stmtIn + simp only [Set.mem_image, Prod.exists, exists_and_right, exists_eq_right] + constructor + · intro ⟨witIn, h⟩ + have := kSF.toFun_empty stmtIn ((extractor.extractIn stmtIn).symm witIn) + simp at this + exact ⟨_, this.mp h⟩ + · intro ⟨witMid, h⟩ + have := (kSF.toFun_empty stmtIn witMid).mpr h + exact ⟨_, this⟩ + -- simp only [not_exists] + -- intro witMid hToFun + -- have := kSF.toFun_empty stmtIn witMid hToFun + -- simp_all toFun_next := fun m hDir stmtIn tr hToFunNext msg => by - simp; exact kSF.toFun_next m hDir stmtIn tr (by simpa [Set.language] using hToFunNext) msg + simp only [not_exists] + intro witMid hToFunNext + have := kSF.toFun_next m hDir stmtIn tr msg witMid hToFunNext + simp_all toFun_full := fun stmtIn tr hToFunFull => by - exact kSF.toFun_full stmtIn tr (by simpa [Set.language] using hToFunFull) - -/-- A round-by-round extractor basically goes backwards, extracting witnesses round-by-round in -opposite to the prover. -/ -structure NewExtractor.RoundByRound (WitMid : Fin (n + 1) → Type) where - -- what if, just one function? - -- extract : (m : Fin (n + 1)) → StmtIn → Transcript m pSpec → WitMid m → QueryLog oSpec → WitIn - extractIn : WitMid 0 → WitIn - extractMid : (m : Fin n) → StmtIn → Transcript m.succ pSpec → - WitMid m.succ → QueryLog oSpec → WitMid m.castSucc - extractOut : WitOut → WitMid (.last n) - + simp only [Fin.val_last, Set.mem_image, Prod.exists, exists_and_right, exists_eq_right, + probEvent_eq_zero_iff, not_exists] + intro stmtOut hStmtOut witOut hRelOut + have hProb : [fun stmtOut ↦ (stmtOut, witOut) ∈ relOut | run stmtIn tr verifier] > 0 := by + simp only [Fin.val_last, gt_iff_lt, probEvent_pos_iff] + exact ⟨stmtOut, hStmtOut, hRelOut⟩ + have := kSF.toFun_full stmtIn tr witOut hProb + simp_all + +/-- A state function & a one-shot round-by-round extractor gives rise to a knowledge state function + where the intermediate witness types are all equal to the input witness type -/ +def StateFunction.toKnowledgeStateFunction + {relIn : Set (StmtIn × WitIn)} {relOut : Set (StmtOut × WitOut)} + {verifier : Verifier oSpec StmtIn StmtOut pSpec} + (oneShotE : Extractor.RoundByRoundOneShot oSpec StmtIn WitIn pSpec) + (stF : verifier.StateFunction relIn.language relOut.language) : + verifier.KnowledgeStateFunction relIn relOut (fun _ => WitIn) oneShotE.toRoundByRound where + toFun := fun m stmtIn tr wit => stF.toFun m stmtIn tr ∨ (stmtIn, wit) ∈ relIn + toFun_empty := fun stmtIn witIn => by + have := stF.toFun_empty stmtIn + simp_all + -- refine Iff.trans (stF.toFun_empty stmtIn).symm ?_ + sorry + -- (by simp; intro h; have := (stF.toFun_empty stmtIn).mpr h; simp_all) + -- stop + -- contrapose! this + -- simp_all [Extractor.RoundByRoundOneShot.toRoundByRound] + -- sorry + toFun_next := fun m hDir stmtIn tr msg witMid h => by sorry + -- have := stF.toFun_next m hDir stmtIn tr + -- contrapose! this + -- simp_all + -- refine ⟨?_, ⟨msg, h.1⟩⟩ + toFun_full := fun stmtIn tr witOut h => by + have := stF.toFun_full stmtIn tr + contrapose! this + simp_all + obtain ⟨x, hx, hRelOut⟩ := h + exact ⟨x, hx, witOut, hRelOut⟩ + +/-- Coercion to the underlying function of a state function -/ instance {langIn : Set StmtIn} {langOut : Set StmtOut} {verifier : Verifier oSpec StmtIn StmtOut pSpec} : CoeFun (verifier.StateFunction langIn langOut) (fun _ => (m : Fin (n + 1)) → StmtIn → Transcript m pSpec → Prop) := ⟨fun f => f.toFun⟩ +/-- Coercion to the underlying function of a knowledge state function -/ instance {relIn : Set (StmtIn × WitIn)} {relOut : Set (StmtOut × WitOut)} - {verifier : Verifier oSpec StmtIn StmtOut pSpec} {WitMid : Fin (n + 1) → Type} : - CoeFun (verifier.KnowledgeStateFunction relIn relOut WitMid) + {verifier : Verifier oSpec StmtIn StmtOut pSpec} {WitMid : Fin (n + 1) → Type} + {extractor : Extractor.RoundByRound oSpec StmtIn WitIn WitOut pSpec WitMid} : + CoeFun (verifier.KnowledgeStateFunction relIn relOut WitMid extractor) (fun _ => (m : Fin (n + 1)) → StmtIn → Transcript m pSpec → WitMid m → Prop) := ⟨fun f => f.toFun⟩ @@ -157,7 +261,7 @@ def rbrSoundness (langIn : Set StmtIn) (langOut : Set StmtOut) ∀ witIn : WitIn, ∀ prover : Prover oSpec StmtIn WitIn StmtOut WitOut pSpec, ∀ i : pSpec.ChallengeIdx, - let ex : OracleComp (oSpec ++ₒ [pSpec.Challenge]ₒ) _ := do + letI ex : OracleComp (oSpec ++ₒ [pSpec.Challenge]ₒ) _ := do return (← prover.runToRound i.1.castSucc stmtIn witIn, ← pSpec.getChallenge i) [fun ⟨⟨transcript, _⟩, challenge⟩ => ¬ stateFunction i.1.castSucc stmtIn transcript ∧ @@ -191,16 +295,16 @@ class IsRBRSound (langIn : Set StmtIn) (langOut : Set StmtOut) is at most `rbrKnowledgeError i`. -/ -def rbrKnowledgeSoundness (relIn : Set (StmtIn × WitIn)) (relOut : Set (StmtOut × WitOut)) +def rbrKnowledgeSoundnessOneShot (relIn : Set (StmtIn × WitIn)) (relOut : Set (StmtOut × WitOut)) (verifier : Verifier oSpec StmtIn StmtOut pSpec) (rbrKnowledgeError : pSpec.ChallengeIdx → ℝ≥0) : Prop := ∃ stateFunction : verifier.StateFunction relIn.language relOut.language, - ∃ extractor : Extractor.RoundByRound oSpec StmtIn WitIn pSpec, + ∃ extractor : Extractor.RoundByRoundOneShot oSpec StmtIn WitIn pSpec, ∀ stmtIn : StmtIn, ∀ witIn : WitIn, ∀ prover : Prover oSpec StmtIn WitIn StmtOut WitOut pSpec, ∀ i : pSpec.ChallengeIdx, - let ex : OracleComp (oSpec ++ₒ [pSpec.Challenge]ₒ) _ := (do + letI ex : OracleComp (oSpec ++ₒ [pSpec.Challenge]ₒ) _ := (do let result ← prover.runWithLogToRound i.1.castSucc stmtIn witIn let chal ← pSpec.getChallenge i return (result, chal)) @@ -212,24 +316,24 @@ def rbrKnowledgeSoundness (relIn : Set (StmtIn × WitIn)) (relOut : Set (StmtOut | ex] ≤ rbrKnowledgeError i -- Tentative new definition of rbr knowledge soundness, using the knowledge state function -def newRbrKnowledgeSoundness (relIn : Set (StmtIn × WitIn)) (relOut : Set (StmtOut × WitOut)) +def rbrKnowledgeSoundness (relIn : Set (StmtIn × WitIn)) (relOut : Set (StmtOut × WitOut)) (verifier : Verifier oSpec StmtIn StmtOut pSpec) (rbrKnowledgeError : pSpec.ChallengeIdx → ℝ≥0) : Prop := ∃ WitMid : Fin (n + 1) → Type, - ∃ kSF : verifier.KnowledgeStateFunction relIn relOut WitMid, - ∃ extractor : NewExtractor.RoundByRound WitMid (WitIn := WitIn) (WitOut := WitOut), + ∃ extractor : Extractor.RoundByRound oSpec StmtIn WitIn WitOut pSpec WitMid, + ∃ kSF : verifier.KnowledgeStateFunction relIn relOut WitMid extractor, ∀ stmtIn : StmtIn, ∀ witIn : WitIn, ∀ prover : Prover oSpec StmtIn WitIn StmtOut WitOut pSpec, ∀ i : pSpec.ChallengeIdx, - let ex : OracleComp (oSpec ++ₒ [pSpec.Challenge]ₒ) _ := (do + letI ex : OracleComp (oSpec ++ₒ [pSpec.Challenge]ₒ) _ := (do let result ← prover.runWithLogToRound i.1.castSucc stmtIn witIn let chal ← pSpec.getChallenge i return (result, chal)) - [fun ⟨⟨transcript, _, proveQueryLog⟩, challenge⟩ => + [fun ⟨⟨transcript, _, _⟩, challenge⟩ => ∃ witMid, ¬ kSF i.1.castSucc stmtIn transcript - (extractor.extractMid i.1 stmtIn (transcript.concat challenge) witMid proveQueryLog) ∧ + (extractor.extractMid i.1 stmtIn (transcript.concat challenge) witMid) ∧ kSF i.1.succ stmtIn (transcript.concat challenge) witMid | ex] ≤ rbrKnowledgeError i @@ -243,6 +347,34 @@ class IsRBRKnowledgeSound (relIn : Set (StmtIn × WitIn)) (relOut : Set (StmtOut rbrKnowledgeError : pSpec.ChallengeIdx → ℝ≥0 is_rbr_knowledge_sound : rbrKnowledgeSoundness relIn relOut verifier rbrKnowledgeError +/-- Implication: old rbr knowledge soundness implies new rbr knowledge soundness (with the same + error) -/ +theorem rbrKnowledgeSoundnessOneShot_implies_rbrKnowledgeSoundness + {relIn : Set (StmtIn × WitIn)} {relOut : Set (StmtOut × WitOut)} + {verifier : Verifier oSpec StmtIn StmtOut pSpec} + {rbrKnowledgeError : pSpec.ChallengeIdx → ℝ≥0} + (h : verifier.rbrKnowledgeSoundnessOneShot relIn relOut rbrKnowledgeError) : + verifier.rbrKnowledgeSoundness relIn relOut rbrKnowledgeError := by + unfold rbrKnowledgeSoundness + unfold rbrKnowledgeSoundnessOneShot at h + obtain ⟨stF, oneShotE, h⟩ := h + refine ⟨fun _ => WitIn, oneShotE.toRoundByRound, stF.toKnowledgeStateFunction oneShotE, ?_⟩ + intro stmtIn witIn prover i + have := h stmtIn witIn prover i + simp at h ⊢ + clear h + refine le_trans ?_ this + simp + refine probEvent_mono ?_ + intro ⟨⟨tr, _, _⟩, chal⟩ hx + simp [StateFunction.toKnowledgeStateFunction] + intro hCastSucc witIn' hSucc + simp_all + have := stF.toFun_empty + -- refine ⟨?_, hCastSucc, hSucc⟩ + sorry + -- obtain ⟨WitMid, extractor, kSF⟩ + end RoundByRound end Verifier @@ -252,10 +384,9 @@ open Verifier section OracleProtocol variable - {ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} - {ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} - [Oₛᵢ : ∀ i, OracleInterface (OStmtIn i)] - [∀ i, OracleInterface (pSpec.Message i)] + {ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} [Oₛᵢ : ∀ i, OracleInterface (OStmtIn i)] + {ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} [Oₛₒ : ∀ i, OracleInterface (OStmtOut i)] + [Oₘ : ∀ i, OracleInterface (pSpec.Message i)] namespace OracleVerifier @@ -266,6 +397,16 @@ def StateFunction (verifier : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec) := verifier.toVerifier.StateFunction langIn langOut +@[reducible, simp] +def KnowledgeStateFunction + (relIn : Set ((StmtIn × ∀ i, OStmtIn i) × WitIn)) + (relOut : Set ((StmtOut × ∀ i, OStmtOut i) × WitOut)) + (verifier : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec) + (WitMid : Fin (n + 1) → Type) + (extractor : Extractor.RoundByRound oSpec + (StmtIn × (∀ i, OStmtIn i)) WitIn WitOut pSpec WitMid) := + verifier.toVerifier.KnowledgeStateFunction relIn relOut WitMid extractor + /-- Round-by-round soundness of an oracle reduction is the same as for non-oracle reductions. -/ def rbrSoundness (langIn : Set (StmtIn × ∀ i, OStmtIn i)) @@ -295,13 +436,13 @@ namespace Proof @[reducible, simp] def rbrSoundness (langIn : Set Statement) - (verifier : Verifier oSpec Statement Bool pSpec) + (verifier : Verifier oSpec Statement TrivialStatement pSpec) (rbrSoundnessError : pSpec.ChallengeIdx → ℝ≥0) : Prop := verifier.rbrSoundness langIn acceptRejectRel.language rbrSoundnessError @[reducible, simp] -def rbrKnowledgeSoundness (relation : Set (Statement × Bool)) - (verifier : Verifier oSpec Statement Bool pSpec) +def rbrKnowledgeSoundness (relation : Set (Statement × Witness)) + (verifier : Verifier oSpec Statement TrivialStatement pSpec) (rbrKnowledgeError : pSpec.ChallengeIdx → ℝ≥0) : Prop := verifier.rbrKnowledgeSoundness relation acceptRejectRel rbrKnowledgeError @@ -313,7 +454,8 @@ namespace OracleProof @[reducible, simp] def rbrSoundness (langIn : Set (Statement × ∀ i, OStatement i)) - (verifier : OracleVerifier oSpec Statement OStatement Bool (fun _ : Empty => Unit) pSpec) + (verifier : OracleVerifier oSpec Statement OStatement + TrivialStatement TrivialOracleStatement pSpec) (rbrSoundnessError : pSpec.ChallengeIdx → ℝ≥0) : Prop := verifier.rbrSoundness langIn acceptRejectOracleRel.language rbrSoundnessError @@ -321,7 +463,8 @@ def rbrSoundness reductions. -/ def rbrKnowledgeSoundness (relIn : Set ((Statement × ∀ i, OStatement i) × Witness)) - (verifier : OracleVerifier oSpec Statement OStatement Bool (fun _ : Empty => Unit) pSpec) + (verifier : OracleVerifier oSpec Statement OStatement + TrivialStatement TrivialOracleStatement pSpec) (rbrKnowledgeError : pSpec.ChallengeIdx → ℝ≥0) : Prop := verifier.rbrKnowledgeSoundness relIn acceptRejectOracleRel rbrKnowledgeError diff --git a/ArkLib/OracleReduction/VectorIOR.lean b/ArkLib/OracleReduction/VectorIOR.lean index 5190d9b4e..2aeb84079 100644 --- a/ArkLib/OracleReduction/VectorIOR.lean +++ b/ArkLib/OracleReduction/VectorIOR.lean @@ -93,10 +93,11 @@ variable {n : ℕ} {ι : Type} witnesses to be vectors as well, though this can be done if needed. -/ @[reducible] def VectorIOR (oSpec : OracleSpec ι) - (StmtIn : Type) {ιₛᵢ : Type} (OStmtIn : ιₛᵢ → Type) (WitIn : Type) - (StmtOut : Type) {ιₛₒ : Type} (OStmtOut : ιₛₒ → Type) (WitOut : Type) - (vPSpec : ProtocolSpec.VectorSpec n) (A : Type) - [∀ i, OracleInterface (OStmtIn i)] := + (StmtIn : Type) {ιₛᵢ : Type} (OStmtIn : ιₛᵢ → Type) [Oₛᵢ : ∀ i, OracleInterface (OStmtIn i)] + (WitIn : Type) + (StmtOut : Type) {ιₛₒ : Type} (OStmtOut : ιₛₒ → Type) [Oₛₒ : ∀ i, OracleInterface (OStmtOut i)] + (WitOut : Type) + (vPSpec : ProtocolSpec.VectorSpec n) (A : Type) := OracleReduction oSpec StmtIn OStmtIn WitIn StmtOut OStmtOut WitOut (vPSpec.toProtocolSpec A) /-- Vector Interactive Oracle Proofs @@ -118,8 +119,11 @@ open scoped NNReal namespace VectorIOR -variable {StmtIn WitIn StmtOut WitOut : Type} {ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} - [∀ i, OracleInterface (OStmtIn i)] {ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} +variable + {StmtIn : Type} {ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} [Oₛᵢ : ∀ i, OracleInterface (OStmtIn i)] + {WitIn : Type} + {StmtOut : Type} {ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} [Oₛₒ : ∀ i, OracleInterface (OStmtOut i)] + {WitOut : Type} /-- A vector IOR is **secure** with respect to input relation `relIn`, output relation `relOut`, and round-by-round knowledge error `ε_rbr` if it satisfies (perfect) completeness and round-by-round @@ -161,7 +165,7 @@ class IsSecure /-- The reduction is round-by-round knowledge sound with respect to `relIn`, `relOut`, `ε_rbr`, and the state function. -/ is_rbr_knowledge_sound : - OracleProof.rbrKnowledgeSoundness relation vectorIOP.verifier ε_rbr + OracleProof.rbrKnowledgeSoundness relation (vectorIOP.verifier (Oₛₒ := isEmptyElim)) ε_rbr /-- A vector IOP **of proximity** is **secure** with respect to completeness relation `completeRelation`, soundness relation `soundRelation`, and round-by-round knowledge error @@ -180,6 +184,6 @@ class IsSecureWithGap /-- The reduction is round-by-round knowledge sound with respect to `relIn`, `relOut`, `ε_rbr`, and the state function. -/ is_rbr_knowledge_sound : - OracleProof.rbrKnowledgeSoundness soundRelation vectorIOP.verifier ε_rbr + OracleProof.rbrKnowledgeSoundness soundRelation (vectorIOP.verifier (Oₛₒ := isEmptyElim)) ε_rbr end VectorIOP diff --git a/ArkLib/ToVCVio/Oracle.lean b/ArkLib/ToVCVio/Oracle.lean index 9a584c3e0..2f3db9b61 100644 --- a/ArkLib/ToVCVio/Oracle.lean +++ b/ArkLib/ToVCVio/Oracle.lean @@ -17,9 +17,9 @@ variable {ι : Type} {α β γ : Type} /-- A function that implements the oracle interface specified by `spec`, and queries no further oracles. -/ +@[reducible, simp] def Oracle (spec : OracleSpec ι) := (i : ι) → spec.domain i → spec.range i - variable [DecidableEq α] [DecidableEq β] [Inhabited β] [Fintype β] [Inhabited γ] [Fintype γ] namespace OracleSpec