ROM Collision Infrastructure

Collision predicates on QueryLog and QueryCache, together with structural lemmas relating log entries and cache entries when running loggingOracle inside cachingOracle.

Main declarations

• OracleComp.LogHasCollision: two log entries at distinct positions with distinct inputs but HEq-equal outputs.
• OracleComp.CacheHasCollision: two distinct cache inputs map to the same output.
• OracleComp.cache_lookup_eq_of_noCollision: in a collision-free cache, a value determines at most one query input.
• OracleComp.log_entry_in_cache_and_mono: every log entry ends up in the cache, and the cache is monotone.
• OracleComp.cache_entry_in_log_or_initial: every new cache entry has a corresponding log entry.

Collision Predicates

def OracleComp.LogHasCollision {ι : Type} {spec : OracleSpec ι} (log : spec.QueryLog) : Prop

A query log has a collision: two entries at distinct positions with distinct inputs but HEq-equal outputs.

def OracleComp.CacheHasCollision {ι : Type} {spec : OracleSpec ι} (cache : spec.QueryCache) : Prop

A cache has a collision: two distinct inputs map to the same output.

theorem OracleComp.cache_lookup_eq_of_noCollision {ι : Type} {spec : OracleSpec ι} {cache : spec.QueryCache} {t₀ t₁ : spec.Domain} {v : spec.Range t₀} (hno : ¬CacheHasCollision cache) (h₀ : cache t₀ = some v) (h₁ : ∃ (v' : spec.Range t₁), cache t₁ = some v' ∧ v' ≍ v) : t₀ = t₁

In a collision-free cache, a value determines at most one query input.

Log entries are cached after logging inside caching

theorem OracleComp.log_entry_in_cache_and_mono {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} {α : Type} (oa : OracleComp spec α) (cache₀ : spec.QueryCache) (z : (α × spec.QueryLog) × spec.QueryCache) (hmem : z ∈ support ((simulateQ cachingOracle (simulateQ loggingOracle oa).run).run cache₀)) : (∀ entry ∈ z.1.2, z.2 entry.fst = some entry.snd) ∧ cache₀ ≤ z.2

When running loggingOracle inside cachingOracle, every log entry ends up in the cache.

We prove two properties simultaneously by induction:

1. Every log entry is in the final cache.
2. The initial cache is a subset of the final cache (monotonicity).

The proof works by induction on oa. The pure case is trivial (empty log). For query t >>= mx: the logging oracle decomposes as query t >>= fun u => map (prepend ⟨t,u⟩) ..., and cachingOracle caches the query result u at t. By the IH applied to mx u, all sub-log entries are in the final cache, and cache monotonicity ensures t ↦ u persists.

theorem OracleComp.cache_entry_in_log_or_initial {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} {α : Type} (oa : OracleComp spec α) (cache₀ : spec.QueryCache) (z : (α × spec.QueryLog) × spec.QueryCache) (hmem : z ∈ support ((simulateQ cachingOracle (simulateQ loggingOracle oa).run).run cache₀)) (t₀ : spec.Domain) (v : spec.Range t₀) : z.2 t₀ = some v → cache₀ t₀ = some v ∨ ∃ entry ∈ z.1.2, entry.fst = t₀ ∧ entry.snd ≍ v

Converse of log_entry_in_cache_and_mono: when running loggingOracle inside cachingOracle, every cache entry that was not in the initial cache has a corresponding log entry. Combined with log_entry_in_cache_and_mono, this shows that (starting from ∅) the cache entries and log entries have the same set of (input, output) pairs.

Proof by structural induction on oa, mirroring log_entry_in_cache_and_mono.