gzfs.lean

本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。

1import ZlibF.Zlib.gzfs
2
3/-!
4# Closed forms of the `vsnprintf` calls of the gz files
5
6`gz_error`, `gz_open`, `gzopen`, `gzopen64` and `gzdopen` call `vsnprintf` with three formats only: `"%s"`,
7`"%s%s%s"` and `"<fd:%d>"`. For each of them the lemmas below give the output (`formatBytes`) in closed form, and
8`vsnprintf_ret` says that the call does not fault and returns the length that the full output has (C99), whatever the
9buffer size, when the destination range is inside a writable block; the bytes written are the first `size - 1` bytes of
10the output followed by a NUL.
11
12The strings the `%s` conversions read are given by hypotheses of the form `cstring p h = .ok (s, h)` (the bytes before
13the first NUL), the format by `cstring fmt h = .ok (f, h)`.
14-/
15
16namespace Zlib.GzFs.Proofs
17open C Zlib.GzFs
18
19/-- The bytes of the decimal text of an integer, with a minus sign for a negative one. -/
20def decBytes (z : Int) : Array UInt8 :=
21  (if z < 0 then #[45] else #[]) ++ ((Nat.toDigits 10 z.natAbs).toArray.map fun c => c.toNat.toUInt8)
22
23theorem parse_s : parseSpec #[37, 115] 1 = some ({ conv := 115 }, 2) := by decide
24theorem parse_fd : parseSpec #[60, 102, 100, 58, 37, 100, 62] 5 = some ({ conv := 100 }, 6) := by decide
25theorem parse_sss1 : parseSpec #[37, 115, 37, 115, 37, 115] 1 = some ({ conv := 115 }, 2) := by decide
26theorem parse_sss2 : parseSpec #[37, 115, 37, 115, 37, 115] 3 = some ({ conv := 115 }, 4) := by decide
27theorem parse_sss3 : parseSpec #[37, 115, 37, 115, 37, 115] 5 = some ({ conv := 115 }, 6) := by decide
28
29
30theorem heapStr_of {h : Heap} {p : BPtr} {s : Array UInt8} (hs : cstring p h = .ok (s, h)) : heapStr h p = some s := by
31  simp [heapStr, hs]
32
33/-- `printf("%s", p)` is the string at `p`. -/
34theorem formatBytes_s {h : Heap} {p : BPtr} {s : Array UInt8} (hp : p ≠ .null) (hs : cstring p h = .ok (s, h)) :
35    formatBytes #[37, 115] [.str p] h = .ok (s, h) := by
36  have hr := heapStr_of hs
37  have hpb : (p == Ptr.null) = false := by simpa using hp
38  simp [formatBytes, formatGo, parse_s, argStr, hr, hpb, pad]
39
40end Zlib.GzFs.Proofs