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 : ContextLens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut]
(P : Prover pSpec oSpec InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut)
:
Prover pSpec oSpec OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut
The outer prover after lifting invokes the inner prover on the projected input, and lifts the output
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Verifier.liftContext
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type}
[lens : StatementLens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut]
(V : Verifier pSpec oSpec InnerStmtIn InnerStmtOut)
:
Verifier pSpec oSpec OuterStmtIn OuterStmtOut
The outer verifier after lifting invokes the inner verifier on the projected input, and lifts the output
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Reduction.liftContext
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut : Type}
[lens : ContextLens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut]
(R : Reduction pSpec oSpec InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut)
:
Reduction pSpec oSpec OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut
The outer reduction after lifting is the combination of the lifting of the prover and verifier
Equations
- R.liftContext = { prover := R.prover.liftContext, verifier := R.verifier.liftContext }
Instances For
def
StraightlineExtractor.liftContext
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut : Type}
[lens : StatementLens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut]
[lensInv : WitnessLensInv OuterWitIn OuterWitOut InnerWitIn InnerWitOut]
(E : StraightlineExtractor pSpec oSpec InnerStmtIn InnerWitIn InnerWitOut)
:
StraightlineExtractor pSpec oSpec OuterStmtIn OuterWitIn OuterWitOut
The outer extractor after lifting invokes the inner extractor on the projected input, and lifts the output
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
RBRExtractor.liftContext
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut : Type}
[lens : ContextLens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut]
[rbrLensInv : RBRWitnessLensInv OuterWitIn InnerWitIn]
(E : RBRExtractor pSpec oSpec InnerStmtIn InnerWitIn)
:
RBRExtractor pSpec oSpec OuterStmtIn OuterWitIn
The outer round-by-round extractor after lifting invokes the inner extractor on the projected input, and lifts the output
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Verifier.compatStatement
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type}
(lens : StatementLens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut)
(V : Verifier pSpec oSpec InnerStmtIn InnerStmtOut)
:
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
- One or more equations did not get rendered due to their size.
Instances For
def
Reduction.compatContext
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
[(i : pSpec.ChallengeIdx) → VCVCompatible (pSpec.Challenge i)]
{OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut : Type}
(lens : ContextLens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut)
(R : Reduction pSpec oSpec InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut)
:
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
- One or more equations did not get rendered due to their size.
Instances For
def
Verifier.StraightlineExtractor.compatWit
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterWitIn OuterWitOut InnerStmtIn InnerWitIn InnerWitOut : Type}
[oSpec.FiniteRange]
(lensInv : WitnessLensInv OuterWitIn OuterWitOut InnerWitIn InnerWitOut)
(E : StraightlineExtractor pSpec oSpec InnerStmtIn InnerWitIn InnerWitOut)
:
OuterWitOut → InnerWitIn → Prop
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
- One or more equations did not get rendered due to their size.
Instances For
def
Verifier.StateFunction.liftContext
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type}
[oSpec.FiniteRange]
[lens : StatementLens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut]
(outerLangIn : Set OuterStmtIn)
(outerLangOut : Set OuterStmtOut)
(innerLangIn : Set InnerStmtIn)
(innerLangOut : Set InnerStmtOut)
(V : Verifier pSpec oSpec InnerStmtIn InnerStmtOut)
[lensRBRSound :
StatementLens.IsRBRSound outerLangIn outerLangOut innerLangIn innerLangOut (compatStatement lens V) lens]
(stF : StateFunction pSpec oSpec innerLangIn innerLangOut V)
:
StateFunction pSpec oSpec outerLangIn outerLangOut V.liftContext
The outer state function after lifting invokes the inner state function on the projected input, and lifts the output
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Prover.liftContext_processRound
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut : Type}
[(i : pSpec.ChallengeIdx) → VCVCompatible (pSpec.Challenge i)]
[lens : ContextLens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut]
{i : Fin n}
(P : Prover pSpec oSpec InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut)
{resultRound :
OracleComp (oSpec ++ₒ [pSpec.Challenge]ₒ)
(ProtocolSpec.Transcript i.castSucc pSpec × P.liftContext.PrvState i.castSucc)}
:
processRound i P.liftContext 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}
[(i : pSpec.ChallengeIdx) → VCVCompatible (pSpec.Challenge i)]
[lens : ContextLens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut]
{outerStmtIn : OuterStmtIn}
{outerWitIn : OuterWitIn}
{i : Fin (n + 1)}
(P : Prover pSpec oSpec InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut)
:
runToRound i outerStmtIn outerWitIn P.liftContext = do
let __discr ←
runToRound i (StatementLens.projStmt OuterStmtOut InnerStmtOut outerStmtIn)
(WitnessLens.projWit OuterWitOut InnerWitOut outerWitIn) P
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}
[(i : pSpec.ChallengeIdx) → VCVCompatible (pSpec.Challenge i)]
[lens : ContextLens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut]
{outerStmtIn : OuterStmtIn}
{outerWitIn : OuterWitIn}
{i : Fin (n + 1)}
(P : Prover pSpec oSpec InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut)
:
runWithLogToRound i outerStmtIn outerWitIn P.liftContext = do
let __discr ←
runWithLogToRound i (StatementLens.projStmt OuterStmtOut InnerStmtOut outerStmtIn)
(WitnessLens.projWit OuterWitOut InnerWitOut outerWitIn) P
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}
[(i : pSpec.ChallengeIdx) → VCVCompatible (pSpec.Challenge i)]
[lens : ContextLens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut]
{outerStmtIn : OuterStmtIn}
{outerWitIn : OuterWitIn}
(P : Prover pSpec oSpec InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut)
:
run outerStmtIn outerWitIn P.liftContext = do
let __discr ←
run (StatementLens.projStmt OuterStmtOut InnerStmtOut outerStmtIn)
(WitnessLens.projWit OuterWitOut InnerWitOut outerWitIn) P
match __discr with
| (innerStmtOut, innerWitOut, fullTranscript) =>
pure
(StatementLens.liftStmt InnerStmtIn (outerStmtIn, innerStmtOut), WitnessLens.liftWit InnerWitIn (outerWitIn, innerWitOut), fullTranscript)
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}
[(i : pSpec.ChallengeIdx) → VCVCompatible (pSpec.Challenge i)]
[lens : ContextLens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut]
{outerStmtIn : OuterStmtIn}
{outerWitIn : OuterWitIn}
(P : Prover pSpec oSpec InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut)
:
runWithLog outerStmtIn outerWitIn P.liftContext = do
let __discr ←
runWithLog (StatementLens.projStmt OuterStmtOut InnerStmtOut outerStmtIn)
(WitnessLens.projWit OuterWitOut InnerWitOut outerWitIn) P
match __discr with
| (innerStmtOut, innerWitOut, fullTranscript, queryLog) =>
pure
(StatementLens.liftStmt InnerStmtIn (outerStmtIn, innerStmtOut), WitnessLens.liftWit InnerWitIn (outerWitIn, innerWitOut), fullTranscript, queryLog)
theorem
Reduction.liftContext_run
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut : Type}
[(i : pSpec.ChallengeIdx) → VCVCompatible (pSpec.Challenge i)]
[lens : ContextLens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut]
{outerStmtIn : OuterStmtIn}
{outerWitIn : OuterWitIn}
(R : Reduction pSpec oSpec InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut)
:
run outerStmtIn outerWitIn R.liftContext = do
let __discr ←
run (StatementLens.projStmt OuterStmtOut InnerStmtOut outerStmtIn)
(WitnessLens.projWit OuterWitOut InnerWitOut outerWitIn) R
match __discr with
| ((prvInnerStmtOut, innerWitOut), verInnerStmtOut, fullTranscript) =>
pure
((StatementLens.liftStmt InnerStmtIn (outerStmtIn, prvInnerStmtOut), WitnessLens.liftWit InnerWitIn (outerWitIn, innerWitOut)), StatementLens.liftStmt InnerStmtIn (outerStmtIn, verInnerStmtOut), fullTranscript)
theorem
Reduction.liftContext_runWithLog
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut : Type}
[(i : pSpec.ChallengeIdx) → VCVCompatible (pSpec.Challenge i)]
[lens : ContextLens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut]
{outerStmtIn : OuterStmtIn}
{outerWitIn : OuterWitIn}
(R : Reduction pSpec oSpec InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut)
:
runWithLog outerStmtIn outerWitIn R.liftContext = do
let __discr ←
runWithLog (StatementLens.projStmt OuterStmtOut InnerStmtOut outerStmtIn)
(WitnessLens.projWit OuterWitOut InnerWitOut outerWitIn) R
match __discr with
| ((prvInnerStmtOut, innerWitOut), verInnerStmtOut, fullTranscript, queryLog) =>
pure
((StatementLens.liftStmt InnerStmtIn (outerStmtIn, prvInnerStmtOut), WitnessLens.liftWit InnerWitIn (outerWitIn, innerWitOut)), StatementLens.liftStmt InnerStmtIn (outerStmtIn, verInnerStmtOut), fullTranscript, queryLog)
theorem
Reduction.liftContext_completeness
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut : Type}
[(i : pSpec.ChallengeIdx) → VCVCompatible (pSpec.Challenge i)]
[oSpec.FiniteRange]
{outerRelIn : OuterStmtIn → OuterWitIn → Prop}
{outerRelOut : OuterStmtOut → OuterWitOut → Prop}
{innerRelIn : InnerStmtIn → InnerWitIn → Prop}
{innerRelOut : InnerStmtOut → InnerWitOut → Prop}
{R : Reduction pSpec oSpec InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut}
{completenessError : NNReal}
[lens : ContextLens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut]
[lensComplete : ContextLens.IsComplete outerRelIn innerRelIn outerRelOut innerRelOut (compatContext lens R) lens]
(h : completeness innerRelIn innerRelOut R completenessError)
:
completeness outerRelIn outerRelOut R.liftContext 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) → VCVCompatible (pSpec.Challenge i)]
[oSpec.FiniteRange]
{outerRelIn : OuterStmtIn → OuterWitIn → Prop}
{outerRelOut : OuterStmtOut → OuterWitOut → Prop}
{innerRelIn : InnerStmtIn → InnerWitIn → Prop}
{innerRelOut : InnerStmtOut → InnerWitOut → Prop}
{R : Reduction pSpec oSpec InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut}
[lens : ContextLens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut OuterWitIn OuterWitOut InnerWitIn InnerWitOut]
[lensComplete : ContextLens.IsComplete outerRelIn innerRelIn outerRelOut innerRelOut (compatContext lens R) lens]
(h : perfectCompleteness innerRelIn innerRelOut R)
:
perfectCompleteness outerRelIn outerRelOut R.liftContext
theorem
Verifier.liftContext_soundness
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type}
[(i : pSpec.ChallengeIdx) → VCVCompatible (pSpec.Challenge i)]
[oSpec.FiniteRange]
[Inhabited InnerStmtOut]
{outerLangIn : Set OuterStmtIn}
{outerLangOut : Set OuterStmtOut}
{innerLangIn : Set InnerStmtIn}
{innerLangOut : Set InnerStmtOut}
{soundnessError : NNReal}
[lens : StatementLens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut]
(V : Verifier pSpec oSpec InnerStmtIn InnerStmtOut)
[lensSound : StatementLens.IsSound outerLangIn outerLangOut innerLangIn innerLangOut (compatStatement lens V) lens]
(h : soundness innerLangIn innerLangOut V soundnessError)
:
soundness outerLangIn outerLangOut V.liftContext 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) → VCVCompatible (pSpec.Challenge i)]
[oSpec.FiniteRange]
[Inhabited InnerStmtOut]
[Inhabited InnerWitIn]
{outerRelIn : OuterStmtIn → OuterWitIn → Prop}
{outerRelOut : OuterStmtOut → OuterWitOut → Prop}
{innerRelIn : InnerStmtIn → InnerWitIn → Prop}
{innerRelOut : InnerStmtOut → InnerWitOut → Prop}
{knowledgeError : NNReal}
[lens : StatementLens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut]
(lensInv : WitnessLensInv OuterWitIn OuterWitOut InnerWitIn InnerWitOut)
(V : Verifier pSpec oSpec InnerStmtIn InnerStmtOut)
[lensKnowledgeSound :
StatementLens.IsKnowledgeSound outerRelIn innerRelIn outerRelOut innerRelOut (compatStatement lens V)
(fun (x : OuterWitOut) (x : InnerWitIn) => True) lensInv lens]
(h : knowledgeSoundness innerRelIn innerRelOut V knowledgeError)
:
knowledgeSoundness outerRelIn outerRelOut V.liftContext knowledgeError
theorem
Verifier.liftContext_rbr_soundness
{n : ℕ}
{pSpec : ProtocolSpec n}
{ι : Type}
{oSpec : OracleSpec ι}
{OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type}
[(i : pSpec.ChallengeIdx) → VCVCompatible (pSpec.Challenge i)]
[oSpec.FiniteRange]
[Inhabited InnerStmtOut]
{outerLangIn : Set OuterStmtIn}
{outerLangOut : Set OuterStmtOut}
{innerLangIn : Set InnerStmtIn}
{innerLangOut : Set InnerStmtOut}
{rbrSoundnessError : pSpec.ChallengeIdx → NNReal}
[lens : StatementLens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut]
(V : Verifier pSpec oSpec InnerStmtIn InnerStmtOut)
[lensRBRSound :
StatementLens.IsRBRSound outerLangIn outerLangOut innerLangIn innerLangOut (compatStatement lens V) lens]
(h : rbrSoundness innerLangIn innerLangOut V rbrSoundnessError)
:
rbrSoundness outerLangIn outerLangOut V.liftContext 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) → VCVCompatible (pSpec.Challenge i)]
[oSpec.FiniteRange]
[Inhabited InnerStmtOut]
[Inhabited InnerWitIn]
{outerRelIn : OuterStmtIn → OuterWitIn → Prop}
{outerRelOut : OuterStmtOut → OuterWitOut → Prop}
{innerRelIn : InnerStmtIn → InnerWitIn → Prop}
{innerRelOut : InnerStmtOut → InnerWitOut → Prop}
{rbrKnowledgeError : pSpec.ChallengeIdx → NNReal}
[lens : StatementLens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut]
(lensInv : WitnessLensInv OuterWitIn OuterWitOut InnerWitIn InnerWitOut)
(V : Verifier pSpec oSpec InnerStmtIn InnerStmtOut)
[lensKnowledgeSound :
StatementLens.IsKnowledgeSound outerRelIn innerRelIn outerRelOut innerRelOut (compatStatement lens V)
(fun (x : OuterWitOut) (x : InnerWitIn) => True) lensInv lens]
(h : rbrKnowledgeSoundness innerRelIn innerRelOut V rbrKnowledgeError)
:
rbrKnowledgeSoundness outerRelIn outerRelOut V.liftContext rbrKnowledgeError
Equations
Instances For
Instances For
Equations
- innerRelIn_Test (f, t) x✝ = (∑ x ∈ {0, 1}, Polynomial.eval x f = t)
Instances For
Equations
- OuterStmtOut_Test = (Polynomial ℤ × Polynomial ℤ × ℤ × ℤ)
Instances For
Equations
- outerRelOut_Test (p, q, t, r) x✝ = (Polynomial.eval r (p * q) = t)
Instances For
Equations
- innerRelOut_Test (f, t, r) x✝ = (Polynomial.eval r f = t)
Instances For
def
testLensComplete :
ContextLens.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), PUnit.unit) =>
match x_1 with
| ((f, snd), PUnit.unit) => p * q = f)
testLens