First slice: SQLite header, b-tree pages and records, read and proved (bar v2)

.github/workflows/bar.yml

@@ -0,0 +1,21 @@
+name: verified bar
+
+on:
+  push:
+  pull_request:
+  # Rerun when the spec reviewer approves, or an approval is dismissed.
+  pull_request_review:
+    types: [submitted, dismissed]
+
+jobs:
+  bar:
+    # pull-requests: read lets the check confirm the spec approval on GitHub.
+    permissions:
+      contents: read
+      pull-requests: read
+    # Both lines pin the same commit of Proven-Commons/mission: bar v2, as
+    # proposed in its pull request #2. Move both to a release tag once
+    # mission publishes one.
+    uses: Proven-Commons/mission/.github/workflows/verified-bar.yml@6ba85c27abaaf07905c9316aa96dc29f7b5847a2
+    with:
+      bar-ref: 6ba85c27abaaf07905c9316aa96dc29f7b5847a2

.gitignore

@@ -1 +1,2 @@
 .lake/
+__pycache__/

Main.lean

@@ -0,0 +1,201 @@
+/-
+  Command line front end.
+
+    sqlite dump FILE
+
+  reads a database file and prints, one per line:
+
+    header F1 ... F18         its header, as `header` gives it;
+    page N PAGE, page N FAIL  each whole page of the file in turn, N from
+                              1 to the file's length divided by the page
+                              size, as `page` gives it, or FAIL when it is
+                              not a b-tree page this reader accepts;
+    record N P ROWID VALUES,  after a page, for each cell whose payload is
+    record N P ROWID FAIL     all on its page and not empty, in the order
+                              of the cell pointers: P is the cell's
+                              pointer, ROWID its rowid (`-` on an index
+                              page), and VALUES the record the payload
+                              holds, as `record` gives it, or FAIL when it
+                              is not a record. An empty payload holds no
+                              record and gets no line.
+
+  It exits with 0. When the file does not start with a header this
+  reader accepts, it prints nothing on standard output and exits with
+  1; on wrong arguments or a file it cannot read, it prints nothing on
+  standard output and exits with 2.
+
+    sqlite serve
+
+  answers requests on standard input, one per line, for the
+  differential tests. Bytes are hex digits, two per byte, and an empty
+  field is written `-`. Numbers are decimal.
+
+    varint HEX       prints  OK, the value, the length and the hex of the
+                             rest, or FAIL                  (readVarint)
+    header HEX       prints  OK and the 18 fields, or FAIL  (readHeader)
+    page N HEX       prints  OK and page N of the file HEX, read with the
+                             file's own header, or FAIL     (readPage)
+    record HEX       prints  OK and the values, or FAIL     (readRecord)
+    local T U P      prints  OK and how many bytes of a payload of P
+                             bytes stay on a page of type T (2, 5, 10
+                             or 13) and usable size U       (localOf)
+
+  A page is written as its type, first freeblock, cell count, content
+  start, fragmented bytes and right-most pointer (`-` on a leaf page),
+  then `|`, then its cells, separated by spaces. A cell is written as
+  its pointer, left child, payload size, rowid, payload hex and
+  overflow page, separated by `/`, with `-` for a field the cell does
+  not have. A value is written `null`, `int:Z`, `real:BITS` (the 64
+  bits as a decimal number), `blob:HEX` or `text:HEX`.
+
+  A malformed request prints `error`: an unknown operation, the wrong
+  number of fields, hex digits that are not in pairs or not lower case,
+  or a number that is not decimal. A request line may end in LF or
+  CR LF.
+
+  Every answer comes from the proved functions in `Sqlite/`. The hex
+  coding, the output and the request handling here are covered by the
+  tests, not by a proof.
+-/
+
+import Sqlite
+
+open Sqlite Spec
+
+def hexValue (c : Char) : Option Nat :=
+  if '0' ≤ c ∧ c ≤ '9' then some (c.toNat - '0'.toNat)
+  else if 'a' ≤ c ∧ c ≤ 'f' then some (c.toNat - 'a'.toNat + 10)
+  else none
+
+/-- Bytes from hex digits in pairs. Tail recursive, so that long inputs
+    do not use the stack. -/
+def hexBytes (cs : List Char) (acc : Array UInt8) : Option (Array UInt8) :=
+  match cs with
+  | [] => some acc
+  | a :: b :: rest =>
+    match hexValue a, hexValue b with
+    | some hi, some lo => hexBytes rest (acc.push (hi * 16 + lo).toUInt8)
+    | _, _ => none
+  | [_] => none
+
+/-- The bytes a field gives: `-` for none, else hex digits in pairs. -/
+def fromHex (f : String) : Option (List UInt8) :=
+  if f = "-" then some [] else if f.isEmpty then none else (hexBytes f.toList #[]).map (·.toList)
+
+def hexDigit (n : Nat) : Char :=
+  if n < 10 then Char.ofNat ('0'.toNat + n) else Char.ofNat ('a'.toNat + n - 10)
+
+/-- A field for a list of bytes: `-` when it is empty. -/
+def toHex (bs : List UInt8) : String :=
+  if bs.isEmpty then "-"
+  else String.ofList (bs.flatMap fun b => [hexDigit (b.toNat / 16), hexDigit (b.toNat % 16)])
+
+/-- A decimal number, without sign or leading `+`. -/
+def decimal (s : String) : Option Nat :=
+  if !s.isEmpty && s.all Char.isDigit then s.toNat? else none
+
+def opt {α} [ToString α] : Option α → String
+  | some a => toString a
+  | none => "-"
+
+def showHeader (h : Header) : String :=
+  " ".intercalate (List.map toString [h.pageSize, h.writeVersion, h.readVersion, h.reserved,
+    h.changeCounter, h.databaseSize, h.freelistTrunk, h.freelistCount, h.schemaCookie,
+    h.schemaFormat, h.cacheSize, h.largestRoot, h.textEncoding, h.userVersion,
+    h.incrementalVacuum, h.applicationId, h.versionValidFor, h.sqliteVersion])
+
+def showCell (p : Nat) (c : Cell) : String :=
+  s!"{p}/{opt c.leftChild}/{opt c.payloadSize}/{opt c.rowid}/{toHex c.payload}/{opt c.overflow}"
+
+def showPage (pg : Page) : String :=
+  let ph := pg.header
+  let cells := (pg.pointers.zip pg.cells).map fun (p, c) => showCell p c
+  s!"{ph.type.code} {ph.firstFreeblock} {ph.cellCount} {ph.contentStart} {ph.fragmented} " ++
+    s!"{opt ph.rightmost} |" ++ String.join (cells.map (" " ++ ·))
+
+def showValue : Value → String
+  | .null => "null"
+  | .int z => s!"int:{z}"
+  | .real b => s!"real:{b}"
+  | .blob bs => s!"blob:{toHex bs}"
+  | .text bs => s!"text:{toHex bs}"
+
+def showValues (vs : List Value) : String := " ".intercalate (vs.map showValue)
+
+/-- The answer to one request line, or `none` when it is malformed. -/
+def request (line : String) : Option String :=
+  match line.splitOn " " with
+  | ["varint", h] => do
+    let b ← fromHex h
+    pure (match readVarint b with
+      | some (v, k, rest) => s!"OK {v} {k} {toHex rest}"
+      | none => "FAIL")
+  | ["header", h] => do
+    let b ← fromHex h
+    pure (match readHeader b with
+      | some hd => s!"OK {showHeader hd}"
+      | none => "FAIL")
+  | ["page", n, h] => do
+    let n ← decimal n
+    let b ← fromHex h
+    pure (match readHeader b >>= fun hd => readPage hd b n with
+      | some pg => s!"OK {showPage pg}"
+      | none => "FAIL")
+  | ["record", h] => do
+    let b ← fromHex h
+    pure (match readRecord b with
+      | some vs => s!"OK {showValues vs}"
+      | none => "FAIL")
+  | ["local", t, u, p] => do
+    let t ← (decimal t).bind pageType?
+    let u ← decimal u
+    let p ← decimal p
+    pure s!"OK {localOf t u p}"
+  | _ => none
+
+/-- A request line without its line ending, LF or CR LF. -/
+def chomp (line : String) : String :=
+  let cs := line.toList
+  if cs.getLast? = some '\n' then
+    let cs := cs.dropLast
+    String.ofList (if cs.getLast? = some '\r' then cs.dropLast else cs)
+  else line
+
+def serve : IO Unit := do
+  let stdin ← IO.getStdin
+  let stdout ← IO.getStdout
+  repeat
+    let line ← stdin.getLine
+    if line.isEmpty then break
+    stdout.putStrLn ((request (chomp line)).getD "error")
+    stdout.flush
+
+/-- The header, then each page and the records of its cells. -/
+def dump (file : List UInt8) : IO UInt32 := do
+  match readHeader file with
+  | none => IO.eprintln "not a database header this reader accepts"; return 1
+  | some h =>
+    IO.println s!"header {showHeader h}"
+    for i in [0:file.length / h.pageSize] do
+      let n := i + 1
+      match readPage h file n with
+      | none => IO.println s!"page {n} FAIL"
+      | some pg =>
+        IO.println s!"page {n} {showPage pg}"
+        for (p, c) in pg.pointers.zip pg.cells do
+          if c.overflow.isNone && !c.payload.isEmpty then
+            match readRecord c.payload with
+            | some vs => IO.println s!"record {n} {p} {opt c.rowid} {showValues vs}"
+            | none => IO.println s!"record {n} {p} {opt c.rowid} FAIL"
+    return 0
+
+def usage : String := "usage: sqlite dump FILE\n       sqlite serve"
+
+def main (args : List String) : IO UInt32 := do
+  match args with
+  | ["dump", path] =>
+    match ← (IO.FS.readBinFile path).toBaseIO with
+    | .error e => IO.eprintln s!"cannot read {path}: {e}"; return 2
+    | .ok bytes => dump bytes.toList
+  | ["serve"] => serve; return 0
+  | _ => IO.eprintln usage; return 2

Proofs.lean

@@ -0,0 +1,6 @@
+import Proofs.Bytes
+import Proofs.Varint
+import Proofs.Header
+import Proofs.Record
+import Proofs.Page
+import Proofs.Main

Proofs/Bytes.lean

@@ -0,0 +1,144 @@
+import Sqlite
+
+/-!
+  Fixed-width fields: `take?`, big-endian integers, and `readBE`.
+-/
+
+namespace SqliteProofs
+
+open Spec Sqlite
+
+theorem take?_eq (w : Nat) (b c r : List UInt8) :
+    take? w b = some (c, r) ↔ c.length = w ∧ b = c ++ r := by
+  unfold take?
+  dsimp only
+  constructor
+  · intro h
+    split at h
+    · rename_i hl
+      simp only [Option.some.injEq, Prod.mk.injEq] at h
+      obtain ⟨rfl, rfl⟩ := h
+      exact ⟨hl, (List.take_append_drop w b).symm⟩
+    · exact absurd h (by simp)
+  · rintro ⟨hl, rfl⟩
+    subst hl
+    simp
+
+theorem take?_append (c r : List UInt8) : take? c.length (c ++ r) = some (c, r) :=
+  (take?_eq _ _ _ _).mpr ⟨rfl, rfl⟩
+
+theorem bigEndian_eq (bs : List UInt8) : bigEndian bs = beNat bs := rfl
+
+theorem beBytes_length (w n : Nat) : (beBytes w n).length = w := by
+  simp [beBytes]
+
+theorem foldl_be (acc : Nat) (bs : List UInt8) :
+    bs.foldl (fun n b => n * 256 + b.toNat) acc =
+      acc * 256 ^ bs.length + bs.foldl (fun n b => n * 256 + b.toNat) 0 := by
+  induction bs generalizing acc with
+  | nil => simp
+  | cons b bs ih =>
+    simp only [List.foldl_cons, List.length_cons]
+    rw [ih, ih (0 * 256 + b.toNat)]
+    simp [Nat.pow_succ, Nat.mul_add, Nat.mul_assoc, Nat.add_assoc, Nat.mul_comm]
+
+theorem beNat_append (a b : List UInt8) : beNat (a ++ b) = beNat a * 256 ^ b.length + beNat b := by
+  unfold beNat
+  rw [List.foldl_append, foldl_be]
+
+theorem beNat_cons (b : UInt8) (bs : List UInt8) :
+    beNat (b :: bs) = b.toNat * 256 ^ bs.length + beNat bs := by
+  unfold beNat
+  rw [List.foldl_cons, foldl_be]
+  simp
+
+theorem beNat_lt (bs : List UInt8) : beNat bs < 256 ^ bs.length := by
+  induction bs with
+  | nil => simp [beNat]
+  | cons b bs ih =>
+    rw [beNat_cons, List.length_cons, Nat.pow_succ]
+    have hb : b.toNat ≤ 255 := by have := b.toNat_lt; omega
+    have h1 : b.toNat * 256 ^ bs.length ≤ 255 * 256 ^ bs.length := Nat.mul_le_mul_right _ hb
+    omega
+
+theorem beBytes_succ (w n : Nat) :
+    beBytes (w + 1) n = (n / 256 ^ w % 256).toUInt8 :: beBytes w n := by
+  simp [beBytes, List.range_succ]
+
+theorem toNat_toUInt8 (n : Nat) (h : n < 256) : n.toUInt8.toNat = n := by
+  simp [Nat.toUInt8, Nat.mod_eq_of_lt h]
+
+theorem beNat_beBytes (w n : Nat) : beNat (beBytes w n) = n % 256 ^ w := by
+  induction w with
+  | zero => simp [beBytes, beNat, Nat.mod_one]
+  | succ w ih =>
+    rw [beBytes_succ, beNat_cons, ih, beBytes_length,
+      toNat_toUInt8 _ (Nat.mod_lt _ (by decide)), Nat.pow_succ, Nat.mod_mul,
+      Nat.mul_comm (n / 256 ^ w % 256)]
+    omega
+
+theorem beNat_beBytes_of_lt (w n : Nat) (h : n < 256 ^ w) : beNat (beBytes w n) = n := by
+  rw [beNat_beBytes, Nat.mod_eq_of_lt h]
+
+theorem beBytes_add (w a n : Nat) : beBytes w (a * 256 ^ w + n) = beBytes w n := by
+  unfold beBytes
+  apply List.map_congr_left
+  intro i hi
+  simp only [List.mem_reverse, List.mem_range] at hi
+  congr 1
+  obtain ⟨d, rfl⟩ : ∃ d, w = i + d + 1 := ⟨w - i - 1, by omega⟩
+  rw [show i + d + 1 = i + (d + 1) by omega, Nat.pow_add, ← Nat.mul_assoc,
+    Nat.mul_right_comm a, Nat.add_comm, Nat.add_mul_div_right _ _ (Nat.pow_pos (by decide)),
+    Nat.pow_succ, ← Nat.mul_assoc, Nat.add_mul_mod_self_right]
+
+theorem beBytes_beNat (c : List UInt8) : beBytes c.length (beNat c) = c := by
+  induction c with
+  | nil => rfl
+  | cons b c ih =>
+    rw [List.length_cons, beBytes_succ, beNat_cons]
+    have hc := beNat_lt c
+    have hdiv : (b.toNat * 256 ^ c.length + beNat c) / 256 ^ c.length = b.toNat := by
+      rw [Nat.add_comm, Nat.add_mul_div_right _ _ (Nat.pow_pos (by decide)),
+        Nat.div_eq_of_lt hc, Nat.zero_add]
+    rw [hdiv, Nat.mod_eq_of_lt b.toNat_lt, beBytes_add, ih]
+    simp
+
+theorem readBE_iff (w : Nat) (b : List UInt8) (n : Nat) (r : List UInt8) :
+    readBE w b = some (n, r) ↔ n < 256 ^ w ∧ b = beBytes w n ++ r := by
+  unfold readBE
+  constructor
+  · intro h
+    simp only [Option.map_eq_some_iff, Prod.exists] at h
+    obtain ⟨c, r', hc, he⟩ := h
+    simp only [Prod.mk.injEq] at he
+    obtain ⟨rfl, rfl⟩ := he
+    obtain ⟨hl, rfl⟩ := (take?_eq _ _ _ _).mp hc
+    subst hl
+    exact ⟨beNat_lt c, by rw [bigEndian_eq, beBytes_beNat]⟩
+  · rintro ⟨hn, rfl⟩
+    have := (take?_eq w (beBytes w n ++ r) (beBytes w n) r).mpr ⟨beBytes_length _ _, rfl⟩
+    rw [this]
+    simp [bigEndian_eq, beNat_beBytes_of_lt _ _ hn]
+
+theorem readBE_append (w n : Nat) (r : List UInt8) (hn : n < 256 ^ w) :
+    readBE w (beBytes w n ++ r) = some (n, r) :=
+  (readBE_iff _ _ _ _).mpr ⟨hn, rfl⟩
+
+theorem guard_some (p : Prop) [Decidable p] (u : Unit) :
+    (guard p : Option Unit) = some u ↔ p := by
+  unfold guard
+  split <;> simp_all [failure, pure]
+
+theorem take?_append' (w : Nat) (c r : List UInt8) (h : c.length = w) :
+    take? w (c ++ r) = some (c, r) :=
+  (take?_eq _ _ _ _).mpr ⟨h, rfl⟩
+
+theorem beBytes_one (a : Nat) (h : a < 256) : beBytes 1 a = [a.toUInt8] := by
+  simp [beBytes, Nat.mod_eq_of_lt h]
+
+theorem readBE_one (a : UInt8) (r : List UInt8) : readBE 1 (a :: r) = some (a.toNat, r) := by
+  have := readBE_append 1 a.toNat r (by simpa using a.toNat_lt)
+  rw [beBytes_one _ a.toNat_lt] at this
+  simpa using this
+
+end SqliteProofs