Rational hitting lists: dense records

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/DenseRecords.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

def Complexity.RationalHitting.StackLanguage.codeWord : List Bool → List Bool

Self-delimiting word records (distinct from the final output encoding).

Equations

• Complexity.RationalHitting.StackLanguage.codeWord [] = [true]
• Complexity.RationalHitting.StackLanguage.codeWord (b :: w) = false :: b :: Complexity.RationalHitting.StackLanguage.codeWord w

@[simp]

theorem Complexity.RationalHitting.StackLanguage.codeWord_length (w : List Bool) : (codeWord w).length = 2 * w.length + 1

def Complexity.RationalHitting.StackLanguage.pairWord (w : List Bool) : List Bool

Escape each data bit by prefixing it with a false marker.

Equations

• Complexity.RationalHitting.StackLanguage.pairWord w = List.flatMap (fun (b : Bool) => [false, b]) w

@[simp]

theorem Complexity.RationalHitting.StackLanguage.pairWord_nil : pairWord [] = []

@[simp]

theorem Complexity.RationalHitting.StackLanguage.pairWord_cons (b : Bool) (w : List Bool) : pairWord (b :: w) = false :: b :: pairWord w

@[simp]

theorem Complexity.RationalHitting.StackLanguage.pairWord_append (u v : List Bool) : pairWord (u ++ v) = pairWord u ++ pairWord v

theorem Complexity.RationalHitting.StackLanguage.codeWord_pair (w : List Bool) : codeWord w = pairWord w ++ [true]

def Complexity.RationalHitting.StackLanguage.packLoop (a b : Fin 3) : Program (Fin 3)

Move and escape the bits of one record.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.RationalHitting.StackLanguage.eval_packLoop (a b : Fin 3) (hab : a ≠ b) (s : Store (Fin 3)) : Eval (packLoop a b) s (Function.update (Function.update s a []) b (pairWord (s a).reverse ++ s b)) (4 * (s a).length + 1)

def Complexity.RationalHitting.StackLanguage.packRecord : Program (Fin 3)

Consume a binary word, prepending one encoded reversed record.

Equations

• Complexity.RationalHitting.StackLanguage.packRecord = (Complexity.RationalHitting.StackLanguage.Program.push 1 true).seq (Complexity.RationalHitting.StackLanguage.packLoop 0 1)

theorem Complexity.RationalHitting.StackLanguage.eval_packRecord (s : Store (Fin 3)) : Eval packRecord s (Function.update (Function.update s 0 []) 1 (codeWord (s 0).reverse ++ s 1)) (4 * (s 0).length + 3)

def Complexity.RationalHitting.StackLanguage.unpackBody : Program (Fin 3)

Read one escaped data bit or consume the record terminator.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.RationalHitting.StackLanguage.eval_unpackLoop (w tail : List Bool) (s : Store (Fin 3)) (h0 : s 0 = codeWord w ++ tail) (h2 : s 2 = [true]) : Eval (Program.loop 2 unpackBody) s (Function.update (Function.update (Function.update s 0 tail) 1 (w.reverse ++ s 1)) 2 []) (5 * w.length + 6)

def Complexity.RationalHitting.StackLanguage.unpackRecord : Program (Fin 3)

Remove one self-delimiting record; produce its reversed binary word.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.RationalHitting.StackLanguage.eval_unpackRecord (w tail : List Bool) (s : Store (Fin 3)) (h0 : s 0 = codeWord w ++ tail) (h2 : s 2 = []) : Eval unpackRecord s (Function.update (Function.update (Function.update s 0 tail) 1 (w.reverse ++ s 1)) 2 []) (5 * w.length + 8)

def Complexity.RationalHitting.StackLanguage.codeArray (ws : List (List Bool)) : List Bool

Dense serialized arrays of variable-width binary records.

Equations

• Complexity.RationalHitting.StackLanguage.codeArray ws = List.flatMap Complexity.RationalHitting.StackLanguage.codeWord ws

@[simp]

theorem Complexity.RationalHitting.StackLanguage.codeArray_nil : codeArray [] = []

@[simp]

theorem Complexity.RationalHitting.StackLanguage.codeArray_cons (w : List Bool) (ws : List (List Bool)) : codeArray (w :: ws) = codeWord w ++ codeArray ws

@[simp]

theorem Complexity.RationalHitting.StackLanguage.codeArray_append (u v : List (List Bool)) : codeArray (u ++ v) = codeArray u ++ codeArray v

theorem Complexity.RationalHitting.StackLanguage.codeArray_nonempty (w : List Bool) (ws : List (List Bool)) : codeArray (w :: ws) ≠ []

def Complexity.RationalHitting.StackLanguage.unpackMove : Fin 3 ↪ Fin 4

Register embedding for the unpacking stage of a record move.

Equations

• Complexity.RationalHitting.StackLanguage.unpackMove = { toFun := ![0, 2, 3], inj' := Complexity.RationalHitting.StackLanguage.unpackMove._proof_1 }

def Complexity.RationalHitting.StackLanguage.packMove : Fin 3 ↪ Fin 4

Register embedding for the packing stage of a record move.

Equations

• Complexity.RationalHitting.StackLanguage.packMove = { toFun := ![2, 1, 3], inj' := Complexity.RationalHitting.StackLanguage.packMove._proof_1 }

def Complexity.RationalHitting.StackLanguage.recordMove : Program (Fin 4)

Move one delimited record between stacks.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.RationalHitting.StackLanguage.eval_recordMove (w tail : List Bool) (s : Store (Fin 4)) (h0 : s 0 = codeWord w ++ tail) (h2 : s 2 = []) (h3 : s 3 = []) : Eval recordMove s (Function.update (Function.update s 0 tail) 1 (codeWord w ++ s 1)) (9 * w.length + 12)

theorem Complexity.RationalHitting.StackLanguage.eval_recordMove_rename {K : Type} [DecidableEq K] (f : Fin 4 ↪ K) (w tail : List Bool) (s : Store K) (h0 : s (f 0) = codeWord w ++ tail) (h2 : s (f 2) = []) (h3 : s (f 3) = []) : Eval (Program.rename (⇑f) recordMove) s (Function.update (Function.update s (f 0) tail) (f 1) (codeWord w ++ s (f 1))) (9 * w.length + 12)

def Complexity.RationalHitting.StackLanguage.arrayForward : Fin 4 ↪ Fin 8

Register embedding for moving records forward during a scan.

Equations

• Complexity.RationalHitting.StackLanguage.arrayForward = { toFun := ![0, 1, 2, 3], inj' := Complexity.RationalHitting.StackLanguage.arrayForward._proof_1 }

def Complexity.RationalHitting.StackLanguage.arrayBackward : Fin 4 ↪ Fin 8

Register embedding for restoring records after a scan.

Equations

• Complexity.RationalHitting.StackLanguage.arrayBackward = { toFun := ![1, 0, 2, 3], inj' := Complexity.RationalHitting.StackLanguage.arrayBackward._proof_1 }

def Complexity.RationalHitting.StackLanguage.scanBody : Program (Fin 8)

Move one record and decrement the unary scan counter.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RationalHitting.StackLanguage.scan : Program (Fin 8)

Scan the specified number of records using a unary counter.

Equations

• Complexity.RationalHitting.StackLanguage.scan = Complexity.RationalHitting.StackLanguage.Program.loop 4 Complexity.RationalHitting.StackLanguage.scanBody

def Complexity.RationalHitting.StackLanguage.scanCost (ws : List (List Bool)) : ℕ

Number of real finite-stack macrosteps for scanning a given prefix.

Equations

• Complexity.RationalHitting.StackLanguage.scanCost ws = (List.map (fun (w : List Bool) => 9 * w.length + 15) ws).sum + 1

theorem Complexity.RationalHitting.StackLanguage.eval_scan (pre : List (List Bool)) (tail : List Bool) (s : Store (Fin 8)) (h0 : s 0 = codeArray pre ++ tail) (h4 : s 4 = List.replicate pre.length true) (h2 : s 2 = []) (h3 : s 3 = []) : Eval scan s (Function.update (Function.update (Function.update s 0 tail) 1 (codeArray pre.reverse ++ s 1)) 4 []) (scanCost pre)

theorem Complexity.RationalHitting.StackLanguage.scanCost_bound (ws : List (List Bool)) : scanCost ws ≤ 15 * (codeArray ws).length + 1

def Complexity.RationalHitting.StackLanguage.restore : Program (Fin 8)

Restore all scanned records to the original stack.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RationalHitting.StackLanguage.restoreCost (ws : List (List Bool)) : ℕ

Stack-step count for restoring the given list of records.

Equations

• Complexity.RationalHitting.StackLanguage.restoreCost ws = (List.map (fun (w : List Bool) => 9 * w.length + 13) ws).sum + 1

theorem Complexity.RationalHitting.StackLanguage.eval_restore (ws : List (List Bool)) (s : Store (Fin 8)) (h1 : s 1 = codeArray ws) (h2 : s 2 = []) (h3 : s 3 = []) : Eval restore s (Function.update (Function.update s 1 []) 0 (codeArray ws.reverse ++ s 0)) (restoreCost ws)

theorem Complexity.RationalHitting.StackLanguage.restoreCost_bound (ws : List (List Bool)) : restoreCost ws ≤ 13 * (codeArray ws).length + 1

@[simp]

theorem Complexity.RationalHitting.StackLanguage.codeArray_reverse_length (ws : List (List Bool)) : (codeArray ws.reverse).length = (codeArray ws).length

def Complexity.RationalHitting.StackLanguage.peekUnpack : Fin 3 ↪ Fin 8

Register embedding for unpacking a record without consuming it permanently.

Equations

• Complexity.RationalHitting.StackLanguage.peekUnpack = { toFun := ![0, 2, 3], inj' := Complexity.RationalHitting.StackLanguage.peekUnpack._proof_1 }

def Complexity.RationalHitting.StackLanguage.peekPack : Fin 3 ↪ Fin 8

Register embedding for restoring a peeked record.

Equations

• Complexity.RationalHitting.StackLanguage.peekPack = { toFun := ![2, 0, 3], inj' := Complexity.RationalHitting.StackLanguage.peekPack._proof_1 }

def Complexity.RationalHitting.StackLanguage.peekRecord : Program (Fin 8)

Copy the next record while restoring its original representation.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.RationalHitting.StackLanguage.eval_peekRecord (w tail : List Bool) (s : Store (Fin 8)) (h0 : s 0 = codeWord w ++ tail) (h2 : s 2 = []) (h3 : s 3 = []) (h5 : s 5 = []) (h6 : s 6 = []) (h7 : s 7 = []) : Eval peekRecord s (Function.update s 5 w) (18 * w.length + 22)

def Complexity.RationalHitting.StackLanguage.arrayRead : Program (Fin 8)

Indexed read. Register 4 is a unary index; register 0 is a serialized array and is restored byte-for-byte. Register 5 receives the exact binary word.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.RationalHitting.StackLanguage.eval_arrayRead (pre post : List (List Bool)) (w : List Bool) (s : Store (Fin 8)) (h0 : s 0 = codeArray (pre ++ w :: post)) (h1 : s 1 = []) (h2 : s 2 = []) (h3 : s 3 = []) (h4 : s 4 = List.replicate pre.length true) (h5 : s 5 = []) (h6 : s 6 = []) (h7 : s 7 = []) : ∃ t ≤ 50 * (s 0).length + 30, Eval arrayRead s (Function.update (Function.update s 4 []) 5 w) t