Lifting Reductions to Larger Contexts #
Sequential composition is usually not enough to represent oracle reductions in a modular way. We also need to formalize virtual oracle reductions, which lift reductions from one (virtual / inner) context into the another (real / outer) context.
This is what is meant when we informally say "apply so-and-so protocol to this quantity (derived from the input statement & witness)".
Put in other words, we define a mapping between the input-output interfaces of two (oracle) reductions, without changing anything about the underlying reductions.
Recall that the input-output interface of an oracle reduction consists of:
- Input:
OuterStmtIn : Type,OuterOStmtIn : ιₛᵢ → Type, andOuterWitIn : Type - Output:
OuterStmtOut : Type,OuterOStmtOut : ιₛₒ → Type, andOuterWitOut : Type
The liftContext is defined as the following mappings of projections / lifts:
projStmt : OuterStmtIn → InnerStmtInprojOStmt : (simulation involving OuterOStmtIn to produce InnerOStmtIn)projWit : OuterWitIn → InnerWitInliftStmt : OuterStmtIn × InnerStmtOut → OuterStmtOutliftOStmt : (simulation involving InnerOStmtOut to produce OuterOStmtOut)liftWit : OuterWitIn × InnerWitOut → OuterWitOut
Note that since completeness & soundness for oracle reductions are defined in terms of the same properties after converting to (non-oracle) reductions, we only need to focus our efforts on the non-oracle case.
Note that this exactly corresponds to lenses in programming languages / category theory. Namely,
liftContext on the inputs correspond to a view/get operation (our "proj"), while liftContext
on the output corresponds to a modify/set operation (our "lift").
More precisely, the proj/lift operations correspond to a Lens between two monomial polyonmial
functors: OuterCtxIn y^ OuterCtxOut ⇆ InnerCtxIn y^ InnerCtxOut.
All the lens definitions are in Lens.lean. This file deals with the lens applied to reductions.
See OracleReduction.lean for the application to oracle reduction.
def
Prover.liftContext
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut : Type}
(lens : Context.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut)
(P : Prover oSpec InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut pSpec)
:
Prover oSpec OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut pSpec
The outer prover after lifting invokes the inner prover on the projected input, and lifts the output
Equations
Instances For
def
Verifier.liftContext
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type}
(lens : Statement.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut)
(V : Verifier oSpec InnerStmtIn InnerStmtOut pSpec)
:
Verifier oSpec OuterStmtIn OuterStmtOut pSpec
The outer verifier after lifting invokes the inner verifier on the projected input, and lifts the output
Equations
Instances For
def
Reduction.liftContext
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut : Type}
(lens : Context.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut)
(R : Reduction oSpec InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut pSpec)
:
Reduction oSpec OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut pSpec
The outer reduction after lifting is the combination of the lifting of the prover and verifier
Equations
Instances For
def
Extractor.Straightline.liftContext
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut : Type}
(lens : Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut)
(E : Straightline oSpec InnerStmtIn InnerWitIn InnerWitOut pSpec)
:
Straightline oSpec OuterStmtIn OuterWitIn OuterWitOut pSpec
The outer extractor after lifting invokes the inner extractor on the projected input, and lifts the output
Equations
Instances For
def
Extractor.RoundByRound.liftContext
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut : Type}
{WitMid : Fin (n + 1) → Type}
(lens : Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut)
(E : RoundByRound oSpec InnerStmtIn InnerWitIn InnerWitOut pSpec WitMid)
:
RoundByRound oSpec OuterStmtIn OuterWitIn OuterWitOut pSpec WitMid
The outer round-by-round extractor after lifting invokes the inner extractor on the projected input, and lifts the output
Equations
Instances For
def
Verifier.compatStatement
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type}
(lens : Statement.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut)
(V : Verifier oSpec InnerStmtIn InnerStmtOut pSpec)
:
OuterStmtIn → InnerStmtOut → Prop
Compatibility relation between the outer input statement and the inner output statement, relative to a verifier.
We require that the inner output statement is a possible output of the verifier on the outer input statement, for any given transcript. Note that we have to existentially quantify over transcripts since we only reference the verifier, and there's no way to get the transcript without a prover.
Equations
Instances For
def
Reduction.compatContext
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut : Type}
(lens : Context.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut)
(R : Reduction oSpec InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut pSpec)
:
Compatibility relation between the outer input context and the inner output context, relative to a reduction.
We require that the inner output context (statement + witness) is a possible output of the reduction on the outer input context (statement + witness).
Equations
Instances For
def
Extractor.Straightline.compatWit
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut : Type}
(lens : Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut)
(E : Straightline oSpec InnerStmtIn InnerWitIn InnerWitOut pSpec)
:
Compatibility relation between the outer input witness and the inner output witness, relative to a straightline extractor.
We require that the inner output witness is a possible output of the straightline extractor on the outer input witness, for a given input statement, transcript, and prover and verifier's query logs.
Equations
Instances For
def
Verifier.StateFunction.liftContext
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut σ : Type}
{init : ProbComp σ}
{impl : QueryImpl oSpec (StateT σ ProbComp)}
(lens : Statement.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut)
(V : Verifier oSpec InnerStmtIn InnerStmtOut pSpec)
(outerLangIn : Set OuterStmtIn)
(outerLangOut : Set OuterStmtOut)
(innerLangIn : Set InnerStmtIn)
(innerLangOut : Set InnerStmtOut)
[lensSound : Statement.Lens.IsSound outerLangIn outerLangOut innerLangIn innerLangOut (compatStatement lens V) lens]
(stF : StateFunction init impl innerLangIn innerLangOut V)
:
StateFunction init impl outerLangIn outerLangOut (Verifier.liftContext lens V)
The outer state function after lifting invokes the inner state function on the projected input, and lifts the output
Equations
Instances For
theorem
Prover.liftContext_processRound
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut : Type}
{lens : Context.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut}
{i : Fin n}
{P : Prover oSpec InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut pSpec}
{resultRound :
OracleComp (oSpec ++ₒ [pSpec.Challenge]ₒ)
(ProtocolSpec.Transcript i.castSucc pSpec × (liftContext lens P).PrvState i.castSucc)}
:
processRound i (liftContext lens P) resultRound = do
let __discr ← resultRound
match __discr with
| (transcript, prvState, outerStmtIn, outerWitIn) => do
let __discr ← processRound i P (pure (transcript, prvState))
match __discr with
| (newTranscript, newPrvState) => pure (newTranscript, newPrvState, outerStmtIn, outerWitIn)
Lifting the prover intertwines with the process round function
theorem
Prover.liftContext_runToRound
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut : Type}
{lens : Context.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut}
{outerStmtIn : OuterStmtIn}
{outerWitIn : OuterWitIn}
{i : Fin (n + 1)}
(P : Prover oSpec InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut pSpec)
:
runToRound i outerStmtIn outerWitIn (liftContext lens P) = do
let __discr ←
Function.uncurry (fun (stmt : InnerStmtIn) (wit : InnerWitIn) => runToRound i stmt wit P)
(lens.proj (outerStmtIn, outerWitIn))
match __discr with
| (transcript, prvState) => pure (transcript, prvState, outerStmtIn, outerWitIn)
theorem
Prover.liftContext_runWithLogToRound
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut : Type}
{lens : Context.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut}
{outerStmtIn : OuterStmtIn}
{outerWitIn : OuterWitIn}
{i : Fin (n + 1)}
(P : Prover oSpec InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut pSpec)
:
runWithLogToRound i outerStmtIn outerWitIn (liftContext lens P) = do
let __discr ←
Function.uncurry (fun (stmt : InnerStmtIn) (wit : InnerWitIn) => runWithLogToRound i stmt wit P)
(lens.proj (outerStmtIn, outerWitIn))
match __discr with
| ((transcript, prvState), queryLog) => pure ((transcript, prvState, outerStmtIn, outerWitIn), queryLog)
theorem
Prover.liftContext_run
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut : Type}
{lens : Context.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut}
{outerStmtIn : OuterStmtIn}
{outerWitIn : OuterWitIn}
{P : Prover oSpec InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut pSpec}
:
run outerStmtIn outerWitIn (liftContext lens P) = do
let __discr ←
Function.uncurry (fun (stmt : InnerStmtIn) (wit : InnerWitIn) => run stmt wit P)
(lens.proj (outerStmtIn, outerWitIn))
match __discr with
| (fullTranscript, innerCtxOut) => pure (fullTranscript, lens.lift (outerStmtIn, outerWitIn) innerCtxOut)
Running the lifted outer prover is equivalent to running the inner prover on the projected input, and then integrating the output
theorem
Prover.liftContext_runWithLog
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut : Type}
{lens : Context.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut}
{outerStmtIn : OuterStmtIn}
{outerWitIn : OuterWitIn}
{P : Prover oSpec InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut pSpec}
:
runWithLog outerStmtIn outerWitIn (liftContext lens P) = do
let __discr ←
Function.uncurry (fun (stmt : InnerStmtIn) (wit : InnerWitIn) => runWithLog stmt wit P)
(lens.proj (outerStmtIn, outerWitIn))
match __discr with
| ((fullTranscript, innerCtxOut), queryLog) =>
pure ((fullTranscript, lens.lift (outerStmtIn, outerWitIn) innerCtxOut), queryLog)
Lifting the prover intertwines with logging queries of the prover
theorem
Reduction.liftContext_run
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut : Type}
{lens : Context.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut}
{outerStmtIn : OuterStmtIn}
{outerWitIn : OuterWitIn}
{R : Reduction oSpec InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut pSpec}
:
run outerStmtIn outerWitIn (liftContext lens R) = do
let __discr ←
Function.uncurry (fun (stmt : InnerStmtIn) (wit : InnerWitIn) => run stmt wit R)
(lens.proj (outerStmtIn, outerWitIn))
match __discr with
| ((fullTranscript, innerCtxOut), verInnerStmtOut) =>
pure
((fullTranscript, lens.lift (outerStmtIn, outerWitIn) innerCtxOut), lens.stmt.lift outerStmtIn verInnerStmtOut)
theorem
Reduction.liftContext_runWithLog
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut : Type}
{lens : Context.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut}
{outerStmtIn : OuterStmtIn}
{outerWitIn : OuterWitIn}
{R : Reduction oSpec InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut pSpec}
:
runWithLog outerStmtIn outerWitIn (liftContext lens R) = do
let __discr ←
Function.uncurry (fun (stmt : InnerStmtIn) (wit : InnerWitIn) => runWithLog stmt wit R)
(lens.proj (outerStmtIn, outerWitIn))
match __discr with
| (((fullTranscript, innerCtxOut), verInnerStmtOut), queryLog) =>
pure
(((fullTranscript, lens.lift (outerStmtIn, outerWitIn) innerCtxOut), lens.stmt.lift outerStmtIn verInnerStmtOut), queryLog)
theorem
Reduction.liftContext_completeness
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut : Type}
[(i : pSpec.ChallengeIdx) → OracleComp.SelectableType (pSpec.Challenge i)]
{σ : Type}
{init : ProbComp σ}
{impl : QueryImpl oSpec (StateT σ ProbComp)}
{outerRelIn : Set (OuterStmtIn × OuterWitIn)}
{outerRelOut : Set (OuterStmtOut × OuterWitOut)}
{innerRelIn : Set (InnerStmtIn × InnerWitIn)}
{innerRelOut : Set (InnerStmtOut × InnerWitOut)}
{R : Reduction oSpec InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut pSpec}
{completenessError : NNReal}
{lens : Context.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut}
[lensComplete : Context.Lens.IsComplete outerRelIn innerRelIn outerRelOut innerRelOut (compatContext lens R) lens]
(h : completeness init impl innerRelIn innerRelOut R completenessError)
:
completeness init impl outerRelIn outerRelOut (liftContext lens R) completenessError
Lifting the reduction preserves completeness, assuming the lens satisfies its completeness conditions
theorem
Reduction.liftContext_perfectCompleteness
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut : Type}
[(i : pSpec.ChallengeIdx) → OracleComp.SelectableType (pSpec.Challenge i)]
{σ : Type}
{init : ProbComp σ}
{impl : QueryImpl oSpec (StateT σ ProbComp)}
{outerRelIn : Set (OuterStmtIn × OuterWitIn)}
{outerRelOut : Set (OuterStmtOut × OuterWitOut)}
{innerRelIn : Set (InnerStmtIn × InnerWitIn)}
{innerRelOut : Set (InnerStmtOut × InnerWitOut)}
{R : Reduction oSpec InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut pSpec}
{lens : Context.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut}
[lensComplete : Context.Lens.IsComplete outerRelIn innerRelIn outerRelOut innerRelOut (compatContext lens R) lens]
(h : perfectCompleteness init impl innerRelIn innerRelOut R)
:
perfectCompleteness init impl outerRelIn outerRelOut (liftContext lens R)
theorem
Verifier.liftContext_soundness
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type}
[(i : pSpec.ChallengeIdx) → OracleComp.SelectableType (pSpec.Challenge i)]
{σ : Type}
{init : ProbComp σ}
{impl : QueryImpl oSpec (StateT σ ProbComp)}
[Inhabited InnerStmtOut]
{outerLangIn : Set OuterStmtIn}
{outerLangOut : Set OuterStmtOut}
{innerLangIn : Set InnerStmtIn}
{innerLangOut : Set InnerStmtOut}
{soundnessError : NNReal}
{lens : Statement.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut}
(V : Verifier oSpec InnerStmtIn InnerStmtOut pSpec)
[lensSound : Statement.Lens.IsSound outerLangIn outerLangOut innerLangIn innerLangOut (compatStatement lens V) lens]
(h : soundness init impl innerLangIn innerLangOut V soundnessError)
:
soundness init impl outerLangIn outerLangOut (liftContext lens V) soundnessError
Lifting the reduction preserves soundness, assuming the lens satisfies its soundness conditions
theorem
Verifier.liftContext_knowledgeSoundness
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut : Type}
[(i : pSpec.ChallengeIdx) → OracleComp.SelectableType (pSpec.Challenge i)]
{σ : Type}
{init : ProbComp σ}
{impl : QueryImpl oSpec (StateT σ ProbComp)}
[Inhabited InnerStmtOut]
[Inhabited InnerWitIn]
{outerRelIn : Set (OuterStmtIn × OuterWitIn)}
{outerRelOut : Set (OuterStmtOut × OuterWitOut)}
{innerRelIn : Set (InnerStmtIn × InnerWitIn)}
{innerRelOut : Set (InnerStmtOut × InnerWitOut)}
{knowledgeError : NNReal}
{stmtLens : Statement.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut}
{witLens : Witness.InvLens OuterStmtIn OuterWitIn OuterWitOut InnerWitIn InnerWitOut}
(V : Verifier oSpec InnerStmtIn InnerStmtOut pSpec)
[lensKS :
Extractor.Lens.IsKnowledgeSound outerRelIn innerRelIn outerRelOut innerRelOut (compatStatement stmtLens V)
(fun (x : OuterWitOut) (x : InnerWitIn) => True) { stmt := stmtLens, wit := witLens }]
(h : knowledgeSoundness init impl innerRelIn innerRelOut V knowledgeError)
:
knowledgeSoundness init impl outerRelIn outerRelOut (liftContext stmtLens V) knowledgeError
theorem
Verifier.liftContext_rbr_soundness
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type}
[(i : pSpec.ChallengeIdx) → OracleComp.SelectableType (pSpec.Challenge i)]
{σ : Type}
{init : ProbComp σ}
{impl : QueryImpl oSpec (StateT σ ProbComp)}
[Inhabited InnerStmtOut]
{outerLangIn : Set OuterStmtIn}
{outerLangOut : Set OuterStmtOut}
{innerLangIn : Set InnerStmtIn}
{innerLangOut : Set InnerStmtOut}
{rbrSoundnessError : pSpec.ChallengeIdx → NNReal}
{lens : Statement.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut}
(V : Verifier oSpec InnerStmtIn InnerStmtOut pSpec)
[lensSound : Statement.Lens.IsSound outerLangIn outerLangOut innerLangIn innerLangOut (compatStatement lens V) lens]
(h : rbrSoundness init impl innerLangIn innerLangOut V rbrSoundnessError)
:
rbrSoundness init impl outerLangIn outerLangOut (liftContext lens V) rbrSoundnessError
theorem
Verifier.liftContext_rbr_knowledgeSoundness
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut : Type}
[(i : pSpec.ChallengeIdx) → OracleComp.SelectableType (pSpec.Challenge i)]
{σ : Type}
{init : ProbComp σ}
{impl : QueryImpl oSpec (StateT σ ProbComp)}
[Inhabited InnerStmtOut]
[Inhabited InnerWitIn]
{outerRelIn : Set (OuterStmtIn × OuterWitIn)}
{outerRelOut : Set (OuterStmtOut × OuterWitOut)}
{innerRelIn : Set (InnerStmtIn × InnerWitIn)}
{innerRelOut : Set (InnerStmtOut × InnerWitOut)}
{rbrKnowledgeError : pSpec.ChallengeIdx → NNReal}
{stmtLens : Statement.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut}
{witLens : Witness.InvLens OuterStmtIn OuterWitIn OuterWitOut InnerWitIn InnerWitOut}
(V : Verifier oSpec InnerStmtIn InnerStmtOut pSpec)
[lensKS :
Extractor.Lens.IsKnowledgeSound outerRelIn innerRelIn outerRelOut innerRelOut (compatStatement stmtLens V)
(fun (x : OuterWitOut) (x : InnerWitIn) => True) { stmt := stmtLens, wit := witLens }]
(h : rbrKnowledgeSoundness init impl innerRelIn innerRelOut V rbrKnowledgeError)
:
rbrKnowledgeSoundness init impl outerRelIn outerRelOut (liftContext stmtLens V) rbrKnowledgeError
instance
instTestLensComplete :
Context.Lens.IsComplete outerRelIn_Test innerRelIn_Test outerRelOut_Test innerRelOut_Test
(fun (x : OuterStmtIn_Test × Unit) (x_1 : InnerStmtOut_Test × Unit) =>
match x with
| ((p, q, snd), snd_1) =>
match x_1 with
| ((f, snd), snd_2) => p * q = f)
testLens
def
instTestLensKnowledgeSound :
Extractor.Lens.IsKnowledgeSound outerRelIn_Test innerRelIn_Test outerRelOut_Test innerRelOut_Test
(fun (x : OuterStmtIn_Test) (x_1 : InnerStmtOut_Test) =>
match x with
| (p, q, snd) =>
match x_1 with
| (f, snd) => p * q = f)
(fun (x x : Unit) => True) testLensE