Efficient memoized sampling

An association-list cache preserves the efficiency of a closed probabilistic sampler. The certificate charges for comparing complete key encodings, looking up an answer and writing the returned cache. Queries, samplers and initial caches may capture the input.

The proof uses a sample as a fallback for optional lookup, so neither keys nor values need an inhabitant chosen in advance. Its realizing machine may run and discard the sampler on a hit; the source program still has exactly the joint result/cache law of memoize.

Main results

• Cslib.Probability.IsPPTOn.memoize: certify a memoized sampler through fun_prop.
• Cslib.Probability.memoize_cache_growth_le: bound new storage independently of existing entries.
• Cslib.Probability.memoize_call_size_le: preserve reply sizes and bound local storage growth.
• Cslib.Probability.memoize_cache_size_le: bound the encoded cache using external query budgets.

References

Adapted from Computability/Probabilistic/Memoize.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, reusing the tidy calculus and captured-input rules.

theorem Cslib.Probability.IsPPTOn.memoize {α Key Value : Type} [BEq Key] [LawfulBEq Key] {input : α ↪ List Bool} {keyEncoding : Key ↪ List Bool} {valueEncoding : Value ↪ List Bool} {compute : α → Key → ProbComp Value} {query : α → Key} {cache : α → List (Key × Value)} (hcompute : IsPPTOn input valueEncoding fun (a : α) => compute a (query a)) (hquery : Turing.MultiTapeTM.ComputableTidilyInPolyTime query input keyEncoding) (hcache : Turing.MultiTapeTM.ComputableTidilyInPolyTime cache input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair keyEncoding valueEncoding))) : IsPPTOn input (Turing.MultiTapeTM.encPair valueEncoding (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair keyEncoding valueEncoding))) fun (a : α) => Cslib.memoize (compute a) (query a) (cache a)

Cache a certified sampler's results using an ordinary list. Runtime query data, captured inputs and the complete returned cache are included in the certificate. No default key or value is required, and repeated keys use their first cached occurrence.

theorem Cslib.Probability.memoize_cache_growth_le {Key Value : Type} [BEq Key] (keyEncoding : Key ↪ List Bool) (valueEncoding : Value ↪ List Bool) (distribution : Key → PMF Value) (key : Key) (cache : List (Key × Value)) (maxValue : ℕ) (hvalues : ∀ value ∈ (distribution key).support, (valueEncoding value).length ≤ maxValue) (result : Value × List (Key × Value)) (hresult : result ∈ (memoize distribution key cache).support) : ((Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair keyEncoding valueEncoding)) result.2).length ≤ ((Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair keyEncoding valueEncoding)) cache).length + 4 * (keyEncoding key).length + 2 * maxValue + 3

A cached call adds at most one encoded entry, charging the complete key and value and both layers of framing. Existing entries need no size invariant: a cache hit preserves the cache.

theorem Cslib.Probability.memoize_call_size_le {Key Value : Type} [BEq Key] [LawfulBEq Key] (keyEncoding : Key ↪ List Bool) (valueEncoding : Value ↪ List Bool) (distribution : Key → PMF Value) (key : Key) (cache : List (Key × Value)) (maxValue : ℕ) (hcache : ∀ entry ∈ cache, (valueEncoding entry.2).length ≤ maxValue) (hvalues : ∀ value ∈ (distribution key).support, (valueEncoding value).length ≤ maxValue) (result : Value × List (Key × Value)) (hresult : result ∈ (memoize distribution key cache).support) : (valueEncoding result.1).length ≤ maxValue ∧ (∀ entry ∈ result.2, (valueEncoding entry.2).length ≤ maxValue) ∧ ((Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair keyEncoding valueEncoding)) result.2).length ≤ ((Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair keyEncoding valueEncoding)) cache).length + 4 * (keyEncoding key).length + 2 * maxValue + 3

A cached call preserves a reply-size invariant and adds at most one encoded entry. The bound charges the complete key and value, including both layers of framing.

theorem Cslib.Probability.memoize_cache_size_le {α Key Value : Type} [BEq Key] (keyEncoding : Key ↪ List Bool) (valueEncoding : Value ↪ List Bool) (distribution : Key → PMF Value) (program : ProbOracleComp (fun (x : Key) => Value) α) (calls maxKey maxValue : ℕ) (hcalls : program.IsQueryBounded calls) (hkeys : ProbOracleComp.QueriesSatisfy (fun (key : Key) => (keyEncoding key).length ≤ maxKey) program) (hvalues : ∀ (key : Key), (keyEncoding key).length ≤ maxKey → ∀ value ∈ (distribution key).support, (valueEncoding value).length ≤ maxValue) (cache cache' : List (Key × Value)) (hcache : ∀ entry ∈ cache, (keyEncoding entry.1).length ≤ maxKey ∧ (valueEncoding entry.2).length ≤ maxValue) (result : α) (h : (result, cache') ∈ ((OracleComp.interpret (ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) (memoize distribution)) program).run cache).support) : ((Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair keyEncoding valueEncoding)) cache').length ≤ (cache.length + calls) * (4 * maxKey + 2 * maxValue + 3)

Bounds on external calls, encoded keys and replies bound the complete cache of a randomized client. Preassigned entries are included, as are both pair and list framing costs.