Native Turing-machine certificates for sparse memory

The association list is encoded as a list of encoded address/value pairs. Equality, first-match search and filtering are implemented by the existing native multitape-machine calculus. No memory operation is an oracle. Bounds depend on encoded address lengths, rather than allocating space up to the numeric address. The cost functions are asymptotic bound expressions for ComputableTidilyInO, not exact native step counts: one finite machine and a constant factor work for all inputs, for each fixed choice of address and value encodings.

Main definitions

• SparseMemory.encoding: the binary encoding of a finite sparse store.
• SparseMemory.scanTime, SparseMemory.scanSpace: parameterized scan bounds.

Main results

• SparseMemory.read_inO, insert_inO: native TM read/write implementations with parameterized time and space, including argument extraction and a uniform read default.
• SparseMemory.length_encoding_le: stored-cell and word-length bound on the encoding.
• SparseMemory.read_inO_cube, insert_inO_cube: cubic time and linear workspace in full encoded input length; these conservative bounds are not optimality claims.
• SparseMemory.read_polytime, insert_polytime: registered polynomial-time corollaries.

References

Uses Mathlib's association lists and Christian Reitwiessner's encoded native multitape-machine calculus (ComputableTidilyInO.eq, findWith, and filterWith).

def Cslib.GenericRAM.SparseMemory.encoding {Address Value : Type} (encA : Address ↪ List Bool) (encV : Value ↪ List Bool) : SparseMemory Address Value ↪ List Bool

Encode the distinct bindings using the existing framed pair and list encodings.

@[simp]

theorem Cslib.GenericRAM.SparseMemory.encoding_apply {Address Value : Type} (encA : Address ↪ List Bool) (encV : Value ↪ List Bool) (s : SparseMemory Address Value) : (encoding encA encV) s = (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encA encV)) s.entries

def Cslib.GenericRAM.SparseMemory.queryEncoding {Address Value : Type} (encA : Address ↪ List Bool) (encV : Value ↪ List Bool) : Address × SparseMemory Address Value ↪ List Bool

Encode a queried address and the store.

def Cslib.GenericRAM.SparseMemory.compareTime {Address Value : Type} (encA : Address ↪ List Bool) (encV : Value ↪ List Bool) (q : Address × Address × Value) : ℕ

The cost expression of the certified address comparison, including argument extraction.

def Cslib.GenericRAM.SparseMemory.compareSpace {Address Value : Type} (encA : Address ↪ List Bool) (encV : Value ↪ List Bool) (q : Address × Address × Value) : ℕ

Workspace for the certified address comparison, including argument extraction.

def Cslib.GenericRAM.SparseMemory.scanTime {Address Value : Type} (encA : Address ↪ List Bool) (encV : Value ↪ List Bool) (q : Address × SparseMemory Address Value) : ℕ

First-match search time: encoded input overhead plus one bounded scan round per binding.

def Cslib.GenericRAM.SparseMemory.scanSpace {Address Value : Type} (encA : Address ↪ List Bool) (encV : Value ↪ List Bool) (q : Address × SparseMemory Address Value) : ℕ

First-match search workspace: input, store and the largest comparison workspace.

def Cslib.GenericRAM.SparseMemory.maxKeyLength {Address Value : Type} (encA : Address ↪ List Bool) (s : SparseMemory Address Value) : ℕ

Maximum encoded address length among stored cells, zero for the empty store.

def Cslib.GenericRAM.SparseMemory.maxValueLength {Address Value : Type} (encV : Value ↪ List Bool) (s : SparseMemory Address Value) : ℕ

Maximum encoded value length among stored cells, zero for the empty store.

theorem Cslib.GenericRAM.SparseMemory.length_encoding_le {Address Value : Type} (encA : Address ↪ List Bool) (encV : Value ↪ List Bool) (s : SparseMemory Address Value) : ((encoding encA encV) s).length ≤ s.entries.length * (4 * maxKeyLength encA s + 2 * maxValueLength encV s + 3)

The encoded store depends on the number and encoded sizes of stored cells.

theorem Cslib.GenericRAM.SparseMemory.scanTime_le {Address Value : Type} (encA : Address ↪ List Bool) (encV : Value ↪ List Bool) (q : Address × SparseMemory Address Value) : scanTime encA encV q ≤ 3 * ((queryEncoding encA encV) q).length + (q.2.entries.length + 1) * ((encA q.1).length + ((encoding encA encV) q.2).length + 2 * (2 * (encA q.1).length + 2 * maxKeyLength encA q.2 + maxValueLength encV q.2 + 2) + ((encA q.1).length + 1) * ((encA q.1).length + maxKeyLength encA q.2 + 1))

A bound using entry count, encoded input length, and maximum key/value lengths.

theorem Cslib.GenericRAM.SparseMemory.scanSpace_le {Address Value : Type} (encA : Address ↪ List Bool) (encV : Value ↪ List Bool) (q : Address × SparseMemory Address Value) : scanSpace encA encV q ≤ 3 * ((queryEncoding encA encV) q).length + (encA q.1).length + ((encoding encA encV) q.2).length + 2 * (2 * (encA q.1).length + 2 * maxKeyLength encA q.2 + maxValueLength encV q.2 + 2) + (2 * (encA q.1).length + maxKeyLength encA q.2 + 1)

Scan workspace is linear in the retained encoding and the largest encoded words.

theorem Cslib.GenericRAM.SparseMemory.maxKeyLength_le_encoding {Address Value : Type} (encA : Address ↪ List Bool) (encV : Value ↪ List Bool) (s : SparseMemory Address Value) : maxKeyLength encA s ≤ ((encoding encA encV) s).length

Every stored address is bounded by the total encoded store.

theorem Cslib.GenericRAM.SparseMemory.maxValueLength_le_encoding {Address Value : Type} (encA : Address ↪ List Bool) (encV : Value ↪ List Bool) (s : SparseMemory Address Value) : maxValueLength encV s ≤ ((encoding encA encV) s).length

Every stored value is bounded by the total encoded store.

theorem Cslib.GenericRAM.SparseMemory.scanTime_le_cube {Address Value : Type} (encA : Address ↪ List Bool) (encV : Value ↪ List Bool) (q : Address × SparseMemory Address Value) : scanTime encA encV q ≤ 30 * (((queryEncoding encA encV) q).length + 1) ^ 3

In particular, the scan's parameterized time bound is cubic in its encoded input length.

theorem Cslib.GenericRAM.SparseMemory.scanSpace_le_linear {Address Value : Type} (encA : Address ↪ List Bool) (encV : Value ↪ List Bool) (q : Address × SparseMemory Address Value) : scanSpace encA encV q ≤ 30 * (((queryEncoding encA encV) q).length + 1)

The scan's workspace bound is linear in its encoded input length.

theorem Cslib.GenericRAM.SparseMemory.find_inO {Address Value : Type} (encA : Address ↪ List Bool) (encV : Value ↪ List Bool) [DecidableEq Address] : Turing.MultiTapeTM.ComputableTidilyInO (fun (q : Address × SparseMemory Address Value) => List.find? (fun (e : Address × Value) => decide (q.1 = e.1)) q.2.entries) (queryEncoding encA encV) (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encPair encA encV)) (scanTime encA encV) (scanSpace encA encV)

A native multitape machine searches the finite store, with parameterized time and space.

theorem Cslib.GenericRAM.SparseMemory.erase_entries_inO {Address Value : Type} (encA : Address ↪ List Bool) (encV : Value ↪ List Bool) [DecidableEq Address] : Turing.MultiTapeTM.ComputableTidilyInO (fun (q : Address × SparseMemory Address Value) => List.filter (fun (e : Address × Value) => decide (q.1 ≠ e.1)) q.2.entries) (queryEncoding encA encV) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encA encV)) (scanTime encA encV) (scanSpace encA encV)

Filtering implements erasure using the same parameterized scan bounds.

def Cslib.GenericRAM.SparseMemory.writeEncoding {Address Value : Type} (encA : Address ↪ List Bool) (encV : Value ↪ List Bool) : (Address × Value) × SparseMemory Address Value ↪ List Bool

Binary input convention for a write: a new binding followed by the finite store.

def Cslib.GenericRAM.SparseMemory.writeTime {Address Value : Type} (encA : Address ↪ List Bool) (encV : Value ↪ List Bool) (q : (Address × Value) × SparseMemory Address Value) : ℕ

Charged write time, including preparing the scan and the new binding.

def Cslib.GenericRAM.SparseMemory.writeSpace {Address Value : Type} (encA : Address ↪ List Bool) (encV : Value ↪ List Bool) (q : (Address × Value) × SparseMemory Address Value) : ℕ

Charged write workspace.

theorem Cslib.GenericRAM.SparseMemory.insert_inO {Address Value : Type} (encA : Address ↪ List Bool) (encV : Value ↪ List Bool) [DecidableEq Address] : Turing.MultiTapeTM.ComputableTidilyInO (fun (q : (Address × Value) × SparseMemory Address Value) => AList.insert q.1.1 q.1.2 q.2) (writeEncoding encA encV) (encoding encA encV) (writeTime encA encV) (writeSpace encA encV)

Native TM implementation of insertion/replacement, including all argument preparation.

def Cslib.GenericRAM.SparseMemory.readEncoding {Address Value : Type} (encA : Address ↪ List Bool) (encV : Value ↪ List Bool) : (Address × SparseMemory Address Value) × Value ↪ List Bool

A read input supplies both the queried store and its default value.

def Cslib.GenericRAM.SparseMemory.readTime {Address Value : Type} (encA : Address ↪ List Bool) (encV : Value ↪ List Bool) (q : (Address × SparseMemory Address Value) × Value) : ℕ

Read time, including extraction of the query and the input-supplied default.

def Cslib.GenericRAM.SparseMemory.readSpace {Address Value : Type} (encA : Address ↪ List Bool) (encV : Value ↪ List Bool) (q : (Address × SparseMemory Address Value) × Value) : ℕ

Read workspace, including the input-supplied default.

theorem Cslib.GenericRAM.SparseMemory.read_inO {Address Value : Type} (encA : Address ↪ List Bool) (encV : Value ↪ List Bool) [DecidableEq Address] : Turing.MultiTapeTM.ComputableTidilyInO (fun (q : (Address × SparseMemory Address Value) × Value) => read q.2 q.1.1 q.1.2) (readEncoding encA encV) encV (readTime encA encV) (readSpace encA encV)

Native TM implementation of total memory reads, uniform also in the default value.

theorem Cslib.GenericRAM.SparseMemory.insert_inO_cube {Address Value : Type} (encA : Address ↪ List Bool) (encV : Value ↪ List Bool) [DecidableEq Address] : Turing.MultiTapeTM.ComputableTidilyInO (fun (q : (Address × Value) × SparseMemory Address Value) => AList.insert q.1.1 q.1.2 q.2) (writeEncoding encA encV) (encoding encA encV) (fun (q : (Address × Value) × SparseMemory Address Value) => (((writeEncoding encA encV) q).length + 1) ^ 3) fun (q : (Address × Value) × SparseMemory Address Value) => ((writeEncoding encA encV) q).length

A cubic-time, linear-space specialization of the parameterized write certificate.

theorem Cslib.GenericRAM.SparseMemory.read_inO_cube {Address Value : Type} (encA : Address ↪ List Bool) (encV : Value ↪ List Bool) [DecidableEq Address] : Turing.MultiTapeTM.ComputableTidilyInO (fun (q : (Address × SparseMemory Address Value) × Value) => read q.2 q.1.1 q.1.2) (readEncoding encA encV) encV (fun (q : (Address × SparseMemory Address Value) × Value) => (((readEncoding encA encV) q).length + 1) ^ 3) fun (q : (Address × SparseMemory Address Value) × Value) => ((readEncoding encA encV) q).length

A cubic-time, linear-space specialization of the parameterized read certificate.

theorem Cslib.GenericRAM.SparseMemory.insert_polytime {Address Value : Type} (encA : Address ↪ List Bool) (encV : Value ↪ List Bool) [DecidableEq Address] : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (q : (Address × Value) × SparseMemory Address Value) => AList.insert q.1.1 q.1.2 q.2) (writeEncoding encA encV) (encoding encA encV)

Polynomial-time writes are a corollary of the native parameterized certificate.

theorem Cslib.GenericRAM.SparseMemory.read_polytime {Address Value : Type} (encA : Address ↪ List Bool) (encV : Value ↪ List Bool) [DecidableEq Address] : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (q : (Address × SparseMemory Address Value) × Value) => read q.2 q.1.1 q.1.2) (readEncoding encA encV) encV

Polynomial-time reads are uniform in the queried address, store, and default value.

theorem Cslib.GenericRAM.SparseMemory.maxKeyLength_insert_le {Address Value : Type} (encA : Address ↪ List Bool) [DecidableEq Address] (a : Address) (v : Value) (s : SparseMemory Address Value) : maxKeyLength encA (AList.insert a v s) ≤ max (encA a).length (maxKeyLength encA s)

Writing preserves maximum key length up to the newly supplied address.

theorem Cslib.GenericRAM.SparseMemory.maxValueLength_insert_le {Address Value : Type} (encV : Value ↪ List Bool) [DecidableEq Address] (a : Address) (v : Value) (s : SparseMemory Address Value) : maxValueLength encV (AList.insert a v s) ≤ max (encV v).length (maxValueLength encV s)

Writing preserves maximum value length up to the newly supplied value.