Efficient oracle substitution with saved samples

A supplied list replaces fresh draws in a closed external handler. Its local contract covers every supplied value and the fallback used on short lists. The sample list only shrinks, so no additional storage invariant is needed. The certificate retains the output, ordinary private state and unused suffix; only the separate distribution law forgets that suffix.

Main results

• Cslib.Probability.IsOraclePPTOn.run_interpret_withSampleList: arbitrary encoded callers and saved values, with all sample consumption and storage charged.
• Cslib.Probability.IsOraclePPT.run_interpret_withSampleList: security-parameter specialization.

References

Adapted from Computability/Probabilistic/Presample.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the common stateful substitution theorem.

theorem Cslib.Probability.IsOraclePPTOn.run_interpret_withSampleList {Operation α β Caller State Value : Type} [DecidableEq Operation] [Finite Operation] {source : α ↪ List Bool} {input : Caller ↪ List Bool} {output : β ↪ List Bool} {stateEncoding : State ↪ List Bool} {valueEncoding : Value ↪ List Bool} {program : α → WordOracleComp Operation β} {oracle : Caller → Value → Operation × List Bool → State → ProbComp (List Bool × State)} {prepare : Caller → α} {initial : Caller → State} {values : Caller → List Value} {resources : Caller → List Bool → ℕ} (hprogram : IsOraclePPTOn source output program) (fallback : Value) (hprepare : Turing.MultiTapeTM.ComputableTidilyInPolyTime prepare input source) (horacle : IsPPTOn (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair input valueEncoding) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encFinite Operation) Turing.MultiTapeTM.encBits) stateEncoding)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits stateEncoding) fun (pair : (Caller × Value) × (Operation × List Bool) × State) => oracle pair.1.1 pair.1.2 pair.2.1 pair.2.2) (hinitial : Turing.MultiTapeTM.ComputableTidilyInPolyTime initial input stateEncoding) (hvalues : Turing.MultiTapeTM.ComputableTidilyInPolyTime values input (Turing.MultiTapeTM.encList valueEncoding)) (invariant : Caller → State → Prop) (hinit : ∀ (a : Caller), invariant a (initial a)) (hresources : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : Caller × List Bool) => resources pair.1 pair.2) (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encUnary) (hpreserve : ∀ (a : Caller) (value : Value) (request : Operation × List Bool) (state : State), invariant a state → ∀ result ∈ (oracle a value request state).eval.support, invariant a result.2 ∧ result.1.length ≤ resources a request.2 ∧ (stateEncoding result.2).length ≤ (stateEncoding state).length + resources a request.2) : IsPPTOn input (Turing.MultiTapeTM.encPair output (Turing.MultiTapeTM.encPair stateEncoding (Turing.MultiTapeTM.encList valueEncoding))) fun (a : Caller) => (OracleComp.interpret (ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (ProbComp.unifFin n)) (OracleComp.withSampleList fallback (oracle a))) (program (prepare a))).run (initial a, values a)

Supply saved samples to a closed external handler. Bounds hold for every supplied value, including the fallback on an exhausted list. The certificate retains the complete final state.

theorem Cslib.Probability.IsOraclePPT.run_interpret_withSampleList {Operation β Caller State Value : Type} [DecidableEq Operation] [Finite Operation] {input : Caller ↪ List Bool} {output : β ↪ List Bool} {stateEncoding : State ↪ List Bool} {valueEncoding : Value ↪ List Bool} {program : ℕ → List Bool → WordOracleComp Operation β} {oracle : Caller → Value → Operation × List Bool → State → ProbComp (List Bool × State)} {prepare : Caller → ℕ × List Bool} {initial : Caller → State} {values : Caller → List Value} {resources : Caller → List Bool → ℕ} (hprogram : IsOraclePPT output program) (fallback : Value) (hprepare : Turing.MultiTapeTM.ComputableTidilyInPolyTime prepare input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits)) (horacle : IsPPTOn (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair input valueEncoding) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encFinite Operation) Turing.MultiTapeTM.encBits) stateEncoding)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits stateEncoding) fun (pair : (Caller × Value) × (Operation × List Bool) × State) => oracle pair.1.1 pair.1.2 pair.2.1 pair.2.2) (hinitial : Turing.MultiTapeTM.ComputableTidilyInPolyTime initial input stateEncoding) (hvalues : Turing.MultiTapeTM.ComputableTidilyInPolyTime values input (Turing.MultiTapeTM.encList valueEncoding)) (invariant : Caller → State → Prop) (hinit : ∀ (a : Caller), invariant a (initial a)) (hresources : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : Caller × List Bool) => resources pair.1 pair.2) (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encUnary) (hpreserve : ∀ (a : Caller) (value : Value) (request : Operation × List Bool) (state : State), invariant a state → ∀ result ∈ (oracle a value request state).eval.support, invariant a result.2 ∧ result.1.length ≤ resources a request.2 ∧ (stateEncoding result.2).length ≤ (stateEncoding state).length + resources a request.2) : IsPPTOn input (Turing.MultiTapeTM.encPair output (Turing.MultiTapeTM.encPair stateEncoding (Turing.MultiTapeTM.encList valueEncoding))) fun (a : Caller) => (OracleComp.interpret (ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (ProbComp.unifFin n)) (OracleComp.withSampleList fallback (oracle a))) (program (prepare a).1 (prepare a).2)).run (initial a, values a)

Security-parameter specialization of saved-sample substitution, retaining the complete ordinary state and unused suffix under the same local resource contract.