Memoized oracle computations

An association-list cache in front of a strict oracle PPT computation is strict oracle PPT. On a cache hit the stored value is returned and the computation does not run, so it makes no external call; on a miss it runs once and its result is stored. The certificate charges comparing complete key encodings, the lookup and writing the returned cache.

The closed rule Cslib.Probability.IsPPTOn.memoize may run and discard its sampler on a hit. An oracle computation cannot be run speculatively: a stateful external oracle observes every call.

Main results

• Cslib.ProbOracleComp.mem_support_memoize: a possible result of a cached call is a hit or a possible result of the computation, stored at the front of the cache.
• Cslib.ProbOracleComp.memoize_call_size_le: a cached call preserves a value-size invariant and adds at most one encoded entry, for every external oracle.
• Cslib.Probability.IsOraclePPTOn.memoize: certify a memoized oracle computation by fun_prop.

References

Adapts Computability/Probabilistic/Memoize.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8 to oracle computations.

theorem Cslib.ProbOracleComp.mem_support_memoize {Query Key Value : Type} {spec : Query → Type} [BEq Key] (compute : Key → ProbOracleComp spec Value) (key : Key) (cache : List (Key × Value)) {result : Value × List (Key × Value)} (hresult : result ∈ (memoize compute key cache).support) : List.lookup key cache = some result.1 ∧ result.2 = cache ∨ List.lookup key cache = none ∧ result.1 ∈ (compute key).support ∧ result.2 = (key, result.1) :: cache

A possible result of a cached call is either a hit, leaving the cache unchanged, or a possible result of the computation, stored at the front of the cache.

theorem Cslib.ProbOracleComp.memoize_call_size_le {Query Key Value : Type} {spec : Query → Type} [BEq Key] [LawfulBEq Key] (keyEncoding : Key ↪ List Bool) (valueEncoding : Value ↪ List Bool) (compute : Key → ProbOracleComp spec Value) (key : Key) (cache : List (Key × Value)) (maxValue : ℕ) (hcache : ∀ entry ∈ cache, (valueEncoding entry.2).length ≤ maxValue) (hvalues : ∀ value ∈ (compute key).support, (valueEncoding value).length ≤ maxValue) {result : Value × List (Key × Value)} (hresult : result ∈ (memoize compute 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 bound on the encoded values of all entries, returns a value within that bound and adds at most one encoded entry, for every possible result under every external oracle. The growth charges the complete key and value and both layers of framing.

theorem Cslib.Probability.IsOraclePPTOn.memoize {Operation α Key Value : Type} [DecidableEq Operation] [Finite Operation] [BEq Key] [LawfulBEq Key] [Nonempty Value] {input : α ↪ List Bool} {keyEncoding : Key ↪ List Bool} {valueEncoding : Value ↪ List Bool} {compute : α → Key → WordOracleComp Operation Value} {query : α → Key} {cache : α → List (Key × Value)} (hcompute : IsOraclePPTOn 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))) : IsOraclePPTOn 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 strict oracle PPT computation's results in an ordinary list. On a hit the computation does not run and makes no external call; on a miss it runs once. Comparing complete key encodings, the lookup and the complete returned cache are charged. Repeated keys use their first cached occurrence. The inhabitant of Value is never returned.